-- Mathlib/RingTheory/MvPowerSeries/NoZeroDivisors.lean
theorem mem_nonZeroDivisors_of_constantCoeff {φ : MvPowerSeries σ R}
    (hφ : constantCoeff σ R φ ∈ nonZeroDivisors R) :
    φ ∈ nonZeroDivisors (MvPowerSeries σ R)

Proof state:
case h.e'_2
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
hφ : (constantCoeff σ R) φ ∈ nonZeroDivisors R
x : MvPowerSeries σ R
hx : x * φ = 0
d e : σ →₀ ℕ
he : ∀ y < e, (coeff R y) x = (coeff R y) 0
⊢ (coeff R e) x * (constantCoeff σ R) φ = ∑ p ∈ antidiagonal e, (coeff R p.1) x * (coeff R p.2) φ

Tactic:
rw [Finset.sum_eq_single (e,0), coeff_zero_eq_constantCoeff]

Result:
case h.e'_2.h₀
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
hφ : (constantCoeff σ R) φ ∈ nonZeroDivisors R
x : MvPowerSeries σ R
hx : x * φ = 0
d e : σ →₀ ℕ
he : ∀ y < e, (coeff R y) x = (coeff R y) 0
⊢ ∀ b ∈ antidiagonal e, b ≠ (e, 0) → (coeff R b.1) x * (coeff R b.2) φ = 0

case h.e'_2.h₁
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
hφ : (constantCoeff σ R) φ ∈ nonZeroDivisors R
x : MvPowerSeries σ R
hx : x * φ = 0
d e : σ →₀ ℕ
he : ∀ y < e, (coeff R y) x = (coeff R y) 0
⊢ (e, 0) ∉ antidiagonal e → (coeff R (e, 0).1) x * (coeff R (e, 0).2) φ = 0

Proof state:
case h
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
hφ : (constantCoeff σ R) φ ∈ nonZeroDivisors R
x : MvPowerSeries σ R
hx : x * φ = 0
d : σ →₀ ℕ
⊢ ∀ (x_1 : σ →₀ ℕ), (∀ y < x_1, (coeff R y) x = (coeff R y) 0) → (coeff R x_1) x = (coeff R x_1) 0

Tactic:
intro e he

Result:
case h
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
hφ : (constantCoeff σ R) φ ∈ nonZeroDivisors R
x : MvPowerSeries σ R
hx : x * φ = 0
d e : σ →₀ ℕ
he : ∀ y < e, (coeff R y) x = (coeff R y) 0
⊢ (coeff R e) x = (coeff R e) 0

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
hφ : (constantCoeff σ R) φ ∈ nonZeroDivisors R
x : MvPowerSeries σ R
hx : x * φ = 0
⊢ x = 0

Tactic:
ext d

Result:
case h
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
hφ : (constantCoeff σ R) φ ∈ nonZeroDivisors R
x : MvPowerSeries σ R
hx : x * φ = 0
d : σ →₀ ℕ
⊢ (coeff R d) x = (coeff R d) 0

Proof state:
case h
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
hφ : (constantCoeff σ R) φ ∈ nonZeroDivisors R
x : MvPowerSeries σ R
hx : x * φ = 0
d : σ →₀ ℕ
⊢ (coeff R d) x = (coeff R d) 0

Tactic:
apply WellFoundedLT.induction d

Result:
case h
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
hφ : (constantCoeff σ R) φ ∈ nonZeroDivisors R
x : MvPowerSeries σ R
hx : x * φ = 0
d : σ →₀ ℕ
⊢ ∀ (x_1 : σ →₀ ℕ), (∀ y < x_1, (coeff R y) x = (coeff R y) 0) → (coeff R x_1) x = (coeff R x_1) 0

Proof state:
case h.e'_2.h₀.mk
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
hφ : (constantCoeff σ R) φ ∈ nonZeroDivisors R
x : MvPowerSeries σ R
hx : x * φ = 0
d e : σ →₀ ℕ
he : ∀ y < e, (coeff R y) x = (coeff R y) 0
u snd✝ : σ →₀ ℕ
huv : (u, snd✝) ∈ antidiagonal e
a✝ : (u, snd✝) ≠ (e, 0)
⊢ u < e

Tactic:
apply lt_of_le_of_ne

Result:
case h.e'_2.h₀.mk.a
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
hφ : (constantCoeff σ R) φ ∈ nonZeroDivisors R
x : MvPowerSeries σ R
hx : x * φ = 0
d e : σ →₀ ℕ
he : ∀ y < e, (coeff R y) x = (coeff R y) 0
u snd✝ : σ →₀ ℕ
huv : (u, snd✝) ∈ antidiagonal e
a✝ : (u, snd✝) ≠ (e, 0)
⊢ u ≤ e

case h.e'_2.h₀.mk.a
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
hφ : (constantCoeff σ R) φ ∈ nonZeroDivisors R
x : MvPowerSeries σ R
hx : x * φ = 0
d e : σ →₀ ℕ
he : ∀ y < e, (coeff R y) x = (coeff R y) 0
u snd✝ : σ →₀ ℕ
huv : (u, snd✝) ∈ antidiagonal e
a✝ : (u, snd✝) ≠ (e, 0)
⊢ u ≠ e

Proof state:
case h.e'_2.h₀.mk.a
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
hφ : (constantCoeff σ R) φ ∈ nonZeroDivisors R
x : MvPowerSeries σ R
hx : x * φ = 0
d u snd✝ : σ →₀ ℕ
he : ∀ y < u, (coeff R y) x = (coeff R y) 0
huv : (u, snd✝) ∈ antidiagonal u
a✝ : (u, snd✝) ≠ (u, 0)
⊢ False

Tactic:
simp_all

Result:
no goals

Proof state:
case h.e'_2.h₀
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
hφ : (constantCoeff σ R) φ ∈ nonZeroDivisors R
x : MvPowerSeries σ R
hx : x * φ = 0
d e : σ →₀ ℕ
he : ∀ y < e, (coeff R y) x = (coeff R y) 0
⊢ ∀ b ∈ antidiagonal e, b ≠ (e, 0) → (coeff R b.1) x * (coeff R b.2) φ = 0

Tactic:
rintro ⟨u, _⟩ huv _

Result:
case h.e'_2.h₀.mk
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
hφ : (constantCoeff σ R) φ ∈ nonZeroDivisors R
x : MvPowerSeries σ R
hx : x * φ = 0
d e : σ →₀ ℕ
he : ∀ y < e, (coeff R y) x = (coeff R y) 0
u snd✝ : σ →₀ ℕ
huv : (u, snd✝) ∈ antidiagonal e
a✝ : (u, snd✝) ≠ (e, 0)
⊢ (coeff R (u, snd✝).1) x * (coeff R (u, snd✝).2) φ = 0

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
hφ : (constantCoeff σ R) φ ∈ nonZeroDivisors R
x : MvPowerSeries σ R
hx : x * φ = 0
d e : σ →₀ ℕ
he : ∀ y < e, (coeff R y) x = (coeff R y) 0
u snd✝ : σ →₀ ℕ
huv : (u, snd✝) ∈ antidiagonal e
a✝ : (u, snd✝) ≠ (e, 0)
this : u < e
⊢ (coeff R (u, snd✝).1) x * (coeff R (u, snd✝).2) φ = 0

Tactic:
simp only [he u this, zero_mul, map_zero]

Result:
no goals

Proof state:
case h.e'_2.h₀.mk.a
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
hφ : (constantCoeff σ R) φ ∈ nonZeroDivisors R
x : MvPowerSeries σ R
hx : x * φ = 0
d e : σ →₀ ℕ
he : ∀ y < e, (coeff R y) x = (coeff R y) 0
u snd✝ : σ →₀ ℕ
huv : (u, snd✝) ∈ antidiagonal e
a✝ : (u, snd✝) ≠ (e, 0)
⊢ u ≤ e

Tactic:
simp only [← mem_antidiagonal.mp huv, le_add_iff_nonneg_right, zero_le]

Result:
no goals

Proof state:
case h
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
hφ : (constantCoeff σ R) φ ∈ nonZeroDivisors R
x : MvPowerSeries σ R
hx : x * φ = 0
d e : σ →₀ ℕ
he : ∀ y < e, (coeff R y) x = (coeff R y) 0
⊢ (coeff R e) x * (constantCoeff σ R) φ = (coeff R e) (x * φ)

Tactic:
convert (coeff_mul e x φ).symm

Result:
case h.e'_2
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
hφ : (constantCoeff σ R) φ ∈ nonZeroDivisors R
x : MvPowerSeries σ R
hx : x * φ = 0
d e : σ →₀ ℕ
he : ∀ y < e, (coeff R y) x = (coeff R y) 0
⊢ (coeff R e) x * (constantCoeff σ R) φ = ∑ p ∈ antidiagonal e, (coeff R p.1) x * (coeff R p.2) φ

Proof state:
case h
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
hφ : (constantCoeff σ R) φ ∈ nonZeroDivisors R
x : MvPowerSeries σ R
hx : x * φ = 0
d e : σ →₀ ℕ
he : ∀ y < e, (coeff R y) x = (coeff R y) 0
⊢ (coeff R e) x = (coeff R e) 0

Tactic:
rw [map_zero, ← mul_right_mem_nonZeroDivisors_eq_zero_iff hφ, ← map_zero (f := coeff R e), ← hx]

Result:
case h
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
hφ : (constantCoeff σ R) φ ∈ nonZeroDivisors R
x : MvPowerSeries σ R
hx : x * φ = 0
d e : σ →₀ ℕ
he : ∀ y < e, (coeff R y) x = (coeff R y) 0
⊢ (coeff R e) x * (constantCoeff σ R) φ = (coeff R e) (x * φ)

Proof state:
case h.e'_2.h₀.mk.a
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
hφ : (constantCoeff σ R) φ ∈ nonZeroDivisors R
x : MvPowerSeries σ R
hx : x * φ = 0
d e : σ →₀ ℕ
he : ∀ y < e, (coeff R y) x = (coeff R y) 0
u snd✝ : σ →₀ ℕ
huv : (u, snd✝) ∈ antidiagonal e
a✝ : (u, snd✝) ≠ (e, 0)
⊢ u ≠ e

Tactic:
rintro rfl

Result:
case h.e'_2.h₀.mk.a
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
hφ : (constantCoeff σ R) φ ∈ nonZeroDivisors R
x : MvPowerSeries σ R
hx : x * φ = 0
d u snd✝ : σ →₀ ℕ
he : ∀ y < u, (coeff R y) x = (coeff R y) 0
huv : (u, snd✝) ∈ antidiagonal u
a✝ : (u, snd✝) ≠ (u, 0)
⊢ False

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
hφ : (constantCoeff σ R) φ ∈ nonZeroDivisors R
⊢ φ ∈ nonZeroDivisors (MvPowerSeries σ R)

Tactic:
intro x hx

Result:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
hφ : (constantCoeff σ R) φ ∈ nonZeroDivisors R
x : MvPowerSeries σ R
hx : x * φ = 0
⊢ x = 0