case pos
K : Type u
inst✝ : Field K
x y : RatFunc K
hx : x = 0
⊢ num (x * y) ∣ num x * num y

case neg
K : Type u
inst✝ : Field K
x y : RatFunc K
hx : ¬x = 0
⊢ num (x * y) ∣ num x * num y
K : Type u
inst✝ : Field K
x y : RatFunc K
⊢ num (x * y) ∣ num x * num y
by_cases hx : x = 0
case pos
K : Type u
inst✝ : Field K
x y : RatFunc K
hx : ¬x = 0
hy : y = 0
⊢ num (x * y) ∣ num x * num y

case neg
K : Type u
inst✝ : Field K
x y : RatFunc K
hx : ¬x = 0
hy : ¬y = 0
⊢ num (x * y) ∣ num x * num y
case neg
K : Type u
inst✝ : Field K
x y : RatFunc K
hx : ¬x = 0
⊢ num (x * y) ∣ num x * num y
by_cases hy : y = 0
case neg
K : Type u
inst✝ : Field K
x y : RatFunc K
hx : ¬x = 0
hy : ¬y = 0
⊢ ∃ q hq, x * y = ↑(algebraMap K[X] (RatFunc K)) (num x * num y) / ↑(algebraMap K[X] (RatFunc K)) q
case neg
K : Type u
inst✝ : Field K
x y : RatFunc K
hx : ¬x = 0
hy : ¬y = 0
⊢ num (x * y) ∣ num x * num y
rw [num_dvd (mul_ne_zero (num_ne_zero hx) (num_ne_zero hy))]
case neg
K : Type u
inst✝ : Field K
x y : RatFunc K
hx : ¬x = 0
hy : ¬y = 0
⊢ x * y = ↑(algebraMap K[X] (RatFunc K)) (num x * num y) / ↑(algebraMap K[X] (RatFunc K)) (denom x * denom y)
case neg
K : Type u
inst✝ : Field K
x y : RatFunc K
hx : ¬x = 0
hy : ¬y = 0
⊢ ∃ q hq, x * y = ↑(algebraMap K[X] (RatFunc K)) (num x * num y) / ↑(algebraMap K[X] (RatFunc K)) q
refine' ⟨x.denom * y.denom, mul_ne_zero (denom_ne_zero x) (denom_ne_zero y), _⟩
no goals
case neg
K : Type u
inst✝ : Field K
x y : RatFunc K
hx : ¬x = 0
hy : ¬y = 0
⊢ x * y = ↑(algebraMap K[X] (RatFunc K)) (num x * num y) / ↑(algebraMap K[X] (RatFunc K)) (denom x * denom y)
rw [RingHom.map_mul, RingHom.map_mul, ← div_mul_div_comm, num_div_denom, num_div_denom]
no goals
case pos
K : Type u
inst✝ : Field K
x y : RatFunc K
hx : x = 0
⊢ num (x * y) ∣ num x * num y
simp [hx]
no goals
case pos
K : Type u
inst✝ : Field K
x y : RatFunc K
hx : ¬x = 0
hy : y = 0
⊢ num (x * y) ∣ num x * num y
simp [hy]