awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
a : α
s : Set α
h : a ∉ s → f a = 1
refine : ∀ (x : α) (hx : x ∈ mulSupport f), x ∈ insert a s → x ∈ s
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ insert a s), f i) (∏ᶠ (i : α) (_ : i ∈ s), f i)

Tactic:
refine finprod_mem_inter_mulSupport_eq' _ _ _ fun x hx => ⟨?_, Or.inr⟩

Premises used: finprod_mem_inter_mulSupport_eq', Iff.intro, Or.inr
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s : Set α
x : α
hx : x ∈ mulSupport f
h : x ∉ s → f x = 1
⊢ x ∈ s

Tactic:
not_imp_comm.1 h hx

Premises used: not_imp_comm, Iff.mp
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
a : α
s : Set α
h : a ∉ s → f a = 1
x : α
hx : x ∈ mulSupport f
hxs : x ∈ s
⊢ x ∈ s

Tactic:
hxs
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s : Set α
x : α
hx : x ∈ mulSupport f
h : x ∉ s → f x = 1
⊢ x ∈ s

Tactic:
exacts [not_imp_comm.1 h hx, hxs]

Premises used: not_imp_comm, Iff.mp
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
a : α
s : Set α
h : f a = 1
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ insert a s), f i) (∏ᶠ (i : α) (_ : i ∈ s), f i)

Tactic:
finprod_mem_insert_of_eq_one_if_notMem fun _ => h

Premises used: finprod_mem_insert_of_eq_one_if_notMem
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
N : Type u_6
inst : CommMonoid N
f : α → N
a : α
hf : HasFiniteMulSupport f
pos : ∀ (ha : a ∈ mulSupport f), f a ∣ finprod f
neg : ∀ (ha : a ∉ mulSupport f), f a ∣ finprod f
⊢ f a ∣ finprod f

Tactic:
by_cases ha : a ∈ mulSupport f

Premises used: Function.mulSupport
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
N : Type u_6
inst : CommMonoid N
f : α → N
a : α
hf : HasFiniteMulSupport f
ha : a ∈ mulSupport f
pos : f a ∣ ∏ i ∈ Finite.toFinset (s := mulSupport f) hf, f i
⊢ f a ∣ finprod f

Tactic:
rw [finprod_eq_prod_of_mulSupport_toFinset_subset f hf (Set.Subset.refl _)]

Premises used: Set.Subset.refl, finprod_eq_prod_of_mulSupport_toFinset_subset
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
N : Type u_6
inst : CommMonoid N
f : α → N
a : α
hf : HasFiniteMulSupport f
ha : a ∈ mulSupport f
⊢ f a ∣ ∏ i ∈ Finite.toFinset (s := mulSupport f) hf, f i

Tactic:
Finset.dvd_prod_of_mem f ((Finite.mem_toFinset hf).mpr ha)

Premises used: Iff.mpr, Finset.dvd_prod_of_mem, Set.Finite.mem_toFinset
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
N : Type u_6
inst : CommMonoid N
f : α → N
a : α
hf : HasFiniteMulSupport f
ha : a ∈ mulSupport f
⊢ f a ∣ ∏ i ∈ Finite.toFinset (s := mulSupport f) hf, f i

Tactic:
exact Finset.dvd_prod_of_mem f ((Finite.mem_toFinset hf).mpr ha)

Premises used: Iff.mpr, Finset.dvd_prod_of_mem, Set.Finite.mem_toFinset
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
N : Type u_6
inst : CommMonoid N
f : α → N
a : α
hf : HasFiniteMulSupport f
ha : a ∉ mulSupport f
neg : 1 ∣ finprod f
⊢ f a ∣ finprod f

Tactic:
rw [notMem_mulSupport.mp ha]

Premises used: Iff.mp, Function.notMem_mulSupport
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
N : Type u_6
inst : CommMonoid N
f : α → N
a : α
hf : HasFiniteMulSupport f
ha : a ∉ mulSupport f
⊢ 1 ∣ finprod f

Tactic:
one_dvd (finprod f)

Premises used: finprod, one_dvd
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
N : Type u_6
inst : CommMonoid N
f : α → N
a : α
hf : HasFiniteMulSupport f
ha : a ∉ mulSupport f
⊢ 1 ∣ finprod f

Tactic:
exact one_dvd (finprod f)

Premises used: finprod, one_dvd
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
a b : α
h : a ≠ b
h₁ : a ∉ {b}
hs : Set.Finite (α := α) {b}
⊢ ∏ᶠ (i : α) (_ : Membership.mem (γ := Set α) {a, b} i), f i = f a * f b

Tactic:
rw [finprod_mem_insert, finprod_mem_singleton]

Premises used: finprod_mem_insert, finprod_mem_singleton
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
a b : α
h : a ≠ b
⊢ a ∉ {b}

Tactic:
h

Premises used: Set.Mem, setOf, Set.singleton
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
a b : α
h : a ≠ b
⊢ Set.Finite (α := α) {b}

Tactic:
finite_singleton b

Premises used: Set.finite_singleton
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
a b : α
h : a ≠ b
⊢ a ∉ {b}

Tactic:
exacts [h, finite_singleton b]

Premises used: Set.finite_singleton
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
f : α → M
s : Set β
g : β → α
hg : InjOn g (s ∩ mulSupport (f ∘ g))
pos :
  ∀ (hs : (s ∩ mulSupport (f ∘ g)).Finite),
    Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ g '' s), f i) (∏ᶠ (j : β) (_ : j ∈ s), f (g j))
neg :
  ∀ (hs : ¬(s ∩ mulSupport (f ∘ g)).Finite),
    Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ g '' s), f i) (∏ᶠ (j : β) (_ : j ∈ s), f (g j))
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ g '' s), f i) (∏ᶠ (j : β) (_ : j ∈ s), f (g j))

Tactic:
by_cases hs : (s ∩ mulSupport (f ∘ g)).Finite

Premises used: Set.Finite, Function.comp, Inter.inter, Function.mulSupport
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
f : α → M
s : Set β
g : β → α
hg : InjOn g (s ∩ mulSupport (f ∘ g))
hs : (s ∩ mulSupport (f ∘ g)).Finite
⊢ ∀ x ∈ hs.toFinset (s := s ∩ mulSupport (f ∘ g)), ∀ y ∈ hs.toFinset (s := s ∩ mulSupport (f ∘ g)), g x = g y → x = y

Tactic:
simpa only [hs.mem_toFinset]

Premises used: Set.Finite.mem_toFinset
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
f : α → M
s : Set β
g : β → α
hg : InjOn g (s ∩ mulSupport (f ∘ g))
hs : (s ∩ mulSupport (f ∘ g)).Finite
⊢ ∀ x ∈ hs.toFinset (s := s ∩ mulSupport (f ∘ g)), ∀ y ∈ hs.toFinset (s := s ∩ mulSupport (f ∘ g)), g x = g y → x = y

Tactic:
have hg : ∀ x ∈ hs.toFinset, ∀ y ∈ hs.toFinset, g x = g y → x = y := by
        simpa only [hs.mem_toFinset]
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
f : α → M
s : Set β
g : β → α
hg_1 : InjOn g (s ∩ mulSupport (f ∘ g))
hs : (s ∩ mulSupport (f ∘ g)).Finite
hg : ∀ x ∈ hs.toFinset (s := s ∩ mulSupport (f ∘ g)), ∀ y ∈ hs.toFinset (s := s ∩ mulSupport (f ∘ g)), g x = g y → x = y
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : β) (_ : i ∈ s), (f ∘ g) i) (∏ i ∈ hs.toFinset (s := s ∩ mulSupport (f ∘ g)), (f ∘ g) i)

Tactic:
have := finprod_mem_eq_prod (comp f g) hs
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
f : α → M
s : Set β
g : β → α
hg_1 : InjOn g (s ∩ mulSupport (f ∘ g))
hs : (s ∩ mulSupport (f ∘ g)).Finite
hg : ∀ x ∈ hs.toFinset (s := s ∩ mulSupport (f ∘ g)), ∀ y ∈ hs.toFinset (s := s ∩ mulSupport (f ∘ g)), g x = g y → x = y
this :
  Eq.{u_5 + 1} (α := M) (∏ᶠ (i : β) (_ : i ∈ s), f (g i))
    (∏ i ∈ hs.toFinset (s := s ∩ mulSupport.{u_2, u_5} (M := M) fun (x : β) ↦ f (g x)), f (g i))
pos :
  Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ g '' s), f i)
    (∏ x ∈ Finset.image g (hs.toFinset (s := s ∩ mulSupport (f ∘ g))), f x)
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ g '' s), f i) (∏ᶠ (j : β) (_ : j ∈ s), f (g j))

Tactic:
rw [this, ← Finset.prod_image hg]

Premises used: Finset.prod_image
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
f : α → M
s : Set β
g : β → α
hg_1 : InjOn g (s ∩ mulSupport (f ∘ g))
hs : (s ∩ mulSupport (f ∘ g)).Finite
hg : ∀ x ∈ hs.toFinset (s := s ∩ mulSupport (f ∘ g)), ∀ y ∈ hs.toFinset (s := s ∩ mulSupport (f ∘ g)), g x = g y → x = y
this :
  Eq.{u_5 + 1} (α := M) (∏ᶠ (i : β) (_ : i ∈ s), f (g i))
    (∏ i ∈ hs.toFinset (s := s ∩ mulSupport.{u_2, u_5} (M := M) fun (x : β) ↦ f (g x)), f (g i))
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ g '' s), f i)
    (∏ x ∈ Finset.image g (hs.toFinset (s := s ∩ mulSupport (f ∘ g))), f x)

Tactic:
finprod_mem_eq_prod_of_inter_mulSupport_eq f ?_

Premises used: finprod_mem_eq_prod_of_inter_mulSupport_eq
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
f : α → M
s : Set β
g : β → α
hg_1 : InjOn g (s ∩ mulSupport (f ∘ g))
hs : (s ∩ mulSupport (f ∘ g)).Finite
hg : ∀ x ∈ hs.toFinset (s := s ∩ mulSupport (f ∘ g)), ∀ y ∈ hs.toFinset (s := s ∩ mulSupport (f ∘ g)), g x = g y → x = y
this :
  Eq.{u_5 + 1} (α := M) (∏ᶠ (i : β) (_ : i ∈ s), f (g i))
    (∏ i ∈ hs.toFinset (s := s ∩ mulSupport.{u_2, u_5} (M := M) fun (x : β) ↦ f (g x)), f (g i))
pos : g '' s ∩ mulSupport f = (↑(Finset.image g (hs.toFinset (s := s ∩ mulSupport (f ∘ g)))) : Set α) ∩ mulSupport f
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ g '' s), f i)
    (∏ x ∈ Finset.image g (hs.toFinset (s := s ∩ mulSupport (f ∘ g))), f x)

Tactic:
refine finprod_mem_eq_prod_of_inter_mulSupport_eq f ?_

Premises used: finprod_mem_eq_prod_of_inter_mulSupport_eq
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
f : α → M
s : Set β
g : β → α
hg_1 : InjOn g (s ∩ mulSupport (f ∘ g))
hs : (s ∩ mulSupport (f ∘ g)).Finite
hg : ∀ x ∈ hs.toFinset (s := s ∩ mulSupport (f ∘ g)), ∀ y ∈ hs.toFinset (s := s ∩ mulSupport (f ∘ g)), g x = g y → x = y
this :
  Eq.{u_5 + 1} (α := M) (∏ᶠ (i : β) (_ : i ∈ s), f (g i))
    (∏ i ∈ hs.toFinset (s := s ∩ mulSupport.{u_2, u_5} (M := M) fun (x : β) ↦ f (g x)), f (g i))
pos : g '' s ∩ mulSupport f = g '' (↑(hs.toFinset (s := s ∩ mulSupport (f ∘ g))) : Set β) ∩ mulSupport f
pos₁ : g '' s ∩ mulSupport f = g '' (s ∩ mulSupport (f ∘ g)) ∩ mulSupport f
pos₂ : g '' s ∩ mulSupport f = g '' s ∩ mulSupport f ∩ mulSupport f
pos₃ : g '' s ∩ mulSupport f = g '' s ∩ (mulSupport f ∩ mulSupport f)
pos₄ pos₅ : g '' s ∩ mulSupport f = g '' s ∩ mulSupport f
⊢ g '' s ∩ mulSupport f = (↑(Finset.image g (hs.toFinset (s := s ∩ mulSupport (f ∘ g)))) : Set α) ∩ mulSupport f

Tactic:
rw [Finset.coe_image, hs.coe_toFinset, ← image_inter_mulSupport_eq, inter_assoc, inter_self]

Premises used: Set.inter_self, Finset.coe_image, Set.Finite.coe_toFinset, Set.image_inter_mulSupport_eq, Set.inter_assoc
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
f : α → M
s : Set β
g : β → α
hg : InjOn g (s ∩ mulSupport (f ∘ g))
hs : ¬(s ∩ mulSupport.{u_2, u_5} (M := M) fun (x : β) ↦ f (g x)).Finite
neg : (g '' s ∩ mulSupport f).Infinite
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ g '' s), f i) (∏ᶠ (j : β) (_ : j ∈ s), f (g j))

Tactic:
rw [finprod_mem_eq_one_of_infinite hs, finprod_mem_eq_one_of_infinite]

Premises used: finprod_mem_eq_one_of_infinite
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
f : α → M
s : Set β
g : β → α
hg : InjOn g (s ∩ mulSupport (f ∘ g))
hs : ¬(s ∩ mulSupport.{u_2, u_5} (M := M) fun (x : β) ↦ f (g x)).Finite
neg : (g '' (s ∩ mulSupport (f ∘ g))).Infinite
neg₁ neg₂ neg₃ neg₄ : (s ∩ mulSupport (f ∘ g)).Infinite
⊢ (g '' s ∩ mulSupport f).Infinite

Tactic:
rwa [image_inter_mulSupport_eq, infinite_image_iff hg]

Premises used: Set.infinite_image_iff, Set.image_inter_mulSupport_eq
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
f : α → M
s : Set β
g : β → α
hg : InjOn g (s ∩ mulSupport (f ∘ g))
pos :
  ∀ (hs : (s ∩ mulSupport (f ∘ g)).Finite),
    Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ g '' s), f i) (∏ᶠ (j : β) (_ : j ∈ s), f (g j))
neg neg₁ :
  ∀ (hs : ¬(s ∩ mulSupport (f ∘ g)).Finite),
    Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ g '' s), f i) (∏ᶠ (j : β) (_ : j ∈ s), f (g j))
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ g '' s), f i) (∏ᶠ (j : β) (_ : j ∈ s), f (g j))

Tactic:
classical
    by_cases hs : (s ∩ mulSupport (f ∘ g)).Finite
    · have hg : ∀ x ∈ hs.toFinset, ∀ y ∈ hs.toFinset, g x = g y → x = y := by
        simpa only [hs.mem_toFinset]
      have := finprod_mem_eq_prod (comp f g) hs
      unfold Function.comp at this
      rw [this, ← Finset.prod_image hg]
      refine finprod_mem_eq_prod_of_inter_mulSupport_eq f ?_
      rw [Finset.coe_image, hs.coe_toFinset, ← image_inter_mulSupport_eq, inter_assoc, inter_self]
    · unfold Function.comp at hs
      rw [finprod_mem_eq_one_of_infinite hs, finprod_mem_eq_one_of_infinite]
      rwa [image_inter_mulSupport_eq, infinite_image_iff hg]

