case intro
α : Type ?u.305800
β : Type ?u.305803
γ : Type ?u.305806
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι ι' : Type u
r : ι → ι → Prop
r' : ι' → ι' → Prop
inst✝¹ : IsWellOrder ι r
inst✝ : IsWellOrder ι' r'
o : Ordinal
ho : type r = o
ho' : type r' = o
f : (a : Ordinal) → a < o → Ordinal
i : ι
j : ι'
hj : typein r' j = typein r i
⊢ familyOfBFamily' r ho f i ≤ sup (familyOfBFamily' r' ho' f)
α : Type ?u.305800
β : Type ?u.305803
γ : Type ?u.305806
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι ι' : Type u
r : ι → ι → Prop
r' : ι' → ι' → Prop
inst✝¹ : IsWellOrder ι r
inst✝ : IsWellOrder ι' r'
o : Ordinal
ho : type r = o
ho' : type r' = o
f : (a : Ordinal) → a < o → Ordinal
i : ι
⊢ familyOfBFamily' r ho f i ≤ sup (familyOfBFamily' r' ho' f)
cases'
  typein_surj r'
    (by
      rw [ho', ← ho]
      exact typein_lt_type r i) with
  j hj
case intro
α : Type ?u.305800
β : Type ?u.305803
γ : Type ?u.305806
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι ι' : Type u
r : ι → ι → Prop
r' : ι' → ι' → Prop
inst✝¹ : IsWellOrder ι r
inst✝ : IsWellOrder ι' r'
o : Ordinal
ho : type r = o
ho' : type r' = o
f : (a : Ordinal) → a < o → Ordinal
i : ι
j : ι'
hj : typein r' j = typein r i
⊢ f (typein r' j) (_ : typein r' j < o) ≤ sup fun i => f (typein r' i) (_ : typein r' i < o)
case intro
α : Type ?u.305800
β : Type ?u.305803
γ : Type ?u.305806
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι ι' : Type u
r : ι → ι → Prop
r' : ι' → ι' → Prop
inst✝¹ : IsWellOrder ι r
inst✝ : IsWellOrder ι' r'
o : Ordinal
ho : type r = o
ho' : type r' = o
f : (a : Ordinal) → a < o → Ordinal
i : ι
j : ι'
hj : typein r' j = typein r i
⊢ familyOfBFamily' r ho f i ≤ sup (familyOfBFamily' r' ho' f)
simp_rw [familyOfBFamily', ← hj]
no goals
case intro
α : Type ?u.305800
β : Type ?u.305803
γ : Type ?u.305806
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι ι' : Type u
r : ι → ι → Prop
r' : ι' → ι' → Prop
inst✝¹ : IsWellOrder ι r
inst✝ : IsWellOrder ι' r'
o : Ordinal
ho : type r = o
ho' : type r' = o
f : (a : Ordinal) → a < o → Ordinal
i : ι
j : ι'
hj : typein r' j = typein r i
⊢ f (typein r' j) (_ : typein r' j < o) ≤ sup fun i => f (typein r' i) (_ : typein r' i < o)
apply le_sup
α : Type ?u.305800
β : Type ?u.305803
γ : Type ?u.305806
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι ι' : Type u
r : ι → ι → Prop
r' : ι' → ι' → Prop
inst✝¹ : IsWellOrder ι r
inst✝ : IsWellOrder ι' r'
o : Ordinal
ho : type r = o
ho' : type r' = o
f : (a : Ordinal) → a < o → Ordinal
i : ι
⊢ ?m.306085 < type r

α : Type ?u.305800
β : Type ?u.305803
γ : Type ?u.305806
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι ι' : Type u
r : ι → ι → Prop
r' : ι' → ι' → Prop
inst✝¹ : IsWellOrder ι r
inst✝ : IsWellOrder ι' r'
o : Ordinal
ho : type r = o
ho' : type r' = o
f : (a : Ordinal) → a < o → Ordinal
i : ι
⊢ Ordinal

α : Type ?u.305800
β : Type ?u.305803
γ : Type ?u.305806
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι ι' : Type u
r : ι → ι → Prop
r' : ι' → ι' → Prop
inst✝¹ : IsWellOrder ι r
inst✝ : IsWellOrder ι' r'
o : Ordinal
ho : type r = o
ho' : type r' = o
f : (a : Ordinal) → a < o → Ordinal
i : ι
⊢ Ordinal
α : Type ?u.305800
β : Type ?u.305803
γ : Type ?u.305806
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι ι' : Type u
r : ι → ι → Prop
r' : ι' → ι' → Prop
inst✝¹ : IsWellOrder ι r
inst✝ : IsWellOrder ι' r'
o : Ordinal
ho : type r = o
ho' : type r' = o
f : (a : Ordinal) → a < o → Ordinal
i : ι
⊢ ?m.306085 < type r'
rw [ho', ← ho]
no goals
α : Type ?u.305800
β : Type ?u.305803
γ : Type ?u.305806
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι ι' : Type u
r : ι → ι → Prop
r' : ι' → ι' → Prop
inst✝¹ : IsWellOrder ι r
inst✝ : IsWellOrder ι' r'
o : Ordinal
ho : type r = o
ho' : type r' = o
f : (a : Ordinal) → a < o → Ordinal
i : ι
⊢ ?m.306085 < type r

α : Type ?u.305800
β : Type ?u.305803
γ : Type ?u.305806
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι ι' : Type u
r : ι → ι → Prop
r' : ι' → ι' → Prop
inst✝¹ : IsWellOrder ι r
inst✝ : IsWellOrder ι' r'
o : Ordinal
ho : type r = o
ho' : type r' = o
f : (a : Ordinal) → a < o → Ordinal
i : ι
⊢ Ordinal

α : Type ?u.305800
β : Type ?u.305803
γ : Type ?u.305806
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι ι' : Type u
r : ι → ι → Prop
r' : ι' → ι' → Prop
inst✝¹ : IsWellOrder ι r
inst✝ : IsWellOrder ι' r'
o : Ordinal
ho : type r = o
ho' : type r' = o
f : (a : Ordinal) → a < o → Ordinal
i : ι
⊢ Ordinal
exact typein_lt_type r i