-- Mathlib/GroupTheory/Perm/List.lean
theorem formPerm_ext_iff {x y x' y' : α} {l l' : List α} (hd : Nodup (x :: y :: l))
    (hd' : Nodup (x' :: y' :: l')) :
    formPerm (x :: y :: l) = formPerm (x' :: y' :: l') ↔ (x :: y :: l) ~r (x' :: y' :: l')

Proof state:
case h.h
α : Type u_1
inst✝ : DecidableEq α
x y x' y' : α
l l' : List α
hd : (x :: y :: l).Nodup
hd' : (x' :: y' :: l').Nodup
h : ∀ (x_1 : α), (x :: y :: l).formPerm x_1 = (x' :: y' :: l').formPerm x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < (x :: y :: l).length
hx' : (x :: y :: l).get ⟨n, hn⟩ = x'
hl : (x :: y :: l).length = (x' :: y' :: l').length
k : ℕ
hk : k < ((x :: y :: l).rotate n).length
hk' : k < (x' :: y' :: l').length
⊢ (x :: y :: l)[(k + n) % (x :: y :: l).length] = (x' :: y' :: l')[k]

Tactic:
induction' k with k IH

Result:
case h.h.zero
α : Type u_1
inst✝ : DecidableEq α
x y x' y' : α
l l' : List α
hd : (x :: y :: l).Nodup
hd' : (x' :: y' :: l').Nodup
h : ∀ (x_1 : α), (x :: y :: l).formPerm x_1 = (x' :: y' :: l').formPerm x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < (x :: y :: l).length
hx' : (x :: y :: l).get ⟨n, hn⟩ = x'
hl : (x :: y :: l).length = (x' :: y' :: l').length
hk : 0 < ((x :: y :: l).rotate n).length
hk' : 0 < (x' :: y' :: l').length
⊢ (x :: y :: l)[(0 + n) % (x :: y :: l).length] = (x' :: y' :: l')[0]

case h.h.succ
α : Type u_1
inst✝ : DecidableEq α
x y x' y' : α
l l' : List α
hd : (x :: y :: l).Nodup
hd' : (x' :: y' :: l').Nodup
h : ∀ (x_1 : α), (x :: y :: l).formPerm x_1 = (x' :: y' :: l').formPerm x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < (x :: y :: l).length
hx' : (x :: y :: l).get ⟨n, hn⟩ = x'
hl : (x :: y :: l).length = (x' :: y' :: l').length
k : ℕ
IH :
  ∀ (hk : k < ((x :: y :: l).rotate n).length) (hk' : k < (x' :: y' :: l').length),
    (x :: y :: l)[(k + n) % (x :: y :: l).length] = (x' :: y' :: l')[k]
hk : k + 1 < ((x :: y :: l).rotate n).length
hk' : k + 1 < (x' :: y' :: l').length
⊢ (x :: y :: l)[(k + 1 + n) % (x :: y :: l).length] = (x' :: y' :: l')[k + 1]

Proof state:
case h.h.succ.e_i
α : Type u_1
inst✝ : DecidableEq α
x y x' y' : α
l l' : List α
hd : (x :: y :: l).Nodup
hd' : (x' :: y' :: l').Nodup
h : ∀ (x_1 : α), (x :: y :: l).formPerm x_1 = (x' :: y' :: l').formPerm x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < (x :: y :: l).length
hx' : (x :: y :: l).get ⟨n, hn⟩ = x'
hl : (x :: y :: l).length = (x' :: y' :: l').length
k : ℕ
IH :
  ∀ (hk : k < ((x :: y :: l).rotate n).length) (hk' : k < (x' :: y' :: l').length),
    (x :: y :: l)[(k + n) % (x :: y :: l).length] = (x' :: y' :: l')[k]
hk : k + 1 < ((x :: y :: l).rotate n).length
hk' : k + 1 < (x' :: y' :: l').length
⊢ (k + n + 1) % (x' :: y' :: l').length = ((k + n) % (x' :: y' :: l').length + 1) % (x' :: y' :: l').length

Tactic:
apply Nat.add_mod

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
x y x' y' : α
l l' : List α
hd : (x :: y :: l).Nodup
hd' : (x' :: y' :: l').Nodup
h : ∀ (x_1 : α), (x :: y :: l).formPerm x_1 = (x' :: y' :: l').formPerm x_1
⊢ x :: y :: l ~r x' :: y' :: l'

Tactic:
have hx : x' ∈ x :: y :: l := by
  have : x' ∈ { z | formPerm (x :: y :: l) z ≠ z } := by
    rw [Set.mem_setOf_eq, h x', formPerm_apply_head _ _ _ hd']
    simp only [mem_cons, nodup_cons] at hd'
    push_neg at hd'
    exact hd'.left.left.symm
  simpa using support_formPerm_le' _ this

Result:
α : Type u_1
inst✝ : DecidableEq α
x y x' y' : α
l l' : List α
hd : (x :: y :: l).Nodup
hd' : (x' :: y' :: l').Nodup
h : ∀ (x_1 : α), (x :: y :: l).formPerm x_1 = (x' :: y' :: l').formPerm x_1
hx : x' ∈ x :: y :: l
⊢ x :: y :: l ~r x' :: y' :: l'