awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : CommMonoid M
inst_1 : CommMonoid N
G : Type u_7
inst_2 : FunLike G M N
inst_3 : MonoidHomClass G M N
g : G
f : ι → M
s : Finset ι
simp :
  Eq.{u_4 + 1} (α := N) (Multiset.prod (Multiset.map ((⇑g : (a : M) → N) ∘ f) s.val))
    (Multiset.prod (Multiset.map (fun (x : ι) ↦ (g : (a : M) → N) (f x)) s.val))
⊢ Eq.{u_4 + 1} (α := N) ((g : (a : M) → N) (∏ x ∈ s, f x) : N) (∏ x ∈ s, (g : (a : M) → N) (f x) : N)

Tactic:
simp only [Finset.prod_eq_multiset_prod, map_multiset_prod, Multiset.map_map]

Premises used: map_multiset_prod, Finset.prod_eq_multiset_prod, Multiset.map_map
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : CommMonoid M
inst_1 : CommMonoid N
G : Type u_7
inst_2 : FunLike G M N
inst_3 : MonoidHomClass G M N
g : G
f : ι → M
s : Finset ι
⊢ Eq.{u_4 + 1} (α := N) (Multiset.prod (Multiset.map ((⇑g : (a : M) → N) ∘ f) s.val))
    (Multiset.prod (Multiset.map (fun (x : ι) ↦ (g : (a : M) → N) (f x)) s.val))

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

Tactic:
rfl

Premises used: Multiset.foldr, Multiset.prod, Finset.prod, List.foldr, rfl
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
⊢ Eq (α := (f : ι → M) → M) (Finset.prod ∅) fun (x : ι → M) ↦ 1

Tactic:
rfl

Premises used: Multiset.foldr, Multiset.prod, Finset.prod, List.foldr, rfl
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
M : Type u_3
f : ι → M
inst : CommMonoid M
inst_1 : IsEmpty ι
s : Finset ι
rw : Eq.{u_3 + 1} (α := M) (∏ i ∈ ∅, f i) 1
rw₁ rw₂ : Eq.{u_3 + 1} (α := M) 1 1
⊢ Eq.{u_3 + 1} (α := M) (∏ i ∈ s, f i) 1

Tactic:
rw [eq_empty_of_isEmpty s, prod_empty]

Premises used: Finset.prod_empty, Finset.eq_empty_of_isEmpty
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
M : Type u_3
s : Finset ι
inst : CommMonoid M
⊢ Eq.{u_3 + 1} (α := M) (∏ _x ∈ s, 1) 1

Tactic:
simp only [Finset.prod, Multiset.map_const', Multiset.prod_replicate, one_pow]

Premises used: one_pow, Multiset.prod_replicate, Finset.prod, Multiset.map_const'
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_3
inst : CommMonoid M
s : Finset ι
e : ι ↪ κ
f : κ → M
rw :
  Eq.{u_3 + 1} (α := M) (Multiset.prod (Multiset.map ((fun (x : κ) ↦ f x) ∘ (⇑e : (a : ι) → κ)) s.val))
    (∏ x ∈ s, f ((e : (a : ι) → κ) x))
⊢ Eq.{u_3 + 1} (α := M) (∏ x ∈ map e s, f x) (∏ x ∈ s, f ((e : (a : ι) → κ) x))

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

Premises used: Finset.prod, Finset.map_val, Multiset.map_map
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_3
inst : CommMonoid M
s : Finset ι
e : ι ↪ κ
f : κ → M
⊢ Eq.{u_3 + 1} (α := M) (Multiset.prod (Multiset.map ((fun (x : κ) ↦ f x) ∘ (⇑e : (a : ι) → κ)) s.val))
    (∏ x ∈ s, f ((e : (a : ι) → κ) x))

Tactic:
rfl
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_3
inst : CommMonoid M
s : Finset ι
e : ι ↪ κ
h : ∀ (f : κ → M), (map e s).prod f = ∏ x ∈ s, f ((e : (a : ι) → κ) x)
⊢ Eq (α := (f : κ → M) → M) (map e s).prod fun (f : κ → M) ↦ ∏ x ∈ s, f ((e : (a : ι) → κ) x)

Tactic:
funext f
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_3
inst : CommMonoid M
s : Finset ι
e : ι ↪ κ
f : κ → M
⊢ (map e s).prod f = ∏ x ∈ s, f ((e : (a : ι) → κ) x)

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
s : Finset ι
f : ι → M
rw : (List.map f s.toList).prod = (Multiset.map f s.val).prod
rw₁ : (↑(List.map f s.toList) : Multiset M).prod = (Multiset.map f s.val).prod
rw₂ : (Multiset.map f (↑s.toList : Multiset ι)).prod = (Multiset.map f s.val).prod
rw₃ rw₄ : (Multiset.map f s.val).prod = (Multiset.map f s.val).prod
⊢ (List.map f s.toList).prod = s.prod f

Tactic:
rw [Finset.prod, ← Multiset.prod_coe, ← Multiset.map_coe, Finset.coe_toList]

Premises used: Finset.coe_toList, Finset.prod, Multiset.map_coe, Multiset.prod_coe
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
M : Type u_7
inst : CommMonoid M
s : Finset M
⊢ s.toList.prod = ∏ x ∈ s, x

Tactic:
simpa using s.prod_map_toList id

Premises used: Finset.prod_map_toList, id
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
σ : Equiv.Perm ι
s : Finset ι
f : ι → M
hs : {a : ι | (σ : (a : ι) → ι) a ≠ a} ⊆ (↑s : Set ι)
⊢ Eq.{u_3 + 1} (α := M) (∏ x ∈ s, f ((Equiv.toEmbedding σ : (a : ι) → ι) x)) (∏ x ∈ map (Equiv.toEmbedding σ) s, f x)

Tactic:
(prod_map s σ.toEmbedding f).symm

Premises used: Equiv.toEmbedding, Finset.prod_map, Eq.symm
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
σ : Equiv.Perm ι
s : Finset ι
f : ι → M
hs : {a : ι | (σ : (a : ι) → ι) a ≠ a} ⊆ (↑s : Set ι)
h : s = map (Equiv.toEmbedding σ) s
⊢ Eq.{u_3 + 1} (α := M) (∏ x ∈ s, f ((σ : (a : ι) → ι) x)) (∏ x ∈ s, f x)

Tactic:
convert! (prod_map s σ.toEmbedding f).symm

Premises used: Equiv.toEmbedding, Finset.prod_map, Eq.symm
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
σ : Equiv.Perm ι
s : Finset ι
f : ι → M
hs : {a : ι | (σ : (a : ι) → ι) a ≠ a} ⊆ (↑s : Set ι)
⊢ s = map (Equiv.toEmbedding σ) s

Tactic:
(map_perm hs).symm

Premises used: Eq.symm, Finset.map_perm
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
σ : Equiv.Perm ι
s : Finset ι
f : ι → M
hs : {a : ι | (σ : (a : ι) → ι) a ≠ a} ⊆ (↑s : Set ι)
⊢ s = map (Equiv.toEmbedding σ) s

Tactic:
exact (map_perm hs).symm

Premises used: Eq.symm, Finset.map_perm
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
σ : Equiv.Perm ι
s : Finset ι
f : ι → ι → M
hs : {a : ι | (σ : (a : ι) → ι) a ≠ a} ⊆ (↑s : Set ι)
⊢ Eq.{u_3 + 1} (α := M) (∏ x ∈ s, (fun (x : ι) ↦ f x ((Equiv.symm σ : (a : ι) → ι) x)) ((σ : (a : ι) → ι) x))
    (∏ x ∈ s, (fun (x : ι) ↦ f x ((Equiv.symm σ : (a : ι) → ι) x)) x)

Tactic:
σ.prod_comp s (fun x => f x (σ.symm x)) hs

Premises used: Equiv.Perm.prod_comp, Equiv.symm, DFunLike.coe
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
σ : Equiv.Perm ι
s : Finset ι
f : ι → ι → M
hs : {a : ι | (σ : (a : ι) → ι) a ≠ a} ⊆ (↑s : Set ι)
h : ∀ (x : ι), x = (Equiv.symm σ : (a : ι) → ι) ((σ : (a : ι) → ι) x : ι)
⊢ Eq.{u_3 + 1} (α := M) (∏ x ∈ s, f ((σ : (a : ι) → ι) x) x) (∏ x ∈ s, f x ((Equiv.symm σ : (a : ι) → ι) x))

Tactic:
convert! σ.prod_comp s (fun x => f x (σ.symm x)) hs

Premises used: Equiv.Perm.prod_comp, Equiv.symm, DFunLike.coe
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
σ : Equiv.Perm ι
s : Finset ι
f : ι → ι → M
hs : {a : ι | (σ : (a : ι) → ι) a ≠ a} ⊆ (↑s : Set ι)
x : ι
h h₁ : x = x
⊢ x = (Equiv.symm σ : (a : ι) → ι) ((σ : (a : ι) → ι) x : ι)

Tactic:
rw [Equiv.symm_apply_apply]

Premises used: Equiv.symm_apply_apply
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_3
inst : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
i : (a : ι) → a ∈ s → κ
hi : ∀ (a : ι) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : ι) (ha₁ : a₁ ∈ s) (a₂ : ι) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ b ∈ t, ∃ (a : ι) (ha : a ∈ s), i a ha = b
h : ∀ (a : ι) (ha : a ∈ s), f a = g (i a ha)
⊢ Eq.{u_3 + 1} (α := M) (∏ x ∈ s, f x) (∏ x ∈ t, g x)

Tactic:
congr_arg Multiset.prod (Multiset.map_eq_map_of_bij_of_nodup f g s.2 t.2 i hi i_inj i_surj h)

Premises used: Multiset.prod, Finset.nodup, Finset.prod, Multiset.map_eq_map_of_bij_of_nodup, congr_arg
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_3
inst : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
i : (a : ι) → a ∈ s → κ
j : (a : κ) → a ∈ t → ι
hi : ∀ (a : ι) (ha : a ∈ s), i a ha ∈ t
hj : ∀ (a : κ) (ha : a ∈ t), j a ha ∈ s
left_inv : ∀ (a : ι) (ha : a ∈ s), j (i a ha) ⋯ = a
right_inv : ∀ (a : κ) (ha : a ∈ t), i (j a ha) ⋯ = a
h : ∀ (a : ι) (ha : a ∈ s), f a = g (i a ha)
⊢ Eq.{u_3 + 1} (α := M) (∏ x ∈ s, f x) (∏ x ∈ t, g x)

Tactic:
prod_bij i hi (fun a1 h1 a2 h2 eq ↦ ?_) (fun b hb ↦ ⟨_, hj b hb, right_inv b hb⟩) h

Premises used: Exists.intro, Finset.prod_bij
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_3
inst : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
i : (a : ι) → a ∈ s → κ
j : (a : κ) → a ∈ t → ι
hi : ∀ (a : ι) (ha : a ∈ s), i a ha ∈ t
hj : ∀ (a : κ) (ha : a ∈ t), j a ha ∈ s
left_inv : ∀ (a : ι) (ha : a ∈ s), j (i a ha) ⋯ = a
right_inv : ∀ (a : κ) (ha : a ∈ t), i (j a ha) ⋯ = a
h : ∀ (a : ι) (ha : a ∈ s), f a = g (i a ha)
refine : ∀ (a1 : ι) (h1 : a1 ∈ s) (a2 : ι) (h2 : a2 ∈ s) (eq : i a1 h1 = i a2 h2), a1 = a2
⊢ Eq.{u_3 + 1} (α := M) (∏ x ∈ s, f x) (∏ x ∈ t, g x)

Tactic:
refine prod_bij i hi (fun a1 h1 a2 h2 eq ↦ ?_) (fun b hb ↦ ⟨_, hj b hb, right_inv b hb⟩) h

Premises used: Exists.intro, Finset.prod_bij
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_3
inst : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
i : (a : ι) → a ∈ s → κ
j : (a : κ) → a ∈ t → ι
hi : ∀ (a : ι) (ha : a ∈ s), i a ha ∈ t
hj : ∀ (a : κ) (ha : a ∈ t), j a ha ∈ s
left_inv : ∀ (a : ι) (ha : a ∈ s), j (i a ha) ⋯ = a
right_inv : ∀ (a : κ) (ha : a ∈ t), i (j a ha) ⋯ = a
h : ∀ (a : ι) (ha : a ∈ s), f a = g (i a ha)
a1 : ι
h1 : a1 ∈ s
a2 : ι
h2 : a2 ∈ s
eq : i a1 h1 = i a2 h2
rw : j (i a1 h1) ⋯ = j (i a2 h2) ⋯
⊢ a1 = a2

Tactic:
rw [← left_inv a1 h1, ← left_inv a2 h2]
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_3
inst : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
i : (a : ι) → a ∈ s → κ
j : (a : κ) → a ∈ t → ι
hi : ∀ (a : ι) (ha : a ∈ s), i a ha ∈ t
hj : ∀ (a : κ) (ha : a ∈ t), j a ha ∈ s
left_inv : ∀ (a : ι) (ha : a ∈ s), j (i a ha) ⋯ = a
right_inv : ∀ (a : κ) (ha : a ∈ t), i (j a ha) ⋯ = a
h : ∀ (a : ι) (ha : a ∈ s), f a = g (i a ha)
a1 : ι
h1 : a1 ∈ s
a2 : ι
h2 : a2 ∈ s
eq : i a1 h1 = i a2 h2
⊢ j (i a1 h1) ⋯ = j (i a2 h2) ⋯

Tactic:
simp only [eq]
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_3
inst : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
i : ι → κ
hi : ∀ a ∈ s, i a ∈ t
i_inj : Set.InjOn i (↑s : Set ι)
i_surj : Set.SurjOn i (↑s : Set ι) (↑t : Set κ)
h : ∀ a ∈ s, f a = g (i a)
⊢ ∀ b ∈ t, ∃ (a : ι) (ha : a ∈ s), (fun (a : ι) (x : a ∈ s) ↦ i a) a ha = b

Tactic:
simpa using i_surj
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_3
inst : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
i : ι → κ
j : κ → ι
hi : ∀ a ∈ s, i a ∈ t
hj : ∀ a ∈ t, j a ∈ s
left_inv : ∀ a ∈ s, j (i a) = a
right_inv : ∀ a ∈ t, i (j a) = a
h : ∀ a ∈ s, f a = g (i a)
⊢ Eq.{u_3 + 1} (α := M) (∏ x ∈ s, f x) (∏ x ∈ t, g x)

Tactic:
prod_bij' (fun a _ ↦ i a) (fun b _ ↦ j b) hi hj left_inv right_inv h

Premises used: Finset.prod_bij'
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_3
inst : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
e : ι ≃ κ
hst : ∀ (i : ι), i ∈ s ↔ Membership.mem (α := κ) t ((e : (a : ι) → κ) i : κ)
hfg : ∀ i ∈ s, f i = g ((e : (a : ι) → κ) i)
⊢ Eq.{u_3 + 1} (α := M) (∏ i ∈ s, f i) (∏ i ∈ t, g i)

Tactic:
prod_nbij' e e.symm ?_ ?_ ?_ ?_ hfg

Premises used: Equiv.symm, Finset.prod_nbij', DFunLike.coe
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_3
inst : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
e : ι ≃ κ
hst : ∀ (i : ι), i ∈ s ↔ Membership.mem (α := κ) t ((e : (a : ι) → κ) i : κ)
hfg : ∀ i ∈ s, f i = g ((e : (a : ι) → κ) i)
refine_1 : ∀ a ∈ s, Membership.mem (α := κ) t ((e : (a : ι) → κ) a : κ)
refine_2 : ∀ a ∈ t, Membership.mem (α := ι) s ((e.symm : (a : κ) → ι) a : ι)
refine_3 : ∀ a ∈ s, (e.symm : (a : κ) → ι) ((e : (a : ι) → κ) a : κ) = a
refine_4 : ∀ a ∈ t, (e : (a : ι) → κ) ((e.symm : (a : κ) → ι) a : ι) = a
⊢ Eq.{u_3 + 1} (α := M) (∏ i ∈ s, f i) (∏ i ∈ t, g i)

Tactic:
refine prod_nbij' e e.symm ?_ ?_ ?_ ?_ hfg

Premises used: Equiv.symm, Finset.prod_nbij', DFunLike.coe
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_3
inst : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
e : ι ≃ κ
hst : ∀ (i : ι), i ∈ s ↔ Membership.mem (α := κ) t ((e : (a : ι) → κ) i : κ)
hfg : ∀ i ∈ s, f i = g ((e : (a : ι) → κ) i)
⊢ ∀ a ∈ s, Membership.mem (α := κ) t ((e : (a : ι) → κ) a : κ)

Tactic:
simp [hst]
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_3
inst : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
e : ι ≃ κ
hst : ∀ (i : ι), i ∈ s ↔ Membership.mem (α := κ) t ((e : (a : ι) → κ) i : κ)
hfg : ∀ i ∈ s, f i = g ((e : (a : ι) → κ) i)
⊢ ∀ a ∈ t, Membership.mem (α := ι) s ((e.symm : (a : κ) → ι) a : ι)

Tactic:
simp [hst]
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_3
inst : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
e : ι ≃ κ
hst : ∀ (i : ι), i ∈ s ↔ Membership.mem (α := κ) t ((e : (a : ι) → κ) i : κ)
hfg : ∀ i ∈ s, f i = g ((e : (a : ι) → κ) i)
⊢ ∀ a ∈ s, (e.symm : (a : κ) → ι) ((e : (a : ι) → κ) a : κ) = a

Tactic:
simp [hst]
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_3
inst : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
e : ι ≃ κ
hst : ∀ (i : ι), i ∈ s ↔ Membership.mem (α := κ) t ((e : (a : ι) → κ) i : κ)
hfg : ∀ i ∈ s, f i = g ((e : (a : ι) → κ) i)
⊢ ∀ a ∈ t, (e : (a : ι) → κ) ((e.symm : (a : κ) → ι) a : ι) = a

Tactic:
simp [hst]
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_3
inst : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
e : ι → κ
he : Bijective e
hst : ∀ (i : ι), i ∈ s ↔ e i ∈ t
hfg : ∀ i ∈ s, f i = g (e i)
⊢ Eq.{u_3 + 1} (α := M) (∏ i ∈ s, f i) (∏ i ∈ t, g i)

Tactic:
prod_equiv (.ofBijective e he) hst hfg

Premises used: Finset.prod_equiv, Equiv.ofBijective
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : CommMonoid M
inst_1 : CommMonoid N
r : M → N → Prop
f : ι → M
g : ι → N
s : Finset ι
h₁ : r 1 1
h₂ : ∀ (a : ι) (b : M) (c : N), r b c → r (f a * b) (g a * c)
delta :
  r (Multiset.prod (Multiset.map (fun (x : ι) ↦ f x) s.val)) (Multiset.prod (Multiset.map (fun (x : ι) ↦ g x) s.val))
⊢ r (∏ x ∈ s, f x) (∏ x ∈ s, g x)

Tactic:
delta Finset.prod

Premises used: Finset.prod
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : CommMonoid M
inst_1 : CommMonoid N
r : M → N → Prop
f : ι → M
g : ι → N
s : Finset ι
h₁ : r 1 1
h₂ : ∀ (a : ι) (b : M) (c : N), r b c → r (f a * b) (g a * c)
h₃ : r 1 1
h₄ : ∀ ⦃a : ι⦄ ⦃b : M⦄ ⦃c : N⦄, r b c → r (f a * b) (g a * c)
⊢ r (Multiset.prod (Multiset.map (fun (x : ι) ↦ f x) s.val)) (Multiset.prod (Multiset.map (fun (x : ι) ↦ g x) s.val))

Tactic:
apply Multiset.prod_hom_rel

Premises used: Multiset.prod_hom_rel
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : CommMonoid M
inst_1 : CommMonoid N
r : M → N → Prop
f : ι → M
g : ι → N
s : Finset ι
h₁ : r 1 1
h₂ : ∀ (a : ι) (b : M) (c : N), r b c → r (f a * b) (g a * c)
⊢ r 1 1

Tactic:
assumption
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : CommMonoid M
inst_1 : CommMonoid N
r : M → N → Prop
f : ι → M
g : ι → N
s : Finset ι
h₁ : r 1 1
h₂ : ∀ (a : ι) (b : M) (c : N), r b c → r (f a * b) (g a * c)
⊢ ∀ ⦃a : ι⦄ ⦃b : M⦄ ⦃c : N⦄, r b c → r (f a * b) (g a * c)

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

Tactic:
rfl

Premises used: Finset.univ, Finset.attach, rfl
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
p : Prop
inst_1 : Decidable p
s t : Finset ι
f : ι → M
⊢ Eq.{u_3 + 1} (α := M) (∏ x ∈ if p then s else t, f x) (if p then ∏ x ∈ s, f x else ∏ x ∈ t, f x)

Tactic:
apply_ite (fun s => ∏ x ∈ s, f x) _ _ _

Premises used: apply_ite, Finset.prod
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
p : Prop
inst_1 : Decidable p
s : Finset ι
f g : ι → M
pos : ∀ (h : p), Eq.{u_3 + 1} (α := M) (∏ x ∈ s, f x) (∏ x ∈ s, f x)
neg : ∀ (h : ¬p), Eq.{u_3 + 1} (α := M) (∏ x ∈ s, g x) (∏ x ∈ s, g x)
⊢ Eq.{u_3 + 1} (α := M) (∏ x ∈ s, if p then f x else g x) (if p then ∏ x ∈ s, f x else ∏ x ∈ s, g x)

Tactic:
split_ifs with h
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
p : Prop
inst_1 : Decidable p
s : Finset ι
f g : ι → M
h : p
⊢ Eq.{u_3 + 1} (α := M) (∏ x ∈ s, f x) (∏ x ∈ s, f x)

Tactic:
rfl
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
p : Prop
inst_1 : Decidable p
s : Finset ι
f g : ι → M
h : ¬p
⊢ Eq.{u_3 + 1} (α := M) (∏ x ∈ s, g x) (∏ x ∈ s, g x)

Tactic:
rfl
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
p : Prop
inst_1 : Decidable p
s : Finset ι
f : p → ι → M
g : ¬p → ι → M
pos : ∀ (h : p), Eq.{u_3 + 1} (α := M) (∏ x ∈ s, f h x) (∏ x ∈ s, f h x)
neg : ∀ (h : ¬p), Eq.{u_3 + 1} (α := M) (∏ x ∈ s, g h x) (∏ x ∈ s, g h x)
⊢ Eq.{u_3 + 1} (α := M) (∏ x ∈ s, if h : p then f h x else g h x) (if h : p then ∏ x ∈ s, f h x else ∏ x ∈ s, g h x)

Tactic:
split_ifs with h
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
p : Prop
inst_1 : Decidable p
s : Finset ι
f : p → ι → M
g : ¬p → ι → M
h : p
⊢ Eq.{u_3 + 1} (α := M) (∏ x ∈ s, f h x) (∏ x ∈ s, f h x)

Tactic:
rfl
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
p : Prop
inst_1 : Decidable p
s : Finset ι
f : p → ι → M
g : ¬p → ι → M
h : ¬p
⊢ Eq.{u_3 + 1} (α := M) (∏ x ∈ s, g h x) (∏ x ∈ s, g h x)

Tactic:
rfl
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
p : Prop
inst_1 : Decidable p
s : Finset ι
f : ι → M
⊢ Eq.{u_3 + 1} (α := M) (if p then ∏ x ∈ s, f x else 1) (∏ x ∈ s, if p then f x else 1)

Tactic:
simp only [prod_ite_irrel, prod_const_one]

Premises used: Finset.prod_const_one, Finset.prod_ite_irrel
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
p : Prop
inst_1 : Decidable p
s : Finset ι
f : ι → M
⊢ Eq.{u_3 + 1} (α := M) (if p then 1 else ∏ x ∈ s, f x) (∏ x ∈ s, if p then 1 else f x)

Tactic:
simp only [prod_ite_irrel, prod_const_one]

Premises used: Finset.prod_const_one, Finset.prod_ite_irrel
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
M : Type u_3
s : Finset ι
f : ι → M
inst : CommMonoid M
h : Ne.{u_3 + 1} (α := M) (∏ x ∈ s, f x) 1
⊢ s.Nonempty

Tactic:
s.eq_empty_or_nonempty.elim (fun H => False.elim <| h <| H.symm ▸ prod_empty) id

Premises used: Finset.prod_empty, False.elim, Eq.rec, id, Or.elim, Eq.symm, Finset.eq_empty_or_nonempty
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
M : Type u_3
inst : CommMonoid M
f : ℕ → M
rw : Eq.{u_3 + 1} (α := M) (∏ k ∈ ∅, f k) 1
rw₁ rw₂ : Eq.{u_3 + 1} (α := M) 1 1
⊢ Eq.{u_3 + 1} (α := M) (∏ k ∈ range 0, f k) 1

Tactic:
rw [range_zero, prod_empty]

Premises used: Finset.prod_empty, Finset.range_zero
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
inst : DecidableEq ι
p : ι → Prop
inst_1 : DecidablePred p
l : List ι
⊢ ∑ x ∈ l.toFinset with p x, count x l = countP (fun (b : ι) ↦ decide (p b)) l

Tactic:
simp [Finset.sum, sum_map_count_dedup_filter_eq_countP p l]

Premises used: List.sum_map_count_dedup_filter_eq_countP, Finset.sum
-- 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 : ι)
⊢ Eq.{u_3 + 1} (α := M) (∏ x : { x : ι // x ∈ m }, f x) (∏ x ∈ m.toFinset, g x)

Tactic:
prod_bij' (fun x _ ↦ x) (fun x hx ↦ ⟨x, Multiset.mem_toFinset.1 hx⟩) ?_ ?_ ?_ ?_ ?_

Premises used: Subtype.mk, Finset.prod_bij', Iff.mp, Subtype.val, Multiset.mem_toFinset
-- 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 : ι)
refine_1 :
  ∀ (a : { x : ι // x ∈ m }) (ha : Membership.mem (γ := Finset { x : ι // x ∈ m }) univ a),
    (fun (x : { x : ι // x ∈ m }) (x_1 : Membership.mem (γ := Finset { x : ι // x ∈ m }) univ x) ↦ (↑x : ι)) a ha ∈
      m.toFinset
refine_2 :
  ∀ (a : ι) (ha : a ∈ m.toFinset),
    Membership.mem (γ := Finset { x : ι // x ∈ m }) univ
      ((fun (x : ι) (hx : x ∈ m.toFinset) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ m) x ⋯) a ha)
refine_3 :
  ∀ (a : { x : ι // x ∈ m }) (ha : Membership.mem (γ := Finset { x : ι // x ∈ m }) univ a),
    (fun (x : ι) (hx : x ∈ m.toFinset) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ m) x ⋯)
        ((fun (x : { x : ι // x ∈ m }) (x_1 : Membership.mem (γ := Finset { x : ι // x ∈ m }) univ x) ↦ (↑x : ι)) a ha)
        ⋯ =
      a
refine_4 :
  ∀ (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
refine_5 :
  ∀ (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)
⊢ Eq.{u_3 + 1} (α := M) (∏ x : { x : ι // x ∈ m }, f x) (∏ x ∈ m.toFinset, g x)

Tactic:
refine prod_bij' (fun x _ ↦ x) (fun x hx ↦ ⟨x, Multiset.mem_toFinset.1 hx⟩) ?_ ?_ ?_ ?_ ?_

Premises used: Finset.prod_bij'
-- 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),
    (fun (x : { x : ι // x ∈ m }) (x_1 : Membership.mem (γ := Finset { x : ι // x ∈ m }) univ x) ↦ (↑x : ι)) a ha ∈
      m.toFinset

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 : ι) (ha : a ∈ m.toFinset),
    Membership.mem (γ := Finset { x : ι // x ∈ m }) univ
      ((fun (x : ι) (hx : x ∈ m.toFinset) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ m) x ⋯) a ha)

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),
    (fun (x : ι) (hx : x ∈ m.toFinset) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ m) x ⋯)
        ((fun (x : { x : ι // x ∈ m }) (x_1 : Membership.mem (γ := Finset { x : ι // x ∈ m }) univ x) ↦ (↑x : ι)) a ha)
        ⋯ =
      a

Tactic:
simp [hfg]