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

State before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
i : Nat
hi : i < n
hp : p x[i] = true
⊢ findIdx x p 0 n ≤ i
Tactic:
apply Nat.le_of_not_lt
State after:
case a
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
i : Nat
hi : i < n
hp : p x[i] = true
⊢ ¬i < findIdx x p 0 n

State before:
case a
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
i : Nat
hi : i < n
hp : p x[i] = true
⊢ ¬i < findIdx x p 0 n
Tactic:
intro h
State after:
case a
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
i : Nat
hi : i < n
hp : p x[i] = true
h : i < findIdx x p 0 n
⊢ False

State before:
case a
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
i : Nat
hi : i < n
hp : p x[i] = true
h : i < findIdx x p 0 n
⊢ False
Tactic:
have : p x[i] = false := get_findIdx_of_lt x p i i.zero_le h
State after:
case a
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
i : Nat
hi : i < n
hp : p x[i] = true
h : i < findIdx x p 0 n
this : p x[i] = false
⊢ False

State before:
case a
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
i : Nat
hi : i < n
hp : p x[i] = true
h : i < findIdx x p 0 n
this : p x[i] = false
⊢ False
Tactic:
rewrite [this] at hp
State after:
case a
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
i : Nat
hi : i < n
hp : false = true
h : i < findIdx x p 0 n
this : p x[i] = false
⊢ False

State before:
case a
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
i : Nat
hi : i < n
hp : false = true
h : i < findIdx x p 0 n
this : p x[i] = false
⊢ False
Tactic:
cases hp
State after:
no goals