case nil
α : Type u_1
β : Type ?u.817926
inst✝ : DecidableEq α
x : α
hl : Nodup []
⊢ formPerm [] = 1 ↔ length [] ≤ 1

case cons
α : Type u_1
β : Type ?u.817926
inst✝ : DecidableEq α
x hd : α
tl : List α
hl : Nodup (hd :: tl)
⊢ formPerm (hd :: tl) = 1 ↔ length (hd :: tl) ≤ 1
α : Type u_1
β : Type ?u.817926
inst✝ : DecidableEq α
l : List α
x : α
hl : Nodup l
⊢ formPerm l = 1 ↔ length l ≤ 1
cases' l with hd tl
no goals
case nil
α : Type u_1
β : Type ?u.817926
inst✝ : DecidableEq α
x : α
hl : Nodup []
⊢ formPerm [] = 1 ↔ length [] ≤ 1
simp
case cons
α : Type u_1
β : Type ?u.817926
inst✝ : DecidableEq α
x hd : α
tl : List α
hl : Nodup (hd :: tl)
⊢ formPerm (hd :: tl) = 1 ↔ ↑(formPerm (hd :: tl)) hd = hd
case cons
α : Type u_1
β : Type ?u.817926
inst✝ : DecidableEq α
x hd : α
tl : List α
hl : Nodup (hd :: tl)
⊢ formPerm (hd :: tl) = 1 ↔ length (hd :: tl) ≤ 1
rw [← formPerm_apply_mem_eq_self_iff _ hl hd (mem_cons_self _ _)]
case cons.mp
α : Type u_1
β : Type ?u.817926
inst✝ : DecidableEq α
x hd : α
tl : List α
hl : Nodup (hd :: tl)
⊢ formPerm (hd :: tl) = 1 → ↑(formPerm (hd :: tl)) hd = hd

case cons.mpr
α : Type u_1
β : Type ?u.817926
inst✝ : DecidableEq α
x hd : α
tl : List α
hl : Nodup (hd :: tl)
⊢ ↑(formPerm (hd :: tl)) hd = hd → formPerm (hd :: tl) = 1
case cons
α : Type u_1
β : Type ?u.817926
inst✝ : DecidableEq α
x hd : α
tl : List α
hl : Nodup (hd :: tl)
⊢ formPerm (hd :: tl) = 1 ↔ ↑(formPerm (hd :: tl)) hd = hd
constructor
no goals
case cons.mp
α : Type u_1
β : Type ?u.817926
inst✝ : DecidableEq α
x hd : α
tl : List α
hl : Nodup (hd :: tl)
⊢ formPerm (hd :: tl) = 1 → ↑(formPerm (hd :: tl)) hd = hd
simp (config := { contextual := true })
case cons.mpr
α : Type u_1
β : Type ?u.817926
inst✝ : DecidableEq α
x hd : α
tl : List α
hl : Nodup (hd :: tl)
h : ↑(formPerm (hd :: tl)) hd = hd
⊢ formPerm (hd :: tl) = 1
case cons.mpr
α : Type u_1
β : Type ?u.817926
inst✝ : DecidableEq α
x hd : α
tl : List α
hl : Nodup (hd :: tl)
⊢ ↑(formPerm (hd :: tl)) hd = hd → formPerm (hd :: tl) = 1
intro h
case cons.mpr
α : Type u_1
β : Type ?u.817926
inst✝ : DecidableEq α
x hd : α
tl : List α
hl : Nodup (hd :: tl)
h : tl = []
⊢ formPerm (hd :: tl) = 1
case cons.mpr
α : Type u_1
β : Type ?u.817926
inst✝ : DecidableEq α
x hd : α
tl : List α
hl : Nodup (hd :: tl)
h : ↑(formPerm (hd :: tl)) hd = hd
⊢ formPerm (hd :: tl) = 1
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
no goals
case cons.mpr
α : Type u_1
β : Type ?u.817926
inst✝ : DecidableEq α
x hd : α
tl : List α
hl : Nodup (hd :: tl)
h : tl = []
⊢ formPerm (hd :: tl) = 1
simp [h]