awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K_1 : Type u
inst : CommRing K_1
inst_1 : IsDomain K_1
A : Type u_1
k : Type u_2
K : Type u_3
inst_2 : CommRing A
inst_3 : IsDomain A
inst_4 : Field k
inst_5 : Field K
inst_6 : Algebra.{u_1, u_2} A[X] k
inst_7 : Algebra.{u_1, u_3} A[X] K
inst_8 : SMul k K
inst_9 : FaithfulSMul.{u_1, u_2} A[X] k
inst_10 : FaithfulSMul.{u_1, u_3} A[X] K
inst_11 : IsScalarTower.{u_1, u_2, u_3} A[X] k K
b : k
c : K
p q : A[X]
hq : q ≠ 0
f :
  q •
      (HDiv.hDiv (α := A⟮X⟯) (β := A⟮X⟯) ((algebraMap A[X] A⟮X⟯ : (a : A[X]) → A⟮X⟯) p : A⟮X⟯)
            ((algebraMap A[X] A⟮X⟯ : (a : A[X]) → A⟮X⟯) q : A⟮X⟯) •
          b) •
        c =
    q •
      HDiv.hDiv (α := A⟮X⟯) (β := A⟮X⟯) ((algebraMap A[X] A⟮X⟯ : (a : A[X]) → A⟮X⟯) p : A⟮X⟯)
          ((algebraMap A[X] A⟮X⟯ : (a : A[X]) → A⟮X⟯) q : A⟮X⟯) •
        b • c
⊢ (HDiv.hDiv (α := A⟮X⟯) (β := A⟮X⟯) ((algebraMap A[X] A⟮X⟯ : (a : A[X]) → A⟮X⟯) p : A⟮X⟯)
          ((algebraMap A[X] A⟮X⟯ : (a : A[X]) → A⟮X⟯) q : A⟮X⟯) •
        b) •
      c =
    HDiv.hDiv (α := A⟮X⟯) (β := A⟮X⟯) ((algebraMap A[X] A⟮X⟯ : (a : A[X]) → A⟮X⟯) p : A⟮X⟯)
        ((algebraMap A[X] A⟮X⟯ : (a : A[X]) → A⟮X⟯) q : A⟮X⟯) •
      b • c

Tactic:
rw [← smul_right_inj hq]

Premises used: smul_right_inj
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K_1 : Type u
inst : CommRing K_1
inst_1 : IsDomain K_1
A : Type u_1
k : Type u_2
K : Type u_3
inst_2 : CommRing A
inst_3 : IsDomain A
inst_4 : Field k
inst_5 : Field K
inst_6 : Algebra.{u_1, u_2} A[X] k
inst_7 : Algebra.{u_1, u_3} A[X] K
inst_8 : SMul k K
inst_9 : FaithfulSMul.{u_1, u_2} A[X] k
inst_10 : FaithfulSMul.{u_1, u_3} A[X] K
inst_11 : IsScalarTower.{u_1, u_2, u_3} A[X] k K
b : k
c : K
p q : A[X]
hq : q ≠ 0
f :
  (HMul.hMul (α := A⟮X⟯) ((algebraMap A[X] A⟮X⟯ : (a : A[X]) → A⟮X⟯) q : A⟮X⟯)
          (HDiv.hDiv (α := A⟮X⟯) (β := A⟮X⟯) ((algebraMap A[X] A⟮X⟯ : (a : A[X]) → A⟮X⟯) p : A⟮X⟯)
            ((algebraMap A[X] A⟮X⟯ : (a : A[X]) → A⟮X⟯) q : A⟮X⟯)) •
        b) •
      c =
    HMul.hMul (α := A⟮X⟯) ((algebraMap A[X] A⟮X⟯ : (a : A[X]) → A⟮X⟯) q : A⟮X⟯)
        (HDiv.hDiv (α := A⟮X⟯) (β := A⟮X⟯) ((algebraMap A[X] A⟮X⟯ : (a : A[X]) → A⟮X⟯) p : A⟮X⟯)
          ((algebraMap A[X] A⟮X⟯ : (a : A[X]) → A⟮X⟯) q : A⟮X⟯)) •
      b • c
⊢ q •
      (HDiv.hDiv (α := A⟮X⟯) (β := A⟮X⟯) ((algebraMap A[X] A⟮X⟯ : (a : A[X]) → A⟮X⟯) p : A⟮X⟯)
            ((algebraMap A[X] A⟮X⟯ : (a : A[X]) → A⟮X⟯) q : A⟮X⟯) •
          b) •
        c =
    q •
      HDiv.hDiv (α := A⟮X⟯) (β := A⟮X⟯) ((algebraMap A[X] A⟮X⟯ : (a : A[X]) → A⟮X⟯) p : A⟮X⟯)
          ((algebraMap A[X] A⟮X⟯ : (a : A[X]) → A⟮X⟯) q : A⟮X⟯) •
        b • c

