awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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)
⊢ 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 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)
Tactic: constructor
-- 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)
have left : (q.leadingCoeff / (a.leadingCoeff⁻¹ * (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff))⁻¹ *
    a.leadingCoeff⁻¹⁻¹ =
  (q.leadingCoeff / (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff)⁻¹
Tactic: congr
-- 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])
      (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 right : (q.leadingCoeff / (a.leadingCoeff⁻¹ * (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff))⁻¹ *
    a.leadingCoeff⁻¹⁻¹ =
  (q.leadingCoeff / (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff)⁻¹
Tactic: congr
-- 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
⊢ (q.leadingCoeff / (a.leadingCoeff⁻¹ * (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff))⁻¹ *
      a.leadingCoeff⁻¹⁻¹ =
    (q.leadingCoeff / (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff)⁻¹
have left : a.leadingCoeff⁻¹ * (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff / 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]
-- 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
left :
  a.leadingCoeff⁻¹ * (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff / q.leadingCoeff *
      a.leadingCoeff⁻¹⁻¹ =
    (q.leadingCoeff / (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff)⁻¹
⊢ (q.leadingCoeff / (a.leadingCoeff⁻¹ * (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff))⁻¹ *
      a.leadingCoeff⁻¹⁻¹ =
    (q.leadingCoeff / (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff)⁻¹
have left₁ : a.leadingCoeff⁻¹⁻¹ *
    (a.leadingCoeff⁻¹ * (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff / q.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]
-- 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
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)⁻¹
⊢ (q.leadingCoeff / (a.leadingCoeff⁻¹ * (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff))⁻¹ *
      a.leadingCoeff⁻¹⁻¹ =
    (q.leadingCoeff / (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff)⁻¹
have left₂ : a.leadingCoeff⁻¹⁻¹ *
    (a.leadingCoeff⁻¹ * ((@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff / q.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]
-- 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
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)⁻¹
⊢ (q.leadingCoeff / (a.leadingCoeff⁻¹ * (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff))⁻¹ *
      a.leadingCoeff⁻¹⁻¹ =
    (q.leadingCoeff / (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff)⁻¹
have left₃ : a.leadingCoeff⁻¹⁻¹ * a.leadingCoeff⁻¹ *
    ((@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff / q.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]
-- 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
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)⁻¹
⊢ (q.leadingCoeff / (a.leadingCoeff⁻¹ * (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff))⁻¹ *
      a.leadingCoeff⁻¹⁻¹ =
    (q.leadingCoeff / (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff)⁻¹
have left₄ : a.leadingCoeff * a.leadingCoeff⁻¹ * ((@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff / q.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]
-- 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
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)⁻¹
⊢ (q.leadingCoeff / (a.leadingCoeff⁻¹ * (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff))⁻¹ *
      a.leadingCoeff⁻¹⁻¹ =
    (q.leadingCoeff / (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff)⁻¹
have left₅ : 1 * ((@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff / q.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]
-- 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
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)⁻¹
⊢ (q.leadingCoeff / (a.leadingCoeff⁻¹ * (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff))⁻¹ *
      a.leadingCoeff⁻¹⁻¹ =
    (q.leadingCoeff / (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff)⁻¹
have left₆ : (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff / q.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]
-- 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
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)⁻¹
⊢ (q.leadingCoeff / (a.leadingCoeff⁻¹ * (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff))⁻¹ *
      a.leadingCoeff⁻¹⁻¹ =
    (q.leadingCoeff / (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff)⁻¹
have left₇ : (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff / q.leadingCoeff =
  (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff / q.leadingCoeff
Tactic: rw [inv_div, mul_comm, mul_div_assoc, ← mul_assoc, inv_inv, mul_inv_cancel₀ ha',
          one_mul, inv_div]
-- 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
⊢ (q.leadingCoeff / (a.leadingCoeff⁻¹ * (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff))⁻¹ *
      a.leadingCoeff⁻¹⁻¹ =
    (q.leadingCoeff / (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff)⁻¹
have right : a.leadingCoeff⁻¹ * (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff / 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]