awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField (goal)
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
K : Type u_2
inst_2 : Field K
inst_3 : Fintype K
M : Matrix n n K
h : Nonempty n
p : ℕ
hp_1 : CharP K p
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ (expand K (Fintype.card K) : (a : K[X]) → K[X]) (det (M ^ Fintype.card K).charmatrix) =
    HPow.hPow (α := K[X]) (det M.charmatrix) (Fintype.card K)
have inl : Eq.{u_2 + 1} (α := K[X])
  ((detMonoidHom : (a : Matrix n n K[X]) → K[X])
      ((AlgHom.mapMatrix (expand K (Fintype.card K)) : (a : Matrix n n K[X]) → Matrix n n K[X])
        (M ^ Fintype.card K).charmatrix) :
    K[X])
  ((detMonoidHom : (a : Matrix n n K[X]) → K[X])
      (HPow.hPow (α := Matrix.{u_1, u_1, u_2} n n K[X]) M.charmatrix (Fintype.card K)) :
    K[X])
Tactic: rw [AlgHom.map_det, ← coe_detMonoidHom, ← (detMonoidHom : Matrix n n K[X] →* K[X]).map_pow]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField (goal)
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
K : Type u_2
inst_2 : Field K
inst_3 : Fintype K
M : Matrix n n K
h : Nonempty n
p : ℕ
hp_1 : CharP K p
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ Eq.{u_2 + 1} (α := K[X])
    ((detMonoidHom : (a : Matrix n n K[X]) → K[X])
        ((AlgHom.mapMatrix (expand K (Fintype.card K)) : (a : Matrix n n K[X]) → Matrix n n K[X])
          (M ^ Fintype.card K).charmatrix) :
      K[X])
    ((detMonoidHom : (a : Matrix n n K[X]) → K[X])
        (HPow.hPow (α := Matrix.{u_1, u_1, u_2} n n K[X]) M.charmatrix (Fintype.card K)) :
      K[X])
have inl : (AlgHom.mapMatrix (expand K (Fintype.card K)) : (a : Matrix n n K[X]) → Matrix n n K[X])
    (M ^ Fintype.card K).charmatrix =
  HPow.hPow (α := Matrix.{u_1, u_1, u_2} n n K[X]) M.charmatrix (Fintype.card K)
Tactic: apply congr_arg det
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField (goal)
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
K : Type u_2
inst_2 : Field K
inst_3 : Fintype K
M : Matrix n n K
h : Nonempty n
p : ℕ
hp_1 : CharP K p
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ (AlgHom.mapMatrix (expand K (Fintype.card K)) : (a : Matrix n n K[X]) → Matrix n n K[X])
      (M ^ Fintype.card K).charmatrix =
    HPow.hPow (α := Matrix.{u_1, u_1, u_2} n n K[X]) M.charmatrix (Fintype.card K)
have inl : Eq (α := (Matrix n n K)[X])
  ((matPolyEquiv : (a : Matrix n n K[X]) → (Matrix n n K)[X])
      ((AlgHom.mapMatrix (expand K (Fintype.card K)) : (a : Matrix n n K[X]) → Matrix n n K[X])
        (M ^ Fintype.card K).charmatrix) :
    (Matrix n n K)[X])
  ((matPolyEquiv : (a : Matrix n n K[X]) → (Matrix n n K)[X])
      (HPow.hPow (α := Matrix.{u_1, u_1, u_2} n n K[X]) M.charmatrix (Fintype.card K)) :
    (Matrix n n K)[X])
Tactic: refine matPolyEquiv.injective ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField (goal)
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
K : Type u_2
inst_2 : Field K
inst_3 : Fintype K
M : Matrix n n K
h : Nonempty n
p : ℕ
hp_1 : CharP K p
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ Eq (α := (Matrix n n K)[X])
    ((matPolyEquiv : (a : Matrix n n K[X]) → (Matrix n n K)[X])
        ((AlgHom.mapMatrix (expand K (Fintype.card K)) : (a : Matrix n n K[X]) → Matrix n n K[X])
          (M ^ Fintype.card K).charmatrix) :
      (Matrix n n K)[X])
    ((matPolyEquiv : (a : Matrix n n K[X]) → (Matrix n n K)[X])
        (HPow.hPow (α := Matrix.{u_1, u_1, u_2} n n K[X]) M.charmatrix (Fintype.card K)) :
      (Matrix n n K)[X])
have inl : (matPolyEquiv : (a : Matrix n n K[X]) → (Matrix n n K)[X])
    ((AlgHom.mapMatrix (expand K (p ^ k)) : (a : Matrix n n K[X]) → Matrix n n K[X]) (M ^ p ^ k).charmatrix) =
  HSub.hSub (β := (Matrix n n K)[X]) (HPow.hPow (α := (Matrix n n K)[X]) X (p ^ k))
    ((C : (a : Matrix n n K) → (Matrix n n K)[X]) (M ^ p ^ k) : (Matrix n n K)[X])
Tactic: rw [map_pow, matPolyEquiv_charmatrix, hk, sub_pow_char_pow_of_commute, ← C_pow]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField (goal)
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
K : Type u_2
inst_2 : Field K
inst_3 : Fintype K
M : Matrix n n K
h : Nonempty n
p : ℕ
hp_1 : CharP K p
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
inl :
  (matPolyEquiv : (a : Matrix n n K[X]) → (Matrix n n K)[X])
      ((AlgHom.mapMatrix (expand K (p ^ k)) : (a : Matrix n n K[X]) → Matrix n n K[X]) (M ^ p ^ k).charmatrix) =
    HSub.hSub (β := (Matrix n n K)[X]) (HPow.hPow (α := (Matrix n n K)[X]) X (p ^ k))
      ((C : (a : Matrix n n K) → (Matrix n n K)[X]) (M ^ p ^ k) : (Matrix n n K)[X])
⊢ Eq (α := (Matrix n n K)[X])
    ((matPolyEquiv : (a : Matrix n n K[X]) → (Matrix n n K)[X])
        ((AlgHom.mapMatrix (expand K (Fintype.card K)) : (a : Matrix n n K[X]) → Matrix n n K[X])
          (M ^ Fintype.card K).charmatrix) :
      (Matrix n n K)[X])
    ((matPolyEquiv : (a : Matrix n n K[X]) → (Matrix n n K)[X])
        (HPow.hPow (α := Matrix.{u_1, u_1, u_2} n n K[X]) M.charmatrix (Fintype.card K)) :
      (Matrix n n K)[X])
have inl₁ : Commute (S := (Matrix n n K)[X]) X ((C : (a : Matrix n n K) → (Matrix n n K)[X]) M)
Tactic: rw [map_pow, matPolyEquiv_charmatrix, hk, sub_pow_char_pow_of_commute, ← C_pow]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField (hypothesis)
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
p : ℕ
inst_2 : Fact (Nat.Prime p)
M : Matrix n n (ZMod p)
⊢ Eq (α := (ZMod p)[X]) (M ^ p).charpoly M.charpoly
have h : Eq (α := (ZMod p)[X]) (M ^ Fintype.card (ZMod p)).charpoly M.charpoly
Tactic: have h := FiniteField.Matrix.charpoly_pow_card M
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField (goal)
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
p : ℕ
inst_2 : Fact (Nat.Prime p)
M : Matrix n n (ZMod p)
h : Eq (α := (ZMod p)[X]) (M ^ Fintype.card (ZMod p)).charpoly M.charpoly
⊢ Eq (α := (ZMod p)[X]) (M ^ p).charpoly M.charpoly
have rwa : ∀ (h : Eq (α := (ZMod p)[X]) (M ^ p).charpoly M.charpoly), Eq (α := (ZMod p)[X]) (M ^ p).charpoly M.charpoly
Tactic: rwa [ZMod.card] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField (goal)
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
K : Type u_2
inst_2 : Field K
inst_3 : Fintype K
M : Matrix n n K
⊢ (M ^ Fintype.card K).trace = M.trace ^ Fintype.card K
have inl : IsEmpty n → (M ^ Fintype.card K).trace = M.trace ^ Fintype.card K
Tactic: cases isEmpty_or_nonempty n
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField (goal)
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
K : Type u_2
inst_2 : Field K
inst_3 : Fintype K
M : Matrix n n K
inl : IsEmpty n → (M ^ Fintype.card K).trace = M.trace ^ Fintype.card K
⊢ (M ^ Fintype.card K).trace = M.trace ^ Fintype.card K
have inr : Nonempty n → (M ^ Fintype.card K).trace = M.trace ^ Fintype.card K
Tactic: cases isEmpty_or_nonempty n
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField (goal)
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
K : Type u_2
inst_2 : Field K
inst_3 : Fintype K
M : Matrix n n K
h : Nonempty n
⊢ (M ^ Fintype.card K).trace = M.trace ^ Fintype.card K
have inr : -coeff (M ^ Fintype.card K).charpoly (Fintype.card n - 1) = M.trace ^ Fintype.card K
Tactic: rw [Matrix.trace_eq_neg_charpoly_coeff, Matrix.trace_eq_neg_charpoly_coeff,
    FiniteField.Matrix.charpoly_pow_card, FiniteField.pow_card]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField (goal)
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
K : Type u_2
inst_2 : Field K
inst_3 : Fintype K
M : Matrix n n K
h : Nonempty n
inr : -coeff (M ^ Fintype.card K).charpoly (Fintype.card n - 1) = M.trace ^ Fintype.card K
⊢ (M ^ Fintype.card K).trace = M.trace ^ Fintype.card K
have inr₁ : -coeff (M ^ Fintype.card K).charpoly (Fintype.card n - 1) = (-coeff M.charpoly (Fintype.card n - 1)) ^ Fintype.card K
Tactic: rw [Matrix.trace_eq_neg_charpoly_coeff, Matrix.trace_eq_neg_charpoly_coeff,
    FiniteField.Matrix.charpoly_pow_card, FiniteField.pow_card]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField (goal)
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
K : Type u_2
inst_2 : Field K
inst_3 : Fintype K
M : Matrix n n K
h : Nonempty n
inr : -coeff (M ^ Fintype.card K).charpoly (Fintype.card n - 1) = M.trace ^ Fintype.card K
inr₁ :
  -coeff (M ^ Fintype.card K).charpoly (Fintype.card n - 1) = (-coeff M.charpoly (Fintype.card n - 1)) ^ Fintype.card K
⊢ (M ^ Fintype.card K).trace = M.trace ^ Fintype.card K
have inr₂ : -coeff M.charpoly (Fintype.card n - 1) = (-coeff M.charpoly (Fintype.card n - 1)) ^ Fintype.card K
Tactic: rw [Matrix.trace_eq_neg_charpoly_coeff, Matrix.trace_eq_neg_charpoly_coeff,
    FiniteField.Matrix.charpoly_pow_card, FiniteField.pow_card]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField (goal)
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
K : Type u_2
inst_2 : Field K
inst_3 : Fintype K
M : Matrix n n K
h : Nonempty n
inr : -coeff (M ^ Fintype.card K).charpoly (Fintype.card n - 1) = M.trace ^ Fintype.card K
inr₁ :
  -coeff (M ^ Fintype.card K).charpoly (Fintype.card n - 1) = (-coeff M.charpoly (Fintype.card n - 1)) ^ Fintype.card K
inr₂ : -coeff M.charpoly (Fintype.card n - 1) = (-coeff M.charpoly (Fintype.card n - 1)) ^ Fintype.card K
⊢ (M ^ Fintype.card K).trace = M.trace ^ Fintype.card K
have inr₃ : -coeff M.charpoly (Fintype.card n - 1) = -coeff M.charpoly (Fintype.card n - 1)
Tactic: rw [Matrix.trace_eq_neg_charpoly_coeff, Matrix.trace_eq_neg_charpoly_coeff,
    FiniteField.Matrix.charpoly_pow_card, FiniteField.pow_card]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField (hypothesis)
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
p : ℕ
inst_2 : Fact (Nat.Prime p)
M : Matrix n n (ZMod p)
⊢ (M ^ p).trace = M.trace ^ p
have h : (M ^ Fintype.card (ZMod p)).trace = M.trace ^ Fintype.card (ZMod p)
Tactic: have h := FiniteField.trace_pow_card M
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField (goal)
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
p : ℕ
inst_2 : Fact (Nat.Prime p)
M : Matrix n n (ZMod p)
h : (M ^ Fintype.card (ZMod p)).trace = M.trace ^ Fintype.card (ZMod p)
⊢ (M ^ p).trace = M.trace ^ p
have rwa : ∀ (h : (M ^ p).trace = M.trace ^ p), (M ^ p).trace = M.trace ^ p
Tactic: rwa [ZMod.card] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap (goal)
Goal:
ι : Type u_1
inst : Fintype ι
M : Type u_2
inst_1 : AddCommGroup M
R : Type u_3
inst_2 : CommRing R
inst_3 : Module R M
b : ι → M
inst_4 : DecidableEq ι
A : Matrix ι ι R
j : ι
⊢ Eq.{u_2 + 1} (α := M)
    ((((fromMatrix R b : (a : Matrix ι ι R) → (ι → R) →ₗ[R] M) A : (ι → R) →ₗ[R] M) : (a : ι → R) → M)
        (Pi.single (M := fun (a : ι) ↦ R) j 1) :
      M)
    (∑ i : ι, A i j • b i : M)
have rw : Eq.{u_2 + 1} (α := M) (∑ i : ι, HSMul.hSMul (α := Rᵐᵒᵖ) (MulOpposite.op 1) (A.col j) i • b i) (∑ i : ι, A i j • b i)
Tactic: rw [PiToModule.fromMatrix_apply, Fintype.linearCombination_apply, Matrix.mulVec_single]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap (goal)
Goal:
ι : Type u_1
inst : Fintype ι
M : Type u_2
inst_1 : AddCommGroup M
R : Type u_3
inst_2 : CommRing R
inst_3 : Module R M
b : ι → M
inst_4 : DecidableEq ι
A : Matrix ι ι R
j : ι
⊢ Eq.{u_2 + 1} (α := M) (∑ i : ι, HSMul.hSMul (α := Rᵐᵒᵖ) (MulOpposite.op 1) (A.col j) i • b i) (∑ i : ι, A i j • b i)
have simp_rw : Eq.{u_2 + 1} (α := M) (∑ x : ι, HSMul.hSMul (α := Rᵐᵒᵖ) 1 (A.col j) x • b x) (∑ i : ι, A i j • b i)
Tactic: simp_rw [MulOpposite.op_one, one_smul, col_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap (goal)
Goal:
ι : Type u_1
inst : Fintype ι
M : Type u_2
inst_1 : AddCommGroup M
R : Type u_3
inst_2 : CommRing R
inst_3 : Module R M
b : ι → M
inst_4 : DecidableEq ι
A : Matrix ι ι R
j : ι
simp_rw : Eq.{u_2 + 1} (α := M) (∑ x : ι, HSMul.hSMul (α := Rᵐᵒᵖ) 1 (A.col j) x • b x) (∑ i : ι, A i j • b i)
⊢ Eq.{u_2 + 1} (α := M) (∑ i : ι, HSMul.hSMul (α := Rᵐᵒᵖ) (MulOpposite.op 1) (A.col j) i • b i) (∑ i : ι, A i j • b i)
have simp_rw₁ : Eq.{u_2 + 1} (α := M) (∑ x : ι, A.col j x • b x) (∑ i : ι, A i j • b i)
Tactic: simp_rw [MulOpposite.op_one, one_smul, col_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap (goal)
Goal:
ι : Type u_1
inst : Fintype ι
M : Type u_2
inst_1 : AddCommGroup M
R : Type u_3
inst_2 : CommRing R
inst_3 : Module R M
b : ι → M
inst_4 : DecidableEq ι
f : Module.End R M
i : ι
⊢ Eq.{u_2 + 1} (α := M)
    ((((fromEnd R b : (a : Module.End R M) → (ι → R) →ₗ[R] M) f : (ι → R) →ₗ[R] M) : (a : ι → R) → M)
        (Pi.single (M := fun (a : ι) ↦ R) i 1) :
      M)
    ((f : (a : M) → M) (b i) : M)
have rw : Eq (α := M)
  ((f : (a : M) → M) ((Fintype.linearCombination R b : (a : ι → R) → M) (Pi.single (M := fun (a : ι) ↦ R) i 1) : M) : M)
  ((f : (a : M) → M) (b i) : M)
Tactic: rw [PiToModule.fromEnd_apply, Fintype.linearCombination_apply_single, one_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap (goal)
Goal:
ι : Type u_1
inst : Fintype ι
M : Type u_2
inst_1 : AddCommGroup M
R : Type u_3
inst_2 : CommRing R
inst_3 : Module R M
b : ι → M
inst_4 : DecidableEq ι
f : Module.End R M
i : ι
rw :
  Eq (α := M)
    ((f : (a : M) → M) ((Fintype.linearCombination R b : (a : ι → R) → M) (Pi.single (M := fun (a : ι) ↦ R) i 1) : M) :
      M)
    ((f : (a : M) → M) (b i) : M)
⊢ Eq.{u_2 + 1} (α := M)
    ((((fromEnd R b : (a : Module.End R M) → (ι → R) →ₗ[R] M) f : (ι → R) →ₗ[R] M) : (a : ι → R) → M)
        (Pi.single (M := fun (a : ι) ↦ R) i 1) :
      M)
    ((f : (a : M) → M) (b i) : M)
have rw₁ : Eq (α := M) ((f : (a : M) → M) (HSMul.hSMul.{u_3, u_2, u_2} (α := R) 1 (b i)) : M) ((f : (a : M) → M) (b i) : M)
Tactic: rw [PiToModule.fromEnd_apply, Fintype.linearCombination_apply_single, one_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap (goal)
Goal:
ι : Type u_1
inst : Fintype ι
M : Type u_2
inst_1 : AddCommGroup M
R : Type u_3
inst_2 : CommRing R
inst_3 : Module R M
b : ι → M
inst_4 : DecidableEq ι
f : Module.End R M
i : ι
rw :
  Eq (α := M)
    ((f : (a : M) → M) ((Fintype.linearCombination R b : (a : ι → R) → M) (Pi.single (M := fun (a : ι) ↦ R) i 1) : M) :
      M)
    ((f : (a : M) → M) (b i) : M)
rw₁ : Eq (α := M) ((f : (a : M) → M) (HSMul.hSMul.{u_3, u_2, u_2} (α := R) 1 (b i)) : M) ((f : (a : M) → M) (b i) : M)
⊢ Eq.{u_2 + 1} (α := M)
    ((((fromEnd R b : (a : Module.End R M) → (ι → R) →ₗ[R] M) f : (ι → R) →ₗ[R] M) : (a : ι → R) → M)
        (Pi.single (M := fun (a : ι) ↦ R) i 1) :
      M)
    ((f : (a : M) → M) (b i) : M)
have rw₂ : Eq (α := M) ((f : (a : M) → M) (b i) : M) ((f : (a : M) → M) (b i) : M)
Tactic: rw [PiToModule.fromEnd_apply, Fintype.linearCombination_apply_single, one_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap (goal)
Goal:
ι : Type u_1
inst : Fintype ι
M : Type u_2
inst_1 : AddCommGroup M
R : Type u_3
inst_2 : CommRing R
inst_3 : Module R M
b : ι → M
hb : Eq (α := Submodule R M) (Submodule.span R (Set.range b)) ⊤
x y : Module.End R M
e :
  Eq (α := (ι → R) →ₗ[R] M) ((fromEnd R b : (a : Module.End R M) → (ι → R) →ₗ[R] M) x : (ι → R) →ₗ[R] M)
    ((fromEnd R b : (a : Module.End R M) → (ι → R) →ₗ[R] M) y : (ι → R) →ₗ[R] M)
⊢ x = y
have h : ∀ (m : M), Eq (α := M) ((x : (a : M) → M) m : M) ((y : (a : M) → M) m : M)
Tactic: ext m
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap (goal)
Goal:
ι : Type u_1
inst : Fintype ι
M : Type u_2
inst_1 : AddCommGroup M
R : Type u_3
inst_2 : CommRing R
inst_3 : Module R M
b : ι → M
hb : Eq (α := Submodule R M) (Submodule.span R (Set.range b)) ⊤
x y : Module.End R M
e :
  Eq (α := (ι → R) →ₗ[R] M) ((fromEnd R b : (a : Module.End R M) → (ι → R) →ₗ[R] M) x : (ι → R) →ₗ[R] M)
    ((fromEnd R b : (a : Module.End R M) → (ι → R) →ₗ[R] M) y : (ι → R) →ₗ[R] M)
m : M
⊢ Membership.mem (γ := Submodule R M) (LinearMap.range (Fintype.linearCombination R b)) m
have rw : Membership.mem (γ := Submodule R M) ⊤ m
Tactic: rw [(Fintype.range_linearCombination R b).trans hb]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap (goal)
Goal:
ι : Type u_1
inst : Fintype ι
M : Type u_2
inst_1 : AddCommGroup M
R : Type u_3
inst_2 : CommRing R
inst_3 : Module R M
b : ι → M
hb : Eq (α := Submodule R M) (Submodule.span R (Set.range b)) ⊤
x y : Module.End R M
e :
  Eq (α := (ι → R) →ₗ[R] M) ((fromEnd R b : (a : Module.End R M) → (ι → R) →ₗ[R] M) x : (ι → R) →ₗ[R] M)
    ((fromEnd R b : (a : Module.End R M) → (ι → R) →ₗ[R] M) y : (ι → R) →ₗ[R] M)
m : M
⊢ Eq (α := M) ((x : (a : M) → M) m : M) ((y : (a : M) → M) m : M)
have h : ∀ (m : ι → R),
  Eq (α := M) ((x : (a : M) → M) ((Fintype.linearCombination R b : (a : ι → R) → M) m : M) : M)
    ((y : (a : M) → M) ((Fintype.linearCombination R b : (a : ι → R) → M) m : M) : M)
Tactic: obtain ⟨m, rfl⟩ : m ∈ LinearMap.range (Fintype.linearCombination R b) := by
    rw [(Fintype.range_linearCombination R b).trans hb]
    exact Submodule.mem_top
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap (goal)
Goal:
ι : Type u_1
inst : Fintype ι
M : Type u_2
inst_1 : AddCommGroup M
R : Type u_3
inst_2 : CommRing R
inst_3 : Module R M
b : ι → M
inst_4 : DecidableEq ι
A : Matrix ι ι R
f : Module.End R M
⊢ Represents b A f ↔ ∀ (j : ι), Eq (α := M) (∑ i : ι, A i j • b i : M) ((f : (a : M) → M) (b j) : M)
have mp : Represents b A f → ∀ (j : ι), Eq (α := M) (∑ i : ι, A i j • b i : M) ((f : (a : M) → M) (b j) : M)
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap (goal)
Goal:
ι : Type u_1
inst : Fintype ι
M : Type u_2
inst_1 : AddCommGroup M
R : Type u_3
inst_2 : CommRing R
inst_3 : Module R M
b : ι → M
inst_4 : DecidableEq ι
A : Matrix ι ι R
f : Module.End R M
mp : Represents b A f → ∀ (j : ι), Eq (α := M) (∑ i : ι, A i j • b i : M) ((f : (a : M) → M) (b j) : M)
⊢ Represents b A f ↔ ∀ (j : ι), Eq (α := M) (∑ i : ι, A i j • b i : M) ((f : (a : M) → M) (b j) : M)
have mpr : (∀ (j : ι), Eq (α := M) (∑ i : ι, A i j • b i : M) ((f : (a : M) → M) (b j) : M)) → Represents b A f
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap (hypothesis)
Goal:
ι : Type u_1
inst : Fintype ι
M : Type u_2
inst_1 : AddCommGroup M
R : Type u_3
inst_2 : CommRing R
inst_3 : Module R M
b : ι → M
inst_4 : DecidableEq ι
A : Matrix ι ι R
f : Module.End R M
h : Represents b A f
i : ι
⊢ Eq (α := M) (∑ i_1 : ι, A i_1 i • b i_1 : M) ((f : (a : M) → M) (b i) : M)
have this : Eq.{u_2 + 1} (α := M)
  ((((PiToModule.fromMatrix R b : (a : Matrix ι ι R) → (ι → R) →ₗ[R] M) A : (ι → R) →ₗ[R] M) : (a : ι → R) → M)
      (Pi.single (M := fun (a : ι) ↦ R) i 1) :
    M)
  ((((PiToModule.fromEnd R b : (a : Module.End R M) → (ι → R) →ₗ[R] M) f : (ι → R) →ₗ[R] M) : (a : ι → R) → M)
      (Pi.single (M := fun (a : ι) ↦ R) i 1) :
    M)
Tactic: have := LinearMap.congr_fun h (Pi.single i 1)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap (goal)
Goal:
ι : Type u_1
inst : Fintype ι
M : Type u_2
inst_1 : AddCommGroup M
R : Type u_3
inst_2 : CommRing R
inst_3 : Module R M
b : ι → M
inst_4 : DecidableEq ι
A : Matrix ι ι R
f : Module.End R M
h : Represents b A f
i : ι
this :
  Eq.{u_2 + 1} (α := M)
    ((((PiToModule.fromMatrix R b : (a : Matrix ι ι R) → (ι → R) →ₗ[R] M) A : (ι → R) →ₗ[R] M) : (a : ι → R) → M)
        (Pi.single (M := fun (a : ι) ↦ R) i 1) :
      M)
    ((((PiToModule.fromEnd R b : (a : Module.End R M) → (ι → R) →ₗ[R] M) f : (ι → R) →ₗ[R] M) : (a : ι → R) → M)
        (Pi.single (M := fun (a : ι) ↦ R) i 1) :
      M)
⊢ Eq (α := M) (∑ i_1 : ι, A i_1 i • b i_1 : M) ((f : (a : M) → M) (b i) : M)
have mp : ∀
  (this :
    Eq.{u_2 + 1} (α := M)
      ((((PiToModule.fromMatrix R b : (a : Matrix ι ι R) → (ι → R) →ₗ[R] M) A : (ι → R) →ₗ[R] M) : (a : ι → R) → M)
          (Pi.single (M := fun (a : ι) ↦ R) i 1) :
        M)
      ((f : (a : M) → M) (b i) : M)),
  Eq (α := M) (∑ i_1 : ι, A i_1 i • b i_1 : M) ((f : (a : M) → M) (b i) : M)
Tactic: rwa [PiToModule.fromEnd_apply_single_one, PiToModule.fromMatrix_apply_single_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap (goal)
Goal:
ι : Type u_1
inst : Fintype ι
M : Type u_2
inst_1 : AddCommGroup M
R : Type u_3
inst_2 : CommRing R
inst_3 : Module R M
b : ι → M
inst_4 : DecidableEq ι
A : Matrix ι ι R
f : Module.End R M
h : Represents b A f
i : ι
this :
  Eq.{u_2 + 1} (α := M)
    ((((PiToModule.fromMatrix R b : (a : Matrix ι ι R) → (ι → R) →ₗ[R] M) A : (ι → R) →ₗ[R] M) : (a : ι → R) → M)
        (Pi.single (M := fun (a : ι) ↦ R) i 1) :
      M)
    ((((PiToModule.fromEnd R b : (a : Module.End R M) → (ι → R) →ₗ[R] M) f : (ι → R) →ₗ[R] M) : (a : ι → R) → M)
        (Pi.single (M := fun (a : ι) ↦ R) i 1) :
      M)
mp :
  ∀
    (this :
      Eq.{u_2 + 1} (α := M)
        ((((PiToModule.fromMatrix R b : (a : Matrix ι ι R) → (ι → R) →ₗ[R] M) A : (ι → R) →ₗ[R] M) : (a : ι → R) → M)
            (Pi.single (M := fun (a : ι) ↦ R) i 1) :
          M)
        ((f : (a : M) → M) (b i) : M)),
    Eq (α := M) (∑ i_1 : ι, A i_1 i • b i_1 : M) ((f : (a : M) → M) (b i) : M)
⊢ Eq (α := M) (∑ i_1 : ι, A i_1 i • b i_1 : M) ((f : (a : M) → M) (b i) : M)
have mp₁ : ∀ (this : Eq (α := M) (∑ i_1 : ι, A i_1 i • b i_1 : M) ((f : (a : M) → M) (b i) : M)),
  Eq (α := M) (∑ i_1 : ι, A i_1 i • b i_1 : M) ((f : (a : M) → M) (b i) : M)
Tactic: rwa [PiToModule.fromEnd_apply_single_one, PiToModule.fromMatrix_apply_single_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap (goal)
Goal:
ι : Type u_1
inst : Fintype ι
M : Type u_2
inst_1 : AddCommGroup M
R : Type u_3
inst_2 : CommRing R
inst_3 : Module R M
b : ι → M
inst_4 : DecidableEq ι
A : Matrix ι ι R
f : Module.End R M
h : ∀ (j : ι), Eq (α := M) (∑ i : ι, A i j • b i : M) ((f : (a : M) → M) (b j) : M)
⊢ Represents b A f
have mpr : ∀ (i : ι),
  Eq.{u_2 + 1} (α := M)
    ((((PiToModule.fromMatrix R b : (a : Matrix ι ι R) → (ι → R) →ₗ[R] M) A ∘ₗ LinearMap.single R (fun (i : ι) ↦ R) i :
            R →ₗ[R] M) :
          (a : R) → M)
        1 :
      M)
    ((((PiToModule.fromEnd R b : (a : Module.End R M) → (ι → R) →ₗ[R] M) f ∘ₗ LinearMap.single R (fun (i : ι) ↦ R) i :
            R →ₗ[R] M) :
          (a : R) → M)
        1 :
      M)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap (goal)
Goal:
ι : Type u_1
inst : Fintype ι
M : Type u_2
inst_1 : AddCommGroup M
R : Type u_3
inst_2 : CommRing R
inst_3 : Module R M
b : ι → M
inst_4 : DecidableEq ι
A : Matrix ι ι R
f : Module.End R M
h : ∀ (j : ι), Eq (α := M) (∑ i : ι, A i j • b i : M) ((f : (a : M) → M) (b j) : M)
i : ι
⊢ Eq.{u_2 + 1} (α := M)
    ((((PiToModule.fromMatrix R b : (a : Matrix ι ι R) → (ι → R) →ₗ[R] M) A ∘ₗ LinearMap.single R (fun (i : ι) ↦ R) i :
            R →ₗ[R] M) :
          (a : R) → M)
        1 :
      M)
    ((((PiToModule.fromEnd R b : (a : Module.End R M) → (ι → R) →ₗ[R] M) f ∘ₗ LinearMap.single R (fun (i : ι) ↦ R) i :
            R →ₗ[R] M) :
          (a : R) → M)
        1 :
      M)
have mpr : Eq (α := M) (∑ i_1 : ι, A i_1 i • b i_1 : M) ((f : (a : M) → M) (b i) : M)
Tactic: simp_rw [LinearMap.comp_apply, LinearMap.coe_single, PiToModule.fromEnd_apply_single_one,
      PiToModule.fromMatrix_apply_single_one]