awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Localization.AtPrime.Extension
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
Rₚ : Type u_3
inst_4 : CommRing Rₚ
inst_5 : Algebra R Rₚ
inst_6 : IsLocalization.AtPrime Rₚ p
inst_7 : IsLocalRing Rₚ
Sₚ : Type u_4
inst_8 : CommRing Sₚ
inst_9 : Algebra S Sₚ
inst_10 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst_11 : Algebra Rₚ Sₚ
P : Ideal S
hPp : P.LiesOver p
inst_12 : Algebra R Sₚ
inst_13 : IsScalarTower R S Sₚ
inst_14 : IsScalarTower R Rₚ Sₚ
inst_15 : p.IsMaximal
inst_16 : P.IsMaximal
inst_17 : LiesOver.{u_3, u_4} (B := Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) (maximalIdeal Rₚ)
h :
  ∀ (x : Rₚ),
    Eq.{u_2 + 1} (α := S ⧸ P)
      ((RingHom.comp (β := HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ : Ideal Rₚ))
              (RingHom.comp (algebraMap (R ⧸ p) (S ⧸ P))
                (RingEquiv.toRingHom (RingEquiv.symm (equivQuotMaximalIdeal p Rₚ))))
              (Ideal.Quotient.mk (maximalIdeal Rₚ)) :
            (a : Rₚ) → S ⧸ P)
          x :
        S ⧸ P)
      ((RingHom.comp (β := HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ : Ideal Rₚ))
              (RingHom.comp (β :=
                HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
                (RingEquiv.toRingHom (RingEquiv.symm (equivQuotientMapOfIsMaximal p Sₚ P)))
                (algebraMap (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
                  (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))))
              (Ideal.Quotient.mk (maximalIdeal Rₚ)) :
            (a : Rₚ) → S ⧸ P)
          x :
        S ⧸ P)
⊢ Eq (α := RingHom.{u_3, u_2} (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ)) (S ⧸ P))
    (RingHom.comp (algebraMap (R ⧸ p) (S ⧸ P)) (RingEquiv.toRingHom (RingEquiv.symm (equivQuotMaximalIdeal p Rₚ))))
    (RingHom.comp (β := HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
      (RingEquiv.toRingHom (RingEquiv.symm (equivQuotientMapOfIsMaximal p Sₚ P)))
      (algebraMap (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
        (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))))

Tactic:
ext x
-- Module: Mathlib.RingTheory.Localization.AtPrime.Extension
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
Rₚ : Type u_3
inst_4 : CommRing Rₚ
inst_5 : Algebra R Rₚ
inst_6 : IsLocalization.AtPrime Rₚ p
inst_7 : IsLocalRing Rₚ
Sₚ : Type u_4
inst_8 : CommRing Sₚ
inst_9 : Algebra S Sₚ
inst_10 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst_11 : Algebra Rₚ Sₚ
P : Ideal S
hPp : P.LiesOver p
inst_12 : Algebra R Sₚ
inst_13 : IsScalarTower R S Sₚ
inst_14 : IsScalarTower R Rₚ Sₚ
inst_15 : p.IsMaximal
inst_16 : P.IsMaximal
inst_17 : LiesOver.{u_3, u_4} (B := Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) (maximalIdeal Rₚ)
x : Rₚ
⊢ Eq.{u_2 + 1} (α := S ⧸ P)
    ((RingHom.comp (β := HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ : Ideal Rₚ))
            (RingHom.comp (algebraMap (R ⧸ p) (S ⧸ P))
              (RingEquiv.toRingHom (RingEquiv.symm (equivQuotMaximalIdeal p Rₚ))))
            (Ideal.Quotient.mk (maximalIdeal Rₚ)) :
          (a : Rₚ) → S ⧸ P)
        x :
      S ⧸ P)
    ((RingHom.comp (β := HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ : Ideal Rₚ))
            (RingHom.comp (β := HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
              (RingEquiv.toRingHom (RingEquiv.symm (equivQuotientMapOfIsMaximal p Sₚ P)))
              (algebraMap (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
                (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))))
            (Ideal.Quotient.mk (maximalIdeal Rₚ)) :
          (a : Rₚ) → S ⧸ P)
        x :
      S ⧸ P)

Tactic:
algebraMap_equivQuotMaximalIdeal_symm_apply p Rₚ Sₚ P x

Premises used: Quotient.liftOn', Ideal.Quotient.mk, AddCon.liftOn, Submodule.Quotient.mk, IsLocalRing.maximalIdeal, IsLocalization.AtPrime.algebraMap_equivQuotMaximalIdeal_symm_apply, Quot.map, DFunLike.coe
-- Module: Mathlib.RingTheory.Localization.AtPrime.Extension
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
Rₚ : Type u_3
inst_4 : CommRing Rₚ
inst_5 : Algebra R Rₚ
inst_6 : IsLocalization.AtPrime Rₚ p
inst_7 : IsLocalRing Rₚ
Sₚ : Type u_4
inst_8 : CommRing Sₚ
inst_9 : Algebra S Sₚ
inst_10 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst_11 : Algebra Rₚ Sₚ
P : Ideal S
hPp : P.LiesOver p
inst_12 : Algebra R Sₚ
inst_13 : IsScalarTower R S Sₚ
inst_14 : IsScalarTower R Rₚ Sₚ
inst_15 : p.IsMaximal
inst_16 : P.IsMaximal
inst_17 : LiesOver.{u_3, u_4} (B := Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) (maximalIdeal Rₚ)
x : Rₚ
⊢ Eq.{u_2 + 1} (α := S ⧸ P)
    ((RingHom.comp (β := HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ : Ideal Rₚ))
            (RingHom.comp (algebraMap (R ⧸ p) (S ⧸ P))
              (RingEquiv.toRingHom (RingEquiv.symm (equivQuotMaximalIdeal p Rₚ))))
            (Ideal.Quotient.mk (maximalIdeal Rₚ)) :
          (a : Rₚ) → S ⧸ P)
        x :
      S ⧸ P)
    ((RingHom.comp (β := HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ : Ideal Rₚ))
            (RingHom.comp (β := HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
              (RingEquiv.toRingHom (RingEquiv.symm (equivQuotientMapOfIsMaximal p Sₚ P)))
              (algebraMap (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
                (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))))
            (Ideal.Quotient.mk (maximalIdeal Rₚ)) :
          (a : Rₚ) → S ⧸ P)
        x :
      S ⧸ P)

Tactic:
exact algebraMap_equivQuotMaximalIdeal_symm_apply p Rₚ Sₚ P x

Premises used: Ideal.Quotient.mk, IsLocalRing.maximalIdeal, IsLocalization.AtPrime.algebraMap_equivQuotMaximalIdeal_symm_apply, DFunLike.coe
-- Module: Mathlib.RingTheory.Localization.AtPrime.Extension
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
Rₚ : Type u_3
inst_4 : CommRing Rₚ
inst_5 : Algebra R Rₚ
inst_6 : IsLocalization.AtPrime Rₚ p
inst_7 : IsLocalRing Rₚ
Sₚ : Type u_4
inst_8 : CommRing Sₚ
inst_9 : Algebra S Sₚ
inst_10 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst_11 : Algebra Rₚ Sₚ
P : Ideal S
hPp : P.LiesOver p
inst_12 : Algebra R Sₚ
inst_13 : IsScalarTower R S Sₚ
inst_14 : IsScalarTower R Rₚ Sₚ
inst_15 : IsDomain R
inst_16 : IsTorsionFree R S
inst_17 : IsTorsionFree R Rₚ
inst_18 : IsTorsionFree S Sₚ
inst_19 : IsTorsionFree Rₚ Sₚ
inst_20 : IsDedekindDomain S
inst_21 : IsDedekindDomain Rₚ
inst_22 : IsDedekindDomain Sₚ
hp : p ≠ ⊥
inst_23 : P.IsPrime
rw : Ne.{u_3 + 1} (α := Ideal Rₚ) (Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) p) ⊥
⊢ Ne (α := Ideal Rₚ) (maximalIdeal Rₚ) ⊥

Tactic:
rw [← map_eq_maximalIdeal p]

Premises used: IsLocalization.AtPrime.map_eq_maximalIdeal
-- Module: Mathlib.RingTheory.Localization.AtPrime.Extension
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
Rₚ : Type u_3
inst_4 : CommRing Rₚ
inst_5 : Algebra R Rₚ
inst_6 : IsLocalization.AtPrime Rₚ p
inst_7 : IsLocalRing Rₚ
Sₚ : Type u_4
inst_8 : CommRing Sₚ
inst_9 : Algebra S Sₚ
inst_10 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst_11 : Algebra Rₚ Sₚ
P : Ideal S
hPp : P.LiesOver p
inst_12 : Algebra R Sₚ
inst_13 : IsScalarTower R S Sₚ
inst_14 : IsScalarTower R Rₚ Sₚ
inst_15 : IsDomain R
inst_16 : IsTorsionFree R S
inst_17 : IsTorsionFree R Rₚ
inst_18 : IsTorsionFree S Sₚ
inst_19 : IsTorsionFree Rₚ Sₚ
inst_20 : IsDedekindDomain S
inst_21 : IsDedekindDomain Rₚ
inst_22 : IsDedekindDomain Sₚ
hp : p ≠ ⊥
inst_23 : P.IsPrime
⊢ Ne.{u_3 + 1} (α := Ideal Rₚ) (Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) p) ⊥

Tactic:
map_ne_bot_of_ne_bot hp

Premises used: Ideal.map_ne_bot_of_ne_bot
-- Module: Mathlib.RingTheory.Localization.AtPrime.Extension
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
Rₚ : Type u_3
inst_4 : CommRing Rₚ
inst_5 : Algebra R Rₚ
inst_6 : IsLocalization.AtPrime Rₚ p
inst_7 : IsLocalRing Rₚ
Sₚ : Type u_4
inst_8 : CommRing Sₚ
inst_9 : Algebra S Sₚ
inst_10 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst_11 : Algebra Rₚ Sₚ
P : Ideal S
hPp : P.LiesOver p
inst_12 : Algebra R Sₚ
inst_13 : IsScalarTower R S Sₚ
inst_14 : IsScalarTower R Rₚ Sₚ
inst_15 : IsDomain R
inst_16 : IsTorsionFree R S
inst_17 : IsTorsionFree R Rₚ
inst_18 : IsTorsionFree S Sₚ
inst_19 : IsTorsionFree Rₚ Sₚ
inst_20 : IsDedekindDomain S
inst_21 : IsDedekindDomain Rₚ
inst_22 : IsDedekindDomain Sₚ
hp : p ≠ ⊥
inst_23 : P.IsPrime
⊢ Ne.{u_3 + 1} (α := Ideal Rₚ) (Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) p) ⊥

Tactic:
exact map_ne_bot_of_ne_bot hp

Premises used: Ideal.map_ne_bot_of_ne_bot
-- Module: Mathlib.RingTheory.Localization.AtPrime.Extension
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
Rₚ : Type u_3
inst_4 : CommRing Rₚ
inst_5 : Algebra R Rₚ
inst_6 : IsLocalization.AtPrime Rₚ p
inst_7 : IsLocalRing Rₚ
Sₚ : Type u_4
inst_8 : CommRing Sₚ
inst_9 : Algebra S Sₚ
inst_10 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst_11 : Algebra Rₚ Sₚ
P : Ideal S
hPp : P.LiesOver p
inst_12 : Algebra R Sₚ
inst_13 : IsScalarTower R S Sₚ
inst_14 : IsScalarTower R Rₚ Sₚ
inst_15 : IsDomain R
inst_16 : IsTorsionFree R S
inst_17 : IsTorsionFree R Rₚ
inst_18 : IsTorsionFree S Sₚ
inst_19 : IsTorsionFree Rₚ Sₚ
inst_20 : IsDedekindDomain S
inst_21 : IsDedekindDomain Rₚ
inst_22 : IsDedekindDomain Sₚ
hp : p ≠ ⊥
inst_23 : P.IsPrime
⊢ Ne (α := Ideal Rₚ) (maximalIdeal Rₚ) ⊥

Tactic:
have h₁ : maximalIdeal Rₚ ≠ ⊥ := by
    rw [← map_eq_maximalIdeal p]
    exact map_ne_bot_of_ne_bot hp
-- Module: Mathlib.RingTheory.Localization.AtPrime.Extension
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
Rₚ : Type u_3
inst_4 : CommRing Rₚ
inst_5 : Algebra R Rₚ
inst_6 : IsLocalization.AtPrime Rₚ p
inst_7 : IsLocalRing Rₚ
Sₚ : Type u_4
inst_8 : CommRing Sₚ
inst_9 : Algebra S Sₚ
inst_10 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst_11 : Algebra Rₚ Sₚ
P : Ideal S
hPp : P.LiesOver p
inst_12 : Algebra R Sₚ
inst_13 : IsScalarTower R S Sₚ
inst_14 : IsScalarTower R Rₚ Sₚ
inst_15 : IsDomain R
inst_16 : IsTorsionFree R S
inst_17 : IsTorsionFree R Rₚ
inst_18 : IsTorsionFree S Sₚ
inst_19 : IsTorsionFree Rₚ Sₚ
inst_20 : IsDedekindDomain S
inst_21 : IsDedekindDomain Rₚ
inst_22 : IsDedekindDomain Sₚ
hp : p ≠ ⊥
inst_23 : P.IsPrime
h₁ : Ne (α := Ideal Rₚ) (maximalIdeal Rₚ) ⊥
⊢ IsPrime.{u_4} (α := Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)

Tactic:
have : (P.map (algebraMap S Sₚ)).IsPrime := isPrime_map_of_liesOver S p Sₚ P
-- Module: Mathlib.RingTheory.Localization.AtPrime.Extension
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
Rₚ : Type u_3
inst_4 : CommRing Rₚ
inst_5 : Algebra R Rₚ
inst_6 : IsLocalization.AtPrime Rₚ p
inst_7 : IsLocalRing Rₚ
Sₚ : Type u_4
inst_8 : CommRing Sₚ
inst_9 : Algebra S Sₚ
inst_10 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst_11 : Algebra Rₚ Sₚ
P : Ideal S
hPp : P.LiesOver p
inst_12 : Algebra R Sₚ
inst_13 : IsScalarTower R S Sₚ
inst_14 : IsScalarTower R Rₚ Sₚ
inst_15 : IsDomain R
inst_16 : IsTorsionFree R S
inst_17 : IsTorsionFree R Rₚ
inst_18 : IsTorsionFree S Sₚ
inst_19 : IsTorsionFree Rₚ Sₚ
inst_20 : IsDedekindDomain S
inst_21 : IsDedekindDomain Rₚ
inst_22 : IsDedekindDomain Sₚ
hp : p ≠ ⊥
inst_23 : P.IsPrime
h₁ : Ne (α := Ideal Rₚ) (maximalIdeal Rₚ) ⊥
this : IsPrime.{u_4} (α := Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
pos :
  ∀ (hP : P = ⊥),
    ramificationIdx.{u_3, u_4} (S := Sₚ) (maximalIdeal Rₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) =
      p.ramificationIdx P
neg :
  ∀ (hP : ¬P = ⊥),
    ramificationIdx.{u_3, u_4} (S := Sₚ) (maximalIdeal Rₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) =
      p.ramificationIdx P
⊢ ramificationIdx.{u_3, u_4} (S := Sₚ) (maximalIdeal Rₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) =
    p.ramificationIdx P

Tactic:
by_cases hP : P = ⊥
-- Module: Mathlib.RingTheory.Localization.AtPrime.Extension
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
Rₚ : Type u_3
inst_4 : CommRing Rₚ
inst_5 : Algebra R Rₚ
inst_6 : IsLocalization.AtPrime Rₚ p
inst_7 : IsLocalRing Rₚ
Sₚ : Type u_4
inst_8 : CommRing Sₚ
inst_9 : Algebra S Sₚ
inst_10 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst_11 : Algebra Rₚ Sₚ
P : Ideal S
hPp : P.LiesOver p
inst_12 : Algebra R Sₚ
inst_13 : IsScalarTower R S Sₚ
inst_14 : IsScalarTower R Rₚ Sₚ
inst_15 : IsDomain R
inst_16 : IsTorsionFree R S
inst_17 : IsTorsionFree R Rₚ
inst_18 : IsTorsionFree S Sₚ
inst_19 : IsTorsionFree Rₚ Sₚ
inst_20 : IsDedekindDomain S
inst_21 : IsDedekindDomain Rₚ
inst_22 : IsDedekindDomain Sₚ
hp : p ≠ ⊥
inst_23 : P.IsPrime
h₁ : Ne (α := Ideal Rₚ) (maximalIdeal Rₚ) ⊥
this : IsPrime.{u_4} (α := Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
hP : P = ⊥
pos :
  ramificationIdx.{u_3, u_4} (S := Sₚ) (maximalIdeal Rₚ) (Ideal.map (R := S) (F := S →+* Sₚ) (algebraMap S Sₚ) ⊥) =
    ramificationIdx.{u_1, u_2} (S := S) p ⊥
pos₁ : ramificationIdx.{u_3, u_4} (S := Sₚ) (maximalIdeal Rₚ) ⊥ = ramificationIdx.{u_1, u_2} (S := S) p ⊥
pos₂ : ramificationIdx.{u_3, u_4} (S := Sₚ) (maximalIdeal Rₚ) ⊥ = 0
⊢ ramificationIdx.{u_3, u_4} (S := Sₚ) (maximalIdeal Rₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) =
    p.ramificationIdx P

Tactic:
simp_rw [hP, Ideal.map_bot, ramificationIdx_bot' hp
      (FaithfulSMul.algebraMap_injective _ _),
      ramificationIdx_bot' h₁ (FaithfulSMul.algebraMap_injective Rₚ Sₚ)]

Premises used: Ideal.map_bot, Ideal.ramificationIdx_bot', FaithfulSMul.algebraMap_injective
-- Module: Mathlib.RingTheory.Localization.AtPrime.Extension
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
Rₚ : Type u_3
inst_4 : CommRing Rₚ
inst_5 : Algebra R Rₚ
inst_6 : IsLocalization.AtPrime Rₚ p
inst_7 : IsLocalRing Rₚ
Sₚ : Type u_4
inst_8 : CommRing Sₚ
inst_9 : Algebra S Sₚ
inst_10 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst_11 : Algebra Rₚ Sₚ
P : Ideal S
hPp : P.LiesOver p
inst_12 : Algebra R Sₚ
inst_13 : IsScalarTower R S Sₚ
inst_14 : IsScalarTower R Rₚ Sₚ
inst_15 : IsDomain R
inst_16 : IsTorsionFree R S
inst_17 : IsTorsionFree R Rₚ
inst_18 : IsTorsionFree S Sₚ
inst_19 : IsTorsionFree Rₚ Sₚ
inst_20 : IsDedekindDomain S
inst_21 : IsDedekindDomain Rₚ
inst_22 : IsDedekindDomain Sₚ
hp : p ≠ ⊥
inst_23 : P.IsPrime
h₁ : Ne (α := Ideal Rₚ) (maximalIdeal Rₚ) ⊥
this : IsPrime.{u_4} (α := Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
hP : ¬P = ⊥
⊢ P.IsMaximal

Tactic:
have : P.IsMaximal := IsPrime.isMaximal inferInstance hP
-- Module: Mathlib.RingTheory.Localization.AtPrime.Extension
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
Rₚ : Type u_3
inst_4 : CommRing Rₚ
inst_5 : Algebra R Rₚ
inst_6 : IsLocalization.AtPrime Rₚ p
inst_7 : IsLocalRing Rₚ
Sₚ : Type u_4
inst_8 : CommRing Sₚ
inst_9 : Algebra S Sₚ
inst_10 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst_11 : Algebra Rₚ Sₚ
P : Ideal S
hPp : P.LiesOver p
inst_12 : Algebra R Sₚ
inst_13 : IsScalarTower R S Sₚ
inst_14 : IsScalarTower R Rₚ Sₚ
inst_15 : IsDomain R
inst_16 : IsTorsionFree R S
inst_17 : IsTorsionFree R Rₚ
inst_18 : IsTorsionFree S Sₚ
inst_19 : IsTorsionFree Rₚ Sₚ
inst_20 : IsDedekindDomain S
inst_21 : IsDedekindDomain Rₚ
inst_22 : IsDedekindDomain Sₚ
hp : p ≠ ⊥
inst_23 : P.IsPrime
h₁ : Ne (α := Ideal Rₚ) (maximalIdeal Rₚ) ⊥
this_1 : IsPrime.{u_4} (α := Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
hP : ¬P = ⊥
this : P.IsMaximal
⊢ LiesOver.{u_3, u_4} (B := Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) (maximalIdeal Rₚ)

Tactic:
have : (Ideal.map (algebraMap S Sₚ) P).LiesOver (maximalIdeal Rₚ) :=
    liesOver_map_of_liesOver p Rₚ Sₚ P
-- Module: Mathlib.RingTheory.Localization.AtPrime.Extension
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
Rₚ : Type u_3
inst_4 : CommRing Rₚ
inst_5 : Algebra R Rₚ
inst_6 : IsLocalization.AtPrime Rₚ p
inst_7 : IsLocalRing Rₚ
Sₚ : Type u_4
inst_8 : CommRing Sₚ
inst_9 : Algebra S Sₚ
inst_10 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst_11 : Algebra Rₚ Sₚ
P : Ideal S
hPp : P.LiesOver p
inst_12 : Algebra R Sₚ
inst_13 : IsScalarTower R S Sₚ
inst_14 : IsScalarTower R Rₚ Sₚ
inst_15 : IsDomain R
inst_16 : IsTorsionFree R S
inst_17 : IsTorsionFree R Rₚ
inst_18 : IsTorsionFree S Sₚ
inst_19 : IsTorsionFree Rₚ Sₚ
inst_20 : IsDedekindDomain S
inst_21 : IsDedekindDomain Rₚ
inst_22 : IsDedekindDomain Sₚ
hp : p ≠ ⊥
inst_23 : P.IsPrime
h₁ : Ne (α := Ideal Rₚ) (maximalIdeal Rₚ) ⊥
this_1 : IsPrime.{u_4} (α := Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
hP : ¬P = ⊥
this_2 : P.IsMaximal
this : LiesOver.{u_3, u_4} (B := Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) (maximalIdeal Rₚ)
rw : P = under.{u_2, u_4} S (B := Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
rw₁ : P = comap (F := S →+* Sₚ) (algebraMap S Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
rw₂ rw₃ : P = P
⊢ LiesOver.{u_2, u_4} (B := Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) P

Tactic:
rw [liesOver_iff, under_def, comap_map_eq_self_of_isMaximal _ (IsPrime.ne_top')]

Premises used: Ideal.liesOver_iff, Ideal.under_def, Ideal.comap_map_eq_self_of_isMaximal, Ideal.IsPrime.ne_top'
-- Module: Mathlib.RingTheory.Localization.AtPrime.Extension
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
Rₚ : Type u_3
inst_4 : CommRing Rₚ
inst_5 : Algebra R Rₚ
inst_6 : IsLocalization.AtPrime Rₚ p
inst_7 : IsLocalRing Rₚ
Sₚ : Type u_4
inst_8 : CommRing Sₚ
inst_9 : Algebra S Sₚ
inst_10 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst_11 : Algebra Rₚ Sₚ
P : Ideal S
hPp : P.LiesOver p
inst_12 : Algebra R Sₚ
inst_13 : IsScalarTower R S Sₚ
inst_14 : IsScalarTower R Rₚ Sₚ
inst_15 : IsDomain R
inst_16 : IsTorsionFree R S
inst_17 : IsTorsionFree R Rₚ
inst_18 : IsTorsionFree S Sₚ
inst_19 : IsTorsionFree Rₚ Sₚ
inst_20 : IsDedekindDomain S
inst_21 : IsDedekindDomain Rₚ
inst_22 : IsDedekindDomain Sₚ
hp : p ≠ ⊥
inst_23 : P.IsPrime
h₁ : Ne (α := Ideal Rₚ) (maximalIdeal Rₚ) ⊥
this_1 : IsPrime.{u_4} (α := Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
hP : ¬P = ⊥
this_2 : P.IsMaximal
this : LiesOver.{u_3, u_4} (B := Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) (maximalIdeal Rₚ)
⊢ LiesOver.{u_2, u_4} (B := Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) P

Tactic:
have : (Ideal.map (algebraMap S Sₚ) P).LiesOver P := by
    rw [liesOver_iff, under_def, comap_map_eq_self_of_isMaximal _ (IsPrime.ne_top')]
-- Module: Mathlib.RingTheory.Localization.AtPrime.Extension
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
Rₚ : Type u_3
inst_4 : CommRing Rₚ
inst_5 : Algebra R Rₚ
inst_6 : IsLocalization.AtPrime Rₚ p
inst_7 : IsLocalRing Rₚ
Sₚ : Type u_4
inst_8 : CommRing Sₚ
inst_9 : Algebra S Sₚ
inst_10 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst_11 : Algebra Rₚ Sₚ
P : Ideal S
hPp : P.LiesOver p
inst_12 : Algebra R Sₚ
inst_13 : IsScalarTower R S Sₚ
inst_14 : IsScalarTower R Rₚ Sₚ
inst_15 : IsDomain R
inst_16 : IsTorsionFree R S
inst_17 : IsTorsionFree R Rₚ
inst_18 : IsTorsionFree S Sₚ
inst_19 : IsTorsionFree Rₚ Sₚ
inst_20 : IsDedekindDomain S
inst_21 : IsDedekindDomain Rₚ
inst_22 : IsDedekindDomain Sₚ
hp : p ≠ ⊥
inst_23 : P.IsPrime
h₁ : Ne (α := Ideal Rₚ) (maximalIdeal Rₚ) ⊥
this_1 : IsPrime.{u_4} (α := Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
hP : ¬P = ⊥
this_2 : P.IsMaximal
this_3 : LiesOver.{u_3, u_4} (B := Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) (maximalIdeal Rₚ)
this : LiesOver.{u_2, u_4} (B := Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) P
⊢ p.ramificationIdx (maximalIdeal Rₚ) *
      ramificationIdx.{u_3, u_4} (S := Sₚ) (maximalIdeal Rₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) =
    p.ramificationIdx P * ramificationIdx.{u_2, u_4} (S := Sₚ) P (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)

Tactic:
have h_main :=
  (ramificationIdx_algebra_tower' p (maximalIdeal Rₚ) (Ideal.map (algebraMap S Sₚ) P)).symm.trans
    <| ramificationIdx_algebra_tower' p P (Ideal.map (algebraMap S Sₚ) P)
-- Module: Mathlib.RingTheory.Localization.AtPrime.Extension
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
Rₚ : Type u_3
inst_4 : CommRing Rₚ
inst_5 : Algebra R Rₚ
inst_6 : IsLocalization.AtPrime Rₚ p
inst_7 : IsLocalRing Rₚ
Sₚ : Type u_4
inst_8 : CommRing Sₚ
inst_9 : Algebra S Sₚ
inst_10 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst_11 : Algebra Rₚ Sₚ
P : Ideal S
hPp : P.LiesOver p
inst_12 : Algebra R Sₚ
inst_13 : IsScalarTower R S Sₚ
inst_14 : IsScalarTower R Rₚ Sₚ
inst_15 : IsDomain R
inst_16 : IsTorsionFree R S
inst_17 : IsTorsionFree R Rₚ
inst_18 : IsTorsionFree S Sₚ
inst_19 : IsTorsionFree Rₚ Sₚ
inst_20 : IsDedekindDomain S
inst_21 : IsDedekindDomain Rₚ
inst_22 : IsDedekindDomain Sₚ
hp : p ≠ ⊥
inst_23 : P.IsPrime
h₁ : Ne (α := Ideal Rₚ) (maximalIdeal Rₚ) ⊥
this_1 : IsPrime.{u_4} (α := Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
hP : ¬P = ⊥
this_2 : P.IsMaximal
this_3 : LiesOver.{u_3, u_4} (B := Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) (maximalIdeal Rₚ)
this : LiesOver.{u_2, u_4} (B := Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) P
h_main :
  p.ramificationIdx (maximalIdeal Rₚ) *
      ramificationIdx.{u_3, u_4} (S := Sₚ) (maximalIdeal Rₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) =
    p.ramificationIdx P * ramificationIdx.{u_2, u_4} (S := Sₚ) P (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
rwa :
  ∀
    (h_main :
      ramificationIdx.{u_1, u_3} (S := Rₚ) p (Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) p) *
          ramificationIdx.{u_3, u_4} (R := Rₚ) (S := Sₚ) (Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) p)
            (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) =
        p.ramificationIdx P),
    Ne.{u_3 + 1} (α := Ideal Rₚ) (Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) p) ⊤
⊢ ramificationIdx.{u_3, u_4} (S := Sₚ) (maximalIdeal Rₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) =
    p.ramificationIdx P

Tactic:
rwa [ramificationIdx_map_self_eq_one IsPrime.ne_top' (map_ne_bot_of_ne_bot hP), mul_one,
    ← map_eq_maximalIdeal p, ramificationIdx_map_self_eq_one _ (map_ne_bot_of_ne_bot hp), one_mul,
    map_eq_maximalIdeal p] at h_main

Premises used: IsLocalization.AtPrime.map_eq_maximalIdeal, Ideal.map_ne_bot_of_ne_bot, mul_one, Ideal.IsPrime.ne_top', one_mul, Ideal.ramificationIdx_map_self_eq_one