mathlib-initiative/mathlib-tactics huggingface dataset:
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

Goal state after:
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
h : n ≤ 1
⊢ False
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
this : ∀ q ∈ t, comap f (localized₀ S f q) = if q ∈ s then q else ⊤
⊢ (t.inf fun i ↦ comap (mkLinearMap S M) (localized₀ S (mkLinearMap S M) i)) = ⨅ q ∈ s, q

Tactic:
rw [Finset.inf_congr rfl this, Finset.inf_ite, Finset.inf_top, inf_top_eq,
      Finset.filter_mem_eq_inter, Finset.inter_eq_right.mpr hs, Finset.inf_eq_iInf]

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
s : Set S
h✝ : Ideal.span s = ⊤
h : ∀ x ∈ s, IsLocalIso R (Localization.Away x)
⊢ IsLocalIso R S

Tactic:
have heq : Ideal.span (Set.range fun i : s ↦ i.1) = ⊤ := by simpa
  have (i : s) : IsLocalIso R (Localization.Away i.1) := h _ i.property
  exact .of_span_range_eq_top _ heq fun i ↦ Localization.Away i.1

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 := ⋯ }
T_exact : T.ShortExact
T_exact' : Function.Exact ⇑(ConcreteCategory.hom T.f) ⇑(ConcreteCategory.hom T.g)
TS_exact' :
  Function.Exact
    ⇑((IsLocalizedModule.map S (T.X₁.localizedModuleMkLinearMap S) (T.X₂.localizedModuleMkLinearMap S))
        (ConcreteCategory.hom T.f))
    ⇑((IsLocalizedModule.map S (T.X₂.localizedModuleMkLinearMap S) (T.X₃.localizedModuleMkLinearMap S))
        (ConcreteCategory.hom T.g))
TS : ShortComplex (ModuleCat (Localization S)) := T.map (localizedModuleFunctor S)
TS_exact : TS.ShortExact
x✝¹ : HasInjectiveDimensionLT T.X₃ (n + 1) :=
  (ShortComplex.ShortExact.hasInjectiveDimensionLT_X₃_iff T_exact n inj).mpr inst✝
x✝ : Injective TS.X₂ := Functor.injective_obj (localizedModuleFunctor S) T.X₂
⊢ HasInjectiveDimensionLE (M.localizedModule S) (n + 1)

Tactic:
exact (TS_exact.hasInjectiveDimensionLT_X₃_iff n ‹_›).mp (ih T.X₃)

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : Small.{v, u} R
S : Submonoid R
X : ModuleCat R
proj : Projective X
⊢ Projective ((localizedModuleFunctor S).obj X)

Tactic:
by
    have : Small.{v} (Localization S) := small_of_surjective Localization.mkHom_surjective
    rw [← IsProjective.iff_projective] at proj ⊢
    simpa [ModuleCat.localizedModuleFunctor] using
      Module.projective_of_isLocalizedModule S (X.localizedModuleMkLinearMap S)

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : Small.{v, u} R
S : Submonoid R
M : ModuleCat R
n : ℕ
⊢ projectiveDimension M ≤ ↑n → projectiveDimension (M.localizedModule S) ≤ ↑n

Tactic:
simp only [projectiveDimension_le_iff]

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : Small.{v, u} R
S : Submonoid R
M : ModuleCat R
n : ℕ
⊢ HasProjectiveDimensionLE M n → HasProjectiveDimensionLE (M.localizedModule S) n
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: R✝ : Type u_1
R : Type u_2
V : Type u_3
inst✝² : AddCommGroup V
inst✝¹ : Semiring R
inst✝ : Module R V
k : ℕ
f g : V⸨X⸩
⊢ ofSuppBddBelow (fun n ↦ Ring.choose (n + ↑k) k • (f + g).coeff (n + ↑k)) ⋯ =
    ofSuppBddBelow (fun n ↦ Ring.choose (n + ↑k) k • f.coeff (n + ↑k)) ⋯ +
      ofSuppBddBelow (fun n ↦ Ring.choose (n + ↑k) k • g.coeff (n + ↑k)) ⋯

Tactic:
ext
    simp only [ofSuppBddBelow, coeff_add', Pi.add_apply, smul_add]

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

Goal state before:
pp: case refine_2
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 : φ ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = n})
h' : n' + w i = n
⊢ IsWeightedHomogeneous w ((pderiv i) 0) n'

Tactic:
rw [map_zero]

Goal state after:
case refine_2
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 : φ ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = n})
h' : n' + w i = n
⊢ IsWeightedHomogeneous w 0 n'
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: σ : Type u_1
R : Type u_3
n k : ℕ
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
i : Fin n
r : R
⊢ esymmAlgHomMonomial σ (fun₀ | i => k) r = C r * esymm σ R (↑i + 1) ^ k

Tactic:
by
  rw [esymmAlgHomMonomial, esymmAlgHom_apply, aeval_monomial, algebraMap_eq,
    Finsupp.prod_single_index]
  exact pow_zero _

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
k : ℕ
⊢ ∑ a ∈ antidiagonal k with a.1 < k, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2 =
    ∑ t ∈ pairs σ k with #t.1 < k, weight σ R k t

Tactic:
← sum_congr rfl (fun a ha ↦ esymm_mul_psum_summand_to_weight σ R k a (mem_filter.mp ha).left),

Goal state after:
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
k : ℕ
⊢ ∑ a ∈ antidiagonal k with a.1 < k, ∑ A ∈ powersetCard a.1 univ, ∑ j, weight σ R k (A, j) =
    ∑ t ∈ pairs σ k with #t.1 < k, weight σ R k t
Module: Mathlib.RingTheory.MvPowerSeries.Expand

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

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 ⟨m, hm⟩ : ∃ m, p • m = d := ⟨d.mapRange (fun a ↦ a / p) (by simp),
          by ext i; simp [(Nat.mul_div_cancel' (h i))]⟩
        rw [← hm, coeff_expand_smul, coeff_of_lt_order]
        simp only [← hm, map_nsmul, smul_eq_mul, Nat.cast_mul, nsmul_eq_mul] at hd
        exact lt_of_mul_lt_mul_left' hd

Goal state after:
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
Module: Mathlib.RingTheory.Morita.Matrix

Goal state before:
pp: R : Type u
ι : Type v
inst✝² : Ring R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : ModuleCat (Matrix ι ι R)
j : ι
m : ↑M
⊢ (fun m ↦ ∑ i, single i j 1 • ↑(m i)) ((fun m i ↦ ⟨single j i 1 • m, ⋯⟩) m) = m

Tactic:
by simp [← mul_smul, ← Finset.sum_smul, sum_single_one]

Goal state after:
Module: Mathlib.RingTheory.NoetherNormalization

Goal state before:
pp: k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v w : Fin (n + 1) →₀ ℕ
hv : v ∈ f.support
hw : w ∈ f.support
ne : v ≠ w
⊢ degreeOf 0 ((T f) ((MvPolynomial.monomial v) (MvPolynomial.coeff v f))) ≠
    degreeOf 0 ((T f) ((MvPolynomial.monomial w) (MvPolynomial.coeff w f)))

Tactic:
rw [degreeOf_zero_t _ _ <| mem_support_iff.mp hv, degreeOf_zero_t _ _ <| mem_support_iff.mp hw]
  refine sum_r_mul_ne f v w (fun i ↦ ?_) (fun i ↦ ?_) ne <;>
  exact lt_of_le_of_lt ((monomial_le_degreeOf i ‹_›).trans (degreeOf_le_totalDegree f i))
    (by lia)

Goal state after:
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)
⊢ n ∈ (X n).vars ∪ (∑ i ∈ range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)).vars ∧
    (X n).vars ∪ (∑ i ∈ range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)).vars ⊆ range (n + 1)

pp: case ind.hpq
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ (xInTermsOfW p ℚ m).vars ∧ (xInTermsOfW p ℚ m).vars ⊆ range (m + 1)
⊢ Disjoint (X n).vars (∑ i ∈ range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)).vars

Tactic:
vars_X,

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)
⊢ n ∈ {n} ∪ (∑ i ∈ range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)).vars ∧
    {n} ∪ (∑ i ∈ range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)).vars ⊆ range (n + 1)

case ind.hpq
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ (xInTermsOfW p ℚ m).vars ∧ (xInTermsOfW p ℚ m).vars ⊆ range (m + 1)
⊢ Disjoint (X n).vars (∑ i ∈ range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)).vars
Module: Mathlib.RingTheory.WittVector.WittPolynomial

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

Tactic:
vars_X,

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

Goal state before:
pp: p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
hn : 0 < n
⊢ (aeval (Function.uncurry fun i ↦ (![] i).coeff)) (wittOne p n) = 0

Tactic:
simp only [hn, wittOne_pos_eq_zero, map_zero]

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

Goal state before:
pp: case ind.e_a
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible ↑p
n : ℕ
H : ∀ m < n, (bind₁ (W_ R)) (xInTermsOfW p R m) = X m
⊢ W_ R n - ∑ x ∈ range n, (bind₁ (W_ R)) (C (↑p ^ x) * xInTermsOfW p R x ^ p ^ (n - x)) = X n * C (↑p ^ n)

Tactic:
rw [wittPolynomial_eq_sum_C_mul_X_pow, sum_range_succ_comm,
    tsub_self, pow_zero, pow_one, mul_comm (X n), add_sub_assoc, add_eq_left, sub_eq_zero]

Goal state after:
case ind.e_a
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible ↑p
n : ℕ
H : ∀ m < n, (bind₁ (W_ R)) (xInTermsOfW p R m) = X m
⊢ ∑ x ∈ range n, C (↑p ^ x) * X x ^ p ^ (n - x) =
    ∑ x ∈ range n, (bind₁ (W_ R)) (C (↑p ^ x) * xInTermsOfW p R x ^ p ^ (n - x))
Module: Mathlib.RingTheory.WittVector.Basic

Goal state before:
pp: case zero
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
⊢ (Nat.unaryCast 0).ghostFun = ↑0

Tactic:
simp [*, Nat.unaryCast, ghostFun_zero, ghostFun_one, ghostFun_add]

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

Goal state before:
pp: case succ
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
n✝ : ℕ
a✝ : n✝.unaryCast.ghostFun = ↑n✝
⊢ (n✝ + 1).unaryCast.ghostFun = ↑(n✝ + 1)

Tactic:
simp [*, Nat.unaryCast, ghostFun_zero, ghostFun_one, ghostFun_add]

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

Goal state before:
pp: p : ℕ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
α : Type u_3
β : Type u_4
inst✝ : Invertible ↑p
⊢ RightInverse (fun x ↦ mk p fun n ↦ (aeval x) (xInTermsOfW p R n)) ghostFun

Tactic:
intro x
    ext n
    have := bind₁_xInTermsOfW_wittPolynomial p R n
    apply_fun aeval x at this
    simpa only [aeval_bind₁, aeval_X, ghostFun, aeval_wittPolynomial]

Goal state after:
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: case refine_2.inr.inr
R : Type u_1
inst✝¹ : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
h : Function.Surjective ⇑(frobenius R p)
n : ℕ
x : R
m : ℕ
h1 : ¬n ≤ m + 1
⊢ (fun m ↦
          if h_1 : n ≤ m then Nat.leRec x (fun ⦃k⦄ hle xk ↦ (fun x hx ↦ x) (Classical.choose ⋯) ⋯) h_1
          else x ^ p ^ (n - m))
        (m + 1) ^
      p =
    (fun m ↦
        if h_1 : n ≤ m then Nat.leRec x (fun ⦃k⦄ hle xk ↦ (fun x hx ↦ x) (Classical.choose ⋯) ⋯) h_1
        else x ^ p ^ (n - m))
      m

Tactic:
· have h1' : ¬ n ≤ m := by lia
      have : n - m = (n - (m + 1)) + 1 := by lia
      simp [h1, h1', this, pow_succ, pow_mul]

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
x : 𝕎 R
i : ℕ
ih : ∀ (y : 𝕎 R), (⇑verschiebung)^[i] x * y = (⇑verschiebung)^[i] (x * (⇑frobenius)^[i] y)
y : 𝕎 R
⊢ (⇑verschiebung)^[i + 1] x * y = (⇑verschiebung)^[i + 1] (x * (⇑frobenius)^[i + 1] y)

Tactic:
| succ i ih =>

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
k i : ℕ
ih : ((⇑frobenius)^[i] x).coeff k = x.coeff k ^ p ^ i
⊢ ((⇑frobenius)^[i + 1] x).coeff k = x.coeff k ^ p ^ (i + 1)

Tactic:
| succ i ih =>

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
hp : Nat.Prime p
this : Nontrivial (PreTilt O p)
a✝ b✝ : PreTilt O p
hfg : a✝ * b✝ = 0
⊢ a✝ = 0 ∨ b✝ = 0

Tactic:
simp_rw [← map_eq_zero hv] at hfg ⊢; contrapose! hfg; rw [Valuation.map_mul]
      exact mul_ne_zero hfg.1 hfg.2

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

Goal state before:
pp: case succ
n : ℕ
ih : hermite n = (fun p ↦ X * p - derivative p)^[n] 1
⊢ hermite (n + 1) = X * (fun p ↦ X * p - derivative p)^[n] 1 - derivative ((fun p ↦ X * p - derivative p)^[n] 1)

Tactic:
← ih,

Goal state after:
case succ
n : ℕ
ih : hermite n = (fun p ↦ X * p - derivative p)^[n] 1
⊢ hermite (n + 1) = X * hermite n - derivative (hermite n)
Module: Mathlib.RingTheory.Polynomial.Hermite.Gaussian

Goal state before:
pp: case zero
x : ℝ
⊢ deriv^[0] (fun y ↦ Real.exp (-(y ^ 2 / 2))) x = (-1) ^ 0 * ((aeval x) (hermite 0) * Real.exp (-(x ^ 2 / 2)))

Tactic:
rw [Function.iterate_zero_apply, pow_zero, one_mul, hermite_zero, C_1, map_one, one_mul]

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

Tactic:
simp [mul_comm]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
⊢ IsRightCancelMulZero R[X] ↔ IsRightCancelMulZero R ∧ IsCancelAdd R

Tactic:
rw [← MulOpposite.isLeftCancelMulZero_iff, (opRingEquiv R).isLeftCancelMulZero_iff,
    isLeftCancelMulZero_iff, MulOpposite.isLeftCancelMulZero_iff, MulOpposite.isCancelAdd_iff]

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

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

Tactic:
simp [mul_comm]

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

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
⊢ Function.support ((MvPowerSeries.expand p hp) φ) ⊆ (fun x ↦ p • x) '' Function.support φ

Tactic:
MvPowerSeries.support_expand

Goal state after:
R : Type u_2
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
⊢ (fun x ↦ p • x) '' Function.support φ ⊆ (fun x ↦ p • x) '' Function.support φ
Module: Mathlib.RingTheory.PowerSeries.Expand

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
⊢ Function.support ((MvPowerSeries.expand p hp) φ) = (fun x ↦ p • x) '' Function.support φ

Tactic:
MvPowerSeries.support_expand

Goal state after:
R : Type u_2
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
⊢ (fun x ↦ p • x) '' Function.support φ = (fun x ↦ p • x) '' Function.support φ
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
u : S ⊗[R] N
P : Submodule R S
hu : u ∈ (rTensor N P.subtype).range
s : Finset S
hs : span R ↑s = P
⊢ ↑s ⊆ ↑(Algebra.adjoin R ↑s)

Tactic:
exact Algebra.subset_adjoin

Goal state after:
Module: Mathlib.RingTheory.RegularLocalRing.Defs

Goal state before:
pp: case neg
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsLocalRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
isf : ¬IsField R
⊢ IsRegularLocalRing R

Tactic:
apply of_spanFinrank_maximalIdeal_le
    rcases IsPrincipalIdealRing.principal (maximalIdeal R) with ⟨x, hx⟩
    simpa only [(IsPrincipalIdealRing.ringKrullDim_eq_one R) isf,
      Nat.cast_le_one, ← Set.ncard_singleton x, hx] using
        Submodule.spanFinrank_span_le_ncard_of_finite (Set.finite_singleton x)

Goal state after:
Module: Mathlib.RingTheory.RegularLocalRing.Defs

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
R' : Type u_2
inst✝¹ : CommRing R'
e : R ≃+* R'
inst✝ : IsRegularRing R
this : IsNoetherianRing R'
⊢ IsRegularRing R'

Tactic:
isRegularRing_iff

Goal state after:
R : Type u_1
inst✝² : CommRing R
R' : Type u_2
inst✝¹ : CommRing R'
e : R ≃+* R'
inst✝ : IsRegularRing R
this : IsNoetherianRing R'
⊢ ∀ (p : Ideal R') [inst : p.IsPrime], IsRegularLocalRing (Localization.AtPrime p)
Module: Mathlib.RingTheory.RegularLocalRing.Defs

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
⊢ IsRegularRing R

Tactic:
isRegularRing_iff

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
⊢ ∀ (p : Ideal R) [inst : p.IsPrime], IsRegularLocalRing (Localization.AtPrime p)
Module: Mathlib.RingTheory.Regular.ProjectiveDimension

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
n✝ : ℕ
M : ModuleCat R
inst✝ : Module.Finite R ↑M
w✝⁴ : Type v
w✝³ : AddCommGroup w✝⁴
w✝² : Module R w✝⁴
w✝¹ : Free R w✝⁴
w✝ : Module.Finite R w✝⁴
f : w✝⁴ →ₗ[R] ↑M
surjf : Function.Surjective ⇑f
S : ShortComplex (ModuleCat R) := ⋯
hS : S.ShortExact
n : ℕ
hn :
  ∀ (M : ModuleCat R) [Module.Finite R ↑M],
    (∀ (L : ModuleCat R), Module.Finite R ↑L → Subsingleton (Ext M L (n + 1))) → HasProjectiveDimensionLT M (n + 1)
h : ∀ (L : ModuleCat R), Module.Finite R ↑L → Subsingleton (Ext M L (n + 1 + 1))
this : ∀ (L : ModuleCat R), Subsingleton (Ext S.X₁ L (n + 1)) ↔ Subsingleton (Ext M L (n + 2))
⊢ ∀ (L : ModuleCat R), Module.Finite R ↑L → Subsingleton (Ext S.X₁ L (n + 1))

Tactic:
simpa [this] using h

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

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : Small.{v, u} R
inst✝² : IsLocalRing R
inst✝¹ : IsNoetherianRing R
M : ModuleCat R
inst✝ : Module.Finite R ↑M
x : R
reg : IsSMulRegular (↑M) x
mem : x ∈ maximalIdeal R
sub : Subsingleton ↑M ↔ Subsingleton (QuotSMulTop x ↑M)
n : ℕ
⊢ Module.Projective R (QuotSMulTop x ↑M) ↔ Subsingleton (QuotSMulTop x ↑M)

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ Projective.of_free⟩

Goal state after:
R : Type u
inst✝⁴ : CommRing R
inst✝³ : Small.{v, u} R
inst✝² : IsLocalRing R
inst✝¹ : IsNoetherianRing R
M : ModuleCat R
inst✝ : Module.Finite R ↑M
x : R
reg : IsSMulRegular (↑M) x
mem : x ∈ maximalIdeal R
sub : Subsingleton ↑M ↔ Subsingleton (QuotSMulTop x ↑M)
n : ℕ
h : Module.Projective R (QuotSMulTop x ↑M)
⊢ Subsingleton (QuotSMulTop x ↑M)
Module: Mathlib.RingTheory.RingInvo

Goal state before:
pp: F : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : EquivLike F R Rᵐᵒᵖ
f : RingInvo R
tE : R ≃ Rᵐᵒᵖ
map_mul'✝ : ∀ (x y : R), tE.toFun (x * y) = tE.toFun x * tE.toFun y
map_add'✝ : ∀ (x y : R), tE.toFun (x + y) = tE.toFun x + tE.toFun y
involution'✝ :
  ∀ (x : R),
    MulOpposite.unop
        ({ toEquiv := tE, map_mul' := map_mul'✝, map_add' := map_add'✝ }.toFun
          (MulOpposite.unop ({ toEquiv := tE, map_mul' := map_mul'✝, map_add' := map_add'✝ }.toFun x))) =
      x
h₁ : { toEquiv := tE, map_mul' := map_mul'✝, map_add' := map_add'✝, involution' := involution'✝ }.toFun = f.toFun
h₂ : { toEquiv := tE, map_mul' := map_mul'✝, map_add' := map_add'✝, involution' := involution'✝ }.invFun = f.invFun
⊢ { toEquiv := tE, map_mul' := map_mul'✝, map_add' := map_add'✝, involution' := involution'✝ } = f

Tactic:
rcases f with ⟨⟨tF, _⟩, _⟩

Goal state after:
F : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : EquivLike F R Rᵐᵒᵖ
tE : R ≃ Rᵐᵒᵖ
map_mul'✝¹ : ∀ (x y : R), tE.toFun (x * y) = tE.toFun x * tE.toFun y
map_add'✝¹ : ∀ (x y : R), tE.toFun (x + y) = tE.toFun x + tE.toFun y
involution'✝¹ :
  ∀ (x : R),
    MulOpposite.unop
        ({ toEquiv := tE, map_mul' := map_mul'✝¹, map_add' := map_add'✝¹ }.toFun
          (MulOpposite.unop ({ toEquiv := tE, map_mul' := map_mul'✝¹, map_add' := map_add'✝¹ }.toFun x))) =
      x
tF : R ≃ Rᵐᵒᵖ
map_mul'✝ : ∀ (x y : R), tF.toFun (x * y) = tF.toFun x * tF.toFun y
map_add'✝ : ∀ (x y : R), tF.toFun (x + y) = tF.toFun x + tF.toFun y
involution'✝ :
  ∀ (x : R),
    MulOpposite.unop
        ({ toEquiv := tF, map_mul' := map_mul'✝, map_add' := map_add'✝ }.toFun
          (MulOpposite.unop ({ toEquiv := tF, map_mul' := map_mul'✝, map_add' := map_add'✝ }.toFun x))) =
      x
h₁ :
  { toEquiv := tE, map_mul' := map_mul'✝¹, map_add' := map_add'✝¹, involution' := involution'✝¹ }.toFun =
    { toEquiv := tF, map_mul' := map_mul'✝, map_add' := map_add'✝, involution' := involution'✝ }.toFun
h₂ :
  { toEquiv := tE, map_mul' := map_mul'✝¹, map_add' := map_add'✝¹, involution' := involution'✝¹ }.invFun =
    { toEquiv := tF, map_mul' := map_mul'✝, map_add' := map_add'✝, involution' := involution'✝ }.invFun
⊢ { toEquiv := tE, map_mul' := map_mul'✝¹, map_add' := map_add'✝¹, involution' := involution'✝¹ } =
    { toEquiv := tF, map_mul' := map_mul'✝, map_add' := map_add'✝, involution' := involution'✝ }