awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.InformationTheory.Coding.KraftMcMillan
Goal:
α : Type u_1
S : Finset (List α)
inst : Fintype α
inst_1 : Nonempty α
h : UniquelyDecodable (↑S : Set (List α))
maxLen : ℕ := S.sup List.length
D : ℝ := (↑(Fintype.card α) : ℝ)
hr : GE.ge (α := ℕ) 0 1
T : Finset (List α) := Finset.image (α := Fin 0 → ↥S) concatFn Finset.univ
hlen_maps : ∀ (x : List α) (hx : x ∈ T), x.length ∈ Finset.Icc 0 (0 * maxLen)
calc :
  ∀ (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₁ :
  ∀ (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₂ :
  ∀ (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) : ℝ)
⊢ ∑ i ∈ Finset.Icc 0 (0 * maxLen),
      HPow.hPow (α := ℝ) (↑(Fintype.card α) : ℝ) i * HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ i ≤
    HMul.hMul (α := ℝ) (↑0 : ℝ) (↑maxLen : ℝ)

Tactic:
rcases maxLen with (_ | _ | maxLen)
-- Module: Mathlib.InformationTheory.Coding.KraftMcMillan
Goal:
α : Type u_1
S : Finset (List α)
inst : Fintype α
inst_1 : Nonempty α
h : UniquelyDecodable (↑S : Set (List α))
maxLen : ℕ := S.sup List.length
D : ℝ := (↑(Fintype.card α) : ℝ)
hr : HAdd.hAdd (α := ℕ) 0 1 ≥ 1
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 * maxLen)
calc :
  ∀
    (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₁ :
  ∀
    (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₂ :
  ∀ (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) : ℝ)
⊢ ∑ i ∈ Finset.Icc (HAdd.hAdd (α := ℕ) 0 1) (HAdd.hAdd (α := ℕ) 0 1 * maxLen),
      HPow.hPow (α := ℝ) (↑(Fintype.card α) : ℝ) i * HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ i ≤
    HMul.hMul (α := ℝ) (↑(HAdd.hAdd (α := ℕ) 0 1) : ℝ) (↑maxLen : ℝ)

Tactic:
rcases maxLen with (_ | _ | maxLen)
-- Module: Mathlib.InformationTheory.Coding.KraftMcMillan
Goal:
α : Type u_1
S : Finset (List α)
inst : Fintype α
inst_1 : Nonempty α
h : UniquelyDecodable (↑S : Set (List α))
maxLen : ℕ := S.sup List.length
D : ℝ := (↑(Fintype.card α) : ℝ)
r : ℕ
hr : r + 1 + 1 ≥ 1
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) * maxLen)
calc :
  ∀ (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₁ :
  ∀ (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₂ :
  ∀ (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) : ℝ)
⊢ ∑ i ∈ Finset.Icc (r + 1 + 1) ((r + 1 + 1) * maxLen),
      HPow.hPow (α := ℝ) (↑(Fintype.card α) : ℝ) i * HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ i ≤
    HMul.hMul (α := ℝ) (↑(r + 1 + 1) : ℝ) (↑maxLen : ℝ)

Tactic:
rcases maxLen with (_ | _ | maxLen)
-- Module: Mathlib.InformationTheory.Coding.KraftMcMillan
Goal:
α : Type u_1
S : Finset (List α)
inst : Fintype α
inst_1 : Nonempty α
h : UniquelyDecodable (↑S : Set (List α))
D : ℝ := (↑(Fintype.card α) : ℝ)
hr : GE.ge (α := ℕ) 0 1
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:
simp at *
-- Module: Mathlib.InformationTheory.Coding.KraftMcMillan
Goal:
α : Type u_1
S : Finset (List α)
inst : Fintype α
inst_1 : Nonempty α
h : UniquelyDecodable (↑S : Set (List α))
D : ℝ := (↑(Fintype.card α) : ℝ)
hr : GE.ge (α := ℕ) 0 1
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:
try simp at *
-- Module: Mathlib.InformationTheory.Coding.KraftMcMillan
Goal:
α : Type u_1
S : Finset (List α)
inst : Fintype α
inst_1 : Nonempty α
h : UniquelyDecodable (↑S : Set (List α))
D : ℝ := (↑(Fintype.card α) : ℝ)
hr : GE.ge (α := ℕ) 0 1
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) : ℝ)

Tactic:
simp at *
-- Module: Mathlib.InformationTheory.Coding.KraftMcMillan
Goal:
α : Type u_1
S : Finset (List α)
inst : Fintype α
inst_1 : Nonempty α
h : UniquelyDecodable (↑S : Set (List α))
D : ℝ := (↑(Fintype.card α) : ℝ)
hr : GE.ge (α := ℕ) 0 1
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) : ℝ)

Tactic:
try simp at *
-- Module: Mathlib.InformationTheory.Coding.KraftMcMillan
Goal:
α : Type u_1
S : Finset (List α)
inst : Fintype α
inst_1 : Nonempty α
h : UniquelyDecodable (↑S : Set (List α))
D : ℝ := (↑(Fintype.card α) : ℝ)
hr : GE.ge (α := ℕ) 0 1
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) : ℝ)

Tactic:
simp at *
-- Module: Mathlib.InformationTheory.Coding.KraftMcMillan
Goal:
α : Type u_1
S : Finset (List α)
inst : Fintype α
inst_1 : Nonempty α
h : UniquelyDecodable (↑S : Set (List α))
D : ℝ := (↑(Fintype.card α) : ℝ)
hr : GE.ge (α := ℕ) 0 1
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) : ℝ)

Tactic:
try simp at *
-- Module: Mathlib.InformationTheory.Coding.KraftMcMillan
Goal:
α : Type u_1
S : Finset (List α)
inst : Fintype α
inst_1 : Nonempty α
h : UniquelyDecodable (↑S : Set (List α))
D : ℝ := (↑(Fintype.card α) : ℝ)
hr : HAdd.hAdd (α := ℕ) 0 1 ≥ 1
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 : ℝ)

Tactic:
simp at *
-- Module: Mathlib.InformationTheory.Coding.KraftMcMillan
Goal:
α : Type u_1
S : Finset (List α)
inst : Fintype α
inst_1 : Nonempty α
h : UniquelyDecodable (↑S : Set (List α))
D : ℝ := (↑(Fintype.card α) : ℝ)
hr : HAdd.hAdd (α := ℕ) 0 1 ≥ 1
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 : ℝ)

Tactic:
try simp at *
-- Module: Mathlib.InformationTheory.Coding.KraftMcMillan
Goal:
α : Type u_1
S : Finset (List α)
inst : Fintype α
inst_1 : Nonempty α
h : UniquelyDecodable (↑S : Set (List α))
D : ℝ := (↑(Fintype.card α) : ℝ)
hr : HAdd.hAdd (α := ℕ) 0 1 ≥ 1
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) : ℝ)

Tactic:
simp at *
-- Module: Mathlib.InformationTheory.Coding.KraftMcMillan
Goal:
α : Type u_1
S : Finset (List α)
inst : Fintype α
inst_1 : Nonempty α
h : UniquelyDecodable (↑S : Set (List α))
D : ℝ := (↑(Fintype.card α) : ℝ)
hr : HAdd.hAdd (α := ℕ) 0 1 ≥ 1
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) : ℝ)

Tactic:
try simp at *
-- Module: Mathlib.InformationTheory.Coding.KraftMcMillan
Goal:
α : Type u_1
S : Finset (List α)
inst : Fintype α
inst_1 : Nonempty α
h : UniquelyDecodable (↑S : Set (List α))
D : ℝ := (↑(Fintype.card α) : ℝ)
hr : HAdd.hAdd (α := ℕ) 0 1 ≥ 1
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) : ℝ)

Tactic:
simp at *
-- Module: Mathlib.InformationTheory.Coding.KraftMcMillan
Goal:
α : Type u_1
S : Finset (List α)
inst : Fintype α
inst_1 : Nonempty α
h : UniquelyDecodable (↑S : Set (List α))
D : ℝ := (↑(Fintype.card α) : ℝ)
hr : HAdd.hAdd (α := ℕ) 0 1 ≥ 1
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) : ℝ)

Tactic:
try simp at *
-- Module: Mathlib.InformationTheory.Coding.KraftMcMillan
Goal:
α : Type u_1
S : Finset (List α)
inst : Fintype α
inst_1 : Nonempty α
h : UniquelyDecodable (↑S : Set (List α))
D : ℝ := (↑(Fintype.card α) : ℝ)
r : ℕ
hr : r + 1 + 1 ≥ 1
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 : ℝ)

Tactic:
simp at *
-- Module: Mathlib.InformationTheory.Coding.KraftMcMillan
Goal:
α : Type u_1
S : Finset (List α)
inst : Fintype α
inst_1 : Nonempty α
h : UniquelyDecodable (↑S : Set (List α))
D : ℝ := (↑(Fintype.card α) : ℝ)
r : ℕ
hr : r + 1 + 1 ≥ 1
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 : ℝ)

Tactic:
try simp at *
-- Module: Mathlib.InformationTheory.Coding.KraftMcMillan
Goal:
α : Type u_1
S : Finset (List α)
inst : Fintype α
inst_1 : Nonempty α
h : UniquelyDecodable (↑S : Set (List α))
D : ℝ := (↑(Fintype.card α) : ℝ)
r : ℕ
hr : r + 1 + 1 ≥ 1
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)
calc : ∀ (hr : True) (hlen_maps : ∀ (x : List α) (hx : x ∈ T), x.length = r + 1 + 1), 0 ≤ HAdd.hAdd (α := ℝ) (↑r : ℝ) 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) : ℝ)

Tactic:
simp at *
-- Module: Mathlib.InformationTheory.Coding.KraftMcMillan
Goal:
α : Type u_1
S : Finset (List α)
inst : Fintype α
inst_1 : Nonempty α
h : UniquelyDecodable (↑S : Set (List α))
D : ℝ := (↑(Fintype.card α) : ℝ)
r : ℕ
hr : r + 1 + 1 ≥ 1
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)
calc : ∀ (hr : True) (hlen_maps : ∀ (x : List α) (hx : x ∈ T), x.length = r + 1 + 1), 0 ≤ HAdd.hAdd (α := ℝ) (↑r : ℝ) 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) : ℝ)

Tactic:
try simp at *
-- Module: Mathlib.InformationTheory.Coding.KraftMcMillan
Goal:
α : Type u_1
S : Finset (List α)
inst : Fintype α
inst_1 : Nonempty α
h : UniquelyDecodable (↑S : Set (List α))
D : ℝ := (↑(Fintype.card α) : ℝ)
r : ℕ
hr : r + 1 + 1 ≥ 1
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))
calc :
  ∀ (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)
⊢ ∑ 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) : ℝ)

Tactic:
simp at *
-- Module: Mathlib.InformationTheory.Coding.KraftMcMillan
Goal:
α : Type u_1
S : Finset (List α)
inst : Fintype α
inst_1 : Nonempty α
h : UniquelyDecodable (↑S : Set (List α))
D : ℝ := (↑(Fintype.card α) : ℝ)
r : ℕ
hr : r + 1 + 1 ≥ 1
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))
calc :
  ∀ (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)
⊢ ∑ 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) : ℝ)

Tactic:
try simp at *
-- Module: Mathlib.InformationTheory.Coding.KraftMcMillan
Goal:
α : Type u_1
S : Finset (List α)
inst : Fintype α
inst_1 : Nonempty α
h : UniquelyDecodable (↑S : Set (List α))
D : ℝ := (↑(Fintype.card α) : ℝ)
r : ℕ
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

Tactic:
positivity
-- Module: Mathlib.InformationTheory.Coding.KraftMcMillan
Goal:
α : Type u_1
S : Finset (List α)
inst : Fintype α
inst_1 : Nonempty α
h : UniquelyDecodable (↑S : Set (List α))
D : ℝ := (↑(Fintype.card α) : ℝ)
r : ℕ
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)
calc :
  HSub.hSub (α := ℝ) (↑((r + 1 + 1) * (maxLen + 1 + 1)) : ℝ) (↑(r + 1) : ℝ) ≤
    (HAdd.hAdd (α := ℝ) (↑r : ℝ) 1 + 1) * (HAdd.hAdd (α := ℝ) (↑maxLen : ℝ) 1 + 1)
calc₁ : r + 1 ≤ (r + 1 + 1) * (maxLen + 1 + 1)
⊢ (↑((r + 1 + 1) * (maxLen + 1 + 1) - (r + 1)) : ℝ) ≤
    (HAdd.hAdd (α := ℝ) (↑r : ℝ) 1 + 1) * (HAdd.hAdd (α := ℝ) (↑maxLen : ℝ) 1 + 1)

Tactic:
rw [Nat.cast_sub]

Premises used: Nat.cast_sub
-- Module: Mathlib.InformationTheory.Coding.KraftMcMillan
Goal:
α : Type u_1
S : Finset (List α)
inst : Fintype α
inst_1 : Nonempty α
h : UniquelyDecodable (↑S : Set (List α))
D : ℝ := (↑(Fintype.card α) : ℝ)
r : ℕ
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)
calc :
  (HAdd.hAdd (α := ℝ) (↑r : ℝ) 1 + 1) * (HAdd.hAdd (α := ℝ) (↑maxLen : ℝ) 1 + 1) - HAdd.hAdd (α := ℝ) (↑r : ℝ) 1 ≤
    (HAdd.hAdd (α := ℝ) (↑r : ℝ) 1 + 1) * (HAdd.hAdd (α := ℝ) (↑maxLen : ℝ) 1 + 1)
⊢ HSub.hSub (α := ℝ) (↑((r + 1 + 1) * (maxLen + 1 + 1)) : ℝ) (↑(r + 1) : ℝ) ≤
    (HAdd.hAdd (α := ℝ) (↑r : ℝ) 1 + 1) * (HAdd.hAdd (α := ℝ) (↑maxLen : ℝ) 1 + 1)

Tactic:
push_cast
-- Module: Mathlib.InformationTheory.Coding.KraftMcMillan
Goal:
α : Type u_1
S : Finset (List α)
inst : Fintype α
inst_1 : Nonempty α
h : UniquelyDecodable (↑S : Set (List α))
D : ℝ := (↑(Fintype.card α) : ℝ)
r : ℕ
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)
nlinarith :
  (HAdd.hAdd (α := ℝ) (↑r : ℝ) 1 + 1) * (HAdd.hAdd (α := ℝ) (↑maxLen : ℝ) 1 + 1) <
      (HAdd.hAdd (α := ℝ) (↑r : ℝ) 1 + 1) * (HAdd.hAdd (α := ℝ) (↑maxLen : ℝ) 1 + 1) - HAdd.hAdd (α := ℝ) (↑r : ℝ) 1 →
    -1 + HSub.hSub (α := ℝ) 0 (↑r : ℝ) +
        ((HAdd.hAdd (α := ℝ) (↑r : ℝ) 1 + 1) * (HAdd.hAdd (α := ℝ) (↑maxLen : ℝ) 1 + 1) -
          ((HAdd.hAdd (α := ℝ) (↑r : ℝ) 1 + 1) * (HAdd.hAdd (α := ℝ) (↑maxLen : ℝ) 1 + 1) -
            HAdd.hAdd (α := ℝ) (↑r : ℝ) 1)) =
      0
⊢ (HAdd.hAdd (α := ℝ) (↑r : ℝ) 1 + 1) * (HAdd.hAdd (α := ℝ) (↑maxLen : ℝ) 1 + 1) - HAdd.hAdd (α := ℝ) (↑r : ℝ) 1 ≤
    (HAdd.hAdd (α := ℝ) (↑r : ℝ) 1 + 1) * (HAdd.hAdd (α := ℝ) (↑maxLen : ℝ) 1 + 1)

Tactic:
nlinarith only
-- Module: Mathlib.InformationTheory.Coding.KraftMcMillan
Goal:
α : Type u_1
S : Finset (List α)
inst : Fintype α
inst_1 : Nonempty α
h : UniquelyDecodable (↑S : Set (List α))
D : ℝ := (↑(Fintype.card α) : ℝ)
r : ℕ
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)
nlinarith :
  (r + 1 + 1) * (maxLen + 1 + 1) < r + 1 →
    HMul.hMul (α := ℤ) 4 (-1) + HSub.hSub (α := ℤ) 0 (↑r : ℤ) + 2 * HSub.hSub (α := ℤ) 0 (↑maxLen : ℤ) +
          ((HAdd.hAdd (α := ℤ) (↑r : ℤ) 1 + 1) * (HAdd.hAdd (α := ℤ) (↑maxLen : ℤ) 1 + 1) + 1 -
            HAdd.hAdd (α := ℤ) (↑r : ℤ) 1) +
        (0 - HSub.hSub (α := ℤ) 0 (↑r : ℤ) * HSub.hSub (α := ℤ) 0 (↑maxLen : ℤ)) =
      0
nlinarith₁ : (r + 1 + 1) * (maxLen + 1 + 1) < r + 1 → GT.gt (α := ℤ) 4 0
nlinarith₂ : (r + 1 + 1) * (maxLen + 1 + 1) < r + 1 → GT.gt (α := ℤ) 2 0
⊢ r + 1 ≤ (r + 1 + 1) * (maxLen + 1 + 1)

Tactic:
nlinarith only
-- 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),
    HPow.hPow (α := ℝ) (∑ w ∈ S, HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ w.length) r ≤
      HMul.hMul (α := ℝ) (↑r : ℝ) (↑(S.sup List.length) : ℝ)

Tactic:
have h_kraft := kraft_mcmillan_inequality_aux h
-- Module: Mathlib.InformationTheory.Coding.KraftMcMillan
Goal:
α : Type u_1
S : Finset (List α)
inst : Fintype α
inst_1 : Nonempty α
h : UniquelyDecodable (↑S : Set (List α))
h_kraft :
  ∀ (r : ℕ) (hr : r ≥ 1),
    HPow.hPow (α := ℝ) (∑ w ∈ S, HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ w.length) r ≤
      HMul.hMul (α := ℝ) (↑r : ℝ) (↑(S.sup List.length) : ℝ)
contrapose! :
  ∀ (h_kraft : LT.lt (α := ℝ) 1 (∑ w ∈ S, HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ w.length)),
    ∃ r ≥ 1,
      HMul.hMul (α := ℝ) (↑r : ℝ) (↑(S.sup List.length) : ℝ) <
        HPow.hPow (α := ℝ) (∑ w ∈ S, HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ w.length) r
⊢ LE.le (α := ℝ) (∑ w ∈ S, HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ w.length) 1

Tactic:
contrapose! h_kraft