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

State before:
n i : Nat
h : i + 1 < n
j : Nat
hj : j < i
hj' : j < n
⊢ (transposAdj i h)[j] = { val := j, isLt := hj' }
Tactic:
simp only [transposAdj, get_transpos]
State after:
n i : Nat
h : i + 1 < n
j : Nat
hj : j < i
hj' : j < n
⊢ (if i + 1 = j then { val := i, isLt := (_ : i < n) }
    else
      if i = j then { val := i + 1, isLt := h }
      else
        { val := j,
          isLt :=
            (_ : (fun x i => i < n) (transpos { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h }) j) }) =
    { val := j, isLt := hj' }

State before:
n i : Nat
h : i + 1 < n
j : Nat
hj : j < i
hj' : j < n
⊢ (if i + 1 = j then { val := i, isLt := (_ : i < n) }
    else
      if i = j then { val := i + 1, isLt := h }
      else
        { val := j,
          isLt :=
            (_ : (fun x i => i < n) (transpos { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h }) j) }) =
    { val := j, isLt := hj' }
Tactic:
simp only [Nat.ne_of_gt <| .step hj, Nat.ne_of_gt hj, if_neg]
State after:
no goals