mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Localization.Integral

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

Tactic:
Algebra.smul_def,

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

Goal state before:
pp: case tmul
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Algebra R S
hf₂ : (algebraMap R T).SurjectiveOnStalks
J : Ideal T
hJ : J.IsPrime
x₁ : S
x₂ : T
y s : R
c : T
hs : c ∉ J
hc : (algebraMap R T) s ∉ J
e : c * (algebraMap R T) s * x₂ = c * (algebraMap R T) y
⊢ x₁ ⊗ₜ[R] (c * (algebraMap R T) y) = x₁ ⊗ₜ[R] (y • c)

Tactic:
Algebra.smul_def,

Goal state after:
case tmul
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Algebra R S
hf₂ : (algebraMap R T).SurjectiveOnStalks
J : Ideal T
hJ : J.IsPrime
x₁ : S
x₂ : T
y s : R
c : T
hs : c ∉ J
hc : (algebraMap R T) s ∉ J
e : c * (algebraMap R T) s * x₂ = c * (algebraMap R T) y
⊢ x₁ ⊗ₜ[R] (c * (algebraMap R T) y) = x₁ ⊗ₜ[R] ((algebraMap R T) y * c)
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: case add
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Algebra R S
hf₂ : (algebraMap R T).SurjectiveOnStalks
J : Ideal T
hJ : J.IsPrime
x₁ x₂ : S ⊗[R] T
t₁ : T
r₁ : R
a₁ : S
hr₁ : r₁ • t₁ ∉ J
e₁ : 1 ⊗ₜ[R] (r₁ • t₁) * x₁ = a₁ ⊗ₜ[R] t₁
t₂ : T
r₂ : R
a₂ : S
hr₂ : r₂ • t₂ ∉ J
e₂ : 1 ⊗ₜ[R] (r₂ • t₂) * x₂ = a₂ ⊗ₜ[R] t₂
this : (r₁ * r₂) • (t₁ * t₂) = r₁ • t₁ * r₂ • t₂
⊢ (1 * 1) ⊗ₜ[R] (r₁ • t₁ * r₂ • t₂) * (x₁ + x₂) = (r₂ • a₁ + r₁ • a₂) ⊗ₜ[R] (t₁ * t₂)

Tactic:
← Algebra.TensorProduct.tmul_mul_tmul,

Goal state after:
case add
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Algebra R S
hf₂ : (algebraMap R T).SurjectiveOnStalks
J : Ideal T
hJ : J.IsPrime
x₁ x₂ : S ⊗[R] T
t₁ : T
r₁ : R
a₁ : S
hr₁ : r₁ • t₁ ∉ J
e₁ : 1 ⊗ₜ[R] (r₁ • t₁) * x₁ = a₁ ⊗ₜ[R] t₁
t₂ : T
r₂ : R
a₂ : S
hr₂ : r₂ • t₂ ∉ J
e₂ : 1 ⊗ₜ[R] (r₂ • t₂) * x₂ = a₂ ⊗ₜ[R] t₂
this : (r₁ * r₂) • (t₁ * t₂) = r₁ • t₁ * r₂ • t₂
⊢ 1 ⊗ₜ[R] (r₁ • t₁) * 1 ⊗ₜ[R] (r₂ • t₂) * (x₁ + x₂) = (r₂ • a₁ + r₁ • a₂) ⊗ₜ[R] (t₁ * t₂)
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: case refine_1
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Algebra R S
hf : (algebraMap R T).SurjectiveOnStalks
g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom
J : Ideal (S ⊗[R] T)
hJ : J.IsPrime
x : S ⊗[R] T
t : T
r : R
a : S
ht : g (r • t) ∉ J
e : 1 ⊗ₜ[R] (r • t) * x = a ⊗ₜ[R] t
H : 1 ⊗ₜ[R] (algebraMap R T) r ∈ J
⊢ False

Tactic:
Algebra.smul_def,

Goal state after:
case refine_1
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Algebra R S
hf : (algebraMap R T).SurjectiveOnStalks
g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom
J : Ideal (S ⊗[R] T)
hJ : J.IsPrime
x : S ⊗[R] T
t : T
r : R
a : S
ht : g ((algebraMap R T) r * t) ∉ J
e : 1 ⊗ₜ[R] (r • t) * x = a ⊗ₜ[R] t
H : 1 ⊗ₜ[R] (algebraMap R T) r ∈ J
⊢ False
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✝³ : IsLocalRing A
inst✝² : IsLocalRing B
inst✝¹ : Flat A B
inst✝ : IsLocalHom (algebraMap A B)
m : Ideal A
hm : m.IsMaximal
eqt : Submodule.restrictScalars A (Ideal.map (algebraMap A B) (IsLocalRing.maximalIdeal A)) = ⊤
this :
  Submodule.restrictScalars A (Ideal.map (algebraMap A B) (IsLocalRing.maximalIdeal A)) ≤
    Submodule.restrictScalars A (IsLocalRing.maximalIdeal B)
⊢ False

Tactic:
eqt,

Goal state after:
A : Type u_1
B : Type u_2
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : IsLocalRing A
inst✝² : IsLocalRing B
inst✝¹ : Flat A B
inst✝ : IsLocalHom (algebraMap A B)
m : Ideal A
hm : m.IsMaximal
eqt : Submodule.restrictScalars A (Ideal.map (algebraMap A B) (IsLocalRing.maximalIdeal A)) = ⊤
this : ⊤ ≤ Submodule.restrictScalars A (IsLocalRing.maximalIdeal B)
⊢ False
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: case refine_3
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
⊢ (↑a).2 + (↑b).1 = 1

Tactic:
rw [add_comm, eq, b.2.2]

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

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

Tactic:
simp_rw [(· ⊔ ·), (·ᶜ),
    SemilatticeSup.sup, (IsIdempotentElem.of_mul_add a.2.1 a.2.2).2.eq, a.2.2]

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

Goal state before:
pp: case refine_2.refine_2
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
x x' : R
hx' : x' ∈ p.asIdeal
heq : f x' = f x
⊢ x' - x ∈ ker f

Tactic:
mem_ker,

Goal state after:
case refine_2.refine_2
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
x x' : R
hx' : x' ∈ p.asIdeal
heq : f x' = f x
⊢ f (x' - x) = 0
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a : { a // IsIdempotentElem a }
⊢ 1 - (↑a - ↑a * ↑a) = ↑⊤

Tactic:
rw [a.2, sub_self, sub_zero]

Goal state after:
R : Type u_1
inst✝ : CommRing R
a : { a // IsIdempotentElem a }
⊢ 1 = ↑⊤
Module: Mathlib.Topology.Compactness.Bases

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
b : Set (Set X)
hb : IsTopologicalBasis b
U : Set X
hUc : IsCompact U
hUo : IsOpen U
⊢ ∃ s, U = ⋃₀ (Subtype.val '' ↑s)

Tactic:
have hb' : b = range (fun i ↦ i : b → Set X) := by simp

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
b : Set (Set X)
hb : IsTopologicalBasis b
U : Set X
hUc : IsCompact U
hUo : IsOpen U
hb' : b = range fun i ↦ ↑i
⊢ ∃ s, U = ⋃₀ (Subtype.val '' ↑s)
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : GeneralizedHeytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
himp : α → α → α
eq_himp : himp = HImp.himp
⊢ ∀ (x y : α), x ≤ y ↔ x ≤ y

Tactic:
rw [← eq_le]

Goal state after:
α : Type u
c : GeneralizedHeytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
himp : α → α → α
eq_himp : himp = HImp.himp
⊢ ∀ (x y : α), x ≤ y ↔ le x y
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
r r' : R
eq : (toPiLocalization R) r = (toPiLocalization R) r'
ne : ¬1 * r = 1 * r'
I : Ideal R
mI : I.IsMaximal
hI : Module.eqIdeal R r r' ≤ I
s : ↥I.primeCompl
hs : ↑s * r = ↑s * r'
⊢ False

Tactic:
exact s.2 (hI hs)

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : GeneralizedCoheytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
sdiff : α → α → α
eq_sdiff : sdiff = SDiff.sdiff
⊢ ∀ (x y : α), x ≤ y ↔ x ≤ y

Tactic:
rw [← eq_le]

Goal state after:
α : Type u
c : GeneralizedCoheytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
sdiff : α → α → α
eq_sdiff : sdiff = SDiff.sdiff
⊢ ∀ (x y : α), x ≤ y ↔ le x y
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : HeytingAlgebra α
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
himp : α → α → α
eq_himp : himp = HImp.himp
compl : α → α
eq_compl : compl = Compl.compl
⊢ ∀ (x y : α), x ≤ y ↔ x ≤ y

Tactic:
rw [← eq_le]

Goal state after:
α : Type u
c : HeytingAlgebra α
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
himp : α → α → α
eq_himp : himp = HImp.himp
compl : α → α
eq_compl : compl = Compl.compl
⊢ ∀ (x y : α), x ≤ y ↔ le x y
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : HeytingAlgebra α
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
himp : α → α → α
eq_himp : himp = HImp.himp
compl : α → α
eq_compl : compl = Compl.compl
⊢ ∀ (a : α), a ⇨ ⊥ = compl a

Tactic:
simp +instances [eq_le, eq_himp, eq_bot, eq_compl]

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : CoheytingAlgebra α
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
sdiff : α → α → α
eq_sdiff : sdiff = SDiff.sdiff
hnot : α → α
eq_hnot : hnot = HNot.hnot
⊢ ∀ (x y : α), x ≤ y ↔ x ≤ y

Tactic:
rw [← eq_le]

Goal state after:
α : Type u
c : CoheytingAlgebra α
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
sdiff : α → α → α
eq_sdiff : sdiff = SDiff.sdiff
hnot : α → α
eq_hnot : hnot = HNot.hnot
⊢ ∀ (x y : α), x ≤ y ↔ le x y
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: ι : Type u_5
R : ι → Type u_4
inst✝¹ : (i : ι) → CommSemiring (R i)
inst✝ : ∀ (i : ι), Nontrivial (R i)
h : Function.Surjective ⇑(toPiLocalization ((i : ι) → R i))
⊢ Finite ι

Tactic:
by
  contrapose! h
  exact toPiLocalization_not_surjective_of_infinite _

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

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

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:
· rintro ⟨sU, hU⟩ x hx
    rcases h.mem_nhds_iff.mp (IsOpen.mem_nhds hU hx) with ⟨sV, ⟨⟨V, H₁, H₂⟩, hsV⟩⟩
    refine ⟨V, H₁, ?_⟩
    cases V
    dsimp at H₂
    subst H₂
    exact hsV

Goal state after:
case mpr
α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
h : ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U' ∈ B, x ∈ U' ∧ U' ≤ U
⊢ IsBasis B
Module: Mathlib.Topology.LocallyClosed

Goal state before:
pp: case mpr
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
hf : IsInducing f
⊢ (∃ s', (∃ U Z, IsOpen[inst✝] U ∧ IsClosed[inst✝] Z ∧ s' = U ∩ Z) ∧ f ⁻¹' s' = s) →
    ∃ U Z, (∃ t, IsOpen[inst✝] t ∧ f ⁻¹' t = U) ∧ (∃ t, IsClosed[inst✝] t ∧ f ⁻¹' t = Z) ∧ s = U ∩ Z

Tactic:
rintro ⟨_, ⟨U, Z, hU, hZ, rfl⟩, rfl⟩

Goal state after:
case mpr
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsInducing f
U Z : Set Y
hU : IsOpen[inst✝] U
hZ : IsClosed[inst✝] Z
⊢ ∃ U_1 Z_1,
    (∃ t, IsOpen[inst✝] t ∧ f ⁻¹' t = U_1) ∧ (∃ t, IsClosed[inst✝] t ∧ f ⁻¹' t = Z_1) ∧ f ⁻¹' (U ∩ Z) = U_1 ∩ Z_1
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
⊢ (∃ s', IsLocallyClosed s' ∧ f ⁻¹' s' = s) ↔ ∃ s', IsLocallyClosed s' ∧ s' ∩ range f = f '' s

Tactic:
← (image_injective.mpr hf.injective).eq_iff,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
hf : IsEmbedding f
⊢ (∃ s', IsLocallyClosed s' ∧ f '' f ⁻¹' s' = f '' s) ↔ ∃ s', IsLocallyClosed s' ∧ s' ∩ range f = f '' s
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
⊢ IsClosedEmbedding f ↔ ∀ (i : ι), IsClosedEmbedding ((U i).carrier.restrictPreimage f)

Tactic:
by
  simp_rw [isClosedEmbedding_iff, forall_and]
  apply and_congr
  · exact hU.isEmbedding_iff_restrictPreimage h
  · simp_rw [range_restrictPreimage]
    exact hU.isClosed_iff_coe_preimage

Goal state after:
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₂
⊢ IsClosed[inst✝¹] W₁ᶜ

Tactic:
by simpa using hW₁.1.1

Goal state after:
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
x : X
U : Set X
hxU : U ∈ 𝓝 x
hU : IsOpen[inst✝²] U
hUs : IsConstructible (U ↓∩ s)
V : Set X
hV₁ : IsOpen[inst✝²] V
hV₂ : IsCompact V
hxV : x ∈ V
hVU : V ⊆ U
this✝ : IsConstructible (V ↓∩ s)
this : IsConstructible (Subtype.val '' V ↓∩ s)
⊢ IsConstructible (V ∩ s)

Tactic:
rwa [Subtype.image_preimage_coe] at this

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
f : R →+* S
hf : f.Flat
P : Ideal S
inst✝¹ : P.IsPrime
Q : Ideal R
inst✝ : Q.IsPrime
hQP : Q = Ideal.comap f P
⊢ (Localization.localRingHom Q P f hQP).Flat

Tactic:
by
  subst hQP
  algebraize [f, Localization.localRingHom (Ideal.comap f P) P f rfl]
  have : IsScalarTower R (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P) :=
    .of_algebraMap_eq fun x ↦ (Localization.localRingHom_to_map _ _ _ rfl x).symm
  rw [RingHom.Flat, Module.flat_iff_of_isLocalization
    (S := (Localization.AtPrime (Ideal.comap f P))) (p := (Ideal.comap f P).primeCompl)]
  exact Module.Flat.trans R S (Localization.AtPrime P)

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

Goal state before:
pp: n : ℕ
f : AddAut (ZMod n)
x : ZMod n
⊢ ↑x.cast * f 1 = f ↑x.cast

Tactic:
← zsmul_eq_mul,

Goal state after:
n : ℕ
f : AddAut (ZMod n)
x : ZMod n
⊢ x.cast • f 1 = f ↑x.cast
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: a b : ℕ
⊢ ∀ i ∈ (a.lcm b).factorization.support,
    (if b.factorization i ≤ a.factorization i then i ^ (a.lcm b).factorization i else 1) ≠ 0

Tactic:
intro p _ H

Goal state after:
a b p : ℕ
a✝ : p ∈ (a.lcm b).factorization.support
H : (if b.factorization p ≤ a.factorization p then p ^ (a.lcm b).factorization p else 1) = 0
⊢ False
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: a b : ℕ
⊢ ∀ i ∈ (a.lcm b).factorization.support,
    (if b.factorization i ≤ a.factorization i then 1 else i ^ (a.lcm b).factorization i) ≠ 0

Tactic:
intro p _ H

Goal state after:
a b p : ℕ
a✝ : p ∈ (a.lcm b).factorization.support
H : (if b.factorization p ≤ a.factorization p then 1 else p ^ (a.lcm b).factorization p) = 0
⊢ False
Module: Mathlib.RingTheory.RingHom.Flat

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.Flat
⊢ (ulift.{u₁, u₂, u_1, u_2} f).Flat

Tactic:
exact .comp (.comp (.of_bijective <| Equiv.bijective _) hf)
      (.of_bijective <| Equiv.bijective _)

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

Goal state before:
pp: case refine_2
R : Type u
inst✝ : CommSemiring R
⊢ vanishingIdeal '' {s | IsIrreducible s} ⊆ vanishingIdeal '' {s | IsClosed s ∧ IsIrreducible s}

Tactic:
rintro _ ⟨s, hs, rfl⟩

Goal state after:
case refine_2
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
hs : s ∈ {s | IsIrreducible s}
⊢ vanishingIdeal s ∈ vanishingIdeal '' {s | IsClosed s ∧ IsIrreducible s}
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing M
inst✝³ : Algebra R A
inst✝² : Algebra R M
F : Type u_4
inst✝¹ : FunLike F A M
inst✝ : AlgHomClass F R A M
f : F
f_inv : M → A
hf : Function.RightInverse f_inv ⇑f
d : Derivation R A A
hd : ∀ (x : A), f x = 0 → f (d x) = 0
x y : M
⊢ f (d (f_inv (x + y))) = f (d (f_inv x)) + f (d (f_inv y))

Tactic:
suffices f (d (f_inv (x + y) - (f_inv x + f_inv y))) = 0 by simpa [sub_eq_zero]

Goal state after:
R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing M
inst✝³ : Algebra R A
inst✝² : Algebra R M
F : Type u_4
inst✝¹ : FunLike F A M
inst✝ : AlgHomClass F R A M
f : F
f_inv : M → A
hf : Function.RightInverse f_inv ⇑f
d : Derivation R A A
hd : ∀ (x : A), f x = 0 → f (d x) = 0
x y : M
⊢ f (d (f_inv (x + y) - (f_inv x + f_inv y))) = 0
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
f g : R
⊢ basicOpen (f * g) ≤ basicOpen f

Tactic:
rw [basicOpen_mul f g]

Goal state after:
R : Type u
inst✝ : CommSemiring R
f g : R
⊢ basicOpen f ⊓ basicOpen g ≤ basicOpen f
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
f g : R
⊢ basicOpen (f * g) ≤ basicOpen g

Tactic:
rw [basicOpen_mul f g]

Goal state after:
R : Type u
inst✝ : CommSemiring R
f g : R
⊢ basicOpen f ⊓ basicOpen g ≤ basicOpen g
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case h_nhds
R : Type u
inst✝ : CommSemiring R
p : PrimeSpectrum R
U : Set (PrimeSpectrum R)
hp : p ∈ U
s : Set R
hs : zeroLocus s = Uᶜ
⊢ ∃ v ∈ Set.range fun r ↦ ↑(basicOpen r), p ∈ v ∧ v ⊆ U

Tactic:
← compl_compl U,

Goal state after:
case h_nhds
R : Type u
inst✝ : CommSemiring R
p : PrimeSpectrum R
U : Set (PrimeSpectrum R)
hp : p ∈ Uᶜᶜ
s : Set R
hs : zeroLocus s = Uᶜ
⊢ ∃ v ∈ Set.range fun r ↦ ↑(basicOpen r), p ∈ v ∧ v ⊆ U
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case hc
G : Type u
inst✝ : Monoid G
n : ℕ
hpos : 0 < n
hG : ∀ (g : G), g ^ n = 1
⊢ ExponentExists G

Tactic:
exact ⟨n, hpos, hG⟩

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝² : LeftCancelMonoid G
inst✝¹ : Finite G
inst✝ : Nontrivial G
⊢ exponent G ≠ 0 ∧ exponent G ≠ 1

Tactic:
exact ⟨exponent_ne_zero_of_finite, mt exp_eq_one_iff.mp (not_subsingleton G)⟩

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G = 0
⊢ exponent G = sSup (Set.range fun g ↦ orderOf g)

Tactic:
he,

Goal state after:
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G = 0
⊢ 0 = sSup (Set.range fun g ↦ orderOf g)
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
hH : IsPGroup p ↥H
hK : IsPGroup p ↥K
inst✝ : K.Normal
⊢ IsPGroup p ↥(Subgroup.comap (QuotientGroup.mk' K) (Subgroup.map (QuotientGroup.mk' K) H))

Tactic:
apply (hH.map (QuotientGroup.mk' K)).comap_of_ker_isPGroup

Goal state after:
p : ℕ
G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
hH : IsPGroup p ↥H
hK : IsPGroup p ↥K
inst✝ : K.Normal
⊢ IsPGroup p ↥(QuotientGroup.mk' K).ker
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

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

Tactic:
isClopen_iff_mul_add,

Goal state after:
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ (∃ e f, e * f = 0 ∧ e + f = 1 ∧ s = ↑(basicOpen e)) ↔ ∃ e f, e * f = 0 ∧ e + f = 1 ∧ 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
h : IsClosedMap (comap (mapRingHom f))
algInst✝ : Algebra R S := f.toAlgebra
a✝ : Nontrivial R
⊢ Algebra.IsIntegral R S

Tactic:
nontriviality S

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
h : IsClosedMap (comap (mapRingHom f))
algInst✝ : Algebra R S := f.toAlgebra
a✝¹ : Nontrivial R
a✝ : Nontrivial S
⊢ Algebra.IsIntegral R S
Module: Mathlib.GroupTheory.Rank

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝³ : Group G
inst✝² : Group H
inst✝¹ : FG G
inst✝ : FG H
f : G →* H
hf : Surjective ⇑f
S : Finset G
hS1 : S.card = rank G
hS2 : Subgroup.closure ↑S = ⊤
⊢ Subgroup.map f ⊤ = ⊤

Tactic:
Subgroup.map_top_of_surjective f hf

Goal state after:
G : Type u_1
H : Type u_2
inst✝³ : Group G
inst✝² : Group H
inst✝¹ : FG G
inst✝ : FG H
f : G →* H
hf : Surjective ⇑f
S : Finset G
hS1 : S.card = rank G
hS2 : Subgroup.closure ↑S = ⊤
⊢ ⊤ = ⊤
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
inst✝ : Group G
g : G
n : ℕ
npos : 0 < n
hn : ∀ (g : G), g ^ n = 1
⊢ IsOfFinOrder g

Tactic:
exact isOfFinOrder_iff_pow_eq_one.mpr ⟨n, npos, hn g⟩

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

Goal state before:
pp: case refine_1.inr.inl.inr
M : Type u_4
N : Type u_5
inst✝¹ : Group M
inst✝ : Group N
h : IsCyclic (M × N)
h✝² : Finite M
h✝¹ : Infinite N
h✝ : Nontrivial M
⊢ (Nat.card M).Coprime (Nat.card N)

Tactic:
rw [(MulEquiv.prodComm ..).isCyclic] at h

Goal state after:
case refine_1.inr.inl.inr
M : Type u_4
N : Type u_5
inst✝¹ : Group M
inst✝ : Group N
h : IsCyclic (N × M)
h✝² : Finite M
h✝¹ : Infinite N
h✝ : Nontrivial M
⊢ (Nat.card M).Coprime (Nat.card N)
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝¹ : Group G
inst✝ : Fintype G
p k : ℕ
hp : Nat.Prime p
h : p ^ k ∣ Nat.card G
this✝ : Fact (Nat.Prime p)
H : Subgroup G
hH : Nat.card ↥H = p ^ k
this : ∀ g ∈ (↑H \ {1}).toFinset, p ∣ orderOf g
⊢ p ^ k ∣ p ^ #(↑H \ {1}).toFinset

Tactic:
k.le_sub_one_of_lt <| k.lt_pow_self hp.one_lt

Goal state after:
G : Type u
inst✝¹ : Group G
inst✝ : Fintype G
p k : ℕ
hp : Nat.Prime p
h : p ^ k ∣ Nat.card G
this✝ : Fact (Nat.Prime p)
H : Subgroup G
hH : Nat.card ↥H = p ^ k
this : ∀ g ∈ (↑H \ {1}).toFinset, p ∣ orderOf g
⊢ p ^ (p ^ k - 1) ∣ p ^ #(↑H \ {1}).toFinset