awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
key : f * f.mirror = k * k.mirror
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
h_dvd_k_rev : h ∣ k.mirror
hk : k = -f
⊢ h ∣ f.mirror
have rwa : h ∣ (-k).mirror
Tactic: rwa [← neg_eq_iff_eq_neg.mpr hk, mirror_neg, dvd_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
key : f * f.mirror = k * k.mirror
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
h_dvd_k_rev : h ∣ k.mirror
hk : k = -f
rwa : h ∣ (-k).mirror
⊢ h ∣ f.mirror
have rwa₁ : h ∣ -k.mirror
Tactic: rwa [← neg_eq_iff_eq_neg.mpr hk, mirror_neg, dvd_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
key : f * f.mirror = k * k.mirror
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
h_dvd_k_rev : h ∣ k.mirror
hk : k = -f.mirror
⊢ g ∣ f.mirror
have rwa : g ∣ -k
Tactic: rwa [← neg_eq_iff_eq_neg.mpr hk, dvd_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.AEval (goal)
Goal:
R : Type u_2
A : Type u_3
M : Type u_1
inst : CommSemiring R
inst_1 : Semiring A
a : A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
m : M
⊢ HSMul.hSMul.{u_2, u_1, u_1} (α := R[X]) (β := AEval R M a) X ((of R M a : (a_1 : M) → AEval R M a) m : AEval R M a) =
    (of R M a : (a_1 : M) → AEval R M a) (a • m)
have rw : Eq (α := AEval R M a)
  ((of R M a : (a_1 : M) → AEval R M a) (HSMul.hSMul.{u_3, u_1, u_1} (α := A) ((aeval a : (a : R[X]) → A) X : A) m) :
    AEval R M a)
  ((of R M a : (a_1 : M) → AEval R M a) (a • m) : AEval R M a)
Tactic: rw [← of_aeval_smul, aeval_X]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.AEval (goal)
Goal:
R : Type u_2
A : Type u_3
M : Type u_1
inst : CommSemiring R
inst_1 : Semiring A
a : A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
m : M
rw :
  Eq (α := AEval R M a)
    ((of R M a : (a_1 : M) → AEval R M a) (HSMul.hSMul.{u_3, u_1, u_1} (α := A) ((aeval a : (a : R[X]) → A) X : A) m) :
      AEval R M a)
    ((of R M a : (a_1 : M) → AEval R M a) (a • m) : AEval R M a)
⊢ HSMul.hSMul.{u_2, u_1, u_1} (α := R[X]) (β := AEval R M a) X ((of R M a : (a_1 : M) → AEval R M a) m : AEval R M a) =
    (of R M a : (a_1 : M) → AEval R M a) (a • m)
have rw₁ : Eq (α := AEval R M a) ((of R M a : (a_1 : M) → AEval R M a) (a • m) : AEval R M a)
  ((of R M a : (a_1 : M) → AEval R M a) (a • m) : AEval R M a)
Tactic: rw [← of_aeval_smul, aeval_X]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.AEval (goal)
Goal:
R : Type u_2
A : Type u_3
M : Type u_1
inst : CommSemiring R
inst_1 : Semiring A
a : A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
m : M
n : ℕ
⊢ HSMul.hSMul (β := AEval R M a) (HPow.hPow (α := R[X]) X n) ((of R M a : (a_1 : M) → AEval R M a) m : AEval R M a) =
    (of R M a : (a_1 : M) → AEval R M a) (a ^ n • m)
have rw : Eq (α := AEval R M a)
  ((of R M a : (a_1 : M) → AEval R M a)
      (HSMul.hSMul.{u_3, u_1, u_1} (α := A) ((aeval a : (a : R[X]) → A) (HPow.hPow (α := R[X]) X n) : A) m) :
    AEval R M a)
  ((of R M a : (a_1 : M) → AEval R M a) (a ^ n • m) : AEval R M a)
Tactic: rw [← of_aeval_smul, aeval_X_pow]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.AEval (goal)
Goal:
R : Type u_2
A : Type u_3
M : Type u_1
inst : CommSemiring R
inst_1 : Semiring A
a : A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
m : M
n : ℕ
rw :
  Eq (α := AEval R M a)
    ((of R M a : (a_1 : M) → AEval R M a)
        (HSMul.hSMul.{u_3, u_1, u_1} (α := A) ((aeval a : (a : R[X]) → A) (HPow.hPow (α := R[X]) X n) : A) m) :
      AEval R M a)
    ((of R M a : (a_1 : M) → AEval R M a) (a ^ n • m) : AEval R M a)
⊢ HSMul.hSMul (β := AEval R M a) (HPow.hPow (α := R[X]) X n) ((of R M a : (a_1 : M) → AEval R M a) m : AEval R M a) =
    (of R M a : (a_1 : M) → AEval R M a) (a ^ n • m)
have rw₁ : Eq (α := AEval R M a) ((of R M a : (a_1 : M) → AEval R M a) (a ^ n • m) : AEval R M a)
  ((of R M a : (a_1 : M) → AEval R M a) (a ^ n • m) : AEval R M a)
Tactic: rw [← of_aeval_smul, aeval_X_pow]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.AEval (goal)
Goal:
R : Type u_1
A : Type u_3
M : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
a : A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
m : AEval R M a
⊢ (LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) (HSMul.hSMul.{u_1, u_2, u_2} (α := R[X]) X m) =
    HSMul.hSMul (β := M) a ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) m : M)
have rw : HSMul.hSMul.{u_3, u_2, u_2} (α := A) (β := M) ((aeval a : (a : R[X]) → A) X : A)
    ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) m : M) =
  HSMul.hSMul (β := M) a ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) m : M)
Tactic: rw [of_symm_smul, aeval_X]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.AEval (goal)
Goal:
R : Type u_1
A : Type u_3
M : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
a : A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
m : AEval R M a
rw :
  HSMul.hSMul.{u_3, u_2, u_2} (α := A) (β := M) ((aeval a : (a : R[X]) → A) X : A)
      ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) m : M) =
    HSMul.hSMul (β := M) a ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) m : M)
⊢ (LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) (HSMul.hSMul.{u_1, u_2, u_2} (α := R[X]) X m) =
    HSMul.hSMul (β := M) a ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) m : M)
have rw₁ : HSMul.hSMul (β := M) a ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) m : M) =
  HSMul.hSMul (β := M) a ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) m : M)
Tactic: rw [of_symm_smul, aeval_X]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.AEval (goal)
Goal:
R : Type u_1
A : Type u_3
M : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
a : A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
r : R
f : R[X]
m : AEval R M a
⊢ (r • f) • m = r • f • m
have a₁ : Eq (α := M) ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) ((r • f) • m) : M)
  ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) (r • f • m) : M)
Tactic: apply (of R M a).symm.injective
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.AEval (goal)
Goal:
R : Type u_1
A : Type u_3
M : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
a : A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
r : R
f : R[X]
m : AEval R M a
⊢ Eq (α := M) ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) ((r • f) • m) : M)
    ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) (r • f • m) : M)
have a₁ : HSMul.hSMul.{u_3, u_2, u_2} (α := A) (β := M) ((aeval a : (a : R[X]) → A) (r • f) : A)
    ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) m : M) =
  (LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) (r • f • m)
Tactic: rw [of_symm_smul, map_smul, smul_assoc, map_smul, of_symm_smul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.AEval (goal)
Goal:
R : Type u_1
A : Type u_3
M : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
a : A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
r : R
f : R[X]
m : AEval R M a
a₁ :
  HSMul.hSMul.{u_3, u_2, u_2} (α := A) (β := M) ((aeval a : (a : R[X]) → A) (r • f) : A)
      ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) m : M) =
    (LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) (r • f • m)
⊢ Eq (α := M) ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) ((r • f) • m) : M)
    ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) (r • f • m) : M)
have a₂ : HSMul.hSMul (β := M) (HSMul.hSMul (β := A) r ((aeval a : (a : R[X]) → A) f : A))
    ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) m : M) =
  (LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) (r • f • m)
Tactic: rw [of_symm_smul, map_smul, smul_assoc, map_smul, of_symm_smul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.AEval (goal)
Goal:
R : Type u_1
A : Type u_3
M : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
a : A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
r : R
f : R[X]
m : AEval R M a
a₁ :
  HSMul.hSMul.{u_3, u_2, u_2} (α := A) (β := M) ((aeval a : (a : R[X]) → A) (r • f) : A)
      ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) m : M) =
    (LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) (r • f • m)
a₂ :
  HSMul.hSMul (β := M) (HSMul.hSMul (β := A) r ((aeval a : (a : R[X]) → A) f : A))
      ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) m : M) =
    (LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) (r • f • m)
⊢ Eq (α := M) ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) ((r • f) • m) : M)
    ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) (r • f • m) : M)
have a₃ : r •
    HSMul.hSMul.{u_3, u_2, u_2} (α := A) (β := M) ((aeval a : (a : R[X]) → A) f : A)
      ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) m : M) =
  (LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) (r • f • m)
Tactic: rw [of_symm_smul, map_smul, smul_assoc, map_smul, of_symm_smul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.AEval (goal)
Goal:
R : Type u_1
A : Type u_3
M : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
a : A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
r : R
f : R[X]
m : AEval R M a
a₁ :
  HSMul.hSMul.{u_3, u_2, u_2} (α := A) (β := M) ((aeval a : (a : R[X]) → A) (r • f) : A)
      ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) m : M) =
    (LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) (r • f • m)
a₂ :
  HSMul.hSMul (β := M) (HSMul.hSMul (β := A) r ((aeval a : (a : R[X]) → A) f : A))
      ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) m : M) =
    (LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) (r • f • m)
a₃ :
  r •
      HSMul.hSMul.{u_3, u_2, u_2} (α := A) (β := M) ((aeval a : (a : R[X]) → A) f : A)
        ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) m : M) =
    (LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) (r • f • m)
⊢ Eq (α := M) ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) ((r • f) • m) : M)
    ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) (r • f • m) : M)
have a₄ : r •
    HSMul.hSMul.{u_3, u_2, u_2} (α := A) (β := M) ((aeval a : (a : R[X]) → A) f : A)
      ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) m : M) =
  HSMul.hSMul (β := M) r ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) (f • m) : M)
Tactic: rw [of_symm_smul, map_smul, smul_assoc, map_smul, of_symm_smul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.AEval (goal)
Goal:
R : Type u_1
A : Type u_3
M : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
a : A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
r : R
f : R[X]
m : AEval R M a
a₁ :
  HSMul.hSMul.{u_3, u_2, u_2} (α := A) (β := M) ((aeval a : (a : R[X]) → A) (r • f) : A)
      ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) m : M) =
    (LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) (r • f • m)
a₂ :
  HSMul.hSMul (β := M) (HSMul.hSMul (β := A) r ((aeval a : (a : R[X]) → A) f : A))
      ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) m : M) =
    (LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) (r • f • m)
a₃ :
  r •
      HSMul.hSMul.{u_3, u_2, u_2} (α := A) (β := M) ((aeval a : (a : R[X]) → A) f : A)
        ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) m : M) =
    (LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) (r • f • m)
a₄ :
  r •
      HSMul.hSMul.{u_3, u_2, u_2} (α := A) (β := M) ((aeval a : (a : R[X]) → A) f : A)
        ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) m : M) =
    HSMul.hSMul (β := M) r ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) (f • m) : M)
⊢ Eq (α := M) ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) ((r • f) • m) : M)
    ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) (r • f • m) : M)
have a₅ : r •
    HSMul.hSMul.{u_3, u_2, u_2} (α := A) (β := M) ((aeval a : (a : R[X]) → A) f : A)
      ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) m : M) =
  r •
    HSMul.hSMul.{u_3, u_2, u_2} (α := A) (β := M) ((aeval a : (a : R[X]) → A) f : A)
      ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) m : M)
Tactic: rw [of_symm_smul, map_smul, smul_assoc, map_smul, of_symm_smul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.AEval (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
a : A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
N : Type u_4
inst_7 : AddCommMonoid N
inst_8 : Module R N
inst_9 : Module.{u_1, u_4} R[X] N
inst_10 : IsScalarTower R R[X] N
f : M →ₗ[R] N
hf : ∀ (m : M), (f : (a : M) → N) (a • m) = HSMul.hSMul.{u_1, u_4, u_4} (α := R[X]) (β := N) X ((f : (a : M) → N) m : N)
p : R[X]
n : ℕ
k : R
h :
  ∀ (x : AEval R M a),
    AddHom.toFun (LinearMap.toAddHom (f ∘ₗ (↑(LinearEquiv.symm (of R M a)) : AEval R M a →ₗ[R] M)))
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) k : R[X]) (HPow.hPow (α := R[X]) X n) • x) =
      HSMul.hSMul (α := R[X])
        ((RingHom.id R[X] : (a : R[X]) → R[X])
            (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) k : R[X]) (HPow.hPow (α := R[X]) X n)) :
          R[X])
        (AddHom.toFun (LinearMap.toAddHom (f ∘ₗ (↑(LinearEquiv.symm (of R M a)) : AEval R M a →ₗ[R] M))) x)
m : AEval R M a
⊢ AddHom.toFun (LinearMap.toAddHom (f ∘ₗ (↑(LinearEquiv.symm (of R M a)) : AEval R M a →ₗ[R] M)))
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) k : R[X]) (HPow.hPow (α := R[X]) X (n + 1)) • m) =
    HSMul.hSMul (α := R[X])
      ((RingHom.id R[X] : (a : R[X]) → R[X])
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) k : R[X]) (HPow.hPow (α := R[X]) X (n + 1))) :
        R[X])
      (AddHom.toFun (LinearMap.toAddHom (f ∘ₗ (↑(LinearEquiv.symm (of R M a)) : AEval R M a →ₗ[R] M))) m)
have simp_rw : (f : (a : M) → N)
    ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M)
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) k : R[X]) (HPow.hPow (α := R[X]) X (n + 1)) • m) :
      M) =
  HSMul.hSMul (β := N) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) k : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))
    ((f : (a : M) → N) ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) m : M) : N)
Tactic: simp_rw [RingHom.id_apply, AddHom.toFun_eq_coe, LinearMap.coe_toAddHom,
        LinearMap.comp_apply, LinearEquiv.coe_toLinearMap] at h ⊢
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.AEval (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
a : A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
N : Type u_4
inst_7 : AddCommMonoid N
inst_8 : Module R N
inst_9 : Module.{u_1, u_4} R[X] N
inst_10 : IsScalarTower R R[X] N
f : M →ₗ[R] N
hf : ∀ (m : M), (f : (a : M) → N) (a • m) = HSMul.hSMul.{u_1, u_4, u_4} (α := R[X]) (β := N) X ((f : (a : M) → N) m : N)
p : R[X]
n : ℕ
k : R
h :
  ∀ (x : AEval R M a),
    (f : (a : M) → N)
        ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M)
            (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) k : R[X]) (HPow.hPow (α := R[X]) X n) • x) :
          M) =
      HSMul.hSMul (β := N) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) k : R[X]) (HPow.hPow (α := R[X]) X n))
        ((f : (a : M) → N) ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) x : M) : N)
m : AEval R M a
⊢ (f : (a : M) → N)
      ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M)
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) k : R[X]) (HPow.hPow (α := R[X]) X (n + 1)) • m) :
        M) =
    HSMul.hSMul (β := N) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) k : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))
      ((f : (a : M) → N) ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) m : M) : N)
have simp_rw : (f : (a : M) → N)
    ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M)
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) k : R[X]) (HPow.hPow (α := R[X]) X n * X) • m) :
      M) =
  HSMul.hSMul (β := N) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) k : R[X]) (HPow.hPow (α := R[X]) X n * X))
    ((f : (a : M) → N) ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) m : M) : N)
Tactic: simp_rw [pow_succ, ← mul_assoc, mul_smul _ X, ← hf, ← of_symm_X_smul, ← h]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.AEval (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
a : A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
N : Type u_4
inst_7 : AddCommMonoid N
inst_8 : Module R N
inst_9 : Module.{u_1, u_4} R[X] N
inst_10 : IsScalarTower R R[X] N
f : M →ₗ[R] N
hf : ∀ (m : M), (f : (a : M) → N) (a • m) = HSMul.hSMul.{u_1, u_4, u_4} (α := R[X]) (β := N) X ((f : (a : M) → N) m : N)
p : R[X]
n : ℕ
k : R
h :
  ∀ (x : AEval R M a),
    (f : (a : M) → N)
        ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M)
            (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) k : R[X]) (HPow.hPow (α := R[X]) X n) • x) :
          M) =
      HSMul.hSMul (β := N) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) k : R[X]) (HPow.hPow (α := R[X]) X n))
        ((f : (a : M) → N) ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) x : M) : N)
m : AEval R M a
simp_rw :
  (f : (a : M) → N)
      ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M)
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) k : R[X]) (HPow.hPow (α := R[X]) X n * X) • m) :
        M) =
    HSMul.hSMul (β := N) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) k : R[X]) (HPow.hPow (α := R[X]) X n * X))
      ((f : (a : M) → N) ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) m : M) : N)
⊢ (f : (a : M) → N)
      ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M)
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) k : R[X]) (HPow.hPow (α := R[X]) X (n + 1)) • m) :
        M) =
    HSMul.hSMul (β := N) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) k : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))
      ((f : (a : M) → N) ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) m : M) : N)
have simp_rw₁ : (f : (a : M) → N)
    ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M)
        ((HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) k : R[X]) (HPow.hPow (α := R[X]) X n) * X) • m) :
      M) =
  HSMul.hSMul (β := N) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) k : R[X]) (HPow.hPow (α := R[X]) X n) * X)
    ((f : (a : M) → N) ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) m : M) : N)
Tactic: simp_rw [pow_succ, ← mul_assoc, mul_smul _ X, ← hf, ← of_symm_X_smul, ← h]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.AEval (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
a : A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
N : Type u_4
inst_7 : AddCommMonoid N
inst_8 : Module R N
inst_9 : Module.{u_1, u_4} R[X] N
inst_10 : IsScalarTower R R[X] N
f : M →ₗ[R] N
hf : ∀ (m : M), (f : (a : M) → N) (a • m) = HSMul.hSMul.{u_1, u_4, u_4} (α := R[X]) (β := N) X ((f : (a : M) → N) m : N)
p : R[X]
n : ℕ
k : R
h :
  ∀ (x : AEval R M a),
    (f : (a : M) → N)
        ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M)
            (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) k : R[X]) (HPow.hPow (α := R[X]) X n) • x) :
          M) =
      HSMul.hSMul (β := N) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) k : R[X]) (HPow.hPow (α := R[X]) X n))
        ((f : (a : M) → N) ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) x : M) : N)
m : AEval R M a
simp_rw :
  (f : (a : M) → N)
      ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M)
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) k : R[X]) (HPow.hPow (α := R[X]) X n * X) • m) :
        M) =
    HSMul.hSMul (β := N) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) k : R[X]) (HPow.hPow (α := R[X]) X n * X))
      ((f : (a : M) → N) ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) m : M) : N)
simp_rw₁ :
  (f : (a : M) → N)
      ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M)
          ((HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) k : R[X]) (HPow.hPow (α := R[X]) X n) * X) • m) :
        M) =
    HSMul.hSMul (β := N) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) k : R[X]) (HPow.hPow (α := R[X]) X n) * X)
      ((f : (a : M) → N) ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) m : M) : N)
⊢ (f : (a : M) → N)
      ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M)
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) k : R[X]) (HPow.hPow (α := R[X]) X (n + 1)) • m) :
        M) =
    HSMul.hSMul (β := N) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) k : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))
      ((f : (a : M) → N) ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) m : M) : N)
have simp_rw₂ : (f : (a : M) → N)
    ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M)
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) k : R[X]) (HPow.hPow (α := R[X]) X n) •
          HSMul.hSMul.{u_1, u_3, u_3} (α := R[X]) X m) :
      M) =
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) k : R[X]) (HPow.hPow (α := R[X]) X n) •
    HSMul.hSMul.{u_1, u_4, u_4} (α := R[X]) (β := N) X
      ((f : (a : M) → N) ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) m : M) : N)
Tactic: simp_rw [pow_succ, ← mul_assoc, mul_smul _ X, ← hf, ← of_symm_X_smul, ← h]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.AEval (goal)
Goal:
R : Type u_3
A : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
a : A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
inst_7 : FaithfulSMul A M
⊢ Eq (α := Ideal R[X]) (annihilator.{u_3, u_2} R[X] (AEval R M a)) (RingHom.ker (F := R[X] →ₐ[R] A) (aeval a))
have h : ∀ (p : R[X]),
  Membership.mem (γ := Ideal R[X]) (annihilator.{u_3, u_2} R[X] (AEval R M a)) p ↔
    Membership.mem (γ := Ideal R[X]) (RingHom.ker (F := R[X] →ₐ[R] A) (aeval a)) p
Tactic: ext p
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.AEval (goal)
Goal:
R : Type u_3
A : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
a : A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
inst_7 : FaithfulSMul A M
p : R[X]
⊢ Membership.mem (γ := Ideal R[X]) (annihilator.{u_3, u_2} R[X] (AEval R M a)) p ↔
    Membership.mem (γ := Ideal R[X]) (RingHom.ker (F := R[X] →ₐ[R] A) (aeval a)) p
have h : (∀ (m : AEval R M a), p • m = 0) ↔ Eq.{u_1 + 1} (α := A) ((aeval a : (a : R[X]) → A) p : A) (0 : A)
Tactic: simp_rw [mem_annihilator, RingHom.mem_ker]