exact AsRatio.intro n d ‹Integer.Nonzero d› ‹b ≃ n / d›
ℕ ℤ : Type
inst✝⁷ : Natural ℕ
inst✝⁶ : Integer ℤ
ℚ : Type
inst✝⁵ : Core ℚ
inst✝⁴ : Addition ℚ
inst✝³ : Multiplication ℚ
inst✝² : Negation ℚ
inst✝¹ : Reciprocation ℚ
inst✝ : Division ℚ
a b : ℚ
x✝¹ : a ≃ b
x✝ : AsRatio a
n d : ℤ
b_nonzero✝ : Integer.Nonzero d
eqv this✝ : a ≃ from_integer n / from_integer d
this : b ≃ from_integer n / from_integer d
⊢ AsRatio b
no goals