awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Basic (goal)
Goal:
G : Type u
inst : Group G
N : Subgroup G
nN : N.Normal
H : Type v
inst_1 : Group H
M_1 : Type x
inst_2 : Monoid M_1
φ : G →* H
M : Subgroup G
nM : M.Normal
h : N ≤ M
⊢ Eq (α := G ⧸ M →* G ⧸ M)
    (MonoidHom.comp (N := HasQuotient.Quotient (G ⧸ N) (B := Subgroup (G ⧸ N)) (Subgroup.map (mk' N) M))
      (quotientQuotientEquivQuotientAux N M h) (map M (Subgroup.map (mk' N) M) (mk' N) ⋯))
    (MonoidHom.id (G ⧸ M))
have h₁ : ∀ (x : G),
  Eq (α := G ⧸ M)
    ((MonoidHom.comp
            (MonoidHom.comp (N := HasQuotient.Quotient (G ⧸ N) (B := Subgroup (G ⧸ N)) (Subgroup.map (mk' N) M))
              (quotientQuotientEquivQuotientAux N M h) (map M (Subgroup.map (mk' N) M) (mk' N) sorry))
            (mk' M) :
          (a : G) → G ⧸ M)
        x :
      G ⧸ M)
    ((MonoidHom.comp (MonoidHom.id (G ⧸ M)) (mk' M) : (a : G) → G ⧸ M) x : G ⧸ M)
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Basic (hypothesis)
Goal:
G : Type u
inst : Group G
H : Subgroup G
h : Subsingleton.{u + 1} (G ⧸ H)
x : G
h_1 : Membership.mem (γ := Subgroup G) ⊤ x
⊢ x ∈ H
have this : 1⁻¹ * x ∈ H
Tactic: have this : 1⁻¹ * x ∈ H := QuotientGroup.eq.1 (Subsingleton.elim _ _)
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Basic (goal)
Goal:
G : Type u
inst : Group G
H : Subgroup G
h : Subsingleton.{u + 1} (G ⧸ H)
x : G
h_1 : Membership.mem (γ := Subgroup G) ⊤ x
this : 1⁻¹ * x ∈ H
⊢ x ∈ H
have rwa : ∀ (this : 1 * x ∈ H), x ∈ H
Tactic: rwa [inv_one, one_mul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Basic (goal)
Goal:
G : Type u
inst : Group G
H : Subgroup G
h : Subsingleton.{u + 1} (G ⧸ H)
x : G
h_1 : Membership.mem (γ := Subgroup G) ⊤ x
this : 1⁻¹ * x ∈ H
rwa : ∀ (this : 1 * x ∈ H), x ∈ H
⊢ x ∈ H
have rwa₁ : ∀ (this : x ∈ H), x ∈ H
Tactic: rwa [inv_one, one_mul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Basic (goal)
Goal:
G : Type u
inst : Group G
H₁ : Subgroup G
inst_1 : H₁.Normal
H₂ : Subgroup (G ⧸ H₁)
inst_2 : H₂.Normal
⊢ Subgroup.comap (mk' H₁) (Subgroup.comap (mk' H₂) (Subgroup.center ((G ⧸ H₁) ⧸ H₂))) =
    Subgroup.comap (mk' (Subgroup.comap (mk' H₁) H₂)) (Subgroup.center (G ⧸ Subgroup.comap (mk' H₁) H₂))
have h : ∀ (x : G),
  x ∈ Subgroup.comap (mk' H₁) (Subgroup.comap (mk' H₂) (Subgroup.center ((G ⧸ H₁) ⧸ H₂))) ↔
    x ∈ Subgroup.comap (mk' (Subgroup.comap (mk' H₁) H₂)) (Subgroup.center (G ⧸ Subgroup.comap (mk' H₁) H₂))
Tactic: ext x
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Basic (goal)
Goal:
G : Type u
inst : Group G
N : Subgroup G
nN : N.Normal
H_1 : Type v
inst_1 : Group H_1
M : Type x
inst_2 : Monoid M
φ : G →* H_1
A : Type u_1
inst_3 : CommGroup A
H : Subgroup G
inst_4 : H.Normal
x : MonoidHom.{u, u_1} (G ⧸ H) A
⊢ (fun (x : ↥(ker (M := MonoidHom.{u, u_1} (↥H) A) (restrictHom H A))) ↦
        (match (motive := ↥(ker (M := MonoidHom.{u, u_1} (↥H) A) (restrictHom H A)) → MonoidHom.{u, u_1} (G ⧸ H) A)
            x with
          | ⟨f, hf⟩ => lift H f ⋯ :
          MonoidHom.{u, u_1} (G ⧸ H) A))
      ((fun (f : MonoidHom.{u, u_1} (G ⧸ H) A) ↦
          (Subtype.mk (p := fun (x : G →* A) ↦
              Membership.mem (γ := Subgroup (G →* A)) (ker (M := MonoidHom.{u, u_1} (↥H) A) (restrictHom H A)) x)
              (f.comp (mk' H)) ⋯ :
            ↥(ker (M := MonoidHom.{u, u_1} (↥H) A) (restrictHom H A))))
        x) =
    x
have h : ∀ (x_1 : G),
  Eq.{u_1 + 1} (α := A)
    ((MonoidHom.comp
            ((fun (x : ↥(ker (M := MonoidHom.{u, u_1} (↥H) A) (restrictHom H A))) ↦
                (match (motive :=
                    ↥(ker (M := MonoidHom.{u, u_1} (↥H) A) (restrictHom H A)) → MonoidHom.{u, u_1} (G ⧸ H) A) x with
                  | ⟨f, hf⟩ => lift H f sorry :
                  MonoidHom.{u, u_1} (G ⧸ H) A))
              ((fun (f : MonoidHom.{u, u_1} (G ⧸ H) A) ↦
                  (Subtype.mk (p := fun (x : G →* A) ↦
                      Membership.mem (γ := Subgroup (G →* A)) (ker (M := MonoidHom.{u, u_1} (↥H) A) (restrictHom H A))
                        x)
                      (f.comp (mk' H)) sorry :
                    ↥(ker (M := MonoidHom.{u, u_1} (↥H) A) (restrictHom H A))))
                x))
            (mk' H) :
          (a : G) → A)
        x_1 :
      A)
    ((x.comp (mk' H) : (a : G) → A) x_1 : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Basic (goal)
Goal:
G : Type u
inst : Group G
N : Subgroup G
nN : N.Normal
H_1 : Type v
inst_1 : Group H_1
M : Type x
inst_2 : Monoid M
φ : G →* H_1
A : Type u_1
inst_3 : CommGroup A
H : Subgroup G
inst_4 : H.Normal
x x_1 : ↥(ker (M := MonoidHom.{u, u_1} (↥H) A) (restrictHom H A))
⊢ (match (motive := ↥(ker (M := MonoidHom.{u, u_1} (↥H) A) (restrictHom H A)) → MonoidHom.{u, u_1} (G ⧸ H) A)
      x * x_1 with
    | ⟨f, hf⟩ => lift H f ⋯) =
    HMul.hMul (α := MonoidHom.{u, u_1} (G ⧸ H) A) (β := MonoidHom.{u, u_1} (G ⧸ H) A)
      (match (motive := ↥(ker (M := MonoidHom.{u, u_1} (↥H) A) (restrictHom H A)) → MonoidHom.{u, u_1} (G ⧸ H) A) x with
        | ⟨f, hf⟩ => lift H f ⋯ :
        MonoidHom.{u, u_1} (G ⧸ H) A)
      (match (motive := ↥(ker (M := MonoidHom.{u, u_1} (↥H) A) (restrictHom H A)) → MonoidHom.{u, u_1} (G ⧸ H) A)
          x_1 with
        | ⟨f, hf⟩ => lift H f ⋯ :
        MonoidHom.{u, u_1} (G ⧸ H) A)
have h : ∀ (x_2 : G),
  Eq.{u_1 + 1} (α := A)
    ((MonoidHom.comp
            (match (motive := ↥(ker (M := MonoidHom.{u, u_1} (↥H) A) (restrictHom H A)) → MonoidHom.{u, u_1} (G ⧸ H) A)
              x * x_1 with
            | ⟨f, hf⟩ => lift H f sorry)
            (mk' H) :
          (a : G) → A)
        x_2 :
      A)
    (((HMul.hMul (α := MonoidHom.{u, u_1} (G ⧸ H) A) (β := MonoidHom.{u, u_1} (G ⧸ H) A)
                (match (motive :=
                    ↥(ker (M := MonoidHom.{u, u_1} (↥H) A) (restrictHom H A)) → MonoidHom.{u, u_1} (G ⧸ H) A) x with
                  | ⟨f, hf⟩ => lift H f sorry :
                  MonoidHom.{u, u_1} (G ⧸ H) A)
                (match (motive :=
                    ↥(ker (M := MonoidHom.{u, u_1} (↥H) A) (restrictHom H A)) → MonoidHom.{u, u_1} (G ⧸ H) A) x_1 with
                  | ⟨f, hf⟩ => lift H f sorry :
                  MonoidHom.{u, u_1} (G ⧸ H) A)).comp
            (mk' H) :
          (a : G) → A)
        x_2 :
      A)
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Basic (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
N : AddSubgroup R
inst_1 : N.Normal
n : ℕ
a : R
⊢ (↑((↑n : R) * a) : R ⧸ N) = HSMul.hSMul (β := R ⧸ N) n (↑a : R ⧸ N)
have rw : (↑(n • a) : R ⧸ N) = HSMul.hSMul (β := R ⧸ N) n (↑a : R ⧸ N)
Tactic: rw [← nsmul_eq_mul, mk_nsmul N a n]
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Basic (goal)
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)
⊢ (↑((↑n : R) * a) : R ⧸ N) = HSMul.hSMul (β := R ⧸ N) n (↑a : R ⧸ N)
have rw₁ : HSMul.hSMul (β := R ⧸ N) n (↑a : R ⧸ N) = HSMul.hSMul (β := R ⧸ N) n (↑a : R ⧸ N)
Tactic: rw [← nsmul_eq_mul, mk_nsmul N a n]
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Basic (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
N : AddSubgroup R
inst_1 : N.Normal
n : ℤ
a : R
⊢ (↑((↑n : R) * a) : R ⧸ N) = HSMul.hSMul (β := R ⧸ N) n (↑a : R ⧸ N)
have rw : (↑(n • a) : R ⧸ N) = HSMul.hSMul (β := R ⧸ N) n (↑a : R ⧸ N)
Tactic: rw [← zsmul_eq_mul, mk_zsmul N a n]
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Basic (goal)
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)
⊢ (↑((↑n : R) * a) : R ⧸ N) = HSMul.hSMul (β := R ⧸ N) n (↑a : R ⧸ N)
have rw₁ : HSMul.hSMul (β := R ⧸ N) n (↑a : R ⧸ N) = HSMul.hSMul (β := R ⧸ N) n (↑a : R ⧸ N)
Tactic: rw [← zsmul_eq_mul, mk_zsmul N a n]
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Basic (goal)
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' := ⋯ }
⊢ Eq (α := Subgroup ((i : ι) → A i)) (MonoidHom.range (G := (i : ι) → A i) (powMonoidHom n)) φ.ker
have 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
Tactic: ext x : 1
-- Lean 4 proof step from Mathlib.InformationTheory.Coding.KraftMcMillan (goal)
Goal:
α : Type u_1
S : Finset (List α)
h : UniquelyDecodable (↑S : Set (List α))
r : ℕ
w₁ w₂ : Fin r → ↥S
hflat : concatFn w₁ = concatFn w₂
⊢ w₁ = w₂
have h₁ : ∀ (i : Fin r), w₁ i = w₂ i
Tactic: funext i
-- Lean 4 proof step from Mathlib.InformationTheory.Coding.KraftMcMillan (hypothesis)
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₁ i = w₂ i
have this : 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)
-- Lean 4 proof step from Mathlib.InformationTheory.Coding.KraftMcMillan (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : Nonempty α
T : Finset (List α)
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
have calc : (↑{x ∈ T | x.length = s}.card : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ s ≤
  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]
-- Lean 4 proof step from Mathlib.InformationTheory.Coding.KraftMcMillan (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : Nonempty α
T : Finset (List α)
s : ℕ
⊢ (↑{x ∈ T | x.length = s}.card : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ s ≤
    HPow.hPow (α := ℝ) (↑(Fintype.card α) : ℝ) s * HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ s
have calc : (↑{x ∈ T | x.length = s}.card : ℝ) ≤ HPow.hPow (α := ℝ) (↑(Fintype.card α) : ℝ) s
Tactic: gcongr
-- Lean 4 proof step from Mathlib.InformationTheory.Coding.KraftMcMillan (goal)
Goal:
α : Type u_1
S : Finset (List α)
r : ℕ
w : Fin r → ↥S
h0 : ∀ (c : ↥S), (↑c : List α) ≠ []
⊢ (concatFn w).length ∈ Finset.Icc r (r * S.sup List.length)
have rw : r ≤ ∑ i : Fin r, (↑(w i) : List α).length ∧ ∑ i : Fin r, (↑(w i) : List α).length ≤ r * S.sup List.length
Tactic: rw [concatFn_length, Finset.mem_Icc]
-- Lean 4 proof step from Mathlib.InformationTheory.Coding.KraftMcMillan (goal)
Goal:
α : Type u_1
S : Finset (List α)
r : ℕ
w : Fin r → ↥S
h0 : ∀ (c : ↥S), (↑c : List α) ≠ []
⊢ r ≤ ∑ i : Fin r, (↑(w i) : List α).length ∧ ∑ i : Fin r, (↑(w i) : List α).length ≤ r * S.sup List.length
have left : r ≤ ∑ i : Fin r, (↑(w i) : List α).length
Tactic: constructor
-- Lean 4 proof step from Mathlib.InformationTheory.Coding.KraftMcMillan (goal)
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
⊢ r ≤ ∑ i : Fin r, (↑(w i) : List α).length ∧ ∑ i : Fin r, (↑(w i) : List α).length ≤ r * S.sup List.length
have right : ∑ i : Fin r, (↑(w i) : List α).length ≤ r * S.sup List.length
Tactic: constructor
-- Lean 4 proof step from Mathlib.InformationTheory.Coding.KraftMcMillan (hypothesis)
Goal:
α : Type u_1
S : Finset (List α)
r : ℕ
w : Fin r → ↥S
h0 : ∀ (c : ↥S), (↑c : List α) ≠ []
⊢ r ≤ ∑ i : Fin r, (↑(w i) : List α).length
have this : 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)
-- 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 α))
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)
have 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)
Tactic: rcases Finset.mem_image.mp hx with ⟨_, _, rfl⟩
Cleared hypotheses: x, hx
-- 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 α))
r : ℕ
hr : r ≥ 1
maxLen : ℕ := S.sup List.length
T : Finset (List α) := Finset.image (α := Fin r → ↥S) concatFn Finset.univ
⊢ HPow.hPow (α := ℝ) (∑ w ∈ S, HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ w.length) r ≤
    HMul.hMul (α := ℝ) (↑r : ℝ) (↑maxLen : ℝ)
have hlen_maps : ∀ (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))
-- 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 α))
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, ∏ i : Fin r, (1 / D) ^ (↑(w i) : List α).length)
    (∑ w : Fin r → ↥S, (1 / D) ^ (concatFn w).length)
have h₁ : ∀ (a : Fin r → ↥S), ∏ i : Fin r, (1 / D) ^ (↑(a i) : List α).length = (1 / D) ^ (concatFn a).length
Tactic: apply Fintype.sum_congr
-- 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 α))
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 ≤
    HMul.hMul (α := ℝ) (↑r : ℝ) (↑maxLen : ℝ)
have calc : ∑ s ∈ Finset.Icc r (r * maxLen), ∑ x ∈ T with x.length = s, (1 / D) ^ x.length ≤
  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
-- 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 α))
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 α) : ℝ)
⊢ ∑ s ∈ Finset.Icc r (r * maxLen), ∑ x ∈ T with x.length = s, (1 / D) ^ x.length ≤
    HMul.hMul (α := ℝ) (↑r : ℝ) (↑maxLen : ℝ)
have calc : ∑ i ∈ Finset.Icc r (r * maxLen),
    HPow.hPow (α := ℝ) (↑(Fintype.card α) : ℝ) i * HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ i ≤
  HMul.hMul (α := ℝ) (↑r : ℝ) (↑maxLen : ℝ)
Tactic: apply le_trans (Finset.sum_le_sum (fun _ _ => sum_pow_length_filter_eq_le_card_mul))
-- 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 α))
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 α) : ℝ)
⊢ ∑ i ∈ Finset.Icc r (r * maxLen),
      HPow.hPow (α := ℝ) (↑(Fintype.card α) : ℝ) i * HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ i ≤
    HMul.hMul (α := ℝ) (↑r : ℝ) (↑maxLen : ℝ)
have 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 : ℝ)
Tactic: rcases r with (_ | _ | r)
Cleared hypotheses: r, hr, T, 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 α))
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 : ℝ)
⊢ ∑ i ∈ Finset.Icc r (r * maxLen),
      HPow.hPow (α := ℝ) (↑(Fintype.card α) : ℝ) i * HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ i ≤
    HMul.hMul (α := ℝ) (↑r : ℝ) (↑maxLen : ℝ)
have 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 : ℝ)
Tactic: rcases r with (_ | _ | r)
Cleared hypotheses: r, hr, T, 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 α))
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 : ℝ)
⊢ ∑ i ∈ Finset.Icc r (r * maxLen),
      HPow.hPow (α := ℝ) (↑(Fintype.card α) : ℝ) i * HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ i ≤
    HMul.hMul (α := ℝ) (↑r : ℝ) (↑maxLen : ℝ)
have 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 : ℝ)
Tactic: rcases r with (_ | _ | r)
Cleared hypotheses: r, hr, T, 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 : 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)
⊢ ∑ i ∈ Finset.Icc 0 (0 * maxLen),
      HPow.hPow (α := ℝ) (↑(Fintype.card α) : ℝ) i * HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ i ≤
    HMul.hMul (α := ℝ) (↑0 : ℝ) (↑maxLen : ℝ)
have 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 : ℝ)
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 : 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 : ℝ)
⊢ ∑ i ∈ Finset.Icc 0 (0 * maxLen),
      HPow.hPow (α := ℝ) (↑(Fintype.card α) : ℝ) i * HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ i ≤
    HMul.hMul (α := ℝ) (↑0 : ℝ) (↑maxLen : ℝ)
have 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) : ℝ)
Tactic: rcases maxLen with (_ | _ | maxLen)
Cleared hypotheses: maxLen, hlen_maps