-- Mathlib/LinearAlgebra/PerfectPairing/Restrict.lean
/-- If a perfect pairing over a field `L` takes values in a subfield `K` along two `K`-subspaces
whose `L` span is full, then these subspaces induce a `K`-structure in the sense of
[*Algebra I*, Bourbaki : Chapter II, §8.1 Definition 1][bourbaki1989]. -/
lemma exists_basis_basis_of_span_eq_top_of_mem_algebraMap
    (M' : Submodule K M) (N' : Submodule K N)
    (hM : span L (M' : Set M) = ⊤)
    (hN : span L (N' : Set N) = ⊤)
    (hp : ∀ᵉ (x ∈ M') (y ∈ N'), p x y ∈ (algebraMap K L).range) :
    ∃ (n : ℕ) (b : Basis (Fin n) L M) (b' : Basis (Fin n) K M'), ∀ i, b i = b' i

Proof state:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra K L
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module L M
inst✝³ : Module L N
inst✝² : Module K M
inst✝¹ : Module K N
inst✝ : IsScalarTower K L M
p : PerfectPairing L M N
M' : Submodule K M
N' : Submodule K N
hM : span L ↑M' = ⊤
hN : span L ↑N' = ⊤
hp : ∀ x ∈ M', ∀ y ∈ N', (p x) y ∈ (algebraMap K L).range
this✝¹ : IsReflexive L M
this✝ : IsReflexive L N
v : Set M
hv₁ : v ⊆ ↑M'
hv₂ : span L v = ⊤
hv₃✝ : LinearIndependent L Subtype.val
b : Basis { x // x ∈ v } L M := Basis.mk hv₃✝ ⋯
this : Fintype ↑v
v' : ↑v → ↥M' := fun i => ⟨↑i, ⋯⟩
hv₃ : LinearIndependent K Subtype.val
⊢ LinearIndependent (ι := ↑v) K v'

Tactic:
rw [show ((↑) : v → M) = M'.subtype ∘ v' by ext; simp [v']] at hv₃

Result:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra K L
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module L M
inst✝³ : Module L N
inst✝² : Module K M
inst✝¹ : Module K N
inst✝ : IsScalarTower K L M
p : PerfectPairing L M N
M' : Submodule K M
N' : Submodule K N
hM : span L ↑M' = ⊤
hN : span L ↑N' = ⊤
hp : ∀ x ∈ M', ∀ y ∈ N', (p x) y ∈ (algebraMap K L).range
this✝¹ : IsReflexive L M
this✝ : IsReflexive L N
v : Set M
hv₁ : v ⊆ ↑M'
hv₂ : span L v = ⊤
hv₃✝ : LinearIndependent L Subtype.val
b : Basis { x // x ∈ v } L M := Basis.mk hv₃✝ ⋯
this : Fintype ↑v
v' : ↑v → ↥M' := fun i => ⟨↑i, ⋯⟩
hv₃ : LinearIndependent K (⇑M'.subtype ∘ v')
⊢ LinearIndependent (ι := ↑v) K v'

Proof state:
case intro.intro.intro
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra K L
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module L M
inst✝³ : Module L N
inst✝² : Module K M
inst✝¹ : Module K N
inst✝ : IsScalarTower K L M
p : PerfectPairing L M N
M' : Submodule K M
N' : Submodule K N
hM : span L ↑M' = ⊤
hN : span L ↑N' = ⊤
hp : ∀ x ∈ M', ∀ y ∈ N', (p x) y ∈ (algebraMap K L).range
this✝¹ : IsReflexive L M
this✝ : IsReflexive L N
v : Set M
hv₁ : v ⊆ ↑M'
hv₂ : span L v = ⊤
hv₃ : LinearIndependent L Subtype.val
b : Basis { x // x ∈ v } L M := Basis.mk hv₃ ⋯
this : Fintype ↑v
v' : ↑v → ↥M' := fun i => ⟨↑i, ⋯⟩
⊢ ∃ n b b', ∀ (i : Fin n), b i = ↑(b' i)

Tactic:
have hv' : LinearIndependent K v' := by
  replace hv₃ := hv₃.restrict_scalars (R := K) <| by
    simp_rw [← Algebra.algebraMap_eq_smul_one]
    exact FaithfulSMul.algebraMap_injective K L
  rw [show ((↑) : v → M) = M'.subtype ∘ v' by ext; simp [v']] at hv₃
  exact hv₃.of_comp

Result:
case intro.intro.intro
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra K L
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module L M
inst✝³ : Module L N
inst✝² : Module K M
inst✝¹ : Module K N
inst✝ : IsScalarTower K L M
p : PerfectPairing L M N
M' : Submodule K M
N' : Submodule K N
hM : span L ↑M' = ⊤
hN : span L ↑N' = ⊤
hp : ∀ x ∈ M', ∀ y ∈ N', (p x) y ∈ (algebraMap K L).range
this✝¹ : IsReflexive L M
this✝ : IsReflexive L N
v : Set M
hv₁ : v ⊆ ↑M'
hv₂ : span L v = ⊤
hv₃ : LinearIndependent L Subtype.val
b : Basis { x // x ∈ v } L M := Basis.mk hv₃ ⋯
this : Fintype ↑v
v' : ↑v → ↥M' := fun i => ⟨↑i, ⋯⟩
hv' : LinearIndependent (ι := ↑v) K v'
⊢ ∃ n b b', ∀ (i : Fin n), b i = ↑(b' i)

Proof state:
case intro.intro.intro
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra K L
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module L M
inst✝³ : Module L N
inst✝² : Module K M
inst✝¹ : Module K N
inst✝ : IsScalarTower K L M
p : PerfectPairing L M N
M' : Submodule K M
N' : Submodule K N
hM : span L ↑M' = ⊤
hN : span L ↑N' = ⊤
hp : ∀ x ∈ M', ∀ y ∈ N', (p x) y ∈ (algebraMap K L).range
this✝¹ : IsReflexive L M
this✝ : IsReflexive L N
v : Set M
hv₁ : v ⊆ ↑M'
hv₂ : span L v = ⊤
hv₃ : LinearIndependent L Subtype.val
b : Basis { x // x ∈ v } L M := Basis.mk hv₃ ⋯
this : Fintype ↑v
v' : ↑v → ↥M' := fun i => ⟨↑i, ⋯⟩
hv' : LinearIndependent (ι := ↑v) K v'
m : M
hm : m ∈ M'
⊢ m ∈ span K v

Tactic:
obtain ⟨w, hw₁, hw₂, hw₃⟩ := exists_linearIndependent L (N' : Set N)

Result:
case intro.intro.intro.intro.intro.intro
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra K L
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module L M
inst✝³ : Module L N
inst✝² : Module K M
inst✝¹ : Module K N
inst✝ : IsScalarTower K L M
p : PerfectPairing L M N
M' : Submodule K M
N' : Submodule K N
hM : span L ↑M' = ⊤
hN : span L ↑N' = ⊤
hp : ∀ x ∈ M', ∀ y ∈ N', (p x) y ∈ (algebraMap K L).range
this✝¹ : IsReflexive L M
this✝ : IsReflexive L N
v : Set M
hv₁ : v ⊆ ↑M'
hv₂ : span L v = ⊤
hv₃ : LinearIndependent L Subtype.val
b : Basis { x // x ∈ v } L M := Basis.mk hv₃ ⋯
this : Fintype ↑v
v' : ↑v → ↥M' := fun i => ⟨↑i, ⋯⟩
hv' : LinearIndependent (ι := ↑v) K v'
m : M
hm : m ∈ M'
w : Set N
hw₁ : w ⊆ ↑N'
hw₂ : span L w = span L ↑N'
hw₃ : LinearIndependent L Subtype.val
⊢ m ∈ span K v

Proof state:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra K L
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module L M
inst✝³ : Module L N
inst✝² : Module K M
inst✝¹ : Module K N
inst✝ : IsScalarTower K L M
p : PerfectPairing L M N
M' : Submodule K M
N' : Submodule K N
hM : span L ↑M' = ⊤
hN : span L ↑N' = ⊤
hp : ∀ x ∈ M', ∀ y ∈ N', (p x) y ∈ (algebraMap K L).range
this✝¹ : IsReflexive L M
this✝ : IsReflexive L N
v : Set M
hv₁ : v ⊆ ↑M'
hv₂ : span L v = ⊤
hv₃✝ : LinearIndependent L Subtype.val
b : Basis { x // x ∈ v } L M := Basis.mk hv₃✝ ⋯
this : Fintype ↑v
v' : ↑v → ↥M' := fun i => ⟨↑i, ⋯⟩
hv₃ : LinearIndependent K (⇑M'.subtype ∘ v')
⊢ LinearIndependent (ι := ↑v) K v'

Tactic:
exact hv₃.of_comp

Result:
no goals