awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (goal)
Goal:
X Y : Compactum
f : X ⟶ Y
xs : Ultrafilter X.A
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : Compactum.{u_1}) ↦ x1 ⟶ x2) (CC := Monad.Algebra.A) f : (a : X.A) → Y.A)
      (X.str xs) =
    Y.str
      (Ultrafilter.map
        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : Compactum.{u_1}) ↦ x1 ⟶ x2) (CC := Monad.Algebra.A) f) :
          (a : X.A) → Y.A)
        xs)
have change : (ConcreteCategory.hom (FC := TypeCat.Fun) (X.a ≫ f.f) :
      (a : (fun (X : Type u_1) ↦ X) (β.obj X.A)) → (fun (X : Type u_1) ↦ X) Y.A)
    xs =
  Y.str
    (Ultrafilter.map
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : Compactum.{u_1}) ↦ x1 ⟶ x2) (CC := Monad.Algebra.A) f) :
        (a : X.A) → Y.A)
      xs)
Tactic: change (X.a ≫ f.f) _ = _
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (goal)
Goal:
X Y : Compactum
f : X ⟶ Y
xs : Ultrafilter X.A
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (X.a ≫ f.f) :
        (a : (fun (X : Type u_1) ↦ X) (β.obj X.A)) → (fun (X : Type u_1) ↦ X) Y.A)
      xs =
    Y.str
      (Ultrafilter.map
        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : Compactum.{u_1}) ↦ x1 ⟶ x2) (CC := Monad.Algebra.A) f) :
          (a : X.A) → Y.A)
        xs)
have rw : (ConcreteCategory.hom (FC := TypeCat.Fun) (β.map f.f ≫ Y.a) :
      (a : (fun (X : Type u_1) ↦ X) (β.obj X.A)) → (fun (X : Type u_1) ↦ X) Y.A)
    xs =
  Y.str
    (Ultrafilter.map
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : Compactum.{u_1}) ↦ x1 ⟶ x2) (CC := Monad.Algebra.A) f) :
        (a : X.A) → Y.A)
      xs)
Tactic: rw [← f.h]
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (goal)
Goal:
X : Compactum
uux : Ultrafilter (Ultrafilter X.A)
⊢ X.str (X.join uux) = X.str (Ultrafilter.map X.str uux)
have change : (ConcreteCategory.hom (FC := TypeCat.Fun) (β.μ.app X.A ≫ X.a) :
      (a : (fun (X : Type u_1) ↦ X) ((β.toFunctor ⋙ β.toFunctor).obj X.A)) → (fun (X : Type u_1) ↦ X) X.A)
    uux =
  X.str (Ultrafilter.map X.str uux)
Tactic: change ((β).μ.app _ ≫ X.a) _ = _
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (goal)
Goal:
X : Compactum
uux : Ultrafilter (Ultrafilter X.A)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (β.μ.app X.A ≫ X.a) :
        (a : (fun (X : Type u_1) ↦ X) ((β.toFunctor ⋙ β.toFunctor).obj X.A)) → (fun (X : Type u_1) ↦ X) X.A)
      uux =
    X.str (Ultrafilter.map X.str uux)
have rw : (ConcreteCategory.hom (FC := TypeCat.Fun) (β.map X.a ≫ X.a) :
      (a : (fun (X : Type u_1) ↦ X) ((β.toFunctor ⋙ β.toFunctor).obj X.A)) → (fun (X : Type u_1) ↦ X) X.A)
    uux =
  X.str (Ultrafilter.map X.str uux)
Tactic: rw [Monad.Algebra.assoc]
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (goal)
Goal:
X : Compactum
S : Set X.A
⊢ IsClosed S ↔ ∀ (F : Ultrafilter X.A), S ∈ F → X.str F ∈ S
have rw : IsOpen Sᶜ ↔ ∀ (F : Ultrafilter X.A), S ∈ F → X.str F ∈ S
Tactic: rw [← isOpen_compl_iff]
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (goal)
Goal:
X : Compactum
S : Set X.A
⊢ IsOpen Sᶜ ↔ ∀ (F : Ultrafilter X.A), S ∈ F → X.str F ∈ S
have mp : IsOpen Sᶜ → ∀ (F : Ultrafilter X.A), S ∈ F → X.str F ∈ S
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (goal)
Goal:
X : Compactum
S : Set X.A
mp : IsOpen Sᶜ → ∀ (F : Ultrafilter X.A), S ∈ F → X.str F ∈ S
⊢ IsOpen Sᶜ ↔ ∀ (F : Ultrafilter X.A), S ∈ F → X.str F ∈ S
have mpr : (∀ (F : Ultrafilter X.A), S ∈ F → X.str F ∈ S) → IsOpen Sᶜ
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (goal)
Goal:
X : Compactum
S : Set X.A
cond : IsOpen Sᶜ
F : Ultrafilter X.A
h : S ∈ F
⊢ X.str F ∈ S
have mp : ∀ (c : X.str F ∉ S), False
Tactic: by_contra c
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (hypothesis)
Goal:
X : Compactum
S : Set X.A
cond : IsOpen Sᶜ
F : Ultrafilter X.A
h : S ∈ F
c : X.str F ∉ S
⊢ False
have cond₁ : Sᶜ ∈ F
Tactic: specialize cond F c
Cleared hypotheses: cond
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (hypothesis)
Goal:
X : Compactum
S : Set X.A
F : Ultrafilter X.A
h : S ∈ F
c : X.str F ∉ S
cond : Sᶜ ∈ F
⊢ False
have cond₁ : S ∉ F
Tactic: rw [compl_mem_iff_notMem] at cond
Cleared hypotheses: cond
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (hypothesis)
Goal:
X : Compactum
S : Set X.A
h1 : ∀ (F : Ultrafilter X.A), S ∈ F → X.str F ∈ S
F : Ultrafilter X.A
h2 : X.str F ∈ Sᶜ
⊢ Sᶜ ∈ F
have h1₁ : S ∈ F → X.str F ∈ S
Tactic: specialize h1 F
Cleared hypotheses: h1
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (goal)
Goal:
X : Compactum
S : Set X.A
F : Ultrafilter X.A
h2 : X.str F ∈ Sᶜ
h1 : S ∈ F → X.str F ∈ S
⊢ Sᶜ ∈ F
have mpr : ∀ (h : S ∈ F), Sᶜ ∈ F
Tactic: rcases F.mem_or_compl_mem S with h | h
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (goal)
Goal:
X : Compactum
S : Set X.A
F : Ultrafilter X.A
h2 : X.str F ∈ Sᶜ
h1 : S ∈ F → X.str F ∈ S
mpr : ∀ (h : S ∈ F), Sᶜ ∈ F
⊢ Sᶜ ∈ F
have mpr₁ : ∀ (h : Sᶜ ∈ F), Sᶜ ∈ F
Tactic: rcases F.mem_or_compl_mem S with h | h
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (goal)
Goal:
X : Compactum
⊢ CompactSpace.{u_1} X.A
have isCompact_univ : IsCompact.{u_1} (X := X.A) Set.univ
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (goal)
Goal:
X : Compactum
⊢ IsCompact.{u_1} (X := X.A) Set.univ
have isCompact_univ : ∀ (f : Ultrafilter X.A),
  (↑f : Filter X.A) ≤ 𝓟 Set.univ → ∃ (x : X.A), Membership.mem (γ := Set X.A) Set.univ x ∧ (↑f : Filter X.A) ≤ 𝓝 x
Tactic: rw [isCompact_iff_ultrafilter_le_nhds]
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (goal)
Goal:
X : Compactum
F : Ultrafilter X.A
h : (↑F : Filter X.A) ≤ 𝓟 Set.univ
⊢ ∃ (x : X.A), Membership.mem (γ := Set X.A) Set.univ x ∧ (↑F : Filter X.A) ≤ 𝓝 x
have isCompact_univ : (↑F : Filter X.A) ≤ 𝓝 (X.str F)
Tactic: refine ⟨X.str F, by tauto, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (goal)
Goal:
X : Compactum
F : Ultrafilter X.A
h : (↑F : Filter X.A) ≤ 𝓟 Set.univ
⊢ (↑F : Filter X.A) ≤ 𝓝 (X.str F)
have isCompact_univ : ∀ (s : Set X.A), X.str F ∈ s → IsOpen s → s ∈ (↑F : Filter X.A)
Tactic: rw [le_nhds_iff]
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (goal)
Goal:
X : Compactum
A B : Set X.A
⊢ basic (A ∩ B) = basic A ∩ basic B
have h : ∀ (G : Ultrafilter X.A), G ∈ basic (A ∩ B) ↔ G ∈ basic A ∩ basic B
Tactic: ext G
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (goal)
Goal:
X : Compactum
A B : Set X.A
G : Ultrafilter X.A
⊢ G ∈ basic (A ∩ B) ↔ G ∈ basic A ∩ basic B
have h : G ∈ basic (A ∩ B) → G ∈ basic A ∩ basic B
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (goal)
Goal:
X : Compactum
A B : Set X.A
G : Ultrafilter X.A
h : G ∈ basic (A ∩ B) → G ∈ basic A ∩ basic B
⊢ G ∈ basic (A ∩ B) ↔ G ∈ basic A ∩ basic B
have h₁ : G ∈ basic A ∩ basic B → G ∈ basic (A ∩ B)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (goal)
Goal:
X : Compactum
A B : Set X.A
G : Ultrafilter X.A
hG : G ∈ basic (A ∩ B)
⊢ G ∈ basic A ∩ basic B
have h : G ∈ basic A
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (goal)
Goal:
X : Compactum
A B : Set X.A
G : Ultrafilter X.A
hG : G ∈ basic (A ∩ B)
h : G ∈ basic A
⊢ G ∈ basic A ∩ basic B
have h₁ : G ∈ basic B
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (goal)
Goal:
X : Compactum
A B : Set X.A
G : Ultrafilter X.A
hG : G ∈ basic (A ∩ B)
⊢ G ∈ basic A
have h : ∀ a ∈ A ∩ B, a ∈ A
Tactic: filter_upwards [hG] with _
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (goal)
Goal:
X : Compactum
A B : Set X.A
G : Ultrafilter X.A
hG : G ∈ basic (A ∩ B)
⊢ G ∈ basic B
have h : ∀ a ∈ A ∩ B, a ∈ B
Tactic: filter_upwards [hG] with _
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (goal)
Goal:
X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ basic (cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun (x : fsu) ↦ (↑x : Set (Set (Ultrafilter X.A)))
C0 : ssu := {Z : Set (Ultrafilter X.A) | ∃ B ∈ F, X.str ⁻¹' B = Z}
AA : Set (Ultrafilter X.A) := {G : Ultrafilter X.A | A ∈ G}
C1 : ssu := insert AA C0
C2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure C1
Q : Set X.A
hQ : Q ∈ F
R : Set X.A
hR : R ∈ F
⊢ X.str ⁻¹' Q ∩ X.str ⁻¹' R ∈ C0
have h : Q ∩ R ∈ F ∧ X.str ⁻¹' (Q ∩ R) = X.str ⁻¹' Q ∩ X.str ⁻¹' R
Tactic: use Q ∩ R
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (goal)
Goal:
X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ basic (cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun (x : fsu) ↦ (↑x : Set (Set (Ultrafilter X.A)))
C0 : ssu := {Z : Set (Ultrafilter X.A) | ∃ B ∈ F, X.str ⁻¹' B = Z}
AA : Set (Ultrafilter X.A) := {G : Ultrafilter X.A | A ∈ G}
C1 : ssu := insert AA C0
C2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure C1
Q : Set X.A
hQ : Q ∈ F
R : Set X.A
hR : R ∈ F
⊢ Q ∩ R ∈ F ∧ X.str ⁻¹' (Q ∩ R) = X.str ⁻¹' Q ∩ X.str ⁻¹' R
have h : Q ∩ R ∈ F
Tactic: simp only [and_true, Set.preimage_inter]
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (hypothesis)
Goal:
X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ basic (cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun (x : fsu) ↦ (↑x : Set (Set (Ultrafilter X.A)))
C0 : ssu := {Z : Set (Ultrafilter X.A) | ∃ B ∈ F, X.str ⁻¹' B = Z}
AA : Set (Ultrafilter X.A) := {G : Ultrafilter X.A | A ∈ G}
C1 : ssu := insert AA C0
C2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure C1
⊢ X.str F ∈ cl A
have claim1 : ∀ B ∈ C0, ∀ C ∈ C0, B ∩ C ∈ C0
Tactic: have claim1 : ∀ (B) (_ : B ∈ C0) (C) (_ : C ∈ C0), B ∩ C ∈ C0 := by
    rintro B ⟨Q, hQ, rfl⟩ C ⟨R, hR, rfl⟩
    use Q ∩ R
    simp only [and_true, Set.preimage_inter]
    exact inter_sets _ hQ hR
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (goal)
Goal:
X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ basic (cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun (x : fsu) ↦ (↑x : Set (Set (Ultrafilter X.A)))
C0 : ssu := {Z : Set (Ultrafilter X.A) | ∃ B ∈ F, X.str ⁻¹' B = Z}
AA : Set (Ultrafilter X.A) := {G : Ultrafilter X.A | A ∈ G}
C1 : ssu := insert AA C0
C2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure C1
claim1 : ∀ B ∈ C0, ∀ C ∈ C0, B ∩ C ∈ C0
Q : Set X.A
hQ : Q ∈ F
⊢ (X.str ⁻¹' Q).Nonempty
have obtain : ∀ q ∈ Q, (X.str ⁻¹' Q).Nonempty
Tactic: obtain ⟨q⟩ := Filter.nonempty_of_mem hQ
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (goal)
Goal:
X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ basic (cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun (x : fsu) ↦ (↑x : Set (Set (Ultrafilter X.A)))
C0 : ssu := {Z : Set (Ultrafilter X.A) | ∃ B ∈ F, X.str ⁻¹' B = Z}
AA : Set (Ultrafilter X.A) := {G : Ultrafilter X.A | A ∈ G}
C1 : ssu := insert AA C0
C2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure C1
claim1 : ∀ B ∈ C0, ∀ C ∈ C0, B ∩ C ∈ C0
Q : Set X.A
hQ : Q ∈ F
q : X.A
h : q ∈ Q
⊢ (X.str ⁻¹' Q).Nonempty
have h : X.incl q ∈ X.str ⁻¹' Q
Tactic: use X.incl q
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (hypothesis)
Goal:
X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ basic (cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun (x : fsu) ↦ (↑x : Set (Set (Ultrafilter X.A)))
C0 : ssu := {Z : Set (Ultrafilter X.A) | ∃ B ∈ F, X.str ⁻¹' B = Z}
AA : Set (Ultrafilter X.A) := {G : Ultrafilter X.A | A ∈ G}
C1 : ssu := insert AA C0
C2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure C1
claim1 : ∀ B ∈ C0, ∀ C ∈ C0, B ∩ C ∈ C0
⊢ X.str F ∈ cl A
have claim2 : ∀ B ∈ C0, B.Nonempty
Tactic: have claim2 : ∀ B ∈ C0, Set.Nonempty B := by
    rintro B ⟨Q, hQ, rfl⟩
    obtain ⟨q⟩ := Filter.nonempty_of_mem hQ
    use X.incl q
    simpa
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (hypothesis)
Goal:
X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ basic (cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun (x : fsu) ↦ (↑x : Set (Set (Ultrafilter X.A)))
C0 : ssu := {Z : Set (Ultrafilter X.A) | ∃ B ∈ F, X.str ⁻¹' B = Z}
AA : Set (Ultrafilter X.A) := {G : Ultrafilter X.A | A ∈ G}
C1 : ssu := insert AA C0
C2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure C1
claim1 : ∀ B ∈ C0, ∀ C ∈ C0, B ∩ C ∈ C0
claim2 : ∀ B ∈ C0, B.Nonempty
Q : Set X.A
hQ : Q ∈ F
⊢ (AA ∩ X.str ⁻¹' Q).Nonempty
have this : (Q ∩ cl A).Nonempty
Tactic: have : (Q ∩ cl A).Nonempty := Filter.nonempty_of_mem (inter_mem hQ hF)
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (goal)
Goal:
X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ basic (cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun (x : fsu) ↦ (↑x : Set (Set (Ultrafilter X.A)))
C0 : ssu := {Z : Set (Ultrafilter X.A) | ∃ B ∈ F, X.str ⁻¹' B = Z}
AA : Set (Ultrafilter X.A) := {G : Ultrafilter X.A | A ∈ G}
C1 : ssu := insert AA C0
C2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure C1
claim1 : ∀ B ∈ C0, ∀ C ∈ C0, B ∩ C ∈ C0
claim2 : ∀ B ∈ C0, B.Nonempty
Q : Set X.A
hQ : Q ∈ F
this : (Q ∩ cl A).Nonempty
⊢ (AA ∩ X.str ⁻¹' Q).Nonempty
have rcases : ∀ (q : X.A) (hq1 : q ∈ Q) (P : Ultrafilter X.A) (hq2 : P ∈ basic A) (hq3 : X.str P = q), (AA ∩ X.str ⁻¹' Q).Nonempty
Tactic: rcases this with ⟨q, hq1, P, hq2, hq3⟩
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (goal)
Goal:
X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ basic (cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun (x : fsu) ↦ (↑x : Set (Set (Ultrafilter X.A)))
C0 : ssu := {Z : Set (Ultrafilter X.A) | ∃ B ∈ F, X.str ⁻¹' B = Z}
AA : Set (Ultrafilter X.A) := {G : Ultrafilter X.A | A ∈ G}
C1 : ssu := insert AA C0
C2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure C1
claim1 : ∀ B ∈ C0, ∀ C ∈ C0, B ∩ C ∈ C0
claim2 : ∀ B ∈ C0, B.Nonempty
Q : Set X.A
hQ : Q ∈ F
q : X.A
hq1 : q ∈ Q
P : Ultrafilter X.A
hq2 : P ∈ basic A
hq3 : X.str P = q
⊢ (AA ∩ X.str ⁻¹' Q).Nonempty
have refine : P ∈ X.str ⁻¹' Q
Tactic: refine ⟨P, hq2, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (hypothesis)
Goal:
X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ basic (cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun (x : fsu) ↦ (↑x : Set (Set (Ultrafilter X.A)))
C0 : ssu := {Z : Set (Ultrafilter X.A) | ∃ B ∈ F, X.str ⁻¹' B = Z}
AA : Set (Ultrafilter X.A) := {G : Ultrafilter X.A | A ∈ G}
C1 : ssu := insert AA C0
C2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure C1
claim1 : ∀ B ∈ C0, ∀ C ∈ C0, B ∩ C ∈ C0
claim2 : ∀ B ∈ C0, B.Nonempty
Q : Set X.A
hQ : Q ∈ F
q : X.A
hq1 : q ∈ Q
P : Ultrafilter X.A
hq2 : P ∈ basic A
hq3 : X.str P = q
⊢ P ∈ X.str ⁻¹' Q
have hq1₁ : X.str P ∈ Q
Tactic: rw [← hq3] at hq1
Cleared hypotheses: hq1, hq2, hq3
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (hypothesis)
Goal:
X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ basic (cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun (x : fsu) ↦ (↑x : Set (Set (Ultrafilter X.A)))
C0 : ssu := {Z : Set (Ultrafilter X.A) | ∃ B ∈ F, X.str ⁻¹' B = Z}
AA : Set (Ultrafilter X.A) := {G : Ultrafilter X.A | A ∈ G}
C1 : ssu := insert AA C0
C2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure C1
claim1 : ∀ B ∈ C0, ∀ C ∈ C0, B ∩ C ∈ C0
claim2 : ∀ B ∈ C0, B.Nonempty
⊢ X.str F ∈ cl A
have claim3 : ∀ B ∈ C0, (AA ∩ B).Nonempty
Tactic: have claim3 : ∀ B ∈ C0, (AA ∩ B).Nonempty := by
    rintro B ⟨Q, hQ, rfl⟩
    have : (Q ∩ cl A).Nonempty := Filter.nonempty_of_mem (inter_mem hQ hF)
    rcases this with ⟨q, hq1, P, hq2, hq3⟩
    refine ⟨P, hq2, ?_⟩
    rw [← hq3] at hq1
    simpa
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (goal)
Goal:
X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ basic (cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun (x : fsu) ↦ (↑x : Set (Set (Ultrafilter X.A)))
C0 : ssu := {Z : Set (Ultrafilter X.A) | ∃ B ∈ F, X.str ⁻¹' B = Z}
AA : Set (Ultrafilter X.A) := {G : Ultrafilter X.A | A ∈ G}
C1 : ssu := insert AA C0
C2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure C1
claim1 : ∀ B ∈ C0, ∀ C ∈ C0, B ∩ C ∈ C0
claim2 : ∀ B ∈ C0, B.Nonempty
claim3 : ∀ B ∈ C0, (AA ∩ B).Nonempty
this : ∀ (T : fsu), ι T ⊆ C1 → (⋂₀ ι T).Nonempty
⊢ X.str F ∈ cl A
have obtain : ∀ (G : Ultrafilter (Ultrafilter X.A)) (h1 : C1 ⊆ (↑G : Filter (Ultrafilter X.A)).sets), X.str F ∈ cl A
Tactic: obtain ⟨G, h1⟩ := exists_ultrafilter_of_finite_inter_nonempty _ this
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (goal)
Goal:
X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ basic (cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun (x : fsu) ↦ (↑x : Set (Set (Ultrafilter X.A)))
C0 : ssu := {Z : Set (Ultrafilter X.A) | ∃ B ∈ F, X.str ⁻¹' B = Z}
AA : Set (Ultrafilter X.A) := {G : Ultrafilter X.A | A ∈ G}
C1 : ssu := insert AA C0
C2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure C1
claim1 : ∀ B ∈ C0, ∀ C ∈ C0, B ∩ C ∈ C0
claim2 : ∀ B ∈ C0, B.Nonempty
claim3 : ∀ B ∈ C0, (AA ∩ B).Nonempty
this : ∀ (T : fsu), ι T ⊆ C1 → (⋂₀ ι T).Nonempty
G : Ultrafilter (Ultrafilter X.A)
h1 : C1 ⊆ (↑G : Filter (Ultrafilter X.A)).sets
⊢ X.str F ∈ cl A
have h : X.join G ∈ basic A ∧ X.str (X.join G) = X.str F
Tactic: use X.join G
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (hypothesis)
Goal:
X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ basic (cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun (x : fsu) ↦ (↑x : Set (Set (Ultrafilter X.A)))
C0 : ssu := {Z : Set (Ultrafilter X.A) | ∃ B ∈ F, X.str ⁻¹' B = Z}
AA : Set (Ultrafilter X.A) := {G : Ultrafilter X.A | A ∈ G}
C1 : ssu := insert AA C0
C2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure C1
claim1 : ∀ B ∈ C0, ∀ C ∈ C0, B ∩ C ∈ C0
claim2 : ∀ B ∈ C0, B.Nonempty
claim3 : ∀ B ∈ C0, (AA ∩ B).Nonempty
this : ∀ (T : fsu), ι T ⊆ C1 → (⋂₀ ι T).Nonempty
G : Ultrafilter (Ultrafilter X.A)
h1 : C1 ⊆ (↑G : Filter (Ultrafilter X.A)).sets
⊢ X.join G ∈ basic A ∧ X.str (X.join G) = X.str F
have this₁ : Ultrafilter.map X.str G = F
Tactic: have : G.map X.str = F := Ultrafilter.coe_le_coe.1 fun S hS => h1 (Or.inr ⟨S, hS, rfl⟩)
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (goal)
Goal:
X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ basic (cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun (x : fsu) ↦ (↑x : Set (Set (Ultrafilter X.A)))
C0 : ssu := {Z : Set (Ultrafilter X.A) | ∃ B ∈ F, X.str ⁻¹' B = Z}
AA : Set (Ultrafilter X.A) := {G : Ultrafilter X.A | A ∈ G}
C1 : ssu := insert AA C0
C2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure C1
claim1 : ∀ B ∈ C0, ∀ C ∈ C0, B ∩ C ∈ C0
claim2 : ∀ B ∈ C0, B.Nonempty
claim3 : ∀ B ∈ C0, (AA ∩ B).Nonempty
this_1 : ∀ (T : fsu), ι T ⊆ C1 → (⋂₀ ι T).Nonempty
G : Ultrafilter (Ultrafilter X.A)
h1 : C1 ⊆ (↑G : Filter (Ultrafilter X.A)).sets
this : Ultrafilter.map X.str G = F
⊢ X.join G ∈ basic A ∧ X.str (X.join G) = X.str F
have h : X.join G ∈ basic A ∧ X.str F = X.str F
Tactic: rw [join_distrib, this]
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (goal)
Goal:
X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ basic (cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun (x : fsu) ↦ (↑x : Set (Set (Ultrafilter X.A)))
C0 : ssu := {Z : Set (Ultrafilter X.A) | ∃ B ∈ F, X.str ⁻¹' B = Z}
AA : Set (Ultrafilter X.A) := {G : Ultrafilter X.A | A ∈ G}
C1 : ssu := insert AA C0
C2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure C1
claim1 : ∀ B ∈ C0, ∀ C ∈ C0, B ∩ C ∈ C0
claim2 : ∀ B ∈ C0, B.Nonempty
claim3 : ∀ B ∈ C0, (AA ∩ B).Nonempty
⊢ X.str F ∈ cl A
have suffices : ∀ (T : fsu), ι T ⊆ C1 → (⋂₀ ι T).Nonempty
Tactic: suffices ∀ T : fsu, ι T ⊆ C1 → (⋂₀ ι T).Nonempty by
    obtain ⟨G, h1⟩ := exists_ultrafilter_of_finite_inter_nonempty _ this
    use X.join G
    have : G.map X.str = F := Ultrafilter.coe_le_coe.1 fun S hS => h1 (Or.inr ⟨S, hS, rfl⟩)
    rw [join_distrib, this]
    exact ⟨h1 (Or.inl rfl), rfl⟩
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (hypothesis)
Goal:
X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ basic (cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun (x : fsu) ↦ (↑x : Set (Set (Ultrafilter X.A)))
C0 : ssu := {Z : Set (Ultrafilter X.A) | ∃ B ∈ F, X.str ⁻¹' B = Z}
AA : Set (Ultrafilter X.A) := {G : Ultrafilter X.A | A ∈ G}
C1 : ssu := insert AA C0
C2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure C1
claim1 : ∀ B ∈ C0, ∀ C ∈ C0, B ∩ C ∈ C0
claim2 : ∀ B ∈ C0, B.Nonempty
claim3 : ∀ B ∈ C0, (AA ∩ B).Nonempty
⊢ ∀ (T : fsu), ι T ⊆ C1 → (⋂₀ ι T).Nonempty
have claim4 : FiniteInter (finiteInterClosure C1)
Tactic: have claim4 := finiteInterClosure_finiteInter C1
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (hypothesis)
Goal:
X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ basic (cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun (x : fsu) ↦ (↑x : Set (Set (Ultrafilter X.A)))
C0 : ssu := {Z : Set (Ultrafilter X.A) | ∃ B ∈ F, X.str ⁻¹' B = Z}
AA : Set (Ultrafilter X.A) := {G : Ultrafilter X.A | A ∈ G}
C1 : ssu := insert AA C0
C2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure C1
claim1 : ∀ B ∈ C0, ∀ C ∈ C0, B ∩ C ∈ C0
claim2 : ∀ B ∈ C0, B.Nonempty
claim3 : ∀ B ∈ C0, (AA ∩ B).Nonempty
claim4 : FiniteInter (finiteInterClosure C1)
⊢ ∀ (T : fsu), ι T ⊆ C1 → (⋂₀ ι T).Nonempty
have claim5 : FiniteInter C0
Tactic: have claim5 : FiniteInter C0 := ⟨⟨_, univ_mem, Set.preimage_univ⟩, claim1⟩
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (goal)
Goal:
X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ basic (cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun (x : fsu) ↦ (↑x : Set (Set (Ultrafilter X.A)))
C0 : ssu := {Z : Set (Ultrafilter X.A) | ∃ B ∈ F, X.str ⁻¹' B = Z}
AA : Set (Ultrafilter X.A) := {G : Ultrafilter X.A | A ∈ G}
C1 : ssu := insert AA C0
C2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure C1
claim1 : ∀ B ∈ C0, ∀ C ∈ C0, B ∩ C ∈ C0
claim2 : ∀ B ∈ C0, B.Nonempty
claim3 : ∀ B ∈ C0, (AA ∩ B).Nonempty
claim4 : FiniteInter (finiteInterClosure C1)
claim5 : FiniteInter C0
this : ∀ P ∈ C2, P ∈ C0 ∨ ∃ Q ∈ C0, P = AA ∩ Q
P : Set (Ultrafilter X.A)
hP : P ∈ C2
⊢ P.Nonempty
have inl : ∀ (h : P ∈ C0), P.Nonempty
Tactic: rcases this P hP with h | h
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (goal)
Goal:
X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ basic (cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun (x : fsu) ↦ (↑x : Set (Set (Ultrafilter X.A)))
C0 : ssu := {Z : Set (Ultrafilter X.A) | ∃ B ∈ F, X.str ⁻¹' B = Z}
AA : Set (Ultrafilter X.A) := {G : Ultrafilter X.A | A ∈ G}
C1 : ssu := insert AA C0
C2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure C1
claim1 : ∀ B ∈ C0, ∀ C ∈ C0, B ∩ C ∈ C0
claim2 : ∀ B ∈ C0, B.Nonempty
claim3 : ∀ B ∈ C0, (AA ∩ B).Nonempty
claim4 : FiniteInter (finiteInterClosure C1)
claim5 : FiniteInter C0
this : ∀ P ∈ C2, P ∈ C0 ∨ ∃ Q ∈ C0, P = AA ∩ Q
P : Set (Ultrafilter X.A)
hP : P ∈ C2
inl : ∀ (h : P ∈ C0), P.Nonempty
⊢ P.Nonempty
have inr : ∀ (h : ∃ Q ∈ C0, P = AA ∩ Q), P.Nonempty
Tactic: rcases this P hP with h | h