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
c : Fin n → R
i : ι
h : ¬∃ (j : Fin n), (f : (a : Fin n) → ι) j = i
j : Fin n
h_1 : Membership.mem (γ := Finset (Fin n)) Finset.univ j
h₁ :
  ∀ (h : ∀ (x : Fin n), ¬(f : (a : Fin n) → ι) x = i) (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
⊢ (c j • if i = (f : (a : Fin n) → ι) j then a j else 0) = 0

Tactic:
rw [not_exists] at h

Premises used: not_exists
-- 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 : ∀ (x : Fin n), ¬(f : (a : Fin n) → ι) x = i
j : Fin n
h_1 : Membership.mem (γ := Finset (Fin n)) Finset.univ j
⊢ ¬(f : (a : Fin n) → ι) j = i

Tactic:
specialize h j
-- 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 : ι
j : Fin n
h_1 : Membership.mem (γ := Finset (Fin n)) Finset.univ j
h : ¬(f : (a : Fin n) → ι) j = i
⊢ ¬i = (f : (a : Fin n) → ι) j

Tactic:
rw [eq_comm] at h

Premises used: eq_comm
-- 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 : ι
j : Fin n
h_1 : Membership.mem (γ := Finset (Fin n)) Finset.univ j
h : ¬i = (f : (a : Fin n) → ι) j
⊢ (c j • if i = (f : (a : Fin n) → ι) j then a j else 0) = 0

Tactic:
simp [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 :
  ∀ (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)

Tactic:
⟨fun j ↦ (h (f j)).choose, ?_⟩

Premises used: Exists.intro, Exists.choose, DFunLike.coe
-- 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 :
  ∀ (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₁ :
  g =
    ∑ x : Fin n,
      HSMul.hSMul (α := R) (β := ι → R)
        ((fun (j : Fin n) ↦
            Exists.choose (p := fun (c : R) ↦
              g ((f : (a : Fin n) → ι) j) =
                (if h : ∃ (j_1 : Fin n), Eq (α := ι) ((f : (a : Fin n) → ι) j_1 : ι) ((f : (a : Fin n) → ι) j : ι) then
                    a
                      (h.choose (p := fun (j_1 : Fin n) ↦
                        Eq (α := ι) ((f : (a : Fin n) → ι) j_1 : ι) ((f : (a : Fin n) → ι) j : ι)))
                  else 0) *
                  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)

Tactic:
refine ⟨fun j ↦ (h (f j)).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
g : ι → R
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
h₁ :
  ∀ (i : ι),
    g i =
      (∑ x : Fin n,
          HSMul.hSMul (α := R) (β := ι → R)
            ((fun (j : Fin n) ↦
                Exists.choose (p := fun (c : R) ↦
                  g ((f : (a : Fin n) → ι) j) =
                    (if h :
                          ∃ (j_1 : Fin n),
                            Eq (α := ι) ((f : (a : Fin n) → ι) j_1 : ι) ((f : (a : Fin n) → ι) j : ι) then
                        a
                          (h.choose (p := fun (j_1 : Fin n) ↦
                            Eq (α := ι) ((f : (a : Fin n) → ι) j_1 : ι) ((f : (a : Fin n) → ι) j : ι)))
                      else 0) *
                      c)
                  ⋯)
              x)
            (Pi.single (M := fun (j : ι) ↦ R) ((f : (a : Fin n) → ι) x) (a x) : (j : ι) → R))
        i
⊢ g =
    ∑ x : Fin n,
      HSMul.hSMul (α := R) (β := ι → R)
        ((fun (j : Fin n) ↦
            Exists.choose (p := fun (c : R) ↦
              g ((f : (a : Fin n) → ι) j) =
                (if h : ∃ (j_1 : Fin n), Eq (α := ι) ((f : (a : Fin n) → ι) j_1 : ι) ((f : (a : Fin n) → ι) j : ι) then
                    a
                      (h.choose (p := fun (j_1 : Fin n) ↦
                        Eq (α := ι) ((f : (a : Fin n) → ι) j_1 : ι) ((f : (a : Fin n) → ι) j : ι)))
                  else 0) *
                  c)
              ⋯)
          x)
        (Pi.single (M := fun (j : ι) ↦ R) ((f : (a : Fin n) → ι) x) (a x) : (j : ι) → R)

Tactic:
ext i
-- 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 :
  ∀ (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
i : ι
h₁ :
  g i =
    ∑ x : Fin n,
      if i = (f : (a : Fin n) → ι) x then
        Exists.choose (p := fun (c : R) ↦ g ((f : (a : Fin n) → ι) x) = a x * c) ⋯ • a x
      else 0
⊢ g i =
    (∑ x : Fin n,
        HSMul.hSMul (α := R) (β := ι → R)
          ((fun (j : Fin n) ↦
              Exists.choose (p := fun (c : R) ↦
                g ((f : (a : Fin n) → ι) j) =
                  (if h :
                        ∃ (j_1 : Fin n), Eq (α := ι) ((f : (a : Fin n) → ι) j_1 : ι) ((f : (a : Fin n) → ι) j : ι) then
                      a
                        (h.choose (p := fun (j_1 : Fin n) ↦
                          Eq (α := ι) ((f : (a : Fin n) → ι) j_1 : ι) ((f : (a : Fin n) → ι) j : ι)))
                    else 0) *
                    c)
                ⋯)
            x)
          (Pi.single (M := fun (j : ι) ↦ R) ((f : (a : Fin n) → ι) x) (a x) : (j : ι) → R))
      i

Tactic:
simp only [EmbeddingLike.apply_eq_iff_eq, exists_eq, ↓reduceDIte, Classical.choose_eq,
        Finset.sum_apply, Pi.smul_apply, Pi.single_apply, smul_ite, smul_zero]

Premises used: Pi.single_apply, Finset.sum_apply, smul_zero, reduceDIte, exists_eq, EmbeddingLike.apply_eq_iff_eq, smul_ite, Classical.choose_eq, 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
g : ι → R
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
i : ι
h₁ :
  (∑ x : Fin n,
      if i = (f : (a : Fin n) → ι) x then
        Exists.choose (p := fun (c : R) ↦ g ((f : (a : Fin n) → ι) x) = a x * c) ⋯ • a x
      else 0) =
    g i
⊢ g i =
    ∑ x : Fin n,
      if i = (f : (a : Fin n) → ι) x then
        Exists.choose (p := fun (c : R) ↦ g ((f : (a : Fin n) → ι) x) = a x * c) ⋯ • a x
      else 0

Tactic:
rw [eq_comm]

Premises used: eq_comm
-- 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 :
  ∀ (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
i : ι
pos :
  ∀ (hj : ∃ (j : Fin n), (f : (a : Fin n) → ι) j = i),
    (∑ x : Fin n,
        if i = (f : (a : Fin n) → ι) x then
          Exists.choose (p := fun (c : R) ↦ g ((f : (a : Fin n) → ι) x) = a x * c) ⋯ • a x
        else 0) =
      g i
neg :
  ∀ (hj : ∀ (j : Fin n), (f : (a : Fin n) → ι) j ≠ i),
    (∑ x : Fin n,
        if i = (f : (a : Fin n) → ι) x then
          Exists.choose (p := fun (c : R) ↦ g ((f : (a : Fin n) → ι) x) = a x * c) ⋯ • a x
        else 0) =
      g i
⊢ (∑ x : Fin n,
      if i = (f : (a : Fin n) → ι) x then
        Exists.choose (p := fun (c : R) ↦ g ((f : (a : Fin n) → ι) x) = a x * c) ⋯ • a x
      else 0) =
    g i

Tactic:
by_cases! hj : ∃ j, f j = i
-- 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 :
  ∀ (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
i : ι
hj : ∃ (j : Fin n), (f : (a : Fin n) → ι) j = i
⊢ (∑ x : Fin n,
      if i = (f : (a : Fin n) → ι) x then
        Exists.choose (p := fun (c : R) ↦ g ((f : (a : Fin n) → ι) x) = a x * c) ⋯ • a x
      else 0) =
    if i = (f : (a : Fin n) → ι) (hj.choose (p := fun (j : Fin n) ↦ (f : (a : Fin n) → ι) j = i)) then
      Exists.choose (p := fun (c : R) ↦
          g ((f : (a : Fin n) → ι) (hj.choose (p := fun (j : Fin n) ↦ (f : (a : Fin n) → ι) j = i))) =
            a (hj.choose (p := fun (j : Fin n) ↦ (f : (a : Fin n) → ι) j = i)) * c)
          ⋯ •
        a (hj.choose (p := fun (j : Fin n) ↦ (f : (a : Fin n) → ι) j = i))
    else 0

Tactic:
Finset.sum_eq_single (M := R) hj.choose ?_ ?_

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
g : ι → R
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
i : ι
hj : ∃ (j : Fin n), (f : (a : Fin n) → ι) j = i
h_1 : i = (f : (a : Fin n) → ι) (hj.choose (p := fun (j : Fin n) ↦ (f : (a : Fin n) → ι) j = i))
x : R
⊢ (if h :
        ∃ (j : Fin n),
          Eq (α := ι) ((f : (a : Fin n) → ι) j : ι)
            ((f : (a : Fin n) → ι) (hj.choose (p := fun (j : Fin n) ↦ (f : (a : Fin n) → ι) j = i)) : ι) then
      a
        (h.choose (p := fun (j : Fin n) ↦
          Eq (α := ι) ((f : (a : Fin n) → ι) j : ι)
            ((f : (a : Fin n) → ι) (hj.choose (p := fun (j : Fin n) ↦ (f : (a : Fin n) → ι) j = i)) : ι)))
    else 0) =
    a (hj.choose (p := fun (j : Fin n) ↦ (f : (a : Fin n) → ι) j = i))

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
g : ι → R
h_1 :
  ∀ (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
i : ι
hj : ∃ (j : Fin n), (f : (a : Fin n) → ι) j = i
j : Fin n
h : j ≠ hj.choose (p := fun (j : Fin n) ↦ (f : (a : Fin n) → ι) j = i)
⊢ Ne (α := ι) ((f : (a : Fin n) → ι) j : ι)
    ((f : (a : Fin n) → ι) (hj.choose (p := fun (j : Fin n) ↦ (f : (a : Fin n) → ι) j = i)) : ι)

Tactic:
have hinj := f.injective.ne 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_1 :
  ∀ (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
i : ι
hj : ∃ (j : Fin n), (f : (a : Fin n) → ι) j = i
j : Fin n
h : j ≠ hj.choose (p := fun (j : Fin n) ↦ (f : (a : Fin n) → ι) j = i)
hinj :
  Ne (α := ι) ((f : (a : Fin n) → ι) j : ι)
    ((f : (a : Fin n) → ι) (hj.choose (p := fun (j : Fin n) ↦ (f : (a : Fin n) → ι) j = i)) : ι)
⊢ (f : (a : Fin n) → ι) j ≠ i

Tactic:
rw [hj.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
g : ι → R
h_1 :
  ∀ (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
i : ι
hj : ∃ (j : Fin n), (f : (a : Fin n) → ι) j = i
j : Fin n
h : j ≠ hj.choose (p := fun (j : Fin n) ↦ (f : (a : Fin n) → ι) j = i)
hinj : (f : (a : Fin n) → ι) j ≠ i
⊢ (if i = (f : (a : Fin n) → ι) j then Exists.choose (p := fun (c : R) ↦ g ((f : (a : Fin n) → ι) j) = a j * c) ⋯ • a j
    else 0) =
    0

Tactic:
simp [hinj.symm]

Premises used: Ne.symm