-- Mathlib/GroupTheory/Perm/Fin.lean
theorem succAbove_cycleRange {n : ℕ} (i j : Fin n) :
    i.succ.succAbove (i.cycleRange j) = swap 0 i.succ j.succ

Proof state:
case succ.inr.inr.a
n✝ : ℕ
i j : Fin (n✝ + 1)
hgt : i < j
⊢ j.succ ≠ i.succ

Tactic:
apply (Fin.succ_injective _).ne hgt.ne.symm

Result:
no goals

Proof state:
case succ.inr.inr.h
n✝ : ℕ
i j : Fin (n✝ + 1)
hgt : i < j
⊢ i.succ ≤ j.castSucc

Tactic:
simpa [Fin.le_iff_val_le_val] using hgt

Result:
no goals

Proof state:
case succ
n✝ : ℕ
i j : Fin (n✝ + 1)
⊢ i.succ.succAbove (i.cycleRange j) = (swap 0 i.succ) j.succ

Tactic:
rcases lt_trichotomy j i with (hlt | heq | hgt)

Result:
case succ.inl
n✝ : ℕ
i j : Fin (n✝ + 1)
hlt : j < i
⊢ i.succ.succAbove (i.cycleRange j) = (swap 0 i.succ) j.succ

case succ.inr.inl
n✝ : ℕ
i j : Fin (n✝ + 1)
heq : j = i
⊢ i.succ.succAbove (i.cycleRange j) = (swap 0 i.succ) j.succ

case succ.inr.inr
n✝ : ℕ
i j : Fin (n✝ + 1)
hgt : i < j
⊢ i.succ.succAbove (i.cycleRange j) = (swap 0 i.succ) j.succ

Proof state:
case succ.inr.inr.a
n✝ : ℕ
i j : Fin (n✝ + 1)
hgt : i < j
⊢ j.succ ≠ 0

Tactic:
apply Fin.succ_ne_zero

Result:
no goals

Proof state:
case succ.inl
n✝ : ℕ
i j : Fin (n✝ + 1)
hlt : j < i
this : (j + 1).castSucc = j.succ
⊢ i.succ.succAbove (i.cycleRange j) = (swap 0 i.succ) j.succ

Tactic:
rw [Fin.cycleRange_of_lt hlt, Fin.succAbove_of_castSucc_lt, this, swap_apply_of_ne_of_ne]

Result:
case succ.inl.a
n✝ : ℕ
i j : Fin (n✝ + 1)
hlt : j < i
this : (j + 1).castSucc = j.succ
⊢ j.succ ≠ 0

case succ.inl.a
n✝ : ℕ
i j : Fin (n✝ + 1)
hlt : j < i
this : (j + 1).castSucc = j.succ
⊢ j.succ ≠ i.succ

case succ.inl.h
n✝ : ℕ
i j : Fin (n✝ + 1)
hlt : j < i
this : (j + 1).castSucc = j.succ
⊢ (j + 1).castSucc < i.succ

Proof state:
case succ.inr.inl
n✝ : ℕ
i j : Fin (n✝ + 1)
heq : j = i
⊢ i.succ.succAbove (i.cycleRange j) = (swap 0 i.succ) j.succ

Tactic:
rw [heq, Fin.cycleRange_self, Fin.succAbove_of_castSucc_lt, swap_apply_right, Fin.castSucc_zero]

Result:
case succ.inr.inl.h
n✝ : ℕ
i j : Fin (n✝ + 1)
heq : j = i
⊢ castSucc 0 < i.succ

Proof state:
case succ.inl.a
n✝ : ℕ
i j : Fin (n✝ + 1)
hlt : j < i
this : (j + 1).castSucc = j.succ
⊢ j.succ ≠ 0

Tactic:
apply Fin.succ_ne_zero

Result:
no goals

Proof state:
case succ.inl.h
n✝ : ℕ
i j : Fin (n✝ + 1)
hlt : j < i
this : (j + 1).castSucc = j.succ
⊢ ↑(j + 1).castSucc < ↑i.succ

Tactic:
simpa [this] using hlt

Result:
no goals

Proof state:
case succ.inl.h
n✝ : ℕ
i j : Fin (n✝ + 1)
hlt : j < i
this : (j + 1).castSucc = j.succ
⊢ (j + 1).castSucc < i.succ

Tactic:
rw [Fin.lt_iff_val_lt_val]

Result:
case succ.inl.h
n✝ : ℕ
i j : Fin (n✝ + 1)
hlt : j < i
this : (j + 1).castSucc = j.succ
⊢ ↑(j + 1).castSucc < ↑i.succ

Proof state:
case succ.inr.inr
n✝ : ℕ
i j : Fin (n✝ + 1)
hgt : i < j
⊢ i.succ.succAbove (i.cycleRange j) = (swap 0 i.succ) j.succ

Tactic:
rw [Fin.cycleRange_of_gt hgt, Fin.succAbove_of_le_castSucc, swap_apply_of_ne_of_ne]

Result:
case succ.inr.inr.a
n✝ : ℕ
i j : Fin (n✝ + 1)
hgt : i < j
⊢ j.succ ≠ 0

case succ.inr.inr.a
n✝ : ℕ
i j : Fin (n✝ + 1)
hgt : i < j
⊢ j.succ ≠ i.succ

case succ.inr.inr.h
n✝ : ℕ
i j : Fin (n✝ + 1)
hgt : i < j
⊢ i.succ ≤ j.castSucc

Proof state:
case zero
i j : Fin 0
⊢ i.succ.succAbove (i.cycleRange j) = (swap 0 i.succ) j.succ

Tactic:
rcases j with ⟨_, ⟨⟩⟩

Result:
no goals

Proof state:
n✝ : ℕ
i j : Fin (n✝ + 1)
hlt : j < i
⊢ (j + 1).castSucc = j.succ

Tactic:
ext

Result:
case h
n✝ : ℕ
i j : Fin (n✝ + 1)
hlt : j < i
⊢ ↑(j + 1).castSucc = ↑j.succ

Proof state:
case succ.inr.inl.h
n✝ : ℕ
i j : Fin (n✝ + 1)
heq : j = i
⊢ 0 < i.succ

Tactic:
apply Fin.succ_pos

Result:
no goals

Proof state:
case succ.inl
n✝ : ℕ
i j : Fin (n✝ + 1)
hlt : j < i
⊢ i.succ.succAbove (i.cycleRange j) = (swap 0 i.succ) j.succ

Tactic:
have : castSucc (j + 1) = j.succ := by
  ext
  rw [coe_castSucc, val_succ, Fin.val_add_one_of_lt (lt_of_lt_of_le hlt i.le_last)]

Result:
case succ.inl
n✝ : ℕ
i j : Fin (n✝ + 1)
hlt : j < i
this : (j + 1).castSucc = j.succ
⊢ i.succ.succAbove (i.cycleRange j) = (swap 0 i.succ) j.succ

Proof state:
n : ℕ
i j : Fin n
⊢ i.succ.succAbove (i.cycleRange j) = (swap 0 i.succ) j.succ

Tactic:
cases n

Result:
case zero
i j : Fin 0
⊢ i.succ.succAbove (i.cycleRange j) = (swap 0 i.succ) j.succ

case succ
n✝ : ℕ
i j : Fin (n✝ + 1)
⊢ i.succ.succAbove (i.cycleRange j) = (swap 0 i.succ) j.succ

Proof state:
case h
n✝ : ℕ
i j : Fin (n✝ + 1)
hlt : j < i
⊢ ↑(j + 1).castSucc = ↑j.succ

Tactic:
rw [coe_castSucc, val_succ, Fin.val_add_one_of_lt (lt_of_lt_of_le hlt i.le_last)]

Result:
no goals

Proof state:
case succ.inl.a
n✝ : ℕ
i j : Fin (n✝ + 1)
hlt : j < i
this : (j + 1).castSucc = j.succ
⊢ j.succ ≠ i.succ

Tactic:
exact (Fin.succ_injective _).ne hlt.ne

Result:
no goals

Proof state:
case succ.inr.inl.h
n✝ : ℕ
i j : Fin (n✝ + 1)
heq : j = i
⊢ castSucc 0 < i.succ

Tactic:
rw [Fin.castSucc_zero]

Result:
case succ.inr.inl.h
n✝ : ℕ
i j : Fin (n✝ + 1)
heq : j = i
⊢ 0 < i.succ