awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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) η
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) η
⊢ 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) B B) (lift (𝟙 A ≫ 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) η
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) η
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) η
rwa₄ :
  ∀
    (this :
      CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift (𝟙 A ≫ 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) η
⊢ 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) 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) η
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 (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 ≫ @inv _ _ inst_1 _ _) f) μ =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η
have this : f ≫ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift (@inv _ _ inst_1 _ _) (𝟙 B)) μ =
  f ≫ CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit B) η
Tactic: have := f ≫= left_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 (@inv _ _ inst_1 _ _) (𝟙 B)) μ =
    f ≫ CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit B) η
⊢ 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) B B) (lift (f ≫ @inv _ _ inst_1 _ _) (f ≫ 𝟙 B)) μ =
      f ≫ CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit B) η),
  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 [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 (@inv _ _ inst_1 _ _) (𝟙 B)) μ =
    f ≫ CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit B) η
rwa :
  ∀
    (this :
      CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift (f ≫ @inv _ _ inst_1 _ _) (f ≫ 𝟙 B)) μ =
        f ≫ CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit B) η),
    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) B B) (lift (f ≫ @inv _ _ inst_1 _ _) f) μ =
      f ≫ CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit B) η),
  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 [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 (@inv _ _ inst_1 _ _) (𝟙 B)) μ =
    f ≫ CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit B) η
rwa :
  ∀
    (this :
      CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift (f ≫ @inv _ _ inst_1 _ _) (f ≫ 𝟙 B)) μ =
        f ≫ CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit B) η),
    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) B B) (lift (f ≫ @inv _ _ inst_1 _ _) f) μ =
        f ≫ CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit B) η),
    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) 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) η
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 (@inv _ _ inst_1 _ _ ≫ f) f) μ =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η
have this : CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (lift (@inv _ _ inst_1 _ _) (𝟙 A)) μ ≫ f =
  CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η ≫ f
Tactic: have := left_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 (@inv _ _ inst_1 _ _) (𝟙 A)) μ ≫ f =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η ≫ f
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift (@inv _ _ inst_1 _ _ ≫ f) f) μ =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η
have rwa : ∀
  (this :
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (lift (@inv _ _ inst_1 _ _) (𝟙 A)) (μ ≫ f) =
      CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η ≫ f),
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift (@inv _ _ inst_1 _ _ ≫ f) 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 (@inv _ _ inst_1 _ _) (𝟙 A)) μ ≫ f =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η ≫ f
rwa :
  ∀
    (this :
      CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (lift (@inv _ _ inst_1 _ _) (𝟙 A)) (μ ≫ f) =
        CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η ≫ f),
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift (@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 (@inv _ _ inst_1 _ _ ≫ f) f) μ =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η
have rwa₁ : ∀
  (this :
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (lift (@inv _ _ inst_1 _ _) (𝟙 A)) ((f ⊗ₘ f) ≫ μ) =
      CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η ≫ f),
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift (@inv _ _ inst_1 _ _ ≫ f) 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 (@inv _ _ inst_1 _ _) (𝟙 A)) μ ≫ f =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η ≫ f
rwa :
  ∀
    (this :
      CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (lift (@inv _ _ inst_1 _ _) (𝟙 A)) (μ ≫ f) =
        CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η ≫ f),
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift (@inv _ _ inst_1 _ _ ≫ f) f) μ =
      CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η
rwa₁ :
  ∀
    (this :
      CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (lift (@inv _ _ inst_1 _ _) (𝟙 A)) ((f ⊗ₘ f) ≫ μ) =
        CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η ≫ f),
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift (@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 (@inv _ _ inst_1 _ _ ≫ f) f) μ =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η
have rwa₂ : ∀
  (this :
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (lift (@inv _ _ inst_1 _ _) (𝟙 A)) ((f ⊗ₘ f) ≫ μ) =
      CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) (η ≫ f)),
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift (@inv _ _ inst_1 _ _ ≫ f) 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 (@inv _ _ inst_1 _ _) (𝟙 A)) μ ≫ f =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η ≫ f
rwa :
  ∀
    (this :
      CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (lift (@inv _ _ inst_1 _ _) (𝟙 A)) (μ ≫ f) =
        CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η ≫ f),
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift (@inv _ _ inst_1 _ _ ≫ f) f) μ =
      CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η
rwa₁ :
  ∀
    (this :
      CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (lift (@inv _ _ inst_1 _ _) (𝟙 A)) ((f ⊗ₘ f) ≫ μ) =
        CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η ≫ f),
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift (@inv _ _ inst_1 _ _ ≫ f) f) μ =
      CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η
rwa₂ :
  ∀
    (this :
      CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (lift (@inv _ _ inst_1 _ _) (𝟙 A)) ((f ⊗ₘ f) ≫ μ) =
        CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) (η ≫ f)),
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift (@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 (@inv _ _ inst_1 _ _ ≫ f) f) μ =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η
have rwa₃ : ∀
  (this :
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (lift (@inv _ _ inst_1 _ _) (𝟙 A)) ((f ⊗ₘ f) ≫ μ) =
      CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η),
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift (@inv _ _ inst_1 _ _ ≫ f) 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 (@inv _ _ inst_1 _ _) (𝟙 A)) μ ≫ f =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η ≫ f
rwa :
  ∀
    (this :
      CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (lift (@inv _ _ inst_1 _ _) (𝟙 A)) (μ ≫ f) =
        CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η ≫ f),
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift (@inv _ _ inst_1 _ _ ≫ f) f) μ =
      CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η
rwa₁ :
  ∀
    (this :
      CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (lift (@inv _ _ inst_1 _ _) (𝟙 A)) ((f ⊗ₘ f) ≫ μ) =
        CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η ≫ f),
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift (@inv _ _ inst_1 _ _ ≫ f) f) μ =
      CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η
rwa₂ :
  ∀
    (this :
      CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (lift (@inv _ _ inst_1 _ _) (𝟙 A)) ((f ⊗ₘ f) ≫ μ) =
        CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) (η ≫ f)),
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift (@inv _ _ inst_1 _ _ ≫ f) f) μ =
      CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η
rwa₃ :
  ∀
    (this :
      CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (lift (@inv _ _ inst_1 _ _) (𝟙 A)) ((f ⊗ₘ f) ≫ μ) =
        CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η),
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift (@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 (@inv _ _ inst_1 _ _ ≫ f) f) μ =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η
have rwa₄ : ∀
  (this :
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift (@inv _ _ inst_1 _ _ ≫ f) (𝟙 A ≫ f)) μ =
      CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η),
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift (@inv _ _ inst_1 _ _ ≫ f) 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