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

Goal state before:
pp: ι : 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✝
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
this : IsScalarTower R R[X] (PolynomialModule R M)
⊢ IsScalarTower S R[X] (PolynomialModule R M)

Tactic:
constructor

Goal state after:
ι : 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✝
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
this : IsScalarTower R R[X] (PolynomialModule R M)
⊢ ∀ (x : S) (y : R[X]) (z : PolynomialModule R M), (x • y) • z = x • y • z
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 : ↥((Algebra.lsmul R R M) a).invtSubmodule
⊢ (fun q ↦ ⟨(Submodule.orderIsoMapComap (of R M a)).symm (Submodule.restrictScalars R q), ⋯⟩)
      ((fun p ↦
          let __AddSubmonoid := AddSubmonoid.map (of R M a) (↑p).toAddSubmonoid;
          { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ })
        p) =
    p

Tactic:
ext

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 : ↥((Algebra.lsmul R R M) a).invtSubmodule
x✝ : M
⊢ x✝ ∈
      ↑((fun q ↦ ⟨(Submodule.orderIsoMapComap (of R M a)).symm (Submodule.restrictScalars R q), ⋯⟩)
          ((fun p ↦
              let __AddSubmonoid := AddSubmonoid.map (of R M a) (↑p).toAddSubmonoid;
              { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ })
            p)) ↔
    x✝ ∈ ↑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
q : Submodule R[X] (AEval R M a)
⊢ (fun p ↦
        let __AddSubmonoid := AddSubmonoid.map (of R M a) (↑p).toAddSubmonoid;
        { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ })
      ((fun q ↦ ⟨(Submodule.orderIsoMapComap (of R M a)).symm (Submodule.restrictScalars R q), ⋯⟩) q) =
    q

Tactic:
ext

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
q : Submodule R[X] (AEval R M a)
x✝ : AEval R M a
⊢ x✝ ∈
      (fun p ↦
          let __AddSubmonoid := AddSubmonoid.map (of R M a) (↑p).toAddSubmonoid;
          { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ })
        ((fun q ↦ ⟨(Submodule.orderIsoMapComap (of R M a)).symm (Submodule.restrictScalars R q), ⋯⟩) q) ↔
    x✝ ∈ q
Module: Mathlib.RingTheory.Finiteness.Nakayama

Goal state before:
pp: case h
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
i : M
s : Set M
a✝ : i ∉ s
hs✝ : s.Finite
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap ((LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) → ∃ r, r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0
r : R
hr1 : r - 1 ∈ I
hs : i ∈ ↑N ∧ s ⊆ ↑N
z : M
hz : z ∈ I • span R s
c : R
hci : c ∈ I
hyz : c • i + z = r • i
⊢ r - c - 1 ∈ I ∧ (r - c) • i ∈ I • span R s

Tactic:
constructor

Goal state after:
case h.left
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
i : M
s : Set M
a✝ : i ∉ s
hs✝ : s.Finite
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap ((LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) → ∃ r, r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0
r : R
hr1 : r - 1 ∈ I
hs : i ∈ ↑N ∧ s ⊆ ↑N
z : M
hz : z ∈ I • span R s
c : R
hci : c ∈ I
hyz : c • i + z = r • i
⊢ r - c - 1 ∈ I

case h.right
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
i : M
s : Set M
a✝ : i ∉ s
hs✝ : s.Finite
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap ((LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) → ∃ r, r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0
r : R
hr1 : r - 1 ∈ I
hs : i ∈ ↑N ∧ s ⊆ ↑N
z : M
hz : z ∈ I • span R s
c : R
hci : c ∈ I
hyz : c • i + z = r • i
⊢ (r - c) • i ∈ I • span R s
Module: Mathlib.RingTheory.ReesAlgebra

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I : Ideal R
f : R[X]
a : ℕ
⊢ f.coeff a ∈ I ^ a ↔ a ∈ f.support → f.coeff a ∈ I ^ a

Tactic:
rw [mem_support_iff, Iff.comm, Classical.imp_iff_right_iff, Ne, ← imp_iff_not_or]

Goal state after:
R : Type u
inst✝ : CommRing R
I : Ideal R
f : R[X]
a : ℕ
⊢ f.coeff a = 0 → f.coeff a ∈ I ^ a
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:
simp_rw [map_add, e₁, e₂]

Goal state after:
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:
simp_rw [map_add, e₁, e₂]

Goal state after:
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:
simp_rw [map_add, e₁, e₂]

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
ι : Type u_3
S : Finset ι
q : ι → R
hq : (↑S).Pairwise (IsCoprime on q)
⊢ ⨆ i ∈ S, torsionBy R M (q i) = ⨆ i ∈ S, torsionBySet R M ↑(Ideal.span {q i})

Tactic:
congr
    ext : 1
    congr
    ext : 1
    exact (torsionBySet_span_singleton_eq _).symm

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

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

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✝² : Monoid R
inst✝¹ : AddCommMonoid M
inst✝ : DistribMulAction R M
p : R
⊢ IsTorsion' M ↥(Submonoid.powers p) ↔ ∀ (x : M), ∃ n, p ^ n • x = 0

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
M : Type u_2
inst✝² : Monoid R
inst✝¹ : AddCommMonoid M
inst✝ : DistribMulAction R M
p : R
⊢ IsTorsion' M ↥(Submonoid.powers p) → ∀ (x : M), ∃ n, p ^ n • x = 0

case mpr
R : Type u_1
M : Type u_2
inst✝² : Monoid R
inst✝¹ : AddCommMonoid M
inst✝ : DistribMulAction R M
p : R
⊢ (∀ (x : M), ∃ n, p ^ n • x = 0) → IsTorsion' M ↥(Submonoid.powers p)
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:
constructor

Goal state after:
case mp
R : Type w
inst✝ : CommRing R
a b : R
ha : a ∈ R⁰
x : R
⊢ a • (mk (R ∙ a * b)) x = 0 → ∃ a_2, a_2 • (mk (R ∙ a * b)) b = (mk (R ∙ a * b)) x

case mpr
R : Type w
inst✝ : CommRing R
a b : R
ha : a ∈ R⁰
x : R
⊢ (∃ a_1, a_1 • (mk (R ∙ a * b)) b = (mk (R ∙ a * b)) x) → a • (mk (R ∙ a * b)) x = 0
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:
add_right_inj,

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 F' : I.Filtration M
⊢ (F ⊓ F').submodule = F.submodule ⊓ F'.submodule

Tactic:
ext

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
x✝ : PolynomialModule R M
⊢ x✝ ∈ (F ⊓ F').submodule ↔ x✝ ∈ F.submodule ⊓ F'.submodule
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₀ : ℕ
⊢ (∀ (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:
constructor

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₀ : ℕ
⊢ (∀ (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)

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
n₀ : ℕ
⊢ (∀ n ≥ n₀, I • F.N n = F.N (n + 1)) →
    ∀ (i : ℕ),
      single R i '' ↑(F.N i) ⊆ ↑(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
⊢ Subsingleton I.Cotangent ↔ IsIdempotentElem I

Tactic:
constructor

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

case mpr
R : Type u
inst✝ : CommRing R
I : Ideal R
⊢ IsIdempotentElem I → Subsingleton I.Cotangent
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₀, F.submodule = Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i))

Tactic:
constructor

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
hF' : ∀ (i : ℕ), (F.N i).FG
⊢ F.submodule.FG → ∃ n₀, F.submodule = Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i))

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₀, F.submodule = Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i))) → F.submodule.FG
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:
ext

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
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₂
x : ↥I₁
hx : x ∈ I₁ • ⊤
a : A
ha : a ∈ I₁
b : A
hb : b ∈ I₁
⊢ (f.toLinearMap.restrict h) ⟨a * b, ⋯⟩ = f a • ⟨f b, ⋯⟩

Tactic:
ext

Goal state after:
R : Type u
S : Type v
S' : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : CommSemiring S'
inst✝⁶ : Algebra S' R
inst✝⁵ : Algebra S S'
inst✝⁴ : IsScalarTower S S' R
I : Ideal R
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I₁ : Ideal A
I₂ : Ideal B
f : A →ₐ[R] B
h : I₁ ≤ comap f I₂
x : ↥I₁
hx : x ∈ I₁ • ⊤
a : A
ha : a ∈ I₁
b : A
hb : b ∈ I₁
⊢ ↑((f.toLinearMap.restrict h) ⟨a * b, ⋯⟩) = ↑(f a • ⟨f b, ⋯⟩)
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))
i : ℕ
hi : i ∈ Finset.range n.succ
s : Finset M
hs : Submodule.span R ↑s = F.N i
this :
  Submodule.span ↥(reesAlgebra I) ↑(Finset.image (⇑(lsingle R i)) s) =
    Submodule.span (↥(reesAlgebra I)) (single R i '' ↑(F.N i))
⊢ (Submodule.span (↥(reesAlgebra I)) (single R ↑⟨i, hi⟩ '' ↑(F.N ↑⟨i, hi⟩))).FG

Tactic:
rw [Subtype.coe_mk, ← this]

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 : ℕ
hi : i ∈ Finset.range n.succ
s : Finset M
hs : Submodule.span R ↑s = F.N i
this :
  Submodule.span ↥(reesAlgebra I) ↑(Finset.image (⇑(lsingle R i)) s) =
    Submodule.span (↥(reesAlgebra I)) (single R i '' ↑(F.N i))
⊢ (Submodule.span ↥(reesAlgebra I) ↑(Finset.image (⇑(lsingle R i)) s)).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
⊢ x ∈ ⨅ i, I ^ i • ⊤ ↔ ∃ r, ↑r • x = x

Tactic:
constructor

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 := ⋯
hN : ∀ (k : ℕ), (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N k = N
⊢ x ∈ ⨅ i, I ^ i • ⊤ → ∃ r, ↑r • x = x

case mpr
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 := ⋯
hN : ∀ (k : ℕ), (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N k = N
⊢ (∃ r, ↑r • x = x) → x ∈ ⨅ i, I ^ i • ⊤
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)
H : Submodule.map (maximalIdeal R).toCotangent M = ⊤
⊢ maximalIdeal R ≤
    Submodule.map (Submodule.subtype (maximalIdeal R)) M ⊔
      Submodule.map (Submodule.subtype (maximalIdeal R)) (maximalIdeal R).toCotangent.ker

Tactic:
← Submodule.map_sup,

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
M : Submodule R ↥(maximalIdeal R)
H : Submodule.map (maximalIdeal R).toCotangent M = ⊤
⊢ maximalIdeal R ≤ Submodule.map (Submodule.subtype (maximalIdeal R)) (M ⊔ (maximalIdeal R).toCotangent.ker)
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:
constructor

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

case mpr
R : Type u_3
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
I : Ideal R
⊢ I = ⊥ ∨ I = ⊤ → IsIdempotentElem I
Module: Mathlib.Algebra.Homology.ComplexShape

Goal state before:
pp: ι : Type u_1
c : ComplexShape ι
i : ι
⊢ Subsingleton { j // c.Rel i j }

Tactic:
constructor

Goal state after:
ι : Type u_1
c : ComplexShape ι
i : ι
⊢ ∀ (a b : { j // c.Rel i j }), a = b
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
S' R : Dᵒᵖ ⥤ CommRingCat
M N : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
φ : S ⟶ F.op ⋙ R
φ' : S' ⟶ R
x✝ : Dᵒᵖ
⊢ CommRingCat.KaehlerDifferential.map ⋯ =
    (ModuleCat.restrictScalarsId'App (CommRingCat.Hom.hom (R.map (𝟙 x✝))) ⋯
        (CommRingCat.KaehlerDifferential (φ'.app x✝))).inv

Tactic:
ext

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S : Cᵒᵖ ⥤ CommRingCat
F : C ⥤ D
S' R : Dᵒᵖ ⥤ CommRingCat
M N : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
φ : S ⟶ F.op ⋙ R
φ' : S' ⟶ R
x✝ : Dᵒᵖ
b✝ : ↑(R.obj x✝)
⊢ (ConcreteCategory.hom (CommRingCat.KaehlerDifferential.map ⋯)) (CommRingCat.KaehlerDifferential.d b✝) =
    (ConcreteCategory.hom
        (ModuleCat.restrictScalarsId'App (CommRingCat.Hom.hom (R.map (𝟙 x✝))) ⋯
            (CommRingCat.KaehlerDifferential (φ'.app x✝))).inv)
      (CommRingCat.KaehlerDifferential.d b✝)
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
S' R : Dᵒᵖ ⥤ CommRingCat
M N : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
φ : S ⟶ F.op ⋙ R
φ' : S' ⟶ R
X✝ Y✝ Z✝ : Dᵒᵖ
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ CommRingCat.KaehlerDifferential.map ⋯ =
    CommRingCat.KaehlerDifferential.map ⋯ ≫
      (ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map x✝¹))).map (CommRingCat.KaehlerDifferential.map ⋯) ≫
        (ModuleCat.restrictScalarsComp'App (CommRingCat.Hom.hom (R.map x✝¹)) (CommRingCat.Hom.hom (R.map x✝))
            (CommRingCat.Hom.hom (R.map (x✝¹ ≫ x✝))) ⋯ (CommRingCat.KaehlerDifferential (φ'.app Z✝))).inv

Tactic:
ext

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S : Cᵒᵖ ⥤ CommRingCat
F : C ⥤ D
S' R : Dᵒᵖ ⥤ CommRingCat
M N : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
φ : S ⟶ F.op ⋙ R
φ' : S' ⟶ R
X✝ Y✝ Z✝ : Dᵒᵖ
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
b✝ : ↑(R.obj X✝)
⊢ (ConcreteCategory.hom (CommRingCat.KaehlerDifferential.map ⋯)) (CommRingCat.KaehlerDifferential.d b✝) =
    (ConcreteCategory.hom
        (CommRingCat.KaehlerDifferential.map ⋯ ≫
          (ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map x✝¹))).map (CommRingCat.KaehlerDifferential.map ⋯) ≫
            (ModuleCat.restrictScalarsComp'App (CommRingCat.Hom.hom (R.map x✝¹)) (CommRingCat.Hom.hom (R.map x✝))
                (CommRingCat.Hom.hom (R.map (x✝¹ ≫ x✝))) ⋯ (CommRingCat.KaehlerDifferential (φ'.app Z✝))).inv))
      (CommRingCat.KaehlerDifferential.d b✝)
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
s t : M.sections
h : ∀ (X : Cᵒᵖ), ↑s X = ↑t X
⊢ ↑s = ↑t

Tactic:
ext

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
s t : M.sections
h : ∀ (X : Cᵒᵖ), ↑s X = ↑t X
x✝ : Cᵒᵖ
⊢ ↑s x✝ = ↑t x✝
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M✝ M₁ M₂ : PresheafOfModules R
M : PresheafOfModules R
s : M.sections
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ (unit R).map f ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map
        (ModuleCat.ofHom ((ringLmapEquivSelf ↑(R.obj Y) ℤ ↑(M.obj Y)).symm (↑s Y))) =
    ModuleCat.ofHom ((ringLmapEquivSelf ↑(R.obj X) ℤ ↑(M.obj X)).symm (↑s X)) ≫ M.map f

Tactic:
ext

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M✝ M₁ M₂ : PresheafOfModules R
M : PresheafOfModules R
s : M.sections
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ (ModuleCat.Hom.hom
        ((unit R).map f ≫
          (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map
            (ModuleCat.ofHom ((ringLmapEquivSelf ↑(R.obj Y) ℤ ↑(M.obj Y)).symm (↑s Y)))))
      1 =
    (ModuleCat.Hom.hom (ModuleCat.ofHom ((ringLmapEquivSelf ↑(R.obj X) ℤ ↑(M.obj X)).symm (↑s X)) ≫ M.map f)) 1
Module: Mathlib.CategoryTheory.GradedObject

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
β γ : Type w
e : β ≃ γ
⊢ (fun i ↦ i) = ⇑e.symm ∘ ⇑e

Tactic:
ext

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
β γ : Type w
e : β ≃ γ
x✝ : β
⊢ x✝ = (⇑e.symm ∘ ⇑e) x✝
Module: Mathlib.CategoryTheory.GradedObject

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
β γ : Type w
e : β ≃ γ
⊢ ⇑e ∘ ⇑e.symm = fun i ↦ i

Tactic:
ext

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
β γ : Type w
e : β ≃ γ
x✝ : γ
⊢ (⇑e ∘ ⇑e.symm) x✝ = x✝
Module: Mathlib.CategoryTheory.GradedObject

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
β : Type u_1
inst✝ : AddCommGroup β
s : β
m n : ℤ
⊢ (fun b ↦ b + (m + n) • s) = (fun b ↦ b + m • s) ∘ fun b ↦ b + n • s

Tactic:
ext

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
β : Type u_1
inst✝ : AddCommGroup β
s : β
m n : ℤ
x✝ : β
⊢ x✝ + (m + n) • s = ((fun b ↦ b + m • s) ∘ fun b ↦ b + n • s) x✝
Module: Mathlib.Algebra.Homology.Single

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

Tactic:
ext

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