Module: Mathlib.InformationTheory.Coding.KraftMcMillan

Goal state before:
pp: case calc.step.zero.zero
α : Type u_1
S : Finset (List α)
inst✝¹ : Fintype α
inst✝ : Nonempty α
h : UniquelyDecodable ↑S
D : ℝ := ↑(Fintype.card α)
hr : 0 ≥ 1
T : Finset (List α) := Finset.image concatFn Finset.univ
hlen_maps : ∀ x ∈ T, x.length ∈ Finset.Icc 0 (0 * 0)
⊢ ∑ i ∈ Finset.Icc 0 (0 * 0), ↑(Fintype.card α) ^ i * (1 / ↑(Fintype.card α)) ^ i ≤ ↑0 * ↑0

pp: case calc.step.zero.succ.zero
α : Type u_1
S : Finset (List α)
inst✝¹ : Fintype α
inst✝ : Nonempty α
h : UniquelyDecodable ↑S
D : ℝ := ↑(Fintype.card α)
hr : 0 ≥ 1
T : Finset (List α) := Finset.image concatFn Finset.univ
hlen_maps : ∀ x ∈ T, x.length ∈ Finset.Icc 0 (0 * (0 + 1))
⊢ ∑ i ∈ Finset.Icc 0 (0 * (0 + 1)), ↑(Fintype.card α) ^ i * (1 / ↑(Fintype.card α)) ^ i ≤ ↑0 * ↑(0 + 1)

pp: case calc.step.zero.succ.succ
α : Type u_1
S : Finset (List α)
inst✝¹ : Fintype α
inst✝ : Nonempty α
h : UniquelyDecodable ↑S
D : ℝ := ↑(Fintype.card α)
hr : 0 ≥ 1
T : Finset (List α) := Finset.image concatFn Finset.univ
maxLen : ℕ
hlen_maps : ∀ x ∈ T, x.length ∈ Finset.Icc 0 (0 * (maxLen + 1 + 1))
⊢ ∑ i ∈ Finset.Icc 0 (0 * (maxLen + 1 + 1)), ↑(Fintype.card α) ^ i * (1 / ↑(Fintype.card α)) ^ i ≤
    ↑0 * ↑(maxLen + 1 + 1)

pp: case calc.step.succ.zero.zero
α : Type u_1
S : Finset (List α)
inst✝¹ : Fintype α
inst✝ : Nonempty α
h : UniquelyDecodable ↑S
D : ℝ := ↑(Fintype.card α)
hr : 0 + 1 ≥ 1
T : Finset (List α) := Finset.image concatFn Finset.univ
hlen_maps : ∀ x ∈ T, x.length ∈ Finset.Icc (0 + 1) ((0 + 1) * 0)
⊢ ∑ i ∈ Finset.Icc (0 + 1) ((0 + 1) * 0), ↑(Fintype.card α) ^ i * (1 / ↑(Fintype.card α)) ^ i ≤ ↑(0 + 1) * ↑0

pp: case calc.step.succ.zero.succ.zero
α : Type u_1
S : Finset (List α)
inst✝¹ : Fintype α
inst✝ : Nonempty α
h : UniquelyDecodable ↑S
D : ℝ := ↑(Fintype.card α)
hr : 0 + 1 ≥ 1
T : Finset (List α) := Finset.image concatFn Finset.univ
hlen_maps : ∀ x ∈ T, x.length ∈ Finset.Icc (0 + 1) ((0 + 1) * (0 + 1))
⊢ ∑ i ∈ Finset.Icc (0 + 1) ((0 + 1) * (0 + 1)), ↑(Fintype.card α) ^ i * (1 / ↑(Fintype.card α)) ^ i ≤
    ↑(0 + 1) * ↑(0 + 1)

pp: case calc.step.succ.zero.succ.succ
α : Type u_1
S : Finset (List α)
inst✝¹ : Fintype α
inst✝ : Nonempty α
h : UniquelyDecodable ↑S
D : ℝ := ↑(Fintype.card α)
hr : 0 + 1 ≥ 1
T : Finset (List α) := Finset.image concatFn Finset.univ
maxLen : ℕ
hlen_maps : ∀ x ∈ T, x.length ∈ Finset.Icc (0 + 1) ((0 + 1) * (maxLen + 1 + 1))
⊢ ∑ i ∈ Finset.Icc (0 + 1) ((0 + 1) * (maxLen + 1 + 1)), ↑(Fintype.card α) ^ i * (1 / ↑(Fintype.card α)) ^ i ≤
    ↑(0 + 1) * ↑(maxLen + 1 + 1)

pp: case calc.step.succ.succ.zero
α : Type u_1
S : Finset (List α)
inst✝¹ : Fintype α
inst✝ : Nonempty α
h : UniquelyDecodable ↑S
D : ℝ := ↑(Fintype.card α)
r : ℕ
hr : r + 1 + 1 ≥ 1
T : Finset (List α) := Finset.image concatFn Finset.univ
hlen_maps : ∀ x ∈ T, x.length ∈ Finset.Icc (r + 1 + 1) ((r + 1 + 1) * 0)
⊢ ∑ i ∈ Finset.Icc (r + 1 + 1) ((r + 1 + 1) * 0), ↑(Fintype.card α) ^ i * (1 / ↑(Fintype.card α)) ^ i ≤
    ↑(r + 1 + 1) * ↑0

pp: case calc.step.succ.succ.succ.zero
α : Type u_1
S : Finset (List α)
inst✝¹ : Fintype α
inst✝ : Nonempty α
h : UniquelyDecodable ↑S
D : ℝ := ↑(Fintype.card α)
r : ℕ
hr : r + 1 + 1 ≥ 1
T : Finset (List α) := Finset.image concatFn Finset.univ
hlen_maps : ∀ x ∈ T, x.length ∈ Finset.Icc (r + 1 + 1) ((r + 1 + 1) * (0 + 1))
⊢ ∑ i ∈ Finset.Icc (r + 1 + 1) ((r + 1 + 1) * (0 + 1)), ↑(Fintype.card α) ^ i * (1 / ↑(Fintype.card α)) ^ i ≤
    ↑(r + 1 + 1) * ↑(0 + 1)

pp: case calc.step.succ.succ.succ.succ
α : Type u_1
S : Finset (List α)
inst✝¹ : Fintype α
inst✝ : Nonempty α
h : UniquelyDecodable ↑S
D : ℝ := ↑(Fintype.card α)
r : ℕ
hr : r + 1 + 1 ≥ 1
T : Finset (List α) := Finset.image concatFn Finset.univ
maxLen : ℕ
hlen_maps : ∀ 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)), ↑(Fintype.card α) ^ i * (1 / ↑(Fintype.card α)) ^ i ≤
    ↑(r + 1 + 1) * ↑(maxLen + 1 + 1)

Tactic:
<;>

Goal state after:
case calc.step.zero.zero
α : Type u_1
S : Finset (List α)
inst✝¹ : Fintype α
inst✝ : Nonempty α
h : UniquelyDecodable ↑S
D : ℝ := ↑(Fintype.card α)
hr : 0 ≥ 1
T : Finset (List α) := Finset.image concatFn Finset.univ
hlen_maps : ∀ x ∈ T, x.length ∈ Finset.Icc 0 (0 * 0)
⊢ ∑ i ∈ Finset.Icc 0 (0 * 0), ↑(Fintype.card α) ^ i * (1 / ↑(Fintype.card α)) ^ i ≤ ↑0 * ↑0

case calc.step.zero.succ.zero
α : Type u_1
S : Finset (List α)
inst✝¹ : Fintype α
inst✝ : Nonempty α
h : UniquelyDecodable ↑S
D : ℝ := ↑(Fintype.card α)
hr : 0 ≥ 1
T : Finset (List α) := Finset.image concatFn Finset.univ
hlen_maps : ∀ x ∈ T, x.length ∈ Finset.Icc 0 (0 * (0 + 1))
⊢ ∑ i ∈ Finset.Icc 0 (0 * (0 + 1)), ↑(Fintype.card α) ^ i * (1 / ↑(Fintype.card α)) ^ i ≤ ↑0 * ↑(0 + 1)

case calc.step.zero.succ.succ
α : Type u_1
S : Finset (List α)
inst✝¹ : Fintype α
inst✝ : Nonempty α
h : UniquelyDecodable ↑S
D : ℝ := ↑(Fintype.card α)
hr : 0 ≥ 1
T : Finset (List α) := Finset.image concatFn Finset.univ
maxLen : ℕ
hlen_maps : ∀ x ∈ T, x.length ∈ Finset.Icc 0 (0 * (maxLen + 1 + 1))
⊢ ∑ i ∈ Finset.Icc 0 (0 * (maxLen + 1 + 1)), ↑(Fintype.card α) ^ i * (1 / ↑(Fintype.card α)) ^ i ≤
    ↑0 * ↑(maxLen + 1 + 1)

case calc.step.succ.zero.zero
α : Type u_1
S : Finset (List α)
inst✝¹ : Fintype α
inst✝ : Nonempty α
h : UniquelyDecodable ↑S
D : ℝ := ↑(Fintype.card α)
hr : 0 + 1 ≥ 1
T : Finset (List α) := Finset.image concatFn Finset.univ
hlen_maps : ∀ x ∈ T, x.length ∈ Finset.Icc (0 + 1) ((0 + 1) * 0)
⊢ ∑ i ∈ Finset.Icc (0 + 1) ((0 + 1) * 0), ↑(Fintype.card α) ^ i * (1 / ↑(Fintype.card α)) ^ i ≤ ↑(0 + 1) * ↑0

case calc.step.succ.zero.succ.zero
α : Type u_1
S : Finset (List α)
inst✝¹ : Fintype α
inst✝ : Nonempty α
h : UniquelyDecodable ↑S
D : ℝ := ↑(Fintype.card α)
hr : 0 + 1 ≥ 1
T : Finset (List α) := Finset.image concatFn Finset.univ
hlen_maps : ∀ x ∈ T, x.length ∈ Finset.Icc (0 + 1) ((0 + 1) * (0 + 1))
⊢ ∑ i ∈ Finset.Icc (0 + 1) ((0 + 1) * (0 + 1)), ↑(Fintype.card α) ^ i * (1 / ↑(Fintype.card α)) ^ i ≤
    ↑(0 + 1) * ↑(0 + 1)

case calc.step.succ.zero.succ.succ
α : Type u_1
S : Finset (List α)
inst✝¹ : Fintype α
inst✝ : Nonempty α
h : UniquelyDecodable ↑S
D : ℝ := ↑(Fintype.card α)
hr : 0 + 1 ≥ 1
T : Finset (List α) := Finset.image concatFn Finset.univ
maxLen : ℕ
hlen_maps : ∀ x ∈ T, x.length ∈ Finset.Icc (0 + 1) ((0 + 1) * (maxLen + 1 + 1))
⊢ ∑ i ∈ Finset.Icc (0 + 1) ((0 + 1) * (maxLen + 1 + 1)), ↑(Fintype.card α) ^ i * (1 / ↑(Fintype.card α)) ^ i ≤
    ↑(0 + 1) * ↑(maxLen + 1 + 1)

case calc.step.succ.succ.zero
α : Type u_1
S : Finset (List α)
inst✝¹ : Fintype α
inst✝ : Nonempty α
h : UniquelyDecodable ↑S
D : ℝ := ↑(Fintype.card α)
r : ℕ
hr : r + 1 + 1 ≥ 1
T : Finset (List α) := Finset.image concatFn Finset.univ
hlen_maps : ∀ x ∈ T, x.length ∈ Finset.Icc (r + 1 + 1) ((r + 1 + 1) * 0)
⊢ ∑ i ∈ Finset.Icc (r + 1 + 1) ((r + 1 + 1) * 0), ↑(Fintype.card α) ^ i * (1 / ↑(Fintype.card α)) ^ i ≤
    ↑(r + 1 + 1) * ↑0

case calc.step.succ.succ.succ.zero
α : Type u_1
S : Finset (List α)
inst✝¹ : Fintype α
inst✝ : Nonempty α
h : UniquelyDecodable ↑S
D : ℝ := ↑(Fintype.card α)
r : ℕ
hr : r + 1 + 1 ≥ 1
T : Finset (List α) := Finset.image concatFn Finset.univ
hlen_maps : ∀ x ∈ T, x.length ∈ Finset.Icc (r + 1 + 1) ((r + 1 + 1) * (0 + 1))
⊢ ∑ i ∈ Finset.Icc (r + 1 + 1) ((r + 1 + 1) * (0 + 1)), ↑(Fintype.card α) ^ i * (1 / ↑(Fintype.card α)) ^ i ≤
    ↑(r + 1 + 1) * ↑(0 + 1)

case calc.step.succ.succ.succ.succ
α : Type u_1
S : Finset (List α)
inst✝¹ : Fintype α
inst✝ : Nonempty α
h : UniquelyDecodable ↑S
D : ℝ := ↑(Fintype.card α)
r : ℕ
hr : r + 1 + 1 ≥ 1
T : Finset (List α) := Finset.image concatFn Finset.univ
maxLen : ℕ
hlen_maps : ∀ 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)), ↑(Fintype.card α) ^ i * (1 / ↑(Fintype.card α)) ^ i ≤
    ↑(r + 1 + 1) * ↑(maxLen + 1 + 1)