G : Type ?u.34693
M : Type u_2
N : Type ?u.34699
α : Sort u_1
β : Sort ?u.34705
ι : Sort ?u.34708
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
a : α
ha : ∀ (x : α), x ≠ a → f x = 1
this : mulSupport (f ∘ PLift.down) ⊆ ↑{{ down := a }}
⊢ (∏ᶠ (x : α), f x) = f a
G : Type ?u.34693
M : Type u_2
N : Type ?u.34699
α : Sort u_1
β : Sort ?u.34705
ι : Sort ?u.34708
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
a : α
ha : ∀ (x : α), x ≠ a → f x = 1
⊢ (∏ᶠ (x : α), f x) = f a
have : mulSupport (f ∘ PLift.down) ⊆ ({PLift.up a} : Finset (PLift α)) := by
  intro x
  contrapose
  simpa [PLift.eq_up_iff_down_eq] using ha x.down
no goals
G : Type ?u.34693
M : Type u_2
N : Type ?u.34699
α : Sort u_1
β : Sort ?u.34705
ι : Sort ?u.34708
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
a : α
ha : ∀ (x : α), x ≠ a → f x = 1
this : mulSupport (f ∘ PLift.down) ⊆ ↑{{ down := a }}
⊢ (∏ᶠ (x : α), f x) = f a
rw [finprod_eq_prod_pLift_of_mulSupport_subset this, Finset.prod_singleton]
G : Type ?u.34693
M : Type u_2
N : Type ?u.34699
α : Sort u_1
β : Sort ?u.34705
ι : Sort ?u.34708
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
a : α
ha : ∀ (x : α), x ≠ a → f x = 1
x : PLift α
⊢ x ∈ mulSupport (f ∘ PLift.down) → x ∈ ↑{{ down := a }}
G : Type ?u.34693
M : Type u_2
N : Type ?u.34699
α : Sort u_1
β : Sort ?u.34705
ι : Sort ?u.34708
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
a : α
ha : ∀ (x : α), x ≠ a → f x = 1
⊢ mulSupport (f ∘ PLift.down) ⊆ ↑{{ down := a }}
intro x
G : Type ?u.34693
M : Type u_2
N : Type ?u.34699
α : Sort u_1
β : Sort ?u.34705
ι : Sort ?u.34708
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
a : α
ha : ∀ (x : α), x ≠ a → f x = 1
x : PLift α
⊢ ¬x ∈ ↑{{ down := a }} → ¬x ∈ mulSupport (f ∘ PLift.down)
G : Type ?u.34693
M : Type u_2
N : Type ?u.34699
α : Sort u_1
β : Sort ?u.34705
ι : Sort ?u.34708
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
a : α
ha : ∀ (x : α), x ≠ a → f x = 1
x : PLift α
⊢ x ∈ mulSupport (f ∘ PLift.down) → x ∈ ↑{{ down := a }}
contrapose
no goals
G : Type ?u.34693
M : Type u_2
N : Type ?u.34699
α : Sort u_1
β : Sort ?u.34705
ι : Sort ?u.34708
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
a : α
ha : ∀ (x : α), x ≠ a → f x = 1
x : PLift α
⊢ ¬x ∈ ↑{{ down := a }} → ¬x ∈ mulSupport (f ∘ PLift.down)
simpa [PLift.eq_up_iff_down_eq] using ha x.down