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

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

State before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop : Nat
⊢ (if h : stop ≤ n then findIdx.loop x p stop h start else findIdx.loop x p n (_ : Nat.le n n) start) ≤ n
Tactic:
if h : stop ≤ n then
  rewrite [dif_pos h]
  refine trans (r:=LE.le) ?_ h
  exact findIdx_loop_le x p stop h start
else
  rewrite [dif_neg h]
  exact findIdx_loop_le x p n .refl start
State after:
no goals

State before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop : Nat
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) ≤ n
Tactic:
rewrite [dif_pos h]
State after:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop : Nat
h : stop ≤ n
⊢ findIdx.loop x p stop h start ≤ n

State before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop : Nat
h : stop ≤ n
⊢ findIdx.loop x p stop h start ≤ n
Tactic:
refine trans (r:=LE.le) ?_ h
State after:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop : Nat
h : stop ≤ n
⊢ findIdx.loop x p stop h start ≤ stop

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

State before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop : Nat
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) ≤ n
Tactic:
rewrite [dif_neg h]
State after:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop : Nat
h : ¬stop ≤ n
⊢ findIdx.loop x p n (_ : Nat.le n n) start ≤ n

State before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop : Nat
h : ¬stop ≤ n
⊢ findIdx.loop x p n (_ : Nat.le n n) start ≤ n
Tactic:
exact findIdx_loop_le x p n .refl start
State after:
no goals