-- Mathlib/Analysis/Analytic/Inverse.lean
theorem radius_right_inv_pos_of_radius_pos_aux1 (n : ℕ) (p : ℕ → ℝ) (hp : ∀ k, 0 ≤ p k) {r a : ℝ}
    (hr : 0 ≤ r) (ha : 0 ≤ a) :
    ∑ k ∈ Ico 2 (n + 1),
        a ^ k *
          ∑ c ∈ ({c | 1 < Composition.length c}.toFinset : Finset (Composition k)),
            r ^ c.length * ∏ j, p (c.blocksFun j) ≤
      ∑ j ∈ Ico 2 (n + 1), r ^ j * (∑ k ∈ Ico 1 n, a ^ k * p k) ^ j :=
  calc
    ∑ k ∈ Ico 2 (n + 1),
          a ^ k *
            ∑ c ∈ ({c | 1 < Composition.length c}.toFinset : Finset (Composition k)),
              r ^ c.length * ∏ j, p (c.blocksFun j) =
        ∑ k ∈ Ico 2 (n + 1),
          ∑ c ∈ ({c | 1 < Composition.length c}.toFinset : Finset (Composition k)),
            ∏ j, r * (a ^ c.blocksFun j * p (c.blocksFun j))

Proof state:
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
⊢ ∑ x ∈ Ico 2 (n + 1),
      ∑ i ∈ {c | 1 < c.length}.toFinset, a ^ x * (r ^ i.length * ∏ j : Fin i.length, p (i.blocksFun j)) =
    ∑ k ∈ Ico 2 (n + 1),
      ∑ c ∈ {c | 1 < c.length}.toFinset, ∏ j : Fin c.length, r * (a ^ c.blocksFun j * p (c.blocksFun j))

Tactic:
congr! with k _ c

Result:
case a.a
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
k : ℕ
a✝¹ : k ∈ Ico 2 (n + 1)
c : Composition k
a✝ : c ∈ {c | 1 < c.length}.toFinset
⊢ a ^ k * (r ^ c.length * ∏ j : Fin c.length, p (c.blocksFun j)) =
    ∏ j : Fin c.length, r * (a ^ c.blocksFun j * p (c.blocksFun j))

Proof state:
case h.mk.h.e_5
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
k : ℕ
blocksFun : Fin k → ℕ
H : ⟨k, blocksFun⟩ ∈ compPartialSumSource 2 (n + 1) n
K : (compChangeOfVariables 2 (n + 1) n ⟨k, blocksFun⟩ H).snd.length = k
j : Fin k
⊢ r * (a ^ ⟨k, blocksFun⟩.snd j * p (⟨k, blocksFun⟩.snd j)) =
    r *
      (a ^ (compChangeOfVariables 2 (n + 1) n ⟨k, blocksFun⟩ H).snd.blocksFun ⟨↑j, ⋯⟩ *
        p ((compChangeOfVariables 2 (n + 1) n ⟨k, blocksFun⟩ H).snd.blocksFun ⟨↑j, ⋯⟩))

Tactic:
rw [compChangeOfVariables_blocksFun]

Result:
no goals

Proof state:
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
⊢ ∑ x ∈ (Ico 2 (n + 1)).sigma fun k => {c | 1 < c.length}.toFinset,
      ∏ j : Fin x.snd.length, r * (a ^ x.snd.blocksFun j * p (x.snd.blocksFun j)) ≤
    ∑ d ∈ compPartialSumTarget 2 (n + 1) n, ∏ j : Fin d.snd.length, r * (a ^ d.snd.blocksFun j * p (d.snd.blocksFun j))

Tactic:
refine
  sum_le_sum_of_subset_of_nonneg ?_ fun x _ _ =>
    prod_nonneg fun j _ => mul_nonneg hr (mul_nonneg (pow_nonneg ha _) (hp _))

Result:
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
⊢ ((Ico 2 (n + 1)).sigma fun k => {c | 1 < c.length}.toFinset) ⊆ compPartialSumTarget 2 (n + 1) n

Proof state:
case a.a
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
k : ℕ
a✝¹ : k ∈ Ico 2 (n + 1)
c : Composition k
a✝ : c ∈ {c | 1 < c.length}.toFinset
⊢ a ^ k * (r ^ c.length * ∏ j : Fin c.length, p (c.blocksFun j)) =
    ∏ j : Fin c.length, r * (a ^ c.blocksFun j * p (c.blocksFun j))

Tactic:
rw [prod_mul_distrib, prod_mul_distrib, prod_pow_eq_pow_sum, Composition.sum_blocksFun,
  prod_const, card_fin]

Result:
case a.a
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
k : ℕ
a✝¹ : k ∈ Ico 2 (n + 1)
c : Composition k
a✝ : c ∈ {c | 1 < c.length}.toFinset
⊢ a ^ k * (r ^ c.length * ∏ j : Fin c.length, p (c.blocksFun j)) =
    r ^ c.length * (a ^ k * ∏ x : Fin c.length, p (c.blocksFun x))

Proof state:
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
⊢ ∑ k ∈ Ico 2 (n + 1), a ^ k * ∑ c ∈ {c | 1 < c.length}.toFinset, r ^ c.length * ∏ j : Fin c.length, p (c.blocksFun j) =
    ∑ k ∈ Ico 2 (n + 1),
      ∑ c ∈ {c | 1 < c.length}.toFinset, ∏ j : Fin c.length, r * (a ^ c.blocksFun j * p (c.blocksFun j))

Tactic:
simp_rw [mul_sum]

Result:
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
⊢ ∑ x ∈ Ico 2 (n + 1),
      ∑ i ∈ {c | 1 < c.length}.toFinset, a ^ x * (r ^ i.length * ∏ j : Fin i.length, p (i.blocksFun j)) =
    ∑ k ∈ Ico 2 (n + 1),
      ∑ c ∈ {c | 1 < c.length}.toFinset, ∏ j : Fin c.length, r * (a ^ c.blocksFun j * p (c.blocksFun j))

Proof state:
case mk
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
k : ℕ
c : Composition k
hd : (2 ≤ k ∧ k < n + 1) ∧ 1 < c.length
⊢ 2 ≤ c.length ∧ c.length < n + 1 ∧ ∀ (j : Fin c.length), c.blocksFun j < n

Tactic:
refine ⟨hd.2, c.length_le.trans_lt hd.1.2, fun j => ?_⟩

Result:
case mk
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
k : ℕ
c : Composition k
hd : (2 ≤ k ∧ k < n + 1) ∧ 1 < c.length
j : Fin c.length
⊢ c.blocksFun j < n

Proof state:
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
⊢ ∑ e ∈ compPartialSumSource 2 (n + 1) n, ∏ j : Fin e.fst, r * (a ^ e.snd j * p (e.snd j)) =
    ∑ j ∈ Ico 2 (n + 1), r ^ j * (∑ k ∈ Ico 1 n, a ^ k * p k) ^ j

Tactic:
rw [compPartialSumSource,
  ← sum_sigma' (Ico 2 (n + 1))
    (fun k : ℕ => (Fintype.piFinset fun _ : Fin k => Ico 1 n : Finset (Fin k → ℕ)))
    (fun n e => ∏ j : Fin n, r * (a ^ e j * p (e j)))]

Result:
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
⊢ ∑ a_1 ∈ Ico 2 (n + 1), ∑ s ∈ Fintype.piFinset fun x => Ico 1 n, ∏ j : Fin a_1, r * (a ^ s j * p (s j)) =
    ∑ j ∈ Ico 2 (n + 1), r ^ j * (∑ k ∈ Ico 1 n, a ^ k * p k) ^ j

Proof state:
case mk
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
k : ℕ
c : Composition k
hd : (2 ≤ k ∧ k < n + 1) ∧ 1 < c.length
j : Fin c.length
⊢ c.blocksFun j < n

Tactic:
have : c ≠ Composition.single k (zero_lt_two.trans_le hd.1.1) := by
  simp [Composition.eq_single_iff_length, ne_of_gt hd.2]

Result:
case mk
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
k : ℕ
c : Composition k
hd : (2 ≤ k ∧ k < n + 1) ∧ 1 < c.length
j : Fin c.length
this : c ≠ Composition.single k ⋯
⊢ c.blocksFun j < n

Proof state:
case h.mk
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
k : ℕ
blocksFun : Fin k → ℕ
H : ⟨k, blocksFun⟩ ∈ compPartialSumSource 2 (n + 1) n
K : (compChangeOfVariables 2 (n + 1) n ⟨k, blocksFun⟩ H).snd.length = k
⊢ ∏ j : Fin ⟨k, blocksFun⟩.fst, r * (a ^ ⟨k, blocksFun⟩.snd j * p (⟨k, blocksFun⟩.snd j)) =
    ∏ j : Fin (compChangeOfVariables 2 (n + 1) n ⟨k, blocksFun⟩ H).snd.length,
      r *
        (a ^ (compChangeOfVariables 2 (n + 1) n ⟨k, blocksFun⟩ H).snd.blocksFun j *
          p ((compChangeOfVariables 2 (n + 1) n ⟨k, blocksFun⟩ H).snd.blocksFun j))

Tactic:
congr 2 <;> try rw [K]

Result:
case h.mk.h.e_5
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
k : ℕ
blocksFun : Fin k → ℕ
H : ⟨k, blocksFun⟩ ∈ compPartialSumSource 2 (n + 1) n
K : (compChangeOfVariables 2 (n + 1) n ⟨k, blocksFun⟩ H).snd.length = k
⊢ HEq (fun j => r * (a ^ ⟨k, blocksFun⟩.snd j * p (⟨k, blocksFun⟩.snd j))) fun j =>
    r *
      (a ^ (compChangeOfVariables 2 (n + 1) n ⟨k, blocksFun⟩ H).snd.blocksFun j *
        p ((compChangeOfVariables 2 (n + 1) n ⟨k, blocksFun⟩ H).snd.blocksFun j))

Proof state:
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
k : ℕ
c : Composition k
hd : (2 ≤ k ∧ k < n + 1) ∧ 1 < c.length
j : Fin c.length
⊢ c ≠ Composition.single k ⋯

Tactic:
simp [Composition.eq_single_iff_length, ne_of_gt hd.2]

Result:
no goals