mathlib-initiative/mathlib-tactics huggingface dataset:
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₆
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'
η : ψ ⟶ ψ'
⊢ id F G ◁ η = (λ_ ψ).hom ≫ η ≫ (λ_ ψ').inv

Tactic:
cat_disch

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'
φ φ' φ'' : CatCospanTransform F' G' F'' G''
θ : φ ⟶ φ'
θ' : φ' ⟶ φ''
⊢ ψ ◁ (θ ≫ θ') = ψ ◁ θ ≫ ψ ◁ θ'

Tactic:
cat_disch

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''
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'''
ψ : CatCospanTransform F G F' G'
φ : CatCospanTransform F' G' F'' G''
τ τ' : CatCospanTransform F'' G'' F''' G'''
γ : τ ⟶ τ'
⊢ ψ.comp φ ◁ γ = (α_ ψ φ τ).hom ≫ ψ ◁ φ ◁ γ ≫ (α_ ψ φ τ').inv

Tactic:
cat_disch

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''
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'''
ψ : CatCospanTransform F G F' G'
φ : CatCospanTransform F' G' F'' G''
τ : CatCospanTransform F'' G'' F''' G'''
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''''
σ : CatCospanTransform F''' G''' F'''' G''''
⊢ (α_ ψ φ τ).hom ▷ σ ≫ (α_ ψ (φ.comp τ) σ).hom ≫ ψ ◁ (α_ φ τ σ).hom = (α_ (ψ.comp φ) τ σ).hom ≫ (α_ ψ φ (τ.comp σ)).hom

Tactic:
cat_disch

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'
φ : CatCospanTransform F' G' F'' G''
⊢ (α_ ψ (id F' G') φ).hom ≫ ψ ◁ (λ_ φ).hom = (ρ_ ψ).hom ▷ φ

Tactic:
cat_disch

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'
φ : CatCospanTransform F' G' F'' G''
⊢ (α_ ψ (id F' G') φ).inv ≫ (ρ_ ψ).hom ▷ φ = ψ ◁ (λ_ φ).hom

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit

Goal state before:
pp: J : Type u
inst✝² : Category.{v, u} J
C : Type u'
inst✝¹ : Category.{v', u'} C
W : J ⥤ Type w
F : J ⥤ C
inst✝ : HasWeightedLimit W F
⊢ W.weightedLimObjMap (𝟙 F) = 𝟙 (W.weightedLimObjObj F)

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit

Goal state before:
pp: J : Type u
inst✝⁴ : Category.{v, u} J
C : Type u'
inst✝³ : Category.{v', u'} C
W : J ⥤ Type w
F₁ F₂ F₃ : J ⥤ C
inst✝² : HasWeightedLimit W F₁
inst✝¹ : HasWeightedLimit W F₂
inst✝ : HasWeightedLimit W F₃
f : F₁ ⟶ F₂
g : F₂ ⟶ F₃
⊢ W.weightedLimObjMap (f ≫ g) = W.weightedLimObjMap f ≫ W.weightedLimObjMap g

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit

Goal state before:
pp: J : Type u
inst✝² : Category.{v, u} J
C : Type u'
inst✝¹ : Category.{v', u'} C
W : J ⥤ Type w
F : J ⥤ C
inst✝ : HasWeightedLimit W F
⊢ weightedLimFlipObjMap (𝟙 W) F = 𝟙 (W.weightedLimObjObj F)

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit

Goal state before:
pp: J : Type u
inst✝⁴ : Category.{v, u} J
C : Type u'
inst✝³ : Category.{v', u'} C
W W' W'' : J ⥤ Type w
g : W ⟶ W'
g' : W' ⟶ W''
F : J ⥤ C
inst✝² : HasWeightedLimit W F
inst✝¹ : HasWeightedLimit W' F
inst✝ : HasWeightedLimit W'' F
⊢ weightedLimFlipObjMap g' F ≫ weightedLimFlipObjMap g F = weightedLimFlipObjMap (g ≫ g') F

Tactic:
cat_disch

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

Goal state before:
pp: 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
x y : F ⊡ G
f : x ⟶ y
h₁ : IsIso f.fst
h₂ : IsIso f.snd
⊢ F.map (inv f.fst) ≫ x.iso.hom = y.iso.hom ≫ G.map (inv f.snd)

Tactic:
cat_disch

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

Goal state before:
pp: 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
x y : F ⊡ G
f : x ⟶ y
h₁ : IsIso f.fst
h₂ : IsIso f.snd
⊢ f ≫ { fst := inv f.fst, snd := inv f.snd, w := ⋯ } = 𝟙 x ∧ { fst := inv f.fst, snd := inv f.snd, w := ⋯ } ≫ f = 𝟙 y

Tactic:
cat_disch

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

Goal state before:
pp: case whiskerLeft
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✝ Z✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f✝ f'✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
a✝ : HomEquiv f✝ f'✝
hf : projectMapAux f✝¹ f✝ = projectMapAux f✝¹ f'✝
⊢ projectObj f✝¹ X✝ ◁ projectMapAux f✝¹ f✝ = projectObj f✝¹ X✝ ◁ projectMapAux f✝¹ f'✝

Tactic:
rw [hf]

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

Goal state before:
pp: case whiskerRight
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)
Y✝ Z✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f✝ f'✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
X✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
a✝ : HomEquiv f✝ f'✝
hf : projectMapAux f✝¹ f✝ = projectMapAux f✝¹ f'✝
⊢ projectMapAux f✝¹ f✝ ▷ projectObj f✝¹ X✝ = projectMapAux f✝¹ f'✝ ▷ projectObj f✝¹ X✝

Tactic:
rw [hf]

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
inst✝ : ChosenPullbacksAlong (curryRightUnitorHom I)
X✝ Y✝ : Over I
u : X✝ ⟶ Y✝
⊢ curryRightUnitorHom I ≫ 𝟙 ((ihom I).obj I) = 𝟙 (𝟙_ C) ≫ curryRightUnitorHom I

Tactic:
cat_disch

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
inst✝¹ : ChosenPullbacksAlong (curryRightUnitorHom I)
inst✝ : BraidedCategory C
X : Over I
A : C
v : A ⟶ (sections I).obj X
v₂ : A ⟶ (ihom I).obj X.left := v ≫ ChosenPullbacksAlong.fst ((ihom I).map X.hom) (curryRightUnitorHom I)
⊢ ((β_ A I).hom ≫ uncurry v₂) ≫ X.hom = ((toOver I).obj A).hom

Tactic:
have comm : toUnit A ≫ (curryRightUnitorHom I) = v₂ ≫ (ihom I).map X.hom := by
      rw [IsTerminal.hom_ext isTerminalTensorUnit (toUnit A) (v ≫ snd ..)]
      simp [v₂, condition]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
I : C
inst✝² : Closed I
inst✝¹ : ChosenPullbacksAlong (curryRightUnitorHom I)
inst✝ : BraidedCategory C
X : Over I
A : C
v : A ⟶ (sections I).obj X
v₂ : A ⟶ (ihom I).obj X.left := v ≫ ChosenPullbacksAlong.fst ((ihom I).map X.hom) (curryRightUnitorHom I)
comm : toUnit A ≫ curryRightUnitorHom I = v₂ ≫ (ihom I).map X.hom
⊢ ((β_ A I).hom ≫ uncurry v₂) ≫ X.hom = ((toOver I).obj A).hom
Module: Mathlib.CategoryTheory.MarkovCategory.Positive

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
inst✝¹ : PositiveCategory C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ f ≫ Δ = f ≫ Δ ≫ (inv f ⊗ₘ 𝟙 Y) ≫ (f ⊗ₘ 𝟙 Y)

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.MarkovCategory.Positive

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
inst✝¹ : PositiveCategory C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ Δ ≫ (𝟙 X ≫ f ⊗ₘ f ≫ 𝟙 Y) = Δ ≫ (f ⊗ₘ f)

Tactic:
cat_disch

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
inst✝¹ : ChosenPullbacksAlong (curryRightUnitorHom I)
inst✝ : BraidedCategory C
X : Over I
A : C
v : A ⟶ (sections I).obj X
⊢ ChosenPullbacksAlong.lift
      (curry
        ((β_ I A).hom ≫
          (β_ A I).hom ≫ uncurry (v ≫ ChosenPullbacksAlong.fst ((ihom I).map X.hom) (curryRightUnitorHom I))))
      (toUnit A) ⋯ =
    v

Tactic:
cat_disch

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} (f : T ⟶ Y) (g : T ⟶ Z),
    Over.homMk (lift (Over.Hom.left f) (Over.Hom.left g) ⋯) ⋯ ≫ (binaryFan Y Z).fst = f

Tactic:
cat_disch

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} (f : T ⟶ Y) (g : T ⟶ Z),
    Over.homMk (lift (Over.Hom.left f) (Over.Hom.left g) ⋯) ⋯ ≫ (binaryFan Y Z).snd = g

Tactic:
cat_disch

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
⊢ Over.Hom.left m = lift (Over.Hom.left a) (Over.Hom.left b) ⋯

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Kleisli

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
U : Comonad C
X : Cokleisli U
Y x✝ : C
f : (fromCokleisli U).obj X ⟶ Y
g : Y ⟶ x✝
⊢ { toFun := fun f ↦ { of := f }, invFun := fun f ↦ f.of, left_inv := ⋯, right_inv := ⋯ } (f ≫ g) =
    { toFun := fun f ↦ { of := f }, invFun := fun f ↦ f.of, left_inv := ⋯, right_inv := ⋯ } f ≫ (toCokleisli U).map g

Tactic:
cat_disch

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

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
inst✝ : MonoidalLeftAction Cᵒᵖ Dᵒᵖ
x✝³ x✝² x✝¹ : C
x✝ : D
⊢ ((α_ x✝³ x✝² x✝¹).hom.op ⊵ₗ op x✝).unop ≫
      (αₗ (op x✝³) (op (x✝² ⊗ x✝¹)) (op x✝)).symm.unop.hom ≫
        (op x✝³ ⊴ₗ (αₗ (op x✝²) (op x✝¹) (op x✝)).symm.unop.hom.op).unop =
    (αₗ (op (x✝³ ⊗ x✝²)) (op x✝¹) (op x✝)).symm.unop.hom ≫
      (αₗ (op x✝³) (op x✝²) (op (unop (op x✝¹ ⊙ₗ op x✝)))).symm.unop.hom

Tactic:
by
    apply Quiver.Hom.op_inj
    apply IsIso.inv_eq_inv.mp
    simp

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

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
inst✝ : MonoidalLeftAction Cᵒᵖ Dᵒᵖ
x✝¹ : C
x✝ : D
⊢ ((λ_ x✝¹).hom.op ⊵ₗ op x✝).unop =
    (αₗ (op (𝟙_ C)) (op x✝¹) (op x✝)).symm.unop.hom ≫ (λₗ (op (unop (op x✝¹ ⊙ₗ op x✝)))).symm.unop.hom

Tactic:
by
    apply Quiver.Hom.op_inj
    apply IsIso.inv_eq_inv.mp
    simp

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

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
inst✝ : MonoidalLeftAction Cᵒᵖ Dᵒᵖ
x✝¹ : C
x✝ : D
⊢ ((ρ_ x✝¹).hom.op ⊵ₗ op x✝).unop =
    (αₗ (op x✝¹) (op (𝟙_ C)) (op x✝)).symm.unop.hom ≫ (op x✝¹ ⊴ₗ (λₗ (op x✝)).symm.unop.hom.op).unop

Tactic:
by
    apply Quiver.Hom.op_inj
    apply IsIso.inv_eq_inv.mp
    simp

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

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
inst✝ : MonoidalRightAction Cᵒᵖ Dᵒᵖ
x✝³ x✝² x✝¹ : C
x✝ : D
⊢ (op x✝ ⊴ᵣ (α_ x✝³ x✝² x✝¹).hom.op).unop ≫
      (αᵣ (op x✝) (op x✝³) (op (x✝² ⊗ x✝¹))).symm.unop.hom ≫
        (αᵣ (op (unop (op x✝ ⊙ᵣ op x✝³))) (op x✝²) (op x✝¹)).symm.unop.hom =
    (αᵣ (op x✝) (op (x✝³ ⊗ x✝²)) (op x✝¹)).symm.unop.hom ≫
      ((αᵣ (op x✝) (op x✝³) (op x✝²)).symm.unop.hom.op ⊵ᵣ op x✝¹).unop

Tactic:
by
    apply Quiver.Hom.op_inj
    apply IsIso.inv_eq_inv.mp
    simp

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

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
inst✝ : MonoidalRightAction Cᵒᵖ Dᵒᵖ
x✝¹ : C
x✝ : D
⊢ (op x✝ ⊴ᵣ (λ_ x✝¹).hom.op).unop =
    (αᵣ (op x✝) (op (𝟙_ C)) (op x✝¹)).symm.unop.hom ≫ ((ρᵣ (op x✝)).symm.unop.hom.op ⊵ᵣ op x✝¹).unop

Tactic:
by
    apply Quiver.Hom.op_inj
    apply IsIso.inv_eq_inv.mp
    simp

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

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
inst✝ : MonoidalRightAction Cᵒᵖ Dᵒᵖ
x✝¹ : C
x✝ : D
⊢ (op x✝ ⊴ᵣ (ρ_ x✝¹).hom.op).unop =
    (αᵣ (op x✝) (op x✝¹) (op (𝟙_ C))).symm.unop.hom ≫ (ρᵣ (op (unop (op x✝ ⊙ᵣ op x✝¹)))).symm.unop.hom

Tactic:
by
    apply Quiver.Hom.op_inj
    apply IsIso.inv_eq_inv.mp
    simp

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M : Bimon C
⊢ Δ.hom ≫ M.X.X ◁ ε.hom = (ρ_ M.X.X).inv

Tactic:
by
    rw [← BimonObjAux_counit, ← BimonObjAux_comul, ComonObj.comul_counit]

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

Goal state before:
pp: J : Type w
inst✝² : Category.{v_1, w} J
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
F : J ⥤ Mon C
c : Cone (F ⋙ forget C)
hc : IsLimit c
⊢ ∀ (j : J),
    (c.pt ◁ hc.lift { pt := 𝟙_ C, π := { app := fun X ↦ η, naturality := ⋯ } } ≫
          hc.lift { pt := c.1 ⊗ c.1, π := { app := fun X ↦ (c.π.app X ⊗ₘ c.π.app X) ≫ μ, naturality := ⋯ } }) ≫
        c.π.app j =
      (ρ_ c.pt).hom ≫ c.π.app j

Tactic:
by simp [whiskerLeft_comp_tensorHom_assoc]

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

Goal state before:
pp: case h₁
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasPushouts C
inst✝³ : HasInitial C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
X₁ X₂ X₃ Y₁ Y₂ Y₃ : Arrow C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
⊢ (α_ X₁.left X₂.right X₃.right).hom ≫
      X₁.left ◁ X₂.right ◁ Arrow.Hom.right f₃ ≫
        (α_ X₁.left X₂.right Y₃.right).inv ≫
          Arrow.Hom.left f₁ ▷ X₂.right ▷ Y₃.right ≫
            (α_ Y₁.left X₂.right Y₃.right).hom ≫ Y₁.left ◁ Arrow.Hom.right f₂ ▷ Y₃.right =
    Arrow.Hom.left f₁ ▷ X₂.right ▷ X₃.right ≫
      (α_ Y₁.left X₂.right X₃.right).hom ≫
        Y₁.left ◁ Arrow.Hom.right f₂ ▷ X₃.right ≫ Y₁.left ◁ Y₂.right ◁ Arrow.Hom.right f₃

Tactic:
cat_disch

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)))
h : ∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))
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)
w₂ :
  (coyoneda.map (adj.unit.app d ▷ d').op).app (R.obj c) =
    ((yoneda.obj (R.obj c)).mapIso (β_ (Opposite.op ((L ⋙ R).1 d)) (Opposite.op d'))).hom ≫
      (coyoneda.map (d' ◁ adj.unit.app d).op).app (R.obj c) ≫
        ((yoneda.obj (R.obj c)).mapIso (β_ (Opposite.op d') (Opposite.op ((𝟭 D).1 d)))).hom
w₃ :
  ⇑(ConcreteCategory.hom ((coyoneda.map (d' ◁ adj.unit.app d).op).app (R.obj c))) =
    ⇑((ihom.adjunction d').homEquiv (Opposite.unop (Opposite.op ((𝟭 D).obj d))) (R.obj c)).symm ∘
      ⇑(ConcreteCategory.hom ((coyoneda.map (adj.unit.app d).op).app ((ihom d').obj (R.obj c)))) ∘
        ⇑((ihom.adjunction d').homEquiv (Opposite.unop (Opposite.op ((L ⋙ R).obj d))) (R.obj c))
⊢ (coyoneda.map (adj.unit.app d).op).app ((ihom d').obj (R.obj c)) ≫
      (coyoneda.obj (Opposite.op d)).map (adj.unit.app ((ihom d').obj (R.obj c))) =
    (coyoneda.obj (Opposite.op ((L ⋙ R).obj d))).map (adj.unit.app ((ihom d').obj (R.obj c))) ≫
      (coyoneda.map (adj.unit.app d).op).app ((L ⋙ R).obj ((ihom d').obj (R.obj c)))

Tactic:
cat_disch

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

Goal state before:
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₁} (tensorLeft X)
| R.X ◁ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ≫ actLeft P Q

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₁} (tensorLeft X)
| η ▷ (P.X ⊗ Q.X)

Tactic:
rw [whiskerLeft_π_actLeft]

Goal state after:
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₁} (tensorLeft X)
| (α_ R.X P.X Q.X).inv ≫ P.actLeft ▷ Q.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₁} (tensorLeft X)
| η ▷ (P.X ⊗ Q.X)
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
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₁} (tensorLeft X)
| R.X ◁ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ≫ actLeft P Q

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₁} (tensorLeft X)
| μ ▷ (P.X ⊗ Q.X)

Tactic:
rw [whiskerLeft_π_actLeft]

Goal state after:
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₁} (tensorLeft X)
| (α_ R.X P.X Q.X).inv ≫ P.actLeft ▷ Q.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₁} (tensorLeft X)
| μ ▷ (P.X ⊗ Q.X)