mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Polynomial.Nilpotent

Goal state before:
pp: case right
R : Type u_1
inst✝ : CommRing R
P : R[X]
hunit : IsUnit P
Q : R[X]
hQ : P * Q = 1
n : ℕ
hn : n ≠ 0
I : Ideal R
hI : I.IsPrime
f : R[X] →+* (R ⧸ I)[X] := mapRingHom (Ideal.Quotient.mk I)
⊢ P.coeff n ∈ I

Tactic:
have hPQ : degree (f P) = 0 ∧ degree (f Q) = 0 := by
      rw [← Nat.WithBot.add_eq_zero_iff, ← degree_mul, ← map_mul, hQ, map_one, degree_one]

Goal state after:
case right
R : Type u_1
inst✝ : CommRing R
P : R[X]
hunit : IsUnit P
Q : R[X]
hQ : P * Q = 1
n : ℕ
hn : n ≠ 0
I : Ideal R
hI : I.IsPrime
f : R[X] →+* (R ⧸ I)[X] := mapRingHom (Ideal.Quotient.mk I)
hPQ : (f P).degree = 0 ∧ (f Q).degree = 0
⊢ P.coeff n ∈ I
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: R : Type u_1
M : Type u
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : RankCondition R
ι : Type u
v : ι → M
hv : Function.Injective v
hs : LinearIndependent R v
x : { s // span R s = span R (Set.range v) }
this : #↑↑x = #↑(Subtype.val ⁻¹' ↑x)
⊢ Function.Injective (Subtype.val ∘ ⇑(Module.Basis.span hs))

Tactic:
convert! hv; ext; simp [Module.Basis.span_apply]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Lifts

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
n : ℕ
r : R
h : f r ∈ Set.range ⇑f
⊢ (monomial n) (f r) ∈ lifts f

Tactic:
use monomial n r

Goal state after:
case h
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
n : ℕ
r : R
h : f r ∈ Set.range ⇑f
⊢ (mapRingHom f) ((monomial n) r) = (monomial n) (f r)
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: case zero
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
I : Ideal R
h : ∀ (i j : n), M i j ∈ I
k : ℕ
c : Equiv.Perm n
this : ∑ x, 1 = Fintype.card n
i : n
⊢ ((X • 1) (c i) i).coeff 0 - (C (M (c i) i)).coeff 0 ∈ I

Tactic:
smul_apply,

Goal state after:
case zero
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
I : Ideal R
h : ∀ (i j : n), M i j ∈ I
k : ℕ
c : Equiv.Perm n
this : ∑ x, 1 = Fintype.card n
i : n
⊢ (X • 1 (c i) i).coeff 0 - (C (M (c i) i)).coeff 0 ∈ I
Module: Mathlib.Tactic.Positivity.Finset

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : Fintype α
G : Type u_2
A : Finset G
⊢ let f := fun x ↦ 1;
  (∀ (s : G), f s ^ 2 = 1) → 0 ≤ #A

Tactic:
intros
  positivity

Goal state after:
Module: Mathlib.Algebra.Polynomial.HasseDeriv

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
hikl : k + l ≤ i
⊢ (i - l).choose k * i.choose l = (k + l).choose k * i.choose (k + l)

Tactic:
apply @cast_injective ℚ

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
hikl : k + l ≤ i
⊢ ↑((i - l).choose k * i.choose l) = ↑((k + l).choose k * i.choose (k + l))
Module: Mathlib.Algebra.Polynomial.HasseDeriv

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k : ℕ
f g : R[X]
⊢ (hasseDeriv k) (f * g) = ∑ ij ∈ antidiagonal k, (hasseDeriv ij.1) f * (hasseDeriv ij.2) g

Tactic:
let D k := (@hasseDeriv R _ k).toAddMonoidHom

Goal state after:
R : Type u_1
inst✝ : Semiring R
k : ℕ
f g : R[X]
D : ℕ → R[X] →+ R[X] := fun k ↦ (hasseDeriv k).toAddMonoidHom
⊢ (hasseDeriv k) (f * g) = ∑ ij ∈ antidiagonal k, (hasseDeriv ij.1) f * (hasseDeriv ij.2) g
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
h₁ : ¬p.natDegree ≤ n
h₂ : n = p.natDegree
⊢ 0 = p.leadingCoeff

Tactic:
exact (h₁ h₂.ge).elim

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
hr : IsUnit r
a b : R[X]
e : a * p + b * q = 1
s : R := ↑hr.unit⁻¹
⊢ IsCoprime (p.scaleRoots r) (q.scaleRoots r)

Tactic:
have : natDegree (a * p) = natDegree (b * q) := by
    apply natDegree_eq_of_natDegree_add_eq_zero
    rw [e, natDegree_one]

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
hr : IsUnit r
a b : R[X]
e : a * p + b * q = 1
s : R := ↑hr.unit⁻¹
this : (a * p).natDegree = (b * q).natDegree
⊢ IsCoprime (p.scaleRoots r) (q.scaleRoots r)
Module: Mathlib.Algebra.Polynomial.Splits

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

Tactic:
rw [Multiset.map_cons, Multiset.prod_cons] at hm

Goal state after:
case inr
R : Type u_1
inst✝ : CommSemiring R
f : R[X]
hf : f.Splits
h : Irreducible f
a✝ : Nontrivial R
a : R
m : Multiset R
hm : f = C f.leadingCoeff * ((X + C a) * (Multiset.map (fun x ↦ X + C x) m).prod)
ha : a ∈ a ::ₘ m
⊢ f.natDegree ≤ 1
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: case pos
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : R[X]
x : S
h : eval₂ f x p = 0
h' : ¬1 ≤ p.natDegree
hp : Polynomial.map f p = 0
⊢ f.IsIntegralElem (f p.leadingCoeff * x)

Tactic:
apply_fun fun q => coeff q p.natDegree at hp

Goal state after:
case pos
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : R[X]
x : S
h : eval₂ f x p = 0
h' : ¬1 ≤ p.natDegree
hp : (Polynomial.map f p).coeff p.natDegree = coeff 0 p.natDegree
⊢ f.IsIntegralElem (f p.leadingCoeff * x)
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: R : Type u_1
S : Type u_4
T : Type u_5
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : CommRing T
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsTorsionFree S T
inst✝¹ : Nontrivial T
inst✝ : IsScalarTower R S T
h : Algebra.IsIntegral R T
⊢ ((algebraMap S T).comp (algebraMap R S)).IsIntegral

Tactic:
← IsScalarTower.algebraMap_eq R S T

Goal state after:
R : Type u_1
S : Type u_4
T : Type u_5
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : CommRing T
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsTorsionFree S T
inst✝¹ : Nontrivial T
inst✝ : IsScalarTower R S T
h : Algebra.IsIntegral R T
⊢ (algebraMap R T).IsIntegral
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: R : Type u_1
S : Type u_4
T : Type u_5
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
h : Algebra.IsIntegral R T
⊢ ((algebraMap S T).comp (algebraMap R S)).IsIntegral

Tactic:
← IsScalarTower.algebraMap_eq R S T

Goal state after:
R : Type u_1
S : Type u_4
T : Type u_5
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
h : Algebra.IsIntegral R T
⊢ (algebraMap R T).IsIntegral
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
g : R →+* R ⧸ Ideal.comap f I := Ideal.Quotient.mk (Ideal.comap f I)
this : (Ideal.quotientMap I f ⋯).comp g = (Ideal.Quotient.mk I).comp f
h : (Ideal.quotientMap I f ⋯).IsIntegral
⊢ g.IsIntegral

Tactic:
exact g.isIntegral_of_surjective Ideal.Quotient.mk_surjective

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

Goal state before:
pp: R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
y : R
hy : ¬IsNilpotent y
h✝ : IsIntegral R (y • z)
p : R[X]
monic : p.Monic
eval0 : eval₂ (algebraMap R A) (y • z) p = 0
h : y ^ p.natDegree = 0
hy0 : y ≠ 0
⊢ False

Tactic:
exact hy ⟨_, h⟩

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

Goal state before:
pp: case right.inr
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p : Ideal S
hp : p.IsPrime
hI : (⊤.prod p).IsPrime
⊢ ∃ a, primeSpectrumProdOfSum R S a = { asIdeal := ⊤.prod p, isPrime := hI }

Tactic:
exact ⟨Sum.inr ⟨p, hp⟩, rfl⟩

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set R
h : 1 ∈ s
x : PrimeSpectrum R
hx : s ⊆ ↑x.asIdeal
x_prime : x.asIdeal.IsPrime
eq_top : x.asIdeal = ⊤
⊢ False

Tactic:
apply x_prime.ne_top eq_top

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set R
h : 1 ∈ s
⊢ zeroLocus s = ∅

Tactic:
rw [Set.eq_empty_iff_forall_notMem]
  intro x hx
  rw [mem_zeroLocus] at hx
  have x_prime : x.asIdeal.IsPrime := by infer_instance
  have eq_top : x.asIdeal = ⊤ := by
    rw [Ideal.eq_top_iff_one]
    exact hx h
  apply x_prime.ne_top eq_top

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set R
h : 1 ∈ s
⊢ zeroLocus s = ∅

Tactic:
by
  rw [Set.eq_empty_iff_forall_notMem]
  intro x hx
  rw [mem_zeroLocus] at hx
  have x_prime : x.asIdeal.IsPrime := by infer_instance
  have eq_top : x.asIdeal = ⊤ := by
    rw [Ideal.eq_top_iff_one]
    exact hx h
  apply x_prime.ne_top eq_top

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 R A
s : S
a : A
ha : IsAlgebraic R a
inst✝ : FaithfulSMul R S
p : R[X]
h : p ≠ 0
eval0 : (aeval a) p = 0
⊢ (aeval (↑Algebra.TensorProduct.includeRight a)) (map (algebraMap R S) p) = 0

Tactic:
← map_aeval_eq_aeval_map (by ext; simp),

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 R A
s : S
a : A
ha : IsAlgebraic R a
inst✝ : FaithfulSMul R S
p : R[X]
h : p ≠ 0
eval0 : (aeval a) p = 0
⊢ ↑Algebra.TensorProduct.includeRight ((aeval a) p) = 0
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)
x' : L
hx : (algebraMap S L) a * x' ∈ ↑(Ideal.span {(algebraMap S L) a})
⊢ (algebraMap S L) a * x' ∈ ↑(Submodule.span K (⇑(algebraMap S L) '' b))

Tactic:
obtain ⟨y', z', rfl⟩ := IsLocalization.exists_mk'_eq S⁰ x'

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})
⊢ (algebraMap S L) a * mk' L y' z' ∈ ↑(Submodule.span K (⇑(algebraMap S L) '' b))
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: case pos
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : IsDomain T
inst✝³ : Algebra S T
inst✝² : Algebra R T
inst✝¹ : IsScalarTower R S T
inst✝ : FaithfulSMul S T
h : FaithfulSMul R S
⊢ finrank R S * finrank S T = finrank R T

pp: case neg
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : IsDomain T
inst✝³ : Algebra S T
inst✝² : Algebra R T
inst✝¹ : IsScalarTower R S T
inst✝ : FaithfulSMul S T
h : ¬FaithfulSMul R S
⊢ finrank R S * finrank S T = finrank R T

Tactic:
· have : FaithfulSMul R T := .trans R S T
    have : IsDomain R := (FaithfulSMul.algebraMap_injective R T).isDomain
    have : IsDomain S := (FaithfulSMul.algebraMap_injective S T).isDomain
    rw [← IsFractionRing.finrank_eq R (FractionRing R) S (FractionRing S),
      ← IsFractionRing.finrank_eq S (FractionRing S) T (FractionRing T),
      ← IsFractionRing.finrank_eq R (FractionRing R) T (FractionRing T),
      Module.finrank_mul_finrank (FractionRing R) (FractionRing S) (FractionRing T)]

Goal state after:
case neg
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : IsDomain T
inst✝³ : Algebra S T
inst✝² : Algebra R T
inst✝¹ : IsScalarTower R S T
inst✝ : FaithfulSMul S T
h : ¬FaithfulSMul R S
⊢ finrank R S * finrank S T = finrank R T
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✝³ : IsDomain B
inst✝² : Flat A B
inst✝¹ : Algebra.IsIntegral A B
inst✝ : FaithfulSMul A B
P : PrimeSpectrum A
⊢ ∃ a, PrimeSpectrum.comap (algebraMap A B) a = P

Tactic:
obtain ⟨P, hP₁, hP₂⟩ := Ideal.exists_ideal_over_prime_of_isIntegral_of_isDomain P.1 (S := B)
    (by simp [(RingHom.injective_iff_ker_eq_bot _).mp (FaithfulSMul.algebraMap_injective A B)])

Goal state after:
A : Type u_1
B : Type u_2
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : IsDomain B
inst✝² : Flat A B
inst✝¹ : Algebra.IsIntegral A B
inst✝ : FaithfulSMul A B
P✝ : PrimeSpectrum A
P : Ideal B
hP₁ : P.IsPrime
hP₂ : Ideal.comap (algebraMap A B) P = P✝.asIdeal
⊢ ∃ a, PrimeSpectrum.comap (algebraMap A B) a = P✝
Module: Mathlib.RingTheory.KrullDimension.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
⊢ KrullDimLE 1 R ↔ ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal

Tactic:
cases subsingleton_or_nontrivial R
  · exact iff_of_true inferInstance fun I h ↦ (h <| Subsingleton.elim ..).elim
  exact Ring.krullDimLE_one_iff_of_isPrime_bot

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
inst✝² : CommRing K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
hS : S ≤ A⁰
s : ↥S
⊢ IsUnit ((algebraMap A K) ↑s)

Tactic:
by
  apply IsLocalization.map_units K (⟨s.1, hS s.2⟩ : A⁰)

Goal state after:
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: case mp
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal S
J : Ideal R
H : J ∈ (comap f I).minimalPrimes
⊢ J ∈ comap f '' I.minimalPrimes

Tactic:
obtain ⟨p, h, rfl⟩ := Ideal.exists_minimalPrimes_comap_eq f J H

Goal state after:
case mp
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I p : Ideal S
h : p ∈ I.minimalPrimes
H : comap f p ∈ (comap f I).minimalPrimes
⊢ comap f p ∈ comap f '' I.minimalPrimes
Module: Mathlib.Topology.LocallyClosed

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

Tactic:
by
  rw [coborder, compl_eq_comm, compl_union, compl_compl, inter_comm]
  rfl

Goal state after:
Module: Mathlib.Topology.NoetherianSpace

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
⊢ [NoetherianSpace α, WellFoundedLT (Closeds α), ∀ (s : Set α), IsCompact s, ∀ (s : Opens α), IsCompact ↑s].TFAE

Tactic:
tfae_have 1 ↔ 2 := by
    simp_rw [isWellFounded_iff]
    exact Opens.compl_bijective.2.wellFounded_iff (@OrderIso.compl (Set α)).lt_iff_lt.symm

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
tfae_1_iff_2 : NoetherianSpace α ↔ WellFoundedLT (Closeds α)
⊢ [NoetherianSpace α, WellFoundedLT (Closeds α), ∀ (s : Set α), IsCompact s, ∀ (s : Opens α), IsCompact ↑s].TFAE
Module: Mathlib.Topology.Spectral.Prespectral

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : PrespectralSpace X
Z U₁ U₂ : Set X
hU₁ : ∀ a ∈ U₁, ∃ t ∈ {U | IsOpen[inst✝¹] U ∧ IsCompact U}, a ∈ t ∧ t ⊆ U₁
hU₂ : ∀ a ∈ U₂, ∃ t ∈ {U | IsOpen[inst✝¹] U ∧ IsCompact U}, a ∈ t ∧ t ⊆ U₂
hU₁Z : (Z ∩ U₁).Nonempty
hU₂Z : (Z ∩ U₂).Nonempty
hU₁₂ : Z ∩ (U₁ ∩ U₂) ⊆ ∅
x₁ : X
hx₁ : x₁ ∈ U₁ ∧ x₁ ∈ Z ∧ x₁ ∉ U₂
x₂ : X
hx₂ : x₂ ∈ U₂ ∧ x₂ ∈ Z ∧ x₂ ∉ U₁
W₁ : Set X
hW₁ : W₁ ∈ {U | IsOpen[inst✝¹] U ∧ IsCompact U} ∧ x₁ ∈ W₁ ∧ W₁ ⊆ U₁
W₂ : Set X
hW₂ : W₂ ∈ {U | IsOpen[inst✝¹] U ∧ IsCompact U} ∧ x₂ ∈ W₂ ∧ W₂ ⊆ U₂
z : X
hz : z ∈ Z
⊢ z ∈ W₁ᶜ ∪ W₂ᶜ

