-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p_1 : Ideal R
P_1 : Ideal S
inst_3 : IsDedekindDomain S
p : Ideal R
hp : Ne.{v + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
m : R ⧸ p
c : R
x_1 : HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p)
x : S
P : ↥(Multiset.toFinset (factors (map (F := R →+* S) f p)))
⊢ Equiv.toFun
      (RingEquiv.toEquiv
        (piQuotientEquiv p hp :
          HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p) ≃+*
            ((P : ↥(Multiset.toFinset (factors (map (F := R →+* S) f p)))) →
              S ⧸ (↑P : Ideal S) ^ p.ramificationIdx (↑P : Ideal S))))
      (HSMul.hSMul (α := R ⧸ p) (β := HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p))
        (Quot.mk (⇑(Submodule.quotientRel p) : R → R → Prop) c)
        (Quot.mk (⇑(Submodule.quotientRel (map f p)) : S → S → Prop) x))
      P =
    HSMul.hSMul (α := R ⧸ p) (β :=
      (P : ↥(Multiset.toFinset (factors (map (F := R →+* S) f p)))) →
        S ⧸ (↑P : Ideal S) ^ p.ramificationIdx (↑P : Ideal S))
      ((RingHom.id (R ⧸ p) : (a : R ⧸ p) → R ⧸ p) (Quot.mk (⇑(Submodule.quotientRel p) : R → R → Prop) c) : R ⧸ p)
      (Equiv.toFun
          (RingEquiv.toEquiv
            (piQuotientEquiv p hp :
              HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p) ≃+*
                ((P : ↥(Multiset.toFinset (factors (map (F := R →+* S) f p)))) →
                  S ⧸ (↑P : Ideal S) ^ p.ramificationIdx (↑P : Ideal S))))
          (Quot.mk (⇑(Submodule.quotientRel (map f p)) : S → S → Prop) x) :
        (P : ↥(Multiset.toFinset (factors (map (F := R →+* S) f p)))) →
          S ⧸ (↑P : Ideal S) ^ p.ramificationIdx (↑P : Ideal S))
      P
have mk : Equiv.toFun
    (RingEquiv.toEquiv
      (piQuotientEquiv p hp :
        HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p) ≃+*
          ((P : ↥(Multiset.toFinset (factors (map (F := R →+* S) f p)))) →
            S ⧸ (↑P : Ideal S) ^ p.ramificationIdx (↑P : Ideal S))))
    (HMul.hMul (α := HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p)) (β :=
      HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p))
      ((algebraMap R (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p)) : (a : R) → S ⧸ map f p) c :
        HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p))
      ((Quotient.mk (map (F := R →+* S) f p) : (a : S) → S ⧸ map f p) x :
        HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p)))
    P =
  HMul.hMul (α := S ⧸ (↑P : Ideal S) ^ p.ramificationIdx (↑P : Ideal S)) (β :=
    S ⧸ (↑P : Ideal S) ^ p.ramificationIdx (↑P : Ideal S))
    ((algebraMap (R ⧸ p) (S ⧸ (↑P : Ideal S) ^ p.ramificationIdx (↑P : Ideal S)) :
          (a : R ⧸ p) → S ⧸ (↑P : Ideal S) ^ p.ramificationIdx (↑P : Ideal S))
        ((Quotient.mk p : (a : R) → R ⧸ p) c) :
      S ⧸ (↑P : Ideal S) ^ p.ramificationIdx (↑P : Ideal S))
    (Equiv.toFun
        (RingEquiv.toEquiv
          (piQuotientEquiv p hp :
            HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p) ≃+*
              ((P : ↥(Multiset.toFinset (factors (map (F := R →+* S) f p)))) →
                S ⧸ (↑P : Ideal S) ^ p.ramificationIdx (↑P : Ideal S))))
        ((Quotient.mk (map (F := R →+* S) f p) : (a : S) → S ⧸ map f p) x) P :
      S ⧸ (↑P : Ideal S) ^ p.ramificationIdx (↑P : Ideal S))
Tactic: simp only [Submodule.Quotient.quot_mk_eq_mk, Quotient.mk_eq_mk, Algebra.smul_def,
        Quotient.algebraMap_quotient_map_quotient, Quotient.mk_algebraMap,
        RingHomCompTriple.comp_apply, Pi.mul_apply, Pi.algebraMap_apply]