awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z P : C
s : BinaryFan.{v, u} X Y
t_1 : BinaryFan.{v, u} Y X
I : IsLimit s
t : Cone.{0, v, 0, u} (pair Y X)
m : t.pt ⟶ s.swap.pt
h : (∀ (j : Discrete WalkingPair), m ≫ s.π.app j = (BinaryFan.swap t).π.app j) → m = I.lift (BinaryFan.swap t)
j : WalkingPair
w :
  Eq (α := t.pt ⟶ Functor.obj.{0, v, 0, u} (pair Y X) { as := (WalkingPair.swap : (a : WalkingPair) → WalkingPair) j })
    (m ≫ s.swap.π.app { as := (WalkingPair.swap : (a : WalkingPair) → WalkingPair) j })
    (t.π.app { as := (WalkingPair.swap : (a : WalkingPair) → WalkingPair) j })
left :
  ∀
    (w :
      Eq (α :=
        t.pt ⟶
          Functor.obj.{0, v, 0, u} (pair Y X)
            { as := (WalkingPair.swap : (a : WalkingPair) → WalkingPair) WalkingPair.left })
        (m ≫ s.swap.π.app { as := (WalkingPair.swap : (a : WalkingPair) → WalkingPair) WalkingPair.left })
        (t.π.app { as := (WalkingPair.swap : (a : WalkingPair) → WalkingPair) WalkingPair.left })),
    Eq (α :=
      (BinaryFan.swap t).pt ⟶ Functor.obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair })
      (m ≫ s.π.app { as := WalkingPair.left }) ((BinaryFan.swap t).π.app { as := WalkingPair.left })
⊢ Eq (α := (BinaryFan.swap t).pt ⟶ Functor.obj.{0, v, 0, u} (pair X Y) { as := j : Discrete WalkingPair })
    (m ≫ s.π.app { as := j }) ((BinaryFan.swap t).π.app { as := j })
have right : ∀
  (w :
    Eq (α :=
      t.pt ⟶
        Functor.obj.{0, v, 0, u} (pair Y X)
          { as := (WalkingPair.swap : (a : WalkingPair) → WalkingPair) WalkingPair.right })
      (m ≫ s.swap.π.app { as := (WalkingPair.swap : (a : WalkingPair) → WalkingPair) WalkingPair.right })
      (t.π.app { as := (WalkingPair.swap : (a : WalkingPair) → WalkingPair) WalkingPair.right })),
  Eq (α :=
    (BinaryFan.swap t).pt ⟶ Functor.obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair })
    (m ≫ s.π.app { as := WalkingPair.right }) ((BinaryFan.swap t).π.app { as := WalkingPair.right })
Tactic: cases j
Cleared hypotheses: j, w
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z P_1 : C
sXY : BinaryFan.{v, u} X Y
sYZ : BinaryFan.{v, u} Y Z
P : IsLimit sXY
Q : IsLimit sYZ
s : BinaryFan.{v, u} sXY.pt Z
R : IsLimit s
t : Cone.{0, v, 0, u} (pair X sYZ.pt)
⊢ Eq (α := t.pt ⟶ Functor.obj.{0, v, 0, u} (pair X sYZ.pt) { as := WalkingPair.right : Discrete WalkingPair })
    (R.lift (BinaryFan.assocInv P t) ≫ (BinaryFan.assoc Q s).π.app { as := WalkingPair.right : Discrete WalkingPair } :
      t.pt ⟶ Functor.obj.{0, v, 0, u} (pair X sYZ.pt) { as := WalkingPair.right : Discrete WalkingPair })
    (t.π.app { as := WalkingPair.right } :
      Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) t.pt)
          { as := WalkingPair.right : Discrete WalkingPair } ⟶
        Functor.obj.{0, v, 0, u} (pair X sYZ.pt) { as := WalkingPair.right : Discrete WalkingPair })
have right : ∀ (j : Discrete WalkingPair),
  Eq (α := t.pt ⟶ Functor.obj.{0, v, 0, u} (pair Y Z) j)
    ((R.lift (BinaryFan.assocInv P t) ≫
          (BinaryFan.assoc Q s).π.app { as := WalkingPair.right : Discrete WalkingPair }) ≫
        sYZ.π.app j :
      t.pt ⟶ Functor.obj.{0, v, 0, u} (pair Y Z) j)
    (t.π.app { as := WalkingPair.right } ≫ sYZ.π.app j : t.pt ⟶ Functor.obj.{0, v, 0, u} (pair Y Z) j)
Tactic: apply Q.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z P_1 : C
sXY : BinaryFan.{v, u} X Y
sYZ : BinaryFan.{v, u} Y Z
P : IsLimit sXY
Q : IsLimit sYZ
s : BinaryFan.{v, u} sXY.pt Z
R : IsLimit s
t : Cone.{0, v, 0, u} (pair X sYZ.pt)
m : t.pt ⟶ (BinaryFan.assoc Q s).pt
w : ∀ (j : Discrete WalkingPair), m ≫ (BinaryFan.assoc Q s).π.app j = t.π.app j
⊢ m = R.lift (BinaryFan.assocInv P t)
have h : (∀ (j : Discrete WalkingPair), m ≫ s.π.app j = (BinaryFan.assocInv P t).π.app j) → m = R.lift (BinaryFan.assocInv P t)
Tactic: have h := R.uniq (BinaryFan.assocInv P t) m
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z P_1 : C
sXY : BinaryFan.{v, u} X Y
sYZ : BinaryFan.{v, u} Y Z
P : IsLimit sXY
Q : IsLimit sYZ
s : BinaryFan.{v, u} sXY.pt Z
R : IsLimit s
t : Cone.{0, v, 0, u} (pair X sYZ.pt)
m : t.pt ⟶ (BinaryFan.assoc Q s).pt
w : ∀ (j : Discrete WalkingPair), m ≫ (BinaryFan.assoc Q s).π.app j = t.π.app j
h :
  (∀ (j : Discrete WalkingPair), m ≫ s.π.app j = (BinaryFan.assocInv P t).π.app j) → m = R.lift (BinaryFan.assocInv P t)
⊢ m = R.lift (BinaryFan.assocInv P t)
have rw : ∀ (j : Discrete WalkingPair), m ≫ s.π.app j = (BinaryFan.assocInv P t).π.app j
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z P_1 : C
sXY : BinaryFan.{v, u} X Y
sYZ : BinaryFan.{v, u} Y Z
P : IsLimit sXY
Q : IsLimit sYZ
s : BinaryFan.{v, u} sXY.pt Z
R : IsLimit s
t : Cone.{0, v, 0, u} (pair X sYZ.pt)
m : t.pt ⟶ (BinaryFan.assoc Q s).pt
w : ∀ (j : Discrete WalkingPair), m ≫ (BinaryFan.assoc Q s).π.app j = t.π.app j
h :
  (∀ (j : Discrete WalkingPair), m ≫ s.π.app j = (BinaryFan.assocInv P t).π.app j) → m = R.lift (BinaryFan.assocInv P t)
⊢ Eq (α :=
    (BinaryFan.assocInv P t).pt ⟶
      Functor.obj.{0, v, 0, u} (pair sXY.pt Z) { as := WalkingPair.left : Discrete WalkingPair })
    (m ≫ s.π.app { as := WalkingPair.left }) ((BinaryFan.assocInv P t).π.app { as := WalkingPair.left })
have left : ∀ (j : Discrete WalkingPair),
  Eq (α := (BinaryFan.assocInv P t).pt ⟶ Functor.obj.{0, v, 0, u} (pair X Y) j)
    ((m ≫ s.π.app { as := WalkingPair.left }) ≫ sXY.π.app j)
    ((BinaryFan.assocInv P t).π.app { as := WalkingPair.left } ≫ sXY.π.app j)
Tactic: apply P.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z P_1 : C
sXY : BinaryFan.{v, u} X Y
sYZ : BinaryFan.{v, u} Y Z
P : IsLimit sXY
Q : IsLimit sYZ
s : BinaryFan.{v, u} sXY.pt Z
R : IsLimit s
t : Cone.{0, v, 0, u} (pair X sYZ.pt)
m : t.pt ⟶ (BinaryFan.assoc Q s).pt
w : ∀ (j : Discrete WalkingPair), m ≫ (BinaryFan.assoc Q s).π.app j = t.π.app j
h :
  (∀ (j : Discrete WalkingPair), m ≫ s.π.app j = (BinaryFan.assocInv P t).π.app j) → m = R.lift (BinaryFan.assocInv P t)
⊢ Eq (α :=
    (BinaryFan.assocInv P t).pt ⟶
      Functor.obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair })
    (CategoryStruct.comp (Y := sXY.pt)
      (m ≫ s.π.app { as := WalkingPair.left } :
        (BinaryFan.assocInv P t).pt ⟶
          Functor.obj.{0, v, 0, u} (pair sXY.pt Z) { as := WalkingPair.left : Discrete WalkingPair })
      (sXY.π.app { as := WalkingPair.right }))
    (CategoryStruct.comp (Y := sXY.pt)
      ((BinaryFan.assocInv P t).π.app { as := WalkingPair.left } :
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) (BinaryFan.assocInv P t).pt)
            { as := WalkingPair.left : Discrete WalkingPair } ⟶
          Functor.obj.{0, v, 0, u} (pair sXY.pt Z) { as := WalkingPair.left : Discrete WalkingPair })
      (sXY.π.app { as := WalkingPair.right }))
have w₁ : m ≫ BinaryFan.IsLimit.lift Q (s.fst ≫ sXY.snd) s.snd = t.π.app { as := WalkingPair.right }
Tactic: replace w : m ≫ BinaryFan.IsLimit.lift Q (s.fst ≫ sXY.snd) s.snd = t.π.app ⟨.right⟩ := by
          simpa using w ⟨.right⟩
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z P_1 : C
sXY : BinaryFan.{v, u} X Y
sYZ : BinaryFan.{v, u} Y Z
P : IsLimit sXY
Q : IsLimit sYZ
s : BinaryFan.{v, u} sXY.pt Z
R : IsLimit s
t : Cone.{0, v, 0, u} (pair X sYZ.pt)
m : t.pt ⟶ (BinaryFan.assoc Q s).pt
w : ∀ (j : Discrete WalkingPair), m ≫ (BinaryFan.assoc Q s).π.app j = t.π.app j
h :
  (∀ (j : Discrete WalkingPair), m ≫ s.π.app j = (BinaryFan.assocInv P t).π.app j) → m = R.lift (BinaryFan.assocInv P t)
⊢ Eq (α :=
    (BinaryFan.assocInv P t).pt ⟶
      Functor.obj.{0, v, 0, u} (pair sXY.pt Z) { as := WalkingPair.right : Discrete WalkingPair })
    (m ≫ s.π.app { as := WalkingPair.right }) ((BinaryFan.assocInv P t).π.app { as := WalkingPair.right })
have w₁ : m ≫ BinaryFan.IsLimit.lift Q (s.fst ≫ sXY.snd) s.snd = t.π.app { as := WalkingPair.right }
Tactic: replace w : m ≫ BinaryFan.IsLimit.lift Q (s.fst ≫ sXY.snd) s.snd = t.π.app ⟨.right⟩ := by
        simpa using w ⟨.right⟩
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y Z P_1 X : C
s : Cone.{0, v, 0, u} (Functor.empty C)
P : IsLimit s
t : BinaryFan.{v, u} s.pt X
Q : IsLimit t
⊢ t.snd ≫
      Q.lift
        (mk (P.lift { pt := X, π := { app := fun (x : Discrete PEmpty.{1}) ↦ x.as.elim, naturality := ⋯ } })
          (𝟙
            (Cone.pt.{0, v, 0, u} (J := Discrete PEmpty.{1}) (F := Functor.empty C)
              { pt := X,
                π :=
                  { app := fun (x : Discrete PEmpty.{1}) ↦ x.as.elim, naturality := ⋯ :
                    NatTrans (Functor.obj (Functor.const (Discrete PEmpty.{1})) X) (Functor.empty C) } :
                Cone.{0, v, 0, u} (Functor.empty C) }))) =
    𝟙 t.pt
have apply : ∀ (j : Discrete WalkingPair),
  (t.snd ≫
        Q.lift
          (mk
            (P.lift
              { pt := X,
                π :=
                  { app := fun (x : Discrete PEmpty.{1}) ↦ x.as.elim, naturality := sorry :
                    NatTrans (Functor.obj (Functor.const (Discrete PEmpty.{1})) X) (Functor.empty C) } :
                Cone.{0, v, 0, u} (Functor.empty C) })
            (𝟙
              (Cone.pt.{0, v, 0, u} (J := Discrete PEmpty.{1}) (F := Functor.empty C)
                { pt := X,
                  π :=
                    { app := fun (x : Discrete PEmpty.{1}) ↦ x.as.elim, naturality := sorry :
                      NatTrans (Functor.obj (Functor.const (Discrete PEmpty.{1})) X) (Functor.empty C) } :
                  Cone.{0, v, 0, u} (Functor.empty C) })))) ≫
      t.π.app j =
    𝟙 t.pt ≫ t.π.app j
Tactic: apply Q.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y Z P_1 X : C
s : Cone.{0, v, 0, u} (Functor.empty C)
P : IsLimit s
t : BinaryFan.{v, u} s.pt X
Q : IsLimit t
⊢ Eq (α := t.pt ⟶ Functor.obj.{0, v, 0, u} (pair s.pt X) { as := WalkingPair.left : Discrete WalkingPair })
    ((t.snd ≫
        Q.lift
          (mk (P.lift { pt := X, π := { app := fun (x : Discrete PEmpty.{1}) ↦ x.as.elim, naturality := ⋯ } })
            (𝟙
              (Cone.pt.{0, v, 0, u} (J := Discrete PEmpty.{1}) (F := Functor.empty C)
                { pt := X,
                  π :=
                    { app := fun (x : Discrete PEmpty.{1}) ↦ x.as.elim, naturality := ⋯ :
                      NatTrans (Functor.obj (Functor.const (Discrete PEmpty.{1})) X) (Functor.empty C) } :
                  Cone.{0, v, 0, u} (Functor.empty C) })))) ≫
      t.π.app { as := WalkingPair.left : Discrete WalkingPair })
    (𝟙 t.pt ≫ t.π.app { as := WalkingPair.left })
have left : ∀ (j : Discrete PEmpty.{1}),
  Eq (α := t.pt ⟶ Functor.obj.{0, v, 0, u} (Functor.empty C) j)
    (((t.snd ≫
          Q.lift
            (mk (P.lift { pt := X, π := { app := fun (x : Discrete PEmpty.{1}) ↦ x.as.elim, naturality := sorry } })
              (𝟙
                (Cone.pt.{0, v, 0, u} (J := Discrete PEmpty.{1}) (F := Functor.empty C)
                  { pt := X,
                    π :=
                      { app := fun (x : Discrete PEmpty.{1}) ↦ x.as.elim, naturality := sorry :
                        NatTrans (Functor.obj (Functor.const (Discrete PEmpty.{1})) X) (Functor.empty C) } :
                    Cone.{0, v, 0, u} (Functor.empty C) })))) ≫
        t.π.app { as := WalkingPair.left : Discrete WalkingPair }) ≫
      s.π.app j)
    ((𝟙 t.pt ≫ t.π.app { as := WalkingPair.left }) ≫ s.π.app j)
Tactic: apply P.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y Z P_1 X : C
s : Cone.{0, v, 0, u} (Functor.empty C)
P : IsLimit s
t : BinaryFan.{v, u} X s.pt
Q : IsLimit t
⊢ t.fst ≫
      Q.lift
        (mk (𝟙 X) (P.lift { pt := X, π := { app := fun (x : Discrete PEmpty.{1}) ↦ x.as.elim, naturality := ⋯ } })) =
    𝟙 t.pt
have apply : ∀ (j : Discrete WalkingPair),
  (t.fst ≫
        Q.lift
          (mk (𝟙 X)
            (P.lift
              { pt := X,
                π :=
                  { app := fun (x : Discrete PEmpty.{1}) ↦ x.as.elim, naturality := sorry :
                    NatTrans (Functor.obj (Functor.const (Discrete PEmpty.{1})) X) (Functor.empty C) } :
                Cone.{0, v, 0, u} (Functor.empty C) }))) ≫
      t.π.app j =
    𝟙 t.pt ≫ t.π.app j
Tactic: apply Q.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y Z P_1 X : C
s : Cone.{0, v, 0, u} (Functor.empty C)
P : IsLimit s
t : BinaryFan.{v, u} X s.pt
Q : IsLimit t
⊢ Eq (α := t.pt ⟶ Functor.obj.{0, v, 0, u} (pair X s.pt) { as := WalkingPair.right : Discrete WalkingPair })
    ((t.fst ≫
        Q.lift
          (mk (𝟙 X) (P.lift { pt := X, π := { app := fun (x : Discrete PEmpty.{1}) ↦ x.as.elim, naturality := ⋯ } }))) ≫
      t.π.app { as := WalkingPair.right : Discrete WalkingPair })
    (𝟙 t.pt ≫ t.π.app { as := WalkingPair.right })
have right : ∀ (j : Discrete PEmpty.{1}),
  Eq (α := t.pt ⟶ Functor.obj.{0, v, 0, u} (Functor.empty C) j)
    (((t.fst ≫
          Q.lift
            (mk (𝟙 X)
              (P.lift { pt := X, π := { app := fun (x : Discrete PEmpty.{1}) ↦ x.as.elim, naturality := sorry } }))) ≫
        t.π.app { as := WalkingPair.right : Discrete WalkingPair }) ≫
      s.π.app j)
    ((𝟙 t.pt ≫ t.π.app { as := WalkingPair.right }) ≫ s.π.app j)
Tactic: apply P.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
F : J → C
c c' : Bicone.{w, uC', uC} F
f g : c ⟶ c'
w : f.hom = g.hom
⊢ f = g
have mk : ∀ (hom : c.pt ⟶ c'.pt) (wπ : ∀ (j : J), hom ≫ c'.π j = c.π j) (wι : ∀ (j : J), c.ι j ≫ hom = c'.ι j)
  (w : { hom := hom, wπ := wπ, wι := wι : BiconeMorphism c c' }.hom = g.hom),
  { hom := hom, wπ := wπ, wι := wι : BiconeMorphism c c' } = g
Tactic: cases f
Cleared hypotheses: f, w
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
F : J → C
c c' : Bicone.{w, uC', uC} F
g : c ⟶ c'
hom : c.pt ⟶ c'.pt
wπ : ∀ (j : J), hom ≫ c'.π j = c.π j
wι : ∀ (j : J), c.ι j ≫ hom = c'.ι j
w : { hom := hom, wπ := wπ, wι := wι : BiconeMorphism c c' }.hom = g.hom
⊢ { hom := hom, wπ := wπ, wι := wι : BiconeMorphism c c' } = g
have mk : ∀ (hom_1 : c.pt ⟶ c'.pt) (wπ_1 : ∀ (j : J), hom_1 ≫ c'.π j = c.π j) (wι_1 : ∀ (j : J), c.ι j ≫ hom_1 = c'.ι j)
  (w : { hom := hom, wπ := wπ, wι := wι : BiconeMorphism c c' }.hom = { hom := hom_1, wπ := wπ_1, wι := wι_1 }.hom),
  { hom := hom, wπ := wπ, wι := wι : BiconeMorphism c c' } = { hom := hom_1, wπ := wπ_1, wι := wι_1 }
Tactic: cases g
Cleared hypotheses: g, w
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J → C
G : Functor.{uC', uD', uC, uD} C D
inst_4 : G.PreservesZeroMorphisms
A : Bicone.{w, uC', uC} F
i j : J
⊢ G.map (A.ι i ≫ A.π j) = if h : i = j then eqToHom ⋯ else 0
have rw : Eq (α := G.obj (F i) ⟶ G.obj (F j)) (G.map (if h : i = j then eqToHom sorry else 0)) (if h : i = j then eqToHom sorry else 0)
Tactic: rw [A.ι_π]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
f : J → C
t : Bicone.{w, uC', uC} f
ht : IsLimit t.toCone
j : J
j' : Discrete J
⊢ t.ι j ≫ t.toCone.π.app j' =
    ht.lift (Fan.mk (f j) fun (j' : J) ↦ if h : j = j' then eqToHom ⋯ else 0) ≫ t.toCone.π.app j'
have rw : t.ι j ≫ t.toCone.π.app j' = NatTrans.app (Cone.π (Fan.mk (f j) fun (j' : J) ↦ if h : j = j' then eqToHom sorry else 0)) j'
Tactic: rw [ht.fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
f : J → C
t : Bicone.{w, uC', uC} f
ht : IsColimit t.toCocone
j : J
j' : Discrete J
⊢ t.toCocone.ι.app j' ≫ t.π j =
    t.toCocone.ι.app j' ≫ ht.desc (Cofan.mk (f j) fun (j' : J) ↦ if h : j' = j then eqToHom ⋯ else 0)
have rw : t.toCocone.ι.app j' ≫ t.π j =
  NatTrans.app (Cocone.ι (Cofan.mk (f j) fun (j' : J) ↦ if h : j' = j then eqToHom sorry else 0)) j'
Tactic: rw [ht.fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J → C
K : Type w'
f : J → C
c : Bicone.{w, uC', uC} f
g : K ≃ J
k k' : K
⊢ Eq (α := (f ∘ (⇑g : (a : K) → J)) k ⟶ (f ∘ (⇑g : (a : K) → J)) k')
    (c.ι ((g : (a : K) → J) k) ≫ c.π ((g : (a : K) → J) k')) (if h : k = k' then eqToHom ⋯ else 0)
have simp : Eq.{uC' + 1} (α := (f ∘ (⇑g : (a : K) → J)) k ⟶ (f ∘ (⇑g : (a : K) → J)) k')
  (if h : Eq.{w + 1} (α := J) ((g : (a : K) → J) k : J) ((g : (a : K) → J) k' : J) then eqToHom sorry else 0)
  (if h : k = k' then eqToHom sorry else 0)
Tactic: simp only [c.ι_π]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J → C
K : Type w'
f : J → C
c : Bicone.{w, uC', uC} f
g : K ≃ J
k k' : K
⊢ Eq.{uC' + 1} (α := (f ∘ (⇑g : (a : K) → J)) k ⟶ (f ∘ (⇑g : (a : K) → J)) k')
    (if h : Eq.{w + 1} (α := J) ((g : (a : K) → J) k : J) ((g : (a : K) → J) k' : J) then eqToHom ⋯ else 0)
    (if h : k = k' then eqToHom ⋯ else 0)
have pos : ∀ (h : Eq.{w + 1} (α := J) ((g : (a : K) → J) k : J) ((g : (a : K) → J) k' : J)) (h' : k = k'),
  Eq.{uC' + 1} (α := (f ∘ (⇑g : (a : K) → J)) k ⟶ (f ∘ (⇑g : (a : K) → J)) k') (eqToHom sorry) (eqToHom sorry)
Tactic: split_ifs with h h' h'
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J → C
K : Type w'
f : J → C
c : Bicone.{w, uC', uC} f
g : K ≃ J
k k' : K
pos :
  ∀ (h : Eq.{w + 1} (α := J) ((g : (a : K) → J) k : J) ((g : (a : K) → J) k' : J)) (h' : k = k'),
    Eq.{uC' + 1} (α := (f ∘ (⇑g : (a : K) → J)) k ⟶ (f ∘ (⇑g : (a : K) → J)) k') (eqToHom ⋯) (eqToHom ⋯)
⊢ Eq.{uC' + 1} (α := (f ∘ (⇑g : (a : K) → J)) k ⟶ (f ∘ (⇑g : (a : K) → J)) k')
    (if h : Eq.{w + 1} (α := J) ((g : (a : K) → J) k : J) ((g : (a : K) → J) k' : J) then eqToHom ⋯ else 0)
    (if h : k = k' then eqToHom ⋯ else 0)
have neg : ∀ (h : Eq.{w + 1} (α := J) ((g : (a : K) → J) k : J) ((g : (a : K) → J) k' : J)) (h' : ¬k = k'),
  Eq.{uC' + 1} (α := (f ∘ (⇑g : (a : K) → J)) k ⟶ (f ∘ (⇑g : (a : K) → J)) k') (eqToHom sorry) 0
Tactic: split_ifs with h h' h'
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J → C
K : Type w'
f : J → C
c : Bicone.{w, uC', uC} f
g : K ≃ J
k k' : K
pos :
  ∀ (h : Eq.{w + 1} (α := J) ((g : (a : K) → J) k : J) ((g : (a : K) → J) k' : J)) (h' : k = k'),
    Eq.{uC' + 1} (α := (f ∘ (⇑g : (a : K) → J)) k ⟶ (f ∘ (⇑g : (a : K) → J)) k') (eqToHom ⋯) (eqToHom ⋯)
neg :
  ∀ (h : Eq.{w + 1} (α := J) ((g : (a : K) → J) k : J) ((g : (a : K) → J) k' : J)) (h' : ¬k = k'),
    Eq.{uC' + 1} (α := (f ∘ (⇑g : (a : K) → J)) k ⟶ (f ∘ (⇑g : (a : K) → J)) k') (eqToHom ⋯) 0
⊢ Eq.{uC' + 1} (α := (f ∘ (⇑g : (a : K) → J)) k ⟶ (f ∘ (⇑g : (a : K) → J)) k')
    (if h : Eq.{w + 1} (α := J) ((g : (a : K) → J) k : J) ((g : (a : K) → J) k' : J) then eqToHom ⋯ else 0)
    (if h : k = k' then eqToHom ⋯ else 0)
have pos₁ : ∀ (h : ¬Eq.{w + 1} (α := J) ((g : (a : K) → J) k : J) ((g : (a : K) → J) k' : J)) (h' : k = k'),
  Eq.{uC' + 1} (α := (f ∘ (⇑g : (a : K) → J)) k ⟶ (f ∘ (⇑g : (a : K) → J)) k') 0 (eqToHom sorry)
Tactic: split_ifs with h h' h'
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J → C
K : Type w'
f : J → C
c : Bicone.{w, uC', uC} f
g : K ≃ J
k k' : K
pos :
  ∀ (h : Eq.{w + 1} (α := J) ((g : (a : K) → J) k : J) ((g : (a : K) → J) k' : J)) (h' : k = k'),
    Eq.{uC' + 1} (α := (f ∘ (⇑g : (a : K) → J)) k ⟶ (f ∘ (⇑g : (a : K) → J)) k') (eqToHom ⋯) (eqToHom ⋯)
neg :
  ∀ (h : Eq.{w + 1} (α := J) ((g : (a : K) → J) k : J) ((g : (a : K) → J) k' : J)) (h' : ¬k = k'),
    Eq.{uC' + 1} (α := (f ∘ (⇑g : (a : K) → J)) k ⟶ (f ∘ (⇑g : (a : K) → J)) k') (eqToHom ⋯) 0
pos₁ :
  ∀ (h : ¬Eq.{w + 1} (α := J) ((g : (a : K) → J) k : J) ((g : (a : K) → J) k' : J)) (h' : k = k'),
    Eq.{uC' + 1} (α := (f ∘ (⇑g : (a : K) → J)) k ⟶ (f ∘ (⇑g : (a : K) → J)) k') 0 (eqToHom ⋯)
⊢ Eq.{uC' + 1} (α := (f ∘ (⇑g : (a : K) → J)) k ⟶ (f ∘ (⇑g : (a : K) → J)) k')
    (if h : Eq.{w + 1} (α := J) ((g : (a : K) → J) k : J) ((g : (a : K) → J) k' : J) then eqToHom ⋯ else 0)
    (if h : k = k' then eqToHom ⋯ else 0)
have neg₁ : ∀ (h : ¬Eq.{w + 1} (α := J) ((g : (a : K) → J) k : J) ((g : (a : K) → J) k' : J)) (h' : ¬k = k'),
  Eq.{uC' + 1} (α := (f ∘ (⇑g : (a : K) → J)) k ⟶ (f ∘ (⇑g : (a : K) → J)) k') 0 0
Tactic: split_ifs with h h' h'
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (hypothesis)
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J → C
K : Type w'
f : J → C
c : Bicone.{w, uC', uC} f
g : K ≃ J
k k' : K
h : Eq.{w + 1} (α := J) ((g : (a : K) → J) k : J) ((g : (a : K) → J) k' : J)
h' : ¬k = k'
⊢ Eq.{uC' + 1} (α := (f ∘ (⇑g : (a : K) → J)) k ⟶ (f ∘ (⇑g : (a : K) → J)) k') (eqToHom ⋯) 0
have h₁ : k = k'
Tactic: simp [Equiv.apply_eq_iff_eq g] at h h'
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (hypothesis)
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J → C
K : Type w'
f : J → C
c : Bicone.{w, uC', uC} f
g : K ≃ J
k k' : K
h : ¬Eq.{w + 1} (α := J) ((g : (a : K) → J) k : J) ((g : (a : K) → J) k' : J)
h' : k = k'
⊢ Eq.{uC' + 1} (α := (f ∘ (⇑g : (a : K) → J)) k ⟶ (f ∘ (⇑g : (a : K) → J)) k') 0 (eqToHom ⋯)
have h₁ : ¬k = k'
Tactic: simp [Equiv.apply_eq_iff_eq g] at h h'
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J → C
K : Type w'
f : J → C
c : Bicone.{w, uC', uC} f
g : K ≃ J
⊢ (c.whisker g).IsBilimit ≃ c.IsBilimit
have refine_1 : (hc : (c.whisker g).IsBilimit) → IsLimit c.toCone
Tactic: refine equivOfSubsingletonOfSubsingleton (fun hc => ⟨?_, ?_⟩) fun hc => ⟨?_, ?_⟩