-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
f :
  ∀ (p q : K[X]) (hq : q ≠ 0),
    HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯)
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯)
            (HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p : K⟮X⟯)
                ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯)).num :
          K⟮X⟯)
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯)
            (HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p : K⟮X⟯)
                ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯)).denom :
          K⟮X⟯) =
      HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p : K⟮X⟯)
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯)
f₁ :
  ∀ (p q : K[X]) (hq : q ≠ 0) (q_div_ne_zero : q / @gcd _ CommSemiring.toCommMonoidWithZero _ p q ≠ 0),
    HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯)
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯)
            (HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p : K⟮X⟯)
                ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯)).num :
          K⟮X⟯)
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯)
            (HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p : K⟮X⟯)
                ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯)).denom :
          K⟮X⟯) =
      HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p : K⟮X⟯)
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯)
f₂ :
  ∀ (p q : K[X]) (hq : q ≠ 0) (q_div_ne_zero : q / @gcd _ CommSemiring.toCommMonoidWithZero _ p q ≠ 0),
    @gcd _ CommSemiring.toCommMonoidWithZero _ p q ∣ q
f₃ :
  ∀ (p q : K[X]) (hq : q ≠ 0) (q_div_ne_zero : q / @gcd _ CommSemiring.toCommMonoidWithZero _ p q ≠ 0),
    @gcd _ CommSemiring.toCommMonoidWithZero _ p q ∣ p
f₄ :
  ∀ (p q : K[X]) (hq : q ≠ 0) (q_div_ne_zero : q / @gcd _ CommSemiring.toCommMonoidWithZero _ p q ≠ 0),
    Ne (α := K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (q / @gcd _ CommSemiring.toCommMonoidWithZero _ p q) : K⟮X⟯)
      (0 : K⟮X⟯)
f₅ :
  ∀ (p q : K[X]) (hq : q ≠ 0) (q_div_ne_zero : q / @gcd _ CommSemiring.toCommMonoidWithZero _ p q ≠ 0),
    Ne (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯) (0 : K⟮X⟯)
f₆ :
  ∀ (p q : K[X]) (hq : q ≠ 0) (q_div_ne_zero : q / @gcd _ CommSemiring.toCommMonoidWithZero _ p q ≠ 0),
    Ne (α := K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯)
          ((C : (a : K) → K[X]) (q / @gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff⁻¹) :
        K⟮X⟯)
      (0 : K⟮X⟯)
f₇ :
  ∀ (p q : K[X]) (hq : q ≠ 0) (q_div_ne_zero : q / @gcd _ CommSemiring.toCommMonoidWithZero _ p q ≠ 0),
    @gcd _ CommSemiring.toCommMonoidWithZero _ p q ∣ p
f₈ :
  ∀ (p q : K[X]) (hq : q ≠ 0) (q_div_ne_zero : q / @gcd _ CommSemiring.toCommMonoidWithZero _ p q ≠ 0),
    Ne (α := K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (q / @gcd _ CommSemiring.toCommMonoidWithZero _ p q) : K⟮X⟯)
      (0 : K⟮X⟯)
f₉ :
  ∀ (p q : K[X]) (hq : q ≠ 0) (q_div_ne_zero : q / @gcd _ CommSemiring.toCommMonoidWithZero _ p q ≠ 0),
    Ne (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯) (0 : K⟮X⟯)
f₁₀ :
  ∀ (p q : K[X]) (hq : q ≠ 0) (q_div_ne_zero : q / @gcd _ CommSemiring.toCommMonoidWithZero _ p q ≠ 0),
    Ne (α := K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯)
          ((C : (a : K) → K[X]) (q / @gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff⁻¹) :
        K⟮X⟯)
      (0 : K⟮X⟯)
f₁₁ :
  ∀ (p q : K[X]) (hq : q ≠ 0) (q_div_ne_zero : q / @gcd _ CommSemiring.toCommMonoidWithZero _ p q ≠ 0),
    Ne (α := K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (q / @gcd _ CommSemiring.toCommMonoidWithZero _ p q) : K⟮X⟯)
      (0 : K⟮X⟯)
f₁₂ :
  ∀ (p q : K[X]) (hq : q ≠ 0) (q_div_ne_zero : q / @gcd _ CommSemiring.toCommMonoidWithZero _ p q ≠ 0),
    Ne (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯) (0 : K⟮X⟯)
f₁₃ :
  ∀ (p q : K[X]) (hq : q ≠ 0) (q_div_ne_zero : q / @gcd _ CommSemiring.toCommMonoidWithZero _ p q ≠ 0),
    Ne (α := K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯)
          ((C : (a : K) → K[X]) (q / @gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff⁻¹) :
        K⟮X⟯)
      (0 : K⟮X⟯)
f₁₄ :
  ∀ (p q : K[X]) (hq : q ≠ 0) (q_div_ne_zero : q / @gcd _ CommSemiring.toCommMonoidWithZero _ p q ≠ 0),
    Ne (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯) (0 : K⟮X⟯)
f₁₅ f₁₆ :
  ∀ (p q : K[X]) (hq : q ≠ 0) (q_div_ne_zero : q / @gcd _ CommSemiring.toCommMonoidWithZero _ p q ≠ 0),
    Ne (α := K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯)
          ((C : (a : K) → K[X]) (q / @gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff⁻¹) :
        K⟮X⟯)
      (0 : K⟮X⟯)
⊢ HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.num : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.denom : K⟮X⟯) =
    x

Tactic:
classical
  induction x using RatFunc.induction_on with | _ p q hq
  have q_div_ne_zero : q / gcd p q ≠ 0 := right_div_gcd_ne_zero hq
  rw [num_div p q, denom_div p hq, map_mul, map_mul, mul_div_mul_left,
    div_eq_div_iff, ← map_mul, ← map_mul, mul_comm _ q, ←
    EuclideanDomain.mul_div_assoc, ← EuclideanDomain.mul_div_assoc, mul_comm]
  · apply gcd_dvd_right
  · apply gcd_dvd_left
  · exact algebraMap_ne_zero q_div_ne_zero
  · exact algebraMap_ne_zero hq
  · refine algebraMap_ne_zero (mt Polynomial.C_eq_zero.mp ?_)
    exact inv_ne_zero (Polynomial.leadingCoeff_ne_zero.mpr q_div_ne_zero)

Premises used: Polynomial.C_eq_zero, RatFunc.algebraMap_ne_zero, mt, div_eq_div_iff, EuclideanDomain.mul_div_assoc, map_mul, RatFunc.induction_on, Iff.mp, mul_div_mul_left, mul_comm, GCDMonoid.gcd_dvd_left, GCDMonoid.gcd_dvd_right