-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
p q a : K[X]
hq : q ≠ 0
ha : a ≠ 0
ha' : a.leadingCoeff ≠ 0
hainv : a.leadingCoeff⁻¹ ≠ 0
hdeg : (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).degree ≤ q.degree
hdeg' :
  (HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) a.leadingCoeff⁻¹ : K[X])
        (@gcd _ CommSemiring.toCommMonoidWithZero _ p q)).degree ≤
    q.degree
hdivp :
  HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) a.leadingCoeff⁻¹ : K[X])
      (@gcd _ CommSemiring.toCommMonoidWithZero _ p q) ∣
    p
hdivq :
  HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) a.leadingCoeff⁻¹ : K[X])
      (@gcd _ CommSemiring.toCommMonoidWithZero _ p q) ∣
    q
rw :
  HMul.hMul (α := K[X])
        ((C : (a : K) → K[X])
            ((q.leadingCoeff / (a.leadingCoeff⁻¹ * (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff))⁻¹ *
              a.leadingCoeff⁻¹⁻¹) :
          K[X])
        (p / @gcd _ CommSemiring.toCommMonoidWithZero _ p q) =
      HMul.hMul (α := K[X])
        ((C : (a : K) → K[X]) (q.leadingCoeff / (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff)⁻¹ : K[X])
        (p / @gcd _ CommSemiring.toCommMonoidWithZero _ p q) ∧
    HMul.hMul (α := K[X])
        ((C : (a : K) → K[X])
            ((q.leadingCoeff / (a.leadingCoeff⁻¹ * (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff))⁻¹ *
              a.leadingCoeff⁻¹⁻¹) :
          K[X])
        (q / @gcd _ CommSemiring.toCommMonoidWithZero _ p q) =
      HMul.hMul (α := K[X])
        ((C : (a : K) → K[X]) (q.leadingCoeff / (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff)⁻¹ : K[X])
        (q / @gcd _ CommSemiring.toCommMonoidWithZero _ p q)
⊢ HMul.hMul (α := K[X])
        ((C : (a : K) → K[X])
            (a * q /
                  (a *
                    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) a.leadingCoeff⁻¹ : K[X])
                      (@gcd _ CommSemiring.toCommMonoidWithZero _ p q))).leadingCoeff⁻¹ :
          K[X])
        (a * p /
          (a *
            HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) a.leadingCoeff⁻¹ : K[X])
              (@gcd _ CommSemiring.toCommMonoidWithZero _ p q))) =
      HMul.hMul (α := K[X])
        ((C : (a : K) → K[X]) (q / @gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff⁻¹ : K[X])
        (p / @gcd _ CommSemiring.toCommMonoidWithZero _ p q) ∧
    HMul.hMul (α := K[X])
        ((C : (a : K) → K[X])
            (a * q /
                  (a *
                    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) a.leadingCoeff⁻¹ : K[X])
                      (@gcd _ CommSemiring.toCommMonoidWithZero _ p q))).leadingCoeff⁻¹ :
          K[X])
        (a * q /
          (a *
            HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) a.leadingCoeff⁻¹ : K[X])
              (@gcd _ CommSemiring.toCommMonoidWithZero _ p q))) =
      HMul.hMul (α := K[X])
        ((C : (a : K) → K[X]) (q / @gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff⁻¹ : K[X])
        (q / @gcd _ CommSemiring.toCommMonoidWithZero _ p q)

Tactic:
rw [EuclideanDomain.mul_div_mul_cancel ha hdivp, EuclideanDomain.mul_div_mul_cancel ha hdivq,
        leadingCoeff_div hdeg, leadingCoeff_div hdeg', Polynomial.leadingCoeff_mul,
        Polynomial.leadingCoeff_C, div_C_mul, div_C_mul, ← mul_assoc, ← Polynomial.C_mul, ←
        mul_assoc, ← Polynomial.C_mul]

Premises used: Polynomial.leadingCoeff_mul, mul_assoc, EuclideanDomain.mul_div_mul_cancel, Polynomial.C_mul, Polynomial.leadingCoeff_div, Polynomial.leadingCoeff_C, Polynomial.div_C_mul