mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Join.Pseudofunctor

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : Category.{v_1, u_1} A
inst✝¹ : Category.{v_2, u_2} B
inst✝ : Category.{v_3, u_3} C
F : B ⥤ C
⊢ mapWhiskerLeft (𝟭 A) F.leftUnitor.hom =
    (mapCompRight A (𝟭 B) F).hom ≫
      Functor.whiskerRight mapPairId.hom (mapPair (𝟭 A) F) ≫ (mapPair (𝟭 A) F).leftUnitor.hom

Tactic:
apply natTrans_ext

Goal state after:
case h₁
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : Category.{v_1, u_1} A
inst✝¹ : Category.{v_2, u_2} B
inst✝ : Category.{v_3, u_3} C
F : B ⥤ C
⊢ (inclLeft A B).whiskerLeft (mapWhiskerLeft (𝟭 A) F.leftUnitor.hom) =
    (inclLeft A B).whiskerLeft
      ((mapCompRight A (𝟭 B) F).hom ≫
        Functor.whiskerRight mapPairId.hom (mapPair (𝟭 A) F) ≫ (mapPair (𝟭 A) F).leftUnitor.hom)

case h₂
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : Category.{v_1, u_1} A
inst✝¹ : Category.{v_2, u_2} B
inst✝ : Category.{v_3, u_3} C
F : B ⥤ C
⊢ (inclRight A B).whiskerLeft (mapWhiskerLeft (𝟭 A) F.leftUnitor.hom) =
    (inclRight A B).whiskerLeft
      ((mapCompRight A (𝟭 B) F).hom ≫
        Functor.whiskerRight mapPairId.hom (mapPair (𝟭 A) F) ≫ (mapPair (𝟭 A) F).leftUnitor.hom)
Module: Mathlib.CategoryTheory.Join.Pseudofunctor

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : Category.{v_1, u_1} A
inst✝¹ : Category.{v_2, u_2} B
inst✝ : Category.{v_3, u_3} C
F : A ⥤ B
⊢ mapWhiskerRight F.leftUnitor.hom (𝟭 C) =
    (mapCompLeft C (𝟭 A) F).hom ≫
      Functor.whiskerRight mapPairId.hom (mapPair F (𝟭 C)) ≫ (mapPair F (𝟭 C)).leftUnitor.hom

Tactic:
apply natTrans_ext

Goal state after:
case h₁
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : Category.{v_1, u_1} A
inst✝¹ : Category.{v_2, u_2} B
inst✝ : Category.{v_3, u_3} C
F : A ⥤ B
⊢ (inclLeft A C).whiskerLeft (mapWhiskerRight F.leftUnitor.hom (𝟭 C)) =
    (inclLeft A C).whiskerLeft
      ((mapCompLeft C (𝟭 A) F).hom ≫
        Functor.whiskerRight mapPairId.hom (mapPair F (𝟭 C)) ≫ (mapPair F (𝟭 C)).leftUnitor.hom)

case h₂
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : Category.{v_1, u_1} A
inst✝¹ : Category.{v_2, u_2} B
inst✝ : Category.{v_3, u_3} C
F : A ⥤ B
⊢ (inclRight A C).whiskerLeft (mapWhiskerRight F.leftUnitor.hom (𝟭 C)) =
    (inclRight A C).whiskerLeft
      ((mapCompLeft C (𝟭 A) F).hom ≫
        Functor.whiskerRight mapPairId.hom (mapPair F (𝟭 C)) ≫ (mapPair F (𝟭 C)).leftUnitor.hom)
Module: Mathlib.CategoryTheory.Join.Pseudofunctor

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : Category.{v_1, u_1} A
inst✝¹ : Category.{v_2, u_2} B
inst✝ : Category.{v_3, u_3} C
F : B ⥤ C
⊢ mapWhiskerLeft (𝟭 A) F.rightUnitor.hom =
    (mapCompRight A F (𝟭 C)).hom ≫ (mapPair (𝟭 A) F).whiskerLeft mapPairId.hom ≫ (mapPair (𝟭 A) F).rightUnitor.hom

Tactic:
apply natTrans_ext

Goal state after:
case h₁
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : Category.{v_1, u_1} A
inst✝¹ : Category.{v_2, u_2} B
inst✝ : Category.{v_3, u_3} C
F : B ⥤ C
⊢ (inclLeft A B).whiskerLeft (mapWhiskerLeft (𝟭 A) F.rightUnitor.hom) =
    (inclLeft A B).whiskerLeft
      ((mapCompRight A F (𝟭 C)).hom ≫ (mapPair (𝟭 A) F).whiskerLeft mapPairId.hom ≫ (mapPair (𝟭 A) F).rightUnitor.hom)

case h₂
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : Category.{v_1, u_1} A
inst✝¹ : Category.{v_2, u_2} B
inst✝ : Category.{v_3, u_3} C
F : B ⥤ C
⊢ (inclRight A B).whiskerLeft (mapWhiskerLeft (𝟭 A) F.rightUnitor.hom) =
    (inclRight A B).whiskerLeft
      ((mapCompRight A F (𝟭 C)).hom ≫ (mapPair (𝟭 A) F).whiskerLeft mapPairId.hom ≫ (mapPair (𝟭 A) F).rightUnitor.hom)
Module: Mathlib.CategoryTheory.Join.Pseudofunctor

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : Category.{v_1, u_1} A
inst✝¹ : Category.{v_2, u_2} B
inst✝ : Category.{v_3, u_3} C
F : A ⥤ B
⊢ mapWhiskerRight F.rightUnitor.hom (𝟭 C) =
    (mapCompLeft C F (𝟭 B)).hom ≫ (mapPair F (𝟭 C)).whiskerLeft mapPairId.hom ≫ (mapPair F (𝟭 C)).rightUnitor.hom

Tactic:
apply natTrans_ext

Goal state after:
case h₁
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : Category.{v_1, u_1} A
inst✝¹ : Category.{v_2, u_2} B
inst✝ : Category.{v_3, u_3} C
F : A ⥤ B
⊢ (inclLeft A C).whiskerLeft (mapWhiskerRight F.rightUnitor.hom (𝟭 C)) =
    (inclLeft A C).whiskerLeft
      ((mapCompLeft C F (𝟭 B)).hom ≫ (mapPair F (𝟭 C)).whiskerLeft mapPairId.hom ≫ (mapPair F (𝟭 C)).rightUnitor.hom)

case h₂
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : Category.{v_1, u_1} A
inst✝¹ : Category.{v_2, u_2} B
inst✝ : Category.{v_3, u_3} C
F : A ⥤ B
⊢ (inclRight A C).whiskerLeft (mapWhiskerRight F.rightUnitor.hom (𝟭 C)) =
    (inclRight A C).whiskerLeft
      ((mapCompLeft C F (𝟭 B)).hom ≫ (mapPair F (𝟭 C)).whiskerLeft mapPairId.hom ≫ (mapPair F (𝟭 C)).rightUnitor.hom)
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
F F' : C ⋆ D ⥤ E
α : F ⟶ F'
⊢ mkNatTrans ((inclLeft C D).whiskerLeft α) ((inclRight C D).whiskerLeft α) ⋯ = α

Tactic:
apply natTrans_ext

Goal state after:
case h₁
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F F' : C ⋆ D ⥤ E
α : F ⟶ F'
⊢ (inclLeft C D).whiskerLeft (mkNatTrans ((inclLeft C D).whiskerLeft α) ((inclRight C D).whiskerLeft α) ⋯) =
    (inclLeft C D).whiskerLeft α

case h₂
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F F' : C ⋆ D ⥤ E
α : F ⟶ F'
⊢ (inclRight C D).whiskerLeft (mkNatTrans ((inclLeft C D).whiskerLeft α) ((inclRight C D).whiskerLeft α) ⋯) =
    (inclRight C D).whiskerLeft α
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
F F' F'' : C ⋆ D ⥤ E
αₗ : inclLeft C D ⋙ F ⟶ inclLeft C D ⋙ F'
αᵣ : inclRight C D ⋙ F ⟶ inclRight C D ⋙ F'
βₗ : inclLeft C D ⋙ F' ⟶ inclLeft C D ⋙ F''
βᵣ : inclRight C D ⋙ F' ⟶ inclRight C D ⋙ F''
h :
  whiskerRight (edgeTransform C D) F ≫ (Prod.snd C D).whiskerLeft αᵣ =
    (Prod.fst C D).whiskerLeft αₗ ≫ whiskerRight (edgeTransform C D) F'
h' :
  whiskerRight (edgeTransform C D) F' ≫ (Prod.snd C D).whiskerLeft βᵣ =
    (Prod.fst C D).whiskerLeft βₗ ≫ whiskerRight (edgeTransform C D) F''
⊢ mkNatTrans (αₗ ≫ βₗ) (αᵣ ≫ βᵣ) ⋯ = mkNatTrans αₗ αᵣ h ≫ mkNatTrans βₗ βᵣ h'

Tactic:
apply natTrans_ext

Goal state after:
case h₁
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F F' F'' : C ⋆ D ⥤ E
αₗ : inclLeft C D ⋙ F ⟶ inclLeft C D ⋙ F'
αᵣ : inclRight C D ⋙ F ⟶ inclRight C D ⋙ F'
βₗ : inclLeft C D ⋙ F' ⟶ inclLeft C D ⋙ F''
βᵣ : inclRight C D ⋙ F' ⟶ inclRight C D ⋙ F''
h :
  whiskerRight (edgeTransform C D) F ≫ (Prod.snd C D).whiskerLeft αᵣ =
    (Prod.fst C D).whiskerLeft αₗ ≫ whiskerRight (edgeTransform C D) F'
h' :
  whiskerRight (edgeTransform C D) F' ≫ (Prod.snd C D).whiskerLeft βᵣ =
    (Prod.fst C D).whiskerLeft βₗ ≫ whiskerRight (edgeTransform C D) F''
⊢ (inclLeft C D).whiskerLeft (mkNatTrans (αₗ ≫ βₗ) (αᵣ ≫ βᵣ) ⋯) =
    (inclLeft C D).whiskerLeft (mkNatTrans αₗ αᵣ h ≫ mkNatTrans βₗ βᵣ h')

case h₂
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F F' F'' : C ⋆ D ⥤ E
αₗ : inclLeft C D ⋙ F ⟶ inclLeft C D ⋙ F'
αᵣ : inclRight C D ⋙ F ⟶ inclRight C D ⋙ F'
βₗ : inclLeft C D ⋙ F' ⟶ inclLeft C D ⋙ F''
βᵣ : inclRight C D ⋙ F' ⟶ inclRight C D ⋙ F''
h :
  whiskerRight (edgeTransform C D) F ≫ (Prod.snd C D).whiskerLeft αᵣ =
    (Prod.fst C D).whiskerLeft αₗ ≫ whiskerRight (edgeTransform C D) F'
h' :
  whiskerRight (edgeTransform C D) F' ≫ (Prod.snd C D).whiskerLeft βᵣ =
    (Prod.fst C D).whiskerLeft βₗ ≫ whiskerRight (edgeTransform C D) F''
⊢ (inclRight C D).whiskerLeft (mkNatTrans (αₗ ≫ βₗ) (αᵣ ≫ βᵣ) ⋯) =
    (inclRight C D).whiskerLeft (mkNatTrans αₗ αᵣ h ≫ mkNatTrans βₗ βᵣ h')
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), HasCoproductsOfShape (a ⟶ b) D
J : Type u_1
inst✝ : Category.{v_1, u_1} J
hJ : IsConnected J
G : Over F
x✝ : limitsOfShape (fun f ↦ Equifibered f.hom) J G
i j : C
f : i ⟶ j
c : J ⥤ Over F
α : (const J).obj G ⟶ c
hc : IsLimit { pt := G, π := α }
H : ∀ (j : J), Equifibered ({ diag := c, π := α, isLimit := hc }.diag.obj j).hom
s : PullbackCone (G.hom.app j) (F.map f)
hcᵢ : IsLimit ((Over.forget F ⋙ (evaluation C D).obj i).mapCone { pt := G, π := α }) :=
  isLimitOfPreserves (Over.forget F ⋙ (evaluation C D).obj i) hc
hcⱼ : IsLimit ((Over.forget F ⋙ (evaluation C D).obj j).mapCone { pt := G, π := α }) :=
  isLimitOfPreserves (Over.forget F ⋙ (evaluation C D).obj j) hc
l : s.pt ⟶ G.left.obj i :=
  hcᵢ.lift
    { pt := s.1, π := { app := fun k ↦ ⋯.lift (s.fst ≫ (Over.Hom.left (α.app k)).app j) s.snd ⋯, naturality := ⋯ } }
k : J
⊢ G.hom.app i = (Over.Hom.left (α.app k)).app i ≫ (c.obj k).hom.app i

Tactic:
simp [← comp_app]

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 ≫
      (Functor.ofOpSequence (functorMap f)).map (homOfLE hh).op ≫
        Pi.π (fun i ↦ if i < m + 1 then M i else N i) m ≫ eqToHom h₁ ≫ eqToHom h₂ =
    Pi.π (fun m ↦ if m < n + 1 then M m else N m) m

Tactic:
slice_lhs 2 4 => rw [ih (by lia)]

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
⊢ 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
Module: Mathlib.CategoryTheory.Limits.SmallComplete

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

Tactic:
exact #(X ⟶ yp)

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
⊢ preservesColimitsOfShape K = ⨅ F, preservesColimit F

Tactic:
by
  ext G
  simp only [preservesColimitsOfShape_iff, iInf_apply, preservesColimit_iff, iInf_Prop_eq]
  exact ⟨fun _ ↦ inferInstance, fun _ ↦ ⟨inferInstance⟩⟩

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

Goal state before:
pp: case assoc
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✝ U✝ V✝ : 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)
g✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ projectMapAux f✝¹ ((f✝.comp g✝).comp h✝) = projectMapAux f✝¹ (f✝.comp (g✝.comp h✝))

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

