o : Ordinal
f : (b : Ordinal) → b < o → Ordinal → Ordinal
H : ∀ (i : Ordinal) (hi : i < o), IsNormal (f i hi)
a : Ordinal
⊢ (∀ (i : Ordinal) (hi : i < o), f i hi a = a) ↔ ∀ (i : Ordinal) (hi : i < o), f i hi a ≤ a
o : Ordinal
f : (b : Ordinal) → b < o → Ordinal → Ordinal
H : ∀ (i : Ordinal) (hi : i < o), IsNormal (f i hi)
a : Ordinal
⊢ (∀ (i : Ordinal) (hi : i < o), f i hi a = a) ↔ ∃ b, derivBFamily o f b = a
rw [← le_iff_derivBFamily H]
o : Ordinal
f : (b : Ordinal) → b < o → Ordinal → Ordinal
H : ∀ (i : Ordinal) (hi : i < o), IsNormal (f i hi)
a : Ordinal
h : ∀ (i : Ordinal) (hi : i < o), f i hi a ≤ a
i : Ordinal
hi : i < o
⊢ f i hi a = a
o : Ordinal
f : (b : Ordinal) → b < o → Ordinal → Ordinal
H : ∀ (i : Ordinal) (hi : i < o), IsNormal (f i hi)
a : Ordinal
⊢ (∀ (i : Ordinal) (hi : i < o), f i hi a = a) ↔ ∀ (i : Ordinal) (hi : i < o), f i hi a ≤ a
refine' ⟨fun h i hi => le_of_eq (h i hi), fun h i hi => _⟩
o : Ordinal
f : (b : Ordinal) → b < o → Ordinal → Ordinal
H : ∀ (i : Ordinal) (hi : i < o), IsNormal (f i hi)
a : Ordinal
h : ∀ (i : Ordinal) (hi : i < o), f i hi a ≤ a
i : Ordinal
hi : i < o
⊢ f i hi a ≤ a
o : Ordinal
f : (b : Ordinal) → b < o → Ordinal → Ordinal
H : ∀ (i : Ordinal) (hi : i < o), IsNormal (f i hi)
a : Ordinal
h : ∀ (i : Ordinal) (hi : i < o), f i hi a ≤ a
i : Ordinal
hi : i < o
⊢ f i hi a = a
rw [← (H i hi).le_iff_eq]
no goals
o : Ordinal
f : (b : Ordinal) → b < o → Ordinal → Ordinal
H : ∀ (i : Ordinal) (hi : i < o), IsNormal (f i hi)
a : Ordinal
h : ∀ (i : Ordinal) (hi : i < o), f i hi a ≤ a
i : Ordinal
hi : i < o
⊢ f i hi a ≤ a
exact h i hi