awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ (Finsupp.single j (a j) : (a : Free.ChooseBasisIndex ℤ M) → ℤ) i = Matrix.diagonal a i j
have pos : ∀ (h : i = j), (Finsupp.single j (a j) : (a : Free.ChooseBasisIndex ℤ M) → ℤ) i = Matrix.diagonal a i j
Tactic: by_cases h : 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
pos : ∀ (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
have neg : ∀ (h : ¬i = j), (Finsupp.single j (a j) : (a : Free.ChooseBasisIndex ℤ M) → ℤ) i = Matrix.diagonal a i j
Tactic: by_cases h : 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_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
⊢ (Finsupp.single j (a j) : (a : Free.ChooseBasisIndex ℤ M) → ℤ) i = Matrix.diagonal a i j
have pos : (Finsupp.single j (a j) : (a : Free.ChooseBasisIndex ℤ M) → ℤ) j = Matrix.diagonal a j j
Tactic: rw [h, Matrix.diagonal_apply_eq, Finsupp.single_eq_same]
-- 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_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
⊢ (Finsupp.single j (a j) : (a : Free.ChooseBasisIndex ℤ M) → ℤ) i = Matrix.diagonal a i j
have pos₁ : (Finsupp.single j (a j) : (a : Free.ChooseBasisIndex ℤ M) → ℤ) j = a j
Tactic: rw [h, Matrix.diagonal_apply_eq, Finsupp.single_eq_same]
-- 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_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
⊢ (Finsupp.single j (a j) : (a : Free.ChooseBasisIndex ℤ M) → ℤ) i = Matrix.diagonal a i j
have pos₂ : a j = a j
Tactic: rw [h, Matrix.diagonal_apply_eq, Finsupp.single_eq_same]
-- 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_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
⊢ (Finsupp.single j (a j) : (a : Free.ChooseBasisIndex ℤ M) → ℤ) i = Matrix.diagonal a i j
have neg : Eq (α := ℤ) ((Finsupp.single j (a j) : (a : Free.ChooseBasisIndex ℤ M) → ℤ) i : ℤ) (0 : ℤ)
Tactic: rw [Matrix.diagonal_apply_ne _ h, Finsupp.single_eq_of_ne 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_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 : ℤ)
⊢ (Finsupp.single j (a j) : (a : Free.ChooseBasisIndex ℤ M) → ℤ) i = Matrix.diagonal a i j
have neg₁ : Eq (α := ℤ) 0 0
Tactic: rw [Matrix.diagonal_apply_ne _ h, Finsupp.single_eq_of_ne 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) :=
  ⋯
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)
have calc_2 : ∏ i : Free.ChooseBasisIndex ℤ M, (a i).natAbs =
  Nat.card.{u_1} ((i : Free.ChooseBasisIndex ℤ M) → ZMod (smithNormalFormCoeffs b h i).natAbs)
Tactic: simp_rw [Nat.card_congr (quotientEquivPiZMod N b h).toEquiv, Nat.card_pi, Nat.card_zmod, a]
-- 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_2 :
  ∏ i : Free.ChooseBasisIndex ℤ M, (a i).natAbs =
    Nat.card.{u_1} ((i : Free.ChooseBasisIndex ℤ M) → ZMod (smithNormalFormCoeffs b h i).natAbs)
⊢ ∏ i : Free.ChooseBasisIndex ℤ M, (a i).natAbs = Nat.card.{u_1} (M ⧸ N)
have calc_2₁ : Eq (α := ℕ) (∏ i : Free.ChooseBasisIndex ℤ M, (a i).natAbs)
  (∏ a : Free.ChooseBasisIndex ℤ M, Nat.card (ZMod (smithNormalFormCoeffs b h a).natAbs))
Tactic: simp_rw [Nat.card_congr (quotientEquivPiZMod N b h).toEquiv, Nat.card_pi, Nat.card_zmod, a]
-- 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_2 :
  ∏ i : Free.ChooseBasisIndex ℤ M, (a i).natAbs =
    Nat.card.{u_1} ((i : Free.ChooseBasisIndex ℤ M) → ZMod (smithNormalFormCoeffs b h i).natAbs)
calc_2₁ :
  Eq (α := ℕ) (∏ i : Free.ChooseBasisIndex ℤ M, (a i).natAbs)
    (∏ a : Free.ChooseBasisIndex ℤ M, Nat.card (ZMod (smithNormalFormCoeffs b h a).natAbs))
⊢ ∏ i : Free.ChooseBasisIndex ℤ M, (a i).natAbs = Nat.card.{u_1} (M ⧸ N)
have calc_2₂ : Eq (α := ℕ) (∏ i : Free.ChooseBasisIndex ℤ M, (a i).natAbs)
  (∏ x : Free.ChooseBasisIndex ℤ M, (smithNormalFormCoeffs b h x).natAbs)
