[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ x : α
l : List α
h : ¬x ∈ l
⊢ ↑(formPerm l) x = x
[PROOFSTEP]
cases' l with y l
[GOAL]
case nil
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l : List α
x✝ x : α
h : ¬x ∈ []
⊢ ↑(formPerm []) x = x
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
h : ¬x ∈ y :: l
⊢ ↑(formPerm (y :: l)) x = x
[PROOFSTEP]
induction' l with z l IH generalizing x y
[GOAL]
case cons.nil
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝¹ x✝ y✝ : α
l : List α
h✝ : ¬x✝ ∈ y✝ :: l
x y : α
h : ¬x ∈ [y]
⊢ ↑(formPerm [y]) x = x
[PROOFSTEP]
simp
[GOAL]
case cons.cons
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ x✝ y✝ : α
l✝ : List α
h✝ : ¬x✝ ∈ y✝ :: l✝
z : α
l : List α
IH : ∀ (x y : α), ¬x ∈ y :: l → ↑(formPerm (y :: l)) x = x
x y : α
h : ¬x ∈ y :: z :: l
⊢ ↑(formPerm (y :: z :: l)) x = x
[PROOFSTEP]
specialize IH x z (mt (mem_cons_of_mem y) h)
[GOAL]
case cons.cons
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ x✝ y✝ : α
l✝ : List α
h✝ : ¬x✝ ∈ y✝ :: l✝
z : α
l : List α
x y : α
h : ¬x ∈ y :: z :: l
IH : ↑(formPerm (z :: l)) x = x
⊢ ↑(formPerm (y :: z :: l)) x = x
[PROOFSTEP]
simp only [not_or, mem_cons] at h
[GOAL]
case cons.cons
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ x✝ y✝ : α
l✝ : List α
h✝ : ¬x✝ ∈ y✝ :: l✝
z : α
l : List α
x y : α
IH : ↑(formPerm (z :: l)) x = x
h : ¬x = y ∧ ¬x = z ∧ ¬x ∈ l
⊢ ↑(formPerm (y :: z :: l)) x = x
[PROOFSTEP]
simp [IH, swap_apply_of_ne_of_ne, h]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ x : α
l : List α
h : x ∈ l
⊢ ↑(formPerm l) x ∈ l
[PROOFSTEP]
cases' l with y l
[GOAL]
case nil
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l : List α
x✝ x : α
h : x ∈ []
⊢ ↑(formPerm []) x ∈ []
[PROOFSTEP]
simp at h
[GOAL]
case cons
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
h : x ∈ y :: l
⊢ ↑(formPerm (y :: l)) x ∈ y :: l
[PROOFSTEP]
induction' l with z l IH generalizing x y
[GOAL]
case cons.nil
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝¹ x✝ y✝ : α
l : List α
h✝ : x✝ ∈ y✝ :: l
x y : α
h : x ∈ [y]
⊢ ↑(formPerm [y]) x ∈ [y]
[PROOFSTEP]
simpa using h
[GOAL]
case cons.cons
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ x✝ y✝ : α
l✝ : List α
h✝ : x✝ ∈ y✝ :: l✝
z : α
l : List α
IH : ∀ (x y : α), x ∈ y :: l → ↑(formPerm (y :: l)) x ∈ y :: l
x y : α
h : x ∈ y :: z :: l
⊢ ↑(formPerm (y :: z :: l)) x ∈ y :: z :: l
[PROOFSTEP]
by_cases hx : x ∈ z :: l
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ x✝ y✝ : α
l✝ : List α
h✝ : x✝ ∈ y✝ :: l✝
z : α
l : List α
IH : ∀ (x y : α), x ∈ y :: l → ↑(formPerm (y :: l)) x ∈ y :: l
x y : α
h : x ∈ y :: z :: l
hx : x ∈ z :: l
⊢ ↑(formPerm (y :: z :: l)) x ∈ y :: z :: l
[PROOFSTEP]
rw [formPerm_cons_cons, mul_apply, swap_apply_def]
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ x✝ y✝ : α
l✝ : List α
h✝ : x✝ ∈ y✝ :: l✝
z : α
l : List α
IH : ∀ (x y : α), x ∈ y :: l → ↑(formPerm (y :: l)) x ∈ y :: l
x y : α
h : x ∈ y :: z :: l
hx : x ∈ z :: l
⊢ (if ↑(formPerm (z :: l)) x = y then z else if ↑(formPerm (z :: l)) x = z then y else ↑(formPerm (z :: l)) x) ∈
    y :: z :: l
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ x✝ y✝ : α
l✝ : List α
h✝¹ : x✝ ∈ y✝ :: l✝
z : α
l : List α
IH : ∀ (x y : α), x ∈ y :: l → ↑(formPerm (y :: l)) x ∈ y :: l
x y : α
h : x ∈ y :: z :: l
hx : x ∈ z :: l
h✝ : ↑(formPerm (z :: l)) x = y
⊢ z ∈ y :: z :: l
[PROOFSTEP]
simp [IH _ _ hx]
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ x✝ y✝ : α
l✝ : List α
h✝² : x✝ ∈ y✝ :: l✝
z : α
l : List α
IH : ∀ (x y : α), x ∈ y :: l → ↑(formPerm (y :: l)) x ∈ y :: l
x y : α
h : x ∈ y :: z :: l
hx : x ∈ z :: l
h✝¹ : ¬↑(formPerm (z :: l)) x = y
h✝ : ↑(formPerm (z :: l)) x = z
⊢ y ∈ y :: z :: l
[PROOFSTEP]
simp
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ x✝ y✝ : α
l✝ : List α
h✝² : x✝ ∈ y✝ :: l✝
z : α
l : List α
IH : ∀ (x y : α), x ∈ y :: l → ↑(formPerm (y :: l)) x ∈ y :: l
x y : α
h : x ∈ y :: z :: l
hx : x ∈ z :: l
h✝¹ : ¬↑(formPerm (z :: l)) x = y
h✝ : ¬↑(formPerm (z :: l)) x = z
⊢ ↑(formPerm (z :: l)) x ∈ y :: z :: l
[PROOFSTEP]
simpa [*] using IH _ _ hx
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ x✝ y✝ : α
l✝ : List α
h✝ : x✝ ∈ y✝ :: l✝
z : α
l : List α
IH : ∀ (x y : α), x ∈ y :: l → ↑(formPerm (y :: l)) x ∈ y :: l
x y : α
h : x ∈ y :: z :: l
hx : ¬x ∈ z :: l
⊢ ↑(formPerm (y :: z :: l)) x ∈ y :: z :: l
[PROOFSTEP]
replace h : x = y := Or.resolve_right (mem_cons.1 h) hx
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ x✝ y✝ : α
l✝ : List α
h✝ : x✝ ∈ y✝ :: l✝
z : α
l : List α
IH : ∀ (x y : α), x ∈ y :: l → ↑(formPerm (y :: l)) x ∈ y :: l
x y : α
hx : ¬x ∈ z :: l
h : x = y
⊢ ↑(formPerm (y :: z :: l)) x ∈ y :: z :: l
[PROOFSTEP]
simp [formPerm_apply_of_not_mem _ _ hx, ← h]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ x : α
l : List α
h : ↑(formPerm l) x ∈ l
⊢ x ∈ l
[PROOFSTEP]
cases' l with y l
[GOAL]
case nil
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l : List α
x✝ x : α
h : ↑(formPerm []) x ∈ []
⊢ x ∈ []
[PROOFSTEP]
simp at h
[GOAL]
case cons
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
h : ↑(formPerm (y :: l)) x ∈ y :: l
⊢ x ∈ y :: l
[PROOFSTEP]
induction' l with z l IH generalizing x y
[GOAL]
case cons.nil
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝¹ x✝ y✝ : α
l : List α
h✝ : ↑(formPerm (y✝ :: l)) x✝ ∈ y✝ :: l
x y : α
h : ↑(formPerm [y]) x ∈ [y]
⊢ x ∈ [y]
[PROOFSTEP]
simpa using h
[GOAL]
case cons.cons
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ x✝ y✝ : α
l✝ : List α
h✝ : ↑(formPerm (y✝ :: l✝)) x✝ ∈ y✝ :: l✝
z : α
l : List α
IH : ∀ (x y : α), ↑(formPerm (y :: l)) x ∈ y :: l → x ∈ y :: l
x y : α
h : ↑(formPerm (y :: z :: l)) x ∈ y :: z :: l
⊢ x ∈ y :: z :: l
[PROOFSTEP]
by_cases hx : (z :: l).formPerm x ∈ z :: l
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ x✝ y✝ : α
l✝ : List α
h✝ : ↑(formPerm (y✝ :: l✝)) x✝ ∈ y✝ :: l✝
z : α
l : List α
IH : ∀ (x y : α), ↑(formPerm (y :: l)) x ∈ y :: l → x ∈ y :: l
x y : α
h : ↑(formPerm (y :: z :: l)) x ∈ y :: z :: l
hx : ↑(formPerm (z :: l)) x ∈ z :: l
⊢ x ∈ y :: z :: l
[PROOFSTEP]
rw [List.formPerm_cons_cons, mul_apply, swap_apply_def] at h
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ x✝ y✝ : α
l✝ : List α
h✝ : ↑(formPerm (y✝ :: l✝)) x✝ ∈ y✝ :: l✝
z : α
l : List α
IH : ∀ (x y : α), ↑(formPerm (y :: l)) x ∈ y :: l → x ∈ y :: l
x y : α
h :
  (if ↑(formPerm (z :: l)) x = y then z else if ↑(formPerm (z :: l)) x = z then y else ↑(formPerm (z :: l)) x) ∈
    y :: z :: l
hx : ↑(formPerm (z :: l)) x ∈ z :: l
⊢ x ∈ y :: z :: l
[PROOFSTEP]
split_ifs at h
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ x✝ y✝ : α
l✝ : List α
h✝¹ : ↑(formPerm (y✝ :: l✝)) x✝ ∈ y✝ :: l✝
z : α
l : List α
IH : ∀ (x y : α), ↑(formPerm (y :: l)) x ∈ y :: l → x ∈ y :: l
x y : α
hx : ↑(formPerm (z :: l)) x ∈ z :: l
h✝ : ↑(formPerm (z :: l)) x = y
h : z ∈ y :: z :: l
⊢ x ∈ y :: z :: l
[PROOFSTEP]
aesop
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ x✝ y✝ : α
l✝ : List α
h✝² : ↑(formPerm (y✝ :: l✝)) x✝ ∈ y✝ :: l✝
z : α
l : List α
IH : ∀ (x y : α), ↑(formPerm (y :: l)) x ∈ y :: l → x ∈ y :: l
x y : α
hx : ↑(formPerm (z :: l)) x ∈ z :: l
h✝¹ : ¬↑(formPerm (z :: l)) x = y
h✝ : ↑(formPerm (z :: l)) x = z
h : y ∈ y :: z :: l
⊢ x ∈ y :: z :: l
[PROOFSTEP]
aesop
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ x✝ y✝ : α
l✝ : List α
h✝² : ↑(formPerm (y✝ :: l✝)) x✝ ∈ y✝ :: l✝
z : α
l : List α
IH : ∀ (x y : α), ↑(formPerm (y :: l)) x ∈ y :: l → x ∈ y :: l
x y : α
hx : ↑(formPerm (z :: l)) x ∈ z :: l
h✝¹ : ¬↑(formPerm (z :: l)) x = y
h✝ : ¬↑(formPerm (z :: l)) x = z
h : ↑(formPerm (z :: l)) x ∈ y :: z :: l
⊢ x ∈ y :: z :: l
[PROOFSTEP]
aesop
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ x✝ y✝ : α
l✝ : List α
h✝ : ↑(formPerm (y✝ :: l✝)) x✝ ∈ y✝ :: l✝
z : α
l : List α
IH : ∀ (x y : α), ↑(formPerm (y :: l)) x ∈ y :: l → x ∈ y :: l
x y : α
h : ↑(formPerm (y :: z :: l)) x ∈ y :: z :: l
hx : ¬↑(formPerm (z :: l)) x ∈ z :: l
⊢ x ∈ y :: z :: l
[PROOFSTEP]
replace hx := (Function.Injective.eq_iff (Equiv.injective _)).mp (List.formPerm_apply_of_not_mem _ _ hx)
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ x✝ y✝ : α
l✝ : List α
h✝ : ↑(formPerm (y✝ :: l✝)) x✝ ∈ y✝ :: l✝
z : α
l : List α
IH : ∀ (x y : α), ↑(formPerm (y :: l)) x ∈ y :: l → x ∈ y :: l
x y : α
h : ↑(formPerm (y :: z :: l)) x ∈ y :: z :: l
hx : ↑(formPerm (z :: l)) x = x
⊢ x ∈ y :: z :: l
[PROOFSTEP]
simp only [List.formPerm_cons_cons, hx, Equiv.Perm.coe_mul, Function.comp_apply, List.mem_cons, swap_apply_def,
  ite_eq_left_iff] at h
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ x✝ y✝ : α
l✝ : List α
h✝ : ↑(formPerm (y✝ :: l✝)) x✝ ∈ y✝ :: l✝
z : α
l : List α
IH : ∀ (x y : α), ↑(formPerm (y :: l)) x ∈ y :: l → x ∈ y :: l
x y : α
hx : ↑(formPerm (z :: l)) x = x
h :
  (if x = y then z else if x = z then y else x) = y ∨
    (¬x = y → (if x = z then y else x) = z) ∨ (if x = y then z else if x = z then y else x) ∈ l
⊢ x ∈ y :: z :: l
[PROOFSTEP]
simp only [List.mem_cons]
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ x✝ y✝ : α
l✝ : List α
h✝ : ↑(formPerm (y✝ :: l✝)) x✝ ∈ y✝ :: l✝
z : α
l : List α
IH : ∀ (x y : α), ↑(formPerm (y :: l)) x ∈ y :: l → x ∈ y :: l
x y : α
hx : ↑(formPerm (z :: l)) x = x
h :
  (if x = y then z else if x = z then y else x) = y ∨
    (¬x = y → (if x = z then y else x) = z) ∨ (if x = y then z else if x = z then y else x) ∈ l
⊢ x = y ∨ x = z ∨ x ∈ l
[PROOFSTEP]
rcases h with h | h | h
[GOAL]
case neg.inl
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ x✝ y✝ : α
l✝ : List α
h✝ : ↑(formPerm (y✝ :: l✝)) x✝ ∈ y✝ :: l✝
z : α
l : List α
IH : ∀ (x y : α), ↑(formPerm (y :: l)) x ∈ y :: l → x ∈ y :: l
x y : α
hx : ↑(formPerm (z :: l)) x = x
h : (if x = y then z else if x = z then y else x) = y
⊢ x = y ∨ x = z ∨ x ∈ l
[PROOFSTEP]
split_ifs at h  with h1
[GOAL]
case neg.inr.inl
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ x✝ y✝ : α
l✝ : List α
h✝ : ↑(formPerm (y✝ :: l✝)) x✝ ∈ y✝ :: l✝
z : α
l : List α
IH : ∀ (x y : α), ↑(formPerm (y :: l)) x ∈ y :: l → x ∈ y :: l
x y : α
hx : ↑(formPerm (z :: l)) x = x
h : ¬x = y → (if x = z then y else x) = z
⊢ x = y ∨ x = z ∨ x ∈ l
[PROOFSTEP]
split_ifs at h  with h1
[GOAL]
case neg.inr.inr
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ x✝ y✝ : α
l✝ : List α
h✝ : ↑(formPerm (y✝ :: l✝)) x✝ ∈ y✝ :: l✝
z : α
l : List α
IH : ∀ (x y : α), ↑(formPerm (y :: l)) x ∈ y :: l → x ∈ y :: l
x y : α
hx : ↑(formPerm (z :: l)) x = x
h : (if x = y then z else if x = z then y else x) ∈ l
⊢ x = y ∨ x = z ∨ x ∈ l
[PROOFSTEP]
split_ifs at h  with h1
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ x✝ y✝ : α
l✝ : List α
h✝ : ↑(formPerm (y✝ :: l✝)) x✝ ∈ y✝ :: l✝
z : α
l : List α
IH : ∀ (x y : α), ↑(formPerm (y :: l)) x ∈ y :: l → x ∈ y :: l
x y : α
hx : ↑(formPerm (z :: l)) x = x
h1 : x = y
h : z = y
⊢ x = y ∨ x = z ∨ x ∈ l
[PROOFSTEP]
try {aesop
}
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ x✝ y✝ : α
l✝ : List α
h✝ : ↑(formPerm (y✝ :: l✝)) x✝ ∈ y✝ :: l✝
z : α
l : List α
IH : ∀ (x y : α), ↑(formPerm (y :: l)) x ∈ y :: l → x ∈ y :: l
x y : α
hx : ↑(formPerm (z :: l)) x = x
h1 : x = y
h : z = y
⊢ x = y ∨ x = z ∨ x ∈ l
[PROOFSTEP]
{aesop
}
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ x✝ y✝ : α
l✝ : List α
h✝ : ↑(formPerm (y✝ :: l✝)) x✝ ∈ y✝ :: l✝
z : α
l : List α
IH : ∀ (x y : α), ↑(formPerm (y :: l)) x ∈ y :: l → x ∈ y :: l
x y : α
hx : ↑(formPerm (z :: l)) x = x
h1 : x = y
h : z = y
⊢ x = y ∨ x = z ∨ x ∈ l
[PROOFSTEP]
aesop
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ x✝ y✝ : α
l✝ : List α
h✝¹ : ↑(formPerm (y✝ :: l✝)) x✝ ∈ y✝ :: l✝
z : α
l : List α
IH : ∀ (x y : α), ↑(formPerm (y :: l)) x ∈ y :: l → x ∈ y :: l
x y : α
hx : ↑(formPerm (z :: l)) x = x
h1 : ¬x = y
h✝ : x = z
h : y = y
⊢ x = y ∨ x = z ∨ x ∈ l
[PROOFSTEP]
try {aesop
}
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ x✝ y✝ : α
l✝ : List α
h✝¹ : ↑(formPerm (y✝ :: l✝)) x✝ ∈ y✝ :: l✝
z : α
l : List α
IH : ∀ (x y : α), ↑(formPerm (y :: l)) x ∈ y :: l → x ∈ y :: l
x y : α
hx : ↑(formPerm (z :: l)) x = x
h1 : ¬x = y
h✝ : x = z
h : y = y
⊢ x = y ∨ x = z ∨ x ∈ l
[PROOFSTEP]
{aesop
}
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ x✝ y✝ : α
l✝ : List α
h✝¹ : ↑(formPerm (y✝ :: l✝)) x✝ ∈ y✝ :: l✝
z : α
l : List α
IH : ∀ (x y : α), ↑(formPerm (y :: l)) x ∈ y :: l → x ∈ y :: l
x y : α
hx : ↑(formPerm (z :: l)) x = x
h1 : ¬x = y
h✝ : x = z
h : y = y
⊢ x = y ∨ x = z ∨ x ∈ l
[PROOFSTEP]
aesop
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ x✝ y✝ : α
l✝ : List α
h✝¹ : ↑(formPerm (y✝ :: l✝)) x✝ ∈ y✝ :: l✝
z : α
l : List α
IH : ∀ (x y : α), ↑(formPerm (y :: l)) x ∈ y :: l → x ∈ y :: l
x y : α
hx : ↑(formPerm (z :: l)) x = x
h1 : ¬x = y
h✝ : ¬x = z
h : x = y
⊢ x = y ∨ x = z ∨ x ∈ l
[PROOFSTEP]
try {aesop
}
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ x✝ y✝ : α
l✝ : List α
h✝¹ : ↑(formPerm (y✝ :: l✝)) x✝ ∈ y✝ :: l✝
z : α
l : List α
IH : ∀ (x y : α), ↑(formPerm (y :: l)) x ∈ y :: l → x ∈ y :: l
x y : α
hx : ↑(formPerm (z :: l)) x = x
h1 : ¬x = y
h✝ : ¬x = z
h : x = y
⊢ x = y ∨ x = z ∨ x ∈ l
[PROOFSTEP]
{aesop
}
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ x✝ y✝ : α
l✝ : List α
h✝¹ : ↑(formPerm (y✝ :: l✝)) x✝ ∈ y✝ :: l✝
z : α
l : List α
IH : ∀ (x y : α), ↑(formPerm (y :: l)) x ∈ y :: l → x ∈ y :: l
x y : α
hx : ↑(formPerm (z :: l)) x = x
h1 : ¬x = y
h✝ : ¬x = z
h : x = y
⊢ x = y ∨ x = z ∨ x ∈ l
[PROOFSTEP]
aesop
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ x✝ y✝ : α
l✝ : List α
h✝ : ↑(formPerm (y✝ :: l✝)) x✝ ∈ y✝ :: l✝
z : α
l : List α
IH : ∀ (x y : α), ↑(formPerm (y :: l)) x ∈ y :: l → x ∈ y :: l
x y : α
hx : ↑(formPerm (z :: l)) x = x
h1 : x = z
h : ¬x = y → y = z
⊢ x = y ∨ x = z ∨ x ∈ l
[PROOFSTEP]
try {aesop
}
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ x✝ y✝ : α
l✝ : List α
h✝ : ↑(formPerm (y✝ :: l✝)) x✝ ∈ y✝ :: l✝
z : α
l : List α
IH : ∀ (x y : α), ↑(formPerm (y :: l)) x ∈ y :: l → x ∈ y :: l
x y : α
hx : ↑(formPerm (z :: l)) x = x
h1 : x = z
h : ¬x = y → y = z
⊢ x = y ∨ x = z ∨ x ∈ l
[PROOFSTEP]
{aesop
}
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ x✝ y✝ : α
l✝ : List α
h✝ : ↑(formPerm (y✝ :: l✝)) x✝ ∈ y✝ :: l✝
z : α
l : List α
IH : ∀ (x y : α), ↑(formPerm (y :: l)) x ∈ y :: l → x ∈ y :: l
x y : α
hx : ↑(formPerm (z :: l)) x = x
h1 : x = z
h : ¬x = y → y = z
⊢ x = y ∨ x = z ∨ x ∈ l
[PROOFSTEP]
aesop
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ x✝ y✝ : α
l✝ : List α
h✝ : ↑(formPerm (y✝ :: l✝)) x✝ ∈ y✝ :: l✝
z : α
l : List α
IH : ∀ (x y : α), ↑(formPerm (y :: l)) x ∈ y :: l → x ∈ y :: l
x y : α
hx : ↑(formPerm (z :: l)) x = x
h1 : ¬x = z
h : ¬x = y → x = z
⊢ x = y ∨ x = z ∨ x ∈ l
[PROOFSTEP]
try {aesop
}
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ x✝ y✝ : α
l✝ : List α
h✝ : ↑(formPerm (y✝ :: l✝)) x✝ ∈ y✝ :: l✝
z : α
l : List α
IH : ∀ (x y : α), ↑(formPerm (y :: l)) x ∈ y :: l → x ∈ y :: l
x y : α
hx : ↑(formPerm (z :: l)) x = x
h1 : ¬x = z
h : ¬x = y → x = z
⊢ x = y ∨ x = z ∨ x ∈ l
[PROOFSTEP]
{aesop
}
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ x✝ y✝ : α
l✝ : List α
h✝ : ↑(formPerm (y✝ :: l✝)) x✝ ∈ y✝ :: l✝
z : α
l : List α
IH : ∀ (x y : α), ↑(formPerm (y :: l)) x ∈ y :: l → x ∈ y :: l
x y : α
hx : ↑(formPerm (z :: l)) x = x
h1 : ¬x = z
h : ¬x = y → x = z
⊢ x = y ∨ x = z ∨ x ∈ l
[PROOFSTEP]
aesop
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ x✝ y✝ : α
l✝ : List α
h✝ : ↑(formPerm (y✝ :: l✝)) x✝ ∈ y✝ :: l✝
z : α
l : List α
IH : ∀ (x y : α), ↑(formPerm (y :: l)) x ∈ y :: l → x ∈ y :: l
x y : α
hx : ↑(formPerm (z :: l)) x = x
h1 : x = y
h : z ∈ l
⊢ x = y ∨ x = z ∨ x ∈ l
[PROOFSTEP]
try {aesop
}
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ x✝ y✝ : α
l✝ : List α
h✝ : ↑(formPerm (y✝ :: l✝)) x✝ ∈ y✝ :: l✝
z : α
l : List α
IH : ∀ (x y : α), ↑(formPerm (y :: l)) x ∈ y :: l → x ∈ y :: l
x y : α
hx : ↑(formPerm (z :: l)) x = x
h1 : x = y
h : z ∈ l
⊢ x = y ∨ x = z ∨ x ∈ l
[PROOFSTEP]
{aesop
}
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ x✝ y✝ : α
l✝ : List α
h✝ : ↑(formPerm (y✝ :: l✝)) x✝ ∈ y✝ :: l✝
z : α
l : List α
IH : ∀ (x y : α), ↑(formPerm (y :: l)) x ∈ y :: l → x ∈ y :: l
x y : α
hx : ↑(formPerm (z :: l)) x = x
h1 : x = y
h : z ∈ l
⊢ x = y ∨ x = z ∨ x ∈ l
[PROOFSTEP]
aesop
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ x✝ y✝ : α
l✝ : List α
h✝¹ : ↑(formPerm (y✝ :: l✝)) x✝ ∈ y✝ :: l✝
z : α
l : List α
IH : ∀ (x y : α), ↑(formPerm (y :: l)) x ∈ y :: l → x ∈ y :: l
x y : α
hx : ↑(formPerm (z :: l)) x = x
h1 : ¬x = y
h✝ : x = z
h : y ∈ l
⊢ x = y ∨ x = z ∨ x ∈ l
[PROOFSTEP]
try {aesop
}
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ x✝ y✝ : α
l✝ : List α
h✝¹ : ↑(formPerm (y✝ :: l✝)) x✝ ∈ y✝ :: l✝
z : α
l : List α
IH : ∀ (x y : α), ↑(formPerm (y :: l)) x ∈ y :: l → x ∈ y :: l
x y : α
hx : ↑(formPerm (z :: l)) x = x
h1 : ¬x = y
h✝ : x = z
h : y ∈ l
⊢ x = y ∨ x = z ∨ x ∈ l
[PROOFSTEP]
{aesop
}
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ x✝ y✝ : α
l✝ : List α
h✝¹ : ↑(formPerm (y✝ :: l✝)) x✝ ∈ y✝ :: l✝
z : α
l : List α
IH : ∀ (x y : α), ↑(formPerm (y :: l)) x ∈ y :: l → x ∈ y :: l
x y : α
hx : ↑(formPerm (z :: l)) x = x
h1 : ¬x = y
h✝ : x = z
h : y ∈ l
⊢ x = y ∨ x = z ∨ x ∈ l
[PROOFSTEP]
aesop
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ x✝ y✝ : α
l✝ : List α
h✝¹ : ↑(formPerm (y✝ :: l✝)) x✝ ∈ y✝ :: l✝
z : α
l : List α
IH : ∀ (x y : α), ↑(formPerm (y :: l)) x ∈ y :: l → x ∈ y :: l
x y : α
hx : ↑(formPerm (z :: l)) x = x
h1 : ¬x = y
h✝ : ¬x = z
h : x ∈ l
⊢ x = y ∨ x = z ∨ x ∈ l
[PROOFSTEP]
try {aesop
}
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ x✝ y✝ : α
l✝ : List α
h✝¹ : ↑(formPerm (y✝ :: l✝)) x✝ ∈ y✝ :: l✝
z : α
l : List α
IH : ∀ (x y : α), ↑(formPerm (y :: l)) x ∈ y :: l → x ∈ y :: l
x y : α
hx : ↑(formPerm (z :: l)) x = x
h1 : ¬x = y
h✝ : ¬x = z
h : x ∈ l
⊢ x = y ∨ x = z ∨ x ∈ l
[PROOFSTEP]
{aesop
}
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ x✝ y✝ : α
l✝ : List α
h✝¹ : ↑(formPerm (y✝ :: l✝)) x✝ ∈ y✝ :: l✝
z : α
l : List α
IH : ∀ (x y : α), ↑(formPerm (y :: l)) x ∈ y :: l → x ∈ y :: l
x y : α
hx : ↑(formPerm (z :: l)) x = x
h1 : ¬x = y
h✝ : ¬x = z
h : x ∈ l
⊢ x = y ∨ x = z ∨ x ∈ l
[PROOFSTEP]
aesop
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ x✝ y✝ : α
l✝ : List α
h✝ : ↑(formPerm (y✝ :: l✝)) x✝ ∈ y✝ :: l✝
z : α
l : List α
IH : ∀ (x y : α), ↑(formPerm (y :: l)) x ∈ y :: l → x ∈ y :: l
x y : α
hx : ↑(formPerm (z :: l)) x = x
h1 : ¬x = z
h : ¬x = y → x = z
⊢ x = y ∨ x = z ∨ x ∈ l
[PROOFSTEP]
simp [h1, imp_false] at h
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝¹ : List α
x✝¹ x✝ y✝ : α
l✝ : List α
h✝ : ↑(formPerm (y✝ :: l✝)) x✝ ∈ y✝ :: l✝
z : α
l : List α
IH : ∀ (x y : α), ↑(formPerm (y :: l)) x ∈ y :: l → x ∈ y :: l
x y : α
hx : ↑(formPerm (z :: l)) x = x
h1 : ¬x = z
h : x = y
⊢ x = y ∨ x = z ∨ x ∈ l
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l : List α
x✝ x y : α
xs : List α
⊢ ↑(formPerm (x :: (xs ++ [y]))) y = x
[PROOFSTEP]
induction' xs with z xs IH generalizing x y
[GOAL]
case nil
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l : List α
x✝¹ x✝ y✝ x y : α
⊢ ↑(formPerm (x :: ([] ++ [y]))) y = x
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l : List α
x✝¹ x✝ y✝ z : α
xs : List α
IH : ∀ (x y : α), ↑(formPerm (x :: (xs ++ [y]))) y = x
x y : α
⊢ ↑(formPerm (x :: (z :: xs ++ [y]))) y = x
[PROOFSTEP]
simp [IH]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l : List α
x✝ x : α
xs : List α
⊢ ↑(formPerm (x :: xs)) (getLast (x :: xs) (_ : x :: xs ≠ [])) = x
[PROOFSTEP]
induction' xs using List.reverseRecOn with xs y _ generalizing x
[GOAL]
case H0
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l : List α
x✝¹ x✝ x : α
⊢ ↑(formPerm [x]) (getLast [x] (_ : [x] ≠ [])) = x
[PROOFSTEP]
simp
[GOAL]
case H1
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l : List α
x✝¹ x✝ : α
xs : List α
y : α
a✝ : ∀ (x : α), ↑(formPerm (x :: xs)) (getLast (x :: xs) (_ : x :: xs ≠ [])) = x
x : α
⊢ ↑(formPerm (x :: (xs ++ [y]))) (getLast (x :: (xs ++ [y])) (_ : x :: (xs ++ [y]) ≠ [])) = x
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l : List α
x✝ x : α
xs : List α
⊢ length xs < length (x :: xs)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l : List α
x✝ x : α
xs : List α
⊢ ↑(formPerm (x :: xs)) (nthLe (x :: xs) (length xs) (_ : length xs < Nat.succ (length xs))) = x
[PROOFSTEP]
rw [nthLe_cons_length, formPerm_apply_getLast]
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l : List α
x✝ x : α
xs : List α
⊢ length xs = length xs
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l : List α
x✝ x y : α
xs : List α
h : Nodup (x :: y :: xs)
⊢ ↑(formPerm (x :: y :: xs)) x = y
[PROOFSTEP]
simp [formPerm_apply_of_not_mem _ _ h.not_mem]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
hl : 1 < length l
⊢ ↑(formPerm l) (nthLe l 0 (_ : 0 < length l)) = nthLe l 1 hl
[PROOFSTEP]
rcases l with (_ | ⟨x, _ | ⟨y, tl⟩⟩)
[GOAL]
case nil
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l : List α
x : α
h : Nodup []
hl : 1 < length []
⊢ ↑(formPerm []) (nthLe [] 0 (_ : 0 < length [])) = nthLe [] 1 hl
[PROOFSTEP]
simp at hl
[GOAL]
case cons.nil
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l : List α
x✝ x : α
h : Nodup [x]
hl : 1 < length [x]
⊢ ↑(formPerm [x]) (nthLe [x] 0 (_ : 0 < length [x])) = nthLe [x] 1 hl
[PROOFSTEP]
simp
[GOAL]
case cons.cons
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l : List α
x✝ x y : α
tl : List α
h : Nodup (x :: y :: tl)
hl : 1 < length (x :: y :: tl)
⊢ ↑(formPerm (x :: y :: tl)) (nthLe (x :: y :: tl) 0 (_ : 0 < length (x :: y :: tl))) = nthLe (x :: y :: tl) 1 hl
[PROOFSTEP]
simpa using formPerm_apply_head _ _ _ h
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l : List α
x✝ x y : α
⊢ ↑(formPerm (y :: l)) x = y ↔ ↑(formPerm (y :: l)) x = ↑(formPerm (y :: l)) (getLast (y :: l) (_ : y :: l ≠ []))
[PROOFSTEP]
rw [formPerm_apply_getLast]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x : α
l l' : List α
⊢ {x | ↑(prod (zipWith swap l l')) x ≠ x} ≤ ↑(toFinset l ⊔ toFinset l')
[PROOFSTEP]
simp only [Set.sup_eq_union, Set.le_eq_subset]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x : α
l l' : List α
⊢ {x | ↑(prod (zipWith swap l l')) x ≠ x} ⊆ ↑(toFinset l ⊔ toFinset l')
[PROOFSTEP]
induction' l with y l hl generalizing l'
[GOAL]
case nil
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l : List α
x : α
l'✝ l' : List α
⊢ {x | ↑(prod (zipWith swap [] l')) x ≠ x} ⊆ ↑(toFinset [] ⊔ toFinset l')
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x : α
l'✝ : List α
y : α
l : List α
hl : ∀ (l' : List α), {x | ↑(prod (zipWith swap l l')) x ≠ x} ⊆ ↑(toFinset l ⊔ toFinset l')
l' : List α
⊢ {x | ↑(prod (zipWith swap (y :: l) l')) x ≠ x} ⊆ ↑(toFinset (y :: l) ⊔ toFinset l')
[PROOFSTEP]
cases' l' with z l'
[GOAL]
case cons.nil
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x : α
l' : List α
y : α
l : List α
hl : ∀ (l' : List α), {x | ↑(prod (zipWith swap l l')) x ≠ x} ⊆ ↑(toFinset l ⊔ toFinset l')
⊢ {x | ↑(prod (zipWith swap (y :: l) [])) x ≠ x} ⊆ ↑(toFinset (y :: l) ⊔ toFinset [])
[PROOFSTEP]
simp
[GOAL]
case cons.cons
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x : α
l'✝ : List α
y : α
l : List α
hl : ∀ (l' : List α), {x | ↑(prod (zipWith swap l l')) x ≠ x} ⊆ ↑(toFinset l ⊔ toFinset l')
z : α
l' : List α
⊢ {x | ↑(prod (zipWith swap (y :: l) (z :: l'))) x ≠ x} ⊆ ↑(toFinset (y :: l) ⊔ toFinset (z :: l'))
[PROOFSTEP]
intro x
[GOAL]
case cons.cons
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l'✝ : List α
y : α
l : List α
hl : ∀ (l' : List α), {x | ↑(prod (zipWith swap l l')) x ≠ x} ⊆ ↑(toFinset l ⊔ toFinset l')
z : α
l' : List α
x : α
⊢ x ∈ {x | ↑(prod (zipWith swap (y :: l) (z :: l'))) x ≠ x} → x ∈ ↑(toFinset (y :: l) ⊔ toFinset (z :: l'))
[PROOFSTEP]
simp only [Set.union_subset_iff, mem_cons, zipWith_cons_cons, foldr, prod_cons, mul_apply]
[GOAL]
case cons.cons
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l'✝ : List α
y : α
l : List α
hl : ∀ (l' : List α), {x | ↑(prod (zipWith swap l l')) x ≠ x} ⊆ ↑(toFinset l ⊔ toFinset l')
z : α
l' : List α
x : α
⊢ x ∈ {x | ↑(swap y z) (↑(prod (zipWith swap l l')) x) ≠ x} → x ∈ ↑(toFinset (y :: l) ⊔ toFinset (z :: l'))
[PROOFSTEP]
intro hx
[GOAL]
case cons.cons
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l'✝ : List α
y : α
l : List α
hl : ∀ (l' : List α), {x | ↑(prod (zipWith swap l l')) x ≠ x} ⊆ ↑(toFinset l ⊔ toFinset l')
z : α
l' : List α
x : α
hx : x ∈ {x | ↑(swap y z) (↑(prod (zipWith swap l l')) x) ≠ x}
⊢ x ∈ ↑(toFinset (y :: l) ⊔ toFinset (z :: l'))
[PROOFSTEP]
by_cases h : x ∈ {x | (zipWith swap l l').prod x ≠ x}
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l'✝ : List α
y : α
l : List α
hl : ∀ (l' : List α), {x | ↑(prod (zipWith swap l l')) x ≠ x} ⊆ ↑(toFinset l ⊔ toFinset l')
z : α
l' : List α
x : α
hx : x ∈ {x | ↑(swap y z) (↑(prod (zipWith swap l l')) x) ≠ x}
h : x ∈ {x | ↑(prod (zipWith swap l l')) x ≠ x}
⊢ x ∈ ↑(toFinset (y :: l) ⊔ toFinset (z :: l'))
[PROOFSTEP]
specialize hl l' h
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l'✝ : List α
y : α
l : List α
z : α
l' : List α
x : α
hx : x ∈ {x | ↑(swap y z) (↑(prod (zipWith swap l l')) x) ≠ x}
h : x ∈ {x | ↑(prod (zipWith swap l l')) x ≠ x}
hl : x ∈ ↑(toFinset l ⊔ toFinset l')
⊢ x ∈ ↑(toFinset (y :: l) ⊔ toFinset (z :: l'))
[PROOFSTEP]
simp only [ge_iff_le, Finset.le_eq_subset, Finset.sup_eq_union, Finset.coe_union, coe_toFinset, Set.mem_union,
  Set.mem_setOf_eq] at hl
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l'✝ : List α
y : α
l : List α
z : α
l' : List α
x : α
hx : x ∈ {x | ↑(swap y z) (↑(prod (zipWith swap l l')) x) ≠ x}
h : x ∈ {x | ↑(prod (zipWith swap l l')) x ≠ x}
hl : x ∈ l ∨ x ∈ l'
⊢ x ∈ ↑(toFinset (y :: l) ⊔ toFinset (z :: l'))
[PROOFSTEP]
refine' Or.elim hl (fun hm => _) fun hm => _
[GOAL]
case pos.refine'_1
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l'✝ : List α
y : α
l : List α
z : α
l' : List α
x : α
hx : x ∈ {x | ↑(swap y z) (↑(prod (zipWith swap l l')) x) ≠ x}
h : x ∈ {x | ↑(prod (zipWith swap l l')) x ≠ x}
hl : x ∈ l ∨ x ∈ l'
hm : x ∈ l
⊢ x ∈ ↑(toFinset (y :: l) ⊔ toFinset (z :: l'))
[PROOFSTEP]
simp only [Finset.coe_insert, Set.mem_insert_iff, Finset.mem_coe, toFinset_cons, mem_toFinset] at hm ⊢
[GOAL]
case pos.refine'_1
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l'✝ : List α
y : α
l : List α
z : α
l' : List α
x : α
hx : x ∈ {x | ↑(swap y z) (↑(prod (zipWith swap l l')) x) ≠ x}
h : x ∈ {x | ↑(prod (zipWith swap l l')) x ≠ x}
hl : x ∈ l ∨ x ∈ l'
hm : x ∈ l
⊢ x ∈ insert y (toFinset l) ⊔ insert z (toFinset l')
[PROOFSTEP]
simp [hm]
[GOAL]
case pos.refine'_2
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l'✝ : List α
y : α
l : List α
z : α
l' : List α
x : α
hx : x ∈ {x | ↑(swap y z) (↑(prod (zipWith swap l l')) x) ≠ x}
h : x ∈ {x | ↑(prod (zipWith swap l l')) x ≠ x}
hl : x ∈ l ∨ x ∈ l'
hm : x ∈ l'
⊢ x ∈ ↑(toFinset (y :: l) ⊔ toFinset (z :: l'))
[PROOFSTEP]
simp only [Finset.coe_insert, Set.mem_insert_iff, Finset.mem_coe, toFinset_cons, mem_toFinset] at hm ⊢
[GOAL]
case pos.refine'_2
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l'✝ : List α
y : α
l : List α
z : α
l' : List α
x : α
hx : x ∈ {x | ↑(swap y z) (↑(prod (zipWith swap l l')) x) ≠ x}
h : x ∈ {x | ↑(prod (zipWith swap l l')) x ≠ x}
hl : x ∈ l ∨ x ∈ l'
hm : x ∈ l'
⊢ x ∈ insert y (toFinset l) ⊔ insert z (toFinset l')
[PROOFSTEP]
simp [hm]
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l'✝ : List α
y : α
l : List α
hl : ∀ (l' : List α), {x | ↑(prod (zipWith swap l l')) x ≠ x} ⊆ ↑(toFinset l ⊔ toFinset l')
z : α
l' : List α
x : α
hx : x ∈ {x | ↑(swap y z) (↑(prod (zipWith swap l l')) x) ≠ x}
h : ¬x ∈ {x | ↑(prod (zipWith swap l l')) x ≠ x}
⊢ x ∈ ↑(toFinset (y :: l) ⊔ toFinset (z :: l'))
[PROOFSTEP]
simp only [not_not, Set.mem_setOf_eq] at h
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l'✝ : List α
y : α
l : List α
hl : ∀ (l' : List α), {x | ↑(prod (zipWith swap l l')) x ≠ x} ⊆ ↑(toFinset l ⊔ toFinset l')
z : α
l' : List α
x : α
hx : x ∈ {x | ↑(swap y z) (↑(prod (zipWith swap l l')) x) ≠ x}
h : ↑(prod (zipWith swap l l')) x = x
⊢ x ∈ ↑(toFinset (y :: l) ⊔ toFinset (z :: l'))
[PROOFSTEP]
simp only [h, Set.mem_setOf_eq] at hx
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l'✝ : List α
y : α
l : List α
hl : ∀ (l' : List α), {x | ↑(prod (zipWith swap l l')) x ≠ x} ⊆ ↑(toFinset l ⊔ toFinset l')
z : α
l' : List α
x : α
h : ↑(prod (zipWith swap l l')) x = x
hx : ↑(swap y z) x ≠ x
⊢ x ∈ ↑(toFinset (y :: l) ⊔ toFinset (z :: l'))
[PROOFSTEP]
rw [swap_apply_ne_self_iff] at hx
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l'✝ : List α
y : α
l : List α
hl : ∀ (l' : List α), {x | ↑(prod (zipWith swap l l')) x ≠ x} ⊆ ↑(toFinset l ⊔ toFinset l')
z : α
l' : List α
x : α
h : ↑(prod (zipWith swap l l')) x = x
hx : y ≠ z ∧ (x = y ∨ x = z)
⊢ x ∈ ↑(toFinset (y :: l) ⊔ toFinset (z :: l'))
[PROOFSTEP]
rcases hx with ⟨hyz, rfl | rfl⟩
[GOAL]
case neg.intro.inl
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l'✝ l : List α
hl : ∀ (l' : List α), {x | ↑(prod (zipWith swap l l')) x ≠ x} ⊆ ↑(toFinset l ⊔ toFinset l')
z : α
l' : List α
x : α
h : ↑(prod (zipWith swap l l')) x = x
hyz : x ≠ z
⊢ x ∈ ↑(toFinset (x :: l) ⊔ toFinset (z :: l'))
[PROOFSTEP]
simp
[GOAL]
case neg.intro.inr
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l'✝ : List α
y : α
l : List α
hl : ∀ (l' : List α), {x | ↑(prod (zipWith swap l l')) x ≠ x} ⊆ ↑(toFinset l ⊔ toFinset l')
l' : List α
x : α
h : ↑(prod (zipWith swap l l')) x = x
hyz : y ≠ x
⊢ x ∈ ↑(toFinset (y :: l) ⊔ toFinset (x :: l'))
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
l✝ : List α
x : α
inst✝ : Fintype α
l l' : List α
⊢ support (prod (zipWith swap l l')) ≤ toFinset l ⊔ toFinset l'
[PROOFSTEP]
intro x hx
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
l✝ : List α
x✝ : α
inst✝ : Fintype α
l l' : List α
x : α
hx : x ∈ support (prod (zipWith swap l l'))
⊢ x ∈ toFinset l ⊔ toFinset l'
[PROOFSTEP]
have hx' : x ∈ {x | (zipWith swap l l').prod x ≠ x} := by simpa using hx
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
l✝ : List α
x✝ : α
inst✝ : Fintype α
l l' : List α
x : α
hx : x ∈ support (prod (zipWith swap l l'))
⊢ x ∈ {x | ↑(prod (zipWith swap l l')) x ≠ x}
[PROOFSTEP]
simpa using hx
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
l✝ : List α
x✝ : α
inst✝ : Fintype α
l l' : List α
x : α
hx : x ∈ support (prod (zipWith swap l l'))
hx' : x ∈ {x | ↑(prod (zipWith swap l l')) x ≠ x}
⊢ x ∈ toFinset l ⊔ toFinset l'
[PROOFSTEP]
simpa using zipWith_swap_prod_support' _ _ hx'
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l : List α
x : α
⊢ {x | ↑(formPerm l) x ≠ x} ≤ ↑(toFinset l)
[PROOFSTEP]
refine' (zipWith_swap_prod_support' l l.tail).trans _
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l : List α
x : α
⊢ ↑(toFinset l ⊔ toFinset (tail l)) ≤ ↑(toFinset l)
[PROOFSTEP]
simpa [Finset.subset_iff] using tail_subset l
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
l : List α
x : α
inst✝ : Fintype α
⊢ support (formPerm l) ≤ toFinset l
[PROOFSTEP]
intro x hx
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
l : List α
x✝ : α
inst✝ : Fintype α
x : α
hx : x ∈ support (formPerm l)
⊢ x ∈ toFinset l
[PROOFSTEP]
have hx' : x ∈ {x | formPerm l x ≠ x} := by simpa using hx
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
l : List α
x✝ : α
inst✝ : Fintype α
x : α
hx : x ∈ support (formPerm l)
⊢ x ∈ {x | ↑(formPerm l) x ≠ x}
[PROOFSTEP]
simpa using hx
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
l : List α
x✝ : α
inst✝ : Fintype α
x : α
hx : x ∈ support (formPerm l)
hx' : x ∈ {x | ↑(formPerm l) x ≠ x}
⊢ x ∈ toFinset l
[PROOFSTEP]
simpa using support_formPerm_le' _ hx'
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l : List α
x : α
xs : List α
h : Nodup xs
n : ℕ
hn : n + 1 < length xs
⊢ ↑(formPerm xs) (nthLe xs n (_ : n < length xs)) = nthLe xs (n + 1) hn
[PROOFSTEP]
induction' n with n IH generalizing xs
[GOAL]
case zero
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l : List α
x : α
xs✝ : List α
h✝ : Nodup xs✝
n : ℕ
hn✝ : n + 1 < length xs✝
xs : List α
h : Nodup xs
hn : Nat.zero + 1 < length xs
⊢ ↑(formPerm xs) (nthLe xs Nat.zero (_ : Nat.zero < length xs)) = nthLe xs (Nat.zero + 1) hn
[PROOFSTEP]
simpa using formPerm_apply_nthLe_zero _ h _
[GOAL]
case succ
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l : List α
x : α
xs✝ : List α
h✝ : Nodup xs✝
n✝ : ℕ
hn✝ : n✝ + 1 < length xs✝
n : ℕ
IH :
  ∀ (xs : List α),
    Nodup xs → ∀ (hn : n + 1 < length xs), ↑(formPerm xs) (nthLe xs n (_ : n < length xs)) = nthLe xs (n + 1) hn
xs : List α
h : Nodup xs
hn : Nat.succ n + 1 < length xs
⊢ ↑(formPerm xs) (nthLe xs (Nat.succ n) (_ : Nat.succ n < length xs)) = nthLe xs (Nat.succ n + 1) hn
[PROOFSTEP]
rcases xs with (_ | ⟨x, _ | ⟨y, l⟩⟩)
[GOAL]
case succ.nil
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l : List α
x : α
xs : List α
h✝ : Nodup xs
n✝ : ℕ
hn✝ : n✝ + 1 < length xs
n : ℕ
IH :
  ∀ (xs : List α),
    Nodup xs → ∀ (hn : n + 1 < length xs), ↑(formPerm xs) (nthLe xs n (_ : n < length xs)) = nthLe xs (n + 1) hn
h : Nodup []
hn : Nat.succ n + 1 < length []
⊢ ↑(formPerm []) (nthLe [] (Nat.succ n) (_ : Nat.succ n < length [])) = nthLe [] (Nat.succ n + 1) hn
[PROOFSTEP]
simp at hn
[GOAL]
case succ.cons.nil
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l : List α
x✝ : α
xs : List α
h✝ : Nodup xs
n✝ : ℕ
hn✝ : n✝ + 1 < length xs
n : ℕ
IH :
  ∀ (xs : List α),
    Nodup xs → ∀ (hn : n + 1 < length xs), ↑(formPerm xs) (nthLe xs n (_ : n < length xs)) = nthLe xs (n + 1) hn
x : α
h : Nodup [x]
hn : Nat.succ n + 1 < length [x]
⊢ ↑(formPerm [x]) (nthLe [x] (Nat.succ n) (_ : Nat.succ n < length [x])) = nthLe [x] (Nat.succ n + 1) hn
[PROOFSTEP]
simp
[GOAL]
case succ.cons.cons
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
xs : List α
h✝ : Nodup xs
n✝ : ℕ
hn✝ : n✝ + 1 < length xs
n : ℕ
IH :
  ∀ (xs : List α),
    Nodup xs → ∀ (hn : n + 1 < length xs), ↑(formPerm xs) (nthLe xs n (_ : n < length xs)) = nthLe xs (n + 1) hn
x y : α
l : List α
h : Nodup (x :: y :: l)
hn : Nat.succ n + 1 < length (x :: y :: l)
⊢ ↑(formPerm (x :: y :: l)) (nthLe (x :: y :: l) (Nat.succ n) (_ : Nat.succ n < length (x :: y :: l))) =
    nthLe (x :: y :: l) (Nat.succ n + 1) hn
[PROOFSTEP]
specialize IH (y :: l) h.of_cons _
[GOAL]
case succ.cons.cons
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
xs : List α
h✝ : Nodup xs
n✝ : ℕ
hn✝ : n✝ + 1 < length xs
n : ℕ
IH :
  ∀ (xs : List α),
    Nodup xs → ∀ (hn : n + 1 < length xs), ↑(formPerm xs) (nthLe xs n (_ : n < length xs)) = nthLe xs (n + 1) hn
x y : α
l : List α
h : Nodup (x :: y :: l)
hn : Nat.succ n + 1 < length (x :: y :: l)
⊢ n + 1 < length (y :: l)
[PROOFSTEP]
simpa [Nat.succ_lt_succ_iff] using hn
[GOAL]
case succ.cons.cons
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
xs : List α
h✝ : Nodup xs
n✝ : ℕ
hn✝ : n✝ + 1 < length xs
n : ℕ
IH✝ :
  ∀ (xs : List α),
    Nodup xs → ∀ (hn : n + 1 < length xs), ↑(formPerm xs) (nthLe xs n (_ : n < length xs)) = nthLe xs (n + 1) hn
x y : α
l : List α
h : Nodup (x :: y :: l)
hn : Nat.succ n + 1 < length (x :: y :: l)
IH :
  ↑(formPerm (y :: l)) (nthLe (y :: l) n (_ : n < length (y :: l))) =
    nthLe (y :: l) (n + 1) (_ : n + 1 < length (y :: l))
⊢ ↑(formPerm (x :: y :: l)) (nthLe (x :: y :: l) (Nat.succ n) (_ : Nat.succ n < length (x :: y :: l))) =
    nthLe (x :: y :: l) (Nat.succ n + 1) hn
[PROOFSTEP]
simp only [swap_apply_eq_iff, coe_mul, formPerm_cons_cons, Function.comp]
[GOAL]
case succ.cons.cons
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
xs : List α
h✝ : Nodup xs
n✝ : ℕ
hn✝ : n✝ + 1 < length xs
n : ℕ
IH✝ :
  ∀ (xs : List α),
    Nodup xs → ∀ (hn : n + 1 < length xs), ↑(formPerm xs) (nthLe xs n (_ : n < length xs)) = nthLe xs (n + 1) hn
x y : α
l : List α
h : Nodup (x :: y :: l)
hn : Nat.succ n + 1 < length (x :: y :: l)
IH :
  ↑(formPerm (y :: l)) (nthLe (y :: l) n (_ : n < length (y :: l))) =
    nthLe (y :: l) (n + 1) (_ : n + 1 < length (y :: l))
⊢ ↑(formPerm (y :: l)) (nthLe (x :: y :: l) (Nat.succ n) (_ : Nat.succ n < length (x :: y :: l))) =
    ↑(swap x y) (nthLe (x :: y :: l) (Nat.succ n + 1) hn)
[PROOFSTEP]
simp only [nthLe, get_cons_succ] at *
[GOAL]
case succ.cons.cons
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
xs : List α
h✝ : Nodup xs
n✝ : ℕ
hn✝ : n✝ + 1 < length xs
n : ℕ
IH✝ :
  ∀ (xs : List α),
    Nodup xs →
      ∀ (hn : n + 1 < length xs),
        ↑(formPerm xs) (get xs { val := n, isLt := (_ : n < length xs) }) = get xs { val := n + 1, isLt := hn }
x y : α
l : List α
h : Nodup (x :: y :: l)
hn : Nat.succ n + 1 < length (x :: y :: l)
IH :
  ↑(formPerm (y :: l)) (get (y :: l) { val := n, isLt := (_ : n < length (y :: l)) }) =
    get l { val := n, isLt := (_ : n < length l) }
⊢ ↑(formPerm (y :: l)) (get (y :: l) { val := n, isLt := (_ : n < length (y :: l)) }) =
    ↑(swap x y) (get l { val := n, isLt := (_ : n < length l) })
[PROOFSTEP]
rw [← IH, swap_apply_of_ne_of_ne]
[GOAL]
case succ.cons.cons.a
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
xs : List α
h✝ : Nodup xs
n✝ : ℕ
hn✝ : n✝ + 1 < length xs
n : ℕ
IH✝ :
  ∀ (xs : List α),
    Nodup xs →
      ∀ (hn : n + 1 < length xs),
        ↑(formPerm xs) (get xs { val := n, isLt := (_ : n < length xs) }) = get xs { val := n + 1, isLt := hn }
x y : α
l : List α
h : Nodup (x :: y :: l)
hn : Nat.succ n + 1 < length (x :: y :: l)
IH :
  ↑(formPerm (y :: l)) (get (y :: l) { val := n, isLt := (_ : n < length (y :: l)) }) =
    get l { val := n, isLt := (_ : n < length l) }
⊢ ↑(formPerm (y :: l)) (get (y :: l) { val := n, isLt := (_ : n < length (y :: l)) }) ≠ x
[PROOFSTEP]
intro hx
[GOAL]
case succ.cons.cons.a
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
xs : List α
h✝ : Nodup xs
n✝ : ℕ
hn✝ : n✝ + 1 < length xs
n : ℕ
IH✝ :
  ∀ (xs : List α),
    Nodup xs →
      ∀ (hn : n + 1 < length xs),
        ↑(formPerm xs) (get xs { val := n, isLt := (_ : n < length xs) }) = get xs { val := n + 1, isLt := hn }
x y : α
l : List α
h : Nodup (x :: y :: l)
hn : Nat.succ n + 1 < length (x :: y :: l)
IH :
  ↑(formPerm (y :: l)) (get (y :: l) { val := n, isLt := (_ : n < length (y :: l)) }) =
    get l { val := n, isLt := (_ : n < length l) }
hx : ↑(formPerm (y :: l)) (get (y :: l) { val := n, isLt := (_ : n < length (y :: l)) }) = x
⊢ False
[PROOFSTEP]
rw [← hx, IH] at h
[GOAL]
case succ.cons.cons.a
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
xs : List α
h✝ : Nodup xs
n✝ : ℕ
hn✝ : n✝ + 1 < length xs
n : ℕ
IH✝ :
  ∀ (xs : List α),
    Nodup xs →
      ∀ (hn : n + 1 < length xs),
        ↑(formPerm xs) (get xs { val := n, isLt := (_ : n < length xs) }) = get xs { val := n + 1, isLt := hn }
x y : α
l : List α
hn : Nat.succ n + 1 < length (x :: y :: l)
h : Nodup (get l { val := n, isLt := (_ : n < length l) } :: y :: l)
IH :
  ↑(formPerm (y :: l)) (get (y :: l) { val := n, isLt := (_ : n < length (y :: l)) }) =
    get l { val := n, isLt := (_ : n < length l) }
hx : ↑(formPerm (y :: l)) (get (y :: l) { val := n, isLt := (_ : n < length (y :: l)) }) = x
⊢ False
[PROOFSTEP]
simp [get_mem] at h
[GOAL]
case succ.cons.cons.a
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
xs : List α
h✝ : Nodup xs
n✝ : ℕ
hn✝ : n✝ + 1 < length xs
n : ℕ
IH✝ :
  ∀ (xs : List α),
    Nodup xs →
      ∀ (hn : n + 1 < length xs),
        ↑(formPerm xs) (get xs { val := n, isLt := (_ : n < length xs) }) = get xs { val := n + 1, isLt := hn }
x y : α
l : List α
h : Nodup (x :: y :: l)
hn : Nat.succ n + 1 < length (x :: y :: l)
IH :
  ↑(formPerm (y :: l)) (get (y :: l) { val := n, isLt := (_ : n < length (y :: l)) }) =
    get l { val := n, isLt := (_ : n < length l) }
⊢ ↑(formPerm (y :: l)) (get (y :: l) { val := n, isLt := (_ : n < length (y :: l)) }) ≠ y
[PROOFSTEP]
intro hx
[GOAL]
case succ.cons.cons.a
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
xs : List α
h✝ : Nodup xs
n✝ : ℕ
hn✝ : n✝ + 1 < length xs
n : ℕ
IH✝ :
  ∀ (xs : List α),
    Nodup xs →
      ∀ (hn : n + 1 < length xs),
        ↑(formPerm xs) (get xs { val := n, isLt := (_ : n < length xs) }) = get xs { val := n + 1, isLt := hn }
x y : α
l : List α
h : Nodup (x :: y :: l)
hn : Nat.succ n + 1 < length (x :: y :: l)
IH :
  ↑(formPerm (y :: l)) (get (y :: l) { val := n, isLt := (_ : n < length (y :: l)) }) =
    get l { val := n, isLt := (_ : n < length l) }
hx : ↑(formPerm (y :: l)) (get (y :: l) { val := n, isLt := (_ : n < length (y :: l)) }) = y
⊢ False
[PROOFSTEP]
rw [← hx, IH] at h
[GOAL]
case succ.cons.cons.a
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
xs : List α
h✝ : Nodup xs
n✝ : ℕ
hn✝ : n✝ + 1 < length xs
n : ℕ
IH✝ :
  ∀ (xs : List α),
    Nodup xs →
      ∀ (hn : n + 1 < length xs),
        ↑(formPerm xs) (get xs { val := n, isLt := (_ : n < length xs) }) = get xs { val := n + 1, isLt := hn }
x y : α
l : List α
hn : Nat.succ n + 1 < length (x :: y :: l)
h : Nodup (x :: get l { val := n, isLt := (_ : n < length l) } :: l)
IH :
  ↑(formPerm (y :: l)) (get (y :: l) { val := n, isLt := (_ : n < length (y :: l)) }) =
    get l { val := n, isLt := (_ : n < length l) }
hx : ↑(formPerm (y :: l)) (get (y :: l) { val := n, isLt := (_ : n < length (y :: l)) }) = y
⊢ False
[PROOFSTEP]
simp [get_mem] at h
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l : List α
x : α
xs : List α
h : Nodup xs
n : ℕ
hn : n < length xs
⊢ ↑(formPerm xs) (nthLe xs n hn) = nthLe xs ((n + 1) % length xs) (_ : (n + 1) % length xs < length xs)
[PROOFSTEP]
cases' xs with x xs
[GOAL]
case nil
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l : List α
x : α
n : ℕ
h : Nodup []
hn : n < length []
⊢ ↑(formPerm []) (nthLe [] n hn) = nthLe [] ((n + 1) % length []) (_ : (n + 1) % length [] < length [])
[PROOFSTEP]
simp at hn
[GOAL]
case cons
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l : List α
x✝ : α
n : ℕ
x : α
xs : List α
h : Nodup (x :: xs)
hn : n < length (x :: xs)
⊢ ↑(formPerm (x :: xs)) (nthLe (x :: xs) n hn) =
    nthLe (x :: xs) ((n + 1) % length (x :: xs)) (_ : (n + 1) % length (x :: xs) < length (x :: xs))
[PROOFSTEP]
have : n ≤ xs.length := by
  refine' Nat.le_of_lt_succ _
  simpa using hn
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l : List α
x✝ : α
n : ℕ
x : α
xs : List α
h : Nodup (x :: xs)
hn : n < length (x :: xs)
⊢ n ≤ length xs
[PROOFSTEP]
refine' Nat.le_of_lt_succ _
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l : List α
x✝ : α
n : ℕ
x : α
xs : List α
h : Nodup (x :: xs)
hn : n < length (x :: xs)
⊢ n < Nat.succ (length xs)
[PROOFSTEP]
simpa using hn
[GOAL]
case cons
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l : List α
x✝ : α
n : ℕ
x : α
xs : List α
h : Nodup (x :: xs)
hn : n < length (x :: xs)
this : n ≤ length xs
⊢ ↑(formPerm (x :: xs)) (nthLe (x :: xs) n hn) =
    nthLe (x :: xs) ((n + 1) % length (x :: xs)) (_ : (n + 1) % length (x :: xs) < length (x :: xs))
[PROOFSTEP]
rcases this.eq_or_lt with (rfl | hn')
[GOAL]
case cons.inl
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l : List α
x✝ x : α
xs : List α
h : Nodup (x :: xs)
hn : length xs < length (x :: xs)
this : length xs ≤ length xs
⊢ ↑(formPerm (x :: xs)) (nthLe (x :: xs) (length xs) hn) =
    nthLe (x :: xs) ((length xs + 1) % length (x :: xs)) (_ : (length xs + 1) % length (x :: xs) < length (x :: xs))
[PROOFSTEP]
simp
[GOAL]
case cons.inl
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l : List α
x✝ x : α
xs : List α
h : Nodup (x :: xs)
hn : length xs < length (x :: xs)
this : length xs ≤ length xs
⊢ x = nthLe (x :: xs) 0 (_ : 0 < length (x :: xs))
[PROOFSTEP]
simp [nthLe]
[GOAL]
case cons.inr
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l : List α
x✝ : α
n : ℕ
x : α
xs : List α
h : Nodup (x :: xs)
hn : n < length (x :: xs)
this : n ≤ length xs
hn' : n < length xs
⊢ ↑(formPerm (x :: xs)) (nthLe (x :: xs) n hn) =
    nthLe (x :: xs) ((n + 1) % length (x :: xs)) (_ : (n + 1) % length (x :: xs) < length (x :: xs))
[PROOFSTEP]
rw [formPerm_apply_lt _ h _ (Nat.succ_lt_succ hn')]
[GOAL]
case cons.inr
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l : List α
x✝ : α
n : ℕ
x : α
xs : List α
h : Nodup (x :: xs)
hn : n < length (x :: xs)
this : n ≤ length xs
hn' : n < length xs
⊢ nthLe (x :: xs) (n + 1) (_ : Nat.succ n < Nat.succ (length xs)) =
    nthLe (x :: xs) ((n + 1) % length (x :: xs)) (_ : (n + 1) % length (x :: xs) < length (x :: xs))
[PROOFSTEP]
congr
[GOAL]
case cons.inr.e_n
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l : List α
x✝ : α
n : ℕ
x : α
xs : List α
h : Nodup (x :: xs)
hn : n < length (x :: xs)
this : n ≤ length xs
hn' : n < length xs
⊢ n + 1 = (n + 1) % length (x :: xs)
[PROOFSTEP]
rw [Nat.mod_eq_of_lt]
[GOAL]
case cons.inr.e_n
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l : List α
x✝ : α
n : ℕ
x : α
xs : List α
h : Nodup (x :: xs)
hn : n < length (x :: xs)
this : n ≤ length xs
hn' : n < length xs
⊢ n + 1 < length (x :: xs)
[PROOFSTEP]
simpa [Nat.succ_eq_add_one]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
h' : ∀ (x : α), l ≠ [x]
⊢ {x | ↑(formPerm l) x ≠ x} = ↑(toFinset l)
[PROOFSTEP]
apply _root_.le_antisymm
[GOAL]
case a
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
h' : ∀ (x : α), l ≠ [x]
⊢ {x | ↑(formPerm l) x ≠ x} ≤ ↑(toFinset l)
[PROOFSTEP]
exact support_formPerm_le' l
[GOAL]
case a
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
h' : ∀ (x : α), l ≠ [x]
⊢ ↑(toFinset l) ≤ {x | ↑(formPerm l) x ≠ x}
[PROOFSTEP]
intro x hx
[GOAL]
case a
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l : List α
h : Nodup l
h' : ∀ (x : α), l ≠ [x]
x : α
hx : x ∈ ↑(toFinset l)
⊢ x ∈ {x | ↑(formPerm l) x ≠ x}
[PROOFSTEP]
simp only [Finset.mem_coe, mem_toFinset] at hx
[GOAL]
case a
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l : List α
h : Nodup l
h' : ∀ (x : α), l ≠ [x]
x : α
hx : x ∈ l
⊢ x ∈ {x | ↑(formPerm l) x ≠ x}
[PROOFSTEP]
obtain ⟨n, hn, rfl⟩ := nthLe_of_mem hx
[GOAL]
case a.intro.intro
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < length l
hx : nthLe l n hn ∈ l
⊢ nthLe l n hn ∈ {x | ↑(formPerm l) x ≠ x}
[PROOFSTEP]
rw [Set.mem_setOf_eq, formPerm_apply_nthLe _ h]
[GOAL]
case a.intro.intro
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < length l
hx : nthLe l n hn ∈ l
⊢ nthLe l ((n + 1) % length l) (_ : (n + 1) % length l < length l) ≠ nthLe l n hn
[PROOFSTEP]
intro H
[GOAL]
case a.intro.intro
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < length l
hx : nthLe l n hn ∈ l
H : nthLe l ((n + 1) % length l) (_ : (n + 1) % length l < length l) = nthLe l n hn
⊢ False
[PROOFSTEP]
rw [nodup_iff_nthLe_inj] at h
[GOAL]
case a.intro.intro
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : ∀ (i j : ℕ) (h₁ : i < length l) (h₂ : j < length l), nthLe l i h₁ = nthLe l j h₂ → i = j
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < length l
hx : nthLe l n hn ∈ l
H : nthLe l ((n + 1) % length l) (_ : (n + 1) % length l < length l) = nthLe l n hn
⊢ False
[PROOFSTEP]
specialize h _ _ _ _ H
[GOAL]
case a.intro.intro
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < length l
hx : nthLe l n hn ∈ l
H : nthLe l ((n + 1) % length l) (_ : (n + 1) % length l < length l) = nthLe l n hn
h : (n + 1) % length l = n
⊢ False
[PROOFSTEP]
cases' (Nat.succ_le_of_lt hn).eq_or_lt with hn' hn'
[GOAL]
case a.intro.intro.inl
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < length l
hx : nthLe l n hn ∈ l
H : nthLe l ((n + 1) % length l) (_ : (n + 1) % length l < length l) = nthLe l n hn
h : (n + 1) % length l = n
hn' : Nat.succ n = length l
⊢ False
[PROOFSTEP]
simp only [← hn', Nat.mod_self] at h
[GOAL]
case a.intro.intro.inl
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < length l
hx : nthLe l n hn ∈ l
H : nthLe l ((n + 1) % length l) (_ : (n + 1) % length l < length l) = nthLe l n hn
hn' : Nat.succ n = length l
h : 0 = n
⊢ False
[PROOFSTEP]
refine' not_exists.mpr h' _
[GOAL]
case a.intro.intro.inl
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < length l
hx : nthLe l n hn ∈ l
H : nthLe l ((n + 1) % length l) (_ : (n + 1) % length l < length l) = nthLe l n hn
hn' : Nat.succ n = length l
h : 0 = n
⊢ ∃ x, l = [x]
[PROOFSTEP]
rw [← length_eq_one]
[GOAL]
case a.intro.intro.inl
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < length l
hx : nthLe l n hn ∈ l
H : nthLe l ((n + 1) % length l) (_ : (n + 1) % length l < length l) = nthLe l n hn
hn' : Nat.succ n = length l
h : 0 = n
⊢ length l = 1
[PROOFSTEP]
simpa [← h, eq_comm] using hn'
[GOAL]
case a.intro.intro.inr
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < length l
hx : nthLe l n hn ∈ l
H : nthLe l ((n + 1) % length l) (_ : (n + 1) % length l < length l) = nthLe l n hn
h : (n + 1) % length l = n
hn' : Nat.succ n < length l
⊢ False
[PROOFSTEP]
simp [Nat.mod_eq_of_lt hn'] at h
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
l✝ : List α
x : α
inst✝ : Fintype α
l : List α
h : Nodup l
h' : ∀ (x : α), l ≠ [x]
⊢ support (formPerm l) = toFinset l
[PROOFSTEP]
rw [← Finset.coe_inj]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
l✝ : List α
x : α
inst✝ : Fintype α
l : List α
h : Nodup l
h' : ∀ (x : α), l ≠ [x]
⊢ ↑(support (formPerm l)) = ↑(toFinset l)
[PROOFSTEP]
convert support_formPerm_of_nodup' _ h h'
[GOAL]
case h.e'_2
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
l✝ : List α
x : α
inst✝ : Fintype α
l : List α
h : Nodup l
h' : ∀ (x : α), l ≠ [x]
⊢ ↑(support (formPerm l)) = {x | ↑(formPerm l) x ≠ x}
[PROOFSTEP]
simp [Set.ext_iff]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
⊢ formPerm (rotate l 1) = formPerm l
[PROOFSTEP]
have h' : Nodup (l.rotate 1) := by simpa using h
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
⊢ Nodup (rotate l 1)
[PROOFSTEP]
simpa using h
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
h' : Nodup (rotate l 1)
⊢ formPerm (rotate l 1) = formPerm l
[PROOFSTEP]
ext x
[GOAL]
case H
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l : List α
h : Nodup l
h' : Nodup (rotate l 1)
x : α
⊢ ↑(formPerm (rotate l 1)) x = ↑(formPerm l) x
[PROOFSTEP]
by_cases hx : x ∈ l.rotate 1
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l : List α
h : Nodup l
h' : Nodup (rotate l 1)
x : α
hx : x ∈ rotate l 1
⊢ ↑(formPerm (rotate l 1)) x = ↑(formPerm l) x
[PROOFSTEP]
obtain ⟨k, hk, rfl⟩ := nthLe_of_mem hx
[GOAL]
case pos.intro.intro
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
h' : Nodup (rotate l 1)
k : ℕ
hk : k < length (rotate l 1)
hx : nthLe (rotate l 1) k hk ∈ rotate l 1
⊢ ↑(formPerm (rotate l 1)) (nthLe (rotate l 1) k hk) = ↑(formPerm l) (nthLe (rotate l 1) k hk)
[PROOFSTEP]
rw [formPerm_apply_nthLe _ h', nthLe_rotate l, nthLe_rotate l, formPerm_apply_nthLe _ h]
[GOAL]
case pos.intro.intro
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
h' : Nodup (rotate l 1)
k : ℕ
hk : k < length (rotate l 1)
hx : nthLe (rotate l 1) k hk ∈ rotate l 1
⊢ nthLe l (((k + 1) % length (rotate l 1) + 1) % length l)
      (_ : ((k + 1) % length (rotate l 1) + 1) % length l < length l) =
    nthLe l (((k + 1) % length l + 1) % length l) (_ : ((k + 1) % length l + 1) % length l < length l)
[PROOFSTEP]
simp
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l : List α
h : Nodup l
h' : Nodup (rotate l 1)
x : α
hx : ¬x ∈ rotate l 1
⊢ ↑(formPerm (rotate l 1)) x = ↑(formPerm l) x
[PROOFSTEP]
rw [formPerm_apply_of_not_mem _ _ hx, formPerm_apply_of_not_mem]
[GOAL]
case neg.h
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l : List α
h : Nodup l
h' : Nodup (rotate l 1)
x : α
hx : ¬x ∈ rotate l 1
⊢ ¬x ∈ l
[PROOFSTEP]
simpa using hx
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
n : ℕ
⊢ formPerm (rotate l n) = formPerm l
[PROOFSTEP]
induction' n with n hn
[GOAL]
case zero
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
⊢ formPerm (rotate l Nat.zero) = formPerm l
[PROOFSTEP]
simp
[GOAL]
case succ
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
n : ℕ
hn : formPerm (rotate l n) = formPerm l
⊢ formPerm (rotate l (Nat.succ n)) = formPerm l
[PROOFSTEP]
rw [Nat.succ_eq_add_one, ← rotate_rotate, formPerm_rotate_one, hn]
[GOAL]
case succ.h
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
n : ℕ
hn : formPerm (rotate l n) = formPerm l
⊢ Nodup (rotate l n)
[PROOFSTEP]
rwa [IsRotated.nodup_iff]
[GOAL]
case succ.h
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
n : ℕ
hn : formPerm (rotate l n) = formPerm l
⊢ rotate l n ~r l
[PROOFSTEP]
exact IsRotated.forall l n
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x : α
l l' : List α
hd : Nodup l
h : l ~r l'
⊢ formPerm l = formPerm l'
[PROOFSTEP]
obtain ⟨n, rfl⟩ := h
[GOAL]
case intro
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
hd : Nodup l
n : ℕ
⊢ formPerm l = formPerm (rotate l n)
[PROOFSTEP]
exact (formPerm_rotate l hd n).symm
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
⊢ formPerm (reverse l) = (formPerm l)⁻¹
[PROOFSTEP]
rw [eq_comm, inv_eq_iff_mul_eq_one]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
⊢ formPerm l * formPerm (reverse l) = 1
[PROOFSTEP]
ext x
[GOAL]
case H
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l : List α
h : Nodup l
x : α
⊢ ↑(formPerm l * formPerm (reverse l)) x = ↑1 x
[PROOFSTEP]
rw [mul_apply, one_apply]
[GOAL]
case H
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l : List α
h : Nodup l
x : α
⊢ ↑(formPerm l) (↑(formPerm (reverse l)) x) = x
[PROOFSTEP]
cases' Classical.em (x ∈ l) with hx hx
[GOAL]
case H.inl
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l : List α
h : Nodup l
x : α
hx : x ∈ l
⊢ ↑(formPerm l) (↑(formPerm (reverse l)) x) = x
[PROOFSTEP]
obtain ⟨k, hk, rfl⟩ := nthLe_of_mem (mem_reverse.mpr hx)
[GOAL]
case H.inl.intro.intro
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length (reverse l)
hx : nthLe (reverse l) k hk ∈ l
⊢ ↑(formPerm l) (↑(formPerm (reverse l)) (nthLe (reverse l) k hk)) = nthLe (reverse l) k hk
[PROOFSTEP]
have h1 : l.length - 1 - k < l.length := by
  rw [Nat.sub_sub, add_comm]
  exact Nat.sub_lt_self (Nat.succ_pos _) (Nat.succ_le_of_lt (by simpa using hk))
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length (reverse l)
hx : nthLe (reverse l) k hk ∈ l
⊢ length l - 1 - k < length l
[PROOFSTEP]
rw [Nat.sub_sub, add_comm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length (reverse l)
hx : nthLe (reverse l) k hk ∈ l
⊢ length l - (k + 1) < length l
[PROOFSTEP]
exact Nat.sub_lt_self (Nat.succ_pos _) (Nat.succ_le_of_lt (by simpa using hk))
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length (reverse l)
hx : nthLe (reverse l) k hk ∈ l
⊢ k < length l
[PROOFSTEP]
simpa using hk
[GOAL]
case H.inl.intro.intro
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length (reverse l)
hx : nthLe (reverse l) k hk ∈ l
h1 : length l - 1 - k < length l
⊢ ↑(formPerm l) (↑(formPerm (reverse l)) (nthLe (reverse l) k hk)) = nthLe (reverse l) k hk
[PROOFSTEP]
have h2 : length l - 1 - (k + 1) % length (reverse l) < length l := by rw [Nat.sub_sub, length_reverse];
  exact
    Nat.sub_lt_self (by rw [add_comm]; exact Nat.succ_pos _)
      (by rw [add_comm]; exact Nat.succ_le_of_lt (Nat.mod_lt _ (length_pos_of_mem hx)))
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length (reverse l)
hx : nthLe (reverse l) k hk ∈ l
h1 : length l - 1 - k < length l
⊢ length l - 1 - (k + 1) % length (reverse l) < length l
[PROOFSTEP]
rw [Nat.sub_sub, length_reverse]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length (reverse l)
hx : nthLe (reverse l) k hk ∈ l
h1 : length l - 1 - k < length l
⊢ length l - (1 + (k + 1) % length l) < length l
[PROOFSTEP]
exact
  Nat.sub_lt_self (by rw [add_comm]; exact Nat.succ_pos _)
    (by rw [add_comm]; exact Nat.succ_le_of_lt (Nat.mod_lt _ (length_pos_of_mem hx)))
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length (reverse l)
hx : nthLe (reverse l) k hk ∈ l
h1 : length l - 1 - k < length l
⊢ 0 < 1 + (k + 1) % length l
[PROOFSTEP]
rw [add_comm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length (reverse l)
hx : nthLe (reverse l) k hk ∈ l
h1 : length l - 1 - k < length l
⊢ 0 < (k + 1) % length l + 1
[PROOFSTEP]
exact Nat.succ_pos _
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length (reverse l)
hx : nthLe (reverse l) k hk ∈ l
h1 : length l - 1 - k < length l
⊢ 1 + (k + 1) % length l ≤ length l
[PROOFSTEP]
rw [add_comm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length (reverse l)
hx : nthLe (reverse l) k hk ∈ l
h1 : length l - 1 - k < length l
⊢ (k + 1) % length l + 1 ≤ length l
[PROOFSTEP]
exact Nat.succ_le_of_lt (Nat.mod_lt _ (length_pos_of_mem hx))
[GOAL]
case H.inl.intro.intro
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length (reverse l)
hx : nthLe (reverse l) k hk ∈ l
h1 : length l - 1 - k < length l
h2 : length l - 1 - (k + 1) % length (reverse l) < length l
⊢ ↑(formPerm l) (↑(formPerm (reverse l)) (nthLe (reverse l) k hk)) = nthLe (reverse l) k hk
[PROOFSTEP]
rw [formPerm_apply_nthLe l.reverse (nodup_reverse.mpr h), nthLe_reverse' _ _ _ h1, nthLe_reverse' _ _ _ h2,
  formPerm_apply_nthLe _ h]
[GOAL]
case H.inl.intro.intro
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length (reverse l)
hx : nthLe (reverse l) k hk ∈ l
h1 : length l - 1 - k < length l
h2 : length l - 1 - (k + 1) % length (reverse l) < length l
⊢ nthLe l ((length l - 1 - (k + 1) % length (reverse l) + 1) % length l)
      (_ : (length l - 1 - (k + 1) % length (reverse l) + 1) % length l < length l) =
    nthLe l (length l - 1 - k) h1
[PROOFSTEP]
congr
[GOAL]
case H.inl.intro.intro.e_n
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length (reverse l)
hx : nthLe (reverse l) k hk ∈ l
h1 : length l - 1 - k < length l
h2 : length l - 1 - (k + 1) % length (reverse l) < length l
⊢ (length l - 1 - (k + 1) % length (reverse l) + 1) % length l = length l - 1 - k
[PROOFSTEP]
rw [length_reverse] at *
[GOAL]
case H.inl.intro.intro.e_n
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk✝ : k < length (reverse l)
hk : k < length l
hx : nthLe (reverse l) k hk✝ ∈ l
h1 : length l - 1 - k < length l
h2 : length l - 1 - (k + 1) % length l < length l
⊢ (length l - 1 - (k + 1) % length l + 1) % length l = length l - 1 - k
[PROOFSTEP]
cases' lt_or_eq_of_le (Nat.succ_le_of_lt hk) with h h
[GOAL]
case H.inl.intro.intro.e_n.inl
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h✝ : Nodup l
k : ℕ
hk✝ : k < length (reverse l)
hk : k < length l
hx : nthLe (reverse l) k hk✝ ∈ l
h1 : length l - 1 - k < length l
h2 : length l - 1 - (k + 1) % length l < length l
h : Nat.succ k < length l
⊢ (length l - 1 - (k + 1) % length l + 1) % length l = length l - 1 - k
[PROOFSTEP]
rw [Nat.mod_eq_of_lt h, ← Nat.sub_add_comm, Nat.succ_sub_succ_eq_sub, Nat.mod_eq_of_lt h1]
[GOAL]
case H.inl.intro.intro.e_n.inl
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h✝ : Nodup l
k : ℕ
hk✝ : k < length (reverse l)
hk : k < length l
hx : nthLe (reverse l) k hk✝ ∈ l
h1 : length l - 1 - k < length l
h2 : length l - 1 - (k + 1) % length l < length l
h : Nat.succ k < length l
⊢ Nat.succ k ≤ length l - 1
[PROOFSTEP]
exact (Nat.le_sub_iff_add_le (length_pos_of_mem hx)).2 (Nat.succ_le_of_lt h)
[GOAL]
case H.inl.intro.intro.e_n.inr
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h✝ : Nodup l
k : ℕ
hk✝ : k < length (reverse l)
hk : k < length l
hx : nthLe (reverse l) k hk✝ ∈ l
h1 : length l - 1 - k < length l
h2 : length l - 1 - (k + 1) % length l < length l
h : Nat.succ k = length l
⊢ (length l - 1 - (k + 1) % length l + 1) % length l = length l - 1 - k
[PROOFSTEP]
rw [← h]
[GOAL]
case H.inl.intro.intro.e_n.inr
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h✝ : Nodup l
k : ℕ
hk✝ : k < length (reverse l)
hk : k < length l
hx : nthLe (reverse l) k hk✝ ∈ l
h1 : length l - 1 - k < length l
h2 : length l - 1 - (k + 1) % length l < length l
h : Nat.succ k = length l
⊢ (Nat.succ k - 1 - (k + 1) % Nat.succ k + 1) % Nat.succ k = Nat.succ k - 1 - k
[PROOFSTEP]
simp
[GOAL]
case H.inr
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l : List α
h : Nodup l
x : α
hx : ¬x ∈ l
⊢ ↑(formPerm l) (↑(formPerm (reverse l)) x) = x
[PROOFSTEP]
rw [formPerm_apply_of_not_mem x l.reverse, formPerm_apply_of_not_mem _ _ hx]
[GOAL]
case H.inr
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l : List α
h : Nodup l
x : α
hx : ¬x ∈ l
⊢ ¬x ∈ reverse l
[PROOFSTEP]
simpa using hx
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
n k : ℕ
hk : k < length l
⊢ ↑(formPerm l ^ n) (nthLe l k hk) = nthLe l ((k + n) % length l) (_ : (k + n) % length l < length l)
[PROOFSTEP]
induction' n with n hn
[GOAL]
case zero
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length l
⊢ ↑(formPerm l ^ Nat.zero) (nthLe l k hk) =
    nthLe l ((k + Nat.zero) % length l) (_ : (k + Nat.zero) % length l < length l)
[PROOFSTEP]
simp [Nat.mod_eq_of_lt hk]
[GOAL]
case succ
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length l
n : ℕ
hn : ↑(formPerm l ^ n) (nthLe l k hk) = nthLe l ((k + n) % length l) (_ : (k + n) % length l < length l)
⊢ ↑(formPerm l ^ Nat.succ n) (nthLe l k hk) =
    nthLe l ((k + Nat.succ n) % length l) (_ : (k + Nat.succ n) % length l < length l)
[PROOFSTEP]
simp [pow_succ, mul_apply, hn, formPerm_apply_nthLe _ h, Nat.succ_eq_add_one, ← Nat.add_assoc]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ x : α
l : List α
h : Nodup (x :: l)
n : ℕ
⊢ ↑(formPerm (x :: l) ^ n) x = nthLe (x :: l) (n % length (x :: l)) (_ : n % length (x :: l) < length (x :: l))
[PROOFSTEP]
convert formPerm_pow_apply_nthLe _ h n 0 (Nat.succ_pos _)
[GOAL]
case h.e'_3.h.e'_3.h.e'_5
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ x : α
l : List α
h : Nodup (x :: l)
n : ℕ
⊢ n = 0 + n
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
⊢ formPerm (x :: y :: l) = formPerm (x' :: y' :: l') ↔ (x :: y :: l) ~r (x' :: y' :: l')
[PROOFSTEP]
refine' ⟨fun h => _, fun hr => formPerm_eq_of_isRotated hd hr⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : formPerm (x :: y :: l) = formPerm (x' :: y' :: l')
⊢ (x :: y :: l) ~r (x' :: y' :: l')
[PROOFSTEP]
rw [Equiv.Perm.ext_iff] at h
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
⊢ (x :: y :: l) ~r (x' :: y' :: l')
[PROOFSTEP]
have hx : x' ∈ x :: y :: l :=
  by
  have : x' ∈ {z | formPerm (x :: y :: l) z ≠ z} :=
    by
    rw [Set.mem_setOf_eq, h x', formPerm_apply_head _ _ _ hd']
    simp only [mem_cons, nodup_cons] at hd'
    push_neg at hd'
    exact hd'.left.left.symm
  simpa using support_formPerm_le' _ this
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
⊢ x' ∈ x :: y :: l
[PROOFSTEP]
have : x' ∈ {z | formPerm (x :: y :: l) z ≠ z} :=
  by
  rw [Set.mem_setOf_eq, h x', formPerm_apply_head _ _ _ hd']
  simp only [mem_cons, nodup_cons] at hd'
  push_neg at hd'
  exact hd'.left.left.symm
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
⊢ x' ∈ {z | ↑(formPerm (x :: y :: l)) z ≠ z}
[PROOFSTEP]
rw [Set.mem_setOf_eq, h x', formPerm_apply_head _ _ _ hd']
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
⊢ y' ≠ x'
[PROOFSTEP]
simp only [mem_cons, nodup_cons] at hd'
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
hd' : ¬(x' = y' ∨ x' ∈ l') ∧ ¬y' ∈ l' ∧ Nodup l'
⊢ y' ≠ x'
[PROOFSTEP]
push_neg at hd'
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
hd' : (x' ≠ y' ∧ ¬x' ∈ l') ∧ ¬y' ∈ l' ∧ Nodup l'
⊢ y' ≠ x'
[PROOFSTEP]
exact hd'.left.left.symm
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
this : x' ∈ {z | ↑(formPerm (x :: y :: l)) z ≠ z}
⊢ x' ∈ x :: y :: l
[PROOFSTEP]
simpa using support_formPerm_le' _ this
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
hx : x' ∈ x :: y :: l
⊢ (x :: y :: l) ~r (x' :: y' :: l')
[PROOFSTEP]
obtain ⟨n, hn, hx'⟩ := nthLe_of_mem hx
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < length (x :: y :: l)
hx' : nthLe (x :: y :: l) n hn = x'
⊢ (x :: y :: l) ~r (x' :: y' :: l')
[PROOFSTEP]
have hl : (x :: y :: l).length = (x' :: y' :: l').length :=
  by
  rw [← dedup_eq_self.mpr hd, ← dedup_eq_self.mpr hd', ← card_toFinset, ← card_toFinset]
  refine' congr_arg Finset.card _
  rw [← Finset.coe_inj, ← support_formPerm_of_nodup' _ hd (by simp), ← support_formPerm_of_nodup' _ hd' (by simp)]
  simp only [h]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < length (x :: y :: l)
hx' : nthLe (x :: y :: l) n hn = x'
⊢ length (x :: y :: l) = length (x' :: y' :: l')
[PROOFSTEP]
rw [← dedup_eq_self.mpr hd, ← dedup_eq_self.mpr hd', ← card_toFinset, ← card_toFinset]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < length (x :: y :: l)
hx' : nthLe (x :: y :: l) n hn = x'
⊢ Finset.card (toFinset (x :: y :: l)) = Finset.card (toFinset (x' :: y' :: l'))
[PROOFSTEP]
refine' congr_arg Finset.card _
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < length (x :: y :: l)
hx' : nthLe (x :: y :: l) n hn = x'
⊢ toFinset (x :: y :: l) = toFinset (x' :: y' :: l')
[PROOFSTEP]
rw [← Finset.coe_inj, ← support_formPerm_of_nodup' _ hd (by simp), ← support_formPerm_of_nodup' _ hd' (by simp)]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < length (x :: y :: l)
hx' : nthLe (x :: y :: l) n hn = x'
⊢ ∀ (x_1 : α), x :: y :: l ≠ [x_1]
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < length (x :: y :: l)
hx' : nthLe (x :: y :: l) n hn = x'
⊢ ∀ (x : α), x' :: y' :: l' ≠ [x]
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < length (x :: y :: l)
hx' : nthLe (x :: y :: l) n hn = x'
⊢ {x_1 | ↑(formPerm (x :: y :: l)) x_1 ≠ x_1} = {x | ↑(formPerm (x' :: y' :: l')) x ≠ x}
[PROOFSTEP]
simp only [h]
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < length (x :: y :: l)
hx' : nthLe (x :: y :: l) n hn = x'
hl : length (x :: y :: l) = length (x' :: y' :: l')
⊢ (x :: y :: l) ~r (x' :: y' :: l')
[PROOFSTEP]
use n
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < length (x :: y :: l)
hx' : nthLe (x :: y :: l) n hn = x'
hl : length (x :: y :: l) = length (x' :: y' :: l')
⊢ rotate (x :: y :: l) n = x' :: y' :: l'
[PROOFSTEP]
apply List.ext_nthLe
[GOAL]
case h.hl
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < length (x :: y :: l)
hx' : nthLe (x :: y :: l) n hn = x'
hl : length (x :: y :: l) = length (x' :: y' :: l')
⊢ length (rotate (x :: y :: l) n) = length (x' :: y' :: l')
[PROOFSTEP]
rw [length_rotate, hl]
[GOAL]
case h.h
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < length (x :: y :: l)
hx' : nthLe (x :: y :: l) n hn = x'
hl : length (x :: y :: l) = length (x' :: y' :: l')
⊢ ∀ (n_1 : ℕ) (h₁ : n_1 < length (rotate (x :: y :: l) n)) (h₂ : n_1 < length (x' :: y' :: l')),
    nthLe (rotate (x :: y :: l) n) n_1 h₁ = nthLe (x' :: y' :: l') n_1 h₂
[PROOFSTEP]
intro k hk hk'
[GOAL]
case h.h
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < length (x :: y :: l)
hx' : nthLe (x :: y :: l) n hn = x'
hl : length (x :: y :: l) = length (x' :: y' :: l')
k : ℕ
hk : k < length (rotate (x :: y :: l) n)
hk' : k < length (x' :: y' :: l')
⊢ nthLe (rotate (x :: y :: l) n) k hk = nthLe (x' :: y' :: l') k hk'
[PROOFSTEP]
rw [nthLe_rotate]
[GOAL]
case h.h
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < length (x :: y :: l)
hx' : nthLe (x :: y :: l) n hn = x'
hl : length (x :: y :: l) = length (x' :: y' :: l')
k : ℕ
hk : k < length (rotate (x :: y :: l) n)
hk' : k < length (x' :: y' :: l')
⊢ nthLe (x :: y :: l) ((k + n) % length (x :: y :: l)) (_ : (k + n) % length (x :: y :: l) < length (x :: y :: l)) =
    nthLe (x' :: y' :: l') k hk'
[PROOFSTEP]
induction' k with k IH
[GOAL]
case h.h.zero
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < length (x :: y :: l)
hx' : nthLe (x :: y :: l) n hn = x'
hl : length (x :: y :: l) = length (x' :: y' :: l')
k : ℕ
hk✝ : k < length (rotate (x :: y :: l) n)
hk'✝ : k < length (x' :: y' :: l')
hk : Nat.zero < length (rotate (x :: y :: l) n)
hk' : Nat.zero < length (x' :: y' :: l')
⊢ nthLe (x :: y :: l) ((Nat.zero + n) % length (x :: y :: l))
      (_ : (Nat.zero + n) % length (x :: y :: l) < length (x :: y :: l)) =
    nthLe (x' :: y' :: l') Nat.zero hk'
[PROOFSTEP]
refine' Eq.trans _ hx'
[GOAL]
case h.h.zero
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < length (x :: y :: l)
hx' : nthLe (x :: y :: l) n hn = x'
hl : length (x :: y :: l) = length (x' :: y' :: l')
k : ℕ
hk✝ : k < length (rotate (x :: y :: l) n)
hk'✝ : k < length (x' :: y' :: l')
hk : Nat.zero < length (rotate (x :: y :: l) n)
hk' : Nat.zero < length (x' :: y' :: l')
⊢ nthLe (x :: y :: l) ((Nat.zero + n) % length (x :: y :: l))
      (_ : (Nat.zero + n) % length (x :: y :: l) < length (x :: y :: l)) =
    nthLe (x :: y :: l) n hn
[PROOFSTEP]
congr
[GOAL]
case h.h.zero.e_n
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < length (x :: y :: l)
hx' : nthLe (x :: y :: l) n hn = x'
hl : length (x :: y :: l) = length (x' :: y' :: l')
k : ℕ
hk✝ : k < length (rotate (x :: y :: l) n)
hk'✝ : k < length (x' :: y' :: l')
hk : Nat.zero < length (rotate (x :: y :: l) n)
hk' : Nat.zero < length (x' :: y' :: l')
⊢ (Nat.zero + n) % length (x :: y :: l) = n
[PROOFSTEP]
simpa using hn
[GOAL]
case h.h.succ
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < length (x :: y :: l)
hx' : nthLe (x :: y :: l) n hn = x'
hl : length (x :: y :: l) = length (x' :: y' :: l')
k✝ : ℕ
hk✝ : k✝ < length (rotate (x :: y :: l) n)
hk'✝ : k✝ < length (x' :: y' :: l')
k : ℕ
IH :
  ∀ (hk : k < length (rotate (x :: y :: l) n)) (hk' : k < length (x' :: y' :: l')),
    nthLe (x :: y :: l) ((k + n) % length (x :: y :: l)) (_ : (k + n) % length (x :: y :: l) < length (x :: y :: l)) =
      nthLe (x' :: y' :: l') k hk'
hk : Nat.succ k < length (rotate (x :: y :: l) n)
hk' : Nat.succ k < length (x' :: y' :: l')
⊢ nthLe (x :: y :: l) ((Nat.succ k + n) % length (x :: y :: l))
      (_ : (Nat.succ k + n) % length (x :: y :: l) < length (x :: y :: l)) =
    nthLe (x' :: y' :: l') (Nat.succ k) hk'
[PROOFSTEP]
have : k.succ = (k + 1) % (x' :: y' :: l').length := by rw [← Nat.succ_eq_add_one, Nat.mod_eq_of_lt hk']
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < length (x :: y :: l)
hx' : nthLe (x :: y :: l) n hn = x'
hl : length (x :: y :: l) = length (x' :: y' :: l')
k✝ : ℕ
hk✝ : k✝ < length (rotate (x :: y :: l) n)
hk'✝ : k✝ < length (x' :: y' :: l')
k : ℕ
IH :
  ∀ (hk : k < length (rotate (x :: y :: l) n)) (hk' : k < length (x' :: y' :: l')),
    nthLe (x :: y :: l) ((k + n) % length (x :: y :: l)) (_ : (k + n) % length (x :: y :: l) < length (x :: y :: l)) =
      nthLe (x' :: y' :: l') k hk'
hk : Nat.succ k < length (rotate (x :: y :: l) n)
hk' : Nat.succ k < length (x' :: y' :: l')
⊢ Nat.succ k = (k + 1) % length (x' :: y' :: l')
[PROOFSTEP]
rw [← Nat.succ_eq_add_one, Nat.mod_eq_of_lt hk']
[GOAL]
case h.h.succ
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < length (x :: y :: l)
hx' : nthLe (x :: y :: l) n hn = x'
hl : length (x :: y :: l) = length (x' :: y' :: l')
k✝ : ℕ
hk✝ : k✝ < length (rotate (x :: y :: l) n)
hk'✝ : k✝ < length (x' :: y' :: l')
k : ℕ
IH :
  ∀ (hk : k < length (rotate (x :: y :: l) n)) (hk' : k < length (x' :: y' :: l')),
    nthLe (x :: y :: l) ((k + n) % length (x :: y :: l)) (_ : (k + n) % length (x :: y :: l) < length (x :: y :: l)) =
      nthLe (x' :: y' :: l') k hk'
hk : Nat.succ k < length (rotate (x :: y :: l) n)
hk' : Nat.succ k < length (x' :: y' :: l')
this : Nat.succ k = (k + 1) % length (x' :: y' :: l')
⊢ nthLe (x :: y :: l) ((Nat.succ k + n) % length (x :: y :: l))
      (_ : (Nat.succ k + n) % length (x :: y :: l) < length (x :: y :: l)) =
    nthLe (x' :: y' :: l') (Nat.succ k) hk'
[PROOFSTEP]
simp_rw [this]
[GOAL]
case h.h.succ
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < length (x :: y :: l)
hx' : nthLe (x :: y :: l) n hn = x'
hl : length (x :: y :: l) = length (x' :: y' :: l')
k✝ : ℕ
hk✝ : k✝ < length (rotate (x :: y :: l) n)
hk'✝ : k✝ < length (x' :: y' :: l')
k : ℕ
IH :
  ∀ (hk : k < length (rotate (x :: y :: l) n)) (hk' : k < length (x' :: y' :: l')),
    nthLe (x :: y :: l) ((k + n) % length (x :: y :: l)) (_ : (k + n) % length (x :: y :: l) < length (x :: y :: l)) =
      nthLe (x' :: y' :: l') k hk'
hk : Nat.succ k < length (rotate (x :: y :: l) n)
hk' : Nat.succ k < length (x' :: y' :: l')
this : Nat.succ k = (k + 1) % length (x' :: y' :: l')
⊢ nthLe (x :: y :: l) (((k + 1) % length (x' :: y' :: l') + n) % length (x :: y :: l))
      (_ : ((k + 1) % length (x' :: y' :: l') + n) % length (x :: y :: l) < length (x :: y :: l)) =
    nthLe (x' :: y' :: l') ((k + 1) % length (x' :: y' :: l'))
      (_ : (k + 1) % length (x' :: y' :: l') < length (x' :: y' :: l'))
[PROOFSTEP]
rw [← formPerm_apply_nthLe _ hd' k (k.lt_succ_self.trans hk'), ← IH (k.lt_succ_self.trans hk), ← h,
  formPerm_apply_nthLe _ hd]
[GOAL]
case h.h.succ
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < length (x :: y :: l)
hx' : nthLe (x :: y :: l) n hn = x'
hl : length (x :: y :: l) = length (x' :: y' :: l')
k✝ : ℕ
hk✝ : k✝ < length (rotate (x :: y :: l) n)
hk'✝ : k✝ < length (x' :: y' :: l')
k : ℕ
IH :
  ∀ (hk : k < length (rotate (x :: y :: l) n)) (hk' : k < length (x' :: y' :: l')),
    nthLe (x :: y :: l) ((k + n) % length (x :: y :: l)) (_ : (k + n) % length (x :: y :: l) < length (x :: y :: l)) =
      nthLe (x' :: y' :: l') k hk'
hk : Nat.succ k < length (rotate (x :: y :: l) n)
hk' : Nat.succ k < length (x' :: y' :: l')
this : Nat.succ k = (k + 1) % length (x' :: y' :: l')
⊢ nthLe (x :: y :: l) (((k + 1) % length (x' :: y' :: l') + n) % length (x :: y :: l))
      (_ : ((k + 1) % length (x' :: y' :: l') + n) % length (x :: y :: l) < length (x :: y :: l)) =
    nthLe (x :: y :: l) (((k + n) % length (x :: y :: l) + 1) % length (x :: y :: l))
      (_ : ((k + n) % length (x :: y :: l) + 1) % length (x :: y :: l) < length (x :: y :: l))
[PROOFSTEP]
congr 1
[GOAL]
case h.h.succ.e_n
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < length (x :: y :: l)
hx' : nthLe (x :: y :: l) n hn = x'
hl : length (x :: y :: l) = length (x' :: y' :: l')
k✝ : ℕ
hk✝ : k✝ < length (rotate (x :: y :: l) n)
hk'✝ : k✝ < length (x' :: y' :: l')
k : ℕ
IH :
  ∀ (hk : k < length (rotate (x :: y :: l) n)) (hk' : k < length (x' :: y' :: l')),
    nthLe (x :: y :: l) ((k + n) % length (x :: y :: l)) (_ : (k + n) % length (x :: y :: l) < length (x :: y :: l)) =
      nthLe (x' :: y' :: l') k hk'
hk : Nat.succ k < length (rotate (x :: y :: l) n)
hk' : Nat.succ k < length (x' :: y' :: l')
this : Nat.succ k = (k + 1) % length (x' :: y' :: l')
⊢ ((k + 1) % length (x' :: y' :: l') + n) % length (x :: y :: l) =
    ((k + n) % length (x :: y :: l) + 1) % length (x :: y :: l)
[PROOFSTEP]
have h1 : 1 = 1 % (x' :: y' :: l').length := by simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < length (x :: y :: l)
hx' : nthLe (x :: y :: l) n hn = x'
hl : length (x :: y :: l) = length (x' :: y' :: l')
k✝ : ℕ
hk✝ : k✝ < length (rotate (x :: y :: l) n)
hk'✝ : k✝ < length (x' :: y' :: l')
k : ℕ
IH :
  ∀ (hk : k < length (rotate (x :: y :: l) n)) (hk' : k < length (x' :: y' :: l')),
    nthLe (x :: y :: l) ((k + n) % length (x :: y :: l)) (_ : (k + n) % length (x :: y :: l) < length (x :: y :: l)) =
      nthLe (x' :: y' :: l') k hk'
hk : Nat.succ k < length (rotate (x :: y :: l) n)
hk' : Nat.succ k < length (x' :: y' :: l')
this : Nat.succ k = (k + 1) % length (x' :: y' :: l')
⊢ 1 = 1 % length (x' :: y' :: l')
[PROOFSTEP]
simp
[GOAL]
case h.h.succ.e_n
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < length (x :: y :: l)
hx' : nthLe (x :: y :: l) n hn = x'
hl : length (x :: y :: l) = length (x' :: y' :: l')
k✝ : ℕ
hk✝ : k✝ < length (rotate (x :: y :: l) n)
hk'✝ : k✝ < length (x' :: y' :: l')
k : ℕ
IH :
  ∀ (hk : k < length (rotate (x :: y :: l) n)) (hk' : k < length (x' :: y' :: l')),
    nthLe (x :: y :: l) ((k + n) % length (x :: y :: l)) (_ : (k + n) % length (x :: y :: l) < length (x :: y :: l)) =
      nthLe (x' :: y' :: l') k hk'
hk : Nat.succ k < length (rotate (x :: y :: l) n)
hk' : Nat.succ k < length (x' :: y' :: l')
this : Nat.succ k = (k + 1) % length (x' :: y' :: l')
h1 : 1 = 1 % length (x' :: y' :: l')
⊢ ((k + 1) % length (x' :: y' :: l') + n) % length (x :: y :: l) =
    ((k + n) % length (x :: y :: l) + 1) % length (x :: y :: l)
[PROOFSTEP]
rw [hl, Nat.mod_eq_of_lt hk', h1, ← Nat.add_mod, Nat.succ_add, Nat.succ_eq_add_one]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l : List α
x✝ : α
hl : Nodup l
x : α
hx : x ∈ l
⊢ ↑(formPerm l) x = x ↔ length l ≤ 1
[PROOFSTEP]
obtain ⟨k, hk, rfl⟩ := nthLe_of_mem hx
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l : List α
x : α
hl : Nodup l
k : ℕ
hk : k < length l
hx : nthLe l k hk ∈ l
⊢ ↑(formPerm l) (nthLe l k hk) = nthLe l k hk ↔ length l ≤ 1
[PROOFSTEP]
rw [formPerm_apply_nthLe _ hl, hl.nthLe_inj_iff]
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l : List α
x : α
hl : Nodup l
k : ℕ
hk : k < length l
hx : nthLe l k hk ∈ l
⊢ (k + 1) % length l = k ↔ length l ≤ 1
[PROOFSTEP]
cases hn : l.length
[GOAL]
case intro.intro.zero
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l : List α
x : α
hl : Nodup l
k : ℕ
hk : k < length l
hx : nthLe l k hk ∈ l
hn : length l = Nat.zero
⊢ (k + 1) % Nat.zero = k ↔ Nat.zero ≤ 1
[PROOFSTEP]
exact absurd k.zero_le (hk.trans_le hn.le).not_le
[GOAL]
case intro.intro.succ
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l : List α
x : α
hl : Nodup l
k : ℕ
hk : k < length l
hx : nthLe l k hk ∈ l
n✝ : ℕ
hn : length l = Nat.succ n✝
⊢ (k + 1) % Nat.succ n✝ = k ↔ Nat.succ n✝ ≤ 1
[PROOFSTEP]
rw [hn] at hk
[GOAL]
case intro.intro.succ
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l : List α
x : α
hl : Nodup l
k : ℕ
hk✝ : k < length l
hx : nthLe l k hk✝ ∈ l
n✝ : ℕ
hk : k < Nat.succ n✝
hn : length l = Nat.succ n✝
⊢ (k + 1) % Nat.succ n✝ = k ↔ Nat.succ n✝ ≤ 1
[PROOFSTEP]
cases' (Nat.le_of_lt_succ hk).eq_or_lt with hk' hk'
[GOAL]
case intro.intro.succ.inl
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l : List α
x : α
hl : Nodup l
k : ℕ
hk✝ : k < length l
hx : nthLe l k hk✝ ∈ l
n✝ : ℕ
hk : k < Nat.succ n✝
hn : length l = Nat.succ n✝
hk' : k = n✝
⊢ (k + 1) % Nat.succ n✝ = k ↔ Nat.succ n✝ ≤ 1
[PROOFSTEP]
simp [← hk', Nat.succ_le_succ_iff, eq_comm]
[GOAL]
case intro.intro.succ.inr
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l : List α
x : α
hl : Nodup l
k : ℕ
hk✝ : k < length l
hx : nthLe l k hk✝ ∈ l
n✝ : ℕ
hk : k < Nat.succ n✝
hn : length l = Nat.succ n✝
hk' : k < n✝
⊢ (k + 1) % Nat.succ n✝ = k ↔ Nat.succ n✝ ≤ 1
[PROOFSTEP]
simpa [Nat.mod_eq_of_lt (Nat.succ_lt_succ hk'), Nat.succ_lt_succ_iff] using k.zero_le.trans_lt hk'
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l : List α
x✝ : α
hl : Nodup l
x : α
hx : x ∈ l
⊢ ↑(formPerm l) x ≠ x ↔ 2 ≤ length l
[PROOFSTEP]
rw [Ne.def, formPerm_apply_mem_eq_self_iff _ hl x hx, not_le]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l : List α
x✝ : α
hl : Nodup l
x : α
hx : x ∈ l
⊢ 1 < length l ↔ 2 ≤ length l
[PROOFSTEP]
exact ⟨Nat.succ_le_of_lt, Nat.lt_of_succ_le⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l : List α
x : α
h : ↑(formPerm l) x ≠ x
⊢ x ∈ l
[PROOFSTEP]
suffices x ∈ {y | formPerm l y ≠ y} by
  rw [← mem_toFinset]
  exact support_formPerm_le' _ this
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l : List α
x : α
h : ↑(formPerm l) x ≠ x
this : x ∈ {y | ↑(formPerm l) y ≠ y}
⊢ x ∈ l
[PROOFSTEP]
rw [← mem_toFinset]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l : List α
x : α
h : ↑(formPerm l) x ≠ x
this : x ∈ {y | ↑(formPerm l) y ≠ y}
⊢ x ∈ toFinset l
[PROOFSTEP]
exact support_formPerm_le' _ this
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l : List α
x : α
h : ↑(formPerm l) x ≠ x
⊢ x ∈ {y | ↑(formPerm l) y ≠ y}
[PROOFSTEP]
simpa using h
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l : List α
x : α
hl : Nodup l
⊢ formPerm l = 1 ↔ length l ≤ 1
[PROOFSTEP]
cases' l with hd tl
[GOAL]
case nil
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
x : α
hl : Nodup []
⊢ formPerm [] = 1 ↔ length [] ≤ 1
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
x hd : α
tl : List α
hl : Nodup (hd :: tl)
⊢ formPerm (hd :: tl) = 1 ↔ length (hd :: tl) ≤ 1
[PROOFSTEP]
rw [← formPerm_apply_mem_eq_self_iff _ hl hd (mem_cons_self _ _)]
[GOAL]
case cons
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
x hd : α
tl : List α
hl : Nodup (hd :: tl)
⊢ formPerm (hd :: tl) = 1 ↔ ↑(formPerm (hd :: tl)) hd = hd
[PROOFSTEP]
constructor
[GOAL]
case cons.mp
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
x hd : α
tl : List α
hl : Nodup (hd :: tl)
⊢ formPerm (hd :: tl) = 1 → ↑(formPerm (hd :: tl)) hd = hd
[PROOFSTEP]
simp (config := { contextual := true })
[GOAL]
case cons.mpr
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
x hd : α
tl : List α
hl : Nodup (hd :: tl)
⊢ ↑(formPerm (hd :: tl)) hd = hd → formPerm (hd :: tl) = 1
[PROOFSTEP]
intro h
[GOAL]
case cons.mpr
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
x hd : α
tl : List α
hl : Nodup (hd :: tl)
h : ↑(formPerm (hd :: tl)) hd = hd
⊢ formPerm (hd :: tl) = 1
[PROOFSTEP]
simp only [(hd :: tl).formPerm_apply_mem_eq_self_iff hl hd (mem_cons_self hd tl), add_le_iff_nonpos_left, length,
  nonpos_iff_eq_zero, length_eq_zero] at h
[GOAL]
case cons.mpr
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
x hd : α
tl : List α
hl : Nodup (hd :: tl)
h : tl = []
⊢ formPerm (hd :: tl) = 1
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x : α
l l' : List α
hl : Nodup l
hl' : Nodup l'
⊢ formPerm l = formPerm l' ↔ l ~r l' ∨ length l ≤ 1 ∧ length l' ≤ 1
[PROOFSTEP]
rcases l with (_ | ⟨x, _ | ⟨y, l⟩⟩)
[GOAL]
case nil
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l : List α
x : α
l' : List α
hl' : Nodup l'
hl : Nodup []
⊢ formPerm [] = formPerm l' ↔ [] ~r l' ∨ length [] ≤ 1 ∧ length l' ≤ 1
[PROOFSTEP]
suffices l'.length ≤ 1 ↔ l' = nil ∨ l'.length ≤ 1 by simpa [eq_comm, formPerm_eq_one_iff, hl, hl', length_eq_zero]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l : List α
x : α
l' : List α
hl' : Nodup l'
hl : Nodup []
this : length l' ≤ 1 ↔ l' = [] ∨ length l' ≤ 1
⊢ formPerm [] = formPerm l' ↔ [] ~r l' ∨ length [] ≤ 1 ∧ length l' ≤ 1
[PROOFSTEP]
simpa [eq_comm, formPerm_eq_one_iff, hl, hl', length_eq_zero]
[GOAL]
case nil
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l : List α
x : α
l' : List α
hl' : Nodup l'
hl : Nodup []
⊢ length l' ≤ 1 ↔ l' = [] ∨ length l' ≤ 1
[PROOFSTEP]
refine' ⟨fun h => Or.inr h, _⟩
[GOAL]
case nil
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l : List α
x : α
l' : List α
hl' : Nodup l'
hl : Nodup []
⊢ l' = [] ∨ length l' ≤ 1 → length l' ≤ 1
[PROOFSTEP]
rintro (rfl | h)
[GOAL]
case nil.inl
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l : List α
x : α
hl hl' : Nodup []
⊢ length [] ≤ 1
[PROOFSTEP]
simp
[GOAL]
case nil.inr
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l : List α
x : α
l' : List α
hl' : Nodup l'
hl : Nodup []
h : length l' ≤ 1
⊢ length l' ≤ 1
[PROOFSTEP]
exact h
[GOAL]
case cons.nil
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l : List α
x✝ : α
l' : List α
hl' : Nodup l'
x : α
hl : Nodup [x]
⊢ formPerm [x] = formPerm l' ↔ [x] ~r l' ∨ length [x] ≤ 1 ∧ length l' ≤ 1
[PROOFSTEP]
suffices l'.length ≤ 1 ↔ [x] ~r l' ∨ l'.length ≤ 1 by
  simpa [eq_comm, formPerm_eq_one_iff, hl, hl', length_eq_zero, le_rfl]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l : List α
x✝ : α
l' : List α
hl' : Nodup l'
x : α
hl : Nodup [x]
this : length l' ≤ 1 ↔ [x] ~r l' ∨ length l' ≤ 1
⊢ formPerm [x] = formPerm l' ↔ [x] ~r l' ∨ length [x] ≤ 1 ∧ length l' ≤ 1
[PROOFSTEP]
simpa [eq_comm, formPerm_eq_one_iff, hl, hl', length_eq_zero, le_rfl]
[GOAL]
case cons.nil
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l : List α
x✝ : α
l' : List α
hl' : Nodup l'
x : α
hl : Nodup [x]
⊢ length l' ≤ 1 ↔ [x] ~r l' ∨ length l' ≤ 1
[PROOFSTEP]
refine' ⟨fun h => Or.inr h, _⟩
[GOAL]
case cons.nil
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l : List α
x✝ : α
l' : List α
hl' : Nodup l'
x : α
hl : Nodup [x]
⊢ [x] ~r l' ∨ length l' ≤ 1 → length l' ≤ 1
[PROOFSTEP]
rintro (h | h)
[GOAL]
case cons.nil.inl
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l : List α
x✝ : α
l' : List α
hl' : Nodup l'
x : α
hl : Nodup [x]
h : [x] ~r l'
⊢ length l' ≤ 1
[PROOFSTEP]
simp [← h.perm.length_eq]
[GOAL]
case cons.nil.inr
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l : List α
x✝ : α
l' : List α
hl' : Nodup l'
x : α
hl : Nodup [x]
h : length l' ≤ 1
⊢ length l' ≤ 1
[PROOFSTEP]
exact h
[GOAL]
case cons.cons
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l' : List α
hl' : Nodup l'
x y : α
l : List α
hl : Nodup (x :: y :: l)
⊢ formPerm (x :: y :: l) = formPerm l' ↔ (x :: y :: l) ~r l' ∨ length (x :: y :: l) ≤ 1 ∧ length l' ≤ 1
[PROOFSTEP]
rcases l' with (_ | ⟨x', _ | ⟨y', l'⟩⟩)
[GOAL]
case cons.cons.nil
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hl : Nodup (x :: y :: l)
hl' : Nodup []
⊢ formPerm (x :: y :: l) = formPerm [] ↔ (x :: y :: l) ~r [] ∨ length (x :: y :: l) ≤ 1 ∧ length [] ≤ 1
[PROOFSTEP]
simp [formPerm_eq_one_iff _ hl, -formPerm_cons_cons]
[GOAL]
case cons.cons.cons.nil
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hl : Nodup (x :: y :: l)
x' : α
hl' : Nodup [x']
⊢ formPerm (x :: y :: l) = formPerm [x'] ↔ (x :: y :: l) ~r [x'] ∨ length (x :: y :: l) ≤ 1 ∧ length [x'] ≤ 1
[PROOFSTEP]
simp [formPerm_eq_one_iff _ hl, -formPerm_cons_cons]
[GOAL]
case cons.cons.cons.cons
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
hl : Nodup (x :: y :: l)
x' y' : α
l' : List α
hl' : Nodup (x' :: y' :: l')
⊢ formPerm (x :: y :: l) = formPerm (x' :: y' :: l') ↔
    (x :: y :: l) ~r (x' :: y' :: l') ∨ length (x :: y :: l) ≤ 1 ∧ length (x' :: y' :: l') ≤ 1
[PROOFSTEP]
simp [-formPerm_cons_cons, formPerm_ext_iff hl hl', Nat.succ_le_succ_iff]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l : List α
x : α
hx : x ∈ l
n : ℤ
⊢ ↑(formPerm l ^ n) x ∈ l
[PROOFSTEP]
by_cases h : (l.formPerm ^ n) x = x
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l : List α
x : α
hx : x ∈ l
n : ℤ
h : ↑(formPerm l ^ n) x = x
⊢ ↑(formPerm l ^ n) x ∈ l
[PROOFSTEP]
simpa [h] using hx
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l : List α
x : α
hx : x ∈ l
n : ℤ
h : ¬↑(formPerm l ^ n) x = x
⊢ ↑(formPerm l ^ n) x ∈ l
[PROOFSTEP]
have h : x ∈ {x | (l.formPerm ^ n) x ≠ x} := h
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l : List α
x : α
hx : x ∈ l
n : ℤ
h✝ : ¬↑(formPerm l ^ n) x = x
h : x ∈ {x | ↑(formPerm l ^ n) x ≠ x}
⊢ ↑(formPerm l ^ n) x ∈ l
[PROOFSTEP]
rw [← set_support_apply_mem] at h
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l : List α
x : α
hx : x ∈ l
n : ℤ
h✝ : ¬↑(formPerm l ^ n) x = x
h : ↑(formPerm l ^ n) x ∈ {x | ↑(formPerm l ^ n) x ≠ x}
⊢ ↑(formPerm l ^ n) x ∈ l
[PROOFSTEP]
replace h := set_support_zpow_subset _ _ h
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l : List α
x : α
hx : x ∈ l
n : ℤ
h✝ : ¬↑(formPerm l ^ n) x = x
h : ↑(formPerm l ^ n) x ∈ {x_1 | ↑(formPerm l) x_1 ≠ x_1}
⊢ ↑(formPerm l ^ n) x ∈ l
[PROOFSTEP]
simpa using support_formPerm_le' _ h
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l : List α
x : α
hl : Nodup l
⊢ formPerm l ^ length l = 1
[PROOFSTEP]
ext x
[GOAL]
case H
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l : List α
x✝ : α
hl : Nodup l
x : α
⊢ ↑(formPerm l ^ length l) x = ↑1 x
[PROOFSTEP]
by_cases hx : x ∈ l
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l : List α
x✝ : α
hl : Nodup l
x : α
hx : x ∈ l
⊢ ↑(formPerm l ^ length l) x = ↑1 x
[PROOFSTEP]
obtain ⟨k, hk, rfl⟩ := nthLe_of_mem hx
[GOAL]
case pos.intro.intro
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l : List α
x : α
hl : Nodup l
k : ℕ
hk : k < length l
hx : nthLe l k hk ∈ l
⊢ ↑(formPerm l ^ length l) (nthLe l k hk) = ↑1 (nthLe l k hk)
[PROOFSTEP]
simp [formPerm_pow_apply_nthLe _ hl, Nat.mod_eq_of_lt hk]
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l : List α
x✝ : α
hl : Nodup l
x : α
hx : ¬x ∈ l
⊢ ↑(formPerm l ^ length l) x = ↑1 x
[PROOFSTEP]
have : x ∉ {x | (l.formPerm ^ l.length) x ≠ x} := by
  intro H
  refine' hx _
  replace H := set_support_zpow_subset l.formPerm l.length H
  simpa using support_formPerm_le' _ H
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l : List α
x✝ : α
hl : Nodup l
x : α
hx : ¬x ∈ l
⊢ ¬x ∈ {x | ↑(formPerm l ^ length l) x ≠ x}
[PROOFSTEP]
intro H
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l : List α
x✝ : α
hl : Nodup l
x : α
hx : ¬x ∈ l
H : x ∈ {x | ↑(formPerm l ^ length l) x ≠ x}
⊢ False
[PROOFSTEP]
refine' hx _
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l : List α
x✝ : α
hl : Nodup l
x : α
hx : ¬x ∈ l
H : x ∈ {x | ↑(formPerm l ^ length l) x ≠ x}
⊢ x ∈ l
[PROOFSTEP]
replace H := set_support_zpow_subset l.formPerm l.length H
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l : List α
x✝ : α
hl : Nodup l
x : α
hx : ¬x ∈ l
H : x ∈ {x | ↑(formPerm l) x ≠ x}
⊢ x ∈ l
[PROOFSTEP]
simpa using support_formPerm_le' _ H
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l : List α
x✝ : α
hl : Nodup l
x : α
hx : ¬x ∈ l
this : ¬x ∈ {x | ↑(formPerm l ^ length l) x ≠ x}
⊢ ↑(formPerm l ^ length l) x = ↑1 x
[PROOFSTEP]
simpa using this