α : Type u_2
β : Type u_1
ι : Type ?u.386315
G : Type ?u.386318
M : Type u_3
N : Type ?u.386324
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a b : α
s✝ t : Set α
s : Finset β
f : α → β → M
h : ∀ (b : β), b ∈ s → Set.Finite (mulSupport fun a => f a b)
hU :
  (mulSupport fun a => ∏ b in s, f a b) ⊆
    ↑(Finite.toFinset (_ : Set.Finite (⋃ (i : β) (_ : i ∈ ↑s), mulSupport fun a => f a i)))
⊢ (∏ᶠ (a : α), ∏ b in s, f a b) = ∏ b in s, ∏ᶠ (a : α), f a b
α : Type u_2
β : Type u_1
ι : Type ?u.386315
G : Type ?u.386318
M : Type u_3
N : Type ?u.386324
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a b : α
s✝ t : Set α
s : Finset β
f : α → β → M
h : ∀ (b : β), b ∈ s → Set.Finite (mulSupport fun a => f a b)
⊢ (∏ᶠ (a : α), ∏ b in s, f a b) = ∏ b in s, ∏ᶠ (a : α), f a b
have hU :
  (mulSupport fun a => ∏ b in 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.def, mem_mulSupport, Finset.mem_coe]
  contrapose! hx
  rw [mem_mulSupport, not_not, Finset.prod_congr rfl hx, Finset.prod_const_one]
α : Type u_2
β : Type u_1
ι : Type ?u.386315
G : Type ?u.386318
M : Type u_3
N : Type ?u.386324
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a b : α
s✝ t : Set α
s : Finset β
f : α → β → M
h : ∀ (b : β), b ∈ s → Set.Finite (mulSupport fun a => f a b)
hU :
  (mulSupport fun a => ∏ b in s, f a b) ⊆
    ↑(Finite.toFinset (_ : Set.Finite (⋃ (i : β) (_ : i ∈ ↑s), mulSupport fun a => f a i)))
⊢ ∏ y in s, ∏ x in Finite.toFinset (_ : Set.Finite (⋃ (i : β) (_ : i ∈ ↑s), mulSupport fun a => f a i)), f x y =
    ∏ b in s, ∏ᶠ (a : α), f a b
α : Type u_2
β : Type u_1
ι : Type ?u.386315
G : Type ?u.386318
M : Type u_3
N : Type ?u.386324
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a b : α
s✝ t : Set α
s : Finset β
f : α → β → M
h : ∀ (b : β), b ∈ s → Set.Finite (mulSupport fun a => f a b)
hU :
  (mulSupport fun a => ∏ b in s, f a b) ⊆
    ↑(Finite.toFinset (_ : Set.Finite (⋃ (i : β) (_ : i ∈ ↑s), mulSupport fun a => f a i)))
⊢ (∏ᶠ (a : α), ∏ b in s, f a b) = ∏ b in s, ∏ᶠ (a : α), f a b
rw [finprod_eq_prod_of_mulSupport_subset _ hU, Finset.prod_comm]
α : Type u_2
β : Type u_1
ι : Type ?u.386315
G : Type ?u.386318
M : Type u_3
N : Type ?u.386324
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a b✝ : α
s✝ t : Set α
s : Finset β
f : α → β → M
h : ∀ (b : β), b ∈ s → Set.Finite (mulSupport fun a => f a b)
hU :
  (mulSupport fun a => ∏ b in s, f a b) ⊆
    ↑(Finite.toFinset (_ : Set.Finite (⋃ (i : β) (_ : i ∈ ↑s), mulSupport fun a => f a i)))
b : β
hb : b ∈ s
⊢ (mulSupport fun x => f x b) ⊆ ↑(Finite.toFinset (_ : Set.Finite (⋃ (i : β) (_ : i ∈ ↑s), mulSupport fun a => f a i)))
α : Type u_2
β : Type u_1
ι : Type ?u.386315
G : Type ?u.386318
M : Type u_3
N : Type ?u.386324
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a b : α
s✝ t : Set α
s : Finset β
f : α → β → M
h : ∀ (b : β), b ∈ s → Set.Finite (mulSupport fun a => f a b)
hU :
  (mulSupport fun a => ∏ b in s, f a b) ⊆
    ↑(Finite.toFinset (_ : Set.Finite (⋃ (i : β) (_ : i ∈ ↑s), mulSupport fun a => f a i)))
⊢ ∏ y in s, ∏ x in Finite.toFinset (_ : Set.Finite (⋃ (i : β) (_ : i ∈ ↑s), mulSupport fun a => f a i)), f x y =
    ∏ b in s, ∏ᶠ (a : α), f a b
refine' Finset.prod_congr rfl fun b hb => (finprod_eq_prod_of_mulSupport_subset _ _).symm
α : Type u_2
β : Type u_1
ι : Type ?u.386315
G : Type ?u.386318
M : Type u_3
N : Type ?u.386324
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a✝ b✝ : α
s✝ t : Set α
s : Finset β
f : α → β → M
h : ∀ (b : β), b ∈ s → Set.Finite (mulSupport fun a => f a b)
hU :
  (mulSupport fun a => ∏ b in s, f a b) ⊆
    ↑(Finite.toFinset (_ : Set.Finite (⋃ (i : β) (_ : i ∈ ↑s), mulSupport fun a => f a i)))
b : β
hb : b ∈ s
a : α
ha : a ∈ mulSupport fun x => f x b
⊢ a ∈ ↑(Finite.toFinset (_ : Set.Finite (⋃ (i : β) (_ : i ∈ ↑s), mulSupport fun a => f a i)))
α : Type u_2
β : Type u_1
ι : Type ?u.386315
G : Type ?u.386318
M : Type u_3
N : Type ?u.386324
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a b✝ : α
s✝ t : Set α
s : Finset β
f : α → β → M
h : ∀ (b : β), b ∈ s → Set.Finite (mulSupport fun a => f a b)
hU :
  (mulSupport fun a => ∏ b in s, f a b) ⊆
    ↑(Finite.toFinset (_ : Set.Finite (⋃ (i : β) (_ : i ∈ ↑s), mulSupport fun a => f a i)))
b : β
hb : b ∈ s
⊢ (mulSupport fun x => f x b) ⊆ ↑(Finite.toFinset (_ : Set.Finite (⋃ (i : β) (_ : i ∈ ↑s), mulSupport fun a => f a i)))
intro a ha
α : Type u_2
β : Type u_1
ι : Type ?u.386315
G : Type ?u.386318
M : Type u_3
N : Type ?u.386324
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a✝ b✝ : α
s✝ t : Set α
s : Finset β
f : α → β → M
h : ∀ (b : β), b ∈ s → Set.Finite (mulSupport fun a => f a b)
hU :
  (mulSupport fun a => ∏ b in s, f a b) ⊆
    ↑(Finite.toFinset (_ : Set.Finite (⋃ (i : β) (_ : i ∈ ↑s), mulSupport fun a => f a i)))
b : β
hb : b ∈ s
a : α
ha : a ∈ mulSupport fun x => f x b
⊢ ∃ i i_1, a ∈ mulSupport fun a => f a i
α : Type u_2
β : Type u_1
ι : Type ?u.386315
G : Type ?u.386318
M : Type u_3
N : Type ?u.386324
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a✝ b✝ : α
s✝ t : Set α
s : Finset β
f : α → β → M
h : ∀ (b : β), b ∈ s → Set.Finite (mulSupport fun a => f a b)
hU :
  (mulSupport fun a => ∏ b in s, f a b) ⊆
    ↑(Finite.toFinset (_ : Set.Finite (⋃ (i : β) (_ : i ∈ ↑s), mulSupport fun a => f a i)))
b : β
hb : b ∈ s
a : α
ha : a ∈ mulSupport fun x => f x b
⊢ a ∈ ↑(Finite.toFinset (_ : Set.Finite (⋃ (i : β) (_ : i ∈ ↑s), mulSupport fun a => f a i)))
simp only [Finite.coe_toFinset, mem_iUnion]
no goals
α : Type u_2
β : Type u_1
ι : Type ?u.386315
G : Type ?u.386318
M : Type u_3
N : Type ?u.386324
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a✝ b✝ : α
s✝ t : Set α
s : Finset β
f : α → β → M
h : ∀ (b : β), b ∈ s → Set.Finite (mulSupport fun a => f a b)
hU :
  (mulSupport fun a => ∏ b in s, f a b) ⊆
    ↑(Finite.toFinset (_ : Set.Finite (⋃ (i : β) (_ : i ∈ ↑s), mulSupport fun a => f a i)))
b : β
hb : b ∈ s
a : α
ha : a ∈ mulSupport fun x => f x b
⊢ ∃ i i_1, a ∈ mulSupport fun a => f a i
exact ⟨b, hb, ha⟩
α : Type u_2
β : Type u_1
ι : Type ?u.386315
G : Type ?u.386318
M : Type u_3
N : Type ?u.386324
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a b : α
s✝ t : Set α
s : Finset β
f : α → β → M
h : ∀ (b : β), b ∈ s → Set.Finite (mulSupport fun a => f a b)
⊢ (mulSupport fun a => ∏ b in s, f a b) ⊆ ⋃ (i : β) (_ : i ∈ ↑s), mulSupport fun a => f a i
α : Type u_2
β : Type u_1
ι : Type ?u.386315
G : Type ?u.386318
M : Type u_3
N : Type ?u.386324
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a b : α
s✝ t : Set α
s : Finset β
f : α → β → M
h : ∀ (b : β), b ∈ s → Set.Finite (mulSupport fun a => f a b)
⊢ (mulSupport fun a => ∏ b in s, f a b) ⊆
    ↑(Finite.toFinset (_ : Set.Finite (⋃ (i : β) (_ : i ∈ ↑s), mulSupport fun a => f a i)))
rw [Finite.coe_toFinset]
α : Type u_2
β : Type u_1
ι : Type ?u.386315
G : Type ?u.386318
M : Type u_3
N : Type ?u.386324
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a b : α
s✝ t : Set α
s : Finset β
f : α → β → M
h : ∀ (b : β), b ∈ s → Set.Finite (mulSupport fun a => f a b)
x : α
hx : x ∈ mulSupport fun a => ∏ b in s, f a b
⊢ x ∈ ⋃ (i : β) (_ : i ∈ ↑s), mulSupport fun a => f a i
α : Type u_2
β : Type u_1
ι : Type ?u.386315
G : Type ?u.386318
M : Type u_3
N : Type ?u.386324
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a b : α
s✝ t : Set α
s : Finset β
f : α → β → M
h : ∀ (b : β), b ∈ s → Set.Finite (mulSupport fun a => f a b)
⊢ (mulSupport fun a => ∏ b in s, f a b) ⊆ ⋃ (i : β) (_ : i ∈ ↑s), mulSupport fun a => f a i
intro x hx
α : Type u_2
β : Type u_1
ι : Type ?u.386315
G : Type ?u.386318
M : Type u_3
N : Type ?u.386324
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a b : α
s✝ t : Set α
s : Finset β
f : α → β → M
h : ∀ (b : β), b ∈ s → Set.Finite (mulSupport fun a => f a b)
x : α
hx : x ∈ mulSupport fun a => ∏ b in s, f a b
⊢ ∃ i, i ∈ s ∧ ¬f x i = 1
α : Type u_2
β : Type u_1
ι : Type ?u.386315
G : Type ?u.386318
M : Type u_3
N : Type ?u.386324
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a b : α
s✝ t : Set α
s : Finset β
f : α → β → M
h : ∀ (b : β), b ∈ s → Set.Finite (mulSupport fun a => f a b)
x : α
hx : x ∈ mulSupport fun a => ∏ b in s, f a b
⊢ x ∈ ⋃ (i : β) (_ : i ∈ ↑s), mulSupport fun a => f a i
simp only [exists_prop, mem_iUnion, Ne.def, mem_mulSupport, Finset.mem_coe]
α : Type u_2
β : Type u_1
ι : Type ?u.386315
G : Type ?u.386318
M : Type u_3
N : Type ?u.386324
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a b : α
s✝ t : Set α
s : Finset β
f : α → β → M
h : ∀ (b : β), b ∈ s → Set.Finite (mulSupport fun a => f a b)
x : α
hx : ∀ (i : β), i ∈ s → f x i = 1
⊢ ¬x ∈ mulSupport fun a => ∏ b in s, f a b
α : Type u_2
β : Type u_1
ι : Type ?u.386315
G : Type ?u.386318
M : Type u_3
N : Type ?u.386324
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a b : α
s✝ t : Set α
s : Finset β
f : α → β → M
h : ∀ (b : β), b ∈ s → Set.Finite (mulSupport fun a => f a b)
x : α
hx : x ∈ mulSupport fun a => ∏ b in s, f a b
⊢ ∃ i, i ∈ s ∧ ¬f x i = 1
contrapose! hx
no goals
α : Type u_2
β : Type u_1
ι : Type ?u.386315
G : Type ?u.386318
M : Type u_3
N : Type ?u.386324
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a b : α
s✝ t : Set α
s : Finset β
f : α → β → M
h : ∀ (b : β), b ∈ s → Set.Finite (mulSupport fun a => f a b)
x : α
hx : ∀ (i : β), i ∈ s → f x i = 1
⊢ ¬x ∈ mulSupport fun a => ∏ b in s, f a b
rw [mem_mulSupport, not_not, Finset.prod_congr rfl hx, Finset.prod_const_one]