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

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

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
⊢ p (bisect h✝ hstart ⋯) = true

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
⊢ p (bisect ⋯ ⋯ hstop) = true

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

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

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

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:
case e_a
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 = start

Tactic:
apply Nat.le_antisymm

Result:
case e_a.h₁
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 ≤ start

case e_a.h₂
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:
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
⊢ p (bisect ⋯ ⋯ hstop) = true

Tactic:
exact bisect_true ..

Result:
no goals

Proof state:
case e_a.h₁
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 ≤ start

Tactic:
exact Nat.le_of_not_gt h'

Result:
no goals

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

Tactic:
unfold bisect

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

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_avg_left (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
⊢ p (start.avg stop) = true

Tactic:
rw [← hstart]

Result:
start stop : Nat
p : Nat → Bool
h : start < stop
hstart : p start = true
hstop : p stop = false
h' : ¬start < start.avg stop
⊢ p (start.avg stop) = p start

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 e_a.h₂
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 Nat.le_avg_left (Nat.le_of_lt h)

Result:
no goals

Proof state:
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
this : start.avg stop - start < stop - start
⊢ p (bisect h✝ hstart ⋯) = true

Tactic:
exact bisect_true ..

Result:
no goals

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

Tactic:
simp only

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

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

Tactic:
congr

Result:
case e_a
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 = start