mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst✝¹² : Semiring R
inst✝¹¹ : (i : ι) → AddCommMonoid (M₁ i)
inst✝¹⁰ : (i : ι) → Module R (M₁ i)
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R M₂
inst✝⁷ : Semiring S
inst✝⁶ : Module S M₂
inst✝⁵ : SMulCommClass R S M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module S M₃
inst✝² : Module R M₃
inst✝¹ : SMulCommClass R S M₃
ι' : Type u_1
σ : ι ≃ ι'
f : MultilinearMap R (fun i ↦ M₁ (σ.symm i)) M₂
inst✝ : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
this : DecidableEq ι' := σ.symm.decidableEq
⊢ ∀ (x y : M₁ i),
    (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ)) (update m i (x + y)) =
      (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ)) (update m i x) + (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ)) (update m i y)

Tactic:
rw [← σ.symm_apply_apply i]

Goal state after:
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst✝¹² : Semiring R
inst✝¹¹ : (i : ι) → AddCommMonoid (M₁ i)
inst✝¹⁰ : (i : ι) → Module R (M₁ i)
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R M₂
inst✝⁷ : Semiring S
inst✝⁶ : Module S M₂
inst✝⁵ : SMulCommClass R S M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module S M₃
inst✝² : Module R M₃
inst✝¹ : SMulCommClass R S M₃
ι' : Type u_1
σ : ι ≃ ι'
f : MultilinearMap R (fun i ↦ M₁ (σ.symm i)) M₂
inst✝ : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
this : DecidableEq ι' := σ.symm.decidableEq
⊢ ∀ (x y : M₁ (σ.symm (σ i))),
    (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ)) (update m (σ.symm (σ i)) (x + y)) =
      (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ)) (update m (σ.symm (σ i)) x) +
        (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ)) (update m (σ.symm (σ i)) y)
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst✝¹² : Semiring R
inst✝¹¹ : (i : ι) → AddCommMonoid (M₁ i)
inst✝¹⁰ : (i : ι) → Module R (M₁ i)
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R M₂
inst✝⁷ : Semiring S
inst✝⁶ : Module S M₂
inst✝⁵ : SMulCommClass R S M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module S M₃
inst✝² : Module R M₃
inst✝¹ : SMulCommClass R S M₃
ι' : Type u_1
σ : ι ≃ ι'
f : MultilinearMap R (fun i ↦ M₁ (σ.symm i)) M₂
inst✝ : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
c : R
this : DecidableEq ι' := σ.symm.decidableEq
⊢ ∀ (x : M₁ i),
    (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ)) (update m i (c • x)) = c • (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ)) (update m i x)

Tactic:
rw [← σ.symm_apply_apply i]

Goal state after:
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst✝¹² : Semiring R
inst✝¹¹ : (i : ι) → AddCommMonoid (M₁ i)
inst✝¹⁰ : (i : ι) → Module R (M₁ i)
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R M₂
inst✝⁷ : Semiring S
inst✝⁶ : Module S M₂
inst✝⁵ : SMulCommClass R S M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module S M₃
inst✝² : Module R M₃
inst✝¹ : SMulCommClass R S M₃
ι' : Type u_1
σ : ι ≃ ι'
f : MultilinearMap R (fun i ↦ M₁ (σ.symm i)) M₂
inst✝ : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
c : R
this : DecidableEq ι' := σ.symm.decidableEq
⊢ ∀ (x : M₁ (σ.symm (σ i))),
    (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ)) (update m (σ.symm (σ i)) (c • x)) =
      c • (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ)) (update m (σ.symm (σ i)) x)
Module: Mathlib.CategoryTheory.Limits.Types.Limits

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : Small.{u, max u v} ↑F.sections
x✝¹ : Cone F
x✝ : x✝¹.pt ⟶ (limitCone F).pt
w : ∀ (j : J), x✝ ≫ (limitCone F).π.app j = x✝¹.π.app j
⊢ x✝ = ↾fun v ↦ (equivShrink ↑F.sections) ⟨fun j ↦ (hom (x✝¹.π.app j)) v, ⋯⟩

