mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: case neg
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
M : Matrix n n R
inst✝ : Nontrivial R
hn : Fintype.card n = 2
this : Nonempty n
i : ℕ
hi : i ∉ range 3
⊢ M.charpoly.coeff i = (X ^ 2 - C M.trace * X + C M.det).coeff i

Tactic:
Finset.mem_range,

Goal state after:
case neg
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
M : Matrix n n R
inst✝ : Nontrivial R
hn : Fintype.card n = 2
this : Nonempty n
i : ℕ
hi : ¬i < 3
⊢ M.charpoly.coeff i = (X ^ 2 - C M.trace * X + C M.det).coeff i
Module: Mathlib.Algebra.Polynomial.HasseDeriv

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k l i : ℕ
⊢ (monomial (i - (k + l))) ↑((i - l).choose k * i.choose l) =
    (monomial (i - (k + l))) (↑((k + l).choose k) * ↑(i.choose (k + l)))

Tactic:
← Nat.cast_mul

Goal state after:
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
⊢ (monomial (i - (k + l))) ↑((i - l).choose k * i.choose l) =
    (monomial (i - (k + l))) ↑((k + l).choose k * i.choose (k + l))
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : f.Splits
hf0 : ¬f.leadingCoeff = 0
m : Multiset R
hm : f = C f.leadingCoeff * (Multiset.map (fun x ↦ X - C x) m).prod
⊢ f.roots = m

Tactic:
rw [hm, roots_C_mul _ hf0, roots_multiset_prod_X_sub_C]

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsIntegralClosure A R B
h : IsIntegral R 1
⊢ (algebraMap A B) (mk' A 1 h) = (algebraMap A B) 1

Tactic:
algebraMap_mk',

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsIntegralClosure A R B
h : IsIntegral R 1
⊢ 1 = (algebraMap A B) 1
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsIntegralClosure A R B
h : IsIntegral R 0
⊢ (algebraMap A B) (mk' A 0 h) = (algebraMap A B) 0

Tactic:
algebraMap_mk',

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsIntegralClosure A R B
h : IsIntegral R 0
⊢ 0 = (algebraMap A B) 0
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsIntegralClosure A R B
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A B
x : R
h : IsIntegral R ((algebraMap R B) x)
⊢ (algebraMap A B) (mk' A ((algebraMap R B) x) h) = (algebraMap A B) ((algebraMap R A) x)

Tactic:
algebraMap_mk',

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsIntegralClosure A R B
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A B
x : R
h : IsIntegral R ((algebraMap R B) x)
⊢ (algebraMap R B) x = (algebraMap A B) ((algebraMap R A) x)
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: case neg.a
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
Rₘ : Type u_3
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
p : Rₘ[X]
hp : p.leadingCoeff ∈ (algebraMap R Rₘ).range
n : ℕ
h₁ : n ∈ p.support
h₂ : ¬n = p.natDegree
this : n + 1 ≤ p.natDegree
⊢ (algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff) * p.coeff n ∈ (algebraMap R Rₘ).range

Tactic:
rw [← Algebra.smul_def]

Goal state after:
case neg.a
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
Rₘ : Type u_3
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
p : Rₘ[X]
hp : p.leadingCoeff ∈ (algebraMap R Rₘ).range
n : ℕ
h₁ : n ∈ p.support
h₂ : ¬n = p.natDegree
this : n + 1 ≤ p.natDegree
⊢ ↑(commonDenom M p.support p.coeff) • p.coeff n ∈ (algebraMap R Rₘ).range
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
fl : FaithfullyFlat R M
N : Type u_1
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Nontrivial N
n : N
hn : n ≠ 0
I : Ideal R := (R ∙ n).annihilator
I_ne_top : ¬I = ⊤
inc : R ⧸ I →ₗ[R] N := Submodule.liftQ I ((LinearMap.lsmul R N).flip n) ⋯
⊢ inc.ker ≤ ⊥

Tactic:
intro r hr

Goal state after:
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
fl : FaithfullyFlat R M
N : Type u_1
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Nontrivial N
n : N
hn : n ≠ 0
I : Ideal R := (R ∙ n).annihilator
I_ne_top : ¬I = ⊤
inc : R ⧸ I →ₗ[R] N := Submodule.liftQ I ((LinearMap.lsmul R N).flip n) ⋯
r : R ⧸ I
hr : r ∈ inc.ker
⊢ r ∈ ⊥
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
⊢ ∃ i, p.coeff i ∈ ↑(comap f J) \ ↑(comap f I)

Tactic:
have rbar_root :
    (p.map (Ideal.Quotient.mk (I.comap f))).eval₂ (Quotient.lift (I.comap f) _ quotient_f)
        (Ideal.Quotient.mk I r) =
      0 := by
    convert! Quotient.eq_zero_iff_mem.mpr hpI
    exact _root_.trans (eval₂_map _ _ _) (hom_eval₂ p f (Ideal.Quotient.mk I) r).symm

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, p.coeff i ∈ ↑(comap f J) \ ↑(comap f I)
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
t s : S
hst : s * t = 1
a✝ : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
p : (↥R[s])[X]
hpm : p.Monic
hpt : eval₂ (algebraMap (↥R[s]) S) t p = 0
this : Polynomial.map (algebraMap (↥R[s]) S) p ∈ lifts φ.toRingHom
q : R[X][X]
hqp : Polynomial.map φ.toRingHom q = Polynomial.map (algebraMap (↥R[s]) S) p
hqd : q.degree = (Polynomial.map (algebraMap (↥R[s]) S) p).degree
hqm : q.Monic
⊢ eval₂ φ.toRingHom t q = 0

Tactic:
rw [← eval_map, hqp, eval_map, hpt]

Goal state after:
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 ⋯
⊢ (aeval a) p = 0

Tactic:
← eval_map_algebraMap,

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 ⋯
⊢ eval a (map (algebraMap (↥(integralClosure R S)) A) p) = 0
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: A : Type u_3
inst✝⁹ : CommRing A
L : Type u_5
inst✝⁸ : Field L
inst✝⁷ : Algebra A L
C : Type u_6
inst✝⁶ : CommRing C
inst✝⁵ : IsDomain C
inst✝⁴ : Algebra C L
inst✝³ : IsIntegralClosure C A L
inst✝² : Algebra A C
inst✝¹ : IsScalarTower A C L
inst✝ : Algebra.IsAlgebraic A L
inj : ∀ (x : A), (algebraMap A L) x = 0 → x = 0
z : L
x : A
hx : x ≠ 0
int : IsIntegral A (x • z)
⊢ z * (algebraMap C L) ↑(mk' C (x • z) int, ⟨(algebraMap A C) x, ⋯⟩).2 =
    (algebraMap C L) (mk' C (x • z) int, ⟨(algebraMap A C) x, ⋯⟩).1

Tactic:
algebraMap_mk',

Goal state after:
A : Type u_3
inst✝⁹ : CommRing A
L : Type u_5
inst✝⁸ : Field L
inst✝⁷ : Algebra A L
C : Type u_6
inst✝⁶ : CommRing C
inst✝⁵ : IsDomain C
inst✝⁴ : Algebra C L
inst✝³ : IsIntegralClosure C A L
inst✝² : Algebra A C
inst✝¹ : IsScalarTower A C L
inst✝ : Algebra.IsAlgebraic A L
inj : ∀ (x : A), (algebraMap A L) x = 0 → x = 0
z : L
x : A
hx : x ≠ 0
int : IsIntegral A (x • z)
⊢ z * (algebraMap C L) ↑(mk' C (x • z) int, ⟨(algebraMap A C) x, ⋯⟩).2 = x • z
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
y z : S
hy : y ∈ nonZeroDivisors S
alg_y : IsAlgebraic R y
alg_yz : IsAlgebraic R (y * z)
t : S
ht : t ∈ R[y]
r : R
hr : r ≠ 0
eq : y * t = (algebraMap R S) r
⊢ IsAlgebraic R z

Tactic:
have := alg_yz.mul (Algebra.isAlgebraic_adjoin_singleton_iff.mpr alg_y _ ht)

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : NoZeroDivisors R
y z : S
hy : y ∈ nonZeroDivisors S
alg_y : IsAlgebraic R y
alg_yz : IsAlgebraic R (y * z)
t : S
ht : t ∈ R[y]
r : R
hr : r ≠ 0
eq : y * t = (algebraMap R S) r
this : IsAlgebraic R (y * z * t)
⊢ IsAlgebraic R z
Module: Mathlib.RingTheory.LocalRing.ResidueField.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : IsLocalRing R
inst✝³ : CommRing S
inst✝² : IsLocalRing S
inst✝¹ : CommRing T
inst✝ : IsLocalRing T
f : R ≃+* S
x : ResidueField S
⊢ (map ↑f) ((map ↑f.symm) x) = x

Tactic:
by simp only [map_map, RingEquiv.comp_symm, map_id, RingHom.id_apply]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : FaithfullyFlat R A
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : IsNoetherian A (A ⊗[R] M)
⊢ IsNoetherian R M

Tactic:
isNoetherian_iff'

Goal state after:
R : Type u_1
M : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : FaithfullyFlat R A
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : WellFoundedGT (Submodule A (A ⊗[R] M))
⊢ WellFoundedGT (Submodule R M)
Module: Mathlib.RingTheory.Spectrum.Prime.RingHom

Goal state before:
pp: ι : Type u_3
R : ι → Type u_2
inst✝ : (i : ι) → CommSemiring (R i)
x✝¹ x✝ : (i : ι) × PrimeSpectrum (R i)
i : ι
p : PrimeSpectrum (R i)
j : ι
q : PrimeSpectrum (R j)
eq : sigmaToPi R ⟨i, p⟩ = sigmaToPi R ⟨j, q⟩
⊢ ⟨i, p⟩ = ⟨j, q⟩

Tactic:
obtain rfl | ne := eq_or_ne i j

Goal state after:
case inl
ι : Type u_3
R : ι → Type u_2
inst✝ : (i : ι) → CommSemiring (R i)
x✝¹ x✝ : (i : ι) × PrimeSpectrum (R i)
i : ι
p q : PrimeSpectrum (R i)
eq : sigmaToPi R ⟨i, p⟩ = sigmaToPi R ⟨i, q⟩
⊢ ⟨i, p⟩ = ⟨i, q⟩

case inr
ι : Type u_3
R : ι → Type u_2
inst✝ : (i : ι) → CommSemiring (R i)
x✝¹ x✝ : (i : ι) × PrimeSpectrum (R i)
i : ι
p : PrimeSpectrum (R i)
j : ι
q : PrimeSpectrum (R j)
eq : sigmaToPi R ⟨i, p⟩ = sigmaToPi R ⟨j, q⟩
ne : i ≠ j
⊢ ⟨i, p⟩ = ⟨j, q⟩
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

Tactic:
rwa [Ring.krullDimLE_one_iff_of_isPrime_bot]

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

Goal state before:
pp: case e'_2.e_a
A : Type u_1
K : Type u_2
inst✝⁶ : CommRing A
S : Submonoid A
hS : S ≤ A⁰
inst✝⁵ : Field K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
x : K
x✝² x✝¹ : A
x✝ : x✝¹ ∈ S
⊢ ((algebraMap A K) x✝¹)⁻¹ =
    ↑((IsUnit.liftRight ((IsLocalization.toLocalizationMap A⁰ K).toMonoidHom.domRestrict A⁰) ⋯) ⟨x✝¹, ⋯⟩)⁻¹

Tactic:
Units.val_inv_eq_inv_val

Goal state after:
case e'_2.e_a
A : Type u_1
K : Type u_2
inst✝⁶ : CommRing A
S : Submonoid A
hS : S ≤ A⁰
inst✝⁵ : Field K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
x : K
x✝² x✝¹ : A
x✝ : x✝¹ ∈ S
⊢ ((algebraMap A K) x✝¹)⁻¹ =
    (↑((IsUnit.liftRight ((IsLocalization.toLocalizationMap A⁰ K).toMonoidHom.domRestrict A⁰) ⋯) ⟨x✝¹, ⋯⟩))⁻¹
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a : { a // IsIdempotentElem a }
⊢ (↑a, 1 - ↑a).1 * (↑a, 1 - ↑a).2 = 0

Tactic:
simp_rw [mul_sub, mul_one, a.2.eq, sub_self]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I J : Ideal S
h : J ∈ I.minimalPrimes
this✝ : J.IsPrime
K : Ideal R
hK : K.IsPrime
e₁ : comap f I ≤ K
e₂ : K ≤ comap f J
this : RingHom.ker f ≤ K
⊢ comap f J ≤ comap f (map f K)

Tactic:
apply Ideal.comap_mono _

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I J : Ideal S
h : J ∈ I.minimalPrimes
this✝ : J.IsPrime
K : Ideal R
hK : K.IsPrime
e₁ : comap f I ≤ K
e₂ : K ≤ comap f J
this : RingHom.ker f ≤ K
⊢ J ≤ map f K
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
⊢ comap f '' (map f I).minimalPrimes = comap f '' map f '' (I ⊔ RingHom.ker f).minimalPrimes

Tactic:
rw [← Ideal.comap_minimalPrimes_eq_of_surjective hf, ← Set.image_comp,
    Ideal.comap_map_of_surjective f hf, Set.image_congr, Set.image_id, 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
⊢ ∀ a ∈ (I ⊔ RingHom.ker f).minimalPrimes, (comap f ∘ map f) a = id a
Module: Mathlib.Topology.Sets.OpenCover

Goal state before:
pp: ι : Type u_1
X : Type u_3
inst✝ : TopologicalSpace X
S : Set (Opens X)
hS : IsBasis S
U : ι → Opens X
hU : IsOpenCover U
⊢ IsOpenCover fun V ↦ (↑V).1

Tactic:
refine top_le_iff.mp fun x _ ↦ ?_

Goal state after:
ι : Type u_1
X : Type u_3
inst✝ : TopologicalSpace X
S : Set (Opens X)
hS : IsBasis S
U : ι → Opens X
hU : IsOpenCover U
x : X
x✝ : x ∈ ⊤
⊢ x ∈ ⨆ V, (↑V).1
Module: Mathlib.Topology.Sets.Opens

Goal state before:
pp: case of_equiv
α : Type u_2
inst✝¹ : TopologicalSpace α
ι : Type u_5
inst✝ : Finite ι
α✝ β✝ : Type u_5
e : α✝ ≃ β✝
ih : ∀ (U : α✝ → Opens α), ↑(⨅ i, U i) = ⋂ i, ↑(U i)
U : β✝ → Opens α
⊢ ↑(⨅ x, U (e x)) = ⋂ i, ↑(U i)

Tactic:
← e.surjective.iInter_comp,

Goal state after:
case of_equiv
α : Type u_2
inst✝¹ : TopologicalSpace α
ι : Type u_5
inst✝ : Finite ι
α✝ β✝ : Type u_5
e : α✝ ≃ β✝
ih : ∀ (U : α✝ → Opens α), ↑(⨅ i, U i) = ⋂ i, ↑(U i)
U : β✝ → Opens α
⊢ ↑(⨅ x, U (e x)) = ⋂ x, ↑(U (e x))
Module: Mathlib.Topology.LocallyClosed

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ s ⊆ coborder s

Tactic:
by
  rw [coborder, subset_compl_iff_disjoint_right]
  exact disjoint_sdiff_self_right

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

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
U : Opens α
⊢ ¬(↑U).Nonempty ↔ ↑U = ↑⊥

Tactic:
coe_bot,

Goal state after:
α : Type u_2
inst✝ : TopologicalSpace α
U : Opens α
⊢ ¬(↑U).Nonempty ↔ ↑U = ∅
Module: Mathlib.Topology.Sets.Opens

Goal state before:
pp: case mpr.refine_2
α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
h : ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U' ∈ B, x ∈ U' ∧ U' ≤ U
x : α
sU : Set α
hx : x ∈ sU
hsU : IsOpen[inst✝] sU
⊢ ∃ v ∈ SetLike.coe '' B, x ∈ v ∧ v ⊆ sU

Tactic:
rcases @h ⟨sU, hsU⟩ x hx with ⟨V, hV, H⟩

Goal state after:
case mpr.refine_2
α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
h : ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U' ∈ B, x ∈ U' ∧ U' ≤ U
x : α
sU : Set α
hx : x ∈ sU
hsU : IsOpen[inst✝] sU
V : Opens α
hV : V ∈ B
H : x ∈ V ∧ V ≤ { carrier := sU, is_open' := hsU }
⊢ ∃ v ∈ SetLike.coe '' B, x ∈ v ∧ v ⊆ sU
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
H : IsProperMap f
s : Set β
y : ↑s
⊢ IsCompact (Subtype.val '' s.restrictPreimage f ⁻¹' {y})

Tactic:
image_val_preimage_restrictPreimage,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
H : IsProperMap f
s : Set β
y : ↑s
⊢ IsCompact (f ⁻¹' Subtype.val '' {y})
Module: Mathlib.Topology.LocallyClosed

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
tfae_1_to_2 : IsLocallyClosed s → IsOpen[inst✝] (coborder s)
tfae_2_to_3 : IsOpen[inst✝] (coborder s) → ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)
h : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)
x : X
hx : x ∈ s
t : Set X
ht : t ∈ 𝓝 x
ht' : IsClosed[instTopologicalSpaceSubtype] (t ↓∩ s)
U : Set X
hUt : U ⊆ t
hU : IsOpen[inst✝] U
hxU : x ∈ U
⊢ ∃ U, x ∈ U ∧ IsOpen[inst✝] U ∧ U ∩ closure[inst✝] s ⊆ s

Tactic:
rw [isClosed_preimage_val] at ht'

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
tfae_1_to_2 : IsLocallyClosed s → IsOpen[inst✝] (coborder s)
tfae_2_to_3 : IsOpen[inst✝] (coborder s) → ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)
h : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)
x : X
hx : x ∈ s
t : Set X
ht : t ∈ 𝓝 x
ht' : t ∩ closure[inst✝] (t ∩ s) ⊆ s
U : Set X
hUt : U ⊆ t
hU : IsOpen[inst✝] U
hxU : x ∈ U
⊢ ∃ U, x ∈ U ∧ IsOpen[inst✝] U ∧ U ∩ closure[inst✝] s ⊆ s
Module: Mathlib.Topology.Sets.Opens

Goal state before:
pp: α : Type u_5
t₁ t₂ : TopologicalSpace α
Us : Set (Opens α)
hUs : IsBasis Us
⊢ t₁ ≤ generateFrom (SetLike.coe '' Us) ↔ ∀ U ∈ Us, IsOpen[t₁] ↑U

Tactic:
simp [Set.subset_def, le_generateFrom_iff_subset_isOpen]

Goal state after:
Module: Mathlib.Topology.NoetherianSpace

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
⊢ NoetherianSpace ↑s ↔ ∀ t ⊆ s, IsCompact t

Tactic:
simp only [noetherianSpace_iff_isCompact, IsEmbedding.subtypeVal.isCompact_iff,
    Subtype.forall_set_subtype]

Goal state after:
Module: Mathlib.Topology.Spectral.Prespectral

Goal state before:
pp: case refine_1
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PrespectralSpace X
f : X → Y
hfc : Continuous[inst✝², inst✝¹] f
h : IsOpenMap f
U : Set Y
hs : U ⊆ Set.range f
hU : IsOpen[inst✝¹] U
hc : IsCompact U
Us : Set (Opens X)
hUs : Us ⊆ {U | IsCompact ↑U}
heq : { carrier := f ⁻¹' U, is_open' := ⋯ } = sSup Us
t : Finset ↑Us
ht : U ⊆ ⋃ i ∈ t, f '' ↑↑i
⊢ IsCompact (⨆ s ∈ t, ↑s).carrier

Tactic:
simp only [iSup_mk, carrier_eq_coe, coe_mk]
    exact t.finite_toSet.isCompact_biUnion fun i _ ↦ hUs i.2

Goal state after:
Module: Mathlib.Order.Ideal

Goal state before:
pp: case empty
P : Type u_1
inst✝ : CompleteLattice P
I : Ideal P
α : Type u_2
f : α → P
s : Set α
⊢ ⨆ i ∈ ∅, f i ∈ I ↔ ∀ i ∈ ∅, f i ∈ I

Tactic:
simp [↓iSup_insert, sup_mem_iff, *]

Goal state after:
Module: Mathlib.Order.Ideal

Goal state before:
pp: case insert
P : Type u_1
inst✝ : CompleteLattice P
I : Ideal P
α : Type u_2
f : α → P
s : Set α
a✝² : α
s✝ : Set α
a✝¹ : a✝² ∉ s✝
hs✝ : s✝.Finite
a✝ : ⨆ i ∈ s✝, f i ∈ I ↔ ∀ i ∈ s✝, f i ∈ I
⊢ ⨆ i ∈ insert a✝² s✝, f i ∈ I ↔ ∀ i ∈ insert a✝² s✝, f i ∈ I

Tactic:
simp [↓iSup_insert, sup_mem_iff, *]

Goal state after:
Module: Mathlib.Topology.Sober

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
x : α
S : Set α
h : IsGenericPoint x S
f : α → β
hf : Continuous f
⊢ IsGenericPoint (f x) (closure (f '' S))

Tactic:
by
  rw [isGenericPoint_def, ← h.def, ← image_singleton, closure_image_closure hf]

Goal state after:
Module: Mathlib.RingTheory.Ideal.GoingDown

Goal state before:
pp: case refine_1
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
H :
  ∀ (P : Ideal S) [inst : P.IsPrime],
    Function.Surjective (PrimeSpectrum.comap (Localization.localRingHom (Ideal.under R P) P (algebraMap R S) ⋯))
p : Ideal R
x✝¹ : p.IsPrime
Q : Ideal S
x✝ : Q.IsPrime
hlt : p < Ideal.under R Q
pl : Ideal (Localization.AtPrime (Ideal.under R Q)) :=
  Ideal.map (algebraMap R (Localization.AtPrime (Ideal.under R Q))) p
this : pl.IsPrime
Pl : Ideal (Localization.AtPrime Q)
isPrime✝ : Pl.IsPrime
hl :
  PrimeSpectrum.comap (Localization.localRingHom (Ideal.under R Q) Q (algebraMap R S) ⋯)
      { asIdeal := Pl, isPrime := isPrime✝ } =
    { asIdeal := pl, isPrime := ⋯ }
⊢ Ideal.under S Pl ≤ Q

pp: case refine_2
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
H :
  ∀ (P : Ideal S) [inst : P.IsPrime],
    Function.Surjective (PrimeSpectrum.comap (Localization.localRingHom (Ideal.under R P) P (algebraMap R S) ⋯))
p : Ideal R
x✝¹ : p.IsPrime
Q : Ideal S
x✝ : Q.IsPrime
hlt : p < Ideal.under R Q
pl : Ideal (Localization.AtPrime (Ideal.under R Q)) :=
  Ideal.map (algebraMap R (Localization.AtPrime (Ideal.under R Q))) p
this : pl.IsPrime
Pl : Ideal (Localization.AtPrime Q)
isPrime✝ : Pl.IsPrime
hl :
  PrimeSpectrum.comap (Localization.localRingHom (Ideal.under R Q) Q (algebraMap R S) ⋯)
      { asIdeal := Pl, isPrime := isPrime✝ } =
    { asIdeal := pl, isPrime := ⋯ }
⊢ p = Ideal.under R (Ideal.under S Pl)

Tactic:
· exact (IsLocalization.AtPrime.orderIsoOfPrime _ Q ⟨Pl, inferInstance⟩).2.2

Goal state after:
case refine_2
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
H :
  ∀ (P : Ideal S) [inst : P.IsPrime],
    Function.Surjective (PrimeSpectrum.comap (Localization.localRingHom (Ideal.under R P) P (algebraMap R S) ⋯))
p : Ideal R
x✝¹ : p.IsPrime
Q : Ideal S
x✝ : Q.IsPrime
hlt : p < Ideal.under R Q
pl : Ideal (Localization.AtPrime (Ideal.under R Q)) :=
  Ideal.map (algebraMap R (Localization.AtPrime (Ideal.under R Q))) p
this : pl.IsPrime
Pl : Ideal (Localization.AtPrime Q)
isPrime✝ : Pl.IsPrime
hl :
  PrimeSpectrum.comap (Localization.localRingHom (Ideal.under R Q) Q (algebraMap R S) ⋯)
      { asIdeal := Pl, isPrime := isPrime✝ } =
    { asIdeal := pl, isPrime := ⋯ }
⊢ p = Ideal.under R (Ideal.under S Pl)
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I : Ideal R
hle : I ≤ nilradical R
⊢ Bijective (comap (Ideal.Quotient.mk I))

Tactic:
by
  refine ⟨comap_injective_of_surjective _ Ideal.Quotient.mk_surjective, ?_⟩
  simpa [← Set.range_eq_univ, range_comap_of_surjective _ _ Ideal.Quotient.mk_surjective,
    zeroLocus_eq_univ_iff]

Goal state after: