awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : Field K
p q : K[X]
hq : q ≠ 0
q_div_ne_zero : q / @gcd _ CommSemiring.toCommMonoidWithZero _ p q ≠ 0
f : @gcd _ CommSemiring.toCommMonoidWithZero _ p q ∣ q
f₁ : @gcd _ CommSemiring.toCommMonoidWithZero _ p q ∣ p
f₂ :
  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₃ : Ne (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯) (0 : K⟮X⟯)
⊢ 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⟯)
have f₄ : 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⟯)
Tactic: 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]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : Field K
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⟯)
have f : ¬(q / @gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff⁻¹ = 0
Tactic: refine algebraMap_ne_zero (mt Polynomial.C_eq_zero.mp ?_)
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : Field K
x : 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
have 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⟯)
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)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
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⟯)
⊢ 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
have 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⟯)
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)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
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⟯)
⊢ 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
have 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
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)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
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
⊢ 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
have 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
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)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
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
⊢ 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
have 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⟯)
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)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
⊢ IsCoprime x.num x.denom
have f : ∀ (p q : K[X]) (hq : q ≠ 0),
  IsCoprime
    (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
    (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
Tactic: induction x using RatFunc.induction_on with | _ p q hq
Cleared hypotheses: 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
⊢ IsCoprime
    (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
    (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
have f : IsCoprime
  (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 [num_div, denom_div _ hq]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
⊢ IsCoprime x.num x.denom
have f : ∀ (p q : K[X]) (hq : q ≠ 0),
  IsCoprime
    (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
    (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
Tactic: classical
  induction x using RatFunc.induction_on with | _ p q hq
  rw [num_div, denom_div _ hq]
  exact (isCoprime_mul_unit_left
    ((leadingCoeff_ne_zero.2 <| right_div_gcd_ne_zero hq).isUnit.inv.map C) _ _).2
      (isCoprime_div_gcd_div_gcd hq)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
f :
  ∀ (p q : K[X]) (hq : q ≠ 0),
    IsCoprime
      (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
      (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
⊢ IsCoprime x.num x.denom
have f₁ : ∀ (p q : K[X]) (hq : q ≠ 0),
  IsCoprime
    (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: classical
  induction x using RatFunc.induction_on with | _ p q hq
  rw [num_div, denom_div _ hq]
  exact (isCoprime_mul_unit_left
    ((leadingCoeff_ne_zero.2 <| right_div_gcd_ne_zero hq).isUnit.inv.map C) _ _).2
      (isCoprime_div_gcd_div_gcd hq)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
h : x.num = 0
⊢ x = 0
have rw : 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⟯) =
  0
Tactic: rw [← num_div_denom x, h, map_zero, zero_div]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
h : x.num = 0
rw :
  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⟯) =
    0
⊢ x = 0
have rw₁ : HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) 0 : K⟮X⟯)
    ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.denom : K⟮X⟯) =
  0
Tactic: rw [← num_div_denom x, h, map_zero, zero_div]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
h : x.num = 0
rw :
  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⟯) =
    0
rw₁ :
  HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) 0 : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.denom : K⟮X⟯) =
    0
⊢ x = 0
have rw₂ : HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) (0 : K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.denom : K⟮X⟯) = 0
Tactic: rw [← num_div_denom x, h, map_zero, zero_div]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
h : x.num = 0
rw :
  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⟯) =
    0
rw₁ :
  HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) 0 : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.denom : K⟮X⟯) =
    0
rw₂ : HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) (0 : K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.denom : K⟮X⟯) = 0
⊢ x = 0
have rw₃ : Eq.{u + 1} (α := K⟮X⟯) 0 0
Tactic: rw [← num_div_denom x, h, map_zero, zero_div]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
p q : K[X]
hq : q ≠ 0
⊢ x.num * q = p * x.denom ↔
    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⟯)
have rw : Eq (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (x.num * q) : K⟮X⟯)
    ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (p * x.denom) : K⟮X⟯) ↔
  HMul.hMul (β := K⟮X⟯) x ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯) =
    (algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p
Tactic: rw [← (algebraMap_injective K).eq_iff, eq_div_iff (algebraMap_ne_zero hq)]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
p q : K[X]
hq : q ≠ 0
| HMul.hMul (β := K⟮X⟯) x ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯) =
    (algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p
have rw : HMul.hMul (β := 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⟯))
    ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯) =
  (algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p
Tactic: rw [← num_div_denom x]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
p q : K[X]
hq : q ≠ 0
⊢ Eq (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (x.num * q) : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (p * x.denom) : K⟮X⟯) ↔
    HMul.hMul (β := K⟮X⟯) x ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯) =
      (algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p
have conv_rhs : Eq (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (x.num * q) : K⟮X⟯)
    ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (p * x.denom) : K⟮X⟯) ↔
  HMul.hMul (β := 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⟯))
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯) =
    (algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p
Tactic: conv_rhs => rw [← num_div_denom x]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
p q : K[X]
hq : q ≠ 0
⊢ Eq (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (x.num * q) : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (p * x.denom) : K⟮X⟯) ↔
    HMul.hMul (β := 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⟯))
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯) =
      (algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p
have rw : Ne (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.denom : K⟮X⟯) (0 : K⟮X⟯)
Tactic: rw [map_mul, map_mul, div_eq_mul_inv, mul_assoc, mul_comm (Inv.inv _), ←
    mul_assoc, ← div_eq_mul_inv, div_eq_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : Field K
x y : K⟮X⟯
| x + y
have rw : 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⟯) +
  HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) y.num : K⟮X⟯)
    ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) y.denom : K⟮X⟯)
Tactic: rw [← num_div_denom x, ← num_div_denom y]