α : Type u_1
inst✝ : DivisionRing α
σα : OfScientific α
n✝¹ n✝ x✝ : ℕ
σh : OfScientific.ofScientific = fun m s e => ↑(Rat.ofScientific m s e)
h : x✝ = Nat.mul n✝¹ (10 ^ n✝)
⊢ ↑(↑n✝¹ * 10 ^ n✝) = ↑n✝¹ * 10 ^ n✝
α : Type u_1
inst✝ : DivisionRing α
σα : OfScientific α
n✝¹ n✝ x✝ : ℕ
σh : OfScientific.ofScientific = fun m s e => ↑(Rat.ofScientific m s e)
h : x✝ = Nat.mul n✝¹ (10 ^ n✝)
⊢ OfScientific.ofScientific (↑n✝¹) false ↑n✝ = ↑x✝
simp [σh, Rat.ofScientific_false_def, h]
no goals
α : Type u_1
inst✝ : DivisionRing α
σα : OfScientific α
n✝¹ n✝ x✝ : ℕ
σh : OfScientific.ofScientific = fun m s e => ↑(Rat.ofScientific m s e)
h : x✝ = Nat.mul n✝¹ (10 ^ n✝)
⊢ ↑(↑n✝¹ * 10 ^ n✝) = ↑n✝¹ * 10 ^ n✝
norm_cast