awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Basic (hypothesis)
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
f : End R M
h :
  ∀ (g : End R M) (x : M),
    Eq (α := M) ((g : (a : M) → M) ((f : (a : M) → M) x : M) : M) ((f : (a : M) → M) ((g : (a : M) → M) x : M) : M)
h_1 : Nontrivial M
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
i : Free.ChooseBasisIndex R M := ⋯.some
⊢ ∃ (α : R) (h : ∀ (g : R), g * α = α * g),
    ∀ (x : M), Eq (α := M) ((f : (a : M) → M) x : M) ((smulLeft α ⋯ : (a : M) → M) x : M)
have H : ∀ (x : M),
  (f : (a : M) → M) x =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R)
      ((((b.repr : (a : M) → Free.ChooseBasisIndex R M →₀ R)
                ((f : (a : M) → M) ((b : (a : Free.ChooseBasisIndex R M) → M) i : M)) :
              Finsupp.{u_3, u_2} (Free.ChooseBasisIndex R M) R) :
            (a : Free.ChooseBasisIndex R M) → R)
          i :
        R)
      x
Tactic: have H x : f x = b.repr (f (b i)) i • x := by simpa using (h ((b.coord i).smulRight x) (b i)).symm
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Determinant (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Free R M
inst_4 : Module.Finite R M
inst_5 : Nontrivial M
this : Nonempty.{u_2 + 1} (Module.Free.ChooseBasisIndex R M) := ⋯
⊢ Eq.{u_1 + 1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) 0 : R) (0 : R)
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Finite.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : Module.Finite R M
⊢ Fintype (ChooseBasisIndex R M)
have refine : Finite.{v + 1} (ChooseBasisIndex R M)
Tactic: refine @Fintype.ofFinite _ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Finite.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : Module.Finite R M
⊢ Finite.{v + 1} (ChooseBasisIndex R M)
have inl : Subsingleton R → Finite.{v + 1} (ChooseBasisIndex R M)
Tactic: cases subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Finite.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : Module.Finite R M
inl : Subsingleton R → Finite.{v + 1} (ChooseBasisIndex R M)
⊢ Finite.{v + 1} (ChooseBasisIndex R M)
have inr : Nontrivial R → Finite.{v + 1} (ChooseBasisIndex R M)
Tactic: cases subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Finite.Basic (hypothesis)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : Module.Finite R M
h : Subsingleton R
⊢ Finite.{v + 1} (ChooseBasisIndex R M)
have this : Subsingleton M
Tactic: have := Module.subsingleton R M
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Finite.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
ι : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Finite ι
b : Basis ι R M
⊢ Module.Finite R M
have intro : ∀ (val : Fintype ι), Module.Finite R M
Tactic: cases nonempty_fintype ι
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Finite.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
ι : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Finite ι
b : Basis ι R M
val : Fintype ι
⊢ Module.Finite R M
have intro : Eq (α := Submodule R M) (Submodule.span R (↑(Finset.image.{u_3, u_2} (α := ι) (⇑b : (a : ι) → M) Finset.univ) : Set M))
  ⊤
Tactic: refine ⟨⟨Finset.univ.image b, ?_⟩⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Finite.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
ι : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Finite ι
b : Basis ι R M
val : Fintype ι
⊢ Module.Finite R M
have intro : Eq (α := Submodule R M) (Submodule.span R (↑(Finset.image.{u_3, u_2} (α := ι) (⇑b : (a : ι) → M) Finset.univ) : Set M))
  ⊤
Tactic: classical
    refine ⟨⟨Finset.univ.image b, ?_⟩⟩
    simp only [Set.image_univ, Finset.coe_univ, Finset.coe_image, Basis.span_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Finite.Basic (goal)
Goal:
R : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : Module.Finite R M
inst_5 : Finite ι₁
inst_6 : Finite ι₂
⊢ Module.Finite R (Matrix ι₁ ι₂ M)
have intro : ∀ (val : Fintype ι₁), Module.Finite R (Matrix ι₁ ι₂ M)
Tactic: cases nonempty_fintype ι₁
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Finite.Basic (goal)
Goal:
R : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : Module.Finite R M
inst_5 : Finite ι₁
inst_6 : Finite ι₂
val : Fintype ι₁
⊢ Module.Finite R (Matrix ι₁ ι₂ M)
have intro : ∀ (val : Fintype ι₂), Module.Finite R (Matrix ι₁ ι₂ M)
Tactic: cases nonempty_fintype ι₂
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient (hypothesis)
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
⊢ Int.natAbs ((LinearMap.det : (a : M →ₗ[ℤ] M) → ℤ) (N.subtype ∘ₗ AddMonoidHom.toIntLinearMap (↑e : M →+ ↥N))) =
    Nat.card.{u_1} (M ⧸ N)
have h : finrank.{0, u_1} ℤ ↥N = finrank ℤ M
Tactic: have h : Module.finrank ℤ N = Module.finrank ℤ M :=
    (AddEquiv.toIntLinearEquiv e : M ≃ₗ[ℤ] N).symm.finrank_eq
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient (hypothesis)
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
⊢ Int.natAbs ((LinearMap.det : (a : M →ₗ[ℤ] M) → ℤ) (N.subtype ∘ₗ AddMonoidHom.toIntLinearMap (↑e : M →+ ↥N))) =
    Nat.card.{u_1} (M ⧸ N)
have 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)
Tactic: have ab_eq := smithNormalFormBotBasis_def b h
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient (goal)
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) :=
  ⋯
⊢ Int.natAbs ((LinearMap.det : (a : M →ₗ[ℤ] M) → ℤ) (N.subtype ∘ₗ AddMonoidHom.toIntLinearMap (↑e : M →+ ↥N))) =
    Nat.card.{u_1} (M ⧸ N)
have suffices : Int.natAbs ((LinearMap.det : (a : M →ₗ[ℤ] M) → ℤ) f) = Nat.card.{u_1} (M ⧸ N)
Tactic: suffices (LinearMap.det f).natAbs = Nat.card (M ⧸ N) by
    calc
      _ = (LinearMap.det (N.subtype ∘ₗ
            (AddEquiv.toIntLinearEquiv e : M ≃ₗ[ℤ] N))).natAbs := rfl
      _ = (LinearMap.det (N.subtype ∘ₗ _)).natAbs :=
            Int.natAbs_eq_iff_associated.mpr (LinearMap.associated_det_comp_equiv _ _ _)
      _ = Nat.card (M ⧸ N) := this
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient (goal)
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)
have rw : (↑((ab : (a : Free.ChooseBasisIndex ℤ M) → ↥N) i) : M) =
  HSMul.hSMul (β := M) (a i) ((b' : (a : Free.ChooseBasisIndex ℤ M) → M) i : M)
Tactic: rw [f_apply, b'.equiv_apply, Equiv.refl_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient (hypothesis)
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) :=
  ⋯
⊢ Int.natAbs ((LinearMap.det : (a : M →ₗ[ℤ] M) → ℤ) f) = Nat.card.{u_1} (M ⧸ N)
have 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)
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
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient (goal)
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 ((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))
have rw : Int.natAbs ((LinearMap.det : (a : M →ₗ[ℤ] M) → ℤ) f) = Int.natAbs ((LinearMap.det : (a : M →ₗ[ℤ] M) → ℤ) f)
Tactic: rw [LinearMap.det_toMatrix]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient (goal)
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)
⊢ (Matrix.diagonal a).det.natAbs = Int.natAbs (∏ i : Free.ChooseBasisIndex ℤ M, a i)
have rw : Int.natAbs (∏ i : Free.ChooseBasisIndex ℤ M, a i) = Int.natAbs (∏ i : Free.ChooseBasisIndex ℤ M, a i)
Tactic: rw [Matrix.det_diagonal]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient (goal)
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 ((LinearMap.det : (a : M →ₗ[ℤ] M) → ℤ) f) = Nat.card.{u_1} (M ⧸ N)
have 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
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) := ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient (goal)
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
⊢ Int.natAbs ((LinearMap.det : (a : M →ₗ[ℤ] M) → ℤ) f) = Nat.card.{u_1} (M ⧸ N)
have calc_2 : ∏ i : Free.ChooseBasisIndex ℤ M, (a i).natAbs = 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) := ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient (goal)
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
have calc_1 : (LinearMap.toMatrix b' b' : (a : M →ₗ[ℤ] M) → Matrix (Free.ChooseBasisIndex ℤ M) (Free.ChooseBasisIndex ℤ M) ℤ) f =
  Matrix.diagonal a
Tactic: congr 2
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient (goal)
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)
⊢ (LinearMap.toMatrix b' b' : (a : M →ₗ[ℤ] M) → Matrix (Free.ChooseBasisIndex ℤ M) (Free.ChooseBasisIndex ℤ M) ℤ) f =
    Matrix.diagonal a
have 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
Tactic: ext i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient (goal)
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
⊢ (LinearMap.toMatrix b' b' : (a : M →ₗ[ℤ] M) → Matrix (Free.ChooseBasisIndex ℤ M) (Free.ChooseBasisIndex ℤ M) ℤ) f i
      j =
    Matrix.diagonal a i j
have calc_1 : (Finsupp.single j (a j) : (a : Free.ChooseBasisIndex ℤ M) → ℤ) i = Matrix.diagonal a i j
Tactic: rw [LinearMap.toMatrix_apply, ha, map_smul, Basis.repr_self, Finsupp.smul_single,
      smul_eq_mul, mul_one]