let bQ := (b : ℚ)
ℕ ℤ ℚ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Subtraction ℚ
inst✝⁴ : Reciprocation ℚ
inst✝³ : Division ℚ
inst✝² : Sign ℚ
a b c d : ℤ
inst✝¹ : Integer.Nonzero b
inst✝ : Integer.Nonzero d
aQ : ℚ := from_integer a
⊢ from_integer a / from_integer b + from_integer c / from_integer d ≃
    from_integer (a * d + b * c) / from_integer (b * d)
ℕ ℤ ℚ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Subtraction ℚ
inst✝⁴ : Reciprocation ℚ
inst✝³ : Division ℚ
inst✝² : Sign ℚ
a b c d : ℤ
inst✝¹ : Integer.Nonzero b
inst✝ : Integer.Nonzero d
aQ : ℚ := from_integer a
bQ : ℚ := from_integer b
⊢ from_integer a / from_integer b + from_integer c / from_integer d ≃
    from_integer (a * d + b * c) / from_integer (b * d)