awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Products (hypothesis)
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
inst_1 : Unique β
f : β → C
s : Cone.{w, v, w, u} (Discrete.functor f)
m :
  s.pt ⟶
    Cone.pt.{w, v, w, u} (J := Discrete β) (F := Discrete.functor f)
      { pt := f default,
        π :=
          Discrete.natTrans fun (x : Discrete β) ↦
            match (motive :=
              (x : Discrete β) →
                Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (Discrete β)) (f default)) x ⟶
                  Functor.obj.{w, v, w, u} (Discrete.functor f) x)
              x with
            | { as := j } => eqToHom ⋯ }
w :
  ∀ (j : Discrete β),
    m ≫
        NatTrans.app
          (Cone.π
            { pt := f default,
              π :=
                Discrete.natTrans fun (x : Discrete β) ↦
                  match (motive :=
                    (x : Discrete β) →
                      Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (Discrete β)) (f default)) x ⟶
                        Functor.obj.{w, v, w, u} (Discrete.functor f) x)
                    x with
                  | { as := j } => eqToHom ⋯ })
          j =
      s.π.app j
⊢ m = s.π.app default
have w₁ : Eq (α := s.pt ⟶ Functor.obj.{w, v, w, u} (Discrete.functor f) default)
  (m ≫
    NatTrans.app
      (Cone.π
        { pt := f default,
          π :=
            Discrete.natTrans fun (x : Discrete β) ↦
              match (motive :=
                (x : Discrete β) →
                  Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (Discrete β)) (f default)) x ⟶
                    Functor.obj.{w, v, w, u} (Discrete.functor f) x)
                x with
              | { as := j } => eqToHom sorry })
      default)
  (s.π.app default)
Tactic: specialize w default
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Products (goal)
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
X Y : C
e : X ≅ Y
J : Type u_1
inst_1 : Unique J
⊢ IsLimit.{u_1, v, u_1, u} (J := Discrete J) (F := Discrete.functor fun (x : J) ↦ Y) (mk X fun (x : J) ↦ e.hom)
have refine_1 : ∀ (s : Fan.{u_1, v, u} (C := C) fun (x : J) ↦ Y) (j : J),
  CategoryStruct.comp (Y :=
      Cone.pt.{u_1, v, u_1, u} (J := Discrete J) (F := Discrete.functor fun (x : J) ↦ Y) (mk X fun (x : J) ↦ e.hom))
      ((fun (s : Fan.{u_1, v, u} (C := C) fun (x : J) ↦ Y) ↦ s.proj default ≫ e.inv) s)
      (proj (mk X fun (x : J) ↦ e.hom) j) =
    s.proj j
Tactic: refine Fan.IsLimit.mk _ (fun s ↦ s.proj default ≫ e.inv) (fun s j ↦ ?_) fun s m hm ↦ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Products (goal)
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
X Y : C
e : X ≅ Y
J : Type u_1
inst_1 : Unique J
refine_1 :
  ∀ (s : Fan.{u_1, v, u} (C := C) fun (x : J) ↦ Y) (j : J),
    CategoryStruct.comp (Y :=
        Cone.pt.{u_1, v, u_1, u} (J := Discrete J) (F := Discrete.functor fun (x : J) ↦ Y) (mk X fun (x : J) ↦ e.hom))
        ((fun (s : Fan.{u_1, v, u} (C := C) fun (x : J) ↦ Y) ↦ s.proj default ≫ e.inv) s)
        (proj (mk X fun (x : J) ↦ e.hom) j) =
      s.proj j
⊢ IsLimit.{u_1, v, u_1, u} (J := Discrete J) (F := Discrete.functor fun (x : J) ↦ Y) (mk X fun (x : J) ↦ e.hom)
have refine_2 : ∀ (s : Fan.{u_1, v, u} (C := C) fun (x : J) ↦ Y)
  (m :
    s.pt ⟶
      Cone.pt.{u_1, v, u_1, u} (J := Discrete J) (F := Discrete.functor fun (x : J) ↦ Y) (mk X fun (x : J) ↦ e.hom))
  (hm : ∀ (j : J), m ≫ proj (mk X fun (x : J) ↦ e.hom) j = s.proj j),
  m = (fun (s : Fan.{u_1, v, u} (C := C) fun (x : J) ↦ Y) ↦ s.proj default ≫ e.inv) s
Tactic: refine Fan.IsLimit.mk _ (fun s ↦ s.proj default ≫ e.inv) (fun s j ↦ ?_) fun s m hm ↦ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Products (goal)
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
X Y : C
e : X ≅ Y
J : Type u_1
inst_1 : Unique J
s : Fan.{u_1, v, u} (C := C) fun (x : J) ↦ Y
j : J
⊢ CategoryStruct.comp (Y :=
      Cone.pt.{u_1, v, u_1, u} (J := Discrete J) (F := Discrete.functor fun (x : J) ↦ Y) (mk X fun (x : J) ↦ e.hom))
      ((fun (s : Fan.{u_1, v, u} (C := C) fun (x : J) ↦ Y) ↦ s.proj default ≫ e.inv) s)
      (proj (mk X fun (x : J) ↦ e.hom) j) =
    s.proj j
have refine_1 : CategoryStruct.comp (Y :=
    Cone.pt.{u_1, v, u_1, u} (J := Discrete J) (F := Discrete.functor fun (x : J) ↦ Y) (mk X fun (x : J) ↦ e.hom))
    ((fun (s : Fan.{u_1, v, u} (C := C) fun (x : J) ↦ Y) ↦ s.proj default ≫ e.inv) s)
    (proj (mk X fun (x : J) ↦ e.hom) default) =
  s.proj default
Tactic: obtain rfl : j = default := Subsingleton.elim _ _
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Products (goal)
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
inst_1 : Unique β
f : β → C
x : Discrete β
j : β
⊢ Functor.obj.{w, v, w, u} (Discrete.functor f) { as := j : Discrete β } =
    Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (Discrete β)) (f default)) { as := j : Discrete β }
have dsimp : f j = f default
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Products (goal)
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
inst_1 : Unique β
f : β → C
x : Discrete β
j : β
⊢ f j = f default
have e_a : j = default
Tactic: congr
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Products (goal)
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
inst_1 : Unique β
f : β → C
s : Cocone.{w, v, w, u} (Discrete.functor f)
j : Discrete β
⊢ CategoryStruct.comp (Y :=
      Functor.obj.{w, v, w, u}
        (Functor.obj (Functor.const (Discrete β))
          (Cocone.pt.{w, v, w, u} (J := Discrete β) (F := Discrete.functor f)
            { pt := f default,
              ι :=
                Discrete.natTrans fun (x : Discrete β) ↦
                  match (motive :=
                    (x : Discrete β) →
                      Functor.obj.{w, v, w, u} (Discrete.functor f) x ⟶
                        Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (Discrete β)) (f default)) x)
                    x with
                  | { as := j } => eqToHom ⋯ :
              Cocone.{w, v, w, u} (Discrete.functor f) }))
        j)
      (NatTrans.app
        (Cocone.ι
          { pt := f default,
            ι :=
              Discrete.natTrans fun (x : Discrete β) ↦
                match (motive :=
                  (x : Discrete β) →
                    Functor.obj.{w, v, w, u} (Discrete.functor f) x ⟶
                      Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (Discrete β)) (f default)) x)
                  x with
                | { as := j } => eqToHom ⋯ })
        j)
      (s.ι.app default) =
    s.ι.app j
have obtain : Eq (α := Functor.obj.{w, v, w, u} (Discrete.functor f) default ⟶ s.pt)
  (CategoryStruct.comp (Y :=
    Functor.obj.{w, v, w, u} (C := Discrete β)
      (Functor.obj (Functor.const (Discrete β))
        (Cocone.pt.{w, v, w, u} (J := Discrete β) (F := Discrete.functor f)
          { pt := f default,
            ι :=
              Discrete.natTrans fun (x : Discrete β) ↦
                match (motive :=
                  (x : Discrete β) →
                    Functor.obj.{w, v, w, u} (Discrete.functor f) x ⟶
                      Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (Discrete β)) (f default)) x)
                  x with
                | { as := j } => eqToHom sorry :
            Cocone.{w, v, w, u} (Discrete.functor f) }))
      default)
    (NatTrans.app
      (Cocone.ι
        { pt := f default,
          ι :=
            Discrete.natTrans fun (x : Discrete β) ↦
              match (motive :=
                (x : Discrete β) →
                  Functor.obj.{w, v, w, u} (Discrete.functor f) x ⟶
                    Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (Discrete β)) (f default)) x)
                x with
              | { as := j } => eqToHom sorry })
      default)
    (s.ι.app default))
  (s.ι.app default)
Tactic: obtain rfl := Subsingleton.elim j default
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Products (hypothesis)
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
inst_1 : Unique β
f : β → C
s : Cocone.{w, v, w, u} (Discrete.functor f)
m :
  Cocone.pt.{w, v, w, u} (J := Discrete β) (F := Discrete.functor f)
      { pt := f default,
        ι :=
          Discrete.natTrans fun (x : Discrete β) ↦
            match (motive :=
              (x : Discrete β) →
                Functor.obj.{w, v, w, u} (Discrete.functor f) x ⟶
                  Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (Discrete β)) (f default)) x)
              x with
            | { as := j } => eqToHom ⋯ :
        Cocone.{w, v, w, u} (Discrete.functor f) } ⟶
    s.pt
w :
  ∀ (j : Discrete β),
    NatTrans.app
          (Cocone.ι
            { pt := f default,
              ι :=
                Discrete.natTrans fun (x : Discrete β) ↦
                  match (motive :=
                    (x : Discrete β) →
                      Functor.obj.{w, v, w, u} (Discrete.functor f) x ⟶
                        Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (Discrete β)) (f default)) x)
                    x with
                  | { as := j } => eqToHom ⋯ })
          j ≫
        m =
      s.ι.app j
⊢ m = s.ι.app default
have w₁ : Eq (α := Functor.obj.{w, v, w, u} (Discrete.functor f) default ⟶ s.pt)
  (NatTrans.app
      (Cocone.ι
        { pt := f default,
          ι :=
            Discrete.natTrans fun (x : Discrete β) ↦
              match (motive :=
                (x : Discrete β) →
                  Functor.obj.{w, v, w, u} (Discrete.functor f) x ⟶
                    Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (Discrete β)) (f default)) x)
                x with
              | { as := j } => eqToHom sorry })
      default ≫
    m)
  (s.ι.app default)
Tactic: specialize w default
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Products (goal)
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
X Y : C
e : X ≅ Y
J : Type u_1
inst_1 : Unique J
⊢ IsColimit.{u_1, v, u_1, u} (J := Discrete J) (F := Discrete.functor fun (x : J) ↦ X) (mk Y fun (x : J) ↦ e.hom)
have refine_1 : ∀ (s : Cofan.{u_1, v, u} (C := C) fun (x : J) ↦ X) (j : J),
  CategoryStruct.comp (Y :=
      Cocone.pt.{u_1, v, u_1, u} (J := Discrete J) (F := Discrete.functor fun (x : J) ↦ X) (mk Y fun (x : J) ↦ e.hom))
      (inj.{u_1, v, u} (f := fun (x : J) ↦ X) (mk Y fun (x : J) ↦ e.hom) j)
      ((fun (s : Cofan.{u_1, v, u} (C := C) fun (x : J) ↦ X) ↦ e.inv ≫ s.inj default) s) =
    s.inj j
Tactic: refine Cofan.IsColimit.mk _ (fun s ↦ e.inv ≫ s.inj default) (fun s j ↦ ?_) fun s m hm ↦ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Products (goal)
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
X Y : C
e : X ≅ Y
J : Type u_1
inst_1 : Unique J
refine_1 :
  ∀ (s : Cofan.{u_1, v, u} (C := C) fun (x : J) ↦ X) (j : J),
    CategoryStruct.comp (Y :=
        Cocone.pt.{u_1, v, u_1, u} (J := Discrete J) (F := Discrete.functor fun (x : J) ↦ X) (mk Y fun (x : J) ↦ e.hom))
        (inj.{u_1, v, u} (f := fun (x : J) ↦ X) (mk Y fun (x : J) ↦ e.hom) j)
        ((fun (s : Cofan.{u_1, v, u} (C := C) fun (x : J) ↦ X) ↦ e.inv ≫ s.inj default) s) =
      s.inj j
⊢ IsColimit.{u_1, v, u_1, u} (J := Discrete J) (F := Discrete.functor fun (x : J) ↦ X) (mk Y fun (x : J) ↦ e.hom)
have refine_2 : ∀ (s : Cofan.{u_1, v, u} (C := C) fun (x : J) ↦ X)
  (m :
    Cocone.pt.{u_1, v, u_1, u} (J := Discrete J) (F := Discrete.functor fun (x : J) ↦ X) (mk Y fun (x : J) ↦ e.hom) ⟶
      s.pt)
  (hm : ∀ (j : J), inj.{u_1, v, u} (f := fun (x : J) ↦ X) (mk Y fun (x : J) ↦ e.hom) j ≫ m = s.inj j),
  m = (fun (s : Cofan.{u_1, v, u} (C := C) fun (x : J) ↦ X) ↦ e.inv ≫ s.inj default) s
Tactic: refine Cofan.IsColimit.mk _ (fun s ↦ e.inv ≫ s.inj default) (fun s j ↦ ?_) fun s m hm ↦ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Products (goal)
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
X Y : C
e : X ≅ Y
J : Type u_1
inst_1 : Unique J
s : Cofan.{u_1, v, u} (C := C) fun (x : J) ↦ X
j : J
⊢ CategoryStruct.comp (Y :=
      Cocone.pt.{u_1, v, u_1, u} (J := Discrete J) (F := Discrete.functor fun (x : J) ↦ X) (mk Y fun (x : J) ↦ e.hom))
      (inj.{u_1, v, u} (f := fun (x : J) ↦ X) (mk Y fun (x : J) ↦ e.hom) j)
      ((fun (s : Cofan.{u_1, v, u} (C := C) fun (x : J) ↦ X) ↦ e.inv ≫ s.inj default) s) =
    s.inj j
have refine_1 : CategoryStruct.comp (Y :=
    Cocone.pt.{u_1, v, u_1, u} (J := Discrete J) (F := Discrete.functor fun (x : J) ↦ X) (mk Y fun (x : J) ↦ e.hom))
    (inj.{u_1, v, u} (β := J) (f := fun (x : J) ↦ X) (mk Y fun (x : J) ↦ e.hom) default)
    ((fun (s : Cofan.{u_1, v, u} (C := C) fun (x : J) ↦ X) ↦ e.inv ≫ s.inj default) s) =
  s.inj default
Tactic: obtain rfl : j = default := Subsingleton.elim _ _
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Products (goal)
Goal:
β : Type w
C : Type u
inst : Category.{v, u} C
γ : Type w'
ε : β ≃ γ
f : γ → C
inst_1 : HasProduct.{w', v, u} f
inst_2 : HasProduct.{w, v, u} (β := β) (f ∘ (⇑ε : (a : β) → γ))
b : β
⊢ Eq.{v + 1} (α := piObj.{w, v, u} (β := β) (f ∘ (⇑ε : (a : β) → γ)) ⟶ f ((ε : (a : β) → γ) b))
    (CategoryStruct.comp (Y := piObj.{w', v, u} f) (Iso.hom (reindex ε f)) (π f ((ε : (a : β) → γ) b)))
    (π (f ∘ (⇑ε : (a : β) → γ)) b)
have dsimp : Eq.{v + 1} (α := piObj.{w, v, u} (β := β) (f ∘ (⇑ε : (a : β) → γ)) ⟶ f ((ε : (a : β) → γ) b))
  (CategoryStruct.comp (Y := piObj.{w', v, u} f)
    (Iso.hom
      (HasLimit.isoOfEquivalence (Discrete.equivalence ε)
        (Discrete.natIso fun (x : Discrete β) ↦ Iso.refl (f ((ε : (a : β) → γ) x.as)))))
    (π f ((ε : (a : β) → γ) b)))
  (π (f ∘ (⇑ε : (a : β) → γ)) b)
Tactic: dsimp [Pi.reindex]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Products (goal)
Goal:
β : Type w
C : Type u
inst : Category.{v, u} C
γ : Type w'
ε : β ≃ γ
f : γ → C
inst_1 : HasProduct.{w', v, u} f
inst_2 : HasProduct.{w, v, u} (β := β) (f ∘ (⇑ε : (a : β) → γ))
b : β
⊢ Eq.{v + 1} (α := piObj.{w, v, u} (β := β) (f ∘ (⇑ε : (a : β) → γ)) ⟶ f ((ε : (a : β) → γ) b))
    (CategoryStruct.comp (Y := piObj.{w', v, u} f)
      (Iso.hom
        (HasLimit.isoOfEquivalence (Discrete.equivalence ε)
          (Discrete.natIso fun (x : Discrete β) ↦ Iso.refl (f ((ε : (a : β) → γ) x.as)))))
      (π f ((ε : (a : β) → γ) b)))
    (π (f ∘ (⇑ε : (a : β) → γ)) b)
have simp : Eq.{v + 1} (α := piObj.{w, v, u} (β := β) (f ∘ (⇑ε : (a : β) → γ)) ⟶ f ((ε : (a : β) → γ) b))
  (CategoryStruct.comp (Y := f ((ε : (a : β) → γ) ((ε.symm : (a : γ) → β) ((ε : (a : β) → γ) b : γ) : β)))
      (limit.π (Discrete.functor (f ∘ (⇑ε : (a : β) → γ))) { as := (ε.symm : (a : γ) → β) ((ε : (a : β) → γ) b : γ) })
      (Functor.map (Discrete.functor f) ((Discrete.equivalence ε).counit.app { as := (ε : (a : β) → γ) b })) :
    limit.{w, w, v, u} (J := Discrete β) (Discrete.functor (f ∘ (⇑ε : (a : β) → γ))) ⟶ f ((ε : (a : β) → γ) b))
  (π (f ∘ (⇑ε : (a : β) → γ)) b : piObj.{w, v, u} (β := β) (f ∘ (⇑ε : (a : β) → γ)) ⟶ (f ∘ (⇑ε : (a : β) → γ)) b)
Tactic: simp only [HasLimit.isoOfEquivalence_hom_π, Discrete.equivalence_inverse, Discrete.functor_obj,
    Function.comp_apply, Functor.id_obj, Discrete.equivalence_functor, Functor.comp_obj,
    Discrete.natIso_inv_app, Iso.refl_inv, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Products (goal)
Goal:
β : Type w
C : Type u
inst : Category.{v, u} C
γ : Type w'
ε : β ≃ γ
f : γ → C
inst_1 : HasCoproduct.{w', v, u} f
inst_2 : HasCoproduct.{w, v, u} (β := β) (f ∘ (⇑ε : (a : β) → γ))
b : β
⊢ Eq.{v + 1} (α := (f ∘ (⇑ε : (a : β) → γ)) b ⟶ sigmaObj.{w', v, u} f)
    (CategoryStruct.comp (Y := sigmaObj.{w, v, u} (β := β) (f ∘ (⇑ε : (a : β) → γ))) (ι (f ∘ (⇑ε : (a : β) → γ)) b)
      (Iso.hom (reindex ε f)))
    (ι f ((ε : (a : β) → γ) b))
have dsimp : Eq.{v + 1} (α := f ((ε : (a : β) → γ) b) ⟶ sigmaObj.{w', v, u} f)
  (CategoryStruct.comp (Y := sigmaObj.{w, v, u} (β := β) (f ∘ (⇑ε : (a : β) → γ))) (ι (f ∘ (⇑ε : (a : β) → γ)) b)
      (Iso.hom
        (HasColimit.isoOfEquivalence (Discrete.equivalence ε)
          (Discrete.natIso fun (x : Discrete β) ↦ Iso.refl (f ((ε : (a : β) → γ) x.as))))) :
    f ((ε : (a : β) → γ) b) ⟶ sigmaObj.{w', v, u} f)
  (ι f ((ε : (a : β) → γ) b) : f ((ε : (a : β) → γ) b) ⟶ sigmaObj.{w', v, u} f)
Tactic: dsimp [Sigma.reindex]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Products (goal)
Goal:
β : Type w
C : Type u
inst : Category.{v, u} C
γ : Type w'
ε : β ≃ γ
f : γ → C
inst_1 : HasCoproduct.{w', v, u} f
inst_2 : HasCoproduct.{w, v, u} (β := β) (f ∘ (⇑ε : (a : β) → γ))
b : β
⊢ Eq.{v + 1} (α := f ((ε : (a : β) → γ) b) ⟶ sigmaObj.{w', v, u} f)
    (CategoryStruct.comp (Y := sigmaObj.{w, v, u} (β := β) (f ∘ (⇑ε : (a : β) → γ))) (ι (f ∘ (⇑ε : (a : β) → γ)) b)
        (Iso.hom
          (HasColimit.isoOfEquivalence (Discrete.equivalence ε)
            (Discrete.natIso fun (x : Discrete β) ↦ Iso.refl (f ((ε : (a : β) → γ) x.as))))) :
      f ((ε : (a : β) → γ) b) ⟶ sigmaObj.{w', v, u} f)
    (ι f ((ε : (a : β) → γ) b) : f ((ε : (a : β) → γ) b) ⟶ sigmaObj.{w', v, u} f)
have simp : Eq.{v + 1} (α := f ((ε : (a : β) → γ) b) ⟶ sigmaObj.{w', v, u} f)
  (CategoryStruct.comp (Y := f ((ε : (a : β) → γ) ((ε.symm : (a : γ) → β) ((ε : (a : β) → γ) b : γ) : β)))
      (Functor.map (Discrete.functor (f ∘ (⇑ε : (a : β) → γ))) ((Discrete.equivalence ε).unit.app { as := b }))
      (colimit.ι (Discrete.functor f)
        { as := (ε : (a : β) → γ) ((ε.symm : (a : γ) → β) ((ε : (a : β) → γ) b : γ) : β) }) :
    f ((ε : (a : β) → γ) b) ⟶ colimit.{w', w', v, u} (Discrete.functor f))
  (ι f ((ε : (a : β) → γ) b) : f ((ε : (a : β) → γ) b) ⟶ sigmaObj.{w', v, u} f)
Tactic: simp only [HasColimit.ι_isoOfEquivalence_hom, Functor.id_obj, Discrete.functor_obj,
    Function.comp_apply, Discrete.equivalence_functor, Discrete.equivalence_inverse,
    Functor.comp_obj, Discrete.natIso_inv_app, Iso.refl_inv, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Products (hypothesis)
Goal:
β : Type w
C : Type u
inst : Category.{v, u} C
γ : Type w'
ε : β ≃ γ
f : γ → C
inst_1 : HasCoproduct.{w', v, u} f
inst_2 : HasCoproduct.{w, v, u} (β := β) (f ∘ (⇑ε : (a : β) → γ))
b : β
⊢ Eq.{v + 1} (α := f ((ε : (a : β) → γ) b) ⟶ sigmaObj.{w', v, u} f)
    (CategoryStruct.comp (Y := f ((ε : (a : β) → γ) ((ε.symm : (a : γ) → β) ((ε : (a : β) → γ) b : γ) : β)))
        (Functor.map (Discrete.functor (f ∘ (⇑ε : (a : β) → γ))) ((Discrete.equivalence ε).unit.app { as := b }))
        (colimit.ι (Discrete.functor f)
          { as := (ε : (a : β) → γ) ((ε.symm : (a : γ) → β) ((ε : (a : β) → γ) b : γ) : β) }) :
      f ((ε : (a : β) → γ) b) ⟶ colimit.{w', w', v, u} (Discrete.functor f))
    (ι f ((ε : (a : β) → γ) b) : f ((ε : (a : β) → γ) b) ⟶ sigmaObj.{w', v, u} f)
have h : Eq.{v + 1} (α :=
  Functor.obj.{w', v, w', u} (Discrete.functor f)
      { as := (ε : (a : β) → γ) ((ε.symm : (a : γ) → β) ((ε : (a : β) → γ) b : γ) : β) : Discrete γ } ⟶
    colimit.{w', w', v, u} (Discrete.functor f))
  (Functor.map (Discrete.functor f) (Discrete.eqToHom' sorry) ≫
    colimit.ι (Discrete.functor f) { as := (ε : (a : β) → γ) b })
  (colimit.ι (Discrete.functor f) { as := (ε : (a : β) → γ) ((ε.symm : (a : γ) → β) ((ε : (a : β) → γ) b : γ) : β) })
Tactic: have h := colimit.w (Discrete.functor f) (Discrete.eqToHom' (ε.apply_symm_apply (ε b)))
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Products (goal)
Goal:
β : Type w
C : Type u
inst : Category.{v, u} C
γ : Type w'
ε : β ≃ γ
f : γ → C
inst_1 : HasCoproduct.{w', v, u} f
inst_2 : HasCoproduct.{w, v, u} (β := β) (f ∘ (⇑ε : (a : β) → γ))
b : β
h :
  Eq.{v + 1} (α :=
    f ((ε : (a : β) → γ) ((ε.symm : (a : γ) → β) ((ε : (a : β) → γ) b : γ) : β)) ⟶
      colimit.{w', w', v, u} (Discrete.functor f))
    (CategoryStruct.comp (Y := f ((ε : (a : β) → γ) b)) (Functor.map (Discrete.functor f) (Discrete.eqToHom' ⋯))
        (colimit.ι (Discrete.functor f) { as := (ε : (a : β) → γ) b }) :
      f ((ε : (a : β) → γ) ((ε.symm : (a : γ) → β) ((ε : (a : β) → γ) b : γ) : β)) ⟶
        colimit.{w', w', v, u} (Discrete.functor f))
    (colimit.ι (Discrete.functor f) { as := (ε : (a : β) → γ) ((ε.symm : (a : γ) → β) ((ε : (a : β) → γ) b : γ) : β) } :
      Functor.obj.{w', v, w', u} (Discrete.functor f)
          { as := (ε : (a : β) → γ) ((ε.symm : (a : γ) → β) ((ε : (a : β) → γ) b : γ) : β) : Discrete γ } ⟶
        colimit.{w', w', v, u} (Discrete.functor f))
⊢ Eq.{v + 1} (α := f ((ε : (a : β) → γ) b) ⟶ sigmaObj.{w', v, u} f)
    (CategoryStruct.comp (Y := f ((ε : (a : β) → γ) ((ε.symm : (a : γ) → β) ((ε : (a : β) → γ) b : γ) : β)))
        (Functor.map (Discrete.functor (f ∘ (⇑ε : (a : β) → γ))) ((Discrete.equivalence ε).unit.app { as := b }))
        (colimit.ι (Discrete.functor f)
          { as := (ε : (a : β) → γ) ((ε.symm : (a : γ) → β) ((ε : (a : β) → γ) b : γ) : β) }) :
      f ((ε : (a : β) → γ) b) ⟶ colimit.{w', w', v, u} (Discrete.functor f))
    (ι f ((ε : (a : β) → γ) b) : f ((ε : (a : β) → γ) b) ⟶ sigmaObj.{w', v, u} f)
have erw : Eq.{v + 1} (α := f ((ε : (a : β) → γ) b) ⟶ sigmaObj.{w', v, u} f)
  (CategoryStruct.comp (Y := f ((ε : (a : β) → γ) b)) (eqToHom sorry)
      (colimit.ι (Discrete.functor f) { as := (ε : (a : β) → γ) b }) :
    f ((ε : (a : β) → γ) b) ⟶ colimit.{w', w', v, u} (Discrete.functor f))
  (ι f ((ε : (a : β) → γ) b) : f ((ε : (a : β) → γ) b) ⟶ sigmaObj.{w', v, u} f)
Tactic: erw [← h, eqToHom_map, eqToHom_map, eqToHom_trans_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Products (goal)
Goal:
β : Type w
C : Type u
inst : Category.{v, u} C
γ : Type w'
ε : β ≃ γ
f : γ → C
inst_1 : HasCoproduct.{w', v, u} f
inst_2 : HasCoproduct.{w, v, u} (β := β) (f ∘ (⇑ε : (a : β) → γ))
b : β
h :
  Eq.{v + 1} (α :=
    f ((ε : (a : β) → γ) ((ε.symm : (a : γ) → β) ((ε : (a : β) → γ) b : γ) : β)) ⟶
      colimit.{w', w', v, u} (Discrete.functor f))
    (CategoryStruct.comp (Y := f ((ε : (a : β) → γ) b)) (Functor.map (Discrete.functor f) (Discrete.eqToHom' ⋯))
        (colimit.ι (Discrete.functor f) { as := (ε : (a : β) → γ) b }) :
      f ((ε : (a : β) → γ) ((ε.symm : (a : γ) → β) ((ε : (a : β) → γ) b : γ) : β)) ⟶
        colimit.{w', w', v, u} (Discrete.functor f))
    (colimit.ι (Discrete.functor f) { as := (ε : (a : β) → γ) ((ε.symm : (a : γ) → β) ((ε : (a : β) → γ) b : γ) : β) } :
      Functor.obj.{w', v, w', u} (Discrete.functor f)
          { as := (ε : (a : β) → γ) ((ε.symm : (a : γ) → β) ((ε : (a : β) → γ) b : γ) : β) : Discrete γ } ⟶
        colimit.{w', w', v, u} (Discrete.functor f))
erw :
  Eq.{v + 1} (α := f ((ε : (a : β) → γ) b) ⟶ sigmaObj.{w', v, u} f)
    (CategoryStruct.comp (Y := f ((ε : (a : β) → γ) b)) (eqToHom ⋯)
        (colimit.ι (Discrete.functor f) { as := (ε : (a : β) → γ) b }) :
      f ((ε : (a : β) → γ) b) ⟶ colimit.{w', w', v, u} (Discrete.functor f))
    (ι f ((ε : (a : β) → γ) b) : f ((ε : (a : β) → γ) b) ⟶ sigmaObj.{w', v, u} f)
⊢ Eq.{v + 1} (α := f ((ε : (a : β) → γ) b) ⟶ sigmaObj.{w', v, u} f)
    (CategoryStruct.comp (Y := f ((ε : (a : β) → γ) ((ε.symm : (a : γ) → β) ((ε : (a : β) → γ) b : γ) : β)))
        (Functor.map (Discrete.functor (f ∘ (⇑ε : (a : β) → γ))) ((Discrete.equivalence ε).unit.app { as := b }))
        (colimit.ι (Discrete.functor f)
          { as := (ε : (a : β) → γ) ((ε.symm : (a : γ) → β) ((ε : (a : β) → γ) b : γ) : β) }) :
      f ((ε : (a : β) → γ) b) ⟶ colimit.{w', w', v, u} (Discrete.functor f))
    (ι f ((ε : (a : β) → γ) b) : f ((ε : (a : β) → γ) b) ⟶ sigmaObj.{w', v, u} f)
have p : { as := b : Discrete β } = { as := (ε.symm : (a : γ) → β) ((ε : (a : β) → γ) b : γ) }
Tactic: erw [← h, eqToHom_map, eqToHom_map, eqToHom_trans_assoc]