Theorem: Permutation.get_transposAdj_self (Fifteen/Data/Permutation/Basic.lean)

State before:
n i : Nat
h : i + 1 < n
h' : i < n
⊢ (transposAdj i h)[i] = { val := i + 1, isLt := h }
Tactic:
simp only [transposAdj, get_transpos, i.succ_ne_self, if_neg, if_pos]
State after:
no goals