case nil
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
⊢ support (List.prod []) ≤ List.foldr (fun x x_1 => x ⊔ x_1) ⊥ (List.map support [])

case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g hd : Perm α
tl : List (Perm α)
hl : support (List.prod tl) ≤ List.foldr (fun x x_1 => x ⊔ x_1) ⊥ (List.map support tl)
⊢ support (List.prod (hd :: tl)) ≤ List.foldr (fun x x_1 => x ⊔ x_1) ⊥ (List.map support (hd :: tl))
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
⊢ support (List.prod l) ≤ List.foldr (fun x x_1 => x ⊔ x_1) ⊥ (List.map support l)
induction' l with hd tl hl
no goals
case nil
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
⊢ support (List.prod []) ≤ List.foldr (fun x x_1 => x ⊔ x_1) ⊥ (List.map support [])
simp
case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g hd : Perm α
tl : List (Perm α)
hl : support (List.prod tl) ≤ List.foldr (fun x x_1 => x ⊔ x_1) ⊥ (List.map support tl)
⊢ support (hd * List.prod tl) ≤ support hd ⊔ List.foldr (fun x x_1 => x ⊔ x_1) ⊥ (List.map support tl)
case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g hd : Perm α
tl : List (Perm α)
hl : support (List.prod tl) ≤ List.foldr (fun x x_1 => x ⊔ x_1) ⊥ (List.map support tl)
⊢ support (List.prod (hd :: tl)) ≤ List.foldr (fun x x_1 => x ⊔ x_1) ⊥ (List.map support (hd :: tl))
rw [List.prod_cons, List.map_cons, List.foldr_cons]
case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g hd : Perm α
tl : List (Perm α)
hl : support (List.prod tl) ≤ List.foldr (fun x x_1 => x ⊔ x_1) ⊥ (List.map support tl)
⊢ support hd ⊔ support (List.prod tl) ≤ support hd ⊔ List.foldr (fun x x_1 => x ⊔ x_1) ⊥ (List.map support tl)
case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g hd : Perm α
tl : List (Perm α)
hl : support (List.prod tl) ≤ List.foldr (fun x x_1 => x ⊔ x_1) ⊥ (List.map support tl)
⊢ support (hd * List.prod tl) ≤ support hd ⊔ List.foldr (fun x x_1 => x ⊔ x_1) ⊥ (List.map support tl)
refine' (support_mul_le hd tl.prod).trans _
no goals
case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g hd : Perm α
tl : List (Perm α)
hl : support (List.prod tl) ≤ List.foldr (fun x x_1 => x ⊔ x_1) ⊥ (List.map support tl)
⊢ support hd ⊔ support (List.prod tl) ≤ support hd ⊔ List.foldr (fun x x_1 => x ⊔ x_1) ⊥ (List.map support tl)
exact sup_le_sup le_rfl hl