mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.GradedObject.Braiding

Goal state before:
pp: I : Type u_1
inst✝²⁰ : AddCommMonoid I
C : Type u_2
inst✝¹⁹ : Category.{v_1, u_2} C
inst✝¹⁸ : MonoidalCategory C
X Y Z : GradedObject I C
inst✝¹⁷ : BraidedCategory C
inst✝¹⁶ : X.HasTensor Y
inst✝¹⁵ : Y.HasTensor Z
inst✝¹⁴ : Z.HasTensor X
inst✝¹³ : Z.HasTensor Y
inst✝¹² : X.HasTensor Z
inst✝¹¹ : (tensorObj X Y).HasTensor Z
inst✝¹⁰ : X.HasTensor (tensorObj Y Z)
inst✝⁹ : Z.HasTensor (tensorObj X Y)
inst✝⁸ : (tensorObj Z X).HasTensor Y
inst✝⁷ : X.HasTensor (tensorObj Z Y)
inst✝⁶ : (tensorObj X Z).HasTensor Y
inst✝⁵ : X.HasGoodTensor₁₂Tensor Y Z
inst✝⁴ : X.HasGoodTensorTensor₂₃ Y Z
inst✝³ : Z.HasGoodTensor₁₂Tensor X Y
inst✝² : Z.HasGoodTensorTensor₂₃ X Y
inst✝¹ : X.HasGoodTensor₁₂Tensor Z Y
inst✝ : X.HasGoodTensorTensor₂₃ Z Y
k i₁ i₂ i₃ : I
h : i₁ + i₂ + i₃ = k
⊢ ιTensorObj₃ X Y Z i₁ i₂ i₃ k h ≫
      (associator X Y Z).inv k ≫
        (tensorObjDesc fun i j hij ↦ (β_ (tensorObj X Y i) (Z j)).hom ≫ ιTensorObj Z (tensorObj X Y) j i k ⋯) ≫
          (associator Z X Y).inv k =
    ιTensorObj₃ X Y Z i₁ i₂ i₃ k h ≫
      whiskerLeft X (fun k ↦ tensorObjDesc fun i j hij ↦ (β_ (Y i) (Z j)).hom ≫ ιTensorObj Z Y j i k ⋯) k ≫
        (associator X Z Y).inv k ≫
          whiskerRight (fun k ↦ tensorObjDesc fun i j hij ↦ (β_ (X i) (Z j)).hom ≫ ιTensorObj Z X j i k ⋯) Y k

Tactic:
conv_lhs => rw [ιTensorObj₃_associator_inv_assoc, ιTensorObj₃'_eq X Y Z i₁ i₂ i₃ k h _ rfl, assoc,
    ι_tensorObjDesc_assoc, assoc, ← MonoidalCategory.tensorHom_id,
    BraidedCategory.braiding_naturality_assoc,
    BraidedCategory.braiding_tensor_left_hom, assoc, assoc, assoc, assoc, Iso.inv_hom_id_assoc,
    MonoidalCategory.id_tensorHom,
    ← ιTensorObj₃_eq_assoc Z X Y i₃ i₁ i₂ k (by rw [add_assoc, add_comm i₃, h]) _ rfl,
    ιTensorObj₃_associator_inv, Iso.hom_inv_id_assoc]

