theorem Units.eq_imp_equiv {μ : Sort u_1} [Setoid μ] {u1 u2 : μ} (h : u1 = u2) : u1 ≈ u2

def Units.tacticSimp_dim : Lean.ParserDescr

macro that reduces expressions involving dimensions or units by simplifying using the lemmas tagged with the attributes dimension_set, derived_unit_set or base_unit_set.

Equations

• Units.tacticSimp_dim = Lean.ParserDescr.node `Units.tacticSimp_dim 1024 (Lean.ParserDescr.nonReservedSymbol "simp_dim" false)

def Units.tacticAuto_equiv : Lean.ParserDescr

Helper tactic that tries to prove equalities or equivalences between dimensions or units. It tries the following strategies in order:

1. propositional equality check using module tactic
2. propositional equivalence on units using module tactic

Equations

• Units.tacticAuto_equiv = Lean.ParserDescr.node `Units.tacticAuto_equiv 1024 (Lean.ParserDescr.nonReservedSymbol "auto_equiv" false)

def Units.tacticAuto_dim : Lean.ParserDescr

Helper tactic that tries to prove equalities between dimensions or units. It tries the following strategies in order:

1. propositional equality check using rfl
2. simplification using simp with the lemmas tagged with the attribute dimension_set or derived_unit_set. so we don't use native_decide that would require to trust the compiler.

Equations

• Units.tacticAuto_dim = Lean.ParserDescr.node `Units.tacticAuto_dim 1024 (Lean.ParserDescr.nonReservedSymbol "auto_dim" false)