α✝ : Type ?u.358821
β : Type ?u.358824
γ : Type ?u.358827
r✝ : α✝ → α✝ → Prop
s : β → β → Prop
t : γ → γ → Prop
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
f : (a : Ordinal) → a < type r → Ordinal
o : Ordinal
⊢ (∀ (i : Ordinal) (h : i < type r), f i h < o) ↔ ∀ (i : α), f (typein r i) (_ : typein r i < type r) < o
α✝ : Type ?u.358821
β : Type ?u.358824
γ : Type ?u.358827
r✝ : α✝ → α✝ → Prop
s : β → β → Prop
t : γ → γ → Prop
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
f : (a : Ordinal) → a < type r → Ordinal
o : Ordinal
⊢ blsub (type r) f ≤ o ↔ (lsub fun a => f (typein r a) (_ : typein r a < type r)) ≤ o
rw [blsub_le_iff, lsub_le_iff]
no goals
α✝ : Type ?u.358821
β : Type ?u.358824
γ : Type ?u.358827
r✝ : α✝ → α✝ → Prop
s : β → β → Prop
t : γ → γ → Prop
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
f : (a : Ordinal) → a < type r → Ordinal
o : Ordinal
⊢ (∀ (i : Ordinal) (h : i < type r), f i h < o) ↔ ∀ (i : α), f (typein r i) (_ : typein r i < type r) < o
exact ⟨fun H b => H _ _, fun H i h => by simpa only [typein_enum] using H (enum r i h)⟩
no goals
α✝ : Type ?u.358821
β : Type ?u.358824
γ : Type ?u.358827
r✝ : α✝ → α✝ → Prop
s : β → β → Prop
t : γ → γ → Prop
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
f : (a : Ordinal) → a < type r → Ordinal
o : Ordinal
H : ∀ (i : α), f (typein r i) (_ : typein r i < type r) < o
i : Ordinal
h : i < type r
⊢ f i h < o
simpa only [typein_enum] using H (enum r i h)