awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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 : ι), ∃ (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
-- 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
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
choose : (a : (i : ι) → R) → (ha : ∀ (i : ι), a i ≠ 0) → (ha' : ∀ (i : ι), a i • s i ∈ N) → (n : ℕ) × Basis (Fin n) R M
⊢ (n : ℕ) × Basis (Fin n) R M

Tactic:
choose a ha ha' using exists_a
-- 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
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
rw : ∀ (a_1 : ι), Membership.mem (γ := Finset ι) Finset.univ a_1 → a a_1 ≠ 0
⊢ A ≠ 0

Tactic:
rw [Finset.prod_ne_zero_iff]

Premises used: Finset.prod_ne_zero_iff
-- 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
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_1 : ι), Membership.mem (γ := Finset ι) Finset.univ a_1 → a a_1 ≠ 0

Tactic:
simpa using ha
-- 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
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

Tactic:
have hA : A ≠ 0 := by
      rw [Finset.prod_ne_zero_iff]
      simpa using ha
-- 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
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
⊢ φ.ker = ⊥

Tactic:
have : LinearMap.ker φ = ⊥ := LinearMap.ker_lsmul hA
-- 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
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)
rw : ∀ m ∈ range s, Membership.mem (α := M) N ((φ : (a : M) → M) m : M)
⊢ φ.range ≤ N

Tactic:
rw [LinearMap.range_eq_map, ← hs, map_span_le]

Premises used: Submodule.map_span_le, LinearMap.range_eq_map
-- 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
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)
i : ι
⊢ Membership.mem (α := M) N ((φ : (a : M) → M) (s i) : M)

Tactic:
apply this
-- 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
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 φ ⋯
suffices : ∀ (i : ι), Membership.mem (α := M) N ((φ : (a : M) → M) (s i) : M)
⊢ φ.range ≤ N

Tactic:
suffices ∀ i, φ (s i) ∈ N by
        rw [LinearMap.range_eq_map, ← hs, map_span_le]
        rintro _ ⟨i, rfl⟩
        apply this
-- 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
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 : ι
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := R) (∏ j ∈ {i}ᶜ, a j) (a i • s i) ∈ N

Tactic:
N.smul_mem _ (ha' i)

Premises used: Set.Mem, Submodule.smul_mem
-- 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
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 : ι
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)
⊢ Membership.mem (α := M) N ((φ : (a : M) → M) (s i) : M)

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]

Premises used: Finset.univ, Compl.compl, Finset.prod, Singleton.singleton, Submodule.smul_mem
-- 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
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

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]
-- 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
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
obtain : (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:
obtain ⟨n, b : Basis (Fin n) R (LinearMap.range φ)⟩ := Submodule.basisOfPidOfLE this sI_basis

Premises used: Submodule.basisOfPidOfLE
-- 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_1 : ι → 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 : ℕ
b : Basis.{0, u_2, u_3} (Fin n) R ↥φ.range
⊢ (n : ℕ) × Basis (Fin n) R M

Tactic:
exact ⟨n, b.map ψ.symm⟩
-- 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
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
intro : ∀ (val : Fintype ι), Free R M
⊢ Free R M

Tactic:
cases nonempty_fintype ι

Premises used: nonempty_fintype
-- 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
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
val : Fintype ι
intro : ∀ (n : ℕ) (b : Basis (Fin n) R M), Free R M
⊢ Free R M

Tactic:
obtain ⟨n, b⟩ : Σ n, Basis (Fin n) R M := Module.basisOfFiniteTypeTorsionFree hs

Premises used: Module.basisOfFiniteTypeTorsionFree
-- 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
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
val : Fintype ι
n : ℕ
b : Basis (Fin n) R M
⊢ Free R M

Tactic:
Module.Free.of_basis b

Premises used: Module.Free.of_basis
-- 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
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
val : Fintype ι
n : ℕ
b : Basis (Fin n) R M
⊢ Free R M

Tactic:
exact Module.Free.of_basis b

Premises used: Module.Free.of_basis
-- 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 : Module.Finite R M
inst_6 : IsTorsionFree R M
obtain : ∀ (n : ℕ) (b : Basis (Fin n) R M), Free R M
⊢ Free R M

Tactic:
obtain ⟨n, b⟩ : Σ n, Basis (Fin n) R M := Module.basisOfFiniteTypeTorsionFree'

Premises used: Module.basisOfFiniteTypeTorsionFree'
-- 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_1 : ι → M
inst_3 : IsPrincipalIdealRing R
inst_4 : IsDomain R
inst_5 : Module.Finite R M
inst_6 : IsTorsionFree R M
n : ℕ
b : Basis (Fin n) R M
⊢ Free R M

Tactic:
Module.Free.of_basis b

Premises used: Module.Free.of_basis