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 : 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 :
  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
rw : Ne (α := Ideal Rₚ) (maximalIdeal Rₚ) ⊤
⊢ Ne.{u_3 + 1} (α := Ideal Rₚ) (Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) p) ⊤

Tactic:
rw [map_eq_maximalIdeal]

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
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 :
  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 (α := Ideal Rₚ) (maximalIdeal Rₚ) ⊤

Tactic:
IsPrime.ne_top'

Premises used: 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_1 : Ideal S
hPp : P_1.LiesOver p
inst_12 : IsDomain R
inst_13 : IsDedekindDomain S
inst_14 : IsTorsionFree R S
inst_15 : Algebra R Sₚ
inst_16 : IsScalarTower R S Sₚ
inst_17 : IsScalarTower R Rₚ Sₚ
hp : p ≠ ⊥
P : (↑(p.primesOver S) : Type u_2)
⊢ (↑P : Ideal S).IsMaximal

Tactic:
have : P.val.IsMaximal := Ring.DimensionLEOne.maximalOfPrime
      (ne_bot_of_mem_primesOver hp P.prop) (primesOver.isPrime p 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_1 : Ideal S
hPp : P_1.LiesOver p
inst_12 : IsDomain R
inst_13 : IsDedekindDomain S
inst_14 : IsTorsionFree R S
inst_15 : Algebra R Sₚ
inst_16 : IsScalarTower R S Sₚ
inst_17 : IsScalarTower R Rₚ Sₚ
hp : p ≠ ⊥
P : (↑(p.primesOver S) : Type u_2)
this : (↑P : Ideal S).IsMaximal
⊢ (fun (Q : (↑(primesOver (maximalIdeal Rₚ) Sₚ) : Type u_4)) ↦
        (Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Set (Ideal S)) (p.primesOver S) x)
            (comap (F := S →+* Sₚ) (algebraMap S Sₚ) (↑Q : Ideal Sₚ)) ⋯ :
          { x : Ideal S // Membership.mem (γ := Set (Ideal S)) (p.primesOver S) x }))
      ((fun (P : (↑(p.primesOver S) : Type u_2)) ↦
          (Subtype.mk (p := fun (x : Ideal Sₚ) ↦
              Membership.mem (γ := Set (Ideal Sₚ)) (primesOver (maximalIdeal Rₚ) Sₚ) x)
              (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) (↑P : Ideal S)) ⋯ :
            { x : Ideal Sₚ // Membership.mem (γ := Set (Ideal Sₚ)) (primesOver (maximalIdeal Rₚ) Sₚ) x }))
        P) =
    P

Tactic:
SetCoe.ext <| IsLocalization.AtPrime.under_map_of_isMaximal S p Sₚ P.1

Premises used: SetCoe.ext, IsLocalization.AtPrime.under_map_of_isMaximal, Subtype.val
-- 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_1 : Ideal S
hPp : P_1.LiesOver p
inst_12 : IsDomain R
inst_13 : IsDedekindDomain S
inst_14 : IsTorsionFree R S
inst_15 : Algebra R Sₚ
inst_16 : IsScalarTower R S Sₚ
inst_17 : IsScalarTower R Rₚ Sₚ
hp : p ≠ ⊥
P : (↑(p.primesOver S) : Type u_2)
this : (↑P : Ideal S).IsMaximal
⊢ (fun (Q : (↑(primesOver (maximalIdeal Rₚ) Sₚ) : Type u_4)) ↦
        (Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Set (Ideal S)) (p.primesOver S) x)
            (comap (F := S →+* Sₚ) (algebraMap S Sₚ) (↑Q : Ideal Sₚ)) ⋯ :
          { x : Ideal S // Membership.mem (γ := Set (Ideal S)) (p.primesOver S) x }))
      ((fun (P : (↑(p.primesOver S) : Type u_2)) ↦
          (Subtype.mk (p := fun (x : Ideal Sₚ) ↦
              Membership.mem (γ := Set (Ideal Sₚ)) (primesOver (maximalIdeal Rₚ) Sₚ) x)
              (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) (↑P : Ideal S)) ⋯ :
            { x : Ideal Sₚ // Membership.mem (γ := Set (Ideal Sₚ)) (primesOver (maximalIdeal Rₚ) Sₚ) x }))
        P) =
    P

Tactic:
exact SetCoe.ext <| IsLocalization.AtPrime.under_map_of_isMaximal S p Sₚ P.1

Premises used: SetCoe.ext, IsLocalization.AtPrime.under_map_of_isMaximal, Subtype.val
-- 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 : IsDomain R
inst_13 : IsDedekindDomain S
inst_14 : IsTorsionFree R S
inst_15 : Algebra R Sₚ
inst_16 : IsScalarTower R S Sₚ
inst_17 : IsScalarTower R Rₚ Sₚ
hp : p ≠ ⊥
Q Q' : (↑(p.primesOver S) : Type u_2)
⊢ LE.le.{u_4} (α := (↑(primesOver (maximalIdeal Rₚ) Sₚ) : Type u_4))
      (({
              toFun := fun (P : (↑(p.primesOver S) : Type u_2)) ↦
                Subtype.mk (p := fun (x : Ideal Sₚ) ↦
                  Membership.mem (γ := Set (Ideal Sₚ)) (primesOver (maximalIdeal Rₚ) Sₚ) x)
                  (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) (↑P : Ideal S)) ⋯,
              invFun := fun (Q : (↑(primesOver (maximalIdeal Rₚ) Sₚ) : Type u_4)) ↦
                Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Set (Ideal S)) (p.primesOver S) x)
                  (comap (F := S →+* Sₚ) (algebraMap S Sₚ) (↑Q : Ideal Sₚ)) ⋯,
              left_inv := ⋯, right_inv := ⋯ } :
            (a : (↑(p.primesOver S) : Type u_2)) → (↑((maximalIdeal Rₚ).primesOver Sₚ) : Type u_4))
          Q :
        (↑(primesOver (maximalIdeal Rₚ) Sₚ) : Type u_4))
      (({
              toFun := fun (P : (↑(p.primesOver S) : Type u_2)) ↦
                Subtype.mk (p := fun (x : Ideal Sₚ) ↦
                  Membership.mem (γ := Set (Ideal Sₚ)) (primesOver (maximalIdeal Rₚ) Sₚ) x)
                  (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) (↑P : Ideal S)) ⋯,
              invFun := fun (Q : (↑(primesOver (maximalIdeal Rₚ) Sₚ) : Type u_4)) ↦
                Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Set (Ideal S)) (p.primesOver S) x)
                  (comap (F := S →+* Sₚ) (algebraMap S Sₚ) (↑Q : Ideal Sₚ)) ⋯,
              left_inv := ⋯, right_inv := ⋯ } :
            (a : (↑(p.primesOver S) : Type u_2)) → (↑((maximalIdeal Rₚ).primesOver Sₚ) : Type u_4))
          Q' :
        (↑(primesOver (maximalIdeal Rₚ) Sₚ) : Type u_4)) ↔
    Q ≤ Q'

Tactic:
⟨fun h ↦ ?_, fun h ↦ map_mono h⟩

Premises used: Iff.intro, Ideal.map_mono
-- 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 : IsDomain R
inst_13 : IsDedekindDomain S
inst_14 : IsTorsionFree R S
inst_15 : Algebra R Sₚ
inst_16 : IsScalarTower R S Sₚ
inst_17 : IsScalarTower R Rₚ Sₚ
hp : p ≠ ⊥
Q Q' : (↑(p.primesOver S) : Type u_2)
h :
  LE.le.{u_4} (α := (↑(primesOver (maximalIdeal Rₚ) Sₚ) : Type u_4))
    (({
            toFun := fun (P : (↑(p.primesOver S) : Type u_2)) ↦
              Subtype.mk (p := fun (x : Ideal Sₚ) ↦
                Membership.mem (γ := Set (Ideal Sₚ)) (primesOver (maximalIdeal Rₚ) Sₚ) x)
                (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) (↑P : Ideal S)) ⋯,
            invFun := fun (Q : (↑(primesOver (maximalIdeal Rₚ) Sₚ) : Type u_4)) ↦
              Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Set (Ideal S)) (p.primesOver S) x)
                (comap (F := S →+* Sₚ) (algebraMap S Sₚ) (↑Q : Ideal Sₚ)) ⋯,
            left_inv := ⋯, right_inv := ⋯ } :
          (a : (↑(p.primesOver S) : Type u_2)) → (↑((maximalIdeal Rₚ).primesOver Sₚ) : Type u_4))
        Q :
      (↑(primesOver (maximalIdeal Rₚ) Sₚ) : Type u_4))
    (({
            toFun := fun (P : (↑(p.primesOver S) : Type u_2)) ↦
              Subtype.mk (p := fun (x : Ideal Sₚ) ↦
                Membership.mem (γ := Set (Ideal Sₚ)) (primesOver (maximalIdeal Rₚ) Sₚ) x)
                (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) (↑P : Ideal S)) ⋯,
            invFun := fun (Q : (↑(primesOver (maximalIdeal Rₚ) Sₚ) : Type u_4)) ↦
              Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Set (Ideal S)) (p.primesOver S) x)
                (comap (F := S →+* Sₚ) (algebraMap S Sₚ) (↑Q : Ideal Sₚ)) ⋯,
            left_inv := ⋯, right_inv := ⋯ } :
          (a : (↑(p.primesOver S) : Type u_2)) → (↑((maximalIdeal Rₚ).primesOver Sₚ) : Type u_4))
        Q' :
      (↑(primesOver (maximalIdeal Rₚ) Sₚ) : Type u_4))
⊢ (↑Q' : Ideal S).IsMaximal

Tactic:
have : Q'.1.IsMaximal :=
      (primesOver.isPrime p Q').isMaximal (ne_bot_of_mem_primesOver hp Q'.prop)
-- 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 : IsDomain R
inst_13 : IsDedekindDomain S
inst_14 : IsTorsionFree R S
inst_15 : Algebra R Sₚ
inst_16 : IsScalarTower R S Sₚ
inst_17 : IsScalarTower R Rₚ Sₚ
hp : p ≠ ⊥
Q Q' : (↑(p.primesOver S) : Type u_2)
h :
  LE.le.{u_4} (α := (↑(primesOver (maximalIdeal Rₚ) Sₚ) : Type u_4))
    (({
            toFun := fun (P : (↑(p.primesOver S) : Type u_2)) ↦
              Subtype.mk (p := fun (x : Ideal Sₚ) ↦
                Membership.mem (γ := Set (Ideal Sₚ)) (primesOver (maximalIdeal Rₚ) Sₚ) x)
                (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) (↑P : Ideal S)) ⋯,
            invFun := fun (Q : (↑(primesOver (maximalIdeal Rₚ) Sₚ) : Type u_4)) ↦
              Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Set (Ideal S)) (p.primesOver S) x)
                (comap (F := S →+* Sₚ) (algebraMap S Sₚ) (↑Q : Ideal Sₚ)) ⋯,
            left_inv := ⋯, right_inv := ⋯ } :
          (a : (↑(p.primesOver S) : Type u_2)) → (↑((maximalIdeal Rₚ).primesOver Sₚ) : Type u_4))
        Q :
      (↑(primesOver (maximalIdeal Rₚ) Sₚ) : Type u_4))
    (({
            toFun := fun (P : (↑(p.primesOver S) : Type u_2)) ↦
              Subtype.mk (p := fun (x : Ideal Sₚ) ↦
                Membership.mem (γ := Set (Ideal Sₚ)) (primesOver (maximalIdeal Rₚ) Sₚ) x)
                (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) (↑P : Ideal S)) ⋯,
            invFun := fun (Q : (↑(primesOver (maximalIdeal Rₚ) Sₚ) : Type u_4)) ↦
              Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Set (Ideal S)) (p.primesOver S) x)
                (comap (F := S →+* Sₚ) (algebraMap S Sₚ) (↑Q : Ideal Sₚ)) ⋯,
            left_inv := ⋯, right_inv := ⋯ } :
          (a : (↑(p.primesOver S) : Type u_2)) → (↑((maximalIdeal Rₚ).primesOver Sₚ) : Type u_4))
        Q' :
      (↑(primesOver (maximalIdeal Rₚ) Sₚ) : Type u_4))
this : (↑Q' : Ideal S).IsMaximal
⊢ Q ≤ Q'

Tactic:
simpa [under_map_of_isMaximal S p] using le_comap_of_map_le h

Premises used: Ideal.le_comap_of_map_le, IsLocalization.AtPrime.under_map_of_isMaximal
-- 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ₚ
inst_12 : IsDomain R
inst_13 : IsDedekindDomain S
inst_14 : IsTorsionFree R S
inst_15 : Algebra R Sₚ
inst_16 : IsScalarTower R S Sₚ
inst_17 : IsScalarTower R Rₚ Sₚ
hp : p ≠ ⊥
P : (↑(p.primesOver S) : Type u_2)
⊢ Eq.{u_4 + 1} (α := Ideal Sₚ)
    (↑((primesOverEquivPrimesOver p Rₚ Sₚ hp :
            (a : (↑(p.primesOver S) : Type u_2)) → (↑((maximalIdeal Rₚ).primesOver Sₚ) : Type u_4))
          P) :
      Ideal Sₚ)
    (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) (↑P : Ideal S))

Tactic:
rfl

Premises used: Ideal.map, Submodule.span, rfl
-- 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ₚ
inst_12 : IsDomain R
inst_13 : IsDedekindDomain S
inst_14 : IsTorsionFree R S
inst_15 : Algebra R Sₚ
inst_16 : IsScalarTower R S Sₚ
inst_17 : IsScalarTower R Rₚ Sₚ
hp : p ≠ ⊥
Q : (↑(primesOver (maximalIdeal Rₚ) Sₚ) : Type u_4)
⊢ Eq (α := Ideal S)
    (↑((OrderIso.symm (primesOverEquivPrimesOver p Rₚ Sₚ hp) :
            (a : (↑((maximalIdeal Rₚ).primesOver Sₚ) : Type u_4)) → (↑(p.primesOver S) : Type u_2))
          Q) :
      Ideal S)
    (comap (F := S →+* Sₚ) (algebraMap S Sₚ) (↑Q : Ideal Sₚ))

Tactic:
rfl

Premises used: Ideal.comap, rfl
-- 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ₚ
inst_12 : IsDomain R
inst_13 : IsDedekindDomain S
inst_14 : IsTorsionFree R S
inst_15 : Algebra R Sₚ
inst_16 : IsScalarTower R S Sₚ
inst_17 : IsScalarTower R Rₚ Sₚ
inst_18 : p.IsMaximal
hp : p ≠ ⊥
P : (↑(p.primesOver S) : Type u_2)
⊢ NeZero p

Tactic:
have : NeZero p := ⟨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ₚ
inst_12 : IsDomain R
inst_13 : IsDedekindDomain S
inst_14 : IsTorsionFree R S
inst_15 : Algebra R Sₚ
inst_16 : IsScalarTower R S Sₚ
inst_17 : IsScalarTower R Rₚ Sₚ
inst_18 : p.IsMaximal
hp : p ≠ ⊥
P : (↑(p.primesOver S) : Type u_2)
this : NeZero p
⊢ (↑P : Ideal S).IsMaximal

Tactic:
have : P.val.IsMaximal := Ring.DimensionLEOne.maximalOfPrime
    (ne_bot_of_mem_primesOver (NeZero.ne _) P.prop) inferInstance
-- 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ₚ
inst_12 : IsDomain R
inst_13 : IsDedekindDomain S
inst_14 : IsTorsionFree R S
inst_15 : Algebra R Sₚ
inst_16 : IsScalarTower R S Sₚ
inst_17 : IsScalarTower R Rₚ Sₚ
inst_18 : p.IsMaximal
hp : p ≠ ⊥
P : (↑(p.primesOver S) : Type u_2)
this_1 : NeZero p
this : (↑P : Ideal S).IsMaximal
⊢ LiesOver.{u_3, u_4} (B := Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) (↑P : Ideal S)) (maximalIdeal Rₚ)

Tactic:
have : (P.1.map (algebraMap S Sₚ)).LiesOver (maximalIdeal Rₚ) := liesOver_map_of_liesOver 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ₚ
inst_12 : IsDomain R
inst_13 : IsDedekindDomain S
inst_14 : IsTorsionFree R S
inst_15 : Algebra R Sₚ
inst_16 : IsScalarTower R S Sₚ
inst_17 : IsScalarTower R Rₚ Sₚ
inst_18 : p.IsMaximal
hp : p ≠ ⊥
P : (↑(p.primesOver S) : Type u_2)
this_1 : NeZero p
this_2 : (↑P : Ideal S).IsMaximal
this : LiesOver.{u_3, u_4} (B := Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) (↑P : Ideal S)) (maximalIdeal Rₚ)
⊢ inertiaDeg.{u_3, u_4} (S := Sₚ) (maximalIdeal Rₚ)
      (↑((primesOverEquivPrimesOver p Rₚ Sₚ hp :
              (a : (↑(p.primesOver S) : Type u_2)) → (↑((maximalIdeal Rₚ).primesOver Sₚ) : Type u_4))
            P) :
        Ideal Sₚ) =
    p.inertiaDeg (↑P : Ideal S)

Tactic:
inertiaDeg_map_eq_inertiaDeg p _ _ _

Premises used: IsLocalization.AtPrime.inertiaDeg_map_eq_inertiaDeg, Ideal.map, Submodule.span
-- 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ₚ
inst_12 : IsDomain R
inst_13 : IsDedekindDomain S
inst_14 : IsTorsionFree R S
inst_15 : Algebra R Sₚ
inst_16 : IsScalarTower R S Sₚ
inst_17 : IsScalarTower R Rₚ Sₚ
inst_18 : p.IsMaximal
hp : p ≠ ⊥
P : (↑(p.primesOver S) : Type u_2)
this_1 : NeZero p
this_2 : (↑P : Ideal S).IsMaximal
this : LiesOver.{u_3, u_4} (B := Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) (↑P : Ideal S)) (maximalIdeal Rₚ)
⊢ inertiaDeg.{u_3, u_4} (S := Sₚ) (maximalIdeal Rₚ)
      (↑((primesOverEquivPrimesOver p Rₚ Sₚ hp :
              (a : (↑(p.primesOver S) : Type u_2)) → (↑((maximalIdeal Rₚ).primesOver Sₚ) : Type u_4))
            P) :
        Ideal Sₚ) =
    p.inertiaDeg (↑P : Ideal S)

Tactic:
exact inertiaDeg_map_eq_inertiaDeg p _ _ _

Premises used: IsLocalization.AtPrime.inertiaDeg_map_eq_inertiaDeg
-- 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ₚ
inst_12 : IsDomain R
inst_13 : IsDedekindDomain S
inst_14 : IsTorsionFree R S
inst_15 : Algebra R Sₚ
inst_16 : IsScalarTower R S Sₚ
inst_17 : IsScalarTower R Rₚ Sₚ
hp : p ≠ ⊥
inst_18 : NoZeroSMulDivisors R Rₚ
inst_19 : NoZeroSMulDivisors S Sₚ
inst_20 : NoZeroSMulDivisors Rₚ Sₚ
inst_21 : IsDedekindDomain Rₚ
inst_22 : IsDedekindDomain Sₚ
P : (↑(p.primesOver S) : Type u_2)
⊢ ramificationIdx.{u_3, u_4} (S := Sₚ) (maximalIdeal Rₚ)
      (↑((primesOverEquivPrimesOver p Rₚ Sₚ hp :
              (a : (↑(p.primesOver S) : Type u_2)) → (↑((maximalIdeal Rₚ).primesOver Sₚ) : Type u_4))
            P) :
        Ideal Sₚ) =
    p.ramificationIdx (↑P : Ideal S)

Tactic:
ramificationIdx_map_eq_ramificationIdx p _ _ _ hp

Premises used: Ideal.map, Submodule.span, IsLocalization.AtPrime.ramificationIdx_map_eq_ramificationIdx
-- Module: Mathlib.RingTheory.Localization.Away.AdjoinRoot
Goal:
R : Type u_1
inst : CommRing R
r : R
⊢ Eq (α := Away r)
    ((aeval (IsLocalization.Away.invSelf r) : (a : R[X]) → Away r)
        (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1) :
      Away r)
    (0 : Away r)

Tactic:
simp
-- Module: Mathlib.RingTheory.Localization.Away.AdjoinRoot
Goal:
R : Type u_1
inst : CommRing R
r : R
⊢ Away r (AdjoinRoot (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1))

Tactic:
IsLocalization.isLocalization_of_algEquiv _ (Localization.awayEquivAdjoin r)

Premises used: Localization.awayEquivAdjoin, IsLocalization.isLocalization_of_algEquiv
-- Module: Mathlib.RingTheory.Localization.Away.AdjoinRoot
Goal:
R : Type u_1
inst : CommRing R
r : R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Away r S
⊢ Algebra.FinitePresentation R S

Tactic:
(AdjoinRoot.finitePresentation _).equiv <|
    (Localization.awayEquivAdjoin r).symm.trans <| IsLocalization.algEquiv (Submonoid.powers r) _ _

Premises used: Algebra.FinitePresentation.equiv, AlgEquiv.symm, Localization.awayEquivAdjoin, AlgEquiv.trans, IsLocalization.algEquiv, Submonoid.powers