-- 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
_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 ⋯) } =
    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 ⋯) :
        K⟮X⟯ }
⊢ 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 :=
      HMul.hMul (α := FractionRing K[X]) (β := FractionRing K[X])
        ((algebraMap K[X] (FractionRing K[X]) : (a : K[X]) → FractionRing K[X])
            ((algebraMap R K[X] : (a : R) → K[X]) c) :
          FractionRing K[X])
        (IsLocalization.mk' (FractionRing K[X]) p
            (Subtype.mk (p := fun (x : K[X]) ↦ Membership.mem (γ := Submonoid K[X]) K[X]⁰ x) q sorry) :
          FractionRing K[X]) :
    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]