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

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

State before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
hstop : stop ≤ n
i : Nat
x✝ : findIdx.loop x p stop hstop i < n
h :
  (if hi : i < stop then
      let_fun this := (_ : i < n);
      bif p x[i] then i else findIdx.loop x p stop hstop (i + 1)
    else stop) <
    stop
⊢ p
      x[if hi : i < stop then
          let_fun this := (_ : i < n);
          bif p x[i] then i else findIdx.loop x p stop hstop (i + 1)
        else stop] =
    true
Tactic:
if hi : i < stop then
  rewrite [dif_pos hi] at h
  rewrite [getElem_eq rfl (dif_pos hi)]
  dsimp at *
  if hp : p (x[i]'(trans (r:=LT.lt) (s:=LE.le) hi hstop)) = true then
    rewrite [getElem_eq rfl (by rw [hp, cond_true])]
    exact hp
  else
    have hp := Bool.eq_false_iff.mpr hp
    rewrite [getElem_eq rfl (by rw [hp, cond_false])]
    rewrite [hp, cond_false] at h
    exact get_findIdx_loop x p stop hstop (i+1) h
else
  rewrite [dif_neg hi] at h
  exact absurd h stop.lt_irrefl
State after:
no goals

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

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

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

State before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
hstop : stop ≤ n
i : Nat
x✝ : findIdx.loop x p stop hstop i < n
hi : i < stop
h : (bif p x[i] then i else findIdx.loop x p stop hstop (i + 1)) < stop
⊢ p x[bif p x[i] then i else findIdx.loop x p stop hstop (i + 1)] = true
Tactic:
if hp : p (x[i]'(trans (r:=LT.lt) (s:=LE.le) hi hstop)) = true then
  rewrite [getElem_eq rfl (by rw [hp, cond_true])]
  exact hp
else
  have hp := Bool.eq_false_iff.mpr hp
  rewrite [getElem_eq rfl (by rw [hp, cond_false])]
  rewrite [hp, cond_false] at h
  exact get_findIdx_loop x p stop hstop (i+1) h
State after:
no goals

State before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
hstop : stop ≤ n
i : Nat
x✝ : findIdx.loop x p stop hstop i < n
hi : i < stop
h : (bif p x[i] then i else findIdx.loop x p stop hstop (i + 1)) < stop
hp : p x[i] = true
⊢ p x[bif p x[i] then i else findIdx.loop x p stop hstop (i + 1)] = true
Tactic:
rewrite [getElem_eq rfl (by rw [hp, cond_true])]
State after:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
hstop : stop ≤ n
i : Nat
x✝ : findIdx.loop x p stop hstop i < n
hi : i < stop
h : (bif p x[i] then i else findIdx.loop x p stop hstop (i + 1)) < stop
hp : p x[i] = true
⊢ p x[i] = true

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

State before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
hstop : stop ≤ n
i : Nat
x✝ : findIdx.loop x p stop hstop i < n
hi : i < stop
h : (bif p x[i] then i else findIdx.loop x p stop hstop (i + 1)) < stop
hp : p x[i] = true
⊢ (bif p x[i] then i else findIdx.loop x p stop hstop (i + 1)) = ?m.160149
Tactic:
rw [hp, cond_true]
State after:
no goals

State before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
hstop : stop ≤ n
i : Nat
x✝ : findIdx.loop x p stop hstop i < n
hi : i < stop
h : (bif p x[i] then i else findIdx.loop x p stop hstop (i + 1)) < stop
hp : ¬p x[i] = true
⊢ p x[bif p x[i] then i else findIdx.loop x p stop hstop (i + 1)] = true
Tactic:
have hp := Bool.eq_false_iff.mpr hp
State after:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
hstop : stop ≤ n
i : Nat
x✝ : findIdx.loop x p stop hstop i < n
hi : i < stop
h : (bif p x[i] then i else findIdx.loop x p stop hstop (i + 1)) < stop
hp✝ : ¬p x[i] = true
hp : p x[i] = false
⊢ p x[bif p x[i] then i else findIdx.loop x p stop hstop (i + 1)] = true

State before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
hstop : stop ≤ n
i : Nat
x✝ : findIdx.loop x p stop hstop i < n
hi : i < stop
h : (bif p x[i] then i else findIdx.loop x p stop hstop (i + 1)) < stop
hp✝ : ¬p x[i] = true
hp : p x[i] = false
⊢ p x[bif p x[i] then i else findIdx.loop x p stop hstop (i + 1)] = true
Tactic:
rewrite [getElem_eq rfl (by rw [hp, cond_false])]
State after:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
hstop : stop ≤ n
i : Nat
x✝ : findIdx.loop x p stop hstop i < n
hi : i < stop
h : (bif p x[i] then i else findIdx.loop x p stop hstop (i + 1)) < stop
hp✝ : ¬p x[i] = true
hp : p x[i] = false
⊢ p x[findIdx.loop x p stop hstop (i + 1)] = true

State before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
hstop : stop ≤ n
i : Nat
x✝ : findIdx.loop x p stop hstop i < n
hi : i < stop
h : (bif p x[i] then i else findIdx.loop x p stop hstop (i + 1)) < stop
hp✝ : ¬p x[i] = true
hp : p x[i] = false
⊢ p x[findIdx.loop x p stop hstop (i + 1)] = true
Tactic:
rewrite [hp, cond_false] at h
State after:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
hstop : stop ≤ n
i : Nat
x✝ : findIdx.loop x p stop hstop i < n
hi : i < stop
h : findIdx.loop x p stop hstop (i + 1) < stop
hp✝ : ¬p x[i] = true
hp : p x[i] = false
⊢ p x[findIdx.loop x p stop hstop (i + 1)] = true

State before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
hstop : stop ≤ n
i : Nat
x✝ : findIdx.loop x p stop hstop i < n
hi : i < stop
h : findIdx.loop x p stop hstop (i + 1) < stop
hp✝ : ¬p x[i] = true
hp : p x[i] = false
⊢ p x[findIdx.loop x p stop hstop (i + 1)] = true
Tactic:
exact get_findIdx_loop x p stop hstop (i+1) h
State after:
no goals

State before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
hstop : stop ≤ n
i : Nat
x✝ : findIdx.loop x p stop hstop i < n
hi : i < stop
h : (bif p x[i] then i else findIdx.loop x p stop hstop (i + 1)) < stop
hp✝ : ¬p x[i] = true
hp : p x[i] = false
⊢ (bif p x[i] then i else findIdx.loop x p stop hstop (i + 1)) = ?m.160313
Tactic:
rw [hp, cond_false]
State after:
no goals

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

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