awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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]) (denom 1) 1

Tactic:
convert! denom_div (1 : 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
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⟯)).denom =
    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:
denom_div p one_ne_zero

Premises used: RatFunc.denom_div, one_ne_zero
-- 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₁ :
  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)
⊢ Eq.{u + 1} (α := K[X]) (denom ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p)) 1

Tactic:
convert! denom_div p one_ne_zero

Premises used: RatFunc.denom_div, one_ne_zero
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
p : K[X]
⊢ 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:
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⟯)).denom ∣
      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⟯)).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

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⟯)).denom ∣
    q

Tactic:
simp [hq]
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
p q : K[X]
hq : ¬q = 0
neg : q / @gcd _ CommSemiring.toCommMonoidWithZero _ p q ∣ q
neg₁ : (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⟯)).denom ∣
    q

Tactic:
rw [denom_div _ hq, C_mul_dvd]

Premises used: RatFunc.denom_div, Polynomial.C_mul_dvd
-- 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 ∣ q

Tactic:
EuclideanDomain.div_dvd_of_dvd (gcd_dvd_right p q)

Premises used: EuclideanDomain.div_dvd_of_dvd, GCDMonoid.gcd_dvd_right
-- 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 ∣ q

Tactic:
exact EuclideanDomain.div_dvd_of_dvd (gcd_dvd_right p q)

Premises used: EuclideanDomain.div_dvd_of_dvd, GCDMonoid.gcd_dvd_right
-- 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]
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
neg₃ neg₄ : ∀ (hq : ¬q = 0), (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⟯)).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

Premises used: inv_eq_zero, Ne, Polynomial.C_mul_dvd, Polynomial.leadingCoeff_eq_zero
-- 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⟯)
            (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

Tactic:
induction x using RatFunc.induction_on with | _ p q hq

Premises used: RatFunc.induction_on
-- 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 ≠ 0

Tactic:
have q_div_ne_zero : q / gcd p q ≠ 0 := right_div_gcd_ne_zero hq
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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⟯)
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⟯)
⊢ 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:
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]

Premises used: RatFunc.num_div, div_eq_div_iff, EuclideanDomain.mul_div_assoc, map_mul, RatFunc.denom_div, mul_div_mul_left, mul_comm
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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
⊢ @gcd _ CommSemiring.toCommMonoidWithZero _ p q ∣ q

Tactic:
apply gcd_dvd_right

Premises used: GCDMonoid.gcd_dvd_right
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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
⊢ @gcd _ CommSemiring.toCommMonoidWithZero _ p q ∣ p

Tactic:
apply gcd_dvd_left

Premises used: GCDMonoid.gcd_dvd_left
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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⟯) (q / @gcd _ CommSemiring.toCommMonoidWithZero _ p q) : K⟮X⟯) (0 : K⟮X⟯)

Tactic:
algebraMap_ne_zero q_div_ne_zero

Premises used: RatFunc.algebraMap_ne_zero
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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⟯) (q / @gcd _ CommSemiring.toCommMonoidWithZero _ p q) : K⟮X⟯) (0 : K⟮X⟯)

Tactic:
exact algebraMap_ne_zero q_div_ne_zero

Premises used: RatFunc.algebraMap_ne_zero
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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⟯) q : K⟮X⟯) (0 : K⟮X⟯)

Tactic:
algebraMap_ne_zero hq

Premises used: RatFunc.algebraMap_ne_zero
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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⟯) q : K⟮X⟯) (0 : K⟮X⟯)

Tactic:
exact algebraMap_ne_zero hq

Premises used: RatFunc.algebraMap_ne_zero
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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⟯)

Tactic:
algebraMap_ne_zero (mt Polynomial.C_eq_zero.mp ?_)

Premises used: Polynomial.C_eq_zero, RatFunc.algebraMap_ne_zero, mt, Iff.mp
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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 : ¬(q / @gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff⁻¹ = 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⟯)

Tactic:
refine algebraMap_ne_zero (mt Polynomial.C_eq_zero.mp ?_)

Premises used: Polynomial.C_eq_zero, RatFunc.algebraMap_ne_zero, mt, Iff.mp
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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
⊢ ¬(q / @gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff⁻¹ = 0

Tactic:
inv_ne_zero (Polynomial.leadingCoeff_ne_zero.mpr q_div_ne_zero)

Premises used: Iff.mpr, Polynomial.leadingCoeff_ne_zero, inv_ne_zero
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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
⊢ ¬(q / @gcd _ CommSemiring.toCommMonoidWithZero _ p q).leadingCoeff⁻¹ = 0

Tactic:
exact inv_ne_zero (Polynomial.leadingCoeff_ne_zero.mpr q_div_ne_zero)

Premises used: Iff.mpr, Polynomial.leadingCoeff_ne_zero, inv_ne_zero
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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

Tactic:
induction x using RatFunc.induction_on with | _ p q hq

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

Premises used: RatFunc.num_div, RatFunc.denom_div
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
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:
(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)

Premises used: Iff.mpr, Polynomial.C, IsUnit.inv, Ne.isUnit, isCoprime_mul_unit_left, isCoprime_div_gcd_div_gcd, right_div_gcd_ne_zero, Polynomial.leadingCoeff_ne_zero, IsUnit.map
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
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:
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)

Premises used: Iff.mpr, Polynomial.C, IsUnit.inv, Ne.isUnit, isCoprime_mul_unit_left, isCoprime_div_gcd_div_gcd, right_div_gcd_ne_zero, Polynomial.leadingCoeff_ne_zero, IsUnit.map
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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
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))
⊢ IsCoprime x.num 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)

Premises used: RatFunc.num_div, RatFunc.induction_on
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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
rw₃ rw₄ : Eq.{u + 1} (α := K⟮X⟯) 0 0
⊢ x = 0

Tactic:
rw [← num_div_denom x, h, map_zero, zero_div]

Premises used: zero_div, map_zero, RatFunc.num_div_denom
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
hx : x ≠ 0
⊢ x.num ≠ 0

Tactic:
mt num_eq_zero_iff.mp hx

Premises used: mt, RatFunc.num_eq_zero_iff, Iff.mp
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
p q : K[X]
hq : q ≠ 0
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
⊢ 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⟯)

Tactic:
rw [← (algebraMap_injective K).eq_iff, eq_div_iff (algebraMap_ne_zero hq)]

Premises used: Function.Injective.eq_iff, RatFunc.algebraMap_ne_zero, RatFunc.algebraMap_injective, eq_div_iff
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
p q : K[X]
hq : q ≠ 0
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
| 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 [← num_div_denom x]

Premises used: RatFunc.num_div_denom
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
p q : K[X]
hq : q ≠ 0
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
⊢ 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:
conv_rhs => rw [← num_div_denom x]

Premises used: RatFunc.num_div_denom
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
p q : K[X]
hq : q ≠ 0
rw : Ne (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.denom : K⟮X⟯) (0 : K⟮X⟯)
⊢ 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:
rw [map_mul, map_mul, div_eq_mul_inv, mul_assoc, mul_comm (Inv.inv _), ←
    mul_assoc, ← div_eq_mul_inv, div_eq_iff]

Premises used: mul_assoc, div_eq_mul_inv, map_mul, div_eq_iff, Inv.inv, mul_comm
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
p q : K[X]
hq : q ≠ 0
⊢ Ne (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.denom : K⟮X⟯) (0 : K⟮X⟯)

Tactic:
algebraMap_ne_zero (denom_ne_zero x)

Premises used: RatFunc.algebraMap_ne_zero, RatFunc.denom_ne_zero
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
p q : K[X]
hq : q ≠ 0
⊢ Ne (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.denom : K⟮X⟯) (0 : K⟮X⟯)

Tactic:
exact algebraMap_ne_zero (denom_ne_zero x)

Premises used: RatFunc.algebraMap_ne_zero, RatFunc.denom_ne_zero
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
x y : K⟮X⟯
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⟯)
| x + y

Tactic:
rw [← num_div_denom x, ← num_div_denom y]

Premises used: RatFunc.num_div_denom
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
x y : K⟮X⟯
conv_lhs :
  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⟯) =
    HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (x.num * y.denom + x.denom * y.num) : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (x.denom * y.denom) : K⟮X⟯)
⊢ x + y =
    HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (x.num * y.denom + x.denom * y.num) : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (x.denom * y.denom) : K⟮X⟯)

Tactic:
conv_lhs => rw [← num_div_denom x, ← num_div_denom y]

Premises used: RatFunc.num_div_denom
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
x y : K⟮X⟯
hb : Ne (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.denom : K⟮X⟯) (0 : K⟮X⟯)
hd : Ne (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) y.denom : K⟮X⟯) (0 : 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⟯) +
      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⟯) =
    HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (x.num * y.denom + x.denom * y.num) : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (x.denom * y.denom) : K⟮X⟯)

Tactic:
rw [div_add_div, map_mul, map_add, map_mul, map_mul]

Premises used: map_add, map_mul, div_add_div