mathlib-initiative/mathlib-tactics huggingface dataset:
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
f g : End F
A : PointedGaloisObject F
⊢ (ConcreteCategory.hom (f.app A.obj)) ((ConcreteCategory.hom (g.app A.obj)) A.pt) =
    (ConcreteCategory.hom (f.app A.obj))
      ((ConcreteCategory.hom (F.map ((AutGalois.π F A) ((endEquivAutGalois F) g)).hom)) A.pt)

Tactic:
endEquivAutGalois_π

Goal state after:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
f g : End F
A : PointedGaloisObject F
⊢ (ConcreteCategory.hom (f.app A.obj)) ((ConcreteCategory.hom (g.app A.obj)) A.pt) =
    (ConcreteCategory.hom (f.app A.obj)) ((ConcreteCategory.hom (g.app A.obj)) A.pt)
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
f : Aut F
A : C
inst✝ : IsGalois A
a : (F.obj A).obj
⊢ (ConcreteCategory.hom
        (F.map
          ((AutGalois.π F { obj := A, pt := a, isGalois := ⋯ })
              ((endEquivAutGalois F) ↑((Aut.unitsEndEquivAut F).symm f))).hom))
      a =
    (ConcreteCategory.hom (f.hom.app A)) a

Tactic:
endEquivAutGalois_π

Goal state after:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
f : Aut F
A : C
inst✝ : IsGalois A
a : (F.obj A).obj
⊢ (ConcreteCategory.hom ((↑((Aut.unitsEndEquivAut F).symm f)).app { obj := A, pt := a, isGalois := ⋯ }.obj))
      { obj := A, pt := a, isGalois := ⋯ }.pt =
    (ConcreteCategory.hom (f.hom.app A)) a
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✝
x✝ y : (F.obj X✝).obj
F' : C ⥤ FintypeCat := F ⋙ FintypeCat.uSwitch
this : FiberFunctor F' := comp_right FintypeCat.uSwitch
e : (Y : C) → (F'.obj Y).obj ≃ (F.obj Y).obj := fun Y ↦ (F.obj Y).uSwitchEquiv
x' : (F'.obj X✝).obj := (e X✝).symm x✝
hx' : x' = (e X✝).symm x✝
y' : (F'.obj X✝).obj := (e X✝).symm y
hy' : y' = (e X✝).symm y
g' : Aut F'
hg' : (ConcreteCategory.hom (g'.hom.app X✝)) x' = y'
gapp : (Y : C) → F.obj Y ≅ F.obj Y :=
  fun Y ↦ FintypeCat.equivEquivIso ((e Y).symm.trans ((FintypeCat.equivEquivIso.symm (Iso.app g' Y)).trans (e Y)))
X Y : C
f : X ⟶ Y
x : (F.obj X).obj
⊢ (ConcreteCategory.hom
        (FintypeCat.equivEquivIso
            ((F.obj Y).uSwitchEquiv.symm.trans
              ((FintypeCat.equivEquivIso.symm (Iso.app g' Y)).trans (F.obj Y).uSwitchEquiv))).hom)
      ((ConcreteCategory.hom (F.map f)) x) =
    (F.obj Y).uSwitchEquiv
      ((ConcreteCategory.hom (g'.hom.app Y)) ((ConcreteCategory.hom (F'.map f)) ((F.obj X).uSwitchEquiv.symm x)))

Tactic:
FintypeCat.uSwitchEquiv_symm_naturality (F.map f)

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✝
x✝ y : (F.obj X✝).obj
F' : C ⥤ FintypeCat := F ⋙ FintypeCat.uSwitch
this : FiberFunctor F' := comp_right FintypeCat.uSwitch
e : (Y : C) → (F'.obj Y).obj ≃ (F.obj Y).obj := fun Y ↦ (F.obj Y).uSwitchEquiv
x' : (F'.obj X✝).obj := (e X✝).symm x✝
hx' : x' = (e X✝).symm x✝
y' : (F'.obj X✝).obj := (e X✝).symm y
hy' : y' = (e X✝).symm y
g' : Aut F'
hg' : (ConcreteCategory.hom (g'.hom.app X✝)) x' = y'
gapp : (Y : C) → F.obj Y ≅ F.obj Y :=
  fun Y ↦ FintypeCat.equivEquivIso ((e Y).symm.trans ((FintypeCat.equivEquivIso.symm (Iso.app g' Y)).trans (e Y)))
X Y : C
f : X ⟶ Y
x : (F.obj X).obj
⊢ (ConcreteCategory.hom
        (FintypeCat.equivEquivIso
            ((F.obj Y).uSwitchEquiv.symm.trans
              ((FintypeCat.equivEquivIso.symm (Iso.app g' Y)).trans (F.obj Y).uSwitchEquiv))).hom)
      ((ConcreteCategory.hom (F.map f)) x) =
    (F.obj Y).uSwitchEquiv
      ((ConcreteCategory.hom (g'.hom.app Y)) ((F.obj Y).uSwitchEquiv.symm ((ConcreteCategory.hom (F.map f)) x)))
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
G : Type u₁
inst✝¹ : Groupoid G
H : Type u₂
inst✝ : Groupoid H
φ : C ⥤ G
ψ : G ⥤ H
⊢ (of C ⋙ lift φ) ⋙ ψ = φ ⋙ ψ

Tactic:
lift_spec

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
G : Type u₁
inst✝¹ : Groupoid G
H : Type u₂
inst✝ : Groupoid H
φ : C ⥤ G
ψ : G ⥤ H
⊢ φ ⋙ ψ = φ ⋙ ψ
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
G✝ : Type u₁
inst✝ : Groupoid G✝
F G : FreeGroupoid C ⥤ G✝
h : of C ⋙ F = of C ⋙ G
⊢ lift (of C ⋙ G) = G

Tactic:
← lift_unique (of C ⋙ G) G rfl

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
G✝ : Type u₁
inst✝ : Groupoid G✝
F G : FreeGroupoid C ⥤ G✝
h : of C ⋙ F = of C ⋙ G
⊢ G = G
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: case refl
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✝
c₄ : C
q : φ.obj d✝ ⟶ φ.obj c₄
hq : q ∈ {x | Map.Arrows φ hφ S (φ.obj d✝) (φ.obj c₄) x}
g : d✝ ⟶ c₄
he : φ.obj d✝ = φ.obj d✝
hg : g ∈ S.arrows d✝ c₄
gq : q = eqToHom ⋯ ≫ φ.map g ≫ eqToHom ⋯
⊢ φ.map f ≫ eqToHom ⋯ ≫ φ.map g ≫ eqToHom ⋯ ∈ {x | Map.Arrows φ hφ S (φ.obj c✝) (φ.obj c₄) x}

Tactic:
← eq_conj_eqToHom,

Goal state after:
case refl
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✝
c₄ : C
q : φ.obj d✝ ⟶ φ.obj c₄
hq : q ∈ {x | Map.Arrows φ hφ S (φ.obj d✝) (φ.obj c₄) x}
g : d✝ ⟶ c₄
he : φ.obj d✝ = φ.obj d✝
hg : g ∈ S.arrows d✝ c₄
gq : q = eqToHom ⋯ ≫ φ.map g ≫ eqToHom ⋯
⊢ φ.map f ≫ φ.map g ∈ {x | Map.Arrows φ hφ S (φ.obj c✝) (φ.obj c₄) x}
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: case mpr
C : Type u
inst✝¹ : Groupoid C
S : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
c : C
γ : c ⟶ c
γS : γ ∈ S.arrows c c
⊢ {x | Map.Arrows φ hφ S (φ.obj c) (φ.obj c) x}.Nonempty

Tactic:
exact ⟨φ.map γ, ⟨γ, γS⟩⟩

Goal state after:
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
j : J
x : ↑(F.obj j)
hx : (ConcreteCategory.hom (colimit.ι F j)) x = 0
⊢ ∃ j' i, (ModuleCat.Hom.hom (F.map i)) x = 0

Tactic:
rw [show 0 = colimit.ι F j 0 by simp, colimit_rep_eq_iff_exists] at hx

Goal state after:
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
j : J
x : ↑(F.obj j)
hx : ∃ k f g, (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map g)) 0
⊢ ∃ j' i, (ModuleCat.Hom.hom (F.map i)) x = 0
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
U : FormalCoproduct C
α : Type
inst✝ : HasProductsOfShape α C
s : Fan fun x ↦ U
f : s.pt.I → (U.powerFan α).pt.I
φ : (i : s.pt.I) → s.pt.obj i ⟶ (U.powerFan α).pt.obj (f i)
hm : ∀ (j : α), { f := f, φ := φ } ≫ (U.powerFan α).proj j = s.proj j
⊢ f = fun i a ↦ (s.proj a).f i

Tactic:
by
        ext i
        dsimp
        ext a
        exact congr_fun (congr_arg FormalCoproduct.Hom.f (hm a)) i

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.BifunctorCokernel

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C : Type u_3
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, u_3} C
inst✝⁸ : HasZeroMorphisms C₁
inst✝⁷ : HasZeroMorphisms C₂
inst✝⁶ : HasZeroMorphisms C
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
c₁ : CokernelCofork f₁
hc₁ : IsColimit c₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
c₂ : CokernelCofork f₂
hc₂ : IsColimit c₂
F : C₁ ⥤ C₂ ⥤ C
inst✝⁵ : (F.obj c₁.pt).PreservesZeroMorphisms
inst✝⁴ : F.PreservesZeroMorphisms
inst✝³ : PreservesColimit (parallelPair f₂ 0) (F.obj c₁.pt)
inst✝² : PreservesColimit (parallelPair f₁ 0) (F.flip.obj Y₂)
inst✝¹ : HasBinaryCoproduct ((F.obj X₁).obj Y₂) ((F.obj Y₁).obj X₂)
inst✝ : PreservesColimit (parallelPair f₁ 0) (F.flip.obj X₂)
s : CokernelCofork (coprod.desc ((F.map f₁).app Y₂) ((F.obj Y₁).map f₂))
l : (c₁.map (F.flip.obj Y₂)).pt ⟶ s.pt
hl : Cofork.π (c₁.map (F.flip.obj Y₂)) ≫ l = Cofork.π s
this : coprod.inr ≫ coprod.desc ((F.map f₁).app Y₂) ((F.obj Y₁).map f₂) ≫ Cofork.π s = coprod.inr ≫ 0
⊢ (F.obj c₁.pt).map f₂ ≫ l = 0 ≫ l

Tactic:
rw [coprod.inr_desc_assoc, ← dsimp% hl, NatTrans.naturality_assoc, comp_zero] at this

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
C : Type u_3
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, u_3} C
inst✝⁸ : HasZeroMorphisms C₁
inst✝⁷ : HasZeroMorphisms C₂
inst✝⁶ : HasZeroMorphisms C
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
c₁ : CokernelCofork f₁
hc₁ : IsColimit c₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
c₂ : CokernelCofork f₂
hc₂ : IsColimit c₂
F : C₁ ⥤ C₂ ⥤ C
inst✝⁵ : (F.obj c₁.pt).PreservesZeroMorphisms
inst✝⁴ : F.PreservesZeroMorphisms
inst✝³ : PreservesColimit (parallelPair f₂ 0) (F.obj c₁.pt)
inst✝² : PreservesColimit (parallelPair f₁ 0) (F.flip.obj Y₂)
inst✝¹ : HasBinaryCoproduct ((F.obj X₁).obj Y₂) ((F.obj Y₁).obj X₂)
inst✝ : PreservesColimit (parallelPair f₁ 0) (F.flip.obj X₂)
s : CokernelCofork (coprod.desc ((F.map f₁).app Y₂) ((F.obj Y₁).map f₂))
l : (c₁.map (F.flip.obj Y₂)).pt ⟶ s.pt
hl : Cofork.π (c₁.map (F.flip.obj Y₂)) ≫ l = Cofork.π s
this : (F.map (Cofork.π c₁)).app X₂ ≫ (F.obj c₁.pt).map f₂ ≫ l = 0
⊢ (F.obj c₁.pt).map f₂ ≫ l = 0 ≫ l
Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct

Goal state before:
pp: case e_a
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
n m : ℕ
h : ¬m + 1 < n
this : homOfLE ⋯ = homOfLE ⋯ ≫ homOfLE ⋯
⊢ (Functor.ofOpSequence (functorMap f)).map (homOfLE ⋯).op ≫
      Pi.π (fun m ↦ if m < n then M m else N m) (m + 1) ≫ eqToHom ⋯ =
    Pi.π (fun m_1 ↦ if m_1 < m + 1 then M m_1 else N m_1) (m + 1) ≫ eqToHom ⋯

Tactic:
exact functorMap_commSq_aux f (by lia) (by lia)

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

Goal state before:
pp: case neg
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 : ℕ
h : ¬m < n
⊢ (Pi.lift fun m ↦ s.π.app (Opposite.op (m + 1)) ≫ Pi.π (fun i ↦ if x : i < m + 1 then M i else N i) m ≫ eqToHom ⋯) ≫
      (cone f).π.app (Opposite.op n) ≫ Pi.π (fun m ↦ if x : m < n then M m else N m) m =
    s.π.app (Opposite.op n) ≫ Pi.π (fun m ↦ if x : m < n then M m else N m) m

Tactic:
rw [cone_π_app_comp_Pi_π_neg f _ _ h]

Goal state after:
case neg
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 : ℕ
h : ¬m < n
⊢ (Pi.lift fun m ↦ s.π.app (Opposite.op (m + 1)) ≫ Pi.π (fun i ↦ if x : i < m + 1 then M i else N i) m ≫ eqToHom ⋯) ≫
      Pi.π M m ≫ f m ≫ eqToHom ⋯ =
    s.π.app (Opposite.op n) ≫ Pi.π (fun m ↦ if x : m < n then M m else N m) m
Module: Mathlib.CategoryTheory.Limits.Types.PreservesLimit

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : Type u'
inst✝¹ : Category.{v', u'} J
inst✝ : LocallySmall.{w, v, u} C
F : J ⥤ Cᵒᵖ
c : Cone F
c' : Cocone (F.leftOp ⋙ shrinkYoneda.{w, v, u})
hc : IsLimit c
hc' : IsColimit c'
⊢ ObjectProperty.preservesLimit F = (MorphismProperty.single (coconePtToShrinkYoneda c hc')).isLocal

Tactic:
by
  ext P
  rw [← nonempty_isLimit_mapCone_iff c hc' P]
  exact ⟨fun _ ↦ ⟨isLimitOfPreserves P hc⟩,
    fun ⟨h⟩ ↦ preservesLimit_of_preserves_limit_cone hc h⟩

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : C
Y Z : Over X
inst✝ : ChosenPullbacksAlong Z.hom
T✝ : Over X
u : T✝ ⟶ Y
v : T✝ ⟶ Z
⊢ Over.Hom.left u ≫ Y.hom = Over.Hom.left v ≫ Z.hom

Tactic:
by rw [Over.w u, Over.w v]

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Monadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝² : HasCoequalizerOfIsSplitPair G
inst✝¹ : PreservesColimitOfIsSplitPair G
inst✝ : ReflectsColimitOfIsSplitPair G
this : ∀ (X : adj.toMonad.Algebra), IsIso ((comparisonAdjunction adj).unit.app X)
⊢ ∀ (Y : D), IsIso ((comparisonAdjunction adj).counit.app Y)

Tactic:
intro Y

Goal state after:
C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝² : HasCoequalizerOfIsSplitPair G
inst✝¹ : PreservesColimitOfIsSplitPair G
inst✝ : ReflectsColimitOfIsSplitPair G
this : ∀ (X : adj.toMonad.Algebra), IsIso ((comparisonAdjunction adj).unit.app X)
Y : D
⊢ IsIso ((comparisonAdjunction adj).counit.app Y)
Module: Mathlib.CategoryTheory.Monad.Monadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝² : HasReflexiveCoequalizers D
inst✝¹ : G.ReflectsIsomorphisms
inst✝ : PreservesColimitOfIsReflexivePair G
this : ∀ (X : adj.toMonad.Algebra), IsIso ((comparisonAdjunction adj).unit.app X)
⊢ ∀ (Y : D), IsIso ((comparisonAdjunction adj).counit.app Y)

Tactic:
intro Y

Goal state after:
C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝² : HasReflexiveCoequalizers D
inst✝¹ : G.ReflectsIsomorphisms
inst✝ : PreservesColimitOfIsReflexivePair G
this : ∀ (X : adj.toMonad.Algebra), IsIso ((comparisonAdjunction adj).unit.app X)
Y : D
⊢ IsIso ((comparisonAdjunction adj).counit.app Y)
Module: Mathlib.CategoryTheory.Monoidal.Action.Basic

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

Tactic:
by
  rw [Iso.comp_inv_eq, Category.assoc, Eq.comm, Iso.inv_comp_eq, actionAssocIso_hom_naturality]

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

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 C
inst✝ : MonoidalRightAction C D
d₁ d₂ : D
c₁ c₂ c₃ c₄ : C
f : d₁ ⟶ d₂
g : c₁ ⟶ c₂
h : c₃ ⟶ c₄
⊢ ((f ⊙ᵣₘ g) ⊙ᵣₘ h) ≫ (αᵣ d₂ c₂ c₄).inv = (αᵣ d₁ c₁ c₃).inv ≫ (f ⊙ᵣₘ g ⊗ₘ h)

Tactic:
by
  rw [Iso.comp_inv_eq, Category.assoc, Eq.comm, Iso.inv_comp_eq, actionAssocIso_hom_naturality]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
M : C
inst✝¹ : MonObj M
X : C
inst✝ : ModObj M X
Z Z' : C
g : Z' ⟶ Z
m : Z ⟶ M
x : Z ⟶ X
⊢ g ≫ lift m x ≫ γ = lift (g ≫ m) (g ≫ x) ≫ γ

Tactic:
comp_lift_assoc

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
M : C
inst✝¹ : MonObj M
X : C
inst✝ : ModObj M X
Z Z' : C
g : Z' ⟶ Z
m : Z ⟶ M
x : Z ⟶ X
⊢ lift (g ≫ m) (g ≫ x) ≫ γ = lift (g ≫ m) (g ≫ x) ≫ γ
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
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)
| (coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ▷ T.X ≫ actRight P Q) ▷ T.X

pp: case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
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)
| actRight P Q

pp: case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
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.X) T.X T.X).inv

Tactic:
π_tensor_id_actRight,

Goal state after:
case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
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.X T.X).hom ≫
      P.X ◁ Q.actRight ≫ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)) ▷
    T.X

case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
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)
| actRight P Q

case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
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.X) T.X T.X).inv
Module: Mathlib.CategoryTheory.Monoidal.Ring

Goal state before:
pp: case refine_2
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
R : C
inst✝¹ : MonObj R
inst✝ : AddMonObj R
h : ∀ ⦃X : C⦄ (a b c : X ⟶ R), a * (b + c) = a * b + a * c
⊢ R ◁ σ ≫ μ = lift (R ◁ fst R R ≫ μ) (R ◁ snd R R ≫ μ) ≫ σ

Tactic:
replace h := h (fst R (R ⊗ R)) (snd _ _ ≫ fst _ _) (snd _ _ ≫ snd _ _)
    simp only [Hom.mul_def, Hom.add_def] at h
    convert! h using 2
    · cat_disch
    · ext
      · simp only [lift_fst]
        congr 1
        cat_disch
      · simp only [lift_snd]
        congr 1
        cat_disch

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

Goal state before:
pp: case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
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₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| R.X ◁ (coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ▷ T.X ≫ actRight P Q)

pp: case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
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₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| actLeft P Q

pp: case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
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₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| (α_ R.X (P.X ⊗ Q.X) T.X).hom

Tactic:
π_tensor_id_actRight,

Goal state after:
case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
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₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| R.X ◁
    ((α_ P.X Q.X T.X).hom ≫
      P.X ◁ Q.actRight ≫ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft))

case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
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₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| actLeft P Q

case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
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₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| (α_ R.X (P.X ⊗ Q.X) T.X).hom
Module: Mathlib.CategoryTheory.Monoidal.Closed.Functor

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : CartesianMonoidalCategory C
inst✝³ : CartesianMonoidalCategory D
F : C ⥤ D
inst✝² : MonoidalClosed C
inst✝¹ : MonoidalClosed D
inst✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
A B : C
⊢ uncurry ((expComparison F A).natTrans.app B) = inv (prodComparison F A ((ihom A).obj B)) ≫ F.map ((ihom.ev A).app B)

Tactic:
uncurry_eq,

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : CartesianMonoidalCategory C
inst✝³ : CartesianMonoidalCategory D
F : C ⥤ D
inst✝² : MonoidalClosed C
inst✝¹ : MonoidalClosed D
inst✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
A B : C
⊢ F.obj A ◁ (expComparison F A).natTrans.app B ≫ (ihom.ev (F.obj A)).app (F.obj B) =
    inv (prodComparison F A ((ihom A).obj B)) ≫ F.map ((ihom.ev A).app B)
Module: Mathlib.CategoryTheory.Monoidal.Closed.Ideal

Goal state before:
pp: case comm1
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : CartesianMonoidalCategory C
inst✝³ : Reflective i
inst✝² : MonoidalClosed C
inst✝¹ : CartesianMonoidalCategory D
inst✝ : ExponentialIdeal i
l : i.EssImageSubcategory ⥤ D
φ : l ⋙ i ≅ i.essImage.ι
B : D
⊢ i ⋙ tensorLeft (i.obj B) ≅ tensorLeft B ⋙ i

Tactic:
symm
          refine NatIso.ofComponents (fun X => ?_) (fun f => ?_)
          · haveI :=
              Adjunction.rightAdjoint_preservesLimits.{0, 0} (reflectorAdjunction i)
            apply asIso (prodComparison i B X)
          · dsimp [asIso]
            rw [prodComparison_natural_whiskerLeft]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Closed.Ideal

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Reflective i
inst✝³ : MonoidalClosed C
inst✝² : CartesianMonoidalCategory D
inst✝¹ : ExponentialIdeal i
inst✝ : BraidedCategory C
A B : C
⊢ prodComparison (reflector i) A B ≫ (bijection i A B ((reflector i).obj (A ⊗ B))) (𝟙 ((reflector i).obj (A ⊗ B))) =
    𝟙 ((reflector i).obj (A ⊗ B))

Tactic:
rw [← (bijection i _ _ _).injective.eq_iff, bijection_natural, ← bijection_symm_apply_id,
        Equiv.apply_symm_apply, Category.id_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
V : Type u₂
inst✝⁴ : Category.{v₂, u₂} V
inst✝³ : MonoidalCategory C
inst✝² : MonoidalCategory V
inst✝¹ : MonoidalClosed V
F G H : C ⥤ V
inst✝ : DayConvolution F H
ℌ : DayConvolutionInternalHom F G H
x y : C
⊢ (DayConvolution.unit F H).app (x, y) ≫ ℌ.ev_app.app (x ⊗ y) = MonoidalClosed.uncurry (ℌ.π y x)

Tactic:
have := Functor.descOfIsLeftKanExtension_fac_app (F ⊛ H)
    (DayConvolution.unit F H) G

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
V : Type u₂
inst✝⁴ : Category.{v₂, u₂} V
inst✝³ : MonoidalCategory C
inst✝² : MonoidalCategory V
inst✝¹ : MonoidalClosed V
F G H : C ⥤ V
inst✝ : DayConvolution F H
ℌ : DayConvolutionInternalHom F G H
x y : C
this :
  ∀ (β : F ⊠ H ⟶ tensor C ⋙ G) (X : C × C),
    (DayConvolution.unit F H).app X ≫
        ((F ⊛ H).descOfIsLeftKanExtension (DayConvolution.unit F H) G β).app ((tensor C).obj X) =
      β.app X
⊢ (DayConvolution.unit F H).app (x, y) ≫ ℌ.ev_app.app (x ⊗ y) = MonoidalClosed.uncurry (ℌ.π y x)
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ (ε ≫ η) ≫ Δ = ε ≫ (λ_ (𝟙_ C)).inv ≫ (η ⊗ₘ η)

Tactic:
simp [MonObj.tensorObj.one_def]

Goal state after: