α : Type u_2
β : Type u_1
γ : Type ?u.20498
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder β s
f : r ≼i s
h : ¬∃ b, ∀ (x : β), s x b ↔ ∃ y, ↑f y = x
b x : β
x✝¹ : ∀ (y : β), s y x → Acc s y
IH : ∀ (y : β), s y x → ∃ a, ↑f a = y
hn : ∀ (x_1 : α), ¬↑f x_1 = x
y : β
x✝ : ∃ y_1, ↑f y_1 = y
a : α
e : ↑f a = y
⊢ s (↑f a) x
α : Type u_2
β : Type u_1
γ : Type ?u.20498
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder β s
f : r ≼i s
h : ¬∃ b, ∀ (x : β), s x b ↔ ∃ y, ↑f y = x
b x : β
x✝¹ : ∀ (y : β), s y x → Acc s y
IH : ∀ (y : β), s y x → ∃ a, ↑f a = y
hn : ∀ (x_1 : α), ¬↑f x_1 = x
y : β
x✝ : ∃ y_1, ↑f y_1 = y
a : α
e : ↑f a = y
⊢ s y x
rw [← e]
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.20498
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder β s
f : r ≼i s
h : ¬∃ b, ∀ (x : β), s x b ↔ ∃ y, ↑f y = x
b x : β
x✝¹ : ∀ (y : β), s y x → Acc s y
IH : ∀ (y : β), s y x → ∃ a, ↑f a = y
hn : ∀ (x_1 : α), ¬↑f x_1 = x
y : β
x✝ : ∃ y_1, ↑f y_1 = y
a : α
e : ↑f a = y
⊢ s (↑f a) x
exact
  (trichotomous _ _).resolve_right
    (not_or_of_not (hn a) fun hl => not_exists.2 hn (f.init hl))