case inl
a b : Ordinal
hb : 0 < b
hba : b ≤ a ^ ω
ha : a = 0
⊢ nfp (fun x => a * x) b = a ^ ω

case inr
a b : Ordinal
hb : 0 < b
hba : b ≤ a ^ ω
ha : 0 < a
⊢ nfp (fun x => a * x) b = a ^ ω
a b : Ordinal
hb : 0 < b
hba : b ≤ a ^ ω
⊢ nfp (fun x => a * x) b = a ^ ω
cases' eq_zero_or_pos a with ha ha
case inr.a
a b : Ordinal
hb : 0 < b
hba : b ≤ a ^ ω
ha : 0 < a
⊢ nfp (fun x => a * x) b ≤ a ^ ω

case inr.a
a b : Ordinal
hb : 0 < b
hba : b ≤ a ^ ω
ha : 0 < a
⊢ a ^ ω ≤ nfp (fun x => a * x) b
case inr
a b : Ordinal
hb : 0 < b
hba : b ≤ a ^ ω
ha : 0 < a
⊢ nfp (fun x => a * x) b = a ^ ω
apply le_antisymm
case inr.a
a b : Ordinal
hb : 0 < b
hba : b ≤ a ^ ω
ha : 0 < a
⊢ nfp (fun x => a * x) 1 ≤ nfp (fun x => a * x) b
case inr.a
a b : Ordinal
hb : 0 < b
hba : b ≤ a ^ ω
ha : 0 < a
⊢ a ^ ω ≤ nfp (fun x => a * x) b
rw [← nfp_mul_one ha]
no goals
case inr.a
a b : Ordinal
hb : 0 < b
hba : b ≤ a ^ ω
ha : 0 < a
⊢ nfp (fun x => a * x) 1 ≤ nfp (fun x => a * x) b
exact nfp_monotone (mul_isNormal ha).monotone (one_le_iff_pos.2 hb)
case inl
a b : Ordinal
hb : 0 < b
hba : b ≤ 0
ha : a = 0
⊢ nfp (fun x => 0 * x) b = 0
case inl
a b : Ordinal
hb : 0 < b
hba : b ≤ a ^ ω
ha : a = 0
⊢ nfp (fun x => a * x) b = a ^ ω
rw [ha, zero_opow omega_ne_zero] at hba ⊢
case inl
a b : Ordinal
hb : 0 < b
hba : b ≤ 0
ha : a = 0
⊢ id 0 = 0
case inl
a b : Ordinal
hb : 0 < b
hba : b ≤ 0
ha : a = 0
⊢ nfp (fun x => 0 * x) b = 0
rw [Ordinal.le_zero.1 hba, nfp_zero_mul]
no goals
case inl
a b : Ordinal
hb : 0 < b
hba : b ≤ 0
ha : a = 0
⊢ id 0 = 0
rfl
case inr.a
a b : Ordinal
hb : 0 < b
hba : b ≤ a ^ ω
ha : 0 < a
⊢ (fun x x_1 => x * x_1) a (a ^ ω) ≤ a ^ ω
case inr.a
a b : Ordinal
hb : 0 < b
hba : b ≤ a ^ ω
ha : 0 < a
⊢ nfp (fun x => a * x) b ≤ a ^ ω
apply nfp_le_fp (mul_isNormal ha).monotone hba
case inr.a
a b : Ordinal
hb : 0 < b
hba : b ≤ a ^ ω
ha : 0 < a
⊢ a * a ^ ω ≤ a ^ ω
case inr.a
a b : Ordinal
hb : 0 < b
hba : b ≤ a ^ ω
ha : 0 < a
⊢ (fun x x_1 => x * x_1) a (a ^ ω) ≤ a ^ ω
dsimp only
no goals
case inr.a
a b : Ordinal
hb : 0 < b
hba : b ≤ a ^ ω
ha : 0 < a
⊢ a * a ^ ω ≤ a ^ ω
rw [← opow_one_add, one_add_omega]