awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : Free ℤ M
inst_2 : Module.Finite ℤ M
N : Submodule ℤ M
E : Type u_2
inst_3 : EquivLike E M ↥N
inst_4 : AddEquivClass E M ↥N
e : E
b : Basis (Free.ChooseBasisIndex ℤ M) ℤ M := Free.chooseBasis ℤ M
h : finrank.{0, u_1} ℤ ↥N = finrank ℤ M
a : Free.ChooseBasisIndex ℤ M → ℤ := smithNormalFormCoeffs b h
b' : Basis (Free.ChooseBasisIndex ℤ M) ℤ M := smithNormalFormTopBasis b h
ab : Basis (Free.ChooseBasisIndex ℤ M) ℤ ↥N := smithNormalFormBotBasis b h
ab_eq :
  ∀ (i : Free.ChooseBasisIndex ℤ M),
    (↑((smithNormalFormBotBasis b h : (a : Free.ChooseBasisIndex ℤ M) → ↥N) i) : M) =
      HSMul.hSMul (β := M) (smithNormalFormCoeffs b h i)
        ((smithNormalFormTopBasis b h : (a : Free.ChooseBasisIndex ℤ M) → M) i : M)
e' : M ≃ₗ[ℤ] ↥N := b'.equiv ab (Equiv.refl (Free.ChooseBasisIndex ℤ M))
f : M →ₗ[ℤ] M := N.subtype ∘ₗ (↑e' : M →ₗ[ℤ] ↥N)
f_apply : ∀ (x : M),
  Eq (α := M) ((f : (a : M) → M) x : M)
    ((↑((b'.equiv ab (Equiv.refl (Free.ChooseBasisIndex ℤ M)) : (a : M) → ↥N) x) : M) : M) :=
  ⋯
i : Free.ChooseBasisIndex ℤ M
⊢ (↑((ab : (a : Free.ChooseBasisIndex ℤ M) → ↥N) i) : M) =
    HSMul.hSMul (β := M) (a i) ((b' : (a : Free.ChooseBasisIndex ℤ M) → M) i : M)

Tactic:
exact ab_eq i
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : Free ℤ M
inst_2 : Module.Finite ℤ M
N : Submodule ℤ M
E : Type u_2
inst_3 : EquivLike E M ↥N
inst_4 : AddEquivClass E M ↥N
e : E
b : Basis (Free.ChooseBasisIndex ℤ M) ℤ M := Free.chooseBasis ℤ M
h : finrank.{0, u_1} ℤ ↥N = finrank ℤ M
a : Free.ChooseBasisIndex ℤ M → ℤ := smithNormalFormCoeffs b h
b' : Basis (Free.ChooseBasisIndex ℤ M) ℤ M := smithNormalFormTopBasis b h
ab : Basis (Free.ChooseBasisIndex ℤ M) ℤ ↥N := smithNormalFormBotBasis b h
ab_eq :
  ∀ (i : Free.ChooseBasisIndex ℤ M),
    (↑((smithNormalFormBotBasis b h : (a : Free.ChooseBasisIndex ℤ M) → ↥N) i) : M) =
      HSMul.hSMul (β := M) (smithNormalFormCoeffs b h i)
        ((smithNormalFormTopBasis b h : (a : Free.ChooseBasisIndex ℤ M) → M) i : M)
e' : M ≃ₗ[ℤ] ↥N := b'.equiv ab (Equiv.refl (Free.ChooseBasisIndex ℤ M))
f : M →ₗ[ℤ] M := N.subtype ∘ₗ (↑e' : M →ₗ[ℤ] ↥N)
f_apply : ∀ (x : M),
  Eq (α := M) ((f : (a : M) → M) x : M)
    ((↑((b'.equiv ab (Equiv.refl (Free.ChooseBasisIndex ℤ M)) : (a : M) → ↥N) x) : M) : M) :=
  ⋯
⊢ ∀ (i : Free.ChooseBasisIndex ℤ M),
    (f : (a : M) → M) ((b' : (a : Free.ChooseBasisIndex ℤ M) → M) i : M) =
      HSMul.hSMul (β := M) (a i) ((b' : (a : Free.ChooseBasisIndex ℤ M) → M) i : M)

Tactic:
have ha : ∀ i, f (b' i) = a i • b' i := by
    intro i
    rw [f_apply, b'.equiv_apply, Equiv.refl_apply]
    exact ab_eq i
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : Free ℤ M
inst_2 : Module.Finite ℤ M
N : Submodule ℤ M
E : Type u_2
inst_3 : EquivLike E M ↥N
inst_4 : AddEquivClass E M ↥N
e : E
b : Basis (Free.ChooseBasisIndex ℤ M) ℤ M := Free.chooseBasis ℤ M
h : finrank.{0, u_1} ℤ ↥N = finrank ℤ M
a : Free.ChooseBasisIndex ℤ M → ℤ := smithNormalFormCoeffs b h
b' : Basis (Free.ChooseBasisIndex ℤ M) ℤ M := smithNormalFormTopBasis b h
ab : Basis (Free.ChooseBasisIndex ℤ M) ℤ ↥N := smithNormalFormBotBasis b h
ab_eq :
  ∀ (i : Free.ChooseBasisIndex ℤ M),
    (↑((smithNormalFormBotBasis b h : (a : Free.ChooseBasisIndex ℤ M) → ↥N) i) : M) =
      HSMul.hSMul (β := M) (smithNormalFormCoeffs b h i)
        ((smithNormalFormTopBasis b h : (a : Free.ChooseBasisIndex ℤ M) → M) i : M)
e' : M ≃ₗ[ℤ] ↥N := b'.equiv ab (Equiv.refl (Free.ChooseBasisIndex ℤ M))
f : M →ₗ[ℤ] M := N.subtype ∘ₗ (↑e' : M →ₗ[ℤ] ↥N)
f_apply : ∀ (x : M),
  Eq (α := M) ((f : (a : M) → M) x : M)
    ((↑((b'.equiv ab (Equiv.refl (Free.ChooseBasisIndex ℤ M)) : (a : M) → ↥N) x) : M) : M) :=
  ⋯
ha :
  ∀ (i : Free.ChooseBasisIndex ℤ M),
    (f : (a : M) → M) ((b' : (a : Free.ChooseBasisIndex ℤ M) → M) i : M) =
      HSMul.hSMul (β := M) (a i) ((b' : (a : Free.ChooseBasisIndex ℤ M) → M) i : M)
rw rw₁ : Int.natAbs ((LinearMap.det : (a : M →ₗ[ℤ] M) → ℤ) f) = Int.natAbs ((LinearMap.det : (a : M →ₗ[ℤ] M) → ℤ) f)
⊢ Int.natAbs ((LinearMap.det : (a : M →ₗ[ℤ] M) → ℤ) f) =
    Int.natAbs
      (Matrix.det.{0, u_1} (n := Free.ChooseBasisIndex ℤ M)
        ((LinearMap.toMatrix b' b' : (a : M →ₗ[ℤ] M) → Matrix (Free.ChooseBasisIndex ℤ M) (Free.ChooseBasisIndex ℤ M) ℤ)
          f))

Tactic:
rw [LinearMap.det_toMatrix]

Premises used: LinearMap.det_toMatrix
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : Free ℤ M
inst_2 : Module.Finite ℤ M
N : Submodule ℤ M
E : Type u_2
inst_3 : EquivLike E M ↥N
inst_4 : AddEquivClass E M ↥N
e : E
b : Basis (Free.ChooseBasisIndex ℤ M) ℤ M := Free.chooseBasis ℤ M
h : finrank.{0, u_1} ℤ ↥N = finrank ℤ M
a : Free.ChooseBasisIndex ℤ M → ℤ := smithNormalFormCoeffs b h
b' : Basis (Free.ChooseBasisIndex ℤ M) ℤ M := smithNormalFormTopBasis b h
ab : Basis (Free.ChooseBasisIndex ℤ M) ℤ ↥N := smithNormalFormBotBasis b h
ab_eq :
  ∀ (i : Free.ChooseBasisIndex ℤ M),
    (↑((smithNormalFormBotBasis b h : (a : Free.ChooseBasisIndex ℤ M) → ↥N) i) : M) =
      HSMul.hSMul (β := M) (smithNormalFormCoeffs b h i)
        ((smithNormalFormTopBasis b h : (a : Free.ChooseBasisIndex ℤ M) → M) i : M)
e' : M ≃ₗ[ℤ] ↥N := b'.equiv ab (Equiv.refl (Free.ChooseBasisIndex ℤ M))
f : M →ₗ[ℤ] M := N.subtype ∘ₗ (↑e' : M →ₗ[ℤ] ↥N)
f_apply : ∀ (x : M),
  Eq (α := M) ((f : (a : M) → M) x : M)
    ((↑((b'.equiv ab (Equiv.refl (Free.ChooseBasisIndex ℤ M)) : (a : M) → ↥N) x) : M) : M) :=
  ⋯
ha :
  ∀ (i : Free.ChooseBasisIndex ℤ M),
    (f : (a : M) → M) ((b' : (a : Free.ChooseBasisIndex ℤ M) → M) i : M) =
      HSMul.hSMul (β := M) (a i) ((b' : (a : Free.ChooseBasisIndex ℤ M) → M) i : M)
⊢ Int.natAbs
      (Matrix.det.{0, u_1} (n := Free.ChooseBasisIndex ℤ M)
        ((LinearMap.toMatrix b' b' : (a : M →ₗ[ℤ] M) → Matrix (Free.ChooseBasisIndex ℤ M) (Free.ChooseBasisIndex ℤ M) ℤ)
          f)) =
    (Matrix.diagonal a).det.natAbs

Tactic:
?_
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : Free ℤ M
inst_2 : Module.Finite ℤ M
N : Submodule ℤ M
E : Type u_2
inst_3 : EquivLike E M ↥N
inst_4 : AddEquivClass E M ↥N
e : E
b : Basis (Free.ChooseBasisIndex ℤ M) ℤ M := Free.chooseBasis ℤ M
h : finrank.{0, u_1} ℤ ↥N = finrank ℤ M
a : Free.ChooseBasisIndex ℤ M → ℤ := smithNormalFormCoeffs b h
b' : Basis (Free.ChooseBasisIndex ℤ M) ℤ M := smithNormalFormTopBasis b h
ab : Basis (Free.ChooseBasisIndex ℤ M) ℤ ↥N := smithNormalFormBotBasis b h
ab_eq :
  ∀ (i : Free.ChooseBasisIndex ℤ M),
    (↑((smithNormalFormBotBasis b h : (a : Free.ChooseBasisIndex ℤ M) → ↥N) i) : M) =
      HSMul.hSMul (β := M) (smithNormalFormCoeffs b h i)
        ((smithNormalFormTopBasis b h : (a : Free.ChooseBasisIndex ℤ M) → M) i : M)
e' : M ≃ₗ[ℤ] ↥N := b'.equiv ab (Equiv.refl (Free.ChooseBasisIndex ℤ M))
f : M →ₗ[ℤ] M := N.subtype ∘ₗ (↑e' : M →ₗ[ℤ] ↥N)
f_apply : ∀ (x : M),
  Eq (α := M) ((f : (a : M) → M) x : M)
    ((↑((b'.equiv ab (Equiv.refl (Free.ChooseBasisIndex ℤ M)) : (a : M) → ↥N) x) : M) : M) :=
  ⋯
ha :
  ∀ (i : Free.ChooseBasisIndex ℤ M),
    (f : (a : M) → M) ((b' : (a : Free.ChooseBasisIndex ℤ M) → M) i : M) =
      HSMul.hSMul (β := M) (a i) ((b' : (a : Free.ChooseBasisIndex ℤ M) → M) i : M)
rw rw₁ : Int.natAbs (∏ i : Free.ChooseBasisIndex ℤ M, a i) = Int.natAbs (∏ i : Free.ChooseBasisIndex ℤ M, a i)
⊢ (Matrix.diagonal a).det.natAbs = Int.natAbs (∏ i : Free.ChooseBasisIndex ℤ M, a i)

Tactic:
rw [Matrix.det_diagonal]

Premises used: Matrix.det_diagonal
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : Free ℤ M
inst_2 : Module.Finite ℤ M
N : Submodule ℤ M
E : Type u_2
inst_3 : EquivLike E M ↥N
inst_4 : AddEquivClass E M ↥N
e : E
b : Basis (Free.ChooseBasisIndex ℤ M) ℤ M := Free.chooseBasis ℤ M
h : finrank.{0, u_1} ℤ ↥N = finrank ℤ M
a : Free.ChooseBasisIndex ℤ M → ℤ := smithNormalFormCoeffs b h
b' : Basis (Free.ChooseBasisIndex ℤ M) ℤ M := smithNormalFormTopBasis b h
ab : Basis (Free.ChooseBasisIndex ℤ M) ℤ ↥N := smithNormalFormBotBasis b h
ab_eq :
  ∀ (i : Free.ChooseBasisIndex ℤ M),
    (↑((smithNormalFormBotBasis b h : (a : Free.ChooseBasisIndex ℤ M) → ↥N) i) : M) =
      HSMul.hSMul (β := M) (smithNormalFormCoeffs b h i)
        ((smithNormalFormTopBasis b h : (a : Free.ChooseBasisIndex ℤ M) → M) i : M)
e' : M ≃ₗ[ℤ] ↥N := b'.equiv ab (Equiv.refl (Free.ChooseBasisIndex ℤ M))
f : M →ₗ[ℤ] M := N.subtype ∘ₗ (↑e' : M →ₗ[ℤ] ↥N)
f_apply : ∀ (x : M),
  Eq (α := M) ((f : (a : M) → M) x : M)
    ((↑((b'.equiv ab (Equiv.refl (Free.ChooseBasisIndex ℤ M)) : (a : M) → ↥N) x) : M) : M) :=
  ⋯
ha :
  ∀ (i : Free.ChooseBasisIndex ℤ M),
    (f : (a : M) → M) ((b' : (a : Free.ChooseBasisIndex ℤ M) → M) i : M) =
      HSMul.hSMul (β := M) (a i) ((b' : (a : Free.ChooseBasisIndex ℤ M) → M) i : M)
⊢ Int.natAbs (∏ i : Free.ChooseBasisIndex ℤ M, a i) = ∏ i : Free.ChooseBasisIndex ℤ M, (a i).natAbs

Tactic:
map_prod Int.natAbsHom a Finset.univ

Premises used: Finset.univ, Int.natAbsHom, map_prod, Int.natAbs
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : Free ℤ M
inst_2 : Module.Finite ℤ M
N : Submodule ℤ M
E : Type u_2
inst_3 : EquivLike E M ↥N
inst_4 : AddEquivClass E M ↥N
e : E
b : Basis (Free.ChooseBasisIndex ℤ M) ℤ M := Free.chooseBasis ℤ M
h : finrank.{0, u_1} ℤ ↥N = finrank ℤ M
a : Free.ChooseBasisIndex ℤ M → ℤ := smithNormalFormCoeffs b h
b' : Basis (Free.ChooseBasisIndex ℤ M) ℤ M := smithNormalFormTopBasis b h
ab : Basis (Free.ChooseBasisIndex ℤ M) ℤ ↥N := smithNormalFormBotBasis b h
ab_eq :
  ∀ (i : Free.ChooseBasisIndex ℤ M),
    (↑((smithNormalFormBotBasis b h : (a : Free.ChooseBasisIndex ℤ M) → ↥N) i) : M) =
      HSMul.hSMul (β := M) (smithNormalFormCoeffs b h i)
        ((smithNormalFormTopBasis b h : (a : Free.ChooseBasisIndex ℤ M) → M) i : M)
e' : M ≃ₗ[ℤ] ↥N := b'.equiv ab (Equiv.refl (Free.ChooseBasisIndex ℤ M))
f : M →ₗ[ℤ] M := N.subtype ∘ₗ (↑e' : M →ₗ[ℤ] ↥N)
f_apply : ∀ (x : M),
  Eq (α := M) ((f : (a : M) → M) x : M)
    ((↑((b'.equiv ab (Equiv.refl (Free.ChooseBasisIndex ℤ M)) : (a : M) → ↥N) x) : M) : M) :=
  ⋯
ha :
  ∀ (i : Free.ChooseBasisIndex ℤ M),
    (f : (a : M) → M) ((b' : (a : Free.ChooseBasisIndex ℤ M) → M) i : M) =
      HSMul.hSMul (β := M) (a i) ((b' : (a : Free.ChooseBasisIndex ℤ M) → M) i : M)
⊢ ∏ i : Free.ChooseBasisIndex ℤ M, (a i).natAbs = Nat.card.{u_1} (M ⧸ N)

Tactic:
?_
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : Free ℤ M
inst_2 : Module.Finite ℤ M
N : Submodule ℤ M
E : Type u_2
inst_3 : EquivLike E M ↥N
inst_4 : AddEquivClass E M ↥N
e : E
b : Basis (Free.ChooseBasisIndex ℤ M) ℤ M := Free.chooseBasis ℤ M
h : finrank.{0, u_1} ℤ ↥N = finrank ℤ M
a : Free.ChooseBasisIndex ℤ M → ℤ := smithNormalFormCoeffs b h
b' : Basis (Free.ChooseBasisIndex ℤ M) ℤ M := smithNormalFormTopBasis b h
ab : Basis (Free.ChooseBasisIndex ℤ M) ℤ ↥N := smithNormalFormBotBasis b h
ab_eq :
  ∀ (i : Free.ChooseBasisIndex ℤ M),
    (↑((smithNormalFormBotBasis b h : (a : Free.ChooseBasisIndex ℤ M) → ↥N) i) : M) =
      HSMul.hSMul (β := M) (smithNormalFormCoeffs b h i)
        ((smithNormalFormTopBasis b h : (a : Free.ChooseBasisIndex ℤ M) → M) i : M)
e' : M ≃ₗ[ℤ] ↥N := b'.equiv ab (Equiv.refl (Free.ChooseBasisIndex ℤ M))
f : M →ₗ[ℤ] M := N.subtype ∘ₗ (↑e' : M →ₗ[ℤ] ↥N)
f_apply : ∀ (x : M),
  Eq (α := M) ((f : (a : M) → M) x : M)
    ((↑((b'.equiv ab (Equiv.refl (Free.ChooseBasisIndex ℤ M)) : (a : M) → ↥N) x) : M) : M) :=
  ⋯
ha :
  ∀ (i : Free.ChooseBasisIndex ℤ M),
    (f : (a : M) → M) ((b' : (a : Free.ChooseBasisIndex ℤ M) → M) i : M) =
      HSMul.hSMul (β := M) (a i) ((b' : (a : Free.ChooseBasisIndex ℤ M) → M) i : M)
calc_1 :
  Int.natAbs
      (Matrix.det.{0, u_1} (n := Free.ChooseBasisIndex ℤ M)
        ((LinearMap.toMatrix b' b' : (a : M →ₗ[ℤ] M) → Matrix (Free.ChooseBasisIndex ℤ M) (Free.ChooseBasisIndex ℤ M) ℤ)
          f)) =
    (Matrix.diagonal a).det.natAbs
calc_2 : ∏ i : Free.ChooseBasisIndex ℤ M, (a i).natAbs = Nat.card.{u_1} (M ⧸ N)
⊢ Int.natAbs ((LinearMap.det : (a : M →ₗ[ℤ] M) → ℤ) f) = Nat.card.{u_1} (M ⧸ N)

Tactic:
calc
    Int.natAbs (LinearMap.det f) = Int.natAbs (LinearMap.toMatrix b' b' f).det := by
      rw [LinearMap.det_toMatrix]
    _ = Int.natAbs (Matrix.diagonal a).det := ?_
    _ = Int.natAbs (∏ i, a i) := by rw [Matrix.det_diagonal]
    _ = ∏ i, Int.natAbs (a i) := map_prod Int.natAbsHom a Finset.univ
    _ = Nat.card (M ⧸ N) := ?_

Premises used: Finset.univ, Int.natAbsHom, Nat.card, LinearMap.det, map_prod, Finset.prod, HasQuotient.Quotient, Int.natAbs, DFunLike.coe, Matrix.det, Matrix.diagonal, LinearMap.toMatrix
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : Free ℤ M
inst_2 : Module.Finite ℤ M
N : Submodule ℤ M
E : Type u_2
inst_3 : EquivLike E M ↥N
inst_4 : AddEquivClass E M ↥N
e : E
b : Basis (Free.ChooseBasisIndex ℤ M) ℤ M := Free.chooseBasis ℤ M
h : finrank.{0, u_1} ℤ ↥N = finrank ℤ M
a : Free.ChooseBasisIndex ℤ M → ℤ := smithNormalFormCoeffs b h
b' : Basis (Free.ChooseBasisIndex ℤ M) ℤ M := smithNormalFormTopBasis b h
ab : Basis (Free.ChooseBasisIndex ℤ M) ℤ ↥N := smithNormalFormBotBasis b h
ab_eq :
  ∀ (i : Free.ChooseBasisIndex ℤ M),
    (↑((smithNormalFormBotBasis b h : (a : Free.ChooseBasisIndex ℤ M) → ↥N) i) : M) =
      HSMul.hSMul (β := M) (smithNormalFormCoeffs b h i)
        ((smithNormalFormTopBasis b h : (a : Free.ChooseBasisIndex ℤ M) → M) i : M)
e' : M ≃ₗ[ℤ] ↥N := b'.equiv ab (Equiv.refl (Free.ChooseBasisIndex ℤ M))
f : M →ₗ[ℤ] M := N.subtype ∘ₗ (↑e' : M →ₗ[ℤ] ↥N)
f_apply : ∀ (x : M),
  Eq (α := M) ((f : (a : M) → M) x : M)
    ((↑((b'.equiv ab (Equiv.refl (Free.ChooseBasisIndex ℤ M)) : (a : M) → ↥N) x) : M) : M) :=
  ⋯
ha :
  ∀ (i : Free.ChooseBasisIndex ℤ M),
    (f : (a : M) → M) ((b' : (a : Free.ChooseBasisIndex ℤ M) → M) i : M) =
      HSMul.hSMul (β := M) (a i) ((b' : (a : Free.ChooseBasisIndex ℤ M) → M) i : M)
calc_1 :
  (LinearMap.toMatrix b' b' : (a : M →ₗ[ℤ] M) → Matrix (Free.ChooseBasisIndex ℤ M) (Free.ChooseBasisIndex ℤ M) ℤ) f =
    Matrix.diagonal a
⊢ Int.natAbs
      (Matrix.det.{0, u_1} (n := Free.ChooseBasisIndex ℤ M)
        ((LinearMap.toMatrix b' b' : (a : M →ₗ[ℤ] M) → Matrix (Free.ChooseBasisIndex ℤ M) (Free.ChooseBasisIndex ℤ M) ℤ)
          f)) =
    (Matrix.diagonal a).det.natAbs

Tactic:
congr 2
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : Free ℤ M
inst_2 : Module.Finite ℤ M
N : Submodule ℤ M
E : Type u_2
inst_3 : EquivLike E M ↥N
inst_4 : AddEquivClass E M ↥N
e : E
b : Basis (Free.ChooseBasisIndex ℤ M) ℤ M := Free.chooseBasis ℤ M
h : finrank.{0, u_1} ℤ ↥N = finrank ℤ M
a : Free.ChooseBasisIndex ℤ M → ℤ := smithNormalFormCoeffs b h
b' : Basis (Free.ChooseBasisIndex ℤ M) ℤ M := smithNormalFormTopBasis b h
ab : Basis (Free.ChooseBasisIndex ℤ M) ℤ ↥N := smithNormalFormBotBasis b h
ab_eq :
  ∀ (i : Free.ChooseBasisIndex ℤ M),
    (↑((smithNormalFormBotBasis b h : (a : Free.ChooseBasisIndex ℤ M) → ↥N) i) : M) =
      HSMul.hSMul (β := M) (smithNormalFormCoeffs b h i)
        ((smithNormalFormTopBasis b h : (a : Free.ChooseBasisIndex ℤ M) → M) i : M)
e' : M ≃ₗ[ℤ] ↥N := b'.equiv ab (Equiv.refl (Free.ChooseBasisIndex ℤ M))
f : M →ₗ[ℤ] M := N.subtype ∘ₗ (↑e' : M →ₗ[ℤ] ↥N)
f_apply : ∀ (x : M),
  Eq (α := M) ((f : (a : M) → M) x : M)
    ((↑((b'.equiv ab (Equiv.refl (Free.ChooseBasisIndex ℤ M)) : (a : M) → ↥N) x) : M) : M) :=
  ⋯
ha :
  ∀ (i : Free.ChooseBasisIndex ℤ M),
    (f : (a : M) → M) ((b' : (a : Free.ChooseBasisIndex ℤ M) → M) i : M) =
      HSMul.hSMul (β := M) (a i) ((b' : (a : Free.ChooseBasisIndex ℤ M) → M) i : M)
calc_1 :
  ∀ (i j : Free.ChooseBasisIndex ℤ M),
    (LinearMap.toMatrix b' b' : (a : M →ₗ[ℤ] M) → Matrix (Free.ChooseBasisIndex ℤ M) (Free.ChooseBasisIndex ℤ M) ℤ) f i
        j =
      Matrix.diagonal a i j
⊢ (LinearMap.toMatrix b' b' : (a : M →ₗ[ℤ] M) → Matrix (Free.ChooseBasisIndex ℤ M) (Free.ChooseBasisIndex ℤ M) ℤ) f =
    Matrix.diagonal a

Tactic:
ext i j
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : Free ℤ M
inst_2 : Module.Finite ℤ M
N : Submodule ℤ M
E : Type u_2
inst_3 : EquivLike E M ↥N
inst_4 : AddEquivClass E M ↥N
e : E
b : Basis (Free.ChooseBasisIndex ℤ M) ℤ M := Free.chooseBasis ℤ M
h : finrank.{0, u_1} ℤ ↥N = finrank ℤ M
a : Free.ChooseBasisIndex ℤ M → ℤ := smithNormalFormCoeffs b h
b' : Basis (Free.ChooseBasisIndex ℤ M) ℤ M := smithNormalFormTopBasis b h
ab : Basis (Free.ChooseBasisIndex ℤ M) ℤ ↥N := smithNormalFormBotBasis b h
ab_eq :
  ∀ (i : Free.ChooseBasisIndex ℤ M),
    (↑((smithNormalFormBotBasis b h : (a : Free.ChooseBasisIndex ℤ M) → ↥N) i) : M) =
      HSMul.hSMul (β := M) (smithNormalFormCoeffs b h i)
        ((smithNormalFormTopBasis b h : (a : Free.ChooseBasisIndex ℤ M) → M) i : M)
e' : M ≃ₗ[ℤ] ↥N := b'.equiv ab (Equiv.refl (Free.ChooseBasisIndex ℤ M))
f : M →ₗ[ℤ] M := N.subtype ∘ₗ (↑e' : M →ₗ[ℤ] ↥N)
f_apply : ∀ (x : M),
  Eq (α := M) ((f : (a : M) → M) x : M)
    ((↑((b'.equiv ab (Equiv.refl (Free.ChooseBasisIndex ℤ M)) : (a : M) → ↥N) x) : M) : M) :=
  ⋯
ha :
  ∀ (i : Free.ChooseBasisIndex ℤ M),
    (f : (a : M) → M) ((b' : (a : Free.ChooseBasisIndex ℤ M) → M) i : M) =
      HSMul.hSMul (β := M) (a i) ((b' : (a : Free.ChooseBasisIndex ℤ M) → M) i : M)
i j : Free.ChooseBasisIndex ℤ M
calc_1 : (Finsupp.single j (a j) : (a : Free.ChooseBasisIndex ℤ M) → ℤ) i = Matrix.diagonal a i j
⊢ (LinearMap.toMatrix b' b' : (a : M →ₗ[ℤ] M) → Matrix (Free.ChooseBasisIndex ℤ M) (Free.ChooseBasisIndex ℤ M) ℤ) f i
      j =
    Matrix.diagonal a i j

Tactic:
rw [LinearMap.toMatrix_apply, ha, map_smul, Basis.repr_self, Finsupp.smul_single,
      smul_eq_mul, mul_one]

Premises used: smul_eq_mul, mul_one, Finsupp.smul_single, Module.Basis.repr_self, LinearMap.toMatrix_apply, map_smul
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : Free ℤ M
inst_2 : Module.Finite ℤ M
N : Submodule ℤ M
E : Type u_2
inst_3 : EquivLike E M ↥N
inst_4 : AddEquivClass E M ↥N
e : E
b : Basis (Free.ChooseBasisIndex ℤ M) ℤ M := Free.chooseBasis ℤ M
h : finrank.{0, u_1} ℤ ↥N = finrank ℤ M
a : Free.ChooseBasisIndex ℤ M → ℤ := smithNormalFormCoeffs b h
b' : Basis (Free.ChooseBasisIndex ℤ M) ℤ M := smithNormalFormTopBasis b h
ab : Basis (Free.ChooseBasisIndex ℤ M) ℤ ↥N := smithNormalFormBotBasis b h
ab_eq :
  ∀ (i : Free.ChooseBasisIndex ℤ M),
    (↑((smithNormalFormBotBasis b h : (a : Free.ChooseBasisIndex ℤ M) → ↥N) i) : M) =
      HSMul.hSMul (β := M) (smithNormalFormCoeffs b h i)
        ((smithNormalFormTopBasis b h : (a : Free.ChooseBasisIndex ℤ M) → M) i : M)
e' : M ≃ₗ[ℤ] ↥N := b'.equiv ab (Equiv.refl (Free.ChooseBasisIndex ℤ M))
f : M →ₗ[ℤ] M := N.subtype ∘ₗ (↑e' : M →ₗ[ℤ] ↥N)
f_apply : ∀ (x : M),
  Eq (α := M) ((f : (a : M) → M) x : M)
    ((↑((b'.equiv ab (Equiv.refl (Free.ChooseBasisIndex ℤ M)) : (a : M) → ↥N) x) : M) : M) :=
  ⋯
ha :
  ∀ (i : Free.ChooseBasisIndex ℤ M),
    (f : (a : M) → M) ((b' : (a : Free.ChooseBasisIndex ℤ M) → M) i : M) =
      HSMul.hSMul (β := M) (a i) ((b' : (a : Free.ChooseBasisIndex ℤ M) → M) i : M)
i j : Free.ChooseBasisIndex ℤ M
pos : ∀ (h : i = j), (Finsupp.single j (a j) : (a : Free.ChooseBasisIndex ℤ M) → ℤ) i = Matrix.diagonal a i j
neg : ∀ (h : ¬i = j), (Finsupp.single j (a j) : (a : Free.ChooseBasisIndex ℤ M) → ℤ) i = Matrix.diagonal a i j
⊢ (Finsupp.single j (a j) : (a : Free.ChooseBasisIndex ℤ M) → ℤ) i = Matrix.diagonal a i j

Tactic:
by_cases h : i = j
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : Free ℤ M
inst_2 : Module.Finite ℤ M
N : Submodule ℤ M
E : Type u_2
inst_3 : EquivLike E M ↥N
inst_4 : AddEquivClass E M ↥N
e : E
b : Basis (Free.ChooseBasisIndex ℤ M) ℤ M := Free.chooseBasis ℤ M
h_1 : finrank.{0, u_1} ℤ ↥N = finrank ℤ M
a : Free.ChooseBasisIndex ℤ M → ℤ := smithNormalFormCoeffs b h_1
b' : Basis (Free.ChooseBasisIndex ℤ M) ℤ M := smithNormalFormTopBasis b h_1
ab : Basis (Free.ChooseBasisIndex ℤ M) ℤ ↥N := smithNormalFormBotBasis b h_1
ab_eq :
  ∀ (i : Free.ChooseBasisIndex ℤ M),
    (↑((smithNormalFormBotBasis b h_1 : (a : Free.ChooseBasisIndex ℤ M) → ↥N) i) : M) =
      HSMul.hSMul (β := M) (smithNormalFormCoeffs b h_1 i)
        ((smithNormalFormTopBasis b h_1 : (a : Free.ChooseBasisIndex ℤ M) → M) i : M)
e' : M ≃ₗ[ℤ] ↥N := b'.equiv ab (Equiv.refl (Free.ChooseBasisIndex ℤ M))
f : M →ₗ[ℤ] M := N.subtype ∘ₗ (↑e' : M →ₗ[ℤ] ↥N)
f_apply : ∀ (x : M),
  Eq (α := M) ((f : (a : M) → M) x : M)
    ((↑((b'.equiv ab (Equiv.refl (Free.ChooseBasisIndex ℤ M)) : (a : M) → ↥N) x) : M) : M) :=
  ⋯
ha :
  ∀ (i : Free.ChooseBasisIndex ℤ M),
    (f : (a : M) → M) ((b' : (a : Free.ChooseBasisIndex ℤ M) → M) i : M) =
      HSMul.hSMul (β := M) (a i) ((b' : (a : Free.ChooseBasisIndex ℤ M) → M) i : M)
i j : Free.ChooseBasisIndex ℤ M
h : i = j
pos : (Finsupp.single j (a j) : (a : Free.ChooseBasisIndex ℤ M) → ℤ) j = Matrix.diagonal a j j
pos₁ : (Finsupp.single j (a j) : (a : Free.ChooseBasisIndex ℤ M) → ℤ) j = a j
pos₂ pos₃ : a j = a j
⊢ (Finsupp.single j (a j) : (a : Free.ChooseBasisIndex ℤ M) → ℤ) i = Matrix.diagonal a i j

Tactic:
rw [h, Matrix.diagonal_apply_eq, Finsupp.single_eq_same]

Premises used: Finsupp.single_eq_same, Matrix.diagonal_apply_eq
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : Free ℤ M
inst_2 : Module.Finite ℤ M
N : Submodule ℤ M
E : Type u_2
inst_3 : EquivLike E M ↥N
inst_4 : AddEquivClass E M ↥N
e : E
b : Basis (Free.ChooseBasisIndex ℤ M) ℤ M := Free.chooseBasis ℤ M
h_1 : finrank.{0, u_1} ℤ ↥N = finrank ℤ M
a : Free.ChooseBasisIndex ℤ M → ℤ := smithNormalFormCoeffs b h_1
b' : Basis (Free.ChooseBasisIndex ℤ M) ℤ M := smithNormalFormTopBasis b h_1
ab : Basis (Free.ChooseBasisIndex ℤ M) ℤ ↥N := smithNormalFormBotBasis b h_1
ab_eq :
  ∀ (i : Free.ChooseBasisIndex ℤ M),
    (↑((smithNormalFormBotBasis b h_1 : (a : Free.ChooseBasisIndex ℤ M) → ↥N) i) : M) =
      HSMul.hSMul (β := M) (smithNormalFormCoeffs b h_1 i)
        ((smithNormalFormTopBasis b h_1 : (a : Free.ChooseBasisIndex ℤ M) → M) i : M)
e' : M ≃ₗ[ℤ] ↥N := b'.equiv ab (Equiv.refl (Free.ChooseBasisIndex ℤ M))
f : M →ₗ[ℤ] M := N.subtype ∘ₗ (↑e' : M →ₗ[ℤ] ↥N)
f_apply : ∀ (x : M),
  Eq (α := M) ((f : (a : M) → M) x : M)
    ((↑((b'.equiv ab (Equiv.refl (Free.ChooseBasisIndex ℤ M)) : (a : M) → ↥N) x) : M) : M) :=
  ⋯
ha :
  ∀ (i : Free.ChooseBasisIndex ℤ M),
    (f : (a : M) → M) ((b' : (a : Free.ChooseBasisIndex ℤ M) → M) i : M) =
      HSMul.hSMul (β := M) (a i) ((b' : (a : Free.ChooseBasisIndex ℤ M) → M) i : M)
i j : Free.ChooseBasisIndex ℤ M
h : ¬i = j
neg : Eq (α := ℤ) ((Finsupp.single j (a j) : (a : Free.ChooseBasisIndex ℤ M) → ℤ) i : ℤ) (0 : ℤ)
neg₁ neg₂ : Eq (α := ℤ) 0 0
⊢ (Finsupp.single j (a j) : (a : Free.ChooseBasisIndex ℤ M) → ℤ) i = Matrix.diagonal a i j

Tactic:
rw [Matrix.diagonal_apply_ne _ h, Finsupp.single_eq_of_ne h]

Premises used: Finsupp.single_eq_of_ne, Matrix.diagonal_apply_ne