-- Mathlib/Topology/UrysohnsLemma.lean
theorem continuous_lim (c : CU P) : Continuous c.lim

Proof state:
case pos
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
ihn : ∀ (c : CU P), ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim x_1) (c.lim x) ≤ (3 / 4) ^ n
c : CU P
hxl : x ∈ c.left.U
⊢ ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim x_1) (c.lim x) ≤ (3 / 4) ^ (n + 1)

Tactic:
filter_upwards [IsOpen.mem_nhds c.left.open_U hxl, ihn c.left] with _ hyl hyd

Result:
case h
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
ihn : ∀ (c : CU P), ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim x_1) (c.lim x) ≤ (3 / 4) ^ n
c : CU P
hxl : x ∈ c.left.U
a✝ : X
hyl : a✝ ∈ c.left.U
hyd : dist (c.left.lim a✝) (c.left.lim x) ≤ (3 / 4) ^ n
⊢ dist (c.lim a✝) (c.lim x) ≤ (3 / 4) ^ (n + 1)

Proof state:
case h
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
ihn : ∀ (c : CU P), ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim x_1) (c.lim x) ≤ (3 / 4) ^ n
c : CU P
y : X
hydl : dist (c.left.right.lim y) (c.left.right.lim x) ≤ (3 / 4) ^ n
hydr : dist (c.right.lim y) (c.right.lim x) ≤ (3 / 4) ^ n
hxl : x ∉ c.left.left.U
hyl : y ∉ c.left.left.U
⊢ (dist (midpoint ℝ 1 (c.left.right.lim y)) (midpoint ℝ 1 (c.left.right.lim x)) +
        dist (c.right.lim y) (c.right.lim x)) /
      2 ≤
    (3 / 4) ^ n * (3 / 4)

Tactic:
refine (div_le_div_of_nonneg_right (add_le_add_right (dist_midpoint_midpoint_le _ _ _ _) _)
  zero_le_two).trans ?_

Result:
case h
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
ihn : ∀ (c : CU P), ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim x_1) (c.lim x) ≤ (3 / 4) ^ n
c : CU P
y : X
hydl : dist (c.left.right.lim y) (c.left.right.lim x) ≤ (3 / 4) ^ n
hydr : dist (c.right.lim y) (c.right.lim x) ≤ (3 / 4) ^ n
hxl : x ∉ c.left.left.U
hyl : y ∉ c.left.left.U
⊢ ((dist 1 1 + dist (c.left.right.lim y) (c.left.right.lim x)) / 2 + dist (c.right.lim y) (c.right.lim x)) / 2 ≤
    (3 / 4) ^ n * (3 / 4)

Proof state:
case h
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
ihn : ∀ (c : CU P), ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim x_1) (c.lim x) ≤ (3 / 4) ^ n
c : CU P
hxl : x ∈ c.left.U
a✝ : X
hyl : a✝ ∈ c.left.U
hyd : dist (c.left.lim a✝) (c.left.lim x) ≤ (3 / 4) ^ n
⊢ 2⁻¹ * dist (c.left.lim a✝) (c.left.lim x) ≤ 3 / 4 * (3 / 4) ^ n

Tactic:
gcongr

Result:
no goals

Proof state:
case intro.intro.succ
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
ihn : ∀ (c : CU P), ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim x_1) (c.lim x) ≤ (3 / 4) ^ n
c : CU P
⊢ ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim x_1) (c.lim x) ≤ (3 / 4) ^ (n + 1)

Tactic:
by_cases hxl : x ∈ c.left.U

Result:
case pos
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
ihn : ∀ (c : CU P), ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim x_1) (c.lim x) ≤ (3 / 4) ^ n
c : CU P
hxl : x ∈ c.left.U
⊢ ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim x_1) (c.lim x) ≤ (3 / 4) ^ (n + 1)

case neg
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
ihn : ∀ (c : CU P), ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim x_1) (c.lim x) ≤ (3 / 4) ^ n
c : CU P
hxl : x ∉ c.left.U
⊢ ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim x_1) (c.lim x) ≤ (3 / 4) ^ (n + 1)

Proof state:
case h
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
ihn : ∀ (c : CU P), ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim x_1) (c.lim x) ≤ (3 / 4) ^ n
c : CU P
hxl : x ∈ c.left.U
a✝ : X
hyl : a✝ ∈ c.left.U
hyd : dist (c.left.lim a✝) (c.left.lim x) ≤ (3 / 4) ^ n
⊢ dist (c.lim a✝) (c.lim x) ≤ (3 / 4) ^ (n + 1)

Tactic:
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)]

Result:
case h
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
ihn : ∀ (c : CU P), ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim x_1) (c.lim x) ≤ (3 / 4) ^ n
c : CU P
hxl : x ∈ c.left.U
a✝ : X
hyl : a✝ ∈ c.left.U
hyd : dist (c.left.lim a✝) (c.left.lim x) ≤ (3 / 4) ^ n
⊢ dist (midpoint ℝ (c.left.lim a✝) 0) (midpoint ℝ (c.left.lim x) 0) ≤ 3 / 4 * (3 / 4) ^ n

Proof state:
case intro.intro.zero.h
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
c : CU P
y : X
⊢ dist (c.lim y) (c.lim x) ≤ (3 / 4) ^ 0

Tactic:
rw [pow_zero]

Result:
case intro.intro.zero.h
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
c : CU P
y : X
⊢ dist (c.lim y) (c.lim x) ≤ 1

Proof state:
case neg
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
ihn : ∀ (c : CU P), ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim x_1) (c.lim x) ≤ (3 / 4) ^ n
c : CU P
hxl : x ∉ c.left.U
⊢ ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim x_1) (c.lim x) ≤ (3 / 4) ^ (n + 1)

Tactic:
replace hxl : x ∈ c.left.right.Cᶜ :=
  compl_subset_compl.2 c.left.right.subset hxl

Result:
case neg
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
ihn : ∀ (c : CU P), ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim x_1) (c.lim x) ≤ (3 / 4) ^ n
c : CU P
hxl : x ∈ c.left.right.Cᶜ
⊢ ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim x_1) (c.lim x) ≤ (3 / 4) ^ (n + 1)

Proof state:
case h
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
ihn : ∀ (c : CU P), ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim x_1) (c.lim x) ≤ (3 / 4) ^ n
c : CU P
y : X
hydl : dist (c.left.right.lim y) (c.left.right.lim x) ≤ (3 / 4) ^ n
hydr : dist (c.right.lim y) (c.right.lim x) ≤ (3 / 4) ^ n
hxl : x ∉ c.left.left.U
hyl : y ∉ c.left.left.U
⊢ dist (midpoint ℝ (midpoint ℝ 1 (c.left.right.lim y)) (c.right.lim y))
      (midpoint ℝ (midpoint ℝ 1 (c.left.right.lim x)) (c.right.lim x)) ≤
    (3 / 4) ^ n * (3 / 4)

Tactic:
refine (dist_midpoint_midpoint_le _ _ _ _).trans ?_

Result:
case h
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
ihn : ∀ (c : CU P), ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim x_1) (c.lim x) ≤ (3 / 4) ^ n
c : CU P
y : X
hydl : dist (c.left.right.lim y) (c.left.right.lim x) ≤ (3 / 4) ^ n
hydr : dist (c.right.lim y) (c.right.lim x) ≤ (3 / 4) ^ n
hxl : x ∉ c.left.left.U
hyl : y ∉ c.left.left.U
⊢ (dist (midpoint ℝ 1 (c.left.right.lim y)) (midpoint ℝ 1 (c.left.right.lim x)) +
        dist (c.right.lim y) (c.right.lim x)) /
      2 ≤
    (3 / 4) ^ n * (3 / 4)

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
c : CU P
⊢ 0 < 2⁻¹ ∧ 2⁻¹ < 3 / 4 ∧ 3 / 4 < 1

Tactic:
norm_num

Result:
no goals

Proof state:
case intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
c : CU P
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
n : ℕ
x✝ : True
⊢ ∀ᶠ (x_1 : X) in 𝓝 x, c.lim x_1 ∈ Metric.closedBall (c.lim x) ((3 / 4) ^ n)

Tactic:
simp only [Metric.mem_closedBall]

Result:
case intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
c : CU P
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
n : ℕ
x✝ : True
⊢ ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim x_1) (c.lim x) ≤ (3 / 4) ^ n

Proof state:
case intro.intro.zero.h
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
c : CU P
y : X
⊢ dist (c.lim y) (c.lim x) ≤ 1

Tactic:
exact Real.dist_le_of_mem_Icc_01 (c.lim_mem_Icc _) (c.lim_mem_Icc _)

Result:
no goals