-- Mathlib/LinearAlgebra/BilinearForm/DualLattice.lean
lemma dualSubmodule_span_of_basis {ι} [Finite ι] [DecidableEq ι]
    (hB : B.Nondegenerate) (b : Basis ι S M) :
    B.dualSubmodule (Submodule.span R (Set.range b)) =
      Submodule.span R (Set.range <| B.dualBasis hB b)

Proof state:
case intro.a.intro.intro
R : Type u_4
S : Type u_2
M : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Field S
inst✝⁶ : AddCommGroup M
inst✝⁵ : Algebra R S
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
hB : B.Nondegenerate
b : Basis ι S M
val✝ : Fintype ι
i : ι
f : ι → R
hy : ∑ i : ι, f i • b i ∈ Submodule.span R (Set.range ⇑b)
⊢ (B ((B.dualBasis hB b) i)) (∑ i : ι, f i • b i) ∈ 1

Tactic:
simp only [map_sum, map_smul]

Result:
case intro.a.intro.intro
R : Type u_4
S : Type u_2
M : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Field S
inst✝⁶ : AddCommGroup M
inst✝⁵ : Algebra R S
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
hB : B.Nondegenerate
b : Basis ι S M
val✝ : Fintype ι
i : ι
f : ι → R
hy : ∑ i : ι, f i • b i ∈ Submodule.span R (Set.range ⇑b)
⊢ ∑ x : ι, (B ((B.dualBasis hB b) i)) (f x • b x) ∈ 1

Proof state:
case intro.a.h
R : Type u_4
S : Type u_2
M : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Field S
inst✝⁶ : AddCommGroup M
inst✝⁵ : Algebra R S
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
hB : B.Nondegenerate
b : Basis ι S M
val✝ : Fintype ι
x : M
hx : x ∈ B.dualSubmodule (Submodule.span R (Set.range ⇑b))
⊢ ∀ c ∈ Finset.univ,
    ((B.dualBasis hB b).repr x) c • (B.dualBasis hB b) c ∈ Submodule.span R (Set.range ⇑(B.dualBasis hB b))

Tactic:
rintro i -

Result:
case intro.a.h
R : Type u_4
S : Type u_2
M : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Field S
inst✝⁶ : AddCommGroup M
inst✝⁵ : Algebra R S
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
hB : B.Nondegenerate
b : Basis ι S M
val✝ : Fintype ι
x : M
hx : x ∈ B.dualSubmodule (Submodule.span R (Set.range ⇑b))
i : ι
⊢ ((B.dualBasis hB b).repr x) i • (B.dualBasis hB b) i ∈ Submodule.span R (Set.range ⇑(B.dualBasis hB b))

Proof state:
case intro.a
R : Type u_4
S : Type u_2
M : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Field S
inst✝⁶ : AddCommGroup M
inst✝⁵ : Algebra R S
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
hB : B.Nondegenerate
b : Basis ι S M
val✝ : Fintype ι
x : M
hx : x ∈ B.dualSubmodule (Submodule.span R (Set.range ⇑b))
⊢ ∑ i : ι, ((B.dualBasis hB b).repr x) i • (B.dualBasis hB b) i ∈ Submodule.span R (Set.range ⇑(B.dualBasis hB b))

Tactic:
apply sum_mem

Result:
case intro.a.h
R : Type u_4
S : Type u_2
M : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Field S
inst✝⁶ : AddCommGroup M
inst✝⁵ : Algebra R S
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
hB : B.Nondegenerate
b : Basis ι S M
val✝ : Fintype ι
x : M
hx : x ∈ B.dualSubmodule (Submodule.span R (Set.range ⇑b))
⊢ ∀ c ∈ Finset.univ,
    ((B.dualBasis hB b).repr x) c • (B.dualBasis hB b) c ∈ Submodule.span R (Set.range ⇑(B.dualBasis hB b))

Proof state:
case intro.a.intro.intro.h
R : Type u_4
S : Type u_2
M : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Field S
inst✝⁶ : AddCommGroup M
inst✝⁵ : Algebra R S
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
hB : B.Nondegenerate
b : Basis ι S M
val✝ : Fintype ι
i : ι
f : ι → R
hy : ∑ i : ι, f i • b i ∈ Submodule.span R (Set.range ⇑b)
⊢ ∀ c ∈ Finset.univ, (B ((B.dualBasis hB b) i)) (f c • b c) ∈ 1

Tactic:
rintro j -

Result:
case intro.a.intro.intro.h
R : Type u_4
S : Type u_2
M : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Field S
inst✝⁶ : AddCommGroup M
inst✝⁵ : Algebra R S
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
hB : B.Nondegenerate
b : Basis ι S M
val✝ : Fintype ι
i : ι
f : ι → R
hy : ∑ i : ι, f i • b i ∈ Submodule.span R (Set.range ⇑b)
j : ι
⊢ (B ((B.dualBasis hB b) i)) (f j • b j) ∈ 1

Proof state:
case intro.a.intro.intro
R : Type u_4
S : Type u_2
M : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Field S
inst✝⁶ : AddCommGroup M
inst✝⁵ : Algebra R S
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
hB : B.Nondegenerate
b : Basis ι S M
val✝ : Fintype ι
i : ι
f : ι → R
hy : ∑ i : ι, f i • b i ∈ Submodule.span R (Set.range ⇑b)
⊢ ∑ x : ι, (B ((B.dualBasis hB b) i)) (f x • b x) ∈ 1

Tactic:
apply sum_mem

Result:
case intro.a.intro.intro.h
R : Type u_4
S : Type u_2
M : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Field S
inst✝⁶ : AddCommGroup M
inst✝⁵ : Algebra R S
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
hB : B.Nondegenerate
b : Basis ι S M
val✝ : Fintype ι
i : ι
f : ι → R
hy : ∑ i : ι, f i • b i ∈ Submodule.span R (Set.range ⇑b)
⊢ ∀ c ∈ Finset.univ, (B ((B.dualBasis hB b) i)) (f c • b c) ∈ 1

Proof state:
case intro.a
R : Type u_4
S : Type u_2
M : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Field S
inst✝⁶ : AddCommGroup M
inst✝⁵ : Algebra R S
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
hB : B.Nondegenerate
b : Basis ι S M
val✝ : Fintype ι
x : M
hx : x ∈ B.dualSubmodule (Submodule.span R (Set.range ⇑b))
⊢ x ∈ Submodule.span R (Set.range ⇑(B.dualBasis hB b))

Tactic:
rw [← (B.dualBasis hB b).sum_repr x]

Result:
case intro.a
R : Type u_4
S : Type u_2
M : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Field S
inst✝⁶ : AddCommGroup M
inst✝⁵ : Algebra R S
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
hB : B.Nondegenerate
b : Basis ι S M
val✝ : Fintype ι
x : M
hx : x ∈ B.dualSubmodule (Submodule.span R (Set.range ⇑b))
⊢ ∑ i : ι, ((B.dualBasis hB b).repr x) i • (B.dualBasis hB b) i ∈ Submodule.span R (Set.range ⇑(B.dualBasis hB b))

Proof state:
case intro.a
R : Type u_4
S : Type u_2
M : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Field S
inst✝⁶ : AddCommGroup M
inst✝⁵ : Algebra R S
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
hB : B.Nondegenerate
b : Basis ι S M
val✝ : Fintype ι
⊢ Submodule.span R (Set.range ⇑(B.dualBasis hB b)) ≤ B.dualSubmodule (Submodule.span R (Set.range ⇑b))

Tactic:
rw [Submodule.span_le]

Result:
case intro.a
R : Type u_4
S : Type u_2
M : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Field S
inst✝⁶ : AddCommGroup M
inst✝⁵ : Algebra R S
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
hB : B.Nondegenerate
b : Basis ι S M
val✝ : Fintype ι
⊢ Set.range ⇑(B.dualBasis hB b) ⊆ ↑(B.dualSubmodule (Submodule.span R (Set.range ⇑b)))