-- Mathlib/.lake/packages/batteries/Batteries/Data/Array/Monadic.lean
theorem SatisfiesM_anyM_iff_exists [Monad m] [LawfulMonad m]
    (p : α → m Bool) (as : Array α) (start stop) (q : Fin as.size → Prop)
    (hp : ∀ i : Fin as.size, start ≤ i.1 → i.1 < stop → SatisfiesM (· = true ↔ q i) (p as[i])) :
    SatisfiesM
      (fun res => res = true ↔ ∃ i : Fin as.size, start ≤ i.1 ∧ i.1 < stop ∧ q i)
      (anyM p as start stop)

Proof state:
case inr
m : Type → Type u_1
α : Type u_2
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
as : Array α
start stop : Nat
q : Fin as.size → Prop
hp : ∀ (i : Fin as.size), start ≤ ↑i → ↑i < stop → SatisfiesM (fun x => x = true ↔ q i) (p as[i])
hstart : min stop as.size ≤ start
⊢ ∀ (x : Fin as.size), start ≤ ↑x → ↑x < stop → ¬q x

Tactic:
intro j h₁ h₂

Result:
case inr
m : Type → Type u_1
α : Type u_2
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
as : Array α
start stop : Nat
q : Fin as.size → Prop
hp : ∀ (i : Fin as.size), start ≤ ↑i → ↑i < stop → SatisfiesM (fun x => x = true ↔ q i) (p as[i])
hstart : min stop as.size ≤ start
j : Fin as.size
h₁ : start ≤ ↑j
h₂ : ↑j < stop
⊢ ¬q j

Proof state:
case inl.refine_2.h_2
m : Type → Type u_1
α : Type u_2
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
as : Array α
start stop : Nat
q : Fin as.size → Prop
hp : ∀ (i : Fin as.size), start ≤ ↑i → ↑i < stop → SatisfiesM (fun x => x = true ↔ q i) (p as[i])
hstart : start ≤ min stop as.size
i : Fin as.size
h₂ : ↑i < stop
x✝ : (fun j => start ≤ j ∧ ¬∃ i, start ≤ ↑i ∧ ↑i < j ∧ q i) ↑i
h₁ : start ≤ ↑i
h₃ : ¬∃ i_1, start ≤ ↑i_1 ∧ ↑i_1 < ↑i ∧ q i_1
c✝ : Bool
hq : ¬q i
⊢ start ≤ ↑i + 1 ∧ ¬∃ i_1, start ≤ ↑i_1 ∧ ↑i_1 < ↑i + 1 ∧ q i_1

Tactic:
refine ⟨Nat.le_succ_of_le h₁, h₃.imp fun ⟨j, h₃, h₄, h₅⟩ => ⟨j, h₃, ?_, h₅⟩⟩

Result:
case inl.refine_2.h_2
m : Type → Type u_1
α : Type u_2
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
as : Array α
start stop : Nat
q : Fin as.size → Prop
hp : ∀ (i : Fin as.size), start ≤ ↑i → ↑i < stop → SatisfiesM (fun x => x = true ↔ q i) (p as[i])
hstart : start ≤ min stop as.size
i : Fin as.size
h₂ : ↑i < stop
x✝¹ : (fun j => start ≤ j ∧ ¬∃ i, start ≤ ↑i ∧ ↑i < j ∧ q i) ↑i
h₁ : start ≤ ↑i
h₃✝ : ¬∃ i_1, start ≤ ↑i_1 ∧ ↑i_1 < ↑i ∧ q i_1
c✝ : Bool
hq : ¬q i
x✝ : ∃ i_1, start ≤ ↑i_1 ∧ ↑i_1 < ↑i + 1 ∧ q i_1
j : Fin as.size
h₃ : start ≤ ↑j
h₄ : ↑j < ↑i + 1
h₅ : q j
⊢ ↑j < ↑i

Proof state:
case inl.refine_2
m : Type → Type u_1
α : Type u_2
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
as : Array α
start stop : Nat
q : Fin as.size → Prop
hp : ∀ (i : Fin as.size), start ≤ ↑i → ↑i < stop → SatisfiesM (fun x => x = true ↔ q i) (p as[i])
hstart : start ≤ min stop as.size
i : Fin as.size
h₂ : ↑i < stop
x✝ : (fun j => start ≤ j ∧ ¬∃ i, start ≤ ↑i ∧ ↑i < j ∧ q i) ↑i
h₁ : start ≤ ↑i
h₃ : ¬∃ i_1, start ≤ ↑i_1 ∧ ↑i_1 < ↑i ∧ q i_1
a✝ : Bool
hq : a✝ = true ↔ q i
⊢ match a✝ with
  | true => ∃ i, start ≤ ↑i ∧ ↑i < stop ∧ q i
  | false => (fun j => start ≤ j ∧ ¬∃ i, start ≤ ↑i ∧ ↑i < j ∧ q i) (↑i + 1)

Tactic:
split <;> simp at hq

Result:
case inl.refine_2.h_1
m : Type → Type u_1
α : Type u_2
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
as : Array α
start stop : Nat
q : Fin as.size → Prop
hp : ∀ (i : Fin as.size), start ≤ ↑i → ↑i < stop → SatisfiesM (fun x => x = true ↔ q i) (p as[i])
hstart : start ≤ min stop as.size
i : Fin as.size
h₂ : ↑i < stop
x✝ : (fun j => start ≤ j ∧ ¬∃ i, start ≤ ↑i ∧ ↑i < j ∧ q i) ↑i
h₁ : start ≤ ↑i
h₃ : ¬∃ i_1, start ≤ ↑i_1 ∧ ↑i_1 < ↑i ∧ q i_1
c✝ : Bool
hq : q i
⊢ ∃ i, start ≤ ↑i ∧ ↑i < stop ∧ q i

case inl.refine_2.h_2
m : Type → Type u_1
α : Type u_2
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
as : Array α
start stop : Nat
q : Fin as.size → Prop
hp : ∀ (i : Fin as.size), start ≤ ↑i → ↑i < stop → SatisfiesM (fun x => x = true ↔ q i) (p as[i])
hstart : start ≤ min stop as.size
i : Fin as.size
h₂ : ↑i < stop
x✝ : (fun j => start ≤ j ∧ ¬∃ i, start ≤ ↑i ∧ ↑i < j ∧ q i) ↑i
h₁ : start ≤ ↑i
h₃ : ¬∃ i_1, start ≤ ↑i_1 ∧ ↑i_1 < ↑i ∧ q i_1
c✝ : Bool
hq : ¬q i
⊢ start ≤ ↑i + 1 ∧ ¬∃ i_1, start ≤ ↑i_1 ∧ ↑i_1 < ↑i + 1 ∧ q i_1

Proof state:
case inr
m : Type → Type u_1
α : Type u_2
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
as : Array α
start stop : Nat
q : Fin as.size → Prop
hp : ∀ (i : Fin as.size), start ≤ ↑i → ↑i < stop → SatisfiesM (fun x => x = true ↔ q i) (p as[i])
hstart : min stop as.size ≤ start
⊢ SatisfiesM (fun res => res = true ↔ ∃ i, start ≤ ↑i ∧ ↑i < stop ∧ q i) (anyM p as start stop)

Tactic:
rw [anyM_stop_le_start (h := hstart)]

Result:
case inr
m : Type → Type u_1
α : Type u_2
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
as : Array α
start stop : Nat
q : Fin as.size → Prop
hp : ∀ (i : Fin as.size), start ≤ ↑i → ↑i < stop → SatisfiesM (fun x => x = true ↔ q i) (p as[i])
hstart : min stop as.size ≤ start
⊢ SatisfiesM (fun res => res = true ↔ ∃ i, start ≤ ↑i ∧ ↑i < stop ∧ q i) (pure false)

Proof state:
m : Type → Type u_1
α : Type u_2
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
as : Array α
start stop : Nat
q : Fin as.size → Prop
hp : ∀ (i : Fin as.size), start ≤ ↑i → ↑i < stop → SatisfiesM (fun x => x = true ↔ q i) (p as[i])
hstart : start ≤ min stop as.size
x✝¹ : Bool
x✝ :
  bif x✝¹ then ∃ i, start ≤ ↑i ∧ ↑i < stop ∧ q i
  else start ≤ min stop as.size ∧ ¬∃ i, start ≤ ↑i ∧ ↑i < min stop as.size ∧ q i
h :
  bif false then ∃ i, start ≤ ↑i ∧ ↑i < stop ∧ q i
  else start ≤ min stop as.size ∧ ¬∃ i, start ≤ ↑i ∧ ↑i < min stop as.size ∧ q i
⊢ ¬∃ i, start ≤ ↑i ∧ ↑i < stop ∧ q i

Tactic:
exact h.2.imp fun ⟨j, h₁, h₂, hq⟩ => ⟨j, h₁, Nat.lt_min.2 ⟨h₂, j.2⟩, hq⟩

Result:
no goals

Proof state:
case inl.refine_2.h_2
m : Type → Type u_1
α : Type u_2
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
as : Array α
start stop : Nat
q : Fin as.size → Prop
hp : ∀ (i : Fin as.size), start ≤ ↑i → ↑i < stop → SatisfiesM (fun x => x = true ↔ q i) (p as[i])
hstart : start ≤ min stop as.size
i : Fin as.size
h₂ : ↑i < stop
x✝¹ : (fun j => start ≤ j ∧ ¬∃ i, start ≤ ↑i ∧ ↑i < j ∧ q i) ↑i
h₁ : start ≤ ↑i
h₃✝ : ¬∃ i_1, start ≤ ↑i_1 ∧ ↑i_1 < ↑i ∧ q i_1
c✝ : Bool
hq : ¬q i
x✝ : ∃ i_1, start ≤ ↑i_1 ∧ ↑i_1 < ↑i + 1 ∧ q i_1
j : Fin as.size
h₃ : start ≤ ↑j
h₄ : ↑j < ↑i + 1
h₅ : q j
⊢ ↑j < ↑i

Tactic:
refine Nat.lt_of_le_of_ne (Nat.le_of_lt_succ h₄) fun e => hq (Fin.eq_of_val_eq e ▸ h₅)

Result:
no goals

Proof state:
m : Type → Type u_1
α : Type u_2
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
as : Array α
start stop : Nat
q : Fin as.size → Prop
hp : ∀ (i : Fin as.size), start ≤ ↑i → ↑i < stop → SatisfiesM (fun x => x = true ↔ q i) (p as[i])
hstart : start ≤ min stop as.size
x✝¹ : Bool
x✝ :
  bif x✝¹ then ∃ i, start ≤ ↑i ∧ ↑i < stop ∧ q i
  else start ≤ min stop as.size ∧ ¬∃ i, start ≤ ↑i ∧ ↑i < min stop as.size ∧ q i
h :
  bif false then ∃ i, start ≤ ↑i ∧ ↑i < stop ∧ q i
  else start ≤ min stop as.size ∧ ¬∃ i, start ≤ ↑i ∧ ↑i < min stop as.size ∧ q i
⊢ false = true ↔ ∃ i, start ≤ ↑i ∧ ↑i < stop ∧ q i

Tactic:
simp only [false_iff, reduceCtorEq]

Result:
m : Type → Type u_1
α : Type u_2
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
as : Array α
start stop : Nat
q : Fin as.size → Prop
hp : ∀ (i : Fin as.size), start ≤ ↑i → ↑i < stop → SatisfiesM (fun x => x = true ↔ q i) (p as[i])
hstart : start ≤ min stop as.size
x✝¹ : Bool
x✝ :
  bif x✝¹ then ∃ i, start ≤ ↑i ∧ ↑i < stop ∧ q i
  else start ≤ min stop as.size ∧ ¬∃ i, start ≤ ↑i ∧ ↑i < min stop as.size ∧ q i
h :
  bif false then ∃ i, start ≤ ↑i ∧ ↑i < stop ∧ q i
  else start ≤ min stop as.size ∧ ¬∃ i, start ≤ ↑i ∧ ↑i < min stop as.size ∧ q i
⊢ ¬∃ i, start ≤ ↑i ∧ ↑i < stop ∧ q i