awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.Quotient
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsPrincipalIdealRing R
inst_5 : Finite ι
N : Submodule R M
b : Basis ι R M
h : finrank.{u_2, u_3} R ↥N = finrank R M
this : Fintype ι
a : ι → R := smithNormalFormCoeffs b h
b' : Basis ι R M := smithNormalFormTopBasis b h
ab : Basis.{u_1, u_2, u_3} ι R ↥N := smithNormalFormBotBasis b h
ab_eq :
  ∀ (i : ι),
    (↑((smithNormalFormBotBasis b h : (a : ι) → ↥N) i) : M) =
      HSMul.hSMul (β := M) (smithNormalFormCoeffs b h i) ((smithNormalFormTopBasis b h : (a : ι) → M) i : M)
mem_I_iff : ∀ (x : M), x ∈ N ↔ ∀ (i : ι), a i ∣ (((b'.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i
N' : Submodule R (ι → R) := pi (φ := fun (a : ι) ↦ R) Set.univ fun (i : ι) ↦ R ∙ a i
x : ι → R
hdvd : ∀ (i : ι), ∃ (a_1 : R), x i = a i * a_1
⊢ ∃ (y : M),
    (∀ (i : ι), a i ∣ (((b'.repr : (a : M) → ι →₀ R) y : ι →₀ R) : (a : ι) → R) i) ∧
      (⇑((b'.repr : (a : M) → ι →₀ R) y : ι →₀ R) : (a : ι) → R) = x

Tactic:
⟨∑ i, x i • b' i, fun i => ?_, ?_⟩

Premises used: Finset.univ, And.intro, Exists.intro, HSMul.hSMul, DFunLike.coe, Finset.sum
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.Quotient
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsPrincipalIdealRing R
inst_5 : Finite ι
N : Submodule R M
b : Basis ι R M
h : finrank.{u_2, u_3} R ↥N = finrank R M
this : Fintype ι
a : ι → R := smithNormalFormCoeffs b h
b' : Basis ι R M := smithNormalFormTopBasis b h
ab : Basis.{u_1, u_2, u_3} ι R ↥N := smithNormalFormBotBasis b h
ab_eq :
  ∀ (i : ι),
    (↑((smithNormalFormBotBasis b h : (a : ι) → ↥N) i) : M) =
      HSMul.hSMul (β := M) (smithNormalFormCoeffs b h i) ((smithNormalFormTopBasis b h : (a : ι) → M) i : M)
mem_I_iff : ∀ (x : M), x ∈ N ↔ ∀ (i : ι), a i ∣ (((b'.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i
N' : Submodule R (ι → R) := pi (φ := fun (a : ι) ↦ R) Set.univ fun (i : ι) ↦ R ∙ a i
x : ι → R
hdvd : ∀ (i : ι), ∃ (a_1 : R), x i = a i * a_1
h₁ :
  ∀ (i : ι),
    a i ∣
      ((b'.repr : (a : M) → ι →₀ R) (∑ i : ι, HSMul.hSMul (β := M) (x i) ((b' : (a : ι) → M) i : M)) : (a : ι) → R) i
h₂ :
  (⇑((b'.repr : (a : M) → ι →₀ R) (∑ i : ι, HSMul.hSMul (β := M) (x i) ((b' : (a : ι) → M) i : M))) : (a : ι) → R) = x
⊢ ∃ (y : M),
    (∀ (i : ι), a i ∣ (((b'.repr : (a : M) → ι →₀ R) y : ι →₀ R) : (a : ι) → R) i) ∧
      (⇑((b'.repr : (a : M) → ι →₀ R) y : ι →₀ R) : (a : ι) → R) = x

Tactic:
refine ⟨∑ i, x i • b' i, fun i => ?_, ?_⟩
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.Quotient
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsPrincipalIdealRing R
inst_5 : Finite ι
N : Submodule R M
b : Basis ι R M
h : finrank.{u_2, u_3} R ↥N = finrank R M
this : Fintype ι
a : ι → R := smithNormalFormCoeffs b h
b' : Basis ι R M := smithNormalFormTopBasis b h
ab : Basis.{u_1, u_2, u_3} ι R ↥N := smithNormalFormBotBasis b h
ab_eq :
  ∀ (i : ι),
    (↑((smithNormalFormBotBasis b h : (a : ι) → ↥N) i) : M) =
      HSMul.hSMul (β := M) (smithNormalFormCoeffs b h i) ((smithNormalFormTopBasis b h : (a : ι) → M) i : M)
mem_I_iff : ∀ (x : M), x ∈ N ↔ ∀ (i : ι), a i ∣ (((b'.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i
N' : Submodule R (ι → R) := pi (φ := fun (a : ι) ↦ R) Set.univ fun (i : ι) ↦ R ∙ a i
x : ι → R
hdvd : ∀ (i : ι), ∃ (a_1 : R), x i = a i * a_1
i : ι
h₁ : a i ∣ x i
⊢ a i ∣ ((b'.repr : (a : M) → ι →₀ R) (∑ i : ι, HSMul.hSMul (β := M) (x i) ((b' : (a : ι) → M) i : M)) : (a : ι) → R) i

Tactic:
rw [b'.repr_sum_self]

Premises used: Module.Basis.repr_sum_self
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.Quotient
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsPrincipalIdealRing R
inst_5 : Finite ι
N : Submodule R M
b : Basis ι R M
h : finrank.{u_2, u_3} R ↥N = finrank R M
this : Fintype ι
a : ι → R := smithNormalFormCoeffs b h
b' : Basis ι R M := smithNormalFormTopBasis b h
ab : Basis.{u_1, u_2, u_3} ι R ↥N := smithNormalFormBotBasis b h
ab_eq :
  ∀ (i : ι),
    (↑((smithNormalFormBotBasis b h : (a : ι) → ↥N) i) : M) =
      HSMul.hSMul (β := M) (smithNormalFormCoeffs b h i) ((smithNormalFormTopBasis b h : (a : ι) → M) i : M)
mem_I_iff : ∀ (x : M), x ∈ N ↔ ∀ (i : ι), a i ∣ (((b'.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i
N' : Submodule R (ι → R) := pi (φ := fun (a : ι) ↦ R) Set.univ fun (i : ι) ↦ R ∙ a i
x : ι → R
hdvd : ∀ (i : ι), ∃ (a_1 : R), x i = a i * a_1
h₁ h₂ : x = x
⊢ (⇑((b'.repr : (a : M) → ι →₀ R) (∑ i : ι, HSMul.hSMul (β := M) (x i) ((b' : (a : ι) → M) i : M))) : (a : ι) → R) = x

Tactic:
rw [b'.repr_sum_self]

Premises used: Module.Basis.repr_sum_self
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.Quotient
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsPrincipalIdealRing R
inst_5 : Finite ι
N : Submodule R M
b : Basis ι R M
h : finrank.{u_2, u_3} R ↥N = finrank R M
this : Fintype ι
a : ι → R := smithNormalFormCoeffs b h
b' : Basis ι R M := smithNormalFormTopBasis b h
ab : Basis.{u_1, u_2, u_3} ι R ↥N := smithNormalFormBotBasis b h
ab_eq :
  ∀ (i : ι),
    (↑((smithNormalFormBotBasis b h : (a : ι) → ↥N) i) : M) =
      HSMul.hSMul (β := M) (smithNormalFormCoeffs b h i) ((smithNormalFormTopBasis b h : (a : ι) → M) i : M)
mem_I_iff : ∀ (x : M), x ∈ N ↔ ∀ (i : ι), a i ∣ (((b'.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i
N' : Submodule R (ι → R) := pi (φ := fun (a : ι) ↦ R) Set.univ fun (i : ι) ↦ R ∙ a i
x : ι → R
hdvd : ∀ (i : ι), ∃ (a_1 : R), x i = a i * a_1
i : ι
⊢ a i ∣ x i

Tactic:
hdvd i
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.Quotient
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsPrincipalIdealRing R
inst_5 : Finite ι
N : Submodule R M
b : Basis ι R M
h : finrank.{u_2, u_3} R ↥N = finrank R M
this : Fintype ι
a : ι → R := smithNormalFormCoeffs b h
b' : Basis ι R M := smithNormalFormTopBasis b h
ab : Basis.{u_1, u_2, u_3} ι R ↥N := smithNormalFormBotBasis b h
ab_eq :
  ∀ (i : ι),
    (↑((smithNormalFormBotBasis b h : (a : ι) → ↥N) i) : M) =
      HSMul.hSMul (β := M) (smithNormalFormCoeffs b h i) ((smithNormalFormTopBasis b h : (a : ι) → M) i : M)
mem_I_iff : ∀ (x : M), x ∈ N ↔ ∀ (i : ι), a i ∣ (((b'.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i
N' : Submodule R (ι → R) := pi (φ := fun (a : ι) ↦ R) Set.univ fun (i : ι) ↦ R ∙ a i
x : ι → R
hdvd : ∀ (i : ι), ∃ (a_1 : R), x i = a i * a_1
i : ι
⊢ a i ∣ x i

Tactic:
exact hdvd i
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.Quotient
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsPrincipalIdealRing R
inst_5 : Finite ι
N : Submodule R M
b : Basis ι R M
h : finrank.{u_2, u_3} R ↥N = finrank R M
this : Fintype ι
a : ι → R := smithNormalFormCoeffs b h
b' : Basis ι R M := smithNormalFormTopBasis b h
ab : Basis.{u_1, u_2, u_3} ι R ↥N := smithNormalFormBotBasis b h
ab_eq :
  ∀ (i : ι),
    (↑((smithNormalFormBotBasis b h : (a : ι) → ↥N) i) : M) =
      HSMul.hSMul (β := M) (smithNormalFormCoeffs b h i) ((smithNormalFormTopBasis b h : (a : ι) → M) i : M)
mem_I_iff : ∀ (x : M), x ∈ N ↔ ∀ (i : ι), a i ∣ (((b'.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i
N' : Submodule R (ι → R) := pi (φ := fun (a : ι) ↦ R) Set.univ fun (i : ι) ↦ R ∙ a i
⊢ map (↑b'.equivFun : M →ₗ[R] ι → R) N = N'

Tactic:
have : Submodule.map (b'.equivFun : M →ₗ[R] ι → R) N = N' := by
    ext x
    simp only [N', Submodule.mem_map, Submodule.mem_pi, mem_span_singleton, Set.mem_univ,
      mem_I_iff, smul_eq_mul, forall_true_left, LinearEquiv.coe_coe,
      Basis.equivFun_apply, mul_comm _ (a _), eq_comm (b := (x _))]
    constructor
    · rintro ⟨y, hy, rfl⟩ i
      exact hy i
    · rintro hdvd
      refine ⟨∑ i, x i • b' i, fun i => ?_, ?_⟩ <;> rw [b'.repr_sum_self]
      · exact hdvd i
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.Quotient
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsPrincipalIdealRing R
inst_5 : Finite ι
N : Submodule R M
b : Basis ι R M
h : finrank.{u_2, u_3} R ↥N = finrank R M
this_1 : Fintype ι
a : ι → R := smithNormalFormCoeffs b h
b' : Basis ι R M := smithNormalFormTopBasis b h
ab : Basis.{u_1, u_2, u_3} ι R ↥N := smithNormalFormBotBasis b h
ab_eq :
  ∀ (i : ι),
    (↑((smithNormalFormBotBasis b h : (a : ι) → ↥N) i) : M) =
      HSMul.hSMul (β := M) (smithNormalFormCoeffs b h i) ((smithNormalFormTopBasis b h : (a : ι) → M) i : M)
mem_I_iff : ∀ (x : M), x ∈ N ↔ ∀ (i : ι), a i ∣ (((b'.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i
N' : Submodule R (ι → R) := pi (φ := fun (a : ι) ↦ R) Set.univ fun (i : ι) ↦ R ∙ a i
this : map (↑b'.equivFun : M →ₗ[R] ι → R) N = N'
refine : ((ι → R) ⧸ N') ≃ₗ[R] (i : ι) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {smithNormalFormCoeffs b h i})
⊢ (M ⧸ N) ≃ₗ[R] (i : ι) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {smithNormalFormCoeffs b h i})

Tactic:
refine (Submodule.Quotient.equiv N N' b'.equivFun this).trans (re₂₃ := inferInstance)
    (re₃₂ := inferInstance) ?_

Premises used: Submodule.Quotient.equiv, LinearEquiv.trans, Module.Basis.equivFun
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.Quotient
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsPrincipalIdealRing R
inst_5 : Finite ι
N : Submodule R M
b : Basis ι R M
h : finrank.{u_2, u_3} R ↥N = finrank R M
this_1 : Fintype ι
a : ι → R := smithNormalFormCoeffs b h
b' : Basis ι R M := smithNormalFormTopBasis b h
ab : Basis.{u_1, u_2, u_3} ι R ↥N := smithNormalFormBotBasis b h
ab_eq :
  ∀ (i : ι),
    (↑((smithNormalFormBotBasis b h : (a : ι) → ↥N) i) : M) =
      HSMul.hSMul (β := M) (smithNormalFormCoeffs b h i) ((smithNormalFormTopBasis b h : (a : ι) → M) i : M)
mem_I_iff : ∀ (x : M), x ∈ N ↔ ∀ (i : ι), a i ∣ (((b'.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i
N' : Submodule R (ι → R) := pi (φ := fun (a : ι) ↦ R) Set.univ fun (i : ι) ↦ R ∙ a i
this : map (↑b'.equivFun : M →ₗ[R] ι → R) N = N'
⊢ ((ι → R) ⧸ N') ≃ₗ[R] (i : ι) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {smithNormalFormCoeffs b h i})

Tactic:
exact Submodule.quotientPi (show _ → Submodule R R from fun i => span R ({a i} : Set R))

Premises used: Submodule.quotientPi, Submodule.span, Singleton.singleton
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.Quotient
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsPrincipalIdealRing R
inst_5 : Finite ι
N : Submodule R M
b : Basis ι R M
h : finrank.{u_2, u_3} R ↥N = finrank R M
this_1 : Fintype ι
a : ι → R := smithNormalFormCoeffs b h
b' : Basis ι R M := smithNormalFormTopBasis b h
ab : Basis.{u_1, u_2, u_3} ι R ↥N := smithNormalFormBotBasis b h
ab_eq :
  ∀ (i : ι),
    (↑((smithNormalFormBotBasis b h : (a : ι) → ↥N) i) : M) =
      HSMul.hSMul (β := M) (smithNormalFormCoeffs b h i) ((smithNormalFormTopBasis b h : (a : ι) → M) i : M)
mem_I_iff : ∀ (x : M), x ∈ N ↔ ∀ (i : ι), a i ∣ (((b'.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i
N' : Submodule R (ι → R) := pi (φ := fun (a : ι) ↦ R) Set.univ fun (i : ι) ↦ R ∙ a i
this : map (↑b'.equivFun : M →ₗ[R] ι → R) N = N'
⊢ ((ι → R) ⧸ N') ≃ₗ[R] (i : ι) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {smithNormalFormCoeffs b h i})

Tactic:
classical
  exact Submodule.quotientPi (show _ → Submodule R R from fun i => span R ({a i} : Set R))
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.Quotient
Goal:
M : Type u_3
inst : AddCommGroup M
inst_1 : Free ℤ M
inst_2 : Module.Finite ℤ M
N : Submodule ℤ M
h : finrank.{0, u_3} ℤ ↥N = finrank ℤ M
b : Basis (Free.ChooseBasisIndex ℤ M) ℤ M := Free.chooseBasis ℤ M
a : Free.ChooseBasisIndex ℤ M → ℤ := smithNormalFormCoeffs b h
e : M ⧸ N ≃+ ((i : Free.ChooseBasisIndex ℤ M) → ZMod (smithNormalFormCoeffs b h i).natAbs) := N.quotientEquivPiZMod b h
⊢ ∀ (i : Free.ChooseBasisIndex ℤ M), NeZero (a i).natAbs

Tactic:
have : ∀ i, NeZero (a i).natAbs := fun i ↦
    ⟨Int.natAbs_ne_zero.mpr (smithNormalFormCoeffs_ne_zero b h i)⟩
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.Quotient
Goal:
M : Type u_3
inst : AddCommGroup M
inst_1 : Free ℤ M
inst_2 : Module.Finite ℤ M
N : Submodule ℤ M
h : finrank.{0, u_3} ℤ ↥N = finrank ℤ M
b : Basis (Free.ChooseBasisIndex ℤ M) ℤ M := Free.chooseBasis ℤ M
a : Free.ChooseBasisIndex ℤ M → ℤ := smithNormalFormCoeffs b h
e : M ⧸ N ≃+ ((i : Free.ChooseBasisIndex ℤ M) → ZMod (smithNormalFormCoeffs b h i).natAbs) := N.quotientEquivPiZMod b h
this : ∀ (i : Free.ChooseBasisIndex ℤ M), NeZero (a i).natAbs
⊢ Finite.{u_3 + 1} (M ⧸ N)

Tactic:
Finite.of_equiv (Π i, ZMod (a i).natAbs) e.symm

Premises used: Finite.of_equiv, EquivLike.toEquiv, AddEquiv.symm
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.Quotient
Goal:
M : Type u_3
inst : AddCommGroup M
inst_1 : Free ℤ M
inst_2 : Module.Finite ℤ M
N : Submodule ℤ M
h : finrank.{0, u_3} ℤ ↥N = finrank ℤ M
b : Basis (Free.ChooseBasisIndex ℤ M) ℤ M := Free.chooseBasis ℤ M
a : Free.ChooseBasisIndex ℤ M → ℤ := smithNormalFormCoeffs b h
e : M ⧸ N ≃+ ((i : Free.ChooseBasisIndex ℤ M) → ZMod (smithNormalFormCoeffs b h i).natAbs) := N.quotientEquivPiZMod b h
this : ∀ (i : Free.ChooseBasisIndex ℤ M), NeZero (a i).natAbs
⊢ Finite.{u_3 + 1} (M ⧸ N)

Tactic:
exact Finite.of_equiv (Π i, ZMod (a i).natAbs) e.symm

Premises used: Finite.of_equiv
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.Quotient
Goal:
M : Type u_3
inst : AddCommGroup M
inst_1 : Free ℤ M
inst_2 : Module.Finite ℤ M
N : Submodule ℤ M
⊢ Finite.{u_3 + 1} (M ⧸ N) ↔ finrank.{0, u_3} ℤ ↥N = finrank ℤ M

Tactic:
⟨fun h ↦ le_antisymm (finrank_le N) <|
    ((LinearMap.lsmul ℤ M (Nat.card (M ⧸ N))).codRestrict N
      fun x ↦ ?_).finrank_le_finrank_of_injective ?_, fun h ↦ finiteQuotientOfFreeOfRankEq N h⟩

Premises used: le_antisymm, Submodule.finiteQuotientOfFreeOfRankEq, Iff.intro, Submodule.finrank_le, LinearMap.finrank_le_finrank_of_injective
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.Quotient
Goal:
M : Type u_3
inst : AddCommGroup M
inst_1 : Free ℤ M
inst_2 : Module.Finite ℤ M
N : Submodule ℤ M
refine_1 :
  ∀ (h : Finite.{u_3 + 1} (M ⧸ N)) (x : M),
    Membership.mem (α := M) N
      ((((LinearMap.lsmul ℤ M : (a : ℤ) → M →ₗ[ℤ] M) (↑(Nat.card.{u_3} (M ⧸ N)) : ℤ) : M →ₗ[ℤ] M) : (a : M) → M) x : M)
refine_2 :
  ∀ (h : Finite.{u_3 + 1} (M ⧸ N)),
    Function.Injective (α := M) (β := ↥N)
      (⇑(LinearMap.codRestrict N ((LinearMap.lsmul ℤ M : (a : ℤ) → M →ₗ[ℤ] M) (↑(Nat.card.{u_3} (M ⧸ N)) : ℤ)) ⋯) :
        (a : M) → ↥N)
⊢ Finite.{u_3 + 1} (M ⧸ N) ↔ finrank.{0, u_3} ℤ ↥N = finrank ℤ M

Tactic:
refine ⟨fun h ↦ le_antisymm (finrank_le N) <|
    ((LinearMap.lsmul ℤ M (Nat.card (M ⧸ N))).codRestrict N
      fun x ↦ ?_).finrank_le_finrank_of_injective ?_, fun h ↦ finiteQuotientOfFreeOfRankEq N h⟩
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.Quotient
Goal:
M : Type u_3
inst : AddCommGroup M
inst_1 : Free ℤ M
inst_2 : Module.Finite ℤ M
N : Submodule ℤ M
h : Finite.{u_3 + 1} (M ⧸ N)
x : M
⊢ Membership.mem (α := M) N
    ((((LinearMap.lsmul ℤ M : (a : ℤ) → M →ₗ[ℤ] M) (↑(Nat.card.{u_3} (M ⧸ N)) : ℤ) : M →ₗ[ℤ] M) : (a : M) → M) x : M)

Tactic:
simpa using AddSubgroup.nsmul_index_mem N.toAddSubgroup x

Premises used: Submodule.toAddSubgroup, AddSubgroup.nsmul_index_mem
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.Quotient
Goal:
M : Type u_3
inst : AddCommGroup M
inst_1 : Free ℤ M
inst_2 : Module.Finite ℤ M
N : Submodule ℤ M
h : Finite.{u_3 + 1} (M ⧸ N)
⊢ Function.Injective (α := M) (β := ↥N)
    (⇑(LinearMap.codRestrict N ((LinearMap.lsmul ℤ M : (a : ℤ) → M →ₗ[ℤ] M) (↑(Nat.card.{u_3} (M ⧸ N)) : ℤ)) ⋯) :
      (a : M) → ↥N)

Tactic:
(LinearMap.lsmul_injective ?_).codRestrict _

Premises used: Function.Injective.codRestrict, LinearMap.lsmul_injective, Set.codRestrict
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.Quotient
Goal:
M : Type u_3
inst : AddCommGroup M
inst_1 : Free ℤ M
inst_2 : Module.Finite ℤ M
N : Submodule ℤ M
h : Finite.{u_3 + 1} (M ⧸ N)
refine_2 : Ne (α := ℤ) (↑(Nat.card.{u_3} (M ⧸ N)) : ℤ) 0
⊢ Function.Injective (α := M) (β := ↥N)
    (⇑(LinearMap.codRestrict N ((LinearMap.lsmul ℤ M : (a : ℤ) → M →ₗ[ℤ] M) (↑(Nat.card.{u_3} (M ⧸ N)) : ℤ)) ⋯) :
      (a : M) → ↥N)

Tactic:
refine (LinearMap.lsmul_injective ?_).codRestrict _

Premises used: Function.Injective.codRestrict, LinearMap.lsmul_injective
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.Quotient
Goal:
M : Type u_3
inst : AddCommGroup M
inst_1 : Free ℤ M
inst_2 : Module.Finite ℤ M
N : Submodule ℤ M
h : Finite.{u_3 + 1} (M ⧸ N)
⊢ Ne (α := ℤ) (↑(Nat.card.{u_3} (M ⧸ N)) : ℤ) 0

Tactic:
Int.ofNat_ne_zero.mpr <| Nat.card_ne_zero.mpr
      ⟨Set.nonempty_iff_univ_nonempty.mpr Set.univ_nonempty, h⟩

Premises used: Iff.mpr, Set.univ_nonempty, Int.ofNat_ne_zero, Set.nonempty_iff_univ_nonempty, And.intro, Nat.card_ne_zero
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.Quotient
Goal:
M : Type u_3
inst : AddCommGroup M
inst_1 : Free ℤ M
inst_2 : Module.Finite ℤ M
N : Submodule ℤ M
h : Finite.{u_3 + 1} (M ⧸ N)
⊢ Ne (α := ℤ) (↑(Nat.card.{u_3} (M ⧸ N)) : ℤ) 0

Tactic:
exact Int.ofNat_ne_zero.mpr <| Nat.card_ne_zero.mpr
      ⟨Set.nonempty_iff_univ_nonempty.mpr Set.univ_nonempty, h⟩

Premises used: Iff.mpr, Set.univ_nonempty, Int.ofNat_ne_zero, Set.nonempty_iff_univ_nonempty, And.intro, Nat.card_ne_zero
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.Quotient
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsPrincipalIdealRing R
inst_5 : Finite ι
F : Type u_4
inst_6 : CommRing F
inst_7 : Algebra F R
inst_8 : Module F M
inst_9 : IsScalarTower F R M
b : Basis ι R M
N : Submodule R M
h : finrank.{u_2, u_3} R ↥N = finrank R M
haveI :
  (this : Fintype ι) →
    (M ⧸ N) ≃ₗ[F] ⨁ (i : ι), HasQuotient.Quotient R (B := Ideal R) (Ideal.span {smithNormalFormCoeffs b h i})
⊢ (M ⧸ N) ≃ₗ[F] ⨁ (i : ι), HasQuotient.Quotient R (B := Ideal R) (Ideal.span {smithNormalFormCoeffs b h i})

Tactic:
haveI := Fintype.ofFinite ι
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.Quotient
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsPrincipalIdealRing R
inst_5 : Finite ι
F : Type u_4
inst_6 : CommRing F
inst_7 : Algebra F R
inst_8 : Module F M
inst_9 : IsScalarTower F R M
b : Basis ι R M
N : Submodule R M
h : finrank.{u_2, u_3} R ↥N = finrank R M
this : Fintype ι
⊢ (M ⧸ N) ≃ₗ[F] ⨁ (i : ι), HasQuotient.Quotient R (B := Ideal R) (Ideal.span {smithNormalFormCoeffs b h i})

Tactic:
exact ((N.quotientEquivPiSpan b _).restrictScalars F).trans
    (DirectSum.linearEquivFunOnFintype _ _ _).symm

Premises used: LinearEquiv.symm, LinearEquiv.restrictScalars, DirectSum.linearEquivFunOnFintype, Submodule.quotientEquivPiSpan, LinearEquiv.trans
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.Quotient
Goal:
R : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsPrincipalIdealRing R
F : Type u_4
inst_5 : CommRing F
inst_6 : Algebra F R
inst_7 : Module F M
inst_8 : IsScalarTower F R M
N : Submodule R M
ι : Type u_5
inst_9 : Fintype ι
b : Basis ι R M
inst_10 : Nontrivial F
h : finrank.{u_2, u_3} R ↥N = finrank R M
inst_11 :
  ∀ (i : ι), Free.{u_4, u_2} F (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {smithNormalFormCoeffs b h i}))
inst_12 :
  ∀ (i : ι),
    Module.Finite.{u_4, u_2} F (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {smithNormalFormCoeffs b h i}))
rw :
  finrank F (⨁ (i : ι), HasQuotient.Quotient R (B := Ideal R) (Ideal.span {smithNormalFormCoeffs b h i})) =
    ∑ i : ι, finrank.{u_4, u_2} F (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {smithNormalFormCoeffs b h i}))
rw₁ rw₂ :
  Eq (α := ℕ)
    (∑ i : ι, finrank.{u_4, u_2} F (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {smithNormalFormCoeffs b h i})))
    (∑ i : ι, finrank.{u_4, u_2} F (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {smithNormalFormCoeffs b h i})))
⊢ finrank.{u_4, u_3} F (M ⧸ N) =
    ∑ i : ι, finrank.{u_4, u_2} F (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {smithNormalFormCoeffs b h i}))

Tactic:
rw [LinearEquiv.finrank_eq <| quotientEquivDirectSum F b h, Module.finrank_directSum]

Premises used: Submodule.quotientEquivDirectSum, LinearEquiv.finrank_eq, Module.finrank_directSum
-- Module: Mathlib.LinearAlgebra.FreeModule.IdealQuotient
Goal:
S : Type u_3
inst : CommRing S
inst_1 : IsDomain S
inst_2 : Free ℤ S
inst_3 : Module.Finite ℤ S
I : Ideal S
hI : I ≠ ⊥
⊢ Finite.{u_3 + 1} (S ⧸ I)

Tactic:
let b := Module.Free.chooseBasis ℤ S
  Submodule.finiteQuotientOfFreeOfRankEq (I.restrictScalars ℤ) <| finrank_eq_finrank b I hI

Premises used: Ideal.finrank_eq_finrank, Submodule.restrictScalars, Int, Submodule.finiteQuotientOfFreeOfRankEq, Submodule.quotientRel, Module.Free.chooseBasis
-- Module: Mathlib.LinearAlgebra.FreeModule.IdealQuotient
Goal:
R : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain R
inst_4 : IsPrincipalIdealRing R
inst_5 : IsDomain S
F : Type u_4
inst_6 : CommRing F
inst_7 : Algebra F R
inst_8 : Algebra F S
inst_9 : IsScalarTower F R S
I : Ideal S
hI : I ≠ ⊥
ι : Type u_5
inst_10 : Fintype ι
b : Basis ι R S
inst_11 : Nontrivial F
inst_12 : ∀ (i : ι), Free.{u_4, u_2} F (HasQuotient.Quotient R (B := Ideal R) (span {smithCoeffs b I hI i}))
inst_13 : ∀ (i : ι), Module.Finite.{u_4, u_2} F (HasQuotient.Quotient R (B := Ideal R) (span {smithCoeffs b I hI i}))
rw :
  finrank F (⨁ (i : ι), HasQuotient.Quotient R (B := Ideal R) (span {smithCoeffs b I hI i})) =
    ∑ i : ι, finrank.{u_4, u_2} F (HasQuotient.Quotient R (B := Ideal R) (span {smithCoeffs b I hI i}))
rw₁ rw₂ :
  Eq (α := ℕ) (∑ i : ι, finrank.{u_4, u_2} F (HasQuotient.Quotient R (B := Ideal R) (span {smithCoeffs b I hI i})))
    (∑ i : ι, finrank.{u_4, u_2} F (HasQuotient.Quotient R (B := Ideal R) (span {smithCoeffs b I hI i})))
⊢ finrank.{u_4, u_3} F (S ⧸ I) =
    ∑ i : ι, finrank.{u_4, u_2} F (HasQuotient.Quotient R (B := Ideal R) (span {smithCoeffs b I hI i}))

Tactic:
rw [LinearEquiv.finrank_eq <| quotientEquivDirectSum F b hI, Module.finrank_directSum]

Premises used: LinearEquiv.finrank_eq, Ideal.quotientEquivDirectSum, Module.finrank_directSum
-- 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
snf : SmithNormalForm N ι n
rcases :
  ∀ (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.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}))
⊢ N.toAddSubgroup.index =
    Nat.card R ^ (Fintype.card ι - n) *
      ∏ i : Fin n, AddSubgroup.index.{u_2} (G := R) (Submodule.toAddSubgroup (Ideal.span {snf.a i}))

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