awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
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
⊢ 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)
have inr₃ : Ne.{u_2 + 1} (α := L) ((φ : (a : R[X]) → L) (↑q : R[X]) : L) (0 : L)
Tactic: rw [div_add_div, div_eq_div_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
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)
⊢ 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)
have inr₄ : Ne.{u_2 + 1} (α := L) ((φ : (a : R[X]) → L) (↑q' : R[X]) : L) (0 : L)
Tactic: rw [div_add_div, div_eq_div_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
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) ((↑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)
have 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)
Tactic: rw [mul_comm _ p, mul_comm _ p', mul_comm _ (φ p'), add_comm]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
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) (β := L) ((φ : (a : R[X]) → L) (↑q : R[X]) : L) ((φ : (a : R[X]) → L) (↑q' : R[X]) : L) ≠ 0
have inr : Ne.{u_2 + 1} (α := L) ((φ : (a : R[X]) → L) (↑(q * q') : R[X]) : L) (0 : L)
Tactic: simp only [← map_mul, ← Submonoid.coe_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
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) (β := L) ((φ : (a : R[X]) → L) (↑q : R[X]) : L) ((φ : (a : R[X]) → L) (↑q' : R[X]) : L) ≠ 0
have inr : Ne.{u_2 + 1} (α := L) ((φ : (a : R[X]) → L) (↑(q * q') : R[X]) : L) (0 : L)
Tactic: try simp only [← map_mul, ← Submonoid.coe_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
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]
⊢ 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)
have rw : HDiv.hDiv (α := L) (β := L) ((φ : (a : R[X]) → L) x : L) ((φ : (a : R[X]) → L) (↑1 : R[X]) : L) = (φ : (a : R[X]) → L) x
Tactic: rw [← Localization.mk_one_eq_algebraMap, liftRingHom_apply_ofFractionRing_mk]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
⊢ ∀ (a b : K⟮X⟯), a / b = a * b⁻¹
have frac_tac : ∀ (toFractionRing : FractionRing K[X]) (b : K⟮X⟯),
  { toFractionRing := toFractionRing : K⟮X⟯ } / b = { toFractionRing := toFractionRing : K⟮X⟯ } * b⁻¹
Tactic: frac_tac
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
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⁻¹
⊢ ∀ (a b : K⟮X⟯), a / b = a * b⁻¹
have 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⟯ }⁻¹
Tactic: frac_tac
-- 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]
c : R
x : K⟮X⟯
⊢ 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
have _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' := sorry, map_mul' := sorry,
                map_zero' := sorry, map_add' := sorry } :
              RingHom.{u_1, u} R K⟮X⟯) :
            (a : R) → K⟮X⟯)
          c :
        K⟮X⟯)
      (RatFunc.mk p q)
Tactic: induction x using RatFunc.induction_on' with | _ p q hq
Cleared hypotheses: x
-- 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]
c : R
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)
have _pq : 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' := sorry, map_mul' := sorry } :
            MonoidHom.{u_1, u} R K⟮X⟯) :
          (a : R) → K⟮X⟯)
        c :
      K⟮X⟯)
    (RatFunc.mk p q)
Tactic: rw [RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk, mk_one', ← mk_smul,
      mk_def_of_ne (c • p) hq, mk_def_of_ne p hq, ← ofFractionRing_mul,
      IsLocalization.mul_mk'_eq_mk'_of_mul, Algebra.smul_def]
-- 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]
c : R
p q : K[X]
hq : q ≠ 0
_pq :
  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' := ⋯ } :
              MonoidHom.{u_1, u} R K⟮X⟯) :
            (a : R) → K⟮X⟯)
          c :
        K⟮X⟯)
      (RatFunc.mk p q)
⊢ 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)
have _pq₁ : 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' := sorry } :
            OneHom.{u_1, u} R K⟮X⟯) :
          (a : R) → K⟮X⟯)
        c :
      K⟮X⟯)
    (RatFunc.mk p q)
Tactic: rw [RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk, mk_one', ← mk_smul,
      mk_def_of_ne (c • p) hq, mk_def_of_ne p hq, ← ofFractionRing_mul,
      IsLocalization.mul_mk'_eq_mk'_of_mul, Algebra.smul_def]
-- 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]
c : R
p q : K[X]
hq : q ≠ 0
_pq :
  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' := ⋯ } :
              MonoidHom.{u_1, u} R K⟮X⟯) :
            (a : R) → K⟮X⟯)
          c :
        K⟮X⟯)
      (RatFunc.mk p q)
_pq₁ :
  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' := ⋯ } :
              OneHom.{u_1, u} R K⟮X⟯) :
            (a : R) → K⟮X⟯)
          c :
        K⟮X⟯)
      (RatFunc.mk p q)
⊢ 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)
have _pq₂ : c • RatFunc.mk p q = RatFunc.mk ((algebraMap R K[X] : (a : R) → K[X]) c) 1 * RatFunc.mk p q
Tactic: rw [RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk, mk_one', ← mk_smul,
      mk_def_of_ne (c • p) hq, mk_def_of_ne p hq, ← ofFractionRing_mul,
      IsLocalization.mul_mk'_eq_mk'_of_mul, Algebra.smul_def]
-- 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]
c : R
p q : K[X]
hq : q ≠ 0
_pq :
  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' := ⋯ } :
              MonoidHom.{u_1, u} R K⟮X⟯) :
            (a : R) → K⟮X⟯)
          c :
        K⟮X⟯)
      (RatFunc.mk p q)
_pq₁ :
  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' := ⋯ } :
              OneHom.{u_1, u} R K⟮X⟯) :
            (a : R) → K⟮X⟯)
          c :
        K⟮X⟯)
      (RatFunc.mk p q)
_pq₂ : c • RatFunc.mk p q = RatFunc.mk ((algebraMap R K[X] : (a : R) → K[X]) c) 1 * RatFunc.mk p q
⊢ 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)
have _pq₃ : c • RatFunc.mk p q =
  {
      toFractionRing :=
        (algebraMap K[X] (FractionRing K[X]) : (a : K[X]) → FractionRing K[X])
          ((algebraMap R K[X] : (a : R) → K[X]) c) } *
    RatFunc.mk p q
Tactic: rw [RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk, mk_one', ← mk_smul,
      mk_def_of_ne (c • p) hq, mk_def_of_ne p hq, ← ofFractionRing_mul,
      IsLocalization.mul_mk'_eq_mk'_of_mul, Algebra.smul_def]
-- 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]
c : R
p q : K[X]
hq : q ≠ 0
_pq :
  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' := ⋯ } :
              MonoidHom.{u_1, u} R K⟮X⟯) :
            (a : R) → K⟮X⟯)
          c :
        K⟮X⟯)
      (RatFunc.mk p q)
_pq₁ :
  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' := ⋯ } :
              OneHom.{u_1, u} R K⟮X⟯) :
            (a : R) → K⟮X⟯)
          c :
        K⟮X⟯)
      (RatFunc.mk p q)
_pq₂ : c • RatFunc.mk p q = RatFunc.mk ((algebraMap R K[X] : (a : R) → K[X]) c) 1 * RatFunc.mk p q
_pq₃ :
  c • RatFunc.mk p q =
    {
        toFractionRing :=
          (algebraMap K[X] (FractionRing K[X]) : (a : K[X]) → FractionRing K[X])
            ((algebraMap R K[X] : (a : R) → K[X]) c) } *
      RatFunc.mk p q
⊢ 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)
have _pq₄ : RatFunc.mk (c • p) q =
  {
      toFractionRing :=
        (algebraMap K[X] (FractionRing K[X]) : (a : K[X]) → FractionRing K[X])
          ((algebraMap R K[X] : (a : R) → K[X]) c) } *
    RatFunc.mk p q
Tactic: rw [RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk, mk_one', ← mk_smul,
      mk_def_of_ne (c • p) hq, mk_def_of_ne p hq, ← ofFractionRing_mul,
      IsLocalization.mul_mk'_eq_mk'_of_mul, Algebra.smul_def]
-- 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]
c : R
p q : K[X]
hq : q ≠ 0
_pq :
  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' := ⋯ } :
              MonoidHom.{u_1, u} R K⟮X⟯) :
            (a : R) → K⟮X⟯)
          c :
        K⟮X⟯)
      (RatFunc.mk p q)
_pq₁ :
  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' := ⋯ } :
              OneHom.{u_1, u} R K⟮X⟯) :
            (a : R) → K⟮X⟯)
          c :
        K⟮X⟯)
      (RatFunc.mk p q)
_pq₂ : c • RatFunc.mk p q = RatFunc.mk ((algebraMap R K[X] : (a : R) → K[X]) c) 1 * RatFunc.mk p q
_pq₃ :
  c • RatFunc.mk p q =
    {
        toFractionRing :=
          (algebraMap K[X] (FractionRing K[X]) : (a : K[X]) → FractionRing K[X])
            ((algebraMap R K[X] : (a : R) → K[X]) c) } *
      RatFunc.mk p q
_pq₄ :
  RatFunc.mk (c • p) q =
    {
        toFractionRing :=
          (algebraMap K[X] (FractionRing K[X]) : (a : K[X]) → FractionRing K[X])
            ((algebraMap R K[X] : (a : R) → K[X]) c) } *
      RatFunc.mk p q
⊢ 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)
have _pq₅ : {
    toFractionRing :=
      IsLocalization.mk' (FractionRing K[X]) (c • p)
        (Subtype.mk (p := fun (x : K[X]) ↦ Membership.mem (γ := Submonoid K[X]) K[X]⁰ x) q sorry) } =
  {
      toFractionRing :=
        (algebraMap K[X] (FractionRing K[X]) : (a : K[X]) → FractionRing K[X])
          ((algebraMap R K[X] : (a : R) → K[X]) c) :
      K⟮X⟯ } *
    RatFunc.mk p q
Tactic: rw [RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk, mk_one', ← mk_smul,
      mk_def_of_ne (c • p) hq, mk_def_of_ne p hq, ← ofFractionRing_mul,
      IsLocalization.mul_mk'_eq_mk'_of_mul, Algebra.smul_def]
-- 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]
c : R
p q : K[X]
hq : q ≠ 0
_pq :
  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' := ⋯ } :
              MonoidHom.{u_1, u} R K⟮X⟯) :
            (a : R) → K⟮X⟯)
          c :
        K⟮X⟯)
      (RatFunc.mk p q)
_pq₁ :
  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' := ⋯ } :
              OneHom.{u_1, u} R K⟮X⟯) :
            (a : R) → K⟮X⟯)
          c :
        K⟮X⟯)
      (RatFunc.mk p q)
_pq₂ : c • RatFunc.mk p q = RatFunc.mk ((algebraMap R K[X] : (a : R) → K[X]) c) 1 * RatFunc.mk p q
_pq₃ :
  c • RatFunc.mk p q =
    {
        toFractionRing :=
          (algebraMap K[X] (FractionRing K[X]) : (a : K[X]) → FractionRing K[X])
            ((algebraMap R K[X] : (a : R) → K[X]) c) } *
      RatFunc.mk p q
_pq₄ :
  RatFunc.mk (c • p) q =
    {
        toFractionRing :=
          (algebraMap K[X] (FractionRing K[X]) : (a : K[X]) → FractionRing K[X])
            ((algebraMap R K[X] : (a : R) → K[X]) c) } *
      RatFunc.mk p q
_pq₅ :
  {
      toFractionRing :=
        IsLocalization.mk' (FractionRing K[X]) (c • p)
          (Subtype.mk (p := fun (x : K[X]) ↦ Membership.mem (γ := Submonoid K[X]) K[X]⁰ x) q ⋯) } =
    {
        toFractionRing :=
          (algebraMap K[X] (FractionRing K[X]) : (a : K[X]) → FractionRing K[X])
            ((algebraMap R K[X] : (a : R) → K[X]) c) :
        K⟮X⟯ } *
      RatFunc.mk p q
⊢ 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)
have _pq₆ : {
    toFractionRing :=
      IsLocalization.mk' (FractionRing K[X]) (c • p)
        (Subtype.mk (p := fun (x : K[X]) ↦ Membership.mem (γ := Submonoid K[X]) K[X]⁰ x) q sorry) } =
  HMul.hMul (α := K⟮X⟯)
    {
      toFractionRing :=
        (algebraMap K[X] (FractionRing K[X]) : (a : K[X]) → FractionRing K[X])
          ((algebraMap R K[X] : (a : R) → K[X]) c) :
      K⟮X⟯ }
    {
      toFractionRing :=
        IsLocalization.mk' (FractionRing K[X]) p
          (Subtype.mk (p := fun (x : K[X]) ↦ Membership.mem (γ := Submonoid K[X]) K[X]⁰ x) q sorry) :
      K⟮X⟯ }
Tactic: rw [RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk, mk_one', ← mk_smul,
      mk_def_of_ne (c • p) hq, mk_def_of_ne p hq, ← ofFractionRing_mul,
      IsLocalization.mul_mk'_eq_mk'_of_mul, Algebra.smul_def]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
x : K[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)
have rw : { toFractionRing := (algebraMap K[X] (FractionRing K[X]) : (a : K[X]) → FractionRing K[X]) x } = RatFunc.mk x 1
Tactic: rw [← mk_one, mk_one']
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
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
⊢ 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)
have 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 }
Tactic: rw [← mk_one, mk_one']
-- 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]
r : 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)
have 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)
Tactic: rw [mk_one']
-- 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]
⊢ 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 : 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⟯)
Tactic: rw [← mk_eq_div, mk_smul, mk_eq_div]