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) ⊔
      LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q))
    v
x : M
hx :
  Membership.mem (γ := Submodule R M)
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) p)) x
y : M
hy :
  Membership.mem (γ := Submodule R M)
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q)) y
hxy : x + y = v
rw : Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (q * p) : M →ₗ[R] M) : (a : M) → M) x : 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 : M →ₗ[R] M) :
          (a : M) → M)
        x :
      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 : M →ₗ[R] M) : (a : M) → M) x : 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) (p * q) : M →ₗ[R] M) : (a : M) → M) x : M) (0 : M)
have rw₄ : Eq.{w + 1} (α := M) 0 0
Tactic: rw [mul_comm, aeval_mul, Module.End.mul_apply, LinearMap.mem_ker.1 hx, 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) ⊔
      LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q))
    v
x : M
hx :
  Membership.mem (γ := Submodule R M)
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) p)) x
y : M
hy :
  Membership.mem (γ := Submodule R M)
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q)) y
hxy : x + y = v
⊢ 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
have h_eval_x : Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q) : M →ₗ[R] M) : (a : M) → M) x : M) (0 : M)
Tactic: have h_eval_x : aeval f (p * q) x = 0 := by
    rw [mul_comm, aeval_mul, Module.End.mul_apply, LinearMap.mem_ker.1 hx, 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) ⊔
      LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q))
    v
x : M
hx :
  Membership.mem (γ := Submodule R M)
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) p)) x
y : M
hy :
  Membership.mem (γ := Submodule R M)
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q)) y
hxy : x + y = v
h_eval_x : Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q) : M →ₗ[R] M) : (a : M) → M) x : M) (0 : M)
⊢ Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q) : M →ₗ[R] M) : (a : M) → M) y : 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) q : M →ₗ[R] M) :
        (a : M) → M)
      y :
    M)
  (0 : M)
Tactic: rw [aeval_mul, Module.End.mul_apply, LinearMap.mem_ker.1 hy, 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) ⊔
      LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q))
    v
x : M
hx :
  Membership.mem (γ := Submodule R M)
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) p)) x
y : M
hy :
  Membership.mem (γ := Submodule R M)
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q)) y
hxy : x + y = v
h_eval_x : Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q) : M →ₗ[R] M) : (a : M) → M) x : M) (0 : M)
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) q : M →ₗ[R] M) :
          (a : M) → M)
        y :
      M)
    (0 : M)
⊢ Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q) : M →ₗ[R] M) : (a : M) → M) y : 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) q : M →ₗ[R] M) : (a : M) → M) y : M) :
    M)
  (0 : M)
Tactic: rw [aeval_mul, Module.End.mul_apply, LinearMap.mem_ker.1 hy, 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) ⊔
      LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q))
    v
x : M
hx :
  Membership.mem (γ := Submodule R M)
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) p)) x
y : M
hy :
  Membership.mem (γ := Submodule R M)
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q)) y
hxy : x + y = v
h_eval_x : Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q) : M →ₗ[R] M) : (a : M) → M) x : M) (0 : M)
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) q : M →ₗ[R] M) :
          (a : M) → M)
        y :
      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) q : M →ₗ[R] M) : (a : M) → M) y : M) :
      M)
    (0 : M)
⊢ Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q) : M →ₗ[R] M) : (a : M) → M) y : 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 hy, 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) ⊔
      LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q))
    v
x : M
hx :
  Membership.mem (γ := Submodule R M)
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) p)) x
y : M
hy :
  Membership.mem (γ := Submodule R M)
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q)) y
hxy : x + y = v
h_eval_x : Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q) : M →ₗ[R] M) : (a : M) → M) x : M) (0 : M)
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) q : M →ₗ[R] M) :
          (a : M) → M)
        y :
      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) q : M →ₗ[R] M) : (a : M) → M) y : 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 * q) : M →ₗ[R] M) : (a : M) → M) y : M) (0 : M)
have rw₃ : Eq.{w + 1} (α := M) 0 0
Tactic: rw [aeval_mul, Module.End.mul_apply, LinearMap.mem_ker.1 hy, 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) ⊔
      LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q))
    v
x : M
hx :
  Membership.mem (γ := Submodule R M)
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) p)) x
y : M
hy :
  Membership.mem (γ := Submodule R M)
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q)) y
hxy : x + y = v
h_eval_x : Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q) : M →ₗ[R] M) : (a : M) → M) x : M) (0 : M)
⊢ 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
have h_eval_y : Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q) : M →ₗ[R] M) : (a : M) → M) y : M) (0 : M)
Tactic: have h_eval_y : aeval f (p * q) y = 0 := by
    rw [aeval_mul, Module.End.mul_apply, LinearMap.mem_ker.1 hy, 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) ⊔
      LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q))
    v
x : M
hx :
  Membership.mem (γ := Submodule R M)
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) p)) x
y : M
hy :
  Membership.mem (γ := Submodule R M)
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q)) y
hxy : x + y = v
h_eval_x : Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q) : M →ₗ[R] M) : (a : M) → M) x : M) (0 : M)
h_eval_y : Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q) : M →ₗ[R] M) : (a : M) → M) y : M) (0 : M)
⊢ 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
have rw : Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q) : M →ₗ[R] M) : (a : M) → M) v : M) (0 : M)
Tactic: rw [LinearMap.mem_ker, ← hxy, map_add, h_eval_x, h_eval_y, add_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) ⊔
      LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q))
    v
x : M
hx :
  Membership.mem (γ := Submodule R M)
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) p)) x
y : M
hy :
  Membership.mem (γ := Submodule R M)
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q)) y
hxy : x + y = v
h_eval_x : Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q) : M →ₗ[R] M) : (a : M) → M) x : M) (0 : M)
h_eval_y : Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q) : M →ₗ[R] M) : (a : M) → M) y : M) (0 : M)
rw : Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q) : M →ₗ[R] M) : (a : M) → M) v : M) (0 : M)
⊢ 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
have rw₁ : Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q) : M →ₗ[R] M) : (a : M) → M) (x + y) : M) (0 : M)
Tactic: rw [LinearMap.mem_ker, ← hxy, map_add, h_eval_x, h_eval_y, add_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) ⊔
      LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q))
    v
x : M
hx :
  Membership.mem (γ := Submodule R M)
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) p)) x
y : M
hy :
  Membership.mem (γ := Submodule R M)
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q)) y
hxy : x + y = v
h_eval_x : Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q) : M →ₗ[R] M) : (a : M) → M) x : M) (0 : M)
h_eval_y : Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q) : M →ₗ[R] M) : (a : M) → M) y : M) (0 : M)
rw : Eq (α := 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 * q) : M →ₗ[R] M) : (a : M) → M) (x + y) : M) (0 : M)
⊢ 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
have rw₂ : HAdd.hAdd (α := M) (β := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q) : M →ₗ[R] M) : (a : M) → M) x : M)
    ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q) : M →ₗ[R] M) : (a : M) → M) y : M) =
  0
Tactic: rw [LinearMap.mem_ker, ← hxy, map_add, h_eval_x, h_eval_y, add_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) ⊔
      LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q))
    v
x : M
hx :
  Membership.mem (γ := Submodule R M)
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) p)) x
y : M
hy :
  Membership.mem (γ := Submodule R M)
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q)) y
hxy : x + y = v
h_eval_x : Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q) : M →ₗ[R] M) : (a : M) → M) x : M) (0 : M)
h_eval_y : Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q) : M →ₗ[R] M) : (a : M) → M) y : M) (0 : M)
rw : Eq (α := 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 * q) : M →ₗ[R] M) : (a : M) → M) (x + y) : M) (0 : M)
rw₂ :
  HAdd.hAdd (α := M) (β := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q) : M →ₗ[R] M) : (a : M) → M) x : M)
      ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q) : M →ₗ[R] M) : (a : M) → M) y : M) =
    0
⊢ 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
have rw₃ : HAdd.hAdd (α := M) (β := M) (0 : M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q) : M →ₗ[R] M) : (a : M) → M) y : M) = 0
Tactic: rw [LinearMap.mem_ker, ← hxy, map_add, h_eval_x, h_eval_y, add_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) ⊔
      LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q))
    v
x : M
hx :
  Membership.mem (γ := Submodule R M)
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) p)) x
y : M
hy :
  Membership.mem (γ := Submodule R M)
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q)) y
hxy : x + y = v
h_eval_x : Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q) : M →ₗ[R] M) : (a : M) → M) x : M) (0 : M)
h_eval_y : Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q) : M →ₗ[R] M) : (a : M) → M) y : M) (0 : M)
rw : Eq (α := 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 * q) : M →ₗ[R] M) : (a : M) → M) (x + y) : M) (0 : M)
rw₂ :
  HAdd.hAdd (α := M) (β := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q) : M →ₗ[R] M) : (a : M) → M) x : M)
      ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q) : M →ₗ[R] M) : (a : M) → M) y : M) =
    0
rw₃ :
  HAdd.hAdd (α := M) (β := M) (0 : M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q) : M →ₗ[R] M) : (a : M) → M) y : M) =
    0
⊢ 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
have rw₄ : HAdd.hAdd (α := M) 0 0 = 0
Tactic: rw [LinearMap.mem_ker, ← hxy, map_add, h_eval_x, h_eval_y, add_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) ⊔
      LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q))
    v
x : M
hx :
  Membership.mem (γ := Submodule R M)
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) p)) x
y : M
hy :
  Membership.mem (γ := Submodule R M)
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q)) y
hxy : x + y = v
h_eval_x : Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q) : M →ₗ[R] M) : (a : M) → M) x : M) (0 : M)
h_eval_y : Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q) : M →ₗ[R] M) : (a : M) → M) y : M) (0 : M)
rw : Eq (α := 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 * q) : M →ₗ[R] M) : (a : M) → M) (x + y) : M) (0 : M)
rw₂ :
  HAdd.hAdd (α := M) (β := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q) : M →ₗ[R] M) : (a : M) → M) x : M)
      ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q) : M →ₗ[R] M) : (a : M) → M) y : M) =
    0
rw₃ :
  HAdd.hAdd (α := M) (β := M) (0 : M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q) : M →ₗ[R] M) : (a : M) → M) y : M) =
    0
rw₄ : HAdd.hAdd (α := M) 0 0 = 0
⊢ 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
have rw₅ : Eq.{w + 1} (α := M) 0 0
Tactic: rw [LinearMap.mem_ker, ← hxy, map_add, h_eval_x, h_eval_y, add_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]
hpq : IsCoprime p q
⊢ Eq.{w + 1} (α := Submodule R M)
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) p) ⊔
      LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q))
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q)))
have apply : LE.le.{w} (α := Submodule R M)
  (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) (p * q)))
  (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) p) ⊔
    LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q))
Tactic: apply le_antisymm sup_ker_aeval_le_ker_aeval_mul
-- 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]
hpq : IsCoprime p q
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
⊢ Membership.mem (γ := Submodule R M)
    (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) p) ⊔
      LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q))
    v
have rw : ∃ (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
Tactic: rw [Submodule.mem_sup]
-- 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]
hpq : IsCoprime p q
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
⊢ ∃ (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 rcases : ∀ (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
Tactic: rcases hpq with ⟨p', q', hpq'⟩
Cleared hypotheses: hpq
-- 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) (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]