case refine'_1
α : Type ?u.32966
r : α → α → Prop
ι : Type u
f : ι → Ordinal → Ordinal
c : Ordinal
hc : ℵ₀ < cof c
hc' : Cardinal.lift (#ι) < cof c
hf : ∀ (i : ι) (b : Ordinal), b < c → f i b < c
a : Ordinal
ha : a < c
⊢ Cardinal.lift (max ℵ₀ (#ι)) < cof c

case refine'_2
α : Type ?u.32966
r : α → α → Prop
ι : Type u
f : ι → Ordinal → Ordinal
c : Ordinal
hc : ℵ₀ < cof c
hc' : Cardinal.lift (#ι) < cof c
hf : ∀ (i : ι) (b : Ordinal), b < c → f i b < c
a : Ordinal
ha : a < c
l : List ι
⊢ List.foldr f a l < c
α : Type ?u.32966
r : α → α → Prop
ι : Type u
f : ι → Ordinal → Ordinal
c : Ordinal
hc : ℵ₀ < cof c
hc' : Cardinal.lift (#ι) < cof c
hf : ∀ (i : ι) (b : Ordinal), b < c → f i b < c
a : Ordinal
ha : a < c
⊢ nfpFamily f a < c
refine' sup_lt_ord_lift ((Cardinal.lift_le.2 (mk_list_le_max ι)).trans_lt _) fun l => _
case refine'_1
α : Type ?u.32966
r : α → α → Prop
ι : Type u
f : ι → Ordinal → Ordinal
c : Ordinal
hc : ℵ₀ < cof c
hc' : Cardinal.lift (#ι) < cof c
hf : ∀ (i : ι) (b : Ordinal), b < c → f i b < c
a : Ordinal
ha : a < c
⊢ max (Cardinal.lift ℵ₀) (Cardinal.lift (#ι)) < cof c
case refine'_1
α : Type ?u.32966
r : α → α → Prop
ι : Type u
f : ι → Ordinal → Ordinal
c : Ordinal
hc : ℵ₀ < cof c
hc' : Cardinal.lift (#ι) < cof c
hf : ∀ (i : ι) (b : Ordinal), b < c → f i b < c
a : Ordinal
ha : a < c
⊢ Cardinal.lift (max ℵ₀ (#ι)) < cof c
rw [lift_max]
α : Type ?u.32966
r : α → α → Prop
ι : Type u
f : ι → Ordinal → Ordinal
c : Ordinal
hc : ℵ₀ < cof c
hc' : Cardinal.lift (#ι) < cof c
hf : ∀ (i : ι) (b : Ordinal), b < c → f i b < c
a : Ordinal
ha : a < c
⊢ Cardinal.lift ℵ₀ < cof c
case refine'_1
α : Type ?u.32966
r : α → α → Prop
ι : Type u
f : ι → Ordinal → Ordinal
c : Ordinal
hc : ℵ₀ < cof c
hc' : Cardinal.lift (#ι) < cof c
hf : ∀ (i : ι) (b : Ordinal), b < c → f i b < c
a : Ordinal
ha : a < c
⊢ max (Cardinal.lift ℵ₀) (Cardinal.lift (#ι)) < cof c
apply max_lt _ hc'
no goals
α : Type ?u.32966
r : α → α → Prop
ι : Type u
f : ι → Ordinal → Ordinal
c : Ordinal
hc : ℵ₀ < cof c
hc' : Cardinal.lift (#ι) < cof c
hf : ∀ (i : ι) (b : Ordinal), b < c → f i b < c
a : Ordinal
ha : a < c
⊢ Cardinal.lift ℵ₀ < cof c
rwa [Cardinal.lift_aleph0]
case refine'_2.nil
α : Type ?u.32966
r : α → α → Prop
ι : Type u
f : ι → Ordinal → Ordinal
c : Ordinal
hc : ℵ₀ < cof c
hc' : Cardinal.lift (#ι) < cof c
hf : ∀ (i : ι) (b : Ordinal), b < c → f i b < c
a : Ordinal
ha : a < c
⊢ List.foldr f a [] < c

case refine'_2.cons
α : Type ?u.32966
r : α → α → Prop
ι : Type u
f : ι → Ordinal → Ordinal
c : Ordinal
hc : ℵ₀ < cof c
hc' : Cardinal.lift (#ι) < cof c
hf : ∀ (i : ι) (b : Ordinal), b < c → f i b < c
a : Ordinal
ha : a < c
i : ι
l : List ι
H : List.foldr f a l < c
⊢ List.foldr f a (i :: l) < c
case refine'_2
α : Type ?u.32966
r : α → α → Prop
ι : Type u
f : ι → Ordinal → Ordinal
c : Ordinal
hc : ℵ₀ < cof c
hc' : Cardinal.lift (#ι) < cof c
hf : ∀ (i : ι) (b : Ordinal), b < c → f i b < c
a : Ordinal
ha : a < c
l : List ι
⊢ List.foldr f a l < c
induction' l with i l H
no goals
case refine'_2.nil
α : Type ?u.32966
r : α → α → Prop
ι : Type u
f : ι → Ordinal → Ordinal
c : Ordinal
hc : ℵ₀ < cof c
hc' : Cardinal.lift (#ι) < cof c
hf : ∀ (i : ι) (b : Ordinal), b < c → f i b < c
a : Ordinal
ha : a < c
⊢ List.foldr f a [] < c
exact ha
no goals
case refine'_2.cons
α : Type ?u.32966
r : α → α → Prop
ι : Type u
f : ι → Ordinal → Ordinal
c : Ordinal
hc : ℵ₀ < cof c
hc' : Cardinal.lift (#ι) < cof c
hf : ∀ (i : ι) (b : Ordinal), b < c → f i b < c
a : Ordinal
ha : a < c
i : ι
l : List ι
H : List.foldr f a l < c
⊢ List.foldr f a (i :: l) < c
exact hf _ _ H