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

Goal state before:
pp: R : Type u
inst✝² : Semiring R
S : Type v
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Nontrivial S
p : S[X]
hlifts : p ∈ lifts f
hp : p.Monic
⊢ ∃ q, map f q = p ∧ q.degree = p.degree ∧ q.Monic

Tactic:
by
  rw [lifts_iff_coeff_lifts] at hlifts
  let g : ℕ → R := fun k ↦ (hlifts k).choose
  have hg k : f (g k) = p.coeff k := (hlifts k).choose_spec
  let q : R[X] := X ^ p.natDegree + ∑ k ∈ Finset.range p.natDegree, C (g k) * X ^ k
  have hq : map f q = p := by
    simp_rw [q, Polynomial.map_add, Polynomial.map_sum, Polynomial.map_mul, Polynomial.map_pow,
      map_X, map_C, hg, ← hp.as_sum]
  have h : q.Monic := monic_X_pow_add (by simp_rw [← Fin.sum_univ_eq_sum_range, degree_sum_fin_lt])
  exact ⟨q, hq, hq ▸ (h.degree_map f).symm, h⟩

Goal state after:
Module: Mathlib.Data.Nat.Choose.Vandermonde

Goal state before:
pp: m n k : ℕ
⊢ ((X + 1) ^ m * (X + 1) ^ n).coeff k = ∑ ij ∈ antidiagonal k, m.choose ij.1 * n.choose ij.2

Tactic:
by
      rw [coeff_mul, Finset.sum_congr rfl]
      simp only [coeff_X_add_one_pow, cast_id, imp_true_iff]

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
A : Matrix n n R
h : IsUnit A
this : Invertible A
⊢ C A⁻¹.det * (C.mapMatrix A * ((scalar n) X - C.mapMatrix A⁻¹)).det =
    C A⁻¹.det * (C.mapMatrix A * (scalar n) X - 1).det

Tactic:
rw [mul_sub, ← map_mul]; simp

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
hM : IsNilpotent M
a✝ : Nontrivial R
p : R[X] := M.charpolyRev
| p - 1

Tactic:
rw [← modByMonic_add_div p X]

Goal state after:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
hM : IsNilpotent M
a✝ : Nontrivial R
p : R[X] := M.charpolyRev
| p %ₘ X + X * (p /ₘ X) - 1
Module: Mathlib.Algebra.Polynomial.HasseDeriv

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
D : ℕ → R[X] →+ R[X] := fun k ↦ (hasseDeriv k).toAddMonoidHom
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
x : ℕ × ℕ
hm : x.1 ≤ m
hn : x.2 ≤ n
⊢ (monomial (m + n - x.2 - x.1)) (↑(m.choose x.1) * r * (↑(n.choose x.2) * s)) =
    (monomial (m + n - (x.1 + x.2))) (↑(m.choose x.1) * ↑(n.choose x.2) * (r * s))

Tactic:
← tsub_add_eq_tsub_tsub,

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
D : ℕ → R[X] →+ R[X] := fun k ↦ (hasseDeriv k).toAddMonoidHom
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
x : ℕ × ℕ
hm : x.1 ≤ m
hn : x.2 ≤ n
⊢ (monomial (m + n - (x.2 + x.1))) (↑(m.choose x.1) * r * (↑(n.choose x.2) * s)) =
    (monomial (m + n - (x.1 + x.2))) (↑(m.choose x.1) * ↑(n.choose x.2) * (r * s))
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.Algebra.Polynomial.Splits

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p : R[X]
hp : p.Splits
r : R
this : ∀ (i : R), (X + C r + C i).Splits
⊢ ((Polynomial.taylor r) p).Splits

Tactic:
induction hp using Submonoid.closure_induction <;> aesop

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
S : Type u_4
inst✝¹ : CommRing S
inst✝ : IsDomain S
f : R[X]
hf : f.Splits
φ : R →+* S
hφ : map φ f ≠ 0
⊢ (map φ f).roots = Multiset.map (⇑φ) f.roots

Tactic:
by
  induction hf using Submonoid.closure_induction with
  | mem p hp => obtain (⟨r, rfl⟩ | ⟨a, rfl⟩) := hp <;> simp
  | one => simp
  | mul x y _ _ hx hy => simp_all [roots_mul, show x * y ≠ 0 by aesop]

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
S : Type u_4
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : Algebra S B
inst✝² : IsScalarTower R S B
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A B
isIntegral : Algebra.IsIntegral R S
x : R
⊢ mk' A ((algebraMap S B) ((algebraMap R S) x)) ⋯ = (algebraMap R A) x

Tactic:
simp_rw [← IsScalarTower.algebraMap_apply, mk'_algebraMap]

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

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

Tactic:
rw [mk_ker]

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

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type v
inst✝ : Nonempty ι
⊢ FaithfullyFlat R (ι →₀ R)

Tactic:
by
  classical exact of_linearEquiv _ _ (finsuppLEquivDirectSum R R ι)

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
t t' : Set (PrimeSpectrum R)
f : R
hf : ∀ x ∈ t, f ∈ x.asIdeal
g : R
hg : ∀ x ∈ t', g ∈ x.asIdeal
x : PrimeSpectrum R
hxt : x ∈ t
hxt' : x ∈ t'
⊢ f + g ∈ x.asIdeal

Tactic:
apply Submodule.add_mem

Goal state after:
case h₁
R : Type u
inst✝ : CommSemiring R
t t' : Set (PrimeSpectrum R)
f : R
hf : ∀ x ∈ t, f ∈ x.asIdeal
g : R
hg : ∀ x ∈ t', g ∈ x.asIdeal
x : PrimeSpectrum R
hxt : x ∈ t
hxt' : x ∈ t'
⊢ f ∈ x.asIdeal

case h₂
R : Type u
inst✝ : CommSemiring R
t t' : Set (PrimeSpectrum R)
f : R
hf : ∀ x ∈ t, f ∈ x.asIdeal
g : R
hg : ∀ x ∈ t', g ∈ x.asIdeal
x : PrimeSpectrum R
hxt : x ∈ t
hxt' : x ∈ t'
⊢ g ∈ x.asIdeal
Module: Mathlib.RingTheory.Spectrum.Prime.RingHom

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
hf : Function.Surjective (comap f)
x : R
hfx : IsUnit (f x)
hx : ¬IsUnit x
p : Ideal R
hp : p.IsMaximal
right✝ : x ∈ p
q : Ideal S
hqp : q.IsPrime
hq : Ideal.comap f q = p
⊢ False

Tactic:
exact hqp.ne_top (q.eq_top_of_isUnit_mem (q.mem_comap.mp (by rwa [hq])) hfx)

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
a✝ b✝ c✝ : α
⊢ le a✝ b✝ → le b✝ c✝ → le a✝ c✝

Tactic:
hab

Goal state after:
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
a✝ b✝ c✝ : α
hab : le a✝ b✝
⊢ le b✝ c✝ → le a✝ c✝
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
a✝ b✝ : α
⊢ le a✝ b✝ → le b✝ a✝ → a✝ = b✝

Tactic:
hab

Goal state after:
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
a✝ b✝ : α
hab : le a✝ b✝
⊢ le b✝ a✝ → a✝ = b✝
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)
inst✝ : Infinite ι
surj : Function.Surjective ⇑(toPiLocalization ((i : ι) → R i))
J : Ideal ((i : ι) → R i)
max : J.IsMaximal
notMem : { asIdeal := J, isPrime := ⋯ } ∉ Set.range (PrimeSpectrum.sigmaToPi R)
r : (i : ι) → R i
hr : (toPiLocalization ((i : ι) → R i)) r = Function.update 0 { asIdeal := J, isMaximal := max } 1
this : r = 0
⊢ False

Tactic:
replace hr := congr_fun hr ⟨J, max⟩

Goal state after:
ι : Type u_5
R : ι → Type u_4
inst✝² : (i : ι) → CommSemiring (R i)
inst✝¹ : ∀ (i : ι), Nontrivial (R i)
inst✝ : Infinite ι
surj : Function.Surjective ⇑(toPiLocalization ((i : ι) → R i))
J : Ideal ((i : ι) → R i)
max : J.IsMaximal
notMem : { asIdeal := J, isPrime := ⋯ } ∉ Set.range (PrimeSpectrum.sigmaToPi R)
r : (i : ι) → R i
this : r = 0
hr :
  (toPiLocalization ((i : ι) → R i)) r { asIdeal := J, isMaximal := max } =
    Function.update 0 { asIdeal := J, isMaximal := max } 1 { asIdeal := J, isMaximal := max }
⊢ False
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
surj✝ : Function.Surjective ⇑(toPiLocalization R)
surj : Function.Surjective (⇑(mapPiLocalization (toPiLocalization R).toRingHom ⋯) ∘ ⇑(toPiLocalization R))
⊢ Finite (MaximalSpectrum R)

Tactic:
← AlgHom.coe_toRingHom,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
surj✝ : Function.Surjective ⇑(toPiLocalization R)
surj : Function.Surjective (⇑(mapPiLocalization (toPiLocalization R).toRingHom ⋯) ∘ ⇑↑(toPiLocalization R))
⊢ Finite (MaximalSpectrum R)
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)
inst✝ : Infinite ι
surj : Function.Surjective ⇑(toPiLocalization ((i : ι) → R i))
⊢ Function.Surjective ⇑(MaximalSpectrum.toPiLocalization ((i : ι) → R i))

Tactic:
← AlgHom.coe_toRingHom,

Goal state after:
ι : Type u_5
R : ι → Type u_4
inst✝² : (i : ι) → CommSemiring (R i)
inst✝¹ : ∀ (i : ι), Nontrivial (R i)
inst✝ : Infinite ι
surj : Function.Surjective ⇑(toPiLocalization ((i : ι) → R i))
⊢ Function.Surjective ⇑↑(MaximalSpectrum.toPiLocalization ((i : ι) → R i))
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
surj : Function.Surjective (⇑(mapPiLocalization (toPiLocalization R).toRingHom) ∘ ⇑(toPiLocalization R))
⊢ Finite (PrimeSpectrum R)

Tactic:
← AlgHom.coe_toRingHom,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
surj : Function.Surjective (⇑(mapPiLocalization (toPiLocalization R).toRingHom) ∘ ⇑↑(toPiLocalization R))
⊢ Finite (PrimeSpectrum R)
Module: Mathlib.Topology.Sets.Opens

Goal state before:
pp: case mpr.refine_1
α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
h : ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U' ∈ B, x ∈ U' ∧ U' ≤ U
⊢ ∀ u ∈ SetLike.coe '' B, IsOpen[inst✝] u

Tactic:
rintro sU ⟨U, -, rfl⟩

Goal state after:
case mpr.refine_1
α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
h : ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U' ∈ B, x ∈ U' ∧ U' ≤ U
U : Opens α
⊢ IsOpen[inst✝] ↑U
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 : α
⊢ ∃ x y, x ≠ y

Tactic:
exact ⟨⊥, {x}, ne_of_apply_ne SetLike.coe (Set.empty_ne_singleton x)⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
⊢ Subsingleton (Compacts α) ↔ IsEmpty α

Tactic:
by
  refine ⟨fun h => ?_, fun _ => inferInstance⟩
  contrapose! h
  infer_instance

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: case cons
X : Type u_2
inst✝ : TopologicalSpace X
ι : Type u_4
t : ι → Set X
i : ι
s : Finset ι
ih : i ∉ s
hi : (∀ i ∈ s, IsRetrocompact (t i)) → IsRetrocompact (s.sup t)
ht : ∀ i_1 ∈ Finset.cons i s ih, IsRetrocompact (t i_1)
⊢ IsRetrocompact (t i ⊔ s.sup t)

Tactic:
exact (ht _ <| by simp).union <| hi <| Finset.forall_of_forall_cons ht

Goal state after:
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✝ : Subsingleton α
⊢ Subsingleton (NonemptyCompacts α)

Tactic:
refine ⟨fun K L => NonemptyCompacts.ext ?_⟩
  rw [Subsingleton.eq_univ_of_nonempty K.nonempty, Subsingleton.eq_univ_of_nonempty L.nonempty]

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
⊢ IsConstructible s

Tactic:
by
  have (x : _) : ∃ U, IsOpen U ∧ IsCompact U ∧ x ∈ U ∧ IsConstructible (U ∩ s) :=
    have ⟨U, hxU, hU, hUs⟩ := hs x
    have ⟨V, ⟨hV₁, hV₂⟩, hxV, hVU⟩ := PrespectralSpace.isTopologicalBasis.mem_nhds_iff.mp hxU
    have : IsConstructible (V ↓∩ s) :=
      (hUs.preimage_of_isOpenEmbedding (IsOpenEmbedding.id.restrict hVU hV₁) :)
    have : IsConstructible (V ∩ s) := by
      have := this.image_of_isOpenEmbedding hV₁.isOpenEmbedding_subtypeVal
        (by simpa using hV₂.isRetrocompact hV₁)
      rwa [Subtype.image_preimage_coe] at this
    ⟨V, hV₁, hV₂, hxV, this⟩
  choose U hU hU' hxU hUs using this
  obtain ⟨σ, hσ, htσ⟩ := ht.elim_nhds_subcover U (fun x _ ↦ (hU x).mem_nhds (hxU x))
  convert! IsConstructible.biUnion σ.finite_toSet (fun x _ ↦ hUs x)
  apply subset_antisymm
  · rw [← Set.iUnion₂_inter, Set.subset_inter_iff]
    exact ⟨hst.trans htσ, subset_rfl⟩
  · exact Set.iUnion₂_subset fun _ _ ↦ Set.inter_subset_right

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

Goal state before:
pp: 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
hI✝ : I ^ 2 = ⊥
inst✝ : IsScalarTower R A B
hI : I ^ 2 = ⊥
f : Derivation R A ↥I
x y : A
⊢ ↑(f (x * y)) + (algebraMap A B) (x * y) = (↑(f x) + (algebraMap A B) x) * (↑(f y) + (algebraMap A B) y)

Tactic:
by
      have : (f x : B) * f y = 0 := by
        rw [← Ideal.mem_bot, ← hI, pow_two]
        convert! Ideal.mul_mem_mul (f x).2 (f y).2 using 1
      simp only [map_mul, f.leibniz, add_mul, mul_add, Submodule.coe_add,
        Submodule.coe_smul_of_tower, Algebra.smul_def, this]
      ring

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
inst✝ : (Ideal.comap f P).IsPrime
algInst✝¹ : Algebra R S := f.toAlgebra
algInst✝ : Algebra (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P) :=
  (Localization.localRingHom (Ideal.comap f P) P f ⋯).toAlgebra
algebraizeInst✝ : Module.Flat R S
this : IsScalarTower R (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P)
⊢ (Localization.localRingHom (Ideal.comap f P) P f ⋯).Flat

Tactic:
rw [RingHom.Flat, Module.flat_iff_of_isLocalization
    (S := (Localization.AtPrime (Ideal.comap f P))) (p := (Ideal.comap f P).primeCompl)]

Goal state after:
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
inst✝ : (Ideal.comap f P).IsPrime
algInst✝¹ : Algebra R S := f.toAlgebra
algInst✝ : Algebra (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P) :=
  (Localization.localRingHom (Ideal.comap f P) P f ⋯).toAlgebra
algebraizeInst✝ : Module.Flat R S
this : IsScalarTower R (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P)
⊢ Module.Flat R (Localization.AtPrime P)
Module: Mathlib.RingTheory.RingHom.Flat

Goal state before:
pp: ⊢ flat.IsStableUnderCobaseChange

Tactic:
flat,

Goal state after:
⊢ (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] f ↦ f.Flat).IsStableUnderCobaseChange
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
t : Set (PrimeSpectrum R)
I : Set R
hI : closure t = zeroLocus I
⊢ t ⊆ closure t ∧ t ⊆ zeroLocus ↑(vanishingIdeal t)

Tactic:
exact ⟨subset_closure, subset_zeroLocus_vanishingIdeal t⟩

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
ι : Type u_1
f : ι → R
⊢ (zeroLocus (⋃ i, {f i}))ᶜ = Set.univ ↔ zeroLocus ↑(Ideal.span (Set.range f)) = ∅

Tactic:
compl_involutive.eq_iff

Goal state after:
R : Type u
inst✝ : CommSemiring R
ι : Type u_1
f : ι → R
⊢ zeroLocus (⋃ i, {f i}) = Set.univᶜ ↔ zeroLocus ↑(Ideal.span (Set.range f)) = ∅
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
hpα : p ∣ Nat.card α
a : α
ha : a ∈ fixedPoints G α
hpf : p ∣ Nat.card ↑(fixedPoints G α)
hα : Nontrivial ↑(fixedPoints G α)
b : α
hb : b ∈ fixedPoints G α
hba : ⟨b, hb⟩ ≠ ⟨a, ha⟩
hab : a = b
⊢ ⟨b, hb⟩ = ⟨a, ha⟩

Tactic:
hab

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
inst✝¹ : Nontrivial G
inst✝ : Finite G
⊢ Nontrivial ↥(Subgroup.center G)

Tactic:
have := (hG.of_equiv ConjAct.toConjAct).exists_fixed_point_of_prime_dvd_card_of_fixed_point G

Goal state after:
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
inst✝¹ : Nontrivial G
inst✝ : Finite G
this : p ∣ Nat.card G → ∀ {a : G}, a ∈ fixedPoints (ConjAct G) G → ∃ b ∈ fixedPoints (ConjAct G) G, a ≠ b
⊢ Nontrivial ↥(Subgroup.center G)
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case pos
G : Type u
inst✝ : CommMonoid G
h : ∃ g, orderOf g = 0
⊢ exponent G = 0

Tactic:
obtain ⟨g, hg⟩ := h
    exact exponent_eq_zero_of_order_zero hg

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x y : R
hx : IsIdempotentElem x
hs : IsClopen ↑(basicOpen x)
hy : IsIdempotentElem y
eq : ↑(basicOpen x) = ↑(basicOpen y)
⊢ x = y

Tactic:
exact basicOpen_injOn_isIdempotentElem hx hy (SetLike.ext' eq)

Goal state after:
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 = ↑(basicOpen e)

Tactic:
refine ⟨fun h ↦ ?_, ?_⟩
  · have ⟨e, f, h⟩ := exists_mul_eq_zero_add_eq_one_basicOpen_eq_of_isClopen h
    exact ⟨e, f, by simp only [h, and_self]⟩
  rintro ⟨e, f, mul, add, rfl⟩
  exact isClopen_basicOpen_of_mul_add e f mul add

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
⊢ Function.Bijective fun e ↦ { carrier := ↑(basicOpen (↑e).1), isClopen' := ⋯ }

Tactic:
by
      refine ⟨fun ⟨x, hx⟩ ⟨y, hy⟩ eq ↦ mul_eq_zero_add_eq_one_ext_left ?_, fun s ↦ ?_⟩
      · exact basicOpen_injOn_isIdempotentElem (IsIdempotentElem.of_mul_add hx.1 hx.2).1
          (IsIdempotentElem.of_mul_add hy.1 hy.2).1 <| SetLike.ext' (congr_arg (·.1) eq)
      · have ⟨e, f, mul, add, eq⟩ := isClopen_iff_mul_add.mp s.2
        exact ⟨⟨(e, f), mul, add⟩, SetLike.ext' eq.symm⟩

Goal state after:
Module: Mathlib.GroupTheory.Rank

Goal state before:
pp: G : Type u_1
inst✝ : Group G
g : G
⊢ Nat.card ↥(centralizer {g}) = Nat.card ↥(MulAction.stabilizer (ConjAct G) g)

Tactic:
centralizer_eq_comap_stabilizer

Goal state after:
G : Type u_1
inst✝ : Group G
g : G
⊢ Nat.card ↥(comap ConjAct.toConjAct.toMonoidHom (MulAction.stabilizer (ConjAct G) g)) =
    Nat.card ↥(MulAction.stabilizer (ConjAct G) g)
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: case succ
G : Type u_1
inst✝ : CommMonoid G
p : ℕ
hp : Fact (Nat.Prime p)
p' : ℕ
hp' : Fact (Nat.Prime p')
hne : p ≠ p'
g : G
hg' : ∃ n, orderOf g = p' ^ n
n : ℕ
hn : orderOf g = p ^ (n + 1)
⊢ g = 1

Tactic:
obtain ⟨_, hn'⟩ := hg'

Goal state after:
case succ
G : Type u_1
inst✝ : CommMonoid G
p : ℕ
hp : Fact (Nat.Prime p)
p' : ℕ
hp' : Fact (Nat.Prime p')
hne : p ≠ p'
g : G
n : ℕ
hn : orderOf g = p ^ (n + 1)
w✝ : ℕ
hn' : orderOf g = p' ^ w✝
⊢ g = 1
Module: Mathlib.RingTheory.SimpleModule.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set ι
p : ι → Submodule R M
hp : ∀ i ∈ s, IsSemisimpleModule R ↥(p i)
⊢ IsSemisimpleModule R ↥(⨆ i ∈ s, p i)

Tactic:
refine isSemisimpleModule_of_isSemisimpleModule_submodule
    ((comap_equiv_self_of_inj_of_le (injective_subtype _) ?_).isSemisimpleModule_iff.mpr <| hp · ·)
    (biSup_comap_subtype_eq_top ..)
  simp_rw [range_subtype, le_biSup p ‹_›]

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

Goal state before:
pp: ι✝ : Type u_1
R : Type u_2
S : Type u_3
inst✝⁹ : Ring R
inst✝⁸ : Ring S
M✝ : Type u_4
inst✝⁷ : AddCommGroup M✝
inst✝⁶ : Module R M✝
m : Submodule R M✝
N : Type u_5
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι : Type u_7
inst✝³ : Finite ι
M : ι → Type u_6
inst✝² : (i : ι) → AddCommGroup (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : ∀ (i : ι), IsSemisimpleModule R (M i)
⊢ IsSemisimpleModule R ((i : ι) → M i)

Tactic:
exact isSemisimpleModule_of_isSemisimpleModule_submodule' (p := (range <| single _ _ ·))
    (fun i ↦ .range _) (by simp_rw [range_eq_map, Submodule.iSup_map_single, Submodule.pi_top])

Goal state after:
Module: Mathlib.RingTheory.ReesAlgebra

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
a✝ b✝ : R[X]
hf : a✝ ∈ {f | ∀ (i : ℕ), f.coeff i ∈ I ^ i}
hg : b✝ ∈ {f | ∀ (i : ℕ), f.coeff i ∈ I ^ i}
i : ℕ
⊢ ∑ x ∈ Finset.antidiagonal i, a✝.coeff x.1 * b✝.coeff x.2 ∈ I ^ i

Tactic:
apply Ideal.sum_mem

Goal state after:
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
a✝ b✝ : R[X]
hf : a✝ ∈ {f | ∀ (i : ℕ), f.coeff i ∈ I ^ i}
hg : b✝ ∈ {f | ∀ (i : ℕ), f.coeff i ∈ I ^ i}
i : ℕ
⊢ ∀ c ∈ Finset.antidiagonal i, a✝.coeff c.1 * b✝.coeff c.2 ∈ I ^ i
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
r : R
h : (Ideal.span {r}).IsTwoSided
hM : IsTorsionBy R M r
⊢ IsTorsionBySet R M ↑(Ideal.span {r})

Tactic:
← isTorsionBySet_span_singleton_iff

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
r : R
h : (Ideal.span {r}).IsTwoSided
hM : IsTorsionBySet R M ↑(R ∙ r)
⊢ IsTorsionBySet R M ↑(Ideal.span {r})
Module: Mathlib.RingTheory.Nakayama

Goal state before:
pp: case a
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N N' P : Submodule R M
hN' : N'.FG
hN'le : N' ≤ P
hNN' : P ≤ N ⊔ I • N'
hNN'' : P ≤ N ⊔ N'
h1 : map N.mkQ P = map N.mkQ N'
⊢ map N.mkQ (I • N') ≤ map N.mkQ P

Tactic:
rw [h1]

Goal state after:
case a
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N N' P : Submodule R M
hN' : N'.FG
hN'le : N' ≤ P
hNN' : P ≤ N ⊔ I • N'
hNN'' : P ≤ N ⊔ N'
h1 : map N.mkQ P = map N.mkQ N'
⊢ map N.mkQ (I • N') ≤ map N.mkQ N'
Module: Mathlib.RingTheory.Nakayama

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s : Set (M ⧸ I • N)
hN : N.FG
hIjac : I ≤ ⊥.jacobson
hsspan : span R s = map (I • N).mkQ N
⊢ ∃ t, Set.InjOn (⇑(I • N).mkQ) t ∧ ⇑(I • N).mkQ '' t = s ∧ span R t = N

Tactic:
use Quotient.out '' s

Goal state after:
case h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s : Set (M ⧸ I • N)
hN : N.FG
hIjac : I ≤ ⊥.jacobson
hsspan : span R s = map (I • N).mkQ N
⊢ Set.InjOn (⇑(I • N).mkQ) (Quotient.out '' s) ∧ ⇑(I • N).mkQ '' Quotient.out '' s = s ∧ span R (Quotient.out '' s) = N