awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Associated (goal)
Goal:
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : IsCancelMulZero M₀
inst_2 : (a : M₀) → DecidablePred (Associated a)
a : M₀
s : Multiset M₀
induct :
  ∀ (n : M₀) (h : ∀ a ∈ s, Prime a) (div : ∀ a ∈ s, a ∣ n) (uniq : ∀ (a : M₀), countP (Associated a) s ≤ 1), s.prod ∣ n
h : ∀ a_1 ∈ a ::ₘ s, Prime a_1
uniq : ∀ (a_1 : M₀), countP (Associated a_1) (a ::ₘ s) ≤ 1
k : M₀
div : ∀ a_1 ∈ a ::ₘ s, a_1 ∣ a * k
b : M₀
b_in_s : b ∈ s
b_div_n : b ∣ a * k
a_prime : Prime a
b_prime : Prime b
⊢ b ∣ k
have cons : ∀ (b_div_a : b ∣ a), False
Tactic: refine (b_prime.dvd_or_dvd b_div_n).resolve_left fun b_div_a => ?_
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Associated (hypothesis)
Goal:
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : IsCancelMulZero M₀
inst_2 : (a : M₀) → DecidablePred (Associated a)
a : M₀
s : Multiset M₀
induct :
  ∀ (n : M₀) (h : ∀ a ∈ s, Prime a) (div : ∀ a ∈ s, a ∣ n) (uniq : ∀ (a : M₀), countP (Associated a) s ≤ 1), s.prod ∣ n
h : ∀ a_1 ∈ a ::ₘ s, Prime a_1
uniq : ∀ (a_1 : M₀), countP (Associated a_1) (a ::ₘ s) ≤ 1
k : M₀
div : ∀ a_1 ∈ a ::ₘ s, a_1 ∣ a * k
b : M₀
b_in_s : b ∈ s
b_div_n : b ∣ a * k
a_prime : Prime a
b_prime : Prime b
b_div_a : b ∣ a
⊢ False
have assoc : b ~ᵤ a
Tactic: have assoc := b_prime.associated_of_dvd a_prime b_div_a
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Associated (hypothesis)
Goal:
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : IsCancelMulZero M₀
inst_2 : (a : M₀) → DecidablePred (Associated a)
a : M₀
s : Multiset M₀
induct :
  ∀ (n : M₀) (h : ∀ a ∈ s, Prime a) (div : ∀ a ∈ s, a ∣ n) (uniq : ∀ (a : M₀), countP (Associated a) s ≤ 1), s.prod ∣ n
h : ∀ a_1 ∈ a ::ₘ s, Prime a_1
uniq : ∀ (a_1 : M₀), countP (Associated a_1) (a ::ₘ s) ≤ 1
k : M₀
div : ∀ a_1 ∈ a ::ₘ s, a_1 ∣ a * k
b : M₀
b_in_s : b ∈ s
b_div_n : b ∣ a * k
a_prime : Prime a
b_prime : Prime b
b_div_a : b ∣ a
assoc : b ~ᵤ a
⊢ False
have this : countP (Associated a) (a ::ₘ s) ≤ 1
Tactic: have := uniq a
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Associated (hypothesis)
Goal:
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : IsCancelMulZero M₀
inst_2 : (a : M₀) → DecidablePred (Associated a)
a : M₀
s : Multiset M₀
induct :
  ∀ (n : M₀) (h : ∀ a ∈ s, Prime a) (div : ∀ a ∈ s, a ∣ n) (uniq : ∀ (a : M₀), countP (Associated a) s ≤ 1), s.prod ∣ n
h : ∀ a_1 ∈ a ::ₘ s, Prime a_1
uniq : ∀ (a_1 : M₀), countP (Associated a_1) (a ::ₘ s) ≤ 1
k : M₀
div : ∀ a_1 ∈ a ::ₘ s, a_1 ∣ a * k
b : M₀
b_in_s : b ∈ s
b_div_n : b ∣ a * k
a_prime : Prime a
b_prime : Prime b
b_div_a : b ∣ a
assoc : b ~ᵤ a
this : countP (Associated a) (a ::ₘ s) ≤ 1
⊢ False
have this₁ : ¬∃ a_1 ∈ s, a ~ᵤ a_1
Tactic: rw [Multiset.countP_cons_of_pos _ (Associated.refl _), Nat.succ_le_succ_iff, ← not_lt,
      Multiset.countP_pos] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Associated (goal)
Goal:
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : IsCancelMulZero M₀
inst_2 : (a : M₀) → DecidablePred (Associated a)
s : Multiset M₀
n : M₀
h : ∀ a ∈ s, Prime a
div : ∀ a ∈ s, a ∣ n
uniq : ∀ (a : M₀), countP (Associated a) s ≤ 1
⊢ s.prod ∣ n
have empty : ∀ (n : M₀) (h : ∀ (a : M₀), Membership.mem (γ := Multiset M₀) 0 a → Prime a)
  (div : ∀ (a : M₀), Membership.mem (γ := Multiset M₀) 0 a → a ∣ n) (uniq : ∀ (a : M₀), countP (Associated a) 0 ≤ 1),
  prod 0 ∣ n
Tactic: induction s using Multiset.induction_on generalizing n with
  | empty => simp only [Multiset.prod_zero, one_dvd]
  | cons a s induct =>
    rw [Multiset.prod_cons]
    obtain ⟨k, rfl⟩ : a ∣ n := div a (Multiset.mem_cons_self a s)
    gcongr
    refine induct _ (fun a ha => h a (Multiset.mem_cons_of_mem ha)) (fun b b_in_s => ?_)
      fun a => (Multiset.countP_le_of_le _ (Multiset.le_cons_self _ _)).trans (uniq a)
    have b_div_n := div b (Multiset.mem_cons_of_mem b_in_s)
    have a_prime := h a (Multiset.mem_cons_self a s)
    have b_prime := h b (Multiset.mem_cons_of_mem b_in_s)
    refine (b_prime.dvd_or_dvd b_div_n).resolve_left fun b_div_a => ?_
    have assoc := b_prime.associated_of_dvd a_prime b_div_a
    have := uniq a
    rw [Multiset.countP_cons_of_pos _ (Associated.refl _), Nat.succ_le_succ_iff, ← not_lt,
      Multiset.countP_pos] at this
    exact this ⟨b, b_in_s, assoc.symm⟩
Cleared hypotheses: s, n, h, div, uniq
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Associated (goal)
Goal:
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : IsCancelMulZero M₀
inst_2 : (a : M₀) → DecidablePred (Associated a)
s : Multiset M₀
n : M₀
h : ∀ a ∈ s, Prime a
div : ∀ a ∈ s, a ∣ n
uniq : ∀ (a : M₀), countP (Associated a) s ≤ 1
empty :
  ∀ (n : M₀) (h : ∀ (a : M₀), Membership.mem (γ := Multiset M₀) 0 a → Prime a)
    (div : ∀ (a : M₀), Membership.mem (γ := Multiset M₀) 0 a → a ∣ n) (uniq : ∀ (a : M₀), countP (Associated a) 0 ≤ 1),
    prod 0 ∣ n
⊢ s.prod ∣ n
have cons : ∀ (a : M₀) (s : Multiset M₀)
  (induct :
    ∀ (n : M₀) (h : ∀ a ∈ s, Prime a) (div : ∀ a ∈ s, a ∣ n) (uniq : ∀ (a : M₀), countP (Associated a) s ≤ 1),
      s.prod ∣ n)
  (n : M₀) (h : ∀ a_1 ∈ a ::ₘ s, Prime a_1) (div : ∀ a_1 ∈ a ::ₘ s, a_1 ∣ n)
  (uniq : ∀ (a_1 : M₀), countP (Associated a_1) (a ::ₘ s) ≤ 1), (a ::ₘ s).prod ∣ n
Tactic: induction s using Multiset.induction_on generalizing n with
  | empty => simp only [Multiset.prod_zero, one_dvd]
  | cons a s induct =>
    rw [Multiset.prod_cons]
    obtain ⟨k, rfl⟩ : a ∣ n := div a (Multiset.mem_cons_self a s)
    gcongr
    refine induct _ (fun a ha => h a (Multiset.mem_cons_of_mem ha)) (fun b b_in_s => ?_)
      fun a => (Multiset.countP_le_of_le _ (Multiset.le_cons_self _ _)).trans (uniq a)
    have b_div_n := div b (Multiset.mem_cons_of_mem b_in_s)
    have a_prime := h a (Multiset.mem_cons_self a s)
    have b_prime := h b (Multiset.mem_cons_of_mem b_in_s)
    refine (b_prime.dvd_or_dvd b_div_n).resolve_left fun b_div_a => ?_
    have assoc := b_prime.associated_of_dvd a_prime b_div_a
    have := uniq a
    rw [Multiset.countP_cons_of_pos _ (Associated.refl _), Nat.succ_le_succ_iff, ← not_lt,
      Multiset.countP_pos] at this
    exact this ⟨b, b_in_s, assoc.symm⟩
Cleared hypotheses: s, n, h, div, uniq
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Associated (goal)
Goal:
ι : Type u_1
M : Type u_2
inst : CommMonoid M
p : Finset ι
f : ι → M
⊢ Eq.{u_2 + 1} (α := Associates M) (∏ i ∈ p, Associates.mk (f i)) (Associates.mk (∏ i ∈ p, f i))
have rw : Eq.{u_2 + 1} (α := Associates M) (Multiset.prod (Multiset.map (fun (i : ι) ↦ Associates.mk (f i)) p.val))
  (Associates.mk (∏ i ∈ p, f i))
Tactic: rw [Finset.prod_eq_multiset_prod, ← Function.comp_def, ← Multiset.map_map, prod_mk,
    ← Finset.prod_eq_multiset_prod]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Associated (goal)
Goal:
ι : Type u_1
M : Type u_2
inst : CommMonoid M
p : Finset ι
f : ι → M
rw :
  Eq.{u_2 + 1} (α := Associates M) (Multiset.prod (Multiset.map (fun (i : ι) ↦ Associates.mk (f i)) p.val))
    (Associates.mk (∏ i ∈ p, f i))
⊢ Eq.{u_2 + 1} (α := Associates M) (∏ i ∈ p, Associates.mk (f i)) (Associates.mk (∏ i ∈ p, f i))
have rw₁ : Eq (α := Associates M) (Multiset.prod (Multiset.map (Associates.mk ∘ f) p.val)) (Associates.mk (∏ i ∈ p, f i))
Tactic: rw [Finset.prod_eq_multiset_prod, ← Function.comp_def, ← Multiset.map_map, prod_mk,
    ← Finset.prod_eq_multiset_prod]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Associated (goal)
Goal:
ι : Type u_1
M : Type u_2
inst : CommMonoid M
p : Finset ι
f : ι → M
rw :
  Eq.{u_2 + 1} (α := Associates M) (Multiset.prod (Multiset.map (fun (i : ι) ↦ Associates.mk (f i)) p.val))
    (Associates.mk (∏ i ∈ p, f i))
rw₁ : Eq (α := Associates M) (Multiset.prod (Multiset.map (Associates.mk ∘ f) p.val)) (Associates.mk (∏ i ∈ p, f i))
⊢ Eq.{u_2 + 1} (α := Associates M) (∏ i ∈ p, Associates.mk (f i)) (Associates.mk (∏ i ∈ p, f i))
have rw₂ : Eq (α := Associates M) (Multiset.prod (Multiset.map Associates.mk (Multiset.map f p.val)))
  (Associates.mk (∏ i ∈ p, f i))
Tactic: rw [Finset.prod_eq_multiset_prod, ← Function.comp_def, ← Multiset.map_map, prod_mk,
    ← Finset.prod_eq_multiset_prod]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Associated (goal)
Goal:
ι : Type u_1
M : Type u_2
inst : CommMonoid M
p : Finset ι
f : ι → M
rw :
  Eq.{u_2 + 1} (α := Associates M) (Multiset.prod (Multiset.map (fun (i : ι) ↦ Associates.mk (f i)) p.val))
    (Associates.mk (∏ i ∈ p, f i))
rw₁ : Eq (α := Associates M) (Multiset.prod (Multiset.map (Associates.mk ∘ f) p.val)) (Associates.mk (∏ i ∈ p, f i))
rw₂ :
  Eq (α := Associates M) (Multiset.prod (Multiset.map Associates.mk (Multiset.map f p.val)))
    (Associates.mk (∏ i ∈ p, f i))
⊢ Eq.{u_2 + 1} (α := Associates M) (∏ i ∈ p, Associates.mk (f i)) (Associates.mk (∏ i ∈ p, f i))
have rw₃ : Eq (α := Associates M) (Associates.mk (Multiset.map f p.val).prod) (Associates.mk (∏ i ∈ p, f i))
Tactic: rw [Finset.prod_eq_multiset_prod, ← Function.comp_def, ← Multiset.map_map, prod_mk,
    ← Finset.prod_eq_multiset_prod]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Associated (goal)
Goal:
ι : Type u_1
M : Type u_2
inst : CommMonoid M
p : Finset ι
f : ι → M
rw :
  Eq.{u_2 + 1} (α := Associates M) (Multiset.prod (Multiset.map (fun (i : ι) ↦ Associates.mk (f i)) p.val))
    (Associates.mk (∏ i ∈ p, f i))
rw₁ : Eq (α := Associates M) (Multiset.prod (Multiset.map (Associates.mk ∘ f) p.val)) (Associates.mk (∏ i ∈ p, f i))
rw₂ :
  Eq (α := Associates M) (Multiset.prod (Multiset.map Associates.mk (Multiset.map f p.val)))
    (Associates.mk (∏ i ∈ p, f i))
rw₃ : Eq (α := Associates M) (Associates.mk (Multiset.map f p.val).prod) (Associates.mk (∏ i ∈ p, f i))
⊢ Eq.{u_2 + 1} (α := Associates M) (∏ i ∈ p, Associates.mk (f i)) (Associates.mk (∏ i ∈ p, f i))
have rw₄ : Eq.{u_2 + 1} (α := Associates M) (Associates.mk (∏ x ∈ p, f x)) (Associates.mk (∏ i ∈ p, f i))
Tactic: rw [Finset.prod_eq_multiset_prod, ← Function.comp_def, ← Multiset.map_map, prod_mk,
    ← Finset.prod_eq_multiset_prod]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Associated (goal)
Goal:
M : Type u_2
inst : CommMonoid M
p q : Multiset M
⊢ Multiset.Rel Associated p q ↔
    Eq (α := Multiset (Associates M)) (Multiset.map Associates.mk p) (Multiset.map Associates.mk q)
have rw : Multiset.Rel Associated p q ↔
  Multiset.Rel (fun (a b : M) ↦ Eq (α := Associates M) (Associates.mk a) (Associates.mk b)) p q
Tactic: rw [← Multiset.rel_eq, Multiset.rel_map]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Associated (goal)
Goal:
M : Type u_2
inst : CommMonoid M
p q : Multiset (Associates M)
h : p ≤ q
⊢ p.prod ≤ q.prod
have haveI : ∀ (this : DecidableEq (Associates M)), p.prod ≤ q.prod
Tactic: haveI := Classical.decEq (Associates M)
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Associated (goal)
Goal:
M : Type u_2
inst : CommMonoid M
p q : Multiset (Associates M)
h : p ≤ q
this_1 : DecidableEq (Associates M)
this : p.prod ≤ (p + (q - p)).prod
⊢ p.prod ≤ q.prod
have rwa : ∀ (this : p.prod ≤ q.prod), p.prod ≤ q.prod
Tactic: rwa [add_tsub_cancel_of_le h] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Associated (goal)
Goal:
M : Type u_2
inst : CommMonoid M
p q : Multiset (Associates M)
h : p ≤ q
this : DecidableEq (Associates M)
⊢ p.prod ≤ q.prod
have suffices : p.prod ≤ (p + (q - p)).prod
Tactic: suffices p.prod ≤ (p + (q - p)).prod by rwa [add_tsub_cancel_of_le h] at this
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Associated (goal)
Goal:
M : Type u_2
inst : CommMonoid M
p q : Multiset (Associates M)
h : p ≤ q
this : DecidableEq (Associates M)
⊢ p.prod ≤ (p + (q - p)).prod
have suffices : p.prod * 1 ≤ p.prod * (q - p).prod
Tactic: suffices p.prod * 1 ≤ p.prod * (q - p).prod by simpa
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Balance (goal)
Goal:
ι : Type u_1
G : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup G
inst_2 : Module ℚ≥0 G
f : ι → G
⊢ Eq.{u_4 + 1} (α := G) (∑ x : ι, balance f x) 0
have inl : IsEmpty ι → Eq.{u_4 + 1} (α := G) (∑ x : ι, balance f x) 0
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Balance (goal)
Goal:
ι : Type u_1
G : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup G
inst_2 : Module ℚ≥0 G
f : ι → G
inl : IsEmpty ι → Eq.{u_4 + 1} (α := G) (∑ x : ι, balance f x) 0
⊢ Eq.{u_4 + 1} (α := G) (∑ x : ι, balance f x) 0
have inr : Nonempty ι → Eq.{u_4 + 1} (α := G) (∑ x : ι, balance f x) 0
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Balance (goal)
Goal:
ι : Type u_1
G : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup G
inst_2 : Module ℚ≥0 G
f : ι → G
⊢ balance (balance f) = balance f
have inl : IsEmpty ι → balance (balance f) = balance f
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Balance (goal)
Goal:
ι : Type u_1
G : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup G
inst_2 : Module ℚ≥0 G
f : ι → G
inl : IsEmpty ι → balance (balance f) = balance f
⊢ balance (balance f) = balance f
have inr : Nonempty ι → balance (balance f) = balance f
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Balance (goal)
Goal:
ι : Type u_1
G : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup G
inst_2 : Module ℚ≥0 G
f : ι → G
h : IsEmpty ι
⊢ balance (balance f) = balance f
have inl : ∀ (x : ι), balance (balance f) x = balance f x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Balance (goal)
Goal:
ι : Type u_1
G : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup G
inst_2 : Module ℚ≥0 G
f : ι → G
h : Nonempty ι
⊢ balance (balance f) = balance f
have inr : ∀ (x : ι), balance (balance f) x = balance f x
Tactic: ext x
-- 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
f : ι → M
inst_2 : Fintype ι
⊢ 𝔼 i : ι, f i = HSMul.hSMul (α := ℚ≥0) (β := M) (↑(Fintype.card ι) : ℚ≥0)⁻¹ (∑ i : ι, f i)
have rw : HSMul.hSMul (α := ℚ≥0) (β := M) (↑(card.{u_1} (α := ι) univ) : ℚ≥0)⁻¹ (∑ i : ι, f i) =
  HSMul.hSMul (α := ℚ≥0) (β := M) (↑(Fintype.card ι) : ℚ≥0)⁻¹ (∑ i : ι, f i)
Tactic: rw [expect, card_univ]
-- 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
f : ι → M
inst_2 : Fintype ι
rw :
  HSMul.hSMul (α := ℚ≥0) (β := M) (↑(card.{u_1} (α := ι) univ) : ℚ≥0)⁻¹ (∑ i : ι, f i) =
    HSMul.hSMul (α := ℚ≥0) (β := M) (↑(Fintype.card ι) : ℚ≥0)⁻¹ (∑ i : ι, f i)
⊢ 𝔼 i : ι, f i = HSMul.hSMul (α := ℚ≥0) (β := M) (↑(Fintype.card ι) : ℚ≥0)⁻¹ (∑ i : ι, f i)
have rw₁ : HSMul.hSMul (α := ℚ≥0) (β := M) (↑(Fintype.card ι) : ℚ≥0)⁻¹ (∑ i : ι, f i) =
  HSMul.hSMul (α := ℚ≥0) (β := M) (↑(Fintype.card ι) : ℚ≥0)⁻¹ (∑ i : ι, f i)
Tactic: rw [expect, card_univ]
-- 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 g : ι → M
t : Finset ι
hst : s = t
h : ∀ i ∈ t, f i = g i
⊢ Eq.{u_3 + 1} (α := M) (𝔼 i ∈ s, f i) (𝔼 i ∈ t, g i)
have rw : HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#s) : ℚ≥0)⁻¹ (∑ i ∈ s, f i) = 𝔼 i ∈ t, g i
Tactic: rw [expect, expect, sum_congr hst h, hst]
-- 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 g : ι → M
t : Finset ι
hst : s = t
h : ∀ i ∈ t, f i = g i
rw : HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#s) : ℚ≥0)⁻¹ (∑ i ∈ s, f i) = 𝔼 i ∈ t, g i
⊢ Eq.{u_3 + 1} (α := M) (𝔼 i ∈ s, f i) (𝔼 i ∈ t, g i)
have rw₁ : HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#s) : ℚ≥0)⁻¹ (∑ i ∈ s, f i) =
  HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#t) : ℚ≥0)⁻¹ (∑ i ∈ t, g i)
Tactic: rw [expect, expect, sum_congr hst h, hst]
-- 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 g : ι → M
t : Finset ι
hst : s = t
h : ∀ i ∈ t, f i = g i
rw : HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#s) : ℚ≥0)⁻¹ (∑ i ∈ s, f i) = 𝔼 i ∈ t, g i
rw₁ :
  HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#s) : ℚ≥0)⁻¹ (∑ i ∈ s, f i) =
    HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#t) : ℚ≥0)⁻¹ (∑ i ∈ t, g i)
⊢ Eq.{u_3 + 1} (α := M) (𝔼 i ∈ s, f i) (𝔼 i ∈ t, g i)
have rw₂ : HSMul.hSMul (α := ℚ≥0) (↑(#s) : ℚ≥0)⁻¹ (t.sum g) = HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#t) : ℚ≥0)⁻¹ (∑ i ∈ t, g i)
Tactic: rw [expect, expect, sum_congr hst h, hst]
-- 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 g : ι → M
t : Finset ι
hst : s = t
h : ∀ i ∈ t, f i = g i
rw : HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#s) : ℚ≥0)⁻¹ (∑ i ∈ s, f i) = 𝔼 i ∈ t, g i
rw₁ :
  HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#s) : ℚ≥0)⁻¹ (∑ i ∈ s, f i) =
    HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#t) : ℚ≥0)⁻¹ (∑ i ∈ t, g i)
rw₂ : HSMul.hSMul (α := ℚ≥0) (↑(#s) : ℚ≥0)⁻¹ (t.sum g) = HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#t) : ℚ≥0)⁻¹ (∑ i ∈ t, g i)
⊢ Eq.{u_3 + 1} (α := M) (𝔼 i ∈ s, f i) (𝔼 i ∈ t, g i)
have rw₃ : HSMul.hSMul (α := ℚ≥0) (↑(#t) : ℚ≥0)⁻¹ (t.sum g) = HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#t) : ℚ≥0)⁻¹ (∑ i ∈ t, g i)
Tactic: rw [expect, expect, sum_congr hst h, hst]
-- 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 t : Finset ι
f g : ι → M
p q : ι → Prop
inst_2 : DecidablePred p
inst_3 : DecidablePred q
hst : s = t
hpq : ∀ i ∈ t, p i ↔ q i
h : ∀ i ∈ t, q i → f i = g i
⊢ {i ∈ s | p i} = {i ∈ t | q i}
have rw : {i ∈ t | p i} = {i ∈ t | q i}
Tactic: rw [hst, filter_inj'.2 hpq]
-- 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 t : Finset ι
f g : ι → M
p q : ι → Prop
inst_2 : DecidablePred p
inst_3 : DecidablePred q
hst : s = t
hpq : ∀ i ∈ t, p i ↔ q i
h : ∀ i ∈ t, q i → f i = g i
rw : {i ∈ t | p i} = {i ∈ t | q i}
⊢ {i ∈ s | p i} = {i ∈ t | q i}
have rw₁ : filter q t = {i ∈ t | q i}
Tactic: rw [hst, filter_inj'.2 hpq]
-- 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
⊢ Eq.{u_3 + 1} (α := M) (𝔼 i ∈ s, 𝔼 j ∈ t, f i j) (𝔼 j ∈ t, 𝔼 i ∈ s, f i j)
have rw : HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#s) : ℚ≥0)⁻¹ (∑ 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]
-- 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
⊢ Eq.{u_3 + 1} (α := M) (𝔼 i ∈ s, 𝔼 j ∈ t, f i j) (𝔼 j ∈ t, 𝔼 i ∈ s, f i j)
have 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)
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)
⊢ Eq.{u_3 + 1} (α := M) (𝔼 i ∈ s, 𝔼 j ∈ t, f i j) (𝔼 j ∈ t, 𝔼 i ∈ s, f i j)
have 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)
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)
⊢ Eq.{u_3 + 1} (α := M) (𝔼 i ∈ s, 𝔼 j ∈ t, f i j) (𝔼 j ∈ t, 𝔼 i ∈ s, f i j)
have 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)
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)
⊢ Eq.{u_3 + 1} (α := M) (𝔼 i ∈ s, 𝔼 j ∈ t, f i j) (𝔼 j ∈ t, 𝔼 i ∈ s, f i j)
have 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)
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)
⊢ Eq.{u_3 + 1} (α := M) (𝔼 i ∈ s, 𝔼 j ∈ t, f i j) (𝔼 j ∈ t, 𝔼 i ∈ s, f i j)
have 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))
Tactic: rw [expect, expect, ← expect_sum_comm, ← expect_sum_comm, expect, expect, smul_comm, sum_comm]