[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c : CU X
n : ℕ
x : X
hx : x ∈ c.C
⊢ approx n c x = 0
[PROOFSTEP]
induction' n with n ihn generalizing c
[GOAL]
case zero
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
hx✝ : x ∈ c✝.C
c : CU X
hx : x ∈ c.C
⊢ approx Nat.zero c x = 0
[PROOFSTEP]
exact indicator_of_not_mem (fun (hU : x ∈ c.Uᶜ) => hU <| c.subset hx) _
[GOAL]
case succ
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
hx✝ : x ∈ c✝.C
n : ℕ
ihn : ∀ (c : CU X), x ∈ c.C → approx n c x = 0
c : CU X
hx : x ∈ c.C
⊢ approx (Nat.succ n) c x = 0
[PROOFSTEP]
simp only [approx]
[GOAL]
case succ
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
hx✝ : x ∈ c✝.C
n : ℕ
ihn : ∀ (c : CU X), x ∈ c.C → approx n c x = 0
c : CU X
hx : x ∈ c.C
⊢ midpoint ℝ (approx n (left c) x) (approx n (right c) x) = 0
[PROOFSTEP]
rw [ihn, ihn, midpoint_self]
[GOAL]
case succ.hx
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
hx✝ : x ∈ c✝.C
n : ℕ
ihn : ∀ (c : CU X), x ∈ c.C → approx n c x = 0
c : CU X
hx : x ∈ c.C
⊢ x ∈ (right c).C
case succ.hx
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
hx✝ : x ∈ c✝.C
n : ℕ
ihn : ∀ (c : CU X), x ∈ c.C → approx n c x = 0
c : CU X
hx : x ∈ c.C
⊢ x ∈ (left c).C
[PROOFSTEP]
exacts [c.subset_right_C hx, hx]
[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c : CU X
n : ℕ
x : X
hx : ¬x ∈ c.U
⊢ approx n c x = 1
[PROOFSTEP]
induction' n with n ihn generalizing c
[GOAL]
case zero
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
hx✝ : ¬x ∈ c✝.U
c : CU X
hx : ¬x ∈ c.U
⊢ approx Nat.zero c x = 1
[PROOFSTEP]
rw [← mem_compl_iff] at hx 
[GOAL]
case zero
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
hx✝ : ¬x ∈ c✝.U
c : CU X
hx : x ∈ c.Uᶜ
⊢ approx Nat.zero c x = 1
[PROOFSTEP]
exact indicator_of_mem hx _
[GOAL]
case succ
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
hx✝ : ¬x ∈ c✝.U
n : ℕ
ihn : ∀ (c : CU X), ¬x ∈ c.U → approx n c x = 1
c : CU X
hx : ¬x ∈ c.U
⊢ approx (Nat.succ n) c x = 1
[PROOFSTEP]
simp only [approx]
[GOAL]
case succ
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
hx✝ : ¬x ∈ c✝.U
n : ℕ
ihn : ∀ (c : CU X), ¬x ∈ c.U → approx n c x = 1
c : CU X
hx : ¬x ∈ c.U
⊢ midpoint ℝ (approx n (left c) x) (approx n (right c) x) = 1
[PROOFSTEP]
rw [ihn, ihn, midpoint_self]
[GOAL]
case succ.hx
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
hx✝ : ¬x ∈ c✝.U
n : ℕ
ihn : ∀ (c : CU X), ¬x ∈ c.U → approx n c x = 1
c : CU X
hx : ¬x ∈ c.U
⊢ ¬x ∈ (right c).U
case succ.hx
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
hx✝ : ¬x ∈ c✝.U
n : ℕ
ihn : ∀ (c : CU X), ¬x ∈ c.U → approx n c x = 1
c : CU X
hx : ¬x ∈ c.U
⊢ ¬x ∈ (left c).U
[PROOFSTEP]
exacts [hx, fun hU => hx <| c.left_U_subset hU]
[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c : CU X
n : ℕ
x : X
⊢ 0 ≤ approx n c x
[PROOFSTEP]
induction' n with n ihn generalizing c
[GOAL]
case zero
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
c : CU X
⊢ 0 ≤ approx Nat.zero c x
[PROOFSTEP]
exact indicator_nonneg (fun _ _ => zero_le_one) _
[GOAL]
case succ
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
n : ℕ
ihn : ∀ (c : CU X), 0 ≤ approx n c x
c : CU X
⊢ 0 ≤ approx (Nat.succ n) c x
[PROOFSTEP]
simp only [approx, midpoint_eq_smul_add, invOf_eq_inv]
[GOAL]
case succ
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
n : ℕ
ihn : ∀ (c : CU X), 0 ≤ approx n c x
c : CU X
⊢ 0 ≤ 2⁻¹ • (approx n (left c) x + approx n (right c) x)
[PROOFSTEP]
refine' mul_nonneg (inv_nonneg.2 zero_le_two) (add_nonneg _ _)
[GOAL]
case succ.refine'_1
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
n : ℕ
ihn : ∀ (c : CU X), 0 ≤ approx n c x
c : CU X
⊢ 0 ≤ approx n (left c) x
[PROOFSTEP]
apply ihn
[GOAL]
case succ.refine'_2
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
n : ℕ
ihn : ∀ (c : CU X), 0 ≤ approx n c x
c : CU X
⊢ 0 ≤ approx n (right c) x
[PROOFSTEP]
apply ihn
[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c : CU X
n : ℕ
x : X
⊢ approx n c x ≤ 1
[PROOFSTEP]
induction' n with n ihn generalizing c
[GOAL]
case zero
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
c : CU X
⊢ approx Nat.zero c x ≤ 1
[PROOFSTEP]
exact indicator_apply_le' (fun _ => le_rfl) fun _ => zero_le_one
[GOAL]
case succ
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
n : ℕ
ihn : ∀ (c : CU X), approx n c x ≤ 1
c : CU X
⊢ approx (Nat.succ n) c x ≤ 1
[PROOFSTEP]
simp only [approx, midpoint_eq_smul_add, invOf_eq_inv, smul_eq_mul, ← div_eq_inv_mul]
[GOAL]
case succ
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
n : ℕ
ihn : ∀ (c : CU X), approx n c x ≤ 1
c : CU X
⊢ (approx n (left c) x + approx n (right c) x) / 2 ≤ 1
[PROOFSTEP]
have := add_le_add (ihn (left c)) (ihn (right c))
[GOAL]
case succ
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
n : ℕ
ihn : ∀ (c : CU X), approx n c x ≤ 1
c : CU X
this : approx n (left c) x + approx n (right c) x ≤ 1 + 1
⊢ (approx n (left c) x + approx n (right c) x) / 2 ≤ 1
[PROOFSTEP]
norm_num at this 
[GOAL]
case succ
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
n : ℕ
ihn : ∀ (c : CU X), approx n c x ≤ 1
c : CU X
this : approx n (left c) x + approx n (right c) x ≤ 2
⊢ (approx n (left c) x + approx n (right c) x) / 2 ≤ 1
[PROOFSTEP]
exact Iff.mpr (div_le_one zero_lt_two) this
[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c₁ c₂ : CU X
h : c₁.U ⊆ c₂.C
n₁ n₂ : ℕ
x : X
⊢ approx n₂ c₂ x ≤ approx n₁ c₁ x
[PROOFSTEP]
by_cases hx : x ∈ c₁.U
[GOAL]
case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c₁ c₂ : CU X
h : c₁.U ⊆ c₂.C
n₁ n₂ : ℕ
x : X
hx : x ∈ c₁.U
⊢ approx n₂ c₂ x ≤ approx n₁ c₁ x
[PROOFSTEP]
calc
  approx n₂ c₂ x = 0 := approx_of_mem_C _ _ (h hx)
  _ ≤ approx n₁ c₁ x := approx_nonneg _ _ _
[GOAL]
case neg
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c₁ c₂ : CU X
h : c₁.U ⊆ c₂.C
n₁ n₂ : ℕ
x : X
hx : ¬x ∈ c₁.U
⊢ approx n₂ c₂ x ≤ approx n₁ c₁ x
[PROOFSTEP]
calc
  approx n₂ c₂ x ≤ 1 := approx_le_one _ _ _
  _ = approx n₁ c₁ x := (approx_of_nmem_U _ _ hx).symm
[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c : CU X
n : ℕ
x : X
⊢ approx n c x ∈ Icc (approx n (right c) x) (approx n (left c) x)
[PROOFSTEP]
induction' n with n ihn generalizing c
[GOAL]
case zero
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
c : CU X
⊢ approx Nat.zero c x ∈ Icc (approx Nat.zero (right c) x) (approx Nat.zero (left c) x)
[PROOFSTEP]
exact ⟨le_rfl, indicator_le_indicator_of_subset (compl_subset_compl.2 c.left_U_subset) (fun _ => zero_le_one) _⟩
[GOAL]
case succ
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
n : ℕ
ihn : ∀ (c : CU X), approx n c x ∈ Icc (approx n (right c) x) (approx n (left c) x)
c : CU X
⊢ approx (Nat.succ n) c x ∈ Icc (approx (Nat.succ n) (right c) x) (approx (Nat.succ n) (left c) x)
[PROOFSTEP]
simp only [approx, mem_Icc]
[GOAL]
case succ
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
n : ℕ
ihn : ∀ (c : CU X), approx n c x ∈ Icc (approx n (right c) x) (approx n (left c) x)
c : CU X
⊢ midpoint ℝ (approx n (left (right c)) x) (approx n (right (right c)) x) ≤
      midpoint ℝ (approx n (left c) x) (approx n (right c) x) ∧
    midpoint ℝ (approx n (left c) x) (approx n (right c) x) ≤
      midpoint ℝ (approx n (left (left c)) x) (approx n (right (left c)) x)
[PROOFSTEP]
refine' ⟨midpoint_le_midpoint _ (ihn _).1, midpoint_le_midpoint (ihn _).2 _⟩
[GOAL]
case succ.refine'_1
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
n : ℕ
ihn : ∀ (c : CU X), approx n c x ∈ Icc (approx n (right c) x) (approx n (left c) x)
c : CU X
⊢ approx n (left (right c)) x ≤ approx n (left c) x
[PROOFSTEP]
apply approx_le_approx_of_U_sub_C
[GOAL]
case succ.refine'_2
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
n : ℕ
ihn : ∀ (c : CU X), approx n c x ∈ Icc (approx n (right c) x) (approx n (left c) x)
c : CU X
⊢ approx n (right c) x ≤ approx n (right (left c)) x
[PROOFSTEP]
apply approx_le_approx_of_U_sub_C
[GOAL]
case succ.refine'_1.h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
n : ℕ
ihn : ∀ (c : CU X), approx n c x ∈ Icc (approx n (right c) x) (approx n (left c) x)
c : CU X
⊢ (left c).U ⊆ (left (right c)).C
case succ.refine'_2.h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
n : ℕ
ihn : ∀ (c : CU X), approx n c x ∈ Icc (approx n (right c) x) (approx n (left c) x)
c : CU X
⊢ (right (left c)).U ⊆ (right c).C
[PROOFSTEP]
exacts [subset_closure, subset_closure]
[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c : CU X
n : ℕ
x : X
⊢ approx n c x ≤ approx (n + 1) c x
[PROOFSTEP]
induction' n with n ihn generalizing c
[GOAL]
case zero
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
c : CU X
⊢ approx Nat.zero c x ≤ approx (Nat.zero + 1) c x
[PROOFSTEP]
simp only [approx, right_U, right_le_midpoint]
[GOAL]
case zero
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
c : CU X
⊢ indicator c.Uᶜ 1 x ≤ indicator (left c).Uᶜ 1 x
[PROOFSTEP]
exact (approx_mem_Icc_right_left c 0 x).2
[GOAL]
case succ
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
n : ℕ
ihn : ∀ (c : CU X), approx n c x ≤ approx (n + 1) c x
c : CU X
⊢ approx (Nat.succ n) c x ≤ approx (Nat.succ n + 1) c x
[PROOFSTEP]
rw [approx, approx]
[GOAL]
case succ
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
n : ℕ
ihn : ∀ (c : CU X), approx n c x ≤ approx (n + 1) c x
c : CU X
⊢ midpoint ℝ (approx n (left c) x) (approx n (right c) x) ≤
    midpoint ℝ (approx (n + 1) (left c) x) (approx (n + 1) (right c) x)
[PROOFSTEP]
exact midpoint_le_midpoint (ihn _) (ihn _)
[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c : CU X
x : X
h : x ∈ c.C
⊢ CU.lim c x = 0
[PROOFSTEP]
simp only [CU.lim, approx_of_mem_C, h, ciSup_const]
[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c : CU X
x : X
h : ¬x ∈ c.U
⊢ CU.lim c x = 1
[PROOFSTEP]
simp only [CU.lim, approx_of_nmem_U c _ h, ciSup_const]
[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c : CU X
x : X
⊢ CU.lim c x = midpoint ℝ (CU.lim (left c) x) (CU.lim (right c) x)
[PROOFSTEP]
refine' tendsto_nhds_unique (c.tendsto_approx_atTop x) ((tendsto_add_atTop_iff_nat 1).1 _)
[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c : CU X
x : X
⊢ Tendsto (fun n => approx (n + 1) c x) atTop (𝓝 (midpoint ℝ (CU.lim (left c) x) (CU.lim (right c) x)))
[PROOFSTEP]
simp only [approx]
[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c : CU X
x : X
⊢ Tendsto (fun n => midpoint ℝ (approx (Nat.add n 0) (left c) x) (approx (Nat.add n 0) (right c) x)) atTop
    (𝓝 (midpoint ℝ (CU.lim (left c) x) (CU.lim (right c) x)))
[PROOFSTEP]
exact (c.left.tendsto_approx_atTop x).midpoint (c.right.tendsto_approx_atTop x)
[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c : CU X
⊢ Continuous (CU.lim c)
[PROOFSTEP]
obtain ⟨h0, h1234, h1⟩ : 0 < (2⁻¹ : ℝ) ∧ (2⁻¹ : ℝ) < 3 / 4 ∧ (3 / 4 : ℝ) < 1 := by norm_num
[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c : CU X
⊢ 0 < 2⁻¹ ∧ 2⁻¹ < 3 / 4 ∧ 3 / 4 < 1
[PROOFSTEP]
norm_num
[GOAL]
case intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c : CU X
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
⊢ Continuous (CU.lim c)
[PROOFSTEP]
refine'
  continuous_iff_continuousAt.2 fun x =>
    (Metric.nhds_basis_closedBall_pow (h0.trans h1234) h1).tendsto_right_iff.2 fun n _ => _
[GOAL]
case intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c : CU X
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
n : ℕ
x✝ : True
⊢ ∀ᶠ (x_1 : X) in 𝓝 x, CU.lim c x_1 ∈ Metric.closedBall (CU.lim c x) ((3 / 4) ^ n)
[PROOFSTEP]
simp only [Metric.mem_closedBall]
[GOAL]
case intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c : CU X
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
n : ℕ
x✝ : True
⊢ ∀ᶠ (x_1 : X) in 𝓝 x, dist (CU.lim c x_1) (CU.lim c x) ≤ (3 / 4) ^ n
[PROOFSTEP]
induction' n with n ihn generalizing c
[GOAL]
case intro.intro.zero
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
c : CU X
⊢ ∀ᶠ (x_1 : X) in 𝓝 x, dist (CU.lim c x_1) (CU.lim c x) ≤ (3 / 4) ^ Nat.zero
[PROOFSTEP]
refine' eventually_of_forall fun y => _
[GOAL]
case intro.intro.zero
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
c : CU X
y : X
⊢ dist (CU.lim c y) (CU.lim c x) ≤ (3 / 4) ^ Nat.zero
[PROOFSTEP]
rw [pow_zero]
[GOAL]
case intro.intro.zero
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
c : CU X
y : X
⊢ dist (CU.lim c y) (CU.lim c x) ≤ 1
[PROOFSTEP]
exact Real.dist_le_of_mem_Icc_01 (c.lim_mem_Icc _) (c.lim_mem_Icc _)
[GOAL]
case intro.intro.succ
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
ihn : ∀ (c : CU X), ∀ᶠ (x_1 : X) in 𝓝 x, dist (CU.lim c x_1) (CU.lim c x) ≤ (3 / 4) ^ n
c : CU X
⊢ ∀ᶠ (x_1 : X) in 𝓝 x, dist (CU.lim c x_1) (CU.lim c x) ≤ (3 / 4) ^ Nat.succ n
[PROOFSTEP]
by_cases hxl : x ∈ c.left.U
[GOAL]
case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
ihn : ∀ (c : CU X), ∀ᶠ (x_1 : X) in 𝓝 x, dist (CU.lim c x_1) (CU.lim c x) ≤ (3 / 4) ^ n
c : CU X
hxl : x ∈ (left c).U
⊢ ∀ᶠ (x_1 : X) in 𝓝 x, dist (CU.lim c x_1) (CU.lim c x) ≤ (3 / 4) ^ Nat.succ n
[PROOFSTEP]
filter_upwards [IsOpen.mem_nhds c.left.open_U hxl, ihn c.left] with _ hyl hyd
[GOAL]
case h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
ihn : ∀ (c : CU X), ∀ᶠ (x_1 : X) in 𝓝 x, dist (CU.lim c x_1) (CU.lim c x) ≤ (3 / 4) ^ n
c : CU X
hxl : x ∈ (left c).U
a✝ : X
hyl : a✝ ∈ (left c).U
hyd : dist (CU.lim (left c) a✝) (CU.lim (left c) x) ≤ (3 / 4) ^ n
⊢ dist (CU.lim c a✝) (CU.lim c x) ≤ (3 / 4) ^ Nat.succ n
[PROOFSTEP]
rw [pow_succ, c.lim_eq_midpoint, c.lim_eq_midpoint, c.right.lim_of_mem_C _ (c.left_U_subset_right_C hyl),
  c.right.lim_of_mem_C _ (c.left_U_subset_right_C hxl)]
[GOAL]
case h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
ihn : ∀ (c : CU X), ∀ᶠ (x_1 : X) in 𝓝 x, dist (CU.lim c x_1) (CU.lim c x) ≤ (3 / 4) ^ n
c : CU X
hxl : x ∈ (left c).U
a✝ : X
hyl : a✝ ∈ (left c).U
hyd : dist (CU.lim (left c) a✝) (CU.lim (left c) x) ≤ (3 / 4) ^ n
⊢ dist (midpoint ℝ (CU.lim (left c) a✝) 0) (midpoint ℝ (CU.lim (left c) x) 0) ≤ 3 / 4 * (3 / 4) ^ n
[PROOFSTEP]
refine' (dist_midpoint_midpoint_le _ _ _ _).trans _
[GOAL]
case h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
ihn : ∀ (c : CU X), ∀ᶠ (x_1 : X) in 𝓝 x, dist (CU.lim c x_1) (CU.lim c x) ≤ (3 / 4) ^ n
c : CU X
hxl : x ∈ (left c).U
a✝ : X
hyl : a✝ ∈ (left c).U
hyd : dist (CU.lim (left c) a✝) (CU.lim (left c) x) ≤ (3 / 4) ^ n
⊢ (dist (CU.lim (left c) a✝) (CU.lim (left c) x) + dist 0 0) / 2 ≤ 3 / 4 * (3 / 4) ^ n
[PROOFSTEP]
rw [dist_self, add_zero, div_eq_inv_mul]
[GOAL]
case h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
ihn : ∀ (c : CU X), ∀ᶠ (x_1 : X) in 𝓝 x, dist (CU.lim c x_1) (CU.lim c x) ≤ (3 / 4) ^ n
c : CU X
hxl : x ∈ (left c).U
a✝ : X
hyl : a✝ ∈ (left c).U
hyd : dist (CU.lim (left c) a✝) (CU.lim (left c) x) ≤ (3 / 4) ^ n
⊢ 2⁻¹ * dist (CU.lim (left c) a✝) (CU.lim (left c) x) ≤ 3 / 4 * (3 / 4) ^ n
[PROOFSTEP]
gcongr
[GOAL]
case neg
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
ihn : ∀ (c : CU X), ∀ᶠ (x_1 : X) in 𝓝 x, dist (CU.lim c x_1) (CU.lim c x) ≤ (3 / 4) ^ n
c : CU X
hxl : ¬x ∈ (left c).U
⊢ ∀ᶠ (x_1 : X) in 𝓝 x, dist (CU.lim c x_1) (CU.lim c x) ≤ (3 / 4) ^ Nat.succ n
[PROOFSTEP]
replace hxl : x ∈ c.left.right.Cᶜ
[GOAL]
case hxl
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
ihn : ∀ (c : CU X), ∀ᶠ (x_1 : X) in 𝓝 x, dist (CU.lim c x_1) (CU.lim c x) ≤ (3 / 4) ^ n
c : CU X
hxl : ¬x ∈ (left c).U
⊢ x ∈ (right (left c)).Cᶜ
case neg
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
ihn : ∀ (c : CU X), ∀ᶠ (x_1 : X) in 𝓝 x, dist (CU.lim c x_1) (CU.lim c x) ≤ (3 / 4) ^ n
c : CU X
hxl : x ∈ (right (left c)).Cᶜ
⊢ ∀ᶠ (x_1 : X) in 𝓝 x, dist (CU.lim c x_1) (CU.lim c x) ≤ (3 / 4) ^ Nat.succ n
[PROOFSTEP]
exact compl_subset_compl.2 c.left.right.subset hxl
[GOAL]
case neg
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
ihn : ∀ (c : CU X), ∀ᶠ (x_1 : X) in 𝓝 x, dist (CU.lim c x_1) (CU.lim c x) ≤ (3 / 4) ^ n
c : CU X
hxl : x ∈ (right (left c)).Cᶜ
⊢ ∀ᶠ (x_1 : X) in 𝓝 x, dist (CU.lim c x_1) (CU.lim c x) ≤ (3 / 4) ^ Nat.succ n
[PROOFSTEP]
filter_upwards [IsOpen.mem_nhds (isOpen_compl_iff.2 c.left.right.closed_C) hxl, ihn c.left.right, ihn c.right] with y
  hyl hydl hydr
[GOAL]
case h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
ihn : ∀ (c : CU X), ∀ᶠ (x_1 : X) in 𝓝 x, dist (CU.lim c x_1) (CU.lim c x) ≤ (3 / 4) ^ n
c : CU X
hxl : x ∈ (right (left c)).Cᶜ
y : X
hyl : y ∈ (right (left c)).Cᶜ
hydl : dist (CU.lim (right (left c)) y) (CU.lim (right (left c)) x) ≤ (3 / 4) ^ n
hydr : dist (CU.lim (right c) y) (CU.lim (right c) x) ≤ (3 / 4) ^ n
⊢ dist (CU.lim c y) (CU.lim c x) ≤ (3 / 4) ^ Nat.succ n
[PROOFSTEP]
replace hxl : x ∉ c.left.left.U
[GOAL]
case hxl
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
ihn : ∀ (c : CU X), ∀ᶠ (x_1 : X) in 𝓝 x, dist (CU.lim c x_1) (CU.lim c x) ≤ (3 / 4) ^ n
c : CU X
hxl : x ∈ (right (left c)).Cᶜ
y : X
hyl : y ∈ (right (left c)).Cᶜ
hydl : dist (CU.lim (right (left c)) y) (CU.lim (right (left c)) x) ≤ (3 / 4) ^ n
hydr : dist (CU.lim (right c) y) (CU.lim (right c) x) ≤ (3 / 4) ^ n
⊢ ¬x ∈ (left (left c)).U
case h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
ihn : ∀ (c : CU X), ∀ᶠ (x_1 : X) in 𝓝 x, dist (CU.lim c x_1) (CU.lim c x) ≤ (3 / 4) ^ n
c : CU X
y : X
hyl : y ∈ (right (left c)).Cᶜ
hydl : dist (CU.lim (right (left c)) y) (CU.lim (right (left c)) x) ≤ (3 / 4) ^ n
hydr : dist (CU.lim (right c) y) (CU.lim (right c) x) ≤ (3 / 4) ^ n
hxl : ¬x ∈ (left (left c)).U
⊢ dist (CU.lim c y) (CU.lim c x) ≤ (3 / 4) ^ Nat.succ n
[PROOFSTEP]
exact compl_subset_compl.2 c.left.left_U_subset_right_C hxl
[GOAL]
case h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
ihn : ∀ (c : CU X), ∀ᶠ (x_1 : X) in 𝓝 x, dist (CU.lim c x_1) (CU.lim c x) ≤ (3 / 4) ^ n
c : CU X
y : X
hyl : y ∈ (right (left c)).Cᶜ
hydl : dist (CU.lim (right (left c)) y) (CU.lim (right (left c)) x) ≤ (3 / 4) ^ n
hydr : dist (CU.lim (right c) y) (CU.lim (right c) x) ≤ (3 / 4) ^ n
hxl : ¬x ∈ (left (left c)).U
⊢ dist (CU.lim c y) (CU.lim c x) ≤ (3 / 4) ^ Nat.succ n
[PROOFSTEP]
replace hyl : y ∉ c.left.left.U
[GOAL]
case hyl
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
ihn : ∀ (c : CU X), ∀ᶠ (x_1 : X) in 𝓝 x, dist (CU.lim c x_1) (CU.lim c x) ≤ (3 / 4) ^ n
c : CU X
y : X
hyl : y ∈ (right (left c)).Cᶜ
hydl : dist (CU.lim (right (left c)) y) (CU.lim (right (left c)) x) ≤ (3 / 4) ^ n
hydr : dist (CU.lim (right c) y) (CU.lim (right c) x) ≤ (3 / 4) ^ n
hxl : ¬x ∈ (left (left c)).U
⊢ ¬y ∈ (left (left c)).U
case h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
ihn : ∀ (c : CU X), ∀ᶠ (x_1 : X) in 𝓝 x, dist (CU.lim c x_1) (CU.lim c x) ≤ (3 / 4) ^ n
c : CU X
y : X
hydl : dist (CU.lim (right (left c)) y) (CU.lim (right (left c)) x) ≤ (3 / 4) ^ n
hydr : dist (CU.lim (right c) y) (CU.lim (right c) x) ≤ (3 / 4) ^ n
hxl : ¬x ∈ (left (left c)).U
hyl : ¬y ∈ (left (left c)).U
⊢ dist (CU.lim c y) (CU.lim c x) ≤ (3 / 4) ^ Nat.succ n
[PROOFSTEP]
exact compl_subset_compl.2 c.left.left_U_subset_right_C hyl
[GOAL]
case h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
ihn : ∀ (c : CU X), ∀ᶠ (x_1 : X) in 𝓝 x, dist (CU.lim c x_1) (CU.lim c x) ≤ (3 / 4) ^ n
c : CU X
y : X
hydl : dist (CU.lim (right (left c)) y) (CU.lim (right (left c)) x) ≤ (3 / 4) ^ n
hydr : dist (CU.lim (right c) y) (CU.lim (right c) x) ≤ (3 / 4) ^ n
hxl : ¬x ∈ (left (left c)).U
hyl : ¬y ∈ (left (left c)).U
⊢ dist (CU.lim c y) (CU.lim c x) ≤ (3 / 4) ^ Nat.succ n
[PROOFSTEP]
simp only [pow_succ, c.lim_eq_midpoint, c.left.lim_eq_midpoint, c.left.left.lim_of_nmem_U _ hxl,
  c.left.left.lim_of_nmem_U _ hyl]
[GOAL]
case h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
ihn : ∀ (c : CU X), ∀ᶠ (x_1 : X) in 𝓝 x, dist (CU.lim c x_1) (CU.lim c x) ≤ (3 / 4) ^ n
c : CU X
y : X
hydl : dist (CU.lim (right (left c)) y) (CU.lim (right (left c)) x) ≤ (3 / 4) ^ n
hydr : dist (CU.lim (right c) y) (CU.lim (right c) x) ≤ (3 / 4) ^ n
hxl : ¬x ∈ (left (left c)).U
hyl : ¬y ∈ (left (left c)).U
⊢ dist (midpoint ℝ (midpoint ℝ 1 (CU.lim (right (left c)) y)) (CU.lim (right c) y))
      (midpoint ℝ (midpoint ℝ 1 (CU.lim (right (left c)) x)) (CU.lim (right c) x)) ≤
    3 / 4 * (3 / 4) ^ n
[PROOFSTEP]
refine' (dist_midpoint_midpoint_le _ _ _ _).trans _
[GOAL]
case h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
ihn : ∀ (c : CU X), ∀ᶠ (x_1 : X) in 𝓝 x, dist (CU.lim c x_1) (CU.lim c x) ≤ (3 / 4) ^ n
c : CU X
y : X
hydl : dist (CU.lim (right (left c)) y) (CU.lim (right (left c)) x) ≤ (3 / 4) ^ n
hydr : dist (CU.lim (right c) y) (CU.lim (right c) x) ≤ (3 / 4) ^ n
hxl : ¬x ∈ (left (left c)).U
hyl : ¬y ∈ (left (left c)).U
⊢ (dist (midpoint ℝ 1 (CU.lim (right (left c)) y)) (midpoint ℝ 1 (CU.lim (right (left c)) x)) +
        dist (CU.lim (right c) y) (CU.lim (right c) x)) /
      2 ≤
    3 / 4 * (3 / 4) ^ n
[PROOFSTEP]
refine' (div_le_div_of_le_of_nonneg (add_le_add_right (dist_midpoint_midpoint_le _ _ _ _) _) zero_le_two).trans _
[GOAL]
case h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
ihn : ∀ (c : CU X), ∀ᶠ (x_1 : X) in 𝓝 x, dist (CU.lim c x_1) (CU.lim c x) ≤ (3 / 4) ^ n
c : CU X
y : X
hydl : dist (CU.lim (right (left c)) y) (CU.lim (right (left c)) x) ≤ (3 / 4) ^ n
hydr : dist (CU.lim (right c) y) (CU.lim (right c) x) ≤ (3 / 4) ^ n
hxl : ¬x ∈ (left (left c)).U
hyl : ¬y ∈ (left (left c)).U
⊢ ((dist 1 1 + dist (CU.lim (right (left c)) y) (CU.lim (right (left c)) x)) / 2 +
        dist (CU.lim (right c) y) (CU.lim (right c) x)) /
      2 ≤
    3 / 4 * (3 / 4) ^ n
[PROOFSTEP]
rw [dist_self, zero_add]
[GOAL]
case h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
ihn : ∀ (c : CU X), ∀ᶠ (x_1 : X) in 𝓝 x, dist (CU.lim c x_1) (CU.lim c x) ≤ (3 / 4) ^ n
c : CU X
y : X
hydl : dist (CU.lim (right (left c)) y) (CU.lim (right (left c)) x) ≤ (3 / 4) ^ n
hydr : dist (CU.lim (right c) y) (CU.lim (right c) x) ≤ (3 / 4) ^ n
hxl : ¬x ∈ (left (left c)).U
hyl : ¬y ∈ (left (left c)).U
⊢ (dist (CU.lim (right (left c)) y) (CU.lim (right (left c)) x) / 2 + dist (CU.lim (right c) y) (CU.lim (right c) x)) /
      2 ≤
    3 / 4 * (3 / 4) ^ n
[PROOFSTEP]
set r := (3 / 4 : ℝ) ^ n
[GOAL]
case h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
c : CU X
y : X
hxl : ¬x ∈ (left (left c)).U
hyl : ¬y ∈ (left (left c)).U
r : ℝ := (3 / 4) ^ n
ihn : ∀ (c : CU X), ∀ᶠ (x_1 : X) in 𝓝 x, dist (CU.lim c x_1) (CU.lim c x) ≤ r
hydl : dist (CU.lim (right (left c)) y) (CU.lim (right (left c)) x) ≤ r
hydr : dist (CU.lim (right c) y) (CU.lim (right c) x) ≤ r
⊢ (dist (CU.lim (right (left c)) y) (CU.lim (right (left c)) x) / 2 + dist (CU.lim (right c) y) (CU.lim (right c) x)) /
      2 ≤
    3 / 4 * r
[PROOFSTEP]
calc
  _ ≤ (r / 2 + r) / 2 := by gcongr
  _ = _ := by field_simp; ring
[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
c : CU X
y : X
hxl : ¬x ∈ (left (left c)).U
hyl : ¬y ∈ (left (left c)).U
r : ℝ := (3 / 4) ^ n
ihn : ∀ (c : CU X), ∀ᶠ (x_1 : X) in 𝓝 x, dist (CU.lim c x_1) (CU.lim c x) ≤ r
hydl : dist (CU.lim (right (left c)) y) (CU.lim (right (left c)) x) ≤ r
hydr : dist (CU.lim (right c) y) (CU.lim (right c) x) ≤ r
⊢ (dist (CU.lim (right (left c)) y) (CU.lim (right (left c)) x) / 2 + dist (CU.lim (right c) y) (CU.lim (right c) x)) /
      2 ≤
    (r / 2 + r) / 2
[PROOFSTEP]
gcongr
[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
c : CU X
y : X
hxl : ¬x ∈ (left (left c)).U
hyl : ¬y ∈ (left (left c)).U
r : ℝ := (3 / 4) ^ n
ihn : ∀ (c : CU X), ∀ᶠ (x_1 : X) in 𝓝 x, dist (CU.lim c x_1) (CU.lim c x) ≤ r
hydl : dist (CU.lim (right (left c)) y) (CU.lim (right (left c)) x) ≤ r
hydr : dist (CU.lim (right c) y) (CU.lim (right c) x) ≤ r
⊢ (r / 2 + r) / 2 = 3 / 4 * r
[PROOFSTEP]
field_simp
[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
c : CU X
y : X
hxl : ¬x ∈ (left (left c)).U
hyl : ¬y ∈ (left (left c)).U
r : ℝ := (3 / 4) ^ n
ihn : ∀ (c : CU X), ∀ᶠ (x_1 : X) in 𝓝 x, dist (CU.lim c x_1) (CU.lim c x) ≤ r
hydl : dist (CU.lim (right (left c)) y) (CU.lim (right (left c)) x) ≤ r
hydr : dist (CU.lim (right c) y) (CU.lim (right c) x) ≤ r
⊢ (3 ^ n * 4 ^ n + 3 ^ n * (4 ^ n * 2)) * (4 * 4 ^ n) = 3 * 3 ^ n * (4 ^ n * 2 * 4 ^ n * 2)
[PROOFSTEP]
ring
[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
s t : Set X
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
⊢ ∃ f, EqOn (↑f) 0 s ∧ EqOn (↑f) 1 t ∧ ∀ (x : X), ↑f x ∈ Icc 0 1
[PROOFSTEP]
set c : Urysohns.CU X := ⟨s, tᶜ, hs, ht.isOpen_compl, disjoint_left.1 hd⟩
[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
s t : Set X
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
c : Urysohns.CU X :=
  { C := s, U := tᶜ, closed_C := hs, open_U := (_ : IsOpen tᶜ), subset := (_ : ∀ ⦃a : X⦄, a ∈ s → ¬a ∈ t) }
⊢ ∃ f, EqOn (↑f) 0 s ∧ EqOn (↑f) 1 t ∧ ∀ (x : X), ↑f x ∈ Icc 0 1
[PROOFSTEP]
exact ⟨⟨c.lim, c.continuous_lim⟩, c.lim_of_mem_C, fun x hx => c.lim_of_nmem_U _ fun h => h hx, c.lim_mem_Icc⟩
