K : Type u
inst✝ : Field K
x y : RatFunc K
⊢ ∃ p, x + y = ↑(algebraMap K[X] (RatFunc K)) p / ↑(algebraMap K[X] (RatFunc K)) (denom x * denom y)
K : Type u
inst✝ : Field K
x y : RatFunc K
⊢ denom (x + y) ∣ denom x * denom y
rw [denom_dvd (mul_ne_zero (denom_ne_zero x) (denom_ne_zero y))]
K : Type u
inst✝ : Field K
x y : RatFunc K
⊢ x + y =
    ↑(algebraMap K[X] (RatFunc K)) (num x * denom y + denom x * num y) /
      ↑(algebraMap K[X] (RatFunc K)) (denom x * denom y)
K : Type u
inst✝ : Field K
x y : RatFunc K
⊢ ∃ p, x + y = ↑(algebraMap K[X] (RatFunc K)) p / ↑(algebraMap K[X] (RatFunc K)) (denom x * denom y)
refine' ⟨x.num * y.denom + x.denom * y.num, _⟩
case hb
K : Type u
inst✝ : Field K
x y : RatFunc K
⊢ ↑(algebraMap K[X] (RatFunc K)) (denom x) ≠ 0

case hd
K : Type u
inst✝ : Field K
x y : RatFunc K
⊢ ↑(algebraMap K[X] (RatFunc K)) (denom y) ≠ 0
K : Type u
inst✝ : Field K
x y : RatFunc K
⊢ x + y =
    ↑(algebraMap K[X] (RatFunc K)) (num x * denom y + denom x * num y) /
      ↑(algebraMap K[X] (RatFunc K)) (denom x * denom y)
rw [RingHom.map_mul, RingHom.map_add, RingHom.map_mul, RingHom.map_mul, ← div_add_div,
  num_div_denom, num_div_denom]
no goals
case hb
K : Type u
inst✝ : Field K
x y : RatFunc K
⊢ ↑(algebraMap K[X] (RatFunc K)) (denom x) ≠ 0
exact algebraMap_ne_zero (denom_ne_zero x)
no goals
case hd
K : Type u
inst✝ : Field K
x y : RatFunc K
⊢ ↑(algebraMap K[X] (RatFunc K)) (denom y) ≠ 0
exact algebraMap_ne_zero (denom_ne_zero y)