Tactic:
simp_rw [← smul_assoc, Algebra.smul_def q]

Premises used: smul_assoc, Algebra.smul_def
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K_1 : Type u
inst : CommRing K_1
inst_1 : IsDomain K_1
A : Type u_1
k : Type u_2
K : Type u_3
inst_2 : CommRing A
inst_3 : IsDomain A
inst_4 : Field k
inst_5 : Field K
inst_6 : Algebra.{u_1, u_2} A[X] k
inst_7 : Algebra.{u_1, u_3} A[X] K
inst_8 : SMul k K
inst_9 : FaithfulSMul.{u_1, u_2} A[X] k
inst_10 : FaithfulSMul.{u_1, u_3} A[X] K
inst_11 : IsScalarTower.{u_1, u_2, u_3} A[X] k K
b : k
c : K
p q : A[X]
hq : q ≠ 0
f :
  HSMul.hSMul (α := A⟮X⟯) ((algebraMap A[X] A⟮X⟯ : (a : A[X]) → A⟮X⟯) p : A⟮X⟯) b • c =
    HSMul.hSMul (α := A⟮X⟯) ((algebraMap A[X] A⟮X⟯ : (a : A[X]) → A⟮X⟯) p : A⟮X⟯) (b • c)
⊢ (HMul.hMul (α := A⟮X⟯) ((algebraMap A[X] A⟮X⟯ : (a : A[X]) → A⟮X⟯) q : A⟮X⟯)
          (HDiv.hDiv (α := A⟮X⟯) (β := A⟮X⟯) ((algebraMap A[X] A⟮X⟯ : (a : A[X]) → A⟮X⟯) p : A⟮X⟯)
            ((algebraMap A[X] A⟮X⟯ : (a : A[X]) → A⟮X⟯) q : A⟮X⟯)) •
        b) •
      c =
    HMul.hMul (α := A⟮X⟯) ((algebraMap A[X] A⟮X⟯ : (a : A[X]) → A⟮X⟯) q : A⟮X⟯)
        (HDiv.hDiv (α := A⟮X⟯) (β := A⟮X⟯) ((algebraMap A[X] A⟮X⟯ : (a : A[X]) → A⟮X⟯) p : A⟮X⟯)
          ((algebraMap A[X] A⟮X⟯ : (a : A[X]) → A⟮X⟯) q : A⟮X⟯)) •
      b • c

Tactic:
field_simp [hq]
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K_1 : Type u
inst : CommRing K_1
inst_1 : IsDomain K_1
A : Type u_1
k : Type u_2
K : Type u_3
inst_2 : CommRing A
inst_3 : IsDomain A
inst_4 : Field k
inst_5 : Field K
inst_6 : Algebra.{u_1, u_2} A[X] k
inst_7 : Algebra.{u_1, u_3} A[X] K
inst_8 : SMul k K
inst_9 : FaithfulSMul.{u_1, u_2} A[X] k
inst_10 : FaithfulSMul.{u_1, u_3} A[X] K
inst_11 : IsScalarTower.{u_1, u_2, u_3} A[X] k K
b : k
c : K
p q : A[X]
hq : q ≠ 0
⊢ HSMul.hSMul (α := A⟮X⟯) ((algebraMap A[X] A⟮X⟯ : (a : A[X]) → A⟮X⟯) p : A⟮X⟯) b • c =
    HSMul.hSMul (α := A⟮X⟯) ((algebraMap A[X] A⟮X⟯ : (a : A[X]) → A⟮X⟯) p : A⟮X⟯) (b • c)

Tactic:
simp
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K_1 : Type u
inst : CommRing K_1
inst_1 : IsDomain K_1
A : Type u_1
k : Type u_2
K : Type u_3
inst_2 : CommRing A
inst_3 : IsDomain A
inst_4 : Field k
inst_5 : Field K
inst_6 : Algebra.{u_1, u_2} A[X] k
inst_7 : Algebra.{u_1, u_3} A[X] K
inst_8 : SMul k K
inst_9 : FaithfulSMul.{u_1, u_2} A[X] k
inst_10 : FaithfulSMul.{u_1, u_3} A[X] K
inst_11 : IsScalarTower.{u_1, u_2, u_3} A[X] k K
a : A⟮X⟯
b : k
c : K
f :
  ∀ (p q : A[X]) (hq : q ≠ 0),
    (HDiv.hDiv (α := A⟮X⟯) (β := A⟮X⟯) ((algebraMap A[X] A⟮X⟯ : (a : A[X]) → A⟮X⟯) p : A⟮X⟯)
            ((algebraMap A[X] A⟮X⟯ : (a : A[X]) → A⟮X⟯) q : A⟮X⟯) •
          b) •
        c =
      HDiv.hDiv (α := A⟮X⟯) (β := A⟮X⟯) ((algebraMap A[X] A⟮X⟯ : (a : A[X]) → A⟮X⟯) p : A⟮X⟯)
          ((algebraMap A[X] A⟮X⟯ : (a : A[X]) → A⟮X⟯) q : A⟮X⟯) •
        b • c
⊢ (a • b) • c = a • b • c

Tactic:
induction a using RatFunc.induction_on with | f p q hq =>
    rw [← smul_right_inj hq]
    simp_rw [← smul_assoc, Algebra.smul_def q]
    field_simp [hq]
    simp

Premises used: smul_assoc, RatFunc.induction_on
-- 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
rw :
  (HMul.hMul (α := K[X])
        ((C : (a : K) → K[X]) (a * q / @gcd _ CommSemiring.toCommMonoidWithZero _ (a * p) (a * q)).leadingCoeff⁻¹ :
          K[X])
        (a * p / @gcd _ CommSemiring.toCommMonoidWithZero _ (a * p) (a * q)),
      HMul.hMul (α := K[X])
        ((C : (a : K) → K[X]) (a * q / @gcd _ CommSemiring.toCommMonoidWithZero _ (a * p) (a * q)).leadingCoeff⁻¹ :
          K[X])
        (a * q / @gcd _ CommSemiring.toCommMonoidWithZero _ (a * p) (a * 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]) (q / @gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff⁻¹ : K[X])
        (q / @gcd _ CommSemiring.toCommMonoidWithZero _ p q))
⊢ (if a * q = 0 then (0, 1)
    else
      (HMul.hMul (α := K[X])
          ((C : (a : K) → K[X]) (a * q / @gcd _ CommSemiring.toCommMonoidWithZero _ (a * p) (a * q)).leadingCoeff⁻¹ :
            K[X])
          (a * p / @gcd _ CommSemiring.toCommMonoidWithZero _ (a * p) (a * q)),
        HMul.hMul (α := K[X])
          ((C : (a : K) → K[X]) (a * q / @gcd _ CommSemiring.toCommMonoidWithZero _ (a * p) (a * q)).leadingCoeff⁻¹ :
            K[X])
          (a * q / @gcd _ CommSemiring.toCommMonoidWithZero _ (a * p) (a * q)))) =
    if q = 0 then (0, 1)
    else
      (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]) (q / @gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff⁻¹ : K[X])
          (q / @gcd _ CommSemiring.toCommMonoidWithZero _ p q))

Tactic:
rw [if_neg hq, if_neg (mul_ne_zero ha hq)]

Premises used: mul_ne_zero, if_neg
-- 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
⊢ a.leadingCoeff ≠ 0

Tactic:
have ha' : a.leadingCoeff ≠ 0 := Polynomial.leadingCoeff_ne_zero.mpr ha
-- 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
⊢ a.leadingCoeff⁻¹ ≠ 0

Tactic:
have hainv : a.leadingCoeff⁻¹ ≠ 0 := inv_ne_zero ha'
-- 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
simp :
  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)
⊢ (HMul.hMul (α := K[X])
        ((C : (a : K) → K[X]) (a * q / @gcd _ CommSemiring.toCommMonoidWithZero _ (a * p) (a * q)).leadingCoeff⁻¹ :
          K[X])
        (a * p / @gcd _ CommSemiring.toCommMonoidWithZero _ (a * p) (a * q)),
      HMul.hMul (α := K[X])
        ((C : (a : K) → K[X]) (a * q / @gcd _ CommSemiring.toCommMonoidWithZero _ (a * p) (a * q)).leadingCoeff⁻¹ :
          K[X])
        (a * q / @gcd _ CommSemiring.toCommMonoidWithZero _ (a * p) (a * 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]) (q / @gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff⁻¹ : K[X])
        (q / @gcd _ CommSemiring.toCommMonoidWithZero _ p q))

Tactic:
simp only [Prod.ext_iff, gcd_mul_left, normalize_apply a, Polynomial.coe_normUnit, mul_assoc,
        CommGroupWithZero.coe_normUnit _ ha']

Premises used: CommGroupWithZero.coe_normUnit, gcd_mul_left, mul_assoc, Prod.ext_iff, normalize_apply, Polynomial.coe_normUnit
-- 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
⊢ (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).degree ≤ q.degree

Tactic:
have hdeg : (gcd p q).degree ≤ q.degree := degree_gcd_le_right _ hq
-- 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
rw : (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).degree ≤ q.degree
⊢ (HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) a.leadingCoeff⁻¹ : K[X])
        (@gcd _ CommSemiring.toCommMonoidWithZero _ p q)).degree ≤
    q.degree

Tactic:
rw [Polynomial.degree_mul, Polynomial.degree_C hainv, zero_add]

Premises used: Polynomial.degree_C, zero_add, Polynomial.degree_mul
-- 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
⊢ (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).degree ≤ q.degree

Tactic:
hdeg
-- 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
⊢ (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).degree ≤ q.degree

Tactic:
exact hdeg
-- 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
⊢ (HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) a.leadingCoeff⁻¹ : K[X])
        (@gcd _ CommSemiring.toCommMonoidWithZero _ p q)).degree ≤
    q.degree

Tactic:
have hdeg' : (Polynomial.C a.leadingCoeff⁻¹ * gcd p q).degree ≤ q.degree := by
        rw [Polynomial.degree_mul, Polynomial.degree_C hainv, zero_add]
        exact hdeg
-- 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
⊢ HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) a.leadingCoeff⁻¹ : K[X])
      (@gcd _ CommSemiring.toCommMonoidWithZero _ p q) ∣
    p

Tactic:
have hdivp : Polynomial.C a.leadingCoeff⁻¹ * gcd p q ∣ p :=
        (C_mul_dvd hainv).mpr (gcd_dvd_left p q)
-- 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
⊢ HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) a.leadingCoeff⁻¹ : K[X])
      (@gcd _ CommSemiring.toCommMonoidWithZero _ p q) ∣
    q

Tactic:
have hdivq : Polynomial.C a.leadingCoeff⁻¹ * gcd p q ∣ q :=
        (C_mul_dvd hainv).mpr (gcd_dvd_right p q)
-- 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
left :
  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)
right :
  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])
            ((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:
constructor
-- 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
left :
  (q.leadingCoeff / (a.leadingCoeff⁻¹ * (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff))⁻¹ *
      a.leadingCoeff⁻¹⁻¹ =
    (q.leadingCoeff / (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff)⁻¹
⊢ 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)

Tactic:
congr
-- 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
right :
  (q.leadingCoeff / (a.leadingCoeff⁻¹ * (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff))⁻¹ *
      a.leadingCoeff⁻¹⁻¹ =
    (q.leadingCoeff / (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff)⁻¹
⊢ 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:
congr
-- 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
left :
  a.leadingCoeff⁻¹ * (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff / q.leadingCoeff *
      a.leadingCoeff⁻¹⁻¹ =
    (q.leadingCoeff / (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff)⁻¹
left₁ :
  a.leadingCoeff⁻¹⁻¹ *
      (a.leadingCoeff⁻¹ * (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff / q.leadingCoeff) =
    (q.leadingCoeff / (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff)⁻¹
left₂ :
  a.leadingCoeff⁻¹⁻¹ *
      (a.leadingCoeff⁻¹ * ((@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff / q.leadingCoeff)) =
    (q.leadingCoeff / (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff)⁻¹
left₃ :
  a.leadingCoeff⁻¹⁻¹ * a.leadingCoeff⁻¹ *
      ((@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff / q.leadingCoeff) =
    (q.leadingCoeff / (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff)⁻¹
left₄ :
  a.leadingCoeff * a.leadingCoeff⁻¹ * ((@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff / q.leadingCoeff) =
    (q.leadingCoeff / (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff)⁻¹
left₅ :
  1 * ((@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff / q.leadingCoeff) =
    (q.leadingCoeff / (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff)⁻¹
left₆ :
  (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff / q.leadingCoeff =
    (q.leadingCoeff / (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff)⁻¹
left₇ left₈ :
  (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff / q.leadingCoeff =
    (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff / q.leadingCoeff
⊢ (q.leadingCoeff / (a.leadingCoeff⁻¹ * (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff))⁻¹ *
      a.leadingCoeff⁻¹⁻¹ =
    (q.leadingCoeff / (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff)⁻¹

Tactic:
rw [inv_div, mul_comm, mul_div_assoc, ← mul_assoc, inv_inv, mul_inv_cancel₀ ha',
          one_mul, inv_div]

Premises used: mul_inv_cancel₀, mul_assoc, mul_div_assoc, inv_inv, mul_comm, inv_div, one_mul