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✝³ : Y.HasTensor Z
inst✝² : Z.HasTensor Y
inst✝¹ : X.HasTensor Z
inst✝ : Z.HasTensor X
f : X ⟶ Y
⊢ whiskerRight f Z ≫ (braiding Y Z).hom = (braiding X Z).hom ≫ whiskerLeft Z f

Tactic:
dsimp [braiding]
  cat_disch

Goal state after:
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 : GradedObject I C
inst✝² : SymmetricCategory C
inst✝¹ : X.HasTensor Y
inst✝ : Y.HasTensor X
⊢ (braiding X Y).hom ≫ (braiding Y X).hom = 𝟙 (tensorObj X Y)

Tactic:
dsimp [braiding]
  cat_disch

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

Goal state before:
pp: case refine_3
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
g₁ : Y ⟶ X₁
g₂ : Y ⟶ X₂
g₃ : Y ⟶ X₃
b : Y ⟶ S
hg₁ : g₁ ≫ f₁ = b
hg₂ : g₂ ≫ f₂ = b
hg₃ : g₃ ≫ f₃ = b
φ₁₂ : Y ⟶ h₁₂.pullback
w₁ : φ₁₂ ≫ h₁₂.p₁ = g₁
w₂ : φ₁₂ ≫ h₁₂.p₂ = g₂
φ₂₃ : Y ⟶ h₂₃.pullback
w₂' : φ₂₃ ≫ h₂₃.p₁ = g₂
w₃ : φ₂₃ ≫ h₂₃.p₂ = g₃
φ : Y ⟶ h.chosenPullback.pullback
w₁₂ : φ ≫ h.chosenPullback.p₁ = φ₁₂
w₂₃ : φ ≫ h.chosenPullback.p₂ = φ₂₃
⊢ φ ≫ h.p₃ = φ ≫ h.chosenPullback.p₂ ≫ h₂₃.p₂

Tactic:
← p₂₃,

Goal state after:
case refine_3
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
g₁ : Y ⟶ X₁
g₂ : Y ⟶ X₂
g₃ : Y ⟶ X₃
b : Y ⟶ S
hg₁ : g₁ ≫ f₁ = b
hg₂ : g₂ ≫ f₂ = b
hg₃ : g₃ ≫ f₃ = b
φ₁₂ : Y ⟶ h₁₂.pullback
w₁ : φ₁₂ ≫ h₁₂.p₁ = g₁
w₂ : φ₁₂ ≫ h₁₂.p₂ = g₂
φ₂₃ : Y ⟶ h₂₃.pullback
w₂' : φ₂₃ ≫ h₂₃.p₁ = g₂
w₃ : φ₂₃ ≫ h₂₃.p₂ = g₃
φ : Y ⟶ h.chosenPullback.pullback
w₁₂ : φ ≫ h.chosenPullback.p₁ = φ₁₂
w₂₃ : φ ≫ h.chosenPullback.p₂ = φ₂₃
⊢ φ ≫ h.p₃ = φ ≫ h.p₂₃ ≫ h₂₃.p₂
Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct

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

Tactic:
have : homOfLE (by lia : n ≤ m + 1) =
        homOfLE (by lia : n ≤ m) ≫ homOfLE (by lia : m ≤ m + 1) := by simp

Goal state after:
case 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
n m✝ k m : ℕ
h : n ≤ m
hh : ¬k < m + 1
ih :
  (Functor.ofOpSequence (functorMap f)).map (homOfLE h).op ≫
      Pi.π (fun m ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m) k ≫ eqToHom ⋯ =
    Pi.π (fun i ↦ if x : i < m then M i else N i) k ≫ eqToHom ⋯
this : homOfLE ⋯ = homOfLE ⋯ ≫ homOfLE ⋯
⊢ (Functor.ofOpSequence (functorMap f)).map (homOfLE ⋯).op ≫
      Pi.π (fun m ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m) k ≫ eqToHom ⋯ =
    Pi.π (fun i ↦ if x : i < m + 1 then M i else N i) k ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits

Goal state before:
pp: case refine_2
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 := ⋯ } }
⊢ l ≫ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).snd = s.snd

Tactic:
dsimp
    obtain ⟨k⟩ : Nonempty J := inferInstance
    rw [show G.hom.app i = (α.app k).left.app i ≫ (c.obj k).hom.app i by simp [← comp_app]]
    exact (hcᵢ.fac_assoc ..).trans (by simp)

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

