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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝³ : CommSemiring R
A : Type u_2
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
q : Ideal R
hqp : q.IsPrime
inst✝ : IsLocalization.AtPrime A q
I : Ideal R
hIq : q ∈ I.minimalPrimes
this : IsLocalRing A
⊢ Ideal.under R (Ideal.map (algebraMap R A) q) ∈ I.minimalPrimes

Tactic:
map_eq_maximalIdeal q A,

Goal state after:
case refine_1
R : Type u_1
inst✝³ : CommSemiring R
A : Type u_2
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
q : Ideal R
hqp : q.IsPrime
inst✝ : IsLocalization.AtPrime A q
I : Ideal R
hIq : q ∈ I.minimalPrimes
this : IsLocalRing A
⊢ Ideal.under R (IsLocalRing.maximalIdeal A) ∈ I.minimalPrimes
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: case refine_2
R : Type u_1
inst✝³ : CommSemiring R
A : Type u_2
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
q : Ideal R
hqp : q.IsPrime
inst✝ : IsLocalization.AtPrime A q
I : Ideal R
hIq : q ∈ I.minimalPrimes
this : IsLocalRing A
J : Ideal A
hJ : J ∈ Ideal.under R ⁻¹' I.minimalPrimes
⊢ Ideal.map (algebraMap R A) q ≤ J

Tactic:
rw [← IsLocalization.under_le_under_iff q.primeCompl A,
      AtPrime.map_eq_maximalIdeal q A, AtPrime.under_maximalIdeal A q]

Goal state after:
case refine_2
R : Type u_1
inst✝³ : CommSemiring R
A : Type u_2
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
q : Ideal R
hqp : q.IsPrime
inst✝ : IsLocalization.AtPrime A q
I : Ideal R
hIq : q ∈ I.minimalPrimes
this : IsLocalRing A
J : Ideal A
hJ : J ∈ Ideal.under R ⁻¹' I.minimalPrimes
⊢ q ≤ Ideal.under R J
Module: Mathlib.Topology.LocallyClosed

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ (s ∪ (frontier s)ᶜ)ᶜ = closure[inst✝] s \ s

Tactic:
compl_union,

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ sᶜ ∩ (frontier s)ᶜᶜ = closure[inst✝] s \ s
Module: Mathlib.Topology.LocallyClosed

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ (s ∪ (closure[inst✝] s)ᶜ)ᶜ = closure[inst✝] s \ s

Tactic:
compl_union,

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ sᶜ ∩ (closure[inst✝] s)ᶜᶜ = closure[inst✝] s \ s
Module: Mathlib.Topology.LocallyClosed

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ sᶜ ∩ closure[inst✝] s = closure[inst✝] s \ s

Tactic:
inter_comm

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ closure[inst✝] s ∩ sᶜ = closure[inst✝] s \ s
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
h : IsInducing f
⊢ IsInducing (s.restrictPreimage f)

Tactic:
← IsInducing.subtypeVal.of_comp_iff,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
h : IsInducing f
⊢ IsInducing (Subtype.val ∘ s.restrictPreimage f)
Module: Mathlib.Topology.LocallyClosed

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
U Z : Set X
hU : IsOpen[inst✝] U
hZ : IsClosed[inst✝] Z
⊢ frontier (U ∩ Z) ⊆ closure[inst✝] Z

Tactic:
refine frontier_subset_closure.trans (closure_mono inter_subset_right)

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
⊢ IsClosedMap f ↔ ∀ (i : ι), IsClosedMap ((U i).carrier.restrictPreimage f)

Tactic:
refine ⟨fun h i => h.restrictPreimage _, fun H s hs ↦ ?_⟩
  rw [hU.isClosed_iff_coe_preimage]
  intro i
  convert! H i _ ⟨⟨_, hs.1, eq_compl_comm.mpr rfl⟩⟩
  ext ⟨x, hx⟩
  suffices (∃ y, y ∈ s ∧ f y = x) ↔ ∃ y, y ∈ s ∧ f y ∈ U i ∧ f y = x by simpa [← Subtype.coe_inj]
  exact ⟨fun ⟨a, b, c⟩ => ⟨a, b, c.symm ▸ hx, c⟩, by tauto⟩

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 : Continuous[inst✝¹, inst✝] f
⊢ IsInducing f ↔ ∀ (i : ι), IsInducing ((U i).carrier.restrictPreimage f)

Tactic:
← IsInducing.subtypeVal.of_comp_iff,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
h : Continuous[inst✝¹, inst✝] f
⊢ IsInducing f ↔ ∀ (i : ι), IsInducing (Subtype.val ∘ (U i).carrier.restrictPreimage f)
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 : α
f : BoundedLatticeHom α β
L : BooleanSubalgebra β
⊢ ∀ {a : α}, a ∈ ⇑f ⁻¹' ↑L → aᶜ ∈ ⇑f ⁻¹' ↑L

Tactic:
by simp [map_compl']

Goal state after:
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
ht : IsQuasiSeparated t
h : s ⊆ t
⊢ IsQuasiSeparated s

Tactic:
intro U V hU hU' hU'' hV hV' hV''
  exact ht U V (hU.trans h) hU' hU'' (hV.trans h) hV' hV''

Goal state after:
Module: Mathlib.Order.Ideal

Goal state before:
pp: case empty
P : Type u_2
inst✝¹ : SemilatticeSup P
inst✝ : OrderBot P
t : Ideal P
ι : Type u_3
f : ι → P
⊢ ∅.sup f ∈ t ↔ ∀ i ∈ ∅, f i ∈ t

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Order.Ideal

Goal state before:
pp: case insert
P : Type u_2
inst✝¹ : SemilatticeSup P
inst✝ : OrderBot P
t : Ideal P
ι : Type u_3
f : ι → P
a✝² : ι
s✝ : Finset ι
a✝¹ : a✝² ∉ s✝
a✝ : s✝.sup f ∈ t ↔ ∀ i ∈ s✝, f i ∈ t
⊢ (insert a✝² s✝).sup f ∈ t ↔ ∀ i ∈ insert a✝² s✝, f i ∈ t

Tactic:
simp [*]

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

Goal state before:
pp: case refine_2
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
x : Y
⊢ x ∈ ⋃ i ∈ t, f '' ↑↑i → x ∈ U

Tactic:
simp_rw [Set.mem_iUnion]

Goal state after:
case refine_2
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
x : Y
⊢ (∃ i, ∃ (_ : i ∈ t), x ∈ f '' ↑↑i) → x ∈ U
Module: Mathlib.Topology.Sets.Compacts

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
K L : Compacts α
h : Disjoint K L
x : α
⊢ x ∈ ↑K ∩ ↑L → x ∈ ∅

Tactic:
⟨hxK, hxL⟩

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
K L : Compacts α
h : Disjoint K L
x : α
hxK : x ∈ ↑K
hxL : x ∈ ↑L
⊢ x ∈ ∅
Module: Mathlib.Topology.Sets.Compacts

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α ≃ₜ β
s : Compacts α
⊢ Compacts.map ⇑f.symm ⋯ (Compacts.map ⇑f ⋯ s) = s

Tactic:
by
    ext1
    simp only [coe_map, ← image_comp, f.symm_comp_self, image_id]

Goal state after:
Module: Mathlib.Order.Ideal

Goal state before:
pp: P : Type u_1
inst✝¹ : LE P
inst✝ : OrderTop P
S : Set (Ideal P)
hS₁ : IsChain (fun x1 x2 ↦ x1 ≤ x2) S
hS₂ : S.Nonempty
hS₃ : ⊤ ∉ S
⊢ ∃ x, x ≠ ⊤ ∧ x ∈ upperBounds S

Tactic:
refine ⟨IsIdeal.toIdeal <| isIdeal_sUnion_of_isChain (C := SetLike.coe '' S) ?_
    (hS₁.image_of_map_rel _ _ _ ?_) (hS₂.image _), ?_, ?_⟩

Goal state after:
case refine_1
P : Type u_1
inst✝¹ : LE P
inst✝ : OrderTop P
S : Set (Ideal P)
hS₁ : IsChain (fun x1 x2 ↦ x1 ≤ x2) S
hS₂ : S.Nonempty
hS₃ : ⊤ ∉ S
⊢ ∀ I ∈ SetLike.coe '' S, IsIdeal I

case refine_2
P : Type u_1
inst✝¹ : LE P
inst✝ : OrderTop P
S : Set (Ideal P)
hS₁ : IsChain (fun x1 x2 ↦ x1 ≤ x2) S
hS₂ : S.Nonempty
hS₃ : ⊤ ∉ S
⊢ ∀ (x y : Ideal P), x ≤ y → ↑x ⊆ ↑y

case refine_3
P : Type u_1
inst✝¹ : LE P
inst✝ : OrderTop P
S : Set (Ideal P)
hS₁ : IsChain (fun x1 x2 ↦ x1 ≤ x2) S
hS₂ : S.Nonempty
hS₃ : ⊤ ∉ S
⊢ ⋯.toIdeal ≠ ⊤

case refine_4
P : Type u_1
inst✝¹ : LE P
inst✝ : OrderTop P
S : Set (Ideal P)
hS₁ : IsChain (fun x1 x2 ↦ x1 ≤ x2) S
hS₂ : S.Nonempty
hS₃ : ⊤ ∉ S
⊢ ⋯.toIdeal ∈ upperBounds S
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
ι : Type u_4
s : Finset ι
t : ι → Set X
ht : ∀ i ∈ s, IsRetrocompact (t i)
⊢ IsRetrocompact (s.inf t)

Tactic:
by
  induction s using Finset.cons_induction with
  | empty => simp
  | cons i s ih hi =>
    rw [Finset.inf_cons]
    exact (ht _ <| by simp).inter <| hi <| Finset.forall_of_forall_cons ht

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: case refine_1
X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
hs : IsRetrocompact s
t : Set X
htopen : IsOpen[inst✝] t
htcomp : IsCompact t
⊢ IsCompact (t ∩ s)

Tactic:
inter_comm

Goal state after:
case refine_1
X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
hs : IsRetrocompact s
t : Set X
htopen : IsOpen[inst✝] t
htcomp : IsCompact t
⊢ IsCompact (s ∩ t)
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 X
hs : IsRetrocompact s
hfemb : IsEmbedding f
hfcomp : IsRetrocompact (range f)
U : Set Y
hUcomp : IsCompact U
hUopen : IsOpen[inst✝] U
⊢ IsCompact (U ∩ range f)

Tactic:
inter_comm

Goal state after:
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hs : IsRetrocompact s
hfemb : IsEmbedding f
hfcomp : IsRetrocompact (range f)
U : Set Y
hUcomp : IsCompact U
hUopen : IsOpen[inst✝] U
⊢ IsCompact (range f ∩ U)
Module: Mathlib.Topology.Sets.Compacts

Goal state before:
pp: case empty
α : Type u_1
inst✝ : TopologicalSpace α
ι : Type u_4
f : ι → CompactOpens α
⊢ ↑(∅.sup f) = ⋃ i ∈ ∅, ↑(f i)

Tactic:
simp [*]

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

Goal state before:
pp: case insert
α : Type u_1
inst✝ : TopologicalSpace α
ι : Type u_4
f : ι → CompactOpens α
a✝² : ι
s✝ : Finset ι
a✝¹ : a✝² ∉ s✝
a✝ : ↑(s✝.sup f) = ⋃ i ∈ s✝, ↑(f i)
⊢ ↑((insert a✝² s✝).sup f) = ⋃ i ∈ insert a✝² s✝, ↑(f i)

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Topology.Sober

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

Tactic:
apply subset_antisymm

Goal state after:
case h.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✝
⊢ closure {x} ⊆ S✝

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}
Module: Mathlib.Topology.Sober

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
V W : Set α
inst✝ : QuasiSober ↑V
hW : IsClosed W
⊢ QuasiSober ↑(W ∩ V)

Tactic:
inter_comm

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
V W : Set α
inst✝ : QuasiSober ↑V
hW : IsClosed W
⊢ QuasiSober ↑(V ∩ W)
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
ι : Type u_4
U : ι → Opens X
hU : IsOpenCover U
h₁ : ∀ (i : ι), IsRetrocompact ↑(U i)
h₂ : ∀ (i : ι), IsQuasiSeparated ↑(U i)
V₁ V₂ : Set X
ho₁ : IsOpen[inst✝] V₁
hc₁ : IsCompact V₁
ho₂ : IsOpen[inst✝] V₂
hc₂ : IsCompact V₂
t : Finset ι
ht : V₁ ⊆ ⋃ i ∈ t, (U i).carrier
⊢ V₁ ∩ V₂ = ⋃ i ∈ t, ↑(U i) ∩ V₁ ∩ (↑(U i) ∩ V₂)

Tactic:
apply subset_antisymm

Goal state after:
case a
X : Type u_2
inst✝ : TopologicalSpace X
ι : Type u_4
U : ι → Opens X
hU : IsOpenCover U
h₁ : ∀ (i : ι), IsRetrocompact ↑(U i)
h₂ : ∀ (i : ι), IsQuasiSeparated ↑(U i)
V₁ V₂ : Set X
ho₁ : IsOpen[inst✝] V₁
hc₁ : IsCompact V₁
ho₂ : IsOpen[inst✝] V₂
hc₂ : IsCompact V₂
t : Finset ι
ht : V₁ ⊆ ⋃ i ∈ t, (U i).carrier
⊢ V₁ ∩ V₂ ⊆ ⋃ i ∈ t, ↑(U i) ∩ V₁ ∩ (↑(U i) ∩ V₂)

case a
X : Type u_2
inst✝ : TopologicalSpace X
ι : Type u_4
U : ι → Opens X
hU : IsOpenCover U
h₁ : ∀ (i : ι), IsRetrocompact ↑(U i)
h₂ : ∀ (i : ι), IsQuasiSeparated ↑(U i)
V₁ V₂ : Set X
ho₁ : IsOpen[inst✝] V₁
hc₁ : IsCompact V₁
ho₂ : IsOpen[inst✝] V₂
hc₂ : IsCompact V₂
t : Finset ι
ht : V₁ ⊆ ⋃ i ∈ t, (U i).carrier
⊢ ⋃ i ∈ t, ↑(U i) ∩ V₁ ∩ (↑(U i) ∩ V₂) ⊆ V₁ ∩ V₂
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
ι : Type u_4
s : Finset ι
t : ι → Set X
ht : ∀ i ∈ s, IsLocallyConstructible (t i)
⊢ IsLocallyConstructible (s.inf t)

Tactic:
by
  induction s using Finset.cons_induction with
  | empty => simp
  | cons i s ih hi =>
    rw [Finset.inf_cons]
    exact (ht _ <| by simp).inter <| hi <| Finset.forall_of_forall_cons ht

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
hs : IsLocallyConstructible s
hf : IsOpenEmbedding f
⊢ IsLocallyConstructible (f ⁻¹' s)

Tactic:
by
  intro x
  obtain ⟨U, hxU, hU, H⟩ := hs (f x)
  exact ⟨f ⁻¹' U, hf.continuous.continuousAt.preimage_mem_nhds hxU, hU.preimage hf.continuous,
    (H.preimage_of_isOpenEmbedding (hf.restrictPreimage _) :)⟩

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝² : TopologicalSpace X
s t : Set X
inst✝¹ : PrespectralSpace X
inst✝ : QuasiSeparatedSpace X
hs : IsLocallyConstructible s
hst : s ⊆ t
ht : IsCompact t
U : X → Set X
hU : ∀ (x : X), IsOpen[inst✝²] (U x)
hU' : ∀ (x : X), IsCompact (U x)
hxU : ∀ (x : X), x ∈ U x
hUs : ∀ (x : X), IsConstructible (U x ∩ s)
σ : Finset X
hσ : ∀ x ∈ σ, x ∈ t
htσ : t ⊆ ⋃ x ∈ σ, U x
⊢ s = ⋃ i ∈ ↑σ, U i ∩ s

Tactic:
apply subset_antisymm

Goal state after:
case a
X : Type u_2
inst✝² : TopologicalSpace X
s t : Set X
inst✝¹ : PrespectralSpace X
inst✝ : QuasiSeparatedSpace X
hs : IsLocallyConstructible s
hst : s ⊆ t
ht : IsCompact t
U : X → Set X
hU : ∀ (x : X), IsOpen[inst✝²] (U x)
hU' : ∀ (x : X), IsCompact (U x)
hxU : ∀ (x : X), x ∈ U x
hUs : ∀ (x : X), IsConstructible (U x ∩ s)
σ : Finset X
hσ : ∀ x ∈ σ, x ∈ t
htσ : t ⊆ ⋃ x ∈ σ, U x
⊢ s ⊆ ⋃ i ∈ ↑σ, U i ∩ s

case a
X : Type u_2
inst✝² : TopologicalSpace X
s t : Set X
inst✝¹ : PrespectralSpace X
inst✝ : QuasiSeparatedSpace X
hs : IsLocallyConstructible s
hst : s ⊆ t
ht : IsCompact t
U : X → Set X
hU : ∀ (x : X), IsOpen[inst✝²] (U x)
hU' : ∀ (x : X), IsCompact (U x)
hxU : ∀ (x : X), x ∈ U x
hUs : ∀ (x : X), IsConstructible (U x ∩ s)
σ : Finset X
hσ : ∀ x ∈ σ, x ∈ t
htσ : t ⊆ ⋃ x ∈ σ, U x
⊢ ⋃ i ∈ ↑σ, U i ∩ s ⊆ s
Module: Mathlib.Topology.Constructible

Goal state before:
pp: case a
X : Type u_2
inst✝² : TopologicalSpace X
s t : Set X
inst✝¹ : PrespectralSpace X
inst✝ : QuasiSeparatedSpace X
hs : IsLocallyConstructible s
hst : s ⊆ t
ht : IsCompact t
U : X → Set X
hU : ∀ (x : X), IsOpen[inst✝²] (U x)
hU' : ∀ (x : X), IsCompact (U x)
hxU : ∀ (x : X), x ∈ U x
hUs : ∀ (x : X), IsConstructible (U x ∩ s)
σ : Finset X
hσ : ∀ x ∈ σ, x ∈ t
htσ : t ⊆ ⋃ x ∈ σ, U x
⊢ ⋃ i ∈ ↑σ, U i ∩ s ⊆ s

Tactic:
· exact Set.iUnion₂_subset fun _ _ ↦ Set.inter_subset_right

Goal state after:
Module: Mathlib.RingTheory.RingHom.FaithfullyFlat

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
⊢ f.FaithfullyFlat ↔ f.Flat ∧ Function.Surjective (PrimeSpectrum.comap f)

Tactic:
by
  algebraize [f]
  rw [← algebraMap_toAlgebra f, faithfullyFlat_algebraMap_iff, flat_algebraMap_iff]
  exact ⟨fun h ↦ ⟨inferInstance, PrimeSpectrum.comap_surjective_of_faithfullyFlat⟩,
    fun ⟨h, hf⟩ ↦ .of_comap_surjective hf⟩

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra.HasGoingDown R S
p q : Ideal R
inst✝³ : p.IsPrime
inst✝² : q.IsPrime
hpq : p < q
P : Ideal S
left✝ : P.IsPrime
right✝ : P.LiesOver p
inst✝¹ : P.IsPrime
inst✝ : P.LiesOver q
hPQ : P ≤ P
hc : ¬P < P
⊢ False

Tactic:
simp [P.over_def p, P.over_def q] at hpq

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
⊢ (Finite { I // I.IsPrime } ∧ ∀ (I : Ideal R), I.IsPrime → I.IsMaximal) ↔
    Finite ↑{I | I.IsMaximal} ∧ sInf {I | I.IsMaximal} ≤ nilradical R

Tactic:
← Set.coe_ofPred,

Goal state after:
R : Type u
inst✝ : CommSemiring R
⊢ (Finite ↑{x | x.IsPrime} ∧ ∀ (I : Ideal R), I.IsPrime → I.IsMaximal) ↔
    Finite ↑{I | I.IsMaximal} ∧ sInf {I | I.IsMaximal} ≤ nilradical R
Module: Mathlib.Data.ZMod.QuotientGroup

Goal state before:
pp: n : ℕ
A : Type u_1
R : Type u_2
inst✝³ : AddGroup A
inst✝² : Ring R
α : Type u_3
β : Type u_4
inst✝¹ : AddGroup α
a : α
inst✝ : AddAction α β
b : β
⊢ ((zmultiplesHom ↥(zmultiples a)) ⟨a, ⋯⟩) ↑(minimalPeriod (fun x ↦ a +ᵥ x) b) ∈ stabilizer (↥(zmultiples a)) b

Tactic:
mem_stabilizer_iff,

Goal state after:
n : ℕ
A : Type u_1
R : Type u_2
inst✝³ : AddGroup A
inst✝² : Ring R
α : Type u_3
β : Type u_4
inst✝¹ : AddGroup α
a : α
inst✝ : AddAction α β
b : β
⊢ ((zmultiplesHom ↥(zmultiples a)) ⟨a, ⋯⟩) ↑(minimalPeriod (fun x ↦ a +ᵥ x) b) +ᵥ b = b
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H : Subgroup G
hp : Fact (Nat.Prime (Nat.card G))
this✝ : Finite G
this : Nat.card ↥H = 1 ∨ Nat.card ↥H = Nat.card G
⊢ H = ⊥ ∨ H = ⊤

Tactic:
← eq_bot_iff_card,

Goal state after:
G : Type u_2
inst✝ : Group G
H : Subgroup G
hp : Fact (Nat.Prime (Nat.card G))
this✝ : Finite G
this : H = ⊥ ∨ Nat.card ↥H = Nat.card G
⊢ H = ⊥ ∨ H = ⊤
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
h₁ : Function.Surjective (comap f)
h₂ : GeneralizingMap (comap f)
⊢ IsQuotientMap (comap f)

Tactic:
by
  rw [Topology.isQuotientMap_iff_isClosed]
  refine ⟨h₁, fun s ↦ ⟨fun hs ↦ hs.preimage (continuous_comap f),
    fun hsc ↦ Set.image_preimage_eq s h₁ ▸ ?_⟩⟩
  apply isClosed_image_of_stableUnderSpecialization _ _ hsc
  rw [Set.image_preimage_eq s h₁, ← stableUnderGeneralization_compl_iff]
  convert! h₂.stableUnderGeneralization_image hsc.isOpen_compl.stableUnderGeneralization
  rw [← Set.preimage_compl, Set.image_preimage_eq _ h₁]

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: case inr
p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
h : IsPGroup p G
hp : p ≠ 0
⊢ ∃ n, Nat.card G ∣ p ^ n

Tactic:
refine ⟨Nat.card G, Nat.dvd_pow_self_iff NeZero.out hp |>.mpr fun q hq ↦ ?_⟩

Goal state after:
case inr
p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
h : IsPGroup p G
hp : p ≠ 0
q : ℕ
hq : q ∈ (Nat.card G).primeFactors
⊢ q ∈ p.primeFactors
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 }
⊢ basicOpen (↑a).1 ⊓ basicOpen (↑b).1 = basicOpen (↑a).1 ↔ a ≤ b

Tactic:
← basicOpen_mul

Goal state after:
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 }
⊢ basicOpen ((↑a).1 * (↑b).1) = basicOpen (↑a).1 ↔ a ≤ b
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal S
⊢ closure (comap f '' zeroLocus ↑I) = zeroLocus ↑(Ideal.comap f I)

Tactic:
apply subset_antisymm

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
⊢ closure (comap f '' zeroLocus ↑I) ⊆ zeroLocus ↑(Ideal.comap f I)

case a
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal S
⊢ zeroLocus ↑(Ideal.comap f I) ⊆ closure (comap f '' zeroLocus ↑I)
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: case pos
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
P : Subgroup G
hP : IsPGroup p ↥P
H : Subgroup G
inst✝ : H.Normal
h_cop : (Nat.card ↥H).Coprime H.index
h1 : Nat.card ↥H = 0
⊢ P ≤ H ∨ Disjoint H P

Tactic:
rw [h1, Nat.coprime_zero_left, Subgroup.index_eq_one] at h_cop

Goal state after:
case pos
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
P : Subgroup G
hP : IsPGroup p ↥P
H : Subgroup G
inst✝ : H.Normal
h_cop : H = ⊤
h1 : Nat.card ↥H = 0
⊢ P ≤ H ∨ Disjoint H P
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: case h.inl
α : Type u_1
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → #{a | a ^ n = 1} ≤ n
IH : ∀ m < 0, m ∣ Fintype.card α → 0 < #{a | orderOf a = m} → #{a | orderOf a = m} = φ m
hd : 0 ∣ Fintype.card α
hpos : 0 < #{a | orderOf a = 0}
⊢ #{a | orderOf a = 0} = φ 0

Tactic:
cases Fintype.card_ne_zero (eq_zero_of_zero_dvd hd)

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

Goal state before:
pp: T : Type u
inst✝¹ : CommRing T
inst✝ : IsLocalRing T
x : PrimeSpectrum (ResidueField T)
⊢ PrimeSpectrum.comap (residue T) x = closedPoint T

Tactic:
rw [Subsingleton.elim x ⊥]
  ext1
  exact Ideal.mk_ker

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommGroup α
inst✝ : IsSimpleGroup α
⊢ Nat.Prime (Nat.card α)

Tactic:
by
  have hα : Nontrivial α := IsSimpleGroup.toNontrivial
  obtain ⟨g, hg⟩ := IsCyclic.exists_generator (α := α)
  replace hα : Nat.card α ≠ 1 := by contrapose! hα; exact (Nat.card_eq_one_iff_unique.mp hα).1
  rw [← orderOf_eq_card_of_forall_mem_zpowers hg] at hα ⊢
  have h (n : ℕ) : orderOf g ∣ n ∨ n.Coprime (orderOf g) := by
    refine (IsSimpleOrder.eq_bot_or_eq_top (Subgroup.zpowers (g ^ n))).imp ?_ fun h ↦ ?_
    · simp [orderOf_dvd_iff_pow_eq_one]
    · simp only [Nat.coprime_iff_gcd_eq_one]
      have hgn : g ∈ Subgroup.zpowers (g ^ n) := by simp_all only [ne_eq, orderOf_eq_one_iff,
        Subgroup.mem_top]
      exact mem_zpowers_pow_iff.mp hgn
  apply Nat.prime_of_coprime
  · refine Nat.one_lt_iff_ne_zero_and_ne_one.mpr ⟨?_, hα⟩
    contrapose! h
    exact ⟨37, by simp [h]⟩
  · intro n hn hn0
    exact ((h n).resolve_left (Nat.not_dvd_of_pos_of_lt (Nat.pos_iff_ne_zero.mpr hn0) hn)).symm

Goal state after:
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 : Sylow p G
hP : (↑P).relIndex (normalizer ↑P) ≠ 0
⊢ ¬p ∣ (↑P).relIndex (normalizer ↑↑P) * (normalizer ↑↑P).index

Tactic:
P.coe_coe,

Goal state after:
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
hP : (↑P).relIndex (normalizer ↑P) ≠ 0
⊢ ¬p ∣ (↑P).relIndex (normalizer ↑P) * (normalizer ↑P).index
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
N : Subgroup G
inst✝¹ : N.Normal
inst✝ : Finite (Sylow p ↥N)
P : Sylow p ↥N
g : G
x✝ : g ∈ ⊤
n : ↥N
hn : n • MulAut.conjNormal g • P = P
⊢ ↑n * g ∈ normalizer ↑(map N.subtype ↑P)

Tactic:
rw [smul_def, ← mul_smul, ← MulAut.conjNormal_val, ← MulAut.conjNormal.map_mul,
    Sylow.ext_iff, pointwise_smul_def, Subgroup.pointwise_smul_def] at hn

Goal state after:
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
N : Subgroup G
inst✝¹ : N.Normal
inst✝ : Finite (Sylow p ↥N)
P : Sylow p ↥N
g : G
x✝ : g ∈ ⊤
n : ↥N
hn : map ((MulDistribMulAction.toMonoidEnd (MulAut ↥N) ↥N) (MulAut.conjNormal (↑n * g))) ↑P = ↑P
⊢ ↑n * g ∈ normalizer ↑(map N.subtype ↑P)