awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.BigOperators.ModEq
Goal:
n : ℕ
l : List ℕ
h : ∀ x ∈ l, x ≡ 1 [MOD n]
⊢ l.prod ≡ 1 [MOD n]

Tactic:
simpa using listProd_map_one h

Premises used: Nat.ModEq.listProd_map_one
-- Module: Mathlib.Algebra.BigOperators.ModEq
Goal:
α : Type u_1
n : ℕ
l : List α
f g : α → ℕ
h : ∀ x ∈ l, f x ≡ g x [MOD n]
nil :
  ∀ (h : ∀ (x : α), Membership.mem (γ := List α) [] x → f x ≡ g x [MOD n]),
    (List.map f []).sum ≡ (List.map g []).sum [MOD n]
cons :
  ∀ (head : α) (tail : List α),
    (∀ (h : ∀ x ∈ tail, f x ≡ g x [MOD n]), (List.map f tail).sum ≡ (List.map g tail).sum [MOD n]) →
      ∀ (h : ∀ x ∈ head :: tail, f x ≡ g x [MOD n]),
        (List.map f (head :: tail)).sum ≡ (List.map g (head :: tail)).sum [MOD n]
⊢ (List.map f l).sum ≡ (List.map g l).sum [MOD n]

Tactic:
induction l
-- Module: Mathlib.Algebra.BigOperators.ModEq
Goal:
α : Type u_1
n : ℕ
l : List α
f g : α → ℕ
h : ∀ (x : α), Membership.mem (γ := List α) [] x → f x ≡ g x [MOD n]
⊢ (List.map f []).sum ≡ (List.map g []).sum [MOD n]

Tactic:
aesop (add unsafe ModEq.add)

Premises used: Nat.ModEq.add
-- Module: Mathlib.Algebra.BigOperators.ModEq
Goal:
α : Type u_1
n : ℕ
l : List α
f g : α → ℕ
head : α
tail : List α
tail_ih : ∀ (h : ∀ x ∈ tail, f x ≡ g x [MOD n]), (List.map f tail).sum ≡ (List.map g tail).sum [MOD n]
h : ∀ x ∈ head :: tail, f x ≡ g x [MOD n]
⊢ (List.map f (head :: tail)).sum ≡ (List.map g (head :: tail)).sum [MOD n]

Tactic:
aesop (add unsafe ModEq.add)

Premises used: Nat.ModEq.add
-- Module: Mathlib.Algebra.BigOperators.ModEq
Goal:
α : Type u_1
n : ℕ
l : List α
f : α → ℕ
h : ∀ x ∈ l, f x ≡ 0 [MOD n]
⊢ (List.map f l).sum ≡ 0 [MOD n]

Tactic:
simpa using listSum_map h

Premises used: Nat.ModEq.listSum_map
-- Module: Mathlib.Algebra.BigOperators.ModEq
Goal:
n : ℕ
l : List ℕ
h : ∀ x ∈ l, x ≡ 0 [MOD n]
⊢ l.sum ≡ 0 [MOD n]

Tactic:
simpa using listSum_map h

Premises used: Nat.ModEq.listSum_map
-- Module: Mathlib.Algebra.BigOperators.ModEq
Goal:
α : Type u_1
n : ℕ
f g : α → ℕ
s : Multiset α
h : ∀ x ∈ s, f x ≡ g x [MOD n]
mk :
  ∀ (l : List α)
    (h :
      ∀ (x : α),
        Membership.mem (γ := Multiset α) (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) l) x →
          f x ≡ g x [MOD n]),
    (Multiset.map f (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) l)).prod ≡
      (Multiset.map g (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) l)).prod [MOD n]
⊢ (Multiset.map f s).prod ≡ (Multiset.map g s).prod [MOD n]

Tactic:
rcases s with ⟨l⟩
-- Module: Mathlib.Algebra.BigOperators.ModEq
Goal:
α : Type u_1
n : ℕ
f g : α → ℕ
s : Multiset α
l : List α
h :
  ∀ (x : α),
    Membership.mem (γ := Multiset α) (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) l) x → f x ≡ g x [MOD n]
⊢ (Multiset.map f (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) l)).prod ≡
    (Multiset.map g (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) l)).prod [MOD n]

Tactic:
simpa using listProd_map (l := l) h

Premises used: Nat.ModEq.listProd_map
-- Module: Mathlib.Algebra.BigOperators.ModEq
Goal:
α : Type u_1
n : ℕ
f : α → ℕ
s : Multiset α
h : ∀ x ∈ s, f x ≡ 1 [MOD n]
⊢ (Multiset.map f s).prod ≡ 1 [MOD n]

Tactic:
simpa using multisetProd_map h

Premises used: Nat.ModEq.multisetProd_map
-- Module: Mathlib.Algebra.BigOperators.ModEq
Goal:
n : ℕ
s : Multiset ℕ
h : ∀ x ∈ s, x ≡ 1 [MOD n]
⊢ s.prod ≡ 1 [MOD n]

Tactic:
simpa using multisetProd_map_one h

Premises used: Nat.ModEq.multisetProd_map_one
-- Module: Mathlib.Algebra.BigOperators.ModEq
Goal:
α : Type u_1
n : ℕ
f g : α → ℕ
s : Multiset α
h : ∀ x ∈ s, f x ≡ g x [MOD n]
mk :
  ∀ (l : List α)
    (h :
      ∀ (x : α),
        Membership.mem (γ := Multiset α) (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) l) x →
          f x ≡ g x [MOD n]),
    (Multiset.map f (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) l)).sum ≡
      (Multiset.map g (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) l)).sum [MOD n]
⊢ (Multiset.map f s).sum ≡ (Multiset.map g s).sum [MOD n]

Tactic:
rcases s with ⟨l⟩
-- Module: Mathlib.Algebra.BigOperators.ModEq
Goal:
α : Type u_1
n : ℕ
f g : α → ℕ
s : Multiset α
l : List α
h :
  ∀ (x : α),
    Membership.mem (γ := Multiset α) (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) l) x → f x ≡ g x [MOD n]
⊢ (Multiset.map f (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) l)).sum ≡
    (Multiset.map g (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) l)).sum [MOD n]

Tactic:
simpa using listSum_map (l := l) h

Premises used: Nat.ModEq.listSum_map
-- Module: Mathlib.Algebra.BigOperators.ModEq
Goal:
α : Type u_1
n : ℕ
f : α → ℕ
s : Multiset α
h : ∀ x ∈ s, f x ≡ 0 [MOD n]
⊢ (Multiset.map f s).sum ≡ 0 [MOD n]

Tactic:
simpa using multisetSum_map h

Premises used: Nat.ModEq.multisetSum_map
-- Module: Mathlib.Algebra.BigOperators.ModEq
Goal:
n : ℕ
s : Multiset ℕ
h : ∀ x ∈ s, x ≡ 0 [MOD n]
⊢ s.sum ≡ 0 [MOD n]

Tactic:
simpa using multisetSum_map h

Premises used: Nat.ModEq.multisetSum_map
-- Module: Mathlib.Algebra.BigOperators.ModEq
Goal:
α : Type u_1
n : ℕ
f g : α → ℕ
s : Finset α
h : ∀ x ∈ s, f x ≡ g x [MOD n]
⊢ ∏ x ∈ s, f x ≡ ∏ x ∈ s, g x [MOD n]

Tactic:
.multisetProd_map (s := s.1) h

Premises used: Nat.ModEq.multisetProd_map, Finset.prod
-- Module: Mathlib.Algebra.BigOperators.ModEq
Goal:
α : Type u_1
n : ℕ
f : α → ℕ
s : Finset α
h : ∀ x ∈ s, f x ≡ 1 [MOD n]
⊢ ∏ x ∈ s, f x ≡ 1 [MOD n]

Tactic:
simpa using ModEq.prod h

Premises used: Nat.ModEq.prod
-- Module: Mathlib.Algebra.BigOperators.ModEq
Goal:
α : Type u_1
n : ℕ
f g : α → ℕ
s : Finset α
h : ∀ x ∈ s, f x ≡ g x [MOD n]
⊢ ∑ x ∈ s, f x ≡ ∑ x ∈ s, g x [MOD n]

Tactic:
.multisetSum_map (s := s.1) h

Premises used: Nat.ModEq.multisetSum_map, Finset.sum
-- Module: Mathlib.Algebra.BigOperators.ModEq
Goal:
α : Type u_1
n : ℕ
f : α → ℕ
s : Finset α
h : ∀ x ∈ s, f x ≡ 0 [MOD n]
⊢ ∑ x ∈ s, f x ≡ 0 [MOD n]

Tactic:
simpa using ModEq.sum h

Premises used: Nat.ModEq.sum
-- Module: Mathlib.Algebra.BigOperators.ModEq
Goal:
α : Type u_1
n : ℕ
f : α → ℕ
inst : DecidableEq α
s : Finset α
a : α
hf : ∀ x ∈ s, x ≠ a → f x ≡ 1 [MOD n]
simp :
  ∀ (hf : ∀ x ∈ s, x ≠ a → Eq (α := ZMod n) (↑(f x) : ZMod n) 1),
    Eq (α := ZMod n) (∏ i ∈ s, (↑(f i) : ZMod n)) (if a ∈ s then (↑(f a) : ZMod n) else 1)
⊢ ∏ x ∈ s, f x ≡ if a ∈ s then f a else 1 [MOD n]

Tactic:
simp only [← ZMod.natCast_eq_natCast_iff, cast_one, cast_prod, apply_ite Nat.cast] at *

Premises used: apply_ite, Nat.cast_prod, Nat.cast, ZMod.natCast_eq_natCast_iff, Nat.cast_one
-- Module: Mathlib.Algebra.BigOperators.ModEq
Goal:
α : Type u_1
n : ℕ
f : α → ℕ
inst : DecidableEq α
s : Finset α
a : α
hf : ∀ x ∈ s, x ≠ a → Eq (α := ZMod n) (↑(f x) : ZMod n) 1
⊢ Eq (α := ZMod n) (∏ i ∈ s, (↑(f i) : ZMod n)) (if a ∈ s then (↑(f a) : ZMod n) else 1)

Tactic:
Finset.prod_eq_ite _ hf

Premises used: Finset.prod_eq_ite
-- Module: Mathlib.Algebra.BigOperators.ModEq
Goal:
α : Type u_1
n : ℕ
f : α → ℕ
inst : DecidableEq α
s : Finset α
a : α
hf : ∀ x ∈ s, x ≠ a → Eq (α := ZMod n) (↑(f x) : ZMod n) 1
⊢ Eq (α := ZMod n) (∏ i ∈ s, (↑(f i) : ZMod n)) (if a ∈ s then (↑(f a) : ZMod n) else 1)

Tactic:
exact Finset.prod_eq_ite _ hf

Premises used: Finset.prod_eq_ite
-- Module: Mathlib.Algebra.BigOperators.ModEq
Goal:
α : Type u_1
n : ℕ
f : α → ℕ
s : Finset α
a : α
ha : a ∉ s → f a ≡ 1 [MOD n]
hf : ∀ x ∈ s, x ≠ a → f x ≡ 1 [MOD n]
simp :
  ∀ (ha : a ∉ s → Eq (α := ZMod n) (↑(f a) : ZMod n) 1) (hf : ∀ x ∈ s, x ≠ a → Eq (α := ZMod n) (↑(f x) : ZMod n) 1),
    Eq (α := ZMod n) (∏ i ∈ s, (↑(f i) : ZMod n)) (↑(f a) : ZMod n)
⊢ ∏ x ∈ s, f x ≡ f a [MOD n]

Tactic:
simp only [← ZMod.natCast_eq_natCast_iff, cast_one, cast_prod] at *

Premises used: Nat.cast_prod, ZMod.natCast_eq_natCast_iff, Nat.cast_one
-- Module: Mathlib.Algebra.BigOperators.ModEq
Goal:
α : Type u_1
n : ℕ
f : α → ℕ
s : Finset α
a : α
ha : a ∉ s → Eq (α := ZMod n) (↑(f a) : ZMod n) 1
hf : ∀ x ∈ s, x ≠ a → Eq (α := ZMod n) (↑(f x) : ZMod n) 1
h₀ : ∀ b ∈ s, b ≠ a → Eq (α := ZMod n) (↑(f b) : ZMod n) 1
h₁ : a ∉ s → Eq (α := ZMod n) (↑(f a) : ZMod n) 1
⊢ Eq (α := ZMod n) (∏ i ∈ s, (↑(f i) : ZMod n)) (↑(f a) : ZMod n)

Tactic:
apply Finset.prod_eq_single

Premises used: Finset.prod_eq_single
-- Module: Mathlib.Algebra.BigOperators.ModEq
Goal:
α : Type u_1
n : ℕ
f : α → ℕ
s : Finset α
a : α
ha : a ∉ s → Eq (α := ZMod n) (↑(f a) : ZMod n) 1
hf : ∀ x ∈ s, x ≠ a → Eq (α := ZMod n) (↑(f x) : ZMod n) 1
⊢ ∀ b ∈ s, b ≠ a → Eq (α := ZMod n) (↑(f b) : ZMod n) 1

Tactic:
assumption
-- Module: Mathlib.Algebra.BigOperators.ModEq
Goal:
α : Type u_1
n : ℕ
f : α → ℕ
s : Finset α
a : α
ha : a ∉ s → Eq (α := ZMod n) (↑(f a) : ZMod n) 1
hf : ∀ x ∈ s, x ≠ a → Eq (α := ZMod n) (↑(f x) : ZMod n) 1
⊢ a ∉ s → Eq (α := ZMod n) (↑(f a) : ZMod n) 1

Tactic:
assumption
-- Module: Mathlib.Algebra.BigOperators.ModEq
Goal:
α : Type u_1
n : ℕ
f : α → ℕ
inst : DecidableEq α
s : Finset α
a : α
hf : ∀ x ∈ s, x ≠ a → f x ≡ 0 [MOD n]
simp :
  ∀ (hf : ∀ x ∈ s, x ≠ a → Eq (α := ZMod n) (↑(f x) : ZMod n) 0),
    Eq (α := ZMod n) (∑ x ∈ s, (↑(f x) : ZMod n)) (if a ∈ s then (↑(f a) : ZMod n) else 0)
⊢ ∑ x ∈ s, f x ≡ if a ∈ s then f a else 0 [MOD n]

Tactic:
simp only [← ZMod.natCast_eq_natCast_iff, cast_zero, cast_sum, apply_ite Nat.cast] at *

Premises used: apply_ite, Nat.cast, Nat.cast_sum, ZMod.natCast_eq_natCast_iff, Nat.cast_zero
-- Module: Mathlib.Algebra.BigOperators.ModEq
Goal:
α : Type u_1
n : ℕ
f : α → ℕ
inst : DecidableEq α
s : Finset α
a : α
hf : ∀ x ∈ s, x ≠ a → Eq (α := ZMod n) (↑(f x) : ZMod n) 0
⊢ Eq (α := ZMod n) (∑ x ∈ s, (↑(f x) : ZMod n)) (if a ∈ s then (↑(f a) : ZMod n) else 0)

Tactic:
Finset.sum_eq_ite _ hf

Premises used: Finset.sum_eq_ite
-- Module: Mathlib.Algebra.BigOperators.ModEq
Goal:
α : Type u_1
n : ℕ
f : α → ℕ
inst : DecidableEq α
s : Finset α
a : α
hf : ∀ x ∈ s, x ≠ a → Eq (α := ZMod n) (↑(f x) : ZMod n) 0
⊢ Eq (α := ZMod n) (∑ x ∈ s, (↑(f x) : ZMod n)) (if a ∈ s then (↑(f a) : ZMod n) else 0)

Tactic:
exact Finset.sum_eq_ite _ hf

Premises used: Finset.sum_eq_ite
-- Module: Mathlib.Algebra.BigOperators.ModEq
Goal:
α : Type u_1
n : ℕ
f : α → ℕ
s : Finset α
a : α
ha : a ∉ s → f a ≡ 0 [MOD n]
hf : ∀ x ∈ s, x ≠ a → f x ≡ 0 [MOD n]
simp :
  ∀ (ha : a ∉ s → Eq (α := ZMod n) (↑(f a) : ZMod n) 0) (hf : ∀ x ∈ s, x ≠ a → Eq (α := ZMod n) (↑(f x) : ZMod n) 0),
    Eq (α := ZMod n) (∑ x ∈ s, (↑(f x) : ZMod n)) (↑(f a) : ZMod n)
⊢ ∑ x ∈ s, f x ≡ f a [MOD n]

Tactic:
simp only [← ZMod.natCast_eq_natCast_iff, cast_zero, cast_sum] at *

Premises used: Nat.cast_sum, ZMod.natCast_eq_natCast_iff, Nat.cast_zero
-- Module: Mathlib.Algebra.BigOperators.ModEq
Goal:
α : Type u_1
n : ℕ
f : α → ℕ
s : Finset α
a : α
ha : a ∉ s → Eq (α := ZMod n) (↑(f a) : ZMod n) 0
hf : ∀ x ∈ s, x ≠ a → Eq (α := ZMod n) (↑(f x) : ZMod n) 0
h₀ : ∀ b ∈ s, b ≠ a → Eq (α := ZMod n) (↑(f b) : ZMod n) 0
h₁ : a ∉ s → Eq (α := ZMod n) (↑(f a) : ZMod n) 0
⊢ Eq (α := ZMod n) (∑ x ∈ s, (↑(f x) : ZMod n)) (↑(f a) : ZMod n)

Tactic:
apply Finset.sum_eq_single

Premises used: Finset.sum_eq_single
-- Module: Mathlib.Algebra.BigOperators.ModEq
Goal:
α : Type u_1
n : ℕ
f : α → ℕ
s : Finset α
a : α
ha : a ∉ s → Eq (α := ZMod n) (↑(f a) : ZMod n) 0
hf : ∀ x ∈ s, x ≠ a → Eq (α := ZMod n) (↑(f x) : ZMod n) 0
⊢ ∀ b ∈ s, b ≠ a → Eq (α := ZMod n) (↑(f b) : ZMod n) 0

Tactic:
assumption
-- Module: Mathlib.Algebra.BigOperators.ModEq
Goal:
α : Type u_1
n : ℕ
f : α → ℕ
s : Finset α
a : α
ha : a ∉ s → Eq (α := ZMod n) (↑(f a) : ZMod n) 0
hf : ∀ x ∈ s, x ≠ a → Eq (α := ZMod n) (↑(f x) : ZMod n) 0
⊢ a ∉ s → Eq (α := ZMod n) (↑(f a) : ZMod n) 0

Tactic:
assumption
-- Module: Mathlib.Algebra.BigOperators.ModEq
Goal:
α : Type u_1
n : ℤ
l : List α
f g : α → ℤ
h : ∀ x ∈ l, f x ≡ g x [ZMOD n]
nil :
  ∀ (h : ∀ (x : α), Membership.mem (γ := List α) [] x → f x ≡ g x [ZMOD n]),
    (List.map f []).prod ≡ (List.map g []).prod [ZMOD n]
cons :
  ∀ (head : α) (tail : List α),
    (∀ (h : ∀ x ∈ tail, f x ≡ g x [ZMOD n]), (List.map f tail).prod ≡ (List.map g tail).prod [ZMOD n]) →
      ∀ (h : ∀ x ∈ head :: tail, f x ≡ g x [ZMOD n]),
        (List.map f (head :: tail)).prod ≡ (List.map g (head :: tail)).prod [ZMOD n]
⊢ (List.map f l).prod ≡ (List.map g l).prod [ZMOD n]

Tactic:
induction l
-- Module: Mathlib.Algebra.BigOperators.ModEq
Goal:
α : Type u_1
n : ℤ
l : List α
f g : α → ℤ
h : ∀ (x : α), Membership.mem (γ := List α) [] x → f x ≡ g x [ZMOD n]
⊢ (List.map f []).prod ≡ (List.map g []).prod [ZMOD n]

Tactic:
aesop (add unsafe ModEq.mul)

Premises used: Int.ModEq.mul
-- Module: Mathlib.Algebra.BigOperators.ModEq
Goal:
α : Type u_1
n : ℤ
l : List α
f g : α → ℤ
head : α
tail : List α
tail_ih : ∀ (h : ∀ x ∈ tail, f x ≡ g x [ZMOD n]), (List.map f tail).prod ≡ (List.map g tail).prod [ZMOD n]
h : ∀ x ∈ head :: tail, f x ≡ g x [ZMOD n]
⊢ (List.map f (head :: tail)).prod ≡ (List.map g (head :: tail)).prod [ZMOD n]

Tactic:
aesop (add unsafe ModEq.mul)

Premises used: Int.ModEq.mul
-- Module: Mathlib.Algebra.BigOperators.ModEq
Goal:
α : Type u_1
n : ℤ
l : List α
f : α → ℤ
h : ∀ x ∈ l, f x ≡ 1 [ZMOD n]
⊢ List.prod (List.map (fun (x : α) ↦ 1) l) ≡ 1 [ZMOD n]

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.ModEq
Goal:
n : ℤ
l : List ℤ
h : ∀ x ∈ l, x ≡ 1 [ZMOD n]
⊢ l.prod ≡ 1 [ZMOD n]

Tactic:
simpa using listProd_map_one h

Premises used: Int.ModEq.listProd_map_one
-- Module: Mathlib.Algebra.BigOperators.ModEq
Goal:
α : Type u_1
n : ℤ
l : List α
f g : α → ℤ
h : ∀ x ∈ l, f x ≡ g x [ZMOD n]
nil :
  ∀ (h : ∀ (x : α), Membership.mem (γ := List α) [] x → f x ≡ g x [ZMOD n]),
    (List.map f []).sum ≡ (List.map g []).sum [ZMOD n]
cons :
  ∀ (head : α) (tail : List α),
    (∀ (h : ∀ x ∈ tail, f x ≡ g x [ZMOD n]), (List.map f tail).sum ≡ (List.map g tail).sum [ZMOD n]) →
      ∀ (h : ∀ x ∈ head :: tail, f x ≡ g x [ZMOD n]),
        (List.map f (head :: tail)).sum ≡ (List.map g (head :: tail)).sum [ZMOD n]
⊢ (List.map f l).sum ≡ (List.map g l).sum [ZMOD n]

Tactic:
induction l
-- Module: Mathlib.Algebra.BigOperators.ModEq
Goal:
α : Type u_1
n : ℤ
l : List α
f g : α → ℤ
h : ∀ (x : α), Membership.mem (γ := List α) [] x → f x ≡ g x [ZMOD n]
⊢ (List.map f []).sum ≡ (List.map g []).sum [ZMOD n]

Tactic:
aesop (add unsafe ModEq.add)

Premises used: Int.ModEq.add
-- Module: Mathlib.Algebra.BigOperators.ModEq
Goal:
α : Type u_1
n : ℤ
l : List α
f g : α → ℤ
head : α
tail : List α
tail_ih : ∀ (h : ∀ x ∈ tail, f x ≡ g x [ZMOD n]), (List.map f tail).sum ≡ (List.map g tail).sum [ZMOD n]
h : ∀ x ∈ head :: tail, f x ≡ g x [ZMOD n]
⊢ (List.map f (head :: tail)).sum ≡ (List.map g (head :: tail)).sum [ZMOD n]

Tactic:
aesop (add unsafe ModEq.add)

Premises used: Int.ModEq.add
-- Module: Mathlib.Algebra.BigOperators.ModEq
Goal:
α : Type u_1
n : ℤ
l : List α
f : α → ℤ
h : ∀ x ∈ l, f x ≡ 0 [ZMOD n]
⊢ (List.map f l).sum ≡ 0 [ZMOD n]

Tactic:
simpa using listSum_map h

Premises used: Int.ModEq.listSum_map
-- Module: Mathlib.Algebra.BigOperators.ModEq
Goal:
n : ℤ
l : List ℤ
h : ∀ x ∈ l, x ≡ 0 [ZMOD n]
⊢ l.sum ≡ 0 [ZMOD n]

Tactic:
simpa using listSum_map_zero h

Premises used: Int.ModEq.listSum_map_zero
-- Module: Mathlib.Algebra.BigOperators.ModEq
Goal:
α : Type u_1
n : ℤ
f g : α → ℤ
s : Multiset α
h : ∀ x ∈ s, f x ≡ g x [ZMOD n]
mk :
  ∀ (l : List α)
    (h :
      ∀ (x : α),
        Membership.mem (γ := Multiset α) (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) l) x →
          f x ≡ g x [ZMOD n]),
    (Multiset.map f (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) l)).prod ≡
      (Multiset.map g (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) l)).prod [ZMOD n]
⊢ (Multiset.map f s).prod ≡ (Multiset.map g s).prod [ZMOD n]

Tactic:
rcases s with ⟨l⟩
-- Module: Mathlib.Algebra.BigOperators.ModEq
Goal:
α : Type u_1
n : ℤ
f g : α → ℤ
s : Multiset α
l : List α
h :
  ∀ (x : α),
    Membership.mem (γ := Multiset α) (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) l) x → f x ≡ g x [ZMOD n]
⊢ (Multiset.map f (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) l)).prod ≡
    (Multiset.map g (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) l)).prod [ZMOD n]

Tactic:
simpa using listProd_map (l := l) h

Premises used: Int.ModEq.listProd_map
-- Module: Mathlib.Algebra.BigOperators.ModEq
Goal:
α : Type u_1
n : ℤ
f : α → ℤ
s : Multiset α
h : ∀ x ∈ s, f x ≡ 1 [ZMOD n]
⊢ (Multiset.map f s).prod ≡ 1 [ZMOD n]

Tactic:
simpa using multisetProd_map h

Premises used: Int.ModEq.multisetProd_map
-- Module: Mathlib.Algebra.BigOperators.ModEq
Goal:
n : ℤ
s : Multiset ℤ
h : ∀ x ∈ s, x ≡ 1 [ZMOD n]
⊢ s.prod ≡ 1 [ZMOD n]

Tactic:
simpa using multisetProd_map_one h

Premises used: Int.ModEq.multisetProd_map_one
-- Module: Mathlib.Algebra.BigOperators.ModEq
Goal:
α : Type u_1
n : ℤ
f g : α → ℤ
s : Multiset α
h : ∀ x ∈ s, f x ≡ g x [ZMOD n]
mk :
  ∀ (l : List α)
    (h :
      ∀ (x : α),
        Membership.mem (γ := Multiset α) (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) l) x →
          f x ≡ g x [ZMOD n]),
    (Multiset.map f (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) l)).sum ≡
      (Multiset.map g (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) l)).sum [ZMOD n]
⊢ (Multiset.map f s).sum ≡ (Multiset.map g s).sum [ZMOD n]

Tactic:
rcases s with ⟨l⟩
-- Module: Mathlib.Algebra.BigOperators.ModEq
Goal:
α : Type u_1
n : ℤ
f g : α → ℤ
s : Multiset α
l : List α
h :
  ∀ (x : α),
    Membership.mem (γ := Multiset α) (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) l) x → f x ≡ g x [ZMOD n]
⊢ (Multiset.map f (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) l)).sum ≡
    (Multiset.map g (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) l)).sum [ZMOD n]

Tactic:
simpa using listSum_map (l := l) h

Premises used: Int.ModEq.listSum_map
-- Module: Mathlib.Algebra.BigOperators.ModEq
Goal:
α : Type u_1
n : ℤ
f : α → ℤ
s : Multiset α
h : ∀ x ∈ s, f x ≡ 0 [ZMOD n]
⊢ (Multiset.map f s).sum ≡ 0 [ZMOD n]

Tactic:
simpa using multisetSum_map h

Premises used: Int.ModEq.multisetSum_map
-- Module: Mathlib.Algebra.BigOperators.ModEq
Goal:
n : ℤ
s : Multiset ℤ
h : ∀ x ∈ s, x ≡ 0 [ZMOD n]
⊢ s.sum ≡ 0 [ZMOD n]

Tactic:
simpa using multisetSum_map_zero h

Premises used: Int.ModEq.multisetSum_map_zero
-- Module: Mathlib.Algebra.BigOperators.ModEq
Goal:
α : Type u_1
n : ℤ
f g : α → ℤ
s : Finset α
h : ∀ x ∈ s, f x ≡ g x [ZMOD n]
⊢ ∏ x ∈ s, f x ≡ ∏ x ∈ s, g x [ZMOD n]

Tactic:
.multisetProd_map (s := s.1) h

Premises used: Finset.prod, Int.ModEq.multisetProd_map
-- Module: Mathlib.Algebra.BigOperators.ModEq
Goal:
α : Type u_1
n : ℤ
f : α → ℤ
s : Finset α
h : ∀ x ∈ s, f x ≡ 1 [ZMOD n]
⊢ ∏ x ∈ s, f x ≡ 1 [ZMOD n]

Tactic:
simpa using ModEq.prod h

Premises used: Int.ModEq.prod
-- Module: Mathlib.Algebra.BigOperators.ModEq
Goal:
α : Type u_1
n : ℤ
f g : α → ℤ
s : Finset α
h : ∀ x ∈ s, f x ≡ g x [ZMOD n]
⊢ ∑ x ∈ s, f x ≡ ∑ x ∈ s, g x [ZMOD n]

Tactic:
.multisetSum_map (s := s.1) h

Premises used: Int.ModEq.multisetSum_map, Finset.sum
-- Module: Mathlib.Algebra.BigOperators.ModEq
Goal:
α : Type u_1
n : ℤ
f : α → ℤ
s : Finset α
h : ∀ x ∈ s, f x ≡ 0 [ZMOD n]
⊢ ∑ x ∈ s, f x ≡ 0 [ZMOD n]

Tactic:
.multisetSum_map_zero (s := s.1) h

Premises used: Int.ModEq.multisetSum_map_zero, Finset.sum
-- Module: Mathlib.Algebra.BigOperators.ModEq
Goal:
α : Type u_1
n : ℤ
f : α → ℤ
inst : DecidableEq α
s : Finset α
a : α
hf : ∀ x ∈ s, x ≠ a → f x ≡ 1 [ZMOD n]
simp :
  ∀ (hf : ∀ x ∈ s, x ≠ a → Eq (α := ZMod n.natAbs) (↑(f x) : ZMod n.natAbs) 1),
    Eq (α := ZMod n.natAbs) (∏ i ∈ s, (↑(f i) : ZMod n.natAbs)) (if a ∈ s then (↑(f a) : ZMod n.natAbs) else 1)
⊢ ∏ x ∈ s, f x ≡ if a ∈ s then f a else 1 [ZMOD n]

Tactic:
simp only [← modEq_natAbs (n := n), ← ZMod.intCast_eq_intCast_iff, cast_one, cast_prod,
    apply_ite Int.cast] at *

Premises used: Int.cast, apply_ite, Int.modEq_natAbs, ZMod.intCast_eq_intCast_iff, Int.cast_prod, Int.cast_one
-- Module: Mathlib.Algebra.BigOperators.ModEq
Goal:
α : Type u_1
n : ℤ
f : α → ℤ
inst : DecidableEq α
s : Finset α
a : α
hf : ∀ x ∈ s, x ≠ a → Eq (α := ZMod n.natAbs) (↑(f x) : ZMod n.natAbs) 1
⊢ Eq (α := ZMod n.natAbs) (∏ i ∈ s, (↑(f i) : ZMod n.natAbs)) (if a ∈ s then (↑(f a) : ZMod n.natAbs) else 1)

Tactic:
Finset.prod_eq_ite _ hf

Premises used: Finset.prod_eq_ite
-- Module: Mathlib.Algebra.BigOperators.ModEq
Goal:
α : Type u_1
n : ℤ
f : α → ℤ
inst : DecidableEq α
s : Finset α
a : α
hf : ∀ x ∈ s, x ≠ a → Eq (α := ZMod n.natAbs) (↑(f x) : ZMod n.natAbs) 1
⊢ Eq (α := ZMod n.natAbs) (∏ i ∈ s, (↑(f i) : ZMod n.natAbs)) (if a ∈ s then (↑(f a) : ZMod n.natAbs) else 1)

Tactic:
exact Finset.prod_eq_ite _ hf

Premises used: Finset.prod_eq_ite
-- Module: Mathlib.Algebra.BigOperators.ModEq
Goal:
α : Type u_1
n : ℤ
f : α → ℤ
s : Finset α
a : α
ha : a ∉ s → f a ≡ 1 [ZMOD n]
hf : ∀ x ∈ s, x ≠ a → f x ≡ 1 [ZMOD n]
simp :
  ∀ (ha : a ∉ s → Eq (α := ZMod n.natAbs) (↑(f a) : ZMod n.natAbs) 1)
    (hf : ∀ x ∈ s, x ≠ a → Eq (α := ZMod n.natAbs) (↑(f x) : ZMod n.natAbs) 1),
    Eq (α := ZMod n.natAbs) (∏ i ∈ s, (↑(f i) : ZMod n.natAbs)) (↑(f a) : ZMod n.natAbs)
⊢ ∏ x ∈ s, f x ≡ f a [ZMOD n]

Tactic:
simp only [← modEq_natAbs (n := n), ← ZMod.intCast_eq_intCast_iff, cast_one, cast_prod] at *

Premises used: Int.modEq_natAbs, ZMod.intCast_eq_intCast_iff, Int.cast_prod, Int.cast_one
-- Module: Mathlib.Algebra.BigOperators.ModEq
Goal:
α : Type u_1
n : ℤ
f : α → ℤ
s : Finset α
a : α
ha : a ∉ s → Eq (α := ZMod n.natAbs) (↑(f a) : ZMod n.natAbs) 1
hf : ∀ x ∈ s, x ≠ a → Eq (α := ZMod n.natAbs) (↑(f x) : ZMod n.natAbs) 1
h₀ : ∀ b ∈ s, b ≠ a → Eq (α := ZMod n.natAbs) (↑(f b) : ZMod n.natAbs) 1
h₁ : a ∉ s → Eq (α := ZMod n.natAbs) (↑(f a) : ZMod n.natAbs) 1
⊢ Eq (α := ZMod n.natAbs) (∏ i ∈ s, (↑(f i) : ZMod n.natAbs)) (↑(f a) : ZMod n.natAbs)

Tactic:
apply Finset.prod_eq_single

Premises used: Finset.prod_eq_single
-- Module: Mathlib.Algebra.BigOperators.ModEq
Goal:
α : Type u_1
n : ℤ
f : α → ℤ
s : Finset α
a : α
ha : a ∉ s → Eq (α := ZMod n.natAbs) (↑(f a) : ZMod n.natAbs) 1
hf : ∀ x ∈ s, x ≠ a → Eq (α := ZMod n.natAbs) (↑(f x) : ZMod n.natAbs) 1
⊢ ∀ b ∈ s, b ≠ a → Eq (α := ZMod n.natAbs) (↑(f b) : ZMod n.natAbs) 1

Tactic:
assumption
-- Module: Mathlib.Algebra.BigOperators.ModEq
Goal:
α : Type u_1
n : ℤ
f : α → ℤ
s : Finset α
a : α
ha : a ∉ s → Eq (α := ZMod n.natAbs) (↑(f a) : ZMod n.natAbs) 1
hf : ∀ x ∈ s, x ≠ a → Eq (α := ZMod n.natAbs) (↑(f x) : ZMod n.natAbs) 1
⊢ a ∉ s → Eq (α := ZMod n.natAbs) (↑(f a) : ZMod n.natAbs) 1

Tactic:
assumption
-- Module: Mathlib.Algebra.BigOperators.ModEq
Goal:
α : Type u_1
n : ℤ
f : α → ℤ
inst : DecidableEq α
s : Finset α
a : α
hf : ∀ x ∈ s, x ≠ a → f x ≡ 0 [ZMOD n]
simp :
  ∀ (hf : ∀ x ∈ s, x ≠ a → Eq (α := ZMod n.natAbs) (↑(f x) : ZMod n.natAbs) 0),
    Eq (α := ZMod n.natAbs) (∑ x ∈ s, (↑(f x) : ZMod n.natAbs)) (if a ∈ s then (↑(f a) : ZMod n.natAbs) else 0)
⊢ ∑ x ∈ s, f x ≡ if a ∈ s then f a else 0 [ZMOD n]

Tactic:
simp only [← modEq_natAbs (n := n), ← ZMod.intCast_eq_intCast_iff, cast_zero, cast_sum,
    apply_ite Int.cast] at *

Premises used: Int.cast, Int.cast_zero, apply_ite, Int.cast_sum, Int.modEq_natAbs, ZMod.intCast_eq_intCast_iff
-- Module: Mathlib.Algebra.BigOperators.ModEq
Goal:
α : Type u_1
n : ℤ
f : α → ℤ
inst : DecidableEq α
s : Finset α
a : α
hf : ∀ x ∈ s, x ≠ a → Eq (α := ZMod n.natAbs) (↑(f x) : ZMod n.natAbs) 0
⊢ Eq (α := ZMod n.natAbs) (∑ x ∈ s, (↑(f x) : ZMod n.natAbs)) (if a ∈ s then (↑(f a) : ZMod n.natAbs) else 0)

Tactic:
Finset.sum_eq_ite _ hf

Premises used: Finset.sum_eq_ite
-- Module: Mathlib.Algebra.BigOperators.ModEq
Goal:
α : Type u_1
n : ℤ
f : α → ℤ
inst : DecidableEq α
s : Finset α
a : α
hf : ∀ x ∈ s, x ≠ a → Eq (α := ZMod n.natAbs) (↑(f x) : ZMod n.natAbs) 0
⊢ Eq (α := ZMod n.natAbs) (∑ x ∈ s, (↑(f x) : ZMod n.natAbs)) (if a ∈ s then (↑(f a) : ZMod n.natAbs) else 0)

Tactic:
exact Finset.sum_eq_ite _ hf

Premises used: Finset.sum_eq_ite
-- Module: Mathlib.Algebra.BigOperators.ModEq
Goal:
α : Type u_1
n : ℤ
f : α → ℤ
s : Finset α
a : α
ha : a ∉ s → f a ≡ 0 [ZMOD n]
hf : ∀ x ∈ s, x ≠ a → f x ≡ 0 [ZMOD n]
simp :
  ∀ (ha : a ∉ s → Eq (α := ZMod n.natAbs) (↑(f a) : ZMod n.natAbs) 0)
    (hf : ∀ x ∈ s, x ≠ a → Eq (α := ZMod n.natAbs) (↑(f x) : ZMod n.natAbs) 0),
    Eq (α := ZMod n.natAbs) (∑ x ∈ s, (↑(f x) : ZMod n.natAbs)) (↑(f a) : ZMod n.natAbs)
⊢ ∑ x ∈ s, f x ≡ f a [ZMOD n]

Tactic:
simp only [← modEq_natAbs (n := n), ← ZMod.intCast_eq_intCast_iff, cast_zero, cast_sum] at *

Premises used: Int.cast_zero, Int.cast_sum, Int.modEq_natAbs, ZMod.intCast_eq_intCast_iff