-- Mathlib/Algebra/Module/LinearMap/Polynomial.lean
lemma polyCharpoly_coeff_eq_zero_of_basis (b : Basis ι R L) (b' : Basis ι' R L) (k : ℕ)
    (H : (polyCharpoly φ b).coeff k = 0) :
    (polyCharpoly φ b').coeff k = 0

Proof state:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ι' : Type u_6
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup L
inst✝⁸ : Module R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
φ : L →ₗ[R] End R M
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ι'
inst✝¹ : Free R M
inst✝ : Module.Finite R M
b : Basis ι R L
b' : Basis ι' R L
k : ℕ
B : Basis (Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M) R (End R M) := (Free.chooseBasis R M).end
H : ↑(MvPolynomial.bind₁ (toMvPolynomial b B φ)) ((charpoly.univ R (Free.ChooseBasisIndex R M)).coeff k) = 0
g : ι → MvPolynomial ι' R := toMvPolynomial b' b id
⊢ ↑(MvPolynomial.bind₁ (toMvPolynomial b' B φ)) ((charpoly.univ R (Free.ChooseBasisIndex R M)).coeff k) = 0

Tactic:
apply_fun (MvPolynomial.bind₁ g) at H

Result:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ι' : Type u_6
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup L
inst✝⁸ : Module R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
φ : L →ₗ[R] End R M
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ι'
inst✝¹ : Free R M
inst✝ : Module.Finite R M
b : Basis ι R L
b' : Basis ι' R L
k : ℕ
B : Basis (Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M) R (End R M) := (Free.chooseBasis R M).end
g : ι → MvPolynomial ι' R := toMvPolynomial b' b id
H :
  (MvPolynomial.bind₁ g)
      (↑(MvPolynomial.bind₁ (toMvPolynomial b B φ)) ((charpoly.univ R (Free.ChooseBasisIndex R M)).coeff k)) =
    (MvPolynomial.bind₁ g) 0
⊢ ↑(MvPolynomial.bind₁ (toMvPolynomial b' B φ)) ((charpoly.univ R (Free.ChooseBasisIndex R M)).coeff k) = 0

Proof state:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ι' : Type u_6
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup L
inst✝⁸ : Module R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
φ : L →ₗ[R] End R M
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ι'
inst✝¹ : Free R M
inst✝ : Module.Finite R M
b : Basis ι R L
b' : Basis ι' R L
k : ℕ
H :
  ↑(MvPolynomial.bind₁ (toMvPolynomial b (Free.chooseBasis R M).end φ))
      ((charpoly.univ R (Free.ChooseBasisIndex R M)).coeff k) =
    0
⊢ ↑(MvPolynomial.bind₁ (toMvPolynomial b' (Free.chooseBasis R M).end φ))
      ((charpoly.univ R (Free.ChooseBasisIndex R M)).coeff k) =
    0

Tactic:
set B := (Module.Free.chooseBasis R M).end

Result:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ι' : Type u_6
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup L
inst✝⁸ : Module R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
φ : L →ₗ[R] End R M
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ι'
inst✝¹ : Free R M
inst✝ : Module.Finite R M
b : Basis ι R L
b' : Basis ι' R L
k : ℕ
B : Basis (Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M) R (End R M) := (Free.chooseBasis R M).end
H : ↑(MvPolynomial.bind₁ (toMvPolynomial b B φ)) ((charpoly.univ R (Free.ChooseBasisIndex R M)).coeff k) = 0
⊢ ↑(MvPolynomial.bind₁ (toMvPolynomial b' B φ)) ((charpoly.univ R (Free.ChooseBasisIndex R M)).coeff k) = 0

Proof state:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ι' : Type u_6
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup L
inst✝⁸ : Module R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
φ : L →ₗ[R] End R M
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ι'
inst✝¹ : Free R M
inst✝ : Module.Finite R M
b : Basis ι R L
b' : Basis ι' R L
k : ℕ
B : Basis (Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M) R (End R M) := (Free.chooseBasis R M).end
g : ι → MvPolynomial ι' R := toMvPolynomial b' b id
H :
  (MvPolynomial.bind₁ g)
      (↑(MvPolynomial.bind₁ (toMvPolynomial b B φ)) ((charpoly.univ R (Free.ChooseBasisIndex R M)).coeff k)) =
    (MvPolynomial.bind₁ g) 0
this : toMvPolynomial b' B φ = fun i => (MvPolynomial.bind₁ g) (toMvPolynomial b B φ i)
⊢ ↑(MvPolynomial.bind₁ (toMvPolynomial b' B φ)) ((charpoly.univ R (Free.ChooseBasisIndex R M)).coeff k) = 0

Tactic:
rwa [map_zero, RingHom.coe_coe, MvPolynomial.bind₁_bind₁, ← this] at H

Result:
no goals

Proof state:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ι' : Type u_6
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup L
inst✝⁸ : Module R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
φ : L →ₗ[R] End R M
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ι'
inst✝¹ : Free R M
inst✝ : Module.Finite R M
b : Basis ι R L
b' : Basis ι' R L
k : ℕ
H : (φ.polyCharpoly b).coeff k = 0
⊢ (φ.polyCharpoly b').coeff k = 0

Tactic:
rw [polyCharpoly, polyCharpolyAux, Polynomial.coeff_map] at H ⊢

Result:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ι' : Type u_6
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup L
inst✝⁸ : Module R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
φ : L →ₗ[R] End R M
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ι'
inst✝¹ : Free R M
inst✝ : Module.Finite R M
b : Basis ι R L
b' : Basis ι' R L
k : ℕ
H :
  ↑(MvPolynomial.bind₁ (toMvPolynomial b (Free.chooseBasis R M).end φ))
      ((charpoly.univ R (Free.ChooseBasisIndex R M)).coeff k) =
    0
⊢ ↑(MvPolynomial.bind₁ (toMvPolynomial b' (Free.chooseBasis R M).end φ))
      ((charpoly.univ R (Free.ChooseBasisIndex R M)).coeff k) =
    0

Proof state:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ι' : Type u_6
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup L
inst✝⁸ : Module R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
φ : L →ₗ[R] End R M
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ι'
inst✝¹ : Free R M
inst✝ : Module.Finite R M
b : Basis ι R L
b' : Basis ι' R L
k : ℕ
B : Basis (Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M) R (End R M) := (Free.chooseBasis R M).end
H : ↑(MvPolynomial.bind₁ (toMvPolynomial b B φ)) ((charpoly.univ R (Free.ChooseBasisIndex R M)).coeff k) = 0
⊢ ↑(MvPolynomial.bind₁ (toMvPolynomial b' B φ)) ((charpoly.univ R (Free.ChooseBasisIndex R M)).coeff k) = 0

Tactic:
set g := toMvPolynomial b' b LinearMap.id

Result:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ι' : Type u_6
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup L
inst✝⁸ : Module R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
φ : L →ₗ[R] End R M
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ι'
inst✝¹ : Free R M
inst✝ : Module.Finite R M
b : Basis ι R L
b' : Basis ι' R L
k : ℕ
B : Basis (Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M) R (End R M) := (Free.chooseBasis R M).end
H : ↑(MvPolynomial.bind₁ (toMvPolynomial b B φ)) ((charpoly.univ R (Free.ChooseBasisIndex R M)).coeff k) = 0
g : ι → MvPolynomial ι' R := toMvPolynomial b' b id
⊢ ↑(MvPolynomial.bind₁ (toMvPolynomial b' B φ)) ((charpoly.univ R (Free.ChooseBasisIndex R M)).coeff k) = 0