mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.SimpleModule.Basic

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
f✝ : End (End R M) M
s : Finset M
x : ↥s →₀ M := Finsupp.equivFunOnFinite.symm fun x ↦ ↑x
w✝ : Submodule R (↥s →₀ M)
h : IsCompl (R ∙ x) w✝
p : (↥s →₀ M) →ₗ[R] ↥s →₀ M := (R ∙ x).projection w✝ h
f : End (End R (↥s →₀ M)) (↥s →₀ M) := (End.ringHomEndFinsupp ↥s) f✝
this : f (p • x) = f x
⊢ p (f x) ∈ R ∙ x

Tactic:
]

Goal state after:
R : Type u_2
inst✝³ : Ring R
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
f✝ : End (End R M) M
s : Finset M
x : ↥s →₀ M := Finsupp.equivFunOnFinite.symm fun x ↦ ↑x
w✝ : Submodule R (↥s →₀ M)
h : IsCompl (R ∙ x) w✝
p : (↥s →₀ M) →ₗ[R] ↥s →₀ M := (R ∙ x).projection w✝ h
f : End (End R (↥s →₀ M)) (↥s →₀ M) := (End.ringHomEndFinsupp ↥s) f✝
this : f (p • x) = f x
⊢ p (f x) ∈ R ∙ x
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
S : Type u_3
inst✝² : CommMonoid S
inst✝¹ : DistribMulAction S M
inst✝ : SMulCommClass S R M
x y : M
a : S
hx : a • x = 0
b : S
hy : b • y = 0
⊢ 0 = 0

Tactic:
]

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
S : Type u_3
inst✝² : CommMonoid S
inst✝¹ : DistribMulAction S M
inst✝ : SMulCommClass S R M
a : R
x : M
x✝ : x ∈ {x | ∃ a, a • x = 0}
b : S
h : b • x = 0
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : R
⊢ (∀ ⦃x : M⦄, a • x = 0) ↔ ∀ (m : M), a • m = 0

Tactic:
]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
⊢ (∀ (x : R) (h : x ∈ s) (a : M), ↑⟨x, h⟩ • a = 0) ↔ ∀ x ∈ s, ∀ (m : M), x • m = 0

