-- Mathlib/Analysis/Analytic/Composition.lean
theorem compPartialSumTarget_tendsto_prod_atTop :
    Tendsto (fun (p : ℕ × ℕ) => compPartialSumTarget 0 p.1 p.2) atTop atTop

Proof state:
case h'.mk
n : ℕ
c : Composition n
⊢ ∃ n_1, ⟨n, c⟩ ∈ compPartialSumTarget 0 n_1.1 n_1.2

Tactic:
simp only [mem_compPartialSumTarget_iff]

Result:
case h'.mk
n : ℕ
c : Composition n
⊢ ∃ n_1, 0 ≤ c.length ∧ c.length < n_1.1 ∧ ∀ (j : Fin c.length), c.blocksFun j < n_1.2

Proof state:
⊢ Tendsto (fun p => compPartialSumTarget 0 p.1 p.2) atTop atTop

Tactic:
apply Monotone.tendsto_atTop_finset

Result:
case h

⊢ Monotone fun p => compPartialSumTarget 0 p.1 p.2

case h'

⊢ ∀ (x : (n : ℕ) × Composition n), ∃ n, x ∈ compPartialSumTarget 0 n.1 n.2

Proof state:
case h'.mk.intro
n✝ : ℕ
c : Composition n✝
n : ℕ
hn : n ∈ upperBounds ↑(Finset.image (fun i => c.blocksFun i) Finset.univ)
j : Fin c.length
⊢ c.blocksFun j ≤ n

Tactic:
apply hn

Result:
case h'.mk.intro.a
n✝ : ℕ
c : Composition n✝
n : ℕ
hn : n ∈ upperBounds ↑(Finset.image (fun i => c.blocksFun i) Finset.univ)
j : Fin c.length
⊢ c.blocksFun j ∈ ↑(Finset.image (fun i => c.blocksFun i) Finset.univ)

Proof state:
case h
m n : ℕ × ℕ
hmn : m ≤ n
a : (n : ℕ) × Composition n
ha : a ∈ (fun p => compPartialSumTarget 0 p.1 p.2) m
this✝ : ∀ i < m.1, i < n.1
this : ∀ i < m.2, i < n.2
⊢ a ∈ (fun p => compPartialSumTarget 0 p.1 p.2) n

Tactic:
aesop

Result:
no goals

Proof state:
case h

⊢ Monotone fun p => compPartialSumTarget 0 p.1 p.2

Tactic:
intro m n hmn a ha

Result:
case h
m n : ℕ × ℕ
hmn : m ≤ n
a : (n : ℕ) × Composition n
ha : a ∈ (fun p => compPartialSumTarget 0 p.1 p.2) m
⊢ a ∈ (fun p => compPartialSumTarget 0 p.1 p.2) n

Proof state:
case h'.mk.intro
n✝ : ℕ
c : Composition n✝
n : ℕ
hn : n ∈ upperBounds ↑(Finset.image (fun i => c.blocksFun i) Finset.univ)
⊢ ∃ n, 0 ≤ c.length ∧ c.length < n.1 ∧ ∀ (j : Fin c.length), c.blocksFun j < n.2

Tactic:
refine
  ⟨max n c.length + 1, bot_le, lt_of_le_of_lt (le_max_right n c.length) (lt_add_one _), fun j =>
    lt_of_le_of_lt (le_trans ?_ (le_max_left _ _)) (lt_add_one _)⟩

Result:
case h'.mk.intro
n✝ : ℕ
c : Composition n✝
n : ℕ
hn : n ∈ upperBounds ↑(Finset.image (fun i => c.blocksFun i) Finset.univ)
j : Fin c.length
⊢ c.blocksFun j ≤ n

Proof state:
case h
m n : ℕ × ℕ
hmn : m ≤ n
a : (n : ℕ) × Composition n
ha : a ∈ (fun p => compPartialSumTarget 0 p.1 p.2) m
⊢ a ∈ (fun p => compPartialSumTarget 0 p.1 p.2) n

Tactic:
have : ∀ i, i < m.1 → i < n.1 := fun i hi => lt_of_lt_of_le hi hmn.1

Result:
case h
m n : ℕ × ℕ
hmn : m ≤ n
a : (n : ℕ) × Composition n
ha : a ∈ (fun p => compPartialSumTarget 0 p.1 p.2) m
this : ∀ i < m.1, i < n.1
⊢ a ∈ (fun p => compPartialSumTarget 0 p.1 p.2) n

Proof state:
case h'.mk
n : ℕ
c : Composition n
⊢ ∃ n_1, 0 ≤ c.length ∧ c.length < n_1.1 ∧ ∀ (j : Fin c.length), c.blocksFun j < n_1.2

Tactic:
obtain ⟨n, hn⟩ : BddAbove ((Finset.univ.image fun i : Fin c.length => c.blocksFun i) : Set ℕ) :=
  Finset.bddAbove _

Result:
case h'.mk.intro
n✝ : ℕ
c : Composition n✝
n : ℕ
hn : n ∈ upperBounds ↑(Finset.image (fun i => c.blocksFun i) Finset.univ)
⊢ ∃ n, 0 ≤ c.length ∧ c.length < n.1 ∧ ∀ (j : Fin c.length), c.blocksFun j < n.2

Proof state:
case h
m n : ℕ × ℕ
hmn : m ≤ n
a : (n : ℕ) × Composition n
ha : a ∈ (fun p => compPartialSumTarget 0 p.1 p.2) m
this : ∀ i < m.1, i < n.1
⊢ a ∈ (fun p => compPartialSumTarget 0 p.1 p.2) n

Tactic:
have : ∀ i, i < m.2 → i < n.2 := fun i hi => lt_of_lt_of_le hi hmn.2

Result:
case h
m n : ℕ × ℕ
hmn : m ≤ n
a : (n : ℕ) × Composition n
ha : a ∈ (fun p => compPartialSumTarget 0 p.1 p.2) m
this✝ : ∀ i < m.1, i < n.1
this : ∀ i < m.2, i < n.2
⊢ a ∈ (fun p => compPartialSumTarget 0 p.1 p.2) n

Proof state:
case h'.mk.intro.a
n✝ : ℕ
c : Composition n✝
n : ℕ
hn : n ∈ upperBounds ↑(Finset.image (fun i => c.blocksFun i) Finset.univ)
j : Fin c.length
⊢ c.blocksFun j ∈ ↑(Finset.image (fun i => c.blocksFun i) Finset.univ)

Tactic:
simp only [Finset.mem_image_of_mem, Finset.mem_coe, Finset.mem_univ]

Result:
no goals

Proof state:
case h'

⊢ ∀ (x : (n : ℕ) × Composition n), ∃ n, x ∈ compPartialSumTarget 0 n.1 n.2

Tactic:
rintro ⟨n, c⟩

Result:
case h'.mk
n : ℕ
c : Composition n
⊢ ∃ n_1, ⟨n, c⟩ ∈ compPartialSumTarget 0 n_1.1 n_1.2