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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a : K
n : ℤ
⊢ D (a ^ n) = n • a ^ (n - 1) • D a

Tactic:
by_cases hn : n = 0

Goal state after:
case pos
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a : K
n : ℤ
hn : n = 0
⊢ D (a ^ n) = n • a ^ (n - 1) • D a

case neg
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a : K
n : ℤ
hn : ¬n = 0
⊢ D (a ^ n) = n • a ^ (n - 1) • D a
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: case neg.inl
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a : K
n : ℤ
hn : ¬n = 0
ha : ¬a = 0
h : n = ↑n.natAbs
⊢ n.natAbs • a ^ (n.natAbs - 1) • D a = n.natAbs • a ^ (↑n.natAbs - 1) • D a

Tactic:
← zpow_natCast

Goal state after:
case neg.inl
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a : K
n : ℤ
hn : ¬n = 0
ha : ¬a = 0
h : n = ↑n.natAbs
⊢ n.natAbs • a ^ ↑(n.natAbs - 1) • D a = n.natAbs • a ^ (↑n.natAbs - 1) • D a
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
⊢ SetLike.coe '' Set.range basicOpen = Set.range fun r ↦ ↑(basicOpen r)

Tactic:
rw [← Set.range_comp]

Goal state after:
R : Type u
inst✝ : CommSemiring R
⊢ Set.range (SetLike.coe ∘ basicOpen) = Set.range fun r ↦ ↑(basicOpen r)
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
⊢ exponent G = 0 ↔ ∀ n > 0, ∃ g, g ^ n ≠ 1

Tactic:
by
  rw [exponent_eq_zero_iff, ExponentExists]
  push Not
  rfl

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
inst✝¹ : (i : ι) → CommRing (R i)
inst✝ : DecidableEq ι
i : ι
f : R i
⊢ comap (Pi.evalRingHom R i) '' ↑(basicOpen f) = ↑(basicOpen (Pi.single i f))

Tactic:
by
  ext p
  refine ⟨?_, ?_⟩
  · rintro ⟨p, hp, rfl⟩
    simpa
  · intro hp
    have : p ∈ Set.range (PrimeSpectrum.comap (Pi.evalRingHom R i)) := by
      rw [range_comap_of_surjective _ _ (RingHom.surjective _), mem_zeroLocus,
        SetLike.coe_subset_coe]
      intro x hx
      rw [RingHom.mem_ker, Pi.evalRingHom_apply] at hx
      have : Pi.single i f * x = 0 := by
        ext j
        by_cases h : i = j
        · subst h
          simp [hx]
        · simp [h]
      obtain (h | h) := Ideal.IsPrime.mem_or_mem_of_mul_eq_zero p.isPrime this <;> tauto
    obtain ⟨q, rfl⟩ := this
    exact ⟨q, by simpa using hp, by ext; simp⟩

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : DiscreteTopology (PrimeSpectrum R)
x : PiLocalization R
f : PrimeSpectrum R → R
hf✝ : ∀ (p : PrimeSpectrum R), ↑(basicOpen (f p)) = {p}
e : PrimeSpectrum R ≃ ↑(Set.range f) := Equiv.ofInjective f ⋯
loc : ∀ (a : ↑(Set.range f)), IsLocalization.AtPrime (Localization.Away ↑a) (e.symm a).asIdeal
algE : (a : ↑(Set.range f)) → Localization.AtPrime (e.symm a).asIdeal ≃ₐ[R] Localization.Away ↑a :=
  fun a ↦
    IsLocalization.algEquiv (e.symm a).asIdeal.primeCompl (Localization.AtPrime (e.symm a).asIdeal)
      (Localization.Away ↑a)
span_eq : Ideal.span (Set.range f) = ⊤
hf : ∀ (a : ↑(Set.range f)), ↑(basicOpen ↑a) = {e.symm a}
a b : ↑(Set.range f)
ne : a ≠ b
⊢ basicOpen (↑a * ↑b) = ⊥

Tactic:
simp_rw [basicOpen_mul, SetLike.ext'_iff, TopologicalSpace.Opens.coe_inf, hf]

Goal state after:
R : Type u
inst✝¹ : CommSemiring R
inst✝ : DiscreteTopology (PrimeSpectrum R)
x : PiLocalization R
f : PrimeSpectrum R → R
hf✝ : ∀ (p : PrimeSpectrum R), ↑(basicOpen (f p)) = {p}
e : PrimeSpectrum R ≃ ↑(Set.range f) := Equiv.ofInjective f ⋯
loc : ∀ (a : ↑(Set.range f)), IsLocalization.AtPrime (Localization.Away ↑a) (e.symm a).asIdeal
algE : (a : ↑(Set.range f)) → Localization.AtPrime (e.symm a).asIdeal ≃ₐ[R] Localization.Away ↑a :=
  fun a ↦
    IsLocalization.algEquiv (e.symm a).asIdeal.primeCompl (Localization.AtPrime (e.symm a).asIdeal)
      (Localization.Away ↑a)
span_eq : Ideal.span (Set.range f) = ⊤
hf : ∀ (a : ↑(Set.range f)), ↑(basicOpen ↑a) = {e.symm a}
a b : ↑(Set.range f)
ne : a ≠ b
⊢ {e.symm a} ∩ {e.symm b} = ↑⊥
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x : R
hx : x ∈ {e | IsIdempotentElem e}
y : R
hy : y ∈ {e | IsIdempotentElem e}
eq : basicOpen x = basicOpen y
⊢ x = y

Tactic:
by_contra! ne

Goal state after:
R : Type u
inst✝ : CommSemiring R
x : R
hx : x ∈ {e | IsIdempotentElem e}
y : R
hy : y ∈ {e | IsIdempotentElem e}
eq : basicOpen x = basicOpen y
ne : x ≠ y
⊢ False
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
h : IsCyclic α
⊢ ∃ g, orderOf g = Nat.card α

Tactic:
obtain ⟨g, hg⟩ := h.exists_generator

Goal state after:
α : Type u_1
inst✝ : Group α
h : IsCyclic α
g : α
hg : ∀ (x : α), x ∈ zpowers g
⊢ ∃ g, orderOf g = Nat.card α
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: case h
α : Type u_1
inst✝ : Group α
h : IsCyclic α
g : α
hg : ∀ (x : α), x ∈ zpowers g
⊢ Nat.card ↥(zpowers g) = Nat.card α

Tactic:
(eq_top_iff' (zpowers g)).mpr hg

Goal state after:
case h
α : Type u_1
inst✝ : Group α
h : IsCyclic α
g : α
hg : ∀ (x : α), x ∈ zpowers g
⊢ Nat.card ↥⊤ = Nat.card α
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst✝⁵ : Group α
inst✝⁴ : Group G
inst✝³ : Group G'
M : Type u_4
inst✝² : Monoid M
inst✝¹ : IsCyclic G
inst✝ : MulDistribMulAction M G
n✝ : ℕ
hn : Nat.card G = n✝
m n : M
g : G
hg : orderOf g = Nat.card G
⊢ (m * n) • g = m • n • g

Tactic:
mul_smul

Goal state after:
α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst✝⁵ : Group α
inst✝⁴ : Group G
inst✝³ : Group G'
M : Type u_4
inst✝² : Monoid M
inst✝¹ : IsCyclic G
inst✝ : MulDistribMulAction M G
n✝ : ℕ
hn : Nat.card G = n✝
m n : M
g : G
hg : orderOf g = Nat.card G
⊢ m • n • g = m • n • g
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: G : Type u_2
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsCyclic G
d : ℕ
a b : ZMod d
hGcard : Nat.card G = d
h : ∀ (t : G), t ^ a.val = t ^ b.val
⊢ a = b

Tactic:
obtain ⟨g, hg⟩ := IsCyclic.exists_generator (α := G)

Goal state after:
G : Type u_2
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsCyclic G
d : ℕ
a b : ZMod d
hGcard : Nat.card G = d
h : ∀ (t : G), t ^ a.val = t ^ b.val
g : G
hg : ∀ (x : G), x ∈ zpowers g
⊢ a = b
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case h
G : Type u
inst✝ : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range orderOf).Nonempty
hfin : (Set.range orderOf).Finite
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hp : Nat.Prime p
k : ℕ := (orderOf t).factorization p
hpe : k < (exponent G).factorization p
hk : k = (orderOf t).factorization p
g : G
hg : orderOf g = p ^ (exponent G).factorization p
⊢ orderOf t < orderOf (t ^ p ^ k * g)

Tactic:
have hpk : p ^ k ∣ orderOf t := Nat.ordProj_dvd _ _

Goal state after:
case h
G : Type u
inst✝ : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range orderOf).Nonempty
hfin : (Set.range orderOf).Finite
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hp : Nat.Prime p
k : ℕ := (orderOf t).factorization p
hpe : k < (exponent G).factorization p
hk : k = (orderOf t).factorization p
g : G
hg : orderOf g = p ^ (exponent G).factorization p
hpk : p ^ k ∣ orderOf t
⊢ orderOf t < orderOf (t ^ p ^ k * g)
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsLocalRing R
U : TopologicalSpace.Opens (PrimeSpectrum R)
⊢ closedPoint R ∈ U ↔ U = ⊤

Tactic:
by
  constructor
  · rw [eq_top_iff]
    exact fun h x _ => (specializes_closedPoint x).mem_open U.2 h
  · rintro rfl
    exact TopologicalSpace.Opens.mem_top _

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
⊢ Nat.card (Sylow p G) ≡ 1 [MOD p]

Tactic:
have : fixedPoints P.1 (Sylow p G) = {P} :=
    Set.ext fun Q : Sylow p G =>
      calc
        Q ∈ fixedPoints P (Sylow p G) ↔ P.1 ≤ Q := P.2.sylow_mem_fixedPoints_iff
        _ ↔ Q.1 = P.1 := ⟨P.3 Q.2, ge_of_eq⟩
        _ ↔ Q ∈ {P} := Sylow.ext_iff.symm.trans Set.mem_singleton_iff.symm

Goal state after:
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
this : fixedPoints (↥↑P) (Sylow p G) = {P}
⊢ Nat.card (Sylow p G) ≡ 1 [MOD p]
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: case refine_2
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : IsSimpleGroup α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
hα : orderOf g ≠ 1
n : ℕ
h : Subgroup.zpowers (g ^ n) = ⊤
⊢ n.Coprime (orderOf g)

Tactic:
simp only [Nat.coprime_iff_gcd_eq_one]

Goal state after:
case refine_2
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : IsSimpleGroup α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
hα : orderOf g ≠ 1
n : ℕ
h : Subgroup.zpowers (g ^ n) = ⊤
⊢ n.gcd (orderOf g) = 1
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: case refine_2
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : IsSimpleGroup α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
hα : orderOf g ≠ 1
n : ℕ
h : Subgroup.zpowers (g ^ n) = ⊤
⊢ n.Coprime (orderOf g)

Tactic:
simp only [Nat.coprime_iff_gcd_eq_one]
      have hgn : g ∈ Subgroup.zpowers (g ^ n) := by simp_all only [ne_eq, orderOf_eq_one_iff,
        Subgroup.mem_top]
      exact mem_zpowers_pow_iff.mp hgn

Goal state after:
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
inst✝ : CommMonoid G
x✝ : ↥(torsion G)
x : G
n : ℕ
npos : n > 0
hn : Function.IsPeriodicPt (fun x_1 ↦ x * x_1) n 1
⊢ ↑(⟨x, ⋯⟩ ^ n) * 1 = 1

Tactic:
_root_.mul_one,

Goal state after:
G : Type u_1
inst✝ : CommMonoid G
x✝ : ↥(torsion G)
x : G
n : ℕ
npos : n > 0
hn : Function.IsPeriodicPt (fun x_1 ↦ x * x_1) n 1
⊢ ↑(⟨x, ⋯⟩ ^ n) = 1
Module: Mathlib.RingTheory.Coprime.Ideal

Goal state before:
pp: case refine_2
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
⊢ ∀ (h : a ∉ t),
    t.Nonempty →
      ((∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤) →
        ((∃ μ, ∑ i ∈ Finset.cons a t h, ↑(μ i) = 1) ↔ (↑(Finset.cons a t h)).Pairwise fun i j ↦ I i ⊔ I j = ⊤)

Tactic:
hat

Goal state after:
case refine_2
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
⊢ t.Nonempty →
    ((∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤) →
      ((∃ μ, ∑ i ∈ Finset.cons a t hat, ↑(μ i) = 1) ↔ (↑(Finset.cons a t hat)).Pairwise fun i j ↦ I i ⊔ I j = ⊤)
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: case inr
G : Type u
inst✝³ : Group G
inst✝² : Finite G
hnc : ∀ (H : Subgroup G), IsCoatom H → H.Normal
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
K : Subgroup G
hK : IsCoatom K
hNK : normalizer ↑P ≤ K
this : K.Normal
hPK : ↑P ≤ K
⊢ normalizer ↑P ⊔ K = ⊤

Tactic:
P.normalizer_sup_eq_top' hPK

Goal state after:
case inr
G : Type u
inst✝³ : Group G
inst✝² : Finite G
hnc : ∀ (H : Subgroup G), IsCoatom H → H.Normal
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
K : Subgroup G
hK : IsCoatom K
hNK : normalizer ↑P ≤ K
this : K.Normal
hPK : ↑P ≤ K
⊢ ⊤ = ⊤
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: case refine_1
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x₁ x₂ y₁ y₂ : X
hsat₁ : IsMaximal (last s) x₁
hsat₂ : IsMaximal (last s) x₂
hsaty₁ : IsMaximal (snoc s x₁ hsat₁).last y₁
hsaty₂ : IsMaximal (snoc s x₂ hsat₂).last y₂
hr₁ : Iso (last s, x₁) (x₂, y₂)
hr₂ : Iso (x₁, y₁) (last s, x₂)
e : Fin (s.length + 1 + 1) ≃ Fin (s.length + 1 + 1) := Equiv.swap (Fin.last (s.length + 1)) (Fin.last s.length).castSucc
h1 : ∀ {i : Fin s.length}, i.castSucc.castSucc ≠ (Fin.last s.length).castSucc
h2 : ∀ {i : Fin s.length}, i.castSucc.castSucc ≠ Fin.last (s.length + 1)
i : Fin ((snoc s x₁ hsat₁).snoc y₁ hsaty₁).length
⊢ Iso (x₁, y₁) (s.toFun (Fin.last s.length), (snoc s x₂ hsat₂).toFun (Fin.last s.length.succ))

Tactic:
show (s.snoc _ hsat₂).toFun (Fin.last _) = x₂ from last_snoc _ _ _

Goal state after:
case refine_1
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x₁ x₂ y₁ y₂ : X
hsat₁ : IsMaximal (last s) x₁
hsat₂ : IsMaximal (last s) x₂
hsaty₁ : IsMaximal (snoc s x₁ hsat₁).last y₁
hsaty₂ : IsMaximal (snoc s x₂ hsat₂).last y₂
hr₁ : Iso (last s, x₁) (x₂, y₂)
hr₂ : Iso (x₁, y₁) (last s, x₂)
e : Fin (s.length + 1 + 1) ≃ Fin (s.length + 1 + 1) := Equiv.swap (Fin.last (s.length + 1)) (Fin.last s.length).castSucc
h1 : ∀ {i : Fin s.length}, i.castSucc.castSucc ≠ (Fin.last s.length).castSucc
h2 : ∀ {i : Fin s.length}, i.castSucc.castSucc ≠ Fin.last (s.length + 1)
i : Fin ((snoc s x₁ hsat₁).snoc y₁ hsaty₁).length
⊢ Iso (x₁, y₁) (s.toFun (Fin.last s.length), x₂)
Module: Mathlib.RingTheory.SimpleModule.Basic

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
f✝ : End (End R M) M
s : Finset M
x : ↥s →₀ M := Finsupp.equivFunOnFinite.symm fun x ↦ ↑x
w✝ : Submodule R (↥s →₀ M)
h : IsCompl (R ∙ x) w✝
p : (↥s →₀ M) →ₗ[R] ↥s →₀ M := (R ∙ x).projection w✝ h
f : End (End R (↥s →₀ M)) (↥s →₀ M) := (End.ringHomEndFinsupp ↥s) f✝
this : f (p • x) = f x
⊢ f x ∈ R ∙ x

Tactic:
by rw [← this, map_smul, End.smul_def]; apply projection_apply_mem

Goal state after:
Module: Mathlib.Algebra.Polynomial.Module.Basic

Goal state before:
pp: case neg
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_5
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
x y : PolynomialModule R M
r✝ r₁ r₂ : R
m m' m₁ m₂ m₁' m₂' : M
r : R[X]
n : ℕ
a : R
i : ℕ
hn : ¬n ≤ i
⊢ 0 = (r * (monomial n) a).coeff i

Tactic:
· rw [Polynomial.coeff_mul, Finset.sum_eq_zero]
      simp [Polynomial.coeff_monomial]
      lia

Goal state after:
Module: Mathlib.RingTheory.ReesAlgebra

Goal state before:
pp: case succ.refine_1
R : Type u
inst✝ : CommRing R
I : Ideal R
n : ℕ
hn : ∀ {r : R}, r ∈ I ^ n → (monomial n) r ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
r✝ : R
hr✝ : r✝ ∈ I * I ^ n
r : R
hr : r ∈ I
s : R
hs : s ∈ I ^ n
⊢ (monomial (1 + n)) (r * s) ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)

Tactic:
← monomial_mul_monomial

Goal state after:
case succ.refine_1
R : Type u
inst✝ : CommRing R
I : Ideal R
n : ℕ
hn : ∀ {r : R}, r ∈ I ^ n → (monomial n) r ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
r✝ : R
hr✝ : r✝ ∈ I * I ^ n
r : R
hr : r ∈ I
s : R
hs : s ∈ I ^ n
⊢ (monomial 1) r * (monomial n) s ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
Module: Mathlib.Algebra.Polynomial.Module.Basic

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : R[X]
q : PolynomialModule R M
⊢ (comp p) (p' • q) = p'.comp p • (comp p) q

Tactic:
rw [comp_apply, map_smul, eval_smul, Polynomial.comp, Polynomial.eval_map, comp_apply]
  rfl

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Nakayama

Goal state before:
pp: case insert.refine_2
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
i : M
s : Set M
a✝ : i ∉ s
hs✝ : s.Finite
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap ((LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) → ∃ r, r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0
r : R
hr1 : r - 1 ∈ I
hs : i ∈ ↑N ∧ s ⊆ ↑N
c : R
hc1 : c - 1 ∈ I
hci : c • i ∈ I • span R s
n : M
hn : n ∈ N
z : M
hz : z ∈ I • span R s
d : R
left✝ : d ∈ I
hyz : d • i + z = r • n
⊢ (d * c) • i + c • z ∈ I • span R s

Tactic:
mul_smul

Goal state after:
case insert.refine_2
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
i : M
s : Set M
a✝ : i ∉ s
hs✝ : s.Finite
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap ((LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) → ∃ r, r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0
r : R
hr1 : r - 1 ∈ I
hs : i ∈ ↑N ∧ s ⊆ ↑N
c : R
hc1 : c - 1 ∈ I
hci : c • i ∈ I • span R s
n : M
hn : n ∈ N
z : M
hz : z ∈ I • span R s
d : R
left✝ : d ∈ I
hyz : d • i + z = r • n
⊢ d • c • i + c • z ∈ I • span R s
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
i j k : ℕ
⊢ (I ^ k * I ^ i) • F.N j ≤ I ^ k • F.N (i + j)

Tactic:
mul_smul

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
i j k : ℕ
⊢ I ^ k • I ^ i • F.N j ≤ I ^ k • F.N (i + j)
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I✝ : Ideal R
F F' : I✝.Filtration M
I : Ideal R
N : Submodule R M
i : ℕ
⊢ (I ^ 1 * I ^ i) • N ≤ I ^ i • N

Tactic:
mul_smul

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I✝ : Ideal R
F F' : I✝.Filtration M
I : Ideal R
N : Submodule R M
i : ℕ
⊢ I ^ 1 • I ^ i • N ≤ I ^ i • N
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : I.Filtration M
r : ↥(reesAlgebra I)
f : PolynomialModule R M
hf : f ∈ {f | ∀ (i : ℕ), f.coeff i ∈ F.N i}
i j k : ℕ
e : (j, k) ∈ Finset.antidiagonal i
⊢ (↑r).coeff (j, k).1 • f.coeff (j, k).2 ∈ F.N i

Tactic:
rw [Finset.mem_antidiagonal] at e

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : I.Filtration M
r : ↥(reesAlgebra I)
f : PolynomialModule R M
hf : f ∈ {f | ∀ (i : ℕ), f.coeff i ∈ F.N i}
i j k : ℕ
e : (j, k).1 + (j, k).2 = i
⊢ (↑r).coeff (j, k).1 • f.coeff (j, k).2 ∈ F.N i
Module: Mathlib.Algebra.Category.ModuleCat.Differentials.Basic

Goal state before:
pp: A B : CommRingCat
f : A ⟶ B
M : ModuleCat ↑B
α β : KaehlerDifferential f ⟶ M
h : ∀ (b : ↑B), (ConcreteCategory.hom α) (d b) = (ConcreteCategory.hom β) (d b)
y : ↑B
⊢ (_root_.KaehlerDifferential.D ↑A ↑B) y ∈ ↑(ModuleCat.Hom.hom (α - β)).ker

Tactic:
rw [SetLike.mem_coe, LinearMap.mem_ker, ModuleCat.hom_sub, LinearMap.sub_apply, sub_eq_zero]

Goal state after:
A B : CommRingCat
f : A ⟶ B
M : ModuleCat ↑B
α β : KaehlerDifferential f ⟶ M
h : ∀ (b : ↑B), (ConcreteCategory.hom α) (d b) = (ConcreteCategory.hom β) (d b)
y : ↑B
⊢ (ModuleCat.Hom.hom α) ((_root_.KaehlerDifferential.D ↑A ↑B) y) =
    (ModuleCat.Hom.hom β) ((_root_.KaehlerDifferential.D ↑A ↑B) y)
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I : Ideal R
⊢ Function.Injective ⇑I.cotangentToQuotientSquare

Tactic:
rw [injective_iff_map_eq_zero]
  intro x hx
  obtain ⟨x, rfl⟩ := I.toCotangent_surjective x
  rw [toCotangent_to_quotient_square] at hx
  rwa [Ideal.toCotangent_eq_zero, ← Submodule.Quotient.mk_eq_zero (I ^ 2)]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S : Cᵒᵖ ⥤ CommRingCat
F : C ⥤ D
S' R : Dᵒᵖ ⥤ CommRingCat
M N : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
φ : S ⟶ F.op ⋙ R
φ' : S' ⟶ R
M' : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
d' : M'.Derivation' φ'
X Y : Dᵒᵖ
f : X ⟶ Y
b : ↑(R.obj X)
⊢ (ConcreteCategory.hom (d'.app Y).desc)
      ((ModuleCat.Hom.hom ((relativeDifferentials' φ').map f)) (CommRingCat.KaehlerDifferential.d b)) =
    (ModuleCat.Hom.hom (M'.map f)) ((d'.app X).d b)

Tactic:
Derivation'.app_apply

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S : Cᵒᵖ ⥤ CommRingCat
F : C ⥤ D
S' R : Dᵒᵖ ⥤ CommRingCat
M N : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
φ : S ⟶ F.op ⋙ R
φ' : S' ⟶ R
M' : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
d' : M'.Derivation' φ'
X Y : Dᵒᵖ
f : X ⟶ Y
b : ↑(R.obj X)
⊢ (ConcreteCategory.hom (d'.app Y).desc)
      ((ModuleCat.Hom.hom ((relativeDifferentials' φ').map f)) (CommRingCat.KaehlerDifferential.d b)) =
    (ModuleCat.Hom.hom (M'.map f)) (d'.d b)
Module: Mathlib.CategoryTheory.Monoidal.End

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{v_1, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
m n n' : M
g : n ⟶ n'
X : C
inst✝ : F.LaxMonoidal
⊢ (F.map g).app ((F.obj m).obj X) ≫ (μ F m n').app X = (μ F m n).app X ≫ (F.map (m ◁ g)).app X

Tactic:
by
  rw [← id_tensorHom, ← μ_naturality₂ F (𝟙 m) g X]
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
F : A → C ⥤ C
zero : F 0 ≅ 𝟭 C
add : (n m : A) → F (n + m) ≅ F n ⋙ F m
assoc_hom_app :
  ∀ (m₁ m₂ m₃ : A) (X : C),
    (add (m₁ + m₂) m₃).hom.app X ≫ (F m₃).map ((add m₁ m₂).hom.app X) =
      eqToHom ⋯ ≫ (add m₁ (m₂ + m₃)).hom.app X ≫ (add m₂ m₃).hom.app ((F m₁).obj X)
n : A
X : C
⊢ (F (0 + n)).obj X = (F n).obj ((𝟭 C).obj X)

Tactic:
dsimp; rw [zero_add]

Goal state after:
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
n : A
X : C
⊢ (h.F n).obj ((𝟭 C).obj X) = (h.F (0 + n)).obj X

Tactic:
dsimp; rw [zero_add]

Goal state after:
Module: Mathlib.Algebra.Homology.HomologicalComplex

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
X₁ : ι → V
d₁ : (i j : ι) → X₁ i ⟶ X₁ j
s₁ : ∀ (i j : ι), ¬c.Rel i j → d₁ i j = 0
h₁ : ∀ (i j k : ι), c.Rel i j → c.Rel j k → d₁ i j ≫ d₁ j k = 0
d₂ : (i j : ι) → X₁ i ⟶ X₁ j
s₂ : ∀ (i j : ι), ¬c.Rel i j → d₂ i j = 0
h₂ : ∀ (i j k : ι), c.Rel i j → c.Rel j k → d₂ i j ≫ d₂ j k = 0
h_d :
  ∀ (i j : ι),
    c.Rel i j →
      { X := X₁, d := d₁, shape := s₁, d_comp_d' := h₁ }.d i j ≫ eqToHom ⋯ =
        eqToHom ⋯ ≫ { X := X₁, d := d₂, shape := s₂, d_comp_d' := h₂ }.d i j
⊢ { X := X₁, d := d₁, shape := s₁, d_comp_d' := h₁ } = { X := X₁, d := d₂, shape := s₂, d_comp_d' := h₂ }

Tactic:
simp only [mk.injEq, heq_eq_eq, true_and]

Goal state after:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
X₁ : ι → V
d₁ : (i j : ι) → X₁ i ⟶ X₁ j
s₁ : ∀ (i j : ι), ¬c.Rel i j → d₁ i j = 0
h₁ : ∀ (i j k : ι), c.Rel i j → c.Rel j k → d₁ i j ≫ d₁ j k = 0
d₂ : (i j : ι) → X₁ i ⟶ X₁ j
s₂ : ∀ (i j : ι), ¬c.Rel i j → d₂ i j = 0
h₂ : ∀ (i j k : ι), c.Rel i j → c.Rel j k → d₂ i j ≫ d₂ j k = 0
h_d :
  ∀ (i j : ι),
    c.Rel i j →
      { X := X₁, d := d₁, shape := s₁, d_comp_d' := h₁ }.d i j ≫ eqToHom ⋯ =
        eqToHom ⋯ ≫ { X := X₁, d := d₂, shape := s₂, d_comp_d' := h₂ }.d i j
⊢ d₁ = d₂
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
⊢ ∀ {X Y : Discrete A} (f : X ⟶ Y) (X' : Discrete A),
    MonoidalCategoryStruct.whiskerRight ((Discrete.functor h.F).map f) ((Discrete.functor h.F).obj X') ≫
        (h.add Y.as X'.as).symm.hom =
      (h.add X.as X'.as).symm.hom ≫ (Discrete.functor h.F).map (MonoidalCategoryStruct.whiskerRight f X')

Tactic:
by
        rintro ⟨X⟩ ⟨Y⟩ ⟨⟨⟨rfl⟩⟩⟩ ⟨X'⟩
        ext
        simp

Goal state after: