awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.PID (goal)
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
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)
I : Set ι :=
  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 : Submodule R M := span R (range (ι := (↑I : Type u_1)) (s ∘ fun (x : (↑I : Type u_1)) ↦ (↑x : ι)))
_sI : (↑I : Type u_1) → ↥N := fun (i : (↑I : Type u_1)) ↦ Subtype.mk (p := fun (x : M) ↦ x ∈ N) (s (↑i : ι)) ⋯
sI_basis : Basis.{u_1, u_2, u_3} (↑I : Type u_1) R ↥N := Basis.span indepI
i : ι
hi : i ∈ I
⊢ ∃ (a : R), a ≠ 0 ∧ a • s i ∈ N
have right : HSMul.hSMul.{u_2, u_3, u_3} (α := R) 1 (s i) ∈ N
Tactic: use 1, zero_ne_one.symm
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.PID (goal)
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
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)
I : Set ι :=
  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 : Submodule R M := span R (range (ι := (↑I : Type u_1)) (s ∘ fun (x : (↑I : Type u_1)) ↦ (↑x : ι)))
_sI : (↑I : Type u_1) → ↥N := fun (i : (↑I : Type u_1)) ↦ Subtype.mk (p := fun (x : M) ↦ x ∈ N) (s (↑i : ι)) ⋯
sI_basis : Basis.{u_1, u_2, u_3} (↑I : Type u_1) R ↥N := Basis.span indepI
i : ι
hi : i ∈ I
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := R) 1 (s i) ∈ N
have right : s i ∈ N
Tactic: rw [one_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.PID (hypothesis)
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
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)
I : Set ι :=
  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 : Submodule R M := span R (range (ι := (↑I : Type u_1)) (s ∘ fun (x : (↑I : Type u_1)) ↦ (↑x : ι)))
_sI : (↑I : Type u_1) → ↥N := fun (i : (↑I : Type u_1)) ↦ Subtype.mk (p := fun (x : M) ↦ x ∈ N) (s (↑i : ι)) ⋯
sI_basis : Basis.{u_1, u_2, u_3} (↑I : Type u_1) R ↥N := Basis.span indepI
⊢ (n : ℕ) × Basis (Fin n) R M
have exists_a : ∀ (i : ι), ∃ (a : R), a ≠ 0 ∧ a • s i ∈ N
Tactic: 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
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.PID (goal)
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
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)
I : Set ι :=
  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 : Submodule R M := span R (range (ι := (↑I : Type u_1)) (s ∘ fun (x : (↑I : Type u_1)) ↦ (↑x : ι)))
_sI : (↑I : Type u_1) → ↥N := fun (i : (↑I : Type u_1)) ↦ Subtype.mk (p := fun (x : M) ↦ x ∈ N) (s (↑i : ι)) ⋯
sI_basis : Basis.{u_1, u_2, u_3} (↑I : Type u_1) R ↥N := Basis.span indepI
exists_a : ∀ (i : ι), ∃ (a : R), a ≠ 0 ∧ a • s i ∈ N
⊢ (n : ℕ) × Basis (Fin n) R M
have choose : (a : (i : ι) → R) → (ha : ∀ (i : ι), a i ≠ 0) → (ha' : ∀ (i : ι), a i • s i ∈ N) → (n : ℕ) × Basis (Fin n) R M
Tactic: choose a ha ha' using exists_a
Cleared hypotheses: exists_a
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.PID (goal)
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
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)
I : Set ι :=
  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 : Submodule R M := span R (range (ι := (↑I : Type u_1)) (s ∘ fun (x : (↑I : Type u_1)) ↦ (↑x : ι)))
_sI : (↑I : Type u_1) → ↥N := fun (i : (↑I : Type u_1)) ↦ Subtype.mk (p := fun (x : M) ↦ x ∈ N) (s (↑i : ι)) ⋯
sI_basis : Basis.{u_1, u_2, u_3} (↑I : Type u_1) R ↥N := Basis.span indepI
a : (i : ι) → R
ha : ∀ (i : ι), a i ≠ 0
ha' : ∀ (i : ι), a i • s i ∈ N
A : R := ∏ i : ι, a i
⊢ A ≠ 0
have rw : ∀ (a_1 : ι), Membership.mem (γ := Finset ι) Finset.univ a_1 → a a_1 ≠ 0
Tactic: rw [Finset.prod_ne_zero_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.PID (hypothesis)
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
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)
I : Set ι :=
  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 : Submodule R M := span R (range (ι := (↑I : Type u_1)) (s ∘ fun (x : (↑I : Type u_1)) ↦ (↑x : ι)))
_sI : (↑I : Type u_1) → ↥N := fun (i : (↑I : Type u_1)) ↦ Subtype.mk (p := fun (x : M) ↦ x ∈ N) (s (↑i : ι)) ⋯
sI_basis : Basis.{u_1, u_2, u_3} (↑I : Type u_1) R ↥N := Basis.span indepI
a : (i : ι) → R
ha : ∀ (i : ι), a i ≠ 0
ha' : ∀ (i : ι), a i • s i ∈ N
A : R := ∏ i : ι, a i
⊢ (n : ℕ) × Basis (Fin n) R M
have hA : A ≠ 0
Tactic: have hA : A ≠ 0 := by
      rw [Finset.prod_ne_zero_iff]
      simpa using ha
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.PID (hypothesis)
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
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)
I : Set ι :=
  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 : Submodule R M := span R (range (ι := (↑I : Type u_1)) (s ∘ fun (x : (↑I : Type u_1)) ↦ (↑x : ι)))
_sI : (↑I : Type u_1) → ↥N := fun (i : (↑I : Type u_1)) ↦ Subtype.mk (p := fun (x : M) ↦ x ∈ N) (s (↑i : ι)) ⋯
sI_basis : Basis.{u_1, u_2, u_3} (↑I : Type u_1) R ↥N := Basis.span indepI
a : (i : ι) → R
ha : ∀ (i : ι), a i ≠ 0
ha' : ∀ (i : ι), a i • s i ∈ N
A : R := ∏ i : ι, a i
hA : A ≠ 0
φ : M →ₗ[R] M := (LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) A
⊢ (n : ℕ) × Basis (Fin n) R M
have this₁ : φ.ker = ⊥
Tactic: have : LinearMap.ker φ = ⊥ := LinearMap.ker_lsmul hA
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.PID (goal)
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
this_1 :
  ∃ (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)
I : Set ι :=
  this_1.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 : Submodule R M := span R (range (ι := (↑I : Type u_1)) (s ∘ fun (x : (↑I : Type u_1)) ↦ (↑x : ι)))
_sI : (↑I : Type u_1) → ↥N := fun (i : (↑I : Type u_1)) ↦ Subtype.mk (p := fun (x : M) ↦ x ∈ N) (s (↑i : ι)) ⋯
sI_basis : Basis.{u_1, u_2, u_3} (↑I : Type u_1) R ↥N := Basis.span indepI
a : (i : ι) → R
ha : ∀ (i : ι), a i ≠ 0
ha' : ∀ (i : ι), a i • s i ∈ N
A : R := ∏ i : ι, a i
hA : A ≠ 0
φ : M →ₗ[R] M := (LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) A
this_2 : φ.ker = ⊥
ψ : M ≃ₗ[R] ↥φ.range := LinearEquiv.ofInjective φ ⋯
this : ∀ (i : ι), Membership.mem (α := M) N ((φ : (a : M) → M) (s i) : M)
⊢ φ.range ≤ N
have rw : ∀ m ∈ range s, Membership.mem (α := M) N ((φ : (a : M) → M) m : M)
Tactic: rw [LinearMap.range_eq_map, ← hs, map_span_le]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.PID (goal)
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
this_1 :
  ∃ (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)
I : Set ι :=
  this_1.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 : Submodule R M := span R (range (ι := (↑I : Type u_1)) (s ∘ fun (x : (↑I : Type u_1)) ↦ (↑x : ι)))
_sI : (↑I : Type u_1) → ↥N := fun (i : (↑I : Type u_1)) ↦ Subtype.mk (p := fun (x : M) ↦ x ∈ N) (s (↑i : ι)) ⋯
sI_basis : Basis.{u_1, u_2, u_3} (↑I : Type u_1) R ↥N := Basis.span indepI
a : (i : ι) → R
ha : ∀ (i : ι), a i ≠ 0
ha' : ∀ (i : ι), a i • s i ∈ N
A : R := ∏ i : ι, a i
hA : A ≠ 0
φ : M →ₗ[R] M := (LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) A
this : φ.ker = ⊥
ψ : M ≃ₗ[R] ↥φ.range := LinearEquiv.ofInjective φ ⋯
⊢ φ.range ≤ N
have suffices : ∀ (i : ι), Membership.mem (α := M) N ((φ : (a : M) → M) (s i) : M)
Tactic: suffices ∀ i, φ (s i) ∈ N by
        rw [LinearMap.range_eq_map, ← hs, map_span_le]
        rintro _ ⟨i, rfl⟩
        apply this
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.PID (goal)
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
this_1 :
  ∃ (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)
I : Set ι :=
  this_1.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 : Submodule R M := span R (range (ι := (↑I : Type u_1)) (s ∘ fun (x : (↑I : Type u_1)) ↦ (↑x : ι)))
_sI : (↑I : Type u_1) → ↥N := fun (i : (↑I : Type u_1)) ↦ Subtype.mk (p := fun (x : M) ↦ x ∈ N) (s (↑i : ι)) ⋯
sI_basis : Basis.{u_1, u_2, u_3} (↑I : Type u_1) R ↥N := Basis.span indepI
a : (i : ι) → R
ha : ∀ (i : ι), a i ≠ 0
ha' : ∀ (i : ι), a i • s i ∈ N
A : R := ∏ i : ι, a i
hA : A ≠ 0
φ : M →ₗ[R] M := (LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) A
this : φ.ker = ⊥
ψ : M ≃ₗ[R] ↥φ.range := LinearEquiv.ofInjective φ ⋯
i : ι
⊢ Membership.mem (α := M) N ((φ : (a : M) → M) (s i) : M)
have j : HSMul.hSMul.{u_2, u_3, u_3} (α := R) (∏ j ∈ {i}ᶜ, a j) (a i • s i) =
  HSMul.hSMul.{u_2, u_3, u_3} (α := R) (∏ j : ι, a j) (s i)
Tactic: 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.PID (hypothesis)
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
this_1 :
  ∃ (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)
I : Set ι :=
  this_1.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 : Submodule R M := span R (range (ι := (↑I : Type u_1)) (s ∘ fun (x : (↑I : Type u_1)) ↦ (↑x : ι)))
_sI : (↑I : Type u_1) → ↥N := fun (i : (↑I : Type u_1)) ↦ Subtype.mk (p := fun (x : M) ↦ x ∈ N) (s (↑i : ι)) ⋯
sI_basis : Basis.{u_1, u_2, u_3} (↑I : Type u_1) R ↥N := Basis.span indepI
a : (i : ι) → R
ha : ∀ (i : ι), a i ≠ 0
ha' : ∀ (i : ι), a i • s i ∈ N
A : R := ∏ i : ι, a i
hA : A ≠ 0
φ : M →ₗ[R] M := (LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) A
this : φ.ker = ⊥
ψ : M ≃ₗ[R] ↥φ.range := LinearEquiv.ofInjective φ ⋯
⊢ (n : ℕ) × Basis (Fin n) R M
have this₁ : φ.range ≤ N
Tactic: 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.PID (goal)
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
this_1 :
  ∃ (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)
I : Set ι :=
  this_1.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 : Submodule R M := span R (range (ι := (↑I : Type u_1)) (s ∘ fun (x : (↑I : Type u_1)) ↦ (↑x : ι)))
_sI : (↑I : Type u_1) → ↥N := fun (i : (↑I : Type u_1)) ↦ Subtype.mk (p := fun (x : M) ↦ x ∈ N) (s (↑i : ι)) ⋯
sI_basis : Basis.{u_1, u_2, u_3} (↑I : Type u_1) R ↥N := Basis.span indepI
a : (i : ι) → R
ha : ∀ (i : ι), a i ≠ 0
ha' : ∀ (i : ι), a i • s i ∈ N
A : R := ∏ i : ι, a i
hA : A ≠ 0
φ : M →ₗ[R] M := (LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) A
this_2 : φ.ker = ⊥
ψ : M ≃ₗ[R] ↥φ.range := LinearEquiv.ofInjective φ ⋯
this : φ.range ≤ N
⊢ (n : ℕ) × Basis (Fin n) R M
have obtain : (n : ℕ) → (b : Basis.{0, u_2, u_3} (Fin n) R ↥φ.range) → (n : ℕ) × Basis (Fin n) R M
Tactic: obtain ⟨n, b : Basis (Fin n) R (LinearMap.range φ)⟩ := Submodule.basisOfPidOfLE this sI_basis
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.PID (goal)
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
⊢ (n : ℕ) × Basis (Fin n) R M
have 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
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⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.PID (goal)
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
⊢ (n : ℕ) × Basis (Fin n) R M
have 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
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⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.PID (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsPrincipalIdealRing R
inst_4 : IsDomain R
inst_5 : Finite ι
s : ι → M
hs : Eq (α := Submodule R M) (span R (range s)) ⊤
inst_6 : IsTorsionFree R M
⊢ Free R M
have intro : ∀ (val : Fintype ι), Free R M
Tactic: cases nonempty_fintype ι