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

State before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i k : Nat
hk : k ≥ i
hk' : k < findIdx.loop x p stop h i
x✝ : k < n
⊢ p x[k] = false
Tactic:
have hkstop : k < stop :=
  trans (r:=LT.lt) (s:=LE.le) hk' <| findIdx_loop_le x p stop h i
State after:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i k : Nat
hk : k ≥ i
hk' : k < findIdx.loop x p stop h i
x✝ : k < n
hkstop : k < stop
⊢ p x[k] = false

State before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i k : Nat
hk : k ≥ i
hk' : k < findIdx.loop x p stop h i
x✝ : k < n
hkstop : k < stop
⊢ p x[k] = false
Tactic:
have histop : i < stop := trans hk hkstop
State after:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i k : Nat
hk : k ≥ i
hk' : k < findIdx.loop x p stop h i
x✝ : k < n
hkstop : k < stop
histop : i < stop
⊢ p x[k] = false

State before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i k : Nat
hk : k ≥ i
hk' : k < findIdx.loop x p stop h i
x✝ : k < n
hkstop : k < stop
histop : i < stop
⊢ p x[k] = false
Tactic:
conv at hk' =>
  unfold findIdx.loop; rw [dif_pos histop]; dsimp
State after:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i k : Nat
hk : k ≥ i
x✝ : k < n
hkstop : k < stop
histop : i < stop
hk' : k < bif p x[i] then i else findIdx.loop x p stop h (i + 1)
⊢ p x[k] = false

State before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i k : Nat
hk : k ≥ i
x✝ : k < n
hkstop : k < stop
histop : i < stop
hk' : k < bif p x[i] then i else findIdx.loop x p stop h (i + 1)
⊢ p x[k] = false
Tactic:
match hpi : p (x[i]'(trans (r:=LT.lt) (s:=LE.le) histop h)) with
| true =>
  rewrite [hpi, cond_true] at hk'
  exact absurd hk' <| Nat.not_lt_of_le hk
| false =>
  rewrite [hpi, cond_false] at hk'
  cases Nat.eq_or_lt_of_le hk with
  | inl heq => exact heq ▸ hpi
  | inr hlt => exact get_findIdx_loop_of_lt x p stop h (i+1) k hlt hk'
State after:
no goals

State before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i k : Nat
hk : k ≥ i
x✝ : k < n
hkstop : k < stop
histop : i < stop
hk' : k < bif p x[i] then i else findIdx.loop x p stop h (i + 1)
hpi : p x[i] = true
⊢ p x[k] = false
Tactic:
rewrite [hpi, cond_true] at hk'
State after:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i k : Nat
hk : k ≥ i
x✝ : k < n
hkstop : k < stop
histop : i < stop
hk' : k < i
hpi : p x[i] = true
⊢ p x[k] = false

State before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i k : Nat
hk : k ≥ i
x✝ : k < n
hkstop : k < stop
histop : i < stop
hk' : k < i
hpi : p x[i] = true
⊢ p x[k] = false
Tactic:
exact absurd hk' <| Nat.not_lt_of_le hk
State after:
no goals

State before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i k : Nat
hk : k ≥ i
x✝ : k < n
hkstop : k < stop
histop : i < stop
hk' : k < bif p x[i] then i else findIdx.loop x p stop h (i + 1)
hpi : p x[i] = false
⊢ p x[k] = false
Tactic:
rewrite [hpi, cond_false] at hk'
State after:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i k : Nat
hk : k ≥ i
x✝ : k < n
hkstop : k < stop
histop : i < stop
hk' : k < findIdx.loop x p stop h (i + 1)
hpi : p x[i] = false
⊢ p x[k] = false

State before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i k : Nat
hk : k ≥ i
x✝ : k < n
hkstop : k < stop
histop : i < stop
hk' : k < findIdx.loop x p stop h (i + 1)
hpi : p x[i] = false
⊢ p x[k] = false
Tactic:
cases Nat.eq_or_lt_of_le hk with
| inl heq => exact heq ▸ hpi
| inr hlt => exact get_findIdx_loop_of_lt x p stop h (i+1) k hlt hk'
State after:
no goals

State before:
case inl
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i k : Nat
hk : k ≥ i
x✝ : k < n
hkstop : k < stop
histop : i < stop
hk' : k < findIdx.loop x p stop h (i + 1)
hpi : p x[i] = false
heq : i = k
⊢ p x[k] = false
Tactic:
exact heq ▸ hpi
State after:
no goals

State before:
case inr
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i k : Nat
hk : k ≥ i
x✝ : k < n
hkstop : k < stop
histop : i < stop
hk' : k < findIdx.loop x p stop h (i + 1)
hpi : p x[i] = false
hlt : i < k
⊢ p x[k] = false
Tactic:
exact get_findIdx_loop_of_lt x p stop h (i+1) k hlt hk'
State after:
no goals