mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Field R
f : R[X]
hf : ∀ {g : R[X]}, Irreducible g → g ∣ f → g.degree = 1
hf0 : ¬f = 0
⊢ f.Splits

Tactic:
obtain ⟨u, hu⟩ := factors_prod hf0

Goal state after:
case neg
R : Type u_1
inst✝ : Field R
f : R[X]
hf : ∀ {g : R[X]}, Irreducible g → g ∣ f → g.degree = 1
hf0 : ¬f = 0
u : R[X]ˣ
hu : (factors f).prod * ↑u = f
⊢ f.Splits
Module: Mathlib.RingTheory.Ideal.GoingUp

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
I J : Ideal S
inst✝ : I.IsPrime
hIJ : I ≤ J
r : S
p : R[X]
p_ne_zero : Polynomial.map (Quotient.mk (comap f I)) p ≠ 0
hpI : eval₂ f r p ∈ I
hrJ : r ∈ ↑J
hrI : r ∉ ↑I
rbar_ne_zero : (Quotient.mk I) r ≠ 0
rbar_mem_J : (Quotient.mk I) r ∈ map (Quotient.mk I) J
quotient_f : ∀ x ∈ comap f I, ((Quotient.mk I).comp f) x = 0
rbar_root :
  eval₂ (Quotient.lift (comap f I) ((Quotient.mk I).comp f) quotient_f) ((Quotient.mk I) r)
      (Polynomial.map (Quotient.mk (comap f I)) p) =
    0
i : ℕ
ne_zero : (Polynomial.map (Quotient.mk (comap f I)) p).coeff i ≠ 0
mem :
  (Polynomial.map (Quotient.mk (comap f I)) p).coeff i ∈
    comap (Quotient.lift (comap f I) ((Quotient.mk I).comp f) quotient_f) (map (Quotient.mk I) J)
⊢ ∃ i, p.coeff i ∈ ↑(comap f J) \ ↑(comap f I)

Tactic:
rw [coeff_map] at ne_zero mem

Goal state after:
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
I J : Ideal S
inst✝ : I.IsPrime
hIJ : I ≤ J
r : S
p : R[X]
p_ne_zero : Polynomial.map (Quotient.mk (comap f I)) p ≠ 0
hpI : eval₂ f r p ∈ I
hrJ : r ∈ ↑J
hrI : r ∉ ↑I
rbar_ne_zero : (Quotient.mk I) r ≠ 0
rbar_mem_J : (Quotient.mk I) r ∈ map (Quotient.mk I) J
quotient_f : ∀ x ∈ comap f I, ((Quotient.mk I).comp f) x = 0
rbar_root :
  eval₂ (Quotient.lift (comap f I) ((Quotient.mk I).comp f) quotient_f) ((Quotient.mk I) r)
      (Polynomial.map (Quotient.mk (comap f I)) p) =
    0
i : ℕ
ne_zero : (Quotient.mk (comap f I)) (p.coeff i) ≠ 0
mem :
  (Quotient.mk (comap f I)) (p.coeff i) ∈
    comap (Quotient.lift (comap f I) ((Quotient.mk I).comp f) quotient_f) (map (Quotient.mk I) J)
⊢ ∃ i, p.coeff i ∈ ↑(comap f J) \ ↑(comap f I)
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N1 : Type u_1
inst✝⁵ : AddCommGroup N1
inst✝⁴ : Module R N1
N2 : Type u_2
inst✝³ : AddCommGroup N2
inst✝² : Module R N2
N3 : Type u_3
inst✝¹ : AddCommGroup N3
inst✝ : Module R N3
l12 : N1 →ₗ[R] N2
l23 : N2 →ₗ[R] N3
fl : FaithfullyFlat R M
ex : Function.Exact ⇑(LinearMap.rTensor M l12) ⇑(LinearMap.rTensor M l23)
n1 : N1
hn1 : l23 (l12 n1) ≠ 0
E : Submodule R N3 := R ∙ l23 (l12 n1)
hE : Nontrivial ↥E
eq1 : ∀ (m : M), l23 (l12 n1) ⊗ₜ[R] m = 0
c : ↥E ⊗[R] M →₀ R
b : ⦃a : ↥E ⊗[R] M⦄ → a ∈ ↑c.support → ↥E
a : ⦃a : ↥E ⊗[R] M⦄ → a ∈ ↑c.support → M
hy : ∀ ⦃a_1 : ↥E ⊗[R] M⦄ (a_2 : a_1 ∈ ↑c.support), b a_2 ⊗ₜ[R] a a_2 = a_1
r : ⦃a : ↥E ⊗[R] M⦄ → a ∈ c.support → R := fun a ha ↦ ⋯.choose
hr : ∀ ⦃i : ↥E ⊗[R] M⦄ (hi : i ∈ c.support), b hi = r hi • ⟨l23 (l12 n1), ⋯⟩
i : ↥E ⊗[R] M
hi : i ∈ c.support
⊢ (LinearMap.rTensor M E.subtype) (c ((r hi • ⟨l23 (l12 n1), ⋯⟩) ⊗ₜ[R] a hi) • (r hi • ⟨l23 (l12 n1), ⋯⟩) ⊗ₜ[R] a hi) =
    (LinearMap.rTensor M E.subtype) 0

Tactic:
smul_tmul,

Goal state after:
R : Type u
M : Type v
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N1 : Type u_1
inst✝⁵ : AddCommGroup N1
inst✝⁴ : Module R N1
N2 : Type u_2
inst✝³ : AddCommGroup N2
inst✝² : Module R N2
N3 : Type u_3
inst✝¹ : AddCommGroup N3
inst✝ : Module R N3
l12 : N1 →ₗ[R] N2
l23 : N2 →ₗ[R] N3
fl : FaithfullyFlat R M
ex : Function.Exact ⇑(LinearMap.rTensor M l12) ⇑(LinearMap.rTensor M l23)
n1 : N1
hn1 : l23 (l12 n1) ≠ 0
E : Submodule R N3 := R ∙ l23 (l12 n1)
hE : Nontrivial ↥E
eq1 : ∀ (m : M), l23 (l12 n1) ⊗ₜ[R] m = 0
c : ↥E ⊗[R] M →₀ R
b : ⦃a : ↥E ⊗[R] M⦄ → a ∈ ↑c.support → ↥E
a : ⦃a : ↥E ⊗[R] M⦄ → a ∈ ↑c.support → M
hy : ∀ ⦃a_1 : ↥E ⊗[R] M⦄ (a_2 : a_1 ∈ ↑c.support), b a_2 ⊗ₜ[R] a a_2 = a_1
r : ⦃a : ↥E ⊗[R] M⦄ → a ∈ c.support → R := fun a ha ↦ ⋯.choose
hr : ∀ ⦃i : ↥E ⊗[R] M⦄ (hi : i ∈ c.support), b hi = r hi • ⟨l23 (l12 n1), ⋯⟩
i : ↥E ⊗[R] M
hi : i ∈ c.support
⊢ (LinearMap.rTensor M E.subtype) (c (⟨l23 (l12 n1), ⋯⟩ ⊗ₜ[R] (r hi • a hi)) • ⟨l23 (l12 n1), ⋯⟩ ⊗ₜ[R] (r hi • a hi)) =
    (LinearMap.rTensor M E.subtype) 0
Module: Mathlib.RingTheory.Ideal.GoingUp

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal R
hf₁ : Function.Injective ⇑f
hf₂ : f.IsIntegral
⊢ RingHom.ker f ≤ I

Tactic:
simp [(RingHom.injective_iff_ker_eq_bot f).mp hf₁]

Goal state after:
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: case tmul
R : Type u
M : Type v
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N1 : Type u_1
inst✝⁵ : AddCommGroup N1
inst✝⁴ : Module R N1
N2 : Type u_2
inst✝³ : AddCommGroup N2
inst✝² : Module R N2
N3 : Type u_3
inst✝¹ : AddCommGroup N3
inst✝ : Module R N3
l12 : N1 →ₗ[R] N2
l23 : N2 →ₗ[R] N3
fl : FaithfullyFlat R M
ex : Function.Exact ⇑(LinearMap.rTensor M l12) ⇑(LinearMap.rTensor M l23)
complex : l12.range ≤ l23.ker
H : Type u_2 := ↥l23.ker ⧸ (Submodule.inclusion complex).range
e : H ⊗[R] M ≃ₗ[R]
  ↥l23.ker ⊗[R] M ⧸ (TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id).range :=
  quotientTensorEquiv M (Submodule.inclusion complex).range
m : M
x : N2
hx : l23 x = 0
⊢ ∃ a, (TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id) a = ⟨x, hx⟩ ⊗ₜ[R] m

Tactic:
have mem : x ⊗ₜ[R] m ∈ LinearMap.ker (l23.rTensor M) := by simp [hx]

Goal state after:
case tmul
R : Type u
M : Type v
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N1 : Type u_1
inst✝⁵ : AddCommGroup N1
inst✝⁴ : Module R N1
N2 : Type u_2
inst✝³ : AddCommGroup N2
inst✝² : Module R N2
N3 : Type u_3
inst✝¹ : AddCommGroup N3
inst✝ : Module R N3
l12 : N1 →ₗ[R] N2
l23 : N2 →ₗ[R] N3
fl : FaithfullyFlat R M
ex : Function.Exact ⇑(LinearMap.rTensor M l12) ⇑(LinearMap.rTensor M l23)
complex : l12.range ≤ l23.ker
H : Type u_2 := ↥l23.ker ⧸ (Submodule.inclusion complex).range
e : H ⊗[R] M ≃ₗ[R]
  ↥l23.ker ⊗[R] M ⧸ (TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id).range :=
  quotientTensorEquiv M (Submodule.inclusion complex).range
m : M
x : N2
hx : l23 x = 0
mem : x ⊗ₜ[R] m ∈ (LinearMap.rTensor M l23).ker
⊢ ∃ a, (TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id) a = ⟨x, hx⟩ ⊗ₜ[R] m
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: case refine_2
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
inst✝ : Algebra.IsAlgebraic R S
a : A
h : IsAlgebraic S a
p✝ : S[X]
hp : p✝ ≠ 0
eval0 : (aeval a) p✝ = 0
hRS : FaithfulSMul R S
this✝¹ : NoZeroDivisors R
this✝ : Nontrivial R
this : IsDomain R
r : R
hr : r ≠ 0
int : ∀ z ∈ Finset.image p✝.coeff p✝.support, IsIntegral R (r • z)
p : (↥(integralClosure R S).toSubring)[X] := (r • p✝).toSubring (integralClosure R S).toSubring ⋯
⊢ r • (AlgHom.restrictScalars R (aeval a)) p✝ = 0

Tactic:
AlgHom.restrictScalars_apply,

Goal state after:
case refine_2
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
inst✝ : Algebra.IsAlgebraic R S
a : A
h : IsAlgebraic S a
p✝ : S[X]
hp : p✝ ≠ 0
eval0 : (aeval a) p✝ = 0
hRS : FaithfulSMul R S
this✝¹ : NoZeroDivisors R
this✝ : Nontrivial R
this : IsDomain R
r : R
hr : r ≠ 0
int : ∀ z ∈ Finset.image p✝.coeff p✝.support, IsIntegral R (r • z)
p : (↥(integralClosure R S).toSubring)[X] := (r • p✝).toSubring (integralClosure R S).toSubring ⋯
⊢ r • (aeval a) p✝ = 0
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: case refine_2
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
inst✝ : Algebra.IsAlgebraic R S
a : A
h : IsAlgebraic S a
p✝ : S[X]
hp : p✝ ≠ 0
eval0 : (aeval a) p✝ = 0
hRS : FaithfulSMul R S
this✝¹ : NoZeroDivisors R
this✝ : Nontrivial R
this : IsDomain R
r : R
hr : r ≠ 0
int : ∀ z ∈ Finset.image p✝.coeff p✝.support, IsIntegral R (r • z)
p : (↥(integralClosure R S).toSubring)[X] := (r • p✝).toSubring (integralClosure R S).toSubring ⋯
⊢ r • 0 = 0

Tactic:
smul_zero

Goal state after:
case refine_2
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
inst✝ : Algebra.IsAlgebraic R S
a : A
h : IsAlgebraic S a
p✝ : S[X]
hp : p✝ ≠ 0
eval0 : (aeval a) p✝ = 0
hRS : FaithfulSMul R S
this✝¹ : NoZeroDivisors R
this✝ : Nontrivial R
this : IsDomain R
r : R
hr : r ≠ 0
int : ∀ z ∈ Finset.image p✝.coeff p✝.support, IsIntegral R (r • z)
p : (↥(integralClosure R S).toSubring)[X] := (r • p✝).toSubring (integralClosure R S).toSubring ⋯
⊢ 0 = 0
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: case refine_2
R : Type u_1
inst✝¹⁵ : CommRing R
S : Type u_2
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
Rf : Type u_5
Sf : Type u_6
inst✝¹² : CommRing Rf
inst✝¹¹ : CommRing Sf
inst✝¹⁰ : Algebra R Rf
inst✝⁹ : Algebra S Sf
inst✝⁸ : Algebra Rf Sf
inst✝⁷ : Algebra R Sf
inst✝⁶ : IsScalarTower R S Sf
inst✝⁵ : IsScalarTower R Rf Sf
M : Submonoid R
inst✝⁴ : IsLocalization M Rf
inst✝³ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sf
inst✝² : Algebra ↥(integralClosure R S) ↥(integralClosure Rf Sf)
inst✝¹ : IsScalarTower (↥(integralClosure R S)) (↥(integralClosure Rf Sf)) Sf
inst✝ : IsScalarTower R ↥(integralClosure R S) ↥(integralClosure Rf Sf)
s : Sf
hs : s ∈ integralClosure Rf Sf
x : S
m₁ : R
hm₁ : m₁ ∈ ↑M
e : s * (algebraMap R Sf) m₁ = (algebraMap S Sf) x
m₂ : R
hm₂ : m₂ ∈ M
hm₂s : IsIntegral R ((algebraMap R Sf) m₂ * s)
m₃ : R
hm₃ : m₃ ∈ M
hm₃s : IsIntegral R (m₃ • m₂ • x)
⊢ (algebraMap S Sf) x * (algebraMap R Sf) m₂ * (algebraMap R Sf) m₃ =
    (algebraMap R Sf) m₃ * (algebraMap R Sf) m₂ * (algebraMap S Sf) x

Tactic:
ring

Goal state after:
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: case e'_2
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
P : Ideal S
inst✝ : P.IsPrime
H : ∀ (s : S), ∃ x r, ∃ c ∉ P, f r ∉ P ∧ c * f r * s = c * f x
y✝ : Localization.AtPrime P
x✝ : S × ↥P.primeCompl
y t : S
h : t ∈ P.primeCompl
yx ys : R
yc : S
hyc : yc ∉ P
hy : f ys ∉ P
ey : yc * f ys * y = yc * f yx
tx ts : R
yt : S
hyt : yt ∉ P
ht : f ts ∉ P
et : yt * f ts * t = yt * f tx
⊢ yc * yt * (t * (f yx * f ts)) = yc * f yx * (yt * f ts * t)

Tactic:
ring

Goal state after:
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: case e'_3
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
P : Ideal S
inst✝ : P.IsPrime
H : ∀ (s : S), ∃ x r, ∃ c ∉ P, f r ∉ P ∧ c * f r * s = c * f x
y✝ : Localization.AtPrime P
x✝ : S × ↥P.primeCompl
y t : S
h : t ∈ P.primeCompl
yx ys : R
yc : S
hyc : yc ∉ P
hy : f ys ∉ P
ey : yc * f ys * y = yc * f yx
tx ts : R
yt : S
hyt : yt ∉ P
ht : f ts ∉ P
et : yt * f ts * t = yt * f tx
⊢ yc * yt * (f ys * f tx * y) = yc * f ys * y * (yt * f tx)

Tactic:
ring

Goal state after:
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommRing R
S : Type u_2
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
inst✝¹ : FaithfullyFlat R S
inst✝ : FaithfullyFlat S M
N : Type (max u_1 u_3)
x✝³ : AddCommGroup N
x✝² : Module R N
N' : Type (max u_1 u_3)
x✝¹ : AddCommGroup N'
x✝ : Module R N'
f : N →ₗ[R] N'
aux : lTensor M f = 0
⊢ f = 0

Tactic:
rw [zero_iff_lTensor_zero (R := R) (M := S) f,
    show f.lTensor S = (AlgebraTensorModule.map (A := S) LinearMap.id f).restrictScalars R by aesop,
    show (0 :  S ⊗[R] N →ₗ[R] S ⊗[R] N') = (0 : S ⊗[R] N →ₗ[S] S ⊗[R] N').restrictScalars R by rfl,
    restrictScalars_inj, zero_iff_lTensor_zero (R := S) (M := M)]

Goal state after:
R : Type u_1
inst✝⁸ : CommRing R
S : Type u_2
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
inst✝¹ : FaithfullyFlat R S
inst✝ : FaithfullyFlat S M
N : Type (max u_1 u_3)
x✝³ : AddCommGroup N
x✝² : Module R N
N' : Type (max u_1 u_3)
x✝¹ : AddCommGroup N'
x✝ : Module R N'
f : N →ₗ[R] N'
aux : lTensor M f = 0
⊢ lTensor M (AlgebraTensorModule.map LinearMap.id f) = 0
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : CommSemigroup S
a b c : { a // IsIdempotentElem a }
hab : ↑a * ↑b = ↑a
hac : ↑a * ↑c = ↑a
⊢ ↑a * ↑⟨↑b * ↑c, ⋯⟩ = ↑a

Tactic:
by simp_rw [← mul_assoc]; rw [hab, hac]

Goal state after:
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x : R
p : Ideal R
hxp : x ∈ p
hp₃ : ∀ ⦃y : Ideal R⦄, (fun q ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
hp₁ : p.IsPrime
hp₂ : I ≤ p
this : map (algebraMap R (Localization.AtPrime p)) p ≤ (map (algebraMap R (Localization.AtPrime p)) I).radical
n : ℕ
a : ↥I
b t : ↥p.primeCompl
ht : ↑t * (x ^ n * ↑b) = ↑t * ↑a
⊢ (x * (↑t * ↑b)) ^ (n + 1) = ↑t ^ n * ↑b ^ n * x * (↑t * (x ^ n * ↑b))

Tactic:
ring

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.RingHom

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
hf : Function.Surjective (comap f)
x : R
hfx : IsUnit (f x)
hx : ¬IsUnit x
p : Ideal R
hp : p.IsMaximal
right✝ : x ∈ p
q : Ideal S
hqp : q.IsPrime
hq : comap f { asIdeal := q, isPrime := hqp } = { asIdeal := p, isPrime := ⋯ }
⊢ False

Tactic:
simp only [PrimeSpectrum.ext_iff, comap_asIdeal] at hq

Goal state after:
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
hf : Function.Surjective (comap f)
x : R
hfx : IsUnit (f x)
hx : ¬IsUnit x
p : Ideal R
hp : p.IsMaximal
right✝ : x ∈ p
q : Ideal S
hqp : q.IsPrime
hq : Ideal.comap f q = p
⊢ False
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
S : Type u_3
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal R
⊢ (I ⊔ comap f ⊥).minimalPrimes = (I ⊔ RingHom.ker f).minimalPrimes

pp: R : Type u_1
inst✝¹ : CommRing R
S : Type u_3
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal R
⊢ ∀ a ∈ (I ⊔ RingHom.ker f).minimalPrimes, (comap f ∘ map f) a = id a

Tactic:
RingHom.ker

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
S : Type u_3
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal R
⊢ (I ⊔ comap f ⊥).minimalPrimes = (I ⊔ comap f ⊥).minimalPrimes

R : Type u_1
inst✝¹ : CommRing R
S : Type u_3
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal R
⊢ ∀ a ∈ (I ⊔ RingHom.ker f).minimalPrimes, (comap f ∘ map f) a = id a
Module: Mathlib.Topology.Compactness.Bases

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
b : Set (Set X)
hb : IsTopologicalBasis b
U : Set X
hUc : IsCompact U
hUo : IsOpen U
hb' : b = range fun i ↦ ↑i
⊢ ∃ s, U = ⋃₀ (Subtype.val '' ↑s)

Tactic:
rw [hb'] at hb

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
b : Set (Set X)
hb : IsTopologicalBasis (range fun i ↦ ↑i)
U : Set X
hUc : IsCompact U
hUo : IsOpen U
hb' : b = range fun i ↦ ↑i
⊢ ∃ s, U = ⋃₀ (Subtype.val '' ↑s)
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
r r' : R
eq : (toPiLocalization R) r = (toPiLocalization R) r'
⊢ r = r'

Tactic:
← one_mul r,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
r r' : R
eq : (toPiLocalization R) r = (toPiLocalization R) r'
⊢ 1 * r = r'
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
surj : Function.Surjective ⇑(toPiLocalization R)
⊢ Finite (MaximalSpectrum R)

Tactic:
replace surj := mapPiLocalization_bijective _ ⟨toPiLocalization_injective R, surj⟩
    |>.2.comp surj

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
surj✝ : Function.Surjective ⇑(toPiLocalization R)
surj : Function.Surjective (⇑(mapPiLocalization (toPiLocalization R).toRingHom ⋯) ∘ ⇑(toPiLocalization R))
⊢ Finite (MaximalSpectrum R)
Module: Mathlib.Order.BooleanSubalgebra

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : BooleanAlgebra α
inst✝¹ : BooleanAlgebra β
inst✝ : BooleanAlgebra γ
L✝ M : BooleanSubalgebra α
f : BoundedLatticeHom α β
s✝ t : Set α
a b : α
L : BooleanSubalgebra α
s : Set α
hs : s = ↑L
⊢ s = ↑L.toSublattice

Tactic:
subst hs

Goal state after:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : BooleanAlgebra α
inst✝¹ : BooleanAlgebra β
inst✝ : BooleanAlgebra γ
L✝ M : BooleanSubalgebra α
f : BoundedLatticeHom α β
s t : Set α
a b : α
L : BooleanSubalgebra α
⊢ ↑L = ↑L.toSublattice
Module: Mathlib.Order.BooleanSubalgebra

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : BooleanAlgebra α
inst✝¹ : BooleanAlgebra β
inst✝ : BooleanAlgebra γ
L✝ M : BooleanSubalgebra α
f : BoundedLatticeHom α β
s✝ t : Set α
a b : α
L : BooleanSubalgebra α
s : Set α
hs : s = ↑L
⊢ ∀ {a : α}, a ∈ (L.copy s ⋯).carrier → aᶜ ∈ (L.copy s ⋯).carrier

Tactic:
subst hs

Goal state after:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : BooleanAlgebra α
inst✝¹ : BooleanAlgebra β
inst✝ : BooleanAlgebra γ
L✝ M : BooleanSubalgebra α
f : BoundedLatticeHom α β
s t : Set α
a b : α
L : BooleanSubalgebra α
__Sublattice✝ : Sublattice α := L.copy ↑L ⋯
⊢ ∀ {a : α}, a ∈ (L.copy ↑L ⋯).carrier → aᶜ ∈ (L.copy ↑L ⋯).carrier
Module: Mathlib.Order.BooleanSubalgebra

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : BooleanAlgebra α
inst✝¹ : BooleanAlgebra β
inst✝ : BooleanAlgebra γ
L✝ M : BooleanSubalgebra α
f : BoundedLatticeHom α β
s✝ t : Set α
a b : α
L : BooleanSubalgebra α
s : Set α
hs : s = ↑L
⊢ ⊥ ∈ (L.copy s ⋯).carrier

Tactic:
subst hs

Goal state after:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : BooleanAlgebra α
inst✝¹ : BooleanAlgebra β
inst✝ : BooleanAlgebra γ
L✝ M : BooleanSubalgebra α
f : BoundedLatticeHom α β
s t : Set α
a b : α
L : BooleanSubalgebra α
__Sublattice✝ : Sublattice α := L.copy ↑L ⋯
⊢ ⊥ ∈ (L.copy ↑L ⋯).carrier
Module: Mathlib.Topology.Sets.Opens

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
ι : Type u_5
U : ι → Opens X
hU : IsBasis (range U)
W : Opens X
hW : IsCompact W.carrier
κ : Type u
a : κ → ι
heq : W = ⨆ k, U (a k)
s : Finset κ
hs : W.carrier ⊆ ⋃ i ∈ s, (U (a i)).carrier
⊢ ∃ κ, ∃ (_ : Finite κ), ∃ a, W = ⨆ k, U (a k)

Tactic:
use s, s.finite_toSet, a ∘ Subtype.val

Goal state after:
case h
X : Type u
inst✝ : TopologicalSpace X
ι : Type u_5
U : ι → Opens X
hU : IsBasis (range U)
W : Opens X
hW : IsCompact W.carrier
κ : Type u
a : κ → ι
heq : W = ⨆ k, U (a k)
s : Finset κ
hs : W.carrier ⊆ ⋃ i ∈ s, (U (a i)).carrier
⊢ W = ⨆ k, U ((a ∘ Subtype.val) k)
Module: Mathlib.Order.Ideal

Goal state before:
pp: P : Type u_1
inst✝¹ : LE P
inst✝ : OrderTop P
⊢ IsCoatomic (Ideal P)

Tactic:
apply IsCoatomic.of_isChain_bounded

Goal state after:
P : Type u_1
inst✝¹ : LE P
inst✝ : OrderTop P
⊢ ∀ (c : Set (Ideal P)), IsChain (fun x1 x2 ↦ x1 ≤ x2) c → c.Nonempty → ⊤ ∉ c → ∃ x, x ≠ ⊤ ∧ x ∈ upperBounds c
Module: Mathlib.Topology.Constructible

Goal state before:
pp: case mem
X : Type u_2
inst✝ : TopologicalSpace X
p : (s : Set X) → IsConstructible s → Prop
open_retrocompact : ∀ (U : Set X) (hUopen : IsOpen[inst✝] U) (hUcomp : IsRetrocompact U), p U ⋯
union : ∀ (s : Set X) (hs : IsConstructible s) (t : Set X) (ht : IsConstructible t), p s hs → p t ht → p (s ∪ t) ⋯
compl : ∀ (s : Set X) (hs : IsConstructible s), p s hs → p sᶜ ⋯
s U : Set X
hU : U ∈ {U | IsOpen[inst✝] U ∧ IsRetrocompact U}
⊢ p U ⋯

Tactic:
exact open_retrocompact _ hU.1 hU.2

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set Y
hf : IsOpenEmbedding f
hfcomp : IsRetrocompact (range f)
hsf : s ⊆ range f
hs : IsConstructible (f ⁻¹' s)
⊢ IsConstructible s

Tactic:
simpa [image_preimage_eq_range_inter, inter_eq_right.2 hsf]
    using hs.image_of_isOpenEmbedding hf hfcomp

Goal state after:
Module: Mathlib.RingTheory.Derivation.ToSquareZero

Goal state before:
pp: case refine_3
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
inst✝ : IsScalarTower R A B
hI : I ^ 2 = ⊥
f : A →ₐ[R] B
e : (Ideal.Quotient.mkₐ R I).comp f = IsScalarTower.toAlgHom R A (B ⧸ I)
x y : A
F : A →ₗ[R] ↥I := diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B) ⋯
this : f x * f y = 0 + (f x * (algebraMap A B) y - (algebraMap A B) x * (algebraMap A B) y) + (algebraMap A B) x * f y
⊢ 0 + (f x * (algebraMap A B) y - (algebraMap A B) x * (algebraMap A B) y) + (algebraMap A B) x * f y -
      (algebraMap A B) x * (algebraMap A B) y =
    (algebraMap A B) x * f y - (algebraMap A B) x * (algebraMap A B) y +
      ((algebraMap A B) y * f x - (algebraMap A B) y * (algebraMap A B) x)

Tactic:
ring

Goal state after:
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
this : ↑(f x) * ↑(f y) = 0
⊢ (algebraMap A B) x * ↑(f y) + (algebraMap A B) y * ↑(f x) + (algebraMap A B) x * (algebraMap A B) y =
    0 + (algebraMap A B) x * ↑(f y) + (↑(f x) * (algebraMap A B) y + (algebraMap A B) x * (algebraMap A B) y)

Tactic:
ring

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case mp
R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
H : zeroLocus ↑x.asIdeal ⊆ {x}
⊢ x.asIdeal.IsMaximal

Tactic:
rcases x.asIdeal.exists_le_maximal x.2.1 with ⟨m, hm, hxm⟩

Goal state after:
case mp
R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
H : zeroLocus ↑x.asIdeal ⊆ {x}
m : Ideal R
hm : m.IsMaximal
hxm : x.asIdeal ≤ m
⊢ x.asIdeal.IsMaximal
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring A
inst✝³ : AddCommMonoid M
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
r : R
⊢ r • 0 = 0

Tactic:
smul_zero

Goal state after:
R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring A
inst✝³ : AddCommMonoid M
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
r : R
⊢ 0 = 0
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring A
inst✝³ : AddCommMonoid M
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
n : ℕ
⊢ n • 0 = 0

Tactic:
smul_zero

Goal state after:
R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring A
inst✝³ : AddCommMonoid M
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
n : ℕ
⊢ 0 = 0