awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
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)
⊢ β * α = 1 + (β * α - 1)
have refine_2 : β * α = β * α
Tactic: rw [add_sub_cancel]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
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)
⊢ Membership.mem (γ := Submodule S S) (Ideal.map (F := R →+* S) (algebraMap R S) p) x
have obtain : ∀ (β γ : R) (hγ : γ ∈ p) (hβ : β * α = 1 + γ),
  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]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (hypothesis)
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 (γ := Submodule S S) (Ideal.map (F := R →+* S) (algebraMap R S) p) x
have 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))
Tactic: have := Ideal.mul_mem_left _ (algebraMap _ _ β) hαx
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (hypothesis)
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 (γ := Submodule S S) (Ideal.map (F := R →+* S) (algebraMap R S) p) x
have this₁ : 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
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
have refine : 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
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
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)
have 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)
Tactic: rw [Algebra.smul_def]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
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)
    (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) γ : S) x)
have 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)
Tactic: apply Ideal.mul_mem_right
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
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))
have 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))
Tactic: rw [← map_eq_maximalIdeal p, Ideal.map_map,
      ← IsScalarTower.algebraMap_eq, Ideal.map_map, ← IsScalarTower.algebraMap_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
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))
⊢ 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))
have 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))
Tactic: rw [← map_eq_maximalIdeal p, Ideal.map_map,
      ← IsScalarTower.algebraMap_eq, Ideal.map_map, ← IsScalarTower.algebraMap_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
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))
⊢ 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))
have 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))
Tactic: rw [← map_eq_maximalIdeal p, Ideal.map_map,
      ← IsScalarTower.algebraMap_eq, Ideal.map_map, ← IsScalarTower.algebraMap_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
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))
⊢ 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))
have 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)
Tactic: rw [← map_eq_maximalIdeal p, Ideal.map_map,
      ← IsScalarTower.algebraMap_eq, Ideal.map_map, ← IsScalarTower.algebraMap_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
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)
⊢ 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))
have 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)
Tactic: rw [← map_eq_maximalIdeal p, Ideal.map_map,
      ← IsScalarTower.algebraMap_eq, Ideal.map_map, ← IsScalarTower.algebraMap_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (hypothesis)
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ₚ
⊢ 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ₚ)))
have 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))
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]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
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))
⊢ 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ₚ)))
have 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ₚ)))))
Tactic: refine (Ideal.quotEquivOfEq ?_).trans
    (RingHom.quotientKerEquivOfSurjective (f := algebraMap S (Sₚ ⧸ pSₚ)) ?_)