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
x✝² x✝¹ : (PointedGaloisObject F)ᵒᵖ
A : C
a : (F.obj A).obj
isGalois✝¹ : IsGalois A
B : C
b : (F.obj B).obj
isGalois✝ : IsGalois B
x✝ :
  Opposite.op { obj := A, pt := a, isGalois := isGalois✝¹ } ⟶ Opposite.op { obj := B, pt := b, isGalois := isGalois✝ }
f :
  (Opposite.unop (Opposite.op { obj := B, pt := b, isGalois := isGalois✝ })).obj ⟶
    (Opposite.unop (Opposite.op { obj := A, pt := a, isGalois := isGalois✝¹ })).obj
hf : (ConcreteCategory.hom (F.map f)) b = a
⊢ (((incl F).op ⋙ coyoneda).map (Opposite.op { val := f, comp := hf }) ≫
      match Opposite.op { obj := B, pt := b, isGalois := isGalois✝ } with
      | Opposite.op { obj := A, pt := a, isGalois := isGalois } =>
        { app := fun X ↦ ↾fun f ↦ (ConcreteCategory.hom (F.map f)) a, naturality := ⋯ }) =
    (match Opposite.op { obj := A, pt := a, isGalois := isGalois✝¹ } with
      | Opposite.op { obj := A, pt := a, isGalois := isGalois } =>
        { app := fun X ↦ ↾fun f ↦ (ConcreteCategory.hom (F.map f)) a, naturality := ⋯ }) ≫
      ((const (PointedGaloisObject F)ᵒᵖ).obj (F ⋙ FintypeCat.incl)).map (Opposite.op { val := f, comp := hf })

Tactic:
by
      ext Y (g : (A : C) ⟶ Y)
      suffices h : F.map g (F.map f b) = F.map g a by simpa
      rw [hf]

Goal state after:
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
⊢ t = s

Tactic:
change id t = id s

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
⊢ id t = id s
Module: Mathlib.CategoryTheory.Galois.Topology

Goal state before:
pp: C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
X : C
⊢ Continuous fun p ↦ p.1 • p.2

Tactic:
let g : Aut (F.obj X) × F.obj X → F.obj X := fun ⟨σ, x⟩ ↦ σ.hom x

Goal state after:
C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
X : C
g : Aut (F.obj X) × (F.obj X).obj → (F.obj X).obj :=
  fun x ↦
    match x with
    | (σ, x) => (ConcreteCategory.hom σ.hom) x
⊢ Continuous fun p ↦ p.1 • p.2
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
⊢ MulAction.IsPretransitive (Aut F) (F.obj X).obj

Tactic:
obtain ⟨A, f, hgal⟩ := exists_hom_from_galois_of_connected F X
  have hs : Function.Surjective (F.map f) := surjective_of_nonempty_fiber_of_isConnected F f
  refine ⟨fun x y ↦ ?_⟩
  obtain ⟨a, ha⟩ := hs x
  obtain ⟨b, hb⟩ := hs y
  have : MulAction.IsPretransitive (Aut F) (F.obj A) := isPretransitive_of_isGalois F A
  obtain ⟨σ, (hσ : σ.hom.app A a = b)⟩ := MulAction.exists_smul_eq (Aut F) a b
  use σ
  rw [← ha, ← hb]
  change (F.map f ≫ σ.hom.app X) a = F.map f b
  rw [σ.hom.naturality, FintypeCat.comp_apply, hσ]

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

Goal state before:
pp: G : Type u₁
inst✝ : Groupoid G
⊢ lift (𝟭 G) ⋙ of G = 𝟭 (FreeGroupoid G)

Tactic:
by
  rw [lift_unique (of G) (lift (𝟭 G) ⋙ of G) (by rw [← Functor.assoc, lift_spec, Functor.id_comp])]
  symm; apply lift_unique
  rw [Functor.comp_id]

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

Goal state before:
pp: C✝ : Type u
inst✝ : Category.{v, u} C✝
C : Cat
⊢ map (𝟙 C).toFunctor = 𝟙 (of (FreeGroupoid ↑C))

