⊢ (fun a => sup fun n => (HMul.hMul 0^[n]) a) = id
⊢ nfp (HMul.hMul 0) = id
rw [← sup_iterate_eq_nfp]
case zero
a : Ordinal
⊢ (HMul.hMul 0^[Nat.zero]) a ≤ id a

case succ
a : Ordinal
n : ℕ
n_ih✝ : (HMul.hMul 0^[n]) a ≤ id a
⊢ (HMul.hMul 0^[Nat.succ n]) a ≤ id a
a : Ordinal
n : ℕ
⊢ (HMul.hMul 0^[n]) a ≤ id a
induction' n with n _
case succ
a : Ordinal
n : ℕ
n_ih✝ : (HMul.hMul 0^[n]) a ≤ id a
⊢ (HMul.hMul 0 ∘ HMul.hMul 0^[n]) a ≤ id a
case succ
a : Ordinal
n : ℕ
n_ih✝ : (HMul.hMul 0^[n]) a ≤ id a
⊢ (HMul.hMul 0^[Nat.succ n]) a ≤ id a
rw [Function.iterate_succ']
case succ
a : Ordinal
n : ℕ
n_ih✝ : (HMul.hMul 0^[n]) a ≤ id a
⊢ 0 * (HMul.hMul 0^[n]) a ≤ a
case succ
a : Ordinal
n : ℕ
n_ih✝ : (HMul.hMul 0^[n]) a ≤ id a
⊢ (HMul.hMul 0 ∘ HMul.hMul 0^[n]) a ≤ id a
change 0 * _ ≤ a
case succ
a : Ordinal
n : ℕ
n_ih✝ : (HMul.hMul 0^[n]) a ≤ id a
⊢ 0 ≤ a
case succ
a : Ordinal
n : ℕ
n_ih✝ : (HMul.hMul 0^[n]) a ≤ id a
⊢ 0 * (HMul.hMul 0^[n]) a ≤ a
rw [zero_mul]
no goals
case succ
a : Ordinal
n : ℕ
n_ih✝ : (HMul.hMul 0^[n]) a ≤ id a
⊢ 0 ≤ a
exact Ordinal.zero_le a
no goals
case zero
a : Ordinal
⊢ (HMul.hMul 0^[Nat.zero]) a ≤ id a
rfl