case refine'_1
ι : Type u
f✝ : ι → Ordinal → Ordinal
hι : Nonempty ι
f : ι → Ordinal → Ordinal
H : ∀ (i : ι), IsNormal (f i)
a b : Ordinal
h : ∀ (i : ι), f i b ≤ nfpFamily f a
⊢ b ≤ nfpFamily f a

case refine'_2
ι : Type u
f✝ : ι → Ordinal → Ordinal
hι : Nonempty ι
f : ι → Ordinal → Ordinal
H : ∀ (i : ι), IsNormal (f i)
a b : Ordinal
h : b ≤ nfpFamily f a
i : ι
⊢ f i b ≤ nfpFamily f a
ι : Type u
f✝ : ι → Ordinal → Ordinal
hι : Nonempty ι
f : ι → Ordinal → Ordinal
H : ∀ (i : ι), IsNormal (f i)
a b : Ordinal
⊢ (∀ (i : ι), f i b ≤ nfpFamily f a) ↔ b ≤ nfpFamily f a
refine' ⟨fun h => _, fun h i => _⟩
case refine'_2
ι : Type u
f✝ : ι → Ordinal → Ordinal
hι : Nonempty ι
f : ι → Ordinal → Ordinal
H : ∀ (i : ι), IsNormal (f i)
a b : Ordinal
h : b ≤ nfpFamily f a
i : ι
⊢ f i b ≤ f i (nfpFamily f a)
case refine'_2
ι : Type u
f✝ : ι → Ordinal → Ordinal
hι : Nonempty ι
f : ι → Ordinal → Ordinal
H : ∀ (i : ι), IsNormal (f i)
a b : Ordinal
h : b ≤ nfpFamily f a
i : ι
⊢ f i b ≤ nfpFamily f a
rw [← nfpFamily_fp (H i)]
no goals
case refine'_2
ι : Type u
f✝ : ι → Ordinal → Ordinal
hι : Nonempty ι
f : ι → Ordinal → Ordinal
H : ∀ (i : ι), IsNormal (f i)
a b : Ordinal
h : b ≤ nfpFamily f a
i : ι
⊢ f i b ≤ f i (nfpFamily f a)
exact (H i).monotone h
case refine'_1.intro
ι : Type u
f✝ f : ι → Ordinal → Ordinal
H : ∀ (i : ι), IsNormal (f i)
a b : Ordinal
h : ∀ (i : ι), f i b ≤ nfpFamily f a
i : ι
⊢ b ≤ nfpFamily f a
case refine'_1
ι : Type u
f✝ : ι → Ordinal → Ordinal
hι : Nonempty ι
f : ι → Ordinal → Ordinal
H : ∀ (i : ι), IsNormal (f i)
a b : Ordinal
h : ∀ (i : ι), f i b ≤ nfpFamily f a
⊢ b ≤ nfpFamily f a
cases' hι with i
no goals
case refine'_1.intro
ι : Type u
f✝ f : ι → Ordinal → Ordinal
H : ∀ (i : ι), IsNormal (f i)
a b : Ordinal
h : ∀ (i : ι), f i b ≤ nfpFamily f a
i : ι
⊢ b ≤ nfpFamily f a
exact ((H i).self_le b).trans (h i)