mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RepresentationTheory.Homological.FiniteCyclic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Finite G
this : Fintype G
g : G
y : MonoidAlgebra k G
⊢ ∀ i ∈ Finset.univ, y.coeff (g⁻¹ * i) = y.coeff (g⁻¹ * i)

Tactic:
lia

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.Resolution

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
n : ℕ
f : k[Fin (n + 1 + 1) → G]
⊢ (Hom.hom ((standardComplex k G).d (n + 1) n)) f = (d k G (n + 1)) f

Tactic:
by
  rw [← Representation.IntertwiningMap.toLinearMap_apply, d_eq]; rfl

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.Resolution

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
x✝ : ↑((standardComplex k G).X 1)
⊢ (forget₂ToModuleCat k G).d 1 0 ≫ (forget₂ToModuleCatHomotopyEquiv k G).hom.f 0 = 0

Tactic:
← (forget₂ToModuleCatHomotopyEquiv k G).1.2 1 0 rfl

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
x✝ : ↑((standardComplex k G).X 1)
⊢ (forget₂ToModuleCatHomotopyEquiv k G).hom.f 1 ≫
      ((ChainComplex.single₀ (ModuleCat k)).obj ((forget₂ (Rep k G) (ModuleCat k)).obj (trivial k G k))).d 1 0 =
    0
Module: Mathlib.RepresentationTheory.Homological.Resolution

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
⊢ QuasiIso (((forget₂ (Rep k G) (ModuleCat k)).mapHomologicalComplex (ComplexShape.down ℕ)).map (εToSingle₀ k G))

Tactic:
have h : QuasiIso (forget₂ToModuleCatHomotopyEquiv k G).hom := inferInstance

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
h : QuasiIso (forget₂ToModuleCatHomotopyEquiv k G).hom
⊢ QuasiIso (((forget₂ (Rep k G) (ModuleCat k)).mapHomologicalComplex (ComplexShape.down ℕ)).map (εToSingle₀ k G))
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
inst✝ : A.IsTrivial
f : Additive G →+ ↑A
g h : G
⊢ (⇑f ∘ ⇑Additive.ofMul) (g * h) = (A.ρ g) ((⇑f ∘ ⇑Additive.ofMul) h) + (⇑f ∘ ⇑Additive.ofMul) g

Tactic:
by
    simp only [Function.comp_apply, ofMul_mul, map_add,
      isTrivial_apply A.ρ g (f (Additive.ofMul h)), add_comm (f (Additive.ofMul g))]

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.TateCohomology.Basic

Goal state before:
pp: R G : Type u
inst✝² : CommRing R
inst✝¹ : Group G
inst✝ : Fintype G
M : Rep R G
⊢ M.tateNorm = ModuleCat.ofHom ((Finsupp.lsum R) fun x ↦ LinearMap.pi fun x ↦ M.ρ.norm)

Tactic:
by
  ext
  simp_all [tateNorm, chainsIso₀, cochainsIso₀, Unique.eq_default]

Goal state after:
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Finite G
η₁ η₂ : Aut (forget k G)
h : η₁.hom.hom.app rightFDRep = η₂.hom.hom.app rightFDRep
this : Fintype G
X : FDRep k G
v : ↑((forget k G).obj X).obj
h1 :
  (forget k G).map (ofRightFDRep X v) ≫ η₁.hom.hom.app X =
    η₁.hom.hom.app rightFDRep ≫ (forget k G).map (ofRightFDRep X v)
h2 :
  (forget k G).map (ofRightFDRep X v) ≫ η₂.hom.hom.app X =
    η₂.hom.hom.app rightFDRep ≫ (forget k G).map (ofRightFDRep X v)
⊢ (Hom.hom (η₁.hom.hom.app X).hom) v = (Hom.hom (η₂.hom.hom.app X).hom) v

Tactic:
rw [h, ← h2] at h1

