α : Type u_1
β : Type ?u.198351
γ : Type ?u.198354
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
o₁ o₂ : Ordinal
h₁ : o₁ < type r
h₂ : o₂ < type r
h : enum r o₁ h₁ = enum r o₂ h₂
hne : ¬o₁ = o₂
⊢ False
α : Type u_1
β : Type ?u.198351
γ : Type ?u.198354
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
o₁ o₂ : Ordinal
h₁ : o₁ < type r
h₂ : o₂ < type r
h : enum r o₁ h₁ = enum r o₂ h₂
⊢ o₁ = o₂
by_contra hne
α : Type u_1
β : Type ?u.198351
γ : Type ?u.198354
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
o₁ o₂ : Ordinal
h₁ : o₁ < type r
h₂ : o₂ < type r
h : enum r o₁ h₁ = enum r o₂ h₂
hne : ¬o₁ = o₂
this : IsIrrefl α r
⊢ False
α : Type u_1
β : Type ?u.198351
γ : Type ?u.198354
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
o₁ o₂ : Ordinal
h₁ : o₁ < type r
h₂ : o₂ < type r
h : enum r o₁ h₁ = enum r o₂ h₂
hne : ¬o₁ = o₂
⊢ False
haveI : IsIrrefl _ r := inferInstance
case inl.a
α : Type u_1
β : Type ?u.198351
γ : Type ?u.198354
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
o₁ o₂ : Ordinal
h₁ : o₁ < type r
h₂ : o₂ < type r
h : enum r o₁ h₁ = enum r o₂ h₂
hne : ¬o₁ = o₂
this : IsIrrefl α r
hlt : o₁ < o₂
⊢ r ?inl.a ?inl.a

case inl.a
α : Type u_1
β : Type ?u.198351
γ : Type ?u.198354
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
o₁ o₂ : Ordinal
h₁ : o₁ < type r
h₂ : o₂ < type r
h : enum r o₁ h₁ = enum r o₂ h₂
hne : ¬o₁ = o₂
this : IsIrrefl α r
hlt : o₁ < o₂
⊢ α

case inr.a
α : Type u_1
β : Type ?u.198351
γ : Type ?u.198354
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
o₁ o₂ : Ordinal
h₁ : o₁ < type r
h₂ : o₂ < type r
h : enum r o₁ h₁ = enum r o₂ h₂
hne : ¬o₁ = o₂
this : IsIrrefl α r
hlt : o₁ > o₂
⊢ r ?inr.a ?inr.a

case inr.a
α : Type u_1
β : Type ?u.198351
γ : Type ?u.198354
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
o₁ o₂ : Ordinal
h₁ : o₁ < type r
h₂ : o₂ < type r
h : enum r o₁ h₁ = enum r o₂ h₂
hne : ¬o₁ = o₂
this : IsIrrefl α r
hlt : o₁ > o₂
⊢ α
α : Type u_1
β : Type ?u.198351
γ : Type ?u.198354
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
o₁ o₂ : Ordinal
h₁ : o₁ < type r
h₂ : o₂ < type r
h : enum r o₁ h₁ = enum r o₂ h₂
hne : ¬o₁ = o₂
this : IsIrrefl α r
⊢ False
cases' lt_or_gt_of_ne hne with hlt hlt <;> apply (this).1
no goals
case inl.a
α : Type u_1
β : Type ?u.198351
γ : Type ?u.198354
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
o₁ o₂ : Ordinal
h₁ : o₁ < type r
h₂ : o₂ < type r
h : enum r o₁ h₁ = enum r o₂ h₂
hne : ¬o₁ = o₂
this : IsIrrefl α r
hlt : o₁ < o₂
⊢ r ?inl.a ?inl.a
rwa [← @enum_lt_enum α r _ o₁ o₂ h₁ h₂, h] at hlt
case inr.a
α : Type u_1
β : Type ?u.198351
γ : Type ?u.198354
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
o₁ o₂ : Ordinal
h₁ : o₁ < type r
h₂ : o₂ < type r
h : enum r o₁ h₁ = enum r o₂ h₂
hne : ¬o₁ = o₂
this : IsIrrefl α r
hlt✝ : o₁ > o₂
hlt : o₂ < o₁
⊢ r ?inr.a ?inr.a
case inr.a
α : Type u_1
β : Type ?u.198351
γ : Type ?u.198354
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
o₁ o₂ : Ordinal
h₁ : o₁ < type r
h₂ : o₂ < type r
h : enum r o₁ h₁ = enum r o₂ h₂
hne : ¬o₁ = o₂
this : IsIrrefl α r
hlt : o₁ > o₂
⊢ r ?inr.a ?inr.a
rw [GT.gt] at hlt
no goals
case inr.a
α : Type u_1
β : Type ?u.198351
γ : Type ?u.198354
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
o₁ o₂ : Ordinal
h₁ : o₁ < type r
h₂ : o₂ < type r
h : enum r o₁ h₁ = enum r o₂ h₂
hne : ¬o₁ = o₂
this : IsIrrefl α r
hlt✝ : o₁ > o₂
hlt : o₂ < o₁
⊢ r ?inr.a ?inr.a
rwa [← @enum_lt_enum α r _ o₂ o₁ h₂ h₁, h] at hlt
no goals
α : Type u_1
β : Type ?u.198351
γ : Type ?u.198354
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
o₁ o₂ : Ordinal
h₁ : o₁ < type r
h₂ : o₂ < type r
h : o₁ = o₂
⊢ enum r o₁ h₁ = enum r o₂ h₂
simp_rw [h]