awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
r : K
y : K[X] × ↥K[X]⁰
H :
  { toFractionRing := r • Localization.mk y.1 y.2 : K⟮X⟯ } =
    HSMul.hSMul (α := K[X]) ((Polynomial.C : (a : K) → K[X]) r : K[X])
      { toFractionRing := Localization.mk y.1 y.2 : K⟮X⟯ }
H₁ :
  { toFractionRing := r • Localization.mk y.1 y.2 : K⟮X⟯ } =
    { toFractionRing := HSMul.hSMul (α := K[X]) ((Polynomial.C : (a : K) → K[X]) r : K[X]) (Localization.mk y.1 y.2) }
H₂ :
  { toFractionRing := Localization.mk (r • y.1) y.2 : K⟮X⟯ } =
    { toFractionRing := HSMul.hSMul (α := K[X]) ((Polynomial.C : (a : K) → K[X]) r : K[X]) (Localization.mk y.1 y.2) }
H₃ :
  { toFractionRing := Localization.mk (r • y.1) y.2 : K⟮X⟯ } =
    { toFractionRing := Localization.mk (HSMul.hSMul (α := K[X]) ((Polynomial.C : (a : K) → K[X]) r : K[X]) y.1) y.2 }
H₄ :
  { toFractionRing := Localization.mk (r • y.1) y.2 : K⟮X⟯ } =
    { toFractionRing := Localization.mk (HMul.hMul (α := K[X]) ((Polynomial.C : (a : K) → K[X]) r : K[X]) y.1) y.2 }
H₅ H₆ :
  { toFractionRing := Localization.mk (HMul.hMul (α := K[X]) ((Polynomial.C : (a : K) → K[X]) r : K[X]) y.1) y.2 :
      K⟮X⟯ } =
    { toFractionRing := Localization.mk (HMul.hMul (α := K[X]) ((Polynomial.C : (a : K) → K[X]) r : K[X]) y.1) y.2 }
⊢ r • { toFractionRing := Localization.mk y.1 y.2 : K⟮X⟯ } =
    HSMul.hSMul (α := K[X]) ((Polynomial.C : (a : K) → K[X]) r : K[X])
      { toFractionRing := Localization.mk y.1 y.2 : K⟮X⟯ }

Tactic:
rw [← ofFractionRing_smul, ← ofFractionRing_smul, Localization.smul_mk,
    Localization.smul_mk, smul_eq_mul, Polynomial.smul_eq_C_mul]

Premises used: Polynomial.smul_eq_C_mul, RatFunc.ofFractionRing_smul, Localization.smul_mk, smul_eq_mul
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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
pos : ∀ (hq : q = 0), RatFunc.mk (c • p) q = c • RatFunc.mk p q
neg : ∀ (hq : ¬q = 0), RatFunc.mk (c • p) q = c • RatFunc.mk p q
⊢ RatFunc.mk (c • p) q = c • RatFunc.mk p q

Tactic:
by_cases hq : q = 0
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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⟯ }
pos₄ pos₅ : Eq.{u + 1} (α := K⟮X⟯) { toFractionRing := 0 } { toFractionRing := 0 }
⊢ RatFunc.mk (c • p) q = c • RatFunc.mk p q

Tactic:
rw [hq, mk_zero, mk_zero, ← ofFractionRing_smul, smul_zero]

Premises used: smul_zero, RatFunc.ofFractionRing_smul, RatFunc.mk_zero
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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⟯ }
neg₃ neg₄ :
  {
      toFractionRing :=
        c • Localization.mk p (Subtype.mk (p := fun (x : K[X]) ↦ Membership.mem (γ := Submonoid K[X]) K[X]⁰ x) q ⋯) :
      K⟮X⟯ } =
    {
      toFractionRing :=
        c • Localization.mk p (Subtype.mk (p := fun (x : K[X]) ↦ Membership.mem (γ := Submonoid K[X]) K[X]⁰ x) q ⋯) }
⊢ RatFunc.mk (c • p) q = c • RatFunc.mk p q

Tactic:
rw [mk_eq_localization_mk _ hq, mk_eq_localization_mk _ hq, ← Localization.smul_mk, ←
      ofFractionRing_smul]

Premises used: RatFunc.mk_eq_localization_mk, RatFunc.ofFractionRing_smul, Localization.smul_mk
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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
rw₃ rw₄ : c • p • RatFunc.mk q r = c • p • RatFunc.mk q r
⊢ (c • p) • RatFunc.mk q r = c • p • RatFunc.mk q r

Tactic:
rw [← mk_smul, smul_assoc, mk_smul, mk_smul]

Premises used: RatFunc.mk_smul, smul_assoc
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
inst_1 : Subsingleton K
⊢ Subsingleton.{u + 1} K⟮X⟯

Tactic:
toFractionRing_injective.subsingleton

Premises used: RatFunc.toFractionRing_injective, Function.Injective.subsingleton
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
inst_1 : Nontrivial K
⊢ Nontrivial.{u} K⟮X⟯

Tactic:
ofFractionRing_injective.nontrivial

Premises used: Function.Injective.nontrivial, RatFunc.ofFractionRing_injective
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
x x_1 : K⟮X⟯
toFractionRing toFractionRing_1 : FractionRing K[X]
⊢ ({ toFractionRing := toFractionRing : K⟮X⟯ } * { toFractionRing := toFractionRing_1 : K⟮X⟯ }).toFractionRing =
    { toFractionRing := toFractionRing : K⟮X⟯ }.toFractionRing *
      { toFractionRing := toFractionRing_1 : K⟮X⟯ }.toFractionRing

Tactic:
simp [← ofFractionRing_mul]

Premises used: RatFunc.ofFractionRing_mul
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
x x_1 : K⟮X⟯
toFractionRing toFractionRing_1 : FractionRing K[X]
⊢ ({ toFractionRing := toFractionRing : K⟮X⟯ } + { toFractionRing := toFractionRing_1 : K⟮X⟯ }).toFractionRing =
    { toFractionRing := toFractionRing : K⟮X⟯ }.toFractionRing +
      { toFractionRing := toFractionRing_1 : K⟮X⟯ }.toFractionRing

Tactic:
simp [← ofFractionRing_add]

Premises used: RatFunc.ofFractionRing_add
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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)
frac_tac₂ frac_tac₃ 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⟯ })
⊢ ∀ (a b c : K⟮X⟯), a * b * c = a * (b * c)

Tactic:
frac_tac
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
frac_tac frac_tac₁ frac_tac₂ :
  ∀ (toFractionRing : FractionRing K[X]),
    1 * { toFractionRing := toFractionRing : K⟮X⟯ } = { toFractionRing := toFractionRing }
⊢ ∀ (a : K⟮X⟯), 1 * a = a

Tactic:
frac_tac
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
frac_tac frac_tac₁ frac_tac₂ :
  ∀ (toFractionRing : FractionRing K[X]),
    { toFractionRing := toFractionRing : K⟮X⟯ } * 1 = { toFractionRing := toFractionRing }
⊢ ∀ (a : K⟮X⟯), a * 1 = a

Tactic:
frac_tac
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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⟯ }
frac_tac₁ frac_tac₂ 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⟯ }
⊢ ∀ (a b : K⟮X⟯), a * b = b * a

Tactic:
frac_tac
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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)
frac_tac₂ frac_tac₃ 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⟯ })
⊢ ∀ (a b c : K⟮X⟯), a + b + c = a + (b + c)

Tactic:
frac_tac
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
frac_tac frac_tac₁ frac_tac₂ :
  ∀ (toFractionRing : FractionRing K[X]),
    0 + { toFractionRing := toFractionRing : K⟮X⟯ } = { toFractionRing := toFractionRing }
⊢ ∀ (a : K⟮X⟯), 0 + a = a

Tactic:
frac_tac
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
frac_tac frac_tac₁ frac_tac₂ :
  ∀ (toFractionRing : FractionRing K[X]),
    { toFractionRing := toFractionRing : K⟮X⟯ } + 0 = { toFractionRing := toFractionRing }
⊢ ∀ (a : K⟮X⟯), a + 0 = a

Tactic:
frac_tac
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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
smul_tac₄ smul_tac₅ smul_tac₆ smul_tac₇ :
  ∀ (toFractionRing : FractionRing K[X]), { toFractionRing := HSMul.hSMul (α := ℕ) 0 toFractionRing : K⟮X⟯ } = 0
⊢ ∀ (x : K⟮X⟯), HSMul.hSMul (α := ℕ) 0 x = 0

Tactic:
smul_tac
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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⟯ }
smul_tac₄ smul_tac₅ smul_tac₆ smul_tac₇ :
  ∀ (toFractionRing : FractionRing K[X]),
    { toFractionRing := (x + 1) • toFractionRing : K⟮X⟯ } =
      { toFractionRing := x • toFractionRing : K⟮X⟯ } + { toFractionRing := toFractionRing : K⟮X⟯ }
⊢ ∀ (x_1 : K⟮X⟯), (x + 1) • x_1 = x • x_1 + x_1

Tactic:
smul_tac
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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
frac_tac₁ frac_tac₂ 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⟯ }
⊢ ∀ (a b : K⟮X⟯), a - b = a + -b

Tactic:
frac_tac
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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
smul_tac₄ smul_tac₅ smul_tac₆ smul_tac₇ :
  ∀ (toFractionRing : FractionRing K[X]), { toFractionRing := HSMul.hSMul (α := ℤ) 0 toFractionRing : K⟮X⟯ } = 0
⊢ ∀ (a : K⟮X⟯), HSMul.hSMul (α := ℤ) 0 a = 0

Tactic:
smul_tac
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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⟯ }
smul_tac₄ smul_tac₅ smul_tac₆ 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⟯ }
⊢ ∀ (a : K⟮X⟯), HSMul.hSMul (α := ℤ) (↑x.succ : ℤ) a = HSMul.hSMul (α := ℤ) (↑x : ℤ) a + a

Tactic:
smul_tac
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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⟯ }
smul_tac₄ smul_tac₅ smul_tac₆ smul_tac₇ :
  ∀ (toFractionRing : FractionRing K[X]),
    { toFractionRing := Int.negSucc x • toFractionRing : K⟮X⟯ } =
      -{ toFractionRing := HSMul.hSMul (α := ℤ) (↑x.succ : ℤ) toFractionRing }
⊢ ∀ (a : K⟮X⟯), Int.negSucc x • a = -HSMul.hSMul (α := ℤ) (↑x.succ : ℤ) a

Tactic:
smul_tac
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
frac_tac frac_tac₁ frac_tac₂ :
  ∀ (toFractionRing : FractionRing K[X]),
    -{ toFractionRing := toFractionRing : K⟮X⟯ } + { toFractionRing := toFractionRing : K⟮X⟯ } = 0
⊢ ∀ (a : K⟮X⟯), -a + a = 0

Tactic:
frac_tac
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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⟯ }
frac_tac₁ frac_tac₂ 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⟯ }
⊢ ∀ (a b : K⟮X⟯), a + b = b + a

Tactic:
frac_tac
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
frac_tac frac_tac₁ frac_tac₂ :
  ∀ (toFractionRing : FractionRing K[X]), 0 * { toFractionRing := toFractionRing : K⟮X⟯ } = 0
⊢ ∀ (a : K⟮X⟯), 0 * a = 0

Tactic:
frac_tac
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
frac_tac frac_tac₁ frac_tac₂ :
  ∀ (toFractionRing : FractionRing K[X]), { toFractionRing := toFractionRing : K⟮X⟯ } * 0 = 0
⊢ ∀ (a : K⟮X⟯), a * 0 = 0

Tactic:
frac_tac
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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
frac_tac₂ frac_tac₃ 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⟯ }
⊢ ∀ (a b c : K⟮X⟯), a * (b + c) = a * b + a * c

Tactic:
frac_tac
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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⟯ } * c + 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⟯ } * c + { toFractionRing := toFractionRing_1 : K⟮X⟯ } * c
frac_tac₂ frac_tac₃ 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_2 : K⟮X⟯ } +
        { toFractionRing := toFractionRing_1 : K⟮X⟯ } * { toFractionRing := toFractionRing_2 : K⟮X⟯ }
⊢ ∀ (a b c : K⟮X⟯), (a + b) * c = a * c + b * c

Tactic:
frac_tac
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst_1 : CommGroupWithZero G₀
inst_2 : Field L
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : FunLike.{u_5 + 1, u_3 + 1, u_4 + 1} F R[X] S[X]
inst_6 : MonoidHomClass.{u_5, u_3, u_4} F R[X] S[X]
φ : F
hφ : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ S[X]⁰)
f : R⟮X⟯
p q p' q' : R[X]
hq : Membership.mem (γ := Submonoid R[X]) R[X]⁰ q
hq' : Membership.mem (γ := Submonoid R[X]) R[X]⁰ q'
h : q' * p = q * p'
simp :
  (Localization.r S[X]⁰ : (a : S[X] × ↥S[X]⁰) → S[X] × ↥S[X]⁰ → Prop)
    (((φ : (a : R[X]) → S[X]) p,
        Subtype.mk (p := fun (x : S[X]) ↦ Membership.mem (γ := Submonoid S[X]) S[X]⁰ x) ((φ : (a : R[X]) → S[X]) q) ⋯) :
      S[X] × ↥S[X]⁰)
    ((φ : (a : R[X]) → S[X]) p',
      Subtype.mk (p := fun (x : S[X]) ↦ Membership.mem (γ := Submonoid S[X]) S[X]⁰ x) ((φ : (a : R[X]) → S[X]) q') ⋯)
⊢ Eq.{u_4 + 1} (α := S⟮X⟯)
    ((fun (n d : R[X]) ↦
        (if h :
              Membership.mem.{u_4, u_4} (α := S[X]) (γ := Submonoid S[X]) S[X]⁰ ((φ : (a : R[X]) → S[X]) d : S[X]) then
            {
              toFractionRing :=
                Localization.mk ((φ : (a : R[X]) → S[X]) n)
                  (Subtype.mk (p := fun (x : S[X]) ↦ Membership.mem (γ := Submonoid S[X]) S[X]⁰ x)
                    ((φ : (a : R[X]) → S[X]) d) h) }
          else 0 :
          S⟮X⟯))
      p q)
    ((fun (n d : R[X]) ↦
        (if h :
              Membership.mem.{u_4, u_4} (α := S[X]) (γ := Submonoid S[X]) S[X]⁰ ((φ : (a : R[X]) → S[X]) d : S[X]) then
            {
              toFractionRing :=
                Localization.mk ((φ : (a : R[X]) → S[X]) n)
                  (Subtype.mk (p := fun (x : S[X]) ↦ Membership.mem (γ := Submonoid S[X]) S[X]⁰ x)
                    ((φ : (a : R[X]) → S[X]) d) h) }
          else 0 :
          S⟮X⟯))
      p' q')

Tactic:
simp only [Submonoid.mem_comap.mp (hφ hq), Submonoid.mem_comap.mp (hφ hq'),
        dif_pos, ofFractionRing.injEq, Localization.mk_eq_mk_iff]

Premises used: RatFunc.ofFractionRing.injEq, Submonoid.mem_comap, dif_pos, Iff.mp, Localization.mk_eq_mk_iff
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst_1 : CommGroupWithZero G₀
inst_2 : Field L
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : FunLike.{u_5 + 1, u_3 + 1, u_4 + 1} F R[X] S[X]
inst_6 : MonoidHomClass.{u_5, u_3, u_4} F R[X] S[X]
φ : F
hφ : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ S[X]⁰)
f : R⟮X⟯
p q p' q' : R[X]
hq : Membership.mem (γ := Submonoid R[X]) R[X]⁰ q
hq' : Membership.mem (γ := Submonoid R[X]) R[X]⁰ q'
h : q' * p = q * p'
⊢ (Localization.r S[X]⁰ : (a : S[X] × ↥S[X]⁰) → S[X] × ↥S[X]⁰ → Prop)
    (((φ : (a : R[X]) → S[X]) p,
        Subtype.mk (p := fun (x : S[X]) ↦ Membership.mem (γ := Submonoid S[X]) S[X]⁰ x) ((φ : (a : R[X]) → S[X]) q) ⋯) :
      S[X] × ↥S[X]⁰)
    ((φ : (a : R[X]) → S[X]) p',
      Subtype.mk (p := fun (x : S[X]) ↦ Membership.mem (γ := Submonoid S[X]) S[X]⁰ x) ((φ : (a : R[X]) → S[X]) q') ⋯)

Tactic:
Localization.r_of_eq ?_

Premises used: Localization.r_of_eq
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst_1 : CommGroupWithZero G₀
inst_2 : Field L
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : FunLike.{u_5 + 1, u_3 + 1, u_4 + 1} F R[X] S[X]
inst_6 : MonoidHomClass.{u_5, u_3, u_4} F R[X] S[X]
φ : F
hφ : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ S[X]⁰)
f : R⟮X⟯
p q p' q' : R[X]
hq : Membership.mem (γ := Submonoid R[X]) R[X]⁰ q
hq' : Membership.mem (γ := Submonoid R[X]) R[X]⁰ q'
h : q' * p = q * p'
refine :
  HMul.hMul (α := S[X]) (β := S[X])
      ((↑((φ : (a : R[X]) → S[X]) p',
                Subtype.mk (p := fun (x : S[X]) ↦ Membership.mem (γ := Submonoid S[X]) S[X]⁰ x)
                  ((φ : (a : R[X]) → S[X]) q') ⋯).2 :
          S[X]) :
        S[X])
      (((φ : (a : R[X]) → S[X]) p,
            Subtype.mk (p := fun (x : S[X]) ↦ Membership.mem (γ := Submonoid S[X]) S[X]⁰ x) ((φ : (a : R[X]) → S[X]) q)
              ⋯).1 :
        S[X]) =
    HMul.hMul (α := S[X]) (β := S[X])
      ((↑((φ : (a : R[X]) → S[X]) p,
                Subtype.mk (p := fun (x : S[X]) ↦ Membership.mem (γ := Submonoid S[X]) S[X]⁰ x)
                  ((φ : (a : R[X]) → S[X]) q) ⋯).2 :
          S[X]) :
        S[X])
      (((φ : (a : R[X]) → S[X]) p',
            Subtype.mk (p := fun (x : S[X]) ↦ Membership.mem (γ := Submonoid S[X]) S[X]⁰ x) ((φ : (a : R[X]) → S[X]) q')
              ⋯).1 :
        S[X])
⊢ (Localization.r S[X]⁰ : (a : S[X] × ↥S[X]⁰) → S[X] × ↥S[X]⁰ → Prop)
    (((φ : (a : R[X]) → S[X]) p,
        Subtype.mk (p := fun (x : S[X]) ↦ Membership.mem (γ := Submonoid S[X]) S[X]⁰ x) ((φ : (a : R[X]) → S[X]) q) ⋯) :
      S[X] × ↥S[X]⁰)
    ((φ : (a : R[X]) → S[X]) p',
      Subtype.mk (p := fun (x : S[X]) ↦ Membership.mem (γ := Submonoid S[X]) S[X]⁰ x) ((φ : (a : R[X]) → S[X]) q') ⋯)

Tactic:
refine Localization.r_of_eq ?_

Premises used: Localization.r_of_eq