mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.TensorProduct.MvPolynomial

Goal state before:
pp: R : Type u
N : Type v
inst✝⁴ : CommSemiring R
σ : Type u_1
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : CommSemiring N
inst✝ : Algebra R N
f : σ → S
p : MvPolynomial σ R
⊢ (aeval fun x ↦ 1 ⊗ₜ[R] f x) p = 1 ⊗ₜ[R] (aeval f) p

Tactic:
by
  induction p using MvPolynomial.induction_on with
  | C a =>
    simp only [algHom_C, Algebra.TensorProduct.algebraMap_apply]
    rw [← mul_one ((algebraMap R N) a), ← Algebra.smul_def, smul_tmul, Algebra.smul_def, mul_one]
  | add p q hp hq => simp [hp, hq, tmul_add]
  | mul_X p i h => simp [h]

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

Goal state before:
pp: case inr.inr
R : Type u_1
inst✝ : CommRing R
p : R[X]
r a : R
hr : IsLeftRegular r
h✝ : Nontrivial R
hp : p ≠ 0
q : R[X]
e : p = (X - C a) ^ rootMultiplicity a p * q
hq : ¬X - C a ∣ q
hq0 : q ≠ 0
⊢ rootMultiplicity (a * r) (q.scaleRoots r * (X - C (a * r)) ^ rootMultiplicity a p) = rootMultiplicity a p

pp: case inr.inr.hp
R : Type u_1
inst✝ : CommRing R
p : R[X]
r a : R
hr : IsLeftRegular r
h✝ : Nontrivial R
hp : p ≠ 0
q : R[X]
e : p = (X - C a) ^ rootMultiplicity a p * q
hq : ¬X - C a ∣ q
hq0 : q ≠ 0
⊢ (X - C a).leadingCoeff ^ rootMultiplicity a p ≠ 0

pp: case inr.inr.h
R : Type u_1
inst✝ : CommRing R
p : R[X]
r a : R
hr : IsLeftRegular r
h✝ : Nontrivial R
hp : p ≠ 0
q : R[X]
e : p = (X - C a) ^ rootMultiplicity a p * q
hq : ¬X - C a ∣ q
hq0 : q ≠ 0
⊢ ((X - C a) ^ rootMultiplicity a p).leadingCoeff * q.leadingCoeff ≠ 0

Tactic:
rootMultiplicity_mul_X_sub_C_pow (q.scaleRoots_ne_zero hq0 _)

Goal state after:
case inr.inr
R : Type u_1
inst✝ : CommRing R
p : R[X]
r a : R
hr : IsLeftRegular r
h✝ : Nontrivial R
hp : p ≠ 0
q : R[X]
e : p = (X - C a) ^ rootMultiplicity a p * q
hq : ¬X - C a ∣ q
hq0 : q ≠ 0
⊢ rootMultiplicity (a * r) (q.scaleRoots r) + rootMultiplicity a p = rootMultiplicity a p

case inr.inr.hp
R : Type u_1
inst✝ : CommRing R
p : R[X]
r a : R
hr : IsLeftRegular r
h✝ : Nontrivial R
hp : p ≠ 0
q : R[X]
e : p = (X - C a) ^ rootMultiplicity a p * q
hq : ¬X - C a ∣ q
hq0 : q ≠ 0
⊢ (X - C a).leadingCoeff ^ rootMultiplicity a p ≠ 0

case inr.inr.h
R : Type u_1
inst✝ : CommRing R
p : R[X]
r a : R
hr : IsLeftRegular r
h✝ : Nontrivial R
hp : p ≠ 0
q : R[X]
e : p = (X - C a) ^ rootMultiplicity a p * q
hq : ¬X - C a ∣ q
hq0 : q ≠ 0
⊢ ((X - C a) ^ rootMultiplicity a p).leadingCoeff * q.leadingCoeff ≠ 0
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommSemiring R
S : Submonoid R[X] := MonoidHom.mrange C
hS : ↑S = {x | ∃ a, C a = x}
a : R
g : R[X]
hg : g ∈ Submonoid.closure {x | ∃ a, X + C a = x}
⊢ ∃ m, C a * g = C (C a * g).leadingCoeff * (Multiset.map (fun x ↦ X + C x) m).prod

Tactic:
obtain ⟨mg, hmg, rfl⟩ := Submonoid.exists_multiset_of_mem_closure hg

Goal state after:
case refine_1
R : Type u_1
inst✝ : CommSemiring R
S : Submonoid R[X] := MonoidHom.mrange C
hS : ↑S = {x | ∃ a, C a = x}
a : R
mg : Multiset R[X]
hmg : ∀ y ∈ mg, y ∈ {x | ∃ a, X + C a = x}
hg : mg.prod ∈ Submonoid.closure {x | ∃ a, X + C a = x}
⊢ ∃ m, C a * mg.prod = C (C a * mg.prod).leadingCoeff * (Multiset.map (fun x ↦ X + C x) m).prod
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ integralClosure R A = ⊤ ↔ Algebra.IsIntegral R A

Tactic:
by
  rw [← top_le_iff, le_integralClosure_iff_isIntegral,
      (Subalgebra.topEquiv (R := R) (A := A)).isIntegral_iff]

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

Goal state before:
pp: case succ.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ih : ∀ {f g : R[X]}, f ≠ 0 → g ≠ 0 → ∀ (p : R[X]), f * g = p → p.Splits → p.natDegree = n → f.Splits ∧ g.Splits
f g : R[X]
hf₀ : f ≠ 0
hg₀ : g ≠ 0
p : R[X]
hp : f * g = p
h : p.Splits
hn : p.natDegree = n + 1
a : R
ha : eval a p = 0
this : X - C a ∣ f ∨ X - C a ∣ g
hf2 :
  ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] (n : ℕ)
    (ih : ∀ {f g : R[X]}, f ≠ 0 → g ≠ 0 → ∀ (p : R[X]), f * g = p → p.Splits → p.natDegree = n → f.Splits ∧ g.Splits)
    {f g : R[X]} (hf₀ : f ≠ 0) (hg₀ : g ≠ 0) (p : R[X]) (hp : f * g = p) (h : p.Splits) (hn : p.natDegree = n + 1)
    (a : R) (ha : eval a p = 0) (this : X - C a ∣ f ∨ X - C a ∣ g), X - C a ∣ f → f.Splits ∧ g.Splits
hf : ¬X - C a ∣ f
⊢ f.Splits ∧ g.Splits

