awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
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
⊢ (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
have 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
Tactic: rw [← smul_right_inj hq]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
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
⊢ 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
have 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
Tactic: simp_rw [← smul_assoc, Algebra.smul_def q]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
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
⊢ (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
have 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)
Tactic: field_simp [hq]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
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
⊢ (a • b) • c = a • b • c
have 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
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
Cleared hypotheses: a
-- 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
⊢ (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))
have 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))
Tactic: rw [if_neg hq, if_neg (mul_ne_zero ha hq)]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (hypothesis)
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
p q a : K[X]
hq : q ≠ 0
ha : a ≠ 0
⊢ (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))
have ha' : a.leadingCoeff ≠ 0
Tactic: have ha' : a.leadingCoeff ≠ 0 := Polynomial.leadingCoeff_ne_zero.mpr ha
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (hypothesis)
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
⊢ (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))
have hainv : a.leadingCoeff⁻¹ ≠ 0
Tactic: have hainv : a.leadingCoeff⁻¹ ≠ 0 := inv_ne_zero ha'
-- 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
⊢ (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))
have 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)
Tactic: simp only [Prod.ext_iff, gcd_mul_left, normalize_apply a, Polynomial.coe_normUnit, mul_assoc,
        CommGroupWithZero.coe_normUnit _ ha']
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (hypothesis)
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
⊢ 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 hdeg : (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).degree ≤ q.degree
Tactic: have hdeg : (gcd p q).degree ≤ q.degree := degree_gcd_le_right _ hq
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (hypothesis)
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 * 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 hdeg' : (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
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (hypothesis)
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 * 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 hdivp : 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)
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (hypothesis)
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 * 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 hdivq : 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)
-- 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])
            ((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)
have 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)
Tactic: constructor