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

Goal state before:
pp: case mpr
A : Type u_1
inst✝ : Ring A
F : IdealFilter A
a : WithIdealFilter F
s : Set (WithIdealFilter F)
I : Ideal A
hI : I ∈ F
hIs : a +ᵥ idealSet I ⊆ s
⊢ s ∈ 𝓝 a

Tactic:
refine ((F.addGroupFilterBasis).nhds_hasBasis a).mem_iff.2 ?_

Goal state after:
case mpr
A : Type u_1
inst✝ : Ring A
F : IdealFilter A
a : WithIdealFilter F
s : Set (WithIdealFilter F)
I : Ideal A
hI : I ∈ F
hIs : a +ᵥ idealSet I ⊆ s
⊢ ∃ i ∈ F.addGroupFilterBasis, (fun y ↦ a + y) '' i ⊆ s
Module: Mathlib.RingTheory.KrullDimension.LocalRing

Goal state before:
pp: case refine_3
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 : R
hI : x ∈ I
hx : x ≠ 0
this : IsLocalRing.maximalIdeal R ≤ I
⊢ I.IsMaximal

Tactic:
have := Ideal.IsMaximal.eq_of_le (IsLocalRing.maximalIdeal.isMaximal R) hI_prime.ne_top this

Goal state after:
case refine_3
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 : R
hI : x ∈ I
hx : x ≠ 0
this✝ : IsLocalRing.maximalIdeal R ≤ I
this : IsLocalRing.maximalIdeal R = I
⊢ I.IsMaximal
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
n : ℕ
H :
  ∀ m < n + 1,
    ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (s : Finset R),
      p ∈ (span ↑s).minimalPrimes → s.card = m → p.height ≤ ↑m
