awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.Matrix
Goal:
K : Type u_1
M : Type u_2
L : Type v
inst : CommRing K
inst_1 : Ring M
inst_2 : Algebra K M
inst_3 : Module.Free K M
inst_4 : Module.Finite K M
inst_5 : CommRing L
inst_6 : IsDomain L
inst_7 : Algebra K L
this : Nontrivial K
h : lift.{v, u_2} (Module.rank K M) = Module.rank L (M →ₗ[K] L)
h₁ h₂ : lift.{v, u_2} (Module.rank K M) = lift.{v, u_2} (Module.rank K M)
⊢ lift.{v, u_2} (Module.rank K M) = lift.{max u_2 v, max u_2 v} (Module.rank L (M →ₗ[K] L))

Tactic:
rw [lift_id, Module.rank_linearMap_self]

Premises used: Module.rank_linearMap_self, Cardinal.lift_id
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.Matrix
Goal:
K : Type u_1
M : Type u_2
L : Type v
inst : CommRing K
inst_1 : Ring M
inst_2 : Algebra K M
inst_3 : Module.Free K M
inst_4 : Module.Finite K M
inst_5 : CommRing L
inst_6 : IsDomain L
inst_7 : Algebra K L
⊢ LE.le (α := ℕ) ((toNat : (a : Cardinal.{max u_2 v}) → ℕ) #(M →ₐ[K] L) : ℕ)
    ((toNat : (a : Cardinal.{max u_2 v}) → ℕ) (lift.{v, u_2} (Module.rank K M)) : ℕ)

Tactic:
toNat_le_toNat (cardinalMk_algHom_le_rank K M L) ?_

Premises used: Cardinal.toNat_le_toNat, cardinalMk_algHom_le_rank
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.Matrix
Goal:
K : Type u_1
M : Type u_2
L : Type v
inst : CommRing K
inst_1 : Ring M
inst_2 : Algebra K M
inst_3 : Module.Free K M
inst_4 : Module.Finite K M
inst_5 : CommRing L
inst_6 : IsDomain L
inst_7 : Algebra K L
h : finrank K M = (toNat : (a : Cardinal.{max u_2 v}) → ℕ) (lift.{v, u_2} (Module.rank K M))
convert! : lift.{v, u_2} (Module.rank K M) < ℵ₀
⊢ Nat.card (M →ₐ[K] L) ≤ finrank K M

Tactic:
convert! toNat_le_toNat (cardinalMk_algHom_le_rank K M L) ?_

Premises used: Cardinal.toNat_le_toNat, cardinalMk_algHom_le_rank
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.Matrix
Goal:
K : Type u_1
M : Type u_2
L : Type v
inst : CommRing K
inst_1 : Ring M
inst_2 : Algebra K M
inst_3 : Module.Free K M
inst_4 : Module.Finite K M
inst_5 : CommRing L
inst_6 : IsDomain L
inst_7 : Algebra K L
h : finrank K M = (toNat : (a : Cardinal.{u_2}) → ℕ) (Module.rank K M)
h₁ h₂ :
  Eq (α := ℕ) ((toNat : (a : Cardinal.{u_2}) → ℕ) (Module.rank K M) : ℕ)
    ((toNat : (a : Cardinal.{u_2}) → ℕ) (Module.rank K M) : ℕ)
⊢ finrank K M = (toNat : (a : Cardinal.{max u_2 v}) → ℕ) (lift.{v, u_2} (Module.rank K M))

Tactic:
rw [toNat_lift, finrank]

Premises used: Cardinal.toNat_lift, Module.finrank
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.Matrix
Goal:
K : Type u_1
M : Type u_2
L : Type v
inst : CommRing K
inst_1 : Ring M
inst_2 : Algebra K M
inst_3 : Module.Free K M
inst_4 : Module.Finite K M
inst_5 : CommRing L
inst_6 : IsDomain L
inst_7 : Algebra K L
rw : Module.rank K M < ℵ₀
⊢ lift.{v, u_2} (Module.rank K M) < ℵ₀

Tactic:
rw [lift_lt_aleph0]

Premises used: Cardinal.lift_lt_aleph0
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.Matrix
Goal:
K : Type u_1
M : Type u_2
L : Type v
inst : CommRing K
inst_1 : Ring M
inst_2 : Algebra K M
inst_3 : Module.Free K M
inst_4 : Module.Finite K M
inst_5 : CommRing L
inst_6 : IsDomain L
inst_7 : Algebra K L
this : Nontrivial K
⊢ Module.rank K M < ℵ₀

Tactic:
apply Module.rank_lt_aleph0

Premises used: Module.rank_lt_aleph0
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.Matrix
Goal:
R : Type u
S : Type u'
M : Type v
N : Type w
inst : AddCommGroup M
inst_1 : Module.Finite ℤ M
inst_2 : Free ℤ M
inst_3 : AddCommGroup N
inst_4 : Module.Finite ℤ N
⊢ Module.Finite ℤ (M →+ N)

Tactic:
Module.Finite.equiv (addMonoidHomLequivInt ℤ).symm

Premises used: LinearEquiv.symm, Int, addMonoidHomLequivInt, Module.Finite.equiv
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.Matrix
Goal:
R : Type u
S : Type u'
M : Type v
N : Type w
inst : AddCommGroup M
inst_1 : Module.Finite ℤ M
inst_2 : Free ℤ M
inst_3 : AddCommGroup N
inst_4 : Free ℤ N
⊢ Free ℤ (M →+ N)

Tactic:
letI : Module.Free ℤ (M →ₗ[ℤ] N) := Module.Free.linearMap _ _ _ _
  Module.Free.of_equiv (addMonoidHomLequivInt ℤ).symm

Premises used: LinearEquiv.symm, Int, Module.Free.of_equiv, addMonoidHomLequivInt
-- 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
haveI :
  (this : Fintype ι) →
    (M ⧸ 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:
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 ι
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
⊢ ∀ (i : ι),
    (↑((smithNormalFormBotBasis b h : (a : ι) → ↥N) i) : M) =
      HSMul.hSMul (β := M) (smithNormalFormCoeffs b h i) ((smithNormalFormTopBasis b h : (a : ι) → M) i : M)

Tactic:
have ab_eq := smithNormalFormBotBasis_def b h
-- 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)
x : M
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
⊢ x ∈ N ↔ ∀ (i : ι), a i ∣ (((b'.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i

Tactic:
simp_rw [ab.mem_submodule_iff', ab, ab_eq]

Premises used: Module.Basis.mem_submodule_iff'
-- 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)
x : M
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:
simp only [← mul_smul, b'.repr_sum_self, mul_comm]

Premises used: mul_comm, Module.Basis.repr_sum_self, SemigroupAction.mul_smul
-- 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)
x : M
⊢ ∀ (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]
-- 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)
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
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)
⊢ (∃ (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
-- 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)
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
i : ι
⊢ a i ∣
    ((b'.repr : (a : M) → ι →₀ R)
          (∑ x : ι,
            c x •
              HSMul.hSMul (β := M) (smithNormalFormCoeffs b h x) ((smithNormalFormTopBasis b h : (a : ι) → M) x : M)) :
        (a : ι) → R)
      i

Tactic:
⟨c i, this c i⟩

Premises used: Exists.intro
-- 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)
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
i : ι
⊢ a i ∣
    ((b'.repr : (a : M) → ι →₀ R)
          (∑ x : ι,
            c x •
              HSMul.hSMul (β := M) (smithNormalFormCoeffs b h x) ((smithNormalFormTopBasis b h : (a : ι) → M) x : M)) :
        (a : ι) → R)
      i

Tactic:
exact ⟨c i, this c 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)
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
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)
⊢ ∃ (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
-- 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)
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 : (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:
⟨c, b'.ext_elem fun i => Eq.trans (hc i) (this c i).symm⟩

Premises used: Module.Basis.ext_elem, Exists.intro, Eq.symm, Eq.trans
-- 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)
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 : (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:
exact ⟨c, b'.ext_elem fun i => Eq.trans (hc i) (this c i).symm⟩
-- 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)
⊢ ∀ (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⟩
-- 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
h₁ : ∀ (x : ι → R), x ∈ map (↑b'.equivFun : M →ₗ[R] ι → R) N ↔ x ∈ N'
⊢ map (↑b'.equivFun : M →ₗ[R] ι → R) N = N'

Tactic:
ext x
-- 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
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
⊢ x ∈ map (↑b'.equivFun : M →ₗ[R] ι → R) N ↔ x ∈ N'

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 _))]

Premises used: forall_true_left, Submodule.mem_pi, Submodule.mem_map, Submodule.mem_span_singleton, eq_comm, Module.Basis.equivFun_apply, Set.mem_univ, mul_comm, smul_eq_mul, LinearEquiv.coe_coe
-- 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
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
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
⊢ (∃ (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:
constructor
-- 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
y : M
hy : ∀ (i : ι), a i ∣ (((b'.repr : (a : M) → ι →₀ R) y : ι →₀ R) : (a : ι) → R) i
i : ι
⊢ ∃ (a_1 : R), (((b'.repr : (a : M) → ι →₀ R) y : ι →₀ R) : (a : ι) → R) i = a i * a_1

Tactic:
hy 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
y : M
hy : ∀ (i : ι), a i ∣ (((b'.repr : (a : M) → ι →₀ R) y : ι →₀ R) : (a : ι) → R) i
i : ι
⊢ ∃ (a_1 : R), (((b'.repr : (a : M) → ι →₀ R) y : ι →₀ R) : (a : ι) → R) i = a i * a_1

Tactic:
exact hy i