-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
T : Type u_2
inst_2 : Monoid T
f : R →* T
fS : MonoidHom.{u_1, u_2} (↥S) Tˣ
hf : ∀ (s : ↥S), Eq.{u_2 + 1} (α := T) ((f : (a : R) → T) (↑s : R) : T) ((↑((fS : (a : ↥S) → Tˣ) s) : T) : T)
φ : MonoidHom.{u_1, u_2} (OreLocalization S R) T
huniv :
  ∀ (r : R),
    Eq.{u_2 + 1} (α := T)
      ((φ : (a : OreLocalization S R) → T) ((numeratorHom : (a : R) → OreLocalization S R) r : OreLocalization S R) : T)
      ((f : (a : R) → T) r : T)
r : R
s : ↥S
h :
  (φ : (a : OreLocalization S R) → T) (r /ₒ s) =
    HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((f : (a : R) → T) r : T)
h₁ :
  (φ : (a : OreLocalization S R) → T) (r /ₒ s) =
    HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T)
      ((φ : (a : OreLocalization S R) → T) ((numeratorHom : (a : R) → OreLocalization S R) r : OreLocalization S R) : T)
h₂ :
  (φ : (a : OreLocalization S R) → T) (r /ₒ s) =
    HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T)
      ((φ : (a : OreLocalization S R) → T) (r /ₒ 1) : T)
h₃ :
  HMul.hMul (α := T) (β := T) (1 : T) ((φ : (a : OreLocalization S R) → T) (r /ₒ s) : T) =
    HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T)
      ((φ : (a : OreLocalization S R) → T) (r /ₒ 1) : T)
h₄ :
  HMul.hMul (α := T) (β := T) ((↑1 : T) : T) ((φ : (a : OreLocalization S R) → T) (r /ₒ s) : T) =
    HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T)
      ((φ : (a : OreLocalization S R) → T) (r /ₒ 1) : T)
h₅ :
  HMul.hMul (β := T)
      (↑(HMul.hMul (α := Tˣ) (β := Tˣ) (((fS : (a : ↥S) → Tˣ) s)⁻¹ : Tˣ) ((fS : (a : ↥S) → Tˣ) s : Tˣ)) : T)
      ((φ : (a : OreLocalization S R) → T) (r /ₒ s) : T) =
    HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T)
      ((φ : (a : OreLocalization S R) → T) (r /ₒ 1) : T)
h₆ :
  HMul.hMul (β := T) (HMul.hMul (α := T) (↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) (↑((fS : (a : ↥S) → Tˣ) s) : T))
      ((φ : (a : OreLocalization S R) → T) (r /ₒ s) : T) =
    HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T)
      ((φ : (a : OreLocalization S R) → T) (r /ₒ 1) : T)
h₇ :
  (↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) *
      HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s) : T) : T)
        ((φ : (a : OreLocalization S R) → T) (r /ₒ s) : T) =
    HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T)
      ((φ : (a : OreLocalization S R) → T) (r /ₒ 1) : T)
⊢ Eq.{u_2 + 1} (α := T) ((φ : (a : OreLocalization S R) → T) (r /ₒ s) : T)
    ((universalMulHom f fS hf : (a : OreLocalization S R) → T) (r /ₒ s) : T)
have h₈ : (↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) *
    HMul.hMul (α := T) (β := T) ((f : (a : R) → T) (↑s : R) : T) ((φ : (a : OreLocalization S R) → T) (r /ₒ s) : T) =
  HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((φ : (a : OreLocalization S R) → T) (r /ₒ 1) : T)
Tactic: rw [universalMulHom_apply, ← huniv r, numeratorHom_apply, ← one_mul (φ (r /ₒ s)), ←
    Units.val_one, ← inv_mul_cancel (fS s), Units.val_mul, mul_assoc, ← hf, ← huniv, ← φ.map_mul,
    numeratorHom_apply, OreLocalization.mul_cancel]