-- 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
X : Type ?u.80272
inst_2 : MulAction R X
T : Type u_2
inst_3 : 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)
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
ra : R
sa : ↥S
ha : (↑sa : R) * r₁ = ra * (↑s₂ : R)
c :
  HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) (sa * s₁))⁻¹ : T) : T) ((f : (a : R) → T) (ra * r₂) : T) =
    HMul.hMul (α := T)
      (liftExpand
        (fun (r : R) (s : ↥S) ↦
          HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((f : (a : R) → T) r : T))
        ⋯ (r₁ /ₒ s₁))
      (liftExpand
        (fun (r : R) (s : ↥S) ↦
          HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((f : (a : R) → T) r : T))
        ⋯ (r₂ /ₒ s₂))
c₁ :
  HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) (sa * s₁))⁻¹ : T) : T) ((f : (a : R) → T) (ra * r₂) : T) =
    HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s₁)⁻¹ : T) : T) ((f : (a : R) → T) r₁ : T) *
      liftExpand
        (fun (r : R) (s : ↥S) ↦
          HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((f : (a : R) → T) r : T))
        ⋯ (r₂ /ₒ s₂)
c₂ :
  HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) (sa * s₁))⁻¹ : T) : T) ((f : (a : R) → T) (ra * r₂) : T) =
    HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s₁)⁻¹ : T) : T) ((f : (a : R) → T) r₁ : T) *
      HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s₂)⁻¹ : T) : T) ((f : (a : R) → T) r₂ : T)
c₃ :
  (f : (a : R) → T) (ra * r₂) =
    (↑((fS : (a : ↥S) → Tˣ) (sa * s₁)) : T) *
      (HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s₁)⁻¹ : T) : T) ((f : (a : R) → T) r₁ : T) *
        HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s₂)⁻¹ : T) : T) ((f : (a : R) → T) r₂ : T))
c₄ :
  HMul.hMul (α := T) (β := T) ((f : (a : R) → T) ra : T) ((f : (a : R) → T) r₂ : T) =
    (↑((fS : (a : ↥S) → Tˣ) (sa * s₁)) : T) *
      (HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s₁)⁻¹ : T) : T) ((f : (a : R) → T) r₁ : T) *
        HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s₂)⁻¹ : T) : T) ((f : (a : R) → T) r₂ : T))
c₅ :
  HMul.hMul (α := T) (β := T) ((f : (a : R) → T) ra : T) ((f : (a : R) → T) r₂ : T) =
    (↑(HMul.hMul (α := Tˣ) (β := Tˣ) ((fS : (a : ↥S) → Tˣ) sa : Tˣ) ((fS : (a : ↥S) → Tˣ) s₁ : Tˣ)) : T) *
      (HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s₁)⁻¹ : T) : T) ((f : (a : R) → T) r₁ : T) *
        HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s₂)⁻¹ : T) : T) ((f : (a : R) → T) r₂ : T))
c₆ :
  HMul.hMul (α := T) (β := T) ((f : (a : R) → T) ra : T) ((f : (a : R) → T) r₂ : T) =
    HMul.hMul (α := T) (↑((fS : (a : ↥S) → Tˣ) sa) : T) (↑((fS : (a : ↥S) → Tˣ) s₁) : T) *
      (HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s₁)⁻¹ : T) : T) ((f : (a : R) → T) r₁ : T) *
        HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s₂)⁻¹ : T) : T) ((f : (a : R) → T) r₂ : T))
c₇ :
  HMul.hMul (α := T) (β := T) ((f : (a : R) → T) ra : T) ((f : (a : R) → T) r₂ : T) =
    (↑((fS : (a : ↥S) → Tˣ) sa) : T) *
      ((↑((fS : (a : ↥S) → Tˣ) s₁) : T) *
        (HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s₁)⁻¹ : T) : T) ((f : (a : R) → T) r₁ : T) *
          HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s₂)⁻¹ : T) : T) ((f : (a : R) → T) r₂ : T)))
c₈ :
  HMul.hMul (α := T) (β := T) ((f : (a : R) → T) ra : T) ((f : (a : R) → T) r₂ : T) =
    (↑((fS : (a : ↥S) → Tˣ) sa) : T) *
      ((↑((fS : (a : ↥S) → Tˣ) s₁) : T) *
          HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s₁)⁻¹ : T) : T) ((f : (a : R) → T) r₁ : T) *
        HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s₂)⁻¹ : T) : T) ((f : (a : R) → T) r₂ : T))
⊢ liftExpand
      (fun (r : R) (s : ↥S) ↦
        HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((f : (a : R) → T) r : T))
      ⋯ (ra * r₂ /ₒ (sa * s₁)) =
    HMul.hMul (α := T)
      (liftExpand
        (fun (r : R) (s : ↥S) ↦
          HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((f : (a : R) → T) r : T))
        ⋯ (r₁ /ₒ s₁))
      (liftExpand
        (fun (r : R) (s : ↥S) ↦
          HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((f : (a : R) → T) r : T))
        ⋯ (r₂ /ₒ s₂))
have c₉ : HMul.hMul (α := T) (β := T) ((f : (a : R) → T) ra : T) ((f : (a : R) → T) r₂ : T) =
  (↑((fS : (a : ↥S) → Tˣ) sa) : T) *
    (HMul.hMul (β := T) (HMul.hMul (α := T) (↑((fS : (a : ↥S) → Tˣ) s₁) : T) (↑((fS : (a : ↥S) → Tˣ) s₁)⁻¹ : T))
        ((f : (a : R) → T) r₁ : T) *
      HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s₂)⁻¹ : T) : T) ((f : (a : R) → T) r₂ : T))
Tactic: rw [liftExpand_of, liftExpand_of, liftExpand_of, Units.inv_mul_eq_iff_eq_mul, map_mul, map_mul,
      Units.val_mul, mul_assoc, ← mul_assoc (fS s₁ : T), ← mul_assoc (fS s₁ : T), Units.mul_inv,
      one_mul, ← hf, ← mul_assoc, ← map_mul _ _ r₁, ha, map_mul, hf s₂, mul_assoc,
      ← mul_assoc (fS s₂ : T), (fS s₂).mul_inv, one_mul]