-- Module: Mathlib.FieldTheory.RatFunc.Basic
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]⁰
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)
        ⋯ =
      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 := 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 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)
        ⋯)

Tactic:
cases y using Localization.induction_on with | _ p'q'