mathlib-initiative/mathlib-tactics huggingface dataset:
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:
by
    intro f hf a₀ h₁ h₂
    refine HenselianLocalRing.is_henselian f hf a₀ h₁ ?_
    contrapose h₂
    rw [← mem_nonunits_iff, ← IsLocalRing.mem_maximalIdeal, ← Ideal.Quotient.eq_zero_iff_mem] at h₂
    rw [h₂]
    exact not_isUnit_zero

Goal state after:
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: case succ.refine_1
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit ((Ideal.Quotient.mk I) (Polynomial.eval a₀ (derivative f)))
f' : R[X] := derivative f
c : ℕ → R := fun n ↦ Nat.recOn n a₀ fun x b ↦ b - Polynomial.eval b f * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
n : ℕ
ih : Polynomial.eval (c n) f ∈ I ^ (n + 1)
⊢ ((taylor (c n)) f).coeff 0 * (-(Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ)) ^ 0 +
      ((taylor (c n)) f).coeff 1 * (-(Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ)) ^ 1 ∈
    I ^ (n + 1 + 1)

Tactic:
taylor_coeff_zero,

Goal state after:
case succ.refine_1
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit ((Ideal.Quotient.mk I) (Polynomial.eval a₀ (derivative f)))
f' : R[X] := derivative f
c : ℕ → R := fun n ↦ Nat.recOn n a₀ fun x b ↦ b - Polynomial.eval b f * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
n : ℕ
ih : Polynomial.eval (c n) f ∈ I ^ (n + 1)
⊢ Polynomial.eval (c n) f * (-(Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ)) ^ 0 +
      ((taylor (c n)) f).coeff 1 * (-(Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ)) ^ 1 ∈
    I ^ (n + 1 + 1)
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
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)
⊢ IsNilpotent (map (algebraMap R (Localization.AtPrime q)) q)

Tactic:
let qs : ℕ →o (Ideal (R ⧸ I))ᵒᵈ :=
    { toFun n := ((q.map f ^ n).comap f).map (Ideal.Quotient.mk I)
      monotone' i j e := Ideal.map_mono (Ideal.comap_mono (Ideal.pow_le_pow_right e)) }

Goal state after:
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' := ⋯ }
⊢ IsNilpotent (map (algebraMap R (Localization.AtPrime q)) q)
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: case hIjac
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 := ⋯
qs : ℕ →o (Ideal (R ⧸ I))ᵒᵈ := ⋯
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → qs n = qs m
⊢ map f q ≤ ⊥.jacobson

Tactic:
rw [IsLocalRing.jacobson_eq_maximalIdeal, Localization.AtPrime.map_eq_maximalIdeal]
    exact bot_ne_top

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
H : ∀ ⦃J : Ideal R⦄, J.FG → I ⊓ J = I * J
⊢ ∀ ⦃I_1 : Ideal R⦄, I_1.FG → Function.Injective ⇑(LinearMap.lTensor (R ⧸ I) (Submodule.subtype I_1))

Tactic:
intro J hJ

Goal state after:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
H : ∀ ⦃J : Ideal R⦄, J.FG → I ⊓ J = I * J
J : Ideal R
hJ : J.FG
⊢ Function.Injective ⇑(LinearMap.lTensor (R ⧸ I) (Submodule.subtype J))
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
⊢ m.height = 1

Tactic:
refine le_antisymm ?_ ?_

Goal state after:
case refine_1
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
m : Ideal R
inst✝ : m.IsMaximal
h : ¬IsField R
⊢ m.height ≤ 1

case refine_2
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
m : Ideal R
inst✝ : m.IsMaximal
h : ¬IsField R
⊢ 1 ≤ m.height
Module: Mathlib.RingTheory.KrullDimension.Polynomial

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
p : Ideal R
inst✝² : p.IsMaximal
P : Ideal R[X]
inst✝¹ : P.IsMaximal
inst✝ : P.LiesOver p
x✝ : Field (R ⧸ p) := Quotient.field p
h : (Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R R[X]) p)) P).height = 1
⊢ P.height = p.height + 1

Tactic:
height_eq_height_add_of_liesOver_of_hasGoingDown p,

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
p : Ideal R
inst✝² : p.IsMaximal
P : Ideal R[X]
inst✝¹ : P.IsMaximal
inst✝ : P.LiesOver p
x✝ : Field (R ⧸ p) := Quotient.field p
h : (Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R R[X]) p)) P).height = 1
⊢ p.height + (Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R R[X]) p)) P).height = p.height + 1
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
⊢ ↑(Submodule.spanFinrank I) = p.height

Tactic:
refine le_antisymm ?_ ?_

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

case refine_2
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
⊢ p.height ≤ ↑(Submodule.spanFinrank I)
Module: Mathlib.RingTheory.KrullDimension.Polynomial

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
⊢ ringKrullDim R[X] = ringKrullDim R + 1

Tactic:
refine le_antisymm ?_ ?_

Goal state after:
case refine_1
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
⊢ ringKrullDim R[X] ≤ ringKrullDim R + 1

case refine_2
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
⊢ ringKrullDim R + 1 ≤ ringKrullDim R[X]
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: 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))) ⋯
⊢ p = under R (PrimeSpectrum.comap (Quotient.mk (map (algebraMap R S) p)) (RelSeries.head lq)).asIdeal

Tactic:
refine le_antisymm ?_ ?_

Goal state after:
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))) ⋯
⊢ p ≤ under R (PrimeSpectrum.comap (Quotient.mk (map (algebraMap R S) p)) (RelSeries.head lq)).asIdeal

case refine_2
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))) ⋯
⊢ under R (PrimeSpectrum.comap (Quotient.mk (map (algebraMap R S) p)) (RelSeries.head lq)).asIdeal ≤ p
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: case refine_2
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
⊢ ∀ a ∈ s, ({I ∈ s | (I.colon Set.univ).radical = (a.colon Set.univ).radical}.inf id).IsPrimary

Tactic:
intro J hJ

Goal state after:
case refine_2
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
⊢ ({I ∈ s | (I.colon Set.univ).radical = (J.colon Set.univ).radical}.inf id).IsPrimary
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
hxt : x ∈ (t.erase q).inf id
hxq : x ∉ q
⊢ ((q.colon Set.univ).radical ⊓ ({x_1 ∈ t | x ∉ x_1}.erase q).inf fun q ↦ (q.colon Set.univ).radical) =
    (fun J ↦ (J.colon Set.univ).radical) q

Tactic:
inf_eq_left,

Goal state after:
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
hxt : x ∈ (t.erase q).inf id
hxq : x ∉ q
⊢ (q.colon Set.univ).radical ≤ ({x_1 ∈ t | x ∉ x_1}.erase q).inf fun q ↦ (q.colon Set.univ).radical
Module: Mathlib.RingTheory.LocalProperties.Injective

Goal state before:
pp: R : Type u
inst✝¹⁴ : CommRing R
M : Type v
inst✝¹³ : AddCommGroup M
inst✝¹² : Module R M
S : Submonoid R
inst✝¹¹ : Small.{v, u} R
inst✝¹⁰ : IsNoetherianRing R
Rₛ : Type u'
inst✝⁹ : Small.{v', u'} Rₛ
inst✝⁸ : CommRing Rₛ
inst✝⁷ : Algebra R Rₛ
Mₛ : Type v'
inst✝⁶ : AddCommGroup Mₛ
inst✝⁵ : Module R Mₛ
inst✝⁴ : Module Rₛ Mₛ
inst✝³ : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst✝² : IsLocalization S Rₛ
inst✝¹ : IsLocalizedModule S f
inst✝ : Injective R M
⊢ Injective Rₛ Mₛ

Tactic:
have MB : Baer R M := Baer.of_injective ‹_›
  simp only [← Baer.iff_injective, Module.Baer.iff_surjective] at MB ⊢
  intro Iₛ g
  obtain ⟨I, rfl⟩ : ∃ I, .localized' Rₛ S (Algebra.linearMap R Rₛ) I = Iₛ :=
    ⟨Iₛ.comap (algebraMap R Rₛ), by simp [Ideal.localized'_eq_map, IsLocalization.map_under S]⟩
  have : FinitePresentation R I := finitePresentation_of_finite R I
  obtain ⟨⟨g', a⟩, e : a.1 • g = _⟩ := surj S (mapExtendScalars S (I.toLocalized' _ _ _) f Rₛ) g
  obtain ⟨g', rfl⟩ := MB I g'
  refine ⟨IsLocalization.mk' Rₛ 1 a • mapExtendScalars S (Algebra.linearMap _ _) f _ g', ?_⟩
  apply ((Module.End.isUnit_iff _).mp ((IsLocalization.map_units Rₛ a).map
    (algebraMap _ (Module.End Rₛ _)))).1
  simp_rw [algebraMap_end_apply, map_smul, ← mul_smul, algebraMap_smul, IsLocalization.mk'_spec', e]
  apply LinearMap.restrictScalars_injective R
  refine IsLocalizedModule.linearMap_ext S (I.toLocalized' Rₛ S (Algebra.linearMap R Rₛ)) f ?_
  ext
  simp [-Algebra.linearMap_apply]

Goal state after:
Module: Mathlib.RingTheory.LocalIso

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
ι : Type u_3
f : ι → S
h : Ideal.span (Set.range f) = ⊤
T : ι → Type u_4
inst✝⁵ : (i : ι) → CommSemiring (T i)
inst✝⁴ : (i : ι) → Algebra R (T i)
inst✝³ : (i : ι) → Algebra S (T i)
inst✝² : ∀ (i : ι), IsScalarTower R S (T i)
inst✝¹ : ∀ (i : ι), IsLocalization.Away (f i) (T i)
inst✝ : ∀ (i : ι), IsLocalIso R (T i)
⊢ IsLocalIso R S

Tactic:
refine ⟨fun q hq ↦ ?_⟩
  obtain ⟨i, hi⟩ : ∃ i, f i ∉ q := by
    rw [← PrimeSpectrum.iSup_basicOpen_eq_top_iff] at h
    have : ⟨q, hq⟩ ∈ ⨆ i, PrimeSpectrum.basicOpen (f i) := by simp [h]
    simpa using this
  have : ⟨q, hq⟩ ∈ PrimeSpectrum.basicOpen (f i) := hi
  rw [← SetLike.mem_coe, ← PrimeSpectrum.localization_away_comap_range (T i)] at this
  obtain ⟨q', hq'⟩ := this
  obtain ⟨g', hg', h⟩ := exists_notMem_isStandardOpenImmersion (R := R) q'.1
  obtain ⟨n, g, hg⟩ := IsLocalization.Away.surj (f i) g'
  refine ⟨g * (f i), ?_, ?_⟩
  · refine Ideal.IsPrime.mul_notMem hq ?_ hi
    simp only [PrimeSpectrum.ext_iff, PrimeSpectrum.comap_asIdeal] at hq'
    rwa [← hq', Ideal.mem_comap, ← hg, Ideal.mul_unit_mem_iff_mem]
    exact (IsLocalization.Away.algebraMap_isUnit (f i)).pow n
  · have : IsLocalization.Away g' (Localization.Away (algebraMap S (T i) g)) := by
      rw [← hg]
      exact .of_associated
        (associated_mul_unit_right _ _ ((IsLocalization.Away.algebraMap_isUnit (f i)).pow n)).symm
    let e₁ : Localization.Away (algebraMap S (T i) g) ≃ₐ[S] Localization.Away (g * f i) :=
      IsLocalization.algEquiv (.powers (g * f i)) _ _
    let e₂ : Localization.Away g' ≃ₐ[R] Localization.Away (g * f i) :=
      ((IsLocalization.algEquiv (.powers g') _ _).restrictScalars R).trans (e₁.restrictScalars R)
    exact .of_algEquiv e₂

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 := ⋯ }
⊢ ∃ g, Q = g • P

Tactic:
have (N : _) : Nonempty (F.obj N) := by
    obtain ⟨g, hg⟩ := Algebra.IsInvariant.exists_smul_of_under_eq A
      (B' N.1.1) (G ⧸ N.1.1) (P.under _) (Q.under _) hPQ
    exact ⟨g, hg⟩

Goal state after:
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)
⊢ ∃ g, Q = g • P
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case mp
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
h : ¬x = 0
⊢ ¬∀ (n : ℕ), (PowerSeries.coeff n) x.powerSeriesPart = (PowerSeries.coeff n) 0

Tactic:
not_forall

Goal state after:
case mp
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
h : ¬x = 0
⊢ ∃ x_1, ¬(PowerSeries.coeff x_1) x.powerSeriesPart = (PowerSeries.coeff x_1) 0
Module: Mathlib.RingTheory.Localization.AtPrime.Extension

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
p : Ideal R
inst✝⁴ : p.IsPrime
Sₚ : Type u_4
inst✝³ : CommRing Sₚ
inst✝² : Algebra S Sₚ
inst✝¹ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
P : Ideal S
hPp : P.LiesOver p
inst✝ : P.IsMaximal
x : Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P
⊢ ∃ a, (algebraMap S (Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)) a = x

Tactic:
by
  obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
  obtain ⟨x, s, rfl⟩ := IsLocalization.exists_mk'_eq (algebraMapSubmonoid S p.primeCompl) x
  obtain ⟨s', hs⟩ := Ideal.Quotient.mk_surjective (I := P) (Ideal.Quotient.mk P s)⁻¹
  simp only [IsScalarTower.algebraMap_eq S Sₚ (Sₚ ⧸ _), Quotient.algebraMap_eq, RingHom.comp_apply]
  use x * s'
  rw [← sub_eq_zero, ← map_sub, Quotient.eq_zero_iff_mem]
  have h₀ : (P.map (algebraMap S Sₚ)).IsPrime := isPrime_map_of_liesOver S p Sₚ P
  have h₁ : s.1 ∉ P := (Set.disjoint_left.mp <| disjoint_primeCompl_of_liesOver P p) s.prop
  have h₂ : algebraMap S Sₚ s ∉ Ideal.map (algebraMap S Sₚ) P := by
    rwa [← mem_comap, comap_map_eq_self_of_isMaximal _ h₀.ne_top]
  refine (h₀.mem_or_mem ?_).resolve_left h₂
  rw [mul_sub, mul_mk'_eq_mk'_of_mul, mk'_mul_cancel_left, ← map_mul, ← map_sub, ← mem_comap,
    comap_map_eq_self_of_isMaximal _ IsPrime.ne_top', ← Ideal.Quotient.eq, map_mul, map_mul, hs,
    mul_comm, inv_mul_cancel_right₀ (Quotient.eq_zero_iff_mem.not.mpr h₁)]

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.EulerIdentity

Goal state before:
pp: case succ
R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
φ : MvPolynomial σ R
i : σ
n : ℕ
h : φ.IsHomogeneous (n + 1)
⊢ ((pderiv i) φ).IsHomogeneous (n + 1 - 1)

Tactic:
exact IsWeightedHomogeneous.pderiv h rfl

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case pos
K : Type u_2
inst✝ : Field K
n : WithZero (Multiplicative ℤ)
hn0 : n = 0
⊢ ∃ a, Valued.v a = n

pp: case neg
K : Type u_2
inst✝ : Field K
n : WithZero (Multiplicative ℤ)
hn0 : ¬n = 0
⊢ ∃ a, Valued.v a = n

Tactic:
· use 0; simp [hn0]

Goal state after:
case neg
K : Type u_2
inst✝ : Field K
n : WithZero (Multiplicative ℤ)
hn0 : ¬n = 0
⊢ ∃ a, Valued.v a = n
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case h.refine_1
K : Type u_2
inst✝ : Field K
uK : UniformSpace K
d : ℤ
S : Set (K × K)
hS : S ∈ uniformity K
γ : (WithZero (Multiplicative ℤ))ˣ := Units.mk0 (exp (-(d + 1))) ⋯
x : K⸨X⸩
hx : Valued.v x = ↑γ
this : Valued.v.restrict x ≠ 0
⊢ {P | Valued.v (P.2 - P.1) < ↑γ} ∈ uniformity K⸨X⸩

Tactic:
rw [← hx]

Goal state after:
case h.refine_1
K : Type u_2
inst✝ : Field K
uK : UniformSpace K
d : ℤ
S : Set (K × K)
hS : S ∈ uniformity K
γ : (WithZero (Multiplicative ℤ))ˣ := Units.mk0 (exp (-(d + 1))) ⋯
x : K⸨X⸩
hx : Valued.v x = ↑γ
this : Valued.v.restrict x ≠ 0
⊢ {P | Valued.v (P.2 - P.1) < Valued.v x} ∈ uniformity K⸨X⸩
Module: Mathlib.RingTheory.Localization.AtPrime.Extension

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹⁷ : CommRing R
inst✝¹⁶ : CommRing S
inst✝¹⁵ : Algebra R S
p : Ideal R
inst✝¹⁴ : p.IsPrime
Rₚ : Type u_3
inst✝¹³ : CommRing Rₚ
inst✝¹² : Algebra R Rₚ
inst✝¹¹ : IsLocalization.AtPrime Rₚ p
inst✝¹⁰ : IsLocalRing Rₚ
Sₚ : Type u_4
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra S Sₚ
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝⁶ : Algebra Rₚ Sₚ
P : Ideal S
hPp : P.LiesOver p
inst✝⁵ : IsDomain R
inst✝⁴ : IsDedekindDomain S
inst✝³ : IsTorsionFree R S
inst✝² : Algebra R Sₚ
inst✝¹ : IsScalarTower R S Sₚ
inst✝ : IsScalarTower R Rₚ Sₚ
hp : p ≠ ⊥
Q Q' : ↑(p.primesOver S)
⊢ { toFun := fun P ↦ ⟨Ideal.map (algebraMap S Sₚ) ↑P, ⋯⟩, invFun := fun Q ↦ ⟨comap (algebraMap S Sₚ) ↑Q, ⋯⟩,
          left_inv := ⋯, right_inv := ⋯ }
        Q ≤
      { toFun := fun P ↦ ⟨Ideal.map (algebraMap S Sₚ) ↑P, ⋯⟩, invFun := fun Q ↦ ⟨comap (algebraMap S Sₚ) ↑Q, ⋯⟩,
          left_inv := ⋯, right_inv := ⋯ }
        Q' ↔
    Q ≤ Q'

Tactic:
by
    refine ⟨fun h ↦ ?_, fun h ↦ map_mono h⟩
    have : Q'.1.IsMaximal :=
      (primesOver.isPrime p Q').isMaximal (ne_bot_of_mem_primesOver hp Q'.prop)
    simpa [under_map_of_isMaximal S p] using le_comap_of_map_le h

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case right
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
D : ℤ
φ : ℤ → Set K⸨X⸩ := ⋯
intersec₁ : ⋂ n ∈ Set.Iio D, φ n ⊆ {x | ∀ d < D, coeff hℱ d = x.coeff d}
ℓ : ℤ := ⋯
N : ℤ := ⋯
intersec₂ : ⋂ n ∈ Set.Iio D, φ n ⊇ (⋂ n ∈ Set.Iio ℓ, φ n) ∩ ⋂ n ∈ Set.Icc ℓ N, φ n
⊢ ⋂ n ∈ Set.Icc ℓ N, φ n ∈ ℱ

Tactic:
· rw [biInter_mem (Set.finite_Icc ℓ N)]
      intro i _
      apply (coeff_tendsto hℱ _).eventually
      simp

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

Goal state before:
pp: case inr
σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h : #t.1 ≤ k ∧ (#t.1 = k → t.2 ∈ t.1)
h1 : t.2 ∉ t.1
⊢ #(cons t.2 t.1 h1, t.2).1 ≤ k ∧ (#(cons t.2 t.1 h1, t.2).1 = k → (cons t.2 t.1 h1, t.2).2 ∈ (cons t.2 t.1 h1, t.2).1)

Tactic:
simp only [h1] at h

Goal state after:
case inr
σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h1 : t.2 ∉ t.1
h : #t.1 ≤ k ∧ (#t.1 = k → False)
⊢ #(cons t.2 t.1 h1, t.2).1 ≤ k ∧ (#(cons t.2 t.1 h1, t.2).1 = k → (cons t.2 t.1 h1, t.2).2 ∈ (cons t.2 t.1 h1, t.2).1)
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝ : CommRing R
hp : NeZero p
n : ℕ
⊢ (W_ R n).vars ⊆ range (n + 1)

Tactic:
by
  rw [← map_wittPolynomial p (Int.castRingHom R), ← wittPolynomial_vars p ℤ]
  apply vars_map

Goal state after:
Module: Mathlib.RingTheory.Teichmuller

Goal state before:
pp: p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : CharP (R ⧸ I) p
x : Perfection (R ⧸ I) p
m : ℕ
⊢ x.teichmullerAux m ≡ x.teichmullerAux (m + 1) [SMOD I ^ m]

Tactic:
by
  obtain _ | m := m
  · simp
  symm
  rw [teichmullerAux, pow_succ' p, pow_mul]
  exact .pow_pow_add_one (I.natCast_mem_of_charP_quotient p) (m := m) <| by
    simp [SModEq.idealQuotientMk, coeff_pow_p']

Goal state after: