awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Action.Basic (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalLeftAction.{v_1, u_1, v_2, u_2} C D
x y : C
f : x ⟶ y
inst_4 : IsIso f
z : D
⊢ inv f ⊵ₗ z ≫ f ⊵ₗ z = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ y z)
have rw : (inv f ≫ f) ⊵ₗ z = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ y z)
Tactic: rw [← comp_actionHomLeft, IsIso.inv_hom_id, id_actionHomLeft]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Action.Basic (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalLeftAction.{v_1, u_1, v_2, u_2} C D
x y : C
f : x ⟶ y
inst_4 : IsIso f
z : D
rw : (inv f ≫ f) ⊵ₗ z = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ y z)
⊢ inv f ⊵ₗ z ≫ f ⊵ₗ z = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ y z)
have rw₁ : 𝟙 y ⊵ₗ z = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ y z)
Tactic: rw [← comp_actionHomLeft, IsIso.inv_hom_id, id_actionHomLeft]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Action.Basic (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalLeftAction.{v_1, u_1, v_2, u_2} C D
x y : C
f : x ⟶ y
inst_4 : IsIso f
z : D
rw : (inv f ≫ f) ⊵ₗ z = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ y z)
rw₁ : 𝟙 y ⊵ₗ z = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ y z)
⊢ inv f ⊵ₗ z ≫ f ⊵ₗ z = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ y z)
have rw₂ : Eq.{v_2 + 1} (α :=
  @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ y z ⟶
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ y z)
  (𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ y z))
  (𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ y z))
Tactic: rw [← comp_actionHomLeft, IsIso.inv_hom_id, id_actionHomLeft]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Action.Basic (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
x y : D
f : x ⟶ y
⊢ Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ y
        (tensorUnit.{v_1, u_1} C (𝒞 := inst)))
    (f ⊵ᵣ tensorUnit.{v_1, u_1} C (𝒞 := inst)) (Iso.hom (ρᵣ x) ≫ f ≫ Iso.inv (ρᵣ y))
have rw : Eq (α :=
  @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⟶
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ y (tensorUnit.{v_1, u_1} C (𝒞 := inst)))
  (f ⊵ᵣ tensorUnit.{v_1, u_1} C (𝒞 := inst))
  ((f ⊵ᵣ tensorUnit.{v_1, u_1} C (𝒞 := inst) ≫ Iso.hom (ρᵣ y)) ≫ Iso.inv (ρᵣ y))
Tactic: rw [← Category.assoc, actionUnitIso_hom_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Action.Basic (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
z z' : D
f : z ⟶ z'
x y : C
⊢ Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ z
        (tensorObj.{v_1, u_1} (𝒞 := inst) x y) ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ z'
        (tensorObj.{v_1, u_1} (𝒞 := inst) x y))
    (f ⊵ᵣ tensorObj.{v_1, u_1} (𝒞 := inst) x y) (Iso.hom (αᵣ z x y) ≫ (f ⊵ᵣ x) ⊵ᵣ y ≫ Iso.inv (αᵣ z' x y))
have simp : Eq (α :=
  @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ z (tensorObj.{v_1, u_1} (𝒞 := inst) x y) ⟶
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ z'
      (tensorObj.{v_1, u_1} (𝒞 := inst) x y))
  (f ⊙ᵣₘ 𝟙 (tensorObj.{v_1, u_1} (𝒞 := inst) x y)) (Iso.hom (αᵣ z x y) ≫ ((f ⊙ᵣₘ 𝟙 x) ⊙ᵣₘ 𝟙 y) ≫ Iso.inv (αᵣ z' x y))
Tactic: simp only [← actionHom_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Action.Basic (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
z z' : D
f : z ⟶ z'
x y : C
⊢ Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ z
        (tensorObj.{v_1, u_1} (𝒞 := inst) x y) ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ z'
        (tensorObj.{v_1, u_1} (𝒞 := inst) x y))
    (f ⊙ᵣₘ 𝟙 (tensorObj.{v_1, u_1} (𝒞 := inst) x y)) (Iso.hom (αᵣ z x y) ≫ ((f ⊙ᵣₘ 𝟙 x) ⊙ᵣₘ 𝟙 y) ≫ Iso.inv (αᵣ z' x y))
have rw : Eq (α :=
  @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ z (tensorObj.{v_1, u_1} (𝒞 := inst) x y) ⟶
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ z'
      (tensorObj.{v_1, u_1} (𝒞 := inst) x y))
  (f ⊙ᵣₘ 𝟙 (tensorObj.{v_1, u_1} (𝒞 := inst) x y)) (((f ⊙ᵣₘ 𝟙 x ⊗ₘ 𝟙 y) ≫ Iso.hom (αᵣ z' x y)) ≫ Iso.inv (αᵣ z' x y))
Tactic: rw [← Category.assoc, ← actionAssocIso_hom_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Action.Basic (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
d₁ d₂ : D
c₁ c₂ c₃ c₄ : C
f : d₁ ⟶ d₂
g : c₁ ⟶ c₂
h : c₃ ⟶ c₄
⊢ Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d₁ c₁) c₃ ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d₂
        (tensorObj.{v_1, u_1} (𝒞 := inst) c₂ c₄))
    (((f ⊙ᵣₘ g) ⊙ᵣₘ h) ≫ Iso.inv (αᵣ d₂ c₂ c₄)) (Iso.inv (αᵣ d₁ c₁ c₃) ≫ (f ⊙ᵣₘ g ⊗ₘ h))
have rw : Eq (α :=
  @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _
      (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d₁ c₁) c₃ ⟶
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _
      (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d₂ c₂) c₄)
  ((f ⊙ᵣₘ g) ⊙ᵣₘ h) ((Iso.inv (αᵣ d₁ c₁ c₃) ≫ (f ⊙ᵣₘ g ⊗ₘ h)) ≫ Iso.hom (αᵣ d₂ c₂ c₄))
Tactic: rw [Iso.comp_inv_eq, Category.assoc, Eq.comm, Iso.inv_comp_eq, actionAssocIso_hom_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Action.Basic (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
d₁ d₂ : D
c₁ c₂ c₃ c₄ : C
f : d₁ ⟶ d₂
g : c₁ ⟶ c₂
h : c₃ ⟶ c₄
rw :
  Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d₁ c₁) c₃ ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d₂ c₂) c₄)
    ((f ⊙ᵣₘ g) ⊙ᵣₘ h) ((Iso.inv (αᵣ d₁ c₁ c₃) ≫ (f ⊙ᵣₘ g ⊗ₘ h)) ≫ Iso.hom (αᵣ d₂ c₂ c₄))
⊢ Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d₁ c₁) c₃ ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d₂
        (tensorObj.{v_1, u_1} (𝒞 := inst) c₂ c₄))
    (((f ⊙ᵣₘ g) ⊙ᵣₘ h) ≫ Iso.inv (αᵣ d₂ c₂ c₄)) (Iso.inv (αᵣ d₁ c₁ c₃) ≫ (f ⊙ᵣₘ g ⊗ₘ h))
have rw₁ : Eq (α :=
  @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _
      (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d₁ c₁) c₃ ⟶
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _
      (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d₂ c₂) c₄)
  ((f ⊙ᵣₘ g) ⊙ᵣₘ h) (Iso.inv (αᵣ d₁ c₁ c₃) ≫ (f ⊙ᵣₘ g ⊗ₘ h) ≫ Iso.hom (αᵣ d₂ c₂ c₄))
Tactic: rw [Iso.comp_inv_eq, Category.assoc, Eq.comm, Iso.inv_comp_eq, actionAssocIso_hom_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Action.Basic (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
d₁ d₂ : D
c₁ c₂ c₃ c₄ : C
f : d₁ ⟶ d₂
g : c₁ ⟶ c₂
h : c₃ ⟶ c₄
rw :
  Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d₁ c₁) c₃ ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d₂ c₂) c₄)
    ((f ⊙ᵣₘ g) ⊙ᵣₘ h) ((Iso.inv (αᵣ d₁ c₁ c₃) ≫ (f ⊙ᵣₘ g ⊗ₘ h)) ≫ Iso.hom (αᵣ d₂ c₂ c₄))
rw₁ :
  Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d₁ c₁) c₃ ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d₂ c₂) c₄)
    ((f ⊙ᵣₘ g) ⊙ᵣₘ h) (Iso.inv (αᵣ d₁ c₁ c₃) ≫ (f ⊙ᵣₘ g ⊗ₘ h) ≫ Iso.hom (αᵣ d₂ c₂ c₄))
⊢ Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d₁ c₁) c₃ ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d₂
        (tensorObj.{v_1, u_1} (𝒞 := inst) c₂ c₄))
    (((f ⊙ᵣₘ g) ⊙ᵣₘ h) ≫ Iso.inv (αᵣ d₂ c₂ c₄)) (Iso.inv (αᵣ d₁ c₁ c₃) ≫ (f ⊙ᵣₘ g ⊗ₘ h))
have rw₂ : Eq (α :=
  @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _
      (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d₁ c₁) c₃ ⟶
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _
      (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d₂ c₂) c₄)
  (Iso.inv (αᵣ d₁ c₁ c₃) ≫ (f ⊙ᵣₘ g ⊗ₘ h) ≫ Iso.hom (αᵣ d₂ c₂ c₄)) ((f ⊙ᵣₘ g) ⊙ᵣₘ h)
Tactic: rw [Iso.comp_inv_eq, Category.assoc, Eq.comm, Iso.inv_comp_eq, actionAssocIso_hom_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Action.Basic (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
d₁ d₂ : D
c₁ c₂ c₃ c₄ : C
f : d₁ ⟶ d₂
g : c₁ ⟶ c₂
h : c₃ ⟶ c₄
rw :
  Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d₁ c₁) c₃ ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d₂ c₂) c₄)
    ((f ⊙ᵣₘ g) ⊙ᵣₘ h) ((Iso.inv (αᵣ d₁ c₁ c₃) ≫ (f ⊙ᵣₘ g ⊗ₘ h)) ≫ Iso.hom (αᵣ d₂ c₂ c₄))
rw₁ :
  Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d₁ c₁) c₃ ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d₂ c₂) c₄)
    ((f ⊙ᵣₘ g) ⊙ᵣₘ h) (Iso.inv (αᵣ d₁ c₁ c₃) ≫ (f ⊙ᵣₘ g ⊗ₘ h) ≫ Iso.hom (αᵣ d₂ c₂ c₄))
rw₂ :
  Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d₁ c₁) c₃ ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d₂ c₂) c₄)
    (Iso.inv (αᵣ d₁ c₁ c₃) ≫ (f ⊙ᵣₘ g ⊗ₘ h) ≫ Iso.hom (αᵣ d₂ c₂ c₄)) ((f ⊙ᵣₘ g) ⊙ᵣₘ h)
⊢ Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d₁ c₁) c₃ ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d₂
        (tensorObj.{v_1, u_1} (𝒞 := inst) c₂ c₄))
    (((f ⊙ᵣₘ g) ⊙ᵣₘ h) ≫ Iso.inv (αᵣ d₂ c₂ c₄)) (Iso.inv (αᵣ d₁ c₁ c₃) ≫ (f ⊙ᵣₘ g ⊗ₘ h))
have rw₃ : Eq (α :=
  @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d₁
      (tensorObj.{v_1, u_1} (𝒞 := inst) c₁ c₃) ⟶
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _
      (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d₂ c₂) c₄)
  ((f ⊙ᵣₘ g ⊗ₘ h) ≫ Iso.hom (αᵣ d₂ c₂ c₄)) (Iso.hom (αᵣ d₁ c₁ c₃) ≫ ((f ⊙ᵣₘ g) ⊙ᵣₘ h))
Tactic: rw [Iso.comp_inv_eq, Category.assoc, Eq.comm, Iso.inv_comp_eq, actionAssocIso_hom_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Action.Basic (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
d₁ d₂ : D
c₁ c₂ c₃ c₄ : C
f : d₁ ⟶ d₂
g : c₁ ⟶ c₂
h : c₃ ⟶ c₄
rw :
  Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d₁ c₁) c₃ ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d₂ c₂) c₄)
    ((f ⊙ᵣₘ g) ⊙ᵣₘ h) ((Iso.inv (αᵣ d₁ c₁ c₃) ≫ (f ⊙ᵣₘ g ⊗ₘ h)) ≫ Iso.hom (αᵣ d₂ c₂ c₄))
rw₁ :
  Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d₁ c₁) c₃ ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d₂ c₂) c₄)
    ((f ⊙ᵣₘ g) ⊙ᵣₘ h) (Iso.inv (αᵣ d₁ c₁ c₃) ≫ (f ⊙ᵣₘ g ⊗ₘ h) ≫ Iso.hom (αᵣ d₂ c₂ c₄))
rw₂ :
  Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d₁ c₁) c₃ ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d₂ c₂) c₄)
    (Iso.inv (αᵣ d₁ c₁ c₃) ≫ (f ⊙ᵣₘ g ⊗ₘ h) ≫ Iso.hom (αᵣ d₂ c₂ c₄)) ((f ⊙ᵣₘ g) ⊙ᵣₘ h)
rw₃ :
  Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d₁
        (tensorObj.{v_1, u_1} (𝒞 := inst) c₁ c₃) ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d₂ c₂) c₄)
    ((f ⊙ᵣₘ g ⊗ₘ h) ≫ Iso.hom (αᵣ d₂ c₂ c₄)) (Iso.hom (αᵣ d₁ c₁ c₃) ≫ ((f ⊙ᵣₘ g) ⊙ᵣₘ h))
⊢ Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d₁ c₁) c₃ ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d₂
        (tensorObj.{v_1, u_1} (𝒞 := inst) c₂ c₄))
    (((f ⊙ᵣₘ g) ⊙ᵣₘ h) ≫ Iso.inv (αᵣ d₂ c₂ c₄)) (Iso.inv (αᵣ d₁ c₁ c₃) ≫ (f ⊙ᵣₘ g ⊗ₘ h))
have rw₄ : Eq (α :=
  @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d₁
      (tensorObj.{v_1, u_1} (𝒞 := inst) c₁ c₃) ⟶
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _
      (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d₂ c₂) c₄)
  (Iso.hom (αᵣ d₁ c₁ c₃) ≫ ((f ⊙ᵣₘ g) ⊙ᵣₘ h)) (Iso.hom (αᵣ d₁ c₁ c₃) ≫ ((f ⊙ᵣₘ g) ⊙ᵣₘ h))
Tactic: rw [Iso.comp_inv_eq, Category.assoc, Eq.comm, Iso.inv_comp_eq, actionAssocIso_hom_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Action.Basic (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
d d' : D
f : d ⟶ d'
⊢ Eq (α :=
    d ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d'
        (tensorUnit.{v_1, u_1} C (𝒞 := inst)))
    (Iso.inv (ρᵣ d) ≫ f ⊵ᵣ tensorUnit.{v_1, u_1} C (𝒞 := inst)) (f ≫ Iso.inv (ρᵣ d'))
have rw : Eq (α :=
  @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⟶
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d' (tensorUnit.{v_1, u_1} C (𝒞 := inst)))
  (f ⊵ᵣ tensorUnit.{v_1, u_1} C (𝒞 := inst)) (Iso.hom (ρᵣ d) ≫ f ≫ Iso.inv (ρᵣ d'))
Tactic: rw [Iso.inv_comp_eq, ← Category.assoc, Eq.comm, Iso.comp_inv_eq, actionUnitIso_hom_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Action.Basic (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
d d' : D
f : d ⟶ d'
rw :
  Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d'
        (tensorUnit.{v_1, u_1} C (𝒞 := inst)))
    (f ⊵ᵣ tensorUnit.{v_1, u_1} C (𝒞 := inst)) (Iso.hom (ρᵣ d) ≫ f ≫ Iso.inv (ρᵣ d'))
⊢ Eq (α :=
    d ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d'
        (tensorUnit.{v_1, u_1} C (𝒞 := inst)))
    (Iso.inv (ρᵣ d) ≫ f ⊵ᵣ tensorUnit.{v_1, u_1} C (𝒞 := inst)) (f ≫ Iso.inv (ρᵣ d'))
have rw₁ : Eq (α :=
  @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⟶
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d' (tensorUnit.{v_1, u_1} C (𝒞 := inst)))
  (f ⊵ᵣ tensorUnit.{v_1, u_1} C (𝒞 := inst)) ((Iso.hom (ρᵣ d) ≫ f) ≫ Iso.inv (ρᵣ d'))
Tactic: rw [Iso.inv_comp_eq, ← Category.assoc, Eq.comm, Iso.comp_inv_eq, actionUnitIso_hom_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Action.Basic (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
d d' : D
f : d ⟶ d'
rw :
  Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d'
        (tensorUnit.{v_1, u_1} C (𝒞 := inst)))
    (f ⊵ᵣ tensorUnit.{v_1, u_1} C (𝒞 := inst)) (Iso.hom (ρᵣ d) ≫ f ≫ Iso.inv (ρᵣ d'))
rw₁ :
  Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d'
        (tensorUnit.{v_1, u_1} C (𝒞 := inst)))
    (f ⊵ᵣ tensorUnit.{v_1, u_1} C (𝒞 := inst)) ((Iso.hom (ρᵣ d) ≫ f) ≫ Iso.inv (ρᵣ d'))
⊢ Eq (α :=
    d ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d'
        (tensorUnit.{v_1, u_1} C (𝒞 := inst)))
    (Iso.inv (ρᵣ d) ≫ f ⊵ᵣ tensorUnit.{v_1, u_1} C (𝒞 := inst)) (f ≫ Iso.inv (ρᵣ d'))
have rw₂ : Eq (α :=
  @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⟶
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d' (tensorUnit.{v_1, u_1} C (𝒞 := inst)))
  ((Iso.hom (ρᵣ d) ≫ f) ≫ Iso.inv (ρᵣ d')) (f ⊵ᵣ tensorUnit.{v_1, u_1} C (𝒞 := inst))
Tactic: rw [Iso.inv_comp_eq, ← Category.assoc, Eq.comm, Iso.comp_inv_eq, actionUnitIso_hom_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Action.Basic (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
d d' : D
f : d ⟶ d'
rw :
  Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d'
        (tensorUnit.{v_1, u_1} C (𝒞 := inst)))
    (f ⊵ᵣ tensorUnit.{v_1, u_1} C (𝒞 := inst)) (Iso.hom (ρᵣ d) ≫ f ≫ Iso.inv (ρᵣ d'))
rw₁ :
  Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d'
        (tensorUnit.{v_1, u_1} C (𝒞 := inst)))
    (f ⊵ᵣ tensorUnit.{v_1, u_1} C (𝒞 := inst)) ((Iso.hom (ρᵣ d) ≫ f) ≫ Iso.inv (ρᵣ d'))
rw₂ :
  Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d'
        (tensorUnit.{v_1, u_1} C (𝒞 := inst)))
    ((Iso.hom (ρᵣ d) ≫ f) ≫ Iso.inv (ρᵣ d')) (f ⊵ᵣ tensorUnit.{v_1, u_1} C (𝒞 := inst))
⊢ Eq (α :=
    d ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d'
        (tensorUnit.{v_1, u_1} C (𝒞 := inst)))
    (Iso.inv (ρᵣ d) ≫ f ⊵ᵣ tensorUnit.{v_1, u_1} C (𝒞 := inst)) (f ≫ Iso.inv (ρᵣ d'))
have rw₃ : Eq (α :=
  @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⟶
    d')
  (Iso.hom (ρᵣ d) ≫ f) (f ⊵ᵣ tensorUnit.{v_1, u_1} C (𝒞 := inst) ≫ Iso.hom (ρᵣ d'))
Tactic: rw [Iso.inv_comp_eq, ← Category.assoc, Eq.comm, Iso.comp_inv_eq, actionUnitIso_hom_naturality]