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)
dsimp :
  N.toAddSubgroup.index =
    Nat.card R ^ (Fintype.card ι - n) *
      ∏ i : Fin n, AddSubgroup.index.{u_2} (G := R) (Submodule.toAddSubgroup (Ideal.span {a i}))
⊢ N.toAddSubgroup.index =
    Nat.card R ^ (Fintype.card ι - n) *
      ∏ i : Fin n,
        AddSubgroup.index.{u_2} (G := R)
          (Submodule.toAddSubgroup
            (Ideal.span {{ bM := bM, bN := bN, f := f, a := a, snf := snf : SmithNormalForm N ι n }.a i}))

Tactic:
dsimp only
-- 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)
⊢ let N' := Submodule.map (↑bM.equivFun : M →ₗ[R] ι → R) N;
  N' = Submodule.map (↑bM.equivFun : M →ₗ[R] ι → R) N

Tactic:
set N' : Submodule R (ι → R) := N.map bM.equivFun.toLinearMap with hN'

Premises used: Submodule, LinearEquiv.toLinearMap, Submodule.map, Module.Basis.equivFun
-- 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)
i : Fin n
simp :
  Eq (α := ι → R) ((↑((bM.equivFun.submoduleMap N : (a : ↥N) → ↥N') ((bN : (a : Fin n) → ↥N) i)) : ι → R) : ι → R)
    (Pi.single (M := fun (j : ι) ↦ R) ((f : (a : Fin n) → ι) i) (a i) : (j : ι) → R)
⊢ 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)

Tactic:
simp only [map_apply, bN']

Premises used: Module.Basis.map_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)
i : Fin n
rw :
  Eq (α := ι → R) ((bM.equivFun : (a : M) → ι → R) (↑((bN : (a : Fin n) → ↥N) i) : M) : ι → R)
    (Pi.single (M := fun (j : ι) ↦ R) ((f : (a : Fin n) → ι) i) (a i) : (j : ι) → R)
⊢ Eq (α := ι → R) ((↑((bM.equivFun.submoduleMap N : (a : ↥N) → ↥N') ((bN : (a : Fin n) → ↥N) i)) : ι → R) : ι → R)
    (Pi.single (M := fun (j : ι) ↦ R) ((f : (a : Fin n) → ι) i) (a i) : (j : ι) → R)

Tactic:
rw [LinearEquiv.submoduleMap_apply]

Premises used: LinearEquiv.submoduleMap_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)
i : Fin n
simp :
  HSMul.hSMul (β := ι → R) (a i) (Pi.single (M := fun (j : ι) ↦ R) ((f : (a : Fin n) → ι) i) 1 : (j : ι) → R) =
    Pi.single (M := fun (j : ι) ↦ R) ((f : (a : Fin n) → ι) i) (a i)
⊢ Eq (α := ι → R) ((bM.equivFun : (a : M) → ι → R) (↑((bN : (a : Fin n) → ↥N) i) : M) : ι → R)
    (Pi.single (M := fun (j : ι) ↦ R) ((f : (a : Fin n) → ι) i) (a i) : (j : ι) → R)

Tactic:
simp only [equivFun_apply, snf, map_smul, repr_self, Finsupp.single_eq_pi_single]

Premises used: Module.Basis.equivFun_apply, Finsupp.single_eq_pi_single, Module.Basis.repr_self, map_smul
-- 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)
i : Fin n
h :
  ∀ (j : ι),
    HSMul.hSMul (β := ι → R) (a i) (Pi.single (M := fun (j : ι) ↦ R) ((f : (a : Fin n) → ι) i) 1 : (j : ι) → R) j =
      Pi.single (M := fun (j : ι) ↦ R) ((f : (a : Fin n) → ι) i) (a i) j
⊢ HSMul.hSMul (β := ι → R) (a i) (Pi.single (M := fun (j : ι) ↦ R) ((f : (a : Fin n) → ι) i) 1 : (j : ι) → R) =
    Pi.single (M := fun (j : ι) ↦ R) ((f : (a : Fin n) → ι) i) (a i)

Tactic:
ext 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)
i : Fin n
j : ι
⊢ HSMul.hSMul (β := ι → R) (a i) (Pi.single (M := fun (j : ι) ↦ R) ((f : (a : Fin n) → ι) i) 1 : (j : ι) → R) j =
    Pi.single (M := fun (j : ι) ↦ R) ((f : (a : Fin n) → ι) i) (a i) j

Tactic:
simp [Pi.single_apply]

Premises used: Pi.single_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)
⊢ ∀ (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)

Tactic:
have snf' : ∀ i, (bN' i : ι → R) = Pi.single (f i) (a i) := by
    intro i
    simp only [map_apply, bN']
    rw [LinearEquiv.submoduleMap_apply]
    simp only [equivFun_apply, snf, map_smul, repr_self, Finsupp.single_eq_pi_single]
    ext j
    simp [Pi.single_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)
⊢ let e : (ι → R) ≃+ M := (↑bM.equivFun.symm : (ι → R) ≃+ M);
  e = (↑bM.equivFun.symm : (ι → R) ≃+ M)

Tactic:
set e : (ι → R) ≃+ M := ↑bM.equivFun.symm with he

Premises used: LinearEquiv.symm, Module.Basis.equivFun
-- 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)
e : (ι → R) ≃+ M := (↑bM.equivFun.symm : (ι → R) ≃+ M)
he : e = (↑bM.equivFun.symm : (ι → R) ≃+ M)
e' : (ι → R) →+ M := (↑e : (ι → R) →+ M)
⊢ Function.Surjective (α := ι → R) (β := M) (⇑e' : (a : ι → R) → M)

Tactic:
have he' : Function.Surjective e' := e.surjective
-- 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)
e : (ι → R) ≃+ M := (↑bM.equivFun.symm : (ι → R) ≃+ M)
he : e = (↑bM.equivFun.symm : (ι → R) ≃+ M)
e' : (ι → R) →+ M := (↑e : (ι → R) →+ M)
he' : Function.Surjective (α := ι → R) (β := M) (⇑e' : (a : ι → R) → M)
⊢ N.toAddSubgroup.index = AddSubgroup.index (G := ι → R) (AddSubgroup.comap e' N.toAddSubgroup)

Tactic:
(AddSubgroup.index_comap_of_surjective N.toAddSubgroup he').symm

Premises used: AddSubgroup.index_comap_of_surjective, Submodule.toAddSubgroup, Eq.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)
e : (ι → R) ≃+ M := (↑bM.equivFun.symm : (ι → R) ≃+ M)
he : e = (↑bM.equivFun.symm : (ι → R) ≃+ M)
e' : (ι → R) →+ M := (↑e : (ι → R) →+ M)
he' : Function.Surjective (α := ι → R) (β := M) (⇑e' : (a : ι → R) → M)
h :
  Eq (α := AddGroup (ι → R)) AddCommGroup.toAddGroup (Pi.addGroup (f := fun (a : ι) ↦ R)) →
    Eq (α := AddSubgroup (ι → R)) N'.toAddSubgroup (AddSubgroup.comap e' N.toAddSubgroup)
⊢ N.toAddSubgroup.index = AddSubgroup.index (G := ι → R) N'.toAddSubgroup

Tactic:
convert! (AddSubgroup.index_comap_of_surjective N.toAddSubgroup he').symm using 2

Premises used: AddSubgroup.index_comap_of_surjective, Submodule.toAddSubgroup, Eq.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)
e : (ι → R) ≃+ M := (↑bM.equivFun.symm : (ι → R) ≃+ M)
he : e = (↑bM.equivFun.symm : (ι → R) ≃+ M)
e' : (ι → R) →+ M := (↑e : (ι → R) →+ M)
he' : Function.Surjective (α := ι → R) (β := M) (⇑e' : (a : ι → R) → M)
e_2 : Eq (α := AddGroup (ι → R)) AddCommGroup.toAddGroup (Pi.addGroup (f := fun (a : ι) ↦ R))
h :
  Eq (α := AddSubgroup (ι → R)) (Submodule.map (↑bM.equivFun : M →ₗ[R] ι → R) N).toAddSubgroup
    (AddSubgroup.map (↑(↑bM.equivFun : M ≃+ (ι → R)) : M →+ ι → R) N.toAddSubgroup)
⊢ Eq (α := AddSubgroup (ι → R)) N'.toAddSubgroup (AddSubgroup.comap e' N.toAddSubgroup)

Tactic:
rw [AddSubgroup.comap_equiv_eq_map_symm, he, hN', LinearEquiv.coe_toAddEquiv_symm,
    AddEquiv.symm_symm]

Premises used: AddSubgroup.comap_equiv_eq_map_symm, LinearEquiv.coe_toAddEquiv_symm, AddEquiv.symm_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)
e : (ι → R) ≃+ M := (↑bM.equivFun.symm : (ι → R) ≃+ M)
he : e = (↑bM.equivFun.symm : (ι → R) ≃+ M)
e' : (ι → R) →+ M := (↑e : (ι → R) →+ M)
he' : Function.Surjective (α := ι → R) (β := M) (⇑e' : (a : ι → R) → M)
e_2 : Eq (α := AddGroup (ι → R)) AddCommGroup.toAddGroup (Pi.addGroup (f := fun (a : ι) ↦ R))
⊢ Eq (α := AddSubgroup (ι → R)) (Submodule.map (↑bM.equivFun : M →ₗ[R] ι → R) N).toAddSubgroup
    (AddSubgroup.map (↑(↑bM.equivFun : M ≃+ (ι → R)) : M →+ ι → R) N.toAddSubgroup)

Tactic:
Submodule.map_toAddSubgroup ..

Premises used: AddMonoidHomClass.toAddMonoidHom, AddEquivClass.toAddEquiv, Submodule.map_toAddSubgroup
-- 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)
e : (ι → R) ≃+ M := (↑bM.equivFun.symm : (ι → R) ≃+ M)
he : e = (↑bM.equivFun.symm : (ι → R) ≃+ M)
e' : (ι → R) →+ M := (↑e : (ι → R) →+ M)
he' : Function.Surjective (α := ι → R) (β := M) (⇑e' : (a : ι → R) → M)
e_2 : Eq (α := AddGroup (ι → R)) AddCommGroup.toAddGroup (Pi.addGroup (f := fun (a : ι) ↦ R))
⊢ Eq (α := AddSubgroup (ι → R)) (Submodule.map (↑bM.equivFun : M →ₗ[R] ι → R) N).toAddSubgroup
    (AddSubgroup.map (↑(↑bM.equivFun : M ≃+ (ι → R)) : M →+ ι → R) N.toAddSubgroup)

Tactic:
exact Submodule.map_toAddSubgroup ..

Premises used: Submodule.map_toAddSubgroup
-- 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)
⊢ N.toAddSubgroup.index = AddSubgroup.index (G := ι → R) N'.toAddSubgroup

Tactic:
have hNN' : N.toAddSubgroup.index = N'.toAddSubgroup.index := by
    set e : (ι → R) ≃+ M := ↑bM.equivFun.symm with he
    let e' : (ι → R) →+ M := e
    have he' : Function.Surjective e' := e.surjective
    convert! (AddSubgroup.index_comap_of_surjective N.toAddSubgroup he').symm using 2
    rw [AddSubgroup.comap_equiv_eq_map_symm, he, hN', LinearEquiv.coe_toAddEquiv_symm,
    AddEquiv.symm_symm]
    exact Submodule.map_toAddSubgroup ..
-- 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
rw :
  AddSubgroup.index (G := ι → R) N'.toAddSubgroup =
    Nat.card R ^ (Fintype.card ι - n) *
      ∏ i : Fin n, AddSubgroup.index.{u_2} (G := R) (Submodule.toAddSubgroup (Ideal.span {a i}))
⊢ N.toAddSubgroup.index =
    Nat.card R ^ (Fintype.card ι - n) *
      ∏ i : Fin n, AddSubgroup.index.{u_2} (G := R) (Submodule.toAddSubgroup (Ideal.span {a i}))

Tactic:
rw [hNN']
-- 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
h :
  ∀ (g : ι → R),
    Membership.mem (γ := AddSubgroup (ι → R)) N'.toAddSubgroup g ↔
      Membership.mem (γ := AddSubgroup (ι → R))
        (AddSubgroup.pi (f := fun (i : ι) ↦ R) Set.univ fun (i : ι) ↦
          Submodule.toAddSubgroup
            (Ideal.span
              {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
⊢ Eq (α := AddSubgroup (ι → R)) N'.toAddSubgroup
    (AddSubgroup.pi (f := fun (i : ι) ↦ R) Set.univ fun (i : ι) ↦
      Submodule.toAddSubgroup
        (Ideal.span
          {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}))

Tactic:
ext g
-- 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)) ↔
    ∀ (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
⊢ Membership.mem (γ := AddSubgroup (ι → R)) N'.toAddSubgroup g ↔
    Membership.mem (γ := AddSubgroup (ι → R))
      (AddSubgroup.pi (f := fun (i : ι) ↦ R) Set.univ fun (i : ι) ↦
        Submodule.toAddSubgroup
          (Ideal.span
            {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

Tactic:
simp only [Submodule.mem_toAddSubgroup, bN'.mem_submodule_iff', snf', AddSubgroup.mem_pi,
      Set.mem_univ, true_implies, Ideal.mem_span_singleton]

Premises used: AddSubgroup.mem_pi, Module.Basis.mem_submodule_iff', Submodule.mem_toAddSubgroup, true_implies, Set.mem_univ, Ideal.mem_span_singleton