awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
S : Type u_6
R : Type u_7
inst : CommRing R
p : Ideal R
inst_1 : p.IsMaximal
Sₚ : Type u_9
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : CommRing Sₚ
inst_5 : Algebra S Sₚ
inst_6 : Algebra R Sₚ
inst_7 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst_8 : IsScalarTower R S Sₚ
x : S
hx :
  Membership.mem (γ := Submodule S S)
    (comap (F := S →+* Sₚ) (algebraMap S Sₚ)
      (Ideal.map (R := S) (F := S →+* Sₚ) (algebraMap S Sₚ) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
    x
α : R
hα : α ∉ p
hαx : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p) (α • x)
β : R
hβ :
  Eq (α := R ⧸ p) ((Ideal.Quotient.mk p : (a : R) → R ⧸ p) β : R ⧸ p)
    (((Ideal.Quotient.mk p : (a : R) → R ⧸ p) α)⁻¹ : R ⧸ p)
refine_1 : Ne (α := R ⧸ p) ((Ideal.Quotient.mk p : (a : R) → R ⧸ p) α : R ⧸ p) (0 : R ⧸ p)
⊢ β * α - 1 ∈ p

Tactic:
rw [← Ideal.Quotient.eq_zero_iff_mem, map_sub, map_one,
        map_mul, hβ, inv_mul_cancel₀, sub_self]

Premises used: map_sub, sub_self, Ideal.Quotient.eq_zero_iff_mem, map_mul, map_one, inv_mul_cancel₀
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
S : Type u_6
R : Type u_7
inst : CommRing R
p : Ideal R
inst_1 : p.IsMaximal
Sₚ : Type u_9
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : CommRing Sₚ
inst_5 : Algebra S Sₚ
inst_6 : Algebra R Sₚ
inst_7 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst_8 : IsScalarTower R S Sₚ
x : S
hx :
  Membership.mem (γ := Submodule S S)
    (comap (F := S →+* Sₚ) (algebraMap S Sₚ)
      (Ideal.map (R := S) (F := S →+* Sₚ) (algebraMap S Sₚ) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
    x
α : R
hα : α ∉ p
hαx : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p) (α • x)
β : R
hβ :
  Eq (α := R ⧸ p) ((Ideal.Quotient.mk p : (a : R) → R ⧸ p) β : R ⧸ p)
    (((Ideal.Quotient.mk p : (a : R) → R ⧸ p) α)⁻¹ : R ⧸ p)
refine_1 : ¬Eq (α := R ⧸ p) ((Ideal.Quotient.mk p : (a : R) → R ⧸ p) α : R ⧸ p) (0 : R ⧸ p)
refine_1₁ refine_1₂ refine_1₃ refine_1₄ : α ∉ p
⊢ Ne (α := R ⧸ p) ((Ideal.Quotient.mk p : (a : R) → R ⧸ p) α : R ⧸ p) (0 : R ⧸ p)

Tactic:
rwa [Ne, Ideal.Quotient.eq_zero_iff_mem]

Premises used: Ne, Ideal.Quotient.eq_zero_iff_mem
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
S : Type u_6
R : Type u_7
inst : CommRing R
p : Ideal R
inst_1 : p.IsMaximal
Sₚ : Type u_9
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : CommRing Sₚ
inst_5 : Algebra S Sₚ
inst_6 : Algebra R Sₚ
inst_7 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst_8 : IsScalarTower R S Sₚ
x : S
hx :
  Membership.mem (γ := Submodule S S)
    (comap (F := S →+* Sₚ) (algebraMap S Sₚ)
      (Ideal.map (R := S) (F := S →+* Sₚ) (algebraMap S Sₚ) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
    x
α : R
hα : α ∉ p
hαx : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p) (α • x)
β : R
hβ :
  Eq (α := R ⧸ p) ((Ideal.Quotient.mk p : (a : R) → R ⧸ p) β : R ⧸ p)
    (((Ideal.Quotient.mk p : (a : R) → R ⧸ p) α)⁻¹ : R ⧸ p)
refine_2 refine_2₁ : β * α = β * α
⊢ β * α = 1 + (β * α - 1)

Tactic:
rw [add_sub_cancel]

Premises used: add_sub_cancel
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
S : Type u_6
R : Type u_7
inst : CommRing R
p : Ideal R
inst_1 : p.IsMaximal
Sₚ : Type u_9
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : CommRing Sₚ
inst_5 : Algebra S Sₚ
inst_6 : Algebra R Sₚ
inst_7 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst_8 : IsScalarTower R S Sₚ
x : S
hx :
  Membership.mem (γ := Submodule S S)
    (comap (F := S →+* Sₚ) (algebraMap S Sₚ)
      (Ideal.map (R := S) (F := S →+* Sₚ) (algebraMap S Sₚ) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
    x
α : R
hα : α ∉ p
hαx : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p) (α • x)
obtain :
  ∀ (β γ : R) (hγ : γ ∈ p) (hβ : β * α = 1 + γ),
    Membership.mem (γ := Submodule S S) (Ideal.map (F := R →+* S) (algebraMap R S) p) x
⊢ Membership.mem (γ := Submodule S S) (Ideal.map (F := R →+* S) (algebraMap R S) p) x

Tactic:
obtain ⟨β, γ, hγ, hβ⟩ : ∃ β γ, γ ∈ p ∧ β * α = 1 + γ := by
    obtain ⟨β, hβ⟩ := Ideal.Quotient.mk_surjective (I := p) (Ideal.Quotient.mk p α)⁻¹
    refine ⟨β, β * α - 1, ?_, ?_⟩
    · rw [← Ideal.Quotient.eq_zero_iff_mem, map_sub, map_one,
        map_mul, hβ, inv_mul_cancel₀, sub_self]
      rwa [Ne, Ideal.Quotient.eq_zero_iff_mem]
    · rw [add_sub_cancel]
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
S : Type u_6
R : Type u_7
inst : CommRing R
p : Ideal R
inst_1 : p.IsMaximal
Sₚ : Type u_9
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : CommRing Sₚ
inst_5 : Algebra S Sₚ
inst_6 : Algebra R Sₚ
inst_7 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst_8 : IsScalarTower R S Sₚ
x : S
hx :
  Membership.mem (γ := Submodule S S)
    (comap (F := S →+* Sₚ) (algebraMap S Sₚ)
      (Ideal.map (R := S) (F := S →+* Sₚ) (algebraMap S Sₚ) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
    x
α : R
hα : α ∉ p
hαx : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p) (α • x)
β γ : R
hγ : γ ∈ p
hβ : β * α = 1 + γ
⊢ Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)
    (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) β : S) (α • x))

Tactic:
have := Ideal.mul_mem_left _ (algebraMap _ _ β) hαx
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
S : Type u_6
R : Type u_7
inst : CommRing R
p : Ideal R
inst_1 : p.IsMaximal
Sₚ : Type u_9
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : CommRing Sₚ
inst_5 : Algebra S Sₚ
inst_6 : Algebra R Sₚ
inst_7 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst_8 : IsScalarTower R S Sₚ
x : S
hx :
  Membership.mem (γ := Submodule S S)
    (comap (F := S →+* Sₚ) (algebraMap S Sₚ)
      (Ideal.map (R := S) (F := S →+* Sₚ) (algebraMap S Sₚ) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
    x
α : R
hα : α ∉ p
hαx : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p) (α • x)
β γ : R
hγ : γ ∈ p
hβ : β * α = 1 + γ
this :
  Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)
    (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) β : S) (α • x))
⊢ Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p) (x + γ • x)

Tactic:
rw [← Algebra.smul_def, smul_smul, hβ, add_smul, one_smul] at this

Premises used: smul_smul, one_smul, add_smul, Algebra.smul_def
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
S : Type u_6
R : Type u_7
inst : CommRing R
p : Ideal R
inst_1 : p.IsMaximal
Sₚ : Type u_9
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : CommRing Sₚ
inst_5 : Algebra S Sₚ
inst_6 : Algebra R Sₚ
inst_7 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst_8 : IsScalarTower R S Sₚ
x : S
hx :
  Membership.mem (γ := Submodule S S)
    (comap (F := S →+* Sₚ) (algebraMap S Sₚ)
      (Ideal.map (R := S) (F := S →+* Sₚ) (algebraMap S Sₚ) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
    x
α : R
hα : α ∉ p
hαx : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p) (α • x)
β γ : R
hγ : γ ∈ p
hβ : β * α = 1 + γ
this : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p) (x + γ • x)
⊢ Membership.mem (γ := Submodule S S) (Ideal.map (F := R →+* S) (algebraMap R S) p) x

Tactic:
(Submodule.add_mem_iff_left pS ?_).mp this

Premises used: Algebra.algebraMap, Set.Mem, setOf, Ideal.map, Submodule.add_mem_iff_left, Iff.mp
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
S : Type u_6
R : Type u_7
inst : CommRing R
p : Ideal R
inst_1 : p.IsMaximal
Sₚ : Type u_9
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : CommRing Sₚ
inst_5 : Algebra S Sₚ
inst_6 : Algebra R Sₚ
inst_7 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst_8 : IsScalarTower R S Sₚ
x : S
hx :
  Membership.mem (γ := Submodule S S)
    (comap (F := S →+* Sₚ) (algebraMap S Sₚ)
      (Ideal.map (R := S) (F := S →+* Sₚ) (algebraMap S Sₚ) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
    x
α : R
hα : α ∉ p
hαx : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p) (α • x)
β γ : R
hγ : γ ∈ p
hβ : β * α = 1 + γ
this : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p) (x + γ • x)
refine : Membership.mem (γ := Submodule S S) (Ideal.map (F := R →+* S) (algebraMap R S) p) (γ • x)
⊢ Membership.mem (γ := Submodule S S) (Ideal.map (F := R →+* S) (algebraMap R S) p) x

Tactic:
refine (Submodule.add_mem_iff_left pS ?_).mp this
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
S : Type u_6
R : Type u_7
inst : CommRing R
p : Ideal R
inst_1 : p.IsMaximal
Sₚ : Type u_9
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : CommRing Sₚ
inst_5 : Algebra S Sₚ
inst_6 : Algebra R Sₚ
inst_7 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst_8 : IsScalarTower R S Sₚ
x : S
hx :
  Membership.mem (γ := Submodule S S)
    (comap (F := S →+* Sₚ) (algebraMap S Sₚ)
      (Ideal.map (R := S) (F := S →+* Sₚ) (algebraMap S Sₚ) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
    x
α : R
hα : α ∉ p
hαx : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p) (α • x)
β γ : R
hγ : γ ∈ p
hβ : β * α = 1 + γ
this : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p) (x + γ • x)
rw :
  Membership.mem (γ := Submodule S S) (Ideal.map (F := R →+* S) (algebraMap R S) p)
    (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) γ : S) x)
⊢ Membership.mem (γ := Submodule S S) (Ideal.map (F := R →+* S) (algebraMap R S) p) (γ • x)

Tactic:
rw [Algebra.smul_def]

Premises used: Algebra.smul_def
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
S : Type u_6
R : Type u_7
inst : CommRing R
p : Ideal R
inst_1 : p.IsMaximal
Sₚ : Type u_9
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : CommRing Sₚ
inst_5 : Algebra S Sₚ
inst_6 : Algebra R Sₚ
inst_7 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst_8 : IsScalarTower R S Sₚ
x : S
hx :
  Membership.mem (γ := Submodule S S)
    (comap (F := S →+* Sₚ) (algebraMap S Sₚ)
      (Ideal.map (R := S) (F := S →+* Sₚ) (algebraMap S Sₚ) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
    x
α : R
hα : α ∉ p
hαx : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p) (α • x)
β γ : R
hγ : γ ∈ p
hβ : β * α = 1 + γ
this : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p) (x + γ • x)
h :
  Membership.mem.{u_6, u_6} (α := S) (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)
    ((algebraMap R S : (a : R) → S) γ : S)
⊢ Membership.mem (γ := Submodule S S) (Ideal.map (F := R →+* S) (algebraMap R S) p)
    (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) γ : S) x)

Tactic:
apply Ideal.mul_mem_right

Premises used: Ideal.mul_mem_right
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
S : Type u_6
R : Type u_7
inst : CommRing R
p : Ideal R
inst_1 : p.IsMaximal
Sₚ : Type u_9
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : CommRing Sₚ
inst_5 : Algebra S Sₚ
inst_6 : Algebra R Sₚ
inst_7 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst_8 : IsScalarTower R S Sₚ
x : S
hx :
  Membership.mem (γ := Submodule S S)
    (comap (F := S →+* Sₚ) (algebraMap S Sₚ)
      (Ideal.map (R := S) (F := S →+* Sₚ) (algebraMap S Sₚ) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
    x
α : R
hα : α ∉ p
hαx : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p) (α • x)
β γ : R
hγ : γ ∈ p
hβ : β * α = 1 + γ
this : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p) (x + γ • x)
⊢ Membership.mem.{u_6, u_6} (α := S) (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)
    ((algebraMap R S : (a : R) → S) γ : S)

Tactic:
Ideal.mem_map_of_mem _ hγ

Premises used: Ideal.mem_map_of_mem, Set.Mem
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
S : Type u_6
R : Type u_7
inst : CommRing R
p : Ideal R
inst_1 : p.IsMaximal
Sₚ : Type u_9
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : CommRing Sₚ
inst_5 : Algebra S Sₚ
inst_6 : Algebra R Sₚ
inst_7 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst_8 : IsScalarTower R S Sₚ
x : S
hx :
  Membership.mem (γ := Submodule S S)
    (comap (F := S →+* Sₚ) (algebraMap S Sₚ)
      (Ideal.map (R := S) (F := S →+* Sₚ) (algebraMap S Sₚ) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
    x
α : R
hα : α ∉ p
hαx : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p) (α • x)
β γ : R
hγ : γ ∈ p
hβ : β * α = 1 + γ
this : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p) (x + γ • x)
⊢ Membership.mem.{u_6, u_6} (α := S) (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)
    ((algebraMap R S : (a : R) → S) γ : S)

Tactic:
exact Ideal.mem_map_of_mem _ hγ

Premises used: Ideal.mem_map_of_mem
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
S_1 : Type u_2
inst_1 : CommSemiring S_1
inst_2 : Algebra R_1 S_1
P_1 : Type u_3
inst_3 : CommSemiring P_1
p_1 : Ideal R_1
inst_4 : p_1.IsPrime
Rₚ_1 : Type u_4
inst_5 : CommSemiring Rₚ_1
inst_6 : Algebra R_1 Rₚ_1
inst_7 : IsLocalization.AtPrime Rₚ_1 p_1
inst_8 : IsLocalRing Rₚ_1
Sₚ_1 : Type u_5
inst_9 : CommSemiring Sₚ_1
inst_10 : Algebra S_1 Sₚ_1
inst_11 : IsLocalization (algebraMapSubmonoid S_1 p_1.primeCompl) Sₚ_1
inst_12 : Algebra Rₚ_1 Sₚ_1
P : Ideal S_1
S : Type u_6
R : Type u_7
inst_13 : CommRing R
p : Ideal R
inst_14 : p.IsMaximal
Rₚ : Type u_8
inst_15 : CommRing Rₚ
inst_16 : Algebra R Rₚ
inst_17 : IsLocalization.AtPrime Rₚ p
inst_18 : IsLocalRing Rₚ
Sₚ : Type u_9
inst_19 : CommRing S
inst_20 : Algebra R S
inst_21 : CommRing Sₚ
inst_22 : Algebra S Sₚ
inst_23 : Algebra R Sₚ
inst_24 : Algebra Rₚ Sₚ
inst_25 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst_26 : IsScalarTower R S Sₚ
inst_27 : IsScalarTower R Rₚ Sₚ
rw :
  Eq.{u_9 + 1} (α := Ideal Sₚ)
    (Ideal.map (R := Rₚ) (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) p))
    (Ideal.map (R := S) (F := S →+* Sₚ) (algebraMap S Sₚ) (Ideal.map (F := R →+* S) (algebraMap R S) p))
rw₁ :
  Eq.{u_9 + 1} (α := Ideal Sₚ)
    (Ideal.map (F := R →+* Sₚ)
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Rₚ Sₚ) (algebraMap R Rₚ)) p)
    (Ideal.map (R := S) (F := S →+* Sₚ) (algebraMap S Sₚ) (Ideal.map (F := R →+* S) (algebraMap R S) p))
rw₂ :
  Eq.{u_9 + 1} (α := Ideal Sₚ) (Ideal.map (F := R →+* Sₚ) (algebraMap R Sₚ) p)
    (Ideal.map (R := S) (F := S →+* Sₚ) (algebraMap S Sₚ) (Ideal.map (F := R →+* S) (algebraMap R S) p))
rw₃ :
  Eq.{u_9 + 1} (α := Ideal Sₚ) (Ideal.map (F := R →+* Sₚ) (algebraMap R Sₚ) p)
    (Ideal.map (F := R →+* Sₚ) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S Sₚ) (algebraMap R S))
      p)
rw₄ rw₅ :
  Eq.{u_9 + 1} (α := Ideal Sₚ) (Ideal.map (F := R →+* Sₚ) (algebraMap R Sₚ) p)
    (Ideal.map (F := R →+* Sₚ) (algebraMap R Sₚ) p)
⊢ Eq.{u_9 + 1} (α := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ))
    (Ideal.map (R := S) (F := S →+* Sₚ) (algebraMap S Sₚ) (Ideal.map (F := R →+* S) (algebraMap R S) p))

Tactic:
rw [← map_eq_maximalIdeal p, Ideal.map_map,
      ← IsScalarTower.algebraMap_eq, Ideal.map_map, ← IsScalarTower.algebraMap_eq]

Premises used: IsLocalization.AtPrime.map_eq_maximalIdeal, Ideal.map_map, IsScalarTower.algebraMap_eq
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
S_1 : Type u_2
inst_1 : CommSemiring S_1
inst_2 : Algebra R_1 S_1
P_1 : Type u_3
inst_3 : CommSemiring P_1
p_1 : Ideal R_1
inst_4 : p_1.IsPrime
Rₚ_1 : Type u_4
inst_5 : CommSemiring Rₚ_1
inst_6 : Algebra R_1 Rₚ_1
inst_7 : IsLocalization.AtPrime Rₚ_1 p_1
inst_8 : IsLocalRing Rₚ_1
Sₚ_1 : Type u_5
inst_9 : CommSemiring Sₚ_1
inst_10 : Algebra S_1 Sₚ_1
inst_11 : IsLocalization (algebraMapSubmonoid S_1 p_1.primeCompl) Sₚ_1
inst_12 : Algebra Rₚ_1 Sₚ_1
P : Ideal S_1
S : Type u_6
R : Type u_7
inst_13 : CommRing R
p : Ideal R
inst_14 : p.IsMaximal
Rₚ : Type u_8
inst_15 : CommRing Rₚ
inst_16 : Algebra R Rₚ
inst_17 : IsLocalization.AtPrime Rₚ p
inst_18 : IsLocalRing Rₚ
Sₚ : Type u_9
inst_19 : CommRing S
inst_20 : Algebra R S
inst_21 : CommRing Sₚ
inst_22 : Algebra S Sₚ
inst_23 : Algebra R Sₚ
inst_24 : Algebra Rₚ Sₚ
inst_25 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst_26 : IsScalarTower R S Sₚ
inst_27 : IsScalarTower R Rₚ Sₚ
⊢ Eq.{u_9 + 1} (α := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ))
    (Ideal.map (R := S) (F := S →+* Sₚ) (algebraMap S Sₚ) (Ideal.map (F := R →+* S) (algebraMap R S) p))

Tactic:
haveI h : pSₚ = Ideal.map (algebraMap S Sₚ) pS := by
    rw [← map_eq_maximalIdeal p, Ideal.map_map,
      ← IsScalarTower.algebraMap_eq, Ideal.map_map, ← IsScalarTower.algebraMap_eq]
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
S_1 : Type u_2
inst_1 : CommSemiring S_1
inst_2 : Algebra R_1 S_1
P_1 : Type u_3
inst_3 : CommSemiring P_1
p_1 : Ideal R_1
inst_4 : p_1.IsPrime
Rₚ_1 : Type u_4
inst_5 : CommSemiring Rₚ_1
inst_6 : Algebra R_1 Rₚ_1
inst_7 : IsLocalization.AtPrime Rₚ_1 p_1
inst_8 : IsLocalRing Rₚ_1
Sₚ_1 : Type u_5
inst_9 : CommSemiring Sₚ_1
inst_10 : Algebra S_1 Sₚ_1
inst_11 : IsLocalization (algebraMapSubmonoid S_1 p_1.primeCompl) Sₚ_1
inst_12 : Algebra Rₚ_1 Sₚ_1
P : Ideal S_1
S : Type u_6
R : Type u_7
inst_13 : CommRing R
p : Ideal R
inst_14 : p.IsMaximal
Rₚ : Type u_8
inst_15 : CommRing Rₚ
inst_16 : Algebra R Rₚ
inst_17 : IsLocalization.AtPrime Rₚ p
inst_18 : IsLocalRing Rₚ
Sₚ : Type u_9
inst_19 : CommRing S
inst_20 : Algebra R S
inst_21 : CommRing Sₚ
inst_22 : Algebra S Sₚ
inst_23 : Algebra R Sₚ
inst_24 : Algebra Rₚ Sₚ
inst_25 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst_26 : IsScalarTower R S Sₚ
inst_27 : IsScalarTower R Rₚ Sₚ
h :
  Eq.{u_9 + 1} (α := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ))
    (Ideal.map (R := S) (F := S →+* Sₚ) (algebraMap S Sₚ) (Ideal.map (F := R →+* S) (algebraMap R S) p))
refine_1 :
  Eq (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)
    (RingHom.ker (F :=
      RingHom.{u_6, u_9} S
        (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ))))
      (algebraMap S
          (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ))) :
        RingHom.{u_6, u_9} S
          (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ)))))
refine_2 :
  Function.Surjective.{u_6 + 1, u_9 + 1} (α := S) (β :=
    HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ)))
    (⇑(algebraMap S
            (HasQuotient.Quotient Sₚ (B := Ideal Sₚ)
              (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ))) :
          RingHom.{u_6, u_9} S
            (HasQuotient.Quotient Sₚ (B := Ideal Sₚ)
              (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ)))) :
      (a : S) → Sₚ ⧸ pSₚ)
⊢ RingEquiv.{u_6, u_9} (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ₚ)))

Tactic:
refine (Ideal.quotEquivOfEq ?_).trans
    (RingHom.quotientKerEquivOfSurjective (f := algebraMap S (Sₚ ⧸ pSₚ)) ?_)
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
S_1 : Type u_2
inst_1 : CommSemiring S_1
inst_2 : Algebra R_1 S_1
P_1 : Type u_3
inst_3 : CommSemiring P_1
p_1 : Ideal R_1
inst_4 : p_1.IsPrime
Rₚ_1 : Type u_4
inst_5 : CommSemiring Rₚ_1
inst_6 : Algebra R_1 Rₚ_1
inst_7 : IsLocalization.AtPrime Rₚ_1 p_1
inst_8 : IsLocalRing Rₚ_1
Sₚ_1 : Type u_5
inst_9 : CommSemiring Sₚ_1
inst_10 : Algebra S_1 Sₚ_1
inst_11 : IsLocalization (algebraMapSubmonoid S_1 p_1.primeCompl) Sₚ_1
inst_12 : Algebra Rₚ_1 Sₚ_1
P : Ideal S_1
S : Type u_6
R : Type u_7
inst_13 : CommRing R
p : Ideal R
inst_14 : p.IsMaximal
Rₚ : Type u_8
inst_15 : CommRing Rₚ
inst_16 : Algebra R Rₚ
inst_17 : IsLocalization.AtPrime Rₚ p
inst_18 : IsLocalRing Rₚ
Sₚ : Type u_9
inst_19 : CommRing S
inst_20 : Algebra R S
inst_21 : CommRing Sₚ
inst_22 : Algebra S Sₚ
inst_23 : Algebra R Sₚ
inst_24 : Algebra Rₚ Sₚ
inst_25 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst_26 : IsScalarTower R S Sₚ
inst_27 : IsScalarTower R Rₚ Sₚ
h :
  Eq.{u_9 + 1} (α := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ))
    (Ideal.map (R := S) (F := S →+* Sₚ) (algebraMap S Sₚ) (Ideal.map (F := R →+* S) (algebraMap R S) p))
x : HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ))
refine_2 :
  ∀ (x : Sₚ),
    ∃ (a : S),
      Eq.{u_9 + 1} (α :=
        HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ)))
        (((algebraMap S
                  (HasQuotient.Quotient Sₚ (B := Ideal Sₚ)
                    (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ))) :
                RingHom.{u_6, u_9} S
                  (HasQuotient.Quotient Sₚ (B := Ideal Sₚ)
                    (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ)))) :
              (a : S) → Sₚ ⧸ pSₚ)
            a :
          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ₚ ⧸ pSₚ) x :
          HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ)))
⊢ ∃ (a : S),
    ((algebraMap S
              (HasQuotient.Quotient Sₚ (B := Ideal Sₚ)
                (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ))) :
            RingHom.{u_6, u_9} S
              (HasQuotient.Quotient Sₚ (B := Ideal Sₚ)
                (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ)))) :
          (a : S) → Sₚ ⧸ pSₚ)
        a =
      x

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

Premises used: Ideal.Quotient.mk_surjective, rfl
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
S_1 : Type u_2
inst_1 : CommSemiring S_1
inst_2 : Algebra R_1 S_1
P_1 : Type u_3
inst_3 : CommSemiring P_1
p_1 : Ideal R_1
inst_4 : p_1.IsPrime
Rₚ_1 : Type u_4
inst_5 : CommSemiring Rₚ_1
inst_6 : Algebra R_1 Rₚ_1
inst_7 : IsLocalization.AtPrime Rₚ_1 p_1
inst_8 : IsLocalRing Rₚ_1
Sₚ_1 : Type u_5
inst_9 : CommSemiring Sₚ_1
inst_10 : Algebra S_1 Sₚ_1
inst_11 : IsLocalization (algebraMapSubmonoid S_1 p_1.primeCompl) Sₚ_1
inst_12 : Algebra Rₚ_1 Sₚ_1
P : Ideal S_1
S : Type u_6
R : Type u_7
inst_13 : CommRing R
p : Ideal R
inst_14 : p.IsMaximal
Rₚ : Type u_8
inst_15 : CommRing Rₚ
inst_16 : Algebra R Rₚ
inst_17 : IsLocalization.AtPrime Rₚ p
inst_18 : IsLocalRing Rₚ
Sₚ : Type u_9
inst_19 : CommRing S
inst_20 : Algebra R S
inst_21 : CommRing Sₚ
inst_22 : Algebra S Sₚ
inst_23 : Algebra R Sₚ
inst_24 : Algebra Rₚ Sₚ
inst_25 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst_26 : IsScalarTower R S Sₚ
inst_27 : IsScalarTower R Rₚ Sₚ
h :
  Eq.{u_9 + 1} (α := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ))
    (Ideal.map (R := S) (F := S →+* Sₚ) (algebraMap S Sₚ) (Ideal.map (F := R →+* S) (algebraMap R S) p))
x : S
s : ↥(algebraMapSubmonoid S p.primeCompl)
α : R
hα : α ∉ p
e : (algebraMap R S : (a : R) → S) α = (↑s : S)
obtain :
  ∀ (β : R)
    (hβ :
      Eq (α := R ⧸ p) ((Ideal.Quotient.mk p : (a : R) → R ⧸ p) β : R ⧸ p)
        (((Ideal.Quotient.mk p : (a : R) → R ⧸ p) α)⁻¹ : R ⧸ p)),
    ∃ (β : R), ∃ γ ∈ p, α * β = 1 + γ
⊢ ∃ (β : R), ∃ γ ∈ p, α * β = 1 + γ

Tactic:
obtain ⟨β, hβ⟩ := Ideal.Quotient.mk_surjective (I := p) (Ideal.Quotient.mk p α)⁻¹

Premises used: Ideal.Quotient.mk, Ideal.Quotient.mk_surjective, Inv.inv, DFunLike.coe