-- Mathlib/RingTheory/MvPowerSeries/Basic.lean
theorem X_pow_dvd_iff {s : σ} {n : ℕ} {φ : MvPowerSeries σ R} :
    (X s : MvPowerSeries σ R) ^ n ∣ φ ↔ ∀ m : σ →₀ ℕ, m s < n → coeff R m φ = 0

Proof state:
case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), m s < n → (coeff R m) φ = 0
m : σ →₀ ℕ
H : ¬m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).1 + (i, j).2 = m
hi : (i, j).1 = single s n
⊢ single s n + (i, j).2 - single s n + single s n = single s n + (i, j).2

Tactic:
ext

Result:
case pos.h
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), m s < n → (coeff R m) φ = 0
m : σ →₀ ℕ
H : ¬m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).1 + (i, j).2 = m
hi : (i, j).1 = single s n
a✝ : σ
⊢ (single s n + (i, j).2 - single s n + single s n) a✝ = (single s n + (i, j).2) a✝

Proof state:
case mp.intro
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
m : σ →₀ ℕ
h : m s < n
⊢ ∀ x ∈ antidiagonal m, (coeff R x.1) (X s ^ n) * (coeff R x.2) φ = 0

Tactic:
rintro ⟨i, j⟩ hij

Result:
case mp.intro.mk
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
m : σ →₀ ℕ
h : m s < n
i j : σ →₀ ℕ
hij : (i, j) ∈ antidiagonal m
⊢ (coeff R (i, j).1) (X s ^ n) * (coeff R (i, j).2) φ = 0

Proof state:
case neg.mk
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), m s < n → (coeff R m) φ = 0
m : σ →₀ ℕ
H : ¬m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).1 + (i, j).2 = m
⊢ ((coeff R (i, j).1) (X s ^ n) * (coeff R (i, j).2) fun m => (coeff R (m + single s n)) φ) = 0

Tactic:
rw [coeff_X_pow]

Result:
case neg.mk
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), m s < n → (coeff R m) φ = 0
m : σ →₀ ℕ
H : ¬m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).1 + (i, j).2 = m
⊢ ((if (i, j).1 = single s n then 1 else 0) * (coeff R (i, j).2) fun m => (coeff R (m + single s n)) φ) = 0

Proof state:
case pos.h₀.mk
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), m s < n → (coeff R m) φ = 0
m : σ →₀ ℕ
H : m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).1 + (i, j).2 = m
hne : (i, j) ≠ (single s n, m - single s n)
⊢ ((if (i, j).1 = single s n then 1 else 0) * (coeff R (i, j).2) fun m => (coeff R (m + single s n)) φ) = 0

Tactic:
split_ifs with hi

Result:
case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), m s < n → (coeff R m) φ = 0
m : σ →₀ ℕ
H : m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).1 + (i, j).2 = m
hne : (i, j) ≠ (single s n, m - single s n)
hi : (i, j).1 = single s n
⊢ (1 * (coeff R (i, j).2) fun m => (coeff R (m + single s n)) φ) = 0

case neg
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), m s < n → (coeff R m) φ = 0
m : σ →₀ ℕ
H : m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).1 + (i, j).2 = m
hne : (i, j) ≠ (single s n, m - single s n)
hi : ¬(i, j).1 = single s n
⊢ (0 * (coeff R (i, j).2) fun m => (coeff R (m + single s n)) φ) = 0

Proof state:
case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), m s < n → (coeff R m) φ = 0
m : σ →₀ ℕ
H : n ≤ m s
t : σ
hst : s = t
⊢ (m - single s n + single s n) t = m t

Tactic:
subst t

Result:
case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), m s < n → (coeff R m) φ = 0
m : σ →₀ ℕ
H : n ≤ m s
⊢ (m - single s n + single s n) s = m s

Proof state:
case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), m s < n → (coeff R m) φ = 0
m : σ →₀ ℕ
H : ¬m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).1 + (i, j).2 = m
hi : (i, j).1 = single s n
⊢ False

Tactic:
apply H

Result:
case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), m s < n → (coeff R m) φ = 0
m : σ →₀ ℕ
H : ¬m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).1 + (i, j).2 = m
hi : (i, j).1 = single s n
⊢ m - single s n + single s n = m

Proof state:
case neg
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), m s < n → (coeff R m) φ = 0
m : σ →₀ ℕ
H : ¬m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).1 + (i, j).2 = m
hi : ¬(i, j).1 = single s n
⊢ (0 * (coeff R (i, j).2) fun m => (coeff R (m + single s n)) φ) = 0

Tactic:
exact zero_mul _

Result:
no goals

Proof state:
case mp.intro.mk.hnc
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
m : σ →₀ ℕ
h : m s < n
i j : σ →₀ ℕ
hij : (i, j) ∈ antidiagonal m
⊢ ¬(i, j).1 = single s n

Tactic:
contrapose! h

Result:
case mp.intro.mk.hnc
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
m i j : σ →₀ ℕ
hij : (i, j) ∈ antidiagonal m
h : (i, j).1 = single s n
⊢ n ≤ m s

Proof state:
case neg.a
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), m s < n → (coeff R m) φ = 0
m : σ →₀ ℕ
H : ¬m - single s n + single s n = m
⊢ m s < n

Tactic:
contrapose! H

Result:
case neg.a
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), m s < n → (coeff R m) φ = 0
m : σ →₀ ℕ
H : n ≤ m s
⊢ m - single s n + single s n = m

Proof state:
case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), m s < n → (coeff R m) φ = 0
m : σ →₀ ℕ
H : m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).1 + (i, j).2 = m
hne : (i, j) ≠ (single s n, m - single s n)
hi : (i, j).1 = single s n
⊢ (1 * (coeff R (i, j).2) fun m => (coeff R (m + single s n)) φ) = 0

Tactic:
exfalso

Result:
case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), m s < n → (coeff R m) φ = 0
m : σ →₀ ℕ
H : m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).1 + (i, j).2 = m
hne : (i, j) ≠ (single s n, m - single s n)
hi : (i, j).1 = single s n
⊢ False

Proof state:
case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), m s < n → (coeff R m) φ = 0
m : σ →₀ ℕ
H : m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).1 + (i, j).2 = m
hne : (i, j) ≠ (single s n, m - single s n)
hi : (i, j).1 = single s n
⊢ i = (i, j).1 ∧ j = (i, j).1 + (i, j).2 - (i, j).1

Tactic:
refine ⟨rfl, ?_⟩

Result:
case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), m s < n → (coeff R m) φ = 0
m : σ →₀ ℕ
H : m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).1 + (i, j).2 = m
hne : (i, j) ≠ (single s n, m - single s n)
hi : (i, j).1 = single s n
⊢ j = (i, j).1 + (i, j).2 - (i, j).1

Proof state:
case neg
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), m s < n → (coeff R m) φ = 0
m : σ →₀ ℕ
H : ¬m - single s n + single s n = m
⊢ ∀ x ∈ antidiagonal m, ((coeff R x.1) (X s ^ n) * (coeff R x.2) fun m => (coeff R (m + single s n)) φ) = 0

Tactic:
rintro ⟨i, j⟩ hij

Result:
case neg.mk
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), m s < n → (coeff R m) φ = 0
m : σ →₀ ℕ
H : ¬m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j) ∈ antidiagonal m
⊢ ((coeff R (i, j).1) (X s ^ n) * (coeff R (i, j).2) fun m => (coeff R (m + single s n)) φ) = 0