-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.BaseChange (goal)
Goal:
ι : Type u_1
ι' : Type u_2
inst : Finite ι'
K : Type u_3
L : Type u_4
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
v : ι → ι' → K
hv : LinearIndependent K v
let let₁ let₂ let₃ let₄ let₅ let₆ :
  LinearIndependent L (M := ι' → L) fun (i : ι) ↦ (⇑(algebraMap K L) : (a : K) → L) ∘ v i
let₇ :
  let this := Fintype.ofFinite ι';
  let I := ⋯.extend (K := K) (V := ι' → K) (v := id) (s := range v) (t := univ) ⋯;
  let b : Module.Basis (↑I : Type (max u_2 u_3)) K (ι' → K) := Module.Basis.extend (s := range v) ⋯;
  let b' : Module.Basis (↑I : Type (max u_2 u_3)) L (ι' → L) :=
    Module.Basis.map (M := L ⊗[K] (ι' → K)) (Module.Basis.baseChange L b) (piScalarRight K L L ι');
  let v' : (i : ι) → (↑I : Type (max u_2 u_3)) := fun (i : ι) ↦ Subtype.mk (p := fun (x : ι' → K) ↦ x ∈ I) (v i) ⋯;
  ∀
    (hv' :
      Eq (α := ι → ι' → L) ((⇑b' : (a : (↑I : Type (max u_2 u_3))) → ι' → L) ∘ v') fun (i : ι) ↦
        (⇑(algebraMap K L) : (a : K) → L) ∘ v i),
    LinearIndependent L (M := ι' → L) fun (i : ι) ↦ (⇑(algebraMap K L) : (a : K) → L) ∘ v i
let₈ :
  let this := Fintype.ofFinite ι';
  let I := ⋯.extend (K := K) (V := ι' → K) (v := id) (s := range v) (t := univ) ⋯;
  let b : Module.Basis (↑I : Type (max u_2 u_3)) K (ι' → K) := Module.Basis.extend (s := range v) ⋯;
  let b' : Module.Basis (↑I : Type (max u_2 u_3)) L (ι' → L) :=
    Module.Basis.map (M := L ⊗[K] (ι' → K)) (Module.Basis.baseChange L b) (piScalarRight K L L ι');
  let v' : (i : ι) → (↑I : Type (max u_2 u_3)) := fun (i : ι) ↦ Subtype.mk (p := fun (x : ι' → K) ↦ x ∈ I) (v i) ⋯;
  ∀
    (hv' :
      Eq (α := ι → ι' → L) ((⇑b' : (a : (↑I : Type (max u_2 u_3))) → ι' → L) ∘ v') fun (i : ι) ↦
        (⇑(algebraMap K L) : (a : K) → L) ∘ v i)
    (h_inj : Injective v'), LinearIndependent L (M := ι' → L) fun (i : ι) ↦ (⇑(algebraMap K L) : (a : K) → L) ∘ v i
⊢ LinearIndependent L (M := ι' → L) fun (i : ι) ↦ (⇑(algebraMap K L) : (a : K) → L) ∘ v i
have let₉ : let this := Fintype.ofFinite ι';
let I := sorry.extend (K := K) (V := ι' → K) (v := id) (s := range v) (t := univ) sorry;
let b : Module.Basis (↑I : Type (max u_2 u_3)) K (ι' → K) := Module.Basis.extend (s := range v) sorry;
let b' : Module.Basis (↑I : Type (max u_2 u_3)) L (ι' → L) :=
  Module.Basis.map (M := L ⊗[K] (ι' → K)) (Module.Basis.baseChange L b) (piScalarRight K L L ι');
let v' : (i : ι) → (↑I : Type (max u_2 u_3)) := fun (i : ι) ↦ Subtype.mk (p := fun (x : ι' → K) ↦ x ∈ I) (v i) sorry;
∀
  (hv' :
    Eq (α := ι → ι' → L) ((⇑b' : (a : (↑I : Type (max u_2 u_3))) → ι' → L) ∘ v') fun (i : ι) ↦
      (⇑(algebraMap K L) : (a : K) → L) ∘ v i)
  (h_inj : Injective v'), LinearIndependent L (M := ι' → L) ((⇑b' : (a : (↑I : Type (max u_2 u_3))) → ι' → L) ∘ v')
Tactic: classical
  let : Fintype ι' := .ofFinite ι'
  let I : Set (ι' → K) := hv.linearIndepOn_id.extend (subset_univ _)
  let b : Module.Basis I K (ι' → K) := .extend hv.linearIndepOn_id
  let b' : Module.Basis I L (ι' → L) := (b.baseChange L).map (TensorProduct.piScalarRight K L L ι')
  let v' (i : ι) : I := ⟨v i, hv.linearIndepOn_id.subset_extend _ <| mem_range_self i⟩
  have hv' : b' ∘ v' = fun i ↦ algebraMap K L ∘ v i := by
    ext; simp [b', b, v', Module.Basis.extend, Algebra.algebraMap_eq_smul_one]
  have h_inj : Injective v' := fun i j hij ↦ by have : Injective v := hv.injective; aesop
  rw [← hv']
  exact b'.linearIndependent.comp _ h_inj