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

case cons
α : Type u_1
β : Type ?u.4870
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
h : x ∈ y :: l
⊢ ↑(formPerm (y :: l)) x ∈ y :: l
α : Type u_1
β : Type ?u.4870
inst✝ : DecidableEq α
l✝ : List α
x✝ x : α
l : List α
h : x ∈ l
⊢ ↑(formPerm l) x ∈ l
cases' l with y l
case cons.nil
α : Type u_1
β : Type ?u.4870
inst✝ : DecidableEq α
l✝ : List α
x✝¹ x✝ y✝ : α
l : List α
h✝ : x✝ ∈ y✝ :: l
x y : α
h : x ∈ [y]
⊢ ↑(formPerm [y]) x ∈ [y]

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

case neg
α : Type u_1
β : Type ?u.4870
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
case cons.cons
α : Type u_1
β : Type ?u.4870
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
by_cases hx : x ∈ z :: l
case pos
α : Type u_1
β : Type ?u.4870
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
case pos
α : Type u_1
β : Type ?u.4870
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
rw [formPerm_cons_cons, mul_apply, swap_apply_def]
case pos.inl
α : Type u_1
β : Type ?u.4870
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

case pos.inr.inl
α : Type u_1
β : Type ?u.4870
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

case pos.inr.inr
α : Type u_1
β : Type ?u.4870
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
case pos
α : Type u_1
β : Type ?u.4870
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
split_ifs
case pos.inr.inl
α : Type u_1
β : Type ?u.4870
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

case pos.inr.inr
α : Type u_1
β : Type ?u.4870
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
case pos.inl
α : Type u_1
β : Type ?u.4870
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

case pos.inr.inl
α : Type u_1
β : Type ?u.4870
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

case pos.inr.inr
α : Type u_1
β : Type ?u.4870
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
. simp [IH _ _ hx]
case pos.inr.inr
α : Type u_1
β : Type ?u.4870
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
case pos.inr.inl
α : Type u_1
β : Type ?u.4870
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

case pos.inr.inr
α : Type u_1
β : Type ?u.4870
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
. simp
no goals
case pos.inr.inr
α : Type u_1
β : Type ?u.4870
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
. simpa [*] using IH _ _ hx
no goals
case pos.inl
α : Type u_1
β : Type ?u.4870
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
simp [IH _ _ hx]
no goals
case pos.inr.inl
α : Type u_1
β : Type ?u.4870
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
simp
no goals
case pos.inr.inr
α : Type u_1
β : Type ?u.4870
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
simpa [*] using IH _ _ hx
case neg
α : Type u_1
β : Type ?u.4870
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
case neg
α : Type u_1
β : Type ?u.4870
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
replace h : x = y := Or.resolve_right (mem_cons.1 h) hx
no goals
case neg
α : Type u_1
β : Type ?u.4870
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
simp [formPerm_apply_of_not_mem _ _ hx, ← h]