mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ map (algebraMap R (Localization.AtPrime p)) p ≤ (map (algebraMap R (Localization.AtPrime p)) I).radical

Tactic:
Ideal.radical_eq_sInf,

Goal state after:
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
⊢ map (algebraMap R (Localization.AtPrime p)) p ≤
    sInf {J | map (algebraMap R (Localization.AtPrime p)) I ≤ J ∧ J.IsPrime}
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
x : (i : ι) → R i
⊢ x ∈ ker (Pi.evalRingHom R i) → x ∈ p.asIdeal

Tactic:
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.RingTheory.Spectrum.Prime.RingHom

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
I : Ideal R
hI : ker f = I
p : Ideal R
isPrime✝ : p.IsPrime
hp : { asIdeal := p, isPrime := isPrime✝ } ∈ zeroLocus ↑I
⊢ (fun p ↦ ⟨PrimeSpectrum.comap f p, ⋯⟩)
      ((fun x ↦
          match x with
          | ⟨{ asIdeal := p, isPrime := isPrime }, hp⟩ => { asIdeal := map f p, isPrime := ⋯ })
        ⟨{ asIdeal := p, isPrime := isPrime✝ }, hp⟩) =
    ⟨{ asIdeal := p, isPrime := isPrime✝ }, hp⟩

Tactic:
simp only [Subtype.mk.injEq, PrimeSpectrum.ext_iff, comap_asIdeal]

Goal state after:
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
I : Ideal R
hI : ker f = I
p : Ideal R
isPrime✝ : p.IsPrime
hp : { asIdeal := p, isPrime := isPrime✝ } ∈ zeroLocus ↑I
⊢ comap f (map f p) = p
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 x : Ideal R
⊢ x ∈ (I ⊔ RingHom.ker f).minimalPrimes → (comap f ∘ map f) x = id x

Tactic:
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: ι : 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
i : ι
I : MaximalSpectrum (R i)
hr :
  (algebraMap ((i : ι) → R i) (Localization.AtPrime (Ideal.comap (Pi.evalRingHom R i) I.asIdeal))) r =
    Function.update 0 { asIdeal := J, isMaximal := max } 1
      { asIdeal := Ideal.comap (Pi.evalRingHom R i) I.asIdeal, isMaximal := ⋯ }
⊢ (Localization.AtPrime.mapPiEvalRingHom I.asIdeal) 0 =
    (Localization.AtPrime.mapPiEvalRingHom I.asIdeal)
      ((algebraMap ((i : ι) → R i) (Localization.AtPrime (Ideal.comap (Pi.evalRingHom R i) I.asIdeal))) 0)

Tactic:
map_zero

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: case h
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 : 1 = Function.update 0 { asIdeal := J, isPrime := ⋯ } 1 I
eq : I = { asIdeal := J, isPrime := ⋯ }
⊢ False

Tactic:
have : I.1 = J := congr_arg (·.1) eq

Goal state after:
case h
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 : 1 = Function.update 0 { asIdeal := J, isPrime := ⋯ } 1 I
eq : I = { asIdeal := J, isPrime := ⋯ }
this : I.asIdeal = J
⊢ False
Module: Mathlib.Topology.Sets.OpenCover

Goal state before:
pp: case inr
X : Type u_1
ι : Type u_2
inst✝ : TopologicalSpace X
U : ι → Opens X
hn : Pairwise ((fun x1 x2 ↦ ¬Disjoint x1 x2) on U)
h : ∀ (i : ι), IsPreirreducible ↑(U i)
s : Set X
hs : IsOpen[inst✝] s
hsU : s ⊆ ⋃ i, ↑(U i)
x : X
hx : x ∈ s
i : ι
hi : x ∈ ↑(U i)
⊢ IsPreirreducible s

Tactic:
rcases exists_mem_irreducibleComponents_subset_of_isIrreducible (U i).carrier ⟨⟨x, hi⟩, h i⟩
      with ⟨u, hu, hUu⟩

Goal state after:
case inr
X : Type u_1
ι : Type u_2
inst✝ : TopologicalSpace X
U : ι → Opens X
hn : Pairwise ((fun x1 x2 ↦ ¬Disjoint x1 x2) on U)
h : ∀ (i : ι), IsPreirreducible ↑(U i)
s : Set X
hs : IsOpen[inst✝] s
hsU : s ⊆ ⋃ i, ↑(U i)
x : X
hx : x ∈ s
i : ι
hi : x ∈ ↑(U i)
u : Set X
hu : u ∈ irreducibleComponents X
hUu : (U i).carrier ⊆ u
⊢ IsPreirreducible s
Module: Mathlib.Topology.Sets.Opens

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
Us : Set (Opens α)
x : α
⊢ x ∈ sSup Us ↔ ∃ u ∈ Us, x ∈ u

Tactic:
simp_rw [sSup_eq_iSup, mem_iSup, exists_prop]

Goal state after:
Module: Mathlib.Topology.LocallyClosed

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hs : IsLocallyClosed s
ht : IsLocallyClosed t
⊢ IsLocallyClosed (s ∩ t)

Tactic:
obtain ⟨U₁, Z₁, hU₁, hZ₁, rfl⟩ := hs

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
t : Set X
ht : IsLocallyClosed t
U₁ Z₁ : Set X
hU₁ : IsOpen[inst✝] U₁
hZ₁ : IsClosed[inst✝] Z₁
⊢ IsLocallyClosed (U₁ ∩ Z₁ ∩ t)
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 α
⊢ x ∈ sU → IsOpen[inst✝] sU → ∃ v ∈ SetLike.coe '' B, x ∈ v ∧ v ⊆ sU

Tactic:
hx

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
⊢ IsOpen[inst✝] sU → ∃ v ∈ SetLike.coe '' B, x ∈ v ∧ v ⊆ sU
Module: Mathlib.Topology.LocallyClosed

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
hf : IsInducing f
⊢ IsLocallyClosed s ↔ ∃ s', IsLocallyClosed s' ∧ f ⁻¹' s' = s

Tactic:
simp_rw [IsLocallyClosed, hf.isOpen_iff, hf.isClosed_iff]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
hf : IsInducing f
⊢ (∃ U Z, (∃ t, IsOpen[inst✝] t ∧ f ⁻¹' t = U) ∧ (∃ t, IsClosed[inst✝] t ∧ f ⁻¹' t = Z) ∧ s = U ∩ Z) ↔
    ∃ s', (∃ U Z, IsOpen[inst✝] U ∧ IsClosed[inst✝] Z ∧ s' = U ∩ Z) ∧ f ⁻¹' s' = s
Module: Mathlib.Topology.Sets.Opens

Goal state before:
pp: case mpr
α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
h : ∀ (U : Opens α), ∃ Us ⊆ B, U = sSup Us
U : Opens α
x : α
⊢ x ∈ U → ∃ U' ∈ B, x ∈ U' ∧ U' ≤ U

Tactic:
hx

Goal state after:
case mpr
α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
h : ∀ (U : Opens α), ∃ Us ⊆ B, U = sSup Us
U : Opens α
x : α
hx : x ∈ U
⊢ ∃ U' ∈ B, x ∈ U' ∧ U' ≤ U
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
⊢ closure[inst✝] (range f) = univ ↔ ∀ (i : ι), {x | x ∈ U i} ⊆ closure[inst✝] (range f)

Tactic:
rw [← iUnion_subset_iff, ← Set.univ_subset_iff, iff_iff_eq]

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
⊢ (univ ⊆ closure[inst✝] (range f)) = (⋃ i, {x | x ∈ U i} ⊆ closure[inst✝] (range f))
Module: Mathlib.Topology.NoetherianSpace

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
⊢ (∀ (k : Opens α), IsCompactElement k) ↔ ∀ (s : Opens α), IsCompact ↑s

Tactic:
exact forall_congr' Opens.isCompactElement_iff

Goal state after:
Module: Mathlib.Topology.NoetherianSpace

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
s : Closeds α
H : ∀ y < s, ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ y = sSup S
h₀ : s ≠ ⊥
z₁ : Closeds α
hz₁' : ¬↑s ⊆ ↑z₁
z₂ : Closeds α
hz₂' : ¬↑s ⊆ ↑z₂
h : ↑s ⊆ ↑z₁ ∪ ↑z₂
⊢ ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ s = sSup S

Tactic:
rcases H (s ⊓ z₁) (inf_lt_left.2 hz₁') with ⟨S₁, hSf₁, hS₁, h₁⟩

Goal state after:
case neg
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
s : Closeds α
H : ∀ y < s, ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ y = sSup S
h₀ : s ≠ ⊥
z₁ : Closeds α
hz₁' : ¬↑s ⊆ ↑z₁
z₂ : Closeds α
hz₂' : ¬↑s ⊆ ↑z₂
h : ↑s ⊆ ↑z₁ ∪ ↑z₂
S₁ : Set (Closeds α)
hSf₁ : S₁.Finite
hS₁ : ∀ t ∈ S₁, IsIrreducible ↑t
h₁ : s ⊓ z₁ = sSup S₁
⊢ ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ s = sSup S
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
x : α
⊢ x ∈ f ⁻¹' U → x ∈ s

Tactic:
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
x : α
⊢ x ∈ f ⁻¹' V → x ∈ s

Tactic:
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_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
⊢ x ∈ K → ∃ t ∈ 𝓝[K] x, ∃ W, IsCompact W ∧ IsOpen[inst✝¹] W ∧ t ⊆ W ∧ W ⊆ U

Tactic:
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.Order.Ideal

Goal state before:
pp: P : Type u_1
inst✝² : PartialOrder P
inst✝¹ : OrderTop P
inst✝ : Nontrivial P
⊢ ∃ I, I.IsMaximal

Tactic:
rcases exists_ne (⊤ : P) with ⟨a, ha⟩
  rw [← isProper_principal_iff] at ha
  rcases ha.exists_le_maximal with ⟨I, -, hI⟩
  exact ⟨I, hI⟩

Goal state after:
Module: Mathlib.Topology.Sober

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
inst✝ : QuasiSober β
T : Set β
hT : IsClosed[inst✝¹] T
hS : IsIrreducible (f ⁻¹' T)
hS' : IsClosed[inst✝²] (f ⁻¹' T)
hS'' : IsIrreducible (T ∩ range f)
y : α
hx : IsGenericPoint (f y) (closure[inst✝¹] (T ∩ range f))
hxT : f y ∈ T
z : β
⊢ z ∈ range f → (z ∈ closure[inst✝¹] (T ∩ range f) ↔ z ∈ T)

Tactic:
exact fun hy => ⟨fun h => hT.closure_eq ▸ closure_mono inter_subset_left h,
      fun h => subset_closure ⟨h, hy⟩⟩

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: case compl
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
hs' : IsConstructible (f '' s)
⊢ IsConstructible (f '' sᶜ)

Tactic:
rw [← range_sdiff_image hf.injective]
    exact (hfcomp.isConstructible hf.isClosed_range.isOpen_compl).of_compl.sdiff hs'

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: case sdiff.insert
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✝ t : Set ι
ht : t.Finite
hV : ⋃ i ∈ t, b i ∈ {U | IsOpen[inst✝³] U ∧ IsRetrocompact U}
i : ι
s : Set ι
hi : i ∉ s
hs : s.Finite
ih : ∀ (hU : ⋃ i ∈ s, b i ∈ {U | IsOpen[inst✝³] U ∧ IsRetrocompact U}), P (⋃ i ∈ s, b i \ ⋃ i ∈ t, b i) ⋯
hU : ⋃ i_1 ∈ insert i s, b i_1 ∈ {U | IsOpen[inst✝³] U ∧ IsRetrocompact U}
⊢ P (⋃ i_1 ∈ insert i s, b i_1 \ ⋃ i ∈ t, b i) ⋯

Tactic:
biUnion_insert

Goal state after:
case sdiff.insert
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✝ t : Set ι
ht : t.Finite
hV : ⋃ i ∈ t, b i ∈ {U | IsOpen[inst✝³] U ∧ IsRetrocompact U}
i : ι
s : Set ι
hi : i ∉ s
hs : s.Finite
ih : ∀ (hU : ⋃ i ∈ s, b i ∈ {U | IsOpen[inst✝³] U ∧ IsRetrocompact U}), P (⋃ i ∈ s, b i \ ⋃ i ∈ t, b i) ⋯
hU : ⋃ i_1 ∈ insert i s, b i_1 ∈ {U | IsOpen[inst✝³] U ∧ IsRetrocompact U}
⊢ P ((b i \ ⋃ i ∈ t, b i) ∪ ⋃ x ∈ s, b x \ ⋃ i ∈ t, b i) ⋯
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: case neg.inl
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a : K
n : ℤ
hn : ¬n = 0
ha : ¬a = 0
h : n = ↑n.natAbs
⊢ D (a ^ ↑n.natAbs) = ↑n.natAbs • a ^ (↑n.natAbs - 1) • D a

Tactic:
simp only [zpow_natCast, leibniz_pow, natCast_zsmul]

Goal state after:
case neg.inl
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a : K
n : ℤ
hn : ¬n = 0
ha : ¬a = 0
h : n = ↑n.natAbs
⊢ n.natAbs • a ^ (n.natAbs - 1) • D a = n.natAbs • a ^ (↑n.natAbs - 1) • D a
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case h₂
G : Type u
inst✝ : Monoid G
h_congr_thm✝ :
  ∀ {b c : Prop} {α : Type} {x : Decidable b} [inst : Decidable c] {x_1 : b → α} {u : c → α} {y : ¬b → α} {v : ¬c → α}
    (h₁ : b = c), (∀ (h : c), x_1 ⋯ = u h) → (∀ (h : ¬c), y ⋯ = v h) → dite b x_1 y = dite c u v
h✝ : ∃ n, 0 < n ∧ ∀ (g : G), g ^ n = 1
x✝ : ℕ
⊢ (∀ (g : Gᵐᵒᵖ), g ^ x✝ = 1) ↔ ∀ (g : G), g ^ x✝ = 1

pp: case h₁
G : Type u
inst✝ : Monoid G
x✝ : ℕ
⊢ (∀ (g : Gᵐᵒᵖ), g ^ x✝ = 1) ↔ ∀ (g : G), g ^ x✝ = 1

Tactic:
all_goals exact ⟨(op_injective <| · <| op ·), (unop_injective <| · <| unop ·)⟩

Goal state after:
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))
x : (i : ι) → R i
⊢ x ∈ RingHom.ker (Pi.evalRingHom R i) → x ∈ p.asIdeal

Tactic:
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.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst✝³ : Group α
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : IsCyclic α
H : Subgroup α
this : (a : Prop) → Decidable a
g : α
hg : ∀ (x : α), x ∈ zpowers g
hx : ¬∃ x ∈ H, x ≠ 1
x : α
h : x ∈ ⊥
⊢ x ∈ H

Tactic:
by rw [Subgroup.mem_bot.1 h]; exact H.one_mem

Goal state after:
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
x : α
⊢ x ∈ {a | a ^ n = 1} → x ∈ (↑(zpowers (g ^ (Fintype.card α / n.gcd (Fintype.card α))))).toFinset

Tactic:
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.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
⊢ Nat.card G = 1 ∨ p ∣ Nat.card G

Tactic:
cases finite_or_infinite G
  · obtain ⟨n, hn⟩ := iff_card.mp hG
    rw [hn]
    rcases n with - | n
    · exact Or.inl rfl
    · exact Or.inr ⟨p ^ n, by rw [pow_succ']⟩
  · rw [Nat.card_eq_zero_of_infinite]
    exact Or.inr ⟨0, rfl⟩

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
this : Fintype α
⊢ Nat.card α ≡ Nat.card ↑(fixedPoints G α) [MOD p]

Tactic:
have := Fintype.ofFinite (fixedPoints G α)

Goal state after:
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
this✝ : Fintype α
this : Fintype ↑(fixedPoints G α)
⊢ Nat.card α ≡ Nat.card ↑(fixedPoints G α) [MOD p]
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case H'
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : ExponentExists G
x : ℕ
⊢ x < exponent G → ∃ a ∈ Set.range fun g ↦ orderOf g, x < a

Tactic:
hx

Goal state after:
case H'
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : ExponentExists G
x : ℕ
hx : x < exponent G
⊢ ∃ a ∈ Set.range fun g ↦ orderOf g, x < a
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
a b : { e // e.1 * e.2 = 0 ∧ e.1 + e.2 = 1 }
h : basicOpen ((↑a).1 * (↑b).1) = basicOpen (↑a).1
this : IsIdempotentElem (↑a).1
⊢ a ⊓ b = a

Tactic:
exact mul_eq_zero_add_eq_one_ext_left (basicOpen_injOn_isIdempotentElem
      (this.mul (IsIdempotentElem.of_mul_add b.2.1 b.2.2).1) this h)

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

Goal state before:
pp: case a
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal S
x : PrimeSpectrum R
hx : Ideal.comap f I ≤ x.asIdeal
p' : Ideal S
hp' : p'.IsPrime
hp'' : I ≤ p'
hq₁ : Ideal.comap f p' ∈ (Ideal.comap f I).minimalPrimes
hq₂ : Ideal.comap f p' ≤ x.asIdeal
⊢ x ∈ closure (comap f '' zeroLocus ↑I)

Tactic:
let p'' : PrimeSpectrum S := ⟨p', hp'⟩

Goal state after:
case a
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal S
x : PrimeSpectrum R
hx : Ideal.comap f I ≤ x.asIdeal
p' : Ideal S
hp' : p'.IsPrime
hp'' : I ≤ p'
hq₁ : Ideal.comap f p' ∈ (Ideal.comap f I).minimalPrimes
hq₂ : Ideal.comap f p' ≤ x.asIdeal
p'' : PrimeSpectrum S := { asIdeal := p', isPrime := hp' }
⊢ x ∈ closure (comap f '' zeroLocus ↑I)
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
hG : Monoid.exponent G = 2
x : G
⊢ orderOf x = 2 → x ≠ 1

Tactic:
rintro hx rfl; norm_num at hx

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

Goal state before:
pp: α : Type u_1
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → #{a | a ^ n = 1} ≤ n
a : α
b : ↥(zpowers a)
i : ℤ
hi : (fun x ↦ a ^ x) i = ↑b
⊢ 1 ^ i = 1

Tactic:
one_zpow

Goal state after:
α : Type u_1
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → #{a | a ^ n = 1} ≤ n
a : α
b : ↥(zpowers a)
i : ℤ
hi : (fun x ↦ a ^ x) i = ↑b
⊢ 1 = 1
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P Q : Sylow p G
⊢ ∃ g, g • P = Q

Tactic:
by
    have H := fun {R : Sylow p G} {S : orbit G P} =>
      calc
        S ∈ fixedPoints R (orbit G P) ↔ S.1 ∈ fixedPoints R (Sylow p G) :=
          forall_congr' fun a => Subtype.ext_iff
        _ ↔ R.1 ≤ S := R.2.sylow_mem_fixedPoints_iff
        _ ↔ S.1.1 = R := ⟨fun h => R.3 S.1.2 h, ge_of_eq⟩
    suffices Set.Nonempty (fixedPoints Q (orbit G P)) by
      exact Exists.elim this fun R hR => by
        rw [← Sylow.ext (H.mp hR)]
        exact R.2
    apply Q.2.nonempty_fixed_point_of_prime_not_dvd_card
    refine fun h => hp.out.not_dvd_one (Nat.modEq_zero_iff_dvd.mp ?_)
    calc
      1 = Nat.card (fixedPoints P (orbit G P)) := ?_
      _ ≡ Nat.card (orbit G P) [MOD p] := (P.2.card_modEq_card_fixedPoints (orbit G P)).symm
      _ ≡ 0 [MOD p] := Nat.modEq_zero_iff_dvd.mpr h
    rw [← Nat.card_unique (α := ({⟨P, mem_orbit_self P⟩} : Set (orbit G P))), eq_comm]
    congr
    rw [Set.eq_singleton_iff_unique_mem]
    exact ⟨H.mpr rfl, fun R h => Subtype.ext (Sylow.ext (H.mp h))⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
p : ℕ
hp : Nat.Prime p
hα : Nat.card α = p ^ 2
this✝¹ : Finite α
this✝ : Nontrivial α
h_cyc : ¬IsCyclic α
g : α
hg : g ≠ 1
this : orderOf g ∈ (p ^ 2).divisors
⊢ ∃ a < 3, p ^ a = orderOf g

Tactic:
simpa [Nat.divisors_prime_pow hp 2] using this

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

Goal state before:
pp: G : Type u_2
inst✝¹ : Group G
inst✝ : Finite G
h : IsCyclic G
⊢ Nat.card (MulAut G) = Nat.card (ZMod (Nat.card G))ˣ

Tactic:
exact Nat.card_congr (mulAutMulEquiv G)

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝¹ : Group G
H : Subgroup G
inst✝ : Finite ↑↑H
x : G
hx : ∀ (n : G), n ∈ H ↔ x * n * x⁻¹ ∈ H
y✝ : G ⧸ H
y : G
hy : Quotient.mk'' y ∈ orbit ↥H ↑x
b : G
hb₁ : b ∈ H
hb₂✝ : (fun m ↦ m • ↑x) ⟨b, hb₁⟩ = Quotient.mk'' y
hb₂ : (b * x)⁻¹ * y ∈ H
⊢ b⁻¹ * (x * (y⁻¹ * x)⁻¹ * x⁻¹) ∈ H

Tactic:
hx

Goal state after:
G : Type u
inst✝¹ : Group G
H : Subgroup G
inst✝ : Finite ↑↑H
x : G
hx : ∀ (n : G), n ∈ H ↔ x * n * x⁻¹ ∈ H
y✝ : G ⧸ H
y : G
hy : Quotient.mk'' y ∈ orbit ↥H ↑x
b : G
hb₁ : b ∈ H
hb₂✝ : (fun m ↦ m • ↑x) ⟨b, hb₁⟩ = Quotient.mk'' y
hb₂ : x * ((b * x)⁻¹ * y) * x⁻¹ ∈ H
⊢ b⁻¹ * (x * (y⁻¹ * x)⁻¹ * x⁻¹) ∈ H