-- Mathlib/.lake/packages/batteries/Batteries/Data/Nat/Bisect.lean
theorem bisect_lt_stop {p : Nat → Bool} (h : start < stop) (hstart : p start = true)
    (hstop : p stop = false) : bisect h hstart hstop < stop

Proof state:
case isTrue
start stop : Nat
p : Nat → Bool
h : start < stop
hstart : p start = true
hstop : p stop = false
h✝ : start < start.avg stop
⊢ (match hmid : p (start.avg stop) with
    | false => bisect h✝ hstart hmid
    | true => bisect ⋯ hmid hstop) <
    stop

Tactic:
split

Result:
case isTrue.h_1
start stop : Nat
p : Nat → Bool
h : start < stop
hstart : p start = true
hstop : p stop = false
h✝ : start < start.avg stop
heq✝ : p (start.avg stop) = false
⊢ bisect h✝ hstart ⋯ < stop

case isTrue.h_2
start stop : Nat
p : Nat → Bool
h : start < stop
hstart : p start = true
hstop : p stop = false
h✝ : start < start.avg stop
heq✝ : p (start.avg stop) = true
⊢ bisect ⋯ ⋯ hstop < stop

Proof state:
start stop : Nat
p : Nat → Bool
h : start < stop
hstart : p start = true
hstop : p stop = false
h' : start < start.avg stop
heq✝ : p (start.avg stop) = false
⊢ start.avg stop - start < stop - start

Tactic:
apply Nat.sub_lt_sub_right

Result:
case a
start stop : Nat
p : Nat → Bool
h : start < stop
hstart : p start = true
hstop : p stop = false
h' : start < start.avg stop
heq✝ : p (start.avg stop) = false
⊢ start ≤ start.avg stop

case a
start stop : Nat
p : Nat → Bool
h : start < stop
hstart : p start = true
hstop : p stop = false
h' : start < start.avg stop
heq✝ : p (start.avg stop) = false
⊢ start.avg stop < stop

Proof state:
case a
start stop : Nat
p : Nat → Bool
h : start < stop
hstart : p start = true
hstop : p stop = false
h' : start < start.avg stop
heq✝ : p (start.avg stop) = false
⊢ start ≤ start.avg stop

Tactic:
exact Nat.le_of_lt h'

Result:
no goals

Proof state:
start stop : Nat
p : Nat → Bool
h : start < stop
hstart : p start = true
hstop : p stop = false
⊢ (if hstartmid : start < start.avg stop then
      match hmid : p (start.avg stop) with
      | false => bisect hstartmid hstart hmid
      | true => bisect ⋯ hmid hstop
    else start.avg stop) <
    stop

Tactic:
split

Result:
case isTrue
start stop : Nat
p : Nat → Bool
h : start < stop
hstart : p start = true
hstop : p stop = false
h✝ : start < start.avg stop
⊢ (match hmid : p (start.avg stop) with
    | false => bisect h✝ hstart hmid
    | true => bisect ⋯ hmid hstop) <
    stop

case isFalse
start stop : Nat
p : Nat → Bool
h : start < stop
hstart : p start = true
hstop : p stop = false
h✝ : ¬start < start.avg stop
⊢ start.avg stop < stop

Proof state:
start stop : Nat
p : Nat → Bool
h : start < stop
hstart : p start = true
hstop : p stop = false
⊢ (let mid := start.avg stop;
    let_fun hmidstop := ⋯;
    if hstartmid : start < mid then
      match hmid : p mid with
      | false => bisect hstartmid hstart hmid
      | true => bisect hmidstop hmid hstop
    else mid) <
    stop

Tactic:
simp only

Result:
start stop : Nat
p : Nat → Bool
h : start < stop
hstart : p start = true
hstop : p stop = false
⊢ (if hstartmid : start < start.avg stop then
      match hmid : p (start.avg stop) with
      | false => bisect hstartmid hstart hmid
      | true => bisect ⋯ hmid hstop
    else start.avg stop) <
    stop

Proof state:
case isTrue.h_2
start stop : Nat
p : Nat → Bool
h : start < stop
hstart : p start = true
hstop : p stop = false
h✝ : start < start.avg stop
heq✝ : p (start.avg stop) = true
⊢ bisect ⋯ ⋯ hstop < stop

Tactic:
exact bisect_lt_stop ..

Result:
no goals

Proof state:
case a
start stop : Nat
p : Nat → Bool
h : start < stop
hstart : p start = true
hstop : p stop = false
h' : start < start.avg stop
heq✝ : p (start.avg stop) = false
this : start.avg stop - start < stop - start
⊢ start.avg stop < stop

Tactic:
exact avg_lt_right h

Result:
no goals

Proof state:
case isFalse
start stop : Nat
p : Nat → Bool
h : start < stop
hstart : p start = true
hstop : p stop = false
h✝ : ¬start < start.avg stop
⊢ start.avg stop < stop

Tactic:
exact avg_lt_right h

Result:
no goals

Proof state:
start stop : Nat
p : Nat → Bool
h : start < stop
hstart : p start = true
hstop : p stop = false
h' : start < start.avg stop
heq✝ : p (start.avg stop) = false
this : start.avg stop - start < stop - start
⊢ bisect h' hstart ⋯ < stop

Tactic:
apply Nat.lt_trans

Result:
case h₁
start stop : Nat
p : Nat → Bool
h : start < stop
hstart : p start = true
hstop : p stop = false
h' : start < start.avg stop
heq✝ : p (start.avg stop) = false
this : start.avg stop - start < stop - start
⊢ bisect h' hstart ⋯ < ?m

case a
start stop : Nat
p : Nat → Bool
h : start < stop
hstart : p start = true
hstop : p stop = false
h' : start < start.avg stop
heq✝ : p (start.avg stop) = false
this : start.avg stop - start < stop - start
⊢ ?m < stop

case m
start stop : Nat
p : Nat → Bool
h : start < stop
hstart : p start = true
hstop : p stop = false
h' : start < start.avg stop
heq✝ : p (start.avg stop) = false
this : start.avg stop - start < stop - start
⊢ Nat

Proof state:
case h₁
start stop : Nat
p : Nat → Bool
h : start < stop
hstart : p start = true
hstop : p stop = false
h' : start < start.avg stop
heq✝ : p (start.avg stop) = false
this : start.avg stop - start < stop - start
⊢ bisect h' hstart ⋯ < ?m

Tactic:
exact bisect_lt_stop ..

Result:
no goals

Proof state:
case a
start stop : Nat
p : Nat → Bool
h : start < stop
hstart : p start = true
hstop : p stop = false
h' : start < start.avg stop
heq✝ : p (start.avg stop) = false
⊢ start.avg stop < stop

Tactic:
exact Nat.avg_lt_right h

Result:
no goals

Proof state:
start stop : Nat
p : Nat → Bool
h : start < stop
hstart : p start = true
hstop : p stop = false
⊢ bisect h hstart hstop < stop

Tactic:
unfold bisect

Result:
start stop : Nat
p : Nat → Bool
h : start < stop
hstart : p start = true
hstop : p stop = false
⊢ (let mid := start.avg stop;
    let_fun hmidstop := ⋯;
    if hstartmid : start < mid then
      match hmid : p mid with
      | false => bisect hstartmid hstart hmid
      | true => bisect hmidstop hmid hstop
    else mid) <
    stop