Goal state before:
pp: J : Type u_1
inst✝⁴ : Category.{v_1, u_1} J
K : Type u_2
inst✝³ : Category.{v_2, u_2} K
C : Type u_3
inst✝² : Category.{v_3, u_3} C
F✝ : J ⥤ C
D : Type u_4
inst✝¹ : Category.{v_4, u_4} D
G : K ⥤ D
F : J ⥤ C
inst✝ : HasWeakLimit F
j j' : J
hj : j = j'
⊢ F.obj j = F.obj j'

Tactic:
subst hj; rfl

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

Goal state before:
pp: case h.ρ_hom
C : Type u
motive : {X Y : F C} → (X ⟶ Y) → Prop
X✝ Y : F C
id : ∀ (X : F C), motive (𝟙 X)
α_hom : ∀ (X Y Z : F C), motive (α_ X Y Z).hom
α_inv : ∀ (X Y Z : F C), motive (α_ X Y Z).inv
l_hom : ∀ (X : F C), motive (λ_ X).hom
l_inv : ∀ (X : F C), motive (λ_ X).inv
ρ_hom : ∀ (X : F C), motive (ρ_ X).hom
ρ_inv : ∀ (X : F C), motive (ρ_ X).inv
comp : ∀ {X Y Z : F C} (f : X ⟶ Y) (g : Y ⟶ Z), motive f → motive g → motive (f ≫ g)
whiskerLeft : ∀ (X : F C) {Y Z : F C} (f : Y ⟶ Z), motive f → motive (X ◁ f)
whiskerRight : ∀ {X Y : F C} (f : X ⟶ Y) (Z : F C), motive f → motive (f ▷ Z)
X : F C
⊢ motive ⟦Hom.ρ_hom X⟧

Tactic:
exact ρ_hom X

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
c : C
d : D
inst✝ : IsIso (L.map (adj.unit.app ((ihom d).obj (R.obj c)) ⊗ₘ adj.unit.app d))
⊢ adj.unit.app ((ihom d).obj (R.obj c)) ≫ adjRetraction adj c d = 𝟙 ((𝟭 D).obj ((ihom d).obj (R.obj c)))

Tactic:
by
  suffices (_ ◁ adj.unit.app _) ≫ adjRetractionAux adj c d = (ihom.ev _).app _ by
    simp only [id_obj, adjRetraction, ← curry_natural_left, this]
    simp [curry_eq]
  simp only [id_obj, adjRetractionAux, Functor.map_inv, Functor.comp_map,
    braiding_naturality_right_assoc]
  slice_lhs 2 3 =>
    simp only [← id_tensorHom, ← tensorHom_id, tensorHom_comp_tensorHom, Category.id_comp,
      Category.comp_id]
  slice_lhs 2 4 =>
    rw [← adj.unit_naturality_assoc]
  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
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'))
x✝² : ∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))
x✝¹ : C
x✝ : D
⊢ IsIso (adj.unit.app ((ihom x✝).obj (R.obj x✝¹)))

Tactic:
by
    -- It is enough to show that the unit is a split monomorphism, and the retraction is given
    -- by `adjRetraction` above.
    let _ : Reflective R := { L := L, adj := adj }
    have : IsIso adj.toMonad.μ := μ_iso_of_reflective (R := R)
    dsimp
    rw [← dsimp% [Adjunction.toMonad] adj.toMonad.isSplitMono_iff_isIso_unit]
    exact ⟨⟨adjRetraction adj _ _, adjRetraction_is_retraction adj _ _⟩⟩

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 = X.X ◁ 𝟙 Q.X ≫ Q.actLeft

Tactic:
whiskerLeft_id,

Goal state after:
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 = 𝟙 (X.X ⊗ Q.X) ≫ Q.actLeft
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 : C
inst✝³ : MonObj M
X : D
N : C
inst✝² : MonObj N
e₁ : M ≅ N
inst✝¹ : IsMonHom e₁.hom
Y : D
e₂ : X ≅ Y
inst✝ : ModObj M X
⊢ η ⊵ₗ Y ≫ (e₁.inv ⊙ₗₘ e₂.inv) ≫ γ ≫ e₂.hom = (λₗ Y).hom

Tactic:
have : η ⊵ₗ Y ≫ (e₁.inv ⊙ₗₘ e₂.inv) = _ ⊴ₗ e₂.inv ≫ (η ≫ e₁.inv) ⊵ₗ X := by
      rw [actionHom_def', comp_actionHomLeft, action_exchange_assoc]

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 : C
inst✝³ : MonObj M
X : D
N : C
inst✝² : MonObj N
e₁ : M ≅ N
inst✝¹ : IsMonHom e₁.hom
Y : D
e₂ : X ≅ Y
inst✝ : ModObj M X
this : η ⊵ₗ Y ≫ (e₁.inv ⊙ₗₘ e₂.inv) = 𝟙_ C ⊴ₗ e₂.inv ≫ (η ≫ e₁.inv) ⊵ₗ X
⊢ η ⊵ₗ Y ≫ (e₁.inv ⊙ₗₘ e₂.inv) ≫ γ ≫ e₂.hom = (λₗ Y).hom
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: case a.a
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₁} (tensorRight X)
| P.X ◁ (Q.X ◁ η ≫ Q.actRight)

pp: case a.a
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₁} (tensorRight X)
| coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)

pp: case a
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₁} (tensorRight X)
| (α_ P.X Q.X (𝟙_ C)).hom

Tactic:
actRight_one

Goal state after:
case a.a
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₁} (tensorRight X)
| P.X ◁ (ρ_ Q.X).hom

case a.a
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₁} (tensorRight X)
| coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)

case a
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₁} (tensorRight X)
| (α_ P.X Q.X (𝟙_ C)).hom
Module: Mathlib.CategoryTheory.Monoidal.Closed.Ideal

Goal state before:
pp: 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
X Y : D
⊢ IsIso ((reflectorAdjunction i).unit.app (i.obj X ⊗ i.obj Y))

Tactic:
apply Functor.essImage.unit_isIso

Goal state after:
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
X Y : D
⊢ i.essImage (i.obj X ⊗ i.obj Y)
Module: Mathlib.CategoryTheory.Monoidal.Closed.Ideal

Goal state before:
pp: 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✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) (reflector i)
ir : reflector i ⊣ i := reflectorAdjunction i
L : C ⥤ D := reflector i
η : 𝟭 C ⟶ L ⋙ i := ir.unit
ε : i ⋙ L ⟶ 𝟭 D := ir.counit
B : D
A : C
q : i.obj (L.obj (A ⟹ i.obj B)) ⟶ A ⟹ i.obj B :=
  curry
    ((ir.homEquiv (A ⊗ i.obj (L.obj (A ⟹ i.obj B))) B)
      ((prodComparison L A (i.obj (L.obj (A ⟹ i.obj B))) ≫
          L.obj A ◁ ε.app (L.obj (A ⟹ i.obj B)) ≫ inv (prodComparison (reflector i) A (A ⟹ i.obj B))) ≫
        (ir.homEquiv ((ihom A ⋙ tensorLeft A).obj (i.obj B)) B).symm ((ihom.ev A).app (i.obj B))))
⊢ prodComparison (reflector i) A (A ⟹ i.obj B) ≫
      (reflector i).obj A ◁ 𝟙 ((reflector i).obj (A ⟹ i.obj B)) ≫
        inv (prodComparison (reflector i) A (A ⟹ i.obj B)) ≫
          (ir.homEquiv ((ihom A ⋙ tensorLeft A).obj (i.obj B)) B).symm ((ihom.ev A).app (i.obj B)) =
    (ir.homEquiv (A ⊗ (A ⟹ i.obj B)) B).symm ((ihom.ev A).app (i.obj B))

Tactic:
whiskerLeft_id,

Goal state after:
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✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) (reflector i)
ir : reflector i ⊣ i := reflectorAdjunction i
L : C ⥤ D := reflector i
η : 𝟭 C ⟶ L ⋙ i := ir.unit
ε : i ⋙ L ⟶ 𝟭 D := ir.counit
B : D
A : C
q : i.obj (L.obj (A ⟹ i.obj B)) ⟶ A ⟹ i.obj B :=
  curry
    ((ir.homEquiv (A ⊗ i.obj (L.obj (A ⟹ i.obj B))) B)
      ((prodComparison L A (i.obj (L.obj (A ⟹ i.obj B))) ≫
          L.obj A ◁ ε.app (L.obj (A ⟹ i.obj B)) ≫ inv (prodComparison (reflector i) A (A ⟹ i.obj B))) ≫
        (ir.homEquiv ((ihom A ⋙ tensorLeft A).obj (i.obj B)) B).symm ((ihom.ev A).app (i.obj B))))
⊢ prodComparison (reflector i) A (A ⟹ i.obj B) ≫
      𝟙 ((reflector i).obj A ⊗ (reflector i).obj (A ⟹ i.obj B)) ≫
        inv (prodComparison (reflector i) A (A ⟹ i.obj B)) ≫
          (ir.homEquiv ((ihom A ⋙ tensorLeft A).obj (i.obj B)) B).symm ((ihom.ev A).app (i.obj B)) =
    (ir.homEquiv (A ⊗ (A ⟹ i.obj B)) B).symm ((ihom.ev A).app (i.obj B))
Module: Mathlib.CategoryTheory.Monoidal.Conv

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
M N : C
inst✝¹ : ComonObj M
inst✝ : MonObj N
f : Conv M N
⊢ 1 * f = f

Tactic:
by simp [one_eq, mul_eq, ← whisker_exchange_assoc]

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
M N : C
inst✝¹ : ComonObj M
inst✝ : MonObj N
f : Conv M N
⊢ f * 1 = f

Tactic:
by simp [one_eq, mul_eq, ← whisker_exchange_assoc]

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
this : Δ ≫ 𝒮 ▷ A ≫ μ ≫ ε = ε ≫ η ≫ ε
⊢ 𝒮 ≫ ε = ε

Tactic:
Bimon.mul_counit,

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

Goal state before:
pp: case a.a.a.a.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 ◁ (β_ A A).hom ≫ (α_ A A A).inv ≫ (β_ A A).hom ▷ A ≫ (α_ A A A).hom ≫ A ◁ μ)

pp: case a.a.a.a.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

pp: case a.a.a.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 A).inv

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

pp: case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj 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

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 ◁ Δ

pp: case a.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 ◁ 𝒮 ▷ A

Tactic:
rw [← BraidedCategory.hexagon_reverse_assoc, Iso.inv_hom_id_assoc,
      ← BraidedCategory.braiding_naturality_left]

Goal state after:
case a.a.a.a.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 A A).inv ≫ μ ▷ A ≫ (β_ A A).hom)

case a.a.a.a.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

case a.a.a.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 A).inv

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

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

case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj 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 ◁ Δ

case a.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 ◁ 𝒮 ▷ A
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)
R S T U : Mon C
P : Bimod R S
Q : Bimod S T
L : Bimod T U
⊢ P.actRight ▷ (Q.tensorBimod L).X ≫ invAux P Q L =
    ((α_ P.X S.X (Q.tensorBimod L).X).hom ≫ P.X ◁ (Q.tensorBimod L).actLeft) ≫ invAux P Q L

Tactic:
dsimp [invAux]
      refine (cancel_epi ((tensorLeft _).map (coequalizer.π _ _))).1 ?_
      dsimp [TensorBimod.X]
      slice_lhs 1 2 => rw [whisker_exchange]
      slice_lhs 2 4 => rw [id_tensor_π_preserves_coequalizer_inv_desc]
      slice_lhs 1 2 => rw [associator_inv_naturality_left]
      slice_lhs 2 3 =>
        rw [← comp_whiskerRight, coequalizer.condition, comp_whiskerRight, comp_whiskerRight]
      slice_rhs 1 2 => rw [associator_naturality_right]
      slice_rhs 2 3 =>
        rw [← whiskerLeft_comp, TensorBimod.whiskerLeft_π_actLeft,
          whiskerLeft_comp, whiskerLeft_comp]
      slice_rhs 4 6 => rw [id_tensor_π_preserves_coequalizer_inv_desc]
      slice_rhs 3 4 => rw [associator_inv_naturality_middle]
      monoidal

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

Goal state before:
pp: J : Type w
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimitsOfShape J C
inst✝ : MonoidalCategory C
F : J ⥤ C
j : J
⊢ (ρ_ (limit F)).hom ≫ limit.π F j =
    limit F ◁ { pt := 𝟙_ C, π := { app := fun x ↦ 𝟙 (𝟙_ C), naturality := ⋯ } }.π.app j ≫
      (ρ_ (limit F)).hom ≫ limit.π F j

Tactic:
whiskerLeft_id,

Goal state after:
J : Type w
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimitsOfShape J C
inst✝ : MonoidalCategory C
F : J ⥤ C
j : J
⊢ (ρ_ (limit F)).hom ≫ limit.π F j = 𝟙 (limit F ⊗ 𝟙_ C) ≫ (ρ_ (limit F)).hom ≫ limit.π F j
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Functor

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : RightRigidCategory C
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ (f ≫ g)ᘁ.op.mop = fᘁ.op.mop ≫ gᘁ.op.mop

Tactic:
by simp [comp_rightAdjointMate]

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Ind

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
H : P ≤ isFinitelyPresentable C
inst✝ : IsFinitelyAccessibleCategory C
X : C
x✝ : P.ind X
Z : C
g : Z ⟶ X
hZ : IsFinitelyPresentable Z
J : Type w
w✝¹ : SmallCategory J
w✝ : IsFiltered J
pres : ColimitPresentation J X
h : ∀ (i : J), P (pres.diag.obj i)
⊢ ∃ W u v, u ≫ v = g ∧ P W

Tactic:
have : IsFinitelyPresentable Z := hZ
    obtain ⟨j, u, hcomp⟩ := IsFinitelyPresentable.exists_hom_of_isColimit pres.isColimit g
    exact ⟨_, u, pres.ι.app j, hcomp, h j⟩

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Ind

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{u_2, u_1} D
P : ObjectProperty D
e : C ≌ D
inst✝ : P.IsClosedUnderIsomorphisms
X : D
x✝³ : Type w
x✝² : SmallCategory x✝³
x✝¹ : IsFiltered x✝³
x✝ : ∃ pres, ∀ (i : x✝³), P (pres.diag.obj i)
pres : ColimitPresentation x✝³ X
h : ∀ (i : x✝³), P (pres.diag.obj i)
⊢ ∃ pres, ∀ (i : x✝³), P.inverseImage e.functor (pres.diag.obj i)

Tactic:
exact ⟨pres.map e.inverse, fun i ↦ P.prop_of_iso ((e.counitIso.app _).symm) (h i)⟩

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.OfBiproducts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
f g h k : X ⟶ Y
⊢ leftAdd X Y (rightAdd X Y f g) (rightAdd X Y h k) = rightAdd X Y (leftAdd X Y f h) (leftAdd X Y g k)

Tactic:
let diag : X ⊞ X ⟶ Y ⊞ Y := biprod.lift (biprod.desc f g) (biprod.desc h k)

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
f g h k : X ⟶ Y
diag : X ⊞ X ⟶ Y ⊞ Y := biprod.lift (biprod.desc f g) (biprod.desc h k)
⊢ leftAdd X Y (rightAdd X Y f g) (rightAdd X Y h k) = rightAdd X Y (leftAdd X Y f h) (leftAdd X Y g k)
Module: Mathlib.CategoryTheory.Presentable.Adjunction

Goal state before:
pp: C : Type u
D : Type u'
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Category.{v', u'} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
P : ObjectProperty C
hP : P.IsCardinalFilteredGenerator κ
inst✝² : G.IsCardinalAccessible κ
inst✝¹ : G.Full
inst✝ : G.Faithful
⊢ P.map F ≤ isCardinalPresentable D κ

Tactic:
rintro Y ⟨X, hX, ⟨e⟩⟩
    have hX' := hP.le_isCardinalPresentable X hX
    rw [isCardinalPresentable_iff] at hX' ⊢
    have := adj.isCardinalPresentable_leftAdjoint_obj κ X
    exact isCardinalPresentable_of_iso e κ

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
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 N : Bimod X Y
P Q : Bimod Y Z
f : M ⟶ N
g : P ⟶ Q
⊢ M.whiskerLeft g ≫ whiskerRight f Q = whiskerRight f P ≫ N.whiskerLeft g

Tactic:
ext
  apply coequalizer.hom_ext
  dsimp
  slice_lhs 1 2 => rw [ι_colimMap, parallelPairHom_app_one]
  slice_lhs 2 3 => rw [ι_colimMap, parallelPairHom_app_one]
  slice_lhs 1 2 => rw [whisker_exchange]
  simp

Goal state after: