-- Mathlib/Order/Estimator.lean
theorem Estimator.improveUntilAux_spec (a : Thunk α) (p : α → Bool)
    [Estimator a ε] [WellFoundedGT (range (bound a : ε → α))] (e : ε) (r : Bool) :
    match Estimator.improveUntilAux a p e r with
    | .error _ => ¬ p a.get
    | .ok e' => p (bound a e')

Proof state:
α : Type u_1
ε : Type u_2
inst✝² : Preorder α
a : Thunk α
p : α → Bool
inst✝¹ : Estimator a ε
inst✝ : WellFoundedGT ↑(range (bound a))
e : ε
r : Bool
⊢ match
    if p (bound a e) = true then pure e
    else
      match improve a e, ⋯ with
      | none, x => Except.error (if r = true then none else some e)
      | some e', x => improveUntilAux a p e' true with
  | Except.error a_1 => ¬p a.get = true
  | Except.ok e' => p (bound a e') = true

Tactic:
by_cases h : p (bound a e)

Result:
case pos
α : Type u_1
ε : Type u_2
inst✝² : Preorder α
a : Thunk α
p : α → Bool
inst✝¹ : Estimator a ε
inst✝ : WellFoundedGT ↑(range (bound a))
e : ε
r : Bool
h : p (bound a e) = true
⊢ match
    if p (bound a e) = true then pure e
    else
      match improve a e, ⋯ with
      | none, x => Except.error (if r = true then none else some e)
      | some e', x => improveUntilAux a p e' true with
  | Except.error a_1 => ¬p a.get = true
  | Except.ok e' => p (bound a e') = true

case neg
α : Type u_1
ε : Type u_2
inst✝² : Preorder α
a : Thunk α
p : α → Bool
inst✝¹ : Estimator a ε
inst✝ : WellFoundedGT ↑(range (bound a))
e : ε
r : Bool
h : ¬p (bound a e) = true
⊢ match
    if p (bound a e) = true then pure e
    else
      match improve a e, ⋯ with
      | none, x => Except.error (if r = true then none else some e)
      | some e', x => improveUntilAux a p e' true with
  | Except.error a_1 => ¬p a.get = true
  | Except.ok e' => p (bound a e') = true

Proof state:
α : Type u_1
ε : Type u_2
inst✝² : Preorder α
a : Thunk α
p : α → Bool
inst✝¹ : Estimator a ε
inst✝ : WellFoundedGT ↑(range (bound a))
e : ε
r : Bool
h : ¬p (bound a e) = true
eq :
  match none with
  | none => bound a e = a.get
  | some e' => bound a e < bound a e'
⊢ match
    if false = true then pure e
    else
      match none, eq with
      | none, x => Except.error (if r = true then none else some e)
      | some e', x => improveUntilAux a p e' true with
  | Except.error a_1 => ¬p a.get = true
  | Except.ok e' => p (bound a e') = true

Tactic:
simp only [Bool.not_eq_true]

Result:
α : Type u_1
ε : Type u_2
inst✝² : Preorder α
a : Thunk α
p : α → Bool
inst✝¹ : Estimator a ε
inst✝ : WellFoundedGT ↑(range (bound a))
e : ε
r : Bool
h : ¬p (bound a e) = true
eq :
  match none with
  | none => bound a e = a.get
  | some e' => bound a e < bound a e'
⊢ match if false = true then pure e else Except.error (if r = true then none else some e) with
  | Except.error a_1 => p a.get = false
  | Except.ok e' => p (bound a e') = true

Proof state:
α : Type u_1
ε : Type u_2
inst✝² : Preorder α
a : Thunk α
p : α → Bool
inst✝¹ : Estimator a ε
inst✝ : WellFoundedGT ↑(range (bound a))
e : ε
r : Bool
⊢ match improveUntilAux a p e r with
  | Except.error a_1 => ¬p a.get = true
  | Except.ok e' => p (bound a e') = true

Tactic:
rw [Estimator.improveUntilAux]

Result:
α : Type u_1
ε : Type u_2
inst✝² : Preorder α
a : Thunk α
p : α → Bool
inst✝¹ : Estimator a ε
inst✝ : WellFoundedGT ↑(range (bound a))
e : ε
r : Bool
⊢ match
    if p (bound a e) = true then pure e
    else
      match improve a e, ⋯ with
      | none, x => Except.error (if r = true then none else some e)
      | some e', x => improveUntilAux a p e' true with
  | Except.error a_1 => ¬p a.get = true
  | Except.ok e' => p (bound a e') = true

Proof state:
case neg
α : Type u_1
ε : Type u_2
inst✝² : Preorder α
a : Thunk α
p : α → Bool
inst✝¹ : Estimator a ε
inst✝ : WellFoundedGT ↑(range (bound a))
e : ε
r : Bool
h : ¬p (bound a e) = true
⊢ match
    if p (bound a e) = true then pure e
    else
      match improve a e, ⋯ with
      | none, x => Except.error (if r = true then none else some e)
      | some e', x => improveUntilAux a p e' true with
  | Except.error a_1 => ¬p a.get = true
  | Except.ok e' => p (bound a e') = true

Tactic:
simp only [h]

Result:
case neg
α : Type u_1
ε : Type u_2
inst✝² : Preorder α
a : Thunk α
p : α → Bool
inst✝¹ : Estimator a ε
inst✝ : WellFoundedGT ↑(range (bound a))
e : ε
r : Bool
h : ¬p (bound a e) = true
⊢ match
    if false = true then pure e
    else
      match improve a e, ⋯ with
      | none, x => Except.error (if r = true then none else some e)
      | some e', x => improveUntilAux a p e' true with
  | Except.error a_1 => ¬p a.get = true
  | Except.ok e' => p (bound a e') = true

Proof state:
α : Type u_1
ε : Type u_2
inst✝² : Preorder α
a : Thunk α
p : α → Bool
inst✝¹ : Estimator a ε
inst✝ : WellFoundedGT ↑(range (bound a))
e : ε
r : Bool
h : ¬p a.get = true
eq :
  match none with
  | none => bound a e = a.get
  | some e' => bound a e < bound a e'
⊢ match if false = true then pure e else Except.error (if r = true then none else some e) with
  | Except.error a_1 => p a.get = false
  | Except.ok e' => p (bound a e') = true

Tactic:
exact Bool.bool_eq_false h

Result:
no goals

Proof state:
α : Type u_1
ε : Type u_2
inst✝² : Preorder α
a : Thunk α
p : α → Bool
inst✝¹ : Estimator a ε
inst✝ : WellFoundedGT ↑(range (bound a))
e : ε
r : Bool
h : ¬p (bound a e) = true
eq :
  match none with
  | none => bound a e = a.get
  | some e' => bound a e < bound a e'
⊢ match if false = true then pure e else Except.error (if r = true then none else some e) with
  | Except.error a_1 => p a.get = false
  | Except.ok e' => p (bound a e') = true

Tactic:
rw [eq] at h

Result:
α : Type u_1
ε : Type u_2
inst✝² : Preorder α
a : Thunk α
p : α → Bool
inst✝¹ : Estimator a ε
inst✝ : WellFoundedGT ↑(range (bound a))
e : ε
r : Bool
h : ¬p a.get = true
eq :
  match none with
  | none => bound a e = a.get
  | some e' => bound a e < bound a e'
⊢ match if false = true then pure e else Except.error (if r = true then none else some e) with
  | Except.error a_1 => p a.get = false
  | Except.ok e' => p (bound a e') = true

Proof state:
α : Type u_1
ε : Type u_2
inst✝² : Preorder α
a : Thunk α
p : α → Bool
inst✝¹ : Estimator a ε
inst✝ : WellFoundedGT ↑(range (bound a))
e : ε
r : Bool
h : ¬p (bound a e) = true
e' : ε
x✝ :
  match some e' with
  | none => bound a e = a.get
  | some e' => bound a e < bound a e'
⊢ match
    if false = true then pure e
    else
      match some e', x✝ with
      | none, x => Except.error (if r = true then none else some e)
      | some e', x => improveUntilAux a p e' true with
  | Except.error a_1 => ¬p a.get = true
  | Except.ok e' => p (bound a e') = true

Tactic:
exact Estimator.improveUntilAux_spec a p e' true

Result:
no goals

Proof state:
case pos
α : Type u_1
ε : Type u_2
inst✝² : Preorder α
a : Thunk α
p : α → Bool
inst✝¹ : Estimator a ε
inst✝ : WellFoundedGT ↑(range (bound a))
e : ε
r : Bool
h : p (bound a e) = true
⊢ match
    if p (bound a e) = true then pure e
    else
      match improve a e, ⋯ with
      | none, x => Except.error (if r = true then none else some e)
      | some e', x => improveUntilAux a p e' true with
  | Except.error a_1 => ¬p a.get = true
  | Except.ok e' => p (bound a e') = true

Tactic:
simp only [h]

Result:
case pos
α : Type u_1
ε : Type u_2
inst✝² : Preorder α
a : Thunk α
p : α → Bool
inst✝¹ : Estimator a ε
inst✝ : WellFoundedGT ↑(range (bound a))
e : ε
r : Bool
h : p (bound a e) = true
⊢ match
    if True then pure e
    else
      match improve a e, ⋯ with
      | none, x => Except.error (if r = true then none else some e)
      | some e', x => improveUntilAux a p e' true with
  | Except.error a_1 => ¬p a.get = true
  | Except.ok e' => p (bound a e') = true