awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : P.IsMaximal
rw :
  P =
    RingHom.ker (F :=
      RingHom.{u_2, u_4} S (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)))
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
          (algebraMap Sₚ (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)))
          (algebraMap S Sₚ) :
        RingHom.{u_2, u_4} S (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)))
rw₁ :
  P =
    comap (F := S →+* Sₚ) (algebraMap S Sₚ : S →+* Sₚ)
      (RingHom.ker (F := Sₚ →+* HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
        (algebraMap Sₚ (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))))
⊢ P =
    RingHom.ker (F :=
      RingHom.{u_2, u_4} S (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)))
      (algebraMap S (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)) :
        RingHom.{u_2, u_4} S (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)))
have rw₂ : P =
  comap (F := S →+* Sₚ) (algebraMap S Sₚ : S →+* Sₚ)
    (RingHom.ker (F := Sₚ →+* HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
      (Ideal.Quotient.mk (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)))
Tactic: rw [IsScalarTower.algebraMap_eq S Sₚ (Sₚ ⧸ _), ← RingHom.comap_ker, Quotient.algebraMap_eq,
        mk_ker, comap_map_eq_self_of_isMaximal _ (isPrime_map_of_liesOver S p Sₚ P).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 : P.IsMaximal
rw :
  P =
    RingHom.ker (F :=
      RingHom.{u_2, u_4} S (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)))
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
          (algebraMap Sₚ (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)))
          (algebraMap S Sₚ) :
        RingHom.{u_2, u_4} S (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)))
rw₁ :
  P =
    comap (F := S →+* Sₚ) (algebraMap S Sₚ : S →+* Sₚ)
      (RingHom.ker (F := Sₚ →+* HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
        (algebraMap Sₚ (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))))
rw₂ :
  P =
    comap (F := S →+* Sₚ) (algebraMap S Sₚ : S →+* Sₚ)
      (RingHom.ker (F := Sₚ →+* HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
        (Ideal.Quotient.mk (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)))
⊢ P =
    RingHom.ker (F :=
      RingHom.{u_2, u_4} S (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)))
      (algebraMap S (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)) :
        RingHom.{u_2, u_4} S (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)))
have rw₃ : P = comap (F := S →+* Sₚ) (algebraMap S Sₚ : S →+* Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
Tactic: rw [IsScalarTower.algebraMap_eq S Sₚ (Sₚ ⧸ _), ← RingHom.comap_ker, Quotient.algebraMap_eq,
        mk_ker, comap_map_eq_self_of_isMaximal _ (isPrime_map_of_liesOver S p Sₚ P).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 : P.IsMaximal
rw :
  P =
    RingHom.ker (F :=
      RingHom.{u_2, u_4} S (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)))
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
          (algebraMap Sₚ (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)))
          (algebraMap S Sₚ) :
        RingHom.{u_2, u_4} S (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)))
rw₁ :
  P =
    comap (F := S →+* Sₚ) (algebraMap S Sₚ : S →+* Sₚ)
      (RingHom.ker (F := Sₚ →+* HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
        (algebraMap Sₚ (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))))
rw₂ :
  P =
    comap (F := S →+* Sₚ) (algebraMap S Sₚ : S →+* Sₚ)
      (RingHom.ker (F := Sₚ →+* HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
        (Ideal.Quotient.mk (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)))
rw₃ : P = comap (F := S →+* Sₚ) (algebraMap S Sₚ : S →+* Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
⊢ P =
    RingHom.ker (F :=
      RingHom.{u_2, u_4} S (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)))
      (algebraMap S (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)) :
        RingHom.{u_2, u_4} S (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)))
have rw₄ : P = P
Tactic: rw [IsScalarTower.algebraMap_eq S Sₚ (Sₚ ⧸ _), ← RingHom.comap_ker, Quotient.algebraMap_eq,
        mk_ker, comap_map_eq_self_of_isMaximal _ (isPrime_map_of_liesOver S p Sₚ P).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
Sₚ : Type u_4
inst_4 : CommRing Sₚ
inst_5 : Algebra S Sₚ
inst_6 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
P : Ideal S
hPp : P.LiesOver p
inst_7 : P.IsMaximal
x : S
s : ↥(algebraMapSubmonoid S p.primeCompl)
⊢ ((RingEquiv.symm (equivQuotientMapOfIsMaximal p Sₚ P) :
          RingEquiv.{u_4, u_2} (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
            (S ⧸ P)) :
        (a : Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P) → S ⧸ P)
      ((Ideal.Quotient.mk (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) :
          (a : Sₚ) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
        (mk' Sₚ x s)) =
    HMul.hMul (α := S ⧸ P) (β := S ⧸ P) ((Ideal.Quotient.mk P : (a : S) → S ⧸ P) x : S ⧸ P)
      (((Ideal.Quotient.mk P : (a : S) → S ⧸ P) (↑s : S))⁻¹ : S ⧸ P)
have this : IsPrime.{u_4} (α := Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
Tactic: have : (Ideal.map (algebraMap S Sₚ) P).IsPrime := isPrime_map_of_liesOver S p Sₚ P
-- 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
Sₚ : Type u_4
inst_4 : CommRing Sₚ
inst_5 : Algebra S Sₚ
inst_6 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
P : Ideal S
hPp : P.LiesOver p
inst_7 : P.IsMaximal
x : S
s : ↥(algebraMapSubmonoid S p.primeCompl)
this : IsPrime.{u_4} (α := Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
⊢ ((RingEquiv.symm (equivQuotientMapOfIsMaximal p Sₚ P) :
          RingEquiv.{u_4, u_2} (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
            (S ⧸ P)) :
        (a : Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P) → S ⧸ P)
      ((Ideal.Quotient.mk (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) :
          (a : Sₚ) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
        (mk' Sₚ x s)) =
    HMul.hMul (α := S ⧸ P) (β := S ⧸ P) ((Ideal.Quotient.mk P : (a : S) → S ⧸ P) x : S ⧸ P)
      (((Ideal.Quotient.mk P : (a : S) → S ⧸ P) (↑s : S))⁻¹ : S ⧸ P)
have h₁ : Ne (α := S ⧸ P) ((Ideal.Quotient.mk P : (a : S) → S ⧸ P) (↑s : S) : S ⧸ P) (0 : S ⧸ P)
Tactic: have h₁ : Ideal.Quotient.mk P ↑s ≠ 0 :=
    Quotient.eq_zero_iff_mem.not.mpr <|
      (Set.disjoint_left.mp <| disjoint_primeCompl_of_liesOver P p) s.prop
-- 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
Sₚ : Type u_4
inst_4 : CommRing Sₚ
inst_5 : Algebra S Sₚ
inst_6 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
P : Ideal S
hPp : P.LiesOver p
inst_7 : P.IsMaximal
x : S
s : ↥(algebraMapSubmonoid S p.primeCompl)
this : IsPrime.{u_4} (α := Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
h₁ : Ne (α := S ⧸ P) ((Ideal.Quotient.mk P : (a : S) → S ⧸ P) (↑s : S) : S ⧸ P) (0 : S ⧸ P)
⊢ ((RingEquiv.symm (equivQuotientMapOfIsMaximal p Sₚ P) :
          RingEquiv.{u_4, u_2} (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
            (S ⧸ P)) :
        (a : Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P) → S ⧸ P)
      ((Ideal.Quotient.mk (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) :
          (a : Sₚ) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
        (mk' Sₚ x s)) =
    HMul.hMul (α := S ⧸ P) (β := S ⧸ P) ((Ideal.Quotient.mk P : (a : S) → S ⧸ P) x : S ⧸ P)
      (((Ideal.Quotient.mk P : (a : S) → S ⧸ P) (↑s : S))⁻¹ : S ⧸ P)
have h₂ : Ne.{u_4 + 1} (α := HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
  (((equivQuotientMapOfIsMaximal p Sₚ P :
          RingEquiv.{u_2, u_4} (S ⧸ P)
            (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))) :
        (a : S ⧸ P) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
      ((Ideal.Quotient.mk P : (a : S) → S ⧸ P) (↑s : S)) :
    HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
  (0 : HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
Tactic: have h₂ : equivQuotientMapOfIsMaximal p Sₚ P (Ideal.Quotient.mk P ↑s) ≠ 0 := by
    rwa [RingEquiv.map_ne_zero_iff]
-- 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
Sₚ : Type u_4
inst_4 : CommRing Sₚ
inst_5 : Algebra S Sₚ
inst_6 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
P : Ideal S
hPp : P.LiesOver p
inst_7 : P.IsMaximal
x : S
s : ↥(algebraMapSubmonoid S p.primeCompl)
this : IsPrime.{u_4} (α := Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
h₁ : Ne (α := S ⧸ P) ((Ideal.Quotient.mk P : (a : S) → S ⧸ P) (↑s : S) : S ⧸ P) (0 : S ⧸ P)
h₂ :
  Ne.{u_4 + 1} (α := HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
    (((equivQuotientMapOfIsMaximal p Sₚ P :
            RingEquiv.{u_2, u_4} (S ⧸ P)
              (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))) :
          (a : S ⧸ P) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
        ((Ideal.Quotient.mk P : (a : S) → S ⧸ P) (↑s : S)) :
      HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
    (0 : HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
⊢ ((RingEquiv.symm (equivQuotientMapOfIsMaximal p Sₚ P) :
          RingEquiv.{u_4, u_2} (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
            (S ⧸ P)) :
        (a : Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P) → S ⧸ P)
      ((Ideal.Quotient.mk (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) :
          (a : Sₚ) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
        (mk' Sₚ x s)) =
    HMul.hMul (α := S ⧸ P) (β := S ⧸ P) ((Ideal.Quotient.mk P : (a : S) → S ⧸ P) x : S ⧸ P)
      (((Ideal.Quotient.mk P : (a : S) → S ⧸ P) (↑s : S))⁻¹ : S ⧸ P)
have rw : Eq (α := HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
  ((Ideal.Quotient.mk (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) : (a : Sₚ) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
      (mk' Sₚ x s) :
    HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
  (((equivQuotientMapOfIsMaximal p Sₚ P :
          RingEquiv.{u_2, u_4} (S ⧸ P)
            (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))) :
        (a : S ⧸ P) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
      (HMul.hMul (α := S ⧸ P) (β := S ⧸ P) ((Ideal.Quotient.mk P : (a : S) → S ⧸ P) x : S ⧸ P)
        (((Ideal.Quotient.mk P : (a : S) → S ⧸ P) (↑s : S))⁻¹ : S ⧸ P)) :
    HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
Tactic: rw [RingEquiv.symm_apply_eq, ← mul_left_inj' h₂, map_mul, mul_assoc, ← map_mul,
    inv_mul_cancel₀ h₁, map_one, mul_one, equivQuotientMapOfIsMaximal_apply_mk,
    ← map_mul, mk'_spec, Quotient.mk_algebraMap, equivQuotientMapOfIsMaximal_apply_mk,
    Quotient.mk_algebraMap]
-- 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 : 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 : HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ)
⊢ Eq.{u_2 + 1} (α := S ⧸ P)
    ((algebraMap (R ⧸ p) (S ⧸ P) : (a : R ⧸ p) → S ⧸ P)
        (((RingEquiv.symm (equivQuotMaximalIdeal p Rₚ) :
              RingEquiv.{u_3, u_1} (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ)) (R ⧸ p)) :
            (a : Rₚ ⧸ maximalIdeal Rₚ) → R ⧸ p)
          x) :
      S ⧸ P)
    (((RingEquiv.symm (equivQuotientMapOfIsMaximal p Sₚ P) :
            RingEquiv.{u_4, u_2}
              (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)) (S ⧸ P)) :
          (a : Sₚ ⧸ Ideal.map (algebraMap S Sₚ) 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)) :
            (a : Rₚ ⧸ maximalIdeal Rₚ) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
          x) :
      S ⧸ P)
have obtain : ∀ (x : Rₚ),
  Eq.{u_2 + 1} (α := S ⧸ P)
    ((algebraMap (R ⧸ p) (S ⧸ P) : (a : R ⧸ p) → S ⧸ P)
        (((RingEquiv.symm (equivQuotMaximalIdeal p Rₚ) :
              RingEquiv.{u_3, u_1} (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ)) (R ⧸ p)) :
            (a : Rₚ ⧸ maximalIdeal Rₚ) → R ⧸ p)
          ((Ideal.Quotient.mk (maximalIdeal Rₚ) : (a : Rₚ) → Rₚ ⧸ maximalIdeal Rₚ) x)) :
      S ⧸ P)
    (((RingEquiv.symm (equivQuotientMapOfIsMaximal p Sₚ P) :
            RingEquiv.{u_4, u_2}
              (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)) (S ⧸ P)) :
          (a : Sₚ ⧸ Ideal.map (algebraMap S Sₚ) 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)) :
            (a : Rₚ ⧸ maximalIdeal Rₚ) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
          ((Ideal.Quotient.mk (maximalIdeal Rₚ) : (a : Rₚ) → Rₚ ⧸ maximalIdeal Rₚ) x)) :
      S ⧸ P)
Tactic: obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
Cleared hypotheses: x
-- 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 : 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ₚ)
⊢ inertiaDeg.{u_3, u_4} (S := Sₚ) (maximalIdeal Rₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) = p.inertiaDeg P
have rw : finrank.{u_3, u_4} (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
    (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)) =
  finrank.{u_1, u_2} (R ⧸ p) (S ⧸ P)
Tactic: rw [inertiaDeg_algebraMap, inertiaDeg_algebraMap]
-- 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 : 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ₚ)
⊢ finrank.{u_3, u_4} (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
      (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)) =
    finrank.{u_1, u_2} (R ⧸ p) (S ⧸ P)
have refine : 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: refine Algebra.finrank_eq_of_equiv_equiv (equivQuotMaximalIdeal p Rₚ).symm
    (equivQuotientMapOfIsMaximal p Sₚ P).symm ?_
-- 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 : 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ₚ)
⊢ 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))))
have 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)
Tactic: ext x
-- 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
⊢ Ne (α := Ideal Rₚ) (maximalIdeal Rₚ) ⊥
have rw : Ne.{u_3 + 1} (α := Ideal Rₚ) (Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) p) ⊥
Tactic: rw [← map_eq_maximalIdeal p]
-- 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
⊢ ramificationIdx.{u_3, u_4} (S := Sₚ) (maximalIdeal Rₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) =
    p.ramificationIdx P
have h₁ : Ne (α := Ideal Rₚ) (maximalIdeal Rₚ) ⊥
Tactic: have h₁ : maximalIdeal Rₚ ≠ ⊥ := by
    rw [← map_eq_maximalIdeal p]
    exact map_ne_bot_of_ne_bot hp