awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Konig (goal)
Goal:
J : Type u
inst : SmallCategory J
F : J ⥤ TopCat
inst_1 : IsCofilteredOrEmpty J
h : ∀ (j : J), Nonempty.{v + 1} (↑(F.obj j) : Type v)
G : Finset J
H : Finset (FiniteDiagramArrow G)
inl : IsEmpty J → (partialSections F H).Nonempty
inr inr₁ : Nonempty J → (partialSections F H).Nonempty
inr₂ : Nonempty J → ∀ (this : IsCofiltered J), (partialSections F H).Nonempty
⊢ (partialSections F H).Nonempty
have h₁ : Nonempty J →
  ∀ (this : IsCofiltered J),
    (fun (j : J) ↦
        if hj : j ∈ G then
          (ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) (X :=
                F.obj (IsCofiltered.inf G H)) (F.map (IsCofiltered.infTo G H hj)) :
              (a : (↑(F.obj (IsCofiltered.inf G H)) : Type v)) → (↑(F.obj j) : Type v))
            (Nonempty.some sorry)
        else sorry.some) ∈
      partialSections F H
Tactic: classical
  cases isEmpty_or_nonempty J
  · exact ⟨isEmptyElim, fun {j} => IsEmpty.elim' inferInstance j.1⟩
  haveI : IsCofiltered J := ⟨⟩
  use fun j : J =>
    if hj : j ∈ G then F.map (IsCofiltered.infTo G H hj) (h (IsCofiltered.inf G H)).some
    else (h _).some
  rintro ⟨X, Y, hX, hY, f⟩ hf
  dsimp only
  rwa [dif_pos hX, dif_pos hY, ← comp_app, ← F.map_comp, @IsCofiltered.infTo_commutes _ _ _ G H]
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Konig (goal)
Goal:
J : Type u
inst : SmallCategory J
F : J ⥤ TopCat
⊢ Directed (α := Set ((j : J) → (↑(F.obj j) : Type v))) Superset fun (G : FiniteDiagram J) ↦
    partialSections F (G.snd (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G)))
have intro : ∀ (A y : FiniteDiagram J),
  ∃ (z : FiniteDiagram J),
    Superset (α := Set ((j : J) → (↑(F.obj j) : Type v)))
        ((fun (G : FiniteDiagram J) ↦
            partialSections F (G.snd (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))))
          A)
        ((fun (G : FiniteDiagram J) ↦
            partialSections F (G.snd (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))))
          z) ∧
      Superset (α := Set ((j : J) → (↑(F.obj j) : Type v)))
        ((fun (G : FiniteDiagram J) ↦
            partialSections F (G.snd (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))))
          y)
        ((fun (G : FiniteDiagram J) ↦
            partialSections F (G.snd (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))))
          z)
Tactic: classical
  intro A B
  let ιA : FiniteDiagramArrow A.1 → FiniteDiagramArrow (A.1 ⊔ B.1) := fun f =>
    ⟨f.1, f.2.1, Finset.mem_union_left _ f.2.2.1, Finset.mem_union_left _ f.2.2.2.1, f.2.2.2.2⟩
  let ιB : FiniteDiagramArrow B.1 → FiniteDiagramArrow (A.1 ⊔ B.1) := fun f =>
    ⟨f.1, f.2.1, Finset.mem_union_right _ f.2.2.1, Finset.mem_union_right _ f.2.2.2.1, f.2.2.2.2⟩
  refine ⟨⟨A.1 ⊔ B.1, A.2.image ιA ⊔ B.2.image ιB⟩, ?_, ?_⟩
  · rintro u hu f hf
    have : ιA f ∈ A.2.image ιA ⊔ B.2.image ιB := by
      apply Finset.mem_union_left
      rw [Finset.mem_image]
      exact ⟨f, hf, rfl⟩
    exact hu this
  · rintro u hu f hf
    have : ιB f ∈ A.2.image ιA ⊔ B.2.image ιB := by
      apply Finset.mem_union_right
      rw [Finset.mem_image]
      exact ⟨f, hf, rfl⟩
    exact hu this
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Konig (goal)
Goal:
J : Type u
inst : SmallCategory J
F : J ⥤ TopCat
inst_1 : IsCofilteredOrEmpty J
inst_2 : ∀ (j : J), Nonempty (↑(F.obj j) : Type (max u v))
inst_3 : ∀ (j : J), CompactSpace (↑(F.obj j) : Type (max u v))
inst_4 : ∀ (j : J), T2Space (↑(F.obj j) : Type (max u v))
⊢ Nonempty (↑(limitCone.{u, v, u} F).pt : Type (max u v))
have obtain : ∀ (u : (j : J) → (↑(F.obj j) : Type (max u v)))
  (hu :
    Membership.mem (γ := Set ((j : J) → (↑(F.obj j) : Type (max u v))))
      (⋂ (i : FiniteDiagram J), partialSections F (i.snd (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G)))) u),
  Nonempty (↑(limitCone.{u, v, u} F).pt : Type (max u v))
Tactic: obtain ⟨u, hu⟩ :=
    IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed (fun G => partialSections F _)
      (partialSections.directed F) (fun G => partialSections.nonempty F _)
      (fun G => IsClosed.isCompact (partialSections.closed F _)) fun G =>
      partialSections.closed F _
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Konig (goal)
Goal:
J : Type u
inst : SmallCategory J
F : J ⥤ TopCat
inst_1 : IsCofilteredOrEmpty J
inst_2 : ∀ (j : J), Nonempty (↑(F.obj j) : Type (max u v))
inst_3 : ∀ (j : J), CompactSpace (↑(F.obj j) : Type (max u v))
inst_4 : ∀ (j : J), T2Space (↑(F.obj j) : Type (max u v))
u : (j : J) → (↑(F.obj j) : Type (max u v))
hu :
  Membership.mem (γ := Set ((j : J) → (↑(F.obj j) : Type (max u v))))
    (⋂ (i : FiniteDiagram J), partialSections F (i.snd (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G)))) u
⊢ Nonempty (↑(limitCone.{u, v, u} F).pt : Type (max u v))
have property : Membership.mem (γ := Set ((j : J) → (↑(F.obj j) : Type (max v u))))
  {u : (j : J) → (↑(F.obj j) : Type (max v u)) |
    ∀ {i j : J} (f : i ⟶ j),
      (ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max v u)), (↑Y : Type (max v u)))) (CC := carrier)
              (F.map f) :
            (a : (↑(F.obj i) : Type (max v u))) → (↑(F.obj j) : Type (max v u)))
          (u i) =
        u j}
  u
Tactic: use u
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Konig (goal)
Goal:
J : Type u
inst : SmallCategory J
F : J ⥤ TopCat
inst_1 : IsCofilteredOrEmpty J
inst_2 : ∀ (j : J), Nonempty (↑(F.obj j) : Type (max u v))
inst_3 : ∀ (j : J), CompactSpace (↑(F.obj j) : Type (max u v))
inst_4 : ∀ (j : J), T2Space (↑(F.obj j) : Type (max u v))
⊢ Nonempty (↑(limitCone.{u, v, u} F).pt : Type (max u v))
have obtain : ∀ (u : (j : J) → (↑(F.obj j) : Type (max u v)))
  (hu :
    Membership.mem (γ := Set ((j : J) → (↑(F.obj j) : Type (max u v))))
      (⋂ (i : FiniteDiagram J), partialSections F (i.snd (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G)))) u),
  Nonempty (↑(limitCone.{u, v, u} F).pt : Type (max u v))
Tactic: classical
  obtain ⟨u, hu⟩ :=
    IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed (fun G => partialSections F _)
      (partialSections.directed F) (fun G => partialSections.nonempty F _)
      (fun G => IsClosed.isCompact (partialSections.closed F _)) fun G =>
      partialSections.closed F _
  use u
  intro X Y f
  let G : FiniteDiagram J := ⟨{X, Y}, {⟨X, Y, by grind, by grind, f⟩}⟩
  exact hu _ ⟨G, rfl⟩ (Finset.mem_singleton_self _)
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Konig (goal)
Goal:
J : Type u
inst : SmallCategory J
F : J ⥤ TopCat
inst_1 : IsCofilteredOrEmpty J
inst_2 : ∀ (j : J), Nonempty (↑(F.obj j) : Type (max u v))
inst_3 : ∀ (j : J), CompactSpace (↑(F.obj j) : Type (max u v))
inst_4 : ∀ (j : J), T2Space (↑(F.obj j) : Type (max u v))
obtain :
  ∀ (u : (j : J) → (↑(F.obj j) : Type (max u v)))
    (hu :
      Membership.mem (γ := Set ((j : J) → (↑(F.obj j) : Type (max u v))))
        (⋂ (i : FiniteDiagram J), partialSections F (i.snd (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))))
        u),
    Nonempty (↑(limitCone.{u, v, u} F).pt : Type (max u v))
⊢ Nonempty (↑(limitCone.{u, v, u} F).pt : Type (max u v))
have property : ∀ (u : (j : J) → (↑(F.obj j) : Type (max u v)))
  (hu :
    Membership.mem (γ := Set ((j : J) → (↑(F.obj j) : Type (max u v))))
      (⋂ (i : FiniteDiagram J), partialSections F (i.snd (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G)))) u),
  Membership.mem (γ := Set ((j : J) → (↑(F.obj j) : Type (max v u))))
    {u : (j : J) → (↑(F.obj j) : Type (max v u)) |
      ∀ {i j : J} (f : i ⟶ j),
        (ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max v u)), (↑Y : Type (max v u)))) (CC :=
                carrier) (F.map f) :
              (a : (↑(F.obj i) : Type (max v u))) → (↑(F.obj j) : Type (max v u)))
            (u i) =
          u j}
    u
Tactic: classical
  obtain ⟨u, hu⟩ :=
    IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed (fun G => partialSections F _)
      (partialSections.directed F) (fun G => partialSections.nonempty F _)
      (fun G => IsClosed.isCompact (partialSections.closed F _)) fun G =>
      partialSections.closed F _
  use u
  intro X Y f
  let G : FiniteDiagram J := ⟨{X, Y}, {⟨X, Y, by grind, by grind, f⟩}⟩
  exact hu _ ⟨G, rfl⟩ (Finset.mem_singleton_self _)
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Konig (goal)
Goal:
J : Type u
inst : SmallCategory J
F : J ⥤ TopCat
inst_1 : IsCofilteredOrEmpty J
inst_2 : ∀ (j : J), Nonempty (↑(F.obj j) : Type (max u v))
inst_3 : ∀ (j : J), CompactSpace (↑(F.obj j) : Type (max u v))
inst_4 : ∀ (j : J), T2Space (↑(F.obj j) : Type (max u v))
obtain :
  ∀ (u : (j : J) → (↑(F.obj j) : Type (max u v)))
    (hu :
      Membership.mem (γ := Set ((j : J) → (↑(F.obj j) : Type (max u v))))
        (⋂ (i : FiniteDiagram J), partialSections F (i.snd (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))))
        u),
    Nonempty (↑(limitCone.{u, v, u} F).pt : Type (max u v))
property :
  ∀ (u : (j : J) → (↑(F.obj j) : Type (max u v)))
    (hu :
      Membership.mem (γ := Set ((j : J) → (↑(F.obj j) : Type (max u v))))
        (⋂ (i : FiniteDiagram J), partialSections F (i.snd (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))))
        u),
    Membership.mem (γ := Set ((j : J) → (↑(F.obj j) : Type (max v u))))
      {u : (j : J) → (↑(F.obj j) : Type (max v u)) |
        ∀ {i j : J} (f : i ⟶ j),
          (ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max v u)), (↑Y : Type (max v u)))) (CC :=
                  carrier) (F.map f) :
                (a : (↑(F.obj i) : Type (max v u))) → (↑(F.obj j) : Type (max v u)))
              (u i) =
            u j}
      u
⊢ Nonempty (↑(limitCone.{u, v, u} F).pt : Type (max u v))
have property₁ : ∀ (u : (j : J) → (↑(F.obj j) : Type (max u v)))
  (hu :
    Membership.mem (γ := Set ((j : J) → (↑(F.obj j) : Type (max u v))))
      (⋂ (i : FiniteDiagram J), partialSections F (i.snd (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G)))) u)
  {X Y : J} (f : X ⟶ Y),
  (ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max v u)), (↑Y : Type (max v u)))) (CC := carrier)
          (F.map f) :
        (a : (↑(F.obj X) : Type (max v u))) → (↑(F.obj Y) : Type (max v u)))
      (u X) =
    u Y
Tactic: classical
  obtain ⟨u, hu⟩ :=
    IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed (fun G => partialSections F _)
      (partialSections.directed F) (fun G => partialSections.nonempty F _)
      (fun G => IsClosed.isCompact (partialSections.closed F _)) fun G =>
      partialSections.closed F _
  use u
  intro X Y f
  let G : FiniteDiagram J := ⟨{X, Y}, {⟨X, Y, by grind, by grind, f⟩}⟩
  exact hu _ ⟨G, rfl⟩ (Finset.mem_singleton_self _)
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Products (goal)
Goal:
J : Type v
inst : Category.{w, v} J
ι : Type v
α : ι → TopCat
S : Cone (Discrete.functor α)
m : S.pt ⟶ (piFan.{v, u} α).pt
h : ∀ (j : Discrete ι), m ≫ (piFan.{v, u} α).π.app j = S.π.app j
⊢ m =
    ofHom
      {
        toFun := fun (s : (↑S.1 : Type (max u v))) (i : ι) ↦
          (ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC :=
                carrier) (X := Functor.obj (Functor.obj (Functor.const (Discrete ι)) S.pt) { as := i : Discrete ι })
                (S.π.app { as := i }) :
              (a : (↑(((Functor.const (Discrete ι)).obj S.pt).obj { as := i }) : Type (max u v))) →
                (↑((Discrete.functor α).obj { as := i }) : Type (max u v)))
            s,
        continuous_toFun := ⋯ }
have w : ∀ (x : (↑S.pt : Type (max u v))),
  Eq (α := (↑(piFan.{v, u} α).pt : Type (max u v)))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC := carrier)
            m :
          (a : (↑S.pt : Type (max u v))) → (↑(piFan α).pt : Type (max u v)))
        x :
      (↑(piFan.{v, u} α).pt : Type (max u v)))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC := carrier)
            (X := S.pt) (Y := (piFan.{v, u} α).pt)
            (ofHom
              {
                toFun := fun (s : (↑S.1 : Type (max u v))) (i : ι) ↦
                  (ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v))))
                        (CC := carrier) (X :=
                        Functor.obj (Functor.obj (Functor.const (Discrete ι)) S.pt) { as := i : Discrete ι })
                        (S.π.app { as := i }) :
                      (a : (↑(((Functor.const (Discrete ι)).obj S.pt).obj { as := i }) : Type (max u v))) →
                        (↑((Discrete.functor α).obj { as := i }) : Type (max u v)))
                    s,
                continuous_toFun := sorry }) :
          (a : (↑S.pt : Type (max u v))) → (↑(piFan α).pt : Type (max u v)))
        x :
      (↑(piFan.{v, u} α).pt : Type (max u v)))
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Products (goal)
Goal:
J : Type v
inst : Category.{w, v} J
ι : Type v
α : ι → TopCat
S : Cone (Discrete.functor α)
m : S.pt ⟶ (piFan.{v, u} α).pt
h : ∀ (j : Discrete ι), m ≫ (piFan.{v, u} α).π.app j = S.π.app j
x : (↑S.pt : Type (max u v))
⊢ Eq (α := (↑(piFan.{v, u} α).pt : Type (max u v)))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC := carrier)
            m :
          (a : (↑S.pt : Type (max u v))) → (↑(piFan α).pt : Type (max u v)))
        x :
      (↑(piFan.{v, u} α).pt : Type (max u v)))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC := carrier)
            (X := S.pt) (Y := (piFan.{v, u} α).pt)
            (ofHom
              {
                toFun := fun (s : (↑S.1 : Type (max u v))) (i : ι) ↦
                  (ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v))))
                        (CC := carrier) (X :=
                        Functor.obj (Functor.obj (Functor.const (Discrete ι)) S.pt) { as := i : Discrete ι })
                        (S.π.app { as := i }) :
                      (a : (↑(((Functor.const (Discrete ι)).obj S.pt).obj { as := i }) : Type (max u v))) →
                        (↑((Discrete.functor α).obj { as := i }) : Type (max u v)))
                    s,
                continuous_toFun := ⋯ }) :
          (a : (↑S.pt : Type (max u v))) → (↑(piFan α).pt : Type (max u v)))
        x :
      (↑(piFan.{v, u} α).pt : Type (max u v)))
have w : ∀ (i : ι),
  Eq (α := (↑(α i) : Type (max u v)))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC := carrier)
            m :
          (a : (↑S.pt : Type (max u v))) → (↑(piFan α).pt : Type (max u v)))
        x i :
      (↑(α i) : Type (max u v)))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC := carrier)
            (X := S.pt) (Y := (piFan.{v, u} α).pt)
            (ofHom
              {
                toFun := fun (s : (↑S.1 : Type (max u v))) (i : ι) ↦
                  (ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v))))
                        (CC := carrier) (X :=
                        Functor.obj (Functor.obj (Functor.const (Discrete ι)) S.pt) { as := i : Discrete ι })
                        (S.π.app { as := i }) :
                      (a : (↑(((Functor.const (Discrete ι)).obj S.pt).obj { as := i }) : Type (max u v))) →
                        (↑((Discrete.functor α).obj { as := i }) : Type (max u v)))
                    s,
                continuous_toFun := sorry }) :
          (a : (↑S.pt : Type (max u v))) → (↑(piFan α).pt : Type (max u v)))
        x i :
      (↑(α i) : Type (max u v)))
Tactic: funext i
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Products (goal)
Goal:
J : Type v
inst : Category.{w, v} J
ι : Type v
α : ι → TopCat
i : ι
⊢ α i ⟶ of ((i : ι) × (↑(α i) : Type (max u v)))
have refine_1 : (↑(α i) : Type (max u v)) → (i : ι) × (↑(α i) : Type (max u v))
Tactic: refine ofHom (ContinuousMap.mk ?_ ?_)
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Products (goal)
Goal:
J : Type v
inst : Category.{w, v} J
ι : Type v
α : ι → TopCat
i : ι
refine_1 : (↑(α i) : Type (max u v)) → (i : ι) × (↑(α i) : Type (max u v))
⊢ α i ⟶ of ((i : ι) × (↑(α i) : Type (max u v)))
have refine_2 : Continuous (X := (↑(α i) : Type (max u v))) (Y := (i : ι) × (↑(α i) : Type (max u v)))
  (id (Sigma.mk (β := fun (i : ι) ↦ (↑(α i) : Type (max u v))) i))
Tactic: refine ofHom (ContinuousMap.mk ?_ ?_)
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Products (goal)
Goal:
J : Type v
inst : Category.{w, v} J
ι : Type v
β : ι → TopCat
s : Cocone (Discrete.functor β)
j : Discrete ι
⊢ (sigmaCofan.{v, u} β).ι.app j ≫
      ofHom
        {
          toFun := fun (s_1 : (↑(of ((i : ι) × (↑(β i) : Type (max u v)))) : Type (max u v))) ↦
            (ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC :=
                  carrier) (X :=
                  Functor.obj (Discrete.functor β)
                    { as := s_1.fst (β := fun (i : ι) ↦ (↑(β i) : Type (max u v))) : Discrete ι })
                  (s.ι.app { as := s_1.fst (β := fun (i : ι) ↦ (↑(β i) : Type (max u v))) : Discrete ι }) :
                (a : (↑((Discrete.functor β).obj { as := s_1.fst }) : Type (max u v))) →
                  (↑(((Functor.const (Discrete ι)).obj s.pt).obj { as := s_1.fst }) : Type (max u v)))
              (s_1.snd (β := fun (i : ι) ↦ (↑(β i) : Type (max u v)))),
          continuous_toFun := ⋯ : C((i : ι) × (↑(β i) : Type (max u v)), (↑s.1 : Type (max u v))) } =
    s.ι.app j
have mk : ∀ (as : ι),
  Eq (α := Functor.obj (Discrete.functor β) { as := as : Discrete ι } ⟶ s.pt)
    ((sigmaCofan.{v, u} β).ι.app { as := as } ≫
      ofHom
        {
          toFun := fun (s_1 : (↑(of ((i : ι) × (↑(β i) : Type (max u v)))) : Type (max u v))) ↦
            (ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC :=
                  carrier) (X :=
                  Functor.obj (Discrete.functor β)
                    { as := s_1.fst (β := fun (i : ι) ↦ (↑(β i) : Type (max u v))) : Discrete ι })
                  (s.ι.app { as := s_1.fst (β := fun (i : ι) ↦ (↑(β i) : Type (max u v))) : Discrete ι }) :
                (a : (↑((Discrete.functor β).obj { as := s_1.fst }) : Type (max u v))) →
                  (↑(((Functor.const (Discrete ι)).obj s.pt).obj { as := s_1.fst }) : Type (max u v)))
              (s_1.snd (β := fun (i : ι) ↦ (↑(β i) : Type (max u v)))),
          continuous_toFun := sorry : C((i : ι) × (↑(β i) : Type (max u v)), (↑s.1 : Type (max u v))) })
    (s.ι.app { as := as })
Tactic: cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Products (goal)
Goal:
J : Type v
inst : Category.{w, v} J
ι : Type v
β : ι → TopCat
S : Cocone (Discrete.functor β)
m : (sigmaCofan.{v, u} β).pt ⟶ S.pt
h : ∀ (j : Discrete ι), (sigmaCofan.{v, u} β).ι.app j ≫ m = S.ι.app j
⊢ m =
    ofHom
      {
        toFun := fun (s : (↑(of ((i : ι) × (↑(β i) : Type (max u v)))) : Type (max u v))) ↦
          (ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC :=
                carrier) (X :=
                Functor.obj (Discrete.functor β)
                  { as := s.fst (β := fun (i : ι) ↦ (↑(β i) : Type (max u v))) : Discrete ι })
                (S.ι.app { as := s.fst (β := fun (i : ι) ↦ (↑(β i) : Type (max u v))) }) :
              (a : (↑((Discrete.functor β).obj { as := s.fst }) : Type (max u v))) →
                (↑(((Functor.const (Discrete ι)).obj S.pt).obj { as := s.fst }) : Type (max u v)))
            (s.snd (β := fun (i : ι) ↦ (↑(β i) : Type (max u v)))),
        continuous_toFun := ⋯ }
have w : ∀ (i : ι) (x : (↑(β i) : Type (max u v))),
  Eq (α := (↑S.pt : Type (max u v)))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC := carrier)
            m :
          (a : (↑(sigmaCofan β).pt : Type (max u v))) → (↑S.pt : Type (max u v)))
        (Sigma.mk (β := fun (i : ι) ↦ (↑(β i) : Type (max u v))) i x) :
      (↑S.pt : Type (max u v)))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC := carrier)
            (ofHom
              {
                toFun := fun (s : (↑(of ((i : ι) × (↑(β i) : Type (max u v)))) : Type (max u v))) ↦
                  (ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v))))
                        (CC := carrier) (X :=
                        Functor.obj (Discrete.functor β)
                          { as := s.fst (β := fun (i : ι) ↦ (↑(β i) : Type (max u v))) : Discrete ι })
                        (S.ι.app { as := s.fst (β := fun (i : ι) ↦ (↑(β i) : Type (max u v))) : Discrete ι }) :
                      (a : (↑((Discrete.functor β).obj { as := s.fst }) : Type (max u v))) →
                        (↑(((Functor.const (Discrete ι)).obj S.pt).obj { as := s.fst }) : Type (max u v)))
                    (s.snd (β := fun (i : ι) ↦ (↑(β i) : Type (max u v)))),
                continuous_toFun := sorry : C((i : ι) × (↑(β i) : Type (max u v)), (↑S.1 : Type (max u v))) }) :
          (a : (↑(sigmaCofan β).pt : Type (max u v))) → (↑S.pt : Type (max u v)))
        (Sigma.mk (β := fun (i : ι) ↦ (↑(β i) : Type (max u v))) i x) :
      (↑S.pt : Type (max u v)))
Tactic: ext ⟨i, x⟩
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Products (goal)
Goal:
ι : Type v
α : ι → TopCat
i : ι
x : (↑(α i) : Type (max u v))
⊢ Eq (α := (↑(∐ α) : Type (max v u)))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max v u)), (↑Y : Type (max v u)))) (CC := carrier)
            (sigmaIsoSigma.{v, u} α).inv :
          (a : (↑(of ((i : ι) × (↑(α i) : Type (max u v)))) : Type (max v u))) → (↑(∐ α) : Type (max v u)))
        (Sigma.mk (β := fun (i : ι) ↦ (↑(α i) : Type (max u v))) i x) :
      (↑(∐ α) : Type (max v u)))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC := carrier)
            (Y := ∐ α) (Sigma.ι α i) :
          (a : (↑(α i) : Type (max u v))) → (↑(∐ α) : Type (max u v)))
        x :
      (↑(∐ α) : Type (max u v)))
have rw : Eq (α := (↑(∐ α) : Type (max v u)))
  ((ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max v u)), (↑Y : Type (max v u)))) (CC := carrier)
          (sigmaIsoSigma.{v, u} α).inv :
        (a : (↑(of ((i : ι) × (↑(α i) : Type (max u v)))) : Type (max v u))) → (↑(∐ α) : Type (max v u)))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max v u)), (↑Y : Type (max v u)))) (CC :=
            carrier) (sigmaIsoSigma.{v, u} α).hom :
          (a : (↑(∐ α) : Type (max v u))) → (↑(of ((i : ι) × (↑(α i) : Type (max u v)))) : Type (max v u)))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC :=
              carrier) (Y := ∐ α) (Sigma.ι α i) :
            (a : (↑(α i) : Type (max u v))) → (↑(∐ α) : Type (max u v)))
          x)) :
    (↑(∐ α) : Type (max v u)))
  ((ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC := carrier)
          (Y := ∐ α) (Sigma.ι α i) :
        (a : (↑(α i) : Type (max u v))) → (↑(∐ α) : Type (max u v)))
      x :
    (↑(∐ α) : Type (max u v)))
Tactic: rw [← sigmaIsoSigma_hom_ι_apply, ← comp_app, ← comp_app, Iso.hom_inv_id,
    Category.comp_id]