awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))
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ₚ)))))
⊢ 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_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ₚ)
Tactic: refine (Ideal.quotEquivOfEq ?_).trans
    (RingHom.quotientKerEquivOfSurjective (f := algebraMap S (Sₚ ⧸ pSₚ)) ?_)
-- 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))
⊢ 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ₚ)))))
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ₚ))))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
        (algebraMap Sₚ
          (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ))))
        (algebraMap S Sₚ) :
      RingHom.{u_6, u_9} S
        (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ)))))
Tactic: rw [IsScalarTower.algebraMap_eq S Sₚ, Ideal.Quotient.algebraMap_eq, ← RingHom.comap_ker,
      Ideal.mk_ker, h, Ideal.map_map, ← IsScalarTower.algebraMap_eq, ← under_def, under_map_eq_map]
-- 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))
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ₚ))))
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
          (algebraMap Sₚ
            (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ))))
          (algebraMap S Sₚ) :
        RingHom.{u_6, u_9} S
          (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ)))))
⊢ 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ₚ)))))
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ₚ))))
    (RingHom.comp (Ideal.Quotient.mk (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ)))
        (algebraMap S Sₚ) :
      RingHom.{u_6, u_9} S
        (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ)))))
Tactic: rw [IsScalarTower.algebraMap_eq S Sₚ, Ideal.Quotient.algebraMap_eq, ← RingHom.comap_ker,
      Ideal.mk_ker, h, Ideal.map_map, ← IsScalarTower.algebraMap_eq, ← under_def, under_map_eq_map]
-- 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))
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
have 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ₚ)))
Tactic: obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
Cleared hypotheses: x
-- 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))
x : S
s : ↥(algebraMapSubmonoid S p.primeCompl)
α : R
hα : α ∉ p
e : (algebraMap R S : (a : R) → S) α = (↑s : S)
⊢ ∃ (β : R), ∃ γ ∈ p, α * β = 1 + γ
have 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 + γ
Tactic: obtain ⟨β, hβ⟩ := Ideal.Quotient.mk_surjective (I := p) (Ideal.Quotient.mk p α)⁻¹
-- 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))
x : S
s : ↥(algebraMapSubmonoid S p.primeCompl)
α : R
hα : α ∉ p
e : (algebraMap R S : (a : R) → S) α = (↑s : S)
β : 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 + γ
have refine_1 : α * β - 1 ∈ p
Tactic: refine ⟨β, α * β - 1, ?_, ?_⟩
-- 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))
x : S
s : ↥(algebraMapSubmonoid S p.primeCompl)
α : R
hα : α ∉ p
e : (algebraMap R S : (a : R) → S) α = (↑s : S)
β : 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 : α * β - 1 ∈ p
⊢ ∃ (β : R), ∃ γ ∈ p, α * β = 1 + γ
have refine_2 : α * β = 1 + (α * β - 1)
Tactic: refine ⟨β, α * β - 1, ?_, ?_⟩
-- 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))
x : S
s : ↥(algebraMapSubmonoid S p.primeCompl)
α : R
hα : α ∉ p
e : (algebraMap R S : (a : R) → S) α = (↑s : S)
β : 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 ∈ p
have refine_1 : Ne (α := R ⧸ p) ((Ideal.Quotient.mk p : (a : R) → R ⧸ p) α : R ⧸ p) (0 : R ⧸ p)
Tactic: rw [← Ideal.Quotient.eq_zero_iff_mem, map_sub, map_one,
          map_mul, hβ, mul_inv_cancel₀, sub_self]
-- 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))
x : S
s : ↥(algebraMapSubmonoid S p.primeCompl)
α : R
hα : α ∉ p
e : (algebraMap R S : (a : R) → S) α = (↑s : S)
β : 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)
⊢ Ne (α := R ⧸ p) ((Ideal.Quotient.mk p : (a : R) → R ⧸ p) α : R ⧸ p) (0 : R ⧸ p)
have refine_1 : ¬Eq (α := R ⧸ p) ((Ideal.Quotient.mk p : (a : R) → R ⧸ p) α : R ⧸ p) (0 : R ⧸ p)
Tactic: rwa [Ne, Ideal.Quotient.eq_zero_iff_mem]
-- 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))
x : S
s : ↥(algebraMapSubmonoid S p.primeCompl)
α : R
hα : α ∉ p
e : (algebraMap R S : (a : R) → S) α = (↑s : S)
β : 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:
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)
β γ : R
hγ : γ ∈ p
hβ : α * β = 1 + γ
⊢ 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ₚ)
        (β • 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ₚ ⧸ pSₚ)
        (mk' Sₚ x s) :
      HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ)))
have h₁ : Membership.mem (γ := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ))
  (HSub.hSub (α := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (β • x) : Sₚ) (mk' Sₚ x s))
Tactic: rw [IsScalarTower.algebraMap_eq S Sₚ (Sₚ ⧸ pSₚ), Ideal.Quotient.algebraMap_eq,
      RingHom.comp_apply, ← sub_eq_zero, ← map_sub, Ideal.Quotient.eq_zero_iff_mem]