Theorem: Permutation.mem_inversions (Fifteen/Data/Permutation/Inversion.lean)

State before:
n : Nat
x : Permutation n
iv : Inversion x
⊢ iv ∈ inversions x
Tactic:
let ⟨i,j,hlt,hinv⟩ := iv
State after:
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt : i < j
hinv : x[↑i] > x[↑j]
⊢ { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ inversions x

State before:
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt : i < j
hinv : x[↑i] > x[↑j]
⊢ { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ inversions x
Tactic:
dsimp [inversions]
State after:
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt : i < j
hinv : x[↑i] > x[↑j]
⊢ { fst := i, snd := j, lt := hlt, inverted := hinv } ∈
    Nat.fold' n
      (fun j =>
        Nat.fold' ↑j fun i ivs =>
          if h : x[↑i] > x[↑j] then
            Array.push ivs { fst := Fin.castLE (_ : ↑j ≤ n) i, snd := j, lt := (_ : ↑i < ↑j), inverted := h }
          else ivs)
      #[]

State before:
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt : i < j
hinv : x[↑i] > x[↑j]
⊢ { fst := i, snd := j, lt := hlt, inverted := hinv } ∈
    Nat.fold' n
      (fun j =>
        Nat.fold' ↑j fun i ivs =>
          if h : x[↑i] > x[↑j] then
            Array.push ivs { fst := Fin.castLE (_ : ↑j ≤ n) i, snd := j, lt := (_ : ↑i < ↑j), inverted := h }
          else ivs)
      #[]
Tactic:
refine Nat.fold'_induction (motive := fun k (ivs : Array (Inversion x)) => j.1 < k → ⟨i,j,hlt,hinv⟩ ∈ ivs) n _ #[] ?zero ?succ j.2
State after:
case zero
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt : i < j
hinv : x[↑i] > x[↑j]
⊢ (fun k ivs => ↑j < k → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ ivs) 0 #[]

case succ
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt : i < j
hinv : x[↑i] > x[↑j]
⊢ ∀ (i_1 : Nat) (hi : i_1 < n) (a : Array (Inversion x)),
    (fun k ivs => ↑j < k → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ ivs) i_1 a →
      (fun k ivs => ↑j < k → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ ivs) (i_1 + 1)
        (Nat.fold' (↑{ val := i_1, isLt := hi })
          (fun i ivs =>
            if h : x[↑i] > x[↑{ val := i_1, isLt := hi }] then
              Array.push ivs
                { fst := Fin.castLE (_ : ↑{ val := i_1, isLt := hi } ≤ n) i, snd := { val := i_1, isLt := hi },
                  lt := (_ : ↑i < ↑{ val := i_1, isLt := hi }), inverted := h }
            else ivs)
          a)

State before:
case zero
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt : i < j
hinv : x[↑i] > x[↑j]
⊢ (fun k ivs => ↑j < k → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ ivs) 0 #[]

case succ
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt : i < j
hinv : x[↑i] > x[↑j]
⊢ ∀ (i_1 : Nat) (hi : i_1 < n) (a : Array (Inversion x)),
    (fun k ivs => ↑j < k → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ ivs) i_1 a →
      (fun k ivs => ↑j < k → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ ivs) (i_1 + 1)
        (Nat.fold' (↑{ val := i_1, isLt := hi })
          (fun i ivs =>
            if h : x[↑i] > x[↑{ val := i_1, isLt := hi }] then
              Array.push ivs
                { fst := Fin.castLE (_ : ↑{ val := i_1, isLt := hi } ≤ n) i, snd := { val := i_1, isLt := hi },
                  lt := (_ : ↑i < ↑{ val := i_1, isLt := hi }), inverted := h }
            else ivs)
          a)
Tactic:
all_goals simp
State after:
case zero
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt : i < j
hinv : x[↑i] > x[↑j]
⊢ ↑j < 0 → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ #[]

case succ
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt : i < j
hinv : x[↑i] > x[↑j]
⊢ ∀ (i_1 : Nat) (hi : i_1 < n) (a : Array (Inversion x)),
    (↑j < i_1 → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ a) →
      ↑j < i_1 + 1 →
        { fst := i, snd := j, lt := hlt, inverted := hinv } ∈
          Nat.fold' i_1
            (fun i ivs =>
              if h : x[↑i] > x[i_1] then
                Array.push ivs
                  { fst := Fin.castLE (_ : ↑{ val := i_1, isLt := hi } ≤ n) i, snd := { val := i_1, isLt := hi },
                    lt := (_ : ↑i < ↑{ val := i_1, isLt := hi }), inverted := h }
              else ivs)
            a

State before:
case zero
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt : i < j
hinv : x[↑i] > x[↑j]
⊢ ↑j < 0 → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ #[]

case succ
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt : i < j
hinv : x[↑i] > x[↑j]
⊢ ∀ (i_1 : Nat) (hi : i_1 < n) (a : Array (Inversion x)),
    (↑j < i_1 → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ a) →
      ↑j < i_1 + 1 →
        { fst := i, snd := j, lt := hlt, inverted := hinv } ∈
          Nat.fold' i_1
            (fun i ivs =>
              if h : x[↑i] > x[i_1] then
                Array.push ivs
                  { fst := Fin.castLE (_ : ↑{ val := i_1, isLt := hi } ≤ n) i, snd := { val := i_1, isLt := hi },
                    lt := (_ : ↑i < ↑{ val := i_1, isLt := hi }), inverted := h }
              else ivs)
            a
Tactic:
. intro hj; cases hj
State after:
case succ
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt : i < j
hinv : x[↑i] > x[↑j]
⊢ ∀ (i_1 : Nat) (hi : i_1 < n) (a : Array (Inversion x)),
    (↑j < i_1 → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ a) →
      ↑j < i_1 + 1 →
        { fst := i, snd := j, lt := hlt, inverted := hinv } ∈
          Nat.fold' i_1
            (fun i ivs =>
              if h : x[↑i] > x[i_1] then
                Array.push ivs
                  { fst := Fin.castLE (_ : ↑{ val := i_1, isLt := hi } ≤ n) i, snd := { val := i_1, isLt := hi },
                    lt := (_ : ↑i < ↑{ val := i_1, isLt := hi }), inverted := h }
              else ivs)
            a

State before:
case succ
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt : i < j
hinv : x[↑i] > x[↑j]
⊢ ∀ (i_1 : Nat) (hi : i_1 < n) (a : Array (Inversion x)),
    (↑j < i_1 → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ a) →
      ↑j < i_1 + 1 →
        { fst := i, snd := j, lt := hlt, inverted := hinv } ∈
          Nat.fold' i_1
            (fun i ivs =>
              if h : x[↑i] > x[i_1] then
                Array.push ivs
                  { fst := Fin.castLE (_ : ↑{ val := i_1, isLt := hi } ≤ n) i, snd := { val := i_1, isLt := hi },
                    lt := (_ : ↑i < ↑{ val := i_1, isLt := hi }), inverted := h }
              else ivs)
            a
Tactic:
. intro k hk invs IH hjk
  have : i.1 < k := trans (r:=LT.lt (α:=Nat)) hlt (Nat.le_of_succ_le_succ hjk)
  refine Nat.fold'_induction (motive := fun l (ivs' : Array (Inversion x)) => (i.1 < l ∨ j.1 < k) → ⟨i,j,hlt,hinv⟩ ∈ ivs') k _ invs ?_ ?_ (Or.inl this)
  all_goals simp
  . intro hi
    cases hi with
    | inl hi => cases hi
    | inr hj => exact IH hj
  . intro l hl invs' IH' hil
    cases Nat.eq_or_lt_of_le (Nat.le_of_succ_le_succ hjk) with
    | inl heq =>
      cases heq
      have : i.1 ≤ l :=
        Nat.le_of_succ_le_succ (Or.resolve_right hil j.1.lt_irrefl)
      cases Nat.eq_or_lt_of_le this with
      | inl heq =>
        cases heq; rewrite [dif_pos hinv]
        exact Array.mem_push.mpr <| Or.inr rfl
      | inr hlt =>
        specialize IH' (Or.inl hlt)
        if hx : x[l]'(Nat.lt_trans hl j.2) > x[j.1] then
          rewrite [dif_pos hx]
          exact Array.mem_push.mpr <| Or.inl IH'
        else
          rewrite [dif_neg hx]; exact IH'
    | inr hlt =>
      specialize IH' (Or.inr hlt)
      if hx : x[l]'(Nat.lt_trans hl hk) > x[k]'hk then
        rewrite [dif_pos hx]
        exact Array.mem_push.mpr <| Or.inl IH'
      else
        rewrite [dif_neg hx]; exact IH'
State after:
no goals

State before:
case succ
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt : i < j
hinv : x[↑i] > x[↑j]
⊢ ∀ (i_1 : Nat) (hi : i_1 < n) (a : Array (Inversion x)),
    (fun k ivs => ↑j < k → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ ivs) i_1 a →
      (fun k ivs => ↑j < k → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ ivs) (i_1 + 1)
        (Nat.fold' (↑{ val := i_1, isLt := hi })
          (fun i ivs =>
            if h : x[↑i] > x[↑{ val := i_1, isLt := hi }] then
              Array.push ivs
                { fst := Fin.castLE (_ : ↑{ val := i_1, isLt := hi } ≤ n) i, snd := { val := i_1, isLt := hi },
                  lt := (_ : ↑i < ↑{ val := i_1, isLt := hi }), inverted := h }
            else ivs)
          a)
Tactic:
simp
State after:
case succ
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt : i < j
hinv : x[↑i] > x[↑j]
⊢ ∀ (i_1 : Nat) (hi : i_1 < n) (a : Array (Inversion x)),
    (↑j < i_1 → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ a) →
      ↑j < i_1 + 1 →
        { fst := i, snd := j, lt := hlt, inverted := hinv } ∈
          Nat.fold' i_1
            (fun i ivs =>
              if h : x[↑i] > x[i_1] then
                Array.push ivs
                  { fst := Fin.castLE (_ : ↑{ val := i_1, isLt := hi } ≤ n) i, snd := { val := i_1, isLt := hi },
                    lt := (_ : ↑i < ↑{ val := i_1, isLt := hi }), inverted := h }
              else ivs)
            a

State before:
case zero
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt : i < j
hinv : x[↑i] > x[↑j]
⊢ ↑j < 0 → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ #[]
Tactic:
intro hj
State after:
case zero
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt : i < j
hinv : x[↑i] > x[↑j]
hj : ↑j < 0
⊢ { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ #[]

State before:
case zero
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt : i < j
hinv : x[↑i] > x[↑j]
hj : ↑j < 0
⊢ { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ #[]
Tactic:
cases hj
State after:
no goals

State before:
case succ
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt : i < j
hinv : x[↑i] > x[↑j]
⊢ ∀ (i_1 : Nat) (hi : i_1 < n) (a : Array (Inversion x)),
    (↑j < i_1 → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ a) →
      ↑j < i_1 + 1 →
        { fst := i, snd := j, lt := hlt, inverted := hinv } ∈
          Nat.fold' i_1
            (fun i ivs =>
              if h : x[↑i] > x[i_1] then
                Array.push ivs
                  { fst := Fin.castLE (_ : ↑{ val := i_1, isLt := hi } ≤ n) i, snd := { val := i_1, isLt := hi },
                    lt := (_ : ↑i < ↑{ val := i_1, isLt := hi }), inverted := h }
              else ivs)
            a
Tactic:
intro k hk invs IH hjk
State after:
case succ
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt : i < j
hinv : x[↑i] > x[↑j]
k : Nat
hk : k < n
invs : Array (Inversion x)
IH : ↑j < k → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ invs
hjk : ↑j < k + 1
⊢ { fst := i, snd := j, lt := hlt, inverted := hinv } ∈
    Nat.fold' k
      (fun i ivs =>
        if h : x[↑i] > x[k] then
          Array.push ivs
            { fst := Fin.castLE (_ : ↑{ val := k, isLt := hk } ≤ n) i, snd := { val := k, isLt := hk },
              lt := (_ : ↑i < ↑{ val := k, isLt := hk }), inverted := h }
        else ivs)
      invs

State before:
case succ
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt : i < j
hinv : x[↑i] > x[↑j]
k : Nat
hk : k < n
invs : Array (Inversion x)
IH : ↑j < k → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ invs
hjk : ↑j < k + 1
⊢ { fst := i, snd := j, lt := hlt, inverted := hinv } ∈
    Nat.fold' k
      (fun i ivs =>
        if h : x[↑i] > x[k] then
          Array.push ivs
            { fst := Fin.castLE (_ : ↑{ val := k, isLt := hk } ≤ n) i, snd := { val := k, isLt := hk },
              lt := (_ : ↑i < ↑{ val := k, isLt := hk }), inverted := h }
        else ivs)
      invs
Tactic:
have : i.1 < k := trans (r:=LT.lt (α:=Nat)) hlt (Nat.le_of_succ_le_succ hjk)
State after:
case succ
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt : i < j
hinv : x[↑i] > x[↑j]
k : Nat
hk : k < n
invs : Array (Inversion x)
IH : ↑j < k → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ invs
hjk : ↑j < k + 1
this : ↑i < k
⊢ { fst := i, snd := j, lt := hlt, inverted := hinv } ∈
    Nat.fold' k
      (fun i ivs =>
        if h : x[↑i] > x[k] then
          Array.push ivs
            { fst := Fin.castLE (_ : ↑{ val := k, isLt := hk } ≤ n) i, snd := { val := k, isLt := hk },
              lt := (_ : ↑i < ↑{ val := k, isLt := hk }), inverted := h }
        else ivs)
      invs

State before:
case succ
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt : i < j
hinv : x[↑i] > x[↑j]
k : Nat
hk : k < n
invs : Array (Inversion x)
IH : ↑j < k → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ invs
hjk : ↑j < k + 1
this : ↑i < k
⊢ { fst := i, snd := j, lt := hlt, inverted := hinv } ∈
    Nat.fold' k
      (fun i ivs =>
        if h : x[↑i] > x[k] then
          Array.push ivs
            { fst := Fin.castLE (_ : ↑{ val := k, isLt := hk } ≤ n) i, snd := { val := k, isLt := hk },
              lt := (_ : ↑i < ↑{ val := k, isLt := hk }), inverted := h }
        else ivs)
      invs
Tactic:
refine Nat.fold'_induction (motive := fun l (ivs' : Array (Inversion x)) => (i.1 < l ∨ j.1 < k) → ⟨i,j,hlt,hinv⟩ ∈ ivs') k _ invs ?_ ?_ (Or.inl this)
State after:
case succ.refine_1
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt : i < j
hinv : x[↑i] > x[↑j]
k : Nat
hk : k < n
invs : Array (Inversion x)
IH : ↑j < k → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ invs
hjk : ↑j < k + 1
this : ↑i < k
⊢ (fun l ivs' => ↑i < l ∨ ↑j < k → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ ivs') 0 invs

case succ.refine_2
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt : i < j
hinv : x[↑i] > x[↑j]
k : Nat
hk : k < n
invs : Array (Inversion x)
IH : ↑j < k → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ invs
hjk : ↑j < k + 1
this : ↑i < k
⊢ ∀ (i_1 : Nat) (hi : i_1 < k) (a : Array (Inversion x)),
    (fun l ivs' => ↑i < l ∨ ↑j < k → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ ivs') i_1 a →
      (fun l ivs' => ↑i < l ∨ ↑j < k → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ ivs') (i_1 + 1)
        (if h : x[↑{ val := i_1, isLt := hi }] > x[k] then
          Array.push a
            { fst := Fin.castLE (_ : ↑{ val := k, isLt := hk } ≤ n) { val := i_1, isLt := hi },
              snd := { val := k, isLt := hk }, lt := (_ : ↑{ val := i_1, isLt := hi } < ↑{ val := k, isLt := hk }),
              inverted := h }
        else a)

State before:
case succ.refine_1
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt : i < j
hinv : x[↑i] > x[↑j]
k : Nat
hk : k < n
invs : Array (Inversion x)
IH : ↑j < k → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ invs
hjk : ↑j < k + 1
this : ↑i < k
⊢ (fun l ivs' => ↑i < l ∨ ↑j < k → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ ivs') 0 invs

case succ.refine_2
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt : i < j
hinv : x[↑i] > x[↑j]
k : Nat
hk : k < n
invs : Array (Inversion x)
IH : ↑j < k → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ invs
hjk : ↑j < k + 1
this : ↑i < k
⊢ ∀ (i_1 : Nat) (hi : i_1 < k) (a : Array (Inversion x)),
    (fun l ivs' => ↑i < l ∨ ↑j < k → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ ivs') i_1 a →
      (fun l ivs' => ↑i < l ∨ ↑j < k → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ ivs') (i_1 + 1)
        (if h : x[↑{ val := i_1, isLt := hi }] > x[k] then
          Array.push a
            { fst := Fin.castLE (_ : ↑{ val := k, isLt := hk } ≤ n) { val := i_1, isLt := hi },
              snd := { val := k, isLt := hk }, lt := (_ : ↑{ val := i_1, isLt := hi } < ↑{ val := k, isLt := hk }),
              inverted := h }
        else a)
Tactic:
all_goals simp
State after:
case succ.refine_1
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt : i < j
hinv : x[↑i] > x[↑j]
k : Nat
hk : k < n
invs : Array (Inversion x)
IH : ↑j < k → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ invs
hjk : ↑j < k + 1
this : ↑i < k
⊢ ↑i < 0 ∨ ↑j < k → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ invs

case succ.refine_2
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt : i < j
hinv : x[↑i] > x[↑j]
k : Nat
hk : k < n
invs : Array (Inversion x)
IH : ↑j < k → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ invs
hjk : ↑j < k + 1
this : ↑i < k
⊢ ∀ (i_1 : Nat) (hi : i_1 < k) (a : Array (Inversion x)),
    (↑i < i_1 ∨ ↑j < k → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ a) →
      ↑i < i_1 + 1 ∨ ↑j < k →
        { fst := i, snd := j, lt := hlt, inverted := hinv } ∈
          if h : x[i_1] > x[k] then
            Array.push a
              { fst := { val := i_1, isLt := (_ : i_1 < n) }, snd := { val := k, isLt := hk },
                lt := (_ : { val := i_1, isLt := (_ : i_1 < n) } < { val := k, isLt := hk }),
                inverted := (_ : x[↑{ val := i_1, isLt := (_ : i_1 < n) }] > x[↑{ val := k, isLt := hk }]) }
          else a

State before:
case succ.refine_1
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt : i < j
hinv : x[↑i] > x[↑j]
k : Nat
hk : k < n
invs : Array (Inversion x)
IH : ↑j < k → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ invs
hjk : ↑j < k + 1
this : ↑i < k
⊢ ↑i < 0 ∨ ↑j < k → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ invs

case succ.refine_2
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt : i < j
hinv : x[↑i] > x[↑j]
k : Nat
hk : k < n
invs : Array (Inversion x)
IH : ↑j < k → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ invs
hjk : ↑j < k + 1
this : ↑i < k
⊢ ∀ (i_1 : Nat) (hi : i_1 < k) (a : Array (Inversion x)),
    (↑i < i_1 ∨ ↑j < k → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ a) →
      ↑i < i_1 + 1 ∨ ↑j < k →
        { fst := i, snd := j, lt := hlt, inverted := hinv } ∈
          if h : x[i_1] > x[k] then
            Array.push a
              { fst := { val := i_1, isLt := (_ : i_1 < n) }, snd := { val := k, isLt := hk },
                lt := (_ : { val := i_1, isLt := (_ : i_1 < n) } < { val := k, isLt := hk }),
                inverted := (_ : x[↑{ val := i_1, isLt := (_ : i_1 < n) }] > x[↑{ val := k, isLt := hk }]) }
          else a
Tactic:
. intro hi
  cases hi with
  | inl hi => cases hi
  | inr hj => exact IH hj
State after:
case succ.refine_2
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt : i < j
hinv : x[↑i] > x[↑j]
k : Nat
hk : k < n
invs : Array (Inversion x)
IH : ↑j < k → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ invs
hjk : ↑j < k + 1
this : ↑i < k
⊢ ∀ (i_1 : Nat) (hi : i_1 < k) (a : Array (Inversion x)),
    (↑i < i_1 ∨ ↑j < k → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ a) →
      ↑i < i_1 + 1 ∨ ↑j < k →
        { fst := i, snd := j, lt := hlt, inverted := hinv } ∈
          if h : x[i_1] > x[k] then
            Array.push a
              { fst := { val := i_1, isLt := (_ : i_1 < n) }, snd := { val := k, isLt := hk },
                lt := (_ : { val := i_1, isLt := (_ : i_1 < n) } < { val := k, isLt := hk }),
                inverted := (_ : x[↑{ val := i_1, isLt := (_ : i_1 < n) }] > x[↑{ val := k, isLt := hk }]) }
          else a

State before:
case succ.refine_2
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt : i < j
hinv : x[↑i] > x[↑j]
k : Nat
hk : k < n
invs : Array (Inversion x)
IH : ↑j < k → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ invs
hjk : ↑j < k + 1
this : ↑i < k
⊢ ∀ (i_1 : Nat) (hi : i_1 < k) (a : Array (Inversion x)),
    (↑i < i_1 ∨ ↑j < k → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ a) →
      ↑i < i_1 + 1 ∨ ↑j < k →
        { fst := i, snd := j, lt := hlt, inverted := hinv } ∈
          if h : x[i_1] > x[k] then
            Array.push a
              { fst := { val := i_1, isLt := (_ : i_1 < n) }, snd := { val := k, isLt := hk },
                lt := (_ : { val := i_1, isLt := (_ : i_1 < n) } < { val := k, isLt := hk }),
                inverted := (_ : x[↑{ val := i_1, isLt := (_ : i_1 < n) }] > x[↑{ val := k, isLt := hk }]) }
          else a
Tactic:
. intro l hl invs' IH' hil
  cases Nat.eq_or_lt_of_le (Nat.le_of_succ_le_succ hjk) with
  | inl heq =>
    cases heq
    have : i.1 ≤ l :=
      Nat.le_of_succ_le_succ (Or.resolve_right hil j.1.lt_irrefl)
    cases Nat.eq_or_lt_of_le this with
    | inl heq =>
      cases heq; rewrite [dif_pos hinv]
      exact Array.mem_push.mpr <| Or.inr rfl
    | inr hlt =>
      specialize IH' (Or.inl hlt)
      if hx : x[l]'(Nat.lt_trans hl j.2) > x[j.1] then
        rewrite [dif_pos hx]
        exact Array.mem_push.mpr <| Or.inl IH'
      else
        rewrite [dif_neg hx]; exact IH'
  | inr hlt =>
    specialize IH' (Or.inr hlt)
    if hx : x[l]'(Nat.lt_trans hl hk) > x[k]'hk then
      rewrite [dif_pos hx]
      exact Array.mem_push.mpr <| Or.inl IH'
    else
      rewrite [dif_neg hx]; exact IH'
State after:
no goals

State before:
case succ.refine_2
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt : i < j
hinv : x[↑i] > x[↑j]
k : Nat
hk : k < n
invs : Array (Inversion x)
IH : ↑j < k → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ invs
hjk : ↑j < k + 1
this : ↑i < k
⊢ ∀ (i_1 : Nat) (hi : i_1 < k) (a : Array (Inversion x)),
    (fun l ivs' => ↑i < l ∨ ↑j < k → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ ivs') i_1 a →
      (fun l ivs' => ↑i < l ∨ ↑j < k → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ ivs') (i_1 + 1)
        (if h : x[↑{ val := i_1, isLt := hi }] > x[k] then
          Array.push a
            { fst := Fin.castLE (_ : ↑{ val := k, isLt := hk } ≤ n) { val := i_1, isLt := hi },
              snd := { val := k, isLt := hk }, lt := (_ : ↑{ val := i_1, isLt := hi } < ↑{ val := k, isLt := hk }),
              inverted := h }
        else a)
Tactic:
simp
State after:
case succ.refine_2
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt : i < j
hinv : x[↑i] > x[↑j]
k : Nat
hk : k < n
invs : Array (Inversion x)
IH : ↑j < k → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ invs
hjk : ↑j < k + 1
this : ↑i < k
⊢ ∀ (i_1 : Nat) (hi : i_1 < k) (a : Array (Inversion x)),
    (↑i < i_1 ∨ ↑j < k → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ a) →
      ↑i < i_1 + 1 ∨ ↑j < k →
        { fst := i, snd := j, lt := hlt, inverted := hinv } ∈
          if h : x[i_1] > x[k] then
            Array.push a
              { fst := { val := i_1, isLt := (_ : i_1 < n) }, snd := { val := k, isLt := hk },
                lt := (_ : { val := i_1, isLt := (_ : i_1 < n) } < { val := k, isLt := hk }),
                inverted := (_ : x[↑{ val := i_1, isLt := (_ : i_1 < n) }] > x[↑{ val := k, isLt := hk }]) }
          else a

State before:
case succ.refine_1
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt : i < j
hinv : x[↑i] > x[↑j]
k : Nat
hk : k < n
invs : Array (Inversion x)
IH : ↑j < k → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ invs
hjk : ↑j < k + 1
this : ↑i < k
⊢ ↑i < 0 ∨ ↑j < k → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ invs
Tactic:
intro hi
State after:
case succ.refine_1
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt : i < j
hinv : x[↑i] > x[↑j]
k : Nat
hk : k < n
invs : Array (Inversion x)
IH : ↑j < k → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ invs
hjk : ↑j < k + 1
this : ↑i < k
hi : ↑i < 0 ∨ ↑j < k
⊢ { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ invs

State before:
case succ.refine_1
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt : i < j
hinv : x[↑i] > x[↑j]
k : Nat
hk : k < n
invs : Array (Inversion x)
IH : ↑j < k → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ invs
hjk : ↑j < k + 1
this : ↑i < k
hi : ↑i < 0 ∨ ↑j < k
⊢ { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ invs
Tactic:
cases hi with
| inl hi => cases hi
| inr hj => exact IH hj
State after:
no goals

State before:
case succ.refine_1.inl
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt : i < j
hinv : x[↑i] > x[↑j]
k : Nat
hk : k < n
invs : Array (Inversion x)
IH : ↑j < k → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ invs
hjk : ↑j < k + 1
this : ↑i < k
hi : ↑i < 0
⊢ { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ invs
Tactic:
cases hi
State after:
no goals

State before:
case succ.refine_1.inr
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt : i < j
hinv : x[↑i] > x[↑j]
k : Nat
hk : k < n
invs : Array (Inversion x)
IH : ↑j < k → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ invs
hjk : ↑j < k + 1
this : ↑i < k
hj : ↑j < k
⊢ { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ invs
Tactic:
exact IH hj
State after:
no goals

State before:
case succ.refine_2
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt : i < j
hinv : x[↑i] > x[↑j]
k : Nat
hk : k < n
invs : Array (Inversion x)
IH : ↑j < k → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ invs
hjk : ↑j < k + 1
this : ↑i < k
⊢ ∀ (i_1 : Nat) (hi : i_1 < k) (a : Array (Inversion x)),
    (↑i < i_1 ∨ ↑j < k → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ a) →
      ↑i < i_1 + 1 ∨ ↑j < k →
        { fst := i, snd := j, lt := hlt, inverted := hinv } ∈
          if h : x[i_1] > x[k] then
            Array.push a
              { fst := { val := i_1, isLt := (_ : i_1 < n) }, snd := { val := k, isLt := hk },
                lt := (_ : { val := i_1, isLt := (_ : i_1 < n) } < { val := k, isLt := hk }),
                inverted := (_ : x[↑{ val := i_1, isLt := (_ : i_1 < n) }] > x[↑{ val := k, isLt := hk }]) }
          else a
Tactic:
intro l hl invs' IH' hil
State after:
case succ.refine_2
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt : i < j
hinv : x[↑i] > x[↑j]
k : Nat
hk : k < n
invs : Array (Inversion x)
IH : ↑j < k → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ invs
hjk : ↑j < k + 1
this : ↑i < k
l : Nat
hl : l < k
invs' : Array (Inversion x)
IH' : ↑i < l ∨ ↑j < k → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ invs'
hil : ↑i < l + 1 ∨ ↑j < k
⊢ { fst := i, snd := j, lt := hlt, inverted := hinv } ∈
    if h : x[l] > x[k] then
      Array.push invs'
        { fst := { val := l, isLt := (_ : l < n) }, snd := { val := k, isLt := hk },
          lt := (_ : { val := l, isLt := (_ : l < n) } < { val := k, isLt := hk }),
          inverted := (_ : x[↑{ val := l, isLt := (_ : l < n) }] > x[↑{ val := k, isLt := hk }]) }
    else invs'

State before:
case succ.refine_2
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt : i < j
hinv : x[↑i] > x[↑j]
k : Nat
hk : k < n
invs : Array (Inversion x)
IH : ↑j < k → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ invs
hjk : ↑j < k + 1
this : ↑i < k
l : Nat
hl : l < k
invs' : Array (Inversion x)
IH' : ↑i < l ∨ ↑j < k → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ invs'
hil : ↑i < l + 1 ∨ ↑j < k
⊢ { fst := i, snd := j, lt := hlt, inverted := hinv } ∈
    if h : x[l] > x[k] then
      Array.push invs'
        { fst := { val := l, isLt := (_ : l < n) }, snd := { val := k, isLt := hk },
          lt := (_ : { val := l, isLt := (_ : l < n) } < { val := k, isLt := hk }),
          inverted := (_ : x[↑{ val := l, isLt := (_ : l < n) }] > x[↑{ val := k, isLt := hk }]) }
    else invs'
Tactic:
cases Nat.eq_or_lt_of_le (Nat.le_of_succ_le_succ hjk) with
| inl heq =>
  cases heq
  have : i.1 ≤ l :=
    Nat.le_of_succ_le_succ (Or.resolve_right hil j.1.lt_irrefl)
  cases Nat.eq_or_lt_of_le this with
  | inl heq =>
    cases heq; rewrite [dif_pos hinv]
    exact Array.mem_push.mpr <| Or.inr rfl
  | inr hlt =>
    specialize IH' (Or.inl hlt)
    if hx : x[l]'(Nat.lt_trans hl j.2) > x[j.1] then
      rewrite [dif_pos hx]
      exact Array.mem_push.mpr <| Or.inl IH'
    else
      rewrite [dif_neg hx]; exact IH'
| inr hlt =>
  specialize IH' (Or.inr hlt)
  if hx : x[l]'(Nat.lt_trans hl hk) > x[k]'hk then
    rewrite [dif_pos hx]
    exact Array.mem_push.mpr <| Or.inl IH'
  else
    rewrite [dif_neg hx]; exact IH'
State after:
no goals

State before:
case succ.refine_2.inl
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt : i < j
hinv : x[↑i] > x[↑j]
k : Nat
hk : k < n
invs : Array (Inversion x)
IH : ↑j < k → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ invs
hjk : ↑j < k + 1
this : ↑i < k
l : Nat
hl : l < k
invs' : Array (Inversion x)
IH' : ↑i < l ∨ ↑j < k → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ invs'
hil : ↑i < l + 1 ∨ ↑j < k
heq : ↑j = k
⊢ { fst := i, snd := j, lt := hlt, inverted := hinv } ∈
    if h : x[l] > x[k] then
      Array.push invs'
        { fst := { val := l, isLt := (_ : l < n) }, snd := { val := k, isLt := hk },
          lt := (_ : { val := l, isLt := (_ : l < n) } < { val := k, isLt := hk }),
          inverted := (_ : x[↑{ val := l, isLt := (_ : l < n) }] > x[↑{ val := k, isLt := hk }]) }
    else invs'
Tactic:
cases heq
State after:
case succ.refine_2.inl.refl
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt : i < j
hinv : x[↑i] > x[↑j]
invs : Array (Inversion x)
l : Nat
invs' : Array (Inversion x)
hk : ↑j < n
IH : ↑j < ↑j → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ invs
hjk : ↑j < ↑j + 1
this : ↑i < ↑j
hl : l < ↑j
IH' : ↑i < l ∨ ↑j < ↑j → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ invs'
hil : ↑i < l + 1 ∨ ↑j < ↑j
⊢ { fst := i, snd := j, lt := hlt, inverted := hinv } ∈
    if h : x[l] > x[↑j] then
      Array.push invs'
        { fst := { val := l, isLt := (_ : l < n) }, snd := { val := ↑j, isLt := hk },
          lt := (_ : { val := l, isLt := (_ : l < n) } < { val := ↑j, isLt := hk }),
          inverted := (_ : x[↑{ val := l, isLt := (_ : l < n) }] > x[↑{ val := ↑j, isLt := hk }]) }
    else invs'

State before:
case succ.refine_2.inl.refl
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt : i < j
hinv : x[↑i] > x[↑j]
invs : Array (Inversion x)
l : Nat
invs' : Array (Inversion x)
hk : ↑j < n
IH : ↑j < ↑j → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ invs
hjk : ↑j < ↑j + 1
this : ↑i < ↑j
hl : l < ↑j
IH' : ↑i < l ∨ ↑j < ↑j → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ invs'
hil : ↑i < l + 1 ∨ ↑j < ↑j
⊢ { fst := i, snd := j, lt := hlt, inverted := hinv } ∈
    if h : x[l] > x[↑j] then
      Array.push invs'
        { fst := { val := l, isLt := (_ : l < n) }, snd := { val := ↑j, isLt := hk },
          lt := (_ : { val := l, isLt := (_ : l < n) } < { val := ↑j, isLt := hk }),
          inverted := (_ : x[↑{ val := l, isLt := (_ : l < n) }] > x[↑{ val := ↑j, isLt := hk }]) }
    else invs'
Tactic:
have : i.1 ≤ l :=
  Nat.le_of_succ_le_succ (Or.resolve_right hil j.1.lt_irrefl)
State after:
case succ.refine_2.inl.refl
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt : i < j
hinv : x[↑i] > x[↑j]
invs : Array (Inversion x)
l : Nat
invs' : Array (Inversion x)
hk : ↑j < n
IH : ↑j < ↑j → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ invs
hjk : ↑j < ↑j + 1
this✝ : ↑i < ↑j
hl : l < ↑j
IH' : ↑i < l ∨ ↑j < ↑j → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ invs'
hil : ↑i < l + 1 ∨ ↑j < ↑j
this : ↑i ≤ l
⊢ { fst := i, snd := j, lt := hlt, inverted := hinv } ∈
    if h : x[l] > x[↑j] then
      Array.push invs'
        { fst := { val := l, isLt := (_ : l < n) }, snd := { val := ↑j, isLt := hk },
          lt := (_ : { val := l, isLt := (_ : l < n) } < { val := ↑j, isLt := hk }),
          inverted := (_ : x[↑{ val := l, isLt := (_ : l < n) }] > x[↑{ val := ↑j, isLt := hk }]) }
    else invs'

State before:
case succ.refine_2.inl.refl
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt : i < j
hinv : x[↑i] > x[↑j]
invs : Array (Inversion x)
l : Nat
invs' : Array (Inversion x)
hk : ↑j < n
IH : ↑j < ↑j → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ invs
hjk : ↑j < ↑j + 1
this✝ : ↑i < ↑j
hl : l < ↑j
IH' : ↑i < l ∨ ↑j < ↑j → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ invs'
hil : ↑i < l + 1 ∨ ↑j < ↑j
this : ↑i ≤ l
⊢ { fst := i, snd := j, lt := hlt, inverted := hinv } ∈
    if h : x[l] > x[↑j] then
      Array.push invs'
        { fst := { val := l, isLt := (_ : l < n) }, snd := { val := ↑j, isLt := hk },
          lt := (_ : { val := l, isLt := (_ : l < n) } < { val := ↑j, isLt := hk }),
          inverted := (_ : x[↑{ val := l, isLt := (_ : l < n) }] > x[↑{ val := ↑j, isLt := hk }]) }
    else invs'
Tactic:
cases Nat.eq_or_lt_of_le this with
| inl heq =>
  cases heq; rewrite [dif_pos hinv]
  exact Array.mem_push.mpr <| Or.inr rfl
| inr hlt =>
  specialize IH' (Or.inl hlt)
  if hx : x[l]'(Nat.lt_trans hl j.2) > x[j.1] then
    rewrite [dif_pos hx]
    exact Array.mem_push.mpr <| Or.inl IH'
  else
    rewrite [dif_neg hx]; exact IH'
State after:
no goals

State before:
case succ.refine_2.inl.refl.inl
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt : i < j
hinv : x[↑i] > x[↑j]
invs : Array (Inversion x)
l : Nat
invs' : Array (Inversion x)
hk : ↑j < n
IH : ↑j < ↑j → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ invs
hjk : ↑j < ↑j + 1
this✝ : ↑i < ↑j
hl : l < ↑j
IH' : ↑i < l ∨ ↑j < ↑j → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ invs'
hil : ↑i < l + 1 ∨ ↑j < ↑j
this : ↑i ≤ l
heq : ↑i = l
⊢ { fst := i, snd := j, lt := hlt, inverted := hinv } ∈
    if h : x[l] > x[↑j] then
      Array.push invs'
        { fst := { val := l, isLt := (_ : l < n) }, snd := { val := ↑j, isLt := hk },
          lt := (_ : { val := l, isLt := (_ : l < n) } < { val := ↑j, isLt := hk }),
          inverted := (_ : x[↑{ val := l, isLt := (_ : l < n) }] > x[↑{ val := ↑j, isLt := hk }]) }
    else invs'
Tactic:
cases heq
State after:
case succ.refine_2.inl.refl.inl.refl
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt : i < j
hinv : x[↑i] > x[↑j]
invs invs' : Array (Inversion x)
hk : ↑j < n
IH : ↑j < ↑j → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ invs
hjk : ↑j < ↑j + 1
this✝ hl : ↑i < ↑j
IH' : ↑i < ↑i ∨ ↑j < ↑j → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ invs'
hil : ↑i < ↑i + 1 ∨ ↑j < ↑j
this : ↑i ≤ ↑i
⊢ { fst := i, snd := j, lt := hlt, inverted := hinv } ∈
    if h : x[↑i] > x[↑j] then
      Array.push invs'
        { fst := { val := ↑i, isLt := (_ : ↑i < n) }, snd := { val := ↑j, isLt := hk },
          lt := (_ : { val := ↑i, isLt := (_ : ↑i < n) } < { val := ↑j, isLt := hk }),
          inverted := (_ : x[↑{ val := ↑i, isLt := (_ : ↑i < n) }] > x[↑{ val := ↑j, isLt := hk }]) }
    else invs'

State before:
case succ.refine_2.inl.refl.inl.refl
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt : i < j
hinv : x[↑i] > x[↑j]
invs invs' : Array (Inversion x)
hk : ↑j < n
IH : ↑j < ↑j → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ invs
hjk : ↑j < ↑j + 1
this✝ hl : ↑i < ↑j
IH' : ↑i < ↑i ∨ ↑j < ↑j → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ invs'
hil : ↑i < ↑i + 1 ∨ ↑j < ↑j
this : ↑i ≤ ↑i
⊢ { fst := i, snd := j, lt := hlt, inverted := hinv } ∈
    if h : x[↑i] > x[↑j] then
      Array.push invs'
        { fst := { val := ↑i, isLt := (_ : ↑i < n) }, snd := { val := ↑j, isLt := hk },
          lt := (_ : { val := ↑i, isLt := (_ : ↑i < n) } < { val := ↑j, isLt := hk }),
          inverted := (_ : x[↑{ val := ↑i, isLt := (_ : ↑i < n) }] > x[↑{ val := ↑j, isLt := hk }]) }
    else invs'
Tactic:
rewrite [dif_pos hinv]
State after:
case succ.refine_2.inl.refl.inl.refl
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt : i < j
hinv : x[↑i] > x[↑j]
invs invs' : Array (Inversion x)
hk : ↑j < n
IH : ↑j < ↑j → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ invs
hjk : ↑j < ↑j + 1
this✝ hl : ↑i < ↑j
IH' : ↑i < ↑i ∨ ↑j < ↑j → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ invs'
hil : ↑i < ↑i + 1 ∨ ↑j < ↑j
this : ↑i ≤ ↑i
⊢ { fst := i, snd := j, lt := hlt, inverted := hinv } ∈
    Array.push invs'
      { fst := { val := ↑i, isLt := (_ : ↑i < n) }, snd := { val := ↑j, isLt := hk },
        lt := (_ : { val := ↑i, isLt := (_ : ↑i < n) } < { val := ↑j, isLt := hk }),
        inverted := (_ : x[↑{ val := ↑i, isLt := (_ : ↑i < n) }] > x[↑{ val := ↑j, isLt := hk }]) }

State before:
case succ.refine_2.inl.refl.inl.refl
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt : i < j
hinv : x[↑i] > x[↑j]
invs invs' : Array (Inversion x)
hk : ↑j < n
IH : ↑j < ↑j → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ invs
hjk : ↑j < ↑j + 1
this✝ hl : ↑i < ↑j
IH' : ↑i < ↑i ∨ ↑j < ↑j → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ invs'
hil : ↑i < ↑i + 1 ∨ ↑j < ↑j
this : ↑i ≤ ↑i
⊢ { fst := i, snd := j, lt := hlt, inverted := hinv } ∈
    Array.push invs'
      { fst := { val := ↑i, isLt := (_ : ↑i < n) }, snd := { val := ↑j, isLt := hk },
        lt := (_ : { val := ↑i, isLt := (_ : ↑i < n) } < { val := ↑j, isLt := hk }),
        inverted := (_ : x[↑{ val := ↑i, isLt := (_ : ↑i < n) }] > x[↑{ val := ↑j, isLt := hk }]) }
Tactic:
exact Array.mem_push.mpr <| Or.inr rfl
State after:
no goals

State before:
case succ.refine_2.inl.refl.inr
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt✝ : i < j
hinv : x[↑i] > x[↑j]
invs : Array (Inversion x)
l : Nat
invs' : Array (Inversion x)
hk : ↑j < n
IH : ↑j < ↑j → { fst := i, snd := j, lt := hlt✝, inverted := hinv } ∈ invs
hjk : ↑j < ↑j + 1
this✝ : ↑i < ↑j
hl : l < ↑j
IH' : ↑i < l ∨ ↑j < ↑j → { fst := i, snd := j, lt := hlt✝, inverted := hinv } ∈ invs'
hil : ↑i < l + 1 ∨ ↑j < ↑j
this : ↑i ≤ l
hlt : ↑i < l
⊢ { fst := i, snd := j, lt := hlt✝, inverted := hinv } ∈
    if h : x[l] > x[↑j] then
      Array.push invs'
        { fst := { val := l, isLt := (_ : l < n) }, snd := { val := ↑j, isLt := hk },
          lt := (_ : { val := l, isLt := (_ : l < n) } < { val := ↑j, isLt := hk }),
          inverted := (_ : x[↑{ val := l, isLt := (_ : l < n) }] > x[↑{ val := ↑j, isLt := hk }]) }
    else invs'
Tactic:
specialize IH' (Or.inl hlt)
State after:
case succ.refine_2.inl.refl.inr
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt✝ : i < j
hinv : x[↑i] > x[↑j]
invs : Array (Inversion x)
l : Nat
invs' : Array (Inversion x)
hk : ↑j < n
IH : ↑j < ↑j → { fst := i, snd := j, lt := hlt✝, inverted := hinv } ∈ invs
hjk : ↑j < ↑j + 1
this✝ : ↑i < ↑j
hl : l < ↑j
hil : ↑i < l + 1 ∨ ↑j < ↑j
this : ↑i ≤ l
hlt : ↑i < l
IH' : { fst := i, snd := j, lt := hlt✝, inverted := hinv } ∈ invs'
⊢ { fst := i, snd := j, lt := hlt✝, inverted := hinv } ∈
    if h : x[l] > x[↑j] then
      Array.push invs'
        { fst := { val := l, isLt := (_ : l < n) }, snd := { val := ↑j, isLt := hk },
          lt := (_ : { val := l, isLt := (_ : l < n) } < { val := ↑j, isLt := hk }),
          inverted := (_ : x[↑{ val := l, isLt := (_ : l < n) }] > x[↑{ val := ↑j, isLt := hk }]) }
    else invs'

State before:
case succ.refine_2.inl.refl.inr
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt✝ : i < j
hinv : x[↑i] > x[↑j]
invs : Array (Inversion x)
l : Nat
invs' : Array (Inversion x)
hk : ↑j < n
IH : ↑j < ↑j → { fst := i, snd := j, lt := hlt✝, inverted := hinv } ∈ invs
hjk : ↑j < ↑j + 1
this✝ : ↑i < ↑j
hl : l < ↑j
hil : ↑i < l + 1 ∨ ↑j < ↑j
this : ↑i ≤ l
hlt : ↑i < l
IH' : { fst := i, snd := j, lt := hlt✝, inverted := hinv } ∈ invs'
⊢ { fst := i, snd := j, lt := hlt✝, inverted := hinv } ∈
    if h : x[l] > x[↑j] then
      Array.push invs'
        { fst := { val := l, isLt := (_ : l < n) }, snd := { val := ↑j, isLt := hk },
          lt := (_ : { val := l, isLt := (_ : l < n) } < { val := ↑j, isLt := hk }),
          inverted := (_ : x[↑{ val := l, isLt := (_ : l < n) }] > x[↑{ val := ↑j, isLt := hk }]) }
    else invs'
Tactic:
if hx : x[l]'(Nat.lt_trans hl j.2) > x[j.1] then
  rewrite [dif_pos hx]
  exact Array.mem_push.mpr <| Or.inl IH'
else
  rewrite [dif_neg hx]; exact IH'
State after:
no goals

State before:
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt✝ : i < j
hinv : x[↑i] > x[↑j]
invs : Array (Inversion x)
l : Nat
invs' : Array (Inversion x)
hk : ↑j < n
IH : ↑j < ↑j → { fst := i, snd := j, lt := hlt✝, inverted := hinv } ∈ invs
hjk : ↑j < ↑j + 1
this✝ : ↑i < ↑j
hl : l < ↑j
hil : ↑i < l + 1 ∨ ↑j < ↑j
this : ↑i ≤ l
hlt : ↑i < l
IH' : { fst := i, snd := j, lt := hlt✝, inverted := hinv } ∈ invs'
hx : x[l] > x[↑j]
⊢ { fst := i, snd := j, lt := hlt✝, inverted := hinv } ∈
    if h : x[l] > x[↑j] then
      Array.push invs'
        { fst := { val := l, isLt := (_ : l < n) }, snd := { val := ↑j, isLt := hk },
          lt := (_ : { val := l, isLt := (_ : l < n) } < { val := ↑j, isLt := hk }),
          inverted := (_ : x[↑{ val := l, isLt := (_ : l < n) }] > x[↑{ val := ↑j, isLt := hk }]) }
    else invs'
Tactic:
rewrite [dif_pos hx]
State after:
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt✝ : i < j
hinv : x[↑i] > x[↑j]
invs : Array (Inversion x)
l : Nat
invs' : Array (Inversion x)
hk : ↑j < n
IH : ↑j < ↑j → { fst := i, snd := j, lt := hlt✝, inverted := hinv } ∈ invs
hjk : ↑j < ↑j + 1
this✝ : ↑i < ↑j
hl : l < ↑j
hil : ↑i < l + 1 ∨ ↑j < ↑j
this : ↑i ≤ l
hlt : ↑i < l
IH' : { fst := i, snd := j, lt := hlt✝, inverted := hinv } ∈ invs'
hx : x[l] > x[↑j]
⊢ { fst := i, snd := j, lt := hlt✝, inverted := hinv } ∈
    Array.push invs'
      { fst := { val := l, isLt := (_ : l < n) }, snd := { val := ↑j, isLt := hk },
        lt := (_ : { val := l, isLt := (_ : l < n) } < { val := ↑j, isLt := hk }),
        inverted := (_ : x[↑{ val := l, isLt := (_ : l < n) }] > x[↑{ val := ↑j, isLt := hk }]) }

State before:
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt✝ : i < j
hinv : x[↑i] > x[↑j]
invs : Array (Inversion x)
l : Nat
invs' : Array (Inversion x)
hk : ↑j < n
IH : ↑j < ↑j → { fst := i, snd := j, lt := hlt✝, inverted := hinv } ∈ invs
hjk : ↑j < ↑j + 1
this✝ : ↑i < ↑j
hl : l < ↑j
hil : ↑i < l + 1 ∨ ↑j < ↑j
this : ↑i ≤ l
hlt : ↑i < l
IH' : { fst := i, snd := j, lt := hlt✝, inverted := hinv } ∈ invs'
hx : x[l] > x[↑j]
⊢ { fst := i, snd := j, lt := hlt✝, inverted := hinv } ∈
    Array.push invs'
      { fst := { val := l, isLt := (_ : l < n) }, snd := { val := ↑j, isLt := hk },
        lt := (_ : { val := l, isLt := (_ : l < n) } < { val := ↑j, isLt := hk }),
        inverted := (_ : x[↑{ val := l, isLt := (_ : l < n) }] > x[↑{ val := ↑j, isLt := hk }]) }
Tactic:
exact Array.mem_push.mpr <| Or.inl IH'
State after:
no goals

State before:
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt✝ : i < j
hinv : x[↑i] > x[↑j]
invs : Array (Inversion x)
l : Nat
invs' : Array (Inversion x)
hk : ↑j < n
IH : ↑j < ↑j → { fst := i, snd := j, lt := hlt✝, inverted := hinv } ∈ invs
hjk : ↑j < ↑j + 1
this✝ : ↑i < ↑j
hl : l < ↑j
hil : ↑i < l + 1 ∨ ↑j < ↑j
this : ↑i ≤ l
hlt : ↑i < l
IH' : { fst := i, snd := j, lt := hlt✝, inverted := hinv } ∈ invs'
hx : ¬x[l] > x[↑j]
⊢ { fst := i, snd := j, lt := hlt✝, inverted := hinv } ∈
    if h : x[l] > x[↑j] then
      Array.push invs'
        { fst := { val := l, isLt := (_ : l < n) }, snd := { val := ↑j, isLt := hk },
          lt := (_ : { val := l, isLt := (_ : l < n) } < { val := ↑j, isLt := hk }),
          inverted := (_ : x[↑{ val := l, isLt := (_ : l < n) }] > x[↑{ val := ↑j, isLt := hk }]) }
    else invs'
Tactic:
rewrite [dif_neg hx]
State after:
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt✝ : i < j
hinv : x[↑i] > x[↑j]
invs : Array (Inversion x)
l : Nat
invs' : Array (Inversion x)
hk : ↑j < n
IH : ↑j < ↑j → { fst := i, snd := j, lt := hlt✝, inverted := hinv } ∈ invs
hjk : ↑j < ↑j + 1
this✝ : ↑i < ↑j
hl : l < ↑j
hil : ↑i < l + 1 ∨ ↑j < ↑j
this : ↑i ≤ l
hlt : ↑i < l
IH' : { fst := i, snd := j, lt := hlt✝, inverted := hinv } ∈ invs'
hx : ¬x[l] > x[↑j]
⊢ { fst := i, snd := j, lt := hlt✝, inverted := hinv } ∈ invs'

State before:
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt✝ : i < j
hinv : x[↑i] > x[↑j]
invs : Array (Inversion x)
l : Nat
invs' : Array (Inversion x)
hk : ↑j < n
IH : ↑j < ↑j → { fst := i, snd := j, lt := hlt✝, inverted := hinv } ∈ invs
hjk : ↑j < ↑j + 1
this✝ : ↑i < ↑j
hl : l < ↑j
hil : ↑i < l + 1 ∨ ↑j < ↑j
this : ↑i ≤ l
hlt : ↑i < l
IH' : { fst := i, snd := j, lt := hlt✝, inverted := hinv } ∈ invs'
hx : ¬x[l] > x[↑j]
⊢ { fst := i, snd := j, lt := hlt✝, inverted := hinv } ∈ invs'
Tactic:
exact IH'
State after:
no goals

State before:
case succ.refine_2.inr
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt✝ : i < j
hinv : x[↑i] > x[↑j]
k : Nat
hk : k < n
invs : Array (Inversion x)
IH : ↑j < k → { fst := i, snd := j, lt := hlt✝, inverted := hinv } ∈ invs
hjk : ↑j < k + 1
this : ↑i < k
l : Nat
hl : l < k
invs' : Array (Inversion x)
IH' : ↑i < l ∨ ↑j < k → { fst := i, snd := j, lt := hlt✝, inverted := hinv } ∈ invs'
hil : ↑i < l + 1 ∨ ↑j < k
hlt : ↑j < k
⊢ { fst := i, snd := j, lt := hlt✝, inverted := hinv } ∈
    if h : x[l] > x[k] then
      Array.push invs'
        { fst := { val := l, isLt := (_ : l < n) }, snd := { val := k, isLt := hk },
          lt := (_ : { val := l, isLt := (_ : l < n) } < { val := k, isLt := hk }),
          inverted := (_ : x[↑{ val := l, isLt := (_ : l < n) }] > x[↑{ val := k, isLt := hk }]) }
    else invs'
Tactic:
specialize IH' (Or.inr hlt)
State after:
case succ.refine_2.inr
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt✝ : i < j
hinv : x[↑i] > x[↑j]
k : Nat
hk : k < n
invs : Array (Inversion x)
IH : ↑j < k → { fst := i, snd := j, lt := hlt✝, inverted := hinv } ∈ invs
hjk : ↑j < k + 1
this : ↑i < k
l : Nat
hl : l < k
invs' : Array (Inversion x)
hil : ↑i < l + 1 ∨ ↑j < k
hlt : ↑j < k
IH' : { fst := i, snd := j, lt := hlt✝, inverted := hinv } ∈ invs'
⊢ { fst := i, snd := j, lt := hlt✝, inverted := hinv } ∈
    if h : x[l] > x[k] then
      Array.push invs'
        { fst := { val := l, isLt := (_ : l < n) }, snd := { val := k, isLt := hk },
          lt := (_ : { val := l, isLt := (_ : l < n) } < { val := k, isLt := hk }),
          inverted := (_ : x[↑{ val := l, isLt := (_ : l < n) }] > x[↑{ val := k, isLt := hk }]) }
    else invs'

State before:
case succ.refine_2.inr
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt✝ : i < j
hinv : x[↑i] > x[↑j]
k : Nat
hk : k < n
invs : Array (Inversion x)
IH : ↑j < k → { fst := i, snd := j, lt := hlt✝, inverted := hinv } ∈ invs
hjk : ↑j < k + 1
this : ↑i < k
l : Nat
hl : l < k
invs' : Array (Inversion x)
hil : ↑i < l + 1 ∨ ↑j < k
hlt : ↑j < k
IH' : { fst := i, snd := j, lt := hlt✝, inverted := hinv } ∈ invs'
⊢ { fst := i, snd := j, lt := hlt✝, inverted := hinv } ∈
    if h : x[l] > x[k] then
      Array.push invs'
        { fst := { val := l, isLt := (_ : l < n) }, snd := { val := k, isLt := hk },
          lt := (_ : { val := l, isLt := (_ : l < n) } < { val := k, isLt := hk }),
          inverted := (_ : x[↑{ val := l, isLt := (_ : l < n) }] > x[↑{ val := k, isLt := hk }]) }
    else invs'
Tactic:
if hx : x[l]'(Nat.lt_trans hl hk) > x[k]'hk then
  rewrite [dif_pos hx]
  exact Array.mem_push.mpr <| Or.inl IH'
else
  rewrite [dif_neg hx]; exact IH'
State after:
no goals

State before:
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt✝ : i < j
hinv : x[↑i] > x[↑j]
k : Nat
hk : k < n
invs : Array (Inversion x)
IH : ↑j < k → { fst := i, snd := j, lt := hlt✝, inverted := hinv } ∈ invs
hjk : ↑j < k + 1
this : ↑i < k
l : Nat
hl : l < k
invs' : Array (Inversion x)
hil : ↑i < l + 1 ∨ ↑j < k
hlt : ↑j < k
IH' : { fst := i, snd := j, lt := hlt✝, inverted := hinv } ∈ invs'
hx : x[l] > x[k]
⊢ { fst := i, snd := j, lt := hlt✝, inverted := hinv } ∈
    if h : x[l] > x[k] then
      Array.push invs'
        { fst := { val := l, isLt := (_ : l < n) }, snd := { val := k, isLt := hk },
          lt := (_ : { val := l, isLt := (_ : l < n) } < { val := k, isLt := hk }),
          inverted := (_ : x[↑{ val := l, isLt := (_ : l < n) }] > x[↑{ val := k, isLt := hk }]) }
    else invs'
Tactic:
rewrite [dif_pos hx]
State after:
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt✝ : i < j
hinv : x[↑i] > x[↑j]
k : Nat
hk : k < n
invs : Array (Inversion x)
IH : ↑j < k → { fst := i, snd := j, lt := hlt✝, inverted := hinv } ∈ invs
hjk : ↑j < k + 1
this : ↑i < k
l : Nat
hl : l < k
invs' : Array (Inversion x)
hil : ↑i < l + 1 ∨ ↑j < k
hlt : ↑j < k
IH' : { fst := i, snd := j, lt := hlt✝, inverted := hinv } ∈ invs'
hx : x[l] > x[k]
⊢ { fst := i, snd := j, lt := hlt✝, inverted := hinv } ∈
    Array.push invs'
      { fst := { val := l, isLt := (_ : l < n) }, snd := { val := k, isLt := hk },
        lt := (_ : { val := l, isLt := (_ : l < n) } < { val := k, isLt := hk }),
        inverted := (_ : x[↑{ val := l, isLt := (_ : l < n) }] > x[↑{ val := k, isLt := hk }]) }

State before:
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt✝ : i < j
hinv : x[↑i] > x[↑j]
k : Nat
hk : k < n
invs : Array (Inversion x)
IH : ↑j < k → { fst := i, snd := j, lt := hlt✝, inverted := hinv } ∈ invs
hjk : ↑j < k + 1
this : ↑i < k
l : Nat
hl : l < k
invs' : Array (Inversion x)
hil : ↑i < l + 1 ∨ ↑j < k
hlt : ↑j < k
IH' : { fst := i, snd := j, lt := hlt✝, inverted := hinv } ∈ invs'
hx : x[l] > x[k]
⊢ { fst := i, snd := j, lt := hlt✝, inverted := hinv } ∈
    Array.push invs'
      { fst := { val := l, isLt := (_ : l < n) }, snd := { val := k, isLt := hk },
        lt := (_ : { val := l, isLt := (_ : l < n) } < { val := k, isLt := hk }),
        inverted := (_ : x[↑{ val := l, isLt := (_ : l < n) }] > x[↑{ val := k, isLt := hk }]) }
Tactic:
exact Array.mem_push.mpr <| Or.inl IH'
State after:
no goals

State before:
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt✝ : i < j
hinv : x[↑i] > x[↑j]
k : Nat
hk : k < n
invs : Array (Inversion x)
IH : ↑j < k → { fst := i, snd := j, lt := hlt✝, inverted := hinv } ∈ invs
hjk : ↑j < k + 1
this : ↑i < k
l : Nat
hl : l < k
invs' : Array (Inversion x)
hil : ↑i < l + 1 ∨ ↑j < k
hlt : ↑j < k
IH' : { fst := i, snd := j, lt := hlt✝, inverted := hinv } ∈ invs'
hx : ¬x[l] > x[k]
⊢ { fst := i, snd := j, lt := hlt✝, inverted := hinv } ∈
    if h : x[l] > x[k] then
      Array.push invs'
        { fst := { val := l, isLt := (_ : l < n) }, snd := { val := k, isLt := hk },
          lt := (_ : { val := l, isLt := (_ : l < n) } < { val := k, isLt := hk }),
          inverted := (_ : x[↑{ val := l, isLt := (_ : l < n) }] > x[↑{ val := k, isLt := hk }]) }
    else invs'
Tactic:
rewrite [dif_neg hx]
State after:
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt✝ : i < j
hinv : x[↑i] > x[↑j]
k : Nat
hk : k < n
invs : Array (Inversion x)
IH : ↑j < k → { fst := i, snd := j, lt := hlt✝, inverted := hinv } ∈ invs
hjk : ↑j < k + 1
this : ↑i < k
l : Nat
hl : l < k
invs' : Array (Inversion x)
hil : ↑i < l + 1 ∨ ↑j < k
hlt : ↑j < k
IH' : { fst := i, snd := j, lt := hlt✝, inverted := hinv } ∈ invs'
hx : ¬x[l] > x[k]
⊢ { fst := i, snd := j, lt := hlt✝, inverted := hinv } ∈ invs'

State before:
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt✝ : i < j
hinv : x[↑i] > x[↑j]
k : Nat
hk : k < n
invs : Array (Inversion x)
IH : ↑j < k → { fst := i, snd := j, lt := hlt✝, inverted := hinv } ∈ invs
hjk : ↑j < k + 1
this : ↑i < k
l : Nat
hl : l < k
invs' : Array (Inversion x)
hil : ↑i < l + 1 ∨ ↑j < k
hlt : ↑j < k
IH' : { fst := i, snd := j, lt := hlt✝, inverted := hinv } ∈ invs'
hx : ¬x[l] > x[k]
⊢ { fst := i, snd := j, lt := hlt✝, inverted := hinv } ∈ invs'
Tactic:
exact IH'
State after:
no goals