Premises used: Set.inter_self, Set.Finite, Function.comp, Finset.coe_image, Inter.inter, finprod_mem_eq_prod_of_inter_mulSupport_eq, finprod_mem_eq_one_of_infinite, Function.mulSupport, Set.infinite_image_iff, Set.image_inter_mulSupport_eq, Set.inter_assoc, Finset.prod_image
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
f : α → M
s : Set β
g : β → α
hg : InjOn g s
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ g '' s), f i) (∏ᶠ (j : β) (_ : j ∈ s), f (g j))

Tactic:
finprod_mem_image' <| hg.mono inter_subset_left

Premises used: Set.inter_subset_left, Set.InjOn.mono, finprod_mem_image'
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
f : α → M
g : β → α
hg : InjOn g (mulSupport (f ∘ g))
rw : InjOn g (univ ∩ mulSupport (f ∘ g))
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ range g), f i) (∏ᶠ (j : β), f (g j))

Tactic:
rw [← image_univ, finprod_mem_image', finprod_mem_univ]

Premises used: Set.image_univ, finprod_mem_image', finprod_mem_univ
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
f : α → M
g : β → α
hg rwa rwa₁ rwa₂ rwa₃ : InjOn g (mulSupport (f ∘ g))
⊢ InjOn g (univ ∩ mulSupport (f ∘ g))

Tactic:
rwa [univ_inter]

Premises used: Set.univ_inter
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
f : α → M
g : β → α
hg : Injective g
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ range g), f i) (∏ᶠ (j : β), f (g j))

Tactic:
finprod_mem_range' hg.injOn

Premises used: Function.Injective.injOn, finprod_mem_range'
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
s : Set α
t : Set β
f : α → M
g : β → M
e : α → β
he₀ : BijOn e s t
he₁ : ∀ x ∈ s, f x = g (e x)
rw : Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ s), f i) (∏ᶠ (j : α) (_ : j ∈ s), g (e j))
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ s), f i) (∏ᶠ (j : β) (_ : j ∈ t), g j)

Tactic:
rw [← Set.BijOn.image_eq he₀, finprod_mem_image he₀.2.1]

Premises used: Set.BijOn.image_eq, And.right, And.left, finprod_mem_image
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
s : Set α
t : Set β
f : α → M
g : β → M
e : α → β
he₀ : BijOn e s t
he₁ : ∀ x ∈ s, f x = g (e x)
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ s), f i) (∏ᶠ (j : α) (_ : j ∈ s), g (e j))

Tactic:
finprod_mem_congr rfl he₁

Premises used: finprod_mem_congr, rfl
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
s : Set α
t : Set β
f : α → M
g : β → M
e : α → β
he₀ : BijOn e s t
he₁ : ∀ x ∈ s, f x = g (e x)
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ s), f i) (∏ᶠ (j : α) (_ : j ∈ s), g (e j))

Tactic:
exact finprod_mem_congr rfl he₁

Premises used: finprod_mem_congr, rfl
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
f : α → M
g : β → M
e : α → β
he₀ : Bijective e
he₁ : ∀ (x : α), f x = g (e x)
rw :
  Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : Membership.mem (γ := Set α) univ i), f i)
    (∏ᶠ (i : β) (_ : Membership.mem (γ := Set β) univ i), g i)
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α), f i) (∏ᶠ (j : β), g j)

Tactic:
rw [← finprod_mem_univ f, ← finprod_mem_univ g]

Premises used: finprod_mem_univ
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
f : α → M
g : β → M
e : α → β
he₀ : Bijective e
he₁ : ∀ (x : α), f x = g (e x)
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : Membership.mem (γ := Set α) univ i), f i)
    (∏ᶠ (i : β) (_ : Membership.mem (γ := Set β) univ i), g i)

Tactic:
finprod_mem_eq_of_bijOn _ he₀.bijOn_univ fun x _ => he₁ x

Premises used: Function.Bijective.bijOn_univ, finprod_mem_eq_of_bijOn
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
f : α → M
g : β → M
e : α → β
he₀ : Bijective e
he₁ : ∀ (x : α), f x = g (e x)
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : Membership.mem (γ := Set α) univ i), f i)
    (∏ᶠ (i : β) (_ : Membership.mem (γ := Set β) univ i), g i)

Tactic:
exact finprod_mem_eq_of_bijOn _ he₀.bijOn_univ fun x _ => he₁ x

Premises used: Function.Bijective.bijOn_univ, finprod_mem_eq_of_bijOn
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
g : β → M
e : α → β
he₀ : Bijective e
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α), g (e i)) (∏ᶠ (j : β), g j)

Tactic:
finprod_eq_of_bijective e he₀ fun _ => rfl

Premises used: finprod_eq_of_bijective, rfl
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
e : α ≃ β
f : β → M
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α), f ((e : (a : α) → β) i)) (∏ᶠ (i' : β), f i')

Tactic:
finprod_comp e e.bijective

Premises used: Equiv.bijective, finprod_comp, DFunLike.coe
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s : Set α
rw : Injective.{u_1 + 1, u_1 + 1} (α := (↑s : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (j : (↑s : Type u_1)), f (↑j : α)) (∏ᶠ (i : α) (_ : i ∈ s), f i)

Tactic:
rw [← finprod_mem_range, Subtype.range_coe]

Premises used: finprod_mem_range, Subtype.range_coe
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s : Set α
⊢ Injective.{u_1 + 1, u_1 + 1} (α := (↑s : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ s))

Tactic:
Subtype.coe_injective

Premises used: Subtype.coe_injective
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s : Set α
⊢ Injective.{u_1 + 1, u_1 + 1} (α := (↑s : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ s))

Tactic:
exact Subtype.coe_injective

Premises used: Subtype.coe_injective
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
p : α → Prop
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (j : Subtype p), f (↑j : α)) (∏ᶠ (i : α) (_ : p i), f i)

Tactic:
finprod_set_coe_eq_finprod_mem { i | p i }

Premises used: Set.Mem, finprod_set_coe_eq_finprod_mem, setOf
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s t : Set α
h : (s ∩ mulSupport f).Finite
hst : Disjoint (s ∩ t) (s \ t)
hs : (s ∩ t ∩ mulSupport f).Finite
ht : (s \ t ∩ mulSupport f).Finite
⊢ HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∩ t), f i) (∏ᶠ (i : α) (_ : i ∈ s \ t), f i) = ∏ᶠ (i : α) (_ : i ∈ s), f i

Tactic:
rw [← finprod_mem_union', inter_union_diff]

Premises used: finprod_mem_union', Set.inter_union_diff
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s t : Set α
h : (s ∩ mulSupport f).Finite
hst : s ∩ t ⊓ s \ t ≤ ⊥
⊢ Disjoint (s ∩ t) (s \ t)

Tactic:
rw [disjoint_iff_inf_le]

Premises used: disjoint_iff_inf_le
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s t : Set α
h : (s ∩ mulSupport f).Finite
⊢ s ∩ t ⊓ s \ t ≤ ⊥

Tactic:
fun x hx => hx.2.2 hx.1.2

Premises used: Set.Mem, Set.Subset, And.right, And.left
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s t : Set α
h : (s ∩ mulSupport f).Finite
⊢ s ∩ t ⊓ s \ t ≤ ⊥

Tactic:
exact fun x hx => hx.2.2 hx.1.2
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s t : Set α
h : (s ∩ mulSupport f).Finite
⊢ (s ∩ t ∩ mulSupport f).Finite

Tactic:
h.subset fun x hx => ⟨hx.1.1, hx.2⟩

Premises used: Set.Finite.subset, And.right, And.left, And.intro
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s t : Set α
h : (s ∩ mulSupport f).Finite
⊢ (s \ t ∩ mulSupport f).Finite

Tactic:
h.subset fun x hx => ⟨hx.1.1, hx.2⟩

Premises used: Set.Finite.subset, And.right, And.left, And.intro
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s t : Set α
h : (s ∩ mulSupport f).Finite
⊢ (s ∩ t ∩ mulSupport f).Finite

Tactic:
exacts [h.subset fun x hx => ⟨hx.1.1, hx.2⟩, h.subset fun x hx => ⟨hx.1.1, hx.2⟩]

Premises used: Set.Finite.subset, And.intro
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s t : Set α
h : s.Finite
⊢ HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∩ t), f i) (∏ᶠ (i : α) (_ : i ∈ s \ t), f i) = ∏ᶠ (i : α) (_ : i ∈ s), f i

Tactic:
finprod_mem_inter_mul_diff' _ <| h.inter_of_left _

Premises used: Set.Finite.inter_of_left, finprod_mem_inter_mul_diff'
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s t : Set α
hst : s ⊆ t
ht : (t ∩ mulSupport f).Finite
rw :
  HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s), f i) (∏ᶠ (i : α) (_ : i ∈ t \ s), f i) =
    HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ t ∩ s), f i) (∏ᶠ (i : α) (_ : i ∈ t \ s), f i)
rw₁ : Set α
rw₂ rw₃ :
  HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s), f i) (∏ᶠ (i : α) (_ : i ∈ t \ s), f i) =
    HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s), f i) (∏ᶠ (i : α) (_ : i ∈ t \ s), f i)
⊢ HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s), f i) (∏ᶠ (i : α) (_ : i ∈ t \ s), f i) = ∏ᶠ (i : α) (_ : i ∈ t), f i

Tactic:
rw [← finprod_mem_inter_mul_diff' _ ht, inter_eq_self_of_subset_right hst]

Premises used: finprod_mem_inter_mul_diff', Set.inter_eq_self_of_subset_right
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s t : Set α
hst : s ⊆ t
ht : t.Finite
⊢ HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s), f i) (∏ᶠ (i : α) (_ : i ∈ t \ s), f i) = ∏ᶠ (i : α) (_ : i ∈ t), f i

Tactic:
finprod_mem_mul_diff' hst (ht.inter_of_left _)

Premises used: Set.Finite.inter_of_left, finprod_mem_mul_diff'
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
ι : Type u_3
M : Type u_5
inst : CommMonoid M
f : α → M
inst_1 : Finite ι
t : ι → Set α
h : Pairwise (Disjoint on t)
ht : ∀ (i : ι), (t i).Finite
intro :
  ∀ (val : Fintype ι),
    Eq.{u_5 + 1} (α := M) (∏ᶠ (a : α) (_ : Membership.mem (γ := Set α) (⋃ (i : ι), t i) a), f a)
      (∏ᶠ (i : ι) (a : α) (_ : a ∈ t i), f a)
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (a : α) (_ : Membership.mem (γ := Set α) (⋃ (i : ι), t i) a), f a)
    (∏ᶠ (i : ι) (a : α) (_ : a ∈ t i), f a)

Tactic:
cases nonempty_fintype ι

Premises used: nonempty_fintype
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
ι : Type u_3
M : Type u_5
inst : CommMonoid M
f : α → M
inst_1 : Finite ι
t : ι → Set α
h : Pairwise (Disjoint on t)
ht : ∀ (i : ι), (t i).Finite
val : Fintype ι
⊢ ∀ (i : ι), (t i).Finite

Tactic:
ht