awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothOfFree
Goal:
R_1 : Type u_1
S_1 : Type u_2
inst : CommRing R_1
inst_1 : CommRing S_1
inst_2 : Algebra R_1 S_1
R : Type u_1
S : Type u_2
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : Algebra R S
inst_6 : FinitePresentation R S
p : Ideal S
inst_7 : p.IsPrime
inst_8 : IsSmoothAt R p
h : Smooth R S
κ : Type u_2
a : κ → S
b : Module.Basis κ (Localization.AtPrime p) Ω[Localization.AtPrime p⁄R]
hb :
  ∀ (i : κ),
    Eq (α := Ω[Localization.AtPrime p⁄R]) ((b : (a : κ) → Ω[Localization.AtPrime p⁄R]) i : Ω[Localization.AtPrime p⁄R])
      (Function.comp (β := Ω[S⁄R]) (⇑(map R R S (Localization.AtPrime p)) : (a : Ω[S⁄R]) → Ω[Localization.AtPrime p⁄R])
          (⇑(D R S) : (a : S) → Ω[S⁄R]) (a i) :
        Ω[Localization.AtPrime p⁄R])
e : (κ →₀ S) →ₗ[S] Ω[S⁄R] := Finsupp.linearCombination S fun (i : κ) ↦ (D R S : (a : S) → Ω[S⁄R]) (a i)
l₁ : (κ →₀ S) →ₗ[S] κ →₀ Localization.AtPrime p :=
  Finsupp.mapRange.linearMap (Algebra.linearMap S (Localization.AtPrime p))
l₂ : Ω[S⁄R] →ₗ[S] Ω[Localization.AtPrime p⁄R] := map R R S (Localization.AtPrime p)
eₚ : LinearMap (R := Localization.AtPrime p) (RingHom.id (Localization.AtPrime p)) (κ →₀ Localization.AtPrime p)
  Ω[Localization.AtPrime p⁄R] :=
  ((IsLocalizedModule.mapExtendScalars p.primeCompl l₁ l₂ (Localization.AtPrime p) :
        ((κ →₀ S) →ₗ[S] Ω[S⁄R]) →ₗ[S]
          LinearMap (R := Localization.AtPrime p) (RingHom.id (Localization.AtPrime p)) (κ →₀ Localization.AtPrime p)
            Ω[Localization.AtPrime p⁄R]) :
      (a : (κ →₀ S) →ₗ[S] Ω[S⁄R]) →
        (κ →₀ Localization.AtPrime p) →ₗ[Localization.AtPrime p] Ω[Localization.AtPrime p⁄R])
    e
this_1 : eₚ = (↑b.repr.symm : (κ →₀ Localization.AtPrime p) →ₗ[Localization.AtPrime p] Ω[Localization.AtPrime p⁄R])
heₚ :
  Function.Bijective (α := κ →₀ Localization.AtPrime p) (β := Ω[Localization.AtPrime p⁄R])
    (⇑eₚ : (a : κ →₀ Localization.AtPrime p) → Ω[Localization.AtPrime p⁄R])
this : Finite κ
obtain :
  ∀ (g : S) (hg : g ∉ p)
    (h :
      Function.Bijective (α := LocalizedModule (Submonoid.powers g) (κ →₀ S)) (β :=
        LocalizedModule (Submonoid.powers g) Ω[S⁄R])
        (⇑((LocalizedModule.map (Submonoid.powers g) :
                  (a : (κ →₀ S) →ₗ[S] Ω[S⁄R]) →
                    LocalizedModule (Submonoid.powers g) (κ →₀ S) →ₗ[Localization (Submonoid.powers g)]
                      LocalizedModule (Submonoid.powers g) Ω[S⁄R])
                e :
              LinearMap (R := Localization (Submonoid.powers g)) (RingHom.id (Localization (Submonoid.powers g)))
                (LocalizedModule (Submonoid.powers g) (κ →₀ S)) (LocalizedModule (Submonoid.powers g) Ω[S⁄R])) :
          (a : LocalizedModule (Submonoid.powers g) (κ →₀ S)) → LocalizedModule (Submonoid.powers g) Ω[S⁄R])),
    ∃ f ∉ p, IsStandardSmooth.{u_1, u_2} R (Localization.Away f)
⊢ ∃ f ∉ p, IsStandardSmooth.{u_1, u_2} R (Localization.Away f)

Tactic:
obtain ⟨g, hg, h⟩ := Module.FinitePresentation.exists_notMem_bijective e p l₁ l₂ heₚ

Premises used: Module.FinitePresentation.exists_notMem_bijective
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothOfFree
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
choose :
  ∀ (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))),
    ∃ (s : Set S), Eq (α := Ideal S) (Ideal.span s) ⊤ ∧ ∀ x ∈ s, IsStandardSmooth.{u_1, u_2} R (Localization.Away x)
⊢ ∃ (s : Set S), Eq (α := Ideal S) (Ideal.span s) ⊤ ∧ ∀ x ∈ s, IsStandardSmooth.{u_1, u_2} R (Localization.Away x)

Tactic:
choose f hf₁ hf₂ using IsSmoothAt.exists_notMem_isStandardSmooth R (S := S)

Premises used: Algebra.IsSmoothAt.exists_notMem_isStandardSmooth
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothOfFree
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))
simp : ∀ (a : PrimeSpectrum S), IsStandardSmooth.{u_1, u_2} R (Localization.Away (f a.asIdeal))
⊢ ∀ (x : S),
    Membership.mem (γ := Set S) (Set.range fun (p : PrimeSpectrum S) ↦ f p.asIdeal) x →
      IsStandardSmooth.{u_1, u_2} R (Localization.Away x)

Tactic:
simp only [Set.mem_range, forall_exists_index, forall_apply_eq_imp_iff]

Premises used: Set.mem_range, forall_exists_index, forall_apply_eq_imp_iff
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothOfFree
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))
a : PrimeSpectrum S
⊢ IsStandardSmooth.{u_1, u_2} R (Localization.Away (f a.asIdeal))

Tactic:
apply hf₂
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothOfFree
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))
refine : Eq.{u_2 + 1} (α := Ideal S) (Ideal.span (Set.range fun (p : PrimeSpectrum S) ↦ f p.asIdeal)) ⊤
⊢ ∃ (s : Set S), Eq (α := Ideal S) (Ideal.span s) ⊤ ∧ ∀ x ∈ s, IsStandardSmooth.{u_1, u_2} R (Localization.Away x)

Tactic:
refine ⟨Set.range (fun p : PrimeSpectrum S ↦ f p.asIdeal), ?_, by
    simp only [Set.mem_range, forall_exists_index, forall_apply_eq_imp_iff]; intro; apply hf₂⟩
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothOfFree
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))
simp : ∀ (x : PrimeSpectrum S), ∃ (i : PrimeSpectrum S), f i.asIdeal ∉ x.asIdeal
⊢ Eq.{u_2 + 1} (α := Ideal S) (Ideal.span (Set.range fun (p : PrimeSpectrum S) ↦ f p.asIdeal)) ⊤

Tactic:
simp [← PrimeSpectrum.iSup_basicOpen_eq_top_iff, TopologicalSpace.Opens.ext_iff, Set.ext_iff]

Premises used: PrimeSpectrum.iSup_basicOpen_eq_top_iff, Set.ext_iff, TopologicalSpace.Opens.ext_iff
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothOfFree
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))
⊢ ∀ (x : PrimeSpectrum S), ∃ (i : PrimeSpectrum S), f i.asIdeal ∉ x.asIdeal

Tactic:
grind
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Basic
Goal:
R : Type u_1
inst : CommSemiring R
⊢ Eq.{u_1 + 1} (α := Set (Ideal R)) (Set.range asIdeal) {J : Ideal R | J.IsMaximal}

Tactic:
Set.ext fun J ↦
    ⟨fun hJ ↦ let ⟨j, hj⟩ := Set.mem_range.mp hJ; Set.mem_setOf.mpr <| hj ▸ j.isMaximal,
      fun hJ ↦ Set.mem_range.mpr ⟨⟨J, Set.mem_setOf.mp hJ⟩, rfl⟩⟩

Premises used: Iff.mpr, Set.ext, Set.mem_range, _private.0.MaximalSpectrum.range_asIdeal.match_1, MaximalSpectrum.isMaximal, MaximalSpectrum.mk, setOf, Membership.mem, Eq.rec, Set.mem_setOf, Iff.intro, Exists.intro, Ideal.IsMaximal, Iff.mp, rfl
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Basic
Goal:
R : Type u_1
S : Type u_2
P : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring P
inst_3 : Nontrivial R
⊢ Nonempty.{u_1 + 1} (MaximalSpectrum R)

Tactic:
let ⟨I, hI⟩ := Ideal.exists_maximal R
  ⟨⟨I, hI⟩⟩

Premises used: Ideal.exists_maximal, MaximalSpectrum.mk, MaximalSpectrum, Nonempty.intro, _private.0.MaximalSpectrum.instNonemptyOfNontrivial.match_1, Nonempty
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Basic
Goal:
R : Type u_1
inst : CommSemiring R
x x_1 : MaximalSpectrum R
asIdeal : Ideal R
isMaximal : asIdeal.IsMaximal
asIdeal_1 : Ideal R
isMaximal_1 : asIdeal_1.IsMaximal
h :
  { asIdeal := asIdeal, isMaximal := isMaximal : MaximalSpectrum R }.toPrimeSpectrum =
    { asIdeal := asIdeal_1, isMaximal := isMaximal_1 }.toPrimeSpectrum
⊢ { asIdeal := asIdeal, isMaximal := isMaximal : MaximalSpectrum R } =
    { asIdeal := asIdeal_1, isMaximal := isMaximal_1 }

Tactic:
simpa only [MaximalSpectrum.mk.injEq] using PrimeSpectrum.ext_iff.mp h

Premises used: MaximalSpectrum.mk.injEq, PrimeSpectrum.ext_iff, Iff.mp
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Basic
Goal:
R : Type u_1
inst : CommSemiring R
I J : MaximalSpectrum R
h : I ≠ J
⊢ IsCoprime I.asIdeal J.asIdeal

Tactic:
Ideal.isCoprime_iff_sup_eq.mpr <| I.2.coprime_of_ne J.2 <| mt MaximalSpectrum.ext h

Premises used: Iff.mpr, MaximalSpectrum.isMaximal, mt, Ideal.IsMaximal.coprime_of_ne, MaximalSpectrum.ext, Ideal.isCoprime_iff_sup_eq
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
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
h :
  ∀ (x : K),
    Membership.mem (γ := Subalgebra R K)
        (⨅ (v : MaximalSpectrum R), Localization.subalgebra.ofField K v.asIdeal.primeCompl ⋯) x ↔
      Membership.mem (γ := Subalgebra R K) ⊥ x
⊢ Eq.{u_5 + 1} (α := Subalgebra R K)
    (⨅ (v : MaximalSpectrum R), Localization.subalgebra.ofField K v.asIdeal.primeCompl ⋯) ⊥

Tactic:
ext x
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
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
⊢ Membership.mem (γ := Subalgebra R K)
      (⨅ (v : MaximalSpectrum R), Localization.subalgebra.ofField K v.asIdeal.primeCompl ⋯) x ↔
    Membership.mem (γ := Subalgebra R K) ⊥ x

Tactic:
rw [Algebra.mem_bot, Algebra.mem_iInf]

Premises used: Algebra.mem_iInf, Algebra.mem_bot
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
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
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 ⋯) 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

Tactic:
constructor
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
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 :
  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 ⋯) 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

Tactic:
contrapose
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
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
⊢ 1 ∉ denom

Tactic:
simpa [denom] using hrange
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
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
⊢ 1 ∉ denom

Tactic:
have hdenom : (1 : R) ∉ denom := by simpa [denom] using hrange
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
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
h : ∀ (max : Ideal R) (hmax : max.IsMaximal) (hle : denom ≤ max), False
⊢ False

Tactic:
rcases denom.exists_le_maximal (denom.ne_top_iff_one.mpr hdenom) with ⟨max, hmax, hle⟩

Premises used: Iff.mpr, Ideal.ne_top_iff_one, Max.max, Ideal.exists_le_maximal
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
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
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 ⋯)
          (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
⊢ False

Tactic:
rcases hlocal ⟨max, hmax⟩ with ⟨n, d, hd, rfl⟩

Premises used: MaximalSpectrum.mk, rfl
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
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
max : Ideal R
hmax : max.IsMaximal
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 ⋯)
      (HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) n : K) (((algebraMap R K : (a : R) → K) d)⁻¹ : K))
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
⊢ Eq.{u_5 + 1} (α := K) ((LinearMap.toSpanSingleton R K 1 : (a : R) → K) n : K)
    ((LinearMap.toSpanSingleton R K
            (HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) n : K)
              (((algebraMap R K : (a : R) → K) d)⁻¹ : K)) :
          (a : R) → K)
        d :
      K)

Tactic:
simp [Algebra.smul_def, mul_left_comm, mul_inv_cancel₀ <|
      (map_ne_zero_iff _ <| IsFractionRing.injective R K).mpr fun h ↦ hd (h ▸ max.zero_mem :)]

Premises used: Iff.mpr, mul_inv_cancel₀, IsFractionRing.injective, Eq.rec, mul_left_comm, Ideal.zero_mem, Algebra.smul_def, map_ne_zero_iff, Eq.symm
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
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
max : Ideal R
hmax : max.IsMaximal
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 ⋯)
      (HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) n : K) (((algebraMap R K : (a : R) → K) d)⁻¹ : K))
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:
exact hd (hle ⟨n, by simp [Algebra.smul_def, mul_left_comm, mul_inv_cancel₀ <|
      (map_ne_zero_iff _ <| IsFractionRing.injective R K).mpr fun h ↦ hd (h ▸ max.zero_mem :)]⟩)

Premises used: Exists.intro
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
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)
rw₂ rw₃ : Eq.{u_5 + 1} (α := K) ((algebraMap R K : (a : R) → K) y : K) ((algebraMap R K : (a : R) → K) y : 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)

Tactic:
rw [map_one, inv_one, mul_one]

Premises used: inv_one, map_one, mul_one
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
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
⊢ Membership.mem (α := K) (γ := Subalgebra R K)
    (Localization.subalgebra.ofField K { asIdeal := v, isMaximal := hv }.asIdeal.primeCompl ⋯)
    ((algebraMap R K : (a : R) → K) y : K)

Tactic:
exact ⟨y, 1, v.ne_top_iff_one.mp hv.ne_top, by rw [map_one, inv_one, mul_one]⟩
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
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 ⋯)
    ⊥

Tactic:
bot_unique (.trans (fun _ ↦ ?_) (MaximalSpectrum.iInf_localization_eq_bot R K).le)

Premises used: Eq.le, MaximalSpectrum.iInf_localization_eq_bot, bot_unique, LE.le.trans
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
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
refine :
  ∀ (x : K),
    Membership.mem (γ := Subalgebra R K)
        (⨅ (v : PrimeSpectrum R), Localization.subalgebra.ofField K v.asIdeal.primeCompl ⋯) x →
      Membership.mem (γ := Subalgebra R K)
        (⨅ (v : MaximalSpectrum R), Localization.subalgebra.ofField K v.asIdeal.primeCompl ⋯) x
⊢ Eq.{u_5 + 1} (α := Subalgebra R K) (⨅ (v : PrimeSpectrum R), Localization.subalgebra.ofField K v.asIdeal.primeCompl ⋯)
    ⊥

Tactic:
refine bot_unique (.trans (fun _ ↦ ?_) (MaximalSpectrum.iInf_localization_eq_bot R K).le)

Premises used: Eq.le, MaximalSpectrum.iInf_localization_eq_bot, bot_unique, LE.le.trans
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
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 : PrimeSpectrum R), Localization.subalgebra.ofField K v.asIdeal.primeCompl ⋯) x →
    Membership.mem (γ := Subalgebra R K)
      (⨅ (v : MaximalSpectrum R), Localization.subalgebra.ofField K v.asIdeal.primeCompl ⋯) x

Tactic:
simpa only [Algebra.mem_iInf] using fun hx ⟨v, hv⟩ ↦ hx ⟨v, hv.isPrime⟩

Premises used: Algebra.mem_iInf
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
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)
rw : 1 * r = 1 * r'
⊢ r = r'

Tactic:
rw [← one_mul r, ← one_mul r']

Premises used: one_mul
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
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)
by_contra : ∀ (ne : ¬1 * r = 1 * r'), False
⊢ 1 * r = 1 * r'

Tactic:
by_contra ne
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
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'
have : ∀ (I : Ideal R) (mI : I.IsMaximal) (hI : Module.eqIdeal R r r' ≤ I), False
⊢ False

Tactic:
have ⟨I, mI, hI⟩ := (Module.eqIdeal R r r').exists_le_maximal ((Ideal.ne_top_iff_one _).mpr ne)
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
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
have : ∀ (s : ↥I.primeCompl) (hs : (↑s : R) * r = (↑s : R) * r'), False
⊢ False

Tactic:
have ⟨s, hs⟩ := (IsLocalization.eq_iff_exists I.primeCompl _).mp (congr_fun eq ⟨I, mI⟩)
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
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
s : ↥I.primeCompl
hs : (↑s : R) * r = (↑s : R) * r'
⊢ False

Tactic:
s.2 (hI hs)

Premises used: Subtype.property