f✝ : Ordinal → Ordinal
f : Ordinal → Ordinal
H : IsNormal f
a : Ordinal
⊢ f a ≤ a ↔ ∃ o, derivFamily (fun x => f) o = a
f✝ : Ordinal → Ordinal
f : Ordinal → Ordinal
H : IsNormal f
a : Ordinal
⊢ f a ≤ a ↔ ∃ o, deriv f o = a
unfold deriv
f✝ : Ordinal → Ordinal
f : Ordinal → Ordinal
H : IsNormal f
a : Ordinal
⊢ f a ≤ a ↔ Unit → f a ≤ a
f✝ : Ordinal → Ordinal
f : Ordinal → Ordinal
H : IsNormal f
a : Ordinal
⊢ f a ≤ a ↔ ∃ o, derivFamily (fun x => f) o = a
rw [← le_iff_derivFamily fun _ : Unit => H]
no goals
f✝ : Ordinal → Ordinal
f : Ordinal → Ordinal
H : IsNormal f
a : Ordinal
⊢ f a ≤ a ↔ Unit → f a ≤ a
exact ⟨fun h _ => h, fun h => h Unit.unit⟩