K : Type u
inst✝ : Field K
x y : RatFunc K
⊢ ↑(algebraMap K[X] (RatFunc K)) (num x) / ↑(algebraMap K[X] (RatFunc K)) (denom x) +
      ↑(algebraMap K[X] (RatFunc K)) (num y) / ↑(algebraMap K[X] (RatFunc K)) (denom 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
⊢ x + y =
    ↑(algebraMap K[X] (RatFunc K)) (num x * denom y + denom x * num y) /
      ↑(algebraMap K[X] (RatFunc K)) (denom x * denom y)
conv_lhs => rw [← num_div_denom x, ← num_div_denom y]
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
⊢ ↑(algebraMap K[X] (RatFunc K)) (num x) / ↑(algebraMap K[X] (RatFunc K)) (denom x) +
      ↑(algebraMap K[X] (RatFunc K)) (num y) / ↑(algebraMap K[X] (RatFunc K)) (denom y) =
    ↑(algebraMap K[X] (RatFunc K)) (num x * denom y + denom x * num y) /
      ↑(algebraMap K[X] (RatFunc K)) (denom x * denom y)
rw [div_add_div, RingHom.map_mul, RingHom.map_add, RingHom.map_mul, RingHom.map_mul]
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)