awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Expect (goal)
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))
⊢ Eq.{u_3 + 1} (α := M) (𝔼 i ∈ s, 𝔼 j ∈ t, f i j) (𝔼 j ∈ t, 𝔼 i ∈ s, f i j)
have 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))
Tactic: rw [expect, expect, ← expect_sum_comm, ← expect_sum_comm, expect, expect, smul_comm, sum_comm]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Expect (goal)
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))
⊢ Eq.{u_3 + 1} (α := M) (𝔼 i ∈ s, 𝔼 j ∈ t, f i j) (𝔼 j ∈ t, 𝔼 i ∈ s, f i j)
have 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))
Tactic: rw [expect, expect, ← expect_sum_comm, ← expect_sum_comm, expect, expect, smul_comm, sum_comm]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Expect (goal)
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
⊢ ∃ i ∈ s, f i ≠ 0
have contrapose! : ∀ (h : ∀ (i : ι) (_ : i ∈ s), f i = 0), Eq.{u_3 + 1} (α := M) (𝔼 i ∈ s, f i) 0
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Expect (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddCommMonoid M
inst_1 : Module ℚ≥0 M
s : Finset ι
f₁ f₂ g₁ g₂ : ι → M
⊢ 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))
have 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)
Tactic: simp_rw [expect_add_distrib, add_add_add_comm]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Expect (goal)
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
⊢ 𝔼 i ∈ s, f i = HSMul.hSMul (α := ℚ≥0) (↑(#s) : ℚ≥0)⁻¹ (f i)
have rw : HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#s) : ℚ≥0)⁻¹ (∑ i ∈ s, f i) = HSMul.hSMul (α := ℚ≥0) (↑(#s) : ℚ≥0)⁻¹ (f i)
Tactic: rw [expect, sum_eq_single_of_mem _ hi h]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Expect (goal)
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)
⊢ 𝔼 i ∈ s, f i = HSMul.hSMul (α := ℚ≥0) (↑(#s) : ℚ≥0)⁻¹ (f i)
have rw₁ : HSMul.hSMul (α := ℚ≥0) (↑(#s) : ℚ≥0)⁻¹ (f i) = HSMul.hSMul (α := ℚ≥0) (↑(#s) : ℚ≥0)⁻¹ (f i)
Tactic: rw [expect, sum_eq_single_of_mem _ hi h]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Expect (goal)
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
⊢ (𝔼 i ∈ s, if p i then a else 0) = if ∃ i ∈ s, p i then HSMul.hSMul (α := ℚ≥0) (↑(#s) : ℚ≥0)⁻¹ a else 0
have pos : (∃ i ∈ s, p i) → (𝔼 i ∈ s, if p i then a else 0) = HSMul.hSMul (α := ℚ≥0) (↑(#s) : ℚ≥0)⁻¹ a
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Expect (goal)
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
⊢ (𝔼 i ∈ s, if p i then a else 0) = if ∃ i ∈ s, p i then HSMul.hSMul (α := ℚ≥0) (↑(#s) : ℚ≥0)⁻¹ a else 0
have neg : (¬∃ i ∈ s, p i) → Eq.{u_3 + 1} (α := M) (𝔼 i ∈ s, if p i then a else 0) 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Expect (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddCommMonoid M
inst_1 : Module ℚ≥0 M
inst_2 : DecidableEq ι
s t : Finset ι
f : ι → M
⊢ (𝔼 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)
have 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)
Tactic: obtain hst | hst := (s ∩ t).eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Expect (goal)
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)
⊢ (𝔼 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)
have 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)
Tactic: obtain hst | hst := (s ∩ t).eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Expect (goal)
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
⊢ (𝔼 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
have pos : i ∈ s → (𝔼 j ∈ s, if h : i = j then f j h else 0) = HSMul.hSMul (α := ℚ≥0) (↑(#s) : ℚ≥0)⁻¹ (f i sorry)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Expect (goal)
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 ⋯)
⊢ (𝔼 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
have neg : i ∉ s → Eq.{u_3 + 1} (α := M) (𝔼 j ∈ s, if h : i = j then f j h else 0) 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Expect (goal)
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
⊢ (𝔼 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
have pos : i ∈ s → (𝔼 j ∈ s, if h : j = i then f j h else 0) = HSMul.hSMul (α := ℚ≥0) (↑(#s) : ℚ≥0)⁻¹ (f i sorry)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Expect (goal)
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 ⋯)
⊢ (𝔼 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
have neg : i ∉ s → Eq.{u_3 + 1} (α := M) (𝔼 j ∈ s, if h : j = i then f j h else 0) 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Expect (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddCommMonoid M
inst_1 : Module ℚ≥0 M
s : Finset ι
inst_2 : DecidableEq ι
i : ι
f : ι → M
⊢ (𝔼 j ∈ s, if i = j then f j else 0) = if i ∈ s then HSMul.hSMul (α := ℚ≥0) (↑(#s) : ℚ≥0)⁻¹ (f i) else 0
have pos : i ∈ s → (𝔼 j ∈ s, if i = j then f j else 0) = HSMul.hSMul (α := ℚ≥0) (↑(#s) : ℚ≥0)⁻¹ (f i)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Expect (goal)
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)
⊢ (𝔼 j ∈ s, if i = j then f j else 0) = if i ∈ s then HSMul.hSMul (α := ℚ≥0) (↑(#s) : ℚ≥0)⁻¹ (f i) else 0
have neg : i ∉ s → Eq.{u_3 + 1} (α := M) (𝔼 j ∈ s, if i = j then f j else 0) 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Expect (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddCommMonoid M
inst_1 : Module ℚ≥0 M
s : Finset ι
inst_2 : DecidableEq ι
i : ι
f : ι → M
⊢ (𝔼 j ∈ s, if j = i then f j else 0) = if i ∈ s then HSMul.hSMul (α := ℚ≥0) (↑(#s) : ℚ≥0)⁻¹ (f i) else 0
have pos : i ∈ s → (𝔼 j ∈ s, if j = i then f j else 0) = HSMul.hSMul (α := ℚ≥0) (↑(#s) : ℚ≥0)⁻¹ (f i)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Expect (goal)
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)
⊢ (𝔼 j ∈ s, if j = i then f j else 0) = if i ∈ s then HSMul.hSMul (α := ℚ≥0) (↑(#s) : ℚ≥0)⁻¹ (f i) else 0
have neg : i ∉ s → Eq.{u_3 + 1} (α := M) (𝔼 j ∈ s, if j = i then f j else 0) 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Expect (goal)
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
⊢ Eq.{u_3 + 1} (α := M) (𝔼 i ∈ s, f i) (𝔼 i ∈ t, g i)
have simp_rw : HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#s) : ℚ≥0)⁻¹ (∑ x ∈ s, f x) =
  HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#t) : ℚ≥0)⁻¹ (∑ x ∈ t, g x)
Tactic: simp_rw [expect, card_bij i hi i_inj i_surj, sum_bij i hi i_inj i_surj h]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Expect (goal)
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)
⊢ Eq.{u_3 + 1} (α := M) (𝔼 i ∈ s, f i) (𝔼 i ∈ t, g i)
have simp_rw₁ : HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#t) : ℚ≥0)⁻¹ (∑ x ∈ s, f x) =
  HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#t) : ℚ≥0)⁻¹ (∑ x ∈ t, g x)
Tactic: simp_rw [expect, card_bij i hi i_inj i_surj, sum_bij i hi i_inj i_surj h]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Expect (goal)
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)
⊢ Eq.{u_3 + 1} (α := M) (𝔼 i ∈ s, f i) (𝔼 i ∈ t, g i)
have simp_rw : HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#s) : ℚ≥0)⁻¹ (∑ x ∈ s, f x) =
  HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#t) : ℚ≥0)⁻¹ (∑ x ∈ t, g x)
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]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Expect (goal)
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)
⊢ Eq.{u_3 + 1} (α := M) (𝔼 i ∈ s, f i) (𝔼 i ∈ t, g i)
have simp_rw₁ : HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#t) : ℚ≥0)⁻¹ (∑ x ∈ s, f x) =
  HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#t) : ℚ≥0)⁻¹ (∑ x ∈ t, g x)
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]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Expect (goal)
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 κ)
⊢ Eq.{u_3 + 1} (α := M) (𝔼 i ∈ s, f i) (𝔼 i ∈ t, g i)
have simp_rw : HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#s) : ℚ≥0)⁻¹ (∑ x ∈ s, f x) =
  HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#t) : ℚ≥0)⁻¹ (∑ x ∈ t, g x)
Tactic: simp_rw [expect, card_nbij i hi i_inj i_surj, sum_nbij i hi i_inj i_surj h]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Expect (goal)
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)
⊢ Eq.{u_3 + 1} (α := M) (𝔼 i ∈ s, f i) (𝔼 i ∈ t, g i)
have simp_rw₁ : HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#t) : ℚ≥0)⁻¹ (∑ x ∈ s, f x) =
  HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#t) : ℚ≥0)⁻¹ (∑ x ∈ t, g x)
Tactic: simp_rw [expect, card_nbij i hi i_inj i_surj, sum_nbij i hi i_inj i_surj h]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Expect (goal)
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)
⊢ Eq.{u_3 + 1} (α := M) (𝔼 i ∈ s, f i) (𝔼 i ∈ t, g i)
have simp_rw : HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#s) : ℚ≥0)⁻¹ (∑ x ∈ s, f x) =
  HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#t) : ℚ≥0)⁻¹ (∑ x ∈ t, g x)
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]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Expect (goal)
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)
⊢ Eq.{u_3 + 1} (α := M) (𝔼 i ∈ s, f i) (𝔼 i ∈ t, g i)
have simp_rw₁ : HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#t) : ℚ≥0)⁻¹ (∑ x ∈ s, f x) =
  HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#t) : ℚ≥0)⁻¹ (∑ x ∈ t, g x)
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]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Expect (goal)
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)
⊢ Eq.{u_3 + 1} (α := M) (𝔼 i ∈ s, f i) (𝔼 i ∈ t, g i)
have simp_rw : HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#s) : ℚ≥0)⁻¹ (∑ x ∈ s, f x) =
  HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#t) : ℚ≥0)⁻¹ (∑ x ∈ t, g x)
Tactic: simp_rw [expect, card_equiv e hst, sum_equiv e hst hfg]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Expect (goal)
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)
⊢ Eq.{u_3 + 1} (α := M) (𝔼 i ∈ s, f i) (𝔼 i ∈ t, g i)
have simp_rw₁ : HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#t) : ℚ≥0)⁻¹ (∑ x ∈ s, f x) =
  HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#t) : ℚ≥0)⁻¹ (∑ x ∈ t, g x)
Tactic: simp_rw [expect, card_equiv e hst, sum_equiv e hst hfg]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Expect (goal)
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 κ)
⊢ Eq.{u_3 + 1} (α := M) (𝔼 i ∈ image m t, f i) (𝔼 i ∈ t, f (m i))
have 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))
Tactic: simp_rw [expect, card_image_of_injOn hm, sum_image hm]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Expect (goal)
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))
⊢ Eq.{u_3 + 1} (α := M) (𝔼 i ∈ image m t, f i) (𝔼 i ∈ t, f (m i))
have 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))
Tactic: simp_rw [expect, card_image_of_injOn hm, sum_image hm]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Expect (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddCommMonoid M
inst_1 : Module ℚ≥0 M
s : Finset ι
hs : s.Nonempty
a : M
⊢ 𝔼 _i ∈ s, a = a
have ha : Ne (α := ℚ≥0) (↑(#s) : ℚ≥0) 0
Tactic: rw [expect, sum_const, ← Nat.cast_smul_eq_nsmul ℚ≥0, inv_smul_smul₀]
-- 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
s : Finset ι
f : ι → M
⊢ HMul.hMul (α := M) (↑(#s) : M) (𝔼 i ∈ s, f i) = ∑ i ∈ s, f i
have rw : HSMul.hSMul (β := M) (#s) (𝔼 i ∈ s, f i) = ∑ i ∈ s, f i
Tactic: rw [← nsmul_eq_mul, card_smul_expect]
-- 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
s : Finset ι
f : ι → M
rw : HSMul.hSMul (β := M) (#s) (𝔼 i ∈ s, f i) = ∑ i ∈ s, f i
⊢ HMul.hMul (α := M) (↑(#s) : M) (𝔼 i ∈ s, f i) = ∑ i ∈ s, f i
have rw₁ : Eq.{u_3 + 1} (α := M) (∑ i ∈ s, f i) (∑ i ∈ s, f i)
Tactic: rw [← nsmul_eq_mul, card_smul_expect]
-- 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 : IsScalarTower ℚ≥0 M M
s : Finset ι
f : ι → M
a : M
⊢ (𝔼 i ∈ s, f i) * a = 𝔼 i ∈ s, f i * a
have rw : HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#s) : ℚ≥0)⁻¹ (∑ i ∈ s, f i) * a = 𝔼 i ∈ s, f i * a
Tactic: rw [expect, expect, smul_mul_assoc, sum_mul]
-- 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 : 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
⊢ (𝔼 i ∈ s, f i) * a = 𝔼 i ∈ s, f i * a
have rw₁ : HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#s) : ℚ≥0)⁻¹ (∑ i ∈ s, f i) * a =
  HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#s) : ℚ≥0)⁻¹ (∑ i ∈ s, f i * a)
Tactic: rw [expect, expect, smul_mul_assoc, sum_mul]
-- 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 : 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)
⊢ (𝔼 i ∈ s, f i) * a = 𝔼 i ∈ s, f i * a
have rw₂ : HSMul.hSMul (α := ℚ≥0) (↑(#s) : ℚ≥0)⁻¹ ((∑ i ∈ s, f i) * a) =
  HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#s) : ℚ≥0)⁻¹ (∑ i ∈ s, f i * a)
Tactic: rw [expect, expect, smul_mul_assoc, sum_mul]
-- 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 : 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)
⊢ (𝔼 i ∈ s, f i) * a = 𝔼 i ∈ s, f i * a
have rw₃ : HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#s) : ℚ≥0)⁻¹ (∑ i ∈ s, f i * a) =
  HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#s) : ℚ≥0)⁻¹ (∑ i ∈ s, f i * a)
Tactic: rw [expect, expect, smul_mul_assoc, sum_mul]
-- 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
⊢ a * 𝔼 i ∈ s, f i = 𝔼 i ∈ s, a * f i
have rw : a * HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#s) : ℚ≥0)⁻¹ (∑ i ∈ s, f i) = 𝔼 i ∈ s, a * f i
Tactic: rw [expect, expect, mul_smul_comm, mul_sum]