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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
I : Ideal R
inst✝ : Submodule.IsPrincipal I
p : Ideal R
hp : p ∈ I.minimalPrimes
⊢ p.height ≤ 1

Tactic:
by
  have := hp.isPrime
  let f := algebraMap R (Localization.AtPrime p)
  have := Ideal.height_le_one_of_isPrincipal_of_mem_minimalPrimes_of_isLocalRing (I.map f) ?_
  · rwa [← IsLocalization.height_under p.primeCompl,
      Localization.AtPrime.under_maximalIdeal] at this
  · rwa [IsLocalization.minimalPrimes_map p.primeCompl (Localization.AtPrime p) I,
      Set.mem_preimage, Localization.AtPrime.under_maximalIdeal]

Goal state after:
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:
rw [← IsPrincipalIdealRing.ringKrullDim_eq_one _ h]

Goal state after:
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 ≤ ringKrullDim R
Module: Mathlib.RingTheory.KrullDimension.Polynomial

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
p : Ideal R
P : Ideal R[X]
inst✝¹ : P.IsMaximal
inst✝ : P.LiesOver p
⊢ P.height = p.height + 1

Tactic:
have : p.IsPrime := by rw [P.over_def p]; infer_instance

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
p : Ideal R
P : Ideal R[X]
inst✝¹ : P.IsMaximal
inst✝ : P.LiesOver p
this : p.IsPrime
⊢ P.height = p.height + 1
Module: Mathlib.RingTheory.KrullDimension.Polynomial

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

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

Goal state after:
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
x : M
⊢ t.inf (⇑radicalInfTopHom ∘ fun i ↦ (id i).colon {x}) =
    {x_1 ∈ t | x ∉ x_1}.inf fun q ↦ radicalInfTopHom (q.colon Set.univ)

Tactic:
Function.comp_def,

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
x : M
⊢ (t.inf fun x_1 ↦ radicalInfTopHom ((id x_1).colon {x})) =
    {x_1 ∈ t | x ∉ x_1}.inf fun q ↦ radicalInfTopHom (q.colon Set.univ)
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
t : Finset (Submodule R M)
ht : N.IsMinimalPrimaryDecomposition t
s₀ : Finset ↑N.associatedPrimes
hs₀ : IsLowerSet ↑s₀
s : Finset (Submodule R M)
hs : s ⊆ t
hs' : Finset.image (fun q ↦ (q.colon Set.univ).radical) s = Finset.image Subtype.val s₀
S : Submonoid R := ⨅ q ∈ s₀, (↑q).primeCompl
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
⊢ (t.inf fun i ↦ comap (mkLinearMap S M) ((⇑(localized₀FrameHom S (mkLinearMap S M)) ∘ id) i)) = ⨅ q ∈ s, q

Tactic:
Function.comp_def,

Goal state after:
R : Type u_3
M : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
t : Finset (Submodule R M)
ht : N.IsMinimalPrimaryDecomposition t
s₀ : Finset ↑N.associatedPrimes
hs₀ : IsLowerSet ↑s₀
s : Finset (Submodule R M)
hs : s ⊆ t
hs' : Finset.image (fun q ↦ (q.colon Set.univ).radical) s = Finset.image Subtype.val s₀
S : Submonoid R := ⨅ q ∈ s₀, (↑q).primeCompl
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
⊢ (t.inf fun i ↦ comap (mkLinearMap S M) ((localized₀FrameHom S (mkLinearMap S M)) (id i))) = ⨅ q ∈ s, q
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
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
H : ∀ (I : Ideal R) (x : I.IsMaximal), Injective (Localization.AtPrime I) (LocalizedModule I.primeCompl M)
I : Ideal R
x✝¹ : FinitePresentation R ↥I := finitePresentation_of_finite R ↥I
m : Ideal R
x✝ : m.IsMaximal
Rₘ : Type u := Localization.AtPrime m
Mₘ : Type (max u v) := LocalizedModule m.primeCompl M
f : M →ₗ[R] LocalizedModule m.primeCompl M := LocalizedModule.mkLinearMap m.primeCompl M
h : R →ₗ[R] Rₘ := Algebra.linearMap R Rₘ
Iₘ : Ideal Rₘ := Submodule.localized' Rₘ m.primeCompl h I
g : ↥I →ₗ[R] ↥Iₘ := Submodule.toLocalized' Rₘ m.primeCompl h I
gM : (↥I →ₗ[R] M) →ₗ[R] ↥Iₘ →ₗ[Rₘ] LocalizedModule m.primeCompl M :=
  IsLocalizedModule.mapExtendScalars m.primeCompl g f Rₘ
hM : (R →ₗ[R] M) →ₗ[R] Rₘ →ₗ[Rₘ] LocalizedModule m.primeCompl M :=
  IsLocalizedModule.mapExtendScalars m.primeCompl h f Rₘ
eq'' : ↑R (Submodule.subtype Iₘ) = (IsLocalizedModule.map m.primeCompl g h) (Submodule.subtype I)
l : R →ₗ[R] M
⊢ ↑R ((↑R (LinearMap.lcomp Rₘ Mₘ (Submodule.subtype Iₘ)) ∘ₗ hM) l) ∘ₗ g =
    ↑R (((IsLocalizedModule.map m.primeCompl hM gM) (LinearMap.lcomp R M (Submodule.subtype I)) ∘ₗ hM) l) ∘ₗ g

Tactic:
by ext; simp +zetaDelta [-Algebra.linearMap_apply]

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

Goal state before:
pp: case succ
R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
S : Submonoid R
this : Small.{v, u} (Localization S)
n : ℕ
ih : ∀ (M : ModuleCat R) [HasInjectiveDimensionLE M n], HasInjectiveDimensionLE (M.localizedModule S) n
M : ModuleCat R
inst✝ : HasInjectiveDimensionLE M (n + 1)
ei : EnoughInjectives (ModuleCat R)
I : ModuleCat R
inj : Injective I
f : M ⟶ I
monof : Mono f
T : ShortComplex (ModuleCat R) := { X₁ := M, X₂ := I, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }
⊢ HasInjectiveDimensionLE (M.localizedModule S) (n + 1)

Tactic:
have T_exact : T.ShortExact := { exact := ShortComplex.exact_cokernel f }

Goal state after:
case succ
R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
S : Submonoid R
this : Small.{v, u} (Localization S)
n : ℕ
ih : ∀ (M : ModuleCat R) [HasInjectiveDimensionLE M n], HasInjectiveDimensionLE (M.localizedModule S) n
M : ModuleCat R
inst✝ : HasInjectiveDimensionLE M (n + 1)
ei : EnoughInjectives (ModuleCat R)
I : ModuleCat R
inj : Injective I
f : M ⟶ I
monof : Mono f
T : ShortComplex (ModuleCat R) := { X₁ := M, X₂ := I, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }
T_exact : T.ShortExact
⊢ HasInjectiveDimensionLE (M.localizedModule S) (n + 1)
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
⊢ powerSeriesPart 0 = 0

Tactic:
by
  ext
  simp

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: R : Type u_1
F : Type u
inst✝ : Field F
p q : F[X]
f g : F⟮X⟯
⊢ FaithfulSMul F[X] F⸨X⸩

Tactic:
refine (faithfulSMul_iff_algebraMap_injective F[X] F⸨X⸩).mpr ?_
  exact algebraMap_hahnSeries_injective ℤ

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

Goal state before:
pp: R : Type u_1
σ : Type u_2
M : Type u_3
inst✝¹ : CommSemiring R
φ : MvPolynomial σ R
inst✝ : AddCancelCommMonoid M
w : σ → M
n n' : M
i : σ
h : IsWeightedHomogeneous w φ n
h' : n' + w i = n
⊢ IsWeightedHomogeneous w ((pderiv i) φ) n'

Tactic:
rw [← mem_weightedHomogeneousSubmodule, weightedHomogeneousSubmodule_eq_finsupp_supported,
    AddMonoidAlgebra.supported_eq_span_single] at h
  refine Submodule.span_induction ?_ ?_ (fun p q _ _ hp hq ↦ ?_) (fun r p _ h ↦ ?_) h
  · rintro _ ⟨m, hm, rfl⟩
    simp_rw [single_eq_monomial, pderiv_monomial, one_mul]
    by_cases hi : m i = 0
    · rw [hi, Nat.cast_zero, monomial_zero]; apply isWeightedHomogeneous_zero
    convert! isWeightedHomogeneous_monomial ..
    rw [← add_right_cancel_iff (a := w i), h', ← hm, weight_sub_single_add hi]
  · rw [map_zero]; apply isWeightedHomogeneous_zero
  · rw [map_add]; exact hp.add hq
  · rw [(pderiv i).map_smul]; exact (weightedHomogeneousSubmodule ..).smul_mem _ h

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

Goal state before:
pp: case inr
M : Type u_3
S : Type u_4
inst✝³ : AddMonoid M
inst✝² : Finset.HasAntidiagonal M
inst✝¹ : NormedRing S
inst✝ : IsUltrametricDist S
C : M → ℝ
hC : ∀ (a b : M), C (a + b) = C a * C b
f g : M → S
hf : Tendsto (fun i ↦ ‖f i‖ * C i) cofinite (𝓝 0)
hg : Tendsto (fun i ↦ ‖g i‖ * C i) cofinite (𝓝 0)
this :
  ∀ {C : M → ℝ},
    (∀ (a b : M), C (a + b) = C a * C b) →
      Tendsto (fun i ↦ ‖f i‖ * C i) cofinite (𝓝 0) →
        Tendsto (fun i ↦ ‖g i‖ * C i) cofinite (𝓝 0) →
          0 ≤ C → Tendsto (fun a ↦ ‖∑ p ∈ antidiagonal a, f p.1 * g p.2‖ * C a) cofinite (𝓝 0)
hC' : ¬0 ≤ C
⊢ Tendsto (fun x ↦ ‖‖∑ p ∈ antidiagonal x, f p.1 * g p.2‖ * C x‖) cofinite (𝓝 0)

Tactic:
simpa using this (C := |C|) (by simp [hC]) (by simpa using hf.norm)
      (by simpa using hg.norm) (fun _ => by simp)

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case a
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
this : UniformSpace ratfuncAdicComplPkg.space := ratfuncAdicComplPkg.uniformStruct
raw_surj : Function.Surjective ⇑Valued.v
x : ratfuncAdicComplPkg.space
h_cont : Continuous ⇑Valued.v
⊢ Tendsto (⇑Valued.v) (Filter.comap ratfuncAdicComplPkg.coe (𝓝 x)) (𝓝 (⋯.extend (⇑Valued.v) x))

Tactic:
ratfuncAdicComplPkg.isDenseInducing.extend_unique
        Valued.valuedCompletion_apply h_cont

Goal state after:
case a
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
this : UniformSpace ratfuncAdicComplPkg.space := ratfuncAdicComplPkg.uniformStruct
raw_surj : Function.Surjective ⇑Valued.v
x : ratfuncAdicComplPkg.space
h_cont : Continuous ⇑Valued.v
⊢ Tendsto (⇑Valued.v) (Filter.comap ratfuncAdicComplPkg.coe (𝓝 x)) (𝓝 (Valued.v x))
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝¹ : CommRing R
hp : NeZero p
inst✝ : CharZero R
n : ℕ
this : ∀ (i : ℕ), ((monomial (single i (p ^ (n - i)))) (↑p ^ i)).vars = {i}
⊢ (W_ R n).vars = range (n + 1)

Tactic:
rw [wittPolynomial, vars_sum_of_disjoint]

Goal state after:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
hp : NeZero p
inst✝ : CharZero R
n : ℕ
this : ∀ (i : ℕ), ((monomial (single i (p ^ (n - i)))) (↑p ^ i)).vars = {i}
⊢ ((range (n + 1)).biUnion fun i ↦ ((monomial (single i (p ^ (n - i)))) (↑p ^ i)).vars) = range (n + 1)

case h
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
hp : NeZero p
inst✝ : CharZero R
n : ℕ
this : ∀ (i : ℕ), ((monomial (single i (p ^ (n - i)))) (↑p ^ i)).vars = {i}
⊢ Pairwise (Function.onFun Disjoint fun i ↦ ((monomial (single i (p ^ (n - i)))) (↑p ^ i)).vars)
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: case ind
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ (xInTermsOfW p ℚ m).vars ∧ (xInTermsOfW p ℚ m).vars ⊆ range (m + 1)
i : ℕ
⊢ i ∈ {n} ∨ i ∈ (∑ i ∈ range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)).vars → i ∈ {n} ∪ range n

Tactic:
mem_union

Goal state after:
case ind
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ (xInTermsOfW p ℚ m).vars ∧ (xInTermsOfW p ℚ m).vars ⊆ range (m + 1)
i : ℕ
⊢ i ∈ {n} ∨ i ∈ (∑ i ∈ range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)).vars → i ∈ {n} ∨ i ∈ range n
Module: Mathlib.RingTheory.NoetherNormalization

Goal state before:
pp: k : Type u_2
R : Type u_3
inst✝² : Field k
inst✝¹ : CommRing R
inst✝ : Nontrivial R
a : Algebra k R
fin : Algebra.FiniteType k R
s : ℕ
g : MvPolynomial (Fin s) k →ₐ[k] R
inj : Function.Injective ⇑g
int : g.IsIntegral
algInst✝ : Algebra (MvPolynomial (Fin s) k) R := g.toAlgebra
algebraizeInst✝ : Algebra.IsIntegral (MvPolynomial (Fin s) k) R
⊢ algebraMap k R = g.comp (algebraMap k (MvPolynomial (Fin s) k))

Tactic:
IsScalarTower.algebraMap_eq k (MvPolynomial (Fin s) k),

Goal state after:
k : Type u_2
R : Type u_3
inst✝² : Field k
inst✝¹ : CommRing R
inst✝ : Nontrivial R
a : Algebra k R
fin : Algebra.FiniteType k R
s : ℕ
g : MvPolynomial (Fin s) k →ₐ[k] R
inj : Function.Injective ⇑g
int : g.IsIntegral
algInst✝ : Algebra (MvPolynomial (Fin s) k) R := g.toAlgebra
algebraizeInst✝ : Algebra.IsIntegral (MvPolynomial (Fin s) k) R
⊢ (algebraMap (MvPolynomial (Fin s) k) R).comp (algebraMap k (MvPolynomial (Fin s) k)) =
    g.comp (algebraMap k (MvPolynomial (Fin s) k))
Module: Mathlib.RingTheory.WittVector.Basic

Goal state before:
pp: p : ℕ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : R →+* S
n : ℕ
⊢ mapFun (⇑f) n.unaryCast = ↑n

Tactic:
induction n <;> simp [*, Nat.unaryCast, add, one, zero]

Goal state after:
case zero
p : ℕ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : R →+* S
⊢ 0 = ↑0

case succ
p : ℕ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : R →+* S
n✝ : ℕ
a✝ : mapFun (⇑f) n✝.unaryCast = ↑n✝
⊢ ↑n✝ + 1 = ↑(n✝ + 1)
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)
⊢ ↑p ^ n * ⅟↑p ^ n = 1

Tactic:
rw [← mul_pow, mul_invOf_self, one_pow]

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

Goal state before:
pp: p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ (wittStructureRat p Φ n).vars ⊆ Finset.univ ×ˢ Finset.range (n + 1)

Tactic:
by
  rw [wittStructureRat]
  intro x hx
  simp only [Finset.mem_product, true_and, Finset.mem_univ, Finset.mem_range]
  obtain ⟨k, hk, hx'⟩ := mem_vars_bind₁ _ _ hx
  obtain ⟨i, -, hx''⟩ := mem_vars_bind₁ _ _ hx'
  obtain ⟨j, hj, rfl⟩ := mem_vars_rename _ _ hx''
  rw [wittPolynomial_vars, Finset.mem_range] at hj
  replace hk := xInTermsOfW_vars_subset p _ hk
  grind

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

Goal state before:
pp: p : ℕ
R S : Type u
idx : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : ⦃R : Type u_2⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n ↦ peval (φ n) ![x.coeff, y.coeff]
⊢ IsPoly p fun x _Rcr x_1 ↦ f x_1 x_1

Tactic:
refine ⟨⟨fun n => bind₁ (uncurry ![X, X]) (φ n), ?_⟩⟩

Goal state after:
p : ℕ
R S : Type u
idx : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : ⦃R : Type u_2⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n ↦ peval (φ n) ![x.coeff, y.coeff]
⊢ ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x : 𝕎 R),
    (f x x).coeff = fun n ↦ (aeval x.coeff) ((fun n ↦ (bind₁ (uncurry ![X, X])) (φ n)) n)
Module: Mathlib.RingTheory.WittVector.Frobenius

Goal state before:
pp: p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
x : 𝕎 R
⊢ (ghostComponent n) x.frobeniusFun = (ghostComponent (n + 1)) x

Tactic:
by
  simp only [ghostComponent_apply, frobeniusFun, coeff_mk, ← bind₁_frobeniusPoly_wittPolynomial,
    aeval_bind₁]

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

Goal state before:
pp: p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CharP R p
inst✝ : PerfectRing R p
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
n : ℕ
⊢ (frobenius ((map ↑(_root_.frobeniusEquiv R p).symm) f)).coeff n = f.coeff n

Tactic:
by
      rw [frobenius_eq_map_frobenius]
      exact frobenius_apply_frobeniusEquiv_symm R p _

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

Goal state before:
pp: p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
hx : x ≠ 0
⊢ ∃ n x', x'.coeff 0 ≠ 0 ∧ x = (⇑verschiebung)^[n] x'

Tactic:
have hex : ∃ k : ℕ, x.coeff k ≠ 0 := by
    by_contra! hall
    apply hx
    ext i
    simp only [hall, zero_coeff]

Goal state after:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
hx : x ≠ 0
hex : ∃ k, x.coeff k ≠ 0
⊢ ∃ n x', x'.coeff 0 ≠ 0 ∧ x = (⇑verschiebung)^[n] x'
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: case pos
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 : PreTilt O p
hf0 : f = 0
⊢ (val K v O hv p) f = 0 ↔ f = 0

Tactic:
hf0

Goal state after:
case pos
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 : PreTilt O p
hf0 : f = 0
⊢ (val K v O hv p) 0 = 0 ↔ 0 = 0
Module: Mathlib.RingTheory.Polynomial.Hermite.Gaussian

Goal state before:
pp: 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 (fun y ↦ Real.exp (-(y ^ 2 / 2))) x = -x * Real.exp (-(x ^ 2 / 2))

Tactic:
rw [deriv_exp (by simp)]

Goal state after:
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)))
⊢ Real.exp (-(x ^ 2 / 2)) * deriv (fun y ↦ -(y ^ 2 / 2)) x = -x * Real.exp (-(x ^ 2 / 2))
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
R' : Type u_1 := R ⧸ nilradical R
ψ : R' →+* S := Ideal.Quotient.lift (nilradical R) φ ⋯
ι : R →+* R' := algebraMap R R'
hi : Irreducible (Polynomial.map ι f)
a b : R[X]
h : f = a * b
hb : IsUnit (Polynomial.map ι b)
⊢ IsUnit a ∨ IsUnit b

Tactic:
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)

Goal state after:
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
R' : Type u_1 := R ⧸ nilradical R
ψ : R' →+* S := Ideal.Quotient.lift (nilradical R) φ ⋯
ι : R →+* R' := algebraMap R R'
hi : Irreducible (Polynomial.map ι f)
a b : R[X]
h : f = a * b
hb : IsUnit (Polynomial.map ι b)
hn : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (b.coeff i)
⊢ IsUnit a ∨ IsUnit b
Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG

Goal state before:
pp: R : Type u
M : Type u_1
N : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq { P // P.FG }
P : { P // P.FG }
u : ↥↑P ⊗[R] N
this :
  ↑(directLimit R M N) ∘ₗ
      Module.DirectLimit.of R { P // P.FG } (fun P ↦ ↥↑P ⊗[R] N) (fun x x_1 hPQ ↦ rTensor N (inclusion hPQ)) P =
    rTensor N (↑P).subtype
⊢ (directLimit R M N)
      ((Module.DirectLimit.of R { P // P.FG } (fun P ↦ ↥↑P ⊗[R] N) (fun ⦃x x_1⦄ h ↦ rTensor N (inclusion h)) P) u) =
    (rTensor N (↑P).subtype) u

Tactic:
by
    exact DFunLike.congr_fun this u

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

Goal state before:
pp: n : ℕ
hn : 0 < n
x : ℕ
a : x < n
h : 0 < x
⊢ (coeff x) (X * largeSchroderSeries) * (n - x).largeSchroder = (x - 1).largeSchroder * (n - x).largeSchroder

Tactic:
simp_all only [mul_eq_mul_right_iff]
      simp [coeff_X_mul_largeSchroderSeries x (by lia)]

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG

Goal state before:
pp: R : Type u
M : Type u_1
N : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq { P // P.FG }
Q : { Q // Q.FG }
u : M ⊗[R] ↥↑Q
this :
  ↑(directLimit R M N) ∘ₗ
      Module.DirectLimit.of R { Q // Q.FG } (fun Q ↦ M ⊗[R] ↥↑Q) (fun x x_1 hPQ ↦ lTensor M (inclusion hPQ)) Q =
    lTensor M (↑Q).subtype
⊢ (directLimit R M N)
      ((Module.DirectLimit.of R { Q // Q.FG } (fun Q ↦ M ⊗[R] ↥↑Q) (fun x x_1 hPQ ↦ lTensor M (inclusion hPQ)) Q) u) =
    (lTensor M (↑Q).subtype) u

Tactic:
by
    exact DFunLike.congr_fun this u

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG

Goal state before:
pp: R : Type u_1
S : Type u_2
N : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
A : Subalgebra R S
hA : A.FG
t t' : ↥A ⊗[R] N
h : (rTensor N A.val.toLinearMap) t = (rTensor N A.val.toLinearMap) t'
P : Submodule R ↥A
hP : P.FG
u : ↥P ⊗[R] N
hu : (rTensor N P.subtype) u = t
P' : Submodule R ↥A
hP' : P'.FG
u' : ↥P' ⊗[R] N
hu' : (rTensor N P'.subtype) u' = t'
P₁ : Submodule R S := Submodule.map (Subalgebra.toSubmodule A).subtype (P ⊔ P')
hP₁ : P₁.FG
j : ↥P →ₗ[R] ↥P₁ := (Subalgebra.toSubmodule A).subtype.restrict ⋯
j' : ↥P' →ₗ[R] ↥P₁ := (Subalgebra.toSubmodule A).subtype.restrict ⋯
u₁ : ↥P₁ ⊗[R] N := (rTensor N j) u
hu₁ : u₁ = (rTensor N j) u
u'₁ : ↥P₁ ⊗[R] N := (rTensor N j') u'
hu'₁ : u'₁ = (rTensor N j') u'
hj₁ : P₁.subtype ∘ₗ j = A.val.toLinearMap ∘ₗ P.subtype
hj'₁ : P₁.subtype ∘ₗ j' = A.val.toLinearMap ∘ₗ P'.subtype
⊢ (rTensor N A.val.toLinearMap) ((rTensor N P.subtype) u) = (rTensor N A.val.toLinearMap) ((rTensor N P'.subtype) u')

Tactic:
rw [hu, hu', h]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : Module S N
inst✝¹ : IsScalarTower R S N
inst✝ : Flat R S
f : M →ₗ[R] N
hf : IsBaseChange S f
rs : List R
reg : IsWeaklyRegular M rs
⊢ IsWeaklyRegular N (List.map (⇑(algebraMap R S)) rs)

Tactic:
induction rs generalizing M N with
  | nil => simp
  | cons x _ ih =>
    simp only [List.map_cons, isWeaklyRegular_cons_iff] at reg ⊢
    have e := (QuotSMulTop.algebraMapTensorEquivTensorQuotSMulTop x M S).symm ≪≫ₗ
      QuotSMulTop.congr ((algebraMap R S) x) hf.equiv
    have hg : IsBaseChange S <|
        e.toLinearMap.restrictScalars R ∘ₗ TensorProduct.mk R S (QuotSMulTop x M) 1 :=
      IsBaseChange.of_equiv e (fun _ ↦ by simp)
    exact ⟨reg.1.of_flat_of_isBaseChange hf, ih hg reg.2⟩

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

Goal state before:
pp: A : Type u_1
inst✝ : CommRing A
f g q : A⟦X⟧
r : A[X]
I : Ideal A
i : ℕ
hi : i < ((map (Ideal.Quotient.mk I)) g).order.toNat
H : f - ↑r = g * q
⊢ (coeff i) (f - ↑r) ∈ I

Tactic:
rw [H]

Goal state after:
A : Type u_1
inst✝ : CommRing A
f g q : A⟦X⟧
r : A[X]
I : Ideal A
i : ℕ
hi : i < ((map (Ideal.Quotient.mk I)) g).order.toNat
H : f - ↑r = g * q
⊢ (coeff i) (g * q) ∈ I