-- Mathlib/GroupTheory/Perm/List.lean
theorem formPerm_eq_formPerm_iff {l l' : List α} (hl : l.Nodup) (hl' : l'.Nodup) :
    l.formPerm = l'.formPerm ↔ l ~r l' ∨ l.length ≤ 1 ∧ l'.length ≤ 1

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l' : List α
hl' : l'.Nodup
hl : [].Nodup
this : l'.length ≤ 1 ↔ l' = [] ∨ l'.length ≤ 1
⊢ [].formPerm = l'.formPerm ↔ [] ~r l' ∨ [].length ≤ 1 ∧ l'.length ≤ 1

Tactic:
simpa [eq_comm, formPerm_eq_one_iff, hl, hl', length_eq_zero]

Result:
no goals

Proof state:
case cons.cons
α : Type u_1
inst✝ : DecidableEq α
l' : List α
hl' : l'.Nodup
x y : α
l : List α
hl : (x :: y :: l).Nodup
⊢ (x :: y :: l).formPerm = l'.formPerm ↔ x :: y :: l ~r l' ∨ (x :: y :: l).length ≤ 1 ∧ l'.length ≤ 1

Tactic:
rcases l' with (_ | ⟨x', _ | ⟨y', l'⟩⟩)

Result:
case cons.cons.nil
α : Type u_1
inst✝ : DecidableEq α
x y : α
l : List α
hl : (x :: y :: l).Nodup
hl' : [].Nodup
⊢ (x :: y :: l).formPerm = [].formPerm ↔ x :: y :: l ~r [] ∨ (x :: y :: l).length ≤ 1 ∧ [].length ≤ 1

case cons.cons.cons.nil
α : Type u_1
inst✝ : DecidableEq α
x y : α
l : List α
hl : (x :: y :: l).Nodup
x' : α
hl' : [x'].Nodup
⊢ (x :: y :: l).formPerm = [x'].formPerm ↔ x :: y :: l ~r [x'] ∨ (x :: y :: l).length ≤ 1 ∧ [x'].length ≤ 1

case cons.cons.cons.cons
α : Type u_1
inst✝ : DecidableEq α
x y : α
l : List α
hl : (x :: y :: l).Nodup
x' y' : α
l' : List α
hl' : (x' :: y' :: l').Nodup
⊢ (x :: y :: l).formPerm = (x' :: y' :: l').formPerm ↔
    x :: y :: l ~r x' :: y' :: l' ∨ (x :: y :: l).length ≤ 1 ∧ (x' :: y' :: l').length ≤ 1

Proof state:
case cons.cons.nil
α : Type u_1
inst✝ : DecidableEq α
x y : α
l : List α
hl : (x :: y :: l).Nodup
hl' : [].Nodup
⊢ (x :: y :: l).formPerm = [].formPerm ↔ x :: y :: l ~r [] ∨ (x :: y :: l).length ≤ 1 ∧ [].length ≤ 1

Tactic:
simp [formPerm_eq_one_iff _ hl, -formPerm_cons_cons]

Result:
no goals

Proof state:
case nil.inl
α : Type u_1
inst✝ : DecidableEq α
hl hl' : [].Nodup
⊢ [].length ≤ 1

Tactic:
simp

Result:
no goals

Proof state:
case nil
α : Type u_1
inst✝ : DecidableEq α
l' : List α
hl' : l'.Nodup
hl : [].Nodup
⊢ l' = [] ∨ l'.length ≤ 1 → l'.length ≤ 1

Tactic:
rintro (rfl | h)

Result:
case nil.inl
α : Type u_1
inst✝ : DecidableEq α
hl hl' : [].Nodup
⊢ [].length ≤ 1

case nil.inr
α : Type u_1
inst✝ : DecidableEq α
l' : List α
hl' : l'.Nodup
hl : [].Nodup
h : l'.length ≤ 1
⊢ l'.length ≤ 1

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

Tactic:
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]

Result:
case cons.nil
α : Type u_1
inst✝ : DecidableEq α
l' : List α
hl' : l'.Nodup
x : α
hl : [x].Nodup
⊢ l'.length ≤ 1 ↔ [x] ~r l' ∨ l'.length ≤ 1

Proof state:
case cons.nil.inl
α : Type u_1
inst✝ : DecidableEq α
l' : List α
hl' : l'.Nodup
x : α
hl : [x].Nodup
h : [x] ~r l'
⊢ l'.length ≤ 1

Tactic:
simp [← h.perm.length_eq]

Result:
no goals

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

Tactic:
suffices l'.length ≤ 1 ↔ l' = nil ∨ l'.length ≤ 1 by
  simpa [eq_comm, formPerm_eq_one_iff, hl, hl', length_eq_zero]

Result:
case nil
α : Type u_1
inst✝ : DecidableEq α
l' : List α
hl' : l'.Nodup
hl : [].Nodup
⊢ l'.length ≤ 1 ↔ l' = [] ∨ l'.length ≤ 1

Proof state:
case cons.cons.cons.nil
α : Type u_1
inst✝ : DecidableEq α
x y : α
l : List α
hl : (x :: y :: l).Nodup
x' : α
hl' : [x'].Nodup
⊢ (x :: y :: l).formPerm = [x'].formPerm ↔ x :: y :: l ~r [x'] ∨ (x :: y :: l).length ≤ 1 ∧ [x'].length ≤ 1

Tactic:
simp [formPerm_eq_one_iff _ hl, -formPerm_cons_cons]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l' : List α
hl' : l'.Nodup
x : α
hl : [x].Nodup
this : l'.length ≤ 1 ↔ [x] ~r l' ∨ l'.length ≤ 1
⊢ [x].formPerm = l'.formPerm ↔ [x] ~r l' ∨ [x].length ≤ 1 ∧ l'.length ≤ 1

Tactic:
simpa [eq_comm, formPerm_eq_one_iff, hl, hl', length_eq_zero, le_rfl]

Result:
no goals

Proof state:
case cons.nil.inr
α : Type u_1
inst✝ : DecidableEq α
l' : List α
hl' : l'.Nodup
x : α
hl : [x].Nodup
h : l'.length ≤ 1
⊢ l'.length ≤ 1

Tactic:
exact h

Result:
no goals

Proof state:
case cons.nil
α : Type u_1
inst✝ : DecidableEq α
l' : List α
hl' : l'.Nodup
x : α
hl : [x].Nodup
⊢ l'.length ≤ 1 ↔ [x] ~r l' ∨ l'.length ≤ 1

Tactic:
refine ⟨fun h => Or.inr h, ?_⟩

Result:
case cons.nil
α : Type u_1
inst✝ : DecidableEq α
l' : List α
hl' : l'.Nodup
x : α
hl : [x].Nodup
⊢ [x] ~r l' ∨ l'.length ≤ 1 → l'.length ≤ 1

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : l.Nodup
hl' : l'.Nodup
⊢ l.formPerm = l'.formPerm ↔ l ~r l' ∨ l.length ≤ 1 ∧ l'.length ≤ 1

Tactic:
rcases l with (_ | ⟨x, _ | ⟨y, l⟩⟩)

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

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

case cons.cons
α : Type u_1
inst✝ : DecidableEq α
l' : List α
hl' : l'.Nodup
x y : α
l : List α
hl : (x :: y :: l).Nodup
⊢ (x :: y :: l).formPerm = l'.formPerm ↔ x :: y :: l ~r l' ∨ (x :: y :: l).length ≤ 1 ∧ l'.length ≤ 1

Proof state:
case nil.inr
α : Type u_1
inst✝ : DecidableEq α
l' : List α
hl' : l'.Nodup
hl : [].Nodup
h : l'.length ≤ 1
⊢ l'.length ≤ 1

Tactic:
exact h

Result:
no goals

Proof state:
case cons.nil
α : Type u_1
inst✝ : DecidableEq α
l' : List α
hl' : l'.Nodup
x : α
hl : [x].Nodup
⊢ [x] ~r l' ∨ l'.length ≤ 1 → l'.length ≤ 1

Tactic:
rintro (h | h)

Result:
case cons.nil.inl
α : Type u_1
inst✝ : DecidableEq α
l' : List α
hl' : l'.Nodup
x : α
hl : [x].Nodup
h : [x] ~r l'
⊢ l'.length ≤ 1

case cons.nil.inr
α : Type u_1
inst✝ : DecidableEq α
l' : List α
hl' : l'.Nodup
x : α
hl : [x].Nodup
h : l'.length ≤ 1
⊢ l'.length ≤ 1

Proof state:
case cons.cons.cons.cons
α : Type u_1
inst✝ : DecidableEq α
x y : α
l : List α
hl : (x :: y :: l).Nodup
x' y' : α
l' : List α
hl' : (x' :: y' :: l').Nodup
⊢ (x :: y :: l).formPerm = (x' :: y' :: l').formPerm ↔
    x :: y :: l ~r x' :: y' :: l' ∨ (x :: y :: l).length ≤ 1 ∧ (x' :: y' :: l').length ≤ 1

Tactic:
simp [-formPerm_cons_cons, formPerm_ext_iff hl hl', Nat.succ_le_succ_iff]

Result:
no goals

Proof state:
case nil
α : Type u_1
inst✝ : DecidableEq α
l' : List α
hl' : l'.Nodup
hl : [].Nodup
⊢ l'.length ≤ 1 ↔ l' = [] ∨ l'.length ≤ 1

Tactic:
refine ⟨fun h => Or.inr h, ?_⟩

Result:
case nil
α : Type u_1
inst✝ : DecidableEq α
l' : List α
hl' : l'.Nodup
hl : [].Nodup
⊢ l' = [] ∨ l'.length ≤ 1 → l'.length ≤ 1