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
hf : f.IsIntegral
⊢ IsClosedMap (comap f)

Tactic:
refine fun s hs ↦ isClosed_image_of_stableUnderSpecialization _ _ hs ?_
  rintro _ y e ⟨x, hx, rfl⟩
  algebraize [f]
  obtain ⟨q, hq₁, hq₂, hq₃⟩ := Ideal.exists_ideal_over_prime_of_isIntegral y.asIdeal x.asIdeal
    ((le_iff_specializes _ _).mpr e)
  refine ⟨⟨q, hq₂⟩, ((le_iff_specializes _ ⟨q, hq₂⟩).mp hq₁).mem_closed hs hx,
    PrimeSpectrum.ext hq₃⟩

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

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : IsSimpleGroup α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
hα : orderOf g ≠ 1
h : ∀ (n : ℕ), orderOf g ∣ n ∨ n.Coprime (orderOf g)
⊢ ∀ m < orderOf g, m ≠ 0 → (orderOf g).Coprime m

Tactic:
intro n

Goal state after:
case h
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : IsSimpleGroup α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
hα : orderOf g ≠ 1
h : ∀ (n : ℕ), orderOf g ∣ n ∨ n.Coprime (orderOf g)
n : ℕ
⊢ n < orderOf g → n ≠ 0 → (orderOf g).Coprime n
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: α : Type u_1
inst✝¹ : Group α
inst✝ : IsCyclic α
g : α
hg : orderOf g = Nat.card α
⊢ Nat.card α ∣ exponent α

Tactic:
← hg

Goal state after:
α : Type u_1
inst✝¹ : Group α
inst✝ : IsCyclic α
g : α
hg : orderOf g = Nat.card α
⊢ orderOf g ∣ exponent α
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: n : ℕ
⊢ AddMonoid.exponent (ZMod n) = n

Tactic:
IsAddCyclic.exponent_eq_card,

Goal state after:
n : ℕ
⊢ Nat.card (ZMod n) = n
Module: Mathlib.RingTheory.SimpleModule.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : Ring S
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
m : Submodule R M
N : Type u_5
inst✝¹ : AddCommGroup N
inst✝ : Module R N
hR : IsSemisimpleRing R
hS : IsSemisimpleRing S
⊢ IsSemisimpleRing (R × S)

