awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
rw : HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#s) : ℚ≥0)⁻¹ (∑ i ∈ s, 𝔼 j ∈ t, f i j) = 𝔼 j ∈ t, 𝔼 i ∈ s, f i j
rw₁ :
  HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#s) : ℚ≥0)⁻¹ (∑ i ∈ s, 𝔼 j ∈ t, f i j) =
    HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#t) : ℚ≥0)⁻¹ (∑ i ∈ t, 𝔼 i_1 ∈ s, f i_1 i)
rw₂ :
  HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#s) : ℚ≥0)⁻¹ (𝔼 i ∈ t, ∑ j ∈ s, f j i) =
    HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#t) : ℚ≥0)⁻¹ (∑ i ∈ t, 𝔼 i_1 ∈ s, f i_1 i)
rw₃ :
  HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#s) : ℚ≥0)⁻¹ (𝔼 i ∈ t, ∑ j ∈ s, f j i) =
    HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#t) : ℚ≥0)⁻¹ (𝔼 i ∈ s, ∑ j ∈ t, f i j)
rw₄ :
  HSMul.hSMul (α := ℚ≥0) (↑(#s) : ℚ≥0)⁻¹ (HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#t) : ℚ≥0)⁻¹ (∑ i ∈ t, ∑ j ∈ s, f j i)) =
    HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#t) : ℚ≥0)⁻¹ (𝔼 i ∈ s, ∑ j ∈ t, f i j)
rw₅ :
  HSMul.hSMul (α := ℚ≥0) (↑(#s) : ℚ≥0)⁻¹ (HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#t) : ℚ≥0)⁻¹ (∑ i ∈ t, ∑ j ∈ s, f j i)) =
    HSMul.hSMul (α := ℚ≥0) (↑(#t) : ℚ≥0)⁻¹ (HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#s) : ℚ≥0)⁻¹ (∑ i ∈ s, ∑ j ∈ t, f i j))
rw₆ :
  HSMul.hSMul (α := ℚ≥0) (↑(#t) : ℚ≥0)⁻¹ (HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#s) : ℚ≥0)⁻¹ (∑ i ∈ t, ∑ j ∈ s, f j i)) =
    HSMul.hSMul (α := ℚ≥0) (↑(#t) : ℚ≥0)⁻¹ (HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#s) : ℚ≥0)⁻¹ (∑ i ∈ s, ∑ j ∈ t, f i j))
rw₇ rw₈ :
  HSMul.hSMul (α := ℚ≥0) (↑(#t) : ℚ≥0)⁻¹ (HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#s) : ℚ≥0)⁻¹ (∑ y ∈ s, ∑ x ∈ t, f y x)) =
    HSMul.hSMul (α := ℚ≥0) (↑(#t) : ℚ≥0)⁻¹ (HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#s) : ℚ≥0)⁻¹ (∑ i ∈ s, ∑ j ∈ t, f i j))
⊢ Eq.{u_3 + 1} (α := M) (𝔼 i ∈ s, 𝔼 j ∈ t, f i j) (𝔼 j ∈ t, 𝔼 i ∈ s, f i j)

Tactic:
rw [expect, expect, ← expect_sum_comm, ← expect_sum_comm, expect, expect, smul_comm, sum_comm]

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

Tactic:
(expect_congr rfl h).trans s.expect_const_zero

Premises used: Finset.expect_congr, Finset.expect_const_zero, rfl, Eq.trans
-- Module: Mathlib.Algebra.BigOperators.Expect
Goal:
ι : Type u_1
M : Type u_3
inst : AddCommMonoid M
inst_1 : Module ℚ≥0 M
s : Finset ι
f : ι → M
h : Ne.{u_3 + 1} (α := M) (𝔼 i ∈ s, f i) 0
contrapose! : ∀ (h : ∀ (i : ι) (_ : i ∈ s), f i = 0), Eq.{u_3 + 1} (α := M) (𝔼 i ∈ s, f i) 0
⊢ ∃ i ∈ s, f i ≠ 0

Tactic:
contrapose! h
-- Module: Mathlib.Algebra.BigOperators.Expect
Goal:
ι : Type u_1
M : Type u_3
inst : AddCommMonoid M
inst_1 : Module ℚ≥0 M
s : Finset ι
f : ι → M
h : ∀ (i : ι) (_ : i ∈ s), f i = 0
⊢ Eq.{u_3 + 1} (α := M) (𝔼 i ∈ s, f i) 0

Tactic:
expect_eq_zero h

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

Tactic:
exact expect_eq_zero h

Premises used: Finset.expect_eq_zero
-- 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
⊢ 𝔼 i ∈ s, (f i + g i) = HAdd.hAdd (α := M) (𝔼 i ∈ s, f i) (𝔼 i ∈ s, g i)

Tactic:
simp [expect, sum_add_distrib]

Premises used: Finset.expect, Finset.sum_add_distrib
-- Module: Mathlib.Algebra.BigOperators.Expect
Goal:
ι : Type u_1
M : Type u_3
inst : AddCommMonoid M
inst_1 : Module ℚ≥0 M
s : Finset ι
f₁ f₂ g₁ g₂ : ι → M
simp_rw :
  HAdd.hAdd (α := M) (𝔼 i ∈ s, f₁ i) (𝔼 i ∈ s, f₂ i) + HAdd.hAdd (α := M) (𝔼 i ∈ s, g₁ i) (𝔼 i ∈ s, g₂ i) =
    HAdd.hAdd (α := M) (𝔼 i ∈ s, f₁ i) (𝔼 i ∈ s, g₁ i) + HAdd.hAdd (α := M) (𝔼 i ∈ s, f₂ i) (𝔼 i ∈ s, g₂ i)
⊢ HAdd.hAdd (α := M) (𝔼 i ∈ s, (f₁ i + f₂ i)) (𝔼 i ∈ s, (g₁ i + g₂ i)) =
    HAdd.hAdd (α := M) (𝔼 i ∈ s, (f₁ i + g₁ i)) (𝔼 i ∈ s, (f₂ i + g₂ i))

Tactic:
simp_rw [expect_add_distrib, add_add_add_comm]

Premises used: Finset.expect_add_distrib, add_add_add_comm
-- Module: Mathlib.Algebra.BigOperators.Expect
Goal:
ι : Type u_1
M : Type u_3
inst : AddCommMonoid M
inst_1 : Module ℚ≥0 M
s : Finset ι
f : ι → M
i : ι
hi : i ∈ s
h : ∀ j ∈ s, j ≠ i → f j = 0
rw : HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#s) : ℚ≥0)⁻¹ (∑ i ∈ s, f i) = HSMul.hSMul (α := ℚ≥0) (↑(#s) : ℚ≥0)⁻¹ (f i)
rw₁ rw₂ : HSMul.hSMul (α := ℚ≥0) (↑(#s) : ℚ≥0)⁻¹ (f i) = HSMul.hSMul (α := ℚ≥0) (↑(#s) : ℚ≥0)⁻¹ (f i)
⊢ 𝔼 i ∈ s, f i = HSMul.hSMul (α := ℚ≥0) (↑(#s) : ℚ≥0)⁻¹ (f i)

Tactic:
rw [expect, sum_eq_single_of_mem _ hi h]

Premises used: Finset.sum_eq_single_of_mem, 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 ι
p : ι → Prop
inst_2 : DecidablePred p
h : ∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j
a : M
pos : (∃ i ∈ s, p i) → (𝔼 i ∈ s, if p i then a else 0) = HSMul.hSMul (α := ℚ≥0) (↑(#s) : ℚ≥0)⁻¹ a
neg : (¬∃ i ∈ s, p i) → Eq.{u_3 + 1} (α := M) (𝔼 i ∈ s, if p i then a else 0) 0
⊢ (𝔼 i ∈ s, if p i then a else 0) = if ∃ i ∈ s, p i then HSMul.hSMul (α := ℚ≥0) (↑(#s) : ℚ≥0)⁻¹ a else 0

Tactic:
split_ifs
-- Module: Mathlib.Algebra.BigOperators.Expect
Goal:
ι : Type u_1
M : Type u_3
inst : AddCommMonoid M
inst_1 : Module ℚ≥0 M
s : Finset ι
p : ι → Prop
inst_2 : DecidablePred p
h : ∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j
a : M
h_1 : ∃ i ∈ s, p i
⊢ (𝔼 i ∈ s, if p i then a else 0) = HSMul.hSMul (α := ℚ≥0) (↑(#s) : ℚ≥0)⁻¹ a

Tactic:
simp [expect, sum_ite_zero _ _ h, *]

Premises used: Finset.expect, Finset.sum_ite_zero
-- Module: Mathlib.Algebra.BigOperators.Expect
Goal:
ι : Type u_1
M : Type u_3
inst : AddCommMonoid M
inst_1 : Module ℚ≥0 M
s : Finset ι
p : ι → Prop
inst_2 : DecidablePred p
h : ∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j
a : M
h_1 : ¬∃ i ∈ s, p i
⊢ Eq.{u_3 + 1} (α := M) (𝔼 i ∈ s, if p i then a else 0) 0

Tactic:
simp [expect, sum_ite_zero _ _ h, *]

Premises used: Finset.expect, Finset.sum_ite_zero
-- Module: Mathlib.Algebra.BigOperators.Expect
Goal:
ι : Type u_1
M : Type u_3
inst : AddCommMonoid M
inst_1 : Module ℚ≥0 M
inst_2 : DecidableEq ι
s t : Finset ι
f : ι → M
inl :
  ∀ (hst : s ∩ t = ∅),
    (𝔼 i ∈ s, if i ∈ t then f i else 0) =
      HSMul.hSMul (β := M) (HDiv.hDiv (α := ℚ≥0) (↑(#(s ∩ t)) : ℚ≥0) (↑(#s) : ℚ≥0)) (𝔼 i ∈ s ∩ t, f i)
inr :
  ∀ (hst : (s ∩ t).Nonempty),
    (𝔼 i ∈ s, if i ∈ t then f i else 0) =
      HSMul.hSMul (β := M) (HDiv.hDiv (α := ℚ≥0) (↑(#(s ∩ t)) : ℚ≥0) (↑(#s) : ℚ≥0)) (𝔼 i ∈ s ∩ t, f i)
⊢ (𝔼 i ∈ s, if i ∈ t then f i else 0) =
    HSMul.hSMul (β := M) (HDiv.hDiv (α := ℚ≥0) (↑(#(s ∩ t)) : ℚ≥0) (↑(#s) : ℚ≥0)) (𝔼 i ∈ s ∩ t, f i)

Tactic:
obtain hst | hst := (s ∩ t).eq_empty_or_nonempty

Premises used: Inter.inter, Finset.eq_empty_or_nonempty
-- Module: Mathlib.Algebra.BigOperators.Expect
Goal:
ι : Type u_1
M : Type u_3
inst : AddCommMonoid M
inst_1 : Module ℚ≥0 M
inst_2 : DecidableEq ι
s t : Finset ι
f : ι → M
hst : s ∩ t = ∅
⊢ (𝔼 i ∈ s, if i ∈ t then f i else 0) =
    HSMul.hSMul (β := M) (HDiv.hDiv (α := ℚ≥0) (↑(#(s ∩ t)) : ℚ≥0) (↑(#s) : ℚ≥0)) (𝔼 i ∈ s ∩ t, f i)

Tactic:
simp [expect, hst]

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
inst_2 : DecidableEq ι
s t : Finset ι
f : ι → M
hst : (s ∩ t).Nonempty
⊢ (𝔼 i ∈ s, if i ∈ t then f i else 0) =
    HSMul.hSMul (β := M) (HDiv.hDiv (α := ℚ≥0) (↑(#(s ∩ t)) : ℚ≥0) (↑(#s) : ℚ≥0)) (𝔼 i ∈ s ∩ t, f i)

Tactic:
simp [expect, smul_smul, ← inv_mul_eq_div, hst.card_ne_zero]

Premises used: Finset.expect, inv_mul_eq_div, smul_smul, Finset.Nonempty.card_ne_zero
-- Module: Mathlib.Algebra.BigOperators.Expect
Goal:
ι : Type u_1
M : Type u_3
inst : AddCommMonoid M
inst_1 : Module ℚ≥0 M
s : Finset ι
inst_2 : DecidableEq ι
i : ι
f : (j : ι) → i = j → M
pos : i ∈ s → (𝔼 j ∈ s, if h : i = j then f j h else 0) = HSMul.hSMul (α := ℚ≥0) (↑(#s) : ℚ≥0)⁻¹ (f i ⋯)
neg : i ∉ s → Eq.{u_3 + 1} (α := M) (𝔼 j ∈ s, if h : i = j then f j h else 0) 0
⊢ (𝔼 j ∈ s, if h : i = j then f j h else 0) = if i ∈ s then HSMul.hSMul (α := ℚ≥0) (↑(#s) : ℚ≥0)⁻¹ (f i ⋯) else 0

Tactic:
split_ifs
-- Module: Mathlib.Algebra.BigOperators.Expect
Goal:
ι : Type u_1
M : Type u_3
inst : AddCommMonoid M
inst_1 : Module ℚ≥0 M
s : Finset ι
inst_2 : DecidableEq ι
i : ι
f : (j : ι) → i = j → M
h : i ∈ s
⊢ (𝔼 j ∈ s, if h : i = j then f j h else 0) = HSMul.hSMul (α := ℚ≥0) (↑(#s) : ℚ≥0)⁻¹ (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 ι
inst_2 : DecidableEq ι
i : ι
f : (j : ι) → i = j → M
h : i ∉ s
⊢ Eq.{u_3 + 1} (α := M) (𝔼 j ∈ s, if h : i = j then f j h else 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 ι
inst_2 : DecidableEq ι
i : ι
f : (j : ι) → j = i → M
pos : i ∈ s → (𝔼 j ∈ s, if h : j = i then f j h else 0) = HSMul.hSMul (α := ℚ≥0) (↑(#s) : ℚ≥0)⁻¹ (f i ⋯)
neg : i ∉ s → Eq.{u_3 + 1} (α := M) (𝔼 j ∈ s, if h : j = i then f j h else 0) 0
⊢ (𝔼 j ∈ s, if h : j = i then f j h else 0) = if i ∈ s then HSMul.hSMul (α := ℚ≥0) (↑(#s) : ℚ≥0)⁻¹ (f i ⋯) else 0

Tactic:
split_ifs
-- Module: Mathlib.Algebra.BigOperators.Expect
Goal:
ι : Type u_1
M : Type u_3
inst : AddCommMonoid M
inst_1 : Module ℚ≥0 M
s : Finset ι
inst_2 : DecidableEq ι
i : ι
f : (j : ι) → j = i → M
h : i ∈ s
⊢ (𝔼 j ∈ s, if h : j = i then f j h else 0) = HSMul.hSMul (α := ℚ≥0) (↑(#s) : ℚ≥0)⁻¹ (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 ι
inst_2 : DecidableEq ι
i : ι
f : (j : ι) → j = i → M
h : i ∉ s
⊢ Eq.{u_3 + 1} (α := M) (𝔼 j ∈ s, if h : j = i then f j h else 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 ι
inst_2 : DecidableEq ι
i : ι
f : ι → M
pos : i ∈ s → (𝔼 j ∈ s, if i = j then f j else 0) = HSMul.hSMul (α := ℚ≥0) (↑(#s) : ℚ≥0)⁻¹ (f i)
neg : i ∉ s → Eq.{u_3 + 1} (α := M) (𝔼 j ∈ s, if i = j then f j else 0) 0
⊢ (𝔼 j ∈ s, if i = j then f j else 0) = if i ∈ s then HSMul.hSMul (α := ℚ≥0) (↑(#s) : ℚ≥0)⁻¹ (f i) else 0

Tactic:
split_ifs
-- Module: Mathlib.Algebra.BigOperators.Expect
Goal:
ι : Type u_1
M : Type u_3
inst : AddCommMonoid M
inst_1 : Module ℚ≥0 M
s : Finset ι
inst_2 : DecidableEq ι
i : ι
f : ι → M
h : i ∈ s
⊢ (𝔼 j ∈ s, if i = j then f j else 0) = HSMul.hSMul (α := ℚ≥0) (↑(#s) : ℚ≥0)⁻¹ (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 ι
inst_2 : DecidableEq ι
i : ι
f : ι → M
h : i ∉ s
⊢ Eq.{u_3 + 1} (α := M) (𝔼 j ∈ s, if i = j then f j else 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 ι
inst_2 : DecidableEq ι
i : ι
f : ι → M
pos : i ∈ s → (𝔼 j ∈ s, if j = i then f j else 0) = HSMul.hSMul (α := ℚ≥0) (↑(#s) : ℚ≥0)⁻¹ (f i)
neg : i ∉ s → Eq.{u_3 + 1} (α := M) (𝔼 j ∈ s, if j = i then f j else 0) 0
⊢ (𝔼 j ∈ s, if j = i then f j else 0) = if i ∈ s then HSMul.hSMul (α := ℚ≥0) (↑(#s) : ℚ≥0)⁻¹ (f i) else 0

Tactic:
split_ifs
-- Module: Mathlib.Algebra.BigOperators.Expect
Goal:
ι : Type u_1
M : Type u_3
inst : AddCommMonoid M
inst_1 : Module ℚ≥0 M
s : Finset ι
inst_2 : DecidableEq ι
i : ι
f : ι → M
h : i ∈ s
⊢ (𝔼 j ∈ s, if j = i then f j else 0) = HSMul.hSMul (α := ℚ≥0) (↑(#s) : ℚ≥0)⁻¹ (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 ι
inst_2 : DecidableEq ι
i : ι
f : ι → M
h : i ∉ s
⊢ Eq.{u_3 + 1} (α := M) (𝔼 j ∈ s, if j = i then f j else 0) 0

Tactic:
simp [expect, *]

Premises used: Finset.expect
-- 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 ι
f : ι → M
t : Finset κ
g : κ → M
i : (a : ι) → a ∈ s → κ
hi : ∀ (a : ι) (ha : a ∈ s), i a ha ∈ t
h : ∀ (a : ι) (ha : a ∈ s), f a = g (i a ha)
i_inj : ∀ (a₁ : ι) (ha₁ : a₁ ∈ s) (a₂ : ι) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ b ∈ t, ∃ (a : ι) (ha : a ∈ s), i a ha = b
simp_rw :
  HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#s) : ℚ≥0)⁻¹ (∑ x ∈ s, f x) =
    HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#t) : ℚ≥0)⁻¹ (∑ x ∈ t, g x)
simp_rw₁ :
  HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#t) : ℚ≥0)⁻¹ (∑ x ∈ s, f x) =
    HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#t) : ℚ≥0)⁻¹ (∑ x ∈ t, g x)
⊢ Eq.{u_3 + 1} (α := M) (𝔼 i ∈ s, f i) (𝔼 i ∈ t, g i)

Tactic:
simp_rw [expect, card_bij i hi i_inj i_surj, sum_bij i hi i_inj i_surj h]

Premises used: Finset.expect, Finset.sum_bij, Finset.card_bij
-- 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 ι
f : ι → M
t : Finset κ
g : κ → M
i : (a : ι) → a ∈ s → κ
j : (a : κ) → a ∈ t → ι
hi : ∀ (a : ι) (ha : a ∈ s), i a ha ∈ t
hj : ∀ (a : κ) (ha : a ∈ t), j a ha ∈ s
left_inv : ∀ (a : ι) (ha : a ∈ s), j (i a ha) ⋯ = a
right_inv : ∀ (a : κ) (ha : a ∈ t), i (j a ha) ⋯ = a
h : ∀ (a : ι) (ha : a ∈ s), f a = g (i a ha)
simp_rw :
  HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#s) : ℚ≥0)⁻¹ (∑ x ∈ s, f x) =
    HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#t) : ℚ≥0)⁻¹ (∑ x ∈ t, g x)
simp_rw₁ :
  HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#t) : ℚ≥0)⁻¹ (∑ x ∈ s, f x) =
    HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#t) : ℚ≥0)⁻¹ (∑ x ∈ t, g x)
⊢ Eq.{u_3 + 1} (α := M) (𝔼 i ∈ s, f i) (𝔼 i ∈ t, g i)

Tactic:
simp_rw [expect, card_bij' i j hi hj left_inv right_inv, sum_bij' i j hi hj left_inv right_inv h]

Premises used: Finset.expect, Finset.card_bij', Finset.sum_bij'
-- 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 ι
f : ι → M
t : Finset κ
g : κ → M
i : ι → κ
hi : ∀ a ∈ s, i a ∈ t
h : ∀ a ∈ s, f a = g (i a)
i_inj : Set.InjOn i (↑s : Set ι)
i_surj : Set.SurjOn i (↑s : Set ι) (↑t : Set κ)
simp_rw :
  HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#s) : ℚ≥0)⁻¹ (∑ x ∈ s, f x) =
    HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#t) : ℚ≥0)⁻¹ (∑ x ∈ t, g x)
simp_rw₁ :
  HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#t) : ℚ≥0)⁻¹ (∑ x ∈ s, f x) =
    HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#t) : ℚ≥0)⁻¹ (∑ x ∈ t, g x)
⊢ Eq.{u_3 + 1} (α := M) (𝔼 i ∈ s, f i) (𝔼 i ∈ t, g i)

Tactic:
simp_rw [expect, card_nbij i hi i_inj i_surj, sum_nbij i hi i_inj i_surj h]

Premises used: Finset.expect, Finset.sum_nbij, Finset.card_nbij
-- 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 ι
f : ι → M
t : Finset κ
g : κ → M
i : ι → κ
j : κ → ι
hi : ∀ a ∈ s, i a ∈ t
hj : ∀ a ∈ t, j a ∈ s
left_inv : ∀ a ∈ s, j (i a) = a
right_inv : ∀ a ∈ t, i (j a) = a
h : ∀ a ∈ s, f a = g (i a)
simp_rw :
  HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#s) : ℚ≥0)⁻¹ (∑ x ∈ s, f x) =
    HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#t) : ℚ≥0)⁻¹ (∑ x ∈ t, g x)
simp_rw₁ :
  HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#t) : ℚ≥0)⁻¹ (∑ x ∈ s, f x) =
    HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#t) : ℚ≥0)⁻¹ (∑ x ∈ t, g x)
⊢ Eq.{u_3 + 1} (α := M) (𝔼 i ∈ s, f i) (𝔼 i ∈ t, g i)

Tactic:
simp_rw [expect, card_nbij' i j hi hj left_inv right_inv,
    sum_nbij' i j hi hj left_inv right_inv h]

Premises used: Finset.expect, Finset.card_nbij', Finset.sum_nbij'
-- 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 ι
f : ι → M
t : Finset κ
g : κ → M
e : ι ≃ κ
hst : ∀ (i : ι), i ∈ s ↔ Membership.mem (α := κ) t ((e : (a : ι) → κ) i : κ)
hfg : ∀ i ∈ s, f i = g ((e : (a : ι) → κ) i)
simp_rw :
  HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#s) : ℚ≥0)⁻¹ (∑ x ∈ s, f x) =
    HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#t) : ℚ≥0)⁻¹ (∑ x ∈ t, g x)
simp_rw₁ :
  HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#t) : ℚ≥0)⁻¹ (∑ x ∈ s, f x) =
    HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#t) : ℚ≥0)⁻¹ (∑ x ∈ t, g x)
⊢ Eq.{u_3 + 1} (α := M) (𝔼 i ∈ s, f i) (𝔼 i ∈ t, g i)

Tactic:
simp_rw [expect, card_equiv e hst, sum_equiv e hst hfg]

Premises used: Finset.expect, Finset.card_equiv, Finset.sum_equiv
-- 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) (𝔼 x ∈ s ×ˢ t, f x) (𝔼 i ∈ s, 𝔼 j ∈ t, f (i, j))

Tactic:
simp only [expect, card_product, sum_product, smul_sum, mul_inv, mul_smul, Nat.cast_mul]

Premises used: Finset.expect, Finset.card_product, mul_inv, Nat.cast_mul, Finset.smul_sum, Finset.sum_product, SemigroupAction.mul_smul
-- 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 ×ˢ t, f i.1 i.2) (𝔼 i ∈ s, 𝔼 j ∈ t, f i j)

Tactic:
simp only [expect, card_product, sum_product', smul_sum, mul_inv, mul_smul, Nat.cast_mul]

Premises used: Finset.expect, Finset.card_product, mul_inv, Finset.sum_product', Nat.cast_mul, Finset.smul_sum, SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.BigOperators.Expect
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_3
inst : AddCommMonoid M
inst_1 : Module ℚ≥0 M
f : ι → M
t : Finset κ
inst_2 : DecidableEq ι
m : κ → ι
hm : Set.InjOn m (↑t : Set κ)
simp_rw :
  HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#(image m t)) : ℚ≥0)⁻¹ (∑ x ∈ image m t, f x) =
    HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#t) : ℚ≥0)⁻¹ (∑ x ∈ t, f (m x))
simp_rw₁ :
  HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#t) : ℚ≥0)⁻¹ (∑ x ∈ image m t, f x) =
    HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#t) : ℚ≥0)⁻¹ (∑ x ∈ t, f (m x))
⊢ Eq.{u_3 + 1} (α := M) (𝔼 i ∈ image m t, f i) (𝔼 i ∈ t, f (m i))

Tactic:
simp_rw [expect, card_image_of_injOn hm, sum_image hm]

Premises used: Finset.expect, Finset.card_image_of_injOn, Finset.sum_image
-- Module: Mathlib.Algebra.BigOperators.Expect
Goal:
ι : Type u_1
M : Type u_3
inst : AddCommMonoid M
inst_1 : Module ℚ≥0 M
inst_2 : DecidableEq ι
inst_3 : InvolutiveInv ι
s : Finset ι
f : ι → M
⊢ Eq.{u_3 + 1} (α := M) (𝔼 i ∈ s⁻¹, f i) (𝔼 i ∈ s, f i⁻¹)

Tactic:
expect_image inv_injective.injOn

Premises used: Function.Injective.injOn, Finset.expect_image, inv_injective
-- Module: Mathlib.Algebra.BigOperators.Expect
Goal:
ι : Type u_1
M : Type u_3
inst : AddCommMonoid M
inst_1 : Module ℚ≥0 M
inst_2 : DecidableEq ι
inst_3 : InvolutiveNeg ι
s : Finset ι
f : ι → M
⊢ Eq.{u_3 + 1} (α := M) (𝔼 i ∈ -s, f i) (𝔼 i ∈ s, f (-i))

Tactic:
expect_image neg_injective.injOn

Premises used: Function.Injective.injOn, Finset.expect_image, neg_injective
-- Module: Mathlib.Algebra.BigOperators.Expect
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommMonoid M
inst_1 : Module ℚ≥0 M
inst_2 : AddCommMonoid N
inst_3 : Module ℚ≥0 N
F : Type u_5
inst_4 : FunLike F M N
inst_5 : LinearMapClass F ℚ≥0 M N
g : F
f : ι → M
s : Finset ι
⊢ Eq.{u_4 + 1} (α := N) ((g : (a : M) → N) (𝔼 i ∈ s, f i) : N) (𝔼 i ∈ s, (g : (a : M) → N) (f i) : N)

Tactic:
simp only [expect, map_smul, map_sum]

Premises used: Finset.expect, map_sum, map_smul
-- Module: Mathlib.Algebra.BigOperators.Expect
Goal:
ι : Type u_1
M : Type u_3
inst : AddCommMonoid M
inst_1 : Module ℚ≥0 M
inst_2 : Fintype ι
f : ι → M
⊢ HSMul.hSMul (β := M) (Fintype.card ι) (𝔼 i : ι, f i) = ∑ i : ι, f i

Tactic:
Finset.card_smul_expect _ _

Premises used: Finset.card_smul_expect, Fintype.card
-- Module: Mathlib.Algebra.BigOperators.Expect
Goal:
ι : Type u_1
M : Type u_3
inst : AddCommMonoid M
inst_1 : Module ℚ≥0 M
s : Finset ι
hs : s.Nonempty
a : M
ha : Ne (α := ℚ≥0) (↑(#s) : ℚ≥0) 0
⊢ 𝔼 _i ∈ s, a = a

Tactic:
rw [expect, sum_const, ← Nat.cast_smul_eq_nsmul ℚ≥0, inv_smul_smul₀]

Premises used: inv_smul_smul₀, Finset.expect, NNRat, Nat.cast_smul_eq_nsmul, Finset.sum_const
-- Module: Mathlib.Algebra.BigOperators.Expect
Goal:
ι : Type u_1
M : Type u_3
inst : AddCommMonoid M
inst_1 : Module ℚ≥0 M
s : Finset ι
hs : s.Nonempty
a : M
⊢ Ne (α := ℚ≥0) (↑(#s) : ℚ≥0) 0

Tactic:
mod_cast hs.card_ne_zero

Premises used: congrArg, cast, Ne, Nat.cast, Finset.card, Finset.Nonempty.card_ne_zero, Nat.cast_inj._simp_1, Nat.cast_zero, Eq.symm, Not, Eq.trans
-- Module: Mathlib.Algebra.BigOperators.Expect
Goal:
ι : Type u_1
M : Type u_3
inst : AddCommMonoid M
inst_1 : Module ℚ≥0 M
s : Finset ι
hs : s.Nonempty
a : M
⊢ Ne (α := ℚ≥0) (↑(#s) : ℚ≥0) 0

Tactic:
exact mod_cast hs.card_ne_zero

Premises used: Finset.Nonempty.card_ne_zero
-- Module: Mathlib.Algebra.BigOperators.Expect
Goal:
ι : Type u_1
M : Type u_3
inst : AddCommMonoid M
inst_1 : Module ℚ≥0 M
G : Type u_5
inst_2 : DistribSMul G M
inst_3 : SMulCommClass G ℚ≥0 M
a : G
s : Finset ι
f : ι → M
⊢ HSMul.hSMul (β := M) a (𝔼 i ∈ s, f i) = 𝔼 i ∈ s, a • f i

Tactic:
simp only [expect, smul_sum, smul_comm]

Premises used: Finset.expect, Finset.smul_sum, SMulCommClass.smul_comm
-- Module: Mathlib.Algebra.BigOperators.Expect
Goal:
ι : Type u_1
M : Type u_3
inst : AddCommGroup M
inst_1 : Module ℚ≥0 M
s : Finset ι
f g : ι → M
⊢ 𝔼 i ∈ s, (f i - g i) = HSub.hSub (α := M) (𝔼 i ∈ s, f i) (𝔼 i ∈ s, g i)

Tactic:
simp only [expect, sum_sub_distrib, smul_sub]

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

Tactic:
simp [expect]

Premises used: Finset.expect
-- Module: Mathlib.Algebra.BigOperators.Expect
Goal:
ι : Type u_1
M : Type u_3
inst : Semiring M
inst_1 : Module ℚ≥0 M
s : Finset ι
f : ι → M
rw : HSMul.hSMul (β := M) (#s) (𝔼 i ∈ s, f i) = ∑ i ∈ s, f i
rw₁ rw₂ : Eq.{u_3 + 1} (α := M) (∑ i ∈ s, f i) (∑ i ∈ s, f i)
⊢ HMul.hMul (α := M) (↑(#s) : M) (𝔼 i ∈ s, f i) = ∑ i ∈ s, f i

Tactic:
rw [← nsmul_eq_mul, card_smul_expect]

Premises used: Finset.card_smul_expect, nsmul_eq_mul
-- Module: Mathlib.Algebra.BigOperators.Expect
Goal:
ι : Type u_1
M : Type u_3
inst : Semiring M
inst_1 : Module ℚ≥0 M
inst_2 : Fintype ι
f : ι → M
⊢ HMul.hMul (α := M) (↑(Fintype.card ι) : M) (𝔼 i : ι, f i) = ∑ i : ι, f i

Tactic:
Finset.card_mul_expect _ _

Premises used: Finset.card_mul_expect, Fintype.card
-- Module: Mathlib.Algebra.BigOperators.Expect
Goal:
ι : Type u_1
M : Type u_3
inst : Semiring M
inst_1 : Module ℚ≥0 M
inst_2 : IsScalarTower ℚ≥0 M M
s : Finset ι
f : ι → M
a : M
rw : HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#s) : ℚ≥0)⁻¹ (∑ i ∈ s, f i) * a = 𝔼 i ∈ s, f i * a
rw₁ :
  HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#s) : ℚ≥0)⁻¹ (∑ i ∈ s, f i) * a =
    HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#s) : ℚ≥0)⁻¹ (∑ i ∈ s, f i * a)
rw₂ :
  HSMul.hSMul (α := ℚ≥0) (↑(#s) : ℚ≥0)⁻¹ ((∑ i ∈ s, f i) * a) =
    HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#s) : ℚ≥0)⁻¹ (∑ i ∈ s, f i * a)
rw₃ rw₄ :
  HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#s) : ℚ≥0)⁻¹ (∑ i ∈ s, f i * a) =
    HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#s) : ℚ≥0)⁻¹ (∑ i ∈ s, f i * a)
⊢ (𝔼 i ∈ s, f i) * a = 𝔼 i ∈ s, f i * a

Tactic:
rw [expect, expect, smul_mul_assoc, sum_mul]

Premises used: Finset.expect, smul_mul_assoc, Finset.sum_mul