awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
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⟯)
⊢ 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⟯)
have 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⟯)
Tactic: rw [← mk_eq_div, mk_smul, mk_eq_div]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
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⟯)
⊢ 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⟯)
have 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⟯)
Tactic: rw [← mk_eq_div, mk_smul, mk_eq_div]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
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
⊢ (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⟯)
have 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⟯)
Tactic: rw [← mk_eq_div]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (hypothesis)
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
⊢ (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⟯)
have hq' : 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))
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
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]
⊢ (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⟯)
have 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⟯)
Tactic: rcases eq_or_ne q 0 with (rfl | hq)
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
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⟯)
⊢ (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⟯)
have 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⟯)
Tactic: rcases eq_or_ne q 0 with (rfl | hq)
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (hypothesis)
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]
⊢ (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⟯)
have 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)
Tactic: have : (0 : K⟮X⟯) = algebraMap K[X] _ 0 / algebraMap K[X] _ 1 := by simp
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
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)
⊢ (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⟯)
have inl : Ne.{u + 1} (α := K[X]) 1 0
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]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
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]
⊢ (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)
have 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)
Tactic: rcases eq_or_ne q 0 with (rfl | hq)
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
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)
⊢ (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)
have 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)
Tactic: rcases eq_or_ne q 0 with (rfl | hq)
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
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]
⊢ 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)
have 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)
Tactic: rw [← map_div₀, liftMonoidWithZeroHom_apply_div]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
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)
⊢ 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)
have 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)
Tactic: rw [← map_div₀, liftMonoidWithZeroHom_apply_div]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
⊢ Function.Injective.{u + 1, u + 1} (α := K[X]) (β := K⟮X⟯) (⇑(algebraMap K[X] K⟮X⟯) : (a : K[X]) → K⟮X⟯)
have rw : Function.Injective.{u + 1, u + 1} (α := K[X]) (β := K⟮X⟯)
  (ofFractionRing ∘ (⇑(algebraMap K[X] (FractionRing K[X])) : (a : K[X]) → FractionRing K[X]))
Tactic: rw [← ofFractionRing_comp_algebraMap]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
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
⊢ (↑(↑(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
have 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⟯)
Tactic: simp_rw [RingHom.toFun_eq_coe, coe_mapRingHom_eq_coe_map, algebraMap_apply r, map_apply_div,
        map_one, AlgHom.commutes]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
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⟯)
⊢ (↑(↑(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
have 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⟯)
Tactic: simp_rw [RingHom.toFun_eq_coe, coe_mapRingHom_eq_coe_map, algebraMap_apply r, map_apply_div,
        map_one, AlgHom.commutes]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
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⟯)
⊢ (↑(↑(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
have 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⟯)
Tactic: simp_rw [RingHom.toFun_eq_coe, coe_mapRingHom_eq_coe_map, algebraMap_apply r, map_apply_div,
        map_one, AlgHom.commutes]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
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⟯)
⊢ (↑(↑(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
have 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⟯)
Tactic: simp_rw [RingHom.toFun_eq_coe, coe_mapRingHom_eq_coe_map, algebraMap_apply r, map_apply_div,
        map_one, AlgHom.commutes]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
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⟯)
⊢ (↑(↑(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
have 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⟯)
Tactic: simp_rw [RingHom.toFun_eq_coe, coe_mapRingHom_eq_coe_map, algebraMap_apply r, map_apply_div,
        map_one, AlgHom.commutes]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
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]
φ : AlgHom.{u_3, u, u_1} S K[X] L
hφ : LE.le (α := Submonoid K[X]) K[X]⁰ (Submonoid.comap φ L⁰)
r : S
⊢ (↑(↑(liftRingHom φ.toRingHom hφ) : K⟮X⟯ →* L) : OneHom K⟮X⟯ L).toFun ((algebraMap S K⟮X⟯ : (a : S) → K⟮X⟯) r) =
    (algebraMap S L : (a : S) → L) r
have simp_rw : Eq.{u_1 + 1} (α := L)
  ((liftRingHom φ.toRingHom hφ : (a : K⟮X⟯) → L) ((algebraMap S K⟮X⟯ : (a : S) → K⟮X⟯) r : K⟮X⟯) : L)
  ((algebraMap S L : (a : S) → L) r : L)
Tactic: simp_rw [RingHom.toFun_eq_coe, AlgHom.toRingHom_eq_coe, algebraMap_apply r,
        liftRingHom_apply_div, AlgHom.coe_toRingHom, map_one, div_one, AlgHom.commutes]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
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]
φ : AlgHom.{u_3, u, u_1} S K[X] L
hφ : LE.le (α := Submonoid K[X]) K[X]⁰ (Submonoid.comap φ L⁰)
r : S
simp_rw :
  Eq.{u_1 + 1} (α := L)
    ((liftRingHom φ.toRingHom hφ : (a : K⟮X⟯) → L) ((algebraMap S K⟮X⟯ : (a : S) → K⟮X⟯) r : K⟮X⟯) : L)
    ((algebraMap S L : (a : S) → L) r : L)
⊢ (↑(↑(liftRingHom φ.toRingHom hφ) : K⟮X⟯ →* L) : OneHom K⟮X⟯ L).toFun ((algebraMap S K⟮X⟯ : (a : S) → K⟮X⟯) r) =
    (algebraMap S L : (a : S) → L) r
have simp_rw₁ : Eq.{u_1 + 1} (α := L)
  ((liftRingHom (↑φ : K[X] →+* L) sorry : (a : K⟮X⟯) → L) ((algebraMap S K⟮X⟯ : (a : S) → K⟮X⟯) r : K⟮X⟯) : L)
  ((algebraMap S L : (a : S) → L) r : L)
Tactic: simp_rw [RingHom.toFun_eq_coe, AlgHom.toRingHom_eq_coe, algebraMap_apply r,
        liftRingHom_apply_div, AlgHom.coe_toRingHom, map_one, div_one, AlgHom.commutes]