awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
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 (α := Polynomial (MvPolynomial ι R)) (Polynomial.map (RingHom.id (MvPolynomial ι R)))

Tactic:
Polynomial.map_injective (RingHom.id _) Function.injective_id

Premises used: Polynomial.map_injective, Function.injective_id, RingHom.id
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
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 (α := Polynomial (MvPolynomial ι R)) (Polynomial.map (RingHom.id (MvPolynomial ι R)))

Tactic:
exact Polynomial.map_injective (RingHom.id _) Function.injective_id

Premises used: Polynomial.map_injective, Function.injective_id, RingHom.id
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
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

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
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
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
a : f (φ.polyCharpolyAux b bₘ) = f (φ.polyCharpolyAux b bₘ')
⊢ φ.polyCharpolyAux b bₘ = φ.polyCharpolyAux b bₘ'

Tactic:
apply hf
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
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
_h1 : Module.Finite (MvPolynomial ι R) (TensorProduct R (MvPolynomial ι R) M) := ⋯
_h2 : Free (MvPolynomial ι R) (TensorProduct R (MvPolynomial ι R) M) := ⋯
⊢ f (φ.polyCharpolyAux b bₘ) = f (φ.polyCharpolyAux b bₘ')

Tactic:
simp only [f, polyCharpolyAux_map_aeval, polyCharpolyAux_map_aeval]

Premises used: LinearMap.polyCharpolyAux_map_aeval
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
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
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)
rw₁ :
  φ.polyCharpolyAux b bₘ =
    Polynomial.map (↑(bind₁ (toMvPolynomial b bₘ.end φ)) : MvPolynomial (ιM × ιM) R →+* MvPolynomial ι R)
      (charpoly.univ R ιM)
rw₂ rw₃ :
  Eq (α := Polynomial (MvPolynomial ι R))
    (Polynomial.map (↑(bind₁ (toMvPolynomial b bₘ.end φ)) : MvPolynomial (ιM × ιM) R →+* MvPolynomial ι R)
      (charpoly.univ R ιM))
    (Polynomial.map (↑(bind₁ (toMvPolynomial b bₘ.end φ)) : MvPolynomial (ιM × ιM) R →+* MvPolynomial ι R)
      (charpoly.univ R ιM))
⊢ φ.polyCharpoly b =
    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]

Premises used: LinearMap.polyCharpolyAux, LinearMap.polyCharpoly, LinearMap.polyCharpolyAux_basisIndep, Module.Free.chooseBasis
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
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 : DecidableEq ι
inst_7 : Free R M
inst_8 : Module.Finite R M
b : Basis ι R L
⊢ (φ.polyCharpoly b).Monic

Tactic:
(charpoly.univ_monic R _).map _

Premises used: LinearMap.polyCharpolyAux, LinearMap.polyCharpoly, Matrix.charpoly.univ_monic, Polynomial.Monic.map
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
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 : DecidableEq ι
inst_7 : Free R M
inst_8 : Module.Finite R M
b : Basis ι R L
inst_9 : Nontrivial R
⊢ φ.polyCharpoly b ≠ 0

Tactic:
(polyCharpoly_monic _ _).ne_zero

Premises used: LinearMap.polyCharpoly_monic, Polynomial.Monic.ne_zero
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
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 : DecidableEq ι
inst_7 : Free R M
inst_8 : Module.Finite R M
b : Basis ι R L
inst_9 : Nontrivial R
rw : (φ.polyCharpolyAux (ιM := Free.ChooseBasisIndex R M) b (Free.chooseBasis R M)).natDegree = finrank R M
rw₁ :
  Polynomial.natDegree
      (Polynomial.map
        (↑(bind₁ (toMvPolynomial b (Basis.end (Free.chooseBasis R M)) φ)) :
          MvPolynomial (Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M) R →+* MvPolynomial ι R)
        (charpoly.univ R (Free.ChooseBasisIndex R M))) =
    finrank R M
rw₂ :
  Polynomial.natDegree (R := MvPolynomial.{u_3, u_1} (Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M) R)
      (charpoly.univ R (Free.ChooseBasisIndex R M)) =
    finrank R M
rw₃ : Fintype.card.{u_3} (Free.ChooseBasisIndex R M) = finrank R M
rw₄ rw₅ : Fintype.card.{u_3} (Free.ChooseBasisIndex R M) = Fintype.card.{u_3} (Free.ChooseBasisIndex R M)
⊢ (φ.polyCharpoly b).natDegree = finrank R M

Tactic:
rw [polyCharpoly, polyCharpolyAux, (charpoly.univ_monic _ _).natDegree_map,
    charpoly.univ_natDegree, finrank_eq_card_chooseBasisIndex]

Premises used: LinearMap.polyCharpolyAux, LinearMap.polyCharpoly, Matrix.charpoly.univ_monic, Module.finrank_eq_card_chooseBasisIndex, Polynomial.Monic.natDegree_map, Matrix.charpoly.univ_natDegree
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
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 : DecidableEq ι
inst_7 : Free R M
inst_8 : Module.Finite R M
b : Basis ι R L
i j : ℕ
hij : i + j = finrank R M
inst_9 : Nontrivial R
⊢ i + j = Fintype.card.{u_3} (Free.ChooseBasisIndex R M)

Tactic:
rw [finrank_eq_card_chooseBasisIndex] at hij

Premises used: Module.finrank_eq_card_chooseBasisIndex
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
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 : DecidableEq ι
inst_7 : Free R M
inst_8 : Module.Finite R M
b : Basis ι R L
i j : ℕ
hij : i + j = finrank R M
inst_9 : Nontrivial R
hij₁ : i + j = Fintype.card.{u_3} (Free.ChooseBasisIndex R M)
⊢ Nontrivial R

Tactic:
rw [finrank_eq_card_chooseBasisIndex] at hij

Premises used: Module.finrank_eq_card_chooseBasisIndex
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
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 : DecidableEq ι
inst_7 : Free R M
inst_8 : Module.Finite R M
b : Basis ι R L
i j : ℕ
hij : i + j = Fintype.card.{u_3} (Free.ChooseBasisIndex R M)
inst_9 : Nontrivial R
rw :
  IsHomogeneous.{u_5, u_1} (σ := ι) (R := R)
    (((↑(bind₁ (toMvPolynomial b (Basis.end (Free.chooseBasis R M)) φ)) :
          MvPolynomial (Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M) R →+* MvPolynomial ι R) :
        (a : MvPolynomial (Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M) R) → MvPolynomial ι R)
      (Polynomial.coeff (charpoly.univ R (Free.ChooseBasisIndex R M)) i))
    (1 * j)
⊢ ((φ.polyCharpoly b).coeff i).IsHomogeneous j

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

Premises used: LinearMap.polyCharpolyAux, Polynomial.coeff_map, LinearMap.polyCharpoly, one_mul
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
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 : DecidableEq ι
inst_7 : Free R M
inst_8 : Module.Finite R M
b : Basis ι R L
i j : ℕ
hij : i + j = Fintype.card.{u_3} (Free.ChooseBasisIndex R M)
inst_9 : Nontrivial R
hf :
  ∀ (r : R),
    IsHomogeneous.{u_5, u_1} (σ := ι) (R := R) ((algebraMap R (MvPolynomial ι R) : (a : R) → MvPolynomial ι R) r) 0
hg :
  ∀ (i : Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M),
    (toMvPolynomial b (Basis.end (Free.chooseBasis R M)) φ i).IsHomogeneous 1
⊢ IsHomogeneous.{u_5, u_1} (σ := ι) (R := R)
    (((↑(bind₁ (toMvPolynomial b (Basis.end (Free.chooseBasis R M)) φ)) :
          MvPolynomial (Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M) R →+* MvPolynomial ι R) :
        (a : MvPolynomial (Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M) R) → MvPolynomial ι R)
      (Polynomial.coeff (charpoly.univ R (Free.ChooseBasisIndex R M)) i))
    (1 * j)

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

Premises used: Matrix.charpoly.univ_coeff_isHomogeneous, MvPolynomial.IsHomogeneous.eval₂
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
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 : DecidableEq ι
inst_7 : Free R M
inst_8 : Module.Finite R M
b : Basis ι R L
i j : ℕ
hij : i + j = Fintype.card.{u_3} (Free.ChooseBasisIndex R M)
inst_9 : Nontrivial R
⊢ ∀ (r : R),
    IsHomogeneous.{u_5, u_1} (σ := ι) (R := R) ((algebraMap R (MvPolynomial ι R) : (a : R) → MvPolynomial ι R) r) 0

Tactic:
fun r ↦ MvPolynomial.isHomogeneous_C _ _

Premises used: MvPolynomial.isHomogeneous_C
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
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 : DecidableEq ι
inst_7 : Free R M
inst_8 : Module.Finite R M
b : Basis ι R L
i j : ℕ
hij : i + j = Fintype.card.{u_3} (Free.ChooseBasisIndex R M)
inst_9 : Nontrivial R
⊢ ∀ (r : R),
    IsHomogeneous.{u_5, u_1} (σ := ι) (R := R) ((algebraMap R (MvPolynomial ι R) : (a : R) → MvPolynomial ι R) r) 0

Tactic:
exact fun r ↦ MvPolynomial.isHomogeneous_C _ _

Premises used: MvPolynomial.isHomogeneous_C
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
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 : DecidableEq ι
inst_7 : Free R M
inst_8 : Module.Finite R M
b : Basis ι R L
i j : ℕ
hij : i + j = Fintype.card.{u_3} (Free.ChooseBasisIndex R M)
inst_9 : Nontrivial R
⊢ ∀ (i : Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M),
    (toMvPolynomial b (Basis.end (Free.chooseBasis R M)) φ i).IsHomogeneous 1

Tactic:
LinearMap.toMvPolynomial_isHomogeneous _ _ _

Premises used: LinearMap.toMvPolynomial_isHomogeneous
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
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 : DecidableEq ι
inst_7 : Free R M
inst_8 : Module.Finite R M
b : Basis ι R L
i j : ℕ
hij : i + j = Fintype.card.{u_3} (Free.ChooseBasisIndex R M)
inst_9 : Nontrivial R
⊢ ∀ (i : Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M),
    (toMvPolynomial b (Basis.end (Free.chooseBasis R M)) φ i).IsHomogeneous 1

Tactic:
exact LinearMap.toMvPolynomial_isHomogeneous _ _ _

Premises used: LinearMap.toMvPolynomial_isHomogeneous
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
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 : DecidableEq ι
inst_7 : Free R M
inst_8 : Module.Finite R M
b : Basis ι R L
A : Type u_8
inst_9 : CommRing A
inst_10 : Algebra R A
rw :
  Eq (α := Polynomial (MvPolynomial ι A))
    (polyCharpolyAux (L := TensorProduct R A L) (M := TensorProduct R A M) (ιM :=
      Free.ChooseBasisIndex A (TensorProduct R A M)) (tensorProduct R A M M ∘ₗ baseChange A φ) (basis A b)
      (Free.chooseBasis A (TensorProduct R A M)))
    (polyCharpolyAux (L := TensorProduct R A L) (M := TensorProduct R A M) (ιM := Free.ChooseBasisIndex R M)
      (tensorProduct R A M M ∘ₗ baseChange A φ) (basis A b) (basis A (Free.chooseBasis R M)))
⊢ Eq (α := Polynomial (MvPolynomial ι A))
    (polyCharpolyAux (L := TensorProduct R A L) (M := TensorProduct R A M) (ιM :=
      Free.ChooseBasisIndex A (TensorProduct R A M)) (tensorProduct R A M M ∘ₗ baseChange A φ) (basis A b)
      (Free.chooseBasis A (TensorProduct R A M)))
    (Polynomial.map (MvPolynomial.map (algebraMap R A))
      (φ.polyCharpolyAux (ιM := Free.ChooseBasisIndex R M) b (Free.chooseBasis R M)))

Tactic:
rw [← φ.polyCharpolyAux_baseChange]

Premises used: LinearMap.polyCharpolyAux_baseChange
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
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 : DecidableEq ι
inst_7 : Free R M
inst_8 : Module.Finite R M
b : Basis ι R L
A : Type u_8
inst_9 : CommRing A
inst_10 : Algebra R A
⊢ Eq (α := Polynomial (MvPolynomial ι A))
    (polyCharpolyAux (L := TensorProduct R A L) (M := TensorProduct R A M) (ιM :=
      Free.ChooseBasisIndex A (TensorProduct R A M)) (tensorProduct R A M M ∘ₗ baseChange A φ) (basis A b)
      (Free.chooseBasis A (TensorProduct R A M)))
    (polyCharpolyAux (L := TensorProduct R A L) (M := TensorProduct R A M) (ιM := Free.ChooseBasisIndex R M)
      (tensorProduct R A M M ∘ₗ baseChange A φ) (basis A b) (basis A (Free.chooseBasis R M)))

Tactic:
apply polyCharpolyAux_basisIndep

Premises used: LinearMap.polyCharpolyAux_basisIndep
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
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 : DecidableEq ι
inst_7 : Free R M
inst_8 : Module.Finite R M
b : Basis ι R L
x : L
rw :
  Polynomial.map (eval (⇑((b.repr : (a : L) → ι →₀ R) x : ι →₀ R) : (a : ι) → R))
      (φ.polyCharpolyAux (ιM := Free.ChooseBasisIndex R M) b (Free.chooseBasis R M)) =
    charpoly.{u_1, u_3} (M := M) ((φ : (a : L) → End R M) x)
rw₁ 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))
⊢ Polynomial.map (eval (⇑((b.repr : (a : L) → ι →₀ R) x : ι →₀ R) : (a : ι) → R)) (φ.polyCharpoly b) =
    charpoly.{u_1, u_3} (M := M) ((φ : (a : L) → End R M) x)

Tactic:
rw [polyCharpoly, polyCharpolyAux_map_eq_charpoly]

Premises used: LinearMap.polyCharpoly, LinearMap.polyCharpolyAux_map_eq_charpoly
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
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 : DecidableEq ι
inst_7 : Free R M
inst_8 : Module.Finite R M
b : Basis ι R L
x : L
i : ℕ
rw :
  Eq.{u_1 + 1} (α := R)
    ((eval (⇑((b.repr : (a : L) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) : (a : MvPolynomial ι R) → R)
        ((φ.polyCharpolyAux (ιM := Free.ChooseBasisIndex R M) b (Free.chooseBasis R M)).coeff i) :
      R)
    (Polynomial.coeff (charpoly.{u_1, u_3} (M := M) ((φ : (a : L) → End R M) x)) i : R)
rw₁ rw₂ :
  Eq.{u_1 + 1} (α := R) (Polynomial.coeff (charpoly.{u_1, u_3} (M := M) ((φ : (a : L) → End R M) x)) i)
    (Polynomial.coeff (charpoly.{u_1, u_3} (M := M) ((φ : (a : L) → End R M) x)) i)
⊢ Eq.{u_1 + 1} (α := R)
    ((eval (⇑((b.repr : (a : L) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) : (a : MvPolynomial ι R) → R)
        ((φ.polyCharpoly b).coeff i) :
      R)
    (Polynomial.coeff (charpoly.{u_1, u_3} (M := M) ((φ : (a : L) → End R M) x)) i : R)

Tactic:
rw [polyCharpoly, polyCharpolyAux_coeff_eval]

Premises used: LinearMap.polyCharpoly, LinearMap.polyCharpolyAux_coeff_eval
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ι' : Type u_6
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 ι'
inst_7 : DecidableEq ι
inst_8 : DecidableEq ι'
inst_9 : Free R M
inst_10 : Module.Finite R M
b : Basis ι R L
b' : Basis ι' R L
k : ℕ
H : (φ.polyCharpoly b).coeff k = 0
rw :
  ∀
    (H :
      Eq (α := MvPolynomial ι R)
        (((↑(bind₁ (toMvPolynomial b (Basis.end (Free.chooseBasis R M)) φ)) :
                MvPolynomial (Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M) R →+* MvPolynomial ι R) :
              (a : MvPolynomial (Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M) R) → MvPolynomial ι R)
            (Polynomial.coeff (charpoly.univ R (Free.ChooseBasisIndex R M)) k) :
          MvPolynomial ι R)
        (0 : MvPolynomial ι R)),
    Eq (α := MvPolynomial ι' R)
      (((↑(bind₁ (toMvPolynomial b' (Basis.end (Free.chooseBasis R M)) φ)) :
              MvPolynomial (Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M) R →+* MvPolynomial ι' R) :
            (a : MvPolynomial (Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M) R) → MvPolynomial ι' R)
          (Polynomial.coeff (charpoly.univ R (Free.ChooseBasisIndex R M)) k) :
        MvPolynomial ι' R)
      (0 : MvPolynomial ι' R)
⊢ (φ.polyCharpoly b').coeff k = 0

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

Premises used: LinearMap.polyCharpolyAux, Polynomial.coeff_map, LinearMap.polyCharpoly
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ι' : Type u_6
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 ι'
inst_7 : DecidableEq ι
inst_8 : DecidableEq ι'
inst_9 : Free R M
inst_10 : Module.Finite R M
b : Basis ι R L
b' : Basis ι' R L
k : ℕ
H :
  Eq (α := MvPolynomial ι R)
    (((↑(bind₁ (toMvPolynomial b (Basis.end (Free.chooseBasis R M)) φ)) :
            MvPolynomial (Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M) R →+* MvPolynomial ι R) :
          (a : MvPolynomial (Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M) R) → MvPolynomial ι R)
        (Polynomial.coeff (charpoly.univ R (Free.ChooseBasisIndex R M)) k) :
      MvPolynomial ι R)
    (0 : MvPolynomial ι R)
set :
  let B : Basis.{u_3, u_1, u_3} (Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M) R (End R M) :=
    Basis.end (Free.chooseBasis R M);
  ∀
    (H :
      Eq (α := MvPolynomial ι R)
        (((↑(bind₁ (toMvPolynomial b B φ)) :
                MvPolynomial (Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M) R →+* MvPolynomial ι R) :
              (a : MvPolynomial (Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M) R) → MvPolynomial ι R)
            (Polynomial.coeff (charpoly.univ R (Free.ChooseBasisIndex R M)) k) :
          MvPolynomial ι R)
        (0 : MvPolynomial ι R)),
    Eq (α := MvPolynomial ι' R)
      (((↑(bind₁ (toMvPolynomial b' B φ)) :
              MvPolynomial (Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M) R →+* MvPolynomial ι' R) :
            (a : MvPolynomial (Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M) R) → MvPolynomial ι' R)
          (Polynomial.coeff (charpoly.univ R (Free.ChooseBasisIndex R M)) k) :
        MvPolynomial ι' R)
      (0 : MvPolynomial ι' R)
⊢ Eq (α := MvPolynomial ι' R)
    (((↑(bind₁ (toMvPolynomial b' (Basis.end (Free.chooseBasis R M)) φ)) :
            MvPolynomial (Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M) R →+* MvPolynomial ι' R) :
          (a : MvPolynomial (Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M) R) → MvPolynomial ι' R)
        (Polynomial.coeff (charpoly.univ R (Free.ChooseBasisIndex R M)) k) :
      MvPolynomial ι' R)
    (0 : MvPolynomial ι' R)

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

Premises used: Module.Basis.end, Module.Free.chooseBasis