-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
ι : Type u_1
R : Type u_2
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
b : ι → M
inst_3 : IsPrincipalIdealRing R
inst_4 : IsDomain R
inst_5 : Fintype ι
s : ι → M
hs : Eq (α := Submodule R M) (span R (range s)) ⊤
inst_6 : IsTorsionFree R M
We We₁ We₂ We₃ :
  (this :
      ∃ (s_1 : Set ι),
        LinearIndepOn R s s_1 ∧
          ∀ i ∉ s_1, ∃ (a : R), a ≠ 0 ∧ Membership.mem (γ := Submodule R M) (span R (s '' s_1)) (a • s i)) →
    (n : ℕ) × Basis (Fin n) R M
We₄ We₅ We₆ We₇ :
  (this :
      ∃ (s_1 : Set ι),
        LinearIndepOn R s s_1 ∧
          ∀ i ∉ s_1, ∃ (a : R), a ≠ 0 ∧ Membership.mem (γ := Submodule R M) (span R (s '' s_1)) (a • s i)) →
    let I :=
      this.choose (p := fun (s_1 : Set ι) ↦
        LinearIndepOn R s s_1 ∧
          ∀ i ∉ s_1, ∃ (a : R), a ≠ 0 ∧ Membership.mem (γ := Submodule R M) (span R (s '' s_1)) (a • s i));
    (indepI : LinearIndependent (ι := (↑I : Type u_1)) R (s ∘ fun (x : (↑I : Type u_1)) ↦ (↑x : ι))) →
      (hI : ∀ i ∉ I, ∃ (a : R), a ≠ 0 ∧ Membership.mem (γ := Submodule R M) (span R (s '' I)) (a • s i)) →
        (n : ℕ) × Basis (Fin n) R M
We₈ :
  (this :
      ∃ (s_1 : Set ι),
        LinearIndepOn R s s_1 ∧
          ∀ i ∉ s_1, ∃ (a : R), a ≠ 0 ∧ Membership.mem (γ := Submodule R M) (span R (s '' s_1)) (a • s i)) →
    let I :=
      this.choose (p := fun (s_1 : Set ι) ↦
        LinearIndepOn R s s_1 ∧
          ∀ i ∉ s_1, ∃ (a : R), a ≠ 0 ∧ Membership.mem (γ := Submodule R M) (span R (s '' s_1)) (a • s i));
    (indepI : LinearIndependent (ι := (↑I : Type u_1)) R (s ∘ fun (x : (↑I : Type u_1)) ↦ (↑x : ι))) →
      (hI : ∀ i ∉ I, ∃ (a : R), a ≠ 0 ∧ Membership.mem (γ := Submodule R M) (span R (s '' I)) (a • s i)) →
        let N : Submodule R M := span R (range (ι := (↑I : Type u_1)) (s ∘ fun (x : (↑I : Type u_1)) ↦ (↑x : ι)));
        (exists_a : ∀ (i : ι), ∃ (a : R), a ≠ 0 ∧ a • s i ∈ N) → (n : ℕ) × Basis (Fin n) R M
We₉ We₁₀ :
  (this :
      ∃ (s_1 : Set ι),
        LinearIndepOn R s s_1 ∧
          ∀ i ∉ s_1, ∃ (a : R), a ≠ 0 ∧ Membership.mem (γ := Submodule R M) (span R (s '' s_1)) (a • s i)) →
    let I :=
      this.choose (p := fun (s_1 : Set ι) ↦
        LinearIndepOn R s s_1 ∧
          ∀ i ∉ s_1, ∃ (a : R), a ≠ 0 ∧ Membership.mem (γ := Submodule R M) (span R (s '' s_1)) (a • s i));
    (indepI : LinearIndependent (ι := (↑I : Type u_1)) R (s ∘ fun (x : (↑I : Type u_1)) ↦ (↑x : ι))) →
      (hI : ∀ i ∉ I, ∃ (a : R), a ≠ 0 ∧ Membership.mem (γ := Submodule R M) (span R (s '' I)) (a • s i)) →
        let N : Submodule R M := span R (range (ι := (↑I : Type u_1)) (s ∘ fun (x : (↑I : Type u_1)) ↦ (↑x : ι)));
        (a : (i : ι) → R) → (ha : ∀ (i : ι), a i ≠ 0) → (ha' : ∀ (i : ι), a i • s i ∈ N) → (n : ℕ) × Basis (Fin n) R M
We₁₁ We₁₂ :
  (this :
      ∃ (s_1 : Set ι),
        LinearIndepOn R s s_1 ∧
          ∀ i ∉ s_1, ∃ (a : R), a ≠ 0 ∧ Membership.mem (γ := Submodule R M) (span R (s '' s_1)) (a • s i)) →
    let I :=
      this.choose (p := fun (s_1 : Set ι) ↦
        LinearIndepOn R s s_1 ∧
          ∀ i ∉ s_1, ∃ (a : R), a ≠ 0 ∧ Membership.mem (γ := Submodule R M) (span R (s '' s_1)) (a • s i));
    (indepI : LinearIndependent (ι := (↑I : Type u_1)) R (s ∘ fun (x : (↑I : Type u_1)) ↦ (↑x : ι))) →
      (hI : ∀ i ∉ I, ∃ (a : R), a ≠ 0 ∧ Membership.mem (γ := Submodule R M) (span R (s '' I)) (a • s i)) →
        let N : Submodule R M := span R (range (ι := (↑I : Type u_1)) (s ∘ fun (x : (↑I : Type u_1)) ↦ (↑x : ι)));
        (a : (i : ι) → R) →
          (ha : ∀ (i : ι), a i ≠ 0) →
            (ha' : ∀ (i : ι), a i • s i ∈ N) →
              let A : R := ∏ i : ι, a i;
              (hA : A ≠ 0) → (n : ℕ) × Basis (Fin n) R M
We₁₃ We₁₄ :
  (this :
      ∃ (s_1 : Set ι),
        LinearIndepOn R s s_1 ∧
          ∀ i ∉ s_1, ∃ (a : R), a ≠ 0 ∧ Membership.mem (γ := Submodule R M) (span R (s '' s_1)) (a • s i)) →
    let I :=
      this.choose (p := fun (s_1 : Set ι) ↦
        LinearIndepOn R s s_1 ∧
          ∀ i ∉ s_1, ∃ (a : R), a ≠ 0 ∧ Membership.mem (γ := Submodule R M) (span R (s '' s_1)) (a • s i));
    (indepI : LinearIndependent (ι := (↑I : Type u_1)) R (s ∘ fun (x : (↑I : Type u_1)) ↦ (↑x : ι))) →
      (hI : ∀ i ∉ I, ∃ (a : R), a ≠ 0 ∧ Membership.mem (γ := Submodule R M) (span R (s '' I)) (a • s i)) →
        let N : Submodule R M := span R (range (ι := (↑I : Type u_1)) (s ∘ fun (x : (↑I : Type u_1)) ↦ (↑x : ι)));
        (a : (i : ι) → R) →
          (ha : ∀ (i : ι), a i ≠ 0) →
            (ha' : ∀ (i : ι), a i • s i ∈ N) →
              let A : R := ∏ i : ι, a i;
              (hA : A ≠ 0) →
                let φ : M →ₗ[R] M := (LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) A;
                (this : φ.ker = ⊥) → (n : ℕ) × Basis (Fin n) R M
We₁₅ :
  (this :
      ∃ (s_1 : Set ι),
        LinearIndepOn R s s_1 ∧
          ∀ i ∉ s_1, ∃ (a : R), a ≠ 0 ∧ Membership.mem (γ := Submodule R M) (span R (s '' s_1)) (a • s i)) →
    let I :=
      this.choose (p := fun (s_1 : Set ι) ↦
        LinearIndepOn R s s_1 ∧
          ∀ i ∉ s_1, ∃ (a : R), a ≠ 0 ∧ Membership.mem (γ := Submodule R M) (span R (s '' s_1)) (a • s i));
    (indepI : LinearIndependent (ι := (↑I : Type u_1)) R (s ∘ fun (x : (↑I : Type u_1)) ↦ (↑x : ι))) →
      (hI : ∀ i ∉ I, ∃ (a : R), a ≠ 0 ∧ Membership.mem (γ := Submodule R M) (span R (s '' I)) (a • s i)) →
        let N : Submodule R M := span R (range (ι := (↑I : Type u_1)) (s ∘ fun (x : (↑I : Type u_1)) ↦ (↑x : ι)));
        (a : (i : ι) → R) →
          (ha : ∀ (i : ι), a i ≠ 0) →
            (ha' : ∀ (i : ι), a i • s i ∈ N) →
              let A : R := ∏ i : ι, a i;
              (hA : A ≠ 0) →
                let φ : M →ₗ[R] M := (LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) A;
                (this : φ.ker = ⊥) → (this : φ.range ≤ N) → (n : ℕ) × Basis (Fin n) R M
We₁₆ :
  (this :
      ∃ (s_1 : Set ι),
        LinearIndepOn R s s_1 ∧
          ∀ i ∉ s_1, ∃ (a : R), a ≠ 0 ∧ Membership.mem (γ := Submodule R M) (span R (s '' s_1)) (a • s i)) →
    let I :=
      this.choose (p := fun (s_1 : Set ι) ↦
        LinearIndepOn R s s_1 ∧
          ∀ i ∉ s_1, ∃ (a : R), a ≠ 0 ∧ Membership.mem (γ := Submodule R M) (span R (s '' s_1)) (a • s i));
    (indepI : LinearIndependent (ι := (↑I : Type u_1)) R (s ∘ fun (x : (↑I : Type u_1)) ↦ (↑x : ι))) →
      (hI : ∀ i ∉ I, ∃ (a : R), a ≠ 0 ∧ Membership.mem (γ := Submodule R M) (span R (s '' I)) (a • s i)) →
        let N : Submodule R M := span R (range (ι := (↑I : Type u_1)) (s ∘ fun (x : (↑I : Type u_1)) ↦ (↑x : ι)));
        (a : (i : ι) → R) →
          (ha : ∀ (i : ι), a i ≠ 0) →
            (ha' : ∀ (i : ι), a i • s i ∈ N) →
              let A : R := ∏ i : ι, a i;
              (hA : A ≠ 0) →
                let φ : M →ₗ[R] M := (LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) A;
                (this : φ.ker = ⊥) →
                  (this : φ.range ≤ N) →
                    (n : ℕ) → (b : Basis.{0, u_2, u_3} (Fin n) R ↥φ.range) → (n : ℕ) × Basis (Fin n) R M
⊢ (n : ℕ) × Basis (Fin n) R M

Tactic:
classical
    -- We define `N` as the submodule spanned by a maximal linear independent subfamily of `s`
    have := exists_maximal_linearIndepOn R s
    let I : Set ι := this.choose
    obtain
      ⟨indepI : LinearIndependent R (s ∘ (fun x => x) : I → M), hI :
        ∀ i ∉ I, ∃ a : R, a ≠ 0 ∧ a • s i ∈ span R (s '' I)⟩ :=
      this.choose_spec
    let N := span R (range <| (s ∘ (fun x => x) : I → M))
    -- same as `span R (s '' I)` but more convenient
    let _sI : I → N := fun i ↦ ⟨s i.1, subset_span (mem_range_self i)⟩
    -- `s` restricted to `I` is a basis of `N`
    let sI_basis : Basis I R N := Basis.span indepI
    -- Our first goal is to build `A ≠ 0` such that `A • M ⊆ N`
    have exists_a : ∀ i : ι, ∃ a : R, a ≠ 0 ∧ a • s i ∈ N := by
      intro i
      by_cases hi : i ∈ I
      · use 1, zero_ne_one.symm
        rw [one_smul]
        exact subset_span (mem_range_self (⟨i, hi⟩ : I))
      · simpa [image_eq_range s I] using hI i hi
    choose a ha ha' using exists_a
    let A := ∏ i, a i
    have hA : A ≠ 0 := by
      rw [Finset.prod_ne_zero_iff]
      simpa using ha
    -- `M ≃ A • M` because `M` is torsion free and `A ≠ 0`
    let φ : M →ₗ[R] M := LinearMap.lsmul R M A
    have : LinearMap.ker φ = ⊥ := LinearMap.ker_lsmul hA
    let ψ := LinearEquiv.ofInjective φ (LinearMap.ker_eq_bot.mp this)
    have : LinearMap.range φ ≤ N := by
      -- as announced, `A • M ⊆ N`
      suffices ∀ i, φ (s i) ∈ N by
        rw [LinearMap.range_eq_map, ← hs, map_span_le]
        rintro _ ⟨i, rfl⟩
        apply this
      intro i
      calc
        (∏ j ∈ {i}ᶜ, a j) • a i • s i ∈ N := N.smul_mem _ (ha' i)
        _ = (∏ j, a j) • s i := by rw [Fintype.prod_eq_prod_compl_mul i, mul_smul]
    -- Since a submodule of a free `R`-module is free, we get that `A • M` is free
    obtain ⟨n, b : Basis (Fin n) R (LinearMap.range φ)⟩ := Submodule.basisOfPidOfLE this sI_basis
    -- hence `M` is free.
    exact ⟨n, b.map ψ.symm⟩