Theorem: Algdata.BinaryHeap.heapSort.loop.OpSpec.get_eq_of_ge_stop (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
hge : i ≥ x.stop
⊢ y[i] = x.as[i]
Tactic:
induction h with
| zero => rfl
| @succ x n y h IH =>
  specialize @IH hi <| Nat.le_trans (stop_popMax_le_stop lt x) hge
  exact Eq.trans IH <| get_as_popMax_of_ge_stop lt x i hge
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
hge : i ≥ x✝.stop
⊢ 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).stop → y[i] = (popMax lt x).as[i]
hi : i < Array.size y
hge : i ≥ x.stop
⊢ y[i] = x.as[i]
Tactic:
specialize @IH hi <| Nat.le_trans (stop_popMax_le_stop lt x) hge
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
hge : i ≥ x.stop
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
hge : i ≥ x.stop
IH : y[i] = (popMax lt x).as[i]
⊢ y[i] = x.as[i]
Tactic:
exact Eq.trans IH <| get_as_popMax_of_ge_stop lt x i hge
State after:
no goals