Goal state after:
I : Type u_1
inst✝²⁰ : AddCommMonoid I
C : Type u_2
inst✝¹⁹ : Category.{v_1, u_2} C
inst✝¹⁸ : MonoidalCategory C
X Y Z : GradedObject I C
inst✝¹⁷ : BraidedCategory C
inst✝¹⁶ : X.HasTensor Y
inst✝¹⁵ : Y.HasTensor Z
inst✝¹⁴ : Z.HasTensor X
inst✝¹³ : Z.HasTensor Y
inst✝¹² : X.HasTensor Z
inst✝¹¹ : (tensorObj X Y).HasTensor Z
inst✝¹⁰ : X.HasTensor (tensorObj Y Z)
inst✝⁹ : Z.HasTensor (tensorObj X Y)
inst✝⁸ : (tensorObj Z X).HasTensor Y
inst✝⁷ : X.HasTensor (tensorObj Z Y)
inst✝⁶ : (tensorObj X Z).HasTensor Y
inst✝⁵ : X.HasGoodTensor₁₂Tensor Y Z
inst✝⁴ : X.HasGoodTensorTensor₂₃ Y Z
inst✝³ : Z.HasGoodTensor₁₂Tensor X Y
inst✝² : Z.HasGoodTensorTensor₂₃ X Y
inst✝¹ : X.HasGoodTensor₁₂Tensor Z Y
inst✝ : X.HasGoodTensorTensor₂₃ Z Y
k i₁ i₂ i₃ : I
h : i₁ + i₂ + i₃ = k
⊢ MonoidalCategoryStruct.whiskerLeft (X i₁) (β_ (Y i₂) (Z i₃)).hom ≫
      (MonoidalCategoryStruct.associator (X i₁) (Z i₃) (Y i₂)).inv ≫
        MonoidalCategoryStruct.whiskerRight (β_ (X i₁) (Z i₃)).hom (Y i₂) ≫ ιTensorObj₃' Z X Y i₃ i₁ i₂ k ⋯ =
    ιTensorObj₃ X Y Z i₁ i₂ i₃ k h ≫
      whiskerLeft X (fun k ↦ tensorObjDesc fun i j hij ↦ (β_ (Y i) (Z j)).hom ≫ ιTensorObj Z Y j i k ⋯) k ≫
        (associator X Z Y).inv k ≫
          whiskerRight (fun k ↦ tensorObjDesc fun i j hij ↦ (β_ (X i) (Z j)).hom ≫ ιTensorObj Z X j i k ⋯) Y k
Module: Mathlib.CategoryTheory.Join.Basic

Goal state before:
pp: case left
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
a✝ : C
⊢ homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) (fun c d ↦ α.app (c, d)) (𝟙 (left a✝)) =
    𝟙
      (match left a✝ with
      | left x => F.obj x
      | right x => G.obj x)

Tactic:
dsimp only [id_left, homInduction_left]
      simp

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

Goal state before:
pp: I : Type v₁
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
J : Type v₁
inst✝ : SmallCategory J
F : J ⥤ ((i : I) → C i)
c : (i : I) → Cocone (F ⋙ Pi.eval C i)
P : (i : I) → IsColimit (c i)
s : Cocone F
m : (coconeOfCoconeCompEval c).pt ⟶ s.pt
w : ∀ (j : J), (coconeOfCoconeCompEval c).ι.app j ≫ m = s.ι.app j
i : I
⊢ m i = (P i).desc (coconeCompEval s i)

Tactic:
exact (P i).uniq (coconeCompEval s i) (m i) fun j => congr_fun (w j) i

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.BifunctorCokernel

Goal state before:
pp: 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✝³ : PreservesColimit (parallelPair f₂ 0) (F.obj c₁.pt)
inst✝² : PreservesColimit (parallelPair f₁ 0) (F.flip.obj Y₂)
inst✝¹ : HasBinaryCoproduct ((F.obj X₁).obj Y₂) ((F.obj Y₁).obj X₂)
inst✝ : PreservesColimit (parallelPair f₁ 0) (F.flip.obj X₂)
s : CokernelCofork (coprod.desc ((F.map f₁).app Y₂) ((F.obj Y₁).map f₂))
⊢ ∃ l, (F.map (Cofork.π c₁)).app Y₂ ≫ (F.obj c₁.pt).map (Cofork.π c₂) ≫ l = Cofork.π s

Tactic:
obtain ⟨l, hl⟩ := Cofork.IsColimit.desc' (mapIsColimit _ hc₁ (F.flip.obj Y₂)) s.π (by
    have := coprod.inl ≫= s.condition
    rw [coprod.inl_desc_assoc, comp_zero] at this
    rwa [zero_comp])
  obtain ⟨l', hl'⟩ := Cofork.IsColimit.desc' (mapIsColimit _ hc₂ (F.obj c₁.pt)) l (by
    have := coprod.inr ≫= s.condition
    rw [coprod.inr_desc_assoc, ← dsimp% hl, NatTrans.naturality_assoc, comp_zero] at this
    apply Cofork.IsColimit.hom_ext (mapIsColimit _ hc₁ (F.flip.obj X₂))
    rwa [zero_comp, comp_zero])
  exact ⟨l', by cat_disch⟩

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:
subst hij

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : FormalCoproduct C
i : X.I
⊢ (X.objIsoOfEq ⋯).symm = X.objIsoOfEq ⋯
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u₁
inst✝ : Category.{v₁, u₁} A
X Y Z : FormalCoproduct C
f : X ⟶ Z
g : Y ⟶ Z
pb :
  (i : Function.Pullback f.f g.f) → PullbackCone (f.φ (↑i).1 ≫ eqToHom (@_proof_107 C inst✝¹ X Y Z f g i)) (g.φ (↑i).2)
hpb : (i : Function.Pullback f.f g.f) → IsLimit (pb i)
T : FormalCoproduct C
s : PullbackCone f g
m : s.pt ⟶ (pullbackCone f g pb).pt
h₁ : m ≫ (pullbackCone f g pb).fst = s.fst
h₂ : m ≫ (pullbackCone f g pb).snd = s.snd
⊢ m = (homPullbackEquiv f g pb hpb s.pt).invFun ⟨(s.fst, s.snd), ⋯⟩

Tactic:
convert! ((homPullbackEquiv f g pb hpb s.pt).left_inv m).symm using 3

Goal state after:
case e'_3
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u₁
inst✝ : Category.{v₁, u₁} A
X Y Z : FormalCoproduct C
f : X ⟶ Z
g : Y ⟶ Z
pb :
  (i : Function.Pullback f.f g.f) → PullbackCone (f.φ (↑i).1 ≫ eqToHom (@_proof_107 C inst✝¹ X Y Z f g i)) (g.φ (↑i).2)
hpb : (i : Function.Pullback f.f g.f) → IsLimit (pb i)
T : FormalCoproduct C
s : PullbackCone f g
m : s.pt ⟶ (pullbackCone f g pb).pt
h₁ : m ≫ (pullbackCone f g pb).fst = s.fst
h₂ : m ≫ (pullbackCone f g pb).snd = s.snd
⊢ (s.fst, s.snd) = ↑((homPullbackEquiv f g pb hpb s.pt).1 m)
Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct

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

Tactic:
← functorMap_commSq_succ f (m + 1)

Goal state after:
case succ
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
n m : ℕ
h : ¬m + 1 < n
⊢ (Functor.ofOpSequence (functorMap f)).map (homOfLE ⋯).op ≫
      Pi.π (fun m ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m) (m + 1) ≫ eqToHom ⋯ =
    (Functor.ofOpSequence (functorMap f)).map (homOfLE ⋯).op ≫
      Pi.π (fun m_1 ↦ if x : m_1 < Opposite.unop (Opposite.op (m + 1)) then M m_1 else N m_1) (m + 1) ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits

Goal state before:
pp: J : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst✝⁴ : Category.{v_1, u_1} J
inst✝³ : Category.{v_2, u_3} C
inst✝² : Category.{v_3, u_2} K
inst✝¹ : Category.{v_4, u_4} D
F : C ⥤ D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
this✝ : IsClosedUnderIsomorphisms fun f ↦ Coequifibered f.hom
this : ∀ (a b : Cᵒᵖ), HasCoproductsOfShape (a ⟶ b) Dᵒᵖ
e : Over F.op ≌ (Under F)ᵒᵖ := ⋯
f : Over F.op
⊢ (ObjectProperty.op fun f ↦ Coequifibered f.hom).inverseImage e.functor f ↔ Equifibered f.hom

Tactic:
simp [e, MorphismProperty.cancel_left_of_respectsIso, ← coequifibered_unop_iff]

Goal state after:
J : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst✝⁴ : Category.{v_1, u_1} J
inst✝³ : Category.{v_2, u_3} C
inst✝² : Category.{v_3, u_2} K
inst✝¹ : Category.{v_4, u_4} D
F : C ⥤ D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
this✝ : IsClosedUnderIsomorphisms fun f ↦ Coequifibered f.hom
this : ∀ (a b : Cᵒᵖ), HasCoproductsOfShape (a ⟶ b) Dᵒᵖ
e : Over F.op ≌ (Under F)ᵒᵖ := (postEquiv (Opposite.op F) (opUnopEquiv C D)).symm.trans (opEquivOpUnder F)
f : Over F.op
⊢ { app := fun X ↦ (f.hom.app (Opposite.op X)).unop, naturality := ⋯ }.Coequifibered ↔
    Coequifibered (NatTrans.unop f.hom)
Module: Mathlib.CategoryTheory.Localization.BousfieldTransfiniteComposition

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
P : ObjectProperty C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
X Y : C
f✝ : X ⟶ Y
x✝² : P.isLocal.transfiniteCompositionsOfShape J f✝
Z : C
hZ : P Z
hf : P.isLocal.TransfiniteCompositionOfShape J f✝
g : X ⟶ Z
d : (hf.F.op ⋙ yoneda.obj Z).WellOrderInductionData := Functor.WellOrderInductionData.ofExists ⋯ ⋯
σ : ↑(hf.F.op ⋙ yoneda.obj Z).sections := d.sectionsMk (hf.isoBot.hom ≫ g)
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ hf.F.map f ≫ ↑σ (op x✝) = ↑σ (op x✝¹) ≫ ((Functor.const J).obj Z).map f

Tactic:
dsimp
            simpa only [Category.comp_id] using! σ.2 f.op

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

Goal state before:
pp: case comp_id
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝¹ : C → D
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f g : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
X✝ Y✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ projectMapAux f✝¹ (f✝.comp (Hom.id Y✝)) = projectMapAux f✝¹ f✝

Tactic:
dsimp only [projectMapAux]; rw [Category.comp_id]

Goal state after:
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
A : C
⊢ toUnit A ≫ curryRightUnitorHom I = curry (fst I A)

Tactic:
by
  apply uncurry_injective
  simp [uncurry_natural_left, curryRightUnitorHom, fst_def, toUnit]

Goal state after:
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
d : D
⊢ (λₗ (F.obj d)).inv ≫ μₗ F (𝟙_ C) d = F.map (λₗ d).inv

Tactic:
by
  simpa [-μₗ_unitality] using
    (λₗ[C] (F.obj d)).inv ≫=
      (μₗ_unitality F d).symm =≫
      F.map (λₗ[C] d).inv

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)))
tfae_1_to_3 :
  (∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))) → ∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))
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)
⊢ ⇑(ConcreteCategory.hom ((yoneda.map ((pre (adj.unit.app d)).app (R.obj c))).app (Opposite.op d'))) =
    ⇑((ihom.adjunction d).homEquiv d' (R.obj c)) ∘
      ⇑(ConcreteCategory.hom ((coyoneda.map (adj.unit.app d ▷ d').op).app (R.obj c))) ∘
        ⇑((ihom.adjunction ((L ⋙ R).obj d)).homEquiv d' (R.obj c)).symm

Tactic:
rw [← Function.comp_assoc, ((ihom.adjunction ((L ⋙ R).obj d)).homEquiv _ _).eq_comp_symm]

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)))
tfae_1_to_3 :
  (∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))) → ∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))
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)
⊢ ⇑(ConcreteCategory.hom ((yoneda.map ((pre (adj.unit.app d)).app (R.obj c))).app (Opposite.op d'))) ∘
      ⇑((ihom.adjunction ((L ⋙ R).obj d)).homEquiv (Opposite.unop (Opposite.op d')) (R.obj c)) =
    ⇑((ihom.adjunction d).homEquiv d' (R.obj c)) ∘
      ⇑(ConcreteCategory.hom ((coyoneda.map (adj.unit.app d ▷ d').op).app (R.obj c)))
Module: Mathlib.CategoryTheory.Monoidal.Closed.Ideal

Goal state before:
pp: case h_fst
C : Type u₁
D : Type u₂
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Reflective i
inst✝³ : MonoidalClosed C
inst✝² : CartesianMonoidalCategory D
inst✝¹ : ExponentialIdeal i
inst✝ : BraidedCategory C
A B : C
⊢ ((reflectorAdjunction i).unit.app A ⊗ₘ (reflectorAdjunction i).unit.app B) ≫
      fst (i.obj ((reflector i).obj A)) (i.obj ((reflector i).obj B)) =
    ((reflectorAdjunction i).unit.app (A ⊗ B) ≫
        i.map (prodComparison (reflector i) A B) ≫ prodComparison i ((reflector i).obj A) ((reflector i).obj B)) ≫
      fst (i.obj ((reflector i).obj A)) (i.obj ((reflector i).obj B))

Tactic:
tensorHom_fst,

Goal state after:
case h_fst
C : Type u₁
D : Type u₂
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Reflective i
inst✝³ : MonoidalClosed C
inst✝² : CartesianMonoidalCategory D
inst✝¹ : ExponentialIdeal i
inst✝ : BraidedCategory C
A B : C
⊢ fst A B ≫ (reflectorAdjunction i).unit.app A =
    ((reflectorAdjunction i).unit.app (A ⊗ B) ≫
        i.map (prodComparison (reflector i) A B) ≫ prodComparison i ((reflector i).obj A) ((reflector i).obj B)) ≫
      fst (i.obj ((reflector i).obj A)) (i.obj ((reflector i).obj B))
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 H G : C ⥤ V
inst✝¹ : DayConvolution F G
ℌ : DayConvolutionInternalHom F (F ⊛ G) H
inst✝ : DayConvolution F H
x y : C
⊢ ((DayConvolution.corepresentableBy F G).homEquiv (DayConvolution.map (𝟙 F) ℌ.coev_app ≫ ℌ.ev_app)).app (x, y) =
    ((DayConvolution.corepresentableBy F G).homEquiv (𝟙 (F ⊛ G))).app (x, y)

Tactic:
apply MonoidalClosed.curry_injective

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 H G : C ⥤ V
inst✝¹ : DayConvolution F G
ℌ : DayConvolutionInternalHom F (F ⊛ G) H
inst✝ : DayConvolution F H
x y : C
⊢ MonoidalClosed.curry
      (((DayConvolution.corepresentableBy F G).homEquiv (DayConvolution.map (𝟙 F) ℌ.coev_app ≫ ℌ.ev_app)).app (x, y)) =
    MonoidalClosed.curry (((DayConvolution.corepresentableBy F G).homEquiv (𝟙 (F ⊛ G))).app (x, y))
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: 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.tensorBimod Q).tensorBimod L).actRight ≫ hom P Q L = hom P Q L ▷ U.X ≫ (P.tensorBimod (Q.tensorBimod L)).actRight

Tactic:
by
  dsimp; dsimp [hom, homAux]
  refine (cancel_epi ((tensorRight _).map (coequalizer.π _ _))).1 ?_
  simp only [Functor.flip_obj_map, curriedTensor_map_app]
  slice_lhs 1 2 => rw [TensorBimod.π_tensor_id_actRight]
  slice_lhs 3 4 => rw [coequalizer.π_desc]
  slice_rhs 1 2 => rw [← comp_whiskerRight, coequalizer.π_desc, comp_whiskerRight]
  refine (cancel_epi ((tensorRight _ ⋙ tensorRight _).map (coequalizer.π _ _))).1 ?_
  dsimp; dsimp [TensorBimod.X]
  slice_lhs 1 2 => rw [associator_naturality_left]
  slice_lhs 2 3 => rw [← whisker_exchange]
  slice_lhs 3 5 => rw [π_tensor_id_preserves_coequalizer_inv_desc]
  slice_lhs 2 3 => rw [associator_naturality_right]
  slice_rhs 1 3 =>
    rw [← comp_whiskerRight, ← comp_whiskerRight, π_tensor_id_preserves_coequalizer_inv_desc,
      comp_whiskerRight, comp_whiskerRight]
  slice_rhs 3 4 => erw [TensorBimod.π_tensor_id_actRight P (Q.tensorBimod L)]
  slice_rhs 2 3 => erw [associator_naturality_middle]
  dsimp
  slice_rhs 3 4 =>
    rw [← whiskerLeft_comp, TensorBimod.π_tensor_id_actRight, whiskerLeft_comp, whiskerLeft_comp]
  monoidal

Goal state after:
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
⊢ (Δ ⊗ₘ Δ) ≫
      (α_ A A (A ⊗ A)).hom ≫
        A ◁ (α_ A A A).inv ≫
          A ◁ (β_ A A).hom ▷ A ≫
            (α_ A (A ⊗ A) A).inv ≫
              (α_ A A A).inv ▷ A ≫ μ ▷ A ▷ A ≫ (α_ A A A).hom ≫ A ◁ (β_ A A).hom ≫ A ◁ (𝒮 ⊗ₘ 𝒮) ≫ A ◁ μ ≫ μ =
    (ε ⊗ₘ ε) ≫ (λ_ (𝟙_ C)).hom ≫ η

Tactic:
slice_lhs 7 8 =>
    rw [associator_naturality_left]
  slice_lhs 8 9 =>
    rw [← whisker_exchange]
  slice_lhs 9 10 =>
    rw [← whisker_exchange]
  slice_lhs 11 12 =>
    rw [MonObj.mul_assoc_flip]
  slice_lhs 10 11 =>
    rw [associator_inv_naturality_left]
  slice_lhs 11 12 =>
    simp only [← comp_whiskerRight]
    rw [MonObj.mul_assoc]
    simp only [comp_whiskerRight]
  rw [tensorHom_def]
  rw [tensor_whiskerLeft _ _ (β_ A A).hom]
  rw [pentagon_inv_inv_hom_hom_inv_assoc]
  slice_lhs 7 8 =>
    rw [Iso.inv_hom_id]
  rw [Category.id_comp]
  slice_lhs 5 7 =>
    simp only [← whiskerLeft_comp]
    rw [← BraidedCategory.hexagon_forward]
    simp only [whiskerLeft_comp]
  simp only [tensor_whiskerLeft, Category.assoc, Iso.inv_hom_id_assoc, pentagon_inv_inv_hom_inv_inv,
    whisker_assoc, MonObj.mul_assoc, whiskerLeft_inv_hom_assoc]
  slice_lhs 3 4 =>
    simp only [← whiskerLeft_comp]
    rw [BraidedCategory.braiding_naturality_right]
    simp only [whiskerLeft_comp]
  rw [tensorHom_def']
  simp only [whiskerLeft_comp]
  slice_lhs 5 6 =>
    simp only [← whiskerLeft_comp]
    rw [← associator_naturality_right]
    simp only [whiskerLeft_comp]
  slice_lhs 4 5 =>
    simp only [← whiskerLeft_comp]
    rw [← whisker_exchange]
    simp only [whiskerLeft_comp]
  slice_lhs 5 9 =>
    simp only [← whiskerLeft_comp]
    rw [associator_inv_naturality_middle_assoc, Iso.hom_inv_id_assoc]
    simp only [← comp_whiskerRight]
    rw [antipode_right]
    simp only [comp_whiskerRight]
    simp only [whiskerLeft_comp]
  slice_lhs 6 7 =>
    simp only [← whiskerLeft_comp]
    rw [MonObj.one_mul]
  slice_lhs 3 4 =>
    simp only [← whiskerLeft_comp]
    rw [← BraidedCategory.braiding_naturality_left]
    simp only [whiskerLeft_comp]
  slice_lhs 4 5 =>
    simp only [← whiskerLeft_comp]
    rw [← BraidedCategory.braiding_naturality_right]
    simp only [whiskerLeft_comp]
  rw [← associator_naturality_middle_assoc]
  simp only [braiding_tensorUnit_right, whiskerLeft_comp]
  slice_lhs 6 7 =>
    simp only [← whiskerLeft_comp]
    rw [Iso.inv_hom_id]
  simp only [whiskerLeft_id, Category.id_comp]
  slice_lhs 5 6 =>
    rw [whiskerLeft_rightUnitor, Category.assoc, ← rightUnitor_naturality]
  rw [associator_inv_naturality_right_assoc, Iso.hom_inv_id_assoc]
  slice_lhs 3 4 =>
    rw [whisker_exchange]
  slice_lhs 1 3 =>
    simp only [← comp_whiskerRight]
    rw [antipode_right]
    simp only [comp_whiskerRight]
  slice_lhs 2 3 =>
    rw [← whisker_exchange]
  slice_lhs 1 2 =>
    rw [← tensorHom_def]
  slice_lhs 2 3 =>
    rw [rightUnitor_naturality]
  monoidal

Goal state after:
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
⊢ μ ≫ 𝒮 = (𝒮 ⊗ₘ 𝒮) ≫ (β_ A A).hom ≫ μ

Tactic:
apply left_inv_eq_right_inv
    (M := Conv (A ⊗ A) A)
    (a := μ[A])

Goal state after:
case hba
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ μ ≫ 𝒮 * μ = 1

case hac
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ μ * (𝒮 ⊗ₘ 𝒮) ≫ (β_ A A).hom ≫ μ = 1
Module: Mathlib.CategoryTheory.Monoidal.Internal.Module

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A : AlgCat R
x y z : ↑(of R ↑A)
⊢ (Hom.hom (↟(mul' R ↑A))) (x ⊗ₜ[R] y, z).1 * LinearMap.id (x ⊗ₜ[R] y, z).2 =
    (Hom.hom (↟(mul' R ↑A)))
      ((Hom.hom (MonoidalCategoryStruct.whiskerLeft (of R ↑A) (↟(mul' R ↑A))))
        ((Hom.hom (MonoidalCategoryStruct.associator (of R ↑A) (of R ↑A) (of R ↑A)).hom)
          (((TensorProduct.mk R ↑(MonoidalCategoryStruct.tensorObj (of R ↑A) (of R ↑A)) ↑A) (x ⊗ₜ[R] y)) z)))

Tactic:
LinearMap.mul'_apply

Goal state after:
R : Type u
inst✝ : CommRing R
A : AlgCat R
x y z : ↑(of R ↑A)
⊢ x * y * LinearMap.id (x ⊗ₜ[R] y, z).2 =
    (Hom.hom (↟(mul' R ↑A)))
      ((Hom.hom (MonoidalCategoryStruct.whiskerLeft (of R ↑A) (↟(mul' R ↑A))))
        ((Hom.hom (MonoidalCategoryStruct.associator (of R ↑A) (of R ↑A) (of R ↑A)).hom)
          (((TensorProduct.mk R ↑(MonoidalCategoryStruct.tensorObj (of R ↑A) (of R ↑A)) ↑A) (x ⊗ₜ[R] y)) z)))
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution

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
F G : C ⥤ V
inst✝ : DayConvolution F G
x x' y : C
f : x ⟶ x'
⊢ F.map f ▷ G.obj y ≫ (unit F G).app (x', y) = (unit F G).app (x, y) ≫ (F ⊛ G).map (f ▷ y)

Tactic:
by
  simpa [tensorHom_def] using (unit F G).naturality (f ×ₘ 𝟙 _)

Goal state after: