-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
k : ℕ
blocksFun : Fin k → ℕ
H : Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun ∈ compPartialSumSource 2 (n + 1) n
K :
  (compChangeOfVariables 2 (n + 1) n (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) H).snd (β := fun (n : ℕ) ↦
        Composition n).length =
    k
h :
  Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) =
    (compChangeOfVariables 2 (n + 1) n (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) H).snd (β := fun (n : ℕ) ↦
        Composition n).length
h₁ :
  Fin (Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun)) =
    Fin
      (compChangeOfVariables 2 (n + 1) n (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) H).snd (β :=
          fun (n : ℕ) ↦ Composition n).length
h₂ :
  HEq (α :=
    Fintype (Fin (Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun))))
    (Fin.fintype (Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun))) (β :=
    Fintype
      (Fin
        (compChangeOfVariables 2 (n + 1) n (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) H).snd (β :=
            fun (n : ℕ) ↦ Composition n).length))
    (Fin.fintype
      (compChangeOfVariables 2 (n + 1) n (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) H).snd (β :=
          fun (n : ℕ) ↦ Composition n).length)
h₃ :
  HEq (α := Fin (Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun)) → ℝ)
    fun (j : Fin (Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun))) ↦
    r *
      (HPow.hPow (β := ℕ) a
          (Sigma.snd (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) j : ℕ) *
        p (Sigma.snd (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) j))
    (β :=
    Fin
        (compChangeOfVariables 2 (n + 1) n (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) H).snd (β :=
            fun (n : ℕ) ↦ Composition n).length →
      ℝ)
    fun
      (j :
        Fin
          (compChangeOfVariables 2 (n + 1) n (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) H).snd (β :=
              fun (n : ℕ) ↦ Composition n).length) ↦
    r *
      (a ^
          (compChangeOfVariables 2 (n + 1) n (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) H).snd (β :=
                fun (n : ℕ) ↦ Composition n).blocksFun
            j *
        p
          ((compChangeOfVariables 2 (n + 1) n (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) H).snd (β :=
                fun (n : ℕ) ↦ Composition n).blocksFun
            j))
⊢ Eq (α := ℝ)
    (∏ j : Fin ⟨k, blocksFun⟩.fst,
      r *
        (HPow.hPow (β := ℕ) a
            (Sigma.snd (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) j : ℕ) *
          p (Sigma.snd (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) j)))
    (∏ j : Fin (compChangeOfVariables 2 (n + 1) n ⟨k, blocksFun⟩ H).snd.length,
      r *
        (a ^
            (compChangeOfVariables 2 (n + 1) n (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) H).snd (β :=
                  fun (n : ℕ) ↦ Composition n).blocksFun
              j *
          p
            ((compChangeOfVariables 2 (n + 1) n (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocksFun) H).snd (β :=
                  fun (n : ℕ) ↦ Composition n).blocksFun
              j)))

Tactic:
congr 2