mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
h : IsClosedMap (comap (mapRingHom f))
algInst✝ : Algebra R S := f.toAlgebra
a✝¹ : Nontrivial R
a✝ : Nontrivial S
r : S
p : S[X] := C r * X - 1
this✝ : 1 ∈ Ideal.span {X} ⊔ Ideal.comap (mapRingHom f) (Ideal.span {p})
a b : R[X]
hb : b ∈ Ideal.comap (mapRingHom f) (Ideal.span {p})
e : a * X + b = 1
c : S[X]
hc : map (algebraMap R S) b = p * c
this : p.natDegree ≤ 1
⊢ 1 ≤ b.natDegree + 1

Tactic:
by simp

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝ : Group G
Hs : Set (Subgroup G)
h : ∀ H ∈ Hs, IsPGroup p ↥H
hn : ∀ H ∈ Hs, H.Normal
⊢ IsPGroup p ↥(sSup Hs)

Tactic:
rw [sSup_eq_iSup]
  exact biSup_of_normal Hs id h hn

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
h : IsClosedMap (comap (mapRingHom f))
algInst✝ : Algebra R S := f.toAlgebra
a✝¹ : Nontrivial R
a✝ : Nontrivial S
r : S
p : S[X] := C r * X - 1
this✝ : 1 ∈ Ideal.span {X} ⊔ Ideal.comap (mapRingHom f) (Ideal.span {p})
a b : R[X]
hb : b ∈ Ideal.comap (mapRingHom f) (Ideal.span {p})
e : a * X + b = 1
c : S[X]
hc : map (algebraMap R S) b = p * c
this : p.natDegree ≤ 1
⊢ (C r).natDegree ≤ b.natDegree

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
h : IsClosedMap (comap (mapRingHom f))
algInst✝ : Algebra R S := f.toAlgebra
a✝¹ : Nontrivial R
a✝ : Nontrivial S
r : S
p : S[X] := C r * X - 1
this✝ : 1 ∈ Ideal.span {X} ⊔ Ideal.comap (mapRingHom f) (Ideal.span {p})
a b : R[X]
hb : b ∈ Ideal.comap (mapRingHom f) (Ideal.span {p})
e : a * X + b = 1
c : S[X]
hc : map (algebraMap R S) b = p * c
this : p.natDegree ≤ 1
⊢ X.natDegree ≤ 1

Tactic:
by simp

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
⊢ e + (1 - e) = 1

Tactic:
by simp

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: case inr
α : Type u_1
inst✝ : Group α
this✝ : Finite α
this : Nontrivial α
h_cyc : IsCyclic α
hp : Nat.Prime 1
hα : Nat.card α = 1 ^ 2
h_exp : exponent α = 1
⊢ False

Tactic:
· exact Nat.not_prime_one hp

Goal state after:
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : CommMonoid G
inst✝ : CommMonoid H
p : ℕ
⊢ 1 ^ p ^ 0 = 1

Tactic:
by simp

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
inst✝² : Finite G
G' : Type u_2
inst✝¹ : Group G'
f : G →* G'
hf : Function.Surjective ⇑f
p : ℕ
inst✝ : Fact (Nat.Prime p)
this : Finite G'
P : Sylow p G'
Q₀ : Sylow p ↥(comap f ↑P) := ⋯.some
Q : Subgroup G := map (comap f ↑P).subtype ↑Q₀
hPQ : map f Q ≤ ↑P
hpQ : IsPGroup p ↥Q
⊢ ∃ a, mapSurjective hf a = P

Tactic:
have hQ : ¬ p ∣ Q.index := by
    rw [Subgroup.index_map_subtype Q₀.1, P.index_comap_of_surjective hf]
    exact Nat.Prime.not_dvd_mul Fact.out Q₀.not_dvd_index P.not_dvd_index

Goal state after:
G : Type u_1
inst✝³ : Group G
inst✝² : Finite G
G' : Type u_2
inst✝¹ : Group G'
f : G →* G'
hf : Function.Surjective ⇑f
p : ℕ
inst✝ : Fact (Nat.Prime p)
this : Finite G'
P : Sylow p G'
Q₀ : Sylow p ↥(comap f ↑P) := ⋯.some
Q : Subgroup G := map (comap f ↑P).subtype ↑Q₀
hPQ : map f Q ≤ ↑P
hpQ : IsPGroup p ↥Q
hQ : ¬p ∣ Q.index
⊢ ∃ a, mapSurjective hf a = P
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : HasDistribNeg M
⊢ (-1) ^ 2 = 1

Tactic:
by simp

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝¹ : Group G
H : Subgroup G
inst✝ : Finite ↑↑H
x✝ y✝ : ↥(normalizer ↑H)
⊢ x✝⁻¹ * y✝ ∈ comap (normalizer H.carrier).subtype H ↔ (leftRel H) ↑x✝ ↑y✝

Tactic:
leftRel_apply

Goal state after:
G : Type u
inst✝¹ : Group G
H : Subgroup G
inst✝ : Finite ↑↑H
x✝ y✝ : ↥(normalizer ↑H)
⊢ x✝⁻¹ * y✝ ∈ comap (normalizer H.carrier).subtype H ↔ (↑x✝)⁻¹ * ↑y✝ ∈ H
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 : ι
⊢ ∀ (s : Finset ι) (h : a ∉ s),
    s.Nonempty →
      ((∃ μ, ∑ i ∈ s, ↑(μ i) = 1) ↔ (↑s).Pairwise fun i j ↦ I i ⊔ I j = ⊤) →
        ((∃ μ, ∑ i ∈ Finset.cons a s h, ↑(μ i) = 1) ↔ (↑(Finset.cons a s h)).Pairwise fun i j ↦ I i ⊔ I j = ⊤)

Tactic:
t

Goal state after:
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 = ⊤)
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: case refine_1.inl.inr
M : Type u_4
N : Type u_5
inst✝¹ : Group M
inst✝ : Group N
h : IsCyclic (M × N)
h✝¹ : Infinite M
h✝ : Nontrivial N
⊢ (Nat.card M).Coprime (Nat.card N)

Tactic:
exact (not_isCyclic_prod_of_infinite_nontrivial M N h).elim

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝¹ : Group G
inst✝ : Finite G
hn : ∀ {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G), (↑P).Normal
this✝ : Fintype G
ps : Finset ℕ := (Nat.card G).primeFactors
P : (p : ℕ) → Sylow p G := default
this : (p : ℕ) → Fintype ↥↑(P p)
hcomm : _root_.Pairwise fun p₁ p₂ ↦ ∀ (x y : G), x ∈ P ↑p₁ → y ∈ P ↑p₂ → Commute x y
⊢ ∏ p, Nat.card ↥↑(P ↑p) = ∏ p, ↑p ^ (Nat.card G).factorization ↑p

Tactic:
congr 1 with ⟨p, hp⟩

Goal state after:
case e_f
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
hn : ∀ {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G), (↑P).Normal
this✝ : Fintype G
ps : Finset ℕ := (Nat.card G).primeFactors
P : (p : ℕ) → Sylow p G := default
this : (p : ℕ) → Fintype ↥↑(P p)
hcomm : _root_.Pairwise fun p₁ p₂ ↦ ∀ (x y : G), x ∈ P ↑p₁ → y ∈ P ↑p₂ → Commute x y
p : ℕ
hp : p ∈ ps
⊢ Nat.card ↥↑(P ↑⟨p, hp⟩) = ↑⟨p, hp⟩ ^ (Nat.card G).factorization ↑⟨p, hp⟩
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i : Fin (s.length + 1)
hx : s.toFun i ≠ last s
hi : ↑i < (s.length - 1).succ
⊢ (eraseLast s).toFun ⟨↑i, hi⟩ = s.toFun i

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: 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
⊢ ∀ {i : Fin s.length}, i.castSucc.castSucc ≠ (Fin.last s.length).castSucc

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: 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
⊢ ∀ {i : Fin s.length}, i.castSucc.castSucc ≠ Fin.last (s.length + 1)

Tactic:
by simp

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

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
m : M
h : m ≠ 0
r : R
hr : r ∈ torsionOf R M m
⊢ r = 0

Tactic:
rw [mem_torsionOf_iff, smul_eq_zero] at hr
    tauto

Goal state after:
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
n : ℕ
ih :
  ∀ (s : CompositionSeries X) (x : X) (hm : IsMaximal x (last s)),
    head s ≤ x →
      s.length = n → ∃ t, head t = head s ∧ t.length + 1 = n ∧ ∃ (htx : last t = x), s.Equivalent (snoc t (last s) ⋯)
s : CompositionSeries X
x : X
hm : IsMaximal x (last s)
hb : head s ≤ x
hn : s.length = n + 1
h0s : 0 < s.length
hetx : ¬(eraseLast s).last = x
imxs : IsMaximal (x ⊓ (eraseLast s).last) (eraseLast s).last
t : CompositionSeries X
htb : head t = (eraseLast s).head
htl : t.length + 1 = n
htt : last t = x ⊓ (eraseLast s).last
hteqv : Equivalent (eraseLast s) (snoc t (eraseLast s).last ⋯)
hmtx : IsMaximal (last t) x
⊢ (snoc t x hmtx).last = x

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
A : Type u_3
M : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
a : A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower R A M
t : R
m : AEval R M a
⊢ (of R M a).symm (C t • m) = (of R M a).symm (t • m)

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: case succ
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
n : ℕ
ih : ∀ (s₁ s₂ : CompositionSeries X), head s₁ = head s₂ → last s₁ = last s₂ → s₁.length = n → s₁.Equivalent s₂
s₁ s₂ : CompositionSeries X
hb : head s₁ = head s₂
ht : last s₁ = last s₂
hle : s₁.length = n + 1
h0s₂ : 0 < s₂.length
t : CompositionSeries X
htb : head t = head s₁
htl : t.length + 1 = s₁.length
htt : last t = (eraseLast s₂).last
hteq : s₁.Equivalent (snoc t (last s₁) ⋯)
this : t.Equivalent (eraseLast s₂)
⊢ s₁.Equivalent s₂

Tactic:
refine hteq.trans ?_

Goal state after:
case succ
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
n : ℕ
ih : ∀ (s₁ s₂ : CompositionSeries X), head s₁ = head s₂ → last s₁ = last s₂ → s₁.length = n → s₁.Equivalent s₂
s₁ s₂ : CompositionSeries X
hb : head s₁ = head s₂
ht : last s₁ = last s₂
hle : s₁.length = n + 1
h0s₂ : 0 < s₂.length
t : CompositionSeries X
htb : head t = head s₁
htl : t.length + 1 = s₁.length
htt : last t = (eraseLast s₂).last
hteq : s₁.Equivalent (snoc t (last s₁) ⋯)
this : t.Equivalent (eraseLast s₂)
⊢ Equivalent (snoc t (last s₁) ⋯) s₂
Module: Mathlib.Algebra.Polynomial.Module.AEval

Goal state before:
pp: R : Type ?u.5
A : Type ?u.7
M : Type ?u.13
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
a : A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower R A M
q : Submodule R[X] (AEval R M a)
m : M
hm : m ∈ (Submodule.orderIsoMapComap (of R M a)).symm (Submodule.restrictScalars R q)
⊢ m ∈
    Submodule.comap ((Algebra.lsmul R R M) a)
      ((Submodule.orderIsoMapComap (of R M a)).symm (Submodule.restrictScalars R q))

Tactic:
by
    simpa [← X_smul_of] using! q.smul_mem (X : R[X]) hm

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

Goal state before:
pp: case insert
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
hrn : N ≤ comap ((LinearMap.lsmul R M) r) (I • span R (insert i s))
hs : insert i s ⊆ ↑N
⊢ ∃ r, r - 1 ∈ I ∧ N ≤ comap ((LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N

Tactic:
rw [← Set.singleton_union, span_union, smul_sup] at hrn

Goal state after:
case insert
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
hrn : N ≤ comap ((LinearMap.lsmul R M) r) (I • (R ∙ i) ⊔ I • span R s)
hs : insert i s ⊆ ↑N
⊢ ∃ r, r - 1 ∈ I ∧ N ≤ comap ((LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N
Module: Mathlib.Algebra.Polynomial.Module.AEval

Goal state before:
pp: R : Type ?u.5
A : Type ?u.7
M : Type ?u.13
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
a : A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower R A M
p : Submodule R M
hp : p ∈ ((Algebra.lsmul R R M) a).invtSubmodule
x : ↥p
⊢ (of R M a) ↑x ∈ (mapSubmodule R M a) ⟨p, hp⟩

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
⊢ ↑(torsion R M) = {x | (R ∙ x).annihilator ≠ ⊥}

Tactic:
ext x; simp_rw [Submodule.ne_bot_iff, mem_annihilator, mem_span_singleton]
  exact
    ⟨fun ⟨a, hax⟩ =>
      ⟨a, fun _ ⟨b, hb⟩ => by rw [← hb, smul_comm, ← Submonoid.smul_def, hax, smul_zero],
        nonZeroDivisors.coe_ne_zero _⟩,
      fun ⟨a, hax, ha⟩ => ⟨⟨_, mem_nonZeroDivisors_of_ne_zero ha⟩, hax x ⟨1, one_smul _ _⟩⟩⟩

Goal state after:
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
h : ∃ n₀, ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀
n : ℕ
hn : n ≥ h.choose
⊢ (I * I ^ (n - h.choose)) • F.N h.choose = I ^ (n + 1 - h.choose) • F.N h.choose

Tactic:
← pow_succ',

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
h : ∃ n₀, ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀
n : ℕ
hn : n ≥ h.choose
⊢ I ^ (n - h.choose + 1) • F.N h.choose = I ^ (n + 1 - h.choose) • F.N h.choose
Module: Mathlib.Algebra.Category.ModuleCat.Differentials.Basic

Goal state before:
pp: A B A' B' : CommRingCat
f : A ⟶ B
f' : A' ⟶ B'
g : A ⟶ A'
g' : B ⟶ B'
fac : g ≫ f' = f ≫ g'
this : Algebra ↑A ↑B := (Hom.hom f).toAlgebra
⊢ ∀ (b b' : ↑B),
    (_root_.KaehlerDifferential.D ↑A ↑B) (b + b') =
      (_root_.KaehlerDifferential.D ↑A ↑B) b + (_root_.KaehlerDifferential.D ↑A ↑B) b'

Tactic:
by simp

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

Goal state before:
pp: A B A' B' : CommRingCat
f : A ⟶ B
f' : A' ⟶ B'
g : A ⟶ A'
g' : B ⟶ B'
fac : g ≫ f' = f ≫ g'
this : Algebra ↑A ↑B := (Hom.hom f).toAlgebra
⊢ ∀ (b b' : ↑B),
    (_root_.KaehlerDifferential.D ↑A ↑B) (b * b') =
      b • (_root_.KaehlerDifferential.D ↑A ↑B) b' + b' • (_root_.KaehlerDifferential.D ↑A ↑B) b

Tactic:
by simp

Goal state after:
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)
⊢ ⊤ ≤ (ModuleCat.Hom.hom (α - β)).ker

Tactic:
← KaehlerDifferential.span_range_derivation,

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)
⊢ Submodule.span (↑B) (Set.range ⇑(_root_.KaehlerDifferential.D ↑A ↑B)) ≤ (ModuleCat.Hom.hom (α - β)).ker
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: case mpr.zero
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
n₀ : ℕ
F' : Submodule (↥(reesAlgebra I)) (PolynomialModule R M) :=
  Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i))
hF : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
this : ∀ i ≤ n₀, single R i '' ↑(F.N i) ⊆ ↑F'
⊢ single R 0 '' ↑(F.N 0) ⊆ ↑(Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i)))

Tactic:
exact this _ zero_le

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

Goal state before:
pp: A B A' B' : CommRingCat
f : A ⟶ B
f' : A' ⟶ B'
g : A ⟶ A'
g' : B ⟶ B'
fac : g ≫ f' = f ≫ g'
this✝⁵ : Algebra ↑A ↑B := (Hom.hom f).toAlgebra
this✝⁴ : Algebra ↑A' ↑B' := (Hom.hom f').toAlgebra
this✝³ : Algebra ↑A ↑A' := (Hom.hom g).toAlgebra
this✝² : Algebra ↑B ↑B' := (Hom.hom g').toAlgebra
this✝¹ : Algebra ↑A ↑B' := (Hom.hom (g ≫ f')).toAlgebra
this✝ : IsScalarTower ↑A ↑A' ↑B'
this : IsScalarTower ↑A ↑B ↑B'
⊢ ∀ (x y : Ω[↑B⁄↑A]),
    (_root_.KaehlerDifferential.map ↑A ↑A' ↑B ↑B') (x + y) =
      (_root_.KaehlerDifferential.map ↑A ↑A' ↑B ↑B') x + (_root_.KaehlerDifferential.map ↑A ↑A' ↑B ↑B') y

Tactic:
by simp

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

Goal state before:
pp: A B A' B' : CommRingCat
f : A ⟶ B
f' : A' ⟶ B'
g : A ⟶ A'
g' : B ⟶ B'
fac : g ≫ f' = f ≫ g'
this✝⁵ : Algebra ↑A ↑B := (Hom.hom f).toAlgebra
this✝⁴ : Algebra ↑A' ↑B' := (Hom.hom f').toAlgebra
this✝³ : Algebra ↑A ↑A' := (Hom.hom g).toAlgebra
this✝² : Algebra ↑B ↑B' := (Hom.hom g').toAlgebra
this✝¹ : Algebra ↑A ↑B' := (Hom.hom (g ≫ f')).toAlgebra
this✝ : IsScalarTower ↑A ↑A' ↑B'
this : IsScalarTower ↑A ↑B ↑B'
⊢ ∀ (m : ↑B) (x : Ω[↑B⁄↑A]),
    (_root_.KaehlerDifferential.map ↑A ↑A' ↑B ↑B') (m • x) =
      (RingHom.id ↑B) m • (_root_.KaehlerDifferential.map ↑A ↑A' ↑B ↑B') x

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: case refine_1
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
x y : ↥I
e :
  ↑((fun c ↦ ⟨I.cotangentToQuotientSquare c, ⋯⟩) (I.toCotangent x)) =
    ↑((fun c ↦ ⟨I.cotangentToQuotientSquare c, ⋯⟩) (I.toCotangent y))
⊢ I.toCotangent x = I.toCotangent y

Tactic:
rw [I.toCotangent_eq]

Goal state after:
case refine_1
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
x y : ↥I
e :
  ↑((fun c ↦ ⟨I.cotangentToQuotientSquare c, ⋯⟩) (I.toCotangent x)) =
    ↑((fun c ↦ ⟨I.cotangentToQuotientSquare c, ⋯⟩) (I.toCotangent y))
⊢ ↑x - ↑y ∈ I ^ 2
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: case refine_2
R : Type u
S : Type v
S' : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : CommSemiring S'
inst✝⁶ : Algebra S' R
inst✝⁵ : Algebra S S'
inst✝⁴ : IsScalarTower S S' R
I : Ideal R
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I₁ : Ideal A
I₂ : Ideal B
f : A →ₐ[R] B
h : I₁ ≤ comap f I₂
⊢ Submodule.restrictScalars R (I₁ • ⊤) ≤
    Submodule.comap (f.toLinearMap.restrict h) (Submodule.restrictScalars R (I₂ • ⊤))

Tactic:
· intro x hx
    rw [Submodule.restrictScalars_mem] at hx
    refine Submodule.smul_induction_on hx ?_ (fun _ _ ↦ add_mem)
    rintro a ha ⟨b, hb⟩ -
    simp only [SetLike.mk_smul_mk, smul_eq_mul, Submodule.mem_comap, Submodule.restrictScalars_mem]
    convert!
      (Submodule.smul_mem_smul (M := I₂) (r := f a) (n := ⟨f b, h hb⟩) (h ha)
        (Submodule.mem_top)) using 1
    ext
    exact map_mul f a b

Goal state after:
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
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
x : M
N : Submodule R M := ⨅ i, I ^ i • ⊤
k : ℕ
⊢ I ^ k • ⊤ = (I.stableFiltration ⊤).N k

Tactic:
by simp

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
d : (X : Dᵒᵖ) → (M.obj X).Derivation (φ'.app X)
d_map :
  ∀ ⦃X Y : Dᵒᵖ⦄ (f : X ⟶ Y) (x : ↑(R.obj X)),
    (d Y).d ((ConcreteCategory.hom (R.map f)) x) = (ConcreteCategory.hom (M.map f)) ((d X).d x)
X : Dᵒᵖ
⊢ ∀ (a b : ↑(R.obj X)), (d X).d (a + b) = (d X).d a + (d X).d b

Tactic:
by simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
X Y : Cᵒᵖ
f : X ⟶ Y
r : ↑(R.obj X)
m : ↑(M.obj X)
⊢ (ConcreteCategory.hom (M.map f)) (r • m) = (ConcreteCategory.hom (R.map f)) r • (ConcreteCategory.hom (M.map f)) m

Tactic:
by simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M M₁ M₂ : PresheafOfModules R
X✝ Y✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
⊢ ∀ (a b : ↑((forget₂ (ModuleCat ↑(R.obj X✝)) Ab).1 (M.obj X✝))),
    (ConcreteCategory.hom (M.map f)) (a + b) = (ConcreteCategory.hom (M.map f)) a + (ConcreteCategory.hom (M.map f)) b

Tactic:
by simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M M₁ M₂ X✝ Y✝ : PresheafOfModules R
f : X✝ ⟶ Y✝
X : Cᵒᵖ
⊢ ∀ (a b : ↑(X✝.obj X)),
    (ConcreteCategory.hom (f.app X)) (a + b) = (ConcreteCategory.hom (f.app X)) a + (ConcreteCategory.hom (f.app X)) b

Tactic:
by simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M✝ M₁ M₂ : PresheafOfModules R
M : Cᵒᵖ ⥤ Ab
inst✝ : (X : Cᵒᵖ) → Module ↑(R.obj X) ↑(M.obj X)
map_smul :
  ∀ ⦃X Y : Cᵒᵖ⦄ (f : X ⟶ Y) (r : ↑(R.obj X)) (m : ↑(M.obj X)),
    (ConcreteCategory.hom (M.map f)) (r • m) = (ConcreteCategory.hom (R.map f)) r • (ConcreteCategory.hom (M.map f)) m
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ ∀ (x y : ↑(M.obj X)),
    (ConcreteCategory.hom (M.map f)) (x + y) = (ConcreteCategory.hom (M.map f)) x + (ConcreteCategory.hom (M.map f)) y

Tactic:
by simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M M₁ M₂ : PresheafOfModules R
⊢ ∀ (a : M₁ ⟶ M₂), 0 + a = a

Tactic:
by intros; ext1; simp only [add_app, zero_app, zero_add]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M₁ M₂ : PresheafOfModules R
n : ℤ
f : M₁ ⟶ M₂
X : Cᵒᵖ
⊢ (n • f).app X = n • f.app X

Tactic:
by
  ext x
  change (toPresheaf R ⋙ (evaluation _ _).obj X).map (n • f) x = _
  rw [Functor.map_zsmul]
  rfl

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M M₁ M₂ : PresheafOfModules R
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ ∀ (x y : ↑(R.obj X)),
    (ConcreteCategory.hom (R.map f)) (x + y) = (ConcreteCategory.hom (R.map f)) x + (ConcreteCategory.hom (R.map f)) y

Tactic:
by simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M✝ M₁ M₂ : PresheafOfModules R
X : Cᵒᵖ
hX : Limits.IsInitial X
M : PresheafOfModules R
Y Z : Cᵒᵖ
f : Y ⟶ Z
⊢ ∀ (x y : ↑(forgetToPresheafModuleCatObjObj X hX M Y)),
    (ConcreteCategory.hom (M.map f)) (x + y) = (ConcreteCategory.hom (M.map f)) x + (ConcreteCategory.hom (M.map f)) y

Tactic:
by simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M✝ M₁ M₂ : PresheafOfModules R
X✝ : Cᵒᵖ
hX✝ : Limits.IsInitial X✝
X : Cᵒᵖ
hX : Limits.IsInitial X
M N : PresheafOfModules R
f : M ⟶ N
Y : Cᵒᵖ
⊢ ∀ (x y : ↑((forgetToPresheafModuleCatObj X hX M).obj Y)),
    (ConcreteCategory.hom (f.app Y)) (x + y) = (ConcreteCategory.hom (f.app Y)) x + (ConcreteCategory.hom (f.app Y)) y

Tactic:
by simp

Goal state after: