awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.FreeModule.Int
Goal:
ι : Type u_1
M : Type u_3
n : ℕ
inst : AddCommGroup M
inst_1 : Fintype ι
N : Submodule ℤ M
snf : SmithNormalForm N ι n
rcases :
  ∀ (bM : Basis ι ℤ M) (bN : Basis (Fin n) ℤ ↥N) (f : Fin n ↪ ι) (a : Fin n → ℤ)
    (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)),
    Ne (α := ℕ)
        (if n = Fintype.card ι then
          ∏ i : Fin n,
            AddSubgroup.index (G := ℤ)
              (Submodule.toAddSubgroup
                (Ideal.span {{ bM := bM, bN := bN, f := f, a := a, snf := snf : SmithNormalForm N ι n }.a i}))
        else 0)
        0 ↔
      n = Fintype.card ι
⊢ Ne (α := ℕ)
      (if n = Fintype.card ι then
        ∏ i : Fin n, AddSubgroup.index (G := ℤ) (Submodule.toAddSubgroup (Ideal.span {snf.a i}))
      else 0)
      0 ↔
    n = Fintype.card ι

Tactic:
rcases snf with ⟨bM, bN, f, a, snf⟩

Premises used: Module.Basis.SmithNormalForm.a, Module.Basis.SmithNormalForm.bM, Module.Basis.SmithNormalForm.f, Module.Basis.SmithNormalForm.bN
-- Module: Mathlib.LinearAlgebra.FreeModule.Int
Goal:
ι : Type u_1
M : Type u_3
n : ℕ
inst : AddCommGroup M
inst_1 : Fintype ι
N : Submodule ℤ M
bM : Basis ι ℤ M
bN : Basis (Fin n) ℤ ↥N
f : Fin n ↪ ι
a : Fin n → ℤ
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)
simp :
  n = Fintype.card ι →
    ¬Eq (α := ℕ) (∏ x : Fin n, AddSubgroup.index (G := ℤ) (Submodule.toAddSubgroup (Ideal.span {a x}))) 0
⊢ Ne (α := ℕ)
      (if n = Fintype.card ι then
        ∏ i : Fin n,
          AddSubgroup.index (G := ℤ)
            (Submodule.toAddSubgroup
              (Ideal.span {{ bM := bM, bN := bN, f := f, a := a, snf := snf : SmithNormalForm N ι n }.a i}))
      else 0)
      0 ↔
    n = Fintype.card ι

Tactic:
simp only [ne_eq, ite_eq_right_iff, Classical.not_imp, and_iff_left_iff_imp]

Premises used: ne_eq, ite_eq_right_iff, Classical.not_imp, and_iff_left_iff_imp
-- Module: Mathlib.LinearAlgebra.FreeModule.Int
Goal:
ι : Type u_1
M : Type u_3
n : ℕ
inst : AddCommGroup M
inst_1 : Fintype ι
N : Submodule ℤ M
bM : Basis ι ℤ M
bN : Basis (Fin n) ℤ ↥N
f : Fin n ↪ ι
a : Fin n → ℤ
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)
i : Fin n
hi : a i = 0
apply : Eq (α := ↥N) ((bN : (a : Fin n) → ↥N) i : ↥N) (0 : ↥N)
⊢ False

Tactic:
apply Basis.ne_zero bN i

Premises used: Module.Basis.ne_zero
-- Module: Mathlib.LinearAlgebra.FreeModule.Int
Goal:
ι : Type u_1
M : Type u_3
n : ℕ
inst : AddCommGroup M
inst_1 : Fintype ι
N : Submodule ℤ M
bM : Basis ι ℤ M
bN : Basis (Fin n) ℤ ↥N
f : Fin n ↪ ι
a : Fin n → ℤ
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)
i : Fin n
hi : a i = 0
⊢ (↑((bN : (a : Fin n) → ↥N) i) : M) = HSMul.hSMul (β := M) (a i) ((bM : (a : ι) → M) ((f : (a : Fin n) → ι) i : ι) : M)

Tactic:
specialize snf i
-- Module: Mathlib.LinearAlgebra.FreeModule.Int
Goal:
ι : Type u_1
M : Type u_3
n : ℕ
inst : AddCommGroup M
inst_1 : Fintype ι
N : Submodule ℤ M
bM : Basis ι ℤ M
bN : Basis (Fin n) ℤ ↥N
f : Fin n ↪ ι
a : Fin n → ℤ
i : Fin n
hi : a i = 0
snf :
  (↑((bN : (a : Fin n) → ↥N) i) : M) = HSMul.hSMul (β := M) (a i) ((bM : (a : ι) → M) ((f : (a : Fin n) → ι) i : ι) : M)
⊢ Eq (α := ↥N) ((bN : (a : Fin n) → ↥N) i : ↥N) (0 : ↥N)

Tactic:
simpa [hi] using snf
-- Module: Mathlib.LinearAlgebra.FreeModule.Int
Goal:
ι : Type u_1
M : Type u_3
n : ℕ
inst : AddCommGroup M
inst_1 : Fintype ι
N : Submodule ℤ M
bM : Basis ι ℤ M
bN : Basis (Fin n) ℤ ↥N
f : Fin n ↪ ι
a : Fin n → ℤ
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)
⊢ ∀ (i : Fin n), a i ≠ 0

Tactic:
have ha : ∀ i, a i ≠ 0 := by
    intro i hi
    apply Basis.ne_zero bN i
    specialize snf i
    simpa [hi] using snf
-- Module: Mathlib.LinearAlgebra.FreeModule.Int
Goal:
ι : Type u_1
M : Type u_3
n : ℕ
inst : AddCommGroup M
inst_1 : Fintype ι
N : Submodule ℤ M
bM : Basis ι ℤ M
bN : Basis (Fin n) ℤ ↥N
f : Fin n ↪ ι
a : Fin n → ℤ
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)
ha : ∀ (i : Fin n), a i ≠ 0
h : n = Fintype.card ι
⊢ ¬Eq (α := ℕ) (∏ x : Fin n, AddSubgroup.index (G := ℤ) (Submodule.toAddSubgroup (Ideal.span {a x}))) 0

Tactic:
simpa [Ideal.span_singleton_toAddSubgroup_eq_zmultiples, Int.index_zmultiples,
    Finset.prod_eq_zero_iff] using ha

Premises used: Ideal.span_singleton_toAddSubgroup_eq_zmultiples, Finset.prod_eq_zero_iff, Int.index_zmultiples
-- Module: Mathlib.LinearAlgebra.FreeModule.Int
Goal:
ι : Type u_1
inst : Finite ι
N : Submodule ℤ (ι → ℤ)
obtain :
  ∀ (n : ℕ) (snf : Module.Basis.SmithNormalForm N ι n), N.toAddSubgroup.index ≠ 0 ↔ Nonempty.{u_1 + 1} (↥N ≃ₗ[ℤ] ι → ℤ)
⊢ N.toAddSubgroup.index ≠ 0 ↔ Nonempty.{u_1 + 1} (↥N ≃ₗ[ℤ] ι → ℤ)

Tactic:
obtain ⟨n, snf⟩ := N.smithNormalForm <| .ofEquivFun <| .refl ..

Premises used: Submodule.smithNormalForm
-- Module: Mathlib.LinearAlgebra.FreeModule.Int
Goal:
ι : Type u_1
inst : Finite ι
N : Submodule ℤ (ι → ℤ)
n : ℕ
snf : Module.Basis.SmithNormalForm N ι n
have : ∀ (this : Fintype ι), N.toAddSubgroup.index ≠ 0 ↔ Nonempty.{u_1 + 1} (↥N ≃ₗ[ℤ] ι → ℤ)
⊢ N.toAddSubgroup.index ≠ 0 ↔ Nonempty.{u_1 + 1} (↥N ≃ₗ[ℤ] ι → ℤ)

Tactic:
have := Fintype.ofFinite ι
-- Module: Mathlib.LinearAlgebra.FreeModule.Int
Goal:
ι : Type u_1
inst : Finite ι
N : Submodule ℤ (ι → ℤ)
n : ℕ
snf : Module.Basis.SmithNormalForm N ι n
this : Fintype ι
rw : n = Fintype.card ι ↔ Nonempty.{u_1 + 1} (↥N ≃ₗ[ℤ] ι → ℤ)
⊢ N.toAddSubgroup.index ≠ 0 ↔ Nonempty.{u_1 + 1} (↥N ≃ₗ[ℤ] ι → ℤ)

Tactic:
rw [snf.toAddSubgroup_index_ne_zero_iff]

Premises used: Module.Basis.SmithNormalForm.toAddSubgroup_index_ne_zero_iff
-- Module: Mathlib.LinearAlgebra.FreeModule.Int
Goal:
ι : Type u_1
inst : Finite ι
N : Submodule ℤ (ι → ℤ)
n : ℕ
snf : Module.Basis.SmithNormalForm N ι n
this : Fintype ι
rcases : ∀ (bN : Module.Basis (Fin n) ℤ ↥N), n = Fintype.card ι ↔ Nonempty.{u_1 + 1} (↥N ≃ₗ[ℤ] ι → ℤ)
⊢ n = Fintype.card ι ↔ Nonempty.{u_1 + 1} (↥N ≃ₗ[ℤ] ι → ℤ)

Tactic:
rcases snf with ⟨-, bN, -, -, -⟩
-- Module: Mathlib.LinearAlgebra.FreeModule.Int
Goal:
ι : Type u_1
inst : Finite ι
N : Submodule ℤ (ι → ℤ)
n : ℕ
this : Fintype ι
bN : Module.Basis (Fin n) ℤ ↥N
⊢ n = Fintype.card ι ↔ Nonempty.{u_1 + 1} (↥N ≃ₗ[ℤ] ι → ℤ)

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

Premises used: Fintype.card, Iff.intro, Eq, _private.0.Int.submodule_toAddSubgroup_index_ne_zero_iff.match_1
-- Module: Mathlib.LinearAlgebra.FreeModule.Int
Goal:
ι : Type u_1
inst : Finite ι
N : Submodule ℤ (ι → ℤ)
n : ℕ
this : Fintype ι
bN : Module.Basis (Fin n) ℤ ↥N
refine_1 : ∀ (h : n = Fintype.card ι), Nonempty.{u_1 + 1} (↥N ≃ₗ[ℤ] ι → ℤ)
refine_2 : Nonempty.{u_1 + 1} (↥N ≃ₗ[ℤ] ι → ℤ) → ∀ (e : ↥N ≃ₗ[ℤ] ι → ℤ), n = Fintype.card ι
⊢ n = Fintype.card ι ↔ Nonempty.{u_1 + 1} (↥N ≃ₗ[ℤ] ι → ℤ)

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨e⟩ ↦ ?_⟩
-- Module: Mathlib.LinearAlgebra.FreeModule.Int
Goal:
ι : Type u_1
inst : Finite ι
N : Submodule ℤ (ι → ℤ)
n : ℕ
this : Fintype ι
bN : Module.Basis (Fin n) ℤ ↥N
h : n = Fintype.card ι
refine_1 : ∀ (bN : Module.Basis (Fin (Fintype.card ι)) ℤ ↥N), Nonempty.{u_1 + 1} (↥N ≃ₗ[ℤ] ι → ℤ)
⊢ Nonempty.{u_1 + 1} (↥N ≃ₗ[ℤ] ι → ℤ)

Tactic:
subst h
-- Module: Mathlib.LinearAlgebra.FreeModule.Int
Goal:
ι : Type u_1
inst : Finite ι
N : Submodule ℤ (ι → ℤ)
this : Fintype ι
bN : Module.Basis (Fin (Fintype.card ι)) ℤ ↥N
⊢ Nonempty.{u_1 + 1} (↥N ≃ₗ[ℤ] ι → ℤ)

Tactic:
⟨(bN.reindex (Fintype.equivFin _).symm).equivFun⟩

Premises used: Nonempty.intro, Fintype.equivFin, Module.Basis.reindex, Equiv.symm, Module.Basis.equivFun
-- Module: Mathlib.LinearAlgebra.FreeModule.Int
Goal:
ι : Type u_1
inst : Finite ι
N : Submodule ℤ (ι → ℤ)
this : Fintype ι
bN : Module.Basis (Fin (Fintype.card ι)) ℤ ↥N
⊢ Nonempty.{u_1 + 1} (↥N ≃ₗ[ℤ] ι → ℤ)

Tactic:
exact ⟨(bN.reindex (Fintype.equivFin _).symm).equivFun⟩
-- Module: Mathlib.LinearAlgebra.FreeModule.Int
Goal:
ι : Type u_1
inst : Finite ι
N : Submodule ℤ (ι → ℤ)
n : ℕ
this : Fintype ι
bN : Module.Basis (Fin n) ℤ ↥N
h : Nonempty.{u_1 + 1} (↥N ≃ₗ[ℤ] ι → ℤ)
e : ↥N ≃ₗ[ℤ] ι → ℤ
⊢ Fintype.card (Fin n) = Fintype.card ι

Tactic:
have hc := card_eq_of_linearEquiv ℤ <| bN.equivFun.symm.trans e
-- Module: Mathlib.LinearAlgebra.FreeModule.Int
Goal:
ι : Type u_1
inst : Finite ι
N : Submodule ℤ (ι → ℤ)
n : ℕ
this : Fintype ι
bN : Module.Basis (Fin n) ℤ ↥N
h : Nonempty.{u_1 + 1} (↥N ≃ₗ[ℤ] ι → ℤ)
e : ↥N ≃ₗ[ℤ] ι → ℤ
hc : Fintype.card (Fin n) = Fintype.card ι
⊢ n = Fintype.card ι

Tactic:
simpa using hc
-- Module: Mathlib.LinearAlgebra.FreeModule.Int
Goal:
ι : Type u_1
inst : Finite ι
H : AddSubgroup (ι → ℤ)
⊢ AddSubgroup.index.{u_1} (G := ι → ℤ)
        (Submodule.toAddSubgroup (R := ℤ) (module_M := AddCommGroup.toIntModule (ι → ℤ))
          ((AddSubgroup.toIntSubmodule : (a : AddSubgroup (ι → ℤ)) → Submodule ℤ (ι → ℤ)) H)) ≠
      0 ↔
    Nonempty.{u_1 + 1}
      (↥((AddSubgroup.toIntSubmodule : (a : AddSubgroup (ι → ℤ)) → Submodule ℤ (ι → ℤ)) H : Submodule ℤ (ι → ℤ)) ≃ₗ[ℤ]
        ι → ℤ)

Tactic:
submodule_toAddSubgroup_index_ne_zero_iff (N := AddSubgroup.toIntSubmodule H)

Premises used: Int.submodule_toAddSubgroup_index_ne_zero_iff
-- Module: Mathlib.LinearAlgebra.FreeModule.Int
Goal:
ι : Type u_1
inst : Finite ι
H : AddSubgroup (ι → ℤ)
h :
  Nonempty.{u_1 + 1} (↥H ≃+ (ι → ℤ)) ↔
    Nonempty.{u_1 + 1}
      (↥((AddSubgroup.toIntSubmodule : (a : AddSubgroup (ι → ℤ)) → Submodule ℤ (ι → ℤ)) H : Submodule ℤ (ι → ℤ)) ≃ₗ[ℤ]
        ι → ℤ)
⊢ H.index ≠ 0 ↔ Nonempty.{u_1 + 1} (↥H ≃+ (ι → ℤ))

Tactic:
convert! submodule_toAddSubgroup_index_ne_zero_iff (N := AddSubgroup.toIntSubmodule H) using 1

Premises used: Int.submodule_toAddSubgroup_index_ne_zero_iff
-- Module: Mathlib.LinearAlgebra.FreeModule.Int
Goal:
ι : Type u_1
inst : Finite ι
H : AddSubgroup (ι → ℤ)
⊢ Nonempty.{u_1 + 1} (↥H ≃+ (ι → ℤ)) ↔
    Nonempty.{u_1 + 1}
      (↥((AddSubgroup.toIntSubmodule : (a : AddSubgroup (ι → ℤ)) → Submodule ℤ (ι → ℤ)) H : Submodule ℤ (ι → ℤ)) ≃ₗ[ℤ]
        ι → ℤ)

Tactic:
⟨fun ⟨e⟩ ↦ ⟨e.toIntLinearEquiv⟩, fun ⟨e⟩ ↦ ⟨e.toAddEquiv⟩⟩

Premises used: AddEquiv.toIntLinearEquiv, Membership.mem, _private.0.Int.addSubgroup_index_ne_zero_iff.match_1, Subtype, LinearEquiv.toAddEquiv, Int, Nonempty.intro, _private.0.Int.addSubgroup_index_ne_zero_iff.match_2, LinearEquiv, Iff.intro, AddEquiv, Nonempty, AddSubgroup.toIntSubmodule, RingHom.id, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.FreeModule.Int
Goal:
ι : Type u_1
inst : Finite ι
H : AddSubgroup (ι → ℤ)
⊢ Nonempty.{u_1 + 1} (↥H ≃+ (ι → ℤ)) ↔
    Nonempty.{u_1 + 1}
      (↥((AddSubgroup.toIntSubmodule : (a : AddSubgroup (ι → ℤ)) → Submodule ℤ (ι → ℤ)) H : Submodule ℤ (ι → ℤ)) ≃ₗ[ℤ]
        ι → ℤ)

Tactic:
exact ⟨fun ⟨e⟩ ↦ ⟨e.toIntLinearEquiv⟩, fun ⟨e⟩ ↦ ⟨e.toAddEquiv⟩⟩
-- Module: Mathlib.LinearAlgebra.FreeModule.Int
Goal:
ι : Type u_1
inst : Finite ι
H : Subgroup (ι → Multiplicative ℤ)
em : Multiplicative (ι → ℤ) ≃* (ι → Multiplicative ℤ) := MulEquiv.funMultiplicative ι ℤ
H' : Subgroup (Multiplicative (ι → ℤ)) := Subgroup.comap (↑em : Multiplicative (ι → ℤ) →* ι → Multiplicative ℤ) H
eH' : ↥H' ≃* ↥H := (MulEquiv.subgroupCongr ⋯).trans (em.symm.subgroupMap H).symm
⊢ H'.index = H.index

Tactic:
have h : H'.index = H.index := Subgroup.index_comap_of_surjective _ em.surjective
-- Module: Mathlib.LinearAlgebra.FreeModule.Int
Goal:
ι : Type u_1
inst : Finite ι
H : Subgroup (ι → Multiplicative ℤ)
em : Multiplicative (ι → ℤ) ≃* (ι → Multiplicative ℤ) := MulEquiv.funMultiplicative ι ℤ
H' : Subgroup (Multiplicative (ι → ℤ)) := Subgroup.comap (↑em : Multiplicative (ι → ℤ) →* ι → Multiplicative ℤ) H
eH' : ↥H' ≃* ↥H := (MulEquiv.subgroupCongr ⋯).trans (em.symm.subgroupMap H).symm
h : H'.index = H.index
rw :
  Nonempty.{u_1 + 1}
      (↥((Subgroup.toAddSubgroup :
                (a : Subgroup (Multiplicative (ι → ℤ))) → AddSubgroup (Additive (Multiplicative (ι → ℤ))))
              H' :
            AddSubgroup (Additive (Multiplicative (ι → ℤ)))) ≃+
        (ι → ℤ)) ↔
    Nonempty.{u_1 + 1} (↥H ≃* (ι → Multiplicative ℤ))
⊢ H.index ≠ 0 ↔ Nonempty.{u_1 + 1} (↥H ≃* (ι → Multiplicative ℤ))

Tactic:
rw [← h, ← Subgroup.index_toAddSubgroup, addSubgroup_index_ne_zero_iff]

Premises used: Int.addSubgroup_index_ne_zero_iff, Subgroup.index_toAddSubgroup
-- Module: Mathlib.LinearAlgebra.FreeModule.Int
Goal:
ι : Type u_1
inst : Finite ι
H : Subgroup (ι → Multiplicative ℤ)
em : Multiplicative (ι → ℤ) ≃* (ι → Multiplicative ℤ) := MulEquiv.funMultiplicative ι ℤ
H' : Subgroup (Multiplicative (ι → ℤ)) := Subgroup.comap (↑em : Multiplicative (ι → ℤ) →* ι → Multiplicative ℤ) H
eH' : ↥H' ≃* ↥H := (MulEquiv.subgroupCongr ⋯).trans (em.symm.subgroupMap H).symm
h : H'.index = H.index
⊢ Nonempty.{u_1 + 1}
      (↥((Subgroup.toAddSubgroup :
                (a : Subgroup (Multiplicative (ι → ℤ))) → AddSubgroup (Additive (Multiplicative (ι → ℤ))))
              H' :
            AddSubgroup (Additive (Multiplicative (ι → ℤ)))) ≃+
        (ι → ℤ)) ↔
    Nonempty.{u_1 + 1} (↥H ≃* (ι → Multiplicative ℤ))

Tactic:
⟨fun ⟨e⟩ ↦ ⟨(eH'.symm.trans (AddEquiv.toMultiplicative e)).trans em⟩,
    fun ⟨e⟩ ↦ ⟨(MulEquiv.toAdditive ((eH'.trans e).trans em.symm)).trans
      (AddEquiv.additiveMultiplicative _)⟩⟩

Premises used: AddEquiv.toMultiplicative, Subgroup.toAddSubgroup, MulEquiv.trans, _private.0.Int.subgroup_index_ne_zero_iff.match_1, Membership.mem, Subtype, Nonempty.intro, _private.0.Int.subgroup_index_ne_zero_iff.match_2, AddEquiv.additiveMultiplicative, AddEquiv.trans, Iff.intro, AddEquiv, Nonempty, MulEquiv, MulEquiv.symm, DFunLike.coe, MulEquiv.toAdditive
-- Module: Mathlib.LinearAlgebra.FreeModule.Int
Goal:
ι : Type u_1
inst : Finite ι
H : Subgroup (ι → Multiplicative ℤ)
em : Multiplicative (ι → ℤ) ≃* (ι → Multiplicative ℤ) := MulEquiv.funMultiplicative ι ℤ
H' : Subgroup (Multiplicative (ι → ℤ)) := Subgroup.comap (↑em : Multiplicative (ι → ℤ) →* ι → Multiplicative ℤ) H
eH' : ↥H' ≃* ↥H := (MulEquiv.subgroupCongr ⋯).trans (em.symm.subgroupMap H).symm
h : H'.index = H.index
⊢ Nonempty.{u_1 + 1}
      (↥((Subgroup.toAddSubgroup :
                (a : Subgroup (Multiplicative (ι → ℤ))) → AddSubgroup (Additive (Multiplicative (ι → ℤ))))
              H' :
            AddSubgroup (Additive (Multiplicative (ι → ℤ)))) ≃+
        (ι → ℤ)) ↔
    Nonempty.{u_1 + 1} (↥H ≃* (ι → Multiplicative ℤ))

Tactic:
exact ⟨fun ⟨e⟩ ↦ ⟨(eH'.symm.trans (AddEquiv.toMultiplicative e)).trans em⟩,
    fun ⟨e⟩ ↦ ⟨(MulEquiv.toAdditive ((eH'.trans e).trans em.symm)).trans
      (AddEquiv.additiveMultiplicative _)⟩⟩
-- Module: Mathlib.LinearAlgebra.FreeModule.ModN
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
inst : AddCommGroup G
n : ℕ
⊢ ∀ (x : G),
    Membership.mem (γ := AddSubgroup G)
      (Submodule.toAddSubgroup (R := ℤ) (module_M := AddCommGroup.toIntModule G)
        (LinearMap.range (R := ℤ) (M := G) (τ₁₂ := RingHom.id ℤ)
          ((LinearMap.lsmul ℤ G : (a : ℤ) → G →ₗ[ℤ] G) (↑n : ℤ))))
      (n • x)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.FreeModule.ModN
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
inst : AddCommGroup G
n : ℕ
inst_1 : AddMonoid M
f : AddMonoidHom.{u_1, u_3} (ModN G n) M
g : G
Gn : AddSubgroup G :=
  Submodule.toAddSubgroup (R := ℤ) (module_M := AddCommGroup.toIntModule G)
    (LinearMap.range (R := ℤ) (M := G) (τ₁₂ := RingHom.id ℤ) ((LinearMap.lsmul ℤ G : (a : ℤ) → G →ₗ[ℤ] G) (↑n : ℤ)))
this : n • g ∈ AddMonoidHom.ker (QuotientAddGroup.mk' Gn)
simp :
  Eq.{u_3 + 1} (α := M)
    ((f : (a : ModN G n) → M)
        ((QuotientAddGroup.mk'
                (Submodule.toAddSubgroup (R := ℤ) (module_M := AddCommGroup.toIntModule G)
                  (LinearMap.range (R := ℤ) (M := G) (τ₁₂ := RingHom.id ℤ)
                    ((LinearMap.lsmul ℤ G : (a : ℤ) → G →ₗ[ℤ] G) (↑n : ℤ)))) :
              (a : G) → ModN G n)
            (n • g) :
          ModN G n) :
      M)
    (0 : M)
⊢ HSMul.hSMul (β := M) n
      ((f.comp
              (QuotientAddGroup.mk'
                (Submodule.toAddSubgroup (R := ℤ) (module_M := AddCommGroup.toIntModule G)
                  (LinearMap.range (R := ℤ) (M := G) (τ₁₂ := RingHom.id ℤ)
                    ((LinearMap.lsmul ℤ G : (a : ℤ) → G →ₗ[ℤ] G) (↑n : ℤ))))) :
            (a : G) → M)
          g :
        M) =
    0

Tactic:
simp only [AddMonoidHom.coe_comp, comp_apply, ← map_nsmul]

Premises used: AddMonoidHom.coe_comp, Function.comp_apply, map_nsmul
-- Module: Mathlib.LinearAlgebra.FreeModule.ModN
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
inst : AddCommGroup G
n : ℕ
inst_1 : AddMonoid M
f : AddMonoidHom.{u_1, u_3} (ModN G n) M
g : G
Gn : AddSubgroup G :=
  Submodule.toAddSubgroup (R := ℤ) (module_M := AddCommGroup.toIntModule G)
    (LinearMap.range (R := ℤ) (M := G) (τ₁₂ := RingHom.id ℤ) ((LinearMap.lsmul ℤ G : (a : ℤ) → G →ₗ[ℤ] G) (↑n : ℤ)))
this : n • g ∈ AddMonoidHom.ker (QuotientAddGroup.mk' Gn)
change :
  Eq.{u_3 + 1} (α := M) ((f : (a : ModN G n) → M) ((QuotientAddGroup.mk' Gn : (a : G) → G ⧸ Gn) (n • g) : G ⧸ Gn) : M)
    (0 : M)
⊢ Eq.{u_3 + 1} (α := M)
    ((f : (a : ModN G n) → M)
        ((QuotientAddGroup.mk'
                (Submodule.toAddSubgroup (R := ℤ) (module_M := AddCommGroup.toIntModule G)
                  (LinearMap.range (R := ℤ) (M := G) (τ₁₂ := RingHom.id ℤ)
                    ((LinearMap.lsmul ℤ G : (a : ℤ) → G →ₗ[ℤ] G) (↑n : ℤ)))) :
              (a : G) → ModN G n)
            (n • g) :
          ModN G n) :
      M)
    (0 : M)

Tactic:
change f (QuotientAddGroup.mk' Gn (n • g)) = 0

Premises used: QuotientAddGroup.mk', HSMul.hSMul, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.FreeModule.ModN
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
inst : AddCommGroup G
n : ℕ
inst_1 : AddMonoid M
f : AddMonoidHom.{u_1, u_3} (ModN G n) M
g : G
Gn : AddSubgroup G :=
  Submodule.toAddSubgroup (R := ℤ) (module_M := AddCommGroup.toIntModule G)
    (LinearMap.range (R := ℤ) (M := G) (τ₁₂ := RingHom.id ℤ) ((LinearMap.lsmul ℤ G : (a : ℤ) → G →ₗ[ℤ] G) (↑n : ℤ)))
this : n • g ∈ AddMonoidHom.ker (QuotientAddGroup.mk' Gn)
rw : Eq.{u_3 + 1} (α := M) ((f : (a : ModN G n) → M) 0 : M) (0 : M)
rw₁ rw₂ : Eq.{u_3 + 1} (α := M) 0 0
⊢ Eq.{u_3 + 1} (α := M) ((f : (a : ModN G n) → M) ((QuotientAddGroup.mk' Gn : (a : G) → G ⧸ Gn) (n • g) : G ⧸ Gn) : M)
    (0 : M)

Tactic:
rw [this, map_zero]

Premises used: map_zero
-- Module: Mathlib.LinearAlgebra.FreeModule.ModN
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
inst : AddCommGroup G
n : ℕ
inst_1 : AddMonoid M
f : AddMonoidHom.{u_1, u_3} (ModN G n) M
g : G
Gn : AddSubgroup G :=
  Submodule.toAddSubgroup (R := ℤ) (module_M := AddCommGroup.toIntModule G)
    (LinearMap.range (R := ℤ) (M := G) (τ₁₂ := RingHom.id ℤ) ((LinearMap.lsmul ℤ G : (a : ℤ) → G →ₗ[ℤ] G) (↑n : ℤ)))
suffices : n • g ∈ AddMonoidHom.ker (QuotientAddGroup.mk' Gn)
⊢ HSMul.hSMul (β := M) n
      ((f.comp
              (QuotientAddGroup.mk'
                (Submodule.toAddSubgroup (R := ℤ) (module_M := AddCommGroup.toIntModule G)
                  (LinearMap.range (R := ℤ) (M := G) (τ₁₂ := RingHom.id ℤ)
                    ((LinearMap.lsmul ℤ G : (a : ℤ) → G →ₗ[ℤ] G) (↑n : ℤ))))) :
            (a : G) → M)
          g :
        M) =
    0

Tactic:
suffices n • g ∈ (QuotientAddGroup.mk' Gn).ker by
      simp only [AddMonoidHom.coe_comp, comp_apply, ← map_nsmul]
      change f (QuotientAddGroup.mk' Gn (n • g)) = 0 -- Can we avoid `change`?
      rw [this, map_zero]
-- Module: Mathlib.LinearAlgebra.FreeModule.ModN
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
inst : AddCommGroup G
n : ℕ
inst_1 : AddMonoid M
f : AddMonoidHom.{u_1, u_3} (ModN G n) M
g : G
Gn : AddSubgroup G :=
  Submodule.toAddSubgroup (R := ℤ) (module_M := AddCommGroup.toIntModule G)
    (LinearMap.range (R := ℤ) (M := G) (τ₁₂ := RingHom.id ℤ) ((LinearMap.lsmul ℤ G : (a : ℤ) → G →ₗ[ℤ] G) (↑n : ℤ)))
⊢ n • g ∈ AddMonoidHom.ker (QuotientAddGroup.mk' Gn)

Tactic:
simp [QuotientAddGroup.ker_mk', Gn]

Premises used: QuotientAddGroup.ker_mk'
-- Module: Mathlib.LinearAlgebra.FreeModule.ModN
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
inst : AddCommGroup G
n : ℕ
inst_1 : AddMonoid M
φ : { φ : G →+ M // ∀ (g : G), HSMul.hSMul (β := M) n ((φ : (a : G) → M) g : M) = 0 }
g : G
⊢ Membership.mem (α := G) (↑φ : G →+ M).ker
    ((((LinearMap.lsmul ℤ G : (a : ℤ) → G →ₗ[ℤ] G) (↑n : ℤ) : G →ₗ[ℤ] G) : (a : G) → G) g : G)

Tactic:
simpa using φ.property g

Premises used: Subtype.property
-- Module: Mathlib.LinearAlgebra.FreeModule.ModN
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
inst : AddCommGroup G
n : ℕ
inst_1 : AddMonoid M
f : AddMonoidHom.{u_1, u_3} (ModN G n) M
z : G
⊢ Eq.{u_3 + 1} (α := M)
    (((fun (φ : { φ : G →+ M // ∀ (g : G), HSMul.hSMul (β := M) n ((φ : (a : G) → M) g : M) = 0 }) ↦
              (QuotientAddGroup.lift
                  (Submodule.toAddSubgroup (R := ℤ) (module_M := AddCommGroup.toIntModule G)
                    (LinearMap.range (R := ℤ) (M := G) (τ₁₂ := RingHom.id ℤ)
                      ((LinearMap.lsmul ℤ G : (a : ℤ) → G →ₗ[ℤ] G) (↑n : ℤ))))
                  (↑φ : G →+ M) ⋯ :
                AddMonoidHom.{u_1, u_3}
                  (HasQuotient.Quotient G (B := AddSubgroup G)
                    (Submodule.toAddSubgroup (R := ℤ) (module_M := AddCommGroup.toIntModule G)
                      (LinearMap.range (R := ℤ) (M := G) (τ₁₂ := RingHom.id ℤ)
                        ((LinearMap.lsmul ℤ G : (a : ℤ) → G →ₗ[ℤ] G) (↑n : ℤ)))))
                  M))
            ((fun (f : AddMonoidHom.{u_1, u_3} (ModN G n) M) ↦
                (Subtype.mk (p := fun (φ : G →+ M) ↦ ∀ (g : G), HSMul.hSMul (β := M) n ((φ : (a : G) → M) g : M) = 0)
                    (f.comp
                      (QuotientAddGroup.mk'
                        (Submodule.toAddSubgroup (R := ℤ) (module_M := AddCommGroup.toIntModule G)
                          (LinearMap.range (R := ℤ) (M := G) (τ₁₂ := RingHom.id ℤ)
                            ((LinearMap.lsmul ℤ G : (a : ℤ) → G →ₗ[ℤ] G) (↑n : ℤ))))))
                    ⋯ :
                  { φ : G →+ M // ∀ (g : G), HSMul.hSMul (β := M) n ((φ : (a : G) → M) g : M) = 0 }))
              f) :
          (a : G ⧸ ((LinearMap.lsmul ℤ G : (a : ℤ) → G →ₗ[ℤ] G) (↑n : ℤ)).range.toAddSubgroup) → M)
        (↑z : G ⧸ ((LinearMap.lsmul ℤ G : (a : ℤ) → G →ₗ[ℤ] G) (↑n : ℤ)).range.toAddSubgroup) :
      M)
    ((f : (a : G ⧸ ((LinearMap.lsmul ℤ G : (a : ℤ) → G →ₗ[ℤ] G) (↑n : ℤ)).range.toAddSubgroup) → M)
        (↑z : G ⧸ ((LinearMap.lsmul ℤ G : (a : ℤ) → G →ₗ[ℤ] G) (↑n : ℤ)).range.toAddSubgroup) :
      M)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.FreeModule.ModN
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
inst : AddCommGroup G
n : ℕ
inst_1 : AddMonoid M
φ : { φ : G →+ M // ∀ (g : G), HSMul.hSMul (β := M) n ((φ : (a : G) → M) g : M) = 0 }
⊢ (fun (f : AddMonoidHom.{u_1, u_3} (ModN G n) M) ↦
        (Subtype.mk (p := fun (φ : G →+ M) ↦ ∀ (g : G), HSMul.hSMul (β := M) n ((φ : (a : G) → M) g : M) = 0)
            (f.comp
              (QuotientAddGroup.mk'
                (Submodule.toAddSubgroup (R := ℤ) (module_M := AddCommGroup.toIntModule G)
                  (LinearMap.range (R := ℤ) (M := G) (τ₁₂ := RingHom.id ℤ)
                    ((LinearMap.lsmul ℤ G : (a : ℤ) → G →ₗ[ℤ] G) (↑n : ℤ))))))
            ⋯ :
          { φ : G →+ M // ∀ (g : G), HSMul.hSMul (β := M) n ((φ : (a : G) → M) g : M) = 0 }))
      ((fun (φ : { φ : G →+ M // ∀ (g : G), HSMul.hSMul (β := M) n ((φ : (a : G) → M) g : M) = 0 }) ↦
          (QuotientAddGroup.lift
              (Submodule.toAddSubgroup (R := ℤ) (module_M := AddCommGroup.toIntModule G)
                (LinearMap.range (R := ℤ) (M := G) (τ₁₂ := RingHom.id ℤ)
                  ((LinearMap.lsmul ℤ G : (a : ℤ) → G →ₗ[ℤ] G) (↑n : ℤ))))
              (↑φ : G →+ M) ⋯ :
            AddMonoidHom.{u_1, u_3}
              (HasQuotient.Quotient G (B := AddSubgroup G)
                (Submodule.toAddSubgroup (R := ℤ) (module_M := AddCommGroup.toIntModule G)
                  (LinearMap.range (R := ℤ) (M := G) (τ₁₂ := RingHom.id ℤ)
                    ((LinearMap.lsmul ℤ G : (a : ℤ) → G →ₗ[ℤ] G) (↑n : ℤ)))))
              M))
        φ) =
    φ

Tactic:
aesop