case inr
α : Type ?u.345179
β : Type ?u.345182
γ : Type ?u.345185
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
h : succ (sup (typein fun x x_1 => x < x_1)) = lsub (typein fun x x_1 => x < x_1)
⊢ lsub (typein fun x x_1 => x < x_1) = succ o
case inr
α : Type ?u.345179
β : Type ?u.345182
γ : Type ?u.345185
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
h : succ (sup (typein fun x x_1 => x < x_1)) = lsub (typein fun x x_1 => x < x_1)
⊢ sup (typein fun x x_1 => x < x_1) = o
rw [← succ_eq_succ_iff, h]
no goals
case inr
α : Type ?u.345179
β : Type ?u.345182
γ : Type ?u.345185
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
h : succ (sup (typein fun x x_1 => x < x_1)) = lsub (typein fun x x_1 => x < x_1)
⊢ lsub (typein fun x x_1 => x < x_1) = succ o
apply lsub_typein
case inl
α : Type ?u.345179
β : Type ?u.345182
γ : Type ?u.345185
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
h : ∀ (a : Ordinal), a < lsub (typein fun x x_1 => x < x_1) → succ a < lsub (typein fun x x_1 => x < x_1)
⊢ sup (typein fun x x_1 => x < x_1) = o
case inl
α : Type ?u.345179
β : Type ?u.345182
γ : Type ?u.345185
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
h : sup (typein fun x x_1 => x < x_1) = lsub (typein fun x x_1 => x < x_1)
⊢ sup (typein fun x x_1 => x < x_1) = o
rw [sup_eq_lsub_iff_succ] at h
case inl
α : Type ?u.345179
β : Type ?u.345182
γ : Type ?u.345185
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
h : ∀ (a : Ordinal), a < succ o → succ a < succ o
⊢ sup (typein fun x x_1 => x < x_1) = o
case inl
α : Type ?u.345179
β : Type ?u.345182
γ : Type ?u.345185
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
h : ∀ (a : Ordinal), a < lsub (typein fun x x_1 => x < x_1) → succ a < lsub (typein fun x x_1 => x < x_1)
⊢ sup (typein fun x x_1 => x < x_1) = o
simp only [lsub_typein] at h
no goals
case inl
α : Type ?u.345179
β : Type ?u.345182
γ : Type ?u.345185
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
h : ∀ (a : Ordinal), a < succ o → succ a < succ o
⊢ sup (typein fun x x_1 => x < x_1) = o
exact (h o (lt_succ o)).false.elim