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
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
⊢ (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₁ : (r / 2 + r) / 2 = r * (3 / 4)
Tactic: calc _ ≤ (r / 2 + r) / 2 := by gcongr
        _ = _ := by ring
-- 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
x : X
n : ℕ
h : True
⊢ ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim (P := P) x_1) (c.lim (P := P) x) ≤ (3 / 4) ^ n
have 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
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
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
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
⊢ ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim (P := P) x_1) (c.lim (P := P) x) ≤ (3 / 4) ^ n
have 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)
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
Cleared hypotheses: c, n
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
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), IsOpen[inst] v ∧ c ⊆ v ∧ closure[inst] v ⊆ u ∧ P c v ∧ P (closure[inst] v) u
have 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
Tactic: rcases normal_exists_closure_subset c_closed u_open cu with ⟨v, v_open, cv, hv⟩
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
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
⊢ ∃ (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 : ℝ)
have 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 : ℝ)
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
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
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
⊢ ∃ (v : Set X), IsOpen[inst] v ∧ c ⊆ v ∧ closure[inst] v ⊆ u ∧ P c v ∧ P (closure[inst] v) u
have 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
Tactic: rcases exists_compact_closed_between c_comp u_open cu with ⟨k, k_comp, k_closed, ck, ku⟩
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (hypothesis)
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
⊢ ∃ (v : Set X), IsOpen[inst] v ∧ c ⊆ v ∧ closure[inst] v ⊆ u ∧ P c v ∧ P (closure[inst] v) u
have A : closure[inst] (interior k) ⊆ k
Tactic: have A : closure (interior k) ⊆ k :=
        (IsClosed.closure_subset_iff k_closed).2 interior_subset
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
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
⊢ ∃ (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 : ℝ)
have 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 : ℝ)
Tactic: obtain ⟨g, hgs, hgt, (hicc : ∀ x, 0 ≤ g x ∧ g x ≤ 1)⟩ := exists_continuous_zero_one_of_isCompact
    hs ht hd
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
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 : ℝ)
⊢ ∃ (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 : ℝ)
have 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 : ℝ)
Tactic: use 1 - g
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
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 : ℝ)
have h : EqOn (β := ℝ) (⇑(1 - g) : (a : X) → ℝ) 0 t
Tactic: refine ⟨?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
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) → ℝ) 0 t ∧
    EqOn (β := ℝ) (⇑(1 - g) : (a : X) → ℝ) 1 s ∧
      ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((1 - g : (a : X) → ℝ) x : ℝ)
have h₁ : EqOn (β := ℝ) (⇑(1 - g) : (a : X) → ℝ) 1 s
Tactic: refine ⟨?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
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
⊢ 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 : ℝ)
have h₂ : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((1 - g : (a : X) → ℝ) x : ℝ)
Tactic: refine ⟨?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
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 ∈ s
⊢ Eq (α := ℝ) ((1 - g : (a : X) → ℝ) x : ℝ) (1 x : ℝ)
have h : Eq (α := ℝ) ((g : (a : X) → ℝ) x : ℝ) (0 : ℝ)
Tactic: simp only [ContinuousMap.sub_apply, ContinuousMap.one_apply, Pi.one_apply, sub_eq_self]
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
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
⊢ ∃ (f : C(X, ℝ)),
    EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 s ∧
      EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 0 t ∧
        HasCompactSupport (α := X) (β := ℝ) (⇑f : (a : X) → ℝ) ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
have 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) → ℝ) 1 s ∧
      EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 0 t ∧
        HasCompactSupport (α := X) (β := ℝ) (⇑f : (a : X) → ℝ) ∧
          ∀ (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
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
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ᶜ
⊢ ∃ (f : C(X, ℝ)),
    EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 s ∧
      EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 0 t ∧
        HasCompactSupport (α := X) (β := ℝ) (⇑f : (a : X) → ℝ) ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
have rcases : ∀ (f : X → ℝ) (hf : Continuous[inst, _] f)
  (hfs : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) 0 s)
  (hft : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) 1 (interior k)ᶜ)
  (h'f :
    ∀ (x : X),
      Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1)
        (({ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) x : ℝ)),
  ∃ (f : C(X, ℝ)),
    EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 s ∧
      EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 0 t ∧
        HasCompactSupport (α := X) (β := ℝ) (⇑f : (a : X) → ℝ) ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
Tactic: rcases exists_continuous_zero_one_of_isCompact hs isOpen_interior.isClosed_compl
    (disjoint_compl_right_iff_subset.mpr sk) with ⟨⟨f, hf⟩, hfs, hft, h'f⟩
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (hypothesis)
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ᶜ
f : X → ℝ
hf : Continuous[inst, _] f
hfs : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) 0 s
hft : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) 1 (interior k)ᶜ
h'f :
  ∀ (x : X),
    Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1)
      (({ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) x : ℝ)
⊢ ∃ (f : C(X, ℝ)),
    EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 s ∧
      EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 0 t ∧
        HasCompactSupport (α := X) (β := ℝ) (⇑f : (a : X) → ℝ) ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
have A : t ⊆ (interior k)ᶜ
Tactic: have A : t ⊆ (interior k)ᶜ := subset_compl_comm.mpr (interior_subset.trans kt)
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
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ᶜ
f : X → ℝ
hf : Continuous[inst, _] f
hfs : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) 0 s
hft : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) 1 (interior k)ᶜ
h'f :
  ∀ (x : X),
    Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1)
      (({ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) x : ℝ)
A : t ⊆ (interior k)ᶜ
⊢ ∃ (f : C(X, ℝ)),
    EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 s ∧
      EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 0 t ∧
        HasCompactSupport (α := X) (β := ℝ) (⇑f : (a : X) → ℝ) ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
have refine_1 : HasCompactSupport (α := X) (β := ℝ) (⇑{ toFun := fun (x : X) ↦ 1 - f x, continuous_toFun := sorry : C(X, ℝ) } : (a : X) → ℝ)
Tactic: refine ⟨⟨fun x ↦ 1 - f x, by fun_prop⟩, fun x hx ↦ by simpa using hfs hx,
    fun x hx ↦ by simpa [sub_eq_zero] using (hft (A hx)).symm, ?_, fun x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
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ᶜ
f : X → ℝ
hf : Continuous[inst, _] f
hfs : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) 0 s
hft : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) 1 (interior k)ᶜ
h'f :
  ∀ (x : X),
    Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1)
      (({ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) x : ℝ)
A : t ⊆ (interior k)ᶜ
refine_1 :
  HasCompactSupport (α := X) (β := ℝ)
    (⇑{ toFun := fun (x : X) ↦ 1 - f x, continuous_toFun := ⋯ : C(X, ℝ) } : (a : X) → ℝ)
⊢ ∃ (f : C(X, ℝ)),
    EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 s ∧
      EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 0 t ∧
        HasCompactSupport (α := X) (β := ℝ) (⇑f : (a : X) → ℝ) ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
have refine_2 : ∀ (x : X),
  Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1)
    (({ toFun := fun (x : X) ↦ 1 - f x, continuous_toFun := sorry : C(X, ℝ) } : (a : X) → ℝ) x : ℝ)
Tactic: refine ⟨⟨fun x ↦ 1 - f x, by fun_prop⟩, fun x hx ↦ by simpa using hfs hx,
    fun x hx ↦ by simpa [sub_eq_zero] using (hft (A hx)).symm, ?_, fun x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
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ᶜ
f : X → ℝ
hf : Continuous[inst, _] f
hfs : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) 0 s
hft : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) 1 (interior k)ᶜ
h'f :
  ∀ (x : X),
    Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1)
      (({ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) x : ℝ)
A : t ⊆ (interior k)ᶜ
⊢ HasCompactSupport (α := X) (β := ℝ)
    (⇑{ toFun := fun (x : X) ↦ 1 - f x, continuous_toFun := ⋯ : C(X, ℝ) } : (a : X) → ℝ)
have apply : ∀ (x : X) (hx : x ∉ k),
  Eq (α := ℝ) (({ toFun := fun (x : X) ↦ 1 - f x, continuous_toFun := sorry : C(X, ℝ) } : (a : X) → ℝ) x : ℝ) (0 : ℝ)
Tactic: apply HasCompactSupport.intro' k_comp k_closed (fun x hx ↦ ?_)
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
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ᶜ
f : X → ℝ
hf : Continuous[inst, _] f
hfs : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) 0 s
hft : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) 1 (interior k)ᶜ
h'f :
  ∀ (x : X),
    Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1)
      (({ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) x : ℝ)
A : t ⊆ (interior k)ᶜ
x : X
hx : x ∉ k
⊢ Eq (α := ℝ) (({ toFun := fun (x : X) ↦ 1 - f x, continuous_toFun := ⋯ : C(X, ℝ) } : (a : X) → ℝ) x : ℝ) (0 : ℝ)
have simp : 1 = f x
Tactic: simp only [ContinuousMap.coe_mk, sub_eq_zero]
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
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ᶜ
f : X → ℝ
hf : Continuous[inst, _] f
hfs : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) 0 s
hft : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) 1 (interior k)ᶜ
h'f :
  ∀ (x : X),
    Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1)
      (({ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) x : ℝ)
A : t ⊆ (interior k)ᶜ
x : X
hx : x ∉ k
⊢ 1 = f x
have apply : x ∈ (interior k)ᶜ
Tactic: apply (hft _).symm
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
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ᶜ
f : X → ℝ
hf : Continuous[inst, _] f
hfs : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) 0 s
hft : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) 1 (interior k)ᶜ
h'f :
  ∀ (x : X),
    Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1)
      (({ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) x : ℝ)
A : t ⊆ (interior k)ᶜ
x : X
hx : x ∉ k
⊢ x ∈ (interior k)ᶜ
have contrapose : ∀ (hx : x ∉ (interior k)ᶜ), x ∈ k
Tactic: contrapose hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (hypothesis)
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ᶜ
f : X → ℝ
hf : Continuous[inst, _] f
hfs : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) 0 s
hft : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) 1 (interior k)ᶜ
h'f :
  ∀ (x : X),
    Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1)
      (({ toFun := f, continuous_toFun := hf : C(X, ℝ) } : (a : X) → ℝ) x : ℝ)
A : t ⊆ (interior k)ᶜ
x : X
hx : x ∉ (interior k)ᶜ
⊢ x ∈ k
have hx₁ : x ∈ interior k
Tactic: simp only [mem_compl_iff, not_not] at hx
Cleared hypotheses: hx