ι : Type ?u.29184
α : Type u_1
β : Type ?u.29190
r r' : α → α → Prop
inst✝ : IsStrictOrder α r
s t : Set α
hs : ∀ (f : (fun x x_1 => x > x_1) ↪r r), ¬∀ (n : ℕ), ↑f n ∈ s
ht : ∀ (f : (fun x x_1 => x > x_1) ↪r r), ¬∀ (n : ℕ), ↑f n ∈ t
⊢ ∀ (f : (fun x x_1 => x > x_1) ↪r r), ¬∀ (n : ℕ), ↑f n ∈ s ∪ t
ι : Type ?u.29184
α : Type u_1
β : Type ?u.29190
r r' : α → α → Prop
inst✝ : IsStrictOrder α r
s t : Set α
hs : WellFoundedOn s r
ht : WellFoundedOn t r
⊢ WellFoundedOn (s ∪ t) r
rw [wellFoundedOn_iff_no_descending_seq] at *
ι : Type ?u.29184
α : Type u_1
β : Type ?u.29190
r r' : α → α → Prop
inst✝ : IsStrictOrder α r
s t : Set α
hs : ∀ (f : (fun x x_1 => x > x_1) ↪r r), ¬∀ (n : ℕ), ↑f n ∈ s
ht : ∀ (f : (fun x x_1 => x > x_1) ↪r r), ¬∀ (n : ℕ), ↑f n ∈ t
f : (fun x x_1 => x > x_1) ↪r r
hf : ∀ (n : ℕ), ↑f n ∈ s ∪ t
⊢ False
ι : Type ?u.29184
α : Type u_1
β : Type ?u.29190
r r' : α → α → Prop
inst✝ : IsStrictOrder α r
s t : Set α
hs : ∀ (f : (fun x x_1 => x > x_1) ↪r r), ¬∀ (n : ℕ), ↑f n ∈ s
ht : ∀ (f : (fun x x_1 => x > x_1) ↪r r), ¬∀ (n : ℕ), ↑f n ∈ t
⊢ ∀ (f : (fun x x_1 => x > x_1) ↪r r), ¬∀ (n : ℕ), ↑f n ∈ s ∪ t
rintro f hf
case intro.inl
ι : Type ?u.29184
α : Type u_1
β : Type ?u.29190
r r' : α → α → Prop
inst✝ : IsStrictOrder α r
s t : Set α
hs : ∀ (f : (fun x x_1 => x > x_1) ↪r r), ¬∀ (n : ℕ), ↑f n ∈ s
ht : ∀ (f : (fun x x_1 => x > x_1) ↪r r), ¬∀ (n : ℕ), ↑f n ∈ t
f : (fun x x_1 => x > x_1) ↪r r
hf : ∀ (n : ℕ), ↑f n ∈ s ∪ t
g : ℕ ↪o ℕ
hg : ∀ (n : ℕ), ↑f (↑g n) ∈ s
⊢ False

case intro.inr
ι : Type ?u.29184
α : Type u_1
β : Type ?u.29190
r r' : α → α → Prop
inst✝ : IsStrictOrder α r
s t : Set α
hs : ∀ (f : (fun x x_1 => x > x_1) ↪r r), ¬∀ (n : ℕ), ↑f n ∈ s
ht : ∀ (f : (fun x x_1 => x > x_1) ↪r r), ¬∀ (n : ℕ), ↑f n ∈ t
f : (fun x x_1 => x > x_1) ↪r r
hf : ∀ (n : ℕ), ↑f n ∈ s ∪ t
g : ℕ ↪o ℕ
hg : ∀ (n : ℕ), ↑f (↑g n) ∈ t
⊢ False
ι : Type ?u.29184
α : Type u_1
β : Type ?u.29190
r r' : α → α → Prop
inst✝ : IsStrictOrder α r
s t : Set α
hs : ∀ (f : (fun x x_1 => x > x_1) ↪r r), ¬∀ (n : ℕ), ↑f n ∈ s
ht : ∀ (f : (fun x x_1 => x > x_1) ↪r r), ¬∀ (n : ℕ), ↑f n ∈ t
f : (fun x x_1 => x > x_1) ↪r r
hf : ∀ (n : ℕ), ↑f n ∈ s ∪ t
⊢ False
rcases Nat.exists_subseq_of_forall_mem_union f hf with ⟨g, hg | hg⟩
no goals
case intro.inl
ι : Type ?u.29184
α : Type u_1
β : Type ?u.29190
r r' : α → α → Prop
inst✝ : IsStrictOrder α r
s t : Set α
hs : ∀ (f : (fun x x_1 => x > x_1) ↪r r), ¬∀ (n : ℕ), ↑f n ∈ s
ht : ∀ (f : (fun x x_1 => x > x_1) ↪r r), ¬∀ (n : ℕ), ↑f n ∈ t
f : (fun x x_1 => x > x_1) ↪r r
hf : ∀ (n : ℕ), ↑f n ∈ s ∪ t
g : ℕ ↪o ℕ
hg : ∀ (n : ℕ), ↑f (↑g n) ∈ s
⊢ False

case intro.inr
ι : Type ?u.29184
α : Type u_1
β : Type ?u.29190
r r' : α → α → Prop
inst✝ : IsStrictOrder α r
s t : Set α
hs : ∀ (f : (fun x x_1 => x > x_1) ↪r r), ¬∀ (n : ℕ), ↑f n ∈ s
ht : ∀ (f : (fun x x_1 => x > x_1) ↪r r), ¬∀ (n : ℕ), ↑f n ∈ t
f : (fun x x_1 => x > x_1) ↪r r
hf : ∀ (n : ℕ), ↑f n ∈ s ∪ t
g : ℕ ↪o ℕ
hg : ∀ (n : ℕ), ↑f (↑g n) ∈ t
⊢ False
exacts [hs (g.dual.ltEmbedding.trans f) hg, ht (g.dual.ltEmbedding.trans f) hg]