α : Type u_1
β : Type ?u.792756
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : formPerm (x :: y :: l) = formPerm (x' :: y' :: l')
⊢ (x :: y :: l) ~r (x' :: y' :: l')
α : Type u_1
β : Type ?u.792756
inst✝ : DecidableEq α
l✝ : List α
x✝ 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')
refine' ⟨fun h => _, fun hr => formPerm_eq_of_isRotated hd hr⟩
α : Type u_1
β : Type ?u.792756
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
⊢ (x :: y :: l) ~r (x' :: y' :: l')
α : Type u_1
β : Type ?u.792756
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : formPerm (x :: y :: l) = formPerm (x' :: y' :: l')
⊢ (x :: y :: l) ~r (x' :: y' :: l')
rw [Equiv.Perm.ext_iff] at h
α : Type u_1
β : Type ?u.792756
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
hx : x' ∈ x :: y :: l
⊢ (x :: y :: l) ~r (x' :: y' :: l')
α : Type u_1
β : Type ?u.792756
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
⊢ (x :: y :: l) ~r (x' :: y' :: l')
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
case intro.intro
α : Type u_1
β : Type ?u.792756
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < length (x :: y :: l)
hx' : nthLe (x :: y :: l) n hn = x'
⊢ (x :: y :: l) ~r (x' :: y' :: l')
α : Type u_1
β : Type ?u.792756
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
hx : x' ∈ x :: y :: l
⊢ (x :: y :: l) ~r (x' :: y' :: l')
obtain ⟨n, hn, hx'⟩ := nthLe_of_mem hx
case intro.intro
α : Type u_1
β : Type ?u.792756
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < length (x :: y :: l)
hx' : nthLe (x :: y :: l) n hn = x'
hl : length (x :: y :: l) = length (x' :: y' :: l')
⊢ (x :: y :: l) ~r (x' :: y' :: l')
case intro.intro
α : Type u_1
β : Type ?u.792756
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < length (x :: y :: l)
hx' : nthLe (x :: y :: l) n hn = x'
⊢ (x :: y :: l) ~r (x' :: y' :: l')
have hl : (x :: y :: l).length = (x' :: y' :: l').length := by
  rw [← dedup_eq_self.mpr hd, ← dedup_eq_self.mpr hd', ← card_toFinset, ← card_toFinset]
  refine' congr_arg Finset.card _
  rw [← Finset.coe_inj, ← support_formPerm_of_nodup' _ hd (by simp), ←
    support_formPerm_of_nodup' _ hd' (by simp)]
  simp only [h]
case intro.intro
α : Type u_1
β : Type ?u.792756
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < length (x :: y :: l)
hx' : nthLe (x :: y :: l) n hn = x'
hl : length (x :: y :: l) = length (x' :: y' :: l')
⊢ rotate (x :: y :: l) n = x' :: y' :: l'
case intro.intro
α : Type u_1
β : Type ?u.792756
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < length (x :: y :: l)
hx' : nthLe (x :: y :: l) n hn = x'
hl : length (x :: y :: l) = length (x' :: y' :: l')
⊢ (x :: y :: l) ~r (x' :: y' :: l')
use n
case intro.intro.hl
α : Type u_1
β : Type ?u.792756
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < length (x :: y :: l)
hx' : nthLe (x :: y :: l) n hn = x'
hl : length (x :: y :: l) = length (x' :: y' :: l')
⊢ length (rotate (x :: y :: l) n) = length (x' :: y' :: l')

case intro.intro.h
α : Type u_1
β : Type ?u.792756
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < length (x :: y :: l)
hx' : nthLe (x :: y :: l) n hn = x'
hl : length (x :: y :: l) = length (x' :: y' :: l')
⊢ ∀ (n_1 : ℕ) (h₁ : n_1 < length (rotate (x :: y :: l) n)) (h₂ : n_1 < length (x' :: y' :: l')),
    nthLe (rotate (x :: y :: l) n) n_1 h₁ = nthLe (x' :: y' :: l') n_1 h₂
case intro.intro
α : Type u_1
β : Type ?u.792756
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < length (x :: y :: l)
hx' : nthLe (x :: y :: l) n hn = x'
hl : length (x :: y :: l) = length (x' :: y' :: l')
⊢ rotate (x :: y :: l) n = x' :: y' :: l'
apply List.ext_nthLe
α : Type u_1
β : Type ?u.792756
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
this : x' ∈ {z | ↑(formPerm (x :: y :: l)) z ≠ z}
⊢ x' ∈ x :: y :: l
α : Type u_1
β : Type ?u.792756
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
⊢ x' ∈ x :: y :: l
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
no goals
α : Type u_1
β : Type ?u.792756
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
this : x' ∈ {z | ↑(formPerm (x :: y :: l)) z ≠ z}
⊢ x' ∈ x :: y :: l
simpa using support_formPerm_le' _ this
α : Type u_1
β : Type ?u.792756
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
⊢ y' ≠ x'
α : Type u_1
β : Type ?u.792756
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
⊢ x' ∈ {z | ↑(formPerm (x :: y :: l)) z ≠ z}
rw [Set.mem_setOf_eq, h x', formPerm_apply_head _ _ _ hd']
α : Type u_1
β : Type ?u.792756
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
hd' : ¬(x' = y' ∨ x' ∈ l') ∧ ¬y' ∈ l' ∧ Nodup l'
⊢ y' ≠ x'
α : Type u_1
β : Type ?u.792756
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
⊢ y' ≠ x'
simp only [mem_cons, nodup_cons] at hd'
α : Type u_1
β : Type ?u.792756
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
hd' : (x' ≠ y' ∧ ¬x' ∈ l') ∧ ¬y' ∈ l' ∧ Nodup l'
⊢ y' ≠ x'
α : Type u_1
β : Type ?u.792756
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
hd' : ¬(x' = y' ∨ x' ∈ l') ∧ ¬y' ∈ l' ∧ Nodup l'
⊢ y' ≠ x'
push_neg  at hd'
no goals
α : Type u_1
β : Type ?u.792756
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
hd' : (x' ≠ y' ∧ ¬x' ∈ l') ∧ ¬y' ∈ l' ∧ Nodup l'
⊢ y' ≠ x'
exact hd'.left.left.symm
α : Type u_1
β : Type ?u.792756
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < length (x :: y :: l)
hx' : nthLe (x :: y :: l) n hn = x'
⊢ Finset.card (toFinset (x :: y :: l)) = Finset.card (toFinset (x' :: y' :: l'))
α : Type u_1
β : Type ?u.792756
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < length (x :: y :: l)
hx' : nthLe (x :: y :: l) n hn = x'
⊢ length (x :: y :: l) = length (x' :: y' :: l')
rw [← dedup_eq_self.mpr hd, ← dedup_eq_self.mpr hd', ← card_toFinset, ← card_toFinset]
α : Type u_1
β : Type ?u.792756
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < length (x :: y :: l)
hx' : nthLe (x :: y :: l) n hn = x'
⊢ toFinset (x :: y :: l) = toFinset (x' :: y' :: l')
α : Type u_1
β : Type ?u.792756
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < length (x :: y :: l)
hx' : nthLe (x :: y :: l) n hn = x'
⊢ Finset.card (toFinset (x :: y :: l)) = Finset.card (toFinset (x' :: y' :: l'))
refine' congr_arg Finset.card _
α : Type u_1
β : Type ?u.792756
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < length (x :: y :: l)
hx' : nthLe (x :: y :: l) n hn = x'
⊢ {x_1 | ↑(formPerm (x :: y :: l)) x_1 ≠ x_1} = {x | ↑(formPerm (x' :: y' :: l')) x ≠ x}
α : Type u_1
β : Type ?u.792756
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < length (x :: y :: l)
hx' : nthLe (x :: y :: l) n hn = x'
⊢ toFinset (x :: y :: l) = toFinset (x' :: y' :: l')
rw [← Finset.coe_inj, ← support_formPerm_of_nodup' _ hd (by simp), ←
  support_formPerm_of_nodup' _ hd' (by simp)]
no goals
α : Type u_1
β : Type ?u.792756
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < length (x :: y :: l)
hx' : nthLe (x :: y :: l) n hn = x'
⊢ {x_1 | ↑(formPerm (x :: y :: l)) x_1 ≠ x_1} = {x | ↑(formPerm (x' :: y' :: l')) x ≠ x}
simp only [h]
no goals
α : Type u_1
β : Type ?u.792756
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < length (x :: y :: l)
hx' : nthLe (x :: y :: l) n hn = x'
⊢ ∀ (x_1 : α), x :: y :: l ≠ [x_1]
simp
no goals
α : Type u_1
β : Type ?u.792756
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < length (x :: y :: l)
hx' : nthLe (x :: y :: l) n hn = x'
⊢ ∀ (x : α), x' :: y' :: l' ≠ [x]
simp
no goals
case intro.intro.hl
α : Type u_1
β : Type ?u.792756
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < length (x :: y :: l)
hx' : nthLe (x :: y :: l) n hn = x'
hl : length (x :: y :: l) = length (x' :: y' :: l')
⊢ length (rotate (x :: y :: l) n) = length (x' :: y' :: l')
rw [length_rotate, hl]
case intro.intro.h
α : Type u_1
β : Type ?u.792756
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < length (x :: y :: l)
hx' : nthLe (x :: y :: l) n hn = x'
hl : length (x :: y :: l) = length (x' :: y' :: l')
k : ℕ
hk : k < length (rotate (x :: y :: l) n)
hk' : k < length (x' :: y' :: l')
⊢ nthLe (rotate (x :: y :: l) n) k hk = nthLe (x' :: y' :: l') k hk'
case intro.intro.h
α : Type u_1
β : Type ?u.792756
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < length (x :: y :: l)
hx' : nthLe (x :: y :: l) n hn = x'
hl : length (x :: y :: l) = length (x' :: y' :: l')
⊢ ∀ (n_1 : ℕ) (h₁ : n_1 < length (rotate (x :: y :: l) n)) (h₂ : n_1 < length (x' :: y' :: l')),
    nthLe (rotate (x :: y :: l) n) n_1 h₁ = nthLe (x' :: y' :: l') n_1 h₂
intro k hk hk'
case intro.intro.h
α : Type u_1
β : Type ?u.792756
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < length (x :: y :: l)
hx' : nthLe (x :: y :: l) n hn = x'
hl : length (x :: y :: l) = length (x' :: y' :: l')
k : ℕ
hk : k < length (rotate (x :: y :: l) n)
hk' : k < length (x' :: y' :: l')
⊢ nthLe (x :: y :: l) ((k + n) % length (x :: y :: l)) (_ : (k + n) % length (x :: y :: l) < length (x :: y :: l)) =
    nthLe (x' :: y' :: l') k hk'
case intro.intro.h
α : Type u_1
β : Type ?u.792756
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < length (x :: y :: l)
hx' : nthLe (x :: y :: l) n hn = x'
hl : length (x :: y :: l) = length (x' :: y' :: l')
k : ℕ
hk : k < length (rotate (x :: y :: l) n)
hk' : k < length (x' :: y' :: l')
⊢ nthLe (rotate (x :: y :: l) n) k hk = nthLe (x' :: y' :: l') k hk'
rw [nthLe_rotate]
case intro.intro.h.zero
α : Type u_1
β : Type ?u.792756
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < length (x :: y :: l)
hx' : nthLe (x :: y :: l) n hn = x'
hl : length (x :: y :: l) = length (x' :: y' :: l')
k : ℕ
hk✝ : k < length (rotate (x :: y :: l) n)
hk'✝ : k < length (x' :: y' :: l')
hk : Nat.zero < length (rotate (x :: y :: l) n)
hk' : Nat.zero < length (x' :: y' :: l')
⊢ nthLe (x :: y :: l) ((Nat.zero + n) % length (x :: y :: l))
      (_ : (Nat.zero + n) % length (x :: y :: l) < length (x :: y :: l)) =
    nthLe (x' :: y' :: l') Nat.zero hk'

case intro.intro.h.succ
α : Type u_1
β : Type ?u.792756
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < length (x :: y :: l)
hx' : nthLe (x :: y :: l) n hn = x'
hl : length (x :: y :: l) = length (x' :: y' :: l')
k✝ : ℕ
hk✝ : k✝ < length (rotate (x :: y :: l) n)
hk'✝ : k✝ < length (x' :: y' :: l')
k : ℕ
IH :
  ∀ (hk : k < length (rotate (x :: y :: l) n)) (hk' : k < length (x' :: y' :: l')),
    nthLe (x :: y :: l) ((k + n) % length (x :: y :: l)) (_ : (k + n) % length (x :: y :: l) < length (x :: y :: l)) =
      nthLe (x' :: y' :: l') k hk'
hk : Nat.succ k < length (rotate (x :: y :: l) n)
hk' : Nat.succ k < length (x' :: y' :: l')
⊢ nthLe (x :: y :: l) ((Nat.succ k + n) % length (x :: y :: l))
      (_ : (Nat.succ k + n) % length (x :: y :: l) < length (x :: y :: l)) =
    nthLe (x' :: y' :: l') (Nat.succ k) hk'
case intro.intro.h
α : Type u_1
β : Type ?u.792756
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < length (x :: y :: l)
hx' : nthLe (x :: y :: l) n hn = x'
hl : length (x :: y :: l) = length (x' :: y' :: l')
k : ℕ
hk : k < length (rotate (x :: y :: l) n)
hk' : k < length (x' :: y' :: l')
⊢ nthLe (x :: y :: l) ((k + n) % length (x :: y :: l)) (_ : (k + n) % length (x :: y :: l) < length (x :: y :: l)) =
    nthLe (x' :: y' :: l') k hk'
induction' k with k IH
case intro.intro.h.zero
α : Type u_1
β : Type ?u.792756
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < length (x :: y :: l)
hx' : nthLe (x :: y :: l) n hn = x'
hl : length (x :: y :: l) = length (x' :: y' :: l')
k : ℕ
hk✝ : k < length (rotate (x :: y :: l) n)
hk'✝ : k < length (x' :: y' :: l')
hk : Nat.zero < length (rotate (x :: y :: l) n)
hk' : Nat.zero < length (x' :: y' :: l')
⊢ nthLe (x :: y :: l) ((Nat.zero + n) % length (x :: y :: l))
      (_ : (Nat.zero + n) % length (x :: y :: l) < length (x :: y :: l)) =
    nthLe (x :: y :: l) n hn
case intro.intro.h.zero
α : Type u_1
β : Type ?u.792756
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < length (x :: y :: l)
hx' : nthLe (x :: y :: l) n hn = x'
hl : length (x :: y :: l) = length (x' :: y' :: l')
k : ℕ
hk✝ : k < length (rotate (x :: y :: l) n)
hk'✝ : k < length (x' :: y' :: l')
hk : Nat.zero < length (rotate (x :: y :: l) n)
hk' : Nat.zero < length (x' :: y' :: l')
⊢ nthLe (x :: y :: l) ((Nat.zero + n) % length (x :: y :: l))
      (_ : (Nat.zero + n) % length (x :: y :: l) < length (x :: y :: l)) =
    nthLe (x' :: y' :: l') Nat.zero hk'
refine' Eq.trans _ hx'
case intro.intro.h.zero.e_n
α : Type u_1
β : Type ?u.792756
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < length (x :: y :: l)
hx' : nthLe (x :: y :: l) n hn = x'
hl : length (x :: y :: l) = length (x' :: y' :: l')
k : ℕ
hk✝ : k < length (rotate (x :: y :: l) n)
hk'✝ : k < length (x' :: y' :: l')
hk : Nat.zero < length (rotate (x :: y :: l) n)
hk' : Nat.zero < length (x' :: y' :: l')
⊢ (Nat.zero + n) % length (x :: y :: l) = n
case intro.intro.h.zero
α : Type u_1
β : Type ?u.792756
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < length (x :: y :: l)
hx' : nthLe (x :: y :: l) n hn = x'
hl : length (x :: y :: l) = length (x' :: y' :: l')
k : ℕ
hk✝ : k < length (rotate (x :: y :: l) n)
hk'✝ : k < length (x' :: y' :: l')
hk : Nat.zero < length (rotate (x :: y :: l) n)
hk' : Nat.zero < length (x' :: y' :: l')
⊢ nthLe (x :: y :: l) ((Nat.zero + n) % length (x :: y :: l))
      (_ : (Nat.zero + n) % length (x :: y :: l) < length (x :: y :: l)) =
    nthLe (x :: y :: l) n hn
congr
no goals
case intro.intro.h.zero.e_n
α : Type u_1
β : Type ?u.792756
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < length (x :: y :: l)
hx' : nthLe (x :: y :: l) n hn = x'
hl : length (x :: y :: l) = length (x' :: y' :: l')
k : ℕ
hk✝ : k < length (rotate (x :: y :: l) n)
hk'✝ : k < length (x' :: y' :: l')
hk : Nat.zero < length (rotate (x :: y :: l) n)
hk' : Nat.zero < length (x' :: y' :: l')
⊢ (Nat.zero + n) % length (x :: y :: l) = n
simpa using hn
case intro.intro.h.succ
α : Type u_1
β : Type ?u.792756
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < length (x :: y :: l)
hx' : nthLe (x :: y :: l) n hn = x'
hl : length (x :: y :: l) = length (x' :: y' :: l')
k✝ : ℕ
hk✝ : k✝ < length (rotate (x :: y :: l) n)
hk'✝ : k✝ < length (x' :: y' :: l')
k : ℕ
IH :
  ∀ (hk : k < length (rotate (x :: y :: l) n)) (hk' : k < length (x' :: y' :: l')),
    nthLe (x :: y :: l) ((k + n) % length (x :: y :: l)) (_ : (k + n) % length (x :: y :: l) < length (x :: y :: l)) =
      nthLe (x' :: y' :: l') k hk'
hk : Nat.succ k < length (rotate (x :: y :: l) n)
hk' : Nat.succ k < length (x' :: y' :: l')
this : Nat.succ k = (k + 1) % length (x' :: y' :: l')
⊢ nthLe (x :: y :: l) ((Nat.succ k + n) % length (x :: y :: l))
      (_ : (Nat.succ k + n) % length (x :: y :: l) < length (x :: y :: l)) =
    nthLe (x' :: y' :: l') (Nat.succ k) hk'
case intro.intro.h.succ
α : Type u_1
β : Type ?u.792756
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < length (x :: y :: l)
hx' : nthLe (x :: y :: l) n hn = x'
hl : length (x :: y :: l) = length (x' :: y' :: l')
k✝ : ℕ
hk✝ : k✝ < length (rotate (x :: y :: l) n)
hk'✝ : k✝ < length (x' :: y' :: l')
k : ℕ
IH :
  ∀ (hk : k < length (rotate (x :: y :: l) n)) (hk' : k < length (x' :: y' :: l')),
    nthLe (x :: y :: l) ((k + n) % length (x :: y :: l)) (_ : (k + n) % length (x :: y :: l) < length (x :: y :: l)) =
      nthLe (x' :: y' :: l') k hk'
hk : Nat.succ k < length (rotate (x :: y :: l) n)
hk' : Nat.succ k < length (x' :: y' :: l')
⊢ nthLe (x :: y :: l) ((Nat.succ k + n) % length (x :: y :: l))
      (_ : (Nat.succ k + n) % length (x :: y :: l) < length (x :: y :: l)) =
    nthLe (x' :: y' :: l') (Nat.succ k) hk'
have : k.succ = (k + 1) % (x' :: y' :: l').length := by
  rw [← Nat.succ_eq_add_one, Nat.mod_eq_of_lt hk']
case intro.intro.h.succ
α : Type u_1
β : Type ?u.792756
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < length (x :: y :: l)
hx' : nthLe (x :: y :: l) n hn = x'
hl : length (x :: y :: l) = length (x' :: y' :: l')
k✝ : ℕ
hk✝ : k✝ < length (rotate (x :: y :: l) n)
hk'✝ : k✝ < length (x' :: y' :: l')
k : ℕ
IH :
  ∀ (hk : k < length (rotate (x :: y :: l) n)) (hk' : k < length (x' :: y' :: l')),
    nthLe (x :: y :: l) ((k + n) % length (x :: y :: l)) (_ : (k + n) % length (x :: y :: l) < length (x :: y :: l)) =
      nthLe (x' :: y' :: l') k hk'
hk : Nat.succ k < length (rotate (x :: y :: l) n)
hk' : Nat.succ k < length (x' :: y' :: l')
this : Nat.succ k = (k + 1) % length (x' :: y' :: l')
⊢ nthLe (x :: y :: l) (((k + 1) % length (x' :: y' :: l') + n) % length (x :: y :: l))
      (_ : ((k + 1) % length (x' :: y' :: l') + n) % length (x :: y :: l) < length (x :: y :: l)) =
    nthLe (x' :: y' :: l') ((k + 1) % length (x' :: y' :: l'))
      (_ : (k + 1) % length (x' :: y' :: l') < length (x' :: y' :: l'))
case intro.intro.h.succ
α : Type u_1
β : Type ?u.792756
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < length (x :: y :: l)
hx' : nthLe (x :: y :: l) n hn = x'
hl : length (x :: y :: l) = length (x' :: y' :: l')
k✝ : ℕ
hk✝ : k✝ < length (rotate (x :: y :: l) n)
hk'✝ : k✝ < length (x' :: y' :: l')
k : ℕ
IH :
  ∀ (hk : k < length (rotate (x :: y :: l) n)) (hk' : k < length (x' :: y' :: l')),
    nthLe (x :: y :: l) ((k + n) % length (x :: y :: l)) (_ : (k + n) % length (x :: y :: l) < length (x :: y :: l)) =
      nthLe (x' :: y' :: l') k hk'
hk : Nat.succ k < length (rotate (x :: y :: l) n)
hk' : Nat.succ k < length (x' :: y' :: l')
this : Nat.succ k = (k + 1) % length (x' :: y' :: l')
⊢ nthLe (x :: y :: l) ((Nat.succ k + n) % length (x :: y :: l))
      (_ : (Nat.succ k + n) % length (x :: y :: l) < length (x :: y :: l)) =
    nthLe (x' :: y' :: l') (Nat.succ k) hk'
simp_rw [this]
case intro.intro.h.succ
α : Type u_1
β : Type ?u.792756
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < length (x :: y :: l)
hx' : nthLe (x :: y :: l) n hn = x'
hl : length (x :: y :: l) = length (x' :: y' :: l')
k✝ : ℕ
hk✝ : k✝ < length (rotate (x :: y :: l) n)
hk'✝ : k✝ < length (x' :: y' :: l')
k : ℕ
IH :
  ∀ (hk : k < length (rotate (x :: y :: l) n)) (hk' : k < length (x' :: y' :: l')),
    nthLe (x :: y :: l) ((k + n) % length (x :: y :: l)) (_ : (k + n) % length (x :: y :: l) < length (x :: y :: l)) =
      nthLe (x' :: y' :: l') k hk'
hk : Nat.succ k < length (rotate (x :: y :: l) n)
hk' : Nat.succ k < length (x' :: y' :: l')
this : Nat.succ k = (k + 1) % length (x' :: y' :: l')
⊢ nthLe (x :: y :: l) (((k + 1) % length (x' :: y' :: l') + n) % length (x :: y :: l))
      (_ : ((k + 1) % length (x' :: y' :: l') + n) % length (x :: y :: l) < length (x :: y :: l)) =
    nthLe (x :: y :: l) (((k + n) % length (x :: y :: l) + 1) % length (x :: y :: l))
      (_ : ((k + n) % length (x :: y :: l) + 1) % length (x :: y :: l) < length (x :: y :: l))
case intro.intro.h.succ
α : Type u_1
β : Type ?u.792756
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < length (x :: y :: l)
hx' : nthLe (x :: y :: l) n hn = x'
hl : length (x :: y :: l) = length (x' :: y' :: l')
k✝ : ℕ
hk✝ : k✝ < length (rotate (x :: y :: l) n)
hk'✝ : k✝ < length (x' :: y' :: l')
k : ℕ
IH :
  ∀ (hk : k < length (rotate (x :: y :: l) n)) (hk' : k < length (x' :: y' :: l')),
    nthLe (x :: y :: l) ((k + n) % length (x :: y :: l)) (_ : (k + n) % length (x :: y :: l) < length (x :: y :: l)) =
      nthLe (x' :: y' :: l') k hk'
hk : Nat.succ k < length (rotate (x :: y :: l) n)
hk' : Nat.succ k < length (x' :: y' :: l')
this : Nat.succ k = (k + 1) % length (x' :: y' :: l')
⊢ nthLe (x :: y :: l) (((k + 1) % length (x' :: y' :: l') + n) % length (x :: y :: l))
      (_ : ((k + 1) % length (x' :: y' :: l') + n) % length (x :: y :: l) < length (x :: y :: l)) =
    nthLe (x' :: y' :: l') ((k + 1) % length (x' :: y' :: l'))
      (_ : (k + 1) % length (x' :: y' :: l') < length (x' :: y' :: l'))
rw [← formPerm_apply_nthLe _ hd' k (k.lt_succ_self.trans hk'), ←
  IH (k.lt_succ_self.trans hk), ← h, formPerm_apply_nthLe _ hd]
case intro.intro.h.succ.e_n
α : Type u_1
β : Type ?u.792756
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < length (x :: y :: l)
hx' : nthLe (x :: y :: l) n hn = x'
hl : length (x :: y :: l) = length (x' :: y' :: l')
k✝ : ℕ
hk✝ : k✝ < length (rotate (x :: y :: l) n)
hk'✝ : k✝ < length (x' :: y' :: l')
k : ℕ
IH :
  ∀ (hk : k < length (rotate (x :: y :: l) n)) (hk' : k < length (x' :: y' :: l')),
    nthLe (x :: y :: l) ((k + n) % length (x :: y :: l)) (_ : (k + n) % length (x :: y :: l) < length (x :: y :: l)) =
      nthLe (x' :: y' :: l') k hk'
hk : Nat.succ k < length (rotate (x :: y :: l) n)
hk' : Nat.succ k < length (x' :: y' :: l')
this : Nat.succ k = (k + 1) % length (x' :: y' :: l')
⊢ ((k + 1) % length (x' :: y' :: l') + n) % length (x :: y :: l) =
    ((k + n) % length (x :: y :: l) + 1) % length (x :: y :: l)
case intro.intro.h.succ
α : Type u_1
β : Type ?u.792756
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < length (x :: y :: l)
hx' : nthLe (x :: y :: l) n hn = x'
hl : length (x :: y :: l) = length (x' :: y' :: l')
k✝ : ℕ
hk✝ : k✝ < length (rotate (x :: y :: l) n)
hk'✝ : k✝ < length (x' :: y' :: l')
k : ℕ
IH :
  ∀ (hk : k < length (rotate (x :: y :: l) n)) (hk' : k < length (x' :: y' :: l')),
    nthLe (x :: y :: l) ((k + n) % length (x :: y :: l)) (_ : (k + n) % length (x :: y :: l) < length (x :: y :: l)) =
      nthLe (x' :: y' :: l') k hk'
hk : Nat.succ k < length (rotate (x :: y :: l) n)
hk' : Nat.succ k < length (x' :: y' :: l')
this : Nat.succ k = (k + 1) % length (x' :: y' :: l')
⊢ nthLe (x :: y :: l) (((k + 1) % length (x' :: y' :: l') + n) % length (x :: y :: l))
      (_ : ((k + 1) % length (x' :: y' :: l') + n) % length (x :: y :: l) < length (x :: y :: l)) =
    nthLe (x :: y :: l) (((k + n) % length (x :: y :: l) + 1) % length (x :: y :: l))
      (_ : ((k + n) % length (x :: y :: l) + 1) % length (x :: y :: l) < length (x :: y :: l))
congr 1
case intro.intro.h.succ.e_n
α : Type u_1
β : Type ?u.792756
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < length (x :: y :: l)
hx' : nthLe (x :: y :: l) n hn = x'
hl : length (x :: y :: l) = length (x' :: y' :: l')
k✝ : ℕ
hk✝ : k✝ < length (rotate (x :: y :: l) n)
hk'✝ : k✝ < length (x' :: y' :: l')
k : ℕ
IH :
  ∀ (hk : k < length (rotate (x :: y :: l) n)) (hk' : k < length (x' :: y' :: l')),
    nthLe (x :: y :: l) ((k + n) % length (x :: y :: l)) (_ : (k + n) % length (x :: y :: l) < length (x :: y :: l)) =
      nthLe (x' :: y' :: l') k hk'
hk : Nat.succ k < length (rotate (x :: y :: l) n)
hk' : Nat.succ k < length (x' :: y' :: l')
this : Nat.succ k = (k + 1) % length (x' :: y' :: l')
h1 : 1 = 1 % length (x' :: y' :: l')
⊢ ((k + 1) % length (x' :: y' :: l') + n) % length (x :: y :: l) =
    ((k + n) % length (x :: y :: l) + 1) % length (x :: y :: l)
case intro.intro.h.succ.e_n
α : Type u_1
β : Type ?u.792756
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < length (x :: y :: l)
hx' : nthLe (x :: y :: l) n hn = x'
hl : length (x :: y :: l) = length (x' :: y' :: l')
k✝ : ℕ
hk✝ : k✝ < length (rotate (x :: y :: l) n)
hk'✝ : k✝ < length (x' :: y' :: l')
k : ℕ
IH :
  ∀ (hk : k < length (rotate (x :: y :: l) n)) (hk' : k < length (x' :: y' :: l')),
    nthLe (x :: y :: l) ((k + n) % length (x :: y :: l)) (_ : (k + n) % length (x :: y :: l) < length (x :: y :: l)) =
      nthLe (x' :: y' :: l') k hk'
hk : Nat.succ k < length (rotate (x :: y :: l) n)
hk' : Nat.succ k < length (x' :: y' :: l')
this : Nat.succ k = (k + 1) % length (x' :: y' :: l')
⊢ ((k + 1) % length (x' :: y' :: l') + n) % length (x :: y :: l) =
    ((k + n) % length (x :: y :: l) + 1) % length (x :: y :: l)
have h1 : 1 = 1 % (x' :: y' :: l').length := by simp
no goals
case intro.intro.h.succ.e_n
α : Type u_1
β : Type ?u.792756
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < length (x :: y :: l)
hx' : nthLe (x :: y :: l) n hn = x'
hl : length (x :: y :: l) = length (x' :: y' :: l')
k✝ : ℕ
hk✝ : k✝ < length (rotate (x :: y :: l) n)
hk'✝ : k✝ < length (x' :: y' :: l')
k : ℕ
IH :
  ∀ (hk : k < length (rotate (x :: y :: l) n)) (hk' : k < length (x' :: y' :: l')),
    nthLe (x :: y :: l) ((k + n) % length (x :: y :: l)) (_ : (k + n) % length (x :: y :: l) < length (x :: y :: l)) =
      nthLe (x' :: y' :: l') k hk'
hk : Nat.succ k < length (rotate (x :: y :: l) n)
hk' : Nat.succ k < length (x' :: y' :: l')
this : Nat.succ k = (k + 1) % length (x' :: y' :: l')
h1 : 1 = 1 % length (x' :: y' :: l')
⊢ ((k + 1) % length (x' :: y' :: l') + n) % length (x :: y :: l) =
    ((k + n) % length (x :: y :: l) + 1) % length (x :: y :: l)
rw [hl, Nat.mod_eq_of_lt hk', h1, ← Nat.add_mod, Nat.succ_add, Nat.succ_eq_add_one]
no goals
α : Type u_1
β : Type ?u.792756
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < length (x :: y :: l)
hx' : nthLe (x :: y :: l) n hn = x'
hl : length (x :: y :: l) = length (x' :: y' :: l')
k✝ : ℕ
hk✝ : k✝ < length (rotate (x :: y :: l) n)
hk'✝ : k✝ < length (x' :: y' :: l')
k : ℕ
IH :
  ∀ (hk : k < length (rotate (x :: y :: l) n)) (hk' : k < length (x' :: y' :: l')),
    nthLe (x :: y :: l) ((k + n) % length (x :: y :: l)) (_ : (k + n) % length (x :: y :: l) < length (x :: y :: l)) =
      nthLe (x' :: y' :: l') k hk'
hk : Nat.succ k < length (rotate (x :: y :: l) n)
hk' : Nat.succ k < length (x' :: y' :: l')
⊢ Nat.succ k = (k + 1) % length (x' :: y' :: l')
rw [← Nat.succ_eq_add_one, Nat.mod_eq_of_lt hk']
no goals
α : Type u_1
β : Type ?u.792756
inst✝ : DecidableEq α
l✝ : List α
x✝ x y x' y' : α
l l' : List α
hd : Nodup (x :: y :: l)
hd' : Nodup (x' :: y' :: l')
h : ∀ (x_1 : α), ↑(formPerm (x :: y :: l)) x_1 = ↑(formPerm (x' :: y' :: l')) x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < length (x :: y :: l)
hx' : nthLe (x :: y :: l) n hn = x'
hl : length (x :: y :: l) = length (x' :: y' :: l')
k✝ : ℕ
hk✝ : k✝ < length (rotate (x :: y :: l) n)
hk'✝ : k✝ < length (x' :: y' :: l')
k : ℕ
IH :
  ∀ (hk : k < length (rotate (x :: y :: l) n)) (hk' : k < length (x' :: y' :: l')),
    nthLe (x :: y :: l) ((k + n) % length (x :: y :: l)) (_ : (k + n) % length (x :: y :: l) < length (x :: y :: l)) =
      nthLe (x' :: y' :: l') k hk'
hk : Nat.succ k < length (rotate (x :: y :: l) n)
hk' : Nat.succ k < length (x' :: y' :: l')
this : Nat.succ k = (k + 1) % length (x' :: y' :: l')
⊢ 1 = 1 % length (x' :: y' :: l')
simp