mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.FiberedCategory.Cocartesian

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝¹ : p.IsStronglyCocartesian f φ
S' : 𝒮
b' : 𝒳
g : S ⟶ S'
f' : R ⟶ S'
hf' : f' = f ≫ g
φ' : a ⟶ b'
inst✝ : p.IsHomLift f' φ'
⊢ ∃! χ, p.IsHomLift g χ ∧ φ ≫ χ = φ'

Tactic:
subst_hom_lift p f' φ'

Goal state after:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
S✝ : 𝒮
a✝ b✝ : 𝒳
φ : a✝ ⟶ b✝
b' : 𝒳
φ' : a✝ ⟶ b'
R S : 𝒮
a b : 𝒳
f : p.obj a✝ ⟶ S✝
inst✝¹ : p.IsStronglyCocartesian f φ
g : S✝ ⟶ p.obj b'
hf' : p.map φ' = f ≫ g
inst✝ : p.IsHomLift (p.map φ') φ'
⊢ ∃! χ, p.IsHomLift g χ ∧ φ ≫ χ = φ'
Module: Mathlib.CategoryTheory.FiberedCategory.Cocartesian

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝⁴ : Category.{v₁, u₁} 𝒮
inst✝³ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝² : p.IsStronglyCocartesian f φ
S' : 𝒮
b' : 𝒳
g : S ⟶ S'
ψ ψ' : b ⟶ b'
inst✝¹ : p.IsHomLift g ψ
inst✝ : p.IsHomLift g ψ'
h : φ ≫ ψ = φ ≫ ψ'
⊢ map p f φ ⋯ (φ ≫ ψ) = ψ'

Tactic:
map_uniq p f φ (g := g) rfl (φ ≫ ψ) ψ' h.symm

Goal state after:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝⁴ : Category.{v₁, u₁} 𝒮
inst✝³ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝² : p.IsStronglyCocartesian f φ
S' : 𝒮
b' : 𝒳
g : S ⟶ S'
ψ ψ' : b ⟶ b'
inst✝¹ : p.IsHomLift g ψ
inst✝ : p.IsHomLift g ψ'
h : φ ≫ ψ = φ ≫ ψ'
⊢ map p f φ ⋯ (φ ≫ ψ) = map p f φ ⋯ (φ ≫ ψ)
Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived

Goal state before:
pp: C : Type u₁
D : Type u₂
H : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} H
F' : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : L ⋙ F' ⟶ F
W : MorphismProperty C
G : D ⥤ H
e : F ≅ L ⋙ G
inst✝ : L.IsLocalization W
Y : C
s : Cone (StructuredArrow.proj (L.obj Y) L ⋙ F)
m : s.pt ⟶ ((RightExtension.mk G e.inv).coneAt (L.obj Y)).pt
hm : ∀ (j : StructuredArrow (L.obj Y) L), m ≫ ((RightExtension.mk G e.inv).coneAt (L.obj Y)).π.app j = s.π.app j
this :
  m ≫ ((RightExtension.mk G e.inv).coneAt (L.obj Y)).π.app (StructuredArrow.mk (𝟙 (L.obj Y))) =
    s.π.app (StructuredArrow.mk (𝟙 (L.obj Y)))
⊢ m = s.π.app (StructuredArrow.mk (𝟙 (L.obj Y))) ≫ e.hom.app Y

Tactic:
dsimp at this m hm ⊢

Goal state after:
C : Type u₁
D : Type u₂
H : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} H
F' : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : L ⋙ F' ⟶ F
W : MorphismProperty C
G : D ⥤ H
e : F ≅ L ⋙ G
inst✝ : L.IsLocalization W
Y : C
s : Cone (StructuredArrow.proj (L.obj Y) L ⋙ F)
m : s.pt ⟶ G.obj (L.obj Y)
hm : ∀ (j : StructuredArrow (L.obj Y) L), m ≫ G.map j.hom ≫ e.inv.app j.right = s.π.app j
this : m ≫ G.map (𝟙 (L.obj Y)) ≫ e.inv.app Y = s.π.app (StructuredArrow.mk (𝟙 (L.obj Y)))
⊢ m = s.π.app (StructuredArrow.mk (𝟙 (L.obj Y))) ≫ e.hom.app Y
Module: Mathlib.CategoryTheory.Galois.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝² : PreGaloisCategory C
inst✝¹ : FiberFunctor F
X A : C
inst✝ : IsConnected A
h : Nonempty (F.obj X).obj
f : X ⟶ A
Z : C
u v : A ⟶ Z
huv : f ≫ u = f ≫ v
⊢ u = v

Tactic:
by
  apply evaluation_injective_of_isConnected F A Z (F.map f (Classical.arbitrary _))
  simpa using ConcreteCategory.congr_hom (F.congr_map huv) _

Goal state after:
Module: Mathlib.CategoryTheory.Galois.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝³ : PreGaloisCategory C
inst✝² : FiberFunctor F
X A : C
inst✝¹ : Nonempty (F.obj X).obj
inst✝ : IsConnected A
f : X ⟶ A
⊢ Function.Surjective ⇑(ConcreteCategory.hom (F.map f))

Tactic:
by
  have : Epi f := epi_of_nonempty_of_isConnected F f
  exact surjective_on_fiber_of_epi F f

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{u₂, u₁} C
ι₁ : Type u_1
ι₂ : Type u_2
X : C
f₁ : ι₁ → C
f₂ : ι₂ → C
c₁ : Cofan f₁
c₂ : Cofan f₂
bc : BinaryCofan c₁.pt c₂.pt
h₁ : IsColimit c₁
h₂ : IsColimit c₂
h : IsColimit bc
s : Cofan (Sum.elim f₁ f₂)
w : ι₁ ⊕ ι₂
⊢ ((mk bc.pt (c₁.combPairHoms c₂ bc)).inj w ≫
      IsColimit.desc h fun i ↦
        WalkingPair.casesOn (motive := fun t ↦ i = t → (WalkingPair.casesOn i c₁.pt c₂.pt ⟶ s.pt)) i
          (fun h ↦ ⋯ ▸ IsColimit.desc h₁ fun a ↦ s.inj (Sum.inl a))
          (fun h ↦ ⋯ ▸ IsColimit.desc h₂ fun a ↦ s.inj (Sum.inr a)) ⋯) =
    s.inj w

Tactic:
by
      cases w <;>
      · simp only [cofan_mk_inj, combPairHoms, Category.assoc]
        erw [h.fac]
        simp only [Cofan.mk_ι_app, Cofan.IsColimit.fac]

Goal state after:
Module: Mathlib.CategoryTheory.Galois.Decomposition

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X A : C
u : A ⟶ selfProd F X
a : (F.obj A).obj
h : (ConcreteCategory.hom (F.map u)) a = mkSelfProdFib F X
inst✝ : IsConnected A
b : (F.obj A).obj
⊢ (F.obj X).obj ≃ (F.obj X).obj

Tactic:
let σ (t : F.obj X) : F.obj X := F.map (selfProdProj u t) b

Goal state after:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X A : C
u : A ⟶ selfProd F X
a : (F.obj A).obj
h : (ConcreteCategory.hom (F.map u)) a = mkSelfProdFib F X
inst✝ : IsConnected A
b : (F.obj A).obj
σ : (F.obj X).obj → (F.obj X).obj := fun t ↦ (ConcreteCategory.hom (F.map (selfProdProj u t))) b
⊢ (F.obj X).obj ≃ (F.obj X).obj
Module: Mathlib.CategoryTheory.Galois.Prorepresentability

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X : C
inst✝ : IsConnected X
A : C
f : A ⟶ X
hgal : IsGalois A
hs : Function.Surjective ⇑(ConcreteCategory.hom (F.map f))
x y : (F.obj X).obj
a : (F.obj A).obj
ha : (ConcreteCategory.hom (F.map f)) a = x
b : (F.obj A).obj
hb : (ConcreteCategory.hom (F.map f)) b = y
this : MulAction.IsPretransitive (Aut F) (F.obj A).obj
⊢ ∃ g, g • x = y

Tactic:
obtain ⟨σ, (hσ : σ.hom.app A a = b)⟩ := MulAction.exists_smul_eq (Aut F) a b

Goal state after:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X : C
inst✝ : IsConnected X
A : C
f : A ⟶ X
hgal : IsGalois A
hs : Function.Surjective ⇑(ConcreteCategory.hom (F.map f))
x y : (F.obj X).obj
a : (F.obj A).obj
ha : (ConcreteCategory.hom (F.map f)) a = x
b : (F.obj A).obj
hb : (ConcreteCategory.hom (F.map f)) b = y
this : MulAction.IsPretransitive (Aut F) (F.obj A).obj
σ : Aut F
hσ : (ConcreteCategory.hom (σ.hom.app A)) a = b
⊢ ∃ g, g • x = y
Module: Mathlib.CategoryTheory.Galois.IsFundamentalgroup

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝⁶ : Group G
inst✝⁵ : (X : C) → MulAction G (F.obj X).obj
inst✝⁴ : IsNaturalSMul F G
inst✝³ : GaloisCategory C
inst✝² : FiberFunctor F
t : Aut F
X : C
inst✝¹ : IsGalois X
inst✝ : MulAction.IsPretransitive G (F.obj X).obj
a : (F.obj X).obj
g : G
hg : g • a = (ConcreteCategory.hom (t.hom.app X)) a
⊢ ∃ g, ∀ (x : (F.obj X).obj), g • x = (ConcreteCategory.hom (t.hom.app X)) x

Tactic:
exact ⟨g, action_ext_of_isGalois F _ hg⟩

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid

Goal state before:
pp: case nil
V : Type u
inst✝ : Quiver V
X Y : Paths (Symmetrify V)
⊢ EqvGen (HomRel.CompClosure redStep) (Path.nil ≫ Path.nil.reverse) (𝟙 X)

Tactic:
| nil =>

Goal state after:
Module: Mathlib.CategoryTheory.Galois.IsFundamentalgroup

Goal state before:
pp: C : Type u₁
inst✝⁸ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝⁷ : GaloisCategory C
G : Type u_1
inst✝⁶ : Group G
inst✝⁵ : (X : C) → MulAction G (F.obj X).obj
inst✝⁴ : FiberFunctor F
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : CompactSpace G
inst✝ : IsFundamentalGroup F G
⊢ IsHomeomorph ⇑(toAut F G)

Tactic:
by
  rw [isHomeomorph_iff_continuous_bijective]
  exact ⟨toAut_continuous F G, toAut_bijective F G⟩

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: case mpr
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c d : C
f : c ⟶ d
⊢ f ∈ S.arrows c d → Groupoid.inv f ∈ S.arrows d c

Tactic:
apply S.inv

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
c d : C
⊢ ∃ (h : c = c), 𝟙 c = eqToHom h

Tactic:
exact ⟨rfl, rfl⟩

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: case refl
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
Sw : S.IsWide
c : C
⊢ eqToHom ⋯ ∈ S.arrows c c

Tactic:
simp only [eqToHom_refl]

Goal state after:
case refl
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
Sw : S.IsWide
c : C
⊢ 𝟙 c ∈ S.arrows c c
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝¹ : Groupoid C
S✝ : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
S : Subgroupoid C
c d : D
c✝ d✝ : C
f✝ : c✝ ⟶ d✝
hf✝ : f✝ ∈ S.arrows c✝ d✝
⊢ Groupoid.inv f✝ ∈ S.arrows d✝ c✝

Tactic:
apply S.inv

Goal state after:
C : Type u
inst✝¹ : Groupoid C
S✝ : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
S : Subgroupoid C
c d : D
c✝ d✝ : C
f✝ : c✝ ⟶ d✝
hf✝ : f✝ ∈ S.arrows c✝ d✝
⊢ f✝ ∈ S.arrows c✝ d✝
Module: Mathlib.CategoryTheory.Idempotents.Biproducts

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : Preadditive C
P : Karoubi C
⊢ biprod.desc P.decompId_i P.complement.decompId_i ≫ biprod.lift P.decompId_p P.complement.decompId_p =
    𝟙 (P ⊞ P.complement)

Tactic:
by
    apply biprod.hom_ext'
    · rw [biprod.inl_desc_assoc, comp_id, biprod.lift_eq, comp_add, ← decompId_assoc,
        add_eq_left, ← assoc]
      refine (?_ =≫ _).trans zero_comp
      ext
      simp only [comp_f, toKaroubi_obj_X, decompId_i_f, decompId_p_f,
        complement_p, comp_sub, comp_id, idem, sub_self, zero_def]
    · rw [biprod.inr_desc_assoc, comp_id, biprod.lift_eq, comp_add, ← decompId_assoc,
        add_eq_right, ← assoc]
      refine (?_ =≫ _).trans zero_comp
      ext
      simp only [complement_X, comp_f, decompId_i_f, complement_p,
        decompId_p_f, sub_comp, id_comp, idem, sub_self, zero_def]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: 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
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₁
X : Type u₇
inst✝ : Category.{v₇, u₇} X
ψ ψ' : CatCospanTransform F G F₁ G₁
η : ψ ⟶ ψ'
S : CatCommSqOver F G X
⊢ whiskerRight { app := fun y ↦ η.left.app (S.fst.obj y), naturality := ⋯ } F₁ ≫
      ({
                obj := fun S ↦
                  { fst := S.fst ⋙ ψ'.left, snd := S.snd ⋙ ψ'.right,
                    iso :=
                      S.fst.associator ψ'.left F₁ ≪≫
                        S.fst.isoWhiskerLeft (CatCommSq.iso F ψ'.left ψ'.base F₁).symm ≪≫
                          (S.fst.associator F ψ'.base).symm ≪≫
                            isoWhiskerRight S.iso ψ'.base ≪≫
                              S.snd.associator G ψ'.base ≪≫
                                S.snd.isoWhiskerLeft (CatCommSq.iso G ψ'.right ψ'.base G₁) ≪≫
                                  (S.snd.associator ψ'.right G₁).symm },
                map := fun {x y} f ↦ { fst := whiskerRight f.fst ψ'.left, snd := whiskerRight f.snd ψ'.right, w := ⋯ },
                map_id := ⋯, map_comp := ⋯ }.obj
            S).iso.hom =
    ({
                obj := fun S ↦
                  { fst := S.fst ⋙ ψ.left, snd := S.snd ⋙ ψ.right,
                    iso :=
                      S.fst.associator ψ.left F₁ ≪≫
                        S.fst.isoWhiskerLeft (CatCommSq.iso F ψ.left ψ.base F₁).symm ≪≫
                          (S.fst.associator F ψ.base).symm ≪≫
                            isoWhiskerRight S.iso ψ.base ≪≫
                              S.snd.associator G ψ.base ≪≫
                                S.snd.isoWhiskerLeft (CatCommSq.iso G ψ.right ψ.base G₁) ≪≫
                                  (S.snd.associator ψ.right G₁).symm },
                map := fun {x y} f ↦ { fst := whiskerRight f.fst ψ.left, snd := whiskerRight f.snd ψ.right, w := ⋯ },
                map_id := ⋯, map_comp := ⋯ }.obj
            S).iso.hom ≫
      whiskerRight { app := fun y ↦ η.right.app (S.snd.obj y), naturality := ⋯ } G₁

Tactic:
ext t
          have := ψ.squareLeft.iso.inv.app (S.fst.obj t) ≫=
            η.left_coherence_app (S.fst.obj t)
          simp only [Iso.inv_hom_id_app_assoc] at this
          simp [this]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: 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
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₁
X : Type u₇
inst✝ : Category.{v₇, u₇} X
ψ ψ' : CatCospanTransform F G F₁ G₁
η : ψ ⟶ ψ'
S : CatCommSqOver F G X
⊢ whiskerRight { app := fun y ↦ η.left.app (S.fst.obj y), naturality := ⋯ } F₁ ≫
      ({
                obj := fun S ↦
                  { fst := S.fst ⋙ ψ'.left, snd := S.snd ⋙ ψ'.right,
                    iso :=
                      S.fst.associator ψ'.left F₁ ≪≫
                        S.fst.isoWhiskerLeft (CatCommSq.iso F ψ'.left ψ'.base F₁).symm ≪≫
                          (S.fst.associator F ψ'.base).symm ≪≫
                            isoWhiskerRight S.iso ψ'.base ≪≫
                              S.snd.associator G ψ'.base ≪≫
                                S.snd.isoWhiskerLeft (CatCommSq.iso G ψ'.right ψ'.base G₁) ≪≫
                                  (S.snd.associator ψ'.right G₁).symm },
                map := fun {x y} f ↦ { fst := whiskerRight f.fst ψ'.left, snd := whiskerRight f.snd ψ'.right, w := ⋯ },
                map_id := ⋯, map_comp := ⋯ }.obj
            S).iso.hom =
    ({
                obj := fun S ↦
                  { fst := S.fst ⋙ ψ.left, snd := S.snd ⋙ ψ.right,
                    iso :=
                      S.fst.associator ψ.left F₁ ≪≫
                        S.fst.isoWhiskerLeft (CatCommSq.iso F ψ.left ψ.base F₁).symm ≪≫
                          (S.fst.associator F ψ.base).symm ≪≫
                            isoWhiskerRight S.iso ψ.base ≪≫
                              S.snd.associator G ψ.base ≪≫
                                S.snd.isoWhiskerLeft (CatCommSq.iso G ψ.right ψ.base G₁) ≪≫
                                  (S.snd.associator ψ.right G₁).symm },
                map := fun {x y} f ↦ { fst := whiskerRight f.fst ψ.left, snd := whiskerRight f.snd ψ.right, w := ⋯ },
                map_id := ⋯, map_comp := ⋯ }.obj
            S).iso.hom ≫
      whiskerRight { app := fun y ↦ η.right.app (S.snd.obj y), naturality := ⋯ } G₁

Tactic:
by
          ext t
          have := ψ.squareLeft.iso.inv.app (S.fst.obj t) ≫=
            η.left_coherence_app (S.fst.obj t)
          simp only [Iso.inv_hom_id_app_assoc] at this
          simp [this]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Limits.HasLimits

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
F : J ⥤ C
inst✝ : HasColimit F
c : Cocone F
j : J
Q : C
⊢ colimit.ι F j ▷ Q ≫ colimit.desc F c ▷ Q = c.ι.app j ▷ Q

Tactic:
by
  simp [← comp_whiskerRight]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Action.Opposites

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
inst✝ : MonoidalLeftAction Cᵒᵖ Dᵒᵖ
c₁✝ c₂✝ c₃✝ c₄✝ : C
d₁✝ d₂✝ : D
f : c₁✝ ⟶ c₂✝
g : c₃✝ ⟶ c₄✝
h : d₁✝ ⟶ d₂✝
⊢ (((f ⊗ₘ g).op ⊙ₗₘ h.op).unop ≫ (αₗ (op c₂✝) (op c₄✝) (op d₂✝)).symm.unop.hom).op =
    ((αₗ (op c₁✝) (op c₃✝) (op d₁✝)).symm.unop.hom ≫ (f.op ⊙ₗₘ (g.op ⊙ₗₘ h.op).unop.op).unop).op

Tactic:
have := (αₗ (op _) (op _) (op _)).inv ≫=
      MonoidalLeftAction.actionAssocIso_hom_naturality f.op g.op h.op

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
inst✝ : MonoidalLeftAction Cᵒᵖ Dᵒᵖ
c₁✝ c₂✝ c₃✝ c₄✝ : C
d₁✝ d₂✝ : D
f : c₁✝ ⟶ c₂✝
g : c₃✝ ⟶ c₄✝
h : d₁✝ ⟶ d₂✝
this :
  (αₗ (op c₂✝) (op c₄✝) (op d₂✝)).inv ≫ ((f.op ⊗ₘ g.op) ⊙ₗₘ h.op) ≫ (αₗ (op c₁✝) (op c₃✝) (op d₁✝)).hom =
    (αₗ (op c₂✝) (op c₄✝) (op d₂✝)).inv ≫ (αₗ (op c₂✝) (op c₄✝) (op d₂✝)).hom ≫ (f.op ⊙ₗₘ g.op ⊙ₗₘ h.op)
⊢ (((f ⊗ₘ g).op ⊙ₗₘ h.op).unop ≫ (αₗ (op c₂✝) (op c₄✝) (op d₂✝)).symm.unop.hom).op =
    ((αₗ (op c₁✝) (op c₃✝) (op d₁✝)).symm.unop.hom ≫ (f.op ⊙ₗₘ (g.op ⊙ₗₘ h.op).unop.op).unop).op
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : CartesianMonoidalCategory C
M : Mon C
Y Y' : Cᵒᵖ
g : Y ⟶ Y'
f : unop Y ⟶ M.X
⊢ (ConcreteCategory.hom ((shrinkYonedaMon.{w, v, u}.obj M).map g)) (shrinkYonedaMonObjObjEquiv.symm f) =
    shrinkYonedaMonObjObjEquiv.symm (g.unop ≫ f)

Tactic:
by
  simp [shrinkYonedaMon, shrinkYonedaMonObjObjEquiv]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : CartesianMonoidalCategory C
M M' : Mon C
Y : Cᵒᵖ
f : unop Y ⟶ M.X
g : M ⟶ M'
⊢ (ConcreteCategory.hom ((shrinkYonedaMon.{w, v, u}.map g).app Y)) (shrinkYonedaMonObjObjEquiv.symm f) =
    shrinkYonedaMonObjObjEquiv.symm (f ≫ g.hom)

Tactic:
by
  simp [shrinkYonedaMon, shrinkYonedaMonObjObjEquiv]

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

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
inst✝⁴ : MonoidalCategory D
inst✝³ : SymmetricCategory D
inst✝² : MonoidalClosed D
R : C ⥤ D
inst✝¹ : R.Faithful
inst✝ : R.Full
L : D ⥤ C
adj : L ⊣ R
tfae_3_to_4 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))) → ∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))
tfae_4_to_1 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))) →
    ∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))
h : ∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))
d d' : D
c : C
w₁ :
  ⇑(ConcreteCategory.hom ((coyoneda.map (L.map (adj.unit.app d ▷ d')).op).app c)) =
    ⇑(adj.homEquiv (Opposite.unop (Opposite.op ((𝟭 D).obj d ⊗ d'))) c).symm ∘
      ⇑(ConcreteCategory.hom ((coyoneda.map (adj.unit.app d ▷ d').op).app (R.obj c))) ∘
        ⇑(adj.homEquiv (Opposite.unop (Opposite.op ((L ⋙ R).obj d ⊗ d'))) c)
⊢ IsIso ((coyoneda.map (L.map (adj.unit.app d ▷ d')).op).app c)

Tactic:
isIso_iff_bijective,

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : MonoidalCategory D
inst✝³ : SymmetricCategory D
inst✝² : MonoidalClosed D
R : C ⥤ D
inst✝¹ : R.Faithful
inst✝ : R.Full
L : D ⥤ C
adj : L ⊣ R
tfae_3_to_4 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))) → ∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))
tfae_4_to_1 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))) →
    ∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))
h : ∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))
d d' : D
c : C
w₁ :
  ⇑(ConcreteCategory.hom ((coyoneda.map (L.map (adj.unit.app d ▷ d')).op).app c)) =
    ⇑(adj.homEquiv (Opposite.unop (Opposite.op ((𝟭 D).obj d ⊗ d'))) c).symm ∘
      ⇑(ConcreteCategory.hom ((coyoneda.map (adj.unit.app d ▷ d').op).app (R.obj c))) ∘
        ⇑(adj.homEquiv (Opposite.unop (Opposite.op ((L ⋙ R).obj d ⊗ d'))) c)
⊢ Function.Bijective ⇑(ConcreteCategory.hom ((coyoneda.map (L.map (adj.unit.app d ▷ d')).op).app c))
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
A B : Mon C
M : Bimod A B
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| P.actRight ▷ Q.X ▷ T.X ≫ (α_ P.X Q.X T.X).hom

pp: case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
A B : Mon C
M : Bimod A B
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| P.X ◁ Q.actRight

Tactic:
associator_naturality_left

Goal state after:
case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
A B : Mon C
M : Bimod A B
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| (α_ (P.X ⊗ S.X) Q.X T.X).hom ≫ P.actRight ▷ (Q.X ⊗ T.X)

case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
A B : Mon C
M : Bimod A B
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| P.X ◁ Q.actRight