-- Mathlib/Algebra/Module/LinearMap/Polynomial.lean
/-- `LinearMap.polyCharpolyAux` is independent of the choice of basis of the target module.

Proof strategy:
1. Rewrite `polyCharpolyAux` as the (honest, ordinary) characteristic polynomial
   of the basechange of `φ` to the multivariate polynomial ring `MvPolynomial ι R`.
2. Use that the characteristic polynomial of a linear map is independent of the choice of basis.
   This independence result is used transitively via
   `LinearMap.polyCharpolyAux_map_aeval` and `LinearMap.polyCharpolyAux_map_eq_charpoly`. -/
lemma polyCharpolyAux_basisIndep {ιM' : Type*} [Fintype ιM'] [DecidableEq ιM']
    (bₘ' : Basis ιM' R M) :
    polyCharpolyAux φ b bₘ = polyCharpolyAux φ b bₘ'

Proof state:
case a
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup L
inst✝⁸ : Module R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
φ : L →ₗ[R] Module.End R M
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ιM
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
ιM' : Type u_8
inst✝¹ : Fintype ιM'
inst✝ : DecidableEq ιM'
bₘ' : Basis ιM' R M
f : Polynomial (MvPolynomial ι R) → Polynomial (MvPolynomial ι R) := Polynomial.map (aeval X).toRingHom
hf : Function.Injective f
⊢ f (φ.polyCharpolyAux b bₘ) = f (φ.polyCharpolyAux b bₘ')

Tactic:
let _h1 : Module.Finite (MvPolynomial ι R) (TensorProduct R (MvPolynomial ι R) M) :=
  Module.Finite.of_basis (basis (MvPolynomial ι R) bₘ)

Result:
case a
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup L
inst✝⁸ : Module R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
φ : L →ₗ[R] Module.End R M
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ιM
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
ιM' : Type u_8
inst✝¹ : Fintype ιM'
inst✝ : DecidableEq ιM'
bₘ' : Basis ιM' R M
f : Polynomial (MvPolynomial ι R) → Polynomial (MvPolynomial ι R) := Polynomial.map (aeval X).toRingHom
hf : Function.Injective f
_h1 : Module.Finite (MvPolynomial ι R) (TensorProduct R (MvPolynomial ι R) M) :=
  Module.Finite.of_basis (basis (MvPolynomial ι R) bₘ)
⊢ f (φ.polyCharpolyAux b bₘ) = f (φ.polyCharpolyAux b bₘ')

Proof state:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup L
inst✝⁸ : Module R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
φ : L →ₗ[R] Module.End R M
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ιM
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
ιM' : Type u_8
inst✝¹ : Fintype ιM'
inst✝ : DecidableEq ιM'
bₘ' : Basis ιM' R M
f : Polynomial (MvPolynomial ι R) → Polynomial (MvPolynomial ι R) := Polynomial.map (aeval X).toRingHom
⊢ φ.polyCharpolyAux b bₘ = φ.polyCharpolyAux b bₘ'

Tactic:
have hf : Function.Injective f := by
  simp only [f, aeval_X_left, AlgHom.toRingHom_eq_coe, AlgHom.id_toRingHom, Polynomial.map_id]
  exact Polynomial.map_injective (RingHom.id _) Function.injective_id

Result:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup L
inst✝⁸ : Module R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
φ : L →ₗ[R] Module.End R M
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ιM
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
ιM' : Type u_8
inst✝¹ : Fintype ιM'
inst✝ : DecidableEq ιM'
bₘ' : Basis ιM' R M
f : Polynomial (MvPolynomial ι R) → Polynomial (MvPolynomial ι R) := Polynomial.map (aeval X).toRingHom
hf : Function.Injective f
⊢ φ.polyCharpolyAux b bₘ = φ.polyCharpolyAux b bₘ'

Proof state:
case a
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup L
inst✝⁸ : Module R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
φ : L →ₗ[R] Module.End R M
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ιM
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
ιM' : Type u_8
inst✝¹ : Fintype ιM'
inst✝ : DecidableEq ιM'
bₘ' : Basis ιM' R M
f : Polynomial (MvPolynomial ι R) → Polynomial (MvPolynomial ι R) := Polynomial.map (aeval X).toRingHom
hf : Function.Injective f
_h1 : Module.Finite (MvPolynomial ι R) (TensorProduct R (MvPolynomial ι R) M) :=
  Module.Finite.of_basis (basis (MvPolynomial ι R) bₘ)
_h2 : Module.Free (MvPolynomial ι R) (TensorProduct R (MvPolynomial ι R) M) :=
  Module.Free.of_basis (basis (MvPolynomial ι R) bₘ)
⊢ f (φ.polyCharpolyAux b bₘ) = f (φ.polyCharpolyAux b bₘ')

Tactic:
simp only [f, polyCharpolyAux_map_aeval, polyCharpolyAux_map_aeval]

Result:
no goals