-- 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 : 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
mk :
  ∀ (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
⊢ 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)) =
    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))

Tactic:
ext P