α : Type u_1
β : Type ?u.37084
γ : Type ?u.37087
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
f : r ≺i r
h : r (↑f.toRelEmbedding f.top) f.top
⊢ False
α : Type u_1
β : Type ?u.37084
γ : Type ?u.37087
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
f : r ≺i r
⊢ False
have h := f.lt_top f.top
α : Type u_1
β : Type ?u.37084
γ : Type ?u.37087
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
f : r ≺i r
h : r f.top f.top
⊢ False
α : Type u_1
β : Type ?u.37084
γ : Type ?u.37087
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
f : r ≺i r
h : r (↑f.toRelEmbedding f.top) f.top
⊢ False
rw [show f f.top = f.top from InitialSeg.eq (↑f) (InitialSeg.refl r) f.top] at h
no goals
α : Type u_1
β : Type ?u.37084
γ : Type ?u.37087
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
f : r ≺i r
h : r f.top f.top
⊢ False
exact _root_.irrefl _ h