-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
k : Type y
inst : Field R
p q : R[X]
inst_1 : Field k
f : R →+* k
hq0 : ¬q = 0
rw :
  map f
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])
        (p /ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]))) =
    map f p / map f q
rw₁ :
  map f
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])
        (p /ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]))) =
    HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) (map f q).leadingCoeff⁻¹ : k[X])
      (map f p /ₘ HMul.hMul (β := k[X]) (map f q) ((C : (a : k) → k[X]) (map f q).leadingCoeff⁻¹ : k[X]))
rw₂ :
  map f ((C : (a : R) → R[X]) q.leadingCoeff⁻¹) *
      map f (p /ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])) =
    HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) (map f q).leadingCoeff⁻¹ : k[X])
      (map f p /ₘ HMul.hMul (β := k[X]) (map f q) ((C : (a : k) → k[X]) (map f q).leadingCoeff⁻¹ : k[X]))
rw₃ :
  map f ((C : (a : R) → R[X]) q.leadingCoeff⁻¹) *
      (map f p /ₘ map f (HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]))) =
    HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) (map f q).leadingCoeff⁻¹ : k[X])
      (map f p /ₘ HMul.hMul (β := k[X]) (map f q) ((C : (a : k) → k[X]) (map f q).leadingCoeff⁻¹ : k[X]))
rw₄ :
  map f ((C : (a : R) → R[X]) q.leadingCoeff⁻¹) *
      (map f p /ₘ (map f q * map f ((C : (a : R) → R[X]) q.leadingCoeff⁻¹))) =
    HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) (map f q).leadingCoeff⁻¹ : k[X])
      (map f p /ₘ HMul.hMul (β := k[X]) (map f q) ((C : (a : k) → k[X]) (map f q).leadingCoeff⁻¹ : k[X]))
rw₅ :
  HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) ((f : (a : R) → k) q.leadingCoeff⁻¹) : k[X])
      (map f p /ₘ HMul.hMul (β := k[X]) (map f q) ((C : (a : k) → k[X]) ((f : (a : R) → k) q.leadingCoeff⁻¹) : k[X])) =
    HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) (map f q).leadingCoeff⁻¹ : k[X])
      (map f p /ₘ HMul.hMul (β := k[X]) (map f q) ((C : (a : k) → k[X]) (map f q).leadingCoeff⁻¹ : k[X]))
rw₆ :
  HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) ((f : (a : R) → k) q.leadingCoeff⁻¹) : k[X])
      (map f p /ₘ HMul.hMul (β := k[X]) (map f q) ((C : (a : k) → k[X]) ((f : (a : R) → k) q.leadingCoeff⁻¹) : k[X])) =
    HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) ((f : (a : R) → k) q.leadingCoeff)⁻¹ : k[X])
      (map f p /ₘ HMul.hMul (β := k[X]) (map f q) ((C : (a : k) → k[X]) ((f : (a : R) → k) q.leadingCoeff)⁻¹ : k[X]))
rw₇ rw₈ :
  HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) ((f : (a : R) → k) q.leadingCoeff)⁻¹ : k[X])
      (map f p /ₘ HMul.hMul (β := k[X]) (map f q) ((C : (a : k) → k[X]) ((f : (a : R) → k) q.leadingCoeff)⁻¹ : k[X])) =
    HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) ((f : (a : R) → k) q.leadingCoeff)⁻¹ : k[X])
      (map f p /ₘ HMul.hMul (β := k[X]) (map f q) ((C : (a : k) → k[X]) ((f : (a : R) → k) q.leadingCoeff)⁻¹ : k[X]))
⊢ map f (p / q) = map f p / map f q

Tactic:
rw [div_def, div_def, Polynomial.map_mul, map_divByMonic f (monic_mul_leadingCoeff_inv hq0),
      Polynomial.map_mul, map_C, leadingCoeff_map, map_inv₀]

Premises used: Polynomial.div_def, Polynomial.map_mul, map_inv₀, Polynomial.monic_mul_leadingCoeff_inv, Polynomial.leadingCoeff_map, Polynomial.map_C, Polynomial.map_divByMonic