Tactic:
· by_contra! hc
    simp only [Set.mem_union, Set.mem_compl_iff, not_or, not_not] at hc
    exact hU₁₂ ⟨hz, hW₁.2.2 hc.1, hW₂.2.2 hc.2⟩

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:
by
      rw [hx.mem_open_set_iff hf.isOpen_range]
      refine Nonempty.mono ?_ hS''.1
      simpa using subset_closure

Goal state after:
Module: Mathlib.Topology.Constructible

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

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

Tactic:
· rintro x ⟨hx₁, hx₂⟩
      obtain ⟨i, hi, hxi⟩ := Set.mem_iUnion₂.mp (ht hx₁)
      exact Set.mem_iUnion₂.mpr ⟨i, hi, by simpa [*]⟩

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

Goal state before:
pp: X : Type u_2
inst✝² : TopologicalSpace X
s t : Set X
inst✝¹ : PrespectralSpace X
inst✝ : QuasiSeparatedSpace X
hs : IsLocallyConstructible s
hst : s ⊆ t
ht : IsCompact t
⊢ IsConstructible s

Tactic:
have (x : _) : ∃ U, IsOpen U ∧ IsCompact U ∧ x ∈ U ∧ IsConstructible (U ∩ s) :=
    have ⟨U, hxU, hU, hUs⟩ := hs x
    have ⟨V, ⟨hV₁, hV₂⟩, hxV, hVU⟩ := PrespectralSpace.isTopologicalBasis.mem_nhds_iff.mp hxU
    have : IsConstructible (V ↓∩ s) :=
      (hUs.preimage_of_isOpenEmbedding (IsOpenEmbedding.id.restrict hVU hV₁) :)
    have : IsConstructible (V ∩ s) := by
      have := this.image_of_isOpenEmbedding hV₁.isOpenEmbedding_subtypeVal
        (by simpa using hV₂.isRetrocompact hV₁)
      rwa [Subtype.image_preimage_coe] at this
    ⟨V, hV₁, hV₂, hxV, this⟩

Goal state after:
X : Type u_2
inst✝² : TopologicalSpace X
s t : Set X
inst✝¹ : PrespectralSpace X
inst✝ : QuasiSeparatedSpace X
hs : IsLocallyConstructible s
hst : s ⊆ t
ht : IsCompact t
this : ∀ (x : X), ∃ U, IsOpen[inst✝²] U ∧ IsCompact U ∧ x ∈ U ∧ IsConstructible (U ∩ s)
⊢ IsConstructible s
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsRadical
⊢ IsIrreducible (zeroLocus ↑I) ↔ I.IsPrime

Tactic:
rw [Ideal.isPrime_iff, IsIrreducible]

Goal state after:
R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsRadical
⊢ (zeroLocus ↑I).Nonempty ∧ IsPreirreducible (zeroLocus ↑I) ↔ I ≠ ⊤ ∧ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I
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 : Ideal R),
      zeroLocus ↑I ⊆ zeroLocus ↑x ∪ zeroLocus ↑y → zeroLocus ↑I ⊆ zeroLocus ↑x ∨ zeroLocus ↑I ⊆ zeroLocus ↑y) →
    ∀ (z₁ z₂ : Set (PrimeSpectrum R)),
      (∃ I, z₁ = zeroLocus ↑I) →
        (∃ I, z₂ = zeroLocus ↑I) → zeroLocus ↑I ⊆ z₁ ∪ z₂ → zeroLocus ↑I ⊆ z₁ ∨ zeroLocus ↑I ⊆ z₂

