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

Goal state before:
pp: case h.zero
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
p : Ideal R
s : Finset R
hp : p ∈ (span ↑s).minimalPrimes
this : p.IsPrime
H :
  ∀ m < 0,
    ∀ {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
hn : s.card ≤ 0
⊢ p.height = 0

Tactic:
height_eq_zero_iff,

Goal state after:
case h.zero
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
p : Ideal R
s : Finset R
hp : p ∈ (span ↑s).minimalPrimes
this : p.IsPrime
H :
  ∀ m < 0,
    ∀ {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
hn : s.card ≤ 0
⊢ p ∈ minimalPrimes R
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
this : IsLocalRing.maximalIdeal R = I
⊢ I.IsMaximal

Tactic:
exact this ▸ (IsLocalRing.maximalIdeal.isMaximal R)

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

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

Tactic:
nontriviality R[X]
    refine (ringKrullDim_le_iff_isMaximal_height_le (ringKrullDim R + 1)).mpr fun M hM ↦ ?_
    rw [height_eq_height_add_one (M.under R) M, WithBot.coe_add, WithBot.coe_one]
    gcongr
    exact Ideal.height_le_ringKrullDim_of_ne_top Ideal.IsPrime.ne_top'

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

Goal state before:
pp: case pos
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
hb : supportDim R (QuotSMulTop x M) ≠ ⊥
⊢ ↑0 ≤ ↑((supportDim R (QuotSMulTop x M)).unbot hb) + 1

Tactic:
exact WithBot.coe_le_coe.mpr zero_le

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

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommRing R
inst✝⁷ : IsNoetherianRing R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsNoetherianRing S
inst✝³ : Algebra.HasGoingDown R S
p : Ideal R
inst✝² : p.IsPrime
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : P.LiesOver p
lp : LTSeries (PrimeSpectrum R)
hlp : RelSeries.last lp = { asIdeal := p, isPrime := ⋯ }
hlenp : ↑lp.length = p.height
lq : LTSeries (PrimeSpectrum (S ⧸ map (algebraMap R S) p))
hlq : RelSeries.last lq = { asIdeal := map (Quotient.mk (map (algebraMap R S) p)) P, isPrime := ⋯ }
hlenq : ↑lq.length = (map (Quotient.mk (map (algebraMap R S) p)) P).height
l' : LTSeries (PrimeSpectrum S) := lq.map (PrimeSpectrum.comap (Quotient.mk (map (algebraMap R S) p))) ⋯
this✝ : (RelSeries.head l').asIdeal.LiesOver (RelSeries.last lp).asIdeal
lp' : LTSeries (PrimeSpectrum S)
hlp'len : lp'.length = lp.length
hlp' : RelSeries.last lp' = { asIdeal := (RelSeries.head l').asIdeal, isPrime := ⋯ }
right✝ : List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.toList lp') = RelSeries.toList lp
this : (RelSeries.smash lp' l' hlp').length = lp.length + lq.length
⊢ p.height + (map (Quotient.mk (map (algebraMap R S) p)) P).height ≤ P.height

Tactic:
← hlenp,

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
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))) ⋯
this✝ : (RelSeries.head l').asIdeal.LiesOver (RelSeries.last lp).asIdeal
lp' : LTSeries (PrimeSpectrum S)
hlp'len : lp'.length = lp.length
hlp' : RelSeries.last lp' = { asIdeal := (RelSeries.head l').asIdeal, isPrime := ⋯ }
right✝ : List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.toList lp') = RelSeries.toList lp
this : (RelSeries.smash lp' l' hlp').length = lp.length + lq.length
⊢ ↑lp.length + (map (Quotient.mk (map (algebraMap R S) p)) P).height ≤ P.height
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: case refine_3
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
s : Finset (Submodule R M)
hs : s.inf id = N
hs' : ∀ ⦃J : Submodule R M⦄, J ∈ s → J.IsPrimary
⊢ (↑(Finset.image (fun t ↦ t.inf id)
          (Finset.image (fun J ↦ {I ∈ s | (I.colon Set.univ).radical = (J.colon Set.univ).radical}) s))).Pairwise
    ((fun x1 x2 ↦ x1 ≠ x2) on fun J ↦ (J.colon Set.univ).radical)

Tactic:
intro I hI J hJ hIJ
    simp only [Finset.coe_image, Set.mem_image, Finset.mem_coe, exists_exists_and_eq_and] at hI hJ
    obtain ⟨I', hI', hI⟩ := hI
    obtain ⟨J', hJ', hJ⟩ := hJ
    simp only [Function.onFun, ne_eq]
    contrapose hIJ
    suffices (I'.colon Set.univ).radical = (J'.colon Set.univ).radical by
      rw [← hI, ← hJ, this]
    · rw [← hI, colon_finsetInf,
        radical_finset_inf (i := I') (by simp [hI']) (by simp), id_eq] at hIJ
      rw [hIJ, ← hJ, colon_finsetInf,
        radical_finset_inf (i := J') (by simp [hJ']) (by simp), id_eq]

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
N N' : OpenNormalSubgroup G
f : N ⟶ N'
x : { g // Ideal.under (↥(B' ↥↑N.toOpenSubgroup)) Q = g • Ideal.under (↥(B' ↥↑N.toOpenSubgroup)) P }
⊢ Ideal.under (↥(B' ↥↑N'.toOpenSubgroup)) Q =
    (QuotientGroup.map (↑N.toOpenSubgroup) N'.toOpenSubgroup.1 (MonoidHom.id G) ⋯) ↑x •
      Ideal.under (↥(B' ↥↑N'.toOpenSubgroup)) P

Tactic:
have h : B' N'.1.1 ≤ B' N.1.1 := fun x hx n ↦ hx ⟨_, f.le n.2⟩

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
N N' : OpenNormalSubgroup G
f : N ⟶ N'
x : { g // Ideal.under (↥(B' ↥↑N.toOpenSubgroup)) Q = g • Ideal.under (↥(B' ↥↑N.toOpenSubgroup)) P }
h : B' ↥↑N'.toOpenSubgroup ≤ B' ↥↑N.toOpenSubgroup
⊢ Ideal.under (↥(B' ↥↑N'.toOpenSubgroup)) Q =
    (QuotientGroup.map (↑N.toOpenSubgroup) N'.toOpenSubgroup.1 (MonoidHom.id G) ⋯) ↑x •
      Ideal.under (↥(B' ↥↑N'.toOpenSubgroup)) P
Module: Mathlib.RingTheory.LocalIso

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
ι : Type u_3
f : ι → S
h✝ : Ideal.span (Set.range f) = ⊤
T : ι → Type u_4
inst✝⁵ : (i : ι) → CommSemiring (T i)
inst✝⁴ : (i : ι) → Algebra R (T i)
inst✝³ : (i : ι) → Algebra S (T i)
inst✝² : ∀ (i : ι), IsScalarTower R S (T i)
inst✝¹ : ∀ (i : ι), IsLocalization.Away (f i) (T i)
inst✝ : ∀ (i : ι), IsLocalIso R (T i)
q : Ideal S
hq : q.IsPrime
i : ι
hi : f i ∉ q
q' : PrimeSpectrum (T i)
hq' : PrimeSpectrum.comap (algebraMap S (T i)) q' = { asIdeal := q, isPrime := hq }
g' : T i
hg' : g' ∉ q'.asIdeal
h : IsStandardOpenImmersion R (Localization.Away g')
n : ℕ
g : S
hg : g' * (algebraMap S (T i)) (f i) ^ n = (algebraMap S (T i)) g
⊢ IsStandardOpenImmersion R (Localization.Away (g * f i))

Tactic:
have : IsLocalization.Away g' (Localization.Away (algebraMap S (T i) g)) := by
      rw [← hg]
      exact .of_associated
        (associated_mul_unit_right _ _ ((IsLocalization.Away.algebraMap_isUnit (f i)).pow n)).symm
    let e₁ : Localization.Away (algebraMap S (T i) g) ≃ₐ[S] Localization.Away (g * f i) :=
      IsLocalization.algEquiv (.powers (g * f i)) _ _
    let e₂ : Localization.Away g' ≃ₐ[R] Localization.Away (g * f i) :=
      ((IsLocalization.algEquiv (.powers g') _ _).restrictScalars R).trans (e₁.restrictScalars R)
    exact .of_algEquiv e₂

Goal state after:
Module: Mathlib.RingTheory.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)}) = ⊤
⊢ ⊤ ≤ Ideal.span (Set.range fun i ↦ (algebraMap S T) ↑i.fst * ↑i.snd)

Tactic:
← Ideal.top_mul ⊤,

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)}) = ⊤
⊢ ⊤ * ⊤ ≤ Ideal.span (Set.range fun i ↦ (algebraMap S T) ↑i.fst * ↑i.snd)
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
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u'
inst✝⁹ : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)
inst✝⁸ : ∀ (P : Ideal R) [inst : P.IsMaximal], Small.{v', u'} (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 v'
inst✝⁵ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommGroup (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)
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
H : ∀ (I : Ideal R) (x : I.IsMaximal), Injective (Rₚ I) (Mₚ I)
P : Ideal R
hP : P.IsMaximal
m : Mₚ P
r : R
s : ↥P.primeCompl
⊢ ↑s •
      (IsLocalizedModule.linearEquiv P.primeCompl (f P) (LocalizedModule.mkLinearMap P.primeCompl M))
        (IsLocalization.mk' (Rₚ P) r s • m) =
    ↑s •
      (IsLocalization.map (Localization.AtPrime P) (RingHom.id R) ⋯) (IsLocalization.mk' (Rₚ P) r s) •
        (IsLocalizedModule.linearEquiv P.primeCompl (f P) (LocalizedModule.mkLinearMap P.primeCompl M)) m

Tactic:
simp only [← map_smul, ← smul_assoc, IsLocalization.smul_mk'_self, algebraMap_smul,
      IsLocalization.map_id_mk']

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
tfae_1_to_2 : ¬IsLocalRing R → Nontrivial (MaximalSpectrum R)
m₁ : Ideal R
hm₁ : m₁.IsMaximal
m₂ : Ideal R
hm₂ : m₂.IsMaximal
h : { asIdeal := m₁, isMaximal := hm₁ } ≠ { asIdeal := m₂, isMaximal := hm₂ }
x✝ : m₁ = m₂
⊢ { asIdeal := m₁, isMaximal := hm₁ } = { asIdeal := m₂, isMaximal := hm₂ }

Tactic:
by congr

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommRing R
z : R⸨X⸩
h : order z < 0
⊢ (single ↑(order z).natAbs) 1 = (single (-order z)) 1

Tactic:
Int.ofNat_natAbs_of_nonpos

Goal state after:
case neg
R : Type u_1
inst✝ : CommRing R
z : R⸨X⸩
h : order z < 0
⊢ (single (-order z)) 1 = (single (-order z)) 1

case neg
R : Type u_1
inst✝ : CommRing R
z : R⸨X⸩
h : order z < 0
⊢ order z ≤ 0
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case e'_2
K : Type u_2
inst✝ : Field K
P : K[X]
hP : ¬P = 0
span_ne_zero : Ideal.span {P} ≠ 0 ∧ Ideal.span {Polynomial.X} ≠ 0
span_ne_zero' : Ideal.span {↑P} ≠ 0 ∧ (idealX K).asIdeal ≠ 0
⊢ Multiset.count (Ideal.span {Polynomial.X}) (UniqueFactorizationMonoid.normalizedFactors (Ideal.span {P})) =
    Multiset.count Polynomial.X (UniqueFactorizationMonoid.normalizedFactors P)

pp: case e'_3
K : Type u_2
inst✝ : Field K
P : K[X]
hP : ¬P = 0
span_ne_zero : Ideal.span {P} ≠ 0 ∧ Ideal.span {Polynomial.X} ≠ 0
span_ne_zero' : Ideal.span {↑P} ≠ 0 ∧ (idealX K).asIdeal ≠ 0
⊢ Multiset.count (idealX K).asIdeal (UniqueFactorizationMonoid.normalizedFactors (Ideal.span {↑P})) =
    Multiset.count X (UniqueFactorizationMonoid.normalizedFactors ↑P)

pp: case neg.hI
K : Type u_2
inst✝ : Field K
P : K[X]
hP : ¬P = 0
span_ne_zero : Ideal.span {P} ≠ 0 ∧ Ideal.span {Polynomial.X} ≠ 0
span_ne_zero' : Ideal.span {↑P} ≠ 0 ∧ (idealX K).asIdeal ≠ 0
⊢ Ideal.span {↑P} ≠ 0

pp: case neg.hJ
K : Type u_2
inst✝ : Field K
P : K[X]
hP : ¬P = 0
span_ne_zero : Ideal.span {P} ≠ 0 ∧ Ideal.span {Polynomial.X} ≠ 0
span_ne_zero' : Ideal.span {↑P} ≠ 0 ∧ (idealX K).asIdeal ≠ 0
⊢ (idealX K).asIdeal.IsPrime

pp: case neg.hJ₀
K : Type u_2
inst✝ : Field K
P : K[X]
hP : ¬P = 0
span_ne_zero : Ideal.span {P} ≠ 0 ∧ Ideal.span {Polynomial.X} ≠ 0
span_ne_zero' : Ideal.span {↑P} ≠ 0 ∧ (idealX K).asIdeal ≠ 0
⊢ (idealX K).asIdeal ≠ ⊥

Tactic:
exacts [Ideal.count_span_normalizedFactors_eq_of_normUnit hP Polynomial.normUnit_X prime_X,
    Ideal.count_span_normalizedFactors_eq_of_normUnit (by simp [hP]) normUnit_X X_prime,
    span_ne_zero'.1, (idealX K).isPrime, span_ne_zero'.2]

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

Goal state before:
pp: case succ
σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
f : MvPolynomial σ R
k : ℕ
n_ih : (map (iterateFrobenius R p k)) ((expand (p ^ k)) f) = f ^ p ^ k
⊢ (map (iterateFrobenius R p (k + 1))) ((expand (p ^ (k + 1))) f) = f ^ p ^ (k + 1)

Tactic:
symm
    conv_lhs => rw [pow_succ, pow_mul, ← n_ih]
    simp_rw [← map_frobenius_expand p, pow_succ', add_comm k, iterateFrobenius_add,
      ← map_map, ← map_expand, ← expand_mul, iterateFrobenius_one]

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

Goal state before:
pp: case hig
n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : MvPolynomial n R
nontrivial : f.support.Nontrivial
d : n →₀ ℕ
hd : d ∈ f.support
i : n
hdi : d i = 1
disjoint : (↑f.support).PairwiseDisjoint Finsupp.support
isPrimitive : ∀ (r : R), (∀ (d : n →₀ ℕ), r ∣ coeff d f) → IsUnit r
hfd : coeff d f ≠ 0
d₀ : n →₀ ℕ := ⋯
φ : MvPolynomial n R := ⋯
ψ : MvPolynomial n R := ⋯
hf : f = φ * X i + ψ
hφ : φ * X i = (monomial d) (coeff d f)
hdψ : ∀ (k : n →₀ ℕ), coeff k ψ = if d = k then 0 else coeff k f
⊢ i ∉ ψ.vars

Tactic:
suffices ∀ x, d ≠ x → x ∈ f.support → i ∉ x.support by
      simpa [mem_vars_iff_mem_support, hdψ] using this
    exact fun x hxd hx hix ↦
      Finset.disjoint_iff_ne.mp (disjoint hd hx hxd) i (by simp [hdi]) _ hix rfl

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

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝ : CommRing R
c : n →₀ R
i : n
⊢ coeff (Finsupp.single i 1) (∑ a ∈ c.support, c a • X a) = c i

Tactic:
coeff_sum

Goal state after:
n : Type u_1
R : Type u_2
inst✝ : CommRing R
c : n →₀ R
i : n
⊢ ∑ x ∈ c.support, coeff (Finsupp.single i 1) (c x • X x) = c i
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
F : K⟦X⟧
η : (WithZero (Multiplicative ℤ))ˣ
⊢ ∃ P, (PowerSeries.idealX K).intValuation (F - ↑P) < ↑η

Tactic:
by_cases! h_neg : 1 < η

Goal state after:
case pos
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
η : (WithZero (Multiplicative ℤ))ˣ
h_neg : 1 < η
⊢ ∃ P, (PowerSeries.idealX K).intValuation (F - ↑P) < ↑η

case neg
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
η : (WithZero (Multiplicative ℤ))ˣ
h_neg : η ≤ 1
⊢ ∃ P, (PowerSeries.idealX K).intValuation (F - ↑P) < ↑η
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))) ≤ ↑(unzero ⋯) * ↑(Multiplicative.ofAdd (-1))
⊢ (PowerSeries.idealX K).intValuation (F - ↑((trunc (d + 1)) F)) < ↑η

Tactic:
coe_unzero,

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 (-1))
⊢ (PowerSeries.idealX K).intValuation (F - ↑((trunc (d + 1)) F)) < ↑η
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

Goal state before:
pp: case pos
σ : Type u_1
inst✝ : DecidableEq σ
t : Finset σ × σ
h1 : t.2 ∈ t.1
h2 : (t.1.erase t.2, t.2).2 ∈ (t.1.erase t.2, t.2).1
⊢ ((t.1.erase t.2, t.2).1.erase (t.1.erase t.2, t.2).2, (t.1.erase t.2, t.2).2) = t

pp: case neg
σ : Type u_1
inst✝ : DecidableEq σ
t : Finset σ × σ
h1 : t.2 ∈ t.1
h2 : (t.1.erase t.2, t.2).2 ∉ (t.1.erase t.2, t.2).1
⊢ (cons (t.1.erase t.2, t.2).2 (t.1.erase t.2, t.2).1 ⋯, (t.1.erase t.2, t.2).2) = t

pp: case pos
σ : Type u_1
inst✝ : DecidableEq σ
t : Finset σ × σ
h1 : t.2 ∉ t.1
h3 : (cons t.2 t.1 h1, t.2).2 ∈ (cons t.2 t.1 h1, t.2).1
⊢ ((cons t.2 t.1 h1, t.2).1.erase (cons t.2 t.1 h1, t.2).2, (cons t.2 t.1 h1, t.2).2) = t

pp: case neg
σ : Type u_1
inst✝ : DecidableEq σ
t : Finset σ × σ
h1 : t.2 ∉ t.1
h3 : (cons t.2 t.1 h1, t.2).2 ∉ (cons t.2 t.1 h1, t.2).1
⊢ (cons (cons t.2 t.1 h1, t.2).2 (cons t.2 t.1 h1, t.2).1 ⋯, (cons t.2 t.1 h1, t.2).2) = t

Tactic:
· simp at h2

Goal state after:
case neg
σ : Type u_1
inst✝ : DecidableEq σ
t : Finset σ × σ
h1 : t.2 ∈ t.1
h2 : (t.1.erase t.2, t.2).2 ∉ (t.1.erase t.2, t.2).1
⊢ (cons (t.1.erase t.2, t.2).2 (t.1.erase t.2, t.2).1 ⋯, (t.1.erase t.2, t.2).2) = t

case pos
σ : Type u_1
inst✝ : DecidableEq σ
t : Finset σ × σ
h1 : t.2 ∉ t.1
h3 : (cons t.2 t.1 h1, t.2).2 ∈ (cons t.2 t.1 h1, t.2).1
⊢ ((cons t.2 t.1 h1, t.2).1.erase (cons t.2 t.1 h1, t.2).2, (cons t.2 t.1 h1, t.2).2) = t

case neg
σ : Type u_1
inst✝ : DecidableEq σ
t : Finset σ × σ
h1 : t.2 ∉ t.1
h3 : (cons t.2 t.1 h1, t.2).2 ∉ (cons t.2 t.1 h1, t.2).1
⊢ (cons (cons t.2 t.1 h1, t.2).2 (cons t.2 t.1 h1, t.2).1 ⋯, (cons t.2 t.1 h1, t.2).2) = t
Module: Mathlib.RingTheory.NoetherNormalization

Goal state before:
pp: case refine_1
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v w : Fin (n + 1) →₀ ℕ
hv : v ∈ f.support
hw : w ∈ f.support
ne : v ≠ w
i : Fin (n + 1)
⊢ v i < up

Tactic:
exact lt_of_le_of_lt ((monomial_le_degreeOf i ‹_›).trans (degreeOf_le_totalDegree f i))
    (by lia)

Goal state after:
Module: Mathlib.RingTheory.NoetherNormalization

Goal state before:
pp: case refine_2
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v w : Fin (n + 1) →₀ ℕ
hv : v ∈ f.support
hw : w ∈ f.support
ne : v ≠ w
i : Fin (n + 1)
⊢ w i < up

Tactic:
exact lt_of_le_of_lt ((monomial_le_degreeOf i ‹_›).trans (degreeOf_le_totalDegree f i))
    (by lia)

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

Goal state before:
pp: case h.h₀
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH : ∀ m < n, 0 < m → (bind₁ fun k ↦ 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
⊢ ∀ b ∈ Finset.range n, b ≠ 0 → C ↑p ^ b * (bind₁ fun k ↦ 1) (xInTermsOfW p ℚ b) ^ p ^ (n - b) = 0

Tactic:
intro i hin hi0

Goal state after:
case h.h₀
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH : ∀ m < n, 0 < m → (bind₁ fun k ↦ 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
i : ℕ
hin : i ∈ Finset.range n
hi0 : i ≠ 0
⊢ C ↑p ^ i * (bind₁ fun k ↦ 1) (xInTermsOfW p ℚ i) ^ p ^ (n - i) = 0
Module: Mathlib.RingTheory.WittVector.StructurePolynomial

Goal state before:
pp: p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
inj : Function.Injective ⇑(Int.castRingHom ℚ)
⊢ constantCoeff ((map (Int.castRingHom ℚ)) Φ) = (Int.castRingHom ℚ) (constantCoeff Φ)

Tactic:
constantCoeff_map

Goal state after:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
inj : Function.Injective ⇑(Int.castRingHom ℚ)
⊢ (Int.castRingHom ℚ) (constantCoeff Φ) = (Int.castRingHom ℚ) (constantCoeff Φ)
Module: Mathlib.RingTheory.WittVector.MulP

Goal state before:
pp: case «1»
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
ih : ∀ (k : ℕ), (x * ↑n).coeff k = (aeval x.coeff) (wittMulN p n k)
k i : ℕ
⊢ Function.uncurry ![(x * ↑n).coeff, x.coeff] ((fun i ↦ i) ⟨1, ⋯⟩, i) =
    (aeval x.coeff) (Function.uncurry ![wittMulN p n, X] ((fun i ↦ i) ⟨1, ⋯⟩, i))

Tactic:
simp [Function.uncurry, Matrix.cons_val_one, aeval_X]

Goal state after:
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: 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 : ℕ
x : ModP O p
hx0 : x ≠ 0
hxy0 : x * 0 ≠ 0
⊢ x * 0 = 0

Tactic:
rw [mul_zero]

Goal state after: