case refine'_1
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ Continuous fun x => ↑x.snd

case refine'_2
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ Continuous fun x => 1 / 2

case refine'_3
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ Continuous fun x => ↑x.fst * 2 * ↑x.snd

case refine'_4
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ Continuous fun x => ↑x.fst * (2 - 2 * ↑x.snd)

case refine'_5
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ ∀ (x : ↑I × ↑I), ↑x.snd = 1 / 2 → ↑x.fst * 2 * ↑x.snd = ↑x.fst * (2 - 2 * ↑x.snd)
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ Continuous reflTransSymmAux
refine' continuous_if_le _ _ (Continuous.continuousOn _) (Continuous.continuousOn _) _
case refine'_5
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
hx : ↑x.snd = 1 / 2
⊢ ↑x.fst * 2 * ↑x.snd = ↑x.fst * (2 - 2 * ↑x.snd)
case refine'_5
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ ∀ (x : ↑I × ↑I), ↑x.snd = 1 / 2 → ↑x.fst * 2 * ↑x.snd = ↑x.fst * (2 - 2 * ↑x.snd)
intro x hx
case refine'_5
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
hx : ↑x.snd = 1 / 2
⊢ ↑x.fst * (2 * (1 / 2)) = ↑x.fst * (2 - 2 * (1 / 2))
case refine'_5
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
hx : ↑x.snd = 1 / 2
⊢ ↑x.fst * 2 * ↑x.snd = ↑x.fst * (2 - 2 * ↑x.snd)
rw [hx, mul_assoc]
no goals
case refine'_5
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
hx : ↑x.snd = 1 / 2
⊢ ↑x.fst * (2 * (1 / 2)) = ↑x.fst * (2 - 2 * (1 / 2))
norm_num
no goals
case refine'_1
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ Continuous fun x => ↑x.snd
continuity
no goals
case refine'_2
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ Continuous fun x => 1 / 2
continuity
no goals
case refine'_3
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ Continuous fun x => ↑x.fst * 2 * ↑x.snd
continuity
no goals
case refine'_4
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ Continuous fun x => ↑x.fst * (2 - 2 * ↑x.snd)
continuity