awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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]
φ : RingHom.{u_3, u_2} R[X] L
hφ : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ L⁰)
x y : R⟮X⟯
simp : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp only [ZeroHom.toFun_eq_coe, MonoidWithZeroHom.toZeroHom_coe]

Premises used: MonoidWithZeroHom.toZeroHom_coe, ZeroHom.toFun_eq_coe
-- 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]
φ : RingHom.{u_3, u_2} R[X] L
hφ : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ L⁰)
x y : R⟮X⟯
inl : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
inr : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
cases subsingleton_or_nontrivial R

Premises used: subsingleton_or_nontrivial
-- 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]
φ : RingHom.{u_3, u_2} R[X] L
hφ : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ L⁰)
x y : R⟮X⟯
h : Nontrivial R
inr : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
obtain ⟨x⟩ := x
-- 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]
φ : RingHom.{u_3, u_2} R[X] L
hφ : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ L⁰)
y : R⟮X⟯
h : Nontrivial R
x : FractionRing R[X]
inr : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
obtain ⟨y⟩ := y
-- 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]
φ : RingHom.{u_3, u_2} R[X] L
hφ : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ L⁰)
h : Nontrivial R
x y : FractionRing R[X]
inr : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
cases x using Localization.induction_on with | _ pq
-- 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]
φ : RingHom.{u_3, u_2} R[X] L
hφ : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ L⁰)
h : Nontrivial R
y : FractionRing R[X]
pq : R[X] × ↥R[X]⁰
inr : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
cases y using Localization.induction_on with | _ p'q'
-- 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]
φ : RingHom.{u_3, u_2} R[X] L
hφ : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ L⁰)
h : Nontrivial R
pq p'q' : R[X] × ↥R[X]⁰
inr : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
obtain ⟨p, q⟩ := pq
-- 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]
φ : RingHom.{u_3, u_2} R[X] L
hφ : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ L⁰)
h : Nontrivial R
p'q' : R[X] × ↥R[X]⁰
p : R[X]
q : ↥R[X]⁰
inr : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
obtain ⟨p', q'⟩ := p'q'
-- 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]
φ : RingHom.{u_3, u_2} R[X] L
hφ : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ L⁰)
h : Nontrivial R
p : R[X]
q : ↥R[X]⁰
p' : R[X]
q' : ↥R[X]⁰
inr : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rw [← ofFractionRing_add, Localization.add_mk]

Premises used: RatFunc.ofFractionRing_add, Localization.add_mk
-- 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]
φ : RingHom.{u_3, u_2} R[X] L
hφ : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ L⁰)
h : Nontrivial R
p : R[X]
q : ↥R[X]⁰
p' : R[X]
q' : ↥R[X]⁰
inr :
  HDiv.hDiv (α := L) (β := L) ((φ : (a : R[X]) → L) ((↑q : R[X]) * p' + (↑q' : R[X]) * p) : L)
      ((φ : (a : R[X]) → L) (↑(q * q') : R[X]) : L) =
    HDiv.hDiv (α := L) (β := L) ((φ : (a : R[X]) → L) p : L) ((φ : (a : R[X]) → L) (↑q : R[X]) : L) +
      HDiv.hDiv (α := L) (β := L) ((φ : (a : R[X]) → L) p' : L) ((φ : (a : R[X]) → L) (↑q' : R[X]) : L)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp only [RingHom.toMonoidWithZeroHom_eq_coe,
        liftMonoidWithZeroHom_apply_ofFractionRing_mk]

Premises used: RatFunc.liftMonoidWithZeroHom_apply_ofFractionRing_mk, RingHom.toMonoidWithZeroHom_eq_coe
-- 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]
φ : RingHom.{u_3, u_2} R[X] L
hφ : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ L⁰)
h : Nontrivial R
p : R[X]
q : ↥R[X]⁰
p' : R[X]
q' : ↥R[X]⁰
inr :
  HMul.hMul (α := L) ((φ : (a : R[X]) → L) ((↑q : R[X]) * p' + (↑q' : R[X]) * p) : L)
      (HMul.hMul (α := L) (β := L) ((φ : (a : R[X]) → L) (↑q : R[X]) : L) ((φ : (a : R[X]) → L) (↑q' : R[X]) : L)) =
    HMul.hMul (β := L)
      (HMul.hMul (α := L) (β := L) ((φ : (a : R[X]) → L) p : L) ((φ : (a : R[X]) → L) (↑q' : R[X]) : L) +
        HMul.hMul (α := L) (β := L) ((φ : (a : R[X]) → L) (↑q : R[X]) : L) ((φ : (a : R[X]) → L) p' : L))
      ((φ : (a : R[X]) → L) (↑(q * q') : R[X]) : L)
inr₁ : Ne.{u_2 + 1} (α := L) ((φ : (a : R[X]) → L) (↑(q * q') : R[X]) : L) (0 : L)
inr₂ : HMul.hMul (α := L) (β := L) ((φ : (a : R[X]) → L) (↑q : R[X]) : L) ((φ : (a : R[X]) → L) (↑q' : R[X]) : L) ≠ 0
inr₃ : Ne.{u_2 + 1} (α := L) ((φ : (a : R[X]) → L) (↑q : R[X]) : L) (0 : L)
inr₄ : Ne.{u_2 + 1} (α := L) ((φ : (a : R[X]) → L) (↑q' : R[X]) : L) (0 : L)
⊢ HDiv.hDiv (α := L) (β := L) ((φ : (a : R[X]) → L) ((↑q : R[X]) * p' + (↑q' : R[X]) * p) : L)
      ((φ : (a : R[X]) → L) (↑(q * q') : R[X]) : L) =
    HDiv.hDiv (α := L) (β := L) ((φ : (a : R[X]) → L) p : L) ((φ : (a : R[X]) → L) (↑q : R[X]) : L) +
      HDiv.hDiv (α := L) (β := L) ((φ : (a : R[X]) → L) p' : L) ((φ : (a : R[X]) → L) (↑q' : R[X]) : L)

Tactic:
rw [div_add_div, div_eq_div_iff]

Premises used: div_eq_div_iff, div_add_div
-- 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]
φ : RingHom.{u_3, u_2} R[X] L
hφ : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ L⁰)
h : Nontrivial R
p : R[X]
q : ↥R[X]⁰
p' : R[X]
q' : ↥R[X]⁰
inr :
  HMul.hMul (α := L) ((φ : (a : R[X]) → L) (p * (↑q' : R[X]) + p' * (↑q : R[X])) : L)
      (HMul.hMul (α := L) (β := L) ((φ : (a : R[X]) → L) (↑q : R[X]) : L) ((φ : (a : R[X]) → L) (↑q' : R[X]) : L)) =
    HMul.hMul (β := L)
      (HMul.hMul (α := L) (β := L) ((φ : (a : R[X]) → L) p : L) ((φ : (a : R[X]) → L) (↑q' : R[X]) : L) +
        HMul.hMul (α := L) (β := L) ((φ : (a : R[X]) → L) p' : L) ((φ : (a : R[X]) → L) (↑q : R[X]) : L))
      ((φ : (a : R[X]) → L) (↑(q * q') : R[X]) : L)
⊢ HMul.hMul (α := L) ((φ : (a : R[X]) → L) ((↑q : R[X]) * p' + (↑q' : R[X]) * p) : L)
      (HMul.hMul (α := L) (β := L) ((φ : (a : R[X]) → L) (↑q : R[X]) : L) ((φ : (a : R[X]) → L) (↑q' : R[X]) : L)) =
    HMul.hMul (β := L)
      (HMul.hMul (α := L) (β := L) ((φ : (a : R[X]) → L) p : L) ((φ : (a : R[X]) → L) (↑q' : R[X]) : L) +
        HMul.hMul (α := L) (β := L) ((φ : (a : R[X]) → L) (↑q : R[X]) : L) ((φ : (a : R[X]) → L) p' : L))
      ((φ : (a : R[X]) → L) (↑(q * q') : R[X]) : L)

Tactic:
rw [mul_comm _ p, mul_comm _ p', mul_comm _ (φ p'), add_comm]

Premises used: add_comm, mul_comm, DFunLike.coe
-- 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]
φ : RingHom.{u_3, u_2} R[X] L
hφ : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ L⁰)
h : Nontrivial R
p : R[X]
q : ↥R[X]⁰
p' : R[X]
q' : ↥R[X]⁰
⊢ HMul.hMul (α := L) ((φ : (a : R[X]) → L) (p * (↑q' : R[X]) + p' * (↑q : R[X])) : L)
      (HMul.hMul (α := L) (β := L) ((φ : (a : R[X]) → L) (↑q : R[X]) : L) ((φ : (a : R[X]) → L) (↑q' : R[X]) : L)) =
    HMul.hMul (β := L)
      (HMul.hMul (α := L) (β := L) ((φ : (a : R[X]) → L) p : L) ((φ : (a : R[X]) → L) (↑q' : R[X]) : L) +
        HMul.hMul (α := L) (β := L) ((φ : (a : R[X]) → L) p' : L) ((φ : (a : R[X]) → L) (↑q : R[X]) : L))
      ((φ : (a : R[X]) → L) (↑(q * q') : R[X]) : L)

Tactic:
simp only [map_add, map_mul, Submonoid.coe_mul]

Premises used: map_add, map_mul, Submonoid.coe_mul
-- 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]
φ : RingHom.{u_3, u_2} R[X] L
hφ : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ L⁰)
h : Nontrivial R
p : R[X]
q : ↥R[X]⁰
p' : R[X]
q' : ↥R[X]⁰
⊢ Ne.{u_2 + 1} (α := L) ((φ : (a : R[X]) → L) (↑(q * q') : R[X]) : L) (0 : L)

Tactic:
nonZeroDivisors.ne_zero (hφ (SetLike.coe_mem _))

Premises used: SetLike.coe_mem, nonZeroDivisors.ne_zero
-- 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]
φ : RingHom.{u_3, u_2} R[X] L
hφ : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ L⁰)
h : Nontrivial R
p : R[X]
q : ↥R[X]⁰
p' : R[X]
q' : ↥R[X]⁰
⊢ Ne.{u_2 + 1} (α := L) ((φ : (a : R[X]) → L) (↑(q * q') : R[X]) : L) (0 : L)

Tactic:
exact nonZeroDivisors.ne_zero (hφ (SetLike.coe_mem _))

Premises used: SetLike.coe_mem, nonZeroDivisors.ne_zero
-- 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]
φ : RingHom.{u_3, u_2} R[X] L
hφ : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ L⁰)
h : Nontrivial R
p : R[X]
q : ↥R[X]⁰
p' : R[X]
q' : ↥R[X]⁰
inr : Ne.{u_2 + 1} (α := L) ((φ : (a : R[X]) → L) (↑(q * q') : R[X]) : L) (0 : L)
⊢ HMul.hMul (α := L) (β := L) ((φ : (a : R[X]) → L) (↑q : R[X]) : L) ((φ : (a : R[X]) → L) (↑q' : R[X]) : L) ≠ 0

Tactic:
simp only [← map_mul, ← Submonoid.coe_mul]

Premises used: map_mul, Submonoid.coe_mul
-- 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]
φ : RingHom.{u_3, u_2} R[X] L
hφ : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ L⁰)
h : Nontrivial R
p : R[X]
q : ↥R[X]⁰
p' : R[X]
q' : ↥R[X]⁰
inr : Ne.{u_2 + 1} (α := L) ((φ : (a : R[X]) → L) (↑(q * q') : R[X]) : L) (0 : L)
⊢ HMul.hMul (α := L) (β := L) ((φ : (a : R[X]) → L) (↑q : R[X]) : L) ((φ : (a : R[X]) → L) (↑q' : R[X]) : L) ≠ 0

Tactic:
try simp only [← map_mul, ← Submonoid.coe_mul]

Premises used: map_mul, Submonoid.coe_mul
-- 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]
φ : RingHom.{u_3, u_2} R[X] L
hφ : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ L⁰)
h : Nontrivial R
p : R[X]
q : ↥R[X]⁰
p' : R[X]
q' : ↥R[X]⁰
⊢ Ne.{u_2 + 1} (α := L) ((φ : (a : R[X]) → L) (↑q : R[X]) : L) (0 : L)

Tactic:
nonZeroDivisors.ne_zero (hφ (SetLike.coe_mem _))

Premises used: SetLike.coe_mem, nonZeroDivisors.ne_zero
-- 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]
φ : RingHom.{u_3, u_2} R[X] L
hφ : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ L⁰)
h : Nontrivial R
p : R[X]
q : ↥R[X]⁰
p' : R[X]
q' : ↥R[X]⁰
⊢ Ne.{u_2 + 1} (α := L) ((φ : (a : R[X]) → L) (↑q : R[X]) : L) (0 : L)

Tactic:
exact nonZeroDivisors.ne_zero (hφ (SetLike.coe_mem _))

Premises used: SetLike.coe_mem, nonZeroDivisors.ne_zero
-- 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]
φ : RingHom.{u_3, u_2} R[X] L
hφ : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ L⁰)
h : Nontrivial R
p : R[X]
q : ↥R[X]⁰
p' : R[X]
q' : ↥R[X]⁰
⊢ Ne.{u_2 + 1} (α := L) ((φ : (a : R[X]) → L) (↑q' : R[X]) : L) (0 : L)

Tactic:
nonZeroDivisors.ne_zero (hφ (SetLike.coe_mem _))

Premises used: SetLike.coe_mem, nonZeroDivisors.ne_zero
-- 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]
φ : RingHom.{u_3, u_2} R[X] L
hφ : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ L⁰)
h : Nontrivial R
p : R[X]
q : ↥R[X]⁰
p' : R[X]
q' : ↥R[X]⁰
⊢ Ne.{u_2 + 1} (α := L) ((φ : (a : R[X]) → L) (↑q' : R[X]) : L) (0 : L)

Tactic:
exact nonZeroDivisors.ne_zero (hφ (SetLike.coe_mem _))

Premises used: SetLike.coe_mem, nonZeroDivisors.ne_zero
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
L : Type u_2
R : Type u_3
inst : Field L
inst_1 : CommRing R
φ : RingHom.{u_3, u_2} R[X] L
hφ : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ L⁰)
n : R[X]
d : ↥R[X]⁰
⊢ (liftRingHom φ hφ : (a : R⟮X⟯) → L) { toFractionRing := Localization.mk n d : R⟮X⟯ } =
    HDiv.hDiv (α := L) (β := L) ((φ : (a : R[X]) → L) n : L) ((φ : (a : R[X]) → L) (↑d : R[X]) : L)

Tactic:
liftMonoidWithZeroHom_apply_ofFractionRing_mk _ hφ _ _

Premises used: RatFunc.liftMonoidWithZeroHom_apply_ofFractionRing_mk
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
L : Type u_2
R : Type u_3
inst : Field L
inst_1 : CommRing R
φ : RingHom.{u_3, u_2} R[X] L
hφ : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ L⁰)
x : R[X]
rw :
  HDiv.hDiv (α := L) (β := L) ((φ : (a : R[X]) → L) x : L) ((φ : (a : R[X]) → L) (↑1 : R[X]) : L) =
    (φ : (a : R[X]) → L) x
⊢ Eq.{u_2 + 1} (α := L)
    ((liftRingHom φ hφ : (a : R⟮X⟯) → L)
        { toFractionRing := (algebraMap R[X] (FractionRing R[X]) : (a : R[X]) → FractionRing R[X]) x } :
      L)
    ((φ : (a : R[X]) → L) x : L)

Tactic:
rw [← Localization.mk_one_eq_algebraMap, liftRingHom_apply_ofFractionRing_mk]

Premises used: Localization.mk_one_eq_algebraMap, RatFunc.liftRingHom_apply_ofFractionRing_mk
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
L : Type u_2
R : Type u_3
inst : Field L
inst_1 : CommRing R
φ : RingHom.{u_3, u_2} R[X] L
hφ : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ L⁰)
x : R[X]
⊢ HDiv.hDiv (α := L) (β := L) ((φ : (a : R[X]) → L) x : L) ((φ : (a : R[X]) → L) (↑1 : R[X]) : L) =
    (φ : (a : R[X]) → L) x

Tactic:
simp
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
L : Type u_2
R : Type u_3
inst : Field L
inst_1 : CommRing R
inst_2 : Nontrivial R
φ : RingHom.{u_3, u_2} R[X] L
hφ : Function.Injective.{u_3 + 1, u_2 + 1} (α := R[X]) (β := L) (⇑φ : (a : R[X]) → L)
hφ' : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ L⁰)
⊢ Function.Injective.{u_3 + 1, u_2 + 1} (α := R⟮X⟯) (β := L) (⇑(liftRingHom φ hφ') : (a : R⟮X⟯) → L)

Tactic:
liftMonoidWithZeroHom_injective _ hφ

Premises used: nonZeroDivisors_le_comap_nonZeroDivisors_of_injective, RatFunc.liftMonoidWithZeroHom_injective
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain 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
inst_1 : IsDomain K
⊢ Eq.{u + 1} (α := K⟮X⟯) 0⁻¹ 0

Tactic:
frac_tac
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
R : Type u_1
inst_2 : CommSemiring R
inst_3 : Algebra.{u_1, u} R K[X]
⊢ Eq.{u + 1} (α := K⟮X⟯) (RatFunc.mk ((algebraMap R K[X] : (a : R) → K[X]) 1) 1) 1

Tactic:
simp only [mk_one', map_one, ofFractionRing_one]

Premises used: RatFunc.ofFractionRing_one, map_one, RatFunc.mk_one'
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
R : Type u_1
inst_2 : CommSemiring R
inst_3 : Algebra.{u_1, u} R K[X]
x y : R
⊢ RatFunc.mk ((algebraMap R K[X] : (a : R) → K[X]) (x * y)) 1 =
    HMul.hMul (α := K⟮X⟯) (RatFunc.mk ((algebraMap R K[X] : (a : R) → K[X]) x) 1)
      (RatFunc.mk ((algebraMap R K[X] : (a : R) → K[X]) y) 1)

Tactic:
simp only [mk_one', map_mul, ofFractionRing_mul]

Premises used: map_mul, RatFunc.mk_one', RatFunc.ofFractionRing_mul
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
R : Type u_1
inst_2 : CommSemiring R
inst_3 : Algebra.{u_1, u} R K[X]
⊢ Eq.{u + 1} (α := K⟮X⟯) (RatFunc.mk ((algebraMap R K[X] : (a : R) → K[X]) 0) 1) 0

Tactic:
simp only [mk_one', map_zero, ofFractionRing_zero]

Premises used: RatFunc.ofFractionRing_zero, map_zero, RatFunc.mk_one'
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
R : Type u_1
inst_2 : CommSemiring R
inst_3 : Algebra.{u_1, u} R K[X]
x y : R
⊢ RatFunc.mk ((algebraMap R K[X] : (a : R) → K[X]) (x + y)) 1 =
    HAdd.hAdd (α := K⟮X⟯) (RatFunc.mk ((algebraMap R K[X] : (a : R) → K[X]) x) 1)
      (RatFunc.mk ((algebraMap R K[X] : (a : R) → K[X]) y) 1)

Tactic:
simp only [mk_one', map_add, ofFractionRing_add]

Premises used: RatFunc.ofFractionRing_add, map_add, RatFunc.mk_one'
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
R : Type u_1
inst_2 : CommSemiring R
inst_3 : Algebra.{u_1, u} R K[X]
c : R
x : K⟮X⟯
_pq :
  ∀ (p q : K[X]) (hq : q ≠ 0),
    c • RatFunc.mk p q =
      HMul.hMul (α := K⟮X⟯)
        ((({ toFun := fun (x : R) ↦ RatFunc.mk ((algebraMap R K[X] : (a : R) → K[X]) x) 1, map_one' := ⋯, map_mul' := ⋯,
                  map_zero' := ⋯, map_add' := ⋯ } :
                RingHom.{u_1, u} R K⟮X⟯) :
              (a : R) → K⟮X⟯)
            c :
          K⟮X⟯)
        (RatFunc.mk p q)
⊢ c • x =
    HMul.hMul (α := K⟮X⟯)
      ((({ toFun := fun (x : R) ↦ RatFunc.mk ((algebraMap R K[X] : (a : R) → K[X]) x) 1, map_one' := ⋯, map_mul' := ⋯,
                map_zero' := ⋯, map_add' := ⋯ } :
              RingHom.{u_1, u} R K⟮X⟯) :
            (a : R) → K⟮X⟯)
          c :
        K⟮X⟯)
      x

Tactic:
induction x using RatFunc.induction_on' with | _ p q hq
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
x : K[X]
⊢ RatFunc.mk x 1 = (algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x

Tactic:
rfl

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

Tactic:
rw [← mk_one, mk_one']

Premises used: RatFunc.mk_one, RatFunc.mk_one'
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
R : Type u_1
inst_2 : CommSemiring R
inst_3 : Algebra.{u_1, u} R K[X]
r : R
rw :
  Eq.{u + 1} (α := FractionRing K[X])
    (toFractionRing
      {
        toFractionRing :=
          (algebraMap K[X] (FractionRing K[X]) : (a : K[X]) → FractionRing K[X])
            ((algebraMap R K[X] : (a : R) → K[X]) r) })
    ((algebraMap R (FractionRing K[X]) : (a : R) → FractionRing K[X]) r)
⊢ Eq.{u + 1} (α := FractionRing K[X]) (toFractionRing (RatFunc.mk ((algebraMap R K[X] : (a : R) → K[X]) r) 1))
    ((algebraMap R (FractionRing K[X]) : (a : R) → FractionRing K[X]) r)

Tactic:
rw [mk_one']

Premises used: RatFunc.mk_one'