awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.QuotientGroup.Basic
Goal:
R : Type u_1
inst : NonAssocRing R
N : AddSubgroup R
inst_1 : N.Normal
n : ℤ
a : R
rw : (↑(n • a) : R ⧸ N) = HSMul.hSMul (β := R ⧸ N) n (↑a : R ⧸ N)
rw₁ rw₂ : HSMul.hSMul (β := R ⧸ N) n (↑a : R ⧸ N) = HSMul.hSMul (β := R ⧸ N) n (↑a : R ⧸ N)
⊢ (↑((↑n : R) * a) : R ⧸ N) = HSMul.hSMul (β := R ⧸ N) n (↑a : R ⧸ N)

Tactic:
rw [← zsmul_eq_mul, mk_zsmul N a n]

Premises used: zsmul_eq_mul, QuotientAddGroup.mk_zsmul
-- Module: Mathlib.GroupTheory.QuotientGroup.Basic
Goal:
ι : Type u_1
A : ι → Type u_2
inst : (i : ι) → CommGroup (A i)
n : ℕ
⊢ Eq (α := (i : ι) → HasQuotient.Quotient (A i) (B := Subgroup (A i)) (MonoidHom.range (G := A i) (powMonoidHom n)))
    (fun (x : ι) ↦ (↑(1 x) : A x ⧸ (powMonoidHom n).range)) 1

Tactic:
simp [Pi.one_def]

Premises used: Pi.one_def
-- Module: Mathlib.GroupTheory.QuotientGroup.Basic
Goal:
ι : Type u_1
A : ι → Type u_2
inst : (i : ι) → CommGroup (A i)
n : ℕ
x y : (i : ι) → A i
⊢ (fun (x_1 : ι) ↦ (↑((x * y) x_1) : A x_1 ⧸ (powMonoidHom n).range)) =
    HMul.hMul (α :=
      (i : ι) → HasQuotient.Quotient (A i) (B := Subgroup (A i)) (MonoidHom.range (G := A i) (powMonoidHom n)))
      (fun (x_1 : ι) ↦ (↑(x x_1) : A x_1 ⧸ (powMonoidHom n).range)) fun (x : ι) ↦
      (↑(y x) : A x ⧸ (powMonoidHom n).range)

Tactic:
simp [Pi.mul_def]

Premises used: Pi.mul_def
-- Module: Mathlib.GroupTheory.QuotientGroup.Basic
Goal:
ι : Type u_1
A : ι → Type u_2
inst : (i : ι) → CommGroup (A i)
n : ℕ
φ : ((i : ι) → A i) →*
  (i : ι) → HasQuotient.Quotient (A i) (B := Subgroup (A i)) (MonoidHom.range (G := A i) (powMonoidHom n)) :=
  { toFun := fun (x : (i : ι) → A i) (x_1 : ι) ↦ (↑(x x_1) : A x_1 ⧸ (powMonoidHom n).range), map_one' := ⋯,
    map_mul' := ⋯ }
y : (i : ι) → HasQuotient.Quotient (A i) (B := Subgroup (A i)) (MonoidHom.range (G := A i) (powMonoidHom n))
⊢ ((φ : (a : (i : ι) → A i) → (i : ι) → A i ⧸ (powMonoidHom n).range) fun (i : ι) ↦ Quotient.out (y i)) = y

Tactic:
simp [φ]
-- Module: Mathlib.GroupTheory.QuotientGroup.Basic
Goal:
ι : Type u_1
A : ι → Type u_2
inst : (i : ι) → CommGroup (A i)
n : ℕ
φ : ((i : ι) → A i) →*
  (i : ι) → HasQuotient.Quotient (A i) (B := Subgroup (A i)) (MonoidHom.range (G := A i) (powMonoidHom n)) :=
  { toFun := fun (x : (i : ι) → A i) (x_1 : ι) ↦ (↑(x x_1) : A x_1 ⧸ (powMonoidHom n).range), map_one' := ⋯,
    map_mul' := ⋯ }
h :
  ∀ (x : (i : ι) → A i),
    Membership.mem (γ := Subgroup ((i : ι) → A i)) (MonoidHom.range (G := (i : ι) → A i) (powMonoidHom n)) x ↔
      Membership.mem (γ := Subgroup ((i : ι) → A i)) φ.ker x
⊢ Eq (α := Subgroup ((i : ι) → A i)) (MonoidHom.range (G := (i : ι) → A i) (powMonoidHom n)) φ.ker

Tactic:
ext x : 1
-- Module: Mathlib.GroupTheory.QuotientGroup.Basic
Goal:
ι : Type u_1
A : ι → Type u_2
inst : (i : ι) → CommGroup (A i)
n : ℕ
φ : ((i : ι) → A i) →*
  (i : ι) → HasQuotient.Quotient (A i) (B := Subgroup (A i)) (MonoidHom.range (G := A i) (powMonoidHom n)) :=
  { toFun := fun (x : (i : ι) → A i) (x_1 : ι) ↦ (↑(x x_1) : A x_1 ⧸ (powMonoidHom n).range), map_one' := ⋯,
    map_mul' := ⋯ }
x : (i : ι) → A i
⊢ Membership.mem (γ := Subgroup ((i : ι) → A i)) (MonoidHom.range (G := (i : ι) → A i) (powMonoidHom n)) x ↔
    Membership.mem (γ := Subgroup ((i : ι) → A i)) φ.ker x

Tactic:
simpa [φ, funext_iff] using (Classical.skolem (p := fun i a ↦ a ^ n = x i)).symm

Premises used: Classical.skolem, funext_iff, Iff.symm
-- Module: Mathlib.GroupTheory.QuotientGroup.Basic
Goal:
ι : Type u_1
A : ι → Type u_2
inst : (i : ι) → CommGroup (A i)
n : ℕ
x : (i : ι) → A i
⊢ Eq (α := (i : ι) → HasQuotient.Quotient (A i) (B := Subgroup (A i)) (MonoidHom.range (G := A i) (powMonoidHom n)))
    ((mulEquivPiModRangePowMonoidHom A n :
          (a : ((i : ι) → A i) ⧸ (powMonoidHom n).range) → (i : ι) → A i ⧸ (powMonoidHom n).range)
        (↑x : ((i : ι) → A i) ⧸ (powMonoidHom n).range) :
      (i : ι) → HasQuotient.Quotient (A i) (B := Subgroup (A i)) (MonoidHom.range (G := A i) (powMonoidHom n)))
    fun (i : ι) ↦
    ((↑(x i) : HasQuotient.Quotient (A i) (B := Subgroup (A i)) (MonoidHom.range (G := A i) (powMonoidHom n))) :
      HasQuotient.Quotient (A i) (B := Subgroup (A i)) (MonoidHom.range (G := A i) (powMonoidHom n)))

Tactic:
rfl

Premises used: Quotient.liftOn', Con.liftOn, rfl
-- Module: Mathlib.InformationTheory.Coding.KraftMcMillan
Goal:
α : Type u_1
S : Finset (List α)
r : ℕ
w : Fin r → ↥S
⊢ (concatFn w).length = ∑ i : Fin r, (↑(w i) : List α).length

Tactic:
simp [List.sum_ofFn, concatFn]

Premises used: List.sum_ofFn, _private.0.InformationTheory.concatFn
-- Module: Mathlib.InformationTheory.Coding.KraftMcMillan
Goal:
α : Type u_1
S : Finset (List α)
h : UniquelyDecodable (↑S : Set (List α))
r : ℕ
w₁ w₂ : Fin r → ↥S
hflat : concatFn w₁ = concatFn w₂
h₁ : ∀ (i : Fin r), w₁ i = w₂ i
⊢ w₁ = w₂

Tactic:
funext i
-- Module: Mathlib.InformationTheory.Coding.KraftMcMillan
Goal:
α : Type u_1
S : Finset (List α)
h : UniquelyDecodable (↑S : Set (List α))
r : ℕ
w₁ w₂ : Fin r → ↥S
hflat : concatFn w₁ = concatFn w₂
i : Fin r
⊢ ∀ (w : List α),
    Membership.mem (γ := List (List α)) (List.ofFn (n := r) fun (i : Fin r) ↦ (↑(w₁ i) : List α)) w →
      w ∈ (↑S : Set (List α))

Tactic:
simp
-- Module: Mathlib.InformationTheory.Coding.KraftMcMillan
Goal:
α : Type u_1
S : Finset (List α)
h : UniquelyDecodable (↑S : Set (List α))
r : ℕ
w₁ w₂ : Fin r → ↥S
hflat : concatFn w₁ = concatFn w₂
i : Fin r
⊢ ∀ (w : List α),
    Membership.mem (γ := List (List α)) (List.ofFn (n := r) fun (i : Fin r) ↦ (↑(w₂ i) : List α)) w →
      w ∈ (↑S : Set (List α))

Tactic:
simp
-- Module: Mathlib.InformationTheory.Coding.KraftMcMillan
Goal:
α : Type u_1
S : Finset (List α)
h : UniquelyDecodable (↑S : Set (List α))
r : ℕ
w₁ w₂ : Fin r → ↥S
hflat : concatFn w₁ = concatFn w₂
i : Fin r
⊢ Eq.{u_1 + 1} (α := Fin r → List α) (fun (i : Fin r) ↦ (↑(w₁ i) : List α)) fun (i : Fin r) ↦ (↑(w₂ i) : List α)

Tactic:
have := List.ofFn_injective (h _ _ (by simp) (by simp) hflat)
-- Module: Mathlib.InformationTheory.Coding.KraftMcMillan
Goal:
α : Type u_1
S : Finset (List α)
h : UniquelyDecodable (↑S : Set (List α))
r : ℕ
w₁ w₂ : Fin r → ↥S
hflat : concatFn w₁ = concatFn w₂
i : Fin r
this : Eq.{u_1 + 1} (α := Fin r → List α) (fun (i : Fin r) ↦ (↑(w₁ i) : List α)) fun (i : Fin r) ↦ (↑(w₂ i) : List α)
⊢ w₁ i = w₂ i

Tactic:
Subtype.ext (congrArg (fun f => f i) this)

Premises used: Subtype.ext
-- Module: Mathlib.InformationTheory.Coding.KraftMcMillan
Goal:
α : Type u_1
S : Finset (List α)
h : UniquelyDecodable (↑S : Set (List α))
r : ℕ
w₁ w₂ : Fin r → ↥S
hflat : concatFn w₁ = concatFn w₂
i : Fin r
this : Eq.{u_1 + 1} (α := Fin r → List α) (fun (i : Fin r) ↦ (↑(w₁ i) : List α)) fun (i : Fin r) ↦ (↑(w₂ i) : List α)
⊢ w₁ i = w₂ i

Tactic:
exact Subtype.ext (congrArg (fun f => f i) this)

Premises used: Subtype.ext
-- Module: Mathlib.InformationTheory.Coding.KraftMcMillan
Goal:
α : Type u_1
inst : Fintype α
inst_1 : Nonempty α
T : Finset (List α)
s : ℕ
x : List α
hx : x ∈ {x ∈ T | x.length = s}
⊢ HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ x.length = HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ s

Tactic:
simp [Finset.mem_filter.mp hx]

Premises used: Iff.mp, Finset.mem_filter
-- Module: Mathlib.InformationTheory.Coding.KraftMcMillan
Goal:
α : Type u_1
inst : Fintype α
inst_1 : Nonempty α
T : Finset (List α)
s : ℕ
⊢ ∑ x ∈ T with x.length = s, HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ s =
    (↑{x ∈ T | x.length = s}.card : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ s

Tactic:
simp only [Finset.sum_const, nsmul_eq_mul]

Premises used: nsmul_eq_mul, Finset.sum_const
-- Module: Mathlib.InformationTheory.Coding.KraftMcMillan
Goal:
α : Type u_1
inst : Fintype α
inst_1 : Nonempty α
T : Finset (List α)
s : ℕ
calc :
  (↑{x ∈ T | x.length = s}.card : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ s ≤
    HPow.hPow (α := ℝ) (↑(Fintype.card α) : ℝ) s * HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ s
⊢ ∑ x ∈ T with x.length = s, HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ x.length ≤
    HPow.hPow (α := ℝ) (↑(Fintype.card α) : ℝ) s * HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ s

Tactic:
calc
    _ = ∑ x ∈ T.filter (fun x => x.length = s), (1 / (Fintype.card α : ℝ)) ^ s :=
      Finset.sum_congr rfl fun x hx ↦ by simp [Finset.mem_filter.mp hx]
    _ = (T.filter fun x => x.length = s).card * (1 / Fintype.card α) ^ s := by
      simp only [Finset.sum_const, nsmul_eq_mul]

Premises used: Fintype.card, HDiv.hDiv, Nat.cast, Finset.card, OfNat.ofNat, Finset.filter, Eq, Finset.sum_congr, rfl
-- Module: Mathlib.InformationTheory.Coding.KraftMcMillan
Goal:
α : Type u_1
inst : Fintype α
inst_1 : Nonempty α
T : Finset (List α)
s : ℕ
calc : (↑{x ∈ T | x.length = s}.card : ℝ) ≤ HPow.hPow (α := ℝ) (↑(Fintype.card α) : ℝ) s
⊢ (↑{x ∈ T | x.length = s}.card : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ s ≤
    HPow.hPow (α := ℝ) (↑(Fintype.card α) : ℝ) s * HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ s

Tactic:
gcongr
-- Module: Mathlib.InformationTheory.Coding.KraftMcMillan
Goal:
α : Type u_1
inst : Fintype α
inst_1 : Nonempty α
T : Finset (List α)
s : ℕ
⊢ (↑{x ∈ T | x.length = s}.card : ℝ) ≤ HPow.hPow (α := ℝ) (↑(Fintype.card α) : ℝ) s

Tactic:
exact_mod_cast Finset.card_filter_length_eq_le

Premises used: Finset.card_filter_length_eq_le
-- Module: Mathlib.InformationTheory.Coding.KraftMcMillan
Goal:
α : Type u_1
S : Finset (List α)
r : ℕ
w : Fin r → ↥S
h0 : ∀ (c : ↥S), (↑c : List α) ≠ []
rw : r ≤ ∑ i : Fin r, (↑(w i) : List α).length ∧ ∑ i : Fin r, (↑(w i) : List α).length ≤ r * S.sup List.length
⊢ (concatFn w).length ∈ Finset.Icc r (r * S.sup List.length)

Tactic:
rw [concatFn_length, Finset.mem_Icc]

Premises used: _private.0.InformationTheory.concatFn_length, Finset.mem_Icc
-- Module: Mathlib.InformationTheory.Coding.KraftMcMillan
Goal:
α : Type u_1
S : Finset (List α)
r : ℕ
w : Fin r → ↥S
h0 : ∀ (c : ↥S), (↑c : List α) ≠ []
left : r ≤ ∑ i : Fin r, (↑(w i) : List α).length
right : ∑ i : Fin r, (↑(w i) : List α).length ≤ r * S.sup List.length
⊢ r ≤ ∑ i : Fin r, (↑(w i) : List α).length ∧ ∑ i : Fin r, (↑(w i) : List α).length ≤ r * S.sup List.length

Tactic:
constructor
-- Module: Mathlib.InformationTheory.Coding.KraftMcMillan
Goal:
α : Type u_1
S : Finset (List α)
r : ℕ
w : Fin r → ↥S
h0 : ∀ (c : ↥S), (↑c : List α) ≠ []
i : Fin r
h : Membership.mem (γ := Finset (Fin r)) Finset.univ i
⊢ 1 ≤ (↑(w i) : List α).length

Tactic:
grind
-- Module: Mathlib.InformationTheory.Coding.KraftMcMillan
Goal:
α : Type u_1
S : Finset (List α)
r : ℕ
w : Fin r → ↥S
h0 : ∀ (c : ↥S), (↑c : List α) ≠ []
⊢ LE.le (α := ℕ) (∑ x : Fin r, 1) (∑ i : Fin r, (↑(w i) : List α).length)

Tactic:
have : ∑ _, 1 ≤ ∑ i, (w i).val.length :=
      Finset.sum_le_sum (fun i _ => by grind)
-- Module: Mathlib.InformationTheory.Coding.KraftMcMillan
Goal:
α : Type u_1
S : Finset (List α)
r : ℕ
w : Fin r → ↥S
h0 : ∀ (c : ↥S), (↑c : List α) ≠ []
this : LE.le (α := ℕ) (∑ x : Fin r, 1) (∑ i : Fin r, (↑(w i) : List α).length)
⊢ r ≤ ∑ i : Fin r, (↑(w i) : List α).length

Tactic:
simpa using this
-- Module: Mathlib.InformationTheory.Coding.KraftMcMillan
Goal:
α : Type u_1
S : Finset (List α)
r : ℕ
w : Fin r → ↥S
h0 : ∀ (c : ↥S), (↑c : List α) ≠ []
⊢ ∑ i : Fin r, S.sup List.length = r * S.sup List.length

Tactic:
simp
-- Module: Mathlib.InformationTheory.Coding.KraftMcMillan
Goal:
α : Type u_1
S : Finset (List α)
r : ℕ
w : Fin r → ↥S
h0 : ∀ (c : ↥S), (↑c : List α) ≠ []
⊢ ∑ i : Fin r, (↑(w i) : List α).length ≤ r * S.sup List.length

Tactic:
exact (Finset.sum_le_sum (fun i _ => Finset.le_sup (w i).prop)).trans_eq (by simp)

Premises used: LE.le.trans_eq, Subtype.prop, Finset.sum_le_sum, Finset.le_sup
-- 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
set :
  let maxLen := S.sup List.length;
  HPow.hPow (α := ℝ) (∑ w ∈ S, HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ w.length) r ≤
    HMul.hMul (α := ℝ) (↑r : ℝ) (↑maxLen : ℝ)
⊢ HPow.hPow (α := ℝ) (∑ w ∈ S, HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ w.length) r ≤
    HMul.hMul (α := ℝ) (↑r : ℝ) (↑(S.sup List.length) : ℝ)

Tactic:
set maxLen := S.sup List.length

Premises used: Finset.sup, List.length
-- 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
maxLen : ℕ := S.sup List.length
T : Finset (List α) := Finset.image (α := Fin r → ↥S) concatFn Finset.univ
x : List α
hx : x ∈ T
rcases :
  ∀ (w : Fin r → ↥S),
    Membership.mem (γ := Finset (Fin r → ↥S)) Finset.univ w →
      ∀ (hx : concatFn w ∈ T), (concatFn w).length ∈ Finset.Icc r (r * maxLen)
⊢ x.length ∈ Finset.Icc r (r * maxLen)

Tactic:
rcases Finset.mem_image.mp hx with ⟨_, _, rfl⟩

Premises used: Finset.mem_image, Iff.mp, rfl
-- 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
maxLen : ℕ := S.sup List.length
T : Finset (List α) := Finset.image (α := Fin r → ↥S) concatFn Finset.univ
w : Fin r → ↥S
left : Membership.mem (γ := Finset (Fin r → ↥S)) Finset.univ w
hx : concatFn w ∈ T
c : ↥S
hnil : (↑c : List α) = []
⊢ [] ∈ (↑S : Set (List α))

Tactic:
simpa [hnil] using c.prop

Premises used: Subtype.prop
-- 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
maxLen : ℕ := S.sup List.length
T : Finset (List α) := Finset.image (α := Fin r → ↥S) concatFn Finset.univ
w : Fin r → ↥S
left : Membership.mem (γ := Finset (Fin r → ↥S)) Finset.univ w
hx : concatFn w ∈ T
⊢ (concatFn w).length ∈ Finset.Icc r (r * maxLen)

Tactic:
exact concatFn_length_mem_Icc
      (fun c hnil => h.epsilon_not_mem (by simpa [hnil] using c.prop))

Premises used: InformationTheory.UniquelyDecodable.epsilon_not_mem, _private.0.InformationTheory.concatFn_length_mem_Icc
-- 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
maxLen : ℕ := S.sup List.length
T : Finset (List α) := Finset.image (α := Fin r → ↥S) concatFn Finset.univ
⊢ ∀ (x : List α) (hx : x ∈ T), x.length ∈ Finset.Icc r (r * maxLen)

Tactic:
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))
-- 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
maxLen : ℕ := S.sup List.length
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)
D : ℝ := (↑(Fintype.card α) : ℝ)
⊢ HPow.hPow (α := ℝ) (∑ w ∈ S, HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ w.length) r =
    ∑ w : Fin r → ↥S, ∏ i : Fin r, (1 / D) ^ (↑(w i) : List α).length

Tactic:
simpa [(Finset.sum_coe_sort S _).symm] using
        Fintype.sum_pow (f := fun c : S => (1 / D) ^ c.val.length) r

Premises used: Fintype.sum_pow, HDiv.hDiv, HPow.hPow, OfNat.ofNat, Eq.symm, Subtype.val, List.length, Finset.sum_coe_sort
-- 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
maxLen : ℕ := S.sup List.length
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)
D : ℝ := (↑(Fintype.card α) : ℝ)
h₁ : ∀ (a : Fin r → ↥S), ∏ i : Fin r, (1 / D) ^ (↑(a i) : List α).length = (1 / D) ^ (concatFn a).length
⊢ Eq (α := ℝ) (∑ w : Fin r → ↥S, ∏ i : Fin r, (1 / D) ^ (↑(w i) : List α).length)
    (∑ w : Fin r → ↥S, (1 / D) ^ (concatFn w).length)

Tactic:
apply Fintype.sum_congr

Premises used: Fintype.sum_congr
-- 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
maxLen : ℕ := S.sup List.length
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)
D : ℝ := (↑(Fintype.card α) : ℝ)
w : Fin r → ↥S
⊢ ∏ i : Fin r, (1 / D) ^ (↑(w i) : List α).length = (1 / D) ^ (concatFn w).length

Tactic:
simpa [concatFn_length] using Finset.prod_pow_eq_pow_sum Finset.univ _ _

Premises used: _private.0.InformationTheory.concatFn_length, Finset.univ, Finset.prod_pow_eq_pow_sum
-- 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
maxLen : ℕ := S.sup List.length
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)
D : ℝ := (↑(Fintype.card α) : ℝ)
⊢ Eq (α := ℝ) (∑ w : Fin r → ↥S, (1 / D) ^ (concatFn w).length) (∑ x ∈ T, (1 / D) ^ x.length)

Tactic:
(Finset.sum_image (f := fun x => (1 / D) ^ x.length)
        (fun _ _ _ _ hEq => concatFn_injective_of_uniquelyDecodable h r hEq)).symm

Premises used: Finset.sum_image, Eq.symm, _private.0.InformationTheory.concatFn_injective_of_uniquelyDecodable
-- 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
maxLen : ℕ := S.sup List.length
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)
D : ℝ := (↑(Fintype.card α) : ℝ)
⊢ Eq (α := ℝ) (∑ x ∈ T, (1 / D) ^ x.length)
    (∑ s ∈ Finset.Icc r (r * maxLen), ∑ x ∈ T with x.length = s, (1 / D) ^ x.length)

Tactic:
(Finset.sum_fiberwise_of_maps_to hlen_maps _).symm

Premises used: Finset.sum_fiberwise_of_maps_to, Eq.symm
-- 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
maxLen : ℕ := S.sup List.length
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)
D : ℝ := (↑(Fintype.card α) : ℝ)
calc :
  ∑ s ∈ Finset.Icc r (r * maxLen), ∑ x ∈ T with x.length = s, (1 / D) ^ x.length ≤
    HMul.hMul (α := ℝ) (↑r : ℝ) (↑maxLen : ℝ)
⊢ HPow.hPow (α := ℝ) (∑ w ∈ S, HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ w.length) r ≤
    HMul.hMul (α := ℝ) (↑r : ℝ) (↑maxLen : ℝ)

Tactic:
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

Premises used: HMul.hMul, Finset.sum_fiberwise_of_maps_to, Fintype.card, HDiv.hDiv, Finset.Icc, Nat.cast, HPow.hPow, Finset.sum_image, OfNat.ofNat, Eq.symm, Fin, List.length, Finset.sum, _private.0.InformationTheory.concatFn_injective_of_uniquelyDecodable
-- 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
maxLen : ℕ := S.sup List.length
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)
D : ℝ := (↑(Fintype.card α) : ℝ)
calc :
  ∑ i ∈ Finset.Icc r (r * maxLen),
      HPow.hPow (α := ℝ) (↑(Fintype.card α) : ℝ) i * HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ i ≤
    HMul.hMul (α := ℝ) (↑r : ℝ) (↑maxLen : ℝ)
⊢ ∑ s ∈ Finset.Icc r (r * maxLen), ∑ x ∈ T with x.length = s, (1 / D) ^ x.length ≤
    HMul.hMul (α := ℝ) (↑r : ℝ) (↑maxLen : ℝ)

Tactic:
apply le_trans (Finset.sum_le_sum (fun _ _ => sum_pow_length_filter_eq_le_card_mul))

Premises used: Finset.sum_le_sum, _private.0.InformationTheory.sum_pow_length_filter_eq_le_card_mul, le_trans
-- 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
maxLen : ℕ := S.sup List.length
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)
D : ℝ := (↑(Fintype.card α) : ℝ)
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 * maxLen)),
      ∑ i ∈ Finset.Icc 0 (0 * maxLen),
          HPow.hPow (α := ℝ) (↑(Fintype.card α) : ℝ) i * HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ i ≤
        HMul.hMul (α := ℝ) (↑0 : ℝ) (↑maxLen : ℝ)
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 * 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 : ℝ)
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) * 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 : ℝ)
⊢ ∑ i ∈ Finset.Icc r (r * maxLen),
      HPow.hPow (α := ℝ) (↑(Fintype.card α) : ℝ) i * HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ i ≤
    HMul.hMul (α := ℝ) (↑r : ℝ) (↑maxLen : ℝ)

Tactic:
rcases r with (_ | _ | r)