case nil
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
h✝ : f ∈ l
hl✝ : List.Pairwise Disjoint l
h : f ∈ []
hl : List.Pairwise Disjoint []
⊢ ∀ (x : α), x ∈ support f → ↑f x = ↑(List.prod []) x

case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
h✝ : f ∈ l
hl✝ : List.Pairwise Disjoint l
hd : Perm α
tl : List (Perm α)
IH : f ∈ tl → List.Pairwise Disjoint tl → ∀ (x : α), x ∈ support f → ↑f x = ↑(List.prod tl) x
h : f ∈ hd :: tl
hl : List.Pairwise Disjoint (hd :: tl)
⊢ ∀ (x : α), x ∈ support f → ↑f x = ↑(List.prod (hd :: tl)) x
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
h : f ∈ l
hl : List.Pairwise Disjoint l
⊢ ∀ (x : α), x ∈ support f → ↑f x = ↑(List.prod l) x
induction' l with hd tl IH
no goals
case nil
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
h✝ : f ∈ l
hl✝ : List.Pairwise Disjoint l
h : f ∈ []
hl : List.Pairwise Disjoint []
⊢ ∀ (x : α), x ∈ support f → ↑f x = ↑(List.prod []) x
simp at h
case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
h✝ : f ∈ l
hl✝ : List.Pairwise Disjoint l
hd : Perm α
tl : List (Perm α)
IH : f ∈ tl → List.Pairwise Disjoint tl → ∀ (x : α), x ∈ support f → ↑f x = ↑(List.prod tl) x
h : f ∈ hd :: tl
hl : List.Pairwise Disjoint (hd :: tl)
x : α
hx : x ∈ support f
⊢ ↑f x = ↑(List.prod (hd :: tl)) x
case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
h✝ : f ∈ l
hl✝ : List.Pairwise Disjoint l
hd : Perm α
tl : List (Perm α)
IH : f ∈ tl → List.Pairwise Disjoint tl → ∀ (x : α), x ∈ support f → ↑f x = ↑(List.prod tl) x
h : f ∈ hd :: tl
hl : List.Pairwise Disjoint (hd :: tl)
⊢ ∀ (x : α), x ∈ support f → ↑f x = ↑(List.prod (hd :: tl)) x
intro x hx
case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
h✝ : f ∈ l
hl✝ : List.Pairwise Disjoint l
hd : Perm α
tl : List (Perm α)
IH : f ∈ tl → List.Pairwise Disjoint tl → ∀ (x : α), x ∈ support f → ↑f x = ↑(List.prod tl) x
h : f ∈ hd :: tl
hl : (∀ (a' : Perm α), a' ∈ tl → Disjoint hd a') ∧ List.Pairwise Disjoint tl
x : α
hx : x ∈ support f
⊢ ↑f x = ↑(List.prod (hd :: tl)) x
case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
h✝ : f ∈ l
hl✝ : List.Pairwise Disjoint l
hd : Perm α
tl : List (Perm α)
IH : f ∈ tl → List.Pairwise Disjoint tl → ∀ (x : α), x ∈ support f → ↑f x = ↑(List.prod tl) x
h : f ∈ hd :: tl
hl : List.Pairwise Disjoint (hd :: tl)
x : α
hx : x ∈ support f
⊢ ↑f x = ↑(List.prod (hd :: tl)) x
rw [List.pairwise_cons] at hl
case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
h✝ : f ∈ l
hl✝ : List.Pairwise Disjoint l
hd : Perm α
tl : List (Perm α)
IH : f ∈ tl → List.Pairwise Disjoint tl → ∀ (x : α), x ∈ support f → ↑f x = ↑(List.prod tl) x
h : f = hd ∨ f ∈ tl
hl : (∀ (a' : Perm α), a' ∈ tl → Disjoint hd a') ∧ List.Pairwise Disjoint tl
x : α
hx : x ∈ support f
⊢ ↑f x = ↑(List.prod (hd :: tl)) x
case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
h✝ : f ∈ l
hl✝ : List.Pairwise Disjoint l
hd : Perm α
tl : List (Perm α)
IH : f ∈ tl → List.Pairwise Disjoint tl → ∀ (x : α), x ∈ support f → ↑f x = ↑(List.prod tl) x
h : f ∈ hd :: tl
hl : (∀ (a' : Perm α), a' ∈ tl → Disjoint hd a') ∧ List.Pairwise Disjoint tl
x : α
hx : x ∈ support f
⊢ ↑f x = ↑(List.prod (hd :: tl)) x
rw [List.mem_cons] at h
case cons.inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
h : f ∈ l
hl✝ : List.Pairwise Disjoint l
tl : List (Perm α)
IH : f ∈ tl → List.Pairwise Disjoint tl → ∀ (x : α), x ∈ support f → ↑f x = ↑(List.prod tl) x
x : α
hx : x ∈ support f
hl : (∀ (a' : Perm α), a' ∈ tl → Disjoint f a') ∧ List.Pairwise Disjoint tl
⊢ ↑f x = ↑(List.prod (f :: tl)) x

case cons.inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
h✝ : f ∈ l
hl✝ : List.Pairwise Disjoint l
hd : Perm α
tl : List (Perm α)
IH : f ∈ tl → List.Pairwise Disjoint tl → ∀ (x : α), x ∈ support f → ↑f x = ↑(List.prod tl) x
hl : (∀ (a' : Perm α), a' ∈ tl → Disjoint hd a') ∧ List.Pairwise Disjoint tl
x : α
hx : x ∈ support f
h : f ∈ tl
⊢ ↑f x = ↑(List.prod (hd :: tl)) x
case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
h✝ : f ∈ l
hl✝ : List.Pairwise Disjoint l
hd : Perm α
tl : List (Perm α)
IH : f ∈ tl → List.Pairwise Disjoint tl → ∀ (x : α), x ∈ support f → ↑f x = ↑(List.prod tl) x
h : f = hd ∨ f ∈ tl
hl : (∀ (a' : Perm α), a' ∈ tl → Disjoint hd a') ∧ List.Pairwise Disjoint tl
x : α
hx : x ∈ support f
⊢ ↑f x = ↑(List.prod (hd :: tl)) x
rcases h with (rfl | h)
no goals
case cons.inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
h : f ∈ l
hl✝ : List.Pairwise Disjoint l
tl : List (Perm α)
IH : f ∈ tl → List.Pairwise Disjoint tl → ∀ (x : α), x ∈ support f → ↑f x = ↑(List.prod tl) x
x : α
hx : x ∈ support f
hl : (∀ (a' : Perm α), a' ∈ tl → Disjoint f a') ∧ List.Pairwise Disjoint tl
⊢ ↑f x = ↑(List.prod (f :: tl)) x
rw [List.prod_cons, mul_apply,
  not_mem_support.mp ((disjoint_prod_right tl hl.left).mem_imp hx)]
case cons.inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
h✝ : f ∈ l
hl✝ : List.Pairwise Disjoint l
hd : Perm α
tl : List (Perm α)
IH : f ∈ tl → List.Pairwise Disjoint tl → ∀ (x : α), x ∈ support f → ↑f x = ↑(List.prod tl) x
hl : (∀ (a' : Perm α), a' ∈ tl → Disjoint hd a') ∧ List.Pairwise Disjoint tl
x : α
hx : x ∈ support f
h : f ∈ tl
⊢ ¬↑f x ∈ support hd
case cons.inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
h✝ : f ∈ l
hl✝ : List.Pairwise Disjoint l
hd : Perm α
tl : List (Perm α)
IH : f ∈ tl → List.Pairwise Disjoint tl → ∀ (x : α), x ∈ support f → ↑f x = ↑(List.prod tl) x
hl : (∀ (a' : Perm α), a' ∈ tl → Disjoint hd a') ∧ List.Pairwise Disjoint tl
x : α
hx : x ∈ support f
h : f ∈ tl
⊢ ↑f x = ↑(List.prod (hd :: tl)) x
rw [List.prod_cons, mul_apply, ← IH h hl.right _ hx, eq_comm, ← not_mem_support]
case cons.inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
h✝ : f ∈ l
hl✝ : List.Pairwise Disjoint l
hd : Perm α
tl : List (Perm α)
IH : f ∈ tl → List.Pairwise Disjoint tl → ∀ (x : α), x ∈ support f → ↑f x = ↑(List.prod tl) x
hl : (∀ (a' : Perm α), a' ∈ tl → Disjoint hd a') ∧ List.Pairwise Disjoint tl
x : α
hx : x ∈ support f
h : f ∈ tl
⊢ ↑f x ∈ support f
case cons.inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
h✝ : f ∈ l
hl✝ : List.Pairwise Disjoint l
hd : Perm α
tl : List (Perm α)
IH : f ∈ tl → List.Pairwise Disjoint tl → ∀ (x : α), x ∈ support f → ↑f x = ↑(List.prod tl) x
hl : (∀ (a' : Perm α), a' ∈ tl → Disjoint hd a') ∧ List.Pairwise Disjoint tl
x : α
hx : x ∈ support f
h : f ∈ tl
⊢ ¬↑f x ∈ support hd
refine' (hl.left _ h).symm.mem_imp _
no goals
case cons.inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
h✝ : f ∈ l
hl✝ : List.Pairwise Disjoint l
hd : Perm α
tl : List (Perm α)
IH : f ∈ tl → List.Pairwise Disjoint tl → ∀ (x : α), x ∈ support f → ↑f x = ↑(List.prod tl) x
hl : (∀ (a' : Perm α), a' ∈ tl → Disjoint hd a') ∧ List.Pairwise Disjoint tl
x : α
hx : x ∈ support f
h : f ∈ tl
⊢ ↑f x ∈ support f
simpa using hx