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

Goal state before:
pp: case succ.inr.refine_1
n✝ : ℕ
ih :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Etale R S] [Module.Finite R S],
    Module.rankAtStalk S = ↑n✝ →
      ∃ T x x_1, ∃ (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ : Etale R T), IsFiniteSplit T (T ⊗[R] S)
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Etale R S
inst✝ : Module.Finite R S
hn : Module.rankAtStalk S = ↑(n✝ + 1)
h✝ : Nontrivial R
this✝⁵ : Nontrivial S
U : Type u
w✝⁶ : CommRing U
w✝⁵ : Algebra S U
e✝ : S ⊗[R] S ≃ₐ[S] S × U
algInst✝¹ : Algebra (S × U) U := (RingHom.snd S U).toAlgebra
this✝⁴ : IsScalarTower S (S × U) U
this✝³ : Etale S U
this✝² : Module.Finite S U
this✝¹ : ∀ (p : PrimeSpectrum S), 1 + Module.rankAtStalk U p = n✝ + 1
this✝ : Module.rankAtStalk U = ↑n✝
V : Type u
w✝⁴ : CommRing V
w✝³ : Algebra S V
w✝² : Module.FaithfullyFlat S V
w✝¹ : Module.Finite S V
w✝ : Etale S V
hV : IsFiniteSplit V (V ⊗[S] U)
n : ℕ
f : V ⊗[S] U ≃ₐ[V] Fin n → V
algInst✝ : Algebra R V := ((algebraMap S V).comp (algebraMap R S)).toAlgebra
scalarTowerInst✝ : IsScalarTower R S V := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R V))
e : V ⊗[R] S ≃ₐ[V] Unit ⊕ Fin n → V :=
  (TensorProduct.cancelBaseChange R S V V S).symm.trans
    ((TensorProduct.congr AlgEquiv.refl e✝).trans
      ((TensorProduct.prodRight S V V S U).trans
        (((TensorProduct.rid S V V).prodCongr f).trans
          (((AlgEquiv.funUnique V Unit V).symm.prodCongr AlgEquiv.refl).trans
            (AlgEquiv.sumArrowEquivProdArrow Unit (Fin n) V V).symm))))
this : Module.FaithfullyFlat R S
⊢ Module.FaithfullyFlat R V

Tactic:
exact Module.FaithfullyFlat.trans R S V

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring

Goal state before:
pp: case add
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : AddMonoid ι
inst✝⁴ : Semiring A
inst✝³ : SetLike σ A
inst✝² : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝¹ : DecidableEq ι
inst✝ : GradedRing 𝒜
s : Set A
h : ∀ (i : ι) ⦃x : A⦄, x ∈ s → ↑(((decompose 𝒜) x) i) ∈ s
x x✝ y✝ : A
hx✝ : x✝ ∈ Subsemiring.closure s
hy✝ : y✝ ∈ Subsemiring.closure s
h₁ : ∀ (i : ι), ↑(((decompose 𝒜) x✝) i) ∈ Subsemiring.closure s
h₂ : ∀ (i : ι), ↑(((decompose 𝒜) y✝) i) ∈ Subsemiring.closure s
i : ι
⊢ ↑(((decompose 𝒜) (x✝ + y✝)) i) ∈ Subsemiring.closure s

Tactic:
| add _ _ _ _ h₁ h₂ =>

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.AlgHom

Goal state before:
pp: R : Type u_1
A : Type u_6
ι : Type u_10
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
𝒜 : ι → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : 𝒜 →ₐᵍ[R] 𝒜
n x✝¹ : ℕ
ih : ⇑(f ^ x✝¹) = (⇑f)^[x✝¹]
x✝ : A
⊢ (f ^ x✝¹.succ) x✝ = (⇑f)^[x✝¹.succ] x✝

Tactic:
simp [pow_succ, ih]

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
α : Type u_5
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
s : SummableFamily Γ R α
g : Γ
hg : ∑ᶠ (i : α), (s i).coeff g ≠ 0
⊢ g ∈ ⋃ a, (s a).support

Tactic:
finsum_eq_sum _ (s.finite_co_support _)

Goal state after:
Γ : Type u_1
R : Type u_3
α : Type u_5
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
s : SummableFamily Γ R α
g : Γ
hg : ∑ i ∈ Set.Finite.toFinset ⋯, (s i).coeff g ≠ 0
⊢ g ∈ ⋃ a, (s a).support
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : AddCommMonoid R
ι : Type u_7
inst✝ : DecidableEq ι
i : ι
x : R⟦Γ⟧
g : Γ
⊢ ∑ᶠ (i_1 : ι), ((single i x) i_1).coeff g = x.coeff g

Tactic:
finsum_eq_single _ i,

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : AddCommMonoid R
ι : Type u_7
inst✝ : DecidableEq ι
i : ι
x : R⟦Γ⟧
g : Γ
⊢ ((single i x) i).coeff g = x.coeff g

Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : AddCommMonoid R
ι : Type u_7
inst✝ : DecidableEq ι
i : ι
x : R⟦Γ⟧
g : Γ
⊢ ∀ (x_1 : ι), x_1 ≠ i → ((single i x) x_1).coeff g = 0
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
σ : Type u_3
F : FormalGroup R
f : MvPowerSeries σ R
hf : PowerSeries.HasSubst f
⊢ subst ![f, 0] F.toPowerSeries = subst (fun x ↦ f) (subst ![PowerSeries.X, 0] F.toPowerSeries)

Tactic:
subst_comp_subst_apply _ hf.const

Goal state after:
R : Type u_1
inst✝ : CommRing R
σ : Type u_3
F : FormalGroup R
f : MvPowerSeries σ R
hf : PowerSeries.HasSubst f
⊢ subst ![f, 0] F.toPowerSeries = subst (fun s ↦ subst (fun x ↦ f) (![PowerSeries.X, 0] s)) F.toPowerSeries

R : Type u_1
inst✝ : CommRing R
σ : Type u_3
F : FormalGroup R
f : MvPowerSeries σ R
hf : PowerSeries.HasSubst f
⊢ HasSubst ![PowerSeries.X, 0]
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
σ : Type u_3
F : FormalGroup R
f : MvPowerSeries σ R
hf : PowerSeries.HasSubst f
⊢ subst ![0, f] F.toPowerSeries = subst (fun x ↦ f) (subst ![0, PowerSeries.X] F.toPowerSeries)

Tactic:
subst_comp_subst_apply _ hf.const

Goal state after:
R : Type u_1
inst✝ : CommRing R
σ : Type u_3
F : FormalGroup R
f : MvPowerSeries σ R
hf : PowerSeries.HasSubst f
⊢ subst ![0, f] F.toPowerSeries = subst (fun s ↦ subst (fun x ↦ f) (![0, PowerSeries.X] s)) F.toPowerSeries

R : Type u_1
inst✝ : CommRing R
σ : Type u_3
F : FormalGroup R
f : MvPowerSeries σ R
hf : PowerSeries.HasSubst f
⊢ HasSubst ![0, PowerSeries.X]
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✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
f : α →₀ R⟦Γ⟧
a : α
g : Γ
hg : g ∈ (f a).support
⊢ (f a).support.Nonempty

Tactic:
exact ⟨g, hg⟩

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

Goal state before:
pp: case mpr
Γ : Type u_1
R : Type u_3
inst✝⁴ : AddCommGroup Γ
inst✝³ : LinearOrder Γ
inst✝² : IsOrderedAddMonoid Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : R⟦Γ⟧
u i : R
ui : u * i = 1
iu : i * x.leadingCoeff = 1
hx : u = x.leadingCoeff
⊢ IsUnit x

Tactic:
have h :=
      SummableFamily.one_sub_self_mul_hsum_powers (unit_aux x iu _ (neg_add_cancel x.order))

