case nil
α : Type u_1
β : Type ?u.47566
inst✝ : DecidableEq α
l : List α
x✝ x : α
h : ↑(formPerm []) x ∈ []
⊢ x ∈ []

case cons
α : Type u_1
β : Type ?u.47566
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
h : ↑(formPerm (y :: l)) x ∈ y :: l
⊢ x ∈ y :: l
α : Type u_1
β : Type ?u.47566
inst✝ : DecidableEq α
l✝ : List α
x✝ x : α
l : List α
h : ↑(formPerm l) x ∈ l
⊢ x ∈ l
cases' l with y l
case cons.nil
α : Type u_1
β : Type ?u.47566
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]

case cons.cons
α : Type u_1
β : Type ?u.47566
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
case cons
α : Type u_1
β : Type ?u.47566
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
h : ↑(formPerm (y :: l)) x ∈ y :: l
⊢ x ∈ y :: l
induction' l with z l IH generalizing x y
no goals
case nil
α : Type u_1
β : Type ?u.47566
inst✝ : DecidableEq α
l : List α
x✝ x : α
h : ↑(formPerm []) x ∈ []
⊢ x ∈ []
simp at h
no goals
case cons.nil
α : Type u_1
β : Type ?u.47566
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]
simpa using h
case pos
α : Type u_1
β : Type ?u.47566
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

case neg
α : Type u_1
β : Type ?u.47566
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
case cons.cons
α : Type u_1
β : Type ?u.47566
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
by_cases hx : (z :: l).formPerm x ∈ z :: l
case pos
α : Type u_1
β : Type ?u.47566
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
case pos
α : Type u_1
β : Type ?u.47566
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
rw [List.formPerm_cons_cons, mul_apply, swap_apply_def] at h
no goals
case pos
α : Type u_1
β : Type ?u.47566
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
split_ifs at h <;> aesop
case neg
α : Type u_1
β : Type ?u.47566
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
case neg
α : Type u_1
β : Type ?u.47566
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
replace hx :=
  (Function.Injective.eq_iff (Equiv.injective _)).mp (List.formPerm_apply_of_not_mem _ _ hx)
case neg
α : Type u_1
β : Type ?u.47566
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
case neg
α : Type u_1
β : Type ?u.47566
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
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
case neg
α : Type u_1
β : Type ?u.47566
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
case neg
α : Type u_1
β : Type ?u.47566
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
simp only [List.mem_cons]
case neg.inr.inl.inr
α : Type u_1
β : Type ?u.47566
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
case neg
α : Type u_1
β : Type ?u.47566
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
rcases h with h | h | h <;> split_ifs at h with h1 <;> try { aesop }
no goals
case neg.inr.inl.inr
α : Type u_1
β : Type ?u.47566
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
. simp [h1, imp_false] at h
  simp [h]
case neg.inr.inl.inr
α : Type u_1
β : Type ?u.47566
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
case neg.inr.inl.inr
α : Type u_1
β : Type ?u.47566
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
simp [h1, imp_false] at h
no goals
case neg.inr.inl.inr
α : Type u_1
β : Type ?u.47566
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
simp [h]