Tactic:
let : Module (R × S) R := Module.compHom _ (.fst R S)
  let : Module (R × S) S := Module.compHom _ (.snd R S)
  -- e₁, e₂ got falsely flagged by the unused argument linter
  let _e₁ : R →ₛₗ[.fst R S] R := { AddMonoidHom.id R with map_smul' := fun _ _ ↦ rfl }
  let _e₂ : S →ₛₗ[.snd R S] S := { AddMonoidHom.id S with map_smul' := fun _ _ ↦ rfl }
  rw [IsSemisimpleRing, ← _e₁.isSemisimpleModule_iff_of_bijective Function.bijective_id] at hR
  rw [IsSemisimpleRing, ← _e₂.isSemisimpleModule_iff_of_bijective Function.bijective_id] at hS
  rw [IsSemisimpleRing, ← Submodule.topEquiv.isSemisimpleModule_iff_of_bijective
    (LinearEquiv.bijective _), ← LinearMap.sup_range_inl_inr]
  exact .sup (.range _) (.range _)

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

Goal state before:
pp: case succ
R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn :
  ∀ (r : R) (j : ℕ) (m : M),
    r •
        (⇑(↑(coeffLinearEquiv R R).symm ∘ₗ Finsupp.lmapDomain M R Nat.succ ∘ₗ ↑(coeffLinearEquiv R R)))^[n]
          (single R j m) =
      single R (n + j) (r • m)
r : R
j : ℕ
m : M
⊢ r •
      (⇑(↑(coeffLinearEquiv R R).symm ∘ₗ Finsupp.lmapDomain M R Nat.succ ∘ₗ ↑(coeffLinearEquiv R R)))^[n + 1]
        (single R j m) =
    single R (n + 1 + j) (r • m)

Tactic:
Function.iterate_succ,

Goal state after:
case succ
R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn :
  ∀ (r : R) (j : ℕ) (m : M),
    r •
        (⇑(↑(coeffLinearEquiv R R).symm ∘ₗ Finsupp.lmapDomain M R Nat.succ ∘ₗ ↑(coeffLinearEquiv R R)))^[n]
          (single R j m) =
      single R (n + j) (r • m)
r : R
j : ℕ
m : M
⊢ r •
      ((⇑(↑(coeffLinearEquiv R R).symm ∘ₗ Finsupp.lmapDomain M R Nat.succ ∘ₗ ↑(coeffLinearEquiv R R)))^[n] ∘
          ⇑(↑(coeffLinearEquiv R R).symm ∘ₗ Finsupp.lmapDomain M R Nat.succ ∘ₗ ↑(coeffLinearEquiv R R)))
        (single R j m) =
    single R (n + 1 + j) (r • m)
Module: Mathlib.Algebra.Polynomial.Module.AEval

Goal state before:
pp: R : Type u_3
A : Type u_1
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
inst✝ : FaithfulSMul A M
p : R[X]
⊢ (∀ (m : M), (aeval a) p • m = 0) ↔ (aeval a) p = 0

Tactic:
exact ⟨fun h ↦ eq_of_smul_eq_smul (α := M) <| by simp [h], fun h ↦ by simp [h]⟩

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

Goal state before:
pp: case a.refine_1
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : (↑S).Pairwise fun i j ↦ p i ⊔ p j = ⊤
h : S.Nonempty
x : M
hx : ∀ (a : ↑↑(⨅ i ∈ S, p i)), ↑a • x = 0
μ : (i : ι) → ↥(⨅ j ∈ S, ⨅ (_ : j ≠ i), p j)
hμ : ∑ i ∈ S, ↑(μ i) = 1
i : ι
a : R
ha : a ∈ ↑(p i)
⊢ a * ↑(μ i) ∈ ⨅ i ∈ S, p i

Tactic:
rw [mem_iInf]

Goal state after:
case a.refine_1
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : (↑S).Pairwise fun i j ↦ p i ⊔ p j = ⊤
h : S.Nonempty
x : M
hx : ∀ (a : ↑↑(⨅ i ∈ S, p i)), ↑a • x = 0
μ : (i : ι) → ↥(⨅ j ∈ S, ⨅ (_ : j ≠ i), p j)
hμ : ∑ i ∈ S, ↑(μ i) = 1
i : ι
a : R
ha : a ∈ ↑(p i)
⊢ ∀ (i_1 : ι), a * ↑(μ i) ∈ ⨅ (_ : i_1 ∈ S), p i_1
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: case a.refine_1
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : (↑S).Pairwise fun i j ↦ p i ⊔ p j = ⊤
h : S.Nonempty
x : M
hx : ∀ (a : ↑↑(⨅ i ∈ S, p i)), ↑a • x = 0
μ : (i : ι) → ↥(⨅ j ∈ S, ⨅ (_ : j ≠ i), p j)
hμ : ∑ i ∈ S, ↑(μ i) = 1
i : ι
a : R
ha : a ∈ ↑(p i)
j : ι
⊢ a * ↑(μ i) ∈ ⨅ (_ : j ∈ S), p j

Tactic:
rw [mem_iInf]

Goal state after:
case a.refine_1
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : (↑S).Pairwise fun i j ↦ p i ⊔ p j = ⊤
h : S.Nonempty
x : M
hx : ∀ (a : ↑↑(⨅ i ∈ S, p i)), ↑a • x = 0
μ : (i : ι) → ↥(⨅ j ∈ S, ⨅ (_ : j ≠ i), p j)
hμ : ∑ i ∈ S, ↑(μ i) = 1
i : ι
a : R
ha : a ∈ ↑(p i)
j : ι
⊢ j ∈ S → a * ↑(μ i) ∈ p j
Module: Mathlib.RingTheory.Finiteness.Nakayama

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
hin : N ≤ I • N
s : Set M
hfs : s.Finite
hs : span R s = N
⊢ N ≤ comap ((LinearMap.lsmul R M) 1) (I • N)

Tactic:
intro n

Goal state after:
case refine_2
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
hin : N ≤ I • N
s : Set M
hfs : s.Finite
hs : span R s = N
n : M
⊢ n ∈ N → n ∈ comap ((LinearMap.lsmul R M) 1) (I • N)
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) ⊔ 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:
rw [Set.insert_subset_iff] at hs

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 : i ∈ ↑N ∧ 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 insert.refine_2
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
i : M
s : Set M
a✝ : i ∉ s
hs✝ : s.Finite
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap ((LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) → ∃ r, r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0
r : R
hr1 : r - 1 ∈ I
hrn : N ≤ comap ((LinearMap.lsmul R M) r) (I • (R ∙ i) ⊔ I • span R s)
hs : i ∈ ↑N ∧ s ⊆ ↑N
c : R
hc1 : c - 1 ∈ I
hci : c • i ∈ I • span R s
⊢ N ≤ comap ((LinearMap.lsmul R M) (c * r)) (I • span R s)

Tactic:
intro n

Goal state after:
case insert.refine_2
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
i : M
s : Set M
a✝ : i ∉ s
hs✝ : s.Finite
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap ((LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) → ∃ r, r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0
r : R
hr1 : r - 1 ∈ I
hrn : N ≤ comap ((LinearMap.lsmul R M) r) (I • (R ∙ i) ⊔ I • span R s)
hs : i ∈ ↑N ∧ s ⊆ ↑N
c : R
hc1 : c - 1 ∈ I
hci : c • i ∈ I • span R s
n : M
⊢ n ∈ N → n ∈ comap ((LinearMap.lsmul R M) (c * r)) (I • span R s)
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
S : Type u_3
inst✝² : CommMonoid S
inst✝¹ : DistribMulAction S M
inst✝ : SMulCommClass S R M
h : torsion' R M S = ⊤
x : M
⊢ ∃ a, a • x = 0

Tactic:
by
    rw [← @mem_torsion'_iff R, h]
    trivial

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
I J : Ideal R
N : Submodule R M
hN : N.FG
hIN : N ≤ I • N
hIjac : I ≤ J.jacobson
⊢ N ≤ J • N

Tactic:
intro n

Goal state after:
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 : M
⊢ n ∈ N → n ∈ J • N
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), (∏ i ∈ S, ↑⋯.choose) • ↑n = 0

Tactic:
intro n

Goal state after:
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
⊢ (∏ i ∈ S, ↑⋯.choose) • ↑n = 0
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : I.Filtration M
S : Set (I.Filtration M)
i : ℕ
⊢ sSup (N '' S) (i + 1) ≤ sSup (N '' S) i

Tactic:
by
        apply sSup_le_sSup_of_isCofinalFor _
        rintro _ ⟨⟨_, F, hF, rfl⟩, rfl⟩
        exact ⟨_, ⟨⟨_, F, hF, rfl⟩, rfl⟩, F.mono i⟩

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 ≥ 0, I • (I.stableFiltration N).N n = (I.stableFiltration N).N (n + 1)

Tactic:
intro n

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 : ℕ
⊢ n ≥ 0 → I • (I.stableFiltration N).N n = (I.stableFiltration N).N (n + 1)
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
F : I.Filtration M
h : F.Stable
n₀ : ℕ
hn₀ : ∀ (k : ℕ), F.N (n₀ + k) = I ^ k • F.N n₀
⊢ ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀

Tactic:
intro n

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
F : I.Filtration M
h : F.Stable
n₀ : ℕ
hn₀ : ∀ (k : ℕ), F.N (n₀ + k) = I ^ k • F.N n₀
n : ℕ
⊢ n ≥ n₀ → F.N n = I ^ (n - n₀) • F.N n₀
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
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 : ℕ), F.N (n + n₀) ≤ F'.N n

Tactic:
intro n

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
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 : ℕ
⊢ F.N (n + n₀) ≤ F'.N n
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
F F' : I.Filtration M
h : F.Stable
h' : F'.Stable
e : F.N 0 = F'.N 0
n₁ : ℕ
h₁ : ∀ (n : ℕ), F.N (n + n₁) ≤ F'.N n
n₂ : ℕ
h₂ : ∀ (n : ℕ), F'.N (n + n₂) ≤ F.N n
⊢ ∀ (n : ℕ), F.N (n + max n₁ n₂) ≤ F'.N n ∧ F'.N (n + max n₁ n₂) ≤ F.N n

Tactic:
intro n

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
F F' : I.Filtration M
h : F.Stable
h' : F'.Stable
e : F.N 0 = F'.N 0
n₁ : ℕ
h₁ : ∀ (n : ℕ), F.N (n + n₁) ≤ F'.N n
n₂ : ℕ
h₂ : ∀ (n : ℕ), F'.N (n + n₂) ≤ F.N n
n : ℕ
⊢ F.N (n + max n₁ n₂) ≤ F'.N n ∧ F'.N (n + max n₁ n₂) ≤ F.N n
Module: Mathlib.RingTheory.Filtration

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

Tactic:
rw [Subalgebra.smul_def, PolynomialModule.smul_apply]
    apply Submodule.sum_mem
    rintro ⟨j, k⟩ e
    rw [Finset.mem_antidiagonal] at e
    subst e
    exact F.pow_smul_le j k (Submodule.smul_mem_smul (r.2 j) (hf k))

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I : Ideal R
⊢ Submodule.map (Submodule.subtype I) (I • ⊤) = I ^ 2

Tactic:
pow_two,

Goal state after:
R : Type u
inst✝ : CommRing R
I : Ideal R
⊢ Submodule.map (Submodule.subtype I) (I • ⊤) = I * I
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I : Ideal R
x : I.Cotangent
hx : I.cotangentToQuotientSquare x = 0
⊢ x = 0

Tactic:
obtain ⟨x, rfl⟩ := I.toCotangent_surjective x

Goal state after:
R : Type u
inst✝ : CommRing R
I : Ideal R
x : ↥I
hx : I.cotangentToQuotientSquare (I.toCotangent x) = 0
⊢ I.toCotangent x = 0
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: case mp.refine_1
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
⊢ Monotone fun n₀ ↦ Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i))

Tactic:
intro n

Goal state after:
case mp.refine_1
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 : ℕ
⊢ ∀ ⦃b : ℕ⦄,
    n ≤ b →
      (fun n₀ ↦ Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i))) n ≤
        (fun n₀ ↦ Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i))) b
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.Cotangent
e : ↑((fun c ↦ ⟨I.cotangentToQuotientSquare c, ⋯⟩) x) = ↑((fun c ↦ ⟨I.cotangentToQuotientSquare c, ⋯⟩) y)
⊢ x = y

Tactic:
obtain ⟨x, rfl⟩ := I.toCotangent_surjective x

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
y : I.Cotangent
x : ↥I
e :
  ↑((fun c ↦ ⟨I.cotangentToQuotientSquare c, ⋯⟩) (I.toCotangent x)) = ↑((fun c ↦ ⟨I.cotangentToQuotientSquare c, ⋯⟩) y)
⊢ I.toCotangent x = y
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
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra R S
I : Ideal S
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ↥I →ₗ[R] M
hf : ∀ (x y : ↥I), f (x * y) = 0
r : R
x : I.Cotangent
⊢ (↑(QuotientAddGroup.lift (I • ⊤).toAddSubgroup f.toAddMonoidHom ⋯)).toFun (r • x) =
    (RingHom.id R) r • (↑(QuotientAddGroup.lift (I • ⊤).toAddSubgroup f.toAddMonoidHom ⋯)).toFun x

Tactic:
obtain ⟨x, rfl⟩ := I.toCotangent_surjective x

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
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra R S
I : Ideal S
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ↥I →ₗ[R] M
hf : ∀ (x y : ↥I), f (x * y) = 0
r : R
x : ↥I
⊢ (↑(QuotientAddGroup.lift (I • ⊤).toAddSubgroup f.toAddMonoidHom ⋯)).toFun (r • I.toCotangent x) =
    (RingHom.id R) r • (↑(QuotientAddGroup.lift (I • ⊤).toAddSubgroup f.toAddMonoidHom ⋯)).toFun (I.toCotangent x)
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
I : Ideal R
x : I.Cotangent
__spread✝⁻⁰ : I.Cotangent →ₗ[R] I.Cotangent := lift (I.toCotangent ∘ₗ ↑(LinearEquiv.ofEq I I ⋯)) ⋯
⊢ (lift (I.toCotangent ∘ₗ ↑(LinearEquiv.ofEq I I ⋯)) ⋯)
      ((lift (I.toCotangent ∘ₗ ↑(LinearEquiv.ofEq I I ⋯)) ⋯).toFun x) =
    x

Tactic:
obtain ⟨x, rfl⟩ := I.toCotangent_surjective x

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
I : Ideal R
__spread✝⁻⁰ : I.Cotangent →ₗ[R] I.Cotangent := lift (I.toCotangent ∘ₗ ↑(LinearEquiv.ofEq I I ⋯)) ⋯
x : ↥I
⊢ (lift (I.toCotangent ∘ₗ ↑(LinearEquiv.ofEq I I ⋯)) ⋯)
      ((lift (I.toCotangent ∘ₗ ↑(LinearEquiv.ofEq I I ⋯)) ⋯).toFun (I.toCotangent x)) =
    I.toCotangent x
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
I : Ideal R
__spread✝⁻⁰ : I.Cotangent →ₗ[R] I.Cotangent := lift (I.toCotangent ∘ₗ ↑(LinearEquiv.ofEq I I ⋯)) ⋯
x : I.Cotangent
⊢ (lift (I.toCotangent ∘ₗ ↑(LinearEquiv.ofEq I I ⋯)) ⋯).toFun
      ((lift (I.toCotangent ∘ₗ ↑(LinearEquiv.ofEq I I ⋯)) ⋯) x) =
    x

Tactic:
obtain ⟨x, rfl⟩ := I.toCotangent_surjective x

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
I : Ideal R
__spread✝⁻⁰ : I.Cotangent →ₗ[R] I.Cotangent := lift (I.toCotangent ∘ₗ ↑(LinearEquiv.ofEq I I ⋯)) ⋯
x : ↥I
⊢ (lift (I.toCotangent ∘ₗ ↑(LinearEquiv.ofEq I I ⋯)) ⋯).toFun
      ((lift (I.toCotangent ∘ₗ ↑(LinearEquiv.ofEq I I ⋯)) ⋯) (I.toCotangent x)) =
    I.toCotangent x
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
⊢ finrank (ResidueField R) (CotangentSpace R) ≤ 1 ↔ Submodule.IsPrincipal (maximalIdeal R)

Tactic:
rw [Module.finrank_le_one_iff_top_isPrincipal, isPrincipal_iff,
    (maximalIdeal R).toCotangent_surjective.exists, isPrincipal_iff]

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
⊢ (∃ x, ⊤ = ResidueField R ∙ (maximalIdeal R).toCotangent x) ↔ ∃ a, maximalIdeal R = R ∙ a
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 : Cᵒᵖ
⊢ ↑((fun f ↦ sectionsMk (fun X ↦ (ConcreteCategory.hom (f.app X)) 1) ⋯)
          ((fun s ↦
              { app := fun X ↦ ModuleCat.ofHom ((ringLmapEquivSelf ↑(R.obj X) ℤ ↑(M.obj X)).symm (↑s X)),
                naturality := ⋯ })
            s))
      X =
    ↑s X

Tactic:
exact (LinearMap.ringLmapEquivSelf (R.obj X) ℤ (M.obj X)).apply_symm_apply (s.val X)

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
β : Type w
⊢ HasZeroObject (GradedObject β C)

Tactic:
refine ⟨⟨fun _ => 0, fun X => ⟨⟨⟨fun b => 0⟩, fun f => ?_⟩⟩, fun X =>
    ⟨⟨⟨fun b => 0⟩, fun f => ?_⟩⟩⟩⟩

Goal state after:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
β : Type w
X : GradedObject β C
f : (fun x ↦ 0) ⟶ X
⊢ f = default

case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
β : Type w
X : GradedObject β C
f : X ⟶ fun x ↦ 0
⊢ f = default
Module: Mathlib.Algebra.Homology.Single

Goal state before:
pp: V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A : V
⊢ { f := fun i ↦ if h : i = j then eqToHom ⋯ ≫ 𝟙 A ≫ eqToHom ⋯ else 0, comm' := ⋯ } =
    𝟙 { X := fun i ↦ if i = j then A else 0, d := fun x x_1 ↦ 0, shape := ⋯, d_comp_d' := ⋯ }

Tactic:
ext
    dsimp
    split_ifs with h
    · subst h
      simp
    · #adaptation_note /-- nightly-2024-03-07
      previously was `rw [if_neg h]; simp`, but that fails with "motive not type correct"
      This is because dsimp does not simplify numerals;
      this note should be removable once https://github.com/leanprover/lean4/pull/8433 lands. -/
      convert! (id_zero (C := V)).symm
      all_goals simp [if_neg h]

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

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

Tactic:
by dsimp; rw [zero_add]

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

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

Tactic:
by dsimp; rw [zero_add]

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

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
X : C
⊢ (shiftFunctor C (0 + a)).obj X = (shiftFunctor C a).obj ((𝟭 C).obj X)

Tactic:
by dsimp; rw [zero_add]

Goal state after: