awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv :
  Membership.mem (γ := Submodule R M)
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q))) v
p' q' : R[X]
hpq' : p' * p + q' * q = 1
rw :
  Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * p' * q) : M →ₗ[R] M) : (a : M) → M) v : M)
    ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p' * (p * q)) : M →ₗ[R] M) : (a : M) → M) v : M)
⊢ Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (q * (p * p')) : M →ₗ[R] M) : (a : M) → M) v : M)
    ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p' * (p * q)) : M →ₗ[R] M) : (a : M) → M) v : M)
have rw₁ : Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * (p' * q)) : M →ₗ[R] M) : (a : M) → M) v : M)
  ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p' * (p * q)) : M →ₗ[R] M) : (a : M) → M) v : M)
Tactic: rw [mul_comm, mul_assoc, mul_comm, mul_assoc, mul_comm q p]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv :
  Membership.mem (γ := Submodule R M)
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q))) v
p' q' : R[X]
hpq' : p' * p + q' * q = 1
rw :
  Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * p' * q) : M →ₗ[R] M) : (a : M) → M) v : M)
    ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p' * (p * q)) : M →ₗ[R] M) : (a : M) → M) v : M)
rw₁ :
  Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * (p' * q)) : M →ₗ[R] M) : (a : M) → M) v : M)
    ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p' * (p * q)) : M →ₗ[R] M) : (a : M) → M) v : M)
⊢ Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (q * (p * p')) : M →ₗ[R] M) : (a : M) → M) v : M)
    ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p' * (p * q)) : M →ₗ[R] M) : (a : M) → M) v : M)
have rw₂ : Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p' * q * p) : M →ₗ[R] M) : (a : M) → M) v : M)
  ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p' * (p * q)) : M →ₗ[R] M) : (a : M) → M) v : M)
Tactic: rw [mul_comm, mul_assoc, mul_comm, mul_assoc, mul_comm q p]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv :
  Membership.mem (γ := Submodule R M)
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q))) v
p' q' : R[X]
hpq' : p' * p + q' * q = 1
rw :
  Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * p' * q) : M →ₗ[R] M) : (a : M) → M) v : M)
    ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p' * (p * q)) : M →ₗ[R] M) : (a : M) → M) v : M)
rw₁ :
  Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * (p' * q)) : M →ₗ[R] M) : (a : M) → M) v : M)
    ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p' * (p * q)) : M →ₗ[R] M) : (a : M) → M) v : M)
rw₂ :
  Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p' * q * p) : M →ₗ[R] M) : (a : M) → M) v : M)
    ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p' * (p * q)) : M →ₗ[R] M) : (a : M) → M) v : M)
⊢ Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (q * (p * p')) : M →ₗ[R] M) : (a : M) → M) v : M)
    ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p' * (p * q)) : M →ₗ[R] M) : (a : M) → M) v : M)
have rw₃ : Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p' * (q * p)) : M →ₗ[R] M) : (a : M) → M) v : M)
  ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p' * (p * q)) : M →ₗ[R] M) : (a : M) → M) v : M)
Tactic: rw [mul_comm, mul_assoc, mul_comm, mul_assoc, mul_comm q p]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv :
  Membership.mem (γ := Submodule R M)
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q))) v
p' q' : R[X]
hpq' : p' * p + q' * q = 1
rw :
  Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * p' * q) : M →ₗ[R] M) : (a : M) → M) v : M)
    ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p' * (p * q)) : M →ₗ[R] M) : (a : M) → M) v : M)
rw₁ :
  Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * (p' * q)) : M →ₗ[R] M) : (a : M) → M) v : M)
    ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p' * (p * q)) : M →ₗ[R] M) : (a : M) → M) v : M)
rw₂ :
  Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p' * q * p) : M →ₗ[R] M) : (a : M) → M) v : M)
    ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p' * (p * q)) : M →ₗ[R] M) : (a : M) → M) v : M)
rw₃ :
  Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p' * (q * p)) : M →ₗ[R] M) : (a : M) → M) v : M)
    ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p' * (p * q)) : M →ₗ[R] M) : (a : M) → M) v : M)
⊢ Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (q * (p * p')) : M →ₗ[R] M) : (a : M) → M) v : M)
    ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p' * (p * q)) : M →ₗ[R] M) : (a : M) → M) v : M)
have rw₄ : Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p' * (p * q)) : M →ₗ[R] M) : (a : M) → M) v : M)
  ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p' * (p * q)) : M →ₗ[R] M) : (a : M) → M) v : M)
Tactic: rw [mul_comm, mul_assoc, mul_comm, mul_assoc, mul_comm q p]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv :
  Membership.mem (γ := Submodule R M)
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q))) v
p' q' : R[X]
hpq' : p' * p + q' * q = 1
⊢ Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p' * (p * q)) : M →ₗ[R] M) : (a : M) → M) v : M) (0 : M)
have rw : Eq (α := M)
  ((HMul.hMul (α := M →ₗ[R] M) (β := M →ₗ[R] M) ((aeval f : (a : R[X]) → M →ₗ[R] M) p' : M →ₗ[R] M)
          ((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q) : M →ₗ[R] M) :
        (a : M) → M)
      v :
    M)
  (0 : M)
Tactic: rw [aeval_mul, Module.End.mul_apply, LinearMap.mem_ker.1 hv, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv :
  Membership.mem (γ := Submodule R M)
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q))) v
p' q' : R[X]
hpq' : p' * p + q' * q = 1
rw :
  Eq (α := M)
    ((HMul.hMul (α := M →ₗ[R] M) (β := M →ₗ[R] M) ((aeval f : (a : R[X]) → M →ₗ[R] M) p' : M →ₗ[R] M)
            ((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q) : M →ₗ[R] M) :
          (a : M) → M)
        v :
      M)
    (0 : M)
⊢ Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p' * (p * q)) : M →ₗ[R] M) : (a : M) → M) v : M) (0 : M)
have rw₁ : Eq (α := M)
  ((((aeval f : (a : R[X]) → M →ₗ[R] M) p' : M →ₗ[R] M) : (a : M) → M)
      ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q) : M →ₗ[R] M) : (a : M) → M) v : M) :
    M)
  (0 : M)
Tactic: rw [aeval_mul, Module.End.mul_apply, LinearMap.mem_ker.1 hv, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv :
  Membership.mem (γ := Submodule R M)
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q))) v
p' q' : R[X]
hpq' : p' * p + q' * q = 1
rw :
  Eq (α := M)
    ((HMul.hMul (α := M →ₗ[R] M) (β := M →ₗ[R] M) ((aeval f : (a : R[X]) → M →ₗ[R] M) p' : M →ₗ[R] M)
            ((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q) : M →ₗ[R] M) :
          (a : M) → M)
        v :
      M)
    (0 : M)
rw₁ :
  Eq (α := M)
    ((((aeval f : (a : R[X]) → M →ₗ[R] M) p' : M →ₗ[R] M) : (a : M) → M)
        ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q) : M →ₗ[R] M) : (a : M) → M) v : M) :
      M)
    (0 : M)
⊢ Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p' * (p * q)) : M →ₗ[R] M) : (a : M) → M) v : M) (0 : M)
have rw₂ : Eq.{w + 1} (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) p' : M →ₗ[R] M) : (a : M) → M) 0 : M) (0 : M)
Tactic: rw [aeval_mul, Module.End.mul_apply, LinearMap.mem_ker.1 hv, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv :
  Membership.mem (γ := Submodule R M)
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q))) v
p' q' : R[X]
hpq' : p' * p + q' * q = 1
rw :
  Eq (α := M)
    ((HMul.hMul (α := M →ₗ[R] M) (β := M →ₗ[R] M) ((aeval f : (a : R[X]) → M →ₗ[R] M) p' : M →ₗ[R] M)
            ((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q) : M →ₗ[R] M) :
          (a : M) → M)
        v :
      M)
    (0 : M)
rw₁ :
  Eq (α := M)
    ((((aeval f : (a : R[X]) → M →ₗ[R] M) p' : M →ₗ[R] M) : (a : M) → M)
        ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q) : M →ₗ[R] M) : (a : M) → M) v : M) :
      M)
    (0 : M)
rw₂ : Eq.{w + 1} (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) p' : M →ₗ[R] M) : (a : M) → M) 0 : M) (0 : M)
⊢ Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p' * (p * q)) : M →ₗ[R] M) : (a : M) → M) v : M) (0 : M)
have rw₃ : Eq.{w + 1} (α := M) 0 0
Tactic: rw [aeval_mul, Module.End.mul_apply, LinearMap.mem_ker.1 hv, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (hypothesis)
Goal:
R : Type u
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv :
  Membership.mem (γ := Submodule R M)
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q))) v
p' q' : R[X]
hpq' : p' * p + q' * q = 1
⊢ ∃ (y : M),
    Membership.mem (γ := Submodule R M)
        (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) p)) y ∧
      ∃ (z : M),
        Membership.mem (γ := Submodule R M)
            (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q)) z ∧
          y + z = v
have h_eval₂_qpp' : Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (q * (p * p')) : M →ₗ[R] M) : (a : M) → M) v : M) (0 : M)
Tactic: have h_eval₂_qpp' :=
    calc
      aeval f (q * (p * p')) v = aeval f (p' * (p * q)) v := by
        rw [mul_comm, mul_assoc, mul_comm, mul_assoc, mul_comm q p]
      _ = 0 := by rw [aeval_mul, Module.End.mul_apply, LinearMap.mem_ker.1 hv, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv :
  Membership.mem (γ := Submodule R M)
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q))) v
p' q' : R[X]
hpq' : p' * p + q' * q = 1
h_eval₂_qpp' :
  Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (q * (p * p')) : M →ₗ[R] M) : (a : M) → M) v : M) (0 : M)
⊢ Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * (q * q')) : M →ₗ[R] M) : (a : M) → M) v : M)
    ((((aeval f : (a : R[X]) → M →ₗ[R] M) (q' * (p * q)) : M →ₗ[R] M) : (a : M) → M) v : M)
have rw : Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q * q') : M →ₗ[R] M) : (a : M) → M) v : M)
  ((((aeval f : (a : R[X]) → M →ₗ[R] M) (q' * (p * q)) : M →ₗ[R] M) : (a : M) → M) v : M)
Tactic: rw [← mul_assoc, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv :
  Membership.mem (γ := Submodule R M)
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q))) v
p' q' : R[X]
hpq' : p' * p + q' * q = 1
h_eval₂_qpp' :
  Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (q * (p * p')) : M →ₗ[R] M) : (a : M) → M) v : M) (0 : M)
rw :
  Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q * q') : M →ₗ[R] M) : (a : M) → M) v : M)
    ((((aeval f : (a : R[X]) → M →ₗ[R] M) (q' * (p * q)) : M →ₗ[R] M) : (a : M) → M) v : M)
⊢ Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * (q * q')) : M →ₗ[R] M) : (a : M) → M) v : M)
    ((((aeval f : (a : R[X]) → M →ₗ[R] M) (q' * (p * q)) : M →ₗ[R] M) : (a : M) → M) v : M)
have rw₁ : Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (q' * (p * q)) : M →ₗ[R] M) : (a : M) → M) v : M)
  ((((aeval f : (a : R[X]) → M →ₗ[R] M) (q' * (p * q)) : M →ₗ[R] M) : (a : M) → M) v : M)
Tactic: rw [← mul_assoc, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv :
  Membership.mem (γ := Submodule R M)
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q))) v
p' q' : R[X]
hpq' : p' * p + q' * q = 1
h_eval₂_qpp' :
  Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (q * (p * p')) : M →ₗ[R] M) : (a : M) → M) v : M) (0 : M)
⊢ Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (q' * (p * q)) : M →ₗ[R] M) : (a : M) → M) v : M) (0 : M)
have rw : Eq (α := M)
  ((HMul.hMul (α := M →ₗ[R] M) (β := M →ₗ[R] M) ((aeval f : (a : R[X]) → M →ₗ[R] M) q' : M →ₗ[R] M)
          ((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q) : M →ₗ[R] M) :
        (a : M) → M)
      v :
    M)
  (0 : M)
Tactic: rw [aeval_mul, Module.End.mul_apply, LinearMap.mem_ker.1 hv, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv :
  Membership.mem (γ := Submodule R M)
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q))) v
p' q' : R[X]
hpq' : p' * p + q' * q = 1
h_eval₂_qpp' :
  Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (q * (p * p')) : M →ₗ[R] M) : (a : M) → M) v : M) (0 : M)
rw :
  Eq (α := M)
    ((HMul.hMul (α := M →ₗ[R] M) (β := M →ₗ[R] M) ((aeval f : (a : R[X]) → M →ₗ[R] M) q' : M →ₗ[R] M)
            ((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q) : M →ₗ[R] M) :
          (a : M) → M)
        v :
      M)
    (0 : M)
⊢ Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (q' * (p * q)) : M →ₗ[R] M) : (a : M) → M) v : M) (0 : M)
have rw₁ : Eq (α := M)
  ((((aeval f : (a : R[X]) → M →ₗ[R] M) q' : M →ₗ[R] M) : (a : M) → M)
      ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q) : M →ₗ[R] M) : (a : M) → M) v : M) :
    M)
  (0 : M)
Tactic: rw [aeval_mul, Module.End.mul_apply, LinearMap.mem_ker.1 hv, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv :
  Membership.mem (γ := Submodule R M)
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q))) v
p' q' : R[X]
hpq' : p' * p + q' * q = 1
h_eval₂_qpp' :
  Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (q * (p * p')) : M →ₗ[R] M) : (a : M) → M) v : M) (0 : M)
rw :
  Eq (α := M)
    ((HMul.hMul (α := M →ₗ[R] M) (β := M →ₗ[R] M) ((aeval f : (a : R[X]) → M →ₗ[R] M) q' : M →ₗ[R] M)
            ((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q) : M →ₗ[R] M) :
          (a : M) → M)
        v :
      M)
    (0 : M)
rw₁ :
  Eq (α := M)
    ((((aeval f : (a : R[X]) → M →ₗ[R] M) q' : M →ₗ[R] M) : (a : M) → M)
        ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q) : M →ₗ[R] M) : (a : M) → M) v : M) :
      M)
    (0 : M)
⊢ Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (q' * (p * q)) : M →ₗ[R] M) : (a : M) → M) v : M) (0 : M)
have rw₂ : Eq.{w + 1} (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) q' : M →ₗ[R] M) : (a : M) → M) 0 : M) (0 : M)
Tactic: rw [aeval_mul, Module.End.mul_apply, LinearMap.mem_ker.1 hv, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv :
  Membership.mem (γ := Submodule R M)
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q))) v
p' q' : R[X]
hpq' : p' * p + q' * q = 1
h_eval₂_qpp' :
  Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (q * (p * p')) : M →ₗ[R] M) : (a : M) → M) v : M) (0 : M)
rw :
  Eq (α := M)
    ((HMul.hMul (α := M →ₗ[R] M) (β := M →ₗ[R] M) ((aeval f : (a : R[X]) → M →ₗ[R] M) q' : M →ₗ[R] M)
            ((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q) : M →ₗ[R] M) :
          (a : M) → M)
        v :
      M)
    (0 : M)
rw₁ :
  Eq (α := M)
    ((((aeval f : (a : R[X]) → M →ₗ[R] M) q' : M →ₗ[R] M) : (a : M) → M)
        ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q) : M →ₗ[R] M) : (a : M) → M) v : M) :
      M)
    (0 : M)
rw₂ : Eq.{w + 1} (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) q' : M →ₗ[R] M) : (a : M) → M) 0 : M) (0 : M)
⊢ Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (q' * (p * q)) : M →ₗ[R] M) : (a : M) → M) v : M) (0 : M)
have rw₃ : Eq.{w + 1} (α := M) 0 0
Tactic: rw [aeval_mul, Module.End.mul_apply, LinearMap.mem_ker.1 hv, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (hypothesis)
Goal:
R : Type u
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv :
  Membership.mem (γ := Submodule R M)
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q))) v
p' q' : R[X]
hpq' : p' * p + q' * q = 1
h_eval₂_qpp' :
  Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (q * (p * p')) : M →ₗ[R] M) : (a : M) → M) v : M) (0 : M)
⊢ ∃ (y : M),
    Membership.mem (γ := Submodule R M)
        (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) p)) y ∧
      ∃ (z : M),
        Membership.mem (γ := Submodule R M)
            (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q)) z ∧
          y + z = v
have h_eval₂_pqq' : Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * (q * q')) : M →ₗ[R] M) : (a : M) → M) v : M) (0 : M)
Tactic: have h_eval₂_pqq' :=
    calc
      aeval f (p * (q * q')) v = aeval f (q' * (p * q)) v := by rw [← mul_assoc, mul_comm]
      _ = 0 := by rw [aeval_mul, Module.End.mul_apply, LinearMap.mem_ker.1 hv, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (hypothesis)
Goal:
R : Type u
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv :
  Membership.mem (γ := Submodule R M)
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q))) v
p' q' : R[X]
hpq' : p' * p + q' * q = 1
h_eval₂_qpp' :
  Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (q * (p * p')) : M →ₗ[R] M) : (a : M) → M) v : M) (0 : M)
h_eval₂_pqq' :
  Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * (q * q')) : M →ₗ[R] M) : (a : M) → M) v : M) (0 : M)
⊢ ∃ (y : M),
    Membership.mem (γ := Submodule R M)
        (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) p)) y ∧
      ∃ (z : M),
        Membership.mem (γ := Submodule R M)
            (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q)) z ∧
          y + z = v
have h_eval₂_qpp'₁ : Eq (α := M)
  ((HMul.hMul (α := M →ₗ[R] M) (β := M →ₗ[R] M) ((aeval f : (a : R[X]) → M →ₗ[R] M) q : M →ₗ[R] M)
          ((aeval f : (a : R[X]) → M →ₗ[R] M) (p * p') : M →ₗ[R] M) :
        (a : M) → M)
      v :
    M)
  (0 : M)
Tactic: rw [aeval_mul] at h_eval₂_qpp' h_eval₂_pqq'
Cleared hypotheses: h_eval₂_qpp', h_eval₂_pqq'
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (hypothesis)
Goal:
R : Type u
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv :
  Membership.mem (γ := Submodule R M)
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q))) v
p' q' : R[X]
hpq' : p' * p + q' * q = 1
h_eval₂_qpp' :
  Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (q * (p * p')) : M →ₗ[R] M) : (a : M) → M) v : M) (0 : M)
h_eval₂_pqq' :
  Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * (q * q')) : M →ₗ[R] M) : (a : M) → M) v : M) (0 : M)
h_eval₂_qpp'₁ :
  Eq (α := M)
    ((HMul.hMul (α := M →ₗ[R] M) (β := M →ₗ[R] M) ((aeval f : (a : R[X]) → M →ₗ[R] M) q : M →ₗ[R] M)
            ((aeval f : (a : R[X]) → M →ₗ[R] M) (p * p') : M →ₗ[R] M) :
          (a : M) → M)
        v :
      M)
    (0 : M)
⊢ ∃ (y : M),
    Membership.mem (γ := Submodule R M)
        (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) p)) y ∧
      ∃ (z : M),
        Membership.mem (γ := Submodule R M)
            (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q)) z ∧
          y + z = v
have h_eval₂_pqq'₁ : Eq (α := M)
  ((HMul.hMul (α := M →ₗ[R] M) (β := M →ₗ[R] M) ((aeval f : (a : R[X]) → M →ₗ[R] M) p : M →ₗ[R] M)
          ((aeval f : (a : R[X]) → M →ₗ[R] M) (q * q') : M →ₗ[R] M) :
        (a : M) → M)
      v :
    M)
  (0 : M)
Tactic: rw [aeval_mul] at h_eval₂_qpp' h_eval₂_pqq'
Cleared hypotheses: h_eval₂_qpp', h_eval₂_pqq'
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv :
  Membership.mem (γ := Submodule R M)
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q))) v
p' q' : R[X]
hpq' : p' * p + q' * q = 1
h_eval₂_qpp' :
  Eq (α := M)
    ((HMul.hMul (α := M →ₗ[R] M) (β := M →ₗ[R] M) ((aeval f : (a : R[X]) → M →ₗ[R] M) q : M →ₗ[R] M)
            ((aeval f : (a : R[X]) → M →ₗ[R] M) (p * p') : M →ₗ[R] M) :
          (a : M) → M)
        v :
      M)
    (0 : M)
h_eval₂_pqq' :
  Eq (α := M)
    ((HMul.hMul (α := M →ₗ[R] M) (β := M →ₗ[R] M) ((aeval f : (a : R[X]) → M →ₗ[R] M) p : M →ₗ[R] M)
            ((aeval f : (a : R[X]) → M →ₗ[R] M) (q * q') : M →ₗ[R] M) :
          (a : M) → M)
        v :
      M)
    (0 : M)
⊢ ∃ (y : M),
    Membership.mem (γ := Submodule R M)
        (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) p)) y ∧
      ∃ (z : M),
        Membership.mem (γ := Submodule R M)
            (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q)) z ∧
          y + z = v
have f₁ : HAdd.hAdd (α := M) (β := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (q * q') : M →ₗ[R] M) : (a : M) → M) v : M)
    ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * p') : M →ₗ[R] M) : (a : M) → M) v : M) =
  v
Tactic: refine
    ⟨aeval f (q * q') v, LinearMap.mem_ker.1 h_eval₂_pqq', aeval f (p * p') v,
      LinearMap.mem_ker.1 h_eval₂_qpp', ?_⟩