awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ 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)

Tactic:
rfl
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
p q : K[X]
⊢ RatFunc.mk p q =
    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⟯) q : K⟮X⟯)

Tactic:
simp only [mk_eq_div', ofFractionRing_div, ofFractionRing_algebraMap]

Premises used: RatFunc.mk_eq_div', RatFunc.ofFractionRing_div, RatFunc.ofFractionRing_algebraMap
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
R : Type u_1
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]
rw :
  RatFunc.mk (c • p) q =
    c •
      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⟯) q : K⟮X⟯)
rw₁ :
  c • RatFunc.mk p q =
    c •
      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⟯) q : K⟮X⟯)
rw₂ rw₃ :
  c •
      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⟯) q : K⟮X⟯) =
    c •
      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⟯) q : K⟮X⟯)
⊢ HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (c • p) : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯) =
    c •
      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⟯) q : K⟮X⟯)

Tactic:
rw [← mk_eq_div, mk_smul, mk_eq_div]

Premises used: RatFunc.mk_smul, RatFunc.mk_eq_div
-- 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 : R
rw :
  Eq.{u + 1} (α := K⟮X⟯) ((algebraMap R K⟮X⟯ : (a : R) → K⟮X⟯) x : K⟮X⟯)
    (RatFunc.mk ((algebraMap R K[X] : (a : R) → K[X]) x) 1 : K⟮X⟯)
⊢ (algebraMap R K⟮X⟯ : (a : R) → K⟮X⟯) x =
    HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((algebraMap R K[X] : (a : R) → K[X]) x) : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) 1 : K⟮X⟯)

Tactic:
rw [← mk_eq_div]

Premises used: RatFunc.mk_eq_div
-- 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 : R
⊢ Eq.{u + 1} (α := K⟮X⟯) ((algebraMap R K⟮X⟯ : (a : R) → K⟮X⟯) x : K⟮X⟯)
    (RatFunc.mk ((algebraMap R K[X] : (a : R) → K[X]) x) 1 : K⟮X⟯)

Tactic:
rfl
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
R : Type u_1
F : Type u_2
inst_2 : CommRing R
inst_3 : IsDomain R
inst_4 : FunLike.{u_2 + 1, u + 1, u_1 + 1} F K[X] R[X]
inst_5 : MonoidHomClass.{u_2, u, u_1} F K[X] R[X]
φ : F
hφ : LE.le (α := Submonoid K[X]) K[X]⁰ (Submonoid.comap φ R[X]⁰)
p q : K[X]
hq : q ≠ 0
⊢ Ne.{u_1 + 1} (α := R[X]) ((φ : (a : K[X]) → R[X]) q : R[X]) (0 : R[X])

Tactic:
have hq' : φ q ≠ 0 := nonZeroDivisors.ne_zero (hφ (mem_nonZeroDivisors_iff_ne_zero.mpr hq))
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
R : Type u_1
F : Type u_2
inst_2 : CommRing R
inst_3 : IsDomain R
inst_4 : FunLike.{u_2 + 1, u + 1, u_1 + 1} F K[X] R[X]
inst_5 : MonoidHomClass.{u_2, u, u_1} F K[X] R[X]
φ : F
hφ : LE.le (α := Submonoid K[X]) K[X]⁰ (Submonoid.comap φ R[X]⁰)
p q : K[X]
hq : q ≠ 0
hq' : Ne.{u_1 + 1} (α := R[X]) ((φ : (a : K[X]) → R[X]) q : R[X]) (0 : R[X])
⊢ (map φ hφ : (a : K⟮X⟯) → R⟮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⟯) q : K⟮X⟯)) =
    HDiv.hDiv (α := R⟮X⟯) (β := R⟮X⟯) ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((φ : (a : K[X]) → R[X]) p) : R⟮X⟯)
      ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((φ : (a : K[X]) → R[X]) q) : R⟮X⟯)

Tactic:
simp only [← mk_eq_div, mk_eq_localization_mk _ hq, map_apply_ofFractionRing_mk,
    mk_eq_localization_mk _ hq']

Premises used: RatFunc.map_apply_ofFractionRing_mk, RatFunc.mk_eq_localization_mk, RatFunc.mk_eq_div
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
R : Type u_1
F : Type u_2
inst_2 : CommRing R
inst_3 : IsDomain R
inst_4 : FunLike.{u_2 + 1, u + 1, u_1 + 1} F K[X] R[X]
inst_5 : MonoidWithZeroHomClass.{u_2, u, u_1} F K[X] R[X]
φ : F
hφ : LE.le (α := Submonoid K[X]) K[X]⁰ (Submonoid.comap φ R[X]⁰)
p q : K[X]
inl :
  (map φ hφ : (a : K⟮X⟯) → R⟮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⟯) 0 : K⟮X⟯)) =
    HDiv.hDiv (α := R⟮X⟯) (β := R⟮X⟯) ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((φ : (a : K[X]) → R[X]) p) : R⟮X⟯)
      ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((φ : (a : K[X]) → R[X]) 0) : R⟮X⟯)
inr :
  ∀ (hq : q ≠ 0),
    (map φ hφ : (a : K⟮X⟯) → R⟮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⟯) q : K⟮X⟯)) =
      HDiv.hDiv (α := R⟮X⟯) (β := R⟮X⟯) ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((φ : (a : K[X]) → R[X]) p) : R⟮X⟯)
        ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((φ : (a : K[X]) → R[X]) q) : R⟮X⟯)
⊢ (map φ hφ : (a : K⟮X⟯) → R⟮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⟯) q : K⟮X⟯)) =
    HDiv.hDiv (α := R⟮X⟯) (β := R⟮X⟯) ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((φ : (a : K[X]) → R[X]) p) : R⟮X⟯)
      ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((φ : (a : K[X]) → R[X]) q) : R⟮X⟯)

Tactic:
rcases eq_or_ne q 0 with (rfl | hq)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
R : Type u_1
F : Type u_2
inst_2 : CommRing R
inst_3 : IsDomain R
inst_4 : FunLike.{u_2 + 1, u + 1, u_1 + 1} F K[X] R[X]
inst_5 : MonoidWithZeroHomClass.{u_2, u, u_1} F K[X] R[X]
φ : F
hφ : LE.le (α := Submonoid K[X]) K[X]⁰ (Submonoid.comap φ R[X]⁰)
p : K[X]
⊢ 0 =
    HDiv.hDiv (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) 0) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) 1)

Tactic:
simp
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
R : Type u_1
F : Type u_2
inst_2 : CommRing R
inst_3 : IsDomain R
inst_4 : FunLike.{u_2 + 1, u + 1, u_1 + 1} F K[X] R[X]
inst_5 : MonoidWithZeroHomClass.{u_2, u, u_1} F K[X] R[X]
φ : F
hφ : LE.le (α := Submonoid K[X]) K[X]⁰ (Submonoid.comap φ R[X]⁰)
p : K[X]
⊢ 0 =
    HDiv.hDiv (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) 0) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) 1)

Tactic:
have : (0 : K⟮X⟯) = algebraMap K[X] _ 0 / algebraMap K[X] _ 1 := by simp
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
R : Type u_1
F : Type u_2
inst_2 : CommRing R
inst_3 : IsDomain R
inst_4 : FunLike.{u_2 + 1, u + 1, u_1 + 1} F K[X] R[X]
inst_5 : MonoidWithZeroHomClass.{u_2, u, u_1} F K[X] R[X]
φ : F
hφ : LE.le (α := Submonoid K[X]) K[X]⁰ (Submonoid.comap φ R[X]⁰)
p : K[X]
this :
  0 =
    HDiv.hDiv (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) 0) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) 1)
inl : Ne.{u + 1} (α := K[X]) 1 0
⊢ (map φ hφ : (a : K⟮X⟯) → R⟮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⟯) 0 : K⟮X⟯)) =
    HDiv.hDiv (α := R⟮X⟯) (β := R⟮X⟯) ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((φ : (a : K[X]) → R[X]) p) : R⟮X⟯)
      ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((φ : (a : K[X]) → R[X]) 0) : R⟮X⟯)

Tactic:
rw [map_zero, map_zero, map_zero, div_zero, div_zero, this, map_apply_div_ne_zero, map_one,
      map_one, div_one, map_zero, map_zero]

Premises used: map_zero, map_one, div_one, div_zero, RatFunc.map_apply_div_ne_zero
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
R : Type u_1
F : Type u_2
inst_2 : CommRing R
inst_3 : IsDomain R
inst_4 : FunLike.{u_2 + 1, u + 1, u_1 + 1} F K[X] R[X]
inst_5 : MonoidWithZeroHomClass.{u_2, u, u_1} F K[X] R[X]
φ : F
hφ : LE.le (α := Submonoid K[X]) K[X]⁰ (Submonoid.comap φ R[X]⁰)
p : K[X]
this :
  0 =
    HDiv.hDiv (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) 0) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) 1)
⊢ Ne.{u + 1} (α := K[X]) 1 0

Tactic:
one_ne_zero

Premises used: one_ne_zero
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
R : Type u_1
F : Type u_2
inst_2 : CommRing R
inst_3 : IsDomain R
inst_4 : FunLike.{u_2 + 1, u + 1, u_1 + 1} F K[X] R[X]
inst_5 : MonoidWithZeroHomClass.{u_2, u, u_1} F K[X] R[X]
φ : F
hφ : LE.le (α := Submonoid K[X]) K[X]⁰ (Submonoid.comap φ R[X]⁰)
p : K[X]
this :
  0 =
    HDiv.hDiv (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) 0) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) 1)
⊢ Ne.{u + 1} (α := K[X]) 1 0

Tactic:
exact one_ne_zero

Premises used: one_ne_zero
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
R : Type u_1
F : Type u_2
inst_2 : CommRing R
inst_3 : IsDomain R
inst_4 : FunLike.{u_2 + 1, u + 1, u_1 + 1} F K[X] R[X]
inst_5 : MonoidWithZeroHomClass.{u_2, u, u_1} F K[X] R[X]
φ : F
hφ : LE.le (α := Submonoid K[X]) K[X]⁰ (Submonoid.comap φ R[X]⁰)
p q : K[X]
hq : q ≠ 0
⊢ (map φ hφ : (a : K⟮X⟯) → R⟮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⟯) q : K⟮X⟯)) =
    HDiv.hDiv (α := R⟮X⟯) (β := R⟮X⟯) ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((φ : (a : K[X]) → R[X]) p) : R⟮X⟯)
      ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((φ : (a : K[X]) → R[X]) q) : R⟮X⟯)

Tactic:
map_apply_div_ne_zero _ _ _ _ hq

Premises used: RatFunc.map_apply_div_ne_zero
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
R : Type u_1
F : Type u_2
inst_2 : CommRing R
inst_3 : IsDomain R
inst_4 : FunLike.{u_2 + 1, u + 1, u_1 + 1} F K[X] R[X]
inst_5 : MonoidWithZeroHomClass.{u_2, u, u_1} F K[X] R[X]
φ : F
hφ : LE.le (α := Submonoid K[X]) K[X]⁰ (Submonoid.comap φ R[X]⁰)
p q : K[X]
hq : q ≠ 0
⊢ (map φ hφ : (a : K⟮X⟯) → R⟮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⟯) q : K⟮X⟯)) =
    HDiv.hDiv (α := R⟮X⟯) (β := R⟮X⟯) ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((φ : (a : K[X]) → R[X]) p) : R⟮X⟯)
      ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((φ : (a : K[X]) → R[X]) q) : R⟮X⟯)

Tactic:
exact map_apply_div_ne_zero _ _ _ _ hq

Premises used: RatFunc.map_apply_div_ne_zero
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
L : Type u_1
inst_2 : CommGroupWithZero L
φ : MonoidWithZeroHom.{u, u_1} K[X] L
hφ : LE.le (α := Submonoid K[X]) K[X]⁰ (Submonoid.comap φ L⁰)
p q : K[X]
inl :
  (liftMonoidWithZeroHom φ hφ : (a : K⟮X⟯) → L)
      (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⟯) 0 : K⟮X⟯)) =
    HDiv.hDiv (α := L) (β := L) ((φ : (a : K[X]) → L) p : L) ((φ : (a : K[X]) → L) 0 : L)
inr :
  ∀ (hq : q ≠ 0),
    (liftMonoidWithZeroHom φ hφ : (a : K⟮X⟯) → L)
        (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⟯) q : K⟮X⟯)) =
      HDiv.hDiv (α := L) (β := L) ((φ : (a : K[X]) → L) p : L) ((φ : (a : K[X]) → L) q : L)
⊢ (liftMonoidWithZeroHom φ hφ : (a : K⟮X⟯) → L)
      (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⟯) q : K⟮X⟯)) =
    HDiv.hDiv (α := L) (β := L) ((φ : (a : K[X]) → L) p : L) ((φ : (a : K[X]) → L) q : L)

Tactic:
rcases eq_or_ne q 0 with (rfl | hq)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
L : Type u_1
inst_2 : CommGroupWithZero L
φ : MonoidWithZeroHom.{u, u_1} K[X] L
hφ : LE.le (α := Submonoid K[X]) K[X]⁰ (Submonoid.comap φ L⁰)
p : K[X]
⊢ (liftMonoidWithZeroHom φ hφ : (a : K⟮X⟯) → L)
      (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⟯) 0 : K⟮X⟯)) =
    HDiv.hDiv (α := L) (β := L) ((φ : (a : K[X]) → L) p : L) ((φ : (a : K[X]) → L) 0 : L)

Tactic:
simp only [div_zero, map_zero]

Premises used: map_zero, div_zero
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
L : Type u_1
inst_2 : CommGroupWithZero L
φ : MonoidWithZeroHom.{u, u_1} K[X] L
hφ : LE.le (α := Submonoid K[X]) K[X]⁰ (Submonoid.comap φ L⁰)
p q : K[X]
hq : q ≠ 0
⊢ (liftMonoidWithZeroHom φ hφ : (a : K⟮X⟯) → L)
      (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⟯) q : K⟮X⟯)) =
    HDiv.hDiv (α := L) (β := L) ((φ : (a : K[X]) → L) p : L) ((φ : (a : K[X]) → L) q : L)

Tactic:
simp only [← mk_eq_div, mk_eq_localization_mk _ hq,
    liftMonoidWithZeroHom_apply_ofFractionRing_mk]

Premises used: RatFunc.liftMonoidWithZeroHom_apply_ofFractionRing_mk, RatFunc.mk_eq_localization_mk, RatFunc.mk_eq_div
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
L : Type u_1
inst_2 : CommGroupWithZero L
φ : MonoidWithZeroHom.{u, u_1} K[X] L
hφ : LE.le (α := Submonoid K[X]) K[X]⁰ (Submonoid.comap φ L⁰)
p q : 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⟯) p : K⟮X⟯)
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯)) =
    HDiv.hDiv (α := L) (β := L) ((φ : (a : K[X]) → L) p : L) ((φ : (a : K[X]) → L) q : L)
rw₁ rw₂ :
  HDiv.hDiv (α := L) (β := L) ((φ : (a : K[X]) → L) p : L) ((φ : (a : K[X]) → L) q : L) =
    HDiv.hDiv (α := L) (β := L) ((φ : (a : K[X]) → L) p : L) ((φ : (a : K[X]) → L) q : L)
⊢ HDiv.hDiv (α := L) (β := L)
      ((liftMonoidWithZeroHom φ hφ : (a : K⟮X⟯) → L) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p : K⟮X⟯) : L)
      ((liftMonoidWithZeroHom φ hφ : (a : K⟮X⟯) → L) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯) : L) =
    HDiv.hDiv (α := L) (β := L) ((φ : (a : K[X]) → L) p : L) ((φ : (a : K[X]) → L) q : L)

Tactic:
rw [← map_div₀, liftMonoidWithZeroHom_apply_div]

Premises used: RatFunc.liftMonoidWithZeroHom_apply_div, map_div₀
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
L : Type u_1
inst_2 : Field L
φ : RingHom.{u, u_1} K[X] L
hφ : LE.le (α := Submonoid K[X]) K[X]⁰ (Submonoid.comap φ L⁰)
p q : K[X]
⊢ (liftRingHom φ hφ : (a : K⟮X⟯) → L)
      (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⟯) q : K⟮X⟯)) =
    HDiv.hDiv (α := L) (β := L) ((φ : (a : K[X]) → L) p : L) ((φ : (a : K[X]) → L) q : L)

Tactic:
liftMonoidWithZeroHom_apply_div _ hφ _ _

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

Tactic:
liftMonoidWithZeroHom_apply_div' _ hφ _ _

Premises used: RatFunc.liftMonoidWithZeroHom_apply_div'
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
L : Type u_1
inst_2 : Field L
φ : RingHom.{u, u_1} K[X] L
hφ : LE.le (α := Submonoid K[X]) K[X]⁰ (Submonoid.comap φ L⁰)
x : K[X]
⊢ Eq.{u_1 + 1} (α := L) ((liftRingHom φ hφ : (a : K⟮X⟯) → L) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x : K⟮X⟯) : L)
    ((φ : (a : K[X]) → L) x : L)

Tactic:
simpa using liftRingHom_apply_div' φ hφ x 1

Premises used: RatFunc.liftRingHom_apply_div', OfNat.ofNat
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
L : Type u_1
inst_2 : Field L
φ : RingHom.{u, u_1} K[X] L
hφ : LE.le (α := Submonoid K[X]) K[X]⁰ (Submonoid.comap φ L⁰)
⊢ (liftRingHom φ hφ).comp (algebraMap K[X] K⟮X⟯) = φ

Tactic:
RingHom.ext fun _ ↦ liftRingHom_algebraMap _ hφ _

Premises used: RingHom.ext, RatFunc.liftRingHom_algebraMap
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
⊢ Eq.{u + 1} (α := K[X] → K⟮X⟯)
    (ofFractionRing ∘ (⇑(algebraMap K[X] (FractionRing K[X])) : (a : K[X]) → FractionRing K[X]))
    (⇑(algebraMap K[X] K⟮X⟯) : (a : K[X]) → K⟮X⟯)

Tactic:
funext ofFractionRing_algebraMap

Premises used: funext, RatFunc.ofFractionRing_algebraMap
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
rw :
  Function.Injective.{u + 1, u + 1} (α := K[X]) (β := K⟮X⟯)
    (ofFractionRing ∘ (⇑(algebraMap K[X] (FractionRing K[X])) : (a : K[X]) → FractionRing K[X]))
⊢ Function.Injective.{u + 1, u + 1} (α := K[X]) (β := K⟮X⟯) (⇑(algebraMap K[X] K⟮X⟯) : (a : K[X]) → K⟮X⟯)

Tactic:
rw [← ofFractionRing_comp_algebraMap]

Premises used: RatFunc.ofFractionRing_comp_algebraMap
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
⊢ Function.Injective.{u + 1, u + 1} (α := K[X]) (β := K⟮X⟯)
    (ofFractionRing ∘ (⇑(algebraMap K[X] (FractionRing K[X])) : (a : K[X]) → FractionRing K[X]))

Tactic:
ofFractionRing_injective.comp (IsFractionRing.injective _ _)

Premises used: IsFractionRing.injective, RatFunc.ofFractionRing_injective, Function.Injective.comp
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
⊢ Function.Injective.{u + 1, u + 1} (α := K[X]) (β := K⟮X⟯)
    (ofFractionRing ∘ (⇑(algebraMap K[X] (FractionRing K[X])) : (a : K[X]) → FractionRing K[X]))

Tactic:
exact ofFractionRing_injective.comp (IsFractionRing.injective _ _)

Premises used: IsFractionRing.injective, RatFunc.ofFractionRing_injective, Function.Injective.comp
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
L : Type u_1
R : Type u_2
S : Type u_3
inst_2 : Field L
inst_3 : CommRing R
inst_4 : IsDomain R
inst_5 : CommSemiring S
inst_6 : Algebra.{u_3, u} S K[X]
inst_7 : Algebra S L
inst_8 : Algebra.{u_3, u_2} S R[X]
φ_1 : AlgHom.{u_3, u, u_1} S K[X] L
hφ_1 : LE.le (α := Submonoid K[X]) K[X]⁰ (Submonoid.comap φ_1 L⁰)
φ : AlgHom.{u_3, u, u_2} S K[X] R[X]
hφ : LE.le (α := Submonoid K[X]) K[X]⁰ (Submonoid.comap φ R[X]⁰)
r : S
simp_rw :
  Eq.{u_2 + 1} (α := R⟮X⟯) ((mapRingHom φ hφ : (a : K⟮X⟯) → R⟮X⟯) ((algebraMap S K⟮X⟯ : (a : S) → K⟮X⟯) r) : R⟮X⟯)
    ((algebraMap S R⟮X⟯ : (a : S) → R⟮X⟯) r : R⟮X⟯)
simp_rw₁ :
  Eq.{u_2 + 1} (α := R⟮X⟯) ((map φ hφ : (a : K⟮X⟯) → R⟮X⟯) ((algebraMap S K⟮X⟯ : (a : S) → K⟮X⟯) r) : R⟮X⟯)
    ((algebraMap S R⟮X⟯ : (a : S) → R⟮X⟯) r : R⟮X⟯)
simp_rw₂ :
  (map φ hφ : (a : K⟮X⟯) → R⟮X⟯)
      (HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯)
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((algebraMap S K[X] : (a : S) → K[X]) r) : K⟮X⟯)
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) 1 : K⟮X⟯)) =
    HDiv.hDiv (α := R⟮X⟯) (β := R⟮X⟯)
      ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((algebraMap S R[X] : (a : S) → R[X]) r) : R⟮X⟯)
      ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) 1 : R⟮X⟯)
simp_rw₃ :
  HDiv.hDiv (α := R⟮X⟯) (β := R⟮X⟯)
      ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((φ : (a : K[X]) → R[X]) ((algebraMap S K[X] : (a : S) → K[X]) r)) :
        R⟮X⟯)
      ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((φ : (a : K[X]) → R[X]) 1) : R⟮X⟯) =
    HDiv.hDiv (α := R⟮X⟯) (β := R⟮X⟯)
      ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((algebraMap S R[X] : (a : S) → R[X]) r) : R⟮X⟯)
      ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) 1 : R⟮X⟯)
simp_rw₄ :
  HDiv.hDiv (α := R⟮X⟯) (β := R⟮X⟯)
      ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((φ : (a : K[X]) → R[X]) ((algebraMap S K[X] : (a : S) → K[X]) r)) :
        R⟮X⟯)
      (1 : R⟮X⟯) =
    HDiv.hDiv (α := R⟮X⟯) (β := R⟮X⟯)
      ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((algebraMap S R[X] : (a : S) → R[X]) r) : R⟮X⟯) (1 : R⟮X⟯)
⊢ (↑(↑(mapRingHom φ hφ) : K⟮X⟯ →* R⟮X⟯) : OneHom K⟮X⟯ R⟮X⟯).toFun ((algebraMap S K⟮X⟯ : (a : S) → K⟮X⟯) r) =
    (algebraMap S R⟮X⟯ : (a : S) → R⟮X⟯) r

Tactic:
simp_rw [RingHom.toFun_eq_coe, coe_mapRingHom_eq_coe_map, algebraMap_apply r, map_apply_div,
        map_one, AlgHom.commutes]

Premises used: RatFunc.coe_mapRingHom_eq_coe_map, RatFunc.map_apply_div, RingHom.toFun_eq_coe, map_one, AlgHom.commutes, RatFunc.algebraMap_apply
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
R : Type u_2
S : Type u_3
inst_2 : CommRing R
inst_3 : IsDomain R
inst_4 : CommSemiring S
inst_5 : Algebra.{u_3, u} S K[X]
inst_6 : Algebra.{u_3, u_2} S R[X]
φ : AlgHom.{u_3, u, u_2} S K[X] R[X]
hφ : LE.le (α := Submonoid K[X]) K[X]⁰ (Submonoid.comap φ R[X]⁰)
⊢ Eq (α := (a : K⟮X⟯) → R⟮X⟯) (⇑(mapAlgHom φ hφ) : (a : K⟮X⟯) → R⟮X⟯) (⇑(map φ hφ) : (a : K⟮X⟯) → R⟮X⟯)

Tactic:
rfl

Premises used: rfl