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
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)
s' : S
hs :
  Eq (α := S ⧸ P) ((Ideal.Quotient.mk P : (a : S) → S ⧸ P) s' : S ⧸ P)
    (((Ideal.Quotient.mk P : (a : S) → S ⧸ P) (↑s : S))⁻¹ : S ⧸ P)
h₀ : IsPrime.{u_4} (α := Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
⊢ (↑s : S) ∉ P

Tactic:
have h₁ : s.1 ∉ P := (Set.disjoint_left.mp <| disjoint_primeCompl_of_liesOver P p) s.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
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)
s' : S
hs :
  Eq (α := S ⧸ P) ((Ideal.Quotient.mk P : (a : S) → S ⧸ P) s' : S ⧸ P)
    (((Ideal.Quotient.mk P : (a : S) → S ⧸ P) (↑s : S))⁻¹ : S ⧸ P)
h₀ : IsPrime.{u_4} (α := Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
h₁ : (↑s : S) ∉ P
rwa : (↑s : S) ∉ comap (F := S →+* Sₚ) (algebraMap S Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
rwa₁ rwa₂ rwa₃ rwa₄ : (↑s : S) ∉ P
⊢ ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ) ∉ Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P

Tactic:
rwa [← mem_comap, comap_map_eq_self_of_isMaximal _ h₀.ne_top]

Premises used: Ideal.comap_map_eq_self_of_isMaximal, Ideal.IsPrime.ne_top, Ideal.mem_comap
-- 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
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)
s' : S
hs :
  Eq (α := S ⧸ P) ((Ideal.Quotient.mk P : (a : S) → S ⧸ P) s' : S ⧸ P)
    (((Ideal.Quotient.mk P : (a : S) → S ⧸ P) (↑s : S))⁻¹ : S ⧸ P)
h₀ : IsPrime.{u_4} (α := Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
h₁ : (↑s : S) ∉ P
⊢ ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ) ∉ Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P

Tactic:
have h₂ : algebraMap S Sₚ s ∉ Ideal.map (algebraMap S Sₚ) P := by
    rwa [← mem_comap, comap_map_eq_self_of_isMaximal _ h₀.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
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)
s' : S
hs :
  Eq (α := S ⧸ P) ((Ideal.Quotient.mk P : (a : S) → S ⧸ P) s' : S ⧸ P)
    (((Ideal.Quotient.mk P : (a : S) → S ⧸ P) (↑s : S))⁻¹ : S ⧸ P)
h₀ : IsPrime.{u_4} (α := Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
h₁ : (↑s : S) ∉ P
h₂ : ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ) ∉ Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P
⊢ Membership.mem (γ := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
    (HSub.hSub (α := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (x * s') : Sₚ) (mk' Sₚ x s))

Tactic:
(h₀.mem_or_mem ?_).resolve_left h₂

Premises used: Set.Mem, Or.resolve_left, Ideal.IsPrime.mem_or_mem
-- 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
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)
s' : S
hs :
  Eq (α := S ⧸ P) ((Ideal.Quotient.mk P : (a : S) → S ⧸ P) s' : S ⧸ P)
    (((Ideal.Quotient.mk P : (a : S) → S ⧸ P) (↑s : S))⁻¹ : S ⧸ P)
h₀ : IsPrime.{u_4} (α := Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
h₁ : (↑s : S) ∉ P
h₂ : ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ) ∉ Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P
h :
  Membership.mem (γ := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
    (HMul.hMul (α := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ)
      (HSub.hSub (α := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (x * s') : Sₚ) (mk' Sₚ x s)))
⊢ Membership.mem (γ := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
    (HSub.hSub (α := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (x * s') : Sₚ) (mk' Sₚ x s))

Tactic:
refine (h₀.mem_or_mem ?_).resolve_left h₂

Premises used: Or.resolve_left, Ideal.IsPrime.mem_or_mem
-- 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 : 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)
rw₄ rw₅ : P = 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)))

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]

Premises used: Ideal.Quotient.algebraMap_eq, RingHom.comap_ker, HasQuotient.Quotient, Ideal.comap_map_eq_self_of_isMaximal, IsScalarTower.algebraMap_eq, Ideal.mk_ker, Ideal.IsPrime.ne_top, IsLocalization.AtPrime.isPrime_map_of_liesOver
-- 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
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
⊢ Eq (α := 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) x) :
      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)
        ((algebraMap S Sₚ : (a : S) → Sₚ) x) :
      HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, 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
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)
⊢ 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
-- 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
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)
⊢ 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
-- 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
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)
rwa rwa₁ rwa₂ rwa₃ : Ne (α := S ⧸ P) ((Ideal.Quotient.mk P : (a : S) → S ⧸ P) (↑s : S) : S ⧸ P) (0 : S ⧸ P)
⊢ 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:
rwa [RingEquiv.map_ne_zero_iff]

Premises used: RingEquiv.map_ne_zero_iff
-- 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
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)
⊢ 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]
-- 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 : HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ)
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)
⊢ 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)

Tactic:
obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x

Premises used: Ideal.Quotient.mk_surjective, 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ₚ
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 × ↥p.primeCompl
⊢ 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ₚ)
          ((fun (x : R × ↥p.primeCompl) ↦
              (match (motive := R × ↥p.primeCompl → Rₚ) x with
                | (r, m) => mk' Rₚ r m :
                Rₚ))
            x))))
    (((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ₚ)
          ((fun (x : R × ↥p.primeCompl) ↦
              (match (motive := R × ↥p.primeCompl → Rₚ) x with
                | (r, m) => mk' Rₚ r m :
                Rₚ))
            x))))

Tactic:
simp [equivQuotMaximalIdeal_symm_apply_mk, map_mul, Quotient.algebraMap_mk_of_liesOver,
    IsLocalization.algebraMap_mk' S Rₚ Sₚ]

Premises used: map_mul, IsLocalization.algebraMap_mk', IsLocalization.AtPrime.equivQuotMaximalIdeal_symm_apply_mk, Ideal.Quotient.algebraMap_mk_of_liesOver
-- 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 : Algebra R Sₚ
inst_13 : IsScalarTower R S Sₚ
inst_14 : IsScalarTower R Rₚ Sₚ
inst_15 : p.IsMaximal
x : S
⊢ Eq (α := HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ)))
    (((equivQuotientMapMaximalIdeal S p Rₚ Sₚ :
            RingEquiv.{u_2, u_4} (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
              (HasQuotient.Quotient Sₚ (B := Ideal Sₚ)
                (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ)))) :
          (a : S ⧸ Ideal.map (algebraMap R S) p) → Sₚ ⧸ Ideal.map (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ))
        ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p) : (a : S) → S ⧸ Ideal.map (algebraMap R S) p)
          x) :
      HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ)))
    ((Ideal.Quotient.mk (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ)) :
          (a : Sₚ) → Sₚ ⧸ Ideal.map (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ))
        ((algebraMap S Sₚ : (a : S) → Sₚ) x) :
      HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ)))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, 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ₚ
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ₚ)
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)
⊢ inertiaDeg.{u_3, u_4} (S := Sₚ) (maximalIdeal Rₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) = p.inertiaDeg P

Tactic:
rw [inertiaDeg_algebraMap, inertiaDeg_algebraMap]

Premises used: Ideal.inertiaDeg_algebraMap
-- 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ₚ)
⊢ 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:
Algebra.finrank_eq_of_equiv_equiv (equivQuotMaximalIdeal p Rₚ).symm
    (equivQuotientMapOfIsMaximal p Sₚ P).symm ?_

Premises used: Algebra.finrank_eq_of_equiv_equiv, IsLocalization.AtPrime.equivQuotientMapOfIsMaximal, IsLocalization.AtPrime.equivQuotMaximalIdeal, RingEquiv.symm
-- 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ₚ)
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))))
⊢ 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:
refine Algebra.finrank_eq_of_equiv_equiv (equivQuotMaximalIdeal p Rₚ).symm
    (equivQuotientMapOfIsMaximal p Sₚ P).symm ?_

Premises used: Algebra.finrank_eq_of_equiv_equiv, IsLocalization.AtPrime.equivQuotientMapOfIsMaximal, IsLocalization.AtPrime.equivQuotMaximalIdeal, RingEquiv.symm