mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ IsLocalIso R T

Tactic:
by
  -- The proof is purely formal given that open immersions are stable under composition.
  let s : Set S := {g : S | IsStandardOpenImmersion R (Localization.Away g)}
  let T' (g : S) := Localization.Away (algebraMap S T g)
  let (g : S) : Algebra (Localization.Away g) (T' g) := localizationAlgebra (.powers g) T
  let T'' (g : S) (x : T) := Localization.Away (algebraMap _ (T' g) x)
  let t (g : S) : Set T := {x : T | IsStandardOpenImmersion (Localization.Away g) (T'' g x)}
  let ι : Type _ := Σ i : s, t i.1
  have (i : ι) : IsStandardOpenImmersion (Localization.Away i.1.1) (T'' i.1 i.2) := i.2.2
  suffices h : Ideal.span (Set.range fun i : ι ↦ algebraMap S T i.1 * i.2) = ⊤ by
    have (i : ι) : IsStandardOpenImmersion R (T'' i.1 i.2) :=
      have : IsScalarTower R (Localization.Away i.1.1) (T' i.1.1) :=
        IsScalarTower.to₁₃₄ _ S _ _
      have : IsStandardOpenImmersion (Localization.Away i.1.1) (T'' i.1.1 i.2.1) := i.2.2
      have : IsStandardOpenImmersion R (Localization.Away i.1.1) := i.1.2
      .trans _ (Localization.Away i.1.1) _
    exact .of_span_range_eq_top _ h fun i : ι ↦ T'' i.1 i.2
  have h1 := congr(Ideal.map (algebraMap S T) $(span_isStandardOpenImmersion_eq_top R S))
  rw [Ideal.map_top, Ideal.map_span] at h1
  nth_rw 1 [_root_.eq_top_iff, ← Ideal.top_mul ⊤, ← h1, ← span_isStandardOpenImmersion_eq_top S T,
    Ideal.span_mul_span, Ideal.span_le, Set.mul_subset_iff]
  simp only [Set.mem_image, Set.mem_ofPred_eq, SetLike.mem_coe, forall_exists_index, and_imp,
    forall_apply_eq_imp_iff₂]
  intro g hg x hx
  refine Ideal.subset_span ⟨⟨⟨g, hg⟩, ⟨x, ?_⟩⟩, rfl⟩
  simp only [Set.mem_ofPred_eq, t]
  let : Algebra (Localization.Away x) (T'' g x) :=
    localizationAlgebra (.powers x) (T' g)
  have : IsScalarTower S (Localization.Away x) (T'' g x) :=
    IsScalarTower.to₁₃₄ _ T _ _
  have : IsLocalization (algebraMapSubmonoid (Localization.Away x) (.powers g)) (T'' g x) := by
    have : algebraMapSubmonoid (Localization.Away x) (.powers g) =
      algebraMapSubmonoid (Localization.Away x) (.powers (algebraMap S T g)) := by
        simp [IsScalarTower.algebraMap_apply S T (Localization.Away x)]
    rw [this]
    exact .commutes _ (T' g) _ (.powers x) (.powers (algebraMap S T g))
  have : IsPushout S (Localization.Away x) (Localization.Away g) (T'' g x) :=
    Algebra.isPushout_of_isLocalization (.powers g) _ _ _
  exact .of_isPushout S (Localization.Away x) _ _

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
inst✝¹ : IsNoetherianRing R
n : ℕ
M : ModuleCat R
inst✝ : Module.Finite R ↑M
P : Type v
w✝³ : AddCommGroup P
w✝² : Module R P
w✝¹ : Module.Free R P
w✝ : Module.Finite R P
f : P →ₗ[R] ↑M
ih :
  HasProjectiveDimensionLE (of R ↥f.ker) n ↔
    ∀ (m : MaximalSpectrum R), HasProjectiveDimensionLE ((of R ↥f.ker).localizedModule m.asIdeal.primeCompl) n
surjf : Function.Surjective ⇑f
S : ShortComplex (ModuleCat R) := f.shortComplexKer
S_exact : f.shortComplexKer.ShortExact
proj : Projective S.X₂
Sp : (p : MaximalSpectrum R) → ShortComplex (ModuleCat (Localization p.asIdeal.primeCompl)) :=
  fun p ↦ S.map (localizedModuleFunctor p.asIdeal.primeCompl)
Sp_exact : ∀ (p : MaximalSpectrum R), (Sp p).ShortExact
⊢ HasProjectiveDimensionLE M (n + 1) ↔
    ∀ (m : MaximalSpectrum R), HasProjectiveDimensionLE (M.localizedModule m.asIdeal.primeCompl) (n + 1)

Tactic:
have projp (p : MaximalSpectrum R) : Projective (Sp p).X₂ :=
      (ModuleCat.localizedModuleFunctor.{v} p.1.primeCompl).projective_obj_of_projective proj

Goal state after:
case succ
R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
n : ℕ
M : ModuleCat R
inst✝ : Module.Finite R ↑M
P : Type v
w✝³ : AddCommGroup P
w✝² : Module R P
w✝¹ : Module.Free R P
w✝ : Module.Finite R P
f : P →ₗ[R] ↑M
ih :
  HasProjectiveDimensionLE (of R ↥f.ker) n ↔
    ∀ (m : MaximalSpectrum R), HasProjectiveDimensionLE ((of R ↥f.ker).localizedModule m.asIdeal.primeCompl) n
surjf : Function.Surjective ⇑f
S : ShortComplex (ModuleCat R) := f.shortComplexKer
S_exact : f.shortComplexKer.ShortExact
proj : Projective S.X₂
Sp : (p : MaximalSpectrum R) → ShortComplex (ModuleCat (Localization p.asIdeal.primeCompl)) :=
  fun p ↦ S.map (localizedModuleFunctor p.asIdeal.primeCompl)
Sp_exact : ∀ (p : MaximalSpectrum R), (Sp p).ShortExact
projp : ∀ (p : MaximalSpectrum R), Projective (Sp p).X₂
⊢ HasProjectiveDimensionLE M (n + 1) ↔
    ∀ (m : MaximalSpectrum R), HasProjectiveDimensionLE (M.localizedModule m.asIdeal.primeCompl) (n + 1)
Module: Mathlib.RingTheory.LocalRing.Etale

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalRing S
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R S
inst✝¹ : FaithfulSMul R S
inst✝ : Etale R S
this : Module.Free R S
⊢ ∀ (c : R ⧸ maximalIdeal R) (x : S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R)),
    (Ideal.quotEquivOfEq ⋯).toAddEquiv (c • x) = c • (Ideal.quotEquivOfEq ⋯).toAddEquiv x

Tactic:
intro r x
    obtain ⟨r, rfl⟩ := Ideal.Quotient.mk_surjective r
    obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
    simp only [RingEquiv.toAddEquiv_eq_coe]; rfl

Goal state after:
Module: Mathlib.RingTheory.Invariant.Profinite

Goal state before:
pp: case refine_1
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
P : Ideal A
Q : Ideal B
inst✝² : Q.IsPrime
inst✝¹ : Q.LiesOver P
inst✝ : Algebra.IsInvariant A B G
σ : (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q
B' : (G : Type u) → [inst : Monoid G] → [inst_1 : MulSemiringAction G B] → [SMulCommClass G A B] → Subalgebra A B :=
  FixedPoints.subalgebra A B
s : (j : OpenNormalSubgroup G) → (stabilizerHomSurjectiveAuxFunctor P Q σ).obj j
hs : s ∈ (stabilizerHomSurjectiveAuxFunctor P Q σ).sections
a : ↑(ProfiniteGrp.of G).toProfinite.toTop :=
  (ProfiniteGrp.Hom.hom (ProfiniteGrp.of G).isoLimittoFiniteQuotientFunctor.inv) ⟨fun N ↦ ↑↑(s N), ⋯⟩
this : ∀ (N : OpenNormalSubgroup G), ↑a = ↑↑(s N)
N : OpenNormalSubgroup G
x : ↥(B' ↥↑N.toOpenSubgroup)
hN : ↑N ⊆ ↑(MulAction.stabilizer G ↑x)
⊢ x ∈ under (↥(B' ↥↑N.toOpenSubgroup)) (a • Q) ↔ x ∈ under (↥(B' ↥↑N.toOpenSubgroup)) Q

Tactic:
← (s N).1.2

Goal state after:
case refine_1
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
P : Ideal A
Q : Ideal B
inst✝² : Q.IsPrime
inst✝¹ : Q.LiesOver P
inst✝ : Algebra.IsInvariant A B G
σ : (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q
B' : (G : Type u) → [inst : Monoid G] → [inst_1 : MulSemiringAction G B] → [SMulCommClass G A B] → Subalgebra A B :=
  FixedPoints.subalgebra A B
s : (j : OpenNormalSubgroup G) → (stabilizerHomSurjectiveAuxFunctor P Q σ).obj j
hs : s ∈ (stabilizerHomSurjectiveAuxFunctor P Q σ).sections
a : ↑(ProfiniteGrp.of G).toProfinite.toTop :=
  (ProfiniteGrp.Hom.hom (ProfiniteGrp.of G).isoLimittoFiniteQuotientFunctor.inv) ⟨fun N ↦ ↑↑(s N), ⋯⟩
this : ∀ (N : OpenNormalSubgroup G), ↑a = ↑↑(s N)
N : OpenNormalSubgroup G
x : ↥(B' ↥↑N.toOpenSubgroup)
hN : ↑N ⊆ ↑(MulAction.stabilizer G ↑x)
⊢ x ∈ under (↥(B' ↥↑N.toOpenSubgroup)) (a • Q) ↔
    x ∈ ↑↑(s N) • under (↥(FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup)) Q
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case refine_1.negSucc
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
h : ∀ n < 0, f.coeff n = 0
n : ℕ
⊢ ((ofPowerSeries ℤ K) (PowerSeries.mk fun n ↦ f.coeff ↑n)).coeff (Int.negSucc n) = 0

pp: case refine_2
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
n✝ : ℤ
a✝ : n✝ < 0
⊢ ((ofPowerSeries ℤ K) F).coeff n✝ = 0

Tactic:
all_goals
    apply HahnSeries.embDomain_of_notMem_range
    simp only [Nat.coe_castAddMonoidHom, RelEmbedding.coe_mk, Function.Embedding.coeFn_mk,
      Set.mem_range, not_exists, reduceCtorEq]
    intro

Goal state after:
case refine_1.negSucc
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
h : ∀ n < 0, f.coeff n = 0
n x✝ : ℕ
⊢ ¬False

case refine_2
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
n✝ : ℤ
a✝ : n✝ < 0
x✝ : ℕ
⊢ ¬↑x✝ = n✝
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
x✝¹ : σ →₀ ℕ
x✝ : R
⊢ (map (frobenius R p)) ((expand p) ((monomial x✝¹) x✝)) = (monomial x✝¹) x✝ ^ p

Tactic:
simp [monomial_pow, frobenius]

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
U : Set K⸨X⸩
hU : U ∈ 𝓝 (limit hℱ)
γ : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ
hU₁ : {y | Valued.v.restrict (y - limit hℱ) < ↑γ} ⊆ U
this : ∀ᶠ (f : K⸨X⸩) in ℱ, f ∈ {y | Valued.v (y - limit hℱ) < embedding ↑γ}
⊢ ∀ᶠ (f : K⸨X⸩) in ℱ, f ∈ U

Tactic:
simp_rw [← Valued.v.restrict_lt_iff_lt_embedding] at this
    apply this.mono fun _ hf ↦ hU₁ hf

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

Goal state before:
pp: case refine_1
n m : ℕ
hmn : m ≤ n
s : Fin m → ℕ
hs : Antitone s
x✝¹ : Fin m
i✝ : ℕ
this : i✝ ≤ m - 1
i : ℕ
hi : i < m - 1
x✝ : i✝ ≤ i
ih : ∀ (hi : i + 1 < m), (accumulate n m) (invAccumulate n m s) ⟨i + 1, hi⟩ = s ⟨i + 1, hi⟩
him : i < m
⊢ (accumulate n m) (invAccumulate n m s) ⟨i, him⟩ = s ⟨i, him⟩

Tactic:
rw [← Nat.pred_eq_sub_one, Nat.lt_pred_iff, Nat.succ_eq_add_one] at hi
    rw [accumulate_rec (him.trans_le hmn) hi, ih hi, invAccumulate, dif_pos him, dif_pos hi]
    simp only
    exact Nat.sub_add_cancel (hs i.le_succ)

Goal state after:
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 ((algebraMap K⟦X⟧ K⸨X⸩) (F - ↑((trunc (d + 1)) F))) ≤ ↑η * ↑(Multiplicative.ofAdd (-1))
⊢ (valuation K⸨X⸩ (PowerSeries.idealX K)) ↑(F - ↑((trunc (d + 1)) F)) < ↑η

Tactic:
apply lt_of_le_of_lt this

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 ((algebraMap K⟦X⟧ K⸨X⸩) (F - ↑((trunc (d + 1)) F))) ≤ ↑η * ↑(Multiplicative.ofAdd (-1))
⊢ ↑η * ↑(Multiplicative.ofAdd (-1)) < ↑η
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

Goal state before:
pp: case refine_1
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
f : Finset σ × σ → MvPolynomial σ R
⊢ ∀ a ∈ range k, (a, k - a) ∈ {a ∈ antidiagonal k | a.1 < k}

Tactic:
simp +contextual [@eq_comm _ _ k, le_of_lt]

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

Goal state before:
pp: case refine_2
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
f : Finset σ × σ → MvPolynomial σ R
⊢ ∀ a ∈ {a ∈ antidiagonal k | a.1 < k}, a.1 ∈ range k

Tactic:
simp +contextual [@eq_comm _ _ k, le_of_lt]

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

Goal state before:
pp: case refine_3
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
f : Finset σ × σ → MvPolynomial σ R
⊢ ∀ a ∈ range k, (a, k - a).1 = a

Tactic:
simp +contextual [@eq_comm _ _ k, le_of_lt]

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

Goal state before:
pp: case refine_4
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
f : Finset σ × σ → MvPolynomial σ R
⊢ ∀ a ∈ {a ∈ antidiagonal k | a.1 < k}, (a.1, k - a.1) = a

Tactic:
simp +contextual [@eq_comm _ _ k, le_of_lt]

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

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

Tactic:
simp +contextual [@eq_comm _ _ k, le_of_lt]

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
⊢ Subring.map (LaurentSeriesRingEquiv K).toRingHom (powerSeries_as_subring K) =
    (adicCompletionIntegers K⟮X⟯ (idealX K)).toSubring

Tactic:
by
  ext x
  refine ⟨fun ⟨f, ⟨F, _, coe_F⟩, hF⟩ ↦ ?_, fun H ↦ ?_⟩
  · simp only [ValuationSubring.mem_toSubring, ← hF, ← coe_F]
    apply mem_integers_of_powerSeries
  · obtain ⟨F, hF⟩ := exists_powerSeries_of_memIntegers K H
    simp only [Subring.mem_map]
    exact ⟨F, ⟨F, trivial, rfl⟩, hF⟩

Goal state after:
Module: Mathlib.RingTheory.NormTrace

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : Free A B
inst✝ : Module.Finite A B
a : A
x : B
ι : Type u_2 := Free.ChooseBasisIndex A B
⊢ ∃ r, (norm A) (1 + a • x) = 1 + (trace A B) x * a + r * a ^ 2

Tactic:
let b : Basis ι A B := Module.Free.chooseBasis _ _

Goal state after:
A : Type u_1
B : Type u_2
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : Free A B
inst✝ : Module.Finite A B
a : A
x : B
ι : Type u_2 := Free.ChooseBasisIndex A B
b : Basis ι A B := Free.chooseBasis A B
⊢ ∃ r, (norm A) (1 + a • x) = 1 + (trace A B) x * a + r * a ^ 2
Module: Mathlib.RingTheory.NoetherNormalization

Goal state before:
pp: k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
a : k
ha : a ≠ 0
⊢ degreeOf 0 ((T f) ((MvPolynomial.monomial v) a)) = ∑ i, r i * v i

Tactic:
← natDegree_finSuccEquiv,

Goal state after:
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
a : k
ha : a ≠ 0
⊢ ((MvPolynomial.finSuccEquiv k n) ((T f) ((MvPolynomial.monomial v) a))).natDegree = ∑ i, r i * v i
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
n i : ℕ
x✝ : i ∈ range (n + 1)
⊢ (map f) ((monomial (single i (p ^ (n - i)))) (↑p ^ i)) = (monomial (single i (p ^ (n - i)))) (↑p ^ i)

Tactic:
rw [map_monomial, map_pow, map_natCast]

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

Goal state before:
pp: p n : ℕ
⊢ frobeniusPolyAux p n =
    X (n + 1) -
      ∑ i ∈ range n,
        ∑ j ∈ range (p ^ (n - i)),
          (X i ^ p) ^ (p ^ (n - i) - (j + 1)) * frobeniusPolyAux p i ^ (j + 1) *
            C ↑((p ^ (n - i)).choose (j + 1) / p ^ (n - i - v p (j + 1)) * p ^ (j - v p (j + 1)))

Tactic:
by
  rw [frobeniusPolyAux, ← Fin.sum_univ_eq_sum_range]

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

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

Tactic:
← mul_assoc

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

Goal state before:
pp: case zero
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
⊢ (verschiebung (frobenius x)).coeff 0 = (x * ↑p).coeff 0

Tactic:
rw [mul_charP_coeff_zero, verschiebung_coeff_zero]

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 : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
⊢ ModP.preVal K v O p ((coeff 0) 1) ^ p ^ 0 = 1

Tactic:
rw [pow_zero, pow_one, map_one, ← (Ideal.Quotient.mk _).map_one, ModP.preVal_mk hv,
      map_one, v.map_one]
    change (1 : ModP O p) ≠ 0
    exact one_ne_zero

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
⊢ verschiebung (x.shift 1) = (frobeniusEquiv p k).symm (x.shift 1) * ↑p

Tactic:
← verschiebung_frobenius,

Goal state after:
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
⊢ verschiebung (x.shift 1) = verschiebung (frobenius ((frobeniusEquiv p k).symm (x.shift 1)))
Module: Mathlib.RingTheory.Polynomial.Dickson

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
k : ℕ
a : R
⊢ dickson k a 2 = X ^ 2 - C a * (3 - ↑k)

Tactic:
by
  simp only [dickson, sq]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Hermite.Basic

Goal state before:
pp: case p1
n : ℕ
⊢ (hermite n).coeff n ≠ 0

Tactic:
simp [coeff_hermite_self n]

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

Goal state before:
pp: case succ
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
n : ℕ
hn : p.natDegree < n
d : ℕ
hd :
  (PowerSeries.coeff n) (↑p * ↑(invOneSubPow F d)) =
    eval (↑n)
      (match d with
      | 0 => 0
      | d.succ => ∑ i ∈ p.support, p.coeff i • preHilbertPoly F d i)
h_le : ∀ (i : ↥p.support), ↑i ≤ n
⊢ (PowerSeries.coeff n) (↑p * ↑(invOneSubPow F (d + 1))) = ∑ i, p.coeff ↑i * eval (↑n) (preHilbertPoly F d ↑i)

Tactic:
have h (i : p.support) : eval ↑n (preHilbertPoly F d ↑i) = (n + d - ↑i).choose d := by
        rw [preHilbertPoly_eq_choose_sub_add _ _ (h_le i), Nat.sub_add_comm (h_le i)]

Goal state after:
case succ
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
n : ℕ
hn : p.natDegree < n
d : ℕ
hd :
  (PowerSeries.coeff n) (↑p * ↑(invOneSubPow F d)) =
    eval (↑n)
      (match d with
      | 0 => 0
      | d.succ => ∑ i ∈ p.support, p.coeff i • preHilbertPoly F d i)
h_le : ∀ (i : ↥p.support), ↑i ≤ n
h : ∀ (i : ↥p.support), eval (↑n) (preHilbertPoly F d ↑i) = ↑((n + d - ↑i).choose d)
⊢ (PowerSeries.coeff n) (↑p * ↑(invOneSubPow F (d + 1))) = ∑ i, p.coeff ↑i * eval (↑n) (preHilbertPoly F d ↑i)
Module: Mathlib.RingTheory.Polynomial.IrreducibleRing

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : (nilradical R).IsPrime
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
hm : f.Monic
hi : Irreducible (Polynomial.map φ f)
⊢ Irreducible f

Tactic:
by
  let R' := R ⧸ nilradical R
  let ψ : R' →+* S := Ideal.Quotient.lift (nilradical R) φ
    (haveI := RingHom.ker_isPrime φ; nilradical_le_prime (RingHom.ker φ))
  let ι := algebraMap R R'
  rw [show φ = ψ.comp ι from rfl, ← map_map] at hi
  replace hi := hm.map ι |>.irreducible_of_irreducible_map _ _ hi
  refine ⟨fun h ↦ hi.1 <| (mapRingHom ι).isUnit_map h, fun a b h ↦ ?_⟩
  wlog hb : IsUnit (b.map ι) generalizing a b
  · exact (this b a (mul_comm a b ▸ h)
      (hi.2 (by rw [h, Polynomial.map_mul]) |>.resolve_right hb)).symm
  have hn (i : ℕ) (hi : i ≠ 0) : IsNilpotent (b.coeff i) := by
    obtain ⟨_, _, h⟩ := Polynomial.isUnit_iff.1 hb
    simpa only [coeff_map, coeff_C, hi, ite_false, ← RingHom.mem_ker,
      show RingHom.ker ι = nilradical R from Ideal.mk_ker] using! congr(coeff $(h.symm) i)
  refine .inr <| isUnit_of_coeff_isUnit_isNilpotent (isUnit_of_mul_isUnit_right
    (x := a.coeff f.natDegree) <| (IsUnit.neg_iff _).1 ?_) hn
  have hc : f.leadingCoeff = _ := congr(coeff $h f.natDegree)
  rw [hm, coeff_mul, Finset.Nat.sum_antidiagonal_eq_sum_range_succ fun i j ↦ a.coeff i * b.coeff j,
    Finset.sum_range_succ, ← sub_eq_iff_eq_add, Nat.sub_self] at hc
  rw [← add_sub_cancel_left 1 (-(_ * _)), ← sub_eq_add_neg, hc]
  exact IsNilpotent.isUnit_sub_one <| show _ ∈ nilradical R from sum_mem fun i hi ↦
    Ideal.mul_mem_left _ _ <| hn _ <| Nat.sub_ne_zero_of_lt (List.mem_range.1 hi)

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

Goal state before:
pp: case h.right
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
h : F[X]
N : ℕ
hhN : ∀ n > N, (PowerSeries.coeff n) (↑p * ↑(invOneSubPow F d)) = eval (↑n) h
n : ℕ
hn : N < n ∧ p.natDegree < n
⊢ eval (↑n) h = eval (↑n) (p.hilbertPoly d)

Tactic:
rw [← coeff_mul_invOneSubPow_eq_hilbertPoly_eval d hn.2, hhN n hn.1]

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

Goal state before:
pp: case a.e_a.H
n x : ℕ
a✝ : x ∈ range (n + 1)
⊢ x ! * n ! ∣ (x + n)!

Tactic:
simp only [factorial_mul_factorial_dvd_factorial_add]

Goal state after:
Module: Mathlib.RingTheory.PolynomialLaw.Basic

Goal state before:
pp: R : Type u
inst✝⁴ : CommSemiring R
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_2
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₚₗ[R] N
S : Type u
x✝² : CommSemiring S
x✝¹ : Algebra R S
x✝ : S ⊗[R] M
⊢ (1 • f).toFun' S x✝ = f.toFun' S x✝

Tactic:
simp only [smul_def, Pi.smul_apply, _root_.one_smul]

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.Schroder

Goal state before:
pp: case neg
n : ℕ
hn : ¬n = 0
hn' : 0 < n
⊢ n.largeSchroder = (coeff n) (X * largeSchroderSeries) + (coeff n) (X * largeSchroderSeries ^ 2)

Tactic:
coeff_X_mul_largeSchroderSeriesSeries_sq _ hn',

Goal state after:
case neg
n : ℕ
hn : ¬n = 0
hn' : 0 < n
⊢ n.largeSchroder = (coeff n) (X * largeSchroderSeries) + ∑ i ∈ range n, i.largeSchroder * (n - 1 - i).largeSchroder
Module: Mathlib.RingTheory.Radical.NatInt

Goal state before:
pp: case inr.refine_2
z : ℤ
hz : z ≠ 0
p : ℤ
h : ∃ a, (Nat.Prime a ∧ a ∣ z.natAbs ∧ z.natAbs ≠ 0) ∧ ↑a = p
⊢ Prime p ∧ 0 ≤ p ∧ p ∣ z

Tactic:
obtain ⟨n, ⟨pn, dn, -⟩, rfl⟩ := h

Goal state after:
case inr.refine_2
z : ℤ
hz : z ≠ 0
n : ℕ
pn : Nat.Prime n
dn : n ∣ z.natAbs
⊢ Prime ↑n ∧ 0 ≤ ↑n ∧ ↑n ∣ z
Module: Mathlib.RingTheory.PolynomialLaw.Basic

Goal state before:
pp: R : Type u
inst✝⁶ : CommSemiring R
M : Type u_1
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommMonoid N
inst✝² : Module R N
S : Type v
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
f : M →ₚₗ[R] N
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
s' : Finset S
p' : MvPolynomial (Fin s'.card) R ⊗[R] M
h : π R M S ⟨s, p⟩ = π R M S ⟨s', p'⟩
u : ↥(φ R s).range ⊗[R] M := (rTensor M (φ R s).rangeRestrict.toLinearMap) p
hu : u = (rTensor M (φ R s).rangeRestrict.toLinearMap) p
⊢ (Subalgebra.map (φ R s) ⊤).FG

Tactic:
exact Subalgebra.FG.map _ Algebra.FiniteType.out

Goal state after:
Module: Mathlib.RingTheory.PolynomialLaw.Basic

Goal state before:
pp: R : Type u
inst✝⁶ : CommSemiring R
M : Type u_1
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommMonoid N
inst✝² : Module R N
S : Type v
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
f : M →ₚₗ[R] N
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
s' : Finset S
p' : MvPolynomial (Fin s'.card) R ⊗[R] M
h : π R M S ⟨s, p⟩ = π R M S ⟨s', p'⟩
u : ↥(φ R s).range ⊗[R] M := (rTensor M (φ R s).rangeRestrict.toLinearMap) p
hu : u = (rTensor M (φ R s).rangeRestrict.toLinearMap) p
uFG : (φ R s).range.FG
u' : ↥(φ R s').range ⊗[R] M := (rTensor M (φ R s').rangeRestrict.toLinearMap) p'
hu' : u' = (rTensor M (φ R s').rangeRestrict.toLinearMap) p'
⊢ (Subalgebra.map (φ R s') ⊤).FG

Tactic:
exact Subalgebra.FG.map _ Algebra.FiniteType.out

Goal state after: