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

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

State before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop k : Nat
hk : k ≥ start
hk' : k < if h : stop ≤ n then findIdx.loop x p stop h start else findIdx.loop x p n (_ : Nat.le n n) start
x✝ : k < n
⊢ p x[k] = false
Tactic:
if hstop : stop ≤ n then
  rewrite [dif_pos hstop] at hk'
  exact get_findIdx_loop_of_lt x p stop hstop start k hk hk'
else
  rewrite [dif_neg hstop] at hk'
  exact get_findIdx_loop_of_lt x p n .refl start k hk hk'
State after:
no goals

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

State before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop k : Nat
hk : k ≥ start
x✝ : k < n
hstop : stop ≤ n
hk' : k < findIdx.loop x p stop hstop start
⊢ p x[k] = false
Tactic:
exact get_findIdx_loop_of_lt x p stop hstop start k hk hk'
State after:
no goals

State before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop k : Nat
hk : k ≥ start
hk' : k < if h : stop ≤ n then findIdx.loop x p stop h start else findIdx.loop x p n (_ : Nat.le n n) start
x✝ : k < n
hstop : ¬stop ≤ n
⊢ p x[k] = false
Tactic:
rewrite [dif_neg hstop] at hk'
State after:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop k : Nat
hk : k ≥ start
hk' : k < findIdx.loop x p n (_ : Nat.le n n) start
x✝ : k < n
hstop : ¬stop ≤ n
⊢ p x[k] = false

State before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop k : Nat
hk : k ≥ start
hk' : k < findIdx.loop x p n (_ : Nat.le n n) start
x✝ : k < n
hstop : ¬stop ≤ n
⊢ p x[k] = false
Tactic:
exact get_findIdx_loop_of_lt x p n .refl start k hk hk'
State after:
no goals