-- 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:
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}) = nth p (n + 1)

Tactic:
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 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'
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
t : ℕ
ht : f t = nth p (n + 1)
⊢ {i | p (f i) ∧ ∀ k < n + 1, nth p k < f i}.Nonempty

Tactic:
exact ⟨t, ht ▸ (nth_mem _ h), fun _ hk ↦ ht ▸ nth_lt_nth' hk h⟩

Result:
no goals

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 : ℕ
⊢ i ∈ f '' {i | p' (f i)} ↔ i ∈ setOf p'

Tactic:
refine ⟨fun ⟨_, hi, h⟩ ↦ h ▸ hi, fun he ↦ ?_⟩

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 : ℕ
he : i ∈ setOf p'
⊢ i ∈ f '' {i | p' (f i)}

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
h0' : ∀ (k' : ℕ), (p k' ∧ ∀ k < n + 1, nth p k < k') → k' ∈ Set.range f
⊢ 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}

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'
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
⊢ f (sInf {x | p (f x) ∧ ∀ k < n + 1, nth (fun i => p (f i)) k < x}) =
    f (sInf {i | p (f i) ∧ ∀ k < n + 1, nth p k < f i})

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
⊢ {i | p (f i) ∧ ∀ k < n + 1, nth p k < 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 ↔ nth (fun i => p (f i)) m' < k

Tactic:
nth_rw 2 [← hf.lt_iff_lt]

Result:
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

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 (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}

Tactic:
have h0' : ∀ k', (p k' ∧ ∀ k < n + 1, nth p k < k') → k' ∈ Set.range f := fun _ h ↦ h0 _ h.1

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
h0' : ∀ (k' : ℕ), (p k' ∧ ∀ k < n + 1, nth p k < k') → k' ∈ Set.range f
⊢ 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:
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
⊢ f (sInf {x | p (f x) ∧ ∀ k < n + 1, nth (fun i => p (f i)) k < x}) =
    f (sInf {i | p (f i) ∧ ∀ k < n + 1, nth p k < f i})

Tactic:
convert rfl using 8 with k m' hm

Result:
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 ↔ nth (fun i => p (f i)) m' < k

Proof state:
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)}

Tactic:
exact ⟨t, he, rfl⟩

Result:
no goals