mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.WithAlgebraicStructures

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
J : Type w
inst✝³ : Category.{r, w} J
F : J ⥤ ModuleCat R
inst✝² : PreservesColimit F (forget (ModuleCat R))
inst✝¹ : IsFiltered J
inst✝ : HasColimit F
r : R
H : ∃ j', ∀ (j : J) (x : j' ⟶ j) (c : ↑(F.obj j)), r • c = 0 → c = 0
x : ToType (colimit F)
hx : r • x = 0
⊢ x = 0

Tactic:
obtain ⟨j, x, rfl⟩ := Concrete.colimit_exists_rep F x
  rw [← map_smul (colimit.ι F j).hom] at hx
  obtain ⟨j', i, h⟩ := Concrete.colimit_rep_eq_zero (hx := hx)
  obtain ⟨j'', H⟩ := H
  simpa [elementwise_of% (colimit.w F), map_zero] using congr(colimit.ι F _
    $(H (IsFiltered.sup {j, j', j''} { ⟨j, j', by simp, by simp, i⟩ })
      (IsFiltered.toSup _ _ <| by simp)
      (F.map (IsFiltered.toSup _ _ <| by simp) x)
      (by rw [← IsFiltered.toSup_commutes (f := i) (mY := by simp) (mf := by simp), F.map_comp,
        ModuleCat.comp_apply, ← map_smul, ← map_smul, h, map_zero])))

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
h : ChosenPullback f₁ f₂
Y : C
g₁ : Y ⟶ X₁
g₂ : Y ⟶ X₂
b : Y ⟶ S
w : g₁ ≫ f₁ = g₂ ≫ f₂
hf₁ : g₁ ≫ f₁ = b
⊢ Nonempty (h.LiftStruct g₁ g₂ b)

Tactic:
by
  obtain ⟨l, h₁, h₂⟩ := h.isPullback.exists_lift g₁ g₂ w
  exact ⟨{
    f := l
    f_p₁ := h₁
    f_p₂ := h₂
    f_p := by rw [← h.hp₁, ← hf₁, reassoc_of% h₁] }⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct

Goal state before:
pp: C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
m n : ℕ
h : ¬n < m
⊢ (cone f).π.app (Opposite.op m) ≫ Pi.π (fun m_1 ↦ if x : m_1 < Opposite.unop (Opposite.op m) then M m_1 else N m_1) n =
    Pi.π M n ≫ f n ≫ eqToHom ⋯

Tactic:
simp [cone_π_app, dif_neg h]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct

Goal state before:
pp: case e_a.le_succ_of_le
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
s : Cone (Functor.ofOpSequence (functorMap f))
n✝ m n : ℕ
hh : m + 1 ≤ n
ih :
  ∀ (h : m < n),
    (Functor.ofOpSequence (functorMap f)).map (homOfLE hh).op ≫
        Pi.π (fun i ↦ if i < m + 1 then M i else N i) m ≫ eqToHom ⋯ =
      Pi.π (fun m ↦ if m < n then M m else N m) m
h : m < n + 1
this : homOfLE ⋯ = homOfLE hh ≫ homOfLE ⋯
h₁ : (if x : m < m + 1 then M m else N m) = if x : m < n then M m else N m
h₂ : (if x : m < n then M m else N m) = if x : m < n + 1 then M m else N m
⊢ limit.π (Discrete.functor fun m ↦ if m < n + 1 then M m else N m) { as := m } ≫
      (if h : m < n then eqToHom ⋯ else eqToHom ⋯ ≫ f m ≫ eqToHom ⋯) ≫ eqToHom h₂ =
    limit.π (Discrete.functor fun m ↦ if m < n + 1 then M m else N m) { as := m }

Tactic:
rw [dif_pos (by lia)]

Goal state after:
case e_a.le_succ_of_le
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
s : Cone (Functor.ofOpSequence (functorMap f))
n✝ m n : ℕ
hh : m + 1 ≤ n
ih :
  ∀ (h : m < n),
    (Functor.ofOpSequence (functorMap f)).map (homOfLE hh).op ≫
        Pi.π (fun i ↦ if i < m + 1 then M i else N i) m ≫ eqToHom ⋯ =
      Pi.π (fun m ↦ if m < n then M m else N m) m
