case false
m e : Nat
⊢ Rat.ofScientific m false e = if false = true then mkRat (↑m) (10 ^ e) else ↑↑(m * 10 ^ e)

case true
m e : Nat
⊢ Rat.ofScientific m true e = if true = true then mkRat (↑m) (10 ^ e) else ↑↑(m * 10 ^ e)
m : Nat
s : Bool
e : Nat
⊢ Rat.ofScientific m s e = if s = true then mkRat (↑m) (10 ^ e) else ↑↑(m * 10 ^ e)
cases s
case true
m e : Nat
⊢ Rat.ofScientific m true e = if true = true then mkRat (↑m) (10 ^ e) else ↑↑(m * 10 ^ e)
case false
m e : Nat
⊢ Rat.ofScientific m false e = if false = true then mkRat (↑m) (10 ^ e) else ↑↑(m * 10 ^ e)

case true
m e : Nat
⊢ Rat.ofScientific m true e = if true = true then mkRat (↑m) (10 ^ e) else ↑↑(m * 10 ^ e)
exact ofScientific_false_def
no goals
case true
m e : Nat
⊢ Rat.ofScientific m true e = if true = true then mkRat (↑m) (10 ^ e) else ↑↑(m * 10 ^ e)
exact ofScientific_true_def