-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem any_iff_exists {p : α → Bool} {as : Array α} {start stop} :
    as.any p start stop ↔ ∃ (i : Nat) (_ : i < as.size), start ≤ i ∧ i < stop ∧ p as[i]

Proof state:
α : Type u_1
p : α → Bool
as : Array α
start stop : Nat
⊢ as.any p start stop = true ↔ ∃ i x, start ≤ i ∧ i < stop ∧ p as[i] = true

Tactic:
dsimp [any, anyM, Id.run]

Result:
α : Type u_1
p : α → Bool
as : Array α
start stop : Nat
⊢ (if h : stop ≤ as.size then anyM.loop p as stop h start else anyM.loop p as as.size ⋯ start) = true ↔
    ∃ i x, start ≤ i ∧ i < stop ∧ p as[i] = true

Proof state:
α : Type u_1
p : α → Bool
as : Array α
start stop : Nat
h✝ : ¬stop ≤ as.size
i : Nat
hi : i < as.size
ge : start ≤ i
left✝ : i < stop
h : p as[i] = true
⊢ i < as.size

Tactic:
omega

Result:
no goals

Proof state:
case isFalse.mpr.intro.intro.intro.intro
α : Type u_1
p : α → Bool
as : Array α
start stop : Nat
h✝ : ¬stop ≤ as.size
i : Nat
hi : i < as.size
ge : start ≤ i
left✝ : i < stop
h : p as[i] = true
⊢ ∃ i x, start ≤ i ∧ i < as.size ∧ p as[i] = true

Tactic:
exact ⟨i, by omega, by omega, by omega, h⟩

Result:
no goals

Proof state:
case isFalse.mpr
α : Type u_1
p : α → Bool
as : Array α
start stop : Nat
h✝ : ¬stop ≤ as.size
⊢ (∃ i x, start ≤ i ∧ i < stop ∧ p as[i] = true) → ∃ i x, start ≤ i ∧ i < as.size ∧ p as[i] = true

Tactic:
rintro ⟨i, hi, ge, _, h⟩

Result:
case isFalse.mpr.intro.intro.intro.intro
α : Type u_1
p : α → Bool
as : Array α
start stop : Nat
h✝ : ¬stop ≤ as.size
i : Nat
hi : i < as.size
ge : start ≤ i
left✝ : i < stop
h : p as[i] = true
⊢ ∃ i x, start ≤ i ∧ i < as.size ∧ p as[i] = true

Proof state:
case isFalse
α : Type u_1
p : α → Bool
as : Array α
start stop : Nat
h✝ : ¬stop ≤ as.size
⊢ anyM.loop p as as.size ⋯ start = true ↔ ∃ i x, start ≤ i ∧ i < stop ∧ p as[i] = true

Tactic:
rw [anyM_loop_iff_exists]

Result:
case isFalse
α : Type u_1
p : α → Bool
as : Array α
start stop : Nat
h✝ : ¬stop ≤ as.size
⊢ (∃ i x, start ≤ i ∧ i < as.size ∧ p as[i] = true) ↔ ∃ i x, start ≤ i ∧ i < stop ∧ p as[i] = true

Proof state:
case isFalse.mp.intro.intro.intro.intro
α : Type u_1
p : α → Bool
as : Array α
start stop : Nat
h✝ : ¬stop ≤ as.size
i : Nat
hi : i < as.size
ge : start ≤ i
left✝ : i < as.size
h : p as[i] = true
⊢ ∃ i x, start ≤ i ∧ i < stop ∧ p as[i] = true

Tactic:
exact ⟨i, by omega, by omega, by omega, h⟩

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
as : Array α
start stop : Nat
h✝ : ¬stop ≤ as.size
i : Nat
hi : i < as.size
ge : start ≤ i
left✝ : i < as.size
h : p as[i] = true
⊢ i < as.size

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
as : Array α
start stop : Nat
⊢ (if h : stop ≤ as.size then anyM.loop p as stop h start else anyM.loop p as as.size ⋯ start) = true ↔
    ∃ i x, start ≤ i ∧ i < stop ∧ p as[i] = true

Tactic:
split

Result:
case isTrue
α : Type u_1
p : α → Bool
as : Array α
start stop : Nat
h✝ : stop ≤ as.size
⊢ anyM.loop p as stop h✝ start = true ↔ ∃ i x, start ≤ i ∧ i < stop ∧ p as[i] = true

case isFalse
α : Type u_1
p : α → Bool
as : Array α
start stop : Nat
h✝ : ¬stop ≤ as.size
⊢ anyM.loop p as as.size ⋯ start = true ↔ ∃ i x, start ≤ i ∧ i < stop ∧ p as[i] = true

Proof state:
α : Type u_1
p : α → Bool
as : Array α
start stop : Nat
h✝ : ¬stop ≤ as.size
i : Nat
hi : i < as.size
ge : start ≤ i
left✝ : i < as.size
h : p as[i] = true
⊢ start ≤ i

Tactic:
omega

Result:
no goals

Proof state:
case isTrue
α : Type u_1
p : α → Bool
as : Array α
start stop : Nat
h✝ : stop ≤ as.size
⊢ anyM.loop p as stop h✝ start = true ↔ ∃ i x, start ≤ i ∧ i < stop ∧ p as[i] = true

Tactic:
rw [anyM_loop_iff_exists]

Result:
no goals

Proof state:
case isFalse
α : Type u_1
p : α → Bool
as : Array α
start stop : Nat
h✝ : ¬stop ≤ as.size
⊢ (∃ i x, start ≤ i ∧ i < as.size ∧ p as[i] = true) ↔ ∃ i x, start ≤ i ∧ i < stop ∧ p as[i] = true

Tactic:
constructor

Result:
case isFalse.mp
α : Type u_1
p : α → Bool
as : Array α
start stop : Nat
h✝ : ¬stop ≤ as.size
⊢ (∃ i x, start ≤ i ∧ i < as.size ∧ p as[i] = true) → ∃ i x, start ≤ i ∧ i < stop ∧ p as[i] = true

case isFalse.mpr
α : Type u_1
p : α → Bool
as : Array α
start stop : Nat
h✝ : ¬stop ≤ as.size
⊢ (∃ i x, start ≤ i ∧ i < stop ∧ p as[i] = true) → ∃ i x, start ≤ i ∧ i < as.size ∧ p as[i] = true

Proof state:
case isFalse.mp
α : Type u_1
p : α → Bool
as : Array α
start stop : Nat
h✝ : ¬stop ≤ as.size
⊢ (∃ i x, start ≤ i ∧ i < as.size ∧ p as[i] = true) → ∃ i x, start ≤ i ∧ i < stop ∧ p as[i] = true

Tactic:
rintro ⟨i, hi, ge, _, h⟩

Result:
case isFalse.mp.intro.intro.intro.intro
α : Type u_1
p : α → Bool
as : Array α
start stop : Nat
h✝ : ¬stop ≤ as.size
i : Nat
hi : i < as.size
ge : start ≤ i
left✝ : i < as.size
h : p as[i] = true
⊢ ∃ i x, start ≤ i ∧ i < stop ∧ p as[i] = true

Proof state:
α : Type u_1
p : α → Bool
as : Array α
start stop : Nat
h✝ : ¬stop ≤ as.size
i : Nat
hi : i < as.size
ge : start ≤ i
left✝ : i < as.size
h : p as[i] = true
⊢ i < stop

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
as : Array α
start stop : Nat
h✝ : ¬stop ≤ as.size
i : Nat
hi : i < as.size
ge : start ≤ i
left✝ : i < stop
h : p as[i] = true
⊢ start ≤ i

Tactic:
omega

Result:
no goals