awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField
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 :
  (expand K (Fintype.card K) : (a : K[X]) → K[X]) (M ^ Fintype.card K).charpoly =
    HPow.hPow (α := K[X]) M.charpoly (Fintype.card K)
⊢ HPow.hPow (α := K[X]) (M ^ Fintype.card K).charpoly (Fintype.card K) =
    HPow.hPow (α := K[X]) M.charpoly (Fintype.card K)

Tactic:
rw [← FiniteField.expand_card]

Premises used: FiniteField.expand_card
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField
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 :
  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])
⊢ (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)

Tactic:
rw [AlgHom.map_det, ← coe_detMonoidHom, ← (detMonoidHom : Matrix n n K[X] →* K[X]).map_pow]

Premises used: Matrix.detMonoidHom, Matrix.coe_detMonoidHom, AlgHom.map_det, MonoidHom.map_pow
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField
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 :
  (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)
⊢ 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:
apply congr_arg det

Premises used: congr_arg, Matrix.det
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField
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)

Tactic:
matPolyEquiv.injective ?_

Premises used: matPolyEquiv, AlgEquiv.injective
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField
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 :
  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])
⊢ (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:
refine matPolyEquiv.injective ?_

Premises used: matPolyEquiv, AlgEquiv.injective
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField
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])
inl₁ : Commute (S := (Matrix n n K)[X]) X ((C : (a : Matrix n n K) → (Matrix n n K)[X]) M)
⊢ 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:
rw [map_pow, matPolyEquiv_charmatrix, hk, sub_pow_char_pow_of_commute, ← C_pow]

Premises used: sub_pow_char_pow_of_commute, map_pow, Matrix.matPolyEquiv_charmatrix, Polynomial.C_pow
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField
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)
⊢ (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:
(id (matPolyEquiv_eq_X_pow_sub_C (p ^ k) M) :)

Premises used: id, HPow.hPow, matPolyEquiv_eq_X_pow_sub_C
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField
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)
⊢ (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:
exact (id (matPolyEquiv_eq_X_pow_sub_C (p ^ k) M) :)

Premises used: id, HPow.hPow, matPolyEquiv_eq_X_pow_sub_C
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField
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)
⊢ Commute (S := (Matrix n n K)[X]) X ((C : (a : Matrix n n K) → (Matrix n n K)[X]) M)

Tactic:
(C M).commute_X

Premises used: Polynomial.C, Polynomial.commute_X, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField
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)
⊢ Commute (S := (Matrix n n K)[X]) X ((C : (a : Matrix n n K) → (Matrix n n K)[X]) M)

Tactic:
exact (C M).commute_X

Premises used: Polynomial.C, Polynomial.commute_X, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField
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 : IsEmpty n
⊢ Eq (α := K[X]) (M ^ Fintype.card K).charpoly M.charpoly

Tactic:
congr_arg _ (Subsingleton.elim _ _)

Premises used: congr_arg, Subsingleton.elim
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField
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 : IsEmpty n
⊢ Eq (α := K[X]) (M ^ Fintype.card K).charpoly M.charpoly

Tactic:
exact congr_arg _ (Subsingleton.elim _ _)

Premises used: congr_arg, Subsingleton.elim
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField
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 ^ Fintype.card (ZMod p)).charpoly M.charpoly

Tactic:
have h := FiniteField.Matrix.charpoly_pow_card M
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField
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
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (h : Eq (α := (ZMod p)[X]) (M ^ p).charpoly M.charpoly), Eq (α := (ZMod p)[X]) (M ^ p).charpoly M.charpoly
⊢ Eq (α := (ZMod p)[X]) (M ^ p).charpoly M.charpoly

Tactic:
rwa [ZMod.card] at h

Premises used: ZMod.card
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField
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
inr : Nonempty n → (M ^ Fintype.card K).trace = M.trace ^ Fintype.card K
⊢ (M ^ Fintype.card K).trace = M.trace ^ Fintype.card K

Tactic:
cases isEmpty_or_nonempty n

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField
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 : IsEmpty n
⊢ (M ^ Fintype.card K).trace = M.trace ^ Fintype.card K

Tactic:
simp [Matrix.trace]

Premises used: Matrix.trace
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField
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
inr₃ inr₄ : -coeff M.charpoly (Fintype.card n - 1) = -coeff M.charpoly (Fintype.card n - 1)
⊢ (M ^ Fintype.card K).trace = 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]

Premises used: Matrix.trace_eq_neg_charpoly_coeff, FiniteField.Matrix.charpoly_pow_card, FiniteField.pow_card
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField
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 ^ Fintype.card (ZMod p)).trace = M.trace ^ Fintype.card (ZMod p)

Tactic:
have h := FiniteField.trace_pow_card M
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField
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)
rwa rwa₁ rwa₂ rwa₃ : ∀ (h : (M ^ p).trace = M.trace ^ p), (M ^ p).trace = M.trace ^ p
⊢ (M ^ p).trace = M.trace ^ p

Tactic:
rwa [ZMod.card] at h

Premises used: ZMod.card
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
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
w : ι → R
⊢ Eq.{u_2 + 1} (α := M)
    ((((fromMatrix R b : (a : Matrix ι ι R) → (ι → R) →ₗ[R] M) A : (ι → R) →ₗ[R] M) : (a : ι → R) → M) w : M)
    ((Fintype.linearCombination R b : (a : ι → R) → M) (A *ᵥ w) : M)

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, dotProduct, Matrix.mulVec, Finset.sum, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
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 : ι
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)
⊢ 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)

Tactic:
rw [PiToModule.fromMatrix_apply, Fintype.linearCombination_apply, Matrix.mulVec_single]

Premises used: PiToModule.fromMatrix_apply, Fintype.linearCombination_apply, Matrix.mulVec_single
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
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)
simp_rw₁ : Eq.{u_2 + 1} (α := M) (∑ x : ι, 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)

Tactic:
simp_rw [MulOpposite.op_one, one_smul, col_apply]

Premises used: Matrix.col_apply, one_smul, MulOpposite.op_one
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
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
f : Module.End R M
w : ι → R
⊢ Eq.{u_2 + 1} (α := M)
    ((((fromEnd R b : (a : Module.End R M) → (ι → R) →ₗ[R] M) f : (ι → R) →ₗ[R] M) : (a : ι → R) → M) w : M)
    ((f : (a : M) → M) ((Fintype.linearCombination R b : (a : ι → R) → M) w : M) : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
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)
rw₂ rw₃ : Eq (α := M) ((f : (a : M) → M) (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)

Tactic:
rw [PiToModule.fromEnd_apply, Fintype.linearCombination_apply_single, one_smul]

Premises used: PiToModule.fromEnd_apply, one_smul, Fintype.linearCombination_apply_single
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
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)
h : ∀ (m : M), Eq (α := M) ((x : (a : M) → M) m : M) ((y : (a : M) → M) m : M)
⊢ x = y

Tactic:
ext m
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
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
rw : Membership.mem (γ := Submodule R M) ⊤ m
⊢ Membership.mem (γ := Submodule R M) (LinearMap.range (Fintype.linearCombination R b)) m

Tactic:
rw [(Fintype.range_linearCombination R b).trans hb]

Premises used: Fintype.range_linearCombination, Eq.trans
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
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) ⊤ m

Tactic:
Submodule.mem_top

Premises used: Submodule.mem_top
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
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) ⊤ m

Tactic:
exact Submodule.mem_top

Premises used: Submodule.mem_top
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
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
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)
⊢ Eq (α := M) ((x : (a : M) → M) m : M) ((y : (a : 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

Premises used: LinearMap.range, Fintype.linearCombination, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
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 : ι → 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:
(LinearMap.congr_fun e m :)

Premises used: LinearMap.congr_fun
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
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 : ι → 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:
exact (LinearMap.congr_fun e m :)

Premises used: LinearMap.congr_fun
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
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
x : ι → R
⊢ Eq.{u_2 + 1} (α := M) ((Fintype.linearCombination R b : (a : ι → R) → M) (A *ᵥ x) : M)
    ((f : (a : M) → M) ((Fintype.linearCombination R b : (a : ι → R) → M) x : M) : M)

Tactic:
LinearMap.congr_fun h x

Premises used: Multiset.sum, Multiset.foldr, dotProduct, LinearMap.congr_fun, Matrix.mulVec, Finset.sum
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
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 ↔
    ∀ (x : ι → R),
      Eq.{u_2 + 1} (α := M) ((Fintype.linearCombination R b : (a : ι → R) → M) (A *ᵥ x) : M)
        ((f : (a : M) → M) ((Fintype.linearCombination R b : (a : ι → R) → M) x : M) : M)

Tactic:
⟨fun e x => e.congr_fun x, fun H => LinearMap.ext fun x => H x⟩

Premises used: LinearMap.ext, Matrix.Represents.congr_fun, Iff.intro
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
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)
mpr : (∀ (j : ι), Eq (α := M) (∑ i : ι, A i j • b i : M) ((f : (a : M) → M) (b j) : M)) → Represents b A f
⊢ Represents b A f ↔ ∀ (j : ι), Eq (α := M) (∑ i : ι, A i j • b i : M) ((f : (a : M) → M) (b j) : M)

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
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.{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)