awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
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)
⊢ 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
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
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)
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))
⊢ 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_epi_section' (splitEpiBiprodComparison F X Y)
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
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)
this_1 :
  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))
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

Tactic:
apply preservesBinaryBiproduct_of_mono_biprodComparison

Premises used: CategoryTheory.Limits.preservesBinaryBiproduct_of_mono_biprodComparison
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
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 : Cocone.{0, v, 0, u} (pair X Y)
hc : IsColimit c
dsimp : F.obj c.pt ≅ F.obj c.pt
⊢ ((Cocone.precompose (diagramIsoPair (pair X Y ⋙ F)).hom).obj
        (BinaryBicone.toCocone (F.mapBinaryBicone (BinaryBicone.ofColimitCocone hc)))).pt ≅
    (F.mapCocone c).pt

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
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 : Cocone.{0, v, 0, u} (pair X Y)
hc : IsColimit c
⊢ F.obj c.pt ≅ F.obj c.pt

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
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 : Cocone.{0, v, 0, u} (pair X Y)
hc : IsColimit c
j : Discrete WalkingPair
left :
  Eq (α := (pair X Y ⋙ F).obj { as := WalkingPair.left : Discrete WalkingPair } ⟶ (F.mapCocone c).pt)
    (((Cocone.precompose (diagramIsoPair (pair X Y ⋙ F)).hom).obj
              (BinaryBicone.toCocone (F.mapBinaryBicone (BinaryBicone.ofColimitCocone hc)))).ι.app
        { as := WalkingPair.left : Discrete WalkingPair } ≫
      Iso.hom (id (Iso.refl (F.obj c.pt))))
    ((F.mapCocone c).ι.app { as := WalkingPair.left })
right :
  Eq (α := (pair X Y ⋙ F).obj { as := WalkingPair.right : Discrete WalkingPair } ⟶ (F.mapCocone c).pt)
    (((Cocone.precompose (diagramIsoPair (pair X Y ⋙ F)).hom).obj
              (BinaryBicone.toCocone (F.mapBinaryBicone (BinaryBicone.ofColimitCocone hc)))).ι.app
        { as := WalkingPair.right : Discrete WalkingPair } ≫
      Iso.hom (id (Iso.refl (F.obj c.pt))))
    ((F.mapCocone c).ι.app { as := WalkingPair.right })
⊢ ((Cocone.precompose (diagramIsoPair (pair X Y ⋙ F)).hom).obj
              (BinaryBicone.toCocone (F.mapBinaryBicone (BinaryBicone.ofColimitCocone hc)))).ι.app
        j ≫
      Iso.hom (id (Iso.refl (F.obj c.pt))) =
    (F.mapCocone c).ι.app j

Tactic:
rcases j with ⟨⟨⟩⟩
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
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 : Cocone.{0, v, 0, u} (pair X Y)
hc : IsColimit c
⊢ Eq (α := (pair X Y ⋙ F).obj { as := WalkingPair.left : Discrete WalkingPair } ⟶ (F.mapCocone c).pt)
    (((Cocone.precompose (diagramIsoPair (pair X Y ⋙ F)).hom).obj
              (BinaryBicone.toCocone (F.mapBinaryBicone (BinaryBicone.ofColimitCocone hc)))).ι.app
        { as := WalkingPair.left : Discrete WalkingPair } ≫
      Iso.hom (id (Iso.refl (F.obj c.pt))))
    ((F.mapCocone c).ι.app { as := WalkingPair.left })

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
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 : Cocone.{0, v, 0, u} (pair X Y)
hc : IsColimit c
⊢ Eq (α := (pair X Y ⋙ F).obj { as := WalkingPair.right : Discrete WalkingPair } ⟶ (F.mapCocone c).pt)
    (((Cocone.precompose (diagramIsoPair (pair X Y ⋙ F)).hom).obj
              (BinaryBicone.toCocone (F.mapBinaryBicone (BinaryBicone.ofColimitCocone hc)))).ι.app
        { as := WalkingPair.right : Discrete WalkingPair } ≫
      Iso.hom (id (Iso.refl (F.obj c.pt))))
    ((F.mapCocone c).ι.app { as := WalkingPair.right })

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
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 : PreservesColimit (pair X Y) F
b : BinaryBicone.{v, u} X Y
hb : b.IsBilimit
j : Discrete WalkingPair
left :
  Eq (α :=
    obj.{0, v', 0, u'}
        (pair ((pair X Y ⋙ F).obj { as := WalkingPair.left : Discrete WalkingPair })
          ((pair X Y ⋙ F).obj { as := WalkingPair.right : Discrete WalkingPair }))
        { as := WalkingPair.left : Discrete WalkingPair } ⟶
      (BinaryBicone.toCocone (F.mapBinaryBicone b)).pt)
    (((Cocone.precompose (diagramIsoPair (pair X Y ⋙ F)).inv).obj (F.mapCocone b.toCocone)).ι.app
        { as := WalkingPair.left : Discrete WalkingPair } ≫
      Iso.hom (Iso.refl ((Cocone.precompose (diagramIsoPair (pair X Y ⋙ F)).inv).obj (F.mapCocone b.toCocone)).pt))
    ((BinaryBicone.toCocone (F.mapBinaryBicone b)).ι.app { as := WalkingPair.left })
right :
  Eq (α :=
    obj.{0, v', 0, u'}
        (pair ((pair X Y ⋙ F).obj { as := WalkingPair.left : Discrete WalkingPair })
          ((pair X Y ⋙ F).obj { as := WalkingPair.right : Discrete WalkingPair }))
        { as := WalkingPair.right : Discrete WalkingPair } ⟶
      (BinaryBicone.toCocone (F.mapBinaryBicone b)).pt)
    (((Cocone.precompose (diagramIsoPair (pair X Y ⋙ F)).inv).obj (F.mapCocone b.toCocone)).ι.app
        { as := WalkingPair.right : Discrete WalkingPair } ≫
      Iso.hom (Iso.refl ((Cocone.precompose (diagramIsoPair (pair X Y ⋙ F)).inv).obj (F.mapCocone b.toCocone)).pt))
    ((BinaryBicone.toCocone (F.mapBinaryBicone b)).ι.app { as := WalkingPair.right })
⊢ ((Cocone.precompose (diagramIsoPair (pair X Y ⋙ F)).inv).obj (F.mapCocone b.toCocone)).ι.app j ≫
      Iso.hom (Iso.refl ((Cocone.precompose (diagramIsoPair (pair X Y ⋙ F)).inv).obj (F.mapCocone b.toCocone)).pt) =
    (BinaryBicone.toCocone (F.mapBinaryBicone b)).ι.app j

Tactic:
rcases j with ⟨⟨⟩⟩
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
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 : PreservesColimit (pair X Y) F
b : BinaryBicone.{v, u} X Y
hb : b.IsBilimit
⊢ Eq (α :=
    obj.{0, v', 0, u'}
        (pair ((pair X Y ⋙ F).obj { as := WalkingPair.left : Discrete WalkingPair })
          ((pair X Y ⋙ F).obj { as := WalkingPair.right : Discrete WalkingPair }))
        { as := WalkingPair.left : Discrete WalkingPair } ⟶
      (BinaryBicone.toCocone (F.mapBinaryBicone b)).pt)
    (((Cocone.precompose (diagramIsoPair (pair X Y ⋙ F)).inv).obj (F.mapCocone b.toCocone)).ι.app
        { as := WalkingPair.left : Discrete WalkingPair } ≫
      Iso.hom (Iso.refl ((Cocone.precompose (diagramIsoPair (pair X Y ⋙ F)).inv).obj (F.mapCocone b.toCocone)).pt))
    ((BinaryBicone.toCocone (F.mapBinaryBicone b)).ι.app { as := WalkingPair.left })

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
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 : PreservesColimit (pair X Y) F
b : BinaryBicone.{v, u} X Y
hb : b.IsBilimit
⊢ Eq (α :=
    obj.{0, v', 0, u'}
        (pair ((pair X Y ⋙ F).obj { as := WalkingPair.left : Discrete WalkingPair })
          ((pair X Y ⋙ F).obj { as := WalkingPair.right : Discrete WalkingPair }))
        { as := WalkingPair.right : Discrete WalkingPair } ⟶
      (BinaryBicone.toCocone (F.mapBinaryBicone b)).pt)
    (((Cocone.precompose (diagramIsoPair (pair X Y ⋙ F)).inv).obj (F.mapCocone b.toCocone)).ι.app
        { as := WalkingPair.right : Discrete WalkingPair } ≫
      Iso.hom (Iso.refl ((Cocone.precompose (diagramIsoPair (pair X Y ⋙ F)).inv).obj (F.mapCocone b.toCocone)).pt))
    ((BinaryBicone.toCocone (F.mapBinaryBicone b)).ι.app { as := WalkingPair.right })

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.CommGrp_
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : CartesianMonoidalCategory.{v, u} C
X : C
⊢ 0 ▷ X ≫ HAdd.hAdd (α := tensorObj.{v, u} (𝒞 := inst) X X ⟶ X) (fst X X) (snd X X) = Iso.hom (λ_ X)

Tactic:
simp [← leftUnitor_hom]

Premises used: CategoryTheory.CartesianMonoidalCategory.leftUnitor_hom
-- Module: Mathlib.CategoryTheory.Preadditive.CommGrp_
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : CartesianMonoidalCategory.{v, u} C
X : C
⊢ X ◁ 0 ≫ HAdd.hAdd (α := tensorObj.{v, u} (𝒞 := inst) X X ⟶ X) (fst X X) (snd X X) = Iso.hom (ρ_ X)

Tactic:
simp [← rightUnitor_hom]

Premises used: CategoryTheory.CartesianMonoidalCategory.rightUnitor_hom
-- Module: Mathlib.CategoryTheory.Preadditive.CommGrp_
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : CartesianMonoidalCategory.{v, u} C
X : C
⊢ HAdd.hAdd (α := tensorObj.{v, u} (𝒞 := inst) X X ⟶ X) (fst X X) (snd X X) ▷ X ≫
      HAdd.hAdd (α := tensorObj.{v, u} (𝒞 := inst) X X ⟶ X) (fst X X) (snd X X) =
    Iso.hom (α_ X X X) ≫
      X ◁ HAdd.hAdd (α := tensorObj.{v, u} (𝒞 := inst) X X ⟶ X) (fst X X) (snd X X) ≫
        HAdd.hAdd (α := tensorObj.{v, u} (𝒞 := inst) X X ⟶ X) (fst X X) (snd X X)

Tactic:
simp [add_assoc]

Premises used: add_assoc
-- Module: Mathlib.CategoryTheory.Preadditive.CommGrp_
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : CartesianMonoidalCategory.{v, u} C
inst_3 : BraidedCategory.{v, u} C
X : C
⊢ Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) X X ⟶ X) (Iso.hom (β_ X X) ≫ MonObj.mul) MonObj.mul

Tactic:
simp [add_comm]

Premises used: add_comm
-- Module: Mathlib.CategoryTheory.Preadditive.CommGrp_
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : CartesianMonoidalCategory.{v, u} C
X Y Z : C
f g : tensorObj.{v, u} (𝒞 := inst) X Y ⟶ Z
h₁ : lift (𝟙 X) 0 ≫ f = lift (𝟙 X) 0 ≫ g
h₂ : lift 0 (𝟙 Y) ≫ f = lift 0 (𝟙 Y) ≫ g
⊢ f = g

Tactic:
BinaryCofan.IsColimit.hom_ext
    (binaryBiconeIsBilimitOfLimitConeOfIsLimit (tensorProductIsBinaryProduct X Y)).isColimit h₁ h₂

Premises used: CategoryTheory.Limits.BinaryCofan.IsColimit.hom_ext, CategoryTheory.Limits.binaryBiconeIsBilimitOfLimitConeOfIsLimit, CategoryTheory.CartesianMonoidalCategory.tensorProductIsBinaryProduct, CategoryTheory.Limits.BinaryBicone.IsBilimit.isColimit
-- Module: Mathlib.CategoryTheory.Preadditive.CommGrp_
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : CartesianMonoidalCategory.{v, u} C
inst_3 : BraidedCategory.{v, u} C
refine_1 :
  ∀ (x : CommGrp.{v, u} C),
    Eq.{v + 1} (α := tensorUnit.{v, u} C (𝒞 := inst) ⟶ (Functor.obj (𝟭 (CommGrp.{v, u} C)) x).X)
      (MonObj.one ≫ Iso.hom (Iso.refl (CommGrp.X (Functor.obj (CommGrp.forget C ⋙ toCommGrp C) x)))) MonObj.one
refine_2 :
  ∀ (x : CommGrp.{v, u} C),
    Eq.{v + 1} (α :=
      tensorObj.{v, u} (𝒞 := inst) (CommGrp.X (Functor.obj (CommGrp.forget C ⋙ toCommGrp C) x))
          (CommGrp.X (Functor.obj (CommGrp.forget C ⋙ toCommGrp C) x)) ⟶
        (Functor.obj (𝟭 (CommGrp.{v, u} C)) x).X)
      (MonObj.mul ≫ Iso.hom (Iso.refl (CommGrp.X (Functor.obj (CommGrp.forget C ⋙ toCommGrp C) x))))
      ((Iso.hom (Iso.refl (CommGrp.X (Functor.obj (CommGrp.forget C ⋙ toCommGrp C) x))) ⊗ₘ
          Iso.hom (Iso.refl (CommGrp.X (Functor.obj (CommGrp.forget C ⋙ toCommGrp C) x)))) ≫
        MonObj.mul)
refine_3 :
  ∀ {X Y : CommGrp.{v, u} C} (f : X ⟶ Y),
    Eq (α := Functor.obj (CommGrp.forget C ⋙ toCommGrp C) X ⟶ Functor.obj (𝟭 (CommGrp.{v, u} C)) Y)
      (Functor.map (CommGrp.forget C ⋙ toCommGrp C) f ≫
        Iso.hom
          ((fun (x : CommGrp.{v, u} C) ↦
              CommGrp.mkIso (Iso.refl (CommGrp.X (Functor.obj (CommGrp.forget C ⋙ toCommGrp C) x))) ⋯ ⋯)
            Y))
      (Iso.hom
          ((fun (x : CommGrp.{v, u} C) ↦
              CommGrp.mkIso (Iso.refl (CommGrp.X (Functor.obj (CommGrp.forget C ⋙ toCommGrp C) x))) ⋯ ⋯)
            X) ≫
        Functor.map (𝟭 (CommGrp.{v, u} C)) f)
⊢ Iso (C := CommGrp.{v, u} C ⥤ CommGrp.{v, u} C) (CommGrp.forget C ⋙ toCommGrp C) (𝟭 (CommGrp.{v, u} C))

Tactic:
refine NatIso.ofComponents (fun _ => CommGrp.mkIso (Iso.refl _) ?_ ?_) ?_

Premises used: CategoryTheory.Iso.refl, CategoryTheory.CommGrp.X, CategoryTheory.CommGrp.mkIso, CategoryTheory.Functor.obj, CategoryTheory.NatIso.ofComponents
-- Module: Mathlib.CategoryTheory.Preadditive.CommGrp_
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : CartesianMonoidalCategory.{v, u} C
inst_3 : BraidedCategory.{v, u} C
x : CommGrp.{v, u} C
⊢ Eq.{v + 1} (α := tensorUnit.{v, u} C (𝒞 := inst) ⟶ (Functor.obj (𝟭 (CommGrp.{v, u} C)) x).X)
    (MonObj.one ≫ Iso.hom (Iso.refl (CommGrp.X (Functor.obj (CommGrp.forget C ⋙ toCommGrp C) x)))) MonObj.one

Tactic:
((IsZero.iff_id_eq_zero _).2 (Subsingleton.elim _ _)).eq_of_src _ _

Premises used: Iff.mpr, CategoryTheory.Limits.IsZero.eq_of_src, CategoryTheory.Limits.IsZero.iff_id_eq_zero, Subsingleton.elim
-- Module: Mathlib.CategoryTheory.Preadditive.CommGrp_
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : CartesianMonoidalCategory.{v, u} C
inst_3 : BraidedCategory.{v, u} C
x : CommGrp.{v, u} C
⊢ Eq.{v + 1} (α := tensorUnit.{v, u} C (𝒞 := inst) ⟶ (Functor.obj (𝟭 (CommGrp.{v, u} C)) x).X)
    (MonObj.one ≫ Iso.hom (Iso.refl (CommGrp.X (Functor.obj (CommGrp.forget C ⋙ toCommGrp C) x)))) MonObj.one

Tactic:
exact ((IsZero.iff_id_eq_zero _).2 (Subsingleton.elim _ _)).eq_of_src _ _

Premises used: Iff.mpr, CategoryTheory.Limits.IsZero.eq_of_src, CategoryTheory.Limits.IsZero.iff_id_eq_zero, Subsingleton.elim
-- Module: Mathlib.CategoryTheory.Preadditive.CommGrp_
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : CartesianMonoidalCategory.{v, u} C
inst_3 : BraidedCategory.{v, u} C
x : CommGrp.{v, u} C
refine_2 : HAdd.hAdd (α := tensorObj.{v, u} (𝒞 := inst) x.X x.X ⟶ x.X) (fst x.X x.X) (snd x.X x.X) = MonObj.mul
⊢ Eq.{v + 1} (α :=
    tensorObj.{v, u} (𝒞 := inst) (CommGrp.X (Functor.obj (CommGrp.forget C ⋙ toCommGrp C) x))
        (CommGrp.X (Functor.obj (CommGrp.forget C ⋙ toCommGrp C) x)) ⟶
      (Functor.obj (𝟭 (CommGrp.{v, u} C)) x).X)
    (MonObj.mul ≫ Iso.hom (Iso.refl (CommGrp.X (Functor.obj (CommGrp.forget C ⋙ toCommGrp C) x))))
    ((Iso.hom (Iso.refl (CommGrp.X (Functor.obj (CommGrp.forget C ⋙ toCommGrp C) x))) ⊗ₘ
        Iso.hom (Iso.refl (CommGrp.X (Functor.obj (CommGrp.forget C ⋙ toCommGrp C) x)))) ≫
      MonObj.mul)

Tactic:
simp only [Functor.comp_obj, CommGrp.forget_obj, toCommGrp_obj_X, Functor.id_obj,
      mul_def, Iso.refl_hom, Category.comp_id, tensorHom_id, id_whiskerRight, Category.id_comp]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.comp_id, CategoryTheory.MonoidalCategory.id_whiskerRight, CategoryTheory.Functor.id_obj, CategoryTheory.Preadditive.mul_def, CategoryTheory.CommGrp.forget_obj, CategoryTheory.Preadditive.toCommGrp_obj_X, CategoryTheory.Iso.refl_hom, CategoryTheory.MonoidalCategory.tensorHom_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Preadditive.CommGrp_
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : CartesianMonoidalCategory.{v, u} C
inst_3 : BraidedCategory.{v, u} C
x : CommGrp.{v, u} C
⊢ HAdd.hAdd (α := tensorObj.{v, u} (𝒞 := inst) x.X x.X ⟶ x.X) (fst x.X x.X) (snd x.X x.X) = MonObj.mul

Tactic:
apply monoidal_hom_ext

Premises used: _private.0.CategoryTheory.Preadditive.monoidal_hom_ext
-- Module: Mathlib.CategoryTheory.Preadditive.CommGrp_
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : CartesianMonoidalCategory.{v, u} C
inst_3 : BraidedCategory.{v, u} C
⊢ ∀ {X Y : CommGrp.{v, u} C} (f : X ⟶ Y),
    Eq (α := Functor.obj (CommGrp.forget C ⋙ toCommGrp C) X ⟶ Functor.obj (𝟭 (CommGrp.{v, u} C)) Y)
      (Functor.map (CommGrp.forget C ⋙ toCommGrp C) f ≫
        Iso.hom
          ((fun (x : CommGrp.{v, u} C) ↦
              CommGrp.mkIso (Iso.refl (CommGrp.X (Functor.obj (CommGrp.forget C ⋙ toCommGrp C) x))) ⋯ ⋯)
            Y))
      (Iso.hom
          ((fun (x : CommGrp.{v, u} C) ↦
              CommGrp.mkIso (Iso.refl (CommGrp.X (Functor.obj (CommGrp.forget C ⋙ toCommGrp C) x))) ⋯ ⋯)
            X) ≫
        Functor.map (𝟭 (CommGrp.{v, u} C)) f)

Tactic:
cat_disch
-- Module: Mathlib.CategoryTheory.Preadditive.EilenbergMoore
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
T : Monad.{v₁, u₁} C
inst_2 : T.Additive
F G : T.Algebra
α β : F ⟶ G
⊢ T.map (α.f + β.f) ≫ G.a = F.a ≫ (α.f + β.f)

Tactic:
simp only [Functor.map_add, add_comp, Monad.Algebra.Hom.h, comp_add]

Premises used: CategoryTheory.Monad.Algebra.Hom.h, CategoryTheory.Functor.map_add, CategoryTheory.Preadditive.add_comp, CategoryTheory.Preadditive.comp_add
-- Module: Mathlib.CategoryTheory.Preadditive.EilenbergMoore
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
T : Monad.{v₁, u₁} C
inst_2 : T.Additive
F G : T.Algebra
⊢ T.map 0 ≫ G.a = F.a ≫ 0

Tactic:
simp only [Functor.map_zero, zero_comp, comp_zero]

Premises used: CategoryTheory.Limits.comp_zero, CategoryTheory.Functor.map_zero, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.CategoryTheory.Preadditive.EilenbergMoore
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
T : Monad.{v₁, u₁} C
inst_2 : T.Additive
F G : T.Algebra
n : ℕ
α : F ⟶ G
rw : (n • T.map α.f) ≫ G.a = F.a ≫ (n • α.f)
rw₁ : n • T.map α.f ≫ G.a = F.a ≫ (n • α.f)
rw₂ : n • F.a ≫ α.f = F.a ≫ (n • α.f)
rw₃ rw₄ : n • F.a ≫ α.f = n • F.a ≫ α.f
⊢ T.map (n • α.f) ≫ G.a = F.a ≫ (n • α.f)

Tactic:
rw [Functor.map_nsmul, nsmul_comp, Monad.Algebra.Hom.h, comp_nsmul]

Premises used: CategoryTheory.Monad.Algebra.Hom.h, CategoryTheory.Preadditive.nsmul_comp, CategoryTheory.Preadditive.comp_nsmul, CategoryTheory.Functor.map_nsmul
-- Module: Mathlib.CategoryTheory.Preadditive.EilenbergMoore
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
T : Monad.{v₁, u₁} C
inst_2 : T.Additive
F G : T.Algebra
α : F ⟶ G
⊢ T.map (-α.f) ≫ G.a = F.a ≫ (-α.f)

Tactic:
simp only [Functor.map_neg, neg_comp, Monad.Algebra.Hom.h, comp_neg]

Premises used: CategoryTheory.Monad.Algebra.Hom.h, CategoryTheory.Preadditive.comp_neg, CategoryTheory.Preadditive.neg_comp, CategoryTheory.Functor.map_neg
-- Module: Mathlib.CategoryTheory.Preadditive.EilenbergMoore
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
T : Monad.{v₁, u₁} C
inst_2 : T.Additive
F G : T.Algebra
α β : F ⟶ G
⊢ T.map (α.f - β.f) ≫ G.a = F.a ≫ (α.f - β.f)

Tactic:
simp only [Functor.map_sub, sub_comp, Monad.Algebra.Hom.h, comp_sub]

Premises used: CategoryTheory.Monad.Algebra.Hom.h, CategoryTheory.Functor.map_sub, CategoryTheory.Preadditive.comp_sub, CategoryTheory.Preadditive.sub_comp
-- Module: Mathlib.CategoryTheory.Preadditive.EilenbergMoore
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
T : Monad.{v₁, u₁} C
inst_2 : T.Additive
F G : T.Algebra
r : ℤ
α : F ⟶ G
rw : (r • T.map α.f) ≫ G.a = F.a ≫ (r • α.f)
rw₁ : r • T.map α.f ≫ G.a = F.a ≫ (r • α.f)
rw₂ : r • F.a ≫ α.f = F.a ≫ (r • α.f)
rw₃ rw₄ : r • F.a ≫ α.f = r • F.a ≫ α.f
⊢ T.map (r • α.f) ≫ G.a = F.a ≫ (r • α.f)

Tactic:
rw [Functor.map_zsmul, zsmul_comp, Monad.Algebra.Hom.h, comp_zsmul]

Premises used: CategoryTheory.Monad.Algebra.Hom.h, CategoryTheory.Functor.map_zsmul, CategoryTheory.Preadditive.comp_zsmul, CategoryTheory.Preadditive.zsmul_comp
-- Module: Mathlib.CategoryTheory.Preadditive.EilenbergMoore
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
T : Monad.{v₁, u₁} C
inst_2 : T.Additive
U : Comonad.{v₁, u₁} C
inst_3 : U.Additive
F G : U.Coalgebra
α β : F ⟶ G
⊢ F.a ≫ U.map (α.f + β.f) = (α.f + β.f) ≫ G.a

Tactic:
simp only [Functor.map_add, comp_add, Comonad.Coalgebra.Hom.h, add_comp]

Premises used: CategoryTheory.Functor.map_add, CategoryTheory.Comonad.Coalgebra.Hom.h, CategoryTheory.Preadditive.add_comp, CategoryTheory.Preadditive.comp_add
-- Module: Mathlib.CategoryTheory.Preadditive.EilenbergMoore
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
T : Monad.{v₁, u₁} C
inst_2 : T.Additive
U : Comonad.{v₁, u₁} C
inst_3 : U.Additive
F G : U.Coalgebra
⊢ F.a ≫ U.map 0 = 0 ≫ G.a

Tactic:
simp only [Functor.map_zero, comp_zero, zero_comp]

Premises used: CategoryTheory.Limits.comp_zero, CategoryTheory.Functor.map_zero, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.CategoryTheory.Preadditive.EilenbergMoore
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
T : Monad.{v₁, u₁} C
inst_2 : T.Additive
U : Comonad.{v₁, u₁} C
inst_3 : U.Additive
F G : U.Coalgebra
n : ℕ
α : F ⟶ G
rw : F.a ≫ (n • U.map α.f) = (n • α.f) ≫ G.a
rw₁ : n • F.a ≫ U.map α.f = (n • α.f) ≫ G.a
rw₂ : n • α.f ≫ G.a = (n • α.f) ≫ G.a
rw₃ rw₄ : n • α.f ≫ G.a = n • α.f ≫ G.a
⊢ F.a ≫ U.map (n • α.f) = (n • α.f) ≫ G.a

Tactic:
rw [Functor.map_nsmul, comp_nsmul, Comonad.Coalgebra.Hom.h, nsmul_comp]

Premises used: CategoryTheory.Preadditive.nsmul_comp, CategoryTheory.Comonad.Coalgebra.Hom.h, CategoryTheory.Preadditive.comp_nsmul, CategoryTheory.Functor.map_nsmul