mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Bialgebra.MonoidAlgebra

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

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case h_of
R : Type u_1
S : Type u_2
M : Type u_8
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : AddCommMonoid M
f : R →+* S
x✝ : M
⊢ Additive.toMul ((MonoidHom.toAdditiveRight ((↑((counitAlgHom S S[M]).comp (mapRingHom M f))).comp (of R M))) x✝) =
    Additive.toMul ((MonoidHom.toAdditiveRight ((↑(f.comp (counitAlgHom R R[M]).toRingHom)).comp (of R M))) x✝)

Tactic:
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✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : AddCommGroup G
inst✝ : AddCommGroup H
f g : G →+ H
⊢ (mapDomainBialgHomEquiv.trans ((WithConv.equiv (R[G] →ₐc[R] R[H])).symm.trans Additive.ofMul)).toFun (f + g) =
    (mapDomainBialgHomEquiv.trans ((WithConv.equiv (R[G] →ₐc[R] R[H])).symm.trans Additive.ofMul)).toFun f +
      (mapDomainBialgHomEquiv.trans ((WithConv.equiv (R[G] →ₐc[R] R[H])).symm.trans Additive.ofMul)).toFun g

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Regular.IsSMulRegular

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherianRing R
⊢ {r | ∃ x, x ≠ 0 ∧ r • x = 0} = {a | ¬IsSMulRegular M a}

Tactic:
isSMulRegular_iff_right_eq_zero_of_smul,

Goal state after:
R : Type u_1
M : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherianRing R
⊢ {r | ∃ x, x ≠ 0 ∧ r • x = 0} = {a | ¬∀ (m : M), a • m = 0 → m = 0}
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
p : Ideal R
hp : p ∈ (annihilator R M).minimalPrimes
prime : p.IsPrime
Rₚ : Type u_1 := Localization.AtPrime p
this : Nontrivial (LocalizedModule p.primeCompl M)
q : Ideal Rₚ
hq : q ∈ associatedPrimes Rₚ (LocalizedModule p.primeCompl M)
⊢ p ∈ associatedPrimes R M

Tactic:
have q_prime : q.IsPrime := IsAssociatedPrime.isPrime hq

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
p : Ideal R
hp : p ∈ (annihilator R M).minimalPrimes
prime : p.IsPrime
Rₚ : Type u_1 := Localization.AtPrime p
this : Nontrivial (LocalizedModule p.primeCompl M)
q : Ideal Rₚ
hq : q ∈ associatedPrimes Rₚ (LocalizedModule p.primeCompl M)
q_prime : q.IsPrime
⊢ p ∈ associatedPrimes R M
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: case neg
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m n : ℕ
a : A
hn : n ≠ 0
ha : a ∈ ⊥
hm : ¬m = 0
⊢ (if (if 0 = 0 ∧ n = 0 then 1 else 0) = 0 ∧ m = 0 then 1 else 0) = if m = 0 ∨ n = 0 then ↑(m.uniformBell n) else 0

Tactic:
simp only [hm, and_false, ite_false, false_or, if_neg hn]

Goal state after:
Module: Mathlib.RingTheory.Depth.Rees

Goal state before:
pp: case zero
R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
I : Ideal R
N : ModuleCat R
Nfin : Module.Finite R ↑N
Nsupp : Module.support R ↑N ⊆ PrimeSpectrum.zeroLocus ↑I
M : ModuleCat R
inst✝ : Module.Finite R ↑M
smul_lt : I • ⊤ < ⊤
rs : List R
mem : ∀ r ∈ rs, r ∈ I
reg : RingTheory.Sequence.IsRegular (↑M) rs
len : rs.length = 0
⊢ ∀ i < 0, Subsingleton (Ext N M i)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: 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
⊢ (fun n ↦ n.prod fun i k ↦ dp R k (v i)) 0 = 1

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: case dp.mem.zero
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) = ⊤
m : M
x : DividedPowerAlgebra R M
k : ℕ
i : ι
⊢ 0 * dp R k (v i) ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: case dp.mem.mem
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) = ⊤
m : M
x : DividedPowerAlgebra R M
k : ℕ
i : ι
n : ι →₀ ℕ
⊢ (dp R ((Finsupp.single i k + n) i) (v i) * (Finsupp.erase i (Finsupp.single i k + n)).prod fun i k ↦ dp R k (v i)) =
    dp R (k + n i) (v i) * (Finsupp.erase i n).prod fun i k ↦ dp R k (v i)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: case dp.add
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) = ⊤
m✝ m n : M
hm_mem : m ∈ Submodule.span R (Set.range v)
hn_mem : n ∈ Submodule.span R (Set.range v)
hm :
  ∀ (x : DividedPowerAlgebra R M) (k : ℕ),
    x ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i)) →
      x * dp R k m ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
hn :
  ∀ (x : DividedPowerAlgebra R M) (k : ℕ),
    x ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i)) →
      x * dp R k n ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
x : DividedPowerAlgebra R M
k : ℕ
hx : x ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
⊢ x * dp R k (m + n) ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))

Tactic:
dp_add,

Goal state after:
case dp.add
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) = ⊤
m✝ m n : M
hm_mem : m ∈ Submodule.span R (Set.range v)
hn_mem : n ∈ Submodule.span R (Set.range v)
hm :
  ∀ (x : DividedPowerAlgebra R M) (k : ℕ),
    x ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i)) →
      x * dp R k m ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
hn :
  ∀ (x : DividedPowerAlgebra R M) (k : ℕ),
    x ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i)) →
      x * dp R k n ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
x : DividedPowerAlgebra R M
k : ℕ
hx : x ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
⊢ x * ∑ k ∈ antidiagonal k, dp R k.1 m * dp R k.2 n ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: R : Type u_4
M : Type u_5
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
m : M
k : ℕ
⊢ dp R n m ^ k = ↑(k • {n}).multinomial * dp R (k * n) m

Tactic:
rw [Multiset.multinomial_nsmul_singleton, ← Fin.prod_const, prod_dp]

Goal state after:
R : Type u_4
M : Type u_5
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
m : M
k : ℕ
⊢ ↑(Nat.multinomial univ fun _i ↦ n) * dp R (∑ _i, n) m = ↑(Nat.multinomial (range k) fun x ↦ n) * dp R (k * n) m
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_4
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
I : Ideal A
hI : DividedPowers I
g : M →ₗ[R] A
hg : ∀ (m : M), g m ∈ I
f : DividedPowerAlgebra R M →ₐ[R] A
hf : ∀ (n : ℕ) (m : M), f (dp R n m) = hI.dpow n (g m)
x✝¹ : ℕ
x✝ : M
⊢ f (dp R x✝¹ x✝) = hI.dpow x✝¹ (g x✝)

Tactic:
hf

Goal state after:
R : Type u_2
M : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_4
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
I : Ideal A
hI : DividedPowers I
g : M →ₗ[R] A
hg : ∀ (m : M), g m ∈ I
f : DividedPowerAlgebra R M →ₐ[R] A
hf : ∀ (n : ℕ) (m : M), f (dp R n m) = hI.dpow n (g m)
x✝¹ : ℕ
x✝ : M
⊢ hI.dpow x✝¹ (g x✝) = hI.dpow x✝¹ (g x✝)
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_4
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
I : Ideal A
hI : DividedPowers I
g : M →ₗ[R] A
hg : ∀ (m : M), g m ∈ I
x✝ : M
⊢ ((lift hI g hg).toLinearMap ∘ₗ embed R M) x✝ = g x✝

Tactic:
simp

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