Goal state after:
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Finite G
η₁ η₂ : Aut (forget k G)
h : η₁.hom.hom.app rightFDRep = η₂.hom.hom.app rightFDRep
this : Fintype G
X : FDRep k G
v : ↑((forget k G).obj X).obj
h1 : (forget k G).map (ofRightFDRep X v) ≫ η₁.hom.hom.app X = (forget k G).map (ofRightFDRep X v) ≫ η₂.hom.hom.app X
h2 :
  (forget k G).map (ofRightFDRep X v) ≫ η₂.hom.hom.app X =
    η₂.hom.hom.app rightFDRep ≫ (forget k G).map (ofRightFDRep X v)
⊢ (Hom.hom (η₁.hom.hom.app X).hom) v = (Hom.hom (η₂.hom.hom.app X).hom) v
Module: Mathlib.RingTheory.MvPolynomial.Ideal

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : σ →₀ ℕ
i : σ
hx : 1 ≤ degree x
hi : ¬x i = 0
⊢ 1 ≤ x i

Tactic:
lia

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Rename

Goal state before:
pp: σ : Type u_1
τ : Type u_2
γ : Type u_3
R : Type u_4
S : Type u_5
f : σ → τ
g : τ → γ
inst✝² : TendstoCofinite f
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
⊢ renameFun f 0 = 0

Tactic:
ext; simp [coeff_renameFun]

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: case mp
G : Type u_1
A : Type u_2
inst✝² : Group G
inst✝¹ : AddCommGroup A
inst✝ : DistribMulAction G A
x : G →₀ A
y : G × G →₀ A
hy : (y.sum fun g a ↦ single g.2 (g.1⁻¹ • a) - single (g.1 * g.2) a + single g.1 a) = x
⊢ ∃ y, (y.sum fun g a ↦ single g.2 a - single (g.1 * g.2) (g.1 • a) + single g.1 (g.1 • a)) = x

Tactic:
use y.sum (fun g a => single g (g.1⁻¹ • a))

Goal state after:
case h
G : Type u_1
A : Type u_2
inst✝² : Group G
inst✝¹ : AddCommGroup A
inst✝ : DistribMulAction G A
x : G →₀ A
y : G × G →₀ A
hy : (y.sum fun g a ↦ single g.2 (g.1⁻¹ • a) - single (g.1 * g.2) a + single g.1 a) = x
⊢ ((y.sum fun g a ↦ single g (g.1⁻¹ • a)).sum fun g a ↦
      single g.2 a - single (g.1 * g.2) (g.1 • a) + single g.1 (g.1 • a)) =
    x
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: case mp
G : Type u_1
A : Type u_2
inst✝² : Group G
inst✝¹ : AddCommGroup A
inst✝ : DistribMulAction G A
x : G × G →₀ A
y : G × G × G →₀ A
hy :
  (y.sum fun g a ↦
      single (g.2.1, g.2.2) (g.1⁻¹ • a) - single (g.1 * g.2.1, g.2.2) a + single (g.1, g.2.1 * g.2.2) a -
        single (g.1, g.2.1) a) =
    x
⊢ ∃ y,
    (y.sum fun g a ↦
        single (g.2.1, g.2.2) a - single (g.1 * g.2.1, g.2.2) (g.1 • a) + single (g.1, g.2.1 * g.2.2) (g.1 • a) -
          single (g.1, g.2.1) (g.1 • a)) =
      x

Tactic:
use y.sum (fun g a => single g (g.1⁻¹ • a))

Goal state after:
case h
G : Type u_1
A : Type u_2
inst✝² : Group G
inst✝¹ : AddCommGroup A
inst✝ : DistribMulAction G A
x : G × G →₀ A
y : G × G × G →₀ A
hy :
  (y.sum fun g a ↦
      single (g.2.1, g.2.2) (g.1⁻¹ • a) - single (g.1 * g.2.1, g.2.2) a + single (g.1, g.2.1 * g.2.2) a -
        single (g.1, g.2.1) a) =
    x
⊢ ((y.sum fun g a ↦ single g (g.1⁻¹ • a)).sum fun g a ↦
      single (g.2.1, g.2.2) a - single (g.1 * g.2.1, g.2.2) (g.1 • a) + single (g.1, g.2.1 * g.2.2) (g.1 • a) -
        single (g.1, g.2.1) (g.1 • a)) =
    x
Module: Mathlib.RingTheory.AdicCompletion.Topology

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : UniformSpace R
inst✝ : IsUniformAddGroup R
I : Ideal R
hI : IsAdic I
this✝ : (𝓝 0).IsCountablyGenerated
this : (𝓤 R).IsCountablyGenerated
H : ∀ (f : ℕ → R), (∀ {m n : ℕ}, m ≤ n → f m - f n ∈ I ^ m) → ∃ L, ∀ (n : ℕ), f n - L ∈ I ^ n
u : ℕ → R
hu : CauchySeq u
⊢ ∀ (i : ℕ), ∃ N, ∀ (m : ℕ), N ≤ m → ∀ (n : ℕ), N ≤ n → u n - u m ∈ I ^ i

Tactic:
simpa using hI.hasBasis_nhds_zero.uniformity_of_nhds_zero.cauchySeq_iff.mp hu

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Topology

Goal state before:
pp: case mpr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : UniformSpace R
inst✝ : IsUniformAddGroup R
I : Ideal R
hI : IsAdic I
this✝ : (𝓝 0).IsCountablyGenerated
this : (𝓤 R).IsCountablyGenerated
H : CompleteSpace R
f : ℕ → R
hf : ∀ {m n : ℕ}, m ≤ n → f m - f n ∈ I ^ m
⊢ ∃ L, ∀ (n : ℕ), f n - L ∈ I ^ n

Tactic:
obtain ⟨L, hL⟩ := CompleteSpace.complete (f := Filter.atTop.map f)
      (hI.hasBasis_nhds_zero.uniformity_of_nhds_zero.cauchySeq_iff.mpr fun i _ ↦
        ⟨i, fun m hm n hn ↦ by simpa using Ideal.sub_mem _ (hf hm) (hf hn)⟩)

Goal state after:
case mpr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : UniformSpace R
inst✝ : IsUniformAddGroup R
I : Ideal R
hI : IsAdic I
this✝ : (𝓝 0).IsCountablyGenerated
this : (𝓤 R).IsCountablyGenerated
H : CompleteSpace R
f : ℕ → R
hf : ∀ {m n : ℕ}, m ≤ n → f m - f n ∈ I ^ m
L : R
hL : Filter.map f Filter.atTop ≤ 𝓝 L
⊢ ∃ L, ∀ (n : ℕ), f n - L ∈ I ^ n
Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology

Goal state before:
pp: case mpr.h.mpr
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
H₁ : ∀ (n : ℕ), IsOpen[top] ↑(J ^ n)
H₂ : ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s
s : Set R
this : SubmodulesRingBasis fun n ↦ J ^ n • ⊤ := Ideal.adic_basis J
n : ℕ
hn : ↑(J ^ n) ⊆ s
⊢ s ∈ 𝓝 0

Tactic:
rw [mem_nhds_iff]

Goal state after:
case mpr.h.mpr
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
H₁ : ∀ (n : ℕ), IsOpen[top] ↑(J ^ n)
H₂ : ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s
s : Set R
this : SubmodulesRingBasis fun n ↦ J ^ n • ⊤ := Ideal.adic_basis J
n : ℕ
hn : ↑(J ^ n) ⊆ s
⊢ ∃ t ⊆ s, IsOpen[top] t ∧ 0 ∈ t
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: case pos
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
j : Fin n
k : ℕ
x : Fin n →₀ ℕ
h1 : ¬(x = single j 1 ∧ k = 0)
h3 : k = 0
⊢ 0 = (coeff x) (X j)

Tactic:
rw [coeff_X, if_neg (by tauto)]

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Finite σ
l m n : ℕ
h : l ≤ m
h' : l ≤ n
p : MvPowerSeries σ R
x : σ →₀ ℕ
hx : degree x < l
⊢ degree x < m

Tactic:
lia

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Finite σ
l m n : ℕ
h : l ≤ m
h' : l ≤ n
p : MvPowerSeries σ R
x : σ →₀ ℕ
hx : degree x < l
⊢ degree x < n

Tactic:
lia

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.LocalRing

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
this : IsLocalRing (AdicCompletion (maximalIdeal R) R)
x : IsLocalRing.ResidueField (AdicCompletion (maximalIdeal R) R)
y : AdicCompletion (maximalIdeal R) R
hy : (residue (AdicCompletion (maximalIdeal R) R)) y = x
z : R
hz : (Ideal.Quotient.mk (maximalIdeal R ^ 1 • ⊤)) z = ↑y 1
⊢ (of (maximalIdeal R) R) ((algebraMap R R) z) - y ∈ (eval (maximalIdeal R) R 1).ker

Tactic:
simpa [eval, sub_eq_zero] using hz

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Completeness

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a b c : ℕ
h : c = b + a
x : AdicCompletion I ↥(I ^ a • ⊤)
⊢ b ≤ c

Tactic:
lia

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Noetherian

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : IsNoetherianRing R
inst✝³ : Module.Finite R M
A : Type u_3
inst✝² : CommRing A
inst✝¹ : IsArtinianRing A
inst✝ : IsLocalRing A
f : ℕ → A
hf : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD maximalIdeal A ^ m • ⊤]
n : ℕ
hn : maximalIdeal A ^ n = 0
m : ℕ
h : ¬m ≤ n
⊢ n ≤ m

Tactic:
lia

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Completeness

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a b c : ℕ
x : AdicCompletion I M
h : c = b + a
ha : ↑x a = 0
⊢ a ≤ c

Tactic:
lia

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Completeness

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a b c n : ℕ
x : AdicCompletion I M
hxn : ↑x n = 0
i k : ℕ
h : i ≤ i + k
⊢ i + n ≤ i + k + n

Tactic:
lia

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Completeness

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
s : Finset R
hs : Ideal.span ↑s = I ^ n
x : AdicCompletion I ↥(I ^ n • ⊤)
⊢ Function.Surjective ⇑(LinearMap.codRestrict (I ^ n • ⊤) ((lsum R) fun i ↦ ↑i • LinearMap.id) ⋯)

Tactic:
rw [← LinearMap.range_eq_top, LinearMap.range_codRestrict, ← hs, span_smul_eq,
      smul_top_eq_range_lsum]

Goal state after:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
s : Finset R
hs : Ideal.span ↑s = I ^ n
x : AdicCompletion I ↥(I ^ n • ⊤)
⊢ comap ((lsum R) fun i ↦ ↑i • LinearMap.id).range.subtype ((lsum R) fun i ↦ ↑i • LinearMap.id).range = ⊤
Module: Mathlib.RingTheory.AdicCompletion.Completeness

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
fg : I.FG
x : AdicCompletion I R
⊢ x ∈ RingHom.ker (evalOneₐ I).toRingHom ↔ x ∈ (eval I R 1).ker

Tactic:
have eq : I ^ 1 * ⊤ = I := by simp

Goal state after:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
fg : I.FG
x : AdicCompletion I R
eq : I ^ 1 * ⊤ = I
⊢ x ∈ RingHom.ker (evalOneₐ I).toRingHom ↔ x ∈ (eval I R 1).ker
Module: Mathlib.RingTheory.Coalgebra.GroupLike

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup A
inst✝² : Module R A
inst✝¹ : Coalgebra R A
inst✝ : IsTorsionFree R A
a : A
s : Finset A
has : a ∉ s
ha : IsGroupLikeElem R a
hs : ∀ a ∈ s, IsGroupLikeElem R a
d : R
c : A → R
hc : ∑ a ∈ s, c a • a = d • a
ih :
  ∀ (f g : A × A → R), ∑ x ∈ s ×ˢ s, f x • x.1 ⊗ₜ[R] x.2 = ∑ x ∈ s ×ˢ s, g x • x.1 ⊗ₜ[R] x.2 → ∀ i ∈ s ×ˢ s, f i = g i
⊢ d • comul (d • a) = (d • a) ⊗ₜ[R] (d • a)

Tactic:
simp [ha.comul_eq_tmul_self, smul_tmul, tmul_smul, -neg_smul]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
r : R
⊢ ((monomial 0) r).contentIdeal = span {r}

Tactic:
exact contentIdeal_monomial 0 r

Goal state after:
Module: Mathlib.RingTheory.Bialgebra.MonoidAlgebra

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
M : Type u_8
N : Type u_9
O : Type u_10
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Bialgebra R A
inst✝³ : Bialgebra R B
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
e : M ≃* N
⊢ (counitAlgHom R A[N]).comp ↑(domCongr R A e) = counitAlgHom R A[M]

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.RingTheory.Bialgebra.MonoidAlgebra

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
M : Type u_8
N : Type u_9
O : Type u_10
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Bialgebra R A
inst✝³ : Bialgebra R B
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
⊢ (counitAlgHom R (AddMonoidAlgebra A (Additive M))).comp ↑(toAdditiveAlgEquiv R A M) = counitAlgHom R A[M]

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.RingTheory.Bialgebra.MonoidAlgebra

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_8
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommMonoid M
f : R →+* S
⊢ (comulAlgHom S S[M]).comp (mapRingHom M f) =
    (Algebra.TensorProduct.mapRingHom f (mapRingHom M f) (mapRingHom M f) ⋯ ⋯).comp (comulAlgHom R R[M]).toRingHom

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.RingTheory.Bialgebra.MonoidAlgebra

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_8
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommMonoid M
f : R →+* S
⊢ (counitAlgHom S S[M]).comp (mapRingHom M f) = f.comp (counitAlgHom R R[M]).toRingHom

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.RingTheory.Bialgebra.MonoidAlgebra

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
M : Type u_8
N : Type u_9
O : Type u_10
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : Bialgebra R A
inst✝² : Bialgebra R B
inst✝¹ : AddMonoid M
inst✝ : AddMonoid N
⊢ (counitAlgHom R (MonoidAlgebra A (Multiplicative M))).comp ↑(toMultiplicativeAlgEquiv R A M) = counitAlgHom R A[M]

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.RingTheory.Bialgebra.MonoidAlgebra

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_8
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : AddCommMonoid M
f : R →+* S
⊢ (comulAlgHom S S[M]).comp (mapRingHom M f) =
    (Algebra.TensorProduct.mapRingHom f (mapRingHom M f) (mapRingHom M f) ⋯ ⋯).comp (comulAlgHom R R[M]).toRingHom

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.RingTheory.Bialgebra.MonoidAlgebra

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_8
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : AddCommMonoid M
f : R →+* S
⊢ (counitAlgHom S S[M]).comp (mapRingHom M f) = f.comp (counitAlgHom R R[M]).toRingHom

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.SelmerGroup

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : Kˣ
⊢ (valuation K v) ↑x = ?m.34 * ?m.36

Tactic:
rw [valuation_def]

Goal state after:
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : Kˣ
⊢ (v.intValuation.extendToLocalization ⋯ K) ↑x = ?m.34 * ?m.36
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n✝ : ℕ
x✝ y✝ : A
ha : x✝ ∈ ⊥
hb : y✝ ∈ ⊥
⊢ (if x✝ + y✝ = 0 ∧ n✝ = 0 then 1 else 0) =
    ∑ k ∈ antidiagonal n✝, (if x✝ = 0 ∧ k.1 = 0 then 1 else 0) * if y✝ = 0 ∧ k.2 = 0 then 1 else 0

Tactic:
by
    rw [mem_bot.mp ha, mem_bot.mp hb, add_zero]
    simp only [true_and, mul_ite, mul_one, mul_zero]
    split_ifs with h
    · simp [h]
    · symm
      apply sum_eq_zero
      grind [mem_antidiagonal]

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

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
n : ℕ
hn : n ≠ 0
⊢ 0 * hI.dpow n 0 = 0 * 0

Tactic:
zero_mul,

Goal state after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
n : ℕ
hn : n ≠ 0
⊢ 0 = 0 * 0
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: case C
R : Type u_4
M : Type u_5
ι : Type u_6
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
hv : Submodule.span R (Set.range v) = ⊤
r : R
⊢ r • 1 ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))

Tactic:
exact smul_mem _ _ (subset_span ⟨0, by simp⟩)

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

Goal state before:
pp: A : Type u_1
inst✝² : CommSemiring A
M : Type u_2
inst✝¹ : AddCommMonoid M
I : AddSubmonoid M
dpow : ℕ → M → A
dpow_zero : ∀ {x : M}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_3
inst✝ : DecidableEq ι
x : ι → M
dpow_add : ∀ {n : ℕ} {x y : M}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_1 ∈ range n.succ, dpow x_1 x * dpow (n - x_1) y
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, x i ∈ I) → ∀ {n : ℕ}, dpow n (s.sum x) = ∑ k ∈ s.sym n, ∏ i ∈ s, dpow (Multiset.count i ↑k) (x i)
hx : ∀ i ∈ insert a s, x i ∈ I
n : ℕ
hx' : ∀ i ∈ s, x i ∈ I
m : Sym ι n
hm : ∀ a_1 ∈ m, a_1 = a ∨ a_1 ∈ s
i : ι
hi : i ∈ s
⊢ Multiset.count i ↑m = Multiset.count i ↑(Sym.filterNe a m).snd

Tactic:
conv_lhs => rw [← m.fill_filterNe a]

Goal state after:
A : Type u_1
inst✝² : CommSemiring A
M : Type u_2
inst✝¹ : AddCommMonoid M
I : AddSubmonoid M
dpow : ℕ → M → A
dpow_zero : ∀ {x : M}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_3
inst✝ : DecidableEq ι
x : ι → M
dpow_add : ∀ {n : ℕ} {x y : M}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_1 ∈ range n.succ, dpow x_1 x * dpow (n - x_1) y
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, x i ∈ I) → ∀ {n : ℕ}, dpow n (s.sum x) = ∑ k ∈ s.sym n, ∏ i ∈ s, dpow (Multiset.count i ↑k) (x i)
hx : ∀ i ∈ insert a s, x i ∈ I
n : ℕ
hx' : ∀ i ∈ s, x i ∈ I
m : Sym ι n
hm : ∀ a_1 ∈ m, a_1 = a ∨ a_1 ∈ s
i : ι
hi : i ∈ s
⊢ Multiset.count i ↑(Sym.fill a (Sym.filterNe a m).fst (Sym.filterNe a m).snd) =
    Multiset.count i ↑(Sym.filterNe a m).snd
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: A : Type u_1
inst✝³ : CommSemiring A
ι : Type u_2
inst✝² : DecidableEq ι
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra A S
J : Ideal S
hJ : DividedPowers J
b : ι → S
x : ι →₀ A
hx : ∀ i ∈ x.support, b i ∈ J
n : ℕ
⊢ hJ.dpow n (∑ a ∈ x.support, x a • b a) =
    ∑ k ∈ x.support.sym n, x.prod fun i r ↦ r ^ Multiset.count i ↑k • hJ.dpow (Multiset.count i ↑k) (b i)

Tactic:
hJ.dpow_sum (fun i hi ↦ Submodule.smul_of_tower_mem J _ (hx i hi))

Goal state after:
A : Type u_1
inst✝³ : CommSemiring A
ι : Type u_2
inst✝² : DecidableEq ι
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra A S
J : Ideal S
hJ : DividedPowers J
b : ι → S
x : ι →₀ A
hx : ∀ i ∈ x.support, b i ∈ J
n : ℕ
⊢ ∑ k ∈ x.support.sym n, ∏ i ∈ x.support, hJ.dpow (Multiset.count i ↑k) (x i • b i) =
    ∑ k ∈ x.support.sym n, x.prod fun i r ↦ r ^ Multiset.count i ↑k • hJ.dpow (Multiset.count i ↑k) (b i)
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
m✝ n✝ : ℕ
x✝ : B
hx : x✝ ∈ J
⊢ e ↑((m✝ + n✝).choose m✝) * e (hI.dpow (m✝ + n✝) (e.symm x✝)) =
    ↑((m✝ + n✝).choose m✝) * e (hI.dpow (m✝ + n✝) (e.symm x✝))

Tactic:
simp only [map_natCast]

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.Padic

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
x : ℤ_[p]
hx : x ∈ Ideal.span {↑p}
⊢ ‖(↑n !)⁻¹ʳ * ↑x ^ n‖ ≤ (↑p)⁻¹

Tactic:
by_cases hx0 : x = 0

Goal state after:
case pos
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
x : ℤ_[p]
hx : x ∈ Ideal.span {↑p}
hx0 : x = 0
⊢ ‖(↑n !)⁻¹ʳ * ↑x ^ n‖ ≤ (↑p)⁻¹

case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
x : ℤ_[p]
hx : x ∈ Ideal.span {↑p}
hx0 : ¬x = 0
⊢ ‖(↑n !)⁻¹ʳ * ↑x ^ n‖ ≤ (↑p)⁻¹
Module: Mathlib.RingTheory.Regular.RegularSequence

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a b : R
h2 : torsionBy R M b = a • torsionBy R M b → IsSMulRegular M b
ha : IsSMulRegular M a
hb : IsSMulRegular (QuotSMulTop a M) b
⊢ IsSMulRegular M b ∧ IsSMulRegular (QuotSMulTop b M) a

Tactic:
specialize h2 (le_antisymm ?_ (smul_le_self_of_tower a (torsionBy R M b)))

Goal state after:
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a b : R
h2 : torsionBy R M b = a • torsionBy R M b → IsSMulRegular M b
ha : IsSMulRegular M a
hb : IsSMulRegular (QuotSMulTop a M) b
⊢ torsionBy R M b ≤ a • torsionBy R M b

R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a b : R
h2 : IsSMulRegular M b
ha : IsSMulRegular M a
hb : IsSMulRegular (QuotSMulTop a M) b
⊢ IsSMulRegular M b ∧ IsSMulRegular (QuotSMulTop b M) a
Module: Mathlib.RingTheory.DividedPowers.Padic

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
⊢ (dividedPowers p).dpow n x = if hx : x ∈ Ideal.span {↑p} then ⟨dpow' p n ↑x, ⋯⟩ else 0

Tactic:
simp only [dividedPowers, ofInjective]
  split_ifs with hx
  · have hinj : Injective (PadicInt.Coe.ringHom (p := p)) :=
      (Set.injective_codRestrict Subtype.property).mp fun ⦃a₁ a₂⦄ a ↦ a
    have heq : Coe.ringHom ⟨dpow' p n x, dpow'_int p n hx⟩ =
        inverse (n ! : ℚ_[p]) * Coe.ringHom x ^ n := by
      simp [dpow', inverse_eq_inv', Coe.ringHom_apply]
    simpa only [← hinj.eq_iff, (Exists.choose_spec (_ : ∃ a, ∃ _, Coe.ringHom a = _)).2,
      RatAlgebra.dpow_apply, Submodule.mem_top] using! heq.symm
  · rfl

Goal state after:
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
r : R
⊢ IsNilpotent (inl r) ↔ IsNilpotent r

Tactic:
rw [isNilpotent_iff_isNilpotent_fst, fst_inl]

Goal state after:
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x : R[ε]
⊢ TrivSqZeroExt.fst x = 0 ↔
    ∃ c,
      TrivSqZeroExt.fst x = 0 * TrivSqZeroExt.fst c ∧
        TrivSqZeroExt.snd x = 0 • TrivSqZeroExt.snd c + MulOpposite.op (TrivSqZeroExt.fst c) • 1

Tactic:
zero_mul,

Goal state after:
R : Type u_1
inst✝ : Semiring R
x : R[ε]
⊢ TrivSqZeroExt.fst x = 0 ↔
    ∃ c,
      TrivSqZeroExt.fst x = 0 ∧ TrivSqZeroExt.snd x = 0 • TrivSqZeroExt.snd c + MulOpposite.op (TrivSqZeroExt.fst c) • 1