-- 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]⁰)
y : FractionRing R[X]
pq : R[X] × ↥R[X]⁰
⊢ ({ toFractionRing := Localization.mk pq.1 pq.2 : R⟮X⟯ } * { toFractionRing := y : 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 pq.1 pq.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 := y : 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 : ∀ (p'q' : R[X] × ↥R[X]⁰),
  ({ toFractionRing := Localization.mk pq.1 pq.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)
      sorry =
    HMul.hMul (α := S⟮X⟯)
      ({ toFractionRing := Localization.mk pq.1 pq.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)
        sorry)
      ({ 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)
        sorry)
Tactic: cases y using Localization.induction_on with | _ p'q'
Cleared hypotheses: y