ι : Type ?u.6720
α : Type u_1
β : Type ?u.6726
r r' : α → α → Prop
inst✝ : IsStrictOrder α r
s t : Set α
⊢ Nonempty ((fun x x_1 => x > x_1) ↪r fun a b => r a b ∧ a ∈ s ∧ b ∈ s) ↔ ∃ x, ∀ (n : ℕ), ↑x n ∈ s
ι : Type ?u.6720
α : Type u_1
β : Type ?u.6726
r r' : α → α → Prop
inst✝ : IsStrictOrder α r
s t : Set α
⊢ WellFoundedOn s r ↔ ∀ (f : (fun x x_1 => x > x_1) ↪r r), ¬∀ (n : ℕ), ↑f n ∈ s
simp only [wellFoundedOn_iff, RelEmbedding.wellFounded_iff_no_descending_seq, ← not_exists, ←
  not_nonempty_iff, not_iff_not]
case mp
ι : Type ?u.6720
α : Type u_1
β : Type ?u.6726
r r' : α → α → Prop
inst✝ : IsStrictOrder α r
s t : Set α
⊢ Nonempty ((fun x x_1 => x > x_1) ↪r fun a b => r a b ∧ a ∈ s ∧ b ∈ s) → ∃ x, ∀ (n : ℕ), ↑x n ∈ s

case mpr
ι : Type ?u.6720
α : Type u_1
β : Type ?u.6726
r r' : α → α → Prop
inst✝ : IsStrictOrder α r
s t : Set α
⊢ (∃ x, ∀ (n : ℕ), ↑x n ∈ s) → Nonempty ((fun x x_1 => x > x_1) ↪r fun a b => r a b ∧ a ∈ s ∧ b ∈ s)
ι : Type ?u.6720
α : Type u_1
β : Type ?u.6726
r r' : α → α → Prop
inst✝ : IsStrictOrder α r
s t : Set α
⊢ Nonempty ((fun x x_1 => x > x_1) ↪r fun a b => r a b ∧ a ∈ s ∧ b ∈ s) ↔ ∃ x, ∀ (n : ℕ), ↑x n ∈ s
constructor
case mp.intro.mk
ι : Type ?u.6720
α : Type u_1
β : Type ?u.6726
r r' : α → α → Prop
inst✝ : IsStrictOrder α r
s t : Set α
f : ℕ ↪ α
hf : ∀ {a b : ℕ}, r (↑f a) (↑f b) ∧ ↑f a ∈ s ∧ ↑f b ∈ s ↔ a > b
⊢ ∃ x, ∀ (n : ℕ), ↑x n ∈ s
case mp
ι : Type ?u.6720
α : Type u_1
β : Type ?u.6726
r r' : α → α → Prop
inst✝ : IsStrictOrder α r
s t : Set α
⊢ Nonempty ((fun x x_1 => x > x_1) ↪r fun a b => r a b ∧ a ∈ s ∧ b ∈ s) → ∃ x, ∀ (n : ℕ), ↑x n ∈ s
rintro ⟨⟨f, hf⟩⟩
case mp.intro.mk
ι : Type ?u.6720
α : Type u_1
β : Type ?u.6726
r r' : α → α → Prop
inst✝ : IsStrictOrder α r
s t : Set α
f : ℕ ↪ α
hf : ∀ {a b : ℕ}, r (↑f a) (↑f b) ∧ ↑f a ∈ s ∧ ↑f b ∈ s ↔ a > b
H : ∀ (n : ℕ), ↑f n ∈ s
⊢ ∃ x, ∀ (n : ℕ), ↑x n ∈ s
case mp.intro.mk
ι : Type ?u.6720
α : Type u_1
β : Type ?u.6726
r r' : α → α → Prop
inst✝ : IsStrictOrder α r
s t : Set α
f : ℕ ↪ α
hf : ∀ {a b : ℕ}, r (↑f a) (↑f b) ∧ ↑f a ∈ s ∧ ↑f b ∈ s ↔ a > b
⊢ ∃ x, ∀ (n : ℕ), ↑x n ∈ s
have H : ∀ n, f n ∈ s := fun n => (hf.2 n.lt_succ_self).2.2
case mp.intro.mk
ι : Type ?u.6720
α : Type u_1
β : Type ?u.6726
r r' : α → α → Prop
inst✝ : IsStrictOrder α r
s t : Set α
f : ℕ ↪ α
hf : ∀ {a b : ℕ}, r (↑f a) (↑f b) ∧ ↑f a ∈ s ∧ ↑f b ∈ s ↔ a > b
H : ∀ (n : ℕ), ↑f n ∈ s
⊢ ∀ {a b : ℕ}, r (↑f a) (↑f b) ↔ a > b
case mp.intro.mk
ι : Type ?u.6720
α : Type u_1
β : Type ?u.6726
r r' : α → α → Prop
inst✝ : IsStrictOrder α r
s t : Set α
f : ℕ ↪ α
hf : ∀ {a b : ℕ}, r (↑f a) (↑f b) ∧ ↑f a ∈ s ∧ ↑f b ∈ s ↔ a > b
H : ∀ (n : ℕ), ↑f n ∈ s
⊢ ∃ x, ∀ (n : ℕ), ↑x n ∈ s
refine' ⟨⟨f, _⟩, H⟩
no goals
case mp.intro.mk
ι : Type ?u.6720
α : Type u_1
β : Type ?u.6726
r r' : α → α → Prop
inst✝ : IsStrictOrder α r
s t : Set α
f : ℕ ↪ α
hf : ∀ {a b : ℕ}, r (↑f a) (↑f b) ∧ ↑f a ∈ s ∧ ↑f b ∈ s ↔ a > b
H : ∀ (n : ℕ), ↑f n ∈ s
⊢ ∀ {a b : ℕ}, r (↑f a) (↑f b) ↔ a > b
simpa only [H, and_true_iff] using @hf
case mpr.intro.mk
ι : Type ?u.6720
α : Type u_1
β : Type ?u.6726
r r' : α → α → Prop
inst✝ : IsStrictOrder α r
s t : Set α
f : ℕ ↪ α
hf : ∀ {a b : ℕ}, r (↑f a) (↑f b) ↔ a > b
hfs : ∀ (n : ℕ), ↑f n ∈ s
⊢ Nonempty ((fun x x_1 => x > x_1) ↪r fun a b => r a b ∧ a ∈ s ∧ b ∈ s)
case mpr
ι : Type ?u.6720
α : Type u_1
β : Type ?u.6726
r r' : α → α → Prop
inst✝ : IsStrictOrder α r
s t : Set α
⊢ (∃ x, ∀ (n : ℕ), ↑x n ∈ s) → Nonempty ((fun x x_1 => x > x_1) ↪r fun a b => r a b ∧ a ∈ s ∧ b ∈ s)
rintro ⟨⟨f, hf⟩, hfs : ∀ n, f n ∈ s⟩
case mpr.intro.mk
ι : Type ?u.6720
α : Type u_1
β : Type ?u.6726
r r' : α → α → Prop
inst✝ : IsStrictOrder α r
s t : Set α
f : ℕ ↪ α
hf : ∀ {a b : ℕ}, r (↑f a) (↑f b) ↔ a > b
hfs : ∀ (n : ℕ), ↑f n ∈ s
⊢ ∀ {a b : ℕ}, r (↑f a) (↑f b) ∧ ↑f a ∈ s ∧ ↑f b ∈ s ↔ a > b
case mpr.intro.mk
ι : Type ?u.6720
α : Type u_1
β : Type ?u.6726
r r' : α → α → Prop
inst✝ : IsStrictOrder α r
s t : Set α
f : ℕ ↪ α
hf : ∀ {a b : ℕ}, r (↑f a) (↑f b) ↔ a > b
hfs : ∀ (n : ℕ), ↑f n ∈ s
⊢ Nonempty ((fun x x_1 => x > x_1) ↪r fun a b => r a b ∧ a ∈ s ∧ b ∈ s)
refine' ⟨⟨f, _⟩⟩
no goals
case mpr.intro.mk
ι : Type ?u.6720
α : Type u_1
β : Type ?u.6726
r r' : α → α → Prop
inst✝ : IsStrictOrder α r
s t : Set α
f : ℕ ↪ α
hf : ∀ {a b : ℕ}, r (↑f a) (↑f b) ↔ a > b
hfs : ∀ (n : ℕ), ↑f n ∈ s
⊢ ∀ {a b : ℕ}, r (↑f a) (↑f b) ∧ ↑f a ∈ s ∧ ↑f b ∈ s ↔ a > b
simpa only [hfs, and_true_iff] using @hf