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
right :
  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 right₁ : 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
right :
  a.leadingCoeff⁻¹ * (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff / q.leadingCoeff *
      a.leadingCoeff⁻¹⁻¹ =
    (q.leadingCoeff / (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff)⁻¹
right₁ :
  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 right₂ : 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
right :
  a.leadingCoeff⁻¹ * (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff / q.leadingCoeff *
      a.leadingCoeff⁻¹⁻¹ =
    (q.leadingCoeff / (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff)⁻¹
right₁ :
  a.leadingCoeff⁻¹⁻¹ *
      (a.leadingCoeff⁻¹ * (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff / q.leadingCoeff) =
    (q.leadingCoeff / (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff)⁻¹
right₂ :
  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 right₃ : 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
right :
  a.leadingCoeff⁻¹ * (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff / q.leadingCoeff *
      a.leadingCoeff⁻¹⁻¹ =
    (q.leadingCoeff / (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff)⁻¹
right₁ :
  a.leadingCoeff⁻¹⁻¹ *
      (a.leadingCoeff⁻¹ * (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff / q.leadingCoeff) =
    (q.leadingCoeff / (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff)⁻¹
right₂ :
  a.leadingCoeff⁻¹⁻¹ *
      (a.leadingCoeff⁻¹ * ((@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff / q.leadingCoeff)) =
    (q.leadingCoeff / (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff)⁻¹
right₃ :
  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 right₄ : 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
right :
  a.leadingCoeff⁻¹ * (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff / q.leadingCoeff *
      a.leadingCoeff⁻¹⁻¹ =
    (q.leadingCoeff / (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff)⁻¹
right₁ :
  a.leadingCoeff⁻¹⁻¹ *
      (a.leadingCoeff⁻¹ * (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff / q.leadingCoeff) =
    (q.leadingCoeff / (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff)⁻¹
right₂ :
  a.leadingCoeff⁻¹⁻¹ *
      (a.leadingCoeff⁻¹ * ((@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff / q.leadingCoeff)) =
    (q.leadingCoeff / (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff)⁻¹
right₃ :
  a.leadingCoeff⁻¹⁻¹ * a.leadingCoeff⁻¹ *
      ((@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff / q.leadingCoeff) =
    (q.leadingCoeff / (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff)⁻¹
right₄ :
  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 right₅ : 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
right :
  a.leadingCoeff⁻¹ * (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff / q.leadingCoeff *
      a.leadingCoeff⁻¹⁻¹ =
    (q.leadingCoeff / (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff)⁻¹
right₁ :
  a.leadingCoeff⁻¹⁻¹ *
      (a.leadingCoeff⁻¹ * (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff / q.leadingCoeff) =
    (q.leadingCoeff / (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff)⁻¹
right₂ :
  a.leadingCoeff⁻¹⁻¹ *
      (a.leadingCoeff⁻¹ * ((@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff / q.leadingCoeff)) =
    (q.leadingCoeff / (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff)⁻¹
right₃ :
  a.leadingCoeff⁻¹⁻¹ * a.leadingCoeff⁻¹ *
      ((@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff / q.leadingCoeff) =
    (q.leadingCoeff / (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff)⁻¹
right₄ :
  a.leadingCoeff * a.leadingCoeff⁻¹ * ((@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff / q.leadingCoeff) =
    (q.leadingCoeff / (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff)⁻¹
right₅ :
  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 right₆ : (@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
right :
  a.leadingCoeff⁻¹ * (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff / q.leadingCoeff *
      a.leadingCoeff⁻¹⁻¹ =
    (q.leadingCoeff / (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff)⁻¹
right₁ :
  a.leadingCoeff⁻¹⁻¹ *
      (a.leadingCoeff⁻¹ * (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff / q.leadingCoeff) =
    (q.leadingCoeff / (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff)⁻¹
right₂ :
  a.leadingCoeff⁻¹⁻¹ *
      (a.leadingCoeff⁻¹ * ((@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff / q.leadingCoeff)) =
    (q.leadingCoeff / (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff)⁻¹
right₃ :
  a.leadingCoeff⁻¹⁻¹ * a.leadingCoeff⁻¹ *
      ((@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff / q.leadingCoeff) =
    (q.leadingCoeff / (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff)⁻¹
right₄ :
  a.leadingCoeff * a.leadingCoeff⁻¹ * ((@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff / q.leadingCoeff) =
    (q.leadingCoeff / (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff)⁻¹
right₅ :
  1 * ((@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff / q.leadingCoeff) =
    (q.leadingCoeff / (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff)⁻¹
right₆ :
  (@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 right₇ : (@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
p q : K[X]
hq : q ≠ 0
⊢ (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⟯)).numDenom =
    (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 f0 : ∀ (p : K[X]),
  Eq.{u + 1} (α := K[X] × K[X])
    (if Eq.{u + 1} (α := K[X]) 0 0 then (0, 1)
    else
      have r := @gcd _ CommSemiring.toCommMonoidWithZero _ p 0;
      (HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (0 / r).leadingCoeff⁻¹ : K[X]) (p / r),
        HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (0 / r).leadingCoeff⁻¹ : K[X]) (0 / r)))
    (if Eq.{u + 1} (α := K[X]) 1 0 then (0, 1)
    else
      have r : K[X] := @gcd _ CommSemiring.toCommMonoidWithZero _ 0 1;
      (HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (1 / r).leadingCoeff⁻¹ : K[X]) (0 / r),
        HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (1 / r).leadingCoeff⁻¹ : K[X]) (1 / r)))
Tactic: rw [numDenom, liftOn'_div, if_neg hq]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : Field K
p_1 q : K[X]
hq : q ≠ 0
p : K[X]
⊢ Eq.{u + 1} (α := K[X] × K[X])
    (if Eq.{u + 1} (α := K[X]) 0 0 then (0, 1)
    else
      have r := @gcd _ CommSemiring.toCommMonoidWithZero _ p 0;
      (HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (0 / r).leadingCoeff⁻¹ : K[X]) (p / r),
        HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (0 / r).leadingCoeff⁻¹ : K[X]) (0 / r)))
    (if Eq.{u + 1} (α := K[X]) 1 0 then (0, 1)
    else
      have r : K[X] := @gcd _ CommSemiring.toCommMonoidWithZero _ 0 1;
      (HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (1 / r).leadingCoeff⁻¹ : K[X]) (0 / r),
        HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (1 / r).leadingCoeff⁻¹ : K[X]) (1 / r)))
have f0 : Eq.{u + 1} (α := K[X] × K[X]) (0, 1)
  (have r : K[X] := @gcd _ CommSemiring.toCommMonoidWithZero _ 0 1;
  (HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (1 / r).leadingCoeff⁻¹ : K[X]) (0 / r),
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (1 / r).leadingCoeff⁻¹ : K[X]) (1 / r)))
Tactic: rw [if_pos rfl, if_neg (one_ne_zero' K[X])]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : Field K
p q : K[X]
hq : q ≠ 0
⊢ (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 =
    HMul.hMul (α := K[X])
      ((C : (a : K) → K[X]) (q / @gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff⁻¹ : K[X])
      (p / @gcd _ CommSemiring.toCommMonoidWithZero _ p q)
have rw : (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⟯)).numDenom.1 =
  HMul.hMul (α := K[X])
    ((C : (a : K) → K[X]) (q / @gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff⁻¹ : K[X])
    (p / @gcd _ CommSemiring.toCommMonoidWithZero _ p q)
Tactic: rw [num, numDenom_div _ hq]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : Field K
p q : K[X]
hq : q ≠ 0
rw :
  (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⟯)).numDenom.1 =
    HMul.hMul (α := K[X])
      ((C : (a : K) → K[X]) (q / @gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff⁻¹ : K[X])
      (p / @gcd _ CommSemiring.toCommMonoidWithZero _ p q)
⊢ (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 =
    HMul.hMul (α := K[X])
      ((C : (a : K) → K[X]) (q / @gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff⁻¹ : K[X])
      (p / @gcd _ CommSemiring.toCommMonoidWithZero _ p q)
have rw₁ : (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)).1 =
  HMul.hMul (α := K[X])
    ((C : (a : K) → K[X]) (q / @gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff⁻¹ : K[X])
    (p / @gcd _ CommSemiring.toCommMonoidWithZero _ p q)
Tactic: rw [num, numDenom_div _ hq]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : Field K
⊢ Eq.{u + 1} (α := K[X]) (num 0) 0
have h : 0 = HDiv.hDiv (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) 0) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) 1)
Tactic: convert! num_div' (0 : K[X]) one_ne_zero
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : Field K
h :
  0 =
    HDiv.hDiv (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) 0) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) 1)
⊢ Eq.{u + 1} (α := K[X]) (num 0) 0
have h₁ : 0 =
  HMul.hMul (α := K[X])
    ((C : (a : K) → K[X]) (HDiv.hDiv (α := K[X]) 1 (@gcd _ CommSemiring.toCommMonoidWithZero _ 0 1)).leadingCoeff⁻¹ :
      K[X])
    (HDiv.hDiv (α := K[X]) 0 (@gcd _ CommSemiring.toCommMonoidWithZero _ 0 1))
Tactic: convert! num_div' (0 : K[X]) one_ne_zero
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : Field K
p q : 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 =
    HMul.hMul (α := K[X])
      ((C : (a : K) → K[X]) (q / @gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff⁻¹ : K[X])
      (p / @gcd _ CommSemiring.toCommMonoidWithZero _ p q)
have pos : ∀ (hq : q = 0),
  (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 =
    HMul.hMul (α := K[X])
      ((C : (a : K) → K[X]) (q / @gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff⁻¹ : K[X])
      (p / @gcd _ CommSemiring.toCommMonoidWithZero _ p q)
Tactic: by_cases hq : q = 0
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : Field K
p q : K[X]
pos :
  ∀ (hq : q = 0),
    (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 =
      HMul.hMul (α := K[X])
        ((C : (a : K) → K[X]) (q / @gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff⁻¹ : K[X])
        (p / @gcd _ CommSemiring.toCommMonoidWithZero _ p q)
⊢ (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 =
    HMul.hMul (α := K[X])
      ((C : (a : K) → K[X]) (q / @gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff⁻¹ : K[X])
      (p / @gcd _ CommSemiring.toCommMonoidWithZero _ p q)
have neg : ∀ (hq : ¬q = 0),
  (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 =
    HMul.hMul (α := K[X])
      ((C : (a : K) → K[X]) (q / @gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff⁻¹ : K[X])
      (p / @gcd _ CommSemiring.toCommMonoidWithZero _ p q)
Tactic: by_cases hq : q = 0
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : Field K
⊢ Eq.{u + 1} (α := K[X]) (num 1) 1
have h : 1 = HDiv.hDiv (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) 1) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) 1)
Tactic: convert! num_div (1 : K[X]) 1
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : Field K
h :
  1 =
    HDiv.hDiv (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) 1) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) 1)
⊢ Eq.{u + 1} (α := K[X]) (num 1) 1
have h₁ : 1 =
  HMul.hMul (α := K[X])
    ((C : (a : K) → K[X]) (HDiv.hDiv (α := K[X]) 1 (@gcd _ CommSemiring.toCommMonoidWithZero _ 1 1)).leadingCoeff⁻¹ :
      K[X])
    (HDiv.hDiv (α := K[X]) 1 (@gcd _ CommSemiring.toCommMonoidWithZero _ 1 1))
Tactic: convert! num_div (1 : K[X]) 1
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : Field K
p : K[X]
⊢ num ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p) = p
have h : (algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p =
  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⟯) 1 : K⟮X⟯)
Tactic: convert! num_div p 1