awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : IsDiscrete s
x : X
hx : x ∈ s
V : Set X
h : V ∈ 𝓝 x
h' : V ∩ s = {x}
rw : {x}ᶜ ∩ (V ∩ s) = ∅
⊢ {x}ᶜ ∩ V ∩ s = ∅
have rw₁ : Eq (α := Set X) ({x}ᶜ ∩ {x}) ∅
Tactic: rw [inter_assoc, h', compl_inter_self]
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : IsDiscrete s
x : X
hx : x ∈ s
V : Set X
h : V ∈ 𝓝 x
h' : V ∩ s = {x}
rw : {x}ᶜ ∩ (V ∩ s) = ∅
rw₁ : Eq (α := Set X) ({x}ᶜ ∩ {x}) ∅
⊢ {x}ᶜ ∩ V ∩ s = ∅
have rw₂ : Eq.{u_1 + 1} (α := Set X) ∅ ∅
Tactic: rw [inter_assoc, h', compl_inter_self]
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
ι : Type u_3
β : ι → Type u_4
inst : DecidableEq ι
inst_1 : (i : ι) → TopologicalSpace (β i)
x : (i : ι) → β i
i : ι
inst_2 : ∀ (i : ι), T1Space.{u_4} (β i)
⊢ IsClosedEmbedding (update (β := β) x i)
have refine : ∀ (s : Set (β i)) (hs : IsClosed[inst_1 i] s), IsClosed[Pi.topologicalSpace] (update (β := β) x i '' s)
Tactic: refine .of_continuous_injective_isClosedMap (continuous_const.update i continuous_id)
    (update_injective x i) fun s hs ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
ι : Type u_3
β : ι → Type u_4
inst : DecidableEq ι
inst_1 : (i : ι) → TopologicalSpace (β i)
x : (i : ι) → β i
i : ι
inst_2 : ∀ (i : ι), T1Space.{u_4} (β i)
s : Set (β i)
hs : IsClosed[inst_1 i] s
⊢ IsClosed[Pi.topologicalSpace] (update (β := β) x i '' s)
have rw : IsClosed[Pi.topologicalSpace] (Set.pi (α := β) univ (update (β := fun (i : ι) ↦ Set (β i)) (fun (j : ι) ↦ {x j}) i s))
Tactic: rw [update_image]
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
ι : Type u_3
β : ι → Type u_4
inst : DecidableEq ι
inst_1 : (i : ι) → TopologicalSpace (β i)
x : (i : ι) → β i
i : ι
inst_2 : ∀ (i : ι), T1Space.{u_4} (β i)
s : Set (β i)
hs : IsClosed[inst_1 i] s
⊢ IsClosed[Pi.topologicalSpace] (Set.pi (α := β) univ (update (β := fun (i : ι) ↦ Set (β i)) (fun (j : ι) ↦ {x j}) i s))
have hs₁ : ∀ (a : ι),
  Membership.mem (γ := Set ι) univ a →
    IsClosed[inst_1 a] (update (β := fun (i : ι) ↦ Set (β i)) (fun (j : ι) ↦ {x j}) i s a)
Tactic: apply isClosed_set_pi
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
α : Type u_3
inst : TopologicalSpace α
inst_1 : T1Space α
a : α
⊢ 𝓝[≠] a ≤ cofinite
have refine : ∀ (x : α), {x}ᶜ ∈ 𝓝[≠] a
Tactic: refine le_cofinite_iff_compl_singleton_mem.mpr fun x ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
α : Type u_3
inst : TopologicalSpace α
inst_1 : T1Space α
a x : α
⊢ {x}ᶜ ∈ 𝓝[≠] a
have inl : {a}ᶜ ∈ 𝓝[≠] a
Tactic: rcases eq_or_ne a x with rfl | hx
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
α : Type u_3
inst : TopologicalSpace α
inst_1 : T1Space α
a x : α
inl : {a}ᶜ ∈ 𝓝[≠] a
⊢ {x}ᶜ ∈ 𝓝[≠] a
have inr : ∀ (hx : a ≠ x), {x}ᶜ ∈ 𝓝[≠] a
Tactic: rcases eq_or_ne a x with rfl | hx
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
x y : X
⊢ Disjoint (𝓝 x) (𝓝 y) ↔ ¬Inseparable x y
have rw : ¬x ⤳ y ↔ ¬Inseparable x y
Tactic: rw [disjoint_nhds_nhds_iff_not_specializes, specializes_iff_inseparable]
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
x y : X
rw : ¬x ⤳ y ↔ ¬Inseparable x y
⊢ Disjoint (𝓝 x) (𝓝 y) ↔ ¬Inseparable x y
have rw₁ : ¬Inseparable x y ↔ ¬Inseparable x y
Tactic: rw [disjoint_nhds_nhds_iff_not_specializes, specializes_iff_inseparable]
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
x y : X
h : ¬Inseparable x y
⊢ ∃ (u : Set X) (v : Set X), IsOpen[inst] u ∧ IsOpen[inst] v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v
have h₁ : ∃ (i : Set X), (x ∈ i ∧ IsOpen[inst] i) ∧ ∃ (i' : Set X), (y ∈ i' ∧ IsOpen[inst] i') ∧ Disjoint i i'
Tactic: rw [← disjoint_nhds_nhds_iff_not_inseparable,
    (nhds_basis_opens x).disjoint_iff (nhds_basis_opens y)] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
x y : X
h : ∃ (i : Set X), (x ∈ i ∧ IsOpen[inst] i) ∧ ∃ (i' : Set X), (y ∈ i' ∧ IsOpen[inst] i') ∧ Disjoint i i'
⊢ ∃ (u : Set X) (v : Set X), IsOpen[inst] u ∧ IsOpen[inst] v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v
have obtain : ∀ (u : Set X) (hxu : x ∈ u) (hu : IsOpen[inst] u) (v : Set X) (huv : Disjoint u v) (hyv : y ∈ v) (hv : IsOpen[inst] v),
  ∃ (u : Set X) (v : Set X), IsOpen[inst] u ∧ IsOpen[inst] v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v
Tactic: obtain ⟨u, ⟨hxu, hu⟩, v, ⟨hyv, hv⟩, huv⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
y : X
K : Set X
hK : IsCompact K
⊢ y ∈ closure[inst] K ↔ ∃ x ∈ K, Inseparable x y
have refine : ∀ (hy : y ∈ closure[inst] K), ∃ x ∈ K, Inseparable x y
Tactic: refine ⟨fun hy ↦ ?_, fun ⟨x, hxK, hxy⟩ ↦
    (hxy.mem_closed_iff isClosed_closure).1 <| subset_closure hxK⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
y : X
K : Set X
hK : IsCompact K
hy : y ∈ closure[inst] K
⊢ ∃ x ∈ K, Inseparable x y
have contrapose! : ∀ (hy : ∀ (x : X) (_ : x ∈ K), ¬Inseparable x y), y ∉ closure[inst] K
Tactic: contrapose! hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
y : X
K : Set X
hK : IsCompact K
hy : ∀ (x : X) (_ : x ∈ K), ¬Inseparable x y
⊢ y ∉ closure[inst] K
have this : Disjoint (𝓝 y) (𝓝ˢ K)
Tactic: have : Disjoint (𝓝 y) (𝓝ˢ K) := hK.disjoint_nhdsSet_right.2 fun x hx ↦
    (disjoint_nhds_nhds_iff_not_inseparable.2 (hy x hx)).symm
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
K : Set X
hK : IsCompact K
⊢ closure[inst] K = ⋃ x ∈ K, {y : X | Inseparable x y}
have h : ∀ (x : X), x ∈ closure[inst] K ↔ Membership.mem (γ := Set X) (⋃ x ∈ K, {y : X | Inseparable x y}) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
K : Set X
hK : IsCompact K
U : Set X
hU : IsOpen[inst] U
hKU : K ⊆ U
⊢ closure[inst] K ⊆ U
have rw : ∀ (i : X) (j : i ∈ K), {y : X | Inseparable i y} ⊆ U
Tactic: rw [hK.closure_eq_biUnion_inseparable, iUnion₂_subset_iff]
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
K : Set X
hK : IsCompact K
⊢ IsCompact (closure[inst] K)
have refine : ∀ {ι : Type u_1} (U : ι → Set X) (hUo : ∀ (i : ι), IsOpen[inst] (U i)) (hKU : closure[inst] K ⊆ ⋃ (i : ι), U i),
  ∃ (t : Finset ι), closure[inst] K ⊆ ⋃ i ∈ t, U i
Tactic: refine isCompact_of_finite_subcover fun U hUo hKU ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
K : Set X
hK : IsCompact K
ι : Type u_1
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hKU : closure[inst] K ⊆ ⋃ (i : ι), U i
⊢ ∃ (t : Finset ι), closure[inst] K ⊆ ⋃ i ∈ t, U i
have rcases : ∀ (t : Finset ι) (ht : K ⊆ ⋃ i ∈ t, U i), ∃ (t : Finset ι), closure[inst] K ⊆ ⋃ i ∈ t, U i
Tactic: rcases hK.elim_finite_subcover U hUo (subset_closure.trans hKU) with ⟨t, ht⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
K L : Set X
hK : IsCompact K
hL : IsCompact L
h'L : IsClosed[inst] L
hd : Disjoint K L
⊢ SeparatedNhds K L
have simp_rw : ∀ x ∈ K, ∀ x_1 ∈ L, ¬Inseparable x x_1
Tactic: simp_rw [separatedNhds_iff_disjoint, hK.disjoint_nhdsSet_left, hL.disjoint_nhdsSet_right,
    disjoint_nhds_nhds_iff_not_inseparable]
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
K U V : Set X
hK : IsCompact K
hU : IsOpen[inst] U
hV : IsOpen[inst] V
h2K : K ⊆ U ∪ V
⊢ ∃ (K₁ : Set X) (K₂ : Set X), IsCompact K₁ ∧ IsCompact K₂ ∧ K₁ ⊆ U ∧ K₂ ⊆ V ∧ K = K₁ ∪ K₂
have hK' : IsCompact (closure[inst] K)
Tactic: have hK' : IsCompact (closure K) := hK.closure
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
K U V : Set X
hK : IsCompact K
hU : IsOpen[inst] U
hV : IsOpen[inst] V
h2K : K ⊆ U ∪ V
hK' : IsCompact (closure[inst] K)
⊢ SeparatedNhds (closure[inst] K \ U) (closure[inst] K \ V)
have apply : Disjoint (closure[inst] K \ U) (closure[inst] K \ V)
Tactic: apply SeparatedNhds.of_isCompact_isCompact_isClosed (hK'.diff hU) (hK'.diff hV)
      (isClosed_closure.sdiff hV)
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
K U V : Set X
hK : IsCompact K
hU : IsOpen[inst] U
hV : IsOpen[inst] V
h2K : K ⊆ U ∪ V
hK' : IsCompact (closure[inst] K)
⊢ Disjoint (closure[inst] K \ U) (closure[inst] K \ V)
have rw : closure[inst] K ⊆ U ∪ V
Tactic: rw [disjoint_iff_inter_eq_empty, diff_inter_diff, diff_eq_empty]
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
K U V : Set X
hK : IsCompact K
hU : IsOpen[inst] U
hV : IsOpen[inst] V
h2K : K ⊆ U ∪ V
hK' : IsCompact (closure[inst] K)
⊢ ∃ (K₁ : Set X) (K₂ : Set X), IsCompact K₁ ∧ IsCompact K₂ ∧ K₁ ⊆ U ∧ K₂ ⊆ V ∧ K = K₁ ∪ K₂
have this : SeparatedNhds (closure[inst] K \ U) (closure[inst] K \ V)
Tactic: have : SeparatedNhds (closure K \ U) (closure K \ V) := by
    apply SeparatedNhds.of_isCompact_isCompact_isClosed (hK'.diff hU) (hK'.diff hV)
      (isClosed_closure.sdiff hV)
    rw [disjoint_iff_inter_eq_empty, diff_inter_diff, diff_eq_empty]
    exact hK.closure_subset_of_isOpen (hU.union hV) h2K
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
K U V : Set X
hK : IsCompact K
hU : IsOpen[inst] U
hV : IsOpen[inst] V
h2K : K ⊆ U ∪ V
hK' : IsCompact (closure[inst] K)
this : SeparatedNhds (closure[inst] K \ U) (closure[inst] K \ V)
⊢ ∃ (K₁ : Set X) (K₂ : Set X), IsCompact K₁ ∧ IsCompact K₂ ∧ K₁ ⊆ U ∧ K₂ ⊆ V ∧ K = K₁ ∪ K₂
have this₁ : SeparatedNhds (K \ U) (K \ V)
Tactic: have : SeparatedNhds (K \ U) (K \ V) :=
    this.mono (diff_subset_diff_left (subset_closure)) (diff_subset_diff_left (subset_closure))
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
K U V : Set X
hK : IsCompact K
hU : IsOpen[inst] U
hV : IsOpen[inst] V
h2K : K ⊆ U ∪ V
hK' : IsCompact (closure[inst] K)
this_1 : SeparatedNhds (closure[inst] K \ U) (closure[inst] K \ V)
this : SeparatedNhds (K \ U) (K \ V)
⊢ ∃ (K₁ : Set X) (K₂ : Set X), IsCompact K₁ ∧ IsCompact K₂ ∧ K₁ ⊆ U ∧ K₂ ⊆ V ∧ K = K₁ ∪ K₂
have rcases : ∀ (O₁ O₂ : Set X) (h1O₁ : IsOpen[inst] O₁) (h1O₂ : IsOpen[inst] O₂) (h2O₁ : K \ U ⊆ O₁) (h2O₂ : K \ V ⊆ O₂)
  (hO : Disjoint O₁ O₂), ∃ (K₁ : Set X) (K₂ : Set X), IsCompact K₁ ∧ IsCompact K₂ ∧ K₁ ⊆ U ∧ K₂ ⊆ V ∧ K = K₁ ∪ K₂
Tactic: rcases this with ⟨O₁, O₂, h1O₁, h1O₂, h2O₁, h2O₂, hO⟩
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
K U V : Set X
hK : IsCompact K
hU : IsOpen[inst] U
hV : IsOpen[inst] V
h2K : K ⊆ U ∪ V
hK' : IsCompact (closure[inst] K)
this : SeparatedNhds (closure[inst] K \ U) (closure[inst] K \ V)
O₁ O₂ : Set X
h1O₁ : IsOpen[inst] O₁
h1O₂ : IsOpen[inst] O₂
h2O₁ : K \ U ⊆ O₁
h2O₂ : K \ V ⊆ O₂
hO : Disjoint O₁ O₂
⊢ K = K \ O₁ ∪ K \ O₂
have rw : K = K \ (O₁ ∩ O₂)
Tactic: rw [← diff_inter, hO.inter_eq, diff_empty]
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
K U V : Set X
hK : IsCompact K
hU : IsOpen[inst] U
hV : IsOpen[inst] V
h2K : K ⊆ U ∪ V
hK' : IsCompact (closure[inst] K)
this : SeparatedNhds (closure[inst] K \ U) (closure[inst] K \ V)
O₁ O₂ : Set X
h1O₁ : IsOpen[inst] O₁
h1O₂ : IsOpen[inst] O₂
h2O₁ : K \ U ⊆ O₁
h2O₂ : K \ V ⊆ O₂
hO : Disjoint O₁ O₂
rw : K = K \ (O₁ ∩ O₂)
⊢ K = K \ O₁ ∪ K \ O₂
have rw₁ : K = K \ ∅
Tactic: rw [← diff_inter, hO.inter_eq, diff_empty]
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
K U V : Set X
hK : IsCompact K
hU : IsOpen[inst] U
hV : IsOpen[inst] V
h2K : K ⊆ U ∪ V
hK' : IsCompact (closure[inst] K)
this : SeparatedNhds (closure[inst] K \ U) (closure[inst] K \ V)
O₁ O₂ : Set X
h1O₁ : IsOpen[inst] O₁
h1O₂ : IsOpen[inst] O₂
h2O₁ : K \ U ⊆ O₁
h2O₂ : K \ V ⊆ O₂
hO : Disjoint O₁ O₂
rw : K = K \ (O₁ ∩ O₂)
rw₁ : K = K \ ∅
⊢ K = K \ O₁ ∪ K \ O₂
have rw₂ : K = K
Tactic: rw [← diff_inter, hO.inter_eq, diff_empty]
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
ι : Type u_3
s : Set X
hs : IsCompact s
U : ι → Set X
hU : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → IsOpen[inst] (U i)
hsC : s ⊆ ⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), U i
⊢ ∃ (K : ι → Set X),
    (∀ (i : ι), IsCompact (K i)) ∧
      (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), K i
have empty : s = ⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), (fun (x : ι) ↦ (∅ : Set X)) i
Tactic: refine ⟨fun _ => ∅, fun _ => isCompact_empty, fun i => empty_subset _, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
ι : Type u_3
x : ι
t : Finset ι
hx : x ∉ t
ih :
  ∀ {s : Set X} (hs : IsCompact s) (U : ι → Set X) (hU : ∀ i ∈ t, IsOpen[inst] (U i)) (hsC : s ⊆ ⋃ i ∈ t, U i),
    ∃ (K : ι → Set X), (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ t, K i
s : Set X
hs : IsCompact s
U : ι → Set X
hU : ∀ i ∈ insert x t, IsOpen[inst] (U i)
hsC : s ⊆ ⋃ i ∈ insert x t, U i
⊢ ∃ (K : ι → Set X), (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ insert x t, K i
have hsC₁ : s ⊆ U x ∪ ⋃ x ∈ t, U x
Tactic: simp only [Finset.set_biUnion_insert] at hsC
Cleared hypotheses: hsC
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
ι : Type u_3
x : ι
t : Finset ι
hx : x ∉ t
ih :
  ∀ {s : Set X} (hs : IsCompact s) (U : ι → Set X) (hU : ∀ i ∈ t, IsOpen[inst] (U i)) (hsC : s ⊆ ⋃ i ∈ t, U i),
    ∃ (K : ι → Set X), (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ t, K i
s : Set X
hs : IsCompact s
U : ι → Set X
hU : ∀ i ∈ insert x t, IsOpen[inst] (U i)
hsC : s ⊆ U x ∪ ⋃ x ∈ t, U x
⊢ ∃ (K : ι → Set X), (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ insert x t, K i
have hU₁ : IsOpen[inst] (U x) ∧ ∀ x ∈ t, IsOpen[inst] (U x)
Tactic: simp only [Finset.forall_mem_insert] at hU
Cleared hypotheses: hU
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
ι : Type u_3
x : ι
t : Finset ι
hx : x ∉ t
ih :
  ∀ {s : Set X} (hs : IsCompact s) (U : ι → Set X) (hU : ∀ i ∈ t, IsOpen[inst] (U i)) (hsC : s ⊆ ⋃ i ∈ t, U i),
    ∃ (K : ι → Set X), (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ t, K i
s : Set X
hs : IsCompact s
U : ι → Set X
hsC : s ⊆ U x ∪ ⋃ x ∈ t, U x
hU : IsOpen[inst] (U x) ∧ ∀ x ∈ t, IsOpen[inst] (U x)
⊢ ∃ (K : ι → Set X), (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ insert x t, K i
have hU' : ∀ i ∈ t, IsOpen[inst] (U i)
Tactic: have hU' : ∀ i ∈ t, IsOpen (U i) := fun i hi => hU.2 i hi
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
ι : Type u_3
x : ι
t : Finset ι
hx : x ∉ t
ih :
  ∀ {s : Set X} (hs : IsCompact s) (U : ι → Set X) (hU : ∀ i ∈ t, IsOpen[inst] (U i)) (hsC : s ⊆ ⋃ i ∈ t, U i),
    ∃ (K : ι → Set X), (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ t, K i
s : Set X
hs : IsCompact s
U : ι → Set X
hsC : s ⊆ U x ∪ ⋃ x ∈ t, U x
hU : IsOpen[inst] (U x) ∧ ∀ x ∈ t, IsOpen[inst] (U x)
hU' : ∀ i ∈ t, IsOpen[inst] (U i)
⊢ ∃ (K : ι → Set X), (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ insert x t, K i
have insert : ∀ (K₁ K₂ : Set X) (h1K₁ : IsCompact K₁) (h1K₂ : IsCompact K₂) (h2K₁ : K₁ ⊆ U x) (h2K₂ : K₂ ⊆ ⋃ i ∈ (↑t : Set ι), U i)
  (hK : s = K₁ ∪ K₂),
  ∃ (K : ι → Set X), (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ insert x t, K i
Tactic: rcases hs.binary_compact_cover hU.1 (isOpen_biUnion hU') hsC with
      ⟨K₁, K₂, h1K₁, h1K₂, h2K₁, h2K₂, hK⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
ι : Type u_3
x : ι
t : Finset ι
hx : x ∉ t
ih :
  ∀ {s : Set X} (hs : IsCompact s) (U : ι → Set X) (hU : ∀ i ∈ t, IsOpen[inst] (U i)) (hsC : s ⊆ ⋃ i ∈ t, U i),
    ∃ (K : ι → Set X), (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ t, K i
s : Set X
hs : IsCompact s
U : ι → Set X
hsC : s ⊆ U x ∪ ⋃ x ∈ t, U x
hU : IsOpen[inst] (U x) ∧ ∀ x ∈ t, IsOpen[inst] (U x)
hU' : ∀ i ∈ t, IsOpen[inst] (U i)
K₁ K₂ : Set X
h1K₁ : IsCompact K₁
h1K₂ : IsCompact K₂
h2K₁ : K₁ ⊆ U x
h2K₂ : K₂ ⊆ ⋃ i ∈ (↑t : Set ι), U i
hK : s = K₁ ∪ K₂
⊢ ∃ (K : ι → Set X), (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ insert x t, K i
have insert : ∀ (K : ι → Set X) (h1K : ∀ (i : ι), IsCompact (K i)) (h2K : ∀ (i : ι), K i ⊆ U i) (h3K : K₂ = ⋃ i ∈ t, K i),
  ∃ (K : ι → Set X), (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ insert x t, K i
Tactic: rcases ih h1K₂ U hU' h2K₂ with ⟨K, h1K, h2K, h3K⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
ι : Type u_3
x : ι
t : Finset ι
hx : x ∉ t
ih :
  ∀ {s : Set X} (hs : IsCompact s) (U : ι → Set X) (hU : ∀ i ∈ t, IsOpen[inst] (U i)) (hsC : s ⊆ ⋃ i ∈ t, U i),
    ∃ (K : ι → Set X), (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ t, K i
s : Set X
hs : IsCompact s
U : ι → Set X
hsC : s ⊆ U x ∪ ⋃ x ∈ t, U x
hU : IsOpen[inst] (U x) ∧ ∀ x ∈ t, IsOpen[inst] (U x)
hU' : ∀ i ∈ t, IsOpen[inst] (U i)
K₁ K₂ : Set X
h1K₁ : IsCompact K₁
h1K₂ : IsCompact K₂
h2K₁ : K₁ ⊆ U x
h2K₂ : K₂ ⊆ ⋃ i ∈ (↑t : Set ι), U i
hK : s = K₁ ∪ K₂
K : ι → Set X
h1K : ∀ (i : ι), IsCompact (K i)
h2K : ∀ (i : ι), K i ⊆ U i
h3K : K₂ = ⋃ i ∈ t, K i
i : ι
⊢ IsCompact (update (β := fun (a : ι) ↦ Set X) K x K₁ i)
have insert : ∀ (hx : i ∉ t) (hsC : s ⊆ U i ∪ ⋃ x ∈ t, U x) (hU : IsOpen[inst] (U i) ∧ ∀ x ∈ t, IsOpen[inst] (U x)) (h2K₁ : K₁ ⊆ U i),
  IsCompact (update (β := fun (a : ι) ↦ Set X) K i K₁ i)
Tactic: rcases eq_or_ne i x with rfl | hi
Cleared hypotheses: x, hx, hsC, hU, h2K₁
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
ι : Type u_3
x : ι
t : Finset ι
hx : x ∉ t
ih :
  ∀ {s : Set X} (hs : IsCompact s) (U : ι → Set X) (hU : ∀ i ∈ t, IsOpen[inst] (U i)) (hsC : s ⊆ ⋃ i ∈ t, U i),
    ∃ (K : ι → Set X), (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ t, K i
s : Set X
hs : IsCompact s
U : ι → Set X
hsC : s ⊆ U x ∪ ⋃ x ∈ t, U x
hU : IsOpen[inst] (U x) ∧ ∀ x ∈ t, IsOpen[inst] (U x)
hU' : ∀ i ∈ t, IsOpen[inst] (U i)
K₁ K₂ : Set X
h1K₁ : IsCompact K₁
h1K₂ : IsCompact K₂
h2K₁ : K₁ ⊆ U x
h2K₂ : K₂ ⊆ ⋃ i ∈ (↑t : Set ι), U i
hK : s = K₁ ∪ K₂
K : ι → Set X
h1K : ∀ (i : ι), IsCompact (K i)
h2K : ∀ (i : ι), K i ⊆ U i
h3K : K₂ = ⋃ i ∈ t, K i
i : ι
insert :
  ∀ (hx : i ∉ t) (hsC : s ⊆ U i ∪ ⋃ x ∈ t, U x) (hU : IsOpen[inst] (U i) ∧ ∀ x ∈ t, IsOpen[inst] (U x))
    (h2K₁ : K₁ ⊆ U i), IsCompact (update (β := fun (a : ι) ↦ Set X) K i K₁ i)
⊢ IsCompact (update (β := fun (a : ι) ↦ Set X) K x K₁ i)
have insert₁ : ∀ (hi : i ≠ x), IsCompact (update (β := fun (a : ι) ↦ Set X) K x K₁ i)
Tactic: rcases eq_or_ne i x with rfl | hi
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
ι : Type u_3
x : ι
t : Finset ι
hx : x ∉ t
ih :
  ∀ {s : Set X} (hs : IsCompact s) (U : ι → Set X) (hU : ∀ i ∈ t, IsOpen[inst] (U i)) (hsC : s ⊆ ⋃ i ∈ t, U i),
    ∃ (K : ι → Set X), (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ t, K i
s : Set X
hs : IsCompact s
U : ι → Set X
hsC : s ⊆ U x ∪ ⋃ x ∈ t, U x
hU : IsOpen[inst] (U x) ∧ ∀ x ∈ t, IsOpen[inst] (U x)
hU' : ∀ i ∈ t, IsOpen[inst] (U i)
K₁ K₂ : Set X
h1K₁ : IsCompact K₁
h1K₂ : IsCompact K₂
h2K₁ : K₁ ⊆ U x
h2K₂ : K₂ ⊆ ⋃ i ∈ (↑t : Set ι), U i
hK : s = K₁ ∪ K₂
K : ι → Set X
h1K : ∀ (i : ι), IsCompact (K i)
h2K : ∀ (i : ι), K i ⊆ U i
h3K : K₂ = ⋃ i ∈ t, K i
i : ι
⊢ update (β := fun (a : ι) ↦ Set X) K x K₁ i ⊆ U i
have insert : ∀ (hx : i ∉ t) (hsC : s ⊆ U i ∪ ⋃ x ∈ t, U x) (hU : IsOpen[inst] (U i) ∧ ∀ x ∈ t, IsOpen[inst] (U x)) (h2K₁ : K₁ ⊆ U i),
  update (β := fun (a : ι) ↦ Set X) K i K₁ i ⊆ U i
Tactic: rcases eq_or_ne i x with rfl | hi
Cleared hypotheses: x, hx, hsC, hU, h2K₁
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
ι : Type u_3
x : ι
t : Finset ι
hx : x ∉ t
ih :
  ∀ {s : Set X} (hs : IsCompact s) (U : ι → Set X) (hU : ∀ i ∈ t, IsOpen[inst] (U i)) (hsC : s ⊆ ⋃ i ∈ t, U i),
    ∃ (K : ι → Set X), (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ t, K i
s : Set X
hs : IsCompact s
U : ι → Set X
hsC : s ⊆ U x ∪ ⋃ x ∈ t, U x
hU : IsOpen[inst] (U x) ∧ ∀ x ∈ t, IsOpen[inst] (U x)
hU' : ∀ i ∈ t, IsOpen[inst] (U i)
K₁ K₂ : Set X
h1K₁ : IsCompact K₁
h1K₂ : IsCompact K₂
h2K₁ : K₁ ⊆ U x
h2K₂ : K₂ ⊆ ⋃ i ∈ (↑t : Set ι), U i
hK : s = K₁ ∪ K₂
K : ι → Set X
h1K : ∀ (i : ι), IsCompact (K i)
h2K : ∀ (i : ι), K i ⊆ U i
h3K : K₂ = ⋃ i ∈ t, K i
i : ι
insert :
  ∀ (hx : i ∉ t) (hsC : s ⊆ U i ∪ ⋃ x ∈ t, U x) (hU : IsOpen[inst] (U i) ∧ ∀ x ∈ t, IsOpen[inst] (U x))
    (h2K₁ : K₁ ⊆ U i), update (β := fun (a : ι) ↦ Set X) K i K₁ i ⊆ U i
⊢ update (β := fun (a : ι) ↦ Set X) K x K₁ i ⊆ U i
have insert₁ : ∀ (hi : i ≠ x), update (β := fun (a : ι) ↦ Set X) K x K₁ i ⊆ U i
Tactic: rcases eq_or_ne i x with rfl | hi
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
s : Set X
hs : IsCompact s
ι : Type u_3
t : Finset ι
U : ι → Set X
hU : ∀ i ∈ t, IsOpen[inst] (U i)
hsC : s ⊆ ⋃ i ∈ t, U i
⊢ ∃ (K : ι → Set X), (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ t, K i
have empty : ∀ {s : Set X} (hs : IsCompact s) (U : ι → Set X)
  (hU : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → IsOpen[inst] (U i))
  (hsC : s ⊆ ⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), U i),
  ∃ (K : ι → Set X),
    (∀ (i : ι), IsCompact (K i)) ∧
      (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), K i
Tactic: induction t using Finset.induction generalizing U s with
  | empty =>
    refine ⟨fun _ => ∅, fun _ => isCompact_empty, fun i => empty_subset _, ?_⟩
    simpa only [subset_empty_iff, Finset.notMem_empty, iUnion_false, iUnion_empty] using hsC
  | insert x t hx ih =>
    simp only [Finset.set_biUnion_insert] at hsC
    simp only [Finset.forall_mem_insert] at hU
    have hU' : ∀ i ∈ t, IsOpen (U i) := fun i hi => hU.2 i hi
    rcases hs.binary_compact_cover hU.1 (isOpen_biUnion hU') hsC with
      ⟨K₁, K₂, h1K₁, h1K₂, h2K₁, h2K₂, hK⟩
    rcases ih h1K₂ U hU' h2K₂ with ⟨K, h1K, h2K, h3K⟩
    refine ⟨update K x K₁, ?_, ?_, ?_⟩
    · intro i
      rcases eq_or_ne i x with rfl | hi
      · simp only [update_self, h1K₁]
      · simp only [update_of_ne hi, h1K]
    · intro i
      rcases eq_or_ne i x with rfl | hi
      · simp only [update_self, h2K₁]
      · simp only [update_of_ne hi, h2K]
    · simp only [Finset.set_biUnion_insert_update _ hx, hK, h3K]
Cleared hypotheses: s, hs, t, U, hU, hsC