-- 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:
case isTrue
α : Type u_1
p : α → Bool
as : Array α
start stop : Nat
h : stop ≤ as.size
h₁ : start < stop
⊢ (let_fun this := ⋯;
      do
      let __do_lift ← p as[start]
      if __do_lift = true then pure true else anyM.loop p as stop h (start + 1)) =
      true ↔
    ∃ i x, start ≤ i ∧ i < stop ∧ p as[i] = true

Tactic:
dsimp

Result:
case isTrue
α : Type u_1
p : α → Bool
as : Array α
start stop : Nat
h : stop ≤ as.size
h₁ : start < stop
⊢ (if p as[start] = true then true else anyM.loop p as stop h (start + 1)) = 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
i : Nat
hi : i < as.size
ge : start + 1 ≤ i
lt : i < stop
h : p as[i] = true
this : start ≠ i
⊢ i < as.size

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
⊢ ∀ (x : Nat), start ≤ x → x < stop → ∀ (x_1 : x < as.size), p as[x] = false

Tactic:
omega

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
⊢ start ≤ start

Tactic:
omega

Result:
no goals

Proof state:
case isTrue.isFalse.mpr.intro.intro.intro.intro
α : 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
⊢ ∃ i x, start + 1 ≤ i ∧ i < stop ∧ p as[i] = true

Tactic:
have : start ≠ i := by rintro rfl; erw [h] at h₂; simp_all

Result:
case isTrue.isFalse.mpr.intro.intro.intro.intro
α : 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 x, start + 1 ≤ i ∧ i < stop ∧ p as[i] = true

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

Tactic:
split <;> rename_i h₂

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
⊢ true = true ↔ ∃ i x, start ≤ i ∧ i < stop ∧ p as[i] = true

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

Proof state:
case isTrue.isFalse.mp.intro.intro.intro.intro
α : 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
⊢ ∃ i x, start ≤ i ∧ i < stop ∧ p as[i] = true

Tactic:
have : start ≠ i := by rintro rfl; omega

Result:
case isTrue.isFalse.mp.intro.intro.intro.intro
α : 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
⊢ ∃ i x, start ≤ i ∧ i < stop ∧ p as[i] = true

Proof state:
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

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

Result:
case isTrue.isFalse.mpr.intro.intro.intro.intro
α : 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
⊢ ∃ i x, start + 1 ≤ i ∧ i < stop ∧ p as[i] = true

Proof state:
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

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

Result:
case isTrue.isFalse.mp.intro.intro.intro.intro
α : 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
⊢ ∃ 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 < as.size

Tactic:
omega

Result:
no goals

Proof state:
α : 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:
unfold anyM.loop

Result:
α : Type u_1
p : α → Bool
as : Array α
start stop : Nat
h : stop ≤ as.size
⊢ (if hlt : start < stop then
        let_fun this := ⋯;
        do
        let __do_lift ← p as[start]
        if __do_lift = true then pure true else anyM.loop p as stop h (start + 1)
      else pure false) =
      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
⊢ (if hlt : start < stop then
        let_fun this := ⋯;
        do
        let __do_lift ← p as[start]
        if __do_lift = true then pure true else anyM.loop p as stop h (start + 1)
      else pure false) =
      true ↔
    ∃ i x, start ≤ i ∧ i < stop ∧ p as[i] = true

Tactic:
split <;> rename_i h₁

Result:
case isTrue
α : Type u_1
p : α → Bool
as : Array α
start stop : Nat
h : stop ≤ as.size
h₁ : start < stop
⊢ (let_fun this := ⋯;
      do
      let __do_lift ← p as[start]
      if __do_lift = true then pure true else anyM.loop p as stop h (start + 1)) =
      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
h₁ : ¬start < stop
⊢ pure false = 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
i : Nat
hi : i < as.size
ge : start ≤ i
lt : i < stop
h : p as[i] = true
this : start ≠ i
⊢ start + 1 ≤ i

Tactic:
omega

Result:
no goals

Proof state:
case isTrue.isFalse.mpr.intro.intro.intro.intro
α : 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 x, start + 1 ≤ i ∧ i < stop ∧ p as[i] = true

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

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
hi : start < as.size
ge : start + 1 ≤ start
lt : start < stop
h : p as[start] = true
⊢ False

Tactic:
omega

Result:
no goals

Proof state:
case isTrue.isFalse.mp.intro.intro.intro.intro
α : 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
⊢ ∃ i x, start ≤ i ∧ i < stop ∧ p as[i] = true

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

Result:
no goals