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

case cons
ι : Type u_1
α : Type u_2
β : Type ?u.71424
F : Type ?u.71427
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))
ι : Type u_1
α : Type u_2
β : Type ?u.71424
F : Type ?u.71427
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)
induction' t with h tl ih
no goals
case nil
ι : Type u_1
α : Type u_2
β : Type ?u.71424
F : Type ?u.71427
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₂ [])
rfl
case cons
ι : Type u_1
α : Type u_2
β : Type ?u.71424
F : Type ?u.71427
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)
case cons
ι : Type u_1
α : Type u_2
β : Type ?u.71424
F : Type ?u.71427
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))
simp_rw [List.map_cons, List.prod_cons]
no goals
case cons
ι : Type u_1
α : Type u_2
β : Type ?u.71424
F : Type ?u.71427
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)
exact mul_subset_mul (hf h <| List.mem_cons_self _ _)
  (ih fun i hi ↦ hf i <| List.mem_cons_of_mem _ hi)