-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (goal)
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → CommSemiring (R i)
i : ι
S : Submonoid (R i)
T : Submonoid ((i : ι) → R i) := Submonoid.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) S
r₁ : (i : ι) → R i
s₁ : ↥T
r₂ : (i : ι) → R i
s₂ : ↥T
s : ↥S
hs :
  (↑s : R i) *
      HMul.hMul (α := R i) (β := R i)
        ((↑(Subtype.mk (p := fun (x : R i) ↦ x ∈ S)
                (((Pi.evalRingHom R i : ((i : ι) → R i) →+* R i) : (a : (i : ι) → R i) → R i) (↑s₂ : (i : ι) → R i))
                ⋯) :
            R i) :
          R i)
        (((Pi.evalRingHom R i : ((i : ι) → R i) →+* R i) : (a : (i : ι) → R i) → R i) r₁ : R i) =
    (↑s : R i) *
      HMul.hMul (α := R i) (β := R i)
        ((↑(Subtype.mk (p := fun (x : R i) ↦ x ∈ S)
                (((Pi.evalRingHom R i : ((i : ι) → R i) →+* R i) : (a : (i : ι) → R i) → R i) (↑s₁ : (i : ι) → R i))
                ⋯) :
            R i) :
          R i)
        (((Pi.evalRingHom R i : ((i : ι) → R i) →+* R i) : (a : (i : ι) → R i) → R i) r₂ : R i)
j : ι
refine_1 :
  ∀ (S : Submonoid (R j)),
    let T : Submonoid ((i : ι) → R i) := Submonoid.comap (F := ((i : ι) → R i) →+* R j) (Pi.evalRingHom R j) S;
    ∀ (s₁ s₂ : ↥T) (s : ↥S)
      (hs :
        (↑s : R j) *
            HMul.hMul (α := R j) (β := R j)
              ((↑(Subtype.mk (p := fun (x : R j) ↦ x ∈ S)
                      (((Pi.evalRingHom R j : ((i : ι) → R i) →+* R j) : (a : (i : ι) → R i) → R j)
                        (↑s₂ : (i : ι) → R i))
                      ⋯) :
                  R j) :
                R j)
              (((Pi.evalRingHom R j : ((i : ι) → R i) →+* R j) : (a : (i : ι) → R i) → R j) r₁ : R j) =
          (↑s : R j) *
            HMul.hMul (α := R j) (β := R j)
              ((↑(Subtype.mk (p := fun (x : R j) ↦ x ∈ S)
                      (((Pi.evalRingHom R j : ((i : ι) → R i) →+* R j) : (a : (i : ι) → R i) → R j)
                        (↑s₁ : (i : ι) → R i))
                      ⋯) :
                  R j) :
                R j)
              (((Pi.evalRingHom R j : ((i : ι) → R i) →+* R j) : (a : (i : ι) → R i) → R j) r₂ : R j)),
      ((↑(Subtype.mk (p := fun (x : (i : ι) → R i) ↦ x ∈ T) (update (β := R) 0 j (↑s : R j)) ⋯) : (i : ι) → R i) *
            ((↑s₂ : (i : ι) → R i) * r₁))
          j =
        ((↑(Subtype.mk (p := fun (x : (i : ι) → R i) ↦ x ∈ T) (update (β := R) 0 j (↑s : R j)) ⋯) : (i : ι) → R i) *
            ((↑s₁ : (i : ι) → R i) * r₂))
          j
⊢ ((↑(Subtype.mk (p := fun (x : (i : ι) → R i) ↦ x ∈ T) (update (β := R) 0 i (↑s : R i)) ⋯) : (i : ι) → R i) *
        ((↑s₂ : (i : ι) → R i) * r₁))
      j =
    ((↑(Subtype.mk (p := fun (x : (i : ι) → R i) ↦ x ∈ T) (update (β := R) 0 i (↑s : R i)) ⋯) : (i : ι) → R i) *
        ((↑s₁ : (i : ι) → R i) * r₂))
      j
have refine_1₁ : ∀ (ne : j ≠ i),
  ((↑(Subtype.mk (p := fun (x : (i : ι) → R i) ↦ x ∈ T) (update (β := R) 0 i (↑s : R i)) sorry) : (i : ι) → R i) *
        ((↑s₂ : (i : ι) → R i) * r₁))
      j =
    ((↑(Subtype.mk (p := fun (x : (i : ι) → R i) ↦ x ∈ T) (update (β := R) 0 i (↑s : R i)) sorry) : (i : ι) → R i) *
        ((↑s₁ : (i : ι) → R i) * r₂))
      j
Tactic: obtain rfl | ne := eq_or_ne j i