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

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
a✝ b✝ : Kˣ ⧸ (powMonoidHom n).range
hx : a✝ ∈ {x | ∀ v ∉ S, (v.valuationOfNeZeroMod n) x = 1}
hy : b✝ ∈ {x | ∀ v ∉ S, (v.valuationOfNeZeroMod n) x = 1}
v : HeightOneSpectrum R
hv : v ∉ S
⊢ 1 * (v.valuationOfNeZeroMod n) b✝ = 1

Tactic:
hy v hv,

Goal state after:
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
a✝ b✝ : Kˣ ⧸ (powMonoidHom n).range
hx : a✝ ∈ {x | ∀ v ∉ S, (v.valuationOfNeZeroMod n) x = 1}
hy : b✝ ∈ {x | ∀ v ∉ S, (v.valuationOfNeZeroMod n) x = 1}
v : HeightOneSpectrum R
hv : v ∉ S
⊢ 1 * 1 = 1
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: case neg
A : Type u_1
inst✝² : CommSemiring A
M : Type u_2
inst✝¹ : AddCommMonoid M
I : AddSubmonoid M
dpow : ℕ → M → A
dpow_zero : ∀ {x : M}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_3
inst✝ : DecidableEq ι
x : ι → M
dpow_add : ∀ {n : ℕ} {x y : M}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_1 ∈ range n.succ, dpow x_1 x * dpow (n - x_1) y
hx : ∀ i ∈ ∅, x i ∈ I
n : ℕ
hn : ¬n = 0
⊢ dpow n 0 = ↑(#(∅.sym n))

Tactic:
rw [dpow_eval_zero hn, eq_comm, ← cast_zero]

Goal state after:
case neg
A : Type u_1
inst✝² : CommSemiring A
M : Type u_2
inst✝¹ : AddCommMonoid M
I : AddSubmonoid M
dpow : ℕ → M → A
dpow_zero : ∀ {x : M}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_3
inst✝ : DecidableEq ι
x : ι → M
dpow_add : ∀ {n : ℕ} {x y : M}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_1 ∈ range n.succ, dpow x_1 x * dpow (n - x_1) y
hx : ∀ i ∈ ∅, x i ∈ I
n : ℕ
hn : ¬n = 0
⊢ ↑(#(∅.sym n)) = ↑0
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: R : Type u_4
M : Type u_5
ι : Type u_6
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
hv : Submodule.span R (Set.range v) = ⊤
p : DividedPowerAlgebra R M
⊢ p ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))

Tactic:
induction p using DividedPowerAlgebra.induction_on with

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.DPMorphism

Goal state before:
pp: A : Type u_3
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
S : Set A
hS : I = span S
hdp : ∀ {n : ℕ}, ∀ a ∈ S, hI.dpow n a = hI'.dpow n a
⊢ hI' = hI

Tactic:
ext n a

Goal state after:
A : Type u_3
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
S : Set A
hS : I = span S
hdp : ∀ {n : ℕ}, ∀ a ∈ S, hI.dpow n a = hI'.dpow n a
n : ℕ
a : A
x✝ : a ∈ I
⊢ hI'.dpow n a = hI.dpow n a
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
⊢ ofRingEquiv ⋯ (ofRingEquiv h hI) = hI

Tactic:
ext n a

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
n : ℕ
a : A
x✝ : a ∈ I
⊢ (ofRingEquiv ⋯ (ofRingEquiv h hI)).dpow n a = hI.dpow n a
Module: Mathlib.RingTheory.DividedPowers.Padic

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ DividedPowers (Ideal.span {↑p})

Tactic:
by
  classical
  refine ofInjective (Ideal.span {(p : ℤ_[p])}) (⊤)
    PadicInt.Coe.ringHom ((Set.injective_codRestrict Subtype.property).mp fun ⦃a₁ a₂⦄ a ↦ a)
    (RatAlgebra.dividedPowers (⊤ : Ideal ℚ_[p])) ?_ ?_
  · rw [Ideal.map_span, Set.image_singleton, map_natCast]
    simp only [Ideal.span_singleton_eq_top, isUnit_iff_ne_zero, ne_eq, cast_eq_zero]
    exact Nat.Prime.ne_zero hp.elim
  · intro n x hx
    exact ⟨⟨dpow' p n x, dpow'_int p n hx⟩, fun hn ↦ dpow'_mem p hn hx, by
      simp [dpow', inverse_eq_inv', Coe.ringHom_apply, RatAlgebra.dpow_apply,
        Submodule.mem_top, ↓reduceIte]⟩

Goal state after:
Module: Mathlib.RingTheory.Extension.ExtendScalars

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ Function.Surjective ⇑(map (defaultHom R S P))

Tactic:
rw [← LinearMap.range_eq_top,
    ← (Submodule.map_injective_of_injective h1Cotangentι_injective).eq_iff,
    ← LinearMap.range_comp, ← P.h1CotangentEquivCotangent_comp_map, LinearMap.range_comp,
    ← (Algebra.H1Cotangent.exact_map_δ R P.Ring S).linearMap_ker_eq, Submodule.map_top,
    ← exact_hCotangentι_cotangentComplex.linearMap_ker_eq, Submodule.map_equiv_eq_comap_symm,
    LinearMap.ker, LinearMap.ker, ← Submodule.comap_comp]

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ Submodule.comap (H1Cotangent.δ R P.Ring S ∘ₗ ↑P.h1CotangentEquivCotangent.symm) ⊥ =
    Submodule.comap P.cotangentComplex ⊥
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective ⇑f
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
m✝ n✝ : ℕ
hn : n✝ ≠ 0
a : A
ha : a ∈ I
hx : f a ∈ J
⊢ f (hI.dpow m✝ (hI.dpow n✝ a)) = ↑(m✝.uniformBell n✝) * f (hI.dpow (m✝ * n✝) a)

Tactic:
rw [hI.dpow_comp hn ha, _root_.map_mul, map_natCast]

Goal state after:
Module: Mathlib.RingTheory.Frobenius

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
G : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulSemiringAction G S
inst✝⁴ : SMulCommClass G R S
Q : Ideal S
inst✝³ : Finite G
inst✝² : Algebra.IsInvariant R S G
inst✝¹ : Q.IsPrime
inst✝ : Finite (S ⧸ Q)
P : Ideal R := Ideal.under R Q
⊢ ∃ σ, IsArithFrobAt R σ Q

Tactic:
have := Algebra.IsInvariant.isIntegral R S G

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
G : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulSemiringAction G S
inst✝⁴ : SMulCommClass G R S
Q : Ideal S
inst✝³ : Finite G
inst✝² : Algebra.IsInvariant R S G
inst✝¹ : Q.IsPrime
inst✝ : Finite (S ⧸ Q)
P : Ideal R := Ideal.under R Q
this : Algebra.IsIntegral R S
⊢ ∃ σ, IsArithFrobAt R σ Q
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
σ : Type u_3
F : FormalGroup R
f₀ f₁ f₂ : MvPowerSeries σ R
h₀ : PowerSeries.HasSubst f₀
h₁ : PowerSeries.HasSubst f₁
h₂ : PowerSeries.HasSubst f₂
aux₁ : HasSubst ![subst ![Y₀, Y₁] F.toPowerSeries, Y₂]
aux₂ : HasSubst ![Y₀, subst ![Y₁, Y₂] F.toPowerSeries]
this : HasSubst ![f₀, f₁, f₂]
⊢ subst ![f₀, f₁, f₂] (subst ![subst ![Y₀, Y₁] F.toPowerSeries, Y₂] F.toPowerSeries) =
    subst ![f₀, subst ![f₁, f₂] F.toPowerSeries] F.toPowerSeries

Tactic:
rw [F.assoc, subst_comp_subst_apply aux₂ this]
      congr! 2 with s
      fin_cases s
      · simp [subst_X this]
      · simp only [Fin.mk_one, Matrix.cons_val_one, Matrix.cons_val_fin_one,
          subst_comp_subst_apply HasSubst.X_X this]
        congr! 2 with s
        fin_cases s <;> simp [subst]

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

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝⁴ : LinearOrder Γ
inst✝³ : AddCommMonoid Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : CommRing R
inst✝ : BinomialRing R
g : Γ
hg : 0 < g
r s : R
k : ℕ
⊢ (↑↑(toOrderTopSubOnePos ⋯ ^ s)).coeff (k • g) = Ring.choose s k • r ^ k

Tactic:
by
  simp only [val_toOrderTopSubOnePos_coe, binomial_power, coeff_hsum, smul_eq_mul]
  rw [finsum_eq_single _ k, binomialFamily_apply (orderTop_sub_pos hg r), add_sub_cancel_left,
    single_pow, coeff_smul, coeff_single_same (k • g) (r ^ k), smul_eq_mul]
  intro n hn
  rw [binomialFamily_apply, add_sub_cancel_left, coeff_smul, single_pow, coeff_single_of_ne,
    smul_zero]
  · contrapose hn
    apply (StrictMono.injective (nsmul_left_strictMono hg)) hn.symm
  · by_cases hr : r = 0 <;> simp [hr, hg]

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

Goal state before:
pp: case pos.refine_2
Γ : Type u_1
R : Type u_3
V : Type u_4
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : LinearOrder Γ
inst✝³ : IsOrderedCancelAddMonoid Γ
inst✝² : CommRing R
inst✝¹ : CommRing V
inst✝ : Algebra R V
x : V⟦Γ⟧
a b : PowerSeries R
h : 0 < x.orderTop
g : Γ
i : (_ : ℕ) × ℕ × ℕ
his : i ∉ (fun x ↦ ⟨x.1 + x.2, x⟩) '' ↑⋯.toFinset
hisc :
  ∀ (j k : ℕ), ⟨j + k, (j, k)⟩ = i → (PowerSeries.coeff k) b • (PowerSeries.coeff j) a • (x ^ j * x ^ k).coeff g = 0
hi : i.fst ∈ image (fun i ↦ i.1 + i.2) ⋯.toFinset ∧ i.snd.1 + i.snd.2 = i.fst
⊢ (PowerSeries.coeff i.snd.2) b • (PowerSeries.coeff i.snd.1) a • (x ^ i.snd.1 * x ^ i.snd.2).coeff g = 0

Tactic:
exact hisc i.snd.1 i.snd.2 <| Sigma.eq hi.2 (by simp)

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

Goal state before:
pp: case ha
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
⊢ HasSubst ![0, PowerSeries.X]

Tactic:
· exact HasSubst.zero_X

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
this : PowerSeries.HasSubst (subst ![0, PowerSeries.X] F.toPowerSeries)
⊢ HasSubst ![0, PowerSeries.X]

Tactic:
· exact HasSubst.zero_X

Goal state after:
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
⊢ HasSubst ![0, PowerSeries.X]

Tactic:
· exact HasSubst.zero_X

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ Order.krullDim (PrimeSpectrum R[X]) ≤ 2 * ringKrullDim R + 1

Tactic:
ringKrullDim

Goal state after:
R : Type u_1
inst✝ : CommRing R
⊢ Order.krullDim (PrimeSpectrum R[X]) ≤ 2 * Order.krullDim (PrimeSpectrum R) + 1
Module: Mathlib.RingTheory.Spectrum.Prime.LTSeries

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
x : R
n : ℕ
hn :
  ∀ (p : LTSeries (PrimeSpectrum R)),
    x ∈ (RelSeries.last p).asIdeal →
      p.length = n →
        ∃ q,
          x ∈ (q.toFun 1).asIdeal ∧
            n = q.length ∧ RelSeries.head p = RelSeries.head q ∧ RelSeries.last p = RelSeries.last q
p : LTSeries (PrimeSpectrum R)
hx : x ∈ (RelSeries.last p).asIdeal
hp : p.length = n + 1
h0 : ¬n = 0
⊢ ∃ q,
    x ∈ (q.toFun 1).asIdeal ∧
      n + 1 = q.length ∧ RelSeries.head p = RelSeries.head q ∧ RelSeries.last p = RelSeries.last q

Tactic:
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

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
x : R
n : ℕ
hn :
  ∀ (p : LTSeries (PrimeSpectrum R)),
    x ∈ (RelSeries.last p).asIdeal →
      p.length = n →
        ∃ q,
          x ∈ (q.toFun 1).asIdeal ∧
            n = q.length ∧ RelSeries.head p = RelSeries.head q ∧ RelSeries.last p = RelSeries.last q
p : LTSeries (PrimeSpectrum R)
hx : x ∈ (RelSeries.last p).asIdeal
hp : p.length = n + 1
h0 : ¬n = 0
q : PrimeSpectrum R
hxq : x ∈ q.asIdeal
h2 : p.toFun ⟨p.length - 2, ?m.192⟩ < q
hq : q < RelSeries.last p
⊢ ∃ q,
    x ∈ (q.toFun 1).asIdeal ∧
      n + 1 = q.length ∧ RelSeries.head p = RelSeries.head q ∧ RelSeries.last p = RelSeries.last q
Module: Mathlib.RingTheory.KrullDimension.Regular

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
x : R
reg : IsSMulRegular R x
hx : x ∈ maximalIdeal R
⊢ x ∈ Ring.jacobson R

Tactic:
by
    rwa [ringJacobson_eq_maximalIdeal R]

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

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommRing R
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
s : Set R
hs : Ideal.span s = ⊤
Mₚ : ↑s → Type u_3
inst✝⁷ : (g : ↑s) → AddCommGroup (Mₚ g)
inst✝⁶ : (g : ↑s) → Module R (Mₚ g)
Rₚ : ↑s → Type u_4
inst✝⁵ : (g : ↑s) → CommRing (Rₚ g)
inst✝⁴ : (g : ↑s) → Algebra R (Rₚ g)
inst✝³ : ∀ (g : ↑s), IsLocalization.Away (↑g) (Rₚ g)
inst✝² : (g : ↑s) → Module (Rₚ g) (Mₚ g)
inst✝¹ : ∀ (g : ↑s), IsScalarTower R (Rₚ g) (Mₚ g)
ϕ : (g : ↑s) → M →ₗ[R] Mₚ g
inst✝ : ∀ (g : ↑s), IsLocalizedModule (Submonoid.powers ↑g) (ϕ g)
h : ∀ (g : ↑s), FinitePresentation (Rₚ g) (Mₚ g)
⊢ FinitePresentation R M

Tactic:
have : Module.Finite R M :=
    Module.Finite.of_localizationSpan' (Rₚ := Rₚ) s hs ϕ (fun _ ↦ inferInstance)

Goal state after:
R : Type u_1
inst✝¹⁰ : CommRing R
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
s : Set R
hs : Ideal.span s = ⊤
Mₚ : ↑s → Type u_3
inst✝⁷ : (g : ↑s) → AddCommGroup (Mₚ g)
inst✝⁶ : (g : ↑s) → Module R (Mₚ g)
Rₚ : ↑s → Type u_4
inst✝⁵ : (g : ↑s) → CommRing (Rₚ g)
inst✝⁴ : (g : ↑s) → Algebra R (Rₚ g)
inst✝³ : ∀ (g : ↑s), IsLocalization.Away (↑g) (Rₚ g)
inst✝² : (g : ↑s) → Module (Rₚ g) (Mₚ g)
inst✝¹ : ∀ (g : ↑s), IsScalarTower R (Rₚ g) (Mₚ g)
ϕ : (g : ↑s) → M →ₗ[R] Mₚ g
inst✝ : ∀ (g : ↑s), IsLocalizedModule (Submonoid.powers ↑g) (ϕ g)
h : ∀ (g : ↑s), FinitePresentation (Rₚ g) (Mₚ g)
this : Module.Finite R M
⊢ FinitePresentation R M
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
⊢ ∃ g, Q = g • P

Tactic:
let B' := FixedPoints.subalgebra A B

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.63) → [inst : Monoid G] → [inst_1 : MulSemiringAction G B] → [SMulCommClass G A B] → Subalgebra A B :=
  FixedPoints.subalgebra A B
⊢ ∃ g, Q = g • P
Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension

Goal state before:
pp: case succ
R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
n : ℕ
M : ModuleCat R
inst✝ : Module.Finite R ↑M
P : Type v
w✝³ : AddCommGroup P
w✝² : Module R P
w✝¹ : Module.Free R P
w✝ : Module.Finite R P
f : P →ₗ[R] ↑M
ih :
  HasProjectiveDimensionLT (of R ↥f.ker) (n + 1) ↔
    ∀ (m : MaximalSpectrum R), HasProjectiveDimensionLT ((of R ↥f.ker).localizedModule m.asIdeal.primeCompl) (n + 1)
surjf : Function.Surjective ⇑f
S : ShortComplex (ModuleCat R) := f.shortComplexKer
S_exact : f.shortComplexKer.ShortExact
proj : Projective S.X₂
Sp : (p : MaximalSpectrum R) → ShortComplex (ModuleCat (Localization p.asIdeal.primeCompl)) :=
  fun p ↦ S.map (localizedModuleFunctor p.asIdeal.primeCompl)
Sp_exact : ∀ (p : MaximalSpectrum R), (Sp p).ShortExact
projp : ∀ (p : MaximalSpectrum R), Projective (Sp p).X₂
⊢ HasProjectiveDimensionLT f.shortComplexKer.X₁ (n + 1) ↔
    ∀ (m : MaximalSpectrum R), HasProjectiveDimensionLT (M.localizedModule m.asIdeal.primeCompl) (n + 1 + 1)

Tactic:
ih

Goal state after:
case succ
R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
n : ℕ
M : ModuleCat R
inst✝ : Module.Finite R ↑M
P : Type v
w✝³ : AddCommGroup P
w✝² : Module R P
w✝¹ : Module.Free R P
w✝ : Module.Finite R P
f : P →ₗ[R] ↑M
ih :
  HasProjectiveDimensionLT (of R ↥f.ker) (n + 1) ↔
    ∀ (m : MaximalSpectrum R), HasProjectiveDimensionLT ((of R ↥f.ker).localizedModule m.asIdeal.primeCompl) (n + 1)
surjf : Function.Surjective ⇑f
S : ShortComplex (ModuleCat R) := f.shortComplexKer
S_exact : f.shortComplexKer.ShortExact
proj : Projective S.X₂
Sp : (p : MaximalSpectrum R) → ShortComplex (ModuleCat (Localization p.asIdeal.primeCompl)) :=
  fun p ↦ S.map (localizedModuleFunctor p.asIdeal.primeCompl)
Sp_exact : ∀ (p : MaximalSpectrum R), (Sp p).ShortExact
projp : ∀ (p : MaximalSpectrum R), Projective (Sp p).X₂
⊢ (∀ (m : MaximalSpectrum R), HasProjectiveDimensionLT ((of R ↥f.ker).localizedModule m.asIdeal.primeCompl) (n + 1)) ↔
    ∀ (m : MaximalSpectrum R), HasProjectiveDimensionLT (M.localizedModule m.asIdeal.primeCompl) (n + 1 + 1)
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
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
⊢ (↾fun x ↦ ⟨⟨(QuotientGroup.map (↑N.toOpenSubgroup) N.toOpenSubgroup.1 (MonoidHom.id G) ⋯) ↑↑x, ⋯⟩, ⋯⟩) =
    𝟙
      { σ' //
        (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' := ⋯ }) }

Tactic:
by ext ⟨⟨⟨x⟩, hx⟩, hx'⟩; rfl

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
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✝
⊢ (↾fun x ↦ ⟨⟨(QuotientGroup.map (↑X✝.toOpenSubgroup) Z✝.toOpenSubgroup.1 (MonoidHom.id G) ⋯) ↑↑x, ⋯⟩, ⋯⟩) =
    (↾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, ⋯⟩, ⋯⟩

Tactic:
by ext ⟨⟨⟨x⟩, hx⟩, hx'⟩; rfl

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
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
⊢ ∃ a, (stabilizerHom Q P G) a = σ

Tactic:
let B' := FixedPoints.subalgebra A B

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
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.58) → [inst : Monoid G] → [inst_1 : MulSemiringAction G B] → [SMulCommClass G A B] → Subalgebra A B :=
  FixedPoints.subalgebra A B
⊢ ∃ a, (stabilizerHom Q P G) a = σ
Module: Mathlib.RingTheory.LocalRing.MaximalIdeal.Square

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
⊢ maximalIdeal R ^ 2 < maximalIdeal R ↔ ¬maximalIdeal R ^ 2 = maximalIdeal R

Tactic:
simp [lt_iff_le_and_ne, Ideal.pow_le_self]

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
k : ℕ
f : V⸨X⸩
n : ℤ
⊢ k.factorial • Ring.choose (n + ↑k) k • f.coeff (n + ↑k) = (descPochhammer ℤ k).smeval (n + ↑k) • f.coeff (n + ↑k)

Tactic:
Ring.descPochhammer_eq_factorial_smul_choose,

Goal state after:
R : Type u_1
inst✝² : Semiring R
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
k : ℕ
f : V⸨X⸩
n : ℤ
⊢ k.factorial • Ring.choose (n + ↑k) k • f.coeff (n + ↑k) = (k.factorial • Ring.choose (n + ↑k) k) • f.coeff (n + ↑k)
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x y : R⟦X⟧
⊢ (algebraMap R⟦X⟧ R⸨X⸩) x = (algebraMap R⟦X⟧ R⸨X⸩) y → ∃ c, ↑c * x = ↑c * y

Tactic:
rw [coe_algebraMap, ofPowerSeries_injective.eq_iff]

Goal state after:
R : Type u_1
inst✝ : CommRing R
x y : R⟦X⟧
⊢ x = y → ∃ c, ↑c * x = ↑c * y
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
⊢ Ideal.map (f.pullbackSnd g) (ker (f.pullbackFst g)) ≤ ker g

Tactic:
Ideal.map_le_iff_le_comap

Goal state after:
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
⊢ ker (f.pullbackFst g) ≤ Ideal.comap (f.pullbackSnd g) (ker g)