-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Etale (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing S
inst_4 : IsLocalRing R
inst_5 : Module.Finite R S
inst_6 : FaithfulSMul R S
inst_7 : Etale R S
this : Module.Free R S
x : HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R))
r : R
⊢ ((RingEquiv.toAddEquiv (Ideal.quotEquivOfEq ⋯) :
          HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) ≃+
            HasQuotient.Quotient S (B := Ideal S) (maximalIdeal S : Ideal S)) :
        (a : S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R)) → S ⧸ maximalIdeal S)
      (HSMul.hSMul (α := HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R))
        ((Ideal.Quotient.mk (maximalIdeal R) : (a : R) → R ⧸ maximalIdeal R) r :
          HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R : Ideal R))
        x) =
    HSMul.hSMul (α := HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R)) (β :=
      HasQuotient.Quotient S (B := Ideal S) (maximalIdeal S : Ideal S))
      ((Ideal.Quotient.mk (maximalIdeal R) : (a : R) → R ⧸ maximalIdeal R) r :
        HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R : Ideal R))
      (((RingEquiv.toAddEquiv (Ideal.quotEquivOfEq ⋯) :
              HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) ≃+
                HasQuotient.Quotient S (B := Ideal S) (maximalIdeal S : Ideal S)) :
            (a : S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R)) → S ⧸ maximalIdeal S)
          x :
        HasQuotient.Quotient S (B := Ideal S) (maximalIdeal S : Ideal S))
have refine_1 : ∀ (x : S),
  ((RingEquiv.toAddEquiv (Ideal.quotEquivOfEq sorry) :
          HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) ≃+
            HasQuotient.Quotient S (B := Ideal S) (maximalIdeal S : Ideal S)) :
        (a : S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R)) → S ⧸ maximalIdeal S)
      (HSMul.hSMul (α := HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R)) (β :=
        HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)))
        ((Ideal.Quotient.mk (maximalIdeal R) : (a : R) → R ⧸ maximalIdeal R) r :
          HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R : Ideal R))
        ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) :
              (a : S) → S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R))
            x :
          HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)))) =
    HSMul.hSMul (α := HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R)) (β :=
      HasQuotient.Quotient S (B := Ideal S) (maximalIdeal S : Ideal S))
      ((Ideal.Quotient.mk (maximalIdeal R) : (a : R) → R ⧸ maximalIdeal R) r :
        HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R : Ideal R))
      (((RingEquiv.toAddEquiv (Ideal.quotEquivOfEq sorry) :
              HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) ≃+
                HasQuotient.Quotient S (B := Ideal S) (maximalIdeal S : Ideal S)) :
            (a : S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R)) → S ⧸ maximalIdeal S)
          ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) :
              (a : S) → S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R))
            x) :
        HasQuotient.Quotient S (B := Ideal S) (maximalIdeal S : Ideal S))
Tactic: obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
Cleared hypotheses: x