mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Action.Continuous

Goal state before:
pp: V : Type u_1
inst✝⁵ : Category.{v_1, u_1} V
FV : V → V → Type u_2
CV : V → Type u_3
inst✝⁴ : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)
inst✝³ : ConcreteCategory V FV
inst✝² : HasForget₂ V TopCat
G : Type u_4
inst✝¹ : Monoid G
inst✝ : TopologicalSpace G
X : Action V G
g h : G
x : ↑((forget₂ (Action V G) TopCat).obj X)
⊢ (ConcreteCategory.hom ((forget₂ V TopCat).map (X.ρ (g * h)))) x =
    (ConcreteCategory.hom ((forget₂ V TopCat).map (X.ρ h) ≫ (forget₂ V TopCat).map (X.ρ g))) x

Tactic:
rw [← Functor.map_comp, map_mul]

Goal state after:
V : Type u_1
inst✝⁵ : Category.{v_1, u_1} V
FV : V → V → Type u_2
CV : V → Type u_3
inst✝⁴ : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)
inst✝³ : ConcreteCategory V FV
inst✝² : HasForget₂ V TopCat
G : Type u_4
inst✝¹ : Monoid G
inst✝ : TopologicalSpace G
X : Action V G
g h : G
x : ↑((forget₂ (Action V G) TopCat).obj X)
⊢ (ConcreteCategory.hom ((forget₂ V TopCat).map (X.ρ g * X.ρ h))) x =
    (ConcreteCategory.hom ((forget₂ V TopCat).map (X.ρ h ≫ X.ρ g))) x
Module: Mathlib.CategoryTheory.Adjunction.Triple

Goal state before:
pp: case mp
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
H : C ⥤ D
t : Triple F G H
adj : F ⋙ G ⊣ H ⋙ G := ⋯
⊢ IsIso t.adj₁.unit → IsIso t.adj₂.counit

Tactic:
intro h
    let idAdj : 𝟭 C ⊣ H ⋙ G := adj.ofNatIsoLeft (asIso t.adj₁.unit).symm
    exact t.adj₂.isIso_counit_of_iso (idAdj.rightAdjointUniq id)

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Triple

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
F : C ⥤ D
G : D ⥤ C
H : C ⥤ D
t : Triple F G H
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : H.Full
inst✝ : H.Faithful
x✝ : Cᵒᵖ
⊢ t.op.leftToRight.app x✝ = (NatTrans.op t.leftToRight).app x✝

Tactic:
leftToRight,

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
F : C ⥤ D
G : D ⥤ C
H : C ⥤ D
t : Triple F G H
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : H.Full
inst✝ : H.Faithful
x✝ : Cᵒᵖ
⊢ (H.op.rightUnitor.inv ≫
          H.op.whiskerLeft t.op.adj₂.unit ≫
            (H.op.associator G.op F.op).inv ≫ inv (whiskerRight t.op.adj₁.unit F.op) ≫ F.op.leftUnitor.hom).app
      x✝ =
    (NatTrans.op t.leftToRight).app x✝
Module: Mathlib.CategoryTheory.Category.Cat.Adjunction

Goal state before:
pp: X : Type u
C : Cat
x✝ : Cat
x : ConnectedComponents ↑x✝
⊢ (ConcreteCategory.hom (↾(𝟙 x✝).toFunctor.mapConnectedComponents)).toFun x =
    (ConcreteCategory.hom (𝟙 (ConnectedComponents ↑x✝))).toFun x

Tactic:
simpa using (Quotient.exists_rep x).elim (fun _ h ↦ by subst h; rfl)

Goal state after:
Module: Mathlib.CategoryTheory.Category.PartialFun

Goal state before:
pp: X : PartialFun
a : (partialFunToPointed ⋙ pointedToPartialFun).obj X
⊢ (fun a ↦ ⟨some a, ⋯⟩) ((fun a ↦ Option.get ↑a ⋯) a) = a

Tactic:
simp only [some_get, Subtype.coe_eta]

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α →. γ
g : β →. δ
⊢ (f.comp ↑Prod.fst).prodLift (g.comp ↑Prod.snd) = f.prodMap g

Tactic:
by
  aesop

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
⊢ (PFun.id α).prodMap (PFun.id β) = PFun.id (α × β)

Tactic:
by
  aesop

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.OfColimitCommutesFiniteLimit

Goal state before:
pp: K : Type v
inst✝ : SmallCategory K
h :
  ∀ {J : Type v} [inst : SmallCategory J] [FinCategory J] (F : J ⥤ K ⥤ Type v),
    Nonempty (limit (colimit F.flip) ⟶ colimit (limit F))
J : Type v
x✝¹ : SmallCategory J
x✝ : FinCategory J
F : J ⥤ K
this : Nonempty (limit (colimit (F.op ⋙ coyoneda).flip))
⊢ ∃ X, Nonempty (limit (F.op ⋙ yoneda.obj X))

Tactic:
by
    obtain ⟨X, y, -⟩ := Types.jointly_surjective' (this.map (h (F.op ⋙ coyoneda)).some).some
    exact ⟨X, ⟨(limitObjIsoLimitCompEvaluation (F.op ⋙ coyoneda) _).hom y⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.Grothendieck

Goal state before:
pp: 𝒮 : Type u_1
inst✝ : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
S : 𝒮
⊢ (Fiber.inducedFunctor ⋯).EssSurj

Tactic:
by
  apply essSurj_of_surj
  intro Y
  have hYS : (fiberInclusion.obj Y).base = S := by simpa using! Y.2
  use hYS ▸ (fiberInclusion.obj Y).fiber
  apply fiberInclusion_obj_inj
  ext <;> simp [hYS]

Goal state after:
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
inst✝⁶ : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ : J ⥤ C
inst✝⁵ : HasFunctorEnrichedHom V F₁ F₂
inst✝⁴ : HasEnrichedHom V F₁ F₂
inst✝³ : HasFunctorEnrichedHom V F₂ F₃
inst✝² : HasEnrichedHom V F₂ F₃
inst✝¹ : HasFunctorEnrichedHom V F₁ F₃
inst✝ : HasEnrichedHom V F₁ F₃
f : F₁ ⟶ F₂
g : F₂ ⟶ F₃
⊢ (functorHomEquiv V) (f ≫ g) =
    (λ_ (𝟙_ (J ⥤ V))).inv ≫ ((functorHomEquiv V) f ⊗ₘ (functorHomEquiv V) g) ≫ functorEnrichedComp V F₁ F₂ F₃

Tactic:
by
  ext j
  dsimp
  ext k
  rw [homEquiv_comp, assoc, assoc, assoc, assoc, assoc, end_.lift_π, enrichedComp_π]
  simp [tensorHom_comp_tensorHom_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Derived.LeftDerived

Goal state before:
pp: C : Type u_1
H : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_5, u_2} H
F F' : C ⥤ H
e : F ≅ F'
W : MorphismProperty C
⊢ W.Q.HasRightKanExtension F ↔ W.Q.HasRightKanExtension F'

Tactic:
hasRightExtension_iff_of_iso₂ W.Q e

Goal state after:
C : Type u_1
H : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_5, u_2} H
F F' : C ⥤ H
e : F ≅ F'
W : MorphismProperty C
⊢ W.Q.HasRightKanExtension F' ↔ W.Q.HasRightKanExtension F'
Module: Mathlib.CategoryTheory.Galois.Examples

Goal state before:
pp: G : Type u
inst✝ : Group G
X Y : Action FintypeCat G
f : X ⟶ Y
⊢ Function.Injective ⇑(ConcreteCategory.hom ((forget (Action FintypeCat G)).map (Action.imageComplementIncl G f)))

Tactic:
exact Subtype.val_injective

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
F : C ⥤ FintypeCat
inst✝³ : GaloisCategory C
inst✝² : FiberFunctor F
X : C
Y : Action FintypeCat (Aut F)
i : Y ⟶ (functorToAction F).obj X
inst✝¹ : Mono i
inst✝ : IsConnected Y
y : ((forget₂ (Action FintypeCat (Aut F)) FintypeCat).obj Y).obj
⊢ ∃ Z f u, IsConnected Z ∧ Mono f ∧ i = u.hom ≫ (functorToAction F).map f

Tactic:
obtain ⟨Z, f, z, hz, hc, hm⟩ := fiber_in_connected_component F X (i.hom y)

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
F : C ⥤ FintypeCat
inst✝³ : GaloisCategory C
inst✝² : FiberFunctor F
X : C
Y : Action FintypeCat (Aut F)
i : Y ⟶ (functorToAction F).obj X
inst✝¹ : Mono i
inst✝ : IsConnected Y
y : ((forget₂ (Action FintypeCat (Aut F)) FintypeCat).obj Y).obj
Z : C
f : Z ⟶ X
z : (F.obj Z).obj
hz : (ConcreteCategory.hom (F.map f)) z = (ConcreteCategory.hom i.hom) y
hc : IsConnected Z
hm : Mono f
⊢ ∃ Z f u, IsConnected Z ∧ Mono f ∧ i = u.hom ≫ (functorToAction F).map f
Module: Mathlib.CategoryTheory.Galois.Decomposition

Goal state before:
pp: case h.left
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
h1 : (ConcreteCategory.hom (F.map u)) a = mkSelfProdFib F X
h2 : IsConnected A
h3 : Mono u
⊢ IsGalois A

pp: case h.right
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
h1 : (ConcreteCategory.hom (F.map u)) a = mkSelfProdFib F X
h2 : IsConnected A
h3 : Mono u
⊢ Function.Bijective fun f ↦ (ConcreteCategory.hom (F.map f)) a

Tactic:
· refine (isGalois_iff_pretransitive F A).mpr ⟨fun x y ↦ ?_⟩
    obtain ⟨fi1, hfi1⟩ := subobj_selfProd_trans h1 x
    obtain ⟨fi2, hfi2⟩ := subobj_selfProd_trans h1 y
    use fi1 ≪≫ fi2.symm
    change F.map (fi1.hom ≫ fi2.inv) x = y
    simp only [map_comp, FintypeCat.comp_apply]
    rw [hfi1, ← hfi2]
    exact ConcreteCategory.congr_hom (F.mapIso fi2).hom_inv_id y

Goal state after:
case h.right
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
h1 : (ConcreteCategory.hom (F.map u)) a = mkSelfProdFib F X
h2 : IsConnected A
h3 : Mono u
⊢ Function.Bijective fun f ↦ (ConcreteCategory.hom (F.map f)) a
Module: Mathlib.CategoryTheory.Galois.Decomposition

Goal state before:
pp: case h.right
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
h1 : (ConcreteCategory.hom (F.map u)) a = mkSelfProdFib F X
h2 : IsConnected A
h3 : Mono u
⊢ Function.Surjective fun f ↦ (ConcreteCategory.hom (F.map f)) a

Tactic:
intro x

Goal state after:
case h.right
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
h1 : (ConcreteCategory.hom (F.map u)) a = mkSelfProdFib F X
h2 : IsConnected A
h3 : Mono u
x : (F.obj X).obj
⊢ ∃ a_1, (fun f ↦ (ConcreteCategory.hom (F.map f)) a) a_1 = x
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
⊢ MulAction.IsPretransitive (Aut F) (F.obj X).obj

Tactic:
have hs : Function.Surjective (F.map f) := surjective_of_nonempty_fiber_of_isConnected F 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
A : C
f : A ⟶ X
hgal : IsGalois A
hs : Function.Surjective ⇑(ConcreteCategory.hom (F.map f))
⊢ MulAction.IsPretransitive (Aut F) (F.obj X).obj
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x✝¹ x✝ : C
h : (of C).obj x✝¹ = (of C).obj x✝
⊢ x✝¹ = x✝

Tactic:
by cases h; rfl

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ map (𝟭 C) = 𝟭 (FreeGroupoid C)

Tactic:
symm; apply lift_unique; rfl

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
E : Type u₂
inst✝ : Category.{v₂, u₂} E
φ : C ⥤ D
φ' : D ⥤ E
⊢ map (φ ⋙ φ') = map φ ⋙ map φ'

Tactic:
symm; apply lift_unique; rfl

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ Type w
x✝¹ : Cone (pair F G)
x✝ : x✝¹.pt ⟶ (binaryProductCone F G).pt
h : ∀ (j : Discrete WalkingPair), x✝ ≫ (binaryProductCone F G).π.app j = x✝¹.π.app j
⊢ x✝ = prod.lift (BinaryFan.fst x✝¹) (BinaryFan.snd x✝¹)

Tactic:
by
    simp only [← h ⟨WalkingPair.right⟩, ← h ⟨WalkingPair.left⟩]
    congr

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

Goal state before:
pp: C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := ⋯
α : Cardinal.{u} := ⋯
yp : C := ⋯
⊢ (X ⟶ yp) → md

Tactic:
intro f
        exact ⟨_, _, f⟩

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits

Goal state before:
pp: J : Type u_1
J' : Type u_2
C : Type u_3
D : Type u_4
K : Type u_5
K' : Type u_6
inst✝⁵ : Category.{v_1, u_5} K
inst✝⁴ : Category.{v_2, u_6} K'
inst✝³ : Category.{v_3, u_1} J
inst✝² : Category.{v_4, u_2} J'
inst✝¹ : Category.{v_5, u_3} C
inst✝ : Category.{v_6, u_4} D
⊢ (preservesColimitsOfShape K).IsClosedUnderIsomorphisms

Tactic:
rw [preservesColimitsOfShape_eq_iSup]
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Pi

Goal state before:
pp: case h_empty
C : PEmpty.{w + 1} → Type u₁
⊢ ∀ {D : PEmpty.{w + 1} → Type u₂} [inst : (j : PEmpty.{w + 1}) → Category.{v₁, u₁} (C j)]
    [inst_1 : (j : PEmpty.{w + 1}) → Category.{v₂, u₂} (D j)] (L : (j : PEmpty.{w + 1}) → C j ⥤ D j)
    (W : (j : PEmpty.{w + 1}) → MorphismProperty (C j)) [∀ (j : PEmpty.{w + 1}), (W j).ContainsIdentities]
    [∀ (j : PEmpty.{w + 1}), (L j).IsLocalization (W j)], (Functor.pi L).IsLocalization (MorphismProperty.pi W)

Tactic:
D

Goal state after:
case h_empty
C : PEmpty.{w + 1} → Type u₁
D : PEmpty.{w + 1} → Type u₂
⊢ ∀ [inst : (j : PEmpty.{w + 1}) → Category.{v₁, u₁} (C j)] [inst_1 : (j : PEmpty.{w + 1}) → Category.{v₂, u₂} (D j)]
    (L : (j : PEmpty.{w + 1}) → C j ⥤ D j) (W : (j : PEmpty.{w + 1}) → MorphismProperty (C j))
    [∀ (j : PEmpty.{w + 1}), (W j).ContainsIdentities] [∀ (j : PEmpty.{w + 1}), (L j).IsLocalization (W j)],
    (Functor.pi L).IsLocalization (MorphismProperty.pi W)
Module: Mathlib.CategoryTheory.Localization.Pi

Goal state before:
pp: case h_option
J : Type w
inst✝ : Fintype J
hJ :
  ∀ {C : J → Type u₁} {D : J → Type u₂} [inst : (j : J) → Category.{v₁, u₁} (C j)]
    [inst_1 : (j : J) → Category.{v₂, u₂} (D j)] (L : (j : J) → C j ⥤ D j) (W : (j : J) → MorphismProperty (C j))
    [∀ (j : J), (W j).ContainsIdentities] [∀ (j : J), (L j).IsLocalization (W j)],
    (Functor.pi L).IsLocalization (MorphismProperty.pi W)
C : Option J → Type u₁
⊢ ∀ {D : Option J → Type u₂} [inst : (j : Option J) → Category.{v₁, u₁} (C j)]
    [inst_1 : (j : Option J) → Category.{v₂, u₂} (D j)] (L : (j : Option J) → C j ⥤ D j)
    (W : (j : Option J) → MorphismProperty (C j)) [∀ (j : Option J), (W j).ContainsIdentities]
    [∀ (j : Option J), (L j).IsLocalization (W j)], (Functor.pi L).IsLocalization (MorphismProperty.pi W)

Tactic:
D

Goal state after:
case h_option
J : Type w
inst✝ : Fintype J
hJ :
  ∀ {C : J → Type u₁} {D : J → Type u₂} [inst : (j : J) → Category.{v₁, u₁} (C j)]
    [inst_1 : (j : J) → Category.{v₂, u₂} (D j)] (L : (j : J) → C j ⥤ D j) (W : (j : J) → MorphismProperty (C j))
    [∀ (j : J), (W j).ContainsIdentities] [∀ (j : J), (L j).IsLocalization (W j)],
    (Functor.pi L).IsLocalization (MorphismProperty.pi W)
C : Option J → Type u₁
D : Option J → Type u₂
⊢ ∀ [inst : (j : Option J) → Category.{v₁, u₁} (C j)] [inst_1 : (j : Option J) → Category.{v₂, u₂} (D j)]
    (L : (j : Option J) → C j ⥤ D j) (W : (j : Option J) → MorphismProperty (C j))
    [∀ (j : Option J), (W j).ContainsIdentities] [∀ (j : Option J), (L j).IsLocalization (W j)],
    (Functor.pi L).IsLocalization (MorphismProperty.pi W)
Module: Mathlib.CategoryTheory.Localization.Monoidal.Braided

Goal state before:
pp: case refine_1
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝³ : MonoidalCategory C
inst✝² : W.IsMonoidal
inst✝¹ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
inst✝ : BraidedCategory C
⊢ (curriedAssociatorNatIso (LocalizedMonoidal L W ε)).hom ≫
      ofBifunctor.Forward.firstMap₂ (braidingNatIso L W ε) ≫ ofBifunctor.Forward.firstMap₃ (LocalizedMonoidal L W ε) =
    ofBifunctor.Forward.secondMap₁ (braidingNatIso L W ε) ≫
      ofBifunctor.Forward.secondMap₂ (LocalizedMonoidal L W ε) ≫ ofBifunctor.Forward.secondMap₃ (braidingNatIso L W ε)

pp: case refine_2
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝³ : MonoidalCategory C
inst✝² : W.IsMonoidal
inst✝¹ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
inst✝ : BraidedCategory C
⊢ (curriedAssociatorNatIso (LocalizedMonoidal L W ε)).inv ≫
      ofBifunctor.Reverse.firstMap₂ (braidingNatIso L W ε) ≫ ofBifunctor.Reverse.firstMap₃ (LocalizedMonoidal L W ε) =
    ofBifunctor.Reverse.secondMap₁ (braidingNatIso L W ε) ≫
      ofBifunctor.Reverse.secondMap₂ (LocalizedMonoidal L W ε) ≫ ofBifunctor.Reverse.secondMap₃ (braidingNatIso L W ε)

Tactic:
· apply natTrans₃_ext (L') (L') (L') W W W
    simpa using! map_hexagon_forward _ _ _

Goal state after:
case refine_2
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝³ : MonoidalCategory C
inst✝² : W.IsMonoidal
inst✝¹ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
inst✝ : BraidedCategory C
⊢ (curriedAssociatorNatIso (LocalizedMonoidal L W ε)).inv ≫
      ofBifunctor.Reverse.firstMap₂ (braidingNatIso L W ε) ≫ ofBifunctor.Reverse.firstMap₃ (LocalizedMonoidal L W ε) =
    ofBifunctor.Reverse.secondMap₁ (braidingNatIso L W ε) ≫
      ofBifunctor.Reverse.secondMap₂ (LocalizedMonoidal L W ε) ≫ ofBifunctor.Reverse.secondMap₃ (braidingNatIso L W ε)
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Sections

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
I : C
inst✝² : Closed I
inst✝¹ : ChosenPullbacksAlong (curryRightUnitorHom I)
inst✝ : BraidedCategory C
A : C
⊢ ∀ {Y Y' : Over I} (f : (toOver I).obj A ⟶ Y) (g : Y ⟶ Y'),
    { toFun := sectionsCurry, invFun := sectionsUncurry, left_inv := ⋯, right_inv := ⋯ } (f ≫ g) =
      { toFun := sectionsCurry, invFun := sectionsUncurry, left_inv := ⋯, right_inv := ⋯ } f ≫ (sections I).map g

Tactic:
X'

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
I : C
inst✝² : Closed I
inst✝¹ : ChosenPullbacksAlong (curryRightUnitorHom I)
inst✝ : BraidedCategory C
A : C
X' : Over I
⊢ ∀ {Y' : Over I} (f : (toOver I).obj A ⟶ X') (g : X' ⟶ Y'),
    { toFun := sectionsCurry, invFun := sectionsUncurry, left_inv := ⋯, right_inv := ⋯ } (f ≫ g) =
      { toFun := sectionsCurry, invFun := sectionsUncurry, left_inv := ⋯, right_inv := ⋯ } f ≫ (sections I).map g
Module: Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor

Goal state before:
pp: D : Type u_1
D' : Type u_2
inst✝⁶ : Category.{v_1, u_1} D
inst✝⁵ : Category.{v_2, u_2} D'
F : D ⥤ D'
C : Type u_3
inst✝⁴ : Category.{v_3, u_3} C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalLeftAction C D
inst✝¹ : MonoidalLeftAction C D'
inst✝ : F.LaxLeftLinear C
c c' : C
d : D
⊢ c ⊴ₗ μₗ F c' d ≫ μₗ F c (c' ⊙ₗ d) ≫ F.map (αₗ c c' d).inv = (αₗ c c' (F.obj d)).inv ≫ μₗ F (c ⊗ c') d

Tactic:
simpa [-μₗ_associativity, -μₗ_associativity_assoc] using
    (αₗ _ _ _).inv ≫=
      (μₗ_associativity F c c' d).symm =≫
      F.map (αₗ _ _ _).inv

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✝ : MonoidalLeftAction C D
w x : C
y z : D
f : w ⟶ x
g : y ⟶ z
⊢ w ⊴ₗ g ≫ f ⊵ₗ z = f ⊵ₗ y ≫ x ⊴ₗ g

Tactic:
simp only [← id_actionHom, ← actionHom_id, ← actionHom_comp, id_comp, comp_id]

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
w x : D
y z : C
f : w ⟶ x
g : y ⟶ z
⊢ w ⊴ᵣ g ≫ f ⊵ᵣ z = f ⊵ᵣ y ≫ x ⊴ᵣ g

Tactic:
simp only [← id_actionHom, ← actionHom_id, ← actionHom_comp, id_comp, comp_id]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.ExternalProduct.KanExtension

Goal state before:
pp: V : Type u₁
inst✝⁵ : Category.{v₁, u₁} V
inst✝⁴ : MonoidalCategory V
D : Type u₂
D' : Type u₃
E : Type u₄
inst✝³ : Category.{v₂, u₂} D
inst✝² : Category.{v₃, u₃} D'
inst✝¹ : Category.{v₄, u₄} E
H : D ⥤ V
L : D ⥤ D'
H' : D' ⥤ V
α : H ⟶ L ⋙ H'
K : E ⥤ V
d : D'
P : (Functor.LeftExtension.mk H' α).IsPointwiseLeftKanExtensionAt d
e : E
inst✝ : Limits.PreservesColimitsOfShape (CostructuredArrow L d) (tensorLeft (K.obj e))
⊢ (Functor.LeftExtension.mk (K ⊠ H') (extensionUnitRight H' α K)).IsPointwiseLeftKanExtensionAt (e, d)

Tactic:
set cone := Functor.LeftExtension.mk (K ⊠ H')
    (extensionUnitRight H' α K) |>.coconeAt (e, d)
  let equiv := CostructuredArrow.prodEquivalence (𝟭 E) L e d |>.symm
  apply Limits.IsColimit.ofWhiskerEquivalence equiv
  let I : CostructuredArrow L d ⥤ CostructuredArrow (𝟭 E) e × CostructuredArrow L d :=
    -- this definition makes it easier to prove finality of I
    (prod.leftUnitorEquivalence <| CostructuredArrow L d).inverse ⋙
      (Functor.fromPUnit.{0} <| .mk <| 𝟙 _).prod (𝟭 _)
  letI : I.Final := by
    let : Functor.fromPUnit.{0} (.mk (𝟙 e) : CostructuredArrow (𝟭 E) e) |>.Final :=
      Functor.final_fromPUnit_of_isTerminal <| CostructuredArrow.mkIdTerminal (S := 𝟭 E) (Y := e)
    apply Iff.mp <| Functor.final_iff_final_comp
      (F := (prod.leftUnitorEquivalence <| CostructuredArrow L d).inverse)
      (G := Functor.fromPUnit.{0} (.mk (𝟙 e) : CostructuredArrow (𝟭 E) e) |>.prod <| 𝟭 _)
    infer_instance
  apply Functor.Final.isColimitWhiskerEquiv I (Limits.Cocone.whisker equiv.functor cone) |>.toFun
  -- through all the equivalences above, the new cocone we consider is in fact
  -- `(tensorLeft <| K.obj e).mapCocone <| (Functor.LeftExtension.mk H' α).coconeAt d`
  let diag_iso :
      (CostructuredArrow.proj L d ⋙ H) ⋙ tensorLeft (K.obj e) ≅
      I ⋙ equiv.functor ⋙ CostructuredArrow.proj (𝟭 E |>.prod L) (e, d) ⋙ K ⊠ H :=
    NatIso.ofComponents (fun _ ↦ Iso.refl _)
  apply Limits.IsColimit.equivOfNatIsoOfIso diag_iso
    (d := Limits.Cocone.whisker I <| Limits.Cocone.whisker equiv.functor cone)
    (c := (tensorLeft <| K.obj e).mapCocone <| (Functor.LeftExtension.mk H' α).coconeAt d)
    (Limits.Cocone.ext <| .refl _) |>.toFun
  exact Limits.PreservesColimit.preserves (F := tensorLeft <| K.obj e) P |>.some

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

Goal state before:
pp: C : Type u
Z : F C
n n' : (Discrete ∘ NormalMonoidalObject) C
f : n ⟶ n'
⊢ ((tensorFunc C).obj Z).map f = inclusion.map f ▷ Z

Tactic:
by
  cases n
  cases n'
  rcases f with ⟨⟨h⟩⟩
  dsimp at h
  subst h
  simp

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Ind

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
H : P ≤ isFinitelyPresentable C
inst✝ : IsFinitelyAccessibleCategory C
X : C
hfac : ∀ {Z : C} (g : Z ⟶ X) [IsFinitelyPresentable Z], ∃ W u v, u ≫ v = g ∧ P W
⊢ P.ind X

Tactic:
let incl : P.FullSubcategory ⥤ (isFinitelyPresentable.{w} C).FullSubcategory :=
      ObjectProperty.ιOfLE H
    have H (d : CostructuredArrow (isFinitelyPresentable.{w} C).ι X) : ∃ c,
        Nonempty (d ⟶ (CostructuredArrow.pre incl (isFinitelyPresentable.{w} C).ι X).obj c) := by
      obtain ⟨W, u, v, huv, hW⟩ := hfac d.hom
      exact ⟨CostructuredArrow.mk (Y := FullSubcategory.mk _ hW) v,
        ⟨CostructuredArrow.homMk ⟨u⟩ huv⟩⟩
    have : (CostructuredArrow.pre incl (isFinitelyPresentable.{w} C).ι X).Final :=
      Functor.final_of_exists_of_isFiltered_of_fullyFaithful (C := CostructuredArrow (incl ⋙ _) X)
        (CostructuredArrow.pre incl (isFinitelyPresentable.{w} C).ι X) H
    have : IsFiltered (CostructuredArrow P.ι X) :=
      .of_exists_of_isFiltered_of_fullyFaithful (C := CostructuredArrow (incl ⋙ _) X)
        (CostructuredArrow.pre incl (isFinitelyPresentable.{w} C).ι X) H
    obtain ⟨hc⟩ : P.ι.isDenseAt X :=
      Functor.IsDenseAt.of_final (F := (isFinitelyPresentable.{w} C).ι) incl
        (Functor.IsDense.isDenseAt _ _)
    have : EssentiallySmall.{w} (CostructuredArrow P.ι X) :=
      essentiallySmall_of_fully_faithful (C := CostructuredArrow (incl ⋙ _) X)
        (CostructuredArrow.pre incl (isFinitelyPresentable.{w} C).ι X)
    exact of_essentiallySmall_index ⟨_, _, hc⟩ fun Y ↦ Y.left.2

Goal state after: