-- 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.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
hni : (single s n, m - single s n) ∉ antidiagonal m
⊢ (single s n, m - single s n) ∈ antidiagonal m

Tactic:
rwa [mem_antidiagonal, add_comm]

Result:
no goals

Proof state:
case mpr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), m s < n → (coeff R m) φ = 0
⊢ φ = X s ^ n * fun m => (coeff R (m + single s n)) φ

Tactic:
ext m

Result:
case mpr.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 : σ →₀ ℕ
⊢ (coeff R m) φ = (coeff R m) (X s ^ n * fun m => (coeff R (m + single s n)) φ)

Proof state:
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
hni : (single s n, m - single s n) ∉ antidiagonal m
⊢ ((coeff R (single s n, m - single s n).1) (X s ^ n) *
      (coeff R (single s n, m - single s n).2) fun m => (coeff R (m + single s n)) φ) =
    0

Tactic:
exfalso

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
hni : (single s n, m - single s n) ∉ antidiagonal m
⊢ False

Proof state:
case neg.a.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 : n ≤ m s
t : σ
⊢ (m - single s n + single s n) t = m t

Tactic:
by_cases hst : s = 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
t : σ
hst : s = t
⊢ (m - single s n + single s n) t = m t

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 : n ≤ m s
t : σ
hst : ¬s = t
⊢ (m - single s n + single s n) t = m t

Proof state:
case mp
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
⊢ X s ^ n ∣ φ → ∀ (m : σ →₀ ℕ), m s < n → (coeff R m) φ = 0

Tactic:
rintro ⟨φ, rfl⟩ m h

Result:
case mp.intro
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
m : σ →₀ ℕ
h : m s < n
⊢ (coeff R m) (X s ^ n * φ) = 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) ∈ antidiagonal 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 [mem_antidiagonal] at 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).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

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
⊢ (coeff R m) φ =
    (coeff R (single s n, m - single s n).1) (X s ^ n) *
      (coeff R (single s n, m - single s n).2) fun m => (coeff R (m + single s n)) φ

Tactic:
rw [coeff_X_pow, if_pos rfl, one_mul]

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
⊢ (coeff R m) φ = (coeff R (single s n, m - single s n).2) fun m => (coeff R (m + single s n)) φ

Proof state:
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✝

Tactic:
rw [coe_add, coe_add, Pi.add_apply, Pi.add_apply, add_tsub_cancel_left, add_comm]

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 i j : σ →₀ ℕ
hij : (i, j) ∈ antidiagonal m
h : (i, j).1 = single s n
⊢ n ≤ m s

Tactic:
dsimp at 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 = single s n
⊢ n ≤ m s

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
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

Tactic:
exact zero_mul _

Result:
no goals

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
⊢ (coeff R m) φ = (coeff R (single s n, m - single s n).2) fun m => (coeff R (m + single s n)) φ

Tactic:
simpa using congr_arg (fun m : σ →₀ ℕ => coeff R m φ) H.symm

Result:
no goals

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
⊢ j = (i, j).1 + (i, j).2 - (i, j).1

Tactic:
ext t

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
hne : (i, j) ≠ (single s n, m - single s n)
hi : (i, j).1 = single s n
t : σ
⊢ j t = ((i, j).1 + (i, j).2 - (i, j).1) t

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
⊢ ((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
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
hi : ¬(i, j).1 = single s n
⊢ (0 * (coeff R (i, j).2) fun m => (coeff R (m + single s n)) φ) = 0