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

State before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i : Nat
⊢ findIdx.loop x p stop h i ≤ stop
Tactic:
unfold findIdx.loop
State after:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i : Nat
⊢ (if hi : i < stop then
      let_fun this := (_ : i < n);
      bif p x[i] then i else findIdx.loop x p stop h (i + 1)
    else stop) ≤
    stop

State before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i : Nat
⊢ (if hi : i < stop then
      let_fun this := (_ : i < n);
      bif p x[i] then i else findIdx.loop x p stop h (i + 1)
    else stop) ≤
    stop
Tactic:
if hi : i < stop then
  rewrite [dif_pos hi]; dsimp
  match p (x[i]'(trans (r:=LT.lt) (s:=LE.le) hi h)) with
  | true => exact Nat.le_of_lt hi
  | false => exact findIdx_loop_le x p stop h (i+1)
else
  rewrite [dif_neg hi]
  exact .refl
State after:
no goals

State before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i : Nat
hi : i < stop
⊢ (if hi : i < stop then
      let_fun this := (_ : i < n);
      bif p x[i] then i else findIdx.loop x p stop h (i + 1)
    else stop) ≤
    stop
Tactic:
rewrite [dif_pos hi]
State after:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i : Nat
hi : i < stop
⊢ (let_fun this := (_ : i < n);
    bif p x[i] then i else findIdx.loop x p stop h (i + 1)) ≤
    stop

State before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i : Nat
hi : i < stop
⊢ (let_fun this := (_ : i < n);
    bif p x[i] then i else findIdx.loop x p stop h (i + 1)) ≤
    stop
Tactic:
dsimp
State after:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i : Nat
hi : i < stop
⊢ (bif p x[i] then i else findIdx.loop x p stop h (i + 1)) ≤ stop

State before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i : Nat
hi : i < stop
⊢ (bif p x[i] then i else findIdx.loop x p stop h (i + 1)) ≤ stop
Tactic:
match p (x[i]'(trans (r:=LT.lt) (s:=LE.le) hi h)) with
| true => exact Nat.le_of_lt hi
| false => exact findIdx_loop_le x p stop h (i+1)
State after:
no goals

State before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i : Nat
hi : i < stop
⊢ (bif true then i else findIdx.loop x p stop h (i + 1)) ≤ stop
Tactic:
exact Nat.le_of_lt hi
State after:
no goals

State before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i : Nat
hi : i < stop
⊢ (bif false then i else findIdx.loop x p stop h (i + 1)) ≤ stop
Tactic:
exact findIdx_loop_le x p stop h (i+1)
State after:
no goals

State before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i : Nat
hi : ¬i < stop
⊢ (if hi : i < stop then
      let_fun this := (_ : i < n);
      bif p x[i] then i else findIdx.loop x p stop h (i + 1)
    else stop) ≤
    stop
Tactic:
rewrite [dif_neg hi]
State after:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i : Nat
hi : ¬i < stop
⊢ stop ≤ stop

State before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i : Nat
hi : ¬i < stop
⊢ stop ≤ stop
Tactic:
exact .refl
State after:
no goals