awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.FreeModule.Int
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Fintype ι
inst_3 : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis.{0, u_2, u_3} (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf :
  ∀ (i : Fin n),
    (↑((bN : (a : Fin n) → ↥N) i) : M) =
      HSMul.hSMul (β := M) (a i) ((bM : (a : ι) → M) ((f : (a : Fin n) → ι) i : ι) : M)
N' : Submodule R (ι → R) := Submodule.map (↑bM.equivFun : M →ₗ[R] ι → R) N
hN' : N' = Submodule.map (↑bM.equivFun : M →ₗ[R] ι → R) N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' :
  ∀ (i : Fin n),
    Eq (α := ι → R) ((↑((bN' : (a : Fin n) → ↥N') i) : ι → R) : ι → R)
      (Pi.single (M := fun (j : ι) ↦ R) ((f : (a : Fin n) → ι) i) (a i) : (j : ι) → R)
hNN' : N.toAddSubgroup.index = AddSubgroup.index (G := ι → R) N'.toAddSubgroup
g : ι → R
⊢ (∃ (c : Fin n → R),
      g =
        ∑ x : Fin n,
          HSMul.hSMul (β := ι → R) (c x)
            (Pi.single (M := fun (j : ι) ↦ R) ((f : (a : Fin n) → ι) x) (a x) : (j : ι) → R)) ↔
    ∀ (i : ι),
      (if h : ∃ (j : Fin n), (f : (a : Fin n) → ι) j = i then
          a (h.choose (p := fun (j : Fin n) ↦ (f : (a : Fin n) → ι) j = i))
        else 0) ∣
        g i

Tactic:
⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.LinearAlgebra.FreeModule.Int
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Fintype ι
inst_3 : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis.{0, u_2, u_3} (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf :
  ∀ (i : Fin n),
    (↑((bN : (a : Fin n) → ↥N) i) : M) =
      HSMul.hSMul (β := M) (a i) ((bM : (a : ι) → M) ((f : (a : Fin n) → ι) i : ι) : M)
N' : Submodule R (ι → R) := Submodule.map (↑bM.equivFun : M →ₗ[R] ι → R) N
hN' : N' = Submodule.map (↑bM.equivFun : M →ₗ[R] ι → R) N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' :
  ∀ (i : Fin n),
    Eq (α := ι → R) ((↑((bN' : (a : Fin n) → ↥N') i) : ι → R) : ι → R)
      (Pi.single (M := fun (j : ι) ↦ R) ((f : (a : Fin n) → ι) i) (a i) : (j : ι) → R)
hNN' : N.toAddSubgroup.index = AddSubgroup.index (G := ι → R) N'.toAddSubgroup
g : ι → R
h :
  ∀
    (h :
      ∃ (c : Fin n → R),
        g =
          ∑ x : Fin n,
            HSMul.hSMul (β := ι → R) (c x)
              (Pi.single (M := fun (j : ι) ↦ R) ((f : (a : Fin n) → ι) x) (a x) : (j : ι) → R))
    (i : ι),
    (if h : ∃ (j : Fin n), (f : (a : Fin n) → ι) j = i then
        a (h.choose (p := fun (j : Fin n) ↦ (f : (a : Fin n) → ι) j = i))
      else 0) ∣
      g i
h₁ :
  ∀
    (h :
      ∀ (i : ι),
        (if h : ∃ (j : Fin n), (f : (a : Fin n) → ι) j = i then
            a (h.choose (p := fun (j : Fin n) ↦ (f : (a : Fin n) → ι) j = i))
          else 0) ∣
          g i),
    ∃ (c : Fin n → R),
      g =
        ∑ x : Fin n,
          HSMul.hSMul (β := ι → R) (c x)
            (Pi.single (M := fun (j : ι) ↦ R) ((f : (a : Fin n) → ι) x) (a x) : (j : ι) → R)
⊢ (∃ (c : Fin n → R),
      g =
        ∑ x : Fin n,
          HSMul.hSMul (β := ι → R) (c x)
            (Pi.single (M := fun (j : ι) ↦ R) ((f : (a : Fin n) → ι) x) (a x) : (j : ι) → R)) ↔
    ∀ (i : ι),
      (if h : ∃ (j : Fin n), (f : (a : Fin n) → ι) j = i then
          a (h.choose (p := fun (j : Fin n) ↦ (f : (a : Fin n) → ι) j = i))
        else 0) ∣
        g i

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.LinearAlgebra.FreeModule.Int
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Fintype ι
inst_3 : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis.{0, u_2, u_3} (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf :
  ∀ (i : Fin n),
    (↑((bN : (a : Fin n) → ↥N) i) : M) =
      HSMul.hSMul (β := M) (a i) ((bM : (a : ι) → M) ((f : (a : Fin n) → ι) i : ι) : M)
N' : Submodule R (ι → R) := Submodule.map (↑bM.equivFun : M →ₗ[R] ι → R) N
hN' : N' = Submodule.map (↑bM.equivFun : M →ₗ[R] ι → R) N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' :
  ∀ (i : Fin n),
    Eq (α := ι → R) ((↑((bN' : (a : Fin n) → ↥N') i) : ι → R) : ι → R)
      (Pi.single (M := fun (j : ι) ↦ R) ((f : (a : Fin n) → ι) i) (a i) : (j : ι) → R)
hNN' : N.toAddSubgroup.index = AddSubgroup.index (G := ι → R) N'.toAddSubgroup
g : ι → R
h :
  ∃ (c : Fin n → R),
    g =
      ∑ x : Fin n,
        HSMul.hSMul (β := ι → R) (c x) (Pi.single (M := fun (j : ι) ↦ R) ((f : (a : Fin n) → ι) x) (a x) : (j : ι) → R)
h₁ :
  ∀ (c : Fin n → R) (i : ι),
    Dvd.dvd.{u_2} (α := R)
      (if h : ∃ (j : Fin n), (f : (a : Fin n) → ι) j = i then
        a (h.choose (p := fun (j : Fin n) ↦ (f : (a : Fin n) → ι) j = i))
      else 0)
      ((∑ x : Fin n,
          HSMul.hSMul (β := ι → R) (c x)
            (Pi.single (M := fun (j : ι) ↦ R) ((f : (a : Fin n) → ι) x) (a x) : (j : ι) → R))
        i)
⊢ ∀ (i : ι),
    (if h : ∃ (j : Fin n), (f : (a : Fin n) → ι) j = i then
        a (h.choose (p := fun (j : Fin n) ↦ (f : (a : Fin n) → ι) j = i))
      else 0) ∣
      g i

Tactic:
rcases h with ⟨c, rfl⟩

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.FreeModule.Int
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Fintype ι
inst_3 : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis.{0, u_2, u_3} (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf :
  ∀ (i : Fin n),
    (↑((bN : (a : Fin n) → ↥N) i) : M) =
      HSMul.hSMul (β := M) (a i) ((bM : (a : ι) → M) ((f : (a : Fin n) → ι) i : ι) : M)
N' : Submodule R (ι → R) := Submodule.map (↑bM.equivFun : M →ₗ[R] ι → R) N
hN' : N' = Submodule.map (↑bM.equivFun : M →ₗ[R] ι → R) N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' :
  ∀ (i : Fin n),
    Eq (α := ι → R) ((↑((bN' : (a : Fin n) → ↥N') i) : ι → R) : ι → R)
      (Pi.single (M := fun (j : ι) ↦ R) ((f : (a : Fin n) → ι) i) (a i) : (j : ι) → R)
hNN' : N.toAddSubgroup.index = AddSubgroup.index (G := ι → R) N'.toAddSubgroup
c : Fin n → R
i : ι
h :
  Dvd.dvd.{u_2} (α := R)
    (if h : ∃ (j : Fin n), (f : (a : Fin n) → ι) j = i then
      a (h.choose (p := fun (j : Fin n) ↦ (f : (a : Fin n) → ι) j = i))
    else 0)
    (∑ x : Fin n, c x • if i = (f : (a : Fin n) → ι) x then a x else 0)
⊢ Dvd.dvd.{u_2} (α := R)
    (if h : ∃ (j : Fin n), (f : (a : Fin n) → ι) j = i then
      a (h.choose (p := fun (j : Fin n) ↦ (f : (a : Fin n) → ι) j = i))
    else 0)
    ((∑ x : Fin n,
        HSMul.hSMul (β := ι → R) (c x) (Pi.single (M := fun (j : ι) ↦ R) ((f : (a : Fin n) → ι) x) (a x) : (j : ι) → R))
      i)

Tactic:
simp only [Finset.sum_apply, Pi.smul_apply, Pi.single_apply]

Premises used: Pi.single_apply, Finset.sum_apply, Pi.smul_apply
-- Module: Mathlib.LinearAlgebra.FreeModule.Int
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Fintype ι
inst_3 : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis.{0, u_2, u_3} (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf :
  ∀ (i : Fin n),
    (↑((bN : (a : Fin n) → ↥N) i) : M) =
      HSMul.hSMul (β := M) (a i) ((bM : (a : ι) → M) ((f : (a : Fin n) → ι) i : ι) : M)
N' : Submodule R (ι → R) := Submodule.map (↑bM.equivFun : M →ₗ[R] ι → R) N
hN' : N' = Submodule.map (↑bM.equivFun : M →ₗ[R] ι → R) N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' :
  ∀ (i : Fin n),
    Eq (α := ι → R) ((↑((bN' : (a : Fin n) → ↥N') i) : ι → R) : ι → R)
      (Pi.single (M := fun (j : ι) ↦ R) ((f : (a : Fin n) → ι) i) (a i) : (j : ι) → R)
hNN' : N.toAddSubgroup.index = AddSubgroup.index (G := ι → R) N'.toAddSubgroup
c : Fin n → R
i : ι
pos :
  ∀ (h : ∃ (j : Fin n), (f : (a : Fin n) → ι) j = i),
    a (h.choose (p := fun (j : Fin n) ↦ (f : (a : Fin n) → ι) j = i)) ∣
      ∑ x : Fin n, c x • if i = (f : (a : Fin n) → ι) x then a x else 0
neg :
  ∀ (h : ¬∃ (j : Fin n), (f : (a : Fin n) → ι) j = i),
    Dvd.dvd.{u_2} (α := R) 0 (∑ x : Fin n, c x • if i = (f : (a : Fin n) → ι) x then a x else 0)
⊢ Dvd.dvd.{u_2} (α := R)
    (if h : ∃ (j : Fin n), (f : (a : Fin n) → ι) j = i then
      a (h.choose (p := fun (j : Fin n) ↦ (f : (a : Fin n) → ι) j = i))
    else 0)
    (∑ x : Fin n, c x • if i = (f : (a : Fin n) → ι) x then a x else 0)

Tactic:
split_ifs with h
-- Module: Mathlib.LinearAlgebra.FreeModule.Int
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Fintype ι
inst_3 : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis.{0, u_2, u_3} (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf :
  ∀ (i : Fin n),
    (↑((bN : (a : Fin n) → ↥N) i) : M) =
      HSMul.hSMul (β := M) (a i) ((bM : (a : ι) → M) ((f : (a : Fin n) → ι) i : ι) : M)
N' : Submodule R (ι → R) := Submodule.map (↑bM.equivFun : M →ₗ[R] ι → R) N
hN' : N' = Submodule.map (↑bM.equivFun : M →ₗ[R] ι → R) N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' :
  ∀ (i : Fin n),
    Eq (α := ι → R) ((↑((bN' : (a : Fin n) → ↥N') i) : ι → R) : ι → R)
      (Pi.single (M := fun (j : ι) ↦ R) ((f : (a : Fin n) → ι) i) (a i) : (j : ι) → R)
hNN' : N.toAddSubgroup.index = AddSubgroup.index (G := ι → R) N'.toAddSubgroup
c : Fin n → R
i : ι
h : ∃ (j : Fin n), (f : (a : Fin n) → ι) j = i
⊢ a (h.choose (p := fun (j : Fin n) ↦ (f : (a : Fin n) → ι) j = i)) ∣
    c (h.choose (p := fun (j : Fin n) ↦ (f : (a : Fin n) → ι) j = i)) *
      a (h.choose (p := fun (j : Fin n) ↦ (f : (a : Fin n) → ι) j = i))

Tactic:
dvd_mul_left (a h.choose) (c h.choose)

Premises used: dvd_mul_left, Exists.choose
-- Module: Mathlib.LinearAlgebra.FreeModule.Int
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Fintype ι
inst_3 : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis.{0, u_2, u_3} (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf :
  ∀ (i : Fin n),
    (↑((bN : (a : Fin n) → ↥N) i) : M) =
      HSMul.hSMul (β := M) (a i) ((bM : (a : ι) → M) ((f : (a : Fin n) → ι) i : ι) : M)
N' : Submodule R (ι → R) := Submodule.map (↑bM.equivFun : M →ₗ[R] ι → R) N
hN' : N' = Submodule.map (↑bM.equivFun : M →ₗ[R] ι → R) N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' :
  ∀ (i : Fin n),
    Eq (α := ι → R) ((↑((bN' : (a : Fin n) → ↥N') i) : ι → R) : ι → R)
      (Pi.single (M := fun (j : ι) ↦ R) ((f : (a : Fin n) → ι) i) (a i) : (j : ι) → R)
hNN' : N.toAddSubgroup.index = AddSubgroup.index (G := ι → R) N'.toAddSubgroup
c : Fin n → R
i : ι
h : ∃ (j : Fin n), (f : (a : Fin n) → ι) j = i
h₁ :
  (∑ x : Fin n, c x • if i = (f : (a : Fin n) → ι) x then a x else 0) =
    c (h.choose (p := fun (j : Fin n) ↦ (f : (a : Fin n) → ι) j = i)) *
      a (h.choose (p := fun (j : Fin n) ↦ (f : (a : Fin n) → ι) j = i))
⊢ a (h.choose (p := fun (j : Fin n) ↦ (f : (a : Fin n) → ι) j = i)) ∣
    ∑ x : Fin n, c x • if i = (f : (a : Fin n) → ι) x then a x else 0

Tactic:
convert! dvd_mul_left (a h.choose) (c h.choose)

Premises used: dvd_mul_left, Exists.choose
-- Module: Mathlib.LinearAlgebra.FreeModule.Int
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Fintype ι
inst_3 : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis.{0, u_2, u_3} (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf :
  ∀ (i : Fin n),
    (↑((bN : (a : Fin n) → ↥N) i) : M) =
      HSMul.hSMul (β := M) (a i) ((bM : (a : ι) → M) ((f : (a : Fin n) → ι) i : ι) : M)
N' : Submodule R (ι → R) := Submodule.map (↑bM.equivFun : M →ₗ[R] ι → R) N
hN' : N' = Submodule.map (↑bM.equivFun : M →ₗ[R] ι → R) N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' :
  ∀ (i : Fin n),
    Eq (α := ι → R) ((↑((bN' : (a : Fin n) → ↥N') i) : ι → R) : ι → R)
      (Pi.single (M := fun (j : ι) ↦ R) ((f : (a : Fin n) → ι) i) (a i) : (j : ι) → R)
hNN' : N.toAddSubgroup.index = AddSubgroup.index (G := ι → R) N'.toAddSubgroup
c : Fin n → R
i : ι
h : ∃ (j : Fin n), (f : (a : Fin n) → ι) j = i
⊢ h.choose (p := fun (j : Fin n) ↦ (f : (a : Fin n) → ι) j = i) ∉ Finset.univ →
    (c (h.choose (p := fun (j : Fin n) ↦ (f : (a : Fin n) → ι) j = i)) •
        if i = (f : (a : Fin n) → ι) (h.choose (p := fun (j : Fin n) ↦ (f : (a : Fin n) → ι) j = i)) then
          a (h.choose (p := fun (j : Fin n) ↦ (f : (a : Fin n) → ι) j = i))
        else 0) =
      0

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.FreeModule.Int
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Fintype ι
inst_3 : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis.{0, u_2, u_3} (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf :
  ∀ (i : Fin n),
    (↑((bN : (a : Fin n) → ↥N) i) : M) =
      HSMul.hSMul (β := M) (a i) ((bM : (a : ι) → M) ((f : (a : Fin n) → ι) i : ι) : M)
N' : Submodule R (ι → R) := Submodule.map (↑bM.equivFun : M →ₗ[R] ι → R) N
hN' : N' = Submodule.map (↑bM.equivFun : M →ₗ[R] ι → R) N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' :
  ∀ (i : Fin n),
    Eq (α := ι → R) ((↑((bN' : (a : Fin n) → ↥N') i) : ι → R) : ι → R)
      (Pi.single (M := fun (j : ι) ↦ R) ((f : (a : Fin n) → ι) i) (a i) : (j : ι) → R)
hNN' : N.toAddSubgroup.index = AddSubgroup.index (G := ι → R) N'.toAddSubgroup
c : Fin n → R
i : ι
h : ∃ (j : Fin n), (f : (a : Fin n) → ι) j = i
refine :
  ∀ (b : Fin n),
    Membership.mem (γ := Finset (Fin n)) Finset.univ b →
      b ≠ h.choose (p := fun (j : Fin n) ↦ (f : (a : Fin n) → ι) j = i) →
        (c b • if i = (f : (a : Fin n) → ι) b then a b else 0) = 0
⊢ (∑ x : Fin n, c x • if i = (f : (a : Fin n) → ι) x then a x else 0) =
    c (h.choose (p := fun (j : Fin n) ↦ (f : (a : Fin n) → ι) j = i)) *
      if i = (f : (a : Fin n) → ι) (h.choose (p := fun (j : Fin n) ↦ (f : (a : Fin n) → ι) j = i)) then
        a (h.choose (p := fun (j : Fin n) ↦ (f : (a : Fin n) → ι) j = i))
      else 0

Tactic:
refine Finset.sum_eq_single h.choose ?_ (by simp)

Premises used: Finset.sum_eq_single, Exists.choose
-- Module: Mathlib.LinearAlgebra.FreeModule.Int
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Fintype ι
inst_3 : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis.{0, u_2, u_3} (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf :
  ∀ (i : Fin n),
    (↑((bN : (a : Fin n) → ↥N) i) : M) =
      HSMul.hSMul (β := M) (a i) ((bM : (a : ι) → M) ((f : (a : Fin n) → ι) i : ι) : M)
N' : Submodule R (ι → R) := Submodule.map (↑bM.equivFun : M →ₗ[R] ι → R) N
hN' : N' = Submodule.map (↑bM.equivFun : M →ₗ[R] ι → R) N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' :
  ∀ (i : Fin n),
    Eq (α := ι → R) ((↑((bN' : (a : Fin n) → ↥N') i) : ι → R) : ι → R)
      (Pi.single (M := fun (j : ι) ↦ R) ((f : (a : Fin n) → ι) i) (a i) : (j : ι) → R)
hNN' : N.toAddSubgroup.index = AddSubgroup.index (G := ι → R) N'.toAddSubgroup
c : Fin n → R
i : ι
h : ∃ (j : Fin n), (f : (a : Fin n) → ι) j = i
j : Fin n
hj : j ≠ h.choose (p := fun (j : Fin n) ↦ (f : (a : Fin n) → ι) j = i)
⊢ Ne (α := ι) ((f : (a : Fin n) → ι) j : ι)
    ((f : (a : Fin n) → ι) (h.choose (p := fun (j : Fin n) ↦ (f : (a : Fin n) → ι) j = i)) : ι)

Tactic:
have hinj := f.injective.ne hj
-- Module: Mathlib.LinearAlgebra.FreeModule.Int
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Fintype ι
inst_3 : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis.{0, u_2, u_3} (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf :
  ∀ (i : Fin n),
    (↑((bN : (a : Fin n) → ↥N) i) : M) =
      HSMul.hSMul (β := M) (a i) ((bM : (a : ι) → M) ((f : (a : Fin n) → ι) i : ι) : M)
N' : Submodule R (ι → R) := Submodule.map (↑bM.equivFun : M →ₗ[R] ι → R) N
hN' : N' = Submodule.map (↑bM.equivFun : M →ₗ[R] ι → R) N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' :
  ∀ (i : Fin n),
    Eq (α := ι → R) ((↑((bN' : (a : Fin n) → ↥N') i) : ι → R) : ι → R)
      (Pi.single (M := fun (j : ι) ↦ R) ((f : (a : Fin n) → ι) i) (a i) : (j : ι) → R)
hNN' : N.toAddSubgroup.index = AddSubgroup.index (G := ι → R) N'.toAddSubgroup
c : Fin n → R
i : ι
h : ∃ (j : Fin n), (f : (a : Fin n) → ι) j = i
j : Fin n
hj : j ≠ h.choose (p := fun (j : Fin n) ↦ (f : (a : Fin n) → ι) j = i)
hinj :
  Ne (α := ι) ((f : (a : Fin n) → ι) j : ι)
    ((f : (a : Fin n) → ι) (h.choose (p := fun (j : Fin n) ↦ (f : (a : Fin n) → ι) j = i)) : ι)
⊢ (f : (a : Fin n) → ι) j ≠ i

Tactic:
rw [h.choose_spec] at hinj

Premises used: Exists.choose_spec
-- Module: Mathlib.LinearAlgebra.FreeModule.Int
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Fintype ι
inst_3 : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis.{0, u_2, u_3} (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf :
  ∀ (i : Fin n),
    (↑((bN : (a : Fin n) → ↥N) i) : M) =
      HSMul.hSMul (β := M) (a i) ((bM : (a : ι) → M) ((f : (a : Fin n) → ι) i : ι) : M)
N' : Submodule R (ι → R) := Submodule.map (↑bM.equivFun : M →ₗ[R] ι → R) N
hN' : N' = Submodule.map (↑bM.equivFun : M →ₗ[R] ι → R) N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' :
  ∀ (i : Fin n),
    Eq (α := ι → R) ((↑((bN' : (a : Fin n) → ↥N') i) : ι → R) : ι → R)
      (Pi.single (M := fun (j : ι) ↦ R) ((f : (a : Fin n) → ι) i) (a i) : (j : ι) → R)
hNN' : N.toAddSubgroup.index = AddSubgroup.index (G := ι → R) N'.toAddSubgroup
c : Fin n → R
i : ι
h : ∃ (j : Fin n), (f : (a : Fin n) → ι) j = i
j : Fin n
hj : j ≠ h.choose (p := fun (j : Fin n) ↦ (f : (a : Fin n) → ι) j = i)
hinj : (f : (a : Fin n) → ι) j ≠ i
⊢ (c j • if i = (f : (a : Fin n) → ι) j then a j else 0) = 0

Tactic:
simp [hinj.symm]

Premises used: Ne.symm
-- Module: Mathlib.LinearAlgebra.FreeModule.Int
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Fintype ι
inst_3 : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis.{0, u_2, u_3} (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf :
  ∀ (i : Fin n),
    (↑((bN : (a : Fin n) → ↥N) i) : M) =
      HSMul.hSMul (β := M) (a i) ((bM : (a : ι) → M) ((f : (a : Fin n) → ι) i : ι) : M)
N' : Submodule R (ι → R) := Submodule.map (↑bM.equivFun : M →ₗ[R] ι → R) N
hN' : N' = Submodule.map (↑bM.equivFun : M →ₗ[R] ι → R) N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' :
  ∀ (i : Fin n),
    Eq (α := ι → R) ((↑((bN' : (a : Fin n) → ↥N') i) : ι → R) : ι → R)
      (Pi.single (M := fun (j : ι) ↦ R) ((f : (a : Fin n) → ι) i) (a i) : (j : ι) → R)
hNN' : N.toAddSubgroup.index = AddSubgroup.index (G := ι → R) N'.toAddSubgroup
c : Fin n → R
i : ι
h : ∃ (j : Fin n), (f : (a : Fin n) → ι) j = i
⊢ (c (h.choose (p := fun (j : Fin n) ↦ (f : (a : Fin n) → ι) j = i)) *
      if i = (f : (a : Fin n) → ι) (h.choose (p := fun (j : Fin n) ↦ (f : (a : Fin n) → ι) j = i)) then
        a (h.choose (p := fun (j : Fin n) ↦ (f : (a : Fin n) → ι) j = i))
      else 0) =
    c (h.choose (p := fun (j : Fin n) ↦ (f : (a : Fin n) → ι) j = i)) *
      a (h.choose (p := fun (j : Fin n) ↦ (f : (a : Fin n) → ι) j = i))

Tactic:
simp [h.choose_spec]

Premises used: Exists.choose_spec
-- Module: Mathlib.LinearAlgebra.FreeModule.Int
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Fintype ι
inst_3 : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis.{0, u_2, u_3} (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf :
  ∀ (i : Fin n),
    (↑((bN : (a : Fin n) → ↥N) i) : M) =
      HSMul.hSMul (β := M) (a i) ((bM : (a : ι) → M) ((f : (a : Fin n) → ι) i : ι) : M)
N' : Submodule R (ι → R) := Submodule.map (↑bM.equivFun : M →ₗ[R] ι → R) N
hN' : N' = Submodule.map (↑bM.equivFun : M →ₗ[R] ι → R) N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' :
  ∀ (i : Fin n),
    Eq (α := ι → R) ((↑((bN' : (a : Fin n) → ↥N') i) : ι → R) : ι → R)
      (Pi.single (M := fun (j : ι) ↦ R) ((f : (a : Fin n) → ι) i) (a i) : (j : ι) → R)
hNN' : N.toAddSubgroup.index = AddSubgroup.index (G := ι → R) N'.toAddSubgroup
c : Fin n → R
i : ι
h : ¬∃ (j : Fin n), (f : (a : Fin n) → ι) j = i
⊢ Dvd.dvd.{u_2} (α := R) 0 0

Tactic:
dvd_refl (0 : R)

Premises used: OfNat.ofNat, dvd_refl
-- Module: Mathlib.LinearAlgebra.FreeModule.Int
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Fintype ι
inst_3 : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis.{0, u_2, u_3} (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf :
  ∀ (i : Fin n),
    (↑((bN : (a : Fin n) → ↥N) i) : M) =
      HSMul.hSMul (β := M) (a i) ((bM : (a : ι) → M) ((f : (a : Fin n) → ι) i : ι) : M)
N' : Submodule R (ι → R) := Submodule.map (↑bM.equivFun : M →ₗ[R] ι → R) N
hN' : N' = Submodule.map (↑bM.equivFun : M →ₗ[R] ι → R) N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' :
  ∀ (i : Fin n),
    Eq (α := ι → R) ((↑((bN' : (a : Fin n) → ↥N') i) : ι → R) : ι → R)
      (Pi.single (M := fun (j : ι) ↦ R) ((f : (a : Fin n) → ι) i) (a i) : (j : ι) → R)
hNN' : N.toAddSubgroup.index = AddSubgroup.index (G := ι → R) N'.toAddSubgroup
c : Fin n → R
i : ι
h : ¬∃ (j : Fin n), (f : (a : Fin n) → ι) j = i
h₁ : Eq.{u_2 + 1} (α := R) (∑ x : Fin n, c x • if i = (f : (a : Fin n) → ι) x then a x else 0) 0
⊢ Dvd.dvd.{u_2} (α := R) 0 (∑ x : Fin n, c x • if i = (f : (a : Fin n) → ι) x then a x else 0)

Tactic:
convert! dvd_refl (0 : R)

Premises used: OfNat.ofNat, dvd_refl
-- Module: Mathlib.LinearAlgebra.FreeModule.Int
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Fintype ι
inst_3 : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis.{0, u_2, u_3} (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf :
  ∀ (i : Fin n),
    (↑((bN : (a : Fin n) → ↥N) i) : M) =
      HSMul.hSMul (β := M) (a i) ((bM : (a : ι) → M) ((f : (a : Fin n) → ι) i : ι) : M)
N' : Submodule R (ι → R) := Submodule.map (↑bM.equivFun : M →ₗ[R] ι → R) N
hN' : N' = Submodule.map (↑bM.equivFun : M →ₗ[R] ι → R) N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' :
  ∀ (i : Fin n),
    Eq (α := ι → R) ((↑((bN' : (a : Fin n) → ↥N') i) : ι → R) : ι → R)
      (Pi.single (M := fun (j : ι) ↦ R) ((f : (a : Fin n) → ι) i) (a i) : (j : ι) → R)
hNN' : N.toAddSubgroup.index = AddSubgroup.index (G := ι → R) N'.toAddSubgroup
c : Fin n → R
i : ι
h : ¬∃ (j : Fin n), (f : (a : Fin n) → ι) j = i
⊢ Eq.{u_2 + 1} (α := R) (∑ _x : Fin n, 0) 0

Tactic:
Finset.sum_const_zero

Premises used: Finset.sum_const_zero
-- Module: Mathlib.LinearAlgebra.FreeModule.Int
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Fintype ι
inst_3 : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis.{0, u_2, u_3} (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf :
  ∀ (i : Fin n),
    (↑((bN : (a : Fin n) → ↥N) i) : M) =
      HSMul.hSMul (β := M) (a i) ((bM : (a : ι) → M) ((f : (a : Fin n) → ι) i : ι) : M)
N' : Submodule R (ι → R) := Submodule.map (↑bM.equivFun : M →ₗ[R] ι → R) N
hN' : N' = Submodule.map (↑bM.equivFun : M →ₗ[R] ι → R) N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' :
  ∀ (i : Fin n),
    Eq (α := ι → R) ((↑((bN' : (a : Fin n) → ↥N') i) : ι → R) : ι → R)
      (Pi.single (M := fun (j : ι) ↦ R) ((f : (a : Fin n) → ι) i) (a i) : (j : ι) → R)
hNN' : N.toAddSubgroup.index = AddSubgroup.index (G := ι → R) N'.toAddSubgroup
c : Fin n → R
i : ι
h : ¬∃ (j : Fin n), (f : (a : Fin n) → ι) j = i
h₁ :
  ∀ (j : Fin n),
    Membership.mem (γ := Finset (Fin n)) Finset.univ j → (c j • if i = (f : (a : Fin n) → ι) j then a j else 0) = 0
⊢ Eq.{u_2 + 1} (α := R) (∑ x : Fin n, c x • if i = (f : (a : Fin n) → ι) x then a x else 0) 0

Tactic:
convert! Finset.sum_const_zero with j

Premises used: Finset.sum_const_zero