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

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 (midpoint ℝ (c.left.lim a✝) 0) (midpoint ℝ (c.left.lim x) 0) ≤ 3 / 4 * (3 / 4) ^ n

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
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.left.lim a✝) (c.left.lim x) + dist 0 0) / 2 ≤ 3 / 4 * (3 / 4) ^ n

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
⊢ Continuous c.lim

Tactic:
refine
  continuous_iff_continuousAt.2 fun x =>
    (Metric.nhds_basis_closedBall_pow (h0.trans h1234) h1).tendsto_right_iff.2 fun n _ => ?_

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, c.lim x_1 ∈ Metric.closedBall (c.lim x) ((3 / 4) ^ n)

Proof state:
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 : ℕ
c : CU P
y : X
hxl : x ∉ c.left.left.U
hyl : y ∉ c.left.left.U
r : ℝ := (3 / 4) ^ n
ihn : ∀ (c : CU P), ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim x_1) (c.lim x) ≤ r
hydl : dist (c.left.right.lim y) (c.left.right.lim x) ≤ r
hydr : dist (c.right.lim y) (c.right.lim x) ≤ r
⊢ (dist (c.left.right.lim y) (c.left.right.lim x) / 2 + dist (c.right.lim y) (c.right.lim x)) / 2 ≤ (r / 2 + r) / 2

Tactic:
gcongr

Result:
no goals

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 : ℕ
c : CU P
y : X
hxl : x ∉ c.left.left.U
hyl : y ∉ c.left.left.U
r : ℝ := (3 / 4) ^ n
ihn : ∀ (c : CU P), ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim x_1) (c.lim x) ≤ r
hydl : dist (c.left.right.lim y) (c.left.right.lim x) ≤ r
hydr : dist (c.right.lim y) (c.right.lim x) ≤ r
⊢ (dist (c.left.right.lim y) (c.left.right.lim x) / 2 + dist (c.right.lim y) (c.right.lim x)) / 2 ≤ r * (3 / 4)

Tactic:
calc _ ≤ (r / 2 + r) / 2 := by gcongr
  _ = _ := by field_simp; ring

Result:
no goals

Proof state:
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 : ℕ
c : CU P
y : X
hxl : x ∉ c.left.left.U
hyl : y ∉ c.left.left.U
r : ℝ := (3 / 4) ^ n
ihn : ∀ (c : CU P), ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim x_1) (c.lim x) ≤ r
hydl : dist (c.left.right.lim y) (c.left.right.lim x) ≤ r
hydr : dist (c.right.lim y) (c.right.lim x) ≤ r
⊢ (r / 2 + r) / 2 = r * (3 / 4)

Tactic:
field_simp

Result:
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 : ℕ
c : CU P
y : X
hxl : x ∉ c.left.left.U
hyl : y ∉ c.left.left.U
r : ℝ := (3 / 4) ^ n
ihn : ∀ (c : CU P), ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim x_1) (c.lim x) ≤ r
hydl : dist (c.left.right.lim y) (c.left.right.lim x) ≤ r
hydr : dist (c.right.lim y) (c.right.lim x) ≤ r
⊢ (r + r * 2) * 4 = r * 3 * (2 * 2)

Proof state:
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 : ℕ
c : CU P
y : X
hxl : x ∉ c.left.left.U
hyl : y ∉ c.left.left.U
r : ℝ := (3 / 4) ^ n
ihn : ∀ (c : CU P), ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim x_1) (c.lim x) ≤ r
hydl : dist (c.left.right.lim y) (c.left.right.lim x) ≤ r
hydr : dist (c.right.lim y) (c.right.lim x) ≤ r
⊢ (r + r * 2) * 4 = r * 3 * (2 * 2)

Tactic:
ring

Result:
no goals

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.left.lim a✝) (c.left.lim x) + dist 0 0) / 2 ≤ 3 / 4 * (3 / 4) ^ n

Tactic:
rw [dist_self, add_zero, div_eq_inv_mul]

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
⊢ 2⁻¹ * dist (c.left.lim a✝) (c.left.lim x) ≤ 3 / 4 * (3 / 4) ^ n