awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.PluenneckeRuzsa (goal)
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : CommGroup G
A : Finset G
hA : A.Nonempty
B : Finset G
m n : ℕ
hA' : A ∈ A.powerset.erase ∅
C : Finset G
hCmin :
  ∀ x' ∈ A.powerset.erase ∅,
    HDiv.hDiv (α := ℚ≥0) (↑(#(C * B)) : ℚ≥0) (↑(#C) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(x' * B)) : ℚ≥0) (↑(#x') : ℚ≥0)
hC : C.Nonempty
hCA : C ⊆ A
m₁ :
  HMul.hMul (α := ℚ≥0) (↑(#(B ^ m * C)) : ℚ≥0) (↑(#(B ^ n * C)) : ℚ≥0) =
    HMul.hMul (α := ℚ≥0) (↑(#(C * B ^ m)) : ℚ≥0) (↑(#(C * B ^ n)) : ℚ≥0)
⊢ HMul.hMul (α := ℚ≥0) (↑(#(B ^ m / B ^ n)) : ℚ≥0) (↑(#C) : ℚ≥0) ≤
    HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0) ^ (m + n) * (↑(#A) : ℚ≥0) * (↑(#C) : ℚ≥0)
have m₂ : HMul.hMul (α := ℚ≥0) (↑(#(C * B ^ m)) : ℚ≥0) (↑(#(C * B ^ n)) : ℚ≥0) ≤
  HDiv.hDiv (α := ℚ≥0) (↑(#(C * B)) : ℚ≥0) (↑(#C) : ℚ≥0) ^ m * (↑(#C) : ℚ≥0) *
    (HDiv.hDiv (α := ℚ≥0) (↑(#(C * B)) : ℚ≥0) (↑(#C) : ℚ≥0) ^ n * (↑(#C) : ℚ≥0))
Tactic: calc
    (#(B ^ m / B ^ n) * #C : ℚ≥0)
      ≤ #(B ^ m * C) * #(B ^ n * C) := mod_cast ruzsa_triangle_inequality_div_mul_mul ..
    _ = #(C * B ^ m) * #(C * B ^ n) := by simp_rw [mul_comm]
    _ ≤ ((#(C * B) / #C) ^ m * #C) * ((#(C * B) / #C : ℚ≥0) ^ n * #C) := by
      gcongr <;> exact card_mul_pow_le (mul_aux hC hCA hCmin) _
    _ = (#(C * B) / #C) ^ (m + n) * #C * #C := by ring
    _ ≤ (#(A * B) / #A) ^ (m + n) * #A * #C := by gcongr (?_ ^ _) * #?_ * _; exact hCmin _ hA'
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.PluenneckeRuzsa (goal)
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : CommGroup G
A : Finset G
hA : A.Nonempty
B : Finset G
m n : ℕ
hA' : A ∈ A.powerset.erase ∅
C : Finset G
hCmin :
  ∀ x' ∈ A.powerset.erase ∅,
    HDiv.hDiv (α := ℚ≥0) (↑(#(C * B)) : ℚ≥0) (↑(#C) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(x' * B)) : ℚ≥0) (↑(#x') : ℚ≥0)
hC : C.Nonempty
hCA : C ⊆ A
m₁ :
  HMul.hMul (α := ℚ≥0) (↑(#(B ^ m * C)) : ℚ≥0) (↑(#(B ^ n * C)) : ℚ≥0) =
    HMul.hMul (α := ℚ≥0) (↑(#(C * B ^ m)) : ℚ≥0) (↑(#(C * B ^ n)) : ℚ≥0)
m₂ :
  HMul.hMul (α := ℚ≥0) (↑(#(C * B ^ m)) : ℚ≥0) (↑(#(C * B ^ n)) : ℚ≥0) ≤
    HDiv.hDiv (α := ℚ≥0) (↑(#(C * B)) : ℚ≥0) (↑(#C) : ℚ≥0) ^ m * (↑(#C) : ℚ≥0) *
      (HDiv.hDiv (α := ℚ≥0) (↑(#(C * B)) : ℚ≥0) (↑(#C) : ℚ≥0) ^ n * (↑(#C) : ℚ≥0))
⊢ HMul.hMul (α := ℚ≥0) (↑(#(B ^ m / B ^ n)) : ℚ≥0) (↑(#C) : ℚ≥0) ≤
    HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0) ^ (m + n) * (↑(#A) : ℚ≥0) * (↑(#C) : ℚ≥0)
have m₃ : HDiv.hDiv (α := ℚ≥0) (↑(#(C * B)) : ℚ≥0) (↑(#C) : ℚ≥0) ^ m * (↑(#C) : ℚ≥0) *
    (HDiv.hDiv (α := ℚ≥0) (↑(#(C * B)) : ℚ≥0) (↑(#C) : ℚ≥0) ^ n * (↑(#C) : ℚ≥0)) =
  HDiv.hDiv (α := ℚ≥0) (↑(#(C * B)) : ℚ≥0) (↑(#C) : ℚ≥0) ^ (m + n) * (↑(#C) : ℚ≥0) * (↑(#C) : ℚ≥0)
Tactic: calc
    (#(B ^ m / B ^ n) * #C : ℚ≥0)
      ≤ #(B ^ m * C) * #(B ^ n * C) := mod_cast ruzsa_triangle_inequality_div_mul_mul ..
    _ = #(C * B ^ m) * #(C * B ^ n) := by simp_rw [mul_comm]
    _ ≤ ((#(C * B) / #C) ^ m * #C) * ((#(C * B) / #C : ℚ≥0) ^ n * #C) := by
      gcongr <;> exact card_mul_pow_le (mul_aux hC hCA hCmin) _
    _ = (#(C * B) / #C) ^ (m + n) * #C * #C := by ring
    _ ≤ (#(A * B) / #A) ^ (m + n) * #A * #C := by gcongr (?_ ^ _) * #?_ * _; exact hCmin _ hA'
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.PluenneckeRuzsa (goal)
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : CommGroup G
A : Finset G
hA : A.Nonempty
B : Finset G
m n : ℕ
hA' : A ∈ A.powerset.erase ∅
C : Finset G
hCmin :
  ∀ x' ∈ A.powerset.erase ∅,
    HDiv.hDiv (α := ℚ≥0) (↑(#(C * B)) : ℚ≥0) (↑(#C) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(x' * B)) : ℚ≥0) (↑(#x') : ℚ≥0)
hC : C.Nonempty
hCA : C ⊆ A
m₁ :
  HMul.hMul (α := ℚ≥0) (↑(#(B ^ m * C)) : ℚ≥0) (↑(#(B ^ n * C)) : ℚ≥0) =
    HMul.hMul (α := ℚ≥0) (↑(#(C * B ^ m)) : ℚ≥0) (↑(#(C * B ^ n)) : ℚ≥0)
m₂ :
  HMul.hMul (α := ℚ≥0) (↑(#(C * B ^ m)) : ℚ≥0) (↑(#(C * B ^ n)) : ℚ≥0) ≤
    HDiv.hDiv (α := ℚ≥0) (↑(#(C * B)) : ℚ≥0) (↑(#C) : ℚ≥0) ^ m * (↑(#C) : ℚ≥0) *
      (HDiv.hDiv (α := ℚ≥0) (↑(#(C * B)) : ℚ≥0) (↑(#C) : ℚ≥0) ^ n * (↑(#C) : ℚ≥0))
m₃ :
  HDiv.hDiv (α := ℚ≥0) (↑(#(C * B)) : ℚ≥0) (↑(#C) : ℚ≥0) ^ m * (↑(#C) : ℚ≥0) *
      (HDiv.hDiv (α := ℚ≥0) (↑(#(C * B)) : ℚ≥0) (↑(#C) : ℚ≥0) ^ n * (↑(#C) : ℚ≥0)) =
    HDiv.hDiv (α := ℚ≥0) (↑(#(C * B)) : ℚ≥0) (↑(#C) : ℚ≥0) ^ (m + n) * (↑(#C) : ℚ≥0) * (↑(#C) : ℚ≥0)
⊢ HMul.hMul (α := ℚ≥0) (↑(#(B ^ m / B ^ n)) : ℚ≥0) (↑(#C) : ℚ≥0) ≤
    HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0) ^ (m + n) * (↑(#A) : ℚ≥0) * (↑(#C) : ℚ≥0)
have m₄ : HDiv.hDiv (α := ℚ≥0) (↑(#(C * B)) : ℚ≥0) (↑(#C) : ℚ≥0) ^ (m + n) * (↑(#C) : ℚ≥0) * (↑(#C) : ℚ≥0) ≤
  HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0) ^ (m + n) * (↑(#A) : ℚ≥0) * (↑(#C) : ℚ≥0)
Tactic: calc
    (#(B ^ m / B ^ n) * #C : ℚ≥0)
      ≤ #(B ^ m * C) * #(B ^ n * C) := mod_cast ruzsa_triangle_inequality_div_mul_mul ..
    _ = #(C * B ^ m) * #(C * B ^ n) := by simp_rw [mul_comm]
    _ ≤ ((#(C * B) / #C) ^ m * #C) * ((#(C * B) / #C : ℚ≥0) ^ n * #C) := by
      gcongr <;> exact card_mul_pow_le (mul_aux hC hCA hCmin) _
    _ = (#(C * B) / #C) ^ (m + n) * #C * #C := by ring
    _ ≤ (#(A * B) / #A) ^ (m + n) * #A * #C := by gcongr (?_ ^ _) * #?_ * _; exact hCmin _ hA'
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.PluenneckeRuzsa (goal)
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : CommGroup G
A : Finset G
hA : A.Nonempty
B : Finset G
m n : ℕ
⊢ (↑(#(B ^ m / B ^ n)) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(A / B)) : ℚ≥0) (↑(#A) : ℚ≥0) ^ (m + n) * (↑(#A) : ℚ≥0)
have rw : (↑(#(B⁻¹ ^ m / B⁻¹ ^ n)) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(A * B⁻¹)) : ℚ≥0) (↑(#A) : ℚ≥0) ^ (m + n) * (↑(#A) : ℚ≥0)
Tactic: rw [← card_inv, inv_div', ← inv_pow, ← inv_pow, div_eq_mul_inv A]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Randomisation (goal)
Goal:
G : Type u_1
inst : Fintype G
inst_1 : AddCommGroup G
c : AddChar G ℂ → ℝ
d : AddChar G ℂ → ℂ
hcd : AddDissociated.{u_1} (α := AddChar G ℂ) {ψ : AddChar G ℂ | d ψ ≠ 0}
⊢ Eq (α := ℝ) (𝔼 a : G, ∏ ψ : AddChar G ℂ, (c ψ + (HMul.hMul (β := ℂ) (d ψ) ((ψ : (a : G) → ℂ) a : ℂ)).re))
    (∏ ψ : AddChar G ℂ, c ψ)
have refine : (↑(𝔼 a : G, ∏ ψ : AddChar G ℂ, (c ψ + (HMul.hMul (β := ℂ) (d ψ) ((ψ : (a : G) → ℂ) a : ℂ)).re)) : ℂ) =
  (↑(∏ ψ : AddChar G ℂ, c ψ) : ℂ)
Tactic: refine Complex.ofReal_injective ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Randomisation (goal)
Goal:
G : Type u_1
inst : Fintype G
inst_1 : AddCommGroup G
c : AddChar G ℂ → ℝ
d : AddChar G ℂ → ℂ
hcd : AddDissociated.{u_1} (α := AddChar G ℂ) {ψ : AddChar G ℂ | d ψ ≠ 0}
⊢ (↑(𝔼 a : G, ∏ ψ : AddChar G ℂ, (c ψ + (HMul.hMul (β := ℂ) (d ψ) ((ψ : (a : G) → ℂ) a : ℂ)).re)) : ℂ) =
    (↑(∏ ψ : AddChar G ℂ, c ψ) : ℂ)
have push_cast : Eq (α := ℂ)
  (𝔼 i : G, ∏ x : AddChar G ℂ, ((↑(c x) : ℂ) + (↑(HMul.hMul (β := ℂ) (d x) ((x : (a : G) → ℂ) i : ℂ)).re : ℂ)))
  (∏ i : AddChar G ℂ, (↑(c i) : ℂ))
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Randomisation (goal)
Goal:
G : Type u_1
inst : Fintype G
inst_1 : AddCommGroup G
c : AddChar G ℂ → ℝ
d : AddChar G ℂ → ℂ
hcd : AddDissociated.{u_1} (α := AddChar G ℂ) {ψ : AddChar G ℂ | d ψ ≠ 0}
⊢ Eq (α := ℂ)
    (𝔼 i : G, ∏ x : AddChar G ℂ, ((↑(c x) : ℂ) + (↑(HMul.hMul (β := ℂ) (d x) ((x : (a : G) → ℂ) i : ℂ)).re : ℂ)))
    (∑ t : Finset (AddChar G ℂ),
      HMul.hMul (α := ℂ)
        (𝔼 a : G,
          ∏ ψ ∈ t,
            HAdd.hAdd (β := ℂ) (HMul.hMul (β := ℂ) (d ψ) ((ψ : (a : G) → ℂ) a : ℂ))
                ((starRingEnd ℂ : (a : ℂ) → ℂ) (HMul.hMul (β := ℂ) (d ψ) ((ψ : (a : G) → ℂ) a : ℂ)) : ℂ) /
              2)
        (∏ ψ ∈ tᶜ, (↑(c ψ) : ℂ)))
have simp_rw : Eq (α := ℂ)
  (𝔼 i : G, ∏ x : AddChar G ℂ, ((↑(c x) : ℂ) + (↑(HMul.hMul (β := ℂ) (d x) ((x : (a : G) → ℂ) i : ℂ)).re : ℂ)))
  (∑ x : Finset (AddChar G ℂ),
    𝔼 i : G,
      HMul.hMul (α := ℂ)
        (∏ ψ ∈ x,
          HAdd.hAdd (β := ℂ) (HMul.hMul (β := ℂ) (d ψ) ((ψ : (a : G) → ℂ) i : ℂ))
              ((starRingEnd ℂ : (a : ℂ) → ℂ) (HMul.hMul (β := ℂ) (d ψ) ((ψ : (a : G) → ℂ) i : ℂ)) : ℂ) /
            2)
        (∏ ψ ∈ xᶜ, (↑(c ψ) : ℂ)))
Tactic: simp_rw [expect_mul, ← expect_sum_comm, ← Fintype.prod_add, add_comm,
          Complex.re_eq_add_conj]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Randomisation (goal)
Goal:
G : Type u_1
inst : Fintype G
inst_1 : AddCommGroup G
c : AddChar G ℂ → ℝ
d : AddChar G ℂ → ℂ
hcd : AddDissociated.{u_1} (α := AddChar G ℂ) {ψ : AddChar G ℂ | d ψ ≠ 0}
simp_rw :
  Eq (α := ℂ)
    (𝔼 i : G, ∏ x : AddChar G ℂ, ((↑(c x) : ℂ) + (↑(HMul.hMul (β := ℂ) (d x) ((x : (a : G) → ℂ) i : ℂ)).re : ℂ)))
    (∑ x : Finset (AddChar G ℂ),
      𝔼 i : G,
        HMul.hMul (α := ℂ)
          (∏ ψ ∈ x,
            HAdd.hAdd (β := ℂ) (HMul.hMul (β := ℂ) (d ψ) ((ψ : (a : G) → ℂ) i : ℂ))
                ((starRingEnd ℂ : (a : ℂ) → ℂ) (HMul.hMul (β := ℂ) (d ψ) ((ψ : (a : G) → ℂ) i : ℂ)) : ℂ) /
              2)
          (∏ ψ ∈ xᶜ, (↑(c ψ) : ℂ)))
⊢ Eq (α := ℂ)
    (𝔼 i : G, ∏ x : AddChar G ℂ, ((↑(c x) : ℂ) + (↑(HMul.hMul (β := ℂ) (d x) ((x : (a : G) → ℂ) i : ℂ)).re : ℂ)))
    (∑ t : Finset (AddChar G ℂ),
      HMul.hMul (α := ℂ)
        (𝔼 a : G,
          ∏ ψ ∈ t,
            HAdd.hAdd (β := ℂ) (HMul.hMul (β := ℂ) (d ψ) ((ψ : (a : G) → ℂ) a : ℂ))
                ((starRingEnd ℂ : (a : ℂ) → ℂ) (HMul.hMul (β := ℂ) (d ψ) ((ψ : (a : G) → ℂ) a : ℂ)) : ℂ) /
              2)
        (∏ ψ ∈ tᶜ, (↑(c ψ) : ℂ)))
have simp_rw₁ : Eq (α := ℂ)
  (𝔼 i : G, ∏ x : AddChar G ℂ, ((↑(c x) : ℂ) + (↑(HMul.hMul (β := ℂ) (d x) ((x : (a : G) → ℂ) i : ℂ)).re : ℂ)))
  (𝔼 i : G,
    ∑ j : Finset (AddChar G ℂ),
      HMul.hMul (α := ℂ)
        (∏ ψ ∈ j,
          HAdd.hAdd (β := ℂ) (HMul.hMul (β := ℂ) (d ψ) ((ψ : (a : G) → ℂ) i : ℂ))
              ((starRingEnd ℂ : (a : ℂ) → ℂ) (HMul.hMul (β := ℂ) (d ψ) ((ψ : (a : G) → ℂ) i : ℂ)) : ℂ) /
            2)
        (∏ ψ ∈ jᶜ, (↑(c ψ) : ℂ)))
Tactic: simp_rw [expect_mul, ← expect_sum_comm, ← Fintype.prod_add, add_comm,
          Complex.re_eq_add_conj]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Randomisation (goal)
Goal:
G : Type u_1
inst : Fintype G
inst_1 : AddCommGroup G
c : AddChar G ℂ → ℝ
d : AddChar G ℂ → ℂ
hcd : AddDissociated.{u_1} (α := AddChar G ℂ) {ψ : AddChar G ℂ | d ψ ≠ 0}
simp_rw :
  Eq (α := ℂ)
    (𝔼 i : G, ∏ x : AddChar G ℂ, ((↑(c x) : ℂ) + (↑(HMul.hMul (β := ℂ) (d x) ((x : (a : G) → ℂ) i : ℂ)).re : ℂ)))
    (∑ x : Finset (AddChar G ℂ),
      𝔼 i : G,
        HMul.hMul (α := ℂ)
          (∏ ψ ∈ x,
            HAdd.hAdd (β := ℂ) (HMul.hMul (β := ℂ) (d ψ) ((ψ : (a : G) → ℂ) i : ℂ))
                ((starRingEnd ℂ : (a : ℂ) → ℂ) (HMul.hMul (β := ℂ) (d ψ) ((ψ : (a : G) → ℂ) i : ℂ)) : ℂ) /
              2)
          (∏ ψ ∈ xᶜ, (↑(c ψ) : ℂ)))
simp_rw₁ :
  Eq (α := ℂ)
    (𝔼 i : G, ∏ x : AddChar G ℂ, ((↑(c x) : ℂ) + (↑(HMul.hMul (β := ℂ) (d x) ((x : (a : G) → ℂ) i : ℂ)).re : ℂ)))
    (𝔼 i : G,
      ∑ j : Finset (AddChar G ℂ),
        HMul.hMul (α := ℂ)
          (∏ ψ ∈ j,
            HAdd.hAdd (β := ℂ) (HMul.hMul (β := ℂ) (d ψ) ((ψ : (a : G) → ℂ) i : ℂ))
                ((starRingEnd ℂ : (a : ℂ) → ℂ) (HMul.hMul (β := ℂ) (d ψ) ((ψ : (a : G) → ℂ) i : ℂ)) : ℂ) /
              2)
          (∏ ψ ∈ jᶜ, (↑(c ψ) : ℂ)))
⊢ Eq (α := ℂ)
    (𝔼 i : G, ∏ x : AddChar G ℂ, ((↑(c x) : ℂ) + (↑(HMul.hMul (β := ℂ) (d x) ((x : (a : G) → ℂ) i : ℂ)).re : ℂ)))
    (∑ t : Finset (AddChar G ℂ),
      HMul.hMul (α := ℂ)
        (𝔼 a : G,
          ∏ ψ ∈ t,
            HAdd.hAdd (β := ℂ) (HMul.hMul (β := ℂ) (d ψ) ((ψ : (a : G) → ℂ) a : ℂ))
                ((starRingEnd ℂ : (a : ℂ) → ℂ) (HMul.hMul (β := ℂ) (d ψ) ((ψ : (a : G) → ℂ) a : ℂ)) : ℂ) /
              2)
        (∏ ψ ∈ tᶜ, (↑(c ψ) : ℂ)))
have simp_rw₂ : Eq (α := ℂ)
  (𝔼 i : G, ∏ x : AddChar G ℂ, ((↑(c x) : ℂ) + (↑(HMul.hMul (β := ℂ) (d x) ((x : (a : G) → ℂ) i : ℂ)).re : ℂ)))
  (𝔼 i : G,
    ∏ a : AddChar G ℂ,
      (HAdd.hAdd (β := ℂ) (HMul.hMul (β := ℂ) (d a) ((a : (a : G) → ℂ) i : ℂ))
            ((starRingEnd ℂ : (a : ℂ) → ℂ) (HMul.hMul (β := ℂ) (d a) ((a : (a : G) → ℂ) i : ℂ)) : ℂ) /
          2 +
        (↑(c a) : ℂ)))
Tactic: simp_rw [expect_mul, ← expect_sum_comm, ← Fintype.prod_add, add_comm,
          Complex.re_eq_add_conj]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Randomisation (goal)
Goal:
G : Type u_1
inst : Fintype G
inst_1 : AddCommGroup G
c : AddChar G ℂ → ℝ
d : AddChar G ℂ → ℂ
hcd : AddDissociated.{u_1} (α := AddChar G ℂ) {ψ : AddChar G ℂ | d ψ ≠ 0}
simp_rw :
  Eq (α := ℂ)
    (𝔼 i : G, ∏ x : AddChar G ℂ, ((↑(c x) : ℂ) + (↑(HMul.hMul (β := ℂ) (d x) ((x : (a : G) → ℂ) i : ℂ)).re : ℂ)))
    (∑ x : Finset (AddChar G ℂ),
      𝔼 i : G,
        HMul.hMul (α := ℂ)
          (∏ ψ ∈ x,
            HAdd.hAdd (β := ℂ) (HMul.hMul (β := ℂ) (d ψ) ((ψ : (a : G) → ℂ) i : ℂ))
                ((starRingEnd ℂ : (a : ℂ) → ℂ) (HMul.hMul (β := ℂ) (d ψ) ((ψ : (a : G) → ℂ) i : ℂ)) : ℂ) /
              2)
          (∏ ψ ∈ xᶜ, (↑(c ψ) : ℂ)))
simp_rw₁ :
  Eq (α := ℂ)
    (𝔼 i : G, ∏ x : AddChar G ℂ, ((↑(c x) : ℂ) + (↑(HMul.hMul (β := ℂ) (d x) ((x : (a : G) → ℂ) i : ℂ)).re : ℂ)))
    (𝔼 i : G,
      ∑ j : Finset (AddChar G ℂ),
        HMul.hMul (α := ℂ)
          (∏ ψ ∈ j,
            HAdd.hAdd (β := ℂ) (HMul.hMul (β := ℂ) (d ψ) ((ψ : (a : G) → ℂ) i : ℂ))
                ((starRingEnd ℂ : (a : ℂ) → ℂ) (HMul.hMul (β := ℂ) (d ψ) ((ψ : (a : G) → ℂ) i : ℂ)) : ℂ) /
              2)
          (∏ ψ ∈ jᶜ, (↑(c ψ) : ℂ)))
simp_rw₂ :
  Eq (α := ℂ)
    (𝔼 i : G, ∏ x : AddChar G ℂ, ((↑(c x) : ℂ) + (↑(HMul.hMul (β := ℂ) (d x) ((x : (a : G) → ℂ) i : ℂ)).re : ℂ)))
    (𝔼 i : G,
      ∏ a : AddChar G ℂ,
        (HAdd.hAdd (β := ℂ) (HMul.hMul (β := ℂ) (d a) ((a : (a : G) → ℂ) i : ℂ))
              ((starRingEnd ℂ : (a : ℂ) → ℂ) (HMul.hMul (β := ℂ) (d a) ((a : (a : G) → ℂ) i : ℂ)) : ℂ) /
            2 +
          (↑(c a) : ℂ)))
⊢ Eq (α := ℂ)
    (𝔼 i : G, ∏ x : AddChar G ℂ, ((↑(c x) : ℂ) + (↑(HMul.hMul (β := ℂ) (d x) ((x : (a : G) → ℂ) i : ℂ)).re : ℂ)))
    (∑ t : Finset (AddChar G ℂ),
      HMul.hMul (α := ℂ)
        (𝔼 a : G,
          ∏ ψ ∈ t,
            HAdd.hAdd (β := ℂ) (HMul.hMul (β := ℂ) (d ψ) ((ψ : (a : G) → ℂ) a : ℂ))
                ((starRingEnd ℂ : (a : ℂ) → ℂ) (HMul.hMul (β := ℂ) (d ψ) ((ψ : (a : G) → ℂ) a : ℂ)) : ℂ) /
              2)
        (∏ ψ ∈ tᶜ, (↑(c ψ) : ℂ)))
have simp_rw₃ : Eq (α := ℂ)
  (𝔼 i : G, ∏ x : AddChar G ℂ, ((↑(c x) : ℂ) + (↑(HMul.hMul (β := ℂ) (d x) ((x : (a : G) → ℂ) i : ℂ)).re : ℂ)))
  (𝔼 i : G,
    ∏ x : AddChar G ℂ,
      ((↑(c x) : ℂ) +
        HAdd.hAdd (β := ℂ) (HMul.hMul (β := ℂ) (d x) ((x : (a : G) → ℂ) i : ℂ))
            ((starRingEnd ℂ : (a : ℂ) → ℂ) (HMul.hMul (β := ℂ) (d x) ((x : (a : G) → ℂ) i : ℂ)) : ℂ) /
          2))
Tactic: simp_rw [expect_mul, ← expect_sum_comm, ← Fintype.prod_add, add_comm,
          Complex.re_eq_add_conj]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Randomisation (goal)
Goal:
G : Type u_1
inst : Fintype G
inst_1 : AddCommGroup G
c : AddChar G ℂ → ℝ
d : AddChar G ℂ → ℂ
hcd : AddDissociated.{u_1} (α := AddChar G ℂ) {ψ : AddChar G ℂ | d ψ ≠ 0}
⊢ Eq (α := ℂ)
    (𝔼 i : G, ∏ x : AddChar G ℂ, ((↑(c x) : ℂ) + (↑(HMul.hMul (β := ℂ) (d x) ((x : (a : G) → ℂ) i : ℂ)).re : ℂ)))
    (∏ i : AddChar G ℂ, (↑(c i) : ℂ))
have _ : ∀ (t : Finset (AddChar G ℂ)) (ht : t ≠ ∅),
  Eq (α := ℂ)
    (𝔼 a : G,
      ∏ ψ ∈ t,
        HAdd.hAdd (β := ℂ) (HMul.hMul (β := ℂ) (d ψ) ((ψ : (a : G) → ℂ) a : ℂ))
            ((starRingEnd ℂ : (a : ℂ) → ℂ) (HMul.hMul (β := ℂ) (d ψ) ((ψ : (a : G) → ℂ) a : ℂ)) : ℂ) /
          2)
    0
Tactic: calc
    _ = ∑ t, (𝔼 a, ∏ ψ ∈ t, ((d ψ * ψ a) + conj (d ψ * ψ a)) / 2) * ∏ ψ ∈ tᶜ, (c ψ : ℂ) := by
        simp_rw [expect_mul, ← expect_sum_comm, ← Fintype.prod_add, add_comm,
          Complex.re_eq_add_conj]
    _ = (𝔼 a, ∏ ψ ∈ ∅, ((d ψ * ψ a) + conj (d ψ * ψ a)) / 2) * ∏ ψ ∈ ∅ᶜ, (c ψ : ℂ) :=
        Fintype.sum_eq_single ∅ fun t ht ↦ mul_eq_zero_of_left ?_ _
    _ = ∏ ψ, (c ψ : ℂ) := by simp
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Randomisation (goal)
Goal:
G : Type u_1
inst : Fintype G
inst_1 : AddCommGroup G
c : AddChar G ℂ → ℝ
d : AddChar G ℂ → ℂ
hcd : AddDissociated.{u_1} (α := AddChar G ℂ) {ψ : AddChar G ℂ | d ψ ≠ 0}
t : Finset (AddChar G ℂ)
ht : t ≠ ∅
⊢ Eq (α := ℂ)
    (𝔼 a : G,
      ∏ ψ ∈ t,
        HAdd.hAdd (β := ℂ) (HMul.hMul (β := ℂ) (d ψ) ((ψ : (a : G) → ℂ) a : ℂ))
            ((starRingEnd ℂ : (a : ℂ) → ℂ) (HMul.hMul (β := ℂ) (d ψ) ((ψ : (a : G) → ℂ) a : ℂ)) : ℂ) /
          2)
    0
have simp : Eq (α := ℂ)
  (∑ j ∈ t.powerset,
    𝔼 i : G,
      HMul.hMul (α := ℂ) (∏ i_1 ∈ j, HMul.hMul (β := ℂ) (d i_1) ((i_1 : (a : G) → ℂ) i : ℂ))
        (∏ i_1 ∈ t \ j,
          HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (d i_1) : ℂ)
            ((starRingEnd ℂ : (a : ℂ) → ℂ) ((i_1 : (a : G) → ℂ) i : ℂ) : ℂ)))
  0
Tactic: simp only [map_mul, prod_div_distrib, prod_add, prod_const, ← expect_div, expect_sum_comm,
    div_eq_zero_iff, pow_eq_zero_iff', OfNat.ofNat_ne_zero, ne_eq, card_eq_zero,
    false_and, or_false]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Randomisation (goal)
Goal:
G : Type u_1
inst : Fintype G
inst_1 : AddCommGroup G
c : AddChar G ℂ → ℝ
d : AddChar G ℂ → ℂ
hcd : AddDissociated.{u_1} (α := AddChar G ℂ) {ψ : AddChar G ℂ | d ψ ≠ 0}
t : Finset (AddChar G ℂ)
ht : t ≠ ∅
⊢ Eq (α := ℂ)
    (∑ j ∈ t.powerset,
      𝔼 i : G,
        HMul.hMul (α := ℂ) (∏ i_1 ∈ j, HMul.hMul (β := ℂ) (d i_1) ((i_1 : (a : G) → ℂ) i : ℂ))
          (∏ i_1 ∈ t \ j,
            HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (d i_1) : ℂ)
              ((starRingEnd ℂ : (a : ℂ) → ℂ) ((i_1 : (a : G) → ℂ) i : ℂ) : ℂ)))
    0
have refine : ∀ u ∈ t.powerset,
  Eq (α := ℂ)
    (𝔼 i : G,
      HMul.hMul (α := ℂ) (∏ i_1 ∈ u, HMul.hMul (β := ℂ) (d i_1) ((i_1 : (a : G) → ℂ) i : ℂ))
        (∏ i_1 ∈ t \ u,
          HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (d i_1) : ℂ)
            ((starRingEnd ℂ : (a : ℂ) → ℂ) ((i_1 : (a : G) → ℂ) i : ℂ) : ℂ)))
    0
Tactic: refine sum_eq_zero fun u _ ↦ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Randomisation (goal)
Goal:
G : Type u_1
inst : Fintype G
inst_1 : AddCommGroup G
c : AddChar G ℂ → ℝ
d : AddChar G ℂ → ℂ
hcd : AddDissociated.{u_1} (α := AddChar G ℂ) {ψ : AddChar G ℂ | d ψ ≠ 0}
t : Finset (AddChar G ℂ)
ht : t ≠ ∅
u : Finset (AddChar G ℂ)
h : u ∈ t.powerset
⊢ 𝔼 a : G,
      HMul.hMul (α := ℂ) (∏ ψ ∈ u, HMul.hMul (β := ℂ) (d ψ) ((ψ : (a : G) → ℂ) a : ℂ))
        (∏ ψ ∈ t \ u,
          HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (d ψ) : ℂ)
            ((starRingEnd ℂ : (a : ℂ) → ℂ) ((ψ : (a : G) → ℂ) a : ℂ) : ℂ)) =
    HMul.hMul (α := ℂ) (∏ ψ ∈ u, d ψ) (∏ ψ ∈ t \ u, (starRingEnd ℂ : (a : ℂ) → ℂ) (d ψ)) *
      𝔼 a : G, (HSub.hSub (α := AddChar G ℂ) (∑ ψ ∈ u, ψ) (∑ ψ ∈ t \ u, ψ) : (a : G) → ℂ) a
have simp_rw : Eq (α := ℂ)
  (𝔼 a : G,
    HMul.hMul (α := ℂ) (∏ ψ ∈ u, HMul.hMul (β := ℂ) (d ψ) ((ψ : (a : G) → ℂ) a : ℂ))
      (∏ ψ ∈ t \ u,
        HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (d ψ) : ℂ)
          ((starRingEnd ℂ : (a : ℂ) → ℂ) ((ψ : (a : G) → ℂ) a : ℂ) : ℂ)))
  (𝔼 i : G,
    HMul.hMul (β := ℂ) (HMul.hMul (α := ℂ) (∏ ψ ∈ u, d ψ) (∏ ψ ∈ t \ u, (starRingEnd ℂ : (a : ℂ) → ℂ) (d ψ)))
      ((HSub.hSub (α := AddChar G ℂ) (∑ ψ ∈ u, ψ) (∑ ψ ∈ t \ u, ψ) : (a : G) → ℂ) i : ℂ))
Tactic: simp_rw [mul_expect, AddChar.sub_apply, AddChar.sum_apply, mul_mul_mul_comm,
          ← prod_mul_distrib, AddChar.map_neg_eq_conj]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Randomisation (goal)
Goal:
G : Type u_1
inst : Fintype G
inst_1 : AddCommGroup G
c : AddChar G ℂ → ℝ
d : AddChar G ℂ → ℂ
hcd : AddDissociated.{u_1} (α := AddChar G ℂ) {ψ : AddChar G ℂ | d ψ ≠ 0}
t : Finset (AddChar G ℂ)
ht : t ≠ ∅
u : Finset (AddChar G ℂ)
h : u ∈ t.powerset
simp_rw :
  Eq (α := ℂ)
    (𝔼 a : G,
      HMul.hMul (α := ℂ) (∏ ψ ∈ u, HMul.hMul (β := ℂ) (d ψ) ((ψ : (a : G) → ℂ) a : ℂ))
        (∏ ψ ∈ t \ u,
          HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (d ψ) : ℂ)
            ((starRingEnd ℂ : (a : ℂ) → ℂ) ((ψ : (a : G) → ℂ) a : ℂ) : ℂ)))
    (𝔼 i : G,
      HMul.hMul (β := ℂ) (HMul.hMul (α := ℂ) (∏ ψ ∈ u, d ψ) (∏ ψ ∈ t \ u, (starRingEnd ℂ : (a : ℂ) → ℂ) (d ψ)))
        ((HSub.hSub (α := AddChar G ℂ) (∑ ψ ∈ u, ψ) (∑ ψ ∈ t \ u, ψ) : (a : G) → ℂ) i : ℂ))
⊢ 𝔼 a : G,
      HMul.hMul (α := ℂ) (∏ ψ ∈ u, HMul.hMul (β := ℂ) (d ψ) ((ψ : (a : G) → ℂ) a : ℂ))
        (∏ ψ ∈ t \ u,
          HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (d ψ) : ℂ)
            ((starRingEnd ℂ : (a : ℂ) → ℂ) ((ψ : (a : G) → ℂ) a : ℂ) : ℂ)) =
    HMul.hMul (α := ℂ) (∏ ψ ∈ u, d ψ) (∏ ψ ∈ t \ u, (starRingEnd ℂ : (a : ℂ) → ℂ) (d ψ)) *
      𝔼 a : G, (HSub.hSub (α := AddChar G ℂ) (∑ ψ ∈ u, ψ) (∑ ψ ∈ t \ u, ψ) : (a : G) → ℂ) a
have simp_rw₁ : Eq (α := ℂ)
  (𝔼 a : G,
    HMul.hMul (α := ℂ) (∏ ψ ∈ u, HMul.hMul (β := ℂ) (d ψ) ((ψ : (a : G) → ℂ) a : ℂ))
      (∏ ψ ∈ t \ u,
        HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (d ψ) : ℂ)
          ((starRingEnd ℂ : (a : ℂ) → ℂ) ((ψ : (a : G) → ℂ) a : ℂ) : ℂ)))
  (𝔼 i : G,
    HMul.hMul (α := ℂ) (∏ ψ ∈ u, d ψ) (∏ ψ ∈ t \ u, (starRingEnd ℂ : (a : ℂ) → ℂ) (d ψ)) *
      HMul.hMul (α := ℂ) (β := ℂ) ((∑ ψ ∈ u, ψ : (a : G) → ℂ) i : ℂ) ((∑ ψ ∈ t \ u, ψ : (a : G) → ℂ) (-i) : ℂ))
Tactic: simp_rw [mul_expect, AddChar.sub_apply, AddChar.sum_apply, mul_mul_mul_comm,
          ← prod_mul_distrib, AddChar.map_neg_eq_conj]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Randomisation (goal)
Goal:
G : Type u_1
inst : Fintype G
inst_1 : AddCommGroup G
c : AddChar G ℂ → ℝ
d : AddChar G ℂ → ℂ
hcd : AddDissociated.{u_1} (α := AddChar G ℂ) {ψ : AddChar G ℂ | d ψ ≠ 0}
t : Finset (AddChar G ℂ)
ht : t ≠ ∅
u : Finset (AddChar G ℂ)
h : u ∈ t.powerset
simp_rw :
  Eq (α := ℂ)
    (𝔼 a : G,
      HMul.hMul (α := ℂ) (∏ ψ ∈ u, HMul.hMul (β := ℂ) (d ψ) ((ψ : (a : G) → ℂ) a : ℂ))
        (∏ ψ ∈ t \ u,
          HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (d ψ) : ℂ)
            ((starRingEnd ℂ : (a : ℂ) → ℂ) ((ψ : (a : G) → ℂ) a : ℂ) : ℂ)))
    (𝔼 i : G,
      HMul.hMul (β := ℂ) (HMul.hMul (α := ℂ) (∏ ψ ∈ u, d ψ) (∏ ψ ∈ t \ u, (starRingEnd ℂ : (a : ℂ) → ℂ) (d ψ)))
        ((HSub.hSub (α := AddChar G ℂ) (∑ ψ ∈ u, ψ) (∑ ψ ∈ t \ u, ψ) : (a : G) → ℂ) i : ℂ))
simp_rw₁ :
  Eq (α := ℂ)
    (𝔼 a : G,
      HMul.hMul (α := ℂ) (∏ ψ ∈ u, HMul.hMul (β := ℂ) (d ψ) ((ψ : (a : G) → ℂ) a : ℂ))
        (∏ ψ ∈ t \ u,
          HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (d ψ) : ℂ)
            ((starRingEnd ℂ : (a : ℂ) → ℂ) ((ψ : (a : G) → ℂ) a : ℂ) : ℂ)))
    (𝔼 i : G,
      HMul.hMul (α := ℂ) (∏ ψ ∈ u, d ψ) (∏ ψ ∈ t \ u, (starRingEnd ℂ : (a : ℂ) → ℂ) (d ψ)) *
        HMul.hMul (α := ℂ) (β := ℂ) ((∑ ψ ∈ u, ψ : (a : G) → ℂ) i : ℂ) ((∑ ψ ∈ t \ u, ψ : (a : G) → ℂ) (-i) : ℂ))
⊢ 𝔼 a : G,
      HMul.hMul (α := ℂ) (∏ ψ ∈ u, HMul.hMul (β := ℂ) (d ψ) ((ψ : (a : G) → ℂ) a : ℂ))
        (∏ ψ ∈ t \ u,
          HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (d ψ) : ℂ)
            ((starRingEnd ℂ : (a : ℂ) → ℂ) ((ψ : (a : G) → ℂ) a : ℂ) : ℂ)) =
    HMul.hMul (α := ℂ) (∏ ψ ∈ u, d ψ) (∏ ψ ∈ t \ u, (starRingEnd ℂ : (a : ℂ) → ℂ) (d ψ)) *
      𝔼 a : G, (HSub.hSub (α := AddChar G ℂ) (∑ ψ ∈ u, ψ) (∑ ψ ∈ t \ u, ψ) : (a : G) → ℂ) a
have simp_rw₂ : Eq (α := ℂ)
  (𝔼 a : G,
    HMul.hMul (α := ℂ) (∏ ψ ∈ u, HMul.hMul (β := ℂ) (d ψ) ((ψ : (a : G) → ℂ) a : ℂ))
      (∏ ψ ∈ t \ u,
        HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (d ψ) : ℂ)
          ((starRingEnd ℂ : (a : ℂ) → ℂ) ((ψ : (a : G) → ℂ) a : ℂ) : ℂ)))
  (𝔼 i : G,
    HMul.hMul (α := ℂ) (∏ ψ ∈ u, d ψ) (∏ ψ ∈ t \ u, (starRingEnd ℂ : (a : ℂ) → ℂ) (d ψ)) *
      HMul.hMul (α := ℂ) (∏ i_1 ∈ u, (i_1 : (a : G) → ℂ) i) (∏ i_1 ∈ t \ u, (i_1 : (a : G) → ℂ) (-i)))
Tactic: simp_rw [mul_expect, AddChar.sub_apply, AddChar.sum_apply, mul_mul_mul_comm,
          ← prod_mul_distrib, AddChar.map_neg_eq_conj]