awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.BigOperators.Expect
Goal:
ι : Type u_1
M : Type u_3
inst : Semiring M
inst_1 : Module ℚ≥0 M
inst_2 : SMulCommClass ℚ≥0 M M
s : Finset ι
f : ι → M
a : M
rw : a * HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#s) : ℚ≥0)⁻¹ (∑ i ∈ s, f i) = 𝔼 i ∈ s, a * f i
rw₁ :
  a * HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#s) : ℚ≥0)⁻¹ (∑ i ∈ s, f i) =
    HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#s) : ℚ≥0)⁻¹ (∑ i ∈ s, a * f i)
rw₂ :
  HSMul.hSMul (α := ℚ≥0) (↑(#s) : ℚ≥0)⁻¹ (a * ∑ i ∈ s, f i) =
    HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#s) : ℚ≥0)⁻¹ (∑ i ∈ s, a * f i)
rw₃ rw₄ :
  HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#s) : ℚ≥0)⁻¹ (∑ i ∈ s, a * f i) =
    HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#s) : ℚ≥0)⁻¹ (∑ i ∈ s, a * f i)
⊢ a * 𝔼 i ∈ s, f i = 𝔼 i ∈ s, a * f i

Tactic:
rw [expect, expect, mul_smul_comm, mul_sum]

Premises used: Finset.mul_sum, Finset.expect, mul_smul_comm
-- Module: Mathlib.Algebra.BigOperators.Expect
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_3
inst : Semiring M
inst_1 : Module ℚ≥0 M
inst_2 : IsScalarTower ℚ≥0 M M
inst_3 : SMulCommClass ℚ≥0 M M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
simp_rw : Eq.{u_3 + 1} (α := M) (𝔼 i ∈ s, f i * 𝔼 j ∈ t, g j) (𝔼 i ∈ s, 𝔼 j ∈ t, f i * g j)
⊢ HMul.hMul (α := M) (𝔼 i ∈ s, f i) (𝔼 j ∈ t, g j) = 𝔼 i ∈ s, 𝔼 j ∈ t, f i * g j

Tactic:
simp_rw [expect_mul, mul_expect]

Premises used: Finset.expect_mul, Finset.mul_expect
-- Module: Mathlib.Algebra.BigOperators.Expect
Goal:
ι : Type u_1
M : Type u_3
inst : CommSemiring M
inst_1 : Module ℚ≥0 M
inst_2 : IsScalarTower ℚ≥0 M M
inst_3 : SMulCommClass ℚ≥0 M M
s : Finset ι
f : ι → M
n : ℕ
rw :
  HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#s) : ℚ≥0)⁻¹ (∑ i ∈ s, f i) ^ n =
    𝔼 p ∈ Fintype.piFinset (δ := fun (x : Fin n) ↦ ι) fun (x : Fin n) ↦ s, ∏ i : Fin n, f (p i)
rw₁ :
  HPow.hPow (α := ℚ≥0) (↑(#s) : ℚ≥0)⁻¹ n • HPow.hPow (α := M) (∑ i ∈ s, f i) n =
    𝔼 p ∈ Fintype.piFinset (δ := fun (x : Fin n) ↦ ι) fun (x : Fin n) ↦ s, ∏ i : Fin n, f (p i)
rw₂ :
  HSMul.hSMul (β := M) (HPow.hPow (α := ℚ≥0) (↑(#s) : ℚ≥0)⁻¹ n)
      (∑ p ∈ Fintype.piFinset (δ := fun (_i : Fin n) ↦ ι) fun (_i : Fin n) ↦ s, ∏ i : Fin n, f (p i)) =
    𝔼 p ∈ Fintype.piFinset (δ := fun (x : Fin n) ↦ ι) fun (x : Fin n) ↦ s, ∏ i : Fin n, f (p i)
rw₃ :
  HSMul.hSMul (β := M) (HPow.hPow (α := ℚ≥0) (↑(#s) : ℚ≥0)⁻¹ n)
      (∑ p ∈ Fintype.piFinset (δ := fun (_i : Fin n) ↦ ι) fun (_i : Fin n) ↦ s, ∏ i : Fin n, f (p i)) =
    HSMul.hSMul (α := ℚ≥0) (β := M)
      (↑(card.{u_1} (α := (a : Fin n) → ι) (Fintype.piFinset (δ := fun (x : Fin n) ↦ ι) fun (x : Fin n) ↦ s)) : ℚ≥0)⁻¹
      (∑ i ∈ Fintype.piFinset (δ := fun (x : Fin n) ↦ ι) fun (x : Fin n) ↦ s, ∏ i_1 : Fin n, f (i i_1))
rw₄ :
  HSMul.hSMul (β := M) (HPow.hPow (α := ℚ≥0) (↑(#s) : ℚ≥0)⁻¹ n)
      (∑ p ∈ Fintype.piFinset (δ := fun (_i : Fin n) ↦ ι) fun (_i : Fin n) ↦ s, ∏ i : Fin n, f (p i)) =
    HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#s ^ n) : ℚ≥0)⁻¹
      (∑ i ∈ Fintype.piFinset (δ := fun (x : Fin n) ↦ ι) fun (x : Fin n) ↦ s, ∏ i_1 : Fin n, f (i i_1))
rw₅ :
  HSMul.hSMul (β := M) (HPow.hPow (α := ℚ≥0) (↑(#s) : ℚ≥0) n)⁻¹
      (∑ p ∈ Fintype.piFinset (δ := fun (_i : Fin n) ↦ ι) fun (_i : Fin n) ↦ s, ∏ i : Fin n, f (p i)) =
    HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#s ^ n) : ℚ≥0)⁻¹
      (∑ i ∈ Fintype.piFinset (δ := fun (x : Fin n) ↦ ι) fun (x : Fin n) ↦ s, ∏ i_1 : Fin n, f (i i_1))
rw₆ rw₇ :
  HSMul.hSMul (β := M) (HPow.hPow (α := ℚ≥0) (↑(#s) : ℚ≥0) n)⁻¹
      (∑ p ∈ Fintype.piFinset (δ := fun (_i : Fin n) ↦ ι) fun (_i : Fin n) ↦ s, ∏ i : Fin n, f (p i)) =
    HSMul.hSMul (β := M) (HPow.hPow (α := ℚ≥0) (↑(#s) : ℚ≥0) n)⁻¹
      (∑ i ∈ Fintype.piFinset (δ := fun (x : Fin n) ↦ ι) fun (x : Fin n) ↦ s, ∏ i_1 : Fin n, f (i i_1))
⊢ HPow.hPow (α := M) (𝔼 i ∈ s, f i) n =
    𝔼 p ∈ Fintype.piFinset (δ := fun (x : Fin n) ↦ ι) fun (x : Fin n) ↦ s, ∏ i : Fin n, f (p i)

Tactic:
rw [expect, smul_pow, sum_pow', expect, Fintype.card_piFinset_const, inv_pow, Nat.cast_pow]

Premises used: Finset.expect, Fintype.card_piFinset_const, inv_pow, smul_pow, Nat.cast_pow, Finset.sum_pow'
-- Module: Mathlib.Algebra.BigOperators.Expect
Goal:
ι : Type u_1
M : Type u_3
inst : CommSemiring M
inst_1 : Module ℚ≥0 M
inst_2 : IsScalarTower ℚ≥0 M M
inst_3 : SMulCommClass ℚ≥0 M M
s : Finset ι
f : ι → M
n : ℕ
rw :
  HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#s) : ℚ≥0)⁻¹ (∑ i ∈ s, f i) ^ n =
    𝔼 p ∈ Fintype.piFinset (δ := fun (x : Fin n) ↦ ι) fun (x : Fin n) ↦ s, ∏ i : Fin n, f (p i)
rw₁ :
  HPow.hPow (α := ℚ≥0) (↑(#s) : ℚ≥0)⁻¹ n • HPow.hPow (α := M) (∑ i ∈ s, f i) n =
    𝔼 p ∈ Fintype.piFinset (δ := fun (x : Fin n) ↦ ι) fun (x : Fin n) ↦ s, ∏ i : Fin n, f (p i)
rw₂ :
  HSMul.hSMul (β := M) (HPow.hPow (α := ℚ≥0) (↑(#s) : ℚ≥0)⁻¹ n)
      (∑ p ∈ Fintype.piFinset (δ := fun (_i : Fin n) ↦ ι) fun (_i : Fin n) ↦ s, ∏ i : Fin n, f (p i)) =
    𝔼 p ∈ Fintype.piFinset (δ := fun (x : Fin n) ↦ ι) fun (x : Fin n) ↦ s, ∏ i : Fin n, f (p i)
rw₃ :
  HSMul.hSMul (β := M) (HPow.hPow (α := ℚ≥0) (↑(#s) : ℚ≥0)⁻¹ n)
      (∑ p ∈ Fintype.piFinset (δ := fun (_i : Fin n) ↦ ι) fun (_i : Fin n) ↦ s, ∏ i : Fin n, f (p i)) =
    HSMul.hSMul (α := ℚ≥0) (β := M)
      (↑(card.{u_1} (α := (a : Fin n) → ι) (Fintype.piFinset (δ := fun (x : Fin n) ↦ ι) fun (x : Fin n) ↦ s)) : ℚ≥0)⁻¹
      (∑ i ∈ Fintype.piFinset (δ := fun (x : Fin n) ↦ ι) fun (x : Fin n) ↦ s, ∏ i_1 : Fin n, f (i i_1))
rw₄ :
  HSMul.hSMul (β := M) (HPow.hPow (α := ℚ≥0) (↑(#s) : ℚ≥0)⁻¹ n)
      (∑ p ∈ Fintype.piFinset (δ := fun (_i : Fin n) ↦ ι) fun (_i : Fin n) ↦ s, ∏ i : Fin n, f (p i)) =
    HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#s ^ n) : ℚ≥0)⁻¹
      (∑ i ∈ Fintype.piFinset (δ := fun (x : Fin n) ↦ ι) fun (x : Fin n) ↦ s, ∏ i_1 : Fin n, f (i i_1))
rw₅ :
  HSMul.hSMul (β := M) (HPow.hPow (α := ℚ≥0) (↑(#s) : ℚ≥0) n)⁻¹
      (∑ p ∈ Fintype.piFinset (δ := fun (_i : Fin n) ↦ ι) fun (_i : Fin n) ↦ s, ∏ i : Fin n, f (p i)) =
    HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#s ^ n) : ℚ≥0)⁻¹
      (∑ i ∈ Fintype.piFinset (δ := fun (x : Fin n) ↦ ι) fun (x : Fin n) ↦ s, ∏ i_1 : Fin n, f (i i_1))
rw₆ rw₇ :
  HSMul.hSMul (β := M) (HPow.hPow (α := ℚ≥0) (↑(#s) : ℚ≥0) n)⁻¹
      (∑ p ∈ Fintype.piFinset (δ := fun (_i : Fin n) ↦ ι) fun (_i : Fin n) ↦ s, ∏ i : Fin n, f (p i)) =
    HSMul.hSMul (β := M) (HPow.hPow (α := ℚ≥0) (↑(#s) : ℚ≥0) n)⁻¹
      (∑ i ∈ Fintype.piFinset (δ := fun (x : Fin n) ↦ ι) fun (x : Fin n) ↦ s, ∏ i_1 : Fin n, f (i i_1))
⊢ HPow.hPow (α := M) (𝔼 i ∈ s, f i) n =
    𝔼 p ∈ Fintype.piFinset (δ := fun (x : Fin n) ↦ ι) fun (x : Fin n) ↦ s, ∏ i : Fin n, f (p i)

Tactic:
classical
  rw [expect, smul_pow, sum_pow', expect, Fintype.card_piFinset_const, inv_pow, Nat.cast_pow]

Premises used: Finset.expect, Fintype.card_piFinset_const, inv_pow, smul_pow, Nat.cast_pow, Finset.sum_pow'
-- Module: Mathlib.Algebra.BigOperators.Expect
Goal:
ι : Type u_1
M : Type u_3
inst : Semifield M
inst_1 : CharZero M
inst_2 : Fintype ι
inst_3 : Nonempty ι
inst_4 : DecidableEq ι
f : ι → M
i : ι
simp_rw : HSMul.hSMul (α := ℚ≥0) (↑(Fintype.card ι) : ℚ≥0)⁻¹ ((↑(Fintype.card ι) : M) * f i) = f i
⊢ 𝔼 j : ι, (if i = j then (↑(Fintype.card ι) : M) else 0) * f j = f i

Tactic:
simp_rw [expect_univ, ite_mul, zero_mul, sum_ite_eq, if_pos (mem_univ _)]

Premises used: Finset.mem_univ, MulZeroClass.zero_mul, if_pos, ite_mul, Finset.expect_univ, Finset.sum_ite_eq
-- Module: Mathlib.Algebra.BigOperators.Expect
Goal:
ι : Type u_1
M : Type u_3
inst : Semifield M
inst_1 : CharZero M
inst_2 : Fintype ι
inst_3 : Nonempty ι
inst_4 : DecidableEq ι
f : ι → M
i : ι
ha : Ne (α := ℚ≥0) (↑(Fintype.card ι) : ℚ≥0) 0
⊢ HSMul.hSMul (α := ℚ≥0) (↑(Fintype.card ι) : ℚ≥0)⁻¹ ((↑(Fintype.card ι) : M) * f i) = f i

Tactic:
rw [← @NNRat.cast_natCast M, ← NNRat.smul_def, inv_smul_smul₀]

Premises used: inv_smul_smul₀, NNRat.cast_natCast, NNRat.smul_def
-- Module: Mathlib.Algebra.BigOperators.Expect
Goal:
ι : Type u_1
M : Type u_3
inst : Semifield M
inst_1 : CharZero M
inst_2 : Fintype ι
inst_3 : Nonempty ι
inst_4 : DecidableEq ι
f : ι → M
i : ι
⊢ Ne (α := ℚ≥0) (↑(Fintype.card ι) : ℚ≥0) 0

Tactic:
simp [Fintype.card_ne_zero]

Premises used: Fintype.card_ne_zero
-- Module: Mathlib.Algebra.BigOperators.Expect
Goal:
ι : Type u_1
M : Type u_3
inst : Semifield M
inst_1 : CharZero M
inst_2 : Fintype ι
inst_3 : Nonempty ι
inst_4 : DecidableEq ι
f : ι → M
i : ι
simp_rw : 𝔼 i_1 : ι, (if i = i_1 then (↑(Fintype.card ι) : M) else 0) * f i_1 = f i
⊢ 𝔼 j : ι, (if j = i then (↑(Fintype.card ι) : M) else 0) * f j = f i

Tactic:
simp_rw [@eq_comm _ _ i, expect_boole_mul]

Premises used: eq_comm, Finset.expect_boole_mul
-- Module: Mathlib.Algebra.BigOperators.Expect
Goal:
ι : Type u_1
M : Type u_3
inst : Semifield M
inst_1 : CharZero M
s : Finset ι
f : ι → M
rw : HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#s) : ℚ≥0)⁻¹ (∑ i ∈ s, f i) = HDiv.hDiv (α := M) (∑ i ∈ s, f i) (↑(#s) : M)
rw₁ : HMul.hMul (α := M) (↑(↑(#s) : ℚ≥0)⁻¹ : M) (∑ i ∈ s, f i) = HDiv.hDiv (α := M) (∑ i ∈ s, f i) (↑(#s) : M)
rw₂ : HMul.hMul (α := M) (↑(↑(#s) : ℚ≥0)⁻¹ : M) (∑ i ∈ s, f i) = HMul.hMul (α := M) (↑(#s) : M)⁻¹ (∑ i ∈ s, f i)
rw₃ : HMul.hMul (α := M) (↑(↑(#s) : ℚ≥0) : M)⁻¹ (∑ i ∈ s, f i) = HMul.hMul (α := M) (↑(#s) : M)⁻¹ (∑ i ∈ s, f i)
rw₄ rw₅ : HMul.hMul (α := M) (↑(#s) : M)⁻¹ (∑ i ∈ s, f i) = HMul.hMul (α := M) (↑(#s) : M)⁻¹ (∑ i ∈ s, f i)
⊢ 𝔼 i ∈ s, f i = HDiv.hDiv (α := M) (∑ i ∈ s, f i) (↑(#s) : M)

Tactic:
rw [expect, NNRat.smul_def, div_eq_inv_mul, NNRat.cast_inv, NNRat.cast_natCast]

Premises used: Finset.expect, NNRat.cast_inv, div_eq_inv_mul, NNRat.cast_natCast, NNRat.smul_def
-- Module: Mathlib.Algebra.BigOperators.Expect
Goal:
ι : Type u_1
M : Type u_3
inst : Semifield M
inst_1 : CharZero M
inst_2 : Fintype ι
f : ι → M
⊢ 𝔼 i : ι, f i = HDiv.hDiv (α := M) (∑ i : ι, f i) (↑(Fintype.card ι) : M)

Tactic:
Finset.expect_eq_sum_div_card _ _

Premises used: Fintype.card, Finset.expect_eq_sum_div_card
-- Module: Mathlib.Algebra.BigOperators.Expect
Goal:
ι : Type u_1
M : Type u_3
inst : Semifield M
inst_1 : CharZero M
s : Finset ι
f : ι → M
a : M
simp_rw : (𝔼 i ∈ s, f i) * a⁻¹ = 𝔼 i ∈ s, f i * a⁻¹
⊢ (𝔼 i ∈ s, f i) / a = 𝔼 i ∈ s, f i / a

Tactic:
simp_rw [div_eq_mul_inv, expect_mul]

Premises used: Finset.expect_mul, div_eq_mul_inv
-- Module: Mathlib.Algebra.BigOperators.Expect
Goal:
ι : Type u_1
α : Type u_5
π : α → Type u_6
inst : (a : α) → CommSemiring (π a)
inst_1 : (a : α) → Module ℚ≥0 (π a)
s : Finset ι
f : ι → (a : α) → π a
a : α
⊢ Eq.{u_6 + 1} (α := π a) ((𝔼 i ∈ s, f i) a) (𝔼 i ∈ s, f i a)

Tactic:
simp [expect]

Premises used: Finset.expect
-- Module: Mathlib.Algebra.BigOperators.Expect
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : Semifield M
inst_1 : CharZero M
inst_2 : Semifield N
inst_3 : CharZero N
inst_4 : Algebra M N
s : Finset ι
f : ι → M
⊢ Eq.{u_4 + 1} (α := N) (↑(𝔼 i ∈ s, f i) : N) (𝔼 i ∈ s, (↑(f i) : N))

Tactic:
map_expect (algebraMap _ _) _ _

Premises used: Algebra.algebraMap, map_expect
-- Module: Mathlib.Algebra.BigOperators.Expect
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_3
inst : Fintype ι
inst_1 : Fintype κ
inst_2 : AddCommMonoid M
inst_3 : Module ℚ≥0 M
e : ι → κ
he : Bijective e
f : ι → M
g : κ → M
h : ∀ (i : ι), f i = g (e i)
⊢ Set.SurjOn e (↑univ : Set ι) (↑univ : Set κ)

Tactic:
simpa using he.surjective

Premises used: Function.Bijective.surjective
-- Module: Mathlib.Algebra.BigOperators.Expect
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_3
inst : Fintype ι
inst_1 : Fintype κ
inst_2 : AddCommMonoid M
inst_3 : Module ℚ≥0 M
e : ι ≃ κ
f : ι → M
g : κ → M
h : ∀ (i : ι), f i = g ((e : (a : ι) → κ) i)
⊢ Eq.{u_3 + 1} (α := M) (𝔼 i : ι, f i) (𝔼 i : κ, g i)

Tactic:
expect_bijective _ e.bijective f g h

Premises used: Equiv.bijective, Fintype.expect_bijective
-- Module: Mathlib.Algebra.BigOperators.Expect
Goal:
ι : Type u_1
M : Type u_3
inst : Fintype ι
inst_1 : AddCommMonoid M
inst_2 : Module ℚ≥0 M
inst_3 : Nonempty ι
a : M
⊢ 𝔼 _i : ι, a = a

Tactic:
Finset.expect_const univ_nonempty _

Premises used: Finset.expect_const, Finset.univ_nonempty
-- Module: Mathlib.Algebra.BigOperators.Expect
Goal:
ι : Type u_1
M : Type u_3
inst : Fintype ι
inst_1 : AddCommMonoid M
inst_2 : Module ℚ≥0 M
p : ι → Prop
inst_3 : DecidablePred p
h : ∀ (i j : ι), p i → p j → i = j
a : M
⊢ ∀ (i : ι),
    Membership.mem (γ := Finset ι) univ i → ∀ (j : ι), Membership.mem (γ := Finset ι) univ j → p i → p j → i = j

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

Tactic:
simp [univ.expect_ite_zero p (by simpa using h)]

Premises used: Finset.univ, Finset.expect_ite_zero
-- Module: Mathlib.Algebra.BigOperators.Expect
Goal:
ι : Type u_1
M : Type u_3
inst : Fintype ι
inst_1 : AddCommMonoid M
inst_2 : Module ℚ≥0 M
inst_3 : DecidableEq ι
s : Finset ι
f : ι → M
⊢ (𝔼 i : ι, if i ∈ s then f i else 0) = HSMul.hSMul (β := M) s.dens (𝔼 i ∈ s, f i)

Tactic:
simp [Finset.expect_ite_mem, dens]

Premises used: Finset.expect_ite_mem, Finset.dens
-- Module: Mathlib.Algebra.BigOperators.Expect
Goal:
ι : Type u_1
M : Type u_3
inst : Fintype ι
inst_1 : AddCommMonoid M
inst_2 : Module ℚ≥0 M
inst_3 : DecidableEq ι
i : ι
f : (j : ι) → i = j → M
⊢ (𝔼 j : ι, if h : i = j then f j h else 0) = HSMul.hSMul (α := ℚ≥0) (↑(card ι) : ℚ≥0)⁻¹ (f i ⋯)

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Expect
Goal:
ι : Type u_1
M : Type u_3
inst : Fintype ι
inst_1 : AddCommMonoid M
inst_2 : Module ℚ≥0 M
inst_3 : DecidableEq ι
i : ι
f : (j : ι) → j = i → M
⊢ (𝔼 j : ι, if h : j = i then f j h else 0) = HSMul.hSMul (α := ℚ≥0) (↑(card ι) : ℚ≥0)⁻¹ (f i ⋯)

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Expect
Goal:
ι : Type u_1
M : Type u_3
inst : Fintype ι
inst_1 : AddCommMonoid M
inst_2 : Module ℚ≥0 M
inst_3 : DecidableEq ι
i : ι
f : ι → M
⊢ (𝔼 j : ι, if i = j then f j else 0) = HSMul.hSMul (α := ℚ≥0) (↑(card ι) : ℚ≥0)⁻¹ (f i)

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Expect
Goal:
ι : Type u_1
M : Type u_3
inst : Fintype ι
inst_1 : AddCommMonoid M
inst_2 : Module ℚ≥0 M
inst_3 : DecidableEq ι
i : ι
f : ι → M
⊢ (𝔼 j : ι, if j = i then f j else 0) = HSMul.hSMul (α := ℚ≥0) (↑(card ι) : ℚ≥0)⁻¹ (f i)

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Expect
Goal:
ι : Type u_1
M : Type u_3
inst : Fintype ι
inst_1 : Semiring M
inst_2 : Module ℚ≥0 M
inst_3 : Nonempty ι
⊢ Eq.{u_3 + 1} (α := M) (𝔼 _i : ι, 1) 1

Tactic:
expect_const _

Premises used: Fintype.expect_const
-- Module: Mathlib.Algebra.BigOperators.Expect
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_3
inst : Fintype ι
inst_1 : Fintype κ
inst_2 : Semiring M
inst_3 : Module ℚ≥0 M
inst_4 : IsScalarTower ℚ≥0 M M
inst_5 : SMulCommClass ℚ≥0 M M
f : ι → M
g : κ → M
⊢ HMul.hMul (α := M) (𝔼 i : ι, f i) (𝔼 j : κ, g j) = 𝔼 i : ι, 𝔼 j : κ, f i * g j

Tactic:
Finset.expect_mul_expect ..

Premises used: Finset.expect_mul_expect
-- Module: Mathlib.Algebra.BigOperators.Field
Goal:
ι : Type u_1
K : Type u_2
inst : DivisionSemiring K
s : Multiset ι
f : ι → K
a : K
⊢ sum (map (fun (x : ι) ↦ f x / a) s) = (map f s).sum / a

Tactic:
simp only [div_eq_mul_inv, Multiset.sum_map_mul_right]

Premises used: div_eq_mul_inv, Multiset.sum_map_mul_right
-- Module: Mathlib.Algebra.BigOperators.Field
Goal:
ι : Type u_1
K : Type u_2
inst : DivisionSemiring K
s : Finset ι
f : ι → K
a : K
⊢ (∑ i ∈ s, f i) / a = ∑ i ∈ s, f i / a

Tactic:
simp only [div_eq_mul_inv, sum_mul]

Premises used: div_eq_mul_inv, Finset.sum_mul
-- Module: Mathlib.Algebra.BigOperators.Field
Goal:
α : Type u_3
β : Type u_4
inst : Fintype β
s : Finset α
t : α → Finset β
h : (↑s : Set α).PairwiseDisjoint t
⊢ (s.disjiUnion t h).dens = ∑ a ∈ s, (t a).dens

Tactic:
simp [dens, sum_div]

Premises used: Finset.dens, Finset.sum_div
-- Module: Mathlib.Algebra.BigOperators.Field
Goal:
α : Type u_3
β : Type u_4
inst : Fintype β
s : Finset α
t : α → Finset β
inst_1 : DecidableEq β
h : (↑s : Set α).PairwiseDisjoint t
⊢ (s.biUnion t).dens = ∑ u ∈ s, (t u).dens

Tactic:
simp [dens, card_biUnion h, sum_div]

Premises used: Finset.card_biUnion, Finset.dens, Finset.sum_div
-- Module: Mathlib.Algebra.BigOperators.Field
Goal:
α : Type u_3
β : Type u_4
inst : Fintype β
s : Finset α
t : α → Finset β
inst_1 : DecidableEq β
simp :
  HDiv.hDiv (α := ℚ≥0) (↑(#(s.biUnion t)) : ℚ≥0) (↑(Fintype.card β) : ℚ≥0) ≤
    HDiv.hDiv (α := ℚ≥0) (∑ i ∈ s, (↑(#(t i)) : ℚ≥0)) (↑(Fintype.card β) : ℚ≥0)
⊢ (s.biUnion t).dens ≤ ∑ a ∈ s, (t a).dens

Tactic:
simp only [dens, ← sum_div]

Premises used: Finset.dens, Finset.sum_div
-- Module: Mathlib.Algebra.BigOperators.Field
Goal:
α : Type u_3
β : Type u_4
inst : Fintype β
s : Finset α
t : α → Finset β
inst_1 : DecidableEq β
hab : LE.le (α := ℚ≥0) (↑(#(s.biUnion t)) : ℚ≥0) (∑ i ∈ s, (↑(#(t i)) : ℚ≥0))
⊢ HDiv.hDiv (α := ℚ≥0) (↑(#(s.biUnion t)) : ℚ≥0) (↑(Fintype.card β) : ℚ≥0) ≤
    HDiv.hDiv (α := ℚ≥0) (∑ i ∈ s, (↑(#(t i)) : ℚ≥0)) (↑(Fintype.card β) : ℚ≥0)

Tactic:
gcongr
-- Module: Mathlib.Algebra.BigOperators.Field
Goal:
α : Type u_3
β : Type u_4
inst : Fintype β
s : Finset α
t : α → Finset β
inst_1 : DecidableEq β
⊢ LE.le (α := ℚ≥0) (↑(#(s.biUnion t)) : ℚ≥0) (∑ i ∈ s, (↑(#(t i)) : ℚ≥0))

Tactic:
mod_cast card_biUnion_le

Premises used: congrArg, Nat.cast_sum._simp_1, cast, Nat.cast_le._simp_1, LE.le, Finset.biUnion, Nat.cast, Finset.card, Finset.card_biUnion_le, Eq.symm, Eq.trans
-- Module: Mathlib.Algebra.BigOperators.Field
Goal:
α : Type u_3
β : Type u_4
inst : Fintype β
s : Finset α
t : α → Finset β
inst_1 : DecidableEq β
⊢ LE.le (α := ℚ≥0) (↑(#(s.biUnion t)) : ℚ≥0) (∑ i ∈ s, (↑(#(t i)) : ℚ≥0))

Tactic:
exact mod_cast card_biUnion_le

Premises used: Finset.card_biUnion_le
-- Module: Mathlib.Algebra.BigOperators.Field
Goal:
α : Type u_3
β : Type u_4
inst : Fintype β
s : Finset α
inst_1 : DecidableEq α
f : β → α
t : Finset β
h : Set.MapsTo f (↑t : Set β) (↑s : Set α)
⊢ t.dens = ∑ a ∈ s, {b ∈ t | f b = a}.dens

Tactic:
simp [dens, ← sum_div, card_eq_sum_card_fiberwise h]

Premises used: Finset.dens, Finset.sum_div, Finset.card_eq_sum_card_fiberwise
-- Module: Mathlib.Algebra.BigOperators.Field
Goal:
α : Type u_3
β : Type u_4
inst : Fintype β
inst_1 : DecidableEq α
f : β → α
t : Finset β
⊢ t.dens = ∑ a ∈ image f t, {b ∈ t | f b = a}.dens

Tactic:
dens_eq_sum_dens_fiberwise fun _ ↦ mem_image_of_mem _

Premises used: Finset.dens_eq_sum_dens_fiberwise, Finset.mem_image_of_mem
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
n : ℕ
f : ℕ → M
⊢ Eq.{u_2 + 1} (α := M) (∏ i ∈ range n, f i) (∏ i : Fin n, f (↑i : ℕ))

Tactic:
(Fin.prod_univ_eq_prod_range _ _).symm

Premises used: Fin.prod_univ_eq_prod_range, Eq.symm
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
n : ℕ
f : Fin n → M
⊢ (List.ofFn f).prod = ∏ i : Fin n, f i

Tactic:
simp [prod_eq_multiset_prod]

Premises used: Finset.prod_eq_multiset_prod
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
n : ℕ
f : Fin n → M
rw : ∏ i : Fin n, f i = (List.ofFn f).prod
rw₁ rw₂ : Eq.{u_2 + 1} (α := M) (∏ i : Fin n, f i) (∏ i : Fin n, f i)
⊢ ∏ i : Fin n, f i = (List.map f (List.finRange n)).prod

Tactic:
rw [← List.ofFn_eq_map, prod_ofFn]

Premises used: Fin.prod_ofFn, List.ofFn_eq_map
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
f : Fin 0 → M
⊢ Eq.{u_2 + 1} (α := M) (∏ i : Fin 0, f i) 1

Tactic:
rfl

Premises used: Multiset.foldr, Multiset.prod, Finset.prod, List.foldr, rfl
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
n : ℕ
f : Fin (n + 1) → M
x : Fin (n + 1)
rw : ∏ i ∈ Finset.cons x (map x.succAboveEmb univ) ⋯, f i = f x * ∏ i : Fin n, f (x.succAbove i)
rw₁ : f x * ∏ x ∈ map x.succAboveEmb univ, f x = f x * ∏ i : Fin n, f (x.succAbove i)
rw₂ : f x * ∏ x_1 : Fin n, f ((x.succAboveEmb : (a : Fin n) → Fin (n + 1)) x_1) = f x * ∏ i : Fin n, f (x.succAbove i)
rw₃ rw₄ : f x * ∏ x_1 : Fin n, f (x.succAbove x_1) = f x * ∏ i : Fin n, f (x.succAbove i)
⊢ ∏ i : Fin (n + 1), f i = f x * ∏ i : Fin n, f (x.succAbove i)

Tactic:
rw [univ_succAbove n x, prod_cons, Finset.prod_map, coe_succAboveEmb]

Premises used: Fin.univ_succAbove, Finset.prod_cons, Finset.prod_map, Fin.coe_succAboveEmb
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
n : ℕ
f : Fin (n + 1) → M
⊢ ∏ i : Fin (n + 1), f i = f 0 * ∏ i : Fin n, f i.succ

Tactic:
prod_univ_succAbove f 0

Premises used: Fin.succAbove, Fin.succ, Fin.prod_univ_succAbove, OfNat.ofNat, ite
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
n : ℕ
f : Fin (n + 1) → M
⊢ ∏ i : Fin (n + 1), f i = (∏ i : Fin n, f i.castSucc) * f (last n)

Tactic:
simpa [mul_comm] using prod_univ_succAbove f (last n)

Premises used: Fin.prod_univ_succAbove, Fin.last, mul_comm
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
l : List M
⊢ ∏ i : Fin l.length, getElem (valid := fun (as : List M) (i : ℕ) ↦ i < as.length) l (↑i : ℕ) ⋯ = l.prod

Tactic:
simp [Finset.prod_eq_multiset_prod]

Premises used: Finset.prod_eq_multiset_prod
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
ι : Type u_1
M : Type u_2
inst : CommMonoid M
l : List ι
f : ι → M
⊢ ∏ i : Fin l.length, f (getElem (valid := fun (as : List ι) (i : ℕ) ↦ i < as.length) l (↑i : ℕ) ⋯) =
    (List.map f l).prod

Tactic:
simp [Finset.prod_eq_multiset_prod]

Premises used: Finset.prod_eq_multiset_prod
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
n : ℕ
x : M
f : Fin n → M
simp_rw :
  HMul.hMul (α := M) (β := M) (cons (α := fun (a : Fin n.succ) ↦ M) x f 0 : M)
      (∏ i : Fin n, cons (α := fun (a : Fin n.succ) ↦ M) x f i.succ : M) =
    x * ∏ i : Fin n, f i
simp_rw₁ : x * ∏ i : Fin n, cons (α := fun (a : Fin n.succ) ↦ M) x f i.succ = x * ∏ i : Fin n, f i
⊢ ∏ i : Fin n.succ, cons (α := fun (a : Fin n.succ) ↦ M) x f i = x * ∏ i : Fin n, f i

Tactic:
simp_rw [prod_univ_succ, cons_zero, cons_succ]

Premises used: Fin.cons_succ, Fin.prod_univ_succ, Fin.cons_zero
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
n : ℕ
x : M
f : Fin n → M
⊢ ∏ i : Fin n.succ, snoc (α := fun (a : Fin n.succ) ↦ M) f x i = (∏ i : Fin n, f i) * x

Tactic:
simp [prod_univ_castSucc]

Premises used: Fin.prod_univ_castSucc
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
f : Fin 1 → M
⊢ ∏ i : Fin 1, f i = f 0

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
f : Fin 2 → M
⊢ ∏ i : Fin 2, f i = f 0 * f 1

Tactic:
simp [prod_univ_succ]

Premises used: Fin.prod_univ_succ
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
ι : Type u_1
M : Type u_2
inst : CommMonoid M
f : ι → M
a b : ι
⊢ ∏ i : Fin (Nat.succ 0).succ, f (![a, b] i) = f a * f b

Tactic:
prod_univ_two _

Premises used: Eq.mpr, Fin.cons, Fin.induction.go, Fin.prod_univ_two, Fin.induction, Fin.cases, Matrix.vecCons
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
f : Fin 3 → M
rw : f (castSucc 0) * f (castSucc 1) * f (last 2) = f 0 * f 1 * f 2
⊢ ∏ i : Fin 3, f i = f 0 * f 1 * f 2

Tactic:
rw [prod_univ_castSucc, prod_univ_two]

Premises used: Fin.prod_univ_castSucc, Fin.prod_univ_two
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
f : Fin 3 → M
⊢ f (castSucc 0) * f (castSucc 1) * f (last 2) = f 0 * f 1 * f 2

Tactic:
rfl
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
f : Fin 4 → M
rw : f (castSucc 0) * f (castSucc 1) * f (castSucc 2) * f (last 3) = f 0 * f 1 * f 2 * f 3
⊢ ∏ i : Fin 4, f i = f 0 * f 1 * f 2 * f 3

Tactic:
rw [prod_univ_castSucc, prod_univ_three]

Premises used: Fin.prod_univ_castSucc, Fin.prod_univ_three
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
f : Fin 4 → M
⊢ f (castSucc 0) * f (castSucc 1) * f (castSucc 2) * f (last 3) = f 0 * f 1 * f 2 * f 3

Tactic:
rfl
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
f : Fin 5 → M
rw : f (castSucc 0) * f (castSucc 1) * f (castSucc 2) * f (castSucc 3) * f (last 4) = f 0 * f 1 * f 2 * f 3 * f 4
⊢ ∏ i : Fin 5, f i = f 0 * f 1 * f 2 * f 3 * f 4

Tactic:
rw [prod_univ_castSucc, prod_univ_four]

Premises used: Fin.prod_univ_four, Fin.prod_univ_castSucc