awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Finite.Quotient (goal)
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)
x : M
⊢ x ∈ N ↔ ∀ (i : ι), a i ∣ (((b'.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i
have simp_rw : (∃ (c : ι → R),
    x =
      ∑ x : ι,
        c x • HSMul.hSMul (β := M) (smithNormalFormCoeffs b h x) ((smithNormalFormTopBasis b h : (a : ι) → M) x : M)) ↔
  ∀ (i : ι), a i ∣ (((b'.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i
Tactic: simp_rw [ab.mem_submodule_iff', ab, ab_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Finite.Quotient (hypothesis)
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)
x : M
⊢ (∃ (c : ι → R),
      x =
        ∑ x : ι,
          c x •
            HSMul.hSMul (β := M) (smithNormalFormCoeffs b h x) ((smithNormalFormTopBasis b h : (a : ι) → M) x : M)) ↔
    ∀ (i : ι), a i ∣ (((b'.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i
have this₁ : ∀ (c : ι → R) (i : ι),
  ((b'.repr : (a : M) → ι →₀ R) (∑ j : ι, c j • HSMul.hSMul (β := M) (a j) ((b' : (a : ι) → M) j : M)) : (a : ι) → R)
      i =
    a i * c i
Tactic: have : ∀ (c : ι → R) (i), b'.repr (∑ j : ι, c j • a j • b' j) i = a i * c i := by
      intro c i
      simp only [← mul_smul, b'.repr_sum_self, mul_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Finite.Quotient (goal)
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)
x : M
this :
  ∀ (c : ι → R) (i : ι),
    ((b'.repr : (a : M) → ι →₀ R) (∑ j : ι, c j • HSMul.hSMul (β := M) (a j) ((b' : (a : ι) → M) j : M)) : (a : ι) → R)
        i =
      a i * c i
⊢ (∃ (c : ι → R),
      x =
        ∑ x : ι,
          c x •
            HSMul.hSMul (β := M) (smithNormalFormCoeffs b h x) ((smithNormalFormTopBasis b h : (a : ι) → M) x : M)) ↔
    ∀ (i : ι), a i ∣ (((b'.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i
have mp : (∃ (c : ι → R),
    x =
      ∑ x : ι,
        c x • HSMul.hSMul (β := M) (smithNormalFormCoeffs b h x) ((smithNormalFormTopBasis b h : (a : ι) → M) x : M)) →
  ∀ (i : ι), a i ∣ (((b'.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Finite.Quotient (goal)
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)
x : M
this :
  ∀ (c : ι → R) (i : ι),
    ((b'.repr : (a : M) → ι →₀ R) (∑ j : ι, c j • HSMul.hSMul (β := M) (a j) ((b' : (a : ι) → M) j : M)) : (a : ι) → R)
        i =
      a i * c i
mp :
  (∃ (c : ι → R),
      x =
        ∑ x : ι,
          c x •
            HSMul.hSMul (β := M) (smithNormalFormCoeffs b h x) ((smithNormalFormTopBasis b h : (a : ι) → M) x : M)) →
    ∀ (i : ι), a i ∣ (((b'.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i
⊢ (∃ (c : ι → R),
      x =
        ∑ x : ι,
          c x •
            HSMul.hSMul (β := M) (smithNormalFormCoeffs b h x) ((smithNormalFormTopBasis b h : (a : ι) → M) x : M)) ↔
    ∀ (i : ι), a i ∣ (((b'.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i
have mpr : (∀ (i : ι), a i ∣ (((b'.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i) →
  ∃ (c : ι → R),
    x =
      ∑ x : ι,
        c x • HSMul.hSMul (β := M) (smithNormalFormCoeffs b h x) ((smithNormalFormTopBasis b h : (a : ι) → M) x : M)
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Finite.Quotient (goal)
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)
x : M
this :
  ∀ (c : ι → R) (i : ι),
    ((b'.repr : (a : M) → ι →₀ R) (∑ j : ι, c j • HSMul.hSMul (β := M) (a j) ((b' : (a : ι) → M) j : M)) : (a : ι) → R)
        i =
      a i * c i
ha : ∀ (i : ι), a i ∣ (((b'.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i
⊢ ∃ (c : ι → R),
    x =
      ∑ x : ι,
        c x • HSMul.hSMul (β := M) (smithNormalFormCoeffs b h x) ((smithNormalFormTopBasis b h : (a : ι) → M) x : M)
have mpr : ∀ (c : (i : ι) → R) (hc : ∀ (i : ι), (((b'.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i = a i * c i),
  ∃ (c : ι → R),
    x =
      ∑ x : ι,
        c x • HSMul.hSMul (β := M) (smithNormalFormCoeffs b h x) ((smithNormalFormTopBasis b h : (a : ι) → M) x : M)
Tactic: choose c hc using ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Finite.Quotient (hypothesis)
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)
⊢ (M ⧸ N) ≃ₗ[R] (i : ι) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {smithNormalFormCoeffs b h i})
have mem_I_iff : ∀ (x : M), x ∈ N ↔ ∀ (i : ι), a i ∣ (((b'.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i
Tactic: have mem_I_iff : ∀ x, x ∈ N ↔ ∀ i, a i ∣ b'.repr x i := by
    intro x
    simp_rw [ab.mem_submodule_iff', ab, ab_eq]
    have : ∀ (c : ι → R) (i), b'.repr (∑ j : ι, c j • a j • b' j) i = a i * c i := by
      intro c i
      simp only [← mul_smul, b'.repr_sum_self, mul_comm]
    constructor
    · rintro ⟨c, rfl⟩ i
      exact ⟨c i, this c i⟩
    · rintro ha
      choose c hc using ha
      exact ⟨c, b'.ext_elem fun i => Eq.trans (hc i) (this c i).symm⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Finite.Quotient (goal)
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'
have h₁ : ∀ (x : ι → R), x ∈ map (↑b'.equivFun : M →ₗ[R] ι → R) N ↔ x ∈ N'
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Finite.Quotient (goal)
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
⊢ x ∈ map (↑b'.equivFun : M →ₗ[R] ι → R) N ↔ x ∈ N'
have h₁ : (∃ (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) ↔
  ∀ (i : ι), ∃ (a_1 : R), x i = a i * a_1
Tactic: 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 _))]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Finite.Quotient (goal)
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
⊢ (∃ (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) ↔
    ∀ (i : ι), ∃ (a_1 : R), x i = a i * a_1
have h₁ : (∃ (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) →
  ∀ (i : ι), ∃ (a_2 : R), x i = a i * a_2
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Finite.Quotient (goal)
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
h₁ :
  (∃ (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) →
    ∀ (i : ι), ∃ (a_2 : R), x i = a i * a_2
⊢ (∃ (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) ↔
    ∀ (i : ι), ∃ (a_1 : R), x i = a i * a_1
have h₂ : (∀ (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: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Finite.Quotient (goal)
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
have h₁ : ∀ (i : ι),
  a i ∣ ((b'.repr : (a : M) → ι →₀ R) (∑ i : ι, HSMul.hSMul (β := M) (x i) ((b' : (a : ι) → M) i : M)) : (a : ι) → R) i
Tactic: refine ⟨∑ i, x i • b' i, fun i => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Finite.Quotient (goal)
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
⊢ ∃ (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
have h₂ : (⇑((b'.repr : (a : M) → ι →₀ R) (∑ i : ι, HSMul.hSMul (β := M) (x i) ((b' : (a : ι) → M) i : M))) : (a : ι) → R) = x
Tactic: refine ⟨∑ i, x i • b' i, fun i => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Finite.Quotient (goal)
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 ∣ ((b'.repr : (a : M) → ι →₀ R) (∑ i : ι, HSMul.hSMul (β := M) (x i) ((b' : (a : ι) → M) i : M)) : (a : ι) → R) i
have h₁ : a i ∣ x i
Tactic: rw [b'.repr_sum_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Finite.Quotient (goal)
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
⊢ (⇑((b'.repr : (a : M) → ι →₀ R) (∑ i : ι, HSMul.hSMul (β := M) (x i) ((b' : (a : ι) → M) i : M))) : (a : ι) → R) = x
have h₁ : x = x
Tactic: rw [b'.repr_sum_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Finite.Quotient (hypothesis)
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
⊢ (M ⧸ N) ≃ₗ[R] (i : ι) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {smithNormalFormCoeffs b h i})
have this₁ : 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
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Finite.Quotient (goal)
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'
⊢ (M ⧸ N) ≃ₗ[R] (i : ι) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {smithNormalFormCoeffs b h i})
have refine : ((ι → R) ⧸ 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) ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Finite.Quotient (hypothesis)
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
⊢ Finite.{u_3 + 1} (M ⧸ N)
have this : ∀ (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)⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Finite.Quotient (goal)
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
have 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)
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⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Finite.Quotient (goal)
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)
⊢ Finite.{u_3 + 1} (M ⧸ N) ↔ finrank.{0, u_3} ℤ ↥N = finrank ℤ M
have 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)) : ℤ)) sorry) :
      (a : M) → ↥N)
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⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Finite.Quotient (goal)
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)
have refine_2 : Ne (α := ℤ) (↑(Nat.card.{u_3} (M ⧸ N)) : ℤ) 0
Tactic: refine (LinearMap.lsmul_injective ?_).codRestrict _