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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
t : Finset (Submodule R M)
ht : N.IsMinimalPrimaryDecomposition t
⊢ (fun J ↦ (J.colon Set.univ).radical) '' ↑t = N.associatedPrimes

Tactic:
replace h x : radical (N.colon {x}) = (t.filter (x ∉ ·)).inf fun q ↦ radical (q.colon .univ) := by
    simp_rw [← ht.inf_eq, colon_finsetInf, ← radicalInfTopHom_apply, map_finset_inf,
      Function.comp_def, radicalInfTopHom_apply, id_eq]
    rw [Finset.inf_congr rfl (fun q hq ↦ (ht.primary hq).radical_colon_singleton_eq_ite x),
      Finset.inf_ite, Finset.inf_top, top_inf_eq]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
t : Finset (Submodule R M)
ht : N.IsMinimalPrimaryDecomposition t
h : ∀ (x : M), (N.colon {x}).radical = {x_1 ∈ t | x ∉ x_1}.inf fun q ↦ (q.colon Set.univ).radical
⊢ (fun J ↦ (J.colon Set.univ).radical) '' ↑t = N.associatedPrimes
Module: Mathlib.RingTheory.LittleWedderburn

Goal state before:
pp: D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
hD : InductionHyp D
val✝ : Fintype D
Z : Subring D := Subring.center D
hZ : Z ≠ ⊤
this✝ : Field ↥Z := hD.field ⋯
q : ℕ := card ↥Z
card_Z : q = card ↥Z
hq : 1 < q
n : ℕ := finrank (↥Z) D
card_D : card D = q ^ n
h1qn : 1 ≤ q ^ n
Φₙ : ℤ[X] := cyclotomic n ℤ
key : ↑q - 1 + ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card) = ↑q ^ n - 1
this : eval (↑q) Φₙ ∣ ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card)
contra : eval (↑q) Φₙ ∣ ↑q - 1
⊢ False

Tactic:
refine (Nat.le_of_dvd ?_ ?_).not_gt (sub_one_lt_natAbs_cyclotomic_eval (n := n) ?_ hq.ne')

Goal state after:
case refine_1
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
hD : InductionHyp D
val✝ : Fintype D
Z : Subring D := Subring.center D
hZ : Z ≠ ⊤
this✝ : Field ↥Z := hD.field ⋯
q : ℕ := card ↥Z
card_Z : q = card ↥Z
hq : 1 < q
n : ℕ := finrank (↥Z) D
card_D : card D = q ^ n
h1qn : 1 ≤ q ^ n
Φₙ : ℤ[X] := cyclotomic n ℤ
key : ↑q - 1 + ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card) = ↑q ^ n - 1
this : eval (↑q) Φₙ ∣ ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card)
contra : eval (↑q) Φₙ ∣ ↑q - 1
⊢ 0 < q - 1

case refine_2
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
hD : InductionHyp D
val✝ : Fintype D
Z : Subring D := Subring.center D
hZ : Z ≠ ⊤
this✝ : Field ↥Z := hD.field ⋯
q : ℕ := card ↥Z
card_Z : q = card ↥Z
hq : 1 < q
n : ℕ := finrank (↥Z) D
card_D : card D = q ^ n
h1qn : 1 ≤ q ^ n
Φₙ : ℤ[X] := cyclotomic n ℤ
key : ↑q - 1 + ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card) = ↑q ^ n - 1
this : eval (↑q) Φₙ ∣ ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card)
contra : eval (↑q) Φₙ ∣ ↑q - 1
⊢ (eval (↑q) (cyclotomic n ℤ)).natAbs ∣ q - 1

case refine_3
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
hD : InductionHyp D
val✝ : Fintype D
Z : Subring D := Subring.center D
hZ : Z ≠ ⊤
this✝ : Field ↥Z := hD.field ⋯
q : ℕ := card ↥Z
card_Z : q = card ↥Z
hq : 1 < q
n : ℕ := finrank (↥Z) D
card_D : card D = q ^ n
h1qn : 1 ≤ q ^ n
Φₙ : ℤ[X] := cyclotomic n ℤ
key : ↑q - 1 + ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card) = ↑q ^ n - 1
this : eval (↑q) Φₙ ∣ ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card)
contra : eval (↑q) Φₙ ∣ ↑q - 1
⊢ 1 < n
Module: Mathlib.RingTheory.LittleWedderburn

Goal state before:
pp: n : ℕ
IH : ∀ m < n, ∀ (D : Type u_1) [inst : DivisionRing D] [Finite D] (val : Fintype D), card D = m → Subring.center D = ⊤
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
val✝ : Fintype D
hn : card D = n
R : Subring D
hR : R < ⊤
x y : D
hx : x ∈ R
hy : y ∈ R
this : ⟨y, hy⟩ ∈ Subring.center ↥R
⊢ x * y = y * x

Tactic:
Subring.mem_center_iff

Goal state after:
n : ℕ
IH : ∀ m < n, ∀ (D : Type u_1) [inst : DivisionRing D] [Finite D] (val : Fintype D), card D = m → Subring.center D = ⊤
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
val✝ : Fintype D
hn : card D = n
R : Subring D
hR : R < ⊤
x y : D
hx : x ∈ R
hy : y ∈ R
this : ∀ (g : ↥R), g * ⟨y, hy⟩ = ⟨y, hy⟩ * g
⊢ x * y = y * x
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
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
⊢ ∃ g ∉ q, IsStandardOpenImmersion R (Localization.Away g)

Tactic:
refine ⟨g * (f i), ?_, ?_⟩

Goal state after:
case refine_1
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
⊢ g * f i ∉ q

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))
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
S : Submonoid R
inst✝¹¹ : Small.{v, u} R
inst✝¹⁰ : IsNoetherianRing R
Rₛ : Type u'
inst✝⁹ : Small.{v', u'} Rₛ
inst✝⁸ : CommRing Rₛ
inst✝⁷ : Algebra R Rₛ
Mₛ : Type v'
inst✝⁶ : AddCommGroup Mₛ
inst✝⁵ : Module R Mₛ
inst✝⁴ : Module Rₛ Mₛ
inst✝³ : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst✝² : IsLocalization S Rₛ
inst✝¹ : IsLocalizedModule S f
inst✝ : Injective R M
MB : ∀ (I : Ideal R), Function.Surjective ⇑(LinearMap.lcomp R M (Submodule.subtype I))
I : Submodule R R
g : ↥(Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I) →ₗ[Rₛ] Mₛ
this : FinitePresentation R ↥I
a : ↥S
g' : R →ₗ[R] M
e :
  ↑a • g =
    (mapExtendScalars S (Submodule.toLocalized' Rₛ S (Algebra.linearMap R Rₛ) I) f Rₛ)
      ((LinearMap.lcomp R M I.subtype) g', a).1
⊢ ↑R
      ((algebraMap R Rₛ) 1 •
        (LinearMap.lcomp Rₛ Mₛ (Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I).subtype)
          ((mapExtendScalars S (Algebra.linearMap R Rₛ) f Rₛ) g')) =
    ↑R
      ((mapExtendScalars S (Submodule.toLocalized' Rₛ S (Algebra.linearMap R Rₛ) I) f Rₛ)
        ((LinearMap.lcomp R M I.subtype) g'))

Tactic:
refine IsLocalizedModule.linearMap_ext S (I.toLocalized' Rₛ S (Algebra.linearMap R Rₛ)) f ?_

Goal state after:
R : Type u
inst✝¹⁴ : CommRing R
M : Type v
inst✝¹³ : AddCommGroup M
inst✝¹² : Module R M
S : Submonoid R
inst✝¹¹ : Small.{v, u} R
inst✝¹⁰ : IsNoetherianRing R
Rₛ : Type u'
inst✝⁹ : Small.{v', u'} Rₛ
inst✝⁸ : CommRing Rₛ
inst✝⁷ : Algebra R Rₛ
Mₛ : Type v'
inst✝⁶ : AddCommGroup Mₛ
inst✝⁵ : Module R Mₛ
inst✝⁴ : Module Rₛ Mₛ
inst✝³ : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst✝² : IsLocalization S Rₛ
inst✝¹ : IsLocalizedModule S f
inst✝ : Injective R M
MB : ∀ (I : Ideal R), Function.Surjective ⇑(LinearMap.lcomp R M (Submodule.subtype I))
I : Submodule R R
g : ↥(Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I) →ₗ[Rₛ] Mₛ
this : FinitePresentation R ↥I
a : ↥S
g' : R →ₗ[R] M
e :
  ↑a • g =
    (mapExtendScalars S (Submodule.toLocalized' Rₛ S (Algebra.linearMap R Rₛ) I) f Rₛ)
      ((LinearMap.lcomp R M I.subtype) g', a).1
⊢ ↑R
        ((algebraMap R Rₛ) 1 •
          (LinearMap.lcomp Rₛ Mₛ (Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I).subtype)
            ((mapExtendScalars S (Algebra.linearMap R Rₛ) f Rₛ) g')) ∘ₗ
      Submodule.toLocalized' Rₛ S (Algebra.linearMap R Rₛ) I =
    ↑R
        ((mapExtendScalars S (Submodule.toLocalized' Rₛ S (Algebra.linearMap R Rₛ) I) f Rₛ)
          ((LinearMap.lcomp R M I.subtype) g')) ∘ₗ
      Submodule.toLocalized' Rₛ S (Algebra.linearMap R Rₛ) I
Module: Mathlib.RingTheory.LocalIso

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

Tactic:
exact .of_isPushout S (Localization.Away x) _ _

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
N : OpenNormalSubgroup G
⊢ Finite ((stabilizerHomSurjectiveAuxFunctor P Q σ).obj N)

Tactic:
dsimp [stabilizerHomSurjectiveAuxFunctor]

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
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
⊢ Finite
    { σ' //
      { toRingHom := Ideal.quotientMap Q ↑(FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup).val ⋯, commutes' := ⋯ }.comp
          ↑((stabilizerHom (Ideal.under (↥(FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup)) Q) P (G ⧸ ↑N.toOpenSubgroup))
              σ') =
        (↑σ).comp
          { toRingHom := Ideal.quotientMap Q ↑(FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup).val ⋯, commutes' := ⋯ } }
Module: Mathlib.RingTheory.Localization.Pi

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
inst✝⁶ : (i : ι) → CommSemiring (R i)
S' : Type u_4
inst✝⁵ : CommSemiring S'
inst✝⁴ : Algebra ((i : ι) → R i) S'
M : Submonoid ((i : ι) → R i)
inst✝³ : ∀ (i : ι), Ring.KrullDimLE 0 (R i)
inst✝² : ∀ (i : ι), IsLocalRing (R i)
inst✝¹ : IsLocalization M S'
inst✝ : Finite ι
s : S'
S : ι → Type u_2 := fun i ↦ Localization (Submonoid.map (Pi.evalRingHom R i) M)
r : (i : ι) → R i
hr : (RingHom.pi fun i ↦ (algebraMap (R i) (S i)).comp (Pi.evalRingHom R i)) r = (lift ⋯) s
⊢ ∃ a, (algebraMap ((i : ι) → R i) S') a = s

Tactic:
refine ⟨r, (bijective_lift_piRingHom_algebraMap_comp_piEvalRingHom R S _ M).injective ?_⟩

Goal state after:
ι : Type u_1
R : ι → Type u_2
inst✝⁶ : (i : ι) → CommSemiring (R i)
S' : Type u_4
inst✝⁵ : CommSemiring S'
inst✝⁴ : Algebra ((i : ι) → R i) S'
M : Submonoid ((i : ι) → R i)
inst✝³ : ∀ (i : ι), Ring.KrullDimLE 0 (R i)
inst✝² : ∀ (i : ι), IsLocalRing (R i)
inst✝¹ : IsLocalization M S'
inst✝ : Finite ι
s : S'
S : ι → Type u_2 := fun i ↦ Localization (Submonoid.map (Pi.evalRingHom R i) M)
r : (i : ι) → R i
hr : (RingHom.pi fun i ↦ (algebraMap (R i) (S i)).comp (Pi.evalRingHom R i)) r = (lift ⋯) s
⊢ (lift ⋯) ((algebraMap ((i : ι) → R i) S') r) = (lift ⋯) s
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
uK : UniformSpace K
d : ℤ
S : Set (K × K)
hS : S ∈ uniformity K
⊢ ∃ v ∈ uniformity K⸨X⸩, ∀ y ∈ v, (y.1.coeff d, y.2.coeff d) ∈ S

Tactic:
let γ : (ℤᵐ⁰)ˣ := Units.mk0 (exp (-(d + 1))) coe_ne_zero

Goal state after:
K : Type u_2
inst✝ : Field K
uK : UniformSpace K
d : ℤ
S : Set (K × K)
hS : S ∈ uniformity K
γ : (WithZero (Multiplicative ℤ))ˣ := Units.mk0 (exp (-(d + 1))) ⋯
⊢ ∃ v ∈ uniformity K⸨X⸩, ∀ y ∈ v, (y.1.coeff d, y.2.coeff d) ∈ S
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_3
n : ℕ
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : Fintype τ
e : σ ≃ τ
⊢ (↑(renameSymmetricSubalgebra e)).comp (esymmAlgHom σ R n) = esymmAlgHom τ R n

Tactic:
ext i : 2
  simp_rw [AlgHom.comp_apply, esymmAlgHom, aeval_X, AlgEquiv.coe_toAlgHom,
    renameSymmetricSubalgebra_apply_coe, rename_esymm]

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

Goal state before:
pp: σ : Type u_1
inst✝ : DecidableEq σ
t : Finset σ × σ
⊢ pairMap σ (pairMap σ t) = t

Tactic:
rw [pairMap, pairMap]

Goal state after:
σ : Type u_1
inst✝ : DecidableEq σ
t : Finset σ × σ
⊢ (if h :
        (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).2 ∈
          (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).1 then
      ((if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).1.erase
          (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).2,
        (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).2)
    else
      (cons (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).2
          (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).1 h,
        (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).2)) =
    t
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: R : Type u_3
n m : ℕ
inst✝ : CommRing R
h : m ≤ n
p : ↥(symmetricSubalgebra (Fin m) R)
⊢ ∃ a, (esymmAlgHom (Fin m) R n) a = p

Tactic:
obtain ⟨q, rfl⟩ := (esymmAlgHom_fin_bijective R m).2 p

Goal state after:
R : Type u_3
n m : ℕ
inst✝ : CommRing R
h : m ≤ n
q : MvPolynomial (Fin m) R
⊢ ∃ a, (esymmAlgHom (Fin m) R n) a = (esymmAlgHom (Fin m) R m) q
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
⊢ (aeval fun i ↦ ⟨esymm (Fin m) R (↑i + 1), ⋯⟩) (X ⟨↑i, ⋯⟩) = (aeval fun i ↦ ⟨esymm (Fin m) R (↑i + 1), ⋯⟩) (X i)

Tactic:
aeval_X

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: σ : Type u_1
R : Type u_3
n : ℕ
inst✝¹ : Fintype σ
inst✝ : CommRing R
hn : Fintype.card σ = n
i : Fin n
⊢ ⟨esymm σ R (↑i + 1), ⋯⟩ = (aeval fun i ↦ ⟨esymm σ R (↑i + 1), ⋯⟩) (X i)

Tactic:
aeval_X

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

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
d : σ →₀ ℕ
r : R
⊢ (expand p hp) ((monomial d) r) = (monomial (p • d)) r

Tactic:
by
  rw [expand, substAlgHom_monomial (HasSubst.X_pow hp), monomial_eq', Finsupp.prod,
    Finsupp.prod_of_support_subset _ Finsupp.support_smul]
  · simp [pow_mul, algebraMap_apply, Algebra.algebraMap_self]
  · simp

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.MvPowerSeries.Restricted

Goal state before:
pp: R : Type u_1
inst✝ : NormedRing R
σ : Type u_2
c : σ → ℝ
n : σ →₀ ℕ
a : R
⊢ IsRestricted c ((monomial n) a)

Tactic:
by
  classical
  refine tendsto_nhds_of_eventually_eq (Set.Subsingleton.finite ?_)
  simp [Set.Subsingleton, coeff_monomial]

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

Tactic:
← map_frobenius_expand p hp,

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 ^ (k + 1)) ⋯) f)
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
x : RatFuncAdicCompl K
hx : x ∈ adicCompletionIntegers K⟮X⟯ (idealX K)
f : K⸨X⸩ := (ratfuncAdicComplRingEquiv K) x
hf : f = (ratfuncAdicComplRingEquiv K) x
hval : Valued.v f ≤ 1
F : K⟦X⟧
hF : (ofPowerSeries ℤ K) F = f
⊢ ∃ F, (LaurentSeriesRingEquiv K) ((ofPowerSeries ℤ K) F) = x

Tactic:
exact ⟨F, by rw [hF, hf, RingEquiv.symm_apply_apply]⟩

Goal state after:
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✝ : IsPrecomplete I R
x : Perfection (R ⧸ I) p
y : R
n : ℕ
h : (Ideal.Quotient.mk I) y = (coeff (R ⧸ I) p n) x
this : x.teichmullerAux (n + 1) ≡ ⋯.choose [SMOD I ^ (n + 1) • ⊤]
⊢ x.teichmullerFun ≡ y ^ p ^ n [SMOD I ^ (n + 1)]

Tactic:
rw [smul_eq_mul, Ideal.mul_top] at this

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✝ : IsPrecomplete I R
x : Perfection (R ⧸ I) p
y : R
n : ℕ
h : (Ideal.Quotient.mk I) y = (coeff (R ⧸ I) p n) x
this : x.teichmullerAux (n + 1) ≡ ⋯.choose [SMOD I ^ (n + 1)]
⊢ x.teichmullerFun ≡ y ^ p ^ n [SMOD I ^ (n + 1)]
Module: Mathlib.RingTheory.NoetherNormalization

Goal state before:
pp: k : Type u_1
inst✝ : Field k
n : ℕ
I : Ideal (MvPolynomial (Fin 0) k)
hi : I ≠ ⊤
a b : MvPolynomial (Fin 0) k
hab : a - b ∈ I
ne✝ : ¬a = b
eq : a - b = MvPolynomial.C (MvPolynomial.coeff 0 (a - b))
ne : MvPolynomial.coeff 0 (a - b) ≠ 0
c : k
left✝ : MvPolynomial.coeff 0 (a - b) * c = 1
eqr : c * MvPolynomial.coeff 0 (a - b) = 1
⊢ MvPolynomial.C 1 = 1

Tactic:
MvPolynomial.C_1

Goal state after:
k : Type u_1
inst✝ : Field k
n : ℕ
I : Ideal (MvPolynomial (Fin 0) k)
hi : I ≠ ⊤
a b : MvPolynomial (Fin 0) k
hab : a - b ∈ I
ne✝ : ¬a = b
eq : a - b = MvPolynomial.C (MvPolynomial.coeff 0 (a - b))
ne : MvPolynomial.coeff 0 (a - b) ≠ 0
c : k
left✝ : MvPolynomial.coeff 0 (a - b) * c = 1
eqr : c * MvPolynomial.coeff 0 (a - b) = 1
⊢ 1 = 1
Module: Mathlib.RingTheory.WittVector.MulP

Goal state before:
pp: case succ
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 : ℕ
⊢ (x * ↑n + x).coeff k = (aeval x.coeff) ((fun k ↦ (bind₁ (Function.uncurry ![wittMulN p n, X])) (wittAdd p k)) k)

Tactic:
aeval_bind₁,

Goal state after:
case succ
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 : ℕ
⊢ (x * ↑n + x).coeff k = (aeval fun i ↦ (aeval x.coeff) (Function.uncurry ![wittMulN p n, X] i)) (wittAdd p k)
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 : O
⊢ v ↑p < v ((algebraMap O K) x) ↔ (Ideal.Quotient.mk (Ideal.span {↑p})) x ≠ 0

Tactic:
lt_iff_not_ge,

Goal state after:
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 : O
⊢ ¬v ((algebraMap O K) x) ≤ v ↑p ↔ (Ideal.Quotient.mk (Ideal.span {↑p})) x ≠ 0
Module: Mathlib.RingTheory.WittVector.Frobenius

Goal state before:
pp: p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
⊢ ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x : 𝕎 R), x.frobeniusFun.coeff = fun n ↦ (aeval x.coeff) (frobeniusPoly p n)

Tactic:
intros; funext n; apply coeff_frobeniusFun

Goal state after: