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
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)
⊢ 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
-- 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
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)
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)
⊢ dist (c.lim (P := P) y) (c.lim (P := P) x) ≤ (3 / 4) ^ (n + 1)

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]

Premises used: pow_succ, Urysohns.CU.left, Urysohns.CU.lim_of_notMem_U, 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_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
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)
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)
⊢ 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:
grw [dist_midpoint_midpoint_le, dist_midpoint_midpoint_le, dist_self, zero_add]

Premises used: dist_midpoint_midpoint_le, zero_add, dist_self
-- 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
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)
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)
⊢ (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:
set r := (3 / 4 : ℝ) ^ n

Premises used: HDiv.hDiv, OfNat.ofNat
-- 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 : ℕ
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
hc hab : LE.le (α := ℝ) 0 2
⊢ (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:
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 : ℕ
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
⊢ (r / 2 + r) / 2 = r * (3 / 4)

Tactic:
ring
-- 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 : ℕ
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
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
calc₁ : (r / 2 + r) / 2 = r * (3 / 4)
⊢ (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:
calc _ ≤ (r / 2 + r) / 2 := by gcongr
        _ = _ := by ring

Premises used: HDiv.hDiv, HAdd.hAdd, 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
x : X
n : ℕ
h : True
zero : ∀ (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
succ :
  ∀ (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)
⊢ ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim (P := P) x_1) (c.lim (P := P) x) ≤ (3 / 4) ^ n

Tactic:
induction n generalizing c with
  | zero =>
    filter_upwards with y
    rw [pow_zero]
    exact Real.dist_le_of_mem_Icc_01 (c.lim_mem_Icc _) (c.lim_mem_Icc _)
  | succ n ihn =>
    by_cases hxl : x ∈ c.left.U
    · filter_upwards [IsOpen.mem_nhds c.left.open_U hxl, ihn c.left] with _ hyl hyd
      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)]
      refine (dist_midpoint_midpoint_le _ _ _ _).trans ?_
      rw [dist_self, add_zero, div_eq_inv_mul]
      gcongr
    · replace hxl : x ∈ c.left.right.Cᶜ :=
        compl_subset_compl.2 c.left.right.subset hxl
      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
      replace hxl : x ∉ c.left.left.U :=
        compl_subset_compl.2 c.left.left_U_subset_right_C hxl
      replace hyl : y ∉ c.left.left.U :=
        compl_subset_compl.2 c.left.left_U_subset_right_C hyl
      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]
      grw [dist_midpoint_midpoint_le, dist_midpoint_midpoint_le, dist_self, zero_add]
      set r := (3 / 4 : ℝ) ^ n
      calc _ ≤ (r / 2 + r) / 2 := by gcongr
        _ = _ := by ring

Premises used: pow_succ, dist_midpoint_midpoint_le, HDiv.hDiv, zero_add, pow_zero, dist_self, Urysohns.CU.left, Real.dist_le_of_mem_Icc_01, Urysohns.CU.U, LE.le.trans, div_eq_inv_mul, add_zero, OfNat.ofNat, pow_succ', Urysohns.CU.lim_mem_Icc, Urysohns.CU.lim_eq_midpoint
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : NormalSpace X
s t : Set X
hs : IsClosed[inst] s
ht : IsClosed[inst] t
hd : Disjoint s t
P : Set X → Set X → Prop := fun (x x_1 : Set X) ↦ True
c u : Set X
c_closed : IsClosed[inst] c
u_open : IsOpen[inst] u
cu : c ⊆ u
rcases :
  ∀ (v : Set X) (v_open : IsOpen[inst] v) (cv : c ⊆ v) (hv : closure[inst] v ⊆ u),
    ∃ (v : Set X), IsOpen[inst] v ∧ c ⊆ v ∧ closure[inst] v ⊆ u ∧ P c v ∧ P (closure[inst] v) u
⊢ ∃ (v : Set X), IsOpen[inst] v ∧ c ⊆ v ∧ closure[inst] v ⊆ u ∧ P c v ∧ P (closure[inst] v) u

Tactic:
rcases normal_exists_closure_subset c_closed u_open cu with ⟨v, v_open, cv, hv⟩

Premises used: normal_exists_closure_subset
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : NormalSpace X
s t : Set X
hs : IsClosed[inst] s
ht : IsClosed[inst] t
hd : Disjoint s t
P : Set X → Set X → Prop := fun (x x_1 : Set X) ↦ True
c u : Set X
c_closed : IsClosed[inst] c
u_open : IsOpen[inst] u
cu : c ⊆ u
v : Set X
v_open : IsOpen[inst] v
cv : c ⊆ v
hv : closure[inst] v ⊆ u
⊢ ∃ (v : Set X), IsOpen[inst] v ∧ c ⊆ v ∧ closure[inst] v ⊆ u ∧ P c v ∧ P (closure[inst] v) u

Tactic:
⟨v, v_open, cv, hv, trivial, trivial⟩

Premises used: trivial, And.intro, Exists.intro
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : NormalSpace X
s t : Set X
hs : IsClosed[inst] s
ht : IsClosed[inst] t
hd : Disjoint s t
P : Set X → Set X → Prop := fun (x x_1 : Set X) ↦ True
c u : Set X
c_closed : IsClosed[inst] c
u_open : IsOpen[inst] u
cu : c ⊆ u
v : Set X
v_open : IsOpen[inst] v
cv : c ⊆ v
hv : closure[inst] v ⊆ u
⊢ ∃ (v : Set X), IsOpen[inst] v ∧ c ⊆ v ∧ closure[inst] v ⊆ u ∧ P c v ∧ P (closure[inst] v) u

Tactic:
exact ⟨v, v_open, cv, hv, trivial, trivial⟩
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : NormalSpace X
s t : Set X
hs : IsClosed[inst] s
ht : IsClosed[inst] t
hd : Disjoint s t
P : Set X → Set X → Prop := fun (x x_1 : Set X) ↦ True
c : Urysohns.CU P := Urysohns.CU.mk (P := P) s tᶜ trivial hs ⋯ ⋯ ⋯
⊢ ∃ (f : C(X, ℝ)),
    EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 0 s ∧
      EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 t ∧
        ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)

Tactic:
⟨⟨c.lim, c.continuous_lim⟩, c.lim_of_mem_C, fun x hx => c.lim_of_notMem_U _ fun h => h hx,
    c.lim_mem_Icc⟩

Premises used: ContinuousMap.mk, Urysohns.CU.lim, Urysohns.CU.lim_of_mem_C, And.intro, Exists.intro, Urysohns.CU.continuous_lim, Urysohns.CU.lim_of_notMem_U, Urysohns.CU.lim_mem_Icc
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : NormalSpace X
s t : Set X
hs : IsClosed[inst] s
ht : IsClosed[inst] t
hd : Disjoint s t
P : Set X → Set X → Prop := fun (x x_1 : Set X) ↦ True
c : Urysohns.CU P := Urysohns.CU.mk (P := P) s tᶜ trivial hs ⋯ ⋯ ⋯
⊢ ∃ (f : C(X, ℝ)),
    EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 0 s ∧
      EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 t ∧
        ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)

Tactic:
exact ⟨⟨c.lim, c.continuous_lim⟩, c.lim_of_mem_C, fun x hx => c.lim_of_notMem_U _ fun h => h hx,
    c.lim_mem_Icc⟩
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
inst_2 : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed[inst] t
hd : Disjoint s t
⊢ ∃ (k : Set X), IsCompact k ∧ IsClosed[inst] k ∧ s ⊆ interior k ∧ k ⊆ tᶜ

Tactic:
exists_compact_closed_between hs ht.isOpen_compl hd.symm.subset_compl_left

Premises used: IsClosed.isOpen_compl, exists_compact_closed_between, Disjoint.symm, Disjoint.subset_compl_left
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
inst_2 : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed[inst] t
hd : Disjoint s t
obtain :
  ∀ (k : Set X) (k_comp : IsCompact k) (k_closed : IsClosed[inst] k) (sk : s ⊆ interior k) (kt : k ⊆ tᶜ),
    ∃ (f : C(X, ℝ)),
      EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 0 s ∧
        EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 t ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
⊢ ∃ (f : C(X, ℝ)),
    EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 0 s ∧
      EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 t ∧
        ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)

Tactic:
obtain ⟨k, k_comp, k_closed, sk, kt⟩ : ∃ k, IsCompact k ∧ IsClosed k ∧ s ⊆ interior k ∧ k ⊆ tᶜ :=
    exists_compact_closed_between hs ht.isOpen_compl hd.symm.subset_compl_left

Premises used: IsClosed.isOpen_compl, exists_compact_closed_between, Disjoint.symm, Disjoint.subset_compl_left
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
inst_2 : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed[inst] t
hd : Disjoint s t
k : Set X
k_comp : IsCompact k
k_closed : IsClosed[inst] k
sk : s ⊆ interior k
kt : k ⊆ tᶜ
P : Set X → Set X → Prop := fun (C x : Set X) ↦ IsCompact C
c u : Set X
c_comp : P c u
u_open : IsOpen[inst] u
cu : c ⊆ u
rcases :
  ∀ (k : Set X) (k_comp : IsCompact k) (k_closed : IsClosed[inst] k) (ck : c ⊆ interior k) (ku : k ⊆ u),
    ∃ (v : Set X), IsOpen[inst] v ∧ c ⊆ v ∧ closure[inst] v ⊆ u ∧ P c v ∧ P (closure[inst] v) u
⊢ ∃ (v : Set X), IsOpen[inst] v ∧ c ⊆ v ∧ closure[inst] v ⊆ u ∧ P c v ∧ P (closure[inst] v) u

Tactic:
rcases exists_compact_closed_between c_comp u_open cu with ⟨k, k_comp, k_closed, ck, ku⟩

Premises used: exists_compact_closed_between
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
inst_2 : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed[inst] t
hd : Disjoint s t
k_1 : Set X
k_comp_1 : IsCompact k_1
k_closed_1 : IsClosed[inst] k_1
sk : s ⊆ interior k_1
kt : k_1 ⊆ tᶜ
P : Set X → Set X → Prop := fun (C x : Set X) ↦ IsCompact C
c u : Set X
c_comp : P c u
u_open : IsOpen[inst] u
cu : c ⊆ u
k : Set X
k_comp : IsCompact k
k_closed : IsClosed[inst] k
ck : c ⊆ interior k
ku : k ⊆ u
⊢ closure[inst] (interior k) ⊆ k

Tactic:
have A : closure (interior k) ⊆ k :=
        (IsClosed.closure_subset_iff k_closed).2 interior_subset
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
inst_2 : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed[inst] t
hd : Disjoint s t
k_1 : Set X
k_comp_1 : IsCompact k_1
k_closed_1 : IsClosed[inst] k_1
sk : s ⊆ interior k_1
kt : k_1 ⊆ tᶜ
P : Set X → Set X → Prop := fun (C x : Set X) ↦ IsCompact C
c u : Set X
c_comp : P c u
u_open : IsOpen[inst] u
cu : c ⊆ u
k : Set X
k_comp : IsCompact k
k_closed : IsClosed[inst] k
ck : c ⊆ interior k
ku : k ⊆ u
A : closure[inst] (interior k) ⊆ k
⊢ ∃ (v : Set X), IsOpen[inst] v ∧ c ⊆ v ∧ closure[inst] v ⊆ u ∧ P c v ∧ P (closure[inst] v) u

Tactic:
⟨interior k, isOpen_interior, ck, A.trans ku, c_comp,
        k_comp.of_isClosed_subset isClosed_closure A⟩

Premises used: isOpen_interior, HasSubset.Subset.trans, IsCompact.of_isClosed_subset, And.intro, interior, Exists.intro, isClosed_closure
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
inst_2 : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed[inst] t
hd : Disjoint s t
k_1 : Set X
k_comp_1 : IsCompact k_1
k_closed_1 : IsClosed[inst] k_1
sk : s ⊆ interior k_1
kt : k_1 ⊆ tᶜ
P : Set X → Set X → Prop := fun (C x : Set X) ↦ IsCompact C
c u : Set X
c_comp : P c u
u_open : IsOpen[inst] u
cu : c ⊆ u
k : Set X
k_comp : IsCompact k
k_closed : IsClosed[inst] k
ck : c ⊆ interior k
ku : k ⊆ u
A : closure[inst] (interior k) ⊆ k
⊢ ∃ (v : Set X), IsOpen[inst] v ∧ c ⊆ v ∧ closure[inst] v ⊆ u ∧ P c v ∧ P (closure[inst] v) u

Tactic:
refine ⟨interior k, isOpen_interior, ck, A.trans ku, c_comp,
        k_comp.of_isClosed_subset isClosed_closure A⟩
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
inst_2 : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed[inst] t
hd : Disjoint s t
k : Set X
k_comp : IsCompact k
k_closed : IsClosed[inst] k
sk : s ⊆ interior k
kt : k ⊆ tᶜ
P : Set X → Set X → Prop := fun (C x : Set X) ↦ IsCompact C
c : Urysohns.CU P := Urysohns.CU.mk (P := P) k tᶜ k_comp k_closed ⋯ kt ⋯
⊢ ∃ (f : C(X, ℝ)),
    EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 0 s ∧
      EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 t ∧
        ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)

Tactic:
⟨⟨c.lim, c.continuous_lim⟩, fun x hx ↦ c.lim_of_mem_C _ (sk.trans interior_subset hx),
    fun x hx => c.lim_of_notMem_U _ fun h => h hx, c.lim_mem_Icc⟩

Premises used: interior_subset, ContinuousMap.mk, HasSubset.Subset.trans, Urysohns.CU.lim, Urysohns.CU.lim_of_mem_C, And.intro, Exists.intro, Urysohns.CU.continuous_lim, Urysohns.CU.lim_of_notMem_U, Urysohns.CU.lim_mem_Icc
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
inst_2 : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed[inst] t
hd : Disjoint s t
k : Set X
k_comp : IsCompact k
k_closed : IsClosed[inst] k
sk : s ⊆ interior k
kt : k ⊆ tᶜ
P : Set X → Set X → Prop := fun (C x : Set X) ↦ IsCompact C
c : Urysohns.CU P := Urysohns.CU.mk (P := P) k tᶜ k_comp k_closed ⋯ kt ⋯
⊢ ∃ (f : C(X, ℝ)),
    EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 0 s ∧
      EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 t ∧
        ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)

Tactic:
exact ⟨⟨c.lim, c.continuous_lim⟩, fun x hx ↦ c.lim_of_mem_C _ (sk.trans interior_subset hx),
    fun x hx => c.lim_of_notMem_U _ fun h => h hx, c.lim_mem_Icc⟩
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
inst_2 : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed[inst] t
hd : Disjoint s t
obtain :
  ∀ (g : C(X, ℝ)) (hgs : EqOn (β := ℝ) (⇑g : (a : X) → ℝ) 0 s) (hgt : EqOn (β := ℝ) (⇑g : (a : X) → ℝ) 1 t)
    (hicc :
      ∀ (x : X), LE.le (α := ℝ) (0 : ℝ) ((g : (a : X) → ℝ) x : ℝ) ∧ LE.le (α := ℝ) ((g : (a : X) → ℝ) x : ℝ) (1 : ℝ)),
    ∃ (f : C(X, ℝ)),
      EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 0 t ∧
        EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 s ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
⊢ ∃ (f : C(X, ℝ)),
    EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 0 t ∧
      EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 s ∧
        ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)

Tactic:
obtain ⟨g, hgs, hgt, (hicc : ∀ x, 0 ≤ g x ∧ g x ≤ 1)⟩ := exists_continuous_zero_one_of_isCompact
    hs ht hd

Premises used: exists_continuous_zero_one_of_isCompact
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
inst_2 : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed[inst] t
hd : Disjoint s t
g : C(X, ℝ)
hgs : EqOn (β := ℝ) (⇑g : (a : X) → ℝ) 0 s
hgt : EqOn (β := ℝ) (⇑g : (a : X) → ℝ) 1 t
hicc : ∀ (x : X), LE.le (α := ℝ) (0 : ℝ) ((g : (a : X) → ℝ) x : ℝ) ∧ LE.le (α := ℝ) ((g : (a : X) → ℝ) x : ℝ) (1 : ℝ)
h :
  EqOn (β := ℝ) (⇑(1 - g) : (a : X) → ℝ) 0 t ∧
    EqOn (β := ℝ) (⇑(1 - g) : (a : X) → ℝ) 1 s ∧
      ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((1 - g : (a : X) → ℝ) x : ℝ)
⊢ ∃ (f : C(X, ℝ)),
    EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 0 t ∧
      EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 s ∧
        ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)

Tactic:
use 1 - g
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
inst_2 : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed[inst] t
hd : Disjoint s t
g : C(X, ℝ)
hgs : EqOn (β := ℝ) (⇑g : (a : X) → ℝ) 0 s
hgt : EqOn (β := ℝ) (⇑g : (a : X) → ℝ) 1 t
hicc : ∀ (x : X), LE.le (α := ℝ) (0 : ℝ) ((g : (a : X) → ℝ) x : ℝ) ∧ LE.le (α := ℝ) ((g : (a : X) → ℝ) x : ℝ) (1 : ℝ)
⊢ EqOn (β := ℝ) (⇑(1 - g) : (a : X) → ℝ) 0 t ∧
    EqOn (β := ℝ) (⇑(1 - g) : (a : X) → ℝ) 1 s ∧
      ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((1 - g : (a : X) → ℝ) x : ℝ)

Tactic:
⟨?_, ?_, ?_⟩

Premises used: And.intro
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
inst_2 : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed[inst] t
hd : Disjoint s t
g : C(X, ℝ)
hgs : EqOn (β := ℝ) (⇑g : (a : X) → ℝ) 0 s
hgt : EqOn (β := ℝ) (⇑g : (a : X) → ℝ) 1 t
hicc : ∀ (x : X), LE.le (α := ℝ) (0 : ℝ) ((g : (a : X) → ℝ) x : ℝ) ∧ LE.le (α := ℝ) ((g : (a : X) → ℝ) x : ℝ) (1 : ℝ)
h : EqOn (β := ℝ) (⇑(1 - g) : (a : X) → ℝ) 0 t
h₁ : EqOn (β := ℝ) (⇑(1 - g) : (a : X) → ℝ) 1 s
h₂ : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((1 - g : (a : X) → ℝ) x : ℝ)
⊢ EqOn (β := ℝ) (⇑(1 - g) : (a : X) → ℝ) 0 t ∧
    EqOn (β := ℝ) (⇑(1 - g) : (a : X) → ℝ) 1 s ∧
      ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((1 - g : (a : X) → ℝ) x : ℝ)

Tactic:
refine ⟨?_, ?_, ?_⟩
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
inst_2 : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed[inst] t
hd : Disjoint s t
g : C(X, ℝ)
hgs : EqOn (β := ℝ) (⇑g : (a : X) → ℝ) 0 s
hgt : EqOn (β := ℝ) (⇑g : (a : X) → ℝ) 1 t
hicc : ∀ (x : X), LE.le (α := ℝ) (0 : ℝ) ((g : (a : X) → ℝ) x : ℝ) ∧ LE.le (α := ℝ) ((g : (a : X) → ℝ) x : ℝ) (1 : ℝ)
x : X
hx : x ∈ t
⊢ HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((g : (a : X) → ℝ) x : ℝ) = 0

Tactic:
sub_eq_zero_of_eq (hgt.symm hx)

Premises used: sub_eq_zero_of_eq, Set.EqOn.symm
-- Module: Mathlib.Topology.UrysohnsLemma
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
inst_2 : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed[inst] t
hd : Disjoint s t
g : C(X, ℝ)
hgs : EqOn (β := ℝ) (⇑g : (a : X) → ℝ) 0 s
hgt : EqOn (β := ℝ) (⇑g : (a : X) → ℝ) 1 t
hicc : ∀ (x : X), LE.le (α := ℝ) (0 : ℝ) ((g : (a : X) → ℝ) x : ℝ) ∧ LE.le (α := ℝ) ((g : (a : X) → ℝ) x : ℝ) (1 : ℝ)
x : X
hx : x ∈ t
⊢ HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((g : (a : X) → ℝ) x : ℝ) = 0

Tactic:
exact sub_eq_zero_of_eq (hgt.symm hx)

Premises used: sub_eq_zero_of_eq, Set.EqOn.symm