Goal state after:
case mpr
Γ : Type u_1
R : Type u_3
inst✝⁴ : AddCommGroup Γ
inst✝³ : LinearOrder Γ
inst✝² : IsOrderedAddMonoid Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : R⟦Γ⟧
u i : R
ui : u * i = 1
iu : i * x.leadingCoeff = 1
hx : u = x.leadingCoeff
h : (1 - (1 - (single (-x.order)) i * x)) * (SummableFamily.powers (1 - (single (-x.order)) i * x)).hsum = 1
⊢ IsUnit x
Module: Mathlib.RingTheory.KrullDimension.LocalRing

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
x✝ : ¬IsField R ∧ ∀ (x : R), x ≠ 0 → IsLocalRing.maximalIdeal R ≤ (Ideal.span {x}).radical
hn : ¬IsField R
h✝ : ∀ (x : R), x ≠ 0 → IsLocalRing.maximalIdeal R ≤ (Ideal.span {x}).radical
h : ringKrullDim R ≤ 0
⊢ False

Tactic:
have : Ring.KrullDimLE 0 R := Ring.krullDimLE_iff.mpr h
      exact hn Ring.KrullDimLE.isField_of_isDomain

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
x✝ : ¬IsField R ∧ ∀ (x : R), x ≠ 0 → IsLocalRing.maximalIdeal R ≤ (Ideal.span {x}).radical
hn : ¬IsField R
h : ∀ (x : R), x ≠ 0 → IsLocalRing.maximalIdeal R ≤ (Ideal.span {x}).radical
this : ¬ringKrullDim R ≤ 0
I : Ideal R
hI : I ≠ ⊥
hI_prime : I.IsPrime
⊢ ∃ x ∈ I, x ≠ 0

Tactic:
apply by_contradiction fun h ↦ (hI (le_antisymm (fun x ↦ ?_) bot_le))

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
x✝ : ¬IsField R ∧ ∀ (x : R), x ≠ 0 → IsLocalRing.maximalIdeal R ≤ (Ideal.span {x}).radical
hn : ¬IsField R
h✝ : ∀ (x : R), x ≠ 0 → IsLocalRing.maximalIdeal R ≤ (Ideal.span {x}).radical
this : ¬ringKrullDim R ≤ 0
I : Ideal R
hI : I ≠ ⊥
hI_prime : I.IsPrime
h : ¬∃ x ∈ I, x ≠ 0
x : R
⊢ x ∈ I → x ∈ ⊥
Module: Mathlib.RingTheory.KrullDimension.PID

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
h : ¬IsField R
h' : ringKrullDim R < 1
h'' : ringKrullDim R ≤ 0
⊢ IsField R

Tactic:
rw [← Nat.cast_zero, ← Ring.krullDimLE_iff] at h''

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
h : ¬IsField R
h' : ringKrullDim R < 1
h'' : Ring.KrullDimLE 0 R
⊢ IsField R
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
⊢ (Ideal.map C p).height = p.height

Tactic:
have : (p.map C).LiesOver p := ⟨IsMaximal.eq_of_le inferInstance IsPrime.ne_top' le_comap_map⟩
  simp [height_eq_height_add_of_liesOver_of_hasGoingDown p]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
p₁ p₀ : PrimeSpectrum R
h₀ : p₀ < p₁
h₁ : p₁ < closedPoint R
x : R
hx : x ∈ 𝔪
hn : x ∉ p₀.asIdeal
e : ↑(zeroLocus ↑p₀.asIdeal) ≃o PrimeSpectrum (R ⧸ p₀.asIdeal) := p₀.asIdeal.primeSpectrumQuotientOrderIsoZeroLocus.symm
q✝ : Ideal R
hq : q✝ ∈ (p₀.asIdeal + span {x}).minimalPrimes
q : PrimeSpectrum R := { asIdeal := q✝, isPrime := ⋯ }
this : q.asIdeal.IsPrime
hxq : x ∈ q.asIdeal
⊢ ∃ q, x ∈ q.asIdeal ∧ p₀ < q ∧ q.asIdeal < 𝔪

Tactic:
refine ⟨q, hxq, lt_of_le_not_ge (le_sup_left.trans hq.1.2) fun h ↦ hn (h hxq), ?_⟩

Goal state after:
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
p₁ p₀ : PrimeSpectrum R
h₀ : p₀ < p₁
h₁ : p₁ < closedPoint R
x : R
hx : x ∈ 𝔪
hn : x ∉ p₀.asIdeal
e : ↑(zeroLocus ↑p₀.asIdeal) ≃o PrimeSpectrum (R ⧸ p₀.asIdeal) := p₀.asIdeal.primeSpectrumQuotientOrderIsoZeroLocus.symm
q✝ : Ideal R
hq : q✝ ∈ (p₀.asIdeal + span {x}).minimalPrimes
q : PrimeSpectrum R := { asIdeal := q✝, isPrime := ⋯ }
this : q.asIdeal.IsPrime
hxq : x ∈ q.asIdeal
⊢ q.asIdeal < 𝔪
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
⊢ ringKrullDim (R ⧸ ofList rs) + ↑rs.length = ringKrullDim R

Tactic:
have eq : ofList rs = ofList rs • (⊤ : Ideal R) := by simp
  rw [ringKrullDim_eq_of_ringEquiv (quotientEquivAlgOfEq R eq).toRingEquiv,
    ← supportDim_quotient_eq_ringKrullDim, ← supportDim_self_eq_ringKrullDim]
  exact supportDim_add_length_eq_supportDim_of_isRegular rs reg

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 := ⋯ }
N : OpenNormalSubgroup G
g : G ⧸ ↑N.toOpenSubgroup
hg : Ideal.under (↥(B' ↥↑N.toOpenSubgroup)) Q = g • Ideal.under (↥(B' ↥↑N.toOpenSubgroup)) P
⊢ Nonempty (F.obj N)

Tactic:
exact ⟨g, hg⟩

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
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra S T
inst✝³ : Algebra R T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalIso R S
inst✝ : IsLocalIso S T
s : Set S := {g | IsStandardOpenImmersion R (Localization.Away g)}
T' : S → Type u_3 := fun g ↦ Localization.Away ((algebraMap S T) g)
this✝ : (g : S) → Algebra (Localization.Away g) (T' g) := fun g ↦ localizationAlgebra (Submonoid.powers g) T
T'' : S → T → Type u_3 := fun g x ↦ Localization.Away ((algebraMap T (T' g)) x)
t : S → Set T := fun g ↦ {x | IsStandardOpenImmersion (Localization.Away g) (T'' g x)}
ι : Type (max u_3 u_2) := (i : ↑s) × ↑(t ↑i)
this : ∀ (i : ι), IsStandardOpenImmersion (Localization.Away ↑i.fst) (T'' ↑i.fst ↑i.snd)
h1 : Ideal.span (⇑(algebraMap S T) '' {g | IsStandardOpenImmersion R (Localization.Away g)}) = ⊤
g : S
hg : IsStandardOpenImmersion R (Localization.Away g)
x : T
hx : IsStandardOpenImmersion S (Localization.Away x)
⊢ IsStandardOpenImmersion (Localization.Away g) (T'' g x)

Tactic:
let : Algebra (Localization.Away x) (T'' g x) :=
    localizationAlgebra (.powers x) (T' g)

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra S T
inst✝³ : Algebra R T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalIso R S
inst✝ : IsLocalIso S T
s : Set S := {g | IsStandardOpenImmersion R (Localization.Away g)}
T' : S → Type u_3 := fun g ↦ Localization.Away ((algebraMap S T) g)
this✝¹ : (g : S) → Algebra (Localization.Away g) (T' g) := fun g ↦ localizationAlgebra (Submonoid.powers g) T
T'' : S → T → Type u_3 := fun g x ↦ Localization.Away ((algebraMap T (T' g)) x)
t : S → Set T := fun g ↦ {x | IsStandardOpenImmersion (Localization.Away g) (T'' g x)}
ι : Type (max u_3 u_2) := (i : ↑s) × ↑(t ↑i)
this✝ : ∀ (i : ι), IsStandardOpenImmersion (Localization.Away ↑i.fst) (T'' ↑i.fst ↑i.snd)
h1 : Ideal.span (⇑(algebraMap S T) '' {g | IsStandardOpenImmersion R (Localization.Away g)}) = ⊤
g : S
hg : IsStandardOpenImmersion R (Localization.Away g)
x : T
hx : IsStandardOpenImmersion S (Localization.Away x)
this : Algebra (Localization.Away x) (T'' g x) := localizationAlgebra (Submonoid.powers x) (T' g)
⊢ IsStandardOpenImmersion (Localization.Away g) (T'' g x)
Module: Mathlib.RingTheory.LocalProperties.Semilocal

Goal state before:
pp: R : Type u_1
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Finite (MaximalSpectrum R)
M : Type u_2
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_3
inst✝⁷ : (P : Ideal R) → [inst : P.IsMaximal] → CommSemiring (Rₚ P)
inst✝⁶ : (P : Ideal R) → [inst : P.IsMaximal] → Algebra R (Rₚ P)
inst✝⁵ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_4
inst✝⁴ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝³ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → Module (Rₚ P) (Mₚ P)
inst✝¹ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsScalarTower R (Rₚ P) (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
H : ∀ (P : Ideal R) [inst : P.IsMaximal], Module.Finite (Rₚ P) (Mₚ P)
this : Fintype (MaximalSpectrum R)
s : (P : MaximalSpectrum R) → Finset (Mₚ P.asIdeal)
hs : ∀ (P : MaximalSpectrum R), Submodule.span (Rₚ P.asIdeal) ↑(s P) = ⊤
frac : (P : MaximalSpectrum R) → Mₚ P.asIdeal → M × ↥P.asIdeal.primeCompl
hfrac : ∀ (P : MaximalSpectrum R) (y : Mₚ P.asIdeal), (frac P y).2 • y = (f P.asIdeal) (frac P y).1
⊢ Module.Finite R M

Tactic:
use Finset.biUnion Finset.univ fun P ↦ Finset.image (frac P · |>.1) (s P)

Goal state after:
case h
R : Type u_1
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Finite (MaximalSpectrum R)
M : Type u_2
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_3
inst✝⁷ : (P : Ideal R) → [inst : P.IsMaximal] → CommSemiring (Rₚ P)
inst✝⁶ : (P : Ideal R) → [inst : P.IsMaximal] → Algebra R (Rₚ P)
inst✝⁵ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_4
inst✝⁴ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝³ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → Module (Rₚ P) (Mₚ P)
inst✝¹ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsScalarTower R (Rₚ P) (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
H : ∀ (P : Ideal R) [inst : P.IsMaximal], Module.Finite (Rₚ P) (Mₚ P)
this : Fintype (MaximalSpectrum R)
s : (P : MaximalSpectrum R) → Finset (Mₚ P.asIdeal)
hs : ∀ (P : MaximalSpectrum R), Submodule.span (Rₚ P.asIdeal) ↑(s P) = ⊤
frac : (P : MaximalSpectrum R) → Mₚ P.asIdeal → M × ↥P.asIdeal.primeCompl
hfrac : ∀ (P : MaximalSpectrum R) (y : Mₚ P.asIdeal), (frac P y).2 • y = (f P.asIdeal) (frac P y).1
⊢ Submodule.span R ↑(Finset.univ.biUnion fun P ↦ Finset.image (fun x ↦ (frac P x).1) (s P)) = ⊤
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)
⊢ x ∈
      comap ((↑(RingEquiv.symm ((MulSemiringAction.toRingAut G B) a))).comp (algebraMap (↥(B' ↥↑N.toOpenSubgroup)) B))
        Q ↔
    x ∈
      comap
        ((algebraMap (↥(FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup)) B).comp
          ↑(RingEquiv.symm
              ((MulSemiringAction.toRingAut (G ⧸ ↑N.toOpenSubgroup) ↥(FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup))
                ↑↑(s N))))
        Q

Tactic:
congr! 2

Goal state after:
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)
⊢ (↑(RingEquiv.symm ((MulSemiringAction.toRingAut G B) a))).comp (algebraMap (↥(B' ↥↑N.toOpenSubgroup)) B) =
    (algebraMap (↥(FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup)) B).comp
      ↑(RingEquiv.symm
          ((MulSemiringAction.toRingAut (G ⧸ ↑N.toOpenSubgroup) ↥(FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup))
            ↑↑(s N)))
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
P : Ideal A
Q : Ideal B
inst✝² : Q.IsPrime
inst✝¹ : Q.LiesOver P
inst✝ : Algebra.IsInvariant A B G
⊢ Function.Surjective ⇑(stabilizerHom Q P G)

Tactic:
intro σ
  let B' := FixedPoints.subalgebra A B
  obtain ⟨s, hs⟩ := nonempty_sections_of_finite_cofiltered_system
    (stabilizerHomSurjectiveAuxFunctor (G := G) P Q σ)
  let a := (ProfiniteGrp.of G).isoLimittoFiniteQuotientFunctor.inv.hom
    ⟨fun N ↦ (s N).1.1, (fun {N N'} f ↦ congr($(hs f).1.1))⟩
  have (N : OpenNormalSubgroup G) : QuotientGroup.mk (s := N.1.1) a = (s N).1 :=
    congr_fun (congr_arg Subtype.val (ConcreteCategory.congr_hom (ProfiniteGrp.of
      G).isoLimittoFiniteQuotientFunctor.inv_hom_id
        _)) N
  refine ⟨⟨a, ?_⟩, ?_⟩
  · ext x
    obtain ⟨N, hN⟩ := ProfiniteGrp.exist_openNormalSubgroup_sub_open_nhds_of_one
      (stabilizer_isOpen G x) (one_mem _)
    lift x to B' N.1.1 using fun g ↦ hN g.2
    change x ∈ (a • Q).under (B' N.1.1) ↔ x ∈ Q.under (B' N.1.1)
    rw [← (s N).1.2]
    simp only [Ideal.comap_comap, Ideal.pointwise_smul_eq_comap, ← Ideal.comap_coe
          (F := RingEquiv _ _)]
    congr! 2
    ext y
    rw [← this]
    rfl
  · ext x
    obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
    obtain ⟨N, hN⟩ := ProfiniteGrp.exist_openNormalSubgroup_sub_open_nhds_of_one
      (stabilizer_isOpen G x) (one_mem _)
    lift x to B' N.1.1 using fun g ↦ hN g.2
    change Ideal.Quotient.mk Q (QuotientGroup.mk (s := N) a • x).1 = _
    rw [this]
    exact DFunLike.congr_fun (s N).2 (Ideal.Quotient.mk _ x)

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
⊢ (ofPowerSeries ℤ R) x.powerSeriesPart = (single (-order x)) 1 * x

Tactic:
refine Eq.trans ?_ (congr rfl x.single_order_mul_powerSeriesPart)
  rw [← mul_assoc, single_mul_single, neg_add_cancel, mul_one, ← C_apply, C_one, one_mul]

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

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

Tactic:
if_neg (Int.natCast_nonneg _).not_gt,

Goal state after:
case ofNat
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
a✝ : ℕ
⊢ (coeff a✝) f = (coeff (↑a✝).natAbs) f
Module: Mathlib.RingTheory.LaurentSeries

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

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

Tactic:
· rw [Int.ofNat_eq_natCast, coeff_coe_powerSeries, if_neg (Int.natCast_nonneg _).not_gt,
      Int.natAbs_natCast]

Goal state after:
case negSucc
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
a✝ : ℕ
⊢ ((ofPowerSeries ℤ R) f).coeff (Int.negSucc a✝) = if Int.negSucc a✝ < 0 then 0 else (coeff (Int.negSucc a✝).natAbs) f
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case pos
K : Type u_2
inst✝ : Field K
D : ℤ
f : K⸨X⸩
h_val_f : ∀ n < D, f.coeff n = 0
F : K⟦X⟧ := f.powerSeriesPart
ord_nonpos : HahnSeries.order f ≤ 0
s : ℕ
hs : HahnSeries.order f = -↑s
⊢ Valued.v ((ofPowerSeries ℤ K) f.powerSeriesPart) ≤ exp (-(D + ↑s))

Tactic:
by_cases! hDs : D + s ≤ 0
      · apply le_trans ((PowerSeries.idealX K).valuation_le_one F)
        rwa [← log_le_iff_le_exp one_ne_zero, le_neg, log_one, neg_zero]
      · obtain ⟨d, hd⟩ := Int.eq_ofNat_of_zero_le hDs.le
        rw [hd]
        apply (intValuation_le_iff_coeff_lt_eq_zero K F).mpr
        intro n hn
        rw [powerSeriesPart_coeff f n, hs]
        apply h_val_f
        lia

Goal state after: