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 : 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)
⊢ φ.polyCharpoly b =
    Polynomial.map (↑(bind₁ (toMvPolynomial b bₘ.end φ)) : MvPolynomial (ιM × ιM) R →+* MvPolynomial ι R)
      (charpoly.univ R ιM)
have rw₁ : φ.polyCharpolyAux b 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]
-- 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
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)
⊢ φ.polyCharpoly b =
    Polynomial.map (↑(bind₁ (toMvPolynomial b bₘ.end φ)) : MvPolynomial (ιM × ιM) R →+* MvPolynomial ι R)
      (charpoly.univ R ιM)
have 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))
Tactic: rw [polyCharpoly, φ.polyCharpolyAux_basisIndep b (Module.Free.chooseBasis R M) bₘ,
    polyCharpolyAux]
-- 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
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).natDegree = finrank R M
have rw : (φ.polyCharpolyAux (ιM := Free.ChooseBasisIndex R M) b (Free.chooseBasis R M)).natDegree = finrank R M
Tactic: rw [polyCharpoly, polyCharpolyAux, (charpoly.univ_monic _ _).natDegree_map,
    charpoly.univ_natDegree, finrank_eq_card_chooseBasisIndex]
-- 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
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
⊢ (φ.polyCharpoly b).natDegree = finrank R M
have 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
Tactic: rw [polyCharpoly, polyCharpolyAux, (charpoly.univ_monic _ _).natDegree_map,
    charpoly.univ_natDegree, finrank_eq_card_chooseBasisIndex]
-- 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
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
⊢ (φ.polyCharpoly b).natDegree = finrank R M
have 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
Tactic: rw [polyCharpoly, polyCharpolyAux, (charpoly.univ_monic _ _).natDegree_map,
    charpoly.univ_natDegree, finrank_eq_card_chooseBasisIndex]
-- 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
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
⊢ (φ.polyCharpoly b).natDegree = finrank R M
have rw₃ : Fintype.card.{u_3} (Free.ChooseBasisIndex R M) = finrank R M
Tactic: rw [polyCharpoly, polyCharpolyAux, (charpoly.univ_monic _ _).natDegree_map,
    charpoly.univ_natDegree, finrank_eq_card_chooseBasisIndex]
-- 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
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
⊢ (φ.polyCharpoly b).natDegree = finrank R M
have rw₄ : Fintype.card.{u_3} (Free.ChooseBasisIndex R M) = Fintype.card.{u_3} (Free.ChooseBasisIndex R M)
Tactic: rw [polyCharpoly, polyCharpolyAux, (charpoly.univ_monic _ _).natDegree_map,
    charpoly.univ_natDegree, finrank_eq_card_chooseBasisIndex]
-- 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
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
⊢ ((φ.polyCharpoly b).coeff i).IsHomogeneous j
have hij₁ : i + j = Fintype.card.{u_3} (Free.ChooseBasisIndex R M)
Tactic: rw [finrank_eq_card_chooseBasisIndex] at hij
Cleared hypotheses: hij, inst_9
-- 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
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
⊢ ((φ.polyCharpoly b).coeff i).IsHomogeneous j
have 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)
Tactic: rw [polyCharpoly, polyCharpolyAux, Polynomial.coeff_map, ← one_mul j]
-- 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
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
⊢ 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)
have hf : ∀ (r : R),
  IsHomogeneous.{u_5, u_1} (σ := ι) (R := R) ((algebraMap R (MvPolynomial ι R) : (a : R) → MvPolynomial ι R) r) 0
Tactic: apply (charpoly.univ_coeff_isHomogeneous _ _ _ _ hij).eval₂
-- 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
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
⊢ 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)
have hg : ∀ (i : Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M),
  (toMvPolynomial b (Basis.end (Free.chooseBasis R M)) φ i).IsHomogeneous 1
Tactic: apply (charpoly.univ_coeff_isHomogeneous _ _ _ _ hij).eval₂
-- 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
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)))
    (Polynomial.map (MvPolynomial.map (algebraMap R A))
      (φ.polyCharpolyAux (ιM := Free.ChooseBasisIndex R M) b (Free.chooseBasis R M)))
have 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)))
Tactic: rw [← φ.polyCharpolyAux_baseChange]
-- 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
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
⊢ 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)
have 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)
Tactic: rw [polyCharpoly, polyCharpolyAux_map_eq_charpoly]
-- 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
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)
⊢ 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)
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 [polyCharpoly, polyCharpolyAux_map_eq_charpoly]
-- 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
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 : ℕ
⊢ 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)
have 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)
Tactic: rw [polyCharpoly, polyCharpolyAux_coeff_eval]
-- 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
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)
⊢ 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)
have 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)
Tactic: rw [polyCharpoly, polyCharpolyAux_coeff_eval]
-- 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
ι' : 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
⊢ (φ.polyCharpoly b').coeff k = 0
have 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)
Tactic: rw [polyCharpoly, polyCharpolyAux, Polynomial.coeff_map] at H ⊢
Cleared hypotheses: H
-- 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
ι' : 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)
⊢ 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)
have 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)
Tactic: set B := (Module.Free.chooseBasis R M).end
Cleared hypotheses: H
-- 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
ι' : 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 : ℕ
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)
g : (i : ι) → MvPolynomial ι' R := toMvPolynomial b' b id
⊢ 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)
have H₁ : Eq (α := MvPolynomial ι' R)
  ((bind₁ g : (a : MvPolynomial ι R) → 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)
  ((bind₁ g : (a : MvPolynomial ι R) → MvPolynomial ι' R) 0 : MvPolynomial ι' R)
Tactic: apply_fun (MvPolynomial.bind₁ g) at H
Cleared hypotheses: H