Goal state after:
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Over

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : C
Y Z : Over X
inst✝ : ChosenPullbacksAlong Z.hom
T✝ : Over X
a : T✝ ⟶ Y
b : T✝ ⟶ Z
m : T✝ ⟶ (binaryFan Y Z).pt
h₁ : m ≫ (binaryFan Y Z).fst = a
h₂ : m ≫ (binaryFan Y Z).snd = b
⊢ m = Over.homMk (lift (Over.Hom.left a) (Over.Hom.left b) ⋯) ⋯

Tactic:
ext
      dsimp [Over.map, Comma.mapRight]
      cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Action.End

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
F : C ⥤ (D ⥤ D)ᴹᵒᵖ
inst✝ : F.Monoidal
c₁ c₁' c₂ c₂' : C
c₃ c₃' : D
f : c₁ ⟶ c₁'
g : c₂ ⟶ c₂'
h : c₃ ⟶ c₃'
⊢ ((fun {c c'} f d ↦ (F.map f).unmop.app d) (f ⊗ₘ g) c₃ ≫
        (fun c x x_1 f ↦ (F.obj c).unmop.map f) (c₁' ⊗ c₂') c₃ c₃' h) ≫
      ((Functor.Monoidal.μIso F c₁' c₂').unmop.app c₃').symm.hom =
    ((Functor.Monoidal.μIso F c₁ c₂).unmop.app c₃).symm.hom ≫
      (fun {c c'} f d ↦ (F.map f).unmop.app d) f ((F.obj c₂).unmop.obj c₃) ≫
        (fun c x x_1 f ↦ (F.obj c).unmop.map f) c₁' ((F.obj c₂).unmop.obj c₃) ((F.obj c₂').unmop.obj c₃')
          ((fun {c c'} f d ↦ (F.map f).unmop.app d) g c₃ ≫ (fun c x x_1 f ↦ (F.obj c).unmop.map f) c₂' c₃ c₃' h)

Tactic:
have e := congrArg (fun t ↦ t.unmop.app c₃) <|
      Functor.OplaxMonoidal.δ_natural F f g

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
F : C ⥤ (D ⥤ D)ᴹᵒᵖ
inst✝ : F.Monoidal
c₁ c₁' c₂ c₂' : C
c₃ c₃' : D
f : c₁ ⟶ c₁'
g : c₂ ⟶ c₂'
h : c₃ ⟶ c₃'
e :
  (Functor.OplaxMonoidal.δ F c₁ c₂ ≫ (F.map f ⊗ₘ F.map g)).unmop.app c₃ =
    (F.map (f ⊗ₘ g) ≫ Functor.OplaxMonoidal.δ F c₁' c₂').unmop.app c₃
⊢ ((fun {c c'} f d ↦ (F.map f).unmop.app d) (f ⊗ₘ g) c₃ ≫
        (fun c x x_1 f ↦ (F.obj c).unmop.map f) (c₁' ⊗ c₂') c₃ c₃' h) ≫
      ((Functor.Monoidal.μIso F c₁' c₂').unmop.app c₃').symm.hom =
    ((Functor.Monoidal.μIso F c₁ c₂).unmop.app c₃).symm.hom ≫
      (fun {c c'} f d ↦ (F.map f).unmop.app d) f ((F.obj c₂).unmop.obj c₃) ≫
        (fun c x x_1 f ↦ (F.obj c).unmop.map f) c₁' ((F.obj c₂).unmop.obj c₃) ((F.obj c₂').unmop.obj c₃')
          ((fun {c c'} f d ↦ (F.map f).unmop.app d) g c₃ ≫ (fun c x x_1 f ↦ (F.obj c).unmop.map f) c₂' c₃ c₃' h)
Module: Mathlib.CategoryTheory.Monoidal.Ring

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : BraidedCategory C
R : C
inst✝ : RingObj R
⊢ ∀ {X : C} (a b c : X ⟶ R), (a + b) * c = a * c + b * c

Tactic:
rw [← add_mul_iff, RingObj.add_mul R]

Goal state after:
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 H : C ⥤ V
η : F ⟶ G
inst✝³ : DayConvolution F H
inst✝² : DayConvolution H F
inst✝¹ : DayConvolution G H
inst✝ : DayConvolution H G
⊢ map (𝟙 H) η ≫ (braiding H G).hom = (braiding H F).hom ≫ map η (𝟙 H)

Tactic:
by
  apply Functor.hom_ext_of_isLeftKanExtension (H ⊛ F) (unit H F)
  ext ⟨_, _⟩
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.DayFunctor

Goal state before:
pp: case mk
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
β : F ⟶ G
natTrans✝ : F.functor ⟶ G.functor
h : { natTrans := natTrans✝ }.natTrans = β.natTrans
⊢ { natTrans := natTrans✝ } = β

Tactic:
cases β

Goal state after:
case mk.mk
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
natTrans✝¹ natTrans✝ : F.functor ⟶ G.functor
h : { natTrans := natTrans✝¹ }.natTrans = { natTrans := natTrans✝ }.natTrans
⊢ { natTrans := natTrans✝¹ } = { natTrans := natTrans✝ }
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

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

pp: 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

Tactic:
· rw [Conv.mul_eq, Conv.one_eq]
    simp only [comp_whiskerRight, tensor_whiskerLeft, MonObj.tensorObj.mul_def, Category.assoc,
      MonObj.tensorObj.one_def]
    simp only [tensorμ]
    simp only [Category.assoc, Iso.inv_hom_id_assoc]
    exact antipode_comul₁ A

Goal state after:
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.Hopf_

Goal state before:
pp: case a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ (ρ_ A).hom ≫ μ

pp: case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| Δ ▷ A

pp: case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| (A ◁ 𝒮) ▷ A

pp: case a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| (α_ A A A).hom

pp: case a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ A ◁ ε

Tactic:
rw [whiskerLeft_rightUnitor, Category.assoc, ← rightUnitor_naturality]

Goal state after:
case a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| (α_ A A (𝟙_ C)).inv ≫ μ ▷ 𝟙_ C ≫ (ρ_ A).hom

case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| Δ ▷ A

case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| (A ◁ 𝒮) ▷ A

case a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| (α_ A A A).hom

case a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ A ◁ ε
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided

Goal state before:
pp: case e_g.e_f
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ (α_ X Y X).inv ≫ (β_ X Y).hom ▷ X =
    inv (X ◁ (β_ Y X).inv) ≫
      (α_ X X Y).inv ≫
        (β_ X X).hom ▷ Y ≫
          (α_ X X Y).hom ≫
            X ◁ (β_ X Y).hom ≫ (α_ X Y X).inv ≫ (β_ Y X).inv ▷ X ≫ (α_ Y X X).hom ≫ Y ◁ (β_ X X).inv ≫ (α_ Y X X).inv

Tactic:
← assoc

Goal state after:
case e_g.e_f
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ (α_ X Y X).inv ≫ (β_ X Y).hom ▷ X =
    (inv (X ◁ (β_ Y X).inv) ≫ (α_ X X Y).inv) ≫
      (β_ X X).hom ▷ Y ≫
        (α_ X X Y).hom ≫
          X ◁ (β_ X Y).hom ≫ (α_ X Y X).inv ≫ (β_ Y X).inv ▷ X ≫ (α_ Y X X).hom ≫ Y ◁ (β_ X X).inv ≫ (α_ Y X X).inv
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided

Goal state before:
pp: case e_g.e_f
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ (α_ X Y X).inv ≫ (β_ X Y).hom ▷ X =
    (inv (X ◁ (β_ Y X).inv) ≫ (α_ X X Y).inv) ≫
      (β_ X X).hom ▷ Y ≫
        (α_ X X Y).hom ≫
          X ◁ (β_ X Y).hom ≫ (α_ X Y X).inv ≫ (β_ Y X).inv ▷ X ≫ (α_ Y X X).hom ≫ Y ◁ (β_ X X).inv ≫ (α_ Y X X).inv

Tactic:
← assoc

Goal state after:
case e_g.e_f
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ (α_ X Y X).inv ≫ (β_ X Y).hom ▷ X =
    ((inv (X ◁ (β_ Y X).inv) ≫ (α_ X X Y).inv) ≫ (β_ X X).hom ▷ Y) ≫
      (α_ X X Y).hom ≫
        X ◁ (β_ X Y).hom ≫ (α_ X Y X).inv ≫ (β_ Y X).inv ▷ X ≫ (α_ Y X X).hom ≫ Y ◁ (β_ X X).inv ≫ (α_ Y X X).inv
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided

Goal state before:
pp: case e_g.e_f
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ (α_ X Y X).inv ≫ (β_ X Y).hom ▷ X =
    ((inv (X ◁ (β_ Y X).inv) ≫ (α_ X X Y).inv) ≫ (β_ X X).hom ▷ Y) ≫
      (α_ X X Y).hom ≫
        X ◁ (β_ X Y).hom ≫ (α_ X Y X).inv ≫ (β_ Y X).inv ▷ X ≫ (α_ Y X X).hom ≫ Y ◁ (β_ X X).inv ≫ (α_ Y X X).inv

Tactic:
← assoc

Goal state after:
case e_g.e_f
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ (α_ X Y X).inv ≫ (β_ X Y).hom ▷ X =
    (((inv (X ◁ (β_ Y X).inv) ≫ (α_ X X Y).inv) ≫ (β_ X X).hom ▷ Y) ≫ (α_ X X Y).hom) ≫
      X ◁ (β_ X Y).hom ≫ (α_ X Y X).inv ≫ (β_ Y X).inv ▷ X ≫ (α_ Y X X).hom ≫ Y ◁ (β_ X X).inv ≫ (α_ Y X X).inv
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided

Goal state before:
pp: case e_g.e_f
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ (α_ X Y X).inv ≫ (β_ X Y).hom ▷ X =
    (((inv (X ◁ (β_ Y X).inv) ≫ (α_ X X Y).inv) ≫ (β_ X X).hom ▷ Y) ≫ (α_ X X Y).hom) ≫
      X ◁ (β_ X Y).hom ≫ (α_ X Y X).inv ≫ (β_ Y X).inv ▷ X ≫ (α_ Y X X).hom ≫ Y ◁ (β_ X X).inv ≫ (α_ Y X X).inv

Tactic:
← assoc

Goal state after:
case e_g.e_f
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ (α_ X Y X).inv ≫ (β_ X Y).hom ▷ X =
    ((((inv (X ◁ (β_ Y X).inv) ≫ (α_ X X Y).inv) ≫ (β_ X X).hom ▷ Y) ≫ (α_ X X Y).hom) ≫ X ◁ (β_ X Y).hom) ≫
      (α_ X Y X).inv ≫ (β_ Y X).inv ▷ X ≫ (α_ Y X X).hom ≫ Y ◁ (β_ X X).inv ≫ (α_ Y X X).inv
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided

Goal state before:
pp: case e_g.e_f
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ (α_ X Y X).inv ≫ (β_ X Y).hom ▷ X =
    ((((inv (X ◁ (β_ Y X).inv) ≫ (α_ X X Y).inv) ≫ (β_ X X).hom ▷ Y) ≫ (α_ X X Y).hom) ≫ X ◁ (β_ X Y).hom) ≫
      (α_ X Y X).inv ≫ (β_ Y X).inv ▷ X ≫ (α_ Y X X).hom ≫ Y ◁ (β_ X X).inv ≫ (α_ Y X X).inv

Tactic:
← assoc

Goal state after:
case e_g.e_f
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ (α_ X Y X).inv ≫ (β_ X Y).hom ▷ X =
    (((((inv (X ◁ (β_ Y X).inv) ≫ (α_ X X Y).inv) ≫ (β_ X X).hom ▷ Y) ≫ (α_ X X Y).hom) ≫ X ◁ (β_ X Y).hom) ≫
        (α_ X Y X).inv) ≫
      (β_ Y X).inv ▷ X ≫ (α_ Y X X).hom ≫ Y ◁ (β_ X X).inv ≫ (α_ Y X X).inv