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

Goal state before:
pp: case h.succ.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
p : Ideal R
s : Finset R
hp : p ∈ (span ↑s).minimalPrimes
this✝ : p.IsPrime
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
hn : s.card ≤ n + 1
this :
  ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (s : Finset R),
    p ∈ (span ↑s).minimalPrimes →
      p.IsPrime →
        ∀ (n : ℕ),
          (∀ 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) →
            s.card ≤ n + 1 → (∃ (x : IsLocalRing R), p = maximalIdeal R) → p.height ≤ ↑(n + 1)
hR : ¬∃ (x : IsLocalRing R), p = maximalIdeal R
⊢ p.height ≤ ↑(n + 1)

Tactic:
rw [← Localization.AtPrime.under_maximalIdeal (I := p)] at hp ⊢
        rw [IsLocalization.height_under p.primeCompl]
        rw [← Set.mem_preimage, ← IsLocalization.minimalPrimes_map p.primeCompl, map_span] at hp
        exact this _ (s.image (algebraMap R (Localization p.primeCompl))) (by simpa using hp)
          inferInstance _ H (Finset.card_image_le.trans hn) ⟨inferInstance, rfl⟩

Goal state after:
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits

Goal state before:
pp: P : ProfiniteGrp.{u}
U : Set ↑(limit P.diagram).toProfinite.toTop
s : Set ((j : OpenNormalSubgroup ↑P.toProfinite.toTop) → ↑(P.diagram.obj j).toProfinite.toTop)
hsO : IsOpen s
hsv : Subtype.val ⁻¹' s = U
spc : (j : OpenNormalSubgroup ↑P.toProfinite.toTop) → ↑(P.diagram.obj j).toProfinite.toTop
hspc : spc ∈ limitConePtAux P.diagram
uDefaultSpec : spc ∈ s
J : Finset (OpenNormalSubgroup ↑P.toProfinite.toTop)
fJ : (a : OpenNormalSubgroup ↑P.toProfinite.toTop) → Set ↑(P.diagram.obj a).toProfinite.toTop
hJ1 : ∀ a ∈ J, IsOpen (fJ a) ∧ spc a ∈ fJ a
hJ2 : (↑J).pi fJ ⊆ s
M : Subgroup ↑P.toProfinite.toTop := ⨅ j, ↑(↑j).toOpenSubgroup
hM : M.Normal
hMOpen : IsOpen ↑M
m : OpenNormalSubgroup ↑P.toProfinite.toTop := { toSubgroup := M, isOpen' := hMOpen, isNormal' := ⋯ }
origin : ↑P.toProfinite.toTop
horigin : (QuotientGroup.mk' M) origin = spc m
⊢ (U ∩ Set.range ⇑(Hom.hom P.toLimit)).Nonempty

Tactic:
use (toLimit P) origin

Goal state after:
case h
P : ProfiniteGrp.{u}
U : Set ↑(limit P.diagram).toProfinite.toTop
s : Set ((j : OpenNormalSubgroup ↑P.toProfinite.toTop) → ↑(P.diagram.obj j).toProfinite.toTop)
hsO : IsOpen s
hsv : Subtype.val ⁻¹' s = U
spc : (j : OpenNormalSubgroup ↑P.toProfinite.toTop) → ↑(P.diagram.obj j).toProfinite.toTop
hspc : spc ∈ limitConePtAux P.diagram
uDefaultSpec : spc ∈ s
J : Finset (OpenNormalSubgroup ↑P.toProfinite.toTop)
fJ : (a : OpenNormalSubgroup ↑P.toProfinite.toTop) → Set ↑(P.diagram.obj a).toProfinite.toTop
hJ1 : ∀ a ∈ J, IsOpen (fJ a) ∧ spc a ∈ fJ a
hJ2 : (↑J).pi fJ ⊆ s
M : Subgroup ↑P.toProfinite.toTop := ⋯
hM : M.Normal
hMOpen : IsOpen ↑M
m : OpenNormalSubgroup ↑P.toProfinite.toTop := ⋯
origin : ↑P.toProfinite.toTop
horigin : (QuotientGroup.mk' M) origin = spc m
⊢ (Hom.hom P.toLimit) origin ∈ U ∩ Set.range ⇑(Hom.hom P.toLimit)
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'
⊢ Set.SurjOn ⇑(Quotient.mk (map (algebraMap R S) p)) ↑P ↑s'

Tactic:
refine Set.SurjOn.mono subset_rfl hsP'sub fun x hx ↦ ?_

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'
x : S ⧸ map (algebraMap R S) p
hx : x ∈ ↑P'
⊢ x ∈ ⇑(Quotient.mk (map (algebraMap R S) p)) '' ↑P
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: case H
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)
IH :
  ∀ s_1 ∈ s,
    (s.erase s_1).inf id = N → ∃ t ⊆ s.erase s_1, t.inf id = N ∧ ∀ ⦃J : Submodule R M⦄, J ∈ t → ¬(t.erase J).inf id ≤ J
hs : s.inf id = N
⊢ ∃ t ⊆ s, t.inf id = N ∧ ∀ ⦃J : Submodule R M⦄, J ∈ t → ¬(t.erase J).inf id ≤ J

Tactic:
| H s IH =>

Goal state after:
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
I J I' : Submodule R M
hI' : I' ∈ s
hI : {I ∈ s | (I.colon Set.univ).radical = (I'.colon Set.univ).radical}.inf id = I
J' : Submodule R M
hJ' : J' ∈ s
hJ : {I ∈ s | (I.colon Set.univ).radical = (J'.colon Set.univ).radical}.inf id = J
hIJ : (I.colon Set.univ).radical = (J.colon Set.univ).radical
⊢ I = J

Tactic:
suffices (I'.colon Set.univ).radical = (J'.colon Set.univ).radical by
      rw [← hI, ← hJ, this]

Goal state after:
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
I J I' : Submodule R M
hI' : I' ∈ s
hI : {I ∈ s | (I.colon Set.univ).radical = (I'.colon Set.univ).radical}.inf id = I
J' : Submodule R M
hJ' : J' ∈ s
hJ : {I ∈ s | (I.colon Set.univ).radical = (J'.colon Set.univ).radical}.inf id = J
hIJ : (I.colon Set.univ).radical = (J.colon Set.univ).radical
⊢ (I'.colon Set.univ).radical = (J'.colon Set.univ).radical
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
ι : 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
this : { asIdeal := q, isPrime := hq } ∈ PrimeSpectrum.basicOpen (f i)
⊢ ∃ g ∉ q, IsStandardOpenImmersion R (Localization.Away g)

Tactic:
← SetLike.mem_coe,

Goal state after:
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
this : { asIdeal := q, isPrime := hq } ∈ ↑(PrimeSpectrum.basicOpen (f i))
⊢ ∃ g ∉ q, IsStandardOpenImmersion R (Localization.Away g)
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 : OpenNormalSubgroup G
⊢ (↾fun x ↦ ⟨(QuotientGroup.map (↑N.toOpenSubgroup) N.toOpenSubgroup.1 (MonoidHom.id G) ⋯) ↑x, ⋯⟩) =
    𝟙 { g // Ideal.under (↥(B' ↥↑N.toOpenSubgroup)) Q = g • Ideal.under (↥(B' ↥↑N.toOpenSubgroup)) P }

Tactic:
by ext ⟨⟨x⟩, 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
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
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⟩; rfl

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

Goal state before:
pp: case succ
R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
S : Submonoid R
this : Small.{v, u} (Localization S)
n : ℕ
ih : ∀ (M : ModuleCat R) [HasProjectiveDimensionLE M n], HasProjectiveDimensionLE (M.localizedModule S) n
M : ModuleCat R
inst✝ : HasProjectiveDimensionLE M (n + 1)
P : ModuleCat R
projective✝ : Projective P
f : P ⟶ M
epi✝ : Epi f
T : ShortComplex (ModuleCat R) := { X₁ := kernel f, X₂ := P, X₃ := M, f := kernel.ι f, g := f, zero := ⋯ }
T_exact : T.ShortExact
TS : ShortComplex (ModuleCat (Localization S)) := T.map (localizedModuleFunctor S)
TS_exact : TS.ShortExact
⊢ HasProjectiveDimensionLE (M.localizedModule S) (n + 1)

Tactic:
have : Projective TS.X₂ := (ModuleCat.localizedModuleFunctor.{v} S).projective_obj _

Goal state after:
case succ
R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
S : Submonoid R
this✝ : Small.{v, u} (Localization S)
n : ℕ
ih : ∀ (M : ModuleCat R) [HasProjectiveDimensionLE M n], HasProjectiveDimensionLE (M.localizedModule S) n
M : ModuleCat R
inst✝ : HasProjectiveDimensionLE M (n + 1)
P : ModuleCat R
projective✝ : Projective P
f : P ⟶ M
epi✝ : Epi f
T : ShortComplex (ModuleCat R) := { X₁ := kernel f, X₂ := P, X₃ := M, f := kernel.ι f, g := f, zero := ⋯ }
T_exact : T.ShortExact
TS : ShortComplex (ModuleCat (Localization S)) := T.map (localizedModuleFunctor S)
TS_exact : TS.ShortExact
this : Projective TS.X₂
⊢ HasProjectiveDimensionLE (M.localizedModule S) (n + 1)
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommRing R
z : R⸨X⸩
h : order z < 0
⊢ order z ≤ 0

Tactic:
exact h.le

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 (frobenius R p)) ((expand p) ((map (iterateFrobenius R p k)) ((expand (p ^ k)) f))) =
    (map (iterateFrobenius R p (k + 1))) ((expand (p ^ (k + 1))) f)

Tactic:
pow_succ',

Goal state after:
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 (frobenius R p)) ((expand p) ((map (iterateFrobenius R p k)) ((expand (p ^ k)) f))) =
    (map (iterateFrobenius R p (k + 1))) ((expand (p * p ^ k)) f)
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case refine_2
R : Type u_3
m : ℕ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i : ℕ
him : i < m
t : Finset (Fin m)
ht : t ∈ powersetCard (i + 1) univ
hne : t ≠ Iic ⟨i, him⟩
ht' : #t = #(Iic ⟨i, him⟩)
⊢ supDegree (⇑toLex) ((monomial (∑ j ∈ t, fun₀ | j => 1)) 1) <
    supDegree (⇑toLex) ((monomial (∑ j ≤ ⟨i, him⟩, fun₀ | j => 1)) 1)

Tactic:
simp_rw [← single_eq_monomial, supDegree_single_ne_zero _ one_ne_zero,
    ← Finsupp.indicator_eq_sum_single]

Goal state after:
case refine_2
R : Type u_3
m : ℕ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i : ℕ
him : i < m
t : Finset (Fin m)
ht : t ∈ powersetCard (i + 1) univ
hne : t ≠ Iic ⟨i, him⟩
ht' : #t = #(Iic ⟨i, him⟩)
⊢ toLex (Finsupp.indicator t fun x x_1 ↦ 1) < toLex (Finsupp.indicator (Iic ⟨i, him⟩) fun x x_1 ↦ 1)
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
S : Set (K⟮X⟯ × K⟮X⟯)
w✝ : Set K⟮X⟯
hT : w✝ ∈ nhds 0
pre_T : (fun x ↦ x.2 - x.1) ⁻¹' w✝ ⊆ S
d : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ
hd : {y | Valued.v.restrict (y - 0) < ↑d} ⊆ w✝
X : Set K⸨X⸩ := {f | Valued.v f < embedding ↑d}
X_def : X = {f | Valued.v f < embedding ↑d}
x : K⟮X⟯
hx : (restrict₀ (MonoidWithZeroHom.ofClass Valued.v)) x = ↑d
h : x = 0
⊢ False

Tactic:
simp only [h, map_zero] at hx

Goal state after:
K : Type u_2
inst✝ : Field K
S : Set (K⟮X⟯ × K⟮X⟯)
w✝ : Set K⟮X⟯
hT : w✝ ∈ nhds 0
pre_T : (fun x ↦ x.2 - x.1) ⁻¹' w✝ ⊆ S
d : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ
hd : {y | Valued.v.restrict (y - 0) < ↑d} ⊆ w✝
X : Set K⸨X⸩ := {f | Valued.v f < embedding ↑d}
X_def : X = {f | Valued.v f < embedding ↑d}
x : K⟮X⟯
h : x = 0
hx : 0 = ↑d
⊢ False
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case hf
K : Type u_2
inst✝ : Field K
⊢ ∀ (x : WithVal (polynomialValuationX K)), Valued.v ((LaurentSeriesPkg K).coe x) = Valued.v x

Tactic:
intro x
    rw [← WithVal.apply_ofVal, valuation_eq_LaurentSeries_valuation K]
    rfl

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
φ : MvPowerSeries σ R
hφ : φ ≠ 0
d : σ →₀ ℕ
hd : ↑(Finsupp.degree d) < p • φ.order
h : ∃ i, ¬p ∣ d i
⊢ (coeff d) ((expand p hp) φ) = 0

Tactic:
obtain ⟨i, hi⟩ := h
        exact coeff_expand_of_not_dvd p hp φ hi

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
a : adicCompletion K⟮X⟯ (idealX K)
this : ∀ (s : Set (adicCompletion K⟮X⟯ (idealX K))), s ∈ 𝓝 0 ↔ ∃ γ, {x | Valued.v.restrict x < ↑γ} ⊆ s
ha : a = 0
S : Set (WithZero (Multiplicative ℤ))
γ : WithZero (Multiplicative ℤ)
γ_ne_zero : γ ≠ 0
γ_le : Set.Iio γ ⊆ S
x : adicCompletion K⟮X⟯ (idealX K)
hx : Valued.v x = γ
h : x = 0
⊢ False

Tactic:
simp only [h, map_zero] at hx

Goal state after:
K : Type u_2
inst✝ : Field K
a : adicCompletion K⟮X⟯ (idealX K)
this : ∀ (s : Set (adicCompletion K⟮X⟯ (idealX K))), s ∈ 𝓝 0 ↔ ∃ γ, {x | Valued.v.restrict x < ↑γ} ⊆ s
ha : a = 0
S : Set (WithZero (Multiplicative ℤ))
γ : WithZero (Multiplicative ℤ)
γ_ne_zero : γ ≠ 0
γ_le : Set.Iio γ ⊆ S
x : adicCompletion K⟮X⟯ (idealX K)
h : x = 0
hx : 0 = γ
⊢ False
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

Goal state before:
pp: σ : Type u_1
inst✝¹ : Fintype σ
R : Type u_2
inst✝ : CommRing R
k : ℕ
h : 0 < k
hesymm :
  ↑k * esymm σ R k =
    (-1) ^ (k + 1) *
      (∑ x ∈ {a ∈ antidiagonal k | a.1 < k} with 0 < x.1, (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2 +
        ∑ x ∈ {a ∈ antidiagonal k | a.1 < k} with ¬0 < x.1, (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2)
sub_both_sides✝ :
  ↑k * esymm σ R k -
      (-1) ^ (k + 1) * ∑ a ∈ {a ∈ antidiagonal k | a.1 < k} with 0 < a.1, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2 =
    (-1) ^ (k + 1) * ∑ a ∈ {a ∈ antidiagonal k | a.1 < k} with ¬0 < a.1, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2
sub_both_sides :
  (-1) ^ (k + 1) * ↑k * esymm σ R k -
      ∑ a ∈ {a ∈ antidiagonal k | a.1 < k} with 0 < a.1, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2 =
    ∑ a ∈ antidiagonal k with a.1 < k ∧ ¬0 < a.1, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2
a : ℕ × ℕ
ha : a.1 + a.2 = k
left✝ : a.1 < k
ha0 : ¬0 < a.1
⊢ a = (0, k)

Tactic:
rw [← ha, Nat.eq_zero_of_not_pos ha0, zero_add, ← Nat.eq_zero_of_not_pos ha0]

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

Goal state before:
pp: case succ
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p : ℕ
hp : p ≠ 0
inst✝ : ExpChar R p
f : MvPowerSeries σ R
k : ℕ
n_ih : (map (iterateFrobenius R p k)) ((expand (p ^ k) ⋯) f) = f ^ p ^ k
⊢ (map (frobenius R p)) ((expand p hp) ((map (iterateFrobenius R p k)) ((expand (p ^ k) ⋯) f))) =
    (map (iterateFrobenius R p (k + 1))) ((expand (p ^ (k + 1)) ⋯) f)

Tactic:
pow_succ',

Goal state after:
case succ
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p : ℕ
hp : p ≠ 0
inst✝ : ExpChar R p
f : MvPowerSeries σ R
k : ℕ
n_ih : (map (iterateFrobenius R p k)) ((expand (p ^ k) ⋯) f) = f ^ p ^ k
⊢ (map (frobenius R p)) ((expand p hp) ((map (iterateFrobenius R p k)) ((expand (p ^ k) ⋯) f))) =
    (map (iterateFrobenius R p (k + 1))) ((expand (p * p ^ k) ⋯) f)
Module: Mathlib.RingTheory.WittVector.Frobenius

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH :
  ∀ m < n,
    X m ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p m) =
      (bind₁ (wittPolynomial p ℚ ∘ fun n ↦ n + 1)) (xInTermsOfW p ℚ m)
h1 : ↑p ^ n * ⅟↑p ^ n = 1
⊢ X n ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p n) =
    (∑ x ∈ range n, C (↑p ^ x) * X x ^ p ^ (n + 1 - x)) * C (⅟↑p ^ n) + C (↑p ^ n * ⅟↑p ^ n) * X n ^ p +
        C (↑p ^ (n + 1) * ⅟↑p ^ n) * X (n + 1) -
      (∑ x ∈ range n, C (↑p ^ x) * (bind₁ (wittPolynomial p ℚ ∘ fun n ↦ n + 1)) (xInTermsOfW p ℚ x) ^ p ^ (n - x)) *
        C (⅟↑p ^ n)

Tactic:
pow_succ',

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH :
  ∀ m < n,
    X m ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p m) =
      (bind₁ (wittPolynomial p ℚ ∘ fun n ↦ n + 1)) (xInTermsOfW p ℚ m)
h1 : ↑p ^ n * ⅟↑p ^ n = 1
⊢ X n ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p n) =
    (∑ x ∈ range n, C (↑p ^ x) * X x ^ p ^ (n + 1 - x)) * C (⅟↑p ^ n) + C (↑p ^ n * ⅟↑p ^ n) * X n ^ p +
        C (↑p * ↑p ^ n * ⅟↑p ^ n) * X (n + 1) -
      (∑ x ∈ range n, C (↑p ^ x) * (bind₁ (wittPolynomial p ℚ ∘ fun n ↦ n + 1)) (xInTermsOfW p ℚ x) ^ p ^ (n - x)) *
        C (⅟↑p ^ n)
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: case refine_1.le_succ_of_le
R : Type u_1
inst✝¹ : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
h : Function.Surjective ⇑(frobenius R p)
n : ℕ
x✝ : R
m k✝ : ℕ
hle : n ≤ k✝
xk x : R
hx : (frobenius R p) x = xk
⊢ R

Tactic:
use x

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
⊢ (C (↑p ^ i) *
            ∑ k ∈ range (p ^ (n - i)),
              (C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p i)) ^ (k + 1) *
                  (X i ^ p) ^ (p ^ (n - i) - (k + 1)) *
                ↑((p ^ (n - i)).choose (k + 1))) *
          C (⅟↑p ^ n) +
        C (↑p ^ i) * (X i ^ p) ^ p ^ (n - i) * C (⅟↑p ^ n) -
      C (↑p ^ i) * X i ^ p ^ (n - i + 1) * C (⅟↑p ^ n) =
    ∑ i_1 ∈ range (p ^ (n - i)),
      C ↑p *
        (MvPolynomial.map (Int.castRingHom ℚ))
          ((X i ^ p) ^ (p ^ (n - i) - (i_1 + 1)) * frobeniusPolyAux p i ^ (i_1 + 1) *
            C ↑((p ^ (n - i)).choose (i_1 + 1) / p ^ (n - i - v p (i_1 + 1)) * p ^ (i_1 - v p (i_1 + 1))))

Tactic:
pow_succ',

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
⊢ (C (↑p ^ i) *
            ∑ k ∈ range (p ^ (n - i)),
              (C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p i)) ^ (k + 1) *
                  (X i ^ p) ^ (p ^ (n - i) - (k + 1)) *
                ↑((p ^ (n - i)).choose (k + 1))) *
          C (⅟↑p ^ n) +
        C (↑p ^ i) * (X i ^ p) ^ p ^ (n - i) * C (⅟↑p ^ n) -
      C (↑p ^ i) * X i ^ (p * p ^ (n - i)) * C (⅟↑p ^ n) =
    ∑ i_1 ∈ range (p ^ (n - i)),
      C ↑p *
        (MvPolynomial.map (Int.castRingHom ℚ))
          ((X i ^ p) ^ (p ^ (n - i) - (i_1 + 1)) * frobeniusPolyAux p i ^ (i_1 + 1) *
            C ↑((p ^ (n - i)).choose (i_1 + 1) / p ^ (n - i - v p (i_1 + 1)) * p ^ (i_1 - v p (i_1 + 1))))
Module: Mathlib.RingTheory.WittVector.Truncated

Goal state before:
pp: p n : ℕ
R : Type u_1
inst✝ : CommRing R
x : TruncatedWittVector p n R
i : Fin n
⊢ x.out.coeff ↑i = coeff i x

Tactic:
rw [out]; dsimp only; rw [dif_pos i.is_lt, Fin.eta]

Goal state after:
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: case refine_2
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 : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f g : PreTilt O p
hf : f ≠ 0
hg : g ≠ 0
m n : ℕ
hm : (Perfection.coeff (ModP O p) p (max m n)) f ≠ 0
hn : (Perfection.coeff (ModP O p) p (max m n)) g ≠ 0
⊢ (coeff (max m n + 1)) g ^ p ≠ 0

Tactic:
coeff_pow_p g

Goal state after:
case refine_2
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 : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f g : PreTilt O p
hf : f ≠ 0
hg : g ≠ 0
m n : ℕ
hm : (Perfection.coeff (ModP O p) p (max m n)) f ≠ 0
hn : (Perfection.coeff (ModP O p) p (max m n)) g ≠ 0
⊢ (coeff (max m n)) g ≠ 0
Module: Mathlib.RingTheory.WittVector.TeichmullerSeries

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst✝² : CommRing R
inst✝¹ : CharP R p
inst✝ : PerfectRing R p
x : 𝕎 R
n : ℕ
⊢ x - ∑ i ≤ n, (teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ i) (x.coeff i)) * ↑p ^ i ∈ span {↑p ^ (n + 1)}

Tactic:
mem_span_p_pow_iff_le_coeff_eq_zero,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst✝² : CommRing R
inst✝¹ : CharP R p
inst✝ : PerfectRing R p
x : 𝕎 R
n : ℕ
⊢ ∀ m < n + 1, (x - ∑ i ≤ n, (teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ i) (x.coeff i)) * ↑p ^ i).coeff m = 0
Module: Mathlib.RingTheory.Polynomial.Hermite.Basic

Goal state before:
pp: n : ℕ
ih : ∀ {k : ℕ}, Odd (n + k) → (hermite n).coeff k = 0
k : ℕ
hnk : Odd (n + 1 + (k + 1))
⊢ n.succ + k.succ = n + k + 2

Tactic:
by rw [Nat.succ_add, Nat.add_succ]

Goal state after: