-- Mathlib/Data/Set/Finite/Basic.lean
theorem seq_of_forall_finite_exists {γ : Type*} {P : γ → Set γ → Prop}
    (h : ∀ t : Set γ, t.Finite → ∃ c, P c t) : ∃ u : ℕ → γ, ∀ n, P (u n) (u '' Iio n)

Proof state:
γ : Type u_1
P : γ → Set γ → Prop
h : ∀ (t : Set γ), t.Finite → ∃ c, P c t
this : Nonempty γ
⊢ ∃ u, ∀ (n : ℕ), P (u n) (u '' Iio n)

Tactic:
choose! c hc using h

Result:
γ : Type u_1
P : γ → Set γ → Prop
this : Nonempty γ
c : Set γ → γ
hc : ∀ (t : Set γ), t.Finite → P (c t) t
⊢ ∃ u, ∀ (n : ℕ), P (u n) (u '' Iio n)

Proof state:
γ : Type u_1
P : γ → Set γ → Prop
this : Nonempty γ
c : Set γ → γ
hc : ∀ (t : Set γ), t.Finite → P (c t) t
⊢ ∃ u, ∀ (n : ℕ), P (u n) (u '' Iio n)

Tactic:
set f : (n : ℕ) → (g : (m : ℕ) → m < n → γ) → γ := fun n g => c (range fun k : Iio n => g k.1 k.2)

Result:
γ : Type u_1
P : γ → Set γ → Prop
this : Nonempty γ
c : Set γ → γ
hc : ∀ (t : Set γ), t.Finite → P (c t) t
f : (n : ℕ) → ((m : ℕ) → m < n → γ) → γ := fun n g => c (range fun k => g ↑k ⋯)
⊢ ∃ u, ∀ (n : ℕ), P (u n) (u '' Iio n)

Proof state:
case h.e'_1
γ : Type u_1
P : γ → Set γ → Prop
this : Nonempty γ
c : Set γ → γ
hc : ∀ (t : Set γ), t.Finite → P (c t) t
f : (n : ℕ) → ((m : ℕ) → m < n → γ) → γ := fun n g => c (range fun k => g ↑k ⋯)
u : ℕ → γ := fun n => n.strongRecOn' f
n : ℕ
⊢ u n = c (u '' Iio n)

Tactic:
rw [image_eq_range]

Result:
case h.e'_1
γ : Type u_1
P : γ → Set γ → Prop
this : Nonempty γ
c : Set γ → γ
hc : ∀ (t : Set γ), t.Finite → P (c t) t
f : (n : ℕ) → ((m : ℕ) → m < n → γ) → γ := fun n g => c (range fun k => g ↑k ⋯)
u : ℕ → γ := fun n => n.strongRecOn' f
n : ℕ
⊢ u n = c (range fun x => u ↑x)

Proof state:
γ : Type u_1
P : γ → Set γ → Prop
this : Nonempty γ
c : Set γ → γ
hc : ∀ (t : Set γ), t.Finite → P (c t) t
f : (n : ℕ) → ((m : ℕ) → m < n → γ) → γ := fun n g => c (range fun k => g ↑k ⋯)
⊢ ∃ u, ∀ (n : ℕ), P (u n) (u '' Iio n)

Tactic:
set u : ℕ → γ := fun n => Nat.strongRecOn' n f

Result:
γ : Type u_1
P : γ → Set γ → Prop
this : Nonempty γ
c : Set γ → γ
hc : ∀ (t : Set γ), t.Finite → P (c t) t
f : (n : ℕ) → ((m : ℕ) → m < n → γ) → γ := fun n g => c (range fun k => g ↑k ⋯)
u : ℕ → γ := fun n => n.strongRecOn' f
⊢ ∃ u, ∀ (n : ℕ), P (u n) (u '' Iio n)

Proof state:
case h.e'_1
γ : Type u_1
P : γ → Set γ → Prop
this : Nonempty γ
c : Set γ → γ
hc : ∀ (t : Set γ), t.Finite → P (c t) t
f : (n : ℕ) → ((m : ℕ) → m < n → γ) → γ := fun n g => c (range fun k => g ↑k ⋯)
u : ℕ → γ := fun n => n.strongRecOn' f
n : ℕ
⊢ u n = c (range fun x => u ↑x)

Tactic:
exact Nat.strongRecOn'_beta

Result:
no goals

Proof state:
γ : Type u_1
P : γ → Set γ → Prop
this : Nonempty γ
c : Set γ → γ
hc : ∀ (t : Set γ), t.Finite → P (c t) t
f : (n : ℕ) → ((m : ℕ) → m < n → γ) → γ := fun n g => c (range fun k => g ↑k ⋯)
u : ℕ → γ := fun n => n.strongRecOn' f
n : ℕ
⊢ P (u n) (u '' Iio n)

Tactic:
convert hc (u '' Iio n) ((finite_lt_nat _).image _)

Result:
case h.e'_1
γ : Type u_1
P : γ → Set γ → Prop
this : Nonempty γ
c : Set γ → γ
hc : ∀ (t : Set γ), t.Finite → P (c t) t
f : (n : ℕ) → ((m : ℕ) → m < n → γ) → γ := fun n g => c (range fun k => g ↑k ⋯)
u : ℕ → γ := fun n => n.strongRecOn' f
n : ℕ
⊢ u n = c (u '' Iio n)

Proof state:
γ : Type u_1
P : γ → Set γ → Prop
h : ∀ (t : Set γ), t.Finite → ∃ c, P c t
⊢ ∃ u, ∀ (n : ℕ), P (u n) (u '' Iio n)

Tactic:
haveI : Nonempty γ := (h ∅ finite_empty).nonempty

Result:
γ : Type u_1
P : γ → Set γ → Prop
h : ∀ (t : Set γ), t.Finite → ∃ c, P c t
this : Nonempty γ
⊢ ∃ u, ∀ (n : ℕ), P (u n) (u '' Iio n)

Proof state:
γ : Type u_1
P : γ → Set γ → Prop
this : Nonempty γ
c : Set γ → γ
hc : ∀ (t : Set γ), t.Finite → P (c t) t
f : (n : ℕ) → ((m : ℕ) → m < n → γ) → γ := fun n g => c (range fun k => g ↑k ⋯)
u : ℕ → γ := fun n => n.strongRecOn' f
⊢ ∃ u, ∀ (n : ℕ), P (u n) (u '' Iio n)

Tactic:
refine ⟨u, fun n => ?_⟩

Result:
γ : Type u_1
P : γ → Set γ → Prop
this : Nonempty γ
c : Set γ → γ
hc : ∀ (t : Set γ), t.Finite → P (c t) t
f : (n : ℕ) → ((m : ℕ) → m < n → γ) → γ := fun n g => c (range fun k => g ↑k ⋯)
u : ℕ → γ := fun n => n.strongRecOn' f
n : ℕ
⊢ P (u n) (u '' Iio n)