awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Defs (goal)
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
p q : K[X]
hq : q ≠ 0
rw :
  {
      toFractionRing :=
        IsLocalization.mk' (FractionRing K[X]) p
          (Subtype.mk (p := fun (x : K[X]) ↦ Membership.mem (γ := Submonoid K[X]) K[X]⁰ x) q ⋯) } =
    {
      toFractionRing :=
        Localization.mk p (Subtype.mk (p := fun (x : K[X]) ↦ Membership.mem (γ := Submonoid K[X]) K[X]⁰ x) q ⋯) :
      K⟮X⟯ }
⊢ RatFunc.mk p q =
    {
      toFractionRing :=
        Localization.mk p (Subtype.mk (p := fun (x : K[X]) ↦ Membership.mem (γ := Submonoid K[X]) K[X]⁰ x) q ⋯) }
have rw₁ : Eq (α := K⟮X⟯)
  {
    toFractionRing :=
      IsLocalization.mk' (FractionRing K[X]) p
        (Subtype.mk (p := fun (x : K[X]) ↦ Membership.mem (γ := Submonoid K[X]) K[X]⁰ x) q sorry) }
  {
    toFractionRing :=
      IsLocalization.mk' (Localization (M := K[X]) K[X]⁰) p
        (Subtype.mk (p := fun (x : K[X]) ↦ Membership.mem (γ := Submonoid K[X]) K[X]⁰ x) q sorry) }
Tactic: rw [mk_def_of_ne _ hq, Localization.mk_eq_mk']
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Defs (goal)
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
p : K[X]
⊢ RatFunc.mk p 1 = { toFractionRing := (algebraMap K[X] (FractionRing K[X]) : (a : K[X]) → FractionRing K[X]) p }
have rw : RatFunc.mk p 1 = { toFractionRing := IsLocalization.mk' (M := K[X]⁰) (FractionRing K[X]) p 1 }
Tactic: rw [← IsLocalization.mk'_one (M := K[X]⁰) (FractionRing K[X]) p, ← mk_coe_def, Submonoid.coe_one]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Defs (goal)
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
p : K[X]
rw : RatFunc.mk p 1 = { toFractionRing := IsLocalization.mk' (M := K[X]⁰) (FractionRing K[X]) p 1 }
⊢ RatFunc.mk p 1 = { toFractionRing := (algebraMap K[X] (FractionRing K[X]) : (a : K[X]) → FractionRing K[X]) p }
have rw₁ : RatFunc.mk p 1 = RatFunc.mk p (↑1 : K[X])
Tactic: rw [← IsLocalization.mk'_one (M := K[X]⁰) (FractionRing K[X]) p, ← mk_coe_def, Submonoid.coe_one]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Defs (goal)
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
p : K[X]
rw : RatFunc.mk p 1 = { toFractionRing := IsLocalization.mk' (M := K[X]⁰) (FractionRing K[X]) p 1 }
rw₁ : RatFunc.mk p 1 = RatFunc.mk p (↑1 : K[X])
⊢ RatFunc.mk p 1 = { toFractionRing := (algebraMap K[X] (FractionRing K[X]) : (a : K[X]) → FractionRing K[X]) p }
have rw₂ : RatFunc.mk p 1 = RatFunc.mk p 1
Tactic: rw [← IsLocalization.mk'_one (M := K[X]⁰) (FractionRing K[X]) p, ← mk_coe_def, Submonoid.coe_one]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Defs (goal)
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
p q p' q' : K[X]
hq : q ≠ 0
hq' : q' ≠ 0
⊢ RatFunc.mk p q = RatFunc.mk p' q' ↔ p * q' = p' * q
have rw : {
      toFractionRing :=
        IsLocalization.mk' (FractionRing K[X]) p
          (Subtype.mk (p := fun (x : K[X]) ↦ Membership.mem (γ := Submonoid K[X]) K[X]⁰ x) q sorry) } =
    RatFunc.mk p' q' ↔
  p * q' = p' * q
Tactic: rw [mk_def_of_ne _ hq, mk_def_of_ne _ hq', ofFractionRing_injective.eq_iff,
    IsLocalization.mk'_eq_iff_eq',
    (IsFractionRing.injective K[X] (FractionRing K[X])).eq_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Defs (goal)
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
p q p' q' : K[X]
hq : q ≠ 0
hq' : q' ≠ 0
rw :
  {
        toFractionRing :=
          IsLocalization.mk' (FractionRing K[X]) p
            (Subtype.mk (p := fun (x : K[X]) ↦ Membership.mem (γ := Submonoid K[X]) K[X]⁰ x) q ⋯) } =
      RatFunc.mk p' q' ↔
    p * q' = p' * q
⊢ RatFunc.mk p q = RatFunc.mk p' q' ↔ p * q' = p' * q
have rw₁ : Eq (α := K⟮X⟯)
    {
      toFractionRing :=
        IsLocalization.mk' (FractionRing K[X]) p
          (Subtype.mk (p := fun (x : K[X]) ↦ Membership.mem (γ := Submonoid K[X]) K[X]⁰ x) q sorry) }
    {
      toFractionRing :=
        IsLocalization.mk' (FractionRing K[X]) p'
          (Subtype.mk (p := fun (x : K[X]) ↦ Membership.mem (γ := Submonoid K[X]) K[X]⁰ x) q' sorry) } ↔
  p * q' = p' * q
Tactic: rw [mk_def_of_ne _ hq, mk_def_of_ne _ hq', ofFractionRing_injective.eq_iff,
    IsLocalization.mk'_eq_iff_eq',
    (IsFractionRing.injective K[X] (FractionRing K[X])).eq_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Defs (goal)
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
p q p' q' : K[X]
hq : q ≠ 0
hq' : q' ≠ 0
rw :
  {
        toFractionRing :=
          IsLocalization.mk' (FractionRing K[X]) p
            (Subtype.mk (p := fun (x : K[X]) ↦ Membership.mem (γ := Submonoid K[X]) K[X]⁰ x) q ⋯) } =
      RatFunc.mk p' q' ↔
    p * q' = p' * q
rw₁ :
  Eq (α := K⟮X⟯)
      {
        toFractionRing :=
          IsLocalization.mk' (FractionRing K[X]) p
            (Subtype.mk (p := fun (x : K[X]) ↦ Membership.mem (γ := Submonoid K[X]) K[X]⁰ x) q ⋯) }
      {
        toFractionRing :=
          IsLocalization.mk' (FractionRing K[X]) p'
            (Subtype.mk (p := fun (x : K[X]) ↦ Membership.mem (γ := Submonoid K[X]) K[X]⁰ x) q' ⋯) } ↔
    p * q' = p' * q
⊢ RatFunc.mk p q = RatFunc.mk p' q' ↔ p * q' = p' * q
have rw₂ : Eq (α := FractionRing K[X])
    (IsLocalization.mk' (FractionRing K[X]) p
      (Subtype.mk (p := fun (x : K[X]) ↦ Membership.mem (γ := Submonoid K[X]) K[X]⁰ x) q sorry))
    (IsLocalization.mk' (FractionRing K[X]) p'
      (Subtype.mk (p := fun (x : K[X]) ↦ Membership.mem (γ := Submonoid K[X]) K[X]⁰ x) q' sorry)) ↔
  p * q' = p' * q
Tactic: rw [mk_def_of_ne _ hq, mk_def_of_ne _ hq', ofFractionRing_injective.eq_iff,
    IsLocalization.mk'_eq_iff_eq',
    (IsFractionRing.injective K[X] (FractionRing K[X])).eq_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Defs (goal)
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
p q p' q' : K[X]
hq : q ≠ 0
hq' : q' ≠ 0
rw :
  {
        toFractionRing :=
          IsLocalization.mk' (FractionRing K[X]) p
            (Subtype.mk (p := fun (x : K[X]) ↦ Membership.mem (γ := Submonoid K[X]) K[X]⁰ x) q ⋯) } =
      RatFunc.mk p' q' ↔
    p * q' = p' * q
rw₁ :
  Eq (α := K⟮X⟯)
      {
        toFractionRing :=
          IsLocalization.mk' (FractionRing K[X]) p
            (Subtype.mk (p := fun (x : K[X]) ↦ Membership.mem (γ := Submonoid K[X]) K[X]⁰ x) q ⋯) }
      {
        toFractionRing :=
          IsLocalization.mk' (FractionRing K[X]) p'
            (Subtype.mk (p := fun (x : K[X]) ↦ Membership.mem (γ := Submonoid K[X]) K[X]⁰ x) q' ⋯) } ↔
    p * q' = p' * q
rw₂ :
  Eq (α := FractionRing K[X])
      (IsLocalization.mk' (FractionRing K[X]) p
        (Subtype.mk (p := fun (x : K[X]) ↦ Membership.mem (γ := Submonoid K[X]) K[X]⁰ x) q ⋯))
      (IsLocalization.mk' (FractionRing K[X]) p'
        (Subtype.mk (p := fun (x : K[X]) ↦ Membership.mem (γ := Submonoid K[X]) K[X]⁰ x) q' ⋯)) ↔
    p * q' = p' * q
⊢ RatFunc.mk p q = RatFunc.mk p' q' ↔ p * q' = p' * q
have rw₃ : Eq (α := FractionRing K[X])
    ((algebraMap K[X] (FractionRing K[X]) : (a : K[X]) → FractionRing K[X])
        (p * (↑(Subtype.mk (p := fun (x : K[X]) ↦ Membership.mem (γ := Submonoid K[X]) K[X]⁰ x) q' sorry) : K[X])) :
      FractionRing K[X])
    ((algebraMap K[X] (FractionRing K[X]) : (a : K[X]) → FractionRing K[X])
        (p' * (↑(Subtype.mk (p := fun (x : K[X]) ↦ Membership.mem (γ := Submonoid K[X]) K[X]⁰ x) q sorry) : K[X])) :
      FractionRing K[X]) ↔
  p * q' = p' * q
Tactic: rw [mk_def_of_ne _ hq, mk_def_of_ne _ hq', ofFractionRing_injective.eq_iff,
    IsLocalization.mk'_eq_iff_eq',
    (IsFractionRing.injective K[X] (FractionRing K[X])).eq_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Defs (goal)
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
p q p' q' : K[X]
hq : q ≠ 0
hq' : q' ≠ 0
rw :
  {
        toFractionRing :=
          IsLocalization.mk' (FractionRing K[X]) p
            (Subtype.mk (p := fun (x : K[X]) ↦ Membership.mem (γ := Submonoid K[X]) K[X]⁰ x) q ⋯) } =
      RatFunc.mk p' q' ↔
    p * q' = p' * q
rw₁ :
  Eq (α := K⟮X⟯)
      {
        toFractionRing :=
          IsLocalization.mk' (FractionRing K[X]) p
            (Subtype.mk (p := fun (x : K[X]) ↦ Membership.mem (γ := Submonoid K[X]) K[X]⁰ x) q ⋯) }
      {
        toFractionRing :=
          IsLocalization.mk' (FractionRing K[X]) p'
            (Subtype.mk (p := fun (x : K[X]) ↦ Membership.mem (γ := Submonoid K[X]) K[X]⁰ x) q' ⋯) } ↔
    p * q' = p' * q
rw₂ :
  Eq (α := FractionRing K[X])
      (IsLocalization.mk' (FractionRing K[X]) p
        (Subtype.mk (p := fun (x : K[X]) ↦ Membership.mem (γ := Submonoid K[X]) K[X]⁰ x) q ⋯))
      (IsLocalization.mk' (FractionRing K[X]) p'
        (Subtype.mk (p := fun (x : K[X]) ↦ Membership.mem (γ := Submonoid K[X]) K[X]⁰ x) q' ⋯)) ↔
    p * q' = p' * q
rw₃ :
  Eq (α := FractionRing K[X])
      ((algebraMap K[X] (FractionRing K[X]) : (a : K[X]) → FractionRing K[X])
          (p * (↑(Subtype.mk (p := fun (x : K[X]) ↦ Membership.mem (γ := Submonoid K[X]) K[X]⁰ x) q' ⋯) : K[X])) :
        FractionRing K[X])
      ((algebraMap K[X] (FractionRing K[X]) : (a : K[X]) → FractionRing K[X])
          (p' * (↑(Subtype.mk (p := fun (x : K[X]) ↦ Membership.mem (γ := Submonoid K[X]) K[X]⁰ x) q ⋯) : K[X])) :
        FractionRing K[X]) ↔
    p * q' = p' * q
⊢ RatFunc.mk p q = RatFunc.mk p' q' ↔ p * q' = p' * q
have rw₄ : p * (↑(Subtype.mk (p := fun (x : K[X]) ↦ Membership.mem (γ := Submonoid K[X]) K[X]⁰ x) q' sorry) : K[X]) =
    p' * (↑(Subtype.mk (p := fun (x : K[X]) ↦ Membership.mem (γ := Submonoid K[X]) K[X]⁰ x) q sorry) : K[X]) ↔
  p * q' = p' * q
Tactic: rw [mk_def_of_ne _ hq, mk_def_of_ne _ hq', ofFractionRing_injective.eq_iff,
    IsLocalization.mk'_eq_iff_eq',
    (IsFractionRing.injective K[X] (FractionRing K[X])).eq_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Defs (goal)
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
P : Sort v
p q : K[X]
f : K[X] → K[X] → P
f0 : ∀ (p : K[X]), f p 0 = f 0 1
H' : ∀ {p q p' q' : K[X]} (_hq : q ≠ 0) (_hq' : q' ≠ 0), q' * p = q * p' → f p q = f p' q'
H :
  ∀ {p q p' q' : K[X]} (_hq : Membership.mem (γ := Submonoid K[X]) K[X]⁰ q)
    (_hq' : Membership.mem (γ := Submonoid K[X]) K[X]⁰ q'), q' * p = q * p' → f p q = f p' q'
⊢ (RatFunc.mk p q).liftOn f @H = f p q
have pos : ∀ (hq : q = 0), (RatFunc.mk p q).liftOn f @H = f p q
Tactic: by_cases hq : q = 0
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Defs (goal)
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
P : Sort v
p q : K[X]
f : K[X] → K[X] → P
f0 : ∀ (p : K[X]), f p 0 = f 0 1
H' : ∀ {p q p' q' : K[X]} (_hq : q ≠ 0) (_hq' : q' ≠ 0), q' * p = q * p' → f p q = f p' q'
H :
  ∀ {p q p' q' : K[X]} (_hq : Membership.mem (γ := Submonoid K[X]) K[X]⁰ q)
    (_hq' : Membership.mem (γ := Submonoid K[X]) K[X]⁰ q'), q' * p = q * p' → f p q = f p' q'
pos : ∀ (hq : q = 0), (RatFunc.mk p q).liftOn f @H = f p q
⊢ (RatFunc.mk p q).liftOn f @H = f p q
have neg : ∀ (hq : ¬q = 0), (RatFunc.mk p q).liftOn f @H = f p q
Tactic: by_cases hq : q = 0
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Defs (goal)
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
P : Sort v
p q : K[X]
f : K[X] → K[X] → P
f0 : ∀ (p : K[X]), f p 0 = f 0 1
H' : ∀ {p q p' q' : K[X]} (_hq : q ≠ 0) (_hq' : q' ≠ 0), q' * p = q * p' → f p q = f p' q'
H :
  ∀ {p q p' q' : K[X]} (_hq : Membership.mem (γ := Submonoid K[X]) K[X]⁰ q)
    (_hq' : Membership.mem (γ := Submonoid K[X]) K[X]⁰ q'), q' * p = q * p' → f p q = f p' q'
hq : q = 0
⊢ (RatFunc.mk p q).liftOn f @H = f p q
have pos : (RatFunc.mk p 0).liftOn f @H = f p 0
Tactic: subst hq
Cleared hypotheses: q, hq
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Defs (goal)
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
P : Sort v
p q : K[X]
f : K[X] → K[X] → P
f0 : ∀ (p : K[X]), f p 0 = f 0 1
H : ∀ {p q a : K[X]} (_hq : q ≠ 0) (_ha : a ≠ 0), f (a * p) (a * q) = f p q
⊢ (RatFunc.mk p q).liftOn' f @H = f p q
have rw : ∀ {p q p' q' : K[X]} (_hq : q ≠ 0) (_hq' : q' ≠ 0), q' * p = q * p' → f p q = f p' q'
Tactic: rw [RatFunc.liftOn', RatFunc.liftOn_mk _ _ _ f0]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Degree (goal)
Goal:
K : Type u
inst : Field K
⊢ intDegree.{u} (K := K) 0 = 0
have rw : HSub.hSub (α := ℤ) (↑(natDegree.{u} (R := K) (num 0)) : ℤ) (↑(natDegree.{u} (R := K) (denom 0)) : ℤ) = 0
Tactic: rw [intDegree, num_zero, natDegree_zero, denom_zero, natDegree_one, sub_self]
-- 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 0)) : ℤ) (↑(natDegree.{u} (R := K) (denom 0)) : ℤ) = 0
⊢ intDegree.{u} (K := K) 0 = 0
have rw₁ : HSub.hSub (α := ℤ) (↑(natDegree.{u} (R := K) 0) : ℤ) (↑(natDegree.{u} (R := K) (denom 0)) : ℤ) = 0
Tactic: rw [intDegree, num_zero, natDegree_zero, denom_zero, natDegree_one, sub_self]
-- 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 0)) : ℤ) (↑(natDegree.{u} (R := K) (denom 0)) : ℤ) = 0
rw₁ : HSub.hSub (α := ℤ) (↑(natDegree.{u} (R := K) 0) : ℤ) (↑(natDegree.{u} (R := K) (denom 0)) : ℤ) = 0
⊢ intDegree.{u} (K := K) 0 = 0
have rw₂ : HSub.hSub (α := ℤ) (↑0 : ℤ) (↑(natDegree.{u} (R := K) (denom 0)) : ℤ) = 0
Tactic: rw [intDegree, num_zero, natDegree_zero, denom_zero, natDegree_one, sub_self]
-- 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 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
⊢ intDegree.{u} (K := K) 0 = 0
have rw₃ : HSub.hSub (α := ℤ) (↑0 : ℤ) (↑(natDegree.{u} (R := K) 1) : ℤ) = 0
Tactic: rw [intDegree, num_zero, natDegree_zero, denom_zero, natDegree_one, sub_self]
-- 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 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
⊢ intDegree.{u} (K := K) 0 = 0
have rw₄ : HSub.hSub (α := ℤ) (↑0 : ℤ) (↑0 : ℤ) = 0
Tactic: rw [intDegree, num_zero, natDegree_zero, denom_zero, natDegree_one, sub_self]
-- 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 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
⊢ intDegree.{u} (K := K) 0 = 0
have rw₅ : Eq (α := ℤ) 0 0
Tactic: rw [intDegree, num_zero, natDegree_zero, denom_zero, natDegree_one, sub_self]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Degree (goal)
Goal:
K : Type u
inst : Field K
⊢ intDegree.{u} (K := K) 1 = 0
have rw : HSub.hSub (α := ℤ) (↑(natDegree.{u} (R := K) (num 1)) : ℤ) (↑(natDegree.{u} (R := K) (denom 1)) : ℤ) = 0
Tactic: rw [intDegree, num_one, denom_one, sub_self]
-- 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 1)) : ℤ) (↑(natDegree.{u} (R := K) (denom 1)) : ℤ) = 0
⊢ intDegree.{u} (K := K) 1 = 0
have rw₁ : HSub.hSub (α := ℤ) (↑(natDegree.{u} (R := K) 1) : ℤ) (↑(natDegree.{u} (R := K) (denom 1)) : ℤ) = 0
Tactic: rw [intDegree, num_one, denom_one, sub_self]
-- 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 1)) : ℤ) (↑(natDegree.{u} (R := K) (denom 1)) : ℤ) = 0
rw₁ : HSub.hSub (α := ℤ) (↑(natDegree.{u} (R := K) 1) : ℤ) (↑(natDegree.{u} (R := K) (denom 1)) : ℤ) = 0
⊢ intDegree.{u} (K := K) 1 = 0
have rw₂ : HSub.hSub (α := ℤ) (↑(natDegree.{u} (R := K) 1) : ℤ) (↑(natDegree.{u} (R := K) 1) : ℤ) = 0
Tactic: rw [intDegree, num_one, denom_one, sub_self]
-- 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 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
⊢ intDegree.{u} (K := K) 1 = 0
have rw₃ : Eq (α := ℤ) 0 0
Tactic: rw [intDegree, num_one, denom_one, sub_self]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Degree (goal)
Goal:
K : Type u
inst : Field K
k : K
⊢ intDegree.{u} (K := K) ((C : (a : K) → K⟮X⟯) k) = 0
have 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
Tactic: rw [intDegree, num_C, natDegree_C, denom_C, natDegree_one, sub_self]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Degree (goal)
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
⊢ intDegree.{u} (K := K) ((C : (a : K) → K⟮X⟯) k) = 0
have 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
Tactic: rw [intDegree, num_C, natDegree_C, denom_C, natDegree_one, sub_self]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Degree (goal)
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
⊢ intDegree.{u} (K := K) ((C : (a : K) → K⟮X⟯) k) = 0
have rw₂ : HSub.hSub (α := ℤ) (↑0 : ℤ) (↑(natDegree.{u} (R := K) (denom ((C : (a : K) → K⟮X⟯) k))) : ℤ) = 0
Tactic: rw [intDegree, num_C, natDegree_C, denom_C, natDegree_one, sub_self]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Degree (goal)
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
⊢ intDegree.{u} (K := K) ((C : (a : K) → K⟮X⟯) k) = 0
have rw₃ : HSub.hSub (α := ℤ) (↑0 : ℤ) (↑(natDegree.{u} (R := K) 1) : ℤ) = 0
Tactic: rw [intDegree, num_C, natDegree_C, denom_C, natDegree_one, sub_self]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Degree (goal)
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
⊢ intDegree.{u} (K := K) ((C : (a : K) → K⟮X⟯) k) = 0
have rw₄ : HSub.hSub (α := ℤ) (↑0 : ℤ) (↑0 : ℤ) = 0
Tactic: rw [intDegree, num_C, natDegree_C, denom_C, natDegree_one, sub_self]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Degree (goal)
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
⊢ intDegree.{u} (K := K) ((C : (a : K) → K⟮X⟯) k) = 0
have rw₅ : Eq (α := ℤ) 0 0
Tactic: rw [intDegree, num_C, natDegree_C, denom_C, natDegree_one, sub_self]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Degree (goal)
Goal:
K : Type u
inst : Field K
⊢ intDegree.{u} (K := K) X = 1
have rw : HSub.hSub (α := ℤ) (↑(natDegree.{u} (R := K) (num X)) : ℤ) (↑(natDegree.{u} (R := K) (denom X)) : ℤ) = 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
⊢ intDegree.{u} (K := K) X = 1
have rw₁ : HSub.hSub (α := ℤ) (↑(natDegree.{u} (R := K) Polynomial.X) : ℤ) (↑(natDegree.{u} (R := K) (denom X)) : ℤ) = 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
⊢ intDegree.{u} (K := K) X = 1
have rw₂ : HSub.hSub (α := ℤ) (↑1 : ℤ) (↑(natDegree.{u} (R := K) (denom X)) : ℤ) = 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
⊢ intDegree.{u} (K := K) X = 1
have rw₃ : HSub.hSub (α := ℤ) (↑1 : ℤ) (↑(natDegree.{u} (R := K) 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
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
⊢ 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]