awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
hx : x ≠ 0
refine :
  x⁻¹ =
    HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.denom : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.num : K⟮X⟯)
⊢ ∃ (p : K[X]),
    x⁻¹ =
      HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p : K⟮X⟯)
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.num : K⟮X⟯)

Tactic:
refine ⟨x.denom, ?_⟩
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
hx : x ≠ 0
apply : x.denom ∣ x⁻¹.num
⊢ Associated x⁻¹.num x.denom

Tactic:
apply associated_of_dvd_dvd (num_inv_dvd hx)

Premises used: associated_of_dvd_dvd, RatFunc.num_inv_dvd
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
hx : x ≠ 0
⊢ x⁻¹⁻¹.denom ∣ x⁻¹.num

Tactic:
denom_inv_dvd (inv_ne_zero hx)

Premises used: RatFunc.denom_inv_dvd, inv_ne_zero
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
hx : x ≠ 0
h : x = x⁻¹⁻¹
⊢ x.denom ∣ x⁻¹.num

Tactic:
convert! denom_inv_dvd (inv_ne_zero hx)

Premises used: RatFunc.denom_inv_dvd, inv_ne_zero
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
hx : x ≠ 0
h h₁ : x = x
⊢ x = x⁻¹⁻¹

Tactic:
rw [inv_inv]

Premises used: inv_inv
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
hx : x ≠ 0
a : Associated x.num x⁻¹.denom
⊢ Associated x⁻¹.denom x.num

Tactic:
apply Associated.symm

Premises used: Associated.symm
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
hx : x ≠ 0
⊢ Associated x⁻¹⁻¹.num x⁻¹.denom

Tactic:
associated_num_inv (inv_ne_zero hx)

Premises used: inv_ne_zero, RatFunc.associated_num_inv
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
hx : x ≠ 0
h : x = x⁻¹⁻¹
⊢ Associated x.num x⁻¹.denom

Tactic:
convert! associated_num_inv (inv_ne_zero hx)

Premises used: inv_ne_zero, RatFunc.associated_num_inv
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
L : Type u_1
F : Type u_2
inst_1 : Zero L
inst_2 : FunLike.{u_2 + 1, u + 1, u_1 + 1} F K[X] L
inst_3 : ZeroHomClass.{u_2, u, u_1} F K[X] L
φ : F
hφ : Function.Injective.{u + 1, u_1 + 1} (α := K[X]) (β := L) (⇑φ : (a : K[X]) → L)
f : K⟮X⟯
⊢ Ne.{u_1 + 1} (α := L) ((φ : (a : K[X]) → L) f.denom : L) (0 : L)

Tactic:
fun H =>
  (denom_ne_zero f) ((map_eq_zero_iff φ hφ).mp H)

Premises used: map_eq_zero_iff, Iff.mp, Not, RatFunc.denom_ne_zero
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
R : Type u_1
F : Type u_2
inst_1 : CommRing R
inst_2 : IsDomain R
inst_3 : FunLike.{u_2 + 1, u + 1, u_1 + 1} F K[X] R[X]
inst_4 : MonoidHomClass.{u_2, u, u_1} F K[X] R[X]
φ : F
hφ : LE.le (α := Submonoid K[X]) K[X]⁰ (Submonoid.comap φ R[X]⁰)
f : K⟮X⟯
hq : f.denom ≠ 0
⊢ (map φ hφ : (a : K⟮X⟯) → R⟮X⟯) f =
    HDiv.hDiv (α := R⟮X⟯) (β := R⟮X⟯)
      ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((φ : (a : K[X]) → R[X]) f.num) : R⟮X⟯)
      ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((φ : (a : K[X]) → R[X]) f.denom) : R⟮X⟯)

Tactic:
rw [← num_div_denom f, map_apply_div_ne_zero, num_div_denom f]

Premises used: RatFunc.num_div_denom, RatFunc.map_apply_div_ne_zero
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
R : Type u_1
F : Type u_2
inst_1 : CommRing R
inst_2 : IsDomain R
inst_3 : FunLike.{u_2 + 1, u + 1, u_1 + 1} F K[X] R[X]
inst_4 : MonoidHomClass.{u_2, u, u_1} F K[X] R[X]
φ : F
hφ : LE.le (α := Submonoid K[X]) K[X]⁰ (Submonoid.comap φ R[X]⁰)
f : K⟮X⟯
⊢ f.denom ≠ 0

Tactic:
denom_ne_zero _

Premises used: RatFunc.denom_ne_zero
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
R : Type u_1
F : Type u_2
inst_1 : CommRing R
inst_2 : IsDomain R
inst_3 : FunLike.{u_2 + 1, u + 1, u_1 + 1} F K[X] R[X]
inst_4 : MonoidHomClass.{u_2, u, u_1} F K[X] R[X]
φ : F
hφ : LE.le (α := Submonoid K[X]) K[X]⁰ (Submonoid.comap φ R[X]⁰)
f : K⟮X⟯
⊢ f.denom ≠ 0

Tactic:
exact denom_ne_zero _

Premises used: RatFunc.denom_ne_zero
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
L : Type u_1
inst_1 : CommGroupWithZero L
φ : MonoidWithZeroHom.{u, u_1} K[X] L
hφ : LE.le (α := Submonoid K[X]) K[X]⁰ (Submonoid.comap φ L⁰)
f : K⟮X⟯
rw :
  (liftMonoidWithZeroHom φ hφ : (a : K⟮X⟯) → L)
      (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⟯)) =
    HDiv.hDiv (α := L) (β := L)
      ((φ : (a : K[X]) → L)
          (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⟯)).num :
        L)
      ((φ : (a : K[X]) → L)
          (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⟯)).denom :
        L)
rw₁ :
  HDiv.hDiv (α := L) (β := L) ((φ : (a : K[X]) → L) f.num : L) ((φ : (a : K[X]) → L) f.denom : L) =
    HDiv.hDiv (α := L) (β := L)
      ((φ : (a : K[X]) → L)
          (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⟯)).num :
        L)
      ((φ : (a : K[X]) → L)
          (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⟯)).denom :
        L)
rw₂ rw₃ :
  HDiv.hDiv (α := L) (β := L) ((φ : (a : K[X]) → L) f.num : L) ((φ : (a : K[X]) → L) f.denom : L) =
    HDiv.hDiv (α := L) (β := L) ((φ : (a : K[X]) → L) f.num : L) ((φ : (a : K[X]) → L) f.denom : L)
⊢ (liftMonoidWithZeroHom φ hφ : (a : K⟮X⟯) → L) f =
    HDiv.hDiv (α := L) (β := L) ((φ : (a : K[X]) → L) f.num : L) ((φ : (a : K[X]) → L) f.denom : L)

Tactic:
rw [← num_div_denom f, liftMonoidWithZeroHom_apply_div, num_div_denom]

Premises used: RatFunc.liftMonoidWithZeroHom_apply_div, RatFunc.num_div_denom
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
L : Type u_1
inst_1 : Field L
φ : RingHom.{u, u_1} K[X] L
hφ : LE.le (α := Submonoid K[X]) K[X]⁰ (Submonoid.comap φ L⁰)
f : K⟮X⟯
⊢ (liftRingHom φ hφ : (a : K⟮X⟯) → L) f =
    HDiv.hDiv (α := L) (β := L) ((φ : (a : K[X]) → L) f.num : L) ((φ : (a : K[X]) → L) f.denom : L)

Tactic:
liftMonoidWithZeroHom_apply _ hφ _

Premises used: RatFunc.liftMonoidWithZeroHom_apply
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
L : Type u_1
S : Type u_2
inst_1 : Field L
inst_2 : CommSemiring S
inst_3 : Algebra.{u_2, u} S K[X]
inst_4 : Algebra S L
φ : AlgHom.{u_2, u, u_1} S K[X] L
hφ : LE.le (α := Submonoid K[X]) K[X]⁰ (Submonoid.comap φ L⁰)
f : K⟮X⟯
⊢ (liftAlgHom φ hφ : (a : K⟮X⟯) → L) f =
    HDiv.hDiv (α := L) (β := L) ((φ : (a : K[X]) → L) f.num : L) ((φ : (a : K[X]) → L) f.denom : L)

Tactic:
liftMonoidWithZeroHom_apply _ hφ _

Premises used: RatFunc.liftMonoidWithZeroHom_apply
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
x y : K⟮X⟯
hxy : x + y ≠ 0
h_zero : x.num * y.denom + x.denom * y.num = 0
⊢ (x + y).num * (x.denom * y.denom) = (x.num * y.denom + x.denom * y.num) * (x + y).denom

Tactic:
have h := num_denom_add x y
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
x y : K⟮X⟯
hxy : x + y ≠ 0
h_zero : x.num * y.denom + x.denom * y.num = 0
h : (x + y).num * (x.denom * y.denom) = (x.num * y.denom + x.denom * y.num) * (x + y).denom
⊢ (x + y).num * (x.denom * y.denom) = 0

Tactic:
rw [h_zero, zero_mul] at h

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
x y : K⟮X⟯
hxy : x + y ≠ 0
h_zero : x.num * y.denom + x.denom * y.num = 0
h : (x + y).num * (x.denom * y.denom) = 0
⊢ False

Tactic:
(mul_ne_zero (num_ne_zero hxy) (mul_ne_zero x.denom_ne_zero y.denom_ne_zero)) h

Premises used: RatFunc.num_ne_zero, mul_ne_zero, RatFunc.denom_ne_zero
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
x y : K⟮X⟯
hxy : x + y ≠ 0
h_zero : x.num * y.denom + x.denom * y.num = 0
h : (x + y).num * (x.denom * y.denom) = 0
⊢ False

Tactic:
exact (mul_ne_zero (num_ne_zero hxy) (mul_ne_zero x.denom_ne_zero y.denom_ne_zero)) h

Premises used: RatFunc.num_ne_zero, mul_ne_zero, RatFunc.denom_ne_zero
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
p : ℕ
inst_1 : CharP K p
⊢ CharP.{u} K⟮X⟯ p

Tactic:
charP_of_injective_algebraMap' K p

Premises used: charP_of_injective_algebraMap'
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
p : ℕ
inst_1 : ExpChar K p
⊢ ExpChar.{u} K⟮X⟯ p

Tactic:
ExpChar.of_injective_algebraMap' K p

Premises used: ExpChar.of_injective_algebraMap'
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : Field K
inst_1 : CharZero K
⊢ CharZero.{u} K⟮X⟯

Tactic:
Algebra.charZero_of_charZero K _

Premises used: Algebra.charZero_of_charZero
-- Module: Mathlib.FieldTheory.RatFunc.Defs
Goal:
K : Type u
inst : CommRing K
⊢ Function.Injective.{u + 1, u + 1} (α := FractionRing K[X]) ofFractionRing

Tactic:
fun _ _ => ofFractionRing.inj

Premises used: Function.Injective, RatFunc.ofFractionRing.inj
-- Module: Mathlib.FieldTheory.RatFunc.Defs
Goal:
K : Type u
inst : CommRing K
x y : FractionRing K[X]
xy : { toFractionRing := x : K⟮X⟯ }.toFractionRing = { toFractionRing := y }.toFractionRing
subst : { toFractionRing := x : K⟮X⟯ } = { toFractionRing := { toFractionRing := x }.toFractionRing }
⊢ { toFractionRing := x : K⟮X⟯ } = { toFractionRing := y }

Tactic:
subst xy
-- Module: Mathlib.FieldTheory.RatFunc.Defs
Goal:
K : Type u
inst : CommRing K
x : FractionRing K[X]
⊢ { toFractionRing := x : K⟮X⟯ } = { toFractionRing := { toFractionRing := x }.toFractionRing }

Tactic:
rfl
-- Module: Mathlib.FieldTheory.RatFunc.Defs
Goal:
K : Type u
inst : CommRing K
x y : K⟮X⟯
⊢ x.toFractionRing = y.toFractionRing ↔ x = y

Tactic:
toFractionRing_injective.eq_iff

Premises used: RatFunc.toFractionRing_injective, Function.Injective.eq_iff
-- Module: Mathlib.FieldTheory.RatFunc.Defs
Goal:
K : Type u
inst : CommRing K
P : Sort v
n : K[X]
d : ↥K[X]⁰
f : K[X] → K[X] → P
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'
rw :
  Localization.liftOn { toFractionRing := Localization.mk n d : K⟮X⟯ }.toFractionRing
      (fun (p : K[X]) (q : ↥K[X]⁰) ↦ f p (↑q : K[X])) ⋯ =
    f n (↑d : K[X])
⊢ { toFractionRing := Localization.mk n d : K⟮X⟯ }.liftOn f @H = f n (↑d : K[X])

Tactic:
rw [RatFunc.liftOn]

Premises used: RatFunc.liftOn
-- Module: Mathlib.FieldTheory.RatFunc.Defs
Goal:
K : Type u
inst : CommRing K
P : Sort v
n : K[X]
d : ↥K[X]⁰
f : K[X] → K[X] → P
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'
⊢ Localization.liftOn { toFractionRing := Localization.mk n d : K⟮X⟯ }.toFractionRing
      (fun (p : K[X]) (q : ↥K[X]⁰) ↦ f p (↑q : K[X])) ⋯ =
    f n (↑d : K[X])

Tactic:
Localization.liftOn_mk _ _ _ _

Premises used: Localization.mk, Localization.liftOn_mk, Quotient.mk', OreLocalization.oreDiv
-- Module: Mathlib.FieldTheory.RatFunc.Defs
Goal:
K : Type u
inst : CommRing K
P : Sort v
n : K[X]
d : ↥K[X]⁰
f : K[X] → K[X] → P
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'
⊢ Localization.liftOn { toFractionRing := Localization.mk n d : K⟮X⟯ }.toFractionRing
      (fun (p : K[X]) (q : ↥K[X]⁰) ↦ f p (↑q : K[X])) ⋯ =
    f n (↑d : K[X])

Tactic:
exact Localization.liftOn_mk _ _ _ _

Premises used: Localization.liftOn_mk
-- Module: Mathlib.FieldTheory.RatFunc.Defs
Goal:
K : Type u
inst : CommRing K
P : Sort v
f : K[X] → K[X] → P
H : ∀ {p q a : K[X]}, q ≠ 0 → ∀ (_ha : a ≠ 0), f (a * p) (a * q) = f p q
p q p' q' : K[X]
hq : q ≠ 0
hq' : q' ≠ 0
h : q' * p = q * p'
rw : f (q * p') (q' * q) = f (q * p') (q * q')
rw₁ rw₂ : f (q * p') (q * q') = f (q * p') (q * q')
⊢ f (q' * p) (q' * q) = f (q * p') (q * q')

Tactic:
rw [h, mul_comm q']

Premises used: mul_comm
-- Module: Mathlib.FieldTheory.RatFunc.Defs
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
p q : K[X]
rw rw₁ :
  {
      toFractionRing :=
        HDiv.hDiv (α := FractionRing K[X]) (β := FractionRing K[X])
          ((algebraMap K[X] (FractionRing K[X]) : (a : K[X]) → FractionRing K[X]) p : FractionRing K[X])
          ((algebraMap K[X] (FractionRing K[X]) : (a : K[X]) → FractionRing K[X]) q : FractionRing K[X]) :
      K⟮X⟯ } =
    {
      toFractionRing :=
        HDiv.hDiv (α := FractionRing K[X]) (β := FractionRing K[X])
          ((algebraMap K[X] (FractionRing K[X]) : (a : K[X]) → FractionRing K[X]) p : FractionRing K[X])
          ((algebraMap K[X] (FractionRing K[X]) : (a : K[X]) → FractionRing K[X]) q : FractionRing K[X]) }
⊢ RatFunc.mk p q =
    {
      toFractionRing :=
        HDiv.hDiv (α := FractionRing K[X]) (β := FractionRing K[X])
          ((algebraMap K[X] (FractionRing K[X]) : (a : K[X]) → FractionRing K[X]) p : FractionRing K[X])
          ((algebraMap K[X] (FractionRing K[X]) : (a : K[X]) → FractionRing K[X]) q : FractionRing K[X]) }

Tactic:
rw [RatFunc.mk]

Premises used: RatFunc.mk
-- Module: Mathlib.FieldTheory.RatFunc.Defs
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
p : K[X]
rw :
  {
      toFractionRing :=
        HDiv.hDiv (α := FractionRing K[X]) (β := FractionRing K[X])
          ((algebraMap K[X] (FractionRing K[X]) : (a : K[X]) → FractionRing K[X]) p : FractionRing K[X])
          ((algebraMap K[X] (FractionRing K[X]) : (a : K[X]) → FractionRing K[X]) 0 : FractionRing K[X]) :
      K⟮X⟯ } =
    { toFractionRing := 0 }
rw₁ :
  {
      toFractionRing :=
        HDiv.hDiv (α := FractionRing K[X]) (β := FractionRing K[X])
          ((algebraMap K[X] (FractionRing K[X]) : (a : K[X]) → FractionRing K[X]) p : FractionRing K[X])
          (0 : FractionRing K[X]) :
      K⟮X⟯ } =
    { toFractionRing := 0 }
rw₂ rw₃ : Eq.{u + 1} (α := K⟮X⟯) { toFractionRing := 0 } { toFractionRing := 0 }
⊢ RatFunc.mk p 0 = { toFractionRing := 0 }

Tactic:
rw [mk_eq_div', map_zero, div_zero]

Premises used: RatFunc.mk_eq_div', map_zero, div_zero
-- Module: Mathlib.FieldTheory.RatFunc.Defs
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
p : K[X]
q : ↥K[X]⁰
⊢ RatFunc.mk p (↑q : K[X]) = { toFractionRing := IsLocalization.mk' (FractionRing K[X]) p q }

Tactic:
simp only [mk_eq_div', ← Localization.mk_eq_mk', FractionRing.mk_eq_div]

Premises used: Localization.mk_eq_mk', RatFunc.mk_eq_div', FractionRing.mk_eq_div
-- Module: Mathlib.FieldTheory.RatFunc.Defs
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
p q : K[X]
hq : Membership.mem (γ := Submonoid K[X]) K[X]⁰ q
⊢ RatFunc.mk p q =
    {
      toFractionRing :=
        IsLocalization.mk' (FractionRing K[X]) p
          (Subtype.mk (p := fun (x : K[X]) ↦ Membership.mem (γ := Submonoid K[X]) K[X]⁰ x) q hq) }

Tactic:
simp only [← mk_coe_def]

Premises used: RatFunc.mk_coe_def
-- Module: Mathlib.FieldTheory.RatFunc.Defs
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
p q : K[X]
hq : q ≠ 0
⊢ RatFunc.mk p q =
    {
      toFractionRing :=
        IsLocalization.mk' (FractionRing K[X]) p
          (Subtype.mk (p := fun (x : K[X]) ↦ Membership.mem (γ := Submonoid K[X]) K[X]⁰ x) q ⋯) }

Tactic:
mk_def_of_mem p _

Premises used: RatFunc.mk_def_of_mem
-- Module: Mathlib.FieldTheory.RatFunc.Defs
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⟯ }
rw₁ 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' (Localization (M := K[X]) K[X]⁰) p
          (Subtype.mk (p := fun (x : K[X]) ↦ Membership.mem (γ := Submonoid K[X]) K[X]⁰ x) q ⋯) }
⊢ RatFunc.mk p q =
    {
      toFractionRing :=
        Localization.mk p (Subtype.mk (p := fun (x : K[X]) ↦ Membership.mem (γ := Submonoid K[X]) K[X]⁰ x) q ⋯) }

Tactic:
rw [mk_def_of_ne _ hq, Localization.mk_eq_mk']

Premises used: RatFunc.mk_def_of_ne, Localization.mk_eq_mk'
-- Module: Mathlib.FieldTheory.RatFunc.Defs
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])
rw₂ rw₃ : RatFunc.mk p 1 = RatFunc.mk p 1
⊢ RatFunc.mk p 1 = { toFractionRing := (algebraMap K[X] (FractionRing K[X]) : (a : K[X]) → FractionRing K[X]) p }

Tactic:
rw [← IsLocalization.mk'_one (M := K[X]⁰) (FractionRing K[X]) p, ← mk_coe_def, Submonoid.coe_one]

Premises used: RatFunc.mk_coe_def, FractionRing, Polynomial, Submonoid.coe_one, IsLocalization.mk'_one
-- Module: Mathlib.FieldTheory.RatFunc.Defs
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
rw₄ rw₅ :
  p * (↑(Subtype.mk (p := fun (x : K[X]) ↦ Membership.mem (γ := Submonoid K[X]) K[X]⁰ x) q' ⋯) : K[X]) =
      p' * (↑(Subtype.mk (p := fun (x : K[X]) ↦ Membership.mem (γ := Submonoid K[X]) K[X]⁰ x) q ⋯) : K[X]) ↔
    p * q' = p' * q
⊢ RatFunc.mk p q = 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]

Premises used: RatFunc.mk_def_of_ne, IsFractionRing.injective, Function.Injective.eq_iff, FractionRing, Polynomial, RatFunc.ofFractionRing_injective, IsLocalization.mk'_eq_iff_eq'
-- Module: Mathlib.FieldTheory.RatFunc.Defs
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
neg : ∀ (hq : ¬q = 0), (RatFunc.mk p q).liftOn f @H = f p q
⊢ (RatFunc.mk p q).liftOn f @H = f p q

Tactic:
by_cases hq : q = 0
-- Module: Mathlib.FieldTheory.RatFunc.Defs
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
pos : (RatFunc.mk p 0).liftOn f @H = f p 0
⊢ (RatFunc.mk p q).liftOn f @H = f p q

Tactic:
subst hq
-- Module: Mathlib.FieldTheory.RatFunc.Defs
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
P : Sort v
p : 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 0).liftOn f @H = f p 0

Tactic:
simp only [mk_zero, f0, ← Localization.mk_zero 1,
      liftOn_ofFractionRing_mk, Submonoid.coe_one]

Premises used: RatFunc.liftOn_ofFractionRing_mk, Submonoid.coe_one, RatFunc.mk_zero, OfNat.ofNat, Localization.mk_zero
-- Module: Mathlib.FieldTheory.RatFunc.Defs
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

Tactic:
simp only [mk_eq_localization_mk _ hq, liftOn_ofFractionRing_mk]

Premises used: RatFunc.liftOn_ofFractionRing_mk, RatFunc.mk_eq_localization_mk
-- Module: Mathlib.FieldTheory.RatFunc.Defs
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
rw : ∀ {p q p' q' : K[X]} (_hq : q ≠ 0) (_hq' : q' ≠ 0), q' * p = q * p' → f p q = f p' q'
⊢ (RatFunc.mk p q).liftOn' f @H = f p q

Tactic:
rw [RatFunc.liftOn', RatFunc.liftOn_mk _ _ _ f0]

Premises used: nonZeroDivisors.ne_zero, RatFunc.liftOn', RatFunc.liftOn_mk
-- Module: Mathlib.FieldTheory.RatFunc.Defs
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
⊢ ∀ {p q p' q' : K[X]} (_hq : q ≠ 0) (_hq' : q' ≠ 0), q' * p = q * p' → f p q = f p' q'

Tactic:
apply liftOn_condition_of_liftOn'_condition H

Premises used: RatFunc.liftOn_condition_of_liftOn'_condition
-- Module: Mathlib.FieldTheory.RatFunc.Defs
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
P : K⟮X⟯ → Prop
x : FractionRing K[X]
f : ∀ (p q : K[X]), q ≠ 0 → P (RatFunc.mk p q)
x_1 : K[X] × ↥K[X]⁰
p : K[X]
q : ↥K[X]⁰
⊢ P { toFractionRing := Localization.mk (p, q).1 (p, q).2 }

Tactic:
simpa only [mk_coe_def, Localization.mk_eq_mk'] using
        f p q (mem_nonZeroDivisors_iff_ne_zero.mp q.2)

Premises used: RatFunc.mk_coe_def, Localization.mk_eq_mk', Iff.mp, mem_nonZeroDivisors_iff_ne_zero, Subtype.val, Subtype.property