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) :=
  ⋯
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))
calc_2₂ :
  Eq (α := ℕ) (∏ i : Free.ChooseBasisIndex ℤ M, (a i).natAbs)
    (∏ x : Free.ChooseBasisIndex ℤ M, (smithNormalFormCoeffs b h x).natAbs)
⊢ ∏ i : Free.ChooseBasisIndex ℤ M, (a i).natAbs = Nat.card.{u_1} (M ⧸ N)

Tactic:
simp_rw [Nat.card_congr (quotientEquivPiZMod N b h).toEquiv, Nat.card_pi, Nat.card_zmod, a]

Premises used: Submodule.quotientEquivPiZMod, Nat.card_congr, Nat.card_pi, Nat.card_zmod, AddEquiv.toEquiv
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient
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 ι)
rw 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)))
⊢ 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:
rw [Basis.det_comp_basis]

Premises used: Module.Basis.det_comp_basis
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient
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 ((LinearMap.det : (a : M →ₗ[ℤ] M) → ℤ) (N.subtype ∘ₗ (↑e : M →ₗ[ℤ] ↥N))) = Nat.card.{u_1} (M ⧸ N)

Tactic:
natAbs_det_equiv N e

Premises used: Submodule.natAbs_det_equiv, AddMonoidHom.toIntLinearMap
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient
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 ι)
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)))
⊢ 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)

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

Premises used: Function.comp, LinearMap.det, Submodule.natAbs_det_equiv, Module.Basis.det, LinearMap.comp, LinearEquiv.toLinearMap, Int.natAbs, Submodule.subtype, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient
Goal:
E : Type u_1
inst : AddCommGroup E
ι : Type u_2
inst_1 : DecidableEq ι
inst_2 : Fintype ι
bE : Basis ι ℤ E
N : AddSubgroup E
bN : Basis.{u_2, 0, u_1} ι ℤ ↥N
⊢ N.index = Int.natAbs ((bE.det : (a : ι → E) → ℤ) fun (x : ι) ↦ (↑((bN : (a : ι) → ↥N) x) : E))

Tactic:
have : Module.Free ℤ E := Module.Free.of_basis bE
  have : Module.Finite ℤ E := Module.Finite.of_basis bE
  (Submodule.natAbs_det_basis_change bE N.toIntSubmodule bN).symm

Premises used: AddSubgroup.index, Module.Free.of_basis, Module.Finite.of_basis, Submodule.quotientRel, Eq.symm, AddSubgroup.toIntSubmodule, DFunLike.coe, Submodule.natAbs_det_basis_change
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient
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)
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) ⋯)
⊢ 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) ⋯)

Tactic:
rw [relIndex, index_eq_natAbs_det b₂ _ (b₁.map (addSubgroupOfEquivOfLe H).toIntLinearEquiv.symm)]

Premises used: LinearEquiv.symm, AddEquiv.toIntLinearEquiv, AddSubgroup.index_eq_natAbs_det, Module.Basis.map, AddSubgroup.relIndex, AddSubgroup.addSubgroupOfEquivOfLe
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient
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)
⊢ 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) ⋯)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient
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))
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)
                ⋯) :
          ℚ)| :
      ℚ)
    (|(b₂.det : (a : ι → E) → ℚ) (⇑b₁ : (a : ι) → E)| : ℚ)
⊢ Eq (α := ℚ) ((↑(L₁.relIndex L₂) : ℚ) : ℚ) (|(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]

Premises used: Int.cast_abs, Nat.cast_natAbs, Module.Basis.addSubgroupOfClosure, AddSubgroup.relIndex_eq_natAbs_det
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient
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))
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)
              ⋯))| =
    |Matrix.det (b₂.toMatrix (⇑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)| : ℚ)

Tactic:
rw [Basis.det_apply, Basis.det_apply, RingHom.map_det]

Premises used: RingHom.map_det, Module.Basis.det_apply
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient
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))
e_a :
  Eq (α := Matrix ι ι ℚ)
    ((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)
            ⋯) :
      Matrix ι ι ℚ)
    (b₂.toMatrix (⇑b₁ : (a : ι) → E) : Matrix ι ι ℚ)
⊢ |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)
              ⋯))| =
    |Matrix.det (b₂.toMatrix (⇑b₁ : (a : ι) → E))|

Tactic:
congr
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient
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))
e_a :
  ∀ (i j : ι),
    (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)
            ⋯)
        i j =
      b₂.toMatrix (⇑b₁ : (a : ι) → E) i j
⊢ Eq (α := Matrix ι ι ℚ)
    ((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)
            ⋯) :
      Matrix ι ι ℚ)
    (b₂.toMatrix (⇑b₁ : (a : ι) → E) : Matrix ι ι ℚ)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient
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))
i j : ι
⊢ (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)
          ⋯)
      i j =
    b₂.toMatrix (⇑b₁ : (a : ι) → E) i j

Tactic:
simp [Basis.toMatrix_apply]

