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

Proof state:
start stop : Nat
p : Nat → Bool
h : start < stop
hstart : p start = true
hstop : p stop = false
⊢ start ≤
    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

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
⊢ start ≤
    match hmid : p (start.avg stop) with
    | false => bisect h✝ hstart hmid
    | true => bisect ⋯ hmid hstop

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 ≤ start.avg 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
this : start.avg stop - start < stop - start
⊢ start ≤ bisect h' hstart ⋯

Tactic:
exact start_le_bisect ..

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

Tactic:
simp only

Result:
start stop : Nat
p : Nat → Bool
h : start < stop
hstart : p start = true
hstop : p stop = false
⊢ start ≤
    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

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) = true
⊢ start.avg stop ≤ bisect ⋯ ⋯ hstop

Tactic:
exact start_le_bisect ..

Result:
no goals

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
⊢ start ≤
    match hmid : p (start.avg stop) with
    | false => bisect h✝ hstart hmid
    | true => bisect ⋯ hmid hstop

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
⊢ start ≤ bisect h✝ hstart ⋯

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
⊢ start ≤ bisect ⋯ ⋯ hstop

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

Tactic:
unfold bisect

Result:
start stop : Nat
p : Nat → Bool
h : start < stop
hstart : p start = true
hstop : p stop = false
⊢ start ≤
    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

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) = true
⊢ start ≤ ?m

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
h' : start < start.avg stop
heq✝ : p (start.avg stop) = true
⊢ start ≤ bisect ⋯ ⋯ hstop

Tactic:
apply Nat.le_trans

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) = true
⊢ start ≤ ?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) = true
⊢ ?m ≤ bisect ⋯ ⋯ hstop

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) = true
⊢ Nat

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 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
⊢ 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 isFalse
start stop : Nat
p : Nat → Bool
h : start < stop
hstart : p start = true
hstop : p stop = false
h✝ : ¬start < start.avg stop
⊢ start ≤ start.avg stop

Tactic:
exact le_avg_left (Nat.le_of_lt h)

Result:
no goals