α : Type ?u.309348
β : Type ?u.309351
γ : Type ?u.309354
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
f : (a : Ordinal) → a < o → Ordinal
a : Ordinal
h : ∀ (i : (Quotient.out o).α), familyOfBFamily o f i ≤ a
i : Ordinal
hi : i < o
⊢ familyOfBFamily o f (enum (fun x x_1 => x < x_1) i (_ : i < type fun x x_1 => x < x_1)) ≤ a
α : Type ?u.309348
β : Type ?u.309351
γ : Type ?u.309354
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
f : (a : Ordinal) → a < o → Ordinal
a : Ordinal
h : ∀ (i : (Quotient.out o).α), familyOfBFamily o f i ≤ a
i : Ordinal
hi : i < o
⊢ f i hi ≤ a
rw [← familyOfBFamily_enum o f]
no goals
α : Type ?u.309348
β : Type ?u.309351
γ : Type ?u.309354
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
f : (a : Ordinal) → a < o → Ordinal
a : Ordinal
h : ∀ (i : (Quotient.out o).α), familyOfBFamily o f i ≤ a
i : Ordinal
hi : i < o
⊢ familyOfBFamily o f (enum (fun x x_1 => x < x_1) i (_ : i < type fun x x_1 => x < x_1)) ≤ a
exact h _