Tactic: simp_rw [Nat.card_congr (quotientEquivPiZMod N b h).toEquiv, Nat.card_pi, Nat.card_zmod, a]
-- 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
ι : Type u_2
inst_3 : Fintype ι
inst_4 : DecidableEq ι
b : Basis ι ℤ M
N : Submodule ℤ M
bN : Basis.{u_2, 0, u_1} ι ℤ ↥N
e : M ≃ₗ[ℤ] ↥N := b.equiv bN (Equiv.refl ι)
⊢ Int.natAbs ((b.det : (a : ι → M) → ℤ) (Function.comp (β := ↥N) (⇑N.subtype : (a : ↥N) → M) (⇑bN : (a : ι) → ↥N))) =
    Int.natAbs ((LinearMap.det : (a : M →ₗ[ℤ] M) → ℤ) (N.subtype ∘ₗ (↑e : M →ₗ[ℤ] ↥N)))
have rw : Int.natAbs ((LinearMap.det : (a : M →ₗ[ℤ] M) → ℤ) (N.subtype ∘ₗ (↑(b.equiv bN (Equiv.refl ι)) : M →ₗ[ℤ] ↥N))) =
  Int.natAbs ((LinearMap.det : (a : M →ₗ[ℤ] M) → ℤ) (N.subtype ∘ₗ (↑e : M →ₗ[ℤ] ↥N)))
Tactic: rw [Basis.det_comp_basis]
-- 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
ι : Type u_2
inst_3 : Fintype ι
inst_4 : DecidableEq ι
b : Basis ι ℤ M
N : Submodule ℤ M
bN : Basis.{u_2, 0, u_1} ι ℤ ↥N
e : M ≃ₗ[ℤ] ↥N := b.equiv bN (Equiv.refl ι)
⊢ Int.natAbs
      ((b.det : (a : ι → M) → ℤ)
        (Function.comp (β := ↥N) (Subtype.val (p := fun (x : M) ↦ x ∈ N)) (⇑bN : (a : ι) → ↥N))) =
    Nat.card.{u_1} (M ⧸ N)
have M₁ : Int.natAbs ((b.det : (a : ι → M) → ℤ) (Function.comp (β := ↥N) (⇑N.subtype : (a : ↥N) → M) (⇑bN : (a : ι) → ↥N))) =
  Int.natAbs ((LinearMap.det : (a : M →ₗ[ℤ] M) → ℤ) (N.subtype ∘ₗ (↑e : M →ₗ[ℤ] ↥N)))
Tactic: calc
    (b.det (N.subtype ∘ bN)).natAbs = (LinearMap.det (N.subtype ∘ₗ (e : M →ₗ[ℤ] N))).natAbs := by
      rw [Basis.det_comp_basis]
    _ = _ := natAbs_det_equiv N e
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
L₁ L₂ : AddSubgroup E
H : L₁ ≤ L₂
ι : Type u_2
inst_1 : DecidableEq ι
inst_2 : Fintype ι
b₁ : Basis.{u_2, 0, u_1} ι ℤ ↥((toIntSubmodule : (a : AddSubgroup E) → Submodule ℤ E) L₁ : Submodule ℤ E)
b₂ : Basis.{u_2, 0, u_1} ι ℤ ↥((toIntSubmodule : (a : AddSubgroup E) → Submodule ℤ E) L₂ : Submodule ℤ E)
⊢ L₁.relIndex L₂ =
    Int.natAbs
      ((b₂.det : (a : ι → ↥((toIntSubmodule : (a : AddSubgroup E) → Submodule ℤ E) L₂)) → ℤ) fun (i : ι) ↦
        Subtype.mk (p := fun (x : E) ↦
          Membership.mem (γ := Submodule ℤ E)
            ((toIntSubmodule : (a : AddSubgroup E) → Submodule ℤ E) L₂ : Submodule ℤ E) x)
          (↑((b₁ : (a : ι) → ↥((toIntSubmodule : (a : AddSubgroup E) → Submodule ℤ E) L₁)) i) : E) ⋯)
have rw : Int.natAbs
    ((b₂.det : (a : ι → ↥((toIntSubmodule : (a : AddSubgroup E) → Submodule ℤ E) L₂)) → ℤ) fun (x : ι) ↦
      (↑(((b₁.map (LinearEquiv.symm (addSubgroupOfEquivOfLe H).toIntLinearEquiv) :
                Basis.{u_2, 0, u_1} ι ℤ ↥(L₁.addSubgroupOf L₂)) :
              (a : ι) → ↥(L₁.addSubgroupOf L₂))
            x) :
        ↥((toIntSubmodule : (a : AddSubgroup E) → Submodule ℤ E) L₂))) =
  Int.natAbs
    ((b₂.det : (a : ι → ↥((toIntSubmodule : (a : AddSubgroup E) → Submodule ℤ E) L₂)) → ℤ) fun (i : ι) ↦
      Subtype.mk (p := fun (x : E) ↦
        Membership.mem (γ := Submodule ℤ E) ((toIntSubmodule : (a : AddSubgroup E) → Submodule ℤ E) L₂ : Submodule ℤ E)
          x)
        (↑((b₁ : (a : ι) → ↥((toIntSubmodule : (a : AddSubgroup E) → Submodule ℤ E) L₁)) i) : E) sorry)
Tactic: rw [relIndex, index_eq_natAbs_det b₂ _ (b₁.map (addSubgroupOfEquivOfLe H).toIntLinearEquiv.symm)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℚ E
L₁ L₂ : AddSubgroup E
H : L₁ ≤ L₂
ι : Type u_2
inst_2 : DecidableEq ι
inst_3 : Fintype ι
b₁ b₂ : Basis ι ℚ E
h₁ : L₁ = closure (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b₁ : (a : ι) → E))
h₂ : L₂ = closure (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b₂ : (a : ι) → E))
⊢ Eq (α := ℚ) ((↑(L₁.relIndex L₂) : ℚ) : ℚ) (|(b₂.det : (a : ι → E) → ℚ) (⇑b₁ : (a : ι) → E)| : ℚ)
have rw : Eq (α := ℚ)
  (|(↑(((Basis.addSubgroupOfClosure L₂ b₂ h₂).det :
              (a : ι → ↥((toIntSubmodule : (a : AddSubgroup E) → Submodule ℤ E) L₂)) → ℤ)
            fun (i : ι) ↦
            Subtype.mk (p := fun (x : E) ↦
              Membership.mem (γ := Submodule ℤ E)
                ((toIntSubmodule : (a : AddSubgroup E) → Submodule ℤ E) L₂ : Submodule ℤ E) x)
              (↑((Basis.addSubgroupOfClosure L₁ b₁ h₁ :
                      (a : ι) → ↥((toIntSubmodule : (a : AddSubgroup E) → Submodule ℤ E) L₁))
                    i) :
                E)
              sorry) :
        ℚ)| :
    ℚ)
  (|(b₂.det : (a : ι → E) → ℚ) (⇑b₁ : (a : ι) → E)| : ℚ)
Tactic: rw [AddSubgroup.relIndex_eq_natAbs_det L₁ L₂ H (b₁.addSubgroupOfClosure L₁ h₁)
    (b₂.addSubgroupOfClosure L₂ h₂), Nat.cast_natAbs, Int.cast_abs]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℚ E
L₁ L₂ : AddSubgroup E
H : L₁ ≤ L₂
ι : Type u_2
inst_2 : DecidableEq ι
inst_3 : Fintype ι
b₁ b₂ : Basis ι ℚ E
h₁ : L₁ = closure (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b₁ : (a : ι) → E))
h₂ : L₂ = closure (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b₂ : (a : ι) → E))
⊢ Eq (α := ℚ)
    (|(algebraMap ℤ ℚ : (a : ℤ) → ℚ)
          (((Basis.addSubgroupOfClosure L₂ b₂ h₂).det :
                (a : ι → ↥((toIntSubmodule : (a : AddSubgroup E) → Submodule ℤ E) L₂)) → ℤ)
              fun (i : ι) ↦
              Subtype.mk (p := fun (x : E) ↦
                Membership.mem (γ := Submodule ℤ E)
                  ((toIntSubmodule : (a : AddSubgroup E) → Submodule ℤ E) L₂ : Submodule ℤ E) x)
                (↑((Basis.addSubgroupOfClosure L₁ b₁ h₁ :
                        (a : ι) → ↥((toIntSubmodule : (a : AddSubgroup E) → Submodule ℤ E) L₁))
                      i) :
                  E)
                ⋯ :
            ℤ)| :
      ℚ)
    (|(b₂.det : (a : ι → E) → ℚ) (⇑b₁ : (a : ι) → E)| : ℚ)
have rw : |Matrix.det.{0, u_2} (n := ι)
      ((RingHom.mapMatrix (algebraMap ℤ ℚ) : (a : Matrix ι ι ℤ) → Matrix ι ι ℚ)
        ((Basis.addSubgroupOfClosure L₂ b₂ h₂).toMatrix fun (i : ι) ↦
          Subtype.mk (p := fun (x : E) ↦
            Membership.mem (γ := Submodule ℤ E)
              ((toIntSubmodule : (a : AddSubgroup E) → Submodule ℤ E) L₂ : Submodule ℤ E) x)
            (↑((Basis.addSubgroupOfClosure L₁ b₁ h₁ :
                    (a : ι) → ↥((toIntSubmodule : (a : AddSubgroup E) → Submodule ℤ E) L₁))
                  i) :
              E)
            sorry))| =
  |Matrix.det (b₂.toMatrix (⇑b₁ : (a : ι) → E))|
Tactic: rw [Basis.det_apply, Basis.det_apply, RingHom.map_det]