awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : CommGroup G
A : Finset G
hA : A.Nonempty
B : Finset G
m n : ℕ
rw :
  (↑(#(B⁻¹ ^ m / B⁻¹ ^ n)) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(A * B⁻¹)) : ℚ≥0) (↑(#A) : ℚ≥0) ^ (m + n) * (↑(#A) : ℚ≥0)
⊢ (↑(#(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]

Premises used: Finset.card_inv, inv_pow, div_eq_mul_inv, inv_div'
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
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)

Tactic:
pluennecke_ruzsa_inequality_pow_div_pow_mul hA _ _ _

Premises used: Finset.pluennecke_ruzsa_inequality_pow_div_pow_mul
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
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)

Tactic:
exact pluennecke_ruzsa_inequality_pow_div_pow_mul hA _ _ _

Premises used: Finset.pluennecke_ruzsa_inequality_pow_div_pow_mul
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : CommGroup G
A : Finset G
hA : A.Nonempty
B : Finset G
n : ℕ
⊢ (↑(#(B ^ n)) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0) ^ n * (↑(#A) : ℚ≥0)

Tactic:
simpa only [_root_.pow_zero, div_one] using pluennecke_ruzsa_inequality_pow_div_pow_mul hA _ _ 0

Premises used: Finset.pluennecke_ruzsa_inequality_pow_div_pow_mul, pow_zero, OfNat.ofNat, div_one
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : CommGroup G
A : Finset G
hA : A.Nonempty
B : Finset G
n : ℕ
⊢ (↑(#(B ^ n)) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(A / B)) : ℚ≥0) (↑(#A) : ℚ≥0) ^ n * (↑(#A) : ℚ≥0)

Tactic:
simpa only [_root_.pow_zero, div_one] using pluennecke_ruzsa_inequality_pow_div_pow_div hA _ _ 0

Premises used: pow_zero, Finset.pluennecke_ruzsa_inequality_pow_div_pow_div, OfNat.ofNat, div_one
-- Module: Mathlib.Combinatorics.Additive.Randomisation
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 ψ)

Tactic:
Complex.ofReal_injective ?_

Premises used: Complex.ofReal_injective
-- Module: Mathlib.Combinatorics.Additive.Randomisation
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}
refine :
  (↑(𝔼 a : G, ∏ ψ : AddChar G ℂ, (c ψ + (HMul.hMul (β := ℂ) (d ψ) ((ψ : (a : G) → ℂ) a : ℂ)).re)) : ℂ) =
    (↑(∏ ψ : AddChar G ℂ, c ψ) : ℂ)
⊢ Eq (α := ℝ) (𝔼 a : G, ∏ ψ : AddChar G ℂ, (c ψ + (HMul.hMul (β := ℂ) (d ψ) ((ψ : (a : G) → ℂ) a : ℂ)).re))
    (∏ ψ : AddChar G ℂ, c ψ)

Tactic:
refine Complex.ofReal_injective ?_

Premises used: Complex.ofReal_injective
-- Module: Mathlib.Combinatorics.Additive.Randomisation
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}
push_cast :
  Eq (α := ℂ)
    (𝔼 i : G, ∏ x : AddChar G ℂ, ((↑(c x) : ℂ) + (↑(HMul.hMul (β := ℂ) (d x) ((x : (a : G) → ℂ) i : ℂ)).re : ℂ)))
    (∏ i : AddChar G ℂ, (↑(c i) : ℂ))
⊢ (↑(𝔼 a : G, ∏ ψ : AddChar G ℂ, (c ψ + (HMul.hMul (β := ℂ) (d ψ) ((ψ : (a : G) → ℂ) a : ℂ)).re)) : ℂ) =
    (↑(∏ ψ : AddChar G ℂ, c ψ) : ℂ)

Tactic:
push_cast
-- Module: Mathlib.Combinatorics.Additive.Randomisation
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) : ℂ)))
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))
⊢ 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 ψ) : ℂ)))

Tactic:
simp_rw [expect_mul, ← expect_sum_comm, ← Fintype.prod_add, add_comm,
          Complex.re_eq_add_conj]

Premises used: Complex.re_eq_add_conj, Fintype.prod_add, Finset.expect_mul, add_comm, Finset.expect_sum_comm
-- Module: Mathlib.Combinatorics.Additive.Randomisation
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 ℂ),
      HMul.hMul (α := ℂ)
        (𝔼 a : G,
          ∏ ψ ∈ t,
            HAdd.hAdd (β := ℂ) (HMul.hMul (β := ℂ) (d ψ) ((ψ : (a : G) → ℂ) a : ℂ))
                ((starRingEnd ℂ : (a : ℂ) → ℂ) (HMul.hMul (β := ℂ) (d ψ) ((ψ : (a : G) → ℂ) a : ℂ)) : ℂ) /
              2)
        (∏ ψ ∈ tᶜ, (↑(c ψ) : ℂ)) =
    HMul.hMul (α := ℂ)
      (𝔼 a : G,
        ∏ ψ ∈ ∅,
          HAdd.hAdd (β := ℂ) (HMul.hMul (β := ℂ) (d ψ) ((ψ : (a : G) → ℂ) a : ℂ))
              ((starRingEnd ℂ : (a : ℂ) → ℂ) (HMul.hMul (β := ℂ) (d ψ) ((ψ : (a : G) → ℂ) a : ℂ)) : ℂ) /
            2)
      (∏ ψ ∈ ∅ᶜ, (↑(c ψ) : ℂ))

Tactic:
Fintype.sum_eq_single ∅ fun t ht ↦ mul_eq_zero_of_left ?_ _

Premises used: Compl.compl, mul_eq_zero_of_left, Complex.ofReal, Finset.prod, EmptyCollection.emptyCollection, Fintype.sum_eq_single
-- Module: Mathlib.Combinatorics.Additive.Randomisation
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}
⊢ HMul.hMul (α := ℂ)
      (𝔼 a : G,
        ∏ ψ ∈ ∅,
          HAdd.hAdd (β := ℂ) (HMul.hMul (β := ℂ) (d ψ) ((ψ : (a : G) → ℂ) a : ℂ))
              ((starRingEnd ℂ : (a : ℂ) → ℂ) (HMul.hMul (β := ℂ) (d ψ) ((ψ : (a : G) → ℂ) a : ℂ)) : ℂ) /
            2)
      (∏ ψ ∈ ∅ᶜ, (↑(c ψ) : ℂ)) =
    ∏ ψ : AddChar G ℂ, (↑(c ψ) : ℂ)

Tactic:
simp
-- Module: Mathlib.Combinatorics.Additive.Randomisation
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
⊢ Eq (α := ℂ)
    (𝔼 i : G, ∏ x : AddChar G ℂ, ((↑(c x) : ℂ) + (↑(HMul.hMul (β := ℂ) (d x) ((x : (a : G) → ℂ) i : ℂ)).re : ℂ)))
    (∏ i : AddChar G ℂ, (↑(c i) : ℂ))

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

Premises used: HMul.hMul, Finset.univ, Finset.expect, HDiv.hDiv, Finset.prod, HAdd.hAdd, EmptyCollection.emptyCollection, Complex, starRingEnd, OfNat.ofNat, DFunLike.coe, Fintype.sum_eq_single
-- Module: Mathlib.Combinatorics.Additive.Randomisation
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 ≠ ∅
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
⊢ Eq (α := ℂ)
    (𝔼 a : G,
      ∏ ψ ∈ t,
        HAdd.hAdd (β := ℂ) (HMul.hMul (β := ℂ) (d ψ) ((ψ : (a : G) → ℂ) a : ℂ))
            ((starRingEnd ℂ : (a : ℂ) → ℂ) (HMul.hMul (β := ℂ) (d ψ) ((ψ : (a : G) → ℂ) a : ℂ)) : ℂ) /
          2)
    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]

Premises used: Finset.prod_add, OfNat.ofNat_ne_zero, false_and, pow_eq_zero_iff', Finset.prod_const, ne_eq, map_mul, Finset.card_eq_zero, or_false, Finset.expect_div, div_eq_zero_iff, Finset.prod_div_distrib, Finset.expect_sum_comm
-- Module: Mathlib.Combinatorics.Additive.Randomisation
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

Tactic:
sum_eq_zero fun u _ ↦ ?_

Premises used: Finset.sum_eq_zero
-- Module: Mathlib.Combinatorics.Additive.Randomisation
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 ≠ ∅
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
⊢ 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:
refine sum_eq_zero fun u _ ↦ ?_

Premises used: Finset.sum_eq_zero
-- Module: Mathlib.Combinatorics.Additive.Randomisation
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
⊢ HMul.hMul (α := ℂ) (∏ ψ ∈ u, d ψ) (∏ ψ ∈ t \ u, (starRingEnd ℂ : (a : ℂ) → ℂ) (d ψ)) *
      𝔼 a : G, (HSub.hSub (α := AddChar G ℂ) (∑ ψ ∈ u, ψ) (∑ ψ ∈ t \ u, ψ) : (a : G) → ℂ) a =
    0

Tactic:
?_
-- Module: Mathlib.Combinatorics.Additive.Randomisation
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
𝔼 :
  HMul.hMul (α := ℂ) (∏ ψ ∈ u, d ψ) (∏ ψ ∈ t \ u, (starRingEnd ℂ : (a : ℂ) → ℂ) (d ψ)) *
      𝔼 a : G, (HSub.hSub (α := AddChar G ℂ) (∑ ψ ∈ u, ψ) (∑ ψ ∈ t \ u, ψ) : (a : G) → ℂ) a =
    0
⊢ 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:
calc
    𝔼 a, (∏ ψ ∈ u, d ψ * ψ a) * ∏ ψ ∈ t \ u, conj (d ψ) * conj (ψ a)
      = ((∏ ψ ∈ u, d ψ) * ∏ ψ ∈ t \ u, conj (d ψ)) * 𝔼 a, (∑ ψ ∈ u, ψ - ∑ ψ ∈ t \ u, ψ) a := by
        simp_rw [mul_expect, AddChar.sub_apply, AddChar.sum_apply, mul_mul_mul_comm,
          ← prod_mul_distrib, AddChar.map_neg_eq_conj]
    _ = 0 := ?_

Premises used: HMul.hMul, Finset.prod, SDiff.sdiff, Complex, starRingEnd, DFunLike.coe
-- Module: Mathlib.Combinatorics.Additive.Randomisation
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
rw :
  ((∀ a ∈ u, d a ≠ 0) ∧ ∀ a ∈ t \ u, Ne (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (d a) : ℂ) (0 : ℂ)) →
    Ne (α := AddChar G ℂ) (∑ ψ ∈ u, ψ) (∑ ψ ∈ t \ u, ψ)
⊢ HMul.hMul (α := ℂ) (∏ ψ ∈ u, d ψ) (∏ ψ ∈ t \ u, (starRingEnd ℂ : (a : ℂ) → ℂ) (d ψ)) *
      𝔼 a : G, (HSub.hSub (α := AddChar G ℂ) (∑ ψ ∈ u, ψ) (∑ ψ ∈ t \ u, ψ) : (a : G) → ℂ) a =
    0

Tactic:
rw [mul_eq_zero, AddChar.expect_eq_zero_iff_ne_zero, sub_ne_zero, or_iff_not_imp_left, ← Ne,
    mul_ne_zero_iff, prod_ne_zero_iff, prod_ne_zero_iff]

Premises used: sub_ne_zero, Ne, Finset.prod_ne_zero_iff, mul_eq_zero, AddChar.expect_eq_zero_iff_ne_zero, Classical.or_iff_not_imp_left, mul_ne_zero_iff
-- Module: Mathlib.Combinatorics.Additive.Randomisation
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_1 : u ∈ t.powerset
h : (∀ a ∈ u, d a ≠ 0) ∧ ∀ a ∈ t \ u, Ne (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (d a) : ℂ) (0 : ℂ)
⊢ Membership.mem (γ := Set (Finset (AddChar G ℂ)))
    {t : Finset (AddChar G ℂ) | (↑t : Set (AddChar G ℂ)) ⊆ {ψ : AddChar G ℂ | d ψ ≠ 0}} (t \ u)

Tactic:
simpa only [map_ne_zero] using h.2

Premises used: And.right, map_ne_zero
-- Module: Mathlib.Combinatorics.Additive.Randomisation
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 ∈ u, d a ≠ 0) ∧ ∀ a ∈ t \ u, Ne (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (d a) : ℂ) (0 : ℂ)) →
    Ne (α := AddChar G ℂ) (∑ ψ ∈ u, ψ) (∑ ψ ∈ t \ u, ψ)

Tactic:
exact fun h ↦ hcd.ne h.1 (by simpa only [map_ne_zero] using h.2)
    (sdiff_ne_right.2 <| .inl ht).symm

Premises used: Iff.mpr, Ne.symm, sdiff_ne_right, Set.InjOn.ne, Or.inl
-- Module: Mathlib.Combinatorics.Additive.RuzsaCovering
Goal:
G : Type u_1
inst : Group G
K : ℝ
inst_1 : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : (↑(#(A * B)) : ℝ) ≤ K * (↑(#B) : ℝ)
haveI :
  ∀ (this : (F : Set G) → Decidable (F.PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B)),
    ∃ F ⊆ A, (↑(#F) : ℝ) ≤ K ∧ A ⊆ F * (B / B)
⊢ ∃ F ⊆ A, (↑(#F) : ℝ) ≤ K ∧ A ⊆ F * (B / B)

Tactic:
haveI : ∀ F, Decidable ((F : Set G).PairwiseDisjoint (· • B)) := fun F ↦ Classical.dec _
-- Module: Mathlib.Combinatorics.Additive.RuzsaCovering
Goal:
G : Type u_1
inst : Group G
K : ℝ
inst_1 : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : (↑(#(A * B)) : ℝ) ≤ K * (↑(#B) : ℝ)
this : (F : Set G) → Decidable (F.PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B)
C : Finset (Finset G) := {F ∈ A.powerset | (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B}
⊢ (↑∅ : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B

Tactic:
simp [coe_empty]

Premises used: Finset.coe_empty
-- Module: Mathlib.Combinatorics.Additive.RuzsaCovering
Goal:
G : Type u_1
inst : Group G
K : ℝ
inst_1 : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : (↑(#(A * B)) : ℝ) ≤ K * (↑(#B) : ℝ)
this : (F : Set G) → Decidable (F.PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B)
C : Finset (Finset G) := {F ∈ A.powerset | (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B}
obtain : ∀ (F : Finset G) (hFmax : Maximal (fun (x : Finset G) ↦ x ∈ C) F), ∃ F ⊆ A, (↑(#F) : ℝ) ≤ K ∧ A ⊆ F * (B / B)
⊢ ∃ F ⊆ A, (↑(#F) : ℝ) ≤ K ∧ A ⊆ F * (B / B)

Tactic:
obtain ⟨F, hFmax⟩ := C.exists_maximal <| filter_nonempty_iff.2
    ⟨∅, empty_mem_powerset _, by simp [coe_empty]⟩

Premises used: Iff.mpr, Finset.filter_nonempty_iff, Finset.empty_mem_powerset, Finset.exists_maximal, And.intro, Exists.intro, EmptyCollection.emptyCollection
-- Module: Mathlib.Combinatorics.Additive.RuzsaCovering
Goal:
G : Type u_1
inst : Group G
K : ℝ
inst_1 : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : (↑(#(A * B)) : ℝ) ≤ K * (↑(#B) : ℝ)
this : (F : Set G) → Decidable (F.PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B)
C : Finset (Finset G) := {F ∈ A.powerset | (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B}
F : Finset G
hFmax : Maximal (fun (x : Finset G) ↦ x ∈ C) F
⊢ Maximal (fun (x : Finset G) ↦ x ⊆ A ∧ (↑x : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B) F

Tactic:
simp only [C, mem_filter, mem_powerset] at hFmax

Premises used: Finset.mem_powerset, Finset.mem_filter
-- Module: Mathlib.Combinatorics.Additive.RuzsaCovering
Goal:
G : Type u_1
inst : Group G
K : ℝ
inst_1 : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : (↑(#(A * B)) : ℝ) ≤ K * (↑(#B) : ℝ)
this : (F : Set G) → Decidable (F.PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B)
C : Finset (Finset G) := {F ∈ A.powerset | (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B}
F : Finset G
hFmax : Maximal (fun (x : Finset G) ↦ x ⊆ A ∧ (↑x : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B) F
⊢ F ⊆ A

Tactic:
obtain ⟨hFA, hF⟩ := hFmax.1

Premises used: And.left
-- Module: Mathlib.Combinatorics.Additive.RuzsaCovering
Goal:
G : Type u_1
inst : Group G
K : ℝ
inst_1 : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : (↑(#(A * B)) : ℝ) ≤ K * (↑(#B) : ℝ)
this : (F : Set G) → Decidable (F.PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B)
C : Finset (Finset G) := {F ∈ A.powerset | (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B}
F : Finset G
hFmax : Maximal (fun (x : Finset G) ↦ x ⊆ A ∧ (↑x : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B) F
hFA : F ⊆ A
⊢ (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B

Tactic:
obtain ⟨hFA, hF⟩ := hFmax.1

Premises used: And.left
-- Module: Mathlib.Combinatorics.Additive.RuzsaCovering
Goal:
G : Type u_1
inst : Group G
K : ℝ
inst_1 : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : (↑(#(A * B)) : ℝ) ≤ K * (↑(#B) : ℝ)
this : (F : Set G) → Decidable (F.PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B)
C : Finset (Finset G) := {F ∈ A.powerset | (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B}
F : Finset G
hFmax : Maximal (fun (x : Finset G) ↦ x ⊆ A ∧ (↑x : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B) F
hFA : F ⊆ A
hF : (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B
⊢ LT.lt (α := ℝ) 0 (↑(#B) : ℝ)

Tactic:
positivity
-- Module: Mathlib.Combinatorics.Additive.RuzsaCovering
Goal:
G : Type u_1
inst : Group G
K : ℝ
inst_1 : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : (↑(#(A * B)) : ℝ) ≤ K * (↑(#B) : ℝ)
this : (F : Set G) → Decidable (F.PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B)
C : Finset (Finset G) := {F ∈ A.powerset | (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B}
F : Finset G
hFmax : Maximal (fun (x : Finset G) ↦ x ⊆ A ∧ (↑x : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B) F
hFA : F ⊆ A
hF : (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B
refine_1 : HMul.hMul (α := ℝ) (↑(#F) : ℝ) (↑(#B) : ℝ) ≤ K * (↑(#B) : ℝ)
refine_2 : ∀ (a : G) (ha : a ∈ A), a ∈ F * (B / B)
⊢ ∃ F ⊆ A, (↑(#F) : ℝ) ≤ K ∧ A ⊆ F * (B / B)

Tactic:
refine ⟨F, hFA, le_of_mul_le_mul_right ?_ (by positivity : (0 : ℝ) < #B), fun a ha ↦ ?_⟩
-- Module: Mathlib.Combinatorics.Additive.RuzsaCovering
Goal:
G : Type u_1
inst : Group G
K : ℝ
inst_1 : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : (↑(#(A * B)) : ℝ) ≤ K * (↑(#B) : ℝ)
this : (F : Set G) → Decidable (F.PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B)
C : Finset (Finset G) := {F ∈ A.powerset | (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B}
F : Finset G
hFmax : Maximal (fun (x : Finset G) ↦ x ⊆ A ∧ (↑x : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B) F
hFA : F ⊆ A
hF : (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B
rw : HMul.hMul (α := ℝ) (↑(#F) : ℝ) (↑(#B) : ℝ) = (↑(#F * #B) : ℝ)
rw₁ rw₂ : HMul.hMul (α := ℝ) (↑(#F) : ℝ) (↑(#B) : ℝ) = HMul.hMul (α := ℝ) (↑(#F) : ℝ) (↑(#B) : ℝ)
⊢ HMul.hMul (α := ℝ) (↑(#F) : ℝ) (↑(#B) : ℝ) = (↑(#(F * B)) : ℝ)

Tactic:
rw [card_mul_iff.2 <| pairwiseDisjoint_smul_iff.1 hF, Nat.cast_mul]

Premises used: Iff.mpr, Finset.pairwiseDisjoint_smul_iff, Finset.card_mul_iff, Nat.cast_mul, Iff.mp
-- Module: Mathlib.Combinatorics.Additive.RuzsaCovering
Goal:
G : Type u_1
inst : Group G
K : ℝ
inst_1 : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : (↑(#(A * B)) : ℝ) ≤ K * (↑(#B) : ℝ)
this : (F : Set G) → Decidable (F.PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B)
C : Finset (Finset G) := {F ∈ A.powerset | (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B}
F : Finset G
hFmax : Maximal (fun (x : Finset G) ↦ x ⊆ A ∧ (↑x : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B) F
hFA : F ⊆ A
hF : (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B
⊢ LE.le (α := ℝ) (↑(#(F * B)) : ℝ) (↑(#(A * B)) : ℝ)

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.Additive.RuzsaCovering
Goal:
G : Type u_1
inst : Group G
K : ℝ
inst_1 : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : (↑(#(A * B)) : ℝ) ≤ K * (↑(#B) : ℝ)
this : (F : Set G) → Decidable (F.PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B)
C : Finset (Finset G) := {F ∈ A.powerset | (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B}
F : Finset G
hFmax : Maximal (fun (x : Finset G) ↦ x ⊆ A ∧ (↑x : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B) F
hFA : F ⊆ A
hF : (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B
⊢ (↑(#(A * B)) : ℝ) ≤ K * (↑(#B) : ℝ)

Tactic:
hK