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
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 ι
⊢ Free R M
have intro : ∀ (n : ℕ) (b : Basis (Fin n) R M), Free R M
Tactic: obtain ⟨n, b⟩ : Σ n, Basis (Fin n) R M := Module.basisOfFiniteTypeTorsionFree hs
-- 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 : Module.Finite R M
inst_6 : IsTorsionFree R M
⊢ Free R M
have obtain : ∀ (n : ℕ) (b : Basis (Fin n) R M), Free R M
Tactic: obtain ⟨n, b⟩ : Σ n, Basis (Fin n) R M := Module.basisOfFiniteTypeTorsionFree'
-- 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
S : Type u_4
inst_5 : CommRing S
inst_6 : Algebra R S
I : Ideal S
hI₁ : Module.Finite.{u_2, u_4} R ↥I
hI₂ : IsTorsionFree.{u_2, u_4} R ↥I
⊢ Free.{u_2, u_4} R ↥I
have this : Module.Finite.{u_2, u_4} R ↥(restrictScalars R I)
Tactic: have : Module.Finite R (restrictScalars R I) := hI₁
-- 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
S : Type u_4
inst_5 : CommRing S
inst_6 : Algebra R S
I : Ideal S
hI₁ : Module.Finite.{u_2, u_4} R ↥I
hI₂ : IsTorsionFree.{u_2, u_4} R ↥I
this : Module.Finite.{u_2, u_4} R ↥(restrictScalars R I)
⊢ Free.{u_2, u_4} R ↥I
have this₁ : IsTorsionFree.{u_2, u_4} R ↥(restrictScalars R I)
Tactic: have : IsTorsionFree R (restrictScalars R 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
S : Type u_4
inst_5 : CommRing S
inst_6 : Algebra R S
I : Ideal S
hI₁ : Module.Finite.{u_2, u_4} R ↥I
hI₂ : IsTorsionFree.{u_2, u_4} R ↥I
this_1 : Module.Finite.{u_2, u_4} R ↥(restrictScalars R I)
this : IsTorsionFree.{u_2, u_4} R ↥(restrictScalars R I)
⊢ Free.{u_2, u_4} R ↥I
have change : Free.{u_2, u_4} R ↥(restrictScalars R I)
Tactic: change Module.Free R (restrictScalars R I)
-- 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
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
m : ↥N
i : ι
hi : i ∉ range (ι := Fin n) (⇑snf.f : (a : Fin n) → ι)
⊢ Eq.{u_2 + 1} (α := R) ((((snf.bM.repr : (a : M) → ι →₀ R) (↑m : M) : ι →₀ R) : (a : ι) → R) i : R) (0 : R)
have obtain : ∀ (m : M) (hm : m ∈ N),
  Eq.{u_2 + 1} (α := R)
    ((((snf.bM.repr : (a : M) → ι →₀ R) (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N) m hm) : M) : ι →₀ R) : (a : ι) → R) i :
      R)
    (0 : R)
Tactic: obtain ⟨m, hm⟩ := m
Cleared hypotheses: m
-- 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
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
i : ι
hi : i ∉ range (ι := Fin n) (⇑snf.f : (a : Fin n) → ι)
m : M
hm : m ∈ N
⊢ Eq.{u_2 + 1} (α := R)
    ((((snf.bM.repr : (a : M) → ι →₀ R) (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N) m hm) : M) : ι →₀ R) : (a : ι) → R) i :
      R)
    (0 : R)
have obtain : ∀ (c : Fin n →₀ R)
  (hm : (c.sum fun (i : Fin n) (x : R) ↦ HSMul.hSMul (β := M) x (↑((snf.bN : (a : Fin n) → ↥N) i) : M)) ∈ N),
  Eq.{u_2 + 1} (α := R)
    ((((snf.bM.repr : (a : M) → ι →₀ R)
              (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N)
                    (c.sum fun (i : Fin n) (x : R) ↦ HSMul.hSMul (β := M) x (↑((snf.bN : (a : Fin n) → ↥N) i) : M))
                    hm) :
                M) :
            ι →₀ R) :
          (a : ι) → R)
        i :
      R)
    (0 : R)
Tactic: obtain ⟨c, rfl⟩ := snf.bN.mem_submodule_iff.mp hm
Cleared hypotheses: m, hm
-- 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
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
i : ι
hi : i ∉ range (ι := Fin n) (⇑snf.f : (a : Fin n) → ι)
c : Fin n →₀ R
hm : (c.sum fun (i : Fin n) (x : R) ↦ HSMul.hSMul (β := M) x (↑((snf.bN : (a : Fin n) → ↥N) i) : M)) ∈ N
⊢ Eq.{u_2 + 1} (α := R)
    ((((snf.bM.repr : (a : M) → ι →₀ R)
              (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N)
                    (c.sum fun (i : Fin n) (x : R) ↦ HSMul.hSMul (β := M) x (↑((snf.bN : (a : Fin n) → ↥N) i) : M))
                    hm) :
                M) :
            ι →₀ R) :
          (a : ι) → R)
        i :
      R)
    (0 : R)
have hi₁ : ∀ (j : Fin n), (snf.f : (a : Fin n) → ι) j ≠ i
Tactic: replace hi : ∀ j, snf.f j ≠ i := by simpa using hi
Cleared hypotheses: 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
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
m : ↥N
i : Fin n
⊢ Eq.{u_2 + 1} (α := R)
    ((((snf.bM.repr : (a : M) → ι →₀ R) (↑m : M) : ι →₀ R) : (a : ι) → R) ((snf.f : (a : Fin n) → ι) i : ι) : R)
    ((((snf.bN.repr : (a : ↥N) → Fin n →₀ R) (snf.a i • m) : Fin n →₀ R) : (a : Fin n) → R) i : R)
have obtain : ∀ (m : M) (hm : m ∈ N),
  Eq.{u_2 + 1} (α := R)
    ((((snf.bM.repr : (a : M) → ι →₀ R) (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N) m hm) : M) : ι →₀ R) : (a : ι) → R)
        ((snf.f : (a : Fin n) → ι) i : ι) :
      R)
    ((((snf.bN.repr : (a : ↥N) → Fin n →₀ R) (snf.a i • Subtype.mk (p := fun (x : M) ↦ x ∈ N) m hm) : Fin n →₀ R) :
          (a : Fin n) → R)
        i :
      R)
Tactic: obtain ⟨m, hm⟩ := m
Cleared hypotheses: m
-- 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
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
i : Fin n
m : M
hm : m ∈ N
⊢ Eq.{u_2 + 1} (α := R)
    ((((snf.bM.repr : (a : M) → ι →₀ R) (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N) m hm) : M) : ι →₀ R) : (a : ι) → R)
        ((snf.f : (a : Fin n) → ι) i : ι) :
      R)
    ((((snf.bN.repr : (a : ↥N) → Fin n →₀ R) (snf.a i • Subtype.mk (p := fun (x : M) ↦ x ∈ N) m hm) : Fin n →₀ R) :
          (a : Fin n) → R)
        i :
      R)
have obtain : ∀ (c : Fin n →₀ R)
  (hm : (c.sum fun (i : Fin n) (x : R) ↦ HSMul.hSMul (β := M) x (↑((snf.bN : (a : Fin n) → ↥N) i) : M)) ∈ N),
  Eq.{u_2 + 1} (α := R)
    ((((snf.bM.repr : (a : M) → ι →₀ R)
              (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N)
                    (c.sum fun (i : Fin n) (x : R) ↦ HSMul.hSMul (β := M) x (↑((snf.bN : (a : Fin n) → ↥N) i) : M))
                    hm) :
                M) :
            ι →₀ R) :
          (a : ι) → R)
        ((snf.f : (a : Fin n) → ι) i : ι) :
      R)
    ((((snf.bN.repr : (a : ↥N) → Fin n →₀ R)
              (snf.a i •
                Subtype.mk (p := fun (x : M) ↦ x ∈ N)
                  (c.sum fun (i : Fin n) (x : R) ↦ HSMul.hSMul (β := M) x (↑((snf.bN : (a : Fin n) → ↥N) i) : M)) hm) :
            Fin n →₀ R) :
          (a : Fin n) → R)
        i :
      R)
Tactic: obtain ⟨c, rfl⟩ := snf.bN.mem_submodule_iff.mp hm
Cleared hypotheses: m, hm
-- 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
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
i : Fin n
c : Fin n →₀ R
hm : (c.sum fun (i : Fin n) (x : R) ↦ HSMul.hSMul (β := M) x (↑((snf.bN : (a : Fin n) → ↥N) i) : M)) ∈ N
⊢ Subtype.mk (p := fun (x : M) ↦ x ∈ N)
      (c.sum fun (i : Fin n) (t : R) ↦ HSMul.hSMul (β := M) t (↑((snf.bN : (a : Fin n) → ↥N) i) : M)) hm =
    c.sum fun (i : Fin n) (t : R) ↦
      HSMul.hSMul (β := ↥N) t (Subtype.mk (p := fun (x : M) ↦ x ∈ N) (↑((snf.bN : (a : Fin n) → ↥N) i) : M) ⋯)
have a : (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N)
        (c.sum fun (i : Fin n) (t : R) ↦ HSMul.hSMul (β := M) t (↑((snf.bN : (a : Fin n) → ↥N) i) : M)) hm) :
    M) =
  (↑(c.sum fun (i : Fin n) (t : R) ↦
        HSMul.hSMul (β := ↥N) t (Subtype.mk (p := fun (x : M) ↦ x ∈ N) (↑((snf.bN : (a : Fin n) → ↥N) i) : M) sorry)) :
    M)
Tactic: ext
-- 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
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
i : Fin n
c : Fin n →₀ R
hm : (c.sum fun (i : Fin n) (x : R) ↦ HSMul.hSMul (β := M) x (↑((snf.bN : (a : Fin n) → ↥N) i) : M)) ∈ N
⊢ (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N)
          (c.sum fun (i : Fin n) (t : R) ↦ HSMul.hSMul (β := M) t (↑((snf.bN : (a : Fin n) → ↥N) i) : M)) hm) :
      M) =
    (↑(c.sum fun (i : Fin n) (t : R) ↦
          HSMul.hSMul (β := ↥N) t (Subtype.mk (p := fun (x : M) ↦ x ∈ N) (↑((snf.bN : (a : Fin n) → ↥N) i) : M) ⋯)) :
      M)
have a : (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N)
        (c.sum fun (i : Fin n) (t : R) ↦ HSMul.hSMul (β := M) t (↑((snf.bN : (a : Fin n) → ↥N) i) : M)) hm) :
    M) =
  (N.subtype : (a : ↥N) → M)
    (c.sum fun (i : Fin n) (t : R) ↦
      HSMul.hSMul (β := ↥N) t (Subtype.mk (p := fun (x : M) ↦ x ∈ N) (↑((snf.bN : (a : Fin n) → ↥N) i) : M) sorry))
Tactic: change _ = N.subtype _
-- 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
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
i : Fin n
c : Fin n →₀ R
hm : (c.sum fun (i : Fin n) (x : R) ↦ HSMul.hSMul (β := M) x (↑((snf.bN : (a : Fin n) → ↥N) i) : M)) ∈ N
⊢ Eq.{u_2 + 1} (α := R)
    ((((snf.bM.repr : (a : M) → ι →₀ R)
              (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N)
                    (c.sum fun (i : Fin n) (x : R) ↦ HSMul.hSMul (β := M) x (↑((snf.bN : (a : Fin n) → ↥N) i) : M))
                    hm) :
                M) :
            ι →₀ R) :
          (a : ι) → R)
        ((snf.f : (a : Fin n) → ι) i : ι) :
      R)
    ((((snf.bN.repr : (a : ↥N) → Fin n →₀ R)
              (snf.a i •
                Subtype.mk (p := fun (x : M) ↦ x ∈ N)
                  (c.sum fun (i : Fin n) (x : R) ↦ HSMul.hSMul (β := M) x (↑((snf.bN : (a : Fin n) → ↥N) i) : M)) hm) :
            Fin n →₀ R) :
          (a : Fin n) → R)
        i :
      R)
have hm₁ : Subtype.mk (p := fun (x : M) ↦ x ∈ N)
    (c.sum fun (i : Fin n) (t : R) ↦ HSMul.hSMul (β := M) t (↑((snf.bN : (a : Fin n) → ↥N) i) : M)) hm =
  c.sum fun (i : Fin n) (t : R) ↦
    HSMul.hSMul (β := ↥N) t (Subtype.mk (p := fun (x : M) ↦ x ∈ N) (↑((snf.bN : (a : Fin n) → ↥N) i) : M) sorry)
Tactic: replace hm : (⟨Finsupp.sum c fun i t ↦ t • (↑(snf.bN i) : M), hm⟩ : N) =
      Finsupp.sum c fun i t ↦ t • ⟨snf.bN i, (snf.bN i).2⟩ := by
    ext; change _ = N.subtype _; simp [map_finsuppSum]
-- 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
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
i : Fin n
c : Fin n →₀ R
hm_1 : (c.sum fun (i : Fin n) (x : R) ↦ HSMul.hSMul (β := M) x (↑((snf.bN : (a : Fin n) → ↥N) i) : M)) ∈ N
hm :
  Subtype.mk (p := fun (x : M) ↦ x ∈ N)
      (c.sum fun (i : Fin n) (t : R) ↦ HSMul.hSMul (β := M) t (↑((snf.bN : (a : Fin n) → ↥N) i) : M)) hm_1 =
    c.sum fun (i : Fin n) (t : R) ↦
      HSMul.hSMul (β := ↥N) t (Subtype.mk (p := fun (x : M) ↦ x ∈ N) (↑((snf.bN : (a : Fin n) → ↥N) i) : M) ⋯)
⊢ Eq.{u_2 + 1} (α := R)
    ((((snf.bM.repr : (a : M) → ι →₀ R)
              (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N)
                    (c.sum fun (i : Fin n) (x : R) ↦ HSMul.hSMul (β := M) x (↑((snf.bN : (a : Fin n) → ↥N) i) : M))
                    hm_1) :
                M) :
            ι →₀ R) :
          (a : ι) → R)
        ((snf.f : (a : Fin n) → ι) i : ι) :
      R)
    ((((snf.bN.repr : (a : ↥N) → Fin n →₀ R)
              (snf.a i •
                Subtype.mk (p := fun (x : M) ↦ x ∈ N)
                  (c.sum fun (i : Fin n) (x : R) ↦ HSMul.hSMul (β := M) x (↑((snf.bN : (a : Fin n) → ↥N) i) : M))
                  hm_1) :
            Fin n →₀ R) :
          (a : Fin n) → R)
        i :
      R)
have simp_rw : Eq (α := R) ((c : (a : Fin n) → R) i : R) (0 : R) → 0 = HMul.hMul (β := R) (snf.a i) ((c : (a : Fin n) → R) i : R)
Tactic: simp_rw [hm, map_smul, map_finsuppSum, map_smul, Subtype.coe_eta, repr_self,
    Finsupp.smul_single, smul_eq_mul, mul_one, Finsupp.sum_single, Finsupp.smul_apply, snf.snf,
    map_smul, repr_self, Finsupp.smul_single, smul_eq_mul, mul_one, Finsupp.sum_apply,
    Finsupp.single_apply, EmbeddingLike.apply_eq_iff_eq, Finsupp.sum_ite_eq',
    Finsupp.mem_support_iff, ite_not, mul_comm, ite_eq_right_iff]
-- 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
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
i : Fin n
c : Fin n →₀ R
hm_1 : (c.sum fun (i : Fin n) (x : R) ↦ HSMul.hSMul (β := M) x (↑((snf.bN : (a : Fin n) → ↥N) i) : M)) ∈ N
hm :
  Subtype.mk (p := fun (x : M) ↦ x ∈ N)
      (c.sum fun (i : Fin n) (t : R) ↦ HSMul.hSMul (β := M) t (↑((snf.bN : (a : Fin n) → ↥N) i) : M)) hm_1 =
    c.sum fun (i : Fin n) (t : R) ↦
      HSMul.hSMul (β := ↥N) t (Subtype.mk (p := fun (x : M) ↦ x ∈ N) (↑((snf.bN : (a : Fin n) → ↥N) i) : M) ⋯)
⊢ Eq.{u_2 + 1} (α := R)
    ((((snf.bM.repr : (a : M) → ι →₀ R)
              (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N)
                    (c.sum fun (i : Fin n) (x : R) ↦ HSMul.hSMul (β := M) x (↑((snf.bN : (a : Fin n) → ↥N) i) : M))
                    hm_1) :
                M) :
            ι →₀ R) :
          (a : ι) → R)
        ((snf.f : (a : Fin n) → ι) i : ι) :
      R)
    ((((snf.bN.repr : (a : ↥N) → Fin n →₀ R)
              (snf.a i •
                Subtype.mk (p := fun (x : M) ↦ x ∈ N)
                  (c.sum fun (i : Fin n) (x : R) ↦ HSMul.hSMul (β := M) x (↑((snf.bN : (a : Fin n) → ↥N) i) : M))
                  hm_1) :
            Fin n →₀ R) :
          (a : Fin n) → R)
        i :
      R)
have simp_rw : Eq.{u_2 + 1} (α := R)
  (((snf.bM.repr : (a : M) → ι →₀ R)
          (c.sum fun (i : Fin n) (x : R) ↦ HSMul.hSMul (β := M) x (↑((snf.bN : (a : Fin n) → ↥N) i) : M)) :
        (a : ι) → R)
      ((snf.f : (a : Fin n) → ι) i : ι) :
    R)
  ((((snf.bN.repr : (a : ↥N) → Fin n →₀ R)
            (snf.a i •
              Subtype.mk (p := fun (x : M) ↦ x ∈ N)
                (c.sum fun (i : Fin n) (x : R) ↦ HSMul.hSMul (β := M) x (↑((snf.bN : (a : Fin n) → ↥N) i) : M)) hm_1) :
          Fin n →₀ R) :
        (a : Fin n) → R)
      i :
    R)
Tactic: classical
  simp_rw [hm, map_smul, map_finsuppSum, map_smul, Subtype.coe_eta, repr_self,
    Finsupp.smul_single, smul_eq_mul, mul_one, Finsupp.sum_single, Finsupp.smul_apply, snf.snf,
    map_smul, repr_self, Finsupp.smul_single, smul_eq_mul, mul_one, Finsupp.sum_apply,
    Finsupp.single_apply, EmbeddingLike.apply_eq_iff_eq, Finsupp.sum_ite_eq',
    Finsupp.mem_support_iff, ite_not, mul_comm, ite_eq_right_iff]
  exact fun a ↦ (mul_eq_zero_of_right _ a).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
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
i : Fin n
c : Fin n →₀ R
hm_1 : (c.sum fun (i : Fin n) (x : R) ↦ HSMul.hSMul (β := M) x (↑((snf.bN : (a : Fin n) → ↥N) i) : M)) ∈ N
hm :
  Subtype.mk (p := fun (x : M) ↦ x ∈ N)
      (c.sum fun (i : Fin n) (t : R) ↦ HSMul.hSMul (β := M) t (↑((snf.bN : (a : Fin n) → ↥N) i) : M)) hm_1 =
    c.sum fun (i : Fin n) (t : R) ↦
      HSMul.hSMul (β := ↥N) t (Subtype.mk (p := fun (x : M) ↦ x ∈ N) (↑((snf.bN : (a : Fin n) → ↥N) i) : M) ⋯)
simp_rw simp_rw₁ :
  Eq.{u_2 + 1} (α := R)
    (((snf.bM.repr : (a : M) → ι →₀ R)
            (c.sum fun (i : Fin n) (x : R) ↦ HSMul.hSMul (β := M) x (↑((snf.bN : (a : Fin n) → ↥N) i) : M)) :
          (a : ι) → R)
        ((snf.f : (a : Fin n) → ι) i : ι) :
      R)
    ((((snf.bN.repr : (a : ↥N) → Fin n →₀ R)
              (snf.a i •
                Subtype.mk (p := fun (x : M) ↦ x ∈ N)
                  (c.sum fun (i : Fin n) (x : R) ↦ HSMul.hSMul (β := M) x (↑((snf.bN : (a : Fin n) → ↥N) i) : M))
                  hm_1) :
            Fin n →₀ R) :
          (a : Fin n) → R)
        i :
      R)
⊢ Eq.{u_2 + 1} (α := R)
    ((((snf.bM.repr : (a : M) → ι →₀ R)
              (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N)
                    (c.sum fun (i : Fin n) (x : R) ↦ HSMul.hSMul (β := M) x (↑((snf.bN : (a : Fin n) → ↥N) i) : M))
                    hm_1) :
                M) :
            ι →₀ R) :
          (a : ι) → R)
        ((snf.f : (a : Fin n) → ι) i : ι) :
      R)
    ((((snf.bN.repr : (a : ↥N) → Fin n →₀ R)
              (snf.a i •
                Subtype.mk (p := fun (x : M) ↦ x ∈ N)
                  (c.sum fun (i : Fin n) (x : R) ↦ HSMul.hSMul (β := M) x (↑((snf.bN : (a : Fin n) → ↥N) i) : M))
                  hm_1) :
            Fin n →₀ R) :
          (a : Fin n) → R)
        i :
      R)
have simp_rw₂ : Eq.{u_2 + 1} (α := R)
  (((snf.bM.repr : (a : M) → ι →₀ R)
          (c.sum fun (i : Fin n) (x : R) ↦ HSMul.hSMul (β := M) x (↑((snf.bN : (a : Fin n) → ↥N) i) : M)) :
        (a : ι) → R)
      ((snf.f : (a : Fin n) → ι) i : ι) :
    R)
  ((((snf.bN.repr : (a : ↥N) → Fin n →₀ R)
            (HSMul.hSMul (β := ↥N) (snf.a i)
              (c.sum fun (i : Fin n) (t : R) ↦
                HSMul.hSMul (β := ↥N) t
                  (Subtype.mk (p := fun (x : M) ↦ x ∈ N) (↑((snf.bN : (a : Fin n) → ↥N) i) : M) sorry))) :
          Fin n →₀ R) :
        (a : Fin n) → R)
      i :
    R)
Tactic: classical
  simp_rw [hm, map_smul, map_finsuppSum, map_smul, Subtype.coe_eta, repr_self,
    Finsupp.smul_single, smul_eq_mul, mul_one, Finsupp.sum_single, Finsupp.smul_apply, snf.snf,
    map_smul, repr_self, Finsupp.smul_single, smul_eq_mul, mul_one, Finsupp.sum_apply,
    Finsupp.single_apply, EmbeddingLike.apply_eq_iff_eq, Finsupp.sum_ite_eq',
    Finsupp.mem_support_iff, ite_not, mul_comm, ite_eq_right_iff]
  exact fun a ↦ (mul_eq_zero_of_right _ a).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
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
m : ↥N
⊢ Function.comp (β := ι) (⇑((snf.bM.repr : (a : M) → ι →₀ R) (↑m : M) : ι →₀ R) : (a : ι) → R)
      (⇑snf.f : (a : Fin n) → ι) =
    HSMul.hSMul (β := (a : Fin n) → R) snf.a (⇑((snf.bN.repr : (a : ↥N) → Fin n →₀ R) m : Fin n →₀ R) : (a : Fin n) → R)
have h : ∀ (i : Fin n),
  Function.comp (β := ι) (⇑((snf.bM.repr : (a : M) → ι →₀ R) (↑m : M) : ι →₀ R) : (a : ι) → R)
      (⇑snf.f : (a : Fin n) → ι) i =
    HSMul.hSMul (β := (a : Fin n) → R) snf.a (⇑((snf.bN.repr : (a : ↥N) → Fin n →₀ R) m : Fin n →₀ R) : (a : Fin n) → R)
      i
Tactic: ext i
-- 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
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
i : Fin n
⊢ snf.bM.coord ((snf.f : (a : Fin n) → ι) i) ∘ₗ N.subtype = snf.a i • snf.bN.coord i
have h : ∀ (m : ↥N),
  Eq.{u_2 + 1} (α := R) ((snf.bM.coord ((snf.f : (a : Fin n) → ι) i) ∘ₗ N.subtype : (a : ↥N) → R) m : R)
    ((snf.a i • snf.bN.coord i : (a : ↥N) → R) m : R)
Tactic: ext m
-- 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
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
inst_3 : Fintype ι
inst_4 : DecidableEq ι
f : M →ₗ[R] M
hf : ∀ (x : M), Membership.mem (α := M) N ((f : (a : M) → M) x : M)
hf' : ∀ x ∈ N, Membership.mem (α := M) N ((f : (a : M) → M) x : M)
i : Fin n
⊢ Eq.{u_2 + 1} (α := R)
    ((LinearMap.toMatrix snf.bN snf.bN : (a : ↥N →ₗ[R] ↥N) → Matrix (Fin n) (Fin n) R) (f.restrict hf') i i : R)
    ((LinearMap.toMatrix snf.bM snf.bM : (a : M →ₗ[R] M) → Matrix ι ι R) f ((snf.f : (a : Fin n) → ι) i)
        ((snf.f : (a : Fin n) → ι) i) :
      R)
have rw : Eq.{u_2 + 1} (α := R)
  ((((snf.bN.repr : (a : ↥N) → Fin n →₀ R) ((f.restrict hf' : (a : ↥N) → ↥N) ((snf.bN : (a : Fin n) → ↥N) i)) :
          Fin n →₀ R) :
        (a : Fin n) → R)
      i :
    R)
  ((((snf.bN.repr : (a : ↥N) → Fin n →₀ R)
            (HSMul.hSMul (β := ↥N) (snf.a i)
              (Subtype.mk (p := fun (x : M) ↦ x ∈ N)
                  ((f : (a : M) → M) ((snf.bM : (a : ι) → M) ((snf.f : (a : Fin n) → ι) i : ι) : M)) sorry :
                ↥N)) :
          Fin n →₀ R) :
        (a : Fin n) → R)
      i :
    R)
Tactic: rw [LinearMap.toMatrix_apply, LinearMap.toMatrix_apply,
    snf.repr_apply_embedding_eq_repr_smul ⟨_, (hf _)⟩]
-- 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
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
inst_3 : Fintype ι
inst_4 : DecidableEq ι
f : M →ₗ[R] M
hf : ∀ (x : M), Membership.mem (α := M) N ((f : (a : M) → M) x : M)
hf' : ∀ x ∈ N, Membership.mem (α := M) N ((f : (a : M) → M) x : M)
i : Fin n
⊢ Eq.{u_2 + 1} (α := R)
    ((((snf.bN.repr : (a : ↥N) → Fin n →₀ R) ((f.restrict hf' : (a : ↥N) → ↥N) ((snf.bN : (a : Fin n) → ↥N) i)) :
            Fin n →₀ R) :
          (a : Fin n) → R)
        i :
      R)
    ((((snf.bN.repr : (a : ↥N) → Fin n →₀ R)
              (HSMul.hSMul (β := ↥N) (snf.a i)
                (Subtype.mk (p := fun (x : M) ↦ x ∈ N)
                    ((f : (a : M) → M) ((snf.bM : (a : ι) → M) ((snf.f : (a : Fin n) → ι) i : ι) : M)) ⋯ :
                  ↥N)) :
            Fin n →₀ R) :
          (a : Fin n) → R)
        i :
      R)
have e_a : (f.restrict hf' : (a : ↥N) → ↥N) ((snf.bN : (a : Fin n) → ↥N) i) =
  HSMul.hSMul (β := ↥N) (snf.a i)
    (Subtype.mk (p := fun (x : M) ↦ x ∈ N)
        ((f : (a : M) → M) ((snf.bM : (a : ι) → M) ((snf.f : (a : Fin n) → ι) i : ι) : M)) sorry :
      ↥N)
Tactic: congr
-- 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
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
inst_3 : Fintype ι
inst_4 : DecidableEq ι
f : M →ₗ[R] M
hf : ∀ (x : M), Membership.mem (α := M) N ((f : (a : M) → M) x : M)
hf' : ∀ x ∈ N, Membership.mem (α := M) N ((f : (a : M) → M) x : M)
i : Fin n
⊢ (f.restrict hf' : (a : ↥N) → ↥N) ((snf.bN : (a : Fin n) → ↥N) i) =
    HSMul.hSMul (β := ↥N) (snf.a i)
      (Subtype.mk (p := fun (x : M) ↦ x ∈ N)
          ((f : (a : M) → M) ((snf.bM : (a : ι) → M) ((snf.f : (a : Fin n) → ι) i : ι) : M)) ⋯ :
        ↥N)
have e_a : (↑((f.restrict hf' : (a : ↥N) → ↥N) ((snf.bN : (a : Fin n) → ↥N) i)) : M) =
  (↑(HSMul.hSMul (β := ↥N) (snf.a i)
        (Subtype.mk (p := fun (x : M) ↦ x ∈ N)
            ((f : (a : M) → M) ((snf.bM : (a : ι) → M) ((snf.f : (a : Fin n) → ι) i : ι) : M)) sorry :
          ↥N)) :
    M)
Tactic: ext