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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : IsCancelMulZero R
x z : R
hy : IsRadical (x * z)
h0 : x * z ≠ 0
⊢ ∀ (x_1 : R), x ∣ x_1 ^ 2 → x ∣ x_1

Tactic:
refine fun w dvd ↦ ((mul_dvd_mul_iff_right <| right_ne_zero_of_mul h0).mp <| hy 2 _ ?_)

Goal state after:
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : IsCancelMulZero R
x z : R
hy : IsRadical (x * z)
h0 : x * z ≠ 0
w : R
dvd : x ∣ w ^ 2
⊢ x * z ∣ (w * z) ^ 2
Module: Mathlib.RingTheory.Nilpotent.Basic

Goal state before:
pp: R : Type u_1
x y : R
inst✝ : Semiring R
h_comm : Commute x y
hx : x ∈ nonZeroDivisorsLeft R
⊢ IsNilpotent (x * y) ↔ IsNilpotent y

Tactic:
by
  refine ⟨?_, h_comm.isNilpotent_mul_left⟩
  rintro ⟨k, hk⟩
  rw [mul_pow h_comm] at hk
  exact ⟨k, (nonZeroDivisorsLeft R).pow_mem hx k _ hk⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap

Goal state before:
pp: case inr.e_6
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Module.Finite R M
I : Ideal R
h✝ : Nontrivial R
s : Finset M
hs_card : s.card = ⊤.spanFinrank
hs_span : Submodule.span R ↑s = ⊤
this : Submodule.span R (Set.range Subtype.val) = ⊤
A : ↥(isRepresentation R Subtype.val)
h : ∀ (i j : ↥s), ↑A i j ∈ I
hI : range ((isRepresentation.toEnd R Subtype.val this) A) ≤ I • ⊤
⊢ ↑((aeval A) (↑A).charpoly) = ↑0

Tactic:
Polynomial.aeval_subalgebra_coe,

Goal state after:
case inr.e_6
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Module.Finite R M
I : Ideal R
h✝ : Nontrivial R
s : Finset M
hs_card : s.card = ⊤.spanFinrank
hs_span : Submodule.span R ↑s = ⊤
this : Submodule.span R (Set.range Subtype.val) = ⊤
A : ↥(isRepresentation R Subtype.val)
h : ∀ (i j : ↥s), ↑A i j ∈ I
hI : range ((isRepresentation.toEnd R Subtype.val this) A) ≤ I • ⊤
⊢ (aeval ↑A) (↑A).charpoly = ↑0
Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_4
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Ring T
f : R →+* S
x : S
g : S →+* T
p : R[X]
hp : p.Monic
hx : eval x (Polynomial.map f p) = 0
⊢ g (eval x (Polynomial.map f p)) = 0

Tactic:
simp [hx]

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

Goal state before:
pp: R : Type u_5
S : Type u_6
T : Type u_7
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra T S
φ : R ≃+* T
h : (algebraMap T S).comp φ.toRingHom = algebraMap R S
a : S
⊢ IsIntegral R a ↔ IsIntegral T a

Tactic:
constructor <;> intro ha
  · let : Algebra R T := φ.toRingHom.toAlgebra
    let : IsScalarTower R T S :=
      ⟨fun r t s ↦ by simp only [Algebra.smul_def, map_mul, ← h, mul_assoc]; rfl⟩
    exact IsIntegral.tower_top ha
  · have h' : (algebraMap T S) = (algebraMap R S).comp φ.symm.toRingHom := by
      have : RingHomInvPair (φ : R →+* T) φ.symm := RingHomInvPair.of_ringEquiv _
      simp only [← h, RingHom.comp_assoc, RingEquiv.toRingHom_eq_coe, RingHomCompTriple.comp_eq]
    let : Algebra T R := φ.symm.toRingHom.toAlgebra
    let : IsScalarTower T R S :=
      ⟨fun r t s ↦ by simp only [Algebra.smul_def, map_mul, h', mul_assoc]; rfl⟩
    exact IsIntegral.tower_top ha

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
hk : k ≤ Fintype.card n
a✝ : Nontrivial R
hnd : M.charpoly.natDegree = Fintype.card n
⊢ M.charpoly.coeff (Fintype.card n - k) =
    (-1) ^ k * ∑ s ∈ powersetCard k univ, (M.submatrix Subtype.val Subtype.val).det

Tactic:
have hrev : M.charpoly.coeff (Fintype.card n - k) = M.charpoly.reverse.coeff k := by
    simp [Polynomial.coeff_reverse, hnd, hk]

Goal state after:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
hk : k ≤ Fintype.card n
a✝ : Nontrivial R
hnd : M.charpoly.natDegree = Fintype.card n
hrev : M.charpoly.coeff (Fintype.card n - k) = M.charpoly.reverse.coeff k
⊢ M.charpoly.coeff (Fintype.card n - k) =
    (-1) ^ k * ∑ s ∈ powersetCard k univ, (M.submatrix Subtype.val Subtype.val).det
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
n : ℕ
⊢ (∑ x ∈ Finset.antidiagonal n, p.coeff x.1 * q.coeff x.2) * r ^ (p.natDegree + q.natDegree - n) =
    (p.scaleRoots r * q.scaleRoots r).coeff n

Tactic:
rw [coeff_mul, Finset.sum_mul]
    apply Finset.sum_congr rfl
    simp only [Finset.mem_antidiagonal, coeff_scaleRoots, Prod.forall]
    intro a b e
    cases lt_or_ge (natDegree p) a with
    | inl h => simp only [coeff_eq_zero_of_natDegree_lt h, zero_mul]
    | inr ha =>
      cases lt_or_ge (natDegree q) b with
      | inl h => simp only [coeff_eq_zero_of_natDegree_lt h, zero_mul, mul_zero]
      | inr hb =>
        simp only [← e, mul_assoc, mul_comm (r ^ (_ - a)), ← pow_add]
        rw [add_comm (_ - _), tsub_add_tsub_comm ha hb]

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

Goal state before:
pp: case inr
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
h : p.natDegree = q.natDegree
n : ℕ
hn : n ≤ (p + q).natDegree
⊢ (p.coeff n + q.coeff n) * r ^ ((p + q).natDegree - n + (p.natDegree - (p + q).natDegree)) =
    (p.coeff n + q.coeff n) * r ^ (p.natDegree - n)

Tactic:
| inr hn =>

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

Goal state before:
pp: case inr.inr
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
hp : p.Splits
r : R
h✝ : Nontrivial R
hp0 : p ≠ 0
⊢ (p.scaleRoots r).Splits

Tactic:
obtain ⟨m, hm⟩ := splits_iff_exists_multiset'.mp hp

Goal state after:
case inr.inr
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
hp : p.Splits
r : R
h✝ : Nontrivial R
hp0 : p ≠ 0
m : Multiset R
hm : p = C p.leadingCoeff * (Multiset.map (fun x ↦ X + C x) m).prod
⊢ (p.scaleRoots r).Splits
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : f.natDegree ≤ 1
h : Invertible f.leadingCoeff
⊢ f.Splits

Tactic:
by
  obtain ⟨a, b, rfl⟩ := exists_eq_X_add_C_of_natDegree_le_one hf
  rcases eq_or_ne a 0 with rfl | ha
  · simp
  · replace h : Invertible a := by simpa [leadingCoeff, ha] using h
    rw [← mul_invOf_cancel_left a b, C_mul, ← mul_add]
    exact (Splits.C a).mul (Splits.X_add_C _)

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

Goal state before:
pp: case inr
R : Type u_1
inst✝ : Ring R
f : R[X]
hf : f.Splits
a : R
⊢ (X.comp (-X) + (C a).comp (-X)).Splits

Tactic:
X_comp,

Goal state after:
case inr
R : Type u_1
inst✝ : Ring R
f : R[X]
hf : f.Splits
a : R
⊢ (-X + (C a).comp (-X)).Splits
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: S : Type u_4
inst✝ : CommRing S
g : S[X]
mon : g.Monic
I : Ideal S[X]
h : g ∈ I
⊢ eval₂ ((Ideal.Quotient.mk I).comp (algebraMap S S[X])) ((Ideal.Quotient.mk I) X) g = (Ideal.Quotient.mk I) g

Tactic:
eval₂_eq_sum_range

Goal state after:
S : Type u_4
inst✝ : CommRing S
g : S[X]
mon : g.Monic
I : Ideal S[X]
h : g ∈ I
⊢ ∑ i ∈ Finset.range (g.natDegree + 1),
      ((Ideal.Quotient.mk I).comp (algebraMap S S[X])) (g.coeff i) * (Ideal.Quotient.mk I) X ^ i =
    (Ideal.Quotient.mk I) g
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
⊢ (f * X).Splits ↔ f.Splits

Tactic:
by simp [mul_comm f]

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
x y : B
hx : IsIntegral R x
hy : IsIntegral R y
⊢ (algebraMap A B) (mk' A (x * y) ⋯) = (algebraMap A B) (mk' A x hx * mk' A y hy)

Tactic:
simp only [algebraMap_mk', map_mul]

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
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A B
x : R
h : IsIntegral R ((algebraMap R B) x)
⊢ (algebraMap R B) x = (algebraMap A B) ((algebraMap R A) x)

Tactic:
← IsScalarTower.algebraMap_apply

Goal state after:
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
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A B
x : R
h : IsIntegral R ((algebraMap R B) x)
⊢ (algebraMap R B) x = (algebraMap R B) x
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: 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
this : n + 1 ≤ p.natDegree
⊢ (algebraMap R Rₘ) (↑(commonDenom M p.support p.coeff) ^ (p.natDegree - n - 1)) *
      ((algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff) * p.coeff n) ∈
    (algebraMap R Rₘ).range

Tactic:
apply mul_mem

Goal state after:
case neg.a
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
this : n + 1 ≤ p.natDegree
⊢ (algebraMap R Rₘ) (↑(commonDenom M p.support p.coeff) ^ (p.natDegree - n - 1)) ∈ (algebraMap R Rₘ).range

case neg.a
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
this : n + 1 ≤ p.natDegree
⊢ (algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff) * p.coeff n ∈ (algebraMap R Rₘ).range
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
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
⊢ x ⊗ₜ[R] m ∈ (LinearMap.rTensor M l23).ker

Tactic:
simp [hx]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
f g : R
x : PrimeSpectrum R
⊢ x ∈ zeroLocus {f * g} ↔ x ∈ zeroLocus {f} ∪ zeroLocus {g}

Tactic:
simpa using x.2.mul_mem_iff_mem_or_mem

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

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Ring A
inst✝² : Algebra R S
inst✝¹ : Algebra S A
inst✝ : NoZeroDivisors S
s t : Set S
a : A
Rs : Subalgebra R S := adjoin R s
ha : IsAlgebraic (↥Rs) a
Rt : Subalgebra R S := adjoin R t
alg : ∀ x ∈ s \ t, IsAlgebraic (↥Rt) x
Rts : Subalgebra (↥Rt) S := adjoin (↥Rt) s
x✝ : Algebra ↥Rs ↥Rts := (Subalgebra.inclusion ⋯).toAlgebra
this✝¹ : IsScalarTower (↥Rs) (↥Rts) A
this✝ : Algebra.IsAlgebraic ↥Rt ↥Rts
this : IsAlgebraic (↥Rts) a
⊢ IsAlgebraic (↥Rt) a

Tactic:
exact this.restrictScalars Rt

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
p : PrimeSpectrum R
x✝ : p ∈ Set.range (comap f)
q : PrimeSpectrum S
hq : comap f q = p
⊢ Ideal.comap f (Ideal.map f p.asIdeal) = p.asIdeal

Tactic:
by simp [← hq]

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f✝ : R →+* S
hf : Function.Bijective ⇑f✝
f : R ≃+* S := RingEquiv.ofBijective f✝ hf
⊢ (mapPiLocalization (↑f) hf).comp (mapPiLocalization ↑f.symm ⋯) = RingHom.id (PiLocalization S)

Tactic:
← mapPiLocalization_comp

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f✝ : R →+* S
hf : Function.Bijective ⇑f✝
f : R ≃+* S := RingEquiv.ofBijective f✝ hf
⊢ mapPiLocalization ((↑f).comp ↑f.symm) ⋯ = RingHom.id (PiLocalization S)
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f✝ : R →+* S
hf : Function.Bijective ⇑f✝
f : R ≃+* S := RingEquiv.ofBijective f✝ hf
⊢ (mapPiLocalization ↑f.symm ⋯).comp (mapPiLocalization (↑f) hf) = RingHom.id (PiLocalization R)

Tactic:
← mapPiLocalization_comp

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f✝ : R →+* S
hf : Function.Bijective ⇑f✝
f : R ≃+* S := RingEquiv.ofBijective f✝ hf
⊢ mapPiLocalization ((↑f.symm).comp ↑f) ⋯ = RingHom.id (PiLocalization R)
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: R : Type u_1
S : Type u_2
P : Type u_3
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring P
f : R →+* S
g : S →+* P
x✝¹ : PiLocalization R
x✝ : PrimeSpectrum P
⊢ (mapPiLocalization (g.comp f)) x✝¹ x✝ = ((mapPiLocalization g).comp (mapPiLocalization f)) x✝¹ x✝

Tactic:
exact congr($(Localization.localRingHom_comp _ _ _ _ rfl _ rfl) _)

Goal state after:
Module: Mathlib.Topology.LocallyClosed

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
tfae_1_to_2 : IsLocallyClosed s → IsOpen[inst✝] (coborder s)
tfae_2_to_3 : IsOpen[inst✝] (coborder s) → ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)
h : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)
x : X
hx : x ∈ s
⊢ ∃ U, x ∈ U ∧ IsOpen[inst✝] U ∧ U ∩ closure[inst✝] s ⊆ s

Tactic:
by
    obtain ⟨t, ht, ht'⟩ := h x hx
    obtain ⟨U, hUt, hU, hxU⟩ := mem_nhds_iff.mp ht
    rw [isClosed_preimage_val] at ht'
    exact ⟨U, hxU, hU, (subset_inter (inter_subset_left.trans hUt) (hU.inter_closure.trans
      (closure_mono <| inter_subset_inter hUt subset_rfl))).trans ht'⟩

Goal state after:
Module: Mathlib.Topology.NoetherianSpace

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
⊢ NoetherianSpace α ↔ ∀ (s : Opens α), IsCompact ↑s

Tactic:
rw [NoetherianSpace, CompleteLattice.wellFoundedGT_iff_isSupFiniteCompact,
    CompleteLattice.isSupFiniteCompact_iff_all_elements_compact]
  exact forall_congr' Opens.isCompactElement_iff

Goal state after:
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: case inr.refine_2
X : Type u_6
Y : Type u_7
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
h : Continuous[inst✝², inst✝¹] f
ι : Type u_4
U : ι → Opens Y
hU : range f ⊆ ↑(iSup U)
V : ι → Type u_5
inst✝ : (i : ι) → TopologicalSpace (V i)
iV : (i : ι) → V i → X
hiV : ∀ (i : ι), Continuous[inst✝ i, inst✝²] (iV i)
hV : ∀ (i : ι), f ⁻¹' ↑(U i) ⊆ range (iV i)
hV' : ∀ (i : ι), IsEmbedding (f ∘ iV i)
this :
  ∀ {X : Type u_6} {Y : Type u_7} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y),
    Continuous f →
      ∀ {ι : Type u_4} (U : ι → Opens Y),
        range f ⊆ ↑(iSup U) →
          ∀ (V : ι → Type u_5) [inst_2 : (i : ι) → TopologicalSpace (V i)] (iV : (i : ι) → V i → X),
            (∀ (i : ι), Continuous (iV i)) →
              (∀ (i : ι), f ⁻¹' ↑(U i) ⊆ range (iV i)) →
                (∀ (i : ι), IsEmbedding (f ∘ iV i)) → iSup U = ⊤ → IsEmbedding f
hU' : ¬iSup U = ⊤
f₀ : X → ↑(range f) := fun x ↦ ⟨f x, ⋯⟩
hU'' : ⨆ i, (Opens.comap { toFun := Subtype.val, continuous_toFun := ⋯ }) (U i) = ⊤
⊢ range f₀ ⊆ ↑(⨆ i, (Opens.comap { toFun := Subtype.val, continuous_toFun := ⋯ }) (U i))

Tactic:
hU''

Goal state after:
case inr.refine_2
X : Type u_6
Y : Type u_7
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
h : Continuous[inst✝², inst✝¹] f
ι : Type u_4
U : ι → Opens Y
hU : range f ⊆ ↑(iSup U)
V : ι → Type u_5
inst✝ : (i : ι) → TopologicalSpace (V i)
iV : (i : ι) → V i → X
hiV : ∀ (i : ι), Continuous[inst✝ i, inst✝²] (iV i)
hV : ∀ (i : ι), f ⁻¹' ↑(U i) ⊆ range (iV i)
hV' : ∀ (i : ι), IsEmbedding (f ∘ iV i)
this :
  ∀ {X : Type u_6} {Y : Type u_7} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y),
    Continuous f →
      ∀ {ι : Type u_4} (U : ι → Opens Y),
        range f ⊆ ↑(iSup U) →
          ∀ (V : ι → Type u_5) [inst_2 : (i : ι) → TopologicalSpace (V i)] (iV : (i : ι) → V i → X),
            (∀ (i : ι), Continuous (iV i)) →
              (∀ (i : ι), f ⁻¹' ↑(U i) ⊆ range (iV i)) →
                (∀ (i : ι), IsEmbedding (f ∘ iV i)) → iSup U = ⊤ → IsEmbedding f
hU' : ¬iSup U = ⊤
f₀ : X → ↑(range f) := fun x ↦ ⟨f x, ⋯⟩
hU'' : ⨆ i, (Opens.comap { toFun := Subtype.val, continuous_toFun := ⋯ }) (U i) = ⊤
⊢ range f₀ ⊆ ↑⊤
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen[inst✝] U
⊢ IsCompact U → V ⊆ f '' s → IsOpen[inst✝] V → IsCompact V → IsCompact (U ∩ V)

Tactic:
hU''

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen[inst✝] U
hU'' : IsCompact U
⊢ V ⊆ f '' s → IsOpen[inst✝] V → IsCompact V → IsCompact (U ∩ V)
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
ht : IsQuasiSeparated t
h : s ⊆ t
U V : Set α
hU : U ⊆ s
hU' : IsOpen[inst✝] U
⊢ IsCompact U → V ⊆ s → IsOpen[inst✝] V → IsCompact V → IsCompact (U ∩ V)

Tactic:
hU''

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
ht : IsQuasiSeparated t
h : s ⊆ t
U V : Set α
hU : U ⊆ s
hU' : IsOpen[inst✝] U
hU'' : IsCompact U
⊢ V ⊆ s → IsOpen[inst✝] V → IsCompact V → IsCompact (U ∩ V)
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
h : IsOpenEmbedding f
s : Set α
H : IsQuasiSeparated (f '' s)
U V : Set α
hU : U ⊆ s
hU' : IsOpen[inst✝¹] U
⊢ IsCompact U → V ⊆ s → IsOpen[inst✝¹] V → IsCompact V → IsCompact (U ∩ V)

Tactic:
hU''

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
h : IsOpenEmbedding f
s : Set α
H : IsQuasiSeparated (f '' s)
U V : Set α
hU : U ⊆ s
hU' : IsOpen[inst✝¹] U
hU'' : IsCompact U
⊢ V ⊆ s → IsOpen[inst✝¹] V → IsCompact V → IsCompact (U ∩ V)
Module: Mathlib.Topology.QuasiSeparated

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

Tactic:
apply this (hf.subset (by grind)) ha <;> grind

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

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
K L : Compacts α
x : α
hxK : x ∈ ↑K
hxL : x ∈ ↑L
h : {x} ⊆ ↑K → {x} ⊆ ↑L → {x} ⊆ ↑⊥
⊢ x ∈ ∅

Tactic:
singleton_subset_iff

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
K L : Compacts α
x : α
hxK : x ∈ ↑K
hxL : x ∈ ↑L
h : x ∈ ↑K → x ∈ ↑L → x ∈ ↑⊥
⊢ x ∈ ∅
Module: Mathlib.Topology.Sets.Compacts

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : Nonempty α
⊢ ∃ x y, x ≠ y

Tactic:
obtain ⟨x⟩ := ‹Nonempty α›

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : Nonempty α
x : α
⊢ ∃ x y, x ≠ y
Module: Mathlib.Topology.Sober

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
x : α
S Z : Set α
h : IsGenericPoint x S
hZ : IsClosed Z
⊢ x ∈ Z ↔ {x} ⊆ Z

Tactic:
singleton_subset_iff

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
x : α
S Z : Set α
h : IsGenericPoint x S
hZ : IsClosed Z
⊢ x ∈ Z ↔ x ∈ Z
Module: Mathlib.Topology.Sober

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
x : α
S : Set α
hS : IsClosed S
hxS : x ∈ S
this : closure {x} ⊆ S
⊢ (∀ (t' : Set α), IsClosed t' → {x} ⊆ t' → S ⊆ t') ↔ ∀ (Z : Set α), IsClosed Z → x ∈ Z → S ⊆ Z

Tactic:
singleton_subset_iff

Goal state after:
Module: Mathlib.Topology.Sober

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
V W : Set α
inst✝ : QuasiSober ↑W
hV : IsClosed V
⊢ IsClosed (Subtype.val ⁻¹' V)

Tactic:
exact IsClosed.preimage_val hV

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
a : A
n : ℕ
ihn : D (a ^ n) = n • a ^ (n - 1) • D a
hpos : 0 < n
⊢ a ^ (n - 1 + 1) = a ^ n

Tactic:
Nat.sub_add_cancel hpos

Goal state after:
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
⊢ a ^ n = a ^ n
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
N : Type u_5
inst✝⁴ : AddCommMonoid N
inst✝³ : Module A N
inst✝² : Module R N
inst✝¹ : IsScalarTower R A M
inst✝ : IsScalarTower R A N
f : M →ₗ[A] N
e : M ≃ₗ[A] N
r : A
D : Derivation R A M
a✝ : A
⊢ f (r • D a✝) = r • f (D a✝)

Tactic:
simp only [_root_.map_smul]

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
hp : ∃ a ∈ s, a ∉ ↑p.asIdeal
hs : zeroLocus s = Uᶜ
⊢ ∃ v ∈ Set.range fun r ↦ ↑(basicOpen r), p ∈ v ∧ v ⊆ U

Tactic:
obtain ⟨f, hfs, hfp⟩ := hp

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
⊢ ∃ v ∈ Set.range fun r ↦ ↑(basicOpen r), p ∈ v ∧ v ⊆ U
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set R
⊢ ⨆ i ∈ s, basicOpen i = ⊤ ↔ Ideal.span s = ⊤

Tactic:
by
  conv_rhs => rw [← Subtype.range_val (s := s), ← iSup_basicOpen_eq_top_iff]
  simp

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

Goal state before:
pp: case pos
ι : 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
⊢ (Pi.single i f * x) i = 0 i

Tactic:
simp [hx]

Goal state after: