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

Goal state before:
pp: case refine_3
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)
a : S
ha : a ∈ integralClosure R S
b : S
hb : b ∈ integralClosure R S
e :
  (algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf)) ⟨a, ha⟩ =
    (algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf)) ⟨b, hb⟩
this✝ :
  (algebraMap (↥(integralClosure Rf Sf)) Sf) ((algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf)) ⟨a, ha⟩) =
    (algebraMap (↥(integralClosure Rf Sf)) Sf) ((algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf)) ⟨b, hb⟩)
this : (algebraMap S Sf) a = (algebraMap S Sf) b
m : R
hm : m ∈ ↑M
h : ↑⟨(algebraMap R S) m, ⋯⟩ * a = ↑⟨(algebraMap R S) m, ⋯⟩ * b
⊢ (algebraMap (↥(integralClosure R S)) S) (↑⟨(algebraMap R ↥(integralClosure R S)) m, ⋯⟩ * ⟨a, ha⟩) =
    (algebraMap (↥(integralClosure R S)) S) (↑⟨(algebraMap R ↥(integralClosure R S)) m, ⋯⟩ * ⟨b, hb⟩)

Tactic:
simpa only [← IsScalarTower.algebraMap_apply]

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)
⊢ ↑(Ideal.span {(algebraMap S L) a}) ⊆ ↑(Submodule.span K (⇑(algebraMap S L) '' b))

Tactic:
intro x hx

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)
x : L
hx : x ∈ ↑(Ideal.span {(algebraMap S L) a})
⊢ x ∈ ↑(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 : IsLocalization.mk' (Localization.AtPrime P) (f a) ⟨f ↑t, ⋯⟩ = IsLocalization.mk' (Localization.AtPrime P) y 1
⊢ ∃ x r, ∃ c ∉ P, f r ∉ P ∧ c * f r * y = c * f x

Tactic:
IsLocalization.mk'_eq_iff_eq,

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)) (↑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
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
I : Ideal S
hI : I.IsPrime
H : ∀ (I : Ideal S), I.IsMaximal → ∀ (s : S), ∃ x r, ∃ c ∉ I, f r ∉ I ∧ c * f r * s = c * f x
s : S
M : Ideal S
hM : M.IsMaximal
hIM : I ≤ M
⊢ ∃ x r, ∃ c ∉ I, f r ∉ I ∧ c * f r * s = c * f x

Tactic:
obtain ⟨x, r, c, hc, hr, e⟩ := H M hM s

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
I : Ideal S
hI : I.IsPrime
H : ∀ (I : Ideal S), I.IsMaximal → ∀ (s : S), ∃ x r, ∃ c ∉ I, f r ∉ I ∧ c * f r * s = c * f x
s : S
M : Ideal S
hM : M.IsMaximal
hIM : I ≤ M
x r : R
c : S
hc : c ∉ M
hr : f r ∉ M
e : c * f r * s = c * f x
⊢ ∃ x r, ∃ c ∉ I, f r ∉ I ∧ c * f r * s = c * f x
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Module.FaithfullyFlat A B
I : Ideal A
inj : Function.Injective ⇑(↑A (quotIdealMapEquivTensorQuot B I).symm.toLinearMap ∘ₗ (TensorProduct.mk A B (A ⧸ I)) 1)
⊢ comap (algebraMap A B) (map (algebraMap A B) I) ≤ I

Tactic:
intro x hx

Goal state after:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Module.FaithfullyFlat A B
I : Ideal A
inj : Function.Injective ⇑(↑A (quotIdealMapEquivTensorQuot B I).symm.toLinearMap ∘ₗ (TensorProduct.mk A B (A ⧸ I)) 1)
x : A
hx : x ∈ comap (algebraMap A B) (map (algebraMap A B) I)
⊢ x ∈ I
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a✝ b✝ a b c : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
hac : a ≤ c
hbc : b ≤ c
⊢ ⟨((↑a).1 + (↑a).2 * (↑b).1, (↑a).2 * (↑b).2), ⋯⟩ ≤ c

Tactic:
by simp_rw [(· ≤ ·), add_mul, mul_assoc]; rw [hac, hbc]

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

Goal state before:
pp: ι : Type u_3
R : ι → Type u_4
inst✝¹ : (i : ι) → CommRing (R i)
inst✝ : _root_.Finite ι
p : PrimeSpectrum ((i : ι) → R i)
val✝ : Fintype ι
e : ι → (i : ι) → R i := fun i ↦ Function.update 1 i 0
H : ∏ i, e i = 0
i : ι
hi : e i ∈ p.asIdeal
h₁ : Function.Surjective ⇑(Pi.evalRingHom R i) := RingHomSurjective.is_surjective
⊢ ker (Pi.evalRingHom R i) ≤ p.asIdeal

Tactic:
intro x hx

Goal state after:
ι : Type u_3
R : ι → Type u_4
inst✝¹ : (i : ι) → CommRing (R i)
inst✝ : _root_.Finite ι
p : PrimeSpectrum ((i : ι) → R i)
val✝ : Fintype ι
e : ι → (i : ι) → R i := fun i ↦ Function.update 1 i 0
H : ∏ i, e i = 0
i : ι
hi : e i ∈ p.asIdeal
h₁ : Function.Surjective ⇑(Pi.evalRingHom R i) := RingHomSurjective.is_surjective
x : (i : ι) → R i
hx : x ∈ ker (Pi.evalRingHom R i)
⊢ x ∈ p.asIdeal
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : { a // IsIdempotentElem a }
⊢ ↑a * ↑⟨↑a + ↑b - ↑a * ↑b, ⋯⟩ = ↑a

Tactic:
simp_rw [mul_sub, mul_add]

Goal state after:
R : Type u_1
inst✝ : CommRing R
a b : { a // IsIdempotentElem a }
⊢ ↑a * ↑a + ↑a * ↑b - ↑a * (↑a * ↑b) = ↑a
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : { a // IsIdempotentElem a }
⊢ ↑b * ↑⟨↑a + ↑b - ↑a * ↑b, ⋯⟩ = ↑b

Tactic:
simp_rw [mul_sub, mul_add]

Goal state after:
R : Type u_1
inst✝ : CommRing R
a b : { a // IsIdempotentElem a }
⊢ ↑b * ↑a + ↑b * ↑b - ↑b * (↑a * ↑b) = ↑b
Module: Mathlib.RingTheory.Localization.AsSubring

Goal state before:
pp: A : Type u_1
K : Type u_2
inst✝⁶ : CommRing A
S : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
hS : S ≤ A⁰
x : K
⊢ x ∈ (mapToFractionRing K S B hS).range → ∃ a s, ∃ (hs : s ∈ S), x = IsLocalization.mk' K a ⟨s, ⋯⟩

Tactic:
by
    rintro ⟨x, rfl⟩
    obtain ⟨a, s, rfl⟩ := IsLocalization.exists_mk'_eq S x
    use a, s, s.2
    apply IsLocalization.lift_mk'

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

Goal state before:
pp: A : Type u_1
K : Type u_2
inst✝⁶ : CommRing A
S : Submonoid A
hS✝ : S ≤ A⁰
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
hS : S ≤ A⁰
⊢ Function.Bijective ⇑(mapToFractionRing K S B hS).rangeRestrict

Tactic:
refine ⟨fun a b h => ?_, Set.rangeFactorization_surjective⟩
      refine (IsLocalization.lift_injective_iff _).2 (fun a b => ?_) (Subtype.ext_iff.1 h)
      exact ⟨fun h => congr_arg _ (IsLocalization.injective _ hS h),
        fun h => congr_arg _ (IsFractionRing.injective A K h)⟩

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

Goal state before:
pp: case mp
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal S
J : Ideal R
⊢ J ∈ (comap f I).minimalPrimes → J ∈ comap f '' I.minimalPrimes

pp: case mpr
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal S
J : Ideal R
⊢ J ∈ comap f '' I.minimalPrimes → J ∈ (comap f I).minimalPrimes

Tactic:
· intro H
    obtain ⟨p, h, rfl⟩ := Ideal.exists_minimalPrimes_comap_eq f J H
    exact ⟨p, h, rfl⟩

Goal state after:
case mpr
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal S
J : Ideal R
⊢ J ∈ comap f '' I.minimalPrimes → J ∈ (comap f I).minimalPrimes
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
⊢ ∀ a ∈ (I ⊔ RingHom.ker f).minimalPrimes, (comap f ∘ map f) a = id a

Tactic:
intro x hx

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 x : Ideal R
hx : x ∈ (I ⊔ RingHom.ker f).minimalPrimes
⊢ (comap f ∘ map f) x = id x
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
hI :
  (IsLocalization.lift ?hg) ((algebraMap R (Localization J.primeCompl)) r) =
    Function.update 0 { asIdeal := J, isPrime := ⋯ } 1 I
⊢ False

pp: 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)

Tactic:
hJ,

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) 1 = 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.LocalAtTarget

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
H : ∀ (i : ι), IsOpenMap ((U i).carrier.restrictPreimage f)
s : Set α
hs : IsOpen[inst✝¹] s
i : ι
e_1✝ : ↥(U i) = ↑(U i).carrier
x : β
hx : x ∈ U i
this : (∃ y ∈ s, f y = x) ↔ ∃ y ∈ s, f y ∈ U i ∧ f y = x
⊢ ⟨x, hx⟩ ∈ Subtype.val ⁻¹' f '' s ↔ ⟨x, hx⟩ ∈ (U i).carrier.restrictPreimage f '' Subtype.val ⁻¹' s

Tactic:
simpa [← Subtype.coe_inj]

Goal state after:
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
H : ∀ (i : ι), IsClosedMap ((U i).carrier.restrictPreimage f)
s : Set α
hs : IsClosed[inst✝¹] s
i : ι
e_1✝ : ↥(U i) = ↑(U i).carrier
x : β
hx : x ∈ U i
this : (∃ y ∈ s, f y = x) ↔ ∃ y ∈ s, f y ∈ U i ∧ f y = x
⊢ ⟨x, hx⟩ ∈ Subtype.val ⁻¹' f '' s ↔ ⟨x, hx⟩ ∈ (U i).carrier.restrictPreimage f '' (Subtype.val ⁻¹' sᶜ)ᶜ

Tactic:
simpa [← Subtype.coe_inj]

Goal state after:
Module: Mathlib.Order.BooleanSubalgebra

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
a : α
t₁ t₂ : Finset (↑s × ↑s)
⊢ ((t₁.sup fun x ↦ ↑x.1 \ ↑x.2) ⊔ t₂.sup fun x ↦ ↑x.1 \ ↑x.2) = (t₁ ∪ t₂).sup fun x ↦ ↑x.1 \ ↑x.2

Tactic:
Finset.sup_union

Goal state after:
α : Type u_2
inst✝ : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
a : α
t₁ t₂ : Finset (↑s × ↑s)
⊢ ((t₁.sup fun x ↦ ↑x.1 \ ↑x.2) ⊔ t₂.sup fun x ↦ ↑x.1 \ ↑x.2) =
    (t₁.sup fun x ↦ ↑x.1 \ ↑x.2) ⊔ t₂.sup fun x ↦ ↑x.1 \ ↑x.2
Module: Mathlib.Topology.Sets.Closeds

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : TopologicalSpace α
s : Finset ι
U : ι → Clopens α
⊢ ↑(s.sup U) = ⋃ i ∈ s, ↑(U i)

Tactic:
by
  classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert _ _ _ IH => simp [IH]

Goal state after:
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: case convert_1
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen[inst✝] U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen[inst✝] V
hV'' : IsCompact V
⊢ f ⁻¹' U ⊆ s

Tactic:
intro x hx

Goal state after:
case convert_1
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen[inst✝] U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen[inst✝] V
hV'' : IsCompact V
x : α
hx : x ∈ f ⁻¹' U
⊢ x ∈ s
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: case convert_3
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen[inst✝] U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen[inst✝] V
hV'' : IsCompact V
⊢ f ⁻¹' V ⊆ s

Tactic:
intro x hx

Goal state after:
case convert_3
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen[inst✝] U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen[inst✝] V
hV'' : IsCompact V
x : α
hx : x ∈ f ⁻¹' V
⊢ x ∈ s
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 Y
f : X → Y
hf : IsOpenEmbedding f
x : X
U : Set X
hx : x ∈ U
hU : IsOpen[inst✝²] U
V : Set Y
hoV : IsOpen[inst✝¹] V
hcV : IsCompact V
hfx : f x ∈ V
hVf : V ⊆ f '' U
⊢ IsCompact (f ⁻¹' V)

Tactic:
exact hf.toIsInducing.isCompact_preimage' hcV <| Set.SurjOn.subset_range hVf

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

Goal state before:
pp: case refine_3
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : PrespectralSpace X
K U : Set X
hK : IsCompact K
hU : IsOpen[inst✝¹] U
hKU : K ⊆ U
⊢ ∀ x ∈ K, ∃ t ∈ 𝓝[K] x, ∃ W, IsCompact W ∧ IsOpen[inst✝¹] W ∧ t ⊆ W ∧ W ⊆ U

Tactic:
intro x hx

Goal state after:
case refine_3
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : PrespectralSpace X
K U : Set X
hK : IsCompact K
hU : IsOpen[inst✝¹] U
hKU : K ⊆ U
x : X
hx : x ∈ K
⊢ ∃ t ∈ 𝓝[K] x, ∃ W, IsCompact W ∧ IsOpen[inst✝¹] W ∧ t ⊆ W ∧ W ⊆ U
Module: Mathlib.Topology.Constructible

Goal state before:
pp: case union
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s✝ : Set X
hfopen : IsOpenEmbedding f
hfcomp : IsRetrocompact (range f)
s : Set X
hs : IsConstructible s
t : Set X
ht : IsConstructible t
hs' : IsConstructible (f '' s)
ht' : IsConstructible (f '' t)
⊢ IsConstructible (f '' (s ∪ t))

Tactic:
rw [image_union]

Goal state after:
case union
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s✝ : Set X
hfopen : IsOpenEmbedding f
hfcomp : IsRetrocompact (range f)
s : Set X
hs : IsConstructible s
t : Set X
ht : IsConstructible t
hs' : IsConstructible (f '' s)
ht' : IsConstructible (f '' t)
⊢ IsConstructible (f '' s ∪ f '' t)
Module: Mathlib.Topology.Sober

Goal state before:
pp: case a
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : R1Space α
S✝ : Set α
h : IsIrreducible S✝
hs : IsClosed S✝
x : α
hx : x ∈ S✝
⊢ S✝ ⊆ closure {x}

Tactic:
exact isPreirreducible_iff_forall_mem_subset_closure_singleton.mp h.isPreirreducible x hx

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: case union
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s✝ : Set X
hf : IsClosedEmbedding f
hfcomp : IsRetrocompact (range f)ᶜ
s : Set X
hs : IsConstructible s
t : Set X
ht : IsConstructible t
hs' : IsConstructible (f '' s)
ht' : IsConstructible (f '' t)
⊢ IsConstructible (f '' (s ∪ t))

Tactic:
rw [image_union]

Goal state after:
case union
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s✝ : Set X
hf : IsClosedEmbedding f
hfcomp : IsRetrocompact (range f)ᶜ
s : Set X
hs : IsConstructible s
t : Set X
ht : IsConstructible t
hs' : IsConstructible (f '' s)
ht' : IsConstructible (f '' t)
⊢ IsConstructible (f '' s ∪ f '' 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
d : Derivation R A ↥I
x : A
⊢ (Ideal.Quotient.mk I) ↑(d x) + (algebraMap A (B ⧸ I)) x = (algebraMap A (B ⧸ I)) x

Tactic:
simp only [Ideal.Quotient.eq_zero_iff_mem.mpr (d x).prop, zero_add]

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

Goal state before:
pp: case refine_2
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p : PrimeSpectrum (R × S)
h : p ∈ zeroLocus ↑(RingHom.ker (RingHom.fst R S))
⊢ p ∈ Set.range (comap (RingHom.fst R S))

Tactic:
obtain ⟨p, hp, eq⟩ | ⟨p, hp, eq⟩ := p.1.ideal_prod_prime.mp p.2

Goal state after:
case refine_2.inl
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p✝ : PrimeSpectrum (R × S)
h : p✝ ∈ zeroLocus ↑(RingHom.ker (RingHom.fst R S))
p : Ideal R
hp : p.IsPrime
eq : p✝.asIdeal = p.prod ⊤
⊢ p✝ ∈ Set.range (comap (RingHom.fst R S))

case refine_2.inr
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p✝ : PrimeSpectrum (R × S)
h : p✝ ∈ zeroLocus ↑(RingHom.ker (RingHom.fst R S))
p : Ideal S
hp : p.IsPrime
eq : p✝.asIdeal = ⊤.prod p
⊢ p✝ ∈ Set.range (comap (RingHom.fst R S))
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case refine_2
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p : PrimeSpectrum (R × S)
h : p ∈ zeroLocus ↑(RingHom.ker (RingHom.snd R S))
⊢ p ∈ Set.range (comap (RingHom.snd R S))

Tactic:
obtain ⟨p, hp, eq⟩ | ⟨p, hp, eq⟩ := p.1.ideal_prod_prime.mp p.2

Goal state after:
case refine_2.inl
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p✝ : PrimeSpectrum (R × S)
h : p✝ ∈ zeroLocus ↑(RingHom.ker (RingHom.snd R S))
p : Ideal R
hp : p.IsPrime
eq : p✝.asIdeal = p.prod ⊤
⊢ p✝ ∈ Set.range (comap (RingHom.snd R S))

case refine_2.inr
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p✝ : PrimeSpectrum (R × S)
h : p✝ ∈ zeroLocus ↑(RingHom.ker (RingHom.snd R S))
p : Ideal S
hp : p.IsPrime
eq : p✝.asIdeal = ⊤.prod p
⊢ p✝ ∈ Set.range (comap (RingHom.snd R S))
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
inst✝¹ : (i : ι) → CommRing (R i)
inst✝ : DecidableEq ι
i : ι
f : R i
p : PrimeSpectrum ((i : ι) → R i)
hp : p ∈ ↑(basicOpen (Pi.single i f))
⊢ RingHom.ker (Pi.evalRingHom R i) ≤ p.asIdeal

Tactic:
intro x hx

Goal state after:
ι : Type u_1
R : ι → Type u_2
inst✝¹ : (i : ι) → CommRing (R i)
inst✝ : DecidableEq ι
i : ι
f : R i
p : PrimeSpectrum ((i : ι) → R i)
hp : p ∈ ↑(basicOpen (Pi.single i f))
x : (i : ι) → R i
hx : x ∈ RingHom.ker (Pi.evalRingHom R i)
⊢ x ∈ p.asIdeal
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : DiscreteTopology (PrimeSpectrum R)
x : PiLocalization R
f : PrimeSpectrum R → R
hf : ∀ (p : PrimeSpectrum R), ↑(basicOpen (f p)) = {p}
e : PrimeSpectrum R ≃ ↑(Set.range f) := Equiv.ofInjective f ⋯
loc : ∀ (a : ↑(Set.range f)), IsLocalization.AtPrime (Localization.Away ↑a) (e.symm a).asIdeal
algE : (a : ↑(Set.range f)) → Localization.AtPrime (e.symm a).asIdeal ≃ₐ[R] Localization.Away ↑a :=
  fun a ↦
    IsLocalization.algEquiv (e.symm a).asIdeal.primeCompl (Localization.AtPrime (e.symm a).asIdeal)
      (Localization.Away ↑a)
⊢ ∃ a, (toPiLocalization R) a = x

Tactic:
have span_eq : Ideal.span (Set.range f) = ⊤ := iSup_basicOpen_eq_top_iff.mp <| top_unique
    fun p _ ↦ TopologicalSpace.Opens.mem_iSup.mpr ⟨p, (hf p).ge rfl⟩

Goal state after:
R : Type u
inst✝¹ : CommSemiring R
inst✝ : DiscreteTopology (PrimeSpectrum R)
x : PiLocalization R
f : PrimeSpectrum R → R
hf : ∀ (p : PrimeSpectrum R), ↑(basicOpen (f p)) = {p}
e : PrimeSpectrum R ≃ ↑(Set.range f) := Equiv.ofInjective f ⋯
loc : ∀ (a : ↑(Set.range f)), IsLocalization.AtPrime (Localization.Away ↑a) (e.symm a).asIdeal
algE : (a : ↑(Set.range f)) → Localization.AtPrime (e.symm a).asIdeal ≃ₐ[R] Localization.Away ↑a :=
  fun a ↦
    IsLocalization.algEquiv (e.symm a).asIdeal.primeCompl (Localization.AtPrime (e.symm a).asIdeal)
      (Localization.Away ↑a)
span_eq : Ideal.span (Set.range f) = ⊤
⊢ ∃ a, (toPiLocalization R) a = x
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: case a
α : Type u_1
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
⊢ {a | a ^ n = 1} ⊆ (↑(zpowers (g ^ (Fintype.card α / n.gcd (Fintype.card α))))).toFinset

Tactic:
intro x hx

Goal state after:
case a
α : Type u_1
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
x : α
hx : x ∈ {a | a ^ n = 1}
⊢ x ∈ (↑(zpowers (g ^ (Fintype.card α / n.gcd (Fintype.card α))))).toFinset
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case inr
R : Type u
inst✝ : CommSemiring R
x : R
hx : x ∈ {e | IsIdempotentElem e}
y : R
hy : y ∈ {e | IsIdempotentElem e}
eq : basicOpen x = basicOpen y
ne : x ≠ y
this :
  ∀ x ∈ {e | IsIdempotentElem e}, ∀ y ∈ {e | IsIdempotentElem e}, basicOpen x = basicOpen y → x ≠ y → x * y ≠ x → False
ne' : ¬x * y ≠ x
⊢ y * x ≠ y

Tactic:
rwa [mul_comm, of_not_not ne']

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: α : Type u_1
inst✝² : Group α
inst✝¹ : Finite α
inst✝ : IsCyclic α
⊢ ∃ x, ∀ (y : α), y ∈ Submonoid.powers x

Tactic:
by
  simp_rw [mem_powers_iff_mem_zpowers]
  exact IsCyclic.exists_generator

Goal state after: