awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Degree (goal)
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
⊢ intDegree.{u} (K := K) X = 1
have rw₅ : HSub.hSub (α := ℤ) 1 (↑0 : ℤ) = 1
Tactic: rw [intDegree, num_X, Polynomial.natDegree_X, denom_X, Polynomial.natDegree_one,
    Int.ofNat_one, Int.ofNat_zero, sub_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Degree (goal)
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
⊢ intDegree.{u} (K := K) X = 1
have rw₆ : HSub.hSub (α := ℤ) 1 0 = 1
Tactic: rw [intDegree, num_X, Polynomial.natDegree_X, denom_X, Polynomial.natDegree_one,
    Int.ofNat_one, Int.ofNat_zero, sub_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Degree (goal)
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
⊢ intDegree.{u} (K := K) X = 1
have rw₇ : Eq (α := ℤ) 1 1
Tactic: rw [intDegree, num_X, Polynomial.natDegree_X, denom_X, Polynomial.natDegree_one,
    Int.ofNat_one, Int.ofNat_zero, sub_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Degree (goal)
Goal:
K : Type u
inst : Field K
p : K[X]
⊢ intDegree.{u} (K := K) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p) = (↑p.natDegree : ℤ)
have 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 : ℤ)
Tactic: rw [intDegree, RatFunc.num_algebraMap, RatFunc.denom_algebraMap, Polynomial.natDegree_one,
    Int.ofNat_zero, sub_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Degree (goal)
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 : ℤ)
⊢ intDegree.{u} (K := K) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p) = (↑p.natDegree : ℤ)
have rw₁ : HSub.hSub (α := ℤ) (↑p.natDegree : ℤ)
    (↑(natDegree.{u} (R := K) (denom ((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]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Degree (goal)
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 : ℤ)
⊢ intDegree.{u} (K := K) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p) = (↑p.natDegree : ℤ)
have rw₂ : HSub.hSub (α := ℤ) (↑p.natDegree : ℤ) (↑(natDegree.{u} (R := K) 1) : ℤ) = (↑p.natDegree : ℤ)
Tactic: rw [intDegree, RatFunc.num_algebraMap, RatFunc.denom_algebraMap, Polynomial.natDegree_one,
    Int.ofNat_zero, sub_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Degree (goal)
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 : ℤ)
⊢ intDegree.{u} (K := K) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p) = (↑p.natDegree : ℤ)
have rw₃ : HSub.hSub (α := ℤ) (↑p.natDegree : ℤ) (↑0 : ℤ) = (↑p.natDegree : ℤ)
Tactic: rw [intDegree, RatFunc.num_algebraMap, RatFunc.denom_algebraMap, Polynomial.natDegree_one,
    Int.ofNat_zero, sub_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Degree (goal)
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 : ℤ)
⊢ intDegree.{u} (K := K) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p) = (↑p.natDegree : ℤ)
have rw₄ : HSub.hSub (α := ℤ) (↑p.natDegree : ℤ) 0 = (↑p.natDegree : ℤ)
Tactic: rw [intDegree, RatFunc.num_algebraMap, RatFunc.denom_algebraMap, Polynomial.natDegree_one,
    Int.ofNat_zero, sub_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Degree (goal)
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 : ℤ)
⊢ intDegree.{u} (K := K) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p) = (↑p.natDegree : ℤ)
have rw₅ : Eq (α := ℤ) (↑p.natDegree : ℤ) (↑p.natDegree : ℤ)
Tactic: rw [intDegree, RatFunc.num_algebraMap, RatFunc.denom_algebraMap, Polynomial.natDegree_one,
    Int.ofNat_zero, sub_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Degree (goal)
Goal:
K : Type u
inst : Field K
x y : K⟮X⟯
hx : x ≠ 0
hy : y ≠ 0
⊢ (x * y).intDegree = x.intDegree + y.intDegree
have 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 : ℤ)
Tactic: simp only [intDegree, add_sub, sub_add, sub_sub_eq_add_sub, sub_sub, sub_eq_sub_iff_add_eq_add]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Degree (goal)
Goal:
K : Type u
inst : Field K
x y : K⟮X⟯
hx : x ≠ 0
hy : y ≠ 0
⊢ (↑(x * y).num.natDegree : ℤ) + HAdd.hAdd (α := ℤ) (↑x.denom.natDegree : ℤ) (↑y.denom.natDegree : ℤ) =
    HAdd.hAdd (α := ℤ) (↑x.num.natDegree : ℤ) (↑y.num.natDegree : ℤ) + (↑(x * y).denom.natDegree : ℤ)
have norm_cast : (x * y).num.natDegree + (x.denom.natDegree + y.denom.natDegree) =
  x.num.natDegree + y.num.natDegree + (x * y).denom.natDegree
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Degree (goal)
Goal:
K : Type u
inst : Field K
x y : K⟮X⟯
hx : x ≠ 0
hy : y ≠ 0
⊢ (x * y).num.natDegree + (x.denom.natDegree + y.denom.natDegree) =
    x.num.natDegree + y.num.natDegree + (x * y).denom.natDegree
have rw : (x * y).num.natDegree + (x.denom * 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]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Degree (goal)
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
⊢ (x * y).num.natDegree + (x.denom.natDegree + y.denom.natDegree) =
    x.num.natDegree + y.num.natDegree + (x * y).denom.natDegree
have rw₁ : ((x * y).num * (x.denom * 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]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Degree (goal)
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
⊢ (x * y).num.natDegree + (x.denom.natDegree + y.denom.natDegree) =
    x.num.natDegree + y.num.natDegree + (x * y).denom.natDegree
have rw₂ : ((x * y).num * (x.denom * y.denom)).natDegree = (x.num * 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]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Degree (goal)
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
⊢ (x * y).num.natDegree + (x.denom.natDegree + y.denom.natDegree) =
    x.num.natDegree + y.num.natDegree + (x * y).denom.natDegree
have rw₃ : ((x * y).num * (x.denom * y.denom)).natDegree = (x.num * y.num * (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]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Degree (goal)
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
⊢ (x * y).num.natDegree + (x.denom.natDegree + y.denom.natDegree) =
    x.num.natDegree + y.num.natDegree + (x * y).denom.natDegree
have rw₄ : (x.num * y.num * (x * y).denom).natDegree = (x.num * y.num * (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]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Degree (goal)
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
⊢ x⁻¹.intDegree = -x.intDegree
have pos : ∀ (hx : x = 0), x⁻¹.intDegree = -x.intDegree
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Degree (goal)
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
pos : ∀ (hx : x = 0), x⁻¹.intDegree = -x.intDegree
⊢ x⁻¹.intDegree = -x.intDegree
have neg : ∀ (hx : ¬x = 0), x⁻¹.intDegree = -x.intDegree
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Degree (goal)
Goal:
K : Type u
inst : Field K
x y : K⟮X⟯
hx : x ≠ 0
hy : y ≠ 0
hx₁ : x ≠ 0
⊢ (x / y).intDegree = x.intDegree - y.intDegree
have hy₁ : y⁻¹ ≠ 0
Tactic: rw [div_eq_mul_inv, intDegree_mul, intDegree_inv, ← sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Degree (goal)
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
⊢ (-x).intDegree = x.intDegree
have pos : ∀ (hx : x = 0), (-x).intDegree = x.intDegree
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Degree (goal)
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
pos : ∀ (hx : x = 0), (-x).intDegree = x.intDegree
⊢ (-x).intDegree = x.intDegree
have neg : ∀ (hx : ¬x = 0), (-x).intDegree = x.intDegree
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Degree (goal)
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
hx : x = 0
⊢ (-x).intDegree = x.intDegree
have pos : intDegree.{u} (K := K) (-0) = intDegree.{u} (K := K) 0
Tactic: rw [hx, neg_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Degree (goal)
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
hx : x = 0
pos : intDegree.{u} (K := K) (-0) = intDegree.{u} (K := K) 0
⊢ (-x).intDegree = x.intDegree
have pos₁ : intDegree.{u} (K := K) 0 = intDegree.{u} (K := K) 0
Tactic: rw [hx, neg_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Degree (goal)
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
hx : ¬x = 0
⊢ (-x).intDegree = x.intDegree
have neg : HSub.hSub (α := ℤ) (↑(-x).num.natDegree : ℤ) (↑(-x).denom.natDegree : ℤ) =
  HSub.hSub (α := ℤ) (↑(-x.num).natDegree : ℤ) (↑x.denom.natDegree : ℤ)
Tactic: rw [intDegree, intDegree, ← natDegree_neg x.num]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Degree (goal)
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
hx : x ≠ 0
s : K[X]
hs : s ≠ 0
⊢ HSub.hSub (α := ℤ) (↑(x.num * s).natDegree : ℤ) (↑(s * x.denom).natDegree : ℤ) = x.intDegree
have apply : x.num * s * x.denom = x.num * (s * x.denom)
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
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Degree (goal)
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
hx : x ≠ 0
s : K[X]
hs : s ≠ 0
⊢ x.num * s * x.denom = x.num * (s * x.denom)
have rw : x.num * (s * x.denom) = x.num * (s * x.denom)
Tactic: rw [mul_assoc]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Degree (goal)
Goal:
K : Type u
inst : Field K
x y : K⟮X⟯
hy : y ≠ 0
hxy : x + y ≠ 0
⊢ (x + y).intDegree ≤ max x.intDegree y.intDegree
have pos : ∀ (hx : x = 0), (x + y).intDegree ≤ max x.intDegree y.intDegree
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Degree (goal)
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
⊢ (x + y).intDegree ≤ max x.intDegree y.intDegree
have neg : ∀ (hx : ¬x = 0), (x + y).intDegree ≤ max x.intDegree y.intDegree
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Degree (goal)
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
have neg : (x.num * y.denom + x.denom * y.num).natDegree ≤ max (x.num * y.denom).natDegree (x.denom * y.num).natDegree
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]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.IntermediateField (goal)
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
⊢ Eq (α := IntermediateField (↥E) K⟮X⟯) (↥E)⟮ X⟯ ⊤
have rw : LE.le (α := IntermediateField K K⟮X⟯) ⊤ (IntermediateField.adjoin K ((↑E : Set K⟮X⟯) ∪ {X}))
Tactic: rw [← restrictScalars_eq_top_iff (K := K), IntermediateField.restrictScalars_adjoin,
    _root_.eq_top_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.IntermediateField (goal)
Goal:
K : Type u_1
inst : Field K
f : K⟮X⟯
⊢ Eq (α := K⟮X⟯) ((aeval X : (a : (↥K⟮f⟯)[X]) → K⟮X⟯) (f.minpolyX ↥K⟮f⟯) : K⟮X⟯) (0 : K⟮X⟯)
have 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
Tactic: simp only [aeval_sub, aeval_map_algebraMap, aeval_X_left_eq_algebraMap, map_mul, aeval_C,
    IntermediateField.algebraMap_apply, coe_algebraMap]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.IntermediateField (goal)
Goal:
K : Type u_1
inst : Field K
f : K⟮X⟯
⊢ 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
have 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
Tactic: nth_rw 2 [← num_div_denom f]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.IntermediateField (goal)
Goal:
K : Type u_1
inst : Field K
f : K⟮X⟯
⊢ 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
have 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
Tactic: rw [div_mul_cancel₀ _ (algebraMap_ne_zero f.denom_ne_zero)]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.IntermediateField (goal)
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 : K), f = (C : (a : K) → K⟮X⟯) c
have h : f = (C : (a : K) → K⟮X⟯) (f.num.coeff f.denom.natDegree / f.denom.leadingCoeff)
Tactic: use f.num.coeff f.denom.natDegree / f.denom.leadingCoeff
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.IntermediateField (goal)
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
⊢ f = (C : (a : K) → K⟮X⟯) (f.num.coeff f.denom.natDegree / f.denom.leadingCoeff)
have 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⟯)
Tactic: rw [map_div₀, eq_div_iff ((_root_.map_ne_zero C).mpr
    (leadingCoeff_ne_zero.mpr f.denom_ne_zero)), eq_comm]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.IntermediateField (hypothesis)
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⟮X⟯
have this : 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
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.IntermediateField (hypothesis)
Goal:
K : Type u_1
inst : Field K
f : K⟮X⟯
hf : ¬∃ (c : K), f = (C : (a : K) → K⟮X⟯) c
⊢ f.num.natDegree ≤ natDegree (R := ↥K⟮f⟯) (f.minpolyX ↥K⟮f⟯)
have f_ne_zero : f ≠ 0
Tactic: have f_ne_zero : f ≠ 0 := by
    rintro rfl
    exact hf ⟨0, (RingHom.map_zero C).symm⟩
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.IntermediateField (goal)
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
⊢ f.num.natDegree ≤ natDegree (R := ↥K⟮f⟯) (f.minpolyX ↥K⟮f⟯)
have h : Ne (α := ↥K⟮f⟯) (coeff (f.minpolyX ↥K⟮f⟯) f.num.natDegree) 0
Tactic: apply le_natDegree_of_ne_zero
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.IntermediateField (hypothesis)
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
⊢ False
have H₁ : Eq (α := K⟮X⟯) (↑(coeff (f.minpolyX ↥K⟮f⟯) f.num.natDegree) : K⟮X⟯) (↑0 : K⟮X⟯)
Tactic: replace H := congr($(H).val)
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.IntermediateField (hypothesis)
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⟮X⟯) (↑(coeff (f.minpolyX ↥K⟮f⟯) f.num.natDegree) : K⟮X⟯) (↑0 : K⟮X⟯)
⊢ False
have H₁ : HSub.hSub (α := K⟮X⟯) ((C : (a : K) → K⟮X⟯) f.num.leadingCoeff : K⟮X⟯)
    (HMul.hMul (β := K⟮X⟯) f ((C : (a : K) → K⟮X⟯) (f.denom.coeff f.num.natDegree) : K⟮X⟯)) =
  0
Tactic: simp only [coeff_sub, coeff_map, coeff_natDegree, coeff_C_mul, AddSubgroupClass.coe_sub,
    SubalgebraClass.coe_algebraMap, algebraMap_eq_C, MulMemClass.coe_mul, coe_algebraMap,
    ZeroMemClass.coe_zero] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.IntermediateField (hypothesis)
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 :
  HSub.hSub (α := K⟮X⟯) ((C : (a : K) → K⟮X⟯) f.num.leadingCoeff : K⟮X⟯)
      (HMul.hMul (β := K⟮X⟯) f ((C : (a : K) → K⟮X⟯) (f.denom.coeff f.num.natDegree) : K⟮X⟯)) =
    0
⊢ False
have H₁ : f = (C : (a : K) → K⟮X⟯) (f.denom.coeff f.num.natDegree / f.num.leadingCoeff)⁻¹
Tactic: rw [sub_eq_zero, ← mul_right_inj' (inv_ne_zero f_ne_zero), ← mul_assoc, inv_mul_cancel₀ f_ne_zero,
    one_mul, ← eq_div_iff <| (_root_.map_ne_zero C).mpr <| Polynomial.leadingCoeff_ne_zero.mpr
    (num_ne_zero f_ne_zero), ← inv_inj, inv_inv, ← map_div₀, ← map_inv₀] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.IntermediateField (goal)
Goal:
K : Type u_1
inst : Field K
f : K⟮X⟯
⊢ natDegree (R := ↥K⟮f⟯) (f.minpolyX ↥K⟮f⟯) = max f.num.natDegree f.denom.natDegree
have pos : ∀ (hf : ∃ (c : K), f = (C : (a : K) → K⟮X⟯) c),
  natDegree (R := ↥K⟮f⟯) (f.minpolyX ↥K⟮f⟯) = max f.num.natDegree f.denom.natDegree
Tactic: by_cases hf : ∃ c, f = C c