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

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

Tactic:
rw [choose_eq_zero_of_lt hikl, zero_mul]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ max (if {x ∈ p.support | ↑(x.choose n) * p.coeff x = 0} = ∅ then 0 else max 0 0)
      (Finset.fold max 0 (fun x ↦ x - n) ({i ∈ p.support | ¬↑(i.choose n) * p.coeff i = 0})) ≤
    p.natDegree - n

pp: case h
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ max 0 (max 0 0) = max 0 0

Tactic:
· simp only [ite_self, max_eq_right, zero_le, Finset.fold_max_le, true_and, and_imp,
        tsub_le_iff_right, mem_support_iff, Ne, Finset.mem_filter]
      intro x hx hx'
      have hxp : x ≤ p.natDegree := le_natDegree_of_ne_zero hx
      grind

Goal state after:
case h
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ max 0 (max 0 0) = max 0 0
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: case pos
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
Rₘ : Type u_3
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
p : Rₘ[X]
hp : p.leadingCoeff ∈ (algebraMap R Rₘ).range
n : ℕ
h₁ : n ∈ p.support
⊢ p.coeff n * (algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff) ^ (p.natDegree - n) ∈ Set.range ⇑(algebraMap R Rₘ)

Tactic:
by_cases h₂ : n = p.natDegree

Goal state after:
case pos
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
Rₘ : Type u_3
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
p : Rₘ[X]
hp : p.leadingCoeff ∈ (algebraMap R Rₘ).range
n : ℕ
h₁ : n ∈ p.support
h₂ : n = p.natDegree
⊢ p.coeff n * (algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff) ^ (p.natDegree - n) ∈ Set.range ⇑(algebraMap R Rₘ)

case neg
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
Rₘ : Type u_3
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
p : Rₘ[X]
hp : p.leadingCoeff ∈ (algebraMap R Rₘ).range
n : ℕ
h₁ : n ∈ p.support
h₂ : ¬n = p.natDegree
⊢ p.coeff n * (algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff) ^ (p.natDegree - n) ∈ Set.range ⇑(algebraMap R Rₘ)
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: S : Type u_2
inst✝³ : CommRing S
K : Type u_4
inst✝² : CommRing K
inst✝¹ : Algebra S K
inst✝ : IsIntegralClosure S ℤ K
x : K
hx : IsAlgebraic ℤ x
s : S
n : ℕ
ha : -↑n ≠ 0
h : -↑n • x = (algebraMap S K) s
⊢ n ≠ 0

Tactic:
simpa using ha

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

Goal state before:
pp: case tmul
R : Type u
M : Type v
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N1 : Type u_1
inst✝⁵ : AddCommGroup N1
inst✝⁴ : Module R N1
N2 : Type u_2
inst✝³ : AddCommGroup N2
inst✝² : Module R N2
N3 : Type u_3
inst✝¹ : AddCommGroup N3
inst✝ : Module R N3
l12 : N1 →ₗ[R] N2
l23 : N2 →ₗ[R] N3
fl : FaithfullyFlat R M
ex : Function.Exact ⇑(LinearMap.rTensor M l12) ⇑(LinearMap.rTensor M l23)
complex : l12.range ≤ l23.ker
H : Type u_2 := ↥l23.ker ⧸ (Submodule.inclusion complex).range
e : H ⊗[R] M ≃ₗ[R]
  ↥l23.ker ⊗[R] M ⧸ (TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id).range :=
  quotientTensorEquiv M (Submodule.inclusion complex).range
m : M
x : N2
hx : l23 x = 0
mem : x ⊗ₜ[R] m ∈ (LinearMap.rTensor M l23).ker
⊢ ∃ a, (TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id) a = ⟨x, hx⟩ ⊗ₜ[R] m

Tactic:
LinearMap.exact_iff.1 ex

Goal state after:
case tmul
R : Type u
M : Type v
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N1 : Type u_1
inst✝⁵ : AddCommGroup N1
inst✝⁴ : Module R N1
N2 : Type u_2
inst✝³ : AddCommGroup N2
inst✝² : Module R N2
N3 : Type u_3
inst✝¹ : AddCommGroup N3
inst✝ : Module R N3
l12 : N1 →ₗ[R] N2
l23 : N2 →ₗ[R] N3
fl : FaithfullyFlat R M
ex : Function.Exact ⇑(LinearMap.rTensor M l12) ⇑(LinearMap.rTensor M l23)
complex : l12.range ≤ l23.ker
H : Type u_2 := ↥l23.ker ⧸ (Submodule.inclusion complex).range
e : H ⊗[R] M ≃ₗ[R]
  ↥l23.ker ⊗[R] M ⧸ (TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id).range :=
  quotientTensorEquiv M (Submodule.inclusion complex).range
m : M
x : N2
hx : l23 x = 0
mem : x ⊗ₜ[R] m ∈ (LinearMap.rTensor M l12).range
⊢ ∃ a, (TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id) a = ⟨x, hx⟩ ⊗ₜ[R] m
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: 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
⊢ finrank R S * finrank S T = finrank R T

Tactic:
by_cases h : FaithfulSMul R S

Goal state after:
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

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.Localization.Integral

Goal state before:
pp: R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Field K
inst✝⁹ : CommRing L
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R K
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : Algebra K L
inst✝³ : IsScalarTower R S L
inst✝² : IsScalarTower R K L
inst✝¹ : IsFractionRing S L
inst✝ : Algebra.IsIntegral R S
x : S
s : ↥S⁰
⊢ IsAlgebraic K (mk' L x s)

Tactic:
apply IsIntegral.isAlgebraic

Goal state after:
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Field K
inst✝⁹ : CommRing L
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R K
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : Algebra K L
inst✝³ : IsScalarTower R S L
inst✝² : IsScalarTower R K L
inst✝¹ : IsFractionRing S L
inst✝ : Algebra.IsIntegral R S
x : S
s : ↥S⁰
⊢ IsIntegral K (mk' L x s)
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✝ : Flat A B
h : Function.Surjective (PrimeSpectrum.comap (algebraMap A B))
⊢ FaithfullyFlat A B

Tactic:
refine ⟨fun m hm ↦ ?_⟩
  obtain ⟨m', hm'⟩ := h ⟨m, hm.isPrime⟩
  have : m = Ideal.comap (algebraMap A B) m'.asIdeal := by
    rw [← PrimeSpectrum.comap_asIdeal (algebraMap A B) m', hm']
  rw [Ideal.smul_top_eq_map, this]
  exact (Submodule.restrictScalars_eq_top_iff _ _ _).ne.mpr
    fun top ↦ m'.isPrime.ne_top <| top_le_iff.mp <| top ▸ Ideal.map_comap_le

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:
rwa [mem_ker, map_sub, sub_eq_zero]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p : Ideal R
hp : p ∈ minimalPrimes R
⊢ Disjoint ↑p ↑(nonZeroDivisors R)

Tactic:
Set.disjoint_left,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
p : Ideal R
hp : p ∈ minimalPrimes R
⊢ ∀ ⦃a : R⦄, a ∈ ↑p → a ∉ ↑(nonZeroDivisors R)
Module: Mathlib.RingTheory.Spectrum.Prime.RingHom

Goal state before:
pp: case h
R : Type u
inst✝² : CommRing R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : PrimeSpectrum R
k : Type u := ⋯
h : Nontrivial (p.asIdeal.ResidueField ⊗[R] S)
m : Ideal (k ⊗[R] S)
hm : m.IsMaximal
⊢ (comap (algebraMap R S) (comap Algebra.TensorProduct.includeRight.toRingHom { asIdeal := m, isPrime := ⋯ })).asIdeal =
    p.asIdeal

Tactic:
rw [← PrimeSpectrum.comap_comp_apply,
      ← Algebra.TensorProduct.includeLeftRingHom_comp_algebraMap, comap_comp_apply]

Goal state after:
case h
R : Type u
inst✝² : CommRing R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : PrimeSpectrum R
k : Type u := p.asIdeal.ResidueField
h : Nontrivial (p.asIdeal.ResidueField ⊗[R] S)
m : Ideal (k ⊗[R] S)
hm : m.IsMaximal
⊢ (comap (algebraMap R k) (comap Algebra.TensorProduct.includeLeftRingHom { asIdeal := m, isPrime := ⋯ })).asIdeal =
    p.asIdeal
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: case mp
R : Type u_4
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K
hrange : x ∉ range ⇑(algebraMap R K)
hlocal : ∀ (i : MaximalSpectrum R), x ∈ Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯
denom : Ideal R := Submodule.comap (LinearMap.toSpanSingleton R K x) 1
⊢ False

Tactic:
have hdenom : (1 : R) ∉ denom := by simpa [denom] using hrange

Goal state after:
case mp
R : Type u_4
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K
hrange : x ∉ range ⇑(algebraMap R K)
hlocal : ∀ (i : MaximalSpectrum R), x ∈ Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯
denom : Ideal R := Submodule.comap (LinearMap.toSpanSingleton R K x) 1
hdenom : 1 ∉ denom
⊢ False
Module: Mathlib.Topology.Sets.OpenCover

Goal state before:
pp: case neg
X : Type u_1
ι : Type u_2
inst✝ : TopologicalSpace X
U : ι → Opens X
hn : Pairwise ((fun x1 x2 ↦ ¬Disjoint x1 x2) on U)
h : ∀ (i : ι), IsPreirreducible ↑(U i)
s : Set X
hs : IsOpen[inst✝] s
hsU : s ⊆ ⋃ i, ↑(U i)
x : X
hx : x ∈ s
i : ι
hi : x ∈ ↑(U i)
u : Set X
hu : u ∈ irreducibleComponents X
hUu : (U i).carrier ⊆ u
huniv : ¬s ⊆ u
huo : IsOpen[inst✝] uᶜ
a : X
ha₁ : a ∈ s
ha₂ : a ∉ u
j : ι
haj : a ∈ ↑(U j)
hji : j ≠ i
⊢ IsPreirreducible s

Tactic:
rcases inter_nonempty_iff_exists_left.mp
        ((h j) (U i) uᶜ (U i).isOpen huo
        (not_disjoint_iff_nonempty_inter.mp (by simpa using hn hji)) ⟨a, ⟨haj, ha₂⟩⟩).right
        with ⟨x, hx₁, hx₂⟩

Goal state after:
case neg
X : Type u_1
ι : Type u_2
inst✝ : TopologicalSpace X
U : ι → Opens X
hn : Pairwise ((fun x1 x2 ↦ ¬Disjoint x1 x2) on U)
h : ∀ (i : ι), IsPreirreducible ↑(U i)
s : Set X
hs : IsOpen[inst✝] s
hsU : s ⊆ ⋃ i, ↑(U i)
x✝ : X
hx : x✝ ∈ s
i : ι
hi : x✝ ∈ ↑(U i)
u : Set X
hu : u ∈ irreducibleComponents X
hUu : (U i).carrier ⊆ u
huniv : ¬s ⊆ u
huo : IsOpen[inst✝] uᶜ
a : X
ha₁ : a ∈ s
ha₂ : a ∉ u
j : ι
haj : a ∈ ↑(U j)
hji : j ≠ i
x : X
hx₁ : x ∈ ↑(U i)
hx₂ : x ∈ uᶜ
⊢ IsPreirreducible s
Module: Mathlib.Topology.Sets.Opens

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
U V : Opens α
i : U ≤ V
⊢ IsOpen[instTopologicalSpaceSubtype] (range (Set.inclusion ⋯))

Tactic:
by
    rw [Set.range_inclusion i]
    exact U.isOpen.preimage continuous_subtype_val

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 : IsTopologicalBasis (SetLike.coe '' B)
f : α → β
h : IsInducing f
⊢ IsTopologicalBasis (SetLike.coe '' {x | ∃ U ∈ B, { carrier := f ⁻¹' ↑U, is_open' := ⋯ } = x})

Tactic:
convert! H.isInducing h

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
B : Set (Opens β)
H : IsTopologicalBasis (SetLike.coe '' B)
f : α → β
h : IsInducing f
⊢ SetLike.coe '' {x | ∃ U ∈ B, { carrier := f ⁻¹' ↑U, is_open' := ⋯ } = x} = preimage f '' SetLike.coe '' B
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
⊢ IsOpenMap f ↔ ∀ (i : ι), IsOpenMap (f ∘ Subtype.val)

Tactic:
refine ⟨fun hf ↦ fun i ↦ hf.comp (U i).isOpenEmbedding'.isOpenMap, fun hf ↦ ?_⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens α
hU : IsOpenCover U
hf : ∀ (i : ι), IsOpenMap (f ∘ Subtype.val)
⊢ IsOpenMap f
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
hf : ∀ (i : ι), IsOpenMap (f ∘ Subtype.val)
⊢ IsOpenMap f

Tactic:
intro V

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens α
hU : IsOpenCover U
hf : ∀ (i : ι), IsOpenMap (f ∘ Subtype.val)
V : Set α
⊢ IsOpen[inst✝¹] V → IsOpen[inst✝] (f '' V)
Module: Mathlib.Topology.Sets.Closeds

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : β → α
hf : IsInducing f
⊢ Function.Injective (map f ⋯)

Tactic:
intro A

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : β → α
hf : IsInducing f
A : IrreducibleCloseds β
⊢ ∀ ⦃a₂ : IrreducibleCloseds β⦄, map f ⋯ A = map f ⋯ a₂ → A = a₂
Module: Mathlib.Order.Ideal

Goal state before:
pp: P : Type u_1
inst✝¹ : SemilatticeSup P
inst✝ : OrderBot P
x : P
S✝ S : Set (Ideal P)
⊢ IsGLB S (sInf S)

Tactic:
refine ⟨fun s hs ↦ ?_, fun s hs ↦ by rwa [← coe_subset_coe, coe_sInf, subset_iInter₂_iff]⟩
      rw [← coe_subset_coe, coe_sInf]
      exact biInter_subset_of_mem hs

Goal state after:
Module: Mathlib.Topology.KrullDimension

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : QuasiSober Y
inst✝² : T0Space Y
inst✝¹ : QuasiSober X
inst✝ : T0Space X
x : X
f : X → Y
hf : IsOpenEmbedding f
⊢ coheight (f x) = coheight x

Tactic:
rw [← coheight_orderIso (irreducibleSetEquivPoints (α := Y)).symm (f x),
    ← coheight_orderIso (irreducibleSetEquivPoints (α := X)).symm x,
    ← Topology.IsOpenEmbedding.coheight_map hf]
  congr
  ext : 1
  simp [closure_image_closure hf.continuous]

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: case open_retrocompact
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set Y
hfcont : Continuous[inst✝¹, inst✝] f
hf : ∀ (s : Set Y), IsOpen[inst✝] s → IsRetrocompact s → IsRetrocompact (f ⁻¹' s)
U : Set Y
hUopen : IsOpen[inst✝] U
hUcomp : IsRetrocompact U
⊢ IsConstructible (f ⁻¹' U)

Tactic:
| open_retrocompact U hUopen hUcomp =>

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: case open_retrocompact
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hfopen : IsOpenEmbedding f
hfcomp : IsRetrocompact (range f)
U : Set X
hUopen : IsOpen[inst✝¹] U
hUcomp : IsRetrocompact U
⊢ IsConstructible (f '' U)

Tactic:
| open_retrocompact U hUopen hUcomp =>

Goal state after:
Module: Mathlib.Topology.Sober

Goal state before:
pp: case a
α : Type u_1
inst✝ : TopologicalSpace α
ι : Type u_3
U : ι → Opens α
hU : IsOpenCover U
hU' : ∀ (i : ι), QuasiSober ↥(U i)
t : Set α
h : IsPreirreducible t
x : α
hx : x ∈ t
h' : IsClosed t
i : ι
hi : x ∈ U i
H : IsIrreducible (Subtype.val ⁻¹' t)
⊢ t ⊆ closure (Subtype.val '' closure (Subtype.val ⁻¹' t))

Tactic:
refine (subset_closure_inter_of_isPreirreducible_of_isOpen h (U i).isOpen ⟨x, ⟨hx, hi⟩⟩).trans
      (closure_mono ?_)

Goal state after:
case a
α : Type u_1
inst✝ : TopologicalSpace α
ι : Type u_3
U : ι → Opens α
hU : IsOpenCover U
hU' : ∀ (i : ι), QuasiSober ↥(U i)
t : Set α
h : IsPreirreducible t
x : α
hx : x ∈ t
h' : IsClosed t
i : ι
hi : x ∈ U i
H : IsIrreducible (Subtype.val ⁻¹' t)
⊢ t ∩ ↑(U i) ⊆ Subtype.val '' closure (Subtype.val ⁻¹' t)
Module: Mathlib.Topology.Constructible

Goal state before:
pp: case open_retrocompact
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsClosedEmbedding f
hfcomp : IsRetrocompact (range f)ᶜ
U : Set X
hUopen : IsOpen[inst✝¹] U
hUcomp : IsRetrocompact U
⊢ IsConstructible (f '' U)

Tactic:
| open_retrocompact U hUopen hUcomp =>

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
ι : Type u_4
U : ι → Opens X
hU : IsOpenCover U
H : ∀ (i : ι), IsLocallyConstructible (↑(U i) ↓∩ s)
x : X
⊢ ∃ U ∈ 𝓝 x, IsOpen[inst✝] U ∧ IsConstructible (U ↓∩ s)

Tactic:
have ⟨i, hi⟩ := hU.exists_mem x

Goal state after:
X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
ι : Type u_4
U : ι → Opens X
hU : IsOpenCover U
H : ∀ (i : ι), IsLocallyConstructible (↑(U i) ↓∩ s)
x : X
i : ι
hi : x ∈ U i
⊢ ∃ U ∈ 𝓝 x, IsOpen[inst✝] U ∧ IsConstructible (U ↓∩ s)
Module: Mathlib.RingTheory.RingHom.Flat

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
hR : IsField R
f : R →+* S
⊢ f.Flat

Tactic:
by
  let := f.toAlgebra
  let := hR.toField
  rw [← f.algebraMap_toAlgebra, RingHom.flat_algebraMap_iff]
  infer_instance

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

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

Tactic:
compl_compl

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 h₁
R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsRadical
⊢ (zeroLocus ↑I).Nonempty ↔ I ≠ ⊤

pp: case h₂
R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsRadical
⊢ IsPreirreducible (zeroLocus ↑I) ↔ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I

Tactic:
· rw [Set.nonempty_iff_ne_empty, Ne, zeroLocus_empty_iff_eq_top]

Goal state after:
case h₂
R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsRadical
⊢ IsPreirreducible (zeroLocus ↑I) ↔ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring A
inst✝⁶ : CommSemiring B
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : Module A M
inst✝¹ : Module B M
inst✝ : Module R M
D D1 D2 : Derivation R A M
r : R
a✝ b✝ a b : A
⊢ 0 (a * b) = a • 0 b + b • 0 a

Tactic:
simp only [add_zero, LinearMap.zero_apply, smul_zero]

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 : R →+* S
hf : Surjective ⇑f
⊢ ∀ (s : Set (PrimeSpectrum S)), (∃ s_1, sᶜ = zeroLocus s_1) ↔ ∃ t, (∃ s, t = zeroLocus s) ∧ comap f ⁻¹' t = sᶜ

Tactic:
refine fun s =>
      ⟨fun ⟨F, hF⟩ =>
        ⟨zeroLocus (f ⁻¹' F), ⟨f ⁻¹' F, rfl⟩, by
          rw [preimage_comap_zeroLocus, Function.Surjective.image_preimage hf, hF]⟩,
        ?_⟩

Goal state after:
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
hf : Surjective ⇑f
s : Set (PrimeSpectrum S)
⊢ (∃ t, (∃ s, t = zeroLocus s) ∧ comap f ⁻¹' t = sᶜ) → ∃ s_1, sᶜ = zeroLocus s_1
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 (f_inv (x + y) - (f_inv x + f_inv y)) = 0

Tactic:
simp [hf _]

Goal state after:
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 : R
y : M
⊢ f (f_inv (x • y) - x • f_inv y) = 0

Tactic:
simp [hf _]

Goal state after:
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
⊢ f (f_inv 1 - 1) = 0

Tactic:
simp [hf _]

Goal state after:
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 (f_inv (x * y) - f_inv x * f_inv y) = 0

Tactic:
simp [hf _]

Goal state after:
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

pp: case refine_2
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
⊢ IsClosedMap ⇑(primeSpectrumProd R S).symm

Tactic:
· rw [continuous_sum_dom]
    simp only [Function.comp_def, primeSpectrumProd_symm_inl, primeSpectrumProd_symm_inr]
    exact ⟨continuous_comap _, continuous_comap _⟩

Goal state after:
case refine_2
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
⊢ IsClosedMap ⇑(primeSpectrumProd R S).symm
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 : A
⊢ f (f_inv (f x) - x) = 0

Tactic:
simp [hf _]

Goal state after:
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)
s : Set R
hs : zeroLocus s = Uᶜ
f : R
hfs : f ∈ s
hfp : f ∉ ↑p.asIdeal
⊢ zeroLocus s ⊆ (zeroLocus {f})ᶜᶜ

Tactic:
compl_compl

Goal state after:
case h_nhds
R : Type u
inst✝ : CommSemiring R
p : PrimeSpectrum R
U : Set (PrimeSpectrum R)
s : Set R
hs : zeroLocus s = Uᶜ
f : R
hfs : f ∈ s
hfp : f ∉ ↑p.asIdeal
⊢ zeroLocus s ⊆ zeroLocus {f}
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
⊢ ∃ z ∈ closure {x, y}, orderOf z = (orderOf x).lcm (orderOf y)

Tactic:
by_cases hx : orderOf x = 0 <;> by_cases hy : orderOf y = 0

Goal state after:
case pos
G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : orderOf x = 0
hy : orderOf y = 0
⊢ ∃ z ∈ closure {x, y}, orderOf z = (orderOf x).lcm (orderOf y)

case neg
G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : orderOf x = 0
hy : ¬orderOf y = 0
⊢ ∃ z ∈ closure {x, y}, orderOf z = (orderOf x).lcm (orderOf y)

case pos
G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : ¬orderOf x = 0
hy : orderOf y = 0
⊢ ∃ z ∈ closure {x, y}, orderOf z = (orderOf x).lcm (orderOf y)

case neg
G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : ¬orderOf x = 0
hy : ¬orderOf y = 0
⊢ ∃ z ∈ closure {x, y}, orderOf z = (orderOf x).lcm (orderOf y)