mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: case inr
R : Type u_1
inst✝ : CommSemiring R
f g : R[X]
hf : f.Splits
hg✝ : g.natDegree ≤ 1
h : Invertible g.leadingCoeff
hg : g.natDegree = 1
m : Multiset R
hm : f = C f.leadingCoeff * (Multiset.map (fun x ↦ X + C x) m).prod
⊢ ((C f.leadingCoeff).comp g * (Multiset.map (fun x ↦ X + C x) m).prod.comp g).Splits

Tactic:
C_comp,

Goal state after:
case inr
R : Type u_1
inst✝ : CommSemiring R
f g : R[X]
hf : f.Splits
hg✝ : g.natDegree ≤ 1
h : Invertible g.leadingCoeff
hg : g.natDegree = 1
m : Multiset R
hm : f = C f.leadingCoeff * (Multiset.map (fun x ↦ X + C x) m).prod
⊢ (C f.leadingCoeff * (Multiset.map (fun x ↦ X + C x) m).prod.comp g).Splits
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: case inr
R : Type u_1
inst✝ : Ring R
f : R[X]
hf : f.Splits
a : R
⊢ (-X + (C a).comp (-X)).Splits

Tactic:
C_comp,

Goal state after:
case inr
R : Type u_1
inst✝ : Ring R
f : R[X]
hf : f.Splits
a : R
⊢ (-X + C a).Splits
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: R : Type u_1
inst✝ : Field R
f g : R[X]
hp : f.Splits
hp0 : f ≠ 0
hq : f.roots ≤ g.roots
⊢ C f.leadingCoeff * (Multiset.map (fun x ↦ X - C x) f.roots).prod ∣ g

Tactic:
C_mul_dvd (leadingCoeff_ne_zero.2 hp0)

Goal state after:
R : Type u_1
inst✝ : Field R
f g : R[X]
hp : f.Splits
hp0 : f ≠ 0
hq : f.roots ≤ g.roots
⊢ (Multiset.map (fun x ↦ X - C x) f.roots).prod ∣ g
Module: Mathlib.RingTheory.Ideal.GoingUp

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
I : Ideal S
r : S
r_non_zero_divisor : ∀ {x : S}, x * r = 0 → x = 0
hr : r ∈ I
p : R[X]
⊢ p ≠ 0 → eval₂ f r p = 0 → ∃ i, p.coeff i ≠ 0 ∧ p.coeff i ∈ comap f I

Tactic:
refine p.recOnHorner ?_ ?_ ?_
  · intro h
    contradiction
  · intro p a coeff_eq_zero a_ne_zero _ _ hp
    refine ⟨0, ?_, coeff_zero_mem_comap_of_root_mem hr hp⟩
    simp [coeff_eq_zero, a_ne_zero]
  · intro p p_nonzero ih _ hp
    rw [eval₂_mul, eval₂_X] at hp
    obtain ⟨i, hi, mem⟩ := ih p_nonzero (r_non_zero_divisor hp)
    refine ⟨i + 1, ?_, ?_⟩
    · simp [hi]
    · simpa [hi] using mem

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Algebra.IsIntegral R S
inst✝¹ : FaithfulSMul R S
P : Ideal R
inst✝ : P.IsMaximal
⊢ ∃ Q, Q.IsMaximal ∧ Q.LiesOver P

Tactic:
simp_rw [liesOver_iff, eq_comm (a := P)]

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Algebra.IsIntegral R S
inst✝¹ : FaithfulSMul R S
P : Ideal R
inst✝ : P.IsMaximal
⊢ ∃ Q, Q.IsMaximal ∧ under R Q = P
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: case pos.inr
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)
this : NoZeroDivisors R
s : S
hs : s ≠ 0
int_s : IsIntegral S (s • a)
h✝ : Nontrivial R
r : R
hr : r ≠ 0
w✝ : S
e : (algebraMap R S) r = s * w✝
⊢ IsIntegral R (w✝ • s • a)

Tactic:
exact isIntegral_trans _ (int_s.smul _)

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

Goal state before:
pp: case add
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)
complex : l12.range ≤ l23.ker
H : Type u_2 := ↥l23.ker ⧸ (Submodule.inclusion complex).range
e : H ⊗[R] M ≃ₗ[R]
  ↥l23.ker ⊗[R] M ⧸ (TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id).range :=
  quotientTensorEquiv M (Submodule.inclusion complex).range
x y : ↥l23.ker ⊗[R] M
hx : ∃ a, (TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id) a = x
hy : ∃ a, (TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id) a = y
⊢ ∃ a, (TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id) a = x + y

Tactic:
obtain ⟨x, rfl⟩ := hx

Goal state after:
case add
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)
complex : l12.range ≤ l23.ker
H : Type u_2 := ↥l23.ker ⧸ (Submodule.inclusion complex).range
e : H ⊗[R] M ≃ₗ[R]
  ↥l23.ker ⊗[R] M ⧸ (TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id).range :=
  quotientTensorEquiv M (Submodule.inclusion complex).range
y : ↥l23.ker ⊗[R] M
hy : ∃ a, (TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id) a = y
x : ↥(Submodule.inclusion complex).range ⊗[R] M
⊢ ∃ a,
    (TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id) a =
      (TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id) x + y
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: A : Type u_3
inst✝⁹ : CommRing A
L : Type u_5
inst✝⁸ : Field L
inst✝⁷ : Algebra A L
C : Type u_6
inst✝⁶ : CommRing C
inst✝⁵ : IsDomain C
inst✝⁴ : Algebra C L
inst✝³ : IsIntegralClosure C A L
inst✝² : Algebra A C
inst✝¹ : IsScalarTower A C L
inst✝ : Algebra.IsAlgebraic A L
inj : ∀ (x : A), (algebraMap A L) x = 0 → x = 0
z : L
x : A
hx : x ≠ 0
int : IsIntegral A (x • z)
h : (algebraMap A C) x = 0
⊢ (algebraMap A L) x = 0

Tactic:
rw [IsScalarTower.algebraMap_apply A C L, h, map_zero]

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

Goal state before:
pp: 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 S A
inst✝ : NoZeroDivisors S
s t : Set S
a : A
Rs : Subalgebra R S := adjoin R s
ha : IsAlgebraic (↥Rs) a
Rt : Subalgebra R S := adjoin R t
alg : ∀ x ∈ s \ t, IsAlgebraic (↥Rt) x
Rts : Subalgebra (↥Rt) S := adjoin (↥Rt) s
x✝ : Algebra ↥Rs ↥Rts := (Subalgebra.inclusion ⋯).toAlgebra
this : IsScalarTower (↥Rs) (↥Rts) A
⊢ IsAlgebraic (↥Rt) a

Tactic:
have : Algebra.IsAlgebraic Rt Rts := by
    have := ha.nontrivial
    have := Subtype.val_injective (p := (· ∈ Rs)).nontrivial
    have := (isDomain_iff_noZeroDivisors_and_nontrivial Rt).mpr ⟨inferInstance, inferInstance⟩
    rw [← Subalgebra.isAlgebraic_iff, isAlgebraic_adjoin_iff]
    intro x hs
    by_cases ht : x ∈ t
    · exact isAlgebraic_algebraMap (⟨x, subset_adjoin ht⟩ : Rt)
    exact alg _ ⟨hs, ht⟩

Goal state after:
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 S A
inst✝ : NoZeroDivisors S
s t : Set S
a : A
Rs : Subalgebra R S := adjoin R s
ha : IsAlgebraic (↥Rs) a
Rt : Subalgebra R S := adjoin R t
alg : ∀ x ∈ s \ t, IsAlgebraic (↥Rt) x
Rts : Subalgebra (↥Rt) S := adjoin (↥Rt) s
x✝ : Algebra ↥Rs ↥Rts := (Subalgebra.inclusion ⋯).toAlgebra
this✝ : IsScalarTower (↥Rs) (↥Rts) A
this : Algebra.IsAlgebraic ↥Rt ↥Rts
⊢ IsAlgebraic (↥Rt) a
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
S' : Type u_4
inst✝³ : CommRing S'
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Algebra R S'
f : S →ₐ[R] S'
Hf : f.SurjectiveOnStalks
this✝ : Algebra S S' := f.toAlgebra
this : IsScalarTower R S S'
⊢ (Algebra.TensorProduct.map (Algebra.ofId S S') (AlgHom.id R T)).toRingHom =
    ((↑(Algebra.TensorProduct.cancelBaseChange R S S S' T)).comp Algebra.TensorProduct.includeRight).toRingHom

pp: R : Type u_1
inst✝⁶ : CommRing R
S : Type u_2
inst✝⁵ : CommRing S
T : Type u_3
inst✝⁴ : CommRing T
S' : Type u_4
inst✝³ : CommRing S'
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Algebra R S'
f : S →ₐ[R] S'
Hf : f.SurjectiveOnStalks
this✝ : Algebra S S' := f.toAlgebra
this : IsScalarTower R S S'
⊢ ((↑(Algebra.TensorProduct.cancelBaseChange R S S S' T)).comp Algebra.TensorProduct.includeRight).SurjectiveOnStalks

Tactic:
· congr; ext; simp

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
S : Type u_2
inst✝⁵ : CommRing S
T : Type u_3
inst✝⁴ : CommRing T
S' : Type u_4
inst✝³ : CommRing S'
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Algebra R S'
f : S →ₐ[R] S'
Hf : f.SurjectiveOnStalks
this✝ : Algebra S S' := f.toAlgebra
this : IsScalarTower R S S'
⊢ ((↑(Algebra.TensorProduct.cancelBaseChange R S S S' T)).comp Algebra.TensorProduct.includeRight).SurjectiveOnStalks
Module: Mathlib.Algebra.Order.Ring.Idempotent

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

Tactic:
b.2.1

Goal state after:
case refine_1
R : Type u_1
inst✝ : CommSemiring R
a b : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
eq : (↑a).1 = (↑b).1
⊢ 0 = 0
Module: Mathlib.Algebra.Order.Ring.Idempotent

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

Tactic:
b.2.1

Goal state after:
case refine_1
R : Type u_1
inst✝ : CommSemiring R
a b : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
eq : (↑a).2 = (↑b).2
⊢ 0 = 0
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
surj : Function.Surjective ⇑(toPiLocalization R)
I : PrimeSpectrum R
⊢ I.asIdeal.IsMaximal

Tactic:
have ⟨J, max, le⟩ := I.1.exists_le_maximal I.2.ne_top

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
surj : Function.Surjective ⇑(toPiLocalization R)
I : PrimeSpectrum R
J : Ideal R
max : J.IsMaximal
le : I.asIdeal ≤ J
⊢ I.asIdeal.IsMaximal
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
surj : Function.Surjective ⇑(toPiLocalization R)
⊢ Finite (PrimeSpectrum R)

Tactic:
replace surj := (mapPiLocalization_bijective _ ⟨toPiLocalization_injective R, surj⟩).2.comp surj

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
surj : Function.Surjective (⇑(mapPiLocalization (toPiLocalization R).toRingHom) ∘ ⇑(toPiLocalization R))
⊢ Finite (PrimeSpectrum R)
Module: Mathlib.Topology.Sets.Opens

Goal state before:
pp: case mp.mk
α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
h : IsBasis B
sU : Set α
hU : IsOpen[inst✝] sU
x : α
hx : x ∈ { carrier := sU, is_open' := hU }
sV : Set α
hsV : x ∈ sV ∧ sV ⊆ sU
carrier✝ : Set α
is_open'✝ : IsOpen[inst✝] carrier✝
H₁ : { carrier := carrier✝, is_open' := is_open'✝ } ∈ B
H₂ : carrier✝ = sV
⊢ x ∈ { carrier := carrier✝, is_open' := is_open'✝ } ∧
    { carrier := carrier✝, is_open' := is_open'✝ } ≤ { carrier := sU, is_open' := hU }

Tactic:
subst H₂

Goal state after:
case mp.mk
α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
h : IsBasis B
sU : Set α
hU : IsOpen[inst✝] sU
x : α
hx : x ∈ { carrier := sU, is_open' := hU }
carrier✝ : Set α
is_open'✝ : IsOpen[inst✝] carrier✝
H₁ : { carrier := carrier✝, is_open' := is_open'✝ } ∈ B
hsV : x ∈ carrier✝ ∧ carrier✝ ⊆ sU
⊢ x ∈ { carrier := carrier✝, is_open' := is_open'✝ } ∧
    { carrier := carrier✝, is_open' := is_open'✝ } ≤ { carrier := sU, is_open' := hU }
Module: Mathlib.Topology.LocalAtTarget

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

Tactic:
intro t
  suffices ∀ u, IsOpen u → Subtype.val ⁻¹' u = t →
    ∃ v, IsOpen v ∧ Subtype.val ⁻¹' v = s.restrictPreimage f '' t by
      simpa [isOpen_induced_iff]
  exact fun u hu e => ⟨f '' u, H u hu, by simp [← e, image_restrictPreimage]⟩

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

Tactic:
isHomeomorph_iff_isEmbedding_surjective,

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 ↔
    ∀ (i : ι), IsEmbedding ((U i).carrier.restrictPreimage f) ∧ Function.Surjective ((U i).carrier.restrictPreimage f)
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: case inr.refine_1
X : Type u_6
Y : Type u_7
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
h : Continuous[inst✝², inst✝¹] f
ι : Type u_4
U : ι → Opens Y
hU : range f ⊆ ↑(iSup U)
V : ι → Type u_5
inst✝ : (i : ι) → TopologicalSpace (V i)
iV : (i : ι) → V i → X
hiV : ∀ (i : ι), Continuous[inst✝ i, inst✝²] (iV i)
hV : ∀ (i : ι), f ⁻¹' ↑(U i) ⊆ range (iV i)
hV' : ∀ (i : ι), IsEmbedding (f ∘ iV i)
this :
  ∀ {X : Type u_6} {Y : Type u_7} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y),
    Continuous f →
      ∀ {ι : Type u_4} (U : ι → Opens Y),
        range f ⊆ ↑(iSup U) →
          ∀ (V : ι → Type u_5) [inst_2 : (i : ι) → TopologicalSpace (V i)] (iV : (i : ι) → V i → X),
            (∀ (i : ι), Continuous (iV i)) →
              (∀ (i : ι), f ⁻¹' ↑(U i) ⊆ range (iV i)) →
                (∀ (i : ι), IsEmbedding (f ∘ iV i)) → iSup U = ⊤ → IsEmbedding f
hU' : ¬iSup U = ⊤
f₀ : X → ↑(range f) := fun x ↦ ⟨f x, ⋯⟩
hU'' : ⨆ i, (Opens.comap { toFun := Subtype.val, continuous_toFun := ⋯ }) (U i) = ⊤
⊢ Continuous[inst✝², instTopologicalSpaceSubtype] f₀

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: X : Type u_6
Y : Type u_7
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
h : Continuous[inst✝², inst✝¹] f
ι : Type u_4
U : ι → Opens Y
hU : range f ⊆ ↑(iSup U)
V : ι → Type u_5
inst✝ : (i : ι) → TopologicalSpace (V i)
iV : (i : ι) → V i → X
hiV : ∀ (i : ι), Continuous[inst✝ i, inst✝²] (iV i)
hV : ∀ (i : ι), f ⁻¹' ↑(U i) ⊆ range (iV i)
hV' : ∀ (i : ι), IsEmbedding (f ∘ iV i)
this :
  ∀ {X : Type u_6} {Y : Type u_7} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y),
    Continuous f →
      ∀ {ι : Type u_4} (U : ι → Opens Y),
        range f ⊆ ↑(iSup U) →
          ∀ (V : ι → Type u_5) [inst_2 : (i : ι) → TopologicalSpace (V i)] (iV : (i : ι) → V i → X),
            (∀ (i : ι), Continuous (iV i)) →
              (∀ (i : ι), f ⁻¹' ↑(U i) ⊆ range (iV i)) →
                (∀ (i : ι), IsEmbedding (f ∘ iV i)) → iSup U = ⊤ → IsEmbedding f
hU' : ¬iSup U = ⊤
f₀ : X → ↑(range f) := fun x ↦ ⟨f x, ⋯⟩
hU'' : ⨆ i, (Opens.comap { toFun := Subtype.val, continuous_toFun := ⋯ }) (U i) = ⊤
i : ι
⊢ Continuous[inst✝ i, instTopologicalSpaceSubtype] (f₀ ∘ iV i)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.NoetherianSpace

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

Tactic:
· simp only [isPreirreducible_iff_isClosed_union_isClosed, not_forall, not_or] at h₁
      obtain ⟨z₁, z₂, hz₁, hz₂, h, hz₁', hz₂'⟩ := h₁
      lift z₁ to Closeds α using hz₁
      lift z₂ to Closeds α using hz₂
      rcases H (s ⊓ z₁) (inf_lt_left.2 hz₁') with ⟨S₁, hSf₁, hS₁, h₁⟩
      rcases H (s ⊓ z₂) (inf_lt_left.2 hz₂') with ⟨S₂, hSf₂, hS₂, h₂⟩
      refine ⟨S₁ ∪ S₂, hSf₁.union hSf₂, Set.union_subset_iff.2 ⟨hS₁, hS₂⟩, ?_⟩
      rwa [sSup_union, ← h₁, ← h₂, ← inf_sup_left, left_eq_inf]

Goal state after:
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: X : Type u_6
Y : Type u_7
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
h : Continuous[inst✝², inst✝¹] f
ι : Type u_4
U : ι → Opens Y
hU : range f ⊆ ↑(iSup U)
V : ι → Type u_5
inst✝ : (i : ι) → TopologicalSpace (V i)
iV : (i : ι) → V i → X
hiV : ∀ (i : ι), Continuous[inst✝ i, inst✝²] (iV i)
hV : ∀ (i : ι), f ⁻¹' ↑(U i) ⊆ range (iV i)
hV' : ∀ (i : ι), IsEmbedding (f ∘ iV i)
hU' : iSup U = ⊤
i : ι
f' : ↑(iV i ⁻¹' f ⁻¹' ↑(U i)) → X := Subtype.val ∘ (f ⁻¹' ↑(U i)).restrictPreimage (iV i)
this : IsEmbedding f'
hf' : range f' = f ⁻¹' ↑(U i)
e : ↑(iV i ⁻¹' f ⁻¹' ↑(U i)) ≃ₜ ↑(f ⁻¹' ↑(U i)) := this.toHomeomorph.trans (Homeomorph.setCongr hf')
⊢ Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] ((U i).carrier.restrictPreimage f)

Tactic:
fun_prop

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 (T ∩ range f)
hx : IsGenericPoint x (closure[inst✝¹] (T ∩ range f))
hxT : x ∈ T
⊢ x ∈ range f

Tactic:
hx.mem_open_set_iff hf.isOpen_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))
hxT : x ∈ T
⊢ (closure[inst✝¹] (T ∩ range f) ∩ range f).Nonempty
Module: Mathlib.Topology.Sober

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : QuasiSober α
inst✝¹ : IrreducibleSpace α
inst✝ : T0Space α
x : α
⊢ x ∈ genericPoints α ↔ x ∈ {genericPoint α}

Tactic:
rw [genericPoints, irreducibleComponents_eq_singleton]

Goal state after:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : QuasiSober α
inst✝¹ : IrreducibleSpace α
inst✝ : T0Space α
x : α
⊢ x ∈ {x | closure {x} ∈ {univ}} ↔ x ∈ {genericPoint α}
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
l : LTSeries (PrimeSpectrum R)
P : Ideal S
inst✝ : P.IsPrime
lo : P.LiesOver (RelSeries.last l).asIdeal
⊢ ∃ L,
    L.length = l.length ∧
      RelSeries.last L = { asIdeal := P, isPrime := ⋯ } ∧
        List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.toList L) = RelSeries.toList l

Tactic:
induction l using RelSeries.inductionOn generalizing P with
  | singleton q =>
    use RelSeries.singleton _ ⟨P, inferInstance⟩
    simp only [RelSeries.singleton_length, RelSeries.last_singleton, RelSeries.toList_singleton,
      List.map_cons, List.map_nil, List.cons.injEq, and_true, true_and]
    ext : 1
    simpa using lo.over.symm
  | cons l q lt ih =>
    simp only [RelSeries.last_cons] at lo
    obtain ⟨L, len, last, spec⟩ := ih P
    have : L.head.asIdeal.LiesOver l.head.asIdeal := by
      constructor
      rw [← L.toList_getElem_zero_eq_head, ← l.toList_getElem_zero_eq_head, Ideal.under_def]
      have : l.toList[0] = (PrimeSpectrum.comap (algebraMap R S)) L.toList[0] := by
        rw [List.getElem_map_rev (PrimeSpectrum.comap (algebraMap R S)),
          List.getElem_of_eq spec.symm _]
      rwa [PrimeSpectrum.ext_iff] at this
    obtain ⟨Q, Qlt, hQ, Qlo⟩ := Ideal.exists_ideal_lt_liesOver_of_lt L.head.asIdeal lt
    use L.cons ⟨Q, hQ⟩ Qlt
    simp only [RelSeries.cons_length, add_left_inj, RelSeries.last_cons]
    exact ⟨len, last, by simpa [spec] using PrimeSpectrum.ext_iff.mpr Qlo.over.symm⟩

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

Goal state before:
pp: case refine_2
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
H :
  ∀ (P : Ideal S) [inst : P.IsPrime],
    Function.Surjective (PrimeSpectrum.comap (Localization.localRingHom (Ideal.under R P) P (algebraMap R S) ⋯))
p : Ideal R
x✝¹ : p.IsPrime
Q : Ideal S
x✝ : Q.IsPrime
hlt : p < Ideal.under R Q
pl : Ideal (Localization.AtPrime (Ideal.under R Q)) :=
  Ideal.map (algebraMap R (Localization.AtPrime (Ideal.under R Q))) p
this : pl.IsPrime
Pl : Ideal (Localization.AtPrime Q)
isPrime✝ : Pl.IsPrime
hl :
  PrimeSpectrum.comap (Localization.localRingHom (Ideal.under R Q) Q (algebraMap R S) ⋯)
      { asIdeal := Pl, isPrime := isPrime✝ } =
    { asIdeal := pl, isPrime := ⋯ }
⊢ p = Ideal.under R (Ideal.under S Pl)

Tactic:
· let := Localization.AtPrime.algebraOfLiesOver (Q.under R) Q
      replace hl : Pl.under _ = pl := by simpa [PrimeSpectrum.ext_iff] using! hl
      rw [Ideal.under_under, ← Ideal.under_under (B := (Localization.AtPrime <| Q.under R)) Pl, hl,
        Ideal.under_map_of_isLocalizationAtPrime (Q.under R) hlt.le]

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

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
Z : Set (PrimeSpectrum S)
⊢ IsClosed Z ↔ ∃ t, IsClosed t ∧ comap (algebraMap R S) ⁻¹' t = Z

Tactic:
isClosed_iff_zeroLocus,

Goal state after:
R : Type u
S : Type v
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
Z : Set (PrimeSpectrum S)
⊢ (∃ s, Z = zeroLocus s) ↔ ∃ t, (∃ s, t = zeroLocus s) ∧ comap (algebraMap R S) ⁻¹' t = Z
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
⊢ IsCyclic α ↔ ∃ g, zpowers g = ⊤

Tactic:
simp only [eq_top_iff', mem_zpowers_iff]

Goal state after:
α : Type u_1
inst✝ : Group α
⊢ IsCyclic α ↔ ∃ g, ∀ (x : α), ∃ k, g ^ k = x
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
inst✝¹ : (i : ι) → CommRing (R i)
inst✝ : DecidableEq ι
i : ι
f : R i
p : PrimeSpectrum ((i : ι) → R i)
hp : p ∈ ↑(basicOpen (Pi.single i f))
⊢ p ∈ Set.range (comap (Pi.evalRingHom R i))

Tactic:
rw [range_comap_of_surjective _ _ (RingHom.surjective _), mem_zeroLocus,
        SetLike.coe_subset_coe]

Goal state after:
ι : Type u_1
R : ι → Type u_2
inst✝¹ : (i : ι) → CommRing (R i)
inst✝ : DecidableEq ι
i : ι
f : R i
p : PrimeSpectrum ((i : ι) → R i)
hp : p ∈ ↑(basicOpen (Pi.single i f))
⊢ RingHom.ker (Pi.evalRingHom R i) ≤ p.asIdeal
Module: Mathlib.Data.ZMod.QuotientGroup

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝² : Group α
a : α
inst✝¹ : MulAction α β
b : β
inst✝ : Fintype ↑(orbit (↥(zpowers a)) b)
⊢ minimalPeriod (fun x ↦ a • x) b = Fintype.card (ZMod (minimalPeriod (fun x ↦ a • x) b))

Tactic:
ZMod.card

Goal state after:
α : Type u_3
β : Type u_4
inst✝² : Group α
a : α
inst✝¹ : MulAction α β
b : β
inst✝ : Fintype ↑(orbit (↥(zpowers a)) b)
⊢ minimalPeriod (fun x ↦ a • x) b = minimalPeriod (fun x ↦ a • x) b
Module: Mathlib.Data.ZMod.QuotientGroup

Goal state before:
pp: α : 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

Tactic:
Nat.card_zmod,

Goal state after:
α : Type u_3
inst✝ : Group α
a : α
this : Nat.card ↑(MulAction.orbit (↥(zpowers a)) 1) = Function.minimalPeriod (fun x ↦ a • x) 1
⊢ Nat.card ↥(zpowers a) = orderOf a