mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.ModuleCat.Differentials.Basic

Goal state before:
pp: A B : CommRingCat
f : A ⟶ B
M : ModuleCat ↑B
α β : KaehlerDifferential f ⟶ M
h : ∀ (b : ↑B), (ConcreteCategory.hom α) (d b) = (ConcreteCategory.hom β) (d b)
⊢ ⊤ ≤ (ModuleCat.Hom.hom (α - β)).ker

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Differentials.Basic

Goal state before:
pp: A B : CommRingCat
f : A ⟶ B
M : ModuleCat ↑B
α β : KaehlerDifferential f ⟶ M
h : ∀ (b : ↑B), (ConcreteCategory.hom α) (d b) = (ConcreteCategory.hom β) (d b)
⊢ α = β

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Differentials.Basic

Goal state before:
pp: A B A' B' : CommRingCat
f : A ⟶ B
f' : A' ⟶ B'
g : A ⟶ A'
g' : B ⟶ B'
fac : g ≫ f' = f ≫ g'
this✝⁵ : Algebra ↑A ↑B := (Hom.hom f).toAlgebra
this✝⁴ : Algebra ↑A' ↑B' := (Hom.hom f').toAlgebra
this✝³ : Algebra ↑A ↑A' := (Hom.hom g).toAlgebra
this✝² : Algebra ↑B ↑B' := (Hom.hom g').toAlgebra
this✝¹ : Algebra ↑A ↑B' := (Hom.hom (g ≫ f')).toAlgebra
this✝ : IsScalarTower ↑A ↑A' ↑B'
this : IsScalarTower ↑A ↑B ↑B'
⊢ ∀ (x y : Ω[↑B⁄↑A]),
    (_root_.KaehlerDifferential.map ↑A ↑A' ↑B ↑B') (x + y) =
      (_root_.KaehlerDifferential.map ↑A ↑A' ↑B ↑B') x + (_root_.KaehlerDifferential.map ↑A ↑A' ↑B ↑B') y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Differentials.Basic

Goal state before:
pp: A B A' B' : CommRingCat
f : A ⟶ B
f' : A' ⟶ B'
g : A ⟶ A'
g' : B ⟶ B'
fac : g ≫ f' = f ≫ g'
this✝⁵ : Algebra ↑A ↑B := (Hom.hom f).toAlgebra
this✝⁴ : Algebra ↑A' ↑B' := (Hom.hom f').toAlgebra
this✝³ : Algebra ↑A ↑A' := (Hom.hom g).toAlgebra
this✝² : Algebra ↑B ↑B' := (Hom.hom g').toAlgebra
this✝¹ : Algebra ↑A ↑B' := (Hom.hom (g ≫ f')).toAlgebra
this✝ : IsScalarTower ↑A ↑A' ↑B'
this : IsScalarTower ↑A ↑B ↑B'
⊢ ∀ (m : ↑B) (x : Ω[↑B⁄↑A]),
    (_root_.KaehlerDifferential.map ↑A ↑A' ↑B ↑B') (m • x) =
      (RingHom.id ↑B) m • (_root_.KaehlerDifferential.map ↑A ↑A' ↑B ↑B') x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Differentials.Basic

Goal state before:
pp: A B A' B' : CommRingCat
f : A ⟶ B
f' : A' ⟶ B'
g : A ⟶ A'
g' : B ⟶ B'
fac : g ≫ f' = f ≫ g'
b : ↑B
⊢ (ConcreteCategory.hom (map fac)) (d b) = d ((ConcreteCategory.hom g') b)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Differentials.Basic

Goal state before:
pp: A B : CommRingCat
f : A ⟶ B
M : ModuleCat ↑B
D : M.Derivation f
b : ↑B
⊢ (ConcreteCategory.hom D.desc) (CommRingCat.KaehlerDifferential.d b) = D.d b

Tactic:
by

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
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
⊢ r ∈ I ^ 1

Tactic:
by

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.toCotangent.ker = I ^ 2

Tactic:
by

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

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

Tactic:
by

Goal state after:
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 ↔ ↑x - ↑y ∈ I ^ 2

Tactic:
by

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

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

Tactic:
by

Goal state after:
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
⊢ I • ⊤ ≤ Submodule.comap (Submodule.subtype I) (I ^ 2)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I : Ideal R
⊢ Function.Injective ⇑I.cotangentToQuotientSquare

Tactic:
by

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

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

Tactic:
by

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
n₀ : ℕ
⊢ F.submodule = Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i)) ↔
    ∀ n ≥ n₀, I • F.N n = F.N (n + 1)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I : Ideal R
