mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Coprime.Ideal

Goal state before:
pp: case refine_2
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
⊢ ∀ (a : ι) (s : Finset ι) (h : a ∉ s),
    s.Nonempty →
      ((∃ μ, ∑ i ∈ s, ↑(μ i) = 1) ↔ (↑s).Pairwise fun i j ↦ I i ⊔ I j = ⊤) →
        ((∃ μ, ∑ i ∈ Finset.cons a s h, ↑(μ i) = 1) ↔ (↑(Finset.cons a s h)).Pairwise fun i j ↦ I i ⊔ I j = ⊤)

Tactic:
intro a t hat h ih

Goal state after:
case refine_2
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
⊢ (∃ μ, ∑ i ∈ Finset.cons a t hat, ↑(μ i) = 1) ↔ (↑(Finset.cons a t hat)).Pairwise fun i j ↦ I i ⊔ I j = ⊤
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝¹ : Group G
p : ℕ
inst✝ : Subsingleton (Sylow p G)
P : Sylow p G
ϕ : G ≃* G
h : ↑P = Subgroup.map ((MulDistribMulAction.toMonoidEnd (G ≃* G) G) ϕ) ↑P
⊢ Subgroup.map ϕ.toMonoidHom ↑P = ↑P

Tactic:
eq_comm

Goal state after:
G : Type u
inst✝¹ : Group G
p : ℕ
inst✝ : Subsingleton (Sylow p G)
P : Sylow p G
ϕ : G ≃* G
h : Subgroup.map ((MulDistribMulAction.toMonoidEnd (G ≃* G) G) ϕ) ↑P = ↑P
⊢ Subgroup.map ϕ.toMonoidHom ↑P = ↑P
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
R : Type u_6
inst✝² : DivisionRing R
inst✝¹ : Module R M
inst✝ : Nontrivial M
v : M
hv : v ≠ 0
w : M
f : M →ₗ[R] M
eq : f ∘ₗ toSpanSingleton R M v = toSpanSingleton R M w
⊢ (toSpanSingleton (Module.End R M) M v) f = w

Tactic:
by simpa using congr($eq 1)

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
s : Set R
⊢ (∀ ⦃x : M⦄ ⦃a : ↑s⦄, ↑a • x = 0) ↔ s ⊆ ↑(annihilator R M)

Tactic:
Set.subset_def,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
⊢ (∀ ⦃x : M⦄ ⦃a : ↑s⦄, ↑a • x = 0) ↔ ∀ x ∈ s, x ∈ ↑(annihilator R M)
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 : Set R
x : M
hx : ∀ (a : ↑s), ↑a • x = 0
this : Ideal.span s ≤ Ideal.torsionOf R M x
⊢ ∀ (a : ↑↑(Ideal.span s)), ↑a • x = 0

Tactic:
rintro ⟨a, ha⟩

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
x : M
hx : ∀ (a : ↑s), ↑a • x = 0
this : Ideal.span s ≤ Ideal.torsionOf R M x
a : R
ha : a ∈ ↑(Ideal.span s)
⊢ ↑⟨a, ha⟩ • x = 0
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✝¹ : IsSemisimpleModule R M
inst✝ : Module.Finite (End R M) M
⊢ Function.Surjective ⇑(toModuleEnd (End R M) M)

Tactic:
have ⟨s, hs⟩ := Module.Finite.fg_top (R := End R M) (M := M)
  intro f
  have ⟨r, hr⟩ := jacobson_density f s
  refine ⟨r, LinearMap.ext fun m ↦ ?_⟩
  induction hs.ge (trivial : m ∈ ⊤) using Submodule.span_induction with
  | mem m hm => exact (hr m hm).symm
  | zero => simp
  | add _ _ _ _ h₁ h₂ => simpa using congr($h₁ + $h₂)
  | smul g _ _ h => simp_rw [map_smul, 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 : ↑↑(p i)), ↑a • ↑(μ i) • x = 0

Tactic:
rintro ⟨a, ha⟩

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)
⊢ ↑⟨a, ha⟩ • ↑(μ i) • x = 0
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: case pos
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 : ι
hj : j ∈ S
ij : j = i
⊢ a * ↑(μ i) ∈ p j

Tactic:
rw [ij]
        exact Ideal.mul_mem_right _ _ ha

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
hM : IsTorsion R M
⊢ (↑⊤.annihilator ∩ ↑R⁰).Nonempty

Tactic:
by
  obtain ⟨S, hS⟩ := ‹Module.Finite R M›.fg_top
  refine ⟨_, ?_, (∏ x ∈ S, (@hM x).choose : R⁰).prop⟩
  rw [Submonoid.coe_finsetProd, SetLike.mem_coe, ← hS, mem_annihilator_span]
  intro n
  let := Classical.decEq M
  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: 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
i j k : ℕ
⊢ I ^ (i + k) • F.N j ≤ I ^ k • F.N (i + j)

Tactic:
add_comm,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
i j k : ℕ
⊢ I ^ (k + i) • F.N j ≤ I ^ k • F.N (i + j)
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
I : Ideal R
N : Submodule R M
i : ℕ
⊢ I ^ (i + 1) • N ≤ I ^ i • N

Tactic:
add_comm,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I✝ : Ideal R
F F' : I✝.Filtration M
I : Ideal R
N : Submodule R M
i : ℕ
⊢ I ^ (1 + i) • N ≤ I ^ i • 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
I : Ideal R
N : Submodule R M
i : ℕ
⊢ I • I ^ i • N ≤ I ^ (i + 1) • N

Tactic:
add_comm,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I✝ : Ideal R
F F' : I✝.Filtration M
I : Ideal R
N : Submodule R M
i : ℕ
⊢ I • I ^ i • N ≤ I ^ (1 + i) • 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
N : Submodule R M
n : ℕ
a✝ : n ≥ 0
⊢ I • I ^ n • N = I ^ (n + 1) • N

Tactic:
add_comm,

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 ^ (1 + n) • N
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 : I.Filtration M
n₀ : ℕ
hn : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
n✝ : ℕ
ih : F.N (n₀ + n✝) = I ^ n✝ • F.N n₀
⊢ I • I ^ n✝ • F.N n₀ = I ^ (n✝ + 1) • F.N n₀

pp: 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 : I.Filtration M
n₀ : ℕ
hn : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
n✝ : ℕ
ih : F.N (n₀ + n✝) = I ^ n✝ • F.N n₀
⊢ n₀ + n✝ ≥ n₀

Tactic:
add_comm,

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 : I.Filtration M
n₀ : ℕ
hn : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
n✝ : ℕ
ih : F.N (n₀ + n✝) = I ^ n✝ • F.N n₀
⊢ I • I ^ n✝ • F.N n₀ = I ^ (1 + n✝) • F.N n₀

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

Tactic:
add_comm,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
h : F.Stable
n₀ : ℕ
hn₀ : ∀ (k : ℕ), F.N (n₀ + k) = I ^ k • F.N n₀
n : ℕ
hn : n ≥ n₀
⊢ n = n - n₀ + n₀
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
F : I.Filtration M
n₀ : ℕ
⊢ (∀ (i : ℕ),
      single R i '' ↑(F.N i) ⊆ ↑(Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i)))) →
    ∀ n ≥ n₀, I • F.N n = F.N (n + 1)

Tactic:
intro H

Goal state after:
case mp
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
n₀ : ℕ
H :
  ∀ (i : ℕ), single R i '' ↑(F.N i) ⊆ ↑(Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i)))
⊢ ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
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
      rw [← f.hom.map_one, d_map]

Goal state after:
Module: Mathlib.RingTheory.Filtration

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

Tactic:
add_comm,

Goal state after:
case neg.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
n₀ : ℕ
F' : Submodule (↥(reesAlgebra I)) (PolynomialModule R M) :=
  Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i))
hF : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
this : ∀ i ≤ n₀, single R i '' ↑(F.N i) ⊆ ↑F'
j : ℕ
hj : single R j '' ↑(F.N j) ⊆ ↑(Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i)))
hj' : n₀ ≤ j
m : M
hm : m ∈ ↑(I • F.N j)
r : R
hr : r ∈ I
m' : M
hm' : m' ∈ F.N j
⊢ single R (1 + j) (r • m') ∈ ↑(Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i)))
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I : Ideal R
x y : ↥I
⊢ I.toCotangent x - I.toCotangent y = 0 ↔ ↑x - ↑y ∈ I ^ 2

Tactic:
exact I.mem_toCotangent_ker

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

Goal state before:
pp: case mp
R : Type u
inst✝ : CommRing R
I : Ideal R
⊢ Subsingleton I.Cotangent → IsIdempotentElem I

Tactic:
intro H

Goal state after:
case mp
R : Type u
inst✝ : CommRing R
I : Ideal R
H : Subsingleton I.Cotangent
⊢ IsIdempotentElem I
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
⊢ (RingHom.ker f.toRingHom).cotangentIdeal ≤ RingHom.ker f.kerSquareLift.toRingHom

Tactic:
rintro _ ⟨x, hx, rfl⟩; exact hx

Goal state after:
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 := ⨅ i, I ^ i • ⊤
hN : ∀ (k : ℕ), (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N k = N
r : R
hr₁ : r ∈ I
hr₂ : ∀ n ∈ N, r • n = n
⊢ x ∈ ⨅ i, I ^ i • ⊤ → ∃ r, ↑r • x = x

Tactic:
intro H

Goal state after:
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 := ⨅ i, I ^ i • ⊤
hN : ∀ (k : ℕ), (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N k = N
r : R
hr₁ : r ∈ I
hr₂ : ∀ n ∈ N, r • n = n
H : x ∈ ⨅ i, I ^ i • ⊤
⊢ ∃ r, ↑r • x = x
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: case mpr.succ
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
I : Ideal R
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
x : M
N : Submodule R M := ⨅ i, I ^ i • ⊤
hN : ∀ (k : ℕ), (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N k = N
r : ↥I
eq : ↑r • x = x
i : ℕ
hi : x ∈ I ^ i • ⊤
⊢ x ∈ I ^ (i + 1) • ⊤

Tactic:
add_comm,

Goal state after:
case mpr.succ
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
I : Ideal R
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
x : M
N : Submodule R M := ⨅ i, I ^ i • ⊤
hN : ∀ (k : ℕ), (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N k = N
r : ↥I
eq : ↑r • x = x
i : ℕ
hi : x ∈ I ^ i • ⊤
⊢ x ∈ I ^ (1 + i) • ⊤
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)]
  apply le_antisymm
  · obtain ⟨s, hs_card, hs_span⟩ :=
      (⊤ : Submodule R (maximalIdeal R)).exists_span_set_card_eq_spanRank
    have hs_span' : Submodule.span (ResidueField R) ((maximalIdeal R).toCotangent '' s) = ⊤ := by
      rw [← Submodule.restrictScalars_eq_top_iff R,
        Submodule.restrictScalars_span R (ResidueField R) Ideal.Quotient.mk_surjective,
        ← Submodule.map_span, hs_span, Submodule.map_top, Ideal.toCotangent_range]
    rw [← hs_card, ← hs_span']
    grw [Submodule.spanRank_span_le_card, Cardinal.mk_image_le]
  · obtain ⟨s, hs_card, hs_span⟩ :=
      (⊤ : Submodule (ResidueField R) (CotangentSpace R)).exists_span_set_card_eq_spanRank
    have hs_span' : Submodule.span R s =
        Submodule.map (Submodule.mkQ (maximalIdeal R • (⊤ : Submodule R (maximalIdeal R)))) ⊤ := by
      rw [Submodule.map_top, Submodule.range_mkQ]
      change Submodule.span R s = ⊤
      rw [← Submodule.restrictScalars_span R (ResidueField R)
        Ideal.Quotient.mk_surjective, hs_span, Submodule.restrictScalars_top]
    obtain ⟨t, ht_inj, ht_image, ht_span⟩ :=
      Submodule.exists_injOn_mkQ_image_span_eq_of_span_eq_map_mkQ_of_le_jacobson_bot s
        ((Submodule.fg_top (maximalIdeal R)).mpr fg)
        (IsLocalRing.jacobson_eq_maximalIdeal _ bot_ne_top).ge
        hs_span'
    rw [← hs_card, ← ht_span, ← ht_image]
    exact le_of_le_of_eq (Submodule.spanRank_span_le_card t)
      (Cardinal.mk_image_eq_of_injOn _ _ ht_inj).symm

Goal state after:
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: case mp
R : Type u_3
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
I : Ideal R
⊢ IsIdempotentElem I → I = ⊥ ∨ I = ⊤

Tactic:
intro H

Goal state after:
case mp
R : Type u_3
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
I : Ideal R
H : IsIdempotentElem I
⊢ I = ⊥ ∨ I = ⊤
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
R : Dᵒᵖ ⥤ CommRingCat
M : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
φ : S ⟶ F.op ⋙ R
d : M.Derivation φ
X : Dᵒᵖ
⊢ d.d 1 = 0

Tactic:
by
  simpa using d.d_mul (X := X) 1 1

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
app : (X : Cᵒᵖ) → M₁.obj X ≅ M₂.obj X
naturality :
  ∀ ⦃X Y : Cᵒᵖ⦄ (f : X ⟶ Y),
    M₁.map f ≫ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map (app Y).hom = (app X).hom ≫ M₂.map f
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ M₁.map f ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map (app Y).hom ≫
        (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map (app Y).inv =
    (app X).hom ≫ (app X).inv ≫ M₁.map f

Tactic:
Iso.map_hom_inv_id,

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M M₁ M₂ : PresheafOfModules R
app : (X : Cᵒᵖ) → M₁.obj X ≅ M₂.obj X
naturality :
  ∀ ⦃X Y : Cᵒᵖ⦄ (f : X ⟶ Y),
    M₁.map f ≫ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map (app Y).hom = (app X).hom ≫ M₂.map f
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ M₁.map f ≫ 𝟙 ((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M₁.obj Y)) =
    (app X).hom ≫ (app X).inv ≫ M₁.map f
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
a b : S
this : LinearMap.CompatibleSMul ↥(ideal R S) Ω[S⁄R] S (S ⊗[R] S)
⊢ (ideal R S).toCotangent ⟨1 ⊗ₜ[R] (a * b) - (a * b) ⊗ₜ[R] 1, ⋯⟩ =
    (ideal R S).toCotangent (a • ⟨1 ⊗ₜ[R] b - b ⊗ₜ[R] 1, ⋯⟩ + b • ⟨1 ⊗ₜ[R] a - a ⊗ₜ[R] 1, ⋯⟩)

Tactic:
Ideal.toCotangent_eq,

Goal state after:
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
a b : S
this : LinearMap.CompatibleSMul ↥(ideal R S) Ω[S⁄R] S (S ⊗[R] S)
⊢ ↑⟨1 ⊗ₜ[R] (a * b) - (a * b) ⊗ₜ[R] 1, ⋯⟩ - ↑(a • ⟨1 ⊗ₜ[R] b - b ⊗ₜ[R] 1, ⋯⟩ + b • ⟨1 ⊗ₜ[R] a - a ⊗ₜ[R] 1, ⋯⟩) ∈
    ideal R S ^ 2
Module: Mathlib.Algebra.Homology.HomologicalComplex

Goal state before:
pp: case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ : V
d₀ : X₁ ⟶ X₀
succ' : {X₀ X₁ : V} → (f : X₁ ⟶ X₀) → (X₂ : V) ×' (d : X₂ ⟶ X₁) ×' d ≫ f = 0
⊢ (mk X₀ X₁ (succ' d₀).fst d₀ (succ' d₀).snd.fst ⋯ fun S ↦ succ' S.f).d 2 1 =
    (Nat.casesAuxOn 0 (eqToIso ⋯) fun n ↦
          mkXIso X₀ X₁ (succ' d₀).fst d₀ (succ' d₀).snd.fst ⋯ (fun S ↦ succ' S.f) n).hom ≫
      (succ' ((mk X₀ X₁ (succ' d₀).fst d₀ (succ' d₀).snd.fst ⋯ fun S ↦ succ' S.f).d 1 0)).snd.fst

Tactic:
rw [mk_d_2_1]

Goal state after:
case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ : V
d₀ : X₁ ⟶ X₀
succ' : {X₀ X₁ : V} → (f : X₁ ⟶ X₀) → (X₂ : V) ×' (d : X₂ ⟶ X₁) ×' d ≫ f = 0
⊢ (succ' d₀).snd.fst =
    (Nat.casesAuxOn 0 (eqToIso ⋯) fun n ↦
          mkXIso X₀ X₁ (succ' d₀).fst d₀ (succ' d₀).snd.fst ⋯ (fun S ↦ succ' S.f) n).hom ≫
      (succ' ((mk X₀ X₁ (succ' d₀).fst d₀ (succ' d₀).snd.fst ⋯ fun S ↦ succ' S.f).d 1 0)).snd.fst
Module: Mathlib.Algebra.Homology.HomologicalComplex

Goal state before:
pp: case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ : V
d₀ : X₁ ⟶ X₀
succ' : {X₀ X₁ : V} → (f : X₁ ⟶ X₀) → (X₂ : V) ×' (d : X₂ ⟶ X₁) ×' d ≫ f = 0
⊢ (succ' d₀).snd.fst =
    (Nat.casesAuxOn 0 (eqToIso ⋯) fun n ↦
          mkXIso X₀ X₁ (succ' d₀).fst d₀ (succ' d₀).snd.fst ⋯ (fun S ↦ succ' S.f) n).hom ≫
      (succ' ((mk X₀ X₁ (succ' d₀).fst d₀ (succ' d₀).snd.fst ⋯ fun S ↦ succ' S.f).d 1 0)).snd.fst

Tactic:
apply mk'_congr_succ'_d

Goal state after:
case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ : V
d₀ : X₁ ⟶ X₀
succ' : {X₀ X₁ : V} → (f : X₁ ⟶ X₀) → (X₂ : V) ×' (d : X₂ ⟶ X₁) ×' d ≫ f = 0
⊢ d₀ = (mk X₀ X₁ (succ' d₀).fst d₀ (succ' d₀).snd.fst ⋯ fun S ↦ succ' S.f).d 1 0
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
X✝ Y : C
f : X✝ ⟶ Y
m n : A
hmn : m + n = 0
X : C
⊢ n + m = 0

Tactic:
add_comm,

Goal state after:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
X✝ Y : C
f : X✝ ⟶ Y
m n : A
hmn : m + n = 0
X : C
⊢ m + n = 0
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
A : Type u_2
B : Type u_3
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra A B
inst✝⁴ : Algebra S B
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A B
inst✝¹ : IsScalarTower R S B
inst✝ : SMulCommClass S A B
h : Function.Surjective ⇑(algebraMap A B)
y : A
⊢ (D S B) ((algebraMap A B) y) ∈ ↑(map R S A B).range

Tactic:
rw [← KaehlerDifferential.map_D R S A B]

Goal state after:
R : Type u
S : Type v
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
A : Type u_2
B : Type u_3
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra A B
inst✝⁴ : Algebra S B
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A B
inst✝¹ : IsScalarTower R S B
inst✝ : SMulCommClass S A B
h : Function.Surjective ⇑(algebraMap A B)
y : A
⊢ (map R S A B) ((D R A) y) ∈ ↑(map R S A B).range
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
h : Function.Surjective ⇑(algebraMap A B)
⊢ Function.Surjective ⇑(mapBaseChange R A B)

Tactic:
by
  have := subsingleton_of_surjective A B h
  rw [← LinearMap.range_eq_top, range_mapBaseChange, ← top_le_iff]
  exact fun x _ ↦ Subsingleton.elim _ _

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

Goal state before:
pp: case h₁
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
j : ι
A : C
f g : X φ j ⟶ A
h₂ : inrX φ j ≫ f = inrX φ j ≫ g
hij : c.Rel j (c.next j)
h₁ : inlX φ (c.next j) j hij ≫ f = inlX φ (c.next j) j hij ≫ g
this : HasBinaryBiproduct (F.X (c.next j)) (G.X j)
⊢ biprod.inr ≫ (XIsoBiprod φ j (c.next j) hij).inv ≫ f = biprod.inr ≫ (XIsoBiprod φ j (c.next j) hij).inv ≫ g

Tactic:
simpa [-inr_XIsoBiprod_inv, -inr_XIsoBiprod_inv_assoc, inrX, dif_pos hij] using h₂

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
hom : (i j : ι) → C.X i ⟶ D.X j
i j : ι
hij : c.Rel i j
eq1 : (prevD i) hom ≫ D.d i j = 0
eq2 : C.d i j ≫ (dNext j) hom = 0
⊢ ((dNext i) hom + (prevD i) hom) ≫ D.d i j = C.d i j ≫ ((dNext j) hom + (prevD j) hom)

Tactic:
rw [dNext_eq hom hij, prevD_eq hom hij, Preadditive.comp_add, Preadditive.add_comp, eq1, eq2,
      add_zero, zero_add, assoc]

Goal state after: