awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
x : X
n : ℕ
ihn :
  ∀ (c : CU P),
    approx (P := P) n c x ∈ Icc (approx (P := P) n (c.right (P := P)) x) (approx (P := P) n (c.left (P := P)) x)
c : CU P
succ : approx (P := P) n (c.right (P := P).left (P := P)) x ≤ approx (P := P) n (c.left (P := P)) x
⊢ midpoint ℝ (approx (P := P) n (c.right (P := P).left (P := P)) x)
        (approx (P := P) n (c.right (P := P).right (P := P)) x) ≤
      midpoint ℝ (approx (P := P) n (c.left (P := P)) x) (approx (P := P) n (c.right (P := P)) x) ∧
    midpoint ℝ (approx (P := P) n (c.left (P := P)) x) (approx (P := P) n (c.right (P := P)) x) ≤
      midpoint ℝ (approx (P := P) n (c.left (P := P).left (P := P)) x)
        (approx (P := P) n (c.left (P := P).right (P := P)) x)
have succ₁ : approx (P := P) n (c.right (P := P)) x ≤ approx (P := P) n (c.left (P := P).right (P := P)) x
Tactic: refine ⟨midpoint_le_midpoint ?_ (ihn _).1, midpoint_le_midpoint (ihn _).2 ?_⟩
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
x : X
n : ℕ
ihn :
  ∀ (c : CU P),
    approx (P := P) n c x ∈ Icc (approx (P := P) n (c.right (P := P)) x) (approx (P := P) n (c.left (P := P)) x)
c : CU P
⊢ approx (P := P) n (c.right (P := P).left (P := P)) x ≤ approx (P := P) n (c.left (P := P)) x
have succ : c.left (P := P).U (P := P) ⊆ c.right (P := P).left (P := P).C (P := P)
Tactic: apply approx_le_approx_of_U_sub_C
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
x : X
n : ℕ
ihn :
  ∀ (c : CU P),
    approx (P := P) n c x ∈ Icc (approx (P := P) n (c.right (P := P)) x) (approx (P := P) n (c.left (P := P)) x)
c : CU P
⊢ approx (P := P) n (c.right (P := P)) x ≤ approx (P := P) n (c.left (P := P).right (P := P)) x
have succ : c.left (P := P).right (P := P).U (P := P) ⊆ c.right (P := P).C (P := P)
Tactic: apply approx_le_approx_of_U_sub_C
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
c : CU P
n : ℕ
x : X
⊢ approx (P := P) n c x ∈ Icc (approx (P := P) n (c.right (P := P)) x) (approx (P := P) n (c.left (P := P)) x)
have zero : ∀ (c : CU P),
  approx (P := P) 0 c x ∈ Icc (approx (P := P) 0 (c.right (P := P)) x) (approx (P := P) 0 (c.left (P := P)) x)
Tactic: induction n generalizing c with
  | zero =>
    simp only [approx]
    refine ⟨le_rfl, ?_⟩
    grw [left_U_subset]
    rw [Pi.one_apply]; positivity -- TODO: `positivity` doesn't prove that `1 x` is nonnegative
  | succ n ihn =>
    simp only [approx, mem_Icc]
    refine ⟨midpoint_le_midpoint ?_ (ihn _).1, midpoint_le_midpoint (ihn _).2 ?_⟩ <;>
      apply approx_le_approx_of_U_sub_C
    exacts [subset_closure, subset_closure]
Cleared hypotheses: c, n
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
c : CU P
n : ℕ
x : X
zero :
  ∀ (c : CU P),
    approx (P := P) 0 c x ∈ Icc (approx (P := P) 0 (c.right (P := P)) x) (approx (P := P) 0 (c.left (P := P)) x)
⊢ approx (P := P) n c x ∈ Icc (approx (P := P) n (c.right (P := P)) x) (approx (P := P) n (c.left (P := P)) x)
have succ : ∀ (n : ℕ)
  (ihn :
    ∀ (c : CU P),
      approx (P := P) n c x ∈ Icc (approx (P := P) n (c.right (P := P)) x) (approx (P := P) n (c.left (P := P)) x))
  (c : CU P),
  approx (P := P) (n + 1) c x ∈
    Icc (approx (P := P) (n + 1) (c.right (P := P)) x) (approx (P := P) (n + 1) (c.left (P := P)) x)
Tactic: induction n generalizing c with
  | zero =>
    simp only [approx]
    refine ⟨le_rfl, ?_⟩
    grw [left_U_subset]
    rw [Pi.one_apply]; positivity -- TODO: `positivity` doesn't prove that `1 x` is nonnegative
  | succ n ihn =>
    simp only [approx, mem_Icc]
    refine ⟨midpoint_le_midpoint ?_ (ihn _).1, midpoint_le_midpoint (ihn _).2 ?_⟩ <;>
      apply approx_le_approx_of_U_sub_C
    exacts [subset_closure, subset_closure]
Cleared hypotheses: c, n
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
x : X
c : CU P
⊢ approx (P := P) 0 c x ≤ approx (P := P) (HAdd.hAdd (α := ℕ) 0 1) c x
have zero : LE.le (α := ℝ) ((c.U (P := P))ᶜ.indicator 1 x) ((c.left (P := P).U (P := P))ᶜ.indicator 1 x)
Tactic: simp only [approx, right_U, right_le_midpoint]
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
c : CU P
n : ℕ
x : X
⊢ approx (P := P) n c x ≤ approx (P := P) (n + 1) c x
have zero : ∀ (c : CU P), approx (P := P) 0 c x ≤ approx (P := P) (HAdd.hAdd (α := ℕ) 0 1) c x
Tactic: induction n generalizing c with
  | zero =>
    simp only [approx, right_U, right_le_midpoint]
    exact (approx_mem_Icc_right_left c 0 x).2
  | succ n ihn =>
    rw [approx, approx]
    exact midpoint_le_midpoint (ihn _) (ihn _)
Cleared hypotheses: c, n
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
c : CU P
n : ℕ
x : X
zero : ∀ (c : CU P), approx (P := P) 0 c x ≤ approx (P := P) (HAdd.hAdd (α := ℕ) 0 1) c x
⊢ approx (P := P) n c x ≤ approx (P := P) (n + 1) c x
have succ : ∀ (n : ℕ) (ihn : ∀ (c : CU P), approx (P := P) n c x ≤ approx (P := P) (n + 1) c x) (c : CU P),
  approx (P := P) (n + 1) c x ≤ approx (P := P) (n + 1 + 1) c x
Tactic: induction n generalizing c with
  | zero =>
    simp only [approx, right_U, right_le_midpoint]
    exact (approx_mem_Icc_right_left c 0 x).2
  | succ n ihn =>
    rw [approx, approx]
    exact midpoint_le_midpoint (ihn _) (ihn _)
Cleared hypotheses: c, n
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
c : CU P
x : X
⊢ c.lim (P := P) x = midpoint ℝ (c.left (P := P).lim (P := P) x) (c.right (P := P).lim (P := P) x)
have refine : Tendsto (fun (n : ℕ) ↦ approx (P := P) (n + 1) c x) atTop
  (𝓝 (midpoint ℝ (c.left (P := P).lim (P := P) x) (c.right (P := P).lim (P := P) x)))
Tactic: refine tendsto_nhds_unique (c.tendsto_approx_atTop x) ((tendsto_add_atTop_iff_nat 1).1 ?_)
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
c : CU P
⊢ Continuous[inst, _] (c.lim (P := P))
have h0 : LT.lt (α := ℝ) 0 2⁻¹
Tactic: obtain ⟨h0, h1234, h1⟩ : 0 < (2⁻¹ : ℝ) ∧ (2⁻¹ : ℝ) < 3 / 4 ∧ (3 / 4 : ℝ) < 1 := by norm_num
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
c : CU P
h0 : LT.lt (α := ℝ) 0 2⁻¹
⊢ Continuous[inst, _] (c.lim (P := P))
have h1234 : 2⁻¹ < 3 / 4
Tactic: obtain ⟨h0, h1234, h1⟩ : 0 < (2⁻¹ : ℝ) ∧ (2⁻¹ : ℝ) < 3 / 4 ∧ (3 / 4 : ℝ) < 1 := by norm_num
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
c : CU P
h0 : LT.lt (α := ℝ) 0 2⁻¹
h1234 : 2⁻¹ < 3 / 4
⊢ Continuous[inst, _] (c.lim (P := P))
have h1 : 3 / 4 < 1
Tactic: obtain ⟨h0, h1234, h1⟩ : 0 < (2⁻¹ : ℝ) ∧ (2⁻¹ : ℝ) < 3 / 4 ∧ (3 / 4 : ℝ) < 1 := by norm_num
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
c : CU P
h0 : LT.lt (α := ℝ) 0 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
⊢ Continuous[inst, _] (c.lim (P := P))
have fun : ∀ (x : X) (n : ℕ), True → ∀ᶠ (x_2 : X) in 𝓝 x, c.lim (P := P) x_2 ∈ Metric.closedBall (c.lim (P := P) x) ((3 / 4) ^ n)
Tactic: refine
    continuous_iff_continuousAt.2 fun x =>
      (Metric.nhds_basis_closedBall_pow (h0.trans h1234) h1).tendsto_right_iff.2 fun n _ => ?_
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
h0 : LT.lt (α := ℝ) 0 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
h : True
c : CU P
⊢ ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim (P := P) x_1) (c.lim (P := P) x) ≤ HPow.hPow (β := ℕ) (3 / 4) 0
have zero : ∀ (y : X), dist (c.lim (P := P) y) (c.lim (P := P) x) ≤ HPow.hPow (β := ℕ) (3 / 4) 0
Tactic: filter_upwards with y
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
h0 : LT.lt (α := ℝ) 0 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
h : True
n : ℕ
ihn : ∀ (c : CU P), ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim (P := P) x_1) (c.lim (P := P) x) ≤ (3 / 4) ^ n
c : CU P
⊢ ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim (P := P) x_1) (c.lim (P := P) x) ≤ (3 / 4) ^ (n + 1)
have pos : ∀ (hxl : x ∈ c.left (P := P).U (P := P)),
  ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim (P := P) x_1) (c.lim (P := P) x) ≤ (3 / 4) ^ (n + 1)
Tactic: by_cases hxl : x ∈ c.left.U
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
h0 : LT.lt (α := ℝ) 0 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
h : True
n : ℕ
ihn : ∀ (c : CU P), ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim (P := P) x_1) (c.lim (P := P) x) ≤ (3 / 4) ^ n
c : CU P
pos :
  ∀ (hxl : x ∈ c.left (P := P).U (P := P)),
    ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim (P := P) x_1) (c.lim (P := P) x) ≤ (3 / 4) ^ (n + 1)
⊢ ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim (P := P) x_1) (c.lim (P := P) x) ≤ (3 / 4) ^ (n + 1)
have neg : ∀ (hxl : x ∉ c.left (P := P).U (P := P)),
  ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim (P := P) x_1) (c.lim (P := P) x) ≤ (3 / 4) ^ (n + 1)
Tactic: by_cases hxl : x ∈ c.left.U
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
h0 : LT.lt (α := ℝ) 0 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
h : True
n : ℕ
ihn : ∀ (c : CU P), ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim (P := P) x_1) (c.lim (P := P) x) ≤ (3 / 4) ^ n
c : CU P
hxl : x ∈ c.left (P := P).U (P := P)
⊢ ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim (P := P) x_1) (c.lim (P := P) x) ≤ (3 / 4) ^ (n + 1)
have h : ∀ (a : X) (hyl : a ∈ c.left (P := P).U (P := P))
  (hyd : dist (c.left (P := P).lim (P := P) a) (c.left (P := P).lim (P := P) x) ≤ (3 / 4) ^ n),
  dist (c.lim (P := P) a) (c.lim (P := P) x) ≤ (3 / 4) ^ (n + 1)
Tactic: filter_upwards [IsOpen.mem_nhds c.left.open_U hxl, ihn c.left] with _ hyl hyd
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
h0 : LT.lt (α := ℝ) 0 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
h : True
n : ℕ
ihn : ∀ (c : CU P), ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim (P := P) x_1) (c.lim (P := P) x) ≤ (3 / 4) ^ n
c : CU P
hxl : x ∈ c.left (P := P).U (P := P)
a : X
hyl : a ∈ c.left (P := P).U (P := P)
hyd : dist (c.left (P := P).lim (P := P) a) (c.left (P := P).lim (P := P) x) ≤ (3 / 4) ^ n
⊢ dist (c.lim (P := P) a) (c.lim (P := P) x) ≤ (3 / 4) ^ (n + 1)
have h : dist (midpoint ℝ (c.left (P := P).lim (P := P) a) 0) (midpoint ℝ (c.left (P := P).lim (P := P) x) 0) ≤
  3 / 4 * (3 / 4) ^ n
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)]
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
h0 : LT.lt (α := ℝ) 0 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
h : True
n : ℕ
ihn : ∀ (c : CU P), ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim (P := P) x_1) (c.lim (P := P) x) ≤ (3 / 4) ^ n
c : CU P
hxl : x ∈ c.left (P := P).U (P := P)
a : X
hyl : a ∈ c.left (P := P).U (P := P)
hyd : dist (c.left (P := P).lim (P := P) a) (c.left (P := P).lim (P := P) x) ≤ (3 / 4) ^ n
⊢ dist (midpoint ℝ (c.left (P := P).lim (P := P) a) 0) (midpoint ℝ (c.left (P := P).lim (P := P) x) 0) ≤
    3 / 4 * (3 / 4) ^ n
have h : (dist (c.left (P := P).lim (P := P) a) (c.left (P := P).lim (P := P) x) + dist (α := ℝ) 0 0) / 2 ≤ 3 / 4 * (3 / 4) ^ n
Tactic: refine (dist_midpoint_midpoint_le _ _ _ _).trans ?_
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
h0 : LT.lt (α := ℝ) 0 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
h : True
n : ℕ
ihn : ∀ (c : CU P), ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim (P := P) x_1) (c.lim (P := P) x) ≤ (3 / 4) ^ n
c : CU P
hxl : x ∈ c.left (P := P).U (P := P)
a : X
hyl : a ∈ c.left (P := P).U (P := P)
hyd : dist (c.left (P := P).lim (P := P) a) (c.left (P := P).lim (P := P) x) ≤ (3 / 4) ^ n
⊢ (dist (c.left (P := P).lim (P := P) a) (c.left (P := P).lim (P := P) x) + dist (α := ℝ) 0 0) / 2 ≤ 3 / 4 * (3 / 4) ^ n
have h : 2⁻¹ * dist (c.left (P := P).lim (P := P) a) (c.left (P := P).lim (P := P) x) ≤ 3 / 4 * (3 / 4) ^ n
Tactic: rw [dist_self, add_zero, div_eq_inv_mul]
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
h0 : LT.lt (α := ℝ) 0 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
h : True
n : ℕ
ihn : ∀ (c : CU P), ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim (P := P) x_1) (c.lim (P := P) x) ≤ (3 / 4) ^ n
c : CU P
hxl : x ∈ c.left (P := P).U (P := P)
a : X
hyl : a ∈ c.left (P := P).U (P := P)
hyd : dist (c.left (P := P).lim (P := P) a) (c.left (P := P).lim (P := P) x) ≤ (3 / 4) ^ n
⊢ 2⁻¹ * dist (c.left (P := P).lim (P := P) a) (c.left (P := P).lim (P := P) x) ≤ 3 / 4 * (3 / 4) ^ n
have h : 0 ≤ dist (c.left (P := P).lim (P := P) a) (c.left (P := P).lim (P := P) x)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
h0 : LT.lt (α := ℝ) 0 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
h_1 : True
n : ℕ
ihn : ∀ (c : CU P), ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim (P := P) x_1) (c.lim (P := P) x) ≤ (3 / 4) ^ n
c : CU P
hxl : x ∈ c.left (P := P).U (P := P)
a : X
hyl : a ∈ c.left (P := P).U (P := P)
hyd : dist (c.left (P := P).lim (P := P) a) (c.left (P := P).lim (P := P) x) ≤ (3 / 4) ^ n
h : 0 ≤ dist (c.left (P := P).lim (P := P) a) (c.left (P := P).lim (P := P) x)
⊢ 2⁻¹ * dist (c.left (P := P).lim (P := P) a) (c.left (P := P).lim (P := P) x) ≤ 3 / 4 * (3 / 4) ^ n
have h₁ : 0 ≤ 3 / 4
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
h0 : LT.lt (α := ℝ) 0 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
h : True
n : ℕ
ihn : ∀ (c : CU P), ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim (P := P) x_1) (c.lim (P := P) x) ≤ (3 / 4) ^ n
c : CU P
hxl : x ∉ c.left (P := P).U (P := P)
⊢ ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim (P := P) x_1) (c.lim (P := P) x) ≤ (3 / 4) ^ (n + 1)
have hxl₁ : x ∈ (c.left (P := P).right (P := P).C (P := P))ᶜ
Tactic: replace hxl : x ∈ c.left.right.Cᶜ :=
        compl_subset_compl.2 c.left.right.subset hxl
Cleared hypotheses: hxl
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
h0 : LT.lt (α := ℝ) 0 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
h : True
n : ℕ
ihn : ∀ (c : CU P), ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim (P := P) x_1) (c.lim (P := P) x) ≤ (3 / 4) ^ n
c : CU P
hxl : x ∈ (c.left (P := P).right (P := P).C (P := P))ᶜ
⊢ ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim (P := P) x_1) (c.lim (P := P) x) ≤ (3 / 4) ^ (n + 1)
have h : ∀ (y : X) (hyl : y ∈ (c.left (P := P).right (P := P).C (P := P))ᶜ)
  (hydl :
    dist (c.left (P := P).right (P := P).lim (P := P) y) (c.left (P := P).right (P := P).lim (P := P) x) ≤ (3 / 4) ^ n)
  (hydr : dist (c.right (P := P).lim (P := P) y) (c.right (P := P).lim (P := P) x) ≤ (3 / 4) ^ n),
  dist (c.lim (P := P) y) (c.lim (P := P) x) ≤ (3 / 4) ^ (n + 1)
Tactic: 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
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
h0 : LT.lt (α := ℝ) 0 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
h : True
n : ℕ
ihn : ∀ (c : CU P), ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim (P := P) x_1) (c.lim (P := P) x) ≤ (3 / 4) ^ n
c : CU P
hxl : x ∈ (c.left (P := P).right (P := P).C (P := P))ᶜ
y : X
hyl : y ∈ (c.left (P := P).right (P := P).C (P := P))ᶜ
hydl :
  dist (c.left (P := P).right (P := P).lim (P := P) y) (c.left (P := P).right (P := P).lim (P := P) x) ≤ (3 / 4) ^ n
hydr : dist (c.right (P := P).lim (P := P) y) (c.right (P := P).lim (P := P) x) ≤ (3 / 4) ^ n
⊢ dist (c.lim (P := P) y) (c.lim (P := P) x) ≤ (3 / 4) ^ (n + 1)
have hxl₁ : x ∉ c.left (P := P).left (P := P).U (P := P)
Tactic: replace hxl : x ∉ c.left.left.U :=
        compl_subset_compl.2 c.left.left_U_subset_right_C hxl
Cleared hypotheses: hxl
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
h0 : LT.lt (α := ℝ) 0 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
h : True
n : ℕ
ihn : ∀ (c : CU P), ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim (P := P) x_1) (c.lim (P := P) x) ≤ (3 / 4) ^ n
c : CU P
y : X
hyl : y ∈ (c.left (P := P).right (P := P).C (P := P))ᶜ
hydl :
  dist (c.left (P := P).right (P := P).lim (P := P) y) (c.left (P := P).right (P := P).lim (P := P) x) ≤ (3 / 4) ^ n
hydr : dist (c.right (P := P).lim (P := P) y) (c.right (P := P).lim (P := P) x) ≤ (3 / 4) ^ n
hxl : x ∉ c.left (P := P).left (P := P).U (P := P)
⊢ dist (c.lim (P := P) y) (c.lim (P := P) x) ≤ (3 / 4) ^ (n + 1)
have hyl₁ : y ∉ c.left (P := P).left (P := P).U (P := P)
Tactic: replace hyl : y ∉ c.left.left.U :=
        compl_subset_compl.2 c.left.left_U_subset_right_C hyl
Cleared hypotheses: hyl
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
h0 : LT.lt (α := ℝ) 0 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
h : True
n : ℕ
ihn : ∀ (c : CU P), ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim (P := P) x_1) (c.lim (P := P) x) ≤ (3 / 4) ^ n
c : CU P
y : X
hydl :
  dist (c.left (P := P).right (P := P).lim (P := P) y) (c.left (P := P).right (P := P).lim (P := P) x) ≤ (3 / 4) ^ n
hydr : dist (c.right (P := P).lim (P := P) y) (c.right (P := P).lim (P := P) x) ≤ (3 / 4) ^ n
hxl : x ∉ c.left (P := P).left (P := P).U (P := P)
hyl : y ∉ c.left (P := P).left (P := P).U (P := P)
⊢ dist (c.lim (P := P) y) (c.lim (P := P) x) ≤ (3 / 4) ^ (n + 1)
have h : dist (midpoint ℝ (midpoint ℝ 1 (c.left (P := P).right (P := P).lim (P := P) y)) (c.right (P := P).lim (P := P) y))
    (midpoint ℝ (midpoint ℝ 1 (c.left (P := P).right (P := P).lim (P := P) x)) (c.right (P := P).lim (P := P) x)) ≤
  (3 / 4) ^ n * (3 / 4)
Tactic: simp only [pow_succ, c.lim_eq_midpoint, c.left.lim_eq_midpoint,
        c.left.left.lim_of_notMem_U _ hxl, c.left.left.lim_of_notMem_U _ hyl]
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
h0 : LT.lt (α := ℝ) 0 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
h : True
n : ℕ
ihn : ∀ (c : CU P), ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim (P := P) x_1) (c.lim (P := P) x) ≤ (3 / 4) ^ n
c : CU P
y : X
hydl :
  dist (c.left (P := P).right (P := P).lim (P := P) y) (c.left (P := P).right (P := P).lim (P := P) x) ≤ (3 / 4) ^ n
hydr : dist (c.right (P := P).lim (P := P) y) (c.right (P := P).lim (P := P) x) ≤ (3 / 4) ^ n
hxl : x ∉ c.left (P := P).left (P := P).U (P := P)
hyl : y ∉ c.left (P := P).left (P := P).U (P := P)
⊢ dist (midpoint ℝ (midpoint ℝ 1 (c.left (P := P).right (P := P).lim (P := P) y)) (c.right (P := P).lim (P := P) y))
      (midpoint ℝ (midpoint ℝ 1 (c.left (P := P).right (P := P).lim (P := P) x)) (c.right (P := P).lim (P := P) x)) ≤
    (3 / 4) ^ n * (3 / 4)
have h : (dist (c.left (P := P).right (P := P).lim (P := P) y) (c.left (P := P).right (P := P).lim (P := P) x) / 2 +
      dist (c.right (P := P).lim (P := P) y) (c.right (P := P).lim (P := P) x)) /
    2 ≤
  (3 / 4) ^ n * (3 / 4)
Tactic: grw [dist_midpoint_midpoint_le, dist_midpoint_midpoint_le, dist_self, zero_add]
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
h0 : LT.lt (α := ℝ) 0 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
h : True
n : ℕ
ihn : ∀ (c : CU P), ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim (P := P) x_1) (c.lim (P := P) x) ≤ (3 / 4) ^ n
c : CU P
y : X
hydl :
  dist (c.left (P := P).right (P := P).lim (P := P) y) (c.left (P := P).right (P := P).lim (P := P) x) ≤ (3 / 4) ^ n
hydr : dist (c.right (P := P).lim (P := P) y) (c.right (P := P).lim (P := P) x) ≤ (3 / 4) ^ n
hxl : x ∉ c.left (P := P).left (P := P).U (P := P)
hyl : y ∉ c.left (P := P).left (P := P).U (P := P)
⊢ (dist (c.left (P := P).right (P := P).lim (P := P) y) (c.left (P := P).right (P := P).lim (P := P) x) / 2 +
        dist (c.right (P := P).lim (P := P) y) (c.right (P := P).lim (P := P) x)) /
      2 ≤
    (3 / 4) ^ n * (3 / 4)
have h : let r := (3 / 4) ^ n;
∀ (ihn : ∀ (c : CU P), ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim (P := P) x_1) (c.lim (P := P) x) ≤ r)
  (hydl : dist (c.left (P := P).right (P := P).lim (P := P) y) (c.left (P := P).right (P := P).lim (P := P) x) ≤ r)
  (hydr : dist (c.right (P := P).lim (P := P) y) (c.right (P := P).lim (P := P) x) ≤ r),
  (dist (c.left (P := P).right (P := P).lim (P := P) y) (c.left (P := P).right (P := P).lim (P := P) x) / 2 +
        dist (c.right (P := P).lim (P := P) y) (c.right (P := P).lim (P := P) x)) /
      2 ≤
    r * (3 / 4)
Tactic: set r := (3 / 4 : ℝ) ^ n
Cleared hypotheses: ihn, hydl, hydr
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
h0 : LT.lt (α := ℝ) 0 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
h : True
n : ℕ
c : CU P
y : X
hxl : x ∉ c.left (P := P).left (P := P).U (P := P)
hyl : y ∉ c.left (P := P).left (P := P).U (P := P)
r : ℝ := (3 / 4) ^ n
ihn : ∀ (c : CU P), ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim (P := P) x_1) (c.lim (P := P) x) ≤ r
hydl : dist (c.left (P := P).right (P := P).lim (P := P) y) (c.left (P := P).right (P := P).lim (P := P) x) ≤ r
hydr : dist (c.right (P := P).lim (P := P) y) (c.right (P := P).lim (P := P) x) ≤ r
⊢ (dist (c.left (P := P).right (P := P).lim (P := P) y) (c.left (P := P).right (P := P).lim (P := P) x) / 2 +
        dist (c.right (P := P).lim (P := P) y) (c.right (P := P).lim (P := P) x)) /
      2 ≤
    (r / 2 + r) / 2
have hc : LE.le (α := ℝ) 0 2
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
h0 : LT.lt (α := ℝ) 0 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
h : True
n : ℕ
c : CU P
y : X
hxl : x ∉ c.left (P := P).left (P := P).U (P := P)
hyl : y ∉ c.left (P := P).left (P := P).U (P := P)
r : ℝ := (3 / 4) ^ n
ihn : ∀ (c : CU P), ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim (P := P) x_1) (c.lim (P := P) x) ≤ r
hydl : dist (c.left (P := P).right (P := P).lim (P := P) y) (c.left (P := P).right (P := P).lim (P := P) x) ≤ r
hydr : dist (c.right (P := P).lim (P := P) y) (c.right (P := P).lim (P := P) x) ≤ r
⊢ (dist (c.left (P := P).right (P := P).lim (P := P) y) (c.left (P := P).right (P := P).lim (P := P) x) / 2 +
        dist (c.right (P := P).lim (P := P) y) (c.right (P := P).lim (P := P) x)) /
      2 ≤
    r * (3 / 4)
have calc : (dist (c.left (P := P).right (P := P).lim (P := P) y) (c.left (P := P).right (P := P).lim (P := P) x) / 2 +
      dist (c.right (P := P).lim (P := P) y) (c.right (P := P).lim (P := P) x)) /
    2 ≤
  (r / 2 + r) / 2
Tactic: calc _ ≤ (r / 2 + r) / 2 := by gcongr
        _ = _ := by ring