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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
f : R[X]
a b : R
ha : Polynomial.eval a f = 0
hb : Polynomial.eval b f = 0
h : ¬IsUnit (a - b)
h' : IsUnit (Polynomial.eval a (derivative f))
c : R
h✝ :
  c * (b - a) ^ 2 + Polynomial.eval a (derivative f) * (b - a) + Polynomial.eval a f = Polynomial.eval (a + (b - a)) f
⊢ (c * (b - a) + Polynomial.eval a (derivative f)) * (b - a) = 0

Tactic:
grind

Goal state after:
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
f : R[X]
a b : R
ha : Polynomial.eval a f = 0
hb : Polynomial.eval b f = 0
h : ¬IsUnit (a - b)
h' : IsUnit (Polynomial.eval a (derivative f))
c : R
h✝ :
  c * (b - a) ^ 2 + Polynomial.eval a (derivative f) * (b - a) + Polynomial.eval a f = Polynomial.eval (a + (b - a)) f
hc : (c * (b - a) + Polynomial.eval a (derivative f)) * (b - a) = 0
this :
  ∃ b_1,
    (c * (b - a) + Polynomial.eval a (derivative f)) * b_1 = 1 ∧
      b_1 * (c * (b - a) + Polynomial.eval a (derivative f)) = 1
⊢ a = b

Tactic:
grind

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

Goal state before:
pp: case hIN.refine_1
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
I : Ideal R
inst✝ : Submodule.IsPrincipal I
hp : IsLocalRing.maximalIdeal R ∈ I.minimalPrimes
q : Ideal R
h₁ : q.IsPrime
h₂ : q < IsLocalRing.maximalIdeal R
this : IsArtinianRing (R ⧸ I)
f : R →+* Localization.AtPrime q := algebraMap R (Localization.AtPrime q)
qs : ℕ →o (Ideal (R ⧸ I))ᵒᵈ := { toFun := fun n ↦ map (Quotient.mk I) (comap f (map f q ^ n)), monotone' := ⋯ }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → qs n = qs m
⊢ I ≤ ⊥.jacobson

Tactic:
rw [IsLocalRing.jacobson_eq_maximalIdeal]

Goal state after:
case hIN.refine_1
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
I : Ideal R
inst✝ : Submodule.IsPrincipal I
hp : IsLocalRing.maximalIdeal R ∈ I.minimalPrimes
q : Ideal R
h₁ : q.IsPrime
h₂ : q < IsLocalRing.maximalIdeal R
this : IsArtinianRing (R ⧸ I)
f : R →+* Localization.AtPrime q := algebraMap R (Localization.AtPrime q)
qs : ℕ →o (Ideal (R ⧸ I))ᵒᵈ := { toFun := fun n ↦ map (Quotient.mk I) (comap f (map f q ^ n)), monotone' := ⋯ }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → qs n = qs m
⊢ I ≤ IsLocalRing.maximalIdeal R

case hIN.refine_1.h
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
I : Ideal R
inst✝ : Submodule.IsPrincipal I
hp : IsLocalRing.maximalIdeal R ∈ I.minimalPrimes
q : Ideal R
h₁ : q.IsPrime
h₂ : q < IsLocalRing.maximalIdeal R
this : IsArtinianRing (R ⧸ I)
f : R →+* Localization.AtPrime q := algebraMap R (Localization.AtPrime q)
qs : ℕ →o (Ideal (R ⧸ I))ᵒᵈ := { toFun := fun n ↦ map (Quotient.mk I) (comap f (map f q ^ n)), monotone' := ⋯ }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → qs n = qs m
⊢ ⊥ ≠ ⊤
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:
by
  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.Ideal.Pure

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.Pure
x : R
hx : x ∈ I
h : ∃ z ∈ I, z * x = x
⊢ ∃ y ∈ I, x = x * y

Tactic:
grind

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.Pure
⊢ RingHom.ker (RingHom.pi fun p ↦ algebraMap R (Localization.AtPrime (↑p).asIdeal)) = I

Tactic:
refine le_antisymm ?_ fun x hx ↦ ?_
  · rw [Pi.ker_ringHom]
    refine le_trans ?_ I.iInf_ker_le
    simp only [le_iInf_iff]
    exact fun i hi hle ↦ iInf_le_of_le ⟨⟨i, hi⟩, hle⟩ le_rfl
  · rw [RingHom.mem_ker]
    ext p
    rw [RingHom.pi_apply, Pi.zero_apply]
    exact Ideal.le_ker_atPrime_of_forall_exists_eq_mul
      (fun x hx ↦ Ideal.exists_eq_mul_of_pure hx) p.2 hx

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I J : Ideal R
inst✝¹ : I.Pure
inst✝ : J.Pure
h : zeroLocus ↑I = zeroLocus ↑J
s : Set (PrimeSpectrum R)
hs : zeroLocus ↑I = s
ht : zeroLocus ↑J = s
⊢ RingHom.ker (RingHom.pi fun p ↦ algebraMap R (Localization.AtPrime (↑p).asIdeal)) =
    RingHom.ker (RingHom.pi fun p ↦ algebraMap R (Localization.AtPrime (↑p).asIdeal))

Tactic:
rfl

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
p : Ideal R
inst✝ : p.IsPrime
I : Ideal R
hI : p ∈ I.minimalPrimes
hr : Submodule.spanRank I ≤ ↑p.height
hs : (Submodule.generators I).Finite
⊢ ↑hs.toFinset.card = p.height

Tactic:
rw [← Set.ncard_eq_toFinset_card (hs := hs), (IsNoetherian.noetherian I).generators_ncard]

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
p : Ideal R
inst✝ : p.IsPrime
I : Ideal R
hI : p ∈ I.minimalPrimes
hr : Submodule.spanRank I ≤ ↑p.height
hs : (Submodule.generators I).Finite
⊢ ↑(Submodule.spanFinrank I) = p.height
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
I p : Ideal R
inst✝ : p.IsPrime
hrp : I ≤ p
p' : Ideal (R ⧸ I) := map (algebraMap R (R ⧸ I)) p
this✝¹ : p'.IsPrime
s : Finset (R ⧸ I)
hps : p' ∈ (span ↑s).minimalPrimes
hs : ↑s.card = p'.height
hsp' : ↑s ⊆ ↑p'
this✝ : Set.SurjOn ⇑(Quotient.mk I) ↑p ↑s
o : Finset R
hsubset : ↑o ⊆ ↑p
ho : Set.InjOn ⇑(Quotient.mk I) ↑o
himgo : Finset.image (⇑(Quotient.mk I)) o = s
hI : I.FG
t : Finset R := o ∪ ⋯.toFinset
h : p.height ≤ ↑t.card
this : ⋯.toFinset.card = Submodule.spanFinrank I
⊢ t.card ≤ s.card + Submodule.spanFinrank I

Tactic:
grind

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
p : LTSeries (PrimeSpectrum R)
x : R
hx : x ∈ (RelSeries.last p).asIdeal
⊢ ∃ q,
    x ∈ (q.toFun 1).asIdeal ∧
      p.length = q.length ∧ RelSeries.head p = RelSeries.head q ∧ RelSeries.last p = RelSeries.last q

Tactic:
by
  generalize hp : p.length = n
  induction n generalizing p with
  | zero =>
    use RelSeries.singleton _ p.last
    simp only [RelSeries.singleton_toFun, hx, RelSeries.singleton_length, RelSeries.head,
      RelSeries.last_singleton, and_true, true_and]
    rw [show 0 = Fin.last p.length from Fin.zero_eq_mk.mpr hp, RelSeries.last]
  | succ n hn => ?_
  by_cases h0 : n = 0
  · use p
    have h1 : 1 = Fin.last p.length := by
      rw [Fin.last, hp, h0, zero_add]
      exact Fin.natCast_eq_mk (Nat.one_lt_succ_succ 0)
    simpa [h1, hp] using! hx
  obtain ⟨q, hxq, h2, hq⟩ : ∃ q : PrimeSpectrum R, x ∈ q.1 ∧ p ⟨p.length - 2, _⟩ < q ∧ q < p.last :=
    (p ⟨p.length - 1, p.length.sub_lt_succ 1⟩).exist_mem_one_of_mem_two
      (p.strictMono (Nat.pred_lt (by simpa [hp]))) (p.strictMono (Nat.pred_lt (by simp [hp]))) hx
  obtain ⟨Q, hx, hQ, hh, hl⟩ := hn (p.eraseLast.eraseLast.snoc q h2) (by simpa using! hxq) <| by
    simpa [hp] using! Nat.succ_pred_eq_of_ne_zero h0
  have h1 : 1 < Q.length + 1 := Nat.lt_of_sub_ne_zero (hQ.symm.trans_ne h0)
  have h : 1 = (1 : Fin (Q.length + 1)).castSucc := by simp [Fin.one_eq_mk_of_lt h1]
  exact ⟨Q.snoc p.last (by simpa [← hl] using! hq), by simpa [h], by simpa, by simp [← hh], by simp⟩

Goal state after:
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: case h
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
t : Finset (Submodule R M)
ht : N.IsMinimalPrimaryDecomposition t
h : ∀ (x : M), (N.colon {x}).radical = {x_1 ∈ t | x ∉ x_1}.inf fun q ↦ (q.colon Set.univ).radical
q : Submodule R M
hqt : q ∈ ↑t
x : M
hxq : x ∉ q
hxt : ∀ (i : Submodule R M), i ≠ q ∧ i ∈ t → x ∈ id i
⊢ ∀ b ∈ {x_1 ∈ t | x ∉ x_1}.erase q, (q.colon Set.univ).radical ≤ (b.colon Set.univ).radical

Tactic:
grind

Goal state after:
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
t : Finset (Ideal R)
ht : Submodule.IsMinimalPrimaryDecomposition I t
p : Ideal R
hp : p ∈ I.minimalPrimes
⊢ t.inf radical ≤ t.inf (⇑radicalInfTopHom ∘ id)

Tactic:
rfl

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

Goal state before:
pp: case mk
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 := ⋯
N : OpenNormalSubgroup G
val✝ : G ⧸ ↑N.toOpenSubgroup
x : G
hx :
  Ideal.under (↥(B' ↥↑N.toOpenSubgroup)) Q =
    Quot.mk (⇑(QuotientGroup.leftRel ↑N.toOpenSubgroup)) x • Ideal.under (↥(B' ↥↑N.toOpenSubgroup)) P
⊢ ↑((ConcreteCategory.hom
            (↾fun x ↦ ⟨(QuotientGroup.map (↑N.toOpenSubgroup) N.toOpenSubgroup.1 (MonoidHom.id G) ⋯) ↑x, ⋯⟩)).toFun
        ⟨Quot.mk (⇑(QuotientGroup.leftRel ↑N.toOpenSubgroup)) x, hx⟩) =
    ↑((ConcreteCategory.hom
            (𝟙 { g // Ideal.under (↥(B' ↥↑N.toOpenSubgroup)) Q = g • Ideal.under (↥(B' ↥↑N.toOpenSubgroup)) P })).toFun
        ⟨Quot.mk (⇑(QuotientGroup.leftRel ↑N.toOpenSubgroup)) x, hx⟩)

Tactic:
rfl

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

Goal state before:
pp: case mk
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 := ⋯
X✝ Y✝ Z✝ : OpenNormalSubgroup G
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
val✝ : G ⧸ ↑X✝.toOpenSubgroup
x : G
hx :
  Ideal.under (↥(B' ↥↑X✝.toOpenSubgroup)) Q =
    Quot.mk (⇑(QuotientGroup.leftRel ↑X✝.toOpenSubgroup)) x • Ideal.under (↥(B' ↥↑X✝.toOpenSubgroup)) P
⊢ ↑((ConcreteCategory.hom
            (↾fun x ↦ ⟨(QuotientGroup.map (↑X✝.toOpenSubgroup) Z✝.toOpenSubgroup.1 (MonoidHom.id G) ⋯) ↑x, ⋯⟩)).toFun
        ⟨Quot.mk (⇑(QuotientGroup.leftRel ↑X✝.toOpenSubgroup)) x, hx⟩) =
    ↑((ConcreteCategory.hom
            ((↾fun x ↦ ⟨(QuotientGroup.map (↑X✝.toOpenSubgroup) Y✝.toOpenSubgroup.1 (MonoidHom.id G) ⋯) ↑x, ⋯⟩) ≫
              ↾fun x ↦ ⟨(QuotientGroup.map (↑Y✝.toOpenSubgroup) Z✝.toOpenSubgroup.1 (MonoidHom.id G) ⋯) ↑x, ⋯⟩)).toFun
        ⟨Quot.mk (⇑(QuotientGroup.leftRel ↑X✝.toOpenSubgroup)) x, hx⟩)

Tactic:
rfl

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

Goal state before:
pp: case succ
R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
n : ℕ
ih :
  ∀ (M : ModuleCat R),
    HasInjectiveDimensionLE M n ↔
      ∀ (m : MaximalSpectrum R), HasInjectiveDimensionLE (M.localizedModule m.asIdeal.primeCompl) n
M : ModuleCat R
⊢ HasInjectiveDimensionLE M (n + 1) ↔
    ∀ (m : MaximalSpectrum R), HasInjectiveDimensionLE (M.localizedModule m.asIdeal.primeCompl) (n + 1)

Tactic:
have ei : EnoughInjectives (ModuleCat.{v} R) := inferInstance
    rcases ei.1 M with ⟨I, inj, f, monof⟩
    let S := ShortComplex.mk f (cokernel.π f) (cokernel.condition f)
    have S_exact : S.ShortExact := { exact := ShortComplex.exact_cokernel f }
    let Sp (m : MaximalSpectrum R) := S.map (ModuleCat.localizedModuleFunctor m.1.primeCompl)
    have Sp_exact (m : MaximalSpectrum R) : (Sp m).ShortExact :=
      S_exact.map_of_exact (ModuleCat.localizedModuleFunctor m.1.primeCompl)
    have ih' := ih S.X₃
    simp only [HasInjectiveDimensionLE] at ih' ⊢
    rw [← S_exact.hasInjectiveDimensionLT_X₃_iff n inj, ih']
    have injp (m : MaximalSpectrum R) : Injective (Sp m).X₂ :=
      (ModuleCat.localizedModuleFunctor.{v} m.1.primeCompl).injective_obj _
    exact (forall_congr' (fun p ↦ (Sp_exact p).hasInjectiveDimensionLT_X₃_iff n (injp p)))

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), ⋯⟩
this : ∀ (N : OpenNormalSubgroup G), ↑a = ↑(s N)
N : OpenNormalSubgroup G
x : ↥(B' ↥↑N.toOpenSubgroup)
hN : ↑N ⊆ ↑(MulAction.stabilizer G ↑x)
y : ↥(B' ↥↑N.toOpenSubgroup)
⊢ ↑((↑a)⁻¹ • y) = a⁻¹ • ↑y

Tactic:
rfl

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

Goal state before:
pp: case mk
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
P✝ : Ideal A
inst✝⁷ : TopologicalSpace G
inst✝⁶ : CompactSpace G
inst✝⁵ : TotallyDisconnectedSpace G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : TopologicalSpace B
inst✝² : DiscreteTopology B
inst✝¹ : ContinuousSMul G B
P : Ideal A
Q : Ideal B
inst✝ : Q.LiesOver P
σ : (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q
N : OpenNormalSubgroup G
val✝ : G ⧸ ↑N.toOpenSubgroup
x : G
hx :
  Quot.mk (⇑(QuotientGroup.leftRel ↑N.toOpenSubgroup)) x ∈
    MulAction.stabilizer (G ⧸ ↑N.toOpenSubgroup) (under (↥(FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup)) Q)
hx' :
  (let __RingHom := quotientMap Q (FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup).subtype ⋯;
        { toRingHom := __RingHom, commutes' := ⋯ }).comp
      ↑((stabilizerHom (under (↥(FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup)) Q) P (G ⧸ ↑N.toOpenSubgroup))
          ⟨Quot.mk (⇑(QuotientGroup.leftRel ↑N.toOpenSubgroup)) x, hx⟩) =
    (↑σ).comp
      (let __RingHom := quotientMap Q (FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup).subtype ⋯;
      { toRingHom := __RingHom, commutes' := ⋯ })
⊢ ↑↑((ConcreteCategory.hom
              (↾fun x ↦
                ⟨⟨(QuotientGroup.map (↑N.toOpenSubgroup) N.toOpenSubgroup.1 (MonoidHom.id G) ⋯) ↑↑x, ⋯⟩, ⋯⟩)).toFun
          ⟨⟨Quot.mk (⇑(QuotientGroup.leftRel ↑N.toOpenSubgroup)) x, hx⟩, hx'⟩) =
    ↑↑((ConcreteCategory.hom
              (𝟙
                { σ' //
                  (let __RingHom := quotientMap Q (FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup).subtype ⋯;
                        { toRingHom := __RingHom, commutes' := ⋯ }).comp
                      ↑((stabilizerHom (under (↥(FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup)) Q) P
                            (G ⧸ ↑N.toOpenSubgroup))
                          σ') =
                    (↑σ).comp
                      (let __RingHom := quotientMap Q (FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup).subtype ⋯;
                      { toRingHom := __RingHom, commutes' := ⋯ }) })).toFun
          ⟨⟨Quot.mk (⇑(QuotientGroup.leftRel ↑N.toOpenSubgroup)) x, hx⟩, hx'⟩)

Tactic:
rfl

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

Goal state before:
pp: case mk
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
P✝ : Ideal A
inst✝⁷ : TopologicalSpace G
inst✝⁶ : CompactSpace G
inst✝⁵ : TotallyDisconnectedSpace G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : TopologicalSpace B
inst✝² : DiscreteTopology B
inst✝¹ : ContinuousSMul G B
P : Ideal A
Q : Ideal B
inst✝ : Q.LiesOver P
σ : (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q
X✝ Y✝ Z✝ : OpenNormalSubgroup G
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
val✝ : G ⧸ ↑X✝.toOpenSubgroup
x : G
hx :
  Quot.mk (⇑(QuotientGroup.leftRel ↑X✝.toOpenSubgroup)) x ∈
    MulAction.stabilizer (G ⧸ ↑X✝.toOpenSubgroup) (under (↥(FixedPoints.subalgebra A B ↥↑X✝.toOpenSubgroup)) Q)
hx' :
  (let __RingHom := quotientMap Q (FixedPoints.subalgebra A B ↥↑X✝.toOpenSubgroup).subtype ⋯;
        { toRingHom := __RingHom, commutes' := ⋯ }).comp
      ↑((stabilizerHom (under (↥(FixedPoints.subalgebra A B ↥↑X✝.toOpenSubgroup)) Q) P (G ⧸ ↑X✝.toOpenSubgroup))
          ⟨Quot.mk (⇑(QuotientGroup.leftRel ↑X✝.toOpenSubgroup)) x, hx⟩) =
    (↑σ).comp
      (let __RingHom := quotientMap Q (FixedPoints.subalgebra A B ↥↑X✝.toOpenSubgroup).subtype ⋯;
      { toRingHom := __RingHom, commutes' := ⋯ })
⊢ ↑↑((ConcreteCategory.hom
              (↾fun x ↦
                ⟨⟨(QuotientGroup.map (↑X✝.toOpenSubgroup) Z✝.toOpenSubgroup.1 (MonoidHom.id G) ⋯) ↑↑x, ⋯⟩, ⋯⟩)).toFun
          ⟨⟨Quot.mk (⇑(QuotientGroup.leftRel ↑X✝.toOpenSubgroup)) x, hx⟩, hx'⟩) =
    ↑↑((ConcreteCategory.hom
              ((↾fun x ↦
                  ⟨⟨(QuotientGroup.map (↑X✝.toOpenSubgroup) Y✝.toOpenSubgroup.1 (MonoidHom.id G) ⋯) ↑↑x, ⋯⟩, ⋯⟩) ≫
                ↾fun x ↦
                  ⟨⟨(QuotientGroup.map (↑Y✝.toOpenSubgroup) Z✝.toOpenSubgroup.1 (MonoidHom.id G) ⋯) ↑↑x, ⋯⟩, ⋯⟩)).toFun
          ⟨⟨Quot.mk (⇑(QuotientGroup.leftRel ↑X✝.toOpenSubgroup)) x, hx⟩, hx'⟩)

Tactic:
rfl

Goal state after:
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
this : Module.Free R S
r : R
x : S
⊢ ↑(Ideal.quotEquivOfEq ⋯)
      ((Ideal.Quotient.mk (maximalIdeal R)) r • (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (maximalIdeal R))) x) =
    (Ideal.Quotient.mk (maximalIdeal R)) r •
      ↑(Ideal.quotEquivOfEq ⋯) ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) (maximalIdeal R))) x)

Tactic:
rfl

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

Goal state before:
pp: case refine_1
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
P : Ideal A
Q : Ideal B
inst✝² : Q.IsPrime
inst✝¹ : Q.LiesOver P
inst✝ : Algebra.IsInvariant A B G
σ : (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q
B' : (G : Type u) → [inst : Monoid G] → [inst_1 : MulSemiringAction G B] → [SMulCommClass G A B] → Subalgebra A B :=
  FixedPoints.subalgebra A B
s : (j : OpenNormalSubgroup G) → (stabilizerHomSurjectiveAuxFunctor P Q σ).obj j
hs : s ∈ (stabilizerHomSurjectiveAuxFunctor P Q σ).sections
a : ↑(ProfiniteGrp.of G).toProfinite.toTop :=
  (ProfiniteGrp.Hom.hom (ProfiniteGrp.of G).isoLimittoFiniteQuotientFunctor.inv) ⟨fun N ↦ ↑↑(s N), ⋯⟩
this : ∀ (N : OpenNormalSubgroup G), ↑a = ↑↑(s N)
N : OpenNormalSubgroup G
x : ↥(B' ↥↑N.toOpenSubgroup)
hN : ↑N ⊆ ↑(MulAction.stabilizer G ↑x)
y : ↥(B' ↥↑N.toOpenSubgroup)
⊢ ((↑(RingEquiv.symm ((MulSemiringAction.toRingAut G B) a))).comp (algebraMap (↥(B' ↥↑N.toOpenSubgroup)) B)) y =
    ((algebraMap (↥(FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup)) B).comp
        ↑(RingEquiv.symm
            ((MulSemiringAction.toRingAut (G ⧸ ↑N.toOpenSubgroup) ↥(FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup))
              ↑a)))
      y

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case negSucc
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
a✝ : ℕ
⊢ 0 = if Int.negSucc a✝ < 0 then 0 else (coeff (Int.negSucc a✝).natAbs) f

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:
if_pos (Int.negSucc_lt_zero _)

Goal state after:
case negSucc
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
a✝ : ℕ
⊢ 0 = 0

case negSucc
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
a✝ : ℕ
⊢ Int.negSucc a✝ ∉ ⇑Nat.castOrderEmbedding '' (HahnSeries.toPowerSeries.symm f).support
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
P : K[X]
⊢ (Polynomial.idealX K).intValuation P = (idealX K).intValuation ↑P

Tactic:
by
  by_cases hP : P = 0
  · rw [hP, Valuation.map_zero, Polynomial.coe_zero, Valuation.map_zero]
  rw [intValuation_if_neg _ hP, intValuation_if_neg _ <| (by simp [hP])]
  simp only [idealX_span, exp_neg, inv_inj, exp_inj, Nat.cast_inj]
  have span_ne_zero :
    (Ideal.span {P} : Ideal K[X]) ≠ 0 ∧ (Ideal.span {Polynomial.X} : Ideal K[X]) ≠ 0 := by
    simp only [Ideal.zero_eq_bot, ne_eq, Ideal.span_singleton_eq_bot, hP, Polynomial.X_ne_zero,
      not_false_iff, and_self_iff]
  have span_ne_zero' :
    (Ideal.span {↑P} : Ideal K⟦X⟧) ≠ 0 ∧ ((idealX K).asIdeal : Ideal K⟦X⟧) ≠ 0 := by
    simp only [Ideal.zero_eq_bot, ne_eq, Ideal.span_singleton_eq_bot, coe_eq_zero_iff, hP,
      not_false_eq_true, true_and, (idealX K).3]
  classical
  rw [Ideal.count_associates_factors_eq span_ne_zero.1
    (Ideal.span_singleton_prime Polynomial.X_ne_zero |>.mpr prime_X) span_ne_zero.2,
    Ideal.count_associates_factors_eq]
  on_goal 1 => convert! (normalized_count_X_eq_of_coe hP).symm
  exacts [Ideal.count_span_normalizedFactors_eq_of_normUnit hP Polynomial.normUnit_X prime_X,
    Ideal.count_span_normalizedFactors_eq_of_normUnit (by simp [hP]) normUnit_X X_prime,
    span_ne_zero'.1, (idealX K).isPrime, span_ne_zero'.2]

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

Goal state before:
pp: case a
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
fst✝ : R
snd✝ : S
h : f fst✝ = g snd✝
⊢ fst✝ = 0 → g snd✝ = 0

Tactic:
grind

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

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
S : ι → Type u_3
inst✝³ : (i : ι) → CommSemiring (R i)
inst✝² : (i : ι) → CommSemiring (S i)
inst✝¹ : (i : ι) → Algebra (R i) (S i)
M : (i : ι) → Submonoid (R i)
inst✝ : ∀ (i : ι), IsLocalization (M i) (S i)
x y : (i : ι) → R i
eq : (algebraMap ((i : ι) → R i) ((i : ι) → S i)) x = (algebraMap ((i : ι) → R i) ((i : ι) → S i)) y
⊢ ∃ c, ↑c * x = ↑c * y

Tactic:
by
    choose c hc using fun i ↦ exists_of_eq (M := M i) (congr_fun eq i)
    exact ⟨⟨_, fun i _ ↦ (c i).2⟩, funext hc⟩

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
n D : ℤ
f : K⸨X⸩
H : Valued.v f ≤ exp (-D)
hnd : n < D
h_n_ord : HahnSeries.order f ≤ n
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : 0 < HahnSeries.order f
s : ℕ
hs : -HahnSeries.order f = -↑s
⊢ 0 ≤ n - ↑s

Tactic:
grind

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
⊢ BddBelow (Function.support (coeff hℱ))

Tactic:
by
  refine ⟨(exists_lb_support hℱ).choose, fun d hd ↦ ?_⟩
  by_contra hNd
  exact hd ((exists_lb_support hℱ).choose_spec d (not_le.mp hNd))

Goal state after: