awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (hypothesis)
Goal:
X : Compactum
F : Ultrafilter X.A
x : X.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)))
T0 : ssu := {S : Set (Ultrafilter X.A) | ∃ A ∈ F, S = basic A}
AA : Set (Ultrafilter X.A) := X.str ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : (↑F : Filter X.A) ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ A ∈ F, x ∈ cl A
claim3 : ∀ S1 ∈ T0, ∀ S2 ∈ T0, S1 ∩ S2 ∈ T0
claim4 : ∀ S ∈ T0, (AA ∩ S).Nonempty
claim5 : ∀ S ∈ T0, S.Nonempty
claim6 : ∀ S ∈ T2, S.Nonempty
this : ∀ (F : fsu), (↑F : Set (Set (Ultrafilter X.A))) ⊆ T1 → (⋂₀ ι F).Nonempty
G : Ultrafilter (Ultrafilter X.A)
h1 : T1 ⊆ (↑G : Filter (Ultrafilter X.A)).sets
⊢ X.str F = x
have c1 : X.join G = F
Tactic: have c1 : X.join G = F := Ultrafilter.coe_le_coe.1 fun P hP => h1 (Or.inr ⟨P, hP, rfl⟩)
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (goal)
Goal:
X : Compactum
F : Ultrafilter X.A
x : X.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)))
T0 : ssu := {S : Set (Ultrafilter X.A) | ∃ A ∈ F, S = basic A}
AA : Set (Ultrafilter X.A) := X.str ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : (↑F : Filter X.A) ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ A ∈ F, x ∈ cl A
claim3 : ∀ S1 ∈ T0, ∀ S2 ∈ T0, S1 ∩ S2 ∈ T0
claim4 : ∀ S ∈ T0, (AA ∩ S).Nonempty
claim5 : ∀ S ∈ T0, S.Nonempty
claim6 : ∀ S ∈ T2, S.Nonempty
this : ∀ (F : fsu), (↑F : Set (Set (Ultrafilter X.A))) ⊆ T1 → (⋂₀ ι F).Nonempty
G : Ultrafilter (Ultrafilter X.A)
h1 : T1 ⊆ (↑G : Filter (Ultrafilter X.A)).sets
c1 : X.join G = F
⊢ Ultrafilter.map X.str G = X.incl x
have refine : ∀ (P : Set X.A) (hP : P ∈ (↑(X.incl x) : Filter X.A)), P ∈ (↑(Ultrafilter.map X.str G) : Filter X.A)
Tactic: refine Ultrafilter.coe_le_coe.1 fun P hP => ?_
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (goal)
Goal:
X : Compactum
F : Ultrafilter X.A
x : X.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)))
T0 : ssu := {S : Set (Ultrafilter X.A) | ∃ A ∈ F, S = basic A}
AA : Set (Ultrafilter X.A) := X.str ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : (↑F : Filter X.A) ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ A ∈ F, x ∈ cl A
claim3 : ∀ S1 ∈ T0, ∀ S2 ∈ T0, S1 ∩ S2 ∈ T0
claim4 : ∀ S ∈ T0, (AA ∩ S).Nonempty
claim5 : ∀ S ∈ T0, S.Nonempty
claim6 : ∀ S ∈ T2, S.Nonempty
this : ∀ (F : fsu), (↑F : Set (Set (Ultrafilter X.A))) ⊆ T1 → (⋂₀ ι F).Nonempty
G : Ultrafilter (Ultrafilter X.A)
h1 : T1 ⊆ (↑G : Filter (Ultrafilter X.A)).sets
c1 : X.join G = F
P : Set X.A
hP : P ∈ (↑(X.incl x) : Filter X.A)
⊢ P ∈ (↑(Ultrafilter.map X.str G) : Filter X.A)
have apply : AA ⊆ X.str ⁻¹' P
Tactic: apply mem_of_superset (h1 (Or.inl rfl))
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (hypothesis)
Goal:
X : Compactum
F : Ultrafilter X.A
x : X.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)))
T0 : ssu := {S : Set (Ultrafilter X.A) | ∃ A ∈ F, S = basic A}
AA : Set (Ultrafilter X.A) := X.str ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : (↑F : Filter X.A) ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ A ∈ F, x ∈ cl A
claim3 : ∀ S1 ∈ T0, ∀ S2 ∈ T0, S1 ∩ S2 ∈ T0
claim4 : ∀ S ∈ T0, (AA ∩ S).Nonempty
claim5 : ∀ S ∈ T0, S.Nonempty
claim6 : ∀ S ∈ T2, S.Nonempty
this : ∀ (F : fsu), (↑F : Set (Set (Ultrafilter X.A))) ⊆ T1 → (⋂₀ ι F).Nonempty
G : Ultrafilter (Ultrafilter X.A)
h1 : T1 ⊆ (↑G : Filter (Ultrafilter X.A)).sets
c1 : X.join G = F
⊢ X.str F = x
have c2 : Ultrafilter.map X.str G = X.incl x
Tactic: have c2 : G.map X.str = X.incl x := by
      refine Ultrafilter.coe_le_coe.1 fun P hP => ?_
      apply mem_of_superset (h1 (Or.inl rfl))
      rintro x ⟨rfl⟩
      exact hP
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (goal)
Goal:
X : Compactum
F : Ultrafilter X.A
x : X.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)))
T0 : ssu := {S : Set (Ultrafilter X.A) | ∃ A ∈ F, S = basic A}
AA : Set (Ultrafilter X.A) := X.str ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : (↑F : Filter X.A) ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ A ∈ F, x ∈ cl A
claim3 : ∀ S1 ∈ T0, ∀ S2 ∈ T0, S1 ∩ S2 ∈ T0
claim4 : ∀ S ∈ T0, (AA ∩ S).Nonempty
claim5 : ∀ S ∈ T0, S.Nonempty
claim6 : ∀ S ∈ T2, S.Nonempty
⊢ X.str F = x
have suffices : ∀ (F : fsu), (↑F : Set (Set (Ultrafilter X.A))) ⊆ T1 → (⋂₀ ι F).Nonempty
Tactic: suffices ∀ F : fsu, ↑F ⊆ T1 → (⋂₀ ι F).Nonempty by
    obtain ⟨G, h1⟩ := Ultrafilter.exists_ultrafilter_of_finite_inter_nonempty _ this
    have c1 : X.join G = F := Ultrafilter.coe_le_coe.1 fun P hP => h1 (Or.inr ⟨P, hP, rfl⟩)
    have c2 : G.map X.str = X.incl x := by
      refine Ultrafilter.coe_le_coe.1 fun P hP => ?_
      apply mem_of_superset (h1 (Or.inl rfl))
      rintro x ⟨rfl⟩
      exact hP
    simp [← c1, c2]
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (goal)
Goal:
X : Compactum
F : Ultrafilter X.A
x : X.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)))
T0 : ssu := {S : Set (Ultrafilter X.A) | ∃ A ∈ F, S = basic A}
AA : Set (Ultrafilter X.A) := X.str ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : (↑F : Filter X.A) ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ A ∈ F, x ∈ cl A
claim3 : ∀ S1 ∈ T0, ∀ S2 ∈ T0, S1 ∩ S2 ∈ T0
claim4 : ∀ S ∈ T0, (AA ∩ S).Nonempty
claim5 : ∀ S ∈ T0, S.Nonempty
claim6 : ∀ S ∈ T2, S.Nonempty
T : fsu
hT : (↑T : Set (Set (Ultrafilter X.A))) ⊆ T1
⊢ (⋂₀ ι T).Nonempty
have refine : (↑T : Set (Set (Ultrafilter X.A))) ⊆ finiteInterClosure T1
Tactic: refine claim6 _ (finiteInter_mem (.finiteInterClosure_finiteInter _) _ ?_)
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (goal)
Goal:
X : Compactum
⊢ T2Space.{u_1} X.A
have rw : ∀ {x y : X.A} (f : Ultrafilter X.A), (↑f : Filter X.A) ≤ 𝓝 x → (↑f : Filter X.A) ≤ 𝓝 y → x = y
Tactic: rw [t2_iff_ultrafilter]
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (goal)
Goal:
X : Compactum
x y : X.A
F : Ultrafilter X.A
hx : (↑F : Filter X.A) ≤ 𝓝 x
hy : (↑F : Filter X.A) ≤ 𝓝 y
⊢ x = y
have rw : X.str F = y
Tactic: rw [← str_eq_of_le_nhds _ _ hx, ← str_eq_of_le_nhds _ _ hy]
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (goal)
Goal:
X : Compactum
x y : X.A
F : Ultrafilter X.A
hx : (↑F : Filter X.A) ≤ 𝓝 x
hy : (↑F : Filter X.A) ≤ 𝓝 y
rw : X.str F = y
⊢ x = y
have rw₁ : X.str F = X.str F
Tactic: rw [← str_eq_of_le_nhds _ _ hx, ← str_eq_of_le_nhds _ _ hy]
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (goal)
Goal:
X : Compactum
F : Ultrafilter X.A
⊢ F.lim = X.str F
have rw : ∀ (s : Set X.A), X.str F ∈ s → IsOpen s → s ∈ (↑F : Filter X.A)
Tactic: rw [Ultrafilter.lim_eq_iff_le_nhds, le_nhds_iff]
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (goal)
Goal:
X : Compactum
A : Set X.A
⊢ cl A = closure A
have h : ∀ (x : X.A), x ∈ cl A ↔ x ∈ closure A
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (goal)
Goal:
X : Compactum
A : Set X.A
x : X.A
⊢ x ∈ cl A ↔ x ∈ closure A
have h : x ∈ cl A ↔ ∃ (u : Ultrafilter X.A), A ∈ u ∧ (↑u : Filter X.A) ≤ 𝓝 x
Tactic: rw [mem_closure_iff_ultrafilter]
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (goal)
Goal:
X : Compactum
A : Set X.A
x : X.A
⊢ x ∈ cl A ↔ ∃ (u : Ultrafilter X.A), A ∈ u ∧ (↑u : Filter X.A) ≤ 𝓝 x
have h : x ∈ cl A → ∃ (u : Ultrafilter X.A), A ∈ u ∧ (↑u : Filter X.A) ≤ 𝓝 x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (goal)
Goal:
X : Compactum
A : Set X.A
x : X.A
h : x ∈ cl A → ∃ (u : Ultrafilter X.A), A ∈ u ∧ (↑u : Filter X.A) ≤ 𝓝 x
⊢ x ∈ cl A ↔ ∃ (u : Ultrafilter X.A), A ∈ u ∧ (↑u : Filter X.A) ≤ 𝓝 x
have h₁ : (∃ (u : Ultrafilter X.A), A ∈ u ∧ (↑u : Filter X.A) ≤ 𝓝 x) → x ∈ cl A
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (goal)
Goal:
X Y : Compactum
f : X ⟶ Y
⊢ Continuous (X := X.A) (Y := Y.A)
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : Compactum.{u_1}) ↦ x1 ⟶ x2) (CC := Monad.Algebra.A) f) :
      (a : X.A) → Y.A)
have rw : ∀ (x : X.A) (g : Ultrafilter X.A),
  (↑g : Filter X.A) ≤ 𝓝 x →
    Tendsto («β» := Y.A)
      ((⇑(ConcreteCategory.hom (FC := fun (x1 x2 : Compactum.{u_1}) ↦ x1 ⟶ x2) (CC := Monad.Algebra.A) f) :
          (a : X.A) → Y.A) :
        (a : X.A) → Y.A)
      (↑g : Filter X.A)
      (𝓝
          ((ConcreteCategory.hom (FC := fun (x1 x2 : Compactum.{u_1}) ↦ x1 ⟶ x2) (CC := Monad.Algebra.A) f :
              (a : X.A) → Y.A)
            x) :
        Filter Y.A)
Tactic: rw [continuous_iff_ultrafilter]
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (goal)
Goal:
X Y : Compactum
f : X ⟶ Y
x : X.A
g : Ultrafilter X.A
h : (↑g : Filter X.A) ≤ 𝓝 x
⊢ LE.le (α := Filter Y.A)
    ((↑(Ultrafilter.map
            (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : Compactum.{u_1}) ↦ x1 ⟶ x2) (CC := Monad.Algebra.A) f) :
              (a : X.A) → Y.A)
            g) :
        Filter Y.A) :
      Filter Y.A)
    (𝓝
        ((ConcreteCategory.hom (FC := fun (x1 x2 : Compactum.{u_1}) ↦ x1 ⟶ x2) (CC := Monad.Algebra.A) f :
            (a : X.A) → Y.A)
          x) :
      Filter Y.A)
have a : 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)
      g) =
  (ConcreteCategory.hom (FC := fun (x1 x2 : Compactum.{u_1}) ↦ x1 ⟶ x2) (CC := Monad.Algebra.A) f : (a : X.A) → Y.A) x
Tactic: apply le_nhds_of_str_eq
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
⊢ β.η.app X ≫ ↾Ultrafilter.lim = 𝟙 X
have h : ∀ (x : Functor.obj (𝟭 (Type u_1)) X),
  (ConcreteCategory.hom (FC := TypeCat.Fun) (β.η.app X ≫ ↾Ultrafilter.lim)).toFun x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 X)).toFun x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
⊢ β.μ.app X ≫ ↾Ultrafilter.lim = β.map (↾Ultrafilter.lim) ≫ ↾Ultrafilter.lim
have h : ∀ (FF : (β.toFunctor ⋙ β.toFunctor).obj X),
  (ConcreteCategory.hom (FC := TypeCat.Fun) (β.μ.app X ≫ ↾Ultrafilter.lim)).toFun FF =
    TypeCat.Fun.toFun (ConcreteCategory.hom (FC := TypeCat.Fun) (β.map (↾Ultrafilter.lim) ≫ ↾Ultrafilter.lim)) FF
Tactic: ext FF
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
FF : (β.toFunctor ⋙ β.toFunctor).obj X
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (β.μ.app X ≫ ↾Ultrafilter.lim)).toFun FF =
    TypeCat.Fun.toFun (ConcreteCategory.hom (FC := TypeCat.Fun) (β.map (↾Ultrafilter.lim) ≫ ↾Ultrafilter.lim)) FF
have h : ∀ (FF : Ultrafilter (Ultrafilter X)),
  (ConcreteCategory.hom (FC := TypeCat.Fun) (β.μ.app X ≫ ↾Ultrafilter.lim)).toFun FF =
    TypeCat.Fun.toFun (ConcreteCategory.hom (FC := TypeCat.Fun) (β.map (↾Ultrafilter.lim) ≫ ↾Ultrafilter.lim)) FF
Tactic: change Ultrafilter (Ultrafilter X) at FF
Cleared hypotheses: FF
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
FF : Ultrafilter (Ultrafilter X)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (β.μ.app X ≫ ↾Ultrafilter.lim)).toFun FF =
    TypeCat.Fun.toFun (ConcreteCategory.hom (FC := TypeCat.Fun) (β.map (↾Ultrafilter.lim) ≫ ↾Ultrafilter.lim)) FF
have c1 : let x := (Ultrafilter.map Ultrafilter.lim FF).lim;
x = (Ultrafilter.map Ultrafilter.lim FF).lim
Tactic: set x := (Ultrafilter.map Ultrafilter.lim FF).lim with c1
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
FF : Ultrafilter (Ultrafilter X)
x : X := (Ultrafilter.map Ultrafilter.lim FF).lim
c1 : x = (Ultrafilter.map Ultrafilter.lim FF).lim
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (β.μ.app X ≫ ↾Ultrafilter.lim)).toFun FF =
    TypeCat.Fun.toFun (ConcreteCategory.hom (FC := TypeCat.Fun) (β.map (↾Ultrafilter.lim) ≫ ↾Ultrafilter.lim)) FF
have c2 : ∀ (U : Set X) (F : Ultrafilter X), F.lim ∈ U → IsOpen[inst] U → U ∈ F
Tactic: have c2 : ∀ (U : Set X) (F : Ultrafilter X), F.lim ∈ U → IsOpen U → U ∈ F := by
      intro U F h1 hU
      exact isOpen_iff_ultrafilter.mp hU _ h1 _ (Ultrafilter.le_nhds_lim _)
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
FF : Ultrafilter (Ultrafilter X)
x : X := (Ultrafilter.map Ultrafilter.lim FF).lim
c1 : x = (Ultrafilter.map Ultrafilter.lim FF).lim
c2 : ∀ (U : Set X) (F : Ultrafilter X), F.lim ∈ U → IsOpen[inst] U → U ∈ F
⊢ (↑(Ultrafilter.map Ultrafilter.lim FF) : Filter X) ≤ 𝓝 x
have rw : ∀ (s : Set X), x ∈ s → IsOpen[inst] s → s ∈ (↑(Ultrafilter.map Ultrafilter.lim FF) : Filter X)
Tactic: rw [le_nhds_iff]
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
FF : Ultrafilter (Ultrafilter X)
x : X := (Ultrafilter.map Ultrafilter.lim FF).lim
c1 : x = (Ultrafilter.map Ultrafilter.lim FF).lim
c2 : ∀ (U : Set X) (F : Ultrafilter X), F.lim ∈ U → IsOpen[inst] U → U ∈ F
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (β.μ.app X ≫ ↾Ultrafilter.lim)).toFun FF =
    TypeCat.Fun.toFun (ConcreteCategory.hom (FC := TypeCat.Fun) (β.map (↾Ultrafilter.lim) ≫ ↾Ultrafilter.lim)) FF
have c3 : (↑(Ultrafilter.map Ultrafilter.lim FF) : Filter X) ≤ 𝓝 x
Tactic: have c3 : ↑(Ultrafilter.map Ultrafilter.lim FF) ≤ 𝓝 x := by
      rw [le_nhds_iff]
      intro U hx hU
      exact mem_coe.2 (c2 _ _ (by rwa [← c1]) hU)
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
FF : Ultrafilter (Ultrafilter X)
x : X := (Ultrafilter.map Ultrafilter.lim FF).lim
c1 : x = (Ultrafilter.map Ultrafilter.lim FF).lim
c2 : ∀ (U : Set X) (F : Ultrafilter X), F.lim ∈ U → IsOpen[inst] U → U ∈ F
c3 : (↑(Ultrafilter.map Ultrafilter.lim FF) : Filter X) ≤ 𝓝 x
U : Set X
hx : x ∈ U
hU : IsOpen[inst] U
this : Ultrafilter.lim ⁻¹' U ∈ FF
⊢ {G : Ultrafilter X | U ∈ G} ∈ FF
have apply : Ultrafilter.lim ⁻¹' U ⊆ {G : Ultrafilter X | U ∈ G}
Tactic: apply mem_of_superset this
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
FF : Ultrafilter (Ultrafilter X)
x : X := (Ultrafilter.map Ultrafilter.lim FF).lim
c1 : x = (Ultrafilter.map Ultrafilter.lim FF).lim
c2 : ∀ (U : Set X) (F : Ultrafilter X), F.lim ∈ U → IsOpen[inst] U → U ∈ F
c3 : (↑(Ultrafilter.map Ultrafilter.lim FF) : Filter X) ≤ 𝓝 x
U : Set X
hx : x ∈ U
hU : IsOpen[inst] U
⊢ {G : Ultrafilter X | U ∈ G} ∈ FF
have suffices : Ultrafilter.lim ⁻¹' U ∈ FF
Tactic: suffices Ultrafilter.lim ⁻¹' U ∈ FF by
        apply mem_of_superset this
        intro P hP
        exact c2 U P hP hU
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
FF : Ultrafilter (Ultrafilter X)
x : X := (Ultrafilter.map Ultrafilter.lim FF).lim
c1 : x = (Ultrafilter.map Ultrafilter.lim FF).lim
c2 : ∀ (U : Set X) (F : Ultrafilter X), F.lim ∈ U → IsOpen[inst] U → U ∈ F
c3 : (↑(Ultrafilter.map Ultrafilter.lim FF) : Filter X) ≤ 𝓝 x
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (β.μ.app X ≫ ↾Ultrafilter.lim)).toFun FF =
    TypeCat.Fun.toFun (ConcreteCategory.hom (FC := TypeCat.Fun) (β.map (↾Ultrafilter.lim) ≫ ↾Ultrafilter.lim)) FF
have c4 : ∀ (U : Set X), x ∈ U → IsOpen[inst] U → {G : Ultrafilter X | U ∈ G} ∈ FF
Tactic: have c4 : ∀ U : Set X, x ∈ U → IsOpen U → { G : Ultrafilter X | U ∈ G } ∈ FF := by
      intro U hx hU
      suffices Ultrafilter.lim ⁻¹' U ∈ FF by
        apply mem_of_superset this
        intro P hP
        exact c2 U P hP hU
      exact @c3 U (IsOpen.mem_nhds hU hx)
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
FF : Ultrafilter (Ultrafilter X)
x : X := (Ultrafilter.map Ultrafilter.lim FF).lim
c1 : x = (Ultrafilter.map Ultrafilter.lim FF).lim
c2 : ∀ (U : Set X) (F : Ultrafilter X), F.lim ∈ U → IsOpen[inst] U → U ∈ F
c3 : (↑(Ultrafilter.map Ultrafilter.lim FF) : Filter X) ≤ 𝓝 x
c4 : ∀ (U : Set X), x ∈ U → IsOpen[inst] U → {G : Ultrafilter X | U ∈ G} ∈ FF
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (β.μ.app X ≫ ↾Ultrafilter.lim)).toFun FF =
    TypeCat.Fun.toFun (ConcreteCategory.hom (FC := TypeCat.Fun) (β.map (↾Ultrafilter.lim) ≫ ↾Ultrafilter.lim)) FF
have h : (↑((β.μ.app X).hom'.toFun FF) : Filter X) ≤
  𝓝 (TypeCat.Fun.toFun (ConcreteCategory.hom (FC := TypeCat.Fun) (β.map (↾Ultrafilter.lim) ≫ ↾Ultrafilter.lim)) FF)
Tactic: apply lim_eq
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
FF : Ultrafilter (Ultrafilter X)
x : X := (Ultrafilter.map Ultrafilter.lim FF).lim
c1 : x = (Ultrafilter.map Ultrafilter.lim FF).lim
c2 : ∀ (U : Set X) (F : Ultrafilter X), F.lim ∈ U → IsOpen[inst] U → U ∈ F
c3 : (↑(Ultrafilter.map Ultrafilter.lim FF) : Filter X) ≤ 𝓝 x
c4 : ∀ (U : Set X), x ∈ U → IsOpen[inst] U → {G : Ultrafilter X | U ∈ G} ∈ FF
⊢ (↑((β.μ.app X).hom'.toFun FF) : Filter X) ≤
    𝓝 (TypeCat.Fun.toFun (ConcreteCategory.hom (FC := TypeCat.Fun) (β.map (↾Ultrafilter.lim) ≫ ↾Ultrafilter.lim)) FF)
have h : ∀ (s : Set X),
  TypeCat.Fun.toFun (ConcreteCategory.hom (FC := TypeCat.Fun) (β.map (↾Ultrafilter.lim) ≫ ↾Ultrafilter.lim)) FF ∈ s →
    IsOpen[inst] s → s ∈ (↑((β.μ.app X).hom'.toFun FF) : Filter X)
Tactic: rw [le_nhds_iff]
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (hypothesis)
Goal:
X Y : Compactum
f : X.A → Y.A
cont : Continuous f
⊢ β.map (↾f) ≫ Y.a = X.a ≫ ↾f
have cont₁ : ∀ (x : X.A) (g : Ultrafilter X.A), (↑g : Filter X.A) ≤ 𝓝 x → Tendsto f (↑g : Filter X.A) (𝓝 (f x))
Tactic: rw [continuous_iff_ultrafilter] at cont
Cleared hypotheses: cont
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (goal)
Goal:
X Y : Compactum
f : X.A → Y.A
cont : ∀ (x : X.A) (g : Ultrafilter X.A), (↑g : Filter X.A) ≤ 𝓝 x → Tendsto f (↑g : Filter X.A) (𝓝 (f x))
⊢ β.map (↾f) ≫ Y.a = X.a ≫ ↾f
have h : ∀ (F : Ultrafilter X.A),
  (ConcreteCategory.hom (FC := TypeCat.Fun) (β.map (↾f) ≫ Y.a)).toFun F =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.a ≫ ↾f)).toFun F
Tactic: ext (F : Ultrafilter X)
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (hypothesis)
Goal:
X Y : Compactum
f : X.A → Y.A
cont : ∀ (x : X.A) (g : Ultrafilter X.A), (↑g : Filter X.A) ≤ 𝓝 x → Tendsto f (↑g : Filter X.A) (𝓝 (f x))
F : Ultrafilter X.A
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (β.map (↾f) ≫ Y.a)).toFun F =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.a ≫ ↾f)).toFun F
have cont₁ : Tendsto f (↑F : Filter X.A) (𝓝 (f (X.str F)))
Tactic: specialize cont (X.str F) F (le_nhds_of_str_eq F (X.str F) rfl)
Cleared hypotheses: cont
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (goal)
Goal:
X Y : Compactum
⊢ Function.Injective (α := X ⟶ Y) compactumToCompHaus.map
have _ : ∀ ⦃a₁ a₂ : X ⟶ Y⦄, compactumToCompHaus.map a₁ = compactumToCompHaus.map a₂ → a₁ = a₂
Tactic: _
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (goal)
Goal:
X Y : Compactum
a₁ a₂ : X ⟶ Y
h : compactumToCompHaus.map a₁ = compactumToCompHaus.map a₂
⊢ a₁ = a₂
have f : a₁.f = a₂.f
Tactic: apply Monad.Algebra.Hom.ext
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (goal)
Goal:
X Y : Compactum
a₁ a₂ : X ⟶ Y
h : compactumToCompHaus.map a₁ = compactumToCompHaus.map a₂
⊢ a₁.f = a₂.f
have f : ∀ (x : X.A),
  (ConcreteCategory.hom (FC := TypeCat.Fun) a₁.f).toFun x = (ConcreteCategory.hom (FC := TypeCat.Fun) a₂.f).toFun x
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (hypothesis)
Goal:
D : CompHaus
x : Set (↑D.1 : Type u_1)
h : IsOpen x
⊢ IsOpen (id ⁻¹' x)
have h₁ : ∀ (F : Ultrafilter (↑D.1 : Type u_1)), F.lim ∈ x → x ∈ (↑F : Filter (↑D.1 : Type u_1))
Tactic: rw [isOpen_iff_ultrafilter'] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Category.Compactum (goal)
Goal:
D : CompHaus
x : Set (Compactum.ofTopologicalSpace (↑(D.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1)).A
h1 : IsOpen x
⊢ IsOpen (id ⁻¹' x)
have rw : ∀ (F : Ultrafilter (↑D.1 : Type u_1)), F.lim ∈ id ⁻¹' x → id ⁻¹' x ∈ (↑F : Filter (↑D.1 : Type u_1))
Tactic: rw [isOpen_iff_ultrafilter']
-- Lean 4 proof step from Mathlib.Topology.Category.DeltaGenerated (goal)
Goal:
X Y : TopCat
a₁ a₂ : X ⟶ Y
h : topToDeltaGenerated.map a₁ = topToDeltaGenerated.map a₂
⊢ a₁ = a₂
have w : ∀ (x : (↑X : Type u)),
  Eq (α := (↑Y : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) a₁ :
          (a : (↑X : Type u)) → (↑Y : Type u))
        x :
      (↑Y : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) a₂ :
          (a : (↑X : Type u)) → (↑Y : Type u))
        x :
      (↑Y : Type u))
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Category.LightProfinite.AsLimit (goal)
Goal:
S : LightProfinite
x x_1 : ℕᵒᵖ
x_2 : x ⟶ x_1
⊢ CategoryTheory.Functor.map (Functor.obj (Functor.const ℕᵒᵖ) S) x_2 ≫
      (lightToProfiniteFullyFaithful.preimageIso
            ((Cone.forget (S.diagram ⋙ lightToProfinite)).mapIso S.isoMapCone)).inv ≫
        S.asLimitConeAux.π.app x_1 =
    ((lightToProfiniteFullyFaithful.preimageIso
            ((Cone.forget (S.diagram ⋙ lightToProfinite)).mapIso S.isoMapCone)).inv ≫
        S.asLimitConeAux.π.app x) ≫
      S.diagram.map x_2
have simp : CategoryTheory.Functor.map (Functor.obj (Functor.const ℕᵒᵖ) S) x_2 ≫
    (lightToProfiniteFullyFaithful.preimageIso ((Cone.forget (S.diagram ⋙ lightToProfinite)).mapIso S.isoMapCone)).inv ≫
      S.asLimitConeAux.π.app x_1 =
  (lightToProfiniteFullyFaithful.preimageIso ((Cone.forget (S.diagram ⋙ lightToProfinite)).mapIso S.isoMapCone)).inv ≫
    S.asLimitConeAux.π.app x_1
Tactic: simp only [Category.assoc, S.asLimitConeAux.w]
-- Lean 4 proof step from Mathlib.Topology.Category.LightProfinite.AsLimit (goal)
Goal:
S : LightProfinite
x : ℕᵒᵖ
⊢ S.asLimitConeAux.π.app x =
    (lightToProfiniteFullyFaithful.preimageIso ((Cone.forget (S.diagram ⋙ lightToProfinite)).mapIso S.isoMapCone)).hom ≫
      S.asLimitCone.π.app x
have rw : (lightToProfiniteFullyFaithful.preimageIso ((Cone.forget (S.diagram ⋙ lightToProfinite)).mapIso S.isoMapCone)).inv ≫
    S.asLimitConeAux.π.app x =
  S.asLimitCone.π.app x
Tactic: rw [← @Iso.inv_comp_eq]