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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
s : Multiset R
g : R[X]
hg : g.Monic
hg' : g.Splits
⊢ (Multiset.map (fun ij ↦ ij.1 - ij.2) (g.roots ×ˢ s)).prod =
    (Multiset.map (fun ij ↦ -1 * (ij.1 - ij.2)) (s ×ˢ g.roots)).prod

pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
s : Multiset R
g : R[X]
hg : g.Monic
hg' : g.Splits
⊢ (Multiset.map (fun ij ↦ -1 * (ij.1 - ij.2)) (s ×ˢ g.roots)).prod =
    (-1) ^ (s.card * g.roots.card) * (Multiset.map (fun x ↦ eval x g) s).prod

Tactic:
· rw [← Multiset.map_swap_product, Multiset.map_map]; simp

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
s : Multiset R
g : R[X]
hg : g.Monic
hg' : g.Splits
⊢ (Multiset.map (fun ij ↦ -1 * (ij.1 - ij.2)) (s ×ˢ g.roots)).prod =
    (-1) ^ (s.card * g.roots.card) * (Multiset.map (fun x ↦ eval x g) s).prod
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
fl : FaithfullyFlat R M
N : Type u_1
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Nontrivial N
⊢ Nontrivial (N ⊗[R] M)

Tactic:
obtain ⟨n, hn⟩ := nontrivial_iff_exists_ne (0 : N) |>.1 inferInstance

Goal state after:
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
fl : FaithfullyFlat R M
N : Type u_1
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Nontrivial N
n : N
hn : n ≠ 0
⊢ Nontrivial (N ⊗[R] M)
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: case h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
M : Ideal R
hgt : ∀ J > M, ∃ Z, (Multiset.map asIdeal Z).prod ≤ J
h_prM : ¬M.IsPrime
htop : ¬M = ⊤
lt_add : ∀ z ∉ M, M < M + R ∙ z
x : R
hx : x ∉ M
y : R
hy : y ∉ M
hxy : x * y ∈ M
Wx : Multiset (PrimeSpectrum R)
h_Wx : (Multiset.map asIdeal Wx).prod ≤ M + R ∙ x
Wy : Multiset (PrimeSpectrum R)
h_Wy : (Multiset.map asIdeal Wy).prod ≤ M + R ∙ y
⊢ (Multiset.map asIdeal Wx + Multiset.map asIdeal Wy).prod ≤ M

Tactic:
Multiset.prod_add

Goal state after:
case h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
M : Ideal R
hgt : ∀ J > M, ∃ Z, (Multiset.map asIdeal Z).prod ≤ J
h_prM : ¬M.IsPrime
htop : ¬M = ⊤
lt_add : ∀ z ∉ M, M < M + R ∙ z
x : R
hx : x ∉ M
y : R
hy : y ∉ M
hxy : x * y ∈ M
Wx : Multiset (PrimeSpectrum R)
h_Wx : (Multiset.map asIdeal Wx).prod ≤ M + R ∙ x
Wy : Multiset (PrimeSpectrum R)
h_Wy : (Multiset.map asIdeal Wy).prod ≤ M + R ∙ y
⊢ (Multiset.map asIdeal Wx).prod * (Multiset.map asIdeal Wy).prod ≤ M
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: case right
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 : K), IsAlgebraic R x
x : S
f : R[X]
hf₁ : f ≠ 0
hf₂ : (algebraMap S K) ((aeval x) f) = 0
⊢ (aeval x) f = 0

Tactic:
exact
      (injective_iff_map_eq_zero (algebraMap S K)).1 (FaithfulSMul.algebraMap_injective _ _) _
        hf₂

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
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 : y' * (algebraMap R S) z = y * ↑z'
injRS : Function.Injective ⇑(algebraMap R S)
hz0' : (algebraMap R S) z ∈ S⁰
⊢ ↑z' * y = ↑⟨(algebraMap R S) z, hz0'⟩ * y'

Tactic:
rw [mul_comm _ y, mul_comm _ y', yz_eq]

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

Goal state before:
pp: case h
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
M : Ideal A
hgt : ∀ J > M, J ≠ ⊥ → ∃ Z, (Multiset.map asIdeal Z).prod ≤ J ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
h_nzI : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬M.IsPrime
x : A
hx : x ∉ M
y : A
hy : y ∉ M
h_xy : x * y ∈ M
lt_add : ∀ z ∉ M, M < M + A ∙ z
Wx : Multiset (PrimeSpectrum A)
h_Wx_le : (Multiset.map asIdeal Wx).prod ≤ M + A ∙ x
h_Wx_ne✝ : (Multiset.map asIdeal Wx).prod ≠ ⊥
Wy : Multiset (PrimeSpectrum A)
h_Wy_le : (Multiset.map asIdeal Wy).prod ≤ M + A ∙ y
h_Wx_ne : (Multiset.map asIdeal Wy).prod ≠ ⊥
⊢ (Multiset.map asIdeal Wx + Multiset.map asIdeal Wy).prod ≤ M ∧
    (Multiset.map asIdeal Wx + Multiset.map asIdeal Wy).prod ≠ ⊥

Tactic:
Multiset.prod_add

Goal state after:
case h
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
M : Ideal A
hgt : ∀ J > M, J ≠ ⊥ → ∃ Z, (Multiset.map asIdeal Z).prod ≤ J ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
h_nzI : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬M.IsPrime
x : A
hx : x ∉ M
y : A
hy : y ∉ M
h_xy : x * y ∈ M
lt_add : ∀ z ∉ M, M < M + A ∙ z
Wx : Multiset (PrimeSpectrum A)
h_Wx_le : (Multiset.map asIdeal Wx).prod ≤ M + A ∙ x
h_Wx_ne✝ : (Multiset.map asIdeal Wx).prod ≠ ⊥
Wy : Multiset (PrimeSpectrum A)
h_Wy_le : (Multiset.map asIdeal Wy).prod ≤ M + A ∙ y
h_Wx_ne : (Multiset.map asIdeal Wy).prod ≠ ⊥
⊢ (Multiset.map asIdeal Wx).prod * (Multiset.map asIdeal Wy).prod ≤ M ∧
    (Multiset.map asIdeal Wx).prod * (Multiset.map asIdeal Wy).prod ≠ ⊥
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocSemiring R
a b c : R
mul : a * b = c * a
add_ab : a + b = 1
add_ac : a + c = 1
⊢ (a + c) * b = c * (a + b)

Tactic:
add_mul,

Goal state after:
R : Type u_1
inst✝ : NonAssocSemiring R
a b c : R
mul : a * b = c * a
add_ab : a + b = 1
add_ac : a + c = 1
⊢ a * b + c * b = c * (a + b)
Module: Mathlib.Algebra.Order.Ring.Idempotent

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

Tactic:
add_mul,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a✝ b✝ a b : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
⊢ (↑a).1 * ((↑a).2 * (↑b).2) + (↑a).2 * (↑b).1 * ((↑a).2 * (↑b).2) = 0
Module: Mathlib.RingTheory.LocalRing.ResidueField.Ideal

Goal state before:
pp: case h
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R A
inst✝¹ : Algebra R B
I : Ideal R
inst✝ : I.IsPrime
x y : R
e : (Ideal.Quotient.mk I) x = (Ideal.Quotient.mk I) y
⊢ ↑1 * (Ideal.Quotient.mk I) x = ↑1 * (Ideal.Quotient.mk I) y

Tactic:
simp [e]

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

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

Tactic:
add_mul,

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

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

Tactic:
add_mul,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a✝ b✝ a b c : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
⊢ (↑a).2 * (↑b).2 + ((↑a).1 * ((↑a).2 * (↑c).2) + (↑a).2 * (↑b).1 * ((↑a).2 * (↑c).2)) =
    (↑a).2 * ((↑b).2 + (↑b).1 * (↑c).2)
Module: Mathlib.RingTheory.Spectrum.Prime.RingHom

Goal state before:
pp: ι : Type u_3
R : ι → Type u_4
inst✝¹ : (i : ι) → CommRing (R i)
inst✝ : _root_.Finite ι
p : PrimeSpectrum ((i : ι) → R i)
val✝ : Fintype ι
e : ι → (i : ι) → R i := fun i ↦ Function.update 1 i 0
j : ι
⊢ e j j = 0

Tactic:
simp [e]

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 }
⊢ ↑b * ↑⟨↑a + ↑b - ↑a * ↑b, ⋯⟩ = ↑b

Tactic:
simp_rw [mul_sub, mul_add]; rw [← mul_assoc, mul_right_comm, b.2, add_sub_cancel_left]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b c : { a // IsIdempotentElem a }
hac : a ≤ c
hbc : b ≤ c
⊢ (↑a + ↑b) * ↑c - ↑a * ↑b * ↑c = ↑a + ↑b - ↑a * ↑b

Tactic:
add_mul,

Goal state after:
R : Type u_1
inst✝ : CommRing R
a b c : { a // IsIdempotentElem a }
hac : a ≤ c
hbc : b ≤ c
⊢ ↑a * ↑c + ↑b * ↑c - ↑a * ↑b * ↑c = ↑a + ↑b - ↑a * ↑b
Module: Mathlib.Topology.Compactness.Bases

Goal state before:
pp: X : Type u_1
ι : Type u_2
inst✝ : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
U : Set X
hUc : IsCompact U
hUo : IsOpen U
Y : Type u_1
f' : Y → ι
e : U = ⋃ i, (b ∘ f') i
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
t : Finset Y
ht : U ⊆ ⋃ i ∈ t, (b ∘ f') i
⊢ ∃ s, s.Finite ∧ U = ⋃ i ∈ s, b i

Tactic:
classical
  refine ⟨t.image f', Set.toFinite _, le_antisymm ?_ ?_⟩
  · refine Set.Subset.trans ht ?_
    simp only [Set.iUnion_subset_iff]
    intro i hi
    simpa using subset_iUnion₂ (s := fun i _ => b (f' i)) i hi
  · apply Set.iUnion₂_subset
    rintro i hi
    obtain ⟨j, -, rfl⟩ := Finset.mem_image.mp hi
    rw [e]
    exact Set.subset_iUnion (b ∘ f') j

Goal state after:
Module: Mathlib.Topology.LocallyClosed

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ s ⊆ coborder s

Tactic:
rw [coborder, subset_compl_iff_disjoint_right]
  exact disjoint_sdiff_self_right

Goal state after:
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:
rw [coborder, compl_eq_comm, compl_union, compl_compl, inter_comm]

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ closure[inst✝] s ∩ sᶜ = closure[inst✝] s \ s
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
H : IsClosedMap f
s : Set β
t : Set ↑(f ⁻¹' s)
u : Set α
hu : IsClosed[inst✝¹] u
e : Subtype.val ⁻¹' u = t
⊢ Subtype.val ⁻¹' f '' u = s.restrictPreimage f '' t

Tactic:
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 : α → β
H : IsOpenMap f
s : Set β
t : Set ↑(f ⁻¹' s)
u : Set α
hu : IsOpen[inst✝¹] u
e : Subtype.val ⁻¹' u = t
⊢ Subtype.val ⁻¹' f '' u = s.restrictPreimage f '' t

Tactic:
simp [← e, image_restrictPreimage]

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

Goal state before:
pp: case mpr
α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
h : ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U' ∈ B, x ∈ U' ∧ U' ≤ U
⊢ IsBasis B

Tactic:
· refine isTopologicalBasis_of_isOpen_of_nhds ?_ ?_
    · rintro sU ⟨U, -, rfl⟩
      exact U.2
    · intro x sU hx hsU
      rcases @h ⟨sU, hsU⟩ x hx with ⟨V, hV, H⟩
      exact ⟨V, ⟨V, hV, rfl⟩, H⟩

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
B : Set (Opens β)
H : IsBasis B
f : α → β
h : IsInducing f
⊢ IsBasis {x | ∃ U ∈ B, { carrier := f ⁻¹' ↑U, is_open' := ⋯ } = x}

Tactic:
by
  simp only [IsBasis] at H ⊢
  convert! H.isInducing h
  ext; simp

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

Goal state before:
pp: case mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
g : SpectralMap α β
toFun✝ : α → β
spectral'✝ : IsSpectralMap toFun✝
h : { toFun := toFun✝, spectral' := spectral'✝ }.toFun = g.toFun
⊢ { toFun := toFun✝, spectral' := spectral'✝ } = g

Tactic:
cases g

Goal state after:
case mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
toFun✝¹ : α → β
spectral'✝¹ : IsSpectralMap toFun✝¹
toFun✝ : α → β
spectral'✝ : IsSpectralMap toFun✝
h : { toFun := toFun✝¹, spectral' := spectral'✝¹ }.toFun = { toFun := toFun✝, spectral' := spectral'✝ }.toFun
⊢ { toFun := toFun✝¹, spectral' := spectral'✝¹ } = { toFun := toFun✝, spectral' := spectral'✝ }
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
⊢ { toFun := fun U ↦ { carrier := {V | ↑V ⊆ ↑U}, lower' := ⋯, nonempty' := ⋯, directed' := ⋯ },
          invFun := fun I ↦ ⨆ U ∈ I, U.toOpens, left_inv := ⋯, right_inv := ⋯ }
        U ≤
      { toFun := fun U ↦ { carrier := {V | ↑V ⊆ ↑U}, lower' := ⋯, nonempty' := ⋯, directed' := ⋯ },
          invFun := fun I ↦ ⨆ U ∈ I, U.toOpens, left_inv := ⋯, right_inv := ⋯ }
        V ↔
    U ≤ V

Tactic:
change (∀ (W : CompactOpens X), (W : Set X) ⊆ U → (W : Set X) ⊆ V) ↔ U ≤ V

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PrespectralSpace X
U V : Opens X
⊢ (∀ (W : CompactOpens X), ↑W ⊆ ↑U → ↑W ⊆ ↑V) ↔ U ≤ V
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: case inr.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)
a : Set (Set α) := {t | t ∈ s ∧ IsOpen[inst✝¹] t}
b : Set (Set α) := {t | t ∈ s ∧ IsClosed[inst✝¹] t}
heq : s = a ∪ b
t : Set α
ht : t ∈ s
hno : ¬IsOpen[inst✝¹] t
ha : a.Nonempty
⊢ IsCompact (⋂₀ a ∩ ⋂₀ b)

Tactic:
· apply IsCompact.inter_right
      · apply this (hf.subset (by grind)) ha <;> grind
      · exact isClosed_sInter (by grind)

Goal state after:
Module: Mathlib.Topology.Constructible

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

Tactic:
refine ⟨fun hs ↦ ⟨continuous_subtype_val, fun t htopen htcomp ↦ ?_⟩, fun hs t htcomp htopen ↦ ?_⟩

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 (Subtype.val ⁻¹' t)

case refine_2
X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
hs : IsSpectralMap Subtype.val
t : Set X
htcomp : IsCompact t
htopen : IsOpen[inst✝] t
⊢ IsCompact (s ∩ t)
Module: Mathlib.Topology.Sober

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

Tactic:
ext x
  rw [genericPoints, irreducibleComponents_eq_singleton]
  exact ⟨((genericPoint_spec α).eq · |>.symm), (· ▸ genericPoint_spec α)⟩

Goal state after:
Module: Mathlib.RingTheory.Derivation.ToSquareZero

Goal state before:
pp: case refine_1
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hI : I ^ 2 = ⊥
f : A →ₐ[R] B
e : (Ideal.Quotient.mkₐ R I).comp f = IsScalarTower.toAlgHom R A (B ⧸ I)
x✝ : A
⊢ ((Ideal.Quotient.mkₐ R I).comp f) x✝ = ((Ideal.Quotient.mkₐ R I).comp (IsScalarTower.toAlgHom R A B)) x✝

Tactic:
simp [e]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
hg : Function.Bijective ⇑g
hf : (g.comp f).Flat
⊢ f.Flat

Tactic:
let e := RingEquiv.ofBijective g hg

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
hg : Function.Bijective ⇑g
hf : (g.comp f).Flat
e : S ≃+* T := RingEquiv.ofBijective g hg
⊢ f.Flat
Module: Mathlib.RingTheory.RingHom.Flat

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : T →+* R
hg : Function.Bijective ⇑g
hf : (f.comp g).Flat
⊢ f.Flat

Tactic:
let e := RingEquiv.ofBijective g hg

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : T →+* R
hg : Function.Bijective ⇑g
hf : (f.comp g).Flat
e : T ≃+* R := RingEquiv.ofBijective g hg
⊢ f.Flat
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s t : Set (PrimeSpectrum R)
hs : IsClosed s
ht : IsClosed t
⊢ s ⊆ t ∧ ¬t ⊆ s ↔ vanishingIdeal t < vanishingIdeal s

Tactic:
vanishingIdeal_anti_mono_iff hs,

Goal state after:
R : Type u
inst✝ : CommSemiring R
s t : Set (PrimeSpectrum R)
hs : IsClosed s
ht : IsClosed t
⊢ s ⊆ t ∧ ¬vanishingIdeal s ≤ vanishingIdeal t ↔ vanishingIdeal t < vanishingIdeal s
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

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

Tactic:
simp_rw [← SetLike.mem_coe, ← Set.singleton_subset_iff, ← Ideal.span_le, ←
          Ideal.span_singleton_mul_span_singleton]
        refine fun h x y h' => h _ _ ?_
        rw [← hI.radical_le_iff] at h' ⊢
        simpa only [Ideal.radical_inf, Ideal.radical_mul] using h'

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

Goal state before:
pp: case succ.inr
R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring A
inst✝³ : AddCommMonoid M
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
a : A
n : ℕ
ihn : D (a ^ n) = n • a ^ (n - 1) • D a
hpos : 0 < n
⊢ D (a ^ (n + 1)) = (n + 1) • a ^ (n + 1 - 1) • D a

Tactic:
· have : a * a ^ (n - 1) = a ^ n := by rw [← pow_succ', Nat.sub_add_cancel hpos]
      simp only [pow_succ', leibniz, ihn, smul_comm a n (_ : M), smul_smul a, add_smul, this,
        Nat.add_succ_sub_one, add_zero, one_nsmul]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring A
inst✝³ : AddCommMonoid M
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
P : R[X]
x : A
⊢ D ((aeval x) P) = (aeval x) (derivative P) • D x

Tactic:
induction P using Polynomial.induction_on
  · simp
  · simp [add_smul, *]
  · simp [mul_smul, ← Nat.cast_smul_eq_nsmul A]

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
f g : R
inst✝¹ : Algebra R S
inst✝ : IsLocalization.Away f S
⊢ (∃ n, f ^ n ∈ Ideal.span {g}) ↔ IsUnit ((algebraMap R S) g)

Tactic:
Ideal.mem_span_singleton,

Goal state after:
R : Type u
S : Type v
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
f g : R
inst✝¹ : Algebra R S
inst✝ : IsLocalization.Away f S
⊢ (∃ n, g ∣ f ^ n) ↔ IsUnit ((algebraMap R S) g)
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
m : ℕ
hm : Fintype.card α = n.gcd (Fintype.card α) * m
hm0 : 0 < m
⊢ orderOf g / (orderOf g).gcd (Fintype.card α / n.gcd (Fintype.card α)) ≤ n

Tactic:
orderOf_eq_card_of_forall_mem_zpowers hg,

Goal state after:
α : Type u_1
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
m : ℕ
hm : Fintype.card α = n.gcd (Fintype.card α) * m
hm0 : 0 < m
⊢ Nat.card α / (Nat.card α).gcd (Fintype.card α / n.gcd (Fintype.card α)) ≤ n
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: G : Type u_2
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsCyclic G
g : G
hg : ∀ (x : G), x ∈ zpowers g
a b : ZMod (Nat.card G)
h : a.val ≡ b.val [MOD orderOf g]
⊢ a = b

Tactic:
orderOf_eq_card_of_forall_mem_zpowers hg,

Goal state after:
G : Type u_2
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsCyclic G
g : G
hg : ∀ (x : G), x ∈ zpowers g
a b : ZMod (Nat.card G)
h : a.val ≡ b.val [MOD Nat.card G]
⊢ a = b
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
e f : R
⊢ f * e = 0 ∧ f + e = 1 ∧ s = ↑(basicOpen f) ↔ e * f = 0 ∧ e + f = 1 ∧ s = zeroLocus {e}

Tactic:
rw [mul_comm, add_comm, ← and_assoc, ← and_assoc, and_congr_right]

Goal state after:
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
e f : R
⊢ e * f = 0 ∧ e + f = 1 → (s = ↑(basicOpen f) ↔ s = zeroLocus {e})
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.IsIntegral
s : Set (PrimeSpectrum S)
hs : IsClosed s
⊢ StableUnderSpecialization (comap f '' s)

Tactic:
rintro _ y e ⟨x, hx, rfl⟩

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.IsIntegral
s : Set (PrimeSpectrum S)
hs : IsClosed s
y : PrimeSpectrum R
x : PrimeSpectrum S
hx : x ∈ s
e : comap f x ⤳ y
⊢ y ∈ comap f '' s
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case a
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal S
⊢ closure (comap f '' zeroLocus ↑I) ⊆ zeroLocus ↑(Ideal.comap f I)

Tactic:
rw [(isClosed_zeroLocus _).closure_subset_iff, Set.image_subset_iff, preimage_comap_zeroLocus]
    exact zeroLocus_anti_mono (Set.image_preimage_subset _ _)

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: n : ℕ
G : Type u_2
inst✝¹ : AddCommGroup G
inst✝ : Module (ZMod n) G
x✝ : G
⊢ Multiplicative.ofAdd x✝ ^ n ^ 1 = 1

Tactic:
by simp [← ofAdd_nsmul, ZModModule.char_nsmul_eq_zero]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I : Ideal R
| zeroLocus ↑I ∈ irreducibleComponents (PrimeSpectrum R)

Tactic:
← (isClosed_zeroLocus _).closure_eq

Goal state after:
R : Type u
inst✝ : CommSemiring R
I : Ideal R
| closure (zeroLocus ↑I) ∈ irreducibleComponents (PrimeSpectrum R)
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_2
inst✝³ : Infinite G
inst✝² : CommGroup G
inst✝¹ : PartialOrder G
inst✝ : IsOrderedMonoid G
g : G
hg : zpowers g = ⊤
hg1 : 1 < g
x y : Multiplicative ℤ
⊢ x < y → (intEquivOfZPowersEqTop g hg) x < (intEquivOfZPowersEqTop g hg) y

Tactic:
hxy

Goal state after:
G : Type u_2
inst✝³ : Infinite G
inst✝² : CommGroup G
inst✝¹ : PartialOrder G
inst✝ : IsOrderedMonoid G
g : G
hg : zpowers g = ⊤
hg1 : 1 < g
x y : Multiplicative ℤ
hxy : x < y
⊢ (intEquivOfZPowersEqTop g hg) x < (intEquivOfZPowersEqTop g hg) y
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_2
inst✝³ : Infinite G
inst✝² : CommGroup G
inst✝¹ : PartialOrder G
inst✝ : IsOrderedMonoid G
g : G
hg : zpowers g = ⊤
hg1 : 1 < g
x y : Multiplicative ℤ
hxy : x < y
⊢ (intEquivOfZPowersEqTop g hg) x < (intEquivOfZPowersEqTop g hg) y

Tactic:
simp only [intEquivOfZPowersEqTop, MulEquiv.ofBijective_apply, zpowersHom_apply]

Goal state after:
G : Type u_2
inst✝³ : Infinite G
inst✝² : CommGroup G
inst✝¹ : PartialOrder G
inst✝ : IsOrderedMonoid G
g : G
hg : zpowers g = ⊤
hg1 : 1 < g
x y : Multiplicative ℤ
hxy : x < y
⊢ g ^ Multiplicative.toAdd x < g ^ Multiplicative.toAdd y