case h
α : Type u_1
β : Type ?u.349608
ι : Type ?u.349611
G : Type ?u.349614
M : Type u_2
N : Type ?u.349620
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t : Set α
h : a ≠ b
⊢ ¬a ∈ {b}

case hs
α : Type u_1
β : Type ?u.349608
ι : Type ?u.349611
G : Type ?u.349614
M : Type u_2
N : Type ?u.349620
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t : Set α
h : a ≠ b
⊢ Set.Finite {b}
α : Type u_1
β : Type ?u.349608
ι : Type ?u.349611
G : Type ?u.349614
M : Type u_2
N : Type ?u.349620
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t : Set α
h : a ≠ b
⊢ (∏ᶠ (i : α) (_ : i ∈ {a, b}), f i) = f a * f b
rw [finprod_mem_insert, finprod_mem_singleton]
no goals
case h
α : Type u_1
β : Type ?u.349608
ι : Type ?u.349611
G : Type ?u.349614
M : Type u_2
N : Type ?u.349620
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t : Set α
h : a ≠ b
⊢ ¬a ∈ {b}

case hs
α : Type u_1
β : Type ?u.349608
ι : Type ?u.349611
G : Type ?u.349614
M : Type u_2
N : Type ?u.349620
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t : Set α
h : a ≠ b
⊢ Set.Finite {b}
exacts [h, finite_singleton b]