mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Polynomial.Module.AEval

Goal state before:
pp: R : Type ?u.5
A : Type ?u.7
M : Type ?u.13
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
N : Type ?u.26
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module R[X] N
inst✝ : IsScalarTower R R[X] N
f : M →ₗ[R] N
hf : ∀ (m : M), f (a • m) = X • f m
p : R[X]
n : ℕ
k : R
h : ∀ (x : AEval R M a), f ((of R M a).symm ((C k * X ^ n) • x)) = (C k * X ^ n) • f ((of R M a).symm x)
m : AEval R M a
⊢ f ((of R M a).symm ((C k * X ^ (n + 1)) • m)) = (C k * X ^ (n + 1)) • f ((of R M a).symm m)

Tactic:
simp_rw [pow_succ, ← mul_assoc, mul_smul _ X, ← hf, ← of_symm_X_smul, ← h]

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

Goal state before:
pp: R : Type ?u.5
A : Type ?u.7
M : Type ?u.13
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
N : Type ?u.26
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module R[X] N
inst✝ : IsScalarTower R R[X] N
f : M ≃ₗ[R] N
hf : ∀ (m : M), f (a • m) = X • f m
x : AEval R M a
⊢ (⇑(of R M a) ∘ ⇑f.symm) ((LinearMap.ofAEval a (↑f) hf).toFun x) = x

Tactic:
simp [LinearMap.ofAEval]

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

Goal state before:
pp: R : Type ?u.5
A : Type ?u.7
M : Type ?u.13
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
N : Type ?u.26
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module R[X] N
inst✝ : IsScalarTower R R[X] N
f : M ≃ₗ[R] N
hf : ∀ (m : M), f (a • m) = X • f m
x : N
⊢ (LinearMap.ofAEval a (↑f) hf).toFun ((⇑(of R M a) ∘ ⇑f.symm) x) = x

Tactic:
simp [LinearMap.ofAEval]

Goal state after:
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]
⊢ p ∈ annihilator R[X] (AEval R M a) ↔ p ∈ RingHom.ker (aeval a)

Tactic:
[

Goal state after:
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]
⊢ p ∈ annihilator R[X] (AEval R M a) ↔ p ∈ RingHom.ker (aeval a)
Module: Mathlib.RingTheory.Finiteness.Nakayama

Goal state before:
pp: 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
H : ∃ 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

Tactic:
clear hin hs

Goal state after:
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
hfs : s.Finite
H : ∃ 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
Module: Mathlib.Algebra.Polynomial.Module.Basic

Goal state before:
pp: case refine_2
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type u_5
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
x y : PolynomialModule R M
r✝ r₁ r₂ : R
m✝ m' m₁ m₂ m₁' m₂' : M
R' : Type u_6
M' : Type u_7
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Module R M'
inst✝¹ : Algebra R R'
inst✝ : IsScalarTower R R' M'
r s : R
m : PolynomialModule R M
⊢ (((coeffEquiv R).toFun m).sum fun i c ↦ r ^ i • s • c) = (RingHom.id R) s • m.coeff.sum fun i m ↦ r ^ i • m

