awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.BigOperators.Associated
Goal:
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : IsCancelMulZero M₀
inst_2 : (a : M₀) → DecidablePred (Associated a)
a : M₀
s : Multiset M₀
induct :
  ∀ (n : M₀) (h : ∀ a ∈ s, Prime a) (div : ∀ a ∈ s, a ∣ n) (uniq : ∀ (a : M₀), countP (Associated a) s ≤ 1), s.prod ∣ n
h : ∀ a_1 ∈ a ::ₘ s, Prime a_1
uniq : ∀ (a_1 : M₀), countP (Associated a_1) (a ::ₘ s) ≤ 1
k : M₀
div : ∀ a_1 ∈ a ::ₘ s, a_1 ∣ a * k
b : M₀
b_in_s : b ∈ s
b_div_n : b ∣ a * k
a_prime : Prime a
b_prime : Prime b
b_div_a : b ∣ a
assoc : b ~ᵤ a
this : countP (Associated a) (a ::ₘ s) ≤ 1
⊢ ¬∃ a_1 ∈ s, a ~ᵤ a_1

Tactic:
rw [Multiset.countP_cons_of_pos _ (Associated.refl _), Nat.succ_le_succ_iff, ← not_lt,
      Multiset.countP_pos] at this

Premises used: not_lt, Nat.succ_le_succ_iff, Multiset.countP_cons_of_pos, Associated.refl, Multiset.countP_pos
-- Module: Mathlib.Algebra.BigOperators.Associated
Goal:
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : IsCancelMulZero M₀
inst_2 : (a : M₀) → DecidablePred (Associated a)
a : M₀
s : Multiset M₀
induct :
  ∀ (n : M₀) (h : ∀ a ∈ s, Prime a) (div : ∀ a ∈ s, a ∣ n) (uniq : ∀ (a : M₀), countP (Associated a) s ≤ 1), s.prod ∣ n
h : ∀ a_1 ∈ a ::ₘ s, Prime a_1
uniq : ∀ (a_1 : M₀), countP (Associated a_1) (a ::ₘ s) ≤ 1
k : M₀
div : ∀ a_1 ∈ a ::ₘ s, a_1 ∣ a * k
b : M₀
b_in_s : b ∈ s
b_div_n : b ∣ a * k
a_prime : Prime a
b_prime : Prime b
b_div_a : b ∣ a
assoc : b ~ᵤ a
this : ¬∃ a_1 ∈ s, a ~ᵤ a_1
⊢ False

Tactic:
this ⟨b, b_in_s, assoc.symm⟩

Premises used: Associated.symm, And.intro, Exists.intro
-- Module: Mathlib.Algebra.BigOperators.Associated
Goal:
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : IsCancelMulZero M₀
inst_2 : (a : M₀) → DecidablePred (Associated a)
a : M₀
s : Multiset M₀
induct :
  ∀ (n : M₀) (h : ∀ a ∈ s, Prime a) (div : ∀ a ∈ s, a ∣ n) (uniq : ∀ (a : M₀), countP (Associated a) s ≤ 1), s.prod ∣ n
h : ∀ a_1 ∈ a ::ₘ s, Prime a_1
uniq : ∀ (a_1 : M₀), countP (Associated a_1) (a ::ₘ s) ≤ 1
k : M₀
div : ∀ a_1 ∈ a ::ₘ s, a_1 ∣ a * k
b : M₀
b_in_s : b ∈ s
b_div_n : b ∣ a * k
a_prime : Prime a
b_prime : Prime b
b_div_a : b ∣ a
assoc : b ~ᵤ a
this : ¬∃ a_1 ∈ s, a ~ᵤ a_1
⊢ False

Tactic:
exact this ⟨b, b_in_s, assoc.symm⟩

Premises used: Associated.symm, And.intro, Exists.intro
-- Module: Mathlib.Algebra.BigOperators.Associated
Goal:
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : IsCancelMulZero M₀
inst_2 : (a : M₀) → DecidablePred (Associated a)
s : Multiset M₀
n : M₀
h : ∀ a ∈ s, Prime a
div : ∀ a ∈ s, a ∣ n
uniq : ∀ (a : M₀), countP (Associated a) s ≤ 1
empty :
  ∀ (n : M₀) (h : ∀ (a : M₀), Membership.mem (γ := Multiset M₀) 0 a → Prime a)
    (div : ∀ (a : M₀), Membership.mem (γ := Multiset M₀) 0 a → a ∣ n) (uniq : ∀ (a : M₀), countP (Associated a) 0 ≤ 1),
    prod 0 ∣ n
cons :
  ∀ (a : M₀) (s : Multiset M₀)
    (induct :
      ∀ (n : M₀) (h : ∀ a ∈ s, Prime a) (div : ∀ a ∈ s, a ∣ n) (uniq : ∀ (a : M₀), countP (Associated a) s ≤ 1),
        s.prod ∣ n)
    (n : M₀) (h : ∀ a_1 ∈ a ::ₘ s, Prime a_1) (div : ∀ a_1 ∈ a ::ₘ s, a_1 ∣ n)
    (uniq : ∀ (a_1 : M₀), countP (Associated a_1) (a ::ₘ s) ≤ 1), (a ::ₘ s).prod ∣ n
⊢ s.prod ∣ n

Tactic:
induction s using Multiset.induction_on generalizing n with
  | empty => simp only [Multiset.prod_zero, one_dvd]
  | cons a s induct =>
    rw [Multiset.prod_cons]
    obtain ⟨k, rfl⟩ : a ∣ n := div a (Multiset.mem_cons_self a s)
    gcongr
    refine induct _ (fun a ha => h a (Multiset.mem_cons_of_mem ha)) (fun b b_in_s => ?_)
      fun a => (Multiset.countP_le_of_le _ (Multiset.le_cons_self _ _)).trans (uniq a)
    have b_div_n := div b (Multiset.mem_cons_of_mem b_in_s)
    have a_prime := h a (Multiset.mem_cons_self a s)
    have b_prime := h b (Multiset.mem_cons_of_mem b_in_s)
    refine (b_prime.dvd_or_dvd b_div_n).resolve_left fun b_div_a => ?_
    have assoc := b_prime.associated_of_dvd a_prime b_div_a
    have := uniq a
    rw [Multiset.countP_cons_of_pos _ (Associated.refl _), Nat.succ_le_succ_iff, ← not_lt,
      Multiset.countP_pos] at this
    exact this ⟨b, b_in_s, assoc.symm⟩

Premises used: Multiset.prod_zero, Multiset.prod_cons, Multiset.cons, one_dvd, not_lt, Nat.succ_le_succ_iff, Multiset.countP_cons_of_pos, Associated.refl, Multiset.countP_pos, rfl
-- Module: Mathlib.Algebra.BigOperators.Associated
Goal:
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : IsCancelMulZero M₀
inst_2 : Subsingleton.{u_3 + 1} M₀ˣ
s : Finset M₀
n : M₀
h : ∀ a ∈ s, Prime a
div : ∀ a ∈ s, a ∣ n
⊢ ∀ (a : M₀), Membership.mem (γ := Multiset M₀) (Multiset.map (fun (p : M₀) ↦ p) s.val) a → Prime a

Tactic:
simpa only [Multiset.map_id', Finset.mem_def] using h

Premises used: Multiset.map_id', Finset.mem_def
-- Module: Mathlib.Algebra.BigOperators.Associated
Goal:
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : IsCancelMulZero M₀
inst_2 : Subsingleton.{u_3 + 1} M₀ˣ
s : Finset M₀
n : M₀
h : ∀ a ∈ s, Prime a
div : ∀ a ∈ s, a ∣ n
⊢ ∀ (a : M₀), Membership.mem (γ := Multiset M₀) (Multiset.map (fun (p : M₀) ↦ p) s.val) a → a ∣ n

Tactic:
simpa only [Multiset.map_id', Finset.mem_def] using div

Premises used: Multiset.map_id', Finset.mem_def
-- Module: Mathlib.Algebra.BigOperators.Associated
Goal:
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : IsCancelMulZero M₀
inst_2 : Subsingleton.{u_3 + 1} M₀ˣ
s : Finset M₀
n : M₀
h : ∀ a ∈ s, Prime a
div : ∀ a ∈ s, a ∣ n
⊢ ∀ (a : M₀), Multiset.countP (Associated a) (Multiset.map (fun (p : M₀) ↦ p) s.val) ≤ 1

Tactic:
simp only [Multiset.map_id', associated_eq_eq, Multiset.countP_eq_card_filter,
            ← s.val.count_eq_card_filter_eq, ← Multiset.nodup_iff_count_le_one, s.nodup]

Premises used: associated_eq_eq, Multiset.nodup_iff_count_le_one, Multiset.count_eq_card_filter_eq, Finset.nodup, Finset.val, Multiset.map_id', Multiset.countP_eq_card_filter
-- Module: Mathlib.Algebra.BigOperators.Associated
Goal:
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : IsCancelMulZero M₀
inst_2 : Subsingleton.{u_3 + 1} M₀ˣ
s : Finset M₀
n : M₀
h : ∀ a ∈ s, Prime a
div : ∀ a ∈ s, a ∣ n
⊢ ∏ p ∈ s, p ∣ n

Tactic:
exact
      Multiset.prod_primes_dvd n (by simpa only [Multiset.map_id', Finset.mem_def] using h)
        (by simpa only [Multiset.map_id', Finset.mem_def] using div)
        (by
          simp only [Multiset.map_id', associated_eq_eq, Multiset.countP_eq_card_filter,
            ← s.val.count_eq_card_filter_eq, ← Multiset.nodup_iff_count_le_one, s.nodup])

Premises used: Multiset.prod_primes_dvd
-- Module: Mathlib.Algebra.BigOperators.Associated
Goal:
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : IsCancelMulZero M₀
inst_2 : Subsingleton.{u_3 + 1} M₀ˣ
s : Finset M₀
n : M₀
h : ∀ a ∈ s, Prime a
div : ∀ a ∈ s, a ∣ n
⊢ ∏ p ∈ s, p ∣ n

Tactic:
classical
    exact
      Multiset.prod_primes_dvd n (by simpa only [Multiset.map_id', Finset.mem_def] using h)
        (by simpa only [Multiset.map_id', Finset.mem_def] using div)
        (by
          simp only [Multiset.map_id', associated_eq_eq, Multiset.countP_eq_card_filter,
            ← s.val.count_eq_card_filter_eq, ← Multiset.nodup_iff_count_le_one, s.nodup])
-- Module: Mathlib.Algebra.BigOperators.Associated
Goal:
M : Type u_2
inst : CommMonoid M
p : Multiset M
⊢ Eq.{u_2 + 1} (α := Associates M) (Multiset.prod (Multiset.map Associates.mk 0)) (Associates.mk (Multiset.prod 0))

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Associated
Goal:
M : Type u_2
inst : CommMonoid M
p : Multiset M
a : M
s : Multiset M
ih : Eq (α := Associates M) (Multiset.prod (Multiset.map Associates.mk s)) (Associates.mk s.prod)
⊢ Eq (α := Associates M) (Multiset.prod (Multiset.map Associates.mk (a ::ₘ s))) (Associates.mk (a ::ₘ s).prod)

Tactic:
simp [ih, Associates.mk_mul_mk]

Premises used: Associates.mk_mul_mk
-- Module: Mathlib.Algebra.BigOperators.Associated
Goal:
ι : Type u_1
M : Type u_2
inst : CommMonoid M
p : Finset ι
f : ι → M
rw :
  Eq.{u_2 + 1} (α := Associates M) (Multiset.prod (Multiset.map (fun (i : ι) ↦ Associates.mk (f i)) p.val))
    (Associates.mk (∏ i ∈ p, f i))
rw₁ : Eq (α := Associates M) (Multiset.prod (Multiset.map (Associates.mk ∘ f) p.val)) (Associates.mk (∏ i ∈ p, f i))
rw₂ :
  Eq (α := Associates M) (Multiset.prod (Multiset.map Associates.mk (Multiset.map f p.val)))
    (Associates.mk (∏ i ∈ p, f i))
rw₃ : Eq (α := Associates M) (Associates.mk (Multiset.map f p.val).prod) (Associates.mk (∏ i ∈ p, f i))
rw₄ rw₅ : Eq.{u_2 + 1} (α := Associates M) (Associates.mk (∏ x ∈ p, f x)) (Associates.mk (∏ i ∈ p, f i))
⊢ Eq.{u_2 + 1} (α := Associates M) (∏ i ∈ p, Associates.mk (f i)) (Associates.mk (∏ i ∈ p, f i))

Tactic:
rw [Finset.prod_eq_multiset_prod, ← Function.comp_def, ← Multiset.map_map, prod_mk,
    ← Finset.prod_eq_multiset_prod]

Premises used: Associates.prod_mk, Function.comp_def, Finset.prod_eq_multiset_prod, Multiset.map_map
-- Module: Mathlib.Algebra.BigOperators.Associated
Goal:
M : Type u_2
inst : CommMonoid M
p q : Multiset M
rw :
  Multiset.Rel Associated p q ↔
    Multiset.Rel (fun (a b : M) ↦ Eq (α := Associates M) (Associates.mk a) (Associates.mk b)) p q
⊢ Multiset.Rel Associated p q ↔
    Eq (α := Multiset (Associates M)) (Multiset.map Associates.mk p) (Multiset.map Associates.mk q)

Tactic:
rw [← Multiset.rel_eq, Multiset.rel_map]

Premises used: Multiset.rel_eq, Multiset.rel_map
-- Module: Mathlib.Algebra.BigOperators.Associated
Goal:
M : Type u_2
inst : CommMonoid M
p q : Multiset M
⊢ Multiset.Rel Associated p q ↔
    Multiset.Rel (fun (a b : M) ↦ Eq (α := Associates M) (Associates.mk a) (Associates.mk b)) p q

Tactic:
simp only [mk_eq_mk_iff_associated]

Premises used: Associates.mk_eq_mk_iff_associated
-- Module: Mathlib.Algebra.BigOperators.Associated
Goal:
M : Type u_2
inst : CommMonoid M
p : Multiset (Associates M)
⊢ Eq.{u_2 + 1} (α := Associates M) (Multiset.prod 0) 1 ↔
    ∀ (a : Associates M), Membership.mem (γ := Multiset (Associates M)) 0 a → a = 1

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Associated
Goal:
M : Type u_2
inst : CommMonoid M
p : Multiset (Associates M)
⊢ ∀ (a : Associates M) (s : Multiset (Associates M)),
    (s.prod = 1 ↔ ∀ a ∈ s, a = 1) → ((a ::ₘ s).prod = 1 ↔ ∀ a_2 ∈ a ::ₘ s, a_2 = 1)

Tactic:
simp +contextual [mul_eq_one, or_imp, forall_and]

Premises used: or_imp, mul_eq_one, forall_and
-- Module: Mathlib.Algebra.BigOperators.Associated
Goal:
M : Type u_2
inst : CommMonoid M
p q : Multiset (Associates M)
h : p ≤ q
haveI : ∀ (this : DecidableEq (Associates M)), p.prod ≤ q.prod
⊢ p.prod ≤ q.prod

Tactic:
haveI := Classical.decEq (Associates M)
-- Module: Mathlib.Algebra.BigOperators.Associated
Goal:
M : Type u_2
inst : CommMonoid M
p q : Multiset (Associates M)
h : p ≤ q
this_1 : DecidableEq (Associates M)
this : p.prod ≤ (p + (q - p)).prod
rwa rwa₁ rwa₂ rwa₃ : ∀ (this : p.prod ≤ q.prod), p.prod ≤ q.prod
⊢ p.prod ≤ q.prod

Tactic:
rwa [add_tsub_cancel_of_le h] at this

Premises used: add_tsub_cancel_of_le
-- Module: Mathlib.Algebra.BigOperators.Associated
Goal:
M : Type u_2
inst : CommMonoid M
p q : Multiset (Associates M)
h : p ≤ q
this : DecidableEq (Associates M)
suffices : p.prod ≤ (p + (q - p)).prod
⊢ p.prod ≤ q.prod

Tactic:
suffices p.prod ≤ (p + (q - p)).prod by rwa [add_tsub_cancel_of_le h] at this
-- Module: Mathlib.Algebra.BigOperators.Associated
Goal:
M : Type u_2
inst : CommMonoid M
p q : Multiset (Associates M)
h : p ≤ q
this_1 : DecidableEq (Associates M)
this : p.prod * 1 ≤ p.prod * (q - p).prod
⊢ p.prod ≤ (p + (q - p)).prod

Tactic:
simpa
-- Module: Mathlib.Algebra.BigOperators.Associated
Goal:
M : Type u_2
inst : CommMonoid M
p q : Multiset (Associates M)
h : p ≤ q
this : DecidableEq (Associates M)
suffices : p.prod * 1 ≤ p.prod * (q - p).prod
⊢ p.prod ≤ (p + (q - p)).prod

Tactic:
suffices p.prod * 1 ≤ p.prod * (q - p).prod by simpa
-- Module: Mathlib.Algebra.BigOperators.Associated
Goal:
M : Type u_2
inst : CommMonoid M
p q : Multiset (Associates M)
h : p ≤ q
this : DecidableEq (Associates M)
⊢ p.prod * 1 ≤ p.prod * (q - p).prod

Tactic:
mul_mono (le_refl p.prod) one_le

Premises used: le_refl, Multiset.prod, one_le, Associates.mul_mono
-- Module: Mathlib.Algebra.BigOperators.Associated
Goal:
M : Type u_2
inst : CommMonoid M
p q : Multiset (Associates M)
h : p ≤ q
this : DecidableEq (Associates M)
⊢ p.prod * 1 ≤ p.prod * (q - p).prod

Tactic:
exact mul_mono (le_refl p.prod) one_le

Premises used: le_refl, Multiset.prod, one_le, Associates.mul_mono
-- Module: Mathlib.Algebra.BigOperators.Associated
Goal:
M₀ : Type u_3
inst : CommMonoidWithZero M₀
s_1 : Multiset (Associates M₀)
p : Associates M₀
hp : Prime p
a : Associates M₀
s : Multiset (Associates M₀)
ih : p ≤ s.prod → ∃ a ∈ s, p ≤ a
h : p ≤ (a ::ₘ s).prod
⊢ p ≤ a * s.prod

Tactic:
simpa using h
-- Module: Mathlib.Algebra.BigOperators.Associated
Goal:
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : NoZeroDivisors M₀
inst_2 : Nontrivial M₀
s : Multiset M₀
h : ∀ x ∈ s, Prime x
⊢ s.prod ≠ 0

Tactic:
Multiset.prod_ne_zero fun h0 => Prime.ne_zero (h 0 h0) rfl

Premises used: Multiset.prod_ne_zero, Prime.ne_zero, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.BigOperators.Associated
Goal:
M₀ : Type u_3
M : Type u_4
inst : CommMonoidWithZero M
S : Finset M₀
p : M
pp : Prime p
g : M₀ → M
⊢ p ∣ S.prod g ↔ ∃ a ∈ S, p ∣ g a

Tactic:
⟨pp.exists_mem_finset_dvd, fun ⟨_, ha1, ha2⟩ => dvd_trans ha2 (dvd_prod_of_mem g ha1)⟩

Premises used: Dvd.dvd, Finset.dvd_prod_of_mem, Prime.exists_mem_finset_dvd, _private.0.Prime.dvd_finsetProd_iff.match_1, dvd_trans, Finset.prod, Iff.intro
-- Module: Mathlib.Algebra.BigOperators.Associated
Goal:
M₀ : Type u_3
M : Type u_4
inst : CommMonoidWithZero M
S : Finset M₀
p : M
pp : Prime p
g : M₀ → M
hS : ∀ a ∈ S, ¬p ∣ g a
⊢ ¬p ∣ S.prod g

Tactic:
mt (Prime.dvd_finsetProd_iff pp _).1 <| not_exists.2 fun a => not_and.2 (hS a)

Premises used: Iff.mpr, Prime.dvd_finsetProd_iff, not_exists, mt, Iff.mp, not_and
-- Module: Mathlib.Algebra.BigOperators.Associated
Goal:
M₀ : Type u_3
M : Type u_4
inst : CommMonoidWithZero M
S : Finset M₀
p : M
pp : Prime p
g : M₀ → M
hS : ∀ a ∈ S, ¬p ∣ g a
⊢ ¬p ∣ S.prod g

Tactic:
exact mt (Prime.dvd_finsetProd_iff pp _).1 <| not_exists.2 fun a => not_and.2 (hS a)

Premises used: Iff.mpr, Prime.dvd_finsetProd_iff, not_exists, mt, Iff.mp, not_and
-- Module: Mathlib.Algebra.BigOperators.Associated
Goal:
M₀ : Type u_3
M : Type u_4
inst : CommMonoidWithZero M
f : M₀ →₀ M
g : M₀ → M → ℕ
p : ℕ
pp : Prime p
⊢ p ∣ f.prod g ↔ ∃ a ∈ f.support, p ∣ g a ((f : (a : M₀) → M) a)

Tactic:
Prime.dvd_finsetProd_iff pp _

Premises used: Prime.dvd_finsetProd_iff, Finsupp.prod
-- Module: Mathlib.Algebra.BigOperators.Associated
Goal:
M₀ : Type u_3
M : Type u_4
inst : CommMonoidWithZero M
f : M₀ →₀ M
g : M₀ → M → ℕ
p : ℕ
pp : Prime p
hS : ∀ a ∈ f.support, ¬p ∣ g a ((f : (a : M₀) → M) a)
⊢ ¬p ∣ f.prod g

Tactic:
Prime.not_dvd_finsetProd pp hS

Premises used: Prime.not_dvd_finsetProd, Finsupp.prod
-- Module: Mathlib.Algebra.BigOperators.Balance
Goal:
ι : Type u_1
G : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup G
inst_2 : Module ℚ≥0 G
f : ι → G
x : ι
⊢ balance f x = f x - 𝔼 y : ι, f y

Tactic:
rfl

Premises used: Finset.expect, Fintype.balance, rfl
-- Module: Mathlib.Algebra.BigOperators.Balance
Goal:
ι : Type u_1
G : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup G
inst_2 : Module ℚ≥0 G
⊢ Eq (α := ι → G) (balance 0) 0

Tactic:
simp [balance]

Premises used: Fintype.balance
-- Module: Mathlib.Algebra.BigOperators.Balance
Goal:
ι : Type u_1
G : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup G
inst_2 : Module ℚ≥0 G
f g : ι → G
⊢ balance (f + g) = balance f + balance g

Tactic:
simp only [balance, expect_add_distrib, ← const_add, add_sub_add_comm, Pi.add_apply]

Premises used: Finset.expect_add_distrib, Fintype.balance, Pi.add_apply, Function.const_add, add_sub_add_comm
-- Module: Mathlib.Algebra.BigOperators.Balance
Goal:
ι : Type u_1
G : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup G
inst_2 : Module ℚ≥0 G
f g : ι → G
⊢ balance (f - g) = balance f - balance g

Tactic:
simp only [balance, expect_sub_distrib, const_sub, sub_sub_sub_comm, Pi.sub_apply]

Premises used: sub_sub_sub_comm, Finset.expect_sub_distrib, Fintype.balance, Function.const_sub, Pi.sub_apply
-- Module: Mathlib.Algebra.BigOperators.Balance
Goal:
ι : Type u_1
G : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup G
inst_2 : Module ℚ≥0 G
f : ι → G
⊢ balance (-f) = -balance f

Tactic:
simp only [balance, expect_neg_distrib, const_neg, neg_sub', Pi.neg_apply]

Premises used: Finset.expect_neg_distrib, Function.const_neg, Fintype.balance, neg_sub', Pi.neg_apply
-- Module: Mathlib.Algebra.BigOperators.Balance
Goal:
ι : Type u_1
G : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup G
inst_2 : Module ℚ≥0 G
f : ι → G
inl : IsEmpty ι → Eq.{u_4 + 1} (α := G) (∑ x : ι, balance f x) 0
inr : Nonempty ι → Eq.{u_4 + 1} (α := G) (∑ x : ι, balance f x) 0
⊢ Eq.{u_4 + 1} (α := G) (∑ x : ι, balance f x) 0

Tactic:
cases isEmpty_or_nonempty ι

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Algebra.BigOperators.Balance
Goal:
ι : Type u_1
G : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup G
inst_2 : Module ℚ≥0 G
f : ι → G
h : IsEmpty ι
⊢ Eq.{u_4 + 1} (α := G) (∑ x : ι, balance f x) 0

Tactic:
simp [balance_apply]

Premises used: Fintype.balance_apply
-- Module: Mathlib.Algebra.BigOperators.Balance
Goal:
ι : Type u_1
G : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup G
inst_2 : Module ℚ≥0 G
f : ι → G
h : Nonempty ι
⊢ Eq.{u_4 + 1} (α := G) (∑ x : ι, balance f x) 0

Tactic:
simp [balance_apply]

Premises used: Fintype.balance_apply
-- Module: Mathlib.Algebra.BigOperators.Balance
Goal:
ι : Type u_1
G : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup G
inst_2 : Module ℚ≥0 G
f : ι → G
⊢ Eq.{u_4 + 1} (α := G) (𝔼 x : ι, balance f x) 0

Tactic:
simp [expect]

Premises used: Finset.expect
-- Module: Mathlib.Algebra.BigOperators.Balance
Goal:
ι : Type u_1
G : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup G
inst_2 : Module ℚ≥0 G
f : ι → G
inl : IsEmpty ι → balance (balance f) = balance f
inr : Nonempty ι → balance (balance f) = balance f
⊢ balance (balance f) = balance f

Tactic:
cases isEmpty_or_nonempty ι

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Algebra.BigOperators.Balance
Goal:
ι : Type u_1
G : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup G
inst_2 : Module ℚ≥0 G
f : ι → G
h : IsEmpty ι
inl : ∀ (x : ι), balance (balance f) x = balance f x
⊢ balance (balance f) = balance f

Tactic:
ext x
-- Module: Mathlib.Algebra.BigOperators.Balance
Goal:
ι : Type u_1
G : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup G
inst_2 : Module ℚ≥0 G
f : ι → G
h : Nonempty ι
inr : ∀ (x : ι), balance (balance f) x = balance f x
⊢ balance (balance f) = balance f

Tactic:
ext x
-- Module: Mathlib.Algebra.BigOperators.Balance
Goal:
ι : Type u_1
G : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup G
inst_2 : Module ℚ≥0 G
f : ι → G
h : IsEmpty ι
x : ι
⊢ balance (balance f) x = balance f x

Tactic:
simp [balance, expect_sub_distrib, univ_nonempty]

Premises used: Finset.univ_nonempty, Finset.expect_sub_distrib, Fintype.balance
-- Module: Mathlib.Algebra.BigOperators.Balance
Goal:
ι : Type u_1
G : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup G
inst_2 : Module ℚ≥0 G
f : ι → G
h : Nonempty ι
x : ι
⊢ balance (balance f) x = balance f x

Tactic:
simp [balance, expect_sub_distrib, univ_nonempty]

Premises used: Finset.univ_nonempty, Finset.expect_sub_distrib, Fintype.balance
-- Module: Mathlib.Algebra.BigOperators.Balance
Goal:
ι : Type u_1
H : Type u_2
F : Type u_3
G : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup G
inst_2 : Module ℚ≥0 G
inst_3 : AddCommGroup H
inst_4 : Module ℚ≥0 H
inst_5 : FunLike F G H
inst_6 : LinearMapClass F ℚ≥0 G H
g : F
f : ι → G
a : ι
⊢ Eq.{u_2 + 1} (α := H) ((g : (a : G) → H) (balance f a) : H) (balance ((⇑g : (a : G) → H) ∘ f) a : H)

Tactic:
simp [balance, map_expect]

Premises used: Fintype.balance, map_expect
-- Module: Mathlib.Algebra.BigOperators.Expect
Goal:
ι : Type u_1
M : Type u_3
inst : AddCommMonoid M
inst_1 : Module ℚ≥0 M
f : ι → M
inst_2 : Fintype ι
rw :
  HSMul.hSMul (α := ℚ≥0) (β := M) (↑(card.{u_1} (α := ι) univ) : ℚ≥0)⁻¹ (∑ i : ι, f i) =
    HSMul.hSMul (α := ℚ≥0) (β := M) (↑(Fintype.card ι) : ℚ≥0)⁻¹ (∑ i : ι, f i)
rw₁ rw₂ :
  HSMul.hSMul (α := ℚ≥0) (β := M) (↑(Fintype.card ι) : ℚ≥0)⁻¹ (∑ i : ι, f i) =
    HSMul.hSMul (α := ℚ≥0) (β := M) (↑(Fintype.card ι) : ℚ≥0)⁻¹ (∑ i : ι, f i)
⊢ 𝔼 i : ι, f i = HSMul.hSMul (α := ℚ≥0) (β := M) (↑(Fintype.card ι) : ℚ≥0)⁻¹ (∑ i : ι, f i)

Tactic:
rw [expect, card_univ]

Premises used: Finset.card_univ, Finset.expect
-- Module: Mathlib.Algebra.BigOperators.Expect
Goal:
ι : Type u_1
M : Type u_3
inst : AddCommMonoid M
inst_1 : Module ℚ≥0 M
f : ι → M
⊢ Eq.{u_3 + 1} (α := M) (𝔼 i ∈ ∅, f i) 0

Tactic:
simp [expect]

Premises used: Finset.expect
-- Module: Mathlib.Algebra.BigOperators.Expect
Goal:
ι : Type u_1
M : Type u_3
inst : AddCommMonoid M
inst_1 : Module ℚ≥0 M
f : ι → M
i : ι
⊢ 𝔼 j ∈ {i}, f j = f i

Tactic:
simp [expect]

Premises used: Finset.expect
-- Module: Mathlib.Algebra.BigOperators.Expect
Goal:
ι : Type u_1
M : Type u_3
inst : AddCommMonoid M
inst_1 : Module ℚ≥0 M
s : Finset ι
⊢ Eq.{u_3 + 1} (α := M) (𝔼 _i ∈ s, 0) 0

Tactic:
simp [expect]

Premises used: Finset.expect
-- Module: Mathlib.Algebra.BigOperators.Expect
Goal:
ι : Type u_1
M : Type u_3
inst : AddCommMonoid M
inst_1 : Module ℚ≥0 M
s : Finset ι
f g : ι → M
t : Finset ι
hst : s = t
h : ∀ i ∈ t, f i = g i
rw : HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#s) : ℚ≥0)⁻¹ (∑ i ∈ s, f i) = 𝔼 i ∈ t, g i
rw₁ :
  HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#s) : ℚ≥0)⁻¹ (∑ i ∈ s, f i) =
    HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#t) : ℚ≥0)⁻¹ (∑ i ∈ t, g i)
rw₂ : HSMul.hSMul (α := ℚ≥0) (↑(#s) : ℚ≥0)⁻¹ (t.sum g) = HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#t) : ℚ≥0)⁻¹ (∑ i ∈ t, g i)
rw₃ rw₄ :
  HSMul.hSMul (α := ℚ≥0) (↑(#t) : ℚ≥0)⁻¹ (t.sum g) = HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#t) : ℚ≥0)⁻¹ (∑ i ∈ t, g i)
⊢ Eq.{u_3 + 1} (α := M) (𝔼 i ∈ s, f i) (𝔼 i ∈ t, g i)

Tactic:
rw [expect, expect, sum_congr hst h, hst]

Premises used: Finset.expect, Finset.sum_congr
-- Module: Mathlib.Algebra.BigOperators.Expect
Goal:
ι : Type u_1
M : Type u_3
inst : AddCommMonoid M
inst_1 : Module ℚ≥0 M
s t : Finset ι
f g : ι → M
p q : ι → Prop
inst_2 : DecidablePred p
inst_3 : DecidablePred q
hst : s = t
hpq : ∀ i ∈ t, p i ↔ q i
h : ∀ i ∈ t, q i → f i = g i
rw : {i ∈ t | p i} = {i ∈ t | q i}
rw₁ rw₂ : filter q t = {i ∈ t | q i}
⊢ {i ∈ s | p i} = {i ∈ t | q i}

Tactic:
rw [hst, filter_inj'.2 hpq]

Premises used: Iff.mpr, Finset.filter_inj'
-- Module: Mathlib.Algebra.BigOperators.Expect
Goal:
ι : Type u_1
M : Type u_3
inst : AddCommMonoid M
inst_1 : Module ℚ≥0 M
s t : Finset ι
f g : ι → M
p q : ι → Prop
inst_2 : DecidablePred p
inst_3 : DecidablePred q
hst : s = t
hpq : ∀ i ∈ t, p i ↔ q i
h : ∀ i ∈ t, q i → f i = g i
⊢ ∀ i ∈ {i ∈ t | q i}, f i = g i

Tactic:
simpa using h
-- Module: Mathlib.Algebra.BigOperators.Expect
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_3
inst : AddCommMonoid M
inst_1 : Module ℚ≥0 M
s : Finset ι
t : Finset κ
f : ι → κ → M
⊢ Eq.{u_3 + 1} (α := M) (𝔼 i ∈ s, ∑ j ∈ t, f i j) (∑ j ∈ t, 𝔼 i ∈ s, f i j)

Tactic:
simpa only [expect, smul_sum] using sum_comm

Premises used: Finset.expect, Finset.smul_sum, Finset.sum_comm