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 (@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) η
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) η
⊢ 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) 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 B
f g h : A ⟶ B
⊢ f = CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift (g ≫ @inv _ _ inst_1 _ _) h) μ ↔
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift g f) μ = h
have refine_1 : f = CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift (g ≫ @inv _ _ inst_1 _ _) h) μ →
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift g f) μ = h
Tactic: refine ⟨?_, ?_⟩
-- 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 g h : A ⟶ B
refine_1 :
  f = CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift (g ≫ @inv _ _ inst_1 _ _) h) μ →
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift g f) μ = h
⊢ f = CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift (g ≫ @inv _ _ inst_1 _ _) h) μ ↔
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift g f) μ = h
have refine_2 : CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift g f) μ = h →
  f = CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift (g ≫ @inv _ _ inst_1 _ _) h) μ
Tactic: refine ⟨?_, ?_⟩
-- 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 g h : A ⟶ B
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift (f ≫ @inv _ _ inst_1 _ _) g) μ = h ↔
    g = CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift f h) μ
have rw : h = CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift (f ≫ @inv _ _ inst_1 _ _) g) μ ↔
  g = CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift f h) μ
Tactic: rw [eq_comm, eq_lift_inv_left, eq_comm]
-- 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 g h : A ⟶ B
rw :
  h = CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift (f ≫ @inv _ _ inst_1 _ _) g) μ ↔
    g = CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift f h) μ
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift (f ≫ @inv _ _ inst_1 _ _) g) μ = h ↔
    g = CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift f h) μ
have rw₁ : CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift f h) μ = g ↔
  g = CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift f h) μ
Tactic: rw [eq_comm, eq_lift_inv_left, eq_comm]
-- 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 g h : A ⟶ B
rw :
  h = CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift (f ≫ @inv _ _ inst_1 _ _) g) μ ↔
    g = CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift f h) μ
rw₁ :
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift f h) μ = g ↔
    g = CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift f h) μ
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift (f ≫ @inv _ _ inst_1 _ _) g) μ = h ↔
    g = CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift f h) μ
have rw₂ : g = CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift f h) μ ↔
  g = CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift f h) μ
Tactic: rw [eq_comm, eq_lift_inv_left, eq_comm]
-- 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 g h : A ⟶ B
⊢ f = CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift g (h ≫ @inv _ _ inst_1 _ _)) μ ↔
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift f h) μ = g
have refine_1 : f = CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift g (h ≫ @inv _ _ inst_1 _ _)) μ →
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift f h) μ = g
Tactic: refine ⟨?_, ?_⟩
-- 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 g h : A ⟶ B
refine_1 :
  f = CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift g (h ≫ @inv _ _ inst_1 _ _)) μ →
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift f h) μ = g
⊢ f = CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift g (h ≫ @inv _ _ inst_1 _ _)) μ ↔
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift f h) μ = g
have refine_2 : CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift f h) μ = g →
  f = CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift g (h ≫ @inv _ _ inst_1 _ _)) μ
Tactic: refine ⟨?_, ?_⟩
-- 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 g h : A ⟶ B
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift f (g ≫ @inv _ _ inst_1 _ _)) μ = h ↔
    f = CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift h g) μ
have rw : h = CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift f (g ≫ @inv _ _ inst_1 _ _)) μ ↔
  f = CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift h g) μ
Tactic: rw [eq_comm, eq_lift_inv_right, eq_comm]
-- 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 g h : A ⟶ B
rw :
  h = CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift f (g ≫ @inv _ _ inst_1 _ _)) μ ↔
    f = CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift h g) μ
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift f (g ≫ @inv _ _ inst_1 _ _)) μ = h ↔
    f = CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift h g) μ
have rw₁ : CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift h g) μ = f ↔
  f = CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift h g) μ
Tactic: rw [eq_comm, eq_lift_inv_right, eq_comm]
-- 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 g h : A ⟶ B
rw :
  h = CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift f (g ≫ @inv _ _ inst_1 _ _)) μ ↔
    f = CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift h g) μ
rw₁ :
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift h g) μ = f ↔
    f = CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift h g) μ
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift f (g ≫ @inv _ _ inst_1 _ _)) μ = h ↔
    f = CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift h g) μ
have rw₂ : f = CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift h g) μ ↔
  f = CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift h g) μ
Tactic: rw [eq_comm, eq_lift_inv_right, eq_comm]
-- 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 g i : A ⟶ B
h :
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift f i) μ =
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift g i) μ
⊢ f = g
have rwa : ∀
  (h :
    f =
      CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B)
        (lift (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift g i) μ) (i ≫ @inv _ _ inst_1 _ _))
        μ),
  f = g
Tactic: rwa [← eq_lift_inv_right, lift_lift_assoc, lift_comp_inv_right, lift_comp_one_right] at h
Cleared hypotheses: h
-- 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 g i : A ⟶ B
h :
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift f i) μ =
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift g i) μ
rwa :
  ∀
    (h :
      f =
        CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B)
          (lift (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift g i) μ) (i ≫ @inv _ _ inst_1 _ _))
          μ),
    f = g
⊢ f = g
have rwa₁ : ∀
  (h :
    f =
      CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B)
        (lift g (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift i (i ≫ @inv _ _ inst_1 _ _)) μ))
        μ),
  f = g
Tactic: rwa [← eq_lift_inv_right, lift_lift_assoc, lift_comp_inv_right, lift_comp_one_right] at h
Cleared hypotheses: h
-- 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 g i : A ⟶ B
h :
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift f i) μ =
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift g i) μ
rwa :
  ∀
    (h :
      f =
        CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B)
          (lift (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift g i) μ) (i ≫ @inv _ _ inst_1 _ _))
          μ),
    f = g
rwa₁ :
  ∀
    (h :
      f =
        CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B)
          (lift g (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift i (i ≫ @inv _ _ inst_1 _ _)) μ))
          μ),
    f = g
⊢ f = g
have rwa₂ : ∀
  (h :
    f =
      CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B)
        (lift g (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η)) μ),
  f = g
Tactic: rwa [← eq_lift_inv_right, lift_lift_assoc, lift_comp_inv_right, lift_comp_one_right] at h
Cleared hypotheses: h
-- 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 g i : A ⟶ B
h :
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift f i) μ =
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift g i) μ
rwa :
  ∀
    (h :
      f =
        CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B)
          (lift (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift g i) μ) (i ≫ @inv _ _ inst_1 _ _))
          μ),
    f = g
rwa₁ :
  ∀
    (h :
      f =
        CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B)
          (lift g (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift i (i ≫ @inv _ _ inst_1 _ _)) μ))
          μ),
    f = g
rwa₂ :
  ∀
    (h :
      f =
        CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B)
          (lift g (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η)) μ),
    f = g
⊢ f = g
have rwa₃ : ∀ (h : f = g), f = g
Tactic: rwa [← eq_lift_inv_right, lift_lift_assoc, lift_comp_inv_right, lift_comp_one_right] at h
Cleared hypotheses: h
-- 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 : C
inst_2 : GrpObj A
⊢ Eq.{v₁ + 1} (α := A ⟶ A) (@inv _ _ inst_1 _ _ ≫ @inv _ _ inst_1 _ _) (𝟙 A)
have apply : Eq.{v₁ + 1} (α := A ⟶ A)
  (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
    (lift (@inv _ _ inst_1 _ _ ≫ @inv _ _ inst_1 _ _) (@inv _ _ inst_1 _ _)) μ)
  (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (lift (𝟙 A) (@inv _ _ inst_1 _ _)) μ)
Tactic: apply lift_left_mul_ext ι[A]
-- 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 : C
inst_2 : GrpObj A
⊢ Eq.{v₁ + 1} (α := A ⟶ A)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (lift (@inv _ _ inst_1 _ _ ≫ @inv _ _ inst_1 _ _) (@inv _ _ inst_1 _ _)) μ)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (lift (𝟙 A) (@inv _ _ inst_1 _ _)) μ)
have rw : Eq.{v₁ + 1} (α := A ⟶ A)
  (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
    (lift (@inv _ _ inst_1 _ _ ≫ @inv _ _ inst_1 _ _) (@inv _ _ inst_1 _ _)) μ)
  (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η)
Tactic: rw [right_inv, ← comp_toUnit_assoc ι, ← left_inv, comp_lift_assoc, Category.comp_id]
-- 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 : C
inst_2 : GrpObj A
rw :
  Eq.{v₁ + 1} (α := A ⟶ A)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (lift (@inv _ _ inst_1 _ _ ≫ @inv _ _ inst_1 _ _) (@inv _ _ inst_1 _ _)) μ)
    (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η)
⊢ Eq.{v₁ + 1} (α := A ⟶ A)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (lift (@inv _ _ inst_1 _ _ ≫ @inv _ _ inst_1 _ _) (@inv _ _ inst_1 _ _)) μ)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (lift (𝟙 A) (@inv _ _ inst_1 _ _)) μ)
have rw₁ : Eq.{v₁ + 1} (α := A ⟶ A)
  (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
    (lift (@inv _ _ inst_1 _ _ ≫ @inv _ _ inst_1 _ _) (@inv _ _ inst_1 _ _)) μ)
  (@inv _ _ inst_1 _ _ ≫ CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η)
Tactic: rw [right_inv, ← comp_toUnit_assoc ι, ← left_inv, comp_lift_assoc, Category.comp_id]
-- 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 : C
inst_2 : GrpObj A
rw :
  Eq.{v₁ + 1} (α := A ⟶ A)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (lift (@inv _ _ inst_1 _ _ ≫ @inv _ _ inst_1 _ _) (@inv _ _ inst_1 _ _)) μ)
    (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η)
rw₁ :
  Eq.{v₁ + 1} (α := A ⟶ A)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (lift (@inv _ _ inst_1 _ _ ≫ @inv _ _ inst_1 _ _) (@inv _ _ inst_1 _ _)) μ)
    (@inv _ _ inst_1 _ _ ≫ CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η)
⊢ Eq.{v₁ + 1} (α := A ⟶ A)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (lift (@inv _ _ inst_1 _ _ ≫ @inv _ _ inst_1 _ _) (@inv _ _ inst_1 _ _)) μ)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (lift (𝟙 A) (@inv _ _ inst_1 _ _)) μ)
have rw₂ : Eq.{v₁ + 1} (α := A ⟶ A)
  (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
    (lift (@inv _ _ inst_1 _ _ ≫ @inv _ _ inst_1 _ _) (@inv _ _ inst_1 _ _)) μ)
  (@inv _ _ inst_1 _ _ ≫
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (lift (@inv _ _ inst_1 _ _) (𝟙 A)) μ)
Tactic: rw [right_inv, ← comp_toUnit_assoc ι, ← left_inv, comp_lift_assoc, Category.comp_id]
-- 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 : C
inst_2 : GrpObj A
rw :
  Eq.{v₁ + 1} (α := A ⟶ A)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (lift (@inv _ _ inst_1 _ _ ≫ @inv _ _ inst_1 _ _) (@inv _ _ inst_1 _ _)) μ)
    (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η)
rw₁ :
  Eq.{v₁ + 1} (α := A ⟶ A)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (lift (@inv _ _ inst_1 _ _ ≫ @inv _ _ inst_1 _ _) (@inv _ _ inst_1 _ _)) μ)
    (@inv _ _ inst_1 _ _ ≫ CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η)
rw₂ :
  Eq.{v₁ + 1} (α := A ⟶ A)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (lift (@inv _ _ inst_1 _ _ ≫ @inv _ _ inst_1 _ _) (@inv _ _ inst_1 _ _)) μ)
    (@inv _ _ inst_1 _ _ ≫
      CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (lift (@inv _ _ inst_1 _ _) (𝟙 A)) μ)
⊢ Eq.{v₁ + 1} (α := A ⟶ A)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (lift (@inv _ _ inst_1 _ _ ≫ @inv _ _ inst_1 _ _) (@inv _ _ inst_1 _ _)) μ)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (lift (𝟙 A) (@inv _ _ inst_1 _ _)) μ)
have rw₃ : Eq.{v₁ + 1} (α := A ⟶ A)
  (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
    (lift (@inv _ _ inst_1 _ _ ≫ @inv _ _ inst_1 _ _) (@inv _ _ inst_1 _ _)) μ)
  (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
    (lift (@inv _ _ inst_1 _ _ ≫ @inv _ _ inst_1 _ _) (@inv _ _ inst_1 _ _ ≫ 𝟙 A)) μ)
Tactic: rw [right_inv, ← comp_toUnit_assoc ι, ← left_inv, comp_lift_assoc, Category.comp_id]
-- 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 : C
inst_2 : GrpObj A
rw :
  Eq.{v₁ + 1} (α := A ⟶ A)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (lift (@inv _ _ inst_1 _ _ ≫ @inv _ _ inst_1 _ _) (@inv _ _ inst_1 _ _)) μ)
    (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η)
