case h
α : Type u_1
β : Type ?u.190903
ι : Type ?u.190906
G : Type ?u.190909
M : Type u_2
N : Type ?u.190915
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f : α → M
a : α
inst✝ : DecidableEq α
hf : Set.Finite (mulSupport f)
⊢ ∀ {x : α}, f x ≠ 1 → (x ≠ a ↔ x ∈ Finset.erase (Finite.toFinset hf) a)
α : Type u_1
β : Type ?u.190903
ι : Type ?u.190906
G : Type ?u.190909
M : Type u_2
N : Type ?u.190915
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f : α → M
a : α
inst✝ : DecidableEq α
hf : Set.Finite (mulSupport f)
⊢ (∏ᶠ (i : α) (_ : i ≠ a), f i) = ∏ i in Finset.erase (Finite.toFinset hf) a, f i
apply finprod_cond_eq_prod_of_cond_iff
case h
α : Type u_1
β : Type ?u.190903
ι : Type ?u.190906
G : Type ?u.190909
M : Type u_2
N : Type ?u.190915
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f : α → M
a : α
inst✝ : DecidableEq α
hf : Set.Finite (mulSupport f)
x : α
hx : f x ≠ 1
⊢ x ≠ a ↔ x ∈ Finset.erase (Finite.toFinset hf) a
case h
α : Type u_1
β : Type ?u.190903
ι : Type ?u.190906
G : Type ?u.190909
M : Type u_2
N : Type ?u.190915
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f : α → M
a : α
inst✝ : DecidableEq α
hf : Set.Finite (mulSupport f)
⊢ ∀ {x : α}, f x ≠ 1 → (x ≠ a ↔ x ∈ Finset.erase (Finite.toFinset hf) a)
intro x hx
case h
α : Type u_1
β : Type ?u.190903
ι : Type ?u.190906
G : Type ?u.190909
M : Type u_2
N : Type ?u.190915
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f : α → M
a : α
inst✝ : DecidableEq α
hf : Set.Finite (mulSupport f)
x : α
hx : f x ≠ 1
⊢ x ≠ a ↔ x ≠ a ∧ f x ≠ 1
case h
α : Type u_1
β : Type ?u.190903
ι : Type ?u.190906
G : Type ?u.190909
M : Type u_2
N : Type ?u.190915
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f : α → M
a : α
inst✝ : DecidableEq α
hf : Set.Finite (mulSupport f)
x : α
hx : f x ≠ 1
⊢ x ≠ a ↔ x ∈ Finset.erase (Finite.toFinset hf) a
rw [Finset.mem_erase, Finite.mem_toFinset, mem_mulSupport]
no goals
case h
α : Type u_1
β : Type ?u.190903
ι : Type ?u.190906
G : Type ?u.190909
M : Type u_2
N : Type ?u.190915
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f : α → M
a : α
inst✝ : DecidableEq α
hf : Set.Finite (mulSupport f)
x : α
hx : f x ≠ 1
⊢ x ≠ a ↔ x ≠ a ∧ f x ≠ 1
exact ⟨fun h => And.intro h hx, fun h => h.1⟩