-- Lean 4 proof step from Mathlib.InformationTheory.Coding.KraftMcMillan (goal)
Goal:
α : Type u_1
S : Finset (List α)
inst : Fintype α
inst_1 : Nonempty α
h : UniquelyDecodable (↑S : Set (List α))
r : ℕ
hr : r ≥ 1
We :
  HPow.hPow (α := ℝ) (∑ w ∈ S, HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ w.length) r ≤
    HMul.hMul (α := ℝ) (↑r : ℝ) (↑(S.sup List.length) : ℝ)
We₁ :
  let maxLen := S.sup List.length;
  HPow.hPow (α := ℝ) (∑ w ∈ S, HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ w.length) r ≤
    HMul.hMul (α := ℝ) (↑r : ℝ) (↑maxLen : ℝ)
We₂ :
  let maxLen := S.sup List.length;
  HPow.hPow (α := ℝ) (∑ w ∈ S, HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ w.length) r ≤
    HMul.hMul (α := ℝ) (↑r : ℝ) (↑maxLen : ℝ)
We₃ We₄ :
  let maxLen := S.sup List.length;
  let T : Finset (List α) := Finset.image (α := Fin r → ↥S) concatFn Finset.univ;
  ∀ (hlen_maps : ∀ (x : List α) (hx : x ∈ T), x.length ∈ Finset.Icc r (r * maxLen)),
    HPow.hPow (α := ℝ) (∑ w ∈ S, HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ w.length) r ≤
      HMul.hMul (α := ℝ) (↑r : ℝ) (↑maxLen : ℝ)
calc :
  let maxLen := S.sup List.length;
  let T : Finset (List α) := Finset.image (α := Fin r → ↥S) concatFn Finset.univ;
  ∀ (hlen_maps : ∀ (x : List α) (hx : x ∈ T), x.length ∈ Finset.Icc r (r * maxLen)),
    let D : ℝ := (↑(Fintype.card α) : ℝ);
    ∑ s ∈ Finset.Icc r (r * maxLen), ∑ x ∈ T with x.length = s, (1 / D) ^ x.length ≤
      HMul.hMul (α := ℝ) (↑r : ℝ) (↑maxLen : ℝ)
calc₁ :
  let maxLen := S.sup List.length;
  let T : Finset (List α) := Finset.image (α := Fin r → ↥S) concatFn Finset.univ;
  ∀ (hlen_maps : ∀ (x : List α) (hx : x ∈ T), x.length ∈ Finset.Icc r (r * maxLen)),
    ∑ i ∈ Finset.Icc r (r * maxLen),
        HPow.hPow (α := ℝ) (↑(Fintype.card α) : ℝ) i * HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ i ≤
      HMul.hMul (α := ℝ) (↑r : ℝ) (↑maxLen : ℝ)
⊢ HPow.hPow (α := ℝ) (∑ w ∈ S, HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ w.length) r ≤
    HMul.hMul (α := ℝ) (↑r : ℝ) (↑(S.sup List.length) : ℝ)
have calc₂ : ∀ (hr : GE.ge (α := ℕ) 0 1),
  let T : Finset (List α) := Finset.image (α := Fin 0 → ↥S) concatFn Finset.univ;
  ∀ (hlen_maps : ∀ (x : List α) (hx : x ∈ T), x.length ∈ Finset.Icc 0 (HMul.hMul (α := ℕ) 0 0)),
    ∑ i ∈ Finset.Icc 0 (HMul.hMul (α := ℕ) 0 0),
        HPow.hPow (α := ℝ) (↑(Fintype.card α) : ℝ) i * HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ i ≤
      HMul.hMul (α := ℝ) (↑0 : ℝ) (↑0 : ℝ)
Tactic: classical
  -- We use maxLen to bound lengths of `r`-fold concatenations.
  set maxLen := S.sup List.length
  -- Let `T` be the set of all concatenations of `r` codewords from `S`.
  let T : Finset (List α) := Finset.image concatFn (Finset.univ : Finset (Fin r → S))
  -- Any `x ∈ T` is a concatenation of `r` nonempty codewords, hence `r ≤ |x| ≤ r*maxLen`.
  have hlen_maps (x : List α) (hx : x ∈ T) : x.length ∈ Finset.Icc r (r * maxLen) := by
    rcases Finset.mem_image.mp hx with ⟨_, _, rfl⟩
    exact concatFn_length_mem_Icc
      (fun c hnil => h.epsilon_not_mem (by simpa [hnil] using c.prop))
  let D := (Fintype.card α : ℝ)
  -- Expand the `r`-th power as a sum over `r`-tuples of codewords;
  -- each tuple contributes the weight `(1/D)^{|concatFn w|}`.
  calc (∑ w ∈ S, (1 / (Fintype.card α) : ℝ) ^ w.length) ^ r
    _ = ∑ w : Fin r → S, ∏ i : Fin r, (1 / D) ^ (w i).val.length := by
      simpa [(Finset.sum_coe_sort S _).symm] using
        Fintype.sum_pow (f := fun c : S => (1 / D) ^ c.val.length) r
    -- Each tuple contributes the weight `(1/D)^{|concatFn w|}`.
    _ = ∑ w, (1 / D) ^ (concatFn w).length := by
      apply Fintype.sum_congr
      intro w
      simpa [concatFn_length] using Finset.prod_pow_eq_pow_sum Finset.univ _ _
    -- Unique decodability makes `concatFn` injective, so these concatenations are distinct;
    -- we can reindex the sum by the set `T` of words.
    _ = ∑ x ∈ T, (1 / D) ^ x.length :=
      (Finset.sum_image (f := fun x => (1 / D) ^ x.length)
        (fun _ _ _ _ hEq => concatFn_injective_of_uniquelyDecodable h r hEq)).symm
    -- Group the sum over `T` by the length `s`.
    -- The admissible lengths lie in `[r, r*maxLen]` by `hlen_maps`.
    _ = ∑ s ∈ Finset.Icc r (r * maxLen), ∑ x ∈ T with x.length = s, (1 / D) ^ x.length :=
      (Finset.sum_fiberwise_of_maps_to hlen_maps _).symm
  -- For each length `s`, the `s`-fiber contributes at most `D^s * (1/D)^s`:
  -- there are ≤ `D^s` words of length `s`, and each has weight `(1/D)^s`.
  apply le_trans (Finset.sum_le_sum (fun _ _ => sum_pow_length_filter_eq_le_card_mul))
  -- Summing these bounds over the interval s ∈ [r, r * maxLen] multiplies the term
  -- by the number of lengths. Since r ≥ 1, this count is at most r * maxLen.
  rcases r with (_ | _ | r) <;> rcases maxLen with (_ | _ | maxLen)
  all_goals try simp at *
  · positivity
  · rw [Nat.cast_sub] <;> push_cast <;> nlinarith only
Cleared hypotheses: r, hr