Theorem: MvPowerSeries.weightedOrder_add_of_weightedOrder_lt.aux (DividedPowers/ForMathlib/MvPowerSeries/Order.lean)

State before:
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
H : weightedOrder w f < weightedOrder w g
⊢ weightedOrder w (f + g) = weightedOrder w f
Tactic:
obtain ⟨n, hn⟩ := ne_top_iff_exists.mp (ne_top_of_lt H)
State after:
case intro
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : ↑n = weightedOrder w f
⊢ weightedOrder w (f + g) = weightedOrder w f

State before:
case intro
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : ↑n = weightedOrder w f
⊢ weightedOrder w (f + g) = weightedOrder w f
Tactic:
erw [← hn, weightedOrder_eq_nat]
State after:
case intro
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : ↑n = weightedOrder w f
⊢ (∃ d, (weight w) d = n ∧ (coeff α d) (f + g) ≠ 0) ∧ ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff α d) (f + g) = 0

State before:
case intro
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : ↑n = weightedOrder w f
⊢ (∃ d, (weight w) d = n ∧ (coeff α d) (f + g) ≠ 0) ∧ ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff α d) (f + g) = 0
Tactic:
obtain ⟨d, hd, hd'⟩ := ((weightedOrder_eq_nat w).mp hn.symm).1
State after:
case intro.intro.intro
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : ↑n = weightedOrder w f
d : σ →₀ ℕ
hd : (weight w) d = n
hd' : (coeff α d) f ≠ 0
⊢ (∃ d, (weight w) d = n ∧ (coeff α d) (f + g) ≠ 0) ∧ ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff α d) (f + g) = 0

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

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

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

State before:
case h
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : ↑n = weightedOrder w f
d : σ →₀ ℕ
hd : (weight w) d = n
hd' : (coeff α d) f ≠ 0
⊢ (weight w) d = n ∧ (coeff α d) (f + g) ≠ 0
Tactic:
use hd
State after:
case right
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : ↑n = weightedOrder w f
d : σ →₀ ℕ
hd : (weight w) d = n
hd' : (coeff α d) f ≠ 0
⊢ (coeff α d) (f + g) ≠ 0

State before:
case right
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : ↑n = weightedOrder w f
d : σ →₀ ℕ
hd : (weight w) d = n
hd' : (coeff α d) f ≠ 0
⊢ (coeff α d) (f + g) ≠ 0
Tactic:
rw [← hn, ← hd] at H
State after:
case right
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
n : ℕ
hn : ↑n = weightedOrder w f
d : σ →₀ ℕ
H : ↑((weight w) d) < weightedOrder w g
hd : (weight w) d = n
hd' : (coeff α d) f ≠ 0
⊢ (coeff α d) (f + g) ≠ 0

State before:
case right
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
n : ℕ
hn : ↑n = weightedOrder w f
d : σ →₀ ℕ
H : ↑((weight w) d) < weightedOrder w g
hd : (weight w) d = n
hd' : (coeff α d) f ≠ 0
⊢ (coeff α d) (f + g) ≠ 0
Tactic:
rw [(coeff _ _).map_add, coeff_of_lt_weightedOrder w g H, add_zero]
State after:
case right
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
n : ℕ
hn : ↑n = weightedOrder w f
d : σ →₀ ℕ
H : ↑((weight w) d) < weightedOrder w g
hd : (weight w) d = n
hd' : (coeff α d) f ≠ 0
⊢ (coeff α d) f ≠ 0

State before:
case right
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
n : ℕ
hn : ↑n = weightedOrder w f
d : σ →₀ ℕ
H : ↑((weight w) d) < weightedOrder w g
hd : (weight w) d = n
hd' : (coeff α d) f ≠ 0
⊢ (coeff α d) f ≠ 0
Tactic:
exact hd'
State after:
no goals

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

State before:
case intro.intro.intro.right
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : ↑n = weightedOrder w f
d : σ →₀ ℕ
hd : (weight w) d = n
hd' : (coeff α d) f ≠ 0
b : σ →₀ ℕ
hb : (weight w) b < n
⊢ (coeff α b) (f + g) = 0
Tactic:
suffices ↑(weight w b) < weightedOrder w f by
  rw [(coeff _ _).map_add, coeff_of_lt_weightedOrder w f this,
    coeff_of_lt_weightedOrder w g (lt_trans this H), add_zero]
State after:
case intro.intro.intro.right
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : ↑n = weightedOrder w f
d : σ →₀ ℕ
hd : (weight w) d = n
hd' : (coeff α d) f ≠ 0
b : σ →₀ ℕ
hb : (weight w) b < n
⊢ ↑((weight w) b) < weightedOrder w f

State before:
case intro.intro.intro.right
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : ↑n = weightedOrder w f
d : σ →₀ ℕ
hd : (weight w) d = n
hd' : (coeff α d) f ≠ 0
b : σ →₀ ℕ
hb : (weight w) b < n
⊢ ↑((weight w) b) < weightedOrder w f
Tactic:
rw [← hn, ENat.some_eq_coe, Nat.cast_lt]
State after:
case intro.intro.intro.right
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : ↑n = weightedOrder w f
d : σ →₀ ℕ
hd : (weight w) d = n
hd' : (coeff α d) f ≠ 0
b : σ →₀ ℕ
hb : (weight w) b < n
⊢ (weight w) b < n

State before:
case intro.intro.intro.right
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : ↑n = weightedOrder w f
d : σ →₀ ℕ
hd : (weight w) d = n
hd' : (coeff α d) f ≠ 0
b : σ →₀ ℕ
hb : (weight w) b < n
⊢ (weight w) b < n
Tactic:
exact hb
State after:
no goals

State before:
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : ↑n = weightedOrder w f
d : σ →₀ ℕ
hd : (weight w) d = n
hd' : (coeff α d) f ≠ 0
b : σ →₀ ℕ
hb : (weight w) b < n
this : ↑((weight w) b) < weightedOrder w f
⊢ (coeff α b) (f + g) = 0
Tactic:
rw [(coeff _ _).map_add, coeff_of_lt_weightedOrder w f this,
  coeff_of_lt_weightedOrder w g (lt_trans this H), add_zero]
State after:
no goals