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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
h : ringKrullDim R = 1
x : R
hx : x ≠ 0
⊢ IsLocalRing.maximalIdeal R ≤ (Ideal.span {x}).radical

Tactic:
Ideal.radical_eq_sInf

Goal state after:
case refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
h : ringKrullDim R = 1
x : R
hx : x ≠ 0
⊢ IsLocalRing.maximalIdeal R ≤ sInf {J | Ideal.span {x} ≤ J ∧ J.IsPrime}
Module: Mathlib.RingTheory.KrullDimension.PID

Goal state before:
pp: case refine_1
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
m : Ideal R
inst✝ : m.IsMaximal
h : ¬IsField R
⊢ m.height ≤ 1

Tactic:
suffices h : (m.height : WithBot ℕ∞) ≤ 1 by norm_cast at h
    rw [← IsPrincipalIdealRing.ringKrullDim_eq_one _ h]
    exact Ideal.height_le_ringKrullDim_of_ne_top Ideal.IsPrime.ne_top'

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

Goal state before:
pp: P : ProfiniteGrp.{u}
⊢ DenseRange ⇑(Hom.hom P.toLimit)

Tactic:
by
  apply dense_iff_inter_open.mpr
  rintro U ⟨s, hsO, hsv⟩ ⟨⟨spc, hspc⟩, uDefaultSpec⟩
  simp_rw [← hsv, Set.mem_preimage] at uDefaultSpec
  rcases (isOpen_pi_iff.mp hsO) _ uDefaultSpec with ⟨J, fJ, hJ1, hJ2⟩
  let M := iInf (fun (j : J) => j.1.1.1)
  have hM : M.Normal := Subgroup.normal_iInf_normal fun j => j.1.isNormal'
  have hMOpen : IsOpen (M : Set P) := by
    rw [Subgroup.coe_iInf]
    exact isOpen_iInter_of_finite fun i => i.1.1.isOpen'
  let m : OpenNormalSubgroup P := { M with isOpen' := hMOpen }
  rcases QuotientGroup.mk'_surjective M (spc m) with ⟨origin, horigin⟩
  use (toLimit P) origin
  refine ⟨?_, origin, rfl⟩
  rw [← hsv]
  apply hJ2
  intro a a_in_J
  let M_to_Na : m ⟶ a := (iInf_le (fun (j : J) => j.1.1.1) ⟨a, a_in_J⟩).hom
  rw [← (P.toLimit origin).property M_to_Na]
  change (P.toFiniteQuotientFunctor.map M_to_Na) (QuotientGroup.mk' M origin) ∈ _
  rw [horigin]
  exact Set.mem_of_eq_of_mem (hspc M_to_Na) (hJ1 a a_in_J).2

Goal state after:
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
⊢ 1 ≤ q ^ n

Tactic:
← card_D

Goal state after:
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
⊢ 1 ≤ card D
Module: Mathlib.RingTheory.LittleWedderburn

Goal state before:
pp: 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

Tactic:
by_contra! h
      obtain ⟨x, hx⟩ := finrank_le_one_iff.mp h
      refine not_le_of_gt hZ.lt_top (fun y _ ↦ Subring.mem_center_iff.mpr fun z ↦ ?_)
      obtain ⟨r, rfl⟩ := hx y
      obtain ⟨s, rfl⟩ := hx z
      rw [smul_mul_smul_comm, smul_mul_smul_comm, mul_comm]

Goal state after:
Module: Mathlib.RingTheory.LittleWedderburn

Goal state before:
pp: case intro.mk
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
i✝ : ConjClasses Dˣ
x : Dˣ
hx : ConjClasses.mk x ∈ ConjClasses.noncenter Dˣ
Zx : Subring D := Subring.centralizer {↑x}
⊢ eval (↑q) Φₙ ∣ ↑(ConjClasses.mk x).carrier.toFinset.card

Tactic:
rw [Set.toFinset_card, ConjClasses.card_carrier, ← card_congr
        (show Zxˣ ≃* _ from unitsCentralizerEquiv _ x).toEquiv, card_units, card_D]

Goal state after:
case intro.mk
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
i✝ : ConjClasses Dˣ
x : Dˣ
hx : ConjClasses.mk x ∈ ConjClasses.noncenter Dˣ
Zx : Subring D := Subring.centralizer {↑x}
⊢ eval (↑q) Φₙ ∣ ↑((q ^ n - 1) / card (↥Zx)ˣ)
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
N : Submodule R M
h : InfIrred N
⊢ N ≠ ⊤ ∧ ∀ {r : R} {x : M}, r • x ∈ N → x ∈ N ∨ ∃ n, r ^ n • ⊤ ≤ N

Tactic:
refine ⟨h.ne_top, fun {a b} hab ↦ ?_⟩

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
N : Submodule R M
h : InfIrred N
a : R
b : M
hab : a • b ∈ N
⊢ b ∈ N ∨ ∃ n, a ^ n • ⊤ ≤ N
Module: Mathlib.RingTheory.LocalIso

Goal state before:
pp: 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)
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
hq' : Ideal.comap (algebraMap S (T i)) q'.asIdeal = q
⊢ (algebraMap S (T i)) g ∉ q'.asIdeal

Tactic:
← hg,

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)
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
hq' : Ideal.comap (algebraMap S (T i)) q'.asIdeal = q
⊢ g' * (algebraMap S (T i)) (f i) ^ n ∉ q'.asIdeal
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
X : ModuleCat R
inj : Module.Injective R ↑X
x✝ : Small.{v, u} (Localization S) := small_of_surjective Localization.mkHom_surjective
⊢ Module.Injective (Localization S) ↑((localizedModuleFunctor S).1 X)

Tactic:
simpa [ModuleCat.localizedModuleFunctor] using
      Module.injective_of_isLocalizedModule S (X.localizedModuleMkLinearMap S)

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 R T
inst✝ : IsLocalIso R S
g : S
hg : g ∈ {g | IsStandardOpenImmersion R (Localization.Away g)}
⊢ g ∈ ↑(Ideal.comap TensorProduct.includeRight (Ideal.span {g | IsStandardOpenImmersion T (Localization.Away g)}))

Tactic:
apply Ideal.subset_span

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 R T
inst✝ : IsLocalIso R S
g : S
hg : g ∈ {g | IsStandardOpenImmersion R (Localization.Away g)}
⊢ TensorProduct.includeRight g ∈ {g | IsStandardOpenImmersion T (Localization.Away g)}
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
P : K⟮X⟯
⊢ ∀ (p q : K[X]),
    q ≠ 0 →
      (polynomialValuationX K) (RatFunc.mk p q) =
        (valuation K⸨X⸩ (PowerSeries.idealX K)) ((algebraMap K⟮X⟯ K⸨X⸩) (RatFunc.mk p q))

Tactic:
intro f g h

Goal state after:
K : Type u_2
inst✝ : Field K
P : K⟮X⟯
f g : K[X]
h : g ≠ 0
⊢ (polynomialValuationX K) (RatFunc.mk f g) =
    (valuation K⸨X⸩ (PowerSeries.idealX K)) ((algebraMap K⟮X⟯ K⸨X⸩) (RatFunc.mk f g))
Module: Mathlib.RingTheory.MvPolynomial.EulerIdentity

Goal state before:
pp: case refine_3
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
φ : MvPolynomial σ R
inst✝ : Fintype σ
n : ℕ
w : σ → ℕ
h : φ ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = n})
p q : MvPolynomial σ R
x✝¹ : p ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = n})
x✝ : q ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = n})
hp : ∑ i, w i • (X i * (pderiv i) p) = n • p
hq : ∑ i, w i • (X i * (pderiv i) q) = n • q
⊢ ∑ x, w x • (X x * ((pderiv x) p + (pderiv x) q)) = n • (p + q)

Tactic:
left_distrib,

Goal state after:
case refine_3
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
φ : MvPolynomial σ R
inst✝ : Fintype σ
n : ℕ
w : σ → ℕ
h : φ ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = n})
p q : MvPolynomial σ R
x✝¹ : p ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = n})
x✝ : q ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = n})
hp : ∑ i, w i • (X i * (pderiv i) p) = n • p
hq : ∑ i, w i • (X i * (pderiv i) q) = n • q
⊢ ∑ x, w x • (X x * (pderiv x) p + X x * (pderiv x) q) = n • (p + q)
Module: Mathlib.RingTheory.MvPolynomial.Expand

Goal state before:
pp: σ : 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
| f ^ (p ^ k * p)

Tactic:
pow_mul,

Goal state after:
σ : 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
| (f ^ p ^ k) ^ p
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
Rₚ : Type u_3
inst✝¹¹ : CommRing Rₚ
inst✝¹⁰ : Algebra R Rₚ
inst✝⁹ : IsLocalization.AtPrime Rₚ p
inst✝⁸ : IsLocalRing Rₚ
Sₚ : Type u_4
inst✝⁷ : CommRing Sₚ
inst✝⁶ : Algebra S Sₚ
inst✝⁵ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
P : Ideal S
hPp : P.LiesOver p
inst✝³ : Algebra R Sₚ
inst✝² : IsScalarTower R S Sₚ
inst✝¹ : IsScalarTower R Rₚ Sₚ
inst✝ : P.IsPrime
this✝³ : (Ideal.map (algebraMap S Sₚ) P).LiesOver (maximalIdeal Rₚ)
this✝² : (Ideal.map (algebraMap S Sₚ) P).LiesOver P
this✝¹ : (Ideal.map (algebraMap S Sₚ) P).IsPrime
R₁ : Type u_4 := Localization.AtPrime (Ideal.map (algebraMap S Sₚ) P)
R₂ : Type u_2 := Localization.AtPrime P
this✝ : Algebra R₂ R₁ := algebraOfLiesOver P (Ideal.map (algebraMap S Sₚ) P)
this : IsLocalization.AtPrime R₁ P
h : Function.Bijective ⇑(algebraMap R₂ R₁)
key : Ideal.map (algebraMap R R₂) p = comap (algebraMap R₂ R₁) (Ideal.map (algebraMap Rₚ R₁) (maximalIdeal Rₚ))
⊢ (length (Localization.AtPrime (Ideal.map (algebraMap S Sₚ) P))
        (Localization.AtPrime (Ideal.map (algebraMap S Sₚ) P) ⧸
          Ideal.map (algebraMap Rₚ (Localization.AtPrime (Ideal.map (algebraMap S Sₚ) P))) (maximalIdeal Rₚ))).toNat =
    (length (Localization.AtPrime P)
        (Localization.AtPrime P ⧸ Ideal.map (algebraMap R (Localization.AtPrime P)) p)).toNat

Tactic:
rw [Module.length_quotient, Module.length_quotient, key, coheight_comap_of_surjective _ h.2]

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case mp
K : Type u_2
inst✝ : Field K
S : Set (K⟮X⟯ × K⟮X⟯)
T : Set (K⸨X⸩ × K⸨X⸩)
pre_T : (fun x ↦ ((algebraMap K⟮X⟯ K⸨X⸩) x.1, (algebraMap K⟮X⟯ K⸨X⸩) x.2)) ⁻¹' T ⊆ S
R : Set K⸨X⸩
hR : R ∈ nhds 0
pre_R : (fun x ↦ x.2 - x.1) ⁻¹' R ⊆ T
d : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ
hd : {y | Valued.v.restrict (y - 0) < ↑d} ⊆ R
⊢ ∃ t ∈ nhds 0, (fun x ↦ x.2 - x.1) ⁻¹' t ⊆ S

Tactic:
use {P : K⟮X⟯ | Valued.v P < embedding d.1}

Goal state after:
case h
K : Type u_2
inst✝ : Field K
S : Set (K⟮X⟯ × K⟮X⟯)
T : Set (K⸨X⸩ × K⸨X⸩)
pre_T : (fun x ↦ ((algebraMap K⟮X⟯ K⸨X⸩) x.1, (algebraMap K⟮X⟯ K⸨X⸩) x.2)) ⁻¹' T ⊆ S
R : Set K⸨X⸩
hR : R ∈ nhds 0
pre_R : (fun x ↦ x.2 - x.1) ⁻¹' R ⊆ T
d : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ
hd : {y | Valued.v.restrict (y - 0) < ↑d} ⊆ R
⊢ {P | Valued.v P < embedding ↑d} ∈ nhds 0 ∧ (fun x ↦ x.2 - x.1) ⁻¹' {P | Valued.v P < embedding ↑d} ⊆ S
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case right.inr.ind.inl
R : Type u_3
inst✝ : CommRing R
n : ℕ
p : MvPolynomial (Fin n) R
hp : p ∈ symmetricSubalgebra (Fin n) R
h0 : p ≠ 0
ih :
  ∀ y < supDegree (⇑toLex) p,
    ∀ (p : MvPolynomial (Fin n) R) (hp : p ∈ symmetricSubalgebra (Fin n) R),
      p ≠ 0 → supDegree (⇑toLex) p = y → ⟨p, hp⟩ ∈ (esymmAlgHom (Fin n) R n).range
t : Fin n →₀ ℕ := Finsupp.equivFunOnFinite.symm (invAccumulate n n ⇑(ofLex (supDegree (⇑toLex) p)))
hd : supDegree (⇑toLex) (esymmAlgHomMonomial (Fin n) t (leadingCoeff (⇑toLex) p)) = supDegree (⇑toLex) p
he : p = esymmAlgHomMonomial (Fin n) t (leadingCoeff (⇑toLex) p)
⊢ ⟨p, hp⟩ ∈ (esymmAlgHom (Fin n) R n).range

Tactic:
convert! AlgHom.mem_range_self _ (monomial t <| p.leadingCoeff toLex)

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
f : Finset σ × σ → MvPolynomial σ R
⊢ ∑ i ∈ range k, ∑ x ∈ powersetCard i univ, ∑ y, f (x, y) =
    ∑ a ∈ antidiagonal k with a.1 < k, ∑ A ∈ powersetCard a.1 univ, ∑ j, f (A, j)

Tactic:
refine sum_nbij' (fun n ↦ (n, k - n)) Prod.fst ?_ ?_ ?_ ?_ ?_ <;>
    simp +contextual [@eq_comm _ _ k, le_of_lt]

Goal state after:
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:
← WithVal.apply_ofVal,

Goal state after:
case hf
K : Type u_2
inst✝ : Field K
x : WithVal (polynomialValuationX K)
⊢ Valued.v ((LaurentSeriesPkg K).coe x) = (polynomialValuationX K) x.ofVal
Module: Mathlib.RingTheory.MvPowerSeries.Expand

Goal state before:
pp: σ : 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
| f ^ (p ^ k * p)

Tactic:
pow_mul,

Goal state after:
σ : 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
| (f ^ p ^ k) ^ p
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
f : K⸨X⸩
⊢ Valued.v { toCompletion := (LaurentSeriesPkg K).compare ratfuncAdicComplPkg f } = Valued.v f

Tactic:
adicCompletion.valued_ofCompletion

Goal state after:
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
⊢ Valued.v ((LaurentSeriesPkg K).compare ratfuncAdicComplPkg f) = Valued.v f
Module: Mathlib.RingTheory.NoetherNormalization

Goal state before:
pp: k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
fne : f ≠ 0
v : Fin (n + 1) →₀ ℕ
vin : v ∈ f.support
h : (Fin (n + 1) →₀ ℕ) → MvPolynomial (Fin (n + 1)) k := fun w ↦ (MvPolynomial.monomial w) (MvPolynomial.coeff w f)
vs :
  ∀ x ∈ f.support \ {v},
    ((MvPolynomial.finSuccEquiv k n) ((T f) (h x))).degree < ((MvPolynomial.finSuccEquiv k n) ((T f) (h v))).degree
coeff :
  ((MvPolynomial.finSuccEquiv k n) ((T f) (h v + ∑ x ∈ f.support \ {v}, h x))).leadingCoeff =
    ((MvPolynomial.finSuccEquiv k n) ((T f) (h v))).leadingCoeff
⊢ IsUnit ((MvPolynomial.finSuccEquiv k n) ((T f) (h v + ∑ x ∈ f.support \ {v}, h x))).leadingCoeff

Tactic:
rw [leadingCoeff_finSuccEquiv_t] at coeff

Goal state after:
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
fne : f ≠ 0
v : Fin (n + 1) →₀ ℕ
vin : v ∈ f.support
h : (Fin (n + 1) →₀ ℕ) → MvPolynomial (Fin (n + 1)) k := fun w ↦ (MvPolynomial.monomial w) (MvPolynomial.coeff w f)
vs :
  ∀ x ∈ f.support \ {v},
    ((MvPolynomial.finSuccEquiv k n) ((T f) (h x))).degree < ((MvPolynomial.finSuccEquiv k n) ((T f) (h v))).degree
coeff :
  ((MvPolynomial.finSuccEquiv k n) ((T f) (h v + ∑ x ∈ f.support \ {v}, h x))).leadingCoeff =
    (algebraMap k (MvPolynomial (Fin n) k)) (MvPolynomial.coeff v f)
⊢ IsUnit ((MvPolynomial.finSuccEquiv k n) ((T f) (h v + ∑ x ∈ f.support \ {v}, h x))).leadingCoeff
Module: Mathlib.RingTheory.WittVector.Frobenius

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (bind₁ (wittPolynomial p ℚ ∘ fun n ↦ n + 1)) ((bind₁ (xInTermsOfW p ℚ)) (wittPolynomial p ℚ n)) =
    wittPolynomial p ℚ (n + 1)

Tactic:
bind₁_xInTermsOfW_wittPolynomial,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (bind₁ (wittPolynomial p ℚ ∘ fun n ↦ n + 1)) (X n) = wittPolynomial p ℚ (n + 1)
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
p : ℕ
f : Perfection M p
m n✝ n : ℕ
ih : (coeffMonoidHom M p (m + n)) (f ^ p ^ n) = (coeffMonoidHom M p m) f
⊢ (coeffMonoidHom M p (m + n.succ)) (f ^ (p ^ n * p)) = (coeffMonoidHom M p m) f

Tactic:
pow_mul,

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
p : ℕ
f : Perfection M p
m n✝ n : ℕ
ih : (coeffMonoidHom M p (m + n)) (f ^ p ^ n) = (coeffMonoidHom M p m) f
⊢ (coeffMonoidHom M p (m + n.succ)) ((f ^ p ^ n) ^ p) = (coeffMonoidHom M p m) f
Module: Mathlib.RingTheory.WittVector.Frobenius

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n i j : ℕ
hi : i ≤ n
hj : j < p ^ (n - i)
m : ℕ
h : v p (j + 1) = m
h₁ : m ≤ n - i
h₂ : m ≤ j
⊢ j + (n - m) = j + (i + (n - m - i))

Tactic:
add_comm i,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n i j : ℕ
hi : i ≤ n
hj : j < p ^ (n - i)
m : ℕ
h : v p (j + 1) = m
h₁ : m ≤ n - i
h₂ : m ≤ j
⊢ j + (n - m) = j + (n - m - i + i)
Module: Mathlib.RingTheory.WittVector.Verschiebung

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
⊢ (if 0 = 0 then 0 else x.coeff (0 - 1)) = 0

Tactic:
if_pos rfl

Goal state after:
p : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
⊢ 0 = 0
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 : ℕ
y : ModP O p
hxy0 : 0 * y ≠ 0
⊢ 0 * y = 0

Tactic:
rw [zero_mul]

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 * 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))))

Tactic:
pow_mul,

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.Identities

Goal state before:
pp: p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
⊢ (if 1 = 1 then 1 else 0) = 1

Tactic:
if_pos rfl

Goal state after:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
⊢ 1 = 1
Module: Mathlib.RingTheory.WittVector.Complete

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
x y : 𝕎 k
n : ℕ
⊢ (truncate n) (x - y) = 0 ↔ ∀ i < n, (x - y).coeff i = 0

Tactic:
by simp only [← mem_ker_truncate, RingHom.mem_ker]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x : 𝕎 k
h : x.coeff 0 = 0
⊢ x = verschiebung (x.shift 1)

Tactic:
simpa using eq_iterate_verschiebung (n := 1) (by simp [h])

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible 2
⊢ C 1 = 1

Tactic:
C_1

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible 2
⊢ 1 = 1
Module: Mathlib.RingTheory.Polynomial.Hermite.Gaussian

Goal state before:
pp: case succ.hd
n : ℕ
x : ℝ
ih : (deriv^[n] fun y ↦ Real.exp (-(y ^ 2 / 2))) = fun x ↦ (-1) ^ n * ((aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2)))
deriv_gaussian : deriv (fun y ↦ Real.exp (-(y ^ 2 / 2))) x = -x * Real.exp (-(x ^ 2 / 2))
⊢ DifferentiableAt ℝ (fun x ↦ Real.exp (-(x ^ 2 / 2))) x

Tactic:
apply DifferentiableAt.exp; simp

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

Goal state before:
pp: n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
⊢ z ^ (n % 3) * z ^ (3 * (n / 3)) = 1 ∨ z ^ (n % 3) * z ^ (3 * (n / 3)) = z ∨ z ^ (n % 3) * z ^ (3 * (n / 3)) = z ^ 2

Tactic:
pow_mul,

Goal state after:
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
⊢ z ^ (n % 3) * (z ^ 3) ^ (n / 3) = 1 ∨ z ^ (n % 3) * (z ^ 3) ^ (n / 3) = z ∨ z ^ (n % 3) * (z ^ 3) ^ (n / 3) = z ^ 2
Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre

Goal state before:
pp: n : ℕ
⊢ ↑n ! * ((-1) ^ n * (shiftedLegendre n).comp (1 - X)) = ↑n ! * shiftedLegendre n

Tactic:
rw [← mul_assoc, mul_comm (n ! : ℤ[X]), mul_assoc, ← natCast_mul_comp,
    factorial_mul_shiftedLegendre_eq, ← iterate_derivative_comp_one_sub_X]

Goal state after:
n : ℕ
⊢ (⇑derivative)^[n] ((X ^ n * (1 - X) ^ n).comp (1 - X)) = (⇑derivative)^[n] (X ^ n * (1 - X) ^ n)