α✝ : Type ?u.102030
β : Type ?u.102033
γ : Type ?u.102036
r✝ : α✝ → α✝ → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
α : Type u_1
r : α → α → Prop
x✝ : IsWellOrder α r
h : card (type r) = 0
this : IsEmpty { α := α, r := r, wo := x✝ }.α
⊢ type r = 0
α✝ : Type ?u.102030
β : Type ?u.102033
γ : Type ?u.102036
r✝ : α✝ → α✝ → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
α : Type u_1
r : α → α → Prop
x✝ : IsWellOrder α r
h : card (type r) = 0
⊢ type r = 0
haveI := Cardinal.mk_eq_zero_iff.1 h
no goals
α✝ : Type ?u.102030
β : Type ?u.102033
γ : Type ?u.102036
r✝ : α✝ → α✝ → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
α : Type u_1
r : α → α → Prop
x✝ : IsWellOrder α r
h : card (type r) = 0
this : IsEmpty { α := α, r := r, wo := x✝ }.α
⊢ type r = 0
apply type_eq_zero_of_empty
no goals
α : Type ?u.102030
β : Type ?u.102033
γ : Type ?u.102036
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
e : o = 0
⊢ card o = 0
simp only [e, card_zero]