mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
n : ℕ
x✝ : Γ
⊢ 0 < orderTop 0

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
hx : 0 < x.orderTop
⊢ (powers x).hsum - (powers x - ofFinsupp (Finsupp.single 0 1)).hsum = 1

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
hR : HenselianLocalRing R
f : R[X]
⊢ f.Monic →
    ∀ (a₀ : R),
      Polynomial.eval a₀ f ∈ maximalIdeal R →
        IsUnit ((Ideal.Quotient.mk (maximalIdeal R)) (Polynomial.eval a₀ (derivative f))) →
          ∃ a, f.IsRoot a ∧ a - a₀ ∈ maximalIdeal R

Tactic:
hf

Goal state after:
R : Type u_1
inst✝ : CommRing R
hR : HenselianLocalRing R
f : R[X]
hf : f.Monic
⊢ ∀ (a₀ : R),
    Polynomial.eval a₀ f ∈ maximalIdeal R →
      IsUnit ((Ideal.Quotient.mk (maximalIdeal R)) (Polynomial.eval a₀ (derivative f))) →
        ∃ a, f.IsRoot a ∧ a - a₀ ∈ maximalIdeal R
Module: Mathlib.RingTheory.HopfAlgebra.Quotient

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : HopfAlgebra R A
inst✝ : HopfAlgebraStruct R B
g : A →ₐ[R] B
a : A
⊢ (g.toLinearMap ∘ₗ ofConv 1) a = (ofConv 1) a

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.HopfAlgebra.Quotient

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : HopfAlgebra R A
inst✝ : HopfAlgebraStruct R B
g : A →ₗc[R] B
a : A
⊢ (ofConv 1 ∘ₗ g.toLinearMap) a = (ofConv 1) a

Tactic:
simp

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

Goal state before:
pp: case inl
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : Algebra.HasGoingUp R S
p : Ideal R
P : Ideal S
inst✝² : P.IsPrime
inst✝¹ : P.LiesOver p
inst✝ : p.IsPrime
hle : p ≤ p
⊢ ∃ Q, P ≤ Q ∧ Q.IsPrime ∧ Q.LiesOver p

pp: case inr
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : Algebra.HasGoingUp R S
p q : Ideal R
inst✝² : q.IsPrime
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : P.LiesOver p
hle : p ≤ q
h : p ≠ q
⊢ ∃ Q, P ≤ Q ∧ Q.IsPrime ∧ Q.LiesOver q

Tactic:
· use P

Goal state after:
case inr
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : Algebra.HasGoingUp R S
p q : Ideal R
inst✝² : q.IsPrime
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : P.LiesOver p
hle : p ≤ q
h : p ≠ q
⊢ ∃ Q, P ≤ Q ∧ Q.IsPrime ∧ Q.LiesOver q
Module: Mathlib.RingTheory.HopfAlgebra.MonoidAlgebra

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
a : A
⊢ AddMonoidAlgebra.single (-0) ((antipode R) a) = C ((antipode R) a)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.HopfAlgebra.Quotient

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : HopfAlgebraStruct R A
I : Ideal A
inst✝¹ : I.IsTwoSided
inst✝ : Ideal.IsHopfIdeal R I
x✝ : A
⊢ (antipode R ∘ₗ (mkₐ R I).toLinearMap) x✝ = ((mkₐ R I).toLinearMap ∘ₗ antipode R) x✝

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
I : Ideal R
hp✝ : maximalIdeal R ∈ I.minimalPrimes
hp : I.IsMinimalPrime (maximalIdeal R)
J : Ideal (R ⧸ I)
prime : J.IsPrime
this : (Ideal.comap (Ideal.Quotient.mk I) J).IsPrime
⊢ I ≤ RingHom.ker (algebraMap R (R ⧸ I))

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsNoetherianRing R
x : R
hx : Prime x
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization.Away x S
⊢ UniqueFactorizationMonoid R ↔ UniqueFactorizationMonoid S

Tactic:
have : IsDomain S := IsLocalization.Away.isDomain S hx.ne_zero
  refine ⟨fun _ ↦ of_isLocalization (Submonoid.powers x) S, fun _ ↦ ?_⟩
  rw [iff_forall_isPrincipal_of_height_eq_one]
  intro p hp h1
  by_cases hxp : x ∈ p
  · exact ⟨x, p.eq_span_singleton_of_height_eq_one h1 hxp hx⟩
  · have hd := by rwa [← Ideal.disjoint_powers_iff_notMem_of_isPrime x] at hxp
    have := IsLocalization.isPrime_of_isPrime_disjoint (Submonoid.powers x) S p hp hd
    refine p.isPrincipal_of_isPrincipal_isLocalizationAway_of_prime hx hxp S
      (isPrincipal_of_height_eq_one ?_)
    rw [← IsLocalization.height_under (Submonoid.powers x),
      IsLocalization.under_map_of_isPrime_disjoint (Submonoid.powers x) S hp hd, h1]

Goal state after:
Module: Mathlib.RingTheory.IdealFilter.Topology

Goal state before:
pp: A : Type u_1
inst✝ : Ring A
F : IdealFilter A
⊢ F.IsUniform ↔ ∃ B, B.sets = {x | ∃ I ∈ F, ↑I = x}

Tactic:
refine ⟨fun _ ↦ ⟨F.ringFilterBasis, rfl⟩, fun ⟨B, hB⟩ ↦ ⟨fun {I} hI a ↦ ?_⟩⟩
  obtain ⟨V, hbasis, hsub⟩ := B.mul_right a (U := I) (hB.ge (by simpa))
  obtain ⟨J, hJ, rfl⟩ := hB.le hbasis
  exact Order.PFilter.mem_of_le (fun x hx ↦ by simpa using (hsub hx)) hJ

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

Goal state before:
pp: A : Type u_1
inst✝ : Ring A
F : IdealFilter A
h₁ : F.IsUniform
h₂ : F • F = F
I J : Ideal A
hJ : J ∈ F
hcolon : ∀ x ∈ J, Submodule.colon I {x} ∈ F
x : A
hx : x ∈ J
⊢ Submodule.colon I {x} ≤ Submodule.colon (OrderDual.ofDual (OrderDual.toDual I)) {x}

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
h : FG (R ∙ e)
⊢ e + (1 - e) = 1

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
x : R
hx' : ¬IsUnit x
⊢ (span {x}).height ≤ 1

Tactic:
obtain ⟨p, hp⟩ := (span {x}).nonempty_minimalPrimes (by simpa)

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
x : R
hx' : ¬IsUnit x
p : Ideal R
hp : p ∈ (span {x}).minimalPrimes
⊢ (span {x}).height ≤ 1
Module: Mathlib.RingTheory.Ideal.Pure

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
h : FG (R ∙ e)
this : Module.Flat R ((R ⧸ R ∙ e) × R ⧸ span {1 - e})
⊢ LinearMap.fst R (R ⧸ R ∙ e) (R ⧸ span {1 - e}) ∘ₗ LinearMap.inl R (R ⧸ R ∙ e) (R ⧸ span {1 - e}) = LinearMap.id

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
h : ∀ x ∈ I, ∃ y ∈ I, x = x * y
p : Ideal R
inst✝ : p.IsPrime
hle : I ≤ p
x : R
hx : x ∈ I
y : R
hy : y ∈ I
heq : x = x * y
⊢ 1 - y ∣ 1 - y

Tactic:
simp

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.Pure
⊢ ⨅ i, RingHom.ker (algebraMap R (Localization.AtPrime (↑i).asIdeal)) ≤ I

Tactic:
refine le_trans ?_ I.iInf_ker_le

Goal state after:
case refine_1
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.Pure
⊢ ⨅ i, RingHom.ker (algebraMap R (Localization.AtPrime (↑i).asIdeal)) ≤
    ⨅ p, ⨅ (x : p.IsPrime), ⨅ (_ : I ≤ p), RingHom.ker (algebraMap R (Localization.AtPrime p))
Module: Mathlib.RingTheory.KrullDimension.PID

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
m : Ideal R
inst✝ : m.IsMaximal
h : ¬IsField R
⊢ 1 = ⊥.height + 1

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
r : R
p : Ideal R
inst✝ : p.IsPrime
hrm : r ∈ p
⊢ 1 = {r}.encard

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
r : R
p : Ideal R
inst✝ : p.IsPrime
hrp : r ∈ p
⊢ 1 = ↑{r}.encard

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
a✝ : Nontrivial R[X]
M : Ideal R[X]
hM : M.IsMaximal
⊢ ↑M.height ≤ ringKrullDim R + 1

Tactic:
rw [height_eq_height_add_one (M.under R) M, WithBot.coe_add, WithBot.coe_one]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
a✝ : Nontrivial R[X]
M : Ideal R[X]
hM : M.IsMaximal
⊢ ↑(under R M).height + 1 ≤ ringKrullDim R + 1
Module: Mathlib.RingTheory.KrullDimension.Polynomial

Goal state before:
pp: case h_empty
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
ι : Type u_2
inst✝ : Finite ι
⊢ ringKrullDim (MvPolynomial PEmpty.{u_2 + 1} R) = ringKrullDim R + ↑(Nat.card PEmpty.{u_2 + 1})

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.KrullDimension.Regular

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
x : R
h : x ∈ (annihilator R M).jacobson
a✝ : Nontrivial M
p : LTSeries ↑(support R M)
hxp : x ∈ (↑(RelSeries.last p)).asIdeal
q : LTSeries (PrimeSpectrum R)
hxq : x ∈ (q.toFun 1).asIdeal
hq : (p.map Subtype.val ⋯).length = q.length
h0 : ↑(RelSeries.head p) = RelSeries.head q
right✝ : RelSeries.last (p.map Subtype.val ⋯) = RelSeries.last q
hp0 : ¬p.length = 0
x✝ : Fin (p.length - 1)
⊢ ⟨↑x✝.castSucc + 1, ⋯⟩ < ⟨↑x✝.succ + 1, ⋯⟩

Tactic:
simp

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝⁸ : CommRing R
inst✝⁷ : IsNoetherianRing R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsNoetherianRing S
inst✝³ : Algebra.HasGoingDown R S
p : Ideal R
inst✝² : p.IsPrime
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : P.LiesOver p
lp : LTSeries (PrimeSpectrum R)
hlp : RelSeries.last lp = { asIdeal := p, isPrime := ⋯ }
hlenp : ↑lp.length = p.height
lq : LTSeries (PrimeSpectrum (S ⧸ map (algebraMap R S) p))
hlq : RelSeries.last lq = { asIdeal := map (Quotient.mk (map (algebraMap R S) p)) P, isPrime := ⋯ }
hlenq : ↑lq.length = (map (Quotient.mk (map (algebraMap R S) p)) P).height
l' : LTSeries (PrimeSpectrum S) := lq.map (PrimeSpectrum.comap (Quotient.mk (map (algebraMap R S) p))) ⋯
⊢ map (Quotient.mk (map (algebraMap R S) p)) (map (algebraMap R S) p) ≤ (RelSeries.head lq).asIdeal

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.KrullDimension.Regular

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
x : R
hn : ∀ p ∈ (annihilator R M).minimalPrimes, x ∉ p
a✝¹ : Nontrivial M
a✝ : Nontrivial (QuotSMulTop x M)
this✝ : Nonempty ↑(support R M)
this : Nonempty ↑(support R (QuotSMulTop x M))
p : LTSeries ↑(support R (QuotSMulTop x M))
hp : ↑(RelSeries.head p) ∈ support R M ∧ x ∈ ↑(↑(RelSeries.head p)).asIdeal
⊢ support R (QuotSMulTop x M) ⊆ support R M

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
x : R
n : ℕ
hn :
  ∀ (p : LTSeries (PrimeSpectrum R)),
    x ∈ (RelSeries.last p).asIdeal →
      p.length = n →
        ∃ q,
          x ∈ (q.toFun 1).asIdeal ∧
            n = q.length ∧ RelSeries.head p = RelSeries.head q ∧ RelSeries.last p = RelSeries.last q
p : LTSeries (PrimeSpectrum R)
hx✝ : x ∈ (RelSeries.last p).asIdeal
hp : p.length = n + 1
h0 : ¬n = 0
q : PrimeSpectrum R
hxq : x ∈ q.asIdeal
h2 : p.toFun ⟨p.length - 2, ⋯⟩ < q
hq : q < RelSeries.last p
Q : LTSeries (PrimeSpectrum R)
hx : x ∈ (Q.toFun 1).asIdeal
hQ : n = Q.length
hh : ((RelSeries.eraseLast p).eraseLast.snoc q h2).head = RelSeries.head Q
hl : ((RelSeries.eraseLast p).eraseLast.snoc q h2).last = RelSeries.last Q
h1 : 1 < Q.length + 1
h : 1 = Fin.castSucc 1
⊢ RelSeries.last p = (RelSeries.snoc Q (RelSeries.last p) ⋯).last

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.KrullDimension.Regular

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
rs : List R
reg : Sequence.IsRegular R rs
⊢ ofList rs = ofList rs • ⊤

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
s : Finset (Submodule R M)
hs : s.inf id = N
hs' : ∀ ⦃J : Submodule R M⦄, J ∈ s → J.IsPrimary
J : Submodule R M
hJ : J ∈ s
⊢ ∀ ⦃y : Submodule R M⦄,
    y ∈ {I ∈ s | (I.colon Set.univ).radical = (J.colon Set.univ).radical} →
      ((id y).colon Set.univ).radical = ((id J).colon Set.univ).radical

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
s : Finset (Submodule R M)
hs : s.inf id = N
hs' : ∀ ⦃J : Submodule R M⦄, J ∈ s → J.IsPrimary
I J I' : Submodule R M
hI' : I' ∈ s
hI : {I ∈ s | (I.colon Set.univ).radical = (I'.colon Set.univ).radical}.inf id = I
J' : Submodule R M
hJ' : J' ∈ s
hJ : {I ∈ s | (I.colon Set.univ).radical = (J'.colon Set.univ).radical}.inf id = J
hIJ :
  ({I ∈ s | (I.colon Set.univ).radical = (I'.colon Set.univ).radical}.inf fun i ↦ (id i).colon Set.univ).radical =
    (J.colon Set.univ).radical
⊢ ∀ ⦃y : Submodule R M⦄,
    y ∈ {I ∈ s | (I.colon Set.univ).radical = (I'.colon Set.univ).radical} →
      ((id y).colon Set.univ).radical = ((id I').colon Set.univ).radical

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
s : Finset (Submodule R M)
hs : s.inf id = N
hs' : ∀ ⦃J : Submodule R M⦄, J ∈ s → J.IsPrimary
I J I' : Submodule R M
hI' : I' ∈ s
hI : {I ∈ s | (I.colon Set.univ).radical = (I'.colon Set.univ).radical}.inf id = I
J' : Submodule R M
hJ' : J' ∈ s
hJ : {I ∈ s | (I.colon Set.univ).radical = (J'.colon Set.univ).radical}.inf id = J
hIJ : (I'.colon Set.univ).radical = (J.colon Set.univ).radical
⊢ ∀ ⦃y : Submodule R M⦄,
    y ∈ {I ∈ s | (I.colon Set.univ).radical = (J'.colon Set.univ).radical} →
      ((id y).colon Set.univ).radical = ((id J').colon Set.univ).radical

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
N : Submodule R M
h : InfIrred N
a : R
b : M
hab : a • b ∈ N
n : ℕ
⊢ 0 ∈ {x | a ^ n • x ∈ N}

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
N : Submodule R M
a : R
b : M
hab : a • b ∈ N
f : ℕ → Submodule R M := fun n ↦ { carrier := {x | a ^ n • x ∈ N}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
hf : Monotone f
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → { toFun := f, monotone' := hf } n = { toFun := f, monotone' := hf } m
h : ∀ ⦃b c : Submodule R M⦄, b ⊓ c = N → b = N ∨ c = N
⊢ N ≤ N + a ^ n • ⊤

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Invariant.Profinite

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
G : Type u
inst✝¹² : Group G
inst✝¹¹ : MulSemiringAction G B
inst✝¹⁰ : SMulCommClass G A B
inst✝⁹ : TopologicalSpace G
inst✝⁸ : CompactSpace G
inst✝⁷ : TotallyDisconnectedSpace G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : TopologicalSpace B
inst✝⁴ : DiscreteTopology B
inst✝³ : ContinuousSMul G B
inst✝² : IsInvariant A B G
P Q : Ideal B
inst✝¹ : P.IsPrime
inst✝ : Q.IsPrime
hPQ : Ideal.under A P = Ideal.under A Q
B' : (G : Type u) → [inst : Monoid G] → [inst_1 : MulSemiringAction G B] → [SMulCommClass G A B] → Subalgebra A B :=
  FixedPoints.subalgebra A B
F : OpenNormalSubgroup G ⥤ Type u :=
  { obj := fun N ↦ { g // Ideal.under (↥(B' ↥↑N.toOpenSubgroup)) Q = g • Ideal.under (↥(B' ↥↑N.toOpenSubgroup)) P },
    map := fun {N N'} f ↦
      ↾fun x ↦ ⟨(QuotientGroup.map (↑N.toOpenSubgroup) N'.toOpenSubgroup.1 (MonoidHom.id G) ⋯) ↑x, ⋯⟩,
    map_id := ⋯, map_comp := ⋯ }
this : ∀ (N : OpenNormalSubgroup G), Nonempty (F.obj N)
s : (j : OpenNormalSubgroup G) → F.obj j
hs : s ∈ F.sections
a : ↑(ProfiniteGrp.of G).toProfinite.toTop :=
  (ProfiniteGrp.Hom.hom (ProfiniteGrp.of G).isoLimittoFiniteQuotientFunctor.inv) ⟨fun N ↦ ↑(s N), ⋯⟩
N : OpenNormalSubgroup G
⊢ ↑((ProfiniteGrp.Hom.hom (𝟙 (ProfiniteGrp.limit (ProfiniteGrp.of G).diagram))) ⟨fun N ↦ ↑(s N), ⋯⟩) N = ↑(s N)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension

Goal state before:
pp: case coe.top
R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
S : Submonoid R
M : ModuleCat R
aux : ∀ (n : ℕ), injectiveDimension M ≤ ↑n → injectiveDimension (M.localizedModule S) ≤ ↑n
⊢ injectiveDimension M ≤ ↑⊤ → injectiveDimension (M.localizedModule S) ≤ ↑⊤

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension

Goal state before:
pp: case coe.top
R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
M : ModuleCat R
aux : ∀ (n : ℕ), injectiveDimension M ≤ ↑n ↔ ⨆ p, injectiveDimension (M.localizedModule p.asIdeal.primeCompl) ≤ ↑n
⊢ injectiveDimension M ≤ ↑⊤ ↔ ⨆ p, injectiveDimension (M.localizedModule p.asIdeal.primeCompl) ≤ ↑⊤

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension

Goal state before:
pp: case coe.top
R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
M : ModuleCat R
aux : ∀ (n : ℕ), injectiveDimension M ≤ ↑n ↔ ⨆ m, injectiveDimension (M.localizedModule m.asIdeal.primeCompl) ≤ ↑n
⊢ injectiveDimension M ≤ ↑⊤ ↔ ⨆ p, injectiveDimension (M.localizedModule p.asIdeal.primeCompl) ≤ ↑⊤

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension

Goal state before:
pp: case coe.top
R : Type u
inst✝¹ : CommRing R
inst✝ : Small.{v, u} R
S : Submonoid R
M : ModuleCat R
aux : ∀ (n : ℕ), projectiveDimension M ≤ ↑n → projectiveDimension (M.localizedModule S) ≤ ↑n
⊢ projectiveDimension M ≤ ↑⊤ → projectiveDimension (M.localizedModule S) ≤ ↑⊤

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension

Goal state before:
pp: case coe.top
R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
M : ModuleCat R
inst✝ : Module.Finite R ↑M
aux : ∀ (n : ℕ), projectiveDimension M ≤ ↑n ↔ ⨆ p, projectiveDimension (M.localizedModule p.asIdeal.primeCompl) ≤ ↑n
⊢ projectiveDimension M ≤ ↑⊤ ↔ ⨆ p, projectiveDimension (M.localizedModule p.asIdeal.primeCompl) ≤ ↑⊤

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.LocalRing.Etale

Goal state before:
pp: case mp.refine_1
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalRing S
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R S
inst✝¹ : FaithfulSMul R S
inst✝ : FormallyUnramified R S
β : S
hβ : Function.Surjective ⇑(aeval ((residue S) β))
s : S
a✝ : s ∈ ⊤
q : R[X]
hp : (aeval ((residue S) β)) (map (residue R) q) = (residue S) s
⊢ (aeval β) q ∈ Subalgebra.toSubmodule R[β]

Tactic:
adjoin_singleton_eq_range_aeval

Goal state after:
case mp.refine_1
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalRing S
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R S
inst✝¹ : FaithfulSMul R S
inst✝ : FormallyUnramified R S
β : S
hβ : Function.Surjective ⇑(aeval ((residue S) β))
s : S
a✝ : s ∈ ⊤
q : R[X]
hp : (aeval ((residue S) β)) (map (residue R) q) = (residue S) s
⊢ (aeval β) q ∈ Subalgebra.toSubmodule (aeval β).range
Module: Mathlib.RingTheory.LocalRing.Etale

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalRing S
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R S
inst✝¹ : FaithfulSMul R S
inst✝ : Etale R S
β : S
hadj : R[β] = ⊤
h : (minpoly R β).Monic
⊢ (residue S) ((aeval β) (minpoly R β)) = 0

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
f : V⸨X⸩
n : ℤ
⊢ ((hasseDeriv R 0) f).coeff n = (LinearMap.id f).coeff n

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.LocalRing.NonLocalRing

Goal state before:
pp: case isTrue
ι : Type u_1
inst✝² : Nontrivial ι
R : ι → Type u_2
inst✝¹ : (i : ι) → Semiring (R i)
inst✝ : ∀ (i : ι), Nontrivial (R i)
i₁ i₂ : ι
hi : i₁ ≠ i₂
ha : ¬IsUnit fun i ↦ if i = i₁ then 0 else 1
hb : ¬IsUnit fun i ↦ if i = i₁ then 1 else 0
x✝ : ι
h✝ : x✝ = i₁
⊢ 0 + 1 = 1

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.LocalRing.NonLocalRing

Goal state before:
pp: case isFalse
ι : Type u_1
inst✝² : Nontrivial ι
R : ι → Type u_2
inst✝¹ : (i : ι) → Semiring (R i)
inst✝ : ∀ (i : ι), Nontrivial (R i)
i₁ i₂ : ι
hi : i₁ ≠ i₂
ha : ¬IsUnit fun i ↦ if i = i₁ then 0 else 1
hb : ¬IsUnit fun i ↦ if i = i₁ then 1 else 0
x✝ : ι
h✝ : ¬x✝ = i₁
⊢ 1 + 0 = 1

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.LocalRing.NonLocalRing

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
inst✝³ : Semiring R₁
inst✝² : Semiring R₂
inst✝¹ : Nontrivial R₁
inst✝ : Nontrivial R₂
ha : ¬IsUnit (1, 0)
hb : ¬IsUnit (0, 1)
⊢ (1, 0) + (0, 1) = 1

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case zero
R : Type u_1
inst✝² : Semiring R
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
n : ℤ
f : V⸨X⸩
⊢ ((⇑(derivative R))^[0] f).coeff n = (Nat.factorial 0 • (hasseDeriv R 0) f).coeff n

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n✝ : ℕ
⊢ (PowerSeries.coeff n✝) (powerSeriesPart 0) = (PowerSeries.coeff n✝) 0

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case mpr
R : Type u_1
inst✝ : Semiring R
⊢ powerSeriesPart 0 = 0

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ (single ↑n) 1 * (single (-↑n)) 1 = 1

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ (single (-↑n)) 1 * (single ↑n) 1 = 1

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case negSucc
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
a✝ : ℕ
⊢ Int.negSucc a✝ ∉ ⇑Nat.castOrderEmbedding '' (HahnSeries.toPowerSeries.symm f).support

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: R : Type u_2
inst✝ : Semiring R
n : ℕ
⊢ (single ↑n) 1 = (single 1) 1 ^ n

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.LocalRing.Pullback

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Semiring T
f : R →+* T
g : S →+* T
s : S
hs : s ∈ ker g
⊢ ⟨(0, s), ⋯⟩ ∈ ker (f.pullbackFst g)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Localization.Rat

Goal state before:
pp: q : ℚ
⊢ ↑q.den ∈ nonZeroDivisors ℤ

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case refine_1.negSucc
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
h : ∀ n < 0, f.coeff n = 0
n : ℕ
⊢ Int.negSucc n ∉ Set.range ⇑{ toFun := ⇑(Nat.castAddMonoidHom ℤ), inj' := ⋯, map_rel_iff' := ⋯ }

Tactic:
simp only [Nat.coe_castAddMonoidHom, RelEmbedding.coe_mk, Function.Embedding.coeFn_mk,
      Set.mem_range, not_exists, reduceCtorEq]

Goal state after:
case refine_1.negSucc
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
h : ∀ n < 0, f.coeff n = 0
n : ℕ
⊢ ∀ (x : ℕ), ¬False