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

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

State before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop : Nat
h : (if h : stop ≤ n then findIdx.loop x p stop h start else findIdx.loop x p n (_ : Nat.le n n) start) < stop
h' : autoParam (stop ≤ n) _auto✝
x✝ : findIdx x p start stop < n
⊢ p x[if h : stop ≤ n then findIdx.loop x p stop h start else findIdx.loop x p n (_ : Nat.le n n) start] = true
Tactic:
if hstop : stop ≤ n then
  rewrite [getElem_eq rfl (dif_pos hstop)]
  rewrite [dif_pos hstop] at h
  exact get_findIdx_loop x p stop h' start h
else
  rewrite [getElem_eq rfl (dif_neg hstop)]
  rewrite [dif_neg hstop] at h
  exact get_findIdx_loop x p n .refl start <|
    trans (r:=LT.lt) (s:=LE.le) h h'
State after:
no goals

State before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop : Nat
h : (if h : stop ≤ n then findIdx.loop x p stop h start else findIdx.loop x p n (_ : Nat.le n n) start) < stop
h' : autoParam (stop ≤ n) _auto✝
x✝ : findIdx x p start stop < n
hstop : stop ≤ n
⊢ p x[if h : stop ≤ n then findIdx.loop x p stop h start else findIdx.loop x p n (_ : Nat.le n n) start] = true
Tactic:
rewrite [getElem_eq rfl (dif_pos hstop)]
State after:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop : Nat
h : (if h : stop ≤ n then findIdx.loop x p stop h start else findIdx.loop x p n (_ : Nat.le n n) start) < stop
h' : autoParam (stop ≤ n) _auto✝
x✝ : findIdx x p start stop < n
hstop : stop ≤ n
⊢ p x[findIdx.loop x p stop hstop start] = true

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

State before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop : Nat
h' : autoParam (stop ≤ n) _auto✝
x✝ : findIdx x p start stop < n
hstop : stop ≤ n
h : findIdx.loop x p stop hstop start < stop
⊢ p x[findIdx.loop x p stop hstop start] = true
Tactic:
exact get_findIdx_loop x p stop h' start h
State after:
no goals

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

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

State before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop : Nat
h : findIdx.loop x p n (_ : Nat.le n n) start < stop
h' : autoParam (stop ≤ n) _auto✝
x✝ : findIdx x p start stop < n
hstop : ¬stop ≤ n
⊢ p x[findIdx.loop x p n (_ : Nat.le n n) start] = true
Tactic:
exact get_findIdx_loop x p n .refl start <|
  trans (r:=LT.lt) (s:=LE.le) h h'
State after:
no goals