case nil
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
h✝ : List.Pairwise Disjoint l
h : List.Pairwise Disjoint []
⊢ 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 : Perm α
l : List (Perm α)
h✝ : List.Pairwise Disjoint l
hd : Perm α
tl : List (Perm α)
hl : List.Pairwise Disjoint tl → support (List.prod tl) = List.foldr (fun x x_1 => x ⊔ x_1) ⊥ (List.map support tl)
h : List.Pairwise Disjoint (hd :: 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 α)
h : List.Pairwise Disjoint l
⊢ 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 α
l : List (Perm α)
h✝ : List.Pairwise Disjoint l
h : List.Pairwise Disjoint []
⊢ 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 : Perm α
l : List (Perm α)
h✝ : List.Pairwise Disjoint l
hd : Perm α
tl : List (Perm α)
hl : List.Pairwise Disjoint tl → support (List.prod tl) = List.foldr (fun x x_1 => x ⊔ x_1) ⊥ (List.map support tl)
h : (∀ (a' : Perm α), a' ∈ tl → Disjoint hd a') ∧ List.Pairwise Disjoint tl
⊢ support (List.prod (hd :: tl)) = List.foldr (fun x x_1 => x ⊔ x_1) ⊥ (List.map support (hd :: tl))
case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
h✝ : List.Pairwise Disjoint l
hd : Perm α
tl : List (Perm α)
hl : List.Pairwise Disjoint tl → support (List.prod tl) = List.foldr (fun x x_1 => x ⊔ x_1) ⊥ (List.map support tl)
h : List.Pairwise Disjoint (hd :: tl)
⊢ support (List.prod (hd :: tl)) = List.foldr (fun x x_1 => x ⊔ x_1) ⊥ (List.map support (hd :: tl))
rw [List.pairwise_cons] at h
case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
h✝ : List.Pairwise Disjoint l
hd : Perm α
tl : List (Perm α)
hl : List.Pairwise Disjoint tl → support (List.prod tl) = List.foldr (fun x x_1 => x ⊔ x_1) ⊥ (List.map support tl)
h : (∀ (a' : Perm α), a' ∈ tl → Disjoint hd a') ∧ List.Pairwise Disjoint tl
this : Disjoint hd (List.prod tl)
⊢ support (List.prod (hd :: tl)) = List.foldr (fun x x_1 => x ⊔ x_1) ⊥ (List.map support (hd :: tl))
case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
h✝ : List.Pairwise Disjoint l
hd : Perm α
tl : List (Perm α)
hl : List.Pairwise Disjoint tl → support (List.prod tl) = List.foldr (fun x x_1 => x ⊔ x_1) ⊥ (List.map support tl)
h : (∀ (a' : Perm α), a' ∈ tl → Disjoint hd a') ∧ List.Pairwise Disjoint tl
⊢ support (List.prod (hd :: tl)) = List.foldr (fun x x_1 => x ⊔ x_1) ⊥ (List.map support (hd :: tl))
have : Disjoint hd tl.prod := disjoint_prod_right _ h.left
no goals
case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
h✝ : List.Pairwise Disjoint l
hd : Perm α
tl : List (Perm α)
hl : List.Pairwise Disjoint tl → support (List.prod tl) = List.foldr (fun x x_1 => x ⊔ x_1) ⊥ (List.map support tl)
h : (∀ (a' : Perm α), a' ∈ tl → Disjoint hd a') ∧ List.Pairwise Disjoint tl
this : Disjoint hd (List.prod tl)
⊢ support (List.prod (hd :: tl)) = List.foldr (fun x x_1 => x ⊔ x_1) ⊥ (List.map support (hd :: tl))
simp [this.support_mul, hl h.right]