-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem anyM_loop_iff_exists {p : α → Bool} {as : Array α} {start stop} (h : stop ≤ as.size) :
    anyM.loop (m := Id) p as stop h start = true ↔
      ∃ (i : Nat) (_ : i < as.size), start ≤ i ∧ i < stop ∧ p as[i] = true

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

Tactic:
rintro rfl

Result:
α : Type u_1
p : α → Bool
as : Array α
start stop : Nat
h✝ : stop ≤ as.size
h₁ : start < stop
h₂ : ¬p as[start] = true
hi : start < as.size
ge : start ≤ start
lt : start < stop
h : p as[start] = true
⊢ False

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

Tactic:
erw [h] at h₂

Result:
α : Type u_1
p : α → Bool
as : Array α
start stop : Nat
h✝ : stop ≤ as.size
h₁ : start < stop
h₂ : ¬true = true
hi : start < as.size
ge : start ≤ start
lt : start < stop
h : p as[start] = true
⊢ False

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

Tactic:
simp only [true_iff]

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

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

Tactic:
constructor

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

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

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

Tactic:
refine ⟨start, 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
h₁ : start < stop
h₂ : ¬true = true
hi : start < as.size
ge : start ≤ start
lt : start < stop
h : p as[start] = true
⊢ False

Tactic:
simp_all

Result:
no goals

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

Tactic:
rintro rfl

Result:
α : Type u_1
p : α → Bool
as : Array α
start stop : Nat
h✝ : stop ≤ as.size
h₁ : start < stop
h₂ : ¬p as[start] = true
hi : start < as.size
ge : start + 1 ≤ start
lt : start < stop
h : p as[start] = true
⊢ False

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

Tactic:
omega

Result:
no goals

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

Tactic:
rw [anyM_loop_iff_exists]

Result:
case isTrue.isFalse
α : Type u_1
p : α → Bool
as : Array α
start stop : Nat
h : stop ≤ as.size
h₁ : start < stop
h₂ : ¬p as[start] = true
⊢ (∃ i x, start + 1 ≤ i ∧ i < stop ∧ 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
h₁ : start < stop
h₂ : p as[start] = true
⊢ start < stop

Tactic:
omega

Result:
no goals

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

Tactic:
simp

Result:
case isFalse
α : Type u_1
p : α → Bool
as : Array α
start stop : Nat
h : stop ≤ as.size
h₁ : ¬start < stop
⊢ ∀ (x : Nat), start ≤ x → x < stop → ∀ (x_1 : x < as.size), p as[x] = false

Proof state:
α : Type u_1
p : α → Bool
as : Array α
start stop : Nat
h✝ : stop ≤ as.size
h₁ : start < stop
h₂ : ¬p as[start] = true
i : Nat
hi : i < as.size
ge : start + 1 ≤ i
lt : i < stop
h : p as[i] = true
this : start ≠ i
⊢ start ≤ i

Tactic:
omega

Result:
no goals