-- Mathlib/Data/Nat/Nth.lean
lemma nth_comp_of_strictMono {n : ℕ} {f : ℕ → ℕ} (hf : StrictMono f)
    (h0 : ∀ k, p k → k ∈ Set.range f) (h : ∀ hfi : (setOf p).Finite, n < hfi.toFinset.card) :
    f (nth (fun i ↦ p (f i)) n) = nth p n

Proof state:
case h
p : ℕ → Prop
n : ℕ
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
h : ∀ (hfi : (setOf p).Finite), n < #hfi.toFinset
p' : ℕ → Prop
h0p' : ∀ (k : ℕ), p' k → k ∈ Set.range f
i : ℕ
he : i ∈ setOf p'
⊢ i ∈ f '' {i | p' (f i)}

Tactic:
rcases h0p' _ he with ⟨t, rfl⟩

Result:
case h.intro
p : ℕ → Prop
n : ℕ
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
h : ∀ (hfi : (setOf p).Finite), n < #hfi.toFinset
p' : ℕ → Prop
h0p' : ∀ (k : ℕ), p' k → k ∈ Set.range f
t : ℕ
he : f t ∈ setOf p'
⊢ f t ∈ f '' {i | p' (f i)}

Proof state:
case intro
p : ℕ → Prop
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
hs : ∀ {p' : ℕ → Prop}, (∀ (k : ℕ), p' k → k ∈ Set.range f) → f '' {i | p' (f i)} = setOf p'
h : p (nth p 0)
t : ℕ
ht : f t = nth p 0
⊢ {i | p (f i)}.Nonempty

Tactic:
exact ⟨t, Set.mem_setOf_eq ▸ ht ▸ h⟩

Result:
no goals

Proof state:
p : ℕ → Prop
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
hs : ∀ {p' : ℕ → Prop}, (∀ (k : ℕ), p' k → k ∈ Set.range f) → f '' {i | p' (f i)} = setOf p'
h : p (nth p 0)
⊢ {i | p (f i)}.Nonempty

Tactic:
rcases h0 _ h with ⟨t, ht⟩

Result:
case intro
p : ℕ → Prop
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
hs : ∀ {p' : ℕ → Prop}, (∀ (k : ℕ), p' k → k ∈ Set.range f) → f '' {i | p' (f i)} = setOf p'
h : p (nth p 0)
t : ℕ
ht : f t = nth p 0
⊢ {i | p (f i)}.Nonempty

Proof state:
case h.e'_3.h.e'_1.h.e'_3.h.e'_2.h.h.e'_2.h.h'.a
p : ℕ → Prop
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
hs : ∀ {p' : ℕ → Prop}, (∀ (k : ℕ), p' k → k ∈ Set.range f) → f '' {i | p' (f i)} = setOf p'
n : ℕ
ih : ∀ m ≤ n, (∀ (hfi : (setOf p).Finite), m < #hfi.toFinset) → f (nth (fun i => p (f i)) m) = nth p m
h : ∀ (hfi : (setOf p).Finite), n + 1 < #hfi.toFinset
h0' : ∀ (k' : ℕ), (p k' ∧ ∀ k < n + 1, nth p k < k') → k' ∈ Set.range f
k m' : ℕ
hm : m' < n + 1
⊢ nth p m' < f k ↔ f (nth (fun i => p (f i)) m') < f k

Tactic:
convert Iff.rfl using 2

Result:
case h.e'_2.h.e'_3
p : ℕ → Prop
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
hs : ∀ {p' : ℕ → Prop}, (∀ (k : ℕ), p' k → k ∈ Set.range f) → f '' {i | p' (f i)} = setOf p'
n : ℕ
ih : ∀ m ≤ n, (∀ (hfi : (setOf p).Finite), m < #hfi.toFinset) → f (nth (fun i => p (f i)) m) = nth p m
h : ∀ (hfi : (setOf p).Finite), n + 1 < #hfi.toFinset
h0' : ∀ (k' : ℕ), (p k' ∧ ∀ k < n + 1, nth p k < k') → k' ∈ Set.range f
k m' : ℕ
hm : m' < n + 1
⊢ f (nth (fun i => p (f i)) m') = nth p m'

Proof state:
p : ℕ → Prop
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
hs : ∀ {p' : ℕ → Prop}, (∀ (k : ℕ), p' k → k ∈ Set.range f) → f '' {i | p' (f i)} = setOf p'
n : ℕ
ih : ∀ m ≤ n, (∀ (hfi : (setOf p).Finite), m < #hfi.toFinset) → f (nth (fun i => p (f i)) m) = nth p m
h : ∀ (hfi : (setOf p).Finite), n + 1 < #hfi.toFinset
⊢ f (nth (fun i => p (f i)) (n + 1)) = nth p (n + 1)

Tactic:
repeat nth_rw 1 [nth_eq_sInf]

Result:
p : ℕ → Prop
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
hs : ∀ {p' : ℕ → Prop}, (∀ (k : ℕ), p' k → k ∈ Set.range f) → f '' {i | p' (f i)} = setOf p'
n : ℕ
ih : ∀ m ≤ n, (∀ (hfi : (setOf p).Finite), m < #hfi.toFinset) → f (nth (fun i => p (f i)) m) = nth p m
h : ∀ (hfi : (setOf p).Finite), n + 1 < #hfi.toFinset
⊢ f (sInf {x | p (f x) ∧ ∀ k < n + 1, nth (fun i => p (f i)) k < x}) = sInf {x | p x ∧ ∀ k < n + 1, nth p k < x}

Proof state:
case h.e'_2.h.e'_3
p : ℕ → Prop
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
hs : ∀ {p' : ℕ → Prop}, (∀ (k : ℕ), p' k → k ∈ Set.range f) → f '' {i | p' (f i)} = setOf p'
n : ℕ
ih : ∀ m ≤ n, (∀ (hfi : (setOf p).Finite), m < #hfi.toFinset) → f (nth (fun i => p (f i)) m) = nth p m
h : ∀ (hfi : (setOf p).Finite), n + 1 < #hfi.toFinset
h0' : ∀ (k' : ℕ), (p k' ∧ ∀ k < n + 1, nth p k < k') → k' ∈ Set.range f
k m' : ℕ
hm : m' < n + 1
⊢ f (nth (fun i => p (f i)) m') = nth p m'

Tactic:
exact ih m' (Nat.lt_add_one_iff.mp hm) fun hfi ↦ hm.trans (h hfi)

Result:
no goals

Proof state:
p : ℕ → Prop
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
hs : ∀ {p' : ℕ → Prop}, (∀ (k : ℕ), p' k → k ∈ Set.range f) → f '' {i | p' (f i)} = setOf p'
h : p (nth p 0)
⊢ f (sInf {i | p (f i)}) = sInf (setOf p)

Tactic:
rw [← hs h0, ← hf.monotone.map_csInf]

Result:
p : ℕ → Prop
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
hs : ∀ {p' : ℕ → Prop}, (∀ (k : ℕ), p' k → k ∈ Set.range f) → f '' {i | p' (f i)} = setOf p'
h : p (nth p 0)
⊢ {i | p (f i)}.Nonempty

Proof state:
p : ℕ → Prop
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
hs : ∀ {p' : ℕ → Prop}, (∀ (k : ℕ), p' k → k ∈ Set.range f) → f '' {i | p' (f i)} = setOf p'
h : ∀ (hfi : (setOf p).Finite), 0 < #hfi.toFinset
⊢ f (sInf {i | p (f i)}) = sInf (setOf p)

Tactic:
replace h := nth_mem _ h

Result:
p : ℕ → Prop
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
hs : ∀ {p' : ℕ → Prop}, (∀ (k : ℕ), p' k → k ∈ Set.range f) → f '' {i | p' (f i)} = setOf p'
h : p (nth p 0)
⊢ f (sInf {i | p (f i)}) = sInf (setOf p)

Proof state:
case hz
p : ℕ → Prop
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
hs : ∀ {p' : ℕ → Prop}, (∀ (k : ℕ), p' k → k ∈ Set.range f) → f '' {i | p' (f i)} = setOf p'
h : ∀ (hfi : (setOf p).Finite), 0 < #hfi.toFinset
⊢ f (nth (fun i => p (f i)) 0) = nth p 0

case hi
p : ℕ → Prop
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
hs : ∀ {p' : ℕ → Prop}, (∀ (k : ℕ), p' k → k ∈ Set.range f) → f '' {i | p' (f i)} = setOf p'
n✝ : ℕ
a✝ : ∀ m ≤ n✝, (∀ (hfi : (setOf p).Finite), m < #hfi.toFinset) → f (nth (fun i => p (f i)) m) = nth p m
h : ∀ (hfi : (setOf p).Finite), n✝ + 1 < #hfi.toFinset
⊢ f (nth (fun i => p (f i)) (n✝ + 1)) = nth p (n✝ + 1)

Tactic:
case _ =>
  simp_rw [nth_zero]
  replace h := nth_mem _ h
  rw [← hs h0, ← hf.monotone.map_csInf]
  rcases h0 _ h with ⟨t, ht⟩
  exact ⟨t, Set.mem_setOf_eq ▸ ht ▸ h⟩

Result:
case hi
p : ℕ → Prop
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
hs : ∀ {p' : ℕ → Prop}, (∀ (k : ℕ), p' k → k ∈ Set.range f) → f '' {i | p' (f i)} = setOf p'
n✝ : ℕ
a✝ : ∀ m ≤ n✝, (∀ (hfi : (setOf p).Finite), m < #hfi.toFinset) → f (nth (fun i => p (f i)) m) = nth p m
h : ∀ (hfi : (setOf p).Finite), n✝ + 1 < #hfi.toFinset
⊢ f (nth (fun i => p (f i)) (n✝ + 1)) = nth p (n✝ + 1)

Proof state:
p : ℕ → Prop
n : ℕ
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
h : ∀ (hfi : (setOf p).Finite), n < #hfi.toFinset
⊢ f (nth (fun i => p (f i)) n) = nth p n

Tactic:
have hs {p' : ℕ → Prop} (h0p' : ∀ k, p' k → k ∈ Set.range f) :
    f '' {i | p' (f i)} = setOf p' := by
  ext i
  refine ⟨fun ⟨_, hi, h⟩ ↦ h ▸ hi, fun he ↦ ?_⟩
  rcases h0p' _ he with ⟨t, rfl⟩
  exact ⟨t, he, rfl⟩

Result:
p : ℕ → Prop
n : ℕ
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
h : ∀ (hfi : (setOf p).Finite), n < #hfi.toFinset
hs : ∀ {p' : ℕ → Prop}, (∀ (k : ℕ), p' k → k ∈ Set.range f) → f '' {i | p' (f i)} = setOf p'
⊢ f (nth (fun i => p (f i)) n) = nth p n

Proof state:
p : ℕ → Prop
n : ℕ
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
h : ∀ (hfi : (setOf p).Finite), n < #hfi.toFinset
p' : ℕ → Prop
h0p' : ∀ (k : ℕ), p' k → k ∈ Set.range f
⊢ f '' {i | p' (f i)} = setOf p'

Tactic:
ext i

Result:
case h
p : ℕ → Prop
n : ℕ
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
h : ∀ (hfi : (setOf p).Finite), n < #hfi.toFinset
p' : ℕ → Prop
h0p' : ∀ (k : ℕ), p' k → k ∈ Set.range f
i : ℕ
⊢ i ∈ f '' {i | p' (f i)} ↔ i ∈ setOf p'