awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.BigOperators.Ring.List
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

Tactic:
dvd_add (h _ mem_cons_self) (ih fun x hx ↦ h x (mem_cons_of_mem _ hx))

Premises used: List.mem_cons_of_mem, List.mem_cons_self, dvd_add
-- Module: Mathlib.Algebra.BigOperators.Ring.List
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

Tactic:
exact dvd_add (h _ mem_cons_self) (ih fun x hx ↦ h x (mem_cons_of_mem _ hx))

Premises used: List.mem_cons_of_mem, List.mem_cons_self, dvd_add
-- Module: Mathlib.Algebra.BigOperators.Ring.List
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 []
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
⊢ a ∣ 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))

Premises used: dvd_zero, List.cons, List.sum_cons, List.nil
-- Module: Mathlib.Algebra.BigOperators.Ring.List
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_5
inst : NonUnitalNonAssocSemiring R
f : ι → κ → R
a : R
x : List κ
⊢ sum (zipWith (fun (i : ι) (j : κ) ↦ a * f i j) [] x) = a * (zipWith f [] x).sum

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Ring.List
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_5
inst : NonUnitalNonAssocSemiring R
f : ι → κ → R
a : R
x : List ι
⊢ sum (zipWith (fun (i : ι) (j : κ) ↦ a * f i j) x []) = a * (zipWith f x []).sum

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Ring.List
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_5
inst : NonUnitalNonAssocSemiring R
f : ι → κ → R
a : R
i : ι
l₁ : List ι
j : κ
l₂ : List κ
⊢ sum (zipWith (fun (i : ι) (j : κ) ↦ a * f i j) (i :: l₁) (j :: l₂)) = a * (zipWith f (i :: l₁) (j :: l₂)).sum

Tactic:
simp [sum_zipWith_distrib_left, mul_add]

