awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
W X Y Z : C
inst_2 : HasBinaryBiproduct.{uC', uC} W X
inst_3 : HasBinaryBiproduct.{uC', uC} Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ Eq (α := X ⟶ biprod.{uC', uC} Y Z) (CategoryStruct.comp (Y := biprod.{uC', uC} W X) inr (map f g)) (g ≫ inr)
have rw : Eq (α := X ⟶ biprod.{uC', uC} Y Z) (CategoryStruct.comp (Y := biprod.{uC', uC} W X) inr (map' f g)) (g ≫ inr)
Tactic: rw [biprod.map_eq_map']
-- 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
X Y : C
inst_2 : HasBinaryBiproduct.{uC', uC} X Y
b : BinaryBicone.{uC', uC} X Y
hb : b.IsBilimit
⊢ Eq (α := Cone.pt.{0, uC', 0, uC} (BinaryBicone.toCone (BinaryBiproduct.bicone X Y)) ⟶ b.toCone.pt)
    (Iso.inv (hb.isLimit.conePointUniqueUpToIso (BinaryBiproduct.isLimit X Y))) (desc b.inl b.inr)
have refine_1 : ∀ (j : Discrete WalkingPair),
  CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inl
        (Iso.inv (hb.isLimit.conePointUniqueUpToIso (BinaryBiproduct.isLimit X Y))) ≫
      b.toCone.π.app j =
    CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inl (desc b.inl b.inr) ≫ b.toCone.π.app j
Tactic: refine biprod.hom_ext' _ _ (hb.isLimit.hom_ext fun j => ?_) (hb.isLimit.hom_ext fun j => ?_)
-- 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
X Y : C
inst_2 : HasBinaryBiproduct.{uC', uC} X Y
b : BinaryBicone.{uC', uC} X Y
hb : b.IsBilimit
refine_1 :
  ∀ (j : Discrete WalkingPair),
    CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inl
          (Iso.inv (hb.isLimit.conePointUniqueUpToIso (BinaryBiproduct.isLimit X Y))) ≫
        b.toCone.π.app j =
      CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inl (desc b.inl b.inr) ≫ b.toCone.π.app j
⊢ Eq (α := Cone.pt.{0, uC', 0, uC} (BinaryBicone.toCone (BinaryBiproduct.bicone X Y)) ⟶ b.toCone.pt)
    (Iso.inv (hb.isLimit.conePointUniqueUpToIso (BinaryBiproduct.isLimit X Y))) (desc b.inl b.inr)
have refine_2 : ∀ (j : Discrete WalkingPair),
  CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inr
        (Iso.inv (hb.isLimit.conePointUniqueUpToIso (BinaryBiproduct.isLimit X Y))) ≫
      b.toCone.π.app j =
    CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inr (desc b.inl b.inr) ≫ b.toCone.π.app j
Tactic: refine biprod.hom_ext' _ _ (hb.isLimit.hom_ext fun j => ?_) (hb.isLimit.hom_ext fun j => ?_)
-- 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
X Y : C
inst_2 : HasBinaryBiproduct.{uC', uC} X Y
b : BinaryBicone.{uC', uC} X Y
hb : b.IsBilimit
j : Discrete WalkingPair
⊢ CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inl
        (Iso.inv (hb.isLimit.conePointUniqueUpToIso (BinaryBiproduct.isLimit X Y))) ≫
      b.toCone.π.app j =
    CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inl (desc b.inl b.inr) ≫ b.toCone.π.app j
have refine_1 : CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inl
    (NatTrans.app (Cone.π (BinaryBicone.toCone (BinaryBiproduct.bicone X Y))) j) =
  CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inl (desc b.inl b.inr ≫ b.toCone.π.app j)
Tactic: simp only [Category.assoc, IsLimit.conePointUniqueUpToIso_inv_comp]
-- 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
X Y : C
inst_2 : HasBinaryBiproduct.{uC', uC} X Y
b : BinaryBicone.{uC', uC} X Y
hb : b.IsBilimit
j : Discrete WalkingPair
⊢ CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inl
      (NatTrans.app (Cone.π (BinaryBicone.toCone (BinaryBiproduct.bicone X Y))) j) =
    CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inl (desc b.inl b.inr ≫ b.toCone.π.app j)
have refine_1 : Eq (α := X ⟶ obj.{0, uC', 0, uC} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair })
  (CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inl
    (NatTrans.app (Cone.π (BinaryBicone.toCone (BinaryBiproduct.bicone X Y))) { as := WalkingPair.left }))
  (CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inl (desc b.inl b.inr ≫ b.toCone.π.app { as := WalkingPair.left }))
Tactic: rcases j with ⟨⟨⟩⟩
Cleared hypotheses: j
-- 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
X Y : C
inst_2 : HasBinaryBiproduct.{uC', uC} X Y
b : BinaryBicone.{uC', uC} X Y
hb : b.IsBilimit
j : Discrete WalkingPair
refine_1 :
  Eq (α := X ⟶ obj.{0, uC', 0, uC} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair })
    (CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inl
      (NatTrans.app (Cone.π (BinaryBicone.toCone (BinaryBiproduct.bicone X Y))) { as := WalkingPair.left }))
    (CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inl (desc b.inl b.inr ≫ b.toCone.π.app { as := WalkingPair.left }))
⊢ CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inl
      (NatTrans.app (Cone.π (BinaryBicone.toCone (BinaryBiproduct.bicone X Y))) j) =
    CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inl (desc b.inl b.inr ≫ b.toCone.π.app j)
have refine_1₁ : Eq (α := X ⟶ obj.{0, uC', 0, uC} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair })
  (CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inl
    (NatTrans.app (Cone.π (BinaryBicone.toCone (BinaryBiproduct.bicone X Y))) { as := WalkingPair.right }))
  (CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inl (desc b.inl b.inr ≫ b.toCone.π.app { as := WalkingPair.right }))
Tactic: rcases j with ⟨⟨⟩⟩
Cleared hypotheses: j
-- 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
X Y : C
inst_2 : HasBinaryBiproduct.{uC', uC} X Y
b : BinaryBicone.{uC', uC} X Y
hb : b.IsBilimit
j : Discrete WalkingPair
⊢ CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inr
        (Iso.inv (hb.isLimit.conePointUniqueUpToIso (BinaryBiproduct.isLimit X Y))) ≫
      b.toCone.π.app j =
    CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inr (desc b.inl b.inr) ≫ b.toCone.π.app j
have refine_2 : CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inr
    (NatTrans.app (Cone.π (BinaryBicone.toCone (BinaryBiproduct.bicone X Y))) j) =
  CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inr (desc b.inl b.inr ≫ b.toCone.π.app j)
Tactic: simp only [Category.assoc, IsLimit.conePointUniqueUpToIso_inv_comp]
-- 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
X Y : C
inst_2 : HasBinaryBiproduct.{uC', uC} X Y
b : BinaryBicone.{uC', uC} X Y
hb : b.IsBilimit
j : Discrete WalkingPair
⊢ CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inr
      (NatTrans.app (Cone.π (BinaryBicone.toCone (BinaryBiproduct.bicone X Y))) j) =
    CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inr (desc b.inl b.inr ≫ b.toCone.π.app j)
have refine_2 : Eq (α := Y ⟶ obj.{0, uC', 0, uC} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair })
  (CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inr
    (NatTrans.app (Cone.π (BinaryBicone.toCone (BinaryBiproduct.bicone X Y))) { as := WalkingPair.left }))
  (CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inr (desc b.inl b.inr ≫ b.toCone.π.app { as := WalkingPair.left }))
Tactic: rcases j with ⟨⟨⟩⟩
Cleared hypotheses: j
-- 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
X Y : C
inst_2 : HasBinaryBiproduct.{uC', uC} X Y
b : BinaryBicone.{uC', uC} X Y
hb : b.IsBilimit
j : Discrete WalkingPair
refine_2 :
  Eq (α := Y ⟶ obj.{0, uC', 0, uC} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair })
    (CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inr
      (NatTrans.app (Cone.π (BinaryBicone.toCone (BinaryBiproduct.bicone X Y))) { as := WalkingPair.left }))
    (CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inr (desc b.inl b.inr ≫ b.toCone.π.app { as := WalkingPair.left }))
⊢ CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inr
      (NatTrans.app (Cone.π (BinaryBicone.toCone (BinaryBiproduct.bicone X Y))) j) =
    CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inr (desc b.inl b.inr ≫ b.toCone.π.app j)
have refine_2₁ : Eq (α := Y ⟶ obj.{0, uC', 0, uC} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair })
  (CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inr
    (NatTrans.app (Cone.π (BinaryBicone.toCone (BinaryBiproduct.bicone X Y))) { as := WalkingPair.right }))
  (CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inr (desc b.inl b.inr ≫ b.toCone.π.app { as := WalkingPair.right }))
Tactic: rcases j with ⟨⟨⟩⟩
Cleared hypotheses: j
-- 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
b : BinaryBicone.{uC', uC} X Y
hb : b.IsBilimit
⊢ CategoryStruct.comp (Y := biprod.{uC', uC} X Y) (lift b.fst b.snd) (desc b.inl b.inr) = 𝟙 b.pt
have rw : CategoryStruct.comp (Y := biprod.{uC', uC} X Y)
    (Iso.hom (hb.isLimit.conePointUniqueUpToIso (BinaryBiproduct.isLimit X Y))) (desc b.inl b.inr) =
  𝟙 b.pt
Tactic: rw [← biprod.conePointUniqueUpToIso_hom X Y hb, ←
      biprod.conePointUniqueUpToIso_inv X Y hb, Iso.hom_inv_id]
-- 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
b : BinaryBicone.{uC', uC} X Y
hb : b.IsBilimit
rw :
  CategoryStruct.comp (Y := biprod.{uC', uC} X Y)
      (Iso.hom (hb.isLimit.conePointUniqueUpToIso (BinaryBiproduct.isLimit X Y))) (desc b.inl b.inr) =
    𝟙 b.pt
⊢ CategoryStruct.comp (Y := biprod.{uC', uC} X Y) (lift b.fst b.snd) (desc b.inl b.inr) = 𝟙 b.pt
have rw₁ : CategoryStruct.comp (Y := biprod.{uC', uC} X Y)
    (Iso.hom (hb.isLimit.conePointUniqueUpToIso (BinaryBiproduct.isLimit X Y)))
    (Iso.inv (hb.isLimit.conePointUniqueUpToIso (BinaryBiproduct.isLimit X Y))) =
  𝟙 b.pt
Tactic: rw [← biprod.conePointUniqueUpToIso_hom X Y hb, ←
      biprod.conePointUniqueUpToIso_inv X Y hb, Iso.hom_inv_id]
-- 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
b : BinaryBicone.{uC', uC} X Y
hb : b.IsBilimit
rw :
  CategoryStruct.comp (Y := biprod.{uC', uC} X Y)
      (Iso.hom (hb.isLimit.conePointUniqueUpToIso (BinaryBiproduct.isLimit X Y))) (desc b.inl b.inr) =
    𝟙 b.pt
rw₁ :
  CategoryStruct.comp (Y := biprod.{uC', uC} X Y)
      (Iso.hom (hb.isLimit.conePointUniqueUpToIso (BinaryBiproduct.isLimit X Y)))
      (Iso.inv (hb.isLimit.conePointUniqueUpToIso (BinaryBiproduct.isLimit X Y))) =
    𝟙 b.pt
⊢ CategoryStruct.comp (Y := biprod.{uC', uC} X Y) (lift b.fst b.snd) (desc b.inl b.inr) = 𝟙 b.pt
have rw₂ : Eq.{uC' + 1} (α := b.pt ⟶ b.pt) (𝟙 b.pt) (𝟙 b.pt)
Tactic: rw [← biprod.conePointUniqueUpToIso_hom X Y hb, ←
      biprod.conePointUniqueUpToIso_inv X Y hb, Iso.hom_inv_id]
-- 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
b : BinaryBicone.{uC', uC} X Y
hb : b.IsBilimit
⊢ desc b.inl b.inr ≫ lift b.fst b.snd = 𝟙 (biprod.{uC', uC} X Y)
have rw : desc b.inl b.inr ≫ Iso.hom (hb.isLimit.conePointUniqueUpToIso (BinaryBiproduct.isLimit X Y)) = 𝟙 (biprod.{uC', uC} X Y)
Tactic: rw [← biprod.conePointUniqueUpToIso_hom X Y hb, ←
      biprod.conePointUniqueUpToIso_inv X Y hb, Iso.inv_hom_id]
-- 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
b : BinaryBicone.{uC', uC} X Y
hb : b.IsBilimit
rw :
  desc b.inl b.inr ≫ Iso.hom (hb.isLimit.conePointUniqueUpToIso (BinaryBiproduct.isLimit X Y)) =
    𝟙 (biprod.{uC', uC} X Y)
⊢ desc b.inl b.inr ≫ lift b.fst b.snd = 𝟙 (biprod.{uC', uC} X Y)
have rw₁ : Iso.inv (hb.isLimit.conePointUniqueUpToIso (BinaryBiproduct.isLimit X Y)) ≫
    Iso.hom (hb.isLimit.conePointUniqueUpToIso (BinaryBiproduct.isLimit X Y)) =
  𝟙 (biprod.{uC', uC} X Y)
Tactic: rw [← biprod.conePointUniqueUpToIso_hom X Y hb, ←
      biprod.conePointUniqueUpToIso_inv X Y hb, Iso.inv_hom_id]
-- 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
b : BinaryBicone.{uC', uC} X Y
hb : b.IsBilimit
rw :
  desc b.inl b.inr ≫ Iso.hom (hb.isLimit.conePointUniqueUpToIso (BinaryBiproduct.isLimit X Y)) =
    𝟙 (biprod.{uC', uC} X Y)
rw₁ :
  Iso.inv (hb.isLimit.conePointUniqueUpToIso (BinaryBiproduct.isLimit X Y)) ≫
      Iso.hom (hb.isLimit.conePointUniqueUpToIso (BinaryBiproduct.isLimit X Y)) =
    𝟙 (biprod.{uC', uC} X Y)
⊢ desc b.inl b.inr ≫ lift b.fst b.snd = 𝟙 (biprod.{uC', uC} X Y)
have rw₂ : Eq.{uC' + 1} (α := biprod.{uC', uC} X Y ⟶ biprod.{uC', uC} X Y) (𝟙 (biprod.{uC', uC} X Y)) (𝟙 (biprod.{uC', uC} X Y))
Tactic: rw [← biprod.conePointUniqueUpToIso_hom X Y hb, ←
      biprod.conePointUniqueUpToIso_inv X Y hb, Iso.inv_hom_id]
-- 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
X Y : C
inst_2 : HasBinaryBiproduct.{uC', uC} X Y
⊢ IsIso.{uC', uC} (C := C) (X := X) (Y := biprod.{uC', uC} X Y) inl ↔ 𝟙 (biprod.{uC', uC} X Y) = fst ≫ inl
have mp : IsIso.{uC', uC} (C := C) (X := X) (Y := biprod.{uC', uC} X Y) inl → 𝟙 (biprod.{uC', uC} X Y) = fst ≫ inl
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
X Y : C
inst_2 : HasBinaryBiproduct.{uC', uC} X Y
mp : IsIso.{uC', uC} (C := C) (X := X) (Y := biprod.{uC', uC} X Y) inl → 𝟙 (biprod.{uC', uC} X Y) = fst ≫ inl
⊢ IsIso.{uC', uC} (C := C) (X := X) (Y := biprod.{uC', uC} X Y) inl ↔ 𝟙 (biprod.{uC', uC} X Y) = fst ≫ inl
have mpr : 𝟙 (biprod.{uC', uC} X Y) = fst ≫ inl → IsIso.{uC', uC} (C := C) (X := X) (Y := biprod.{uC', uC} X Y) inl
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (hypothesis)
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
X Y : C
inst_2 : HasBinaryBiproduct.{uC', uC} X Y
h : IsIso.{uC', uC} (C := C) (X := X) (Y := biprod.{uC', uC} X Y) inl
⊢ 𝟙 (biprod.{uC', uC} X Y) = fst ≫ inl
have this : Eq.{uC' + 1} (α := biprod.{uC', uC} X Y ⟶ X) (inv inl ≫ CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inl fst)
  (inv inl ≫ 𝟙 X)
Tactic: have := (cancel_epi (inv biprod.inl : X ⊞ Y ⟶ X)).2 <| @biprod.inl_fst _ _ _ X Y _
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (hypothesis)
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
X Y : C
inst_2 : HasBinaryBiproduct.{uC', uC} X Y
h : IsIso.{uC', uC} (C := C) (X := X) (Y := biprod.{uC', uC} X Y) inl
this :
  Eq.{uC' + 1} (α := biprod.{uC', uC} X Y ⟶ X) (inv inl ≫ CategoryStruct.comp (Y := biprod.{uC', uC} X Y) inl fst)
    (inv inl ≫ 𝟙 X)
⊢ 𝟙 (biprod.{uC', uC} X Y) = fst ≫ inl
have this₁ : Eq.{uC' + 1} (α := biprod.{uC', uC} X Y ⟶ X) fst (inv inl)
Tactic: rw [IsIso.inv_hom_id_assoc, Category.comp_id] at this
Cleared hypotheses: this
-- 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
X Y : C
inst_2 : HasBinaryBiproduct.{uC', uC} X Y
h : IsIso.{uC', uC} (C := C) (X := X) (Y := biprod.{uC', uC} X Y) inl
this : Eq.{uC' + 1} (α := biprod.{uC', uC} X Y ⟶ X) fst (inv inl)
⊢ 𝟙 (biprod.{uC', uC} X Y) = fst ≫ inl
have mp : 𝟙 (biprod.{uC', uC} X Y) = inv inl ≫ inl
Tactic: rw [this, IsIso.inv_hom_id]
-- 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
X Y : C
inst_2 : HasBinaryBiproduct.{uC', uC} X Y
h : IsIso.{uC', uC} (C := C) (X := X) (Y := biprod.{uC', uC} X Y) inl
this : Eq.{uC' + 1} (α := biprod.{uC', uC} X Y ⟶ X) fst (inv inl)
mp : 𝟙 (biprod.{uC', uC} X Y) = inv inl ≫ inl
⊢ 𝟙 (biprod.{uC', uC} X Y) = fst ≫ inl
have mp₁ : Eq.{uC' + 1} (α := biprod.{uC', uC} X Y ⟶ biprod.{uC', uC} X Y) (𝟙 (biprod.{uC', uC} X Y)) (𝟙 (biprod.{uC', uC} X Y))
Tactic: rw [this, IsIso.inv_hom_id]
-- 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 W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst_4 : Epi f
inst_5 : Epi g
inst_6 : HasBinaryBiproduct.{uC', uC} W X
inst_7 : HasBinaryBiproduct.{uC', uC} Y Z
⊢ Epi (X := biprod.{uC', uC} W X) (Y := biprod.{uC', uC} Y Z) (map f g)
have rw : Epi (X := biprod.{uC', uC} W X) (Y := biprod.{uC', uC} Y Z)
  (Iso.hom (isoCoprod W X) ≫ coprod.map f g ≫ Iso.inv (isoCoprod Y Z))
Tactic: rw [show biprod.map f g =
    (biprod.isoCoprod _ _).hom ≫ coprod.map f g ≫ (biprod.isoCoprod _ _).inv by aesop]
-- 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 W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst_4 : Epi f
inst_5 : Epi g
inst_6 : HasBinaryBiproduct.{uC', uC} W X
inst_7 : HasBinaryBiproduct.{uC', uC} Y Z
⊢ Epi (X := prod.{uC', uC} W X) (Y := prod.{uC', uC} Y Z) (map f g)
have rw : Epi (X := prod.{uC', uC} W X) (Y := prod.{uC', uC} Y Z)
  (CategoryStruct.comp (Y := biprod.{uC', uC} W X) (Iso.inv (biprod.isoProd W X))
      (CategoryStruct.comp (Y := biprod.{uC', uC} Y Z) (biprod.map f g) (Iso.hom (biprod.isoProd Y Z))) :
    prod.{uC', uC} W X ⟶ prod.{uC', uC} Y Z)
Tactic: rw [show prod.map f g = (biprod.isoProd _ _).inv ≫ biprod.map f g ≫
    (biprod.isoProd _ _).hom by simp]
-- 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 W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst_4 : Mono f
inst_5 : Mono g
inst_6 : HasBinaryBiproduct.{uC', uC} W X
inst_7 : HasBinaryBiproduct.{uC', uC} Y Z
⊢ Mono (X := biprod.{uC', uC} W X) (Y := biprod.{uC', uC} Y Z) (map f g)
have rw : Mono (X := biprod.{uC', uC} W X) (Y := biprod.{uC', uC} Y Z)
  (Iso.hom (isoProd W X) ≫ prod.map f g ≫ Iso.inv (isoProd Y Z))
Tactic: rw [show biprod.map f g = (biprod.isoProd _ _).hom ≫ prod.map f g ≫
    (biprod.isoProd _ _).inv by aesop]
-- 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 W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst_4 : Mono f
inst_5 : Mono g
inst_6 : HasBinaryBiproduct.{uC', uC} W X
inst_7 : HasBinaryBiproduct.{uC', uC} Y Z
⊢ Mono (X := coprod.{uC', uC} W X) (Y := coprod.{uC', uC} Y Z) (map f g)
have rw : Mono (X := coprod.{uC', uC} W X) (Y := coprod.{uC', uC} Y Z)
  (CategoryStruct.comp (Y := biprod.{uC', uC} W X) (Iso.inv (biprod.isoCoprod W X))
      (CategoryStruct.comp (Y := biprod.{uC', uC} Y Z) (biprod.map f g) (Iso.hom (biprod.isoCoprod Y Z))) :
    coprod.{uC', uC} W X ⟶ coprod.{uC', uC} Y Z)
Tactic: rw [show coprod.map f g = (biprod.isoCoprod _ _).inv ≫ biprod.map f g ≫
    (biprod.isoCoprod _ _).hom by simp]
-- 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 : IsLimit c.toCone
s : Fork c.fst 0
⊢ (s.ι ≫ c.snd) ≫ Fork.ι c.fstKernelFork = s.ι
have h₁ : ((s.ι ≫ c.snd) ≫ Fork.ι c.fstKernelFork) ≫ BinaryFan.fst c.toCone = s.ι ≫ BinaryFan.fst c.toCone
Tactic: apply BinaryFan.IsLimit.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 : IsLimit c.toCone
s : Fork c.fst 0
h₁ : ((s.ι ≫ c.snd) ≫ Fork.ι c.fstKernelFork) ≫ BinaryFan.fst c.toCone = s.ι ≫ BinaryFan.fst c.toCone
⊢ (s.ι ≫ c.snd) ≫ Fork.ι c.fstKernelFork = s.ι
have h₂ : ((s.ι ≫ c.snd) ≫ Fork.ι c.fstKernelFork) ≫ BinaryFan.snd c.toCone = s.ι ≫ BinaryFan.snd c.toCone
Tactic: apply BinaryFan.IsLimit.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 : IsLimit c.toCone
s : Fork c.snd 0
⊢ (s.ι ≫ c.fst) ≫ Fork.ι c.sndKernelFork = s.ι
have h₁ : ((s.ι ≫ c.fst) ≫ Fork.ι c.sndKernelFork) ≫ BinaryFan.fst c.toCone = s.ι ≫ BinaryFan.fst c.toCone
Tactic: apply BinaryFan.IsLimit.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 : IsLimit c.toCone
s : Fork c.snd 0
h₁ : ((s.ι ≫ c.fst) ≫ Fork.ι c.sndKernelFork) ≫ BinaryFan.fst c.toCone = s.ι ≫ BinaryFan.fst c.toCone
⊢ (s.ι ≫ c.fst) ≫ Fork.ι c.sndKernelFork = s.ι
have h₂ : ((s.ι ≫ c.fst) ≫ Fork.ι c.sndKernelFork) ≫ BinaryFan.snd c.toCone = s.ι ≫ BinaryFan.snd c.toCone
Tactic: apply BinaryFan.IsLimit.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.inl 0
⊢ Cofork.π c.inlCokernelCofork ≫ c.inr ≫ s.π = s.π
have h₁ : BinaryCofan.inl c.toCocone ≫ Cofork.π c.inlCokernelCofork ≫ c.inr ≫ s.π = BinaryCofan.inl c.toCocone ≫ s.π
Tactic: apply BinaryCofan.IsColimit.hom_ext i