-- Module: Mathlib.InformationTheory.Coding.KraftMcMillan
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 : ℝ)
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 : ℝ)
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 (0 * HAdd.hAdd (α := ℕ) 0 1)),
      ∑ i ∈ Finset.Icc 0 (0 * HAdd.hAdd (α := ℕ) 0 1),
          HPow.hPow (α := ℝ) (↑(Fintype.card α) : ℝ) i * HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ i ≤
        HMul.hMul (α := ℝ) (↑0 : ℝ) (↑(HAdd.hAdd (α := ℕ) 0 1) : ℝ)
calc₄ :
  ∀ (hr : GE.ge (α := ℕ) 0 1),
    let T : Finset (List α) := Finset.image (α := Fin 0 → ↥S) concatFn Finset.univ;
    ∀ (maxLen : ℕ) (hlen_maps : ∀ (x : List α) (hx : x ∈ T), x.length ∈ Finset.Icc 0 (0 * (maxLen + 1 + 1))),
      ∑ i ∈ Finset.Icc 0 (0 * (maxLen + 1 + 1)),
          HPow.hPow (α := ℝ) (↑(Fintype.card α) : ℝ) i * HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ i ≤
        HMul.hMul (α := ℝ) (↑0 : ℝ) (↑(maxLen + 1 + 1) : ℝ)
calc₅ :
  ∀ (hr : HAdd.hAdd (α := ℕ) 0 1 ≥ 1),
    let T : Finset (List α) := Finset.image (α := Fin (HAdd.hAdd (α := ℕ) 0 1) → ↥S) concatFn Finset.univ;
    ∀
      (hlen_maps :
        ∀ (x : List α) (hx : x ∈ T), x.length ∈ Finset.Icc (HAdd.hAdd (α := ℕ) 0 1) (HAdd.hAdd (α := ℕ) 0 1 * 0)),
      ∑ i ∈ Finset.Icc (HAdd.hAdd (α := ℕ) 0 1) (HAdd.hAdd (α := ℕ) 0 1 * 0),
          HPow.hPow (α := ℝ) (↑(Fintype.card α) : ℝ) i * HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ i ≤
        HMul.hMul (α := ℝ) (↑(HAdd.hAdd (α := ℕ) 0 1) : ℝ) (↑0 : ℝ)
calc₆ :
  ∀ (hr : HAdd.hAdd (α := ℕ) 0 1 ≥ 1),
    let T : Finset (List α) := Finset.image (α := Fin (HAdd.hAdd (α := ℕ) 0 1) → ↥S) concatFn Finset.univ;
    ∀
      (hlen_maps :
        ∀ (x : List α) (hx : x ∈ T),
          x.length ∈ Finset.Icc (HAdd.hAdd (α := ℕ) 0 1) (HAdd.hAdd (α := ℕ) 0 1 * HAdd.hAdd (α := ℕ) 0 1)),
      ∑ i ∈ Finset.Icc (HAdd.hAdd (α := ℕ) 0 1) (HAdd.hAdd (α := ℕ) 0 1 * HAdd.hAdd (α := ℕ) 0 1),
          HPow.hPow (α := ℝ) (↑(Fintype.card α) : ℝ) i * HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ i ≤
        HMul.hMul (α := ℝ) (↑(HAdd.hAdd (α := ℕ) 0 1) : ℝ) (↑(HAdd.hAdd (α := ℕ) 0 1) : ℝ)
calc₇ :
  ∀ (hr : HAdd.hAdd (α := ℕ) 0 1 ≥ 1),
    let T : Finset (List α) := Finset.image (α := Fin (HAdd.hAdd (α := ℕ) 0 1) → ↥S) concatFn Finset.univ;
    ∀ (maxLen : ℕ)
      (hlen_maps :
        ∀ (x : List α) (hx : x ∈ T),
          x.length ∈ Finset.Icc (HAdd.hAdd (α := ℕ) 0 1) (HAdd.hAdd (α := ℕ) 0 1 * (maxLen + 1 + 1))),
      ∑ i ∈ Finset.Icc (HAdd.hAdd (α := ℕ) 0 1) (HAdd.hAdd (α := ℕ) 0 1 * (maxLen + 1 + 1)),
          HPow.hPow (α := ℝ) (↑(Fintype.card α) : ℝ) i * HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ i ≤
        HMul.hMul (α := ℝ) (↑(HAdd.hAdd (α := ℕ) 0 1) : ℝ) (↑(maxLen + 1 + 1) : ℝ)
calc₈ :
  ∀ (r : ℕ) (hr : r + 1 + 1 ≥ 1),
    let T : Finset (List α) := Finset.image (α := Fin (r + 1 + 1) → ↥S) concatFn Finset.univ;
    ∀ (hlen_maps : ∀ (x : List α) (hx : x ∈ T), x.length ∈ Finset.Icc (r + 1 + 1) ((r + 1 + 1) * 0)),
      ∑ i ∈ Finset.Icc (r + 1 + 1) ((r + 1 + 1) * 0),
          HPow.hPow (α := ℝ) (↑(Fintype.card α) : ℝ) i * HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ i ≤
        HMul.hMul (α := ℝ) (↑(r + 1 + 1) : ℝ) (↑0 : ℝ)
calc₉ :
  ∀ (r : ℕ) (hr : r + 1 + 1 ≥ 1),
    let T : Finset (List α) := Finset.image (α := Fin (r + 1 + 1) → ↥S) concatFn Finset.univ;
    ∀
      (hlen_maps :
        ∀ (x : List α) (hx : x ∈ T), x.length ∈ Finset.Icc (r + 1 + 1) ((r + 1 + 1) * HAdd.hAdd (α := ℕ) 0 1)),
      ∑ i ∈ Finset.Icc (r + 1 + 1) ((r + 1 + 1) * HAdd.hAdd (α := ℕ) 0 1),
          HPow.hPow (α := ℝ) (↑(Fintype.card α) : ℝ) i * HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ i ≤
        HMul.hMul (α := ℝ) (↑(r + 1 + 1) : ℝ) (↑(HAdd.hAdd (α := ℕ) 0 1) : ℝ)
calc₁₀ :
  ∀ (r : ℕ) (hr : r + 1 + 1 ≥ 1),
    let T : Finset (List α) := Finset.image (α := Fin (r + 1 + 1) → ↥S) concatFn Finset.univ;
    ∀ (maxLen : ℕ)
      (hlen_maps : ∀ (x : List α) (hx : x ∈ T), x.length ∈ Finset.Icc (r + 1 + 1) ((r + 1 + 1) * (maxLen + 1 + 1))),
      ∑ i ∈ Finset.Icc (r + 1 + 1) ((r + 1 + 1) * (maxLen + 1 + 1)),
          HPow.hPow (α := ℝ) (↑(Fintype.card α) : ℝ) i * HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ i ≤
        HMul.hMul (α := ℝ) (↑(r + 1 + 1) : ℝ) (↑(maxLen + 1 + 1) : ℝ)
calc₁₁ :
  ∀ (r : ℕ),
    let T : Finset (List α) := Finset.image (α := Fin (r + 1 + 1) → ↥S) concatFn Finset.univ;
    ∀ (hr : True) (hlen_maps : ∀ (x : List α) (hx : x ∈ T), x.length = r + 1 + 1), 0 ≤ HAdd.hAdd (α := ℝ) (↑r : ℝ) 1
calc₁₂ calc₁₃ :
  ∀ (r : ℕ),
    let T : Finset (List α) := Finset.image (α := Fin (r + 1 + 1) → ↥S) concatFn Finset.univ;
    ∀ (maxLen : ℕ) (hr : True)
      (hlen_maps : ∀ (x : List α) (hx : x ∈ T), r + 1 < x.length ∧ x.length ≤ (r + 1 + 1) * (maxLen + 1 + 1)),
      (↑((r + 1 + 1) * (maxLen + 1 + 1) - (r + 1)) : ℝ) ≤
        (HAdd.hAdd (α := ℝ) (↑r : ℝ) 1 + 1) * (HAdd.hAdd (α := ℝ) (↑maxLen : ℝ) 1 + 1)
⊢ HPow.hPow (α := ℝ) (∑ w ∈ S, HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ w.length) r ≤
    HMul.hMul (α := ℝ) (↑r : ℝ) (↑(S.sup List.length) : ℝ)

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

Premises used: Nat.cast_sub, Fintype.card, HDiv.hDiv, Nat.cast, HPow.hPow, Finset.sup, Finset.sum_le_sum, OfNat.ofNat, Fin, _private.0.InformationTheory.sum_pow_length_filter_eq_le_card_mul, List.length, Finset.sum, le_trans