awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))
⊢ |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))|
have 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)
          sorry) :
    Matrix ι ι ℚ)
  (b₂.toMatrix (⇑b₁ : (a : ι) → E) : Matrix ι ι ℚ)
Tactic: congr
-- 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 (α := 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 ι ι ℚ)
have 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)
          sorry)
      i j =
    b₂.toMatrix (⇑b₁ : (a : ι) → E) i j
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Finite.Matrix (goal)
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
⊢ Module.rank S (M →ₗ[R] N) = lift.{w, v} (Module.rank R M) * lift.{v, w} (Module.rank S N)
have rw : Module.rank S (ChooseBasisIndex R M → 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Finite.Matrix (goal)
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)
⊢ Module.rank S (M →ₗ[R] N) = lift.{w, v} (Module.rank R M) * lift.{v, w} (Module.rank S N)
have 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)
Tactic: rw [(linearMapEquivFun R S M N).rank_eq, rank_fun_eq_lift_mul,
    ← finrank_eq_card_chooseBasisIndex, ← finrank_eq_rank R, lift_natCast]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Finite.Matrix (goal)
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)
⊢ Module.rank S (M →ₗ[R] N) = lift.{w, v} (Module.rank R M) * lift.{v, w} (Module.rank S N)
have 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)
Tactic: rw [(linearMapEquivFun R S M N).rank_eq, rank_fun_eq_lift_mul,
    ← finrank_eq_card_chooseBasisIndex, ← finrank_eq_rank R, lift_natCast]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Finite.Matrix (goal)
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)
⊢ Module.rank S (M →ₗ[R] N) = lift.{w, v} (Module.rank R M) * lift.{v, w} (Module.rank S N)
have 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)
Tactic: rw [(linearMapEquivFun R S M N).rank_eq, rank_fun_eq_lift_mul,
    ← finrank_eq_card_chooseBasisIndex, ← finrank_eq_rank R, lift_natCast]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Finite.Matrix (goal)
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)
⊢ Module.rank S (M →ₗ[R] N) = lift.{w, v} (Module.rank R M) * lift.{v, w} (Module.rank S N)
have 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)
Tactic: rw [(linearMapEquivFun R S M N).rank_eq, rank_fun_eq_lift_mul,
    ← finrank_eq_card_chooseBasisIndex, ← finrank_eq_rank R, lift_natCast]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Finite.Matrix (goal)
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
⊢ finrank S (M →ₗ[R] N) = finrank R M * finrank S N
have 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) : ℕ)
Tactic: simp_rw [finrank, rank_linearMap, toNat_mul, toNat_lift]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Finite.Matrix (goal)
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) : ℕ)
⊢ finrank S (M →ₗ[R] N) = finrank R M * finrank S N
have 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) : ℕ)
Tactic: simp_rw [finrank, rank_linearMap, toNat_mul, toNat_lift]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Finite.Matrix (goal)
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) : ℕ)
⊢ finrank S (M →ₗ[R] N) = finrank R M * finrank S N
have 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) : ℕ)
Tactic: simp_rw [finrank, rank_linearMap, toNat_mul, toNat_lift]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Finite.Matrix (goal)
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
⊢ Module.rank S (M →ₗ[R] S) = lift.{u', v} (Module.rank R M)
have rw : lift.{u', v} (Module.rank R M) * lift.{v, u'} (Module.rank S S) = lift.{u', v} (Module.rank R M)
Tactic: rw [rank_linearMap, rank_self, lift_one, mul_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Finite.Matrix (goal)
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)
⊢ Module.rank S (M →ₗ[R] S) = lift.{u', v} (Module.rank R M)
have rw₁ : lift.{u', v} (Module.rank R M) * lift.{v, u'} 1 = lift.{u', v} (Module.rank R M)
Tactic: rw [rank_linearMap, rank_self, lift_one, mul_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Finite.Matrix (goal)
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)
⊢ Module.rank S (M →ₗ[R] S) = lift.{u', v} (Module.rank R M)
have rw₂ : lift.{u', v} (Module.rank R M) * 1 = lift.{u', v} (Module.rank R M)
Tactic: rw [rank_linearMap, rank_self, lift_one, mul_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Finite.Matrix (goal)
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)
⊢ Module.rank S (M →ₗ[R] S) = lift.{u', v} (Module.rank R M)
have rw₃ : lift.{u', v} (Module.rank R M) = lift.{u', v} (Module.rank R M)
Tactic: rw [rank_linearMap, rank_self, lift_one, mul_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Finite.Matrix (goal)
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
⊢ finrank S (M →ₗ[R] S) = finrank R M
have rw : finrank R M * finrank S S = finrank R M
Tactic: rw [finrank_linearMap, finrank_self, mul_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Finite.Matrix (goal)
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
⊢ finrank S (M →ₗ[R] S) = finrank R M
have rw₁ : finrank R M * 1 = finrank R M
Tactic: rw [finrank_linearMap, finrank_self, mul_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Finite.Matrix (goal)
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
⊢ finrank S (M →ₗ[R] S) = finrank R M
have rw₂ : finrank R M = finrank R M
Tactic: rw [finrank_linearMap, finrank_self, mul_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Finite.Matrix (goal)
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
⊢ #(M →ₐ[K] L) ≤ lift.{v, u_2} (Module.rank K M)
have h : #(M →ₐ[K] L) = lift.{max u_2 v, max u_2 v} #(M →ₐ[K] L)
Tactic: convert! (linearIndependent_algHom_toLinearMap K M L).cardinal_lift_le_rank
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Finite.Matrix (goal)
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)
⊢ #(M →ₐ[K] L) ≤ lift.{v, u_2} (Module.rank K M)
have h₁ : lift.{v, u_2} (Module.rank K M) = lift.{max u_2 v, max u_2 v} (Module.rank L (M →ₗ[K] L))
Tactic: convert! (linearIndependent_algHom_toLinearMap K M L).cardinal_lift_le_rank
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Finite.Matrix (goal)
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
⊢ #(M →ₐ[K] L) = lift.{max u_2 v, max u_2 v} #(M →ₐ[K] L)
have h : #(M →ₐ[K] L) = #(M →ₐ[K] L)
Tactic: rw [lift_id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Finite.Matrix (hypothesis)
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.{v, u_2} (Module.rank K M) = lift.{max u_2 v, max u_2 v} (Module.rank L (M →ₗ[K] L))
have this : Nontrivial K
Tactic: have := Module.nontrivial K L
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Finite.Matrix (goal)
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
this : Nontrivial K
⊢ lift.{v, u_2} (Module.rank K M) = lift.{max u_2 v, max u_2 v} (Module.rank L (M →ₗ[K] L))
have h : lift.{v, u_2} (Module.rank K M) = Module.rank L (M →ₗ[K] L)
Tactic: rw [lift_id, Module.rank_linearMap_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Finite.Matrix (goal)
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
this : Nontrivial K
h : lift.{v, u_2} (Module.rank K M) = Module.rank L (M →ₗ[K] L)
⊢ lift.{v, u_2} (Module.rank K M) = lift.{max u_2 v, max u_2 v} (Module.rank L (M →ₗ[K] L))
have h₁ : lift.{v, u_2} (Module.rank K M) = lift.{v, u_2} (Module.rank K M)
Tactic: rw [lift_id, Module.rank_linearMap_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Finite.Matrix (goal)
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
⊢ Nat.card (M →ₐ[K] L) ≤ finrank K M
have h : finrank K M = (toNat : (a : Cardinal.{max u_2 v}) → ℕ) (lift.{v, u_2} (Module.rank K M))
Tactic: convert! toNat_le_toNat (cardinalMk_algHom_le_rank K M L) ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Finite.Matrix (goal)
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 : finrank K M = (toNat : (a : Cardinal.{max u_2 v}) → ℕ) (lift.{v, u_2} (Module.rank K M))
⊢ Nat.card (M →ₐ[K] L) ≤ finrank K M
have convert! : lift.{v, u_2} (Module.rank K M) < ℵ₀
Tactic: convert! toNat_le_toNat (cardinalMk_algHom_le_rank K M L) ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Finite.Matrix (goal)
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
⊢ finrank K M = (toNat : (a : Cardinal.{max u_2 v}) → ℕ) (lift.{v, u_2} (Module.rank K M))
have h : finrank K M = (toNat : (a : Cardinal.{u_2}) → ℕ) (Module.rank K M)
Tactic: rw [toNat_lift, finrank]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Finite.Matrix (goal)
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 : finrank K M = (toNat : (a : Cardinal.{u_2}) → ℕ) (Module.rank K M)
⊢ finrank K M = (toNat : (a : Cardinal.{max u_2 v}) → ℕ) (lift.{v, u_2} (Module.rank K M))
have h₁ : Eq (α := ℕ) ((toNat : (a : Cardinal.{u_2}) → ℕ) (Module.rank K M) : ℕ)
  ((toNat : (a : Cardinal.{u_2}) → ℕ) (Module.rank K M) : ℕ)
Tactic: rw [toNat_lift, finrank]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Finite.Matrix (goal)
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.{v, u_2} (Module.rank K M) < ℵ₀
have rw : Module.rank K M < ℵ₀
Tactic: rw [lift_lt_aleph0]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Finite.Matrix (hypothesis)
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
⊢ Module.rank K M < ℵ₀
have this : Nontrivial K
Tactic: have := Module.nontrivial K L
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Finite.Quotient (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsPrincipalIdealRing R
inst_5 : Finite ι
N : Submodule R M
b : Basis ι R M
h : finrank.{u_2, u_3} R ↥N = finrank R M
⊢ (M ⧸ N) ≃ₗ[R] (i : ι) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {smithNormalFormCoeffs b h i})
have haveI : (this : Fintype ι) →
  (M ⧸ N) ≃ₗ[R] (i : ι) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {smithNormalFormCoeffs b h i})
Tactic: haveI := Fintype.ofFinite ι
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Finite.Quotient (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsPrincipalIdealRing R
inst_5 : Finite ι
N : Submodule R M
b : Basis ι R M
h : finrank.{u_2, u_3} R ↥N = finrank R M
this : Fintype ι
a : ι → R := smithNormalFormCoeffs b h
b' : Basis ι R M := smithNormalFormTopBasis b h
ab : Basis.{u_1, u_2, u_3} ι R ↥N := smithNormalFormBotBasis b h
⊢ (M ⧸ N) ≃ₗ[R] (i : ι) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {smithNormalFormCoeffs b h i})
have ab_eq : ∀ (i : ι),
  (↑((smithNormalFormBotBasis b h : (a : ι) → ↥N) i) : M) =
    HSMul.hSMul (β := M) (smithNormalFormCoeffs b h i) ((smithNormalFormTopBasis b h : (a : ι) → M) i : M)
Tactic: have ab_eq := smithNormalFormBotBasis_def b h