-- Mathlib/FieldTheory/RatFunc/AsPolynomial.lean
theorem eval_mul {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

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

Tactic:
rw [← Polynomial.eval₂_mul]

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

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

Tactic:
by_cases hxy : Polynomial.eval₂ f a (denom (x * y)) = 0

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

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

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

Tactic:
rw [Polynomial.eval₂_mul] at this

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

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

Tactic:
congr 1

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

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

Tactic:
repeat' rw [← Polynomial.eval₂_mul]

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

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

Tactic:
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]

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

Proof state:
case neg.e_p
K : Type u
inst✝¹ : Field K
L : Type u
inst✝ : Field L
f : K →+* L
a : L
x y : RatFunc K
hx : Polynomial.eval₂ f a x.denom ≠ 0
hy : Polynomial.eval₂ f a y.denom ≠ 0
hxy : ¬Polynomial.eval₂ f a (x * y).denom = 0
⊢ (x * y).num * (x.denom * y.denom) = x.num * y.num * (x * y).denom

Tactic:
apply num_denom_mul

Result:
no goals

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

Tactic:
cases mul_eq_zero.mp this <;> contradiction

Result:
no goals

Proof state:
K : Type u
inst✝¹ : Field K
L : Type u
inst✝ : Field L
f : K →+* L
a : L
x y : RatFunc K
hx : Polynomial.eval₂ f a x.denom ≠ 0
hy : Polynomial.eval₂ f a y.denom ≠ 0
⊢ eval f a (x * y) = eval f a x * eval f a y

Tactic:
unfold eval

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