mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: case pos
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
le : b.factorization p ≤ a.factorization p
⊢ p ^ (a.factorization ⊔ b.factorization) p ∣ p ^ a.factorization p

Tactic:
apply pow_dvd_pow

Goal state after:
case pos
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
le : b.factorization p ≤ a.factorization p
⊢ (a.factorization ⊔ b.factorization) p ≤ a.factorization p
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
⊢ IsClosed {x} ↔ x.asIdeal.IsMaximal

Tactic:
← closure_subset_iff_isClosed,

Goal state after:
R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
⊢ closure {x} ⊆ {x} ↔ x.asIdeal.IsMaximal
Module: Mathlib.RingTheory.RingHom.Flat

Goal state before:
pp: case refine_1
R S T A : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing T
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R T
inst✝⁴ : Algebra S T
inst✝³ : IsScalarTower R S T
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
h : CommRingCat.flat (CommRingCat.ofHom (Algebra.TensorProduct.lmul' R).toRingHom)
⊢ pushout (CommRingCat.ofHom (algebraMap R S)) (CommRingCat.ofHom (algebraMap R S)) ≅ CommRingCat.of (S ⊗[R] S)

Tactic:
exact (CommRingCat.isPushout_tensorProduct R S S).isoPushout.symm

Goal state after:
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: case neg
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
le : ¬b.factorization p ≤ a.factorization p
⊢ p ^ (a.factorization ⊔ b.factorization) p ∣ p ^ b.factorization p

Tactic:
apply pow_dvd_pow

Goal state after:
case neg
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
le : ¬b.factorization p ≤ a.factorization p
⊢ (a.factorization ⊔ b.factorization) p ≤ b.factorization p
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: case zero
R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring A
inst✝³ : AddCommMonoid M
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
a : A
⊢ D (a ^ 0) = 0 • a ^ (0 - 1) • D a

Tactic:
rw [pow_zero, map_one_eq_zero, zero_smul]

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

Goal state before:
pp: case refine_2
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
⊢ (IsClosedMap fun a ↦ comap (RingHom.fst R S) a) ∧ IsClosedMap fun b ↦ comap (RingHom.snd R S) b

Tactic:
exact ⟨isClosedEmbedding_comap_fst.isClosedMap, isClosedEmbedding_comap_snd.isClosedMap⟩

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

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
f : R
p : PrimeSpectrum R
h : (basicOpen f).carrier = {p}
⊢ IsLocalization.AtPrime (Localization.Away f) p.asIdeal

Tactic:
refine .of_le_of_exists_dvd (.powers f) _
      (Submonoid.powers_le.mpr <| by apply h ▸ Set.mem_singleton p) fun r hr ↦ ?_

Goal state after:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
f : R
p : PrimeSpectrum R
h : (basicOpen f).carrier = {p}
r : R
hr : r ∈ p.asIdeal.primeCompl
⊢ ∃ m ∈ Submonoid.powers f, r ∣ m
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
⊢ IsCyclic α ↔ ∃ g, zpowers g = ⊤

Tactic:
simp only [eq_top_iff', mem_zpowers_iff]
  exact ⟨fun ⟨h⟩ ↦ h, fun h ↦ ⟨h⟩⟩

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
h✝ : IsCyclic G
σ : G →* G
h : G
hG : ∀ (x : G), x ∈ zpowers h
m : ℤ
hm : (fun x ↦ h ^ x) m = σ h
⊢ ∃ m, ∀ (g : G), σ g = g ^ m

Tactic:
refine ⟨m, fun g => ?_⟩

Goal state after:
G : Type u_2
inst✝ : Group G
h✝ : IsCyclic G
σ : G →* G
h : G
hG : ∀ (x : G), x ∈ zpowers h
m : ℤ
hm : (fun x ↦ h ^ x) m = σ h
g : G
⊢ σ g = g ^ m
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: case e'_3
G : Type u_2
inst✝ : Group G
k : ℕ
k_pos : k ≠ 0
this : Finite G
a : G
ha : Function.Surjective fun x ↦ a ^ x
k_lt_card_G : a ^ k = 1
⊢ ⊤ ≤ zpowers a

Tactic:
exact fun x _ ↦ ha x

Goal state after:
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
⊢ DenseRange (comap f) ↔ ∀ (I : Ideal R) (h : I ∈ minimalPrimes R), { asIdeal := I, isPrime := ⋯ } ∈ Set.range (comap f)

Tactic:
constructor
  · intro H I hI
    have : I ∈ (RingHom.ker f).minimalPrimes := by
      rw [denseRange_comap_iff_ker_le_nilRadical] at H
      simp only [Set.mem_ofPred, Ideal.IsMinimalPrime] at hI ⊢
      convert! hI using 2 with p
      exact ⟨fun h ↦ ⟨h.1, bot_le⟩, fun h ↦ ⟨h.1, H.trans (h.1.radical_le_iff.mpr bot_le)⟩⟩
    obtain ⟨p, hp, _, rfl⟩ := Ideal.exists_comap_eq_of_mem_minimalPrimes f (I := ⊥) I this
    exact ⟨⟨p, hp⟩, rfl⟩
  · intro H p
    obtain ⟨q, hq, hq'⟩ := Ideal.exists_minimalPrimes_le (J := p.asIdeal) bot_le
    exact ((le_iff_specializes ⟨q, hq.1.1⟩ p).mp hq').mem_closed isClosed_closure
      (subset_closure (H q hq))

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
this✝ : Fintype α
this : Fintype ↑(fixedPoints G α)
key : ∀ (x : α), card { y // Quotient.mk'' y = Quotient.mk'' x } = card ↑(orbit G x)
a : ↑(fixedPoints G α)
ha : a ∈ Finset.univ
x✝ : ↑1 ≠ 0
⊢ ↑1 = ↑(card { x // Quotient.mk'' x = Quotient.mk'' ↑a })

Tactic:
by
          rw [key, mem_fixedPoints_iff_card_orbit_eq_one.mp a.2]

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
⊢ Function.Bijective fun e ↦ { carrier := ↑(basicOpen (↑e).1), isClopen' := ⋯ }

Tactic:
refine ⟨fun ⟨x, hx⟩ ⟨y, hy⟩ eq ↦ mul_eq_zero_add_eq_one_ext_left ?_, fun s ↦ ?_⟩

Goal state after:
case refine_1
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
x✝¹ x✝ : { e // e.1 * e.2 = 0 ∧ e.1 + e.2 = 1 }
x : R × R
hx : x.1 * x.2 = 0 ∧ x.1 + x.2 = 1
y : R × R
hy : y.1 * y.2 = 0 ∧ y.1 + y.2 = 1
eq :
  (fun e ↦ { carrier := ↑(basicOpen (↑e).1), isClopen' := ⋯ }) ⟨x, hx⟩ =
    (fun e ↦ { carrier := ↑(basicOpen (↑e).1), isClopen' := ⋯ }) ⟨y, hy⟩
⊢ (↑⟨x, hx⟩).1 = (↑⟨y, hy⟩).1

case refine_2
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
s : Clopens (PrimeSpectrum R)
⊢ ∃ a, (fun e ↦ { carrier := ↑(basicOpen (↑e).1), isClopen' := ⋯ }) a = s
Module: Mathlib.GroupTheory.Rank

Goal state before:
pp: G : Type u_1
inst✝² : Group G
H K : Subgroup G
inst✝¹ : Group.FG ↥H
inst✝ : Group.FG ↥K
h : H = K
⊢ rank ↥H = rank ↥K

Tactic:
by
  subst h; rfl

Goal state after:
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 ^ (-m) * a * y ^ n) * (y ^ (-n) * b) = y ^ m * (y ^ n * (y ^ (-m) * a)) * (y ^ (-n) * b)

Tactic:
by rw [mem_center_iff.1 ha]

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

Goal state before:
pp: G : Type u_2
inst✝³ : Infinite G
inst✝² : CommGroup G
inst✝¹ : PartialOrder G
inst✝ : IsOrderedMonoid G
g : G
hg : zpowers g = ⊤
hg1 : g < 1
⊢ StrictAnti ⇑(intEquivOfZPowersEqTop g hg)

Tactic:
by
  intro x y hxy
  simp only [intEquivOfZPowersEqTop, MulEquiv.ofBijective_apply, zpowersHom_apply]
  exact zpow_right_strictAnti hg1 hxy

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
N : Subgroup G
inst✝¹ : N.Normal
inst✝ : Finite (Sylow p ↥N)
P : Sylow p ↥N
g : G
x✝ : g ∈ ⊤
n : ↥N
hn : map ((MulDistribMulAction.toMonoidEnd (MulAut ↥N) ↥N) (MulAut.conjNormal (↑n * g))) ↑P = ↑P
this : Function.Injective ⇑(MulEquiv.toMonoidHom (MulAut.conj (↑n * g)))
x : G
⊢ (MulEquiv.toMonoidHom (MulAut.conj (↑n * g))) x ∈
      map (MulEquiv.toMonoidHom (MulAut.conj (↑n * g))) (map N.subtype ↑P) ↔
    ↑n * g * x * (↑n * g)⁻¹ ∈ ↑(map N.subtype ↑P)

Tactic:
rw [map_map, ← congr_arg (map N.subtype) hn, map_map]

Goal state after:
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
N : Subgroup G
inst✝¹ : N.Normal
inst✝ : Finite (Sylow p ↥N)
P : Sylow p ↥N
g : G
x✝ : g ∈ ⊤
n : ↥N
hn : map ((MulDistribMulAction.toMonoidEnd (MulAut ↥N) ↥N) (MulAut.conjNormal (↑n * g))) ↑P = ↑P
this : Function.Injective ⇑(MulEquiv.toMonoidHom (MulAut.conj (↑n * g)))
x : G
⊢ (MulEquiv.toMonoidHom (MulAut.conj (↑n * g))) x ∈
      map ((MulEquiv.toMonoidHom (MulAut.conj (↑n * g))).comp N.subtype) ↑P ↔
    ↑n * g * x * (↑n * g)⁻¹ ∈
      ↑(map (N.subtype.comp ((MulDistribMulAction.toMonoidEnd (MulAut ↥N) ↥N) (MulAut.conjNormal (↑n * g)))) ↑P)
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
m : Submodule R M
⊢ IsSimpleModule R ↥m ↔ IsSimpleOrder ↑(Set.Iic m)

Tactic:
isSimpleModule_iff

Goal state after:
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : Submodule R M
⊢ IsSimpleOrder (Submodule R ↥m) ↔ IsSimpleOrder ↑(Set.Iic m)
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
m : Submodule R M
⊢ IsSimpleModule R (M ⧸ m) ↔ IsSimpleOrder ↑(Set.Ici m)

Tactic:
isSimpleModule_iff

Goal state after:
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : Submodule R M
⊢ IsSimpleOrder (Submodule R (M ⧸ m)) ↔ IsSimpleOrder ↑(Set.Ici 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
⊢ Polynomial.eval p (Polynomial.map (algebraMap R R[X]) p') • (eval p) ((map R[X] (lsingle R 0)) q) =
    eval₂ C p p' • (comp p) q

Tactic:
Polynomial.eval_map,

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
⊢ eval₂ (algebraMap R R[X]) p p' • (eval p) ((map R[X] (lsingle R 0)) q) = eval₂ C p p' • (comp p) q
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 J : Ideal R
N : Submodule R M
hN : N.FG
hIN : N ≤ I • N
hIjac : I ≤ J.jacobson
⊢ N = J • N

Tactic:
by
  refine le_antisymm ?_ (Submodule.smul_le.2 fun _ _ _ => Submodule.smul_mem _ _)
  intro n hn
  obtain ⟨r, hr⟩ := Submodule.exists_sub_one_mem_and_smul_eq_zero_of_fg_of_le_smul I N hN hIN
  obtain ⟨s, hs⟩ := exists_mul_sub_mem_of_sub_one_mem_jacobson r (hIjac hr.1)
  have : n = -(s * r - 1) • n := by
    rw [neg_sub, sub_smul, mul_smul, hr.2 n hn, one_smul, smul_zero, sub_zero]
  rw [this]
  exact Submodule.smul_mem_smul (Submodule.neg_mem _ hs) hn

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Monoid R
inst✝¹ : AddCommMonoid M
inst✝ : DistribMulAction R M
p : R
⊢ IsTorsion' M ↥(Submonoid.powers p) ↔ ∀ (x : M), ∃ n, p ^ n • x = 0

Tactic:
by
  constructor
  · intro h x
    let ⟨⟨a, ⟨n, hn⟩⟩, hx⟩ := @h x
    dsimp at hn
    use n
    rw [hn]
    apply hx
  · intro h x
    let ⟨n, hn⟩ := h x
    exact ⟨⟨_, ⟨n, rfl⟩⟩, hn⟩

Goal state after:
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: case h.succ
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
e : F.N 0 ≤ F'.N 0
n₀ : ℕ
hF : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
n : ℕ
hn : F.N (n + n₀) ≤ F'.N n
⊢ F.N (n + 1 + n₀) ≤ F'.N (n + 1)

Tactic:
rw [add_right_comm, ← hF]

Goal state after:
case h.succ
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
e : F.N 0 ≤ F'.N 0
n₀ : ℕ
hF : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
n : ℕ
hn : F.N (n + n₀) ≤ F'.N n
⊢ I • F.N (n + n₀) ≤ F'.N (n + 1)

case h.succ.a
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
e : F.N 0 ≤ F'.N 0
n₀ : ℕ
hF : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
n : ℕ
hn : F.N (n + n₀) ≤ F'.N n
⊢ n + n₀ ≥ n₀
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 : Submodule R M
s : Set (M ⧸ I • N)
hN : N.FG
hIjac : I ≤ ⊥.jacobson
hsspan : span R s = map (I • N).mkQ N
⊢ ∃ t, Set.InjOn (⇑(I • N).mkQ) t ∧ ⇑(I • N).mkQ '' t = s ∧ span R t = N

Tactic:
use Quotient.out '' s
  split_ands
  · simp [Set.InjOn]
  · simp [Set.image_image]
  · symm; apply eq_of_map_mkQ_eq_map_mkQ_of_le_jacobson_bot hN hIjac
    simp [← hsspan, map_span, Set.image_image]

Goal state after:
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
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Module.Finite R N
f : M →ₗ[R] N
I : Ideal R
Ile : I ≤ ⊥.jacobson
surj : Function.Surjective ⇑((I • ⊤).mkQ ∘ₗ f)
⊢ Submodule.map (I • ⊤).mkQ f.range = ⊤

Tactic:
← LinearMap.range_comp

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Module.Finite R N
f : M →ₗ[R] N
I : Ideal R
Ile : I ≤ ⊥.jacobson
surj : Function.Surjective ⇑((I • ⊤).mkQ ∘ₗ f)
⊢ ((I • ⊤).mkQ ∘ₗ f).range = ⊤
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
⊢ Submodule.map (Submodule.subtype I) (I • ⊤) ≤ I ^ 2

Tactic:
Submodule.map_smul'',

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
⊢ I • Submodule.map (Submodule.subtype I) ⊤ ≤ I ^ 2
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: case a
R : Type u
inst✝⁴ : CommRing R
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
x : A ⧸ RingHom.ker f.toRingHom ^ 2
hx : x ∈ RingHom.ker f.kerSquareLift.toRingHom
⊢ x ∈ (RingHom.ker f.toRingHom).cotangentIdeal

Tactic:
obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x

Goal state after:
case a
R : Type u
inst✝⁴ : CommRing R
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
x : A
hx : (Quotient.mk (RingHom.ker f.toRingHom ^ 2)) x ∈ RingHom.ker f.kerSquareLift.toRingHom
⊢ (Quotient.mk (RingHom.ker f.toRingHom ^ 2)) x ∈ (RingHom.ker f.toRingHom).cotangentIdeal
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
⊢ Module.rank (ResidueField R) (CotangentSpace R) = Submodule.spanRank (maximalIdeal R)

Tactic:
rw [Submodule.rank_eq_spanRank_of_free, ← Submodule.spanRank_top (maximalIdeal R)]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
⊢ ⊤.spanRank = ⊤.spanRank
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: case mp
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 := ⋯
hN : ∀ (k : ℕ), (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N k = N
⊢ x ∈ ⨅ i, I ^ i • ⊤ → ∃ r, ↑r • x = x

pp: case mpr
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 := ⋯
hN : ∀ (k : ℕ), (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N k = N
⊢ (∃ r, ↑r • x = x) → x ∈ ⨅ i, I ^ i • ⊤

Tactic:
· obtain ⟨r, hr₁, hr₂⟩ :=
      Submodule.exists_mem_and_smul_eq_self_of_fg_of_le_smul I N (IsNoetherian.noetherian N) (by
        obtain ⟨k, hk⟩ := (I.stableFiltration_stable ⊤).inter_right (I.trivialFiltration N)
        have := hk k (le_refl _)
        rw [hN, hN] at this
        exact le_of_eq this.symm)
    intro H
    exact ⟨⟨r, hr₁⟩, hr₂ _ H⟩

Goal state after:
case mpr
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 := ⋯
hN : ∀ (k : ℕ), (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N k = N
⊢ (∃ r, ↑r • x = x) → x ∈ ⨅ i, I ^ i • ⊤
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M✝ M₁ M₂ M N : PresheafOfModules R
f : M ⟶ N
s : M.sections
X Y : Cᵒᵖ
g : X ⟶ Y
⊢ (ConcreteCategory.hom (N.map g)) ((ConcreteCategory.hom (f.app X)) (↑s X)) = (ConcreteCategory.hom (f.app Y)) (↑s Y)

Tactic:
rw [← naturality_apply, sections_property]

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 Z : Cᵒᵖ
g : Y ⟶ Z
⊢ (forgetToPresheafModuleCatObj X hX M).map g ≫
      ModuleCat.ofHom { toFun := ⇑(ConcreteCategory.hom (f.app Z)), map_add' := ⋯, map_smul' := ⋯ } =
    ModuleCat.ofHom { toFun := ⇑(ConcreteCategory.hom (f.app Y)), map_add' := ⋯, map_smul' := ⋯ } ≫
      (forgetToPresheafModuleCatObj X hX N).map g

Tactic:
by
    ext x
    exact naturality_apply f g x

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:
rw [← cancel_mono ((F.obj n).map ((ε F).app X)), ← Functor.map_comp]

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).app X) =
    ((μ F (𝟙_ M) n).app X ≫ (F.map (λ_ n).hom).app X) ≫ (F.obj n).map ((ε F).app X)
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
m₁ m₂ m₃ : A
X : C
⊢ 𝟙 ((h.F m₃).obj ((h.F m₁ ⋙ h.F m₂).obj X)) =
    (h.add m₂ m₃).inv.app ((h.F m₁).obj X) ≫
      (h.add m₁ (m₂ + m₃)).inv.app X ≫
        𝟙 ((h.F (m₁ + (m₂ + m₃))).obj X) ≫ (h.add m₁ (m₂ + m₃)).hom.app X ≫ (h.add m₂ m₃).hom.app ((h.F m₁).obj X)

Tactic:
Category.id_comp,

Goal state after:
C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
m₁ m₂ m₃ : A
X : C
⊢ 𝟙 ((h.F m₃).obj ((h.F m₁ ⋙ h.F m₂).obj X)) =
    (h.add m₂ m₃).inv.app ((h.F m₁).obj X) ≫
      (h.add m₁ (m₂ + m₃)).inv.app X ≫ (h.add m₁ (m₂ + m₃)).hom.app X ≫ (h.add m₂ m₃).hom.app ((h.F m₁).obj X)
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 (0 + n)).obj X) = eqToHom ⋯ ≫ 𝟙 ((h.F n).obj ((𝟭 C).obj X)) ≫ eqToHom ⋯

Tactic:
Category.id_comp,

Goal state after:
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 (0 + n)).obj X) = eqToHom ⋯ ≫ eqToHom ⋯
Module: Mathlib.Algebra.Homology.Single

Goal state before:
pp: case neg
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex V c
j : ι
A : V
φ : K.X j ⟶ A
hφ : ∀ (i : ι), c.Rel i j → K.d i j ≫ φ = 0
i k : ι
hik : c.Rel i k
hk : ¬k = j
⊢ 0 = K.d i k ≫ 0

Tactic:
· apply (isZero_single_obj_X c j A k hk).eq_of_tgt

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
J : Type u_3
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_3} J
c : ComplexShape ι
inst✝¹ : HasZeroMorphisms C
F : J ⥤ HomologicalComplex C c
inst✝ : ∀ (n : ι), HasLimit (F ⋙ eval C c n)
n m : ι
h : ¬c.Rel n m
j : J
⊢ limit.π (F ⋙ eval C c n) j ≫ (F.obj j).d n m = 0 ≫ limit.π (F ⋙ eval C c m) j

Tactic:
rw [(F.obj j).shape _ _ h, comp_zero, zero_comp]

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

Goal state before:
pp: case e_a
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
⊢ 𝟙 ((shiftFunctor C 0).obj X) =
    (shiftFunctorAdd' C n' n 0 hn).hom.app X ≫
      𝟙 ((shiftFunctor C n).obj ((shiftFunctor C n').obj X)) ≫ (shiftFunctorAdd' C n' n 0 ⋯).inv.app X

Tactic:
Category.id_comp,

Goal state after:
case e_a
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
⊢ 𝟙 ((shiftFunctor C 0).obj X) = (shiftFunctorAdd' C n' n 0 hn).hom.app X ≫ (shiftFunctorAdd' C n' n 0 ⋯).inv.app X
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
⊢ 𝟙 ((shiftFunctor C p).obj ((shiftFunctor C p').obj X)) =
    (shiftFunctor C p).map ((shiftFunctorAdd' C n' m' p' ⋯).hom.app X) ≫
      (shiftFunctorAdd' C m n p h).hom.app ((shiftFunctor C m').obj ((shiftFunctor C n').obj X)) ≫
        𝟙 ((shiftFunctor C n).obj ((shiftFunctor C m).obj ((shiftFunctor C m').obj ((shiftFunctor C n').obj X)))) ≫
          (shiftFunctorAdd' C m n p h).inv.app ((shiftFunctor C m').obj ((shiftFunctor C n').obj X)) ≫
            (shiftFunctor C p).map ((shiftFunctorAdd' C n' m' p' ⋯).inv.app X)

Tactic:
Category.id_comp,

Goal state after:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
⊢ 𝟙 ((shiftFunctor C p).obj ((shiftFunctor C p').obj X)) =
    (shiftFunctor C p).map ((shiftFunctorAdd' C n' m' p' ⋯).hom.app X) ≫
      (shiftFunctorAdd' C m n p h).hom.app ((shiftFunctor C m').obj ((shiftFunctor C n').obj X)) ≫
        (shiftFunctorAdd' C m n p h).inv.app ((shiftFunctor C m').obj ((shiftFunctor C n').obj X)) ≫
          (shiftFunctor C p).map ((shiftFunctorAdd' C n' m' p' ⋯).inv.app X)