Goal state before:
pp: A : Type u_3
B : Type u_4
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
S : Set A
hS : I = span S
hS' : ∀ s ∈ S, f s ∈ J
hdp : ∀ {n : ℕ}, ∀ a ∈ S, f (hI.dpow n a) = hJ.dpow n (f a)
h : map f I ≤ J
n✝ : ℕ
a : A
ha : a ∈ I
⊢ hJ.dpow n✝ (f a) = f (hI.dpow n✝ a)

Tactic:
rw [← fromGens_coe hI hJ hS h hdp, (fromGens hI hJ hS h hdp).dpow_comp a ha]

Goal state after:
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
S : Type u_4
inst✝⁵ : CommSemiring S
N : Type u_5
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
inst✝² : Module S N
f : M →ₗ[R] N
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R S N
m : M
⊢ (map S f) ((embed R M) m) = (embed S N) (f m)

Tactic:
simp [embed_def, map_apply_dp]

Goal state after:
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
S : Type u_4
inst✝⁵ : CommSemiring S
N : Type u_5
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
inst✝² : Module S N
f : M →ₗ[R] N
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R S N
x✝ : M
⊢ ((map S f).toLinearMap ∘ₗ embed R M) x✝ = (↑R (embed S N) ∘ₗ f) x✝

Tactic:
simp

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

Goal state before:
pp: A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m : ℕ
hmn : m < n
x y : A
hx : x ∈ I
hy : y ∈ I
k : ℕ × ℕ
hk : k ∈ Finset.antidiagonal m
⊢ m.choose k.1 • (x ^ k.1 * y ^ k.2) =
    ↑m ! * ((if x ∈ I then (↑k.1!)⁻¹ʳ * x ^ k.1 else 0) * if y ∈ I then (↑k.2!)⁻¹ʳ * y ^ k.2 else 0)

Tactic:
if_pos hx,

Goal state after:
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m : ℕ
hmn : m < n
x y : A
hx : x ∈ I
hy : y ∈ I
k : ℕ × ℕ
hk : k ∈ Finset.antidiagonal m
⊢ m.choose k.1 • (x ^ k.1 * y ^ k.2) = ↑m ! * ((↑k.1!)⁻¹ʳ * x ^ k.1 * if y ∈ I then (↑k.2!)⁻¹ʳ * y ^ k.2 else 0)
Module: Mathlib.RingTheory.DividedPowers.Padic

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
f : A →+* B
hf : Injective ⇑f
hJ : DividedPowers J
hIJ : Ideal.map f I = J
hmem : ∀ (n : ℕ) {x : A}, x ∈ I → ∃ y, ∃ (_ : n ≠ 0 → y ∈ I), f y = hJ.dpow n (f x)
n✝ : ℕ
x✝ : A
hx : x✝ ∉ I
⊢ (if hx : x✝ ∈ I then ⋯.choose else 0) = 0

Tactic:
simp [dif_neg hx]

Goal state after:
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
n : ℕ
a : A
⊢ (ofRingEquiv h hI).dpow n (e a) = e (hI.dpow n a)

Tactic:
simp

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

Goal state before:
pp: case neg
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
hnI : I ^ n = 0
m : ℕ
x : A
hx : x ∈ I
y : A
hy : y ∈ I
hmn : n ≤ m
h_sub : I ^ m ≤ I ^ n
hxy : (x + y) ^ m = 0
k : ℕ × ℕ
hk : k ∈ Finset.antidiagonal m
⊢ ((if x ∈ I then (↑k.1!)⁻¹ʳ * x ^ k.1 else 0) * if y ∈ I then (↑k.2!)⁻¹ʳ * y ^ k.2 else 0) = 0

Tactic:
if_pos hx,

Goal state after:
case neg
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
hnI : I ^ n = 0
m : ℕ
x : A
hx : x ∈ I
y : A
hy : y ∈ I
hmn : n ≤ m
h_sub : I ^ m ≤ I ^ n
hxy : (x + y) ^ m = 0
k : ℕ × ℕ
hk : k ∈ Finset.antidiagonal m
⊢ ((↑k.1!)⁻¹ʳ * x ^ k.1 * if y ∈ I then (↑k.2!)⁻¹ʳ * y ^ k.2 else 0) = 0
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : hI.IsSubDPIdeal J
inst✝ : (x : A) → Decidable (x ∈ J)
n✝ : ℕ
x✝ y✝ : A
hx : x✝ ∈ J
hy : y✝ ∈ J
⊢ (if x✝ + y✝ ∈ J then hI.dpow n✝ (x✝ + y✝) else 0) =
    ∑ k ∈ Finset.antidiagonal n✝, (if x✝ ∈ J then hI.dpow k.1 x✝ else 0) * if y✝ ∈ J then hI.dpow k.2 y✝ else 0

Tactic:
if_pos hx,

Goal state after:
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : hI.IsSubDPIdeal J
inst✝ : (x : A) → Decidable (x ∈ J)
n✝ : ℕ
x✝ y✝ : A
hx : x✝ ∈ J
hy : y✝ ∈ J
⊢ (if x✝ + y✝ ∈ J then hI.dpow n✝ (x✝ + y✝) else 0) =
    ∑ x ∈ Finset.antidiagonal n✝, hI.dpow x.1 x✝ * if y✝ ∈ J then hI.dpow x.2 y✝ else 0
Module: Mathlib.RingTheory.DividedPowers.RatAlgebra

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
⊢ hI.dpow n x = ((↑n !)⁻¹ • ↑n !) • hI.dpow n x

Tactic:
← one_smul R (hI.dpow n x)

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
⊢ 1 • hI.dpow n x = ((↑n !)⁻¹ • ↑n !) • hI.dpow n x
Module: Mathlib.RingTheory.DividedPowers.Padic

Goal state before:
pp: case pos
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
h✝ : x ∈ Ideal.span {↑p}
⊢ ↑⟨(↑n !)⁻¹ * ↑x ^ n, ⋯⟩ = (↑n !)⁻¹ * ↑x ^ n

Tactic:
simp

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

Goal state before:
pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
h✝ : x ∉ Ideal.span {↑p}
⊢ ↑0 = 0

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
I : Ideal R
inst✝¹ : DecidablePred fun x ↦ x ∈ I
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
⊢ hI.dpow n x = if x ∈ I then (↑n !)⁻¹ʳ * x ^ n else 0

Tactic:
if_pos hx,

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
I : Ideal R
inst✝¹ : DecidablePred fun x ↦ x ∈ I
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
⊢ hI.dpow n x = (↑n !)⁻¹ʳ * x ^ n
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: case mpr.h2
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
x : TrivSqZeroExt R M
n : ℕ
hn : x.fst ^ n = 0
⊢ 0 • (x ^ n).snd + MulOpposite.op 0 • (x ^ n).snd = snd 0

Tactic:
MulOpposite.op_zero,

Goal state after:
case mpr.h2
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
x : TrivSqZeroExt R M
n : ℕ
hn : x.fst ^ n = 0
⊢ 0 • (x ^ n).snd + 0 • (x ^ n).snd = snd 0
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: case h1
K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
r : K[ε]
hxI : ε * r ∈ I
hx0 : ε * r ≠ 0
⊢ fst (ε * r) = fst (fst r • ε)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: case h2
K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
r : K[ε]
hxI : ε * r ∈ I
hx0 : ε * r ≠ 0
⊢ snd (ε * r) = snd (fst r • ε)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: case refine_2.inr.inr
K : Type u_2
inst✝ : DivisionRing K
hI : Ideal.span {ε} < ⊤
⊢ ⊤ = ⊤

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: K : Type u_2
inst✝ : DivisionRing K
b : K[ε]
a : K[ε]ˣ
⊢ ↑a * (↑a⁻¹ * b) = b ∨ b * (↑a⁻¹ * b) = ↑a

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: K : Type u_2
inst✝ : DivisionRing K
a : K[ε]
ha : IsNilpotent a
b : K[ε]ˣ
⊢ a * (↑b⁻¹ * a) = ↑b ∨ ↑b * (↑b⁻¹ * a) = a

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.TotallySplit

Goal state before:
pp: R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Etale R S
inst✝ : Module.Finite R S
hn : Module.rankAtStalk S = ↑0
e : R ⊗[R] S ≃ₐ[R] S := TensorProduct.lid R S
⊢ IsFiniteSplit R S

Tactic:
rw [Nat.cast_zero, Module.rankAtStalk_eq_zero_iff_subsingleton] at hn

Goal state after:
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Etale R S
inst✝ : Module.Finite R S
hn : Subsingleton S
e : R ⊗[R] S ≃ₐ[R] S := TensorProduct.lid R S
⊢ IsFiniteSplit R S
Module: Mathlib.RingTheory.Etale.Weakly

Goal state before:
pp: case ha
R : Type u₁
S : Type u₂
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u₃
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : WeaklyEtale (ULift.{max u₁ u₂ u₃, u₁} R) (ULift.{max u₁ u₂ u₃, u₂} S)
inst✝ : WeaklyEtale (ULift.{max u₁ u₂ u₃, u₂} S) (ULift.{max u₁ u₂ u₃, u₃} T)
x✝ : ULift.{max u₁ u₂ u₃, u₃} T
⊢ (((TensorProduct.lmul' (ULift.{max (max u₁ u₂) u₃, u₁} R)).comp TensorProduct.includeLeft) x✝).down =
    ((((AlgHom.restrictScalars (ULift.{max u₁ u₂ u₃, u₁} R) (TensorProduct.lmul' (ULift.{max u₁ u₂ u₃, u₂} S))).comp
              (TensorProduct.mapOfCompatibleSMul (ULift.{max u₁ u₂ u₃, u₂} S) (ULift.{max (max u₁ u₂) u₃, u₁} R)
                (ULift.{max u₁ u₂ u₃, u₁} R) (ULift.{max u₁ u₂ u₃, u₃} T) (ULift.{max u₁ u₂ u₃, u₃} T))).comp
          TensorProduct.includeLeft)
        x✝).down

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Etale.Weakly

Goal state before:
pp: case hb
R : Type u₁
S : Type u₂
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u₃
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : WeaklyEtale (ULift.{max u₁ u₂ u₃, u₁} R) (ULift.{max u₁ u₂ u₃, u₂} S)
inst✝ : WeaklyEtale (ULift.{max u₁ u₂ u₃, u₂} S) (ULift.{max u₁ u₂ u₃, u₃} T)
x✝ : ULift.{max u₁ u₂ u₃, u₃} T
⊢ (((AlgHom.restrictScalars (ULift.{max (max u₁ u₂) u₃, u₁} R)
              (TensorProduct.lmul' (ULift.{max (max u₁ u₂) u₃, u₁} R))).comp
          TensorProduct.includeRight)
        x✝).down =
    (((AlgHom.restrictScalars (ULift.{max (max u₁ u₂) u₃, u₁} R)
              ((AlgHom.restrictScalars (ULift.{max u₁ u₂ u₃, u₁} R)
                    (TensorProduct.lmul' (ULift.{max u₁ u₂ u₃, u₂} S))).comp
                (TensorProduct.mapOfCompatibleSMul (ULift.{max u₁ u₂ u₃, u₂} S) (ULift.{max (max u₁ u₂) u₃, u₁} R)
                  (ULift.{max u₁ u₂ u₃, u₁} R) (ULift.{max u₁ u₂ u₃, u₃} T) (ULift.{max u₁ u₂ u₃, u₃} T)))).comp
          TensorProduct.includeRight)
        x✝).down

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Extension.ExtendScalars

Goal state before:
pp: R✝ : Type u
S✝ : Type v
inst✝⁵ : CommRing R✝
inst✝⁴ : CommRing S✝
inst✝³ : Algebra R✝ S✝
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
x✝ : P.Ring
⊢ ((IsScalarTower.toAlgHom R P.Ring S).comp (IsScalarTower.toAlgHom R P.Ring P.Ring)) x✝ =
    ((IsScalarTower.toAlgHom R S S).comp (IsScalarTower.toAlgHom R P.Ring S)) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Etale.Finite

Goal state before:
pp: R : Type u
inst✝⁷ : CommRing R
k : Type u
inst✝⁶ : Field k
Ω : Type w
inst✝⁵ : Field Ω
inst✝⁴ : Algebra R Ω
S : Type w
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra S Ω
inst✝ : IsScalarTower R S Ω
A B : FiniteEtale R
f : A ⟶ B
x✝ : ↑A.obj
⊢ ((AlgHom.restrictScalars R
            (Hom.hom
              (ofHom (Algebra.TensorProduct.map (AlgHom.id R R) (Hom.hom f.hom)) ≫
                  (isoMk (Algebra.TensorProduct.lid R ↑B.obj)).hom).hom)).comp
        Algebra.TensorProduct.includeRight)
      x✝ =
    ((AlgHom.restrictScalars R (Hom.hom ((isoMk (Algebra.TensorProduct.lid R ↑A.obj)).hom ≫ f).hom)).comp
        Algebra.TensorProduct.includeRight)
      x✝

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Frobenius

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
inst✝ : IsDomain S
ζ : S
q : ℕ := Nat.card (R ⧸ Ideal.under R Q)
hζ : ζ ^ 0 = 1
hk' : ↑0 ∉ Q
⊢ ↑0 ∈ Q

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring

Goal state before:
pp: case zero
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : AddMonoid ι
inst✝⁴ : Semiring A
inst✝³ : SetLike σ A
inst✝² : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝¹ : DecidableEq ι
inst✝ : GradedRing 𝒜
s : Set A
h : ∀ (i : ι) ⦃x : A⦄, x ∈ s → ↑(((decompose 𝒜) x) i) ∈ s
x : A
i : ι
⊢ ↑(((decompose 𝒜) 0) i) ∈ Subsemiring.closure s

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.AlgHom

Goal state before:
pp: R : Type u_1
A : Type u_6
ι : Type u_10
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
𝒜 : ι → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : 𝒜 →ₐᵍ[R] 𝒜
n : ℕ
x✝ : A
⊢ (f ^ Nat.zero) x✝ = (⇑f)^[Nat.zero] x✝

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring

Goal state before:
pp: case inl
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : AddMonoid ι
inst✝⁴ : Semiring A
inst✝³ : SetLike σ A
inst✝² : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝¹ : DecidableEq ι
inst✝ : GradedRing 𝒜
s : Set A
h : ∀ x ∈ s, IsHomogeneousElem 𝒜 x
i : ι
hx : 0 ∈ insert 0 s
⊢ ↑(((decompose 𝒜) 0) i) ∈ insert 0 s

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.TensorProduct

Goal state before:
pp: case zero
ι : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
inst✝¹² : DecidableEq ι
inst✝¹¹ : AddMonoid ι
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule S B
inst✝⁴ : GradedAlgebra 𝒜
inst✝³ : GradedAlgebra ℬ
inst✝² : Algebra R S
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R S B
f : 𝒜 →ₐᵍ[R] fun x ↦ Submodule.restrictScalars R (ℬ x)
i✝ : ι
hx : ↑((toBaseChange S (𝒜 i✝)) 0) ∈ baseChange S (𝒜 i✝)
⊢ ((AlgHom.liftEquiv R S A B) ↑f).toRingHom ↑((toBaseChange S (𝒜 i✝)) 0) ∈ ℬ i✝

Tactic:
simp

Goal state after: