α : Type u_1
inst✝ : DivisionRing α
σα : OfScientific α
x✝¹ x✝ : ℕ
num✝ : ℤ
denom✝ : ℕ
σh : OfScientific.ofScientific = fun m s e => ↑(Rat.ofScientific m s e)
inv✝ : Invertible ↑denom✝
eq : ↑(mkRat (↑x✝¹) (10 ^ x✝)) = ↑num✝ * ⅟↑denom✝
⊢ ↑(mkRat (↑x✝¹) (10 ^ x✝)) = ↑num✝ * ⅟↑denom✝
α : Type u_1
inst✝ : DivisionRing α
σα : OfScientific α
x✝¹ x✝ : ℕ
num✝ : ℤ
denom✝ : ℕ
σh : OfScientific.ofScientific = fun m s e => ↑(Rat.ofScientific m s e)
inv✝ : Invertible ↑denom✝
eq : ↑(mkRat (↑x✝¹) (10 ^ x✝)) = ↑num✝ * ⅟↑denom✝
⊢ OfScientific.ofScientific x✝¹ true x✝ = ↑num✝ * ⅟↑denom✝
simp only [σh, Rat.ofScientific_true_def]
no goals
α : Type u_1
inst✝ : DivisionRing α
σα : OfScientific α
x✝¹ x✝ : ℕ
num✝ : ℤ
denom✝ : ℕ
σh : OfScientific.ofScientific = fun m s e => ↑(Rat.ofScientific m s e)
inv✝ : Invertible ↑denom✝
eq : ↑(mkRat (↑x✝¹) (10 ^ x✝)) = ↑num✝ * ⅟↑denom✝
⊢ ↑(mkRat (↑x✝¹) (10 ^ x✝)) = ↑num✝ * ⅟↑denom✝
exact eq