no goals
α✝ : Type ?u.153481
β : Type ?u.153484
γ : Type ?u.153487
α : Type u_1
P : α → Prop
r : α → α → Prop
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)
classical
  have : Nonempty α := by
    rcases h ∅ (by simp) with ⟨y, _⟩
    exact ⟨y⟩
  choose! F hF using h
  have h' : ∀ s : Finset α, ∃ y, (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y := fun s => ⟨F s, hF s⟩
  set f := seqOfForallFinsetExistsAux P r h' with hf
  have A : ∀ n : ℕ, P (f n) := by
    intro n
    induction' n using Nat.strong_induction_on with n IH
    have IH' : ∀ x : Fin n, P (f x) := fun n => IH n.1 n.2
    rw [hf, seqOfForallFinsetExistsAux]
    exact
      (Classical.choose_spec
          (h' (Finset.image (fun i : Fin n => f i) (Finset.univ : Finset (Fin n))))
          (by simp [IH'])).1
  refine' ⟨f, A, fun m n hmn => _⟩
  conv_rhs => rw [hf]
  rw [seqOfForallFinsetExistsAux]
  apply
    (Classical.choose_spec
        (h' (Finset.image (fun i : Fin n => f i) (Finset.univ : Finset (Fin n)))) (by simp [A])).2
  exact Finset.mem_image.2 ⟨⟨m, hmn⟩, Finset.mem_univ _, rfl⟩
α✝ : Type ?u.153481
β : Type ?u.153484
γ : Type ?u.153487
α : Type u_1
P : α → Prop
r : α → α → Prop
h : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → ∃ y, P y ∧ ∀ (x : α), x ∈ s → r x y
this : Nonempty α
⊢ ∃ f, (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)
α✝ : Type ?u.153481
β : Type ?u.153484
γ : Type ?u.153487
α : Type u_1
P : α → Prop
r : α → α → Prop
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)
have : Nonempty α := by
  rcases h ∅ (by simp) with ⟨y, _⟩
  exact ⟨y⟩
α✝ : Type ?u.153481
β : Type ?u.153484
γ : Type ?u.153487
α : Type u_1
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → P (F s) ∧ ∀ (x : α), x ∈ s → r x (F s)
⊢ ∃ f, (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)
α✝ : Type ?u.153481
β : Type ?u.153484
γ : Type ?u.153487
α : Type u_1
P : α → Prop
r : α → α → Prop
h : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → ∃ y, P y ∧ ∀ (x : α), x ∈ s → r x y
this : Nonempty α
⊢ ∃ f, (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)
choose! F hF using h
α✝ : Type ?u.153481
β : Type ?u.153484
γ : Type ?u.153487
α : Type u_1
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → P (F s) ∧ ∀ (x : α), x ∈ s → r x (F s)
h' : ∀ (s : Finset α), ∃ y, (∀ (x : α), x ∈ s → P x) → P y ∧ ∀ (x : α), x ∈ s → r x y
⊢ ∃ f, (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)
α✝ : Type ?u.153481
β : Type ?u.153484
γ : Type ?u.153487
α : Type u_1
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → P (F s) ∧ ∀ (x : α), x ∈ s → r x (F s)
⊢ ∃ f, (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)
have h' : ∀ s : Finset α, ∃ y, (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y := fun s => ⟨F s, hF s⟩
α✝ : Type ?u.153481
β : Type ?u.153484
γ : Type ?u.153487
α : Type u_1
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → P (F s) ∧ ∀ (x : α), x ∈ s → r x (F s)
h' : ∀ (s : Finset α), ∃ y, (∀ (x : α), x ∈ s → P x) → P y ∧ ∀ (x : α), x ∈ s → r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
⊢ ∃ f, (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)
α✝ : Type ?u.153481
β : Type ?u.153484
γ : Type ?u.153487
α : Type u_1
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → P (F s) ∧ ∀ (x : α), x ∈ s → r x (F s)
h' : ∀ (s : Finset α), ∃ y, (∀ (x : α), x ∈ s → P x) → P y ∧ ∀ (x : α), x ∈ s → r x y
⊢ ∃ f, (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)
set f := seqOfForallFinsetExistsAux P r h' with hf
α✝ : Type ?u.153481
β : Type ?u.153484
γ : Type ?u.153487
α : Type u_1
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → P (F s) ∧ ∀ (x : α), x ∈ s → r x (F s)
h' : ∀ (s : Finset α), ∃ y, (∀ (x : α), x ∈ s → P x) → P y ∧ ∀ (x : α), x ∈ s → r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
A : ∀ (n : ℕ), P (f n)
⊢ ∃ f, (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)
α✝ : Type ?u.153481
β : Type ?u.153484
γ : Type ?u.153487
α : Type u_1
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → P (F s) ∧ ∀ (x : α), x ∈ s → r x (F s)
h' : ∀ (s : Finset α), ∃ y, (∀ (x : α), x ∈ s → P x) → P y ∧ ∀ (x : α), x ∈ s → r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
⊢ ∃ f, (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)
have A : ∀ n : ℕ, P (f n) := by
  intro n
  induction' n using Nat.strong_induction_on with n IH
  have IH' : ∀ x : Fin n, P (f x) := fun n => IH n.1 n.2
  rw [hf, seqOfForallFinsetExistsAux]
  exact
    (Classical.choose_spec
        (h' (Finset.image (fun i : Fin n => f i) (Finset.univ : Finset (Fin n))))
        (by simp [IH'])).1
α✝ : Type ?u.153481
β : Type ?u.153484
γ : Type ?u.153487
α : Type u_1
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → P (F s) ∧ ∀ (x : α), x ∈ s → r x (F s)
h' : ∀ (s : Finset α), ∃ y, (∀ (x : α), x ∈ s → P x) → P y ∧ ∀ (x : α), x ∈ s → r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
A : ∀ (n : ℕ), P (f n)
m n : ℕ
hmn : m < n
⊢ r (f m) (f n)
α✝ : Type ?u.153481
β : Type ?u.153484
γ : Type ?u.153487
α : Type u_1
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → P (F s) ∧ ∀ (x : α), x ∈ s → r x (F s)
h' : ∀ (s : Finset α), ∃ y, (∀ (x : α), x ∈ s → P x) → P y ∧ ∀ (x : α), x ∈ s → r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
A : ∀ (n : ℕ), P (f n)
⊢ ∃ f, (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)
refine' ⟨f, A, fun m n hmn => _⟩
α✝ : Type ?u.153481
β : Type ?u.153484
γ : Type ?u.153487
α : Type u_1
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → P (F s) ∧ ∀ (x : α), x ∈ s → r x (F s)
h' : ∀ (s : Finset α), ∃ y, (∀ (x : α), x ∈ s → P x) → P y ∧ ∀ (x : α), x ∈ s → r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
A : ∀ (n : ℕ), P (f n)
m n : ℕ
hmn : m < n
⊢ r (f m) (seqOfForallFinsetExistsAux P r h' n)
α✝ : Type ?u.153481
β : Type ?u.153484
γ : Type ?u.153487
α : Type u_1
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → P (F s) ∧ ∀ (x : α), x ∈ s → r x (F s)
h' : ∀ (s : Finset α), ∃ y, (∀ (x : α), x ∈ s → P x) → P y ∧ ∀ (x : α), x ∈ s → r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
A : ∀ (n : ℕ), P (f n)
m n : ℕ
hmn : m < n
⊢ r (f m) (f n)
conv_rhs => rw [hf]
α✝ : Type ?u.153481
β : Type ?u.153484
γ : Type ?u.153487
α : Type u_1
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → P (F s) ∧ ∀ (x : α), x ∈ s → r x (F s)
h' : ∀ (s : Finset α), ∃ y, (∀ (x : α), x ∈ s → P x) → P y ∧ ∀ (x : α), x ∈ s → r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
A : ∀ (n : ℕ), P (f n)
m n : ℕ
hmn : m < n
⊢ r (f m)
    (Classical.choose
      (_ :
        ∃ y,
          (∀ (x : α), x ∈ image (fun i => seqOfForallFinsetExistsAux P r h' ↑i) univ → P x) →
            P y ∧ ∀ (x : α), x ∈ image (fun i => seqOfForallFinsetExistsAux P r h' ↑i) univ → r x y))
α✝ : Type ?u.153481
β : Type ?u.153484
γ : Type ?u.153487
α : Type u_1
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → P (F s) ∧ ∀ (x : α), x ∈ s → r x (F s)
h' : ∀ (s : Finset α), ∃ y, (∀ (x : α), x ∈ s → P x) → P y ∧ ∀ (x : α), x ∈ s → r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
A : ∀ (n : ℕ), P (f n)
m n : ℕ
hmn : m < n
⊢ r (f m) (seqOfForallFinsetExistsAux P r h' n)
rw [seqOfForallFinsetExistsAux]
case a
α✝ : Type ?u.153481
β : Type ?u.153484
γ : Type ?u.153487
α : Type u_1
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → P (F s) ∧ ∀ (x : α), x ∈ s → r x (F s)
h' : ∀ (s : Finset α), ∃ y, (∀ (x : α), x ∈ s → P x) → P y ∧ ∀ (x : α), x ∈ s → r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
A : ∀ (n : ℕ), P (f n)
m n : ℕ
hmn : m < n
⊢ f m ∈ image (fun i => f ↑i) univ
α✝ : Type ?u.153481
β : Type ?u.153484
γ : Type ?u.153487
α : Type u_1
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → P (F s) ∧ ∀ (x : α), x ∈ s → r x (F s)
h' : ∀ (s : Finset α), ∃ y, (∀ (x : α), x ∈ s → P x) → P y ∧ ∀ (x : α), x ∈ s → r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
A : ∀ (n : ℕ), P (f n)
m n : ℕ
hmn : m < n
⊢ r (f m)
    (Classical.choose
      (_ :
        ∃ y,
          (∀ (x : α), x ∈ image (fun i => seqOfForallFinsetExistsAux P r h' ↑i) univ → P x) →
            P y ∧ ∀ (x : α), x ∈ image (fun i => seqOfForallFinsetExistsAux P r h' ↑i) univ → r x y))
apply
  (Classical.choose_spec
      (h' (Finset.image (fun i : Fin n => f i) (Finset.univ : Finset (Fin n)))) (by simp [A])).2
no goals
case a
α✝ : Type ?u.153481
β : Type ?u.153484
γ : Type ?u.153487
α : Type u_1
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → P (F s) ∧ ∀ (x : α), x ∈ s → r x (F s)
h' : ∀ (s : Finset α), ∃ y, (∀ (x : α), x ∈ s → P x) → P y ∧ ∀ (x : α), x ∈ s → r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
A : ∀ (n : ℕ), P (f n)
m n : ℕ
hmn : m < n
⊢ f m ∈ image (fun i => f ↑i) univ
exact Finset.mem_image.2 ⟨⟨m, hmn⟩, Finset.mem_univ _, rfl⟩
case intro
α✝ : Type ?u.153481
β : Type ?u.153484
γ : Type ?u.153487
α : Type u_1
P : α → Prop
r : α → α → Prop
h : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → ∃ y, P y ∧ ∀ (x : α), x ∈ s → r x y
y : α
h✝ : P y ∧ ∀ (x : α), x ∈ ∅ → r x y
⊢ Nonempty α
α✝ : Type ?u.153481
β : Type ?u.153484
γ : Type ?u.153487
α : Type u_1
P : α → Prop
r : α → α → Prop
h : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → ∃ y, P y ∧ ∀ (x : α), x ∈ s → r x y
⊢ Nonempty α
rcases h ∅ (by simp) with ⟨y, _⟩
no goals
case intro
α✝ : Type ?u.153481
β : Type ?u.153484
γ : Type ?u.153487
α : Type u_1
P : α → Prop
r : α → α → Prop
h : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → ∃ y, P y ∧ ∀ (x : α), x ∈ s → r x y
y : α
h✝ : P y ∧ ∀ (x : α), x ∈ ∅ → r x y
⊢ Nonempty α
exact ⟨y⟩
no goals
α✝ : Type ?u.153481
β : Type ?u.153484
γ : Type ?u.153487
α : Type u_1
P : α → Prop
r : α → α → Prop
h : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → ∃ y, P y ∧ ∀ (x : α), x ∈ s → r x y
⊢ ∀ (x : α), x ∈ ∅ → P x
simp
α✝ : Type ?u.153481
β : Type ?u.153484
γ : Type ?u.153487
α : Type u_1
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → P (F s) ∧ ∀ (x : α), x ∈ s → r x (F s)
h' : ∀ (s : Finset α), ∃ y, (∀ (x : α), x ∈ s → P x) → P y ∧ ∀ (x : α), x ∈ s → r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
n : ℕ
⊢ P (f n)
α✝ : Type ?u.153481
β : Type ?u.153484
γ : Type ?u.153487
α : Type u_1
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → P (F s) ∧ ∀ (x : α), x ∈ s → r x (F s)
h' : ∀ (s : Finset α), ∃ y, (∀ (x : α), x ∈ s → P x) → P y ∧ ∀ (x : α), x ∈ s → r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
⊢ ∀ (n : ℕ), P (f n)
intro n
case h
α✝ : Type ?u.153481
β : Type ?u.153484
γ : Type ?u.153487
α : Type u_1
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → P (F s) ∧ ∀ (x : α), x ∈ s → r x (F s)
h' : ∀ (s : Finset α), ∃ y, (∀ (x : α), x ∈ s → P x) → P y ∧ ∀ (x : α), x ∈ s → r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
n : ℕ
IH : ∀ (m : ℕ), m < n → P (f m)
⊢ P (f n)
α✝ : Type ?u.153481
β : Type ?u.153484
γ : Type ?u.153487
α : Type u_1
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → P (F s) ∧ ∀ (x : α), x ∈ s → r x (F s)
h' : ∀ (s : Finset α), ∃ y, (∀ (x : α), x ∈ s → P x) → P y ∧ ∀ (x : α), x ∈ s → r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
n : ℕ
⊢ P (f n)
induction' n using Nat.strong_induction_on with n IH
case h
α✝ : Type ?u.153481
β : Type ?u.153484
γ : Type ?u.153487
α : Type u_1
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → P (F s) ∧ ∀ (x : α), x ∈ s → r x (F s)
h' : ∀ (s : Finset α), ∃ y, (∀ (x : α), x ∈ s → P x) → P y ∧ ∀ (x : α), x ∈ s → r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
n : ℕ
IH : ∀ (m : ℕ), m < n → P (f m)
IH' : ∀ (x : Fin n), P (f ↑x)
⊢ P (f n)
case h
α✝ : Type ?u.153481
β : Type ?u.153484
γ : Type ?u.153487
α : Type u_1
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → P (F s) ∧ ∀ (x : α), x ∈ s → r x (F s)
h' : ∀ (s : Finset α), ∃ y, (∀ (x : α), x ∈ s → P x) → P y ∧ ∀ (x : α), x ∈ s → r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
n : ℕ
IH : ∀ (m : ℕ), m < n → P (f m)
⊢ P (f n)
have IH' : ∀ x : Fin n, P (f x) := fun n => IH n.1 n.2
case h
α✝ : Type ?u.153481
β : Type ?u.153484
γ : Type ?u.153487
α : Type u_1
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → P (F s) ∧ ∀ (x : α), x ∈ s → r x (F s)
h' : ∀ (s : Finset α), ∃ y, (∀ (x : α), x ∈ s → P x) → P y ∧ ∀ (x : α), x ∈ s → r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
n : ℕ
IH : ∀ (m : ℕ), m < n → P (f m)
IH' : ∀ (x : Fin n), P (f ↑x)
⊢ P
    (Classical.choose
      (_ :
        ∃ y,
          (∀ (x : α), x ∈ image (fun i => seqOfForallFinsetExistsAux P r h' ↑i) univ → P x) →
            P y ∧ ∀ (x : α), x ∈ image (fun i => seqOfForallFinsetExistsAux P r h' ↑i) univ → r x y))
case h
α✝ : Type ?u.153481
β : Type ?u.153484
γ : Type ?u.153487
α : Type u_1
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → P (F s) ∧ ∀ (x : α), x ∈ s → r x (F s)
h' : ∀ (s : Finset α), ∃ y, (∀ (x : α), x ∈ s → P x) → P y ∧ ∀ (x : α), x ∈ s → r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
n : ℕ
IH : ∀ (m : ℕ), m < n → P (f m)
IH' : ∀ (x : Fin n), P (f ↑x)
⊢ P (f n)
rw [hf, seqOfForallFinsetExistsAux]
no goals
case h
α✝ : Type ?u.153481
β : Type ?u.153484
γ : Type ?u.153487
α : Type u_1
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → P (F s) ∧ ∀ (x : α), x ∈ s → r x (F s)
h' : ∀ (s : Finset α), ∃ y, (∀ (x : α), x ∈ s → P x) → P y ∧ ∀ (x : α), x ∈ s → r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
n : ℕ
IH : ∀ (m : ℕ), m < n → P (f m)
IH' : ∀ (x : Fin n), P (f ↑x)
⊢ P
    (Classical.choose
      (_ :
        ∃ y,
          (∀ (x : α), x ∈ image (fun i => seqOfForallFinsetExistsAux P r h' ↑i) univ → P x) →
            P y ∧ ∀ (x : α), x ∈ image (fun i => seqOfForallFinsetExistsAux P r h' ↑i) univ → r x y))
exact
  (Classical.choose_spec
      (h' (Finset.image (fun i : Fin n => f i) (Finset.univ : Finset (Fin n))))
      (by simp [IH'])).1
no goals
α✝ : Type ?u.153481
β : Type ?u.153484
γ : Type ?u.153487
α : Type u_1
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → P (F s) ∧ ∀ (x : α), x ∈ s → r x (F s)
h' : ∀ (s : Finset α), ∃ y, (∀ (x : α), x ∈ s → P x) → P y ∧ ∀ (x : α), x ∈ s → r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
n : ℕ
IH : ∀ (m : ℕ), m < n → P (f m)
IH' : ∀ (x : Fin n), P (f ↑x)
⊢ ∀ (x : α), x ∈ image (fun i => f ↑i) univ → P x
simp [IH']
no goals
α✝ : Type ?u.153481
β : Type ?u.153484
γ : Type ?u.153487
α : Type u_1
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ (x : α), x ∈ s → P x) → P (F s) ∧ ∀ (x : α), x ∈ s → r x (F s)
h' : ∀ (s : Finset α), ∃ y, (∀ (x : α), x ∈ s → P x) → P y ∧ ∀ (x : α), x ∈ s → r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
A : ∀ (n : ℕ), P (f n)
m n : ℕ
hmn : m < n
⊢ ∀ (x : α), x ∈ image (fun i => f ↑i) univ → P x
simp [A]