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
x : R⟦Γ⟧
r : R
hr : r * x.leadingCoeff = 1
oinv : Γ
hxo : oinv + x.order = 0
⊢ 0 < (1 - (single oinv) r * x).orderTop

Tactic:
by
  let y := (x - single x.order x.leadingCoeff)
  by_cases hy : y = 0
  · have hrx : (single oinv) r * x = 1 := by
      rw [eq_of_sub_eq_zero hy, single_mul_single, hxo, hr, single_zero_one]
    simp only [hrx, sub_self, orderTop_zero, WithTop.top_pos]
  · have hr' : IsRegular r := IsUnit.isRegular <| .of_mul_eq_one x.leadingCoeff hr
    have hy' : 0 < (single oinv r * y).order := by
      rw [(order_single_mul_of_isRegular hr' hy)]
      refine pos_of_lt_add_right (a := x.order) ?_
      rw [← add_assoc, add_comm x.order, hxo, zero_add]
      exact order_lt_order_of_eq_add_single (sub_add_cancel x _).symm hy
    rw [one_minus_single_neg_mul hr (sub_add_cancel x _).symm _ hxo, orderTop_neg]
    exact zero_lt_orderTop_of_order hy'

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

Goal state before:
pp: case mp
Γ : Type u_1
R : Type u_3
inst✝⁴ : AddCommGroup Γ
inst✝³ : LinearOrder Γ
inst✝² : IsOrderedAddMonoid Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
u i : R⟦Γ⟧
ui : u * i = 1
iu : i * u = 1
⊢ coeff 1 (u.order + i.order) = 1

Tactic:
coeff_one,

Goal state after:
case mp
Γ : Type u_1
R : Type u_3
inst✝⁴ : AddCommGroup Γ
inst✝³ : LinearOrder Γ
inst✝² : IsOrderedAddMonoid Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
u i : R⟦Γ⟧
ui : u * i = 1
iu : i * u = 1
⊢ (if u.order + i.order = 0 then 1 else 0) = 1
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : AddCommGroup Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedAddMonoid Γ
inst✝ : Field R
x : R⟦Γ⟧
x0 : x ≠ 0
⊢ x * x⁻¹ = 1

Tactic:
have h :=
      SummableFamily.one_sub_self_mul_hsum_powers
        (unit_aux x (inv_mul_cancel₀ (leadingCoeff_ne_zero.mpr x0)) _ (neg_add_cancel x.order))

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : AddCommGroup Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedAddMonoid Γ
inst✝ : Field R
x : R⟦Γ⟧
x0 : x ≠ 0
h :
  (1 - (1 - (single (-x.order)) x.leadingCoeff⁻¹ * x)) *
      (SummableFamily.powers (1 - (single (-x.order)) x.leadingCoeff⁻¹ * x)).hsum =
    1
⊢ x * x⁻¹ = 1
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
f : A →ₐc[R] B
hf : Function.Surjective ⇑f
hS : antipode R ∘ₗ f.toLinearMap = f.toLinearMap ∘ₗ antipode R
⊢ HopfAlgebra R B

Tactic:
refine .ofConvInverse (antipode R) (ofConv_injective ?_) (ofConv_injective ?_) <;>
    rw [← LinearMap.cancel_right (show Function.Surjective f.toLinearMap from hf)]

Goal state after:
case refine_1
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
f : A →ₐc[R] B
hf : Function.Surjective ⇑f
hS : antipode R ∘ₗ f.toLinearMap = f.toLinearMap ∘ₗ antipode R
⊢ (toConv (antipode R) * toConv LinearMap.id).ofConv ∘ₗ f.toLinearMap = ofConv 1 ∘ₗ f.toLinearMap

case refine_2
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
f : A →ₐc[R] B
hf : Function.Surjective ⇑f
hS : antipode R ∘ₗ f.toLinearMap = f.toLinearMap ∘ₗ antipode R
⊢ (toConv LinearMap.id * toConv (antipode R)).ofConv ∘ₗ f.toLinearMap = ofConv 1 ∘ₗ f.toLinearMap
Module: Mathlib.Topology.Algebra.ClopenNhdofOne

Goal state before:
pp: case a
G : Type u_1
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : CompactSpace G
inst✝ : TotallyDisconnectedSpace G
H : ClosedSubgroup G
g : G
hg : g ∈ sInf {N | IsOpen ↑N ∧ ↑H ≤ N}
hg_not : g ∉ ↑H
⊢ False

Tactic:
let U : Set G := (g • H)ᶜ

Goal state after:
case a
G : Type u_1
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : CompactSpace G
inst✝ : TotallyDisconnectedSpace G
H : ClosedSubgroup G
g : G
hg : g ∈ sInf {N | IsOpen ↑N ∧ ↑H ≤ N}
hg_not : g ∉ ↑H
U : Set G := (g • ↑H)ᶜ
⊢ False
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I : Ideal R
hI : I ≠ ⊤
⊢ ↑(Cardinal.toENat (Submodule.spanRank I)) ≤ Submodule.spanRank I

Tactic:
exact I.spanRank.ofENat_toENat_le

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
⊢ p ∈ (span ↑hs.toFinset).minimalPrimes

Tactic:
by rwa [hs.coe_toFinset, span, I.span_generators]

Goal state after:
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'
x : R ⧸ I
hx : x ∈ ↑p'
⊢ x ∈ ⇑(Quotient.mk I) '' ↑p

Tactic:
obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x

Goal state after:
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'
x : R
hx : (Quotient.mk I) x ∈ ↑p'
⊢ (Quotient.mk I) x ∈ ⇑(Quotient.mk I) '' ↑p
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
i : ℕ
hi✝ : i < p.length - 1 + 1
hi : i + 1 < q.length + 1
⊢ q.toFun ⟨i + 1, hi⟩ ∈ support R (QuotSMulTop x M)

Tactic:
simpa using!
        ⟨mem_support_mono (by simpa [h0] using! q.monotone (Fin.zero_le _)) p.head.2, q.monotone
          ((Fin.natCast_eq_mk (Nat.lt_of_add_left_lt hi)).trans_le (Nat.le_add_left 1 i)) hxq⟩

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 (algebraMap R S) p ≤ (PrimeSpectrum.comap (Quotient.mk (map (algebraMap R S) p)) (RelSeries.head lq)).asIdeal

Tactic:
PrimeSpectrum.comap_asIdeal,

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))) ⋯
⊢ map (algebraMap R S) p ≤ comap (Quotient.mk (map (algebraMap R S) p)) (RelSeries.head lq).asIdeal
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
MB : ∀ (I : Ideal R), Function.Surjective ⇑(LinearMap.lcomp R M (Submodule.subtype I))
I : Submodule R R
g : ↥(Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I) →ₗ[Rₛ] Mₛ
this : FinitePresentation R ↥I
a : ↥S
g' : R →ₗ[R] M
e :
  ↑a • g =
    (mapExtendScalars S (Submodule.toLocalized' Rₛ S (Algebra.linearMap R Rₛ) I) f Rₛ)
      ((LinearMap.lcomp R M I.subtype) g', a).1
⊢ ∃ a, (LinearMap.lcomp Rₛ Mₛ (Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I).subtype) a = g

Tactic:
refine ⟨IsLocalization.mk' Rₛ 1 a • mapExtendScalars S (Algebra.linearMap _ _) f _ g', ?_⟩

Goal state after:
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
MB : ∀ (I : Ideal R), Function.Surjective ⇑(LinearMap.lcomp R M (Submodule.subtype I))
I : Submodule R R
g : ↥(Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I) →ₗ[Rₛ] Mₛ
this : FinitePresentation R ↥I
a : ↥S
g' : R →ₗ[R] M
e :
  ↑a • g =
    (mapExtendScalars S (Submodule.toLocalized' Rₛ S (Algebra.linearMap R Rₛ) I) f Rₛ)
      ((LinearMap.lcomp R M I.subtype) g', a).1
⊢ (LinearMap.lcomp Rₛ Mₛ (Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I).subtype)
      (IsLocalization.mk' Rₛ 1 a • (mapExtendScalars S (Algebra.linearMap R Rₛ) f Rₛ) g') =
    g
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
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
H : ∀ (I : Ideal R) (x : I.IsMaximal), Injective (Localization.AtPrime I) (LocalizedModule I.primeCompl M)
I : Ideal R
x✝¹ : FinitePresentation R ↥I := finitePresentation_of_finite R ↥I
m : Ideal R
x✝ : m.IsMaximal
Rₘ : Type u := Localization.AtPrime m
Mₘ : Type (max u v) := LocalizedModule m.primeCompl M
f : M →ₗ[R] LocalizedModule m.primeCompl M := LocalizedModule.mkLinearMap m.primeCompl M
h : R →ₗ[R] Rₘ := Algebra.linearMap R Rₘ
Iₘ : Ideal Rₘ := Submodule.localized' Rₘ m.primeCompl h I
g : ↥I →ₗ[R] ↥Iₘ := Submodule.toLocalized' Rₘ m.primeCompl h I
gM : (↥I →ₗ[R] M) →ₗ[R] ↥Iₘ →ₗ[Rₘ] LocalizedModule m.primeCompl M :=
  IsLocalizedModule.mapExtendScalars m.primeCompl g f Rₘ
hM : (R →ₗ[R] M) →ₗ[R] Rₘ →ₗ[Rₘ] LocalizedModule m.primeCompl M :=
  IsLocalizedModule.mapExtendScalars m.primeCompl h f Rₘ
eq'' : ↑R (Submodule.subtype Iₘ) = (IsLocalizedModule.map m.primeCompl g h) (Submodule.subtype I)
eq' :
  ↑R (LinearMap.lcomp Rₘ Mₘ (Submodule.subtype Iₘ)) =
    (IsLocalizedModule.map m.primeCompl hM gM) (LinearMap.lcomp R M (Submodule.subtype I))
⊢ LinearMap.lcomp Rₘ Mₘ (Submodule.subtype Iₘ) =
    (IsLocalizedModule.mapExtendScalars m.primeCompl hM gM Rₘ) (LinearMap.lcomp R M (Submodule.subtype I))

Tactic:
simp [IsLocalizedModule.mapExtendScalars, ← eq']

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : Small.{v, u} R
S : Submonoid R
M : ModuleCat R
⊢ projectiveDimension (M.localizedModule S) ≤ projectiveDimension M

Tactic:
have aux (n : ℕ) : projectiveDimension M ≤ n → projectiveDimension (M.localizedModule S) ≤ n := by
    simp only [projectiveDimension_le_iff]
    intro h
    exact ModuleCat.localizedModule_hasProjectiveDimensionLE n S M
  refine le_of_forall_ge (fun N ↦ ?_)
  induction N with
  | bot =>
    simp only [le_bot_iff, projectiveDimension_eq_bot_iff, ModuleCat.isZero_iff_subsingleton,
      ModuleCat.localizedModule, ← Equiv.subsingleton_congr (equivShrink _)]
    intro _
    apply LocalizedModule.instSubsingleton _
  | coe N =>
    induction N with
    | top => simp
    | coe n => simpa using aux n

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
x : S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R)
r : R
⊢ (Ideal.quotEquivOfEq ⋯).toAddEquiv ((Ideal.Quotient.mk (maximalIdeal R)) r • x) =
    (Ideal.Quotient.mk (maximalIdeal R)) r • (Ideal.quotEquivOfEq ⋯).toAddEquiv x

Tactic:
obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x

Goal state after:
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 ⋯).toAddEquiv
      ((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 ⋯).toAddEquiv ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) (maximalIdeal R))) x)
Module: Mathlib.RingTheory.Invariant.Profinite

Goal state before:
pp: case refine_2
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)
x : B ⧸ Q
⊢ ((stabilizerHom Q P G) ⟨a, ⋯⟩) x = σ x

Tactic:
obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x

Goal state after:
case refine_2
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)
x : B
⊢ ((stabilizerHom Q P G) ⟨a, ⋯⟩) ((mk Q) x) = σ ((mk Q) x)
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x : R⟦X⟧
⊢ ∃ c, ↑c * x = ↑c * x

Tactic:
exact ⟨1, rfl⟩

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

Goal state before:
pp: case refine_1
R : Type u_1
σ : Type u_2
M : Type u_3
inst✝¹ : CommSemiring R
φ : MvPolynomial σ R
inst✝ : AddCancelCommMonoid M
w : σ → M
n n' : M
i : σ
h : φ ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = n})
h' : n' + w i = n
m : σ →₀ ℕ
hm : m ∈ {d | (weight w) d = n}
⊢ IsWeightedHomogeneous w ((pderiv i) ((fun m ↦ AddMonoidAlgebra.single m 1) m)) n'

Tactic:
simp_rw [single_eq_monomial, pderiv_monomial, one_mul]

Goal state after:
case refine_1
R : Type u_1
σ : Type u_2
M : Type u_3
inst✝¹ : CommSemiring R
φ : MvPolynomial σ R
inst✝ : AddCancelCommMonoid M
w : σ → M
n n' : M
i : σ
h : φ ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = n})
h' : n' + w i = n
m : σ →₀ ℕ
hm : m ∈ {d | (weight w) d = n}
⊢ IsWeightedHomogeneous w ((monomial (m - single i 1)) ↑(m i)) n'
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:
obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x

Goal state after:
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ₚ
⊢ ∃ a, (algebraMap S (Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)) a = (Ideal.Quotient.mk (Ideal.map (algebraMap S Sₚ) P)) 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
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
s : ↥(algebraMapSubmonoid S p.primeCompl)
this : (Ideal.map (algebraMap S Sₚ) P).IsPrime
h₁ : (Ideal.Quotient.mk P) ↑s ≠ 0
⊢ (equivQuotientMapOfIsMaximal p Sₚ P) ((Ideal.Quotient.mk P) ↑s) ≠ 0

Tactic:
RingEquiv.map_ne_zero_iff

Goal state after:
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
s : ↥(algebraMapSubmonoid S p.primeCompl)
this : (Ideal.map (algebraMap S Sₚ) P).IsPrime
h₁ : (Ideal.Quotient.mk P) ↑s ≠ 0
⊢ (Ideal.Quotient.mk P) ↑s ≠ 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
s : ↥(algebraMapSubmonoid S p.primeCompl)
this : (Ideal.map (algebraMap S Sₚ) P).IsPrime
h₁ : (Ideal.Quotient.mk P) ↑s ≠ 0
h₂ : (equivQuotientMapOfIsMaximal p Sₚ P) ((Ideal.Quotient.mk P) ↑s) ≠ 0
⊢ (Ideal.Quotient.mk (Ideal.map (algebraMap S Sₚ) P)) (mk' Sₚ x s * (algebraMap S Sₚ) ↑s) =
    (equivQuotientMapOfIsMaximal p Sₚ P) ((Ideal.Quotient.mk P) x)

Tactic:
mk'_spec,

Goal state after:
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
s : ↥(algebraMapSubmonoid S p.primeCompl)
this : (Ideal.map (algebraMap S Sₚ) P).IsPrime
h₁ : (Ideal.Quotient.mk P) ↑s ≠ 0
h₂ : (equivQuotientMapOfIsMaximal p Sₚ P) ((Ideal.Quotient.mk P) ↑s) ≠ 0
⊢ (Ideal.Quotient.mk (Ideal.map (algebraMap S Sₚ) P)) ((algebraMap S Sₚ) x) =
    (equivQuotientMapOfIsMaximal p Sₚ P) ((Ideal.Quotient.mk P) 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✝⁵ : Algebra R Sₚ
inst✝⁴ : IsScalarTower R S Sₚ
inst✝³ : IsScalarTower R Rₚ Sₚ
inst✝² : p.IsMaximal
inst✝¹ : P.IsMaximal
inst✝ : (Ideal.map (algebraMap S Sₚ) P).LiesOver (maximalIdeal Rₚ)
x : Rₚ ⧸ maximalIdeal Rₚ
⊢ (algebraMap (R ⧸ p) (S ⧸ P)) ((equivQuotMaximalIdeal p Rₚ).symm x) =
    (equivQuotientMapOfIsMaximal p Sₚ P).symm
      ((algebraMap (Rₚ ⧸ maximalIdeal Rₚ) (Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)) x)

Tactic:
obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x

Goal state after:
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✝⁵ : Algebra R Sₚ
inst✝⁴ : IsScalarTower R S Sₚ
inst✝³ : IsScalarTower R Rₚ Sₚ
inst✝² : p.IsMaximal
inst✝¹ : P.IsMaximal
inst✝ : (Ideal.map (algebraMap S Sₚ) P).LiesOver (maximalIdeal Rₚ)
x : Rₚ
⊢ (algebraMap (R ⧸ p) (S ⧸ P)) ((equivQuotMaximalIdeal p Rₚ).symm ((Ideal.Quotient.mk (maximalIdeal Rₚ)) x)) =
    (equivQuotientMapOfIsMaximal p Sₚ P).symm
      ((algebraMap (Rₚ ⧸ maximalIdeal Rₚ) (Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P))
        ((Ideal.Quotient.mk (maximalIdeal Rₚ)) x))
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
f : K⸨X⸩
⊢ Valued.v f ≤ 1 ↔ ∃ F, (ofPowerSeries ℤ K) F = f

Tactic:
by
  rw [valuation_le_iff_coeff_lt_log_eq_zero _ one_ne_zero, log_one, neg_zero]
  refine ⟨fun h => ⟨PowerSeries.mk fun n => f.coeff n, ?_⟩, ?_⟩
  on_goal 1 => ext (_ | n)
  · simp only [Int.ofNat_eq_natCast, coeff_coe_powerSeries, coeff_mk]
  on_goal 1 => simp only [h (Int.negSucc n) (Int.negSucc_lt_zero n)]
  on_goal 2 => rintro ⟨F, rfl⟩ _ _
  all_goals
    apply HahnSeries.embDomain_of_notMem_range
    simp only [Nat.coe_castAddMonoidHom, RelEmbedding.coe_mk, Function.Embedding.coeFn_mk,
      Set.mem_range, not_exists, reduceCtorEq]
    intro
  · simp only [not_false_eq_true]
  · lia

Goal state after: