awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.FunctorCategory (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
F G H K : Functor.{v₁, v₂, u₁, u₂} C D
X : C
⊢ Eq (α :=
    MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1)
        (MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1)
          (MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj X) (G.obj X)) (H.obj X))
        (K.obj X) ⟶
      MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj X)
        (MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (G.obj X)
          (MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (H.obj X) (K.obj X))))
    (Iso.hom (α_ (F.obj X) (G.obj X) (H.obj X)) ▷ K.obj X ≫
      Iso.hom (α_ (F.obj X) (MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (G.obj X) (H.obj X)) (K.obj X)) ≫
        F.obj X ◁ Iso.hom (α_ (G.obj X) (H.obj X) (K.obj X)))
    (Iso.hom (α_ (MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj X) (G.obj X)) (H.obj X) (K.obj X)) ≫
      Iso.hom (α_ (F.obj X) (G.obj X) (MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (H.obj X) (K.obj X))))
have w : Eq (α :=
  MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1)
      (MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1)
        (MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj X) (G.obj X)) (H.obj X))
      (K.obj X) ⟶
    MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj X)
      (MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (G.obj X)
        (MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (H.obj X) (K.obj X))))
  (Iso.hom (α_ (MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj X) (G.obj X)) (H.obj X) (K.obj X)) ≫
    Iso.hom (α_ (F.obj X) (G.obj X) (MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (H.obj X) (K.obj X))))
  (Iso.hom (α_ (MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj X) (G.obj X)) (H.obj X) (K.obj X)) ≫
    Iso.hom (α_ (F.obj X) (G.obj X) (MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (H.obj X) (K.obj X))))
Tactic: rw [pentagon]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.FunctorCategory (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
inst_3 : BraidedCategory.{v₂, u₂} D
F G H : Functor.{v₁, v₂, u₁, u₂} C D
⊢ Eq (α :=
    MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category)
        (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) F G) H ⟶
      MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) G
        (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) H F))
    (Iso.hom (α_ F G H) ≫
      Iso.hom
          (NatIso.ofComponents
            (fun (x : C) ↦ β_ (F.obj x) ((MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) G H).obj x)) ⋯) ≫
        Iso.hom (α_ G H F))
    (Iso.hom (NatIso.ofComponents (fun (x : C) ↦ β_ (F.obj x) (G.obj x)) ⋯) ▷ H ≫
      Iso.hom (α_ G F H) ≫ G ◁ Iso.hom (NatIso.ofComponents (fun (x : C) ↦ β_ (F.obj x) (H.obj x)) ⋯))
have w : ∀ (X : C),
  Eq (α :=
    (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category)
            (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) F G) H).obj
        X ⟶
      (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) G
            (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) H F)).obj
        X)
    (NatTrans.app
      (Iso.hom (α_ F G H) ≫
        Iso.hom
            (NatIso.ofComponents
              (fun (x : C) ↦ β_ (F.obj x) ((MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) G H).obj x)) sorry) ≫
          Iso.hom (α_ G H F))
      X)
    (NatTrans.app
      (Iso.hom (NatIso.ofComponents (fun (x : C) ↦ β_ (F.obj x) (G.obj x)) sorry) ▷ H ≫
        Iso.hom (α_ G F H) ≫ G ◁ Iso.hom (NatIso.ofComponents (fun (x : C) ↦ β_ (F.obj x) (H.obj x)) sorry))
      X)
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.FunctorCategory (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
inst_3 : BraidedCategory.{v₂, u₂} D
F G H : Functor.{v₁, v₂, u₁, u₂} C D
⊢ Eq (α :=
    MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) F
        (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) G H) ⟶
      MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category)
        (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) H F) G)
    (Iso.inv (α_ F G H) ≫
      Iso.hom
          (NatIso.ofComponents
            (fun (x : C) ↦ β_ ((MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) F G).obj x) (H.obj x)) ⋯) ≫
        Iso.inv (α_ H F G))
    (F ◁ Iso.hom (NatIso.ofComponents (fun (x : C) ↦ β_ (G.obj x) (H.obj x)) ⋯) ≫
      Iso.inv (α_ F H G) ≫ Iso.hom (NatIso.ofComponents (fun (x : C) ↦ β_ (F.obj x) (H.obj x)) ⋯) ▷ G)
have w : ∀ (X : C),
  Eq (α :=
    (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) F
            (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) G H)).obj
        X ⟶
      (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category)
            (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) H F) G).obj
        X)
    (NatTrans.app
      (Iso.inv (α_ F G H) ≫
        Iso.hom
            (NatIso.ofComponents
              (fun (x : C) ↦ β_ ((MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) F G).obj x) (H.obj x)) sorry) ≫
          Iso.inv (α_ H F G))
      X)
    (NatTrans.app
      (F ◁ Iso.hom (NatIso.ofComponents (fun (x : C) ↦ β_ (G.obj x) (H.obj x)) sorry) ≫
        Iso.inv (α_ F H G) ≫ Iso.hom (NatIso.ofComponents (fun (x : C) ↦ β_ (F.obj x) (H.obj x)) sorry) ▷ G)
      X)
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.FunctorCategory (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
inst_3 : SymmetricCategory.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
⊢ Iso.hom (β_ F G) ≫ Iso.hom (β_ G F) = 𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) F G)
have w : ∀ (X : C),
  NatTrans.app (Iso.hom (β_ F G) ≫ Iso.hom (β_ G F)) X =
    NatTrans.app (𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) F G)) X
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.FunctorCategory (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
E : Type u_1
inst_3 : Category.{v_1, u_1} E
inst_4 : MonoidalCategory.{v_1, u_1} E
e : Equivalence.{v₁, v₂, u₁, u₂} C D
X Y : Functor.{v₂, v_1, u₂, u_1} D E
⊢ Eq (α :=
    tensorObj (𝒞 := Functor.category) (Functor.obj (Equivalence.inverse e.congrLeft) X)
        (Functor.obj (Equivalence.inverse e.congrLeft) Y) ⟶
      Functor.obj (Equivalence.inverse e.congrLeft) (tensorObj (𝒞 := Functor.category) X Y))
    (Functor.LaxMonoidal.μ (Equivalence.inverse e.congrLeft) X Y)
    (NatTrans.app (Adjunction.unit (Equivalence.toAdjunction e.congrLeft))
        (tensorObj (𝒞 := Functor.category) (Functor.obj (Equivalence.inverse e.congrLeft) X)
          (Functor.obj (Equivalence.inverse e.congrLeft) Y)) ≫
      Functor.map (Equivalence.inverse e.congrLeft)
        (CategoryStruct.comp (Y :=
          tensorObj (𝒞 := Functor.category)
            (Functor.obj (Equivalence.functor e.congrLeft) (Functor.obj (Equivalence.inverse e.congrLeft) X))
            (Functor.obj (Equivalence.functor e.congrLeft) (Functor.obj (Equivalence.inverse e.congrLeft) Y)))
          (Functor.OplaxMonoidal.δ (Equivalence.functor e.congrLeft) (Functor.obj (Equivalence.inverse e.congrLeft) X)
            (Functor.obj (Equivalence.inverse e.congrLeft) Y))
          (NatTrans.app (Adjunction.counit (Equivalence.toAdjunction e.congrLeft)) X ⊗ₘ
            NatTrans.app (Adjunction.counit (Equivalence.toAdjunction e.congrLeft)) Y)))
have w : ∀ (x : C),
  Eq (α :=
    (tensorObj (𝒞 := Functor.category) (Functor.obj (Equivalence.inverse e.congrLeft) X)
            (Functor.obj (Equivalence.inverse e.congrLeft) Y)).obj
        x ⟶
      (Functor.obj (Equivalence.inverse e.congrLeft) (tensorObj (𝒞 := Functor.category) X Y)).obj x)
    (NatTrans.app (Functor.LaxMonoidal.μ (Equivalence.inverse e.congrLeft) X Y) x)
    (NatTrans.app
      (NatTrans.app (Adjunction.unit (Equivalence.toAdjunction e.congrLeft))
          (tensorObj (𝒞 := Functor.category) (Functor.obj (Equivalence.inverse e.congrLeft) X)
            (Functor.obj (Equivalence.inverse e.congrLeft) Y)) ≫
        Functor.map (Equivalence.inverse e.congrLeft)
          (CategoryStruct.comp (Y :=
            tensorObj (𝒞 := Functor.category)
              (Functor.obj (Equivalence.functor e.congrLeft) (Functor.obj (Equivalence.inverse e.congrLeft) X))
              (Functor.obj (Equivalence.functor e.congrLeft) (Functor.obj (Equivalence.inverse e.congrLeft) Y)))
            (Functor.OplaxMonoidal.δ (Equivalence.functor e.congrLeft) (Functor.obj (Equivalence.inverse e.congrLeft) X)
              (Functor.obj (Equivalence.inverse e.congrLeft) Y))
            (NatTrans.app (Adjunction.counit (Equivalence.toAdjunction e.congrLeft)) X ⊗ₘ
              NatTrans.app (Adjunction.counit (Equivalence.toAdjunction e.congrLeft)) Y)))
      x)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Grp (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
A B : C
inst_2 : GrpObj B
f : A ⟶ B
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift f (f ≫ @inv _ _ inst_1 _ _)) μ =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η
have this : f ≫ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift (𝟙 B) (@inv _ _ inst_1 _ _)) μ =
  f ≫ CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit B) η
Tactic: have := f ≫= right_inv B
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Grp (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
A B : C
inst_2 : GrpObj B
f : A ⟶ B
this :
  f ≫ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift (𝟙 B) (@inv _ _ inst_1 _ _)) μ =
    f ≫ CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit B) η
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift f (f ≫ @inv _ _ inst_1 _ _)) μ =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η
have rwa : ∀
  (this :
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift (f ≫ 𝟙 B) (f ≫ @inv _ _ inst_1 _ _)) μ =
      f ≫ CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit B) η),
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift f (f ≫ @inv _ _ inst_1 _ _)) μ =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η
Tactic: rwa [comp_lift_assoc, comp_id, reassoc_of% toUnit_unique (f ≫ toUnit B) (toUnit A)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Grp (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
A B : C
inst_2 : GrpObj B
f : A ⟶ B
this :
  f ≫ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift (𝟙 B) (@inv _ _ inst_1 _ _)) μ =
    f ≫ CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit B) η
rwa :
  ∀
    (this :
      CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift (f ≫ 𝟙 B) (f ≫ @inv _ _ inst_1 _ _)) μ =
        f ≫ CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit B) η),
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift f (f ≫ @inv _ _ inst_1 _ _)) μ =
      CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift f (f ≫ @inv _ _ inst_1 _ _)) μ =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η
have rwa₁ : ∀
  (this :
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift f (f ≫ @inv _ _ inst_1 _ _)) μ =
      f ≫ CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit B) η),
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift f (f ≫ @inv _ _ inst_1 _ _)) μ =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η
Tactic: rwa [comp_lift_assoc, comp_id, reassoc_of% toUnit_unique (f ≫ toUnit B) (toUnit A)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Grp (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
A B : C
inst_2 : GrpObj B
f : A ⟶ B
this :
  f ≫ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift (𝟙 B) (@inv _ _ inst_1 _ _)) μ =
    f ≫ CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit B) η
rwa :
  ∀
    (this :
      CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift (f ≫ 𝟙 B) (f ≫ @inv _ _ inst_1 _ _)) μ =
        f ≫ CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit B) η),
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift f (f ≫ @inv _ _ inst_1 _ _)) μ =
      CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η
rwa₁ :
  ∀
    (this :
      CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift f (f ≫ @inv _ _ inst_1 _ _)) μ =
        f ≫ CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit B) η),
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift f (f ≫ @inv _ _ inst_1 _ _)) μ =
      CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift f (f ≫ @inv _ _ inst_1 _ _)) μ =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η
have rwa₂ : ∀
  (this :
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift f (f ≫ @inv _ _ inst_1 _ _)) μ =
      CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η),
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift f (f ≫ @inv _ _ inst_1 _ _)) μ =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η
Tactic: rwa [comp_lift_assoc, comp_id, reassoc_of% toUnit_unique (f ≫ toUnit B) (toUnit A)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Grp (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
A B : C
inst_2 : GrpObj A
inst_3 : GrpObj B
f : A ⟶ B
inst_4 : IsMonHom f
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift f (@inv _ _ inst_1 _ _ ≫ f)) μ =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η
have this : CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (lift (𝟙 A) (@inv _ _ inst_1 _ _)) μ ≫ f =
  CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η ≫ f
Tactic: have := right_inv A =≫ f
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Grp (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
A B : C
inst_2 : GrpObj A
inst_3 : GrpObj B
f : A ⟶ B
inst_4 : IsMonHom f
this :
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (lift (𝟙 A) (@inv _ _ inst_1 _ _)) μ ≫ f =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η ≫ f
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift f (@inv _ _ inst_1 _ _ ≫ f)) μ =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η
have rwa : ∀
  (this :
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (lift (𝟙 A) (@inv _ _ inst_1 _ _)) (μ ≫ f) =
      CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η ≫ f),
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift f (@inv _ _ inst_1 _ _ ≫ f)) μ =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η
Tactic: rwa [assoc, IsMonHom.mul_hom, assoc, IsMonHom.one_hom, lift_map_assoc, id_comp] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Grp (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
A B : C
inst_2 : GrpObj A
inst_3 : GrpObj B
f : A ⟶ B
inst_4 : IsMonHom f
this :
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (lift (𝟙 A) (@inv _ _ inst_1 _ _)) μ ≫ f =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η ≫ f
rwa :
  ∀
    (this :
      CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (lift (𝟙 A) (@inv _ _ inst_1 _ _)) (μ ≫ f) =
        CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η ≫ f),
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift f (@inv _ _ inst_1 _ _ ≫ f)) μ =
      CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift f (@inv _ _ inst_1 _ _ ≫ f)) μ =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η
have rwa₁ : ∀
  (this :
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (lift (𝟙 A) (@inv _ _ inst_1 _ _)) ((f ⊗ₘ f) ≫ μ) =
      CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η ≫ f),
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift f (@inv _ _ inst_1 _ _ ≫ f)) μ =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η
Tactic: rwa [assoc, IsMonHom.mul_hom, assoc, IsMonHom.one_hom, lift_map_assoc, id_comp] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Grp (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
A B : C
inst_2 : GrpObj A
inst_3 : GrpObj B
f : A ⟶ B
inst_4 : IsMonHom f
this :
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (lift (𝟙 A) (@inv _ _ inst_1 _ _)) μ ≫ f =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η ≫ f
rwa :
  ∀
    (this :
      CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (lift (𝟙 A) (@inv _ _ inst_1 _ _)) (μ ≫ f) =
        CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η ≫ f),
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift f (@inv _ _ inst_1 _ _ ≫ f)) μ =
      CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η
rwa₁ :
  ∀
    (this :
      CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (lift (𝟙 A) (@inv _ _ inst_1 _ _)) ((f ⊗ₘ f) ≫ μ) =
        CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η ≫ f),
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift f (@inv _ _ inst_1 _ _ ≫ f)) μ =
      CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift f (@inv _ _ inst_1 _ _ ≫ f)) μ =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η
have rwa₂ : ∀
  (this :
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (lift (𝟙 A) (@inv _ _ inst_1 _ _)) ((f ⊗ₘ f) ≫ μ) =
      CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) (η ≫ f)),
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift f (@inv _ _ inst_1 _ _ ≫ f)) μ =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η
Tactic: rwa [assoc, IsMonHom.mul_hom, assoc, IsMonHom.one_hom, lift_map_assoc, id_comp] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Grp (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
A B : C
inst_2 : GrpObj A
inst_3 : GrpObj B
f : A ⟶ B
inst_4 : IsMonHom f
this :
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (lift (𝟙 A) (@inv _ _ inst_1 _ _)) μ ≫ f =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η ≫ f
rwa :
  ∀
    (this :
      CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (lift (𝟙 A) (@inv _ _ inst_1 _ _)) (μ ≫ f) =
        CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η ≫ f),
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift f (@inv _ _ inst_1 _ _ ≫ f)) μ =
      CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η
rwa₁ :
  ∀
    (this :
      CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (lift (𝟙 A) (@inv _ _ inst_1 _ _)) ((f ⊗ₘ f) ≫ μ) =
        CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η ≫ f),
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift f (@inv _ _ inst_1 _ _ ≫ f)) μ =
      CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η
rwa₂ :
  ∀
    (this :
      CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (lift (𝟙 A) (@inv _ _ inst_1 _ _)) ((f ⊗ₘ f) ≫ μ) =
        CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) (η ≫ f)),
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift f (@inv _ _ inst_1 _ _ ≫ f)) μ =
      CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift f (@inv _ _ inst_1 _ _ ≫ f)) μ =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η
have rwa₃ : ∀
  (this :
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (lift (𝟙 A) (@inv _ _ inst_1 _ _)) ((f ⊗ₘ f) ≫ μ) =
      CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η),
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift f (@inv _ _ inst_1 _ _ ≫ f)) μ =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η
Tactic: rwa [assoc, IsMonHom.mul_hom, assoc, IsMonHom.one_hom, lift_map_assoc, id_comp] at this
Cleared hypotheses: this