-- Mathlib/Order/WellFoundedSet.lean
theorem PartiallyWellOrderedOn.union (hs : s.PartiallyWellOrderedOn r)
    (ht : t.PartiallyWellOrderedOn r) : (s ∪ t).PartiallyWellOrderedOn r

Proof state:
case intro.inl
α : Type u_2
r : α → α → Prop
s t : Set α
hs : s.PartiallyWellOrderedOn r
ht : t.PartiallyWellOrderedOn r
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s ∪ t
g : ℕ ↪o ℕ
hgs : ∀ (n : ℕ), f (g n) ∈ s
⊢ ∃ m n, m < n ∧ r (f m) (f n)

Tactic:
rcases hs _ hgs with ⟨m, n, hlt, hr⟩

Result:
case intro.inl.intro.intro.intro
α : Type u_2
r : α → α → Prop
s t : Set α
hs : s.PartiallyWellOrderedOn r
ht : t.PartiallyWellOrderedOn r
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s ∪ t
g : ℕ ↪o ℕ
hgs : ∀ (n : ℕ), f (g n) ∈ s
m n : ℕ
hlt : m < n
hr : r (f (g m)) (f (g n))
⊢ ∃ m n, m < n ∧ r (f m) (f n)

Proof state:
case intro.inr.intro.intro.intro
α : Type u_2
r : α → α → Prop
s t : Set α
hs : s.PartiallyWellOrderedOn r
ht : t.PartiallyWellOrderedOn r
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s ∪ t
g : ℕ ↪o ℕ
hgt : ∀ (n : ℕ), f (g n) ∈ t
m n : ℕ
hlt : m < n
hr : r (f (g m)) (f (g n))
⊢ ∃ m n, m < n ∧ r (f m) (f n)

Tactic:
exact ⟨g m, g n, g.strictMono hlt, hr⟩

Result:
no goals

Proof state:
α : Type u_2
r : α → α → Prop
s t : Set α
hs : s.PartiallyWellOrderedOn r
ht : t.PartiallyWellOrderedOn r
⊢ (s ∪ t).PartiallyWellOrderedOn r

Tactic:
rintro f hf

Result:
α : Type u_2
r : α → α → Prop
s t : Set α
hs : s.PartiallyWellOrderedOn r
ht : t.PartiallyWellOrderedOn r
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s ∪ t
⊢ ∃ m n, m < n ∧ r (f m) (f n)

Proof state:
α : Type u_2
r : α → α → Prop
s t : Set α
hs : s.PartiallyWellOrderedOn r
ht : t.PartiallyWellOrderedOn r
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s ∪ t
⊢ ∃ m n, m < n ∧ r (f m) (f n)

Tactic:
rcases Nat.exists_subseq_of_forall_mem_union f hf with ⟨g, hgs | hgt⟩

Result:
case intro.inl
α : Type u_2
r : α → α → Prop
s t : Set α
hs : s.PartiallyWellOrderedOn r
ht : t.PartiallyWellOrderedOn r
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s ∪ t
g : ℕ ↪o ℕ
hgs : ∀ (n : ℕ), f (g n) ∈ s
⊢ ∃ m n, m < n ∧ r (f m) (f n)

case intro.inr
α : Type u_2
r : α → α → Prop
s t : Set α
hs : s.PartiallyWellOrderedOn r
ht : t.PartiallyWellOrderedOn r
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s ∪ t
g : ℕ ↪o ℕ
hgt : ∀ (n : ℕ), f (g n) ∈ t
⊢ ∃ m n, m < n ∧ r (f m) (f n)

Proof state:
case intro.inl.intro.intro.intro
α : Type u_2
r : α → α → Prop
s t : Set α
hs : s.PartiallyWellOrderedOn r
ht : t.PartiallyWellOrderedOn r
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s ∪ t
g : ℕ ↪o ℕ
hgs : ∀ (n : ℕ), f (g n) ∈ s
m n : ℕ
hlt : m < n
hr : r (f (g m)) (f (g n))
⊢ ∃ m n, m < n ∧ r (f m) (f n)

Tactic:
exact ⟨g m, g n, g.strictMono hlt, hr⟩

Result:
no goals

Proof state:
case intro.inr
α : Type u_2
r : α → α → Prop
s t : Set α
hs : s.PartiallyWellOrderedOn r
ht : t.PartiallyWellOrderedOn r
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s ∪ t
g : ℕ ↪o ℕ
hgt : ∀ (n : ℕ), f (g n) ∈ t
⊢ ∃ m n, m < n ∧ r (f m) (f n)

Tactic:
rcases ht _ hgt with ⟨m, n, hlt, hr⟩

Result:
case intro.inr.intro.intro.intro
α : Type u_2
r : α → α → Prop
s t : Set α
hs : s.PartiallyWellOrderedOn r
ht : t.PartiallyWellOrderedOn r
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s ∪ t
g : ℕ ↪o ℕ
hgt : ∀ (n : ℕ), f (g n) ∈ t
m n : ℕ
hlt : m < n
hr : r (f (g m)) (f (g n))
⊢ ∃ m n, m < n ∧ r (f m) (f n)