awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst_1 : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (r := fun (x1 x2 : Submodule R R) ↦ x1 > x2) (Set.range I.leadingCoeffNth) ⋯
hm : M ∈ Set.range I.leadingCoeffNth
N : ℕ
HN : I.leadingCoeffNth N = M
s : Finset R[X]
hs : Submodule.span R (↑s : Set R[X]) = I.degreeLE (↑N : WithBot ℕ)
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE (↑N : WithBot ℕ) → Membership.mem (γ := Ideal R[X]) (Ideal.span (↑s : Set R[X])) x
this_1 : Eq (α := Submodule R[X] R[X]) (Submodule.span R[X] (↑s : Set R[X])) (Ideal.span (↑s : Set R[X]))
k : ℕ
ih :
  ∀ m < k,
    ∀ ⦃p : R[X]⦄ (hp : p ∈ I) (hn : p.natDegree = m),
      Membership.mem (γ := Submodule R[X] R[X]) (Ideal.span (↑s : Set R[X])) p
p : R[X]
hp : p ∈ I
hn : p.natDegree = k
h : N < k
hp0 : p ≠ 0
this_2 : Ne.{u + 1} (α := R) 0 1
this_3 : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : q.degree ≤ (↑N : WithBot ℕ)
hlqp : q.leadingCoeff = p.leadingCoeff
hq0 : q ≠ 0
h1 : p.degree = (q * HPow.hPow (α := R[X]) X (k - q.natDegree)).degree
h2 : p.leadingCoeff = (q * HPow.hPow (α := R[X]) X (k - q.natDegree)).leadingCoeff
this : (p - q * HPow.hPow (α := R[X]) X (k - q.natDegree)).degree < (↑p.natDegree : WithBot ℕ)
hpq : ¬p - q * HPow.hPow (α := R[X]) X (k - q.natDegree) = 0
⊢ (p - q * HPow.hPow (α := R[X]) X (k - q.natDegree)).natDegree < k
have neg : ∀
  (this :
    LT.lt (α := WithBot ℕ) (↑(p - q * HPow.hPow (α := R[X]) X (k - q.natDegree)).natDegree : WithBot ℕ)
      (↑p.natDegree : WithBot ℕ))
  (hpq : ¬p - q * HPow.hPow (α := R[X]) X (k - q.natDegree) = 0),
  (p - q * HPow.hPow (α := R[X]) X (k - q.natDegree)).natDegree < k
Tactic: rwa [Polynomial.degree_eq_natDegree hpq, Nat.cast_lt, hn] at this
Cleared hypotheses: this, hpq
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst_1 : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (r := fun (x1 x2 : Submodule R R) ↦ x1 > x2) (Set.range I.leadingCoeffNth) ⋯
hm : M ∈ Set.range I.leadingCoeffNth
N : ℕ
HN : I.leadingCoeffNth N = M
s : Finset R[X]
hs : Submodule.span R (↑s : Set R[X]) = I.degreeLE (↑N : WithBot ℕ)
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE (↑N : WithBot ℕ) → Membership.mem (γ := Ideal R[X]) (Ideal.span (↑s : Set R[X])) x
this_1 : Eq (α := Submodule R[X] R[X]) (Submodule.span R[X] (↑s : Set R[X])) (Ideal.span (↑s : Set R[X]))
k : ℕ
ih :
  ∀ m < k,
    ∀ ⦃p : R[X]⦄ (hp : p ∈ I) (hn : p.natDegree = m),
      Membership.mem (γ := Submodule R[X] R[X]) (Ideal.span (↑s : Set R[X])) p
p : R[X]
hp : p ∈ I
hn : p.natDegree = k
h : N < k
hp0 : p ≠ 0
this_2 : Ne.{u + 1} (α := R) 0 1
this_3 : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : q.degree ≤ (↑N : WithBot ℕ)
hlqp : q.leadingCoeff = p.leadingCoeff
hq0 : q ≠ 0
h1 : p.degree = (q * HPow.hPow (α := R[X]) X (k - q.natDegree)).degree
h2 : p.leadingCoeff = (q * HPow.hPow (α := R[X]) X (k - q.natDegree)).leadingCoeff
this : (p - q * HPow.hPow (α := R[X]) X (k - q.natDegree)).degree < (↑p.natDegree : WithBot ℕ)
hpq : ¬p - q * HPow.hPow (α := R[X]) X (k - q.natDegree) = 0
neg :
  ∀
    (this :
      LT.lt (α := WithBot ℕ) (↑(p - q * HPow.hPow (α := R[X]) X (k - q.natDegree)).natDegree : WithBot ℕ)
        (↑p.natDegree : WithBot ℕ))
    (hpq : ¬p - q * HPow.hPow (α := R[X]) X (k - q.natDegree) = 0),
    (p - q * HPow.hPow (α := R[X]) X (k - q.natDegree)).natDegree < k
⊢ (p - q * HPow.hPow (α := R[X]) X (k - q.natDegree)).natDegree < k
have neg₁ : ∀ (this : (p - q * HPow.hPow (α := R[X]) X (k - q.natDegree)).natDegree < p.natDegree)
  (hpq : ¬p - q * HPow.hPow (α := R[X]) X (k - q.natDegree) = 0),
  (p - q * HPow.hPow (α := R[X]) X (k - q.natDegree)).natDegree < k
Tactic: rwa [Polynomial.degree_eq_natDegree hpq, Nat.cast_lt, hn] at this
Cleared hypotheses: this, hpq
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst_1 : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (r := fun (x1 x2 : Submodule R R) ↦ x1 > x2) (Set.range I.leadingCoeffNth) ⋯
hm : M ∈ Set.range I.leadingCoeffNth
N : ℕ
HN : I.leadingCoeffNth N = M
s : Finset R[X]
hs : Submodule.span R (↑s : Set R[X]) = I.degreeLE (↑N : WithBot ℕ)
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE (↑N : WithBot ℕ) → Membership.mem (γ := Ideal R[X]) (Ideal.span (↑s : Set R[X])) x
this_1 : Eq (α := Submodule R[X] R[X]) (Submodule.span R[X] (↑s : Set R[X])) (Ideal.span (↑s : Set R[X]))
k : ℕ
ih :
  ∀ m < k,
    ∀ ⦃p : R[X]⦄ (hp : p ∈ I) (hn : p.natDegree = m),
      Membership.mem (γ := Submodule R[X] R[X]) (Ideal.span (↑s : Set R[X])) p
p : R[X]
hp : p ∈ I
hn : p.natDegree = k
h : N < k
hp0 : p ≠ 0
this_2 : Ne.{u + 1} (α := R) 0 1
this_3 : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : q.degree ≤ (↑N : WithBot ℕ)
hlqp : q.leadingCoeff = p.leadingCoeff
hq0 : q ≠ 0
h1 : p.degree = (q * HPow.hPow (α := R[X]) X (k - q.natDegree)).degree
h2 : p.leadingCoeff = (q * HPow.hPow (α := R[X]) X (k - q.natDegree)).leadingCoeff
this : (p - q * HPow.hPow (α := R[X]) X (k - q.natDegree)).degree < (↑p.natDegree : WithBot ℕ)
hpq : ¬p - q * HPow.hPow (α := R[X]) X (k - q.natDegree) = 0
neg :
  ∀
    (this :
      LT.lt (α := WithBot ℕ) (↑(p - q * HPow.hPow (α := R[X]) X (k - q.natDegree)).natDegree : WithBot ℕ)
        (↑p.natDegree : WithBot ℕ))
    (hpq : ¬p - q * HPow.hPow (α := R[X]) X (k - q.natDegree) = 0),
    (p - q * HPow.hPow (α := R[X]) X (k - q.natDegree)).natDegree < k
neg₁ :
  ∀ (this : (p - q * HPow.hPow (α := R[X]) X (k - q.natDegree)).natDegree < p.natDegree)
    (hpq : ¬p - q * HPow.hPow (α := R[X]) X (k - q.natDegree) = 0),
    (p - q * HPow.hPow (α := R[X]) X (k - q.natDegree)).natDegree < k
⊢ (p - q * HPow.hPow (α := R[X]) X (k - q.natDegree)).natDegree < k
have neg₂ : ∀ (this : (p - q * HPow.hPow (α := R[X]) X (k - q.natDegree)).natDegree < k)
  (hpq : ¬p - q * HPow.hPow (α := R[X]) X (k - q.natDegree) = 0),
  (p - q * HPow.hPow (α := R[X]) X (k - q.natDegree)).natDegree < k
Tactic: rwa [Polynomial.degree_eq_natDegree hpq, Nat.cast_lt, hn] at this
Cleared hypotheses: this, 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
v : M
⊢ (LinearIndependent.{0, u, w} R (M := M) fun (n : ℕ) ↦ (f ^ n : (a : M) → M) v) ↔
    ∀ (p : R[X]), Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) p : M →ₗ[R] M) : (a : M) → M) v : M) (0 : M) → p = 0
have rw : (∀ (l : ℕ →₀ R),
    Eq.{w + 1} (α := M) ((Finsupp.linearCombination R fun (n : ℕ) ↦ (f ^ n : (a : M) → M) v : (a : ℕ →₀ R) → M) l : M)
        (0 : M) →
      l = 0) ↔
  ∀ (p : R[X]), Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) p : M →ₗ[R] M) : (a : M) → M) v : M) (0 : M) → p = 0
Tactic: rw [linearIndependent_iff]
-- 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
v : M
⊢ (∀ (l : ℕ →₀ R),
      Eq.{w + 1} (α := M) ((Finsupp.linearCombination R fun (n : ℕ) ↦ (f ^ n : (a : M) → M) v : (a : ℕ →₀ R) → M) l : M)
          (0 : M) →
        l = 0) ↔
    ∀ (p : R[X]), Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) p : M →ₗ[R] M) : (a : M) → M) v : M) (0 : M) → p = 0
have simp : (∀ (l : ℕ →₀ R),
    Eq.{w + 1} (α := M) (l.sum fun (i : ℕ) (a : R) ↦ HSMul.hSMul (β := M) a ((f ^ i : (a : M) → M) v : M)) 0 → l = 0) ↔
  ∀ (q : AddMonoidAlgebra R ℕ),
    Eq.{w + 1} (α := M)
        ({ toFinsupp := q : R[X] }.sum fun (n : ℕ) (b : R) ↦ HSMul.hSMul (β := M) b ((f ^ n : (a : M) → M) v : M)) 0 →
      q = 0
Tactic: simp only [Finsupp.linearCombination_apply, aeval_endomorphism, forall_iff_forall_finsupp,
    ofFinsupp_eq_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
⊢ Disjoint.{w} (α := 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))
have rw : LE.le.{w} (α := 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))
  ⊥
Tactic: rw [disjoint_iff_inf_le]
-- 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) ⊓
      LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q))
    v
⊢ Membership.mem (γ := Submodule R M) ⊥ v
have rcases : ∀ (p' q' : R[X]) (hpq' : p' * p + q' * q = 1), Membership.mem (γ := Submodule R M) ⊥ 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]
hpq : IsCoprime p q
⊢ Eq.{w + 1} (α := Submodule R M)
    (LinearMap.range (R := R) (M := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) p) ⊔
      LinearMap.range (R := R) (M := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q))
    ⊤
have rw : LE.le.{w} (α := Submodule R M) ⊤
  (LinearMap.range (R := R) (M := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) p) ⊔
    LinearMap.range (R := R) (M := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q))
Tactic: rw [eq_top_iff]
-- 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
h : Membership.mem (γ := Submodule R M) ⊤ v
⊢ Membership.mem (γ := Submodule R M)
    (LinearMap.range (R := R) (M := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) p) ⊔
      LinearMap.range (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.range (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.range (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
h : Membership.mem (γ := Submodule R M) ⊤ v
⊢ ∃ (y : M),
    Membership.mem (γ := Submodule R M)
        (LinearMap.range (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.range (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.range (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.range (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
h : Membership.mem (γ := Submodule R M) ⊤ v
p' q' : R[X]
hpq' : p' * p + q' * q = 1
⊢ ∃ (y : M),
    Membership.mem (γ := Submodule R M)
        (LinearMap.range (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.range (R := R) (M := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q)) z ∧
          y + z = v
have h : Membership.mem (α := M) (γ := Submodule R M)
    (LinearMap.range (R := R) (M := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) p))
    ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * p') : M →ₗ[R] M) : (a : M) → M) v : M) ∧
  ∃ (z : M),
    Membership.mem (γ := Submodule R M)
        (LinearMap.range (R := R) (M := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q)) z ∧
      HAdd.hAdd (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * p') : M →ₗ[R] M) : (a : M) → M) v : M) z = v
Tactic: use aeval f (p * p') v
-- 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
h : Membership.mem (γ := Submodule R M) ⊤ v
p' q' : R[X]
hpq' : p' * p + q' * q = 1
⊢ Membership.mem (α := M) (γ := Submodule R M)
      (LinearMap.range (R := R) (M := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) p))
      ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * p') : M →ₗ[R] M) : (a : M) → M) v : M) ∧
    ∃ (z : M),
      Membership.mem (γ := Submodule R M)
          (LinearMap.range (R := R) (M := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q)) z ∧
        HAdd.hAdd (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * p') : M →ₗ[R] M) : (a : M) → M) v : M) z = v
have right : ∃ (z : M),
  Membership.mem (γ := Submodule R M)
      (LinearMap.range (R := R) (M := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q)) z ∧
    HAdd.hAdd (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * p') : M →ₗ[R] M) : (a : M) → M) v : M) z = v
Tactic: use LinearMap.mem_range.2 ⟨aeval f p' v, by simp only [Module.End.mul_apply, 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]
v : M
h : Membership.mem (γ := Submodule R M) ⊤ v
p' q' : R[X]
hpq' : p' * p + q' * q = 1
⊢ ∃ (z : M),
    Membership.mem (γ := Submodule R M)
        (LinearMap.range (R := R) (M := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q)) z ∧
      HAdd.hAdd (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * p') : M →ₗ[R] M) : (a : M) → M) v : M) z = v
have h : Membership.mem (α := M) (γ := Submodule R M)
    (LinearMap.range (R := R) (M := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q))
    ((((aeval f : (a : R[X]) → M →ₗ[R] M) (q * q') : M →ₗ[R] M) : (a : M) → M) v : M) ∧
  HAdd.hAdd (α := M) (β := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * p') : M →ₗ[R] M) : (a : M) → M) v : M)
      ((((aeval f : (a : R[X]) → M →ₗ[R] M) (q * q') : M →ₗ[R] M) : (a : M) → M) v : M) =
    v
Tactic: use aeval f (q * q') v
-- 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
h : Membership.mem (γ := Submodule R M) ⊤ v
p' q' : R[X]
hpq' : p' * p + q' * q = 1
⊢ Membership.mem (α := M) (γ := Submodule R M)
      (LinearMap.range (R := R) (M := M) (τ₁₂ := RingHom.id R) ((aeval f : (a : R[X]) → M →ₗ[R] M) q))
      ((((aeval f : (a : R[X]) → M →ₗ[R] M) (q * q') : M →ₗ[R] M) : (a : M) → M) v : M) ∧
    HAdd.hAdd (α := M) (β := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * p') : M →ₗ[R] M) : (a : M) → M) v : M)
        ((((aeval f : (a : R[X]) → M →ₗ[R] M) (q * q') : M →ₗ[R] M) : (a : M) → M) v : M) =
      v
have right : HAdd.hAdd (α := M) (β := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (p * p') : M →ₗ[R] M) : (a : M) → M) v : M)
    ((((aeval f : (a : R[X]) → M →ₗ[R] M) (q * q') : M →ₗ[R] M) : (a : M) → M) v : M) =
  v
Tactic: use LinearMap.mem_range.2 ⟨aeval f q' v, by simp only [Module.End.mul_apply, 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]
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
⊢ 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 rcases : ∀ (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
Tactic: rcases Submodule.mem_sup.1 hv with ⟨x, hx, y, hy, hxy⟩
-- 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
⊢ 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 (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) (q * p) : M →ₗ[R] M) : (a : M) → M) x : M) (0 : M)
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 (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)
⊢ 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 (α := 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)
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 (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)
⊢ 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 (α := 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)
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 (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)
⊢ 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) ((((aeval f : (a : R[X]) → M →ₗ[R] M) q : M →ₗ[R] M) : (a : M) → M) 0 : M) (0 : M)
Tactic: rw [mul_comm, aeval_mul, Module.End.mul_apply, LinearMap.mem_ker.1 hx, map_zero]