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]
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'
⊢ 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])

Tactic:
simpa only [map_mul] using congr_arg φ h

Premises used: congr_arg, map_mul, 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]
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]⁰)
p : R[X]
q : ↥R[X]⁰
p' : R[X]
q' : ↥R[X]⁰
⊢ Membership.mem.{u_4, u_4} (α := S[X]) (γ := Submonoid S[X]) S[X]⁰ ((φ : (a : R[X]) → S[X]) (↑q : R[X]) : S[X])

Tactic:
have hq : φ q ∈ S[X]⁰ := hφ q.prop
-- 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]⁰)
p : R[X]
q : ↥R[X]⁰
p' : R[X]
q' : ↥R[X]⁰
hq : Membership.mem.{u_4, u_4} (α := S[X]) (γ := Submonoid S[X]) S[X]⁰ ((φ : (a : R[X]) → S[X]) (↑q : R[X]) : S[X])
⊢ Membership.mem.{u_4, u_4} (α := S[X]) (γ := Submonoid S[X]) S[X]⁰ ((φ : (a : R[X]) → S[X]) (↑q' : R[X]) : S[X])

Tactic:
have hq' : φ q' ∈ S[X]⁰ := hφ q'.prop
-- 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]⁰)
p : R[X]
q : ↥R[X]⁰
p' : R[X]
q' : ↥R[X]⁰
hq : Membership.mem.{u_4, u_4} (α := S[X]) (γ := Submonoid S[X]) S[X]⁰ ((φ : (a : R[X]) → S[X]) (↑q : R[X]) : S[X])
hq' : Membership.mem.{u_4, u_4} (α := S[X]) (γ := Submonoid S[X]) S[X]⁰ ((φ : (a : R[X]) → S[X]) (↑q' : R[X]) : S[X])
⊢ Membership.mem.{u_4, u_4} (α := S[X]) (γ := Submonoid S[X]) S[X]⁰ ((φ : (a : R[X]) → S[X]) (↑(q * q') : R[X]) : S[X])

Tactic:
simpa using Submonoid.mul_mem _ hq hq'

Premises used: Submonoid.mul_mem
-- 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]⁰)
p : R[X]
q : ↥R[X]⁰
p' : R[X]
q' : ↥R[X]⁰
hq : Membership.mem.{u_4, u_4} (α := S[X]) (γ := Submonoid S[X]) S[X]⁰ ((φ : (a : R[X]) → S[X]) (↑q : R[X]) : S[X])
hq' : Membership.mem.{u_4, u_4} (α := S[X]) (γ := Submonoid S[X]) S[X]⁰ ((φ : (a : R[X]) → S[X]) (↑q' : R[X]) : S[X])
⊢ Membership.mem.{u_4, u_4} (α := S[X]) (γ := Submonoid S[X]) S[X]⁰ ((φ : (a : R[X]) → S[X]) (↑(q * q') : R[X]) : S[X])

Tactic:
have hqq' : φ ↑(q * q') ∈ S[X]⁰ := by simpa using Submonoid.mul_mem _ hq hq'
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
R : Type u_3
S : Type u_4
F : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : FunLike.{u_5 + 1, u_3 + 1, u_4 + 1} F R[X] S[X]
inst_3 : 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]⁰)
n : R[X]
d : ↥R[X]⁰
⊢ Eq.{u_4 + 1} (α := S⟮X⟯) ((map φ hφ : (a : R⟮X⟯) → S⟮X⟯) { toFractionRing := Localization.mk n d } : S⟮X⟯)
    ({
        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 : R[X])) ⋯) } :
      S⟮X⟯)

Tactic:
simp only [map, MonoidHom.coe_mk, OneHom.coe_mk, liftOn_ofFractionRing_mk,
    Submonoid.mem_comap.mp (hφ d.2), ↓reduceDIte]

Premises used: RatFunc.liftOn_ofFractionRing_mk, OneHom.coe_mk, Submonoid.mem_comap, reduceDIte, MonoidHom.coe_mk, RatFunc.map, Iff.mp, Subtype.property
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
R : Type u_3
S : Type u_4
F : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : FunLike.{u_5 + 1, u_3 + 1, u_4 + 1} F R[X] S[X]
inst_3 : 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]⁰)
hf : Function.Injective.{u_3 + 1, u_4 + 1} (α := R[X]) (β := S[X]) (⇑φ : (a : R[X]) → S[X])
x y : FractionRing R[X]
h :
  Eq.{u_4 + 1} (α := S⟮X⟯) ((map φ hφ : (a : R⟮X⟯) → S⟮X⟯) { toFractionRing := x } : S⟮X⟯)
    ((map φ hφ : (a : R⟮X⟯) → S⟮X⟯) { toFractionRing := y } : S⟮X⟯)
H :
  ∀ (y_1 : R[X] × ↥R[X]⁰)
    (h :
      Eq.{u_4 + 1} (α := S⟮X⟯) ((map φ hφ : (a : R⟮X⟯) → S⟮X⟯) { toFractionRing := Localization.mk y_1.1 y_1.2 } : S⟮X⟯)
        ((map φ hφ : (a : R⟮X⟯) → S⟮X⟯) { toFractionRing := y } : S⟮X⟯)),
    { toFractionRing := Localization.mk y_1.1 y_1.2 : R⟮X⟯ } = { toFractionRing := y }
⊢ { toFractionRing := x : R⟮X⟯ } = { toFractionRing := y }

Tactic:
induction x using Localization.induction_on
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
R : Type u_3
S : Type u_4
F : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : FunLike.{u_5 + 1, u_3 + 1, u_4 + 1} F R[X] S[X]
inst_3 : 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]⁰)
hf : Function.Injective.{u_3 + 1, u_4 + 1} (α := R[X]) (β := S[X]) (⇑φ : (a : R[X]) → S[X])
y : FractionRing R[X]
y_1 : R[X] × ↥R[X]⁰
h :
  Eq.{u_4 + 1} (α := S⟮X⟯) ((map φ hφ : (a : R⟮X⟯) → S⟮X⟯) { toFractionRing := Localization.mk y_1.1 y_1.2 } : S⟮X⟯)
    ((map φ hφ : (a : R⟮X⟯) → S⟮X⟯) { toFractionRing := y } : S⟮X⟯)
H :
  ∀ (y : R[X] × ↥R[X]⁰)
    (h :
      Eq.{u_4 + 1} (α := S⟮X⟯) ((map φ hφ : (a : R⟮X⟯) → S⟮X⟯) { toFractionRing := Localization.mk y_1.1 y_1.2 } : S⟮X⟯)
        ((map φ hφ : (a : R⟮X⟯) → S⟮X⟯) { toFractionRing := Localization.mk y.1 y.2 } : S⟮X⟯)),
    { toFractionRing := Localization.mk y_1.1 y_1.2 : R⟮X⟯ } = { toFractionRing := Localization.mk y.1 y.2 }
⊢ { toFractionRing := Localization.mk y_1.1 y_1.2 : R⟮X⟯ } = { toFractionRing := y }

Tactic:
induction y using Localization.induction_on
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
R : Type u_3
S : Type u_4
F : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : FunLike.{u_5 + 1, u_3 + 1, u_4 + 1} F R[X] S[X]
inst_3 : 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]⁰)
hf : Function.Injective.{u_3 + 1, u_4 + 1} (α := R[X]) (β := S[X]) (⇑φ : (a : R[X]) → S[X])
y y_1 : R[X] × ↥R[X]⁰
h :
  Eq.{u_4 + 1} (α := S⟮X⟯) ((map φ hφ : (a : R⟮X⟯) → S⟮X⟯) { toFractionRing := Localization.mk y.1 y.2 } : S⟮X⟯)
    ((map φ hφ : (a : R⟮X⟯) → S⟮X⟯) { toFractionRing := Localization.mk y_1.1 y_1.2 } : S⟮X⟯)
⊢ { toFractionRing := Localization.mk y.1 y.2 : R⟮X⟯ } = { toFractionRing := Localization.mk y_1.1 y_1.2 }

Tactic:
simpa only [map_apply_ofFractionRing_mk, ofFractionRing_injective.eq_iff,
    Localization.mk_eq_mk_iff, Localization.r_iff_exists, mul_cancel_left_coe_nonZeroDivisors,
    exists_const, ← map_mul, hf.eq_iff] using h

Premises used: RatFunc.map_apply_ofFractionRing_mk, Function.Injective.eq_iff, RatFunc.ofFractionRing_injective, map_mul, Localization.r_iff_exists, exists_const, mul_cancel_left_coe_nonZeroDivisors, 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 : RingHomClass.{u_5, u_3, u_4} F R[X] S[X]
φ : F
hφ : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ S[X]⁰)
simp_rw : Eq.{u_4 + 1} (α := S⟮X⟯) ((map φ hφ : (a : R⟮X⟯) → S⟮X⟯) 0) 0
simp_rw₁ :
  Eq.{u_4 + 1} (α := S⟮X⟯) ((map φ hφ : (a : R⟮X⟯) → S⟮X⟯) { toFractionRing := 0 } : S⟮X⟯)
    ({ toFractionRing := 0 } : S⟮X⟯)
simp_rw₂ :
  Eq.{u_4 + 1} (α := S⟮X⟯) ((map φ hφ : (a : R⟮X⟯) → S⟮X⟯) { toFractionRing := Localization.mk 0 1 } : S⟮X⟯)
    ({ toFractionRing := 0 } : S⟮X⟯)
simp_rw₃ :
  Eq.{u_4 + 1} (α := S⟮X⟯) ((map φ hφ : (a : R⟮X⟯) → S⟮X⟯) { toFractionRing := Localization.mk 0 1 } : S⟮X⟯)
    ({ toFractionRing := Localization.mk 0 1 } : S⟮X⟯)
simp_rw₄ :
  {
      toFractionRing :=
        Localization.mk ((φ : (a : R[X]) → S[X]) 0)
          (Subtype.mk (p := fun (x : S[X]) ↦ Membership.mem (γ := Submonoid S[X]) S[X]⁰ x)
            ((φ : (a : R[X]) → S[X]) (↑1 : R[X])) ⋯) :
      S⟮X⟯ } =
    { toFractionRing := Localization.mk 0 1 }
simp_rw₅ :
  {
      toFractionRing :=
        Localization.mk 0
          (Subtype.mk (p := fun (x : S[X]) ↦ Membership.mem (γ := Submonoid S[X]) S[X]⁰ x)
            ((φ : (a : R[X]) → S[X]) (↑1 : R[X])) ⋯) :
      S⟮X⟯ } =
    { toFractionRing := Localization.mk 0 1 }
simp_rw₆ :
  Eq (α := S⟮X⟯)
    ({
        toFractionRing :=
          IsLocalization.mk' (Localization (M := S[X]) S[X]⁰) 0
            (Subtype.mk (p := fun (x : S[X]) ↦ Membership.mem (γ := Submonoid S[X]) S[X]⁰ x)
              ((φ : (a : R[X]) → S[X]) (↑1 : R[X])) ⋯) } :
      S⟮X⟯)
    ({ toFractionRing := IsLocalization.mk' (R := S[X]) (M := S[X]⁰) (Localization (M := S[X]) S[X]⁰) 0 1 } : S⟮X⟯)
⊢ (↑(map φ hφ) : OneHom R⟮X⟯ S⟮X⟯).toFun 0 = 0

Tactic:
simp_rw [MonoidHom.toFun_eq_coe, ← ofFractionRing_zero, ← Localization.mk_zero (1 : R[X]⁰),
        ← Localization.mk_zero (1 : S[X]⁰), map_apply_ofFractionRing_mk, map_zero,
        Localization.mk_eq_mk', IsLocalization.mk'_zero]

Premises used: Localization.mk_eq_mk', RatFunc.map_apply_ofFractionRing_mk, RatFunc.ofFractionRing_zero, map_zero, MonoidHom.toFun_eq_coe, IsLocalization.mk'_zero, OfNat.ofNat, Localization.mk_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]
inst_6 : RingHomClass.{u_5, u_3, u_4} F R[X] S[X]
φ : F
hφ : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ S[X]⁰)
x y : FractionRing R[X]
H :
  ∀ (y_1 : R[X] × ↥R[X]⁰),
    (↑(map φ hφ) : OneHom R⟮X⟯ S⟮X⟯).toFun
        ({ toFractionRing := Localization.mk y_1.1 y_1.2 : R⟮X⟯ } + { toFractionRing := y : R⟮X⟯ }) =
      (↑(map φ hφ) : OneHom R⟮X⟯ S⟮X⟯).toFun { toFractionRing := Localization.mk y_1.1 y_1.2 : R⟮X⟯ } +
        (↑(map φ hφ) : OneHom R⟮X⟯ S⟮X⟯).toFun { toFractionRing := y : R⟮X⟯ }
⊢ (↑(map φ hφ) : OneHom R⟮X⟯ S⟮X⟯).toFun ({ toFractionRing := x : R⟮X⟯ } + { toFractionRing := y : R⟮X⟯ }) =
    (↑(map φ hφ) : OneHom R⟮X⟯ S⟮X⟯).toFun { toFractionRing := x : R⟮X⟯ } +
      (↑(map φ hφ) : OneHom R⟮X⟯ S⟮X⟯).toFun { toFractionRing := y : R⟮X⟯ }

Tactic:
induction x using Localization.induction_on
-- 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 : RingHomClass.{u_5, u_3, u_4} F R[X] S[X]
φ : F
hφ : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ S[X]⁰)
y : FractionRing R[X]
y_1 : R[X] × ↥R[X]⁰
H :
  ∀ (y : R[X] × ↥R[X]⁰),
    (↑(map φ hφ) : OneHom R⟮X⟯ S⟮X⟯).toFun
        ({ toFractionRing := Localization.mk y_1.1 y_1.2 : R⟮X⟯ } +
          { toFractionRing := Localization.mk y.1 y.2 : R⟮X⟯ }) =
      (↑(map φ hφ) : OneHom R⟮X⟯ S⟮X⟯).toFun { toFractionRing := Localization.mk y_1.1 y_1.2 : R⟮X⟯ } +
        (↑(map φ hφ) : OneHom R⟮X⟯ S⟮X⟯).toFun { toFractionRing := Localization.mk y.1 y.2 : R⟮X⟯ }
⊢ (↑(map φ hφ) : OneHom R⟮X⟯ S⟮X⟯).toFun
      ({ toFractionRing := Localization.mk y_1.1 y_1.2 : R⟮X⟯ } + { toFractionRing := y : R⟮X⟯ }) =
    (↑(map φ hφ) : OneHom R⟮X⟯ S⟮X⟯).toFun { toFractionRing := Localization.mk y_1.1 y_1.2 : R⟮X⟯ } +
      (↑(map φ hφ) : OneHom R⟮X⟯ S⟮X⟯).toFun { toFractionRing := y : R⟮X⟯ }

Tactic:
induction y using Localization.induction_on
-- 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 : RingHomClass.{u_5, u_3, u_4} F R[X] S[X]
φ : F
hφ : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ S[X]⁰)
y y_1 : R[X] × ↥R[X]⁰
⊢ (↑(map φ hφ) : OneHom R⟮X⟯ S⟮X⟯).toFun
      ({ toFractionRing := Localization.mk y.1 y.2 : R⟮X⟯ } +
        { toFractionRing := Localization.mk y_1.1 y_1.2 : R⟮X⟯ }) =
    (↑(map φ hφ) : OneHom R⟮X⟯ S⟮X⟯).toFun { toFractionRing := Localization.mk y.1 y.2 : R⟮X⟯ } +
      (↑(map φ hφ) : OneHom R⟮X⟯ S⟮X⟯).toFun { toFractionRing := Localization.mk y_1.1 y_1.2 : R⟮X⟯ }

Tactic:
simp only [← ofFractionRing_add, Localization.add_mk, map_add, map_mul,
          MonoidHom.toFun_eq_coe, map_apply_ofFractionRing_mk, Submonoid.coe_mul,
          -- We have to specify `S[X]⁰` to `mk_mul_mk`, otherwise it will try to rewrite
          -- the wrong occurrence.
          Submonoid.mk_mul_mk S[X]⁰]

Premises used: RatFunc.map_apply_ofFractionRing_mk, nonZeroDivisors, RatFunc.ofFractionRing_add, MonoidHom.toFun_eq_coe, map_add, Polynomial, Submonoid.mk_mul_mk, map_mul, Localization.add_mk, Submonoid.coe_mul
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
R : Type u_3
S : Type u_4
F : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : FunLike.{u_5 + 1, u_3 + 1, u_4 + 1} F R[X] S[X]
inst_3 : RingHomClass.{u_5, u_3, u_4} F R[X] S[X]
φ : F
hφ : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ S[X]⁰)
⊢ Eq (α := (a : R⟮X⟯) → S⟮X⟯) (⇑(mapRingHom φ hφ) : (a : R⟮X⟯) → S⟮X⟯) (⇑(map φ hφ) : (a : R⟮X⟯) → S⟮X⟯)

Tactic:
rfl

Premises used: rfl
-- 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]
φ : MonoidWithZeroHom.{u_3, u_1} R[X] G₀
hφ : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ G₀⁰)
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'
inl :
  Subsingleton R →
    Eq.{u_1 + 1} (α := G₀)
      ((fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀))
        p q)
      ((fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀))
        p' q')
inr :
  Nontrivial R →
    Eq.{u_1 + 1} (α := G₀)
      ((fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀))
        p q)
      ((fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀))
        p' q')
⊢ Eq.{u_1 + 1} (α := G₀)
    ((fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀)) p
      q)
    ((fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀)) p'
      q')

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]
φ : MonoidWithZeroHom.{u_3, u_1} R[X] G₀
hφ : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ G₀⁰)
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'
h_1 : Subsingleton R
inl :
  Eq.{u_1 + 1} (α := G₀)
    ((fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀)) q
      q)
    ((fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀)) p'
      q')
inl₁ :
  Eq.{u_1 + 1} (α := G₀)
    ((fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀)) q
      q)
    ((fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀)) q
      q')
inl₂ inl₃ :
  Eq.{u_1 + 1} (α := G₀)
    ((fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀)) q
      q)
    ((fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀)) q
      q)
⊢ Eq.{u_1 + 1} (α := G₀)
    ((fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀)) p
      q)
    ((fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀)) p'
      q')

Tactic:
rw [Subsingleton.elim p q, Subsingleton.elim p' q, Subsingleton.elim q' q]

Premises used: Subsingleton.elim
-- 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]
φ : MonoidWithZeroHom.{u_3, u_1} R[X] G₀
hφ : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ G₀⁰)
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'
h_1 : Nontrivial R
inr : Ne.{u_1 + 1} (α := G₀) ((φ : (a : R[X]) → G₀) q : G₀) (0 : G₀)
inr₁ : Ne.{u_1 + 1} (α := G₀) ((φ : (a : R[X]) → G₀) q' : G₀) (0 : G₀)
⊢ Eq.{u_1 + 1} (α := G₀)
    ((fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀)) p
      q)
    ((fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀)) p'
      q')

Tactic:
rw [div_eq_div_iff, ← map_mul, mul_comm p, h, map_mul, mul_comm]

Premises used: div_eq_div_iff, map_mul, mul_comm
-- 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]
φ : MonoidWithZeroHom.{u_3, u_1} R[X] G₀
hφ : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ G₀⁰)
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'
h_1 : Nontrivial R
⊢ Ne.{u_1 + 1} (α := G₀) ((φ : (a : R[X]) → G₀) q : G₀) (0 : G₀)

Tactic:
nonZeroDivisors.ne_zero (hφ ‹_›)

Premises used: 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]
φ : MonoidWithZeroHom.{u_3, u_1} R[X] G₀
hφ : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ G₀⁰)
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'
h_1 : Nontrivial R
⊢ Ne.{u_1 + 1} (α := G₀) ((φ : (a : R[X]) → G₀) q : G₀) (0 : G₀)

Tactic:
exact nonZeroDivisors.ne_zero (hφ ‹_›)

Premises used: 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]
φ : MonoidWithZeroHom.{u_3, u_1} R[X] G₀
hφ : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ G₀⁰)
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'
h_1 : Nontrivial R
⊢ Ne.{u_1 + 1} (α := G₀) ((φ : (a : R[X]) → G₀) q' : G₀) (0 : G₀)

Tactic:
nonZeroDivisors.ne_zero (hφ ‹_›)

Premises used: 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]
φ : MonoidWithZeroHom.{u_3, u_1} R[X] G₀
hφ : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ G₀⁰)
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'
h_1 : Nontrivial R
⊢ Ne.{u_1 + 1} (α := G₀) ((φ : (a : R[X]) → G₀) q' : G₀) (0 : G₀)

Tactic:
exact nonZeroDivisors.ne_zero (hφ ‹_›)

Premises used: 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]
φ : MonoidWithZeroHom.{u_3, u_1} R[X] G₀
hφ : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ G₀⁰)
simp_rw :
  Eq.{u_1 + 1} (α := G₀)
    (RatFunc.liftOn.{u_3, u_1 + 1} (K := R) { toFractionRing := 0 }
      (fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀))
      ⋯)
    0
simp_rw₁ :
  Eq.{u_1 + 1} (α := G₀)
    (RatFunc.liftOn.{u_3, u_1 + 1} (K := R) { toFractionRing := Localization.mk 0 1 }
      (fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀))
      ⋯)
    0
simp_rw₂ : HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) 0 : G₀) ((φ : (a : R[X]) → G₀) (↑1 : R[X]) : G₀) = 0
simp_rw₃ : HDiv.hDiv (α := G₀) (β := G₀) (0 : G₀) ((φ : (a : R[X]) → G₀) (↑1 : R[X]) : G₀) = 0
⊢ Eq.{u_1 + 1} (α := G₀)
    (RatFunc.liftOn.{u_3, u_1 + 1} (K := R) 0
      (fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀))
      ⋯)
    0

Tactic:
simp_rw [← ofFractionRing_zero, ← Localization.mk_zero (1 : R[X]⁰), liftOn_ofFractionRing_mk,
      map_zero, zero_div]

Premises used: RatFunc.liftOn_ofFractionRing_mk, zero_div, RatFunc.ofFractionRing_zero, map_zero, OfNat.ofNat, Localization.mk_zero