o : Ordinal
f : (b : Ordinal) → b < o → Ordinal → Ordinal
ho : o ≠ 0
H : ∀ (i : Ordinal) (hi : i < o), IsNormal (f i hi)
a : Ordinal
b : Ordinal
h : ∀ (i : Ordinal) (hi : i < o), f i hi b < nfpBFamily o f a
this : Nonempty (Quotient.out o).α
⊢ b < nfpBFamily o f a
o : Ordinal
f : (b : Ordinal) → b < o → Ordinal → Ordinal
ho : o ≠ 0
H : ∀ (i : Ordinal) (hi : i < o), IsNormal (f i hi)
a : Ordinal
b : Ordinal
h : ∀ (i : Ordinal) (hi : i < o), f i hi b < nfpBFamily o f a
⊢ b < nfpBFamily o f a
haveI := out_nonempty_iff_ne_zero.2 ho
o : Ordinal
f : (b : Ordinal) → b < o → Ordinal → Ordinal
ho : o ≠ 0
H : ∀ (i : Ordinal) (hi : i < o), IsNormal (f i hi)
a : Ordinal
b : Ordinal
h : ∀ (i : Ordinal) (hi : i < o), f i hi b < nfpBFamily o f a
this : Nonempty (Quotient.out o).α
⊢ ∀ (i : (Quotient.out o).α), IsNormal (familyOfBFamily o f i)
o : Ordinal
f : (b : Ordinal) → b < o → Ordinal → Ordinal
ho : o ≠ 0
H : ∀ (i : Ordinal) (hi : i < o), IsNormal (f i hi)
a : Ordinal
b : Ordinal
h : ∀ (i : Ordinal) (hi : i < o), f i hi b < nfpBFamily o f a
this : Nonempty (Quotient.out o).α
⊢ b < nfpBFamily o f a
refine' (apply_lt_nfpFamily_iff.{u, v} _).1 fun _ => h _ _
no goals
o : Ordinal
f : (b : Ordinal) → b < o → Ordinal → Ordinal
ho : o ≠ 0
H : ∀ (i : Ordinal) (hi : i < o), IsNormal (f i hi)
a : Ordinal
b : Ordinal
h : ∀ (i : Ordinal) (hi : i < o), f i hi b < nfpBFamily o f a
this : Nonempty (Quotient.out o).α
⊢ ∀ (i : (Quotient.out o).α), IsNormal (familyOfBFamily o f i)
exact fun _ => H _ _