X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ 1 ≤ 2⁻¹ → False
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ transReflReparamAux 1 = 1
simp [transReflReparamAux]
no goals
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ 1 ≤ 2⁻¹ → False
norm_num