case a
α : Type u
β : Type v
γ : Type w
s : Computation α
h : Terminates s
⊢ length (think s) ≤ length s + 1

case a
α : Type u
β : Type v
γ : Type w
s : Computation α
h : Terminates s
⊢ length s + 1 ≤ length (think s)
α : Type u
β : Type v
γ : Type w
s : Computation α
h : Terminates s
⊢ length (think s) = length s + 1
apply le_antisymm
no goals
case a
α : Type u
β : Type v
γ : Type w
s : Computation α
h : Terminates s
⊢ length (think s) ≤ length s + 1
exact Nat.find_min' _ (Nat.find_spec ((terminates_def _).1 h))
case a
α : Type u
β : Type v
γ : Type w
s : Computation α
h : Terminates s
this : Option.isSome (↑(think s) (length (think s))) = true
⊢ length s + 1 ≤ length (think s)
case a
α : Type u
β : Type v
γ : Type w
s : Computation α
h : Terminates s
⊢ length s + 1 ≤ length (think s)
have : (Option.isSome ((think s).val (length (think s))) : Prop) :=
  Nat.find_spec ((terminates_def _).1 s.think_terminates)
case a
α : Type u
β : Type v
γ : Type w
s : Computation α
h : Terminates s
⊢ Option.isSome (↑(think s) (length (think s))) = true → length s + 1 ≤ length (think s)
case a
α : Type u
β : Type v
γ : Type w
s : Computation α
h : Terminates s
this : Option.isSome (↑(think s) (length (think s))) = true
⊢ length s + 1 ≤ length (think s)
revert this
case a.zero
α : Type u
β : Type v
γ : Type w
s : Computation α
h : Terminates s
this : Option.isSome (↑(think s) Nat.zero) = true
⊢ length s + 1 ≤ Nat.zero

case a.succ
α : Type u
β : Type v
γ : Type w
s : Computation α
h : Terminates s
n : ℕ
this : Option.isSome (↑(think s) (Nat.succ n)) = true
⊢ length s + 1 ≤ Nat.succ n
case a
α : Type u
β : Type v
γ : Type w
s : Computation α
h : Terminates s
⊢ Option.isSome (↑(think s) (length (think s))) = true → length s + 1 ≤ length (think s)
cases' length (think s) with n <;> intro this
no goals
case a.zero
α : Type u
β : Type v
γ : Type w
s : Computation α
h : Terminates s
this : Option.isSome (↑(think s) Nat.zero) = true
⊢ length s + 1 ≤ Nat.zero
simp [think, Stream'.cons] at this
case a.succ.a
α : Type u
β : Type v
γ : Type w
s : Computation α
h : Terminates s
n : ℕ
this : Option.isSome (↑(think s) (Nat.succ n)) = true
⊢ length s ≤ n
case a.succ
α : Type u
β : Type v
γ : Type w
s : Computation α
h : Terminates s
n : ℕ
this : Option.isSome (↑(think s) (Nat.succ n)) = true
⊢ length s + 1 ≤ Nat.succ n
apply Nat.succ_le_succ
case a.succ.a.h
α : Type u
β : Type v
γ : Type w
s : Computation α
h : Terminates s
n : ℕ
this : Option.isSome (↑(think s) (Nat.succ n)) = true
⊢ Option.isSome (↑s n) = true
case a.succ.a
α : Type u
β : Type v
γ : Type w
s : Computation α
h : Terminates s
n : ℕ
this : Option.isSome (↑(think s) (Nat.succ n)) = true
⊢ length s ≤ n
apply Nat.find_min'
no goals
case a.succ.a.h
α : Type u
β : Type v
γ : Type w
s : Computation α
h : Terminates s
n : ℕ
this : Option.isSome (↑(think s) (Nat.succ n)) = true
⊢ Option.isSome (↑s n) = true
apply this