awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ι
intro :
  ∀ (t : (i : ι) → Finset α)
    (h : Pairwise.{u_3} (α := ι) (onFun.{u_3 + 1, u_1 + 1, 1} (β := Set α) Disjoint fun (i : ι) ↦ (↑(t i) : Set α))),
    Eq.{u_5 + 1} (α := M)
      (∏ᶠ (a : α) (_ : Membership.mem (γ := Set α) (⋃ (i : ι), (fun (i : ι) ↦ (↑(t i) : Set α)) i) a), f a)
      (∏ᶠ (i : ι) (a : α) (_ : Membership.mem (γ := Set α) ((fun (i : ι) ↦ (↑(t i) : Set α)) i) a), 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:
lift t to ι → Finset α using ht
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
ι : Type u_3
M : Type u_5
inst : CommMonoid M
f : α → M
inst_1 : Finite ι
val : Fintype ι
t : (i : ι) → Finset α
h : Pairwise.{u_3} (α := ι) (onFun.{u_3 + 1, u_1 + 1, 1} (β := Set α) Disjoint fun (i : ι) ↦ (↑(t i) : Set α))
intro :
  Eq.{u_5 + 1} (α := M) (∏ x : ι, ∏ i ∈ t x, f i)
    (∏ᶠ (i : ι) (a : α) (_ : Membership.mem (γ := Set α) ((fun (i : ι) ↦ (↑(t i) : Set α)) i) a), f a)
intro₁ : (↑Finset.univ : Set ι).PairwiseDisjoint t
⊢ Eq.{u_5 + 1} (α := M)
    (∏ᶠ (a : α) (_ : Membership.mem (γ := Set α) (⋃ (i : ι), (fun (i : ι) ↦ (↑(t i) : Set α)) i) a), f a)
    (∏ᶠ (i : ι) (a : α) (_ : Membership.mem (γ := Set α) ((fun (i : ι) ↦ (↑(t i) : Set α)) i) a), f a)

Tactic:
rw [← biUnion_univ, ← Finset.coe_univ, ← Finset.coe_biUnion, finprod_mem_coe_finset,
      Finset.prod_biUnion]

Premises used: Finset.coe_biUnion, Finset.coe_univ, Finset.prod_biUnion, Set.biUnion_univ, finprod_mem_coe_finset
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
ι : Type u_3
M : Type u_5
inst : CommMonoid M
f : α → M
inst_1 : Finite ι
val : Fintype ι
t : (i : ι) → Finset α
h : Pairwise.{u_3} (α := ι) (onFun.{u_3 + 1, u_1 + 1, 1} (β := Set α) Disjoint fun (i : ι) ↦ (↑(t i) : Set α))
⊢ Eq.{u_5 + 1} (α := M) (∏ x : ι, ∏ i ∈ t x, f i)
    (∏ᶠ (i : ι) (a : α) (_ : Membership.mem (γ := Set α) ((fun (i : ι) ↦ (↑(t i) : Set α)) i) a), f a)

Tactic:
simp only [finprod_mem_coe_finset, finprod_eq_prod_of_fintype]

Premises used: finprod_eq_prod_of_fintype, finprod_mem_coe_finset
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
ι : Type u_3
M : Type u_5
inst : CommMonoid M
f : α → M
inst_1 : Finite ι
val : Fintype ι
t : (i : ι) → Finset α
h : Pairwise.{u_3} (α := ι) (onFun.{u_3 + 1, u_1 + 1, 1} (β := Set α) Disjoint fun (i : ι) ↦ (↑(t i) : Set α))
⊢ (↑Finset.univ : Set ι).PairwiseDisjoint t

Tactic:
fun x _ y _ hxy => Finset.disjoint_coe.1 (h hxy)

Premises used: Finset.disjoint_coe, Set.PairwiseDisjoint, Set.Pairwise, Iff.mp
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
ι : Type u_3
M : Type u_5
inst : CommMonoid M
f : α → M
inst_1 : Finite ι
val : Fintype ι
t : (i : ι) → Finset α
h : Pairwise.{u_3} (α := ι) (onFun.{u_3 + 1, u_1 + 1, 1} (β := Set α) Disjoint fun (i : ι) ↦ (↑(t i) : Set α))
⊢ (↑Finset.univ : Set ι).PairwiseDisjoint t

Tactic:
exact fun x _ y _ hxy => Finset.disjoint_coe.1 (h hxy)

Premises used: Finset.disjoint_coe, Iff.mp
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
ι : Type u_3
M : Type u_5
inst : CommMonoid M
f : α → M
inst_1 : Finite ι
val : Fintype ι
t : (i : ι) → Finset α
h : Pairwise.{u_3} (α := ι) (onFun.{u_3 + 1, u_1 + 1, 1} (β := Set α) Disjoint fun (i : ι) ↦ (↑(t i) : Set α))
intro :
  Eq.{u_5 + 1} (α := M)
    (∏ᶠ (a : α) (_ :
      Membership.mem (γ := Set α) (⋃ (x : ι), ⋃ (_ : Membership.mem (γ := Set ι) univ x), (↑(t x) : Set α)) a), f a)
    (∏ᶠ (i : ι) (a : α) (_ : Membership.mem (γ := Set α) ((fun (i : ι) ↦ (↑(t i) : Set α)) i) a), f a)
intro₁ :
  Eq.{u_5 + 1} (α := M)
    (∏ᶠ (a : α) (_ : Membership.mem (γ := Set α) (⋃ x ∈ (↑Finset.univ : Set ι), (↑(t x) : Set α)) a), f a)
    (∏ᶠ (i : ι) (a : α) (_ : Membership.mem (γ := Set α) ((fun (i : ι) ↦ (↑(t i) : Set α)) i) a), f a)
intro₂ :
  Eq.{u_5 + 1} (α := M) (∏ᶠ (a : α) (_ : a ∈ (↑(Finset.biUnion Finset.univ t) : Set α)), f a)
    (∏ᶠ (i : ι) (a : α) (_ : Membership.mem (γ := Set α) ((fun (i : ι) ↦ (↑(t i) : Set α)) i) a), f a)
intro₃ :
  Eq.{u_5 + 1} (α := M) (∏ i ∈ Finset.biUnion Finset.univ t, f i)
    (∏ᶠ (i : ι) (a : α) (_ : Membership.mem (γ := Set α) ((fun (i : ι) ↦ (↑(t i) : Set α)) i) a), f a)
intro₄ :
  Eq.{u_5 + 1} (α := M) (∏ x : ι, ∏ i ∈ t x, f i)
    (∏ᶠ (i : ι) (a : α) (_ : Membership.mem (γ := Set α) ((fun (i : ι) ↦ (↑(t i) : Set α)) i) a), f a)
intro₅ : (↑Finset.univ : Set ι).PairwiseDisjoint t
intro₆ :
  Eq.{u_5 + 1} (α := M) (∏ x : ι, ∏ i ∈ t x, f i)
    (∏ᶠ (i : ι) (a : α) (_ : Membership.mem (γ := Set α) ((fun (i : ι) ↦ (↑(t i) : Set α)) i) a), f a)
intro₇ : (↑Finset.univ : Set ι).PairwiseDisjoint t
intro₈ :
  Eq.{u_5 + 1} (α := M) (∏ x : ι, ∏ i ∈ t x, f i)
    (∏ᶠ (i : ι) (a : α) (_ : Membership.mem (γ := Set α) ((fun (i : ι) ↦ (↑(t i) : Set α)) i) a), f a)
intro₉ intro₁₀ : (↑Finset.univ : Set ι).PairwiseDisjoint t
⊢ Eq.{u_5 + 1} (α := M)
    (∏ᶠ (a : α) (_ : Membership.mem (γ := Set α) (⋃ (i : ι), (fun (i : ι) ↦ (↑(t i) : Set α)) i) a), f a)
    (∏ᶠ (i : ι) (a : α) (_ : Membership.mem (γ := Set α) ((fun (i : ι) ↦ (↑(t i) : Set α)) i) a), f a)

Tactic:
classical
    rw [← biUnion_univ, ← Finset.coe_univ, ← Finset.coe_biUnion, finprod_mem_coe_finset,
      Finset.prod_biUnion]
    · simp only [finprod_mem_coe_finset, finprod_eq_prod_of_fintype]
    · exact fun x _ y _ hxy => Finset.disjoint_coe.1 (h hxy)

Premises used: Finset.coe_biUnion, Finset.disjoint_coe, Finset.coe_univ, Finset.prod_biUnion, Set.biUnion_univ, finprod_eq_prod_of_fintype, finprod_mem_coe_finset, Iff.mp
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
ι : Type u_3
M : Type u_5
inst : CommMonoid M
f : α → M
I : Set ι
t : ι → Set α
h : I.PairwiseDisjoint t
hI : I.Finite
ht : ∀ i ∈ I, (t i).Finite
haveI :
  ∀ (this : Fintype (↑I : Type u_3)),
    Eq.{u_5 + 1} (α := M) (∏ᶠ (a : α) (_ : Membership.mem (γ := Set α) (⋃ x ∈ I, t x) a), f a)
      (∏ᶠ (i : ι) (_ : i ∈ I) (j : α) (_ : j ∈ t i), f j)
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (a : α) (_ : Membership.mem (γ := Set α) (⋃ x ∈ I, t x) a), f a)
    (∏ᶠ (i : ι) (_ : i ∈ I) (j : α) (_ : j ∈ t i), f j)

Tactic:
haveI := hI.fintype
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
ι : Type u_3
M : Type u_5
inst : CommMonoid M
f : α → M
I : Set ι
t : ι → Set α
h : I.PairwiseDisjoint t
hI : I.Finite
ht : ∀ i ∈ I, (t i).Finite
this : Fintype (↑I : Type u_3)
h₁ :
  Pairwise.{u_3} (α := (↑I : Type u_3))
    (onFun.{u_3 + 1, u_1 + 1, 1} (β := Set α) Disjoint fun (x : (↑I : Type u_3)) ↦ t (↑x : ι))
ht₁ : ∀ (i : (↑I : Type u_3)), (t (↑i : ι)).Finite
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (a : α) (_ : Membership.mem (γ := Set α) (⋃ x ∈ I, t x) a), f a)
    (∏ᶠ (i : ι) (_ : i ∈ I) (j : α) (_ : j ∈ t i), f j)

Tactic:
rw [biUnion_eq_iUnion, finprod_mem_iUnion, ← finprod_set_coe_eq_finprod_mem]

Premises used: finprod_set_coe_eq_finprod_mem, Set.biUnion_eq_iUnion, finprod_mem_iUnion
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
ι : Type u_3
M : Type u_5
inst : CommMonoid M
f : α → M
I : Set ι
t : ι → Set α
h : I.PairwiseDisjoint t
hI : I.Finite
ht : ∀ i ∈ I, (t i).Finite
this : Fintype (↑I : Type u_3)
⊢ Pairwise.{u_3} (α := (↑I : Type u_3))
    (onFun.{u_3 + 1, u_1 + 1, 1} (β := Set α) Disjoint fun (x : (↑I : Type u_3)) ↦ t (↑x : ι))

Tactic:
fun x y hxy => h x.2 y.2 (Subtype.coe_injective.ne hxy)

Premises used: Function.Injective.ne, Subtype.coe_injective, Pairwise, Subtype.property
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
ι : Type u_3
M : Type u_5
inst : CommMonoid M
f : α → M
I : Set ι
t : ι → Set α
h : I.PairwiseDisjoint t
hI : I.Finite
ht : ∀ i ∈ I, (t i).Finite
this : Fintype (↑I : Type u_3)
⊢ ∀ (i : (↑I : Type u_3)), (t (↑i : ι)).Finite

Tactic:
fun b => ht b b.2

Premises used: Subtype.val, Subtype.property
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
ι : Type u_3
M : Type u_5
inst : CommMonoid M
f : α → M
I : Set ι
t : ι → Set α
h : I.PairwiseDisjoint t
hI : I.Finite
ht : ∀ i ∈ I, (t i).Finite
this : Fintype (↑I : Type u_3)
⊢ Pairwise.{u_3} (α := (↑I : Type u_3))
    (onFun.{u_3 + 1, u_1 + 1, 1} (β := Set α) Disjoint fun (x : (↑I : Type u_3)) ↦ t (↑x : ι))

Tactic:
exacts [fun x y hxy => h x.2 y.2 (Subtype.coe_injective.ne hxy), fun b => ht b b.2]

Premises used: Function.Injective.ne, Subtype.coe_injective
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
t : Set (Set α)
h : t.PairwiseDisjoint id
ht₀ : t.Finite
ht₁ : ∀ x ∈ t, x.Finite
rw :
  Eq.{u_5 + 1} (α := M) (∏ᶠ (a : α) (_ : Membership.mem (γ := Set α) (⋃ i ∈ t, i) a), f a)
    (∏ᶠ (s : Set α) (_ : s ∈ t) (a : α) (_ : a ∈ s), f a)
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (a : α) (_ : a ∈ ⋃₀ t), f a) (∏ᶠ (s : Set α) (_ : s ∈ t) (a : α) (_ : a ∈ s), f a)

Tactic:
rw [Set.sUnion_eq_biUnion]

Premises used: Set.sUnion_eq_biUnion
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
t : Set (Set α)
h : t.PairwiseDisjoint id
ht₀ : t.Finite
ht₁ : ∀ x ∈ t, x.Finite
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (a : α) (_ : Membership.mem (γ := Set α) (⋃ i ∈ t, i) a), f a)
    (∏ᶠ (s : Set α) (_ : s ∈ t) (a : α) (_ : a ∈ s), f a)

Tactic:
finprod_mem_biUnion h ht₀ ht₁

Premises used: finprod_mem_biUnion
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
t : Set (Set α)
h : t.PairwiseDisjoint id
ht₀ : t.Finite
ht₁ : ∀ x ∈ t, x.Finite
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (a : α) (_ : Membership.mem (γ := Set α) (⋃ i ∈ t, i) a), f a)
    (∏ᶠ (s : Set α) (_ : s ∈ t) (a : α) (_ : a ∈ s), f a)

Tactic:
exact finprod_mem_biUnion h ht₀ ht₁

Premises used: finprod_mem_biUnion
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : Option α → M
hf : HasFiniteMulSupport (f ∘ some)
⊢ (mulSupport f).Finite

Tactic:
simpa [finite_option]

Premises used: Set.finite_option
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : Option α → M
hf : HasFiniteMulSupport (f ∘ some)
⊢ (mulSupport f).Finite

Tactic:
replace hf : (mulSupport f).Finite := by simpa [finite_option]
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : Option α → M
hf : (mulSupport f).Finite
⊢ none ∉ range some

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : Option α → M
hf : (mulSupport f).Finite
h : ∀ (x : Option α), f x = ∏ᶠ (_ : Membership.mem (γ := Set (Option α)) (insert none (range some)) x), f x
h₁ :
  Eq.{u_5 + 1} (α := M) (∏ᶠ (a : α), f (some a))
    (∏ᶠ (i : Option α) (_ : Membership.mem (γ := Set (Option α)) (range some) i), f i)
⊢ ∏ᶠ (o : Option α), f o = f none * ∏ᶠ (a : α), f (some a)

Tactic:
convert!
    finprod_mem_insert' f (show none ∉ Set.range Option.some by simp) (hf.subset inter_subset_right)

Premises used: Set.Finite.subset, finprod_mem_insert', Set.inter_subset_right
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : Option α → M
hf : (mulSupport f).Finite
x : Option α
⊢ f x = ∏ᶠ (_ : Membership.mem (γ := Set (Option α)) (insert none (range some)) x), f x

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : Option α → M
hf : (mulSupport f).Finite
h : Injective.{u_1 + 1, u_1 + 1} (α := α) some
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (a : α), f (some a))
    (∏ᶠ (i : Option α) (_ : Membership.mem (γ := Set (Option α)) (range some) i), f i)

Tactic:
rw [finprod_mem_range]

Premises used: finprod_mem_range
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : Option α → M
hf : (mulSupport f).Finite
⊢ Injective.{u_1 + 1, u_1 + 1} (α := α) some

Tactic:
Option.some_injective _

Premises used: Option.some_injective
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : Option α → M
hf : (mulSupport f).Finite
⊢ Injective.{u_1 + 1, u_1 + 1} (α := α) some

Tactic:
exact Option.some_injective _

Premises used: Option.some_injective
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : Set α → M
s : Set α
a : α
hs : s.Finite
has : a ∉ s
rw :
  ∏ᶠ (t : Set α) (_ : t ∈ 𝒫 s ∪ insert a '' 𝒫 s), f t =
    HMul.hMul (α := M) (∏ᶠ (t : Set α) (_ : t ∈ 𝒫 s), f t) (∏ᶠ (t : Set α) (_ : t ∈ 𝒫 s), f (insert a t))
rw₁ :
  HMul.hMul (α := M) (∏ᶠ (i : Set α) (_ : i ∈ 𝒫 s), f i) (∏ᶠ (i : Set α) (_ : i ∈ insert a '' 𝒫 s), f i) =
    HMul.hMul (α := M) (∏ᶠ (t : Set α) (_ : t ∈ 𝒫 s), f t) (∏ᶠ (t : Set α) (_ : t ∈ 𝒫 s), f (insert a t))
rw₂ rw₃ :
  HMul.hMul (α := M) (∏ᶠ (i : Set α) (_ : i ∈ 𝒫 s), f i) (∏ᶠ (j : Set α) (_ : j ∈ 𝒫 s), f (insert a j)) =
    HMul.hMul (α := M) (∏ᶠ (t : Set α) (_ : t ∈ 𝒫 s), f t) (∏ᶠ (t : Set α) (_ : t ∈ 𝒫 s), f (insert a t))
⊢ ∏ᶠ (t : Set α) (_ : t ∈ 𝒫 insert a s), f t =
    HMul.hMul (α := M) (∏ᶠ (t : Set α) (_ : t ∈ 𝒫 s), f t) (∏ᶠ (t : Set α) (_ : t ∈ 𝒫 s), f (insert a t))

Tactic:
rw [Set.powerset_insert,
    finprod_mem_union (disjoint_powerset_insert has) hs.powerset (hs.powerset.image (insert a)),
    finprod_mem_image (powerset_insert_injOn has)]

Premises used: Set.Finite.powerset, finprod_mem_union, Set.powerset_insert, Set.disjoint_powerset_insert, Set.powerset_insert_injOn, Insert.insert, Set.Finite.image, finprod_mem_image
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : Set α → M
s : Set α
a : α
hs : s.Finite
has : a ∈ s
nth_rw :
  ∏ᶠ (t : Set α) (_ : t ∈ 𝒫 insert a (s \ {a})), f t =
    HMul.hMul (α := M) (∏ᶠ (t : Set α) (_ : t ∈ 𝒫 (s \ {a})), f t)
      (∏ᶠ (t : Set α) (_ : t ∈ 𝒫 (s \ {a})), f (insert a t))
⊢ ∏ᶠ (t : Set α) (_ : t ∈ 𝒫 s), f t =
    HMul.hMul (α := M) (∏ᶠ (t : Set α) (_ : t ∈ 𝒫 (s \ {a})), f t)
      (∏ᶠ (t : Set α) (_ : t ∈ 𝒫 (s \ {a})), f (insert a t))

Tactic:
nth_rw 1 2 [← Set.insert_diff_self_of_mem has]

Premises used: Set.insert_diff_self_of_mem
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : Set α → M
s : Set α
a : α
hs : s.Finite
has : a ∈ s
⊢ ∏ᶠ (t : Set α) (_ : t ∈ 𝒫 insert a (s \ {a})), f t =
    HMul.hMul (α := M) (∏ᶠ (t : Set α) (_ : t ∈ 𝒫 (s \ {a})), f t)
      (∏ᶠ (t : Set α) (_ : t ∈ 𝒫 (s \ {a})), f (insert a t))

Tactic:
finprod_mem_powerset_insert (hs.subset Set.diff_subset)
    (notMem_diff_of_mem (Set.mem_singleton a))

Premises used: Set.mem_singleton, Set.diff_subset, Set.notMem_diff_of_mem, finprod_mem_powerset_insert, Set.Finite.subset
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : Set α → M
s : Set α
a : α
hs : s.Finite
has : a ∈ s
⊢ ∏ᶠ (t : Set α) (_ : t ∈ 𝒫 insert a (s \ {a})), f t =
    HMul.hMul (α := M) (∏ᶠ (t : Set α) (_ : t ∈ 𝒫 (s \ {a})), f t)
      (∏ᶠ (t : Set α) (_ : t ∈ 𝒫 (s \ {a})), f (insert a t))

Tactic:
exact finprod_mem_powerset_insert (hs.subset Set.diff_subset)
    (notMem_diff_of_mem (Set.mem_singleton a))

Premises used: Set.mem_singleton, Set.diff_subset, Set.notMem_diff_of_mem, finprod_mem_powerset_insert, Set.Finite.subset
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
a : α
hf : HasFiniteMulSupport f
rw : f a * ∏ᶠ (i : α) (_ : i ≠ a), f i = ∏ i ∈ Finite.toFinset (s := mulSupport f) hf, f i
⊢ f a * ∏ᶠ (i : α) (_ : i ≠ a), f i = ∏ᶠ (i : α), f i

Tactic:
rw [finprod_eq_prod _ hf]

Premises used: finprod_eq_prod
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
a : α
hf : HasFiniteMulSupport f
x : α
hx : f x ≠ 1
rw : x ≠ a ↔ f x ≠ 1 ∧ ¬x = a
⊢ x ≠ a ↔ x ∈ Finite.toFinset (s := mulSupport f) hf \ {a}

Tactic:
rw [Finset.mem_sdiff, Finset.mem_singleton, Finite.mem_toFinset, mem_mulSupport]

Premises used: Finset.mem_singleton, Set.Finite.mem_toFinset, Function.mem_mulSupport, Finset.mem_sdiff
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
a : α
hf : HasFiniteMulSupport f
x : α
hx : f x ≠ 1
⊢ x ≠ a ↔ f x ≠ 1 ∧ ¬x = a

Tactic:
grind
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
a : α
hf : HasFiniteMulSupport f
⊢ ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ Finite.toFinset (s := mulSupport f) hf \ {a})

Tactic:
have h : ∀ x : α, f x ≠ 1 → (x ≠ a ↔ x ∈ hf.toFinset \ {a}) := by
      intro x hx
      rw [Finset.mem_sdiff, Finset.mem_singleton, Finite.mem_toFinset, mem_mulSupport]
      grind
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
a : α
hf : HasFiniteMulSupport f
h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ Finite.toFinset (s := mulSupport f) hf \ {a})
rw :
  f a * ∏ i ∈ (Finite.toFinset (s := mulSupport f) hf).erase a, f i = ∏ i ∈ Finite.toFinset (s := mulSupport f) hf, f i
⊢ f a * ∏ᶠ (i : α) (_ : i ≠ a), f i = ∏ i ∈ Finite.toFinset (s := mulSupport f) hf, f i

Tactic:
rw [finprod_cond_eq_prod_of_cond_iff f (fun hx => h _ hx), Finset.sdiff_singleton_eq_erase]

Premises used: Finset.sdiff_singleton_eq_erase, finprod_cond_eq_prod_of_cond_iff
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
a : α
hf : HasFiniteMulSupport f
h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ Finite.toFinset (s := mulSupport f) hf \ {a})
pos :
  ∀ (ha : a ∈ mulSupport f),
    f a * ∏ i ∈ (Finite.toFinset (s := mulSupport f) hf).erase a, f i =
      ∏ i ∈ Finite.toFinset (s := mulSupport f) hf, f i
neg :
  ∀ (ha : a ∉ mulSupport f),
    f a * ∏ i ∈ (Finite.toFinset (s := mulSupport f) hf).erase a, f i =
      ∏ i ∈ Finite.toFinset (s := mulSupport f) hf, f i
⊢ f a * ∏ i ∈ (Finite.toFinset (s := mulSupport f) hf).erase a, f i = ∏ i ∈ Finite.toFinset (s := mulSupport f) hf, f i

Tactic:
by_cases ha : a ∈ mulSupport f

Premises used: Function.mulSupport
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
a : α
hf : HasFiniteMulSupport f
h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ Finite.toFinset (s := mulSupport f) hf \ {a})
ha : a ∈ mulSupport f
⊢ f a * ∏ i ∈ (Finite.toFinset (s := mulSupport f) hf).erase a, f i = ∏ i ∈ Finite.toFinset (s := mulSupport f) hf, f i

Tactic:
apply Finset.mul_prod_erase _ _ ((Finite.mem_toFinset _).mpr ha)

Premises used: Iff.mpr, Set.Finite.mem_toFinset, Finset.mul_prod_erase
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
a : α
hf : HasFiniteMulSupport f
h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ Finite.toFinset (s := mulSupport f) hf \ {a})
ha : a ∉ mulSupport f
⊢ f a = 1

Tactic:
rw [mem_mulSupport, not_not] at ha

Premises used: Classical.not_not, Function.mem_mulSupport
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
a : α
hf : HasFiniteMulSupport f
h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ Finite.toFinset (s := mulSupport f) hf \ {a})
ha : f a = 1
neg :
  Eq.{u_5 + 1} (α := M) (∏ i ∈ (Finite.toFinset (s := mulSupport f) hf).erase a, f i)
    (∏ i ∈ Finite.toFinset (s := mulSupport f) hf, f i)
⊢ f a * ∏ i ∈ (Finite.toFinset (s := mulSupport f) hf).erase a, f i = ∏ i ∈ Finite.toFinset (s := mulSupport f) hf, f i

Tactic:
rw [ha, one_mul]

Premises used: one_mul
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
a : α
hf : HasFiniteMulSupport f
h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ Finite.toFinset (s := mulSupport f) hf \ {a})
ha : f a = 1
⊢ Eq.{u_5 + 1} (α := M) (∏ i ∈ (Finite.toFinset (s := mulSupport f) hf).erase a, f i)
    (∏ i ∈ Finite.toFinset (s := mulSupport f) hf, f i)

Tactic:
apply Finset.prod_erase _ ha

Premises used: Finset.prod_erase
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
a : α
hf : HasFiniteMulSupport f
rw rw₁ rw₂ : f a * ∏ᶠ (i : α) (_ : i ≠ a), f i = ∏ i ∈ Finite.toFinset (s := mulSupport f) hf, f i
rw₃ :
  ∀ (h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ Finite.toFinset (s := mulSupport f) hf \ {a})),
    f a * ∏ᶠ (i : α) (_ : i ≠ a), f i = ∏ i ∈ Finite.toFinset (s := mulSupport f) hf, f i
rw₄ :
  ∀ (h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ Finite.toFinset (s := mulSupport f) hf \ {a})),
    f a * ∏ i ∈ (Finite.toFinset (s := mulSupport f) hf).erase a, f i =
      ∏ i ∈ Finite.toFinset (s := mulSupport f) hf, f i
pos :
  ∀ (h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ Finite.toFinset (s := mulSupport f) hf \ {a})) (ha : a ∈ mulSupport f),
    f a * ∏ i ∈ (Finite.toFinset (s := mulSupport f) hf).erase a, f i =
      ∏ i ∈ Finite.toFinset (s := mulSupport f) hf, f i
neg neg₁ :
  ∀ (h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ Finite.toFinset (s := mulSupport f) hf \ {a})) (ha : a ∉ mulSupport f),
    f a * ∏ i ∈ (Finite.toFinset (s := mulSupport f) hf).erase a, f i =
      ∏ i ∈ Finite.toFinset (s := mulSupport f) hf, f i
⊢ f a * ∏ᶠ (i : α) (_ : i ≠ a), f i = ∏ᶠ (i : α), f i

Tactic:
classical
    rw [finprod_eq_prod _ hf]
    have h : ∀ x : α, f x ≠ 1 → (x ≠ a ↔ x ∈ hf.toFinset \ {a}) := by
      intro x hx
      rw [Finset.mem_sdiff, Finset.mem_singleton, Finite.mem_toFinset, mem_mulSupport]
      grind
    rw [finprod_cond_eq_prod_of_cond_iff f (fun hx => h _ hx), Finset.sdiff_singleton_eq_erase]
    by_cases ha : a ∈ mulSupport f
    · apply Finset.mul_prod_erase _ _ ((Finite.mem_toFinset _).mpr ha)
    · rw [mem_mulSupport, not_not] at ha
      rw [ha, one_mul]
      apply Finset.prod_erase _ ha

Premises used: Finset.sdiff_singleton_eq_erase, Classical.not_not, Function.mem_mulSupport, Function.mulSupport, one_mul, finprod_eq_prod
-- 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
hs : s.Finite
ht : t.Finite
⊢ s.Finite

Tactic:
hs
-- 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
hs : s.Finite
ht : t.Finite
lift :
  ∀ (s : Finset α),
    Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ (↑s : Set α)) (j : β) (_ : j ∈ t), f i j)
      (∏ᶠ (j : β) (_ : j ∈ t) (i : α) (_ : i ∈ (↑s : Set α)), f i j)
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ s) (j : β) (_ : j ∈ t), f i j)
    (∏ᶠ (j : β) (_ : j ∈ t) (i : α) (_ : i ∈ s), f i j)

Tactic:
lift s to Finset α using hs

Premises used: Finset
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
t : Set β
f : α → β → M
ht : t.Finite
s : Finset α
⊢ t.Finite

Tactic:
ht
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
t : Set β
f : α → β → M
ht : t.Finite
s : Finset α
lift :
  ∀ (t : Finset β),
    Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ (↑s : Set α)) (j : β) (_ : j ∈ (↑t : Set β)), f i j)
      (∏ᶠ (j : β) (_ : j ∈ (↑t : Set β)) (i : α) (_ : i ∈ (↑s : Set α)), f i j)
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ (↑s : Set α)) (j : β) (_ : j ∈ t), f i j)
    (∏ᶠ (j : β) (_ : j ∈ t) (i : α) (_ : i ∈ (↑s : Set α)), f i j)

Tactic:
lift t to Finset β using ht

Premises used: Finset
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
f : α → β → M
s : Finset α
t : Finset β
simp : Eq.{u_5 + 1} (α := M) (∏ i ∈ s, ∏ i_1 ∈ t, f i i_1) (∏ i ∈ t, ∏ i_1 ∈ s, f i_1 i)
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ (↑s : Set α)) (j : β) (_ : j ∈ (↑t : Set β)), f i j)
    (∏ᶠ (j : β) (_ : j ∈ (↑t : Set β)) (i : α) (_ : i ∈ (↑s : Set α)), f i j)

Tactic:
simp only [finprod_mem_coe_finset]

Premises used: finprod_mem_coe_finset
-- Module: Mathlib.Algebra.BigOperators.Finprod
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
f : α → β → M
s : Finset α
t : Finset β
⊢ Eq.{u_5 + 1} (α := M) (∏ i ∈ s, ∏ i_1 ∈ t, f i i_1) (∏ i ∈ t, ∏ i_1 ∈ s, f i_1 i)

Tactic:
Finset.prod_comm

Premises used: Finset.prod_comm