awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.UrysohnsLemma
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
succ₁ : approx (P := P) n (c.right (P := P)) x ≤ approx (P := P) n (c.left (P := P).right (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)

Tactic:
refine ⟨midpoint_le_midpoint ?_ (ihn _).1, midpoint_le_midpoint (ihn _).2 ?_⟩
-- Module: Mathlib.Topology.UrysohnsLemma
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 : c.left (P := P).U (P := P) ⊆ c.right (P := P).left (P := P).C (P := P)
⊢ approx (P := P) n (c.right (P := P).left (P := P)) x ≤ approx (P := P) n (c.left (P := P)) x

Tactic:
apply approx_le_approx_of_U_sub_C

Premises used: Urysohns.CU.approx_le_approx_of_U_sub_C
-- Module: Mathlib.Topology.UrysohnsLemma
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 : c.left (P := P).right (P := P).U (P := P) ⊆ c.right (P := P).C (P := P)
⊢ approx (P := P) n (c.right (P := P)) x ≤ approx (P := P) n (c.left (P := P).right (P := P)) x

Tactic:
apply approx_le_approx_of_U_sub_C

Premises used: Urysohns.CU.approx_le_approx_of_U_sub_C
-- Module: Mathlib.Topology.UrysohnsLemma
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
⊢ c.left (P := P).U (P := P) ⊆ c.right (P := P).left (P := P).C (P := P)

Tactic:
subset_closure

Premises used: Set.Mem, subset_closure, setOf, closure, Classical.choose, Set.sInter
-- Module: Mathlib.Topology.UrysohnsLemma
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
⊢ c.left (P := P).right (P := P).U (P := P) ⊆ c.right (P := P).C (P := P)

Tactic:
subset_closure

Premises used: Set.Mem, subset_closure, setOf, closure, Classical.choose, Set.sInter
-- Module: Mathlib.Topology.UrysohnsLemma
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
⊢ c.left (P := P).U (P := P) ⊆ c.right (P := P).left (P := P).C (P := P)

Tactic:
exacts [subset_closure, subset_closure]

Premises used: subset_closure
-- Module: Mathlib.Topology.UrysohnsLemma
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)
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)
⊢ 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)

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]

Premises used: subset_closure, Pi.one_apply, Urysohns.CU.approx, Set.mem_Icc, Urysohns.CU.approx_le_approx_of_U_sub_C, Urysohns.CU.left_U_subset
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
x : X
c : CU P
zero : LE.le (α := ℝ) ((c.U (P := P))ᶜ.indicator 1 x) ((c.left (P := P).U (P := P))ᶜ.indicator 1 x)
⊢ approx (P := P) 0 c x ≤ approx (P := P) (HAdd.hAdd (α := ℕ) 0 1) c x

Tactic:
simp only [approx, right_U, right_le_midpoint]

Premises used: Urysohns.CU.right_U, Urysohns.CU.approx, right_le_midpoint
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
x : X
c : CU P
⊢ LE.le (α := ℝ) ((c.U (P := P))ᶜ.indicator 1 x) ((c.left (P := P).U (P := P))ᶜ.indicator 1 x)

Tactic:
(approx_mem_Icc_right_left c 0 x).2

Premises used: Urysohns.CU.approx_mem_Icc_right_left, Urysohns.CU.approx, And.right, OfNat.ofNat
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
x : X
c : CU P
⊢ LE.le (α := ℝ) ((c.U (P := P))ᶜ.indicator 1 x) ((c.left (P := P).U (P := P))ᶜ.indicator 1 x)

Tactic:
exact (approx_mem_Icc_right_left c 0 x).2

Premises used: Urysohns.CU.approx_mem_Icc_right_left, And.right, OfNat.ofNat
-- Module: Mathlib.Topology.UrysohnsLemma
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 ≤ approx (P := P) (n + 1) c x
c : CU P
⊢ midpoint ℝ (approx (P := P) n (c.left (P := P)) x) (approx (P := P) n (c.right (P := P)) x) ≤
    midpoint ℝ (approx (P := P) (n + 1) (c.left (P := P)) x) (approx (P := P) (n + 1) (c.right (P := P)) x)

Tactic:
midpoint_le_midpoint (ihn _) (ihn _)

Premises used: midpoint_le_midpoint
-- Module: Mathlib.Topology.UrysohnsLemma
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 ≤ approx (P := P) (n + 1) c x
c : CU P
⊢ midpoint ℝ (approx (P := P) n (c.left (P := P)) x) (approx (P := P) n (c.right (P := P)) x) ≤
    midpoint ℝ (approx (P := P) (n + 1) (c.left (P := P)) x) (approx (P := P) (n + 1) (c.right (P := P)) x)

Tactic:
exact midpoint_le_midpoint (ihn _) (ihn _)

Premises used: midpoint_le_midpoint
-- Module: Mathlib.Topology.UrysohnsLemma
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
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
⊢ approx (P := P) n c x ≤ approx (P := P) (n + 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 _)

Premises used: Urysohns.CU.approx_mem_Icc_right_left, Urysohns.CU.right_U, Urysohns.CU.approx, And.right, right_le_midpoint, OfNat.ofNat
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
c : CU P
x : X
⊢ Monotone (β := ℝ) fun (n : ℕ) ↦ approx (P := P) n c x

Tactic:
monotone_nat_of_le_succ fun n => c.approx_le_succ n x

Premises used: Urysohns.CU.approx_le_succ, monotone_nat_of_le_succ
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
c : CU P
x : X
⊢ Tendsto (fun (n : ℕ) ↦ approx (P := P) n c x) atTop (𝓝 (c.lim (P := P) x))

Tactic:
tendsto_atTop_ciSup (c.approx_mono x) ⟨1, fun _ ⟨_, hn⟩ => hn ▸ c.approx_le_one _ _⟩

Premises used: _private.0.Urysohns.CU.bddAbove_range_approx.match_1, tendsto_atTop_ciSup, Urysohns.CU.approx_mono, Eq.rec, Urysohns.CU.lim, LE.le, Urysohns.CU.approx_le_one, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
c : CU P
x : X
h : x ∈ c.C (P := P)
⊢ c.lim (P := P) x = 0

Tactic:
simp only [CU.lim, approx_of_mem_C, h, ciSup_const]

Premises used: Urysohns.CU.approx_of_mem_C, Urysohns.CU.lim, ciSup_const
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
c : CU P
⊢ Disjoint (c.C (P := P)) (Function.support (c.lim (P := P)))

Tactic:
Function.disjoint_support_iff.mpr (fun x hx => lim_of_mem_C c x hx)

Premises used: Iff.mpr, Urysohns.CU.lim_of_mem_C, Function.disjoint_support_iff
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
c : CU P
x : X
h : x ∉ c.U (P := P)
⊢ c.lim (P := P) x = 1

Tactic:
simp only [CU.lim, approx_of_notMem_U c _ h, ciSup_const]

Premises used: Urysohns.CU.lim, ciSup_const, Urysohns.CU.approx_of_notMem_U
-- Module: Mathlib.Topology.UrysohnsLemma
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)

Tactic:
tendsto_nhds_unique (c.tendsto_approx_atTop x) ((tendsto_add_atTop_iff_nat 1).1 ?_)

Premises used: Iff.mp, Filter.tendsto_add_atTop_iff_nat, OfNat.ofNat, tendsto_nhds_unique, Urysohns.CU.tendsto_approx_atTop
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
c : CU P
x : X
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)))
⊢ c.lim (P := P) x = 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 ?_)

Premises used: Iff.mp, Filter.tendsto_add_atTop_iff_nat, OfNat.ofNat, tendsto_nhds_unique, Urysohns.CU.tendsto_approx_atTop
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
c : CU P
x : X
⊢ Tendsto (fun (n : ℕ) ↦ midpoint ℝ (approx (P := P) n (c.left (P := P)) x) (approx (P := P) n (c.right (P := P)) x))
    atTop (𝓝 (midpoint ℝ (c.left (P := P).lim (P := P) x) (c.right (P := P).lim (P := P) x)))

Tactic:
(c.left.tendsto_approx_atTop x).midpoint (c.right.tendsto_approx_atTop x)

Premises used: Filter.Tendsto.midpoint, Urysohns.CU.left, Urysohns.CU.right, Urysohns.CU.tendsto_approx_atTop
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
c : CU P
x : X
⊢ Tendsto (fun (n : ℕ) ↦ midpoint ℝ (approx (P := P) n (c.left (P := P)) x) (approx (P := P) n (c.right (P := P)) x))
    atTop (𝓝 (midpoint ℝ (c.left (P := P).lim (P := P) x) (c.right (P := P).lim (P := P) x)))

Tactic:
exact (c.left.tendsto_approx_atTop x).midpoint (c.right.tendsto_approx_atTop x)

Premises used: Filter.Tendsto.midpoint, Urysohns.CU.left, Urysohns.CU.right, Urysohns.CU.tendsto_approx_atTop
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
c : CU P
x : X
n : ℕ
⊢ approx (P := P) n c x ≤ c.lim (P := P) x

Tactic:
le_ciSup (c.bddAbove_range_approx x) _

Premises used: Urysohns.CU.bddAbove_range_approx, Urysohns.CU.lim, le_ciSup
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
c : CU P
x : X
⊢ 0 ≤ c.lim (P := P) x

Tactic:
(c.approx_nonneg 0 x).trans (c.approx_le_lim x 0)

Premises used: Urysohns.CU.approx_nonneg, LE.le.trans, OfNat.ofNat, Urysohns.CU.approx_le_lim
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
c : CU P
x : X
⊢ c.lim (P := P) x ≤ 1

Tactic:
ciSup_le fun _ => c.approx_le_one _ _

Premises used: Urysohns.CU.lim, Urysohns.CU.approx_le_one, ciSup_le
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
c : CU P
x : X
⊢ Membership.mem (γ := Set ℝ) (Icc 0 1) (c.lim (P := P) x)

Tactic:
⟨c.lim_nonneg x, c.lim_le_one x⟩

Premises used: Set.Mem, setOf, Urysohns.CU.lim_le_one, Set.Icc, And.intro, Urysohns.CU.lim_nonneg
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
c : CU P
⊢ LT.lt (α := ℝ) 0 2⁻¹ ∧ 2⁻¹ < 3 / 4 ∧ 3 / 4 < 1

Tactic:
norm_num
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
c : CU P
⊢ LT.lt (α := ℝ) 0 2⁻¹

Tactic:
obtain ⟨h0, h1234, h1⟩ : 0 < (2⁻¹ : ℝ) ∧ (2⁻¹ : ℝ) < 3 / 4 ∧ (3 / 4 : ℝ) < 1 := by norm_num

Premises used: HDiv.hDiv, Inv.inv, OfNat.ofNat
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
c : CU P
h0 : LT.lt (α := ℝ) 0 2⁻¹
⊢ 2⁻¹ < 3 / 4

Tactic:
obtain ⟨h0, h1234, h1⟩ : 0 < (2⁻¹ : ℝ) ∧ (2⁻¹ : ℝ) < 3 / 4 ∧ (3 / 4 : ℝ) < 1 := by norm_num

Premises used: HDiv.hDiv, Inv.inv, OfNat.ofNat
-- Module: Mathlib.Topology.UrysohnsLemma
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
⊢ 3 / 4 < 1

Tactic:
obtain ⟨h0, h1234, h1⟩ : 0 < (2⁻¹ : ℝ) ∧ (2⁻¹ : ℝ) < 3 / 4 ∧ (3 / 4 : ℝ) < 1 := by norm_num

Premises used: HDiv.hDiv, Inv.inv, OfNat.ofNat
-- Module: Mathlib.Topology.UrysohnsLemma
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))

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

Premises used: Iff.mpr, Metric.nhds_basis_closedBall_pow, LT.lt.trans, Filter.HasBasis.tendsto_right_iff, continuous_iff_continuousAt
-- Module: Mathlib.Topology.UrysohnsLemma
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
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)
⊢ Continuous[inst, _] (c.lim (P := P))

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

Premises used: Iff.mpr, Metric.nhds_basis_closedBall_pow, LT.lt.trans, Filter.HasBasis.tendsto_right_iff, continuous_iff_continuousAt
-- Module: Mathlib.Topology.UrysohnsLemma
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
zero : ∀ (y : X), dist (c.lim (P := P) y) (c.lim (P := P) x) ≤ HPow.hPow (β := ℕ) (3 / 4) 0
⊢ ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim (P := P) x_1) (c.lim (P := P) x) ≤ HPow.hPow (β := ℕ) (3 / 4) 0

Tactic:
filter_upwards with y
-- Module: Mathlib.Topology.UrysohnsLemma
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
y : X
⊢ dist (c.lim (P := P) y) (c.lim (P := P) x) ≤ 1

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

Premises used: Real.dist_le_of_mem_Icc_01, Urysohns.CU.lim_mem_Icc
-- Module: Mathlib.Topology.UrysohnsLemma
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
y : X
⊢ dist (c.lim (P := P) y) (c.lim (P := P) x) ≤ 1

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

Premises used: Real.dist_le_of_mem_Icc_01, Urysohns.CU.lim_mem_Icc
-- Module: Mathlib.Topology.UrysohnsLemma
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)
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)
⊢ ∀ᶠ (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

Premises used: Urysohns.CU.left, Urysohns.CU.U
-- Module: Mathlib.Topology.UrysohnsLemma
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)
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)
⊢ ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim (P := P) x_1) (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

Premises used: Urysohns.CU.left, IsOpen.mem_nhds, Urysohns.CU.open_U
-- Module: Mathlib.Topology.UrysohnsLemma
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 :
  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
⊢ dist (c.lim (P := P) a) (c.lim (P := P) 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)]

Premises used: Urysohns.CU.left_U_subset_right_C, Urysohns.CU.lim_of_mem_C, Urysohns.CU.right, pow_succ', Urysohns.CU.lim_eq_midpoint
-- Module: Mathlib.Topology.UrysohnsLemma
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

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

Premises used: dist_midpoint_midpoint_le, LE.le.trans
-- Module: Mathlib.Topology.UrysohnsLemma
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 :
  (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
⊢ 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:
refine (dist_midpoint_midpoint_le _ _ _ _).trans ?_

Premises used: dist_midpoint_midpoint_le, LE.le.trans
-- Module: Mathlib.Topology.UrysohnsLemma
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 : 2⁻¹ * dist (c.left (P := P).lim (P := P) a) (c.left (P := P).lim (P := P) x) ≤ 3 / 4 * (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

Tactic:
rw [dist_self, add_zero, div_eq_inv_mul]

Premises used: dist_self, div_eq_inv_mul, add_zero
-- Module: Mathlib.Topology.UrysohnsLemma
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)
h₁ : 0 ≤ 3 / 4
⊢ 2⁻¹ * dist (c.left (P := P).lim (P := P) a) (c.left (P := P).lim (P := P) x) ≤ 3 / 4 * (3 / 4) ^ n

Tactic:
gcongr
-- Module: Mathlib.Topology.UrysohnsLemma
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 ∈ (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
-- Module: Mathlib.Topology.UrysohnsLemma
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).right (P := P).C (P := P))ᶜ
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)
⊢ ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim (P := P) x_1) (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

Premises used: Iff.mpr, Urysohns.CU.closed_C, Urysohns.CU.left, IsOpen.mem_nhds, Urysohns.CU.right, isOpen_compl_iff
-- Module: Mathlib.Topology.UrysohnsLemma
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
⊢ 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