case nil
ι : Type u_1
α : Type u_2
β : Type ?u.67083
F : Type ?u.67086
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 [])

case cons
ι : Type u_1
α : Type u_2
β : Type ?u.67083
F : Type ?u.67086
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))
ι : Type u_1
α : Type u_2
β : Type ?u.67083
F : Type ?u.67086
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)
induction' t with h tl ih
no goals
case nil
ι : Type u_1
α : Type u_2
β : Type ?u.67083
F : Type ?u.67086
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 [])
simp_rw [List.map_nil, List.prod_nil, Set.mem_one]
case cons
ι : Type u_1
α : Type u_2
β : Type ?u.67083
F : Type ?u.67086
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)
case cons
ι : Type u_1
α : Type u_2
β : Type ?u.67083
F : Type ?u.67086
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))
simp_rw [List.map_cons, List.prod_cons]
no goals
case cons
ι : Type u_1
α : Type u_2
β : Type ?u.67083
F : Type ?u.67086
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)
exact mul_mem_mul (hg h <| List.mem_cons_self _ _)
  (ih fun i hi ↦ hg i <| List.mem_cons_of_mem _ hi)