awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Sets.Compacts (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
ι : Type u_4
s_1 : Finset ι
f : ι → Compacts α
a : ι
s : Finset ι
h_1 : a ∉ s
h : (↑(s.sup f) : Set α) = s.sup fun (i : ι) ↦ (↑(f i) : Set α)
⊢ (↑((Finset.cons a s h_1).sup f) : Set α) = (Finset.cons a s h_1).sup fun (i : ι) ↦ (↑(f i) : Set α)
have simp_rw : (↑(f a) : Set α) ∪ (↑(s.sup f) : Set α) = (↑(f a) : Set α) ∪ s.sup fun (i : ι) ↦ (↑(f i) : Set α)
Tactic: simp_rw [Finset.sup_cons, coe_sup, sup_eq_union]
-- Lean 4 proof step from Mathlib.Topology.Sets.Compacts (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : Nonempty α
⊢ Nontrivial.{u_1} (Compacts α)
have exists_pair_ne : ∃ (x : Compacts α) (y : Compacts α), x ≠ y
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Sets.Compacts (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : Nonempty α
⊢ ∃ (x : Compacts α) (y : Compacts α), x ≠ y
have exists_pair_ne : ∀ (x : α), ∃ (x : Compacts α) (y : Compacts α), x ≠ y
Tactic: obtain ⟨x⟩ := ‹Nonempty α›
-- Lean 4 proof step from Mathlib.Topology.Sets.Compacts (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ Subsingleton.{u_1 + 1} (Compacts α) ↔ IsEmpty α
have refine : ∀ (h : Subsingleton.{u_1 + 1} (Compacts α)), IsEmpty α
Tactic: refine ⟨fun h => ?_, fun _ => inferInstance⟩
-- Lean 4 proof step from Mathlib.Topology.Sets.Compacts (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
h : Subsingleton.{u_1 + 1} (Compacts α)
⊢ IsEmpty α
have contrapose! : ∀ (h : Nonempty α), Nontrivial.{u_1} (Compacts α)
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Sets.Compacts (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ Nontrivial.{u_1} (Compacts α) ↔ Nonempty α
have rw : ¬Subsingleton.{u_1 + 1} (Compacts α) ↔ Nonempty α
Tactic: rw [← not_subsingleton_iff_nontrivial, subsingleton_iff, not_isEmpty_iff]
-- Lean 4 proof step from Mathlib.Topology.Sets.Compacts (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
rw : ¬Subsingleton.{u_1 + 1} (Compacts α) ↔ Nonempty α
⊢ Nontrivial.{u_1} (Compacts α) ↔ Nonempty α
have rw₁ : ¬IsEmpty α ↔ Nonempty α
Tactic: rw [← not_subsingleton_iff_nontrivial, subsingleton_iff, not_isEmpty_iff]
-- Lean 4 proof step from Mathlib.Topology.Sets.Compacts (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
rw : ¬Subsingleton.{u_1 + 1} (Compacts α) ↔ Nonempty α
rw₁ : ¬IsEmpty α ↔ Nonempty α
⊢ Nontrivial.{u_1} (Compacts α) ↔ Nonempty α
have rw₂ : Nonempty α ↔ Nonempty α
Tactic: rw [← not_subsingleton_iff_nontrivial, subsingleton_iff, not_isEmpty_iff]
-- Lean 4 proof step from Mathlib.Topology.Sets.Compacts (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : Continuous f
⊢ Function.Injective (Compacts.map f hf) ↔ Function.Injective f
have refine : ∀ (h : Function.Injective (Compacts.map f hf)), Function.Injective (β := Compacts β) ((fun (x : β) ↦ {x}) ∘ f)
Tactic: refine ⟨fun h => .of_comp (f := ({·} : β → Compacts β)) ?_, map_injective hf⟩
-- Lean 4 proof step from Mathlib.Topology.Sets.Compacts (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : Continuous f
h : Function.Injective (Compacts.map f hf)
⊢ Function.Injective (β := Compacts β) ((fun (x : β) ↦ {x}) ∘ f)
have simp_rw : Function.Injective.{u_1 + 1, u_2 + 1} (β := Compacts β) fun (x : α) ↦ Compacts.map f hf {x}
Tactic: simp_rw [Function.comp_def, ← map_singleton hf]
-- Lean 4 proof step from Mathlib.Topology.Sets.Compacts (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
f : α ≃ₜ β
s : Compacts α
⊢ Compacts.map (⇑f.symm : (a : β) → α) ⋯ (Compacts.map (⇑f : (a : α) → β) ⋯ s) = s
have h : (↑(Compacts.map (⇑f.symm : (a : β) → α) sorry (Compacts.map (⇑f : (a : α) → β) sorry s)) : Set α) = (↑s : Set α)
Tactic: ext1
-- Lean 4 proof step from Mathlib.Topology.Sets.Compacts (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
f : α ≃ₜ β
s : Compacts β
⊢ Compacts.map (⇑f : (a : α) → β) ⋯ (Compacts.map (⇑f.symm : (a : β) → α) ⋯ s) = s
have h : (↑(Compacts.map (⇑f : (a : α) → β) sorry (Compacts.map (⇑f.symm : (a : β) → α) sorry s)) : Set β) = (↑s : Set β)
Tactic: ext1
-- Lean 4 proof step from Mathlib.Topology.Sets.Compacts (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
s t : NonemptyCompacts α
h :
  Eq.{u_1 + 1} (α := Set α) ((fun (s : NonemptyCompacts α) ↦ s.carrier) s)
    ((fun (s : NonemptyCompacts α) ↦ s.carrier) t)
⊢ s = t
have obtain : ∀ (carrier : Set α) (isCompact' : IsCompact carrier)
  (nonempty' : { carrier := carrier, isCompact' := isCompact' : Compacts α }.carrier.Nonempty)
  (h :
    Eq.{u_1 + 1} (α := Set α)
      ((fun (s : NonemptyCompacts α) ↦ s.carrier)
        { carrier := carrier, isCompact' := isCompact', nonempty' := nonempty' })
      ((fun (s : NonemptyCompacts α) ↦ s.carrier) t)),
  { carrier := carrier, isCompact' := isCompact', nonempty' := nonempty' : NonemptyCompacts α } = t
Tactic: obtain ⟨⟨_, _⟩, _⟩ := s
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Topology.Sets.Compacts (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
t : NonemptyCompacts α
carrier : Set α
isCompact' : IsCompact carrier
nonempty' : { carrier := carrier, isCompact' := isCompact' : Compacts α }.carrier.Nonempty
h :
  Eq.{u_1 + 1} (α := Set α)
    ((fun (s : NonemptyCompacts α) ↦ s.carrier)
      { carrier := carrier, isCompact' := isCompact', nonempty' := nonempty' })
    ((fun (s : NonemptyCompacts α) ↦ s.carrier) t)
⊢ { carrier := carrier, isCompact' := isCompact', nonempty' := nonempty' : NonemptyCompacts α } = t
have obtain : ∀ (carrier_1 : Set α) (isCompact'_1 : IsCompact carrier_1)
  (nonempty'_1 : { carrier := carrier_1, isCompact' := isCompact'_1 : Compacts α }.carrier.Nonempty)
  (h :
    Eq.{u_1 + 1} (α := Set α)
      ((fun (s : NonemptyCompacts α) ↦ s.carrier)
        { carrier := carrier, isCompact' := isCompact', nonempty' := nonempty' })
      ((fun (s : NonemptyCompacts α) ↦ s.carrier)
        { carrier := carrier_1, isCompact' := isCompact'_1, nonempty' := nonempty'_1 })),
  { carrier := carrier, isCompact' := isCompact', nonempty' := nonempty' : NonemptyCompacts α } =
    { carrier := carrier_1, isCompact' := isCompact'_1, nonempty' := nonempty'_1 }
Tactic: obtain ⟨⟨_, _⟩, _⟩ := t
Cleared hypotheses: t, h
-- Lean 4 proof step from Mathlib.Topology.Sets.Compacts (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ Eq (α := Set (Compacts α)) (range toCompacts) {⊥}ᶜ
have h : ∀ (K : Compacts α),
  Membership.mem (γ := Set (Compacts α)) (range toCompacts) K ↔ Membership.mem (γ := Set (Compacts α)) {⊥}ᶜ K
Tactic: ext K
-- Lean 4 proof step from Mathlib.Topology.Sets.Compacts (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
K : Compacts α
⊢ Membership.mem (γ := Set (Compacts α)) (range toCompacts) K ↔ Membership.mem (γ := Set (Compacts α)) {⊥}ᶜ K
have h : Membership.mem (γ := Set (Compacts α)) (range toCompacts) K ↔ (↑K : Set α).Nonempty
Tactic: rw [mem_compl_singleton_iff, ← Compacts.coe_nonempty]
-- Lean 4 proof step from Mathlib.Topology.Sets.Compacts (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
K : Compacts α
⊢ Membership.mem (γ := Set (Compacts α)) (range toCompacts) K ↔ (↑K : Set α).Nonempty
have h : Membership.mem (γ := Set (Compacts α)) (range toCompacts) K → (↑K : Set α).Nonempty
Tactic: refine ⟨?_, fun h => ⟨⟨K, h⟩, rfl⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Sets.Compacts (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ Nonempty.{u_1 + 1} (NonemptyCompacts α) ↔ Nonempty α
have simp_rw : ¬IsEmpty.{u_1 + 1} (NonemptyCompacts α) ↔ ¬IsEmpty α
Tactic: simp_rw [← not_isEmpty_iff, isEmpty_iff]
-- Lean 4 proof step from Mathlib.Topology.Sets.Compacts (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : Subsingleton α
⊢ Subsingleton.{u_1 + 1} (NonemptyCompacts α)
have refine : ∀ (K L : NonemptyCompacts α), (↑K : Set α) = (↑L : Set α)
Tactic: refine ⟨fun K L => NonemptyCompacts.ext ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Sets.Compacts (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : Subsingleton α
K L : NonemptyCompacts α
⊢ (↑K : Set α) = (↑L : Set α)
have rw : univ = (↑L : Set α)
Tactic: rw [Subsingleton.eq_univ_of_nonempty K.nonempty, Subsingleton.eq_univ_of_nonempty L.nonempty]
-- Lean 4 proof step from Mathlib.Topology.Sets.Compacts (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : Subsingleton α
K L : NonemptyCompacts α
rw : univ = (↑L : Set α)
⊢ (↑K : Set α) = (↑L : Set α)
have rw₁ : Eq.{u_1 + 1} (α := Set α) univ univ
Tactic: rw [Subsingleton.eq_univ_of_nonempty K.nonempty, Subsingleton.eq_univ_of_nonempty L.nonempty]
-- Lean 4 proof step from Mathlib.Topology.Sets.Compacts (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ Nontrivial.{u_1} (NonemptyCompacts α) ↔ Nontrivial α
have simp_rw : ¬Subsingleton.{u_1 + 1} (NonemptyCompacts α) ↔ ¬Subsingleton α
Tactic: simp_rw [← not_subsingleton_iff_nontrivial, subsingleton_iff]
-- Lean 4 proof step from Mathlib.Topology.Sets.Compacts (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
K : NonemptyCompacts α
⊢ NonemptyCompacts.map id ⋯ K = K
have h : ∀ (x : α), x ∈ (↑(NonemptyCompacts.map id sorry K) : Set α) ↔ x ∈ (↑K : Set α)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Sets.Compacts (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
f : β → γ
g : α → β
hf : Continuous f
hg : Continuous g
K : NonemptyCompacts α
⊢ NonemptyCompacts.map (f ∘ g) ⋯ K = NonemptyCompacts.map f hf (NonemptyCompacts.map g hg K)
have h : ∀ (x : γ),
  x ∈ (↑(NonemptyCompacts.map (f ∘ g) sorry K) : Set γ) ↔
    x ∈ (↑(NonemptyCompacts.map f hf (NonemptyCompacts.map g hg K)) : Set γ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Sets.Compacts (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : Continuous f
x : α
⊢ NonemptyCompacts.map f hf {x} = {f x}
have h : ∀ (x_1 : β), x_1 ∈ (↑(NonemptyCompacts.map f hf {x}) : Set β) ↔ x_1 ∈ (↑{f x} : Set β)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Sets.Compacts (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
s t : PositiveCompacts α
h :
  Eq.{u_1 + 1} (α := Set α) ((fun (s : PositiveCompacts α) ↦ s.carrier) s)
    ((fun (s : PositiveCompacts α) ↦ s.carrier) t)
⊢ s = t
have obtain : ∀ (carrier : Set α) (isCompact' : IsCompact carrier)
  (interior_nonempty' : (interior { carrier := carrier, isCompact' := isCompact' : Compacts α }.carrier).Nonempty)
  (h :
    Eq.{u_1 + 1} (α := Set α)
      ((fun (s : PositiveCompacts α) ↦ s.carrier)
        { carrier := carrier, isCompact' := isCompact', interior_nonempty' := interior_nonempty' })
      ((fun (s : PositiveCompacts α) ↦ s.carrier) t)),
  { carrier := carrier, isCompact' := isCompact', interior_nonempty' := interior_nonempty' : PositiveCompacts α } = t
Tactic: obtain ⟨⟨_, _⟩, _⟩ := s
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Topology.Sets.Compacts (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
t : PositiveCompacts α
carrier : Set α
isCompact' : IsCompact carrier
interior_nonempty' : (interior { carrier := carrier, isCompact' := isCompact' : Compacts α }.carrier).Nonempty
h :
  Eq.{u_1 + 1} (α := Set α)
    ((fun (s : PositiveCompacts α) ↦ s.carrier)
      { carrier := carrier, isCompact' := isCompact', interior_nonempty' := interior_nonempty' })
    ((fun (s : PositiveCompacts α) ↦ s.carrier) t)
⊢ { carrier := carrier, isCompact' := isCompact', interior_nonempty' := interior_nonempty' : PositiveCompacts α } = t
have obtain : ∀ (carrier_1 : Set α) (isCompact'_1 : IsCompact carrier_1)
  (interior_nonempty'_1 : (interior { carrier := carrier_1, isCompact' := isCompact'_1 : Compacts α }.carrier).Nonempty)
  (h :
    Eq.{u_1 + 1} (α := Set α)
      ((fun (s : PositiveCompacts α) ↦ s.carrier)
        { carrier := carrier, isCompact' := isCompact', interior_nonempty' := interior_nonempty' })
      ((fun (s : PositiveCompacts α) ↦ s.carrier)
        { carrier := carrier_1, isCompact' := isCompact'_1, interior_nonempty' := interior_nonempty'_1 })),
  { carrier := carrier, isCompact' := isCompact', interior_nonempty' := interior_nonempty' : PositiveCompacts α } =
    { carrier := carrier_1, isCompact' := isCompact'_1, interior_nonempty' := interior_nonempty'_1 }
Tactic: obtain ⟨⟨_, _⟩, _⟩ := t
Cleared hypotheses: t, h
-- Lean 4 proof step from Mathlib.Topology.Sets.Compacts (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : WeaklyLocallyCompactSpace α
inst_4 : Nonempty α
⊢ Nonempty.{u_1 + 1} (PositiveCompacts α)
have inhabit : ∀ (inhabited_h : Inhabited α), Nonempty.{u_1 + 1} (PositiveCompacts α)
Tactic: inhabit α
-- Lean 4 proof step from Mathlib.Topology.Sets.Compacts (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : WeaklyLocallyCompactSpace α
inst_4 : Nonempty α
inhabited_h : Inhabited α
⊢ Nonempty.{u_1 + 1} (PositiveCompacts α)
have rcases : ∀ (K : Set α) (hKc : IsCompact K) (hK : Membership.mem (γ := Filter α) (nhds default) K),
  Nonempty.{u_1 + 1} (PositiveCompacts α)
Tactic: rcases exists_compact_mem_nhds (default : α) with ⟨K, hKc, hK⟩
-- Lean 4 proof step from Mathlib.Topology.Sets.Compacts (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
K : PositiveCompacts α
L : PositiveCompacts β
⊢ (interior (K.toCompacts ×ˢ L.toCompacts).carrier).Nonempty
have simp : (interior (↑K.toCompacts : Set α) ×ˢ interior (↑L.toCompacts : Set β)).Nonempty
Tactic: simp only [Compacts.carrier_eq_coe, Compacts.coe_prod, interior_prod_eq]
-- Lean 4 proof step from Mathlib.Topology.Sets.Compacts (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
s t : CompactOpens α
h : Eq.{u_1 + 1} (α := Set α) ((fun (s : CompactOpens α) ↦ s.carrier) s) ((fun (s : CompactOpens α) ↦ s.carrier) t)
⊢ s = t
have obtain : ∀ (carrier : Set α) (isCompact' : IsCompact carrier)
  (isOpen' : IsOpen { carrier := carrier, isCompact' := isCompact' : Compacts α }.carrier)
  (h :
    Eq.{u_1 + 1} (α := Set α)
      ((fun (s : CompactOpens α) ↦ s.carrier) { carrier := carrier, isCompact' := isCompact', isOpen' := isOpen' })
      ((fun (s : CompactOpens α) ↦ s.carrier) t)),
  { carrier := carrier, isCompact' := isCompact', isOpen' := isOpen' : CompactOpens α } = t
Tactic: obtain ⟨⟨_, _⟩, _⟩ := s
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Topology.Sets.Compacts (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
t : CompactOpens α
carrier : Set α
isCompact' : IsCompact carrier
isOpen' : IsOpen { carrier := carrier, isCompact' := isCompact' : Compacts α }.carrier
h :
  Eq.{u_1 + 1} (α := Set α)
    ((fun (s : CompactOpens α) ↦ s.carrier) { carrier := carrier, isCompact' := isCompact', isOpen' := isOpen' })
    ((fun (s : CompactOpens α) ↦ s.carrier) t)
⊢ { carrier := carrier, isCompact' := isCompact', isOpen' := isOpen' : CompactOpens α } = t
have obtain : ∀ (carrier_1 : Set α) (isCompact'_1 : IsCompact carrier_1)
  (isOpen'_1 : IsOpen { carrier := carrier_1, isCompact' := isCompact'_1 : Compacts α }.carrier)
  (h :
    Eq.{u_1 + 1} (α := Set α)
      ((fun (s : CompactOpens α) ↦ s.carrier) { carrier := carrier, isCompact' := isCompact', isOpen' := isOpen' })
      ((fun (s : CompactOpens α) ↦ s.carrier)
        { carrier := carrier_1, isCompact' := isCompact'_1, isOpen' := isOpen'_1 })),
  { carrier := carrier, isCompact' := isCompact', isOpen' := isOpen' : CompactOpens α } =
    { carrier := carrier_1, isCompact' := isCompact'_1, isOpen' := isOpen'_1 }
Tactic: obtain ⟨⟨_, _⟩, _⟩ := t
Cleared hypotheses: t, h
-- Lean 4 proof step from Mathlib.Topology.Sets.Compacts (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
ι : Type u_4
f : ι → CompactOpens α
s : Finset ι
⊢ (↑(s.sup f) : Set α) = ⋃ i ∈ s, (↑(f i) : Set α)
have empty : (↑(Finset.sup ∅ f) : Set α) = ⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), (↑(f i) : Set α)
Tactic: induction s using Finset.induction_on
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Topology.Sets.Compacts (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
ι : Type u_4
f : ι → CompactOpens α
s : Finset ι
empty : (↑(Finset.sup ∅ f) : Set α) = ⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), (↑(f i) : Set α)
⊢ (↑(s.sup f) : Set α) = ⋃ i ∈ s, (↑(f i) : Set α)
have insert : ∀ (a : ι) (s : Finset ι),
  a ∉ s →
    (↑(s.sup f) : Set α) = ⋃ i ∈ s, (↑(f i) : Set α) →
      (↑((insert a s).sup f) : Set α) = ⋃ i ∈ insert a s, (↑(f i) : Set α)
Tactic: induction s using Finset.induction_on
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Topology.Sets.Compacts (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
ι : Type u_4
f : ι → CompactOpens α
s : Finset ι
⊢ (↑(s.sup f) : Set α) = ⋃ i ∈ s, (↑(f i) : Set α)
have empty : (↑(Finset.sup ∅ f) : Set α) = ⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), (↑(f i) : Set α)
Tactic: classical
  induction s using Finset.induction_on <;> simp [*]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Topology.Sets.Compacts (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
ι : Type u_4
f : ι → CompactOpens α
s : Finset ι
empty : (↑(Finset.sup ∅ f) : Set α) = ⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), (↑(f i) : Set α)
⊢ (↑(s.sup f) : Set α) = ⋃ i ∈ s, (↑(f i) : Set α)
have insert : ∀ (a : ι) (s : Finset ι),
  a ∉ s →
    (↑(s.sup f) : Set α) = ⋃ i ∈ s, (↑(f i) : Set α) →
      (↑((insert a s).sup f) : Set α) = ⋃ i ∈ insert a s, (↑(f i) : Set α)
Tactic: classical
  induction s using Finset.induction_on <;> simp [*]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Topology.Sets.OpenCover (goal)
Goal:
ι : Type u_1
X : Type u_3
inst : TopologicalSpace X
S : Set (Opens X)
hS : IsBasis S
U : ι → Opens X
hU : IsOpenCover U
⊢ IsOpenCover (X := X) fun (V : { x : Prod.{u_3, u_1} (Opens X) ι // x.1 ∈ S ∧ x.1 ≤ U x.2 }) ↦ (↑V : Opens X × ι).1
have refine : ∀ (x : X),
  Membership.mem (γ := Opens X) ⊤ x →
    Membership.mem (γ := Opens X)
      (⨆ (V : { x : Prod.{u_3, u_1} (Opens X) ι // x.1 ∈ S ∧ x.1 ≤ U x.2 }), (↑V : Opens X × ι).1) x
Tactic: refine top_le_iff.mp fun x _ ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Sets.OpenCover (goal)
Goal:
ι : Type u_1
X : Type u_3
inst : TopologicalSpace X
S : Set (Opens X)
hS : IsBasis S
U : ι → Opens X
hU : IsOpenCover U
x : X
h : Membership.mem (γ := Opens X) ⊤ x
⊢ Membership.mem (γ := Opens X)
    (⨆ (V : { x : Prod.{u_3, u_1} (Opens X) ι // x.1 ∈ S ∧ x.1 ≤ U x.2 }), (↑V : Opens X × ι).1) x
have obtain : ∀ (i : ι) (hxi : x ∈ U i),
  Membership.mem (γ := Opens X)
    (⨆ (V : { x : Prod.{u_3, u_1} (Opens X) ι // x.1 ∈ S ∧ x.1 ≤ U x.2 }), (↑V : Opens X × ι).1) x
Tactic: obtain ⟨i, hxi⟩ := hU.exists_mem x
-- Lean 4 proof step from Mathlib.Topology.Sets.OpenCover (goal)
Goal:
ι : Type u_1
X : Type u_3
inst : TopologicalSpace X
S : Set (Opens X)
hS : IsBasis S
U : ι → Opens X
hU : IsOpenCover U
x : X
h : Membership.mem (γ := Opens X) ⊤ x
i : ι
hxi : x ∈ U i
⊢ Membership.mem (γ := Opens X)
    (⨆ (V : { x : Prod.{u_3, u_1} (Opens X) ι // x.1 ∈ S ∧ x.1 ≤ U x.2 }), (↑V : Opens X × ι).1) x
have obtain : ∀ (V : Opens X) (hV : V ∈ S) (hxV : x ∈ (↑V : Set X)) (hVU : (↑V : Set X) ⊆ (↑(U i) : Set X)),
  Membership.mem (γ := Opens X)
    (⨆ (V : { x : Prod.{u_3, u_1} (Opens X) ι // x.1 ∈ S ∧ x.1 ≤ U x.2 }), (↑V : Opens X × ι).1) x
Tactic: obtain ⟨_, ⟨V, hV, rfl⟩, hxV, hVU⟩ := hS.exists_subset_of_mem_open hxi (U i).2
-- Lean 4 proof step from Mathlib.Topology.Sets.OpenCover (goal)
Goal:
ι : Type u_1
X : Type u_3
inst : TopologicalSpace X
S : Set (Opens X)
hS : IsBasis S
U : ι → Opens X
hU : IsOpenCover U
x : X
h : Membership.mem (γ := Opens X) ⊤ x
i : ι
hxi : x ∈ U i
V : Opens X
hV : V ∈ S
hxV : x ∈ (↑V : Set X)
hVU : (↑V : Set X) ⊆ (↑(U i) : Set X)
⊢ Membership.mem (γ := Opens X)
    (⨆ (V : { x : Prod.{u_3, u_1} (Opens X) ι // x.1 ∈ S ∧ x.1 ≤ U x.2 }), (↑V : Opens X × ι).1) x
have simp : ∃ (i : { x : Prod.{u_3, u_1} (Opens X) ι // x.1 ∈ S ∧ x.1 ≤ U x.2 }),
  Membership.mem (γ := Opens X) (↑i : Opens X × ι).1 x
Tactic: simp only [Opens.iSup_mk, Opens.carrier_eq_coe, Opens.mem_mk, Set.mem_iUnion, SetLike.mem_coe]
-- Lean 4 proof step from Mathlib.Topology.Sets.OpenCover (goal)
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
U : ι → Opens X
hn : Pairwise ((fun (x1 x2 : Opens X) ↦ ¬Disjoint x1 x2) on U)
h : ∀ (i : ι), IsPreirreducible (↑(U i) : Set X)
s : Set X
hs : IsOpen[inst] s
hsU : s ⊆ ⋃ (i : ι), (↑(U i) : Set X)
⊢ IsPreirreducible s
have inl : ∀ (he : s = ∅), IsPreirreducible s
Tactic: rcases s.eq_empty_or_nonempty with he | hne
-- Lean 4 proof step from Mathlib.Topology.Sets.OpenCover (goal)
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
U : ι → Opens X
hn : Pairwise ((fun (x1 x2 : Opens X) ↦ ¬Disjoint x1 x2) on U)
h : ∀ (i : ι), IsPreirreducible (↑(U i) : Set X)
s : Set X
hs : IsOpen[inst] s
hsU : s ⊆ ⋃ (i : ι), (↑(U i) : Set X)
inl : ∀ (he : s = ∅), IsPreirreducible s
⊢ IsPreirreducible s
have inr : ∀ (hne : s.Nonempty), IsPreirreducible s
Tactic: rcases s.eq_empty_or_nonempty with he | hne
-- Lean 4 proof step from Mathlib.Topology.Sets.OpenCover (goal)
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
U : ι → Opens X
hn : Pairwise ((fun (x1 x2 : Opens X) ↦ ¬Disjoint x1 x2) on U)
h : ∀ (i : ι), IsPreirreducible (↑(U i) : Set X)
s : Set X
hs : IsOpen[inst] s
hsU : s ⊆ ⋃ (i : ι), (↑(U i) : Set X)
he : s = ∅
⊢ IsPreirreducible s
have inl : IsPreirreducible.{u_1} (X := X) ∅
Tactic: rw [he]
-- Lean 4 proof step from Mathlib.Topology.Sets.OpenCover (goal)
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
U : ι → Opens X
hn : Pairwise ((fun (x1 x2 : Opens X) ↦ ¬Disjoint x1 x2) on U)
h : ∀ (i : ι), IsPreirreducible (↑(U i) : Set X)
s : Set X
hs : IsOpen[inst] s
hsU : s ⊆ ⋃ (i : ι), (↑(U i) : Set X)
hne : s.Nonempty
⊢ IsPreirreducible s
have inr : ∀ (x : X) (hx : x ∈ s), IsPreirreducible s
Tactic: choose x hx using hne
Cleared hypotheses: hne
-- Lean 4 proof step from Mathlib.Topology.Sets.OpenCover (goal)
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
U : ι → Opens X
hn : Pairwise ((fun (x1 x2 : Opens X) ↦ ¬Disjoint x1 x2) on U)
h : ∀ (i : ι), IsPreirreducible (↑(U i) : Set X)
s : Set X
hs : IsOpen[inst] s
hsU : s ⊆ ⋃ (i : ι), (↑(U i) : Set X)
x : X
hx : x ∈ s
⊢ IsPreirreducible s
have inr : ∀ (i : ι) (hi : x ∈ (↑(U i) : Set X)), IsPreirreducible s
Tactic: choose i hi using mem_iUnion.mp <| hsU hx
-- Lean 4 proof step from Mathlib.Topology.Sets.OpenCover (goal)
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
U : ι → Opens X
hn : Pairwise ((fun (x1 x2 : Opens X) ↦ ¬Disjoint x1 x2) on U)
h : ∀ (i : ι), IsPreirreducible (↑(U i) : Set X)
s : Set X
hs : IsOpen[inst] s
hsU : s ⊆ ⋃ (i : ι), (↑(U i) : Set X)
x : X
hx : x ∈ s
i : ι
hi : x ∈ (↑(U i) : Set X)
⊢ IsPreirreducible s
have inr : ∀ (u : Set X) (hu : u ∈ irreducibleComponents X) (hUu : (U i).carrier ⊆ u), IsPreirreducible s
Tactic: rcases exists_mem_irreducibleComponents_subset_of_isIrreducible (U i).carrier ⟨⟨x, hi⟩, h i⟩
      with ⟨u, hu, hUu⟩