Tactic:
by simp [map_id, id_eq_id]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasFiniteProducts C
U : FormalCoproduct C
T : C
hT : IsTerminal T
⊢ (𝟭 (SimplicialObject (FormalCoproduct C))).map (U.cechIsoCechNerve hT).hom ≫
      (Arrow.mk ((isTerminalIncl T hT).from U)).augmentedCechNerve.hom =
    (U.cech.augmentOfIsTerminal (isTerminalIncl T hT)).hom ≫
      (SimplicialObject.const (FormalCoproduct C)).map
        (Iso.refl (U.cech.augmentOfIsTerminal (isTerminalIncl T hT)).right).hom

Tactic:
ext : 1

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasFiniteProducts C
U : FormalCoproduct C
T : C
hT : IsTerminal T
n✝ : SimplexCategoryᵒᵖ
⊢ ((𝟭 (SimplicialObject (FormalCoproduct C))).map (U.cechIsoCechNerve hT).hom ≫
          (Arrow.mk ((isTerminalIncl T hT).from U)).augmentedCechNerve.hom).app
      n✝ =
    ((U.cech.augmentOfIsTerminal (isTerminalIncl T hT)).hom ≫
          (SimplicialObject.const (FormalCoproduct C)).map
            (Iso.refl (U.cech.augmentOfIsTerminal (isTerminalIncl T hT)).right).hom).app
      n✝
Module: Mathlib.CategoryTheory.Join.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
a b c d : C ⋆ D
f : a.Hom b
g : b.Hom c
h : c.Hom d
⊢ comp (comp f g) h = comp f (comp g h)

Tactic:
by
    cases a <;>
    cases b <;>
    cases c <;>
    cases d <;>
    simp only [Hom, comp, Category.assoc] <;>
    tauto

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasFiniteProducts C
X✝ Y✝ Z✝ : FormalCoproduct C
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ { app := fun x ↦ powerMap (x✝¹ ≫ x✝) (ToType (Opposite.unop x)), naturality := ⋯ } =
    { app := fun x ↦ powerMap x✝¹ (ToType (Opposite.unop x)), naturality := ⋯ } ≫
      { app := fun x ↦ powerMap x✝ (ToType (Opposite.unop x)), naturality := ⋯ }

Tactic:
ext : 1

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasFiniteProducts C
X✝ Y✝ Z✝ : FormalCoproduct C
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
n✝ : SimplexCategoryᵒᵖ
⊢ { app := fun x ↦ powerMap (x✝¹ ≫ x✝) (ToType (Opposite.unop x)), naturality := ⋯ }.app n✝ =
    ({ app := fun x ↦ powerMap x✝¹ (ToType (Opposite.unop x)), naturality := ⋯ } ≫
          { app := fun x ↦ powerMap x✝ (ToType (Opposite.unop x)), naturality := ⋯ }).app
      n✝
Module: Mathlib.CategoryTheory.Join.Basic

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
E' : Type u₄
inst✝² : Category.{v₄, u₄} E'
J : Type u₅
inst✝¹ : Category.{v₅, u₅} J
K : Type u₆
inst✝ : Category.{v₆, u₆} K
Fₗ : C ⥤ E
Fᵣ : D ⥤ E'
Gₗ : E ⥤ J
Gᵣ : E' ⥤ K
c : C
⊢ (mapPairComp Fₗ Fᵣ Gₗ Gᵣ).hom.app (left c) = 𝟙 (left (Gₗ.obj (Fₗ.obj c)))

Tactic:
by
  dsimp [mapPairComp]
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Join.Basic

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
E' : Type u₄
inst✝² : Category.{v₄, u₄} E'
J : Type u₅
inst✝¹ : Category.{v₅, u₅} J
K : Type u₆
inst✝ : Category.{v₆, u₆} K
Fₗ : C ⥤ E
Fᵣ : D ⥤ E'
Gₗ : E ⥤ J
Gᵣ : E' ⥤ K
d : D
⊢ (mapPairComp Fₗ Fᵣ Gₗ Gᵣ).hom.app (right d) = 𝟙 (right (Gᵣ.obj (Fᵣ.obj d)))

Tactic:
by
  dsimp [mapPairComp]
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Join.Basic

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
E' : Type u₄
inst✝² : Category.{v₄, u₄} E'
J : Type u₅
inst✝¹ : Category.{v₅, u₅} J
K : Type u₆
inst✝ : Category.{v₆, u₆} K
Fₗ : C ⥤ E
Fᵣ : D ⥤ E'
Gₗ : E ⥤ J
Gᵣ : E' ⥤ K
c : C
⊢ (mapPairComp Fₗ Fᵣ Gₗ Gᵣ).inv.app (left c) = 𝟙 (left (Gₗ.obj (Fₗ.obj c)))

Tactic:
by
  dsimp [mapPairComp]
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Join.Basic

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
E' : Type u₄
inst✝² : Category.{v₄, u₄} E'
J : Type u₅
inst✝¹ : Category.{v₅, u₅} J
K : Type u₆
inst✝ : Category.{v₆, u₆} K
Fₗ : C ⥤ E
Fᵣ : D ⥤ E'
Gₗ : E ⥤ J
Gᵣ : E' ⥤ K
d : D
⊢ (mapPairComp Fₗ Fᵣ Gₗ Gᵣ).inv.app (right d) = 𝟙 (right (Gᵣ.obj (Fᵣ.obj d)))

Tactic:
by
  dsimp [mapPairComp]
  simp

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 Y : C
inst✝ : HasBinaryProduct X Y
⊢ IsPullback prod.fst prod.snd 0 0

Tactic:
convert! @of_is_product _ _ X Y 0 _ (limit.isLimit _) HasZeroObject.zeroIsTerminal
    <;> 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 Y : C
b : BinaryBicone X Y
h : b.IsBilimit
⊢ IsPullback b.inl 0 b.snd 0

Tactic:
by
  refine of_right ?_ (by simp) (of_isBilimit h)
  simp

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

Goal state before:
pp: case e_a.le_succ_of_le
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 n : ℕ
hh : m + 1 ≤ n
ih :
  ∀ (h : m < n),
    (Functor.ofOpSequence (functorMap f)).map (homOfLE hh).op ≫
        Pi.π (fun i ↦ if i < m + 1 then M i else N i) m ≫ eqToHom ⋯ =
      Pi.π (fun m ↦ if m < n then M m else N m) m
h : m < n + 1
this : homOfLE ⋯ = homOfLE hh ≫ homOfLE ⋯
h₁ : (if x : m < m + 1 then M m else N m) = if x : m < n then M m else N m
h₂ : (if x : m < n then M m else N m) = if x : m < n + 1 then M m else N m
⊢ functorMap f n ≫ Pi.π (fun m ↦ if m < n then M m else N m) m ≫ eqToHom h₂ =
    Pi.π (fun m ↦ if m < n + 1 then M m else N m) m

Tactic:
simp only [functorMap, dite_eq_ite, Pi.π, Pi.map_π_assoc]

Goal state after:
case e_a.le_succ_of_le
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 n : ℕ
hh : m + 1 ≤ n
ih :
  ∀ (h : m < n),
    (Functor.ofOpSequence (functorMap f)).map (homOfLE hh).op ≫
        Pi.π (fun i ↦ if i < m + 1 then M i else N i) m ≫ eqToHom ⋯ =
      Pi.π (fun m ↦ if m < n then M m else N m) m
h : m < n + 1
this : homOfLE ⋯ = homOfLE hh ≫ homOfLE ⋯
h₁ : (if x : m < m + 1 then M m else N m) = if x : m < n then M m else N m
h₂ : (if x : m < n then M m else N m) = if x : m < n + 1 then M m else N m
⊢ limit.π (Discrete.functor fun m ↦ if m < n + 1 then M m else N m) { as := m } ≫
      (if h : m < n then eqToHom ⋯ else if h_1 : m < n + 1 then eqToHom ⋯ ≫ f m ≫ eqToHom ⋯ else eqToHom ⋯) ≫
        eqToHom h₂ =
    limit.π (Discrete.functor fun m ↦ if m < n + 1 then M m else N m) { as := m }
Module: Mathlib.CategoryTheory.Limits.Types.PreservesLimit

Goal state before:
pp: case e'_2
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' : IsColimit c'
P : Cᵒᵖ ⥤ Type w
⊢ (fun g ↦ coconePtToShrinkYoneda c hc' ≫ g) =
    (⇑(coconeCompShrinkYonedaHomEquiv hc').symm ∘ Types.sectionOfCone (P.mapCone c)) ∘ ⇑shrinkYonedaEquiv

Tactic:
ext : 1

Goal state after:
case e'_2
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' : IsColimit c'
P : Cᵒᵖ ⥤ Type w
x✝ : shrinkYoneda.{w, v, u}.obj (unop c.pt) ⟶ P
⊢ coconePtToShrinkYoneda c hc' ≫ x✝ =
    ((⇑(coconeCompShrinkYonedaHomEquiv hc').symm ∘ Types.sectionOfCone (P.mapCone c)) ∘ ⇑shrinkYonedaEquiv) x✝
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
x y : C
f : x ≅ y
z : D
⊢ f.inv ⊵ₗ z ≫ f.hom ⊵ₗ z = 𝟙 (y ⊙ₗ z)

Tactic:
rw [← comp_actionHomLeft, Iso.inv_hom_id, id_actionHomLeft]

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
x y : D
f : x ≅ y
z : C
⊢ f.inv ⊵ᵣ z ≫ f.hom ⊵ᵣ z = 𝟙 (y ⊙ᵣ z)

Tactic:
rw [← comp_actionHomLeft, Iso.inv_hom_id, id_actionHomLeft]

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A B : Mon C
M : Bimod A B
X Y : Mon C
P Q : Bimod X Y
f : P.X ≅ Q.X
f_left_act_hom : P.actLeft ≫ f.hom = X.X ◁ f.hom ≫ Q.actLeft
f_right_act_hom : P.actRight ≫ f.hom = f.hom ▷ Y.X ≫ Q.actRight
⊢ Q.actLeft ≫ f.inv = X.X ◁ f.inv ≫ P.actLeft

Tactic:
rw [← cancel_mono f.hom, Category.assoc, Category.assoc, Iso.inv_hom_id, Category.comp_id,
          f_left_act_hom, ← Category.assoc, ← whiskerLeft_comp, Iso.inv_hom_id,
          whiskerLeft_id, Category.id_comp]

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
A B : Mon C
M : Bimod A B
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)
⊢ (tensorRight T.X).map (P.actRight ▷ Q.X) ≫ (α_ P.X Q.X T.X).hom ≫ P.X ◁ Q.actRight =
    ((α_ (P.X ⊗ S.X) Q.X T.X).hom ≫ (α_ P.X S.X (Q.X ⊗ T.X)).hom ≫ P.X ◁ S.X ◁ Q.actRight ≫ (α_ P.X S.X Q.X).inv) ≫
      P.actRight ▷ Q.X

Tactic:
by
          dsimp
          slice_lhs 1 2 => rw [associator_naturality_left]
          slice_lhs 2 3 => rw [← whisker_exchange]
          simp

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
inst✝³ : MonoidalCategory C
L : D ⥤ C
inst✝² : L.Monoidal
R : C ⥤ D
inst✝¹ : R.Faithful
inst✝ : R.Full
adj : L ⊣ R
d d' : D
⊢ IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))

Tactic:
by
  have := δ _ _ _ ≫= μ_natural L (adj.unit.app d) (adj.unit.app d')
  rw [δ_μ_assoc] at this
  rw [← this]
  infer_instance

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

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
inst✝⁶ : MonoidalCategory D
inst✝⁵ : SymmetricCategory D
inst✝⁴ : MonoidalClosed D
inst✝³ : MonoidalCategory C
L : D ⥤ C
inst✝² : L.Monoidal
R : C ⥤ D
inst✝¹ : R.Faithful
inst✝ : R.Full
adj : L ⊣ R
c X✝ Y✝ : C
x✝ : X✝ ⟶ Y✝
⊢ δ L (R.obj c) (R.obj X✝) ≫ adj.counit.app c ▷ L.obj (R.obj X✝) ≫ c ◁ (adj.counit.app X✝ ≫ x✝) =
    δ L (R.obj c) (R.obj X✝) ≫ adj.counit.app c ▷ L.obj (R.obj X✝) ≫ c ◁ adj.counit.app X✝ ≫ c ◁ x✝

Tactic:
MonoidalCategory.whiskerLeft_comp

Goal state after:
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
inst✝⁶ : MonoidalCategory D
inst✝⁵ : SymmetricCategory D
inst✝⁴ : MonoidalClosed D
inst✝³ : MonoidalCategory C
L : D ⥤ C
inst✝² : L.Monoidal
R : C ⥤ D
inst✝¹ : R.Faithful
inst✝ : R.Full
adj : L ⊣ R
c X✝ Y✝ : C
x✝ : X✝ ⟶ Y✝
⊢ δ L (R.obj c) (R.obj X✝) ≫ adj.counit.app c ▷ L.obj (R.obj X✝) ≫ c ◁ adj.counit.app X✝ ≫ c ◁ x✝ =
    δ L (R.obj c) (R.obj X✝) ≫ adj.counit.app c ▷ L.obj (R.obj X✝) ≫ c ◁ adj.counit.app X✝ ≫ c ◁ x✝
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
A B : Mon C
M✝ : Bimod A B
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)
X Y Z : Mon C
M : Bimod X Y
N₁ N₂ : Bimod Y Z
f : N₁ ⟶ N₂
| M.X ◁ N₁.actLeft ≫ M.X ◁ f.hom

Tactic:
rw [← whiskerLeft_comp, Hom.left_act_hom]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
A B : Mon C
M✝ : Bimod A B
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)
X Y Z : Mon C
M : Bimod X Y
N₁ N₂ : Bimod Y Z
f : N₁ ⟶ N₂
| M.X ◁ (Y.X ◁ f.hom ≫ N₂.actLeft)
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))))
⊢ I.Final

Tactic:
let : Functor.fromPUnit.{0} (.mk (𝟙 e) : CostructuredArrow (𝟭 E) e) |>.Final :=
      Functor.final_fromPUnit_of_isTerminal <| CostructuredArrow.mkIdTerminal (S := 𝟭 E) (Y := e)

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

Tactic:
let : Functor.fromPUnit.{0} (.mk (𝟙 e) : CostructuredArrow (𝟭 E) e) |>.Final :=
      Functor.final_fromPUnit_of_isTerminal <| CostructuredArrow.mkIdTerminal (S := 𝟭 E) (Y := e)

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) (tensorLeft (K.obj e))
cone : Limits.Cocone (CostructuredArrow.proj ((𝟭 E).prod L) (e, d) ⋙ K ⊠ H) :=
  (Functor.LeftExtension.mk (K ⊠ H') (extensionUnitRight H' α K)).coconeAt (e, d)
equiv : CostructuredArrow (𝟭 E) e × CostructuredArrow L d ≌ CostructuredArrow ((𝟭 E).prod L) (e, d) :=
  (CostructuredArrow.prodEquivalence (𝟭 E) L e d).symm
I : CostructuredArrow L d ⥤ CostructuredArrow (𝟭 E) e × CostructuredArrow L d :=
  (prod.leftUnitorEquivalence (CostructuredArrow L d)).inverse ⋙
    (Functor.fromPUnit (CostructuredArrow.mk (𝟙 ((𝟭 E).obj e)))).prod (𝟭 (CostructuredArrow L d))
this : (Functor.fromPUnit (CostructuredArrow.mk (𝟙 e))).Final :=
  Functor.final_fromPUnit_of_isTerminal CostructuredArrow.mkIdTerminal
⊢ I.Final