case mk
α : Type ?u.23052
β : Type ?u.23055
γ : Type ?u.23058
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
α✝ : Type u_1
r✝ : α✝ → α✝ → Prop
wo✝ : IsWellOrder α✝ r✝
⊢ Quotient.mk isEquivalent { α := α✝, r := r✝, wo := wo✝ } = type { α := α✝, r := r✝, wo := wo✝ }.r
α : Type ?u.23052
β : Type ?u.23055
γ : Type ?u.23058
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
w : WellOrder
⊢ Quotient.mk isEquivalent w = type w.r
cases w
no goals
case mk
α : Type ?u.23052
β : Type ?u.23055
γ : Type ?u.23058
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
α✝ : Type u_1
r✝ : α✝ → α✝ → Prop
wo✝ : IsWellOrder α✝ r✝
⊢ Quotient.mk isEquivalent { α := α✝, r := r✝, wo := wo✝ } = type { α := α✝, r := r✝, wo := wo✝ }.r
rfl