-- Lean 4 proof step from Mathlib.LinearAlgebra.PerfectPairing.Restrict (goal)
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : Module L M
inst_6 : Module L N
inst_7 : Module K M
inst_8 : Module K N
inst_9 : IsScalarTower K L M
p : M →ₗ[L] N →ₗ[L] L
inst_10 : p.IsPerfPair
M' : Submodule K M
N' : Submodule K N
hM : Eq (α := Submodule L M) (span L (↑M' : Set M)) ⊤
hN : Eq (α := Submodule L N) (span L (↑N' : Set N)) ⊤
hp :
  ∀ x ∈ M',
    ∀ y ∈ N',
      Membership.mem.{u_2, u_2} (α := L) (γ := Subring L) (RingHom.range.{u_1, u_2} (R := K) (algebraMap K L))
        ((((p : (a : M) → N →ₗ[L] L) x : N →ₗ[L] L) : (a : N) → L) y : L)
have have₁ have₂ :
  ∀ (this : IsReflexive L M),
    ∃ (n : ℕ) (b : Basis (Fin n) L M) (b' : Basis.{0, u_1, u_3} (Fin n) K ↥M'),
      ∀ (i : Fin n), Eq.{u_3 + 1} (α := M) ((b : (a : Fin n) → M) i : M) ((↑((b' : (a : Fin n) → ↥M') i) : M) : M)
⊢ ∃ (n : ℕ) (b : Basis (Fin n) L M) (b' : Basis.{0, u_1, u_3} (Fin n) K ↥M'),
    ∀ (i : Fin n), Eq.{u_3 + 1} (α := M) ((b : (a : Fin n) → M) i : M) ((↑((b' : (a : Fin n) → ↥M') i) : M) : M)
have have₃ : ∀ (this : IsReflexive L M) (this : IsReflexive L N),
  ∃ (n : ℕ) (b : Basis (Fin n) L M) (b' : Basis.{0, u_1, u_3} (Fin n) K ↥M'),
    ∀ (i : Fin n), Eq.{u_3 + 1} (α := M) ((b : (a : Fin n) → M) i : M) ((↑((b' : (a : Fin n) → ↥M') i) : M) : M)
Tactic: classical
  have : IsReflexive L M := .of_isPerfPair p
  have : IsReflexive L N := .of_isPerfPair p.flip
  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, Module.finrank_of_isPerfPair p]
  let bM := bN.dualBasis.map p.toPerfPair.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.toPerfPair.symm).toMatrix b i j ∈ (algebraMap K L).fieldRange := by
    simp only [Basis.toMatrix, Basis.map_repr, LinearEquiv.symm_symm, LinearEquiv.trans_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)