awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.PreservesZeroMorphisms
J : Type u_1
inst_5 : Finite J
f : J → C
inst_6 : HasBiproduct.{u_1, v, u} f
inst_7 : HasBiproduct.{u_1, v', u'} (F.obj ∘ f)
inst_8 :
  Mono (X := F.obj (biproduct.{u_1, v, u} f)) (Y := biproduct.{u_1, v', u'} (F.obj ∘ f)) (F.biproductComparison f)
this_1 : HasProduct.{u_1, v', u'} (C := D) fun (b : J) ↦ F.obj (f b)
that :
  Eq (α := F.obj (piObj.{u_1, v, u} f) ⟶ piObj.{u_1, v', u'} fun (b : J) ↦ F.obj (f b))
    (piComparison F f : F.obj (piObj.{u_1, v, u} f) ⟶ piObj.{u_1, v', u'} fun (b : J) ↦ F.obj (f b))
    (CategoryStruct.comp (Y := F.obj (biproduct.{u_1, v, u} f)) (Iso.inv (F.mapIso (biproduct.isoProduct f)))
        (CategoryStruct.comp (Y := biproduct.{u_1, v', u'} (F.obj ∘ f)) (F.biproductComparison f)
          (Iso.hom (biproduct.isoProduct (F.obj ∘ f)))) :
      F.obj (piObj.{u_1, v, u} f) ⟶ piObj.{u_1, v', u'} (F.obj ∘ f))
this : IsIso (X := F.obj (biproduct.{u_1, v, u} f)) (Y := biproduct.{u_1, v', u'} (F.obj ∘ f)) (F.biproductComparison f)
⊢ PreservesBiproduct f F
have this₁ : IsIso (X := F.obj (piObj.{u_1, v, u} f)) (Y := piObj.{u_1, v', u'} fun (b : J) ↦ F.obj (f b)) (piComparison F f)
Tactic: haveI : IsIso (piComparison F f) := by
    rw [that]
    infer_instance
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.PreservesZeroMorphisms
J : Type u_1
inst_5 : Finite J
f : J → C
inst_6 : HasBiproduct.{u_1, v, u} f
inst_7 : HasBiproduct.{u_1, v', u'} (F.obj ∘ f)
inst_8 :
  Mono (X := F.obj (biproduct.{u_1, v, u} f)) (Y := biproduct.{u_1, v', u'} (F.obj ∘ f)) (F.biproductComparison f)
this_1 : HasProduct.{u_1, v', u'} (C := D) fun (b : J) ↦ F.obj (f b)
that :
  Eq (α := F.obj (piObj.{u_1, v, u} f) ⟶ piObj.{u_1, v', u'} fun (b : J) ↦ F.obj (f b))
    (piComparison F f : F.obj (piObj.{u_1, v, u} f) ⟶ piObj.{u_1, v', u'} fun (b : J) ↦ F.obj (f b))
    (CategoryStruct.comp (Y := F.obj (biproduct.{u_1, v, u} f)) (Iso.inv (F.mapIso (biproduct.isoProduct f)))
        (CategoryStruct.comp (Y := biproduct.{u_1, v', u'} (F.obj ∘ f)) (F.biproductComparison f)
          (Iso.hom (biproduct.isoProduct (F.obj ∘ f)))) :
      F.obj (piObj.{u_1, v, u} f) ⟶ piObj.{u_1, v', u'} (F.obj ∘ f))
this_2 :
  IsIso (X := F.obj (biproduct.{u_1, v, u} f)) (Y := biproduct.{u_1, v', u'} (F.obj ∘ f)) (F.biproductComparison f)
this : IsIso (X := F.obj (piObj.{u_1, v, u} f)) (Y := piObj.{u_1, v', u'} fun (b : J) ↦ F.obj (f b)) (piComparison F f)
⊢ PreservesBiproduct f F
have this₁ : PreservesLimit (Discrete.functor f) F
Tactic: haveI := PreservesProduct.of_iso_comparison F f
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.PreservesZeroMorphisms
J : Type u_1
inst_5 : Finite J
f : J → C
inst_6 : HasBiproduct.{u_1, v, u} f
inst_7 : HasBiproduct.{u_1, v', u'} (F.obj ∘ f)
inst_8 :
  Epi (X := biproduct.{u_1, v', u'} (F.obj ∘ f)) (Y := F.obj (biproduct.{u_1, v, u} f)) (F.biproductComparison' f)
⊢ PreservesBiproduct f F
have this : Epi (X := biproduct.{u_1, v', u'} (F.obj ∘ f)) (Y := F.obj (biproduct.{u_1, v, u} f))
  (SplitEpi.section_ (F.splitEpiBiproductComparison f))
Tactic: haveI : Epi (splitEpiBiproductComparison F f).section_ := by simpa
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.PreservesZeroMorphisms
J : Type u_1
inst_5 : Finite J
f : J → C
inst_6 : HasBiproduct.{u_1, v, u} f
inst_7 : HasBiproduct.{u_1, v', u'} (F.obj ∘ f)
inst_8 :
  Epi (X := biproduct.{u_1, v', u'} (F.obj ∘ f)) (Y := F.obj (biproduct.{u_1, v, u} f)) (F.biproductComparison' f)
this :
  Epi (X := biproduct.{u_1, v', u'} (F.obj ∘ f)) (Y := F.obj (biproduct.{u_1, v, u} f))
    (SplitEpi.section_ (F.splitEpiBiproductComparison f))
⊢ PreservesBiproduct f F
have this₁ : IsIso (X := F.obj (biproduct.{u_1, v, u} f)) (Y := biproduct.{u_1, v', u'} (F.obj ∘ f)) (F.biproductComparison f)
Tactic: haveI : IsIso (biproductComparison F f) :=
    IsIso.of_epi_section' (splitEpiBiproductComparison F f)
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.PreservesZeroMorphisms
X Y : C
inst_5 : PreservesBinaryBiproduct X Y F
c : Cone.{0, v, 0, u} (pair X Y)
hc : IsLimit c
⊢ ((Cone.postcompose (diagramIsoPair (pair X Y ⋙ F)).inv).obj
        (BinaryBicone.toCone (F.mapBinaryBicone (BinaryBicone.ofLimitCone hc)))).pt ≅
    (F.mapCone c).pt
have dsimp : F.obj c.pt ≅ F.obj c.pt
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.PreservesZeroMorphisms
X Y : C
inst_5 : PreservesBinaryBiproduct X Y F
c : Cone.{0, v, 0, u} (pair X Y)
hc : IsLimit c
j : Discrete WalkingPair
⊢ ((Cone.postcompose (diagramIsoPair (pair X Y ⋙ F)).inv).obj
            (BinaryBicone.toCone (F.mapBinaryBicone (BinaryBicone.ofLimitCone hc)))).π.app
      j =
    Iso.hom (id (Iso.refl (F.obj c.pt))) ≫ (F.mapCone c).π.app j
have left : Eq (α :=
  obj.{0, v', 0, u'}
      (obj (const (Discrete WalkingPair))
        ((Cone.postcompose (diagramIsoPair (pair X Y ⋙ F)).inv).obj
            (BinaryBicone.toCone (F.mapBinaryBicone (BinaryBicone.ofLimitCone hc)))).pt)
      { as := WalkingPair.left : Discrete WalkingPair } ⟶
    (pair X Y ⋙ F).obj { as := WalkingPair.left })
  (((Cone.postcompose (diagramIsoPair (pair X Y ⋙ F)).inv).obj
          (BinaryBicone.toCone (F.mapBinaryBicone (BinaryBicone.ofLimitCone hc)))).π.app
    { as := WalkingPair.left })
  (Iso.hom (id (Iso.refl (F.obj c.pt))) ≫ (F.mapCone c).π.app { as := WalkingPair.left })
Tactic: rcases j with ⟨⟨⟩⟩
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.PreservesZeroMorphisms
X Y : C
inst_5 : PreservesBinaryBiproduct X Y F
c : Cone.{0, v, 0, u} (pair X Y)
hc : IsLimit c
j : Discrete WalkingPair
left :
  Eq (α :=
    obj.{0, v', 0, u'}
        (obj (const (Discrete WalkingPair))
          ((Cone.postcompose (diagramIsoPair (pair X Y ⋙ F)).inv).obj
              (BinaryBicone.toCone (F.mapBinaryBicone (BinaryBicone.ofLimitCone hc)))).pt)
        { as := WalkingPair.left : Discrete WalkingPair } ⟶
      (pair X Y ⋙ F).obj { as := WalkingPair.left })
    (((Cone.postcompose (diagramIsoPair (pair X Y ⋙ F)).inv).obj
            (BinaryBicone.toCone (F.mapBinaryBicone (BinaryBicone.ofLimitCone hc)))).π.app
      { as := WalkingPair.left })
    (Iso.hom (id (Iso.refl (F.obj c.pt))) ≫ (F.mapCone c).π.app { as := WalkingPair.left })
⊢ ((Cone.postcompose (diagramIsoPair (pair X Y ⋙ F)).inv).obj
            (BinaryBicone.toCone (F.mapBinaryBicone (BinaryBicone.ofLimitCone hc)))).π.app
      j =
    Iso.hom (id (Iso.refl (F.obj c.pt))) ≫ (F.mapCone c).π.app j
have right : Eq (α :=
  obj.{0, v', 0, u'}
      (obj (const (Discrete WalkingPair))
        ((Cone.postcompose (diagramIsoPair (pair X Y ⋙ F)).inv).obj
            (BinaryBicone.toCone (F.mapBinaryBicone (BinaryBicone.ofLimitCone hc)))).pt)
      { as := WalkingPair.right : Discrete WalkingPair } ⟶
    (pair X Y ⋙ F).obj { as := WalkingPair.right })
  (((Cone.postcompose (diagramIsoPair (pair X Y ⋙ F)).inv).obj
          (BinaryBicone.toCone (F.mapBinaryBicone (BinaryBicone.ofLimitCone hc)))).π.app
    { as := WalkingPair.right })
  (Iso.hom (id (Iso.refl (F.obj c.pt))) ≫ (F.mapCone c).π.app { as := WalkingPair.right })
Tactic: rcases j with ⟨⟨⟩⟩
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.PreservesZeroMorphisms
X Y : C
inst_5 : PreservesLimit (pair X Y) F
b : BinaryBicone.{v, u} X Y
hb : b.IsBilimit
⊢ ((Cone.postcompose (diagramIsoPair (pair X Y ⋙ F)).hom).obj (F.mapCone b.toCone)).pt ≅
    (BinaryBicone.toCone (F.mapBinaryBicone b)).pt
have dsimp : F.obj b.pt ≅ F.obj b.pt
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.PreservesZeroMorphisms
X Y : C
inst_5 : PreservesLimit (pair X Y) F
b : BinaryBicone.{v, u} X Y
hb : b.IsBilimit
j : Discrete WalkingPair
⊢ ((Cone.postcompose (diagramIsoPair (pair X Y ⋙ F)).hom).obj (F.mapCone b.toCone)).π.app j =
    Iso.hom (id (Iso.refl (F.obj b.pt))) ≫ (BinaryBicone.toCone (F.mapBinaryBicone b)).π.app j
have left : Eq (α :=
  obj.{0, v', 0, u'}
      (obj (const (Discrete WalkingPair))
        ((Cone.postcompose (diagramIsoPair (pair X Y ⋙ F)).hom).obj (F.mapCone b.toCone)).pt)
      { as := WalkingPair.left : Discrete WalkingPair } ⟶
    obj.{0, v', 0, u'}
      (pair ((pair X Y ⋙ F).obj { as := WalkingPair.left }) ((pair X Y ⋙ F).obj { as := WalkingPair.right }))
      { as := WalkingPair.left : Discrete WalkingPair })
  (((Cone.postcompose (diagramIsoPair (pair X Y ⋙ F)).hom).obj (F.mapCone b.toCone)).π.app { as := WalkingPair.left })
  (Iso.hom (id (Iso.refl (F.obj b.pt))) ≫ (BinaryBicone.toCone (F.mapBinaryBicone b)).π.app { as := WalkingPair.left })
Tactic: rcases j with ⟨⟨⟩⟩
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.PreservesZeroMorphisms
X Y : C
inst_5 : PreservesLimit (pair X Y) F
b : BinaryBicone.{v, u} X Y
hb : b.IsBilimit
j : Discrete WalkingPair
left :
  Eq (α :=
    obj.{0, v', 0, u'}
        (obj (const (Discrete WalkingPair))
          ((Cone.postcompose (diagramIsoPair (pair X Y ⋙ F)).hom).obj (F.mapCone b.toCone)).pt)
        { as := WalkingPair.left : Discrete WalkingPair } ⟶
      obj.{0, v', 0, u'}
        (pair ((pair X Y ⋙ F).obj { as := WalkingPair.left }) ((pair X Y ⋙ F).obj { as := WalkingPair.right }))
        { as := WalkingPair.left : Discrete WalkingPair })
    (((Cone.postcompose (diagramIsoPair (pair X Y ⋙ F)).hom).obj (F.mapCone b.toCone)).π.app { as := WalkingPair.left })
    (Iso.hom (id (Iso.refl (F.obj b.pt))) ≫
      (BinaryBicone.toCone (F.mapBinaryBicone b)).π.app { as := WalkingPair.left })
⊢ ((Cone.postcompose (diagramIsoPair (pair X Y ⋙ F)).hom).obj (F.mapCone b.toCone)).π.app j =
    Iso.hom (id (Iso.refl (F.obj b.pt))) ≫ (BinaryBicone.toCone (F.mapBinaryBicone b)).π.app j
have right : Eq (α :=
  obj.{0, v', 0, u'}
      (obj (const (Discrete WalkingPair))
        ((Cone.postcompose (diagramIsoPair (pair X Y ⋙ F)).hom).obj (F.mapCone b.toCone)).pt)
      { as := WalkingPair.right : Discrete WalkingPair } ⟶
    obj.{0, v', 0, u'}
      (pair ((pair X Y ⋙ F).obj { as := WalkingPair.left }) ((pair X Y ⋙ F).obj { as := WalkingPair.right }))
      { as := WalkingPair.right : Discrete WalkingPair })
  (((Cone.postcompose (diagramIsoPair (pair X Y ⋙ F)).hom).obj (F.mapCone b.toCone)).π.app { as := WalkingPair.right })
  (Iso.hom (id (Iso.refl (F.obj b.pt))) ≫ (BinaryBicone.toCone (F.mapBinaryBicone b)).π.app { as := WalkingPair.right })
Tactic: rcases j with ⟨⟨⟩⟩
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.PreservesZeroMorphisms
X Y : C
inst_5 : HasBinaryBiproduct.{v, u} X Y
inst_6 : HasBinaryBiproduct.{v', u'} (F.obj X) (F.obj Y)
inst_7 : Mono (X := F.obj (biprod.{v, u} X Y)) (Y := biprod.{v', u'} (F.obj X) (F.obj Y)) (F.biprodComparison X Y)
⊢ Eq (α := F.obj (prod.{v, u} X Y) ⟶ prod.{v', u'} (F.obj X) (F.obj Y))
    (prodComparison F X Y : F.obj (prod.{v, u} X Y) ⟶ prod.{v', u'} (F.obj X) (F.obj Y))
    (CategoryStruct.comp (Y := F.obj (biprod.{v, u} X Y)) (Iso.inv (F.mapIso (biprod.isoProd X Y)))
        (CategoryStruct.comp (Y := biprod.{v', u'} (F.obj X) (F.obj Y)) (F.biprodComparison X Y)
          (Iso.hom (biprod.isoProd (F.obj X) (F.obj Y)))) :
      F.obj (prod.{v, u} X Y) ⟶ prod.{v', u'} (F.obj X) (F.obj Y))
have h₁ : Eq (α := F.obj (prod.{v, u} X Y) ⟶ F.obj X)
  (CategoryStruct.comp (Y := prod.{v', u'} (F.obj X) (F.obj Y)) (prodComparison F X Y) prod.fst :
    F.obj (prod.{v, u} X Y) ⟶ F.obj X)
  (CategoryStruct.comp (Y := prod.{v', u'} (F.obj X) (F.obj Y))
      (CategoryStruct.comp (Y := F.obj (biprod.{v, u} X Y)) (Iso.inv (F.mapIso (biprod.isoProd X Y)))
          (CategoryStruct.comp (Y := biprod.{v', u'} (F.obj X) (F.obj Y)) (F.biprodComparison X Y)
            (Iso.hom (biprod.isoProd (F.obj X) (F.obj Y)))) :
        F.obj (prod.{v, u} X Y) ⟶ prod.{v', u'} (F.obj X) (F.obj Y))
      (prod.fst : prod.{v', u'} (F.obj X) (F.obj Y) ⟶ F.obj X) :
    F.obj (prod.{v, u} X Y) ⟶ F.obj X)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.PreservesZeroMorphisms
X Y : C
inst_5 : HasBinaryBiproduct.{v, u} X Y
inst_6 : HasBinaryBiproduct.{v', u'} (F.obj X) (F.obj Y)
inst_7 : Mono (X := F.obj (biprod.{v, u} X Y)) (Y := biprod.{v', u'} (F.obj X) (F.obj Y)) (F.biprodComparison X Y)
h₁ :
  Eq (α := F.obj (prod.{v, u} X Y) ⟶ F.obj X)
    (CategoryStruct.comp (Y := prod.{v', u'} (F.obj X) (F.obj Y)) (prodComparison F X Y) prod.fst :
      F.obj (prod.{v, u} X Y) ⟶ F.obj X)
    (CategoryStruct.comp (Y := prod.{v', u'} (F.obj X) (F.obj Y))
        (CategoryStruct.comp (Y := F.obj (biprod.{v, u} X Y)) (Iso.inv (F.mapIso (biprod.isoProd X Y)))
            (CategoryStruct.comp (Y := biprod.{v', u'} (F.obj X) (F.obj Y)) (F.biprodComparison X Y)
              (Iso.hom (biprod.isoProd (F.obj X) (F.obj Y)))) :
          F.obj (prod.{v, u} X Y) ⟶ prod.{v', u'} (F.obj X) (F.obj Y))
        (prod.fst : prod.{v', u'} (F.obj X) (F.obj Y) ⟶ F.obj X) :
      F.obj (prod.{v, u} X Y) ⟶ F.obj X)
⊢ Eq (α := F.obj (prod.{v, u} X Y) ⟶ prod.{v', u'} (F.obj X) (F.obj Y))
    (prodComparison F X Y : F.obj (prod.{v, u} X Y) ⟶ prod.{v', u'} (F.obj X) (F.obj Y))
    (CategoryStruct.comp (Y := F.obj (biprod.{v, u} X Y)) (Iso.inv (F.mapIso (biprod.isoProd X Y)))
        (CategoryStruct.comp (Y := biprod.{v', u'} (F.obj X) (F.obj Y)) (F.biprodComparison X Y)
          (Iso.hom (biprod.isoProd (F.obj X) (F.obj Y)))) :
      F.obj (prod.{v, u} X Y) ⟶ prod.{v', u'} (F.obj X) (F.obj Y))
have h₂ : Eq (α := F.obj (prod.{v, u} X Y) ⟶ F.obj Y)
  (CategoryStruct.comp (Y := prod.{v', u'} (F.obj X) (F.obj Y)) (prodComparison F X Y) prod.snd :
    F.obj (prod.{v, u} X Y) ⟶ F.obj Y)
  (CategoryStruct.comp (Y := prod.{v', u'} (F.obj X) (F.obj Y))
      (CategoryStruct.comp (Y := F.obj (biprod.{v, u} X Y)) (Iso.inv (F.mapIso (biprod.isoProd X Y)))
          (CategoryStruct.comp (Y := biprod.{v', u'} (F.obj X) (F.obj Y)) (F.biprodComparison X Y)
            (Iso.hom (biprod.isoProd (F.obj X) (F.obj Y)))) :
        F.obj (prod.{v, u} X Y) ⟶ prod.{v', u'} (F.obj X) (F.obj Y))
      (prod.snd : prod.{v', u'} (F.obj X) (F.obj Y) ⟶ F.obj Y) :
    F.obj (prod.{v, u} X Y) ⟶ F.obj Y)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.PreservesZeroMorphisms
X Y : C
inst_5 : HasBinaryBiproduct.{v, u} X Y
inst_6 : HasBinaryBiproduct.{v', u'} (F.obj X) (F.obj Y)
inst_7 : Mono (X := F.obj (biprod.{v, u} X Y)) (Y := biprod.{v', u'} (F.obj X) (F.obj Y)) (F.biprodComparison X Y)
⊢ PreservesBinaryBiproduct X Y F
have that : Eq (α := F.obj (prod.{v, u} X Y) ⟶ prod.{v', u'} (F.obj X) (F.obj Y))
  (prodComparison F X Y : F.obj (prod.{v, u} X Y) ⟶ prod.{v', u'} (F.obj X) (F.obj Y))
  (CategoryStruct.comp (Y := F.obj (biprod.{v, u} X Y)) (Iso.inv (F.mapIso (biprod.isoProd X Y)))
      (CategoryStruct.comp (Y := biprod.{v', u'} (F.obj X) (F.obj Y)) (F.biprodComparison X Y)
        (Iso.hom (biprod.isoProd (F.obj X) (F.obj Y)))) :
    F.obj (prod.{v, u} X Y) ⟶ prod.{v', u'} (F.obj X) (F.obj Y))
Tactic: have that :
    prodComparison F X Y =
      (F.mapIso (biprod.isoProd X Y)).inv ≫ biprodComparison F X Y ≫ (biprod.isoProd _ _).hom := by
    ext <;> simp [← Functor.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.PreservesZeroMorphisms
X Y : C
inst_5 : HasBinaryBiproduct.{v, u} X Y
inst_6 : HasBinaryBiproduct.{v', u'} (F.obj X) (F.obj Y)
inst_7 : Mono (X := F.obj (biprod.{v, u} X Y)) (Y := biprod.{v', u'} (F.obj X) (F.obj Y)) (F.biprodComparison X Y)
that :
  Eq (α := F.obj (prod.{v, u} X Y) ⟶ prod.{v', u'} (F.obj X) (F.obj Y))
    (prodComparison F X Y : F.obj (prod.{v, u} X Y) ⟶ prod.{v', u'} (F.obj X) (F.obj Y))
    (CategoryStruct.comp (Y := F.obj (biprod.{v, u} X Y)) (Iso.inv (F.mapIso (biprod.isoProd X Y)))
        (CategoryStruct.comp (Y := biprod.{v', u'} (F.obj X) (F.obj Y)) (F.biprodComparison X Y)
          (Iso.hom (biprod.isoProd (F.obj X) (F.obj Y)))) :
      F.obj (prod.{v, u} X Y) ⟶ prod.{v', u'} (F.obj X) (F.obj Y))
⊢ PreservesBinaryBiproduct X Y F
have this : IsIso (X := F.obj (biprod.{v, u} X Y)) (Y := biprod.{v', u'} (F.obj X) (F.obj Y)) (F.biprodComparison X Y)
Tactic: haveI : IsIso (biprodComparison F X Y) := isIso_of_mono_of_isSplitEpi _
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.PreservesZeroMorphisms
X Y : C
inst_5 : HasBinaryBiproduct.{v, u} X Y
inst_6 : HasBinaryBiproduct.{v', u'} (F.obj X) (F.obj Y)
inst_7 : Mono (X := F.obj (biprod.{v, u} X Y)) (Y := biprod.{v', u'} (F.obj X) (F.obj Y)) (F.biprodComparison X Y)
that :
  Eq (α := F.obj (prod.{v, u} X Y) ⟶ prod.{v', u'} (F.obj X) (F.obj Y))
    (prodComparison F X Y : F.obj (prod.{v, u} X Y) ⟶ prod.{v', u'} (F.obj X) (F.obj Y))
    (CategoryStruct.comp (Y := F.obj (biprod.{v, u} X Y)) (Iso.inv (F.mapIso (biprod.isoProd X Y)))
        (CategoryStruct.comp (Y := biprod.{v', u'} (F.obj X) (F.obj Y)) (F.biprodComparison X Y)
          (Iso.hom (biprod.isoProd (F.obj X) (F.obj Y)))) :
      F.obj (prod.{v, u} X Y) ⟶ prod.{v', u'} (F.obj X) (F.obj Y))
this : IsIso (X := F.obj (biprod.{v, u} X Y)) (Y := biprod.{v', u'} (F.obj X) (F.obj Y)) (F.biprodComparison X Y)
⊢ IsIso (X := F.obj (prod.{v, u} X Y)) (Y := prod.{v', u'} (F.obj X) (F.obj Y)) (prodComparison F X Y)
have rw : IsIso (X := F.obj (prod.{v, u} X Y)) (Y := prod.{v', u'} (F.obj X) (F.obj Y))
  (CategoryStruct.comp (Y := F.obj (biprod.{v, u} X Y)) (Iso.inv (F.mapIso (biprod.isoProd X Y)))
      (CategoryStruct.comp (Y := biprod.{v', u'} (F.obj X) (F.obj Y)) (F.biprodComparison X Y)
        (Iso.hom (biprod.isoProd (F.obj X) (F.obj Y)))) :
    F.obj (prod.{v, u} X Y) ⟶ prod.{v', u'} (F.obj X) (F.obj Y))
Tactic: rw [that]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.PreservesZeroMorphisms
X Y : C
inst_5 : HasBinaryBiproduct.{v, u} X Y
inst_6 : HasBinaryBiproduct.{v', u'} (F.obj X) (F.obj Y)
inst_7 : Mono (X := F.obj (biprod.{v, u} X Y)) (Y := biprod.{v', u'} (F.obj X) (F.obj Y)) (F.biprodComparison X Y)
that :
  Eq (α := F.obj (prod.{v, u} X Y) ⟶ prod.{v', u'} (F.obj X) (F.obj Y))
    (prodComparison F X Y : F.obj (prod.{v, u} X Y) ⟶ prod.{v', u'} (F.obj X) (F.obj Y))
    (CategoryStruct.comp (Y := F.obj (biprod.{v, u} X Y)) (Iso.inv (F.mapIso (biprod.isoProd X Y)))
        (CategoryStruct.comp (Y := biprod.{v', u'} (F.obj X) (F.obj Y)) (F.biprodComparison X Y)
          (Iso.hom (biprod.isoProd (F.obj X) (F.obj Y)))) :
      F.obj (prod.{v, u} X Y) ⟶ prod.{v', u'} (F.obj X) (F.obj Y))
this : IsIso (X := F.obj (biprod.{v, u} X Y)) (Y := biprod.{v', u'} (F.obj X) (F.obj Y)) (F.biprodComparison X Y)
⊢ PreservesBinaryBiproduct X Y F
have this₁ : IsIso (X := F.obj (prod.{v, u} X Y)) (Y := prod.{v', u'} (F.obj X) (F.obj Y)) (prodComparison F X Y)
Tactic: haveI : IsIso (prodComparison F X Y) := by
    rw [that]
    infer_instance
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.PreservesZeroMorphisms
X Y : C
inst_5 : HasBinaryBiproduct.{v, u} X Y
inst_6 : HasBinaryBiproduct.{v', u'} (F.obj X) (F.obj Y)
inst_7 : Mono (X := F.obj (biprod.{v, u} X Y)) (Y := biprod.{v', u'} (F.obj X) (F.obj Y)) (F.biprodComparison X Y)
that :
  Eq (α := F.obj (prod.{v, u} X Y) ⟶ prod.{v', u'} (F.obj X) (F.obj Y))
    (prodComparison F X Y : F.obj (prod.{v, u} X Y) ⟶ prod.{v', u'} (F.obj X) (F.obj Y))
    (CategoryStruct.comp (Y := F.obj (biprod.{v, u} X Y)) (Iso.inv (F.mapIso (biprod.isoProd X Y)))
        (CategoryStruct.comp (Y := biprod.{v', u'} (F.obj X) (F.obj Y)) (F.biprodComparison X Y)
          (Iso.hom (biprod.isoProd (F.obj X) (F.obj Y)))) :
      F.obj (prod.{v, u} X Y) ⟶ prod.{v', u'} (F.obj X) (F.obj Y))
this_1 : IsIso (X := F.obj (biprod.{v, u} X Y)) (Y := biprod.{v', u'} (F.obj X) (F.obj Y)) (F.biprodComparison X Y)
this : IsIso (X := F.obj (prod.{v, u} X Y)) (Y := prod.{v', u'} (F.obj X) (F.obj Y)) (prodComparison F X Y)
⊢ PreservesBinaryBiproduct X Y F
have this₁ : PreservesLimit (pair X Y) F
Tactic: haveI := PreservesLimitPair.of_iso_prod_comparison F X Y
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.PreservesZeroMorphisms
X Y : C
inst_5 : HasBinaryBiproduct.{v, u} X Y
inst_6 : HasBinaryBiproduct.{v', u'} (F.obj X) (F.obj Y)
inst_7 : Epi (X := biprod.{v', u'} (F.obj X) (F.obj Y)) (Y := F.obj (biprod.{v, u} X Y)) (F.biprodComparison' X Y)
⊢ PreservesBinaryBiproduct X Y F
have this : Epi (X := biprod.{v', u'} (F.obj X) (F.obj Y)) (Y := F.obj (biprod.{v, u} X Y))
  (SplitEpi.section_ (F.splitEpiBiprodComparison X Y))
Tactic: haveI : Epi (splitEpiBiprodComparison F X Y).section_ := by simpa