case nil
α : Type u_1
β : Type ?u.820291
inst✝ : DecidableEq α
l : List α
x : α
l' : List α
hl' : Nodup l'
hl : Nodup []
⊢ formPerm [] = formPerm l' ↔ [] ~r l' ∨ length [] ≤ 1 ∧ length l' ≤ 1

case cons.nil
α : Type u_1
β : Type ?u.820291
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

case cons.cons
α : Type u_1
β : Type ?u.820291
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
α : Type u_1
β : Type ?u.820291
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
rcases l with (_ | ⟨x, _ | ⟨y, l⟩⟩)
case nil
α : Type u_1
β : Type ?u.820291
inst✝ : DecidableEq α
l : List α
x : α
l' : List α
hl' : Nodup l'
hl : Nodup []
⊢ length l' ≤ 1 ↔ l' = [] ∨ length l' ≤ 1
case nil
α : Type u_1
β : Type ?u.820291
inst✝ : DecidableEq α
l : List α
x : α
l' : List α
hl' : Nodup l'
hl : Nodup []
⊢ formPerm [] = formPerm l' ↔ [] ~r l' ∨ length [] ≤ 1 ∧ length l' ≤ 1
suffices l'.length ≤ 1 ↔ l' = nil ∨ l'.length ≤ 1 by
  simpa [eq_comm, formPerm_eq_one_iff, hl, hl', length_eq_zero]
case nil
α : Type u_1
β : Type ?u.820291
inst✝ : DecidableEq α
l : List α
x : α
l' : List α
hl' : Nodup l'
hl : Nodup []
⊢ l' = [] ∨ length l' ≤ 1 → length l' ≤ 1
case nil
α : Type u_1
β : Type ?u.820291
inst✝ : DecidableEq α
l : List α
x : α
l' : List α
hl' : Nodup l'
hl : Nodup []
⊢ length l' ≤ 1 ↔ l' = [] ∨ length l' ≤ 1
refine' ⟨fun h => Or.inr h, _⟩
case nil.inl
α : Type u_1
β : Type ?u.820291
inst✝ : DecidableEq α
l : List α
x : α
hl hl' : Nodup []
⊢ length [] ≤ 1

case nil.inr
α : Type u_1
β : Type ?u.820291
inst✝ : DecidableEq α
l : List α
x : α
l' : List α
hl' : Nodup l'
hl : Nodup []
h : length l' ≤ 1
⊢ length l' ≤ 1
case nil
α : Type u_1
β : Type ?u.820291
inst✝ : DecidableEq α
l : List α
x : α
l' : List α
hl' : Nodup l'
hl : Nodup []
⊢ l' = [] ∨ length l' ≤ 1 → length l' ≤ 1
rintro (rfl | h)
no goals
α : Type u_1
β : Type ?u.820291
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
simpa [eq_comm, formPerm_eq_one_iff, hl, hl', length_eq_zero]
no goals
case nil.inl
α : Type u_1
β : Type ?u.820291
inst✝ : DecidableEq α
l : List α
x : α
hl hl' : Nodup []
⊢ length [] ≤ 1
simp
no goals
case nil.inr
α : Type u_1
β : Type ?u.820291
inst✝ : DecidableEq α
l : List α
x : α
l' : List α
hl' : Nodup l'
hl : Nodup []
h : length l' ≤ 1
⊢ length l' ≤ 1
exact h
case cons.nil
α : Type u_1
β : Type ?u.820291
inst✝ : DecidableEq α
l : List α
x✝ : α
l' : List α
hl' : Nodup l'
x : α
hl : Nodup [x]
⊢ length l' ≤ 1 ↔ [x] ~r l' ∨ length l' ≤ 1
case cons.nil
α : Type u_1
β : Type ?u.820291
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
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]
case cons.nil
α : Type u_1
β : Type ?u.820291
inst✝ : DecidableEq α
l : List α
x✝ : α
l' : List α
hl' : Nodup l'
x : α
hl : Nodup [x]
⊢ [x] ~r l' ∨ length l' ≤ 1 → length l' ≤ 1
case cons.nil
α : Type u_1
β : Type ?u.820291
inst✝ : DecidableEq α
l : List α
x✝ : α
l' : List α
hl' : Nodup l'
x : α
hl : Nodup [x]
⊢ length l' ≤ 1 ↔ [x] ~r l' ∨ length l' ≤ 1
refine' ⟨fun h => Or.inr h, _⟩
case cons.nil.inl
α : Type u_1
β : Type ?u.820291
inst✝ : DecidableEq α
l : List α
x✝ : α
l' : List α
hl' : Nodup l'
x : α
hl : Nodup [x]
h : [x] ~r l'
⊢ length l' ≤ 1

case cons.nil.inr
α : Type u_1
β : Type ?u.820291
inst✝ : DecidableEq α
l : List α
x✝ : α
l' : List α
hl' : Nodup l'
x : α
hl : Nodup [x]
h : length l' ≤ 1
⊢ length l' ≤ 1
case cons.nil
α : Type u_1
β : Type ?u.820291
inst✝ : DecidableEq α
l : List α
x✝ : α
l' : List α
hl' : Nodup l'
x : α
hl : Nodup [x]
⊢ [x] ~r l' ∨ length l' ≤ 1 → length l' ≤ 1
rintro (h | h)
no goals
α : Type u_1
β : Type ?u.820291
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
simpa [eq_comm, formPerm_eq_one_iff, hl, hl', length_eq_zero, le_rfl]
no goals
case cons.nil.inl
α : Type u_1
β : Type ?u.820291
inst✝ : DecidableEq α
l : List α
x✝ : α
l' : List α
hl' : Nodup l'
x : α
hl : Nodup [x]
h : [x] ~r l'
⊢ length l' ≤ 1
simp [← h.perm.length_eq]
no goals
case cons.nil.inr
α : Type u_1
β : Type ?u.820291
inst✝ : DecidableEq α
l : List α
x✝ : α
l' : List α
hl' : Nodup l'
x : α
hl : Nodup [x]
h : length l' ≤ 1
⊢ length l' ≤ 1
exact h
case cons.cons.nil
α : Type u_1
β : Type ?u.820291
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

case cons.cons.cons.nil
α : Type u_1
β : Type ?u.820291
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

case cons.cons.cons.cons
α : Type u_1
β : Type ?u.820291
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
case cons.cons
α : Type u_1
β : Type ?u.820291
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
rcases l' with (_ | ⟨x', _ | ⟨y', l'⟩⟩)
no goals
case cons.cons.nil
α : Type u_1
β : Type ?u.820291
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
simp [formPerm_eq_one_iff _ hl, -formPerm_cons_cons]
no goals
case cons.cons.cons.nil
α : Type u_1
β : Type ?u.820291
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
simp [formPerm_eq_one_iff _ hl, -formPerm_cons_cons]
no goals
case cons.cons.cons.cons
α : Type u_1
β : Type ?u.820291
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
simp [-formPerm_cons_cons, formPerm_ext_iff hl hl', Nat.succ_le_succ_iff]