o : Ordinal
f : (b : Ordinal) → b < o → Ordinal → Ordinal
i : Ordinal
hi : i < o
H : IsNormal (f i hi)
a : Ordinal
⊢ familyOfBFamily o f (enum (fun x x_1 => x < x_1) i (_ : i < type fun x x_1 => x < x_1)) (derivBFamily o f a) =
    derivBFamily o f a
o : Ordinal
f : (b : Ordinal) → b < o → Ordinal → Ordinal
i : Ordinal
hi : i < o
H : IsNormal (f i hi)
a : Ordinal
⊢ f i hi (derivBFamily o f a) = derivBFamily o f a
rw [← familyOfBFamily_enum o f]
case H
o : Ordinal
f : (b : Ordinal) → b < o → Ordinal → Ordinal
i : Ordinal
hi : i < o
H : IsNormal (f i hi)
a : Ordinal
⊢ IsNormal (familyOfBFamily o f (enum (fun x x_1 => x < x_1) i (_ : i < type fun x x_1 => x < x_1)))
o : Ordinal
f : (b : Ordinal) → b < o → Ordinal → Ordinal
i : Ordinal
hi : i < o
H : IsNormal (f i hi)
a : Ordinal
⊢ familyOfBFamily o f (enum (fun x x_1 => x < x_1) i (_ : i < type fun x x_1 => x < x_1)) (derivBFamily o f a) =
    derivBFamily o f a
apply derivFamily_fp
case H
o : Ordinal
f : (b : Ordinal) → b < o → Ordinal → Ordinal
i : Ordinal
hi : i < o
H : IsNormal (f i hi)
a : Ordinal
⊢ IsNormal (f i ?H.hi)

case H.hi
o : Ordinal
f : (b : Ordinal) → b < o → Ordinal → Ordinal
i : Ordinal
hi : i < o
H : IsNormal (f i hi)
a : Ordinal
⊢ i < o
case H
o : Ordinal
f : (b : Ordinal) → b < o → Ordinal → Ordinal
i : Ordinal
hi : i < o
H : IsNormal (f i hi)
a : Ordinal
⊢ IsNormal (familyOfBFamily o f (enum (fun x x_1 => x < x_1) i (_ : i < type fun x x_1 => x < x_1)))
rw [familyOfBFamily_enum]
no goals
case H
o : Ordinal
f : (b : Ordinal) → b < o → Ordinal → Ordinal
i : Ordinal
hi : i < o
H : IsNormal (f i hi)
a : Ordinal
⊢ IsNormal (f i ?H.hi)

case H.hi
o : Ordinal
f : (b : Ordinal) → b < o → Ordinal → Ordinal
i : Ordinal
hi : i < o
H : IsNormal (f i hi)
a : Ordinal
⊢ i < o
exact H