awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.RatFunc.Degree
Goal:
K : Type u
inst : Field K
rw : HSub.hSub (α := ℤ) (↑(natDegree.{u} (R := K) (num 0)) : ℤ) (↑(natDegree.{u} (R := K) (denom 0)) : ℤ) = 0
rw₁ : HSub.hSub (α := ℤ) (↑(natDegree.{u} (R := K) 0) : ℤ) (↑(natDegree.{u} (R := K) (denom 0)) : ℤ) = 0
rw₂ : HSub.hSub (α := ℤ) (↑0 : ℤ) (↑(natDegree.{u} (R := K) (denom 0)) : ℤ) = 0
rw₃ : HSub.hSub (α := ℤ) (↑0 : ℤ) (↑(natDegree.{u} (R := K) 1) : ℤ) = 0
rw₄ : HSub.hSub (α := ℤ) (↑0 : ℤ) (↑0 : ℤ) = 0
rw₅ rw₆ : Eq (α := ℤ) 0 0
⊢ intDegree.{u} (K := K) 0 = 0

Tactic:
rw [intDegree, num_zero, natDegree_zero, denom_zero, natDegree_one, sub_self]

Premises used: sub_self, RatFunc.num_zero, Polynomial.natDegree_zero, Polynomial.natDegree_one, RatFunc.intDegree, RatFunc.denom_zero
-- Module: Mathlib.FieldTheory.RatFunc.Degree
Goal:
K : Type u
inst : Field K
rw : HSub.hSub (α := ℤ) (↑(natDegree.{u} (R := K) (num 1)) : ℤ) (↑(natDegree.{u} (R := K) (denom 1)) : ℤ) = 0
rw₁ : HSub.hSub (α := ℤ) (↑(natDegree.{u} (R := K) 1) : ℤ) (↑(natDegree.{u} (R := K) (denom 1)) : ℤ) = 0
rw₂ : HSub.hSub (α := ℤ) (↑(natDegree.{u} (R := K) 1) : ℤ) (↑(natDegree.{u} (R := K) 1) : ℤ) = 0
rw₃ rw₄ : Eq (α := ℤ) 0 0
⊢ intDegree.{u} (K := K) 1 = 0

Tactic:
rw [intDegree, num_one, denom_one, sub_self]

Premises used: RatFunc.num_one, RatFunc.denom_one, sub_self, RatFunc.intDegree
-- Module: Mathlib.FieldTheory.RatFunc.Degree
Goal:
K : Type u
inst : Field K
k : K
rw :
  HSub.hSub (α := ℤ) (↑(natDegree.{u} (R := K) (num ((C : (a : K) → K⟮X⟯) k))) : ℤ)
      (↑(natDegree.{u} (R := K) (denom ((C : (a : K) → K⟮X⟯) k))) : ℤ) =
    0
rw₁ :
  HSub.hSub (α := ℤ) (↑(natDegree.{u} (R := K) ((Polynomial.C : (a : K) → K[X]) k)) : ℤ)
      (↑(natDegree.{u} (R := K) (denom ((C : (a : K) → K⟮X⟯) k))) : ℤ) =
    0
rw₂ : HSub.hSub (α := ℤ) (↑0 : ℤ) (↑(natDegree.{u} (R := K) (denom ((C : (a : K) → K⟮X⟯) k))) : ℤ) = 0
rw₃ : HSub.hSub (α := ℤ) (↑0 : ℤ) (↑(natDegree.{u} (R := K) 1) : ℤ) = 0
rw₄ : HSub.hSub (α := ℤ) (↑0 : ℤ) (↑0 : ℤ) = 0
rw₅ rw₆ : Eq (α := ℤ) 0 0
⊢ intDegree.{u} (K := K) ((C : (a : K) → K⟮X⟯) k) = 0

Tactic:
rw [intDegree, num_C, natDegree_C, denom_C, natDegree_one, sub_self]

Premises used: sub_self, RatFunc.num_C, Polynomial.natDegree_C, Polynomial.natDegree_one, RatFunc.denom_C, RatFunc.intDegree
-- Module: Mathlib.FieldTheory.RatFunc.Degree
Goal:
K : Type u
inst : Field K
rw : HSub.hSub (α := ℤ) (↑(natDegree.{u} (R := K) (num X)) : ℤ) (↑(natDegree.{u} (R := K) (denom X)) : ℤ) = 1
rw₁ : HSub.hSub (α := ℤ) (↑(natDegree.{u} (R := K) Polynomial.X) : ℤ) (↑(natDegree.{u} (R := K) (denom X)) : ℤ) = 1
rw₂ : HSub.hSub (α := ℤ) (↑1 : ℤ) (↑(natDegree.{u} (R := K) (denom X)) : ℤ) = 1
rw₃ : HSub.hSub (α := ℤ) (↑1 : ℤ) (↑(natDegree.{u} (R := K) 1) : ℤ) = 1
rw₄ : HSub.hSub (α := ℤ) (↑1 : ℤ) (↑0 : ℤ) = 1
rw₅ : HSub.hSub (α := ℤ) 1 (↑0 : ℤ) = 1
rw₆ : HSub.hSub (α := ℤ) 1 0 = 1
rw₇ rw₈ : Eq (α := ℤ) 1 1
⊢ intDegree.{u} (K := K) X = 1

Tactic:
rw [intDegree, num_X, Polynomial.natDegree_X, denom_X, Polynomial.natDegree_one,
    Int.ofNat_one, Int.ofNat_zero, sub_zero]

Premises used: Polynomial.natDegree_X, sub_zero, RatFunc.num_X, Int.ofNat_zero, RatFunc.denom_X, Polynomial.natDegree_one, Int.ofNat_one, RatFunc.intDegree
-- Module: Mathlib.FieldTheory.RatFunc.Degree
Goal:
K : Type u
inst : Field K
p : K[X]
rw :
  HSub.hSub (α := ℤ) (↑(natDegree.{u} (R := K) (num ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p))) : ℤ)
      (↑(natDegree.{u} (R := K) (denom ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p))) : ℤ) =
    (↑p.natDegree : ℤ)
rw₁ :
  HSub.hSub (α := ℤ) (↑p.natDegree : ℤ)
      (↑(natDegree.{u} (R := K) (denom ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p))) : ℤ) =
    (↑p.natDegree : ℤ)
rw₂ : HSub.hSub (α := ℤ) (↑p.natDegree : ℤ) (↑(natDegree.{u} (R := K) 1) : ℤ) = (↑p.natDegree : ℤ)
rw₃ : HSub.hSub (α := ℤ) (↑p.natDegree : ℤ) (↑0 : ℤ) = (↑p.natDegree : ℤ)
rw₄ : HSub.hSub (α := ℤ) (↑p.natDegree : ℤ) 0 = (↑p.natDegree : ℤ)
rw₅ rw₆ : Eq (α := ℤ) (↑p.natDegree : ℤ) (↑p.natDegree : ℤ)
⊢ intDegree.{u} (K := K) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p) = (↑p.natDegree : ℤ)

Tactic:
rw [intDegree, RatFunc.num_algebraMap, RatFunc.denom_algebraMap, Polynomial.natDegree_one,
    Int.ofNat_zero, sub_zero]

Premises used: sub_zero, RatFunc.num_algebraMap, Int.ofNat_zero, Polynomial.natDegree_one, RatFunc.denom_algebraMap, RatFunc.intDegree
-- Module: Mathlib.FieldTheory.RatFunc.Degree
Goal:
K : Type u
inst : Field K
x y : K⟮X⟯
hx : x ≠ 0
hy : y ≠ 0
simp :
  (↑(x * y).num.natDegree : ℤ) + HAdd.hAdd (α := ℤ) (↑x.denom.natDegree : ℤ) (↑y.denom.natDegree : ℤ) =
    HAdd.hAdd (α := ℤ) (↑x.num.natDegree : ℤ) (↑y.num.natDegree : ℤ) + (↑(x * y).denom.natDegree : ℤ)
⊢ (x * y).intDegree = x.intDegree + y.intDegree

Tactic:
simp only [intDegree, add_sub, sub_add, sub_sub_eq_add_sub, sub_sub, sub_eq_sub_iff_add_eq_add]

Premises used: sub_add, add_sub, sub_sub_eq_add_sub, sub_eq_sub_iff_add_eq_add, sub_sub, RatFunc.intDegree
-- Module: Mathlib.FieldTheory.RatFunc.Degree
Goal:
K : Type u
inst : Field K
x y : K⟮X⟯
hx : x ≠ 0
hy : y ≠ 0
norm_cast :
  (x * y).num.natDegree + (x.denom.natDegree + y.denom.natDegree) =
    x.num.natDegree + y.num.natDegree + (x * y).denom.natDegree
⊢ (↑(x * y).num.natDegree : ℤ) + HAdd.hAdd (α := ℤ) (↑x.denom.natDegree : ℤ) (↑y.denom.natDegree : ℤ) =
    HAdd.hAdd (α := ℤ) (↑x.num.natDegree : ℤ) (↑y.num.natDegree : ℤ) + (↑(x * y).denom.natDegree : ℤ)

Tactic:
norm_cast
-- Module: Mathlib.FieldTheory.RatFunc.Degree
Goal:
K : Type u
inst : Field K
x y : K⟮X⟯
hx : x ≠ 0
hy : y ≠ 0
rw : (x * y).num.natDegree + (x.denom * y.denom).natDegree = x.num.natDegree + y.num.natDegree + (x * y).denom.natDegree
rw₁ : ((x * y).num * (x.denom * y.denom)).natDegree = x.num.natDegree + y.num.natDegree + (x * y).denom.natDegree
rw₂ : ((x * y).num * (x.denom * y.denom)).natDegree = (x.num * y.num).natDegree + (x * y).denom.natDegree
rw₃ : ((x * y).num * (x.denom * y.denom)).natDegree = (x.num * y.num * (x * y).denom).natDegree
rw₄ rw₅ : (x.num * y.num * (x * y).denom).natDegree = (x.num * y.num * (x * y).denom).natDegree
⊢ (x * y).num.natDegree + (x.denom.natDegree + y.denom.natDegree) =
    x.num.natDegree + y.num.natDegree + (x * y).denom.natDegree

Tactic:
rw [← Polynomial.natDegree_mul x.denom_ne_zero y.denom_ne_zero, ←
    Polynomial.natDegree_mul (RatFunc.num_ne_zero (mul_ne_zero hx hy))
      (mul_ne_zero x.denom_ne_zero y.denom_ne_zero),
    ← Polynomial.natDegree_mul (RatFunc.num_ne_zero hx) (RatFunc.num_ne_zero hy), ←
    Polynomial.natDegree_mul (mul_ne_zero (RatFunc.num_ne_zero hx) (RatFunc.num_ne_zero hy))
      (x * y).denom_ne_zero,
    RatFunc.num_denom_mul]

Premises used: HMul.hMul, Polynomial.natDegree_mul, RatFunc.num_ne_zero, RatFunc.num_denom_mul, mul_ne_zero, RatFunc.denom_ne_zero
-- Module: Mathlib.FieldTheory.RatFunc.Degree
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
pos : ∀ (hx : x = 0), x⁻¹.intDegree = -x.intDegree
neg : ∀ (hx : ¬x = 0), x⁻¹.intDegree = -x.intDegree
⊢ x⁻¹.intDegree = -x.intDegree

Tactic:
by_cases hx : x = 0
-- Module: Mathlib.FieldTheory.RatFunc.Degree
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
hx : x = 0
⊢ x⁻¹.intDegree = -x.intDegree

Tactic:
simp [hx, eq_neg_iff_add_eq_zero, ← intDegree_mul (inv_ne_zero hx) hx]

Premises used: eq_neg_iff_add_eq_zero
-- Module: Mathlib.FieldTheory.RatFunc.Degree
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
hx : ¬x = 0
⊢ x⁻¹.intDegree = -x.intDegree

Tactic:
simp [hx, eq_neg_iff_add_eq_zero, ← intDegree_mul (inv_ne_zero hx) hx]

Premises used: RatFunc.intDegree_mul, inv_ne_zero, eq_neg_iff_add_eq_zero
-- Module: Mathlib.FieldTheory.RatFunc.Degree
Goal:
K : Type u
inst : Field K
x y : K⟮X⟯
hx : x ≠ 0
hy : y ≠ 0
hx₁ : x ≠ 0
hy₁ : y⁻¹ ≠ 0
⊢ (x / y).intDegree = x.intDegree - y.intDegree

Tactic:
rw [div_eq_mul_inv, intDegree_mul, intDegree_inv, ← sub_eq_add_neg]

Premises used: sub_eq_add_neg, RatFunc.intDegree_inv, RatFunc.intDegree_mul, div_eq_mul_inv
-- Module: Mathlib.FieldTheory.RatFunc.Degree
Goal:
K : Type u
inst : Field K
x y : K⟮X⟯
hx : x ≠ 0
hy : y ≠ 0
⊢ x ≠ 0

Tactic:
grind
-- Module: Mathlib.FieldTheory.RatFunc.Degree
Goal:
K : Type u
inst : Field K
x y : K⟮X⟯
hx : x ≠ 0
hy : y ≠ 0
⊢ y⁻¹ ≠ 0

Tactic:
grind
-- Module: Mathlib.FieldTheory.RatFunc.Degree
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
pos : ∀ (hx : x = 0), (-x).intDegree = x.intDegree
neg : ∀ (hx : ¬x = 0), (-x).intDegree = x.intDegree
⊢ (-x).intDegree = x.intDegree

Tactic:
by_cases hx : x = 0
-- Module: Mathlib.FieldTheory.RatFunc.Degree
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
hx : x = 0
pos : intDegree.{u} (K := K) (-0) = intDegree.{u} (K := K) 0
pos₁ pos₂ : intDegree.{u} (K := K) 0 = intDegree.{u} (K := K) 0
⊢ (-x).intDegree = x.intDegree

Tactic:
rw [hx, neg_zero]

Premises used: neg_zero
-- Module: Mathlib.FieldTheory.RatFunc.Degree
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
hx : ¬x = 0
neg :
  HSub.hSub (α := ℤ) (↑(-x).num.natDegree : ℤ) (↑(-x).denom.natDegree : ℤ) =
    HSub.hSub (α := ℤ) (↑(-x.num).natDegree : ℤ) (↑x.denom.natDegree : ℤ)
⊢ (-x).intDegree = x.intDegree

Tactic:
rw [intDegree, intDegree, ← natDegree_neg x.num]

Premises used: RatFunc.num, RatFunc.intDegree, Polynomial.natDegree_neg
-- Module: Mathlib.FieldTheory.RatFunc.Degree
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
hx : ¬x = 0
⊢ HSub.hSub (α := ℤ) (↑(-x).num.natDegree : ℤ) (↑(-x).denom.natDegree : ℤ) =
    HSub.hSub (α := ℤ) (↑(-x.num).natDegree : ℤ) (↑x.denom.natDegree : ℤ)

Tactic:
natDegree_sub_eq_of_prod_eq (num_ne_zero (neg_ne_zero.mpr hx)) (denom_ne_zero (-x))
        (neg_ne_zero.mpr (num_ne_zero hx)) (denom_ne_zero x) (num_denom_neg x)

Premises used: Iff.mpr, RatFunc.num_ne_zero, neg_ne_zero, Polynomial.natDegree_sub_eq_of_prod_eq, Neg.neg, RatFunc.denom_ne_zero, RatFunc.num_denom_neg
-- Module: Mathlib.FieldTheory.RatFunc.Degree
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
hx : ¬x = 0
⊢ HSub.hSub (α := ℤ) (↑(-x).num.natDegree : ℤ) (↑(-x).denom.natDegree : ℤ) =
    HSub.hSub (α := ℤ) (↑(-x.num).natDegree : ℤ) (↑x.denom.natDegree : ℤ)

Tactic:
exact
      natDegree_sub_eq_of_prod_eq (num_ne_zero (neg_ne_zero.mpr hx)) (denom_ne_zero (-x))
        (neg_ne_zero.mpr (num_ne_zero hx)) (denom_ne_zero x) (num_denom_neg x)

Premises used: Iff.mpr, RatFunc.num_ne_zero, neg_ne_zero, Polynomial.natDegree_sub_eq_of_prod_eq, Neg.neg, RatFunc.denom_ne_zero, RatFunc.num_denom_neg
-- Module: Mathlib.FieldTheory.RatFunc.Degree
Goal:
K : Type u
inst : Field K
x y : K⟮X⟯
hxy : x + y ≠ 0
⊢ (x + y).intDegree =
    HSub.hSub (α := ℤ) (↑(x.num * y.denom + x.denom * y.num).natDegree : ℤ) (↑(x.denom * y.denom).natDegree : ℤ)

Tactic:
natDegree_sub_eq_of_prod_eq (num_ne_zero hxy) (x + y).denom_ne_zero
    (num_mul_denom_add_denom_mul_num_ne_zero hxy) (mul_ne_zero x.denom_ne_zero y.denom_ne_zero)
    (num_denom_add x y)

Premises used: RatFunc.num_mul_denom_add_denom_mul_num_ne_zero, RatFunc.num_denom_add, RatFunc.num_ne_zero, HAdd.hAdd, RatFunc.intDegree, mul_ne_zero, Polynomial.natDegree_sub_eq_of_prod_eq, RatFunc.denom_ne_zero
-- Module: Mathlib.FieldTheory.RatFunc.Degree
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
hx : x ≠ 0
s : K[X]
hs : s ≠ 0
apply : x.num * s * x.denom = x.num * (s * x.denom)
⊢ HSub.hSub (α := ℤ) (↑(x.num * s).natDegree : ℤ) (↑(s * x.denom).natDegree : ℤ) = x.intDegree

Tactic:
apply natDegree_sub_eq_of_prod_eq (mul_ne_zero (num_ne_zero hx) hs)
    (mul_ne_zero hs x.denom_ne_zero) (num_ne_zero hx) x.denom_ne_zero

Premises used: RatFunc.num_ne_zero, mul_ne_zero, Polynomial.natDegree_sub_eq_of_prod_eq, RatFunc.denom_ne_zero
-- Module: Mathlib.FieldTheory.RatFunc.Degree
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
hx : x ≠ 0
s : K[X]
hs : s ≠ 0
rw rw₁ : x.num * (s * x.denom) = x.num * (s * x.denom)
⊢ x.num * s * x.denom = x.num * (s * x.denom)

Tactic:
rw [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.FieldTheory.RatFunc.Degree
Goal:
K : Type u
inst : Field K
x y : K⟮X⟯
hy : y ≠ 0
hxy : x + y ≠ 0
pos : ∀ (hx : x = 0), (x + y).intDegree ≤ max x.intDegree y.intDegree
neg : ∀ (hx : ¬x = 0), (x + y).intDegree ≤ max x.intDegree y.intDegree
⊢ (x + y).intDegree ≤ max x.intDegree y.intDegree

Tactic:
by_cases hx : x = 0
-- Module: Mathlib.FieldTheory.RatFunc.Degree
Goal:
K : Type u
inst : Field K
x y : K⟮X⟯
hy : y ≠ 0
hxy : x + y ≠ 0
hx : x = 0
⊢ (x + y).intDegree ≤ max x.intDegree y.intDegree

Tactic:
simp [hx]
-- Module: Mathlib.FieldTheory.RatFunc.Degree
Goal:
K : Type u
inst : Field K
x y : K⟮X⟯
hy : y ≠ 0
hxy : x + y ≠ 0
hx : ¬x = 0
neg : (x.num * y.denom + x.denom * y.num).natDegree ≤ max (x.num * y.denom).natDegree (x.denom * y.num).natDegree
⊢ (x + y).intDegree ≤ max x.intDegree y.intDegree

Tactic:
rw [intDegree_add hxy, ←
    natDegree_num_mul_right_sub_natDegree_denom_mul_left_eq_intDegree hx y.denom_ne_zero,
    mul_comm y.denom, ←
    natDegree_num_mul_right_sub_natDegree_denom_mul_left_eq_intDegree hy x.denom_ne_zero,
    le_max_iff, sub_le_sub_iff_right, Int.ofNat_le, sub_le_sub_iff_right, Int.ofNat_le, ←
    le_max_iff, mul_comm y.num]

Premises used: RatFunc.denom, sub_le_sub_iff_right, RatFunc.intDegree_add, RatFunc.num, RatFunc.natDegree_num_mul_right_sub_natDegree_denom_mul_left_eq_intDegree, mul_comm, Int.ofNat_le, le_max_iff, RatFunc.denom_ne_zero
-- Module: Mathlib.FieldTheory.RatFunc.Degree
Goal:
K : Type u
inst : Field K
x y : K⟮X⟯
hy : y ≠ 0
hxy : x + y ≠ 0
hx : ¬x = 0
⊢ (x.num * y.denom + x.denom * y.num).natDegree ≤ max (x.num * y.denom).natDegree (x.denom * y.num).natDegree

Tactic:
natDegree_add_le _ _

Premises used: Polynomial.natDegree_add_le
-- Module: Mathlib.FieldTheory.RatFunc.Degree
Goal:
K : Type u
inst : Field K
x y : K⟮X⟯
hy : y ≠ 0
hxy : x + y ≠ 0
hx : ¬x = 0
⊢ (x.num * y.denom + x.denom * y.num).natDegree ≤ max (x.num * y.denom).natDegree (x.denom * y.num).natDegree

Tactic:
exact natDegree_add_le _ _

Premises used: Polynomial.natDegree_add_le
-- Module: Mathlib.FieldTheory.RatFunc.IntermediateField
Goal:
K : Type u_1
inst : Field K
g : K⟮X⟯
h : Membership.mem (γ := IntermediateField K K⟮X⟯) ⊤ g
⊢ g =
    HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((aeval X : (a : K[X]) → K⟮X⟯) g.num : K⟮X⟯)
      ((aeval X : (a : K[X]) → K⟮X⟯) g.denom : K⟮X⟯)

Tactic:
simp
-- Module: Mathlib.FieldTheory.RatFunc.IntermediateField
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
rw : LE.le (α := IntermediateField K K⟮X⟯) ⊤ (IntermediateField.adjoin K ((↑E : Set K⟮X⟯) ∪ {X}))
⊢ Eq (α := IntermediateField (↥E) K⟮X⟯) (↥E)⟮ X⟯ ⊤

Tactic:
rw [← restrictScalars_eq_top_iff (K := K), IntermediateField.restrictScalars_adjoin,
    _root_.eq_top_iff]

Premises used: eq_top_iff, IntermediateField.restrictScalars_eq_top_iff, IntermediateField.restrictScalars_adjoin
-- Module: Mathlib.FieldTheory.RatFunc.IntermediateField
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
⊢ {X} ⊆ (↑E : Set K⟮X⟯) ∪ {X}

Tactic:
simp
-- Module: Mathlib.FieldTheory.RatFunc.IntermediateField
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
⊢ LE.le (α := IntermediateField K K⟮X⟯) ⊤ (IntermediateField.adjoin K ((↑E : Set K⟮X⟯) ∪ {X}))

Tactic:
exact le_trans (le_of_eq RatFunc.adjoin_X.symm) (adjoin.mono _ _ _ (by simp))

Premises used: IntermediateField.adjoin.mono, RatFunc.adjoin_X, le_of_eq, Eq.symm, le_trans
-- Module: Mathlib.FieldTheory.RatFunc.IntermediateField
Goal:
K : Type u_1
inst : Field K
f : K⟮X⟯
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra K A
inst_3 : Algebra.{u_1, u_2} (↥K[f]) A
B : Type u_3
inst_4 : CommRing B
inst_5 : Algebra K B
inst_6 : Algebra.{u_1, u_3} (↥K[f]) B
inst_7 : Algebra A B
inst_8 : IsScalarTower K A B
inst_9 : IsScalarTower.{u_1, u_2, u_3} (↥K[f]) A B
⊢ Eq (α := B[X]) (Polynomial.map (algebraMap A B) (f.minpolyX A)) (f.minpolyX B)

Tactic:
simp [minpolyX, Polynomial.map_map, ← IsScalarTower.algebraMap_eq,
    ← IsScalarTower.algebraMap_apply]

Premises used: RatFunc.minpolyX, IsScalarTower.algebraMap_eq, Polynomial.map_map, IsScalarTower.algebraMap_apply
-- Module: Mathlib.FieldTheory.RatFunc.IntermediateField
Goal:
K : Type u_1
inst : Field K
x : K
⊢ Eq.{u_1 + 1} (α := (↥K⟮((C : (a : K) → K⟮X⟯) x : K⟮X⟯)⟯)[X])
    (minpolyX (K := K) ((C : (a : K) → K⟮X⟯) x) ↥K⟮((C : (a : K) → K⟮X⟯) x : K⟮X⟯)⟯) 0

Tactic:
simp [minpolyX, sub_eq_zero, Subtype.ext_iff]

Premises used: sub_eq_zero, RatFunc.minpolyX, Subtype.ext_iff
-- Module: Mathlib.FieldTheory.RatFunc.IntermediateField
Goal:
K : Type u_1
inst : Field K
f : K⟮X⟯
simp :
  HSub.hSub (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) f.num : K⟮X⟯)
      (HMul.hMul (β := K⟮X⟯) f ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) f.denom : K⟮X⟯)) =
    0
⊢ Eq (α := K⟮X⟯) ((aeval X : (a : (↥K⟮f⟯)[X]) → K⟮X⟯) (f.minpolyX ↥K⟮f⟯) : K⟮X⟯) (0 : K⟮X⟯)

Tactic:
simp only [aeval_sub, aeval_map_algebraMap, aeval_X_left_eq_algebraMap, map_mul, aeval_C,
    IntermediateField.algebraMap_apply, coe_algebraMap]

Premises used: Polynomial.aeval_map_algebraMap, IntermediateField.algebraMap_apply, map_mul, Polynomial.aeval_C, RatFunc.aeval_X_left_eq_algebraMap, Polynomial.aeval_sub, IntermediateField.algebraAdjoinAdjoin.coe_algebraMap
-- Module: Mathlib.FieldTheory.RatFunc.IntermediateField
Goal:
K : Type u_1
inst : Field K
f : K⟮X⟯
nth_rw :
  HSub.hSub (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) f.num : K⟮X⟯)
      (HMul.hMul (β := K⟮X⟯)
        (HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) f.num : K⟮X⟯)
          ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) f.denom : K⟮X⟯))
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) f.denom : K⟮X⟯)) =
    0
⊢ HSub.hSub (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) f.num : K⟮X⟯)
      (HMul.hMul (β := K⟮X⟯) f ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) f.denom : K⟮X⟯)) =
    0

Tactic:
nth_rw 2 [← num_div_denom f]

Premises used: RatFunc.num_div_denom
-- Module: Mathlib.FieldTheory.RatFunc.IntermediateField
Goal:
K : Type u_1
inst : Field K
f : K⟮X⟯
rw :
  HSub.hSub (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) f.num : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) f.num : K⟮X⟯) =
    0
⊢ HSub.hSub (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) f.num : K⟮X⟯)
      (HMul.hMul (β := K⟮X⟯)
        (HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) f.num : K⟮X⟯)
          ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) f.denom : K⟮X⟯))
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) f.denom : K⟮X⟯)) =
    0

Tactic:
rw [div_mul_cancel₀ _ (algebraMap_ne_zero f.denom_ne_zero)]

Premises used: div_mul_cancel₀, RatFunc.algebraMap_ne_zero, RatFunc.denom_ne_zero
-- Module: Mathlib.FieldTheory.RatFunc.IntermediateField
Goal:
K : Type u_1
inst : Field K
f : K⟮X⟯
⊢ HSub.hSub (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) f.num : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) f.num : K⟮X⟯) =
    0

Tactic:
sub_self _

Premises used: sub_self
-- Module: Mathlib.FieldTheory.RatFunc.IntermediateField
Goal:
K : Type u_1
inst : Field K
f : K⟮X⟯
⊢ HSub.hSub (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) f.num : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) f.num : K⟮X⟯) =
    0

Tactic:
exact sub_self _

Premises used: sub_self
-- Module: Mathlib.FieldTheory.RatFunc.IntermediateField
Goal:
K : Type u_1
inst : Field K
f : K⟮X⟯
hf : Eq (α := K⟮X⟯) (↑(coeff (f.minpolyX ↥K⟮f⟯) f.denom.natDegree) : K⟮X⟯) 0
h : f = (C : (a : K) → K⟮X⟯) (f.num.coeff f.denom.natDegree / f.denom.leadingCoeff)
⊢ ∃ (c : K), f = (C : (a : K) → K⟮X⟯) c

Tactic:
use f.num.coeff f.denom.natDegree / f.denom.leadingCoeff

Premises used: RatFunc.denom, Polynomial.leadingCoeff, Polynomial.coeff, RatFunc.num, Polynomial.natDegree
-- Module: Mathlib.FieldTheory.RatFunc.IntermediateField
Goal:
K : Type u_1
inst : Field K
f : K⟮X⟯
hf : Eq (α := K⟮X⟯) (↑(coeff (f.minpolyX ↥K⟮f⟯) f.denom.natDegree) : K⟮X⟯) 0
h :
  (C : (a : K) → K⟮X⟯) (f.num.coeff f.denom.natDegree) =
    HMul.hMul (β := K⟮X⟯) f ((C : (a : K) → K⟮X⟯) f.denom.leadingCoeff : K⟮X⟯)
⊢ f = (C : (a : K) → K⟮X⟯) (f.num.coeff f.denom.natDegree / f.denom.leadingCoeff)

Tactic:
rw [map_div₀, eq_div_iff ((_root_.map_ne_zero C).mpr
    (leadingCoeff_ne_zero.mpr f.denom_ne_zero)), eq_comm]

Premises used: Iff.mpr, RatFunc.C, eq_comm, map_div₀, Polynomial.leadingCoeff_ne_zero, map_ne_zero, eq_div_iff, RatFunc.denom_ne_zero
-- Module: Mathlib.FieldTheory.RatFunc.IntermediateField
Goal:
K : Type u_1
inst : Field K
f : K⟮X⟯
hf : Eq (α := K⟮X⟯) (↑(coeff (f.minpolyX ↥K⟮f⟯) f.denom.natDegree) : K⟮X⟯) 0
⊢ (C : (a : K) → K⟮X⟯) (f.num.coeff f.denom.natDegree) =
    HMul.hMul (β := K⟮X⟯) f ((C : (a : K) → K⟮X⟯) f.denom.leadingCoeff : K⟮X⟯)

Tactic:
simpa [sub_eq_zero] using hf

Premises used: sub_eq_zero
-- Module: Mathlib.FieldTheory.RatFunc.IntermediateField
Goal:
K : Type u_1
inst : Field K
f : K⟮X⟯
h : Eq (α := (↥K⟮f⟯)[X]) (f.minpolyX ↥K⟮f⟯) 0
⊢ Eq (α := K⟮X⟯) (↑(coeff (f.minpolyX ↥K⟮f⟯) f.denom.natDegree) : K⟮X⟯) 0

Tactic:
simp [h]
-- Module: Mathlib.FieldTheory.RatFunc.IntermediateField
Goal:
K : Type u_1
inst : Field K
c : K
⊢ Eq.{u_1 + 1} (α := (↥K⟮((C : (a : K) → K⟮X⟯) c : K⟮X⟯)⟯)[X])
    (minpolyX (K := K) ((C : (a : K) → K⟮X⟯) c) ↥K⟮((C : (a : K) → K⟮X⟯) c : K⟮X⟯)⟯) 0

Tactic:
simp
-- Module: Mathlib.FieldTheory.RatFunc.IntermediateField
Goal:
K : Type u_1
inst : Field K
f : K⟮X⟯
hf : ¬∃ (c : K), f = (C : (a : K) → K⟮X⟯) c
⊢ Algebra.IsAlgebraic.{u_1, u_1} ↥K⟮f⟯ ↥(↥K⟮f⟯)⟮ X⟯

Tactic:
have : Algebra.IsAlgebraic K⟮f⟯ K⟮f⟯⟮(X : K⟮X⟯)⟯ :=
    isAlgebraic_adjoin_simple <| isAlgebraic_iff_isIntegral.mp <| f.isAlgebraic_adjoin_simple_X hf
-- Module: Mathlib.FieldTheory.RatFunc.IntermediateField
Goal:
K : Type u_1
inst : Field K
f : K⟮X⟯
hf : ¬∃ (c : K), f = (C : (a : K) → K⟮X⟯) c
this : Algebra.IsAlgebraic.{u_1, u_1} ↥K⟮f⟯ ↥(↥K⟮f⟯)⟮ X⟯
⊢ Algebra.IsAlgebraic.{u_1, u_1} (↥K⟮f⟯) K⟮X⟯

Tactic:
(IntermediateField.adjoinXEquiv K⟮f⟯).isAlgebraic

Premises used: AlgEquiv.isAlgebraic, IntermediateField.adjoin, RatFunc.IntermediateField.adjoinXEquiv, Singleton.singleton
-- Module: Mathlib.FieldTheory.RatFunc.IntermediateField
Goal:
K : Type u_1
inst : Field K
f : K⟮X⟯
hf : ¬∃ (c : K), f = (C : (a : K) → K⟮X⟯) c
this : Algebra.IsAlgebraic.{u_1, u_1} ↥K⟮f⟯ ↥(↥K⟮f⟯)⟮ X⟯
⊢ Algebra.IsAlgebraic.{u_1, u_1} (↥K⟮f⟯) K⟮X⟯

Tactic:
exact (IntermediateField.adjoinXEquiv K⟮f⟯).isAlgebraic

Premises used: AlgEquiv.isAlgebraic, IntermediateField.adjoin, RatFunc.IntermediateField.adjoinXEquiv, Singleton.singleton
-- Module: Mathlib.FieldTheory.RatFunc.IntermediateField
Goal:
K : Type u_1
inst : Field K
f : K⟮X⟯
hf : ¬∃ (c : K), f = (C : (a : K) → K⟮X⟯) c
⊢ f.denom.natDegree ≤ natDegree (R := ↥K⟮f⟯) (f.minpolyX ↥K⟮f⟯)

Tactic:
le_natDegree_of_ne_zero fun H ↦ hf (f.eq_C_of_minpolyX_coeff_eq_zero congr($(H).val))

Premises used: congrArg, RatFunc.eq_C_of_minpolyX_coeff_eq_zero, id, Polynomial.le_natDegree_of_ne_zero, Subtype.val
-- Module: Mathlib.FieldTheory.RatFunc.IntermediateField
Goal:
K : Type u_1
inst : Field K
hf : ¬∃ (c : K), Eq (α := K⟮X⟯) (0 : K⟮X⟯) ((C : (a : K) → K⟮X⟯) c : K⟮X⟯)
⊢ False

Tactic:
hf ⟨0, (RingHom.map_zero C).symm⟩

Premises used: RatFunc.C, RingHom.map_zero, Exists.intro, OfNat.ofNat, Eq.symm
-- Module: Mathlib.FieldTheory.RatFunc.IntermediateField
Goal:
K : Type u_1
inst : Field K
hf : ¬∃ (c : K), Eq (α := K⟮X⟯) (0 : K⟮X⟯) ((C : (a : K) → K⟮X⟯) c : K⟮X⟯)
⊢ False

Tactic:
exact hf ⟨0, (RingHom.map_zero C).symm⟩

Premises used: RatFunc.C, RingHom.map_zero, Exists.intro, OfNat.ofNat, Eq.symm
-- Module: Mathlib.FieldTheory.RatFunc.IntermediateField
Goal:
K : Type u_1
inst : Field K
f : K⟮X⟯
hf : ¬∃ (c : K), f = (C : (a : K) → K⟮X⟯) c
⊢ f ≠ 0

Tactic:
have f_ne_zero : f ≠ 0 := by
    rintro rfl
    exact hf ⟨0, (RingHom.map_zero C).symm⟩
-- Module: Mathlib.FieldTheory.RatFunc.IntermediateField
Goal:
K : Type u_1
inst : Field K
f : K⟮X⟯
hf : ¬∃ (c : K), f = (C : (a : K) → K⟮X⟯) c
f_ne_zero : f ≠ 0
h : Ne (α := ↥K⟮f⟯) (coeff (f.minpolyX ↥K⟮f⟯) f.num.natDegree) 0
⊢ f.num.natDegree ≤ natDegree (R := ↥K⟮f⟯) (f.minpolyX ↥K⟮f⟯)

Tactic:
apply le_natDegree_of_ne_zero

Premises used: Polynomial.le_natDegree_of_ne_zero
-- Module: Mathlib.FieldTheory.RatFunc.IntermediateField
Goal:
K : Type u_1
inst : Field K
f : K⟮X⟯
hf : ¬∃ (c : K), f = (C : (a : K) → K⟮X⟯) c
f_ne_zero : f ≠ 0
H : Eq (α := ↥K⟮f⟯) (coeff (f.minpolyX ↥K⟮f⟯) f.num.natDegree) 0
⊢ Eq (α := K⟮X⟯) (↑(coeff (f.minpolyX ↥K⟮f⟯) f.num.natDegree) : K⟮X⟯) (↑0 : K⟮X⟯)

Tactic:
replace H := congr($(H).val)