-- 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]⁰)
simp_rw :
  Eq.{u_4 + 1} (α := S⟮X⟯)
    (RatFunc.liftOn.{u_3, u_4 + 1} (K := R) { toFractionRing := 1 }
      (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)
      ⋯)
    { toFractionRing := 1 }
simp_rw₁ :
  Eq.{u_4 + 1} (α := S⟮X⟯)
    (RatFunc.liftOn.{u_3, u_4 + 1} (K := R) { toFractionRing := Localization.mk 1 1 }
      (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)
      ⋯)
    { toFractionRing := Localization.mk 1 1 }
simp_rw₂ :
  Eq.{u_4 + 1} (α := S⟮X⟯)
    (if h : Membership.mem (γ := Submonoid S[X]) S[X]⁰ ((φ : (a : R[X]) → S[X]) (↑1 : R[X])) then
      {
        toFractionRing :=
          Localization.mk ((φ : (a : R[X]) → S[X]) 1)
            (Subtype.mk (p := fun (x : S[X]) ↦ Membership.mem (γ := Submonoid S[X]) S[X]⁰ x)
              ((φ : (a : R[X]) → S[X]) (↑1 : R[X])) h) }
    else 0)
    { toFractionRing := Localization.mk 1 1 }
simp_rw₃ :
  Eq.{u_4 + 1} (α := S⟮X⟯)
    (if h : Membership.mem (γ := Submonoid S[X]) S[X]⁰ ((φ : (a : R[X]) → S[X]) 1) then
      {
        toFractionRing :=
          Localization.mk ((φ : (a : R[X]) → S[X]) 1)
            (Subtype.mk (p := fun (x : S[X]) ↦ Membership.mem (γ := Submonoid S[X]) S[X]⁰ x) ((φ : (a : R[X]) → S[X]) 1)
              ⋯) }
    else 0)
    { toFractionRing := Localization.mk 1 1 }
⊢ Eq.{u_4 + 1} (α := S⟮X⟯)
    (RatFunc.liftOn.{u_3, u_4 + 1} (K := R) 1
      (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)
      ⋯)
    1
have simp_rw₄ : Eq.{u_4 + 1} (α := S⟮X⟯)
  (if h : Membership.mem (γ := Submonoid S[X]) S[X]⁰ 1 then
    {
      toFractionRing :=
        Localization.mk 1 (Subtype.mk (p := fun (x : S[X]) ↦ Membership.mem (γ := Submonoid S[X]) S[X]⁰ x) 1 sorry) }
  else 0)
  { toFractionRing := Localization.mk 1 1 }
Tactic: simp_rw [← ofFractionRing_one, ← Localization.mk_one, liftOn_ofFractionRing_mk,
      OneMemClass.coe_one, map_one, OneMemClass.one_mem, dite_true, ofFractionRing.injEq,
      Localization.mk_one, Localization.mk_eq_monoidOf_mk', Submonoid.LocalizationMap.mk'_self]