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

Goal state before:
pp: case neg
R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
hz : IsAlgebraic R z
inj : ∃ a, (algebraMap R A) a = 0 ∧ a ≠ 0
r : R
eq : (algebraMap R A) r = 0
ne : r ≠ 0
⊢ ∃ y, y ≠ 0 ∧ IsIntegral R (y • z)

Tactic:
exact ⟨r, ne, by simpa [← algebraMap_smul A, eq, zero_smul] using isIntegral_zero⟩

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

Goal state before:
pp: R : Type u
M : Type v
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N1 : Type u_1
inst✝⁵ : AddCommGroup N1
inst✝⁴ : Module R N1
N2 : Type u_2
inst✝³ : AddCommGroup N2
inst✝² : Module R N2
N3 : Type u_3
inst✝¹ : AddCommGroup N3
inst✝ : Module R N3
l12 : N1 →ₗ[R] N2
l23 : N2 →ₗ[R] N3
fl : FaithfullyFlat R M
ex : Function.Exact ⇑(LinearMap.rTensor M l12) ⇑(LinearMap.rTensor M l23)
n1 : N1
hn1 : l23 (l12 n1) ≠ 0
E : Submodule R N3 := R ∙ l23 (l12 n1)
hE : Nontrivial ↥E
eq1 : ∀ (m : M), l23 (l12 n1) ⊗ₜ[R] m = 0
x : ↥E ⊗[R] M
⊢ x ∈ ⊤ ↔ x ∈ ⊥

Tactic:
simp only [Submodule.mem_top, Submodule.mem_bot, true_iff]

Goal state after:
R : Type u
M : Type v
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N1 : Type u_1
inst✝⁵ : AddCommGroup N1
inst✝⁴ : Module R N1
N2 : Type u_2
inst✝³ : AddCommGroup N2
inst✝² : Module R N2
N3 : Type u_3
inst✝¹ : AddCommGroup N3
inst✝ : Module R N3
l12 : N1 →ₗ[R] N2
l23 : N2 →ₗ[R] N3
fl : FaithfullyFlat R M
ex : Function.Exact ⇑(LinearMap.rTensor M l12) ⇑(LinearMap.rTensor M l23)
n1 : N1
hn1 : l23 (l12 n1) ≠ 0
E : Submodule R N3 := R ∙ l23 (l12 n1)
hE : Nontrivial ↥E
eq1 : ∀ (m : M), l23 (l12 n1) ⊗ₜ[R] m = 0
x : ↥E ⊗[R] M
⊢ x = 0
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
f g : R
⊢ zeroLocus {f} ⊆ zeroLocus {g} ↔ g ∈ (Ideal.span {f}).radical

Tactic:
rw [← zeroLocus_span {f}, ← zeroLocus_span {g}, zeroLocus_subset_zeroLocus_iff, Ideal.span_le,
    Set.singleton_subset_iff, SetLike.mem_coe]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
f g : R
x : PrimeSpectrum R
⊢ x ∈ zeroLocus {f * g} ↔ x ∈ zeroLocus {f} ∪ zeroLocus {g}

Tactic:
by simpa using x.2.mul_mem_iff_mem_or_mem

Goal state after:
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
⊢ f.SurjectiveOnStalks ↔
    ∀ (I : Ideal S) (x : I.IsMaximal), Function.Surjective ⇑(Localization.localRingHom (Ideal.comap f I) I f ⋯)

Tactic:
by
  refine ⟨fun H I hI ↦ H I hI.isPrime, fun H I hI ↦ ?_⟩
  simp_rw [surjective_localRingHom_iff] at H ⊢
  intro s
  obtain ⟨M, hM, hIM⟩ := I.exists_le_maximal hI.ne_top
  obtain ⟨x, r, c, hc, hr, e⟩ := H M hM s
  exact ⟨x, r, c, fun h ↦ hc (hIM h), fun h ↦ hr (hIM h), e⟩

Goal state after:
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
T : Type u_3
inst✝ : CommRing T
g : S →+* T
f : R →+* S
hg : g.SurjectiveOnStalks
hf : f.SurjectiveOnStalks
⊢ (g.comp f).SurjectiveOnStalks

Tactic:
intro I hI

Goal state after:
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
T : Type u_3
inst✝ : CommRing T
g : S →+* T
f : R →+* S
hg : g.SurjectiveOnStalks
hf : f.SurjectiveOnStalks
I : Ideal T
hI : I.IsPrime
⊢ Function.Surjective ⇑(Localization.localRingHom (Ideal.comap (g.comp f) I) I (g.comp f) ⋯)
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
T : Type u_3
inst✝ : CommRing T
g : S →+* T
f : R →+* S
hg : g.SurjectiveOnStalks
hf : f.SurjectiveOnStalks
I : Ideal T
hI : I.IsPrime
⊢ Function.Surjective ⇑(Localization.localRingHom (Ideal.comap (g.comp f) I) I (g.comp f) ⋯)

Tactic:
have := (hg I hI).comp (hf _ (hI.comap g))

Goal state after:
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
T : Type u_3
inst✝ : CommRing T
g : S →+* T
f : R →+* S
hg : g.SurjectiveOnStalks
hf : f.SurjectiveOnStalks
I : Ideal T
hI : I.IsPrime
this :
  Function.Surjective
    (⇑(Localization.localRingHom (Ideal.comap g I) I g ⋯) ∘
      ⇑(Localization.localRingHom (Ideal.comap f (Ideal.comap g I)) (Ideal.comap g I) f ⋯))
⊢ Function.Surjective ⇑(Localization.localRingHom (Ideal.comap (g.comp f) I) I (g.comp f) ⋯)
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
T : Type u_3
inst✝ : CommRing T
g : S →+* T
f : R →+* S
hg : (g.comp f).SurjectiveOnStalks
⊢ g.SurjectiveOnStalks

Tactic:
intro I hI

Goal state after:
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
T : Type u_3
inst✝ : CommRing T
g : S →+* T
f : R →+* S
hg : (g.comp f).SurjectiveOnStalks
I : Ideal T
hI : I.IsPrime
⊢ Function.Surjective ⇑(Localization.localRingHom (Ideal.comap g I) I g ⋯)
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: case tmul
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Algebra R S
hf₂ : (algebraMap R T).SurjectiveOnStalks
J : Ideal T
hJ : J.IsPrime
x₁ : S
x₂ : T
⊢ ∃ t r a, r • t ∉ J ∧ 1 ⊗ₜ[R] (r • t) * x₁ ⊗ₜ[R] x₂ = a ⊗ₜ[R] t

Tactic:
obtain ⟨y, s, c, hs, hc, e⟩ := (surjective_localRingHom_iff _).mp (hf₂ J hJ) x₂

Goal state after:
case tmul
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Algebra R S
hf₂ : (algebraMap R T).SurjectiveOnStalks
J : Ideal T
hJ : J.IsPrime
x₁ : S
x₂ : T
y s : R
c : T
hs : c ∉ J
hc : (algebraMap R T) s ∉ J
e : c * (algebraMap R T) s * x₂ = c * (algebraMap R T) y
⊢ ∃ t r a, r • t ∉ J ∧ 1 ⊗ₜ[R] (r • t) * x₁ ⊗ₜ[R] x₂ = a ⊗ₜ[R] t
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:
rw [isNoetherian_iff'] at h ⊢

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.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a✝ b✝ a b : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
hab : (↑a).1 * (↑b).1 = (↑a).1
hba : (↑b).1 * (↑a).1 = (↑b).1
⊢ (↑a).1 = (↑b).1

Tactic:
by rw [← hab, mul_comm, hba]

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a✝ b✝ a b : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
⊢ (↑a).1 * ((↑b).1 * (↑b).1) = (↑a).1 * (↑b).1

Tactic:
(IsIdempotentElem.of_mul_add b.2.1 b.2.2).1.eq

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : CommSemigroup S
a b : { a // IsIdempotentElem a }
hab : ↑a * ↑b = ↑a
hba : ↑b * ↑a = ↑b
⊢ ↑a = ↑b

Tactic:
by rw [← hab, mul_comm, hba]

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Idempotent

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

Tactic:
simp_rw [mul_right_comm]

Goal state after:
R : Type u_1
S : Type u_2
inst✝ : CommSemigroup S
a b : { a // IsIdempotentElem a }
⊢ ↑a * ↑a * ↑b = ↑a * ↑b
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
a b : PrimeSpectrum S
⊢ comap f a.asIdeal ≤ comap f b.asIdeal ↔ a ≤ b

Tactic:
rw [← Ideal.map_le_iff_le_comap, Ideal.map_comap_of_surjective f hf,
      PrimeSpectrum.asIdeal_le_asIdeal]

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

Tactic:
refine ⟨fun h i ↦ h.restrictPreimage _, fun H s hs ↦ ?_⟩

Goal state after:
α : 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
⊢ IsOpen[inst✝] (f '' s)
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
⊢ IsHomeomorph f ↔ ∀ (i : ι), IsHomeomorph ((U i).carrier.restrictPreimage f)

Tactic:
simp_rw [isHomeomorph_iff_isEmbedding_surjective, forall_and,
    ← isEmbedding_iff_restrictPreimage hU h,
    surjective_iff_surjective_of_iUnion_eq_univ hU.iSup_set_eq_univ, Opens.carrier_eq_coe]

Goal state after:
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)
tfae_3_to_4 :
  (∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)) →
    ∀ x ∈ s, ∃ U, x ∈ U ∧ IsOpen[inst✝] U ∧ U ∩ closure[inst✝] s ⊆ s
x✝ : ∀ x ∈ s, ∃ U, x ∈ U ∧ IsOpen[inst✝] U ∧ U ∩ closure[inst✝] s ⊆ s
H : ∀ x ∈ s, ∃ U, x ∈ U ∧ IsOpen[inst✝] U ∧ U ∩ closure[inst✝] s ⊆ s := x✝
⊢ IsOpen[instTopologicalSpaceSubtype] (closure[inst✝] s ↓∩ s)

Tactic:
by
    choose U hxU hU e using H
    refine ⟨⋃ x ∈ s, U x ‹_›, isOpen_iUnion (isOpen_iUnion <| hU ·), ext fun x ↦ ⟨?_, ?_⟩⟩
    · rintro ⟨_, ⟨⟨y, rfl⟩, ⟨_, ⟨hy, rfl⟩, hxU⟩⟩⟩
      exact e y hy ⟨hxU, x.2⟩
    · exact (subset_iUnion₂ _ _ <| hxU x ·)

Goal state after:
Module: Mathlib.Topology.LocallyClosed

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ [IsLocallyClosed s, IsOpen[inst✝] (coborder s), ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s),
      ∀ x ∈ s, ∃ U, x ∈ U ∧ IsOpen[inst✝] U ∧ U ∩ closure[inst✝] s ⊆ s,
      IsOpen[instTopologicalSpaceSubtype] (closure[inst✝] s ↓∩ s)].TFAE

Tactic:
by
  tfae_have 1 → 2 := by
    rintro ⟨U, Z, hU, hZ, rfl⟩
    have : Z ∪ (frontier (U ∩ Z))ᶜ = univ := by
      nth_rw 1 [← hZ.closure_eq]
      rw [← compl_subset_iff_union, compl_subset_compl]
      refine frontier_subset_closure.trans (closure_mono inter_subset_right)
    rw [coborder_eq_union_frontier_compl, inter_union_distrib_right, this,
      inter_univ]
    exact hU.union isClosed_frontier.isOpen_compl
  tfae_have 2 → 3
  | h, x => (⟨coborder s, h.mem_nhds <| subset_coborder ·, isClosed_preimage_val_coborder⟩)
  tfae_have 3 → 4
  | h, x, hx => by
    obtain ⟨t, ht, ht'⟩ := h x hx
    obtain ⟨U, hUt, hU, hxU⟩ := mem_nhds_iff.mp ht
    rw [isClosed_preimage_val] at ht'
    exact ⟨U, hxU, hU, (subset_inter (inter_subset_left.trans hUt) (hU.inter_closure.trans
      (closure_mono <| inter_subset_inter hUt subset_rfl))).trans ht'⟩
  tfae_have 4 → 5
  | H => by
    choose U hxU hU e using H
    refine ⟨⋃ x ∈ s, U x ‹_›, isOpen_iUnion (isOpen_iUnion <| hU ·), ext fun x ↦ ⟨?_, ?_⟩⟩
    · rintro ⟨_, ⟨⟨y, rfl⟩, ⟨_, ⟨hy, rfl⟩, hxU⟩⟩⟩
      exact e y hy ⟨hxU, x.2⟩
    · exact (subset_iUnion₂ _ _ <| hxU x ·)
  tfae_have 5 → 1
  | H => by
    convert!
      H.isLocallyClosed.image IsInducing.subtypeVal
        (by simpa using isClosed_closure.isLocallyClosed)
    simpa using subset_closure
  tfae_finish

Goal state after:
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : QuasiSeparatedSpace α
s : Set (Set α)
hf : s.Finite
hne : s.Nonempty
ho : ∀ t ∈ s, IsOpen[inst✝¹] t ∨ IsClosed[inst✝¹] t
hc : ∀ t ∈ s, IsCompact t
this :
  ∀ {α : Type u_1} [inst : TopologicalSpace α] [QuasiSeparatedSpace α] {s : Set (Set α)},
    s.Finite →
      s.Nonempty → (∀ t ∈ s, IsOpen t ∨ IsClosed t) → (∀ t ∈ s, IsCompact t) → (∀ t ∈ s, IsOpen t) → IsCompact (⋂₀ s)
h : ¬∀ t ∈ s, IsOpen[inst✝¹] t
⊢ IsCompact (⋂₀ s)

Tactic:
let a := { t ∈ s | IsOpen t }

Goal state after:
case inr
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : QuasiSeparatedSpace α
s : Set (Set α)
hf : s.Finite
hne : s.Nonempty
ho : ∀ t ∈ s, IsOpen[inst✝¹] t ∨ IsClosed[inst✝¹] t
hc : ∀ t ∈ s, IsCompact t
this :
  ∀ {α : Type u_1} [inst : TopologicalSpace α] [QuasiSeparatedSpace α] {s : Set (Set α)},
    s.Finite →
      s.Nonempty → (∀ t ∈ s, IsOpen t ∨ IsClosed t) → (∀ t ∈ s, IsCompact t) → (∀ t ∈ s, IsOpen t) → IsCompact (⋂₀ s)
h : ¬∀ t ∈ s, IsOpen[inst✝¹] t
a : Set (Set α) := {t | t ∈ s ∧ IsOpen[inst✝¹] t}
⊢ IsCompact (⋂₀ s)
Module: Mathlib.Topology.Constructible

Goal state before:
pp: case open_retrocompact
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)ᶜ
U : Set X
hUopen : IsOpen[inst✝¹] U
hUcomp : IsRetrocompact U
hfU : IsOpen[inst✝] (f '' U ∪ (range f)ᶜ)
⊢ IsConstructible (f '' U)

Tactic:
suffices h : IsRetrocompact (f '' U ∪ (range f)ᶜ) by
      simpa [union_inter_distrib_right, inter_eq_left.2 (image_subset_range ..)]
        using (h.isConstructible hfU).sdiff (hfcomp.isConstructible hf.isClosed_range.isOpen_compl)

Goal state after:
case open_retrocompact
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)ᶜ
U : Set X
hUopen : IsOpen[inst✝¹] U
hUcomp : IsRetrocompact U
hfU : IsOpen[inst✝] (f '' U ∪ (range f)ᶜ)
⊢ IsRetrocompact (f '' U ∪ (range f)ᶜ)
Module: Mathlib.RingTheory.Derivation.ToSquareZero

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
inst✝¹ : Algebra A B
hI : I ^ 2 = ⊥
inst✝ : IsScalarTower R A B
d : Derivation R A ↥I
x : A
⊢ (Ideal.Quotient.mk I) ↑(d x) + (Ideal.Quotient.mk I) ((algebraMap A B) x) = (algebraMap A (B ⧸ I)) x

Tactic:
Ideal.Quotient.eq_zero_iff_mem.mpr (d x).prop,

Goal state after:
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
inst✝¹ : Algebra A B
hI : I ^ 2 = ⊥
inst✝ : IsScalarTower R A B
d : Derivation R A ↥I
x : A
⊢ 0 + (Ideal.Quotient.mk I) ((algebraMap A B) x) = (algebraMap A (B ⧸ I)) x
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
Zs : Set (Set (PrimeSpectrum R))
h : Zs ⊆ Set.range zeroLocus
⊢ ⋂₀ Zs ∈ Set.range zeroLocus

Tactic:
rw [Set.sInter_eq_iInter]

Goal state after:
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
Zs : Set (Set (PrimeSpectrum R))
h : Zs ⊆ Set.range zeroLocus
⊢ ⋂ i, ↑i ∈ Set.range zeroLocus
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
S✝ : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S✝
ι✝ : Type u
S : ι✝ → Set (PrimeSpectrum R)
S_closed : ∀ (i : ι✝), IsClosed (S i)
S_empty : ⋂ i, S i = ∅
I : ι✝ → Ideal R
hI : ∀ (i : ι✝), S i = zeroLocus ↑(I i)
⊢ ∃ u, ⋂ i ∈ u, S i = ∅

Tactic:
simp_rw [hI, ← zeroLocus_iSup, zeroLocus_empty_iff_eq_top, ← top_le_iff] at S_empty ⊢

Goal state after:
R : Type u
S✝ : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S✝
ι✝ : Type u
S : ι✝ → Set (PrimeSpectrum R)
S_closed : ∀ (i : ι✝), IsClosed (S i)
I : ι✝ → Ideal R
hI : ∀ (i : ι✝), S i = zeroLocus ↑(I i)
S_empty : ⊤ ≤ ⨆ i, I i
⊢ ∃ u, ⊤ ≤ ⨆ i ∈ u, I i
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : DiscreteTopology (PrimeSpectrum R)
x : PiLocalization R
⊢ ∃ a, (toPiLocalization R) a = x

Tactic:
have (p : PrimeSpectrum R) : ∃ f, (basicOpen f : Set _) = {p} :=
    have ⟨_, ⟨f, rfl⟩, hpf, hfp⟩ := isTopologicalBasis_basic_opens.isOpen_iff.mp
      (isOpen_discrete {p}) p rfl
    ⟨f, hfp.antisymm <| Set.singleton_subset_iff.mpr hpf⟩

Goal state after:
R : Type u
inst✝¹ : CommSemiring R
inst✝ : DiscreteTopology (PrimeSpectrum R)
x : PiLocalization R
this : ∀ (p : PrimeSpectrum R), ∃ f, ↑(basicOpen f) = {p}
⊢ ∃ a, (toPiLocalization R) a = x
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : Group α
inst✝ : Infinite α
g : α
h : ∀ (x : α), x ∈ zpowers g
⊢ orderOf g = 0

Tactic:
rw [orderOf_eq_card_of_forall_mem_zpowers h, Nat.card_eq_zero_of_infinite]

Goal state after:
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)
span_eq : Ideal.span (Set.range f) = ⊤
hf : ∀ (a : ↑(Set.range f)), ↑(basicOpen ↑a) = {e.symm a}
a b : ↑(Set.range f)
ne : a ≠ b
⊢ basicOpen (↑a * ↑b) = ⊥

Tactic:
by
        simp_rw [basicOpen_mul, SetLike.ext'_iff, TopologicalSpace.Opens.coe_inf, hf]
        exact bot_unique (fun _ ⟨ha, hb⟩ ↦ ne <| e.symm.injective (ha.symm.trans hb))

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
S : Submonoid G
g : G
g_in_s : g ∈ S
this : ⟨g ^ exponent ↥S, ⋯⟩ = 1
⊢ g ^ exponent ↥S = 1

Tactic:
← OneMemClass.coe_eq_one

Goal state after:
G : Type u
inst✝ : Monoid G
S : Submonoid G
g : G
g_in_s : g ∈ S
this : ↑⟨g ^ exponent ↥S, ⋯⟩ = 1
⊢ g ^ exponent ↥S = 1
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case h
G : Type u
inst✝ : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range orderOf).Nonempty
hfin : (Set.range orderOf).Finite
t : G
ht : orderOf t = sSup (Set.range orderOf)
⊢ (exponent G).primeFactorsList.Subperm (orderOf t).primeFactorsList

Tactic:
List.subperm_ext_iff

Goal state after:
case h
G : Type u
inst✝ : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range orderOf).Nonempty
hfin : (Set.range orderOf).Finite
t : G
ht : orderOf t = sSup (Set.range orderOf)
⊢ ∀ x ∈ (exponent G).primeFactorsList,
    List.count x (exponent G).primeFactorsList ≤ List.count x (orderOf t).primeFactorsList
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
hH : IsPGroup p ↥H
K : Type u_2
inst✝ : Group K
ϕ : K →* G
hϕ : IsPGroup p ↥ϕ.ker
⊢ IsPGroup p ↥(Subgroup.comap ϕ H)

Tactic:
by
  intro g
  obtain ⟨j, hj⟩ := hH ⟨ϕ g.1, g.2⟩
  rw [Subtype.ext_iff, H.coe_pow, Subtype.coe_mk, ← ϕ.map_pow] at hj
  obtain ⟨k, hk⟩ := hϕ ⟨g.1 ^ p ^ j, hj⟩
  rw [Subtype.ext_iff, ϕ.ker.coe_pow, Subtype.coe_mk, ← pow_mul, ← pow_add] at hk
  exact ⟨j + k, by rwa [Subtype.ext_iff, (H.comap ϕ).coe_pow]⟩

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
s : Clopens (PrimeSpectrum R)
e f : R
mul : e * f = 0
add : e + f = 1
eq : s.carrier = ↑(basicOpen e)
⊢ ∃ a, (fun e ↦ { carrier := ↑(basicOpen (↑e).1), isClopen' := ⋯ }) a = s

Tactic:
exact ⟨⟨(e, f), mul, add⟩, SetLike.ext' eq.symm⟩

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝¹ : Monoid G
inst✝ : IsCancelMul G
a b : G
h : ∀ (g : G), g ^ 2 = 1
⊢ Commute a b

Tactic:
commute_iff_eq,

Goal state after:
G : Type u
inst✝¹ : Monoid G
inst✝ : IsCancelMul G
a b : G
h : ∀ (g : G), g ^ 2 = 1
⊢ a * b = b * a
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝ : Group G
g : G
P : Sylow p G
⊢ g • P = P ↔ g ∈ normalizer ↑P

Tactic:
rw [eq_comm, SetLike.ext_iff, ← inv_mem_iff (G := G) (H := normalizer P),
      mem_set_normalizer_iff, inv_inv]
  exact
    forall_congr' fun h =>
      iff_congr Iff.rfl
        ⟨fun ⟨a, b, c⟩ => c ▸ by simpa [mul_assoc] using b,
          fun hh => ⟨(MulAut.conj g)⁻¹ h, hh, MulAut.apply_inv_self G (MulAut.conj g) h⟩⟩

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
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : {a | orderOf a = d} = ∅
m : ℕ
hm₁ : m ∈ c.divisors
hm₂ : m ∉ c.divisors.erase d
this : m = d
⊢ #{a | orderOf a = m} = 0

Tactic:
simp [this, h0]

Goal state after:
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Semiring R
inst✝ : Module R M
tR : IsAddTorsion R
f : M
n : ℕ
npos : 0 < n
hn : n • 1 = 0
⊢ ∃ n, 0 < n ∧ n • f = 0

Tactic:
exact ⟨n, npos, by simp only [← Nat.cast_smul_eq_nsmul R _ f, ← nsmul_one, hn, zero_smul]⟩

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Group α
inst✝ : IsCyclic α
g : α
hg : orderOf g = Nat.card α
⊢ Nat.card α ∣ exponent α

Tactic:
rw [← hg]

Goal state after:
α : Type u_1
inst✝¹ : Group α
inst✝ : IsCyclic α
g : α
hg : orderOf g = Nat.card α
⊢ orderOf g ∣ exponent α
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
inst✝ : CommMonoid G
p : ℕ
hp : Fact (Nat.Prime p)
p' : ℕ
hp' : Fact (Nat.Prime p')
hne : p ≠ p'
g : G
hg : g ∈ primaryComponent G p
hg' : g ∈ primaryComponent G p'
⊢ g = 1

Tactic:
by
    rw [mem_primaryComponent_iff_orderOf] at hg hg'
    obtain ⟨_ | n, hn⟩ := hg
    · rwa [pow_zero, orderOf_eq_one_iff] at hn
    · obtain ⟨_, hn'⟩ := hg'
      exact absurd (eq_of_prime_pow_eq hp.out.prime hp'.out.prime n.succ_pos (hn ▸ hn')) hne

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:
rw [hx] at hb₂; simpa [mul_inv_rev, mul_assoc] using hb₂

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝¹ : Group G
H : Subgroup G
inst✝ : Finite ↑↑H
x✝ y✝ : ↥(normalizer ↑H)
⊢ (leftRel (comap (normalizer H.carrier).subtype H)) x✝ y✝ ↔ (leftRel H) ↑x✝ ↑y✝

Tactic:
leftRel_apply (α := normalizer (H : Set G)),

Goal state after:
G : Type u
inst✝¹ : Group G
H : Subgroup G
inst✝ : Finite ↑↑H
x✝ y✝ : ↥(normalizer ↑H)
⊢ x✝⁻¹ * y✝ ∈ comap (normalizer H.carrier).subtype H ↔ (leftRel H) ↑x✝ ↑y✝
Module: Mathlib.RingTheory.Coprime.Ideal

Goal state before:
pp: case refine_1.refine_2
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
⊢ ↑((fun i ↦ if h : i = a then ⟨1, ⋯⟩ else 0) a) = 1

Tactic:
· simp only [dif_pos, Submodule.coe_mk]

Goal state after:
Module: Mathlib.RingTheory.SimpleModule.Basic

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
s : Set (Submodule R M)
ind : iSupIndep Subtype.val
sSup : SupSet.sSup s = ⊤
simple : ∀ m ∈ s, IsSimpleModule R ↥m
⊢ M ≃ₗ[R] Π₀ (m : ↑s), ↥↑m

Tactic:
exact .symm <| .trans (.ofInjective _ ind.dfinsupp_lsum_injective) <| .trans (.ofEq _ ⊤ <|
    by rw [← Submodule.iSup_eq_range_dfinsupp_lsum, ← sSup, sSup_eq_iSup']) Submodule.topEquiv

Goal state after:
Module: Mathlib.RingTheory.SimpleModule.Basic

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p q : Submodule R M
x✝¹ : IsSemisimpleModule R ↥p
x✝ : IsSemisimpleModule R ↥q
f : Bool → Submodule R M := fun t ↦ Bool.rec q p t
⊢ ∀ i ∈ Set.univ, IsSemisimpleModule R ↥(f i)

Tactic:
by rintro (_ | _) _ <;> assumption

Goal state after: