awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
r : R
φ : MvPolynomial σ R
C : (i : σ →₀ ℕ) → R
hc : ∀ (i : σ →₀ ℕ), coeff i φ = r * C i
mpr mpr₁ mpr₂ mpr₃ : (MvPolynomial.C : (a : R) → MvPolynomial σ R) r ∣ φ
h :
  let c' : (σ →₀ ℕ) → R := fun (i : σ →₀ ℕ) ↦ if i ∈ φ.support then C i else 0;
  let ψ : MvPolynomial σ R := ∑ i ∈ φ.support, (monomial i : (a : R) → MvPolynomial σ R) (c' i);
  φ = HMul.hMul (α := MvPolynomial σ R) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) ψ
⊢ (MvPolynomial.C : (a : R) → MvPolynomial σ R) r ∣ φ
have h₁ : let c' : (σ →₀ ℕ) → R := fun (i : σ →₀ ℕ) ↦ if i ∈ φ.support then C i else 0;
let ψ : MvPolynomial σ R := ∑ i ∈ φ.support, (monomial i : (a : R) → MvPolynomial σ R) (c' i);
∀ (m : σ →₀ ℕ),
  coeff m φ =
    coeff m (HMul.hMul (α := MvPolynomial σ R) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) ψ)
Tactic: classical
      let c' : (σ →₀ ℕ) → R := fun i => if i ∈ φ.support then C i else 0
      let ψ : MvPolynomial σ R := ∑ i ∈ φ.support, monomial i (c' i)
      use ψ
      apply MvPolynomial.ext
      intro i
      simp only [ψ, c', coeff_C_mul, coeff_sum, coeff_monomial, Finset.sum_ite_eq']
      split_ifs with hi
      · rw [hc]
      · rw [notMem_support_iff] at hi
        rwa [mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
r : R
φ : MvPolynomial σ R
C : (i : σ →₀ ℕ) → R
hc : ∀ (i : σ →₀ ℕ), coeff i φ = r * C i
mpr mpr₁ mpr₂ mpr₃ : (MvPolynomial.C : (a : R) → MvPolynomial σ R) r ∣ φ
h :
  let c' : (σ →₀ ℕ) → R := fun (i : σ →₀ ℕ) ↦ if i ∈ φ.support then C i else 0;
  let ψ : MvPolynomial σ R := ∑ i ∈ φ.support, (monomial i : (a : R) → MvPolynomial σ R) (c' i);
  φ = HMul.hMul (α := MvPolynomial σ R) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) ψ
h₁ h₂ :
  let c' : (σ →₀ ℕ) → R := fun (i : σ →₀ ℕ) ↦ if i ∈ φ.support then C i else 0;
  let ψ : MvPolynomial σ R := ∑ i ∈ φ.support, (monomial i : (a : R) → MvPolynomial σ R) (c' i);
  ∀ (i : σ →₀ ℕ),
    coeff i φ =
      coeff i (HMul.hMul (α := MvPolynomial σ R) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) ψ)
⊢ (MvPolynomial.C : (a : R) → MvPolynomial σ R) r ∣ φ
have h₃ : ∀ (i : σ →₀ ℕ), coeff i φ = r * if i ∈ φ.support then if i ∈ φ.support then C i else 0 else 0
Tactic: classical
      let c' : (σ →₀ ℕ) → R := fun i => if i ∈ φ.support then C i else 0
      let ψ : MvPolynomial σ R := ∑ i ∈ φ.support, monomial i (c' i)
      use ψ
      apply MvPolynomial.ext
      intro i
      simp only [ψ, c', coeff_C_mul, coeff_sum, coeff_monomial, Finset.sum_ite_eq']
      split_ifs with hi
      · rw [hc]
      · rw [notMem_support_iff] at hi
        rwa [mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
r : R
φ : MvPolynomial σ R
C : (i : σ →₀ ℕ) → R
hc : ∀ (i : σ →₀ ℕ), coeff i φ = r * C i
mpr mpr₁ mpr₂ mpr₃ : (MvPolynomial.C : (a : R) → MvPolynomial σ R) r ∣ φ
h :
  let c' : (σ →₀ ℕ) → R := fun (i : σ →₀ ℕ) ↦ if i ∈ φ.support then C i else 0;
  let ψ : MvPolynomial σ R := ∑ i ∈ φ.support, (monomial i : (a : R) → MvPolynomial σ R) (c' i);
  φ = HMul.hMul (α := MvPolynomial σ R) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) ψ
h₁ h₂ :
  let c' : (σ →₀ ℕ) → R := fun (i : σ →₀ ℕ) ↦ if i ∈ φ.support then C i else 0;
  let ψ : MvPolynomial σ R := ∑ i ∈ φ.support, (monomial i : (a : R) → MvPolynomial σ R) (c' i);
  ∀ (i : σ →₀ ℕ),
    coeff i φ =
      coeff i (HMul.hMul (α := MvPolynomial σ R) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) ψ)
h₃ : ∀ (i : σ →₀ ℕ), coeff i φ = r * if i ∈ φ.support then if i ∈ φ.support then C i else 0 else 0
⊢ (MvPolynomial.C : (a : R) → MvPolynomial σ R) r ∣ φ
have pos : ∀ (i : σ →₀ ℕ) (hi : i ∈ φ.support), coeff i φ = r * C i
Tactic: classical
      let c' : (σ →₀ ℕ) → R := fun i => if i ∈ φ.support then C i else 0
      let ψ : MvPolynomial σ R := ∑ i ∈ φ.support, monomial i (c' i)
      use ψ
      apply MvPolynomial.ext
      intro i
      simp only [ψ, c', coeff_C_mul, coeff_sum, coeff_monomial, Finset.sum_ite_eq']
      split_ifs with hi
      · rw [hc]
      · rw [notMem_support_iff] at hi
        rwa [mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
r : R
φ : MvPolynomial σ R
C : (i : σ →₀ ℕ) → R
hc : ∀ (i : σ →₀ ℕ), coeff i φ = r * C i
mpr mpr₁ mpr₂ mpr₃ : (MvPolynomial.C : (a : R) → MvPolynomial σ R) r ∣ φ
h :
  let c' : (σ →₀ ℕ) → R := fun (i : σ →₀ ℕ) ↦ if i ∈ φ.support then C i else 0;
  let ψ : MvPolynomial σ R := ∑ i ∈ φ.support, (monomial i : (a : R) → MvPolynomial σ R) (c' i);
  φ = HMul.hMul (α := MvPolynomial σ R) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) ψ
h₁ h₂ :
  let c' : (σ →₀ ℕ) → R := fun (i : σ →₀ ℕ) ↦ if i ∈ φ.support then C i else 0;
  let ψ : MvPolynomial σ R := ∑ i ∈ φ.support, (monomial i : (a : R) → MvPolynomial σ R) (c' i);
  ∀ (i : σ →₀ ℕ),
    coeff i φ =
      coeff i (HMul.hMul (α := MvPolynomial σ R) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) ψ)
h₃ : ∀ (i : σ →₀ ℕ), coeff i φ = r * if i ∈ φ.support then if i ∈ φ.support then C i else 0 else 0
pos : ∀ (i : σ →₀ ℕ) (hi : i ∈ φ.support), coeff i φ = r * C i
⊢ (MvPolynomial.C : (a : R) → MvPolynomial σ R) r ∣ φ
have neg : ∀ (i : σ →₀ ℕ) (hi : i ∉ φ.support), coeff i φ = r * 0
Tactic: classical
      let c' : (σ →₀ ℕ) → R := fun i => if i ∈ φ.support then C i else 0
      let ψ : MvPolynomial σ R := ∑ i ∈ φ.support, monomial i (c' i)
      use ψ
      apply MvPolynomial.ext
      intro i
      simp only [ψ, c', coeff_C_mul, coeff_sum, coeff_monomial, Finset.sum_ite_eq']
      split_ifs with hi
      · rw [hc]
      · rw [notMem_support_iff] at hi
        rwa [mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
n : σ
inst : CommSemiring R
⊢ IsRegular (R := MvPolynomial σ R) (X n)
have suffices : IsLeftRegular (R := MvPolynomial σ R) (X n)
Tactic: suffices IsLeftRegular (X n : MvPolynomial σ R) from
    ⟨this, this.right_of_commute <| Commute.all _⟩
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
n : σ
inst : CommSemiring R
P Q : MvPolynomial σ R
hPQ : X n * P = X n * Q
⊢ P = Q
have a : ∀ (i : σ →₀ ℕ), coeff i P = coeff i Q
Tactic: ext i
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
n : σ
inst : CommSemiring R
P Q : MvPolynomial σ R
hPQ : X n * P = X n * Q
i : σ →₀ ℕ
⊢ coeff i P = coeff i Q
have a : coeff (Finsupp.single n 1 + i) (X n * P) = coeff i Q
Tactic: rw [← coeff_X_mul i n P, hPQ, coeff_X_mul i n Q]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
n : σ
inst : CommSemiring R
P Q : MvPolynomial σ R
hPQ : X n * P = X n * Q
i : σ →₀ ℕ
a : coeff (Finsupp.single n 1 + i) (X n * P) = coeff i Q
⊢ coeff i P = coeff i Q
have a₁ : coeff (Finsupp.single n 1 + i) (X n * Q) = coeff i Q
Tactic: rw [← coeff_X_mul i n P, hPQ, coeff_X_mul i n Q]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
n : σ
inst : CommSemiring R
P Q : MvPolynomial σ R
hPQ : X n * P = X n * Q
i : σ →₀ ℕ
a : coeff (Finsupp.single n 1 + i) (X n * P) = coeff i Q
a₁ : coeff (Finsupp.single n 1 + i) (X n * Q) = coeff i Q
⊢ coeff i P = coeff i Q
have a₂ : coeff i Q = coeff i Q
Tactic: rw [← coeff_X_mul i n P, hPQ, coeff_X_mul i n Q]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
⊢ Subset (α := Finset R) (coeffs.{u, u_1} (σ := σ) 1) {1}
have rw : ∀ (x : σ →₀ ℕ),
  Membership.mem (γ := Finset (σ →₀ ℕ)) (support.{u, u_1} (R := R) 1) x → Membership.mem (γ := Finset R) {1} (coeff x 1)
Tactic: rw [coeffs, Finset.image_subset_iff]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
⊢ Subset (α := Finset R) (coeffs.{u, u_1} (σ := σ) 1) {1}
have rw : Subset (α := Finset R) (Finset.image (fun (m : σ →₀ ℕ) ↦ coeff m 1) (support.{u, u_1} (R := R) 1)) {1}
Tactic: classical
    rw [coeffs, Finset.image_subset_iff]
    simp_all [coeff_one]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
rw : Subset (α := Finset R) (Finset.image (fun (m : σ →₀ ℕ) ↦ coeff m 1) (support.{u, u_1} (R := R) 1)) {1}
⊢ Subset (α := Finset R) (coeffs.{u, u_1} (σ := σ) 1) {1}
have rw₁ : ∀ (x : σ →₀ ℕ),
  Membership.mem (γ := Finset (σ →₀ ℕ)) (support.{u, u_1} (R := R) 1) x → Membership.mem (γ := Finset R) {1} (coeff x 1)
Tactic: classical
    rw [coeffs, Finset.image_subset_iff]
    simp_all [coeff_one]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : Nontrivial R
⊢ Eq (α := Finset R) (coeffs.{u, u_1} (σ := σ) 1) {1}
have apply : Subset (α := Finset R) {1} (coeffs.{u, u_1} (σ := σ) 1)
Tactic: apply Finset.Subset.antisymm coeffs_one
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : Nontrivial R
⊢ Subset (α := Finset R) {1} (coeffs.{u, u_1} (σ := σ) 1)
have simp : ∃ (a : σ →₀ ℕ),
  Membership.mem (γ := Finset (σ →₀ ℕ)) (support.{u, u_1} (R := R) 1) a ∧ Eq.{u + 1} (α := R) (coeff a 1) 1
Tactic: simp only [coeffs, Finset.singleton_subset_iff, Finset.mem_image]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
hz : 0 ∈ p.coeffs
⊢ False
have obtain : ∀ (n : σ →₀ ℕ) (hnsupp : n ∈ p.support) (hn : 0 = coeff n p), False
Tactic: obtain ⟨n, hnsupp, hn⟩ := mem_coeffs_iff.mp hz
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
r : R
⊢ Subset (α := Finset R) (coeffs.{u, u_1} (σ := σ) ((C : (a : R) → MvPolynomial σ R) r)) {r}
have rw : Subset (α := Finset R) (if r = 0 then ∅ else {r}) {r}
Tactic: rw [coeffs_C]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
r : R
⊢ Subset (α := Finset R) (if r = 0 then ∅ else {r}) {r}
have isTrue : r = 0 → Subset (α := Finset R) ∅ {r}
Tactic: split
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
r : R
isTrue : r = 0 → Subset (α := Finset R) ∅ {r}
⊢ Subset (α := Finset R) (if r = 0 then ∅ else {r}) {r}
have isFalse : ¬r = 0 → Subset (α := Finset R) {r} {r}
Tactic: split
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
r : R
⊢ Subset (α := Finset R) (coeffs.{u, u_1} (σ := σ) ((C : (a : R) → MvPolynomial σ R) r)) {r}
have rw : Subset (α := Finset R) (if r = 0 then ∅ else {r}) {r}
Tactic: classical
  rw [coeffs_C]
  split <;> simp
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq R
p q : MvPolynomial σ R
h : Disjoint p.support q.support
⊢ (p + q).coeffs = p.coeffs ∪ q.coeffs
have h₁ : ∀ (r : R), r ∈ (p + q).coeffs ↔ r ∈ p.coeffs ∪ q.coeffs
Tactic: ext r
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq R
p q : MvPolynomial σ R
h : Disjoint p.support q.support
r : R
⊢ r ∈ (p + q).coeffs ↔ r ∈ p.coeffs ∪ q.coeffs
have h₁ : (∃ (n : σ →₀ ℕ), ¬coeff n p + coeff n q = 0 ∧ r = coeff n p + coeff n q) ↔
  (∃ (n : σ →₀ ℕ), ¬coeff n p = 0 ∧ r = coeff n p) ∨ ∃ (n : σ →₀ ℕ), ¬coeff n q = 0 ∧ r = coeff n q
Tactic: simp only [mem_coeffs_iff, mem_support_iff, coeff_add, ne_eq, Finset.mem_union]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (hypothesis)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq R
p q : MvPolynomial σ R
h : Disjoint p.support q.support
r : R
⊢ (∃ (n : σ →₀ ℕ), ¬coeff n p + coeff n q = 0 ∧ r = coeff n p + coeff n q) ↔
    (∃ (n : σ →₀ ℕ), ¬coeff n p = 0 ∧ r = coeff n p) ∨ ∃ (n : σ →₀ ℕ), ¬coeff n q = 0 ∧ r = coeff n q
have hl : ∀ (n : σ →₀ ℕ) (hne : coeff n p ≠ 0), coeff n q = 0
Tactic: have hl (n : σ →₀ ℕ) (hne : p.coeff n ≠ 0) : q.coeff n = 0 :=
    notMem_support_iff.mp <| h.notMem_of_mem_left_finset (mem_support_iff.mpr hne)
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (hypothesis)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq R
p q : MvPolynomial σ R
h : Disjoint p.support q.support
r : R
hl : ∀ (n : σ →₀ ℕ) (hne : coeff n p ≠ 0), coeff n q = 0
⊢ (∃ (n : σ →₀ ℕ), ¬coeff n p + coeff n q = 0 ∧ r = coeff n p + coeff n q) ↔
    (∃ (n : σ →₀ ℕ), ¬coeff n p = 0 ∧ r = coeff n p) ∨ ∃ (n : σ →₀ ℕ), ¬coeff n q = 0 ∧ r = coeff n q
have hr : ∀ (n : σ →₀ ℕ) (hne : coeff n q ≠ 0), coeff n p = 0
Tactic: have hr (n : σ →₀ ℕ) (hne : q.coeff n ≠ 0) : p.coeff n = 0 :=
    notMem_support_iff.mp <| h.notMem_of_mem_right_finset (mem_support_iff.mpr hne)
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq R
p q : MvPolynomial σ R
h_1 : Disjoint p.support q.support
r : R
hl : ∀ (n : σ →₀ ℕ) (hne : coeff n p ≠ 0), coeff n q = 0
hr : ∀ (n : σ →₀ ℕ) (hne : coeff n q ≠ 0), coeff n p = 0
n : σ →₀ ℕ
h : ¬coeff n p + coeff n q = 0
⊢ coeff n p ≠ 0 ∨ coeff n q ≠ 0
have pos : ∀ (hp : coeff n p = 0), coeff n p ≠ 0 ∨ coeff n q ≠ 0
Tactic: by_cases hp : coeff n p = 0
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq R
p q : MvPolynomial σ R
h_1 : Disjoint p.support q.support
r : R
hl : ∀ (n : σ →₀ ℕ) (hne : coeff n p ≠ 0), coeff n q = 0
hr : ∀ (n : σ →₀ ℕ) (hne : coeff n q ≠ 0), coeff n p = 0
n : σ →₀ ℕ
h : ¬coeff n p + coeff n q = 0
pos : ∀ (hp : coeff n p = 0), coeff n p ≠ 0 ∨ coeff n q ≠ 0
⊢ coeff n p ≠ 0 ∨ coeff n q ≠ 0
have neg : ∀ (hp : ¬coeff n p = 0), coeff n p ≠ 0 ∨ coeff n q ≠ 0
Tactic: by_cases hp : coeff n p = 0
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (hypothesis)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq R
p q : MvPolynomial σ R
h : Disjoint p.support q.support
r : R
hl : ∀ (n : σ →₀ ℕ) (hne : coeff n p ≠ 0), coeff n q = 0
hr : ∀ (n : σ →₀ ℕ) (hne : coeff n q ≠ 0), coeff n p = 0
⊢ (∃ (n : σ →₀ ℕ), ¬coeff n p + coeff n q = 0 ∧ r = coeff n p + coeff n q) ↔
    (∃ (n : σ →₀ ℕ), ¬coeff n p = 0 ∧ r = coeff n p) ∨ ∃ (n : σ →₀ ℕ), ¬coeff n q = 0 ∧ r = coeff n q
have hor : ∀ (n : σ →₀ ℕ) (h : ¬coeff n p + coeff n q = 0), coeff n p ≠ 0 ∨ coeff n q ≠ 0
Tactic: have hor (n) (h : ¬coeff n p + coeff n q = 0) : coeff n p ≠ 0 ∨ coeff n q ≠ 0 := by
    by_cases hp : coeff n p = 0 <;> simp_all
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq R
p q : MvPolynomial σ R
h : Disjoint p.support q.support
r : R
hl : ∀ (n : σ →₀ ℕ) (hne : coeff n p ≠ 0), coeff n q = 0
hr : ∀ (n : σ →₀ ℕ) (hne : coeff n q ≠ 0), coeff n p = 0
hor : ∀ (n : σ →₀ ℕ) (h : ¬coeff n p + coeff n q = 0), coeff n p ≠ 0 ∨ coeff n q ≠ 0
⊢ (∃ (n : σ →₀ ℕ), ¬coeff n p + coeff n q = 0 ∧ r = coeff n p + coeff n q) ↔
    (∃ (n : σ →₀ ℕ), ¬coeff n p = 0 ∧ r = coeff n p) ∨ ∃ (n : σ →₀ ℕ), ¬coeff n q = 0 ∧ r = coeff n q
have h₁ : (∃ (n : σ →₀ ℕ), ¬coeff n p + coeff n q = 0 ∧ r = coeff n p + coeff n q) →
  ∀ (n : σ →₀ ℕ) (hn1 : ¬coeff n p + coeff n q = 0) (hn2 : r = coeff n p + coeff n q),
    (∃ (n : σ →₀ ℕ), ¬coeff n p = 0 ∧ r = coeff n p) ∨ ∃ (n : σ →₀ ℕ), ¬coeff n q = 0 ∧ r = coeff n q
Tactic: refine ⟨fun ⟨n, hn1, hn2⟩ ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq R
p q : MvPolynomial σ R
h : Disjoint p.support q.support
r : R
hl : ∀ (n : σ →₀ ℕ) (hne : coeff n p ≠ 0), coeff n q = 0
hr : ∀ (n : σ →₀ ℕ) (hne : coeff n q ≠ 0), coeff n p = 0
hor : ∀ (n : σ →₀ ℕ) (h : ¬coeff n p + coeff n q = 0), coeff n p ≠ 0 ∨ coeff n q ≠ 0
h₁ :
  (∃ (n : σ →₀ ℕ), ¬coeff n p + coeff n q = 0 ∧ r = coeff n p + coeff n q) →
    ∀ (n : σ →₀ ℕ) (hn1 : ¬coeff n p + coeff n q = 0) (hn2 : r = coeff n p + coeff n q),
      (∃ (n : σ →₀ ℕ), ¬coeff n p = 0 ∧ r = coeff n p) ∨ ∃ (n : σ →₀ ℕ), ¬coeff n q = 0 ∧ r = coeff n q
⊢ (∃ (n : σ →₀ ℕ), ¬coeff n p + coeff n q = 0 ∧ r = coeff n p + coeff n q) ↔
    (∃ (n : σ →₀ ℕ), ¬coeff n p = 0 ∧ r = coeff n p) ∨ ∃ (n : σ →₀ ℕ), ¬coeff n q = 0 ∧ r = coeff n q
have h₂ : ((∃ (n : σ →₀ ℕ), ¬coeff n p = 0 ∧ r = coeff n p) ∨ ∃ (n : σ →₀ ℕ), ¬coeff n q = 0 ∧ r = coeff n q) →
  ∃ (n : σ →₀ ℕ), ¬coeff n p + coeff n q = 0 ∧ r = coeff n p + coeff n q
Tactic: refine ⟨fun ⟨n, hn1, hn2⟩ ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq R
p q : MvPolynomial σ R
h : Disjoint p.support q.support
r : R
hl : ∀ (n : σ →₀ ℕ) (hne : coeff n p ≠ 0), coeff n q = 0
hr : ∀ (n : σ →₀ ℕ) (hne : coeff n q ≠ 0), coeff n p = 0
hor : ∀ (n : σ →₀ ℕ) (h : ¬coeff n p + coeff n q = 0), coeff n p ≠ 0 ∨ coeff n q ≠ 0
h_1 : ∃ (n : σ →₀ ℕ), ¬coeff n p + coeff n q = 0 ∧ r = coeff n p + coeff n q
n : σ →₀ ℕ
hn1 : ¬coeff n p + coeff n q = 0
hn2 : r = coeff n p + coeff n q
⊢ (∃ (n : σ →₀ ℕ), ¬coeff n p = 0 ∧ r = coeff n p) ∨ ∃ (n : σ →₀ ℕ), ¬coeff n q = 0 ∧ r = coeff n q
have h₁ : ∀ (h : coeff n p ≠ 0), (∃ (n : σ →₀ ℕ), ¬coeff n p = 0 ∧ r = coeff n p) ∨ ∃ (n : σ →₀ ℕ), ¬coeff n q = 0 ∧ r = coeff n q
Tactic: obtain (h | h) := hor n hn1
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq R
p q : MvPolynomial σ R
h : Disjoint p.support q.support
r : R
hl : ∀ (n : σ →₀ ℕ) (hne : coeff n p ≠ 0), coeff n q = 0
hr : ∀ (n : σ →₀ ℕ) (hne : coeff n q ≠ 0), coeff n p = 0
hor : ∀ (n : σ →₀ ℕ) (h : ¬coeff n p + coeff n q = 0), coeff n p ≠ 0 ∨ coeff n q ≠ 0
h_1 : ∃ (n : σ →₀ ℕ), ¬coeff n p + coeff n q = 0 ∧ r = coeff n p + coeff n q
n : σ →₀ ℕ
hn1 : ¬coeff n p + coeff n q = 0
hn2 : r = coeff n p + coeff n q
h₁ :
  ∀ (h : coeff n p ≠ 0),
    (∃ (n : σ →₀ ℕ), ¬coeff n p = 0 ∧ r = coeff n p) ∨ ∃ (n : σ →₀ ℕ), ¬coeff n q = 0 ∧ r = coeff n q
⊢ (∃ (n : σ →₀ ℕ), ¬coeff n p = 0 ∧ r = coeff n p) ∨ ∃ (n : σ →₀ ℕ), ¬coeff n q = 0 ∧ r = coeff n q
have h₂ : ∀ (h : coeff n q ≠ 0), (∃ (n : σ →₀ ℕ), ¬coeff n p = 0 ∧ r = coeff n p) ∨ ∃ (n : σ →₀ ℕ), ¬coeff n q = 0 ∧ r = coeff n q
Tactic: obtain (h | h) := hor n hn1
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
d : σ →₀ ℕ
r : R
⊢ (constantCoeff : (a : MvPolynomial σ R) → R) ((monomial d : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) =
    if d = 0 then r else 0
have rw : coeff.{u, u_1} (σ := σ) 0 ((monomial d : (a : R) → MvPolynomial σ R) r) = if d = 0 then r else 0
Tactic: rw [constantCoeff_eq, coeff_monomial]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
d : σ →₀ ℕ
r : R
rw : coeff.{u, u_1} (σ := σ) 0 ((monomial d : (a : R) → MvPolynomial σ R) r) = if d = 0 then r else 0
⊢ (constantCoeff : (a : MvPolynomial σ R) → R) ((monomial d : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) =
    if d = 0 then r else 0
have rw₁ : (if d = 0 then r else 0) = if d = 0 then r else 0
Tactic: rw [constantCoeff_eq, coeff_monomial]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
⊢ Eq (α := R →+* R) (RingHom.comp (β := MvPolynomial σ R) constantCoeff C) (RingHom.id R)
have a : ∀ (x : R),
  Eq (α := R) ((RingHom.comp (β := MvPolynomial σ R) constantCoeff C : (a : R) → R) x : R)
    ((RingHom.id R : (a : R) → R) x : R)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u_2
S : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Module R S
M : Submodule R S
i : σ →₀ ℕ
x : S
⊢ Membership.mem (α := MvPolynomial σ S) (coeffsIn σ M)
      ((monomial i : (a : S) → MvPolynomial σ S) x : MvPolynomial σ S) ↔
    x ∈ M
have simp : (∀ (i_1 : σ →₀ ℕ), (if i = i_1 then x else 0) ∈ M) ↔ x ∈ M
Tactic: simp only [mem_coeffsIn, coeff_monomial]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u_2
S : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Module R S
M : Submodule R S
i : σ →₀ ℕ
x : S
hs : x ∈ M
j : σ →₀ ℕ
⊢ (if i = j then x else 0) ∈ M
have isTrue : i = j → x ∈ M
Tactic: split
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u_2
S : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Module R S
M : Submodule R S
i : σ →₀ ℕ
x : S
hs : x ∈ M
j : σ →₀ ℕ
isTrue : i = j → x ∈ M
⊢ (if i = j then x else 0) ∈ M
have isFalse : ¬i = j → 0 ∈ M
Tactic: split
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u_2
S : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Module R S
M : Submodule R S
i : σ →₀ ℕ
x : S
⊢ Membership.mem (α := MvPolynomial σ S) (coeffsIn σ M)
      ((monomial i : (a : S) → MvPolynomial σ S) x : MvPolynomial σ S) ↔
    x ∈ M
have simp : (∀ (i_1 : σ →₀ ℕ), (if i = i_1 then x else 0) ∈ M) ↔ x ∈ M
Tactic: classical
  simp only [mem_coeffsIn, coeff_monomial]
  exact ⟨fun h ↦ by simpa using h i, fun hs j ↦ by split <;> simp [hs]⟩
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u_2
S : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Module R S
M : Submodule R S
p : MvPolynomial σ S
i : σ →₀ ℕ
⊢ p * (monomial i : (a : S) → MvPolynomial σ S) 1 ∈ coeffsIn σ M ↔ p ∈ coeffsIn σ M
have simp : (∀ (i_1 : σ →₀ ℕ), (if i ≤ i_1 then coeff (i_1 - i) p * 1 else 0) ∈ M) ↔ ∀ (i : σ →₀ ℕ), coeff i p ∈ M
Tactic: simp only [mem_coeffsIn, coeff_mul_monomial']
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u_2
S : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Module R S
M : Submodule R S
p : MvPolynomial σ S
i : σ →₀ ℕ
⊢ (∀ (i_1 : σ →₀ ℕ), (if i ≤ i_1 then coeff (i_1 - i) p * 1 else 0) ∈ M) ↔ ∀ (i : σ →₀ ℕ), coeff i p ∈ M
have mp : (∀ (i_1 : σ →₀ ℕ), (if i ≤ i_1 then coeff (i_1 - i) p * 1 else 0) ∈ M) → ∀ (i : σ →₀ ℕ), coeff i p ∈ M
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u_2
S : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Module R S
M : Submodule R S
p : MvPolynomial σ S
i : σ →₀ ℕ
mp : (∀ (i_1 : σ →₀ ℕ), (if i ≤ i_1 then coeff (i_1 - i) p * 1 else 0) ∈ M) → ∀ (i : σ →₀ ℕ), coeff i p ∈ M
⊢ (∀ (i_1 : σ →₀ ℕ), (if i ≤ i_1 then coeff (i_1 - i) p * 1 else 0) ∈ M) ↔ ∀ (i : σ →₀ ℕ), coeff i p ∈ M
have mpr : (∀ (i : σ →₀ ℕ), coeff i p ∈ M) → ∀ (i_1 : σ →₀ ℕ), (if i ≤ i_1 then coeff (i_1 - i) p * 1 else 0) ∈ M
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u_2
S : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Module R S
M : Submodule R S
p : MvPolynomial σ S
i_1 : σ →₀ ℕ
hp : ∀ (i : σ →₀ ℕ), coeff i p ∈ M
i : σ →₀ ℕ
⊢ (if i_1 ≤ i then coeff (i - i_1) p * 1 else 0) ∈ M
have mpr : i_1 ≤ i → coeff (i - i_1) p * 1 ∈ M
Tactic: split
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u_2
S : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Module R S
M : Submodule R S
p : MvPolynomial σ S
i_1 : σ →₀ ℕ
hp : ∀ (i : σ →₀ ℕ), coeff i p ∈ M
i : σ →₀ ℕ
mpr : i_1 ≤ i → coeff (i - i_1) p * 1 ∈ M
⊢ (if i_1 ≤ i then coeff (i - i_1) p * 1 else 0) ∈ M
have mpr₁ : ¬i_1 ≤ i → 0 ∈ M
Tactic: split