awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
a : α
s : Set α
f : α → M
h : a ∉ s
hs : (s ∩ mulSupport f).Finite
⊢ ∏ᶠ (i : α) (_ : i ∈ insert a s), f i = f a * ∏ᶠ (i : α) (_ : i ∈ s), f i
have rw : Disjoint {a} s
Tactic: rw [insert_eq, finprod_mem_union' _ _ hs, finprod_mem_singleton]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
a : α
s : Set α
f : α → M
h : a ∉ s
hs : (s ∩ mulSupport f).Finite
rw : Disjoint {a} s
⊢ ∏ᶠ (i : α) (_ : i ∈ insert a s), f i = f a * ∏ᶠ (i : α) (_ : i ∈ s), f i
have rw₁ : ({a} ∩ mulSupport f).Finite
Tactic: rw [insert_eq, finprod_mem_union' _ _ hs, finprod_mem_singleton]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
a : α
s : Set α
h : a ∉ s → f a = 1
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ insert a s), f i) (∏ᶠ (i : α) (_ : i ∈ s), f i)
have refine : ∀ (x : α) (hx : x ∈ mulSupport f), x ∈ insert a s → x ∈ s
Tactic: refine finprod_mem_inter_mulSupport_eq' _ _ _ fun x hx => ⟨?_, Or.inr⟩
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
N : Type u_6
inst : CommMonoid N
f : α → N
a : α
hf : HasFiniteMulSupport f
⊢ f a ∣ finprod f
have pos : ∀ (ha : a ∈ mulSupport f), f a ∣ finprod f
Tactic: by_cases ha : a ∈ mulSupport f
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
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
⊢ f a ∣ finprod f
have neg : ∀ (ha : a ∉ mulSupport f), f a ∣ finprod f
Tactic: by_cases ha : a ∈ mulSupport f
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
N : Type u_6
inst : CommMonoid N
f : α → N
a : α
hf : HasFiniteMulSupport f
ha : a ∈ mulSupport f
⊢ f a ∣ finprod f
have pos : f a ∣ ∏ i ∈ Finite.toFinset (s := mulSupport f) hf, f i
Tactic: rw [finprod_eq_prod_of_mulSupport_toFinset_subset f hf (Set.Subset.refl _)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
N : Type u_6
inst : CommMonoid N
f : α → N
a : α
hf : HasFiniteMulSupport f
ha : a ∉ mulSupport f
⊢ f a ∣ finprod f
have neg : 1 ∣ finprod f
Tactic: rw [notMem_mulSupport.mp ha]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
a b : α
h : a ≠ b
⊢ ∏ᶠ (i : α) (_ : Membership.mem (γ := Set α) {a, b} i), f i = f a * f b
have h₁ : a ∉ {b}
Tactic: rw [finprod_mem_insert, finprod_mem_singleton]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
a b : α
h : a ≠ b
h₁ : a ∉ {b}
⊢ ∏ᶠ (i : α) (_ : Membership.mem (γ := Set α) {a, b} i), f i = f a * f b
have hs : Set.Finite (α := α) {b}
Tactic: rw [finprod_mem_insert, finprod_mem_singleton]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
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))
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ g '' s), f i) (∏ᶠ (j : β) (_ : j ∈ s), f (g j))
have pos : ∀ (hs : (s ∩ mulSupport (f ∘ g)).Finite),
  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
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
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))
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ g '' s), f i) (∏ᶠ (j : β) (_ : j ∈ s), f (g j))
have neg : ∀ (hs : ¬(s ∩ mulSupport (f ∘ g)).Finite),
  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
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (hypothesis)
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
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ g '' s), f i) (∏ᶠ (j : β) (_ : j ∈ s), f (g j))
have hg₁ : ∀ 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]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (hypothesis)
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 ∈ g '' s), f i) (∏ᶠ (j : β) (_ : j ∈ s), f (g j))
have this : 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
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
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) (∏ᶠ (j : β) (_ : j ∈ s), f (g j))
have 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)
Tactic: rw [this, ← Finset.prod_image hg]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
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)
have pos : g '' s ∩ mulSupport f = (↑(Finset.image g (hs.toFinset (s := s ∩ mulSupport (f ∘ g)))) : Set α) ∩ mulSupport f
Tactic: refine finprod_mem_eq_prod_of_inter_mulSupport_eq f ?_
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
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))
⊢ g '' s ∩ mulSupport f = (↑(Finset.image g (hs.toFinset (s := s ∩ mulSupport (f ∘ g)))) : Set α) ∩ mulSupport f
have pos : g '' s ∩ mulSupport f = 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]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
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
⊢ g '' s ∩ mulSupport f = (↑(Finset.image g (hs.toFinset (s := s ∩ mulSupport (f ∘ g)))) : Set α) ∩ mulSupport f
have pos₁ : g '' s ∩ mulSupport f = g '' (s ∩ mulSupport (f ∘ g)) ∩ mulSupport f
Tactic: rw [Finset.coe_image, hs.coe_toFinset, ← image_inter_mulSupport_eq, inter_assoc, inter_self]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
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
⊢ g '' s ∩ mulSupport f = (↑(Finset.image g (hs.toFinset (s := s ∩ mulSupport (f ∘ g)))) : Set α) ∩ mulSupport f
have pos₂ : g '' s ∩ mulSupport f = g '' s ∩ mulSupport f ∩ mulSupport f
Tactic: rw [Finset.coe_image, hs.coe_toFinset, ← image_inter_mulSupport_eq, inter_assoc, inter_self]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
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
⊢ g '' s ∩ mulSupport f = (↑(Finset.image g (hs.toFinset (s := s ∩ mulSupport (f ∘ g)))) : Set α) ∩ mulSupport f
have pos₃ : g '' s ∩ mulSupport f = g '' s ∩ (mulSupport f ∩ mulSupport f)
Tactic: rw [Finset.coe_image, hs.coe_toFinset, ← image_inter_mulSupport_eq, inter_assoc, inter_self]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
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)
⊢ g '' s ∩ mulSupport f = (↑(Finset.image g (hs.toFinset (s := s ∩ mulSupport (f ∘ g)))) : Set α) ∩ mulSupport f
have pos₄ : g '' s ∩ mulSupport f = g '' s ∩ mulSupport f
Tactic: rw [Finset.coe_image, hs.coe_toFinset, ← image_inter_mulSupport_eq, inter_assoc, inter_self]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
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
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ g '' s), f i) (∏ᶠ (j : β) (_ : j ∈ s), f (g j))
have neg : (g '' s ∩ mulSupport f).Infinite
Tactic: rw [finprod_mem_eq_one_of_infinite hs, finprod_mem_eq_one_of_infinite]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
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
⊢ (g '' s ∩ mulSupport f).Infinite
have neg : (g '' (s ∩ mulSupport (f ∘ g))).Infinite
Tactic: rwa [image_inter_mulSupport_eq, infinite_image_iff hg]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
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
⊢ (g '' s ∩ mulSupport f).Infinite
have neg₁ : (s ∩ mulSupport (f ∘ g)).Infinite
Tactic: rwa [image_inter_mulSupport_eq, infinite_image_iff hg]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
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))
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ g '' s), f i) (∏ᶠ (j : β) (_ : j ∈ s), f (g j))
have pos : ∀ (hs : (s ∩ mulSupport (f ∘ g)).Finite),
  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]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
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))
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ g '' s), f i) (∏ᶠ (j : β) (_ : j ∈ s), f (g j))
have neg : ∀ (hs : ¬(s ∩ mulSupport (f ∘ g)).Finite),
  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]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
f : α → M
g : β → α
hg : InjOn g (mulSupport (f ∘ g))
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ range g), f i) (∏ᶠ (j : β), f (g j))
have rw : InjOn g (univ ∩ mulSupport (f ∘ g))
Tactic: rw [← image_univ, finprod_mem_image', finprod_mem_univ]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
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 ∈ t), g j)
have rw : Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : i ∈ s), f i) (∏ᶠ (j : α) (_ : j ∈ s), g (e j))
Tactic: rw [← Set.BijOn.image_eq he₀, finprod_mem_image he₀.2.1]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
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 : α), f i) (∏ᶠ (j : β), g j)
have rw : Eq.{u_5 + 1} (α := M) (∏ᶠ (i : α) (_ : Membership.mem (γ := Set α) univ i), f i)
  (∏ᶠ (i : β) (_ : Membership.mem (γ := Set β) univ i), g i)
Tactic: rw [← finprod_mem_univ f, ← finprod_mem_univ g]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s : Set α
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (j : (↑s : Type u_1)), f (↑j : α)) (∏ᶠ (i : α) (_ : i ∈ s), f i)
have rw : Injective.{u_1 + 1, u_1 + 1} (α := (↑s : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
Tactic: rw [← finprod_mem_range, Subtype.range_coe]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s t : Set α
h : (s ∩ mulSupport f).Finite
⊢ HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∩ t), f i) (∏ᶠ (i : α) (_ : i ∈ s \ t), f i) = ∏ᶠ (i : α) (_ : i ∈ s), f i
have hst : Disjoint (s ∩ t) (s \ t)
Tactic: rw [← finprod_mem_union', inter_union_diff]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
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)
⊢ HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∩ t), f i) (∏ᶠ (i : α) (_ : i ∈ s \ t), f i) = ∏ᶠ (i : α) (_ : i ∈ s), f i
have hs : (s ∩ t ∩ mulSupport f).Finite
Tactic: rw [← finprod_mem_union', inter_union_diff]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
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
⊢ HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s ∩ t), f i) (∏ᶠ (i : α) (_ : i ∈ s \ t), f i) = ∏ᶠ (i : α) (_ : i ∈ s), f i
have ht : (s \ t ∩ mulSupport f).Finite
Tactic: rw [← finprod_mem_union', inter_union_diff]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s t : Set α
h : (s ∩ mulSupport f).Finite
⊢ Disjoint (s ∩ t) (s \ t)
have hst : s ∩ t ⊓ s \ t ≤ ⊥
Tactic: rw [disjoint_iff_inf_le]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
f : α → M
s t : Set α
hst : s ⊆ t
ht : (t ∩ mulSupport f).Finite
⊢ HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s), f i) (∏ᶠ (i : α) (_ : i ∈ t \ s), f i) = ∏ᶠ (i : α) (_ : i ∈ t), f i
have 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)
Tactic: rw [← finprod_mem_inter_mul_diff' _ ht, inter_eq_self_of_subset_right hst]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
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 α
⊢ HMul.hMul (α := M) (∏ᶠ (i : α) (_ : i ∈ s), f i) (∏ᶠ (i : α) (_ : i ∈ t \ s), f i) = ∏ᶠ (i : α) (_ : i ∈ t), f i
have 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)
Tactic: rw [← finprod_mem_inter_mul_diff' _ ht, inter_eq_self_of_subset_right hst]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
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
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (a : α) (_ : Membership.mem (γ := Set α) (⋃ (i : ι), t i) a), f a)
    (∏ᶠ (i : ι) (a : α) (_ : a ∈ t i), f a)
have 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)
Tactic: cases nonempty_fintype ι
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
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 ι
⊢ Eq.{u_5 + 1} (α := M) (∏ᶠ (a : α) (_ : Membership.mem (γ := Set α) (⋃ (i : ι), t i) a), f a)
    (∏ᶠ (i : ι) (a : α) (_ : a ∈ t i), f a)
have 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)
Tactic: lift t to ι → Finset α using ht
Cleared hypotheses: t, h, ht
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
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)
    (∏ᶠ (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)
have 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)
Tactic: rw [← biUnion_univ, ← Finset.coe_univ, ← Finset.coe_biUnion, finprod_mem_coe_finset,
      Finset.prod_biUnion]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
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)
⊢ 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)
have intro₁ : (↑Finset.univ : Set ι).PairwiseDisjoint t
Tactic: rw [← biUnion_univ, ← Finset.coe_univ, ← Finset.coe_biUnion, finprod_mem_coe_finset,
      Finset.prod_biUnion]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finprod (goal)
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)
    (∏ᶠ (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)
have 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)
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)