awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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)⁻¹
right₇ right₈ :
  (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff / q.leadingCoeff =
    (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff / q.leadingCoeff
⊢ (q.leadingCoeff / (a.leadingCoeff⁻¹ * (@gcd _ CommSemiring.toCommMonoidWithZero _ p 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]

Premises used: mul_inv_cancel₀, mul_assoc, mul_div_assoc, inv_inv, mul_comm, inv_div, one_mul
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
p q : K[X]
hq : q ≠ 0
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)))
⊢ (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))

Tactic:
rw [numDenom, liftOn'_div, if_neg hq]

Premises used: RatFunc.numDenom, RatFunc.liftOn'_div, if_neg
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
p_1 q : K[X]
hq : q ≠ 0
p : K[X]
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)))
⊢ 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 [if_pos rfl, if_neg (one_ne_zero' K[X])]

Premises used: one_ne_zero', if_pos, Polynomial, if_neg, rfl
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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]) (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:
simp
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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)
rw₁ 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)
⊢ (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:
rw [num, numDenom_div _ hq]

Premises used: RatFunc.numDenom_div, RatFunc.num
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
⊢ (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)).num =
    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:
num_div' (0 : K[X]) one_ne_zero

Premises used: _private.0.RatFunc.num_div', one_ne_zero, OfNat.ofNat
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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)
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))
⊢ Eq.{u + 1} (α := K[X]) (num 0) 0

Tactic:
convert! num_div' (0 : K[X]) one_ne_zero

Premises used: _private.0.RatFunc.num_div', one_ne_zero, OfNat.ofNat
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
⊢ 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:
simp
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
⊢ 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:
simp
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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)
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)
⊢ (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
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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)

Tactic:
simp [hq]
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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)

Tactic:
num_div' p hq

Premises used: _private.0.RatFunc.num_div'
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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)

Tactic:
exact num_div' p hq

Premises used: _private.0.RatFunc.num_div'
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
⊢ (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)).num =
    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:
num_div (1 : K[X]) 1

Premises used: RatFunc.num_div, OfNat.ofNat
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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)
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))
⊢ Eq.{u + 1} (α := K[X]) (num 1) 1

Tactic:
convert! num_div (1 : K[X]) 1

Premises used: RatFunc.num_div, OfNat.ofNat
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
⊢ 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:
simp
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
⊢ 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:
simp
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
p : 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⟯) 1 : K⟮X⟯)).num =
    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:
num_div p 1

Premises used: RatFunc.num_div, OfNat.ofNat
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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⟯)
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)
⊢ num ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p) = p

Tactic:
convert! num_div p 1

Premises used: RatFunc.num_div, OfNat.ofNat
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
p : K[X]
⊢ (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:
simp
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
p : K[X]
⊢ 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:
simp
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
p q : K[X]
hq : q ≠ 0
rw : p / @gcd _ CommSemiring.toCommMonoidWithZero _ p q ∣ p
rw₁ : (q / @gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff⁻¹ ≠ 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

Tactic:
rw [num_div _ q, C_mul_dvd]

Premises used: RatFunc.num_div, Polynomial.C_mul_dvd
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
p q : K[X]
hq : q ≠ 0
⊢ p / @gcd _ CommSemiring.toCommMonoidWithZero _ p q ∣ p

Tactic:
EuclideanDomain.div_dvd_of_dvd (gcd_dvd_left p q)

Premises used: EuclideanDomain.div_dvd_of_dvd, GCDMonoid.gcd_dvd_left
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
p q : K[X]
hq : q ≠ 0
⊢ p / @gcd _ CommSemiring.toCommMonoidWithZero _ p q ∣ p

Tactic:
exact EuclideanDomain.div_dvd_of_dvd (gcd_dvd_left p q)

Premises used: EuclideanDomain.div_dvd_of_dvd, GCDMonoid.gcd_dvd_left
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
p q : K[X]
hq : q ≠ 0
⊢ (q / @gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff⁻¹ ≠ 0

Tactic:
simpa only [Ne, inv_eq_zero, Polynomial.leadingCoeff_eq_zero] using right_div_gcd_ne_zero hq

Premises used: inv_eq_zero, Ne, right_div_gcd_ne_zero, Polynomial.leadingCoeff_eq_zero
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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
rw₂ : (q / @gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff⁻¹ ≠ 0
rw₃ : p / @gcd _ CommSemiring.toCommMonoidWithZero _ p q ∣ p
rw₄ : (q / @gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff⁻¹ ≠ 0
rw₅ : p / @gcd _ CommSemiring.toCommMonoidWithZero _ p q ∣ p
rw₆ rw₇ : (q / @gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff⁻¹ ≠ 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

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

Premises used: RatFunc.num_div, inv_eq_zero, Ne, Polynomial.C_mul_dvd, Polynomial.leadingCoeff_eq_zero
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
p q : K[X]
hq : q ≠ 0
⊢ 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:
simpa using num_div_dvd p hq

Premises used: RatFunc.num_div_dvd
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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)
rw₁ 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)
⊢ (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)

Tactic:
rw [denom, numDenom_div _ hq]

Premises used: RatFunc.denom, RatFunc.numDenom_div
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
p q : K[X]
hq : q ≠ 0
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
⊢ (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:
rw [denom_div p hq, mul_comm]

Premises used: RatFunc.denom_div, mul_comm
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
p q : K[X]
hq : q ≠ 0
⊢ (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:
Polynomial.monic_mul_leadingCoeff_inv (right_div_gcd_ne_zero hq)

Premises used: right_div_gcd_ne_zero, Polynomial.monic_mul_leadingCoeff_inv
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
p q : K[X]
hq : q ≠ 0
⊢ (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:
exact Polynomial.monic_mul_leadingCoeff_inv (right_div_gcd_ne_zero hq)

Premises used: right_div_gcd_ne_zero, Polynomial.monic_mul_leadingCoeff_inv
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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⟯) p : K⟮X⟯)
          ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯)).denom.Monic
⊢ 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)

Premises used: RatFunc.induction_on, mul_comm
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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⟯) p : K⟮X⟯)
          ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯)).denom.Monic
⊢ 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)

Premises used: RatFunc.induction_on, mul_comm
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
⊢ x.denom ≠ 0

Tactic:
(monic_denom x).ne_zero

Premises used: Polynomial.Monic.ne_zero, RatFunc.monic_denom
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
⊢ (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)).denom =
    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:
denom_div (0 : K[X]) one_ne_zero

Premises used: RatFunc.denom_div, one_ne_zero, OfNat.ofNat
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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)
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))
⊢ Eq.{u + 1} (α := K[X]) (denom 0) 1

Tactic:
convert! denom_div (0 : K[X]) one_ne_zero

Premises used: RatFunc.denom_div, one_ne_zero, OfNat.ofNat
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
⊢ 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:
simp
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
⊢ (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)).denom =
    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:
denom_div (1 : K[X]) one_ne_zero

Premises used: RatFunc.denom_div, one_ne_zero, OfNat.ofNat