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) := 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.SesquilinearForm.Basic

Goal state before:
pp: case mpr.inl
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 : a = 0
⊢ (B x) y = 0

Tactic:
]

Goal state after:
case mpr.inl
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 : a = 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)
⊢ (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.FreeModule.Finite.Matrix

Goal state before:
pp: R : Type u
S : Type u'
M : Type v
N : Type w
inst✝¹² : Ring R
inst✝¹¹ : Ring S
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
inst✝⁸ : Free R M
inst✝⁷ : Module.Finite R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
inst✝⁴ : Module S N
inst✝³ : SMulCommClass R S N
inst✝² : StrongRankCondition R
inst✝¹ : StrongRankCondition S
inst✝ : Free S N
⊢ ↑(finrank R M) * lift.{v, w} (Module.rank S N) = ↑(finrank R M) * lift.{v, w} (Module.rank S N)

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.Finite.Matrix

Goal state before:
pp: R : Type u
S : Type u'
M : Type v
inst✝⁹ : Ring R
inst✝⁸ : Ring S
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : StrongRankCondition R
inst✝² : StrongRankCondition S
inst✝¹ : Module R S
inst✝ : SMulCommClass R S S
⊢ lift.{u', v} (Module.rank R M) = lift.{u', v} (Module.rank R M)

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.Finite.Matrix

Goal state before:
pp: R : Type u
S : Type u'
M : Type v
inst✝⁹ : Ring R
inst✝⁸ : Ring S
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : StrongRankCondition R
inst✝² : StrongRankCondition S
inst✝¹ : Module R S
inst✝ : SMulCommClass R S S
⊢ finrank R M = finrank R M

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.Finite.Matrix

Goal state before:
pp: case e'_3
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
⊢ #(M →ₐ[K] L) = #(M →ₐ[K] L)

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: K : Type u_13
K₁ : Type u_14
V : Type u_16
V₁ : Type u_17
n : Type u_19
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : Field K₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K₁ V₁
I₁ I₁' : K₁ →+* K
B : V₁ →ₛₗ[I₁] V₁ →ₛₗ[I₁'] V
v : n → V₁
hv₁ : B.IsOrthoᵢ v
hv₂ : ∀ (i : n), (B (v i)) (v i) ≠ 0
⊢ ∀ (s : Finset n) (g : n → K₁), ∑ i ∈ s, g i • v i = 0 → ∀ i ∈ s, g i = 0

Tactic:
]

Goal state after:
K : Type u_13
K₁ : Type u_14
V : Type u_16
V₁ : Type u_17
n : Type u_19
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : Field K₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K₁ V₁
I₁ I₁' : K₁ →+* K
B : V₁ →ₛₗ[I₁] V₁ →ₛₗ[I₁'] V
v : n → V₁
hv₁ : B.IsOrthoᵢ v
hv₂ : ∀ (i : n), (B (v i)) (v i) ≠ 0
⊢ ∀ (s : Finset n) (g : n → K₁), ∑ i ∈ s, g i • v i = 0 → ∀ i ∈ s, g i = 0
Module: Mathlib.LinearAlgebra.FreeModule.Finite.Matrix

Goal state before:
pp: case e'_4
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
⊢ lift.{v, u_2} (Module.rank K M) = lift.{v, u_2} (Module.rank K M)

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.Finite.Matrix

Goal state before:
pp: case e'_4
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
⊢ toNat (Module.rank K M) = toNat (Module.rank K M)

Tactic:
]

Goal state after:
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.SesquilinearForm.Basic

Goal state before:
pp: K : Type u_13
K₁ : Type u_14
V : Type u_16
V₁ : Type u_17
n : Type u_19
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : Field K₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K₁ V₁
I₁ I₁' : K₁ →+* K
B : V₁ →ₛₗ[I₁] V₁ →ₛₗ[I₁'] V
v : n → V₁
hv₁ : B.IsOrthoᵢ v
hv₂ : ∀ (i : n), (B (v i)) (v i) ≠ 0
s : Finset n
w : n → K₁
hs : ∑ i ∈ s, w i • v i = 0
i : n
hi : i ∈ s
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: K : Type u_13
K₁ : Type u_14
V : Type u_16
V₁ : Type u_17
n : Type u_19
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : Field K₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K₁ V₁
I₁ I₁' : K₁ →+* K
B : V₁ →ₛₗ[I₁] V₁ →ₛₗ[I₁'] V
v : n → V₁
hv₁ : B.IsOrthoᵢ v
hv₂ : ∀ (i : n), (B (v i)) (v i) ≠ 0
s : Finset n
w : n → K₁
hs : ∑ i ∈ s, w i • v i = 0
i : n
hi : i ∈ s
this : (B (∑ i ∈ s, w i • v i)) (v i) = 0
j : n
_hj : j ∈ s
hij : j ≠ i
⊢ 0 = 0

Tactic:
]

Goal state after:
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 : Dual R M
n : N
g : Dual R N
p : P
m : M
⊢ g n • f m • p = g n • f m • p

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : CommSemiring R₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M
H : B.IsRefl
h : B.ker = ⊥
⊢ B.ker = ⊥

Tactic:
]

Goal state after:
R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : CommSemiring R₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M
H : B.IsRefl
h : B.ker = ⊥
⊢ B.ker = ⊥
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : CommSemiring R₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M
H : B.IsRefl
⊢ B.ker = ⊥ ↔ B.ker = ⊥

pp: R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : CommSemiring R₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M
H : B.IsRefl
⊢ B.IsRefl

Tactic:
]

Goal state after:
R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : CommSemiring R₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M
H : B.IsRefl
⊢ B.IsRefl
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : R →+* R
B : M →ₛₗ[I] M →ₗ[R] R
H : B.IsSymm
x y : M
H1 : (B x) y = 0
⊢ I ((B x) y) = 0

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_5
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : R →+* R
B : M →ₛₗ[I] M →ₗ[R] R
H : B.IsSymm
x y : M
H1 : (B x) y = 0
⊢ I ((B x) y) = 0
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: case neg
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
m : Type u_7
n : Type u_8
inst✝³ : Fintype m
inst✝² : Finite n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
bM : Basis m R M
bN : Basis n R N
j : m
i i' : n
j' : m
hij : ¬i = i' ∨ ¬j = j'
⊢ (toMatrix bM bN) ((dualTensorHom R M N) (bM.coord j ⊗ₜ[R] bN i)) i' j' = Matrix.single i j 1 i' j'

Tactic:
]

Goal state after:
case neg
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
m : Type u_7
n : Type u_8
inst✝³ : Fintype m
inst✝² : Finite n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
bM : Basis m R M
bN : Basis n R N
j : m
i i' : n
j' : m
hij : ¬i = i' ∨ ¬j = j'
⊢ (toMatrix bM bN) ((dualTensorHom R M N) (bM.coord j ⊗ₜ[R] bN i)) i' j' = Matrix.single i j 1 i' j'
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : CommSemiring R₁
inst✝² : AddCommMonoid M₁
inst✝¹ : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M
H : B.IsAlt
inst✝ : IsCancelAdd M
a b c : M₁
hAdd : a + b + c = 0
this : (B a) c + (B a) b = (B a) c + (B b) c
⊢ (B a) b = (B b) c

Tactic:
]

Goal state after:
R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : CommSemiring R₁
inst✝² : AddCommMonoid M₁
inst✝¹ : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M
H : B.IsAlt
inst✝ : IsCancelAdd M
a b c : M₁
hAdd : a + b + c = 0
this : (B a) c + (B a) b = (B a) c + (B b) c
⊢ (B a) b = (B b) c
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : CommSemiring R₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M
H : B.IsAlt
x y : M₁
h : (B x) y = 0
⊢ 0 = 0

Tactic:
]

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

Tactic:
]

Goal state after:
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 : M →ₗ[R] N
⊢ x = x

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: case left
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
⊢ Function.Injective (⇑(dualTensorHomEquivOfBasis (Pi.basisFun R (Fin n))) ∘ ⇑(rTensor N f.dualMap))

Tactic:
]

Goal state after:
case left
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
⊢ Function.Injective (⇑(dualTensorHomEquivOfBasis (Pi.basisFun R (Fin n))) ∘ ⇑(rTensor N f.dualMap))
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: case mp
R : Type u_1
M : Type u_5
M₁ : Type u_6
M₃ : Type u_8
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
I : R →+* R
B : M →ₗ[R] M →ₛₗ[I] M₃
B' : M₁ →ₗ[R] M₁ →ₛₗ[I] M₃
f : M →ₗ[R] M₁
g : M₁ →ₗ[R] M
h : B.IsAdjointPair B' ⇑f ⇑g
x : M
y : M₁
⊢ (B' (f x)) y = (B x) (g y)

Tactic:
]

Goal state after:
case mp
R : Type u_1
M : Type u_5
M₁ : Type u_6
M₃ : Type u_8
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
I : R →+* R
B : M →ₗ[R] M →ₛₗ[I] M₃
B' : M₁ →ₗ[R] M₁ →ₛₗ[I] M₃
f : M →ₗ[R] M₁
g : M₁ →ₗ[R] M
h : B.IsAdjointPair B' ⇑f ⇑g
x : M
y : M₁
⊢ (B' (f x)) y = (B x) (g y)
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_5
M₁ : Type u_6
M₃ : Type u_8
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
I : R →+* R
B : M →ₗ[R] M →ₛₗ[I] M₃
B' : M₁ →ₗ[R] M₁ →ₛₗ[I] M₃
f : M →ₗ[R] M₁
g : M₁ →ₗ[R] M
h : B' ∘ₗ f = B.compl₂ g
x✝ : M
y✝ : M₁
⊢ ((B.compl₂ g) x✝) y✝ = ((B.compl₂ g) x✝) y✝

Tactic:
]

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
⊢ Function.Surjective (⇑(lcomp R N g) ∘ ⇑(dualTensorHomEquivOfBasis (Pi.basisFun R (Fin n))))

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
⊢ Function.Surjective (⇑(lcomp R N g) ∘ ⇑(dualTensorHomEquivOfBasis (Pi.basisFun R (Fin n))))
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: R : Type u_1
M : Type u_5
M₁ : Type u_6
M₃ : Type u_8
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
I : R →+* R
B : M →ₗ[R] M →ₛₗ[I] M₃
B' : M₁ →ₗ[R] M₁ →ₛₗ[I] M₃
f f' : M → M₁
g g' : M₁ → M
h : B.IsAdjointPair B' f g
h' : B.IsAdjointPair B' f' g'
x : M
x✝ : M₁
⊢ (B x) (g x✝) + (B x) (g' x✝) = (B x) (g x✝) + (B x) (g' x✝)

Tactic:
]

Goal state after:
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
fin : Finite ι ∨ Module.Finite R M
h : Function.Bijective ⇑(dualTensorHom R M N)
⊢ Function.Bijective
    (⇑(finsuppLinearMap R) ∘ ⇑(Finsupp.mapRange.linearMap (dualTensorHom R M N) ∘ₗ ↑(finsuppRight R R (Dual R M) N ι)))

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
fin : Finite ι ∨ Module.Finite R M
h : Function.Bijective ⇑(dualTensorHom R M N)
⊢ Function.Bijective
    (⇑(finsuppLinearMap R) ∘ ⇑(Finsupp.mapRange.linearMap (dualTensorHom R M N) ∘ₗ ↑(finsuppRight R R (Dual R M) N ι)))
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: R : Type u_1
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : Module R M₁
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
I : R →+* R
B : M →ₗ[R] M →ₛₗ[I] M₃
B' : M₁ →ₗ[R] M₁ →ₛₗ[I] M₃
B'' : M₂ →ₗ[R] M₂ →ₛₗ[I] M₃
f : M → M₁
g : M₁ → M
f' : M₁ → M₂
g' : M₂ → M₁
h : B.IsAdjointPair B' f g
h' : B'.IsAdjointPair B'' f' g'
x✝¹ : M
x✝ : M₂
⊢ (B x✝¹) (g (g' x✝)) = (B x✝¹) ((fun x ↦ g (g' x)) x✝)

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: R : Type u_1
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup M₁
inst✝² : Module R M₁
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
B : M →ₗ[R] M →ₗ[R] M₂
B' : M₁ →ₗ[R] M₁ →ₗ[R] M₂
f f' : M → M₁
g g' : M₁ → M
h : B.IsAdjointPair B' f g
h' : B.IsAdjointPair B' f' g'
x : M
x✝ : M₁
⊢ (B x) (g x✝) - (B x) (g' x✝) = (B x) (g x✝) - (B x) (g' x✝)

Tactic:
]

Goal state after:
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)
⊢ Function.Injective ⇑(dualTensorHom R M P ∘ₗ lTensor (Dual R M) f)

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)
⊢ Function.Injective ⇑(dualTensorHom R M P ∘ₗ lTensor (Dual R M) f)
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: R : Type u_20
M : Type u_21
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
B : LinearMap.BilinForm R M
F : Type u_22
inst✝¹ : FunLike F M M
inst✝ : LinearMapClass F R M M
f : F
h : IsLeftRegular 2
hB : IsSymm B
hf : ∀ (x : M), (B (f x)) (f x) = (B x) x
x y : M
this : (B x) x + (B (f x)) (f y) + ((B (f x)) (f y) + (B y) y) = (B x) x + (B x) y + ((B x) y + (B y) y)
⊢ 2 * (B (f x)) (f y) = 2 * (B x) y

Tactic:
]

Goal state after:
R : Type u_20
M : Type u_21
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
B : LinearMap.BilinForm R M
F : Type u_22
inst✝¹ : FunLike F M M
inst✝ : LinearMapClass F R M M
f : F
h : IsLeftRegular 2
hB : IsSymm B
hf : ∀ (x : M), (B (f x)) (f x) = (B x) x
x y : M
this : (B x) x + (B (f x)) (f y) + ((B (f x)) (f y) + (B y) y) = (B x) x + (B x) y + ((B x) y + (B y) y)
⊢ 2 * (B (f x)) (f y) = 2 * (B x) y
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)
⊢ LinearMap.id = LinearMap.id

Tactic:
]

Goal state after:
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)
⊢ Function.Surjective (⇑(compRight R g) ∘ ⇑(dualTensorHom R M P))

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)
⊢ Function.Surjective (⇑(compRight R g) ∘ ⇑(dualTensorHom R M P))
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: R : Type u_1
M : Type u_5
M₂ : Type u_7
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
B : M →ₗ[R] M →ₗ[R] M₂
f : End R M
⊢ f ∈ B.skewAdjointSubmodule ↔ (-B).IsAdjointPair B ⇑f ⇑f

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_5
M₂ : Type u_7
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
B : M →ₗ[R] M →ₗ[R] M₂
f : End R M
⊢ f ∈ B.skewAdjointSubmodule ↔ (-B).IsAdjointPair B ⇑f ⇑f
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: R : Type u_1
M : Type u_5
Mₗ₁ : Type u_9
Mₗ₁' : Type u_10
Mₗ₂ : Type u_11
Mₗ₂' : Type u_12
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : AddCommMonoid Mₗ₁
inst✝⁶ : AddCommMonoid Mₗ₂
inst✝⁵ : AddCommMonoid Mₗ₁'
inst✝⁴ : AddCommMonoid Mₗ₂'
inst✝³ : Module R Mₗ₁
inst✝² : Module R Mₗ₂
inst✝¹ : Module R Mₗ₁'
inst✝ : Module R Mₗ₂'
B : Mₗ₁ →ₗ[R] Mₗ₂ →ₗ[R] M
e₁ : Mₗ₁ ≃ₗ[R] Mₗ₁'
e₂ : Mₗ₂ ≃ₗ[R] Mₗ₂'
h : B.SeparatingLeft
x : Mₗ₁'
hx : ∀ (y : Mₗ₂'), (((e₁.arrowCongr (e₂.arrowCongr (LinearEquiv.refl R M))) B) x) y = 0
⊢ e₁.symm x = 0

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_5
Mₗ₁ : Type u_9
Mₗ₁' : Type u_10
Mₗ₂ : Type u_11
Mₗ₂' : Type u_12
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : AddCommMonoid Mₗ₁
inst✝⁶ : AddCommMonoid Mₗ₂
inst✝⁵ : AddCommMonoid Mₗ₁'
inst✝⁴ : AddCommMonoid Mₗ₂'
inst✝³ : Module R Mₗ₁
inst✝² : Module R Mₗ₂
inst✝¹ : Module R Mₗ₁'
inst✝ : Module R Mₗ₂'
B : Mₗ₁ →ₗ[R] Mₗ₂ →ₗ[R] M
e₁ : Mₗ₁ ≃ₗ[R] Mₗ₁'
e₂ : Mₗ₂ ≃ₗ[R] Mₗ₂'
h : B.SeparatingLeft
x : Mₗ₁'
hx : ∀ (y : Mₗ₂'), (((e₁.arrowCongr (e₂.arrowCongr (LinearEquiv.refl R M))) B) x) y = 0
⊢ e₁.symm x = 0
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✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : CommSemiring R₁
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R₁ M₁
inst✝² : CommSemiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M
⊢ B.SeparatingRight ↔ B.SeparatingRight

Tactic:
]

Goal state after: