mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
X₁ X₂ Y₁ Y₂ : C
inst✝¹ : ExactPairing X₁ Y₁
inst✝ : ExactPairing X₂ Y₂
⊢ (η_ X₁ Y₁ ⊗≫ (X₁ ◁ η_ X₂ Y₂) ▷ Y₁ ⊗≫ 𝟙 ((X₁ ⊗ X₂) ⊗ Y₂ ⊗ Y₁)) ▷ (X₁ ⊗ X₂) ≫
      (α_ (X₁ ⊗ X₂) (Y₂ ⊗ Y₁) (X₁ ⊗ X₂)).hom ≫ (X₁ ⊗ X₂) ◁ (𝟙 ((Y₂ ⊗ Y₁) ⊗ X₁ ⊗ X₂) ⊗≫ Y₂ ◁ ε_ X₁ Y₁ ▷ X₂ ⊗≫ ε_ X₂ Y₂) =
    η_ X₁ Y₁ ▷ (X₁ ⊗ X₂) ⊗≫ (X₁ ◁ η_ X₂ Y₂) ▷ (Y₁ ⊗ X₁ ⊗ X₂) ⊗≫ (X₁ ⊗ X₂) ◁ Y₂ ◁ ε_ X₁ Y₁ ▷ X₂ ⊗≫ (X₁ ⊗ X₂) ◁ ε_ X₂ Y₂

Tactic:
monoidal

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
f : ι →₀ R
i : ι
⊢ (b.toDual (b i)) (f.sum fun i a ↦ a • b i) = f i

Tactic:
Finsupp.sum,

Goal state after:
R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
f : ι →₀ R
i : ι
⊢ (b.toDual (b i)) (∑ a ∈ f.support, f a • b a) = f i
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
m : M
i : ι
⊢ (b.toDual m) (b i) = (b.repr m) i

Tactic:
by
  rw [← b.toDual_linearCombination_left, b.linearCombination_repr]

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
X₁ X₂ Y₁ Y₂ : C
inst✝¹ : ExactPairing X₁ Y₁
inst✝ : ExactPairing X₂ Y₂
⊢ η_ X₁ Y₁ ▷ (X₁ ⊗ X₂) ⊗≫ (X₁ ◁ η_ X₂ Y₂) ▷ (Y₁ ⊗ X₁ ⊗ X₂) ⊗≫ (X₁ ⊗ X₂) ◁ Y₂ ◁ ε_ X₁ Y₁ ▷ X₂ ⊗≫ (X₁ ⊗ X₂) ◁ ε_ X₂ Y₂ =
    η_ X₁ Y₁ ▷ (X₁ ⊗ X₂) ⊗≫ X₁ ◁ (η_ X₂ Y₂ ▷ (Y₁ ⊗ X₁) ≫ (X₂ ⊗ Y₂) ◁ ε_ X₁ Y₁) ▷ X₂ ⊗≫ (X₁ ⊗ X₂) ◁ ε_ X₂ Y₂

Tactic:
monoidal

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
l : ι →₀ R
i : ι
⊢ (ε i) (lc e l) = l i

Tactic:
rw [lc, map_finsuppSum, Finsupp.sum_eq_single i (g := fun a b ↦ (ε i) (b • e a))]

Goal state after:
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
l : ι →₀ R
i : ι
⊢ (ε i) (l i • e i) = l i

case h₀
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
l : ι →₀ R
i : ι
⊢ ∀ (b : ι), l b ≠ 0 → b ≠ i → (ε i) (l b • e b) = 0

case h₁
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
l : ι →₀ R
i : ι
⊢ l i = 0 → (ε i) (0 • e i) = 0
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
X₁ X₂ Y₁ Y₂ : C
inst✝¹ : ExactPairing X₁ Y₁
inst✝ : ExactPairing X₂ Y₂
⊢ η_ X₁ Y₁ ▷ (X₁ ⊗ X₂) ⊗≫ X₁ ◁ (𝟙_ C ◁ ε_ X₁ Y₁ ≫ η_ X₂ Y₂ ▷ 𝟙_ C) ▷ X₂ ⊗≫ (X₁ ⊗ X₂) ◁ ε_ X₂ Y₂ =
    𝟙 (𝟙_ C ⊗ X₁ ⊗ X₂) ⊗≫
      (η_ X₁ Y₁ ▷ X₁ ⊗≫ X₁ ◁ ε_ X₁ Y₁) ▷ X₂ ⊗≫ X₁ ◁ (η_ X₂ Y₂ ▷ X₂ ⊗≫ X₂ ◁ ε_ X₂ Y₂) ⊗≫ 𝟙 ((X₁ ⊗ X₂) ⊗ 𝟙_ C)

Tactic:
monoidal

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
X₁ X₂ Y₁ Y₂ : C
inst✝¹ : ExactPairing X₁ Y₁
inst✝ : ExactPairing X₂ Y₂
⊢ 𝟙 (𝟙_ C ⊗ X₁ ⊗ X₂) ⊗≫ ⊗𝟙.hom ▷ X₂ ⊗≫ X₁ ◁ ⊗𝟙.hom ⊗≫ 𝟙 ((X₁ ⊗ X₂) ⊗ 𝟙_ C) = (λ_ (X₁ ⊗ X₂)).hom ≫ (ρ_ (X₁ ⊗ X₂)).inv

Tactic:
monoidal

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : HasRightDual X
inst✝ : HasRightDual Y
f : X ⟶ Y
g : Xᘁ ⟶ Z
⊢ ((ρ_ Yᘁ).inv ≫ Yᘁ ◁ η_ X Xᘁ ≫ Yᘁ ◁ f ▷ Xᘁ ≫ (α_ Yᘁ Y Xᘁ).inv ≫ ε_ Y Yᘁ ▷ Xᘁ ≫ (λ_ Xᘁ).hom) ≫ g =
    𝟙 Yᘁ ⊗≫ Yᘁ ◁ η_ X Xᘁ ≫ Yᘁ ◁ f ▷ Xᘁ ⊗≫ (ε_ Y Yᘁ ▷ Xᘁ ≫ 𝟙_ C ◁ g) ⊗≫ 𝟙 Z

Tactic:
monoidal

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : HasRightDual X
inst✝ : HasRightDual Y
f : X ⟶ Y
g : Xᘁ ⟶ Z
⊢ 𝟙 Yᘁ ⊗≫ Yᘁ ◁ η_ X Xᘁ ≫ Yᘁ ◁ f ▷ Xᘁ ⊗≫ ((Yᘁ ⊗ Y) ◁ g ≫ ε_ Y Yᘁ ▷ Z) ⊗≫ 𝟙 Z =
    (ρ_ Yᘁ).inv ≫ Yᘁ ◁ η_ X Xᘁ ≫ Yᘁ ◁ (f ▷ Xᘁ ≫ Y ◁ g) ≫ (α_ Yᘁ Y Z).inv ≫ ε_ Y Yᘁ ▷ Z ≫ (λ_ Z).hom

Tactic:
monoidal

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : HasLeftDual X
inst✝ : HasLeftDual Y
f : X ⟶ Y
g : ᘁX ⟶ Z
⊢ ((λ_ ᘁY).inv ≫ η_ (ᘁX) X ▷ ᘁY ≫ (ᘁX ◁ f) ▷ ᘁY ≫ (α_ (ᘁX) Y ᘁY).hom ≫ ᘁX ◁ ε_ (ᘁY) Y ≫ (ρ_ ᘁX).hom) ≫ g =
    𝟙 ᘁY ⊗≫ η_ (ᘁX) X ▷ ᘁY ⊗≫ ᘁX ◁ f ▷ ᘁY ⊗≫ (ᘁX ◁ ε_ (ᘁY) Y ≫ g ▷ 𝟙_ C) ⊗≫ 𝟙 Z

Tactic:
monoidal

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : HasLeftDual X
inst✝ : HasLeftDual Y
f : X ⟶ Y
g : ᘁX ⟶ Z
⊢ 𝟙 ᘁY ⊗≫ η_ (ᘁX) X ▷ ᘁY ⊗≫ ᘁX ◁ f ▷ ᘁY ⊗≫ (g ▷ (Y ⊗ ᘁY) ≫ Z ◁ ε_ (ᘁY) Y) ⊗≫ 𝟙 Z =
    (λ_ ᘁY).inv ≫ η_ (ᘁX) X ▷ ᘁY ≫ (ᘁX ◁ f ≫ g ▷ Y) ▷ ᘁY ≫ (α_ Z Y ᘁY).hom ≫ Z ◁ ε_ (ᘁY) Y ≫ (ρ_ Z).hom

Tactic:
monoidal

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky

Goal state before:
pp: K : Type u
inst✝ : DivisionRing K
ι : Type v
hι : Infinite ι
ιK : Type (max u v)
bK : Module.Basis ιK K (ι → K)
e : ℕ ↪ ι
this✝ : lift.{v, u} (Module.rank K (ℕ → K)) ≤ Module.rank K (ι → K)
key : ℵ₀ ≤ Module.rank K (ι → K) ∧ lift.{v, u} #K ≤ Module.rank K (ι → K)
this : Infinite ιK
⊢ Module.rank K (ι → K) = #(ιK →₀ K)

Tactic:
mk_finsupp_lift_of_infinite,

Goal state after:
K : Type u
inst✝ : DivisionRing K
ι : Type v
hι : Infinite ι
ιK : Type (max u v)
bK : Module.Basis ιK K (ι → K)
e : ℕ ↪ ι
this✝ : lift.{v, u} (Module.rank K (ℕ → K)) ≤ Module.rank K (ι → K)
key : ℵ₀ ≤ Module.rank K (ι → K) ∧ lift.{v, u} #K ≤ Module.rank K (ι → K)
this : Infinite ιK
⊢ Module.rank K (ι → K) = max (lift.{u, max u v} #ιK) (lift.{max u v, u} #K)
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
X Y Z : C
inst✝² : HasRightDual X
inst✝¹ : HasRightDual Y
inst✝ : HasRightDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ η_ Y Yᘁ ≫ Y ◁ ((ρ_ Yᘁ).inv ≫ Yᘁ ◁ η_ X Xᘁ ≫ Yᘁ ◁ f ▷ Xᘁ ≫ (α_ Yᘁ Y Xᘁ).inv ≫ ε_ Y Yᘁ ▷ Xᘁ ≫ (λ_ Xᘁ).hom) ≫ g ▷ Xᘁ =
    𝟙 (𝟙_ C) ⊗≫ (η_ Y Yᘁ ▷ 𝟙_ C ≫ (Y ⊗ Yᘁ) ◁ η_ X Xᘁ) ⊗≫ Y ◁ Yᘁ ◁ f ▷ Xᘁ ⊗≫ Y ◁ ε_ Y Yᘁ ▷ Xᘁ ⊗≫ g ▷ Xᘁ ⊗≫ 𝟙 (Z ⊗ Xᘁ)

Tactic:
monoidal

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
X Y Z : C
inst✝² : HasRightDual X
inst✝¹ : HasRightDual Y
inst✝ : HasRightDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ 𝟙 (𝟙_ C) ⊗≫ (𝟙_ C ◁ η_ X Xᘁ ≫ η_ Y Yᘁ ▷ (X ⊗ Xᘁ)) ⊗≫ Y ◁ Yᘁ ◁ f ▷ Xᘁ ⊗≫ Y ◁ ε_ Y Yᘁ ▷ Xᘁ ⊗≫ g ▷ Xᘁ ⊗≫ 𝟙 (Z ⊗ Xᘁ) =
    η_ X Xᘁ ⊗≫ (η_ Y Yᘁ ▷ (X ⊗ Xᘁ) ≫ (Y ⊗ Yᘁ) ◁ f ▷ Xᘁ) ⊗≫ Y ◁ ε_ Y Yᘁ ▷ Xᘁ ⊗≫ g ▷ Xᘁ ⊗≫ 𝟙 (Z ⊗ Xᘁ)

Tactic:
monoidal

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
X Y Z : C
inst✝² : HasRightDual X
inst✝¹ : HasRightDual Y
inst✝ : HasRightDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ η_ X Xᘁ ⊗≫ (𝟙_ C ◁ f ▷ Xᘁ ≫ η_ Y Yᘁ ▷ (Y ⊗ Xᘁ)) ⊗≫ Y ◁ ε_ Y Yᘁ ▷ Xᘁ ⊗≫ g ▷ Xᘁ ⊗≫ 𝟙 (Z ⊗ Xᘁ) =
    η_ X Xᘁ ⊗≫ f ▷ Xᘁ ⊗≫ (η_ Y Yᘁ ▷ Y ⊗≫ Y ◁ ε_ Y Yᘁ) ▷ Xᘁ ⊗≫ g ▷ Xᘁ ⊗≫ 𝟙 (Z ⊗ Xᘁ)

Tactic:
monoidal

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
X Y Z : C
inst✝² : HasRightDual X
inst✝¹ : HasRightDual Y
inst✝ : HasRightDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ η_ X Xᘁ ⊗≫ f ▷ Xᘁ ⊗≫ ⊗𝟙.hom ▷ Xᘁ ⊗≫ g ▷ Xᘁ ⊗≫ 𝟙 (Z ⊗ Xᘁ) = η_ X Xᘁ ≫ f ▷ Xᘁ ≫ g ▷ Xᘁ

Tactic:
monoidal

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
X Y Z : C
inst✝² : HasLeftDual X
inst✝¹ : HasLeftDual Y
inst✝ : HasLeftDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ η_ (ᘁY) Y ≫
      ((λ_ ᘁY).inv ≫ η_ (ᘁX) X ▷ ᘁY ≫ (ᘁX ◁ f) ▷ ᘁY ≫ (α_ (ᘁX) Y ᘁY).hom ≫ ᘁX ◁ ε_ (ᘁY) Y ≫ (ρ_ ᘁX).hom) ▷ Y ≫ ᘁX ◁ g =
    𝟙 (𝟙_ C) ⊗≫ (𝟙_ C ◁ η_ (ᘁY) Y ≫ η_ (ᘁX) X ▷ (ᘁY ⊗ Y)) ⊗≫ ᘁX ◁ f ▷ ᘁY ▷ Y ⊗≫ ᘁX ◁ ε_ (ᘁY) Y ▷ Y ⊗≫ ᘁX ◁ g

Tactic:
monoidal

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
X Y Z : C
inst✝² : HasLeftDual X
inst✝¹ : HasLeftDual Y
inst✝ : HasLeftDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ 𝟙 (𝟙_ C) ⊗≫ (η_ (ᘁX) X ▷ 𝟙_ C ≫ (ᘁX ⊗ X) ◁ η_ (ᘁY) Y) ⊗≫ ᘁX ◁ f ▷ ᘁY ▷ Y ⊗≫ ᘁX ◁ ε_ (ᘁY) Y ▷ Y ⊗≫ ᘁX ◁ g =
    η_ (ᘁX) X ⊗≫ ((ᘁX ⊗ X) ◁ η_ (ᘁY) Y ≫ (ᘁX ◁ f) ▷ (ᘁY ⊗ Y)) ⊗≫ ᘁX ◁ ε_ (ᘁY) Y ▷ Y ⊗≫ ᘁX ◁ g

Tactic:
monoidal

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
X Y Z : C
inst✝² : HasLeftDual X
inst✝¹ : HasLeftDual Y
inst✝ : HasLeftDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ η_ (ᘁX) X ⊗≫ ((ᘁX ◁ f) ▷ 𝟙_ C ≫ (ᘁX ⊗ Y) ◁ η_ (ᘁY) Y) ⊗≫ ᘁX ◁ ε_ (ᘁY) Y ▷ Y ⊗≫ ᘁX ◁ g =
    η_ (ᘁX) X ⊗≫ ᘁX ◁ f ⊗≫ ᘁX ◁ (Y ◁ η_ (ᘁY) Y ⊗≫ ε_ (ᘁY) Y ▷ Y) ⊗≫ ᘁX ◁ g

Tactic:
monoidal

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
X Y Z : C
inst✝² : HasLeftDual X
inst✝¹ : HasLeftDual Y
inst✝ : HasLeftDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ η_ (ᘁX) X ⊗≫ ᘁX ◁ f ⊗≫ ᘁX ◁ ⊗𝟙.hom ⊗≫ ᘁX ◁ g = η_ (ᘁX) X ≫ ᘁX ◁ f ≫ ᘁX ◁ g

Tactic:
monoidal

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X Y Y' Z : C
inst✝ : ExactPairing Y Y'
f : Y' ⊗ X ⟶ Z
⊢ (fun f ↦ Y' ◁ f ≫ (α_ Y' Y Z).inv ≫ ε_ Y Y' ▷ Z ≫ (λ_ Z).hom)
      ((fun f ↦ (λ_ X).inv ≫ η_ Y Y' ▷ X ≫ (α_ Y Y' X).hom ≫ Y ◁ f) f) =
    𝟙 (Y' ⊗ X) ⊗≫ Y' ◁ η_ Y Y' ▷ X ⊗≫ ((Y' ⊗ Y) ◁ f ≫ ε_ Y Y' ▷ Z) ⊗≫ 𝟙 Z

Tactic:
monoidal

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X Y Y' Z : C
inst✝ : ExactPairing Y Y'
f : Y' ⊗ X ⟶ Z
⊢ 𝟙 (Y' ⊗ X) ⊗≫ Y' ◁ η_ Y Y' ▷ X ⊗≫ (ε_ Y Y' ▷ (Y' ⊗ X) ≫ 𝟙_ C ◁ f) ⊗≫ 𝟙 Z =
    𝟙 (Y' ⊗ X) ⊗≫ (Y' ◁ η_ Y Y' ⊗≫ ε_ Y Y' ▷ Y') ▷ X ⊗≫ f

Tactic:
monoidal

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X Y Y' Z : C
inst✝ : ExactPairing Y Y'
f : Y' ⊗ X ⟶ Z
⊢ 𝟙 (Y' ⊗ X) ⊗≫ ⊗𝟙.hom ▷ X ⊗≫ f = f

Tactic:
monoidal

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X Y Y' Z : C
inst✝ : ExactPairing Y Y'
f : X ⟶ Y ⊗ Z
⊢ (fun f ↦ (λ_ X).inv ≫ η_ Y Y' ▷ X ≫ (α_ Y Y' X).hom ≫ Y ◁ f)
      ((fun f ↦ Y' ◁ f ≫ (α_ Y' Y Z).inv ≫ ε_ Y Y' ▷ Z ≫ (λ_ Z).hom) f) =
    𝟙 X ⊗≫ (η_ Y Y' ▷ X ≫ (Y ⊗ Y') ◁ f) ⊗≫ Y ◁ ε_ Y Y' ▷ Z ⊗≫ 𝟙 (Y ⊗ Z)

Tactic:
monoidal

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X Y Y' Z : C
inst✝ : ExactPairing Y Y'
f : X ⟶ Y ⊗ Z
⊢ 𝟙 X ⊗≫ (𝟙_ C ◁ f ≫ η_ Y Y' ▷ (Y ⊗ Z)) ⊗≫ Y ◁ ε_ Y Y' ▷ Z ⊗≫ 𝟙 (Y ⊗ Z) =
    f ⊗≫ (η_ Y Y' ▷ Y ⊗≫ Y ◁ ε_ Y Y') ▷ Z ⊗≫ 𝟙 (Y ⊗ Z)

Tactic:
monoidal

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X Y Y' Z : C
inst✝ : ExactPairing Y Y'
f : X ⟶ Y ⊗ Z
⊢ f ⊗≫ ⊗𝟙.hom ▷ Z ⊗≫ 𝟙 (Y ⊗ Z) = f

Tactic:
monoidal

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X Y Y' Z : C
inst✝ : ExactPairing Y Y'
f : X ⊗ Y ⟶ Z
⊢ (fun f ↦ f ▷ Y ≫ (α_ Z Y' Y).hom ≫ Z ◁ ε_ Y Y' ≫ (ρ_ Z).hom)
      ((fun f ↦ (ρ_ X).inv ≫ X ◁ η_ Y Y' ≫ (α_ X Y Y').inv ≫ f ▷ Y') f) =
    𝟙 (X ⊗ Y) ⊗≫ X ◁ η_ Y Y' ▷ Y ⊗≫ (f ▷ (Y' ⊗ Y) ≫ Z ◁ ε_ Y Y') ⊗≫ 𝟙 Z

Tactic:
monoidal

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X Y Y' Z : C
inst✝ : ExactPairing Y Y'
f : X ⊗ Y ⟶ Z
⊢ 𝟙 (X ⊗ Y) ⊗≫ X ◁ η_ Y Y' ▷ Y ⊗≫ ((X ⊗ Y) ◁ ε_ Y Y' ≫ f ▷ 𝟙_ C) ⊗≫ 𝟙 Z =
    𝟙 (X ⊗ Y) ⊗≫ X ◁ (η_ Y Y' ▷ Y ⊗≫ Y ◁ ε_ Y Y') ⊗≫ f

Tactic:
monoidal

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X Y Y' Z : C
inst✝ : ExactPairing Y Y'
f : X ⊗ Y ⟶ Z
⊢ 𝟙 (X ⊗ Y) ⊗≫ X ◁ ⊗𝟙.hom ⊗≫ f = f

Tactic:
monoidal

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X Y Y' Z : C
inst✝ : ExactPairing Y Y'
f : X ⟶ Z ⊗ Y'
⊢ (fun f ↦ (ρ_ X).inv ≫ X ◁ η_ Y Y' ≫ (α_ X Y Y').inv ≫ f ▷ Y')
      ((fun f ↦ f ▷ Y ≫ (α_ Z Y' Y).hom ≫ Z ◁ ε_ Y Y' ≫ (ρ_ Z).hom) f) =
    𝟙 X ⊗≫ (X ◁ η_ Y Y' ≫ f ▷ (Y ⊗ Y')) ⊗≫ Z ◁ ε_ Y Y' ▷ Y' ⊗≫ 𝟙 (Z ⊗ Y')

Tactic:
monoidal

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X Y Y' Z : C
inst✝ : ExactPairing Y Y'
f : X ⟶ Z ⊗ Y'
⊢ 𝟙 X ⊗≫ (f ▷ 𝟙_ C ≫ (Z ⊗ Y') ◁ η_ Y Y') ⊗≫ Z ◁ ε_ Y Y' ▷ Y' ⊗≫ 𝟙 (Z ⊗ Y') =
    f ⊗≫ Z ◁ (Y' ◁ η_ Y Y' ⊗≫ ε_ Y Y' ▷ Y') ⊗≫ 𝟙 (Z ⊗ Y')

Tactic:
monoidal

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X Y Y' Z : C
inst✝ : ExactPairing Y Y'
f : X ⟶ Z ⊗ Y'
⊢ f ⊗≫ Z ◁ ⊗𝟙.hom ⊗≫ 𝟙 (Z ⊗ Y') = f

Tactic:
monoidal

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

Goal state before:

Tactic:
_ = 𝟙 _ ⊗≫ (X ◁ η_ Y Y' ≫ f ▷ (Y ⊗ Y')) ⊗≫ Z ◁ ε_ Y Y' ▷ Y' ⊗≫ 𝟙 _ := by
        monoidal
      _ = f ⊗≫ Z ◁ (Y' ◁ η_ Y Y' ⊗≫ ε_ Y Y' ▷ Y') ⊗≫ 𝟙 _ := by
        rw [whisker_exchange]; monoidal
      _ = f := by
        rw [coevaluation_evaluation'']; monoidal

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
Y Y' Z : C
inst✝ : ExactPairing Y Y'
f : Y' ⟶ Z
⊢ Y' ◁ (η_ Y Y' ≫ Y ◁ f) ≫ (α_ Y' Y Z).inv ≫ ε_ Y Y' ▷ Z ≫ (λ_ Z).hom =
    Y' ◁ η_ Y Y' ⊗≫ ((Y' ⊗ Y) ◁ f ≫ ε_ Y Y' ▷ Z) ⊗≫ 𝟙 Z

Tactic:
monoidal

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
Y Y' Z : C
inst✝ : ExactPairing Y Y'
f : Y' ⟶ Z
⊢ Y' ◁ η_ Y Y' ⊗≫ (ε_ Y Y' ▷ Y' ≫ 𝟙_ C ◁ f) ⊗≫ 𝟙 Z = (Y' ◁ η_ Y Y' ⊗≫ ε_ Y Y' ▷ Y') ⊗≫ f

Tactic:
monoidal

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
Y Y' Z : C
inst✝ : ExactPairing Y Y'
f : Y' ⟶ Z
⊢  ⊗𝟙.hom ⊗≫ f = (ρ_ Y').hom ≫ f

Tactic:
monoidal

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
Y Y' Z : C
inst✝ : ExactPairing Y Y'
f : Y ⟶ Z
⊢ (η_ Y Y' ≫ f ▷ Y') ▷ Y ≫ (α_ Z Y' Y).hom ≫ Z ◁ ε_ Y Y' ≫ (ρ_ Z).hom =
    η_ Y Y' ▷ Y ⊗≫ (f ▷ (Y' ⊗ Y) ≫ Z ◁ ε_ Y Y') ⊗≫ 𝟙 Z

Tactic:
monoidal

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
Y Y' Z : C
inst✝ : ExactPairing Y Y'
f : Y ⟶ Z
⊢ η_ Y Y' ▷ Y ⊗≫ (Y ◁ ε_ Y Y' ≫ f ▷ 𝟙_ C) ⊗≫ 𝟙 Z = (η_ Y Y' ▷ Y ⊗≫ Y ◁ ε_ Y Y') ⊗≫ f

Tactic:
monoidal

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
Y Y' Z : C
inst✝ : ExactPairing Y Y'
f : Y ⟶ Z
⊢  ⊗𝟙.hom ⊗≫ f = (λ_ Y).hom ≫ f

Tactic:
monoidal

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
Y Z : C
inst✝ : HasLeftDual Z
f : Y ⟶ ᘁZ
⊢ (λ_ Y).inv ≫ η_ (ᘁZ) Z ▷ Y ≫ (α_ (ᘁZ) Z Y).hom ≫ ᘁZ ◁ (Z ◁ f ≫ ε_ (ᘁZ) Z) =
    𝟙 Y ⊗≫ (η_ (ᘁZ) Z ▷ Y ≫ (ᘁZ ⊗ Z) ◁ f) ⊗≫ ᘁZ ◁ ε_ (ᘁZ) Z

Tactic:
monoidal

Goal state after:
Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas

Goal state before:
pp: K : Type u
V : Type v
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
s : Set V
inst✝¹ : Nonempty ↑s
inst✝ : Fintype ↑s
lin_ind : LinearIndependent K Subtype.val
card_eq : s.toFinset.card = finrank K V
⊢ ⇑(setBasisOfLinearIndependentOfCardEqFinrank lin_ind card_eq) = Subtype.val

Tactic:
by
  simp [setBasisOfLinearIndependentOfCardEqFinrank]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
Y Z : C
inst✝ : HasLeftDual Z
f : Y ⟶ ᘁZ
⊢ 𝟙 Y ⊗≫ (𝟙_ C ◁ f ≫ η_ (ᘁZ) Z ▷ ᘁZ) ⊗≫ ᘁZ ◁ ε_ (ᘁZ) Z = f ⊗≫ η_ (ᘁZ) Z ▷ ᘁZ ⊗≫ ᘁZ ◁ ε_ (ᘁZ) Z

Tactic:
monoidal

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
Y Z : C
inst✝ : HasLeftDual Z
f : Y ⟶ ᘁZ
⊢ f ⊗≫ ⊗𝟙.hom = f ≫ (ρ_ ᘁZ).inv

Tactic:
monoidal

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X Y : C
inst✝ : HasRightDual X
f : Y ⟶ Xᘁ
⊢ (ρ_ Y).inv ≫ Y ◁ η_ X Xᘁ ≫ (α_ Y X Xᘁ).inv ≫ (f ▷ X ≫ ε_ X Xᘁ) ▷ Xᘁ =
    𝟙 Y ⊗≫ (Y ◁ η_ X Xᘁ ≫ f ▷ (X ⊗ Xᘁ)) ⊗≫ ε_ X Xᘁ ▷ Xᘁ

Tactic:
monoidal

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X Y : C
inst✝ : HasRightDual X
f : Y ⟶ Xᘁ
⊢ 𝟙 Y ⊗≫ (f ▷ 𝟙_ C ≫ Xᘁ ◁ η_ X Xᘁ) ⊗≫ ε_ X Xᘁ ▷ Xᘁ = f ⊗≫ Xᘁ ◁ η_ X Xᘁ ⊗≫ ε_ X Xᘁ ▷ Xᘁ

Tactic:
monoidal

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X Y : C
inst✝ : HasRightDual X
f : Y ⟶ Xᘁ
⊢ f ⊗≫ ⊗𝟙.hom = f ≫ (λ_ Xᘁ).inv

Tactic:
monoidal

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X X' Y : C
inst✝ : ExactPairing X' Y
i : X ≅ X'
⊢ Y ◁ (η_ X' Y ≫ i.inv ▷ Y) ≫ (α_ Y X Y).inv ≫ (Y ◁ i.hom ≫ ε_ X' Y) ▷ Y =
    Y ◁ η_ X' Y ≫ Y ◁ (i.inv ≫ i.hom) ▷ Y ⊗≫ ε_ X' Y ▷ Y

Tactic:
monoidal

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X X' Y : C
inst✝ : ExactPairing X' Y
i : X ≅ X'
⊢ Y ◁ η_ X' Y ≫ Y ◁ 𝟙 X' ▷ Y ⊗≫ ε_ X' Y ▷ Y = Y ◁ η_ X' Y ⊗≫ ε_ X' Y ▷ Y

Tactic:
monoidal

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X X' Y : C
inst✝ : ExactPairing X' Y
i : X ≅ X'
⊢ (η_ X' Y ≫ i.inv ▷ Y) ▷ X ≫ (α_ X Y X).hom ≫ X ◁ (Y ◁ i.hom ≫ ε_ X' Y) =
    η_ X' Y ▷ X ⊗≫ (i.inv ▷ (Y ⊗ X) ≫ X ◁ Y ◁ i.hom) ⊗≫ X ◁ ε_ X' Y

Tactic:
monoidal

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X X' Y : C
inst✝ : ExactPairing X' Y
i : X ≅ X'
⊢ η_ X' Y ▷ X ⊗≫ (X' ◁ Y ◁ i.hom ≫ i.inv ▷ (Y ⊗ X')) ⊗≫ X ◁ ε_ X' Y =
    𝟙 (𝟙_ C ⊗ X) ⊗≫ (η_ X' Y ▷ X ≫ (X' ⊗ Y) ◁ i.hom) ⊗≫ (i.inv ▷ (Y ⊗ X') ≫ X ◁ ε_ X' Y) ⊗≫ 𝟙 (X ⊗ 𝟙_ C)

Tactic:
monoidal

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X X' Y : C
inst✝ : ExactPairing X' Y
i : X ≅ X'
⊢ 𝟙 (𝟙_ C ⊗ X) ⊗≫ (𝟙_ C ◁ i.hom ≫ η_ X' Y ▷ X') ⊗≫ (X' ◁ ε_ X' Y ≫ i.inv ▷ 𝟙_ C) ⊗≫ 𝟙 (X ⊗ 𝟙_ C) =
    𝟙 (𝟙_ C ⊗ X) ⊗≫ i.hom ⊗≫ (η_ X' Y ▷ X' ⊗≫ X' ◁ ε_ X' Y) ⊗≫ i.inv ⊗≫ 𝟙 (X ⊗ 𝟙_ C)

Tactic:
monoidal

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X X' Y : C
inst✝ : ExactPairing X' Y
i : X ≅ X'
⊢ 𝟙 (𝟙_ C ⊗ X) ⊗≫ i.hom ⊗≫ ⊗𝟙.hom ⊗≫ i.inv ⊗≫ 𝟙 (X ⊗ 𝟙_ C) = 𝟙 (𝟙_ C ⊗ X) ⊗≫ (i.hom ≫ i.inv) ⊗≫ 𝟙 (X ⊗ 𝟙_ C)

Tactic:
monoidal

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X X' Y : C
inst✝ : ExactPairing X' Y
i : X ≅ X'
⊢ 𝟙 (𝟙_ C ⊗ X) ⊗≫ 𝟙 X ⊗≫ 𝟙 (X ⊗ 𝟙_ C) = (λ_ X).hom ≫ (ρ_ X).inv

Tactic:
monoidal

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X Y Y' : C
inst✝ : ExactPairing X Y'
i : Y ≅ Y'
⊢ Y ◁ (η_ X Y' ≫ X ◁ i.inv) ≫ (α_ Y X Y).inv ≫ (i.hom ▷ X ≫ ε_ X Y') ▷ Y =
    Y ◁ η_ X Y' ⊗≫ (Y ◁ X ◁ i.inv ≫ i.hom ▷ (X ⊗ Y)) ⊗≫ ε_ X Y' ▷ Y

Tactic:
monoidal

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X Y Y' : C
inst✝ : ExactPairing X Y'
i : Y ≅ Y'
⊢ Y ◁ η_ X Y' ⊗≫ (i.hom ▷ (X ⊗ Y') ≫ Y' ◁ X ◁ i.inv) ⊗≫ ε_ X Y' ▷ Y =
    𝟙 (Y ⊗ 𝟙_ C) ⊗≫ (Y ◁ η_ X Y' ≫ i.hom ▷ (X ⊗ Y')) ⊗≫ ((Y' ⊗ X) ◁ i.inv ≫ ε_ X Y' ▷ Y) ⊗≫ 𝟙 (𝟙_ C ⊗ Y)

Tactic:
monoidal

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X Y Y' : C
inst✝ : ExactPairing X Y'
i : Y ≅ Y'
⊢ 𝟙 (Y ⊗ 𝟙_ C) ⊗≫ (i.hom ▷ 𝟙_ C ≫ Y' ◁ η_ X Y') ⊗≫ (ε_ X Y' ▷ Y' ≫ 𝟙_ C ◁ i.inv) ⊗≫ 𝟙 (𝟙_ C ⊗ Y) =
    𝟙 (Y ⊗ 𝟙_ C) ⊗≫ i.hom ⊗≫ (Y' ◁ η_ X Y' ⊗≫ ε_ X Y' ▷ Y') ⊗≫ i.inv ⊗≫ 𝟙 (𝟙_ C ⊗ Y)

Tactic:
monoidal

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X Y Y' : C
inst✝ : ExactPairing X Y'
i : Y ≅ Y'
⊢ 𝟙 (Y ⊗ 𝟙_ C) ⊗≫ i.hom ⊗≫ ⊗𝟙.hom ⊗≫ i.inv ⊗≫ 𝟙 (𝟙_ C ⊗ Y) = 𝟙 (Y ⊗ 𝟙_ C) ⊗≫ (i.hom ≫ i.inv) ⊗≫ 𝟙 (𝟙_ C ⊗ Y)

Tactic:
monoidal

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X Y Y' : C
inst✝ : ExactPairing X Y'
i : Y ≅ Y'
⊢ 𝟙 (Y ⊗ 𝟙_ C) ⊗≫ 𝟙 Y ⊗≫ 𝟙 (𝟙_ C ⊗ Y) = (ρ_ Y).hom ≫ (λ_ Y).inv

Tactic:
monoidal

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X Y Y' : C
inst✝ : ExactPairing X Y'
i : Y ≅ Y'
⊢ (η_ X Y' ≫ X ◁ i.inv) ▷ X ≫ (α_ X Y X).hom ≫ X ◁ (i.hom ▷ X ≫ ε_ X Y') =
    η_ X Y' ▷ X ⊗≫ X ◁ (i.inv ≫ i.hom) ▷ X ≫ X ◁ ε_ X Y'

Tactic:
monoidal

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X Y Y' : C
inst✝ : ExactPairing X Y'
i : Y ≅ Y'
⊢ η_ X Y' ▷ X ⊗≫ X ◁ 𝟙 Y' ▷ X ≫ X ◁ ε_ X Y' = η_ X Y' ▷ X ⊗≫ X ◁ ε_ X Y'

Tactic:
monoidal

Goal state after: