Theorem: Algdata.BinaryHeap.heapSort.loop.OpSpec.get_eq_of_lt_start (Algdata/Data/BinaryHeap/Basic.lean)

State before:
α : Type u
lt : α → α → Bool
x : Subarray α
n : Nat
y : Array α
h : loop.OpSpec lt x n y
i : Nat
hi : i < Array.size y
hlt : i < x.start
⊢ y[i] = x.as[i]
Tactic:
induction h with
| zero => rfl
| @succ x n y h IH =>
  specialize @IH hi <| start_popMax lt x ▸ hlt
  exact Eq.trans IH <| get_as_popMax_of_lt_start lt x i hlt
State after:
no goals

State before:
case zero
α : Type u
lt : α → α → Bool
x : Subarray α
n : Nat
y : Array α
i : Nat
x✝ : Subarray α
hi : i < Array.size x✝.as
hlt : i < x✝.start
⊢ x✝.as[i] = x✝.as[i]
Tactic:
rfl
State after:
no goals

State before:
case succ
α : Type u
lt : α → α → Bool
x✝ : Subarray α
n✝ : Nat
y✝ : Array α
i : Nat
x : Subarray α
n : Nat
y : Array α
h : loop.OpSpec lt (popMax lt x) n y
IH : ∀ {hi : i < Array.size y}, i < (popMax lt x).start → y[i] = (popMax lt x).as[i]
hi : i < Array.size y
hlt : i < x.start
⊢ y[i] = x.as[i]
Tactic:
specialize @IH hi <| start_popMax lt x ▸ hlt
State after:
case succ
α : Type u
lt : α → α → Bool
x✝ : Subarray α
n✝ : Nat
y✝ : Array α
i : Nat
x : Subarray α
n : Nat
y : Array α
h : loop.OpSpec lt (popMax lt x) n y
hi : i < Array.size y
hlt : i < x.start
IH : y[i] = (popMax lt x).as[i]
⊢ y[i] = x.as[i]

State before:
case succ
α : Type u
lt : α → α → Bool
x✝ : Subarray α
n✝ : Nat
y✝ : Array α
i : Nat
x : Subarray α
n : Nat
y : Array α
h : loop.OpSpec lt (popMax lt x) n y
hi : i < Array.size y
hlt : i < x.start
IH : y[i] = (popMax lt x).as[i]
⊢ y[i] = x.as[i]
Tactic:
exact Eq.trans IH <| get_as_popMax_of_lt_start lt x i hlt
State after:
no goals