awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Expect (goal)
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
⊢ a * 𝔼 i ∈ s, f i = 𝔼 i ∈ s, a * f i
have rw₁ : a * HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#s) : ℚ≥0)⁻¹ (∑ i ∈ s, f i) =
  HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#s) : ℚ≥0)⁻¹ (∑ i ∈ s, a * f i)
Tactic: rw [expect, expect, mul_smul_comm, mul_sum]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Expect (goal)
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)
⊢ a * 𝔼 i ∈ s, f i = 𝔼 i ∈ s, a * f i
have rw₂ : HSMul.hSMul (α := ℚ≥0) (↑(#s) : ℚ≥0)⁻¹ (a * ∑ i ∈ s, f i) =
  HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#s) : ℚ≥0)⁻¹ (∑ i ∈ s, a * f i)
Tactic: rw [expect, expect, mul_smul_comm, mul_sum]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Expect (goal)
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)
⊢ a * 𝔼 i ∈ s, f i = 𝔼 i ∈ s, a * f i
have rw₃ : HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#s) : ℚ≥0)⁻¹ (∑ i ∈ s, a * f i) =
  HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#s) : ℚ≥0)⁻¹ (∑ i ∈ s, a * f i)
Tactic: rw [expect, expect, mul_smul_comm, mul_sum]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Expect (goal)
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
⊢ HMul.hMul (α := M) (𝔼 i ∈ s, f i) (𝔼 j ∈ t, g j) = 𝔼 i ∈ s, 𝔼 j ∈ t, f i * g j
have simp_rw : Eq.{u_3 + 1} (α := M) (𝔼 i ∈ s, f i * 𝔼 j ∈ t, g j) (𝔼 i ∈ s, 𝔼 j ∈ t, f i * g j)
Tactic: simp_rw [expect_mul, mul_expect]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Expect (goal)
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 : ℕ
⊢ 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)
have 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)
Tactic: rw [expect, smul_pow, sum_pow', expect, Fintype.card_piFinset_const, inv_pow, Nat.cast_pow]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Expect (goal)
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)
⊢ 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)
have 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)
Tactic: rw [expect, smul_pow, sum_pow', expect, Fintype.card_piFinset_const, inv_pow, Nat.cast_pow]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Expect (goal)
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)
⊢ 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)
have 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)
Tactic: rw [expect, smul_pow, sum_pow', expect, Fintype.card_piFinset_const, inv_pow, Nat.cast_pow]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Expect (goal)
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)
⊢ 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)
have 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))
Tactic: rw [expect, smul_pow, sum_pow', expect, Fintype.card_piFinset_const, inv_pow, Nat.cast_pow]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Expect (goal)
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))
⊢ 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)
have 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))
Tactic: rw [expect, smul_pow, sum_pow', expect, Fintype.card_piFinset_const, inv_pow, Nat.cast_pow]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Expect (goal)
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))
⊢ 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)
have 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))
Tactic: rw [expect, smul_pow, sum_pow', expect, Fintype.card_piFinset_const, inv_pow, Nat.cast_pow]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Expect (goal)
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))
⊢ 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)
have 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))
Tactic: rw [expect, smul_pow, sum_pow', expect, Fintype.card_piFinset_const, inv_pow, Nat.cast_pow]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Expect (goal)
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 : ℕ
⊢ 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)
have 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)
Tactic: classical
  rw [expect, smul_pow, sum_pow', expect, Fintype.card_piFinset_const, inv_pow, Nat.cast_pow]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Expect (goal)
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)
⊢ 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)
have 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)
Tactic: classical
  rw [expect, smul_pow, sum_pow', expect, Fintype.card_piFinset_const, inv_pow, Nat.cast_pow]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Expect (goal)
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)
⊢ 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)
have 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)
Tactic: classical
  rw [expect, smul_pow, sum_pow', expect, Fintype.card_piFinset_const, inv_pow, Nat.cast_pow]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Expect (goal)
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)
⊢ 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)
have 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))
Tactic: classical
  rw [expect, smul_pow, sum_pow', expect, Fintype.card_piFinset_const, inv_pow, Nat.cast_pow]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Expect (goal)
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))
⊢ 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)
have 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))
Tactic: classical
  rw [expect, smul_pow, sum_pow', expect, Fintype.card_piFinset_const, inv_pow, Nat.cast_pow]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Expect (goal)
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))
⊢ 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)
have 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))
Tactic: classical
  rw [expect, smul_pow, sum_pow', expect, Fintype.card_piFinset_const, inv_pow, Nat.cast_pow]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Expect (goal)
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))
⊢ 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)
have 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))
Tactic: classical
  rw [expect, smul_pow, sum_pow', expect, Fintype.card_piFinset_const, inv_pow, Nat.cast_pow]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Expect (goal)
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 : ι
⊢ 𝔼 j : ι, (if i = j then (↑(Fintype.card ι) : M) else 0) * f j = f i
have simp_rw : HSMul.hSMul (α := ℚ≥0) (↑(Fintype.card ι) : ℚ≥0)⁻¹ ((↑(Fintype.card ι) : M) * f i) = f i
Tactic: simp_rw [expect_univ, ite_mul, zero_mul, sum_ite_eq, if_pos (mem_univ _)]