no goals
α : Type u_1
s✝ : Set ℕ
inst✝ : Infinite ↑s✝
s t : Set α
e : ℕ → α
he : ∀ (n : ℕ), e n ∈ s ∪ t
⊢ ∃ g, (∀ (n : ℕ), e (↑g n) ∈ s) ∨ ∀ (n : ℕ), e (↑g n) ∈ t
classical
  have : Infinite (e ⁻¹' s) ∨ Infinite (e ⁻¹' t) := by
    simp only [Set.infinite_coe_iff, ← Set.infinite_union, ← Set.preimage_union,
      Set.eq_univ_of_forall fun n => Set.mem_preimage.2 (he n), Set.infinite_univ]
  cases this
  exacts [⟨Nat.orderEmbeddingOfSet (e ⁻¹' s), Or.inl fun n => (Nat.Subtype.ofNat (e ⁻¹' s) _).2⟩,
    ⟨Nat.orderEmbeddingOfSet (e ⁻¹' t), Or.inr fun n => (Nat.Subtype.ofNat (e ⁻¹' t) _).2⟩]
α : Type u_1
s✝ : Set ℕ
inst✝ : Infinite ↑s✝
s t : Set α
e : ℕ → α
he : ∀ (n : ℕ), e n ∈ s ∪ t
this : Infinite ↑(e ⁻¹' s) ∨ Infinite ↑(e ⁻¹' t)
⊢ ∃ g, (∀ (n : ℕ), e (↑g n) ∈ s) ∨ ∀ (n : ℕ), e (↑g n) ∈ t
α : Type u_1
s✝ : Set ℕ
inst✝ : Infinite ↑s✝
s t : Set α
e : ℕ → α
he : ∀ (n : ℕ), e n ∈ s ∪ t
⊢ ∃ g, (∀ (n : ℕ), e (↑g n) ∈ s) ∨ ∀ (n : ℕ), e (↑g n) ∈ t
have : Infinite (e ⁻¹' s) ∨ Infinite (e ⁻¹' t) := by
  simp only [Set.infinite_coe_iff, ← Set.infinite_union, ← Set.preimage_union,
    Set.eq_univ_of_forall fun n => Set.mem_preimage.2 (he n), Set.infinite_univ]
case inl
α : Type u_1
s✝ : Set ℕ
inst✝ : Infinite ↑s✝
s t : Set α
e : ℕ → α
he : ∀ (n : ℕ), e n ∈ s ∪ t
h✝ : Infinite ↑(e ⁻¹' s)
⊢ ∃ g, (∀ (n : ℕ), e (↑g n) ∈ s) ∨ ∀ (n : ℕ), e (↑g n) ∈ t

case inr
α : Type u_1
s✝ : Set ℕ
inst✝ : Infinite ↑s✝
s t : Set α
e : ℕ → α
he : ∀ (n : ℕ), e n ∈ s ∪ t
h✝ : Infinite ↑(e ⁻¹' t)
⊢ ∃ g, (∀ (n : ℕ), e (↑g n) ∈ s) ∨ ∀ (n : ℕ), e (↑g n) ∈ t
α : Type u_1
s✝ : Set ℕ
inst✝ : Infinite ↑s✝
s t : Set α
e : ℕ → α
he : ∀ (n : ℕ), e n ∈ s ∪ t
this : Infinite ↑(e ⁻¹' s) ∨ Infinite ↑(e ⁻¹' t)
⊢ ∃ g, (∀ (n : ℕ), e (↑g n) ∈ s) ∨ ∀ (n : ℕ), e (↑g n) ∈ t
cases this
no goals
case inl
α : Type u_1
s✝ : Set ℕ
inst✝ : Infinite ↑s✝
s t : Set α
e : ℕ → α
he : ∀ (n : ℕ), e n ∈ s ∪ t
h✝ : Infinite ↑(e ⁻¹' s)
⊢ ∃ g, (∀ (n : ℕ), e (↑g n) ∈ s) ∨ ∀ (n : ℕ), e (↑g n) ∈ t

case inr
α : Type u_1
s✝ : Set ℕ
inst✝ : Infinite ↑s✝
s t : Set α
e : ℕ → α
he : ∀ (n : ℕ), e n ∈ s ∪ t
h✝ : Infinite ↑(e ⁻¹' t)
⊢ ∃ g, (∀ (n : ℕ), e (↑g n) ∈ s) ∨ ∀ (n : ℕ), e (↑g n) ∈ t
exacts [⟨Nat.orderEmbeddingOfSet (e ⁻¹' s), Or.inl fun n => (Nat.Subtype.ofNat (e ⁻¹' s) _).2⟩,
  ⟨Nat.orderEmbeddingOfSet (e ⁻¹' t), Or.inr fun n => (Nat.Subtype.ofNat (e ⁻¹' t) _).2⟩]
no goals
α : Type u_1
s✝ : Set ℕ
inst✝ : Infinite ↑s✝
s t : Set α
e : ℕ → α
he : ∀ (n : ℕ), e n ∈ s ∪ t
⊢ Infinite ↑(e ⁻¹' s) ∨ Infinite ↑(e ⁻¹' t)
simp only [Set.infinite_coe_iff, ← Set.infinite_union, ← Set.preimage_union,
  Set.eq_univ_of_forall fun n => Set.mem_preimage.2 (he n), Set.infinite_univ]