rw₁ :
  Eq.{v₁ + 1} (α := A ⟶ A)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (lift (@inv _ _ inst_1 _ _ ≫ @inv _ _ inst_1 _ _) (@inv _ _ inst_1 _ _)) μ)
    (@inv _ _ inst_1 _ _ ≫ CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η)
rw₂ :
  Eq.{v₁ + 1} (α := A ⟶ A)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (lift (@inv _ _ inst_1 _ _ ≫ @inv _ _ inst_1 _ _) (@inv _ _ inst_1 _ _)) μ)
    (@inv _ _ inst_1 _ _ ≫
      CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (lift (@inv _ _ inst_1 _ _) (𝟙 A)) μ)
rw₃ :
  Eq.{v₁ + 1} (α := A ⟶ A)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (lift (@inv _ _ inst_1 _ _ ≫ @inv _ _ inst_1 _ _) (@inv _ _ inst_1 _ _)) μ)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (lift (@inv _ _ inst_1 _ _ ≫ @inv _ _ inst_1 _ _) (@inv _ _ inst_1 _ _ ≫ 𝟙 A)) μ)
⊢ Eq.{v₁ + 1} (α := A ⟶ A)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (lift (@inv _ _ inst_1 _ _ ≫ @inv _ _ inst_1 _ _) (@inv _ _ inst_1 _ _)) μ)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (lift (𝟙 A) (@inv _ _ inst_1 _ _)) μ)
have rw₄ : Eq.{v₁ + 1} (α := A ⟶ A)
  (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
    (lift (@inv _ _ inst_1 _ _ ≫ @inv _ _ inst_1 _ _) (@inv _ _ inst_1 _ _)) μ)
  (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
    (lift (@inv _ _ inst_1 _ _ ≫ @inv _ _ inst_1 _ _) (@inv _ _ inst_1 _ _)) μ)
Tactic: rw [right_inv, ← comp_toUnit_assoc ι, ← left_inv, comp_lift_assoc, Category.comp_id]
-- 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 : C
inst_2 : GrpObj A
⊢ Eq.{v₁ + 1} (α := A ⟶ A) (CategoryTheory.inv (@inv _ _ inst_1 _ _)) (@inv _ _ inst_1 _ _)
have rw : Eq.{v₁ + 1} (α := A ⟶ A) (@inv _ _ inst_1 _ _) (CategoryTheory.inv (@inv _ _ inst_1 _ _))
Tactic: rw [eq_comm, ← CategoryTheory.inv_comp_eq_id, IsIso.inv_inv, inv_comp_inv]
-- 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 : C
inst_2 : GrpObj A
rw : Eq.{v₁ + 1} (α := A ⟶ A) (@inv _ _ inst_1 _ _) (CategoryTheory.inv (@inv _ _ inst_1 _ _))
⊢ Eq.{v₁ + 1} (α := A ⟶ A) (CategoryTheory.inv (@inv _ _ inst_1 _ _)) (@inv _ _ inst_1 _ _)
have rw₁ : Eq.{v₁ + 1} (α := A ⟶ A) (CategoryTheory.inv (CategoryTheory.inv (@inv _ _ inst_1 _ _)) ≫ @inv _ _ inst_1 _ _) (𝟙 A)
Tactic: rw [eq_comm, ← CategoryTheory.inv_comp_eq_id, IsIso.inv_inv, inv_comp_inv]
-- 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 : C
inst_2 : GrpObj A
rw : Eq.{v₁ + 1} (α := A ⟶ A) (@inv _ _ inst_1 _ _) (CategoryTheory.inv (@inv _ _ inst_1 _ _))
rw₁ :
  Eq.{v₁ + 1} (α := A ⟶ A) (CategoryTheory.inv (CategoryTheory.inv (@inv _ _ inst_1 _ _)) ≫ @inv _ _ inst_1 _ _) (𝟙 A)
⊢ Eq.{v₁ + 1} (α := A ⟶ A) (CategoryTheory.inv (@inv _ _ inst_1 _ _)) (@inv _ _ inst_1 _ _)
have rw₂ : Eq.{v₁ + 1} (α := A ⟶ A) (@inv _ _ inst_1 _ _ ≫ @inv _ _ inst_1 _ _) (𝟙 A)
Tactic: rw [eq_comm, ← CategoryTheory.inv_comp_eq_id, IsIso.inv_inv, inv_comp_inv]