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

State before:
n : Nat
x : Permutation n
⊢ Array.Nodup (inversions x)
Tactic:
suffices x.inversions.Nodup ∧ ∀ iv, iv ∈ x.inversions → iv.snd.1 < n
from this.1
State after:
n : Nat
x : Permutation n
⊢ Array.Nodup (inversions x) ∧ ∀ (iv : Inversion x), iv ∈ inversions x → ↑iv.snd < n

State before:
n : Nat
x : Permutation n
⊢ Array.Nodup (inversions x) ∧ ∀ (iv : Inversion x), iv ∈ inversions x → ↑iv.snd < n
Tactic:
dsimp [inversions]
State after:
n : Nat
x : Permutation n
⊢ Array.Nodup
      (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)
        #[]) ∧
    ∀ (iv : Inversion x),
      iv ∈
          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)
            #[] →
        ↑iv.snd < n

State before:
n : Nat
x : Permutation n
⊢ Array.Nodup
      (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)
        #[]) ∧
    ∀ (iv : Inversion x),
      iv ∈
          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)
            #[] →
        ↑iv.snd < n
Tactic:
refine Nat.fold'_induction (motive := fun k (ivs : Array (Inversion x)) => ivs.Nodup ∧ ∀ iv, iv ∈ ivs → iv.snd.1 < k) n _ #[] ?_ ?_
State after:
case refine_1
n : Nat
x : Permutation n
⊢ (fun k ivs => Array.Nodup ivs ∧ ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k) 0 #[]

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

State before:
case refine_1
n : Nat
x : Permutation n
⊢ (fun k ivs => Array.Nodup ivs ∧ ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k) 0 #[]

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

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

State before:
case refine_1
n : Nat
x : Permutation n
⊢ Array.Nodup #[] ∧ ∀ (iv : Inversion x), iv ∈ #[] → ↑iv.snd < 0

case refine_2
n : Nat
x : Permutation n
⊢ ∀ (i : Nat) (hi : i < n) (a : Array (Inversion x)),
    Array.Nodup a →
      (∀ (iv : Inversion x), iv ∈ a → ↑iv.snd < i) →
        Array.Nodup
            (Nat.fold' i
              (fun i_1 ivs =>
                if h : x[↑i_1] > x[i] then
                  Array.push ivs
                    { fst := Fin.castLE (_ : ↑{ val := i, isLt := hi } ≤ n) i_1, snd := { val := i, isLt := hi },
                      lt := (_ : ↑i_1 < ↑{ val := i, isLt := hi }), inverted := h }
                else ivs)
              a) ∧
          ∀ (iv : Inversion x),
            iv ∈
                Nat.fold' i
                  (fun i_1 ivs =>
                    if h : x[↑i_1] > x[i] then
                      Array.push ivs
                        { fst := Fin.castLE (_ : ↑{ val := i, isLt := hi } ≤ n) i_1, snd := { val := i, isLt := hi },
                          lt := (_ : ↑i_1 < ↑{ val := i, isLt := hi }), inverted := h }
                    else ivs)
                  a →
              ↑iv.snd < i + 1
Tactic:
. exact ⟨.nil, fun _ h => nomatch h⟩
State after:
case refine_2
n : Nat
x : Permutation n
⊢ ∀ (i : Nat) (hi : i < n) (a : Array (Inversion x)),
    Array.Nodup a →
      (∀ (iv : Inversion x), iv ∈ a → ↑iv.snd < i) →
        Array.Nodup
            (Nat.fold' i
              (fun i_1 ivs =>
                if h : x[↑i_1] > x[i] then
                  Array.push ivs
                    { fst := Fin.castLE (_ : ↑{ val := i, isLt := hi } ≤ n) i_1, snd := { val := i, isLt := hi },
                      lt := (_ : ↑i_1 < ↑{ val := i, isLt := hi }), inverted := h }
                else ivs)
              a) ∧
          ∀ (iv : Inversion x),
            iv ∈
                Nat.fold' i
                  (fun i_1 ivs =>
                    if h : x[↑i_1] > x[i] then
                      Array.push ivs
                        { fst := Fin.castLE (_ : ↑{ val := i, isLt := hi } ≤ n) i_1, snd := { val := i, isLt := hi },
                          lt := (_ : ↑i_1 < ↑{ val := i, isLt := hi }), inverted := h }
                    else ivs)
                  a →
              ↑iv.snd < i + 1

State before:
case refine_2
n : Nat
x : Permutation n
⊢ ∀ (i : Nat) (hi : i < n) (a : Array (Inversion x)),
    Array.Nodup a →
      (∀ (iv : Inversion x), iv ∈ a → ↑iv.snd < i) →
        Array.Nodup
            (Nat.fold' i
              (fun i_1 ivs =>
                if h : x[↑i_1] > x[i] then
                  Array.push ivs
                    { fst := Fin.castLE (_ : ↑{ val := i, isLt := hi } ≤ n) i_1, snd := { val := i, isLt := hi },
                      lt := (_ : ↑i_1 < ↑{ val := i, isLt := hi }), inverted := h }
                else ivs)
              a) ∧
          ∀ (iv : Inversion x),
            iv ∈
                Nat.fold' i
                  (fun i_1 ivs =>
                    if h : x[↑i_1] > x[i] then
                      Array.push ivs
                        { fst := Fin.castLE (_ : ↑{ val := i, isLt := hi } ≤ n) i_1, snd := { val := i, isLt := hi },
                          lt := (_ : ↑i_1 < ↑{ val := i, isLt := hi }), inverted := h }
                    else ivs)
                  a →
              ↑iv.snd < i + 1
Tactic:
. intro k hk ivs ivs_nodup ivs_lt
  generalize hivs' : Nat.fold' k _ ivs = ivs'
  suffices Array.Nodup ivs' ∧ ∀ iv, iv ∈ ivs' → iv.snd.1 < k ∨ (iv.snd.1 = k ∧ iv.fst.1 < k) by
    refine And.imp_right ?_ this
    intro hivs' iv hiv
    apply Nat.succ_le_succ; apply Nat.le_iff_lt_or_eq.mpr
    exact Or.imp_right And.left (hivs' iv hiv)
  cases hivs'
  refine Nat.fold'_induction (motive := fun l (ivs' : Array (Inversion x)) => ivs'.Nodup ∧ ∀ iv, iv ∈ ivs' → iv.snd.1 < k ∨ (iv.snd.1 = k ∧ iv.fst.1 < l)) k _ ivs ?_ ?_
  all_goals simp
  . exact And.intro ivs_nodup fun iv hiv => Or.inl <| ivs_lt iv hiv
  . intro l hl ivs' ivs'_nodup ivs'_lt
    if hx : x[l]'(Nat.lt_trans hl hk) > x[k] then
      simp only [dif_pos hx, Array.nodup_push, Array.mem_push, ivs'_nodup, true_and]
      constructor
      . intro h
        specialize ivs'_lt _ h; dsimp at ivs'_lt
        refine ivs'_lt.elim ?_ ?_
        . exact Nat.lt_irrefl k
        . intro h; exact Nat.lt_irrefl l h.2
      . intro iv hiv
        cases hiv with
        | inl hmem =>
          refine Or.imp_right ?_ <| ivs'_lt iv hmem
          exact And.imp_right Nat.le.step
        | inr heq =>
          cases heq; dsimp
          exact Or.inr ⟨rfl, l.lt_succ_self⟩
    else
      simp only [dif_neg hx]
      apply And.intro ivs'_nodup
      intro iv hiv; specialize ivs'_lt iv hiv
      refine Or.imp_right ?_ ivs'_lt
      exact And.imp_right Nat.le.step
State after:
no goals

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

State before:
case refine_1
n : Nat
x : Permutation n
⊢ Array.Nodup #[] ∧ ∀ (iv : Inversion x), iv ∈ #[] → ↑iv.snd < 0
Tactic:
exact ⟨.nil, fun _ h => nomatch h⟩
State after:
no goals

State before:
case refine_2
n : Nat
x : Permutation n
⊢ ∀ (i : Nat) (hi : i < n) (a : Array (Inversion x)),
    Array.Nodup a →
      (∀ (iv : Inversion x), iv ∈ a → ↑iv.snd < i) →
        Array.Nodup
            (Nat.fold' i
              (fun i_1 ivs =>
                if h : x[↑i_1] > x[i] then
                  Array.push ivs
                    { fst := Fin.castLE (_ : ↑{ val := i, isLt := hi } ≤ n) i_1, snd := { val := i, isLt := hi },
                      lt := (_ : ↑i_1 < ↑{ val := i, isLt := hi }), inverted := h }
                else ivs)
              a) ∧
          ∀ (iv : Inversion x),
            iv ∈
                Nat.fold' i
                  (fun i_1 ivs =>
                    if h : x[↑i_1] > x[i] then
                      Array.push ivs
                        { fst := Fin.castLE (_ : ↑{ val := i, isLt := hi } ≤ n) i_1, snd := { val := i, isLt := hi },
                          lt := (_ : ↑i_1 < ↑{ val := i, isLt := hi }), inverted := h }
                    else ivs)
                  a →
              ↑iv.snd < i + 1
Tactic:
intro k hk ivs ivs_nodup ivs_lt
State after:
case refine_2
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
⊢ Array.Nodup
      (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)
        ivs) ∧
    ∀ (iv : Inversion x),
      iv ∈
          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)
            ivs →
        ↑iv.snd < k + 1

State before:
case refine_2
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
⊢ Array.Nodup
      (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)
        ivs) ∧
    ∀ (iv : Inversion x),
      iv ∈
          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)
            ivs →
        ↑iv.snd < k + 1
Tactic:
generalize hivs' : Nat.fold' k _ ivs = ivs'
State after:
case refine_2
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
ivs' : Array (Inversion x)
hivs' :
  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)
      ivs =
    ivs'
⊢ Array.Nodup ivs' ∧ ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k + 1

State before:
case refine_2
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
ivs' : Array (Inversion x)
hivs' :
  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)
      ivs =
    ivs'
⊢ Array.Nodup ivs' ∧ ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k + 1
Tactic:
suffices Array.Nodup ivs' ∧ ∀ iv, iv ∈ ivs' → iv.snd.1 < k ∨ (iv.snd.1 = k ∧ iv.fst.1 < k) by
  refine And.imp_right ?_ this
  intro hivs' iv hiv
  apply Nat.succ_le_succ; apply Nat.le_iff_lt_or_eq.mpr
  exact Or.imp_right And.left (hivs' iv hiv)
State after:
case refine_2
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
ivs' : Array (Inversion x)
hivs' :
  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)
      ivs =
    ivs'
⊢ Array.Nodup ivs' ∧ ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < k

State before:
case refine_2
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
ivs' : Array (Inversion x)
hivs' :
  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)
      ivs =
    ivs'
⊢ Array.Nodup ivs' ∧ ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < k
Tactic:
cases hivs'
State after:
case refine_2.refl
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
⊢ Array.Nodup
      (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)
        ivs) ∧
    ∀ (iv : Inversion x),
      iv ∈
          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)
            ivs →
        ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < k

State before:
case refine_2.refl
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
⊢ Array.Nodup
      (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)
        ivs) ∧
    ∀ (iv : Inversion x),
      iv ∈
          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)
            ivs →
        ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < k
Tactic:
refine Nat.fold'_induction (motive := fun l (ivs' : Array (Inversion x)) => ivs'.Nodup ∧ ∀ iv, iv ∈ ivs' → iv.snd.1 < k ∨ (iv.snd.1 = k ∧ iv.fst.1 < l)) k _ ivs ?_ ?_
State after:
case refine_2.refl.refine_1
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
⊢ (fun l ivs' => Array.Nodup ivs' ∧ ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l) 0 ivs

case refine_2.refl.refine_2
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
⊢ ∀ (i : Nat) (hi : i < k) (a : Array (Inversion x)),
    (fun l ivs' => Array.Nodup ivs' ∧ ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l) i a →
      (fun l ivs' => Array.Nodup ivs' ∧ ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l)
        (i + 1)
        (if h : x[↑{ val := i, isLt := hi }] > x[k] then
          Array.push a
            { fst := Fin.castLE (_ : ↑{ val := k, isLt := hk } ≤ n) { val := i, isLt := hi },
              snd := { val := k, isLt := hk }, lt := (_ : ↑{ val := i, isLt := hi } < ↑{ val := k, isLt := hk }),
              inverted := h }
        else a)

State before:
case refine_2.refl.refine_1
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
⊢ (fun l ivs' => Array.Nodup ivs' ∧ ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l) 0 ivs

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

case refine_2.refl.refine_2
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
⊢ ∀ (i : Nat) (hi : i < k) (a : Array (Inversion x)),
    Array.Nodup a →
      (∀ (iv : Inversion x), iv ∈ a → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < i) →
        Array.Nodup
            (if h : x[i] > x[k] then
              Array.push a
                { fst := { val := i, isLt := (_ : i < n) }, snd := { val := k, isLt := hk },
                  lt := (_ : { val := i, isLt := (_ : i < n) } < { val := k, isLt := hk }),
                  inverted := (_ : x[↑{ val := i, isLt := (_ : i < n) }] > x[↑{ val := k, isLt := hk }]) }
            else a) ∧
          ∀ (iv : Inversion x),
            (iv ∈
                if h : x[i] > x[k] then
                  Array.push a
                    { fst := { val := i, isLt := (_ : i < n) }, snd := { val := k, isLt := hk },
                      lt := (_ : { val := i, isLt := (_ : i < n) } < { val := k, isLt := hk }),
                      inverted := (_ : x[↑{ val := i, isLt := (_ : i < n) }] > x[↑{ val := k, isLt := hk }]) }
                else a) →
              ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < i + 1

State before:
case refine_2.refl.refine_1
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
⊢ Array.Nodup ivs ∧ ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < 0

case refine_2.refl.refine_2
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
⊢ ∀ (i : Nat) (hi : i < k) (a : Array (Inversion x)),
    Array.Nodup a →
      (∀ (iv : Inversion x), iv ∈ a → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < i) →
        Array.Nodup
            (if h : x[i] > x[k] then
              Array.push a
                { fst := { val := i, isLt := (_ : i < n) }, snd := { val := k, isLt := hk },
                  lt := (_ : { val := i, isLt := (_ : i < n) } < { val := k, isLt := hk }),
                  inverted := (_ : x[↑{ val := i, isLt := (_ : i < n) }] > x[↑{ val := k, isLt := hk }]) }
            else a) ∧
          ∀ (iv : Inversion x),
            (iv ∈
                if h : x[i] > x[k] then
                  Array.push a
                    { fst := { val := i, isLt := (_ : i < n) }, snd := { val := k, isLt := hk },
                      lt := (_ : { val := i, isLt := (_ : i < n) } < { val := k, isLt := hk }),
                      inverted := (_ : x[↑{ val := i, isLt := (_ : i < n) }] > x[↑{ val := k, isLt := hk }]) }
                else a) →
              ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < i + 1
Tactic:
. exact And.intro ivs_nodup fun iv hiv => Or.inl <| ivs_lt iv hiv
State after:
case refine_2.refl.refine_2
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
⊢ ∀ (i : Nat) (hi : i < k) (a : Array (Inversion x)),
    Array.Nodup a →
      (∀ (iv : Inversion x), iv ∈ a → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < i) →
        Array.Nodup
            (if h : x[i] > x[k] then
              Array.push a
                { fst := { val := i, isLt := (_ : i < n) }, snd := { val := k, isLt := hk },
                  lt := (_ : { val := i, isLt := (_ : i < n) } < { val := k, isLt := hk }),
                  inverted := (_ : x[↑{ val := i, isLt := (_ : i < n) }] > x[↑{ val := k, isLt := hk }]) }
            else a) ∧
          ∀ (iv : Inversion x),
            (iv ∈
                if h : x[i] > x[k] then
                  Array.push a
                    { fst := { val := i, isLt := (_ : i < n) }, snd := { val := k, isLt := hk },
                      lt := (_ : { val := i, isLt := (_ : i < n) } < { val := k, isLt := hk }),
                      inverted := (_ : x[↑{ val := i, isLt := (_ : i < n) }] > x[↑{ val := k, isLt := hk }]) }
                else a) →
              ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < i + 1

State before:
case refine_2.refl.refine_2
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
⊢ ∀ (i : Nat) (hi : i < k) (a : Array (Inversion x)),
    Array.Nodup a →
      (∀ (iv : Inversion x), iv ∈ a → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < i) →
        Array.Nodup
            (if h : x[i] > x[k] then
              Array.push a
                { fst := { val := i, isLt := (_ : i < n) }, snd := { val := k, isLt := hk },
                  lt := (_ : { val := i, isLt := (_ : i < n) } < { val := k, isLt := hk }),
                  inverted := (_ : x[↑{ val := i, isLt := (_ : i < n) }] > x[↑{ val := k, isLt := hk }]) }
            else a) ∧
          ∀ (iv : Inversion x),
            (iv ∈
                if h : x[i] > x[k] then
                  Array.push a
                    { fst := { val := i, isLt := (_ : i < n) }, snd := { val := k, isLt := hk },
                      lt := (_ : { val := i, isLt := (_ : i < n) } < { val := k, isLt := hk }),
                      inverted := (_ : x[↑{ val := i, isLt := (_ : i < n) }] > x[↑{ val := k, isLt := hk }]) }
                else a) →
              ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < i + 1
Tactic:
. intro l hl ivs' ivs'_nodup ivs'_lt
  if hx : x[l]'(Nat.lt_trans hl hk) > x[k] then
    simp only [dif_pos hx, Array.nodup_push, Array.mem_push, ivs'_nodup, true_and]
    constructor
    . intro h
      specialize ivs'_lt _ h; dsimp at ivs'_lt
      refine ivs'_lt.elim ?_ ?_
      . exact Nat.lt_irrefl k
      . intro h; exact Nat.lt_irrefl l h.2
    . intro iv hiv
      cases hiv with
      | inl hmem =>
        refine Or.imp_right ?_ <| ivs'_lt iv hmem
        exact And.imp_right Nat.le.step
      | inr heq =>
        cases heq; dsimp
        exact Or.inr ⟨rfl, l.lt_succ_self⟩
  else
    simp only [dif_neg hx]
    apply And.intro ivs'_nodup
    intro iv hiv; specialize ivs'_lt iv hiv
    refine Or.imp_right ?_ ivs'_lt
    exact And.imp_right Nat.le.step
State after:
no goals

State before:
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
ivs' : Array (Inversion x)
hivs' :
  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)
      ivs =
    ivs'
this : Array.Nodup ivs' ∧ ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < k
⊢ Array.Nodup ivs' ∧ ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k + 1
Tactic:
refine And.imp_right ?_ this
State after:
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
ivs' : Array (Inversion x)
hivs' :
  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)
      ivs =
    ivs'
this : Array.Nodup ivs' ∧ ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < k
⊢ (∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < k) →
    ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k + 1

State before:
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
ivs' : Array (Inversion x)
hivs' :
  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)
      ivs =
    ivs'
this : Array.Nodup ivs' ∧ ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < k
⊢ (∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < k) →
    ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k + 1
Tactic:
intro hivs' iv hiv
State after:
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
ivs' : Array (Inversion x)
hivs'✝ :
  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)
      ivs =
    ivs'
this : Array.Nodup ivs' ∧ ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < k
hivs' : ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < k
iv : Inversion x
hiv : iv ∈ ivs'
⊢ ↑iv.snd < k + 1

State before:
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
ivs' : Array (Inversion x)
hivs'✝ :
  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)
      ivs =
    ivs'
this : Array.Nodup ivs' ∧ ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < k
hivs' : ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < k
iv : Inversion x
hiv : iv ∈ ivs'
⊢ ↑iv.snd < k + 1
Tactic:
apply Nat.succ_le_succ
State after:
case a
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
ivs' : Array (Inversion x)
hivs'✝ :
  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)
      ivs =
    ivs'
this : Array.Nodup ivs' ∧ ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < k
hivs' : ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < k
iv : Inversion x
hiv : iv ∈ ivs'
⊢ ↑iv.snd ≤ k

State before:
case a
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
ivs' : Array (Inversion x)
hivs'✝ :
  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)
      ivs =
    ivs'
this : Array.Nodup ivs' ∧ ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < k
hivs' : ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < k
iv : Inversion x
hiv : iv ∈ ivs'
⊢ ↑iv.snd ≤ k
Tactic:
apply Nat.le_iff_lt_or_eq.mpr
State after:
case a
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
ivs' : Array (Inversion x)
hivs'✝ :
  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)
      ivs =
    ivs'
this : Array.Nodup ivs' ∧ ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < k
hivs' : ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < k
iv : Inversion x
hiv : iv ∈ ivs'
⊢ ↑iv.snd < k ∨ ↑iv.snd = k

State before:
case a
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
ivs' : Array (Inversion x)
hivs'✝ :
  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)
      ivs =
    ivs'
this : Array.Nodup ivs' ∧ ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < k
hivs' : ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < k
iv : Inversion x
hiv : iv ∈ ivs'
⊢ ↑iv.snd < k ∨ ↑iv.snd = k
Tactic:
exact Or.imp_right And.left (hivs' iv hiv)
State after:
no goals

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

State before:
case refine_2.refl.refine_1
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
⊢ Array.Nodup ivs ∧ ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < 0
Tactic:
exact And.intro ivs_nodup fun iv hiv => Or.inl <| ivs_lt iv hiv
State after:
no goals

State before:
case refine_2.refl.refine_2
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
⊢ ∀ (i : Nat) (hi : i < k) (a : Array (Inversion x)),
    Array.Nodup a →
      (∀ (iv : Inversion x), iv ∈ a → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < i) →
        Array.Nodup
            (if h : x[i] > x[k] then
              Array.push a
                { fst := { val := i, isLt := (_ : i < n) }, snd := { val := k, isLt := hk },
                  lt := (_ : { val := i, isLt := (_ : i < n) } < { val := k, isLt := hk }),
                  inverted := (_ : x[↑{ val := i, isLt := (_ : i < n) }] > x[↑{ val := k, isLt := hk }]) }
            else a) ∧
          ∀ (iv : Inversion x),
            (iv ∈
                if h : x[i] > x[k] then
                  Array.push a
                    { fst := { val := i, isLt := (_ : i < n) }, snd := { val := k, isLt := hk },
                      lt := (_ : { val := i, isLt := (_ : i < n) } < { val := k, isLt := hk }),
                      inverted := (_ : x[↑{ val := i, isLt := (_ : i < n) }] > x[↑{ val := k, isLt := hk }]) }
                else a) →
              ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < i + 1
Tactic:
intro l hl ivs' ivs'_nodup ivs'_lt
State after:
case refine_2.refl.refine_2
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
l : Nat
hl : l < k
ivs' : Array (Inversion x)
ivs'_nodup : Array.Nodup ivs'
ivs'_lt : ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l
⊢ Array.Nodup
      (if h : x[l] > x[k] then
        Array.push ivs'
          { 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 ivs') ∧
    ∀ (iv : Inversion x),
      (iv ∈
          if h : x[l] > x[k] then
            Array.push ivs'
              { 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 ivs') →
        ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l + 1

State before:
case refine_2.refl.refine_2
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
l : Nat
hl : l < k
ivs' : Array (Inversion x)
ivs'_nodup : Array.Nodup ivs'
ivs'_lt : ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l
⊢ Array.Nodup
      (if h : x[l] > x[k] then
        Array.push ivs'
          { 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 ivs') ∧
    ∀ (iv : Inversion x),
      (iv ∈
          if h : x[l] > x[k] then
            Array.push ivs'
              { 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 ivs') →
        ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l + 1
Tactic:
if hx : x[l]'(Nat.lt_trans hl hk) > x[k] then
  simp only [dif_pos hx, Array.nodup_push, Array.mem_push, ivs'_nodup, true_and]
  constructor
  . intro h
    specialize ivs'_lt _ h; dsimp at ivs'_lt
    refine ivs'_lt.elim ?_ ?_
    . exact Nat.lt_irrefl k
    . intro h; exact Nat.lt_irrefl l h.2
  . intro iv hiv
    cases hiv with
    | inl hmem =>
      refine Or.imp_right ?_ <| ivs'_lt iv hmem
      exact And.imp_right Nat.le.step
    | inr heq =>
      cases heq; dsimp
      exact Or.inr ⟨rfl, l.lt_succ_self⟩
else
  simp only [dif_neg hx]
  apply And.intro ivs'_nodup
  intro iv hiv; specialize ivs'_lt iv hiv
  refine Or.imp_right ?_ ivs'_lt
  exact And.imp_right Nat.le.step
State after:
no goals

State before:
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
l : Nat
hl : l < k
ivs' : Array (Inversion x)
ivs'_nodup : Array.Nodup ivs'
ivs'_lt : ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l
hx : x[l] > x[k]
⊢ Array.Nodup
      (if h : x[l] > x[k] then
        Array.push ivs'
          { 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 ivs') ∧
    ∀ (iv : Inversion x),
      (iv ∈
          if h : x[l] > x[k] then
            Array.push ivs'
              { 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 ivs') →
        ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l + 1
Tactic:
simp only [dif_pos hx, Array.nodup_push, Array.mem_push, ivs'_nodup, true_and]
State after:
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
l : Nat
hl : l < k
ivs' : Array (Inversion x)
ivs'_nodup : Array.Nodup ivs'
ivs'_lt : ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l
hx : x[l] > x[k]
⊢ ¬{ 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 }]) } ∈
        ivs' ∧
    ∀ (iv : Inversion x),
      iv ∈ ivs' ∨
          iv =
            { 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 }]) } →
        ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l + 1

State before:
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
l : Nat
hl : l < k
ivs' : Array (Inversion x)
ivs'_nodup : Array.Nodup ivs'
ivs'_lt : ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l
hx : x[l] > x[k]
⊢ ¬{ 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 }]) } ∈
        ivs' ∧
    ∀ (iv : Inversion x),
      iv ∈ ivs' ∨
          iv =
            { 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 }]) } →
        ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l + 1
Tactic:
constructor
State after:
case left
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
l : Nat
hl : l < k
ivs' : Array (Inversion x)
ivs'_nodup : Array.Nodup ivs'
ivs'_lt : ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l
hx : x[l] > x[k]
⊢ ¬{ 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 }]) } ∈
      ivs'

case right
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
l : Nat
hl : l < k
ivs' : Array (Inversion x)
ivs'_nodup : Array.Nodup ivs'
ivs'_lt : ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l
hx : x[l] > x[k]
⊢ ∀ (iv : Inversion x),
    iv ∈ ivs' ∨
        iv =
          { 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 }]) } →
      ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l + 1

State before:
case left
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
l : Nat
hl : l < k
ivs' : Array (Inversion x)
ivs'_nodup : Array.Nodup ivs'
ivs'_lt : ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l
hx : x[l] > x[k]
⊢ ¬{ 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 }]) } ∈
      ivs'

case right
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
l : Nat
hl : l < k
ivs' : Array (Inversion x)
ivs'_nodup : Array.Nodup ivs'
ivs'_lt : ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l
hx : x[l] > x[k]
⊢ ∀ (iv : Inversion x),
    iv ∈ ivs' ∨
        iv =
          { 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 }]) } →
      ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l + 1
Tactic:
. intro h
  specialize ivs'_lt _ h; dsimp at ivs'_lt
  refine ivs'_lt.elim ?_ ?_
  . exact Nat.lt_irrefl k
  . intro h; exact Nat.lt_irrefl l h.2
State after:
case right
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
l : Nat
hl : l < k
ivs' : Array (Inversion x)
ivs'_nodup : Array.Nodup ivs'
ivs'_lt : ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l
hx : x[l] > x[k]
⊢ ∀ (iv : Inversion x),
    iv ∈ ivs' ∨
        iv =
          { 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 }]) } →
      ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l + 1

State before:
case right
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
l : Nat
hl : l < k
ivs' : Array (Inversion x)
ivs'_nodup : Array.Nodup ivs'
ivs'_lt : ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l
hx : x[l] > x[k]
⊢ ∀ (iv : Inversion x),
    iv ∈ ivs' ∨
        iv =
          { 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 }]) } →
      ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l + 1
Tactic:
. intro iv hiv
  cases hiv with
  | inl hmem =>
    refine Or.imp_right ?_ <| ivs'_lt iv hmem
    exact And.imp_right Nat.le.step
  | inr heq =>
    cases heq; dsimp
    exact Or.inr ⟨rfl, l.lt_succ_self⟩
State after:
no goals

State before:
case left
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
l : Nat
hl : l < k
ivs' : Array (Inversion x)
ivs'_nodup : Array.Nodup ivs'
ivs'_lt : ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l
hx : x[l] > x[k]
⊢ ¬{ 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 }]) } ∈
      ivs'
Tactic:
intro h
State after:
case left
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
l : Nat
hl : l < k
ivs' : Array (Inversion x)
ivs'_nodup : Array.Nodup ivs'
ivs'_lt : ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l
hx : x[l] > x[k]
h :
  { 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 }]) } ∈
    ivs'
⊢ False

State before:
case left
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
l : Nat
hl : l < k
ivs' : Array (Inversion x)
ivs'_nodup : Array.Nodup ivs'
ivs'_lt : ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l
hx : x[l] > x[k]
h :
  { 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 }]) } ∈
    ivs'
⊢ False
Tactic:
specialize ivs'_lt _ h
State after:
case left
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
l : Nat
hl : l < k
ivs' : Array (Inversion x)
ivs'_nodup : Array.Nodup ivs'
hx : x[l] > x[k]
h :
  { 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 }]) } ∈
    ivs'
ivs'_lt :
  ↑{ 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 }]) }.snd <
      k ∨
    ↑{ 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 }]) }.snd =
        k ∧
      ↑{ 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 }]) }.fst <
        l
⊢ False

State before:
case left
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
l : Nat
hl : l < k
ivs' : Array (Inversion x)
ivs'_nodup : Array.Nodup ivs'
hx : x[l] > x[k]
h :
  { 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 }]) } ∈
    ivs'
ivs'_lt :
  ↑{ 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 }]) }.snd <
      k ∨
    ↑{ 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 }]) }.snd =
        k ∧
      ↑{ 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 }]) }.fst <
        l
⊢ False
Tactic:
dsimp at ivs'_lt
State after:
case left
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
l : Nat
hl : l < k
ivs' : Array (Inversion x)
ivs'_nodup : Array.Nodup ivs'
hx : x[l] > x[k]
h :
  { 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 }]) } ∈
    ivs'
ivs'_lt : k < k ∨ k = k ∧ l < l
⊢ False

State before:
case left
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
l : Nat
hl : l < k
ivs' : Array (Inversion x)
ivs'_nodup : Array.Nodup ivs'
hx : x[l] > x[k]
h :
  { 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 }]) } ∈
    ivs'
ivs'_lt : k < k ∨ k = k ∧ l < l
⊢ False
Tactic:
refine ivs'_lt.elim ?_ ?_
State after:
case left.refine_1
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
l : Nat
hl : l < k
ivs' : Array (Inversion x)
ivs'_nodup : Array.Nodup ivs'
hx : x[l] > x[k]
h :
  { 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 }]) } ∈
    ivs'
ivs'_lt : k < k ∨ k = k ∧ l < l
⊢ k < k → False

case left.refine_2
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
l : Nat
hl : l < k
ivs' : Array (Inversion x)
ivs'_nodup : Array.Nodup ivs'
hx : x[l] > x[k]
h :
  { 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 }]) } ∈
    ivs'
ivs'_lt : k < k ∨ k = k ∧ l < l
⊢ k = k ∧ l < l → False

State before:
case left.refine_1
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
l : Nat
hl : l < k
ivs' : Array (Inversion x)
ivs'_nodup : Array.Nodup ivs'
hx : x[l] > x[k]
h :
  { 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 }]) } ∈
    ivs'
ivs'_lt : k < k ∨ k = k ∧ l < l
⊢ k < k → False

case left.refine_2
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
l : Nat
hl : l < k
ivs' : Array (Inversion x)
ivs'_nodup : Array.Nodup ivs'
hx : x[l] > x[k]
h :
  { 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 }]) } ∈
    ivs'
ivs'_lt : k < k ∨ k = k ∧ l < l
⊢ k = k ∧ l < l → False
Tactic:
. exact Nat.lt_irrefl k
State after:
case left.refine_2
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
l : Nat
hl : l < k
ivs' : Array (Inversion x)
ivs'_nodup : Array.Nodup ivs'
hx : x[l] > x[k]
h :
  { 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 }]) } ∈
    ivs'
ivs'_lt : k < k ∨ k = k ∧ l < l
⊢ k = k ∧ l < l → False

State before:
case left.refine_2
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
l : Nat
hl : l < k
ivs' : Array (Inversion x)
ivs'_nodup : Array.Nodup ivs'
hx : x[l] > x[k]
h :
  { 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 }]) } ∈
    ivs'
ivs'_lt : k < k ∨ k = k ∧ l < l
⊢ k = k ∧ l < l → False
Tactic:
. intro h; exact Nat.lt_irrefl l h.2
State after:
no goals

State before:
case left.refine_1
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
l : Nat
hl : l < k
ivs' : Array (Inversion x)
ivs'_nodup : Array.Nodup ivs'
hx : x[l] > x[k]
h :
  { 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 }]) } ∈
    ivs'
ivs'_lt : k < k ∨ k = k ∧ l < l
⊢ k < k → False
Tactic:
exact Nat.lt_irrefl k
State after:
no goals

State before:
case left.refine_2
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
l : Nat
hl : l < k
ivs' : Array (Inversion x)
ivs'_nodup : Array.Nodup ivs'
hx : x[l] > x[k]
h :
  { 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 }]) } ∈
    ivs'
ivs'_lt : k < k ∨ k = k ∧ l < l
⊢ k = k ∧ l < l → False
Tactic:
intro h
State after:
case left.refine_2
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
l : Nat
hl : l < k
ivs' : Array (Inversion x)
ivs'_nodup : Array.Nodup ivs'
hx : x[l] > x[k]
h✝ :
  { 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 }]) } ∈
    ivs'
ivs'_lt : k < k ∨ k = k ∧ l < l
h : k = k ∧ l < l
⊢ False

State before:
case left.refine_2
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
l : Nat
hl : l < k
ivs' : Array (Inversion x)
ivs'_nodup : Array.Nodup ivs'
hx : x[l] > x[k]
h✝ :
  { 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 }]) } ∈
    ivs'
ivs'_lt : k < k ∨ k = k ∧ l < l
h : k = k ∧ l < l
⊢ False
Tactic:
exact Nat.lt_irrefl l h.2
State after:
no goals

State before:
case right
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
l : Nat
hl : l < k
ivs' : Array (Inversion x)
ivs'_nodup : Array.Nodup ivs'
ivs'_lt : ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l
hx : x[l] > x[k]
⊢ ∀ (iv : Inversion x),
    iv ∈ ivs' ∨
        iv =
          { 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 }]) } →
      ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l + 1
Tactic:
intro iv hiv
State after:
case right
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
l : Nat
hl : l < k
ivs' : Array (Inversion x)
ivs'_nodup : Array.Nodup ivs'
ivs'_lt : ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l
hx : x[l] > x[k]
iv : Inversion x
hiv :
  iv ∈ ivs' ∨
    iv =
      { 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 }]) }
⊢ ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l + 1

State before:
case right
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
l : Nat
hl : l < k
ivs' : Array (Inversion x)
ivs'_nodup : Array.Nodup ivs'
ivs'_lt : ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l
hx : x[l] > x[k]
iv : Inversion x
hiv :
  iv ∈ ivs' ∨
    iv =
      { 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 }]) }
⊢ ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l + 1
Tactic:
cases hiv with
| inl hmem =>
  refine Or.imp_right ?_ <| ivs'_lt iv hmem
  exact And.imp_right Nat.le.step
| inr heq =>
  cases heq; dsimp
  exact Or.inr ⟨rfl, l.lt_succ_self⟩
State after:
no goals

State before:
case right.inl
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
l : Nat
hl : l < k
ivs' : Array (Inversion x)
ivs'_nodup : Array.Nodup ivs'
ivs'_lt : ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l
hx : x[l] > x[k]
iv : Inversion x
hmem : iv ∈ ivs'
⊢ ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l + 1
Tactic:
refine Or.imp_right ?_ <| ivs'_lt iv hmem
State after:
case right.inl
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
l : Nat
hl : l < k
ivs' : Array (Inversion x)
ivs'_nodup : Array.Nodup ivs'
ivs'_lt : ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l
hx : x[l] > x[k]
iv : Inversion x
hmem : iv ∈ ivs'
⊢ ↑iv.snd = k ∧ ↑iv.fst < l → ↑iv.snd = k ∧ ↑iv.fst < l + 1

State before:
case right.inl
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
l : Nat
hl : l < k
ivs' : Array (Inversion x)
ivs'_nodup : Array.Nodup ivs'
ivs'_lt : ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l
hx : x[l] > x[k]
iv : Inversion x
hmem : iv ∈ ivs'
⊢ ↑iv.snd = k ∧ ↑iv.fst < l → ↑iv.snd = k ∧ ↑iv.fst < l + 1
Tactic:
exact And.imp_right Nat.le.step
State after:
no goals

State before:
case right.inr
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
l : Nat
hl : l < k
ivs' : Array (Inversion x)
ivs'_nodup : Array.Nodup ivs'
ivs'_lt : ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l
hx : x[l] > x[k]
iv : Inversion x
heq :
  iv =
    { 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 }]) }
⊢ ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l + 1
Tactic:
cases heq
State after:
case right.inr.refl
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
l : Nat
hl : l < k
ivs' : Array (Inversion x)
ivs'_nodup : Array.Nodup ivs'
ivs'_lt : ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l
hx : x[l] > x[k]
⊢ ↑{ 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 }]) }.snd <
      k ∨
    ↑{ 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 }]) }.snd =
        k ∧
      ↑{ 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 }]) }.fst <
        l + 1

State before:
case right.inr.refl
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
l : Nat
hl : l < k
ivs' : Array (Inversion x)
ivs'_nodup : Array.Nodup ivs'
ivs'_lt : ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l
hx : x[l] > x[k]
⊢ ↑{ 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 }]) }.snd <
      k ∨
    ↑{ 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 }]) }.snd =
        k ∧
      ↑{ 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 }]) }.fst <
        l + 1
Tactic:
dsimp
State after:
case right.inr.refl
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
l : Nat
hl : l < k
ivs' : Array (Inversion x)
ivs'_nodup : Array.Nodup ivs'
ivs'_lt : ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l
hx : x[l] > x[k]
⊢ k < k ∨ k = k ∧ l < l + 1

State before:
case right.inr.refl
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
l : Nat
hl : l < k
ivs' : Array (Inversion x)
ivs'_nodup : Array.Nodup ivs'
ivs'_lt : ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l
hx : x[l] > x[k]
⊢ k < k ∨ k = k ∧ l < l + 1
Tactic:
exact Or.inr ⟨rfl, l.lt_succ_self⟩
State after:
no goals

State before:
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
l : Nat
hl : l < k
ivs' : Array (Inversion x)
ivs'_nodup : Array.Nodup ivs'
ivs'_lt : ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l
hx : ¬x[l] > x[k]
⊢ Array.Nodup
      (if h : x[l] > x[k] then
        Array.push ivs'
          { 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 ivs') ∧
    ∀ (iv : Inversion x),
      (iv ∈
          if h : x[l] > x[k] then
            Array.push ivs'
              { 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 ivs') →
        ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l + 1
Tactic:
simp only [dif_neg hx]
State after:
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
l : Nat
hl : l < k
ivs' : Array (Inversion x)
ivs'_nodup : Array.Nodup ivs'
ivs'_lt : ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l
hx : ¬x[l] > x[k]
⊢ Array.Nodup ivs' ∧ ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l + 1

State before:
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
l : Nat
hl : l < k
ivs' : Array (Inversion x)
ivs'_nodup : Array.Nodup ivs'
ivs'_lt : ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l
hx : ¬x[l] > x[k]
⊢ Array.Nodup ivs' ∧ ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l + 1
Tactic:
apply And.intro ivs'_nodup
State after:
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
l : Nat
hl : l < k
ivs' : Array (Inversion x)
ivs'_nodup : Array.Nodup ivs'
ivs'_lt : ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l
hx : ¬x[l] > x[k]
⊢ ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l + 1

State before:
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
l : Nat
hl : l < k
ivs' : Array (Inversion x)
ivs'_nodup : Array.Nodup ivs'
ivs'_lt : ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l
hx : ¬x[l] > x[k]
⊢ ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l + 1
Tactic:
intro iv hiv
State after:
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
l : Nat
hl : l < k
ivs' : Array (Inversion x)
ivs'_nodup : Array.Nodup ivs'
ivs'_lt : ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l
hx : ¬x[l] > x[k]
iv : Inversion x
hiv : iv ∈ ivs'
⊢ ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l + 1

State before:
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
l : Nat
hl : l < k
ivs' : Array (Inversion x)
ivs'_nodup : Array.Nodup ivs'
ivs'_lt : ∀ (iv : Inversion x), iv ∈ ivs' → ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l
hx : ¬x[l] > x[k]
iv : Inversion x
hiv : iv ∈ ivs'
⊢ ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l + 1
Tactic:
specialize ivs'_lt iv hiv
State after:
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
l : Nat
hl : l < k
ivs' : Array (Inversion x)
ivs'_nodup : Array.Nodup ivs'
hx : ¬x[l] > x[k]
iv : Inversion x
hiv : iv ∈ ivs'
ivs'_lt : ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l
⊢ ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l + 1

State before:
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
l : Nat
hl : l < k
ivs' : Array (Inversion x)
ivs'_nodup : Array.Nodup ivs'
hx : ¬x[l] > x[k]
iv : Inversion x
hiv : iv ∈ ivs'
ivs'_lt : ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l
⊢ ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l + 1
Tactic:
refine Or.imp_right ?_ ivs'_lt
State after:
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
l : Nat
hl : l < k
ivs' : Array (Inversion x)
ivs'_nodup : Array.Nodup ivs'
hx : ¬x[l] > x[k]
iv : Inversion x
hiv : iv ∈ ivs'
ivs'_lt : ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l
⊢ ↑iv.snd = k ∧ ↑iv.fst < l → ↑iv.snd = k ∧ ↑iv.fst < l + 1

State before:
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
l : Nat
hl : l < k
ivs' : Array (Inversion x)
ivs'_nodup : Array.Nodup ivs'
hx : ¬x[l] > x[k]
iv : Inversion x
hiv : iv ∈ ivs'
ivs'_lt : ↑iv.snd < k ∨ ↑iv.snd = k ∧ ↑iv.fst < l
⊢ ↑iv.snd = k ∧ ↑iv.fst < l → ↑iv.snd = k ∧ ↑iv.fst < l + 1
Tactic:
exact And.imp_right Nat.le.step
State after:
no goals