[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝² : Monoid α
inst✝¹ : Monoid β
inst✝ : MonoidHomClass F α β
f : F
a : Set α
as : List (Set α)
⊢ ↑f '' List.prod (a :: as) = List.prod (List.map (fun s => ↑f '' s) (a :: as))
[PROOFSTEP]
rw [List.map_cons, List.prod_cons, List.prod_cons, image_mul, image_list_prod _ _]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : MonoidHomClass F α β
f : F
⊢ ∀ (a : List (Set α)),
    ↑f '' Multiset.prod (Quotient.mk (List.isSetoid (Set α)) a) =
      Multiset.prod (Multiset.map (fun s => ↑f '' s) (Quotient.mk (List.isSetoid (Set α)) a))
[PROOFSTEP]
simpa only [Multiset.quot_mk_to_coe, Multiset.coe_prod, Multiset.coe_map] using image_list_prod f
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : MonoidHomClass F α β
t : Finset ι
f : ι → Set α
a : α
⊢ a ∈ ∏ i in t, f i ↔ ∃ g x, ∏ i in t, g i = a
[PROOFSTEP]
classical
induction' t using Finset.induction_on with i is hi ih generalizing a
· simp_rw [Finset.prod_empty, Set.mem_one]
  exact ⟨fun h ↦ ⟨fun _ ↦ a, fun hi ↦ False.elim (Finset.not_mem_empty _ hi), h.symm⟩, fun ⟨_, _, hf⟩ ↦ hf.symm⟩
rw [Finset.prod_insert hi, Set.mem_mul]
simp_rw [Finset.prod_insert hi]
simp_rw [ih]
constructor
· rintro ⟨x, y, hx, ⟨g, hg, rfl⟩, rfl⟩
  refine ⟨Function.update g i x, ?_, ?_⟩
  · intro j hj
    obtain rfl | hj := Finset.mem_insert.mp hj
    · rwa [Function.update_same]
    · rw [update_noteq (ne_of_mem_of_not_mem hj hi)]
      exact hg hj
  · rw [Finset.prod_update_of_not_mem hi, Function.update_same]
· rintro ⟨g, hg, rfl⟩
  exact ⟨g i, is.prod g, hg (is.mem_insert_self _), ⟨⟨g, fun hi ↦ hg (Finset.mem_insert_of_mem hi), rfl⟩, rfl⟩⟩
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : MonoidHomClass F α β
t : Finset ι
f : ι → Set α
a : α
⊢ a ∈ ∏ i in t, f i ↔ ∃ g x, ∏ i in t, g i = a
[PROOFSTEP]
induction' t using Finset.induction_on with i is hi ih generalizing a
[GOAL]
case empty
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : MonoidHomClass F α β
f : ι → Set α
a✝ a : α
⊢ a ∈ ∏ i in ∅, f i ↔ ∃ g x, ∏ i in ∅, g i = a
[PROOFSTEP]
simp_rw [Finset.prod_empty, Set.mem_one]
[GOAL]
case empty
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : MonoidHomClass F α β
f : ι → Set α
a✝ a : α
⊢ a = 1 ↔ ∃ g h, 1 = a
[PROOFSTEP]
exact ⟨fun h ↦ ⟨fun _ ↦ a, fun hi ↦ False.elim (Finset.not_mem_empty _ hi), h.symm⟩, fun ⟨_, _, hf⟩ ↦ hf.symm⟩
[GOAL]
case insert
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : MonoidHomClass F α β
f : ι → Set α
a✝ : α
i : ι
is : Finset ι
hi : ¬i ∈ is
ih : ∀ (a : α), a ∈ ∏ i in is, f i ↔ ∃ g x, ∏ i in is, g i = a
a : α
⊢ a ∈ ∏ i in insert i is, f i ↔ ∃ g x, ∏ i in insert i is, g i = a
[PROOFSTEP]
rw [Finset.prod_insert hi, Set.mem_mul]
[GOAL]
case insert
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : MonoidHomClass F α β
f : ι → Set α
a✝ : α
i : ι
is : Finset ι
hi : ¬i ∈ is
ih : ∀ (a : α), a ∈ ∏ i in is, f i ↔ ∃ g x, ∏ i in is, g i = a
a : α
⊢ (∃ x y, x ∈ f i ∧ y ∈ ∏ x in is, f x ∧ x * y = a) ↔ ∃ g x, ∏ i in insert i is, g i = a
[PROOFSTEP]
simp_rw [Finset.prod_insert hi]
[GOAL]
case insert
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : MonoidHomClass F α β
f : ι → Set α
a✝ : α
i : ι
is : Finset ι
hi : ¬i ∈ is
ih : ∀ (a : α), a ∈ ∏ i in is, f i ↔ ∃ g x, ∏ i in is, g i = a
a : α
⊢ (∃ x y, x ∈ f i ∧ y ∈ ∏ x in is, f x ∧ x * y = a) ↔ ∃ g h, g i * ∏ i in is, g i = a
[PROOFSTEP]
simp_rw [ih]
[GOAL]
case insert
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : MonoidHomClass F α β
f : ι → Set α
a✝ : α
i : ι
is : Finset ι
hi : ¬i ∈ is
ih : ∀ (a : α), a ∈ ∏ i in is, f i ↔ ∃ g x, ∏ i in is, g i = a
a : α
⊢ (∃ x y, x ∈ f i ∧ (∃ g x, ∏ i in is, g i = y) ∧ x * y = a) ↔ ∃ g h, g i * ∏ i in is, g i = a
[PROOFSTEP]
constructor
[GOAL]
case insert.mp
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : MonoidHomClass F α β
f : ι → Set α
a✝ : α
i : ι
is : Finset ι
hi : ¬i ∈ is
ih : ∀ (a : α), a ∈ ∏ i in is, f i ↔ ∃ g x, ∏ i in is, g i = a
a : α
⊢ (∃ x y, x ∈ f i ∧ (∃ g x, ∏ i in is, g i = y) ∧ x * y = a) → ∃ g h, g i * ∏ i in is, g i = a
[PROOFSTEP]
rintro ⟨x, y, hx, ⟨g, hg, rfl⟩, rfl⟩
[GOAL]
case insert.mp.intro.intro.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : MonoidHomClass F α β
f : ι → Set α
a : α
i : ι
is : Finset ι
hi : ¬i ∈ is
ih : ∀ (a : α), a ∈ ∏ i in is, f i ↔ ∃ g x, ∏ i in is, g i = a
x : α
hx : x ∈ f i
g : ι → α
hg : ∀ {i : ι}, i ∈ is → g i ∈ f i
⊢ ∃ g_1 h, g_1 i * ∏ i in is, g_1 i = x * ∏ i in is, g i
[PROOFSTEP]
refine ⟨Function.update g i x, ?_, ?_⟩
[GOAL]
case insert.mp.intro.intro.intro.intro.intro.intro.refine_1
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : MonoidHomClass F α β
f : ι → Set α
a : α
i : ι
is : Finset ι
hi : ¬i ∈ is
ih : ∀ (a : α), a ∈ ∏ i in is, f i ↔ ∃ g x, ∏ i in is, g i = a
x : α
hx : x ∈ f i
g : ι → α
hg : ∀ {i : ι}, i ∈ is → g i ∈ f i
⊢ ∀ {i_1 : ι}, i_1 ∈ insert i is → update g i x i_1 ∈ f i_1
[PROOFSTEP]
intro j hj
[GOAL]
case insert.mp.intro.intro.intro.intro.intro.intro.refine_1
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : MonoidHomClass F α β
f : ι → Set α
a : α
i : ι
is : Finset ι
hi : ¬i ∈ is
ih : ∀ (a : α), a ∈ ∏ i in is, f i ↔ ∃ g x, ∏ i in is, g i = a
x : α
hx : x ∈ f i
g : ι → α
hg : ∀ {i : ι}, i ∈ is → g i ∈ f i
j : ι
hj : j ∈ insert i is
⊢ update g i x j ∈ f j
[PROOFSTEP]
obtain rfl | hj := Finset.mem_insert.mp hj
[GOAL]
case insert.mp.intro.intro.intro.intro.intro.intro.refine_1.inl
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : MonoidHomClass F α β
f : ι → Set α
a : α
is : Finset ι
ih : ∀ (a : α), a ∈ ∏ i in is, f i ↔ ∃ g x, ∏ i in is, g i = a
x : α
g : ι → α
hg : ∀ {i : ι}, i ∈ is → g i ∈ f i
j : ι
hi : ¬j ∈ is
hx : x ∈ f j
hj : j ∈ insert j is
⊢ update g j x j ∈ f j
[PROOFSTEP]
rwa [Function.update_same]
[GOAL]
case insert.mp.intro.intro.intro.intro.intro.intro.refine_1.inr
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : MonoidHomClass F α β
f : ι → Set α
a : α
i : ι
is : Finset ι
hi : ¬i ∈ is
ih : ∀ (a : α), a ∈ ∏ i in is, f i ↔ ∃ g x, ∏ i in is, g i = a
x : α
hx : x ∈ f i
g : ι → α
hg : ∀ {i : ι}, i ∈ is → g i ∈ f i
j : ι
hj✝ : j ∈ insert i is
hj : j ∈ is
⊢ update g i x j ∈ f j
[PROOFSTEP]
rw [update_noteq (ne_of_mem_of_not_mem hj hi)]
[GOAL]
case insert.mp.intro.intro.intro.intro.intro.intro.refine_1.inr
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : MonoidHomClass F α β
f : ι → Set α
a : α
i : ι
is : Finset ι
hi : ¬i ∈ is
ih : ∀ (a : α), a ∈ ∏ i in is, f i ↔ ∃ g x, ∏ i in is, g i = a
x : α
hx : x ∈ f i
g : ι → α
hg : ∀ {i : ι}, i ∈ is → g i ∈ f i
j : ι
hj✝ : j ∈ insert i is
hj : j ∈ is
⊢ g j ∈ f j
[PROOFSTEP]
exact hg hj
[GOAL]
case insert.mp.intro.intro.intro.intro.intro.intro.refine_2
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : MonoidHomClass F α β
f : ι → Set α
a : α
i : ι
is : Finset ι
hi : ¬i ∈ is
ih : ∀ (a : α), a ∈ ∏ i in is, f i ↔ ∃ g x, ∏ i in is, g i = a
x : α
hx : x ∈ f i
g : ι → α
hg : ∀ {i : ι}, i ∈ is → g i ∈ f i
⊢ update g i x i * ∏ i_1 in is, update g i x i_1 = x * ∏ i in is, g i
[PROOFSTEP]
rw [Finset.prod_update_of_not_mem hi, Function.update_same]
[GOAL]
case insert.mpr
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : MonoidHomClass F α β
f : ι → Set α
a✝ : α
i : ι
is : Finset ι
hi : ¬i ∈ is
ih : ∀ (a : α), a ∈ ∏ i in is, f i ↔ ∃ g x, ∏ i in is, g i = a
a : α
⊢ (∃ g h, g i * ∏ i in is, g i = a) → ∃ x y, x ∈ f i ∧ (∃ g x, ∏ i in is, g i = y) ∧ x * y = a
[PROOFSTEP]
rintro ⟨g, hg, rfl⟩
[GOAL]
case insert.mpr.intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : MonoidHomClass F α β
f : ι → Set α
a : α
i : ι
is : Finset ι
hi : ¬i ∈ is
ih : ∀ (a : α), a ∈ ∏ i in is, f i ↔ ∃ g x, ∏ i in is, g i = a
g : ι → α
hg : ∀ {i_1 : ι}, i_1 ∈ insert i is → g i_1 ∈ f i_1
⊢ ∃ x y, x ∈ f i ∧ (∃ g x, ∏ i in is, g i = y) ∧ x * y = g i * ∏ i in is, g i
[PROOFSTEP]
exact ⟨g i, is.prod g, hg (is.mem_insert_self _), ⟨⟨g, fun hi ↦ hg (Finset.mem_insert_of_mem hi), rfl⟩, rfl⟩⟩
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝³ : CommMonoid α
inst✝² : CommMonoid β
inst✝¹ : MonoidHomClass F α β
inst✝ : Fintype ι
f : ι → Set α
a : α
⊢ a ∈ ∏ i : ι, f i ↔ ∃ g x, ∏ i : ι, g i = a
[PROOFSTEP]
rw [mem_finset_prod]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝³ : CommMonoid α
inst✝² : CommMonoid β
inst✝¹ : MonoidHomClass F α β
inst✝ : Fintype ι
f : ι → Set α
a : α
⊢ (∃ g x, ∏ i : ι, g i = a) ↔ ∃ g x, ∏ i : ι, g i = a
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : MonoidHomClass F α β
t : List ι
f : ι → Set α
g : ι → α
hg : ∀ (i : ι), i ∈ t → g i ∈ f i
⊢ List.prod (List.map g t) ∈ List.prod (List.map f t)
[PROOFSTEP]
induction' t with h tl ih
[GOAL]
case nil
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : MonoidHomClass F α β
t : List ι
f : ι → Set α
g : ι → α
hg✝ : ∀ (i : ι), i ∈ t → g i ∈ f i
hg : ∀ (i : ι), i ∈ [] → g i ∈ f i
⊢ List.prod (List.map g []) ∈ List.prod (List.map f [])
[PROOFSTEP]
simp_rw [List.map_nil, List.prod_nil, Set.mem_one]
[GOAL]
case cons
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : MonoidHomClass F α β
t : List ι
f : ι → Set α
g : ι → α
hg✝ : ∀ (i : ι), i ∈ t → g i ∈ f i
h : ι
tl : List ι
ih : (∀ (i : ι), i ∈ tl → g i ∈ f i) → List.prod (List.map g tl) ∈ List.prod (List.map f tl)
hg : ∀ (i : ι), i ∈ h :: tl → g i ∈ f i
⊢ List.prod (List.map g (h :: tl)) ∈ List.prod (List.map f (h :: tl))
[PROOFSTEP]
simp_rw [List.map_cons, List.prod_cons]
[GOAL]
case cons
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : MonoidHomClass F α β
t : List ι
f : ι → Set α
g : ι → α
hg✝ : ∀ (i : ι), i ∈ t → g i ∈ f i
h : ι
tl : List ι
ih : (∀ (i : ι), i ∈ tl → g i ∈ f i) → List.prod (List.map g tl) ∈ List.prod (List.map f tl)
hg : ∀ (i : ι), i ∈ h :: tl → g i ∈ f i
⊢ g h * List.prod (List.map g tl) ∈ f h * List.prod (List.map f tl)
[PROOFSTEP]
exact mul_mem_mul (hg h <| List.mem_cons_self _ _) (ih fun i hi ↦ hg i <| List.mem_cons_of_mem _ hi)
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : MonoidHomClass F α β
t : List ι
f₁ f₂ : ι → Set α
hf : ∀ (i : ι), i ∈ t → f₁ i ⊆ f₂ i
⊢ List.prod (List.map f₁ t) ⊆ List.prod (List.map f₂ t)
[PROOFSTEP]
induction' t with h tl ih
[GOAL]
case nil
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : MonoidHomClass F α β
t : List ι
f₁ f₂ : ι → Set α
hf✝ : ∀ (i : ι), i ∈ t → f₁ i ⊆ f₂ i
hf : ∀ (i : ι), i ∈ [] → f₁ i ⊆ f₂ i
⊢ List.prod (List.map f₁ []) ⊆ List.prod (List.map f₂ [])
[PROOFSTEP]
rfl
[GOAL]
case cons
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : MonoidHomClass F α β
t : List ι
f₁ f₂ : ι → Set α
hf✝ : ∀ (i : ι), i ∈ t → f₁ i ⊆ f₂ i
h : ι
tl : List ι
ih : (∀ (i : ι), i ∈ tl → f₁ i ⊆ f₂ i) → List.prod (List.map f₁ tl) ⊆ List.prod (List.map f₂ tl)
hf : ∀ (i : ι), i ∈ h :: tl → f₁ i ⊆ f₂ i
⊢ List.prod (List.map f₁ (h :: tl)) ⊆ List.prod (List.map f₂ (h :: tl))
[PROOFSTEP]
simp_rw [List.map_cons, List.prod_cons]
[GOAL]
case cons
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : MonoidHomClass F α β
t : List ι
f₁ f₂ : ι → Set α
hf✝ : ∀ (i : ι), i ∈ t → f₁ i ⊆ f₂ i
h : ι
tl : List ι
ih : (∀ (i : ι), i ∈ tl → f₁ i ⊆ f₂ i) → List.prod (List.map f₁ tl) ⊆ List.prod (List.map f₂ tl)
hf : ∀ (i : ι), i ∈ h :: tl → f₁ i ⊆ f₂ i
⊢ f₁ h * List.prod (List.map f₁ tl) ⊆ f₂ h * List.prod (List.map f₂ tl)
[PROOFSTEP]
exact mul_subset_mul (hf h <| List.mem_cons_self _ _) (ih fun i hi ↦ hf i <| List.mem_cons_of_mem _ hi)
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : MonoidHomClass F α β
t : Multiset ι
f : ι → Set α
g : ι → α
hg : ∀ (i : ι), i ∈ t → g i ∈ f i
⊢ Multiset.prod (Multiset.map g t) ∈ Multiset.prod (Multiset.map f t)
[PROOFSTEP]
induction t using Quotient.inductionOn
[GOAL]
case h
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : MonoidHomClass F α β
f : ι → Set α
g : ι → α
a✝ : List ι
hg : ∀ (i : ι), i ∈ Quotient.mk (List.isSetoid ι) a✝ → g i ∈ f i
⊢ Multiset.prod (Multiset.map g (Quotient.mk (List.isSetoid ι) a✝)) ∈
    Multiset.prod (Multiset.map f (Quotient.mk (List.isSetoid ι) a✝))
[PROOFSTEP]
simp_rw [Multiset.quot_mk_to_coe, Multiset.coe_map, Multiset.coe_prod]
[GOAL]
case h
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : MonoidHomClass F α β
f : ι → Set α
g : ι → α
a✝ : List ι
hg : ∀ (i : ι), i ∈ Quotient.mk (List.isSetoid ι) a✝ → g i ∈ f i
⊢ List.prod (List.map g a✝) ∈ List.prod (List.map f a✝)
[PROOFSTEP]
exact list_prod_mem_list_prod _ _ _ hg
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : MonoidHomClass F α β
t : Multiset ι
f₁ f₂ : ι → Set α
hf : ∀ (i : ι), i ∈ t → f₁ i ⊆ f₂ i
⊢ Multiset.prod (Multiset.map f₁ t) ⊆ Multiset.prod (Multiset.map f₂ t)
[PROOFSTEP]
induction t using Quotient.inductionOn
[GOAL]
case h
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : MonoidHomClass F α β
f₁ f₂ : ι → Set α
a✝ : List ι
hf : ∀ (i : ι), i ∈ Quotient.mk (List.isSetoid ι) a✝ → f₁ i ⊆ f₂ i
⊢ Multiset.prod (Multiset.map f₁ (Quotient.mk (List.isSetoid ι) a✝)) ⊆
    Multiset.prod (Multiset.map f₂ (Quotient.mk (List.isSetoid ι) a✝))
[PROOFSTEP]
simp_rw [Multiset.quot_mk_to_coe, Multiset.coe_map, Multiset.coe_prod]
[GOAL]
case h
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : MonoidHomClass F α β
f₁ f₂ : ι → Set α
a✝ : List ι
hf : ∀ (i : ι), i ∈ Quotient.mk (List.isSetoid ι) a✝ → f₁ i ⊆ f₂ i
⊢ List.prod (List.map f₁ a✝) ⊆ List.prod (List.map f₂ a✝)
[PROOFSTEP]
exact list_prod_subset_list_prod _ _ _ hf
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : MonoidHomClass F α β
l : Finset ι
S : ι → Set α
⊢ (fun f => ∏ i in l, f i) '' pi (↑l) S = ∏ i in l, S i
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : MonoidHomClass F α β
l : Finset ι
S : ι → Set α
x✝ : α
⊢ x✝ ∈ (fun f => ∏ i in l, f i) '' pi (↑l) S ↔ x✝ ∈ ∏ i in l, S i
[PROOFSTEP]
simp_rw [mem_finset_prod, mem_image, mem_pi, exists_prop, Finset.mem_coe]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝³ : CommMonoid α
inst✝² : CommMonoid β
inst✝¹ : MonoidHomClass F α β
inst✝ : Fintype ι
S : ι → Set α
⊢ (fun f => ∏ i : ι, f i) '' pi univ S = ∏ i : ι, S i
[PROOFSTEP]
simpa only [Finset.coe_univ] using image_finset_prod_pi Finset.univ S
