-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
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)))
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))
⊢ 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

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]

Premises used: Pi.algebraMap_apply, Pi.mul_apply, Ideal.Quotient.algebraMap_quotient_map_quotient, RingHomCompTriple.comp_apply, Ideal.Quotient.mk_eq_mk, Algebra.smul_def, Submodule.Quotient.quot_mk_eq_mk, Ideal.Quotient.mk_algebraMap