Tactic:
]

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
s : Set R
x : M
hx : ∀ (a : ↑s), ↑a • x = 0
⊢ ∀ (a : ↑↑(Ideal.span s)), ↑a • x = 0

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
x : M
hx : ∀ (a : ↑s), ↑a • x = 0
⊢ ∀ (a : ↑↑(Ideal.span s)), ↑a • x = 0
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
x : M
hx : ∀ (a : ↑s), ↑a • x = 0
⊢ s ⊆ ↑(Ideal.torsionOf R M x)

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
x : M
hx : ∀ (a : ↑s), ↑a • x = 0
⊢ s ⊆ ↑(Ideal.torsionOf R M 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
a b : R
dvd : a ∣ b
⊢ torsionBySet R M ↑(R ∙ a) ≤ torsionBySet R M {b}

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a b : R
dvd : a ∣ b
⊢ torsionBySet R M ↑(R ∙ a) ≤ torsionBySet R M {b}
Module: Mathlib.RingTheory.Coprime.Ideal

Goal state before:
pp: case refine_2.mpr.refine_3.e_a
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
this : Std.Symm fun x1 x2 ↦ I x1 ⊔ I x2 = ⊤
hs : (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
Hb : ∀ b ∈ ↑t, a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → ↥(⨅ j ∈ t, ⨅ (_ : j ≠ i), I j)
hμ : ∑ i ∈ t, ↑(μ i) = 1
u : R
hu : u ∈ I a
v : R
hv : v ∈ ⨅ i ∈ t, I i
huv : u * 1 + v = 1
j : ι
hj : j ∈ t
⊢ ↑⟨u * ↑(μ j), ⋯⟩ = u * ↑(μ j)

pp: case refine_2.mpr.refine_3.e_a.hnc
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
this : Std.Symm fun x1 x2 ↦ I x1 ⊔ I x2 = ⊤
hs : (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
Hb : ∀ b ∈ ↑t, a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → ↥(⨅ j ∈ t, ⨅ (_ : j ≠ i), I j)
hμ : ∑ i ∈ t, ↑(μ i) = 1
u : R
hu : u ∈ I a
v : R
hv : v ∈ ⨅ i ∈ t, I i
huv : u * 1 + v = 1
j : ι
hj : j ∈ t
⊢ ¬j = a

Tactic:
]

Goal state after:
case refine_2.mpr.refine_3.e_a.hnc
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
this : Std.Symm fun x1 x2 ↦ I x1 ⊔ I x2 = ⊤
hs : (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
Hb : ∀ b ∈ ↑t, a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → ↥(⨅ j ∈ t, ⨅ (_ : j ≠ i), I j)
hμ : ∑ i ∈ t, ↑(μ i) = 1
u : R
hu : u ∈ I a
v : R
hv : v ∈ ⨅ i ∈ t, I i
huv : u * 1 + v = 1
j : ι
hj : j ∈ t
⊢ ¬j = a
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
x✝ : M
h : x✝ = 0
⊢ x✝ ∈ ⊥

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝ : M
h : x✝ = 0
⊢ 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
⊢ torsionBySet R M Set.univ ≤ torsionBySet R M {1}

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ torsionBySet R M Set.univ ≤ torsionBySet R M {1}
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
h : torsionBySet R M s = ⊤
x : M
⊢ x ∈ ⊤

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
h : torsionBySet R M s = ⊤
x : M
⊢ 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
a : R
⊢ torsionBySet R M {a} = ⊤ ↔ torsionBySet R M {a} = ⊤

Tactic:
]

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

Goal state before:
pp: R : Type u_2
A : Type u_3
M : Type u_1
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
m : M
⊢ (of R M a) (a • m) = (of R M a) (a • m)

Tactic:
]

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

Goal state before:
pp: R : Type u_2
A : Type u_3
M : Type u_1
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
m : M
n : ℕ
⊢ (of R M a) (a ^ n • m) = (of R M a) (a ^ n • m)

Tactic:
]

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

Goal state before:
pp: R : Type u_1
A : Type u_3
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
m : AEval R M a
⊢ a • (of R M a).symm m = a • (of R M a).symm m

Tactic:
]

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

Goal state before:
pp: R : Type u_1
A : Type u_3
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
r : R
f : R[X]
m : AEval R M a
⊢ r • (aeval a) f • (of R M a).symm m = r • (aeval a) f • (of R M a).symm m

Tactic:
]

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

Goal state before:
pp: case a
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : (↑S).Pairwise fun i j ↦ p i ⊔ p j = ⊤
h : S.Nonempty
x : M
hx : x ∈ torsionBySet R M ↑(⨅ i ∈ S, p i)
⊢ ∃ μ, ∑ i ∈ S, ↑(μ i) = x

Tactic:
]

Goal state after:
case a
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : (↑S).Pairwise fun i j ↦ p i ⊔ p j = ⊤
h : S.Nonempty
x : M
hx : x ∈ torsionBySet R M ↑(⨅ i ∈ S, p i)
⊢ ∃ μ, ∑ i ∈ S, ↑(μ i) = x
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
n : ℕ
ih :
  ∀ (s : CompositionSeries X) (x : X) (hm : IsMaximal x (last s)),
    head s ≤ x →
      s.length = n → ∃ t, head t = head s ∧ t.length + 1 = n ∧ ∃ (htx : last t = x), s.Equivalent (snoc t (last s) ⋯)
s : CompositionSeries X
x : X
hm : IsMaximal x (last s)
hb : head s ≤ x
hn : s.length = n + 1
h0s : 0 < s.length
hetx : ¬(eraseLast s).last = x
imxs : IsMaximal (x ⊓ (eraseLast s).last) (eraseLast s).last
t : CompositionSeries X
htb : head t = (eraseLast s).head
htl : t.length + 1 = n
htt : last t = x ⊓ (eraseLast s).last
hteqv : Equivalent (eraseLast s) (snoc t (eraseLast s).last ⋯)
hmtx : IsMaximal (last t) x
this : s.Equivalent ((snoc t (eraseLast s).last ⋯).snoc (last s) ⋯)
⊢ x ⊓ (eraseLast s).last = x ⊓ (eraseLast s).last

Tactic:
]

Goal state after:
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)
x : S
y : R[X]
z : PolynomialModule R M
⊢ (algebraMap S R) x • y • z = (algebraMap S R) x • y • z

Tactic:
]

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

Goal state before:
pp: case a.refine_1
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : (↑S).Pairwise fun i j ↦ p i ⊔ p j = ⊤
h : S.Nonempty
x : M
hx : ∀ (a : ↑↑(⨅ i ∈ S, p i)), ↑a • x = 0
μ : (i : ι) → ↥(⨅ j ∈ S, ⨅ (_ : j ≠ i), p j)
hμ : ∑ i ∈ S, ↑(μ i) = 1
i : ι
⊢ ∀ (a : ↑↑(p i)), ↑a • ↑(μ i) • x = 0

Tactic:
]

Goal state after:
case a.refine_1
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : (↑S).Pairwise fun i j ↦ p i ⊔ p j = ⊤
h : S.Nonempty
x : M
hx : ∀ (a : ↑↑(⨅ i ∈ S, p i)), ↑a • x = 0
μ : (i : ι) → ↥(⨅ j ∈ S, ⨅ (_ : j ≠ i), p j)
hμ : ∑ i ∈ S, ↑(μ i) = 1
i : ι
⊢ ∀ (a : ↑↑(p i)), ↑a • ↑(μ i) • x = 0
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 : R
j : ℕ
m : M
⊢ r • id (single R j m) = single R j (r • m)

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 : R
j : ℕ
m : M
⊢ r • id (single R j m) = single R j (r • m)
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: case a.refine_1
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : (↑S).Pairwise fun i j ↦ p i ⊔ p j = ⊤
h : S.Nonempty
x : M
hx : ∀ (a : ↑↑(⨅ i ∈ S, p i)), ↑a • x = 0
μ : (i : ι) → ↥(⨅ j ∈ S, ⨅ (_ : j ≠ i), p j)
hμ : ∑ i ∈ S, ↑(μ i) = 1
i : ι
a : R
ha : a ∈ ↑(p i)
⊢ (↑⟨a, ha⟩ * ↑(μ i)) • x = 0

Tactic:
]

Goal state after:
case a.refine_1
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : (↑S).Pairwise fun i j ↦ p i ⊔ p j = ⊤
h : S.Nonempty
x : M
hx : ∀ (a : ↑↑(⨅ i ∈ S, p i)), ↑a • x = 0
μ : (i : ι) → ↥(⨅ j ∈ S, ⨅ (_ : j ≠ i), p j)
hμ : ∑ i ∈ S, ↑(μ i) = 1
i : ι
a : R
ha : a ∈ ↑(p i)
⊢ (↑⟨a, ha⟩ * ↑(μ i)) • x = 0
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: case zero
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
hb : head s₁ = head s₂
ht : last s₁ = last s₂
hle : s₁.length = 0
⊢ s₂.Equivalent s₂

Tactic:
]

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

Goal state before:
pp: case a.refine_1
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : (↑S).Pairwise fun i j ↦ p i ⊔ p j = ⊤
h : S.Nonempty
x : M
hx : ∀ (a : ↑↑(⨅ i ∈ S, p i)), ↑a • x = 0
μ : (i : ι) → ↥(⨅ j ∈ S, ⨅ (_ : j ≠ i), p j)
hμ : ∑ i ∈ S, ↑(μ i) = 1
i : ι
a : R
ha : a ∈ ↑(p i)
⊢ ∀ (i_1 : ι), a * ↑(μ i) ∈ ⨅ (_ : i_1 ∈ S), p i_1

Tactic:
]

Goal state after:
case a.refine_1
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : (↑S).Pairwise fun i j ↦ p i ⊔ p j = ⊤
h : S.Nonempty
x : M
hx : ∀ (a : ↑↑(⨅ i ∈ S, p i)), ↑a • x = 0
μ : (i : ι) → ↥(⨅ j ∈ S, ⨅ (_ : j ≠ i), p j)
hμ : ∑ i ∈ S, ↑(μ i) = 1
i : ι
a : R
ha : a ∈ ↑(p i)
⊢ ∀ (i_1 : ι), a * ↑(μ i) ∈ ⨅ (_ : i_1 ∈ S), p i_1
Module: Mathlib.Algebra.Polynomial.Module.Basic

Goal state before:
pp: case succ
R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn :
  ∀ (r : R) (j : ℕ) (m : M),
    r •
        (⇑(↑(coeffLinearEquiv R R).symm ∘ₗ Finsupp.lmapDomain M R Nat.succ ∘ₗ ↑(coeffLinearEquiv R R)))^[n]
          (single R j m) =
      single R (n + j) (r • m)
r : R
j : ℕ
m : M
⊢ r •
      (⇑(↑(coeffLinearEquiv R R).symm ∘ₗ Finsupp.lmapDomain M R Nat.succ ∘ₗ ↑(coeffLinearEquiv R R)))^[n]
        ((↑(coeffLinearEquiv R R).symm ∘ₗ Finsupp.lmapDomain M R Nat.succ ∘ₗ ↑(coeffLinearEquiv R R)) (single R j m)) =
    r •
      (⇑(↑(coeffLinearEquiv R R).symm ∘ₗ Finsupp.lmapDomain M R Nat.succ ∘ₗ ↑(coeffLinearEquiv R R)))^[n]
        (single R (1 + j) m)

Tactic:
]

Goal state after:
case succ
R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn :
  ∀ (r : R) (j : ℕ) (m : M),
    r •
        (⇑(↑(coeffLinearEquiv R R).symm ∘ₗ Finsupp.lmapDomain M R Nat.succ ∘ₗ ↑(coeffLinearEquiv R R)))^[n]
          (single R j m) =
      single R (n + j) (r • m)
r : R
j : ℕ
m : M
⊢ r •
      (⇑(↑(coeffLinearEquiv R R).symm ∘ₗ Finsupp.lmapDomain M R Nat.succ ∘ₗ ↑(coeffLinearEquiv R R)))^[n]
        ((↑(coeffLinearEquiv R R).symm ∘ₗ Finsupp.lmapDomain M R Nat.succ ∘ₗ ↑(coeffLinearEquiv R R)) (single R j m)) =
    r •
      (⇑(↑(coeffLinearEquiv R R).symm ∘ₗ Finsupp.lmapDomain M R Nat.succ ∘ₗ ↑(coeffLinearEquiv R R)))^[n]
        (single R (1 + j) m)
Module: Mathlib.Algebra.Polynomial.Module.Basic

Goal state before:
pp: case succ.e_a.e_a
R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn :
  ∀ (r : R) (j : ℕ) (m : M),
    r •
        (⇑(↑(coeffLinearEquiv R R).symm ∘ₗ Finsupp.lmapDomain M R Nat.succ ∘ₗ ↑(coeffLinearEquiv R R)))^[n]
          (single R j m) =
      single R (n + j) (r • m)
