α : Type u_1
β : Type ?u.370818
ι : Type ?u.370821
G : Type ?u.370824
M : Type u_2
N : Type ?u.370830
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a✝ b : α
s t : Set α
a : α
hf : Set.Finite (mulSupport f)
⊢ (f a * ∏ᶠ (i : α) (_ : i ≠ a), f i) = ∏ i in Finite.toFinset hf, f i
α : Type u_1
β : Type ?u.370818
ι : Type ?u.370821
G : Type ?u.370824
M : Type u_2
N : Type ?u.370830
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a✝ b : α
s t : Set α
a : α
hf : Set.Finite (mulSupport f)
⊢ (f a * ∏ᶠ (i : α) (_ : i ≠ a), f i) = ∏ᶠ (i : α), f i
rw [finprod_eq_prod _ hf]
α : Type u_1
β : Type ?u.370818
ι : Type ?u.370821
G : Type ?u.370824
M : Type u_2
N : Type ?u.370830
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a✝ b : α
s t : Set α
a : α
hf : Set.Finite (mulSupport f)
h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ Finite.toFinset hf \ {a})
⊢ (f a * ∏ᶠ (i : α) (_ : i ≠ a), f i) = ∏ i in Finite.toFinset hf, f i
α : Type u_1
β : Type ?u.370818
ι : Type ?u.370821
G : Type ?u.370824
M : Type u_2
N : Type ?u.370830
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a✝ b : α
s t : Set α
a : α
hf : Set.Finite (mulSupport f)
⊢ (f a * ∏ᶠ (i : α) (_ : i ≠ a), f i) = ∏ i in Finite.toFinset hf, f i
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]
  exact ⟨fun h => And.intro hx h, fun h => h.2⟩
α : Type u_1
β : Type ?u.370818
ι : Type ?u.370821
G : Type ?u.370824
M : Type u_2
N : Type ?u.370830
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a✝ b : α
s t : Set α
a : α
hf : Set.Finite (mulSupport f)
h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ Finite.toFinset hf \ {a})
⊢ f a * ∏ i in Finset.erase (Finite.toFinset hf) a, f i = ∏ i in Finite.toFinset hf, f i
α : Type u_1
β : Type ?u.370818
ι : Type ?u.370821
G : Type ?u.370824
M : Type u_2
N : Type ?u.370830
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a✝ b : α
s t : Set α
a : α
hf : Set.Finite (mulSupport f)
h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ Finite.toFinset hf \ {a})
⊢ (f a * ∏ᶠ (i : α) (_ : i ≠ a), f i) = ∏ i in Finite.toFinset hf, f i
rw [finprod_cond_eq_prod_of_cond_iff f (fun hx => h _ hx), Finset.sdiff_singleton_eq_erase]
case pos
α : Type u_1
β : Type ?u.370818
ι : Type ?u.370821
G : Type ?u.370824
M : Type u_2
N : Type ?u.370830
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a✝ b : α
s t : Set α
a : α
hf : Set.Finite (mulSupport f)
h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ Finite.toFinset hf \ {a})
ha : a ∈ mulSupport f
⊢ f a * ∏ i in Finset.erase (Finite.toFinset hf) a, f i = ∏ i in Finite.toFinset hf, f i

case neg
α : Type u_1
β : Type ?u.370818
ι : Type ?u.370821
G : Type ?u.370824
M : Type u_2
N : Type ?u.370830
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a✝ b : α
s t : Set α
a : α
hf : Set.Finite (mulSupport f)
h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ Finite.toFinset hf \ {a})
ha : ¬a ∈ mulSupport f
⊢ f a * ∏ i in Finset.erase (Finite.toFinset hf) a, f i = ∏ i in Finite.toFinset hf, f i
α : Type u_1
β : Type ?u.370818
ι : Type ?u.370821
G : Type ?u.370824
M : Type u_2
N : Type ?u.370830
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a✝ b : α
s t : Set α
a : α
hf : Set.Finite (mulSupport f)
h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ Finite.toFinset hf \ {a})
⊢ f a * ∏ i in Finset.erase (Finite.toFinset hf) a, f i = ∏ i in Finite.toFinset hf, f i
by_cases ha : a ∈ mulSupport f
α : Type u_1
β : Type ?u.370818
ι : Type ?u.370821
G : Type ?u.370824
M : Type u_2
N : Type ?u.370830
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a✝ b : α
s t : Set α
a : α
hf : Set.Finite (mulSupport f)
x : α
hx : f x ≠ 1
⊢ x ≠ a ↔ x ∈ Finite.toFinset hf \ {a}
α : Type u_1
β : Type ?u.370818
ι : Type ?u.370821
G : Type ?u.370824
M : Type u_2
N : Type ?u.370830
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a✝ b : α
s t : Set α
a : α
hf : Set.Finite (mulSupport f)
⊢ ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ Finite.toFinset hf \ {a})
intro x hx
α : Type u_1
β : Type ?u.370818
ι : Type ?u.370821
G : Type ?u.370824
M : Type u_2
N : Type ?u.370830
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a✝ b : α
s t : Set α
a : α
hf : Set.Finite (mulSupport f)
x : α
hx : f x ≠ 1
⊢ x ≠ a ↔ f x ≠ 1 ∧ ¬x = a
α : Type u_1
β : Type ?u.370818
ι : Type ?u.370821
G : Type ?u.370824
M : Type u_2
N : Type ?u.370830
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a✝ b : α
s t : Set α
a : α
hf : Set.Finite (mulSupport f)
x : α
hx : f x ≠ 1
⊢ x ≠ a ↔ x ∈ Finite.toFinset hf \ {a}
rw [Finset.mem_sdiff, Finset.mem_singleton, Finite.mem_toFinset, mem_mulSupport]
no goals
α : Type u_1
β : Type ?u.370818
ι : Type ?u.370821
G : Type ?u.370824
M : Type u_2
N : Type ?u.370830
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a✝ b : α
s t : Set α
a : α
hf : Set.Finite (mulSupport f)
x : α
hx : f x ≠ 1
⊢ x ≠ a ↔ f x ≠ 1 ∧ ¬x = a
exact ⟨fun h => And.intro hx h, fun h => h.2⟩
no goals
case pos
α : Type u_1
β : Type ?u.370818
ι : Type ?u.370821
G : Type ?u.370824
M : Type u_2
N : Type ?u.370830
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a✝ b : α
s t : Set α
a : α
hf : Set.Finite (mulSupport f)
h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ Finite.toFinset hf \ {a})
ha : a ∈ mulSupport f
⊢ f a * ∏ i in Finset.erase (Finite.toFinset hf) a, f i = ∏ i in Finite.toFinset hf, f i
apply Finset.mul_prod_erase _ _ ((Finite.mem_toFinset _).mpr ha)
case neg
α : Type u_1
β : Type ?u.370818
ι : Type ?u.370821
G : Type ?u.370824
M : Type u_2
N : Type ?u.370830
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a✝ b : α
s t : Set α
a : α
hf : Set.Finite (mulSupport f)
h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ Finite.toFinset hf \ {a})
ha : f a = 1
⊢ f a * ∏ i in Finset.erase (Finite.toFinset hf) a, f i = ∏ i in Finite.toFinset hf, f i
case neg
α : Type u_1
β : Type ?u.370818
ι : Type ?u.370821
G : Type ?u.370824
M : Type u_2
N : Type ?u.370830
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a✝ b : α
s t : Set α
a : α
hf : Set.Finite (mulSupport f)
h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ Finite.toFinset hf \ {a})
ha : ¬a ∈ mulSupport f
⊢ f a * ∏ i in Finset.erase (Finite.toFinset hf) a, f i = ∏ i in Finite.toFinset hf, f i
rw [mem_mulSupport, not_not] at ha
case neg
α : Type u_1
β : Type ?u.370818
ι : Type ?u.370821
G : Type ?u.370824
M : Type u_2
N : Type ?u.370830
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a✝ b : α
s t : Set α
a : α
hf : Set.Finite (mulSupport f)
h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ Finite.toFinset hf \ {a})
ha : f a = 1
⊢ ∏ i in Finset.erase (Finite.toFinset hf) a, f i = ∏ i in Finite.toFinset hf, f i
case neg
α : Type u_1
β : Type ?u.370818
ι : Type ?u.370821
G : Type ?u.370824
M : Type u_2
N : Type ?u.370830
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a✝ b : α
s t : Set α
a : α
hf : Set.Finite (mulSupport f)
h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ Finite.toFinset hf \ {a})
ha : f a = 1
⊢ f a * ∏ i in Finset.erase (Finite.toFinset hf) a, f i = ∏ i in Finite.toFinset hf, f i
rw [ha, one_mul]
no goals
case neg
α : Type u_1
β : Type ?u.370818
ι : Type ?u.370821
G : Type ?u.370824
M : Type u_2
N : Type ?u.370830
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a✝ b : α
s t : Set α
a : α
hf : Set.Finite (mulSupport f)
h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ Finite.toFinset hf \ {a})
ha : f a = 1
⊢ ∏ i in Finset.erase (Finite.toFinset hf) a, f i = ∏ i in Finite.toFinset hf, f i
apply Finset.prod_erase _ ha