noncomputable section help

Stream: new members

[pblpbl]

Hi, why is lean failing to synthesize Decidable s1 here?

noncomputable section

structure real :=
  neg: Bool
  dec: Nat
  frac: Nat -> Nat

def c (x : real) : real :=
  let s1 := ∃ N, ∀ n, n >= N -> x.frac n = 9
  if s1 then ⟨x.neg, x.dec + 1, λ n => 0⟩ else x

[Yakov Pechersky]

noncomputable section

structure real :=
  neg: Bool
  dec: Nat
  frac: Nat -> Nat

def c (x : real) : real :=
  let s1 := ∃ N, ∀ n, n >= N -> x.frac n = 9
  have := Classical.propDecidable s1
  if s1 then ⟨x.neg, x.dec + 1, λ n => 0⟩ else x

[Yakov Pechersky]

noncomputable section doesn't also open Classical. So you could also do:

noncomputable section

open Classical

structure real :=
  neg: Bool
  dec: Nat
  frac: Nat -> Nat

def c (x : real) : real :=
  let s1 := ∃ N, ∀ n, n >= N -> x.frac n = 9
  if s1 then ⟨x.neg, x.dec + 1, λ n => 0⟩ else x

[pblpbl]

ok thanks, and where do i get the proof of s1 inside the body of "if s1"? I'd like to apply Nat.find.

edit: found it

def c (x : real) : real :=
  let s1 := ∃ N, ∀ n >= N, x.frac n = 9
  if h : s1 then

[Yakov Pechersky]

import Mathlib.Data.Nat.Find

noncomputable section

open Classical

structure real :=
  neg: Bool
  dec: Nat
  frac: Nat -> Nat

def c (x : real) : real :=
  let s1 := ∃ N, ∀ n, n >= N -> x.frac n = 9
  if h : s1 then ⟨x.neg, x.dec + 1, λ n => Nat.find h⟩ else x