awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst : CommRing R
inst_1 : AddCommGroup L
inst_2 : Module R L
inst_3 : AddCommGroup M
inst_4 : Module R M
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) L (End R M)
inst_5 : Fintype ι
inst_6 : Fintype ιM
inst_7 : DecidableEq ι
inst_8 : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
A : Type u_8
inst_9 : CommRing A
inst_10 : Algebra R A
ij kl : ιM × ιM
⊢ Eq.{u_8 + 1} (α := A)
    ((((Basis.repr (Basis.end (basis A bₘ)) : (a : End A (TensorProduct R A M)) → ιM × ιM →₀ A)
              ((({
                        toFun := fun (a : A) ↦
                          HSMul.hSMul (β := (M →ₗ[R] M) →ₗ[R] TensorProduct R A M →ₗ[A] TensorProduct R A M) a
                            (baseChangeHom R A M M),
                        map_add' := ⋯, map_smul' := ⋯ } :
                      (a : A) → (M →ₗ[R] M) →ₗ[R] TensorProduct R A M →ₗ[A] TensorProduct R A M)
                    1 :
                  (a : M →ₗ[R] M) → TensorProduct R A M →ₗ[A] TensorProduct R A M)
                ((bₘ.end : (a : ιM × ιM) → End R M) kl)) :
            Finsupp.{u_7, u_8} (ιM × ιM) A) :
          (a : ιM × ιM) → A)
        ij :
      A)
    (if kl = ij then 1 else 0 : A)
have e_f : Eq.{u_8 + 1} (α := A)
  ((((Basis.repr (Basis.end (basis A bₘ)) : (a : End A (TensorProduct R A M)) → ιM × ιM →₀ A)
            (HSMul.hSMul (α := A) (β := TensorProduct R A M →ₗ[A] TensorProduct R A M) 1
              (baseChange A ((bₘ.end : (a : ιM × ιM) → End R M) kl))) :
          Finsupp.{u_7, u_8} (ιM × ιM) A) :
        (a : ιM × ιM) → A)
      ij :
    A)
  (if kl = ij then 1 else 0 : A)
Tactic: dsimp only [coe_mk, AddHom.coe_mk, smul_apply, baseChangeHom_apply]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst : CommRing R
inst_1 : AddCommGroup L
inst_2 : Module R L
inst_3 : AddCommGroup M
inst_4 : Module R M
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) L (End R M)
inst_5 : Fintype ι
inst_6 : Fintype ιM
inst_7 : DecidableEq ι
inst_8 : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
A : Type u_8
inst_9 : CommRing A
inst_10 : Algebra R A
ij kl : ιM × ιM
⊢ Eq.{u_8 + 1} (α := A)
    ((((Basis.repr (Basis.end (basis A bₘ)) : (a : End A (TensorProduct R A M)) → ιM × ιM →₀ A)
              (HSMul.hSMul (α := A) (β := TensorProduct R A M →ₗ[A] TensorProduct R A M) 1
                (baseChange A ((bₘ.end : (a : ιM × ιM) → End R M) kl))) :
            Finsupp.{u_7, u_8} (ιM × ιM) A) :
          (a : ιM × ιM) → A)
        ij :
      A)
    (if kl = ij then 1 else 0 : A)
have e_f : Eq.{u_8 + 1} (α := A)
  ((((Basis.repr (Basis.end (basis A bₘ)) : (a : End A (TensorProduct R A M)) → ιM × ιM →₀ A)
            (baseChange A ((bₘ.end : (a : ιM × ιM) → End R M) kl)) :
          Finsupp.{u_7, u_8} (ιM × ιM) A) :
        (a : ιM × ιM) → A)
      ij :
    A)
  (if kl = ij then 1 else 0 : A)
Tactic: rw [one_smul, Basis.baseChange_end, Basis.repr_self_apply]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst : CommRing R
inst_1 : AddCommGroup L
inst_2 : Module R L
inst_3 : AddCommGroup M
inst_4 : Module R M
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) L (End R M)
inst_5 : Fintype ι
inst_6 : Fintype ιM
inst_7 : DecidableEq ι
inst_8 : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
A : Type u_8
inst_9 : CommRing A
inst_10 : Algebra R A
ij kl : ιM × ιM
e_f :
  Eq.{u_8 + 1} (α := A)
    ((((Basis.repr (Basis.end (basis A bₘ)) : (a : End A (TensorProduct R A M)) → ιM × ιM →₀ A)
              (baseChange A ((bₘ.end : (a : ιM × ιM) → End R M) kl)) :
            Finsupp.{u_7, u_8} (ιM × ιM) A) :
          (a : ιM × ιM) → A)
        ij :
      A)
    (if kl = ij then 1 else 0 : A)
⊢ Eq.{u_8 + 1} (α := A)
    ((((Basis.repr (Basis.end (basis A bₘ)) : (a : End A (TensorProduct R A M)) → ιM × ιM →₀ A)
              (HSMul.hSMul (α := A) (β := TensorProduct R A M →ₗ[A] TensorProduct R A M) 1
                (baseChange A ((bₘ.end : (a : ιM × ιM) → End R M) kl))) :
            Finsupp.{u_7, u_8} (ιM × ιM) A) :
          (a : ιM × ιM) → A)
        ij :
      A)
    (if kl = ij then 1 else 0 : A)
have e_f₁ : Eq.{u_8 + 1} (α := A)
  ((((Basis.repr (Basis.end (basis A bₘ)) : (a : End A (TensorProduct R A M)) → ιM × ιM →₀ A)
            ((Basis.end (basis A bₘ) : (a : ιM × ιM) → End A (TensorProduct R A M)) kl) :
          Finsupp.{u_7, u_8} (ιM × ιM) A) :
        (a : ιM × ιM) → A)
      ij :
    A)
  (if kl = ij then 1 else 0 : A)
Tactic: rw [one_smul, Basis.baseChange_end, Basis.repr_self_apply]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst : CommRing R
inst_1 : AddCommGroup L
inst_2 : Module R L
inst_3 : AddCommGroup M
inst_4 : Module R M
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) L (End R M)
inst_5 : Fintype ι
inst_6 : Fintype ιM
inst_7 : DecidableEq ι
inst_8 : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
A : Type u_8
inst_9 : CommRing A
inst_10 : Algebra R A
ij kl : ιM × ιM
e_f :
  Eq.{u_8 + 1} (α := A)
    ((((Basis.repr (Basis.end (basis A bₘ)) : (a : End A (TensorProduct R A M)) → ιM × ιM →₀ A)
              (baseChange A ((bₘ.end : (a : ιM × ιM) → End R M) kl)) :
            Finsupp.{u_7, u_8} (ιM × ιM) A) :
          (a : ιM × ιM) → A)
        ij :
      A)
    (if kl = ij then 1 else 0 : A)
e_f₁ :
  Eq.{u_8 + 1} (α := A)
    ((((Basis.repr (Basis.end (basis A bₘ)) : (a : End A (TensorProduct R A M)) → ιM × ιM →₀ A)
              ((Basis.end (basis A bₘ) : (a : ιM × ιM) → End A (TensorProduct R A M)) kl) :
            Finsupp.{u_7, u_8} (ιM × ιM) A) :
          (a : ιM × ιM) → A)
        ij :
      A)
    (if kl = ij then 1 else 0 : A)
⊢ Eq.{u_8 + 1} (α := A)
    ((((Basis.repr (Basis.end (basis A bₘ)) : (a : End A (TensorProduct R A M)) → ιM × ιM →₀ A)
              (HSMul.hSMul (α := A) (β := TensorProduct R A M →ₗ[A] TensorProduct R A M) 1
                (baseChange A ((bₘ.end : (a : ιM × ιM) → End R M) kl))) :
            Finsupp.{u_7, u_8} (ιM × ιM) A) :
          (a : ιM × ιM) → A)
        ij :
      A)
    (if kl = ij then 1 else 0 : A)
have e_f₂ : Eq.{u_8 + 1} (α := A) (if kl = ij then 1 else 0) (if kl = ij then 1 else 0)
Tactic: rw [one_smul, Basis.baseChange_end, Basis.repr_self_apply]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst : CommRing R
inst_1 : AddCommGroup L
inst_2 : Module R L
inst_3 : AddCommGroup M
inst_4 : Module R M
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) L (End R M)
inst_5 : Fintype ι
inst_6 : Fintype ιM
inst_7 : DecidableEq ι
inst_8 : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
x : L
⊢ Polynomial.map (eval (⇑((b.repr : (a : L) → ι →₀ R) x : ι →₀ R) : (a : ι) → R)) (φ.polyCharpolyAux b bₘ) =
    Matrix.charpoly.{u_1, u_7} (n := ιM)
      ((toMatrix bₘ bₘ : (a : M →ₗ[R] M) → Matrix ιM ιM R) ((φ : (a : L) → End R M) x))
have rw : Eq.{u_1 + 1} (α := Polynomial R)
  (Matrix.charpoly.{u_1, u_7} (n := ιM)
    ((of : (a : ιM → ιM → R) → Matrix ιM ιM R)
      (Function.curry fun (i : ιM × ιM) ↦
        (eval (⇑((b.repr : (a : L) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) : (a : MvPolynomial ι R) → R)
          (toMvPolynomial b bₘ.end φ i))))
  (Matrix.charpoly.{u_1, u_7} (n := ιM)
    ((toMatrix bₘ bₘ : (a : M →ₗ[R] M) → Matrix ιM ιM R) ((φ : (a : L) → End R M) x)))
Tactic: rw [polyCharpolyAux, Polynomial.map_map, ← MvPolynomial.eval₂Hom_C_eq_bind₁,
    MvPolynomial.comp_eval₂Hom, charpoly.univ_map_eval₂Hom]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst : CommRing R
inst_1 : AddCommGroup L
inst_2 : Module R L
inst_3 : AddCommGroup M
inst_4 : Module R M
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) L (End R M)
inst_5 : Fintype ι
inst_6 : Fintype ιM
inst_7 : DecidableEq ι
inst_8 : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
x : L
⊢ Eq.{u_1 + 1} (α := Polynomial R)
    (Matrix.charpoly.{u_1, u_7} (n := ιM)
      ((of : (a : ιM → ιM → R) → Matrix ιM ιM R)
        (Function.curry fun (i : ιM × ιM) ↦
          (eval (⇑((b.repr : (a : L) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) : (a : MvPolynomial ι R) → R)
            (toMvPolynomial b bₘ.end φ i))))
    (Matrix.charpoly.{u_1, u_7} (n := ιM)
      ((toMatrix bₘ bₘ : (a : M →ₗ[R] M) → Matrix ιM ιM R) ((φ : (a : L) → End R M) x)))
have e_M : Eq (α := Matrix ιM ιM R)
  ((of : (a : ιM → ιM → R) → Matrix ιM ιM R)
      (Function.curry fun (i : ιM × ιM) ↦
        (eval (⇑((b.repr : (a : L) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) : (a : MvPolynomial ι R) → R)
          (toMvPolynomial b bₘ.end φ i)) :
    Matrix ιM ιM R)
  ((toMatrix bₘ bₘ : (a : M →ₗ[R] M) → Matrix ιM ιM R) ((φ : (a : L) → End R M) x) : Matrix ιM ιM R)
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst : CommRing R
inst_1 : AddCommGroup L
inst_2 : Module R L
inst_3 : AddCommGroup M
inst_4 : Module R M
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) L (End R M)
inst_5 : Fintype ι
inst_6 : Fintype ιM
inst_7 : DecidableEq ι
inst_8 : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
x : L
⊢ Eq (α := Matrix ιM ιM R)
    ((of : (a : ιM → ιM → R) → Matrix ιM ιM R)
        (Function.curry fun (i : ιM × ιM) ↦
          (eval (⇑((b.repr : (a : L) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) : (a : MvPolynomial ι R) → R)
            (toMvPolynomial b bₘ.end φ i)) :
      Matrix ιM ιM R)
    ((toMatrix bₘ bₘ : (a : M →ₗ[R] M) → Matrix ιM ιM R) ((φ : (a : L) → End R M) x) : Matrix ιM ιM R)
have e_M : ∀ (i j : ιM),
  Eq.{u_1 + 1} (α := R)
    ((of : (a : ιM → ιM → R) → Matrix ιM ιM R)
        (Function.curry fun (i : ιM × ιM) ↦
          (eval (⇑((b.repr : (a : L) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) : (a : MvPolynomial ι R) → R)
            (toMvPolynomial b bₘ.end φ i))
        i j :
      R)
    ((toMatrix bₘ bₘ : (a : M →ₗ[R] M) → Matrix ιM ιM R) ((φ : (a : L) → End R M) x) i j : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst : CommRing R
inst_1 : AddCommGroup L
inst_2 : Module R L
inst_3 : AddCommGroup M
inst_4 : Module R M
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) L (End R M)
inst_5 : Fintype ι
inst_6 : Fintype ιM
inst_7 : DecidableEq ι
inst_8 : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
x : L
i j : ιM
⊢ Eq.{u_1 + 1} (α := R)
    ((of : (a : ιM → ιM → R) → Matrix ιM ιM R)
        (Function.curry fun (i : ιM × ιM) ↦
          (eval (⇑((b.repr : (a : L) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) : (a : MvPolynomial ι R) → R)
            (toMvPolynomial b bₘ.end φ i))
        i j :
      R)
    ((toMatrix bₘ bₘ : (a : M →ₗ[R] M) → Matrix ιM ιM R) ((φ : (a : L) → End R M) x) i j : R)
have e_M : Eq.{u_1 + 1} (α := R)
  ((((bₘ.end.repr : (a : End R M) → ιM × ιM →₀ R) ((φ : (a : L) → End R M) x) : Finsupp.{u_7, u_1} (ιM × ιM) R) :
        (a : ιM × ιM) → R)
      (i, j) :
    R)
  ((toMatrix bₘ bₘ : (a : M →ₗ[R] M) → Matrix ιM ιM R) ((φ : (a : L) → End R M) x) i j : R)
Tactic: rw [of_apply, Function.curry_apply, toMvPolynomial_eval_eq_apply, LinearEquiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (hypothesis)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst : CommRing R
inst_1 : AddCommGroup L
inst_2 : Module R L
inst_3 : AddCommGroup M
inst_4 : Module R M
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) L (End R M)
inst_5 : Fintype ι
inst_6 : Fintype ιM
inst_7 : DecidableEq ι
inst_8 : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
inst_9 : Module.Finite R M
inst_10 : Free R M
x : L
⊢ Polynomial.map (eval (⇑((b.repr : (a : L) → ι →₀ R) x : ι →₀ R) : (a : ι) → R)) (φ.polyCharpolyAux b bₘ) =
    charpoly.{u_1, u_3} (M := M) ((φ : (a : L) → End R M) x)
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst : CommRing R
inst_1 : AddCommGroup L
inst_2 : Module R L
inst_3 : AddCommGroup M
inst_4 : Module R M
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) L (End R M)
inst_5 : Fintype ι
inst_6 : Fintype ιM
inst_7 : DecidableEq ι
inst_8 : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
inst_9 : Module.Finite R M
inst_10 : Free R M
x : L
h : Nontrivial R
⊢ Polynomial.map (eval (⇑((b.repr : (a : L) → ι →₀ R) x : ι →₀ R) : (a : ι) → R)) (φ.polyCharpolyAux b bₘ) =
    charpoly.{u_1, u_3} (M := M) ((φ : (a : L) → End R M) x)
have rw : Eq.{u_1 + 1} (α := Polynomial R)
  (Matrix.charpoly.{u_1, u_7} (n := ιM)
    ((toMatrix bₘ bₘ : (a : M →ₗ[R] M) → Matrix ιM ιM R) ((φ : (a : L) → End R M) x)))
  (charpoly.{u_1, u_3} (M := M) ((φ : (a : L) → End R M) x))
Tactic: rw [polyCharpolyAux_map_eq_toMatrix_charpoly, LinearMap.charpoly_toMatrix]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst : CommRing R
inst_1 : AddCommGroup L
inst_2 : Module R L
inst_3 : AddCommGroup M
inst_4 : Module R M
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) L (End R M)
inst_5 : Fintype ι
inst_6 : Fintype ιM
inst_7 : DecidableEq ι
inst_8 : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
inst_9 : Module.Finite R M
inst_10 : Free R M
x : L
h : Nontrivial R
rw :
  Eq.{u_1 + 1} (α := Polynomial R)
    (Matrix.charpoly.{u_1, u_7} (n := ιM)
      ((toMatrix bₘ bₘ : (a : M →ₗ[R] M) → Matrix ιM ιM R) ((φ : (a : L) → End R M) x)))
    (charpoly.{u_1, u_3} (M := M) ((φ : (a : L) → End R M) x))
⊢ Polynomial.map (eval (⇑((b.repr : (a : L) → ι →₀ R) x : ι →₀ R) : (a : ι) → R)) (φ.polyCharpolyAux b bₘ) =
    charpoly.{u_1, u_3} (M := M) ((φ : (a : L) → End R M) x)
have rw₁ : Eq.{u_1 + 1} (α := Polynomial R) (charpoly.{u_1, u_3} (M := M) ((φ : (a : L) → End R M) x))
  (charpoly.{u_1, u_3} (M := M) ((φ : (a : L) → End R M) x))
Tactic: rw [polyCharpolyAux_map_eq_toMatrix_charpoly, LinearMap.charpoly_toMatrix]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (hypothesis)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst : CommRing R
inst_1 : AddCommGroup L
inst_2 : Module R L
inst_3 : AddCommGroup M
inst_4 : Module R M
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) L (End R M)
inst_5 : Fintype ι
inst_6 : Fintype ιM
inst_7 : DecidableEq ι
inst_8 : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
inst_9 : Module.Finite R M
inst_10 : Free R M
x : L
i : ℕ
⊢ Eq.{u_1 + 1} (α := R)
    ((eval (⇑((b.repr : (a : L) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) : (a : MvPolynomial ι R) → R)
        ((φ.polyCharpolyAux b bₘ).coeff i) :
      R)
    (Polynomial.coeff (charpoly.{u_1, u_3} (M := M) ((φ : (a : L) → End R M) x)) i : R)
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst : CommRing R
inst_1 : AddCommGroup L
inst_2 : Module R L
inst_3 : AddCommGroup M
inst_4 : Module R M
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) L (End R M)
inst_5 : Fintype ι
inst_6 : Fintype ιM
inst_7 : DecidableEq ι
inst_8 : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
inst_9 : Module.Finite R M
inst_10 : Free R M
x : L
i : ℕ
h : Nontrivial R
⊢ Eq.{u_1 + 1} (α := R)
    ((eval (⇑((b.repr : (a : L) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) : (a : MvPolynomial ι R) → R)
        ((φ.polyCharpolyAux b bₘ).coeff i) :
      R)
    (Polynomial.coeff (charpoly.{u_1, u_3} (M := M) ((φ : (a : L) → End R M) x)) i : R)
have rw : (eval (⇑((b.repr : (a : L) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) : (a : MvPolynomial ι R) → R)
    ((φ.polyCharpolyAux b bₘ).coeff i) =
  (Polynomial.map (eval (⇑((b.repr : (a : L) → ι →₀ R) x : ι →₀ R) : (a : ι) → R)) (φ.polyCharpolyAux b bₘ)).coeff i
Tactic: rw [← polyCharpolyAux_map_eq_charpoly φ b bₘ x, Polynomial.coeff_map]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst : CommRing R
inst_1 : AddCommGroup L
inst_2 : Module R L
inst_3 : AddCommGroup M
inst_4 : Module R M
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) L (End R M)
inst_5 : Fintype ι
inst_6 : Fintype ιM
inst_7 : DecidableEq ι
inst_8 : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
inst_9 : Module.Finite R M
inst_10 : Free R M
x : L
i : ℕ
h : Nontrivial R
rw :
  (eval (⇑((b.repr : (a : L) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) : (a : MvPolynomial ι R) → R)
      ((φ.polyCharpolyAux b bₘ).coeff i) =
    (Polynomial.map (eval (⇑((b.repr : (a : L) → ι →₀ R) x : ι →₀ R) : (a : ι) → R)) (φ.polyCharpolyAux b bₘ)).coeff i
⊢ Eq.{u_1 + 1} (α := R)
    ((eval (⇑((b.repr : (a : L) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) : (a : MvPolynomial ι R) → R)
        ((φ.polyCharpolyAux b bₘ).coeff i) :
      R)
    (Polynomial.coeff (charpoly.{u_1, u_3} (M := M) ((φ : (a : L) → End R M) x)) i : R)
have rw₁ : Eq.{u_1 + 1} (α := R)
  ((eval (⇑((b.repr : (a : L) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) : (a : MvPolynomial ι R) → R)
      ((φ.polyCharpolyAux b bₘ).coeff i) :
    R)
  ((eval (⇑((b.repr : (a : L) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) : (a : MvPolynomial ι R) → R)
      ((φ.polyCharpolyAux b bₘ).coeff i) :
    R)
Tactic: rw [← polyCharpolyAux_map_eq_charpoly φ b bₘ x, Polynomial.coeff_map]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst : CommRing R
inst_1 : AddCommGroup L
inst_2 : Module R L
inst_3 : AddCommGroup M
inst_4 : Module R M
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) L (End R M)
inst_5 : Fintype ι
inst_6 : Fintype ιM
inst_7 : DecidableEq ι
inst_8 : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
A : Type u_8
inst_9 : CommRing A
inst_10 : Algebra R A
inst_11 : Module.Finite A (A ⊗[R] M)
inst_12 : Free A (A ⊗[R] M)
x : ι → A
⊢ Eq (α := Polynomial A) (Polynomial.map (AlgHom.toRingHom (aeval x)) (φ.polyCharpolyAux b bₘ))
    (charpoly (M := A ⊗[R] M)
      ((tensorProduct R A M M ∘ₗ baseChange A φ : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M)
        ((LinearEquiv.symm (Basis.repr (basis A b)) : (a : ι →₀ A) → A ⊗[R] L)
          ((Equiv.symm Finsupp.equivFunOnFinite : (a : ι → A) → ι →₀ A) x))))
have rw : Eq (α := Polynomial A) (Polynomial.map (AlgHom.toRingHom (aeval x)) (φ.polyCharpolyAux b bₘ))
  (Polynomial.map (RingHom.comp (eval x) (MvPolynomial.map (algebraMap R A))) (φ.polyCharpolyAux b bₘ))
Tactic: rw [← polyCharpolyAux_map_eval (tensorProduct R A M M ∘ₗ baseChange A φ) _ (basis A bₘ),
    polyCharpolyAux_baseChange, Polynomial.map_map]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst : CommRing R
inst_1 : AddCommGroup L
inst_2 : Module R L
inst_3 : AddCommGroup M
inst_4 : Module R M
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) L (End R M)
inst_5 : Fintype ι
inst_6 : Fintype ιM
inst_7 : DecidableEq ι
inst_8 : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
A : Type u_8
inst_9 : CommRing A
inst_10 : Algebra R A
inst_11 : Module.Finite A (A ⊗[R] M)
inst_12 : Free A (A ⊗[R] M)
x : ι → A
⊢ Eq (α := Polynomial A) (Polynomial.map (AlgHom.toRingHom (aeval x)) (φ.polyCharpolyAux b bₘ))
    (Polynomial.map (RingHom.comp (eval x) (MvPolynomial.map (algebraMap R A))) (φ.polyCharpolyAux b bₘ))
have e_f : Eq (α := MvPolynomial ι R →+* A) (AlgHom.toRingHom (aeval x))
  (RingHom.comp (eval x) (MvPolynomial.map (algebraMap R A)))
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst : CommRing R
inst_1 : AddCommGroup L
inst_2 : Module R L
inst_3 : AddCommGroup M
inst_4 : Module R M
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) L (End R M)
inst_5 : Fintype ι
inst_6 : Fintype ιM
inst_7 : DecidableEq ι
inst_8 : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
ιM' : Type u_8
inst_9 : Fintype ιM'
inst_10 : DecidableEq ιM'
bₘ' : Basis ιM' R M
f : Polynomial (MvPolynomial ι R) → Polynomial (MvPolynomial ι R) := Polynomial.map (AlgHom.toRingHom (aeval X))
⊢ Function.Injective f
have simp : Function.Injective (α := Polynomial (MvPolynomial ι R)) (Polynomial.map (RingHom.id (MvPolynomial ι R)))
Tactic: simp only [f, aeval_X_left, AlgHom.toRingHom_eq_coe, AlgHom.id_toRingHom]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (hypothesis)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst : CommRing R
inst_1 : AddCommGroup L
inst_2 : Module R L
inst_3 : AddCommGroup M
inst_4 : Module R M
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) L (End R M)
inst_5 : Fintype ι
inst_6 : Fintype ιM
inst_7 : DecidableEq ι
inst_8 : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
ιM' : Type u_8
inst_9 : Fintype ιM'
inst_10 : DecidableEq ιM'
bₘ' : Basis ιM' R M
f : Polynomial (MvPolynomial ι R) → Polynomial (MvPolynomial ι R) := Polynomial.map (AlgHom.toRingHom (aeval X))
⊢ φ.polyCharpolyAux b bₘ = φ.polyCharpolyAux b bₘ'
have hf : Function.Injective f
Tactic: have hf : Function.Injective f := by
    simp only [f, aeval_X_left, AlgHom.toRingHom_eq_coe, AlgHom.id_toRingHom]
    exact Polynomial.map_injective (RingHom.id _) Function.injective_id
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst : CommRing R
inst_1 : AddCommGroup L
inst_2 : Module R L
inst_3 : AddCommGroup M
inst_4 : Module R M
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) L (End R M)
inst_5 : Fintype ι
inst_6 : Fintype ιM
inst_7 : DecidableEq ι
inst_8 : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
ιM' : Type u_8
inst_9 : Fintype ιM'
inst_10 : DecidableEq ιM'
bₘ' : Basis ιM' R M
f : Polynomial (MvPolynomial ι R) → Polynomial (MvPolynomial ι R) := Polynomial.map (AlgHom.toRingHom (aeval X))
hf : Function.Injective f
⊢ φ.polyCharpolyAux b bₘ = φ.polyCharpolyAux b bₘ'
have a : f (φ.polyCharpolyAux b bₘ) = f (φ.polyCharpolyAux b bₘ')
Tactic: apply hf
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst : CommRing R
inst_1 : AddCommGroup L
inst_2 : Module R L
inst_3 : AddCommGroup M
inst_4 : Module R M
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) L (End R M)
inst_5 : Fintype ι
inst_6 : Fintype ιM
inst_7 : DecidableEq ι
inst_8 : Free R M
inst_9 : Module.Finite R M
b : Basis ι R L
inst_10 : DecidableEq ιM
bₘ : Basis ιM R M
⊢ φ.polyCharpoly b =
    Polynomial.map (↑(bind₁ (toMvPolynomial b bₘ.end φ)) : MvPolynomial (ιM × ιM) R →+* MvPolynomial ι R)
      (charpoly.univ R ιM)
have rw : φ.polyCharpolyAux (ιM := Free.ChooseBasisIndex R M) b (Free.chooseBasis R M) =
  Polynomial.map (↑(bind₁ (toMvPolynomial b bₘ.end φ)) : MvPolynomial (ιM × ιM) R →+* MvPolynomial ι R)
    (charpoly.univ R ιM)
Tactic: rw [polyCharpoly, φ.polyCharpolyAux_basisIndep b (Module.Free.chooseBasis R M) bₘ,
    polyCharpolyAux]