-- 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]
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])
hqq' :
  Membership.mem.{u_4, u_4} (α := S[X]) (γ := Submonoid S[X]) S[X]⁰ ((φ : (a : R[X]) → S[X]) (↑(q * q') : R[X]) : S[X])
H H₁ :
  ({ toFractionRing := Localization.mk p q : R⟮X⟯ } * { toFractionRing := Localization.mk p' q' : R⟮X⟯ }).liftOn
      (fun (n d : R[X]) ↦
        if h : Membership.mem.{u_4, u_4} (α := S[X]) (γ := Submonoid S[X]) S[X]⁰ ((φ : (a : R[X]) → S[X]) d : S[X]) then
          {
            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) h) }
        else 0)
      ⋯ =
    HMul.hMul (α := S⟮X⟯)
      ({ toFractionRing := Localization.mk p q : R⟮X⟯ }.liftOn
        (fun (n d : R[X]) ↦
          if h :
              Membership.mem.{u_4, u_4} (α := S[X]) (γ := Submonoid S[X]) S[X]⁰ ((φ : (a : R[X]) → S[X]) d : S[X]) then
            {
              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) h) :
              S⟮X⟯ }
          else 0)
        ⋯)
      ({ toFractionRing := Localization.mk p' q' : R⟮X⟯ }.liftOn
        (fun (n d : R[X]) ↦
          if h :
              Membership.mem.{u_4, u_4} (α := S[X]) (γ := Submonoid S[X]) S[X]⁰ ((φ : (a : R[X]) → S[X]) d : S[X]) then
            {
              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) h) :
              S⟮X⟯ }
          else 0)
        ⋯)
⊢ ({ toFractionRing := Localization.mk (p, q).1 (p, q).2 : R⟮X⟯ } *
          { toFractionRing := Localization.mk (p', q').1 (p', q').2 : R⟮X⟯ }).liftOn
      (fun (n d : R[X]) ↦
        if h : Membership.mem.{u_4, u_4} (α := S[X]) (γ := Submonoid S[X]) S[X]⁰ ((φ : (a : R[X]) → S[X]) d : S[X]) then
          {
            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) h) }
        else 0)
      ⋯ =
    HMul.hMul (α := S⟮X⟯)
      ({ toFractionRing := Localization.mk (p, q).1 (p, q).2 : R⟮X⟯ }.liftOn
        (fun (n d : R[X]) ↦
          if h :
              Membership.mem.{u_4, u_4} (α := S[X]) (γ := Submonoid S[X]) S[X]⁰ ((φ : (a : R[X]) → S[X]) d : S[X]) then
            {
              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) h) :
              S⟮X⟯ }
          else 0)
        ⋯)
      ({ toFractionRing := Localization.mk (p', q').1 (p', q').2 : R⟮X⟯ }.liftOn
        (fun (n d : R[X]) ↦
          if h :
              Membership.mem.{u_4, u_4} (α := S[X]) (γ := Submonoid S[X]) S[X]⁰ ((φ : (a : R[X]) → S[X]) d : S[X]) then
            {
              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) h) :
              S⟮X⟯ }
          else 0)
        ⋯)
have H₂ : { toFractionRing := Localization.mk p q * Localization.mk p' q' : R⟮X⟯ }.liftOn
    (fun (n d : R[X]) ↦
      if h : Membership.mem.{u_4, u_4} (α := S[X]) (γ := Submonoid S[X]) S[X]⁰ ((φ : (a : R[X]) → S[X]) d : S[X]) then
        {
          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) h) }
      else 0)
    sorry =
  HMul.hMul (α := S⟮X⟯)
    ({ toFractionRing := Localization.mk p q : R⟮X⟯ }.liftOn
      (fun (n d : R[X]) ↦
        if h : Membership.mem.{u_4, u_4} (α := S[X]) (γ := Submonoid S[X]) S[X]⁰ ((φ : (a : R[X]) → S[X]) d : S[X]) then
          {
            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) h) :
            S⟮X⟯ }
        else 0)
      sorry)
    ({ toFractionRing := Localization.mk p' q' : R⟮X⟯ }.liftOn
      (fun (n d : R[X]) ↦
        if h : Membership.mem.{u_4, u_4} (α := S[X]) (γ := Submonoid S[X]) S[X]⁰ ((φ : (a : R[X]) → S[X]) d : S[X]) then
          {
            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) h) :
            S⟮X⟯ }
        else 0)
      sorry)
Tactic: simp_rw [← ofFractionRing_mul, Localization.mk_mul, liftOn_ofFractionRing_mk, dif_pos hq,
      dif_pos hq', dif_pos hqq', ← ofFractionRing_mul, Submonoid.coe_mul, map_mul,
      Localization.mk_mul, Submonoid.mk_mul_mk]