-- Mathlib/RingTheory/MvPowerSeries/Order.lean
theorem weightedOrder_add_of_weightedOrder_lt.aux
    (H : f.weightedOrder w < g.weightedOrder w) :
    (f + g).weightedOrder w = f.weightedOrder w

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : ↑n = weightedOrder w f
d : σ →₀ ℕ
hd' : (coeff R d) f ≠ 0
hd : (weight w) d = n
b : σ →₀ ℕ
hb : (weight w) b < n
this : ↑((weight w) b) < weightedOrder w f
⊢ (coeff R b) (f + g) = 0

Tactic:
rw [(coeff _ _).map_add, coeff_eq_zero_of_lt_weightedOrder w this,
  coeff_eq_zero_of_lt_weightedOrder w (lt_trans this H), add_zero]

Result:
no goals

Proof state:
case intro.intro.intro.right
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : ↑n = weightedOrder w f
d : σ →₀ ℕ
hd' : (coeff R d) f ≠ 0
hd : (weight w) d = n
b : σ →₀ ℕ
hb : (weight w) b < n
⊢ (weight w) b < n

Tactic:
exact hb

Result:
no goals

Proof state:
case intro.intro.intro.left
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : ↑n = weightedOrder w f
d : σ →₀ ℕ
hd' : (coeff R d) f ≠ 0
hd : (weight w) d = n
⊢ ∃ d, (coeff R d) (f + g) ≠ 0 ∧ (weight w) d = n

Tactic:
refine ⟨d, ?_, hd⟩

Result:
case intro.intro.intro.left
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : ↑n = weightedOrder w f
d : σ →₀ ℕ
hd' : (coeff R d) f ≠ 0
hd : (weight w) d = n
⊢ (coeff R d) (f + g) ≠ 0

Proof state:
case intro
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : ↑n = weightedOrder w f
⊢ (∃ d, (coeff R d) (f + g) ≠ 0 ∧ (weight w) d = n) ∧ ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff R d) (f + g) = 0

Tactic:
obtain ⟨d, hd', hd⟩ := ((weightedOrder_eq_nat w).mp hn.symm).1

Result:
case intro.intro.intro
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : ↑n = weightedOrder w f
d : σ →₀ ℕ
hd' : (coeff R d) f ≠ 0
hd : (weight w) d = n
⊢ (∃ d, (coeff R d) (f + g) ≠ 0 ∧ (weight w) d = n) ∧ ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff R d) (f + g) = 0

Proof state:
case intro.intro.intro.right
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : ↑n = weightedOrder w f
d : σ →₀ ℕ
hd' : (coeff R d) f ≠ 0
hd : (weight w) d = n
⊢ ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff R d) (f + g) = 0

Tactic:
intro b hb

Result:
case intro.intro.intro.right
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : ↑n = weightedOrder w f
d : σ →₀ ℕ
hd' : (coeff R d) f ≠ 0
hd : (weight w) d = n
b : σ →₀ ℕ
hb : (weight w) b < n
⊢ (coeff R b) (f + g) = 0

Proof state:
case intro
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : ↑n = weightedOrder w f
⊢ weightedOrder w (f + g) = weightedOrder w f

Tactic:
rw [← hn, weightedOrder_eq_nat]

Result:
case intro
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : ↑n = weightedOrder w f
⊢ (∃ d, (coeff R d) (f + g) ≠ 0 ∧ (weight w) d = n) ∧ ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff R d) (f + g) = 0

Proof state:
case intro.intro.intro.right
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : ↑n = weightedOrder w f
d : σ →₀ ℕ
hd' : (coeff R d) f ≠ 0
hd : (weight w) d = n
b : σ →₀ ℕ
hb : (weight w) b < n
⊢ (coeff R b) (f + g) = 0

Tactic:
suffices weight w b < weightedOrder w f by
  rw [(coeff _ _).map_add, coeff_eq_zero_of_lt_weightedOrder w this,
    coeff_eq_zero_of_lt_weightedOrder w (lt_trans this H), add_zero]

Result:
case intro.intro.intro.right
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : ↑n = weightedOrder w f
d : σ →₀ ℕ
hd' : (coeff R d) f ≠ 0
hd : (weight w) d = n
b : σ →₀ ℕ
hb : (weight w) b < n
⊢ ↑((weight w) b) < weightedOrder w f

Proof state:
case intro.intro.intro.left
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
n : ℕ
hn : ↑n = weightedOrder w f
d : σ →₀ ℕ
H : ↑((weight w) d) < weightedOrder w g
hd' : (coeff R d) f ≠ 0
hd : (weight w) d = n
⊢ (coeff R d) (f + g) ≠ 0

Tactic:
rw [(coeff _ _).map_add, coeff_eq_zero_of_lt_weightedOrder w H, add_zero]

Result:
case intro.intro.intro.left
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
n : ℕ
hn : ↑n = weightedOrder w f
d : σ →₀ ℕ
H : ↑((weight w) d) < weightedOrder w g
hd' : (coeff R d) f ≠ 0
hd : (weight w) d = n
⊢ (coeff R d) f ≠ 0

Proof state:
case intro.intro.intro.left
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : ↑n = weightedOrder w f
d : σ →₀ ℕ
hd' : (coeff R d) f ≠ 0
hd : (weight w) d = n
⊢ (coeff R d) (f + g) ≠ 0

Tactic:
rw [← hn, ← hd] at H

Result:
case intro.intro.intro.left
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
n : ℕ
hn : ↑n = weightedOrder w f
d : σ →₀ ℕ
H : ↑((weight w) d) < weightedOrder w g
hd' : (coeff R d) f ≠ 0
hd : (weight w) d = n
⊢ (coeff R d) (f + g) ≠ 0

Proof state:
case intro.intro.intro.left
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
n : ℕ
hn : ↑n = weightedOrder w f
d : σ →₀ ℕ
H : ↑((weight w) d) < weightedOrder w g
hd' : (coeff R d) f ≠ 0
hd : (weight w) d = n
⊢ (coeff R d) f ≠ 0

Tactic:
exact hd'

Result:
no goals

Proof state:
case intro.intro.intro
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : ↑n = weightedOrder w f
d : σ →₀ ℕ
hd' : (coeff R d) f ≠ 0
hd : (weight w) d = n
⊢ (∃ d, (coeff R d) (f + g) ≠ 0 ∧ (weight w) d = n) ∧ ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff R d) (f + g) = 0

Tactic:
constructor

Result:
case intro.intro.intro.left
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : ↑n = weightedOrder w f
d : σ →₀ ℕ
hd' : (coeff R d) f ≠ 0
hd : (weight w) d = n
⊢ ∃ d, (coeff R d) (f + g) ≠ 0 ∧ (weight w) d = n

case intro.intro.intro.right
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : ↑n = weightedOrder w f
d : σ →₀ ℕ
hd' : (coeff R d) f ≠ 0
hd : (weight w) d = n
⊢ ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff R d) (f + g) = 0

Proof state:
case intro.intro.intro.right
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : ↑n = weightedOrder w f
d : σ →₀ ℕ
hd' : (coeff R d) f ≠ 0
hd : (weight w) d = n
b : σ →₀ ℕ
hb : (weight w) b < n
⊢ ↑((weight w) b) < weightedOrder w f

Tactic:
rw [← hn, Nat.cast_lt]

Result:
case intro.intro.intro.right
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : ↑n = weightedOrder w f
d : σ →₀ ℕ
hd' : (coeff R d) f ≠ 0
hd : (weight w) d = n
b : σ →₀ ℕ
hb : (weight w) b < n
⊢ (weight w) b < n