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
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))
⊢ 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_epi_section' (splitEpiBiprodComparison F X Y)
-- 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 : Cocone.{0, v, 0, u} (pair X Y)
hc : IsColimit c
⊢ ((Cocone.precompose (diagramIsoPair (pair X Y ⋙ F)).hom).obj
        (BinaryBicone.toCocone (F.mapBinaryBicone (BinaryBicone.ofColimitCocone hc)))).pt ≅
    (F.mapCocone 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 : Cocone.{0, v, 0, u} (pair X Y)
hc : IsColimit c
j : Discrete WalkingPair
⊢ ((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
have 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 })
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 : 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 })
⊢ ((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
have 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 })
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 : PreservesColimit (pair X Y) F
b : BinaryBicone.{v, u} X Y
hb : b.IsBilimit
j : Discrete WalkingPair
⊢ ((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
have 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 })
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 : 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 })
⊢ ((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
have 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 })
Tactic: rcases j with ⟨⟨⟩⟩
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.CommGrp_ (goal)
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
⊢ Iso (C := CommGrp.{v, u} C ⥤ CommGrp.{v, u} C) (CommGrp.forget C ⋙ toCommGrp C) (𝟭 (CommGrp.{v, u} C))
have 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
Tactic: refine NatIso.ofComponents (fun _ => CommGrp.mkIso (Iso.refl _) ?_ ?_) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.CommGrp_ (goal)
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
⊢ Iso (C := CommGrp.{v, u} C ⥤ CommGrp.{v, u} C) (CommGrp.forget C ⋙ toCommGrp C) (𝟭 (CommGrp.{v, u} C))
have 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)
Tactic: refine NatIso.ofComponents (fun _ => CommGrp.mkIso (Iso.refl _) ?_ ?_) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.CommGrp_ (goal)
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)
⊢ Iso (C := CommGrp.{v, u} C ⥤ CommGrp.{v, u} C) (CommGrp.forget C ⋙ toCommGrp C) (𝟭 (CommGrp.{v, u} C))
have 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))) sorry sorry)
          Y))
    (Iso.hom
        ((fun (x : CommGrp.{v, u} C) ↦
            CommGrp.mkIso (Iso.refl (CommGrp.X (Functor.obj (CommGrp.forget C ⋙ toCommGrp C) x))) sorry sorry)
          X) ≫
      Functor.map (𝟭 (CommGrp.{v, u} C)) f)
Tactic: refine NatIso.ofComponents (fun _ => CommGrp.mkIso (Iso.refl _) ?_ ?_) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.CommGrp_ (goal)
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} (α :=
    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)
have 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
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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.EilenbergMoore (goal)
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
⊢ T.map (n • α.f) ≫ G.a = F.a ≫ (n • α.f)
have rw : (n • T.map α.f) ≫ G.a = F.a ≫ (n • α.f)
Tactic: rw [Functor.map_nsmul, nsmul_comp, Monad.Algebra.Hom.h, comp_nsmul]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.EilenbergMoore (goal)
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)
⊢ T.map (n • α.f) ≫ G.a = F.a ≫ (n • α.f)
have rw₁ : n • T.map α.f ≫ G.a = F.a ≫ (n • α.f)
Tactic: rw [Functor.map_nsmul, nsmul_comp, Monad.Algebra.Hom.h, comp_nsmul]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.EilenbergMoore (goal)
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)
⊢ T.map (n • α.f) ≫ G.a = F.a ≫ (n • α.f)
have rw₂ : n • F.a ≫ α.f = F.a ≫ (n • α.f)
Tactic: rw [Functor.map_nsmul, nsmul_comp, Monad.Algebra.Hom.h, comp_nsmul]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.EilenbergMoore (goal)
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)
⊢ T.map (n • α.f) ≫ G.a = F.a ≫ (n • α.f)
have rw₃ : n • F.a ≫ α.f = n • F.a ≫ α.f
Tactic: rw [Functor.map_nsmul, nsmul_comp, Monad.Algebra.Hom.h, comp_nsmul]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.EilenbergMoore (goal)
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
⊢ T.map (r • α.f) ≫ G.a = F.a ≫ (r • α.f)
have rw : (r • T.map α.f) ≫ G.a = F.a ≫ (r • α.f)
Tactic: rw [Functor.map_zsmul, zsmul_comp, Monad.Algebra.Hom.h, comp_zsmul]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.EilenbergMoore (goal)
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)
⊢ T.map (r • α.f) ≫ G.a = F.a ≫ (r • α.f)
have rw₁ : r • T.map α.f ≫ G.a = F.a ≫ (r • α.f)
Tactic: rw [Functor.map_zsmul, zsmul_comp, Monad.Algebra.Hom.h, comp_zsmul]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.EilenbergMoore (goal)
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)
⊢ T.map (r • α.f) ≫ G.a = F.a ≫ (r • α.f)
have rw₂ : r • F.a ≫ α.f = F.a ≫ (r • α.f)
Tactic: rw [Functor.map_zsmul, zsmul_comp, Monad.Algebra.Hom.h, comp_zsmul]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.EilenbergMoore (goal)
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)
⊢ T.map (r • α.f) ≫ G.a = F.a ≫ (r • α.f)
have rw₃ : r • F.a ≫ α.f = r • F.a ≫ α.f
Tactic: rw [Functor.map_zsmul, zsmul_comp, Monad.Algebra.Hom.h, comp_zsmul]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.EilenbergMoore (goal)
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
⊢ F.a ≫ U.map (n • α.f) = (n • α.f) ≫ G.a
have rw : F.a ≫ (n • U.map α.f) = (n • α.f) ≫ G.a
Tactic: rw [Functor.map_nsmul, comp_nsmul, Comonad.Coalgebra.Hom.h, nsmul_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.EilenbergMoore (goal)
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
⊢ F.a ≫ U.map (n • α.f) = (n • α.f) ≫ G.a
have rw₁ : n • F.a ≫ U.map α.f = (n • α.f) ≫ G.a
Tactic: rw [Functor.map_nsmul, comp_nsmul, Comonad.Coalgebra.Hom.h, nsmul_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.EilenbergMoore (goal)
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
⊢ F.a ≫ U.map (n • α.f) = (n • α.f) ≫ G.a
have rw₂ : n • α.f ≫ G.a = (n • α.f) ≫ G.a
Tactic: rw [Functor.map_nsmul, comp_nsmul, Comonad.Coalgebra.Hom.h, nsmul_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.EilenbergMoore (goal)
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
⊢ F.a ≫ U.map (n • α.f) = (n • α.f) ≫ G.a
have rw₃ : n • α.f ≫ G.a = n • α.f ≫ G.a
Tactic: rw [Functor.map_nsmul, comp_nsmul, Comonad.Coalgebra.Hom.h, nsmul_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.EilenbergMoore (goal)
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
r : ℤ
α : F ⟶ G
⊢ F.a ≫ U.map (r • α.f) = (r • α.f) ≫ G.a
have rw : F.a ≫ (r • U.map α.f) = (r • α.f) ≫ G.a
Tactic: rw [Functor.map_zsmul, comp_zsmul, Comonad.Coalgebra.Hom.h, zsmul_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.EilenbergMoore (goal)
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
r : ℤ
α : F ⟶ G
rw : F.a ≫ (r • U.map α.f) = (r • α.f) ≫ G.a
⊢ F.a ≫ U.map (r • α.f) = (r • α.f) ≫ G.a
have rw₁ : r • F.a ≫ U.map α.f = (r • α.f) ≫ G.a
Tactic: rw [Functor.map_zsmul, comp_zsmul, Comonad.Coalgebra.Hom.h, zsmul_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.EilenbergMoore (goal)
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
r : ℤ
α : F ⟶ G
rw : F.a ≫ (r • U.map α.f) = (r • α.f) ≫ G.a
rw₁ : r • F.a ≫ U.map α.f = (r • α.f) ≫ G.a
⊢ F.a ≫ U.map (r • α.f) = (r • α.f) ≫ G.a
have rw₂ : r • α.f ≫ G.a = (r • α.f) ≫ G.a
Tactic: rw [Functor.map_zsmul, comp_zsmul, Comonad.Coalgebra.Hom.h, zsmul_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.EilenbergMoore (goal)
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
r : ℤ
α : F ⟶ G
rw : F.a ≫ (r • U.map α.f) = (r • α.f) ≫ G.a
rw₁ : r • F.a ≫ U.map α.f = (r • α.f) ≫ G.a
rw₂ : r • α.f ≫ G.a = (r • α.f) ≫ G.a
⊢ F.a ≫ U.map (r • α.f) = (r • α.f) ≫ G.a
have rw₃ : r • α.f ≫ G.a = r • α.f ≫ G.a
Tactic: rw [Functor.map_zsmul, comp_zsmul, Comonad.Coalgebra.Hom.h, zsmul_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.EndoFunctor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
F : Functor.{v₁, v₁, u₁, u₁} C C
inst_2 : F.Additive
A₁ A₂ : Algebra F
n : ℕ
α : A₁ ⟶ A₂
⊢ F.map (n • α.f) ≫ A₂.str = A₁.str ≫ (n • α.f)
have rw : F.map (n • α.f) ≫ A₂.str = n • A₁.str ≫ α.f
Tactic: rw [comp_nsmul, Functor.map_nsmul, nsmul_comp, Endofunctor.Algebra.Hom.h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.EndoFunctor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
F : Functor.{v₁, v₁, u₁, u₁} C C
inst_2 : F.Additive
A₁ A₂ : Algebra F
n : ℕ
α : A₁ ⟶ A₂
rw : F.map (n • α.f) ≫ A₂.str = n • A₁.str ≫ α.f
⊢ F.map (n • α.f) ≫ A₂.str = A₁.str ≫ (n • α.f)
have rw₁ : (n • F.map α.f) ≫ A₂.str = n • A₁.str ≫ α.f
Tactic: rw [comp_nsmul, Functor.map_nsmul, nsmul_comp, Endofunctor.Algebra.Hom.h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.EndoFunctor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
F : Functor.{v₁, v₁, u₁, u₁} C C
inst_2 : F.Additive
A₁ A₂ : Algebra F
n : ℕ
α : A₁ ⟶ A₂
rw : F.map (n • α.f) ≫ A₂.str = n • A₁.str ≫ α.f
rw₁ : (n • F.map α.f) ≫ A₂.str = n • A₁.str ≫ α.f
⊢ F.map (n • α.f) ≫ A₂.str = A₁.str ≫ (n • α.f)
have rw₂ : n • F.map α.f ≫ A₂.str = n • A₁.str ≫ α.f
Tactic: rw [comp_nsmul, Functor.map_nsmul, nsmul_comp, Endofunctor.Algebra.Hom.h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.EndoFunctor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
F : Functor.{v₁, v₁, u₁, u₁} C C
inst_2 : F.Additive
A₁ A₂ : Algebra F
n : ℕ
α : A₁ ⟶ A₂
rw : F.map (n • α.f) ≫ A₂.str = n • A₁.str ≫ α.f
rw₁ : (n • F.map α.f) ≫ A₂.str = n • A₁.str ≫ α.f
rw₂ : n • F.map α.f ≫ A₂.str = n • A₁.str ≫ α.f
⊢ F.map (n • α.f) ≫ A₂.str = A₁.str ≫ (n • α.f)
have rw₃ : n • A₁.str ≫ α.f = n • A₁.str ≫ α.f
Tactic: rw [comp_nsmul, Functor.map_nsmul, nsmul_comp, Endofunctor.Algebra.Hom.h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.EndoFunctor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
F : Functor.{v₁, v₁, u₁, u₁} C C
inst_2 : F.Additive
A₁ A₂ : Algebra F
r : ℤ
α : A₁ ⟶ A₂
⊢ F.map (r • α.f) ≫ A₂.str = A₁.str ≫ (r • α.f)
have rw : F.map (r • α.f) ≫ A₂.str = r • A₁.str ≫ α.f
Tactic: rw [comp_zsmul, Functor.map_zsmul, zsmul_comp, Endofunctor.Algebra.Hom.h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.EndoFunctor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
F : Functor.{v₁, v₁, u₁, u₁} C C
inst_2 : F.Additive
A₁ A₂ : Algebra F
r : ℤ
α : A₁ ⟶ A₂
rw : F.map (r • α.f) ≫ A₂.str = r • A₁.str ≫ α.f
⊢ F.map (r • α.f) ≫ A₂.str = A₁.str ≫ (r • α.f)
have rw₁ : (r • F.map α.f) ≫ A₂.str = r • A₁.str ≫ α.f
Tactic: rw [comp_zsmul, Functor.map_zsmul, zsmul_comp, Endofunctor.Algebra.Hom.h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.EndoFunctor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
F : Functor.{v₁, v₁, u₁, u₁} C C
inst_2 : F.Additive
A₁ A₂ : Algebra F
r : ℤ
α : A₁ ⟶ A₂
rw : F.map (r • α.f) ≫ A₂.str = r • A₁.str ≫ α.f
rw₁ : (r • F.map α.f) ≫ A₂.str = r • A₁.str ≫ α.f
⊢ F.map (r • α.f) ≫ A₂.str = A₁.str ≫ (r • α.f)
have rw₂ : r • F.map α.f ≫ A₂.str = r • A₁.str ≫ α.f
Tactic: rw [comp_zsmul, Functor.map_zsmul, zsmul_comp, Endofunctor.Algebra.Hom.h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.EndoFunctor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
F : Functor.{v₁, v₁, u₁, u₁} C C
inst_2 : F.Additive
A₁ A₂ : Algebra F
r : ℤ
α : A₁ ⟶ A₂
rw : F.map (r • α.f) ≫ A₂.str = r • A₁.str ≫ α.f
rw₁ : (r • F.map α.f) ≫ A₂.str = r • A₁.str ≫ α.f
rw₂ : r • F.map α.f ≫ A₂.str = r • A₁.str ≫ α.f
⊢ F.map (r • α.f) ≫ A₂.str = A₁.str ≫ (r • α.f)
have rw₃ : r • A₁.str ≫ α.f = r • A₁.str ≫ α.f
Tactic: rw [comp_zsmul, Functor.map_zsmul, zsmul_comp, Endofunctor.Algebra.Hom.h]