awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.FreeModule.Basic
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
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
r : R
⊢ HMul.hMul (β := R) r
      ((b.coord i : (a : M) → R) ((f : (a : M) → M) ((b : (a : Free.ChooseBasisIndex R M) → M) i : M) : M) : R) =
    HMul.hMul (α := R)
      ((b.coord i : (a : M) → R) ((f : (a : M) → M) ((b : (a : Free.ChooseBasisIndex R M) → M) i : M) : M) : R) r

Tactic:
simpa using congr(b.coord i $(H <| r • b i))
-- Module: Mathlib.LinearAlgebra.FreeModule.Basic
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
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
⊢ ∃ (α : R) (h : ∀ (g : R), g * α = α * g),
    ∀ (x : M), Eq (α := M) ((f : (a : M) → M) x : M) ((smulLeft α ⋯ : (a : M) → M) x : M)

Tactic:
exact ⟨b.coord i <| f <| b i, fun r ↦ by simpa using congr(b.coord i $(H <| r • b i)), H⟩
-- Module: Mathlib.LinearAlgebra.FreeModule.Basic
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
⊢ Membership.mem (γ := Submonoid (End R M)) (Submonoid.center (End R M)) f ↔
    ∃ (α : R) (hα : Membership.mem (γ := Submonoid R) (Submonoid.center R) α), f = smulLeft α hα

Tactic:
mem_center_iff

Premises used: Set.Mem, setOf, Set.center, Module.End.mem_center_iff
-- Module: Mathlib.LinearAlgebra.FreeModule.Basic
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
⊢ Membership.mem (γ := Subsemigroup (End R M)) (Subsemigroup.center (End R M)) f ↔
    ∃ (α : R) (hα : Membership.mem (γ := Subsemigroup R) (Subsemigroup.center R) α), f = smulLeft α hα

Tactic:
mem_center_iff

Premises used: Set.Mem, setOf, Set.center, Module.End.mem_center_iff
-- Module: Mathlib.LinearAlgebra.FreeModule.Determinant
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) := ⋯
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.LinearAlgebra.FreeModule.Determinant
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) := ⋯
h : Nontrivial R
⊢ Eq.{u_1 + 1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) 0 : R) (0 : R)

Tactic:
LinearMap.det_zero' (Module.Free.chooseBasis R M)

Premises used: LinearMap.det_zero', Module.Free.chooseBasis
-- Module: Mathlib.LinearAlgebra.FreeModule.Determinant
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) := ⋯
h : Nontrivial R
⊢ Eq.{u_1 + 1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) 0 : R) (0 : R)

Tactic:
exact LinearMap.det_zero' (Module.Free.chooseBasis R M)

Premises used: LinearMap.det_zero', Module.Free.chooseBasis
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.Basic
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
refine : Finite.{v + 1} (ChooseBasisIndex R M)
⊢ Fintype (ChooseBasisIndex R M)

Tactic:
refine @Fintype.ofFinite _ ?_

Premises used: Fintype.ofFinite
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.Basic
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)
inr : Nontrivial R → Finite.{v + 1} (ChooseBasisIndex R M)
⊢ Finite.{v + 1} (ChooseBasisIndex R M)

Tactic:
cases subsingleton_or_nontrivial R

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.Basic
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
⊢ Subsingleton M

Tactic:
have := Module.subsingleton R M
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.Basic
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
this : Subsingleton M
⊢ Finite.{v + 1} (↑(Exists.choose (p := fun (S : Set M) ↦ Nonempty (Basis (↑S : Type v) R M)) ⋯) : Type v)

Tactic:
infer_instance
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.Basic
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 : Nontrivial R
⊢ Finite.{v + 1} (ChooseBasisIndex R M)

Tactic:
Module.Finite.finite_basis (chooseBasis _ _)

Premises used: Module.Finite.finite_basis, Module.Free.chooseBasis
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.Basic
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 : Nontrivial R
⊢ Finite.{v + 1} (ChooseBasisIndex R M)

Tactic:
exact Module.Finite.finite_basis (chooseBasis _ _)

Premises used: Module.Finite.finite_basis, Module.Free.chooseBasis
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.Basic
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
intro : ∀ (val : Fintype ι), Module.Finite R M
⊢ Module.Finite R M

Tactic:
cases nonempty_fintype ι

Premises used: nonempty_fintype
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.Basic
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

Tactic:
⟨⟨Finset.univ.image b, ?_⟩⟩

Premises used: Finset.univ, Module.Finite.of_fg_top, Exists.intro, DFunLike.coe, Finset.image
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.Basic
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 ι
intro :
  Eq (α := Submodule R M)
    (Submodule.span R (↑(Finset.image.{u_3, u_2} (α := ι) (⇑b : (a : ι) → M) Finset.univ) : Set M)) ⊤
⊢ Module.Finite R M

Tactic:
refine ⟨⟨Finset.univ.image b, ?_⟩⟩
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.Basic
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 ι
⊢ Eq (α := Submodule R M)
    (Submodule.span R (↑(Finset.image.{u_3, u_2} (α := ι) (⇑b : (a : ι) → M) Finset.univ) : Set M)) ⊤

Tactic:
simp only [Set.image_univ, Finset.coe_univ, Finset.coe_image, Basis.span_eq]

Premises used: Set.image_univ, Finset.coe_univ, Finset.coe_image, Module.Basis.span_eq
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.Basic
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 ι
intro :
  Eq (α := Submodule R M)
    (Submodule.span R (↑(Finset.image.{u_3, u_2} (α := ι) (⇑b : (a : ι) → M) Finset.univ) : Set M)) ⊤
⊢ Module.Finite R M

Tactic:
classical
    refine ⟨⟨Finset.univ.image b, ?_⟩⟩
    simp only [Set.image_univ, Finset.coe_univ, Finset.coe_image, Basis.span_eq]

Premises used: Set.image_univ, Finset.coe_univ, Finset.coe_image, Module.Basis.span_eq
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.Basic
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 ι₂
intro : ∀ (val : Fintype ι₁), Module.Finite R (Matrix ι₁ ι₂ M)
⊢ Module.Finite R (Matrix ι₁ ι₂ M)

Tactic:
cases nonempty_fintype ι₁

Premises used: nonempty_fintype
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.Basic
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 ι₁
intro : ∀ (val : Fintype ι₂), Module.Finite R (Matrix ι₁ ι₂ M)
⊢ Module.Finite R (Matrix ι₁ ι₂ M)

Tactic:
cases nonempty_fintype ι₂

Premises used: nonempty_fintype
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.Basic
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 ι₁
val_1 : Fintype ι₂
⊢ Module.Finite R (Matrix ι₁ ι₂ M)

Tactic:
Module.Finite.of_basis <| (Free.chooseBasis _ _).matrix _ _

Premises used: Module.Basis.matrix, Module.Finite.of_basis, Module.Free.chooseBasis
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.Basic
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 ι₁
val_1 : Fintype ι₂
⊢ Module.Finite R (Matrix ι₁ ι₂ M)

Tactic:
exact Module.Finite.of_basis <| (Free.chooseBasis _ _).matrix _ _

Premises used: Module.Basis.matrix, Module.Finite.of_basis, Module.Free.chooseBasis
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.Basic
Goal:
ι₁ : Type u_1
ι₂ : Type u_2
R : Type u_3
inst : Semiring R
inst_1 : Finite ι₁
inst_2 : Finite ι₂
⊢ Module.Finite R (Matrix ι₁ ι₂ R)

Tactic:
inferInstance

Premises used: inferInstance
-- 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
⊢ finrank.{0, u_1} ℤ ↥N = finrank ℤ M

Tactic:
have h : Module.finrank ℤ N = Module.finrank ℤ M :=
    (AddEquiv.toIntLinearEquiv e : M ≃ₗ[ℤ] N).symm.finrank_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 : 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
⊢ ∀ (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
-- 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) :=
  ⋯
this : Int.natAbs ((LinearMap.det : (a : M →ₗ[ℤ] M) → ℤ) f) = Nat.card.{u_1} (M ⧸ N)
⊢ Int.natAbs
      ((LinearMap.det : (a : M →ₗ[ℤ] M) → ℤ)
        (N.subtype ∘ₗ (↑(AddEquiv.toIntLinearEquiv (↑e : M ≃+ ↥N)) : M →ₗ[ℤ] ↥N))) =
    Int.natAbs
      ((LinearMap.det : (a : M →ₗ[ℤ] M) → ℤ) (N.subtype ∘ₗ (↑(AddEquiv.toIntLinearEquiv (↑e : M ≃+ ↥N)) : M →ₗ[ℤ] ↥N)))

Tactic:
rfl

Premises used: rfl
-- 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) :=
  ⋯
this : Int.natAbs ((LinearMap.det : (a : M →ₗ[ℤ] M) → ℤ) f) = Nat.card.{u_1} (M ⧸ N)
⊢ Int.natAbs
      ((LinearMap.det : (a : M →ₗ[ℤ] M) → ℤ)
        (N.subtype ∘ₗ (↑(AddEquiv.toIntLinearEquiv (↑e : M ≃+ ↥N)) : M →ₗ[ℤ] ↥N))) =
    Int.natAbs ((LinearMap.det : (a : M →ₗ[ℤ] M) → ℤ) (N.subtype ∘ₗ (↑e' : M →ₗ[ℤ] ↥N)))

Tactic:
Int.natAbs_eq_iff_associated.mpr (LinearMap.associated_det_comp_equiv _ _ _)

Premises used: Iff.mpr, Int.natAbs_eq_iff_associated, LinearMap.associated_det_comp_equiv
-- 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) :=
  ⋯
this : Int.natAbs ((LinearMap.det : (a : M →ₗ[ℤ] M) → ℤ) f) = Nat.card.{u_1} (M ⧸ N)
⊢ Int.natAbs ((LinearMap.det : (a : M →ₗ[ℤ] M) → ℤ) (N.subtype ∘ₗ (↑e' : M →ₗ[ℤ] ↥N))) = Nat.card.{u_1} (M ⧸ N)

Tactic:
this
-- 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) :=
  ⋯
this : Int.natAbs ((LinearMap.det : (a : M →ₗ[ℤ] M) → ℤ) f) = Nat.card.{u_1} (M ⧸ N)
⊢ Int.natAbs ((LinearMap.det : (a : M →ₗ[ℤ] M) → ℤ) (N.subtype ∘ₗ AddMonoidHom.toIntLinearMap (↑e : M →+ ↥N))) =
    Nat.card.{u_1} (M ⧸ N)

Tactic:
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

Premises used: Iff.mpr, Int.natAbs_eq_iff_associated, AddEquiv.toIntLinearEquiv, Nat.card, AddEquivClass.toAddEquiv, LinearMap.det, HasQuotient.Quotient, LinearMap.comp, LinearEquiv.toLinearMap, Int.natAbs, Submodule.subtype, DFunLike.coe, LinearMap.associated_det_comp_equiv, rfl
-- 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) :=
  ⋯
suffices : Int.natAbs ((LinearMap.det : (a : M →ₗ[ℤ] M) → ℤ) f) = Nat.card.{u_1} (M ⧸ N)
⊢ Int.natAbs ((LinearMap.det : (a : M →ₗ[ℤ] M) → ℤ) (N.subtype ∘ₗ AddMonoidHom.toIntLinearMap (↑e : M →+ ↥N))) =
    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
-- 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
rw :
  (↑((ab : (a : Free.ChooseBasisIndex ℤ M) → ↥N) i) : M) =
    HSMul.hSMul (β := M) (a i) ((b' : (a : Free.ChooseBasisIndex ℤ M) → M) i : 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:
rw [f_apply, b'.equiv_apply, Equiv.refl_apply]

Premises used: Equiv.refl_apply, Module.Basis.equiv_apply
-- 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:
ab_eq i