awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (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
P Q X Y : C
c : BinaryBicone.{uC', uC} X Y
i : IsColimit c.toCocone
s : Cofork c.inl 0
h₁ : BinaryCofan.inl c.toCocone ≫ Cofork.π c.inlCokernelCofork ≫ c.inr ≫ s.π = BinaryCofan.inl c.toCocone ≫ s.π
⊢ Cofork.π c.inlCokernelCofork ≫ c.inr ≫ s.π = s.π
have h₂ : BinaryCofan.inr c.toCocone ≫ Cofork.π c.inlCokernelCofork ≫ c.inr ≫ s.π = BinaryCofan.inr c.toCocone ≫ s.π
Tactic: apply BinaryCofan.IsColimit.hom_ext i
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (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
P Q X Y : C
c : BinaryBicone.{uC', uC} X Y
i : IsColimit c.toCocone
s : Cofork c.inr 0
⊢ Cofork.π c.inrCokernelCofork ≫ c.inl ≫ s.π = s.π
have h₁ : BinaryCofan.inl c.toCocone ≫ Cofork.π c.inrCokernelCofork ≫ c.inl ≫ s.π = BinaryCofan.inl c.toCocone ≫ s.π
Tactic: apply BinaryCofan.IsColimit.hom_ext i
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (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
P Q X Y : C
c : BinaryBicone.{uC', uC} X Y
i : IsColimit c.toCocone
s : Cofork c.inr 0
h₁ : BinaryCofan.inl c.toCocone ≫ Cofork.π c.inrCokernelCofork ≫ c.inl ≫ s.π = BinaryCofan.inl c.toCocone ≫ s.π
⊢ Cofork.π c.inrCokernelCofork ≫ c.inl ≫ s.π = s.π
have h₂ : BinaryCofan.inr c.toCocone ≫ Cofork.π c.inrCokernelCofork ≫ c.inl ≫ s.π = BinaryCofan.inr c.toCocone ≫ s.π
Tactic: apply BinaryCofan.IsColimit.hom_ext i
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (goal)
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
P Q : C
inst_2 : HasBinaryBiproduct.{uC', uC} P Q
⊢ Eq.{uC' + 1} (α := op P ⟶ biprod.{uC', uC} (op P) (op Q))
    (CategoryStruct.comp (Y := op (biprod.{uC', uC} P Q)) (Quiver.Hom.op fst) (Iso.hom (opIso P Q)) :
      op P ⟶ biprod.{uC', uC} (op P) (op Q))
    (inl : op P ⟶ biprod.{uC', uC} (op P) (op Q))
have h₀ : Eq.{uC' + 1} (α := op P ⟶ op P)
  (CategoryStruct.comp (Y := biprod.{uC', uC} (op P) (op Q))
    (CategoryStruct.comp (Y := op (biprod.{uC', uC} P Q)) (Quiver.Hom.op fst) (Iso.hom (opIso P Q)) :
      op P ⟶ biprod.{uC', uC} (op P) (op Q))
    (fst : biprod.{uC', uC} (op P) (op Q) ⟶ op P))
  (CategoryStruct.comp (Y := biprod.{uC', uC} (op P) (op Q)) inl fst)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (goal)
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
P Q : C
inst_2 : HasBinaryBiproduct.{uC', uC} P Q
h₀ :
  Eq.{uC' + 1} (α := op P ⟶ op P)
    (CategoryStruct.comp (Y := biprod.{uC', uC} (op P) (op Q))
      (CategoryStruct.comp (Y := op (biprod.{uC', uC} P Q)) (Quiver.Hom.op fst) (Iso.hom (opIso P Q)) :
        op P ⟶ biprod.{uC', uC} (op P) (op Q))
      (fst : biprod.{uC', uC} (op P) (op Q) ⟶ op P))
    (CategoryStruct.comp (Y := biprod.{uC', uC} (op P) (op Q)) inl fst)
⊢ Eq.{uC' + 1} (α := op P ⟶ biprod.{uC', uC} (op P) (op Q))
    (CategoryStruct.comp (Y := op (biprod.{uC', uC} P Q)) (Quiver.Hom.op fst) (Iso.hom (opIso P Q)) :
      op P ⟶ biprod.{uC', uC} (op P) (op Q))
    (inl : op P ⟶ biprod.{uC', uC} (op P) (op Q))
have h₁ : Eq.{uC' + 1} (α := op P ⟶ op Q)
  (CategoryStruct.comp (Y := biprod.{uC', uC} (op P) (op Q))
    (CategoryStruct.comp (Y := op (biprod.{uC', uC} P Q)) (Quiver.Hom.op fst) (Iso.hom (opIso P Q)) :
      op P ⟶ biprod.{uC', uC} (op P) (op Q))
    (snd : biprod.{uC', uC} (op P) (op Q) ⟶ op Q))
  (CategoryStruct.comp (Y := biprod.{uC', uC} (op P) (op Q)) inl snd)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (goal)
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
P Q : C
inst_2 : HasBinaryBiproduct.{uC', uC} P Q
⊢ Eq.{uC' + 1} (α := op Q ⟶ biprod.{uC', uC} (op P) (op Q))
    (CategoryStruct.comp (Y := op (biprod.{uC', uC} P Q)) (Quiver.Hom.op snd) (Iso.hom (opIso P Q)) :
      op Q ⟶ biprod.{uC', uC} (op P) (op Q))
    (inr : op Q ⟶ biprod.{uC', uC} (op P) (op Q))
have h₀ : Eq.{uC' + 1} (α := op Q ⟶ op P)
  (CategoryStruct.comp (Y := biprod.{uC', uC} (op P) (op Q))
    (CategoryStruct.comp (Y := op (biprod.{uC', uC} P Q)) (Quiver.Hom.op snd) (Iso.hom (opIso P Q)) :
      op Q ⟶ biprod.{uC', uC} (op P) (op Q))
    (fst : biprod.{uC', uC} (op P) (op Q) ⟶ op P))
  (CategoryStruct.comp (Y := biprod.{uC', uC} (op P) (op Q)) inr fst)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (goal)
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
P Q : C
inst_2 : HasBinaryBiproduct.{uC', uC} P Q
h₀ :
  Eq.{uC' + 1} (α := op Q ⟶ op P)
    (CategoryStruct.comp (Y := biprod.{uC', uC} (op P) (op Q))
      (CategoryStruct.comp (Y := op (biprod.{uC', uC} P Q)) (Quiver.Hom.op snd) (Iso.hom (opIso P Q)) :
        op Q ⟶ biprod.{uC', uC} (op P) (op Q))
      (fst : biprod.{uC', uC} (op P) (op Q) ⟶ op P))
    (CategoryStruct.comp (Y := biprod.{uC', uC} (op P) (op Q)) inr fst)
⊢ Eq.{uC' + 1} (α := op Q ⟶ biprod.{uC', uC} (op P) (op Q))
    (CategoryStruct.comp (Y := op (biprod.{uC', uC} P Q)) (Quiver.Hom.op snd) (Iso.hom (opIso P Q)) :
      op Q ⟶ biprod.{uC', uC} (op P) (op Q))
    (inr : op Q ⟶ biprod.{uC', uC} (op P) (op Q))
have h₁ : Eq.{uC' + 1} (α := op Q ⟶ op Q)
  (CategoryStruct.comp (Y := biprod.{uC', uC} (op P) (op Q))
    (CategoryStruct.comp (Y := op (biprod.{uC', uC} P Q)) (Quiver.Hom.op snd) (Iso.hom (opIso P Q)) :
      op Q ⟶ biprod.{uC', uC} (op P) (op Q))
    (snd : biprod.{uC', uC} (op P) (op Q) ⟶ op Q))
  (CategoryStruct.comp (Y := biprod.{uC', uC} (op P) (op Q)) inr snd)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (goal)
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
P Q : C
inst_2 : HasBinaryBiproduct.{uC', uC} P Q
⊢ Eq.{uC' + 1} (α := biprod.{uC', uC} (op P) (op Q) ⟶ op P)
    (CategoryStruct.comp (Y := op (biprod.{uC', uC} P Q)) (Iso.inv (opIso P Q)) (Quiver.Hom.op inl) :
      biprod.{uC', uC} (op P) (op Q) ⟶ op P)
    (fst : biprod.{uC', uC} (op P) (op Q) ⟶ op P)
have h₀ : Eq.{uC' + 1} (α := op P ⟶ op P)
  (CategoryStruct.comp (Y := biprod.{uC', uC} (op P) (op Q)) (inl : op P ⟶ biprod.{uC', uC} (op P) (op Q))
    (CategoryStruct.comp (Y := op (biprod.{uC', uC} P Q)) (Iso.inv (opIso P Q)) (Quiver.Hom.op inl) :
      biprod.{uC', uC} (op P) (op Q) ⟶ op P))
  (CategoryStruct.comp (Y := biprod.{uC', uC} (op P) (op Q)) inl fst)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (goal)
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
P Q : C
inst_2 : HasBinaryBiproduct.{uC', uC} P Q
h₀ :
  Eq.{uC' + 1} (α := op P ⟶ op P)
    (CategoryStruct.comp (Y := biprod.{uC', uC} (op P) (op Q)) (inl : op P ⟶ biprod.{uC', uC} (op P) (op Q))
      (CategoryStruct.comp (Y := op (biprod.{uC', uC} P Q)) (Iso.inv (opIso P Q)) (Quiver.Hom.op inl) :
        biprod.{uC', uC} (op P) (op Q) ⟶ op P))
    (CategoryStruct.comp (Y := biprod.{uC', uC} (op P) (op Q)) inl fst)
⊢ Eq.{uC' + 1} (α := biprod.{uC', uC} (op P) (op Q) ⟶ op P)
    (CategoryStruct.comp (Y := op (biprod.{uC', uC} P Q)) (Iso.inv (opIso P Q)) (Quiver.Hom.op inl) :
      biprod.{uC', uC} (op P) (op Q) ⟶ op P)
    (fst : biprod.{uC', uC} (op P) (op Q) ⟶ op P)
have h₁ : Eq.{uC' + 1} (α := op Q ⟶ op P)
  (CategoryStruct.comp (Y := biprod.{uC', uC} (op P) (op Q)) (inr : op Q ⟶ biprod.{uC', uC} (op P) (op Q))
    (CategoryStruct.comp (Y := op (biprod.{uC', uC} P Q)) (Iso.inv (opIso P Q)) (Quiver.Hom.op inl) :
      biprod.{uC', uC} (op P) (op Q) ⟶ op P))
  (CategoryStruct.comp (Y := biprod.{uC', uC} (op P) (op Q)) inr fst)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (goal)
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
P Q : C
inst_2 : HasBinaryBiproduct.{uC', uC} P Q
⊢ Eq.{uC' + 1} (α := biprod.{uC', uC} (op P) (op Q) ⟶ op Q)
    (CategoryStruct.comp (Y := op (biprod.{uC', uC} P Q)) (Iso.inv (opIso P Q)) (Quiver.Hom.op inr) :
      biprod.{uC', uC} (op P) (op Q) ⟶ op Q)
    (snd : biprod.{uC', uC} (op P) (op Q) ⟶ op Q)
have h₀ : Eq.{uC' + 1} (α := op P ⟶ op Q)
  (CategoryStruct.comp (Y := biprod.{uC', uC} (op P) (op Q)) (inl : op P ⟶ biprod.{uC', uC} (op P) (op Q))
    (CategoryStruct.comp (Y := op (biprod.{uC', uC} P Q)) (Iso.inv (opIso P Q)) (Quiver.Hom.op inr) :
      biprod.{uC', uC} (op P) (op Q) ⟶ op Q))
  (CategoryStruct.comp (Y := biprod.{uC', uC} (op P) (op Q)) inl snd)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (goal)
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
P Q : C
inst_2 : HasBinaryBiproduct.{uC', uC} P Q
h₀ :
  Eq.{uC' + 1} (α := op P ⟶ op Q)
    (CategoryStruct.comp (Y := biprod.{uC', uC} (op P) (op Q)) (inl : op P ⟶ biprod.{uC', uC} (op P) (op Q))
      (CategoryStruct.comp (Y := op (biprod.{uC', uC} P Q)) (Iso.inv (opIso P Q)) (Quiver.Hom.op inr) :
        biprod.{uC', uC} (op P) (op Q) ⟶ op Q))
    (CategoryStruct.comp (Y := biprod.{uC', uC} (op P) (op Q)) inl snd)
⊢ Eq.{uC' + 1} (α := biprod.{uC', uC} (op P) (op Q) ⟶ op Q)
    (CategoryStruct.comp (Y := op (biprod.{uC', uC} P Q)) (Iso.inv (opIso P Q)) (Quiver.Hom.op inr) :
      biprod.{uC', uC} (op P) (op Q) ⟶ op Q)
    (snd : biprod.{uC', uC} (op P) (op Q) ⟶ op Q)
have h₁ : Eq.{uC' + 1} (α := op Q ⟶ op Q)
  (CategoryStruct.comp (Y := biprod.{uC', uC} (op P) (op Q)) (inr : op Q ⟶ biprod.{uC', uC} (op P) (op Q))
    (CategoryStruct.comp (Y := op (biprod.{uC', uC} P Q)) (Iso.inv (opIso P Q)) (Quiver.Hom.op inr) :
      biprod.{uC', uC} (op P) (op Q) ⟶ op Q))
  (CategoryStruct.comp (Y := biprod.{uC', uC} (op P) (op Q)) inr snd)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (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
P Q X Y : C
inst_4 : HasBinaryBiproduct.{uC', uC} X Y
hY : IsZero.{uC', uC} Y
⊢ biprod.fst ≫ biprod.inl = 𝟙 (biprod.{uC', uC} X Y)
have h₀ : CategoryStruct.comp (Y := biprod.{uC', uC} X Y) (biprod.fst ≫ biprod.inl) biprod.fst =
  𝟙 (biprod.{uC', uC} X Y) ≫ biprod.fst
Tactic: apply CategoryTheory.Limits.biprod.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (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
P Q X Y : C
inst_4 : HasBinaryBiproduct.{uC', uC} X Y
hY : IsZero.{uC', uC} Y
h₀ :
  CategoryStruct.comp (Y := biprod.{uC', uC} X Y) (biprod.fst ≫ biprod.inl) biprod.fst =
    𝟙 (biprod.{uC', uC} X Y) ≫ biprod.fst
⊢ biprod.fst ≫ biprod.inl = 𝟙 (biprod.{uC', uC} X Y)
have h₁ : CategoryStruct.comp (Y := biprod.{uC', uC} X Y) (biprod.fst ≫ biprod.inl) biprod.snd =
  𝟙 (biprod.{uC', uC} X Y) ≫ biprod.snd
Tactic: apply CategoryTheory.Limits.biprod.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (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
P Q X Y : C
inst_4 : HasBinaryBiproduct.{uC', uC} X Y
hY : IsZero.{uC', uC} Y
⊢ CategoryStruct.comp (Y := biprod.{uC', uC} X Y) (biprod.fst ≫ biprod.inl) biprod.snd =
    𝟙 (biprod.{uC', uC} X Y) ≫ biprod.snd
have h₁ : Eq.{uC' + 1} (α := biprod.{uC', uC} X Y ⟶ Y) 0 biprod.snd
Tactic: simp only [Category.assoc, biprod.inl_fst, Category.comp_id, Category.id_comp, biprod.inl_snd,
        comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (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
P Q X Y : C
inst_4 : HasBinaryBiproduct.{uC', uC} X Y
hY : IsZero.{uC', uC} X
⊢ biprod.snd ≫ biprod.inr = 𝟙 (biprod.{uC', uC} X Y)
have h₀ : CategoryStruct.comp (Y := biprod.{uC', uC} X Y) (biprod.snd ≫ biprod.inr) biprod.fst =
  𝟙 (biprod.{uC', uC} X Y) ≫ biprod.fst
Tactic: apply CategoryTheory.Limits.biprod.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (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
P Q X Y : C
inst_4 : HasBinaryBiproduct.{uC', uC} X Y
hY : IsZero.{uC', uC} X
h₀ :
  CategoryStruct.comp (Y := biprod.{uC', uC} X Y) (biprod.snd ≫ biprod.inr) biprod.fst =
    𝟙 (biprod.{uC', uC} X Y) ≫ biprod.fst
⊢ biprod.snd ≫ biprod.inr = 𝟙 (biprod.{uC', uC} X Y)
have h₁ : CategoryStruct.comp (Y := biprod.{uC', uC} X Y) (biprod.snd ≫ biprod.inr) biprod.snd =
  𝟙 (biprod.{uC', uC} X Y) ≫ biprod.snd
Tactic: apply CategoryTheory.Limits.biprod.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (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
P Q X Y : C
inst_4 : HasBinaryBiproduct.{uC', uC} X Y
hY : IsZero.{uC', uC} X
⊢ CategoryStruct.comp (Y := biprod.{uC', uC} X Y) (biprod.snd ≫ biprod.inr) biprod.fst =
    𝟙 (biprod.{uC', uC} X Y) ≫ biprod.fst
have h₀ : Eq.{uC' + 1} (α := biprod.{uC', uC} X Y ⟶ X) 0 biprod.fst
Tactic: simp only [Category.assoc, biprod.inr_snd, Category.comp_id, Category.id_comp, biprod.inr_fst,
        comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (goal)
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
A B : C
inst_2 : HasBinaryBiproduct.{uC', uC} A B
⊢ IsZero.{uC', uC} (biprod.{uC', uC} A B) ↔ IsZero.{uC', uC} A ∧ IsZero.{uC', uC} B
have mp : IsZero.{uC', uC} (biprod.{uC', uC} A B) → IsZero.{uC', uC} A ∧ IsZero.{uC', uC} B
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (goal)
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
A B : C
inst_2 : HasBinaryBiproduct.{uC', uC} A B
mp : IsZero.{uC', uC} (biprod.{uC', uC} A B) → IsZero.{uC', uC} A ∧ IsZero.{uC', uC} B
⊢ IsZero.{uC', uC} (biprod.{uC', uC} A B) ↔ IsZero.{uC', uC} A ∧ IsZero.{uC', uC} B
have mpr : IsZero.{uC', uC} A ∧ IsZero.{uC', uC} B → IsZero.{uC', uC} (biprod.{uC', uC} A B)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (goal)
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
A B : C
inst_2 : HasBinaryBiproduct.{uC', uC} A B
h : IsZero.{uC', uC} (biprod.{uC', uC} A B)
⊢ IsZero.{uC', uC} A ∧ IsZero.{uC', uC} B
have mp : ∀ (h : Eq.{uC' + 1} (α := biprod.{uC', uC} A B ⟶ biprod.{uC', uC} A B) (𝟙 (biprod.{uC', uC} A B)) 0),
  Eq.{uC' + 1} (α := A ⟶ A) (𝟙 A) 0 ∧ Eq.{uC' + 1} (α := B ⟶ B) (𝟙 B) 0
Tactic: simp only [IsZero.iff_id_eq_zero] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (goal)
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
A B : C
inst_2 : HasBinaryBiproduct.{uC', uC} A B
hA : IsZero.{uC', uC} A
hB : IsZero.{uC', uC} B
⊢ IsZero.{uC', uC} (biprod.{uC', uC} A B)
have mpr : Eq.{uC' + 1} (α := biprod.{uC', uC} A B ⟶ biprod.{uC', uC} A B) (𝟙 (biprod.{uC', uC} A B)) 0
Tactic: rw [IsZero.iff_id_eq_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (goal)
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
A B : C
inst_2 : HasBinaryBiproduct.{uC', uC} A B
hA : IsZero.{uC', uC} A
hB : IsZero.{uC', uC} B
⊢ Eq.{uC' + 1} (α := biprod.{uC', uC} A B ⟶ biprod.{uC', uC} A B) (𝟙 (biprod.{uC', uC} A B)) 0
have mpr : 𝟙 (biprod.{uC', uC} A B) ≫ biprod.fst = CategoryStruct.comp (Y := biprod.{uC', uC} A B) 0 biprod.fst
Tactic: apply biprod.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (goal)
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
A B : C
inst_2 : HasBinaryBiproduct.{uC', uC} A B
hA : IsZero.{uC', uC} A
hB : IsZero.{uC', uC} B
mpr : 𝟙 (biprod.{uC', uC} A B) ≫ biprod.fst = CategoryStruct.comp (Y := biprod.{uC', uC} A B) 0 biprod.fst
⊢ Eq.{uC' + 1} (α := biprod.{uC', uC} A B ⟶ biprod.{uC', uC} A B) (𝟙 (biprod.{uC', uC} A B)) 0
have mpr₁ : 𝟙 (biprod.{uC', uC} A B) ≫ biprod.snd = CategoryStruct.comp (Y := biprod.{uC', uC} A B) 0 biprod.snd
Tactic: apply biprod.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst_3 : IsIso (X := biprod.{v, u} W X) (Y := biprod.{v, u} Y Z) (biprod.map f g)
⊢ f ≫
      CategoryStruct.comp (Y := biprod.{v, u} Y Z) biprod.inl
        (CategoryStruct.comp (Y := biprod.{v, u} W X) (inv (biprod.map f g)) biprod.fst) =
    𝟙 W
have t : Eq.{v + 1} (α := W ⟶ W)
  ((fun (p : biprod.{v, u} W X ⟶ biprod.{v, u} W X) ↦ biprod.inl ≫ p ≫ biprod.fst)
    (CategoryStruct.comp (Y := biprod.{v, u} Y Z) (biprod.map f g) (inv (biprod.map f g))))
  ((fun (p : biprod.{v, u} W X ⟶ biprod.{v, u} W X) ↦ biprod.inl ≫ p ≫ biprod.fst) (𝟙 (biprod.{v, u} W X)))
Tactic: have t := congrArg (fun p : W ⊞ X ⟶ W ⊞ X => biprod.inl ≫ p ≫ biprod.fst)
          (IsIso.hom_inv_id (biprod.map f g))
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst_3 : IsIso (X := biprod.{v, u} W X) (Y := biprod.{v, u} Y Z) (biprod.map f g)
t :
  Eq.{v + 1} (α := W ⟶ W)
    ((fun (p : biprod.{v, u} W X ⟶ biprod.{v, u} W X) ↦ biprod.inl ≫ p ≫ biprod.fst)
      (CategoryStruct.comp (Y := biprod.{v, u} Y Z) (biprod.map f g) (inv (biprod.map f g))))
    ((fun (p : biprod.{v, u} W X ⟶ biprod.{v, u} W X) ↦ biprod.inl ≫ p ≫ biprod.fst) (𝟙 (biprod.{v, u} W X)))
⊢ f ≫
      CategoryStruct.comp (Y := biprod.{v, u} Y Z) biprod.inl
        (CategoryStruct.comp (Y := biprod.{v, u} W X) (inv (biprod.map f g)) biprod.fst) =
    𝟙 W
have t₁ : f ≫
    CategoryStruct.comp (Y := biprod.{v, u} Y Z) biprod.inl
      (CategoryStruct.comp (Y := biprod.{v, u} W X) (inv (biprod.map f g)) biprod.fst) =
  CategoryStruct.comp (Y := biprod.{v, u} W X) biprod.inl biprod.fst
Tactic: simp only [Category.id_comp, Category.assoc, biprod.inl_map_assoc] at t
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst_3 : IsIso (X := biprod.{v, u} W X) (Y := biprod.{v, u} Y Z) (biprod.map f g)
⊢ CategoryStruct.comp (Y := biprod.{v, u} Y Z) biprod.inl
        (CategoryStruct.comp (Y := biprod.{v, u} W X) (inv (biprod.map f g)) biprod.fst) ≫
      f =
    𝟙 Y
have t : Eq.{v + 1} (α := Y ⟶ Y)
  ((fun (p : biprod.{v, u} Y Z ⟶ biprod.{v, u} Y Z) ↦ biprod.inl ≫ p ≫ biprod.fst)
    (CategoryStruct.comp (Y := biprod.{v, u} W X) (inv (biprod.map f g)) (biprod.map f g)))
  ((fun (p : biprod.{v, u} Y Z ⟶ biprod.{v, u} Y Z) ↦ biprod.inl ≫ p ≫ biprod.fst) (𝟙 (biprod.{v, u} Y Z)))
Tactic: have t := congrArg (fun p : Y ⊞ Z ⟶ Y ⊞ Z => biprod.inl ≫ p ≫ biprod.fst)
          (IsIso.inv_hom_id (biprod.map f g))
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst_3 : IsIso (X := biprod.{v, u} W X) (Y := biprod.{v, u} Y Z) (biprod.map f g)
t :
  Eq.{v + 1} (α := Y ⟶ Y)
    ((fun (p : biprod.{v, u} Y Z ⟶ biprod.{v, u} Y Z) ↦ biprod.inl ≫ p ≫ biprod.fst)
      (CategoryStruct.comp (Y := biprod.{v, u} W X) (inv (biprod.map f g)) (biprod.map f g)))
    ((fun (p : biprod.{v, u} Y Z ⟶ biprod.{v, u} Y Z) ↦ biprod.inl ≫ p ≫ biprod.fst) (𝟙 (biprod.{v, u} Y Z)))
⊢ CategoryStruct.comp (Y := biprod.{v, u} Y Z) biprod.inl
        (CategoryStruct.comp (Y := biprod.{v, u} W X) (inv (biprod.map f g)) biprod.fst) ≫
      f =
    𝟙 Y
have t₁ : CategoryStruct.comp (Y := biprod.{v, u} Y Z) biprod.inl
    (CategoryStruct.comp (Y := biprod.{v, u} W X) (inv (biprod.map f g)) (biprod.fst ≫ f)) =
  CategoryStruct.comp (Y := biprod.{v, u} Y Z) biprod.inl biprod.fst
Tactic: simp only [Category.id_comp, Category.assoc, biprod.map_fst] at t
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst_3 : IsIso (X := biprod.{v, u} W X) (Y := biprod.{v, u} Y Z) (biprod.map f g)
t :
  CategoryStruct.comp (Y := biprod.{v, u} Y Z) biprod.inl
      (CategoryStruct.comp (Y := biprod.{v, u} W X) (inv (biprod.map f g)) (biprod.fst ≫ f)) =
    CategoryStruct.comp (Y := biprod.{v, u} Y Z) biprod.inl biprod.fst
⊢ CategoryStruct.comp (Y := biprod.{v, u} Y Z) biprod.inl
        (CategoryStruct.comp (Y := biprod.{v, u} W X) (inv (biprod.map f g)) biprod.fst) ≫
      f =
    𝟙 Y
have simp : CategoryStruct.comp (Y := biprod.{v, u} Y Z) biprod.inl
    (CategoryStruct.comp (Y := biprod.{v, u} W X) (inv (biprod.map f g)) (biprod.fst ≫ f)) =
  𝟙 Y
Tactic: simp only [Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst_3 : IsIso (X := biprod.{v, u} W X) (Y := biprod.{v, u} Y Z) (biprod.map f g)
⊢ IsIso (X := biprod.{v, u} X W) (Y := biprod.{v, u} Z Y) (biprod.map g f)
have rw : IsIso (X := biprod.{v, u} X W) (Y := biprod.{v, u} Z Y)
  (CategoryStruct.comp (Y := biprod.{v, u} W X) (Iso.hom (biprod.braiding X W) : biprod.{v, u} X W ⟶ biprod.{v, u} W X)
      (CategoryStruct.comp (Y := biprod.{v, u} Y Z) (biprod.map f g : biprod.{v, u} W X ⟶ biprod.{v, u} Y Z)
          (Iso.hom (biprod.braiding Y Z) : biprod.{v, u} Y Z ⟶ biprod.{v, u} Z Y) :
        biprod.{v, u} W X ⟶ biprod.{v, u} Z Y) :
    biprod.{v, u} X W ⟶ biprod.{v, u} Z Y)
Tactic: rw [← biprod.braiding_map_braiding]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
Goal:
j : WalkingPair
⊢ (fun (x : WalkingPair) ↦
        (match (motive := WalkingPair → WalkingPair) x with
          | left => right
          | right => left :
          WalkingPair))
      ((fun (x : WalkingPair) ↦
          (match (motive := WalkingPair → WalkingPair) x with
            | left => right
            | right => left :
            WalkingPair))
        j) =
    j
have left : (fun (x : WalkingPair) ↦
      (match (motive := WalkingPair → WalkingPair) x with
        | left => right
        | right => left :
        WalkingPair))
    ((fun (x : WalkingPair) ↦
        (match (motive := WalkingPair → WalkingPair) x with
          | left => right
          | right => left :
          WalkingPair))
      left) =
  left
Tactic: cases j
Cleared hypotheses: j