mathlib-initiative/mathlib-tactics huggingface dataset:
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) := ⋯
⊢ ∀ (i : ↑(Basis.ofVectorSpaceIndex K V)),
    ((TensorProduct.mk K (Dual K V) K).compr₂ₛₗ
          (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 i) =
      ((TensorProduct.mk K (Dual K V) K).compr₂ₛₗ
          (↑(TensorProduct.lid K (Dual K V)).symm ∘ₗ ↑(TensorProduct.rid K (Dual K V))))
        ((Basis.ofVectorSpace K V).dualBasis 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
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := ⋯
⊢ ∀ (i : ↑(Basis.ofVectorSpaceIndex K V)),
    ((TensorProduct.mk K (Dual K V) K).compr₂ₛₗ
          (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 i) =
      ((TensorProduct.mk K (Dual K V) K).compr₂ₛₗ
          (↑(TensorProduct.lid K (Dual K V)).symm ∘ₗ ↑(TensorProduct.rid K (Dual K V))))
        ((Basis.ofVectorSpace K V).dualBasis 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)
⊢ ((TensorProduct.mk K (Dual K V) K).compr₂ₛₗ
        (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) =
    ((TensorProduct.mk K (Dual K V) K).compr₂ₛₗ
        (↑(TensorProduct.lid K (Dual K V)).symm ∘ₗ ↑(TensorProduct.rid K (Dual K V))))
      ((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)
⊢ ((TensorProduct.mk K (Dual K V) K).compr₂ₛₗ
        (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) =
    ((TensorProduct.mk K (Dual K V) K).compr₂ₛₗ
        (↑(TensorProduct.lid K (Dual K V)).symm ∘ₗ ↑(TensorProduct.rid K (Dual K V))))
      ((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.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) := ⋯
⊢ ((TensorProduct.mk K K V).compr₂ₛₗ
        (LinearMap.lTensor V (contractLeft K V) ∘ₗ
          ↑(TensorProduct.assoc K V (Dual K V) V) ∘ₗ LinearMap.rTensor V (coevaluation K V)))
      1 =
    ((TensorProduct.mk K K V).compr₂ₛₗ (↑(TensorProduct.rid K V).symm ∘ₗ ↑(TensorProduct.lid K V))) 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) := ⋯
⊢ ((TensorProduct.mk K K V).compr₂ₛₗ
        (LinearMap.lTensor V (contractLeft K V) ∘ₗ
          ↑(TensorProduct.assoc K V (Dual K V) V) ∘ₗ LinearMap.rTensor V (coevaluation K V)))
      1 =
    ((TensorProduct.mk K K V).compr₂ₛₗ (↑(TensorProduct.rid K V).symm ∘ₗ ↑(TensorProduct.lid K V))) 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) := ⋯
⊢ ∀ (i : ↑(Basis.ofVectorSpaceIndex K V)),
    (((TensorProduct.mk K K V).compr₂ₛₗ
            (LinearMap.lTensor V (contractLeft K V) ∘ₗ
              ↑(TensorProduct.assoc K V (Dual K V) V) ∘ₗ LinearMap.rTensor V (coevaluation K V)))
          1)
        ((Basis.ofVectorSpace K V) i) =
      (((TensorProduct.mk K K V).compr₂ₛₗ (↑(TensorProduct.rid K V).symm ∘ₗ ↑(TensorProduct.lid K V))) 1)
        ((Basis.ofVectorSpace K V) 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
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := ⋯
⊢ ∀ (i : ↑(Basis.ofVectorSpaceIndex K V)),
    (((TensorProduct.mk K K V).compr₂ₛₗ
            (LinearMap.lTensor V (contractLeft K V) ∘ₗ
              ↑(TensorProduct.assoc K V (Dual K V) V) ∘ₗ LinearMap.rTensor V (coevaluation K V)))
          1)
        ((Basis.ofVectorSpace K V) i) =
      (((TensorProduct.mk K K V).compr₂ₛₗ (↑(TensorProduct.rid K V).symm ∘ₗ ↑(TensorProduct.lid K V))) 1)
        ((Basis.ofVectorSpace K V) 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.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
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.lTensor V (contractLeft K 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)
⊢ ∑ x,
      (LinearMap.lTensor V (contractLeft K 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
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 (Basis.ofVectorSpace K V) j ⊗ₜ[K] 1 else 0) = (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)
⊢ (if j ∈ Finset.univ then (Basis.ofVectorSpace K V) j ⊗ₜ[K] 1 else 0) = (Basis.ofVectorSpace K V) j ⊗ₜ[K] 1
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : N →ₗ[R] P
x✝² : Dual R M
x✝¹ : N
x✝ : M
⊢ (((AlgebraTensorModule.curry (dualTensorHom R M P ∘ₗ lTensor (Dual R M) f)) x✝²) x✝¹) x✝ =
    (((AlgebraTensorModule.curry (compRight R f ∘ₗ dualTensorHom R M N)) x✝²) x✝¹) x✝

Tactic:
;

Goal state after:
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : N →ₗ[R] P
x✝² : Dual R M
x✝¹ : N
x✝ : M
⊢ (((AlgebraTensorModule.curry (dualTensorHom R M P ∘ₗ lTensor (Dual R M) f)) x✝²) x✝¹) x✝ =
    (((AlgebraTensorModule.curry (compRight R f ∘ₗ dualTensorHom R M N)) x✝²) x✝¹) x✝
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
x✝² : Dual R N
x✝¹ : P
x✝ : M
⊢ (((AlgebraTensorModule.curry (dualTensorHom R M P ∘ₗ rTensor P f.dualMap)) x✝²) x✝¹) x✝ =
    (((AlgebraTensorModule.curry (lcomp R P f ∘ₗ dualTensorHom R N P)) x✝²) x✝¹) x✝

Tactic:
;

Goal state after:
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
x✝² : Dual R N
x✝¹ : P
x✝ : M
⊢ (((AlgebraTensorModule.curry (dualTensorHom R M P ∘ₗ rTensor P f.dualMap)) x✝²) x✝¹) x✝ =
    (((AlgebraTensorModule.curry (lcomp R P f ∘ₗ dualTensorHom R N P)) x✝²) x✝¹) x✝
Module: Mathlib.LinearAlgebra.FreeModule.Finite.Matrix

Goal state before:
pp: K : Type u_1
M : Type u_2
L : Type v
inst✝⁷ : CommRing K
inst✝⁶ : Ring M
inst✝⁵ : Algebra K M
inst✝⁴ : Module.Free K M
inst✝³ : Module.Finite K M
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
⊢ Module.rank K M < ℵ₀

Tactic:
;

Goal state after:
K : Type u_1
M : Type u_2
L : Type v
inst✝⁷ : CommRing K
inst✝⁶ : Ring M
inst✝⁵ : Algebra K M
inst✝⁴ : Module.Free K M
inst✝³ : Module.Finite K M
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
⊢ Module.rank K M < ℵ₀
Module: Mathlib.LinearAlgebra.FreeModule.Finite.Matrix

Goal state before:
pp: K : Type u_1
M : Type u_2
L : Type v
inst✝⁷ : CommRing K
inst✝⁶ : Ring M
inst✝⁵ : Algebra K M
inst✝⁴ : Module.Free K M
inst✝³ : Module.Finite K M
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
this : Nontrivial K
⊢ Module.rank K M < ℵ₀

Tactic:
;

Goal state after:
K : Type u_1
M : Type u_2
L : Type v
inst✝⁷ : CommRing K
inst✝⁶ : Ring M
inst✝⁵ : Algebra K M
inst✝⁴ : Module.Free K M
inst✝³ : Module.Finite K M
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
this : Nontrivial K
⊢ Module.rank K M < ℵ₀
Module: Mathlib.Algebra.Category.FGModuleCat.Basic

Goal state before:
pp: R : Type u
inst✝ : Ring R
⊢ Module.Finite R ↑(ModuleCat.of R PUnit.{v + 1})

Tactic:
;

Goal state after:
R : Type u
inst✝ : Ring R
⊢ Module.Finite R ↑(ModuleCat.of R PUnit.{v + 1})
Module: Mathlib.Algebra.Category.FGModuleCat.Basic

Goal state before:
pp: R : Type u
inst✝⁶ : Ring R
V W : Type v
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : Module.Finite R V
inst✝² : AddCommGroup W
inst✝¹ : Module R W
inst✝ : Module.Finite R W
e : V ≃ₗ[R] W
x : ↑(of R V).obj
⊢ (ModuleCat.Hom.hom (ConcreteCategory.ofHom ↑e ≫ ConcreteCategory.ofHom ↑e.symm).hom) x =
    (ModuleCat.Hom.hom (𝟙 (of R V)).hom) x

Tactic:
;

Goal state after:
R : Type u
inst✝⁶ : Ring R
V W : Type v
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : Module.Finite R V
inst✝² : AddCommGroup W
inst✝¹ : Module R W
inst✝ : Module.Finite R W
e : V ≃ₗ[R] W
x : ↑(of R V).obj
⊢ (ModuleCat.Hom.hom (ConcreteCategory.ofHom ↑e ≫ ConcreteCategory.ofHom ↑e.symm).hom) x =
    (ModuleCat.Hom.hom (𝟙 (of R V)).hom) x
Module: Mathlib.Algebra.Category.FGModuleCat.Basic

Goal state before:
pp: R : Type u
inst✝⁶ : Ring R
V W : Type v
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : Module.Finite R V
inst✝² : AddCommGroup W
inst✝¹ : Module R W
inst✝ : Module.Finite R W
e : V ≃ₗ[R] W
x : ↑(of R W).obj
⊢ (ModuleCat.Hom.hom (ConcreteCategory.ofHom ↑e.symm ≫ ConcreteCategory.ofHom ↑e).hom) x =
    (ModuleCat.Hom.hom (𝟙 (of R W)).hom) x

Tactic:
;

Goal state after:
R : Type u
inst✝⁶ : Ring R
V W : Type v
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : Module.Finite R V
inst✝² : AddCommGroup W
inst✝¹ : Module R W
inst✝ : Module.Finite R W
e : V ≃ₗ[R] W
x : ↑(of R W).obj
⊢ (ModuleCat.Hom.hom (ConcreteCategory.ofHom ↑e.symm ≫ ConcreteCategory.ofHom ↑e).hom) x =
    (ModuleCat.Hom.hom (𝟙 (of R W)).hom) x
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h : 1 ∈ (dualTensorHom R M M).range
s : Finset (Dual R M × M)
eq : (dualTensorHom R M M) (∑ i ∈ s, i.1 ⊗ₜ[R] i.2) = 1
f : (↥s → R) →ₗ[R] M := Fintype.linearCombination R fun x ↦ (↑x).2
x✝ : M
⊢ (f ∘ₗ pi fun x ↦ (↑x).1) x✝ = 1 x✝

Tactic:
;

Goal state after:
R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h : 1 ∈ (dualTensorHom R M M).range
s : Finset (Dual R M × M)
eq : (dualTensorHom R M M) (∑ i ∈ s, i.1 ⊗ₜ[R] i.2) = 1
f : (↥s → R) →ₗ[R] M := Fintype.linearCombination R fun x ↦ (↑x).2
x✝ : M
⊢ (f ∘ₗ pi fun x ↦ (↑x).1) x✝ = 1 x✝
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
M₁ : Type u_6
inst✝⁵ : CommRing R
inst✝⁴ : CommSemiring R₁
inst✝³ : AddCommMonoid M₁
inst✝² : Module R₁ M₁
I : R₁ →+* R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
B : M₁ →ₛₗ[I] M₁ →ₛₗ[I] R
⊢ B.IsAlt ↔ B = -B.flip

Tactic:
constructor <;> intro h
  · ext
    simp_rw [neg_apply, flip_apply]
    exact (h.neg _ _).symm
  intro x
  let h' := congr_fun₂ h x x
  simp only [neg_apply, flip_apply, ← add_eq_zero_iff_eq_neg] at h'
  exact add_self_eq_zero.mp h'

Goal state after:
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: case right
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module.Finite R M
inst✝ : Projective R M
n : ℕ
f : (Fin n → R) →ₗ[R] M
g : M →ₗ[R] Fin n → R
eq : f ∘ₗ g = LinearMap.id
φ : M →ₗ[R] N
x✝ : M
⊢ ((lcomp R N g ∘ₗ lcomp R N f) φ) x✝ = (LinearMap.id φ) x✝

Tactic:
;

Goal state after:
case right
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module.Finite R M
inst✝ : Projective R M
n : ℕ
f : (Fin n → R) →ₗ[R] M
g : M →ₗ[R] Fin n → R
eq : f ∘ₗ g = LinearMap.id
φ : M →ₗ[R] N
x✝ : M
⊢ ((lcomp R N g ∘ₗ lcomp R N f) φ) x✝ = (LinearMap.id φ) x✝
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝¹ : Dual R M
x✝ : M
⊢ (((AlgebraTensorModule.curry (dualTensorHom R M R)) x✝¹) 1) x✝ =
    (((AlgebraTensorModule.curry ↑(TensorProduct.rid R (Dual R M))) x✝¹) 1) x✝

Tactic:
;

Goal state after:
R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝¹ : Dual R M
x✝ : M
⊢ (((AlgebraTensorModule.curry (dualTensorHom R M R)) x✝¹) 1) x✝ =
    (((AlgebraTensorModule.curry ↑(TensorProduct.rid R (Dual R M))) x✝¹) 1) x✝
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : DecidableEq ι
x✝² : Dual R M
a✝¹ : ι
x✝¹ : N
x✝ : M
a✝ : ι
⊢ ((((AlgebraTensorModule.curry (dualTensorHom R M (ι →₀ N))) x✝² ∘ₗ Finsupp.lsingle a✝¹) x✝¹) x✝) a✝ =
    ((((AlgebraTensorModule.curry
                (finsuppLinearMap R ∘ₗ
                  Finsupp.mapRange.linearMap (dualTensorHom R M N) ∘ₗ ↑(finsuppRight R R (Dual R M) N ι)))
              x✝² ∘ₗ
            Finsupp.lsingle a✝¹)
          x✝¹)
        x✝)
      a✝

Tactic:
;

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : DecidableEq ι
x✝² : Dual R M
a✝¹ : ι
x✝¹ : N
x✝ : M
a✝ : ι
⊢ ((((AlgebraTensorModule.curry (dualTensorHom R M (ι →₀ N))) x✝² ∘ₗ Finsupp.lsingle a✝¹) x✝¹) x✝) a✝ =
    ((((AlgebraTensorModule.curry
                (finsuppLinearMap R ∘ₗ
                  Finsupp.mapRange.linearMap (dualTensorHom R M N) ∘ₗ ↑(finsuppRight R R (Dual R M) N ι)))
              x✝² ∘ₗ
            Finsupp.lsingle a✝¹)
          x✝¹)
        x✝)
      a✝
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : DecidableEq ι
x✝² : Dual R M
a✝¹ : ι
x✝¹ : N
x✝ : M
a✝ : ι
⊢ (if a✝¹ = a✝ then x✝² x✝ • x✝¹ else 0) = (if a✝¹ = a✝ then (dualTensorHom R M N) (x✝² ⊗ₜ[R] x✝¹) else 0) x✝

Tactic:
;

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : DecidableEq ι
x✝² : Dual R M
a✝¹ : ι
x✝¹ : N
x✝ : M
a✝ : ι
⊢ (if a✝¹ = a✝ then x✝² x✝ • x✝¹ else 0) = (if a✝¹ = a✝ then (dualTensorHom R M N) (x✝² ⊗ₜ[R] x✝¹) else 0) x✝
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : N →ₗ[R] P
g : P →ₗ[R] N
comp_eq_id : g ∘ₗ f = LinearMap.id
h : Function.Bijective ⇑(dualTensorHom R M P)
x✝¹ : M →ₗ[R] N
x✝ : M
⊢ ((compRight R g ∘ₗ compRight R f) x✝¹) x✝ = (LinearMap.id x✝¹) x✝

Tactic:
;

Goal state after:
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : N →ₗ[R] P
g : P →ₗ[R] N
comp_eq_id : g ∘ₗ f = LinearMap.id
h : Function.Bijective ⇑(dualTensorHom R M P)
x✝¹ : M →ₗ[R] N
x✝ : M
⊢ ((compRight R g ∘ₗ compRight R f) x✝¹) x✝ = (LinearMap.id x✝¹) x✝
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Finite ι
h : Function.Bijective ⇑(dualTensorHom R M N)
x✝¹ : ι → N
x✝ : ι
⊢ (↑(Finsupp.linearEquivFunOnFinite R N ι) ∘ₗ ↑(Finsupp.linearEquivFunOnFinite R N ι).symm) x✝¹ x✝ = LinearMap.id x✝¹ x✝

Tactic:
;

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Finite ι
h : Function.Bijective ⇑(dualTensorHom R M N)
x✝¹ : ι → N
x✝ : ι
⊢ (↑(Finsupp.linearEquivFunOnFinite R N ι) ∘ₗ ↑(Finsupp.linearEquivFunOnFinite R N ι).symm) x✝¹ x✝ = LinearMap.id x✝¹ x✝
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
b : Basis ι R M
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
x✝¹ : Dual R M ⊗[R] N
x✝ : M
⊢ ((dualTensorHomEquiv R M N) x✝¹) x✝ = ((dualTensorHomEquivOfBasis b) x✝¹) x✝

Tactic:
;

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
b : Basis ι R M
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
x✝¹ : Dual R M ⊗[R] N
x✝ : M
⊢ ((dualTensorHomEquiv R M N) x✝¹) x✝ = ((dualTensorHomEquivOfBasis b) x✝¹) x✝
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: R : Type u_1
M : Type u_5
M₁ : Type u_6
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₁
inst✝ : Module R M₁
B : M →ₗ[R] M →ₗ[R] M₁
hB : B.IsRefl
hB' : B.SeparatingRight
⊢ B.SeparatingLeft

Tactic:
separatingLeft_iff_ker_eq_bot,

Goal state after:
R : Type u_1
M : Type u_5
M₁ : Type u_6
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₁
inst✝ : Module R M₁
B : M →ₗ[R] M →ₗ[R] M₁
hB : B.IsRefl
hB' : B.SeparatingRight
⊢ B.ker = ⊥