-- 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))
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))
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) (β := T) (1 : 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) *
      HMul.hMul (α := 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) ((f : (a : R) → T) (↑sa : R) : T)
      (HMul.hMul (α := 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) ((f : (a : R) → T) (↑sa : R) : 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) ((f : (a : R) → T) ((↑sa : R) * 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) ((f : (a : R) → T) (ra * (↑s₂ : 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) ((f : (a : R) → T) ra : T) ((f : (a : R) → T) (↑s₂ : 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) ((f : (a : R) → T) ra : 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)
c₁₈ :
  HMul.hMul (α := T) (β := T) ((f : (a : R) → T) ra : T) ((f : (a : R) → T) r₂ : T) =
    HMul.hMul (α := T) ((f : (a : R) → T) ra : T)
      ((↑((fS : (a : ↥S) → Tˣ) s₂) : 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) ((f : (a : R) → T) ra : 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))
⊢ 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) =
  HMul.hMul (α := T) ((f : (a : R) → T) ra : T) (HMul.hMul (α := T) (β := T) (1 : 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]