-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
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
⊢ 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)
have 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)
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]