Tactic:
[

Goal state after:
case refine_2
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type u_5
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
x y : PolynomialModule R M
r✝ r₁ r₂ : R
m✝ m' m₁ m₂ m₁' m₂' : M
R' : Type u_6
M' : Type u_7
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Module R M'
inst✝¹ : Algebra R R'
inst✝ : IsScalarTower R R' M'
r s : R
m : PolynomialModule R M
⊢ (((coeffEquiv R).toFun m).sum fun i c ↦ r ^ i • s • c) = (RingHom.id R) s • m.coeff.sum fun i m ↦ r ^ i • m
Module: Mathlib.Algebra.Polynomial.Module.Basic

Goal state before:
pp: case zero
R : Type u_2
M : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
R' : Type u_6
M' : Type u_7
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Module R M'
inst✝¹ : Algebra R R'
inst✝ : IsScalarTower R R' M'
f : M →ₗ[R] M'
r : R
⊢ (eval ((algebraMap R R') r)) ((map R' f) 0) = f ((eval r) 0)

Tactic:
[

Goal state after:
case zero
R : Type u_2
M : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
R' : Type u_6
M' : Type u_7
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Module R M'
inst✝¹ : Algebra R R'
inst✝ : IsScalarTower R R' M'
f : M →ₗ[R] M'
r : R
⊢ (eval ((algebraMap R R') r)) ((map R' f) 0) = f ((eval r) 0)
Module: Mathlib.Algebra.Polynomial.Module.Basic

Goal state before:
pp: case add
R : Type u_2
M : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
R' : Type u_6
M' : Type u_7
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Module R M'
inst✝¹ : Algebra R R'
inst✝ : IsScalarTower R R' M'
f✝ : M →ₗ[R] M'
r : R
f g : PolynomialModule R M
e₁ : (eval ((algebraMap R R') r)) ((map R' f✝) f) = f✝ ((eval r) f)
e₂ : (eval ((algebraMap R R') r)) ((map R' f✝) g) = f✝ ((eval r) g)
⊢ (eval ((algebraMap R R') r)) ((map R' f✝) (f + g)) = f✝ ((eval r) (f + g))

Tactic:
[

Goal state after:
case add
R : Type u_2
M : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
R' : Type u_6
M' : Type u_7
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Module R M'
inst✝¹ : Algebra R R'
inst✝ : IsScalarTower R R' M'
f✝ : M →ₗ[R] M'
r : R
f g : PolynomialModule R M
e₁ : (eval ((algebraMap R R') r)) ((map R' f✝) f) = f✝ ((eval r) f)
e₂ : (eval ((algebraMap R R') r)) ((map R' f✝) g) = f✝ ((eval r) g)
⊢ (eval ((algebraMap R R') r)) ((map R' f✝) (f + g)) = f✝ ((eval r) (f + g))
Module: Mathlib.Algebra.Polynomial.Module.Basic

Goal state before:
pp: case add
R : Type u_2
inst✝² : CommRing R
S : Type u_8
inst✝¹ : CommRing S
inst✝ : Algebra S R
x : R
f g : PolynomialModule S S
e₁ : (aeval x) (equivPolynomial f) = (eval x) ((map R (Algebra.linearMap S R)) f)
e₂ : (aeval x) (equivPolynomial g) = (eval x) ((map R (Algebra.linearMap S R)) g)
⊢ (aeval x) (equivPolynomial (f + g)) = (eval x) ((map R (Algebra.linearMap S R)) (f + g))

Tactic:
[

Goal state after:
case add
R : Type u_2
inst✝² : CommRing R
S : Type u_8
inst✝¹ : CommRing S
inst✝ : Algebra S R
x : R
f g : PolynomialModule S S
e₁ : (aeval x) (equivPolynomial f) = (eval x) ((map R (Algebra.linearMap S R)) f)
e₂ : (aeval x) (equivPolynomial g) = (eval x) ((map R (Algebra.linearMap S R)) g)
⊢ (aeval x) (equivPolynomial (f + g)) = (eval x) ((map R (Algebra.linearMap S R)) (f + g))
Module: Mathlib.Algebra.Polynomial.Module.Basic

Goal state before:
pp: case zero
R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : R[X]
r : R
⊢ (eval r ∘ₗ comp p) 0 = (eval (Polynomial.eval r p)) 0

Tactic:
[

Goal state after:
case zero
R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : R[X]
r : R
⊢ (eval r ∘ₗ comp p) 0 = (eval (Polynomial.eval r p)) 0
Module: Mathlib.Algebra.Polynomial.Module.Basic

Goal state before:
pp: case add
R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : R[X]
r : R
x✝ y✝ : PolynomialModule R M
e₁ : (eval r ∘ₗ comp p) x✝ = (eval (Polynomial.eval r p)) x✝
e₂ : (eval r ∘ₗ comp p) y✝ = (eval (Polynomial.eval r p)) y✝
⊢ (eval r ∘ₗ comp p) (x✝ + y✝) = (eval (Polynomial.eval r p)) (x✝ + y✝)

Tactic:
[

Goal state after:
case add
R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : R[X]
r : R
x✝ y✝ : PolynomialModule R M
e₁ : (eval r ∘ₗ comp p) x✝ = (eval (Polynomial.eval r p)) x✝
e₂ : (eval r ∘ₗ comp p) y✝ = (eval (Polynomial.eval r p)) y✝
⊢ (eval r ∘ₗ comp p) (x✝ + y✝) = (eval (Polynomial.eval r p)) (x✝ + y✝)
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : DecidableEq ι
S : Finset ι
q : ι → R
hq : (↑S).Pairwise (IsCoprime on q)
hM : IsTorsionBySet R M ↑(S.inf fun i ↦ Ideal.span {q i})
⊢ DirectSum.IsInternal fun i ↦ torsionBy R M (q ↑i)

Tactic:
Finset.inf_eq_iInf

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : DecidableEq ι
S : Finset ι
q : ι → R
hq : (↑S).Pairwise (IsCoprime on q)
hM : IsTorsionBySet R M ↑(⨅ a ∈ S, Ideal.span {q a})
⊢ DirectSum.IsInternal fun i ↦ torsionBy R M (q ↑i)
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 : M
hn : n ∈ N
r : R
hr : r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0
s : R
hs : s * r - 1 ∈ J
this : n = -(s * r - 1) • n
⊢ n ∈ J • N

Tactic:
this

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
hn : n ∈ N
r : R
hr : r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0
s : R
hs : s * r - 1 ∈ J
this : n = -(s * r - 1) • n
⊢ -(s * r - 1) • 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✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : M
⊢ x ∈ ↑(torsion R M) ↔ x ∈ {x | (R ∙ x).annihilator ≠ ⊥}

Tactic:
[

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : M
⊢ x ∈ ↑(torsion R M) ↔ x ∈ {x | (R ∙ x).annihilator ≠ ⊥}
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 N' : Submodule R M
hN' : N'.FG
hIJ : I ≤ J.jacobson
hNN : N' ≤ N ⊔ I • N'
hNN' : N ⊔ N' = N ⊔ I • N'
h_comap : Function.Injective (comap N.mkQ)
this : map N.mkQ (I • N') = map N.mkQ N'
⊢ map N.mkQ N' ≤ map N.mkQ (I • N')

Tactic:
this

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 N' : Submodule R M
hN' : N'.FG
hIJ : I ≤ J.jacobson
hNN : N' ≤ N ⊔ I • N'
hNN' : N ⊔ N' = N ⊔ I • N'
h_comap : Function.Injective (comap N.mkQ)
this : map N.mkQ (I • N') = map N.mkQ N'
⊢ map N.mkQ N' ≤ map N.mkQ N'
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : IsAddTorsionFree M
x y : M
h : y ≠ 0
r s : ℕ
hrs : x + r • y = x + s • y
⊢ r = s

Tactic:
rw [add_right_inj, ← natCast_zsmul, ← natCast_zsmul] at hrs

Goal state after:
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : IsAddTorsionFree M
x y : M
h : y ≠ 0
r s : ℕ
hrs : ↑r • y = ↑s • y
⊢ r = s
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 ↔ ∃ n₀, ∀ n ≥ n₀, I • F.N n = F.N (n + 1)

Tactic:
[

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
hF' : ∀ (i : ℕ), (F.N i).FG
⊢ F.submodule.FG ↔ ∃ n₀, ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
Module: Mathlib.RingTheory.Ideal.Cotangent

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

Tactic:
rw [to_quotient_square_comp_toCotangent, LinearMap.range_comp, I.range_subtype]

Goal state after:
R : Type u
inst✝ : CommRing R
I : Ideal R
⊢ Submodule.map (Submodule.mkQ (I ^ 2)) I = Submodule.restrictScalars R I.cotangentIdeal
Module: Mathlib.RingTheory.Filtration

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

Tactic:
[

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
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))
⊢ (Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n), single R i '' ↑(F.N i))).FG
Module: Mathlib.RingTheory.Filtration

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

Tactic:
Submodule.span_iUnion₂,

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
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, ⨆ (_ : i ≤ n), Submodule.span (↥(reesAlgebra I)) (single R i '' ↑(F.N i))).FG
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
k : ℕ
hk :
  ∀ n ≥ k,
    I • (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N n = (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N (n + 1)
this : I • N = (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N (k + 1)
⊢ N ≤ I • N

Tactic:
hN

Goal state after:
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
k : ℕ
hk :
  ∀ n ≥ k,
    I • (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N n = (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N (n + 1)
this : I • N = N
⊢ N ≤ I • N
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: case hsur
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
s : Set ↥(maximalIdeal R)
⊢ Function.Surjective ⇑(algebraMap R (ResidueField R))

Tactic:
exact Ideal.Quotient.mk_surjective

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
⊢ (∃ x, ⊤ = ResidueField R ∙ (maximalIdeal R).toCotangent x) ↔ ∃ a, maximalIdeal R = R ∙ a

Tactic:
[

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.CategoryTheory.GradedObject

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
β : Type u_1
X Y : GradedObject β C
f g : X ⟶ Y
h : ∀ (x : β), f x = g x
⊢ f = g

Tactic:
by
  funext
  apply h

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject

Goal state before:
pp: I : Type u_1
J : Type u_2
C : Type u_4
inst✝¹ : Category.{v_1, u_4} C
X : GradedObject I C
p : I → J
j : J
inst✝ : X.HasMap p
c : X.CofanMapObjFun p j
hc : IsColimit c
i : I
hi : p i = j
⊢ Cofan.inj c ⟨i, hi⟩ ≫ (iso hc).hom = X.ιMapObj p i j hi

Tactic:
by
  apply IsColimit.comp_coconePointUniqueUpToIso_hom

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

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x✝ : S ⊗[R] S
x y : S
⊢ x ⊗ₜ[R] y - (x * y) ⊗ₜ[R] 1 = x • (1 ⊗ₜ[R] y - y ⊗ₜ[R] 1)

Tactic:
[

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x✝ : S ⊗[R] S
x y : S
⊢ x ⊗ₜ[R] y - (x * y) ⊗ₜ[R] 1 = x • (1 ⊗ₜ[R] y - y ⊗ₜ[R] 1)
Module: Mathlib.Algebra.Homology.HomologicalComplex

Goal state before:
pp: case neg
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
A B : HomologicalComplex V c
f : A.Hom B
i j : ι
hij : ¬c.Rel i j
⊢ f.f i ≫ B.d i j = 0 ≫ f.f j

Tactic:
B.shape i j hij,

Goal state after:
case neg
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
A B : HomologicalComplex V c
f : A.Hom B
i j : ι
hij : ¬c.Rel i j
⊢ f.f i ≫ 0 = 0 ≫ f.f j
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: case a.refine_2
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x✝ : S ⊗[R] S
x y : S
this : x ⊗ₜ[R] y - (x * y) ⊗ₜ[R] 1 = x • (1 ⊗ₜ[R] y - y ⊗ₜ[R] 1)
⊢ x ⊗ₜ[R] y - (x * y) ⊗ₜ[R] 1 ∈ Submodule.span S (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)

Tactic:
this

Goal state after:
case a.refine_2
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x✝ : S ⊗[R] S
x y : S
this : x ⊗ₜ[R] y - (x * y) ⊗ₜ[R] 1 = x • (1 ⊗ₜ[R] y - y ⊗ₜ[R] 1)
⊢ x • (1 ⊗ₜ[R] y - y ⊗ₜ[R] 1) ∈ Submodule.span S (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)
Module: Mathlib.Algebra.Homology.HomologicalComplex

Goal state before:
pp: case hnc
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
j : ι
h : ¬c.Rel (c.prev j) j
i : ι
hi : c.Rel i j
this : c.prev j = i
⊢ False

Tactic:
this

Goal state after:
case hnc
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
j i : ι
h : ¬c.Rel i j
hi : c.Rel i j
this : c.prev j = i
⊢ False
Module: Mathlib.Algebra.Homology.HomologicalComplex

Goal state before:
pp: case hnc
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i : ι
h : ¬c.Rel i (c.next i)
j : ι
hj : c.Rel i j
this : c.next i = j
⊢ False

Tactic:
this

Goal state after:
case hnc
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i j : ι
h : ¬c.Rel i j
hj : c.Rel i j
this : c.next i = j
⊢ False
Module: Mathlib.Algebra.Homology.HomologicalComplex

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C C₁ C₂ C₃ : HomologicalComplex V c
f : (i : ι) → C₁.X i ≅ C₂.X i
hf : ∀ (i j : ι), c.Rel i j → (f i).hom ≫ C₂.d i j = C₁.d i j ≫ (f j).hom
⊢ { f := fun i ↦ (f i).inv, comm' := ⋯ } ≫ { f := fun i ↦ (f i).hom, comm' := hf } = 𝟙 C₂

Tactic:
ext i
    exact (f i).inv_hom_id

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

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y z : S
⊢ single x z + single y z - single (x + y) z ∈ kerTotal R S

Tactic:
[

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y z : S
⊢ single x z + single y z - single (x + y) z ∈ kerTotal R S
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
x y z : S
⊢ single y (z * x) + single x (z * y) - single (x * y) z ∈ kerTotal R S

Tactic:
[

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y z : S
⊢ single y (z * x) + single x (z * y) - single (x * y) z ∈ kerTotal R S
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
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
[

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
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: case a
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (linearCombination S ⇑(D R S)).ker ≤ (kerTotal R S).mkQ.ker

Tactic:
rw [← KaehlerDifferential.derivationQuotKerTotal_lift_comp_linearCombination]

Goal state after:
case a
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (linearCombination S ⇑(D R S)).ker ≤
    ((derivationQuotKerTotal R S).liftKaehlerDifferential ∘ₗ linearCombination S ⇑(D R S)).ker
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
x : S →₀ S
this : (derivationQuotKerTotal R S).liftKaehlerDifferential ((linearCombination S ⇑(D R S)) x) = (kerTotal R S).mkQ x
⊢ ((kerTotal R S).liftQ (linearCombination S ⇑(D R S)) ⋯).toFun
      ((derivationQuotKerTotal R S).liftKaehlerDifferential ((linearCombination S ⇑(D R S)) x)) =
    (linearCombination S ⇑(D R S)) x

Tactic:
this

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
x : S →₀ S
this : (derivationQuotKerTotal R S).liftKaehlerDifferential ((linearCombination S ⇑(D R S)) x) = (kerTotal R S).mkQ x
⊢ ((kerTotal R S).liftQ (linearCombination S ⇑(D R S)) ⋯).toFun ((kerTotal R S).mkQ x) =
    (linearCombination S ⇑(D R S)) x