-- 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 (ι := ↑v) K v'
m : M
hm : m ∈ M'
w : Set N
hw₁ : w ⊆ ↑N'
hw₂ : span L w = ⊤
hw₃ : LinearIndependent L Subtype.val
bN : Basis { x // x ∈ w } L N := Basis.mk hw₃ ⋯
this : Fintype ↑w
e : ↑v ≃ ↑w
bM : Basis { x // x ∈ w } L M := bN.dualBasis.map p.toDualLeft.symm
hbM : ∀ (j : ↑w), ∀ x ∈ M', (bM.repr x) j = (p x) ↑j
hj : ∀ (j : ↑w), (bM.repr m) j ∈ (algebraMap K L).range
i : ↑w
j : ↑v
⊢ bN i ∈ N'

Tactic:
simpa [bN] using hw₁ i.2

Result:
no goals

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 (ι := ↑v) K v'
this : span K (range v') = ⊤
e : { x // x ∈ v } ≃ Fin (Nat.card { x // x ∈ v }) := Finite.equivFin { x // x ∈ v }
⊢ ⊤ ≤ span K (range v')

Tactic:
rw [this]

Result:
no goals

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 (ι := ↑v) K v'
this : span K (range v') = ⊤
e : { x // x ∈ v } ≃ Fin (Nat.card { x // x ∈ v }) := Finite.equivFin { x // x ∈ v }
b' : Basis (↑v) K ↥M' := Basis.mk hv' ⋯
⊢ ∃ n b b', ∀ (i : Fin n), b i = ↑(b' i)

Tactic:
exact ⟨_, b.reindex e, b'.reindex e, fun i ↦ by simp [b, b', v']⟩

Result:
no goals

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' = ⊤
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 = ⊤
hw₃ : LinearIndependent L Subtype.val
bN : Basis { x // x ∈ w } L N := Basis.mk hw₃ ⋯
this : Fintype ↑w
e : ↑v ≃ ↑w
bM : Basis { x // x ∈ w } L M := bN.dualBasis.map p.toDualLeft.symm
hbM : ∀ (j : ↑w), ∀ x ∈ M', (bM.repr x) j = (p x) ↑j
hj : ∀ (j : ↑w), (bM.repr m) j ∈ (algebraMap K L).range
hp : ∀ (i : ↑w) (j : ↑v), (bN.dualBasis.map p.toDualLeft.symm).toMatrix (⇑b) i j ∈ (algebraMap K L).fieldRange
hA : ∀ (i : { x // x ∈ v }) (j : { x // x ∈ w }), b.toMatrix (⇑bM) i j ∈ (algebraMap K L).range
⊢ span K v = span K (range ⇑b)

Tactic:
simp [b]

Result:
no goals

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'
⊢ ∃ n b b', ∀ (i : Fin n), b i = ↑(b' i)

Tactic:
suffices span K (Set.range v') = ⊤ by
  let e := (Module.Finite.finite_basis b).equivFin
  let b' : Basis _ K M' := Basis.mk hv' (by rw [this])
  exact ⟨_, b.reindex e, b'.reindex e, fun i ↦ by simp [b, b', v']⟩

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'
⊢ span K (range 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' = ⊤
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 = ⊤
hw₃ : LinearIndependent L Subtype.val
bN : Basis { x // x ∈ w } L N := Basis.mk hw₃ ⋯
this : Fintype ↑w
e : ↑v ≃ ↑w
bM : Basis { x // x ∈ w } L M := bN.dualBasis.map p.toDualLeft.symm
hbM : ∀ (j : ↑w), ∀ x ∈ M', (bM.repr x) j = (p x) ↑j
hj : ∀ (j : ↑w), (bM.repr m) j ∈ (algebraMap K L).range
hp : ∀ (i : ↑w) (j : ↑v), (bN.dualBasis.map p.toDualLeft.symm).toMatrix (⇑b) i j ∈ (algebraMap K L).fieldRange
i : { x // x ∈ v }
j : { x // x ∈ w }
⊢ b.toMatrix ⇑bM * (bN.dualBasis.map p.toDualLeft.symm).toMatrix ⇑b = 1

Tactic:
simp [bM]

Result:
no goals