s : Set Ordinal
a : Ordinal
⊢ (∀ {ι : Type u}, Nonempty ι → ∀ (f : ι → Ordinal), (∀ (i : ι), f i ∈ s) → sup f ∈ s) ↔
    ∀ {o : Ordinal},
      o ≠ 0 → ∀ (f : (a : Ordinal) → a < o → Ordinal), (∀ (i : Ordinal) (hi : i < o), f i hi ∈ s) → bsup o f ∈ s
s : Set Ordinal
a : Ordinal
⊢ IsClosed s ↔
    ∀ {o : Ordinal},
      o ≠ 0 → ∀ (f : (a : Ordinal) → a < o → Ordinal), (∀ (i : Ordinal) (hi : i < o), f i hi ∈ s) → bsup o f ∈ s
rw [isClosed_iff_sup]
case refine'_1
s : Set Ordinal
a : Ordinal
H : ∀ {ι : Type u}, Nonempty ι → ∀ (f : ι → Ordinal), (∀ (i : ι), f i ∈ s) → sup f ∈ s
o : Ordinal
ho : o ≠ 0
f : (a : Ordinal) → a < o → Ordinal
hf : ∀ (i : Ordinal) (hi : i < o), f i hi ∈ s
⊢ ∀ (i : (Quotient.out o).α), familyOfBFamily o f i ∈ s

case refine'_2
s : Set Ordinal
a : Ordinal
H :
  ∀ {o : Ordinal},
    o ≠ 0 → ∀ (f : (a : Ordinal) → a < o → Ordinal), (∀ (i : Ordinal) (hi : i < o), f i hi ∈ s) → bsup o f ∈ s
ι : Type u
hι : Nonempty ι
f : ι → Ordinal
hf : ∀ (i : ι), f i ∈ s
⊢ sup f ∈ s
s : Set Ordinal
a : Ordinal
⊢ (∀ {ι : Type u}, Nonempty ι → ∀ (f : ι → Ordinal), (∀ (i : ι), f i ∈ s) → sup f ∈ s) ↔
    ∀ {o : Ordinal},
      o ≠ 0 → ∀ (f : (a : Ordinal) → a < o → Ordinal), (∀ (i : Ordinal) (hi : i < o), f i hi ∈ s) → bsup o f ∈ s
refine' ⟨fun H o ho f hf => H (out_nonempty_iff_ne_zero.2 ho) _ _, fun H ι hι f hf => _⟩
no goals
case refine'_1
s : Set Ordinal
a : Ordinal
H : ∀ {ι : Type u}, Nonempty ι → ∀ (f : ι → Ordinal), (∀ (i : ι), f i ∈ s) → sup f ∈ s
o : Ordinal
ho : o ≠ 0
f : (a : Ordinal) → a < o → Ordinal
hf : ∀ (i : Ordinal) (hi : i < o), f i hi ∈ s
⊢ ∀ (i : (Quotient.out o).α), familyOfBFamily o f i ∈ s
exact fun i => hf _ _
case refine'_2
s : Set Ordinal
a : Ordinal
H :
  ∀ {o : Ordinal},
    o ≠ 0 → ∀ (f : (a : Ordinal) → a < o → Ordinal), (∀ (i : Ordinal) (hi : i < o), f i hi ∈ s) → bsup o f ∈ s
ι : Type u
hι : Nonempty ι
f : ι → Ordinal
hf : ∀ (i : ι), f i ∈ s
⊢ bsup (type WellOrderingRel) (bfamilyOfFamily f) ∈ s
case refine'_2
s : Set Ordinal
a : Ordinal
H :
  ∀ {o : Ordinal},
    o ≠ 0 → ∀ (f : (a : Ordinal) → a < o → Ordinal), (∀ (i : Ordinal) (hi : i < o), f i hi ∈ s) → bsup o f ∈ s
ι : Type u
hι : Nonempty ι
f : ι → Ordinal
hf : ∀ (i : ι), f i ∈ s
⊢ sup f ∈ s
rw [← bsup_eq_sup]
case refine'_2.a
s : Set Ordinal
a : Ordinal
H :
  ∀ {o : Ordinal},
    o ≠ 0 → ∀ (f : (a : Ordinal) → a < o → Ordinal), (∀ (i : Ordinal) (hi : i < o), f i hi ∈ s) → bsup o f ∈ s
ι : Type u
hι : Nonempty ι
f : ι → Ordinal
hf : ∀ (i : ι), f i ∈ s
⊢ ∀ (i : Ordinal) (hi : i < type WellOrderingRel), bfamilyOfFamily f i hi ∈ s
case refine'_2
s : Set Ordinal
a : Ordinal
H :
  ∀ {o : Ordinal},
    o ≠ 0 → ∀ (f : (a : Ordinal) → a < o → Ordinal), (∀ (i : Ordinal) (hi : i < o), f i hi ∈ s) → bsup o f ∈ s
ι : Type u
hι : Nonempty ι
f : ι → Ordinal
hf : ∀ (i : ι), f i ∈ s
⊢ bsup (type WellOrderingRel) (bfamilyOfFamily f) ∈ s
apply H (type_ne_zero_iff_nonempty.2 hι)
no goals
case refine'_2.a
s : Set Ordinal
a : Ordinal
H :
  ∀ {o : Ordinal},
    o ≠ 0 → ∀ (f : (a : Ordinal) → a < o → Ordinal), (∀ (i : Ordinal) (hi : i < o), f i hi ∈ s) → bsup o f ∈ s
ι : Type u
hι : Nonempty ι
f : ι → Ordinal
hf : ∀ (i : ι), f i ∈ s
⊢ ∀ (i : Ordinal) (hi : i < type WellOrderingRel), bfamilyOfFamily f i hi ∈ s
exact fun i hi => hf _