Tactic:
· rintro h _ _ ⟨x, rfl⟩ ⟨y, rfl⟩
        exact h x y

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

Goal state before:
pp: R S T A : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing T
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R T
inst✝⁴ : Algebra S T
inst✝³ : IsScalarTower R S T
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
h : CommRingCat.flat (CommRingCat.ofHom (Algebra.TensorProduct.lmul' R).toRingHom)
⊢ IsPushout
    (CommRingCat.ofHom
      (Algebra.TensorProduct.map (IsScalarTower.toAlgHom R S T) (IsScalarTower.toAlgHom R S A)).toRingHom)
    (CommRingCat.ofHom (Algebra.TensorProduct.lmul' R).toRingHom)
    (CommRingCat.ofHom (Algebra.TensorProduct.mapOfCompatibleSMul S R T T A).toRingHom)
    (CommRingCat.ofHom (Algebra.TensorProduct.includeLeft.comp (algebraMap S T)))

Tactic:
refine .of_iso
      (isPushout_map_codiagonal (CommRingCat.ofHom <| algebraMap S T)
        (CommRingCat.ofHom <| algebraMap S A) (CommRingCat.ofHom <| algebraMap R S))
      ?_ ?_ (.refl _) ?_ ?_ ?_ ?_ ?_
    · exact (CommRingCat.isPushout_tensorProduct R S S).isoPushout.symm
    · exact pushout.congrHom (by simp [IsScalarTower.algebraMap_eq R S T])
          (by simp [IsScalarTower.algebraMap_eq R S A]) ≪≫
        (CommRingCat.isPushout_tensorProduct R T A).isoPushout.symm
    · exact (CommRingCat.isPushout_tensorProduct S T A).isoPushout.symm
    all_goals ext <;> simp

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

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

Tactic:
by
  rw [← SetLike.coe_subset_coe, basicOpen_eq_zeroLocus_compl, basicOpen_eq_zeroLocus_compl,
    Set.compl_subset_compl, zeroLocus_subset_zeroLocus_singleton_iff]

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
⊢ Monoid.exponent Gᵐᵒᵖ = Monoid.exponent G

Tactic:
simp only [Monoid.exponent, ExponentExists]

Goal state after:
G : Type u
inst✝ : Monoid G
⊢ (if h : ∃ n, 0 < n ∧ ∀ (g : Gᵐᵒᵖ), g ^ n = 1 then Nat.find h else 0) =
    if h : ∃ n, 0 < n ∧ ∀ (g : G), g ^ n = 1 then Nat.find h else 0
Module: Mathlib.Data.ZMod.QuotientGroup

Goal state before:
pp: a : ℤ
⊢ Nat.card (ℤ ⧸ AddSubgroup.zmultiples a) = a.natAbs

Tactic:
Nat.card_congr (quotientZMultiplesEquivZMod a).toEquiv,

Goal state after:
a : ℤ
⊢ Nat.card (ZMod a.natAbs) = a.natAbs
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
g : α
hx : ∀ (x : α), x ∈ Submonoid.powers g
⊢ orderOf g = Nat.card α

Tactic:
by
  rw [orderOf_eq_card_of_forall_mem_zpowers]
  exact fun x ↦ Submonoid.powers_le_zpowers _ (hx _)

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
k : ℕ
k_pos : k ≠ 0
k_lt_card_G : k < Nat.card G
this : Finite G
a : G
ha : Function.Surjective fun x ↦ a ^ x
⊢ ∃ a, a ^ k ≠ 1

Tactic:
use a

Goal state after:
case h
G : Type u_2
inst✝ : Group G
k : ℕ
k_pos : k ≠ 0
k_lt_card_G : k < Nat.card G
this : Finite G
a : G
ha : Function.Surjective fun x ↦ a ^ x
⊢ a ^ k ≠ 1
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
this : exponent G ≠ 0 ↔ (Set.range orderOf).Finite
⊢ exponent G = 0 ↔ (Set.range orderOf).Infinite

Tactic:
rwa [Ne, not_iff_comm, Iff.comm] at this

Goal state after: