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

State before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i : Nat
hi : i ≤ stop
⊢ findIdx.loop x p stop h i ≥ i
Tactic:
unfold findIdx.loop
State after:
α : 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) ≥
    i

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) ≥
    i
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.refl
  | false =>
    apply Nat.le_of_succ_le
    exact findIdx_loop_ge x p stop h (i+1) hi
else
  rewrite [dif_neg hi]; assumption
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
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) ≥
    i
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
hi : i < stop
⊢ (let_fun this := (_ : i < n);
    bif p x[i] then i else findIdx.loop x p stop h (i + 1)) ≥
    i

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

State before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i : Nat
hi✝ : i ≤ stop
hi : i < stop
⊢ (bif p x[i] then i else findIdx.loop x p stop h (i + 1)) ≥ i
Tactic:
match p (x[i]'(trans (r:=LT.lt) (s:=LE.le) hi h)) with
| true => exact Nat.le.refl
| false =>
  apply Nat.le_of_succ_le
  exact findIdx_loop_ge x p stop h (i+1) 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
hi : i < stop
⊢ (bif true then i else findIdx.loop x p stop h (i + 1)) ≥ i
Tactic:
exact Nat.le.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
hi : i < stop
⊢ (bif false then i else findIdx.loop x p stop h (i + 1)) ≥ i
Tactic:
apply Nat.le_of_succ_le
State after:
case h
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i : Nat
hi✝ : i ≤ stop
hi : i < stop
⊢ Nat.succ i ≤ bif false then i else findIdx.loop x p stop h (i + 1)

State before:
case h
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i : Nat
hi✝ : i ≤ stop
hi : i < stop
⊢ Nat.succ i ≤ bif false then i else findIdx.loop x p stop h (i + 1)
Tactic:
exact findIdx_loop_ge x p stop h (i+1) 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
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) ≥
    i
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
hi : ¬i < stop
⊢ stop ≥ i

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