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

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
I : Ideal S
hZ : IsClosed (zeroLocus ↑I)
hf : StableUnderSpecialization (comap f '' zeroLocus ↑I)
p : PrimeSpectrum R
hp : p ∈ zeroLocus ↑(Ideal.comap f I)
⊢ p ∈ comap f '' zeroLocus ↑I

Tactic:
obtain ⟨q, hqI, hq, hqle⟩ := p.asIdeal.exists_ideal_comap_le_prime I hp

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
I : Ideal S
hZ : IsClosed (zeroLocus ↑I)
hf : StableUnderSpecialization (comap f '' zeroLocus ↑I)
p : PrimeSpectrum R
hp : p ∈ zeroLocus ↑(Ideal.comap f I)
q : Ideal S
hqI : q ≥ I
hq : q.IsPrime
hqle : Ideal.comap f q ≤ p.asIdeal
⊢ p ∈ comap f '' zeroLocus ↑I
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
h₁ : Function.Surjective (comap f)
h₂ : GeneralizingMap (comap f)
⊢ IsQuotientMap (comap f)

Tactic:
rw [Topology.isQuotientMap_iff_isClosed]
  refine ⟨h₁, fun s ↦ ⟨fun hs ↦ hs.preimage (continuous_comap f),
    fun hsc ↦ Set.image_preimage_eq s h₁ ▸ ?_⟩⟩
  apply isClosed_image_of_stableUnderSpecialization _ _ hsc
  rw [Set.image_preimage_eq s h₁, ← stableUnderGeneralization_compl_iff]
  convert! h₂.stableUnderGeneralization_image hsc.isOpen_compl.stableUnderGeneralization
  rw [← Set.preimage_compl, Set.image_preimage_eq _ h₁]

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case refine_3
G : Type u_1
inst✝¹ : Monoid G
inst✝ : Nontrivial G
p : ℕ
hp : Nat.Prime p
h : ∀ (g : G), g ≠ 1 → orderOf g = p
⊢ p ∣ exponent G

Tactic:
obtain ⟨g, hg⟩ := exists_ne (1 : G)

Goal state after:
case refine_3
G : Type u_1
inst✝¹ : Monoid G
inst✝ : Nontrivial G
p : ℕ
hp : Nat.Prime p
h : ∀ (g : G), g ≠ 1 → orderOf g = p
g : G
hg : g ≠ 1
⊢ p ∣ exponent G
Module: Mathlib.Algebra.Module.ZMod

Goal state before:
pp: n : ℕ
M : Type u_1
M₁ : Type u_2
inst✝¹ : NeZero n
inst✝ : AddCommMonoid M
h : ∀ (x : M), n • x = 0
c : ℕ
x : M
⊢ (c % n) • x = c • x

Tactic:
suffices (c % n + c / n * n) • x = c • x by rwa [add_nsmul, mul_nsmul, h, add_zero] at this

Goal state after:
n : ℕ
M : Type u_1
M₁ : Type u_2
inst✝¹ : NeZero n
inst✝ : AddCommMonoid M
h : ∀ (x : M), n • x = 0
c : ℕ
x : M
⊢ (c % n + c / n * n) • x = c • x
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: α : Type u_1
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → #{a | a ^ n = 1} ≤ n
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : {a | orderOf a = d} = ∅
⊢ c = #{x | x ^ c = 1}

Tactic:
apply congr_arg card

Goal state after:
α : Type u_1
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → #{a | a ^ n = 1} ≤ n
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := ⋯
hc0 : 0 < c
h0 : {a | orderOf a = d} = ∅
⊢ univ = {x | x ^ c = 1}
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: T : Type u
inst✝¹ : CommRing T
inst✝ : IsLocalRing T
x : PrimeSpectrum (ResidueField T)
⊢ PrimeSpectrum.comap (residue T) x = closedPoint T

Tactic:
rw [Subsingleton.elim x ⊥]

Goal state after:
T : Type u
inst✝¹ : CommRing T
inst✝ : IsLocalRing T
x : PrimeSpectrum (ResidueField T)
⊢ PrimeSpectrum.comap (residue T) ⊥ = closedPoint T
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
⊢ ↑((fun x_1 ↦ ⟨x, ⋯⟩ * x_1)^[n] 1) = ↑1

Tactic:
dsimp

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
⊢ ↑((fun x_1 ↦ ⟨x, ⋯⟩ * x_1)^[n] 1) = 1
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝² : Group G
hp : Fact (Nat.Prime p)
P : Sylow p G
inst✝¹ : (↑P).Normal
inst✝ : (↑P).FiniteIndex
h✝ : p ∣ Nat.card (G ⧸ ↑P)
x : G ⧸ ↑P
hx : orderOf x = p
h : IsPGroup p ↥(zpowers x)
Q : Subgroup G := comap (QuotientGroup.mk' ↑P) (zpowers x)
hQ : IsPGroup p ↥Q
⊢ False

Tactic:
replace hp := mt orderOf_eq_one_iff.mpr (ne_of_eq_of_ne hx hp.1.ne_one)

Goal state after:
p : ℕ
G : Type u_1
inst✝² : Group G
P : Sylow p G
inst✝¹ : (↑P).Normal
inst✝ : (↑P).FiniteIndex
h✝ : p ∣ Nat.card (G ⧸ ↑P)
x : G ⧸ ↑P
hx : orderOf x = p
h : IsPGroup p ↥(zpowers x)
Q : Subgroup G := comap (QuotientGroup.mk' ↑P) (zpowers x)
hQ : IsPGroup p ↥Q
hp : ¬x = 1
⊢ False
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝² : Group G
P : Sylow p G
inst✝¹ : (↑P).Normal
inst✝ : (↑P).FiniteIndex
h✝ : p ∣ Nat.card (G ⧸ ↑P)
x : G ⧸ ↑P
hx : orderOf x = p
h : IsPGroup p ↥(zpowers x)
Q : Subgroup G := comap (QuotientGroup.mk' ↑P) (zpowers x)
hQ : IsPGroup p ↥Q
hp : ¬x = 1
⊢ False

Tactic:
← zpowers_eq_bot,

Goal state after:
p : ℕ
G : Type u_1
inst✝² : Group G
P : Sylow p G
inst✝¹ : (↑P).Normal
inst✝ : (↑P).FiniteIndex
h✝ : p ∣ Nat.card (G ⧸ ↑P)
x : G ⧸ ↑P
hx : orderOf x = p
h : IsPGroup p ↥(zpowers x)
Q : Subgroup G := comap (QuotientGroup.mk' ↑P) (zpowers x)
hQ : IsPGroup p ↥Q
hp : ¬zpowers x = ⊥
⊢ False
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_2
inst✝¹ : Group G
inst✝ : Finite G
h : IsCyclic G
⊢ Nat.card (MulAut G) = (Nat.card G).totient

Tactic:
by
  rw [← ZMod.card_units_eq_totient, ← Nat.card_eq_fintype_card]
  exact Nat.card_congr (mulAutMulEquiv G)

Goal state after:
Module: Mathlib.Order.CompactlyGenerated.Intervals

Goal state before:
pp: case refine_2
ι : Type u_1
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
x✝ : ↑(Iic a)
s : Set α
hs : ∀ x ∈ s, IsCompactElement x
hx✝ : sSup s ≤ a
hx : ∀ b ∈ s, b ≤ a
f : ↑s → ↑(Iic a) := fun y ↦ ⟨↑y, ⋯⟩
⊢ sSup (range f) = ⟨sSup s, hx✝⟩

Tactic:
rw [Subtype.ext_iff]

Goal state after:
case refine_2
ι : Type u_1
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
x✝ : ↑(Iic a)
s : Set α
hs : ∀ x ∈ s, IsCompactElement x
hx✝ : sSup s ≤ a
hx : ∀ b ∈ s, b ≤ a
f : ↑s → ↑(Iic a) := fun y ↦ ⟨↑y, ⋯⟩
⊢ ↑(sSup (range f)) = ↑⟨sSup s, hx✝⟩
Module: Mathlib.Order.CompactlyGenerated.Intervals

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
s : Set ι
f : ι → α
h : ∀ i ∈ s, ComplementedLattice ↑(Iic (f i))
h' : ⨆ i ∈ s, f i = ⊤
t : (i : ι) → i ∈ s → Set α
ht : ∀ (i : ι) (a : i ∈ s), f i = sSup (t i a)
ht' : ∀ (i : ι) (a : i ∈ s), ∀ a_1 ∈ t i a, IsAtom a_1
u : Set α := ⋃ i, ⋃ (hi : i ∈ s), t i hi
⊢ u ⊆ {a | IsAtom a}

Tactic:
rintro a ⟨-, ⟨i, rfl⟩, ⟨-, ⟨hi, rfl⟩, ha : a ∈ t i hi⟩⟩

Goal state after:
ι : Type u_1
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
s : Set ι
f : ι → α
h : ∀ i ∈ s, ComplementedLattice ↑(Iic (f i))
h' : ⨆ i ∈ s, f i = ⊤
t : (i : ι) → i ∈ s → Set α
ht : ∀ (i : ι) (a : i ∈ s), f i = sSup (t i a)
ht' : ∀ (i : ι) (a : i ∈ s), ∀ a_1 ∈ t i a, IsAtom a_1
u : Set α := ⋃ i, ⋃ (hi : i ∈ s), t i hi
a : α
i : ι
hi : i ∈ s
ha : a ∈ t i hi
⊢ a ∈ {a | IsAtom a}
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: case refine_1
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
hp' : Fact (Nat.Prime p)
⊢ ((P : Sylow (↑⟨p, hp⟩) G) → ↥P) ≃* ↥↑(P ↑⟨p, hp⟩)

Tactic:
letI := unique_of_normal _ (hn (P p))

Goal state after:
case refine_1
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
hp' : Fact (Nat.Prime p)
this : Unique (Sylow p G) := (P p).unique_of_normal ⋯
⊢ ((P : Sylow (↑⟨p, hp⟩) G) → ↥P) ≃* ↥↑(P ↑⟨p, hp⟩)
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
x b a y : X
ha : x ⊓ y = a
hxy : x ≠ y
hxb : IsMaximal x b
hyb : IsMaximal y b
⊢ IsMaximal a y

Tactic:
have hb : x ⊔ y = b := sup_eq_of_isMaximal hxb hyb hxy

Goal state after:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
x b a y : X
ha : x ⊓ y = a
hxy : x ≠ y
hxb : IsMaximal x b
hyb : IsMaximal y b
hb : x ⊔ y = b
⊢ IsMaximal a y
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✝ : IsSimpleModule R M
m : M
hm : m ≠ 0
⊢ Function.Surjective ⇑(toSpanSingleton R M m)

Tactic:
rw [← range_eq_top, ← span_singleton_eq_range, span_singleton_eq_top R hm]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : R
⊢ IsTorsionBySet R M {a} ↔ IsTorsionBy R M a

Tactic:
refine ⟨fun h x => @h _ ⟨_, Set.mem_singleton _⟩, fun h x => ?_⟩
  rintro ⟨b, rfl : b = a⟩; exact @h _

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
⊢ Equivalent ((eraseLast s).snoc (last s) ⋯) ((snoc t (eraseLast s).last ⋯).snoc (last s) ⋯)

Tactic:
exact Equivalent.snoc hteqv (by simpa using iso_refl)

Goal state after:
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:
simpa [← X_smul_of] using! q.smul_mem (X : R[X]) hm

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

Goal state before:
pp: ι : 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]
x : PolynomialModule R R
⊢ (coeffAddEquiv.trans (AddMonoidAlgebra.coeffAddEquiv.symm.trans (toFinsuppIso R).symm.toAddEquiv)).toFun (r • x) =
    (RingHom.id R[X]) r •
      (coeffAddEquiv.trans (AddMonoidAlgebra.coeffAddEquiv.symm.trans (toFinsuppIso R).symm.toAddEquiv)).toFun x

Tactic:
dsimp

Goal state after:
ι : 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]
x : PolynomialModule R R
⊢ (toFinsuppIso R).symm (AddMonoidAlgebra.coeffAddEquiv.symm (coeffAddEquiv (r • x))) =
    r * (toFinsuppIso R).symm (AddMonoidAlgebra.coeffAddEquiv.symm (coeffAddEquiv x))
Module: Mathlib.RingTheory.ReesAlgebra

Goal state before:
pp: case zero
R : Type u
inst✝ : CommRing R
I : Ideal R
r : R
hr : r ∈ I ^ 0
⊢ (monomial 0) r ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)

Tactic:
exact Subalgebra.algebraMap_mem _ _

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

Goal state before:
pp: case h
R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_3
inst✝² : CommMonoid S
inst✝¹ : DistribMulAction S M
inst✝ : SMulCommClass S R M
s : S
x : M
a : S
h : a • x = 0
⊢ a • s • ↑⟨x, ⋯⟩ = 0

Tactic:
dsimp

Goal state after:
case h
R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_3
inst✝² : CommMonoid S
inst✝¹ : DistribMulAction S M
inst✝ : SMulCommClass S R M
s : S
x : M
a : S
h : a • x = 0
⊢ a • s • x = 0
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✝ : Module.Finite R M
hM : IsTorsion R M
S : Finset M
hS : span R ↑S = ⊤
n : ↑↑S
this : DecidableEq M := Classical.decEq M
⊢ (∏ i ∈ S, ↑⋯.choose) • ↑n = 0

Tactic:
rw [← Finset.prod_erase_mul _ _ n.prop, mul_smul, ← Submonoid.smul_def, (@hM n).choose_spec,
    smul_zero]

Goal state after:
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: case h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
n : ℕ
a✝ : n ≥ 0
⊢ I • (I.stableFiltration N).N n = (I.stableFiltration N).N (n + 1)

Tactic:
dsimp

Goal state after:
case h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
n : ℕ
a✝ : n ≥ 0
⊢ I • I ^ n • N = I ^ (n + 1) • N
Module: Mathlib.Algebra.Category.ModuleCat.Differentials.Basic

Goal state before:
pp: A B : CommRingCat
M : ModuleCat ↑B
f : A ⟶ B
d : ↑B → ↑M
d_add : ∀ (b b' : ↑B), d (b + b') = d b + d b'
d_mul : ∀ (b b' : ↑B), d (b * b') = b • d b' + b' • d b
d_map : ∀ (a : ↑A), d ((ConcreteCategory.hom f) a) = 0
this✝ : Algebra ↑A ↑B := (CommRingCat.Hom.hom f).toAlgebra
this : Module ↑A ↑M := Module.compHom (↑M) (CommRingCat.Hom.hom f)
a : ↑A
b : ↑B
⊢ d (a • b) = (RingHom.id ↑A) a • d b

Tactic:
dsimp

Goal state after:
A B : CommRingCat
M : ModuleCat ↑B
f : A ⟶ B
d : ↑B → ↑M
d_add : ∀ (b b' : ↑B), d (b + b') = d b + d b'
d_mul : ∀ (b b' : ↑B), d (b * b') = b • d b' + b' • d b
d_map : ∀ (a : ↑A), d ((ConcreteCategory.hom f) a) = 0
this✝ : Algebra ↑A ↑B := (CommRingCat.Hom.hom f).toAlgebra
this : Module ↑A ↑M := Module.compHom (↑M) (CommRingCat.Hom.hom f)
a : ↑A
b : ↑B
⊢ d (a • b) = a • d b
Module: Mathlib.Algebra.Category.ModuleCat.Differentials.Basic

Goal state before:
pp: A B : CommRingCat
M : ModuleCat ↑B
f : A ⟶ B
d : ↑B → ↑M
d_add : ∀ (b b' : ↑B), d (b + b') = d b + d b'
d_mul : ∀ (b b' : ↑B), d (b * b') = b • d b' + b' • d b
d_map : ∀ (a : ↑A), d ((ConcreteCategory.hom f) a) = 0
this✝ : Algebra ↑A ↑B := (CommRingCat.Hom.hom f).toAlgebra
this : Module ↑A ↑M := Module.compHom (↑M) (CommRingCat.Hom.hom f)
⊢ { toFun := d, map_add' := d_add, map_smul' := ⋯ } 1 = 0

Tactic:
dsimp

Goal state after:
A B : CommRingCat
M : ModuleCat ↑B
f : A ⟶ B
d : ↑B → ↑M
d_add : ∀ (b b' : ↑B), d (b + b') = d b + d b'
d_mul : ∀ (b b' : ↑B), d (b * b') = b • d b' + b' • d b
d_map : ∀ (a : ↑A), d ((ConcreteCategory.hom f) a) = 0
this✝ : Algebra ↑A ↑B := (CommRingCat.Hom.hom f).toAlgebra
this : Module ↑A ↑M := Module.compHom (↑M) (CommRingCat.Hom.hom f)
⊢ d 1 = 0
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: case mp.refine_2
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
hF' : ∀ (i : ℕ), (F.N i).FG
H : F.submodule.FG
⊢ iSup
      ⇑{ toFun := fun n₀ ↦ Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i)),
          monotone' := ⋯ } =
    F.submodule

Tactic:
dsimp

Goal state after:
case mp.refine_2
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
hF' : ∀ (i : ℕ), (F.N i).FG
H : F.submodule.FG
⊢ ⨆ n₀, Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i)) = F.submodule
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: 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
⊢ (R ⧸ I ^ 2) ⧸ map (Quotient.mk (I ^ 2)) I ≃+* R ⧸ I

Tactic:
refine (DoubleQuot.quotQuotEquivQuotSup _ _).trans ?_

Goal state after:
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
⊢ R ⧸ I ^ 2 ⊔ I ≃+* R ⧸ I
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
⊢ (∃ x, R ∙ x = ⊤) ↔ ∃ a, maximalIdeal R = R ∙ a

Tactic:
← (map_injective_of_injective (injective_subtype _)).eq_iff,

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
⊢ (∃ x, map (Submodule.subtype (maximalIdeal R)) (R ∙ x) = map (Submodule.subtype (maximalIdeal R)) ⊤) ↔
    ∃ a, maximalIdeal R = R ∙ a
Module: Mathlib.Algebra.Homology.ComplexShape

Goal state before:
pp: α : Type u_1
inst✝¹ : AddRightCancelSemigroup α
inst✝ : DecidableEq α
a x✝¹ x✝ : α
⊢ Decidable ((up' a).Rel x✝¹ x✝)

Tactic:
dsimp

Goal state after:
α : Type u_1
inst✝¹ : AddRightCancelSemigroup α
inst✝ : DecidableEq α
a x✝¹ x✝ : α
⊢ Decidable (x✝¹ + a = x✝)
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 : M.Derivation φ
f : M ⟶ N
X : Cᵒᵖ
a : ↑(S.obj X)
⊢ ((ModuleCat.Hom.hom (f.app (F.op.obj X))).toAddMonoidHom.comp d.d) ((ConcreteCategory.hom (φ.app X)) a) = 0

Tactic:
dsimp

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
d : M.Derivation φ
f : M ⟶ N
X : Cᵒᵖ
a : ↑(S.obj X)
⊢ (ModuleCat.Hom.hom (f.app (Opposite.op (F.obj (Opposite.unop X))))) (d.d ((ConcreteCategory.hom (φ.app X)) a)) = 0
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
x✝ : Dᵒᵖ
⊢ CommRingCat.KaehlerDifferential.map ⋯ =
    (ModuleCat.restrictScalarsId' (RingCat.Hom.hom ((R ⋙ forget₂ CommRingCat RingCat).map (𝟙 x✝))) ⋯).inv.app
      (CommRingCat.KaehlerDifferential (φ'.app x✝))

Tactic:
dsimp

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
x✝ : Dᵒᵖ
⊢ CommRingCat.KaehlerDifferential.map ⋯ =
    (ModuleCat.restrictScalarsId'App (CommRingCat.Hom.hom (R.map (𝟙 x✝))) ⋯
        (CommRingCat.KaehlerDifferential (φ'.app x✝))).inv
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
X✝ Y✝ Z✝ : Dᵒᵖ
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ CommRingCat.KaehlerDifferential.map ⋯ =
    CommRingCat.KaehlerDifferential.map ⋯ ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom ((R ⋙ forget₂ CommRingCat RingCat).map x✝¹))).map
          (CommRingCat.KaehlerDifferential.map ⋯) ≫
        (ModuleCat.restrictScalarsComp' (RingCat.Hom.hom ((R ⋙ forget₂ CommRingCat RingCat).map x✝¹))
                (RingCat.Hom.hom ((R ⋙ forget₂ CommRingCat RingCat).map x✝))
                (RingCat.Hom.hom ((R ⋙ forget₂ CommRingCat RingCat).map (x✝¹ ≫ x✝))) ⋯).inv.app
          (CommRingCat.KaehlerDifferential (φ'.app Z✝))

Tactic:
dsimp

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
X✝ Y✝ Z✝ : Dᵒᵖ
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ CommRingCat.KaehlerDifferential.map ⋯ =
    CommRingCat.KaehlerDifferential.map ⋯ ≫
      (ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map x✝¹))).map (CommRingCat.KaehlerDifferential.map ⋯) ≫
        (ModuleCat.restrictScalarsComp'App (CommRingCat.Hom.hom (R.map x✝¹)) (CommRingCat.Hom.hom (R.map x✝))
            (CommRingCat.Hom.hom (R.map (x✝¹ ≫ x✝))) ⋯ (CommRingCat.KaehlerDifferential (φ'.app Z✝))).inv
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
        ((relativeDifferentials' φ').map f ≫
          (ModuleCat.restrictScalars (RingCat.Hom.hom ((R ⋙ forget₂ CommRingCat RingCat).map f))).map (d'.app Y).desc))
      (CommRingCat.KaehlerDifferential.d b) =
    (ConcreteCategory.hom ((d'.app X).desc ≫ M'.map f)) (CommRingCat.KaehlerDifferential.d b)

Tactic:
dsimp

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)) ((ModuleCat.Hom.hom (d'.app X).desc) (CommRingCat.KaehlerDifferential.d b))
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 : PresheafOfModules R
s : M.sections
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ (ModuleCat.Hom.hom
        ((unit R).map f ≫
          (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map
            (ModuleCat.ofHom ((ringLmapEquivSelf ↑(R.obj Y) ℤ ↑(M.obj Y)).symm (↑s Y)))))
      1 =
    (ModuleCat.Hom.hom (ModuleCat.ofHom ((ringLmapEquivSelf ↑(R.obj X) ℤ ↑(M.obj X)).symm (↑s X)) ≫ M.map f)) 1

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M✝ M₁ M₂ : PresheafOfModules R
M : PresheafOfModules R
s : M.sections
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ 1 ((ModuleCat.Hom.hom ((unit R).map f)) 1) • ↑s Y = (ModuleCat.Hom.hom (M.map f)) (1 • ↑s X)