case refine'_5
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ ∀ (x : ↑I), ↑x = 1 / 2 → 2 * ↑x = 1
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ Continuous transReflReparamAux
refine' continuous_if_le _ _ (Continuous.continuousOn _) (Continuous.continuousOn _) _ <;>
  [continuity; continuity; continuity; continuity; skip]
case refine'_5
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I
hx : ↑x = 1 / 2
⊢ 2 * ↑x = 1
case refine'_5
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ ∀ (x : ↑I), ↑x = 1 / 2 → 2 * ↑x = 1
intro x hx
no goals
case refine'_5
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I
hx : ↑x = 1 / 2
⊢ 2 * ↑x = 1
simp [hx]