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

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
⊢ start ≤ start.avg stop

Tactic:
exact Nat.le_avg_left (Nat.le_of_lt h)

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
h' : ¬start < start.avg stop
heq : start.avg stop = start
⊢ p (start + 1) = p stop

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
heq : start.avg stop = start
⊢ start + 1 = stop

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 ⋯ + 1) = false

Tactic:
exact bisect_add_one_false ..

Result:
no goals

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
⊢ start.avg stop ≤ start

Tactic:
exact Nat.le_of_not_gt h'

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
heq : start.avg stop = start
⊢ stop ≤ start + 1

Tactic:
exact Nat.le_add_one_of_avg_eq_left heq

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 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 + 1) = false

Tactic:
exact bisect_add_one_false ..

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
heq : start.avg stop = start
⊢ start + 1 = stop

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
heq : start.avg stop = start
⊢ start + 1 ≤ stop

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
heq : start.avg stop = start
⊢ stop ≤ start + 1

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:
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) +
        1) =
    false

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 ⋯ + 1) = false

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 + 1) = false

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) +
        1) =
    false

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) +
        1) =
    false

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 + 1) = false

Proof state:
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 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 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 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
heq : start.avg stop = start
⊢ start + 1 ≤ stop

Tactic:
exact Nat.succ_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
⊢ p (bisect h hstart hstop + 1) = false

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) +
        1) =
    false

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) +
        1) =
    false

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) +
        1) =
    false

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 : start.avg stop = start
⊢ p (start.avg stop + 1) = false

Tactic:
rw [← hstop, heq]

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