mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Enriched.FunctorCategory

Goal state before:
pp: V : Type u₁
inst✝⁸ : Category.{v₁, u₁} V
inst✝⁷ : MonoidalCategory V
C : Type u₂
inst✝⁶ : Category.{v₂, u₂} C
J : Type u₃
inst✝⁵ : Category.{v₃, u₃} J
K : Type u₄
inst✝⁴ : Category.{v₄, u₄} K
inst✝³ : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ F₄ : J ⥤ C
inst✝² : HasEnrichedHom V F₁ F₂
inst✝¹ : HasEnrichedHom V F₂ F₃
inst✝ : HasEnrichedHom V F₁ F₃
i j : J
f : i ⟶ j
this :
  end_.π (diagram V F₂ F₃) i ≫
      (ρ_ (F₂.obj i ⟶[V] F₃.obj i)).inv ≫
        (F₂.obj i ⟶[V] F₃.obj i) ◁ (eHomEquiv V) (F₃.map f) ≫ eComp V (F₂.obj i) (F₃.obj i) (F₃.obj j) =
    end_.π (diagram V F₂ F₃) j ≫
      (λ_ (F₂.obj j ⟶[V] F₃.obj j)).inv ≫
        ((eHomEquiv V) (F₂.map f) ▷ F₂.obj j ⟶[V] F₃.obj j) ≫ eComp V (F₂.obj i) (F₂.obj j) (F₃.obj j)
| end_.π (diagram V F₁ F₂) i ▷ enrichedHom V F₂ F₃ ≫
    (F₁.obj i ⟶[V] F₂.obj i) ◁ end_.π (diagram V F₂ F₃) i ≫
      (ρ_ ((F₁.obj i ⟶[V] F₂.obj i) ⊗ F₂.obj i ⟶[V] F₃.obj i)).inv ≫
        (α_ (F₁.obj i ⟶[V] F₂.obj i) (F₂.obj i ⟶[V] F₃.obj i) (𝟙_ V)).hom ≫
          (F₁.obj i ⟶[V] F₂.obj i) ◁ (F₂.obj i ⟶[V] F₃.obj i) ◁ (eHomEquiv V) (F₃.map f) ≫
            (α_ (F₁.obj i ⟶[V] F₂.obj i) (F₂.obj i ⟶[V] F₃.obj i) (F₃.obj i ⟶[V] F₃.obj j)).inv ≫
              (eComp V (F₁.obj i) (F₂.obj i) (F₃.obj i) ▷ F₃.obj i ⟶[V] F₃.obj j) ≫
                eComp V (F₁.obj i) (F₃.obj i) (F₃.obj j)

Tactic:
associator_inv_naturality_right_assoc,

Goal state after:
V : Type u₁
inst✝⁸ : Category.{v₁, u₁} V
inst✝⁷ : MonoidalCategory V
C : Type u₂
inst✝⁶ : Category.{v₂, u₂} C
J : Type u₃
inst✝⁵ : Category.{v₃, u₃} J
K : Type u₄
inst✝⁴ : Category.{v₄, u₄} K
inst✝³ : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ F₄ : J ⥤ C
inst✝² : HasEnrichedHom V F₁ F₂
inst✝¹ : HasEnrichedHom V F₂ F₃
inst✝ : HasEnrichedHom V F₁ F₃
i j : J
f : i ⟶ j
this :
  end_.π (diagram V F₂ F₃) i ≫
      (ρ_ (F₂.obj i ⟶[V] F₃.obj i)).inv ≫
        (F₂.obj i ⟶[V] F₃.obj i) ◁ (eHomEquiv V) (F₃.map f) ≫ eComp V (F₂.obj i) (F₃.obj i) (F₃.obj j) =
    end_.π (diagram V F₂ F₃) j ≫
      (λ_ (F₂.obj j ⟶[V] F₃.obj j)).inv ≫
        ((eHomEquiv V) (F₂.map f) ▷ F₂.obj j ⟶[V] F₃.obj j) ≫ eComp V (F₂.obj i) (F₂.obj j) (F₃.obj j)
| end_.π (diagram V F₁ F₂) i ▷ enrichedHom V F₂ F₃ ≫
    (F₁.obj i ⟶[V] F₂.obj i) ◁ end_.π (diagram V F₂ F₃) i ≫
      (ρ_ ((F₁.obj i ⟶[V] F₂.obj i) ⊗ F₂.obj i ⟶[V] F₃.obj i)).inv ≫
        (α_ (F₁.obj i ⟶[V] F₂.obj i) (F₂.obj i ⟶[V] F₃.obj i) (𝟙_ V)).hom ≫
          (α_ (F₁.obj i ⟶[V] F₂.obj i) (F₂.obj i ⟶[V] F₃.obj i) (𝟙_ V)).inv ≫
            ((F₁.obj i ⟶[V] F₂.obj i) ⊗ F₂.obj i ⟶[V] F₃.obj i) ◁ (eHomEquiv V) (F₃.map f) ≫
              (eComp V (F₁.obj i) (F₂.obj i) (F₃.obj i) ▷ F₃.obj i ⟶[V] F₃.obj j) ≫
                eComp V (F₁.obj i) (F₃.obj i) (F₃.obj j)
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
⊢ m = s.π.app (StructuredArrow.mk (𝟙 (L.obj Y))) ≫ e.hom.app Y

Tactic:
have := hm (StructuredArrow.mk (𝟙 (L.obj Y)))
    dsimp at this m hm ⊢
    simp [← reassoc_of% this]

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

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
J : SingleObj (Aut X) ⥤ C := SingleObj.functor (Aut.toEnd X)
e : (F ⋙ FintypeCat.incl).obj (colimit J) ≅
  MulAction.orbitRel.Quotient (Aut X) ((J ⋙ F ⋙ FintypeCat.incl).obj (SingleObj.star (Aut X))) :=
  preservesColimitIso (F ⋙ FintypeCat.incl) J ≪≫ (SingleObj.Types.colimitEquivQuotient (J ⋙ F ⋙ FintypeCat.incl)).toIso
⊢ IsTerminal (colimit (SingleObj.functor (Aut.toEnd X))) ≃ Unique (MulAction.orbitRel.Quotient (Aut X) (F.obj X).obj)

Tactic:
apply Equiv.trans

Goal state after:
case e₁
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X : C
inst✝ : IsConnected X
J : SingleObj (Aut X) ⥤ C := ⋯
e : (F ⋙ FintypeCat.incl).obj (colimit J) ≅
  MulAction.orbitRel.Quotient (Aut X) ((J ⋙ F ⋙ FintypeCat.incl).obj (SingleObj.star (Aut X))) := ⋯
⊢ IsTerminal (colimit (SingleObj.functor (Aut.toEnd X))) ≃ ?β

case e₂
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X : C
inst✝ : IsConnected X
J : SingleObj (Aut X) ⥤ C := ⋯
e : (F ⋙ FintypeCat.incl).obj (colimit J) ≅
  MulAction.orbitRel.Quotient (Aut X) ((J ⋙ F ⋙ FintypeCat.incl).obj (SingleObj.star (Aut X))) := ⋯
⊢ ?β ≃ Unique (MulAction.orbitRel.Quotient (Aut X) (F.obj X).obj)

case β
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X : C
inst✝ : IsConnected X
J : SingleObj (Aut X) ⥤ C := ⋯
e : (F ⋙ FintypeCat.incl).obj (colimit J) ≅
  MulAction.orbitRel.Quotient (Aut X) ((J ⋙ F ⋙ FintypeCat.incl).obj (SingleObj.star (Aut X))) := ⋯
⊢ Sort ?u.105
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 := fun t ↦ (ConcreteCategory.hom (F.map (selfProdProj u t))) b
t s : (F.obj X).obj
hs : (ConcreteCategory.hom (F.map (selfProdProj u t))) b = (ConcreteCategory.hom (F.map (selfProdProj u s))) b
h' : selfProdProj u t = selfProdProj u s
⊢ id t = id ((ConcreteCategory.hom (F.map (selfProdProj u s))) a)

Tactic:
← selfProdProj_fiber h t,

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
t s : (F.obj X).obj
hs : (ConcreteCategory.hom (F.map (selfProdProj u t))) b = (ConcreteCategory.hom (F.map (selfProdProj u s))) b
h' : selfProdProj u t = selfProdProj u s
⊢ id ((ConcreteCategory.hom (F.map (selfProdProj u t))) a) = id ((ConcreteCategory.hom (F.map (selfProdProj u s))) a)
Module: Mathlib.CategoryTheory.Galois.Topology

Goal state before:
pp: C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
⊢ IsClosed (Set.range ⇑(autEmbedding F))

Tactic:
rw [autEmbedding_range]

Goal state after:
C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
⊢ IsClosed (⋂ f, {a | F.map f.hom ≫ (a f.right).hom = (a f.left).hom ≫ F.map f.hom})
Module: Mathlib.CategoryTheory.Galois.Topology

Goal state before:
pp: case refine_1
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
U : Set ((X : C) → Aut (F.obj X))
hUopen : IsOpen U
h1 : 1 ∈ ⇑(autEmbedding F) ⁻¹' U
h : IsOpen (⇑(autEmbedding F) ⁻¹' U)
I : Finset C
u : (a : C) → Set (Aut (F.obj a))
ho : ∀ a ∈ I, IsOpen (u a) ∧ 1 a ∈ u a
ha : (↑I).pi u ⊆ U
fι : ↥I → Type
ff : (X : ↥I) → fι X → C
fc : (X : ↥I) → (i : fι X) → ff X i ⟶ ↑X
h4 : (X : ↥I) → Limits.IsColimit (Limits.Cofan.mk (↑X) (fc X))
h5 : ∀ (X : ↥I) (i : fι X), IsConnected (ff X i)
h6 : ∀ (X : ↥I), Finite (fι X)
X : C
Y : ↥I
hA2 : X ∈ (fun X ↦ Set.range (ff X)) Y
⊢ IsConnected X

Tactic:
obtain ⟨i, rfl⟩ := hA2

Goal state after:
case refine_1
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
U : Set ((X : C) → Aut (F.obj X))
hUopen : IsOpen U
h1 : 1 ∈ ⇑(autEmbedding F) ⁻¹' U
h : IsOpen (⇑(autEmbedding F) ⁻¹' U)
I : Finset C
u : (a : C) → Set (Aut (F.obj a))
ho : ∀ a ∈ I, IsOpen (u a) ∧ 1 a ∈ u a
ha : (↑I).pi u ⊆ U
fι : ↥I → Type
ff : (X : ↥I) → fι X → C
fc : (X : ↥I) → (i : fι X) → ff X i ⟶ ↑X
h4 : (X : ↥I) → Limits.IsColimit (Limits.Cofan.mk (↑X) (fc X))
h5 : ∀ (X : ↥I) (i : fι X), IsConnected (ff X i)
h6 : ∀ (X : ↥I), Finite (fι X)
Y : ↥I
i : fι Y
⊢ IsConnected (ff Y i)
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
⊢ ∀ (x y : G),
    NatIso.ofComponents (isoOnObj F (x * y)) ⋯ =
      NatIso.ofComponents (isoOnObj F x) ⋯ * NatIso.ofComponents (isoOnObj F y) ⋯

Tactic:
intro g h

Goal state after:
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
g h : G
⊢ NatIso.ofComponents (isoOnObj F (g * h)) ⋯ =
    NatIso.ofComponents (isoOnObj F g) ⋯ * NatIso.ofComponents (isoOnObj F h) ⋯
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
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : CompactSpace G
inst✝ : ∀ (X : C), ContinuousSMul G (F.obj X).obj
h : ∀ (X : C) [IsGalois X], MulAction.IsPretransitive G (F.obj X).obj
t : Aut F
gi : PointedGaloisObject F → G
hgi : ∀ (X : PointedGaloisObject F) (x : (F.obj X.obj).obj), gi X • x = (ConcreteCategory.hom (t.hom.app X.obj)) x
⊢ ∃ a, (toAut F G) a = t

Tactic:
let cl (X : PointedGaloisObject F) : Set G := gi X • MulAction.stabilizer G X.pt

Goal state after:
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
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : CompactSpace G
inst✝ : ∀ (X : C), ContinuousSMul G (F.obj X).obj
h : ∀ (X : C) [IsGalois X], MulAction.IsPretransitive G (F.obj X).obj
t : Aut F
gi : PointedGaloisObject F → G
hgi : ∀ (X : PointedGaloisObject F) (x : (F.obj X.obj).obj), gi X • x = (ConcreteCategory.hom (t.hom.app X.obj)) x
cl : PointedGaloisObject F → Set G := fun X ↦ gi X • ↑(MulAction.stabilizer G X.pt)
⊢ ∃ a, (toAut F G) a = t
Module: Mathlib.CategoryTheory.Galois.EssSurj

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝⁵ : GaloisCategory C
inst✝⁴ : FiberFunctor F
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
V U : OpenSubgroup (Aut F)
h : (↑U).Normal
A : C
u : (functorToAction F).obj A ≅ ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ ↑U))
hUinV : U ≤ V
s : Cocone (quotientDiag V h u ⋙ functorToAction F)
f : (coconeQuotientDiag h u hUinV).pt ⟶ s.pt
hf : ∀ (j : SingleObj (↥↑V ⧸ (↑U).subgroupOf ↑V)), (coconeQuotientDiag h u hUinV).ι.app j ≫ f = s.ι.app j
⊢ f = coconeQuotientDiagDesc h u hUinV s

Tactic:
by
    apply Action.hom_ext
    ext (x : Aut F ⧸ V.toSubgroup)
    induction x using Quotient.inductionOn with | _ σ
    simp [← hf (SingleObj.star _), ← ConcreteCategory.comp_apply]

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

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
s : Set (Subgroupoid C)
c✝ d✝ : C
p✝ : c✝ ⟶ d✝
hp : p✝ ∈ ⋂ S ∈ s, S.arrows c✝ d✝
⊢ Groupoid.inv p✝ ∈ ⋂ S ∈ s, S.arrows d✝ c✝

Tactic:
by rw [mem_iInter₂] at hp ⊢; exact fun S hS => S.inv (hp S hS)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech

Goal state before:
pp: case h₂
C : Type u
inst✝¹ : Category.{v, u} C
U V W : FormalCoproduct C
f : U ⟶ V
g : V ⟶ W
α : Type t
inst✝ : HasProductsOfShape α C
i✝ : (U.power α).I
b✝ : α
⊢ (Pi.map fun a ↦ f.φ (i✝ a) ≫ g.φ (f.f (i✝ a))) ≫ Pi.π (W.obj ∘ g.f ∘ f.f ∘ i✝) b✝ =
    Pi.π (U.obj ∘ i✝) b✝ ≫ f.φ (i✝ b✝) ≫ g.φ (f.f (i✝ b✝))

Tactic:
apply Pi.map_π

Goal state after:
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'
P : Cᵒᵖ ⥤ Type w
s : ↑(F ⋙ P).sections
j₁ j₂ : Jᵒᵖ
f : j₁ ⟶ j₂
⊢ (F.leftOp ⋙ shrinkYoneda.{w, v, u}).map f ≫ shrinkYonedaEquiv.symm (↑s (unop j₂)) =
    shrinkYonedaEquiv.symm (↑s (unop j₁)) ≫ ((Functor.const Jᵒᵖ).obj P).map f

Tactic:
rw [← s.property f.unop]

Goal state after:
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'
P : Cᵒᵖ ⥤ Type w
s : ↑(F ⋙ P).sections
j₁ j₂ : Jᵒᵖ
f : j₁ ⟶ j₂
⊢ (F.leftOp ⋙ shrinkYoneda.{w, v, u}).map f ≫ shrinkYonedaEquiv.symm (↑s (unop j₂)) =
    shrinkYonedaEquiv.symm ((ConcreteCategory.hom ((F ⋙ P).map f.unop)) (↑s (unop j₂))) ≫
      ((Functor.const Jᵒᵖ).obj P).map f
Module: Mathlib.CategoryTheory.Monad.EquivMon

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ Y : Mon (C ⥤ C)
f : X✝ ⟶ Y
X : C
⊢ (ofMon X✝).η.app X ≫ f.hom.app X = (ofMon Y).η.app X

Tactic:
by
        simpa [-IsMonHom.one_hom] using congrArg (fun t ↦ t.app X) (IsMonHom.one_hom f.hom)

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)
this : ∀ (Y : D), IsIso ((comparisonAdjunction adj).counit.app Y)
⊢ (comparison adj).IsEquivalence

Tactic:
exact (comparisonAdjunction adj).toEquivalence.isEquivalence_inverse

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✝² : HasReflexiveCoequalizers D
inst✝¹ : G.ReflectsIsomorphisms
inst✝ : PreservesColimitOfIsReflexivePair G
this✝ : ∀ (X : adj.toMonad.Algebra), IsIso ((comparisonAdjunction adj).unit.app X)
this : ∀ (Y : D), IsIso ((comparisonAdjunction adj).counit.app Y)
⊢ (comparison adj).IsEquivalence

Tactic:
exact (comparisonAdjunction adj).toEquivalence.isEquivalence_inverse

Goal state after:
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
inst✝ : MonoidalLeftAction C D
c₁ c₂ c₃ : C
d : D
⊢ ((mopEquiv (D ⥤ D)).inverse.map
          (Quiver.Hom.mop { app := fun x ↦ (αₗ c₁ c₂ x).inv, naturality := ⋯ } ▷ (curriedActionMop C D).obj c₃ ≫
            Quiver.Hom.mop { app := fun x ↦ (αₗ (c₁ ⊗ c₂) c₃ x).inv, naturality := ⋯ } ≫
              (curriedActionMop C D).map (α_ c₁ c₂ c₃).hom)).app
      d =
    ((mopEquiv (D ⥤ D)).inverse.map
          ((α_ ((curriedActionMop C D).obj c₁) ((curriedActionMop C D).obj c₂) ((curriedActionMop C D).obj c₃)).hom ≫
            (curriedActionMop C D).obj c₁ ◁ Quiver.Hom.mop { app := fun x ↦ (αₗ c₂ c₃ x).inv, naturality := ⋯ } ≫
              Quiver.Hom.mop { app := fun x ↦ (αₗ c₁ (c₂ ⊗ c₃) x).inv, naturality := ⋯ })).app
      d

Tactic:
simpa [-associator_actionHom] using
      (IsIso.inv_eq_inv.mpr <| associator_actionHom c₁ c₂ c₃ d).symm =≫
        (α_ c₁ c₂ c₃).hom ⊵ₗ d

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasPushouts C
inst✝³ : HasInitial C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : Arrow C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ Arrow.Hom.left ((f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂)) = Arrow.Hom.left (f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂)

Tactic:
apply pushout.hom_ext <;> simp [whisker_exchange_assoc]

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

Goal state before:
pp: case h₀
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasPushouts C
inst✝³ : HasInitial C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
X₁ X₂ X₃ Y₁ Y₂ Y₃ : Arrow C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
⊢ X₁.right ◁ X₂.left ◁ Arrow.Hom.right f₃ ≫
      (α_ X₁.right X₂.left Y₃.right).inv ≫
        Arrow.Hom.right f₁ ▷ X₂.left ▷ Y₃.right ≫
          (α_ Y₁.right X₂.left Y₃.right).hom ≫
            Y₁.right ◁ Arrow.Hom.left f₂ ▷ Y₃.right ≫ Y₁.right ◁ pushout.inr (Y₂.hom ▷ Y₃.left) (Y₂.left ◁ Y₃.hom) =
    Arrow.Hom.right f₁ ▷ (X₂.left ⊗ X₃.right) ≫
      Y₁.right ◁ (X₂.left ◁ Arrow.Hom.right f₃ ≫ Arrow.Hom.left f₂ ▷ Y₃.right) ≫
        Y₁.right ◁ pushout.inr (Y₂.hom ▷ Y₃.left) (Y₂.left ◁ Y₃.hom)

Tactic:
associator_inv_naturality_right_assoc,

Goal state after:
case h₀
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasPushouts C
inst✝³ : HasInitial C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
X₁ X₂ X₃ Y₁ Y₂ Y₃ : Arrow C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
⊢ (α_ X₁.right X₂.left X₃.right).inv ≫
      (X₁.right ⊗ X₂.left) ◁ Arrow.Hom.right f₃ ≫
        Arrow.Hom.right f₁ ▷ X₂.left ▷ Y₃.right ≫
          (α_ Y₁.right X₂.left Y₃.right).hom ≫
            Y₁.right ◁ Arrow.Hom.left f₂ ▷ Y₃.right ≫ Y₁.right ◁ pushout.inr (Y₂.hom ▷ Y₃.left) (Y₂.left ◁ Y₃.hom) =
    Arrow.Hom.right f₁ ▷ (X₂.left ⊗ X₃.right) ≫
      Y₁.right ◁ (X₂.left ◁ Arrow.Hom.right f₃ ≫ Arrow.Hom.left f₂ ▷ Y₃.right) ≫
        Y₁.right ◁ pushout.inr (Y₂.hom ▷ Y₃.left) (Y₂.left ◁ Y₃.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
L : D ⥤ C
inst✝² : MonoidalClosed C
inst✝¹ : MonoidalClosed D
inst✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
h : L ⊣ F
A : C
⊢ (conjugateEquiv (h.comp (ihom.adjunction A)) ((ihom.adjunction (F.obj A)).comp h))
      (natTrans (prodComparisonNatTrans L (F.obj A) ≫ L.whiskerLeft ((curriedTensor C).map (h.counit.app A)))) =
    ((mateEquiv (ihom.adjunction A) (ihom.adjunction (F.obj A))) (prodComparisonNatIso F A).inv).natTrans

Tactic:
have conjeq := iterated_mateEquiv_conjugateEquiv h h
    (ihom.adjunction (F.obj A)) (ihom.adjunction A)
    (prodComparisonNatTrans L (F.obj A) ≫
      Functor.whiskerLeft L ((curriedTensor C).map (h.counit.app A)))

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
L : D ⥤ C
inst✝² : MonoidalClosed C
inst✝¹ : MonoidalClosed D
inst✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
h : L ⊣ F
A : C
conjeq :
  ((mateEquiv (ihom.adjunction A) (ihom.adjunction (F.obj A)))
        ((mateEquiv h h)
          (prodComparisonNatTrans L (F.obj A) ≫ L.whiskerLeft ((curriedTensor C).map (h.counit.app A))))).natTrans =
    (conjugateEquiv (h.comp (ihom.adjunction A)) ((ihom.adjunction (F.obj A)).comp h))
      (prodComparisonNatTrans L (F.obj A) ≫ L.whiskerLeft ((curriedTensor C).map (h.counit.app A)))
⊢ (conjugateEquiv (h.comp (ihom.adjunction A)) ((ihom.adjunction (F.obj A)).comp h))
      (natTrans (prodComparisonNatTrans L (F.obj A) ≫ L.whiskerLeft ((curriedTensor C).map (h.counit.app A)))) =
    ((mateEquiv (ihom.adjunction A) (ihom.adjunction (F.obj A))) (prodComparisonNatIso F A).inv).natTrans
Module: Mathlib.CategoryTheory.Monoidal.Closed.InternalCurrying

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : MonoidalCategory C
x y z : C
inst✝² : Closed x
inst✝¹ : Closed y
inst✝ : Closed (x ⊗ y)
⊢ x ◁ y ◁ ihomUncurry x y z ≫ (α_ x y ((ihom (x ⊗ y)).obj z)).inv ≫ (ihom.ev (x ⊗ y)).app z =
    uncurry ((ihom.ev y).app ((ihom x).obj z))

Tactic:
associator_inv_naturality_right_assoc,

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : MonoidalCategory C
x y z : C
inst✝² : Closed x
inst✝¹ : Closed y
inst✝ : Closed (x ⊗ y)
⊢ (α_ x y ((ihom y).obj ((ihom x).obj z))).inv ≫ (x ⊗ y) ◁ ihomUncurry x y z ≫ (ihom.ev (x ⊗ y)).app z =
    uncurry ((ihom.ev y).app ((ihom x).obj z))
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
⊢ (reflectorAdjunction i).unit.app A ⊗ₘ (reflectorAdjunction i).unit.app B =
    (reflectorAdjunction i).unit.app (A ⊗ B) ≫
      i.map (prodComparison (reflector i) A B) ≫ prodComparison i ((reflector i).obj A) ((reflector i).obj B)

Tactic:
apply hom_ext

Goal state after:
case h_fst
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
⊢ ((reflectorAdjunction i).unit.app A ⊗ₘ (reflectorAdjunction i).unit.app B) ≫
      fst (i.obj ((reflector i).obj A)) (i.obj ((reflector i).obj B)) =
    ((reflectorAdjunction i).unit.app (A ⊗ B) ≫
        i.map (prodComparison (reflector i) A B) ≫ prodComparison i ((reflector i).obj A) ((reflector i).obj B)) ≫
      fst (i.obj ((reflector i).obj A)) (i.obj ((reflector i).obj B))

case h_snd
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
⊢ ((reflectorAdjunction i).unit.app A ⊗ₘ (reflectorAdjunction i).unit.app B) ≫
      snd (i.obj ((reflector i).obj A)) (i.obj ((reflector i).obj B)) =
    ((reflectorAdjunction i).unit.app (A ⊗ B) ≫
        i.map (prodComparison (reflector i) A B) ≫ prodComparison i ((reflector i).obj A) ((reflector i).obj B)) ≫
      snd (i.obj ((reflector i).obj A)) (i.obj ((reflector i).obj B))
Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence

Goal state before:
pp: C : Type u
X✝ Y✝ X' X Y : F C
f : X ⟶ Y
ih :
  ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ f ≫ (normalizeIsoApp' C Y n).hom = (normalizeIsoApp' C X n).hom ≫ inclusion.map (eqToHom ⋯)
n : NormalMonoidalObject C
⊢ inclusionObj n ◁ X' ◁ f ≫
      (α_ (inclusionObj n) X' Y).inv ≫
        (normalizeIsoApp' C X' n).hom ▷ Y ≫ (normalizeIsoApp' C Y (X'.normalizeObj n)).hom =
    ((α_ (inclusionObj n) X' X).inv ≫
        (normalizeIsoApp' C X' n).hom ▷ X ≫ (normalizeIsoApp' C X (X'.normalizeObj n)).hom) ≫
      inclusion.map (eqToHom ⋯)

Tactic:
associator_inv_naturality_right_assoc,

Goal state after:
C : Type u
X✝ Y✝ X' X Y : F C
f : X ⟶ Y
ih :
  ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ f ≫ (normalizeIsoApp' C Y n).hom = (normalizeIsoApp' C X n).hom ≫ inclusion.map (eqToHom ⋯)
n : NormalMonoidalObject C
⊢ (α_ (inclusionObj n) X' X).inv ≫
      (inclusionObj n ⊗ X') ◁ f ≫ (normalizeIsoApp' C X' n).hom ▷ Y ≫ (normalizeIsoApp' C Y (X'.normalizeObj n)).hom =
    ((α_ (inclusionObj n) X' X).inv ≫
        (normalizeIsoApp' C X' n).hom ▷ X ≫ (normalizeIsoApp' C X (X'.normalizeObj n)).hom) ≫
      inclusion.map (eqToHom ⋯)
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
this : Δ ≫ 𝒮 ▷ A ≫ μ ≫ ε = Δ ≫ 𝒮 ▷ A ≫ μ ≫ ε
| Δ ≫ 𝒮 ▷ A ≫ μ ≫ ε = Δ ≫ 𝒮 ▷ A ≫ μ ≫ ε

Tactic:
rhs
    rw [antipode_left_assoc]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
this : Δ ≫ 𝒮 ▷ A ≫ μ ≫ ε = Δ ≫ 𝒮 ▷ A ≫ μ ≫ ε
| ε ≫ η ≫ ε