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_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:
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
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
⊢ Module.Finite.{u_2, u_4} R ↥(restrictScalars R I)

Tactic:
have : Module.Finite R (restrictScalars R 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
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)
⊢ IsTorsionFree.{u_2, u_4} R ↥(restrictScalars R I)

Tactic:
have : IsTorsionFree R (restrictScalars R 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
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)
change : Free.{u_2, u_4} R ↥(restrictScalars R I)
⊢ Free.{u_2, u_4} R ↥I

Tactic:
change Module.Free R (restrictScalars R I)

Premises used: Submodule.restrictScalars, Membership.mem, Subtype, Module.Free
-- 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
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 ↥(restrictScalars R I)

Tactic:
Module.free_of_finite_type_torsion_free'

Premises used: Module.free_of_finite_type_torsion_free'
-- 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
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 ↥(restrictScalars R I)

Tactic:
exact Module.free_of_finite_type_torsion_free'

Premises used: Module.free_of_finite_type_torsion_free'
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
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 : Module.Finite R M
⊢ Free R M ↔ IsTorsionFree R M

Tactic:
⟨fun _ ↦ inferInstance, fun _ ↦ inferInstance⟩

Premises used: inferInstance, Iff.intro
-- 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
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
m : ↥N
i : ι
hi : i ∉ range (ι := Fin n) (⇑snf.f : (a : Fin n) → ι)
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)
⊢ Eq.{u_2 + 1} (α := R) ((((snf.bM.repr : (a : M) → ι →₀ R) (↑m : M) : ι →₀ R) : (a : ι) → R) i : R) (0 : R)

Tactic:
obtain ⟨m, hm⟩ := m
-- 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
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
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)
⊢ 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 ⟨c, rfl⟩ := snf.bN.mem_submodule_iff.mp hm

Premises used: Module.Basis.mem_submodule_iff, Iff.mp, Module.Basis.SmithNormalForm.bN, rfl
-- 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
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
⊢ ∀ (j : Fin n), (snf.f : (a : Fin n) → ι) j ≠ i

Tactic:
simpa using 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
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
⊢ ∀ (j : Fin n), (snf.f : (a : Fin n) → ι) j ≠ i

Tactic:
replace hi : ∀ j, snf.f j ≠ i := by simpa using 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
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
i : ι
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
hi : ∀ (j : Fin n), (snf.f : (a : Fin n) → ι) j ≠ i
⊢ 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:
simp [hi, snf.snf, map_finsuppSum]

Premises used: Module.Basis.SmithNormalForm.snf, map_finsuppSum
-- 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
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
i : ι
hi : i ∉ range (ι := Fin n) (⇑snf.f : (a : Fin n) → ι)
⊢ N ≤ (snf.bM.coord i).ker

Tactic:
fun m hm ↦ snf.repr_eq_zero_of_notMem_range ⟨m, hm⟩ hi

Premises used: Set.Mem, setOf, Subtype.mk, Set.preimage, Set.singleton, Module.Basis.SmithNormalForm.repr_eq_zero_of_notMem_range
-- 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
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
m : ↥N
i : Fin n
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)
⊢ 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)

Tactic:
obtain ⟨m, hm⟩ := m
-- 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
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
i : Fin n
m : M
hm : m ∈ N
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)
⊢ 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 ⟨c, rfl⟩ := snf.bN.mem_submodule_iff.mp hm

Premises used: Module.Basis.mem_submodule_iff, Iff.mp, Module.Basis.SmithNormalForm.bN, rfl
-- 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
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
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) ⋯)) :
      M)
⊢ 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) ⋯)

Tactic:
ext
-- 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
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
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) ⋯))
⊢ (↑(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)

Tactic:
change _ = N.subtype _

Premises used: Submodule.subtype, DFunLike.coe
-- 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
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) =
    (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) ⋯))

Tactic:
simp [map_finsuppSum]

Premises used: map_finsuppSum
-- 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
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) ⋯)

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]
-- 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
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 :
  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)
⊢ 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)

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]

Premises used: Finsupp.mem_support_iff, Finsupp.sum_ite_eq', Module.Basis.SmithNormalForm.snf, EmbeddingLike.apply_eq_iff_eq, Finsupp.smul_apply, ite_eq_right_iff, Subtype.coe_eta, map_finsuppSum, mul_comm, ite_not, Finsupp.single_apply, smul_eq_mul, mul_one, Finsupp.sum_apply, Finsupp.smul_single, Finsupp.sum_single, Module.Basis.repr_self, map_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
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 (α := 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:
fun a ↦ (mul_eq_zero_of_right _ a).symm

Premises used: Module.Basis.SmithNormalForm.a, mul_eq_zero_of_right, Eq.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
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 (α := 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:
exact fun a ↦ (mul_eq_zero_of_right _ a).symm

Premises used: mul_eq_zero_of_right, Eq.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
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
m : ↥N
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
⊢ 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)

Tactic:
ext i
-- 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
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
m : ↥N
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:
simp [Pi.smul_apply (snf.a i)]

Premises used: Module.Basis.SmithNormalForm.a, Pi.smul_apply
-- 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
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
i : Fin n
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)
⊢ snf.bM.coord ((snf.f : (a : Fin n) → ι) i) ∘ₗ N.subtype = snf.a i • snf.bN.coord i

Tactic:
ext m
-- 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
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
i : Fin n
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:
simp [Pi.smul_apply (snf.a i)]

Premises used: Module.Basis.SmithNormalForm.a, Pi.smul_apply
-- 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
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
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)) ⋯ :
                  ↥N)) :
            Fin n →₀ R) :
          (a : Fin n) → R)
        i :
      R)
⊢ 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)

Tactic:
rw [LinearMap.toMatrix_apply, LinearMap.toMatrix_apply,
    snf.repr_apply_embedding_eq_repr_smul ⟨_, (hf _)⟩]

Premises used: Module.Basis.SmithNormalForm.repr_apply_embedding_eq_repr_smul, Subtype.mk, LinearMap.toMatrix_apply
-- 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
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
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)) ⋯ :
        ↥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)

Tactic:
congr
-- 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
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
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)) ⋯ :
            ↥N)) :
      M)
⊢ (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)

Tactic:
ext