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 : K[X]
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⟯)
⊢ num ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p) = p
have h₁ : p =
  HMul.hMul (α := K[X])
    ((C : (a : K) → K[X]) (1 / @gcd _ CommSemiring.toCommMonoidWithZero _ p 1).leadingCoeff⁻¹ : K[X])
    (p / @gcd _ CommSemiring.toCommMonoidWithZero _ p 1)
Tactic: convert! num_div p 1
-- 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 ∣
    p
have rw : p / @gcd _ CommSemiring.toCommMonoidWithZero _ p q ∣ p
Tactic: rw [num_div _ q, C_mul_dvd]
-- 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 : p / @gcd _ CommSemiring.toCommMonoidWithZero _ p q ∣ 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⟯) q : K⟮X⟯)).num ∣
    p
have rw₁ : (q / @gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff⁻¹ ≠ 0
Tactic: rw [num_div _ q, C_mul_dvd]
-- 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 ∣
    p
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) ∣
  p
Tactic: classical
  rw [num_div _ q, C_mul_dvd]
  · exact EuclideanDomain.div_dvd_of_dvd (gcd_dvd_left p q)
  · simpa only [Ne, inv_eq_zero, Polynomial.leadingCoeff_eq_zero] using right_div_gcd_ne_zero 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 :
  HMul.hMul (α := K[X])
      ((C : (a : K) → K[X]) (q / @gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff⁻¹ : K[X])
      (p / @gcd _ CommSemiring.toCommMonoidWithZero _ p q) ∣
    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⟯) q : K⟮X⟯)).num ∣
    p
have rw₁ : p / @gcd _ CommSemiring.toCommMonoidWithZero _ p q ∣ p
Tactic: classical
  rw [num_div _ q, C_mul_dvd]
  · exact EuclideanDomain.div_dvd_of_dvd (gcd_dvd_left p q)
  · simpa only [Ne, inv_eq_zero, Polynomial.leadingCoeff_eq_zero] using right_div_gcd_ne_zero 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 :
  HMul.hMul (α := K[X])
      ((C : (a : K) → K[X]) (q / @gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff⁻¹ : K[X])
      (p / @gcd _ CommSemiring.toCommMonoidWithZero _ p q) ∣
    p
rw₁ : p / @gcd _ CommSemiring.toCommMonoidWithZero _ p q ∣ 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⟯) q : K⟮X⟯)).num ∣
    p
have rw₂ : (q / @gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff⁻¹ ≠ 0
Tactic: classical
  rw [num_div _ q, C_mul_dvd]
  · exact EuclideanDomain.div_dvd_of_dvd (gcd_dvd_left p q)
  · simpa only [Ne, inv_eq_zero, Polynomial.leadingCoeff_eq_zero] using right_div_gcd_ne_zero 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
⊢ (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 =
    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 : (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.2 =
  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 [denom, 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.2 =
    HMul.hMul (α := K[X])
      ((C : (a : K) → K[X]) (q / @gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff⁻¹ : K[X])
      (q / @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⟯)).denom =
    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]) (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)).2 =
  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 [denom, 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
⊢ (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.Monic
have f : (HMul.hMul (β := K[X]) (q / @gcd _ CommSemiring.toCommMonoidWithZero _ p q)
    ((C : (a : K) → K[X]) (q / @gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff⁻¹ : K[X])).Monic
Tactic: rw [denom_div p hq, mul_comm]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
⊢ x.denom.Monic
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⟯) p : K⟮X⟯)
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯)).denom.Monic
Tactic: induction x using RatFunc.induction_on with
  | f p q hq =>
    rw [denom_div p hq, mul_comm]
    exact Polynomial.monic_mul_leadingCoeff_inv (right_div_gcd_ne_zero hq)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
⊢ x.denom.Monic
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⟯) p : K⟮X⟯)
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯)).denom.Monic
Tactic: classical
  induction x using RatFunc.induction_on with
  | f p q hq =>
    rw [denom_div p hq, mul_comm]
    exact Polynomial.monic_mul_leadingCoeff_inv (right_div_gcd_ne_zero hq)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : Field K
⊢ Eq.{u + 1} (α := K[X]) (denom 0) 1
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! denom_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]) (denom 0) 1
have h₁ : 1 =
  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]) 1 (@gcd _ CommSemiring.toCommMonoidWithZero _ 0 1))
Tactic: convert! denom_div (0 : K[X]) one_ne_zero
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : Field K
⊢ Eq.{u + 1} (α := K[X]) (denom 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! denom_div (1 : K[X]) one_ne_zero
-- 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]) (denom 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! denom_div (1 : K[X]) one_ne_zero
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : Field K
p : K[X]
⊢ Eq.{u + 1} (α := K[X]) (denom ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p)) 1
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! denom_div p one_ne_zero
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : Field K
p : K[X]
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⟯)
⊢ Eq.{u + 1} (α := K[X]) (denom ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p)) 1
have h₁ : 1 =
  HMul.hMul (α := K[X])
    ((C : (a : K) → K[X]) (1 / @gcd _ CommSemiring.toCommMonoidWithZero _ p 1).leadingCoeff⁻¹ : K[X])
    (1 / @gcd _ CommSemiring.toCommMonoidWithZero _ p 1)
Tactic: convert! denom_div p 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⟯)).denom ∣
    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⟯)).denom ∣
    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⟯)).denom ∣
      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⟯)).denom ∣
    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⟯)).denom ∣
    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]
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⟯)).denom ∣
    q
have neg : q / @gcd _ CommSemiring.toCommMonoidWithZero _ p q ∣ q
Tactic: rw [denom_div _ hq, C_mul_dvd]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : Field K
p q : K[X]
hq : ¬q = 0
neg : q / @gcd _ CommSemiring.toCommMonoidWithZero _ p q ∣ 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⟯)).denom ∣
    q
have neg₁ : (q / @gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff⁻¹ ≠ 0
Tactic: rw [denom_div _ hq, C_mul_dvd]
-- 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⟯)).denom ∣
    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⟯)).denom ∣
    q
Tactic: classical
  by_cases hq : q = 0
  · simp [hq]
  rw [denom_div _ hq, C_mul_dvd]
  · exact EuclideanDomain.div_dvd_of_dvd (gcd_dvd_right p q)
  · simpa only [Ne, inv_eq_zero, Polynomial.leadingCoeff_eq_zero] using right_div_gcd_ne_zero hq
-- 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⟯)).denom ∣
      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⟯)).denom ∣
    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⟯)).denom ∣
    q
Tactic: classical
  by_cases hq : q = 0
  · simp [hq]
  rw [denom_div _ hq, C_mul_dvd]
  · exact EuclideanDomain.div_dvd_of_dvd (gcd_dvd_right p q)
  · simpa only [Ne, inv_eq_zero, Polynomial.leadingCoeff_eq_zero] using right_div_gcd_ne_zero hq
-- 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⟯)).denom ∣
      q
neg 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⟯)).denom ∣
      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⟯)).denom ∣
    q
have neg₂ : ∀ (hq : ¬q = 0), q / @gcd _ CommSemiring.toCommMonoidWithZero _ p q ∣ q
Tactic: classical
  by_cases hq : q = 0
  · simp [hq]
  rw [denom_div _ hq, C_mul_dvd]
  · exact EuclideanDomain.div_dvd_of_dvd (gcd_dvd_right p q)
  · simpa only [Ne, inv_eq_zero, Polynomial.leadingCoeff_eq_zero] using right_div_gcd_ne_zero hq
-- 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⟯)).denom ∣
      q
neg 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⟯)).denom ∣
      q
neg₂ : ∀ (hq : ¬q = 0), q / @gcd _ CommSemiring.toCommMonoidWithZero _ p q ∣ 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⟯)).denom ∣
    q
have neg₃ : ∀ (hq : ¬q = 0), (q / @gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff⁻¹ ≠ 0
Tactic: classical
  by_cases hq : q = 0
  · simp [hq]
  rw [denom_div _ hq, C_mul_dvd]
  · exact EuclideanDomain.div_dvd_of_dvd (gcd_dvd_right p q)
  · simpa only [Ne, inv_eq_zero, Polynomial.leadingCoeff_eq_zero] using right_div_gcd_ne_zero hq
-- 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: induction x using RatFunc.induction_on with | _ p q hq
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (hypothesis)
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⟯)
          (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 q_div_ne_zero : q / @gcd _ CommSemiring.toCommMonoidWithZero _ p q ≠ 0
Tactic: have q_div_ne_zero : q / gcd p q ≠ 0 := right_div_gcd_ne_zero 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
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⟯)
have f : @gcd _ CommSemiring.toCommMonoidWithZero _ p q ∣ q
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
f : @gcd _ CommSemiring.toCommMonoidWithZero _ p q ∣ q
⊢ 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₁ : @gcd _ CommSemiring.toCommMonoidWithZero _ p q ∣ p
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
f : @gcd _ CommSemiring.toCommMonoidWithZero _ p q ∣ q
f₁ : @gcd _ CommSemiring.toCommMonoidWithZero _ p q ∣ p
⊢ 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⟯) (q / @gcd _ CommSemiring.toCommMonoidWithZero _ p q) : 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
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⟯)
⊢ 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⟯) q : 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]