-- Mathlib/Data/Fintype/Basic.lean
theorem exists_seq_of_forall_finset_exists' {α : Type*} (P : α → Prop) (r : α → α → Prop)
    [IsSymm α r] (h : ∀ s : Finset α, (∀ x ∈ s, P x) → ∃ y, P y ∧ ∀ x ∈ s, r x y) :
    ∃ f : ℕ → α, (∀ n, P (f n)) ∧ Pairwise (r on f)

Proof state:
case intro.intro.inr.inr
α : Type u_4
P : α → Prop
r : α → α → Prop
inst✝ : IsSymm α r
h✝ : ∀ (s : Finset α), (∀ x ∈ s, P x) → ∃ y, P y ∧ ∀ 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 on f) m n

Tactic:
unfold Function.onFun

Result:
case intro.intro.inr.inr
α : Type u_4
P : α → Prop
r : α → α → Prop
inst✝ : IsSymm α r
h✝ : ∀ (s : Finset α), (∀ x ∈ s, P x) → ∃ y, P y ∧ ∀ 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)

Proof state:
case intro.intro
α : Type u_4
P : α → Prop
r : α → α → Prop
inst✝ : IsSymm α r
h : ∀ (s : Finset α), (∀ x ∈ s, P x) → ∃ y, P y ∧ ∀ 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)) ∧ Pairwise (r on f)

Tactic:
refine ⟨f, hf, fun m n hmn => ?_⟩

Result:
case intro.intro
α : Type u_4
P : α → Prop
r : α → α → Prop
inst✝ : IsSymm α r
h : ∀ (s : Finset α), (∀ x ∈ s, P x) → ∃ y, P y ∧ ∀ 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 on f) m n

Proof state:
case intro.intro.inr.inr
α : Type u_4
P : α → Prop
r : α → α → Prop
inst✝ : IsSymm α r
h✝ : ∀ (s : Finset α), (∀ x ∈ s, P x) → ∃ y, P y ∧ ∀ 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)

Tactic:
apply symm

Result:
case intro.intro.inr.inr.a
α : Type u_4
P : α → Prop
r : α → α → Prop
inst✝ : IsSymm α r
h✝ : ∀ (s : Finset α), (∀ x ∈ s, P x) → ∃ y, P y ∧ ∀ 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)

Proof state:
case intro.intro.inr.inr.a
α : Type u_4
P : α → Prop
r : α → α → Prop
inst✝ : IsSymm α r
h✝ : ∀ (s : Finset α), (∀ x ∈ s, P x) → ∃ y, P y ∧ ∀ 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)

Tactic:
exact hf' n m h

Result:
no goals

Proof state:
case intro.intro
α : Type u_4
P : α → Prop
r : α → α → Prop
inst✝ : IsSymm α r
h : ∀ (s : Finset α), (∀ x ∈ s, P x) → ∃ y, P y ∧ ∀ 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 on f) m n

Tactic:
rcases lt_trichotomy m n with (h | rfl | h)

Result:
case intro.intro.inl
α : Type u_4
P : α → Prop
r : α → α → Prop
inst✝ : IsSymm α r
h✝ : ∀ (s : Finset α), (∀ x ∈ s, P x) → ∃ y, P y ∧ ∀ 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 on f) m n

case intro.intro.inr.inl
α : Type u_4
P : α → Prop
r : α → α → Prop
inst✝ : IsSymm α r
h : ∀ (s : Finset α), (∀ x ∈ s, P x) → ∃ y, P y ∧ ∀ 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 on f) m m

case intro.intro.inr.inr
α : Type u_4
P : α → Prop
r : α → α → Prop
inst✝ : IsSymm α r
h✝ : ∀ (s : Finset α), (∀ x ∈ s, P x) → ∃ y, P y ∧ ∀ 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 on f) m n

Proof state:
case intro.intro.inl
α : Type u_4
P : α → Prop
r : α → α → Prop
inst✝ : IsSymm α r
h✝ : ∀ (s : Finset α), (∀ x ∈ s, P x) → ∃ y, P y ∧ ∀ 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 on f) m n

Tactic:
exact hf' m n h

Result:
no goals

Proof state:
α : Type u_4
P : α → Prop
r : α → α → Prop
inst✝ : IsSymm α r
h : ∀ (s : Finset α), (∀ x ∈ s, P x) → ∃ y, P y ∧ ∀ x ∈ s, r x y
⊢ ∃ f, (∀ (n : ℕ), P (f n)) ∧ Pairwise (r on f)

Tactic:
rcases exists_seq_of_forall_finset_exists P r h with ⟨f, hf, hf'⟩

Result:
case intro.intro
α : Type u_4
P : α → Prop
r : α → α → Prop
inst✝ : IsSymm α r
h : ∀ (s : Finset α), (∀ x ∈ s, P x) → ∃ y, P y ∧ ∀ 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)) ∧ Pairwise (r on f)

Proof state:
case intro.intro.inr.inl
α : Type u_4
P : α → Prop
r : α → α → Prop
inst✝ : IsSymm α r
h : ∀ (s : Finset α), (∀ x ∈ s, P x) → ∃ y, P y ∧ ∀ 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 on f) m m

Tactic:
exact (hmn rfl).elim

Result:
no goals