mathlib-initiative/mathlib-tactics huggingface dataset:
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
S : Type u_1
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : FaithfullyFlat R S
inst✝⁴ : Flat S (S ⊗[R] M)
N P : Type (max u v)
inst✝³ : AddCommGroup N
inst✝² : AddCommGroup P
inst✝¹ : Module R N
inst✝ : Module R P
f : N →ₗ[R] P
hf : Function.Injective ⇑f
this✝ : Flat R (S ⊗[R] M)
this :
  LinearMap.lTensor S (LinearMap.lTensor M f) =
    ↑(TensorProduct.assoc R S M P) ∘ₗ LinearMap.lTensor (S ⊗[R] M) f ∘ₗ ↑(TensorProduct.assoc R S M N).symm
⊢ Function.Injective ⇑(LinearMap.lTensor S (LinearMap.lTensor M f))

Tactic:
simpa [this] using Flat.lTensor_preserves_injective_linearMap f hf

Goal state after:
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: case refine_1
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
g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom
J : Ideal (S ⊗[R] T)
hJ : J.IsPrime
x : S ⊗[R] T
t : T
r : R
a : S
ht : g ((algebraMap R T) r * t) ∉ J
e : 1 ⊗ₜ[R] (r • t) * x = a ⊗ₜ[R] t
H : 1 ⊗ₜ[R] (algebraMap R T) r ∈ J
⊢ False

Tactic:
g.map_mul

Goal state after:
case refine_1
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
g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom
J : Ideal (S ⊗[R] T)
hJ : J.IsPrime
x : S ⊗[R] T
t : T
r : R
a : S
ht : g ((algebraMap R T) r) * g t ∉ J
e : 1 ⊗ₜ[R] (r • t) * x = a ⊗ₜ[R] t
H : 1 ⊗ₜ[R] (algebraMap R T) r ∈ J
⊢ False
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ᶜ ⊔ bᶜ)ᶜ ≤ b

Tactic:
by simp_rw [(· ≤ ·), (· ⊔ ·), (·ᶜ), SemilatticeSup.sup,
    mul_assoc, (IsIdempotentElem.of_mul_add b.2.1 b.2.2).1.eq]

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

Goal state before:
pp: ι : Type u_3
R : ι → Type u_2
inst✝² : (i : ι) → CommSemiring (R i)
inst✝¹ : Infinite ι
inst✝ : ∀ (i : ι), Nontrivial (R i)
J : Ideal ((i : ι) → R i) :=
  let __spread.0 := AddMonoidHom.mrange DFinsupp.coeFnAddMonoidHom;
  { toAddSubmonoid := __spread.0, smul_mem' := ⋯ }
⊢ 1 ∉ J

Tactic:
by
    -- take a maximal ideal I containing J
    rintro ⟨x, hx⟩
    have ⟨i, hi⟩ := x.support.exists_notMem
    simpa [DFinsupp.coeFnAddMonoidHom, DFinsupp.notMem_support_iff.mp hi] using congr_fun hx i

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
H : ∀ (I : Ideal R), I.IsPrime → I ∈ minimalPrimes R ∨ I.IsMaximal
⊢ KrullDimLE 1 R

Tactic:
rwa [Ring.krullDimLE_one_iff]

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
⊢ IsLocalization S ↥(subalgebra K S hS)

Tactic:
dsimp +instances only [Localization.subalgebra]

Goal state after:
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
⊢ IsLocalization S
    ↥((mapToFractionRing K S (Localization S) hS).range.copy
        {x | ∃ a s, ∃ (hs : s ∈ S), x = IsLocalization.mk' K a ⟨s, ⋯⟩} ⋯)
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b c : { x // IsIdempotentElem x }
⊢ ↑(SemilatticeInf.inf a ⟨↑b + ↑c - ↑b * ↑c, ⋯⟩) =
    ↑(SemilatticeInf.inf a b) + ↑(SemilatticeInf.inf a c) - ↑(SemilatticeInf.inf a b) * ↑(SemilatticeInf.inf a c)

Tactic:
SemilatticeInf.inf,

Goal state after:
R : Type u_1
inst✝ : CommRing R
a b c : { x // IsIdempotentElem x }
⊢ ↑(Lattice.inf a ⟨↑b + ↑c - ↑b * ↑c, ⋯⟩) =
    ↑(Lattice.inf a b) + ↑(Lattice.inf a c) - ↑(Lattice.inf a b) * ↑(Lattice.inf a c)
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b c : { x // IsIdempotentElem x }
⊢ ↑(SemilatticeInf.inf a ⟨↑b + ↑c - ↑b * ↑c, ⋯⟩) =
    ↑(SemilatticeInf.inf a b) + ↑(SemilatticeInf.inf a c) - ↑(SemilatticeInf.inf a b) * ↑(SemilatticeInf.inf a c)

Tactic:
SemilatticeInf.inf,

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

Goal state before:
pp: case refine_2
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
⊢ ∃ x, I ≤ x.asIdeal ∧ comap f x = p

Tactic:
· have hp : ker f ≤ p.asIdeal := (Ideal.comap_mono bot_le).trans h_I_p
    refine ⟨⟨p.asIdeal.map f, Ideal.map_isPrime_of_surjective hf hp⟩, fun x hx => ?_, ?_⟩
    · obtain ⟨x', rfl⟩ := hf x
      exact Ideal.mem_map_of_mem f (h_I_p hx)
    · ext x
      rw [comap_asIdeal, Ideal.mem_comap, Ideal.mem_map_iff_of_surjective f hf]
      refine ⟨?_, fun hx => ⟨x, hx, rfl⟩⟩
      rintro ⟨x', hx', heq⟩
      rw [← sub_sub_cancel x' x]
      refine p.asIdeal.sub_mem hx' (hp ?_)
      rwa [mem_ker, map_sub, sub_eq_zero]

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

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

Tactic:
rw [add_sub_cancel]

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

Goal state before:
pp: R : Type u_4
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
y : R
v : Ideal R
hv : v.IsMaximal
⊢ (algebraMap R K) y = (algebraMap R K) y * ((algebraMap R K) 1)⁻¹

Tactic:
by rw [map_one, inv_one, mul_one]

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

Goal state before:
pp: κ : Type u_2
X : Type u_3
Y : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
v : κ → Opens Y
hv : IsOpenCover v
f : C(X, Y)
⊢ IsOpenCover fun k ↦ (Opens.comap f) (v k)

Tactic:
by
  simp [IsOpenCover, ← preimage_iUnion, hv.iSup_set_eq_univ]

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

Goal state before:
pp: ι : Type u_1
X : Type u_3
inst✝¹ : TopologicalSpace X
u : ι → Opens X
hu : IsOpenCover u
inst✝ : CompactSpace X
⊢ ∃ s, IsOpenCover fun i ↦ u ↑i

Tactic:
by
  rw [IsOpenCover, eq_top_iff, ← SetLike.coe_subset_coe] at hu
  obtain ⟨s, hs⟩ := IsCompact.elim_finite_subcover isCompact_univ _ (fun i ↦ (u i).2)
    (by simpa using hu)
  use s
  simpa [IsOpenCover, eq_top_iff, ← SetLike.coe_subset_coe, Set.iUnion_subtype] using hs

Goal state after:
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 : IsEmbedding f
⊢ (∃ s', IsLocallyClosed s' ∧ f '' f ⁻¹' s' = f '' s) ↔ ∃ s', IsLocallyClosed s' ∧ s' ∩ range f = f '' s

Tactic:
image_preimage_eq_inter_range

Goal state after:
Module: Mathlib.Topology.LocallyClosed

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsInducing f
hf' : IsLocallyClosed (range f)
t : Set Y
ht : IsLocallyClosed t
hs : IsLocallyClosed (f ⁻¹' t)
⊢ IsLocallyClosed (f '' f ⁻¹' t)

Tactic:
image_preimage_eq_inter_range

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsInducing f
hf' : IsLocallyClosed (range f)
t : Set Y
ht : IsLocallyClosed t
hs : IsLocallyClosed (f ⁻¹' t)
⊢ IsLocallyClosed (t ∩ range f)
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
⊢ IsEmbedding f ∧ Function.Surjective f ↔
    ∀ (i : ι), IsEmbedding ((U i).carrier.restrictPreimage f) ∧ Function.Surjective ((U i).carrier.restrictPreimage f)

Tactic:
forall_and,

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
⊢ IsEmbedding f ∧ Function.Surjective f ↔
    (∀ (x : ι), IsEmbedding ((U x).carrier.restrictPreimage f)) ∧
      ∀ (x : ι), Function.Surjective ((U x).carrier.restrictPreimage f)
Module: Mathlib.Order.BooleanSubalgebra

Goal state before:
pp: case h
α : Type u_2
inst✝ : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
a : α
t✝¹ : Finset (↑s × ↑s)
x✝⁵ : ↑s × ↑s
t✝ : Finset (↑s × ↑s)
x✝⁴ : ∃ t, (t✝.sup fun x ↦ ↑x.1 \ ↑x.2)ᶜ = t.sup fun x ↦ ↑x.1 \ ↑x.2
x y : ↑s
x✝³ : (x, y) ∉ t✝
tc✝ : Finset (↑s × ↑s)
eq✝ : (t✝.sup fun x ↦ ↑x.1 \ ↑x.2)ᶜ = tc✝.sup fun x ↦ ↑x.1 \ ↑x.2
x✝² : ↑s × ↑s
tc : Finset (↑s × ↑s)
x✝¹ : ∃ t, ((↑x \ ↑y)ᶜ ⊓ tc.sup fun x ↦ ↑x.1 \ ↑x.2) = t.sup fun x ↦ ↑x.1 \ ↑x.2
z w : ↑s
x✝ : (z, w) ∉ tc
t : Finset (↑s × ↑s)
eq : ((↑x \ ↑y)ᶜ ⊓ tc.sup fun x ↦ ↑x.1 \ ↑x.2) = t.sup fun x ↦ ↑x.1 \ ↑x.2
⊢ ((↑x \ ↑y)ᶜ ⊓ ↑z \ ↑w ⊔ t.sup fun x ↦ ↑x.1 \ ↑x.2) =
    ({(z, ⟨↑x ⊔ ↑w, ⋯⟩), (⟨↑y ⊓ ↑z, ⋯⟩, w)} ∪ t).sup fun x ↦ ↑x.1 \ ↑x.2

Tactic:
Finset.sup_union,

Goal state after:
case h
α : Type u_2
inst✝ : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
a : α
t✝¹ : Finset (↑s × ↑s)
x✝⁵ : ↑s × ↑s
t✝ : Finset (↑s × ↑s)
x✝⁴ : ∃ t, (t✝.sup fun x ↦ ↑x.1 \ ↑x.2)ᶜ = t.sup fun x ↦ ↑x.1 \ ↑x.2
x y : ↑s
x✝³ : (x, y) ∉ t✝
tc✝ : Finset (↑s × ↑s)
eq✝ : (t✝.sup fun x ↦ ↑x.1 \ ↑x.2)ᶜ = tc✝.sup fun x ↦ ↑x.1 \ ↑x.2
x✝² : ↑s × ↑s
tc : Finset (↑s × ↑s)
x✝¹ : ∃ t, ((↑x \ ↑y)ᶜ ⊓ tc.sup fun x ↦ ↑x.1 \ ↑x.2) = t.sup fun x ↦ ↑x.1 \ ↑x.2
z w : ↑s
x✝ : (z, w) ∉ tc
t : Finset (↑s × ↑s)
eq : ((↑x \ ↑y)ᶜ ⊓ tc.sup fun x ↦ ↑x.1 \ ↑x.2) = t.sup fun x ↦ ↑x.1 \ ↑x.2
⊢ ((↑x \ ↑y)ᶜ ⊓ ↑z \ ↑w ⊔ t.sup fun x ↦ ↑x.1 \ ↑x.2) =
    ({(z, ⟨↑x ⊔ ↑w, ⋯⟩), (⟨↑y ⊓ ↑z, ⋯⟩, w)}.sup fun x ↦ ↑x.1 \ ↑x.2) ⊔ t.sup fun x ↦ ↑x.1 \ ↑x.2
Module: Mathlib.Order.BooleanSubalgebra

Goal state before:
pp: case h
α : Type u_2
inst✝ : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
a : α
t✝¹ : Finset (↑s × ↑s)
x✝⁵ : ↑s × ↑s
t✝ : Finset (↑s × ↑s)
x✝⁴ : ∃ t, (t✝.sup fun x ↦ ↑x.1 \ ↑x.2)ᶜ = t.sup fun x ↦ ↑x.1 \ ↑x.2
x y : ↑s
x✝³ : (x, y) ∉ t✝
tc✝ : Finset (↑s × ↑s)
eq✝ : (t✝.sup fun x ↦ ↑x.1 \ ↑x.2)ᶜ = tc✝.sup fun x ↦ ↑x.1 \ ↑x.2
x✝² : ↑s × ↑s
tc : Finset (↑s × ↑s)
x✝¹ : ∃ t, ((↑x \ ↑y)ᶜ ⊓ tc.sup fun x ↦ ↑x.1 \ ↑x.2) = t.sup fun x ↦ ↑x.1 \ ↑x.2
z w : ↑s
x✝ : (z, w) ∉ tc
t : Finset (↑s × ↑s)
eq : ((↑x \ ↑y)ᶜ ⊓ tc.sup fun x ↦ ↑x.1 \ ↑x.2) = t.sup fun x ↦ ↑x.1 \ ↑x.2
⊢ ((↑x \ ↑y)ᶜ ⊓ ↑z \ ↑w ⊔ t.sup fun x ↦ ↑x.1 \ ↑x.2) =
    (↑z \ (↑x ⊔ ↑w) ⊔ {(⟨↑y ⊓ ↑z, ⋯⟩, w)}.sup fun x ↦ ↑x.1 \ ↑x.2) ⊔ t.sup fun x ↦ ↑x.1 \ ↑x.2

Tactic:
Finset.sup_singleton,

Goal state after:
case h
α : Type u_2
inst✝ : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
a : α
t✝¹ : Finset (↑s × ↑s)
x✝⁵ : ↑s × ↑s
t✝ : Finset (↑s × ↑s)
x✝⁴ : ∃ t, (t✝.sup fun x ↦ ↑x.1 \ ↑x.2)ᶜ = t.sup fun x ↦ ↑x.1 \ ↑x.2
x y : ↑s
x✝³ : (x, y) ∉ t✝
tc✝ : Finset (↑s × ↑s)
eq✝ : (t✝.sup fun x ↦ ↑x.1 \ ↑x.2)ᶜ = tc✝.sup fun x ↦ ↑x.1 \ ↑x.2
x✝² : ↑s × ↑s
tc : Finset (↑s × ↑s)
x✝¹ : ∃ t, ((↑x \ ↑y)ᶜ ⊓ tc.sup fun x ↦ ↑x.1 \ ↑x.2) = t.sup fun x ↦ ↑x.1 \ ↑x.2
z w : ↑s
x✝ : (z, w) ∉ tc
t : Finset (↑s × ↑s)
eq : ((↑x \ ↑y)ᶜ ⊓ tc.sup fun x ↦ ↑x.1 \ ↑x.2) = t.sup fun x ↦ ↑x.1 \ ↑x.2
⊢ ((↑x \ ↑y)ᶜ ⊓ ↑z \ ↑w ⊔ t.sup fun x ↦ ↑x.1 \ ↑x.2) = ↑z \ (↑x ⊔ ↑w) ⊔ (↑y ⊓ ↑z) \ ↑w ⊔ t.sup fun x ↦ ↑x.1 \ ↑x.2
Module: Mathlib.Topology.Sets.Closeds

Goal state before:
pp: α : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
s : Opens α
⊢ IsAtom ((Closeds.complOrderIso α) s.compl) ↔ ∃ x, s.compl.compl = {x}.compl

Tactic:
simp only [(Closeds.complOrderIso α).isAtom_iff, Closeds.isAtom_iff,
    Closeds.compl_bijective.injective.eq_iff]

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
U V : Set α
hU : U ⊆ s
hU' : IsOpen[inst✝] U
hU'' : IsCompact U
hV : V ⊆ s
hV' : IsOpen[inst✝] V
hV'' : IsCompact V
⊢ IsCompact (U ∩ V)

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

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : Continuous f
h : Function.Injective (Compacts.map f hf)
⊢ Function.Injective fun x ↦ {f x}

Tactic:
← map_singleton hf

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : Continuous f
h : Function.Injective (Compacts.map f hf)
⊢ Function.Injective fun x ↦ Compacts.map f hf {x}
Module: Mathlib.Order.Ideal

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

Tactic:
hS₁

Goal state after:
P : Type u_1
inst✝¹ : LE P
inst✝ : OrderTop P
S : Set (Ideal P)
hS₁ : IsChain (fun x1 x2 ↦ x1 ≤ x2) S
⊢ S.Nonempty → ⊤ ∉ S → ∃ x, x ≠ ⊤ ∧ x ∈ upperBounds S
Module: Mathlib.Topology.Sets.Compacts

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
⊢ Nonempty (NonemptyCompacts α) ↔ Nonempty α

Tactic:
by
  simp_rw [← not_isEmpty_iff, isEmpty_iff]

Goal state after:
Module: Mathlib.Topology.Sober

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : QuasiSober α
inst✝ : T0Space α
s : TopologicalSpace.IrreducibleCloseds α
⊢ (fun x ↦ { carrier := closure {x}, isIrreducible' := ⋯, isClosed' := ⋯ }) ((fun s ↦ ⋯.genericPoint) s) = s

Tactic:
by
    refine TopologicalSpace.IrreducibleCloseds.ext ?_
    simp only [IsIrreducible.genericPoint_closure_eq, TopologicalSpace.IrreducibleCloseds.coe_mk,
      closure_eq_iff_isClosed.mpr s.3]
    rfl

Goal state after:
Module: Mathlib.Topology.Sober

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
inst✝ : QuasiSober β
x : β
T : Set β
hT : IsClosed[inst✝¹] T
hS : IsIrreducible (f ⁻¹' T)
hS' : IsClosed[inst✝²] (f ⁻¹' T)
hS'' : IsIrreducible (f '' f ⁻¹' T)
hx : IsGenericPoint x (closure[inst✝¹] (f '' f ⁻¹' T))
⊢ ∃ x, IsGenericPoint x (f ⁻¹' T)

Tactic:
image_preimage_eq_inter_range

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
inst✝ : QuasiSober β
x : β
T : Set β
hT : IsClosed[inst✝¹] T
hS : IsIrreducible (f ⁻¹' T)
hS' : IsClosed[inst✝²] (f ⁻¹' T)
hS'' : IsIrreducible (T ∩ range f)
hx : IsGenericPoint x (closure[inst✝¹] (T ∩ range f))
⊢ ∃ x, IsGenericPoint x (f ⁻¹' T)
Module: Mathlib.Topology.Sober

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

Tactic:
exact closure_mono inter_subset_left hx.mem

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

Goal state before:
pp: case cons
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.HasGoingDown R S
l : RelSeries {(a, b) | a < b}
q : PrimeSpectrum R
lt : (q, l.head) ∈ {(a, b) | a < b}
ih :
  ∀ (P : Ideal S) [inst : P.IsPrime] [lo : P.LiesOver l.last.asIdeal],
    ∃ L,
      L.length = l.length ∧
        RelSeries.last L = { asIdeal := P, isPrime := ⋯ } ∧
          List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.toList L) = l.toList
P : Ideal S
inst✝ : P.IsPrime
lo : P.LiesOver (l.cons q lt).last.asIdeal
⊢ ∃ L,
    L.length = (l.cons q lt).length ∧
      RelSeries.last L = { asIdeal := P, isPrime := ⋯ } ∧
        List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.toList L) = (l.cons q lt).toList

Tactic:
| cons l q lt ih =>

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✝
R : Type u_3
S : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.Flat R S
⊢ ∀ (P : Ideal S) [inst : P.IsPrime],
    Function.Surjective (PrimeSpectrum.comap (Localization.localRingHom (Ideal.under R P) P (algebraMap R S) ⋯))

Tactic:
intro P

Goal state after:
R✝ : Type u_1
S✝ : Type u_2
inst✝⁶ : CommRing R✝
inst✝⁵ : CommRing S✝
inst✝⁴ : Algebra R✝ S✝
R : Type u_3
S : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.Flat R S
P : Ideal S
⊢ ∀ [inst : P.IsPrime],
    Function.Surjective (PrimeSpectrum.comap (Localization.localRingHom (Ideal.under R P) P (algebraMap R S) ⋯))
Module: Mathlib.RingTheory.RingHom.Flat

Goal state before:
pp: R S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
h :
  ∀ (J : Ideal S) (x : J.IsPrime),
    (fun {R S} [CommRing R] [CommRing S] ↦ Flat) (Localization.localRingHom (Ideal.comap f J) J f ⋯)
algInst✝ : Algebra R S := ⋯
⊢ ∀ (P : Ideal S) [inst : P.IsMaximal], Module.Flat R (Localization.AtPrime P)

Tactic:
intro P

Goal state after:
R S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
h :
  ∀ (J : Ideal S) (x : J.IsPrime),
    (fun {R S} [CommRing R] [CommRing S] ↦ Flat) (Localization.localRingHom (Ideal.comap f J) J f ⋯)
algInst✝ : Algebra R S := f.toAlgebra
P : Ideal S
⊢ ∀ [inst : P.IsMaximal], Module.Flat R (Localization.AtPrime P)
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: case neg
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
le : ¬b.factorization p ≤ a.factorization p
⊢ 1 ∣ p ^ a.factorization p

Tactic:
apply one_dvd

Goal state after:
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: case pos
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
le : b.factorization p ≤ a.factorization p
⊢ 1 ∣ p ^ b.factorization p

Tactic:
apply one_dvd

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
⊢ IrreducibleSpace (PrimeSpectrum R) ↔ (nilradical R).IsPrime

Tactic:
by
  simp [irreducibleSpace_def, isIrreducible_iff_vanishingIdeal_isPrime]

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case hfin
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (exponent G).factorization.support
he : 0 < exponent G
g : G
hg : g ^ (exponent G / p) ≠ 1
k : ℕ
hk : exponent G = p ^ (exponent G).factorization p * k
t : ℕ
ht : (exponent G).factorization p = t.succ
⊢ (g ^ k) ^ p ^ (t + 1) = 1

Tactic:
· rw [← Nat.succ_eq_add_one, ← ht, ← pow_mul, mul_comm, ← hk]
    exact pow_exponent_eq_one g

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
⊢ (∀ (a : PrimeSpectrum R), x ≤ a → a = x) ↔ IsMax x

Tactic:
exact ⟨fun H a h ↦ (H a h).le, fun H a h ↦ le_antisymm (H h) h⟩

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range orderOf).Nonempty
⊢ (Set.range orderOf).Finite

Tactic:
rwa [← exponent_ne_zero_iff_range_orderOf_finite hG.orderOf_pos]

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Fact (Nat.Prime p)
⊢ (∀ (g : G), ∃ k, orderOf g ∣ p ^ k) ↔ ∀ (g : G), ∃ k, orderOf g = p ^ k

Tactic:
Nat.dvd_prime_pow Fact.out

Goal state after:
p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Fact (Nat.Prime p)
⊢ (∀ (g : G), ∃ k, ∃ k_1 ≤ k, orderOf g = p ^ k_1) ↔ ∀ (g : G), ∃ k, orderOf g = p ^ k
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite G
⊢ (∃ n, Nat.card G ∣ p ^ n) ↔ ∃ n, Nat.card G = p ^ n

Tactic:
Nat.dvd_prime_pow Fact.out

Goal state after:
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite G
⊢ (∃ n, ∃ k ≤ n, Nat.card G = p ^ k) ↔ ∃ n, Nat.card G = p ^ n
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : Fact (Nat.Prime p)
⊢ (∃ n, Monoid.exponent G ∣ p ^ n) ↔ ∃ n, Monoid.exponent G = p ^ n

Tactic:
Nat.dvd_prime_pow Fact.out

Goal state after:
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : Fact (Nat.Prime p)
⊢ (∃ n, ∃ k ≤ n, Monoid.exponent G = p ^ k) ↔ ∃ n, Monoid.exponent G = p ^ n
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
hG : IsPGroup p G
H : Type u_2
inst✝ : Group H
ϕ : G →* H
hϕ : Function.Surjective ⇑ϕ
⊢ IsPGroup p H

Tactic:
refine fun h => Exists.elim (hϕ h) fun g hg => Exists.imp (fun k hk => ?_) (hG g)
  rw [← hg, ← ϕ.map_pow, hk, ϕ.map_one]

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝¹ : CancelCommMonoid G
inst✝ : Fintype G
⊢ exponent G = iSup orderOf

Tactic:
exact exponent_eq_iSup_orderOf orderOf_pos

Goal state after:
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
hf : f.IsIntegral
⊢ IsClosedMap (comap f)

Tactic:
by
  refine fun s hs ↦ isClosed_image_of_stableUnderSpecialization _ _ hs ?_
  rintro _ y e ⟨x, hx, rfl⟩
  algebraize [f]
  obtain ⟨q, hq₁, hq₂, hq₃⟩ := Ideal.exists_ideal_over_prime_of_isIntegral y.asIdeal x.asIdeal
    ((le_iff_specializes _ _).mpr e)
  refine ⟨⟨q, hq₂⟩, ((le_iff_specializes _ ⟨q, hq₂⟩).mp hq₁).mem_closed hs hx,
    PrimeSpectrum.ext hq₃⟩

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P Q : Sylow p G
⊢ ↥↑P ≃* ↥↑Q

Tactic:
by
  rw [← Classical.choose_spec (exists_smul_eq G P Q)]
  exact P.equivSMul (Classical.choose (exists_smul_eq G P Q))

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

Goal state before:
pp: A : Type u_4
inst✝³ : AddCommGroup A
inst✝² : LinearOrder A
inst✝¹ : IsOrderedAddMonoid A
inst✝ : Nontrivial A
g : A
hs : Function.Surjective fun x ↦ x • g
h_ne : g ≠ 0
⊢ Nonempty (A ≃+o ℤ)

Tactic:
wlog hg' : 0 < g

Goal state after:
case inr
A : Type u_4
inst✝³ : AddCommGroup A
inst✝² : LinearOrder A
inst✝¹ : IsOrderedAddMonoid A
inst✝ : Nontrivial A
g : A
hs : Function.Surjective fun x ↦ x • g
h_ne : g ≠ 0
this :
  ∀ {A : Type u_4} [inst : AddCommGroup A] [inst_1 : LinearOrder A] [IsOrderedAddMonoid A] [Nontrivial A] (g : A),
    (Function.Surjective fun x ↦ x • g) → g ≠ 0 → 0 < g → Nonempty (A ≃+o ℤ)
hg' : ¬0 < g
⊢ Nonempty (A ≃+o ℤ)

A : Type u_4
inst✝³ : AddCommGroup A
inst✝² : LinearOrder A
inst✝¹ : IsOrderedAddMonoid A
inst✝ : Nontrivial A
g : A
hs : Function.Surjective fun x ↦ x • g
h_ne : g ≠ 0
hg' : 0 < g
⊢ Nonempty (A ≃+o ℤ)
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
inst✝² : Finite G
G' : Type u_2
inst✝¹ : Group G'
f : G →* G'
hf : Function.Surjective ⇑f
p : ℕ
inst✝ : Fact (Nat.Prime p)
this : Finite G'
⊢ Function.Surjective (mapSurjective hf)

Tactic:
intro P

Goal state after:
G : Type u_1
inst✝³ : Group G
inst✝² : Finite G
G' : Type u_2
inst✝¹ : Group G'
f : G →* G'
hf : Function.Surjective ⇑f
p : ℕ
inst✝ : Fact (Nat.Prime p)
this : Finite G'
P : Sylow p G'
⊢ ∃ a, mapSurjective hf a = P
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: case inl
M : Type u_4
N : Type u_5
inst✝³ : CommGroup M
inst✝² : Group N
f : M →* N
h : (Nat.card ↥f.ker).Coprime (Nat.card ↥f.range)
inst✝¹ : IsCyclic ↥f.ker
inst✝ : IsCyclic ↥f.range
h✝ : Infinite ↥f.ker
⊢ IsCyclic M

Tactic:
Nat.card_eq_zero_of_infinite,

Goal state after:
case inl
M : Type u_4
N : Type u_5
inst✝³ : CommGroup M
inst✝² : Group N
f : M →* N
h : Nat.Coprime 0 (Nat.card ↥f.range)
inst✝¹ : IsCyclic ↥f.ker
inst✝ : IsCyclic ↥f.range
h✝ : Infinite ↥f.ker
⊢ IsCyclic M