case refine'_9
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I
hx : ↑x = 1 / 4
⊢ 2 * ↑x = if ↑x ≤ 1 / 2 then ↑x + 1 / 4 else 1 / 2 * (↑x + 1)
case refine'_9
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ ∀ (x : ↑I), ↑x = 1 / 4 → 2 * ↑x = if ↑x ≤ 1 / 2 then ↑x + 1 / 4 else 1 / 2 * (↑x + 1)
intro x hx
case refine'_9
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I
hx : ↑x = 1 / 4
⊢ 2 * 4⁻¹ = if 4⁻¹ ≤ 2⁻¹ then 4⁻¹ + 4⁻¹ else 2⁻¹ * (4⁻¹ + 1)
case refine'_9
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I
hx : ↑x = 1 / 4
⊢ 2 * ↑x = if ↑x ≤ 1 / 2 then ↑x + 1 / 4 else 1 / 2 * (↑x + 1)
simp [hx]
no goals
case refine'_9
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I
hx : ↑x = 1 / 4
⊢ 2 * 4⁻¹ = if 4⁻¹ ≤ 2⁻¹ then 4⁻¹ + 4⁻¹ else 2⁻¹ * (4⁻¹ + 1)
norm_num