-- Mathlib/Algebra/BigOperators/Finprod.lean
theorem finprod_prod_comm (s : Finset β) (f : α → β → M)
    (h : ∀ b ∈ s, (mulSupport fun a => f a b).Finite) :
    (∏ᶠ a : α, ∏ b ∈ s, f a b) = ∏ b ∈ s, ∏ᶠ a : α, f a b

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
s : Finset β
f : α → β → M
h : ∀ b ∈ s, (mulSupport fun a => f a b).Finite
hU : (mulSupport fun a => ∏ b ∈ s, f a b) ⊆ ↑⋯.toFinset
b : β
hb : b ∈ s
a : α
ha : a ∈ mulSupport fun x => f x b
⊢ ∃ i, ∃ (_ : i ∈ ↑s), a ∈ mulSupport fun a => f a i

Tactic:
exact ⟨b, hb, ha⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
s : Finset β
f : α → β → M
h : ∀ b ∈ s, (mulSupport fun a => f a b).Finite
hU : (mulSupport fun a => ∏ b ∈ s, f a b) ⊆ ↑⋯.toFinset
b : β
hb : b ∈ s
a : α
ha : a ∈ mulSupport fun x => f x b
⊢ a ∈ ↑⋯.toFinset

Tactic:
simp only [Finite.coe_toFinset, mem_iUnion]

Result:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
s : Finset β
f : α → β → M
h : ∀ b ∈ s, (mulSupport fun a => f a b).Finite
hU : (mulSupport fun a => ∏ b ∈ s, f a b) ⊆ ↑⋯.toFinset
b : β
hb : b ∈ s
a : α
ha : a ∈ mulSupport fun x => f x b
⊢ ∃ i, ∃ (_ : i ∈ ↑s), a ∈ mulSupport fun a => f a i

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
s : Finset β
f : α → β → M
h : ∀ b ∈ s, (mulSupport fun a => f a b).Finite
hU : (mulSupport fun a => ∏ b ∈ s, f a b) ⊆ ↑⋯.toFinset
b : β
hb : b ∈ s
⊢ (mulSupport fun x => f x b) ⊆ ↑⋯.toFinset

Tactic:
intro a ha

Result:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
s : Finset β
f : α → β → M
h : ∀ b ∈ s, (mulSupport fun a => f a b).Finite
hU : (mulSupport fun a => ∏ b ∈ s, f a b) ⊆ ↑⋯.toFinset
b : β
hb : b ∈ s
a : α
ha : a ∈ mulSupport fun x => f x b
⊢ a ∈ ↑⋯.toFinset

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
s : Finset β
f : α → β → M
h : ∀ b ∈ s, (mulSupport fun a => f a b).Finite
x : α
hx : x ∈ mulSupport fun a => ∏ b ∈ s, f a b
⊢ x ∈ ⋃ i ∈ ↑s, mulSupport fun a => f a i

Tactic:
simp only [exists_prop, mem_iUnion, Ne, mem_mulSupport, Finset.mem_coe]

Result:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
s : Finset β
f : α → β → M
h : ∀ b ∈ s, (mulSupport fun a => f a b).Finite
x : α
hx : x ∈ mulSupport fun a => ∏ b ∈ s, f a b
⊢ ∃ i ∈ s, ¬f x i = 1

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
s : Finset β
f : α → β → M
h : ∀ b ∈ s, (mulSupport fun a => f a b).Finite
x : α
hx : x ∈ mulSupport fun a => ∏ b ∈ s, f a b
⊢ ∃ i ∈ s, ¬f x i = 1

Tactic:
contrapose! hx

Result:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
s : Finset β
f : α → β → M
h : ∀ b ∈ s, (mulSupport fun a => f a b).Finite
x : α
hx : ∀ i ∈ s, f x i = 1
⊢ x ∉ mulSupport fun a => ∏ b ∈ s, f a b

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
s : Finset β
f : α → β → M
h : ∀ b ∈ s, (mulSupport fun a => f a b).Finite
⊢ (mulSupport fun a => ∏ b ∈ s, f a b) ⊆ ↑⋯.toFinset

Tactic:
rw [Finite.coe_toFinset]

Result:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
s : Finset β
f : α → β → M
h : ∀ b ∈ s, (mulSupport fun a => f a b).Finite
⊢ (mulSupport fun a => ∏ b ∈ s, f a b) ⊆ ⋃ i ∈ ↑s, mulSupport fun a => f a i

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
s : Finset β
f : α → β → M
h : ∀ b ∈ s, (mulSupport fun a => f a b).Finite
x : α
hx : ∀ i ∈ s, f x i = 1
⊢ x ∉ mulSupport fun a => ∏ b ∈ s, f a b

Tactic:
rw [mem_mulSupport, not_not, Finset.prod_congr rfl hx, Finset.prod_const_one]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
s : Finset β
f : α → β → M
h : ∀ b ∈ s, (mulSupport fun a => f a b).Finite
⊢ (mulSupport fun a => ∏ b ∈ s, f a b) ⊆ ⋃ i ∈ ↑s, mulSupport fun a => f a i

Tactic:
intro x hx

Result:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
s : Finset β
f : α → β → M
h : ∀ b ∈ s, (mulSupport fun a => f a b).Finite
x : α
hx : x ∈ mulSupport fun a => ∏ b ∈ s, f a b
⊢ x ∈ ⋃ i ∈ ↑s, mulSupport fun a => f a i

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
s : Finset β
f : α → β → M
h : ∀ b ∈ s, (mulSupport fun a => f a b).Finite
⊢ ∏ᶠ (a : α), ∏ b ∈ s, f a b = ∏ b ∈ s, ∏ᶠ (a : α), f a b

Tactic:
have hU :
  (mulSupport fun a => ∏ b ∈ s, f a b) ⊆
    (s.finite_toSet.biUnion fun b hb => h b (Finset.mem_coe.1 hb)).toFinset := by
  rw [Finite.coe_toFinset]
  intro x hx
  simp only [exists_prop, mem_iUnion, Ne, mem_mulSupport, Finset.mem_coe]
  contrapose! hx
  rw [mem_mulSupport, not_not, Finset.prod_congr rfl hx, Finset.prod_const_one]

Result:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
s : Finset β
f : α → β → M
h : ∀ b ∈ s, (mulSupport fun a => f a b).Finite
hU : (mulSupport fun a => ∏ b ∈ s, f a b) ⊆ ↑⋯.toFinset
⊢ ∏ᶠ (a : α), ∏ b ∈ s, f a b = ∏ b ∈ s, ∏ᶠ (a : α), f a b

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
s : Finset β
f : α → β → M
h : ∀ b ∈ s, (mulSupport fun a => f a b).Finite
hU : (mulSupport fun a => ∏ b ∈ s, f a b) ⊆ ↑⋯.toFinset
⊢ ∏ y ∈ s, ∏ x ∈ ⋯.toFinset, f x y = ∏ b ∈ s, ∏ᶠ (a : α), f a b

Tactic:
refine Finset.prod_congr rfl fun b hb => (finprod_eq_prod_of_mulSupport_subset _ ?_).symm

Result:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
s : Finset β
f : α → β → M
h : ∀ b ∈ s, (mulSupport fun a => f a b).Finite
hU : (mulSupport fun a => ∏ b ∈ s, f a b) ⊆ ↑⋯.toFinset
b : β
hb : b ∈ s
⊢ (mulSupport fun x => f x b) ⊆ ↑⋯.toFinset

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
s : Finset β
f : α → β → M
h : ∀ b ∈ s, (mulSupport fun a => f a b).Finite
hU : (mulSupport fun a => ∏ b ∈ s, f a b) ⊆ ↑⋯.toFinset
⊢ ∏ᶠ (a : α), ∏ b ∈ s, f a b = ∏ b ∈ s, ∏ᶠ (a : α), f a b

Tactic:
rw [finprod_eq_prod_of_mulSupport_subset _ hU, Finset.prod_comm]

Result:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
s : Finset β
f : α → β → M
h : ∀ b ∈ s, (mulSupport fun a => f a b).Finite
hU : (mulSupport fun a => ∏ b ∈ s, f a b) ⊆ ↑⋯.toFinset
⊢ ∏ y ∈ s, ∏ x ∈ ⋯.toFinset, f x y = ∏ b ∈ s, ∏ᶠ (a : α), f a b