w✝ : IsLocalRing R
this✝ : (maximalIdeal R).IsPrime
q : Ideal R
hq : q.IsPrime
hpq : q < maximalIdeal R
hq' : ∀ (q' : Ideal R), q'.IsPrime → q < q' → ¬q' < maximalIdeal R
x : R
s' : Finset R
hxs' : x ∉ s'
hxq : x ∉ q
hn : (insert x s').card ≤ n + 1
hp : maximalIdeal R ∈ (span ↑(insert x s')).minimalPrimes
this : maximalIdeal R ≤ (q ⊔ span {x}).radical
⊢ ↑s' ⊆ ↑(q ⊔ span {x}).radical

Tactic:
have := hp.le.trans this

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
n : ℕ
H :
  ∀ m < n + 1,
    ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (s : Finset R),
      p ∈ (span ↑s).minimalPrimes → s.card = m → p.height ≤ ↑m
w✝ : IsLocalRing R
this✝¹ : (maximalIdeal R).IsPrime
q : Ideal R
hq : q.IsPrime
hpq : q < maximalIdeal R
hq' : ∀ (q' : Ideal R), q'.IsPrime → q < q' → ¬q' < maximalIdeal R
x : R
s' : Finset R
hxs' : x ∉ s'
hxq : x ∉ q
hn : (insert x s').card ≤ n + 1
hp : maximalIdeal R ∈ (span ↑(insert x s')).minimalPrimes
this✝ : maximalIdeal R ≤ (q ⊔ span {x}).radical
this : span ↑(insert x s') ≤ (q ⊔ span {x}).radical
⊢ ↑s' ⊆ ↑(q ⊔ span {x}).radical
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

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

Tactic:
refine Ideal.height_le_card_of_mem_minimalPrimes_span_finset ?_

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'
this : Set.SurjOn ⇑(Quotient.mk I) ↑p ↑s
o : Finset R
hsubset : ↑o ⊆ ↑p
ho : Set.InjOn ⇑(Quotient.mk I) ↑o
himgo : Finset.image (⇑(Quotient.mk I)) o = s
hI : I.FG
t : Finset R := o ∪ ⋯.toFinset
⊢ p ∈ (span ↑t).minimalPrimes
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

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

Tactic:
Set.Finite.coe_toFinset,

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'
this : Set.SurjOn ⇑(Quotient.mk I) ↑p ↑s
o : Finset R
hsubset : ↑o ⊆ ↑p
ho : Set.InjOn ⇑(Quotient.mk I) ↑o
himgo : Finset.image (⇑(Quotient.mk I)) o = s
hI : I.FG
t : Finset R := o ∪ ⋯.toFinset
⊢ p ∈ (span (↑o ∪ Submodule.generators I)).minimalPrimes
Module: Mathlib.RingTheory.Spectrum.Prime.LTSeries

Goal state before:
pp: case succ
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
⊢ ∃ q,
    x ∈ (q.toFun 1).asIdeal ∧
      n + 1 = q.length ∧ RelSeries.head p = RelSeries.head q ∧ RelSeries.last p = RelSeries.last q

Tactic:
| succ n hn =>

Goal state after:
case succ
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
⊢ ∃ 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.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
p : Ideal R
inst✝² : p.IsPrime
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : P.LiesOver p
s : Finset R
hp : p ∈ (span ↑s).minimalPrimes
heq : ↑s.card = p.height
P' : Ideal (S ⧸ map (algebraMap R S) p) := map (Quotient.mk (map (algebraMap R S) p)) P
s' : Finset (S ⧸ map (algebraMap R S) p)
hP' : P' ∈ (span ↑s').minimalPrimes
heq' : ↑s'.card = P'.height
hsP'sub : ↑s' ⊆ ↑P'
this : Set.SurjOn ⇑(Quotient.mk (map (algebraMap R S) p)) ↑P ↑s'
o : Finset S
ho : ↑o ⊆ ↑P
hinj : Set.InjOn ⇑(Quotient.mk (map (algebraMap R S) p)) ↑o
himgo : Finset.image (⇑(Quotient.mk (map (algebraMap R S) p))) o = s'
t : Finset S := Finset.image (⇑(algebraMap R S)) s ∪ o
⊢ P.height ≤ ↑t.card

Tactic:
refine Ideal.height_le_card_of_mem_minimalPrimes_span_finset ?_

Goal state after:
R : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : IsNoetherianRing R
S : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsNoetherianRing S
p : Ideal R
inst✝² : p.IsPrime
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : P.LiesOver p
s : Finset R
hp : p ∈ (span ↑s).minimalPrimes
heq : ↑s.card = p.height
P' : Ideal (S ⧸ map (algebraMap R S) p) := map (Quotient.mk (map (algebraMap R S) p)) P
s' : Finset (S ⧸ map (algebraMap R S) p)
hP' : P' ∈ (span ↑s').minimalPrimes
heq' : ↑s'.card = P'.height
hsP'sub : ↑s' ⊆ ↑P'
this : Set.SurjOn ⇑(Quotient.mk (map (algebraMap R S) p)) ↑P ↑s'
o : Finset S
ho : ↑o ⊆ ↑P
hinj : Set.InjOn ⇑(Quotient.mk (map (algebraMap R S) p)) ↑o
himgo : Finset.image (⇑(Quotient.mk (map (algebraMap R S) p))) o = s'
t : Finset S := Finset.image (⇑(algebraMap R S)) s ∪ o
⊢ P ∈ (span ↑t).minimalPrimes
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
s₀ : Finset ↑N.associatedPrimes
hs₀ : IsLowerSet ↑s₀
q : Submodule R M
hqp : q.IsPrimary
p : ↑N.associatedPrimes
S : Submonoid R := ⨅ q ∈ s₀, (↑q).primeCompl
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
hp : p ∉ s₀
hq : ¬↑(q.colon Set.univ) ⊆ ⋃ r ∈ s₀, ↑↑r
y : R
hy1 : y ∈ ↑(q.colon Set.univ)
hy2 : y ∉ ⋃ r ∈ s₀, ↑↑r
⊢ ∀ (a : Ideal R) (b : a ∈ N.associatedPrimes), ⟨a, b⟩ ∈ s₀ → y ∉ a

Tactic:
intro r hrI hrs

Goal state after:
R : Type u_3
M : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
s₀ : Finset ↑N.associatedPrimes
hs₀ : IsLowerSet ↑s₀
q : Submodule R M
hqp : q.IsPrimary
p : ↑N.associatedPrimes
S : Submonoid R := ⨅ q ∈ s₀, (↑q).primeCompl
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
hp : p ∉ s₀
hq : ¬↑(q.colon Set.univ) ⊆ ⋃ r ∈ s₀, ↑↑r
y : R
hy1 : y ∈ ↑(q.colon Set.univ)
hy2 : y ∉ ⋃ r ∈ s₀, ↑↑r
r : Ideal R
hrI : r ∈ N.associatedPrimes
hrs : ⟨r, hrI⟩ ∈ s₀
⊢ y ∉ r
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: case neg
R : Type u_3
M : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
s₀ : Finset ↑N.associatedPrimes
hs₀ : IsLowerSet ↑s₀
q : Submodule R M
hqp : q.IsPrimary
p : ↑N.associatedPrimes
S : Submonoid R := ⨅ q ∈ s₀, (↑q).primeCompl
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
hp : p ∉ s₀
hq : ¬↑(q.colon Set.univ) ⊆ ⋃ r ∈ s₀, ↑↑r
y : R
hy1 : y ∈ ↑(q.colon Set.univ)
hy2 : y ∈ S
⊢ comap (mkLinearMap S M) (localized₀ S (mkLinearMap S M) q) = ⊤

Tactic:
rw [eq_top_iff, ← map_le_iff_le_comap, map_top]

Goal state after:
case neg
R : Type u_3
M : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
s₀ : Finset ↑N.associatedPrimes
hs₀ : IsLowerSet ↑s₀
q : Submodule R M
hqp : q.IsPrimary
p : ↑N.associatedPrimes
S : Submonoid R := ⨅ q ∈ s₀, (↑q).primeCompl
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
hp : p ∉ s₀
hq : ¬↑(q.colon Set.univ) ⊆ ⋃ r ∈ s₀, ↑↑r
y : R
hy1 : y ∈ ↑(q.colon Set.univ)
hy2 : y ∈ S
⊢ (mkLinearMap S M).range ≤ localized₀ S (mkLinearMap S M) q
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.63) → [inst : Monoid G] → [inst_1 : MulSemiringAction G B] → [SMulCommClass G A B] → Subalgebra A B :=
  FixedPoints.subalgebra A B
⊢ ∃ g, Q = g • P

Tactic:
let F : OpenNormalSubgroup G ⥤ Type _ :=
  { obj N := { g : G ⧸ N.1.1 // Q.under (B' N.1.1) = g • P.under (B' N.1.1) }
    map {N N'} f := ↾fun x ↦ ⟨(QuotientGroup.map _ _ (.id _) (leOfHom f)) x.1, by
      have h : B' N'.1.1 ≤ B' N.1.1 := fun x hx n ↦ hx ⟨_, f.le n.2⟩
      obtain ⟨x, hx⟩ := x
      obtain ⟨x, rfl⟩ := QuotientGroup.mk_surjective x
      simpa only [Ideal.comap_comap, Ideal.pointwise_smul_eq_comap, ← Ideal.comap_coe
        (F := RingEquiv _ _)] using! congr(Ideal.comap (Subalgebra.inclusion h).toRingHom $hx)⟩
    map_id N := by ext ⟨⟨x⟩, hx⟩; rfl
    map_comp f g := by ext ⟨⟨x⟩, hx⟩; rfl }

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 := ⋯ }
⊢ ∃ g, Q = g • P
Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
S : Submonoid R
M : ModuleCat R
aux : ∀ (n : ℕ), injectiveDimension M ≤ ↑n → injectiveDimension (M.localizedModule S) ≤ ↑n
⊢ injectiveDimension (M.localizedModule S) ≤ injectiveDimension M

Tactic:
refine le_of_forall_ge (fun N ↦ ?_)

Goal state after:
R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
S : Submonoid R
M : ModuleCat R
aux : ∀ (n : ℕ), injectiveDimension M ≤ ↑n → injectiveDimension (M.localizedModule S) ≤ ↑n
N : WithBot ℕ∞
⊢ injectiveDimension M ≤ N → injectiveDimension (M.localizedModule S) ≤ N
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
aux : ∀ (n : ℕ), projectiveDimension M ≤ ↑n → projectiveDimension (M.localizedModule S) ≤ ↑n
⊢ projectiveDimension (M.localizedModule S) ≤ projectiveDimension M

Tactic:
refine le_of_forall_ge (fun N ↦ ?_)

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : Small.{v, u} R
S : Submonoid R
M : ModuleCat R
aux : ∀ (n : ℕ), projectiveDimension M ≤ ↑n → projectiveDimension (M.localizedModule S) ≤ ↑n
N : WithBot ℕ∞
⊢ projectiveDimension M ≤ N → projectiveDimension (M.localizedModule S) ≤ N
Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
M : ModuleCat R
inst✝ : Module.Finite R ↑M
⊢ projectiveDimension M = ⨆ p, projectiveDimension (M.localizedModule p.asIdeal.primeCompl)

Tactic:
have aux (n : ℕ) : projectiveDimension M ≤ n ↔ ⨆ (p : MaximalSpectrum R), projectiveDimension
    (M.localizedModule p.1.primeCompl) ≤ n := by
    simp only [projectiveDimension_le_iff, iSup_le_iff]
    exact M.hasProjectiveDimensionLE_iff_forall_maximalSpectrum n
  refine eq_of_forall_ge_iff (fun N ↦ ?_)
  induction N with
  | bot =>
    simp only [le_bot_iff, projectiveDimension_eq_bot_iff, ModuleCat.isZero_iff_subsingleton,
      iSup_eq_bot, ModuleCat.localizedModule, ← Equiv.subsingleton_congr (equivShrink _)]
    refine ⟨fun h p ↦ LocalizedModule.instSubsingleton _, fun h ↦ ?_⟩
    apply Module.subsingleton_of_localization_maximal (R := R)
      (fun p ↦ LocalizedModule p.primeCompl M) (fun p ↦ LocalizedModule.mkLinearMap p.primeCompl M)
    intro p hp
    exact h ⟨p, hp⟩
  | coe N =>
    induction N with
    | top => simp
    | coe n => simpa using aux n

Goal state after:
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)
s' : S
hs : (Ideal.Quotient.mk P) s' = ((Ideal.Quotient.mk P) ↑s)⁻¹
⊢ ∃ a,
    (Ideal.Quotient.mk (Ideal.map (algebraMap S Sₚ) P)) ((algebraMap S Sₚ) a) =
      (Ideal.Quotient.mk (Ideal.map (algebraMap S Sₚ) P)) (mk' Sₚ x s)

Tactic:
use x * s'

Goal state after:
case h
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)
s' : S
hs : (Ideal.Quotient.mk P) s' = ((Ideal.Quotient.mk P) ↑s)⁻¹
⊢ (Ideal.Quotient.mk (Ideal.map (algebraMap S Sₚ) P)) ((algebraMap S Sₚ) (x * s')) =
    (Ideal.Quotient.mk (Ideal.map (algebraMap S Sₚ) P)) (mk' Sₚ x s)
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case h
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
η : (WithZero (Multiplicative ℤ))ˣ
h_neg : Multiplicative.toAdd (unzero ⋯) ≤ 0
d : ℕ
hd : Multiplicative.toAdd (unzero ⋯) = -↑d
this : Valued.v ((ofPowerSeries ℤ K) (F - ↑((trunc (d + 1)) F))) ≤ ↑(Multiplicative.ofAdd (-↑d + -1))
⊢ (PowerSeries.idealX K).intValuation (F - ↑((trunc (d + 1)) F)) < ↑η

Tactic:
ofAdd_add,

Goal state after:
case h
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
η : (WithZero (Multiplicative ℤ))ˣ
h_neg : Multiplicative.toAdd (unzero ⋯) ≤ 0
d : ℕ
hd : Multiplicative.toAdd (unzero ⋯) = -↑d
this :
  Valued.v ((ofPowerSeries ℤ K) (F - ↑((trunc (d + 1)) F))) ≤ ↑(Multiplicative.ofAdd (-↑d) * Multiplicative.ofAdd (-1))
⊢ (PowerSeries.idealX K).intValuation (F - ↑((trunc (d + 1)) F)) < ↑η
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
k : ℕ
⊢ ↑k * ∑ t ∈ powersetCard k univ, ∏ i ∈ t, X i = (-1) ^ k * ∑ x ∈ powersetCard k univ, (-1) ^ k * ↑k * ∏ i ∈ x, X i

Tactic:
← mul_sum,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
k : ℕ
⊢ ↑k * ∑ t ∈ powersetCard k univ, ∏ i ∈ t, X i = (-1) ^ k * ((-1) ^ k * ↑k * ∑ i ∈ powersetCard k univ, ∏ i ∈ i, X i)
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case mul_X
R : Type u_3
n m : ℕ
inst✝ : CommRing R
h : m ≤ n
p : MvPolynomial (Fin m) R
i : Fin m
hp : (esymmAlgHom (Fin m) R m) p ∈ (esymmAlgHom (Fin m) R n).range
⊢ (esymmAlgHom (Fin m) R m) (p * X i) ∈ (esymmAlgHom (Fin m) R n).range

Tactic:
| mul_X p i hp =>

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Expand

Goal state before:
pp: case neg
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPolynomial σ R
n : σ →₀ ℕ
h : ∃ i, ¬p ∣ n i
⊢ (coeff n) ((expand p hp) ↑φ) = MvPolynomial.coeff n ((MvPolynomial.expand p) φ)

Tactic:
obtain ⟨i, hi⟩ := h
    rw [coeff_expand_of_not_dvd p hp _ hi, MvPolynomial.coeff_expand_of_not_dvd _ hi]

Goal state after:
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝ : CommRing R
n i : ℕ
⊢ (monomial (single i (p ^ (n - i)))) (↑p ^ i) = C (↑p ^ i) * X i ^ p ^ (n - i)

Tactic:
rw [monomial_eq, Finsupp.prod_single_index]

Goal state after:
p : ℕ
R : Type u_1
inst✝ : CommRing R
n i : ℕ
⊢ X i ^ 0 = 1
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
n i : ℕ
a✝ : i ∈ range (n + 1)
⊢ (if single i (p ^ (n - i)) = 0 then ↑p ^ i else 0) = 0

Tactic:
rw [if_neg]

Goal state after:
case hnc
p : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
n i : ℕ
a✝ : i ∈ range (n + 1)
⊢ ¬single i (p ^ (n - i)) = 0
Module: Mathlib.RingTheory.Teichmuller

Goal state before:
pp: case succ
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 + 1 + 1) ≡ x.teichmullerAux (m + 1) [SMOD I ^ (m + 1)]

Tactic:
rw [teichmullerAux, pow_succ' p, pow_mul]

Goal state after:
case succ
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 : ℕ
⊢ (Quotient.out ((coeff (R ⧸ I) p (m + 1)) x) ^ p) ^ p ^ m ≡ x.teichmullerAux (m + 1) [SMOD I ^ (m + 1)]
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
inst✝ : IsAdicComplete I R
x y : Perfection (R ⧸ I) p
n : ℕ
⊢ ∃ z,
    (Ideal.Quotient.mk I) z = (coeff (R ⧸ I) p n) (x * y) ∧
      z ^ p ^ n ≡ x.teichmullerFun * y.teichmullerFun [SMOD I ^ (n + 1)]

Tactic:
refine ⟨(coeff _ p n x).out * (coeff _ p n y).out, by simp, ?_⟩

Goal state after:
p : ℕ
inst✝³ : Fact (Nat.Prime p)
R : Type u_1
inst✝² : CommRing R
I : Ideal R
inst✝¹ : CharP (R ⧸ I) p
inst✝ : IsAdicComplete I R
x y : Perfection (R ⧸ I) p
n : ℕ
⊢ (Quotient.out ((coeff (R ⧸ I) p n) x) * Quotient.out ((coeff (R ⧸ I) p n) y)) ^ p ^ n ≡
    x.teichmullerFun * y.teichmullerFun [SMOD I ^ (n + 1)]
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
x✝ : Perfection R p
⊢ (pthRoot R p) x✝ = ↑(frobeniusEquiv (Perfection R p) p).symm x✝

Tactic:
simpa [RingEquiv.eq_symm_apply] using ext <| coeffMonoidHom_pow_p' _

Goal state after:
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: p : ℕ
inst✝³ : Fact (Nat.Prime p)
R : Type u₁
inst✝² : CommSemiring R
inst✝¹ : CharP R p
inst✝ : PerfectRing R p
f : ℕ → R
hf : ∀ (n : ℕ), f (n + 1) ^ p = f n
n✝ n : ℕ
ih : (⇑(frobeniusEquiv R p).symm)^[n] (f 0) = f n
⊢ (⇑(frobeniusEquiv R p).symm)^[n.succ] (f 0) ^ p = f n.succ ^ p

Tactic:
rw [Function.iterate_succ_apply', frobeniusEquiv_symm_pow_p, ih, hf]

Goal state after:
Module: Mathlib.RingTheory.WittVector.MulP

Goal state before:
pp: p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
x : 𝕎 R
k : ℕ
⊢ (x * ↑n).coeff k = (aeval x.coeff) (wittMulN p n k)

Tactic:
induction n generalizing k with

Goal state after:
Module: Mathlib.RingTheory.WittVector.IsPoly

Goal state before:
pp: p : ℕ
R S : Type u
idx : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
⊢ ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x y : 𝕎 R), (x + y).coeff = fun n ↦ peval (wittAdd p n) ![x.coeff, y.coeff]

Tactic:
by intros; ext; exact add_coeff _ _ _

Goal state after:
Module: Mathlib.RingTheory.WittVector.Identities

Goal state before:
pp: case succ.succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
ih : ∀ {m : ℕ}, m < n → (x * ↑p ^ n).coeff m = 0
m' : ℕ
h : m' + 1 < n + 1
⊢ (x * ↑p ^ n * ↑p).coeff (m' + 1) = 0

Tactic:
| succ m' =>

Goal state after:
Module: Mathlib.RingTheory.WittVector.Identities

Goal state before:
pp: case succ.succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
ih : ∀ {m : ℕ}, m < n → ((⇑verschiebung)^[n] x).coeff m = 0
m' : ℕ
h : m' + 1 < n + 1
⊢ (verschiebung ((⇑verschiebung)^[n] x)).coeff (m' + 1) = 0

Tactic:
| succ m' =>

Goal state after:
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: case neg
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
hp : Fact (Nat.Prime p)
r : O
hx : v ↑p ^ (1 / ↑p) < v ((algebraMap O K) r)
s : O
hy : v ↑p ^ (1 / ↑p) < v ((algebraMap O K) s)
h1p : 0 < 1 / ↑p
hvp : 0 < v ↑p
⊢ v ↑p ^ 1 ≤ v ↑p ^ (1 / ↑p) * v ↑p ^ (1 / ↑p)

Tactic:
← rpow_add (ne_of_gt hvp)

Goal state after:
case neg
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
hp : Fact (Nat.Prime p)
r : O
hx : v ↑p ^ (1 / ↑p) < v ((algebraMap O K) r)
s : O
hy : v ↑p ^ (1 / ↑p) < v ((algebraMap O K) s)
h1p : 0 < 1 / ↑p
hvp : 0 < v ↑p
⊢ v ↑p ^ 1 ≤ v ↑p ^ (1 / ↑p + 1 / ↑p)