awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
R : Type u_1
inst_1 : IsDomain K
inst_2 : Monoid R
inst_3 : DistribMulAction.{u_1, u} R K[X]
inst_4 : IsScalarTower.{u_1, u, u} R K[X] K[X]
c : R
p q : K[X]
this : SMulZeroClass.{u_1, u} R (FractionRing K[X]) := inferInstance
hq : q = 0
pos : RatFunc.mk (c • p) 0 = c • RatFunc.mk p 0
pos₁ : { toFractionRing := 0 } = c • RatFunc.mk p 0
pos₂ : { toFractionRing := 0 } = HSMul.hSMul (β := K⟮X⟯) c { toFractionRing := 0 : K⟮X⟯ }
pos₃ : { toFractionRing := 0 } = { toFractionRing := HSMul.hSMul (β := FractionRing K[X]) c 0 : K⟮X⟯ }
⊢ RatFunc.mk (c • p) q = c • RatFunc.mk p q
have pos₄ : Eq.{u + 1} (α := K⟮X⟯) { toFractionRing := 0 } { toFractionRing := 0 }
Tactic: rw [hq, mk_zero, mk_zero, ← ofFractionRing_smul, smul_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
R : Type u_1
inst_1 : IsDomain K
inst_2 : Monoid R
inst_3 : DistribMulAction.{u_1, u} R K[X]
inst_4 : IsScalarTower.{u_1, u, u} R K[X] K[X]
c : R
p q : K[X]
this : SMulZeroClass.{u_1, u} R (FractionRing K[X]) := inferInstance
hq : ¬q = 0
⊢ RatFunc.mk (c • p) q = c • RatFunc.mk p q
have neg : {
    toFractionRing :=
      Localization.mk (c • p) (Subtype.mk (p := fun (x : K[X]) ↦ Membership.mem (γ := Submonoid K[X]) K[X]⁰ x) q sorry) :
    K⟮X⟯ } =
  c • RatFunc.mk p q
Tactic: rw [mk_eq_localization_mk _ hq, mk_eq_localization_mk _ hq, ← Localization.smul_mk, ←
      ofFractionRing_smul]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
R : Type u_1
inst_1 : IsDomain K
inst_2 : Monoid R
inst_3 : DistribMulAction.{u_1, u} R K[X]
inst_4 : IsScalarTower.{u_1, u, u} R K[X] K[X]
c : R
p q : K[X]
this : SMulZeroClass.{u_1, u} R (FractionRing K[X]) := inferInstance
hq : ¬q = 0
neg :
  {
      toFractionRing :=
        Localization.mk (c • p) (Subtype.mk (p := fun (x : K[X]) ↦ Membership.mem (γ := Submonoid K[X]) K[X]⁰ x) q ⋯) :
      K⟮X⟯ } =
    c • RatFunc.mk p q
⊢ RatFunc.mk (c • p) q = c • RatFunc.mk p q
have neg₁ : {
    toFractionRing :=
      Localization.mk (c • p) (Subtype.mk (p := fun (x : K[X]) ↦ Membership.mem (γ := Submonoid K[X]) K[X]⁰ x) q sorry) :
    K⟮X⟯ } =
  c •
    {
      toFractionRing :=
        Localization.mk p (Subtype.mk (p := fun (x : K[X]) ↦ Membership.mem (γ := Submonoid K[X]) K[X]⁰ x) q sorry) :
      K⟮X⟯ }
Tactic: rw [mk_eq_localization_mk _ hq, mk_eq_localization_mk _ hq, ← Localization.smul_mk, ←
      ofFractionRing_smul]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
R : Type u_1
inst_1 : IsDomain K
inst_2 : Monoid R
inst_3 : DistribMulAction.{u_1, u} R K[X]
inst_4 : IsScalarTower.{u_1, u, u} R K[X] K[X]
c : R
p q : K[X]
this : SMulZeroClass.{u_1, u} R (FractionRing K[X]) := inferInstance
hq : ¬q = 0
neg :
  {
      toFractionRing :=
        Localization.mk (c • p) (Subtype.mk (p := fun (x : K[X]) ↦ Membership.mem (γ := Submonoid K[X]) K[X]⁰ x) q ⋯) :
      K⟮X⟯ } =
    c • RatFunc.mk p q
neg₁ :
  {
      toFractionRing :=
        Localization.mk (c • p) (Subtype.mk (p := fun (x : K[X]) ↦ Membership.mem (γ := Submonoid K[X]) K[X]⁰ x) q ⋯) :
      K⟮X⟯ } =
    c •
      {
        toFractionRing :=
          Localization.mk p (Subtype.mk (p := fun (x : K[X]) ↦ Membership.mem (γ := Submonoid K[X]) K[X]⁰ x) q ⋯) :
        K⟮X⟯ }
⊢ RatFunc.mk (c • p) q = c • RatFunc.mk p q
have neg₂ : {
    toFractionRing :=
      c • Localization.mk p (Subtype.mk (p := fun (x : K[X]) ↦ Membership.mem (γ := Submonoid K[X]) K[X]⁰ x) q sorry) :
    K⟮X⟯ } =
  c •
    {
      toFractionRing :=
        Localization.mk p (Subtype.mk (p := fun (x : K[X]) ↦ Membership.mem (γ := Submonoid K[X]) K[X]⁰ x) q sorry) :
      K⟮X⟯ }
Tactic: rw [mk_eq_localization_mk _ hq, mk_eq_localization_mk _ hq, ← Localization.smul_mk, ←
      ofFractionRing_smul]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
R : Type u_1
inst_1 : IsDomain K
inst_2 : Monoid R
inst_3 : DistribMulAction.{u_1, u} R K[X]
inst_4 : IsScalarTower.{u_1, u, u} R K[X] K[X]
c : R
p q : K[X]
this : SMulZeroClass.{u_1, u} R (FractionRing K[X]) := inferInstance
hq : ¬q = 0
neg :
  {
      toFractionRing :=
        Localization.mk (c • p) (Subtype.mk (p := fun (x : K[X]) ↦ Membership.mem (γ := Submonoid K[X]) K[X]⁰ x) q ⋯) :
      K⟮X⟯ } =
    c • RatFunc.mk p q
neg₁ :
  {
      toFractionRing :=
        Localization.mk (c • p) (Subtype.mk (p := fun (x : K[X]) ↦ Membership.mem (γ := Submonoid K[X]) K[X]⁰ x) q ⋯) :
      K⟮X⟯ } =
    c •
      {
        toFractionRing :=
          Localization.mk p (Subtype.mk (p := fun (x : K[X]) ↦ Membership.mem (γ := Submonoid K[X]) K[X]⁰ x) q ⋯) :
        K⟮X⟯ }
neg₂ :
  {
      toFractionRing :=
        c • Localization.mk p (Subtype.mk (p := fun (x : K[X]) ↦ Membership.mem (γ := Submonoid K[X]) K[X]⁰ x) q ⋯) :
      K⟮X⟯ } =
    c •
      {
        toFractionRing :=
          Localization.mk p (Subtype.mk (p := fun (x : K[X]) ↦ Membership.mem (γ := Submonoid K[X]) K[X]⁰ x) q ⋯) :
        K⟮X⟯ }
⊢ RatFunc.mk (c • p) q = c • RatFunc.mk p q
have neg₃ : {
    toFractionRing :=
      c • Localization.mk p (Subtype.mk (p := fun (x : K[X]) ↦ Membership.mem (γ := Submonoid K[X]) K[X]⁰ x) q sorry) :
    K⟮X⟯ } =
  {
    toFractionRing :=
      c • Localization.mk p (Subtype.mk (p := fun (x : K[X]) ↦ Membership.mem (γ := Submonoid K[X]) K[X]⁰ x) q sorry) }
Tactic: rw [mk_eq_localization_mk _ hq, mk_eq_localization_mk _ hq, ← Localization.smul_mk, ←
      ofFractionRing_smul]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
R : Type u_1
inst_1 : IsDomain K
inst_2 : Monoid R
inst_3 : DistribMulAction.{u_1, u} R K[X]
inst_4 : IsScalarTower.{u_1, u, u} R K[X] K[X]
c : R
p : K[X]
q_1 : K⟮X⟯
q r : K[X]
h : r ≠ 0
⊢ (c • p) • RatFunc.mk q r = c • p • RatFunc.mk q r
have rw : RatFunc.mk ((c • p) • q) r = c • p • RatFunc.mk q r
Tactic: rw [← mk_smul, smul_assoc, mk_smul, mk_smul]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
R : Type u_1
inst_1 : IsDomain K
inst_2 : Monoid R
inst_3 : DistribMulAction.{u_1, u} R K[X]
inst_4 : IsScalarTower.{u_1, u, u} R K[X] K[X]
c : R
p : K[X]
q_1 : K⟮X⟯
q r : K[X]
h : r ≠ 0
rw : RatFunc.mk ((c • p) • q) r = c • p • RatFunc.mk q r
⊢ (c • p) • RatFunc.mk q r = c • p • RatFunc.mk q r
have rw₁ : RatFunc.mk (c • p • q) r = c • p • RatFunc.mk q r
Tactic: rw [← mk_smul, smul_assoc, mk_smul, mk_smul]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
R : Type u_1
inst_1 : IsDomain K
inst_2 : Monoid R
inst_3 : DistribMulAction.{u_1, u} R K[X]
inst_4 : IsScalarTower.{u_1, u, u} R K[X] K[X]
c : R
p : K[X]
q_1 : K⟮X⟯
q r : K[X]
h : r ≠ 0
rw : RatFunc.mk ((c • p) • q) r = c • p • RatFunc.mk q r
rw₁ : RatFunc.mk (c • p • q) r = c • p • RatFunc.mk q r
⊢ (c • p) • RatFunc.mk q r = c • p • RatFunc.mk q r
have rw₂ : c • RatFunc.mk (p • q) r = c • p • RatFunc.mk q r
Tactic: rw [← mk_smul, smul_assoc, mk_smul, mk_smul]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
R : Type u_1
inst_1 : IsDomain K
inst_2 : Monoid R
inst_3 : DistribMulAction.{u_1, u} R K[X]
inst_4 : IsScalarTower.{u_1, u, u} R K[X] K[X]
c : R
p : K[X]
q_1 : K⟮X⟯
q r : K[X]
h : r ≠ 0
rw : RatFunc.mk ((c • p) • q) r = c • p • RatFunc.mk q r
rw₁ : RatFunc.mk (c • p • q) r = c • p • RatFunc.mk q r
rw₂ : c • RatFunc.mk (p • q) r = c • p • RatFunc.mk q r
⊢ (c • p) • RatFunc.mk q r = c • p • RatFunc.mk q r
have rw₃ : c • p • RatFunc.mk q r = c • p • RatFunc.mk q r
Tactic: rw [← mk_smul, smul_assoc, mk_smul, mk_smul]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
⊢ ∀ (a b c : K⟮X⟯), a * b * c = a * (b * c)
have frac_tac : ∀ (toFractionRing : FractionRing K[X]) (b c : K⟮X⟯),
  { toFractionRing := toFractionRing : K⟮X⟯ } * b * c = { toFractionRing := toFractionRing : K⟮X⟯ } * (b * c)
Tactic: frac_tac
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
frac_tac :
  ∀ (toFractionRing : FractionRing K[X]) (b c : K⟮X⟯),
    { toFractionRing := toFractionRing : K⟮X⟯ } * b * c = { toFractionRing := toFractionRing : K⟮X⟯ } * (b * c)
⊢ ∀ (a b c : K⟮X⟯), a * b * c = a * (b * c)
have frac_tac₁ : ∀ (toFractionRing toFractionRing_1 : FractionRing K[X]) (c : K⟮X⟯),
  { toFractionRing := toFractionRing : K⟮X⟯ } * { toFractionRing := toFractionRing_1 : K⟮X⟯ } * c =
    { toFractionRing := toFractionRing : K⟮X⟯ } * ({ toFractionRing := toFractionRing_1 : K⟮X⟯ } * c)
Tactic: frac_tac
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
frac_tac :
  ∀ (toFractionRing : FractionRing K[X]) (b c : K⟮X⟯),
    { toFractionRing := toFractionRing : K⟮X⟯ } * b * c = { toFractionRing := toFractionRing : K⟮X⟯ } * (b * c)
frac_tac₁ :
  ∀ (toFractionRing toFractionRing_1 : FractionRing K[X]) (c : K⟮X⟯),
    { toFractionRing := toFractionRing : K⟮X⟯ } * { toFractionRing := toFractionRing_1 : K⟮X⟯ } * c =
      { toFractionRing := toFractionRing : K⟮X⟯ } * ({ toFractionRing := toFractionRing_1 : K⟮X⟯ } * c)
⊢ ∀ (a b c : K⟮X⟯), a * b * c = a * (b * c)
have frac_tac₂ : ∀ (toFractionRing toFractionRing_1 toFractionRing_2 : FractionRing K[X]),
  { toFractionRing := toFractionRing : K⟮X⟯ } * { toFractionRing := toFractionRing_1 : K⟮X⟯ } *
      { toFractionRing := toFractionRing_2 : K⟮X⟯ } =
    { toFractionRing := toFractionRing : K⟮X⟯ } *
      ({ toFractionRing := toFractionRing_1 : K⟮X⟯ } * { toFractionRing := toFractionRing_2 : K⟮X⟯ })
Tactic: frac_tac
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
⊢ ∀ (a : K⟮X⟯), 1 * a = a
have frac_tac : ∀ (toFractionRing : FractionRing K[X]),
  1 * { toFractionRing := toFractionRing : K⟮X⟯ } = { toFractionRing := toFractionRing }
Tactic: frac_tac
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
⊢ ∀ (a : K⟮X⟯), a * 1 = a
have frac_tac : ∀ (toFractionRing : FractionRing K[X]),
  { toFractionRing := toFractionRing : K⟮X⟯ } * 1 = { toFractionRing := toFractionRing }
Tactic: frac_tac
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
⊢ ∀ (a b : K⟮X⟯), a * b = b * a
have frac_tac : ∀ (toFractionRing : FractionRing K[X]) (b : K⟮X⟯),
  { toFractionRing := toFractionRing : K⟮X⟯ } * b = b * { toFractionRing := toFractionRing : K⟮X⟯ }
Tactic: frac_tac
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
frac_tac :
  ∀ (toFractionRing : FractionRing K[X]) (b : K⟮X⟯),
    { toFractionRing := toFractionRing : K⟮X⟯ } * b = b * { toFractionRing := toFractionRing : K⟮X⟯ }
⊢ ∀ (a b : K⟮X⟯), a * b = b * a
have frac_tac₁ : ∀ (toFractionRing toFractionRing_1 : FractionRing K[X]),
  { toFractionRing := toFractionRing : K⟮X⟯ } * { toFractionRing := toFractionRing_1 : K⟮X⟯ } =
    { toFractionRing := toFractionRing_1 : K⟮X⟯ } * { toFractionRing := toFractionRing : K⟮X⟯ }
Tactic: frac_tac
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
⊢ ∀ (a b c : K⟮X⟯), a + b + c = a + (b + c)
have frac_tac : ∀ (toFractionRing : FractionRing K[X]) (b c : K⟮X⟯),
  { toFractionRing := toFractionRing : K⟮X⟯ } + b + c = { toFractionRing := toFractionRing : K⟮X⟯ } + (b + c)
Tactic: frac_tac
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
frac_tac :
  ∀ (toFractionRing : FractionRing K[X]) (b c : K⟮X⟯),
    { toFractionRing := toFractionRing : K⟮X⟯ } + b + c = { toFractionRing := toFractionRing : K⟮X⟯ } + (b + c)
⊢ ∀ (a b c : K⟮X⟯), a + b + c = a + (b + c)
have frac_tac₁ : ∀ (toFractionRing toFractionRing_1 : FractionRing K[X]) (c : K⟮X⟯),
  { toFractionRing := toFractionRing : K⟮X⟯ } + { toFractionRing := toFractionRing_1 : K⟮X⟯ } + c =
    { toFractionRing := toFractionRing : K⟮X⟯ } + ({ toFractionRing := toFractionRing_1 : K⟮X⟯ } + c)
Tactic: frac_tac
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
frac_tac :
  ∀ (toFractionRing : FractionRing K[X]) (b c : K⟮X⟯),
    { toFractionRing := toFractionRing : K⟮X⟯ } + b + c = { toFractionRing := toFractionRing : K⟮X⟯ } + (b + c)
frac_tac₁ :
  ∀ (toFractionRing toFractionRing_1 : FractionRing K[X]) (c : K⟮X⟯),
    { toFractionRing := toFractionRing : K⟮X⟯ } + { toFractionRing := toFractionRing_1 : K⟮X⟯ } + c =
      { toFractionRing := toFractionRing : K⟮X⟯ } + ({ toFractionRing := toFractionRing_1 : K⟮X⟯ } + c)
⊢ ∀ (a b c : K⟮X⟯), a + b + c = a + (b + c)
have frac_tac₂ : ∀ (toFractionRing toFractionRing_1 toFractionRing_2 : FractionRing K[X]),
  { toFractionRing := toFractionRing : K⟮X⟯ } + { toFractionRing := toFractionRing_1 : K⟮X⟯ } +
      { toFractionRing := toFractionRing_2 : K⟮X⟯ } =
    { toFractionRing := toFractionRing : K⟮X⟯ } +
      ({ toFractionRing := toFractionRing_1 : K⟮X⟯ } + { toFractionRing := toFractionRing_2 : K⟮X⟯ })
Tactic: frac_tac
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
⊢ ∀ (a : K⟮X⟯), 0 + a = a
have frac_tac : ∀ (toFractionRing : FractionRing K[X]),
  0 + { toFractionRing := toFractionRing : K⟮X⟯ } = { toFractionRing := toFractionRing }
Tactic: frac_tac
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
⊢ ∀ (a : K⟮X⟯), a + 0 = a
have frac_tac : ∀ (toFractionRing : FractionRing K[X]),
  { toFractionRing := toFractionRing : K⟮X⟯ } + 0 = { toFractionRing := toFractionRing }
Tactic: frac_tac
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
⊢ ∀ (x : K⟮X⟯), HSMul.hSMul (α := ℕ) 0 x = 0
have smul_tac : ∀ (toFractionRing : FractionRing K[X]), HSMul.hSMul (α := ℕ) 0 { toFractionRing := toFractionRing : K⟮X⟯ } = 0
Tactic: smul_tac
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
smul_tac smul_tac₁ smul_tac₂ smul_tac₃ :
  ∀ (toFractionRing : FractionRing K[X]), HSMul.hSMul (α := ℕ) 0 { toFractionRing := toFractionRing : K⟮X⟯ } = 0
⊢ ∀ (x : K⟮X⟯), HSMul.hSMul (α := ℕ) 0 x = 0
have smul_tac₄ : ∀ (toFractionRing : FractionRing K[X]), { toFractionRing := HSMul.hSMul (α := ℕ) 0 toFractionRing : K⟮X⟯ } = 0
Tactic: smul_tac
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
x : ℕ
⊢ ∀ (x_1 : K⟮X⟯), (x + 1) • x_1 = x • x_1 + x_1
have smul_tac : ∀ (toFractionRing : FractionRing K[X]),
  (x + 1) • { toFractionRing := toFractionRing : K⟮X⟯ } =
    x • { toFractionRing := toFractionRing : K⟮X⟯ } + { toFractionRing := toFractionRing : K⟮X⟯ }
Tactic: smul_tac
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
x : ℕ
smul_tac smul_tac₁ smul_tac₂ smul_tac₃ :
  ∀ (toFractionRing : FractionRing K[X]),
    (x + 1) • { toFractionRing := toFractionRing : K⟮X⟯ } =
      x • { toFractionRing := toFractionRing : K⟮X⟯ } + { toFractionRing := toFractionRing : K⟮X⟯ }
⊢ ∀ (x_1 : K⟮X⟯), (x + 1) • x_1 = x • x_1 + x_1
have smul_tac₄ : ∀ (toFractionRing : FractionRing K[X]),
  { toFractionRing := (x + 1) • toFractionRing : K⟮X⟯ } =
    { toFractionRing := x • toFractionRing : K⟮X⟯ } + { toFractionRing := toFractionRing : K⟮X⟯ }
Tactic: smul_tac
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
⊢ ∀ (a b : K⟮X⟯), a - b = a + -b
have frac_tac : ∀ (toFractionRing : FractionRing K[X]) (b : K⟮X⟯),
  { toFractionRing := toFractionRing : K⟮X⟯ } - b = { toFractionRing := toFractionRing : K⟮X⟯ } + -b
Tactic: frac_tac
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
frac_tac :
  ∀ (toFractionRing : FractionRing K[X]) (b : K⟮X⟯),
    { toFractionRing := toFractionRing : K⟮X⟯ } - b = { toFractionRing := toFractionRing : K⟮X⟯ } + -b
⊢ ∀ (a b : K⟮X⟯), a - b = a + -b
have frac_tac₁ : ∀ (toFractionRing toFractionRing_1 : FractionRing K[X]),
  { toFractionRing := toFractionRing : K⟮X⟯ } - { toFractionRing := toFractionRing_1 : K⟮X⟯ } =
    { toFractionRing := toFractionRing : K⟮X⟯ } + -{ toFractionRing := toFractionRing_1 : K⟮X⟯ }
Tactic: frac_tac
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
⊢ ∀ (a : K⟮X⟯), HSMul.hSMul (α := ℤ) 0 a = 0
have smul_tac : ∀ (toFractionRing : FractionRing K[X]), HSMul.hSMul (α := ℤ) 0 { toFractionRing := toFractionRing : K⟮X⟯ } = 0
Tactic: smul_tac
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
smul_tac smul_tac₁ smul_tac₂ smul_tac₃ :
  ∀ (toFractionRing : FractionRing K[X]), HSMul.hSMul (α := ℤ) 0 { toFractionRing := toFractionRing : K⟮X⟯ } = 0
⊢ ∀ (a : K⟮X⟯), HSMul.hSMul (α := ℤ) 0 a = 0
have smul_tac₄ : ∀ (toFractionRing : FractionRing K[X]), { toFractionRing := HSMul.hSMul (α := ℤ) 0 toFractionRing : K⟮X⟯ } = 0
Tactic: smul_tac
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
x : ℕ
⊢ ∀ (a : K⟮X⟯), HSMul.hSMul (α := ℤ) (↑x.succ : ℤ) a = HSMul.hSMul (α := ℤ) (↑x : ℤ) a + a
have smul_tac : ∀ (toFractionRing : FractionRing K[X]),
  HSMul.hSMul (α := ℤ) (↑x.succ : ℤ) { toFractionRing := toFractionRing : K⟮X⟯ } =
    HSMul.hSMul (α := ℤ) (↑x : ℤ) { toFractionRing := toFractionRing : K⟮X⟯ } +
      { toFractionRing := toFractionRing : K⟮X⟯ }
Tactic: smul_tac
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
x : ℕ
smul_tac smul_tac₁ smul_tac₂ smul_tac₃ :
  ∀ (toFractionRing : FractionRing K[X]),
    HSMul.hSMul (α := ℤ) (↑x.succ : ℤ) { toFractionRing := toFractionRing : K⟮X⟯ } =
      HSMul.hSMul (α := ℤ) (↑x : ℤ) { toFractionRing := toFractionRing : K⟮X⟯ } +
        { toFractionRing := toFractionRing : K⟮X⟯ }
⊢ ∀ (a : K⟮X⟯), HSMul.hSMul (α := ℤ) (↑x.succ : ℤ) a = HSMul.hSMul (α := ℤ) (↑x : ℤ) a + a
have smul_tac₄ : ∀ (toFractionRing : FractionRing K[X]),
  { toFractionRing := HSMul.hSMul (α := ℤ) (↑x.succ : ℤ) toFractionRing : K⟮X⟯ } =
    { toFractionRing := HSMul.hSMul (α := ℤ) (↑x : ℤ) toFractionRing : K⟮X⟯ } +
      { toFractionRing := toFractionRing : K⟮X⟯ }
Tactic: smul_tac
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
x : ℕ
⊢ ∀ (a : K⟮X⟯), Int.negSucc x • a = -HSMul.hSMul (α := ℤ) (↑x.succ : ℤ) a
have smul_tac : ∀ (toFractionRing : FractionRing K[X]),
  Int.negSucc x • { toFractionRing := toFractionRing : K⟮X⟯ } =
    -HSMul.hSMul (α := ℤ) (↑x.succ : ℤ) { toFractionRing := toFractionRing : K⟮X⟯ }
Tactic: smul_tac
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
x : ℕ
smul_tac smul_tac₁ smul_tac₂ smul_tac₃ :
  ∀ (toFractionRing : FractionRing K[X]),
    Int.negSucc x • { toFractionRing := toFractionRing : K⟮X⟯ } =
      -HSMul.hSMul (α := ℤ) (↑x.succ : ℤ) { toFractionRing := toFractionRing : K⟮X⟯ }
⊢ ∀ (a : K⟮X⟯), Int.negSucc x • a = -HSMul.hSMul (α := ℤ) (↑x.succ : ℤ) a
have smul_tac₄ : ∀ (toFractionRing : FractionRing K[X]),
  { toFractionRing := Int.negSucc x • toFractionRing : K⟮X⟯ } =
    -{ toFractionRing := HSMul.hSMul (α := ℤ) (↑x.succ : ℤ) toFractionRing }
Tactic: smul_tac
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
⊢ ∀ (a : K⟮X⟯), -a + a = 0
have frac_tac : ∀ (toFractionRing : FractionRing K[X]),
  -{ toFractionRing := toFractionRing : K⟮X⟯ } + { toFractionRing := toFractionRing : K⟮X⟯ } = 0
Tactic: frac_tac
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
⊢ ∀ (a b : K⟮X⟯), a + b = b + a
have frac_tac : ∀ (toFractionRing : FractionRing K[X]) (b : K⟮X⟯),
  { toFractionRing := toFractionRing : K⟮X⟯ } + b = b + { toFractionRing := toFractionRing : K⟮X⟯ }
Tactic: frac_tac
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
frac_tac :
  ∀ (toFractionRing : FractionRing K[X]) (b : K⟮X⟯),
    { toFractionRing := toFractionRing : K⟮X⟯ } + b = b + { toFractionRing := toFractionRing : K⟮X⟯ }
⊢ ∀ (a b : K⟮X⟯), a + b = b + a
have frac_tac₁ : ∀ (toFractionRing toFractionRing_1 : FractionRing K[X]),
  { toFractionRing := toFractionRing : K⟮X⟯ } + { toFractionRing := toFractionRing_1 : K⟮X⟯ } =
    { toFractionRing := toFractionRing_1 : K⟮X⟯ } + { toFractionRing := toFractionRing : K⟮X⟯ }
Tactic: frac_tac
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
⊢ ∀ (a : K⟮X⟯), 0 * a = 0
have frac_tac : ∀ (toFractionRing : FractionRing K[X]), 0 * { toFractionRing := toFractionRing : K⟮X⟯ } = 0
Tactic: frac_tac
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
⊢ ∀ (a : K⟮X⟯), a * 0 = 0
have frac_tac : ∀ (toFractionRing : FractionRing K[X]), { toFractionRing := toFractionRing : K⟮X⟯ } * 0 = 0
Tactic: frac_tac
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
⊢ ∀ (a b c : K⟮X⟯), a * (b + c) = a * b + a * c
have frac_tac : ∀ (toFractionRing : FractionRing K[X]) (b c : K⟮X⟯),
  { toFractionRing := toFractionRing : K⟮X⟯ } * (b + c) =
    { toFractionRing := toFractionRing : K⟮X⟯ } * b + { toFractionRing := toFractionRing : K⟮X⟯ } * c
Tactic: frac_tac
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
frac_tac :
  ∀ (toFractionRing : FractionRing K[X]) (b c : K⟮X⟯),
    { toFractionRing := toFractionRing : K⟮X⟯ } * (b + c) =
      { toFractionRing := toFractionRing : K⟮X⟯ } * b + { toFractionRing := toFractionRing : K⟮X⟯ } * c
⊢ ∀ (a b c : K⟮X⟯), a * (b + c) = a * b + a * c
have frac_tac₁ : ∀ (toFractionRing toFractionRing_1 : FractionRing K[X]) (c : K⟮X⟯),
  { toFractionRing := toFractionRing : K⟮X⟯ } * ({ toFractionRing := toFractionRing_1 : K⟮X⟯ } + c) =
    { toFractionRing := toFractionRing : K⟮X⟯ } * { toFractionRing := toFractionRing_1 : K⟮X⟯ } +
      { toFractionRing := toFractionRing : K⟮X⟯ } * c
Tactic: frac_tac
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
frac_tac :
  ∀ (toFractionRing : FractionRing K[X]) (b c : K⟮X⟯),
    { toFractionRing := toFractionRing : K⟮X⟯ } * (b + c) =
      { toFractionRing := toFractionRing : K⟮X⟯ } * b + { toFractionRing := toFractionRing : K⟮X⟯ } * c
frac_tac₁ :
  ∀ (toFractionRing toFractionRing_1 : FractionRing K[X]) (c : K⟮X⟯),
    { toFractionRing := toFractionRing : K⟮X⟯ } * ({ toFractionRing := toFractionRing_1 : K⟮X⟯ } + c) =
      { toFractionRing := toFractionRing : K⟮X⟯ } * { toFractionRing := toFractionRing_1 : K⟮X⟯ } +
        { toFractionRing := toFractionRing : K⟮X⟯ } * c
⊢ ∀ (a b c : K⟮X⟯), a * (b + c) = a * b + a * c
have frac_tac₂ : ∀ (toFractionRing toFractionRing_1 toFractionRing_2 : FractionRing K[X]),
  { toFractionRing := toFractionRing : K⟮X⟯ } *
      ({ toFractionRing := toFractionRing_1 : K⟮X⟯ } + { toFractionRing := toFractionRing_2 : K⟮X⟯ }) =
    { toFractionRing := toFractionRing : K⟮X⟯ } * { toFractionRing := toFractionRing_1 : K⟮X⟯ } +
      { toFractionRing := toFractionRing : K⟮X⟯ } * { toFractionRing := toFractionRing_2 : K⟮X⟯ }
Tactic: frac_tac
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
⊢ ∀ (a b c : K⟮X⟯), (a + b) * c = a * c + b * c
have frac_tac : ∀ (toFractionRing : FractionRing K[X]) (b c : K⟮X⟯),
  ({ toFractionRing := toFractionRing : K⟮X⟯ } + b) * c = { toFractionRing := toFractionRing : K⟮X⟯ } * c + b * c
Tactic: frac_tac