awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothOfFree (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Smooth R S
f : (p : Ideal S) → [inst_4 : p.IsPrime] → [IsSmoothAt R p] → S
hf₁ : ∀ (p : Ideal S) [inst_4 : p.IsPrime] [inst : IsSmoothAt R p], f p ∉ p
hf₂ :
  ∀ (p : Ideal S) [inst_4 : p.IsPrime] [inst_5 : IsSmoothAt R p],
    IsStandardSmooth.{u_1, u_2} R (Localization.Away (f p))
⊢ Eq.{u_2 + 1} (α := Ideal S) (Ideal.span (Set.range fun (p : PrimeSpectrum S) ↦ f p.asIdeal)) ⊤
have simp : ∀ (x : PrimeSpectrum S), ∃ (i : PrimeSpectrum S), f i.asIdeal ∉ x.asIdeal
Tactic: simp [← PrimeSpectrum.iSup_basicOpen_eq_top_iff, TopologicalSpace.Opens.ext_iff, Set.ext_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Maximal.Localization (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
K : Type u_5
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
⊢ Eq.{u_5 + 1} (α := Subalgebra R K)
    (⨅ (v : MaximalSpectrum R), Localization.subalgebra.ofField K v.asIdeal.primeCompl ⋯) ⊥
have h : ∀ (x : K),
  Membership.mem (γ := Subalgebra R K)
      (⨅ (v : MaximalSpectrum R), Localization.subalgebra.ofField K v.asIdeal.primeCompl sorry) x ↔
    Membership.mem (γ := Subalgebra R K) ⊥ x
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Maximal.Localization (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
K : Type u_5
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
x : K
⊢ Membership.mem (γ := Subalgebra R K)
      (⨅ (v : MaximalSpectrum R), Localization.subalgebra.ofField K v.asIdeal.primeCompl ⋯) x ↔
    Membership.mem (γ := Subalgebra R K) ⊥ x
have h : (∀ (i : MaximalSpectrum R),
    Membership.mem (γ := Subalgebra R K) (Localization.subalgebra.ofField K i.asIdeal.primeCompl sorry) x) ↔
  Membership.mem (γ := Set K) (range.{u_5, u_4 + 1} (ι := R) (⇑(algebraMap R K) : (a : R) → K)) x
Tactic: rw [Algebra.mem_bot, Algebra.mem_iInf]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Maximal.Localization (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
K : Type u_5
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
x : K
⊢ (∀ (i : MaximalSpectrum R),
      Membership.mem (γ := Subalgebra R K) (Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯) x) ↔
    Membership.mem (γ := Set K) (range.{u_5, u_4 + 1} (ι := R) (⇑(algebraMap R K) : (a : R) → K)) x
have h : (∀ (i : MaximalSpectrum R),
    Membership.mem (γ := Subalgebra R K) (Localization.subalgebra.ofField K i.asIdeal.primeCompl sorry) x) →
  Membership.mem (γ := Set K) (range.{u_5, u_4 + 1} (ι := R) (⇑(algebraMap R K) : (a : R) → K)) x
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Maximal.Localization (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
K : Type u_5
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
x : K
h :
  (∀ (i : MaximalSpectrum R),
      Membership.mem (γ := Subalgebra R K) (Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯) x) →
    Membership.mem (γ := Set K) (range.{u_5, u_4 + 1} (ι := R) (⇑(algebraMap R K) : (a : R) → K)) x
⊢ (∀ (i : MaximalSpectrum R),
      Membership.mem (γ := Subalgebra R K) (Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯) x) ↔
    Membership.mem (γ := Set K) (range.{u_5, u_4 + 1} (ι := R) (⇑(algebraMap R K) : (a : R) → K)) x
have h₁ : Membership.mem (γ := Set K) (range.{u_5, u_4 + 1} (ι := R) (⇑(algebraMap R K) : (a : R) → K)) x →
  ∀ (i : MaximalSpectrum R),
    Membership.mem (γ := Subalgebra R K) (Localization.subalgebra.ofField K i.asIdeal.primeCompl sorry) x
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Maximal.Localization (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
K : Type u_5
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
x : K
⊢ (∀ (i : MaximalSpectrum R),
      Membership.mem (γ := Subalgebra R K) (Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯) x) →
    Membership.mem (γ := Set K) (range.{u_5, u_4 + 1} (ι := R) (⇑(algebraMap R K) : (a : R) → K)) x
have h : x ∉ range.{u_5, u_4 + 1} (ι := R) (⇑(algebraMap R K) : (a : R) → K) →
  ¬∀ (i : MaximalSpectrum R),
      Membership.mem (γ := Subalgebra R K) (Localization.subalgebra.ofField K i.asIdeal.primeCompl sorry) x
Tactic: contrapose
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Maximal.Localization (hypothesis)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
K : Type u_5
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
x : K
hrange : x ∉ range.{u_5, u_4 + 1} (ι := R) (⇑(algebraMap R K) : (a : R) → K)
hlocal :
  ∀ (i : MaximalSpectrum R),
    Membership.mem (γ := Subalgebra R K) (Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯) x
denom : Ideal R := Submodule.comap (LinearMap.toSpanSingleton R K x) 1
⊢ False
have hdenom : 1 ∉ denom
Tactic: have hdenom : (1 : R) ∉ denom := by simpa [denom] using hrange
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Maximal.Localization (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
K : Type u_5
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
x : K
hrange : x ∉ range.{u_5, u_4 + 1} (ι := R) (⇑(algebraMap R K) : (a : R) → K)
hlocal :
  ∀ (i : MaximalSpectrum R),
    Membership.mem (γ := Subalgebra R K) (Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯) x
denom : Ideal R := Submodule.comap (LinearMap.toSpanSingleton R K x) 1
hdenom : 1 ∉ denom
⊢ False
have h : ∀ (max : Ideal R) (hmax : max.IsMaximal) (hle : denom ≤ max), False
Tactic: rcases denom.exists_le_maximal (denom.ne_top_iff_one.mpr hdenom) with ⟨max, hmax, hle⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Maximal.Localization (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
K : Type u_5
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
x : K
hrange : x ∉ range.{u_5, u_4 + 1} (ι := R) (⇑(algebraMap R K) : (a : R) → K)
hlocal :
  ∀ (i : MaximalSpectrum R),
    Membership.mem (γ := Subalgebra R K) (Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯) x
denom : Ideal R := Submodule.comap (LinearMap.toSpanSingleton R K x) 1
hdenom : 1 ∉ denom
max : Ideal R
hmax : max.IsMaximal
hle : denom ≤ max
⊢ False
have h : ∀ (n d : R) (hd : d ∈ { asIdeal := max, isMaximal := hmax : MaximalSpectrum R }.asIdeal.primeCompl)
  (hrange :
    HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) n : K) (((algebraMap R K : (a : R) → K) d)⁻¹ : K) ∉
      range.{u_5, u_4 + 1} (ι := R) (⇑(algebraMap R K) : (a : R) → K))
  (hlocal :
    ∀ (i : MaximalSpectrum R),
      Membership.mem (γ := Subalgebra R K) (Localization.subalgebra.ofField K i.asIdeal.primeCompl sorry)
        (HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) n : K)
          (((algebraMap R K : (a : R) → K) d)⁻¹ : K))),
  let denom : Ideal R :=
    Submodule.comap
      (LinearMap.toSpanSingleton R K
        (HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) n : K) (((algebraMap R K : (a : R) → K) d)⁻¹ : K)))
      1;
  ∀ (hdenom : 1 ∉ denom) (hle : denom ≤ max), False
Tactic: rcases hlocal ⟨max, hmax⟩ with ⟨n, d, hd, rfl⟩
Cleared hypotheses: x, hrange, hlocal, denom, hdenom, hle
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Maximal.Localization (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
K : Type u_5
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
y : R
v : Ideal R
hv : v.IsMaximal
⊢ (algebraMap R K : (a : R) → K) y =
    HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) y : K) (((algebraMap R K : (a : R) → K) 1)⁻¹ : K)
have rw : (algebraMap R K : (a : R) → K) y = HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) y : K) (1⁻¹ : K)
Tactic: rw [map_one, inv_one, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Maximal.Localization (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
K : Type u_5
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
y : R
v : Ideal R
hv : v.IsMaximal
rw : (algebraMap R K : (a : R) → K) y = HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) y : K) (1⁻¹ : K)
⊢ (algebraMap R K : (a : R) → K) y =
    HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) y : K) (((algebraMap R K : (a : R) → K) 1)⁻¹ : K)
have rw₁ : (algebraMap R K : (a : R) → K) y = HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) y : K) (1 : K)
Tactic: rw [map_one, inv_one, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Maximal.Localization (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
K : Type u_5
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
y : R
v : Ideal R
hv : v.IsMaximal
rw : (algebraMap R K : (a : R) → K) y = HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) y : K) (1⁻¹ : K)
rw₁ : (algebraMap R K : (a : R) → K) y = HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) y : K) (1 : K)
⊢ (algebraMap R K : (a : R) → K) y =
    HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) y : K) (((algebraMap R K : (a : R) → K) 1)⁻¹ : K)
have rw₂ : Eq.{u_5 + 1} (α := K) ((algebraMap R K : (a : R) → K) y : K) ((algebraMap R K : (a : R) → K) y : K)
Tactic: rw [map_one, inv_one, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Maximal.Localization (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
K : Type u_5
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
⊢ Eq.{u_5 + 1} (α := Subalgebra R K) (⨅ (v : PrimeSpectrum R), Localization.subalgebra.ofField K v.asIdeal.primeCompl ⋯)
    ⊥
have refine : ∀ (x : K),
  Membership.mem (γ := Subalgebra R K)
      (⨅ (v : PrimeSpectrum R), Localization.subalgebra.ofField K v.asIdeal.primeCompl sorry) x →
    Membership.mem (γ := Subalgebra R K)
      (⨅ (v : MaximalSpectrum R), Localization.subalgebra.ofField K v.asIdeal.primeCompl sorry) x
Tactic: refine bot_unique (.trans (fun _ ↦ ?_) (MaximalSpectrum.iInf_localization_eq_bot R K).le)
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Maximal.Localization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
r r' : R
eq :
  Eq (α := PiLocalization R) ((toPiLocalization R : (a : R) → PiLocalization R) r : PiLocalization R)
    ((toPiLocalization R : (a : R) → PiLocalization R) r' : PiLocalization R)
⊢ r = r'
have rw : 1 * r = 1 * r'
Tactic: rw [← one_mul r, ← one_mul r']
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Maximal.Localization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
r r' : R
eq :
  Eq (α := PiLocalization R) ((toPiLocalization R : (a : R) → PiLocalization R) r : PiLocalization R)
    ((toPiLocalization R : (a : R) → PiLocalization R) r' : PiLocalization R)
⊢ 1 * r = 1 * r'
have by_contra : ∀ (ne : ¬1 * r = 1 * r'), False
Tactic: by_contra ne
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Maximal.Localization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
r r' : R
eq :
  Eq (α := PiLocalization R) ((toPiLocalization R : (a : R) → PiLocalization R) r : PiLocalization R)
    ((toPiLocalization R : (a : R) → PiLocalization R) r' : PiLocalization R)
ne : ¬1 * r = 1 * r'
⊢ False
have have : ∀ (I : Ideal R) (mI : I.IsMaximal) (hI : Module.eqIdeal R r r' ≤ I), False
Tactic: have ⟨I, mI, hI⟩ := (Module.eqIdeal R r r').exists_le_maximal ((Ideal.ne_top_iff_one _).mpr ne)
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Maximal.Localization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
r r' : R
eq :
  Eq (α := PiLocalization R) ((toPiLocalization R : (a : R) → PiLocalization R) r : PiLocalization R)
    ((toPiLocalization R : (a : R) → PiLocalization R) r' : PiLocalization R)
ne : ¬1 * r = 1 * r'
I : Ideal R
mI : I.IsMaximal
hI : Module.eqIdeal R r r' ≤ I
⊢ False
have have : ∀ (s : ↥I.primeCompl) (hs : (↑s : R) * r = (↑s : R) * r'), False
Tactic: have ⟨s, hs⟩ := (IsLocalization.eq_iff_exists I.primeCompl _).mp (congr_fun eq ⟨I, mI⟩)
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Maximal.Localization (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
hf : Function.Bijective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
⊢ (mapPiLocalization f hf).comp (↑(toPiLocalization R) : R →+* PiLocalization R) =
    RingHom.comp (AlgHom.toRingHom (toPiLocalization S)) f
have a : ∀ (r : R) (I : MaximalSpectrum S),
  Eq.{u_2 + 1} (α := Localization.AtPrime I.asIdeal)
    ((((mapPiLocalization f hf).comp (↑(toPiLocalization R) : R →+* PiLocalization R) :
            RingHom.{u_1, u_2} R (PiLocalization S)) :
          (a : R) → PiLocalization S)
        r I :
      Localization.AtPrime I.asIdeal)
    ((RingHom.comp (AlgHom.toRingHom (toPiLocalization S)) f : (a : R) → PiLocalization S) r I :
      Localization.AtPrime I.asIdeal)
Tactic: ext r I
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Maximal.Localization (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
hf : Function.Bijective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
r : R
I : MaximalSpectrum S
⊢ Eq.{u_2 + 1} (α := Localization.AtPrime I.asIdeal)
    ((((mapPiLocalization f hf).comp (↑(toPiLocalization R) : R →+* PiLocalization R) :
            RingHom.{u_1, u_2} R (PiLocalization S)) :
          (a : R) → PiLocalization S)
        r I :
      Localization.AtPrime I.asIdeal)
    ((RingHom.comp (AlgHom.toRingHom (toPiLocalization S)) f : (a : R) → PiLocalization S) r I :
      Localization.AtPrime I.asIdeal)
have a : Eq.{u_2 + 1} (α := Localization.AtPrime I.asIdeal)
  (((Localization.localRingHom (Ideal.comap f I.asIdeal) I.asIdeal f sorry :
          RingHom.{u_1, u_2} (Localization.AtPrime (Ideal.comap f I.asIdeal)) (Localization.AtPrime I.asIdeal)) :
        (a : Localization.AtPrime (Ideal.comap f I.asIdeal)) → Localization.AtPrime I.asIdeal)
      ((algebraMap R (Localization.AtPrime (Ideal.comap f I.asIdeal)) :
          (a : R) → Localization.AtPrime (Ideal.comap f I.asIdeal))
        r) :
    Localization.AtPrime I.asIdeal)
  ((algebraMap S (Localization.AtPrime I.asIdeal) : (a : S) → Localization.AtPrime I.asIdeal) ((f : (a : R) → S) r) :
    Localization.AtPrime I.asIdeal)
Tactic: change Localization.localRingHom _ _ _ rfl (algebraMap _ _ r) = algebraMap _ _ (f r)
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Maximal.Localization (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
hf : Function.Bijective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
r : R
I : MaximalSpectrum S
⊢ Eq.{u_2 + 1} (α := Localization.AtPrime I.asIdeal)
    (((Localization.localRingHom (Ideal.comap f I.asIdeal) I.asIdeal f ⋯ :
            RingHom.{u_1, u_2} (Localization.AtPrime (Ideal.comap f I.asIdeal)) (Localization.AtPrime I.asIdeal)) :
          (a : Localization.AtPrime (Ideal.comap f I.asIdeal)) → Localization.AtPrime I.asIdeal)
        ((algebraMap R (Localization.AtPrime (Ideal.comap f I.asIdeal)) :
            (a : R) → Localization.AtPrime (Ideal.comap f I.asIdeal))
          r) :
      Localization.AtPrime I.asIdeal)
    ((algebraMap S (Localization.AtPrime I.asIdeal) : (a : S) → Localization.AtPrime I.asIdeal) ((f : (a : R) → S) r) :
      Localization.AtPrime I.asIdeal)
have a : Eq.{u_2 + 1} (α := Localization.AtPrime I.asIdeal)
  (IsLocalization.mk' (R := S) (M := I.asIdeal.primeCompl) (Localization.AtPrime I.asIdeal) ((f : (a : R) → S) r : S)
    (Subtype.mk (p := fun (x : S) ↦ x ∈ I.asIdeal.primeCompl) 1 sorry : ↥I.asIdeal.primeCompl))
  (IsLocalization.mk' (R := S) (M := I.asIdeal.primeCompl) (Localization.AtPrime I.asIdeal) ((f : (a : R) → S) r : S)
    (1 : ↥I.asIdeal.primeCompl))
Tactic: simp_rw [← IsLocalization.mk'_one (M := (I.1.comap f).primeCompl), Localization.localRingHom_mk',
    ← IsLocalization.mk'_one (M := I.1.primeCompl), Submonoid.coe_one, map_one f]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Maximal.Localization (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f_1 : R →+* S
hf : Function.Bijective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f_1 : (a : R) → S)
f : R ≃+* S := RingEquiv.ofBijective f_1 hf
refine_3 :
  Function.Bijective.{u_1 + 1, u_2 + 1} (α := PiLocalization R) (β := PiLocalization S)
    (⇑(mapPiLocalization f_1 hf) : (a : PiLocalization R) → PiLocalization S)
⊢ Function.Bijective.{u_1 + 1, u_2 + 1} (α := PiLocalization R) (β := PiLocalization S)
    (⇑(mapPiLocalization f_1 hf) : (a : PiLocalization R) → PiLocalization S)
have refine_1 : (mapPiLocalization (↑f : R →+* S) hf).comp (mapPiLocalization (↑f.symm : S →+* R) sorry) = RingHom.id (PiLocalization S)
Tactic: let e := RingEquiv.ofRingHom (mapPiLocalization f hf)
    (mapPiLocalization (f.symm : S →+* R) f.symm.bijective) ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Maximal.Localization (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f_1 : R →+* S
hf : Function.Bijective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f_1 : (a : R) → S)
f : R ≃+* S := RingEquiv.ofBijective f_1 hf
refine_3 :
  Function.Bijective.{u_1 + 1, u_2 + 1} (α := PiLocalization R) (β := PiLocalization S)
    (⇑(mapPiLocalization f_1 hf) : (a : PiLocalization R) → PiLocalization S)
refine_1 :
  (mapPiLocalization (↑f : R →+* S) hf).comp (mapPiLocalization (↑f.symm : S →+* R) ⋯) = RingHom.id (PiLocalization S)
⊢ Function.Bijective.{u_1 + 1, u_2 + 1} (α := PiLocalization R) (β := PiLocalization S)
    (⇑(mapPiLocalization f_1 hf) : (a : PiLocalization R) → PiLocalization S)
have refine_2 : RingHom.comp (mapPiLocalization (↑f.symm : S →+* R) sorry) (mapPiLocalization (↑f : R →+* S) hf) =
  RingHom.id (PiLocalization R)
Tactic: let e := RingEquiv.ofRingHom (mapPiLocalization f hf)
    (mapPiLocalization (f.symm : S →+* R) f.symm.bijective) ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Maximal.Localization (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f_1 : R →+* S
hf : Function.Bijective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f_1 : (a : R) → S)
f : R ≃+* S := RingEquiv.ofBijective f_1 hf
⊢ (mapPiLocalization (↑f : R →+* S) hf).comp (mapPiLocalization (↑f.symm : S →+* R) ⋯) = RingHom.id (PiLocalization S)
have refine_1 : Eq (α := PiLocalization S →+* PiLocalization S)
  (mapPiLocalization (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f : R →+* S) (↑f.symm : S →+* R)) sorry)
  (RingHom.id (PiLocalization S))
Tactic: rw [← mapPiLocalization_comp]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Maximal.Localization (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f_1 : R →+* S
hf : Function.Bijective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f_1 : (a : R) → S)
f : R ≃+* S := RingEquiv.ofBijective f_1 hf
⊢ Eq (α := PiLocalization S →+* PiLocalization S)
    (mapPiLocalization (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f : R →+* S) (↑f.symm : S →+* R)) ⋯)
    (RingHom.id (PiLocalization S))
have refine_1 : Eq (α := PiLocalization S →+* PiLocalization S) (mapPiLocalization (RingHom.id S) sorry) (RingHom.id (PiLocalization S))
Tactic: simp_rw [RingEquiv.comp_symm, mapPiLocalization_id]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Maximal.Localization (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f_1 : R →+* S
hf : Function.Bijective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f_1 : (a : R) → S)
f : R ≃+* S := RingEquiv.ofBijective f_1 hf
⊢ RingHom.comp (mapPiLocalization (↑f.symm : S →+* R) ⋯) (mapPiLocalization (↑f : R →+* S) hf) =
    RingHom.id (PiLocalization R)
have refine_2 : Eq (α := PiLocalization R →+* PiLocalization R)
  (mapPiLocalization (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f.symm : S →+* R) (↑f : R →+* S)) sorry)
  (RingHom.id (PiLocalization R))
Tactic: rw [← mapPiLocalization_comp]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Maximal.Localization (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f_1 : R →+* S
hf : Function.Bijective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f_1 : (a : R) → S)
f : R ≃+* S := RingEquiv.ofBijective f_1 hf
⊢ Eq (α := PiLocalization R →+* PiLocalization R)
    (mapPiLocalization (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f.symm : S →+* R) (↑f : R →+* S)) ⋯)
    (RingHom.id (PiLocalization R))
have refine_2 : Eq (α := PiLocalization R →+* PiLocalization R) (mapPiLocalization (RingHom.id R) sorry) (RingHom.id (PiLocalization R))
Tactic: simp_rw [RingEquiv.symm_comp, mapPiLocalization_id]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Maximal.Localization (goal)
Goal:
ι : Type u_5
R : ι → Type u_4
inst : (i : ι) → CommSemiring (R i)
inst_1 : ∀ (i : ι), Nontrivial.{u_4} (R i)
inst_2 : Infinite ι
surj :
  Function.Surjective (α := (i : ι) → R i) (β := PiLocalization ((i : ι) → R i))
    (⇑(toPiLocalization ((i : ι) → R i)) : (a : (i : ι) → R i) → PiLocalization ((i : ι) → R i))
⊢ False
have have : ∀ (J : Ideal ((i : ι) → R i)) (max : J.IsMaximal)
  (notMem : { asIdeal := J, isPrime := sorry } ∉ Set.range (PrimeSpectrum.sigmaToPi R)), False
Tactic: have ⟨J, max, notMem⟩ := PrimeSpectrum.exists_maximal_notMem_range_sigmaToPi_of_infinite R
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Maximal.Localization (goal)
Goal:
ι : Type u_5
R : ι → Type u_4
inst : (i : ι) → CommSemiring (R i)
inst_1 : ∀ (i : ι), Nontrivial.{u_4} (R i)
inst_2 : Infinite ι
surj :
  Function.Surjective (α := (i : ι) → R i) (β := PiLocalization ((i : ι) → R i))
    (⇑(toPiLocalization ((i : ι) → R i)) : (a : (i : ι) → R i) → PiLocalization ((i : ι) → R i))
J : Ideal ((i : ι) → R i)
max : J.IsMaximal
notMem : { asIdeal := J, isPrime := ⋯ } ∉ Set.range (PrimeSpectrum.sigmaToPi R)
⊢ False
have obtain : ∀ (r : (i : ι) → R i)
  (hr :
    Eq (α := PiLocalization ((i : ι) → R i))
      ((toPiLocalization ((i : ι) → R i) : (a : (i : ι) → R i) → PiLocalization ((i : ι) → R i)) r :
        PiLocalization ((i : ι) → R i))
      (Function.update (β := fun (I : MaximalSpectrum ((i : ι) → R i)) ↦ Localization.AtPrime I.asIdeal) 0
          { asIdeal := J, isMaximal := max } 1 :
        (a : MaximalSpectrum ((i : ι) → R i)) → Localization.AtPrime a.asIdeal)),
  False
Tactic: obtain ⟨r, hr⟩ := surj (Function.update 0 ⟨J, max⟩ 1)