awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Extension (hypothesis)
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ₚ) ⊥
⊢ ramificationIdx.{u_3, u_4} (S := Sₚ) (maximalIdeal Rₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) =
    p.ramificationIdx P
have this : 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
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Extension (goal)
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)
⊢ ramificationIdx.{u_3, u_4} (S := Sₚ) (maximalIdeal Rₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) =
    p.ramificationIdx P
have pos : ∀ (hP : 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 = ⊥
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Extension (goal)
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
⊢ ramificationIdx.{u_3, u_4} (S := Sₚ) (maximalIdeal Rₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) =
    p.ramificationIdx P
have neg : ∀ (hP : ¬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 = ⊥
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Extension (goal)
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 = ⊥
⊢ ramificationIdx.{u_3, u_4} (S := Sₚ) (maximalIdeal Rₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) =
    p.ramificationIdx P
have 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 ⊥
Tactic: simp_rw [hP, Ideal.map_bot, ramificationIdx_bot' hp
      (FaithfulSMul.algebraMap_injective _ _),
      ramificationIdx_bot' h₁ (FaithfulSMul.algebraMap_injective Rₚ Sₚ)]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Extension (goal)
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 ⊥
⊢ ramificationIdx.{u_3, u_4} (S := Sₚ) (maximalIdeal Rₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) =
    p.ramificationIdx P
have pos₁ : ramificationIdx.{u_3, u_4} (S := Sₚ) (maximalIdeal Rₚ) ⊥ = ramificationIdx.{u_1, u_2} (S := S) p ⊥
Tactic: simp_rw [hP, Ideal.map_bot, ramificationIdx_bot' hp
      (FaithfulSMul.algebraMap_injective _ _),
      ramificationIdx_bot' h₁ (FaithfulSMul.algebraMap_injective Rₚ Sₚ)]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Extension (goal)
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 ⊥
⊢ ramificationIdx.{u_3, u_4} (S := Sₚ) (maximalIdeal Rₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) =
    p.ramificationIdx P
have pos₂ : ramificationIdx.{u_3, u_4} (S := Sₚ) (maximalIdeal Rₚ) ⊥ = 0
Tactic: simp_rw [hP, Ideal.map_bot, ramificationIdx_bot' hp
      (FaithfulSMul.algebraMap_injective _ _),
      ramificationIdx_bot' h₁ (FaithfulSMul.algebraMap_injective Rₚ Sₚ)]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Extension (hypothesis)
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 = ⊥
⊢ ramificationIdx.{u_3, u_4} (S := Sₚ) (maximalIdeal Rₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) =
    p.ramificationIdx P
have this₁ : P.IsMaximal
Tactic: have : P.IsMaximal := IsPrime.isMaximal inferInstance hP
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Extension (hypothesis)
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
⊢ ramificationIdx.{u_3, u_4} (S := Sₚ) (maximalIdeal Rₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) =
    p.ramificationIdx P
have this₁ : 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
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Extension (goal)
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
have rw : P = under.{u_2, u_4} S (B := Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
Tactic: rw [liesOver_iff, under_def, comap_map_eq_self_of_isMaximal _ (IsPrime.ne_top')]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Extension (goal)
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)
⊢ LiesOver.{u_2, u_4} (B := Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) P
have rw₁ : P = comap (F := S →+* Sₚ) (algebraMap S Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
Tactic: rw [liesOver_iff, under_def, comap_map_eq_self_of_isMaximal _ (IsPrime.ne_top')]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Extension (goal)
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)
⊢ LiesOver.{u_2, u_4} (B := Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) P
have rw₂ : P = P
Tactic: rw [liesOver_iff, under_def, comap_map_eq_self_of_isMaximal _ (IsPrime.ne_top')]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Extension (hypothesis)
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ₚ)
⊢ ramificationIdx.{u_3, u_4} (S := Sₚ) (maximalIdeal Rₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) =
    p.ramificationIdx P
have this₁ : 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')]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Extension (hypothesis)
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
⊢ ramificationIdx.{u_3, u_4} (S := Sₚ) (maximalIdeal Rₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) =
    p.ramificationIdx P
have 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)
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)
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Extension (goal)
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)
⊢ ramificationIdx.{u_3, u_4} (S := Sₚ) (maximalIdeal Rₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) =
    p.ramificationIdx P
have 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) ⊤
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
Cleared hypotheses: h_main
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Extension (goal)
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.{u_3 + 1} (α := Ideal Rₚ) (Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) p) ⊤
have rw : Ne (α := Ideal Rₚ) (maximalIdeal Rₚ) ⊤
Tactic: rw [map_eq_maximalIdeal]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Extension (hypothesis)
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)
⊢ (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
have this : (↑P : Ideal S).IsMaximal
Tactic: have : P.val.IsMaximal := Ring.DimensionLEOne.maximalOfPrime
      (ne_bot_of_mem_primesOver hp P.prop) (primesOver.isPrime p P)