Theorem: SizedArray.findIdx_ge (Algdata/Data/Array/Sized.lean)

State before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop : Nat
h : start ≤ stop
h' : stop ≤ n
⊢ findIdx x p start stop ≥ start
Tactic:
dsimp [findIdx]
State after:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop : Nat
h : start ≤ stop
h' : stop ≤ n
⊢ (if h : stop ≤ n then findIdx.loop x p stop h start else findIdx.loop x p n (_ : Nat.le n n) start) ≥ start

State before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop : Nat
h : start ≤ stop
h' : stop ≤ n
⊢ (if h : stop ≤ n then findIdx.loop x p stop h start else findIdx.loop x p n (_ : Nat.le n n) start) ≥ start
Tactic:
rewrite [dif_pos h']
State after:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop : Nat
h : start ≤ stop
h' : stop ≤ n
⊢ findIdx.loop x p stop h' start ≥ start

State before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop : Nat
h : start ≤ stop
h' : stop ≤ n
⊢ findIdx.loop x p stop h' start ≥ start
Tactic:
exact findIdx_loop_ge x p stop h' start h
State after:
no goals