case intro.intro
α : Type ?u.360714
β : Type ?u.360717
γ : Type ?u.360720
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
o' : Ordinal
f : (a : Ordinal) → a < o → Ordinal
g : (a : Ordinal) → a < o' → Ordinal
h : brange o f ⊆ brange o' g
a : Ordinal
x✝ : a ∈ brange o fun a ha => succ (f a ha)
b : Ordinal
hb : b < o
hb' : (fun a ha => succ (f a ha)) b hb = a
c : Ordinal
hc : c < o'
hc' : g c hc = f b hb
⊢ a ∈ brange o' fun a ha => succ (g a ha)
α : Type ?u.360714
β : Type ?u.360717
γ : Type ?u.360720
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
o' : Ordinal
f : (a : Ordinal) → a < o → Ordinal
g : (a : Ordinal) → a < o' → Ordinal
h : brange o f ⊆ brange o' g
a : Ordinal
x✝ : a ∈ brange o fun a ha => succ (f a ha)
b : Ordinal
hb : b < o
hb' : (fun a ha => succ (f a ha)) b hb = a
⊢ a ∈ brange o' fun a ha => succ (g a ha)
obtain ⟨c, hc, hc'⟩ := h ⟨b, hb, rfl⟩
case intro.intro
α : Type ?u.360714
β : Type ?u.360717
γ : Type ?u.360720
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
o' : Ordinal
f : (a : Ordinal) → a < o → Ordinal
g : (a : Ordinal) → a < o' → Ordinal
h : brange o f ⊆ brange o' g
a : Ordinal
x✝ : a ∈ brange o fun a ha => succ (f a ha)
b : Ordinal
hb : b < o
c : Ordinal
hc : c < o'
hc' : g c hc = f b hb
hb' : succ (g c hc) = a
⊢ a ∈ brange o' fun a ha => succ (g a ha)
case intro.intro
α : Type ?u.360714
β : Type ?u.360717
γ : Type ?u.360720
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
o' : Ordinal
f : (a : Ordinal) → a < o → Ordinal
g : (a : Ordinal) → a < o' → Ordinal
h : brange o f ⊆ brange o' g
a : Ordinal
x✝ : a ∈ brange o fun a ha => succ (f a ha)
b : Ordinal
hb : b < o
hb' : (fun a ha => succ (f a ha)) b hb = a
c : Ordinal
hc : c < o'
hc' : g c hc = f b hb
⊢ a ∈ brange o' fun a ha => succ (g a ha)
simp_rw [← hc'] at hb'
no goals
case intro.intro
α : Type ?u.360714
β : Type ?u.360717
γ : Type ?u.360720
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
o' : Ordinal
f : (a : Ordinal) → a < o → Ordinal
g : (a : Ordinal) → a < o' → Ordinal
h : brange o f ⊆ brange o' g
a : Ordinal
x✝ : a ∈ brange o fun a ha => succ (f a ha)
b : Ordinal
hb : b < o
c : Ordinal
hc : c < o'
hc' : g c hc = f b hb
hb' : succ (g c hc) = a
⊢ a ∈ brange o' fun a ha => succ (g a ha)
exact ⟨c, hc, hb'⟩