-- Mathlib/Algebra/Module/LinearMap/Polynomial.lean
lemma polyCharpoly_coeff_isHomogeneous (i j : ℕ) (hij : i + j = finrank R M) [Nontrivial R] :
    ((polyCharpoly φ b).coeff i).IsHomogeneous j

Proof state:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
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✝³ : DecidableEq ι
inst✝² : Free R M
inst✝¹ : Module.Finite R M
b : Basis ι R L
i j : ℕ
hij : i + j = Fintype.card (Free.ChooseBasisIndex R M)
inst✝ : Nontrivial R
⊢ ((φ.polyCharpoly b).coeff i).IsHomogeneous j

Tactic:
rw [polyCharpoly, polyCharpolyAux, Polynomial.coeff_map, ← one_mul j]

Result:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
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✝³ : DecidableEq ι
inst✝² : Free R M
inst✝¹ : Module.Finite R M
b : Basis ι R L
i j : ℕ
hij : i + j = Fintype.card (Free.ChooseBasisIndex R M)
inst✝ : Nontrivial R
⊢ (↑(MvPolynomial.bind₁ (toMvPolynomial b (Free.chooseBasis R M).end φ))
        ((charpoly.univ R (Free.ChooseBasisIndex R M)).coeff i)).IsHomogeneous
    (1 * j)

Proof state:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
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✝³ : DecidableEq ι
inst✝² : Free R M
inst✝¹ : Module.Finite R M
b : Basis ι R L
i j : ℕ
hij : i + j = Fintype.card (Free.ChooseBasisIndex R M)
inst✝ : Nontrivial R
⊢ (↑(MvPolynomial.bind₁ (toMvPolynomial b (Free.chooseBasis R M).end φ))
        ((charpoly.univ R (Free.ChooseBasisIndex R M)).coeff i)).IsHomogeneous
    (1 * j)

Tactic:
apply (charpoly.univ_coeff_isHomogeneous _ _ _ _ hij).eval₂

Result:
case hf
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
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✝³ : DecidableEq ι
inst✝² : Free R M
inst✝¹ : Module.Finite R M
b : Basis ι R L
i j : ℕ
hij : i + j = Fintype.card (Free.ChooseBasisIndex R M)
inst✝ : Nontrivial R
⊢ ∀ (r : R), ((algebraMap R (MvPolynomial ι R)) r).IsHomogeneous 0

case hg
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
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✝³ : DecidableEq ι
inst✝² : Free R M
inst✝¹ : Module.Finite R M
b : Basis ι R L
i j : ℕ
hij : i + j = Fintype.card (Free.ChooseBasisIndex R M)
inst✝ : Nontrivial R
⊢ ∀ (i : Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M),
    (toMvPolynomial b (Free.chooseBasis R M).end φ i).IsHomogeneous 1

Proof state:
case hg
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
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✝³ : DecidableEq ι
inst✝² : Free R M
inst✝¹ : Module.Finite R M
b : Basis ι R L
i j : ℕ
hij : i + j = Fintype.card (Free.ChooseBasisIndex R M)
inst✝ : Nontrivial R
⊢ ∀ (i : Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M),
    (toMvPolynomial b (Free.chooseBasis R M).end φ i).IsHomogeneous 1

Tactic:
exact LinearMap.toMvPolynomial_isHomogeneous _ _ _

Result:
no goals

Proof state:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
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✝³ : DecidableEq ι
inst✝² : Free R M
inst✝¹ : Module.Finite R M
b : Basis ι R L
i j : ℕ
hij : i + j = finrank R M
inst✝ : Nontrivial R
⊢ ((φ.polyCharpoly b).coeff i).IsHomogeneous j

Tactic:
rw [finrank_eq_card_chooseBasisIndex] at hij

Result:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
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✝³ : DecidableEq ι
inst✝² : Free R M
inst✝¹ : Module.Finite R M
b : Basis ι R L
i j : ℕ
hij : i + j = Fintype.card (Free.ChooseBasisIndex R M)
inst✝ : Nontrivial R
⊢ ((φ.polyCharpoly b).coeff i).IsHomogeneous j

Proof state:
case hf
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
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✝³ : DecidableEq ι
inst✝² : Free R M
inst✝¹ : Module.Finite R M
b : Basis ι R L
i j : ℕ
hij : i + j = Fintype.card (Free.ChooseBasisIndex R M)
inst✝ : Nontrivial R
⊢ ∀ (r : R), ((algebraMap R (MvPolynomial ι R)) r).IsHomogeneous 0

Tactic:
exact fun r ↦ MvPolynomial.isHomogeneous_C _ _

Result:
no goals