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, derivFamily (familyOfBFamily o f) b = 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
unfold derivBFamily
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 : (Quotient.out o).α), familyOfBFamily o f i a ≤ a

case H
o : Ordinal
f : (b : Ordinal) → b < o → Ordinal → Ordinal
H : ∀ (i : Ordinal) (hi : i < o), IsNormal (f i hi)
a : Ordinal
⊢ ∀ (i : (Quotient.out o).α), IsNormal (familyOfBFamily o f i)
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, derivFamily (familyOfBFamily o f) b = a
rw [← le_iff_derivFamily]
o : Ordinal
f : (b : Ordinal) → b < o → Ordinal → Ordinal
H : ∀ (i : Ordinal) (hi : i < o), IsNormal (f i hi)
a : Ordinal
h : ∀ (i : (Quotient.out o).α), familyOfBFamily o f i 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 : (Quotient.out o).α), familyOfBFamily o f i a ≤ a
refine' ⟨fun h i => h _ _, 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 : (Quotient.out o).α), familyOfBFamily o f i a ≤ a
i : Ordinal
hi : i < o
⊢ familyOfBFamily o f (enum (fun x x_1 => x < x_1) i (_ : i < type fun x x_1 => x < x_1)) 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 : (Quotient.out o).α), familyOfBFamily o f i a ≤ a
i : Ordinal
hi : i < o
⊢ f i hi a ≤ a
rw [← familyOfBFamily_enum o f]
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 : (Quotient.out o).α), familyOfBFamily o f i a ≤ a
i : Ordinal
hi : i < o
⊢ familyOfBFamily o f (enum (fun x x_1 => x < x_1) i (_ : i < type fun x x_1 => x < x_1)) a ≤ a
apply h
no goals
case H
o : Ordinal
f : (b : Ordinal) → b < o → Ordinal → Ordinal
H : ∀ (i : Ordinal) (hi : i < o), IsNormal (f i hi)
a : Ordinal
⊢ ∀ (i : (Quotient.out o).α), IsNormal (familyOfBFamily o f i)
exact fun _ => H _ _