awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
m : Multiset ι
f : { x : ι // x ∈ m } → M
g : ι → M
hfg : ∀ (x : { x : ι // x ∈ m }), f x = g (↑x : ι)
⊢ ∀ (a : ι) (ha : a ∈ m.toFinset),
    (fun (x : { x : ι // x ∈ m }) (x_1 : Membership.mem (γ := Finset { x : ι // x ∈ m }) univ x) ↦ (↑x : ι))
        ((fun (x : ι) (hx : x ∈ m.toFinset) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ m) x ⋯) a ha) ⋯ =
      a

Tactic:
simp [hfg]
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
m : Multiset ι
f : { x : ι // x ∈ m } → M
g : ι → M
hfg : ∀ (x : { x : ι // x ∈ m }), f x = g (↑x : ι)
⊢ ∀ (a : { x : ι // x ∈ m }) (ha : Membership.mem (γ := Finset { x : ι // x ∈ m }) univ a),
    f a =
      g ((fun (x : { x : ι // x ∈ m }) (x_1 : Membership.mem (γ := Finset { x : ι // x ∈ m }) univ x) ↦ (↑x : ι)) a ha)

Tactic:
simp [hfg]
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
s : Finset ι
M : Type u_7
inst : CommMonoid M
f : ι → M
p : M → Prop
hom : ∀ (a b : M), p a → p b → p (a * b)
unit : p 1
base : ∀ x ∈ s, p (f x)
⊢ p (∏ x ∈ s, f x)

Tactic:
Multiset.prod_induction _ _ hom unit (Multiset.forall_mem_map_iff.mpr base)

Premises used: Iff.mpr, Multiset.prod_induction, Finset.prod, Multiset.forall_mem_map_iff
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
s : Finset ι
M : Type u_7
inst : CommMonoid M
f : ι → M
p : M → Prop
hom : ∀ (a b : M), p a → p b → p (a * b)
nonempty : s.Nonempty
base : ∀ x ∈ s, p (f x)
⊢ Ne.{u_7 + 1} (α := Multiset M) (Multiset.map (fun (x : ι) ↦ f x) s.val) ∅

Tactic:
simp [nonempty_iff_ne_empty.mp nonempty]

Premises used: Finset.nonempty_iff_ne_empty, Iff.mp
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
s : Finset ι
n : ℕ
f : ι → M
⊢ ∏ x ∈ s, f x ^ n = HPow.hPow (α := M) (∏ x ∈ s, f x) n

Tactic:
Multiset.prod_map_pow

Premises used: Multiset.prod_map_pow, Finset.prod
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_7
M : Type u_8
inst : CommMonoid M
s t : Finset ι
f : ι → M
h : s ⊆ t
⊢ s.val ≤ t.val

Tactic:
simpa
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
M : Type u_3
inst : AddCommMonoid M
s : Finset ι
f : ι → M
⊢ Eq.{u_3 + 1} (α := Mᵐᵒᵖ) (op (∑ x ∈ s, f x)) (∑ x ∈ s, op (f x))

Tactic:
map_sum opAddEquiv ..

Premises used: MulOpposite.opAddEquiv, map_sum, MulOpposite.op
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
M : Type u_3
inst : AddCommMonoid M
s : Finset ι
f : ι → Mᵐᵒᵖ
⊢ Eq.{u_3 + 1} (α := M) (unop (∑ x ∈ s, f x)) (∑ x ∈ s, unop (f x))

Tactic:
map_sum opAddEquiv.symm ..

Premises used: MulOpposite.opAddEquiv, map_sum, MulOpposite.unop, AddEquiv.symm
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
s : Finset ι
f : ι → M
⊢ Eq.{u_3 + 1} (α := Mᵃᵒᵖ) (op (∏ i ∈ s, f i)) (∏ i ∈ s, op (f i))

Tactic:
map_prod opMulEquiv ..

Premises used: AddOpposite.opMulEquiv, map_prod, AddOpposite.op
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
s : Finset ι
f : ι → Mᵐᵒᵖ
⊢ Eq.{u_3 + 1} (α := M) (unop (∏ i ∈ s, f i)) (∏ i ∈ s, unop (f i))

Tactic:
map_prod opMulEquiv.symm ..

Premises used: AddOpposite.opMulEquiv, map_prod, AddOpposite.unop, MulEquiv.symm
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
G : Type u_5
s : Finset ι
inst : DivisionCommMonoid G
f : ι → G
⊢ Eq.{u_5 + 1} (α := G) (∏ x ∈ s, (f x)⁻¹) (∏ x ∈ s, f x)⁻¹

Tactic:
Multiset.prod_map_inv

Premises used: Finset.prod, Multiset.prod_map_inv
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
G : Type u_5
s : Finset ι
inst : DivisionCommMonoid G
f g : ι → G
⊢ ∏ x ∈ s, f x / g x = HDiv.hDiv (α := G) (∏ x ∈ s, f x) (∏ x ∈ s, g x)

Tactic:
Multiset.prod_map_div

Premises used: Finset.prod, Multiset.prod_map_div
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
G : Type u_5
inst : DivisionCommMonoid G
f : ι → G
s : Finset ι
n : ℤ
⊢ ∏ a ∈ s, f a ^ n = HPow.hPow (α := G) (∏ a ∈ s, f a) n

Tactic:
Multiset.prod_map_zpow

Premises used: Finset.prod, Multiset.prod_map_zpow
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
s : Finset ι
n : ℕ
f : ι → ℕ
rw :
  Multiset.sum (Multiset.map ((fun (x : ℕ) ↦ x % n) ∘ fun (i : ι) ↦ f i) s.val) % n =
    Multiset.sum (Multiset.map (fun (i : ι) ↦ f i % n) s.val) % n
⊢ Multiset.sum (Multiset.map (fun (x : ℕ) ↦ x % n) (Multiset.map (fun (i : ι) ↦ f i) s.val)) % n =
    (∑ i ∈ s, f i % n) % n

Tactic:
rw [Finset.sum, Multiset.map_map]

Premises used: Multiset.map_map, Finset.sum
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
s : Finset ι
n : ℕ
f : ι → ℕ
⊢ Multiset.sum (Multiset.map ((fun (x : ℕ) ↦ x % n) ∘ fun (i : ι) ↦ f i) s.val) % n =
    Multiset.sum (Multiset.map (fun (i : ι) ↦ f i % n) s.val) % n

Tactic:
rfl
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
s : Finset ι
n : ℕ
f : ι → ℕ
rw :
  Multiset.prod (Multiset.map ((fun (x : ℕ) ↦ x % n) ∘ fun (i : ι) ↦ f i) s.val) % n =
    Multiset.prod (Multiset.map (fun (i : ι) ↦ f i % n) s.val) % n
⊢ Multiset.prod (Multiset.map (fun (x : ℕ) ↦ x % n) (Multiset.map (fun (i : ι) ↦ f i) s.val)) % n =
    (∏ i ∈ s, f i % n) % n

Tactic:
rw [Finset.prod, Multiset.map_map]

Premises used: Finset.prod, Multiset.map_map
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
s : Finset ι
n : ℕ
f : ι → ℕ
⊢ Multiset.prod (Multiset.map ((fun (x : ℕ) ↦ x % n) ∘ fun (i : ι) ↦ f i) s.val) % n =
    Multiset.prod (Multiset.map (fun (i : ι) ↦ f i % n) s.val) % n

Tactic:
rfl
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
s : Finset ι
n : ℤ
f : ι → ℤ
rw :
  Multiset.sum (Multiset.map ((fun (x : ℤ) ↦ x % n) ∘ fun (i : ι) ↦ f i) s.val) % n =
    Multiset.sum (Multiset.map (fun (i : ι) ↦ f i % n) s.val) % n
⊢ Multiset.sum (Multiset.map (fun (x : ℤ) ↦ x % n) (Multiset.map (fun (i : ι) ↦ f i) s.val)) % n =
    (∑ i ∈ s, f i % n) % n

Tactic:
rw [Finset.sum, Multiset.map_map]

Premises used: Multiset.map_map, Finset.sum
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
s : Finset ι
n : ℤ
f : ι → ℤ
⊢ Multiset.sum (Multiset.map ((fun (x : ℤ) ↦ x % n) ∘ fun (i : ι) ↦ f i) s.val) % n =
    Multiset.sum (Multiset.map (fun (i : ι) ↦ f i % n) s.val) % n

Tactic:
rfl
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
s : Finset ι
n : ℤ
f : ι → ℤ
rw :
  Multiset.prod (Multiset.map ((fun (x : ℤ) ↦ x % n) ∘ fun (i : ι) ↦ f i) s.val) % n =
    Multiset.prod (Multiset.map (fun (i : ι) ↦ f i % n) s.val) % n
⊢ Multiset.prod (Multiset.map (fun (x : ℤ) ↦ x % n) (Multiset.map (fun (i : ι) ↦ f i) s.val)) % n =
    (∏ i ∈ s, f i % n) % n

Tactic:
rw [Finset.prod, Multiset.map_map]

Premises used: Finset.prod, Multiset.map_map
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
s : Finset ι
n : ℤ
f : ι → ℤ
⊢ Multiset.prod (Multiset.map ((fun (x : ℤ) ↦ x % n) ∘ fun (i : ι) ↦ f i) s.val) % n =
    Multiset.prod (Multiset.map (fun (i : ι) ↦ f i % n) s.val) % n

Tactic:
rfl
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_3
inst : Fintype ι
inst_1 : Fintype κ
inst_2 : CommMonoid M
e : ι → κ
he : Bijective e
f : ι → M
g : κ → M
h : ∀ (x : ι), f x = g (e x)
⊢ ∀ (i : ι),
    Membership.mem (γ := Finset ι) univ i ↔
      Membership.mem.{u_2, u_2} (α := κ) (γ := Finset κ) univ ((Equiv.ofBijective e he : (a : ι) → κ) i : κ)

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_3
inst : Fintype ι
inst_1 : Fintype κ
inst_2 : CommMonoid M
e : ι → κ
he : Bijective e
f : ι → M
g : κ → M
h : ∀ (x : ι), f x = g (e x)
⊢ ∀ (i : ι), Membership.mem (γ := Finset ι) univ i → f i = g ((Equiv.ofBijective e he : (a : ι) → κ) i)

Tactic:
simp [h]
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_3
inst : Fintype ι
inst_1 : Fintype κ
inst_2 : CommMonoid M
e : ι ≃ κ
f : ι → M
g : κ → M
h : ∀ (x : ι), f x = g ((e : (a : ι) → κ) x)
⊢ Eq.{u_3 + 1} (α := M) (∏ x : ι, f x) (∏ x : κ, g x)

Tactic:
prod_bijective _ e.bijective _ _ h

Premises used: Equiv.bijective, Fintype.prod_bijective
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_3
inst : Fintype ι
inst_1 : Fintype κ
inst_2 : CommMonoid M
e : ι → κ
he : Bijective e
g : κ → M
⊢ Eq.{u_3 + 1} (α := M) (∏ i : ι, g (e i)) (∏ i : κ, g i)

Tactic:
prod_bijective _ he _ _ fun _ ↦ rfl

Premises used: Fintype.prod_bijective, rfl
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_3
inst : Fintype ι
inst_1 : Fintype κ
inst_2 : CommMonoid M
e : ι ≃ κ
g : κ → M
⊢ Eq.{u_3 + 1} (α := M) (∏ i : ι, g ((e : (a : ι) → κ) i)) (∏ i : κ, g i)

Tactic:
prod_equiv e _ _ fun _ ↦ rfl

Premises used: Fintype.prod_equiv, rfl
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
M : Type u_3
inst : Fintype ι
inst_1 : CommMonoid M
inst_2 : IsEmpty ι
f : ι → M
⊢ Eq.{u_3 + 1} (α := M) (∏ x : ι, f x) 1

Tactic:
prod_of_isEmpty _

Premises used: Finset.prod_of_isEmpty
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : Fintype ι
f : ↥univ → M
⊢ ∀ (x : Subtype (Membership.mem (γ := Finset ι) univ)),
    f x =
      f
        (Subtype.mk (p := fun (i : ι) ↦ Membership.mem (γ := Finset ι) univ i)
          ((Equiv.subtypeUnivEquiv (p := Membership.mem (γ := Finset ι) univ) ⋯ :
              (a : Subtype (Membership.mem univ)) → ι)
            x)
          ⋯)

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s : Finset ι
f : ι → M
i : ↥s
rw :
  Eq.{u_3 + 1} (α := M) (∏ x ∈ map (Embedding.subtype fun (x : ι) ↦ x ∈ s) (s.attach.erase i), f x)
    (∏ j ∈ s.erase ((Embedding.subtype fun (x : ι) ↦ x ∈ s : (a : ↥s) → ι) i), f j)
⊢ Eq.{u_3 + 1} (α := M) (∏ j ∈ s.attach.erase i, f (↑j : ι)) (∏ j ∈ s.erase (↑i : ι), f j)

Tactic:
rw [← Function.Embedding.coe_subtype, ← prod_map]

Premises used: Function.Embedding.coe_subtype, Finset.prod_map
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s : Finset ι
f : ι → M
i : ↥s
⊢ Eq.{u_3 + 1} (α := M) (∏ x ∈ map (Embedding.subtype fun (x : ι) ↦ x ∈ s) (s.attach.erase i), f x)
    (∏ j ∈ s.erase ((Embedding.subtype fun (x : ι) ↦ x ∈ s : (a : ↥s) → ι) i), f j)

Tactic:
simp [attach_map_val]

Premises used: Finset.attach_map_val
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
α : Type u_6
s : Finset ι
f : ι → Multiset α
⊢ card.{u_6} (α := α) (∑ i ∈ s, f i) = ∑ i ∈ s, (f i).card

Tactic:
map_sum cardHom ..

Premises used: map_sum, Multiset.cardHom, Multiset.card
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
α : Type u_6
a : Multiset α
⊢ Disjoint (List.sum []) a ↔ ∀ (b : Multiset α), Membership.mem (γ := List (Multiset α)) [] b → Disjoint b a

Tactic:
simp only [zero_disjoint, List.not_mem_nil, IsEmpty.forall_iff, forall_const, List.sum_nil]

Premises used: List.sum_nil, Multiset.zero_disjoint, forall_const, List.not_mem_nil, IsEmpty.forall_iff
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
α : Type u_6
a b : Multiset α
bs : List (Multiset α)
ih : Disjoint bs.sum a ↔ ∀ b ∈ bs, Disjoint b a
⊢ Disjoint (b :: bs).sum a ↔ ∀ b_1 ∈ b :: bs, Disjoint b_1 a

Tactic:
simp [ih]
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
α : Type u_6
a : Multiset α
l : List (Multiset α)
nil : Disjoint (List.sum []) a ↔ ∀ (b : Multiset α), Membership.mem (γ := List (Multiset α)) [] b → Disjoint b a
cons :
  ∀ (b : Multiset α) (bs : List (Multiset α)) (ih : Disjoint bs.sum a ↔ ∀ b ∈ bs, Disjoint b a),
    Disjoint (b :: bs).sum a ↔ ∀ b_1 ∈ b :: bs, Disjoint b_1 a
⊢ Disjoint l.sum a ↔ ∀ b ∈ l, Disjoint b a

Tactic:
induction l with
  | nil =>
    simp only [zero_disjoint, List.not_mem_nil, IsEmpty.forall_iff, forall_const, List.sum_nil]
  | cons b bs ih =>
    simp [ih]

Premises used: List.sum_nil, Multiset.cons, Multiset.zero_disjoint, forall_const, List.not_mem_nil, IsEmpty.forall_iff
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
α : Type u_6
a : Multiset α
l : List (Multiset α)
⊢ Disjoint a l.sum ↔ ∀ b ∈ l, Disjoint a b

Tactic:
simpa only [disjoint_comm (a := a)] using disjoint_list_sum_left

Premises used: Multiset.disjoint_list_sum_left, disjoint_comm
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
α : Type u_6
a : Multiset α
i : Multiset (Multiset α)
l : List (Multiset α)
⊢ Disjoint l.sum a ↔ ∀ b ∈ (↑l : Multiset (Multiset α)), Disjoint b a

Tactic:
disjoint_list_sum_left

Premises used: Multiset.disjoint_list_sum_left, Multiset.Mem
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
α : Type u_6
a : Multiset α
i : Multiset (Multiset α)
l : List (Multiset α)
⊢ Disjoint l.sum a ↔ ∀ b ∈ (↑l : Multiset (Multiset α)), Disjoint b a

Tactic:
exact disjoint_list_sum_left

Premises used: Multiset.disjoint_list_sum_left
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
α : Type u_6
a : Multiset α
i : Multiset (Multiset α)
⊢ Disjoint a i.sum ↔ ∀ b ∈ i, Disjoint a b

Tactic:
simpa only [disjoint_comm (a := a)] using disjoint_sum_left

Premises used: disjoint_comm, Multiset.disjoint_sum_left
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
α : Type u_6
i : Finset ι
f : ι → Multiset α
a : Multiset α
⊢ Disjoint (map f i.val).sum a ↔ ∀ b ∈ map f i.val, Disjoint b a

Tactic:
@disjoint_sum_left _ a (map f i.val)

Premises used: Multiset.disjoint_sum_left
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
α : Type u_6
i : Finset ι
f : ι → Multiset α
a : Multiset α
h : (∀ b ∈ i, Disjoint (f b) a) ↔ ∀ b ∈ map f i.val, Disjoint b a
⊢ Disjoint (i.sum f) a ↔ ∀ b ∈ i, Disjoint (f b) a

Tactic:
convert! @disjoint_sum_left _ a (map f i.val)

Premises used: Multiset.disjoint_sum_left
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
α : Type u_6
i : Finset ι
f : ι → Multiset α
a : Multiset α
⊢ (∀ b ∈ i, Disjoint (f b) a) ↔ ∀ b ∈ map f i.val, Disjoint b a

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
α : Type u_6
i : Finset ι
f : ι → Multiset α
a : Multiset α
⊢ Disjoint a (i.sum f) ↔ ∀ b ∈ i, Disjoint a (f b)

Tactic:
simpa only [disjoint_comm] using disjoint_finsetSum_left

Premises used: disjoint_comm, Multiset.disjoint_finsetSum_left
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
α : Type u_6
inst : DecidableEq α
s : Finset ι
a : α
f : ι → Multiset α
rw rw₁ : Eq (α := ℕ) (sum (map (fun (b : ι) ↦ count a (f b)) s.val)) (sum (map (fun (x : ι) ↦ count a (f x)) s.val))
⊢ count a (sum (map (fun (x : ι) ↦ f x) s.val)) = sum (map (fun (x : ι) ↦ count a (f x)) s.val)

Tactic:
rw [count_sum]

Premises used: Multiset.count_sum
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
M : Type u_3
inst : DecidableEq M
inst_1 : CommMonoid M
S : Multiset M
rw : (map id S.toFinset.val).prod ∣ S.prod
⊢ S.toFinset.prod id ∣ S.prod

Tactic:
rw [Finset.prod_eq_multiset_prod]

Premises used: Finset.prod_eq_multiset_prod
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
M : Type u_3
inst : DecidableEq M
inst_1 : CommMonoid M
S : Multiset M
⊢ (map id S.toFinset.val).prod ∣ S.prod

Tactic:
Multiset.prod_dvd_prod_of_le ?_

Premises used: Multiset.prod_dvd_prod_of_le
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
M : Type u_3
inst : DecidableEq M
inst_1 : CommMonoid M
S : Multiset M
refine : map id S.toFinset.val ≤ S
⊢ (map id S.toFinset.val).prod ∣ S.prod

Tactic:
refine Multiset.prod_dvd_prod_of_le ?_

Premises used: Multiset.prod_dvd_prod_of_le
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
M : Type u_3
inst : DecidableEq M
inst_1 : CommMonoid M
S : Multiset M
⊢ map id S.toFinset.val ≤ S

Tactic:
simp [Multiset.dedup_le S]

Premises used: Multiset.dedup_le
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
M : Type u_3
α : Type u_6
inst : CommMonoid M
f : α → Mˣ
s : Finset α
⊢ Eq.{u_3 + 1} (α := M) (↑(∏ i ∈ s, f i) : M) (∏ i ∈ s, (↑(f i) : M))

Tactic:
map_prod (Units.coeHom M) _ _

Premises used: Units.coeHom, map_prod
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
M : Type u_3
inst : Monoid M
s : List M
simp : s.prod = s.sum
⊢ Eq (α := Additive M) ((ofMul : (a : M) → Additive M) s.prod : Additive M)
    (List.sum (List.map (⇑ofMul : (a : M) → Additive M) s) : Additive M)

Tactic:
simp [ofMul]

Premises used: Additive.ofMul
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
M : Type u_3
inst : Monoid M
s : List M
⊢ s.prod = s.sum

Tactic:
rfl
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
M : Type u_3
inst : Monoid M
s : List (Additive M)
simp : s.sum = s.prod
⊢ Eq (α := M) ((toMul : (a : Additive M) → M) s.sum : M) (List.prod (List.map (⇑toMul : (a : Additive M) → M) s) : M)

Tactic:
simp [toMul, ofMul]

Premises used: Additive.toMul, Additive.ofMul
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
M : Type u_3
inst : Monoid M
s : List (Additive M)
⊢ s.sum = s.prod

Tactic:
rfl
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
M : Type u_3
inst : AddMonoid M
s : List M
simp : s.sum = s.prod
⊢ Eq (α := Multiplicative M) ((ofAdd : (a : M) → Multiplicative M) s.sum : Multiplicative M)
    (List.prod (List.map (⇑ofAdd : (a : M) → Multiplicative M) s) : Multiplicative M)

Tactic:
simp [ofAdd]

Premises used: Multiplicative.ofAdd
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
M : Type u_3
inst : AddMonoid M
s : List M
⊢ s.sum = s.prod

Tactic:
rfl
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
M : Type u_3
inst : AddMonoid M
s : List (Multiplicative M)
simp : s.prod = s.sum
⊢ Eq (α := M) ((toAdd : (a : Multiplicative M) → M) s.prod : M)
    (List.sum (List.map (⇑toAdd : (a : Multiplicative M) → M) s) : M)

Tactic:
simp [toAdd, ofAdd]

Premises used: Multiplicative.toAdd, Multiplicative.ofAdd
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
M : Type u_3
inst : AddMonoid M
s : List (Multiplicative M)
⊢ s.prod = s.sum

Tactic:
rfl
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
M : Type u_3
inst : CommMonoid M
s : Multiset M
simp : s.prod = s.sum
⊢ Eq (α := Additive M) ((ofMul : (a : M) → Additive M) s.prod : Additive M)
    (Multiset.sum (Multiset.map (⇑ofMul : (a : M) → Additive M) s) : Additive M)

Tactic:
simp [ofMul]

Premises used: Additive.ofMul
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
M : Type u_3
inst : CommMonoid M
s : Multiset M
⊢ s.prod = s.sum

Tactic:
rfl
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
M : Type u_3
inst : CommMonoid M
s : Multiset (Additive M)
simp : s.sum = s.prod
⊢ Eq (α := M) ((toMul : (a : Additive M) → M) s.sum : M)
    (Multiset.prod (Multiset.map (⇑toMul : (a : Additive M) → M) s) : M)

Tactic:
simp [toMul, ofMul]

Premises used: Additive.toMul, Additive.ofMul
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
M : Type u_3
inst : CommMonoid M
s : Multiset (Additive M)
⊢ s.sum = s.prod

Tactic:
rfl
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
s : Finset ι
f : ι → M
⊢ Eq.{u_3 + 1} (α := Additive M) ((ofMul : (a : M) → Additive M) (∏ i ∈ s, f i) : Additive M)
    (∑ i ∈ s, (ofMul : (a : M) → Additive M) (f i) : Additive M)

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Additive, Multiset.prod, Finset.prod, Finset.sum, rfl
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
s : Finset ι
f : ι → Additive M
⊢ Eq.{u_3 + 1} (α := M) ((toMul : (a : Additive M) → M) (∑ i ∈ s, f i) : M)
    (∏ i ∈ s, (toMul : (a : Additive M) → M) (f i) : M)

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Additive, Multiset.prod, Finset.prod, Finset.sum, rfl
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
M : Type u_3
inst : AddCommMonoid M
s : Multiset M
simp : s.sum = s.prod
⊢ Eq (α := Multiplicative M) ((ofAdd : (a : M) → Multiplicative M) s.sum : Multiplicative M)
    (Multiset.prod (Multiset.map (⇑ofAdd : (a : M) → Multiplicative M) s) : Multiplicative M)

Tactic:
simp [ofAdd]

Premises used: Multiplicative.ofAdd
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
M : Type u_3
inst : AddCommMonoid M
s : Multiset M
⊢ s.sum = s.prod

Tactic:
rfl
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
M : Type u_3
inst : AddCommMonoid M
s : Multiset (Multiplicative M)
simp : s.prod = s.sum
⊢ Eq (α := M) ((toAdd : (a : Multiplicative M) → M) s.prod : M)
    (Multiset.sum (Multiset.map (⇑toAdd : (a : Multiplicative M) → M) s) : M)

Tactic:
simp [toAdd, ofAdd]

Premises used: Multiplicative.toAdd, Multiplicative.ofAdd
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
M : Type u_3
inst : AddCommMonoid M
s : Multiset (Multiplicative M)
⊢ s.prod = s.sum

Tactic:
rfl
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
M : Type u_3
inst : AddCommMonoid M
s : Finset ι
f : ι → M
⊢ Eq.{u_3 + 1} (α := Multiplicative M) ((ofAdd : (a : M) → Multiplicative M) (∑ i ∈ s, f i) : Multiplicative M)
    (∏ i ∈ s, (ofAdd : (a : M) → Multiplicative M) (f i) : Multiplicative M)

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Multiset.prod, Finset.prod, Multiplicative, Finset.sum, rfl
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
M : Type u_3
inst : AddCommMonoid M
s : Finset ι
f : ι → Multiplicative M
⊢ Eq.{u_3 + 1} (α := M) ((toAdd : (a : Multiplicative M) → M) (∏ i ∈ s, f i) : M)
    (∑ i ∈ s, (toAdd : (a : Multiplicative M) → M) (f i) : M)

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Multiset.prod, Finset.prod, Multiplicative, Finset.sum, rfl
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Gaps
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
f : α → α → β
set :
  let p := F.intervalGapsWithin h a b;
  Eq.{u_2 + 1} (α := β) (∏ z ∈ F, f z.1 z.2) (∏ i ∈ range k, f (p (↑i : Fin (k + 1))).2 (p (↑i.succ : Fin (k + 1))).1)
⊢ Eq.{u_2 + 1} (α := β) (∏ z ∈ F, f z.1 z.2)
    (∏ i ∈ range k,
      f (F.intervalGapsWithin h a b (↑i : Fin (k + 1))).2 (F.intervalGapsWithin h a b (↑i.succ : Fin (k + 1))).1)

Tactic:
set p := F.intervalGapsWithin h a b

Premises used: Finset.intervalGapsWithin
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Gaps
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
f : α → α → β
p : (i : Fin (k + 1)) → α × α := F.intervalGapsWithin h a b
symm :
  Eq.{u_2 + 1} (α := β) (∏ i ∈ range k, f (p (↑i : Fin (k + 1))).2 (p (↑i.succ : Fin (k + 1))).1) (∏ z ∈ F, f z.1 z.2)
⊢ Eq.{u_2 + 1} (α := β) (∏ z ∈ F, f z.1 z.2) (∏ i ∈ range k, f (p (↑i : Fin (k + 1))).2 (p (↑i.succ : Fin (k + 1))).1)

Tactic:
symm