ι : Type ?u.95097
α : Type u_1
β : Type ?u.95103
r : α → α → Prop
r' : β → β → Prop
f : α → β
s t : Set α
a : α
inst✝ : IsPreorder α r
h : PartiallyWellOrderedOn s r
this : Preorder α := Preorder.mk (_ : ∀ (a : α), r a a) (_ : ∀ (x x_1 x_2 : α), r x x_1 → r x_1 x_2 → r x x_2)
⊢ WellFoundedOn s fun a b => r a b ∧ ¬r b a
ι : Type ?u.95097
α : Type u_1
β : Type ?u.95103
r : α → α → Prop
r' : β → β → Prop
f : α → β
s t : Set α
a : α
inst✝ : IsPreorder α r
h : PartiallyWellOrderedOn s r
⊢ WellFoundedOn s fun a b => r a b ∧ ¬r b a
letI : Preorder α :=
  { le := r
    le_refl := refl_of r
    le_trans := fun _ _ _ => trans_of r }
ι : Type ?u.95097
α : Type u_1
β : Type ?u.95103
r : α → α → Prop
r' : β → β → Prop
f : α → β
s t : Set α
a : α
inst✝ : IsPreorder α r
this : Preorder α := Preorder.mk (_ : ∀ (a : α), r a a) (_ : ∀ (x x_1 x_2 : α), r x x_1 → r x_1 x_2 → r x x_2)
h : PartiallyWellOrderedOn s fun x x_1 => x ≤ x_1
⊢ ∀ (f : (fun x x_1 => x > x_1) ↪r fun x x_1 => x < x_1), ¬∀ (n : ℕ), ↑f n ∈ s
ι : Type ?u.95097
α : Type u_1
β : Type ?u.95103
r : α → α → Prop
r' : β → β → Prop
f : α → β
s t : Set α
a : α
inst✝ : IsPreorder α r
this : Preorder α := Preorder.mk (_ : ∀ (a : α), r a a) (_ : ∀ (x x_1 x_2 : α), r x x_1 → r x_1 x_2 → r x x_2)
h : PartiallyWellOrderedOn s fun x x_1 => x ≤ x_1
⊢ WellFoundedOn s fun x x_1 => x < x_1
rw [wellFoundedOn_iff_no_descending_seq]
ι : Type ?u.95097
α : Type u_1
β : Type ?u.95103
r : α → α → Prop
r' : β → β → Prop
f✝ : α → β
s t : Set α
a : α
inst✝ : IsPreorder α r
this : Preorder α := Preorder.mk (_ : ∀ (a : α), r a a) (_ : ∀ (x x_1 x_2 : α), r x x_1 → r x_1 x_2 → r x x_2)
h : PartiallyWellOrderedOn s fun x x_1 => x ≤ x_1
f : (fun x x_1 => x > x_1) ↪r fun x x_1 => x < x_1
hf : ∀ (n : ℕ), ↑f n ∈ s
⊢ False
ι : Type ?u.95097
α : Type u_1
β : Type ?u.95103
r : α → α → Prop
r' : β → β → Prop
f : α → β
s t : Set α
a : α
inst✝ : IsPreorder α r
this : Preorder α := Preorder.mk (_ : ∀ (a : α), r a a) (_ : ∀ (x x_1 x_2 : α), r x x_1 → r x_1 x_2 → r x x_2)
h : PartiallyWellOrderedOn s fun x x_1 => x ≤ x_1
⊢ ∀ (f : (fun x x_1 => x > x_1) ↪r fun x x_1 => x < x_1), ¬∀ (n : ℕ), ↑f n ∈ s
intro f hf
case intro.intro.intro
ι : Type ?u.95097
α : Type u_1
β : Type ?u.95103
r : α → α → Prop
r' : β → β → Prop
f✝ : α → β
s t : Set α
a : α
inst✝ : IsPreorder α r
this : Preorder α := Preorder.mk (_ : ∀ (a : α), r a a) (_ : ∀ (x x_1 x_2 : α), r x x_1 → r x_1 x_2 → r x x_2)
h : PartiallyWellOrderedOn s fun x x_1 => x ≤ x_1
f : (fun x x_1 => x > x_1) ↪r fun x x_1 => x < x_1
hf : ∀ (n : ℕ), ↑f n ∈ s
m n : ℕ
hlt : m < n
hle : ↑f m ≤ ↑f n
⊢ False
ι : Type ?u.95097
α : Type u_1
β : Type ?u.95103
r : α → α → Prop
r' : β → β → Prop
f✝ : α → β
s t : Set α
a : α
inst✝ : IsPreorder α r
this : Preorder α := Preorder.mk (_ : ∀ (a : α), r a a) (_ : ∀ (x x_1 x_2 : α), r x x_1 → r x_1 x_2 → r x x_2)
h : PartiallyWellOrderedOn s fun x x_1 => x ≤ x_1
f : (fun x x_1 => x > x_1) ↪r fun x x_1 => x < x_1
hf : ∀ (n : ℕ), ↑f n ∈ s
⊢ False
obtain ⟨m, n, hlt, hle⟩ := h f hf
no goals
case intro.intro.intro
ι : Type ?u.95097
α : Type u_1
β : Type ?u.95103
r : α → α → Prop
r' : β → β → Prop
f✝ : α → β
s t : Set α
a : α
inst✝ : IsPreorder α r
this : Preorder α := Preorder.mk (_ : ∀ (a : α), r a a) (_ : ∀ (x x_1 x_2 : α), r x x_1 → r x_1 x_2 → r x x_2)
h : PartiallyWellOrderedOn s fun x x_1 => x ≤ x_1
f : (fun x x_1 => x > x_1) ↪r fun x x_1 => x < x_1
hf : ∀ (n : ℕ), ↑f n ∈ s
m n : ℕ
hlt : m < n
hle : ↑f m ≤ ↑f n
⊢ False
exact (f.map_rel_iff.2 hlt).not_le hle