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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
⊢ TopologicalSpace.IsTopologicalBasis (SetLike.coe '' Set.range basicOpen)

Tactic:
convert! isTopologicalBasis_basic_opens (R := R)

Goal state after:
R : Type u
inst✝ : CommSemiring R
⊢ SetLike.coe '' Set.range basicOpen = Set.range fun r ↦ ↑(basicOpen r)
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case refine_3
ι : Type u_1
R : ι → Type u_2
inst✝ : (i : ι) → CommRing (R i)
i : ι
⊢ ∀ s ∈ Set.range fun r ↦ ↑(basicOpen r), IsOpen ((fun a ↦ comap (Pi.evalRingHom R i) a) '' s)

Tactic:
rintro - ⟨f, rfl⟩

Goal state after:
case refine_3
ι : Type u_1
R : ι → Type u_2
inst✝ : (i : ι) → CommRing (R i)
i : ι
f : R i
⊢ IsOpen ((fun a ↦ comap (Pi.evalRingHom R i) a) '' (fun r ↦ ↑(basicOpen r)) f)
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : ⊥.factorization p ≠ 0
ht : exponent G = ⊥
⊢ (Nat.factorization 0) p = 0

Tactic:
Nat.factorization_zero,

Goal state after:
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : ⊥.factorization p ≠ 0
ht : exponent G = ⊥
⊢ 0 p = 0
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'
inst✝ : IsCyclic α
H : Subgroup α
this : (a : Prop) → Decidable a
g : α
hg : ∀ (x : α), x ∈ zpowers g
hx✝ : ∃ x ∈ H, x ≠ 1
x✝¹ : α
hx₁ : x✝¹ ∈ H
hx₂ : x✝¹ ≠ 1
k✝ : ℤ
hk✝² : (fun x ↦ g ^ x) k✝ = x✝¹
hk✝¹ : g ^ k✝ = x✝¹
hex : ∃ n, 0 < n ∧ g ^ n ∈ H
x✝ : ↥H
x : α
hx : x ∈ H
k : ℤ
hk✝ : (fun x ↦ g ^ x) k = x
hk : g ^ k = x
⊢ g ^ (↑(Nat.find hex) * (k / ↑(Nat.find hex))) ∈ H

Tactic:
rw [zpow_mul]

Goal state after:
α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst✝³ : Group α
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : IsCyclic α
H : Subgroup α
this : (a : Prop) → Decidable a
g : α
hg : ∀ (x : α), x ∈ zpowers g
hx✝ : ∃ x ∈ H, x ≠ 1
x✝¹ : α
hx₁ : x✝¹ ∈ H
hx₂ : x✝¹ ≠ 1
k✝ : ℤ
hk✝² : (fun x ↦ g ^ x) k✝ = x✝¹
hk✝¹ : g ^ k✝ = x✝¹
hex : ∃ n, 0 < n ∧ g ^ n ∈ H
x✝ : ↥H
x : α
hx : x ∈ H
k : ℤ
hk✝ : (fun x ↦ g ^ x) k = x
hk : g ^ k = x
⊢ (g ^ ↑(Nat.find hex)) ^ (k / ↑(Nat.find hex)) ∈ H
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}
r : R
eq : ∀ (a : ↑(Set.range f)), (algebraMap R (Localization.Away ↑a)) r = (algE a) (x (e.symm a))
I : PrimeSpectrum R
this : (algebraMap R (Localization.Away ↑(e I))) r = (algE (e I)) (x (e.symm (e I)))
⊢ (toPiLocalization R) r I = x I

Tactic:
← AlgEquiv.symm_apply_eq,

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}
r : R
eq : ∀ (a : ↑(Set.range f)), (algebraMap R (Localization.Away ↑a)) r = (algE a) (x (e.symm a))
I : PrimeSpectrum R
this : (algE (e I)).symm ((algebraMap R (Localization.Away ↑(e I))) r) = x (e.symm (e I))
⊢ (toPiLocalization R) r I = x I
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
x y : PrimeSpectrum R
h : x.asIdeal ≤ y.asIdeal
a : R
ha : a ∈ y.asIdeal.primeCompl
⊢ IsUnit ((algebraMap R (Localization.AtPrime x.asIdeal)) ↑⟨a, ha⟩)

Tactic:
← SetLike.coe_subset_coe,

Goal state after:
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
x y : PrimeSpectrum R
h : ↑x.asIdeal ⊆ ↑y.asIdeal
a : R
ha : a ∈ y.asIdeal.primeCompl
⊢ IsUnit ((algebraMap R (Localization.AtPrime x.asIdeal)) ↑⟨a, ha⟩)
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
⊢ g ^ ⋯.choose = (g ^ ⋯.choose) ^ ⋯.choose

Tactic:
← (MulDistribMulAction.toMonoidHom G m).map_cyclic.choose_spec,

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
⊢ g ^ ⋯.choose = (toMonoidHom G m) (g ^ ⋯.choose)
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝ : Group G
n : ℕ
hG : Nat.card G ∣ p ^ n
g : G
⊢ g ^ p ^ n = 1

Tactic:
grw [← orderOf_dvd_iff_pow_eq_one, ← hG, orderOf_dvd_natCard]

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
P : Subgroup G
hP : IsPGroup p ↥P
H : Subgroup G
inst✝ : H.Normal
h_cop : (Nat.card ↥H).Coprime H.index
h1 : ¬Nat.card ↥H = 0
h2 : ¬H.index = 0
⊢ Finite G

Tactic:
apply Nat.finite_of_card_ne_zero

Goal state after:
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
P : Subgroup G
hP : IsPGroup p ↥P
H : Subgroup G
inst✝ : H.Normal
h_cop : (Nat.card ↥H).Coprime H.index
h1 : ¬Nat.card ↥H = 0
h2 : ¬H.index = 0
⊢ Nat.card G ≠ 0
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_2
G' : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : IsCyclic G'
f : G →* G'
hf : f.ker ≤ center G
a b : G
x : G'
y : G
hxy : f y = x
hx : ∀ (a : ↥f.range), a ∈ zpowers ⟨x, ⋯⟩
m : ℤ
hm✝ : (fun x_1 ↦ ⟨x, ⋯⟩ ^ x_1) m = ⟨f a, ⋯⟩
n : ℤ
hn✝ : (fun x_1 ↦ ⟨x, ⋯⟩ ^ x_1) n = ⟨f b, ⋯⟩
hm : x ^ m = f a
hn : x ^ n = f b
ha : y ^ (-m) * a ∈ center G
hb : y ^ (-n) * b ∈ center G
⊢ y ^ m * y ^ n * y ^ (-m) * (a * (y ^ (-n) * b)) = y ^ m * y ^ n * y ^ (-m) * (y ^ (-n) * b * a)

Tactic:
rw [mem_center_iff.1 hb]

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
⊢ IsCompactlyGenerated ↑(Iic a)

Tactic:
refine ⟨fun ⟨x, (hx : x ≤ a)⟩ ↦ ?_⟩

Goal state after:
ι : Type u_1
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
x✝ : ↑(Iic a)
x : α
hx : x ≤ a
⊢ ∃ s, (∀ x ∈ s, IsCompactElement x) ∧ sSup s = ⟨x, hx⟩
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝¹ : Group G
inst✝ : Fintype G
p k : ℕ
hp : Nat.Prime p
h : p ^ k ∣ Nat.card G
this : Fact (Nat.Prime p)
⊢ p ^ k ∣ ∏ g, orderOf g

Tactic:
have ⟨H, hH⟩ := exists_subgroup_card_pow_prime p h

Goal state after:
G : Type u
inst✝¹ : Group G
inst✝ : Fintype G
p k : ℕ
hp : Nat.Prime p
h : p ^ k ∣ Nat.card G
this : Fact (Nat.Prime p)
H : Subgroup G
hH : Nat.card ↥H = p ^ k
⊢ p ^ k ∣ ∏ g, orderOf g
Module: Mathlib.RingTheory.SimpleModule.Basic

Goal state before:
pp: M : Type u_4
inst✝² : AddCommGroup M
R : Type u_6
inst✝¹ : CommRing R
inst✝ : Module R M
simple : IsSimpleModule R M
⊢ (Module.annihilator R M).IsMaximal

Tactic:
have ⟨I, max, ⟨e⟩⟩ := isSimpleModule_iff_quot_maximal.mp simple
  rwa [e.annihilator_eq, I.annihilator_quotient]

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 (eraseLast s).last ⋯).last, last s) ∈ {(x, y) | IsMaximal x y}

Tactic:
simpa using isMaximal_eraseLast_last h0s

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
r : R
f : R[X]
m : AEval R M a
⊢ (r • f) • m = r • f • m

Tactic:
apply (of R M a).symm.injective
    rw [of_symm_smul, map_smul, smul_assoc, map_smul, of_symm_smul]

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 • (R ∙ 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

Tactic:
smul_sup

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.RingTheory.Finiteness.Nakayama

Goal state before:
pp: case h.right
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
z : M
hz : z ∈ I • span R s
c : R
hci : c ∈ I
hyz : c • i + z = r • i
⊢ (r - c) • i ∈ I • span R s

Tactic:
rw [sub_smul, ← hyz, add_sub_cancel_left]
      exact hz

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

Goal state before:
pp: case single
R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : R[X]
r : R
i : ℕ
m : M
⊢ (eval r) (p ^ i • single R 0 m) = Polynomial.eval r p ^ i • m

Tactic:
eval_smul,

Goal state after:
case single
R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : R[X]
r : R
i : ℕ
m : M
⊢ Polynomial.eval r (p ^ i) • (eval r) (single R 0 m) = Polynomial.eval r p ^ i • m
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
⊢ (eval p) (Polynomial.map (algebraMap R R[X]) p' • (map R[X] (lsingle R 0)) q) = p'.comp p • (comp p) q

Tactic:
eval_smul,

Goal state after:
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
⊢ Polynomial.eval p (Polynomial.map (algebraMap R R[X]) p') • (eval p) ((map R[X] (lsingle R 0)) q) =
    p'.comp p • (comp p) q
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:
by
  rw [comp_apply, map_smul, eval_smul, Polynomial.comp, Polynomial.eval_map, comp_apply]
  rfl

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
z : M ⧸ torsion R M
x : M
x✝ : Quotient.mk'' x ∈ torsion R (M ⧸ torsion R M)
a : ↥R⁰
hax : a • Quotient.mk'' x = 0
⊢ Quotient.mk'' x ∈ ⊥

Tactic:
Quotient.mk''_eq_mk,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
z : M ⧸ torsion R M
x : M
x✝ : Quotient.mk'' x ∈ torsion R (M ⧸ torsion R M)
a : ↥R⁰
hax : a • Quotient.mk x = 0
⊢ Quotient.mk'' x ∈ ⊥
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
z : M ⧸ torsion R M
x : M
x✝ : Quotient.mk'' x ∈ torsion R (M ⧸ torsion R M)
a : ↥R⁰
hax : a • x ∈ torsion R M
⊢ Quotient.mk'' x = 0

Tactic:
Quotient.mk''_eq_mk,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
z : M ⧸ torsion R M
x : M
x✝ : Quotient.mk'' x ∈ torsion R (M ⧸ torsion R M)
a : ↥R⁰
hax : a • x ∈ torsion R M
⊢ Quotient.mk x = 0
Module: Mathlib.RingTheory.Nakayama

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
N N' P : Submodule R M
hN' : N'.FG
hN'le : N' ≤ P
hNN' : P ≤ N ⊔ I • N'
hNN'' : P ≤ N ⊔ N'
⊢ map N.mkQ P = map N.mkQ N'

Tactic:
refine le_antisymm ?_ (map_mono hN'le)

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N N' P : Submodule R M
hN' : N'.FG
hN'le : N' ≤ P
hNN' : P ≤ N ⊔ I • N'
hNN'' : P ≤ N ⊔ N'
⊢ map N.mkQ P ≤ map N.mkQ N'
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: case hF'
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
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
hF : F.submodule.FG
F' : I.Filtration M
hf : F' ≤ F
i : ℕ
⊢ (F'.N i).FG

Tactic:
exact IsNoetherian.noetherian _

Goal state after:
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: case hF'
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
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
hF : F.Stable
F' : I.Filtration M
hf : F' ≤ F
i : ℕ
⊢ (F.N i).FG

Tactic:
exact IsNoetherian.noetherian _

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
s : Set (CotangentSpace R)
hs_card : Cardinal.mk ↑s = ⊤.spanRank
hs_span : Submodule.span (ResidueField R) s = ⊤
⊢ Submodule.span R s = Submodule.map (maximalIdeal R • ⊤).mkQ ⊤

Tactic:
rw [Submodule.map_top, Submodule.range_mkQ]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
s : Set (CotangentSpace R)
hs_card : Cardinal.mk ↑s = ⊤.spanRank
hs_span : Submodule.span (ResidueField R) s = ⊤
⊢ Submodule.span R s = ⊤
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
U V W : Cᵒᵖ
i : U ⟶ V
j : V ⟶ W
x : ↑(M.obj U)
⊢ (ConcreteCategory.hom (M.map (i ≫ j))) x = (ConcreteCategory.hom (M.map j)) ((ConcreteCategory.hom (M.map i)) x)

Tactic:
rw [M.map_comp]; rfl

Goal state after:
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
n : M
X : C
inst✝ : F.Monoidal
⊢ (F.obj n).map ((η F).app X) = (μ F (𝟙_ M) n).app X ≫ (F.map (λ_ n).hom).app X

Tactic:
← cancel_mono ((F.obj n).map ((ε F).app X)),

Goal state after:
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
n : M
X : C
inst✝ : F.Monoidal
⊢ (F.obj n).map ((η F).app X) ≫ (F.obj n).map ((ε F).app X) =
    ((μ F (𝟙_ M) n).app X ≫ (F.map (λ_ n).hom).app X) ≫ (F.obj n).map ((ε F).app X)
Module: Mathlib.CategoryTheory.GradedObject

Goal state before:
pp: C : Type u_1
D : Type u_2
J : Type u_4
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
X Y : GradedObject J C
e : X ≅ Y
F : C ⥤ D
j : J
⊢ F.map (e.inv j) ≫ F.map (e.hom j) = 𝟙 (F.obj (Y j))

Tactic:
rw [← F.map_comp, ← GradedObject.categoryOfGradedObjects_comp, e.inv_hom_id,
    GradedObject.categoryOfGradedObjects_id, Functor.map_id]

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
inst✝ : HasShift C A
a₁ a₂ a₃ : A
X : C
⊢ (OplaxMonoidal.δ (shiftMonoidalFunctor C A) { as := a₁ + a₂ } { as := a₃ }).app X ≫
      (LaxMonoidal.μ (shiftMonoidalFunctor C A) (MonoidalCategoryStruct.tensorObj { as := a₁ } { as := a₂ })
              { as := a₃ }).app
          X ≫
        eqToHom ⋯ ≫
          (OplaxMonoidal.δ (shiftMonoidalFunctor C A) { as := a₁ }
                  (MonoidalCategoryStruct.tensorObj { as := a₂ } { as := a₃ })).app
              X ≫
            (OplaxMonoidal.δ (shiftMonoidalFunctor C A) { as := a₂ } { as := a₃ }).app
              (((shiftMonoidalFunctor C A).obj { as := a₁ }).obj X) =
    (eqToHom ⋯ ≫ (OplaxMonoidal.δ (shiftMonoidalFunctor C A) { as := a₁ } { as := a₂ + a₃ }).app X) ≫
      (OplaxMonoidal.δ (shiftMonoidalFunctor C A) { as := a₂ } { as := a₃ }).app
        (((shiftMonoidalFunctor C A).obj { as := a₁ }).obj X)

Tactic:
erw [δ_μ_app_assoc, Category.assoc]

Goal state after:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a₁ a₂ a₃ : A
X : C
⊢ eqToHom ⋯ ≫
      (OplaxMonoidal.δ (shiftMonoidalFunctor C A) { as := a₁ }
              (MonoidalCategoryStruct.tensorObj { as := a₂ } { as := a₃ })).app
          X ≫
        (OplaxMonoidal.δ (shiftMonoidalFunctor C A) { as := a₂ } { as := a₃ }).app
          (((shiftMonoidalFunctor C A).obj { as := a₁ }).obj X) =
    eqToHom ⋯ ≫
      (OplaxMonoidal.δ (shiftMonoidalFunctor C A) { as := a₁ } { as := a₂ + a₃ }).app X ≫
        (OplaxMonoidal.δ (shiftMonoidalFunctor C A) { as := a₂ } { as := a₃ }).app
          (((shiftMonoidalFunctor C A).obj { as := a₁ }).obj X)
Module: Mathlib.Algebra.Homology.HomologicalComplex

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
succ : (S : ShortComplex V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0
S S' : ShortComplex V
h : S = S'
⊢ (succ S).snd.fst = eqToHom ⋯ ≫ (succ S').snd.fst ≫ eqToHom ⋯

Tactic:
subst h
  simp

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

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
succ' : {X₀ X₁ : V} → (f : X₁ ⟶ X₀) → (X₂ : V) ×' (d : X₂ ⟶ X₁) ×' d ≫ f = 0
X Y : V
f g : X ⟶ Y
h : f = g
⊢ (succ' f).snd.fst = eqToHom ⋯ ≫ (succ' g).snd.fst

Tactic:
subst h
  simp

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

Goal state before:
pp: case mp
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex (HomologicalComplex C c)
⊢ S.Exact → ∀ (i : ι), (S.map (eval C c i)).Exact

Tactic:
intro hS i
    exact hS.map (eval C c i)

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

Goal state before:
pp: R : Type u
S : Type v
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
M : Type u_1
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : IsScalarTower R S M
inst✝ : EssFiniteType R S
⊢ Module.Finite S Ω[S⁄R]

Tactic:
classical
  let s := (EssFiniteType.finset R S).image (fun s ↦ D R S s)
  refine ⟨⟨s, top_le_iff.mp ?_⟩⟩
  rw [← span_range_derivation, Submodule.span_le]
  rintro _ ⟨x, rfl⟩
  have : ∀ x ∈ adjoin R (EssFiniteType.finset R S : Set S),
      .D _ _ x ∈ Submodule.span S (s : Set Ω[S⁄R]) := by
    intro x hx
    refine adjoin_induction ?_ ?_ ?_ ?_ hx
    · exact fun x hx ↦ Submodule.subset_span (Finset.mem_image_of_mem _ hx)
    · simp
    · exact fun x y _ _ hx hy ↦ (D R S).map_add x y ▸ add_mem hx hy
    · intro x y _ _ hx hy
      simp only [Derivation.leibniz]
      exact add_mem (Submodule.smul_mem _ _ hy) (Submodule.smul_mem _ _ hx)
  obtain ⟨t, ht, ht', hxt⟩ := (essFiniteType_cond_iff R S (EssFiniteType.finset R S)).mp
    EssFiniteType.cond.choose_spec x
  rw [show D R S x =
    ht'.unit⁻¹ • (D R S (x * t) - x • D R S t) by simp [smul_smul, Units.smul_def]]
  exact Submodule.smul_mem _ _ (sub_mem (this _ hxt) (Submodule.smul_mem _ _ (this _ ht)))

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i j k : ι
hi : c.prev j = i
hk : c.next j = k
inst✝¹ : K.HasHomology j
inst✝ : (K.sc' i j k).HasHomology
⊢ K.pOpcycles j ≫ (K.opcyclesIsoSc' i j k hi hk).hom = (K.sc' i j k).pOpcycles

Tactic:
simp [opcyclesIsoSc', pOpcycles]

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
c : ComplexShape ι
K L : HomologicalComplex C c
inst✝ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (L.X i)
i : ι
⊢ (biprod.inl ≫ biprod.snd).f i = 0

Tactic:
biprod.inl_snd,

Goal state after:
C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
c : ComplexShape ι
K L : HomologicalComplex C c
inst✝ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (L.X i)
i : ι
⊢ Hom.f 0 i = 0
Module: Mathlib.Algebra.Homology.HomotopyCofiber

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i j : ι
hij : c.Rel i j
A : C
f g : A ⟶ X φ i
h₁ : f ≫ fstX φ i j hij = g ≫ fstX φ i j hij
h₂ : f ≫ sndX φ i = g ≫ sndX φ i
this : HasBinaryBiproduct (F.X j) (G.X i)
⊢ f = g

Tactic:
← cancel_mono (XIsoBiprod φ i j hij).hom

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i j : ι
hij : c.Rel i j
A : C
f g : A ⟶ X φ i
h₁ : f ≫ fstX φ i j hij = g ≫ fstX φ i j hij
h₂ : f ≫ sndX φ i = g ≫ sndX φ i
this : HasBinaryBiproduct (F.X j) (G.X i)
⊢ f ≫ (XIsoBiprod φ i j hij).hom = g ≫ (XIsoBiprod φ i j hij).hom
Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v, u_1} C
inst✝³ : Category.{v', u_2} D
inst✝² : Preadditive C
inst✝¹ : Preadditive D
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
⊢ δ 1 2 (Cochain.mk fun p q hpq ↦ homotopyCofiber.fstX φ p q hpq) = 0

Tactic:
by
    ext p _ rfl
    simp [δ_v 1 2 (by lia) _ p (p + 2) (by lia) (p + 1) (p + 1) (by lia) rfl,
      homotopyCofiber.d_fstX φ p (p + 1) (p + 2) rfl, mappingCone,
      show Int.negOnePow 2 = 1 by rfl]

Goal state after: