mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic

Goal state before:
pp: case insert
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s✝ : Set A
a : A
s : Set A
a✝ : a ∉ s
hs✝ : s.Finite
ih : (∀ x ∈ s, IsIntegral R x) → (Subalgebra.toSubmodule (Algebra.adjoin R s)).FG
his : ∀ x ∈ insert a s, IsIntegral R x
⊢ (Subalgebra.toSubmodule (Algebra.adjoin R s) * Subalgebra.toSubmodule R[a]).FG

Tactic:
exact FG.mul
      (ih fun i hi => his i <| Set.mem_insert_of_mem a hi)
      (his a <| Set.mem_insert a s).fg_adjoin_singleton

Goal state after:
Module: Mathlib.Data.Nat.Choose.Cast

Goal state before:
pp: K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : NeZero 2
a : ℕ
⊢ ↑(a.choose 2) = ↑(a.choose 2) * ↑2 / 2

Tactic:
cast_two,

Goal state after:
K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : NeZero 2
a : ℕ
⊢ ↑(a.choose 2) = ↑(a.choose 2) * 2 / 2
Module: Mathlib.Algebra.Polynomial.Lifts

Goal state before:
pp: case inr
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
hlifts : p ∈ lifts f
hp : p.Monic
hR : Nontrivial S
p' : R[X]
h₁ : map f p' = p
h₂ : p'.degree = p.degree
h₃ : p'.Monic
⊢ ∃ q, map f q = p ∧ q.natDegree = p.natDegree ∧ q.Monic

Tactic:
exact ⟨p', h₁, natDegree_eq_of_degree_eq h₂, h₃⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
A : Matrix n n R
h : IsUnit A
this : Invertible A
⊢ C A⁻¹.det * (C.mapMatrix A * (scalar n) X - C.mapMatrix A * C.mapMatrix A⁻¹).det =
    C A⁻¹.det * (C.mapMatrix A * (scalar n) X - 1).det

Tactic:
← map_mul

Goal state after:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
A : Matrix n n R
h : IsUnit A
this : Invertible A
⊢ C A⁻¹.det * (C.mapMatrix A * (scalar n) X - C.mapMatrix (A * A⁻¹)).det =
    C A⁻¹.det * (C.mapMatrix A * (scalar n) X - 1).det
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
s : Finset n
e : ↥s ⊕ { a // a ∉ s } ≃ n := Equiv.sumCompl fun x ↦ x ∈ s
A : Matrix n n R := of (s.piecewise M 1)
h_blocks :
  A.submatrix ⇑e ⇑e = fromBlocks (M.submatrix Subtype.val Subtype.val) (M.submatrix Subtype.val Subtype.val) 0 1
⊢ (fromBlocks (M.submatrix Subtype.val Subtype.val) (M.submatrix Subtype.val Subtype.val) 0 1).det =
    (M.submatrix Subtype.val Subtype.val).det

Tactic:
Matrix.det_fromBlocks_zero₂₁,

Goal state after:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
s : Finset n
e : ↥s ⊕ { a // a ∉ s } ≃ n := Equiv.sumCompl fun x ↦ x ∈ s
A : Matrix n n R := of (s.piecewise M 1)
h_blocks :
  A.submatrix ⇑e ⇑e = fromBlocks (M.submatrix Subtype.val Subtype.val) (M.submatrix Subtype.val Subtype.val) 0 1
⊢ (M.submatrix Subtype.val Subtype.val).det * det 1 = (M.submatrix Subtype.val Subtype.val).det
Module: Mathlib.Algebra.Polynomial.HasseDeriv

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ ((hasseDeriv n) p).natDegree ≤ p.natDegree - n

Tactic:
by
  classical
    rw [hasseDeriv_apply, sum_def]
    refine (natDegree_sum_le _ _).trans ?_
    simp_rw [Function.comp, natDegree_monomial]
    rw [Finset.fold_ite, Finset.fold_const]
    · simp only [ite_self, max_eq_right, zero_le, Finset.fold_max_le, true_and, and_imp,
        tsub_le_iff_right, mem_support_iff, Ne, Finset.mem_filter]
      intro x hx hx'
      have hxp : x ≤ p.natDegree := le_natDegree_of_ne_zero hx
      grind
    · simp

Goal state after:
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
n : ℕ
⊢ (∑ x ∈ Finset.antidiagonal n, p.coeff x.1 * q.coeff x.2) * r ^ (p.natDegree + q.natDegree - n) =
    (p.scaleRoots r * q.scaleRoots r).coeff n

Tactic:
rw [coeff_mul, Finset.sum_mul]

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
n : ℕ
⊢ ∑ i ∈ Finset.antidiagonal n, p.coeff i.1 * q.coeff i.2 * r ^ (p.natDegree + q.natDegree - n) =
    ∑ x ∈ Finset.antidiagonal n, (p.scaleRoots r).coeff x.1 * (q.scaleRoots r).coeff x.2
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : CommSemiring R
p q : R[X]
r : R
inst✝ : NoZeroDivisors R
hp : ¬p = 0
hq : q = 0
⊢ (p * q).scaleRoots r = p.scaleRoots r * q.scaleRoots r

Tactic:
simp [hq]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.IntegralNormalization

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
A : Type u_1
inst✝ : Semiring A
f : R →+* A
p : R[X]
H : f p.leadingCoeff ≠ 0
⊢ (map f p).integralNormalization = map f p.integralNormalization

Tactic:
by
  ext i
  simp [integralNormalization_coeff, degree_map_eq_of_leadingCoeff_ne_zero _ H, apply_ite f,
    leadingCoeff_map_of_leadingCoeff_ne_zero _ H, natDegree_map_eq_iff.mpr (.inl H)]

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal S
⊢ (Ideal.quotientMap I f ⋯).IsIntegral ↔ ((Ideal.Quotient.mk I).comp f).IsIntegral

Tactic:
let g := Ideal.Quotient.mk (I.comap f)
  -- Porting note: added type ascription
  have : (Ideal.quotientMap I f le_rfl).comp g = (Ideal.Quotient.mk I).comp f :=
    Ideal.quotientMap_comp_mk le_rfl
  refine ⟨fun h => ?_, fun h => RingHom.IsIntegral.tower_top g _ (this ▸ h)⟩
  refine this ▸ RingHom.IsIntegral.trans g (Ideal.quotientMap I f le_rfl) ?_ h
  exact g.isIntegral_of_surjective Ideal.Quotient.mk_surjective

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
inst✝² : FaithfullyFlat R M
N : Type u_1
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ ∀ [h : Subsingleton (N ⊗[R] M)], Subsingleton N

Tactic:
change _ → _

Goal state after:
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : FaithfullyFlat R M
N : Type u_1
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ Subsingleton (N ⊗[R] M) → Subsingleton N
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: S : Type u_2
inst✝³ : CommRing S
K : Type u_4
inst✝² : CommRing K
inst✝¹ : Algebra S K
inst✝ : IsIntegralClosure S ℤ K
x : K
hx : IsAlgebraic ℤ x
⊢ ∃ m s, m ≠ 0 ∧ m • x = (algebraMap S K) s

Tactic:
obtain ⟨a, s, ha, h⟩ := hx.exists_smul_eq S

Goal state after:
S : Type u_2
inst✝³ : CommRing S
K : Type u_4
inst✝² : CommRing K
inst✝¹ : Algebra S K
inst✝ : IsIntegralClosure S ℤ K
x : K
hx : IsAlgebraic ℤ x
a : ℤ
s : S
ha : a ≠ 0
h : a • x = (algebraMap S K) s
⊢ ∃ m s, m ≠ 0 ∧ m • x = (algebraMap S K) s
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: case neg
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Ring A
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : NoZeroDivisors S
int : Algebra.IsIntegral R S
a : A
h : IsAlgebraic S a
hRS : ¬Function.Injective ⇑(algebraMap R S)
⊢ IsAlgebraic R a

Tactic:
exact (Algebra.isAlgebraic_of_not_injective
    fun h ↦ hRS <| .of_comp (IsScalarTower.algebraMap_eq R S A ▸ h)).1 _

Goal state after:
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: case neg
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Ring A
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : NoZeroDivisors S
inst✝ : Algebra.IsAlgebraic R S
a : A
h : IsAlgebraic S a
p : S[X]
hp : p ≠ 0
eval0 : (aeval a) p = 0
hRS : ¬Function.Injective ⇑(algebraMap R S)
⊢ IsAlgebraic R a

Tactic:
exact (Algebra.isAlgebraic_of_not_injective
    fun h ↦ hRS <| .of_comp (IsScalarTower.algebraMap_eq R S A ▸ h)).1 _

Goal state after:
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: case inl
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Ring A
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : NoZeroDivisors S
alg : Algebra.IsAlgebraic R S
a : A
h : IsIntegral S a
h✝ : Subsingleton A
this : Nontrivial R
⊢ IsAlgebraic R a

Tactic:
exact Subsingleton.elim a 0 ▸ isAlgebraic_zero

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

Goal state before:
pp: case mp
R : Type u_1
inst✝⁹ : CommRing R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
K : Type u_4
inst✝⁶ : Field K
inst✝⁵ : IsDomain R
inst✝⁴ : Algebra R K
inst✝³ : Algebra S K
inst✝² : Module.IsTorsionFree R K
inst✝¹ : IsFractionRing S K
inst✝ : IsScalarTower R S K
h : ∀ (x : S), IsAlgebraic R x
x : K
this✝¹ : Nontrivial S := MulActionWithZero.nontrivial S K
this✝ : Algebra (FractionRing R) K := FractionRing.liftAlgebra R K
this : IsScalarTower R (FractionRing R) K
⊢ IsAlgebraic R x

Tactic:
rw [IsFractionRing.isAlgebraic_iff R (FractionRing R) K, isAlgebraic_iff_isIntegral]

Goal state after:
case mp
R : Type u_1
inst✝⁹ : CommRing R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
K : Type u_4
inst✝⁶ : Field K
inst✝⁵ : IsDomain R
inst✝⁴ : Algebra R K
inst✝³ : Algebra S K
inst✝² : Module.IsTorsionFree R K
inst✝¹ : IsFractionRing S K
inst✝ : IsScalarTower R S K
h : ∀ (x : S), IsAlgebraic R x
x : K
this✝¹ : Nontrivial S := MulActionWithZero.nontrivial S K
this✝ : Algebra (FractionRing R) K := FractionRing.liftAlgebra R K
this : IsScalarTower R (FractionRing R) K
⊢ IsIntegral (FractionRing R) x
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: R : Type u_1
inst✝¹⁴ : CommRing R
S : Type u_2
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
K : Type u_4
L : Type u_5
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra R K
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : Algebra.IsAlgebraic R S
inst✝³ : IsFractionRing S L
inst✝² : Algebra K L
inst✝¹ : IsScalarTower R S L
inst✝ : IsScalarTower R K L
a : S
b : Set S
inj : Function.Injective ⇑(algebraMap R L)
h : ↑(Ideal.span {a}) ⊆ ↑(Submodule.span R b)
y' : S
z' : ↥S⁰
hx : (algebraMap S L) a * mk' L y' z' ∈ ↑(Ideal.span {(algebraMap S L) a})
y : S
z : R
hz0 : z ≠ 0
yz_eq : z • y' = ↑z' * y
injRS : Function.Injective ⇑(algebraMap R S)
hz0' : (algebraMap R S) z ∈ S⁰
mk_yz_eq : mk' L y' z' = mk' L y ⟨(algebraMap R S) z, hz0'⟩
hy : (algebraMap S L) (a * y) ∈ Submodule.span K (⇑(algebraMap S L) '' b)
⊢ ((algebraMap R K) z)⁻¹ • ((algebraMap S L) a * (algebraMap S L) y) ∈ ↑(Submodule.span K (⇑(algebraMap S L) '' b))

Tactic:
← map_mul

Goal state after:
R : Type u_1
inst✝¹⁴ : CommRing R
S : Type u_2
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
K : Type u_4
L : Type u_5
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra R K
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : Algebra.IsAlgebraic R S
inst✝³ : IsFractionRing S L
inst✝² : Algebra K L
inst✝¹ : IsScalarTower R S L
inst✝ : IsScalarTower R K L
a : S
b : Set S
inj : Function.Injective ⇑(algebraMap R L)
h : ↑(Ideal.span {a}) ⊆ ↑(Submodule.span R b)
y' : S
z' : ↥S⁰
hx : (algebraMap S L) a * mk' L y' z' ∈ ↑(Ideal.span {(algebraMap S L) a})
y : S
z : R
hz0 : z ≠ 0
yz_eq : z • y' = ↑z' * y
injRS : Function.Injective ⇑(algebraMap R S)
hz0' : (algebraMap R S) z ∈ S⁰
mk_yz_eq : mk' L y' z' = mk' L y ⟨(algebraMap R S) z, hz0'⟩
hy : (algebraMap S L) (a * y) ∈ Submodule.span K (⇑(algebraMap S L) '' b)
⊢ ((algebraMap R K) z)⁻¹ • (algebraMap S L) (a * y) ∈ ↑(Submodule.span K (⇑(algebraMap S L) '' b))
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : R
s : ↥M
⊢ ∃ r s_1, IsUnit ((algebraMap R S) s_1) ∧ (algebraMap R S) s_1 * IsLocalization.mk' S x s = (algebraMap R S) r

Tactic:
exact ⟨x, s, IsLocalization.map_units S s, IsLocalization.mk'_spec' S x s⟩

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

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

Tactic:
AlgEquiv.toLinearMap,

Goal state after:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Module.FaithfullyFlat A B
I : Ideal A
⊢ Function.Injective (⇑(↑A ↑↑(quotIdealMapEquivTensorQuot B I).symm) ∘ ⇑((TensorProduct.mk A B (A ⧸ I)) 1))
Module: Mathlib.Topology.Sets.Opens

Goal state before:
pp: case mpr.refine_1
α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
h : ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U' ∈ B, x ∈ U' ∧ U' ≤ U
⊢ ∀ u ∈ SetLike.coe '' B, IsOpen[inst✝] u

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
⊢ ∀ (a : α) (u : Set α), a ∈ u → IsOpen[inst✝] u → ∃ v ∈ SetLike.coe '' B, a ∈ v ∧ v ⊆ u

Tactic:
· rintro sU ⟨U, -, rfl⟩
      exact U.2

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
⊢ ∀ (a : α) (u : Set α), a ∈ u → IsOpen[inst✝] u → ∃ v ∈ SetLike.coe '' B, a ∈ v ∧ v ⊆ u
Module: Mathlib.Order.BooleanSubalgebra

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
f : BoundedLatticeHom α β
h : Surjective ⇑f
⊢ ↑(map f ⊤) = ↑⊤

Tactic:
simp [h.range_eq]

Goal state after:
Module: Mathlib.Order.BooleanSubalgebra

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

Tactic:
rw [Finset.sup_union]

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
hf : ∀ (i : ι), GeneralizingMap (f ∘ Subtype.val)
x : α
y : β
i : ι
hi : x ∈ U i
h : y ⤳ (f ∘ Subtype.val) ⟨x, hi⟩
⊢ ∃ a', (fun x1 x2 ↦ x1 ⤳ x2) a' x ∧ f a' = y

Tactic:
obtain ⟨a, ha, rfl⟩ := hf i h

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens α
hU : IsOpenCover U
hf : ∀ (i : ι), GeneralizingMap (f ∘ Subtype.val)
x : α
i : ι
hi : x ∈ U i
a : ↥(U i)
ha : a ⤳ ⟨x, hi⟩
h : (f ∘ Subtype.val) a ⤳ (f ∘ Subtype.val) ⟨x, hi⟩
⊢ ∃ a', (fun x1 x2 ↦ x1 ⤳ x2) a' x ∧ f a' = (f ∘ Subtype.val) a
Module: Mathlib.Topology.NoetherianSpace

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
S : Set (Set α)
hSf : S.Finite
hSc : ∀ t ∈ S, IsClosed[inst✝¹] t
hSi : ∀ t ∈ S, IsIrreducible t
hSU : Set.univ = ⋃₀ S
⊢ (irreducibleComponents α).Finite

Tactic:
refine hSf.subset fun s hs => ?_

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
S : Set (Set α)
hSf : S.Finite
hSc : ∀ t ∈ S, IsClosed[inst✝¹] t
hSi : ∀ t ∈ S, IsIrreducible t
hSU : Set.univ = ⋃₀ S
s : Set α
hs : s ∈ irreducibleComponents α
⊢ s ∈ S
Module: Mathlib.Topology.Sets.Compacts

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
K : Compacts α
U : Opens α
h : U ∈ K.openRcNhds
⊢ { carrier := closure[inst✝] ↑U, isCompact' := ⋯ } ∈ K.compactNhds

Tactic:
intro x
  have H : (U : Set α) ∈ 𝓝 (x : α) :=
    U.isOpen.mem_nhds <| Compacts.subset_of_mem_openRcNhds h (by simp)
  exact Filter.mem_of_superset H subset_closure

Goal state after:
Module: Mathlib.Topology.KrullDimension

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : QuasiSober Y
inst✝² : T0Space Y
inst✝¹ : QuasiSober X
inst✝ : T0Space X
x : X
f : X → Y
hf : IsOpenEmbedding f
⊢ ↑(irreducibleSetEquivPoints.symm (f x)) = ↑(map f ⋯ (irreducibleSetEquivPoints.symm x))

Tactic:
simp [closure_image_closure hf.continuous]

Goal state after:
Module: Mathlib.Topology.Sober

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
V W : Set α
inst✝ : QuasiSober ↑W
hV : IsClosed V
⊢ IsClosed (Subtype.val ⁻¹' (W ∩ V))

Tactic:
rw [Subtype.preimage_coe_self_inter W V]

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
V W : Set α
inst✝ : QuasiSober ↑W
hV : IsClosed V
⊢ IsClosed (Subtype.val ⁻¹' V)
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case mpr
R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsRadical
⊢ (∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I) → ∀ (x y : Ideal R), x ⊓ y ≤ I → x ≤ I ∨ y ≤ I

Tactic:
simp_rw [or_iff_not_imp_left, SetLike.not_le_iff_exists]
        rintro h s t h' ⟨x, hx, hx'⟩ y hy
        exact h (h' ⟨Ideal.mul_mem_right _ _ hx, Ideal.mul_mem_left _ _ hy⟩) hx'

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
r : R
x : PrimeSpectrum R
⊢ x ∈ ↑(basicOpen r) ↔ x ∈ (zeroLocus {r})ᶜ

Tactic:
by simp only [SetLike.mem_coe, mem_basicOpen, Set.mem_compl_iff, mem_zeroLocus,
    Set.singleton_subset_iff]

Goal state after:
Module: Mathlib.Data.ZMod.QuotientGroup

Goal state before:
pp: α : Type u_3
inst✝ : Group α
a : α
⊢ Nat.card ↥(zpowers a) = orderOf a

Tactic:
have := Nat.card_congr (MulAction.orbitZPowersEquiv a (1 : α))

Goal state after:
α : Type u_3
inst✝ : Group α
a : α
this : Nat.card ↑(MulAction.orbit (↥(zpowers a)) 1) = Nat.card (ZMod (Function.minimalPeriod (fun x ↦ a • x) 1))
⊢ Nat.card ↥(zpowers a) = orderOf a
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:
by
  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⟩
  choose f hf using this
  let e := Equiv.ofInjective f fun p q eq ↦ Set.singleton_injective (hf p ▸ eq ▸ hf q)
  have loc a : IsLocalization.AtPrime (Localization.Away a.1) (e.symm a).1 :=
    (isLocalization_away_iff_atPrime_of_basicOpen_eq_singleton <| hf _).mp <| by
      simp_rw [e, Equiv.apply_ofInjective_symm]; infer_instance
  let algE a := IsLocalization.algEquiv (e.symm a).1.primeCompl
    (Localization.AtPrime (e.symm a).1) (Localization.Away a.1)
  have span_eq : Ideal.span (Set.range f) = ⊤ := iSup_basicOpen_eq_top_iff.mp <| top_unique
    fun p _ ↦ TopologicalSpace.Opens.mem_iSup.mpr ⟨p, (hf p).ge rfl⟩
  replace hf a : (basicOpen a.1 : Set _) = {e.symm a} := by
    simp_rw [e, ← hf, Equiv.apply_ofInjective_symm]
  obtain ⟨r, eq, -⟩ := Localization.existsUnique_algebraMap_eq_of_span_eq_top _ span_eq
    (fun a ↦ algE a (x _)) fun a b ↦ by
      obtain rfl | ne := eq_or_ne a b; · rfl
      have nil : IsNilpotent (a * b : R) := (basicOpen_eq_bot_iff _).mp <| 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))
      apply (IsLocalization.subsingleton (M := .powers (a * b : R)) nil).elim
  refine ⟨r, funext fun I ↦ ?_⟩
  have := eq (e I)
  rwa [← AlgEquiv.symm_apply_eq, AlgEquiv.commutes, e.symm_apply_apply] at this

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: case neg.refine_1
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
h2 : ¬H.index = 0
this : Finite G
h3 : (Nat.card ↥H).Coprime (Nat.card ↥P) ∨ H.index.Coprime (Nat.card ↥P)
h4 : H.index.Coprime (Nat.card ↥P)
⊢ P ≤ H

Tactic:
← Subgroup.relIndex_eq_one

Goal state after:
case neg.refine_1
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
h2 : ¬H.index = 0
this : Finite G
h3 : (Nat.card ↥H).Coprime (Nat.card ↥P) ∨ H.index.Coprime (Nat.card ↥P)
h4 : H.index.Coprime (Nat.card ↥P)
⊢ H.relIndex P = 1
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
⊢ a ^ (↑(orderOf a) * i) = 1

Tactic:
zpow_mul,

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
⊢ (a ^ ↑(orderOf a)) ^ i = 1
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝ : Group G
P Q : Sylow p G
h : ↑P = ↑Q
⊢ P = Q

Tactic:
by cases P; cases Q; congr

Goal state after:
Module: Mathlib.Algebra.Module.ZMod

Goal state before:
pp: p : ℕ
G : Type u_5
inst✝¹ : AddCommGroup G
hp : Nat.Prime p
inst✝ : Module (ZMod p) G
H : Submodule (ZMod p) G
k : ℕ
hk : k ≤ Nat.card ↥H
h'k : k ≠ 0
⊢ ∃ H', Nat.card ↥H' ≤ k ∧ k < p * Nat.card ↥H' ∧ H' ≤ H

Tactic:
obtain ⟨H'm, H'mHm, H'mk, kH'm⟩ := Sylow.exists_subgroup_le_card_le
    (H := AddSubgroup.toSubgroup ((AddSubgroup.toZModSubmodule _).symm H)) hp
      isPGroup_multiplicative hk h'k

Goal state after:
p : ℕ
G : Type u_5
inst✝¹ : AddCommGroup G
hp : Nat.Prime p
inst✝ : Module (ZMod p) G
H : Submodule (ZMod p) G
k : ℕ
hk : k ≤ Nat.card ↥H
h'k : k ≠ 0
H'm : Subgroup (Multiplicative G)
H'mHm : H'm ≤ AddSubgroup.toSubgroup ((AddSubgroup.toZModSubmodule p).symm H)
H'mk : Nat.card ↥H'm ≤ k
kH'm : k < p * Nat.card ↥H'm
⊢ ∃ H', Nat.card ↥H' ≤ k ∧ k < p * Nat.card ↥H' ∧ H' ≤ H
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
⊢ {x | Minimal (fun x ↦ ∃ x₀, (IsClosed x₀ ∧ IsIrreducible x₀) ∧ vanishingIdeal x₀ = x) x} =
    {x | Minimal (Membership.mem {y | y.IsPrime}) x}

Tactic:
← vanishingIdeal_isClosed_isIrreducible

Goal state after:
R : Type u
inst✝ : CommSemiring R
⊢ {x | Minimal (fun x ↦ ∃ x₀, (IsClosed x₀ ∧ IsIrreducible x₀) ∧ vanishingIdeal x₀ = x) x} =
    {x | Minimal (Membership.mem (vanishingIdeal '' {s | IsClosed s ∧ IsIrreducible s})) x}
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
⊢ zeroLocus ∘ SetLike.coe '' minimalPrimes R = irreducibleComponents (PrimeSpectrum R)

Tactic:
← vanishingIdeal_irreducibleComponents,

Goal state after:
R : Type u
inst✝ : CommSemiring R
⊢ zeroLocus ∘ SetLike.coe '' vanishingIdeal '' irreducibleComponents (PrimeSpectrum R) =
    irreducibleComponents (PrimeSpectrum R)
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case mp
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ vanishingIdeal s ∈ minimalPrimes R → closure s ∈ irreducibleComponents (PrimeSpectrum R)

Tactic:
← zeroLocus_minimalPrimes,

Goal state after:
case mp
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ vanishingIdeal s ∈ minimalPrimes R → closure s ∈ zeroLocus ∘ SetLike.coe '' minimalPrimes R
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case mpr
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ closure s ∈ irreducibleComponents (PrimeSpectrum R) → vanishingIdeal s ∈ minimalPrimes R

Tactic:
← vanishingIdeal_irreducibleComponents,

Goal state after:
case mpr
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ closure s ∈ irreducibleComponents (PrimeSpectrum R) →
    vanishingIdeal s ∈ vanishingIdeal '' irreducibleComponents (PrimeSpectrum R)
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_2
inst✝ : AddGroup G
g : G
hg : ∀ (x : G), x ∈ zmultiples g
n : ℕ
hn : Nat.card G = n
i : ℤ
⊢ i • g + -((i - ↑n * (i / ↑n)) • g) = 0

Tactic:
← sub_zsmul,

Goal state after:
G : Type u_2
inst✝ : AddGroup G
g : G
hg : ∀ (x : G), x ∈ zmultiples g
n : ℕ
hn : Nat.card G = n
i : ℤ
⊢ (i - (i - ↑n * (i / ↑n))) • g = 0