case pos
α : Type u_1
β : Type ?u.347101
ι : Type ?u.347104
G : Type ?u.347107
M : Type ?u.347110
N : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a✝ b : α
s t : Set α
f : α → N
a : α
hf : Set.Finite (mulSupport f)
ha : a ∈ mulSupport f
⊢ f a ∣ finprod f

case neg
α : Type u_1
β : Type ?u.347101
ι : Type ?u.347104
G : Type ?u.347107
M : Type ?u.347110
N : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a✝ b : α
s t : Set α
f : α → N
a : α
hf : Set.Finite (mulSupport f)
ha : ¬a ∈ mulSupport f
⊢ f a ∣ finprod f
α : Type u_1
β : Type ?u.347101
ι : Type ?u.347104
G : Type ?u.347107
M : Type ?u.347110
N : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a✝ b : α
s t : Set α
f : α → N
a : α
hf : Set.Finite (mulSupport f)
⊢ f a ∣ finprod f
by_cases ha : a ∈ mulSupport f
case pos
α : Type u_1
β : Type ?u.347101
ι : Type ?u.347104
G : Type ?u.347107
M : Type ?u.347110
N : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a✝ b : α
s t : Set α
f : α → N
a : α
hf : Set.Finite (mulSupport f)
ha : a ∈ mulSupport f
⊢ f a ∣ ∏ i in Finite.toFinset hf, f i
case pos
α : Type u_1
β : Type ?u.347101
ι : Type ?u.347104
G : Type ?u.347107
M : Type ?u.347110
N : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a✝ b : α
s t : Set α
f : α → N
a : α
hf : Set.Finite (mulSupport f)
ha : a ∈ mulSupport f
⊢ f a ∣ finprod f
rw [finprod_eq_prod_of_mulSupport_toFinset_subset f hf (Set.Subset.refl _)]
no goals
case pos
α : Type u_1
β : Type ?u.347101
ι : Type ?u.347104
G : Type ?u.347107
M : Type ?u.347110
N : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a✝ b : α
s t : Set α
f : α → N
a : α
hf : Set.Finite (mulSupport f)
ha : a ∈ mulSupport f
⊢ f a ∣ ∏ i in Finite.toFinset hf, f i
exact Finset.dvd_prod_of_mem f ((Finite.mem_toFinset hf).mpr ha)
case neg
α : Type u_1
β : Type ?u.347101
ι : Type ?u.347104
G : Type ?u.347107
M : Type ?u.347110
N : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a✝ b : α
s t : Set α
f : α → N
a : α
hf : Set.Finite (mulSupport f)
ha : ¬a ∈ mulSupport f
⊢ 1 ∣ finprod f
case neg
α : Type u_1
β : Type ?u.347101
ι : Type ?u.347104
G : Type ?u.347107
M : Type ?u.347110
N : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a✝ b : α
s t : Set α
f : α → N
a : α
hf : Set.Finite (mulSupport f)
ha : ¬a ∈ mulSupport f
⊢ f a ∣ finprod f
rw [nmem_mulSupport.mp ha]
no goals
case neg
α : Type u_1
β : Type ?u.347101
ι : Type ?u.347104
G : Type ?u.347107
M : Type ?u.347110
N : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a✝ b : α
s t : Set α
f : α → N
a : α
hf : Set.Finite (mulSupport f)
ha : ¬a ∈ mulSupport f
⊢ 1 ∣ finprod f
exact one_dvd (finprod f)