case pos
ι : Type u
f : ι → Ordinal → Ordinal
H : ∀ (i : ι), Monotone (f i)
a b : Ordinal
ab : a ≤ b
h : ∀ (i : ι), f i b ≤ b
l : List ι
hι : IsEmpty ι
⊢ List.foldr f a l ≤ b

case neg
ι : Type u
f : ι → Ordinal → Ordinal
H : ∀ (i : ι), Monotone (f i)
a b : Ordinal
ab : a ≤ b
h : ∀ (i : ι), f i b ≤ b
l : List ι
hι : ¬IsEmpty ι
⊢ List.foldr f a l ≤ b
ι : Type u
f : ι → Ordinal → Ordinal
H : ∀ (i : ι), Monotone (f i)
a b : Ordinal
ab : a ≤ b
h : ∀ (i : ι), f i b ≤ b
l : List ι
⊢ List.foldr f a l ≤ b
by_cases hι : IsEmpty ι
no goals
case pos
ι : Type u
f : ι → Ordinal → Ordinal
H : ∀ (i : ι), Monotone (f i)
a b : Ordinal
ab : a ≤ b
h : ∀ (i : ι), f i b ≤ b
l : List ι
hι : IsEmpty ι
⊢ List.foldr f a l ≤ b
rwa [Unique.eq_default l]
case neg.nil
ι : Type u
f : ι → Ordinal → Ordinal
H : ∀ (i : ι), Monotone (f i)
a✝ b : Ordinal
ab✝ : a✝ ≤ b
h : ∀ (i : ι), f i b ≤ b
hι : ¬IsEmpty ι
a : Ordinal
ab : a ≤ b
⊢ List.foldr f a [] ≤ b

case neg.cons
ι : Type u
f : ι → Ordinal → Ordinal
H : ∀ (i : ι), Monotone (f i)
a✝ b : Ordinal
ab✝ : a✝ ≤ b
h : ∀ (i : ι), f i b ≤ b
hι : ¬IsEmpty ι
i : ι
l : List ι
IH : ∀ {a : Ordinal}, a ≤ b → List.foldr f a l ≤ b
a : Ordinal
ab : a ≤ b
⊢ List.foldr f a (i :: l) ≤ b
case neg
ι : Type u
f : ι → Ordinal → Ordinal
H : ∀ (i : ι), Monotone (f i)
a b : Ordinal
ab : a ≤ b
h : ∀ (i : ι), f i b ≤ b
l : List ι
hι : ¬IsEmpty ι
⊢ List.foldr f a l ≤ b
induction' l with i l IH generalizing a
no goals
case neg.cons
ι : Type u
f : ι → Ordinal → Ordinal
H : ∀ (i : ι), Monotone (f i)
a✝ b : Ordinal
ab✝ : a✝ ≤ b
h : ∀ (i : ι), f i b ≤ b
hι : ¬IsEmpty ι
i : ι
l : List ι
IH : ∀ {a : Ordinal}, a ≤ b → List.foldr f a l ≤ b
a : Ordinal
ab : a ≤ b
⊢ List.foldr f a (i :: l) ≤ b
exact (H i (IH ab)).trans (h i)
no goals
case neg.nil
ι : Type u
f : ι → Ordinal → Ordinal
H : ∀ (i : ι), Monotone (f i)
a✝ b : Ordinal
ab✝ : a✝ ≤ b
h : ∀ (i : ι), f i b ≤ b
hι : ¬IsEmpty ι
a : Ordinal
ab : a ≤ b
⊢ List.foldr f a [] ≤ b
exact ab