awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Ideal S
inst_3 : P.IsPrime
s : Subalgebra R S
H : s.saturation (P.primeCompl ⊓ s.toSubmonoid) ⋯ = ⊤
p : Ideal ↥s
inst_4 : p.IsPrime
inst_5 : P.LiesOver p
y z : S
hzP : z ∉ P
right :
  ∀ (a : S) (ha : a * y ∈ s) (haP : a ∈ (↑P.primeCompl : Set S)) (has : a ∈ (↑s.toSubmonoid : Set S)),
    ∃ y' ∈ s, ∃ z' ∉ P, z' ∈ s ∧ ∃ t ∉ P, t * (z * y') = t * (z' * y)
⊢ ∃ y' ∈ s, ∃ z' ∉ P, z' ∈ s ∧ ∃ t ∉ P, t * (z * y') = t * (z' * y)

Tactic:
obtain ⟨a, ⟨haP, has⟩, ha⟩ := H.ge (Set.mem_univ y)

Premises used: Eq.ge, Set.mem_univ
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Ideal S
inst_3 : P.IsPrime
s : Subalgebra R S
H : s.saturation (P.primeCompl ⊓ s.toSubmonoid) ⋯ = ⊤
p : Ideal ↥s
inst_4 : p.IsPrime
inst_5 : P.LiesOver p
y z : S
hzP : z ∉ P
a : S
ha : a * y ∈ s
haP : a ∈ (↑P.primeCompl : Set S)
has : a ∈ (↑s.toSubmonoid : Set S)
right :
  ∀ (b : S) (hb : b * z ∈ s) (hbP : b ∈ (↑P.primeCompl : Set S)) (hbs : b ∈ (↑s.toSubmonoid : Set S)),
    ∃ y' ∈ s, ∃ z' ∉ P, z' ∈ s ∧ ∃ t ∉ P, t * (z * y') = t * (z' * y)
⊢ ∃ y' ∈ s, ∃ z' ∉ P, z' ∈ s ∧ ∃ t ∉ P, t * (z * y') = t * (z' * y)

Tactic:
obtain ⟨b, ⟨hbP, hbs⟩, hb⟩ := H.ge (Set.mem_univ z)

Premises used: Eq.ge, Set.mem_univ
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Ideal S
inst_3 : P.IsPrime
s : Subalgebra R S
H : s.saturation (P.primeCompl ⊓ s.toSubmonoid) ⋯ = ⊤
p : Ideal ↥s
inst_4 : p.IsPrime
inst_5 : P.LiesOver p
y z : S
hzP : z ∉ P
a : S
ha : a * y ∈ s
haP : a ∈ (↑P.primeCompl : Set S)
has : a ∈ (↑s.toSubmonoid : Set S)
b : S
hb : b * z ∈ s
hbP : b ∈ (↑P.primeCompl : Set S)
hbs : b ∈ (↑s.toSubmonoid : Set S)
⊢ 1 * (z * (a * y * b)) = 1 * (b * z * a * y)

Tactic:
ring
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Ideal S
inst_3 : P.IsPrime
s : Subalgebra R S
H : s.saturation (P.primeCompl ⊓ s.toSubmonoid) ⋯ = ⊤
p : Ideal ↥s
inst_4 : p.IsPrime
inst_5 : P.LiesOver p
y z : S
hzP : z ∉ P
a : S
ha : a * y ∈ s
haP : a ∈ (↑P.primeCompl : Set S)
has : a ∈ (↑s.toSubmonoid : Set S)
b : S
hb : b * z ∈ s
hbP : b ∈ (↑P.primeCompl : Set S)
hbs : b ∈ (↑s.toSubmonoid : Set S)
⊢ ∃ y' ∈ s, ∃ z' ∉ P, z' ∈ s ∧ ∃ t ∉ P, t * (z * y') = t * (z' * y)

Tactic:
exact ⟨_, mul_mem ha hbs, _, P.primeCompl.mul_mem (mul_mem hbP hzP) haP, mul_mem hb has, 1,
      P.primeCompl.one_mem, by ring⟩
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P_1 : Type u_3
inst_3 : CommSemiring P_1
I : Ideal R
hI : I.IsPrime
A : Type u_4
B : Type u_5
C : Type u_6
inst_4 : CommRing A
inst_5 : CommRing B
inst_6 : CommRing C
inst_7 : Algebra A B
inst_8 : Algebra A C
inst_9 : Algebra R A
inst_10 : Algebra R B
inst_11 : IsScalarTower R A B
inst_12 : Algebra B C
inst_13 : IsScalarTower A B C
p : Ideal A
inst_14 : p.IsPrime
P : Ideal B
inst_15 : P.IsPrime
inst_16 : P.LiesOver p
⊢ IsLiesOverAlgebra p P

Tactic:
letI := algebraOfLiesOver p P; ⟨rfl⟩

Premises used: Localization.AtPrime.IsLiesOverAlgebra.mk, rfl
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P_1 : Type u_3
inst_3 : CommSemiring P_1
I : Ideal R
hI : I.IsPrime
A : Type u_4
B : Type u_5
C : Type u_6
inst_4 : CommRing A
inst_5 : CommRing B
inst_6 : CommRing C
inst_7 : Algebra A B
inst_8 : Algebra A C
inst_9 : Algebra R A
inst_10 : Algebra R B
inst_11 : IsScalarTower R A B
inst_12 : Algebra B C
inst_13 : IsScalarTower A B C
p : Ideal A
inst_14 : p.IsPrime
P : Ideal B
inst_15 : P.IsPrime
inst_16 : P.LiesOver p
inst_17 : Algebra.{u_4, u_5} (Localization.AtPrime p) (Localization.AtPrime P)
inst_18 : IsLiesOverAlgebra p P
⊢ ∀ (x : R),
    Eq.{u_5 + 1} (α := Localization.AtPrime P)
      ((algebraMap R (Localization.AtPrime P) : (a : R) → Localization.AtPrime P) x : Localization.AtPrime P)
      ((algebraMap (Localization.AtPrime p) (Localization.AtPrime P) :
            (a : Localization.AtPrime p) → Localization.AtPrime P)
          ((algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) x) :
        Localization.AtPrime P)

Tactic:
simp [IsScalarTower.algebraMap_apply R A (Localization.AtPrime p),
      Localization.localRingHom_to_map, IsScalarTower.algebraMap_apply R B (Localization.AtPrime P),
      IsScalarTower.algebraMap_apply R A B, IsLiesOverAlgebra.algebraMap_eq]

Premises used: Localization.localRingHom_to_map, Localization.AtPrime, Localization.AtPrime.IsLiesOverAlgebra.algebraMap_eq, IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P_1 : Type u_3
inst_3 : CommSemiring P_1
I : Ideal R
hI : I.IsPrime
A : Type u_4
B : Type u_5
C : Type u_6
inst_4 : CommRing A
inst_5 : CommRing B
inst_6 : CommRing C
inst_7 : Algebra A B
inst_8 : Algebra A C
inst_9 : Algebra R A
inst_10 : Algebra R B
inst_11 : IsScalarTower R A B
inst_12 : Algebra B C
inst_13 : IsScalarTower A B C
p : Ideal A
inst_14 : p.IsPrime
P : Ideal B
inst_15 : P.IsPrime
inst_16 : P.LiesOver p
Q : Ideal C
inst_17 : Q.IsPrime
inst_18 : Q.LiesOver P
inst_19 : Q.LiesOver p
inst_20 : Algebra.{u_4, u_5} (Localization.AtPrime p) (Localization.AtPrime P)
inst_21 : IsLiesOverAlgebra p P
inst_22 : Algebra.{u_5, u_6} (Localization.AtPrime P) (Localization.AtPrime Q)
inst_23 : IsLiesOverAlgebra P Q
inst_24 : Algebra.{u_4, u_6} (Localization.AtPrime p) (Localization.AtPrime Q)
inst_25 : IsLiesOverAlgebra p Q
⊢ Eq (α := RingHom.{u_4, u_6} (Localization.AtPrime p) (Localization.AtPrime Q))
    (algebraMap (Localization.AtPrime p) (Localization.AtPrime Q))
    (@RingHom.comp.{u_4, u_5, u_6} _ (Localization.AtPrime P) _ _ Semiring.toNonAssocSemiring _
      (algebraMap (Localization.AtPrime P) (Localization.AtPrime Q))
      (algebraMap (Localization.AtPrime p) (Localization.AtPrime P)))

Tactic:
simp [IsLiesOverAlgebra.algebraMap_eq, ← localRingHom_comp, ← IsScalarTower.algebraMap_eq]

Premises used: Localization.AtPrime.IsLiesOverAlgebra.algebraMap_eq, IsScalarTower.algebraMap_eq, Localization.localRingHom_comp
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
ι : Type u_4
R : ι → Type u_5
inst : (i : ι) → CommSemiring (R i)
i : ι
I : Ideal (R i)
inst_1 : I.IsPrime
⊢ Function.Bijective (α := Localization.AtPrime (Ideal.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) I))
    (β := Localization.AtPrime I)
    (⇑(mapPiEvalRingHom (R := R) I) :
      (a : Localization.AtPrime (Ideal.comap (Pi.evalRingHom R i) I)) → Localization.AtPrime I)

Tactic:
Localization.mapPiEvalRingHom_bijective _

Premises used: Set.Mem, setOf, Localization.mapPiEvalRingHom_bijective, Set.preimage, Ideal.primeCompl, Not
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
ι : Type u_4
R : ι → Type u_5
inst : (i : ι) → CommSemiring (R i)
i : ι
I : Ideal (R i)
inst_1 : I.IsPrime
⊢ Eq (α := ((i : ι) → R i) →+* Localization.AtPrime I)
    (RingHom.comp (mapPiEvalRingHom (R := R) I)
      (algebraMap ((i : ι) → R i)
        (Localization.AtPrime (Ideal.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) I))))
    (RingHom.comp (algebraMap (R i) (Localization.AtPrime I)) (Pi.evalRingHom R i))

Tactic:
IsLocalization.map_comp _

Premises used: Set.Mem, Localization.localRingHom, setOf, IsLocalization.map_comp
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
ι : Type u_4
R : ι → Type u_5
inst : (i : ι) → CommSemiring (R i)
i : ι
I : Ideal (R i)
inst_1 : I.IsPrime
r : (i : ι) → R i
⊢ Eq.{u_5 + 1} (α := Localization.AtPrime I)
    ((mapPiEvalRingHom (R := R) I :
          (a : Localization.AtPrime (Ideal.comap (Pi.evalRingHom R i) I)) → Localization.AtPrime I)
        ((algebraMap ((i : ι) → R i)
              (Localization.AtPrime (Ideal.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) I)) :
            (a : (i : ι) → R i) → Localization.AtPrime (Ideal.comap (Pi.evalRingHom R i) I))
          r) :
      Localization.AtPrime I)
    ((algebraMap (R i) (Localization.AtPrime I) : (a : R i) → Localization.AtPrime I) (r i) : Localization.AtPrime I)

Tactic:
localRingHom_to_map ..

Premises used: Localization.localRingHom_to_map, Set.Mem, setOf
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
q : Ideal R
inst_1 : q.IsPrime
S : Type u_4
inst_2 : CommSemiring S
inst_3 : Algebra R S
inst_4 : IsLocalization.AtPrime S q
p : Ideal R
inst_5 : p.IsPrime
hpq : p ≤ q
⊢ Disjoint (↑q.primeCompl : Set R) (↑p : Set R)

Tactic:
simp [Ideal.primeCompl, ← le_compl_iff_disjoint_left, hpq]

Premises used: le_compl_iff_disjoint_left, Ideal.primeCompl
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
q : Ideal R
inst_1 : q.IsPrime
S : Type u_4
inst_2 : CommSemiring S
inst_3 : Algebra R S
inst_4 : IsLocalization.AtPrime S q
p : Ideal R
inst_5 : p.IsPrime
hpq : p ≤ q
⊢ Disjoint (↑q.primeCompl : Set R) (↑p : Set R)

Tactic:
have disj : Disjoint (q.primeCompl : Set R) p := by
    simp [Ideal.primeCompl, ← le_compl_iff_disjoint_left, hpq]
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
q : Ideal R
inst_1 : q.IsPrime
S : Type u_4
inst_2 : CommSemiring S
inst_3 : Algebra R S
inst_4 : IsLocalization.AtPrime S q
p : Ideal R
inst_5 : p.IsPrime
hpq : p ≤ q
disj : Disjoint (↑q.primeCompl : Set R) (↑p : Set R)
⊢ p.IsPrime

Tactic:
simpa
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
q : Ideal R
inst_1 : q.IsPrime
S : Type u_4
inst_2 : CommSemiring S
inst_3 : Algebra R S
inst_4 : IsLocalization.AtPrime S q
p : Ideal R
inst_5 : p.IsPrime
hpq : p ≤ q
disj : Disjoint (↑q.primeCompl : Set R) (↑p : Set R)
⊢ IsPrime.{u_4} (α := S) (map (F := R →+* S) (algebraMap R S) p)

Tactic:
apply IsLocalization.isPrime_of_isPrime_disjoint q.primeCompl _ p (by simpa) disj

Premises used: IsLocalization.isPrime_of_isPrime_disjoint, Ideal.primeCompl
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
q : Ideal R
inst_1 : q.IsPrime
S : Type u_4
inst_2 : CommSemiring S
inst_3 : Algebra R S
inst_4 : IsLocalization.AtPrime S q
p : Ideal R
inst_5 : p.IsPrime
hpq : p ≤ q
disj : Disjoint (↑q.primeCompl : Set R) (↑p : Set R)
⊢ under.{u_1, u_4} R (B := S) (map (F := R →+* S) (algebraMap R S) p) = p

Tactic:
exact IsLocalization.under_map_of_isPrime_disjoint _ _ (by simpa) disj

Premises used: IsLocalization.under_map_of_isPrime_disjoint
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_5
inst : CommSemiring R
p : Ideal R
hp : Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) p
S : Type u_6
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization.AtPrime S p
this : p.IsPrime
⊢ { asIdeal := p, isPrime := ⋯ : PrimeSpectrum R } ∈ Set.Iic { asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }

Tactic:
fun ⦃x⦄ a ↦ a

Premises used: Set.Mem, setOf, Set.Iic
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_5
inst : CommSemiring R
p : Ideal R
hp : Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) p
S : Type u_6
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization.AtPrime S p
this : p.IsPrime
⊢ { asIdeal := p, isPrime := ⋯ : PrimeSpectrum R } ∈ Set.Iic { asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }

Tactic:
exact
    fun ⦃x⦄ a ↦ a
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_4
inst_1 : CommSemiring S
inst_2 : Algebra R S
R' : Type u_5
S' : Type u_6
M : Submonoid R
T : Submonoid S
inst_3 : CommSemiring R'
inst_4 : CommSemiring S'
inst_5 : Algebra R R'
inst_6 : Algebra S S'
inst_7 : Algebra R' S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R S S'
inst_10 : IsScalarTower R R' S'
inst_11 : IsLocalization M R'
inst_12 : IsLocalization T S'
p : Ideal R
P : Ideal S
inst_13 : P.IsPrime
inst_14 : P.LiesOver p
disj : Disjoint (↑T : Set S) (↑P : Set S)
h :
  Eq.{u_5 + 1} (α := Ideal R')
    (Ideal.map (F := R →+* R') (algebraMap R R')
      (under R (under.{u_5, u_6} R' (B := S') (Ideal.map (F := S →+* S') (algebraMap S S') P))))
    (Ideal.map (F := R →+* R') (algebraMap R R') p)
rw :
  Eq (α := Ideal R')
    (Ideal.map (F := R →+* R') (algebraMap R R')
      (under R (under.{u_5, u_6} R' (B := S') (Ideal.map (F := S →+* S') (algebraMap S S') P))))
    (under.{u_5, u_6} R' (B := S') (Ideal.map (F := S →+* S') (algebraMap S S') P))
rw₁ rw₂ :
  Eq (α := Ideal R') (under.{u_5, u_6} R' (B := S') (Ideal.map (F := S →+* S') (algebraMap S S') P))
    (under.{u_5, u_6} R' (B := S') (Ideal.map (F := S →+* S') (algebraMap S S') P))
⊢ Eq (α := Ideal R') (Ideal.map (F := R →+* R') (algebraMap R R') p)
    (under.{u_5, u_6} R' (B := S') (Ideal.map (F := S →+* S') (algebraMap S S') P))

Tactic:
rw [← h, IsLocalization.map_under (M := M)]

Premises used: IsLocalization.map_under
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_4
inst_1 : CommSemiring S
inst_2 : Algebra R S
R' : Type u_5
S' : Type u_6
M : Submonoid R
T : Submonoid S
inst_3 : CommSemiring R'
inst_4 : CommSemiring S'
inst_5 : Algebra R R'
inst_6 : Algebra S S'
inst_7 : Algebra R' S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R S S'
inst_10 : IsScalarTower R R' S'
inst_11 : IsLocalization M R'
inst_12 : IsLocalization T S'
p : Ideal R
P : Ideal S
inst_13 : P.IsPrime
inst_14 : P.LiesOver p
disj : Disjoint (↑T : Set S) (↑P : Set S)
suffices :
  Eq.{u_5 + 1} (α := Ideal R')
    (Ideal.map (F := R →+* R') (algebraMap R R')
      (under R (under.{u_5, u_6} R' (B := S') (Ideal.map (F := S →+* S') (algebraMap S S') P))))
    (Ideal.map (F := R →+* R') (algebraMap R R') p)
⊢ LiesOver.{u_5, u_6} (A := R') (B := S') (Ideal.map (F := S →+* S') (algebraMap S S') P)
    (Ideal.map (F := R →+* R') (algebraMap R R') p)

Tactic:
suffices h : Ideal.map (algebraMap R R') (under R (under R' (P.map (algebraMap S S')))) =
      Ideal.map (algebraMap R R') p from ⟨by rw [← h, IsLocalization.map_under (M := M)]⟩
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_4
inst_1 : CommSemiring S
inst_2 : Algebra R S
R' : Type u_5
S' : Type u_6
M : Submonoid R
T : Submonoid S
inst_3 : CommSemiring R'
inst_4 : CommSemiring S'
inst_5 : Algebra R R'
inst_6 : Algebra S S'
inst_7 : Algebra R' S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R S S'
inst_10 : IsScalarTower R R' S'
inst_11 : IsLocalization M R'
inst_12 : IsLocalization T S'
p : Ideal R
P : Ideal S
inst_13 : P.IsPrime
inst_14 : P.LiesOver p
disj : Disjoint (↑T : Set S) (↑P : Set S)
rw :
  Eq.{u_5 + 1} (α := Ideal R')
    (Ideal.map (F := R →+* R') (algebraMap R R')
      (under.{u_1, u_6} R (B := S') (Ideal.map (F := S →+* S') (algebraMap S S') P)))
    (Ideal.map (F := R →+* R') (algebraMap R R') p)
rw₁ :
  Eq.{u_5 + 1} (α := Ideal R')
    (Ideal.map (F := R →+* R') (algebraMap R R')
      (under R (under.{u_4, u_6} S (B := S') (Ideal.map (F := S →+* S') (algebraMap S S') P))))
    (Ideal.map (F := R →+* R') (algebraMap R R') p)
rw₂ :
  Eq.{u_5 + 1} (α := Ideal R') (Ideal.map (F := R →+* R') (algebraMap R R') (under R P))
    (Ideal.map (F := R →+* R') (algebraMap R R') p)
rw₃ rw₄ :
  Eq.{u_5 + 1} (α := Ideal R') (Ideal.map (F := R →+* R') (algebraMap R R') (under R P))
    (Ideal.map (F := R →+* R') (algebraMap R R') (under R P))
⊢ Eq.{u_5 + 1} (α := Ideal R')
    (Ideal.map (F := R →+* R') (algebraMap R R')
      (under R (under.{u_5, u_6} R' (B := S') (Ideal.map (F := S →+* S') (algebraMap S S') P))))
    (Ideal.map (F := R →+* R') (algebraMap R R') p)

Tactic:
rw [under_under, ← under_under (B := S), under_map_of_isPrime_disjoint _ _ ‹_› disj,
    LiesOver.over (P := P) (p := p)]

Premises used: Ideal.under_under, Ideal.LiesOver.over, IsLocalization.under_map_of_isPrime_disjoint
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_4
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
inst_4 : IsMaximal (under.{u_1, u_4} R (B := S) ⊤)
⊢ Eq (α := Ideal R) (under.{u_1, u_4} R (B := S) ⊤) ⊤

Tactic:
simp
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_4
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
inst_4 : IsMaximal (under.{u_1, u_4} R (B := S) ⊤)
⊢ False

Tactic:
exact Ideal.IsMaximal.ne_top ‹_› (by simp)

Premises used: Ideal.IsMaximal.ne_top
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_4
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
J : Ideal S
inst_4 : IsMaximal (under R J)
obtain : ∀ (m : Ideal S) (maxm : m.IsMaximal) (hm : J ≤ m), J.IsMaximal
⊢ J.IsMaximal

Tactic:
obtain ⟨m, maxm, hm⟩ := exists_le_maximal J <| by
    rintro rfl
    exact Ideal.IsMaximal.ne_top ‹_› (by simp)

Premises used: Ideal.exists_le_maximal
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_4
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
J : Ideal S
inst_4 : IsMaximal (under R J)
m : Ideal S
maxm : m.IsMaximal
hm : J ≤ m
⊢ LE.le (α := Ideal R) (under R J) (under R m)

Tactic:
replace hm : under R J ≤ under R m := comap_mono hm
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_4
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
J : Ideal S
inst_4 : IsMaximal (under R J)
m : Ideal S
maxm : m.IsMaximal
hm : LE.le (α := Ideal R) (under R J) (under R m)
rwa : IsMaximal.{u_4} (α := S) (map (F := R →+* S) (algebraMap R S) (under R J))
rwa₁ : IsMaximal.{u_4} (α := S) (map (F := R →+* S) (algebraMap R S) (under R m))
rwa₂ rwa₃ rwa₄ rwa₅ : m.IsMaximal
⊢ J.IsMaximal

Tactic:
rwa [← IsLocalization.map_under M S J, IsMaximal.eq_of_le ‹_› (IsPrime.under R m).ne_top hm,
    IsLocalization.map_under M S m]

Premises used: IsLocalization.map_under, Ideal.IsMaximal.eq_of_le, Ideal.IsPrime.under, Ideal.IsPrime.ne_top
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
Sₚ : Type u_5
inst_4 : CommSemiring Sₚ
inst_5 : Algebra S Sₚ
inst_6 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
P : Ideal S
inst_7 : P.IsPrime
inst_8 : P.LiesOver p
⊢ IsPrime.{u_5} (α := Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)

Tactic:
isPrime_of_isPrime_disjoint _ _ _ inferInstance (Ideal.disjoint_primeCompl_of_liesOver P p)

Premises used: inferInstance, IsLocalization.isPrime_of_isPrime_disjoint, Ideal.disjoint_primeCompl_of_liesOver
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
p : Ideal R
inst_1 : p.IsPrime
Rₚ : Type u_4
inst_2 : CommSemiring Rₚ
inst_3 : Algebra R Rₚ
inst_4 : IsLocalization.AtPrime Rₚ p
inst_5 : IsLocalRing Rₚ
⊢ Eq.{u_4 + 1} (α := Ideal Rₚ) (Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) p)
    (Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) (under R (maximalIdeal Rₚ)))

Tactic:
congr_arg (Ideal.map (algebraMap R Rₚ)) (under_maximalIdeal Rₚ p).symm

Premises used: Algebra.algebraMap, Ideal.map, congr_arg, IsLocalization.AtPrime.isLocalRing, IsLocalization.AtPrime.under_maximalIdeal, Eq.symm
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
p : Ideal R
inst_1 : p.IsPrime
Rₚ : Type u_4
inst_2 : CommSemiring Rₚ
inst_3 : Algebra R Rₚ
inst_4 : IsLocalization.AtPrime Rₚ p
inst_5 : IsLocalRing Rₚ
h : Eq (α := Ideal Rₚ) (maximalIdeal Rₚ) (Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) (under R (maximalIdeal Rₚ)))
⊢ Eq (α := Ideal Rₚ) (Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) p) (maximalIdeal Rₚ)

Tactic:
convert! congr_arg (Ideal.map (algebraMap R Rₚ)) (under_maximalIdeal Rₚ p).symm

Premises used: Algebra.algebraMap, Ideal.map, congr_arg, IsLocalization.AtPrime.isLocalRing, IsLocalization.AtPrime.under_maximalIdeal, Eq.symm
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
p : Ideal R
inst_1 : p.IsPrime
Rₚ : Type u_4
inst_2 : CommSemiring Rₚ
inst_3 : Algebra R Rₚ
inst_4 : IsLocalization.AtPrime Rₚ p
inst_5 : IsLocalRing Rₚ
h h₁ : Eq (α := Ideal Rₚ) (maximalIdeal Rₚ) (maximalIdeal Rₚ)
⊢ Eq (α := Ideal Rₚ) (maximalIdeal Rₚ) (Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) (under R (maximalIdeal Rₚ)))

Tactic:
rw [map_under p.primeCompl]

Premises used: IsLocalization.map_under, Ideal.primeCompl
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P_1 : Type u_3
inst_3 : CommSemiring P_1
p : Ideal R
inst_4 : p.IsPrime
Rₚ : Type u_4
inst_5 : CommSemiring Rₚ
inst_6 : Algebra R Rₚ
inst_7 : IsLocalization.AtPrime Rₚ p
inst_8 : IsLocalRing Rₚ
Sₚ : Type u_5
inst_9 : CommSemiring Sₚ
inst_10 : Algebra S Sₚ
inst_11 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst_12 : Algebra Rₚ Sₚ
P : Ideal S
rw : IsMaximal (maximalIdeal Rₚ)
⊢ IsMaximal.{u_4} (α := Rₚ) (Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) p)

Tactic:
rw [map_eq_maximalIdeal]

Premises used: IsLocalization.AtPrime.map_eq_maximalIdeal
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P_1 : Type u_3
inst_3 : CommSemiring P_1
p : Ideal R
inst_4 : p.IsPrime
Rₚ : Type u_4
inst_5 : CommSemiring Rₚ
inst_6 : Algebra R Rₚ
inst_7 : IsLocalization.AtPrime Rₚ p
inst_8 : IsLocalRing Rₚ
Sₚ : Type u_5
inst_9 : CommSemiring Sₚ
inst_10 : Algebra S Sₚ
inst_11 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst_12 : Algebra Rₚ Sₚ
P : Ideal S
⊢ IsMaximal (maximalIdeal Rₚ)

Tactic:
maximalIdeal.isMaximal Rₚ

Premises used: IsLocalRing.maximalIdeal.isMaximal
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P_1 : Type u_3
inst_3 : CommSemiring P_1
p : Ideal R
inst_4 : p.IsPrime
Rₚ : Type u_4
inst_5 : CommSemiring Rₚ
inst_6 : Algebra R Rₚ
inst_7 : IsLocalization.AtPrime Rₚ p
inst_8 : IsLocalRing Rₚ
Sₚ : Type u_5
inst_9 : CommSemiring Sₚ
inst_10 : Algebra S Sₚ
inst_11 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst_12 : Algebra Rₚ Sₚ
P : Ideal S
⊢ IsMaximal (maximalIdeal Rₚ)

Tactic:
exact maximalIdeal.isMaximal Rₚ

Premises used: IsLocalRing.maximalIdeal.isMaximal
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
Sₚ : Type u_5
inst_4 : CommSemiring Sₚ
inst_5 : Algebra S Sₚ
inst_6 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
P : Ideal S
inst_7 : P.IsMaximal
inst_8 : P.LiesOver p
⊢ under.{u_2, u_5} S (B := Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) = P

Tactic:
comap_map_eq_self_of_isMaximal _ (isPrime_map_of_liesOver S p Sₚ P).ne_top

Premises used: Ideal.comap_map_eq_self_of_isMaximal, Ideal.IsPrime.ne_top, IsLocalization.AtPrime.isPrime_map_of_liesOver
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
p : Ideal R
inst_1 : p.IsPrime
Rₚ : Type u_4
inst_2 : CommSemiring Rₚ
inst_3 : Algebra R Rₚ
inst_4 : IsLocalization.AtPrime Rₚ p
inst_5 : IsLocalRing Rₚ
inst_6 : p.IsMaximal
n : ℕ
h : ∀ (x : R), Membership.mem (γ := Ideal R) (under R (HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n)) x ↔ x ∈ p ^ n
⊢ under R (HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n) = p ^ n

Tactic:
ext