case zero
Γ✝ : Type ?u.1298389
R : Type u_2
inst✝³ : OrderedCancelAddCommMonoid Γ✝
Γ : Type u_1
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
x : HahnSeries Γ R
⊢ order (x ^ Nat.zero) = Nat.zero • order x

case succ
Γ✝ : Type ?u.1298389
R : Type u_2
inst✝³ : OrderedCancelAddCommMonoid Γ✝
Γ : Type u_1
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
x : HahnSeries Γ R
h : ℕ
IH : order (x ^ h) = h • order x
⊢ order (x ^ Nat.succ h) = Nat.succ h • order x
Γ✝ : Type ?u.1298389
R : Type u_2
inst✝³ : OrderedCancelAddCommMonoid Γ✝
Γ : Type u_1
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
x : HahnSeries Γ R
n : ℕ
⊢ order (x ^ n) = n • order x
induction' n with h IH
case succ.inl
Γ✝ : Type ?u.1298389
R : Type u_2
inst✝³ : OrderedCancelAddCommMonoid Γ✝
Γ : Type u_1
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
h : ℕ
IH : order (0 ^ h) = h • order 0
⊢ order (0 ^ Nat.succ h) = Nat.succ h • order 0

case succ.inr
Γ✝ : Type ?u.1298389
R : Type u_2
inst✝³ : OrderedCancelAddCommMonoid Γ✝
Γ : Type u_1
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
x : HahnSeries Γ R
h : ℕ
IH : order (x ^ h) = h • order x
hx : x ≠ 0
⊢ order (x ^ Nat.succ h) = Nat.succ h • order x
case succ
Γ✝ : Type ?u.1298389
R : Type u_2
inst✝³ : OrderedCancelAddCommMonoid Γ✝
Γ : Type u_1
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
x : HahnSeries Γ R
h : ℕ
IH : order (x ^ h) = h • order x
⊢ order (x ^ Nat.succ h) = Nat.succ h • order x
rcases eq_or_ne x 0 with (rfl | hx)
no goals
case succ.inr
Γ✝ : Type ?u.1298389
R : Type u_2
inst✝³ : OrderedCancelAddCommMonoid Γ✝
Γ : Type u_1
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
x : HahnSeries Γ R
h : ℕ
IH : order (x ^ h) = h • order x
hx : x ≠ 0
⊢ order (x ^ Nat.succ h) = Nat.succ h • order x
rw [pow_succ', order_mul (pow_ne_zero _ hx) hx, succ_nsmul', IH]
no goals
case zero
Γ✝ : Type ?u.1298389
R : Type u_2
inst✝³ : OrderedCancelAddCommMonoid Γ✝
Γ : Type u_1
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
x : HahnSeries Γ R
⊢ order (x ^ Nat.zero) = Nat.zero • order x
simp
no goals
case succ.inl
Γ✝ : Type ?u.1298389
R : Type u_2
inst✝³ : OrderedCancelAddCommMonoid Γ✝
Γ : Type u_1
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
h : ℕ
IH : order (0 ^ h) = h • order 0
⊢ order (0 ^ Nat.succ h) = Nat.succ h • order 0
simp