Theorem: Algdata.BinaryHeap.exists_get_popMax (Algdata/Data/BinaryHeap/Basic.lean)

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
⊢ ∃ k hk, 0 < k ∧ (popMax lt x)[i] = x[k]
Tactic:
delta popMax
State after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
⊢ ∃ k hk,
    0 < k ∧
      (if h : x.start < x.stop then
            let_fun this := (_ : 0 < x.stop - x.start);
            let x :=
              Subarray.swap x { val := 0, isLt := this }
                { val := Subarray.size x - 1,
                  isLt := (_ : Nat.pred (Nat.sub (Subarray.size x) 0) < Nat.sub (Subarray.size x) 0) };
            heapifyDown lt (Subarray.shrinkOne' x h) 0
          else x)[i] =
        x[k]

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
⊢ ∃ k hk,
    0 < k ∧
      (if h : x.start < x.stop then
            let_fun this := (_ : 0 < x.stop - x.start);
            let x :=
              Subarray.swap x { val := 0, isLt := this }
                { val := Subarray.size x - 1,
                  isLt := (_ : Nat.pred (Nat.sub (Subarray.size x) 0) < Nat.sub (Subarray.size x) 0) };
            heapifyDown lt (Subarray.shrinkOne' x h) 0
          else x)[i] =
        x[k]
Tactic:
dsimp
State after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
⊢ ∃ k hk,
    0 < k ∧
      (if h : x.start < x.stop then
            heapifyDown lt
              (Subarray.shrinkOne'
                (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
                  { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
                h)
              0
          else x)[i] =
        x[k]

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
⊢ ∃ k hk,
    0 < k ∧
      (if h : x.start < x.stop then
            heapifyDown lt
              (Subarray.shrinkOne'
                (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
                  { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
                h)
              0
          else x)[i] =
        x[k]
Tactic:
have : i + 1 < x.stop - x.start := Nat.add_lt_of_lt_sub hi
State after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
this : i + 1 < x.stop - x.start
⊢ ∃ k hk,
    0 < k ∧
      (if h : x.start < x.stop then
            heapifyDown lt
              (Subarray.shrinkOne'
                (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
                  { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
                h)
              0
          else x)[i] =
        x[k]

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
this : i + 1 < x.stop - x.start
⊢ ∃ k hk,
    0 < k ∧
      (if h : x.start < x.stop then
            heapifyDown lt
              (Subarray.shrinkOne'
                (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
                  { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
                h)
              0
          else x)[i] =
        x[k]
Tactic:
have : x.start < x.stop := calc
  x.start < i+1+x.start := Nat.lt_add_of_pos_left i.zero_lt_succ
  _       < x.stop := Nat.add_lt_of_lt_sub this
State after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
this✝ : i + 1 < x.stop - x.start
this : x.start < x.stop
⊢ ∃ k hk,
    0 < k ∧
      (if h : x.start < x.stop then
            heapifyDown lt
              (Subarray.shrinkOne'
                (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
                  { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
                h)
              0
          else x)[i] =
        x[k]

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
this✝ : i + 1 < x.stop - x.start
this : x.start < x.stop
⊢ ∃ k hk,
    0 < k ∧
      (if h : x.start < x.stop then
            heapifyDown lt
              (Subarray.shrinkOne'
                (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
                  { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
                h)
              0
          else x)[i] =
        x[k]
Tactic:
simp only [dif_pos this]
State after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
this✝ : i + 1 < x.stop - x.start
this : x.start < x.stop
⊢ ∃ k hk,
    0 < k ∧
      (heapifyDown lt
            (Subarray.shrinkOne'
              (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
                { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
              this)
            0)[i] =
        x[k]

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
this✝ : i + 1 < x.stop - x.start
this : x.start < x.stop
⊢ ∃ k hk,
    0 < k ∧
      (heapifyDown lt
            (Subarray.shrinkOne'
              (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
                { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
              this)
            0)[i] =
        x[k]
Tactic:
have hzero : 0 < x.size := Nat.sub_pos_of_lt this
State after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
this✝ : i + 1 < x.stop - x.start
this : x.start < x.stop
hzero : 0 < Subarray.size x
⊢ ∃ k hk,
    0 < k ∧
      (heapifyDown lt
            (Subarray.shrinkOne'
              (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
                { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
              this)
            0)[i] =
        x[k]

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
this✝ : i + 1 < x.stop - x.start
this : x.start < x.stop
hzero : 0 < Subarray.size x
⊢ ∃ k hk,
    0 < k ∧
      (heapifyDown lt
            (Subarray.shrinkOne'
              (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
                { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
              this)
            0)[i] =
        x[k]
Tactic:
have hlast : x.size-1 < x.size := Nat.pred_lt' <| Nat.add_lt_of_lt_sub hi
State after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
this✝ : i + 1 < x.stop - x.start
this : x.start < x.stop
hzero : 0 < Subarray.size x
hlast : Subarray.size x - 1 < Subarray.size x
⊢ ∃ k hk,
    0 < k ∧
      (heapifyDown lt
            (Subarray.shrinkOne'
              (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
                { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
              this)
            0)[i] =
        x[k]

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
this✝ : i + 1 < x.stop - x.start
this : x.start < x.stop
hzero : 0 < Subarray.size x
hlast : Subarray.size x - 1 < Subarray.size x
⊢ ∃ k hk,
    0 < k ∧
      (heapifyDown lt
            (Subarray.shrinkOne'
              (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
                { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
              this)
            0)[i] =
        x[k]
Tactic:
have ⟨k,hk,h⟩ :=
  exists_get_heapifyDown lt ((x.swap ⟨0,hzero⟩ ⟨x.size-1,hlast⟩).shrinkOne' this) 0 i <| by
    simp only [Subarray.size_shrinkOne', Subarray.size_swap]
    exact hi
State after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
this✝ : i + 1 < x.stop - x.start
this : x.start < x.stop
hzero : 0 < Subarray.size x
hlast : Subarray.size x - 1 < Subarray.size x
k : Nat
hk :
  k <
    Subarray.size
      (Subarray.shrinkOne' (Subarray.swap x { val := 0, isLt := hzero } { val := Subarray.size x - 1, isLt := hlast })
        this)
h :
  (heapifyDown lt
        (Subarray.shrinkOne' (Subarray.swap x { val := 0, isLt := hzero } { val := Subarray.size x - 1, isLt := hlast })
          this)
        0)[i] =
    (Subarray.shrinkOne' (Subarray.swap x { val := 0, isLt := hzero } { val := Subarray.size x - 1, isLt := hlast })
        this)[k]
⊢ ∃ k hk,
    0 < k ∧
      (heapifyDown lt
            (Subarray.shrinkOne'
              (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
                { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
              this)
            0)[i] =
        x[k]

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
this✝ : i + 1 < x.stop - x.start
this : x.start < x.stop
hzero : 0 < Subarray.size x
hlast : Subarray.size x - 1 < Subarray.size x
k : Nat
hk :
  k <
    Subarray.size
      (Subarray.shrinkOne' (Subarray.swap x { val := 0, isLt := hzero } { val := Subarray.size x - 1, isLt := hlast })
        this)
h :
  (heapifyDown lt
        (Subarray.shrinkOne' (Subarray.swap x { val := 0, isLt := hzero } { val := Subarray.size x - 1, isLt := hlast })
          this)
        0)[i] =
    (Subarray.shrinkOne' (Subarray.swap x { val := 0, isLt := hzero } { val := Subarray.size x - 1, isLt := hlast })
        this)[k]
⊢ ∃ k hk,
    0 < k ∧
      (heapifyDown lt
            (Subarray.shrinkOne'
              (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
                { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
              this)
            0)[i] =
        x[k]
Tactic:
simp only [h, Subarray.getElem_shrinkOne', Subarray.getElem_swap]
State after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
this✝ : i + 1 < x.stop - x.start
this : x.start < x.stop
hzero : 0 < Subarray.size x
hlast : Subarray.size x - 1 < Subarray.size x
k : Nat
hk :
  k <
    Subarray.size
      (Subarray.shrinkOne' (Subarray.swap x { val := 0, isLt := hzero } { val := Subarray.size x - 1, isLt := hlast })
        this)
h :
  (heapifyDown lt
        (Subarray.shrinkOne' (Subarray.swap x { val := 0, isLt := hzero } { val := Subarray.size x - 1, isLt := hlast })
          this)
        0)[i] =
    (Subarray.shrinkOne' (Subarray.swap x { val := 0, isLt := hzero } { val := Subarray.size x - 1, isLt := hlast })
        this)[k]
⊢ ∃ k_1 hk_1,
    0 < k_1 ∧ (if Subarray.size x - 1 = k then x[0] else if 0 = k then x[Subarray.size x - 1] else x[k]) = x[k_1]

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
this✝ : i + 1 < x.stop - x.start
this : x.start < x.stop
hzero : 0 < Subarray.size x
hlast : Subarray.size x - 1 < Subarray.size x
k : Nat
hk :
  k <
    Subarray.size
      (Subarray.shrinkOne' (Subarray.swap x { val := 0, isLt := hzero } { val := Subarray.size x - 1, isLt := hlast })
        this)
h :
  (heapifyDown lt
        (Subarray.shrinkOne' (Subarray.swap x { val := 0, isLt := hzero } { val := Subarray.size x - 1, isLt := hlast })
          this)
        0)[i] =
    (Subarray.shrinkOne' (Subarray.swap x { val := 0, isLt := hzero } { val := Subarray.size x - 1, isLt := hlast })
        this)[k]
⊢ ∃ k_1 hk_1,
    0 < k_1 ∧ (if Subarray.size x - 1 = k then x[0] else if 0 = k then x[Subarray.size x - 1] else x[k]) = x[k_1]
Tactic:
clear h
State after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
this✝ : i + 1 < x.stop - x.start
this : x.start < x.stop
hzero : 0 < Subarray.size x
hlast : Subarray.size x - 1 < Subarray.size x
k : Nat
hk :
  k <
    Subarray.size
      (Subarray.shrinkOne' (Subarray.swap x { val := 0, isLt := hzero } { val := Subarray.size x - 1, isLt := hlast })
        this)
⊢ ∃ k_1 hk_1,
    0 < k_1 ∧ (if Subarray.size x - 1 = k then x[0] else if 0 = k then x[Subarray.size x - 1] else x[k]) = x[k_1]

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
this✝ : i + 1 < x.stop - x.start
this : x.start < x.stop
hzero : 0 < Subarray.size x
hlast : Subarray.size x - 1 < Subarray.size x
k : Nat
hk :
  k <
    Subarray.size
      (Subarray.shrinkOne' (Subarray.swap x { val := 0, isLt := hzero } { val := Subarray.size x - 1, isLt := hlast })
        this)
⊢ ∃ k_1 hk_1,
    0 < k_1 ∧ (if Subarray.size x - 1 = k then x[0] else if 0 = k then x[Subarray.size x - 1] else x[k]) = x[k_1]
Tactic:
conv at hk => simp only [Subarray.size_shrinkOne', Subarray.size_swap]
State after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
this✝ : i + 1 < x.stop - x.start
this : x.start < x.stop
hzero : 0 < Subarray.size x
hlast : Subarray.size x - 1 < Subarray.size x
k : Nat
hk✝ :
  k <
    Subarray.size
      (Subarray.shrinkOne' (Subarray.swap x { val := 0, isLt := hzero } { val := Subarray.size x - 1, isLt := hlast })
        this)
hk : k < Subarray.size x - 1
⊢ ∃ k_1 hk,
    0 < k_1 ∧ (if Subarray.size x - 1 = k then x[0] else if 0 = k then x[Subarray.size x - 1] else x[k]) = x[k_1]

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
this✝ : i + 1 < x.stop - x.start
this : x.start < x.stop
hzero : 0 < Subarray.size x
hlast : Subarray.size x - 1 < Subarray.size x
k : Nat
hk✝ :
  k <
    Subarray.size
      (Subarray.shrinkOne' (Subarray.swap x { val := 0, isLt := hzero } { val := Subarray.size x - 1, isLt := hlast })
        this)
hk : k < Subarray.size x - 1
⊢ ∃ k_1 hk,
    0 < k_1 ∧ (if Subarray.size x - 1 = k then x[0] else if 0 = k then x[Subarray.size x - 1] else x[k]) = x[k_1]
Tactic:
simp only [if_neg (Nat.ne_of_gt hk)]
State after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
this✝ : i + 1 < x.stop - x.start
this : x.start < x.stop
hzero : 0 < Subarray.size x
hlast : Subarray.size x - 1 < Subarray.size x
k : Nat
hk✝ :
  k <
    Subarray.size
      (Subarray.shrinkOne' (Subarray.swap x { val := 0, isLt := hzero } { val := Subarray.size x - 1, isLt := hlast })
        this)
hk : k < Subarray.size x - 1
⊢ ∃ k_1 hk, 0 < k_1 ∧ (if 0 = k then x[Subarray.size x - 1] else x[k]) = x[k_1]

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
this✝ : i + 1 < x.stop - x.start
this : x.start < x.stop
hzero : 0 < Subarray.size x
hlast : Subarray.size x - 1 < Subarray.size x
k : Nat
hk✝ :
  k <
    Subarray.size
      (Subarray.shrinkOne' (Subarray.swap x { val := 0, isLt := hzero } { val := Subarray.size x - 1, isLt := hlast })
        this)
hk : k < Subarray.size x - 1
⊢ ∃ k_1 hk, 0 < k_1 ∧ (if 0 = k then x[Subarray.size x - 1] else x[k]) = x[k_1]
Tactic:
if hzk : 0 = k then
  simp only [if_pos hzk]
  exists x.size-1, hlast
  exact ⟨Nat.lt_of_le_of_lt k.zero_le hk, rfl⟩
else
  simp only [if_neg hzk]
  exists k, (Nat.lt_of_lt_of_le hk x.size.pred_le)
  exact ⟨Nat.pos_of_ne_zero (Ne.symm hzk), rfl⟩
State after:
no goals

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
this✝ : i + 1 < x.stop - x.start
this : x.start < x.stop
hzero : 0 < Subarray.size x
hlast : Subarray.size x - 1 < Subarray.size x
⊢ i <
    Subarray.size
      (Subarray.shrinkOne' (Subarray.swap x { val := 0, isLt := hzero } { val := Subarray.size x - 1, isLt := hlast })
        this)
Tactic:
simp only [Subarray.size_shrinkOne', Subarray.size_swap]
State after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
this✝ : i + 1 < x.stop - x.start
this : x.start < x.stop
hzero : 0 < Subarray.size x
hlast : Subarray.size x - 1 < Subarray.size x
⊢ i < Subarray.size x - 1

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
this✝ : i + 1 < x.stop - x.start
this : x.start < x.stop
hzero : 0 < Subarray.size x
hlast : Subarray.size x - 1 < Subarray.size x
⊢ i < Subarray.size x - 1
Tactic:
exact hi
State after:
no goals

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
this✝ : i + 1 < x.stop - x.start
this : x.start < x.stop
hzero : 0 < Subarray.size x
hlast : Subarray.size x - 1 < Subarray.size x
k : Nat
hk✝ :
  k <
    Subarray.size
      (Subarray.shrinkOne' (Subarray.swap x { val := 0, isLt := hzero } { val := Subarray.size x - 1, isLt := hlast })
        this)
hk : k < Subarray.size x - 1
hzk : 0 = k
⊢ ∃ k_1 hk, 0 < k_1 ∧ (if 0 = k then x[Subarray.size x - 1] else x[k]) = x[k_1]
Tactic:
simp only [if_pos hzk]
State after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
this✝ : i + 1 < x.stop - x.start
this : x.start < x.stop
hzero : 0 < Subarray.size x
hlast : Subarray.size x - 1 < Subarray.size x
k : Nat
hk✝ :
  k <
    Subarray.size
      (Subarray.shrinkOne' (Subarray.swap x { val := 0, isLt := hzero } { val := Subarray.size x - 1, isLt := hlast })
        this)
hk : k < Subarray.size x - 1
hzk : 0 = k
⊢ ∃ k hk, 0 < k ∧ x[Subarray.size x - 1] = x[k]

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
this✝ : i + 1 < x.stop - x.start
this : x.start < x.stop
hzero : 0 < Subarray.size x
hlast : Subarray.size x - 1 < Subarray.size x
k : Nat
hk✝ :
  k <
    Subarray.size
      (Subarray.shrinkOne' (Subarray.swap x { val := 0, isLt := hzero } { val := Subarray.size x - 1, isLt := hlast })
        this)
hk : k < Subarray.size x - 1
hzk : 0 = k
⊢ ∃ k hk, 0 < k ∧ x[Subarray.size x - 1] = x[k]
Tactic:
exists x.size-1, hlast
State after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
this✝ : i + 1 < x.stop - x.start
this : x.start < x.stop
hzero : 0 < Subarray.size x
hlast : Subarray.size x - 1 < Subarray.size x
k : Nat
hk✝ :
  k <
    Subarray.size
      (Subarray.shrinkOne' (Subarray.swap x { val := 0, isLt := hzero } { val := Subarray.size x - 1, isLt := hlast })
        this)
hk : k < Subarray.size x - 1
hzk : 0 = k
⊢ 0 < Subarray.size x - 1 ∧ x[Subarray.size x - 1] = x[Subarray.size x - 1]

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
this✝ : i + 1 < x.stop - x.start
this : x.start < x.stop
hzero : 0 < Subarray.size x
hlast : Subarray.size x - 1 < Subarray.size x
k : Nat
hk✝ :
  k <
    Subarray.size
      (Subarray.shrinkOne' (Subarray.swap x { val := 0, isLt := hzero } { val := Subarray.size x - 1, isLt := hlast })
        this)
hk : k < Subarray.size x - 1
hzk : 0 = k
⊢ 0 < Subarray.size x - 1 ∧ x[Subarray.size x - 1] = x[Subarray.size x - 1]
Tactic:
exact ⟨Nat.lt_of_le_of_lt k.zero_le hk, rfl⟩
State after:
no goals

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
this✝ : i + 1 < x.stop - x.start
this : x.start < x.stop
hzero : 0 < Subarray.size x
hlast : Subarray.size x - 1 < Subarray.size x
k : Nat
hk✝ :
  k <
    Subarray.size
      (Subarray.shrinkOne' (Subarray.swap x { val := 0, isLt := hzero } { val := Subarray.size x - 1, isLt := hlast })
        this)
hk : k < Subarray.size x - 1
hzk : ¬0 = k
⊢ ∃ k_1 hk, 0 < k_1 ∧ (if 0 = k then x[Subarray.size x - 1] else x[k]) = x[k_1]
Tactic:
simp only [if_neg hzk]
State after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
this✝ : i + 1 < x.stop - x.start
this : x.start < x.stop
hzero : 0 < Subarray.size x
hlast : Subarray.size x - 1 < Subarray.size x
k : Nat
hk✝ :
  k <
    Subarray.size
      (Subarray.shrinkOne' (Subarray.swap x { val := 0, isLt := hzero } { val := Subarray.size x - 1, isLt := hlast })
        this)
hk : k < Subarray.size x - 1
hzk : ¬0 = k
⊢ ∃ k_1 hk, 0 < k_1 ∧ x[k] = x[k_1]

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
this✝ : i + 1 < x.stop - x.start
this : x.start < x.stop
hzero : 0 < Subarray.size x
hlast : Subarray.size x - 1 < Subarray.size x
k : Nat
hk✝ :
  k <
    Subarray.size
      (Subarray.shrinkOne' (Subarray.swap x { val := 0, isLt := hzero } { val := Subarray.size x - 1, isLt := hlast })
        this)
hk : k < Subarray.size x - 1
hzk : ¬0 = k
⊢ ∃ k_1 hk, 0 < k_1 ∧ x[k] = x[k_1]
Tactic:
exists k, (Nat.lt_of_lt_of_le hk x.size.pred_le)
State after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
this✝ : i + 1 < x.stop - x.start
this : x.start < x.stop
hzero : 0 < Subarray.size x
hlast : Subarray.size x - 1 < Subarray.size x
k : Nat
hk✝ :
  k <
    Subarray.size
      (Subarray.shrinkOne' (Subarray.swap x { val := 0, isLt := hzero } { val := Subarray.size x - 1, isLt := hlast })
        this)
hk : k < Subarray.size x - 1
hzk : ¬0 = k
⊢ 0 < k ∧ x[k] = x[k]

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
this✝ : i + 1 < x.stop - x.start
this : x.start < x.stop
hzero : 0 < Subarray.size x
hlast : Subarray.size x - 1 < Subarray.size x
k : Nat
hk✝ :
  k <
    Subarray.size
      (Subarray.shrinkOne' (Subarray.swap x { val := 0, isLt := hzero } { val := Subarray.size x - 1, isLt := hlast })
        this)
hk : k < Subarray.size x - 1
hzk : ¬0 = k
⊢ 0 < k ∧ x[k] = x[k]
Tactic:
exact ⟨Nat.pos_of_ne_zero (Ne.symm hzk), rfl⟩
State after:
no goals