-- Module: Mathlib.RingTheory.LocalRing.Etale
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
refine_1 :
  ∀ (x : S),
    ((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)) (β :=
          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 ⋯) :
                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))
⊢ ((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))

Tactic:
obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x

Premises used: Ideal.Quotient.mk_surjective, rfl