mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Limits

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{?u.4, u_1} C
I : Type u_2
D : I → Type u_3
inst✝³ : (i : I) → Category.{?u.13, u_3} (D i)
F : (i : I) → C ⥤ D i
hF : JointlyReflectIsomorphisms F
J : Type u_4
inst✝² : Category.{v_1, u_4} J
G : J ⥤ C
c : Cone G
hc : (i : I) → IsLimit ((F i).mapCone c)
inst✝¹ : HasLimit G
inst✝ : ∀ (i : I), PreservesLimit G (F i)
⊢ ∀ (i : I), IsIso ((F i).map (limit.lift G c))

Tactic:
intro i

Goal state after:
C : Type u_1
inst✝⁴ : Category.{?u.4, u_1} C
I : Type u_2
D : I → Type u_3
inst✝³ : (i : I) → Category.{?u.13, u_3} (D i)
F : (i : I) → C ⥤ D i
hF : JointlyReflectIsomorphisms F
J : Type u_4
inst✝² : Category.{v_1, u_4} J
G : J ⥤ C
c : Cone G
hc : (i : I) → IsLimit ((F i).mapCone c)
inst✝¹ : HasLimit G
inst✝ : ∀ (i : I), PreservesLimit G (F i)
i : I
⊢ IsIso ((F i).map (limit.lift G c))
Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Limits

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{?u.4, u_1} C
I : Type u_2
D : I → Type u_3
inst✝³ : (i : I) → Category.{?u.13, u_3} (D i)
F : (i : I) → C ⥤ D i
hF : JointlyReflectIsomorphisms F
J : Type u_4
inst✝² : Category.{v_1, u_4} J
G : J ⥤ C
c : Cocone G
hc : (i : I) → IsColimit ((F i).mapCocone c)
inst✝¹ : HasColimit G
inst✝ : ∀ (i : I), PreservesColimit G (F i)
⊢ ∀ (i : I), IsIso ((F i).map (colimit.desc G c))

Tactic:
intro i

Goal state after:
C : Type u_1
inst✝⁴ : Category.{?u.4, u_1} C
I : Type u_2
D : I → Type u_3
inst✝³ : (i : I) → Category.{?u.13, u_3} (D i)
F : (i : I) → C ⥤ D i
hF : JointlyReflectIsomorphisms F
J : Type u_4
inst✝² : Category.{v_1, u_4} J
G : J ⥤ C
c : Cocone G
hc : (i : I) → IsColimit ((F i).mapCocone c)
inst✝¹ : HasColimit G
inst✝ : ∀ (i : I), PreservesColimit G (F i)
i : I
⊢ IsIso ((F i).map (colimit.desc G c))
Module: Mathlib.CategoryTheory.Galois.Examples

Goal state before:
pp: case h
G : Type u
inst✝² : Group G
X : FintypeCat
inst✝¹ : MulAction G X.obj
inst✝ : MulAction.IsPretransitive G X.obj
h : Nonempty X.obj
Y : Action FintypeCat G
i : Y ⟶ Action.FintypeCat.ofMulAction G X
hm : Mono i
hni : ∀ (a : IsInitial Y), False
y : Y.V.obj
x' : (Action.FintypeCat.ofMulAction G X).V.obj
x : X.obj := (ConcreteCategory.hom i.hom) y
σ : G
hσ : σ • x = x'
⊢ (ConcreteCategory.hom ((Action.FintypeCat.ofMulAction G X).ρ σ)) ((ConcreteCategory.hom i.hom) y) = x'

Tactic:
exact hσ

Goal state after:
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)
g : Aut F
x : Aut F ⧸ ↑V
⊢ (ConcreteCategory.hom
        ((coconeQuotientDiag h u hUinV).pt.ρ g ≫
          FintypeCat.homMk
            (Quotient.lift
              (fun σ ↦ (ConcreteCategory.hom (u.inv ≫ s.ι.app (SingleObj.star (↥↑V ⧸ (↑U).subgroupOf ↑V))).hom) ⟦σ⟧)
              ⋯)))
      x =
    (ConcreteCategory.hom
        (FintypeCat.homMk
            (Quotient.lift
              (fun σ ↦ (ConcreteCategory.hom (u.inv ≫ s.ι.app (SingleObj.star (↥↑V ⧸ (↑U).subgroupOf ↑V))).hom) ⟦σ⟧)
              ⋯) ≫
          s.pt.ρ g))
      x

Tactic:
induction x using Quotient.inductionOn with

Goal state after:
case h
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)
g σ : Aut F
⊢ (ConcreteCategory.hom
        ((coconeQuotientDiag h u hUinV).pt.ρ g ≫
          FintypeCat.homMk
            (Quotient.lift
              (fun σ ↦ (ConcreteCategory.hom (u.inv ≫ s.ι.app (SingleObj.star (↥↑V ⧸ (↑U).subgroupOf ↑V))).hom) ⟦σ⟧)
              ⋯)))
      ⟦σ⟧ =
    (ConcreteCategory.hom
        (FintypeCat.homMk
            (Quotient.lift
              (fun σ ↦ (ConcreteCategory.hom (u.inv ≫ s.ι.app (SingleObj.star (↥↑V ⧸ (↑U).subgroupOf ↑V))).hom) ⟦σ⟧)
              ⋯) ≫
          s.pt.ρ g))
      ⟦σ⟧
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
x : Aut F ⧸ ↑V
⊢ (ConcreteCategory.hom f.hom) x = (ConcreteCategory.hom (coconeQuotientDiagDesc h u hUinV s).hom) x

Tactic:
induction x using Quotient.inductionOn with

Goal state after:
case h
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
σ : Aut F
⊢ (ConcreteCategory.hom f.hom) ⟦σ⟧ = (ConcreteCategory.hom (coconeQuotientDiagDesc h u hUinV s).hom) ⟦σ⟧
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
V : OpenSubgroup (Aut F)
I : Set C
hf : Fintype ↑I
hc : ∀ X ∈ I, IsConnected X
hi : ∀ (σ : Aut F), (∀ (X : ↑I), σ.hom.app ↑X = 𝟙 (F.obj ↑X)) → σ ∈ ↑V
this✝ : ∀ (X : ↑I), IsConnected ↑X
this : ∀ (X : ↑I), Nonempty (F.obj ↑X).obj
hn : Nonempty (F.obj (∏ᶜ fun X ↦ ↑X)).obj
A : C
f : A ⟶ ∏ᶜ fun X ↦ ↑X
hgal : IsGalois A
a : (F.obj A).obj
U : OpenSubgroup (Aut F) := { toSubgroup := MulAction.stabilizer (Aut F) a, isOpen' := ⋯ }
u : (functorToAction F).obj A ≅
  Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ MulAction.stabilizer (Aut F) a)) :=
  fiberIsoQuotientStabilizer A a
hUnormal : (↑U).Normal
σ : Aut F
σinU : σ ∈ U
x : (fun X ↦ X.obj) (Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ MulAction.stabilizer (Aut F) a))).V
⊢ (ConcreteCategory.hom
        ((Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ MulAction.stabilizer (Aut F) a))).ρ σ))
      x =
    (ConcreteCategory.hom
        (𝟙 (Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ MulAction.stabilizer (Aut F) a))).V))
      x

Tactic:
induction x using Quotient.inductionOn with

Goal state after:
case h
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
V : OpenSubgroup (Aut F)
I : Set C
hf : Fintype ↑I
hc : ∀ X ∈ I, IsConnected X
hi : ∀ (σ : Aut F), (∀ (X : ↑I), σ.hom.app ↑X = 𝟙 (F.obj ↑X)) → σ ∈ ↑V
this✝ : ∀ (X : ↑I), IsConnected ↑X
this : ∀ (X : ↑I), Nonempty (F.obj ↑X).obj
hn : Nonempty (F.obj (∏ᶜ fun X ↦ ↑X)).obj
A : C
f : A ⟶ ∏ᶜ fun X ↦ ↑X
hgal : IsGalois A
a : (F.obj A).obj
U : OpenSubgroup (Aut F) := { toSubgroup := MulAction.stabilizer (Aut F) a, isOpen' := ⋯ }
u : (functorToAction F).obj A ≅
  Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ MulAction.stabilizer (Aut F) a)) :=
  fiberIsoQuotientStabilizer A a
hUnormal : (↑U).Normal
σ : Aut F
σinU : σ ∈ U
τ : Aut F
⊢ (ConcreteCategory.hom
        ((Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ MulAction.stabilizer (Aut F) a))).ρ σ))
      ⟦τ⟧ =
    (ConcreteCategory.hom
        (𝟙 (Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ MulAction.stabilizer (Aut F) a))).V))
      ⟦τ⟧
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ ((zeroProdIso X).symm ≪≫ (pullbackZeroZeroIso 0 X).symm).hom ≫ pullback.fst 0 0 = 0

Tactic:
simp [eq_iff_true_of_subsingleton]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
s : Cocone (span 0 (𝟙 X))
⊢ PushoutCocone.inl s ≫ 0 = PushoutCocone.inl s ≫ 𝟙 s.pt

Tactic:
simp [eq_iff_true_of_subsingleton]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ 0 ≫ ((coprodZeroIso X).symm ≪≫ (pushoutZeroZeroIso X 0).symm).hom = pushout.inr 0 0

Tactic:
simp [eq_iff_true_of_subsingleton]

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 = s

Tactic:
by_contra r_ne_s

Goal state after:
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
⊢ False
Module: Mathlib.CategoryTheory.Limits.Types.End

Goal state before:
pp: J✝ : Type u
inst✝¹ : Category.{v, u} J✝
F✝ : J✝ᵒᵖ ⥤ J✝ ⥤ Type (max w u)
J : Type u
inst✝ : Category.{v, u} J
F G : Jᵒᵖ ⥤ J ⥤ Type (max w u)
f : F ⟶ G
x : Types.end_ F
⊢ ∀ ⦃i j : J⦄ (f_1 : i ⟶ j),
    (Hom.hom ((G.obj (op i)).map f_1)) ((fun j ↦ (hom ((f.app (op j)).app j)) (↑x j)) i) =
      (Hom.hom ((G.map f_1.op).app j)) ((fun j ↦ (hom ((f.app (op j)).app j)) (↑x j)) j)

Tactic:
intro i

Goal state after:
J✝ : Type u
inst✝¹ : Category.{v, u} J✝
F✝ : J✝ᵒᵖ ⥤ J✝ ⥤ Type (max w u)
J : Type u
inst✝ : Category.{v, u} J
F G : Jᵒᵖ ⥤ J ⥤ Type (max w u)
f : F ⟶ G
x : Types.end_ F
i : J
⊢ ∀ ⦃j : J⦄ (f_1 : i ⟶ j),
    (Hom.hom ((G.obj (op i)).map f_1)) ((fun j ↦ (hom ((f.app (op j)).app j)) (↑x j)) i) =
      (Hom.hom ((G.map f_1.op).app j)) ((fun j ↦ (hom ((f.app (op j)).app j)) (↑x j)) j)
Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfFunctorialResolutions

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
ρ : C₂ ⥤ C₁
i : 𝟭 C₂ ⟶ ρ ⋙ Φ.functor
hi : ∀ (X₂ : C₂), W₂ (i.app X₂)
hW₁ : W₁ = W₂.inverseImage Φ.functor
inst✝³ : Φ.functor.Full
inst✝² : Φ.functor.Faithful
inst✝¹ : W₂.HasTwoOutOfThreeProperty
inst✝ : W₂.IsMultiplicative
X₂ : C₂
⊢ W₁.IsMultiplicative

Tactic:
by rw [hW₁]; infer_instance

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

Goal state before:
pp: m : Type u → Type u
inst✝¹ : _root_.Monad m
inst✝ : LawfulMonad m
x✝¹ x✝ : Type u
f : x✝¹ ⟶ x✝
⊢ (𝟭 (Type u)).map f ≫ ↾pure = ↾pure ≫ __Functor✝.map f

Tactic:
ext x; exact (LawfulApplicative.map_pure f x).symm

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

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

Tactic:
rw [isIso_iff_bijective, w₁]

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A T : C
hT : IsTerminal T
inst✝ : Mono (hT.from A)
Z : C
f g : Z ⟶ A
⊢ f = g

Tactic:
← cancel_mono (hT.from A)

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A T : C
hT : IsTerminal T
inst✝ : Mono (hT.from A)
Z : C
f g : Z ⟶ A
⊢ f ≫ hT.from A = g ≫ hT.from A
Module: Mathlib.CategoryTheory.Monoidal.Closed.Zero

Goal state before:
pp: case refine_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : HasZeroObject C
X Y : C
this : HasInitial C
⊢ default ≫ default ≫ default = 𝟙 (⊥_ C)

Tactic:
simp [eq_iff_true_of_subsingleton]

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

Goal state before:
pp: case refine_2
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : HasZeroObject C
X Y : C
this : HasInitial C
⊢ (default ≫ default) ≫ default = 𝟙 (𝟙_ C)

Tactic:
simp [eq_iff_true_of_subsingleton]

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) (tensorRight (K.obj e))
cone : Limits.Cocone (CostructuredArrow.proj (L.prod (𝟭 E)) (d, e) ⋙ H ⊠ K) :=
  (Functor.LeftExtension.mk (H' ⊠ K) (extensionUnitLeft H' α K)).coconeAt (d, e)
equiv : CostructuredArrow L d × CostructuredArrow (𝟭 E) e ≌ CostructuredArrow (L.prod (𝟭 E)) (d, e) :=
  (CostructuredArrow.prodEquivalence L (𝟭 E) d e).symm
I : CostructuredArrow L d ⥤ CostructuredArrow L d × CostructuredArrow (𝟭 E) e :=
  (prod.rightUnitorEquivalence (CostructuredArrow L d)).inverse ⋙
    (𝟭 (CostructuredArrow L d)).prod (Functor.fromPUnit (CostructuredArrow.mk (𝟙 ((𝟭 E).obj e))))
⊢ Limits.IsColimit
    (Limits.Cocone.whisker equiv.functor
      ((Functor.LeftExtension.mk (H' ⊠ K) (extensionUnitLeft H' α K)).coconeAt (d, e)))

Tactic:
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.rightUnitorEquivalence <| CostructuredArrow L d).inverse)
      (G := (𝟭 _).prod <| Functor.fromPUnit.{0} (.mk (𝟙 e) : CostructuredArrow (𝟭 E) e))
    infer_instance

Goal state after:
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) (tensorRight (K.obj e))
cone : Limits.Cocone (CostructuredArrow.proj (L.prod (𝟭 E)) (d, e) ⋙ H ⊠ K) :=
  (Functor.LeftExtension.mk (H' ⊠ K) (extensionUnitLeft H' α K)).coconeAt (d, e)
equiv : CostructuredArrow L d × CostructuredArrow (𝟭 E) e ≌ CostructuredArrow (L.prod (𝟭 E)) (d, e) :=
  (CostructuredArrow.prodEquivalence L (𝟭 E) d e).symm
I : CostructuredArrow L d ⥤ CostructuredArrow L d × CostructuredArrow (𝟭 E) e :=
  (prod.rightUnitorEquivalence (CostructuredArrow L d)).inverse ⋙
    (𝟭 (CostructuredArrow L d)).prod (Functor.fromPUnit (CostructuredArrow.mk (𝟙 ((𝟭 E).obj e))))
this : I.Final := isPointwiseLeftKanExtensionAtExtensionUnitLeft._proof_1 d e
⊢ Limits.IsColimit
    (Limits.Cocone.whisker equiv.functor
      ((Functor.LeftExtension.mk (H' ⊠ K) (extensionUnitLeft H' α K)).coconeAt (d, e)))
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.Braided

Goal state before:
pp: C : Type u₁
inst✝¹⁸ : Category.{v₁, u₁} C
V : Type u₂
inst✝¹⁷ : Category.{v₂, u₂} V
inst✝¹⁶ : MonoidalCategory C
inst✝¹⁵ : BraidedCategory C
inst✝¹⁴ : MonoidalCategory V
inst✝¹³ : BraidedCategory V
F G : C ⥤ V
inst✝¹² : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)
inst✝¹¹ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)
H : C ⥤ V
inst✝¹⁰ : DayConvolution F G
inst✝⁹ : DayConvolution G H
inst✝⁸ : DayConvolution F (G ⊛ H)
inst✝⁷ : DayConvolution (F ⊛ G) H
inst✝⁶ : DayConvolution H (F ⊛ G)
inst✝⁵ : DayConvolution H F
inst✝⁴ : DayConvolution (H ⊛ F) G
inst✝³ : DayConvolution H G
inst✝² : DayConvolution F (H ⊛ G)
inst✝¹ : DayConvolution F H
inst✝ : DayConvolution (F ⊛ H) G
⊢ ExternalProduct.extensionUnitRight (G ⊛ H) (unit G H) F ≫
      ((𝟭 C).prod (tensor C)).whiskerLeft
        (unit F (G ⊛ H) ≫
          (tensor C).whiskerLeft ((associator F G H).inv ≫ (braiding (F ⊛ G) H).hom ≫ (associator H F G).inv)) =
    ExternalProduct.extensionUnitRight (G ⊛ H) (unit G H) F ≫
      ((𝟭 C).prod (tensor C)).whiskerLeft
        (unit F (G ⊛ H) ≫
          (tensor C).whiskerLeft (map (𝟙 F) (braiding G H).hom ≫ (associator F H G).inv ≫ map (braiding F H).hom (𝟙 G)))

Tactic:
ext ⟨x, y, z⟩

Goal state after:
C : Type u₁
inst✝¹⁸ : Category.{v₁, u₁} C
V : Type u₂
inst✝¹⁷ : Category.{v₂, u₂} V
inst✝¹⁶ : MonoidalCategory C
inst✝¹⁵ : BraidedCategory C
inst✝¹⁴ : MonoidalCategory V
inst✝¹³ : BraidedCategory V
F G : C ⥤ V
inst✝¹² : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)
inst✝¹¹ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)
H : C ⥤ V
inst✝¹⁰ : DayConvolution F G
inst✝⁹ : DayConvolution G H
inst✝⁸ : DayConvolution F (G ⊛ H)
inst✝⁷ : DayConvolution (F ⊛ G) H
inst✝⁶ : DayConvolution H (F ⊛ G)
inst✝⁵ : DayConvolution H F
inst✝⁴ : DayConvolution (H ⊛ F) G
inst✝³ : DayConvolution H G
inst✝² : DayConvolution F (H ⊛ G)
inst✝¹ : DayConvolution F H
inst✝ : DayConvolution (F ⊛ H) G
x y z : C
⊢ (ExternalProduct.extensionUnitRight (G ⊛ H) (unit G H) F ≫
          ((𝟭 C).prod (tensor C)).whiskerLeft
            (unit F (G ⊛ H) ≫
              (tensor C).whiskerLeft ((associator F G H).inv ≫ (braiding (F ⊛ G) H).hom ≫ (associator H F G).inv))).app
      (x, y, z) =
    (ExternalProduct.extensionUnitRight (G ⊛ H) (unit G H) F ≫
          ((𝟭 C).prod (tensor C)).whiskerLeft
            (unit F (G ⊛ H) ≫
              (tensor C).whiskerLeft
                (map (𝟙 F) (braiding G H).hom ≫ (associator F H G).inv ≫ map (braiding F H).hom (𝟙 G)))).app
      (x, y, z)
Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence

Goal state before:
pp: case mk.comp
C : Type u
X Y X✝ Y✝ Z✝ : F C
f✝ : X✝ ⟶ᵐ Y✝
g✝ : Y✝ ⟶ᵐ Z✝
f_ih✝ : (fun n ↦ X✝.normalizeObj n) = Y✝.normalizeObj
g_ih✝ : (fun n ↦ Y✝.normalizeObj n) = Z✝.normalizeObj
⊢ (fun n ↦ X✝.normalizeObj n) = Z✝.normalizeObj

Tactic:
| comp _ _ _ _ =>

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

Goal state before:
pp: case e'_2
C : Type u
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f : X ⟶ Y
n : NormalMonoidalObject C
e_1✝ :
  (((tensorFunc C).obj X).obj { as := n } ⟶ ((normalize' C).obj Y).obj { as := n }) =
    (inclusionObj n ⊗ X ⟶ inclusionObj (Y.normalizeObj n))
⊢ inclusionObj n ◁ f ≫ (normalizeIsoApp C Y { as := n }).hom = inclusionObj n ◁ f ≫ (normalizeIsoApp' C Y n).hom

Tactic:
rw [normalizeIsoApp_eq]

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

Goal state before:
pp: case e'_3
C : Type u
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f : X ⟶ Y
n : NormalMonoidalObject C
e_1✝ :
  (((tensorFunc C).obj X).obj { as := n } ⟶ ((normalize' C).obj Y).obj { as := n }) =
    (inclusionObj n ⊗ X ⟶ inclusionObj (Y.normalizeObj n))
⊢ (normalizeIsoApp C X { as := n }).hom ≫ eqToHom ⋯ = (normalizeIsoApp' C X n).hom ≫ eqToHom ⋯

Tactic:
rw [normalizeIsoApp_eq]

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

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

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

Tactic:
rw [Iso.hom_inv_id_assoc]

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

case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
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 S T U : Mon C
P : Bimod R S
Q : Bimod S T
L : Bimod T U
| coequalizer.π (TensorBimod.actRight P Q ▷ L.X) ((α_ (TensorBimod.X P Q) T.X L.X).hom ≫ TensorBimod.X P Q ◁ L.actLeft)
Module: Mathlib.CategoryTheory.Monoidal.Limits.Basic

Goal state before:
pp: J : Type w
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimitsOfShape J C
inst✝ : MonoidalCategory C
F G : J ⥤ C
j j' : J
f : j ⟶ j'
⊢ ((Functor.const J).obj (limit F ⊗ limit G)).map f ≫ (limit.π F j' ⊗ₘ limit.π G j') =
    (limit.π F j ⊗ₘ limit.π G j) ≫ (F ⊗ G).map f

Tactic:
by
                dsimp
                simp only [Category.id_comp, tensorHom_comp_tensorHom, limit.w]

Goal state after: