mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Galois.EssSurj

Goal state before:
pp: 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
this :
  ((functorToAction F).obj A).ρ g ≫ (s.ι.app (SingleObj.star (↥↑V ⧸ (↑U).subgroupOf ↑V))).hom =
    (s.ι.app (SingleObj.star (↥↑V ⧸ (↑U).subgroupOf ↑V))).hom ≫ s.pt.ρ g
⊢ (ConcreteCategory.hom
        (((ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ ↑U))).ρ g ≫ u.inv.hom) ≫
          (s.ι.app (SingleObj.star (↥↑V ⧸ (↑U).subgroupOf ↑V))).hom))
      ⟦σ⟧ =
    (ConcreteCategory.hom ((s.ι.app (SingleObj.star (↥↑V ⧸ (↑U).subgroupOf ↑V))).hom ≫ s.pt.ρ g))
      ((ConcreteCategory.hom u.inv.hom) ⟦σ⟧)

Tactic:
rw [← this, u.inv.comm g]

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
this :
  ((functorToAction F).obj A).ρ g ≫ (s.ι.app (SingleObj.star (↥↑V ⧸ (↑U).subgroupOf ↑V))).hom =
    (s.ι.app (SingleObj.star (↥↑V ⧸ (↑U).subgroupOf ↑V))).hom ≫ s.pt.ρ g
⊢ (ConcreteCategory.hom
        ((u.inv.hom ≫ ((functorToAction F).obj A).ρ g) ≫ (s.ι.app (SingleObj.star (↥↑V ⧸ (↑U).subgroupOf ↑V))).hom))
      ⟦σ⟧ =
    (ConcreteCategory.hom (((functorToAction F).obj A).ρ g ≫ (s.ι.app (SingleObj.star (↥↑V ⧸ (↑U).subgroupOf ↑V))).hom))
      ((ConcreteCategory.hom u.inv.hom) ⟦σ⟧)
Module: Mathlib.CategoryTheory.Galois.IsFundamentalgroup

Goal state before:
pp: C : Type u₁
inst✝⁸ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝⁷ : GaloisCategory C
G : Type u_1
inst✝⁶ : Group G
inst✝⁵ : (X : C) → MulAction G (F.obj X).obj
inst✝⁴ : FiberFunctor F
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : CompactSpace G
inst✝ : IsFundamentalGroup F G
⊢ IsHomeomorph ⇑(toAut F G)

Tactic:
rw [isHomeomorph_iff_continuous_bijective]
  exact ⟨toAut_continuous F G, toAut_bijective F G⟩

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

Goal state before:
pp: case right.right
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'
F : C ⥤ E
G : D ⥤ E
α : Prod.fst C D ⋙ F ⟶ Prod.snd C D ⋙ G
x✝ y✝¹ : D
f✝¹ : x✝ ⟶ y✝¹
y✝ : D
f✝ : y✝¹ ⟶ y✝
⊢ homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) (fun c d ↦ α.app (c, d))
      ((inclRight C D).map f✝¹ ≫ (inclRight C D).map f✝) =
    homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) (fun c d ↦ α.app (c, d)) ((inclRight C D).map f✝¹) ≫
      homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) (fun c d ↦ α.app (c, d)) ((inclRight C D).map f✝)

pp: case edge.right
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'
F : C ⥤ E
G : D ⥤ E
α : Prod.fst C D ⋙ F ⟶ Prod.snd C D ⋙ G
c✝ : C
d✝ y✝ : D
f✝ : d✝ ⟶ y✝
⊢ homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) (fun c d ↦ α.app (c, d))
      (edge c✝ d✝ ≫ (inclRight C D).map f✝) =
    homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) (fun c d ↦ α.app (c, d)) (edge c✝ d✝) ≫
      homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) (fun c d ↦ α.app (c, d)) ((inclRight C D).map f✝)

Tactic:
· simp [← Functor.map_comp]

Goal state after:
case edge.right
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'
F : C ⥤ E
G : D ⥤ E
α : Prod.fst C D ⋙ F ⟶ Prod.snd C D ⋙ G
c✝ : C
d✝ y✝ : D
f✝ : d✝ ⟶ y✝
⊢ homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) (fun c d ↦ α.app (c, d))
      (edge c✝ d✝ ≫ (inclRight C D).map f✝) =
    homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) (fun c d ↦ α.app (c, d)) (edge c✝ d✝) ≫
      homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) (fun c d ↦ α.app (c, d)) ((inclRight C D).map f✝)
Module: Mathlib.CategoryTheory.Limits.Preserves.BifunctorCokernel

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

Tactic:
· simp [← Functor.map_comp]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : FormalCoproduct C
i j : X.I
hij : i = j
⊢ (X.objIsoOfEq hij).symm = X.objIsoOfEq ⋯

Tactic:
by
  subst hij
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
⊢ h.p₂ ≫ f₂ = h.p

Tactic:
← p₂₃_p₂_assoc,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
⊢ h.p₂₃ ≫ h₂₃.p₁ ≫ f₂ = h.p
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
Y : C
φ φ' : Y ⟶ h.pullback
h₁ : φ ≫ h.p₁ = φ' ≫ h.p₁
h₂ : φ ≫ h.p₂ = φ' ≫ h.p₂
h₃ : φ ≫ h.p₃ = φ' ≫ h.p₃
⊢ φ = φ'

Tactic:
apply h.isPullback₂.hom_ext

Goal state after:
case h₀
C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
Y : C
φ φ' : Y ⟶ h.pullback
h₁ : φ ≫ h.p₁ = φ' ≫ h.p₁
h₂ : φ ≫ h.p₂ = φ' ≫ h.p₂
h₃ : φ ≫ h.p₃ = φ' ≫ h.p₃
⊢ φ ≫ h.p₁₂ = φ' ≫ h.p₁₂

case h₁
C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
Y : C
φ φ' : Y ⟶ h.pullback
h₁ : φ ≫ h.p₁ = φ' ≫ h.p₁
h₂ : φ ≫ h.p₂ = φ' ≫ h.p₂
h₃ : φ ≫ h.p₃ = φ' ≫ h.p₃
⊢ φ ≫ h.p₂₃ = φ' ≫ h.p₂₃
Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct

Goal state before:
pp: C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
⊢ (Functor.const ℕᵒᵖ).obj (∏ᶜ M) ⟶ Functor.ofOpSequence (functorMap f)

Tactic:
refine NatTrans.ofOpSequence
      (fun n ↦ Limits.Pi.map fun m ↦ if h : m < n then eqToHom (functorObj_eq_pos h).symm else
        f m ≫ eqToHom (functorObj_eq_neg h).symm) (fun n ↦ ?_)
    apply Limits.Pi.hom_ext
    intro m
    simp only [Functor.const_obj_obj, dite_eq_ite, Functor.ofOpSequence_obj, homOfLE_leOfHom,
      Functor.const_obj_map, Category.id_comp, Pi.map_π, Functor.ofOpSequence_map_homOfLE_succ,
      functorMap, Category.assoc, Pi.map_π_assoc]
    split
    · simp [dif_pos (by lia : m < n + 1)]
    · split
      all_goals simp

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

Goal state before:
pp: case pos
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
s : Cone (Functor.ofOpSequence (functorMap f))
n m : ℕ
h : m < n
⊢ ((Pi.lift fun m ↦ s.π.app (Opposite.op (m + 1)) ≫ Pi.π (fun i ↦ if x : i < m + 1 then M i else N i) m ≫ eqToHom ⋯) ≫
        (cone f).π.app (Opposite.op n)) ≫
      Pi.π (fun m ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m) m =
    s.π.app (Opposite.op n) ≫ Pi.π (fun m ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m) m

Tactic:
simp only [Category.assoc, cone_π_app_comp_Pi_π_pos f _ _ h]

Goal state after:
case pos
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
s : Cone (Functor.ofOpSequence (functorMap f))
n m : ℕ
h : m < n
⊢ (Pi.lift fun m ↦ s.π.app (Opposite.op (m + 1)) ≫ Pi.π (fun i ↦ if x : i < m + 1 then M i else N i) m ≫ eqToHom ⋯) ≫
      Pi.π M m ≫ eqToHom ⋯ =
    s.π.app (Opposite.op n) ≫ Pi.π (fun m ↦ if x : m < n then M m else N m) m
Module: Mathlib.CategoryTheory.Limits.Types.End

Goal state before:
pp: J : Type u
inst✝ : Category.{v, u} J
F : Jᵒᵖ ⥤ J ⥤ Type (max w u)
s : Cocone (multispanIndexCoend F).multispan
m : (cowedge F).pt ⟶ s.pt
h : ∀ (j : WalkingMultispan (multispanShapeCoend J)), (cowedge F).ι.app j ≫ m = s.ι.app j
⊢ m = ↾Quot.lift (fun x ↦ (hom (Multicofork.π s x.fst)) x.snd) ⋯

Tactic:
by ext ⟨j⟩; exact ConcreteCategory.congr_hom (h (.right j.fst)) j.snd

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

Goal state before:
pp: J : Type u_1
C : Type u_3
K : Type u_5
inst✝² : Category.{v_1, u_5} K
inst✝¹ : Category.{v_3, u_1} J
inst✝ : Category.{v_5, u_3} C
F F' : K ⥤ J
e : F ≅ F'
⊢ preservesColimit F = preservesColimit F'

Tactic:
ext G
  simp_rw [preservesColimit_iff]
  exact ⟨fun h ↦ preservesColimit_of_iso_diagram _ e,
    fun h ↦ preservesColimit_of_iso_diagram _ e.symm⟩

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

Goal state before:
pp: J : Type u_1
C : Type u_3
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_5, u_3} C
e : K ≌ K'
⊢ preservesColimitsOfShape K = preservesColimitsOfShape K'

Tactic:
ext G
  simp only [preservesColimitsOfShape_iff]
  exact ⟨fun _ ↦ preservesColimitsOfShape_of_equiv e _,
    fun _ ↦ preservesColimitsOfShape_of_equiv e.symm _⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
A' : Type u₄
B' : Type u₅
C' : Type u₆
A'' : Type u₇
B'' : Type u₈
C'' : Type u₉
inst✝⁹ : Category.{v₁, u₁} A
inst✝⁸ : Category.{v₂, u₂} B
inst✝⁷ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
inst✝⁶ : Category.{v₄, u₄} A'
inst✝⁵ : Category.{v₅, u₅} B'
inst✝⁴ : Category.{v₆, u₆} C'
F' : A' ⥤ B'
G' : C' ⥤ B'
inst✝³ : Category.{v₇, u₇} A''
inst✝² : Category.{v₈, u₈} B''
inst✝¹ : Category.{v₉, u₉} C''
F'' : A'' ⥤ B''
G'' : C'' ⥤ B''
ψ ψ' : CatCospanTransform F G F' G'
f : ψ' ⟶ ψ'
inst✝ : IsIso f
e : ψ ≅ ψ'
⊢ e.hom.left ≫ e.inv.left = 𝟙 ψ.left

Tactic:
simp [← category_comp_left]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
A' : Type u₄
B' : Type u₅
C' : Type u₆
A'' : Type u₇
B'' : Type u₈
C'' : Type u₉
inst✝⁹ : Category.{v₁, u₁} A
inst✝⁸ : Category.{v₂, u₂} B
inst✝⁷ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
inst✝⁶ : Category.{v₄, u₄} A'
inst✝⁵ : Category.{v₅, u₅} B'
inst✝⁴ : Category.{v₆, u₆} C'
F' : A' ⥤ B'
G' : C' ⥤ B'
inst✝³ : Category.{v₇, u₇} A''
inst✝² : Category.{v₈, u₈} B''
inst✝¹ : Category.{v₉, u₉} C''
F'' : A'' ⥤ B''
G'' : C'' ⥤ B''
ψ ψ' : CatCospanTransform F G F' G'
f : ψ' ⟶ ψ'
inst✝ : IsIso f
e : ψ ≅ ψ'
⊢ e.inv.left ≫ e.hom.left = 𝟙 ψ'.left

Tactic:
simp [← category_comp_left]

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
D : Type u_2
inst✝¹ : Category.{v_2, u_2} D
inst✝ : MonoidalCategory D
F₁ F₂ : C ⥤ D
f : F₁ ⟶ F₂
x✝² x✝¹ : C
x✝ : x✝² ⟶ x✝¹
⊢ (curriedTensorPre F₁).map x✝ ≫ { app := fun X₂ ↦ f.app x✝¹ ⊗ₘ f.app X₂, naturality := ⋯ } =
    { app := fun X₂ ↦ f.app x✝² ⊗ₘ f.app X₂, naturality := ⋯ } ≫ (curriedTensorPre F₂).map x✝

Tactic:
ext
        simp [← tensorHom_id]

Goal state after:
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
Z : C
⊢ (ofMon X).μ.app Z ≫ f.hom.app Z = ((ofMon X).map (f.hom.app Z) ≫ f.hom.app ((ofMon Y).obj Z)) ≫ (ofMon Y).μ.app Z

Tactic:
simpa [-IsMonHom.mul_hom] using congrArg (fun t ↦ t.app Z) (IsMonHom.mul_hom f.hom)

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

Goal state before:
pp: C : Type u₁
inst✝¹² : Category.{v₁, u₁} C
inst✝¹¹ : MonoidalCategory C
D : Type u₂
inst✝¹⁰ : Category.{v₂, u₂} D
inst✝⁹ : MonoidalLeftAction C D
M' N' O' : D
A✝¹ : C
inst✝⁸ : MonObj A✝¹
M✝¹ N O : D
inst✝⁷ : ModObj A✝¹ M✝¹
inst✝⁶ : ModObj A✝¹ N
inst✝⁵ : ModObj A✝¹ O
A✝ : C
inst✝⁴ : MonObj A✝
M✝ : Mod D A✝
A B : C
inst✝³ : MonObj A
inst✝² : MonObj B
f : A ⟶ B
inst✝¹ : IsMonHom f
M : D
inst✝ : ModObj B M
⊢ η ⊵ₗ M ≫ γ = (λₗ M).hom

Tactic:
ModObj.one_smul

Goal state after:
C : Type u₁
inst✝¹² : Category.{v₁, u₁} C
inst✝¹¹ : MonoidalCategory C
D : Type u₂
inst✝¹⁰ : Category.{v₂, u₂} D
inst✝⁹ : MonoidalLeftAction C D
M' N' O' : D
A✝¹ : C
inst✝⁸ : MonObj A✝¹
M✝¹ N O : D
inst✝⁷ : ModObj A✝¹ M✝¹
inst✝⁶ : ModObj A✝¹ N
inst✝⁵ : ModObj A✝¹ O
A✝ : C
inst✝⁴ : MonObj A✝
M✝ : Mod D A✝
A B : C
inst✝³ : MonObj A
inst✝² : MonObj B
f : A ⟶ B
inst✝¹ : IsMonHom f
M : D
inst✝ : ModObj B M
⊢ (λₗ M).hom = (λₗ M).hom
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Normal

Goal state before:
pp: case refine_2.refine_2
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : CartesianMonoidalCategory C
G H : C
inst✝³ : GrpObj G
inst✝² : GrpObj H
φ : H ⟶ G
inst✝¹ : IsMonHom φ
inst✝ : Mono φ
hnormal : ∀ (X : C), (monoidHom φ X).range.Normal
h' : (X : C) → (X ⟶ G) → (X ⟶ H) → (X ⟶ H)
hh' : ∀ (X : C) (g : X ⟶ G) (h : X ⟶ H), h' X g h ≫ φ = g * h ≫ φ * g⁻¹
⊢ Yoneda.fullyFaithful.preimage
        { app := fun X ↦ ↾fun x ↦ h' (Opposite.unop X) (x ≫ fst G H) (x ≫ snd G H), naturality := ⋯ } ≫
      φ =
    G ◁ φ ≫ conj G

Tactic:
refine yoneda.map_injective ?_
      ext
      simp [hh', conj, comp_mul, comp_inv]

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
⊢ (R.X ◁ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)) ▷ T.X ≫
      actLeft P Q ▷ T.X ≫ actRight P Q =
    (R.X ◁ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)) ▷ T.X ≫
      (α_ R.X (coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)) T.X).hom ≫
        R.X ◁ actRight P Q ≫ actLeft P Q

Tactic:
slice_lhs 1 2 => rw [← comp_whiskerRight, whiskerLeft_π_actLeft, comp_whiskerRight,
    comp_whiskerRight]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
⊢ ((α_ R.X P.X Q.X).inv ▷ T.X ≫
        P.actLeft ▷ Q.X ▷ T.X ≫ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ▷ T.X) ≫
      actRight P Q =
    (R.X ◁ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)) ▷ T.X ≫
      (α_ R.X (coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)) T.X).hom ≫
        R.X ◁ actRight P Q ≫ actLeft P Q
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₂
⊢ X.X ◁ coequalizer.π (M.actRight ▷ N₁.X) ((α_ M.X Y.X N₁.X).hom ≫ M.X ◁ N₁.actLeft) ≫
      TensorBimod.actLeft M N₁ ≫
        colimMap
          (parallelPairHom (M.actRight ▷ N₁.X) ((α_ M.X Y.X N₁.X).hom ≫ M.X ◁ N₁.actLeft) (M.actRight ▷ N₂.X)
            ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft) ((M.X ⊗ Y.X) ◁ f.hom) (M.X ◁ f.hom) ⋯ ⋯) =
    X.X ◁ coequalizer.π (M.actRight ▷ N₁.X) ((α_ M.X Y.X N₁.X).hom ≫ M.X ◁ N₁.actLeft) ≫
      X.X ◁
          colimMap
            (parallelPairHom (M.actRight ▷ N₁.X) ((α_ M.X Y.X N₁.X).hom ≫ M.X ◁ N₁.actLeft) (M.actRight ▷ N₂.X)
              ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft) ((M.X ⊗ Y.X) ◁ f.hom) (M.X ◁ f.hom) ⋯ ⋯) ≫
        TensorBimod.actLeft M N₂

Tactic:
slice_lhs 1 2 => rw [TensorBimod.whiskerLeft_π_actLeft]

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₂
⊢ ((α_ X.X M.X N₁.X).inv ≫
        M.actLeft ▷ N₁.X ≫ coequalizer.π (M.actRight ▷ N₁.X) ((α_ M.X Y.X N₁.X).hom ≫ M.X ◁ N₁.actLeft)) ≫
      colimMap
        (parallelPairHom (M.actRight ▷ N₁.X) ((α_ M.X Y.X N₁.X).hom ≫ M.X ◁ N₁.actLeft) (M.actRight ▷ N₂.X)
          ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft) ((M.X ⊗ Y.X) ◁ f.hom) (M.X ◁ f.hom) ⋯ ⋯) =
    X.X ◁ coequalizer.π (M.actRight ▷ N₁.X) ((α_ M.X Y.X N₁.X).hom ≫ M.X ◁ N₁.actLeft) ≫
      X.X ◁
          colimMap
            (parallelPairHom (M.actRight ▷ N₁.X) ((α_ M.X Y.X N₁.X).hom ≫ M.X ◁ N₁.actLeft) (M.actRight ▷ N₂.X)
              ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft) ((M.X ⊗ Y.X) ◁ f.hom) (M.X ◁ f.hom) ⋯ ⋯) ≫
        TensorBimod.actLeft M N₂
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₁ M₂ : Bimod X Y
f : M₁ ⟶ M₂
N : Bimod Y Z
⊢ X.X ◁ coequalizer.π (M₁.actRight ▷ N.X) ((α_ M₁.X Y.X N.X).hom ≫ M₁.X ◁ N.actLeft) ≫
      TensorBimod.actLeft M₁ N ≫
        colimMap
          (parallelPairHom (M₁.actRight ▷ N.X) ((α_ M₁.X Y.X N.X).hom ≫ M₁.X ◁ N.actLeft) (M₂.actRight ▷ N.X)
            ((α_ M₂.X Y.X N.X).hom ≫ M₂.X ◁ N.actLeft) (f.hom ▷ Y.X ▷ N.X) (f.hom ▷ N.X) ⋯ ⋯) =
    X.X ◁ coequalizer.π (M₁.actRight ▷ N.X) ((α_ M₁.X Y.X N.X).hom ≫ M₁.X ◁ N.actLeft) ≫
      X.X ◁
          colimMap
            (parallelPairHom (M₁.actRight ▷ N.X) ((α_ M₁.X Y.X N.X).hom ≫ M₁.X ◁ N.actLeft) (M₂.actRight ▷ N.X)
              ((α_ M₂.X Y.X N.X).hom ≫ M₂.X ◁ N.actLeft) (f.hom ▷ Y.X ▷ N.X) (f.hom ▷ N.X) ⋯ ⋯) ≫
        TensorBimod.actLeft M₂ N

Tactic:
slice_lhs 1 2 => rw [TensorBimod.whiskerLeft_π_actLeft]

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₁ M₂ : Bimod X Y
f : M₁ ⟶ M₂
N : Bimod Y Z
⊢ ((α_ X.X M₁.X N.X).inv ≫
        M₁.actLeft ▷ N.X ≫ coequalizer.π (M₁.actRight ▷ N.X) ((α_ M₁.X Y.X N.X).hom ≫ M₁.X ◁ N.actLeft)) ≫
      colimMap
        (parallelPairHom (M₁.actRight ▷ N.X) ((α_ M₁.X Y.X N.X).hom ≫ M₁.X ◁ N.actLeft) (M₂.actRight ▷ N.X)
          ((α_ M₂.X Y.X N.X).hom ≫ M₂.X ◁ N.actLeft) (f.hom ▷ Y.X ▷ N.X) (f.hom ▷ N.X) ⋯ ⋯) =
    X.X ◁ coequalizer.π (M₁.actRight ▷ N.X) ((α_ M₁.X Y.X N.X).hom ≫ M₁.X ◁ N.actLeft) ≫
      X.X ◁
          colimMap
            (parallelPairHom (M₁.actRight ▷ N.X) ((α_ M₁.X Y.X N.X).hom ≫ M₁.X ◁ N.actLeft) (M₂.actRight ▷ N.X)
              ((α_ M₂.X Y.X N.X).hom ≫ M₂.X ◁ N.actLeft) (f.hom ▷ Y.X ▷ N.X) (f.hom ▷ N.X) ⋯ ⋯) ≫
        TensorBimod.actLeft M₂ N
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
V : Type u₂
inst✝³ : Category.{v₂, u₂} V
inst✝² : MonoidalCategory C
inst✝¹ : MonoidalCategory V
inst✝ : MonoidalClosed V
F G H : C ⥤ V
ℌ : DayConvolutionInternalHom F G H
G' H' : C ⥤ V
f : G ⟶ G'
ℌ' : DayConvolutionInternalHom F G' H'
c j j' : C
φ : j ⟶ j'
⊢ (ℌ.π c j ≫ ((((dayConvolutionInternalHomDiagramFunctor F).map f).app c).app (op j)).app j) ≫
      ((((dayConvolutionInternalHomDiagramFunctor F).obj G').obj c).obj (op j)).map φ =
    (ℌ.π c j' ≫ ((((dayConvolutionInternalHomDiagramFunctor F).map f).app c).app (op j')).app j') ≫
      ((((dayConvolutionInternalHomDiagramFunctor F).obj G').obj c).map φ.op).app j'

Tactic:
have := congrArg (fun t ↦ t.app j') <|
        dayConvolutionInternalHomDiagramFunctor
          F |>.map f |>.app c |>.naturality φ.op

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
V : Type u₂
inst✝³ : Category.{v₂, u₂} V
inst✝² : MonoidalCategory C
inst✝¹ : MonoidalCategory V
inst✝ : MonoidalClosed V
F G H : C ⥤ V
ℌ : DayConvolutionInternalHom F G H
G' H' : C ⥤ V
f : G ⟶ G'
ℌ' : DayConvolutionInternalHom F G' H'
c j j' : C
φ : j ⟶ j'
this :
  ((((dayConvolutionInternalHomDiagramFunctor F).obj G).obj c).map φ.op ≫
          (((dayConvolutionInternalHomDiagramFunctor F).map f).app c).app (op j)).app
      j' =
    ((((dayConvolutionInternalHomDiagramFunctor F).map f).app c).app (op j') ≫
          (((dayConvolutionInternalHomDiagramFunctor F).obj G').obj c).map φ.op).app
      j'
⊢ (ℌ.π c j ≫ ((((dayConvolutionInternalHomDiagramFunctor F).map f).app c).app (op j)).app j) ≫
      ((((dayConvolutionInternalHomDiagramFunctor F).obj G').obj c).obj (op j)).map φ =
    (ℌ.π c j' ≫ ((((dayConvolutionInternalHomDiagramFunctor F).map f).app c).app (op j')).app j') ≫
      ((((dayConvolutionInternalHomDiagramFunctor F).obj G').obj c).map φ.op).app j'
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 ≫ μ = η ≫ ε ≫ η
⊢ η ≫ 𝒮 = η

Tactic:
Bimon.one_comul_assoc,

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