awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Subcomplex (goal)
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
E : Subcomplex C (D := D)
n : ℕ
i : (↑(E.I (C := C) (D := D) n) : Type u_1)
J : (m : ℕ) → Finset (@cell _ t C D _ m)
x : X
hx : x ∈ (↑(map (C := C) (D := D) n (↑i : cell C n)) : (Fin n → ℝ) → X) '' sphere 0 1
hJ : x ∈ D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ J m, openCell (C := C) (D := D) m j
⊢ x ∈
    D ∪
      ⋃ (m : ℕ),
        ⋃ (_ : m < n),
          ⋃ (j : (↑(E.I (C := C) (D := D) m) : Type u_1)),
            ⋃ (_ :
              Membership.mem (γ := Finset (↑(E.I (C := C) (D := D) m) : Type u_1))
                ((fun (m : ℕ) ↦
                    ((J m).preimage (Subtype.val (p := fun (x : @cell _ t C D _ m) ↦ x ∈ E.I (C := C) (D := D) m)) ⋯ :
                      Finset (↑(E.I (C := C) (D := D) m) : Type u_1)))
                  m)
                j),
              (↑(map (C := C) (D := D) m (↑j : cell C m)) : (Fin m → ℝ) → X) '' closedBall 0 1
have h : ∀ (hJ : x ∉ D → ∃ i < n, ∃ i_1 ∈ J i, x ∈ openCell (C := C) (D := D) i i_1),
  x ∉ D →
    ∃ i < n,
      ∃ i_1 ∈ E.I (C := C) (D := D) i,
        i_1 ∈ J i ∧
          Membership.mem (γ := Set X)
            ((fun (a : Fin i → ℝ) ↦ (↑(map (C := C) (D := D) i i_1) : (Fin i → ℝ) → X) a) '' closedBall 0 1) x
Tactic: simp_rw [iUnion_coe_set, mem_union, mem_iUnion, Finset.mem_preimage, exists_prop,
      Decidable.or_iff_not_imp_left] at hJ ⊢
Cleared hypotheses: hJ
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Subcomplex (hypothesis)
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
E : Subcomplex C (D := D)
n : ℕ
i : (↑(E.I (C := C) (D := D) n) : Type u_1)
J : (m : ℕ) → Finset (@cell _ t C D _ m)
x : X
hx : x ∈ (↑(map (C := C) (D := D) n (↑i : cell C n)) : (Fin n → ℝ) → X) '' sphere 0 1
hJ : x ∉ D → ∃ i < n, ∃ i_1 ∈ J i, x ∈ openCell (C := C) (D := D) i i_1
h : x ∉ D
⊢ ∃ i < n,
    ∃ i_1 ∈ E.I (C := C) (D := D) i,
      i_1 ∈ J i ∧
        Membership.mem (γ := Set X)
          ((fun (a : Fin i → ℝ) ↦ (↑(map (C := C) (D := D) i i_1) : (Fin i → ℝ) → X) a) '' closedBall 0 1) x
have hJ₁ : ∃ i < n, ∃ i_1 ∈ J i, x ∈ openCell (C := C) (D := D) i i_1
Tactic: specialize hJ h
Cleared hypotheses: hJ
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Subcomplex (goal)
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
E : Subcomplex C (D := D)
n : ℕ
i : (↑(E.I (C := C) (D := D) n) : Type u_1)
J : (m : ℕ) → Finset (@cell _ t C D _ m)
x : X
hx : x ∈ (↑(map (C := C) (D := D) n (↑i : cell C n)) : (Fin n → ℝ) → X) '' sphere 0 1
h : x ∉ D
hJ : ∃ i < n, ∃ i_1 ∈ J i, x ∈ openCell (C := C) (D := D) i i_1
⊢ ∃ i < n,
    ∃ i_1 ∈ E.I (C := C) (D := D) i,
      i_1 ∈ J i ∧
        Membership.mem (γ := Set X)
          ((fun (a : Fin i → ℝ) ↦ (↑(map (C := C) (D := D) i i_1) : (Fin i → ℝ) → X) a) '' closedBall 0 1) x
have h₁ : ∀ (m : ℕ) (hmn : m < n) (j : @cell _ t C D _ m) (hj : j ∈ J m) (hxj : x ∈ openCell (C := C) (D := D) m j),
  ∃ i < n,
    ∃ i_1 ∈ E.I (C := C) (D := D) i,
      i_1 ∈ J i ∧
        Membership.mem (γ := Set X)
          ((fun (a : Fin i → ℝ) ↦ (↑(map (C := C) (D := D) i i_1) : (Fin i → ℝ) → X) a) '' closedBall 0 1) x
Tactic: obtain ⟨m, hmn, j, hj, hxj⟩ := hJ
Cleared hypotheses: hJ
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Subcomplex (goal)
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
E : Subcomplex C (D := D)
n : ℕ
i : (↑(E.I (C := C) (D := D) n) : Type u_1)
J : (m : ℕ) → Finset (@cell _ t C D _ m)
x : X
hx : x ∈ (↑(map (C := C) (D := D) n (↑i : cell C n)) : (Fin n → ℝ) → X) '' sphere 0 1
h : x ∉ D
m : ℕ
hmn : m < n
j : @cell _ t C D _ m
hj : j ∈ J m
hxj : x ∈ openCell (C := C) (D := D) m j
⊢ ∃ i < n,
    ∃ i_1 ∈ E.I (C := C) (D := D) i,
      i_1 ∈ J i ∧
        Membership.mem (γ := Set X)
          ((fun (a : Fin i → ℝ) ↦ (↑(map (C := C) (D := D) i i_1) : (Fin i → ℝ) → X) a) '' closedBall 0 1) x
have h₁ : j ∈ E.I (C := C) (D := D) m
Tactic: suffices j ∈ E.I m from ⟨m, hmn, j, this, hj, openCell_subset_closedCell _ _ hxj⟩
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Subcomplex (hypothesis)
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
E : Subcomplex C (D := D)
n : ℕ
i : (↑(E.I (C := C) (D := D) n) : Type u_1)
J : (m : ℕ) → Finset (@cell _ t C D _ m)
x : X
hx : x ∈ (↑(map (C := C) (D := D) n (↑i : cell C n)) : (Fin n → ℝ) → X) '' sphere 0 1
h : x ∉ D
m : ℕ
hmn : m < n
j : @cell _ t C D _ m
hj : j ∈ J m
hxj : x ∈ openCell (C := C) (D := D) m j
⊢ j ∈ E.I (C := C) (D := D) m
have this : x ∈ (↑E : Set X)
Tactic: have : x ∈ (E : Set X) := E.cellFrontier_subset_of_mem i.2 hx
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Subcomplex (goal)
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
E : Subcomplex C (D := D)
n : ℕ
i : (↑(E.I (C := C) (D := D) n) : Type u_1)
J : (m : ℕ) → Finset (@cell _ t C D _ m)
x : X
hx : x ∈ (↑(map (C := C) (D := D) n (↑i : cell C n)) : (Fin n → ℝ) → X) '' sphere 0 1
h : x ∉ D
m : ℕ
hmn : m < n
j : @cell _ t C D _ m
hj : j ∈ J m
hxj : x ∈ openCell (C := C) (D := D) m j
this : x ∈ (↑E : Set X)
⊢ j ∈ E.I (C := C) (D := D) m
have h₁ : ∀ (hj' : ¬j ∈ E.I (C := C) (D := D) m), False
Tactic: by_contra hj'
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Subcomplex (goal)
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
E : Subcomplex C (D := D)
A : Set X
hA : A ⊆ (↑E : Set X)
h :
  (∀ (n : ℕ) (j : (↑(E.I (C := C) (D := D) n) : Type u_1)),
      IsClosed[t] (A ∩ (↑(map (C := C) (D := D) n (↑j : cell C n)) : (Fin n → ℝ) → X) '' closedBall 0 1)) ∧
    IsClosed[t] (A ∩ D)
⊢ IsClosed[t] A
have apply : ∀ (n : ℕ),
  0 < n →
    ∀ (j : @cell _ t C D _ n),
      Disjoint A (openCell (C := C) (D := D) n j) ∨ IsClosed[t] (A ∩ closedCell (C := C) (D := D) n j)
Tactic: apply isClosed_of_disjoint_openCell_or_isClosed_inter_closedCell
      (subset_trans hA (subset_complex (C := C) E)) h.2
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Subcomplex (goal)
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
E : Subcomplex C (D := D)
A : Set X
hA : A ⊆ (↑E : Set X)
h :
  (∀ (n : ℕ) (j : (↑(E.I (C := C) (D := D) n) : Type u_1)),
      IsClosed[t] (A ∩ (↑(map (C := C) (D := D) n (↑j : cell C n)) : (Fin n → ℝ) → X) '' closedBall 0 1)) ∧
    IsClosed[t] (A ∩ D)
n : ℕ
h_1 : 0 < n
j : @cell _ t C D _ n
⊢ Disjoint A (openCell (C := C) (D := D) n j) ∨ IsClosed[t] (A ∩ closedCell (C := C) (D := D) n j)
have pos : ∀ (hj : j ∈ E.I (C := C) (D := D) n),
  Disjoint A (openCell (C := C) (D := D) n j) ∨ IsClosed[t] (A ∩ closedCell (C := C) (D := D) n j)
Tactic: by_cases hj : j ∈ E.I n
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Subcomplex (goal)
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
E : Subcomplex C (D := D)
A : Set X
hA : A ⊆ (↑E : Set X)
h :
  (∀ (n : ℕ) (j : (↑(E.I (C := C) (D := D) n) : Type u_1)),
      IsClosed[t] (A ∩ (↑(map (C := C) (D := D) n (↑j : cell C n)) : (Fin n → ℝ) → X) '' closedBall 0 1)) ∧
    IsClosed[t] (A ∩ D)
n : ℕ
h_1 : 0 < n
j : @cell _ t C D _ n
pos :
  ∀ (hj : j ∈ E.I (C := C) (D := D) n),
    Disjoint A (openCell (C := C) (D := D) n j) ∨ IsClosed[t] (A ∩ closedCell (C := C) (D := D) n j)
⊢ Disjoint A (openCell (C := C) (D := D) n j) ∨ IsClosed[t] (A ∩ closedCell (C := C) (D := D) n j)
have neg : ∀ (hj : j ∉ E.I (C := C) (D := D) n),
  Disjoint A (openCell (C := C) (D := D) n j) ∨ IsClosed[t] (A ∩ closedCell (C := C) (D := D) n j)
Tactic: by_cases hj : j ∈ E.I n
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Subcomplex (goal)
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
inst_2 : FiniteDimensional C (D := D)
E : Subcomplex C (D := D)
⊢ ∀ᶠ (n : ℕ) in Filter.atTop, IsEmpty.{u_1 + 1} (@cell _ t (↑E : Set X) D _ n)
have h : ∀ (n : ℕ) (hn : IsEmpty.{u_1 + 1} (@cell _ t C D _ n)), IsEmpty.{u_1 + 1} (@cell _ t (↑E : Set X) D _ n)
Tactic: filter_upwards [FiniteDimensional.eventually_isEmpty_cell (C := C) (D := D)] with n hn
-- Lean 4 proof step from Mathlib.Topology.Category.CompHaus.Basic (goal)
Goal:
X : TopCat
Y : CompHaus
f :
  (↑((stoneCechObj X).toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) →
    (↑(Y.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)
hf : Continuous f
x : (↑(toTop (P := fun (x : TopCat.{u}) ↦ True) (of (fun (x : TopCat.{u}) ↦ True) (StoneCech (↑X : Type u)))) : Type u)
y : (↑X : Type u)
⊢ stoneCechExtend (g :=
      ContinuousMap.toFun
        (TopCat.Hom.hom
          ((fun (f : stoneCechObj X ⟶ Y) ↦
              TopCat.ofHom
                {
                  toFun :=
                    Function.comp (β :=
                      (fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
                          (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u))
                        (stoneCechObj X))
                      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
                            C((↑(x1.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u),
                              (↑(x2.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)))
                            (CC := fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
                            (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) f) :
                        (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) (stoneCechObj X)) →
                          (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) Y)
                      stoneCechUnit,
                  continuous_toFun := ⋯ : C((↑X : Type u), (↑Y.1 : Type u)) })
            {
              hom :=
                {
                  hom' :=
                    { toFun := f, continuous_toFun := hf :
                      C((↑((stoneCechObj X).toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u),
                        (↑(Y.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) } :
                  (stoneCechObj X).toTop (P := fun (x : TopCat.{u}) ↦ True).Hom
                    (Y.toTop (P := fun (x : TopCat.{u}) ↦ True)) } :
              InducedCategory.Hom (D := TopCat) (F := toTop (P := fun (x : TopCat.{u}) ↦ True)) (stoneCechObj X) Y })))
      ⋯ (stoneCechUnit y) =
    f (stoneCechUnit y)
have apply : Continuous.{u, u} (X := (↑X : Type u)) (Y := (↑((stoneCechObj X).toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u))
  stoneCechUnit
Tactic: apply congr_fun (stoneCechExtend_extends (hf.comp _)) y
-- Lean 4 proof step from Mathlib.Topology.Category.CompHaus.Basic (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CompHaus
FF : J ⥤ TopCat := F ⋙ compHausToTop
⊢ CompactSpace (↑(TopCat.limitCone.{v, u, v} FF).pt : Type (max u v))
have change : CompactSpace
  (↑{u : (j : J) → (↑((F.obj j).toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)) |
        ∀ {i j : J} (f : i ⟶ j),
          (ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat) ↦ True) ↦
                  C((↑(x1.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)),
                    (↑(x2.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v))))
                  (CC := fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦
                  (↑(X.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v))) (F.map f) :
                (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type (max u v))) (F.obj i)) →
                  (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type (max u v))) (F.obj j))
              (u i) =
            u j} :
    Type (max u v))
Tactic: change CompactSpace { u : ∀ j, F.obj j | ∀ {i j : J} (f : i ⟶ j), (F.map f) (u i) = u j }
-- Lean 4 proof step from Mathlib.Topology.Category.CompHaus.Basic (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CompHaus
FF : J ⥤ TopCat := F ⋙ compHausToTop
⊢ CompactSpace
    (↑{u : (j : J) → (↑((F.obj j).toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)) |
          ∀ {i j : J} (f : i ⟶ j),
            (ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat) ↦ True) ↦
                    C((↑(x1.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)),
                      (↑(x2.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v))))
                    (CC := fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦
                    (↑(X.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v))) (F.map f) :
                  (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type (max u v))) (F.obj i)) →
                    (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type (max u v))) (F.obj j))
                (u i) =
              u j} :
      Type (max u v))
have rw : IsCompact (X := (j : J) → (↑((F.obj j).toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)))
  {u : (j : J) → (↑((F.obj j).toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)) |
    ∀ {i j : J} (f : i ⟶ j),
      (ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat) ↦ True) ↦
              C((↑(x1.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)),
                (↑(x2.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v))))
              (CC := fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦
              (↑(X.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v))) (F.map f) :
            (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type (max u v))) (F.obj i)) →
              (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type (max u v))) (F.obj j))
          (u i) =
        u j}
Tactic: rw [← isCompact_iff_compactSpace]
-- Lean 4 proof step from Mathlib.Topology.Category.CompHaus.Basic (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CompHaus
FF : J ⥤ TopCat := F ⋙ compHausToTop
⊢ IsCompact (X := (j : J) → (↑((F.obj j).toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)))
    {u : (j : J) → (↑((F.obj j).toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)) |
      ∀ {i j : J} (f : i ⟶ j),
        (ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat) ↦ True) ↦
                C((↑(x1.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)),
                  (↑(x2.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v))))
                (CC := fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦
                (↑(X.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v))) (F.map f) :
              (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type (max u v))) (F.obj i)) →
                (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type (max u v))) (F.obj j))
            (u i) =
          u j}
have h : IsClosed (X := (j : J) → (↑((F.obj j).toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)))
  {u : (j : J) → (↑((F.obj j).toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)) |
    ∀ {i j : J} (f : i ⟶ j),
      (ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat) ↦ True) ↦
              C((↑(x1.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)),
                (↑(x2.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v))))
              (CC := fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦
              (↑(X.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v))) (F.map f) :
            (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type (max u v))) (F.obj i)) →
              (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type (max u v))) (F.obj j))
          (u i) =
        u j}
Tactic: apply IsClosed.isCompact
-- Lean 4 proof step from Mathlib.Topology.Category.CompHaus.Basic (hypothesis)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CompHaus
FF : J ⥤ TopCat := F ⋙ compHausToTop
⊢ IsClosed (X := (j : J) → (↑((F.obj j).toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)))
    {u : (j : J) → (↑((F.obj j).toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)) |
      ∀ {i j : J} (f : i ⟶ j),
        (ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat) ↦ True) ↦
                C((↑(x1.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)),
                  (↑(x2.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v))))
                (CC := fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦
                (↑(X.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v))) (F.map f) :
              (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type (max u v))) (F.obj i)) →
                (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type (max u v))) (F.obj j))
            (u i) =
          u j}
have this : Eq (α := Set ((j : J) → (↑((F.obj j).toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v))))
  {u : (j : J) → (↑((F.obj j).toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)) |
    ∀ {i j : J} (f : i ⟶ j),
      (ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat) ↦ True) ↦
              C((↑(x1.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)),
                (↑(x2.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v))))
              (CC := fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦
              (↑(X.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v))) (F.map f) :
            (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type (max u v))) (F.obj i)) →
              (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type (max u v))) (F.obj j))
          (u i) =
        u j}
  (⋂ (i : J),
    ⋂ (j : J),
      ⋂ (f : i ⟶ j),
        {u : (j : J) → (↑((F.obj j).toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)) |
          (ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat) ↦ True) ↦
                  C((↑(x1.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)),
                    (↑(x2.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v))))
                  (CC := fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦
                  (↑(X.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v))) (F.map f) :
                (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type (max u v))) (F.obj i)) →
                  (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type (max u v))) (F.obj j))
              (u i) =
            u j})
Tactic: have :
          { u : ∀ j, F.obj j | ∀ {i j : J} (f : i ⟶ j), F.map f (u i) = u j } =
            ⋂ (i : J) (j : J) (f : i ⟶ j), { u | F.map f (u i) = u j } := by
          ext1
          simp only [Set.mem_iInter, Set.mem_setOf_eq]
-- Lean 4 proof step from Mathlib.Topology.Category.CompHaus.Basic (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CompHaus
FF : J ⥤ TopCat := F ⋙ compHausToTop
S : Limits.Cone F
m : S.pt ⟶ (limitCone.{v, u} F).pt
hm : ∀ (j : J), m ≫ (limitCone.{v, u} F).π.app j = S.π.app j
j : J
⊢ m.hom ≫ (TopCat.limitCone.{v, u, v} FF).π.app j = (compHausToTop.mapCone S).π.app j
have simp : m.hom ≫ (TopCat.limitCone.{v, u, v} FF).π.app j = (m ≫ (limitCone.{v, u} F).π.app j).hom
Tactic: simp [← hm]
-- Lean 4 proof step from Mathlib.Topology.Category.CompHaus.Basic (goal)
Goal:
X Y : CompHaus
f : X ⟶ Y
⊢ Epi f ↔
    Function.Surjective (α :=
      (fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦ (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) X)
      (β :=
      (fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦ (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) Y)
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
            C((↑(x1.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u),
              (↑(x2.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)))
            (CC := fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
            (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) f) :
        (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) X) →
          (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) Y)
have mp : Epi f →
  Function.Surjective (α :=
    (fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦ (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) X)
    (β :=
    (fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦ (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) Y)
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
          C((↑(x1.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u),
            (↑(x2.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)))
          (CC := fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
          (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) f) :
      (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) X) →
        (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) Y)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Category.CompHaus.Basic (goal)
Goal:
X Y : CompHaus
f : X ⟶ Y
mp :
  Epi f →
    Function.Surjective (α :=
      (fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦ (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) X)
      (β :=
      (fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦ (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) Y)
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
            C((↑(x1.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u),
              (↑(x2.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)))
            (CC := fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
            (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) f) :
        (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) X) →
          (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) Y)
⊢ Epi f ↔
    Function.Surjective (α :=
      (fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦ (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) X)
      (β :=
      (fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦ (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) Y)
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
            C((↑(x1.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u),
              (↑(x2.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)))
            (CC := fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
            (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) f) :
        (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) X) →
          (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) Y)
have mpr : Function.Surjective (α :=
    (fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦ (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) X)
    (β :=
    (fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦ (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) Y)
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
          C((↑(x1.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u),
            (↑(x2.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)))
          (CC := fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
          (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) f) :
      (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) X) →
        (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) Y) →
  Epi f
Tactic: constructor