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
p : Submodule R M
hp : p ∈ ((Algebra.lsmul R R M) a).invtSubmodule
x : AEval R M a
hx : x ∈ (mapSubmodule R M a) ⟨p, hp⟩
⊢ (of R M a).symm ↑⟨x, hx⟩ ∈ p

Tactic:
;

Goal state after:
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
p : Submodule R M
hp : p ∈ ((Algebra.lsmul R R M) a).invtSubmodule
x : AEval R M a
hx : x ∈ (mapSubmodule R M a) ⟨p, hp⟩
⊢ (of R M a).symm ↑⟨x, hx⟩ ∈ p
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
p : Submodule R M
hp : p ∈ ((Algebra.lsmul R R M) a).invtSubmodule
x : ↥p
⊢ (equiv_mapSubmodule a p hp) (LinearMap.restrict ((Algebra.lsmul R R M) a) hp • x) = X • (equiv_mapSubmodule a p hp) x

Tactic:
by simp [equiv_mapSubmodule, X_smul_of]

Goal state after:
Module: Mathlib.RingTheory.ReesAlgebra

Goal state before:
pp: case succ.refine_1
R : Type u
inst✝ : CommRing R
I : Ideal R
n : ℕ
hn : ∀ {r : R}, r ∈ I ^ n → (monomial n) r ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
r : R
hr : r ∈ I * I ^ n
⊢ ∀ r ∈ I, ∀ n_1 ∈ I ^ n, (monomial (n + 1)) (r • n_1) ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)

Tactic:
intro r

Goal state after:
case succ.refine_1
R : Type u
inst✝ : CommRing R
I : Ideal R
n : ℕ
hn : ∀ {r : R}, r ∈ I ^ n → (monomial n) r ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
r✝ : R
hr : r✝ ∈ I * I ^ n
r : R
⊢ r ∈ I → ∀ n_1 ∈ I ^ n, (monomial (n + 1)) (r • n_1) ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
Module: Mathlib.RingTheory.ReesAlgebra

Goal state before:
pp: case a
R : Type u
inst✝ : CommRing R
I : Ideal R
⊢ reesAlgebra I ≤ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)

Tactic:
· intro p hp
    rw [p.as_sum_support]
    apply Subalgebra.sum_mem _ _
    rintro i -
    exact monomial_mem_adjoin_monomial (hp i)

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

Goal state before:
pp: case single.monomial
R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
i : ℕ
m : M
n✝ : ℕ
a✝ : R
⊢ r ^ (n✝ + i) • a✝ • m = (a✝ * r ^ n✝) • r ^ i • m

Tactic:
;

Goal state after:
case single.monomial
R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
i : ℕ
m : M
n✝ : ℕ
a✝ : R
⊢ r ^ (n✝ + i) • a✝ • m = (a✝ * r ^ n✝) • r ^ i • m
Module: Mathlib.Algebra.Polynomial.Module.Basic

Goal state before:
pp: case single
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
i : ℕ
m : M
⊢ (algebraMap R R') r ^ i • f m = r ^ i • f m

Tactic:
;

Goal state after:
case single
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
i : ℕ
m : M
⊢ (algebraMap R R') r ^ i • f m = r ^ i • f 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
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : (↑S).Pairwise fun i j ↦ p i ⊔ p j = ⊤
T : Finset ι
hT : T ⊆ S
i : ι
hi : i ∈ S
hiT : i ∉ T
this : torsionBySet R M ↑(p i ⊔ ⨅ i ∈ T, p i) = torsionBySet R M ↑(p i) ⊓ torsionBySet R M ↑(⨅ i ∈ T, p i)
j : ι
hj : j ∈ T
⊢ p i ⊔ p j = ⊤

Tactic:
;

Goal state after:
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 = ⊤
T : Finset ι
hT : T ⊆ S
i : ι
hi : i ∈ S
hiT : i ∉ T
this : torsionBySet R M ↑(p i ⊔ ⨅ i ∈ T, p i) = torsionBySet R M ↑(p i) ⊓ torsionBySet R M ↑(⨅ i ∈ T, p i)
j : ι
hj : j ∈ T
⊢ p i ⊔ p j = ⊤
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
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : (↑S).Pairwise fun i j ↦ p i ⊔ p j = ⊤
T : Finset ι
hT : T ⊆ S
i : ι
hi : i ∈ S
hiT : i ∉ T
this : torsionBySet R M ↑(p i ⊔ ⨅ i ∈ T, p i) = torsionBySet R M ↑(p i) ⊓ torsionBySet R M ↑(⨅ i ∈ T, p i)
j : ι
hj : j ∈ T
⊢ i ≠ j

Tactic:
;

Goal state after:
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 = ⊤
T : Finset ι
hT : T ⊆ S
i : ι
hi : i ∈ S
hiT : i ∉ T
this : torsionBySet R M ↑(p i ⊔ ⨅ i ∈ T, p i) = torsionBySet R M ↑(p i) ⊓ torsionBySet R M ↑(⨅ i ∈ T, p i)
j : ι
hj : j ∈ T
⊢ i ≠ j
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
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : (↑S).Pairwise fun i j ↦ p i ⊔ p j = ⊤
T : Finset ι
hT : T ⊆ S
i : ι
hi : i ∈ S
hiT : i ∉ T
this : torsionBySet R M ↑(p i ⊔ ⨅ i ∈ T, p i) = torsionBySet R M ↑(p i) ⊓ torsionBySet R M ↑(⨅ i ∈ T, p i)
hj : i ∈ T
⊢ False

Tactic:
;

Goal state after:
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 = ⊤
T : Finset ι
hT : T ⊆ S
i : ι
hi : i ∈ S
hiT : i ∉ T
this : torsionBySet R M ↑(p i ⊔ ⨅ i ∈ T, p i) = torsionBySet R M ↑(p i) ⊓ torsionBySet R M ↑(⨅ i ∈ T, p i)
hj : i ∈ T
⊢ False
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: case mk
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a : R
p : Submodule R ↥(torsionBy R M a)
c✝ : R ⧸ R ∙ a
b : R
⊢ ∀ {x : ↥(torsionBy R M a)}, x ∈ ↑p → Quot.mk (⇑(R ∙ a).quotientRel) b • x ∈ ↑p

Tactic:
;

Goal state after:
case mk
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a : R
p : Submodule R ↥(torsionBy R M a)
c✝ : R ⧸ R ∙ a
b : R
⊢ ∀ {x : ↥(torsionBy R M a)}, x ∈ ↑p → Quot.mk (⇑(R ∙ a).quotientRel) b • x ∈ ↑p
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
a : R
p : Submodule R ↥(torsionBy R M a)
⊢ ∀ (c : R ⧸ R ∙ a) {x : ↥(torsionBy R M a)}, x ∈ ↑p → c • x ∈ ↑p

Tactic:
rintro ⟨b⟩; exact p.smul_mem b

Goal state after:
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
a : R
x✝ : Submodule (R ⧸ R ∙ a) ↥(torsionBy R M a)
⊢ (fun p ↦ { carrier := ↑p, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ })
      ((restrictScalarsEmbedding R (R ⧸ R ∙ a) ↥(torsionBy R M a)).toFun x✝) =
    x✝

Tactic:
;

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a : R
x✝ : Submodule (R ⧸ R ∙ a) ↥(torsionBy R M a)
⊢ (fun p ↦ { carrier := ↑p, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ })
      ((restrictScalarsEmbedding R (R ⧸ R ∙ a) ↥(torsionBy R M a)).toFun x✝) =
    x✝
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
a : R
x✝¹ : Submodule (R ⧸ R ∙ a) ↥(torsionBy R M a)
x✝ : ↥(torsionBy R M a)
⊢ x✝ ∈
      (fun p ↦ { carrier := ↑p, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ })
        ((restrictScalarsEmbedding R (R ⧸ R ∙ a) ↥(torsionBy R M a)).toFun x✝¹) ↔
    x✝ ∈ x✝¹

Tactic:
;

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a : R
x✝¹ : Submodule (R ⧸ R ∙ a) ↥(torsionBy R M a)
x✝ : ↥(torsionBy R M a)
⊢ x✝ ∈
      (fun p ↦ { carrier := ↑p, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ })
        ((restrictScalarsEmbedding R (R ⧸ R ∙ a) ↥(torsionBy R M a)).toFun x✝¹) ↔
    x✝ ∈ x✝¹
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
a : R
x✝ : Submodule R ↥(torsionBy R M a)
⊢ (restrictScalarsEmbedding R (R ⧸ R ∙ a) ↥(torsionBy R M a)).toFun
      ((fun p ↦ { carrier := ↑p, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }) x✝) =
    x✝

Tactic:
;

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a : R
x✝ : Submodule R ↥(torsionBy R M a)
⊢ (restrictScalarsEmbedding R (R ⧸ R ∙ a) ↥(torsionBy R M a)).toFun
      ((fun p ↦ { carrier := ↑p, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }) x✝) =
    x✝
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
a : R
x✝¹ : Submodule R ↥(torsionBy R M a)
x✝ : ↥(torsionBy R M a)
⊢ x✝ ∈
      (restrictScalarsEmbedding R (R ⧸ R ∙ a) ↥(torsionBy R M a)).toFun
        ((fun p ↦ { carrier := ↑p, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }) x✝¹) ↔
    x✝ ∈ x✝¹

Tactic:
;

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a : R
x✝¹ : Submodule R ↥(torsionBy R M a)
x✝ : ↥(torsionBy R M a)
⊢ x✝ ∈
      (restrictScalarsEmbedding R (R ⧸ R ∙ a) ↥(torsionBy R M a)).toFun
        ((fun p ↦ { carrier := ↑p, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }) x✝¹) ↔
    x✝ ∈ x✝¹
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.Algebra.Module.Torsion.Basic

Goal state before:
pp: case h
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : (x : M) → Decidable (x = 0)
p : R
hM : IsTorsion' M ↥(Submonoid.powers p)
d : ℕ
hd : d ≠ 0
s : Fin d → M
hs : span R (Set.range s) = ⊤
oj : Option (Fin d) := List.argmax (fun i ↦ pOrder hM (s i)) (List.finRange d)
hoj : oj.isSome = true
i : Fin d
⊢ s i ∈ ↑(torsionBy R M (p ^ pOrder hM (s (oj.get hoj))))

Tactic:
;

Goal state after:
case h
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : (x : M) → Decidable (x = 0)
p : R
hM : IsTorsion' M ↥(Submonoid.powers p)
d : ℕ
hd : d ≠ 0
s : Fin d → M
hs : span R (Set.range s) = ⊤
oj : Option (Fin d) := List.argmax (fun i ↦ pOrder hM (s i)) (List.finRange d)
hoj : oj.isSome = true
i : Fin d
⊢ s i ∈ ↑(torsionBy R M (p ^ pOrder hM (s (oj.get hoj))))
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: R : Type w
inst✝ : CommRing R
a b : R
ha : a ∈ R⁰
x : R ⧸ R ∙ a * b
⊢ x ∈ torsionBy R (R ⧸ R ∙ a * b) a ↔ x ∈ R ∙ (mk (R ∙ a * b)) b

Tactic:
;

Goal state after:
R : Type w
inst✝ : CommRing R
a b : R
ha : a ∈ R⁰
x : R ⧸ R ∙ a * b
⊢ x ∈ torsionBy R (R ⧸ R ∙ a * b) a ↔ x ∈ R ∙ (mk (R ∙ a * b)) b
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: R : Type w
inst✝ : CommRing R
a b : R
ha : a ∈ R⁰
x : R
⊢ a • (mk (R ∙ a * b)) x = 0 ↔ ∃ a_1, a_1 • (mk (R ∙ a * b)) b = (mk (R ∙ a * b)) x

Tactic:
;

Goal state after:
R : Type w
inst✝ : CommRing R
a b : R
ha : a ∈ R⁰
x : R
⊢ a • (mk (R ∙ a * b)) x = 0 ↔ ∃ a_1, a_1 • (mk (R ∙ a * b)) b = (mk (R ∙ a * b)) x
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 ^ 1 • I ^ i • N ≤ I ^ i • N

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 F' : I✝.Filtration M
I : Ideal R
N : Submodule R M
i : ℕ
⊢ I ^ 1 • I ^ i • N ≤ I ^ i • N
Module: Mathlib.RingTheory.Filtration

Goal state before:
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:
;

Goal state after:
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: case h.zero
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)
⊢ 0 ≤ 0 + n₀

Tactic:
;

Goal state after:
case h.zero
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)
⊢ 0 ≤ 0 + n₀
Module: Mathlib.RingTheory.Nakayama

Goal state before:
pp: case a
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N N' : Submodule R M
hN : N.FG
hIjac : I ≤ ⊥.jacobson
hmaple : N = I • N ⊔ N'
⊢ N' ≤ I • N ⊔ N'

Tactic:
;

Goal state after:
case a
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N N' : Submodule R M
hN : N.FG
hIjac : I ≤ ⊥.jacobson
hmaple : N = I • N ⊔ N'
⊢ N' ≤ I • N ⊔ N'
Module: Mathlib.RingTheory.Nakayama

Goal state before:
pp: case h.refine_2.refine_2
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s : Set (M ⧸ I • N)
hN : N.FG
hIjac : I ≤ ⊥.jacobson
hsspan : span R s = map (I • N).mkQ N
⊢ N = span R (Quotient.out '' s)

Tactic:
;

Goal state after:
case h.refine_2.refine_2
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s : Set (M ⧸ I • N)
hN : N.FG
hIjac : I ≤ ⊥.jacobson
hsspan : span R s = map (I • N).mkQ N
⊢ N = span R (Quotient.out '' s)
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: case refine_1
R : Type u
inst✝ : CommRing R
I : Ideal R
x✝ : R ⧸ I ^ 2
hx✝ : x✝ ∈ I.cotangentIdeal • I.cotangentIdeal
x : R
hx : x ∈ ↑I
y : R
hy : y ∈ ↑I
⊢ (Quotient.mk (I ^ 2)).toSemilinearMap x • (Quotient.mk (I ^ 2)).toSemilinearMap y ∈ ⊥

Tactic:
;

Goal state after:
case refine_1
R : Type u
inst✝ : CommRing R
I : Ideal R
x✝ : R ⧸ I ^ 2
hx✝ : x✝ ∈ I.cotangentIdeal • I.cotangentIdeal
x : R
hx : x ∈ ↑I
y : R
hy : y ∈ ↑I
⊢ (Quotient.mk (I ^ 2)).toSemilinearMap x • (Quotient.mk (I ^ 2)).toSemilinearMap y ∈ ⊥
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I : Ideal R
x✝ : R ⧸ I ^ 2
hx✝ : x✝ ∈ I.cotangentIdeal • I.cotangentIdeal
x : R
hx : x ∈ ↑I
y : R
hy : y ∈ ↑I
⊢ (fun x1 x2 ↦ x1 * x2) x y ∈ I * I

Tactic:
;

Goal state after:
R : Type u
inst✝ : CommRing R
I : Ideal R
x✝ : R ⧸ I ^ 2
hx✝ : x✝ ∈ I.cotangentIdeal • I.cotangentIdeal
x : R
hx : x ∈ ↑I
y : R
hy : y ∈ ↑I
⊢ (fun x1 x2 ↦ x1 * x2) x y ∈ I * I
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: case refine_2
R : Type u
inst✝ : CommRing R
I : Ideal R
x✝ : R ⧸ I ^ 2
hx✝ : x✝ ∈ I.cotangentIdeal • I.cotangentIdeal
x y : R ⧸ I ^ 2
hx : x ∈ ⊥
hy : y ∈ ⊥
⊢ x + y ∈ ⊥

Tactic:
;

Goal state after:
case refine_2
R : Type u
inst✝ : CommRing R
I : Ideal R
x✝ : R ⧸ I ^ 2
hx✝ : x✝ ∈ I.cotangentIdeal • I.cotangentIdeal
x y : R ⧸ I ^ 2
hx : x ∈ ⊥
hy : y ∈ ⊥
⊢ x + y ∈ ⊥
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I : Ideal R
⊢ Submodule.map (Submodule.mkQ (I ^ 2)) I = Submodule.restrictScalars R I.cotangentIdeal

Tactic:
;

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.Ideal.Cotangent

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I : Ideal R
x✝ : R ⧸ I ^ 2
⊢ x✝ ∈ Submodule.map (Submodule.mkQ (I ^ 2)) I ↔ x✝ ∈ Submodule.restrictScalars R I.cotangentIdeal

Tactic:
;

Goal state after:
R : Type u
inst✝ : CommRing R
I : Ideal R
x✝ : R ⧸ I ^ 2
⊢ x✝ ∈ Submodule.map (Submodule.mkQ (I ^ 2)) I ↔ x✝ ∈ Submodule.restrictScalars R I.cotangentIdeal
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:
;

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
x : I.Cotangent
⊢ I.cotangentToQuotientSquare x ∈ I.cotangentToQuotientSquare.range
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
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 : A
ha : a ∈ RingHom.ker f.toRingHom ^ 2
⊢ f.toRingHom a = 0

Tactic:
;

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
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 : A
ha : a ∈ RingHom.ker f.toRingHom ^ 2
⊢ f.toRingHom a = 0
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: case refine_2
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
⊢ ∀ (r : R),
    (↑↑(Quotient.lift (RingHom.ker f.toRingHom ^ 2) f.toRingHom ⋯)).toFun
        ((algebraMap R (A ⧸ RingHom.ker f.toRingHom ^ 2)) r) =
      (algebraMap R B) r

Tactic:
intro r

Goal state after:
case refine_2
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
r : R
⊢ (↑↑(Quotient.lift (RingHom.ker f.toRingHom ^ 2) f.toRingHom ⋯)).toFun
      ((algebraMap R (A ⧸ RingHom.ker f.toRingHom ^ 2)) r) =
    (algebraMap R B) r
Module: Mathlib.RingTheory.Ideal.Cotangent

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

Tactic:
;

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

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

Tactic:
;

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

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

Tactic:
;

Goal state after:
case a
R : Type u
inst✝⁴ : CommRing R
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
x : A
hx : x ∈ ↑(RingHom.ker f.toRingHom)
⊢ (Quotient.mk (RingHom.ker f.toRingHom ^ 2)).toSemilinearMap x ∈ RingHom.ker f.kerSquareLift.toRingHom
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) ↑(Submodule.span R (⇑(lsingle R i) '' ↑s)) =
    Submodule.span (↥(reesAlgebra I)) (single R i '' ↑(F.N i))

Tactic:
← Submodule.map_span,

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
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) ↑(Submodule.map (lsingle R i) (Submodule.span R ↑s)) =
    Submodule.span (↥(reesAlgebra I)) (single R i '' ↑(F.N i))
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) ↑(Submodule.map (lsingle R i) (F.N i)) =
    Submodule.span (↥(reesAlgebra I)) (single R i '' ↑(F.N i))

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
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) ↑(Submodule.map (lsingle R i) (F.N i)) =
    Submodule.span (↥(reesAlgebra I)) (single R i '' ↑(F.N i))