K : Type u
inst✝¹ : Field K
L : Type u_1
inst✝ : Field L
f : K →+* L
a : L
x y : RatFunc K
hx : Polynomial.eval₂ f a (denom x) ≠ 0
hy : Polynomial.eval₂ f a (denom y) ≠ 0
⊢ Polynomial.eval₂ f a (num (x * y)) / Polynomial.eval₂ f a (denom (x * y)) =
    Polynomial.eval₂ f a (num x) / Polynomial.eval₂ f a (denom x) *
      (Polynomial.eval₂ f a (num y) / Polynomial.eval₂ f a (denom y))
K : Type u
inst✝¹ : Field K
L : Type u_1
inst✝ : Field L
f : K →+* L
a : L
x y : RatFunc K
hx : Polynomial.eval₂ f a (denom x) ≠ 0
hy : Polynomial.eval₂ f a (denom y) ≠ 0
⊢ eval f a (x * y) = eval f a x * eval f a y
unfold eval
case pos
K : Type u
inst✝¹ : Field K
L : Type u_1
inst✝ : Field L
f : K →+* L
a : L
x y : RatFunc K
hx : Polynomial.eval₂ f a (denom x) ≠ 0
hy : Polynomial.eval₂ f a (denom y) ≠ 0
hxy : Polynomial.eval₂ f a (denom (x * y)) = 0
⊢ Polynomial.eval₂ f a (num (x * y)) / Polynomial.eval₂ f a (denom (x * y)) =
    Polynomial.eval₂ f a (num x) / Polynomial.eval₂ f a (denom x) *
      (Polynomial.eval₂ f a (num y) / Polynomial.eval₂ f a (denom y))

case neg
K : Type u
inst✝¹ : Field K
L : Type u_1
inst✝ : Field L
f : K →+* L
a : L
x y : RatFunc K
hx : Polynomial.eval₂ f a (denom x) ≠ 0
hy : Polynomial.eval₂ f a (denom y) ≠ 0
hxy : ¬Polynomial.eval₂ f a (denom (x * y)) = 0
⊢ Polynomial.eval₂ f a (num (x * y)) / Polynomial.eval₂ f a (denom (x * y)) =
    Polynomial.eval₂ f a (num x) / Polynomial.eval₂ f a (denom x) *
      (Polynomial.eval₂ f a (num y) / Polynomial.eval₂ f a (denom y))
K : Type u
inst✝¹ : Field K
L : Type u_1
inst✝ : Field L
f : K →+* L
a : L
x y : RatFunc K
hx : Polynomial.eval₂ f a (denom x) ≠ 0
hy : Polynomial.eval₂ f a (denom y) ≠ 0
⊢ Polynomial.eval₂ f a (num (x * y)) / Polynomial.eval₂ f a (denom (x * y)) =
    Polynomial.eval₂ f a (num x) / Polynomial.eval₂ f a (denom x) *
      (Polynomial.eval₂ f a (num y) / Polynomial.eval₂ f a (denom y))
by_cases hxy : Polynomial.eval₂ f a (denom (x * y)) = 0
case neg
K : Type u
inst✝¹ : Field K
L : Type u_1
inst✝ : Field L
f : K →+* L
a : L
x y : RatFunc K
hx : Polynomial.eval₂ f a (denom x) ≠ 0
hy : Polynomial.eval₂ f a (denom y) ≠ 0
hxy : ¬Polynomial.eval₂ f a (denom (x * y)) = 0
⊢ Polynomial.eval₂ f a (num (x * y)) * (Polynomial.eval₂ f a (denom x) * Polynomial.eval₂ f a (denom y)) =
    Polynomial.eval₂ f a (num x) * Polynomial.eval₂ f a (num y) * Polynomial.eval₂ f a (denom (x * y))
case neg
K : Type u
inst✝¹ : Field K
L : Type u_1
inst✝ : Field L
f : K →+* L
a : L
x y : RatFunc K
hx : Polynomial.eval₂ f a (denom x) ≠ 0
hy : Polynomial.eval₂ f a (denom y) ≠ 0
hxy : ¬Polynomial.eval₂ f a (denom (x * y)) = 0
⊢ Polynomial.eval₂ f a (num (x * y)) / Polynomial.eval₂ f a (denom (x * y)) =
    Polynomial.eval₂ f a (num x) / Polynomial.eval₂ f a (denom x) *
      (Polynomial.eval₂ f a (num y) / Polynomial.eval₂ f a (denom y))
rw [div_mul_div_comm, eq_div_iff (mul_ne_zero hx hy), div_eq_mul_inv, mul_right_comm, ←
  div_eq_mul_inv, div_eq_iff hxy]
case neg
K : Type u
inst✝¹ : Field K
L : Type u_1
inst✝ : Field L
f : K →+* L
a : L
x y : RatFunc K
hx : Polynomial.eval₂ f a (denom x) ≠ 0
hy : Polynomial.eval₂ f a (denom y) ≠ 0
hxy : ¬Polynomial.eval₂ f a (denom (x * y)) = 0
⊢ Polynomial.eval₂ f a (num (x * y) * (denom x * denom y)) = Polynomial.eval₂ f a (num x * num y * denom (x * y))
case neg
K : Type u
inst✝¹ : Field K
L : Type u_1
inst✝ : Field L
f : K →+* L
a : L
x y : RatFunc K
hx : Polynomial.eval₂ f a (denom x) ≠ 0
hy : Polynomial.eval₂ f a (denom y) ≠ 0
hxy : ¬Polynomial.eval₂ f a (denom (x * y)) = 0
⊢ Polynomial.eval₂ f a (num (x * y)) * (Polynomial.eval₂ f a (denom x) * Polynomial.eval₂ f a (denom y)) =
    Polynomial.eval₂ f a (num x) * Polynomial.eval₂ f a (num y) * Polynomial.eval₂ f a (denom (x * y))
simp only [← Polynomial.eval₂_mul]
case neg.e_p
K : Type u
inst✝¹ : Field K
L : Type u_1
inst✝ : Field L
f : K →+* L
a : L
x y : RatFunc K
hx : Polynomial.eval₂ f a (denom x) ≠ 0
hy : Polynomial.eval₂ f a (denom y) ≠ 0
hxy : ¬Polynomial.eval₂ f a (denom (x * y)) = 0
⊢ num (x * y) * (denom x * denom y) = num x * num y * denom (x * y)
case neg
K : Type u
inst✝¹ : Field K
L : Type u_1
inst✝ : Field L
f : K →+* L
a : L
x y : RatFunc K
hx : Polynomial.eval₂ f a (denom x) ≠ 0
hy : Polynomial.eval₂ f a (denom y) ≠ 0
hxy : ¬Polynomial.eval₂ f a (denom (x * y)) = 0
⊢ Polynomial.eval₂ f a (num (x * y) * (denom x * denom y)) = Polynomial.eval₂ f a (num x * num y * denom (x * y))
congr 1
no goals
case neg.e_p
K : Type u
inst✝¹ : Field K
L : Type u_1
inst✝ : Field L
f : K →+* L
a : L
x y : RatFunc K
hx : Polynomial.eval₂ f a (denom x) ≠ 0
hy : Polynomial.eval₂ f a (denom y) ≠ 0
hxy : ¬Polynomial.eval₂ f a (denom (x * y)) = 0
⊢ num (x * y) * (denom x * denom y) = num x * num y * denom (x * y)
apply num_denom_mul
case pos
K : Type u
inst✝¹ : Field K
L : Type u_1
inst✝ : Field L
f : K →+* L
a : L
x y : RatFunc K
hx : Polynomial.eval₂ f a (denom x) ≠ 0
hy : Polynomial.eval₂ f a (denom y) ≠ 0
hxy : Polynomial.eval₂ f a (denom (x * y)) = 0
this : Polynomial.eval₂ f a (denom x * denom y) = 0
⊢ Polynomial.eval₂ f a (num (x * y)) / Polynomial.eval₂ f a (denom (x * y)) =
    Polynomial.eval₂ f a (num x) / Polynomial.eval₂ f a (denom x) *
      (Polynomial.eval₂ f a (num y) / Polynomial.eval₂ f a (denom y))
case pos
K : Type u
inst✝¹ : Field K
L : Type u_1
inst✝ : Field L
f : K →+* L
a : L
x y : RatFunc K
hx : Polynomial.eval₂ f a (denom x) ≠ 0
hy : Polynomial.eval₂ f a (denom y) ≠ 0
hxy : Polynomial.eval₂ f a (denom (x * y)) = 0
⊢ Polynomial.eval₂ f a (num (x * y)) / Polynomial.eval₂ f a (denom (x * y)) =
    Polynomial.eval₂ f a (num x) / Polynomial.eval₂ f a (denom x) *
      (Polynomial.eval₂ f a (num y) / Polynomial.eval₂ f a (denom y))
have := Polynomial.eval₂_eq_zero_of_dvd_of_eval₂_eq_zero f a (denom_mul_dvd x y) hxy
case pos
K : Type u
inst✝¹ : Field K
L : Type u_1
inst✝ : Field L
f : K →+* L
a : L
x y : RatFunc K
hx : Polynomial.eval₂ f a (denom x) ≠ 0
hy : Polynomial.eval₂ f a (denom y) ≠ 0
hxy : Polynomial.eval₂ f a (denom (x * y)) = 0
this : Polynomial.eval₂ f a (denom x) * Polynomial.eval₂ f a (denom y) = 0
⊢ Polynomial.eval₂ f a (num (x * y)) / Polynomial.eval₂ f a (denom (x * y)) =
    Polynomial.eval₂ f a (num x) / Polynomial.eval₂ f a (denom x) *
      (Polynomial.eval₂ f a (num y) / Polynomial.eval₂ f a (denom y))
case pos
K : Type u
inst✝¹ : Field K
L : Type u_1
inst✝ : Field L
f : K →+* L
a : L
x y : RatFunc K
hx : Polynomial.eval₂ f a (denom x) ≠ 0
hy : Polynomial.eval₂ f a (denom y) ≠ 0
hxy : Polynomial.eval₂ f a (denom (x * y)) = 0
this : Polynomial.eval₂ f a (denom x * denom y) = 0
⊢ Polynomial.eval₂ f a (num (x * y)) / Polynomial.eval₂ f a (denom (x * y)) =
    Polynomial.eval₂ f a (num x) / Polynomial.eval₂ f a (denom x) *
      (Polynomial.eval₂ f a (num y) / Polynomial.eval₂ f a (denom y))
rw [Polynomial.eval₂_mul] at this
no goals
case pos
K : Type u
inst✝¹ : Field K
L : Type u_1
inst✝ : Field L
f : K →+* L
a : L
x y : RatFunc K
hx : Polynomial.eval₂ f a (denom x) ≠ 0
hy : Polynomial.eval₂ f a (denom y) ≠ 0
hxy : Polynomial.eval₂ f a (denom (x * y)) = 0
this : Polynomial.eval₂ f a (denom x) * Polynomial.eval₂ f a (denom y) = 0
⊢ Polynomial.eval₂ f a (num (x * y)) / Polynomial.eval₂ f a (denom (x * y)) =
    Polynomial.eval₂ f a (num x) / Polynomial.eval₂ f a (denom x) *
      (Polynomial.eval₂ f a (num y) / Polynomial.eval₂ f a (denom y))
cases mul_eq_zero.mp this <;> contradiction