-- 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:
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 = span L ↑M'
hv₃ : LinearIndependent L Subtype.val
⊢ ∃ n b b', ∀ (i : Fin n), b i = ↑(b' i)

Tactic:
rw [hM] at hv₂

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

Proof state:
case h
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
x✝ : { x // x ∈ v }
⊢ ↑x✝ = (⇑M'.subtype ∘ v') x✝

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

Tactic:
let e := (Module.Finite.finite_basis b).equivFin

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

Tactic:
classical
have : IsReflexive L M := p.reflexive_left
have : IsReflexive L N := p.reflexive_right
obtain ⟨v, hv₁, hv₂, hv₃⟩ := exists_linearIndependent L (M' : Set M)
rw [hM] at hv₂
let b : Basis _ L M := Basis.mk hv₃ <| by rw [← hv₂, Subtype.range_coe_subtype, Set.setOf_mem_eq]
have : Fintype v := Set.Finite.fintype <| Module.Finite.finite_basis b
set v' : v → M' := fun i ↦ ⟨i, hv₁ (Subtype.coe_prop i)⟩
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
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']⟩
suffices span K v = M' by
  apply Submodule.map_injective_of_injective M'.injective_subtype
  rw [Submodule.map_span, ← Set.image_univ, Set.image_image]
  simpa [v']
refine le_antisymm (Submodule.span_le.mpr hv₁) fun m hm ↦ ?_
obtain ⟨w, hw₁, hw₂, hw₃⟩ := exists_linearIndependent L (N' : Set N)
rw [hN] at hw₂
let bN : Basis _ L N := Basis.mk hw₃ <| by rw [← hw₂, Subtype.range_coe_subtype, Set.setOf_mem_eq]
have : Fintype w := Set.Finite.fintype <| Module.Finite.finite_basis bN
have e : v ≃ w := Fintype.equivOfCardEq <| by rw [← Module.finrank_eq_card_basis b,
  ← Module.finrank_eq_card_basis bN, p.finrank_eq]
let bM := bN.dualBasis.map p.toDualLeft.symm
have hbM (j : w) (x : M) (hx : x ∈ M') : bM.repr x j = p x (j : N) := by simp [bM, bN]
have hj (j : w) : bM.repr m j ∈ (algebraMap K L).range := (hbM _ _ hm) ▸ hp m hm j (hw₁ j.2)
replace hp (i : w) (j : v) :
    (bN.dualBasis.map p.toDualLeft.symm).toMatrix b i j ∈ (algebraMap K L).fieldRange := by
  simp only [Basis.toMatrix, Basis.map_repr, LinearEquiv.symm_symm, LinearEquiv.trans_apply,
    toDualLeft_apply, Basis.dualBasis_repr]
  exact hp (b j) (by simpa [b] using hv₁ j.2) (bN i) (by simpa [bN] using hw₁ i.2)
have hA (i j) : b.toMatrix bM i j ∈ (algebraMap K L).range :=
  Matrix.mem_subfield_of_mul_eq_one_of_mem_subfield_left e _ (by simp [bM]) hp i j
have h_span : span K v = span K (Set.range b) := by simp [b]
rw [h_span, Basis.mem_span_iff_repr_mem, ← Basis.toMatrix_mulVec_repr bM b m]
exact fun i ↦ Subring.sum_mem _ fun j _ ↦ Subring.mul_mem _ (hA i j) (hj j)

Result:
no goals