h : m < n + 1
this : homOfLE ⋯ = homOfLE hh ≫ homOfLE ⋯
h₁ : (if x : m < m + 1 then M m else N m) = if x : m < n then M m else N m
h₂ : (if x : m < n then M m else N m) = if x : m < n + 1 then M m else N m
⊢ limit.π (Discrete.functor fun m ↦ if m < n + 1 then M m else N m) { as := m } ≫ eqToHom ⋯ ≫ eqToHom h₂ =
    limit.π (Discrete.functor fun m ↦ if m < n + 1 then M m else N m) { as := m }
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
A' : Type u₄
B' : Type u₅
C' : Type u₆
inst✝⁶ : Category.{v₁, u₁} A
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
inst✝³ : Category.{v₄, u₄} A'
inst✝² : Category.{v₅, u₅} B'
inst✝¹ : Category.{v₆, u₆} C'
F' : A' ⥤ B'
G' : C' ⥤ B'
ψ' : CatCospanTransform F G F' G'
f : ψ' ⟶ ψ'
inst✝ : IsIso f
⊢ inv f.base = (inv f).base

Tactic:
by
  symm
  apply IsIso.eq_inv_of_inv_hom_id
  simp [← CatCospanTransform.category_comp_base]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Free.Basic

Goal state before:
pp: case comp
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝¹ : C → D
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f g : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
X✝ Y✝ Z✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f✝ f'✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g✝ g'✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
a✝¹ : HomEquiv f✝ f'✝
a✝ : HomEquiv g✝ g'✝
hf : projectMapAux f✝¹ f✝ = projectMapAux f✝¹ f'✝
hg : projectMapAux f✝¹ g✝ = projectMapAux f✝¹ g'✝
⊢ projectMapAux f✝¹ f✝ ≫ projectMapAux f✝¹ g✝ = projectMapAux f✝¹ f'✝ ≫ projectMapAux f✝¹ g'✝

Tactic:
rw [hf, hg]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Monoidal.Braided

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝³ : MonoidalCategory C
inst✝² : W.IsMonoidal
inst✝¹ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
inst✝ : BraidedCategory C
X Y Z : C
⊢ (α_ (L'.obj X) (L'.obj Y) (L'.obj Z)).inv ≫
      (((braidingNatIso L W ε).app (L'.obj X ⊗ L'.obj Y)).app (L'.obj Z)).hom ≫
        (α_ (L'.obj Z) (L'.obj X) (L'.obj Y)).inv =
    L'.obj X ◁ (((braidingNatIso L W ε).app (L'.obj Y)).app (L'.obj Z)).hom ≫
      (α_ (L'.obj X) (L'.obj Z) (L'.obj Y)).inv ≫
        (((braidingNatIso L W ε).app (L'.obj X)).app (L'.obj Z)).hom ▷ L'.obj Y

Tactic:
by
  simp only [associator_inv, Iso.app_hom, braidingNatIso_hom_app]
  slice_rhs 0 4 =>
    simp only [Functor.flip_obj_obj, Functor.CoreMonoidal.toMonoidal_toLaxMonoidal,
      Functor.CoreMonoidal.toMonoidal_toOplaxMonoidal, MonoidalCategory.whiskerLeft_comp, assoc,
      Functor.Monoidal.whiskerLeft_δ_μ, comp_id]
  slice_lhs 6 7 =>
    rw [braidingNatIso_hom_app_naturality_μ_right, braidingNatIso_hom_app]
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Free.Basic

Goal state before:
pp: case l_inv_hom
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝ : C → D
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f g : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
X✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ projectMapAux f✝ ((l_inv X✝).comp (l_hom X✝)) = projectMapAux f✝ (Hom.id X✝)

Tactic:
| l_inv_hom =>

Goal state after:
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
I : C
inst✝¹ : ChosenPullbacksAlong (𝟙 I)
inst✝ : ExponentiableMorphism (𝟙 I)
⊢ Functor.whiskerRight (pushforwardId I).hom (pullback (𝟙 I)) ≫ (pullbackPushforwardAdj (𝟙 I)).counit =
    (pullbackPushforwardAdj (𝟙 I)).counit

Tactic:
by
  rw [pushforwardId, Adjunction.rightAdjointUniq_hom_counit]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Monoidal.Functor

Goal state before:
pp: case refine_1
C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory D
inst✝⁵ : MonoidalCategory E
L : C ⥤ D
W : MorphismProperty C
inst✝⁴ : L.IsLocalization W
inst✝³ : L.Monoidal
F : D ⥤ E
G : C ⥤ E
inst✝² : G.Monoidal
inst✝¹ : W.ContainsIdentities
inst✝ : Lifting L W G F
e : L ⋙ F ≅ G := Lifting.iso L W G F
X₁ X₂ X₃ : C
⊢ ((curriedTensorPreIsoPost L W F G).hom.app (L.obj X₁)).app (L.obj X₂) ▷ F.obj (L.obj X₃) ≫
      ((curriedTensorPreIsoPost L W F G).hom.app (L.obj X₁ ⊗ L.obj X₂)).app (L.obj X₃) ≫
        F.map (α_ (L.obj X₁) (L.obj X₂) (L.obj X₃)).hom =
    (α_ (F.obj (L.obj X₁)) (F.obj (L.obj X₂)) (F.obj (L.obj X₃))).hom ≫
      F.obj (L.obj X₁) ◁ ((curriedTensorPreIsoPost L W F G).hom.app (L.obj X₂)).app (L.obj X₃) ≫
        ((curriedTensorPreIsoPost L W F G).hom.app (L.obj X₁)).app (L.obj X₂ ⊗ L.obj X₃)

Tactic:
rw [curriedTensorPreIsoPost_hom_app_app, curriedTensorPreIsoPost_hom_app_app,
      curriedTensorPreIsoPost_hom_app_app' L W F G (μIso L _ _) (Iso.refl _),
      curriedTensorPreIsoPost_hom_app_app' L W F G (Iso.refl _) (μIso L _ _)]

Goal state after:
case refine_1
C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory D
inst✝⁵ : MonoidalCategory E
L : C ⥤ D
W : MorphismProperty C
inst✝⁴ : L.IsLocalization W
inst✝³ : L.Monoidal
F : D ⥤ E
G : C ⥤ E
inst✝² : G.Monoidal
inst✝¹ : W.ContainsIdentities
inst✝ : Lifting L W G F
e : L ⋙ F ≅ G := Lifting.iso L W G F
X₁ X₂ X₃ : C
⊢ (((Lifting.iso L W G F).hom.app X₁ ⊗ₘ (Lifting.iso L W G F).hom.app X₂) ≫
          μ G X₁ X₂ ≫ (Lifting.iso L W G F).inv.app (X₁ ⊗ X₂) ≫ F.map (δ L X₁ X₂)) ▷
        F.obj (L.obj X₃) ≫
      ((F.map (μIso L X₁ X₂).hom ≫ (Lifting.iso L W G F).hom.app (X₁ ⊗ X₂) ⊗ₘ
            F.map (Iso.refl (L.obj X₃)).hom ≫ (Lifting.iso L W G F).hom.app X₃) ≫
          μ G (X₁ ⊗ X₂) X₃ ≫
            (Lifting.iso L W G F).inv.app ((X₁ ⊗ X₂) ⊗ X₃) ≫
              F.map (δ L (X₁ ⊗ X₂) X₃ ≫ ((μIso L X₁ X₂).inv ⊗ₘ (Iso.refl (L.obj X₃)).inv))) ≫
        F.map (α_ (L.obj X₁) (L.obj X₂) (L.obj X₃)).hom =
    (α_ (F.obj (L.obj X₁)) (F.obj (L.obj X₂)) (F.obj (L.obj X₃))).hom ≫
      F.obj (L.obj X₁) ◁
          (((Lifting.iso L W G F).hom.app X₂ ⊗ₘ (Lifting.iso L W G F).hom.app X₃) ≫
            μ G X₂ X₃ ≫ (Lifting.iso L W G F).inv.app (X₂ ⊗ X₃) ≫ F.map (δ L X₂ X₃)) ≫
        (F.map (Iso.refl (L.obj X₁)).hom ≫ (Lifting.iso L W G F).hom.app X₁ ⊗ₘ
            F.map (μIso L X₂ X₃).hom ≫ (Lifting.iso L W G F).hom.app (X₂ ⊗ X₃)) ≫
          μ G X₁ (X₂ ⊗ X₃) ≫
            (Lifting.iso L W G F).inv.app (X₁ ⊗ X₂ ⊗ X₃) ≫
              F.map (δ L X₁ (X₂ ⊗ X₃) ≫ ((Iso.refl (L.obj X₁)).inv ⊗ₘ (μIso L X₂ X₃).inv))
Module: Mathlib.CategoryTheory.Monoidal.Action.End

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
F : C ⥤ (D ⥤ D)ᴹᵒᵖ
inst✝ : F.Monoidal
c₁ c₁' c₂ c₂' : C
c₃ c₃' : D
f : c₁ ⟶ c₁'
g : c₂ ⟶ c₂'
h : c₃ ⟶ c₃'
e :
  (Functor.OplaxMonoidal.δ F c₁ c₂ ≫ (F.map f ⊗ₘ F.map g)).unmop.app c₃ =
    (F.map (f ⊗ₘ g) ≫ Functor.OplaxMonoidal.δ F c₁' c₂').unmop.app c₃
⊢ ((fun {c c'} f d ↦ (F.map f).unmop.app d) (f ⊗ₘ g) c₃ ≫
        (fun c x x_1 f ↦ (F.obj c).unmop.map f) (c₁' ⊗ c₂') c₃ c₃' h) ≫
      ((Functor.Monoidal.μIso F c₁' c₂').unmop.app c₃').symm.hom =
    ((Functor.Monoidal.μIso F c₁ c₂).unmop.app c₃).symm.hom ≫
      (fun {c c'} f d ↦ (F.map f).unmop.app d) f ((F.obj c₂).unmop.obj c₃) ≫
        (fun c x x_1 f ↦ (F.obj c).unmop.map f) c₁' ((F.obj c₂).unmop.obj c₃) ((F.obj c₂').unmop.obj c₃')
          ((fun {c c'} f d ↦ (F.map f).unmop.app d) g c₃ ≫ (fun c x x_1 f ↦ (F.obj c).unmop.map f) c₂' c₃ c₃' h)

Tactic:
dsimp at e

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
F : C ⥤ (D ⥤ D)ᴹᵒᵖ
inst✝ : F.Monoidal
c₁ c₁' c₂ c₂' : C
c₃ c₃' : D
f : c₁ ⟶ c₁'
g : c₂ ⟶ c₂'
h : c₃ ⟶ c₃'
e :
  (Functor.OplaxMonoidal.δ F c₁ c₂).unmop.app c₃ ≫
      (F.map f).unmop.app ((F.obj c₂).unmop.obj c₃) ≫ (F.obj c₁').unmop.map ((F.map g).unmop.app c₃) =
    (F.map (f ⊗ₘ g)).unmop.app c₃ ≫ (Functor.OplaxMonoidal.δ F c₁' c₂').unmop.app c₃
⊢ ((fun {c c'} f d ↦ (F.map f).unmop.app d) (f ⊗ₘ g) c₃ ≫
        (fun c x x_1 f ↦ (F.obj c).unmop.map f) (c₁' ⊗ c₂') c₃ c₃' h) ≫
      ((Functor.Monoidal.μIso F c₁' c₂').unmop.app c₃').symm.hom =
    ((Functor.Monoidal.μIso F c₁ c₂).unmop.app c₃).symm.hom ≫
      (fun {c c'} f d ↦ (F.map f).unmop.app d) f ((F.obj c₂).unmop.obj c₃) ≫
        (fun c x x_1 f ↦ (F.obj c).unmop.map f) c₁' ((F.obj c₂).unmop.obj c₃) ((F.obj c₂').unmop.obj c₃')
          ((fun {c c'} f d ↦ (F.map f).unmop.app d) g c₃ ≫ (fun c x x_1 f ↦ (F.obj c).unmop.map f) c₂' c₃ c₃' h)
Module: Mathlib.CategoryTheory.Monoidal.Action.End

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
F : C ⥤ (D ⥤ D)ᴹᵒᵖ
inst✝ : F.Monoidal
c x y : C
f : x ⟶ y
d : D
e :
  (F.obj c ◁ F.map f ≫ Functor.LaxMonoidal.μ F c y).unmop.app d =
    (Functor.LaxMonoidal.μ F c x ≫ F.map (c ◁ f)).unmop.app d
⊢ (F.map (c ◁ f)).unmop.app d =
    ((Functor.Monoidal.μIso F c x).unmop.app d).symm.hom ≫
      (F.obj c).unmop.map ((F.map f).unmop.app d) ≫ ((Functor.Monoidal.μIso F c y).unmop.app d).symm.inv

Tactic:
dsimp at e

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
F : C ⥤ (D ⥤ D)ᴹᵒᵖ
inst✝ : F.Monoidal
c x y : C
f : x ⟶ y
d : D
e :
  (F.obj c).unmop.map ((F.map f).unmop.app d) ≫ (Functor.LaxMonoidal.μ F c y).unmop.app d =
    (Functor.LaxMonoidal.μ F c x).unmop.app d ≫ (F.map (c ◁ f)).unmop.app d
⊢ (F.map (c ◁ f)).unmop.app d =
    ((Functor.Monoidal.μIso F c x).unmop.app d).symm.hom ≫
      (F.obj c).unmop.map ((F.map f).unmop.app d) ≫ ((Functor.Monoidal.μIso F c y).unmop.app d).symm.inv
Module: Mathlib.CategoryTheory.Monoidal.Action.End

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
F : C ⥤ (D ⥤ D)ᴹᵒᵖ
inst✝ : F.Monoidal
x y c : C
f : x ⟶ y
d : D
e :
  (F.map f ▷ F.obj c ≫ Functor.LaxMonoidal.μ F y c).unmop.app d =
    (Functor.LaxMonoidal.μ F x c ≫ F.map (f ▷ c)).unmop.app d
⊢ (F.map (f ▷ c)).unmop.app d =
    ((Functor.Monoidal.μIso F x c).unmop.app d).symm.hom ≫
      (F.map f).unmop.app ((F.obj c).unmop.obj d) ≫ ((Functor.Monoidal.μIso F y c).unmop.app d).symm.inv

Tactic:
dsimp at e

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
F : C ⥤ (D ⥤ D)ᴹᵒᵖ
inst✝ : F.Monoidal
x y c : C
f : x ⟶ y
d : D
e :
  (F.map f).unmop.app ((F.obj c).unmop.obj d) ≫ (Functor.LaxMonoidal.μ F y c).unmop.app d =
    (Functor.LaxMonoidal.μ F x c).unmop.app d ≫ (F.map (f ▷ c)).unmop.app d
⊢ (F.map (f ▷ c)).unmop.app d =
    ((Functor.Monoidal.μIso F x c).unmop.app d).symm.hom ≫
      (F.map f).unmop.app ((F.obj c).unmop.obj d) ≫ ((Functor.Monoidal.μIso F y c).unmop.app d).symm.inv
Module: Mathlib.CategoryTheory.Monoidal.Action.End

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
F : C ⥤ (D ⥤ D)ᴹᵒᵖ
inst✝ : F.Monoidal
c₁ c₂ c₃ : C
d : D
e :
  (Functor.OplaxMonoidal.δ F (c₁ ⊗ c₂) c₃ ≫
            Functor.OplaxMonoidal.δ F c₁ c₂ ▷ F.obj c₃ ≫ (α_ (F.obj c₁) (F.obj c₂) (F.obj c₃)).hom).unmop.app
      d =
    (F.map (α_ c₁ c₂ c₃).hom ≫
            Functor.OplaxMonoidal.δ F c₁ (c₂ ⊗ c₃) ≫ F.obj c₁ ◁ Functor.OplaxMonoidal.δ F c₂ c₃).unmop.app
      d
⊢ (F.map (α_ c₁ c₂ c₃).hom).unmop.app d ≫
      ((Functor.Monoidal.μIso F c₁ (c₂ ⊗ c₃)).unmop.app d).symm.hom ≫
        (F.obj c₁).unmop.map ((Functor.Monoidal.μIso F c₂ c₃).unmop.app d).symm.hom =
    ((Functor.Monoidal.μIso F (c₁ ⊗ c₂) c₃).unmop.app d).symm.hom ≫
      ((Functor.Monoidal.μIso F c₁ c₂).unmop.app ((F.obj c₃).unmop.obj d)).symm.hom

Tactic:
dsimp at e

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
F : C ⥤ (D ⥤ D)ᴹᵒᵖ
inst✝ : F.Monoidal
c₁ c₂ c₃ : C
d : D
e :
  (Functor.OplaxMonoidal.δ F (c₁ ⊗ c₂) c₃).unmop.app d ≫
      (Functor.OplaxMonoidal.δ F c₁ c₂).unmop.app ((F.obj c₃).unmop.obj d) ≫
        𝟙 ((F.obj c₁).unmop.obj ((F.obj c₂).unmop.obj ((F.obj c₃).unmop.obj d))) =
    (F.map (α_ c₁ c₂ c₃).hom).unmop.app d ≫
      (Functor.OplaxMonoidal.δ F c₁ (c₂ ⊗ c₃)).unmop.app d ≫
        (F.obj c₁).unmop.map ((Functor.OplaxMonoidal.δ F c₂ c₃).unmop.app d)
⊢ (F.map (α_ c₁ c₂ c₃).hom).unmop.app d ≫
      ((Functor.Monoidal.μIso F c₁ (c₂ ⊗ c₃)).unmop.app d).symm.hom ≫
        (F.obj c₁).unmop.map ((Functor.Monoidal.μIso F c₂ c₃).unmop.app d).symm.hom =
    ((Functor.Monoidal.μIso F (c₁ ⊗ c₂) c₃).unmop.app d).symm.hom ≫
      ((Functor.Monoidal.μIso F c₁ c₂).unmop.app ((F.obj c₃).unmop.obj d)).symm.hom
Module: Mathlib.CategoryTheory.Monoidal.Action.End

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
F : C ⥤ (D ⥤ D)ᴹᵒᵖ
inst✝ : F.Monoidal
c : C
d : D
⊢ (F.map (λ_ c).hom).unmop.app d =
    ((Functor.Monoidal.μIso F (𝟙_ C) c).unmop.app d).symm.hom ≫
      ((Functor.Monoidal.εIso F).unmop.app ((F.obj c).unmop.obj d)).symm.hom

Tactic:
have e := (F.map (λ_ c).hom).unmop.app d ≫=
      (congrArg (fun t ↦ t.unmop.app d) <|
        Functor.OplaxMonoidal.left_unitality F c)

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
F : C ⥤ (D ⥤ D)ᴹᵒᵖ
inst✝ : F.Monoidal
c : C
d : D
e :
  (F.map (λ_ c).hom).unmop.app d ≫ (λ_ (F.obj c)).inv.unmop.app d =
    (F.map (λ_ c).hom).unmop.app d ≫
      (F.map (λ_ c).inv ≫ Functor.OplaxMonoidal.δ F (𝟙_ C) c ≫ Functor.OplaxMonoidal.η F ▷ F.obj c).unmop.app d
⊢ (F.map (λ_ c).hom).unmop.app d =
    ((Functor.Monoidal.μIso F (𝟙_ C) c).unmop.app d).symm.hom ≫
      ((Functor.Monoidal.εIso F).unmop.app ((F.obj c).unmop.obj d)).symm.hom
Module: Mathlib.CategoryTheory.Monoidal.Action.End

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
F : C ⥤ (D ⥤ D)ᴹᵒᵖ
inst✝ : F.Monoidal
c : C
d : D
e :
  (F.map (λ_ c).hom).unmop.app d ≫ (λ_ (F.obj c)).inv.unmop.app d =
    (F.map (λ_ c).hom).unmop.app d ≫
      (F.map (λ_ c).inv ≫ Functor.OplaxMonoidal.δ F (𝟙_ C) c ≫ Functor.OplaxMonoidal.η F ▷ F.obj c).unmop.app d
⊢ (F.map (λ_ c).hom).unmop.app d =
    ((Functor.Monoidal.μIso F (𝟙_ C) c).unmop.app d).symm.hom ≫
      ((Functor.Monoidal.εIso F).unmop.app ((F.obj c).unmop.obj d)).symm.hom

Tactic:
dsimp at e

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
F : C ⥤ (D ⥤ D)ᴹᵒᵖ
inst✝ : F.Monoidal
c : C
d : D
e :
  (F.map (λ_ c).hom).unmop.app d ≫ 𝟙 ((F.obj c).unmop.obj d) =
    (F.map (λ_ c).hom).unmop.app d ≫
      (F.map (λ_ c).inv).unmop.app d ≫
        (Functor.OplaxMonoidal.δ F (𝟙_ C) c).unmop.app d ≫ (Functor.OplaxMonoidal.η F).unmop.app ((F.obj c).unmop.obj d)
⊢ (F.map (λ_ c).hom).unmop.app d =
    ((Functor.Monoidal.μIso F (𝟙_ C) c).unmop.app d).symm.hom ≫
      ((Functor.Monoidal.εIso F).unmop.app ((F.obj c).unmop.obj d)).symm.hom
Module: Mathlib.CategoryTheory.Monoidal.Action.End

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
F : C ⥤ (D ⥤ D)ᴹᵒᵖ
inst✝ : F.Monoidal
c : C
d : D
e :
  (F.map (ρ_ c).hom).unmop.app d ≫ (ρ_ (F.obj c)).inv.unmop.app d =
    (F.map (ρ_ c).hom).unmop.app d ≫
      (F.map (ρ_ c).inv ≫ Functor.OplaxMonoidal.δ F c (𝟙_ C) ≫ F.obj c ◁ Functor.OplaxMonoidal.η F).unmop.app d
⊢ (F.map (ρ_ c).hom).unmop.app d =
    ((Functor.Monoidal.μIso F c (𝟙_ C)).unmop.app d).symm.hom ≫
      (F.obj c).unmop.map ((Functor.Monoidal.εIso F).unmop.app d).symm.hom

Tactic:
dsimp at e

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
F : C ⥤ (D ⥤ D)ᴹᵒᵖ
inst✝ : F.Monoidal
c : C
d : D
e :
  (F.map (ρ_ c).hom).unmop.app d ≫ 𝟙 ((F.obj c).unmop.obj d) =
    (F.map (ρ_ c).hom).unmop.app d ≫
      (F.map (ρ_ c).inv).unmop.app d ≫
        (Functor.OplaxMonoidal.δ F c (𝟙_ C)).unmop.app d ≫ (F.obj c).unmop.map ((Functor.OplaxMonoidal.η F).unmop.app d)
⊢ (F.map (ρ_ c).hom).unmop.app d =
    ((Functor.Monoidal.μIso F c (𝟙_ C)).unmop.app d).symm.hom ≫
      (F.obj c).unmop.map ((Functor.Monoidal.εIso F).unmop.app d).symm.hom
Module: Mathlib.CategoryTheory.Monoidal.Action.End

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
F : C ⥤ D ⥤ D
inst✝ : F.Monoidal
c₁ c₁' : D
c₂ c₂' c₃ c₃' : C
f : c₁ ⟶ c₁'
g : c₂ ⟶ c₂'
h : c₃ ⟶ c₃'
e :
  (Functor.OplaxMonoidal.δ F c₂ c₃ ≫ (F.map g ⊗ₘ F.map h)).app c₁ =
    (F.map (g ⊗ₘ h) ≫ Functor.OplaxMonoidal.δ F c₂' c₃').app c₁
⊢ ((fun {d d'} f c ↦ (F.obj c).map f) f (c₂ ⊗ c₃) ≫
        (fun d x x_1 f ↦ (F.map f).app d) c₁' (c₂ ⊗ c₃) (c₂' ⊗ c₃') (g ⊗ₘ h)) ≫
      ((Functor.Monoidal.μIso F c₂' c₃').app c₁').symm.hom =
    ((Functor.Monoidal.μIso F c₂ c₃).app c₁).symm.hom ≫
      (fun {d d'} f c ↦ (F.obj c).map f)
          ((fun {d d'} f c ↦ (F.obj c).map f) f c₂ ≫ (fun d x x_1 f ↦ (F.map f).app d) c₁' c₂ c₂' g) c₃ ≫
        (fun d x x_1 f ↦ (F.map f).app d) ((F.obj c₂').obj c₁') c₃ c₃' h

Tactic:
dsimp at e

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
F : C ⥤ D ⥤ D
inst✝ : F.Monoidal
c₁ c₁' : D
c₂ c₂' c₃ c₃' : C
f : c₁ ⟶ c₁'
g : c₂ ⟶ c₂'
h : c₃ ⟶ c₃'
e :
  (Functor.OplaxMonoidal.δ F c₂ c₃).app c₁ ≫ (F.map h).app ((F.obj c₂).obj c₁) ≫ (F.obj c₃').map ((F.map g).app c₁) =
    (F.map (g ⊗ₘ h)).app c₁ ≫ (Functor.OplaxMonoidal.δ F c₂' c₃').app c₁
⊢ ((fun {d d'} f c ↦ (F.obj c).map f) f (c₂ ⊗ c₃) ≫
        (fun d x x_1 f ↦ (F.map f).app d) c₁' (c₂ ⊗ c₃) (c₂' ⊗ c₃') (g ⊗ₘ h)) ≫
      ((Functor.Monoidal.μIso F c₂' c₃').app c₁').symm.hom =
    ((Functor.Monoidal.μIso F c₂ c₃).app c₁).symm.hom ≫
      (fun {d d'} f c ↦ (F.obj c).map f)
          ((fun {d d'} f c ↦ (F.obj c).map f) f c₂ ≫ (fun d x x_1 f ↦ (F.map f).app d) c₁' c₂ c₂' g) c₃ ≫
        (fun d x x_1 f ↦ (F.map f).app d) ((F.obj c₂').obj c₁') c₃ c₃' h
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A B : Mon C
M : Bimod A B
X Y : Mon C
P Q : Bimod X Y
f : P.X ≅ Q.X
f_left_act_hom : P.actLeft ≫ f.hom = X.X ◁ f.hom ≫ Q.actLeft
f_right_act_hom : P.actRight ≫ f.hom = f.hom ▷ Y.X ≫ Q.actRight
⊢ Q.actRight = (f.inv ▷ Y.X ≫ f.hom ▷ Y.X) ≫ Q.actRight

Tactic:
← comp_whiskerRight,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A B : Mon C
M : Bimod A B
X Y : Mon C
P Q : Bimod X Y
f : P.X ≅ Q.X
f_left_act_hom : P.actLeft ≫ f.hom = X.X ◁ f.hom ≫ Q.actLeft
f_right_act_hom : P.actRight ≫ f.hom = f.hom ▷ Y.X ≫ Q.actRight
⊢ Q.actRight = (f.inv ≫ f.hom) ▷ Y.X ≫ Q.actRight