ι : Type ?u.48841
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
f : α → β
s t : Set α
a : α
hs : PartiallyWellOrderedOn s r
hf : ∀ (a₁ : α), a₁ ∈ s → ∀ (a₂ : α), a₂ ∈ s → r a₁ a₂ → r' (f a₁) (f a₂)
g' : ℕ → β
hg' : ∀ (n : ℕ), g' n ∈ f '' s
⊢ ∃ m n, m < n ∧ r' (g' m) (g' n)
ι : Type ?u.48841
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
f : α → β
s t : Set α
a : α
hs : PartiallyWellOrderedOn s r
hf : ∀ (a₁ : α), a₁ ∈ s → ∀ (a₂ : α), a₂ ∈ s → r a₁ a₂ → r' (f a₁) (f a₂)
⊢ PartiallyWellOrderedOn (f '' s) r'
intro g' hg'
ι : Type ?u.48841
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
f : α → β
s t : Set α
a : α
hs : PartiallyWellOrderedOn s r
hf : ∀ (a₁ : α), a₁ ∈ s → ∀ (a₂ : α), a₂ ∈ s → r a₁ a₂ → r' (f a₁) (f a₂)
g' : ℕ → β
g : ℕ → α
hgs : ∀ (n : ℕ), g n ∈ s
heq : ∀ (n : ℕ), f (g n) = g' n
⊢ ∃ m n, m < n ∧ r' (g' m) (g' n)
ι : Type ?u.48841
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
f : α → β
s t : Set α
a : α
hs : PartiallyWellOrderedOn s r
hf : ∀ (a₁ : α), a₁ ∈ s → ∀ (a₂ : α), a₂ ∈ s → r a₁ a₂ → r' (f a₁) (f a₂)
g' : ℕ → β
hg' : ∀ (n : ℕ), g' n ∈ f '' s
⊢ ∃ m n, m < n ∧ r' (g' m) (g' n)
choose g hgs heq using hg'
ι : Type ?u.48841
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
f : α → β
s t : Set α
a : α
hs : PartiallyWellOrderedOn s r
hf : ∀ (a₁ : α), a₁ ∈ s → ∀ (a₂ : α), a₂ ∈ s → r a₁ a₂ → r' (f a₁) (f a₂)
g' : ℕ → β
g : ℕ → α
hgs : ∀ (n : ℕ), g n ∈ s
heq : ∀ (n : ℕ), f (g n) = g' n
⊢ f ∘ g = g'

ι : Type ?u.48841
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
f : α → β
s t : Set α
a : α
hs : PartiallyWellOrderedOn s r
hf : ∀ (a₁ : α), a₁ ∈ s → ∀ (a₂ : α), a₂ ∈ s → r a₁ a₂ → r' (f a₁) (f a₂)
g : ℕ → α
hgs : ∀ (n : ℕ), g n ∈ s
heq : ∀ (n : ℕ), f (g n) = (f ∘ g) n
⊢ ∃ m n, m < n ∧ r' ((f ∘ g) m) ((f ∘ g) n)
ι : Type ?u.48841
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
f : α → β
s t : Set α
a : α
hs : PartiallyWellOrderedOn s r
hf : ∀ (a₁ : α), a₁ ∈ s → ∀ (a₂ : α), a₂ ∈ s → r a₁ a₂ → r' (f a₁) (f a₂)
g' : ℕ → β
g : ℕ → α
hgs : ∀ (n : ℕ), g n ∈ s
heq : ∀ (n : ℕ), f (g n) = g' n
⊢ ∃ m n, m < n ∧ r' (g' m) (g' n)
obtain rfl : f ∘ g = g'
ι : Type ?u.48841
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
f : α → β
s t : Set α
a : α
hs : PartiallyWellOrderedOn s r
hf : ∀ (a₁ : α), a₁ ∈ s → ∀ (a₂ : α), a₂ ∈ s → r a₁ a₂ → r' (f a₁) (f a₂)
g : ℕ → α
hgs : ∀ (n : ℕ), g n ∈ s
heq : ∀ (n : ℕ), f (g n) = (f ∘ g) n
⊢ ∃ m n, m < n ∧ r' ((f ∘ g) m) ((f ∘ g) n)
ι : Type ?u.48841
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
f : α → β
s t : Set α
a : α
hs : PartiallyWellOrderedOn s r
hf : ∀ (a₁ : α), a₁ ∈ s → ∀ (a₂ : α), a₂ ∈ s → r a₁ a₂ → r' (f a₁) (f a₂)
g' : ℕ → β
g : ℕ → α
hgs : ∀ (n : ℕ), g n ∈ s
heq : ∀ (n : ℕ), f (g n) = g' n
⊢ f ∘ g = g'

ι : Type ?u.48841
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
f : α → β
s t : Set α
a : α
hs : PartiallyWellOrderedOn s r
hf : ∀ (a₁ : α), a₁ ∈ s → ∀ (a₂ : α), a₂ ∈ s → r a₁ a₂ → r' (f a₁) (f a₂)
g : ℕ → α
hgs : ∀ (n : ℕ), g n ∈ s
heq : ∀ (n : ℕ), f (g n) = (f ∘ g) n
⊢ ∃ m n, m < n ∧ r' ((f ∘ g) m) ((f ∘ g) n)
exact funext heq
case intro.intro.intro
ι : Type ?u.48841
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
f : α → β
s t : Set α
a : α
hs : PartiallyWellOrderedOn s r
hf : ∀ (a₁ : α), a₁ ∈ s → ∀ (a₂ : α), a₂ ∈ s → r a₁ a₂ → r' (f a₁) (f a₂)
g : ℕ → α
hgs : ∀ (n : ℕ), g n ∈ s
heq : ∀ (n : ℕ), f (g n) = (f ∘ g) n
m n : ℕ
hlt : m < n
hmn : r (g m) (g n)
⊢ ∃ m n, m < n ∧ r' ((f ∘ g) m) ((f ∘ g) n)
ι : Type ?u.48841
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
f : α → β
s t : Set α
a : α
hs : PartiallyWellOrderedOn s r
hf : ∀ (a₁ : α), a₁ ∈ s → ∀ (a₂ : α), a₂ ∈ s → r a₁ a₂ → r' (f a₁) (f a₂)
g : ℕ → α
hgs : ∀ (n : ℕ), g n ∈ s
heq : ∀ (n : ℕ), f (g n) = (f ∘ g) n
⊢ ∃ m n, m < n ∧ r' ((f ∘ g) m) ((f ∘ g) n)
obtain ⟨m, n, hlt, hmn⟩ := hs g hgs
no goals
case intro.intro.intro
ι : Type ?u.48841
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
f : α → β
s t : Set α
a : α
hs : PartiallyWellOrderedOn s r
hf : ∀ (a₁ : α), a₁ ∈ s → ∀ (a₂ : α), a₂ ∈ s → r a₁ a₂ → r' (f a₁) (f a₂)
g : ℕ → α
hgs : ∀ (n : ℕ), g n ∈ s
heq : ∀ (n : ℕ), f (g n) = (f ∘ g) n
m n : ℕ
hlt : m < n
hmn : r (g m) (g n)
⊢ ∃ m n, m < n ∧ r' ((f ∘ g) m) ((f ∘ g) n)
exact ⟨m, n, hlt, hf _ (hgs m) _ (hgs n) hmn⟩