-- 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:
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 true 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

Result:
no goals

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
⊢ false = true ↔ ∃ i, start ≤ ↑i ∧ ↑i < stop ∧ q i

Tactic:
simp

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
⊢ ∀ (x : Fin as.size), start ≤ ↑x → ↑x < stop → ¬q x

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) (pure false)

Tactic:
refine .pure ?_

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
⊢ false = true ↔ ∃ i, start ≤ ↑i ∧ ↑i < stop ∧ q 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),
    ↑i < stop →
      (fun j => start ≤ j ∧ ¬∃ i, start ≤ ↑i ∧ ↑i < j ∧ q i) ↑i →
        SatisfiesM
          (fun x =>
            bif x then ∃ i, start ≤ ↑i ∧ ↑i < stop ∧ q i
            else (fun j => start ≤ j ∧ ¬∃ i, start ≤ ↑i ∧ ↑i < j ∧ q i) (↑i + 1))
          (p as[i])

Tactic:
refine fun i h₂ ⟨h₁, h₃⟩ => (hp _ h₁ h₂).imp fun hq => ?_

Result:
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
⊢ bif a✝ then ∃ i, start ≤ ↑i ∧ ↑i < stop ∧ q i else (fun j => start ≤ j ∧ ¬∃ i, start ≤ ↑i ∧ ↑i < j ∧ q i) (↑i + 1)

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
⊢ bif a✝ then ∃ i, start ≤ ↑i ∧ ↑i < stop ∧ q i else (fun j => start ≤ j ∧ ¬∃ i, start ≤ ↑i ∧ ↑i < j ∧ q i) (↑i + 1)

Tactic:
unfold cond

Result:
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)

Proof state:
case inl
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
⊢ SatisfiesM (fun res => res = true ↔ ∃ i, start ≤ ↑i ∧ ↑i < stop ∧ q i) (anyM p as start stop)

Tactic:
refine (SatisfiesM_anyM _ _ _ _ hstart
  (fal := fun j => start ≤ j ∧ ¬ ∃ i : Fin as.size, start ≤ i.1 ∧ i.1 < j ∧ q i)
  (tru := ∃ i : Fin as.size, start ≤ i.1 ∧ i.1 < stop ∧ q i) ?_ ?_).imp ?_

Result:
case inl.refine_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
⊢ (fun j => start ≤ j ∧ ¬∃ i, start ≤ ↑i ∧ ↑i < j ∧ q i) start

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),
    ↑i < stop →
      (fun j => start ≤ j ∧ ¬∃ i, start ≤ ↑i ∧ ↑i < j ∧ q i) ↑i →
        SatisfiesM
          (fun x =>
            bif x then ∃ i, start ≤ ↑i ∧ ↑i < stop ∧ q i
            else (fun j => start ≤ j ∧ ¬∃ i, start ≤ ↑i ∧ ↑i < j ∧ q i) (↑i + 1))
          (p as[i])

case inl.refine_3
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
⊢ ∀ {a : Bool},
    (bif a then ∃ i, start ≤ ↑i ∧ ↑i < stop ∧ q i
      else start ≤ min stop as.size ∧ ¬∃ i, start ≤ ↑i ∧ ↑i < min stop as.size ∧ q i) →
      (a = true ↔ ∃ i, start ≤ ↑i ∧ ↑i < stop ∧ q i)

Proof state:
case inl.refine_3
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
⊢ ∀ {a : Bool},
    (bif a then ∃ i, start ≤ ↑i ∧ ↑i < stop ∧ q i
      else start ≤ min stop as.size ∧ ¬∃ i, start ≤ ↑i ∧ ↑i < min stop as.size ∧ q i) →
      (a = true ↔ ∃ i, start ≤ ↑i ∧ ↑i < stop ∧ q i)

Tactic:
intro
| true, h => simp only [true_iff]; exact h
| false, h =>
  simp only [false_iff, reduceCtorEq]
  exact h.2.imp fun ⟨j, h₁, h₂, hq⟩ => ⟨j, h₁, Nat.lt_min.2 ⟨h₂, j.2⟩, hq⟩

Result:
no goals