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

Goal state after:
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)
Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas

Goal state before:
pp: case neg
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
m : ℕ
h_cases : finrank K V ≤ m
⊢ LinearMap.ker (f ^ finrank K V) ≤ LinearMap.ker (f ^ finrank K V)

Tactic:
]

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

Goal state before:
pp: K : Type u
V : Type v
W : Type v'
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : Module K W
f : V →ₗ[K] W
p : Submodule K W
inst✝¹ : FiniteDimensional K ↥p
inst✝ : FiniteDimensional K ↥f.ker
⊢ lift.{v, v'} (Module.rank K ↥p) + lift.{v', v} (Module.rank K ↥f.ker) < ℵ₀

Tactic:
]

Goal state after:
K : Type u
V : Type v
W : Type v'
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : Module K W
f : V →ₗ[K] W
p : Submodule K W
inst✝¹ : FiniteDimensional K ↥p
inst✝ : FiniteDimensional K ↥f.ker
⊢ lift.{v, v'} (Module.rank K ↥p) + lift.{v', v} (Module.rank K ↥f.ker) < ℵ₀
Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas

Goal state before:
pp: case ha
K : Type u
V : Type v
W : Type v'
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : Module K W
f : V →ₗ[K] W
p : Submodule K W
inst✝¹ : FiniteDimensional K ↥p
inst✝ : FiniteDimensional K ↥f.ker
⊢ Module.Finite K ↥p

Tactic:
]

Goal state after:
case ha
K : Type u
V : Type v
W : Type v'
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : Module K W
f : V →ₗ[K] W
p : Submodule K W
inst✝¹ : FiniteDimensional K ↥p
inst✝ : FiniteDimensional K ↥f.ker
⊢ Module.Finite K ↥p
Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas

Goal state before:
pp: case hb
K : Type u
V : Type v
W : Type v'
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : Module K W
f : V →ₗ[K] W
p : Submodule K W
inst✝¹ : FiniteDimensional K ↥p
inst✝ : FiniteDimensional K ↥f.ker
⊢ Module.Finite K ↥f.ker

Tactic:
]

Goal state after:
case hb
K : Type u
V : Type v
W : Type v'
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : Module K W
f : V →ₗ[K] W
p : Submodule K W
inst✝¹ : FiniteDimensional K ↥p
inst✝ : FiniteDimensional K ↥f.ker
⊢ Module.Finite K ↥f.ker
Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas

Goal state before:
pp: K : Type u
V : Type v
W : Type v'
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : Module K W
f : V →ₗ[K] W
p : Submodule K V
inst✝¹ : FiniteDimensional K (V ⧸ p)
inst✝ : FiniteDimensional K (W ⧸ f.range)
⊢ lift.{v, v'} (Module.rank K (W ⧸ f.range)) + lift.{v', v} (Module.rank K (V ⧸ p)) < ℵ₀

Tactic:
]

Goal state after:
K : Type u
V : Type v
W : Type v'
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : Module K W
f : V →ₗ[K] W
p : Submodule K V
inst✝¹ : FiniteDimensional K (V ⧸ p)
inst✝ : FiniteDimensional K (W ⧸ f.range)
⊢ lift.{v, v'} (Module.rank K (W ⧸ f.range)) + lift.{v', v} (Module.rank K (V ⧸ p)) < ℵ₀
Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas

Goal state before:
pp: case ha
K : Type u
V : Type v
W : Type v'
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : Module K W
f : V →ₗ[K] W
p : Submodule K V
inst✝¹ : FiniteDimensional K (V ⧸ p)
inst✝ : FiniteDimensional K (W ⧸ f.range)
⊢ Module.Finite K (W ⧸ f.range)

Tactic:
]

Goal state after:
case ha
K : Type u
V : Type v
W : Type v'
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : Module K W
f : V →ₗ[K] W
p : Submodule K V
inst✝¹ : FiniteDimensional K (V ⧸ p)
inst✝ : FiniteDimensional K (W ⧸ f.range)
⊢ Module.Finite K (W ⧸ f.range)
Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas

Goal state before:
pp: case hb
K : Type u
V : Type v
W : Type v'
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : Module K W
f : V →ₗ[K] W
p : Submodule K V
inst✝¹ : FiniteDimensional K (V ⧸ p)
inst✝ : FiniteDimensional K (W ⧸ f.range)
⊢ Module.Finite K (V ⧸ p)

Tactic:
]

Goal state after:
case hb
K : Type u
V : Type v
W : Type v'
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : Module K W
f : V →ₗ[K] W
p : Submodule K V
inst✝¹ : FiniteDimensional K (V ⧸ p)
inst✝ : FiniteDimensional K (W ⧸ f.range)
⊢ Module.Finite K (V ⧸ p)
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:
]

Goal state after:
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)
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:
]

Goal state after:
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)
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:
]

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

Goal state after:
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)
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:
]

Goal state after:
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)
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:
]

Goal state after:
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)
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:
]

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

Goal state after:
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'
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'
⊢  ⊗𝟙.hom = (λ_ X).hom ≫ (ρ_ X).inv

Tactic:
]

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X Y Y' : C
inst✝ : ExactPairing X Y'
i : Y ≅ Y'
⊢  ⊗𝟙.hom = (λ_ X).hom ≫ (ρ_ X).inv
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
p₁ : ExactPairing X Y₁
p₂ : ExactPairing X Y₂
⊢ 𝟙 Xᘁ = 𝟙 Y₁

Tactic:
]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y₁ Y₂ : C
p₁ : ExactPairing X Y₁
p₂ : ExactPairing X Y₂
⊢ 𝟙 Xᘁ = 𝟙 Y₁
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
p₁ : ExactPairing X Y₁
p₂ : ExactPairing X Y₂
⊢ 𝟙 Xᘁ = 𝟙 Y₂

Tactic:
]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y₁ Y₂ : C
p₁ : ExactPairing X Y₁
p₂ : ExactPairing X Y₂
⊢ 𝟙 Xᘁ = 𝟙 Y₂
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
p₁ : ExactPairing X₁ Y
p₂ : ExactPairing X₂ Y
⊢ 𝟙 ᘁY = 𝟙 X₁

Tactic:
]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X₁ X₂ Y : C
p₁ : ExactPairing X₁ Y
p₂ : ExactPairing X₂ Y
⊢ 𝟙 ᘁY = 𝟙 X₁
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
p₁ : ExactPairing X₁ Y
p₂ : ExactPairing X₂ Y
⊢ 𝟙 ᘁY = 𝟙 X₂

Tactic:
]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X₁ X₂ Y : C
p₁ : ExactPairing X₁ Y
p₂ : ExactPairing X₂ Y
⊢ 𝟙 ᘁY = 𝟙 X₂
Module: Mathlib.LinearAlgebra.Coevaluation

Goal state before:
pp: K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
⊢ ∑ i,
      (Basis.singleton Unit K).equivFun 1 i • ∑ i, (Basis.ofVectorSpace K V) i ⊗ₜ[K] (Basis.ofVectorSpace K V).coord i =
    ∑ i, (Basis.ofVectorSpace K V) i ⊗ₜ[K] (Basis.ofVectorSpace K V).coord i

Tactic:
]

Goal state after:
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
⊢ ∑ i,
      (Basis.singleton Unit K).equivFun 1 i • ∑ i, (Basis.ofVectorSpace K V) i ⊗ₜ[K] (Basis.ofVectorSpace K V).coord i =
    ∑ i, (Basis.ofVectorSpace K V) i ⊗ₜ[K] (Basis.ofVectorSpace K V).coord i
Module: Mathlib.LinearAlgebra.Coevaluation

Goal state before:
pp: K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ (LinearMap.rTensor (Dual K V) (contractLeft K V) ∘ₗ
        ↑(TensorProduct.assoc K (Dual K V) V (Dual K V)).symm ∘ₗ LinearMap.lTensor (Dual K V) (coevaluation K V))
      ((Basis.ofVectorSpace K V).dualBasis j ⊗ₜ[K] 1) =
    (↑(TensorProduct.lid K (Dual K V)).symm ∘ₗ ↑(TensorProduct.rid K (Dual K V)))
      ((Basis.ofVectorSpace K V).dualBasis j ⊗ₜ[K] 1)

Tactic:
]

Goal state after:
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ (LinearMap.rTensor (Dual K V) (contractLeft K V) ∘ₗ
        ↑(TensorProduct.assoc K (Dual K V) V (Dual K V)).symm ∘ₗ LinearMap.lTensor (Dual K V) (coevaluation K V))
      ((Basis.ofVectorSpace K V).dualBasis j ⊗ₜ[K] 1) =
    (↑(TensorProduct.lid K (Dual K V)).symm ∘ₗ ↑(TensorProduct.rid K (Dual K V)))
      ((Basis.ofVectorSpace K V).dualBasis j ⊗ₜ[K] 1)
Module: Mathlib.LinearAlgebra.Coevaluation

Goal state before:
pp: K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ (LinearMap.rTensor (Dual K V) (contractLeft K V))
      ((TensorProduct.assoc K (Dual K V) V (Dual K V)).symm
        ((LinearMap.lTensor (Dual K V) (coevaluation K V)) ((Basis.ofVectorSpace K V).dualBasis j ⊗ₜ[K] 1))) =
    1 ⊗ₜ[K] (Basis.ofVectorSpace K V).dualBasis j

Tactic:
]

Goal state after:
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ (LinearMap.rTensor (Dual K V) (contractLeft K V))
      ((TensorProduct.assoc K (Dual K V) V (Dual K V)).symm
        ((LinearMap.lTensor (Dual K V) (coevaluation K V)) ((Basis.ofVectorSpace K V).dualBasis j ⊗ₜ[K] 1))) =
    1 ⊗ₜ[K] (Basis.ofVectorSpace K V).dualBasis j
Module: Mathlib.LinearAlgebra.Coevaluation

Goal state before:
pp: K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ (LinearMap.rTensor (Dual K V) (contractLeft K V))
      (∑ x,
        (TensorProduct.assoc K (Dual K V) V (Dual K V)).symm
          ((Basis.ofVectorSpace K V).dualBasis j ⊗ₜ[K]
            ((Basis.ofVectorSpace K V) x ⊗ₜ[K] (Basis.ofVectorSpace K V).coord x))) =
    1 ⊗ₜ[K] (Basis.ofVectorSpace K V).dualBasis j

Tactic:
]

Goal state after:
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ (LinearMap.rTensor (Dual K V) (contractLeft K V))
      (∑ x,
        (TensorProduct.assoc K (Dual K V) V (Dual K V)).symm
          ((Basis.ofVectorSpace K V).dualBasis j ⊗ₜ[K]
            ((Basis.ofVectorSpace K V) x ⊗ₜ[K] (Basis.ofVectorSpace K V).coord x))) =
    1 ⊗ₜ[K] (Basis.ofVectorSpace K V).dualBasis j
Module: Mathlib.LinearAlgebra.Coevaluation

Goal state before:
pp: K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ ∑ x,
      (LinearMap.rTensor (Dual K V) (contractLeft K V))
        ((Basis.ofVectorSpace K V).dualBasis j ⊗ₜ[K] (Basis.ofVectorSpace K V) x ⊗ₜ[K]
          (Basis.ofVectorSpace K V).coord x) =
    1 ⊗ₜ[K] (Basis.ofVectorSpace K V).dualBasis j

Tactic:
]

Goal state after:
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ ∑ x,
      (LinearMap.rTensor (Dual K V) (contractLeft K V))
        ((Basis.ofVectorSpace K V).dualBasis j ⊗ₜ[K] (Basis.ofVectorSpace K V) x ⊗ₜ[K]
          (Basis.ofVectorSpace K V).coord x) =
    1 ⊗ₜ[K] (Basis.ofVectorSpace K V).dualBasis j
Module: Mathlib.LinearAlgebra.Coevaluation

Goal state before:
pp: K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ (if j ∈ Finset.univ then 1 ⊗ₜ[K] (Basis.ofVectorSpace K V).coord j else 0) = 1 ⊗ₜ[K] (Basis.ofVectorSpace K V).coord j

Tactic:
]

Goal state after:
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ (if j ∈ Finset.univ then 1 ⊗ₜ[K] (Basis.ofVectorSpace K V).coord j else 0) = 1 ⊗ₜ[K] (Basis.ofVectorSpace K V).coord j
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring R₁
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : Module R₁ M₁
inst✝⁴ : CommSemiring R₂
inst✝³ : AddCommMonoid M₂
inst✝² : Module R₂ M₂
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I₁ : R₁ →+* R
I₂ : R₂ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M
x : M₂
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Coevaluation

Goal state before:
pp: K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ (LinearMap.lTensor V (contractLeft K V) ∘ₗ
        ↑(TensorProduct.assoc K V (Dual K V) V) ∘ₗ LinearMap.rTensor V (coevaluation K V))
      (1 ⊗ₜ[K] (Basis.ofVectorSpace K V) j) =
    (↑(TensorProduct.rid K V).symm ∘ₗ ↑(TensorProduct.lid K V)) (1 ⊗ₜ[K] (Basis.ofVectorSpace K V) j)

Tactic:
]

Goal state after:
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ (LinearMap.lTensor V (contractLeft K V) ∘ₗ
        ↑(TensorProduct.assoc K V (Dual K V) V) ∘ₗ LinearMap.rTensor V (coevaluation K V))
      (1 ⊗ₜ[K] (Basis.ofVectorSpace K V) j) =
    (↑(TensorProduct.rid K V).symm ∘ₗ ↑(TensorProduct.lid K V)) (1 ⊗ₜ[K] (Basis.ofVectorSpace K V) j)
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: case mp
K : Type u_13
K₁ : Type u_14
K₂ : Type u_15
V : Type u_16
V₁ : Type u_17
V₂ : Type u_18
inst✝⁸ : Field K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
inst✝⁵ : Field K₁
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K₁ V₁
inst✝² : Field K₂
inst✝¹ : AddCommGroup V₂
inst✝ : Module K₂ V₂
I₁ : K₁ →+* K
I₂ : K₂ →+* K
B : V₁ →ₛₗ[I₁] V₂ →ₛₗ[I₂] V
x : V₁
y : V₂
a : K₁
ha : a ≠ 0
H : (B x) y = 0
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Coevaluation

Goal state before:
pp: K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ (LinearMap.lTensor V (contractLeft K V))
      ((TensorProduct.assoc K V (Dual K V) V)
        ((LinearMap.rTensor V (coevaluation K V)) (1 ⊗ₜ[K] (Basis.ofVectorSpace K V) j))) =
    (Basis.ofVectorSpace K V) j ⊗ₜ[K] 1

Tactic:
]

Goal state after:
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ (LinearMap.lTensor V (contractLeft K V))
      ((TensorProduct.assoc K V (Dual K V) V)
        ((LinearMap.rTensor V (coevaluation K V)) (1 ⊗ₜ[K] (Basis.ofVectorSpace K V) j))) =
    (Basis.ofVectorSpace K V) j ⊗ₜ[K] 1
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: case mpr
K : Type u_13
K₁ : Type u_14
K₂ : Type u_15
V : Type u_16
V₁ : Type u_17
V₂ : Type u_18
inst✝⁸ : Field K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
inst✝⁵ : Field K₁
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K₁ V₁
inst✝² : Field K₂
inst✝¹ : AddCommGroup V₂
inst✝ : Module K₂ V₂
I₁ : K₁ →+* K
I₂ : K₂ →+* K
B : V₁ →ₛₗ[I₁] V₂ →ₛₗ[I₂] V
x : V₁
y : V₂
a : K₁
ha : a ≠ 0
H : I₁ a = 0 ∨ (B x) y = 0
⊢ (B x) y = 0

Tactic:
]

Goal state after:
case mpr
K : Type u_13
K₁ : Type u_14
K₂ : Type u_15
V : Type u_16
V₁ : Type u_17
V₂ : Type u_18
inst✝⁸ : Field K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
inst✝⁵ : Field K₁
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K₁ V₁
inst✝² : Field K₂
inst✝¹ : AddCommGroup V₂
inst✝ : Module K₂ V₂
I₁ : K₁ →+* K
I₂ : K₂ →+* K
B : V₁ →ₛₗ[I₁] V₂ →ₛₗ[I₂] V
x : V₁
y : V₂
a : K₁
ha : a ≠ 0
H : I₁ a = 0 ∨ (B x) y = 0
⊢ (B x) y = 0
Module: Mathlib.LinearAlgebra.Coevaluation

Goal state before:
pp: K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ (LinearMap.lTensor V (contractLeft K V))
      (∑ x,
        (TensorProduct.assoc K V (Dual K V) V)
          ((Basis.ofVectorSpace K V) x ⊗ₜ[K] (Basis.ofVectorSpace K V).coord x ⊗ₜ[K] (Basis.ofVectorSpace K V) j)) =
    (Basis.ofVectorSpace K V) j ⊗ₜ[K] 1

Tactic:
]

Goal state after:
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ (LinearMap.lTensor V (contractLeft K V))
      (∑ x,
        (TensorProduct.assoc K V (Dual K V) V)
          ((Basis.ofVectorSpace K V) x ⊗ₜ[K] (Basis.ofVectorSpace K V).coord x ⊗ₜ[K] (Basis.ofVectorSpace K V) j)) =
    (Basis.ofVectorSpace K V) j ⊗ₜ[K] 1