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

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

case cons.cons
α : Type u_1
β : Type ?u.3357
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
case cons
α : Type u_1
β : Type ?u.3357
inst✝ : DecidableEq α
l✝ : List α
x✝ x y : α
l : List α
h : ¬x ∈ y :: l
⊢ ↑(formPerm (y :: l)) x = x
induction' l with z l IH generalizing x y
no goals
case nil
α : Type u_1
β : Type ?u.3357
inst✝ : DecidableEq α
l : List α
x✝ x : α
h : ¬x ∈ []
⊢ ↑(formPerm []) x = x
simp
no goals
case cons.nil
α : Type u_1
β : Type ?u.3357
inst✝ : DecidableEq α
l✝ : List α
x✝¹ x✝ y✝ : α
l : List α
h✝ : ¬x✝ ∈ y✝ :: l
x y : α
h : ¬x ∈ [y]
⊢ ↑(formPerm [y]) x = x
simp
case cons.cons
α : Type u_1
β : Type ?u.3357
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
case cons.cons
α : Type u_1
β : Type ?u.3357
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
specialize IH x z (mt (mem_cons_of_mem y) h)
case cons.cons
α : Type u_1
β : Type ?u.3357
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
case cons.cons
α : Type u_1
β : Type ?u.3357
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
simp only [not_or, mem_cons] at h
no goals
case cons.cons
α : Type u_1
β : Type ?u.3357
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
simp [IH, swap_apply_of_ne_of_ne, h]