awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Finset (goal)
Goal:
ι : Type u_5
s : Finset ι
f : ι → ℕ
n : ℕ
hf : ∀ i ∈ s, n ∣ f i
inl : ∀ (hf : ∀ i ∈ s, 0 ∣ f i), HDiv.hDiv (α := ℕ) (∑ i ∈ s, f i) 0 = ∑ i ∈ s, f i / 0
⊢ (∑ i ∈ s, f i) / n = ∑ i ∈ s, f i / n
have inr : ∀ (hn : n > 0), (∑ i ∈ s, f i) / n = ∑ i ∈ s, f i / n
Tactic: obtain rfl | hn := n.eq_zero_or_pos
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Finset (goal)
Goal:
ι : Type u_5
s : Finset ι
f : ι → ℕ
n : ℕ
hf : ∀ i ∈ s, n ∣ f i
hn : n > 0
⊢ (∑ i ∈ s, f i) / n = ∑ i ∈ s, f i / n
have inr : Eq (α := ℕ) (∑ i ∈ s, f i) (∑ i ∈ s, f i / n * n)
Tactic: rw [Nat.div_eq_iff_eq_mul_left hn (dvd_sum hf), sum_mul]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Finset (goal)
Goal:
ι : Type u_5
s : Finset ι
f : ι → ℕ
n : ℕ
hf : ∀ i ∈ s, n ∣ f i
hn : n > 0
⊢ Eq (α := ℕ) (∑ i ∈ s, f i) (∑ i ∈ s, f i / n * n)
have inr : ∀ (s_1 : ι) (hs : s_1 ∈ s), f s_1 = f s_1 / n * n
Tactic: refine sum_congr rfl fun s hs ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Finset (goal)
Goal:
ι : Type u_5
s_1 : Finset ι
f : ι → ℕ
n : ℕ
hf : ∀ i ∈ s_1, n ∣ f i
hn : n > 0
s : ι
hs : s ∈ s_1
⊢ f s = f s / n * n
have inr : f s = f s
Tactic: rw [Nat.div_mul_cancel (hf _ hs)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Finset (goal)
Goal:
ι : Type u_5
s : Finset ι
f : ι → ℤ
n : ℤ
hf : ∀ i ∈ s, n ∣ f i
⊢ (∑ i ∈ s, f i) / n = ∑ i ∈ s, f i / n
have inl : ∀ (hf : ∀ i ∈ s, 0 ∣ f i), HDiv.hDiv (α := ℤ) (∑ i ∈ s, f i) 0 = ∑ i ∈ s, f i / 0
Tactic: obtain rfl | hn := eq_or_ne n 0
Cleared hypotheses: n, hf
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Finset (goal)
Goal:
ι : Type u_5
s : Finset ι
f : ι → ℤ
n : ℤ
hf : ∀ i ∈ s, n ∣ f i
inl : ∀ (hf : ∀ i ∈ s, 0 ∣ f i), HDiv.hDiv (α := ℤ) (∑ i ∈ s, f i) 0 = ∑ i ∈ s, f i / 0
⊢ (∑ i ∈ s, f i) / n = ∑ i ∈ s, f i / n
have inr : ∀ (hn : n ≠ 0), (∑ i ∈ s, f i) / n = ∑ i ∈ s, f i / n
Tactic: obtain rfl | hn := eq_or_ne n 0
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Finset (goal)
Goal:
ι : Type u_5
s : Finset ι
f : ι → ℤ
n : ℤ
hf : ∀ i ∈ s, n ∣ f i
hn : n ≠ 0
⊢ (∑ i ∈ s, f i) / n = ∑ i ∈ s, f i / n
have inr : Eq (α := ℤ) (∑ i ∈ s, f i) (∑ i ∈ s, f i / n * n)
Tactic: rw [Int.ediv_eq_iff_eq_mul_left hn (dvd_sum hf), sum_mul]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Finset (goal)
Goal:
ι : Type u_5
s : Finset ι
f : ι → ℤ
n : ℤ
hf : ∀ i ∈ s, n ∣ f i
hn : n ≠ 0
⊢ Eq (α := ℤ) (∑ i ∈ s, f i) (∑ i ∈ s, f i / n * n)
have inr : ∀ (s_1 : ι) (hs : s_1 ∈ s), f s_1 = f s_1 / n * n
Tactic: refine sum_congr rfl fun s hs ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Finset (goal)
Goal:
ι : Type u_5
s_1 : Finset ι
f : ι → ℤ
n : ℤ
hf : ∀ i ∈ s_1, n ∣ f i
hn : n ≠ 0
s : ι
hs : s ∈ s_1
⊢ f s = f s / n * n
have inr : f s = f s
Tactic: rw [Int.ediv_mul_cancel (hf _ hs)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.List (goal)
Goal:
R : Type u_5
inst : NonUnitalNonAssocSemiring R
a x : R
xs : List R
ih : ∀ (h : ∀ (b : R), b ∈ xs → Commute a b), Commute a xs.sum
h : ∀ (b : R), b ∈ x :: xs → Commute a b
⊢ Commute a (x :: xs).sum
have cons : Commute a (x + xs.sum)
Tactic: rw [List.sum_cons]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.List (goal)
Goal:
R : Type u_5
inst : NonUnitalNonAssocSemiring R
a : R
l : List R
h : ∀ (b : R), b ∈ l → Commute a b
⊢ Commute a l.sum
have nil : ∀ (h : ∀ (b : R), Membership.mem (γ := List R) [] b → Commute a b), Commute a (sum [])
Tactic: induction l with
  | nil => exact Commute.zero_right _
  | cons x xs ih =>
    rw [List.sum_cons]
    exact (h _ mem_cons_self).add_right (ih fun j hj ↦ h _ <| mem_cons_of_mem _ hj)
Cleared hypotheses: l, h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.List (goal)
Goal:
R : Type u_5
inst : NonUnitalNonAssocSemiring R
a : R
l : List R
h : ∀ (b : R), b ∈ l → Commute a b
nil : ∀ (h : ∀ (b : R), Membership.mem (γ := List R) [] b → Commute a b), Commute a (sum [])
⊢ Commute a l.sum
have cons : ∀ (x : R) (xs : List R) (ih : ∀ (h : ∀ (b : R), b ∈ xs → Commute a b), Commute a xs.sum)
  (h : ∀ (b : R), b ∈ x :: xs → Commute a b), Commute a (x :: xs).sum
Tactic: induction l with
  | nil => exact Commute.zero_right _
  | cons x xs ih =>
    rw [List.sum_cons]
    exact (h _ mem_cons_self).add_right (ih fun j hj ↦ h _ <| mem_cons_of_mem _ hj)
Cleared hypotheses: l, h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.List (goal)
Goal:
M : Type u_3
inst : Monoid M
inst_1 : HasDistribNeg M
l : List M
⊢ (map Neg.neg l).prod = HPow.hPow (α := M) (-1) l.length * l.prod
have nil : prod (map Neg.neg []) = HPow.hPow (α := M) (-1) (length.{u_3} (α := M) []) * prod []
Tactic: induction l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.List (goal)
Goal:
M : Type u_3
inst : Monoid M
inst_1 : HasDistribNeg M
l : List M
nil : prod (map Neg.neg []) = HPow.hPow (α := M) (-1) (length.{u_3} (α := M) []) * prod []
⊢ (map Neg.neg l).prod = HPow.hPow (α := M) (-1) l.length * l.prod
have cons : ∀ (head : M) (tail : List M),
  (map Neg.neg tail).prod = HPow.hPow (α := M) (-1) tail.length * tail.prod →
    (map Neg.neg (head :: tail)).prod = HPow.hPow (α := M) (-1) (head :: tail).length * (head :: tail).prod
Tactic: induction l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.List (goal)
Goal:
M₀ : Type u_4
inst : MonoidWithZero M₀
a : M₀
l : List M₀
h : 0 ∈ a :: l
⊢ (a :: l).prod = 0
have rw : a * l.prod = 0
Tactic: rw [prod_cons]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.List (goal)
Goal:
M₀ : Type u_4
inst : MonoidWithZero M₀
a : M₀
l : List M₀
h : 0 ∈ a :: l
⊢ a * l.prod = 0
have inl : ∀ (ha : 0 = a), a * l.prod = 0
Tactic: rcases mem_cons.1 h with ha | hl
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.List (goal)
Goal:
M₀ : Type u_4
inst : MonoidWithZero M₀
a : M₀
l : List M₀
h : 0 ∈ a :: l
inl : ∀ (ha : 0 = a), a * l.prod = 0
⊢ a * l.prod = 0
have inr : ∀ (hl : 0 ∈ l), a * l.prod = 0
Tactic: rcases mem_cons.1 h with ha | hl
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.List (goal)
Goal:
M₀ : Type u_4
inst : MonoidWithZero M₀
inst_1 : Nontrivial M₀
inst_2 : NoZeroDivisors M₀
a : M₀
l : List M₀
⊢ (a :: l).prod = 0 ↔ 0 ∈ a :: l
have rw : a * l.prod = 0 ↔ 0 ∈ a :: l
Tactic: rw [prod_cons, mul_eq_zero, prod_eq_zero_iff, mem_cons, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.List (goal)
Goal:
M₀ : Type u_4
inst : MonoidWithZero M₀
inst_1 : Nontrivial M₀
inst_2 : NoZeroDivisors M₀
a : M₀
l : List M₀
rw : a * l.prod = 0 ↔ 0 ∈ a :: l
⊢ (a :: l).prod = 0 ↔ 0 ∈ a :: l
have rw₁ : a = 0 ∨ l.prod = 0 ↔ 0 ∈ a :: l
Tactic: rw [prod_cons, mul_eq_zero, prod_eq_zero_iff, mem_cons, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.List (goal)
Goal:
M₀ : Type u_4
inst : MonoidWithZero M₀
inst_1 : Nontrivial M₀
inst_2 : NoZeroDivisors M₀
a : M₀
l : List M₀
rw : a * l.prod = 0 ↔ 0 ∈ a :: l
rw₁ : a = 0 ∨ l.prod = 0 ↔ 0 ∈ a :: l
⊢ (a :: l).prod = 0 ↔ 0 ∈ a :: l
have rw₂ : a = 0 ∨ 0 ∈ l ↔ 0 ∈ a :: l
Tactic: rw [prod_cons, mul_eq_zero, prod_eq_zero_iff, mem_cons, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.List (goal)
Goal:
M₀ : Type u_4
inst : MonoidWithZero M₀
inst_1 : Nontrivial M₀
inst_2 : NoZeroDivisors M₀
a : M₀
l : List M₀
rw : a * l.prod = 0 ↔ 0 ∈ a :: l
rw₁ : a = 0 ∨ l.prod = 0 ↔ 0 ∈ a :: l
rw₂ : a = 0 ∨ 0 ∈ l ↔ 0 ∈ a :: l
⊢ (a :: l).prod = 0 ↔ 0 ∈ a :: l
have rw₃ : a = 0 ∨ 0 ∈ l ↔ 0 = a ∨ 0 ∈ l
Tactic: rw [prod_cons, mul_eq_zero, prod_eq_zero_iff, mem_cons, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.List (goal)
Goal:
M₀ : Type u_4
inst : MonoidWithZero M₀
inst_1 : Nontrivial M₀
inst_2 : NoZeroDivisors M₀
a : M₀
l : List M₀
rw : a * l.prod = 0 ↔ 0 ∈ a :: l
rw₁ : a = 0 ∨ l.prod = 0 ↔ 0 ∈ a :: l
rw₂ : a = 0 ∨ 0 ∈ l ↔ 0 ∈ a :: l
rw₃ : a = 0 ∨ 0 ∈ l ↔ 0 = a ∨ 0 ∈ l
⊢ (a :: l).prod = 0 ↔ 0 ∈ a :: l
have rw₄ : 0 = a ∨ 0 ∈ l ↔ 0 = a ∨ 0 ∈ l
Tactic: rw [prod_cons, mul_eq_zero, prod_eq_zero_iff, mem_cons, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.List (goal)
Goal:
R : Type u_5
inst : NonUnitalSemiring R
a x : R
l : List R
ih : ∀ (h : ∀ (x : R), x ∈ l → a ∣ x), a ∣ l.sum
h : ∀ (x_1 : R), x_1 ∈ x :: l → a ∣ x_1
⊢ a ∣ (x :: l).sum
have cons : a ∣ x + l.sum
Tactic: rw [List.sum_cons]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.List (goal)
Goal:
R : Type u_5
inst : NonUnitalSemiring R
a : R
l : List R
h : ∀ (x : R), x ∈ l → a ∣ x
⊢ a ∣ l.sum
have nil : ∀ (h : ∀ (x : R), Membership.mem (γ := List R) [] x → a ∣ x), a ∣ sum []
Tactic: induction l with
  | nil => exact dvd_zero _
  | cons x l ih =>
    rw [List.sum_cons]
    exact dvd_add (h _ mem_cons_self) (ih fun x hx ↦ h x (mem_cons_of_mem _ hx))
Cleared hypotheses: l, h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.List (goal)
Goal:
R : Type u_5
inst : NonUnitalSemiring R
a : R
l : List R
h : ∀ (x : R), x ∈ l → a ∣ x
nil : ∀ (h : ∀ (x : R), Membership.mem (γ := List R) [] x → a ∣ x), a ∣ sum []
⊢ a ∣ l.sum
have cons : ∀ (x : R) (l : List R) (ih : ∀ (h : ∀ (x : R), x ∈ l → a ∣ x), a ∣ l.sum) (h : ∀ (x_1 : R), x_1 ∈ x :: l → a ∣ x_1),
  a ∣ (x :: l).sum
Tactic: induction l with
  | nil => exact dvd_zero _
  | cons x l ih =>
    rw [List.sum_cons]
    exact dvd_add (h _ mem_cons_self) (ih fun x hx ↦ h x (mem_cons_of_mem _ hx))
Cleared hypotheses: l, h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Multiset (goal)
Goal:
M₀ : Type u_3
inst : CommMonoidWithZero M₀
s : Multiset M₀
h : 0 ∈ s
⊢ s.prod = 0
have rcases : ∀ (s' : Multiset M₀) (hs' : s = 0 ::ₘ s'), s.prod = 0
Tactic: rcases Multiset.exists_cons_of_mem h with ⟨s', hs'⟩
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Multiset (goal)
Goal:
R : Type u_4
inst : NonUnitalSemiring R
s_1 : Multiset R
a x : R
s : Multiset R
ih : (∀ (x : R), x ∈ s → a ∣ x) → a ∣ s.sum
h : ∀ (x_1 : R), x_1 ∈ x ::ₘ s → a ∣ x_1
⊢ a ∣ (x ::ₘ s).sum
have rw : a ∣ x + s.sum
Tactic: rw [sum_cons]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Multiset (goal)
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
s : Multiset ι
f g : ι → R
⊢ Eq.{u_4 + 1} (α := R) (prod (map (fun (i : ι) ↦ f i + g i) s))
    (sum (map (fun (p : Multiset ι × Multiset ι) ↦ (map f p.1).prod * (map g p.2).prod) s.antidiagonal))
have refine_1 : Eq.{u_4 + 1} (α := R) (prod (map (fun (i : ι) ↦ f i + g i) 0))
  (sum (map (fun (p : Multiset ι × Multiset ι) ↦ (map f p.1).prod * (map g p.2).prod) (antidiagonal 0)))
Tactic: refine s.induction_on ?_ fun a s ih ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Multiset (goal)
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
s : Multiset ι
f g : ι → R
refine_1 :
  Eq.{u_4 + 1} (α := R) (prod (map (fun (i : ι) ↦ f i + g i) 0))
    (sum (map (fun (p : Multiset ι × Multiset ι) ↦ (map f p.1).prod * (map g p.2).prod) (antidiagonal 0)))
⊢ Eq.{u_4 + 1} (α := R) (prod (map (fun (i : ι) ↦ f i + g i) s))
    (sum (map (fun (p : Multiset ι × Multiset ι) ↦ (map f p.1).prod * (map g p.2).prod) s.antidiagonal))
have refine_2 : ∀ (a : ι) (s : Multiset ι)
  (ih :
    Eq.{u_4 + 1} (α := R) (prod (map (fun (i : ι) ↦ f i + g i) s))
      (sum (map (fun (p : Multiset ι × Multiset ι) ↦ (map f p.1).prod * (map g p.2).prod) s.antidiagonal))),
  Eq.{u_4 + 1} (α := R) (prod (map (fun (i : ι) ↦ f i + g i) (a ::ₘ s)))
    (sum (map (fun (p : Multiset ι × Multiset ι) ↦ (map f p.1).prod * (map g p.2).prod) (a ::ₘ s).antidiagonal))
Tactic: refine s.induction_on ?_ fun a s ih ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Multiset (goal)
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
s_1 : Multiset ι
f g : ι → R
a : ι
s : Multiset ι
ih :
  Eq.{u_4 + 1} (α := R) (prod (map (fun (i : ι) ↦ f i + g i) s))
    (sum (map (fun (p : Multiset ι × Multiset ι) ↦ (map f p.1).prod * (map g p.2).prod) s.antidiagonal))
⊢ Eq.{u_4 + 1} (α := R) (prod (map (fun (i : ι) ↦ f i + g i) (a ::ₘ s)))
    (sum (map (fun (p : Multiset ι × Multiset ι) ↦ (map f p.1).prod * (map g p.2).prod) (a ::ₘ s).antidiagonal))
have refine_2 : HAdd.hAdd (α := R)
    (sum (map (fun (i : Multiset ι × Multiset ι) ↦ (map f i.1).prod * (f a * (map g i.2).prod)) s.antidiagonal))
    (sum (map (fun (i : Multiset ι × Multiset ι) ↦ (map f i.1).prod * (g a * (map g i.2).prod)) s.antidiagonal)) =
  HAdd.hAdd (α := R)
    (sum (map (fun (x : Multiset ι × Multiset ι) ↦ (map f x.1).prod * (g a * (map g x.2).prod)) s.antidiagonal))
    (sum (map (fun (i : Multiset ι × Multiset ι) ↦ (map f i.1).prod * (f a * (map g i.2).prod)) s.antidiagonal))
Tactic: simp only [map_cons, prod_cons, ih, sum_map_mul_left.symm, add_mul, mul_left_comm (f a),
      mul_left_comm (g a), sum_map_add, antidiagonal_cons, Prod.map_fst, Prod.map_snd,
      id_eq, map_add, map_map, Function.comp_apply, mul_assoc, sum_add]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Multiset (goal)
Goal:
R : Type u_4
inst : NonUnitalNonAssocSemiring R
s : Multiset R
a : R
h : ∀ (b : R), b ∈ s → Commute a b
⊢ Commute a s.sum
have h₁ : ∀ (a_1 : List R) (h : ∀ (b : R), b ∈ ⟦a_1⟧ → Commute a b), Commute a (sum ⟦a_1⟧)
Tactic: induction s using Quotient.inductionOn
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Nat (goal)
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ Even (α := ℕ) (∑ i ∈ s, f i) ↔ Even #({x ∈ s | Odd (f x)})
have rw : (Even (α := ℕ) (∑ x ∈ s with Even (f x), f x) ↔ Even (α := ℕ) (∑ x ∈ s with ¬Even (f x), f x)) ↔
  Even #({x ∈ s | Odd (f x)})
Tactic: rw [← Finset.sum_filter_add_sum_filter_not _ (fun x ↦ Even (f x)), Nat.even_add]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Nat (goal)
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ (Even (α := ℕ) (∑ x ∈ s with Even (f x), f x) ↔ Even (α := ℕ) (∑ x ∈ s with ¬Even (f x), f x)) ↔
    Even #({x ∈ s | Odd (f x)})
have simp : Even (α := ℕ) (∑ x ∈ s with ¬Even (f x), f x) ↔ Even #({x ∈ s | Odd (f x)})
Tactic: simp only [Finset.mem_filter, and_imp, imp_self, implies_true, Finset.even_sum, true_iff]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Nat (goal)
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ Even (α := ℕ) (∑ x ∈ s with ¬Even (f x), f x) ↔ Even #({x ∈ s | Odd (f x)})
have rw : HMod.hMod (α := ℕ) (∑ a ∈ s, if ¬Even (f a) then f a % 2 else 0) 2 = 0 ↔ Even #({x ∈ s | Odd (f x)})
Tactic: rw [Nat.even_iff, Finset.sum_nat_mod, Finset.sum_filter]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Nat (goal)
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ HMod.hMod (α := ℕ) (∑ a ∈ s, if ¬Even (f a) then f a % 2 else 0) 2 = 0 ↔ Even #({x ∈ s | Odd (f x)})
have simp : HMod.hMod (α := ℕ) (∑ x ∈ s, if Odd (f x) then 1 else 0) 2 = 0 ↔ Even #({x ∈ s | Odd (f x)})
Tactic: simp +contextual only [Nat.not_even_iff_odd, Nat.odd_iff.mp]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Nat (goal)
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ HMod.hMod (α := ℕ) (∑ x ∈ s, if Odd (f x) then 1 else 0) 2 = 0 ↔ Even #({x ∈ s | Odd (f x)})
have simp_rw : HMod.hMod (α := ℕ) (∑ a ∈ s with Odd (f a), 1) 2 = 0 ↔ Even #({a ∈ s | Odd (f a)})
Tactic: simp_rw [← Finset.sum_filter, ← Nat.even_iff, Finset.card_eq_sum_ones]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Nat (goal)
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℕ
simp_rw : HMod.hMod (α := ℕ) (∑ a ∈ s with Odd (f a), 1) 2 = 0 ↔ Even #({a ∈ s | Odd (f a)})
⊢ HMod.hMod (α := ℕ) (∑ x ∈ s, if Odd (f x) then 1 else 0) 2 = 0 ↔ Even #({x ∈ s | Odd (f x)})
have simp_rw₁ : Even (α := ℕ) (∑ a ∈ s with Odd (f a), 1) ↔ Even #({a ∈ s | Odd (f a)})
Tactic: simp_rw [← Finset.sum_filter, ← Nat.even_iff, Finset.card_eq_sum_ones]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Nat (goal)
Goal:
ι : Type u_1
M : Type u_2
f : ι → M
s : Finset M
hb : ∀ b ∈ s, Set.Finite.{u_1} (α := ι) {a : ι | f a = b}
t : Finset M := Set.Finite.toFinset (s := (↑s : Set M) ∩ Set.range f) ⋯
⊢ Nat.card.{u_1} (↑(f ⁻¹' (↑s : Set M)) : Type u_1) = ∑ b ∈ s, Nat.card.{u_1} { a : ι // f a = b }
have rw : Nat.card.{u_1} (↑(f ⁻¹' (↑t : Set M)) : Type u_1) = ∑ b ∈ s, Nat.card.{u_1} { a : ι // f a = b }
Tactic: rw [show Nat.card (f ⁻¹' s) = Nat.card (f ⁻¹' t) by simp [t]]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Nat (goal)
Goal:
ι : Type u_1
M : Type u_2
f : ι → M
s : Finset M
hb : ∀ b ∈ s, Set.Finite.{u_1} (α := ι) {a : ι | f a = b}
t : Finset M := Set.Finite.toFinset (s := (↑s : Set M) ∩ Set.range f) ⋯
⊢ Nat.card.{u_1} (↑(f ⁻¹' (↑t : Set M)) : Type u_1) = ∑ b ∈ s, Nat.card.{u_1} { a : ι // f a = b }
have rw : Nat.card.{u_1} (↑(f ⁻¹' (↑t : Set M)) : Type u_1) = ∑ b ∈ t, Nat.card.{u_1} (↑{a : ι | f a = b} : Type u_1)
Tactic: rw [show ∑ b ∈ s, Nat.card {a //f a = b} = ∑ b ∈ t, Nat.card {a | f a = b} by
    exact (Finset.sum_subset (by simp [t]) (by aesop)).symm]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Nat (hypothesis)
Goal:
ι : Type u_1
M : Type u_2
f : ι → M
s : Finset M
hb : ∀ b ∈ s, Set.Finite.{u_1} (α := ι) {a : ι | f a = b}
t : Finset M := Set.Finite.toFinset (s := (↑s : Set M) ∩ Set.range f) ⋯
⊢ Nat.card.{u_1} (↑(f ⁻¹' (↑t : Set M)) : Type u_1) = ∑ b ∈ t, Nat.card.{u_1} (↑{a : ι | f a = b} : Type u_1)
have ht : (f ⁻¹' (↑t : Set M)).Finite
Tactic: have ht : Set.Finite (f ⁻¹' t) := Set.Finite.preimage' (finite_toSet t) (by aesop)
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Nat (goal)
Goal:
ι : Type u_1
M : Type u_2
f : ι → M
s : Finset M
hb : ∀ b ∈ s, Set.Finite.{u_1} (α := ι) {a : ι | f a = b}
t : Finset M := Set.Finite.toFinset (s := (↑s : Set M) ∩ Set.range f) ⋯
ht : (f ⁻¹' (↑t : Set M)).Finite
⊢ Nat.card.{u_1} (↑(f ⁻¹' (↑t : Set M)) : Type u_1) = ∑ b ∈ t, Nat.card.{u_1} (↑{a : ι | f a = b} : Type u_1)
have rw : Eq (α := ℕ)
  (∑ b ∈ image f (ht.toFinset (s := f ⁻¹' (↑t : Set M))), #({a ∈ ht.toFinset (s := f ⁻¹' (↑t : Set M)) | f a = b}))
  (∑ b ∈ t, Nat.card.{u_1} (↑{a : ι | f a = b} : Type u_1))
Tactic: rw [Nat.card_eq_card_finite_toFinset ht, Finset.card_eq_sum_card_image (f := f)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Nat (goal)
Goal:
ι : Type u_1
M : Type u_2
f : ι → M
s : Finset M
hb : ∀ b ∈ s, Set.Finite.{u_1} (α := ι) {a : ι | f a = b}
t : Finset M := Set.Finite.toFinset (s := (↑s : Set M) ∩ Set.range f) ⋯
ht : (f ⁻¹' (↑t : Set M)).Finite
⊢ Eq (α := ℕ)
    (∑ b ∈ image f (ht.toFinset (s := f ⁻¹' (↑t : Set M))), #({a ∈ ht.toFinset (s := f ⁻¹' (↑t : Set M)) | f a = b}))
    (∑ b ∈ t, Nat.card.{u_1} (↑{a : ι | f a = b} : Type u_1))
have refine_1 : image f (ht.toFinset (s := f ⁻¹' (↑t : Set M))) = t
Tactic: refine Finset.sum_congr ?_ fun m hm ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Nat (goal)
Goal:
ι : Type u_1
M : Type u_2
f : ι → M
s : Finset M
hb : ∀ b ∈ s, Set.Finite.{u_1} (α := ι) {a : ι | f a = b}
t : Finset M := Set.Finite.toFinset (s := (↑s : Set M) ∩ Set.range f) ⋯
ht : (f ⁻¹' (↑t : Set M)).Finite
refine_1 : image f (ht.toFinset (s := f ⁻¹' (↑t : Set M))) = t
⊢ Eq (α := ℕ)
    (∑ b ∈ image f (ht.toFinset (s := f ⁻¹' (↑t : Set M))), #({a ∈ ht.toFinset (s := f ⁻¹' (↑t : Set M)) | f a = b}))
    (∑ b ∈ t, Nat.card.{u_1} (↑{a : ι | f a = b} : Type u_1))
have refine_2 : ∀ (m : M) (hm : m ∈ t),
  #({a ∈ ht.toFinset (s := f ⁻¹' (↑t : Set M)) | f a = m}) = Nat.card.{u_1} (↑{a : ι | f a = m} : Type u_1)
Tactic: refine Finset.sum_congr ?_ fun m hm ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Nat (goal)
Goal:
ι : Type u_1
M : Type u_2
f : ι → M
s : Finset M
hb : ∀ b ∈ s, Set.Finite.{u_1} (α := ι) {a : ι | f a = b}
t : Finset M := Set.Finite.toFinset (s := (↑s : Set M) ∩ Set.range f) ⋯
ht : (f ⁻¹' (↑t : Set M)).Finite
m : M
hm : m ∈ t
⊢ #({a ∈ ht.toFinset (s := f ⁻¹' (↑t : Set M)) | f a = m}) = Nat.card.{u_1} (↑{a : ι | f a = m} : Type u_1)
have refine_2 : #({a ∈ ht.toFinset (s := f ⁻¹' (↑t : Set M)) | f a = m}) = #(sorry.toFinset (s := {a : ι | f a = m}))
Tactic: rw [Nat.card_eq_card_finite_toFinset (hb _ (by aesop))]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Nat (goal)
Goal:
ι : Type u_1
M : Type u_2
f : ι → M
s : Finset M
hb : ∀ b ∈ s, Set.Finite.{u_1} (α := ι) {a : ι | f a = b}
t : Finset M := Set.Finite.toFinset (s := (↑s : Set M) ∩ Set.range f) ⋯
ht : (f ⁻¹' (↑t : Set M)).Finite
m : M
hm : m ∈ t
⊢ #({a ∈ ht.toFinset (s := f ⁻¹' (↑t : Set M)) | f a = m}) = #(⋯.toFinset (s := {a : ι | f a = m}))
have refine_2 : {a : ι | f a = m} ⊆ (↑(ht.toFinset (s := f ⁻¹' (↑t : Set M))) : Set ι)
Tactic: suffices {a | f a = m} ⊆ ht.toFinset from
      congr_arg (Finset.card ·) (Finset.ext_iff.mpr fun a ↦ by simpa using fun h ↦ this h)
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Nat (goal)
Goal:
ι : Type u_1
M : Type u_2
f : ι → M
s : Finset M
hb : ∀ b ∈ s, Set.Finite.{u_1} (α := ι) {a : ι | f a = b}
s₁ s₂ s₃ : Nat.card.{u_1} (↑(f ⁻¹' (↑s : Set M)) : Type u_1) = ∑ b ∈ s, Nat.card.{u_1} { a : ι // f a = b }
⊢ Nat.card.{u_1} (↑(f ⁻¹' (↑s : Set M)) : Type u_1) = ∑ b ∈ s, Nat.card.{u_1} { a : ι // f a = b }
have s₄ : let t := Set.Finite.toFinset (s := (↑s : Set M) ∩ Set.range f) sorry;
Nat.card.{u_1} (↑(f ⁻¹' (↑t : Set M)) : Type u_1) = ∑ b ∈ s, Nat.card.{u_1} { a : ι // f a = b }
Tactic: classical
  -- `t = s ∩ Set.range f` as a `Finset`
  let t := (Set.finite_coe_iff.mp (Finite.Set.finite_inter_of_left ↑s (Set.range f))).toFinset
  rw [show Nat.card (f ⁻¹' s) = Nat.card (f ⁻¹' t) by simp [t]]
  rw [show ∑ b ∈ s, Nat.card {a //f a = b} = ∑ b ∈ t, Nat.card {a | f a = b} by
    exact (Finset.sum_subset (by simp [t]) (by aesop)).symm]
  have ht : Set.Finite (f ⁻¹' t) := Set.Finite.preimage' (finite_toSet t) (by aesop)
  rw [Nat.card_eq_card_finite_toFinset ht, Finset.card_eq_sum_card_image (f := f)]
  refine Finset.sum_congr ?_ fun m hm ↦ ?_
  · simpa [← Finset.coe_inj, t] using Set.image_preimage_eq_inter_range
  · rw [Nat.card_eq_card_finite_toFinset (hb _ (by aesop))]
    suffices {a | f a = m} ⊆ ht.toFinset from
      congr_arg (Finset.card ·) (Finset.ext_iff.mpr fun a ↦ by simpa using fun h ↦ this h)
    intro _ h
    simp_all
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Ring.Nat (goal)
Goal:
ι : Type u_1
M : Type u_2
f : ι → M
s : Finset M
hb : ∀ b ∈ s, Set.Finite.{u_1} (α := ι) {a : ι | f a = b}
s₁ s₂ s₃ : Nat.card.{u_1} (↑(f ⁻¹' (↑s : Set M)) : Type u_1) = ∑ b ∈ s, Nat.card.{u_1} { a : ι // f a = b }
s₄ :
  let t := Set.Finite.toFinset (s := (↑s : Set M) ∩ Set.range f) ⋯;
  Nat.card.{u_1} (↑(f ⁻¹' (↑t : Set M)) : Type u_1) = ∑ b ∈ s, Nat.card.{u_1} { a : ι // f a = b }
⊢ Nat.card.{u_1} (↑(f ⁻¹' (↑s : Set M)) : Type u_1) = ∑ b ∈ s, Nat.card.{u_1} { a : ι // f a = b }
have s₅ : let t := Set.Finite.toFinset (s := (↑s : Set M) ∩ Set.range f) sorry;
Nat.card.{u_1} (↑(f ⁻¹' (↑t : Set M)) : Type u_1) = ∑ b ∈ t, Nat.card.{u_1} (↑{a : ι | f a = b} : Type u_1)
Tactic: classical
  -- `t = s ∩ Set.range f` as a `Finset`
  let t := (Set.finite_coe_iff.mp (Finite.Set.finite_inter_of_left ↑s (Set.range f))).toFinset
  rw [show Nat.card (f ⁻¹' s) = Nat.card (f ⁻¹' t) by simp [t]]
  rw [show ∑ b ∈ s, Nat.card {a //f a = b} = ∑ b ∈ t, Nat.card {a | f a = b} by
    exact (Finset.sum_subset (by simp [t]) (by aesop)).symm]
  have ht : Set.Finite (f ⁻¹' t) := Set.Finite.preimage' (finite_toSet t) (by aesop)
  rw [Nat.card_eq_card_finite_toFinset ht, Finset.card_eq_sum_card_image (f := f)]
  refine Finset.sum_congr ?_ fun m hm ↦ ?_
  · simpa [← Finset.coe_inj, t] using Set.image_preimage_eq_inter_range
  · rw [Nat.card_eq_card_finite_toFinset (hb _ (by aesop))]
    suffices {a | f a = m} ⊆ ht.toFinset from
      congr_arg (Finset.card ·) (Finset.ext_iff.mpr fun a ↦ by simpa using fun h ↦ this h)
    intro _ h
    simp_all