awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
p : MvPolynomial σ R
n : σ →₀ ℕ
a : R
ha : a ≠ 0
m : σ →₀ ℕ
r : MvPolynomial σ R
hmn : m ≤ n
h : p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
b : R
hb : b ∣ a
hr : r = (C : (a : R) → MvPolynomial σ R) b
⊢ ∃ (b : R), m ≤ n ∧ b ∣ a ∧ p = (monomial m : (a : R) → MvPolynomial σ R) b
have right : p = (monomial m : (a : R) → MvPolynomial σ R) b
Tactic: use b, hmn, hb
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
p : MvPolynomial σ R
n : σ →₀ ℕ
a : R
ha : a ≠ 0
m : σ →₀ ℕ
r : MvPolynomial σ R
hmn : m ≤ n
h : p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
b : R
hb : b ∣ a
hr : r = (C : (a : R) → MvPolynomial σ R) b
⊢ p = (monomial m : (a : R) → MvPolynomial σ R) b
have right : (monomial m : (a : R) → MvPolynomial σ R) 1 * r = (monomial m : (a : R) → MvPolynomial σ R) b
Tactic: rw [h, mul_comm, hr, C_mul_monomial, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
p : MvPolynomial σ R
n : σ →₀ ℕ
a : R
ha : a ≠ 0
m : σ →₀ ℕ
r : MvPolynomial σ R
hmn : m ≤ n
h : p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
b : R
hb : b ∣ a
hr : r = (C : (a : R) → MvPolynomial σ R) b
right : (monomial m : (a : R) → MvPolynomial σ R) 1 * r = (monomial m : (a : R) → MvPolynomial σ R) b
⊢ p = (monomial m : (a : R) → MvPolynomial σ R) b
have right₁ : r * (monomial m : (a : R) → MvPolynomial σ R) 1 = (monomial m : (a : R) → MvPolynomial σ R) b
Tactic: rw [h, mul_comm, hr, C_mul_monomial, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
p : MvPolynomial σ R
n : σ →₀ ℕ
a : R
ha : a ≠ 0
m : σ →₀ ℕ
r : MvPolynomial σ R
hmn : m ≤ n
h : p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
b : R
hb : b ∣ a
hr : r = (C : (a : R) → MvPolynomial σ R) b
right : (monomial m : (a : R) → MvPolynomial σ R) 1 * r = (monomial m : (a : R) → MvPolynomial σ R) b
right₁ : r * (monomial m : (a : R) → MvPolynomial σ R) 1 = (monomial m : (a : R) → MvPolynomial σ R) b
⊢ p = (monomial m : (a : R) → MvPolynomial σ R) b
have right₂ : HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) b : MvPolynomial σ R)
    ((monomial m : (a : R) → MvPolynomial σ R) 1 : MvPolynomial σ R) =
  (monomial m : (a : R) → MvPolynomial σ R) b
Tactic: rw [h, mul_comm, hr, C_mul_monomial, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
p : MvPolynomial σ R
n : σ →₀ ℕ
a : R
ha : a ≠ 0
m : σ →₀ ℕ
r : MvPolynomial σ R
hmn : m ≤ n
h : p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
b : R
hb : b ∣ a
hr : r = (C : (a : R) → MvPolynomial σ R) b
right : (monomial m : (a : R) → MvPolynomial σ R) 1 * r = (monomial m : (a : R) → MvPolynomial σ R) b
right₁ : r * (monomial m : (a : R) → MvPolynomial σ R) 1 = (monomial m : (a : R) → MvPolynomial σ R) b
right₂ :
  HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) b : MvPolynomial σ R)
      ((monomial m : (a : R) → MvPolynomial σ R) 1 : MvPolynomial σ R) =
    (monomial m : (a : R) → MvPolynomial σ R) b
⊢ p = (monomial m : (a : R) → MvPolynomial σ R) b
have right₃ : Eq (α := MvPolynomial σ R) ((monomial m : (a : R) → MvPolynomial σ R) (b * 1) : MvPolynomial σ R)
  ((monomial m : (a : R) → MvPolynomial σ R) b : MvPolynomial σ R)
Tactic: rw [h, mul_comm, hr, C_mul_monomial, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
p : MvPolynomial σ R
n : σ →₀ ℕ
a : R
ha : a ≠ 0
m : σ →₀ ℕ
r : MvPolynomial σ R
hmn : m ≤ n
h : p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
b : R
hb : b ∣ a
hr : r = (C : (a : R) → MvPolynomial σ R) b
right : (monomial m : (a : R) → MvPolynomial σ R) 1 * r = (monomial m : (a : R) → MvPolynomial σ R) b
right₁ : r * (monomial m : (a : R) → MvPolynomial σ R) 1 = (monomial m : (a : R) → MvPolynomial σ R) b
right₂ :
  HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) b : MvPolynomial σ R)
      ((monomial m : (a : R) → MvPolynomial σ R) 1 : MvPolynomial σ R) =
    (monomial m : (a : R) → MvPolynomial σ R) b
right₃ :
  Eq (α := MvPolynomial σ R) ((monomial m : (a : R) → MvPolynomial σ R) (b * 1) : MvPolynomial σ R)
    ((monomial m : (a : R) → MvPolynomial σ R) b : MvPolynomial σ R)
⊢ p = (monomial m : (a : R) → MvPolynomial σ R) b
have right₄ : Eq (α := MvPolynomial σ R) ((monomial m : (a : R) → MvPolynomial σ R) b : MvPolynomial σ R)
  ((monomial m : (a : R) → MvPolynomial σ R) b : MvPolynomial σ R)
Tactic: rw [h, mul_comm, hr, C_mul_monomial, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
p : MvPolynomial σ R
n : σ →₀ ℕ
a : R
ha : a ≠ 0
m : σ →₀ ℕ
b : R
hmn : m ≤ n
hb : b ∣ a
h : p = (monomial m : (a : R) → MvPolynomial σ R) b
⊢ ∃ (r : MvPolynomial σ R),
    m ≤ n ∧ r ∣ (C : (a : R) → MvPolynomial σ R) a ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
have right : p =
  HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
    ((monomial m : (a : R) → MvPolynomial σ R) 1 : MvPolynomial σ R)
    ((C : (a : R) → MvPolynomial σ R) b : MvPolynomial σ R)
Tactic: use C b, hmn, map_dvd C hb
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
p : MvPolynomial σ R
n : σ →₀ ℕ
a : R
ha : a ≠ 0
m : σ →₀ ℕ
b : R
hmn : m ≤ n
hb : b ∣ a
h : p = (monomial m : (a : R) → MvPolynomial σ R) b
⊢ p =
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
      ((monomial m : (a : R) → MvPolynomial σ R) 1 : MvPolynomial σ R)
      ((C : (a : R) → MvPolynomial σ R) b : MvPolynomial σ R)
have right : p =
  HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) b : MvPolynomial σ R)
    ((monomial m : (a : R) → MvPolynomial σ R) 1 : MvPolynomial σ R)
Tactic: rwa [mul_comm, C_mul_monomial, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
p : MvPolynomial σ R
n : σ →₀ ℕ
a : R
ha : a ≠ 0
m : σ →₀ ℕ
b : R
hmn : m ≤ n
hb : b ∣ a
h : p = (monomial m : (a : R) → MvPolynomial σ R) b
right :
  p =
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) b : MvPolynomial σ R)
      ((monomial m : (a : R) → MvPolynomial σ R) 1 : MvPolynomial σ R)
⊢ p =
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
      ((monomial m : (a : R) → MvPolynomial σ R) 1 : MvPolynomial σ R)
      ((C : (a : R) → MvPolynomial σ R) b : MvPolynomial σ R)
have right₁ : p = (monomial m : (a : R) → MvPolynomial σ R) (b * 1)
Tactic: rwa [mul_comm, C_mul_monomial, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
p : MvPolynomial σ R
n : σ →₀ ℕ
⊢ p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 ↔
    ∃ (m : σ →₀ ℕ) (u : R), m ≤ n ∧ IsUnit u ∧ p = (monomial m : (a : R) → MvPolynomial σ R) u
have inl : ∀ (hR : Subsingleton R),
  p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 ↔
    ∃ (m : σ →₀ ℕ) (u : R), m ≤ n ∧ IsUnit u ∧ p = (monomial m : (a : R) → MvPolynomial σ R) u
Tactic: rcases subsingleton_or_nontrivial R with hR | hR
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
p : MvPolynomial σ R
n : σ →₀ ℕ
inl :
  ∀ (hR : Subsingleton R),
    p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 ↔
      ∃ (m : σ →₀ ℕ) (u : R), m ≤ n ∧ IsUnit u ∧ p = (monomial m : (a : R) → MvPolynomial σ R) u
⊢ p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 ↔
    ∃ (m : σ →₀ ℕ) (u : R), m ≤ n ∧ IsUnit u ∧ p = (monomial m : (a : R) → MvPolynomial σ R) u
have inr : ∀ (hR : Nontrivial R),
  p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 ↔
    ∃ (m : σ →₀ ℕ) (u : R), m ≤ n ∧ IsUnit u ∧ p = (monomial m : (a : R) → MvPolynomial σ R) u
Tactic: rcases subsingleton_or_nontrivial R with hR | hR
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
p : MvPolynomial σ R
n : σ →₀ ℕ
hR : Subsingleton R
⊢ p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 ↔
    ∃ (m : σ →₀ ℕ) (u : R), m ≤ n ∧ IsUnit u ∧ p = (monomial m : (a : R) → MvPolynomial σ R) u
have inl : ∃ (m : σ →₀ ℕ), m ≤ n
Tactic: suffices ∃ m, m ≤ n by simpa [Subsingleton.elim _ p]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
p : MvPolynomial σ R
n : σ →₀ ℕ
hR : Subsingleton R
w : σ →₀ ℕ
⊢ ∃ (m : σ →₀ ℕ), m ≤ n
have h : n ≤ n
Tactic: use n
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
p : MvPolynomial σ R
n : σ →₀ ℕ
hR : Nontrivial R
⊢ p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 ↔
    ∃ (m : σ →₀ ℕ) (u : R), m ≤ n ∧ IsUnit u ∧ p = (monomial m : (a : R) → MvPolynomial σ R) u
have inr : (∃ (m : σ →₀ ℕ) (b : R), m ≤ n ∧ b ∣ 1 ∧ p = (monomial m : (a : R) → MvPolynomial σ R) b) ↔
  ∃ (m : σ →₀ ℕ) (u : R), m ≤ n ∧ IsUnit u ∧ p = (monomial m : (a : R) → MvPolynomial σ R) u
Tactic: rw [dvd_monomial_iff_exists (one_ne_zero' R)]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
p : MvPolynomial σ R
n : σ →₀ ℕ
hR : Nontrivial R
⊢ (∃ (m : σ →₀ ℕ) (b : R), m ≤ n ∧ b ∣ 1 ∧ p = (monomial m : (a : R) → MvPolynomial σ R) b) ↔
    ∃ (m : σ →₀ ℕ) (u : R), m ≤ n ∧ IsUnit u ∧ p = (monomial m : (a : R) → MvPolynomial σ R) u
have inr : ∀ (a : σ →₀ ℕ),
  (∃ (b : R), a ≤ n ∧ b ∣ 1 ∧ p = (monomial a : (a : R) → MvPolynomial σ R) b) ↔
    ∃ (u : R), a ≤ n ∧ IsUnit u ∧ p = (monomial a : (a : R) → MvPolynomial σ R) u
Tactic: apply exists_congr
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
p : MvPolynomial σ R
i : σ
r : R
hr : r ≠ 0
⊢ p ∣ HSMul.hSMul (β := MvPolynomial σ R) r (X i) ↔
    ∃ (s : R), s ∣ r ∧ (p = (C : (a : R) → MvPolynomial σ R) s ∨ p = HSMul.hSMul (β := MvPolynomial σ R) s (X i))
have rw : (∃ (b : R), ∃ a ≤ Finsupp.single i 1, b ∣ r ∧ p = (monomial a : (a : R) → MvPolynomial σ R) b) ↔
  ∃ (s : R),
    s ∣ r ∧
      (p = (C : (a : R) → MvPolynomial σ R) s ∨
        p = HSMul.hSMul (β := MvPolynomial σ R) s ((monomial (Finsupp.single i 1) : (a : R) → MvPolynomial σ R) 1))
Tactic: rw [X, smul_monomial, smul_eq_mul, mul_one, dvd_monomial_iff_exists hr, exists_comm]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
p : MvPolynomial σ R
i : σ
r : R
hr : r ≠ 0
⊢ (∃ (b : R), ∃ a ≤ Finsupp.single i 1, b ∣ r ∧ p = (monomial a : (a : R) → MvPolynomial σ R) b) ↔
    ∃ (s : R),
      s ∣ r ∧
        (p = (C : (a : R) → MvPolynomial σ R) s ∨
          p = HSMul.hSMul (β := MvPolynomial σ R) s ((monomial (Finsupp.single i 1) : (a : R) → MvPolynomial σ R) 1))
have h : ∀ (a : R),
  (∃ a_1 ≤ Finsupp.single i 1, a ∣ r ∧ p = (monomial a_1 : (a : R) → MvPolynomial σ R) a) ↔
    a ∣ r ∧
      (p = (C : (a : R) → MvPolynomial σ R) a ∨
        p = HSMul.hSMul (β := MvPolynomial σ R) a ((monomial (Finsupp.single i 1) : (a : R) → MvPolynomial σ R) 1))
Tactic: apply exists_congr
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
p : MvPolynomial σ R
i : σ
r : R
hr : r ≠ 0
b : R
⊢ (∃ a ≤ Finsupp.single i 1, b ∣ r ∧ p = (monomial a : (a : R) → MvPolynomial σ R) b) ↔
    b ∣ r ∧
      (p = (C : (a : R) → MvPolynomial σ R) b ∨
        p = HSMul.hSMul (β := MvPolynomial σ R) b ((monomial (Finsupp.single i 1) : (a : R) → MvPolynomial σ R) 1))
have h : (∃ a ≤ Finsupp.single i 1, b ∣ r ∧ p = (monomial a : (a : R) → MvPolynomial σ R) b) →
  b ∣ r ∧
    (p = (C : (a : R) → MvPolynomial σ R) b ∨
      p = HSMul.hSMul (β := MvPolynomial σ R) b ((monomial (Finsupp.single i 1) : (a : R) → MvPolynomial σ R) 1))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
p : MvPolynomial σ R
i : σ
r : R
hr : r ≠ 0
b : R
h :
  (∃ a ≤ Finsupp.single i 1, b ∣ r ∧ p = (monomial a : (a : R) → MvPolynomial σ R) b) →
    b ∣ r ∧
      (p = (C : (a : R) → MvPolynomial σ R) b ∨
        p = HSMul.hSMul (β := MvPolynomial σ R) b ((monomial (Finsupp.single i 1) : (a : R) → MvPolynomial σ R) 1))
⊢ (∃ a ≤ Finsupp.single i 1, b ∣ r ∧ p = (monomial a : (a : R) → MvPolynomial σ R) b) ↔
    b ∣ r ∧
      (p = (C : (a : R) → MvPolynomial σ R) b ∨
        p = HSMul.hSMul (β := MvPolynomial σ R) b ((monomial (Finsupp.single i 1) : (a : R) → MvPolynomial σ R) 1))
have h₁ : b ∣ r ∧
    (p = (C : (a : R) → MvPolynomial σ R) b ∨
      p = HSMul.hSMul (β := MvPolynomial σ R) b ((monomial (Finsupp.single i 1) : (a : R) → MvPolynomial σ R) 1)) →
  ∃ a ≤ Finsupp.single i 1, b ∣ r ∧ p = (monomial a : (a : R) → MvPolynomial σ R) b
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
i : σ
r : R
hr : r ≠ 0
b : R
m : σ →₀ ℕ
hmn : m ≤ Finsupp.single i 1
hb : b ∣ r
⊢ b ∣ r ∧
    (Eq (α := MvPolynomial σ R) ((monomial m : (a : R) → MvPolynomial σ R) b : MvPolynomial σ R)
        ((C : (a : R) → MvPolynomial σ R) b : MvPolynomial σ R) ∨
      (monomial m : (a : R) → MvPolynomial σ R) b =
        HSMul.hSMul (β := MvPolynomial σ R) b ((monomial (Finsupp.single i 1) : (a : R) → MvPolynomial σ R) 1))
have h : Eq (α := MvPolynomial σ R) ((monomial m : (a : R) → MvPolynomial σ R) b : MvPolynomial σ R)
    ((C : (a : R) → MvPolynomial σ R) b : MvPolynomial σ R) ∨
  (monomial m : (a : R) → MvPolynomial σ R) b =
    HSMul.hSMul (β := MvPolynomial σ R) b ((monomial (Finsupp.single i 1) : (a : R) → MvPolynomial σ R) 1)
Tactic: simp only [hb, true_and]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
i : σ
r : R
hr : r ≠ 0
b : R
m : σ →₀ ℕ
hmn : m ≤ Finsupp.single i 1
hb : b ∣ r
this : m = 0 ∨ m = Finsupp.single i 1
⊢ Eq (α := MvPolynomial σ R) ((monomial m : (a : R) → MvPolynomial σ R) b : MvPolynomial σ R)
      ((C : (a : R) → MvPolynomial σ R) b : MvPolynomial σ R) ∨
    (monomial m : (a : R) → MvPolynomial σ R) b =
      HSMul.hSMul (β := MvPolynomial σ R) b ((monomial (Finsupp.single i 1) : (a : R) → MvPolynomial σ R) 1)
have f : m = 0 →
  Eq (α := MvPolynomial σ R) ((monomial m : (a : R) → MvPolynomial σ R) b : MvPolynomial σ R)
    ((C : (a : R) → MvPolynomial σ R) b : MvPolynomial σ R)
Tactic: apply this.imp
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
i : σ
r : R
hr : r ≠ 0
b : R
m : σ →₀ ℕ
hmn : m ≤ Finsupp.single i 1
hb : b ∣ r
this : m = 0 ∨ m = Finsupp.single i 1
f :
  m = 0 →
    Eq (α := MvPolynomial σ R) ((monomial m : (a : R) → MvPolynomial σ R) b : MvPolynomial σ R)
      ((C : (a : R) → MvPolynomial σ R) b : MvPolynomial σ R)
⊢ Eq (α := MvPolynomial σ R) ((monomial m : (a : R) → MvPolynomial σ R) b : MvPolynomial σ R)
      ((C : (a : R) → MvPolynomial σ R) b : MvPolynomial σ R) ∨
    (monomial m : (a : R) → MvPolynomial σ R) b =
      HSMul.hSMul (β := MvPolynomial σ R) b ((monomial (Finsupp.single i 1) : (a : R) → MvPolynomial σ R) 1)
have g : m = Finsupp.single i 1 →
  (monomial m : (a : R) → MvPolynomial σ R) b =
    HSMul.hSMul (β := MvPolynomial σ R) b ((monomial (Finsupp.single i 1) : (a : R) → MvPolynomial σ R) 1)
Tactic: apply this.imp
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
i : σ
r : R
hr : r ≠ 0
b : R
m : σ →₀ ℕ
hmn : m ≤ Finsupp.single i 1
hb : b ∣ r
⊢ Eq (α := MvPolynomial σ R) ((monomial m : (a : R) → MvPolynomial σ R) b : MvPolynomial σ R)
      ((C : (a : R) → MvPolynomial σ R) b : MvPolynomial σ R) ∨
    (monomial m : (a : R) → MvPolynomial σ R) b =
      HSMul.hSMul (β := MvPolynomial σ R) b ((monomial (Finsupp.single i 1) : (a : R) → MvPolynomial σ R) 1)
have h : m = 0 ∨ m = Finsupp.single i 1
Tactic: suffices m = 0 ∨ m = Finsupp.single i 1 by
      apply this.imp <;> simp +contextual [smul_monomial, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
i : σ
r : R
hr : r ≠ 0
b : R
m : σ →₀ ℕ
hmn : m ≤ Finsupp.single i 1
hb : b ∣ r
⊢ m = 0 ∨ m = Finsupp.single i 1
have pos : ∀ (hm : Eq (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) (0 : ℕ)), m = 0 ∨ m = Finsupp.single i 1
Tactic: by_cases hm : m i = 0
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
i : σ
r : R
hr : r ≠ 0
b : R
m : σ →₀ ℕ
hmn : m ≤ Finsupp.single i 1
hb : b ∣ r
pos : ∀ (hm : Eq (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) (0 : ℕ)), m = 0 ∨ m = Finsupp.single i 1
⊢ m = 0 ∨ m = Finsupp.single i 1
have neg : ∀ (hm : ¬Eq (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) (0 : ℕ)), m = 0 ∨ m = Finsupp.single i 1
Tactic: by_cases hm : m i = 0
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
i : σ
r : R
hr : r ≠ 0
b : R
m : σ →₀ ℕ
hmn : m ≤ Finsupp.single i 1
hb : b ∣ r
hm : Eq (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
⊢ m = 0 ∨ m = Finsupp.single i 1
have pos : m = 0
Tactic: left
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
i : σ
r : R
hr : r ≠ 0
b : R
m : σ →₀ ℕ
hmn : m ≤ Finsupp.single i 1
hb : b ∣ r
hm : Eq (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
⊢ m = 0
have pos : ∀ (j : σ), Eq (α := ℕ) ((m : (a : σ) → ℕ) j : ℕ) ((0 : (a : σ) → ℕ) j : ℕ)
Tactic: ext j
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
i : σ
r : R
hr : r ≠ 0
b : R
m : σ →₀ ℕ
hmn : m ≤ Finsupp.single i 1
hb : b ∣ r
hm : Eq (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
j : σ
⊢ Eq (α := ℕ) ((m : (a : σ) → ℕ) j : ℕ) ((0 : (a : σ) → ℕ) j : ℕ)
have pos : LE.le (α := ℕ) ((m : (a : σ) → ℕ) j : ℕ) (0 : ℕ)
Tactic: simp only [Finsupp.coe_zero, Pi.zero_apply, ← Nat.le_zero]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
i : σ
r : R
hr : r ≠ 0
b : R
m : σ →₀ ℕ
hmn : m ≤ Finsupp.single i 1
hb : b ∣ r
hm : Eq (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
j : σ
⊢ LE.le (α := ℕ) ((m : (a : σ) → ℕ) j : ℕ) (0 : ℕ)
have pos : ∀ (hj : j = i), LE.le (α := ℕ) ((m : (a : σ) → ℕ) j : ℕ) (0 : ℕ)
Tactic: by_cases hj : j = i
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
i : σ
r : R
hr : r ≠ 0
b : R
m : σ →₀ ℕ
hmn : m ≤ Finsupp.single i 1
hb : b ∣ r
hm : Eq (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
j : σ
pos : ∀ (hj : j = i), LE.le (α := ℕ) ((m : (a : σ) → ℕ) j : ℕ) (0 : ℕ)
⊢ LE.le (α := ℕ) ((m : (a : σ) → ℕ) j : ℕ) (0 : ℕ)
have neg : ∀ (hj : ¬j = i), LE.le (α := ℕ) ((m : (a : σ) → ℕ) j : ℕ) (0 : ℕ)
Tactic: by_cases hj : j = i
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
i : σ
r : R
hr : r ≠ 0
b : R
m : σ →₀ ℕ
hmn : m ≤ Finsupp.single i 1
hb : b ∣ r
hm : Eq (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
j : σ
hj : j = i
⊢ LE.le (α := ℕ) ((m : (a : σ) → ℕ) j : ℕ) (0 : ℕ)
have pos : LE.le (α := ℕ) ((m : (a : σ) → ℕ) j : ℕ) ((m : (a : σ) → ℕ) i : ℕ)
Tactic: rw [← hm, hj]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
i : σ
r : R
hr : r ≠ 0
b : R
m : σ →₀ ℕ
hmn : m ≤ Finsupp.single i 1
hb : b ∣ r
hm : Eq (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
j : σ
hj : j = i
pos : LE.le (α := ℕ) ((m : (a : σ) → ℕ) j : ℕ) ((m : (a : σ) → ℕ) i : ℕ)
⊢ LE.le (α := ℕ) ((m : (a : σ) → ℕ) j : ℕ) (0 : ℕ)
have pos₁ : LE.le (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) ((m : (a : σ) → ℕ) i : ℕ)
Tactic: rw [← hm, hj]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
i : σ
r : R
hr : r ≠ 0
b : R
m : σ →₀ ℕ
hmn : m ≤ Finsupp.single i 1
hb : b ∣ r
hm : ¬Eq (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
⊢ m = 0 ∨ m = Finsupp.single i 1
have neg : m = Finsupp.single i 1
Tactic: right
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
i : σ
r : R
hr : r ≠ 0
b : R
m : σ →₀ ℕ
hmn : m ≤ Finsupp.single i 1
hb : b ∣ r
hm : ¬Eq (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
⊢ m = Finsupp.single i 1
have neg : ∀ (j : σ), Eq (α := ℕ) ((m : (a : σ) → ℕ) j : ℕ) ((Finsupp.single i 1 : (a : σ) → ℕ) j : ℕ)
Tactic: ext j
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
i : σ
r : R
hr : r ≠ 0
b : R
m : σ →₀ ℕ
hmn : m ≤ Finsupp.single i 1
hb : b ∣ r
hm : ¬Eq (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
j : σ
⊢ Eq (α := ℕ) ((m : (a : σ) → ℕ) j : ℕ) ((Finsupp.single i 1 : (a : σ) → ℕ) j : ℕ)
have neg : LE.le (α := ℕ) ((Finsupp.single i 1 : (a : σ) → ℕ) j : ℕ) ((m : (a : σ) → ℕ) j : ℕ)
Tactic: apply le_antisymm (hmn j)
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
i : σ
r : R
hr : r ≠ 0
b : R
m : σ →₀ ℕ
hmn : m ≤ Finsupp.single i 1
hb : b ∣ r
hm : ¬Eq (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
j : σ
⊢ LE.le (α := ℕ) ((Finsupp.single i 1 : (a : σ) → ℕ) j : ℕ) ((m : (a : σ) → ℕ) j : ℕ)
have pos : ∀ (hj : j = i), LE.le (α := ℕ) ((Finsupp.single i 1 : (a : σ) → ℕ) j : ℕ) ((m : (a : σ) → ℕ) j : ℕ)
Tactic: by_cases hj : j = i
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
i : σ
r : R
hr : r ≠ 0
b : R
m : σ →₀ ℕ
hmn : m ≤ Finsupp.single i 1
hb : b ∣ r
hm : ¬Eq (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
j : σ
pos : ∀ (hj : j = i), LE.le (α := ℕ) ((Finsupp.single i 1 : (a : σ) → ℕ) j : ℕ) ((m : (a : σ) → ℕ) j : ℕ)
⊢ LE.le (α := ℕ) ((Finsupp.single i 1 : (a : σ) → ℕ) j : ℕ) ((m : (a : σ) → ℕ) j : ℕ)
have neg : ∀ (hj : ¬j = i), LE.le (α := ℕ) ((Finsupp.single i 1 : (a : σ) → ℕ) j : ℕ) ((m : (a : σ) → ℕ) j : ℕ)
Tactic: by_cases hj : j = i
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.NoZeroDivisors (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
p : MvPolynomial σ R
i : σ
r : R
hr : r ≠ 0
b : R
hb : b ∣ r
hp : p = (C : (a : R) → MvPolynomial σ R) b
⊢ ∃ a ≤ Finsupp.single i 1, b ∣ r ∧ p = (monomial a : (a : R) → MvPolynomial σ R) b
have h : LE.le (α := σ →₀ ℕ) 0 (Finsupp.single i 1) ∧ b ∣ r ∧ p = (monomial 0 : (a : R) → MvPolynomial σ R) b
Tactic: use 0