awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.Action.End
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} D
F : C ⥤ Functor.{v_2, v_2, u_2, u_2} D D
inst_3 : F.Monoidal
c₁ c₁' : D
c₂ c₂' c₃ c₃' : C
f : c₁ ⟶ c₁'
g : c₂ ⟶ c₂'
h : c₃ ⟶ c₃'
⊢ Eq.{v_2 + 1} (α :=
    (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) c₂ c₃)).obj c₁ ⟶
      (tensorObj (𝒞 := Functor.category) (F.obj c₂') (F.obj c₃')).obj c₁)
    ((fun
          (t :
            F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) c₂ c₃) ⟶
              tensorObj (𝒞 := Functor.category) (F.obj c₂') (F.obj c₃')) ↦
        t.app c₁)
      (Functor.OplaxMonoidal.δ F c₂ c₃ ≫ (F.map g ⊗ₘ F.map h)))
    ((fun
          (t :
            F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) c₂ c₃) ⟶
              tensorObj (𝒞 := Functor.category) (F.obj c₂') (F.obj c₃')) ↦
        t.app c₁)
      (F.map (g ⊗ₘ h) ≫ Functor.OplaxMonoidal.δ F c₂' c₃'))

Tactic:
have e := congrArg (fun t ↦ t.app c₁) <|
      Functor.OplaxMonoidal.δ_natural F g h
-- Module: Mathlib.CategoryTheory.Monoidal.Action.End
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} D
F : C ⥤ Functor.{v_2, v_2, u_2, u_2} D D
inst_3 : F.Monoidal
c₁ c₁' : D
c₂ c₂' c₃ c₃' : C
f : c₁ ⟶ c₁'
g : c₂ ⟶ c₂'
h : c₃ ⟶ c₃'
e :
  Eq (α := (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) c₂ c₃)).obj c₁ ⟶ (F.obj c₃').obj ((F.obj c₂').obj c₁))
    (NatTrans.app (Functor.OplaxMonoidal.δ F c₂ c₃) c₁ ≫
      (F.map h).app ((F.obj c₂).obj c₁) ≫ (F.obj c₃').map ((F.map g).app c₁))
    (NatTrans.app (F.map (g ⊗ₘ h)) c₁ ≫ NatTrans.app (Functor.OplaxMonoidal.δ F c₂' c₃') c₁)
⊢ Eq (α := (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) c₂ c₃)).obj c₁ ⟶ (F.obj c₃').obj ((F.obj c₂').obj c₁'))
    (CategoryStruct.comp (Y := (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) c₂' c₃')).obj c₁')
      (CategoryStruct.comp (Y := (fun (d : D) (c : C) ↦ (F.obj c).obj d) c₁' (tensorObj.{v_1, u_1} (𝒞 := inst) c₂ c₃))
        ((fun {d d' : D} (f : d ⟶ d') (c : C) ↦ (F.obj c).map f) f (tensorObj.{v_1, u_1} (𝒞 := inst) c₂ c₃))
        ((fun (d : D) (x x_1 : C) (f : x ⟶ x_1) ↦ (F.map f).app d) c₁' (tensorObj.{v_1, u_1} (𝒞 := inst) c₂ c₃)
          (tensorObj.{v_1, u_1} (𝒞 := inst) c₂' c₃') (g ⊗ₘ h)))
      (Iso.hom (Iso.symm (Iso.app (Functor.Monoidal.μIso F c₂' c₃') c₁'))))
    (CategoryStruct.comp (Y := (F.obj c₃).obj ((F.obj c₂).obj c₁))
      (Iso.hom (Iso.symm (Iso.app (Functor.Monoidal.μIso F c₂ c₃) c₁)))
      (CategoryStruct.comp (Y := (fun (d : D) (c : C) ↦ (F.obj c).obj d) ((F.obj c₂').obj c₁') c₃)
        ((fun {d d' : D} (f : d ⟶ d') (c : C) ↦ (F.obj c).map f)
          (CategoryStruct.comp (Y := (fun (d : D) (c : C) ↦ (F.obj c).obj d) c₁' c₂)
            ((fun {d d' : D} (f : d ⟶ d') (c : C) ↦ (F.obj c).map f) f c₂)
            ((fun (d : D) (x x_1 : C) (f : x ⟶ x_1) ↦ (F.map f).app d) c₁' c₂ c₂' g))
          c₃)
        ((fun (d : D) (x x_1 : C) (f : x ⟶ x_1) ↦ (F.map f).app d) ((F.obj c₂').obj c₁') c₃ c₃' h)))

Tactic:
simp [reassoc_of% e]
-- Module: Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
Goal:
D : Type u_1
D' : Type u_2
inst : Category.{v_1, u_1} D
inst_1 : Category.{v_2, u_2} D'
F : Functor.{v_1, v_2, u_1, u_2} D D'
C : Type u_3
inst_2 : Category.{v_3, u_3} C
inst_3 : MonoidalCategory.{v_3, u_3} C
inst_4 : MonoidalLeftAction.{v_3, u_3, v_1, u_1} C D
inst_5 : MonoidalLeftAction.{v_3, u_3, v_2, u_2} C D'
inst_6 : LaxLeftLinear.{v_1, u_1, v_2, u_2, v_3, u_3} F C
c c' : C
d : D
⊢ Eq (α :=
    @actionObj.{v_3, u_3, v_2, u_2} _ _ inst_2 inst_1 toMonoidalCategoryStruct _ c
        (@actionObj.{v_3, u_3, v_2, u_2} _ _ inst_2 inst_1 toMonoidalCategoryStruct _ c' (F.obj d)) ⟶
      F.obj
        (@actionObj.{v_3, u_3, v_1, u_1} _ _ inst_2 inst toMonoidalCategoryStruct _
          (tensorObj.{v_3, u_3} (𝒞 := inst_2) c c') d))
    (c ⊴ₗ μₗ F c' d ≫
      μₗ F c (@actionObj.{v_3, u_3, v_1, u_1} _ _ inst_2 inst toMonoidalCategoryStruct _ c' d) ≫
        F.map (Iso.inv (αₗ c c' d)))
    (Iso.inv (αₗ c c' (F.obj d)) ≫ μₗ F (tensorObj.{v_3, u_3} (𝒞 := inst_2) c c') d)

Tactic:
simpa [-μₗ_associativity, -μₗ_associativity_assoc] using
    (αₗ _ _ _).inv ≫=
      (μₗ_associativity F c c' d).symm =≫
      F.map (αₗ _ _ _).inv

Premises used: CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso, CategoryTheory.Functor.map, CategoryTheory.Functor.LaxLeftLinear.μₗ_associativity, CategoryTheory.Functor.LaxLeftLinear.μₗ_associativity_assoc, Eq.symm, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
Goal:
D : Type u_1
D' : Type u_2
inst : Category.{v_1, u_1} D
inst_1 : Category.{v_2, u_2} D'
F : Functor.{v_1, v_2, u_1, u_2} D D'
C : Type u_3
inst_2 : Category.{v_3, u_3} C
inst_3 : MonoidalCategory.{v_3, u_3} C
inst_4 : MonoidalLeftAction.{v_3, u_3, v_1, u_1} C D
inst_5 : MonoidalLeftAction.{v_3, u_3, v_2, u_2} C D'
inst_6 : LaxLeftLinear.{v_1, u_1, v_2, u_2, v_3, u_3} F C
d : D
⊢ Eq (α :=
    F.obj d ⟶
      F.obj
        (@actionObj.{v_3, u_3, v_1, u_1} _ _ inst_2 inst toMonoidalCategoryStruct _
          (tensorUnit.{v_3, u_3} C (𝒞 := inst_2)) d))
    (CategoryStruct.comp (Y :=
      @actionObj.{v_3, u_3, v_2, u_2} _ _ inst_2 inst_1 toMonoidalCategoryStruct _
        (tensorUnit.{v_3, u_3} C (𝒞 := inst_2)) (F.obj d))
      (Iso.inv (λₗ (F.obj d))) (μₗ F (tensorUnit.{v_3, u_3} C (𝒞 := inst_2)) d))
    (F.map (Iso.inv (λₗ d)))

Tactic:
simpa [-μₗ_unitality] using
    (λₗ[C] (F.obj d)).inv ≫=
      (μₗ_unitality F d).symm =≫
      F.map (λₗ[C] d).inv

Premises used: CategoryTheory.Functor.map, CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso, CategoryTheory.Functor.LaxLeftLinear.μₗ_unitality, Eq.symm, CategoryTheory.Iso.inv, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
Goal:
D : Type u_1
D' : Type u_2
inst : Category.{v_1, u_1} D
inst_1 : Category.{v_2, u_2} D'
F : Functor.{v_1, v_2, u_1, u_2} D D'
C : Type u_3
inst_2 : Category.{v_3, u_3} C
inst_3 : MonoidalCategory.{v_3, u_3} C
inst_4 : MonoidalLeftAction.{v_3, u_3, v_1, u_1} C D
inst_5 : MonoidalLeftAction.{v_3, u_3, v_2, u_2} C D'
inst_6 : OplaxLeftLinear.{v_1, u_1, v_2, u_2, v_3, u_3} F C
c c' : C
d : D
⊢ Eq (α :=
    F.obj
        (@actionObj.{v_3, u_3, v_1, u_1} _ _ inst_2 inst toMonoidalCategoryStruct _ c
          (@actionObj.{v_3, u_3, v_1, u_1} _ _ inst_2 inst toMonoidalCategoryStruct _ c' d)) ⟶
      @actionObj.{v_3, u_3, v_2, u_2} _ _ inst_2 inst_1 toMonoidalCategoryStruct _
        (tensorObj.{v_3, u_3} (𝒞 := inst_2) c c') (F.obj d))
    (δₗ F c (@actionObj.{v_3, u_3, v_1, u_1} _ _ inst_2 inst toMonoidalCategoryStruct _ c' d) ≫
      c ⊴ₗ δₗ F c' d ≫ Iso.inv (αₗ c c' (F.obj d)))
    (F.map (Iso.inv (αₗ c c' d)) ≫ δₗ F (tensorObj.{v_3, u_3} (𝒞 := inst_2) c c') d)

Tactic:
simpa [-δₗ_associativity, -δₗ_associativity_assoc] using
    F.map (αₗ _ _ _).inv ≫=
      (δₗ_associativity F c c' d).symm =≫
      (αₗ _ _ _).inv

Premises used: CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso, CategoryTheory.Functor.OplaxLeftLinear.δₗ_associativity, CategoryTheory.Functor.map, CategoryTheory.Functor.OplaxLeftLinear.δₗ_associativity_assoc, Eq.symm, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
Goal:
D : Type u_1
D' : Type u_2
inst : Category.{v_1, u_1} D
inst_1 : Category.{v_2, u_2} D'
F : Functor.{v_1, v_2, u_1, u_2} D D'
C : Type u_3
inst_2 : Category.{v_3, u_3} C
inst_3 : MonoidalCategory.{v_3, u_3} C
inst_4 : MonoidalLeftAction.{v_3, u_3, v_1, u_1} C D
inst_5 : MonoidalLeftAction.{v_3, u_3, v_2, u_2} C D'
inst_6 : OplaxLeftLinear.{v_1, u_1, v_2, u_2, v_3, u_3} F C
d : D
⊢ Eq (α :=
    F.obj
        (@actionObj.{v_3, u_3, v_1, u_1} _ _ inst_2 inst toMonoidalCategoryStruct _
          (tensorUnit.{v_3, u_3} C (𝒞 := inst_2)) d) ⟶
      F.obj d)
    (CategoryStruct.comp (Y :=
      @actionObj.{v_3, u_3, v_2, u_2} _ _ inst_2 inst_1 toMonoidalCategoryStruct _
        (tensorUnit.{v_3, u_3} C (𝒞 := inst_2)) (F.obj d))
      (δₗ F (tensorUnit.{v_3, u_3} C (𝒞 := inst_2)) d) (Iso.hom (λₗ (F.obj d))))
    (F.map (Iso.hom (λₗ d)))

Tactic:
simpa [-δₗ_unitality_inv] using
    F.map (λₗ[C] d).hom ≫=
      (δₗ_unitality_inv F d).symm =≫
      (λₗ[C] (F.obj d)).hom

Premises used: CategoryTheory.Functor.OplaxLeftLinear.δₗ_unitality_inv, CategoryTheory.Functor.map, CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso, Eq.symm, CategoryTheory.Iso.hom, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
Goal:
D : Type u_1
D' : Type u_2
inst : Category.{v_1, u_1} D
inst_1 : Category.{v_2, u_2} D'
F : Functor.{v_1, v_2, u_1, u_2} D D'
C : Type u_3
inst_2 : Category.{v_3, u_3} C
inst_3 : MonoidalCategory.{v_3, u_3} C
inst_4 : MonoidalLeftAction.{v_3, u_3, v_1, u_1} C D
inst_5 : MonoidalLeftAction.{v_3, u_3, v_2, u_2} C D'
inst_6 : LeftLinear.{v_1, u_1, v_2, u_2, v_3, u_3} F C
c : C
d : D
⊢ IsIso (X := @actionObj.{v_3, u_3, v_2, u_2} _ _ inst_2 inst_1 toMonoidalCategoryStruct _ c (F.obj d)) (Y :=
    F.obj (@actionObj.{v_3, u_3, v_1, u_1} _ _ inst_2 inst toMonoidalCategoryStruct _ c d)) (μₗ F c d)

Tactic:
Iso.isIso_hom (μₗIso F c d)

Premises used: CategoryTheory.Functor.LeftLinear.μₗIso, CategoryTheory.Iso.isIso_hom
-- Module: Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
Goal:
D : Type u_1
D' : Type u_2
inst : Category.{v_1, u_1} D
inst_1 : Category.{v_2, u_2} D'
F : Functor.{v_1, v_2, u_1, u_2} D D'
C : Type u_3
inst_2 : Category.{v_3, u_3} C
inst_3 : MonoidalCategory.{v_3, u_3} C
inst_4 : MonoidalLeftAction.{v_3, u_3, v_1, u_1} C D
inst_5 : MonoidalLeftAction.{v_3, u_3, v_2, u_2} C D'
inst_6 : LeftLinear.{v_1, u_1, v_2, u_2, v_3, u_3} F C
c : C
d : D
⊢ IsIso (X := F.obj (@actionObj.{v_3, u_3, v_1, u_1} _ _ inst_2 inst toMonoidalCategoryStruct _ c d)) (Y :=
    @actionObj.{v_3, u_3, v_2, u_2} _ _ inst_2 inst_1 toMonoidalCategoryStruct _ c (F.obj d)) (δₗ F c d)

Tactic:
Iso.isIso_inv (μₗIso F c d)

Premises used: CategoryTheory.Functor.LeftLinear.μₗIso, CategoryTheory.Iso.isIso_inv
-- Module: Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
Goal:
D : Type u_1
D' : Type u_2
inst : Category.{v_1, u_1} D
inst_1 : Category.{v_2, u_2} D'
F : Functor.{v_1, v_2, u_1, u_2} D D'
C : Type u_3
inst_2 : Category.{v_3, u_3} C
inst_3 : MonoidalCategory.{v_3, u_3} C
inst_4 : MonoidalLeftAction.{v_3, u_3, v_1, u_1} C D
inst_5 : MonoidalLeftAction.{v_3, u_3, v_2, u_2} C D'
inst_6 : LeftLinear.{v_1, u_1, v_2, u_2, v_3, u_3} F C
c : C
d : D
⊢ Eq (α :=
    F.obj (@actionObj.{v_3, u_3, v_1, u_1} _ _ inst_2 inst toMonoidalCategoryStruct _ c d) ⟶
      @actionObj.{v_3, u_3, v_2, u_2} _ _ inst_2 inst_1 toMonoidalCategoryStruct _ c (F.obj d))
    (CategoryTheory.inv (μₗ F c d)) (δₗ F c d)

Tactic:
Eq.symm <| IsIso.eq_inv_of_hom_inv_id <| μₗ_comp_δₗ F c d

Premises used: CategoryTheory.IsIso.eq_inv_of_hom_inv_id, CategoryTheory.Functor.LeftLinear.μₗ_comp_δₗ, Eq.symm
-- Module: Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
Goal:
D : Type u_1
D' : Type u_2
inst : Category.{v_1, u_1} D
inst_1 : Category.{v_2, u_2} D'
F : Functor.{v_1, v_2, u_1, u_2} D D'
C : Type u_3
inst_2 : Category.{v_3, u_3} C
inst_3 : MonoidalCategory.{v_3, u_3} C
inst_4 : MonoidalLeftAction.{v_3, u_3, v_1, u_1} C D
inst_5 : MonoidalLeftAction.{v_3, u_3, v_2, u_2} C D'
inst_6 : LeftLinear.{v_1, u_1, v_2, u_2, v_3, u_3} F C
c : C
d : D
⊢ Eq (α :=
    @actionObj.{v_3, u_3, v_2, u_2} _ _ inst_2 inst_1 toMonoidalCategoryStruct _ c (F.obj d) ⟶
      F.obj (@actionObj.{v_3, u_3, v_1, u_1} _ _ inst_2 inst toMonoidalCategoryStruct _ c d))
    (CategoryTheory.inv (δₗ F c d)) (μₗ F c d)

Tactic:
Eq.symm <| IsIso.eq_inv_of_hom_inv_id <| δₗ_comp_μₗ F c d

Premises used: CategoryTheory.Functor.LeftLinear.δₗ_comp_μₗ, CategoryTheory.IsIso.eq_inv_of_hom_inv_id, Eq.symm
-- Module: Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
Goal:
D : Type u_1
D' : Type u_2
inst : Category.{v_1, u_1} D
inst_1 : Category.{v_2, u_2} D'
F : Functor.{v_1, v_2, u_1, u_2} D D'
C : Type u_3
inst_2 : Category.{v_3, u_3} C
inst_3 : MonoidalCategory.{v_3, u_3} C
inst_4 : MonoidalRightAction.{v_3, u_3, v_1, u_1} C D
inst_5 : MonoidalRightAction.{v_3, u_3, v_2, u_2} C D'
inst_6 : LaxRightLinear.{v_1, u_1, v_2, u_2, v_3, u_3} F C
d : D
c c' : C
⊢ Eq (α :=
    @actionObj.{v_3, u_3, v_2, u_2} _ _ inst_2 inst_1 toMonoidalCategoryStruct _
        (@actionObj.{v_3, u_3, v_2, u_2} _ _ inst_2 inst_1 toMonoidalCategoryStruct _ (F.obj d) c) c' ⟶
      F.obj
        (@actionObj.{v_3, u_3, v_1, u_1} _ _ inst_2 inst toMonoidalCategoryStruct _ d
          (tensorObj.{v_3, u_3} (𝒞 := inst_2) c c')))
    (μᵣ F d c ⊵ᵣ c' ≫
      μᵣ F (@actionObj.{v_3, u_3, v_1, u_1} _ _ inst_2 inst toMonoidalCategoryStruct _ d c) c' ≫
        F.map (Iso.inv (αᵣ d c c')))
    (Iso.inv (αᵣ (F.obj d) c c') ≫ μᵣ F d (tensorObj.{v_3, u_3} (𝒞 := inst_2) c c'))

Tactic:
simpa [-μᵣ_associativity, -μᵣ_associativity_assoc] using
    (αᵣ _ _ _).inv ≫=
      (μᵣ_associativity F d c c').symm =≫
      F.map (αᵣ _ _ _).inv

Premises used: CategoryTheory.Functor.map, CategoryTheory.Functor.LaxRightLinear.μᵣ_associativity_assoc, CategoryTheory.Functor.LaxRightLinear.μᵣ_associativity, CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso, Eq.symm, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
Goal:
D : Type u_1
D' : Type u_2
inst : Category.{v_1, u_1} D
inst_1 : Category.{v_2, u_2} D'
F : Functor.{v_1, v_2, u_1, u_2} D D'
C : Type u_3
inst_2 : Category.{v_3, u_3} C
inst_3 : MonoidalCategory.{v_3, u_3} C
inst_4 : MonoidalRightAction.{v_3, u_3, v_1, u_1} C D
inst_5 : MonoidalRightAction.{v_3, u_3, v_2, u_2} C D'
inst_6 : LaxRightLinear.{v_1, u_1, v_2, u_2, v_3, u_3} F C
d : D
⊢ Eq (α :=
    F.obj d ⟶
      F.obj
        (@actionObj.{v_3, u_3, v_1, u_1} _ _ inst_2 inst toMonoidalCategoryStruct _ d
          (tensorUnit.{v_3, u_3} C (𝒞 := inst_2))))
    (CategoryStruct.comp (Y :=
      @actionObj.{v_3, u_3, v_2, u_2} _ _ inst_2 inst_1 toMonoidalCategoryStruct _ (F.obj d)
        (tensorUnit.{v_3, u_3} C (𝒞 := inst_2)))
      (Iso.inv (ρᵣ (F.obj d))) (μᵣ F d (tensorUnit.{v_3, u_3} C (𝒞 := inst_2))))
    (F.map (Iso.inv (ρᵣ d)))

Tactic:
simpa [-μᵣ_unitality] using
    (ρᵣ[C] (F.obj d)).inv ≫=
      (μᵣ_unitality F d).symm =≫
      F.map (ρᵣ[C] d).inv

Premises used: CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso, CategoryTheory.Functor.map, CategoryTheory.Functor.LaxRightLinear.μᵣ_unitality, Eq.symm, CategoryTheory.Iso.inv, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
Goal:
D : Type u_1
D' : Type u_2
inst : Category.{v_1, u_1} D
inst_1 : Category.{v_2, u_2} D'
F : Functor.{v_1, v_2, u_1, u_2} D D'
C : Type u_3
inst_2 : Category.{v_3, u_3} C
inst_3 : MonoidalCategory.{v_3, u_3} C
inst_4 : MonoidalRightAction.{v_3, u_3, v_1, u_1} C D
inst_5 : MonoidalRightAction.{v_3, u_3, v_2, u_2} C D'
inst_6 : OplaxRightLinear.{v_1, u_1, v_2, u_2, v_3, u_3} F C
d : D
c c' : C
⊢ Eq (α :=
    F.obj
        (@actionObj.{v_3, u_3, v_1, u_1} _ _ inst_2 inst toMonoidalCategoryStruct _
          (@actionObj.{v_3, u_3, v_1, u_1} _ _ inst_2 inst toMonoidalCategoryStruct _ d c) c') ⟶
      @actionObj.{v_3, u_3, v_2, u_2} _ _ inst_2 inst_1 toMonoidalCategoryStruct _ (F.obj d)
        (tensorObj.{v_3, u_3} (𝒞 := inst_2) c c'))
    (δᵣ F (@actionObj.{v_3, u_3, v_1, u_1} _ _ inst_2 inst toMonoidalCategoryStruct _ d c) c' ≫
      δᵣ F d c ⊵ᵣ c' ≫ Iso.inv (αᵣ (F.obj d) c c'))
    (F.map (Iso.inv (αᵣ d c c')) ≫ δᵣ F d (tensorObj.{v_3, u_3} (𝒞 := inst_2) c c'))

Tactic:
simpa [-δᵣ_associativity, -δᵣ_associativity_assoc] using
    F.map (αᵣ _ _ _).inv ≫=
      (δᵣ_associativity F d c c').symm =≫
      (αᵣ _ _ _).inv

Premises used: CategoryTheory.Functor.OplaxRightLinear.δᵣ_associativity, CategoryTheory.Functor.map, CategoryTheory.Functor.OplaxRightLinear.δᵣ_associativity_assoc, CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso, Eq.symm, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
Goal:
D : Type u_1
D' : Type u_2
inst : Category.{v_1, u_1} D
inst_1 : Category.{v_2, u_2} D'
F : Functor.{v_1, v_2, u_1, u_2} D D'
C : Type u_3
inst_2 : Category.{v_3, u_3} C
inst_3 : MonoidalCategory.{v_3, u_3} C
inst_4 : MonoidalRightAction.{v_3, u_3, v_1, u_1} C D
inst_5 : MonoidalRightAction.{v_3, u_3, v_2, u_2} C D'
inst_6 : OplaxRightLinear.{v_1, u_1, v_2, u_2, v_3, u_3} F C
d : D
⊢ Eq (α :=
    F.obj
        (@actionObj.{v_3, u_3, v_1, u_1} _ _ inst_2 inst toMonoidalCategoryStruct _ d
          (tensorUnit.{v_3, u_3} C (𝒞 := inst_2))) ⟶
      F.obj d)
    (CategoryStruct.comp (Y :=
      @actionObj.{v_3, u_3, v_2, u_2} _ _ inst_2 inst_1 toMonoidalCategoryStruct _ (F.obj d)
        (tensorUnit.{v_3, u_3} C (𝒞 := inst_2)))
      (δᵣ F d (tensorUnit.{v_3, u_3} C (𝒞 := inst_2))) (Iso.hom (ρᵣ (F.obj d))))
    (F.map (Iso.hom (ρᵣ d)))

Tactic:
simpa [-δᵣ_unitality_inv] using
    F.map (ρᵣ[C] d).hom ≫=
      (δᵣ_unitality_inv F d).symm =≫
      (ρᵣ[C] (F.obj d)).hom

Premises used: CategoryTheory.Functor.OplaxRightLinear.δᵣ_unitality_inv, CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso, CategoryTheory.Functor.map, Eq.symm, CategoryTheory.Iso.hom, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
Goal:
D : Type u_1
D' : Type u_2
inst : Category.{v_1, u_1} D
inst_1 : Category.{v_2, u_2} D'
F : Functor.{v_1, v_2, u_1, u_2} D D'
C : Type u_3
inst_2 : Category.{v_3, u_3} C
inst_3 : MonoidalCategory.{v_3, u_3} C
inst_4 : MonoidalRightAction.{v_3, u_3, v_1, u_1} C D
inst_5 : MonoidalRightAction.{v_3, u_3, v_2, u_2} C D'
inst_6 : RightLinear.{v_1, u_1, v_2, u_2, v_3, u_3} F C
c : C
d : D
⊢ IsIso (X := @actionObj.{v_3, u_3, v_2, u_2} _ _ inst_2 inst_1 toMonoidalCategoryStruct _ (F.obj d) c) (Y :=
    F.obj (@actionObj.{v_3, u_3, v_1, u_1} _ _ inst_2 inst toMonoidalCategoryStruct _ d c)) (μᵣ F d c)

Tactic:
Iso.isIso_hom (μᵣIso F d c)

Premises used: CategoryTheory.Iso.isIso_hom, CategoryTheory.Functor.RightLinear.μᵣIso
-- Module: Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
Goal:
D : Type u_1
D' : Type u_2
inst : Category.{v_1, u_1} D
inst_1 : Category.{v_2, u_2} D'
F : Functor.{v_1, v_2, u_1, u_2} D D'
C : Type u_3
inst_2 : Category.{v_3, u_3} C
inst_3 : MonoidalCategory.{v_3, u_3} C
inst_4 : MonoidalRightAction.{v_3, u_3, v_1, u_1} C D
inst_5 : MonoidalRightAction.{v_3, u_3, v_2, u_2} C D'
inst_6 : RightLinear.{v_1, u_1, v_2, u_2, v_3, u_3} F C
c : C
d : D
⊢ IsIso (X := F.obj (@actionObj.{v_3, u_3, v_1, u_1} _ _ inst_2 inst toMonoidalCategoryStruct _ d c)) (Y :=
    @actionObj.{v_3, u_3, v_2, u_2} _ _ inst_2 inst_1 toMonoidalCategoryStruct _ (F.obj d) c) (δᵣ F d c)

Tactic:
Iso.isIso_inv (μᵣIso F d c)

Premises used: CategoryTheory.Iso.isIso_inv, CategoryTheory.Functor.RightLinear.μᵣIso
-- Module: Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
Goal:
D : Type u_1
D' : Type u_2
inst : Category.{v_1, u_1} D
inst_1 : Category.{v_2, u_2} D'
F : Functor.{v_1, v_2, u_1, u_2} D D'
C : Type u_3
inst_2 : Category.{v_3, u_3} C
inst_3 : MonoidalCategory.{v_3, u_3} C
inst_4 : MonoidalRightAction.{v_3, u_3, v_1, u_1} C D
inst_5 : MonoidalRightAction.{v_3, u_3, v_2, u_2} C D'
inst_6 : RightLinear.{v_1, u_1, v_2, u_2, v_3, u_3} F C
c : C
d : D
⊢ Eq (α :=
    F.obj (@actionObj.{v_3, u_3, v_1, u_1} _ _ inst_2 inst toMonoidalCategoryStruct _ d c) ⟶
      @actionObj.{v_3, u_3, v_2, u_2} _ _ inst_2 inst_1 toMonoidalCategoryStruct _ (F.obj d) c)
    (CategoryTheory.inv (μᵣ F d c)) (δᵣ F d c)

Tactic:
Eq.symm <| IsIso.eq_inv_of_hom_inv_id <| μᵣ_comp_δᵣ F d c

Premises used: CategoryTheory.Functor.RightLinear.μᵣ_comp_δᵣ, CategoryTheory.IsIso.eq_inv_of_hom_inv_id, Eq.symm
-- Module: Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
Goal:
D : Type u_1
D' : Type u_2
inst : Category.{v_1, u_1} D
inst_1 : Category.{v_2, u_2} D'
F : Functor.{v_1, v_2, u_1, u_2} D D'
C : Type u_3
inst_2 : Category.{v_3, u_3} C
inst_3 : MonoidalCategory.{v_3, u_3} C
inst_4 : MonoidalRightAction.{v_3, u_3, v_1, u_1} C D
inst_5 : MonoidalRightAction.{v_3, u_3, v_2, u_2} C D'
inst_6 : RightLinear.{v_1, u_1, v_2, u_2, v_3, u_3} F C
c : C
d : D
⊢ Eq (α :=
    @actionObj.{v_3, u_3, v_2, u_2} _ _ inst_2 inst_1 toMonoidalCategoryStruct _ (F.obj d) c ⟶
      F.obj (@actionObj.{v_3, u_3, v_1, u_1} _ _ inst_2 inst toMonoidalCategoryStruct _ d c))
    (CategoryTheory.inv (δᵣ F d c)) (μᵣ F d c)

Tactic:
Eq.symm <| IsIso.eq_inv_of_hom_inv_id <| δᵣ_comp_μᵣ F d c

Premises used: CategoryTheory.Functor.RightLinear.δᵣ_comp_μᵣ, CategoryTheory.IsIso.eq_inv_of_hom_inv_id, Eq.symm
-- Module: Mathlib.CategoryTheory.Monoidal.Action.Opposites
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} D
inst_3 : MonoidalRightAction.{v_1, u_1, v_2, u_2} Cᴹᵒᵖ D
c₁ c₂ c₃ : C
d : D
⊢ d ⊴ᵣ Quiver.Hom.mop (Iso.hom (α_ c₁ c₂ c₃)) ≫
      Iso.hom (αᵣ d { unmop := tensorObj.{v_1, u_1} (𝒞 := inst) c₂ c₃ : Cᴹᵒᵖ } { unmop := c₁ : Cᴹᵒᵖ }) ≫
        Iso.hom (αᵣ d { unmop := c₃ } { unmop := c₂ }) ⊵ᵣ { unmop := c₁ } =
    Iso.hom (αᵣ d { unmop := c₃ : Cᴹᵒᵖ } { unmop := tensorObj.{v_1, u_1} (𝒞 := inst) c₁ c₂ : Cᴹᵒᵖ }) ≫
      Iso.hom
        (αᵣ
          (@MonoidalRightActionStruct.actionObj.{v_1, u_1, v_2, u_2} _ _ monoidalOppositeCategory inst_2
            toMonoidalCategoryStruct _ d { unmop := c₃ : Cᴹᵒᵖ })
          { unmop := c₂ : Cᴹᵒᵖ } { unmop := c₁ : Cᴹᵒᵖ })

Tactic:
simpa only [mop_tensorObj, mop_hom_associator,
      MonoidalRightAction.actionHomRight_inv_hom_assoc] using
      (d ⊴ᵣ (α_ (mop c₃) (mop c₂) (mop c₁)).inv) ≫=
        MonoidalRightAction.actionHom_associator
          (mop c₃) (mop c₂) (mop c₁) d |>.symm

Premises used: CategoryTheory.MonoidalOpposite.mop, CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_associator, CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight, CategoryTheory.mop_tensorObj, CategoryTheory.mop_hom_associator, CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomRight_inv_hom_assoc, CategoryTheory.MonoidalCategoryStruct.associator, Eq.symm, CategoryTheory.whisker_eq, CategoryTheory.Iso.inv