Premises used: Module.Basis.toMatrix_apply
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.Matrix
Goal:
R : Type u
S : Type u'
M : Type v
N : Type w
inst : Ring R
inst_1 : Ring S
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Free R M
inst_5 : Module.Finite R M
inst_6 : AddCommGroup N
inst_7 : Module R N
inst_8 : Module S N
inst_9 : SMulCommClass R S N
inst_10 : Free S N
⊢ Free S (M →ₗ[R] N)

Tactic:
Module.Free.of_equiv (linearMapEquivFun R S M N).symm

Premises used: LinearEquiv.symm, _private.0.linearMapEquivFun, Module.Free.of_equiv
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.Matrix
Goal:
R : Type u
S : Type u'
M : Type v
N : Type w
inst : Ring R
inst_1 : Ring S
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Free R M
inst_5 : Module.Finite R M
inst_6 : AddCommGroup N
inst_7 : Module R N
inst_8 : Module S N
inst_9 : SMulCommClass R S N
inst_10 : Module.Finite S N
⊢ Module.Finite S (M →ₗ[R] N)

Tactic:
Module.Finite.equiv (linearMapEquivFun R S M N).symm

Premises used: LinearEquiv.symm, _private.0.linearMapEquivFun, Module.Finite.equiv
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.Matrix
Goal:
R : Type u
S : Type u'
M : Type v
N : Type w
inst : Ring R
inst_1 : Ring S
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Free R M
inst_5 : Module.Finite R M
inst_6 : AddCommGroup N
inst_7 : Module R N
inst_8 : Module S N
inst_9 : SMulCommClass R S N
inst_10 : StrongRankCondition R
inst_11 : StrongRankCondition S
inst_12 : Free S N
rw : Module.rank S (ChooseBasisIndex R M → N) = lift.{w, v} (Module.rank R M) * lift.{v, w} (Module.rank S N)
rw₁ :
  (↑(Fintype.card.{v} (ChooseBasisIndex R M)) : Cardinal.{max v w}) * lift.{v, w} (Module.rank S N) =
    lift.{w, v} (Module.rank R M) * lift.{v, w} (Module.rank S N)
rw₂ :
  (↑(finrank R M) : Cardinal.{max v w}) * lift.{v, w} (Module.rank S N) =
    lift.{w, v} (Module.rank R M) * lift.{v, w} (Module.rank S N)
rw₃ :
  (↑(finrank R M) : Cardinal.{max v w}) * lift.{v, w} (Module.rank S N) =
    lift.{w, v} (↑(finrank R M) : Cardinal.{v}) * lift.{v, w} (Module.rank S N)
rw₄ rw₅ :
  (↑(finrank R M) : Cardinal.{max v w}) * lift.{v, w} (Module.rank S N) =
    (↑(finrank R M) : Cardinal.{max v w}) * lift.{v, w} (Module.rank S N)
⊢ Module.rank S (M →ₗ[R] N) = lift.{w, v} (Module.rank R M) * lift.{v, w} (Module.rank S N)

Tactic:
rw [(linearMapEquivFun R S M N).rank_eq, rank_fun_eq_lift_mul,
    ← finrank_eq_card_chooseBasisIndex, ← finrank_eq_rank R, lift_natCast]

Premises used: _private.0.linearMapEquivFun, Module.finrank_eq_rank, Cardinal.lift_natCast, Module.finrank_eq_card_chooseBasisIndex, LinearEquiv.rank_eq, rank_fun_eq_lift_mul
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.Matrix
Goal:
R : Type u
S : Type u'
M : Type v
N : Type w
inst : Ring R
inst_1 : Ring S
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Free R M
inst_5 : Module.Finite R M
inst_6 : AddCommGroup N
inst_7 : Module R N
inst_8 : Module S N
inst_9 : SMulCommClass R S N
inst_10 : StrongRankCondition R
inst_11 : StrongRankCondition S
inst_12 : Free S N
simp_rw :
  (toNat : (a : Cardinal.{max w v}) → ℕ) (Module.rank S (M →ₗ[R] N)) =
    HMul.hMul (α := ℕ) (β := ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) (Module.rank R M) : ℕ)
      ((toNat : (a : Cardinal.{w}) → ℕ) (Module.rank S N) : ℕ)
simp_rw₁ :
  (toNat : (a : Cardinal.{max w v}) → ℕ) (lift.{w, v} (Module.rank R M) * lift.{v, w} (Module.rank S N)) =
    HMul.hMul (α := ℕ) (β := ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) (Module.rank R M) : ℕ)
      ((toNat : (a : Cardinal.{w}) → ℕ) (Module.rank S N) : ℕ)
simp_rw₂ :
  HMul.hMul (α := ℕ) (β := ℕ) ((toNat : (a : Cardinal.{max v w}) → ℕ) (lift.{w, v} (Module.rank R M)) : ℕ)
      ((toNat : (a : Cardinal.{max v w}) → ℕ) (lift.{v, w} (Module.rank S N)) : ℕ) =
    HMul.hMul (α := ℕ) (β := ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) (Module.rank R M) : ℕ)
      ((toNat : (a : Cardinal.{w}) → ℕ) (Module.rank S N) : ℕ)
⊢ finrank S (M →ₗ[R] N) = finrank R M * finrank S N

Tactic:
simp_rw [finrank, rank_linearMap, toNat_mul, toNat_lift]

Premises used: Cardinal.toNat_mul, Module.rank_linearMap, Cardinal.toNat_lift, Module.finrank
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.Matrix
Goal:
R : Type u
S : Type u'
M : Type v
inst : Ring R
inst_1 : Ring S
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Free R M
inst_5 : Module.Finite R M
inst_6 : StrongRankCondition R
inst_7 : StrongRankCondition S
inst_8 : Module R S
inst_9 : SMulCommClass R S S
rw : lift.{u', v} (Module.rank R M) * lift.{v, u'} (Module.rank S S) = lift.{u', v} (Module.rank R M)
rw₁ : lift.{u', v} (Module.rank R M) * lift.{v, u'} 1 = lift.{u', v} (Module.rank R M)
rw₂ : lift.{u', v} (Module.rank R M) * 1 = lift.{u', v} (Module.rank R M)
rw₃ rw₄ : lift.{u', v} (Module.rank R M) = lift.{u', v} (Module.rank R M)
⊢ Module.rank S (M →ₗ[R] S) = lift.{u', v} (Module.rank R M)

Tactic:
rw [rank_linearMap, rank_self, lift_one, mul_one]

Premises used: Module.rank_linearMap, Module.rank_self, Cardinal.lift_one, mul_one
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.Matrix
Goal:
R : Type u
S : Type u'
M : Type v
inst : Ring R
inst_1 : Ring S
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Free R M
inst_5 : Module.Finite R M
inst_6 : StrongRankCondition R
inst_7 : StrongRankCondition S
inst_8 : Module R S
inst_9 : SMulCommClass R S S
rw : finrank R M * finrank S S = finrank R M
rw₁ : finrank R M * 1 = finrank R M
rw₂ rw₃ : finrank R M = finrank R M
⊢ finrank S (M →ₗ[R] S) = finrank R M

Tactic:
rw [finrank_linearMap, finrank_self, mul_one]

Premises used: Module.finrank_linearMap, Module.finrank_self, mul_one
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.Matrix
Goal:
R : Type u
S : Type u'
M_1 : Type v
N : Type w
K : Type u_1
M : Type u_2
L : Type v
inst : CommRing K
inst_1 : Ring M
inst_2 : Algebra K M
inst_3 : Module.Free K M
inst_4 : Module.Finite K M
inst_5 : CommRing L
inst_6 : IsDomain L
inst_7 : Algebra K L
⊢ Finite (M →ₐ[K] L)

Tactic:
(linearIndependent_algHom_toLinearMap K M L).finite

Premises used: linearIndependent_algHom_toLinearMap, LinearIndependent.finite
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.Matrix
Goal:
K : Type u_1
M : Type u_2
L : Type v
inst : CommRing K
inst_1 : Ring M
inst_2 : Algebra K M
inst_3 : Module.Free K M
inst_4 : Module.Finite K M
inst_5 : CommRing L
inst_6 : IsDomain L
inst_7 : Algebra K L
⊢ lift.{max u_2 v, max u_2 v} #(M →ₐ[K] L) ≤ lift.{max u_2 v, max u_2 v} (Module.rank L (M →ₗ[K] L))

Tactic:
(linearIndependent_algHom_toLinearMap K M L).cardinal_lift_le_rank

Premises used: LinearIndependent.cardinal_lift_le_rank, linearIndependent_algHom_toLinearMap
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.Matrix
Goal:
K : Type u_1
M : Type u_2
L : Type v
inst : CommRing K
inst_1 : Ring M
inst_2 : Algebra K M
inst_3 : Module.Free K M
inst_4 : Module.Finite K M
inst_5 : CommRing L
inst_6 : IsDomain L
inst_7 : Algebra K L
h : #(M →ₐ[K] L) = lift.{max u_2 v, max u_2 v} #(M →ₐ[K] L)
h₁ : lift.{v, u_2} (Module.rank K M) = lift.{max u_2 v, max u_2 v} (Module.rank L (M →ₗ[K] L))
⊢ #(M →ₐ[K] L) ≤ lift.{v, u_2} (Module.rank K M)

Tactic:
convert! (linearIndependent_algHom_toLinearMap K M L).cardinal_lift_le_rank

Premises used: LinearIndependent.cardinal_lift_le_rank, linearIndependent_algHom_toLinearMap
-- Module: Mathlib.LinearAlgebra.FreeModule.Finite.Matrix
Goal:
K : Type u_1
M : Type u_2
L : Type v
inst : CommRing K
inst_1 : Ring M
inst_2 : Algebra K M
inst_3 : Module.Free K M
inst_4 : Module.Finite K M
inst_5 : CommRing L
inst_6 : IsDomain L
inst_7 : Algebra K L
h h₁ : #(M →ₐ[K] L) = #(M →ₐ[K] L)
⊢ #(M →ₐ[K] L) = lift.{max u_2 v, max u_2 v} #(M →ₐ[K] L)

Tactic:
rw [lift_id]

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

Tactic:
have := Module.nontrivial K L