-- 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
⊢ ∑ k ∈ Ico 2 (n + 1),
      ∑ c ∈ {c | 1 < c.length}.toFinset, ∏ j : Fin c.length, r * (a ^ c.blocksFun j * p (c.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:
rw [sum_sigma']

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

Proof state:
case h.mk.h.e_4.e_2
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 (Fin.fintype ⟨k, blocksFun⟩.fst) (Fin.fintype (compChangeOfVariables 2 (n + 1) n ⟨k, blocksFun⟩ H).snd.length)

Tactic:
rw [K]

Result:
no goals

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

Tactic:
simp [prod_const, ← mul_sum, mul_pow]

Result:
no goals

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

Tactic:
symm

Result:
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)) =
    ∑ d ∈ compPartialSumTarget 2 (n + 1) n, ∏ j : Fin d.snd.length, r * (a ^ d.snd.blocksFun j * p (d.snd.blocksFun j))

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)) =
    ∑ d ∈ compPartialSumTarget 2 (n + 1) n, ∏ j : Fin d.snd.length, r * (a ^ d.snd.blocksFun j * p (d.snd.blocksFun j))

Tactic:
apply compChangeOfVariables_sum

Result:
case h
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
⊢ ∀ (e : (n : ℕ) × (Fin n → ℕ)) (he : e ∈ compPartialSumSource 2 (n + 1) n),
    ∏ j : Fin e.fst, r * (a ^ e.snd j * p (e.snd j)) =
      ∏ j : Fin (compChangeOfVariables 2 (n + 1) n e he).snd.length,
        r *
          (a ^ (compChangeOfVariables 2 (n + 1) n e he).snd.blocksFun j *
            p ((compChangeOfVariables 2 (n + 1) n e he).snd.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
⊢ 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))

Tactic:
rw [Fin.heq_fun_iff K.symm]

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
⊢ ∀ (i : Fin k),
    r * (a ^ ⟨k, blocksFun⟩.snd i * p (⟨k, blocksFun⟩.snd i)) =
      r *
        (a ^ (compChangeOfVariables 2 (n + 1) n ⟨k, blocksFun⟩ H).snd.blocksFun ⟨↑i, ⋯⟩ *
          p ((compChangeOfVariables 2 (n + 1) n ⟨k, blocksFun⟩ H).snd.blocksFun ⟨↑i, ⋯⟩))

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

Tactic:
congr! with j

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

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)) =
    r ^ c.length * (a ^ k * ∏ x : Fin c.length, p (c.blocksFun x))

Tactic:
ring

Result:
no goals

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

Tactic:
simp only [← @MultilinearMap.mkPiAlgebra_apply ℝ (Fin j) _ ℝ]

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