awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (goal)
Goal:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
ι₁ : Type u_4
ι₂ : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module R M₁
inst_4 : Module R M₂
inst_5 : Fintype ι₁
inst_6 : Finite ι₂
inst_7 : DecidableEq ι₁
b₁ : Basis ι₁ R M₁
b₂ : Basis ι₂ R M₂
f : M₁ →ₗ[R] M₂
i : ι₂
c : ι₁ →₀ R
⊢ Eq.{u_1 + 1} (α := R) ((eval (⇑c : (a : ι₁) → R) : (a : MvPolynomial ι₁ R) → R) (toMvPolynomial b₁ b₂ f i) : R)
    ((((b₂.repr : (a : M₂) → ι₂ →₀ R) ((f : (a : M₁) → M₂) ((b₁.repr.symm : (a : ι₁ →₀ R) → M₁) c : M₁)) : ι₂ →₀ R) :
          (a : ι₂) → R)
        i :
      R)
have rw : Eq.{u_1 + 1} (α := R)
  ((eval (⇑c : (a : ι₁) → R) : (a : MvPolynomial ι₁ R) → R)
      (Matrix.toMvPolynomial ((toMatrix b₁ b₂ : (a : M₁ →ₗ[R] M₂) → Matrix ι₂ ι₁ R) f) i) :
    R)
  ((((b₂.repr : (a : M₂) → ι₂ →₀ R) ((f : (a : M₁) → M₂) ((b₁.repr.symm : (a : ι₁ →₀ R) → M₁) c : M₁)) : ι₂ →₀ R) :
        (a : ι₂) → R)
      i :
    R)
Tactic: rw [toMvPolynomial, Matrix.toMvPolynomial_eval_eq_apply,
    ← LinearMap.toMatrix_mulVec_repr b₁ b₂, LinearEquiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (goal)
Goal:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
ι₁ : Type u_4
ι₂ : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module R M₁
inst_4 : Module R M₂
inst_5 : Fintype ι₁
inst_6 : Finite ι₂
inst_7 : DecidableEq ι₁
b₁ : Basis ι₁ R M₁
b₂ : Basis ι₂ R M₂
f : M₁ →ₗ[R] M₂
i : ι₂
c : ι₁ →₀ R
rw :
  Eq.{u_1 + 1} (α := R)
    ((eval (⇑c : (a : ι₁) → R) : (a : MvPolynomial ι₁ R) → R)
        (Matrix.toMvPolynomial ((toMatrix b₁ b₂ : (a : M₁ →ₗ[R] M₂) → Matrix ι₂ ι₁ R) f) i) :
      R)
    ((((b₂.repr : (a : M₂) → ι₂ →₀ R) ((f : (a : M₁) → M₂) ((b₁.repr.symm : (a : ι₁ →₀ R) → M₁) c : M₁)) : ι₂ →₀ R) :
          (a : ι₂) → R)
        i :
      R)
⊢ Eq.{u_1 + 1} (α := R) ((eval (⇑c : (a : ι₁) → R) : (a : MvPolynomial ι₁ R) → R) (toMvPolynomial b₁ b₂ f i) : R)
    ((((b₂.repr : (a : M₂) → ι₂ →₀ R) ((f : (a : M₁) → M₂) ((b₁.repr.symm : (a : ι₁ →₀ R) → M₁) c : M₁)) : ι₂ →₀ R) :
          (a : ι₂) → R)
        i :
      R)
have rw₁ : Eq.{u_1 + 1} (α := R)
  (Matrix.mulVec.{u_1, u_5, u_4} (n := ι₁) ((toMatrix b₁ b₂ : (a : M₁ →ₗ[R] M₂) → Matrix ι₂ ι₁ R) f) (⇑c : (a : ι₁) → R)
      i :
    R)
  ((((b₂.repr : (a : M₂) → ι₂ →₀ R) ((f : (a : M₁) → M₂) ((b₁.repr.symm : (a : ι₁ →₀ R) → M₁) c : M₁)) : ι₂ →₀ R) :
        (a : ι₂) → R)
      i :
    R)
Tactic: rw [toMvPolynomial, Matrix.toMvPolynomial_eval_eq_apply,
    ← LinearMap.toMatrix_mulVec_repr b₁ b₂, LinearEquiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (goal)
Goal:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
ι₁ : Type u_4
ι₂ : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module R M₁
inst_4 : Module R M₂
inst_5 : Fintype ι₁
inst_6 : Finite ι₂
inst_7 : DecidableEq ι₁
b₁ : Basis ι₁ R M₁
b₂ : Basis ι₂ R M₂
f : M₁ →ₗ[R] M₂
i : ι₂
c : ι₁ →₀ R
rw :
  Eq.{u_1 + 1} (α := R)
    ((eval (⇑c : (a : ι₁) → R) : (a : MvPolynomial ι₁ R) → R)
        (Matrix.toMvPolynomial ((toMatrix b₁ b₂ : (a : M₁ →ₗ[R] M₂) → Matrix ι₂ ι₁ R) f) i) :
      R)
    ((((b₂.repr : (a : M₂) → ι₂ →₀ R) ((f : (a : M₁) → M₂) ((b₁.repr.symm : (a : ι₁ →₀ R) → M₁) c : M₁)) : ι₂ →₀ R) :
          (a : ι₂) → R)
        i :
      R)
rw₁ :
  Eq.{u_1 + 1} (α := R)
    (Matrix.mulVec.{u_1, u_5, u_4} (n := ι₁) ((toMatrix b₁ b₂ : (a : M₁ →ₗ[R] M₂) → Matrix ι₂ ι₁ R) f)
        (⇑c : (a : ι₁) → R) i :
      R)
    ((((b₂.repr : (a : M₂) → ι₂ →₀ R) ((f : (a : M₁) → M₂) ((b₁.repr.symm : (a : ι₁ →₀ R) → M₁) c : M₁)) : ι₂ →₀ R) :
          (a : ι₂) → R)
        i :
      R)
⊢ Eq.{u_1 + 1} (α := R) ((eval (⇑c : (a : ι₁) → R) : (a : MvPolynomial ι₁ R) → R) (toMvPolynomial b₁ b₂ f i) : R)
    ((((b₂.repr : (a : M₂) → ι₂ →₀ R) ((f : (a : M₁) → M₂) ((b₁.repr.symm : (a : ι₁ →₀ R) → M₁) c : M₁)) : ι₂ →₀ R) :
          (a : ι₂) → R)
        i :
      R)
have rw₂ : Eq.{u_1 + 1} (α := R)
  (Matrix.mulVec.{u_1, u_5, u_4} (n := ι₁) ((toMatrix b₁ b₂ : (a : M₁ →ₗ[R] M₂) → Matrix ι₂ ι₁ R) f) (⇑c : (a : ι₁) → R)
    i)
  (Matrix.mulVec.{u_1, u_5, u_4} (n := ι₁) ((toMatrix b₁ b₂ : (a : M₁ →ₗ[R] M₂) → Matrix ι₂ ι₁ R) f)
    (⇑((b₁.repr : (a : M₁) → ι₁ →₀ R) ((b₁.repr.symm : (a : ι₁ →₀ R) → M₁) c) : ι₁ →₀ R) : (a : ι₁) → R) i)
Tactic: rw [toMvPolynomial, Matrix.toMvPolynomial_eval_eq_apply,
    ← LinearMap.toMatrix_mulVec_repr b₁ b₂, LinearEquiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (goal)
Goal:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
ι₁ : Type u_4
ι₂ : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module R M₁
inst_4 : Module R M₂
inst_5 : Fintype ι₁
inst_6 : Finite ι₂
inst_7 : DecidableEq ι₁
b₁ : Basis ι₁ R M₁
b₂ : Basis ι₂ R M₂
f : M₁ →ₗ[R] M₂
i : ι₂
c : ι₁ →₀ R
rw :
  Eq.{u_1 + 1} (α := R)
    ((eval (⇑c : (a : ι₁) → R) : (a : MvPolynomial ι₁ R) → R)
        (Matrix.toMvPolynomial ((toMatrix b₁ b₂ : (a : M₁ →ₗ[R] M₂) → Matrix ι₂ ι₁ R) f) i) :
      R)
    ((((b₂.repr : (a : M₂) → ι₂ →₀ R) ((f : (a : M₁) → M₂) ((b₁.repr.symm : (a : ι₁ →₀ R) → M₁) c : M₁)) : ι₂ →₀ R) :
          (a : ι₂) → R)
        i :
      R)
rw₁ :
  Eq.{u_1 + 1} (α := R)
    (Matrix.mulVec.{u_1, u_5, u_4} (n := ι₁) ((toMatrix b₁ b₂ : (a : M₁ →ₗ[R] M₂) → Matrix ι₂ ι₁ R) f)
        (⇑c : (a : ι₁) → R) i :
      R)
    ((((b₂.repr : (a : M₂) → ι₂ →₀ R) ((f : (a : M₁) → M₂) ((b₁.repr.symm : (a : ι₁ →₀ R) → M₁) c : M₁)) : ι₂ →₀ R) :
          (a : ι₂) → R)
        i :
      R)
rw₂ :
  Eq.{u_1 + 1} (α := R)
    (Matrix.mulVec.{u_1, u_5, u_4} (n := ι₁) ((toMatrix b₁ b₂ : (a : M₁ →ₗ[R] M₂) → Matrix ι₂ ι₁ R) f)
      (⇑c : (a : ι₁) → R) i)
    (Matrix.mulVec.{u_1, u_5, u_4} (n := ι₁) ((toMatrix b₁ b₂ : (a : M₁ →ₗ[R] M₂) → Matrix ι₂ ι₁ R) f)
      (⇑((b₁.repr : (a : M₁) → ι₁ →₀ R) ((b₁.repr.symm : (a : ι₁ →₀ R) → M₁) c) : ι₁ →₀ R) : (a : ι₁) → R) i)
⊢ Eq.{u_1 + 1} (α := R) ((eval (⇑c : (a : ι₁) → R) : (a : MvPolynomial ι₁ R) → R) (toMvPolynomial b₁ b₂ f i) : R)
    ((((b₂.repr : (a : M₂) → ι₂ →₀ R) ((f : (a : M₁) → M₂) ((b₁.repr.symm : (a : ι₁ →₀ R) → M₁) c : M₁)) : ι₂ →₀ R) :
          (a : ι₂) → R)
        i :
      R)
have rw₃ : Eq.{u_1 + 1} (α := R)
  (Matrix.mulVec.{u_1, u_5, u_4} (n := ι₁) ((toMatrix b₁ b₂ : (a : M₁ →ₗ[R] M₂) → Matrix ι₂ ι₁ R) f) (⇑c : (a : ι₁) → R)
    i)
  (Matrix.mulVec.{u_1, u_5, u_4} (n := ι₁) ((toMatrix b₁ b₂ : (a : M₁ →ₗ[R] M₂) → Matrix ι₂ ι₁ R) f) (⇑c : (a : ι₁) → R)
    i)
Tactic: rw [toMvPolynomial, Matrix.toMvPolynomial_eval_eq_apply,
    ← LinearMap.toMatrix_mulVec_repr b₁ b₂, LinearEquiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (goal)
Goal:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
ι₁ : Type u_4
ι₂ : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module R M₁
inst_4 : Module R M₂
inst_5 : Fintype ι₁
inst_6 : Finite ι₂
inst_7 : DecidableEq ι₁
b₁ : Basis ι₁ R M₁
b₂ : Basis ι₂ R M₂
f g : M₁ →ₗ[R] M₂
⊢ toMvPolynomial b₁ b₂ (f + g) = toMvPolynomial b₁ b₂ f + toMvPolynomial b₁ b₂ g
have unfold : (fun (i : ι₂) ↦ Matrix.toMvPolynomial ((toMatrix b₁ b₂ : (a : M₁ →ₗ[R] M₂) → Matrix ι₂ ι₁ R) (f + g)) i) =
  HAdd.hAdd (α := (i : ι₂) → MvPolynomial ι₁ R)
    (fun (i : ι₂) ↦ Matrix.toMvPolynomial ((toMatrix b₁ b₂ : (a : M₁ →ₗ[R] M₂) → Matrix ι₂ ι₁ R) f) i) fun (i : ι₂) ↦
    Matrix.toMvPolynomial ((toMatrix b₁ b₂ : (a : M₁ →ₗ[R] M₂) → Matrix ι₂ ι₁ R) g) i
Tactic: unfold toMvPolynomial
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (goal)
Goal:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
ι₁ : Type u_5
ι₂ : Type u_6
ι₃ : Type u_7
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup M₃
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M₃
inst_7 : Fintype ι₁
inst_8 : Fintype ι₂
inst_9 : Finite ι₃
inst_10 : DecidableEq ι₁
inst_11 : DecidableEq ι₂
b₁ : Basis ι₁ R M₁
b₂ : Basis ι₂ R M₂
b₃ : Basis ι₃ R M₃
g : M₂ →ₗ[R] M₃
f : M₁ →ₗ[R] M₂
i : ι₃
⊢ toMvPolynomial b₁ b₃ (g ∘ₗ f) i =
    (bind₁ (toMvPolynomial b₁ b₂ f) : (a : MvPolynomial ι₂ R) → MvPolynomial ι₁ R) (toMvPolynomial b₂ b₃ g i)
have simp : Eq (α := MvPolynomial ι₁ R)
  ((bind₁ (Matrix.toMvPolynomial ((toMatrix b₁ b₂ : (a : M₁ →ₗ[R] M₂) → Matrix ι₂ ι₁ R) f)) :
        (a : MvPolynomial ι₂ R) → MvPolynomial ι₁ R)
      (Matrix.toMvPolynomial ((toMatrix b₂ b₃ : (a : M₂ →ₗ[R] M₃) → Matrix ι₃ ι₂ R) g) i) :
    MvPolynomial ι₁ R)
  ((bind₁ (toMvPolynomial b₁ b₂ f) : (a : MvPolynomial ι₂ R) → MvPolynomial ι₁ R)
      (Matrix.toMvPolynomial ((toMatrix b₂ b₃ : (a : M₂ →ₗ[R] M₃) → Matrix ι₃ ι₂ R) g) i) :
    MvPolynomial ι₁ R)
Tactic: simp only [toMvPolynomial, toMatrix_comp b₁ b₂ b₃, Matrix.toMvPolynomial_mul]
-- 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 : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
A : Type u_8
inst_9 : CommRing A
inst_10 : Algebra R A
⊢ Polynomial.map
      (↑(bind₁
            (toMvPolynomial (M₁ := TensorProduct R A L) (M₂ := End A (TensorProduct R A M)) (basis A b)
              (Basis.end (basis A bₘ)) (tensorProduct R A M M ∘ₗ baseChange A φ))) :
        MvPolynomial (ιM × ιM) A →+* MvPolynomial ι A)
      (charpoly.univ A ιM) =
    Polynomial.map (MvPolynomial.map (algebraMap R A))
      (Polynomial.map (↑(bind₁ (toMvPolynomial b bₘ.end φ)) : MvPolynomial (ιM × ιM) R →+* MvPolynomial ι R)
        (charpoly.univ R ιM))
have rw : Polynomial.map
    (↑(bind₁
          (toMvPolynomial (M₁ := TensorProduct R A L) (M₂ := End A (TensorProduct R A M)) (basis A b)
            (Basis.end (basis A bₘ)) (tensorProduct R A M M ∘ₗ baseChange A φ))) :
      MvPolynomial (ιM × ιM) A →+* MvPolynomial ι A)
    (Polynomial.map (R := MvPolynomial.{u_7, u_1} (ιM × ιM) R) (MvPolynomial.map (algebraMap R A))
      (charpoly.univ R ιM)) =
  Polynomial.map (MvPolynomial.map (algebraMap R A))
    (Polynomial.map (↑(bind₁ (toMvPolynomial b bₘ.end φ)) : MvPolynomial (ιM × ιM) R →+* MvPolynomial ι R)
      (charpoly.univ R ιM))
Tactic: rw [← charpoly.univ_map_map _ (algebraMap R A)]
-- 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 : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
A : Type u_8
inst_9 : CommRing A
inst_10 : Algebra R A
⊢ Polynomial.map
      (↑(bind₁
            (toMvPolynomial (M₁ := TensorProduct R A L) (M₂ := End A (TensorProduct R A M)) (basis A b)
              (Basis.end (basis A bₘ)) (tensorProduct R A M M ∘ₗ baseChange A φ))) :
        MvPolynomial (ιM × ιM) A →+* MvPolynomial ι A)
      (Polynomial.map (R := MvPolynomial.{u_7, u_1} (ιM × ιM) R) (MvPolynomial.map (algebraMap R A))
        (charpoly.univ R ιM)) =
    Polynomial.map (MvPolynomial.map (algebraMap R A))
      (Polynomial.map (↑(bind₁ (toMvPolynomial b bₘ.end φ)) : MvPolynomial (ιM × ιM) R →+* MvPolynomial ι R)
        (charpoly.univ R ιM))
have simp : Polynomial.map (R := MvPolynomial.{u_7, u_1} (ιM × ιM) R)
    (RingHom.comp
      (↑(bind₁
            (toMvPolynomial (M₁ := TensorProduct R A L) (M₂ := End A (TensorProduct R A M)) (basis A b)
              (Basis.end (basis A bₘ)) (tensorProduct R A M M ∘ₗ baseChange A φ))) :
        MvPolynomial (ιM × ιM) A →+* MvPolynomial ι A)
      (MvPolynomial.map (algebraMap R A)))
    (charpoly.univ R ιM) =
  Polynomial.map
    (RingHom.comp (MvPolynomial.map (algebraMap R A))
      (↑(bind₁ (toMvPolynomial b bₘ.end φ)) : MvPolynomial (ιM × ιM) R →+* MvPolynomial ι R))
    (charpoly.univ R ιM)
Tactic: simp only [Polynomial.map_map]
-- 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 : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
A : Type u_8
inst_9 : CommRing A
inst_10 : Algebra R A
⊢ Polynomial.map (R := MvPolynomial.{u_7, u_1} (ιM × ιM) R)
      (RingHom.comp
        (↑(bind₁
              (toMvPolynomial (M₁ := TensorProduct R A L) (M₂ := End A (TensorProduct R A M)) (basis A b)
                (Basis.end (basis A bₘ)) (tensorProduct R A M M ∘ₗ baseChange A φ))) :
          MvPolynomial (ιM × ιM) A →+* MvPolynomial ι A)
        (MvPolynomial.map (algebraMap R A)))
      (charpoly.univ R ιM) =
    Polynomial.map
      (RingHom.comp (MvPolynomial.map (algebraMap R A))
        (↑(bind₁ (toMvPolynomial b bₘ.end φ)) : MvPolynomial (ιM × ιM) R →+* MvPolynomial ι R))
      (charpoly.univ R ιM)
have e_f : RingHom.comp
    (↑(bind₁
          (toMvPolynomial (M₁ := TensorProduct R A L) (M₂ := End A (TensorProduct R A M)) (basis A b)
            (Basis.end (basis A bₘ)) (tensorProduct R A M M ∘ₗ baseChange A φ))) :
      MvPolynomial (ιM × ιM) A →+* MvPolynomial ι A)
    (MvPolynomial.map (algebraMap R A)) =
  RingHom.comp (MvPolynomial.map (algebraMap R A))
    (↑(bind₁ (toMvPolynomial b bₘ.end φ)) : MvPolynomial (ιM × ιM) R →+* MvPolynomial ι R)
Tactic: congr 1
-- 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 : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
A : Type u_8
inst_9 : CommRing A
inst_10 : Algebra R A
⊢ RingHom.comp
      (↑(bind₁
            (toMvPolynomial (M₁ := TensorProduct R A L) (M₂ := End A (TensorProduct R A M)) (basis A b)
              (Basis.end (basis A bₘ)) (tensorProduct R A M M ∘ₗ baseChange A φ))) :
        MvPolynomial (ιM × ιM) A →+* MvPolynomial ι A)
      (MvPolynomial.map (algebraMap R A)) =
    RingHom.comp (MvPolynomial.map (algebraMap R A))
      (↑(bind₁ (toMvPolynomial b bₘ.end φ)) : MvPolynomial (ιM × ιM) R →+* MvPolynomial ι R)
have e_f : ∀ (r : R),
  Eq (α := MvPolynomial ι A)
    ((RingHom.comp
            (↑(bind₁
                  (toMvPolynomial (M₁ := TensorProduct R A L) (M₂ := End A (TensorProduct R A M)) (basis A b)
                    (Basis.end (basis A bₘ)) (tensorProduct R A M M ∘ₗ baseChange A φ))) :
              MvPolynomial (ιM × ιM) A →+* MvPolynomial ι A)
            (MvPolynomial.map (algebraMap R A)) :
          (a : MvPolynomial (ιM × ιM) R) → MvPolynomial ι A)
        ((C : (a : R) → MvPolynomial (ιM × ιM) R) r) :
      MvPolynomial ι A)
    ((RingHom.comp (MvPolynomial.map (algebraMap R A))
            (↑(bind₁ (toMvPolynomial b bₘ.end φ)) : MvPolynomial (ιM × ιM) R →+* MvPolynomial ι R) :
          (a : MvPolynomial (ιM × ιM) R) → MvPolynomial ι A)
        ((C : (a : R) → MvPolynomial (ιM × ιM) R) r) :
      MvPolynomial ι A)
Tactic: apply MvPolynomial.ringHom_ext
-- 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 : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
A : Type u_8
inst_9 : CommRing A
inst_10 : Algebra R A
e_f :
  ∀ (r : R),
    Eq (α := MvPolynomial ι A)
      ((RingHom.comp
              (↑(bind₁
                    (toMvPolynomial (M₁ := TensorProduct R A L) (M₂ := End A (TensorProduct R A M)) (basis A b)
                      (Basis.end (basis A bₘ)) (tensorProduct R A M M ∘ₗ baseChange A φ))) :
                MvPolynomial (ιM × ιM) A →+* MvPolynomial ι A)
              (MvPolynomial.map (algebraMap R A)) :
            (a : MvPolynomial (ιM × ιM) R) → MvPolynomial ι A)
          ((C : (a : R) → MvPolynomial (ιM × ιM) R) r) :
        MvPolynomial ι A)
      ((RingHom.comp (MvPolynomial.map (algebraMap R A))
              (↑(bind₁ (toMvPolynomial b bₘ.end φ)) : MvPolynomial (ιM × ιM) R →+* MvPolynomial ι R) :
            (a : MvPolynomial (ιM × ιM) R) → MvPolynomial ι A)
          ((C : (a : R) → MvPolynomial (ιM × ιM) R) r) :
        MvPolynomial ι A)
⊢ RingHom.comp
      (↑(bind₁
            (toMvPolynomial (M₁ := TensorProduct R A L) (M₂ := End A (TensorProduct R A M)) (basis A b)
              (Basis.end (basis A bₘ)) (tensorProduct R A M M ∘ₗ baseChange A φ))) :
        MvPolynomial (ιM × ιM) A →+* MvPolynomial ι A)
      (MvPolynomial.map (algebraMap R A)) =
    RingHom.comp (MvPolynomial.map (algebraMap R A))
      (↑(bind₁ (toMvPolynomial b bₘ.end φ)) : MvPolynomial (ιM × ιM) R →+* MvPolynomial ι R)
have e_f₁ : ∀ (i : ιM × ιM),
  Eq (α := MvPolynomial ι A)
    ((RingHom.comp
            (↑(bind₁
                  (toMvPolynomial (M₁ := TensorProduct R A L) (M₂ := End A (TensorProduct R A M)) (basis A b)
                    (Basis.end (basis A bₘ)) (tensorProduct R A M M ∘ₗ baseChange A φ))) :
              MvPolynomial (ιM × ιM) A →+* MvPolynomial ι A)
            (MvPolynomial.map (algebraMap R A)) :
          (a : MvPolynomial (ιM × ιM) R) → MvPolynomial ι A)
        (X i) :
      MvPolynomial ι A)
    ((RingHom.comp (MvPolynomial.map (algebraMap R A))
            (↑(bind₁ (toMvPolynomial b bₘ.end φ)) : MvPolynomial (ιM × ιM) R →+* MvPolynomial ι R) :
          (a : MvPolynomial (ιM × ιM) R) → MvPolynomial ι A)
        (X i) :
      MvPolynomial ι A)
Tactic: apply MvPolynomial.ringHom_ext
-- 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 : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
A : Type u_8
inst_9 : CommRing A
inst_10 : Algebra R A
ij : ιM × ιM
⊢ Eq (α := MvPolynomial ι A)
    ((RingHom.comp
            (↑(bind₁
                  (toMvPolynomial (M₁ := TensorProduct R A L) (M₂ := End A (TensorProduct R A M)) (basis A b)
                    (Basis.end (basis A bₘ)) (tensorProduct R A M M ∘ₗ baseChange A φ))) :
              MvPolynomial (ιM × ιM) A →+* MvPolynomial ι A)
            (MvPolynomial.map (algebraMap R A)) :
          (a : MvPolynomial (ιM × ιM) R) → MvPolynomial ι A)
        (X ij) :
      MvPolynomial ι A)
    ((RingHom.comp (MvPolynomial.map (algebraMap R A))
            (↑(bind₁ (toMvPolynomial b bₘ.end φ)) : MvPolynomial (ιM × ιM) R →+* MvPolynomial ι R) :
          (a : MvPolynomial (ιM × ιM) R) → MvPolynomial ι A)
        (X ij) :
      MvPolynomial ι A)
have e_f : Eq (α := MvPolynomial ι A)
  (toMvPolynomial (M₁ := TensorProduct R A L) (M₂ := End A (TensorProduct R A M)) (basis A b) (Basis.end (basis A bₘ))
    (tensorProduct R A M M ∘ₗ baseChange A φ) ij)
  ((MvPolynomial.map (algebraMap R A) : (a : MvPolynomial ι R) → MvPolynomial ι A) (toMvPolynomial b bₘ.end φ ij))
Tactic: simp only [RingHom.coe_comp, RingHom.coe_coe, Function.comp_apply, map_X, bind₁_X_right]
-- 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 : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
A : Type u_8
inst_9 : CommRing A
inst_10 : Algebra R A
ij : ιM × ιM
⊢ Eq (α := MvPolynomial ι A)
    (toMvPolynomial (M₁ := TensorProduct R A L) (M₂ := End A (TensorProduct R A M)) (basis A b) (Basis.end (basis A bₘ))
      (tensorProduct R A M M ∘ₗ baseChange A φ) ij)
    ((MvPolynomial.map (algebraMap R A) : (a : MvPolynomial ι R) → MvPolynomial ι A) (toMvPolynomial b bₘ.end φ ij))
have e_f : Eq (α := MvPolynomial ι A)
  ((bind₁
          (toMvPolynomial (M₁ := TensorProduct R A L) (M₂ := TensorProduct.{u_1, u_8, u_3} R A (End R M)) (basis A b)
            (basis A bₘ.end) (baseChange A φ)) :
        (a : MvPolynomial (ιM × ιM) A) → MvPolynomial ι A)
      (toMvPolynomial (M₁ := TensorProduct.{u_1, u_8, u_3} R A (End R M)) (M₂ := End A (TensorProduct R A M))
        (basis A bₘ.end) (Basis.end (basis A bₘ)) (tensorProduct R A M M) ij) :
    MvPolynomial ι A)
  (toMvPolynomial (M₁ := TensorProduct R A L) (M₂ := TensorProduct.{u_1, u_8, u_3} R A (End R M)) (basis A b)
      (basis A bₘ.end) (baseChange A φ) ij :
    MvPolynomial ι A)
Tactic: rw [toMvPolynomial_comp _ (basis A (Basis.end bₘ)), ← toMvPolynomial_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
ι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
A : Type u_8
inst_9 : CommRing A
inst_10 : Algebra R A
ij : ιM × ιM
this :
  Eq (α := MvPolynomial.{u_7, u_8} (ιM × ιM) A)
    (toMvPolynomial (M₁ := TensorProduct.{u_1, u_8, u_3} R A (End R M)) (M₂ := End A (TensorProduct R A M))
      (basis A bₘ.end) (Basis.end (basis A bₘ)) (tensorProduct R A M M) ij)
    (X ij)
⊢ Eq (α := MvPolynomial ι A)
    ((bind₁
            (toMvPolynomial (M₁ := TensorProduct R A L) (M₂ := TensorProduct.{u_1, u_8, u_3} R A (End R M)) (basis A b)
              (basis A bₘ.end) (baseChange A φ)) :
          (a : MvPolynomial (ιM × ιM) A) → MvPolynomial ι A)
        (toMvPolynomial (M₁ := TensorProduct.{u_1, u_8, u_3} R A (End R M)) (M₂ := End A (TensorProduct R A M))
          (basis A bₘ.end) (Basis.end (basis A bₘ)) (tensorProduct R A M M) ij) :
      MvPolynomial ι A)
    (toMvPolynomial (M₁ := TensorProduct R A L) (M₂ := TensorProduct.{u_1, u_8, u_3} R A (End R M)) (basis A b)
        (basis A bₘ.end) (baseChange A φ) ij :
      MvPolynomial ι A)
have rw : Eq (α := MvPolynomial ι A)
  ((bind₁
          (toMvPolynomial (M₁ := TensorProduct R A L) (M₂ := TensorProduct.{u_1, u_8, u_3} R A (End R M)) (basis A b)
            (basis A bₘ.end) (baseChange A φ)) :
        (a : MvPolynomial (ιM × ιM) A) → MvPolynomial ι A)
      (X ij) :
    MvPolynomial ι A)
  (toMvPolynomial (M₁ := TensorProduct R A L) (M₂ := TensorProduct.{u_1, u_8, u_3} R A (End R M)) (basis A b)
      (basis A bₘ.end) (baseChange A φ) ij :
    MvPolynomial ι A)
Tactic: rw [this, bind₁_X_right]