Tactic:
exact .symm <| hf2 n ih hg₀ hf₀ p ((mul_comm g f).trans hp) h hn a ha this.symm <|
        this.resolve_left hf

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsIntegralClosure A R B
h : IsIntegral R 0
⊢ (algebraMap A B) (mk' A 0 h) = (algebraMap A B) 0

Tactic:
by rw [algebraMap_mk', map_zero]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : Ideal R[X]
Pb : P ≠ ⊥
hP : ∀ (x : R), C x ∈ P → x = 0
m : ↥P
hm : m ≠ 0
pp0 : Polynomial.map (Quotient.mk (comap C P)) ↑m = 0
⊢ ↑m = 0

Tactic:
refine
    (injective_iff_map_eq_zero (Polynomial.mapRingHom (Ideal.Quotient.mk
      (P.comap (C : R →+* R[X]))))).mp
      ?_ _ pp0

Goal state after:
R : Type u_1
inst✝ : CommRing R
P : Ideal R[X]
Pb : P ≠ ⊥
hP : ∀ (x : R), C x ∈ P → x = 0
m : ↥P
hm : m ≠ 0
pp0 : Polynomial.map (Quotient.mk (comap C P)) ↑m = 0
⊢ Function.Injective ⇑(mapRingHom (Quotient.mk (comap C P)))
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
x✝ :
  Flat R M ∧ ∀ (N : Type (max u v)) [inst : AddCommGroup N] [inst_1 : Module R N], Nontrivial N → Nontrivial (N ⊗[R] M)
flat : Flat R M
faithful : ∀ (N : Type (max u v)) [inst : AddCommGroup N] [inst_1 : Module R N], Nontrivial N → Nontrivial (N ⊗[R] M)
⊢ ∀ ⦃m : Ideal R⦄, m.IsMaximal → m • ⊤ ≠ ⊤

Tactic:
intro m hm rid

Goal state after:
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ :
  Flat R M ∧ ∀ (N : Type (max u v)) [inst : AddCommGroup N] [inst_1 : Module R N], Nontrivial N → Nontrivial (N ⊗[R] M)
flat : Flat R M
faithful : ∀ (N : Type (max u v)) [inst : AddCommGroup N] [inst_1 : Module R N], Nontrivial N → Nontrivial (N ⊗[R] M)
m : Ideal R
hm : m.IsMaximal
rid : m • ⊤ = ⊤
⊢ False
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
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
a✝ : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := q.support.sup fun x ↦ (q.coeff x).natDegree
hN : ∀ (i : ℕ), (q.coeff i).natDegree ≤ N
q' : R[X] := q.sum fun i r ↦ X ^ i * reflect N r
this : ∀ (i : ℕ), (aeval t) (reflect N (q.coeff i)) = t ^ N * (aeval s) (q.coeff i)
⊢ IsIntegral R t

Tactic:
refine ⟨q', ?_, ?_⟩

Goal state after:
case refine_1
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
a✝ : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := q.support.sup fun x ↦ (q.coeff x).natDegree
hN : ∀ (i : ℕ), (q.coeff i).natDegree ≤ N
q' : R[X] := q.sum fun i r ↦ X ^ i * reflect N r
this : ∀ (i : ℕ), (aeval t) (reflect N (q.coeff i)) = t ^ N * (aeval s) (q.coeff i)
⊢ q'.Monic

case refine_2
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
a✝ : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := q.support.sup fun x ↦ (q.coeff x).natDegree
hN : ∀ (i : ℕ), (q.coeff i).natDegree ≤ N
q' : R[X] := q.sum fun i r ↦ X ^ i * reflect N r
this : ∀ (i : ℕ), (aeval t) (reflect N (q.coeff i)) = t ^ N * (aeval s) (q.coeff i)
⊢ eval₂ (algebraMap R S) t q' = 0
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: case pos
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
⊢ IsAlgebraic R a

Tactic:
have ⟨s, hs, int_s⟩ := h.exists_integral_multiple

Goal state after:
case pos
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)
⊢ IsAlgebraic R a
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
p : Ideal R
inst✝² : p.IsPrime
q : Ideal S
inst✝¹ : q.IsPrime
hq : p.primesOver S = {q}
inst✝ : Algebra.IsIntegral R S
x✝ : S
hx : x✝ ∉ q
this : ∀ r ∉ p, ∀ (c : S), c * x✝ ≠ (algebraMap R S) r
Q : Ideal S
hQ : Q.IsPrime
hxQ✝ : span {x✝} ≤ Q
hQp : Disjoint ↑Q ↑(Algebra.algebraMapSubmonoid S p.primeCompl)
x : R
hxQ : x ∈ under R Q
hxp : x ∉ p
⊢ False

Tactic:
exact Set.subset_compl_iff_disjoint_right.mpr hQp hxQ ⟨x, hxp, rfl⟩

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

Goal state before:
pp: case left.inl.inr
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
I : Ideal R
hI : I.IsPrime
J' : Ideal S
hJ' : J'.IsPrime
h : I = ⊤ ∧ ⊤ = J'
⊢ Sum.inl { asIdeal := I, isPrime := hI } = Sum.inr { asIdeal := J', isPrime := hJ' }

Tactic:
exact False.elim (hI.ne_top h.left)

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
f : R
I : PrimeSpectrum R
⊢ I ∈ (zeroLocus {f})ᶜ ↔ f ∉ I.asIdeal

Tactic:
by
  rw [Set.mem_compl_iff, mem_zeroLocus, Set.singleton_subset_iff]; rfl

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
⊢ (∀ (x : S), IsAlgebraic R x) → ∀ (x : K), IsAlgebraic R x

Tactic:
intro h x
    let := MulActionWithZero.nontrivial S K
    let := FractionRing.liftAlgebra R K
    have := FractionRing.isScalarTower_liftAlgebra R K
    rw [IsFractionRing.isAlgebraic_iff R (FractionRing R) K, isAlgebraic_iff_isIntegral]
    obtain ⟨a : S, b, ha, rfl⟩ := div_surjective S x
    obtain ⟨f, hf₁, hf₂⟩ := h b
    rw [div_eq_mul_inv]
    refine .mul ?_ (.inv ?_) <;> exact isAlgebraic_iff_isIntegral.mp <|
      (h _).algebraMap.extendScalars (FaithfulSMul.algebraMap_injective R _)

Goal state after:
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
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
⊢ Algebra.IsAlgebraic R S ↔ Algebra.IsAlgebraic R K

Tactic:
simp only [Algebra.isAlgebraic_def]
  constructor
  · intro h x
    let := MulActionWithZero.nontrivial S K
    let := FractionRing.liftAlgebra R K
    have := FractionRing.isScalarTower_liftAlgebra R K
    rw [IsFractionRing.isAlgebraic_iff R (FractionRing R) K, isAlgebraic_iff_isIntegral]
    obtain ⟨a : S, b, ha, rfl⟩ := div_surjective S x
    obtain ⟨f, hf₁, hf₂⟩ := h b
    rw [div_eq_mul_inv]
    refine .mul ?_ (.inv ?_) <;> exact isAlgebraic_iff_isIntegral.mp <|
      (h _).algebraMap.extendScalars (FaithfulSMul.algebraMap_injective R _)
  · intro h x
    obtain ⟨f, hf₁, hf₂⟩ := h (algebraMap S K x)
    use f, hf₁
    rw [Polynomial.aeval_algebraMap_apply] at hf₂
    exact
      (injective_iff_map_eq_zero (algebraMap S K)).1 (FaithfulSMul.algebraMap_injective _ _) _
        hf₂

Goal state after:
Module: Mathlib.RingTheory.LocalRing.ResidueField.Ideal

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
I : Ideal R
inst✝¹ : I.IsPrime
J : Ideal S
inst✝ : J.IsPrime
f : R →+* S
hf : I = comap f J
r : R
⊢ (map I J f hf) ((algebraMap R I.ResidueField) r) = (algebraMap S J.ResidueField) (f r)

Tactic:
rw [IsScalarTower.algebraMap_apply R (Localization.AtPrime I)]
  simp [IsLocalRing.ResidueField.map_residue, Localization.localRingHom_to_map]
  rfl

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✝ : FaithfullyFlat A B
⊢ ∀ {m₁ m₂ : A}, (∀ (a : B), m₁ • a = m₂ • a) → m₁ = m₂

Tactic:
intro a₁ a₂ ha

Goal state after:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : FaithfullyFlat A B
a₁ a₂ : A
ha : ∀ (a : B), a₁ • a = a₂ • a
⊢ a₁ = a₂
Module: Mathlib.RingTheory.KrullDimension.Basic

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

Tactic:
by
  simp_rw [Ring.KrullDimLE, Order.krullDimLE_iff, Nat.cast_zero,
    Order.krullDim_nonpos_iff_forall_isMax,
    (PrimeSpectrum.equivSubtype R).forall_congr_left, Subtype.forall, PrimeSpectrum.isMax_iff]
  rfl

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
I : Ideal S
⊢ comap f '' zeroLocus ↑I = zeroLocus ↑(Ideal.comap f I)

Tactic:
by
  simp only [Set.ext_iff, Set.mem_image, mem_zeroLocus, SetLike.coe_subset_coe]
  refine fun p => ⟨?_, fun h_I_p => ?_⟩
  · rintro ⟨p, hp, rfl⟩ a ha
    exact hp ha
  · 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 b : { a // IsIdempotentElem a }
⊢ ↑⟨1 - ↑a * (1 - ↑b), ⋯⟩ = ↑(b ⊔ ⟨1 - ↑a, ⋯⟩)

Tactic:
simp_rw [(· ⊔ ·), SemilatticeSup.sup,
    add_comm b.1, add_sub_assoc, mul_sub, mul_one, sub_sub_cancel, sub_add, mul_comm]

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

Goal state before:
pp: case mpr
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
⊢ J ∈ comap f '' I.minimalPrimes → J ∈ (comap f I).minimalPrimes

Tactic:
rintro ⟨J, hJ, rfl⟩
    exact Ideal.minimalPrimes_comap_of_surjective hf hJ

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : CompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
eq_sInf : sInf = InfSet.sInf
x✝ : Set α
⊢ IsGLB x✝ (sInf x✝)

Tactic:
by simp +instances only [eq_le, eq_sInf, isGLB_sInf]

Goal state after:
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
J : Ideal R
max : J.IsMaximal
le : I.asIdeal ≤ J
r : R
hr : (toPiLocalization R) r = Function.update 0 { asIdeal := J, isPrime := ⋯ } 1
h : ¬I.asIdeal.IsMaximal
hJ : (algebraMap R (Localization { asIdeal := J, isPrime := ⋯ }.asIdeal.primeCompl)) r = 1
hI✝ : (algebraMap R (Localization I.asIdeal.primeCompl)) r = Function.update 0 { asIdeal := J, isPrime := ⋯ } 1 I
hI : 1 = 0 I
⊢ False

Tactic:
exact one_ne_zero hI

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

Goal state before:
pp: α : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : IndiscreteTopology α
U : Opens α
⊢ ↑U = ∅ ∨ U = ⊤

Tactic:
← coe_eq_univ,

Goal state after:
α : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : IndiscreteTopology α
U : Opens α
⊢ ↑U = ∅ ∨ ↑U = univ
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
⊢ IsLocallyClosed s ↔ ∃ s', IsLocallyClosed s' ∧ s' ∩ range f = f '' s

Tactic:
by
  simp_rw [hf.isInducing.isLocallyClosed_iff,
    ← (image_injective.mpr hf.injective).eq_iff, 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:
rw [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.QuasiSeparated

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

Tactic:
let b := { t ∈ s | IsClosed t }

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

Goal state before:
pp: case a
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PrespectralSpace X
U : Opens X
⊢ (fun I ↦ ⨆ U ∈ I, U.toOpens) ((fun U ↦ { carrier := {V | ↑V ⊆ ↑U}, lower' := ⋯, nonempty' := ⋯, directed' := ⋯ }) U) ≤
    U

Tactic:
simp only [iSup_le_iff]
      exact fun _ ↦ id

Goal state after:
Module: Mathlib.Topology.Spectral.Prespectral

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PrespectralSpace X
U V : Opens X
H : ∀ (W : CompactOpens X), ↑W ⊆ ↑U → ↑W ⊆ ↑V
x : X
hxU : x ∈ U
⊢ x ∈ V

Tactic:
obtain ⟨W, ⟨h₁, h₂⟩, hxW, hWU⟩ := isTopologicalBasis.exists_subset_of_mem_open hxU U.2

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PrespectralSpace X
U V : Opens X
H : ∀ (W : CompactOpens X), ↑W ⊆ ↑U → ↑W ⊆ ↑V
x : X
hxU : x ∈ U
W : Set X
h₁ : IsOpen[inst✝²] W
h₂ : IsCompact W
hxW : x ∈ W
hWU : W ⊆ ↑U
⊢ x ∈ V
Module: Mathlib.Topology.Constructible

Goal state before:
pp: case refine_1
X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
hs : IsRetrocompact s
t : Set X
htopen : IsOpen[inst✝] t
htcomp : IsCompact t
⊢ IsCompact (t ∩ {x | x ∈ s})

Tactic:
ofPred_mem_eq,

Goal state after:
case refine_1
X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
hs : IsRetrocompact s
t : Set X
htopen : IsOpen[inst✝] t
htcomp : IsCompact t
⊢ IsCompact (t ∩ s)
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
⊢ IsRetrocompact s ↔ IsSpectralMap Subtype.val

Tactic:
by
  refine ⟨fun hs ↦ ⟨continuous_subtype_val, fun t htopen htcomp ↦ ?_⟩, fun hs t htcomp htopen ↦ ?_⟩
  · rw [IsEmbedding.subtypeVal.isCompact_iff, image_preimage_eq_inter_range,
      Subtype.range_coe_subtype, ofPred_mem_eq, inter_comm]
    exact hs htcomp htopen
  · simpa using (hs.isCompact_preimage_of_isOpen htopen htcomp).image continuous_subtype_val

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hs : IsRetrocompact s
hfemb : IsEmbedding f
hfcomp : IsRetrocompact (range f)
⊢ IsRetrocompact (f '' s)

Tactic:
by
  rintro U hUcomp hUopen
  rw [← image_inter_preimage, ← hfemb.isCompact_iff]
  refine hs ?_ <| hUopen.preimage hfemb.continuous
  rw [hfemb.isCompact_iff, image_preimage_eq_inter_range, inter_comm]
  exact hfcomp hUcomp hUopen

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
Z : Set (PrimeSpectrum R)
⊢ IsOpen Zᶜ ↔ ∃ s, Z = zeroLocus s

Tactic:
isOpen_iff,

Goal state after:
R : Type u
inst✝ : CommSemiring R
Z : Set (PrimeSpectrum R)
⊢ (∃ s, Zᶜᶜ = zeroLocus s) ↔ ∃ s, Z = zeroLocus s
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case mp
R : Type u
S : Type v
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
s : Set S
⊢ ∃ a, zeroLocus (⇑(algebraMap R S) '' a) = zeroLocus s

Tactic:
refine ⟨(Ideal.span s).comap (algebraMap R S), ?_⟩

Goal state after:
case mp
R : Type u
S : Type v
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
s : Set S
⊢ zeroLocus (⇑(algebraMap R S) '' ↑(Ideal.comap (algebraMap R S) (Ideal.span s))) = zeroLocus s
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case refine_1
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
⊢ Continuous (⇑(primeSpectrumProd R S).symm ∘ Sum.inl) ∧ Continuous (⇑(primeSpectrumProd R S).symm ∘ Sum.inr)

Tactic:
simp only [Function.comp_def, primeSpectrumProd_symm_inl, primeSpectrumProd_symm_inr]

Goal state after:
case refine_1
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
⊢ (Continuous fun x ↦ comap (RingHom.fst R S) x) ∧ Continuous fun x ↦ comap (RingHom.snd R S) x
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
g : G
⊢ g ^ exponent G = 1

Tactic:
by_cases h : ExponentExists G

Goal state after:
case pos
G : Type u
inst✝ : Monoid G
g : G
h : ExponentExists G
⊢ g ^ exponent G = 1

case neg
G : Type u
inst✝ : Monoid G
g : G
h : ¬ExponentExists G
⊢ g ^ exponent G = 1
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))
x : (i : ι) → R i
hx : x ∈ RingHom.ker (Pi.evalRingHom R i)
⊢ x ∈ p.asIdeal

Tactic:
rw [RingHom.mem_ker, Pi.evalRingHom_apply] at hx

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))
x : (i : ι) → R i
hx : x i = 0
⊢ x ∈ p.asIdeal
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case inr.mp
G : Type u
inst✝ : Monoid G
n : ℕ
hpos : n > 0
h : exponent G ∣ n
⊢ ∀ (g : G), g ^ n = 1

Tactic:
g

Goal state after:
case inr.mp
G : Type u
inst✝ : Monoid G
n : ℕ
hpos : n > 0
h : exponent G ∣ n
g : G
⊢ g ^ n = 1