case intro.intro
α✝ : Type ?u.168313
β : Type ?u.168316
γ : Type ?u.168319
α : Type u_1
P : α → Prop
r : α → α → Prop
inst✝ : IsSymm α r
h : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → ∃ y, P y ∧ ∀ (x : α), x ∈ s → r x y
f : ℕ → α
hf : ∀ (n : ℕ), P (f n)
hf' : ∀ (m n : ℕ), m < n → r (f m) (f n)
⊢ ∃ f, (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m ≠ n → r (f m) (f n)
α✝ : Type ?u.168313
β : Type ?u.168316
γ : Type ?u.168319
α : Type u_1
P : α → Prop
r : α → α → Prop
inst✝ : IsSymm α r
h : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → ∃ y, P y ∧ ∀ (x : α), x ∈ s → r x y
⊢ ∃ f, (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m ≠ n → r (f m) (f n)
rcases exists_seq_of_forall_finset_exists P r h with ⟨f, hf, hf'⟩
case intro.intro
α✝ : Type ?u.168313
β : Type ?u.168316
γ : Type ?u.168319
α : Type u_1
P : α → Prop
r : α → α → Prop
inst✝ : IsSymm α r
h : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → ∃ y, P y ∧ ∀ (x : α), x ∈ s → r x y
f : ℕ → α
hf : ∀ (n : ℕ), P (f n)
hf' : ∀ (m n : ℕ), m < n → r (f m) (f n)
m n : ℕ
hmn : m ≠ n
⊢ r (f m) (f n)
case intro.intro
α✝ : Type ?u.168313
β : Type ?u.168316
γ : Type ?u.168319
α : Type u_1
P : α → Prop
r : α → α → Prop
inst✝ : IsSymm α r
h : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → ∃ y, P y ∧ ∀ (x : α), x ∈ s → r x y
f : ℕ → α
hf : ∀ (n : ℕ), P (f n)
hf' : ∀ (m n : ℕ), m < n → r (f m) (f n)
⊢ ∃ f, (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m ≠ n → r (f m) (f n)
refine' ⟨f, hf, fun m n hmn => _⟩
case intro.intro.inl
α✝ : Type ?u.168313
β : Type ?u.168316
γ : Type ?u.168319
α : Type u_1
P : α → Prop
r : α → α → Prop
inst✝ : IsSymm α r
h✝ : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → ∃ y, P y ∧ ∀ (x : α), x ∈ s → r x y
f : ℕ → α
hf : ∀ (n : ℕ), P (f n)
hf' : ∀ (m n : ℕ), m < n → r (f m) (f n)
m n : ℕ
hmn : m ≠ n
h : m < n
⊢ r (f m) (f n)

case intro.intro.inr.inl
α✝ : Type ?u.168313
β : Type ?u.168316
γ : Type ?u.168319
α : Type u_1
P : α → Prop
r : α → α → Prop
inst✝ : IsSymm α r
h : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → ∃ y, P y ∧ ∀ (x : α), x ∈ s → r x y
f : ℕ → α
hf : ∀ (n : ℕ), P (f n)
hf' : ∀ (m n : ℕ), m < n → r (f m) (f n)
m : ℕ
hmn : m ≠ m
⊢ r (f m) (f m)

case intro.intro.inr.inr
α✝ : Type ?u.168313
β : Type ?u.168316
γ : Type ?u.168319
α : Type u_1
P : α → Prop
r : α → α → Prop
inst✝ : IsSymm α r
h✝ : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → ∃ y, P y ∧ ∀ (x : α), x ∈ s → r x y
f : ℕ → α
hf : ∀ (n : ℕ), P (f n)
hf' : ∀ (m n : ℕ), m < n → r (f m) (f n)
m n : ℕ
hmn : m ≠ n
h : n < m
⊢ r (f m) (f n)
case intro.intro
α✝ : Type ?u.168313
β : Type ?u.168316
γ : Type ?u.168319
α : Type u_1
P : α → Prop
r : α → α → Prop
inst✝ : IsSymm α r
h : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → ∃ y, P y ∧ ∀ (x : α), x ∈ s → r x y
f : ℕ → α
hf : ∀ (n : ℕ), P (f n)
hf' : ∀ (m n : ℕ), m < n → r (f m) (f n)
m n : ℕ
hmn : m ≠ n
⊢ r (f m) (f n)
rcases lt_trichotomy m n with (h | rfl | h)
no goals
case intro.intro.inl
α✝ : Type ?u.168313
β : Type ?u.168316
γ : Type ?u.168319
α : Type u_1
P : α → Prop
r : α → α → Prop
inst✝ : IsSymm α r
h✝ : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → ∃ y, P y ∧ ∀ (x : α), x ∈ s → r x y
f : ℕ → α
hf : ∀ (n : ℕ), P (f n)
hf' : ∀ (m n : ℕ), m < n → r (f m) (f n)
m n : ℕ
hmn : m ≠ n
h : m < n
⊢ r (f m) (f n)
exact hf' m n h
no goals
case intro.intro.inr.inl
α✝ : Type ?u.168313
β : Type ?u.168316
γ : Type ?u.168319
α : Type u_1
P : α → Prop
r : α → α → Prop
inst✝ : IsSymm α r
h : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → ∃ y, P y ∧ ∀ (x : α), x ∈ s → r x y
f : ℕ → α
hf : ∀ (n : ℕ), P (f n)
hf' : ∀ (m n : ℕ), m < n → r (f m) (f n)
m : ℕ
hmn : m ≠ m
⊢ r (f m) (f m)
exact (hmn rfl).elim
case intro.intro.inr.inr.a
α✝ : Type ?u.168313
β : Type ?u.168316
γ : Type ?u.168319
α : Type u_1
P : α → Prop
r : α → α → Prop
inst✝ : IsSymm α r
h✝ : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → ∃ y, P y ∧ ∀ (x : α), x ∈ s → r x y
f : ℕ → α
hf : ∀ (n : ℕ), P (f n)
hf' : ∀ (m n : ℕ), m < n → r (f m) (f n)
m n : ℕ
hmn : m ≠ n
h : n < m
⊢ r (f n) (f m)
case intro.intro.inr.inr
α✝ : Type ?u.168313
β : Type ?u.168316
γ : Type ?u.168319
α : Type u_1
P : α → Prop
r : α → α → Prop
inst✝ : IsSymm α r
h✝ : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → ∃ y, P y ∧ ∀ (x : α), x ∈ s → r x y
f : ℕ → α
hf : ∀ (n : ℕ), P (f n)
hf' : ∀ (m n : ℕ), m < n → r (f m) (f n)
m n : ℕ
hmn : m ≠ n
h : n < m
⊢ r (f m) (f n)
apply symm
no goals
case intro.intro.inr.inr.a
α✝ : Type ?u.168313
β : Type ?u.168316
γ : Type ?u.168319
α : Type u_1
P : α → Prop
r : α → α → Prop
inst✝ : IsSymm α r
h✝ : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → ∃ y, P y ∧ ∀ (x : α), x ∈ s → r x y
f : ℕ → α
hf : ∀ (n : ℕ), P (f n)
hf' : ∀ (m n : ℕ), m < n → r (f m) (f n)
m n : ℕ
hmn : m ≠ n
h : n < m
⊢ r (f n) (f m)
exact hf' n m h