⊢ I.cotangentIdeal ^ 2 = ⊥

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I : Ideal R
x : R
⊢ (Quotient.mk (I ^ 2)) x ∈ I.cotangentIdeal ↔ x ∈ I

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I : Ideal R
⊢ I.cotangentToQuotientSquare.range = Submodule.restrictScalars R I.cotangentIdeal

Tactic:
by

Goal state after:
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
x : I.Cotangent
⊢ I.cotangentToQuotientSquare x ∈ I.cotangentToQuotientSquare.range

Tactic:
exact LinearMap.mem_range_self _ _

Goal state after:
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
x : I.Cotangent
⊢ I.cotangentToQuotientSquare x ∈ Submodule.restrictScalars R I.cotangentIdeal

Tactic:
by

Goal state after:
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
⊢ I.Cotangent ≃ₗ[R] ↥I.cotangentIdeal

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I : Ideal R
x : R
hx : x ∈ I
⊢ I.cotangentEquivIdeal.symm ⟨(Submodule.mkQ (I ^ 2)) x, ⋯⟩ = I.toCotangent ⟨x, hx⟩

Tactic:
by

Goal state after:
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
f : A →ₐ[R] B
⊢ A ⧸ RingHom.ker f.toRingHom ^ 2 →ₐ[R] B

Tactic:
by

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

Goal state before:
pp: 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.kerSquareLift.toRingHom = (RingHom.ker f.toRingHom).cotangentIdeal

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
S' : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : CommSemiring S'
inst✝⁶ : Algebra S' R
inst✝⁵ : Algebra S S'
inst✝⁴ : IsScalarTower S S' R
I : Ideal R
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
⊢ (R ⧸ I ^ 2) ⧸ I.cotangentIdeal ≃+* R ⧸ I

Tactic:
by

Goal state after:
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 A
I₂ : Ideal B
f : A →ₐ[R] B
h : I₁ ≤ comap f I₂
⊢ I₁.Cotangent →ₗ[R] I₂.Cotangent

Tactic:
by

Goal state after:
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
x : ↥I
hx : x ∈ (I • ⊤).toAddSubgroup
⊢ x ∈ f.toAddMonoidHom.ker

Tactic:
by

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
hF' : ∀ (i : ℕ), (F.N i).FG
n : ℕ
hn : F.submodule = Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n), single R i '' ↑(F.N i))
i : ℕ
hi : i ∈ Finset.range n.succ
s : Finset M
hs : Submodule.span R ↑s = F.N i
⊢ Submodule.span ↥(reesAlgebra I) ↑(Finset.image (⇑(lsingle R i)) s) =
    Submodule.span (↥(reesAlgebra I)) (single R i '' ↑(F.N i))

Tactic:
by

Goal state after:
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:
by

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

Goal state before:
pp: case refine_1
R : Type u
inst✝⁴ : CommRing R
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
h : Function.Surjective ⇑(lift f hf)
⊢ Function.Surjective ⇑f

Tactic:
← Cotangent.lift_comp_toCotangent f hf,

Goal state after:
case refine_1
R : Type u
inst✝⁴ : CommRing R
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
h : Function.Surjective ⇑(lift f hf)
⊢ Function.Surjective ⇑(lift f hf ∘ₗ ↑R I.toCotangent)
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
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
⊢ Function.Surjective ⇑(lift f hf) ↔ Function.Surjective ⇑f

Tactic:
by

Goal state after:
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 J : Ideal R
hIJ : I = J
x y : ↥I
⊢ (J.toCotangent ∘ₗ ↑(LinearEquiv.ofEq I J hIJ)) (x * y) = 0

Tactic:
by

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
hF' : ∀ (i : ℕ), (F.N i).FG
⊢ F.submodule.FG ↔ F.Stable

Tactic:
by

Goal state after:
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 J : Ideal R
hIJ : I = J
x y : ↥J
⊢ (I.toCotangent ∘ₗ ↑(LinearEquiv.ofEq J I ⋯)) (x * y) = 0

Tactic:
by

Goal state after:
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 J : Ideal R
hIJ : I = J
x : I.Cotangent
⊢ (lift (I.toCotangent ∘ₗ ↑(LinearEquiv.ofEq J I ⋯)) ⋯)
      ((lift (J.toCotangent ∘ₗ ↑(LinearEquiv.ofEq I J hIJ)) ⋯).toFun x) =
    x

Tactic:
by

Goal state after:
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 J : Ideal R
hIJ : I = J
x : I.Cotangent
⊢ (lift (I.toCotangent ∘ₗ ↑(LinearEquiv.ofEq J I ⋯)) ⋯)
      ((lift (J.toCotangent ∘ₗ ↑(LinearEquiv.ofEq I J hIJ)) ⋯).toFun x) =
    x

Tactic:
by
    subst hIJ
    obtain ⟨x, rfl⟩ := I.toCotangent_surjective x
    simp

Goal state after:
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 J : Ideal R
hIJ : I = J
x : J.Cotangent
⊢ (lift (J.toCotangent ∘ₗ ↑(LinearEquiv.ofEq I J hIJ)) ⋯).toFun
      ((lift (I.toCotangent ∘ₗ ↑(LinearEquiv.ofEq J I ⋯)) ⋯) x) =
    x

Tactic:
by

Goal state after:
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 J : Ideal R
hIJ : I = J
x : J.Cotangent
⊢ (lift (J.toCotangent ∘ₗ ↑(LinearEquiv.ofEq I J hIJ)) ⋯).toFun
      ((lift (I.toCotangent ∘ₗ ↑(LinearEquiv.ofEq J I ⋯)) ⋯) x) =
    x

Tactic:
by
    subst hIJ
    obtain ⟨x, rfl⟩ := I.toCotangent_surjective x
    simp

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
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
hF : F.Stable
F' : I.Filtration M
hf : F' ≤ F
⊢ F'.Stable

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
⊢ Subsingleton (CotangentSpace R) ↔ IsField R

Tactic:
by

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
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
x : M
N : Submodule R M := ⨅ i, I ^ i • ⊤
k : ℕ
⊢ I ^ k • ⊤ = (I.stableFiltration ⊤).N k

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
M : Submodule R ↥(maximalIdeal R)
⊢ M = ⊤ → Submodule.map (maximalIdeal R).toCotangent M = ⊤

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
M : Submodule R ↥(maximalIdeal R)
⊢ Submodule.map (maximalIdeal R).toCotangent M = ⊤ ↔ M = ⊤

Tactic:
by

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
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
⊢ N ≤ I • N

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
s : Set ↥(maximalIdeal R)
⊢ Submodule.span (ResidueField R) (⇑(maximalIdeal R).toCotangent '' s) = ⊤ ↔ Submodule.span R s = ⊤

Tactic:
by

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 ↥(maximalIdeal R)
hs_card : Cardinal.mk ↑s = ⊤.spanRank
hs_span : Submodule.span R s = ⊤
⊢ Submodule.span (ResidueField R) (⇑(maximalIdeal R).toCotangent '' s) = ⊤

Tactic:
by

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:
by

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
⊢ Module.rank (ResidueField R) (CotangentSpace R) = Submodule.spanRank (maximalIdeal R)

Tactic:
by

Goal state after:
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) = 0 ↔ IsField R

Tactic:
by

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
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
x : M
⊢ x ∈ ⨅ i, I ^ i • ⊤ ↔ ∃ r, ↑r • x = x

Tactic:
by

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
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
h : I ≤ ⊥.jacobson
x : M
hx : x ∈ ⨅ i, I ^ i • ⊤
r : ↥I
hr : ↑r • x = x
⊢ 1 - ↑r - 1 ∈ ⊥.jacobson

Tactic:
by

Goal state after:
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:
by

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
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
h : I ≤ ⊥.jacobson
⊢ ⨅ i, I ^ i • ⊤ = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
h : I ≠ ⊤
⊢ ⨅ i, I ^ i = ⊥

Tactic:
by

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
surj : Function.Surjective ⇑(algebraMap A B)
I : Ideal B
J : Ideal A
eq : comap (algebraMap A B) I = RingHom.ker (algebraMap A B) ⊔ J
⊢ Function.Surjective ⇑(J.mapCotangent I (Algebra.ofId A B) ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Filtration

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

Tactic:
by

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
inst✝³ : IsDomain R
inst✝² : IsNoetherianRing R
inst✝¹ : Module.IsTorsionFree R M
inst✝ : Module.Finite R M
h : I ≠ ⊤
⊢ ⨅ i, I ^ i • ⊤ = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
inst✝¹ : IsNoetherianRing R
inst✝ : IsDomain R
h : I ≠ ⊤
⊢ ⨅ i, I ^ i = ⊥

Tactic:
by

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
surj : Function.Surjective ⇑(algebraMap A B)
I : Ideal B
J : Ideal A
eq : comap (algebraMap A B) I = RingHom.ker (algebraMap A B) ⊔ J
eqmap : I = map (algebraMap A B) J
x : J.Cotangent
x' : ↥J
hx' : J.toCotangent x' = x
this : Function.Surjective ⇑(Algebra.ofId A B)
hx : ↑x' ∈ J ^ 2 ⊔ RingHom.ker (algebraMap A B)
y : A
hy : y ∈ J ^ 2
z : A
hz : z ∈ RingHom.ker (algebraMap A B)
hyz : y + z = ↑x'
⊢ y + z ∈ J

Tactic:
by

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
surj : Function.Surjective ⇑(algebraMap A B)
I : Ideal B
J : Ideal A
eq : comap (algebraMap A B) I = RingHom.ker (algebraMap A B) ⊔ J
eqmap : I = map (algebraMap A B) J
x : J.Cotangent
x' : ↥J
hx' : J.toCotangent x' = x
this✝ : Function.Surjective ⇑(Algebra.ofId A B)
hx : ↑x' ∈ J ^ 2 ⊔ RingHom.ker (algebraMap A B)
y : A
hy : y ∈ J ^ 2
z : A
hz : z ∈ RingHom.ker (algebraMap A B)
hyz : y + z = ↑x'
this : y + z ∈ J
⊢ 2 ≠ 0

Tactic:
by

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
surj : Function.Surjective ⇑(algebraMap A B)
I : Ideal B
J : Ideal A
eq : comap (algebraMap A B) I = RingHom.ker (algebraMap A B) ⊔ J
eqmap : I = map (algebraMap A B) J
x : J.Cotangent
x' : ↥J
hx' : J.toCotangent x' = x
this✝ : Function.Surjective ⇑(Algebra.ofId A B)
hx : ↑x' ∈ J ^ 2 ⊔ RingHom.ker (algebraMap A B)
y : A
hy : y ∈ J ^ 2
z : A
hz : z ∈ RingHom.ker (algebraMap A B)
hyz : y + z = ↑x'
this : y + z ∈ J
zmemJ : z ∈ J
⊢ x = J.toCotangent ⟨z, zmemJ⟩

Tactic:
by

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
surj : Function.Surjective ⇑(algebraMap A B)
I : Ideal B
J : Ideal A
eq : comap (algebraMap A B) I = RingHom.ker (algebraMap A B) ⊔ J
⊢ (J.mapCotangent I (Algebra.ofId A B) ⋯).ker =
    Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (RingHom.ker (algebraMap A B) ⊓ J))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Projective

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
P : ModuleCat R
inst✝ : Module.Projective R ↑P
⊢ CategoryTheory.Projective P

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Projective

Goal state before:
pp: R : Type u
inst✝² : Ring R
P : ModuleCat R
inst✝¹ : Small.{v, u} R
inst✝ : CategoryTheory.Projective P
⊢ Module.Projective R ↑P

Tactic:
by

Goal state after: