awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 α))
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) : ℝ)
⊢ ∑ i ∈ Finset.Icc 0 (0 * maxLen),
      HPow.hPow (α := ℝ) (↑(Fintype.card α) : ℝ) i * HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ i ≤
    HMul.hMul (α := ℝ) (↑0 : ℝ) (↑maxLen : ℝ)
have 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) : ℝ)
Tactic: rcases maxLen with (_ | _ | maxLen)
Cleared hypotheses: maxLen, hlen_maps
-- 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 α))
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)
⊢ ∑ 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 : ℝ)
have 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 : ℝ)
Tactic: rcases maxLen with (_ | _ | maxLen)
Cleared hypotheses: maxLen, hlen_maps
-- 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 α))
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 : ℝ)
⊢ ∑ 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 : ℝ)
have 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) : ℝ)
Tactic: rcases maxLen with (_ | _ | maxLen)
Cleared hypotheses: maxLen, hlen_maps
-- 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 α))
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) : ℝ)
⊢ ∑ 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 : ℝ)
have 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) : ℝ)
Tactic: rcases maxLen with (_ | _ | maxLen)
Cleared hypotheses: maxLen, hlen_maps
-- 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 α))
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)
⊢ ∑ 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 : ℝ)
have 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 : ℝ)
Tactic: rcases maxLen with (_ | _ | maxLen)
Cleared hypotheses: maxLen, hlen_maps
-- 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 α))
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 : ℝ)
⊢ ∑ 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 : ℝ)
have 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) : ℝ)
Tactic: rcases maxLen with (_ | _ | maxLen)
Cleared hypotheses: maxLen, hlen_maps
-- 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 α))
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) : ℝ)
⊢ ∑ 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 : ℝ)
have 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) : ℝ)
Tactic: rcases maxLen with (_ | _ | maxLen)
Cleared hypotheses: maxLen, hlen_maps
-- 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 α))
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)
⊢ ∑ 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) : ℝ)
have calc : ∀ (hr : True) (hlen_maps : ∀ (x : List α) (hx : x ∈ T), x.length = r + 1 + 1), 0 ≤ HAdd.hAdd (α := ℝ) (↑r : ℝ) 1
Tactic: simp at *
Cleared hypotheses: hr, hlen_maps
-- 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 α))
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)
⊢ ∑ 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) : ℝ)
have calc : ∀ (hr : True) (hlen_maps : ∀ (x : List α) (hx : x ∈ T), x.length = r + 1 + 1), 0 ≤ HAdd.hAdd (α := ℝ) (↑r : ℝ) 1
Tactic: try simp at *
Cleared hypotheses: hr, hlen_maps
-- 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 α))
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))
⊢ ∑ 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) : ℝ)
have 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)
Tactic: simp at *
Cleared hypotheses: hr, hlen_maps
-- 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 α))
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))
⊢ ∑ 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) : ℝ)
have 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)
Tactic: try simp at *
Cleared hypotheses: hr, hlen_maps
-- 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 α))
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)
⊢ (↑((r + 1 + 1) * (maxLen + 1 + 1) - (r + 1)) : ℝ) ≤
    (HAdd.hAdd (α := ℝ) (↑r : ℝ) 1 + 1) * (HAdd.hAdd (α := ℝ) (↑maxLen : ℝ) 1 + 1)
have calc : HSub.hSub (α := ℝ) (↑((r + 1 + 1) * (maxLen + 1 + 1)) : ℝ) (↑(r + 1) : ℝ) ≤
  (HAdd.hAdd (α := ℝ) (↑r : ℝ) 1 + 1) * (HAdd.hAdd (α := ℝ) (↑maxLen : ℝ) 1 + 1)
Tactic: rw [Nat.cast_sub]
-- 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 α))
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)
⊢ (↑((r + 1 + 1) * (maxLen + 1 + 1) - (r + 1)) : ℝ) ≤
    (HAdd.hAdd (α := ℝ) (↑r : ℝ) 1 + 1) * (HAdd.hAdd (α := ℝ) (↑maxLen : ℝ) 1 + 1)
have calc₁ : r + 1 ≤ (r + 1 + 1) * (maxLen + 1 + 1)
Tactic: rw [Nat.cast_sub]
-- 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 α))
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)
⊢ HSub.hSub (α := ℝ) (↑((r + 1 + 1) * (maxLen + 1 + 1)) : ℝ) (↑(r + 1) : ℝ) ≤
    (HAdd.hAdd (α := ℝ) (↑r : ℝ) 1 + 1) * (HAdd.hAdd (α := ℝ) (↑maxLen : ℝ) 1 + 1)
have 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)
Tactic: push_cast
-- 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 α))
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)
⊢ (HAdd.hAdd (α := ℝ) (↑r : ℝ) 1 + 1) * (HAdd.hAdd (α := ℝ) (↑maxLen : ℝ) 1 + 1) - HAdd.hAdd (α := ℝ) (↑r : ℝ) 1 ≤
    (HAdd.hAdd (α := ℝ) (↑r : ℝ) 1 + 1) * (HAdd.hAdd (α := ℝ) (↑maxLen : ℝ) 1 + 1)
have 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
Tactic: nlinarith only
-- 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 α))
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)
⊢ r + 1 ≤ (r + 1 + 1) * (maxLen + 1 + 1)
have 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
Tactic: nlinarith only
-- 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 α))
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
⊢ r + 1 ≤ (r + 1 + 1) * (maxLen + 1 + 1)
have nlinarith₁ : (r + 1 + 1) * (maxLen + 1 + 1) < r + 1 → GT.gt (α := ℤ) 4 0
Tactic: nlinarith only
-- 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 α))
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
⊢ r + 1 ≤ (r + 1 + 1) * (maxLen + 1 + 1)
have nlinarith₂ : (r + 1 + 1) * (maxLen + 1 + 1) < r + 1 → GT.gt (α := ℤ) 2 0
Tactic: nlinarith only
-- Lean 4 proof step from Mathlib.InformationTheory.Coding.KraftMcMillan (hypothesis)
Goal:
α : Type u_1
S : Finset (List α)
inst : Fintype α
inst_1 : Nonempty α
h : UniquelyDecodable (↑S : Set (List α))
⊢ LE.le (α := ℝ) (∑ w ∈ S, HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ w.length) 1
have 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) : ℝ)
Tactic: have h_kraft := kraft_mcmillan_inequality_aux h
-- 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 α))
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) : ℝ)
⊢ LE.le (α := ℝ) (∑ w ∈ S, HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ w.length) 1
have 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
Tactic: contrapose! h_kraft
Cleared hypotheses: h_kraft
-- 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 α))
h_kraft : LT.lt (α := ℝ) 1 (∑ w ∈ S, HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ w.length)
K : ℝ := ∑ w ∈ S, HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ w.length
maxLen : ℕ := S.sup List.length
grw : 1 < K
⊢ |1 / K| < 1
have grw₁ : 0 < K
Tactic: grw [abs_of_pos (by positivity), div_lt_one]
-- Lean 4 proof step from Mathlib.InformationTheory.Coding.KraftMcMillan (hypothesis)
Goal:
α : Type u_1
S : Finset (List α)
inst : Fintype α
inst_1 : Nonempty α
h : UniquelyDecodable (↑S : Set (List α))
h_kraft : LT.lt (α := ℝ) 1 (∑ w ∈ S, HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ w.length)
K : ℝ := ∑ w ∈ S, HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ w.length
maxLen : ℕ := S.sup List.length
⊢ ∃ r ≥ 1,
    HMul.hMul (α := ℝ) (↑r : ℝ) (↑(S.sup List.length) : ℝ) <
      HPow.hPow (α := ℝ) (∑ w ∈ S, HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ w.length) r
have hAbs : |1 / K| < 1
Tactic: have hAbs : |1 / K| < 1 := by
    grw [abs_of_pos (by positivity), div_lt_one] <;> grind