case refine'_1
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

case refine'_2
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 : b ≤ nfpBFamily o f a
i : Ordinal
hi : i < o
⊢ f i hi 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
⊢ (∀ (i : Ordinal) (hi : i < o), f i hi b ≤ nfpBFamily o f a) ↔ b ≤ nfpBFamily o f a
refine' ⟨fun h => _, fun h i hi => _⟩
case refine'_1
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
ho' : 0 < o
⊢ b ≤ nfpBFamily o f a
case refine'_1
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
have ho' : 0 < o := Ordinal.pos_iff_ne_zero.2 ho
no goals
case refine'_1
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
ho' : 0 < o
⊢ b ≤ nfpBFamily o f a
exact ((H 0 ho').self_le b).trans (h 0 ho')
case refine'_2
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 : b ≤ nfpBFamily o f a
i : Ordinal
hi : i < o
⊢ f i hi b ≤ f i hi (nfpBFamily o f a)
case refine'_2
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 : b ≤ nfpBFamily o f a
i : Ordinal
hi : i < o
⊢ f i hi b ≤ nfpBFamily o f a
rw [← nfpBFamily_fp (H i hi)]
no goals
case refine'_2
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 : b ≤ nfpBFamily o f a
i : Ordinal
hi : i < o
⊢ f i hi b ≤ f i hi (nfpBFamily o f a)
exact (H i hi).monotone h