no goals
α : Type ?u.110781
β : Type ?u.110784
γ : Type ?u.110787
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : Ordinal → Ordinal
o : Ordinal
H : IsNormal f
p : Set Ordinal
p0 : Set.Nonempty p
b : Ordinal
H₂ : ∀ (o : Ordinal), b ≤ o ↔ ∀ (a : Ordinal), a ∈ p → a ≤ o
h : ∀ (a : Ordinal), a ∈ p → f a ≤ o
⊢ f b ≤ o
induction b using limitRecOn with
| H₁ =>
  cases' p0 with x px
  have := Ordinal.le_zero.1 ((H₂ _).1 (Ordinal.zero_le _) _ px)
  rw [this] at px
  exact h _ px
| H₂ S _ =>
  rcases not_ball.1 (mt (H₂ S).2 <| (lt_succ S).not_le) with ⟨a, h₁, h₂⟩
  exact (H.le_iff.2 <| succ_le_of_lt <| not_le.1 h₂).trans (h _ h₁)
| H₃ S L _ =>
  refine' (H.2 _ L _).2 fun a h' => _
  rcases not_ball.1 (mt (H₂ a).2 h'.not_le) with ⟨b, h₁, h₂⟩
  exact (H.le_iff.2 <| (not_le.1 h₂).le).trans (h _ h₁)
case H₁.intro
α : Type ?u.110781
β : Type ?u.110784
γ : Type ?u.110787
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : Ordinal → Ordinal
o : Ordinal
H : IsNormal f
p : Set Ordinal
h : ∀ (a : Ordinal), a ∈ p → f a ≤ o
H₂ : ∀ (o : Ordinal), 0 ≤ o ↔ ∀ (a : Ordinal), a ∈ p → a ≤ o
x : Ordinal
px : x ∈ p
⊢ f 0 ≤ o
case H₁
α : Type ?u.110781
β : Type ?u.110784
γ : Type ?u.110787
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : Ordinal → Ordinal
o : Ordinal
H : IsNormal f
p : Set Ordinal
p0 : Set.Nonempty p
h : ∀ (a : Ordinal), a ∈ p → f a ≤ o
H₂ : ∀ (o : Ordinal), 0 ≤ o ↔ ∀ (a : Ordinal), a ∈ p → a ≤ o
⊢ f 0 ≤ o
cases' p0 with x px
case H₁.intro
α : Type ?u.110781
β : Type ?u.110784
γ : Type ?u.110787
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : Ordinal → Ordinal
o : Ordinal
H : IsNormal f
p : Set Ordinal
h : ∀ (a : Ordinal), a ∈ p → f a ≤ o
H₂ : ∀ (o : Ordinal), 0 ≤ o ↔ ∀ (a : Ordinal), a ∈ p → a ≤ o
x : Ordinal
px : x ∈ p
this : x = 0
⊢ f 0 ≤ o
case H₁.intro
α : Type ?u.110781
β : Type ?u.110784
γ : Type ?u.110787
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : Ordinal → Ordinal
o : Ordinal
H : IsNormal f
p : Set Ordinal
h : ∀ (a : Ordinal), a ∈ p → f a ≤ o
H₂ : ∀ (o : Ordinal), 0 ≤ o ↔ ∀ (a : Ordinal), a ∈ p → a ≤ o
x : Ordinal
px : x ∈ p
⊢ f 0 ≤ o
have := Ordinal.le_zero.1 ((H₂ _).1 (Ordinal.zero_le _) _ px)
case H₁.intro
α : Type ?u.110781
β : Type ?u.110784
γ : Type ?u.110787
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : Ordinal → Ordinal
o : Ordinal
H : IsNormal f
p : Set Ordinal
h : ∀ (a : Ordinal), a ∈ p → f a ≤ o
H₂ : ∀ (o : Ordinal), 0 ≤ o ↔ ∀ (a : Ordinal), a ∈ p → a ≤ o
x : Ordinal
px : 0 ∈ p
this : x = 0
⊢ f 0 ≤ o
case H₁.intro
α : Type ?u.110781
β : Type ?u.110784
γ : Type ?u.110787
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : Ordinal → Ordinal
o : Ordinal
H : IsNormal f
p : Set Ordinal
h : ∀ (a : Ordinal), a ∈ p → f a ≤ o
H₂ : ∀ (o : Ordinal), 0 ≤ o ↔ ∀ (a : Ordinal), a ∈ p → a ≤ o
x : Ordinal
px : x ∈ p
this : x = 0
⊢ f 0 ≤ o
rw [this] at px
no goals
case H₁.intro
α : Type ?u.110781
β : Type ?u.110784
γ : Type ?u.110787
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : Ordinal → Ordinal
o : Ordinal
H : IsNormal f
p : Set Ordinal
h : ∀ (a : Ordinal), a ∈ p → f a ≤ o
H₂ : ∀ (o : Ordinal), 0 ≤ o ↔ ∀ (a : Ordinal), a ∈ p → a ≤ o
x : Ordinal
px : 0 ∈ p
this : x = 0
⊢ f 0 ≤ o
exact h _ px
case H₂.intro.intro
α : Type ?u.110781
β : Type ?u.110784
γ : Type ?u.110787
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : Ordinal → Ordinal
o : Ordinal
H : IsNormal f
p : Set Ordinal
p0 : Set.Nonempty p
h : ∀ (a : Ordinal), a ∈ p → f a ≤ o
S : Ordinal
a✝ : (∀ (o : Ordinal), S ≤ o ↔ ∀ (a : Ordinal), a ∈ p → a ≤ o) → f S ≤ o
H₂ : ∀ (o : Ordinal), succ S ≤ o ↔ ∀ (a : Ordinal), a ∈ p → a ≤ o
a : Ordinal
h₁ : a ∈ p
h₂ : ¬a ≤ S
⊢ f (succ S) ≤ o
case H₂
α : Type ?u.110781
β : Type ?u.110784
γ : Type ?u.110787
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : Ordinal → Ordinal
o : Ordinal
H : IsNormal f
p : Set Ordinal
p0 : Set.Nonempty p
h : ∀ (a : Ordinal), a ∈ p → f a ≤ o
S : Ordinal
a✝ : (∀ (o : Ordinal), S ≤ o ↔ ∀ (a : Ordinal), a ∈ p → a ≤ o) → f S ≤ o
H₂ : ∀ (o : Ordinal), succ S ≤ o ↔ ∀ (a : Ordinal), a ∈ p → a ≤ o
⊢ f (succ S) ≤ o
rcases not_ball.1 (mt (H₂ S).2 <| (lt_succ S).not_le) with ⟨a, h₁, h₂⟩
no goals
case H₂.intro.intro
α : Type ?u.110781
β : Type ?u.110784
γ : Type ?u.110787
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : Ordinal → Ordinal
o : Ordinal
H : IsNormal f
p : Set Ordinal
p0 : Set.Nonempty p
h : ∀ (a : Ordinal), a ∈ p → f a ≤ o
S : Ordinal
a✝ : (∀ (o : Ordinal), S ≤ o ↔ ∀ (a : Ordinal), a ∈ p → a ≤ o) → f S ≤ o
H₂ : ∀ (o : Ordinal), succ S ≤ o ↔ ∀ (a : Ordinal), a ∈ p → a ≤ o
a : Ordinal
h₁ : a ∈ p
h₂ : ¬a ≤ S
⊢ f (succ S) ≤ o
exact (H.le_iff.2 <| succ_le_of_lt <| not_le.1 h₂).trans (h _ h₁)
case H₃
α : Type ?u.110781
β : Type ?u.110784
γ : Type ?u.110787
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : Ordinal → Ordinal
o : Ordinal
H : IsNormal f
p : Set Ordinal
p0 : Set.Nonempty p
h : ∀ (a : Ordinal), a ∈ p → f a ≤ o
S : Ordinal
L : IsLimit S
a✝ : ∀ (o' : Ordinal), o' < S → (∀ (o : Ordinal), o' ≤ o ↔ ∀ (a : Ordinal), a ∈ p → a ≤ o) → f o' ≤ o
H₂ : ∀ (o : Ordinal), S ≤ o ↔ ∀ (a : Ordinal), a ∈ p → a ≤ o
a : Ordinal
h' : a < S
⊢ f a ≤ o
case H₃
α : Type ?u.110781
β : Type ?u.110784
γ : Type ?u.110787
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : Ordinal → Ordinal
o : Ordinal
H : IsNormal f
p : Set Ordinal
p0 : Set.Nonempty p
h : ∀ (a : Ordinal), a ∈ p → f a ≤ o
S : Ordinal
L : IsLimit S
a✝ : ∀ (o' : Ordinal), o' < S → (∀ (o : Ordinal), o' ≤ o ↔ ∀ (a : Ordinal), a ∈ p → a ≤ o) → f o' ≤ o
H₂ : ∀ (o : Ordinal), S ≤ o ↔ ∀ (a : Ordinal), a ∈ p → a ≤ o
⊢ f S ≤ o
refine' (H.2 _ L _).2 fun a h' => _
case H₃.intro.intro
α : Type ?u.110781
β : Type ?u.110784
γ : Type ?u.110787
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : Ordinal → Ordinal
o : Ordinal
H : IsNormal f
p : Set Ordinal
p0 : Set.Nonempty p
h : ∀ (a : Ordinal), a ∈ p → f a ≤ o
S : Ordinal
L : IsLimit S
a✝ : ∀ (o' : Ordinal), o' < S → (∀ (o : Ordinal), o' ≤ o ↔ ∀ (a : Ordinal), a ∈ p → a ≤ o) → f o' ≤ o
H₂ : ∀ (o : Ordinal), S ≤ o ↔ ∀ (a : Ordinal), a ∈ p → a ≤ o
a : Ordinal
h' : a < S
b : Ordinal
h₁ : b ∈ p
h₂ : ¬b ≤ a
⊢ f a ≤ o
case H₃
α : Type ?u.110781
β : Type ?u.110784
γ : Type ?u.110787
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : Ordinal → Ordinal
o : Ordinal
H : IsNormal f
p : Set Ordinal
p0 : Set.Nonempty p
h : ∀ (a : Ordinal), a ∈ p → f a ≤ o
S : Ordinal
L : IsLimit S
a✝ : ∀ (o' : Ordinal), o' < S → (∀ (o : Ordinal), o' ≤ o ↔ ∀ (a : Ordinal), a ∈ p → a ≤ o) → f o' ≤ o
H₂ : ∀ (o : Ordinal), S ≤ o ↔ ∀ (a : Ordinal), a ∈ p → a ≤ o
a : Ordinal
h' : a < S
⊢ f a ≤ o
rcases not_ball.1 (mt (H₂ a).2 h'.not_le) with ⟨b, h₁, h₂⟩
no goals
case H₃.intro.intro
α : Type ?u.110781
β : Type ?u.110784
γ : Type ?u.110787
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : Ordinal → Ordinal
o : Ordinal
H : IsNormal f
p : Set Ordinal
p0 : Set.Nonempty p
h : ∀ (a : Ordinal), a ∈ p → f a ≤ o
S : Ordinal
L : IsLimit S
a✝ : ∀ (o' : Ordinal), o' < S → (∀ (o : Ordinal), o' ≤ o ↔ ∀ (a : Ordinal), a ∈ p → a ≤ o) → f o' ≤ o
H₂ : ∀ (o : Ordinal), S ≤ o ↔ ∀ (a : Ordinal), a ∈ p → a ≤ o
a : Ordinal
h' : a < S
b : Ordinal
h₁ : b ∈ p
h₂ : ¬b ≤ a
⊢ f a ≤ o
exact (H.le_iff.2 <| (not_le.1 h₂).le).trans (h _ h₁)