Tactic:
ext x j

Goal state after:
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : Small.{u, max u v} ↑F.sections
x✝¹ : Cone F
x✝ : x✝¹.pt ⟶ (limitCone F).pt
w : ∀ (j : J), x✝ ≫ (limitCone F).π.app j = x✝¹.π.app j
x : x✝¹.pt
j : J
⊢ ↑((equivShrink ↑F.sections).symm ((hom x✝).toFun x)) j =
    ↑((equivShrink ↑F.sections).symm
          ((hom (↾fun v ↦ (equivShrink ↑F.sections) ⟨fun j ↦ (hom (x✝¹.π.app j)) v, ⋯⟩)).toFun x))
      j
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁶ : Semiring R
inst✝⁵ : (i : ι) → AddCommGroup (M₁ i)
inst✝⁴ : AddCommGroup M₂
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
x h h' : (i : ι) → M₁ i
⊢ f x + (f.linearDeriv x) h + ∑ s with 2 ≤ #s, f (s.piecewise h x) -
        (f x + (f.linearDeriv x) h' + ∑ s with 2 ≤ #s, f (s.piecewise h' x)) -
      (f.linearDeriv x) (h - h') =
    ∑ s with 2 ≤ #s, (f (s.piecewise h x) - f (s.piecewise h' x))

Tactic:
add_assoc,

Goal state after:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁶ : Semiring R
inst✝⁵ : (i : ι) → AddCommGroup (M₁ i)
inst✝⁴ : AddCommGroup M₂
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
x h h' : (i : ι) → M₁ i
⊢ f x + ((f.linearDeriv x) h + ∑ s with 2 ≤ #s, f (s.piecewise h x)) -
        (f x + ((f.linearDeriv x) h' + ∑ s with 2 ≤ #s, f (s.piecewise h' x))) -
      (f.linearDeriv x) (h - h') =
    ∑ s with 2 ≤ #s, (f (s.piecewise h x) - f (s.piecewise h' x))
Module: Mathlib.CategoryTheory.Limits.Types.Yoneda

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Category.{v_2, u_2} C
F : J ⥤ C
X : C
s : ↑(F.op ⋙ yoneda.obj X).sections
j j' : J
f : j ⟶ j'
⊢ F.map f ≫ ↑s (op j') = ↑s (op j) ≫ ((const J).obj X).map f

Tactic:
dsimp
        rw [Category.comp_id]
        exact (s.property f.op)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Yoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : Category.{t, w} J
F : J ⥤ C
c : Cocone F
x✝ : (X : C) → IsLimit ((yoneda.obj X).mapCone c.op)
⊢ (fun h x ↦ isLimitOfPreserves (yoneda.obj x) h.op) ((fun h ↦ (yonedaJointlyReflectsLimits F.op c.op h).unop) x✝) = x✝

Tactic:
by ext; apply Subsingleton.elim

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Yoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : Category.{t, w} J
F : J ⥤ C
c : Cone F
x✝ : (X : Cᵒᵖ) → IsLimit ((coyoneda.obj X).mapCone c)
⊢ (fun h x ↦ isLimitOfPreserves (coyoneda.obj x) h) ((fun h ↦ coyonedaJointlyReflectsLimits F c h) x✝) = x✝

Tactic:
by ext; apply Subsingleton.elim

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Creates

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
K✝ : J ⥤ C
J' : Type w₁
inst✝¹ : Category.{w'₁, w₁} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : CreatesColimitsOfShape J F
K : J' ⥤ C
c : Cocone (K ⋙ F)
hc : IsColimit c
⊢ F.mapCocone ((Cocone.whiskeringEquivalence e).inverse.obj (liftColimit (hc.whiskerEquivalence e))) ≅ c

Tactic:
letI inner := (Cocone.whiskeringEquivalence (F := K ⋙ F) e).inverse.mapIso
          (liftedColimitMapsToOriginal (K := e.functor ⋙ K) (hc.whiskerEquivalence e))

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
K✝ : J ⥤ C
J' : Type w₁
inst✝¹ : Category.{w'₁, w₁} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : CreatesColimitsOfShape J F
K : J' ⥤ C
c : Cocone (K ⋙ F)
hc : IsColimit c
inner : (Cocone.whiskeringEquivalence e).inverse.obj (F.mapCocone (liftColimit (hc.whiskerEquivalence e))) ≅
  (Cocone.whiskeringEquivalence e).inverse.obj (Cocone.whisker e.functor c) :=
  (Cocone.whiskeringEquivalence e).inverse.mapIso (liftedColimitMapsToOriginal (hc.whiskerEquivalence e))
⊢ F.mapCocone ((Cocone.whiskeringEquivalence e).inverse.obj (liftColimit (hc.whiskerEquivalence e))) ≅ c
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X : C
P : Cᵒᵖ ⥤ Type w
τ : shrinkYoneda.{w, v, u}.obj X ⟶ P
Y : Cᵒᵖ
f : (shrinkYoneda.{w, v, u}.obj X).obj Y
⊢ (ConcreteCategory.hom
          (((fun x ↦
                  {
                    app := fun Y ↦
                      ↾fun f ↦
                        (ConcreteCategory.hom (P.map (Quiver.Hom.op ((equivShrink ((yoneda.obj X).obj Y)).symm f)))) x,
                    naturality := ⋯ })
                ((fun τ ↦ (ConcreteCategory.hom (τ.app (op X))) ((equivShrink ((yoneda.obj X).obj (op X))) (𝟙 X)))
                  τ)).app
            Y)).toFun
      f =
    (ConcreteCategory.hom (τ.app Y)).toFun f

Tactic:
obtain ⟨f, rfl⟩ := (equivShrink _).surjective f

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X : C
P : Cᵒᵖ ⥤ Type w
τ : shrinkYoneda.{w, v, u}.obj X ⟶ P
Y : Cᵒᵖ
f : (yoneda.obj X).obj Y
⊢ (ConcreteCategory.hom
          (((fun x ↦
                  {
                    app := fun Y ↦
                      ↾fun f ↦
                        (ConcreteCategory.hom (P.map (Quiver.Hom.op ((equivShrink ((yoneda.obj X).obj Y)).symm f)))) x,
                    naturality := ⋯ })
                ((fun τ ↦ (ConcreteCategory.hom (τ.app (op X))) ((equivShrink ((yoneda.obj X).obj (op X))) (𝟙 X)))
                  τ)).app
            Y)).toFun
      ((equivShrink ((yoneda.obj X).obj Y)) f) =
    (ConcreteCategory.hom (τ.app Y)).toFun ((equivShrink ((yoneda.obj X).obj Y)) f)
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X : Cᵒᵖ
P : C ⥤ Type w
τ : shrinkCoyoneda.{w, v, u}.obj X ⟶ P
Y : C
f : (shrinkCoyoneda.{w, v, u}.obj X).obj Y
⊢ (ConcreteCategory.hom
          (((fun x ↦
                  { app := fun Y ↦ ↾fun f ↦ (ConcreteCategory.hom (P.map ((equivShrink (unop X ⟶ Y)).symm f))) x,
                    naturality := ⋯ })
                ((fun τ ↦
                    (ConcreteCategory.hom (τ.app (unop X))) ((equivShrink ((yoneda.obj (unop X)).obj X)) (𝟙 (unop X))))
                  τ)).app
            Y)).toFun
      f =
    (ConcreteCategory.hom (τ.app Y)).toFun f

Tactic:
obtain ⟨f, rfl⟩ := (equivShrink _).surjective f

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X : Cᵒᵖ
P : C ⥤ Type w
τ : shrinkCoyoneda.{w, v, u}.obj X ⟶ P
Y : C
f : (yoneda.obj Y).obj X
⊢ (ConcreteCategory.hom
          (((fun x ↦
                  { app := fun Y ↦ ↾fun f ↦ (ConcreteCategory.hom (P.map ((equivShrink (unop X ⟶ Y)).symm f))) x,
                    naturality := ⋯ })
                ((fun τ ↦
                    (ConcreteCategory.hom (τ.app (unop X))) ((equivShrink ((yoneda.obj (unop X)).obj X)) (𝟙 (unop X))))
                  τ)).app
            Y)).toFun
      ((equivShrink ((yoneda.obj Y).obj X)) f) =
    (ConcreteCategory.hom (τ.app Y)).toFun ((equivShrink ((yoneda.obj Y).obj X)) f)
Module: Mathlib.CategoryTheory.Monoidal.Transport

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategoryStruct D
F : D ⥤ C
inst✝ : F.Faithful
fData : InducingFunctorData F
this : MonoidalCategory D := induced F fData
x✝ : D
⊢ (ρ_ (F.obj x✝)).hom = F.obj x✝ ◁ fData.εIso.hom ≫ (fData.μIso x✝ (𝟙_ D)).hom ≫ F.map (ρ_ x✝).hom

Tactic:
simp [fData.rightUnitor_eq]

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.Monoidal
T : D
⊢ (ε F ≫ η F) ▷ T = 𝟙 (𝟙_ D ⊗ T)

Tactic:
ε_η,

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.Monoidal
T : D
⊢ 𝟙 (𝟙_ D) ▷ T = 𝟙 (𝟙_ D ⊗ T)
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.Monoidal
T : D
⊢ T ◁ (ε F ≫ η F) = 𝟙 (T ⊗ 𝟙_ D)

Tactic:
ε_η,

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.Monoidal
T : D
⊢ T ◁ 𝟙 (𝟙_ D) = 𝟙 (T ⊗ 𝟙_ D)
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: case η
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : C ⥤ D
a b : F.Monoidal
eq : a.toLaxMonoidal = b.toLaxMonoidal
⊢ ε F ≫ η F = ε F ≫ η F

Tactic:
ε_η,

Goal state after:
case η
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : C ⥤ D
a b : F.Monoidal
eq : a.toLaxMonoidal = b.toLaxMonoidal
⊢ ε F ≫ η F = 𝟙 (𝟙_ D)
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: case ε
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : C ⥤ D
a b : F.Monoidal
eq : a.toOplaxMonoidal = b.toOplaxMonoidal
⊢ ε F ≫ η F = ε F ≫ η F

Tactic:
ε_η,

Goal state after:
case ε
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : C ⥤ D
a b : F.Monoidal
eq : a.toOplaxMonoidal = b.toOplaxMonoidal
⊢ ε F ≫ η F = 𝟙 (𝟙_ D)
Module: Mathlib.CategoryTheory.Limits.Opposites

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : J ⥤ Cᵒᵖ
c : Cocone F
hc : IsColimit c
s : Cone F.leftOp
m : s.pt ⟶ (coneLeftOpOfCocone c).pt
w : ∀ (j : Jᵒᵖ), m ≫ (coneLeftOpOfCocone c).π.app j = s.π.app j
j : J
⊢ (c.ι.app j ≫ m.op).unop = (c.ι.app j ≫ (hc.desc (coconeOfConeLeftOp s)).unop.op).unop

Tactic:
simpa only [Quiver.Hom.op_unop, IsColimit.fac, coconeOfConeLeftOp_ι_app] using! w (op j)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Opposites

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : Jᵒᵖ ⥤ C
c : Cone F
hc : IsLimit c
s : Cocone F.rightOp
m : (coconeRightOpOfCone c).pt ⟶ s.pt
w : ∀ (j : J), (coconeRightOpOfCone c).ι.app j ≫ m = s.ι.app j
⊢ m = (hc.lift (coneOfCoconeRightOp s)).op

Tactic:
refine Quiver.Hom.unop_inj (hc.hom_ext fun j => Quiver.Hom.op_inj ?_)
    simpa only [Quiver.Hom.unop_op, IsLimit.fac] using! w (unop j)

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

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X Y Z : D
this :
  ∀ {X Y : D} (f : X ⟶ Y) (X' : D) {Z : D} (h : (𝟭 D).obj Y ⊗ (𝟭 D).obj X' ⟶ Z),
    (G ⋙ F).map f ▷ (G ⋙ F).obj X' ≫ (adj.counit.app Y ⊗ₘ adj.counit.app X') ≫ h =
      (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ (𝟭 D).map f ▷ (𝟭 D).obj X' ≫ h
⊢ δ F (G.obj X ⊗ G.obj Y) (G.obj Z) ≫
      F.map (adj.unit.app (G.obj X ⊗ G.obj Y)) ▷ F.obj (G.obj Z) ≫
        F.map (G.map (δ F (G.obj X) (G.obj Y))) ▷ F.obj (G.obj Z) ≫
          F.map (G.map (adj.counit.app X ⊗ₘ adj.counit.app Y)) ▷ F.obj (G.obj Z) ≫
            (adj.counit.app (X ⊗ Y) ⊗ₘ adj.counit.app Z) ≫ (α_ X Y Z).hom =
    F.map (α_ (G.obj X) (G.obj Y) (G.obj Z)).hom ≫
      F.map (G.obj X ◁ adj.unit.app (G.obj Y ⊗ G.obj Z)) ≫
        F.map (G.obj X ◁ G.map (δ F (G.obj Y) (G.obj Z))) ≫
          F.map (G.obj X ◁ G.map (adj.counit.app Y ⊗ₘ adj.counit.app Z)) ≫
            δ F (G.obj X) (G.obj (Y ⊗ Z)) ≫ (adj.counit.app X ⊗ₘ adj.counit.app (Y ⊗ Z))

Tactic:
dsimp only [id_obj, comp_obj, Functor.comp_map, Functor.id_map] at this

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X Y Z : D
this :
  ∀ {X Y : D} (f : X ⟶ Y) (X' : D) {Z : D} (h : Y ⊗ X' ⟶ Z),
    F.map (G.map f) ▷ F.obj (G.obj X') ≫ (adj.counit.app Y ⊗ₘ adj.counit.app X') ≫ h =
      (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ f ▷ X' ≫ h
⊢ δ F (G.obj X ⊗ G.obj Y) (G.obj Z) ≫
      F.map (adj.unit.app (G.obj X ⊗ G.obj Y)) ▷ F.obj (G.obj Z) ≫
        F.map (G.map (δ F (G.obj X) (G.obj Y))) ▷ F.obj (G.obj Z) ≫
          F.map (G.map (adj.counit.app X ⊗ₘ adj.counit.app Y)) ▷ F.obj (G.obj Z) ≫
            (adj.counit.app (X ⊗ Y) ⊗ₘ adj.counit.app Z) ≫ (α_ X Y Z).hom =
    F.map (α_ (G.obj X) (G.obj Y) (G.obj Z)).hom ≫
      F.map (G.obj X ◁ adj.unit.app (G.obj Y ⊗ G.obj Z)) ≫
        F.map (G.obj X ◁ G.map (δ F (G.obj Y) (G.obj Z))) ≫
          F.map (G.obj X ◁ G.map (adj.counit.app Y ⊗ₘ adj.counit.app Z)) ≫
            δ F (G.obj X) (G.obj (Y ⊗ Z)) ≫ (adj.counit.app X ⊗ₘ adj.counit.app (Y ⊗ Z))
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x✝ W' : MorphismProperty C
h : x✝ ≤ W'
⊢ x✝.multiplicativeClosure ≤ W'.multiplicativeClosure

Tactic:
by simpa using h.trans W'.le_multiplicativeClosure

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
W X Y Z S T : C
f₁ : W ⟶ S
f₂ : X ⟶ S
inst✝¹ : HasPullback f₁ f₂
g₁ : Y ⟶ T
g₂ : Z ⟶ T
inst✝ : HasPullback g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
⊢ (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂).op =
    (pushoutIsoOpPullback g₁.op g₂.op).inv ≫
      pushout.map g₁.op g₂.op f₁.op f₂.op i₁.op i₂.op i₃.op ⋯ ⋯ ≫ (pushoutIsoOpPullback f₁.op f₂.op).hom

Tactic:
Iso.eq_inv_comp

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
W X Y Z S T : C
f₁ : W ⟶ S
f₂ : X ⟶ S
inst✝¹ : HasPullback f₁ f₂
g₁ : Y ⟶ T
g₂ : Z ⟶ T
inst✝ : HasPullback g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
⊢ (pushoutIsoOpPullback g₁.op g₂.op).hom ≫ (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂).op =
    pushout.map g₁.op g₂.op f₁.op f₂.op i₁.op i₂.op i₃.op ⋯ ⋯ ≫ (pushoutIsoOpPullback f₁.op f₂.op).hom
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.LaxMonoidal
x✝ : C
⊢ (adj.homEquiv x✝ (𝟙_ D ⊗ F.obj x✝)) (λ_ (F.obj x✝)).inv =
    (λ_ x✝).inv ≫
      (adj.homEquiv (𝟙_ C ⊗ x✝) (𝟙_ D ⊗ F.obj x✝))
        ((adj.homEquiv (𝟙_ C ⊗ x✝) (F.obj (𝟙_ C) ⊗ F.obj x✝)).symm
            ((adj.unit.app (𝟙_ C) ⊗ₘ adj.unit.app x✝) ≫ μ G (F.obj (𝟙_ C)) (F.obj x✝)) ≫
          (adj.homEquiv (𝟙_ C) (𝟙_ D)).symm (ε G) ▷ F.obj x✝)

Tactic:
Adjunction.homEquiv_naturality_right,

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.LaxMonoidal
x✝ : C
⊢ (adj.homEquiv x✝ (𝟙_ D ⊗ F.obj x✝)) (λ_ (F.obj x✝)).inv =
    (λ_ x✝).inv ≫
      (adj.homEquiv (𝟙_ C ⊗ x✝) (F.obj (𝟙_ C) ⊗ F.obj x✝))
          ((adj.homEquiv (𝟙_ C ⊗ x✝) (F.obj (𝟙_ C) ⊗ F.obj x✝)).symm
            ((adj.unit.app (𝟙_ C) ⊗ₘ adj.unit.app x✝) ≫ μ G (F.obj (𝟙_ C)) (F.obj x✝))) ≫
        G.map ((adj.homEquiv (𝟙_ C) (𝟙_ D)).symm (ε G) ▷ F.obj x✝)
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.LaxMonoidal
x✝ : C
⊢ (adj.homEquiv x✝ (F.obj x✝ ⊗ 𝟙_ D)) (ρ_ (F.obj x✝)).inv =
    (ρ_ x✝).inv ≫
      (adj.homEquiv (x✝ ⊗ 𝟙_ C) (F.obj x✝ ⊗ 𝟙_ D))
        ((adj.homEquiv (x✝ ⊗ 𝟙_ C) (F.obj x✝ ⊗ F.obj (𝟙_ C))).symm
            ((adj.unit.app x✝ ⊗ₘ adj.unit.app (𝟙_ C)) ≫ μ G (F.obj x✝) (F.obj (𝟙_ C))) ≫
          F.obj x✝ ◁ (adj.homEquiv (𝟙_ C) (𝟙_ D)).symm (ε G))

Tactic:
Adjunction.homEquiv_naturality_right,

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.LaxMonoidal
x✝ : C
⊢ (adj.homEquiv x✝ (F.obj x✝ ⊗ 𝟙_ D)) (ρ_ (F.obj x✝)).inv =
    (ρ_ x✝).inv ≫
      (adj.homEquiv (x✝ ⊗ 𝟙_ C) (F.obj x✝ ⊗ F.obj (𝟙_ C)))
          ((adj.homEquiv (x✝ ⊗ 𝟙_ C) (F.obj x✝ ⊗ F.obj (𝟙_ C))).symm
            ((adj.unit.app x✝ ⊗ₘ adj.unit.app (𝟙_ C)) ≫ μ G (F.obj x✝) (F.obj (𝟙_ C)))) ≫
        G.map (F.obj x✝ ◁ (adj.homEquiv (𝟙_ C) (𝟙_ D)).symm (ε G))
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

Goal state before:
pp: case a
C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : MonoidalCategory C
inst✝⁸ : BraidedCategory C
D : Type u₂
inst✝⁷ : Category.{v₂, u₂} D
inst✝⁶ : MonoidalCategory D
inst✝⁵ : BraidedCategory D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : MonoidalCategory E
inst✝² : BraidedCategory E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.LaxBraided
inst✝ : G.LaxBraided
X Y : C
| μ G (F.obj X) (F.obj Y) ≫ G.map (β_ (F.obj X) (F.obj Y)).hom

pp: case a
C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : MonoidalCategory C
inst✝⁸ : BraidedCategory C
D : Type u₂
inst✝⁷ : Category.{v₂, u₂} D
inst✝⁶ : MonoidalCategory D
inst✝⁵ : BraidedCategory D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : MonoidalCategory E
inst✝² : BraidedCategory E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.LaxBraided
inst✝ : G.LaxBraided
X Y : C
| G.map (μ F Y X)

Tactic:
rw [braided]

Goal state after:
case a
C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : MonoidalCategory C
inst✝⁸ : BraidedCategory C
D : Type u₂
inst✝⁷ : Category.{v₂, u₂} D
inst✝⁶ : MonoidalCategory D
inst✝⁵ : BraidedCategory D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : MonoidalCategory E
inst✝² : BraidedCategory E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.LaxBraided
inst✝ : G.LaxBraided
X Y : C
| (β_ (G.obj (F.obj X)) (G.obj (F.obj Y))).hom ≫ μ G (F.obj Y) (F.obj X)

case a
C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : MonoidalCategory C
inst✝⁸ : BraidedCategory C
D : Type u₂
inst✝⁷ : Category.{v₂, u₂} D
inst✝⁶ : MonoidalCategory D
inst✝⁵ : BraidedCategory D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : MonoidalCategory E
inst✝² : BraidedCategory E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.LaxBraided
inst✝ : G.LaxBraided
X Y : C
| G.map (μ F Y X)
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: J : Type u
inst✝² : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝¹ : DecidableEq J
A : Type w
inst✝ : AddCommGroup A
f : Quot F →+ A
hc : IsColimit c
⊢ (Hom.hom (hc.desc (toCocone F f))).comp (desc F c) = f

Tactic:
refine Quot.addMonoidHom_ext F (fun j x ↦ ?_)
  rw [AddMonoidHom.comp_apply, ι_desc]
  change (c.ι.app j ≫ hc.desc (toCocone F f)) _ = _
  rw [hc.fac]
  simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
i : SymmetricCategory C
⊢ reverseBraiding C = i.toBraidedCategory

Tactic:
by
  dsimp only [reverseBraiding]
  congr
  funext X Y
  exact Iso.ext (braiding_swap_eq_inv_braiding Y X).symm

Goal state after: