mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
y : R
hy : ¬IsNilpotent y
h✝ : IsIntegral R (y • z)
p : R[X]
monic : p.Monic
eval0 : eval₂ (algebraMap R A) (y • z) p = 0
h : 1 * (C y * X).leadingCoeff ^ p.natDegree = 0
hy0 : y ≠ 0
⊢ False

pp: R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
y : R
hy : ¬IsNilpotent y
h✝ : IsIntegral R (y • z)
p : R[X]
monic : p.Monic
eval0 : eval₂ (algebraMap R A) (y • z) p = 0
h : (p.comp (C y * X)).coeff (p.natDegree * (C y * X).natDegree) = 0
hy0 : y ≠ 0
⊢ (C y * X).natDegree ≠ 0

Tactic:
one_mul,

Goal state after:
R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
y : R
hy : ¬IsNilpotent y
h✝ : IsIntegral R (y • z)
p : R[X]
monic : p.Monic
eval0 : eval₂ (algebraMap R A) (y • z) p = 0
h : (C y * X).leadingCoeff ^ p.natDegree = 0
hy0 : y ≠ 0
⊢ False

R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
y : R
hy : ¬IsNilpotent y
h✝ : IsIntegral R (y • z)
p : R[X]
monic : p.Monic
eval0 : eval₂ (algebraMap R A) (y • z) p = 0
h : (p.comp (C y * X)).coeff (p.natDegree * (C y * X).natDegree) = 0
hy0 : y ≠ 0
⊢ (C y * X).natDegree ≠ 0
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: case pos.inr
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Ring A
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : NoZeroDivisors S
int : Algebra.IsIntegral R S
a : A
h : IsAlgebraic S a
hRS : Function.Injective ⇑(algebraMap R S)
this : NoZeroDivisors R
s : S
hs : s ≠ 0
int_s : IsIntegral S (s • a)
h✝ : Nontrivial R
r : R
hr : r ≠ 0
w✝ : S
e : (algebraMap R S) r = s * w✝
⊢ IsIntegral R ((s * w✝) • a)

Tactic:
mul_comm,

Goal state after:
case pos.inr
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Ring A
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : NoZeroDivisors S
int : Algebra.IsIntegral R S
a : A
h : IsAlgebraic S a
hRS : Function.Injective ⇑(algebraMap R S)
this : NoZeroDivisors R
s : S
hs : s ≠ 0
int_s : IsIntegral S (s • a)
h✝ : Nontrivial R
r : R
hr : r ≠ 0
w✝ : S
e : (algebraMap R S) r = s * w✝
⊢ IsIntegral R ((w✝ * s) • a)
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: case mpr
R : Type u
inst✝ : CommSemiring R
⊢ zeroLocus ↑⊤ = ∅

Tactic:
apply zeroLocus_empty_of_one_mem

Goal state after:
case mpr
R : Type u
inst✝ : CommSemiring R
⊢ 1 ∈ ↑⊤
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
t t' : Set (PrimeSpectrum R)
r : R
⊢ (∃ y ∈ vanishingIdeal t, ∃ z ∈ vanishingIdeal t', y + z = r) → r ∈ vanishingIdeal (t ∩ t')

Tactic:
mem_vanishingIdeal

Goal state after:
R : Type u
inst✝ : CommSemiring R
t t' : Set (PrimeSpectrum R)
r : R
⊢ (∃ y ∈ vanishingIdeal t, ∃ z ∈ vanishingIdeal t', y + z = r) → ∀ x ∈ t ∩ t', r ∈ x.asIdeal
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
t t' : Set (PrimeSpectrum R)
f : R
hf : f ∈ vanishingIdeal t
g : R
hg : g ∈ vanishingIdeal t'
x : PrimeSpectrum R
hxt : x ∈ t
hxt' : x ∈ t'
⊢ f + g ∈ x.asIdeal

Tactic:
mem_vanishingIdeal

Goal state after:
R : Type u
inst✝ : CommSemiring R
t t' : Set (PrimeSpectrum R)
f : R
hf : ∀ x ∈ t, f ∈ x.asIdeal
g : R
hg : ∀ x ∈ t', g ∈ x.asIdeal
x : PrimeSpectrum R
hxt : x ∈ t
hxt' : x ∈ t'
⊢ f + g ∈ x.asIdeal
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set R
⊢ zeroLocus (s \ {0}) = zeroLocus s

Tactic:
← zeroLocus_insert_zero,

Goal state after:
R : Type u
inst✝ : CommSemiring R
s : Set R
⊢ zeroLocus (insert 0 (s \ {0})) = zeroLocus s
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : NoZeroDivisors R
a b : S
ha : IsAlgebraic R a
hb : IsAlgebraic R b
ra : R
a0 : ra ≠ 0
int_a : IsIntegral R (ra • a)
rb : R
b0 : rb ≠ 0
int_b : IsIntegral R (rb • b)
⊢ IsIntegral R (rb • ra • a + (rb * ra) • b)

Tactic:
mul_comm,

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : NoZeroDivisors R
a b : S
ha : IsAlgebraic R a
hb : IsAlgebraic R b
ra : R
a0 : ra ≠ 0
int_a : IsIntegral R (ra • a)
rb : R
b0 : rb ≠ 0
int_b : IsIntegral R (rb • b)
⊢ IsIntegral R (rb • ra • a + (ra * rb) • b)
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: case mp
R : Type u_1
inst✝⁹ : CommRing R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
K : Type u_4
inst✝⁶ : Field K
inst✝⁵ : IsDomain R
inst✝⁴ : Algebra R K
inst✝³ : Algebra S K
inst✝² : Module.IsTorsionFree R K
inst✝¹ : IsFractionRing S K
inst✝ : IsScalarTower R S K
h : ∀ (x : S), IsAlgebraic R x
this✝¹ : Nontrivial S := MulActionWithZero.nontrivial S K
this✝ : Algebra (FractionRing R) K := FractionRing.liftAlgebra R K
this : IsScalarTower R (FractionRing R) K
a b : S
ha : b ∈ nonZeroDivisors S
f : R[X]
hf₁ : f ≠ 0
hf₂ : (aeval b) f = 0
⊢ IsIntegral (FractionRing R) ((algebraMap S K) a * ((algebraMap S K) b)⁻¹)

Tactic:
refine .mul ?_ (.inv ?_) <;> exact isAlgebraic_iff_isIntegral.mp <|
      (h _).algebraMap.extendScalars (FaithfulSMul.algebraMap_injective R _)

Goal state after:
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: R : Type u_1
inst✝¹⁴ : CommRing R
S : Type u_2
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
K : Type u_4
L : Type u_5
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra R K
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : Algebra.IsAlgebraic R S
inst✝³ : IsFractionRing S L
inst✝² : Algebra K L
inst✝¹ : IsScalarTower R S L
inst✝ : IsScalarTower R K L
a : S
b : Set S
inj : Function.Injective ⇑(algebraMap R L)
h : ↑(Ideal.span {a}) ⊆ ↑(Submodule.span R b)
y' : S
z' : ↥S⁰
hx : (algebraMap S L) a * mk' L y' z' ∈ ↑(Ideal.span {(algebraMap S L) a})
y : S
z : R
hz0 : z ≠ 0
yz_eq : z • y' = ↑z' * y
injRS : Function.Injective ⇑(algebraMap R S)
hz0' : (algebraMap R S) z ∈ S⁰
mk_yz_eq : mk' L y' z' = mk' L y ⟨(algebraMap R S) z, hz0'⟩
hy : (algebraMap S L) (a * y) ∈ Submodule.span K (⇑(algebraMap S L) '' b)
⊢ (algebraMap S L) a * (algebraMap S L) y * ((algebraMap K L) ((algebraMap R K) z))⁻¹ ∈
    ↑(Submodule.span K (⇑(algebraMap S L) '' b))

Tactic:
mul_comm,

Goal state after:
R : Type u_1
inst✝¹⁴ : CommRing R
S : Type u_2
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
K : Type u_4
L : Type u_5
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra R K
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : Algebra.IsAlgebraic R S
inst✝³ : IsFractionRing S L
inst✝² : Algebra K L
inst✝¹ : IsScalarTower R S L
inst✝ : IsScalarTower R K L
a : S
b : Set S
inj : Function.Injective ⇑(algebraMap R L)
h : ↑(Ideal.span {a}) ⊆ ↑(Submodule.span R b)
y' : S
z' : ↥S⁰
hx : (algebraMap S L) a * mk' L y' z' ∈ ↑(Ideal.span {(algebraMap S L) a})
y : S
z : R
hz0 : z ≠ 0
yz_eq : z • y' = ↑z' * y
injRS : Function.Injective ⇑(algebraMap R S)
hz0' : (algebraMap R S) z ∈ S⁰
mk_yz_eq : mk' L y' z' = mk' L y ⟨(algebraMap R S) z, hz0'⟩
hy : (algebraMap S L) (a * y) ∈ Submodule.span K (⇑(algebraMap S L) '' b)
⊢ ((algebraMap K L) ((algebraMap R K) z))⁻¹ * ((algebraMap S L) a * (algebraMap S L) y) ∈
    ↑(Submodule.span K (⇑(algebraMap S L) '' b))
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: case mp
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
P : Ideal S
inst✝ : P.IsPrime
H : Function.Surjective ⇑(Localization.localRingHom (Ideal.comap f P) P f ⋯)
y : S
a : R
t : ↥(Ideal.comap f P).primeCompl
ha : (algebraMap S (Localization.AtPrime P)) (1 * f a) = (algebraMap S (Localization.AtPrime P)) (↑⟨f ↑t, ⋯⟩ * y)
⊢ ∃ x r, ∃ c ∉ P, f r ∉ P ∧ c * f r * y = c * f x

Tactic:
one_mul,

Goal state after:
case mp
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
P : Ideal S
inst✝ : P.IsPrime
H : Function.Surjective ⇑(Localization.localRingHom (Ideal.comap f P) P f ⋯)
y : S
a : R
t : ↥(Ideal.comap f P).primeCompl
ha : (algebraMap S (Localization.AtPrime P)) (f a) = (algebraMap S (Localization.AtPrime P)) (↑⟨f ↑t, ⋯⟩ * y)
⊢ ∃ x r, ∃ c ∉ P, f r ∉ P ∧ c * f r * y = c * f x
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: case tmul
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Algebra R S
hf₂ : (algebraMap R T).SurjectiveOnStalks
J : Ideal T
hJ : J.IsPrime
x₁ : S
x₂ : T
y s : R
c : T
hs : c ∉ J
hc : (algebraMap R T) s ∉ J
e : c * (algebraMap R T) s * x₂ = c * (algebraMap R T) y
⊢ (1 * x₁) ⊗ₜ[R] ((algebraMap R T) s * c * x₂) = (y • x₁) ⊗ₜ[R] c

Tactic:
one_mul,

Goal state after:
case tmul
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Algebra R S
hf₂ : (algebraMap R T).SurjectiveOnStalks
J : Ideal T
hJ : J.IsPrime
x₁ : S
x₂ : T
y s : R
c : T
hs : c ∉ J
hc : (algebraMap R T) s ∉ J
e : c * (algebraMap R T) s * x₂ = c * (algebraMap R T) y
⊢ x₁ ⊗ₜ[R] ((algebraMap R T) s * c * x₂) = (y • x₁) ⊗ₜ[R] c
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: case add
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Algebra R S
hf₂ : (algebraMap R T).SurjectiveOnStalks
J : Ideal T
hJ : J.IsPrime
x₁ x₂ : S ⊗[R] T
t₁ : T
r₁ : R
a₁ : S
hr₁ : r₁ • t₁ ∉ J
e₁ : 1 ⊗ₜ[R] (r₁ • t₁) * x₁ = a₁ ⊗ₜ[R] t₁
t₂ : T
r₂ : R
a₂ : S
hr₂ : r₂ • t₂ ∉ J
e₂ : 1 ⊗ₜ[R] (r₂ • t₂) * x₂ = a₂ ⊗ₜ[R] t₂
this : (r₁ * r₂) • (t₁ * t₂) = r₁ • t₁ * r₂ • t₂
⊢ (1 * a₁) ⊗ₜ[R] (r₂ • t₂ * t₁) + 1 ⊗ₜ[R] (r₂ • t₂) * 1 ⊗ₜ[R] (r₁ • t₁) * x₂ = (r₂ • a₁ + r₁ • a₂) ⊗ₜ[R] (t₁ * t₂)

Tactic:
one_mul,

Goal state after:
case add
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Algebra R S
hf₂ : (algebraMap R T).SurjectiveOnStalks
J : Ideal T
hJ : J.IsPrime
x₁ x₂ : S ⊗[R] T
t₁ : T
r₁ : R
a₁ : S
hr₁ : r₁ • t₁ ∉ J
e₁ : 1 ⊗ₜ[R] (r₁ • t₁) * x₁ = a₁ ⊗ₜ[R] t₁
t₂ : T
r₂ : R
a₂ : S
hr₂ : r₂ • t₂ ∉ J
e₂ : 1 ⊗ₜ[R] (r₂ • t₂) * x₂ = a₂ ⊗ₜ[R] t₂
this : (r₁ * r₂) • (t₁ * t₂) = r₁ • t₁ * r₂ • t₂
⊢ a₁ ⊗ₜ[R] (r₂ • t₂ * t₁) + 1 ⊗ₜ[R] (r₂ • t₂) * 1 ⊗ₜ[R] (r₁ • t₁) * x₂ = (r₂ • a₁ + r₁ • a₂) ⊗ₜ[R] (t₁ * t₂)
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: case add
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Algebra R S
hf₂ : (algebraMap R T).SurjectiveOnStalks
J : Ideal T
hJ : J.IsPrime
x₁ x₂ : S ⊗[R] T
t₁ : T
r₁ : R
a₁ : S
hr₁ : r₁ • t₁ ∉ J
e₁ : 1 ⊗ₜ[R] (r₁ • t₁) * x₁ = a₁ ⊗ₜ[R] t₁
t₂ : T
r₂ : R
a₂ : S
hr₂ : r₂ • t₂ ∉ J
e₂ : 1 ⊗ₜ[R] (r₂ • t₂) * x₂ = a₂ ⊗ₜ[R] t₂
this : (r₁ * r₂) • (t₁ * t₂) = r₁ • t₁ * r₂ • t₂
⊢ (r₂ • a₁) ⊗ₜ[R] (t₂ * t₁) + (1 * a₂) ⊗ₜ[R] (r₁ • t₁ * t₂) = (r₂ • a₁ + r₁ • a₂) ⊗ₜ[R] (t₁ * t₂)

Tactic:
one_mul,

Goal state after:
case add
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Algebra R S
hf₂ : (algebraMap R T).SurjectiveOnStalks
J : Ideal T
hJ : J.IsPrime
x₁ x₂ : S ⊗[R] T
t₁ : T
r₁ : R
a₁ : S
hr₁ : r₁ • t₁ ∉ J
e₁ : 1 ⊗ₜ[R] (r₁ • t₁) * x₁ = a₁ ⊗ₜ[R] t₁
t₂ : T
r₂ : R
a₂ : S
hr₂ : r₂ • t₂ ∉ J
e₂ : 1 ⊗ₜ[R] (r₂ • t₂) * x₂ = a₂ ⊗ₜ[R] t₂
this : (r₁ * r₂) • (t₁ * t₂) = r₁ • t₁ * r₂ • t₂
⊢ (r₂ • a₁) ⊗ₜ[R] (t₂ * t₁) + a₂ ⊗ₜ[R] (r₁ • t₁ * t₂) = (r₂ • a₁ + r₁ • a₂) ⊗ₜ[R] (t₁ * t₂)
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommSemiring R
a b : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
eq : (↑a).1 = (↑b).1
⊢ 0 = (↑b).2 * (↑a).1

Tactic:
mul_comm,

Goal state after:
case refine_1
R : Type u_1
inst✝ : CommSemiring R
a b : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
eq : (↑a).1 = (↑b).1
⊢ 0 = (↑a).1 * (↑b).2
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommSemiring R
a b : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
eq : (↑a).2 = (↑b).2
⊢ (↑a).2 * (↑a).1 = (↑b).1 * (↑a).2

Tactic:
mul_comm,

Goal state after:
case refine_1
R : Type u_1
inst✝ : CommSemiring R
a b : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
eq : (↑a).2 = (↑b).2
⊢ (↑a).1 * (↑a).2 = (↑b).1 * (↑a).2
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a✝ b✝ a b : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
hab : (↑a).1 * (↑b).1 = (↑a).1
hba : (↑b).1 * (↑a).1 = (↑b).1
⊢ (↑a).1 * (↑b).1 = (↑b).1

Tactic:
mul_comm,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a✝ b✝ a b : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
hab : (↑a).1 * (↑b).1 = (↑a).1
hba : (↑b).1 * (↑a).1 = (↑b).1
⊢ (↑b).1 * (↑a).1 = (↑b).1
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : CommSemigroup S
a b : { a // IsIdempotentElem a }
hab : ↑a * ↑b = ↑a
hba : ↑b * ↑a = ↑b
⊢ ↑a * ↑b = ↑b

Tactic:
mul_comm,

Goal state after:
R : Type u_1
S : Type u_2
inst✝ : CommSemigroup S
a b : { a // IsIdempotentElem a }
hab : ↑a * ↑b = ↑a
hba : ↑b * ↑a = ↑b
⊢ ↑b * ↑a = ↑b
Module: Mathlib.RingTheory.KrullDimension.Basic

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommSemiring R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal
hR : ⊥.IsPrime
⊢ KrullDimLE 1 R

pp: case neg
R : Type u_1
inst✝ : CommSemiring R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal
hR : ¬⊥.IsPrime
⊢ KrullDimLE 1 R

Tactic:
· rwa [Ring.krullDimLE_one_iff_of_isPrime_bot]

Goal state after:
case neg
R : Type u_1
inst✝ : CommSemiring R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal
hR : ¬⊥.IsPrime
⊢ KrullDimLE 1 R
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ I.minimalPrimes = (comap (Quotient.mk I) ⊥).minimalPrimes

Tactic:
← RingHom.ker_eq_comap_bot,

Goal state after:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ I.minimalPrimes = (RingHom.ker (Quotient.mk I)).minimalPrimes
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: ι : Type u_5
R : ι → Type u_4
inst✝² : (i : ι) → CommSemiring (R i)
inst✝¹ : ∀ (i : ι), Nontrivial (R i)
inst✝ : Infinite ι
surj : Function.Surjective ⇑(toPiLocalization ((i : ι) → R i))
J : Ideal ((i : ι) → R i)
max : J.IsMaximal
notMem : { asIdeal := J, isPrime := ⋯ } ∉ Set.range (PrimeSpectrum.sigmaToPi R)
r : (i : ι) → R i
hr : (toPiLocalization ((i : ι) → R i)) r = Function.update 0 { asIdeal := J, isMaximal := max } 1
⊢ False

Tactic:
have : r = 0 := funext fun i ↦ toPiLocalization_injective _ <| funext fun I ↦ by
    replace hr := congr_fun hr ⟨_, I.2.comap_piEvalRingHom⟩
    dsimp only [toPiLocalization_apply_apply, Subtype.coe_mk] at hr
    simp_rw [toPiLocalization_apply_apply,
      ← Localization.AtPrime.mapPiEvalRingHom_algebraMap_apply, hr]
    rw [Function.update_of_ne]; · simp_rw [Pi.zero_apply, map_zero]
    exact fun h ↦ notMem ⟨⟨i, I.1, I.2.isPrime⟩, PrimeSpectrum.ext congr($h.1)⟩

Goal state after:
ι : Type u_5
R : ι → Type u_4
inst✝² : (i : ι) → CommSemiring (R i)
inst✝¹ : ∀ (i : ι), Nontrivial (R i)
inst✝ : Infinite ι
surj : Function.Surjective ⇑(toPiLocalization ((i : ι) → R i))
J : Ideal ((i : ι) → R i)
max : J.IsMaximal
notMem : { asIdeal := J, isPrime := ⋯ } ∉ Set.range (PrimeSpectrum.sigmaToPi R)
r : (i : ι) → R i
hr : (toPiLocalization ((i : ι) → R i)) r = Function.update 0 { asIdeal := J, isMaximal := max } 1
this : r = 0
⊢ False
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
surj : Function.Surjective ⇑(toPiLocalization R)
I : PrimeSpectrum R
J : Ideal R
max : J.IsMaximal
le : I.asIdeal ≤ J
r : R
hr : (toPiLocalization R) r = Function.update 0 { asIdeal := J, isPrime := ⋯ } 1
h : ¬I.asIdeal.IsMaximal
hJ : (algebraMap R (Localization { asIdeal := J, isPrime := ⋯ }.asIdeal.primeCompl)) r = 1
hI : (algebraMap R (Localization I.asIdeal.primeCompl)) r = Function.update 0 { asIdeal := J, isPrime := ⋯ } 1 I
⊢ False

Tactic:
← IsLocalization.lift_eq (M := J.primeCompl) (S := Localization J.primeCompl),

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
surj : Function.Surjective ⇑(toPiLocalization R)
I : PrimeSpectrum R
J : Ideal R
max : J.IsMaximal
le : I.asIdeal ≤ J
r : R
hr : (toPiLocalization R) r = Function.update 0 { asIdeal := J, isPrime := ⋯ } 1
h : ¬I.asIdeal.IsMaximal
hJ : (algebraMap R (Localization { asIdeal := J, isPrime := ⋯ }.asIdeal.primeCompl)) r = 1
hI✝ : (algebraMap R (Localization I.asIdeal.primeCompl)) r = Function.update 0 { asIdeal := J, isPrime := ⋯ } 1 I
hI :
  (IsLocalization.lift ?hg) ((algebraMap R (Localization J.primeCompl)) r) =
    Function.update 0 { asIdeal := J, isPrime := ⋯ } 1 I
⊢ False

case hg
R : Type u_1
inst✝ : CommSemiring R
surj : Function.Surjective ⇑(toPiLocalization R)
I : PrimeSpectrum R
J : Ideal R
max : J.IsMaximal
le : I.asIdeal ≤ J
r : R
hr : (toPiLocalization R) r = Function.update 0 { asIdeal := J, isPrime := ⋯ } 1
h : ¬I.asIdeal.IsMaximal
hJ : (algebraMap R (Localization { asIdeal := J, isPrime := ⋯ }.asIdeal.primeCompl)) r = 1
hI : (algebraMap R (Localization I.asIdeal.primeCompl)) r = Function.update 0 { asIdeal := J, isPrime := ⋯ } 1 I
⊢ ∀ (y : ↥J.primeCompl), IsUnit ((algebraMap R (Localization I.asIdeal.primeCompl)) ↑y)
Module: Mathlib.Topology.Sets.Opens

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
ι : Type u_5
b : ι → Opens α
hb : IsBasis (range b)
hb' : ∀ (i : ι), IsCompact ↑(b i)
U : Set α
⊢ IsCompact U ∧ IsOpen[inst✝] U ↔ ∃ s, s.Finite ∧ U = ⋃ i ∈ s, ↑(b i)

Tactic:
by
  apply isCompact_open_iff_eq_finite_iUnion_of_isTopologicalBasis fun i : ι => (b i).1
  · convert! (config := { transparency := .default }) hb
    ext
    simp
  · exact hb'

Goal state after:
Module: Mathlib.Topology.Sets.Closeds

Goal state before:
pp: α : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
s : Opens α
⊢ IsCoatom s ↔ ∃ x, s = {x}.compl

Tactic:
← s.compl_compl,

Goal state after:
α : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
s : Opens α
⊢ IsCoatom s.compl.compl ↔ ∃ x, s.compl.compl = {x}.compl
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: X : Type u_6
Y : Type u_7
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
h : Continuous[inst✝², inst✝¹] f
ι : Type u_4
U : ι → Opens Y
hU : range f ⊆ ↑(iSup U)
V : ι → Type u_5
inst✝ : (i : ι) → TopologicalSpace (V i)
iV : (i : ι) → V i → X
hiV : ∀ (i : ι), Continuous[inst✝ i, inst✝²] (iV i)
hV : ∀ (i : ι), f ⁻¹' ↑(U i) ⊆ range (iV i)
hV' : ∀ (i : ι), IsEmbedding (f ∘ iV i)
hU' : iSup U = ⊤
i : ι
f' : ↑(iV i ⁻¹' f ⁻¹' ↑(U i)) → X := Subtype.val ∘ (f ⁻¹' ↑(U i)).restrictPreimage (iV i)
this : IsEmbedding f'
⊢ range f' = f ⁻¹' ↑(U i)

Tactic:
simpa [f', Set.range_comp, Set.range_restrictPreimage] using hV i

Goal state after:
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
ι : Type u_3
b : ι → Set α
basis : IsTopologicalBasis (range b)
isCompact_inter : ∀ (i j : ι), IsCompact (b i ∩ b j)
U V : Set α
hUopen : IsOpen[inst✝] U
hUcomp : IsCompact U
hVopen : IsOpen[inst✝] V
hVcomp : IsCompact V
i : ι
⊢ IsCompact (b i)

Tactic:
by
      simpa using isCompact_inter i i

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: case refine_2
X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
hs : IsSpectralMap Subtype.val
t : Set X
htcomp : IsCompact t
htopen : IsOpen[inst✝] t
⊢ IsCompact (s ∩ t)

Tactic:
· simpa using (hs.isCompact_preimage_of_isOpen htopen htcomp).image continuous_subtype_val

Goal state after:
Module: Mathlib.Topology.Sober

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
x : α
S : Set α
hS : IsClosed S
hxS : x ∈ S
⊢ IsGenericPoint x S ↔ ∀ (Z : Set α), IsClosed Z → x ∈ Z → S ⊆ Z

Tactic:
have : closure {x} ⊆ S := closure_minimal (singleton_subset_iff.2 hxS) hS

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
x : α
S : Set α
hS : IsClosed S
hxS : x ∈ S
this : closure {x} ⊆ S
⊢ IsGenericPoint x S ↔ ∀ (Z : Set α), IsClosed Z → x ∈ Z → S ⊆ Z
Module: Mathlib.Topology.Constructible

Goal state before:
pp: case sdiff
X : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
P : (s : Set X) → IsConstructible s → Prop
inst✝¹ : QuasiSeparatedSpace X
ι : Type u_4
inst✝ : Nonempty ι
b : ι → Set X
basis : IsTopologicalBasis (range b)
isCompact_basis : ∀ (i : ι), IsCompact (b i)
sdiff : ∀ (i : ι) (s : Set ι) (hs : s.Finite), P (b i \ ⋃ j ∈ s, b j) ⋯
union : ∀ (s : Set X) (hs : IsConstructible s) (t : Set X) (ht : IsConstructible t), P s hs → P t ht → P (s ∪ t) ⋯
s✝ : Set X
this : ∀ (U : Set X), IsCompact U ∧ IsOpen[inst✝³] U ↔ ∃ s, s.Finite ∧ U = ⋃ i ∈ s, b i
s : Set ι
hs : s.Finite
hU : ⋃ i ∈ s, b i ∈ {U | IsOpen[inst✝³] U ∧ IsRetrocompact U}
t : Set ι
ht : t.Finite
hV : ⋃ i ∈ t, b i ∈ {U | IsOpen[inst✝³] U ∧ IsRetrocompact U}
⊢ P ((⋃ i ∈ s, b i) \ ⋃ i ∈ t, b i) ⋯

Tactic:
iUnion_sdiff

Goal state after:
case sdiff
X : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
P : (s : Set X) → IsConstructible s → Prop
inst✝¹ : QuasiSeparatedSpace X
ι : Type u_4
inst✝ : Nonempty ι
b : ι → Set X
basis : IsTopologicalBasis (range b)
isCompact_basis : ∀ (i : ι), IsCompact (b i)
sdiff : ∀ (i : ι) (s : Set ι) (hs : s.Finite), P (b i \ ⋃ j ∈ s, b j) ⋯
union : ∀ (s : Set X) (hs : IsConstructible s) (t : Set X) (ht : IsConstructible t), P s hs → P t ht → P (s ∪ t) ⋯
s✝ : Set X
this : ∀ (U : Set X), IsCompact U ∧ IsOpen[inst✝³] U ↔ ∃ s, s.Finite ∧ U = ⋃ i ∈ s, b i
s : Set ι
hs : s.Finite
hU : ⋃ i ∈ s, b i ∈ {U | IsOpen[inst✝³] U ∧ IsRetrocompact U}
t : Set ι
ht : t.Finite
hV : ⋃ i ∈ t, b i ∈ {U | IsOpen[inst✝³] U ∧ IsRetrocompact U}
⊢ P (⋃ i ∈ s, b i \ ⋃ i ∈ t, b i) ⋯
Module: Mathlib.RingTheory.RingHom.FaithfullyFlat

Goal state before:
pp: R S T : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
hf : f.FaithfullyFlat
hg : g.FaithfullyFlat
algInst✝² : Algebra R S := f.toAlgebra
algInst✝¹ : Algebra S T := g.toAlgebra
algInst✝ : Algebra R T := (g.comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower R S T := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R T))
algebraizeInst✝¹ : Module.FaithfullyFlat R S
algebraizeInst✝ : Module.FaithfullyFlat S T
⊢ (g.comp f).FaithfullyFlat

Tactic:
rw [← algebraMap_toAlgebra (g.comp f), faithfullyFlat_algebraMap_iff]

Goal state after:
R S T : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
hf : f.FaithfullyFlat
hg : g.FaithfullyFlat
algInst✝² : Algebra R S := f.toAlgebra
algInst✝¹ : Algebra S T := g.toAlgebra
algInst✝ : Algebra R T := (g.comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower R S T := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R T))
algebraizeInst✝¹ : Module.FaithfullyFlat R S
algebraizeInst✝ : Module.FaithfullyFlat S T
⊢ Module.FaithfullyFlat R T
Module: Mathlib.RingTheory.Derivation.ToSquareZero

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
inst✝¹ : Algebra A B
hI✝ : I ^ 2 = ⊥
inst✝ : IsScalarTower R A B
hI : I ^ 2 = ⊥
f : Derivation R A ↥I
x y : A
⊢ ↑(f (x * y)) + (algebraMap A B) (x * y) = (↑(f x) + (algebraMap A B) x) * (↑(f y) + (algebraMap A B) y)

Tactic:
have : (f x : B) * f y = 0 := by
        rw [← Ideal.mem_bot, ← hI, pow_two]
        convert! Ideal.mul_mem_mul (f x).2 (f y).2 using 1

Goal state after:
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
inst✝¹ : Algebra A B
hI✝ : I ^ 2 = ⊥
inst✝ : IsScalarTower R A B
hI : I ^ 2 = ⊥
f : Derivation R A ↥I
x y : A
this : ↑(f x) * ↑(f y) = 0
⊢ ↑(f (x * y)) + (algebraMap A B) (x * y) = (↑(f x) + (algebraMap A B) x) * (↑(f y) + (algebraMap A B) y)
Module: Mathlib.Data.ZMod.Aut

Goal state before:
pp: n : ℕ
f : AddAut (ZMod n)
x : ZMod n
⊢ f 1 * x = f x

Tactic:
mul_comm,

Goal state after:
n : ℕ
f : AddAut (ZMod n)
x : ZMod n
⊢ x * f 1 = f x