Premises used: mul_add
-- Module: Mathlib.Algebra.BigOperators.Ring.Multiset
Goal:
M : Type u_2
inst : CommMonoid M
inst_1 : HasDistribNeg M
s : Multiset M
⊢ ∀ (a : List M), (map Neg.neg ⟦a⟧).prod = HPow.hPow (α := M) (-1) (card ⟦a⟧) * prod ⟦a⟧

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Ring.Multiset
Goal:
M₀ : Type u_3
inst : CommMonoidWithZero M₀
s : Multiset M₀
h : 0 ∈ s
rcases : ∀ (s' : Multiset M₀) (hs' : s = 0 ::ₘ s'), s.prod = 0
⊢ s.prod = 0

Tactic:
rcases Multiset.exists_cons_of_mem h with ⟨s', hs'⟩

Premises used: Multiset.exists_cons_of_mem
-- Module: Mathlib.Algebra.BigOperators.Ring.Multiset
Goal:
M₀ : Type u_3
inst : CommMonoidWithZero M₀
s : Multiset M₀
h : 0 ∈ s
s' : Multiset M₀
hs' : s = 0 ::ₘ s'
⊢ s.prod = 0

Tactic:
simp [hs', Multiset.prod_cons]

Premises used: Multiset.prod_cons
-- Module: Mathlib.Algebra.BigOperators.Ring.Multiset
Goal:
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : NoZeroDivisors M₀
inst_2 : Nontrivial M₀
s : Multiset M₀
l : List M₀
⊢ l.prod = 0 ↔ 0 ∈ (↑l : Multiset M₀)

Tactic:
List.prod_eq_zero_iff

Premises used: Multiset.Mem, List.prod_eq_zero_iff
-- Module: Mathlib.Algebra.BigOperators.Ring.Multiset
Goal:
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : NoZeroDivisors M₀
inst_2 : Nontrivial M₀
s : Multiset M₀
l : List M₀
⊢ l.prod = 0 ↔ 0 ∈ (↑l : Multiset M₀)

Tactic:
exact List.prod_eq_zero_iff

Premises used: List.prod_eq_zero_iff
-- Module: Mathlib.Algebra.BigOperators.Ring.Multiset
Goal:
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : NoZeroDivisors M₀
inst_2 : Nontrivial M₀
s : Multiset M₀
h : ¬0 ∈ s
⊢ s.prod ≠ 0

Tactic:
mt prod_eq_zero_iff.1 h

Premises used: Multiset.prod_eq_zero_iff, mt, Iff.mp
-- Module: Mathlib.Algebra.BigOperators.Ring.Multiset
Goal:
ι : Type u_1
R : Type u_4
inst : NonUnitalNonAssocSemiring R
a : R
s : Multiset ι
f : ι → R
⊢ sum (map (fun (i : ι) ↦ a * f i) 0) = a * (map f 0).sum

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Ring.Multiset
Goal:
ι : Type u_1
R : Type u_4
inst : NonUnitalNonAssocSemiring R
a : R
s_1 : Multiset ι
f : ι → R
i : ι
s : Multiset ι
ih : sum (map (fun (i : ι) ↦ a * f i) s) = a * (map f s).sum
⊢ sum (map (fun (i : ι) ↦ a * f i) (i ::ₘ s)) = a * (map f (i ::ₘ s)).sum

Tactic:
simp [ih, mul_add]

Premises used: mul_add
-- Module: Mathlib.Algebra.BigOperators.Ring.Multiset
Goal:
ι : Type u_1
R : Type u_4
inst : NonUnitalNonAssocSemiring R
a : R
s : Multiset ι
f : ι → R
⊢ sum (map (fun (i : ι) ↦ f i * a) 0) = (map f 0).sum * a

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Ring.Multiset
Goal:
ι : Type u_1
R : Type u_4
inst : NonUnitalNonAssocSemiring R
a_1 : R
s_1 : Multiset ι
f : ι → R
a : ι
s : Multiset ι
ih : sum (map (fun (i : ι) ↦ f i * a_1) s) = (map f s).sum * a_1
⊢ sum (map (fun (i : ι) ↦ f i * a_1) (a ::ₘ s)) = (map f (a ::ₘ s)).sum * a_1

Tactic:
simp [ih, add_mul]

Premises used: add_mul
-- Module: Mathlib.Algebra.BigOperators.Ring.Multiset
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
rw : a ∣ x + s.sum
⊢ a ∣ (x ::ₘ s).sum

Tactic:
rw [sum_cons]

Premises used: Multiset.sum_cons
-- Module: Mathlib.Algebra.BigOperators.Ring.Multiset
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

Tactic:
dvd_add (h _ (mem_cons_self _ _)) (ih fun y hy ↦ h _ <| mem_cons.2 <| Or.inr hy)

Premises used: Iff.mpr, Multiset.mem_cons, Multiset.mem_cons_self, Or.inr, dvd_add
-- Module: Mathlib.Algebra.BigOperators.Ring.Multiset
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

Tactic:
exact dvd_add (h _ (mem_cons_self _ _)) (ih fun y hy ↦ h _ <| mem_cons.2 <| Or.inr hy)

Premises used: Iff.mpr, Multiset.mem_cons, Multiset.mem_cons_self, Or.inr, dvd_add
-- Module: Mathlib.Algebra.BigOperators.Ring.Multiset
Goal:
R : Type u_4
inst : CommSemiring R
s : Multiset (Multiset R)
⊢ Eq.{u_4 + 1} (α := R) (prod (map sum 0)) (sum (map prod (Sections 0)))

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Ring.Multiset
Goal:
R : Type u_4
inst : CommSemiring R
s_1 : Multiset (Multiset R)
a : Multiset R
s : Multiset (Multiset R)
ih : (map sum s).prod = (map prod s.Sections).sum
⊢ (map sum (a ::ₘ s)).prod = (map prod (a ::ₘ s).Sections).sum

Tactic:
simp [ih, map_bind, sum_map_mul_left, sum_map_mul_right]

Premises used: Multiset.map_bind, Multiset.sum_map_mul_right, Multiset.sum_map_mul_left
-- Module: Mathlib.Algebra.BigOperators.Ring.Multiset
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))

Tactic:
s.induction_on ?_ fun a s ih ↦ ?_

Premises used: Multiset.induction_on
-- Module: Mathlib.Algebra.BigOperators.Ring.Multiset
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)))
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))
⊢ 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))

Tactic:
refine s.induction_on ?_ fun a s ih ↦ ?_
-- Module: Mathlib.Algebra.BigOperators.Ring.Multiset
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) 0))
    (sum (map (fun (p : Multiset ι × Multiset ι) ↦ (map f p.1).prod * (map g p.2).prod) (antidiagonal 0)))

Tactic:
simp only [map_zero, prod_zero, antidiagonal_zero, map_singleton, mul_one, sum_singleton]

Premises used: Multiset.prod_zero, Multiset.map_singleton, Multiset.map_zero, Multiset.sum_singleton, Multiset.antidiagonal_zero, mul_one
-- Module: Mathlib.Algebra.BigOperators.Ring.Multiset
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))
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))
⊢ 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:
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]

Premises used: Prod.map_snd, add_mul, Multiset.map_cons, Multiset.sum_add, Multiset.prod_cons, mul_assoc, Multiset.antidiagonal_cons, mul_left_comm, Prod.map_fst, Multiset.map_map, Function.comp_apply, Multiset.sum_map_add, Eq.symm, Multiset.map_add, id_eq, Multiset.sum_map_mul_left
-- Module: Mathlib.Algebra.BigOperators.Ring.Multiset
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))
⊢ 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:
add_comm _ _

Premises used: add_comm
-- Module: Mathlib.Algebra.BigOperators.Ring.Multiset
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))
⊢ 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:
exact add_comm _ _

Premises used: add_comm
-- Module: Mathlib.Algebra.BigOperators.Ring.Multiset
Goal:
R : Type u_4
inst : NonUnitalNonAssocSemiring R
s : Multiset R
a : R
h : ∀ (b : R), b ∈ s → Commute a b
h₁ : ∀ (a_1 : List R) (h : ∀ (b : R), b ∈ ⟦a_1⟧ → Commute a b), Commute a (sum ⟦a_1⟧)
⊢ Commute a s.sum

Tactic:
induction s using Quotient.inductionOn
-- Module: Mathlib.Algebra.BigOperators.Ring.Multiset
Goal:
R : Type u_4
inst : NonUnitalNonAssocSemiring R
s : Multiset R
a : R
a_1 : List R
h : ∀ (b : R), b ∈ ⟦a_1⟧ → Commute a b
⊢ Commute a a_1.sum

Tactic:
Commute.list_sum_right _ _ h

Premises used: Commute.list_sum_right
-- Module: Mathlib.Algebra.BigOperators.Ring.Multiset
Goal:
R : Type u_4
inst : NonUnitalNonAssocSemiring R
s : Multiset R
a : R
a_1 : List R
h : ∀ (b : R), b ∈ ⟦a_1⟧ → Commute a b
⊢ Commute a a_1.sum

Tactic:
exact Commute.list_sum_right _ _ h

Premises used: Commute.list_sum_right
-- Module: Mathlib.Algebra.BigOperators.Ring.Multiset
Goal:
R : Type u_4
inst : NonUnitalNonAssocSemiring R
s : Multiset R
b : R
h : ∀ (a : R), a ∈ s → Commute a b
⊢ Commute s.sum b

Tactic:
((Commute.multiset_sum_right _ _) fun _ ha => (h _ ha).symm).symm

Premises used: Commute.multiset_sum_right, Commute.symm
-- Module: Mathlib.Algebra.BigOperators.Ring.Nat
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℕ
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)})
⊢ Even (α := ℕ) (∑ i ∈ s, f i) ↔ Even #({x ∈ s | Odd (f x)})

Tactic:
rw [← Finset.sum_filter_add_sum_filter_not _ (fun x ↦ Even (f x)), Nat.even_add]

Premises used: Nat.even_add, Finset.sum_filter_add_sum_filter_not, Even
-- Module: Mathlib.Algebra.BigOperators.Ring.Nat
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℕ
simp : Even (α := ℕ) (∑ x ∈ s with ¬Even (f x), f x) ↔ Even #({x ∈ s | Odd (f x)})
⊢ (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:
simp only [Finset.mem_filter, and_imp, imp_self, implies_true, Finset.even_sum, true_iff]

Premises used: and_imp, true_iff, imp_self, Finset.even_sum, Finset.mem_filter, implies_true
-- Module: Mathlib.Algebra.BigOperators.Ring.Nat
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℕ
rw : HMod.hMod (α := ℕ) (∑ a ∈ s, if ¬Even (f a) then f a % 2 else 0) 2 = 0 ↔ Even #({x ∈ s | Odd (f x)})
⊢ Even (α := ℕ) (∑ x ∈ s with ¬Even (f x), f x) ↔ Even #({x ∈ s | Odd (f x)})

Tactic:
rw [Nat.even_iff, Finset.sum_nat_mod, Finset.sum_filter]

Premises used: Finset.sum_nat_mod, Nat.even_iff, Finset.sum_filter
-- Module: Mathlib.Algebra.BigOperators.Ring.Nat
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℕ
simp : HMod.hMod (α := ℕ) (∑ x ∈ s, if Odd (f x) then 1 else 0) 2 = 0 ↔ Even #({x ∈ s | Odd (f x)})
⊢ HMod.hMod (α := ℕ) (∑ a ∈ s, if ¬Even (f a) then f a % 2 else 0) 2 = 0 ↔ Even #({x ∈ s | Odd (f x)})

Tactic:
simp +contextual only [Nat.not_even_iff_odd, Nat.odd_iff.mp]

Premises used: Nat.not_even_iff_odd, Iff.mp, Nat.odd_iff
-- Module: Mathlib.Algebra.BigOperators.Ring.Nat
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)})
simp_rw₁ : Even (α := ℕ) (∑ a ∈ s with Odd (f a), 1) ↔ 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)})

Tactic:
simp_rw [← Finset.sum_filter, ← Nat.even_iff, Finset.card_eq_sum_ones]

Premises used: Finset.card_eq_sum_ones, Nat.even_iff, Finset.sum_filter
-- Module: Mathlib.Algebra.BigOperators.Ring.Nat
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ Odd (α := ℕ) (∑ i ∈ s, f i) ↔ Odd #({x ∈ s | Odd (f x)})

Tactic:
simp only [← Nat.not_even_iff_odd, even_sum_iff_even_card_odd]

Premises used: Finset.even_sum_iff_even_card_odd, Nat.not_even_iff_odd
-- Module: Mathlib.Algebra.BigOperators.Ring.Nat
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) = Nat.card.{u_1} (↑(f ⁻¹' (↑t : Set M)) : Type u_1)

Tactic:
simp [t]
-- Module: Mathlib.Algebra.BigOperators.Ring.Nat
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) ⋯
rw : 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 }

Tactic:
rw [show Nat.card (f ⁻¹' s) = Nat.card (f ⁻¹' t) by simp [t]]
-- Module: Mathlib.Algebra.BigOperators.Ring.Nat
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) ⋯
⊢ t ⊆ s

Tactic:
simp [t]
-- Module: Mathlib.Algebra.BigOperators.Ring.Nat
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) ⋯
⊢ ∀ x ∈ s, x ∉ t → Nat.card.{u_1} { a : ι // f a = x } = 0

Tactic:
aesop
-- Module: Mathlib.Algebra.BigOperators.Ring.Nat
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) ⋯
⊢ Eq (α := ℕ) (∑ b ∈ s, Nat.card.{u_1} { a : ι // f a = b }) (∑ b ∈ t, Nat.card.{u_1} (↑{a : ι | f a = b} : Type u_1))

Tactic:
exact (Finset.sum_subset (by simp [t]) (by aesop)).symm

Premises used: Finset.sum_subset, Eq.symm
-- Module: Mathlib.Algebra.BigOperators.Ring.Nat
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) ⋯
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)
⊢ Nat.card.{u_1} (↑(f ⁻¹' (↑t : Set M)) : Type u_1) = ∑ b ∈ s, Nat.card.{u_1} { a : ι // f a = b }

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]
-- Module: Mathlib.Algebra.BigOperators.Ring.Nat
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) ⋯
⊢ ∀ b ∈ (↑t : Set M), (f ⁻¹' {b}).Finite

Tactic:
aesop
-- Module: Mathlib.Algebra.BigOperators.Ring.Nat
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) ⋯
⊢ (f ⁻¹' (↑t : Set M)).Finite

Tactic:
have ht : Set.Finite (f ⁻¹' t) := Set.Finite.preimage' (finite_toSet t) (by aesop)
-- Module: Mathlib.Algebra.BigOperators.Ring.Nat
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
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))
⊢ 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 [Nat.card_eq_card_finite_toFinset ht, Finset.card_eq_sum_card_image (f := f)]

Premises used: Finset.card_eq_sum_card_image, Nat.card_eq_card_finite_toFinset
-- Module: Mathlib.Algebra.BigOperators.Ring.Nat
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))

Tactic:
Finset.sum_congr ?_ fun m hm ↦ ?_

Premises used: Finset.sum_congr
-- Module: Mathlib.Algebra.BigOperators.Ring.Nat
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
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)
⊢ 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:
refine Finset.sum_congr ?_ fun m hm ↦ ?_

Premises used: Finset.sum_congr
-- Module: Mathlib.Algebra.BigOperators.Ring.Nat
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
⊢ image f (ht.toFinset (s := f ⁻¹' (↑t : Set M))) = t

Tactic:
simpa [← Finset.coe_inj, t] using Set.image_preimage_eq_inter_range

Premises used: Finset.coe_inj, Set.image_preimage_eq_inter_range
-- Module: Mathlib.Algebra.BigOperators.Ring.Nat
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
⊢ m ∈ s

Tactic:
aesop
-- Module: Mathlib.Algebra.BigOperators.Ring.Nat
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
refine_2 : #({a ∈ ht.toFinset (s := f ⁻¹' (↑t : Set M)) | f a = m}) = #(⋯.toFinset (s := {a : ι | f a = m}))
⊢ #({a ∈ ht.toFinset (s := f ⁻¹' (↑t : Set M)) | f a = m}) = Nat.card.{u_1} (↑{a : ι | f a = m} : Type u_1)

Tactic:
rw [Nat.card_eq_card_finite_toFinset (hb _ (by aesop))]

Premises used: Nat.card_eq_card_finite_toFinset
-- Module: Mathlib.Algebra.BigOperators.Ring.Nat
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
this : {a : ι | f a = m} ⊆ (↑(ht.toFinset (s := f ⁻¹' (↑t : Set M))) : Set ι)
a : ι
⊢ a ∈ {a ∈ ht.toFinset (s := f ⁻¹' (↑t : Set M)) | f a = m} ↔ a ∈ ⋯.toFinset (s := {a : ι | f a = m})

Tactic:
simpa using fun h ↦ this h
-- Module: Mathlib.Algebra.BigOperators.Ring.Nat
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
refine_2 : {a : ι | f a = m} ⊆ (↑(ht.toFinset (s := f ⁻¹' (↑t : Set M))) : Set ι)
⊢ #({a ∈ ht.toFinset (s := f ⁻¹' (↑t : Set M)) | f a = m}) = #(⋯.toFinset (s := {a : ι | f a = m}))

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)
-- Module: Mathlib.Algebra.BigOperators.Ring.Nat
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 : ι
h : Membership.mem (γ := Set ι) {a : ι | f a = m} a
⊢ a ∈ (↑(ht.toFinset (s := f ⁻¹' (↑t : Set M))) : Set ι)

Tactic:
simp_all