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

Tactic:
rw [Composition.ne_single_iff] at this

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 : ∀ (i : Fin c.length), c.blocksFun i < k
⊢ c.blocksFun j < n

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)
⊢ ((MultilinearMap.mkPiAlgebra ℝ (Fin j) ℝ) fun i => ∑ j ∈ Ico 1 n, r * (a ^ j * p j)) =
    r ^ j * (∑ k ∈ Ico 1 n, a ^ k * p k) ^ j

Tactic:
simp only [MultilinearMap.mkPiAlgebra_apply]

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)
⊢ ∏ i : Fin j, ∑ j ∈ Ico 1 n, r * (a ^ j * p j) = 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
⊢ ⟨k, c⟩ ∈ compPartialSumTarget 2 (n + 1) n

Tactic:
simp only [mem_compPartialSumTarget_iff]

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
⊢ 2 ≤ c.length ∧ c.length < n + 1 ∧ ∀ (j : Fin c.length), c.blocksFun j < n

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
⊢ ∀ (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, ⋯⟩))

Tactic:
intro j

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
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, ⋯⟩))

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)
⊢ (∑ 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

Tactic:
simp only [←
  MultilinearMap.map_sum_finset (MultilinearMap.mkPiAlgebra ℝ (Fin j) ℝ) fun _ (m : ℕ) =>
    r * (a ^ m * p m)]

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)
⊢ ((MultilinearMap.mkPiAlgebra ℝ (Fin j) ℝ) fun i => ∑ j ∈ Ico 1 n, r * (a ^ j * p j)) =
    r ^ j * (∑ k ∈ Ico 1 n, a ^ k * p k) ^ j

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
⊢ ∏ 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:
have K : (compChangeOfVariables 2 (n + 1) n ⟨k, blocksFun⟩ H).snd.length = k := by simp

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

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

Tactic:
rintro ⟨k, blocksFun⟩ H

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

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
this : ∀ (i : Fin c.length), c.blocksFun i < k
⊢ c.blocksFun j < n

Tactic:
exact (this j).trans_le (Nat.lt_succ_iff.mp hd.1.2)

Result:
no goals

Proof state:
case mk
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
k : ℕ
c : Composition k
hd : ⟨k, c⟩ ∈ (Ico 2 (n + 1)).sigma fun k => {c | 1 < c.length}.toFinset
⊢ ⟨k, c⟩ ∈ compPartialSumTarget 2 (n + 1) n

Tactic:
simp only [Set.mem_toFinset (s := {c | 1 < Composition.length c}), mem_Ico, mem_sigma,
  Set.mem_setOf_eq] at hd

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
⊢ ⟨k, c⟩ ∈ compPartialSumTarget 2 (n + 1) n

Proof state:
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
⊢ (compChangeOfVariables 2 (n + 1) n ⟨k, blocksFun⟩ H).snd.length = k

Tactic:
simp

Result:
no goals

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

Tactic:
rintro ⟨k, c⟩ hd

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