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
N : Type u_5
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : IsSemisimpleModule R M
P : Type u_6
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : N →ₗ[R] M
hf : Function.Injective ⇑f
g : N →ₗ[R] P
m : Submodule R M
compl : IsCompl f.range m
x✝ : N
⊢ ((g ∘ₗ LinearMap.linearProjOfIsCompl m f hf compl) ∘ₗ f) x✝ = g x✝

Tactic:
simp

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

Goal state before:
pp: case refine_2.mpr.refine_2
ι : 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 + v = 1
i : ι
hi : ¬i = a
this : ∀ i_1 ∈ t, i_1 ≠ i → ↑(μ i) ∈ I i_1
⊢ ∀ i_1 ∈ Finset.cons a t hat, i_1 ≠ i → u * ↑(μ i) ∈ I i_1

Tactic:
intro j

Goal state after:
case refine_2.mpr.refine_2
ι : 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 + v = 1
i : ι
hi : ¬i = a
this : ∀ i_1 ∈ t, i_1 ≠ i → ↑(μ i) ∈ I i_1
j : ι
⊢ j ∈ Finset.cons a t hat → j ≠ i → u * ↑(μ i) ∈ I j
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
⊢ (snoc t x hmtx).last = x

Tactic:
simp

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

Goal state before:
pp: ι : Type u_3
R : Type u_4
M : Type u_5
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h_ne_zero : ∀ (i : ι), torsionOf R M (v i) = ⊥
i : ι
r : R
hi : r • v i ∈ Submodule.span R (v '' (Set.univ \ {i}))
hv : R ∙ v i ⊓ Submodule.span R (Set.range fun i_1 ↦ v ↑i_1) = ⊥
x✝ : M
⊢ (x✝ ∈ Set.range fun i_1 ↦ v ↑i_1) ↔ x✝ ∈ v '' (Set.univ \ {i})

Tactic:
simp

Goal state after:
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
⊢ ∀ x ∈ t, ↑(if hi : x = a then ⟨v, ⋯⟩ else ⟨u * ↑(μ x), ⋯⟩) = u * ↑(μ x)

Tactic:
intro j

Goal state after:
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 : ι
⊢ j ∈ t → ↑(if hi : j = a then ⟨v, ⋯⟩ else ⟨u * ↑(μ j), ⋯⟩) = u * ↑(μ j)
Module: Mathlib.RingTheory.SimpleModule.Basic

Goal state before:
pp: case zero
R : Type u_2
inst✝⁴ : Ring R
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsSemisimpleModule R M
inst✝ : Module.Finite (End R M) M
s : Finset M
hs : span (End R M) ↑s = ⊤
f : End (End R M) M
r : R
hr : ∀ m ∈ s, f m = r • m
m : M
⊢ ((toModuleEnd (End R M) M) r) 0 = f 0

Tactic:
simp

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
t : R
m : AEval R M a
⊢ (of R M a).symm (C t • m) = (of R M a).symm (t • m)

Tactic:
simp

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

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
m₁ m₂ : M
a✝ : ℕ
⊢ (single R n (m₁ + m₂)).coeff a✝ = (single R n m₁ + single R n m₂).coeff a✝

Tactic:
simp

Goal state after:
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x : X
hm : IsMaximal x (last s)
hb : head s ≤ x
⊢ ∃ t, head t = head s ∧ t.length + 1 = s.length ∧ ∃ (htx : last t = x), s.Equivalent (snoc t (last s) ⋯)

Tactic:
induction hn : s.length generalizing s x with
  | zero =>
    exact (ne_of_gt (lt_of_le_of_lt hb (lt_of_isMaximal hm))
      (subsingleton_of_length_eq_zero hn s.last_mem s.head_mem)).elim
  | succ n ih =>
    have h0s : 0 < s.length := hn.symm ▸ Nat.succ_pos _
    by_cases hetx : s.eraseLast.last = x
    · use s.eraseLast
      simp [← hetx, hn, Equivalent.refl]
    · have imxs : IsMaximal (x ⊓ s.eraseLast.last) s.eraseLast.last :=
        isMaximal_of_eq_inf x s.last rfl (Ne.symm hetx) hm (isMaximal_eraseLast_last h0s)
      have := ih _ _ imxs (le_inf (by simpa) (le_last_of_mem s.eraseLast.head_mem)) (by simp [hn])
      rcases this with ⟨t, htb, htl, htt, hteqv⟩
      have hmtx : IsMaximal t.last x :=
        isMaximal_of_eq_inf s.eraseLast.last s.last (by rw [inf_comm, htt]) hetx
          (isMaximal_eraseLast_last h0s) hm
      use snoc t x hmtx
      refine ⟨by simp [htb], by simp [htl], by simp, ?_⟩
      have : s.Equivalent ((snoc t s.eraseLast.last <| show IsMaximal t.last _ from
        htt.symm ▸ imxs).snoc s.last
          (by simpa using isMaximal_eraseLast_last h0s)) := by
        conv_lhs => rw [eq_snoc_eraseLast h0s]
        exact Equivalent.snoc hteqv (by simpa using iso_refl)
      refine this.trans <| Equivalent.snoc_snoc_swap
        (iso_symm
            (second_iso_of_eq hm
              (sup_eq_of_isMaximal hm (isMaximal_eraseLast_last h0s) (Ne.symm hetx)) htt.symm))
        (second_iso_of_eq (isMaximal_eraseLast_last h0s)
            (sup_eq_of_isMaximal (isMaximal_eraseLast_last h0s) hm hetx) (by rw [inf_comm, htt]))

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:
intro j

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 : ι
⊢ a * ↑(μ i) ∈ ⨅ (_ : j ∈ S), p j
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 + 1]
        (single R j m) =
    single R (n + 1 + j) (r • m)

Tactic:
rw [Function.iterate_succ, Function.comp_apply, add_assoc, ← hn]

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 zero
R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
r : R
n : ℕ
⊢ ((monomial i) r • 0).coeff n = if i ≤ n then r • (coeff 0) (n - i) else 0

Tactic:
simp

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

Tactic:
simp

Goal state after:
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
i : ℕ
m : M
n n✝ : ℕ
a✝ : R
⊢ ((monomial n✝) a✝ • single R i m).coeff n = if i ≤ n then ((monomial n✝) a✝).coeff (n - i) • m else 0

Tactic:
simp

Goal state after:
case monomial
R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
m : M
n n✝ : ℕ
a✝ : R
⊢ (Finsupp.single (n✝ + i) (a✝ • m)) n = if i ≤ n then ((monomial n✝) a✝).coeff (n - i) • m else 0
Module: Mathlib.Algebra.Polynomial.Module.Basic

Goal state before:
pp: case zero
ι : 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 : R[X]
⊢ (toFinsuppIso R).symm (AddMonoidAlgebra.coeffAddEquiv.symm (coeffAddEquiv (r • 0))) =
    r * (toFinsuppIso R).symm (AddMonoidAlgebra.coeffAddEquiv.symm (coeffAddEquiv 0))

Tactic:
simp

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

Tactic:
simp

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

Goal state before:
pp: case pos
ι : 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 : R[X]
n : ℕ
a : R
i : ℕ
hn : n ≤ i
⊢ r.coeff (i - n) * a = (r * (monomial n) a).coeff i

Tactic:
show i = (i - n) + n by lia,

Goal state after:
case pos
ι : 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 : R[X]
n : ℕ
a : R
i : ℕ
hn : n ≤ i
⊢ r.coeff (i - n + n - n) * a = (r * (monomial n) a).coeff (i - n + n)
Module: Mathlib.Algebra.Polynomial.Module.Basic

Goal state before:
pp: case pos
ι : 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 : R[X]
n : ℕ
a : R
i : ℕ
hn : n ≤ i
⊢ r.coeff (i - n + n - n) * a = r.coeff (i - n) * a

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.ReesAlgebra

Goal state before:
pp: case pos
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
⊢ 1 ∈ I ^ 0

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.ReesAlgebra

Goal state before:
pp: case neg
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
i : ℕ
h : ¬i = 0
⊢ 0 ∈ I ^ i

Tactic:
simp

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
r : R[X]
x : PolynomialModule R R
⊢ (toFinsuppIso R).symm (AddMonoidAlgebra.coeffAddEquiv.symm (coeffAddEquiv (r • x))) =
    r * (toFinsuppIso R).symm (AddMonoidAlgebra.coeffAddEquiv.symm (coeffAddEquiv x))

Tactic:
induction x using induction_linear with
    | zero => simp
    | add _ _ hp hq => simp_all [smul_add, mul_add]
    | single n a =>
    ext i
    simp only [coeffAddEquiv_apply, AddMonoidAlgebra.coeffAddEquiv_symm_apply,
      toFinsuppIso_symm_apply, coeff_ofFinsupp, smul_single_apply, smul_eq_mul, coeff_single,
      AddMonoidAlgebra.ofCoeff_single, ofFinsupp_single]
    split_ifs with hn
    · rw [show i = (i - n) + n by lia, Polynomial.coeff_mul_monomial]
      simp
    · rw [Polynomial.coeff_mul, Finset.sum_eq_zero]
      simp [Polynomial.coeff_monomial]
      lia

Goal state after:
Module: Mathlib.RingTheory.ReesAlgebra

Goal state before:
pp: case pos
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
r : R
⊢ (algebraMap R R) r ∈ I ^ 0

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.ReesAlgebra

Goal state before:
pp: case neg
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
r : R
i : ℕ
h : ¬i = 0
⊢ 0 ∈ I ^ i

Tactic:
simp

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

Goal state before:
pp: case refine_2.e_g
ι : 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
i : ℕ
c : M
⊢ r ^ i • s • c = s • r ^ i • c

Tactic:
rw [smul_comm]

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

Goal state before:
pp: case zero
R : Type u_2
inst✝² : CommRing R
S : Type u_8
inst✝¹ : CommRing S
inst✝ : Algebra S R
x : R
⊢ (aeval x) (equivPolynomial 0) = (eval x) ((map R (Algebra.linearMap S R)) 0)

Tactic:
simp

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
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)
⊢ ∀ i_1 ∈ T, p i ⊔ p i_1 = ⊤

Tactic:
intro j

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 : ι
⊢ j ∈ T → p i ⊔ p j = ⊤
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: case zero
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
j : ℕ
⊢ I ^ 0 • F.N j ≤ F.N (0 + j)

Tactic:
simp

Goal state after:
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 : I.Filtration M
n₀ : ℕ
hn : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
⊢ F.N (n₀ + 0) = I ^ 0 • F.N n₀

Tactic:
simp

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

Goal state before:
pp: A : Type u_3
inst✝ : AddCommGroup A
n : ℤ
a : A
⊢ a ∈ A[-n] ↔ a ∈ A[n]

Tactic:
simp

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

Goal state after:
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 F' : I.Filtration M
e : F.N 0 ≤ F'.N 0
n₀ : ℕ
hF : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
n : ℕ
hn : F.N (n + n₀) ≤ F'.N n
⊢ n + n₀ ≥ n₀

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: case h.refine_1
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
h : F.Stable
h' : F'.Stable
e : F.N 0 = F'.N 0
n₁ : ℕ
h₁ : ∀ (n : ℕ), F.N (n + n₁) ≤ F'.N n
n₂ : ℕ
h₂ : ∀ (n : ℕ), F'.N (n + n₂) ≤ F.N n
n : ℕ
⊢ n + n₁ ≤ n + max n₁ n₂

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: case h.refine_2
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
h : F.Stable
h' : F'.Stable
e : F.N 0 = F'.N 0
n₁ : ℕ
h₁ : ∀ (n : ℕ), F.N (n + n₁) ≤ F'.N n
n₂ : ℕ
h₂ : ∀ (n : ℕ), F'.N (n + n₂) ≤ F.N n
n : ℕ
⊢ n + n₂ ≤ n + max n₁ n₂

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Filtration

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
F : I.Filtration M
f : PolynomialModule R M
⊢ f ∈ F.submodule.toAddSubmonoid → f ∈ AddSubmonoid.closure (⋃ i, single R i '' ↑(F.N i))

Tactic:
hf

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
F : I.Filtration M
f : PolynomialModule R M
hf : f ∈ F.submodule.toAddSubmonoid
⊢ f ∈ AddSubmonoid.closure (⋃ i, single R i '' ↑(F.N i))
Module: Mathlib.Algebra.Category.ModuleCat.Differentials.Basic

Goal state before:
pp: A B : CommRingCat
M : ModuleCat ↑B
f : A ⟶ B
d : ↑B → ↑M
d_add : ∀ (b b' : ↑B), d (b + b') = d b + d b'
d_mul : ∀ (b b' : ↑B), d (b * b') = b • d b' + b' • d b
d_map : ∀ (a : ↑A), d ((ConcreteCategory.hom f) a) = 0
this✝ : Algebra ↑A ↑B := (CommRingCat.Hom.hom f).toAlgebra
this : Module ↑A ↑M := Module.compHom (↑M) (CommRingCat.Hom.hom f)
a : ↑A
b : ↑B
⊢ d (a • b) = (RingHom.id ↑A) a • d b

Tactic:
by
      dsimp
      rw [RingHom.smul_toAlgebra, d_mul, d_map, smul_zero, add_zero]
      rfl

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

Goal state before:
pp: A B A' B' : CommRingCat
f : A ⟶ B
f' : A' ⟶ B'
g : A ⟶ A'
g' : B ⟶ B'
fac : g ≫ f' = f ≫ g'
this : Algebra ↑A ↑B := (Hom.hom f).toAlgebra
⊢ ∀ (b b' : ↑B),
    (_root_.KaehlerDifferential.D ↑A ↑B) (b + b') =
      (_root_.KaehlerDifferential.D ↑A ↑B) b + (_root_.KaehlerDifferential.D ↑A ↑B) b'

Tactic:
simp

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

Goal state before:
pp: A B A' B' : CommRingCat
f : A ⟶ B
f' : A' ⟶ B'
g : A ⟶ A'
g' : B ⟶ B'
fac : g ≫ f' = f ≫ g'
this : Algebra ↑A ↑B := (Hom.hom f).toAlgebra
⊢ ∀ (b b' : ↑B),
    (_root_.KaehlerDifferential.D ↑A ↑B) (b * b') =
      b • (_root_.KaehlerDifferential.D ↑A ↑B) b' + b' • (_root_.KaehlerDifferential.D ↑A ↑B) b

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I : Ideal R
x : ↥I
⊢ x ∈ I.toCotangent.ker ↔ ↑x ∈ Submodule.map (Submodule.subtype I) I.toCotangent.ker

Tactic:
simp

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

Goal state before:
pp: R : Type u
S : Type v
S' : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : CommSemiring S'
inst✝⁶ : Algebra S' R
inst✝⁵ : Algebra S S'
inst✝⁴ : IsScalarTower S S' R
I✝ : Ideal R
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal R
__spread✝⁻⁰ : I.Cotangent →ₗ[R] I.Cotangent := lift (I.toCotangent ∘ₗ ↑(LinearEquiv.ofEq I I ⋯)) ⋯
x : ↥I
⊢ (lift (I.toCotangent ∘ₗ ↑(LinearEquiv.ofEq I I ⋯)) ⋯)
      ((lift (I.toCotangent ∘ₗ ↑(LinearEquiv.ofEq I I ⋯)) ⋯).toFun (I.toCotangent x)) =
    I.toCotangent x

Tactic:
simp

Goal state after: