X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ (if 1 ≤ 4⁻¹ then 2 else if 1 ≤ 2⁻¹ then 1 + 4⁻¹ else 2⁻¹ * (1 + 1)) = 1
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ transAssocReparamAux 1 = 1
simp [transAssocReparamAux]
no goals
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ (if 1 ≤ 4⁻¹ then 2 else if 1 ≤ 2⁻¹ then 1 + 4⁻¹ else 2⁻¹ * (1 + 1)) = 1
norm_num