r : R
j : ℕ
m : M
⊢ (↑(coeffLinearEquiv R R).symm ∘ₗ Finsupp.lmapDomain M R Nat.succ ∘ₗ ↑(coeffLinearEquiv R R)) (single R j m) =
    single R j.succ m

Tactic:
]

Goal state after:
case succ.e_a.e_a
R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn :
  ∀ (r : R) (j : ℕ) (m : M),
    r •
        (⇑(↑(coeffLinearEquiv R R).symm ∘ₗ Finsupp.lmapDomain M R Nat.succ ∘ₗ ↑(coeffLinearEquiv R R)))^[n]
          (single R j m) =
      single R (n + j) (r • m)
r : R
j : ℕ
m : M
⊢ (↑(coeffLinearEquiv R R).symm ∘ₗ Finsupp.lmapDomain M R Nat.succ ∘ₗ ↑(coeffLinearEquiv R R)) (single R j m) =
    single R j.succ m
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: case a.refine_1
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : (↑S).Pairwise fun i j ↦ p i ⊔ p j = ⊤
h : S.Nonempty
x : M
hx : ∀ (a : ↑↑(⨅ i ∈ S, p i)), ↑a • x = 0
μ : (i : ι) → ↥(⨅ j ∈ S, ⨅ (_ : j ≠ i), p j)
hμ : ∑ i ∈ S, ↑(μ i) = 1
i : ι
a : R
ha : a ∈ ↑(p i)
j : ι
⊢ j ∈ S → a * ↑(μ i) ∈ p j

Tactic:
]

Goal state after:
case a.refine_1
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : (↑S).Pairwise fun i j ↦ p i ⊔ p j = ⊤
h : S.Nonempty
x : M
hx : ∀ (a : ↑↑(⨅ i ∈ S, p i)), ↑a • x = 0
μ : (i : ι) → ↥(⨅ j ∈ S, ⨅ (_ : j ≠ i), p j)
hμ : ∑ i ∈ S, ↑(μ i) = 1
i : ι
a : R
ha : a ∈ ↑(p i)
j : ι
⊢ j ∈ S → a * ↑(μ i) ∈ p j
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
hn : ∃ S, S.Finite ∧ span R S = N
hin : N ≤ I • N
⊢ ∃ r, r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0

Tactic:
]

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
hn : ∃ S, S.Finite ∧ span R S = N
hin : N ≤ I • N
⊢ ∃ r, r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0
Module: Mathlib.RingTheory.Finiteness.Nakayama

Goal state before:
pp: case refine_1
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
⊢ 0 ∈ I

Tactic:
]

Goal state after:
case refine_1
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
⊢ 0 ∈ I
Module: Mathlib.RingTheory.Finiteness.Nakayama

Goal state before:
pp: case refine_2
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
⊢ N ≤ comap ((LinearMap.lsmul R M) 1) (I • N)

Tactic:
]

Goal state after:
case refine_2
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
⊢ N ≤ comap ((LinearMap.lsmul R M) 1) (I • N)
Module: Mathlib.RingTheory.Finiteness.Nakayama

Goal state before:
pp: case refine_2
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
n : M
hn : n ∈ N
⊢ ((LinearMap.lsmul R M) 1) n ∈ I • N

Tactic:
]

Goal state after:
case refine_2
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
n : M
hn : n ∈ N
⊢ ((LinearMap.lsmul R M) 1) n ∈ I • N
Module: Mathlib.RingTheory.Finiteness.Nakayama

Goal state before:
pp: case refine_2
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
n : M
hn : n ∈ N
⊢ n ∈ I • N

Tactic:
]

Goal state after:
case refine_2
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
n : M
hn : n ∈ N
⊢ n ∈ I • N
Module: Mathlib.RingTheory.Finiteness.Nakayama

Goal state before:
pp: case refine_3
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
⊢ N ≤ N

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Nakayama

Goal state before:
pp: case empty
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
r : R
hr1 : r - 1 ∈ I
right✝ : ∅ ⊆ ↑N
n : M
hrn : ((LinearMap.lsmul R M) r) n = 0
hn : n ∈ N
⊢ r • n = 0

Tactic:
]

Goal state after:
case empty
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
r : R
hr1 : r - 1 ∈ I
right✝ : ∅ ⊆ ↑N
n : M
hrn : ((LinearMap.lsmul R M) r) n = 0
hn : n ∈ N
⊢ r • n = 0
Module: Mathlib.Algebra.Polynomial.Module.Basic

Goal state before:
pp: case monomial
R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
g : PolynomialModule R M
n f_n : ℕ
f_a : R
⊢ (if f_n ≤ n then f_a • g.coeff (n - f_n) else 0) =
    ∑ k ∈ Finset.range n.succ, ((monomial f_n) f_a).coeff k • g.coeff (n - k)

Tactic:
]

Goal state after:
case monomial
R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
g : PolynomialModule R M
n f_n : ℕ
f_a : R
⊢ (if f_n ≤ n then f_a • g.coeff (n - f_n) else 0) =
    ∑ k ∈ Finset.range n.succ, ((monomial f_n) f_a).coeff k • g.coeff (n - k)
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: case pos
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : (↑S).Pairwise fun i j ↦ p i ⊔ p j = ⊤
h : S.Nonempty
x : M
hx : ∀ (a : ↑↑(⨅ i ∈ S, p i)), ↑a • x = 0
μ : (i : ι) → ↥(⨅ j ∈ S, ⨅ (_ : j ≠ i), p j)
hμ : ∑ i ∈ S, ↑(μ i) = 1
i : ι
a : R
ha : a ∈ ↑(p i)
j : ι
hj : j ∈ S
ij : j = i
⊢ a * ↑(μ i) ∈ p i

Tactic:
]

Goal state after:
case pos
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : (↑S).Pairwise fun i j ↦ p i ⊔ p j = ⊤
h : S.Nonempty
x : M
hx : ∀ (a : ↑↑(⨅ i ∈ S, p i)), ↑a • x = 0
μ : (i : ι) → ↥(⨅ j ∈ S, ⨅ (_ : j ≠ i), p j)
hμ : ∑ i ∈ S, ↑(μ i) = 1
i : ι
a : R
ha : a ∈ ↑(p i)
j : ι
hj : j ∈ S
ij : j = i
⊢ a * ↑(μ i) ∈ p i
Module: Mathlib.RingTheory.Finiteness.Nakayama

Goal state before:
pp: case insert
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
hrn : N ≤ comap ((LinearMap.lsmul R M) r) (I • (R ∙ i) ⊔ I • span R s)
hs : insert i s ⊆ ↑N
⊢ ∃ r, r - 1 ∈ I ∧ N ≤ comap ((LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N

Tactic:
]

Goal state after:
case insert
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
hrn : N ≤ comap ((LinearMap.lsmul R M) r) (I • (R ∙ i) ⊔ I • span R s)
hs : insert i s ⊆ ↑N
⊢ ∃ r, r - 1 ∈ I ∧ N ≤ comap ((LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N
Module: Mathlib.RingTheory.Finiteness.Nakayama

Goal state before:
pp: case insert
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
hrn : N ≤ comap ((LinearMap.lsmul R M) r) (I • (R ∙ i) ⊔ I • span R s)
hs : i ∈ ↑N ∧ s ⊆ ↑N
⊢ ∃ r, r - 1 ∈ I ∧ N ≤ comap ((LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N

Tactic:
]

Goal state after:
case insert
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
hrn : N ≤ comap ((LinearMap.lsmul R M) r) (I • (R ∙ i) ⊔ I • span R s)
hs : i ∈ ↑N ∧ s ⊆ ↑N
⊢ ∃ r, r - 1 ∈ I ∧ N ≤ comap ((LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N