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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
a : ↑A
⊢ single 1 a ∈ boundaries₁ A

Tactic:
use single (1, 1) a

Goal state after:
case h
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
a : ↑A
⊢ (ModuleCat.Hom.hom (d₂₁ A)) (single (1, 1) a) = single 1 a
Module: Mathlib.RingTheory.PowerSeries.Ideal

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
P : Ideal R⟦X⟧
inst✝ : P.IsPrime
⊢ spanFinrank P ≤ spanFinrank (Ideal.map constantCoeff P) + 1

Tactic:
by_cases hfg : P.FG

Goal state after:
case pos
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R⟦X⟧
inst✝ : P.IsPrime
hfg : P.FG
⊢ spanFinrank P ≤ spanFinrank (Ideal.map constantCoeff P) + 1

case neg
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R⟦X⟧
inst✝ : P.IsPrime
hfg : ¬P.FG
⊢ spanFinrank P ≤ spanFinrank (Ideal.map constantCoeff P) + 1
Module: Mathlib.RingTheory.AdicCompletion.Topology

Goal state before:
pp: case mp
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
N : ℕ → ℕ
hN : ∀ (i m : ℕ), N i ≤ m → ∀ (n : ℕ), N i ≤ n → u n - u m ∈ I ^ i
L : R
hL : ∀ (n : ℕ), u ((Finset.Iic n).sup N) - L ∈ I ^ n
⊢ ∃ a, Filter.Tendsto u Filter.atTop (𝓝 a)

Tactic:
use L

Goal state after:
case h
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
N : ℕ → ℕ
hN : ∀ (i m : ℕ), N i ≤ m → ∀ (n : ℕ), N i ≤ n → u n - u m ∈ I ^ i
L : R
hL : ∀ (n : ℕ), u ((Finset.Iic n).sup N) - L ∈ I ^ n
⊢ Filter.Tendsto u Filter.atTop (𝓝 L)
Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology

Goal state before:
pp: case mpr.h
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
⊢ 𝓝 0 = 𝓝 0

Tactic:
· ext s
      let := Ideal.adic_basis J
      rw [J.hasBasis_nhds_zero_adic.mem_iff]
      constructor <;> intro H
      · rcases H₂ s H with ⟨n, h⟩
        exact ⟨n, trivial, h⟩
      · rcases H with ⟨n, -, hn⟩
        rw [mem_nhds_iff]
        exact ⟨_, hn, H₁ n, (J ^ n).zero_mem⟩

Goal state after:
Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology

Goal state before:
pp: case mpr.right
A : Type u_2
inst✝² : CommRing A
inst✝¹ : TopologicalSpace A
inst✝ : IsTopologicalRing A
a✝ : DiscreteTopology A
⊢ ∀ s ∈ 𝓝 0, ∃ n, ↑(⊥ ^ n) ⊆ s

Tactic:
intro U U_nhds

Goal state after:
case mpr.right
A : Type u_2
inst✝² : CommRing A
inst✝¹ : TopologicalSpace A
inst✝ : IsTopologicalRing A
a✝ : DiscreteTopology A
U : Set A
U_nhds : U ∈ 𝓝 0
⊢ ∃ n, ↑(⊥ ^ n) ⊆ U
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

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

Tactic:
coeff_one,

Goal state after:
case pos
R : Type u_2
inst✝ : CommSemiring R
n k : ℕ
x : Fin n →₀ ℕ
h1 : ¬(x = 0 ∧ k = 1)
h3 : k = 1
⊢ 0 = if x = 0 then 1 else 0
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 • ⊤)
⊢ ↑((ofPowSMul I M a) x) c = (powSMulQuotInclusion I M h ⊤) (↑x b)

Tactic:
← x.prop (show b ≤ c by lia),

Goal state after:
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 • ⊤)
⊢ ↑((ofPowSMul I M a) x) c = (powSMulQuotInclusion I M h ⊤) ((transitionMap I ↥(I ^ a • ⊤) ⋯) (↑x c))
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: σ✝ : Type u_1
R✝ : Type u_2
n : ℕ
inst✝³ : CommRing R✝
inst✝² : Finite σ✝
σ : Type u_3
R : Type u_4
inst✝¹ : Finite σ
inst✝ : CommRing R
x✝ : MvPowerSeries σ R
n✝ : σ →₀ ℕ
⊢ (coeff n✝) (toAdicCompletionInv σ R ((↑↑(toAdicCompletion σ R).toRingHom).toFun x✝)) = (coeff n✝) x✝

Tactic:
simp [coeff_toAdicCompletionInv, coeff_toAdicCompletion_val_apply_out]

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
h : I.FG
x : ℕ → AdicCompletion I M
hx : ∀ {m n : ℕ}, m ≤ n → x m ≡ x n [SMOD I ^ m • ⊤]
L : AdicCompletion I M := ⟨fun i ↦ ↑(x i) i, ⋯⟩
⊢ ∃ L, ∀ (n : ℕ), x n ≡ L [SMOD I ^ n • ⊤]

Tactic:
use L

Goal state after:
case h
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : I.FG
x : ℕ → AdicCompletion I M
hx : ∀ {m n : ℕ}, m ≤ n → x m ≡ x n [SMOD I ^ m • ⊤]
L : AdicCompletion I M := ⋯
⊢ ∀ (n : ℕ), x n ≡ L [SMOD I ^ n • ⊤]
Module: Mathlib.RingTheory.Congruence.Star

Goal state before:
pp: R : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : StarRing R
r : R → R → Prop
hr : ∀ (a b : R), r a b → r (Star.star a) (Star.star b)
a b w✝ x✝ y✝ z✝ : R
h1 : Rel r w✝ x✝
h2 : Rel r y✝ z✝
⊢ Rel r (Star.star y✝ * Star.star w✝) (Star.star z✝ * Star.star x✝)

Tactic:
exact (h2.star hr).mul (h1.star hr)

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ p.contentIdeal = ⊥ ↔ p = 0

Tactic:
simp only [contentIdeal_def, span_eq_bot]
  refine ⟨?_, fun h ↦ by simp [h]⟩
  contrapose!
  exact fun h ↦ ⟨p.leadingCoeff, coeff_mem_coeffs (leadingCoeff_ne_zero.mpr h),
    leadingCoeff_ne_zero.mpr h⟩

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

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
b : NNReal
hb : 1 < b
p : R[X]
hp0 : ¬p = 0
⊢ gaussNorm (v.intAdicAbv hb) 1 p < 1 ↔ p.contentIdeal ≤ v.asIdeal

Tactic:
have hsupp_nonempty : p.support.Nonempty := by grind [support_nonempty]

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
b : NNReal
hb : 1 < b
p : R[X]
hp0 : ¬p = 0
hsupp_nonempty : p.support.Nonempty
⊢ gaussNorm (v.intAdicAbv hb) 1 p < 1 ↔ p.contentIdeal ≤ v.asIdeal
Module: Mathlib.RingTheory.DedekindDomain.GaussLemma

Goal state before:
pp: case neg.mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
b : NNReal
hb : 1 < b
p : R[X]
hp0 : ¬p = 0
hsupp_nonempty : p.support.Nonempty
⊢ (p.support.sup' ⋯ fun x ↦ (v.intAdicAbv hb) (p.coeff x)) < 1 → ∀ x ∈ p.coeffs, (v.intAdicAbv hb) x < 1

pp: case neg.mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
b : NNReal
hb : 1 < b
p : R[X]
hp0 : ¬p = 0
hsupp_nonempty : p.support.Nonempty
⊢ (∀ x ∈ p.coeffs, (v.intAdicAbv hb) x < 1) → (p.support.sup' ⋯ fun x ↦ (v.intAdicAbv hb) (p.coeff x)) < 1

Tactic:
· contrapose!
    simp only [mem_coeffs_iff, mem_support_iff, ↓existsAndEq, and_true, forall_exists_index,
      and_imp]
    intro _ h1 h2
    exact Finset.le_sup'_of_le (fun n ↦ (v.intAdicAbv hb) (p.coeff n)) (by simp [h1]) h2

Goal state after:
case neg.mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
b : NNReal
hb : 1 < b
p : R[X]
hp0 : ¬p = 0
hsupp_nonempty : p.support.Nonempty
⊢ (∀ x ∈ p.coeffs, (v.intAdicAbv hb) x < 1) → (p.support.sup' ⋯ fun x ↦ (v.intAdicAbv hb) (p.coeff x)) < 1
Module: Mathlib.RingTheory.Bialgebra.MonoidAlgebra

Goal state before:
pp: R : Type u_1
A : Type u_3
M : Type u_8
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Bialgebra R A
inst✝ : AddMonoid M
m : M
a : A
⊢ (toMultiplicativeBialgEquiv R A M) (single m a) = MonoidAlgebra.single (Multiplicative.ofAdd m) a

Tactic:
by
  simp [toMultiplicativeBialgEquiv]

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

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
a : A
ha : a ∉ ⊥
⊢ (if a = 0 ∧ n = 0 then 1 else 0) = 0

Tactic:
by
    simp only [mem_bot] at ha
    rw [if_neg]
    exact not_and_of_not_left (n = 0) ha

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

Goal state before:
pp: case pos
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
x✝¹ x✝ : A
hx : x✝ ∈ ⊥
hn : n = 0
⊢ (if n = 0 then 1 else 0) = if n = 0 then x✝¹ ^ n else 0

Tactic:
if_pos hn,

Goal state after:
case pos
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
x✝¹ x✝ : A
hx : x✝ ∈ ⊥
hn : n = 0
⊢ 1 = if n = 0 then x✝¹ ^ n else 0
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
a : A
n : ℕ
hn : n ≠ 0
hnI : ∀ {y : A}, y ∈ I → n • y = 0
hI : DividedPowers I
ha : a ∈ I
h_fac : ↑n ! * hI.dpow n a = n • ↑(n - 1)! * hI.dpow n a
⊢ ↑n ! * hI.dpow n a = 0

Tactic:
h_fac,

Goal state after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
a : A
n : ℕ
hn : n ≠ 0
hnI : ∀ {y : A}, y ∈ I → n • y = 0
hI : DividedPowers I
ha : a ∈ I
h_fac : ↑n ! * hI.dpow n a = n • ↑(n - 1)! * hI.dpow n a
⊢ n • ↑(n - 1)! * hI.dpow n a = 0
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: case inl
R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
hn : n = 0
⊢ dp R n 0 = if n = 0 then 1 else 0

Tactic:
if_pos hn,

Goal state after:
case inl
R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
hn : n = 0
⊢ dp R n 0 = 1
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: case insert
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
⊢ dpow n ((insert a s).sum x) = ∑ k ∈ (insert a s).sym n, ∏ i ∈ insert a s, dpow (Multiset.count i ↑k) (x i)

Tactic:
sum_insert ha,

Goal state after:
case insert
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
⊢ dpow n (x a + ∑ x_1 ∈ s, x x_1) = ∑ k ∈ (insert a s).sym n, ∏ i ∈ insert a s, dpow (Multiset.count i ↑k) (x i)
Module: Mathlib.RingTheory.Depth.Rees

Goal state before:
pp: 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
n : ℕ
ih :
  ∀ (M : ModuleCat R) [Module.Finite R ↑M],
    I • ⊤ < ⊤ →
      ∀ (rs : List R),
        (∀ r ∈ rs, r ∈ I) → RingTheory.Sequence.IsRegular (↑M) rs → rs.length = n → ∀ i < n, Subsingleton (Ext N M i)
M : ModuleCat R
inst✝ : Module.Finite R ↑M
smul_lt : I • ⊤ < ⊤
rs : List R
i✝ : ℕ
le_rad : I ≤ (Module.annihilator R ↑N).radical
a : R
rs' : List R
k : ℕ
hk : a ^ k ∈ Module.annihilator R ↑N
reg : IsSMulRegular (↑M) a ∧ RingTheory.Sequence.IsRegular (QuotSMulTop a ↑M) rs'
mem : a ∈ I ∧ ∀ a ∈ rs', a ∈ I
len : rs'.length = n
i : ℕ
hi : i + 1 < n + 1
g : AddCommGrpCat.of (Ext N (M.smulShortComplex a).X₁ (i + 1)) ⟶
  AddCommGrpCat.of (Ext N (M.smulShortComplex a).X₂ (i + 1)) :=
  AddCommGrpCat.ofHom ((Ext.mk₀ (M.smulShortComplex a).f).postcomp N ⋯)
mono_g : Mono (AddCommGrpCat.ofHom ((Ext.mk₀ (a • 𝟙 M)).postcomp N ⋯))
gk : AddCommGrpCat.of (Ext N (M.smulShortComplex (a ^ k)).X₁ (i + 1)) ⟶
  AddCommGrpCat.of (Ext N (M.smulShortComplex (a ^ k)).X₂ (i + 1)) :=
  AddCommGrpCat.ofHom ((Ext.mk₀ (M.smulShortComplex (a ^ k)).f).postcomp N ⋯)
⊢ Mono (AddCommGrpCat.ofHom ((Ext.mk₀ (a ^ k • 𝟙 M)).postcomp N ⋯))

Tactic:
exact (Ext.postcomp_smul_id_mono_iff (a ^ k) (i + 1)).mpr <|
            ((Ext.postcomp_smul_id_mono_iff a (i + 1)).mp mono_g).pow k

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
ι : Type u_3
r : ι → A
n : ℕ
a : ι
s : Finset ι
has : a ∉ s
hrec : s.Nonempty → (∀ i ∈ s, r i ∈ I) → hI.dpow n (∏ i ∈ s, r i) = n ! ^ (#s - 1) • ∏ i ∈ s, hI.dpow n (r i)
hs : (insert a s).Nonempty
hs' : ∀ i ∈ insert a s, r i ∈ I
h : s.Nonempty
this : #s = #s - 1 + 1
⊢ r a ^ n * ↑n ! ^ (#s - 1) = ↑n ! ^ #s * hI.dpow n (r a)

Tactic:
nth_rewrite 2 [this]

Goal state after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_3
r : ι → A
n : ℕ
a : ι
s : Finset ι
has : a ∉ s
hrec : s.Nonempty → (∀ i ∈ s, r i ∈ I) → hI.dpow n (∏ i ∈ s, r i) = n ! ^ (#s - 1) • ∏ i ∈ s, hI.dpow n (r i)
hs : (insert a s).Nonempty
hs' : ∀ i ∈ insert a s, r i ∈ I
h : s.Nonempty
this : #s = #s - 1 + 1
⊢ r a ^ n * ↑n ! ^ (#s - 1) = ↑n ! ^ (#s - 1 + 1) * hI.dpow n (r a)
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
m : ℕ
x : A
hx : x ∉ I
⊢ dpow I m x = 0

Tactic:
by simp [dpow, hx]

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
x : A
hx : x ∈ I
⊢ dpow I 0 x = 1

Tactic:
by simp [dpow, 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✝ : ℕ
x✝ y✝ : B
hx : x✝ ∈ J
hy : y✝ ∈ J
⊢ e (hI.dpow n✝ (e.symm (x✝ + y✝))) = ∑ k ∈ antidiagonal n✝, e (hI.dpow k.1 (e.symm x✝)) * e (hI.dpow k.2 (e.symm y✝))

Tactic:
by
    simp only [map_add]
    rw [hI.dpow_add (symm_apply_mem_of_equiv_iff.mpr (h ▸ hx))
        (symm_apply_mem_of_equiv_iff.mpr (h ▸ hy))]
    simp only [map_sum, map_mul]

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)!
hnI : I ^ n = 0
m : ℕ
x : A
hx : x ∈ I
y : A
hy : y ∈ I
hmn : n ≤ m
h_sub : I ^ m ≤ I ^ n
⊢ (x + y) ^ m = 0

Tactic:
rw [← Ideal.mem_bot, ← Ideal.zero_eq_bot, ← hnI]

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)!
hnI : I ^ n = 0
m : ℕ
x : A
hx : x ∈ I
y : A
hy : y ∈ I
hmn : n ≤ m
h_sub : I ^ m ≤ I ^ n
⊢ (x + y) ^ m ∈ I ^ n
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
⊢ y ^ k.2 * x ^ k.1 = 0

Tactic:
rw [← Ideal.mem_bot, ← Ideal.zero_eq_bot, ← hnI]

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
⊢ y ^ k.2 * x ^ k.1 ∈ I ^ n
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
m : ℕ
a x : A
hx : x ∈ I
⊢ (↑m !)⁻¹ʳ * a ^ m * x ^ m = a ^ m * ((↑m !)⁻¹ʳ * x ^ m)

Tactic:
mul_comm _ (a ^ m),

Goal state after:
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
m : ℕ
a x : A
hx : x ∈ I
⊢ a ^ m * (↑m !)⁻¹ʳ * x ^ m = a ^ m * ((↑m !)⁻¹ʳ * x ^ m)
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 k : ℕ
hk : k ≠ 0
hkm : m * k < n
x : A
hx : x ∈ I
hmn : m < n
hm0 : ¬m = 0
hkn : k < n
⊢ ↑(m * k)! = ↑k ! ^ m * (↑m ! * ↑(m.uniformBell k))

Tactic:
← uniformBell_mul_eq _ hk

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 k : ℕ
hk : k ≠ 0
hkm : m * k < n
x : A
hx : x ∈ I
hmn : m < n
hm0 : ¬m = 0
hkn : k < n
⊢ ↑(m.uniformBell k * k ! ^ m * m !) = ↑k ! ^ m * (↑m ! * ↑(m.uniformBell k))
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 k : ℕ
hk : k ≠ 0
hkm : m * k < n
x : A
hx : x ∈ I
⊢ dpow I m (dpow I k x) = ↑(m.uniformBell k) * dpow I (m * k) x

Tactic:
have hmn : m < n := lt_of_le_of_lt (Nat.le_mul_of_pos_right _ (Nat.pos_of_ne_zero hk)) hkm
  rw [dpow_eq_of_mem (m := m * k) hx, dpow_eq_of_mem (dpow_mem hk hx)]
  by_cases hm0 : m = 0
  · simp only [hm0, zero_mul, _root_.pow_zero, mul_one, uniformBell_zero_left, cast_one, one_mul]
  · have hkn : k < n := lt_of_le_of_lt (Nat.le_mul_of_pos_left _ (Nat.pos_of_ne_zero hm0)) hkm
    rw [dpow_eq_of_mem hx, mul_pow, ← pow_mul, mul_comm k, ← mul_assoc, ← mul_assoc]
    apply congr_arg₂ _ _ rfl
    rw [eq_mul_inverse_iff_mul_eq _ _ _ (hn_fac.natCast_factorial_of_lt hkm),
      mul_assoc, inverse_mul_eq_iff_eq_mul _ _ _ (hn_fac.natCast_factorial_of_lt hmn),
      inverse_pow_mul_eq_iff_eq_mul _ _ (hn_fac.natCast_factorial_of_lt hkn),
      ← uniformBell_mul_eq _ hk]
    push_cast
    ring_nf

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

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
⊢ (if hx : x ∈ Ideal.span {↑p} then ⋯.choose else 0) = if hx : x ∈ Ideal.span {↑p} then ⟨dpow' p n ↑x, ⋯⟩ else 0
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
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherian R M
rs rs' : List R
h1 : IsRegular M rs
h2 : rs ~ rs'
⊢ IsRegular M rs'

Tactic:
obtain ⟨h3, h4⟩ := h1

Goal state after:
R : Type u_1
M : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherian R M
rs rs' : List R
h2 : rs ~ rs'
h3 : IsWeaklyRegular M rs
h4 : ⊤ ≠ Ideal.ofList rs • ⊤
⊢ IsRegular M rs'
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
x✝ : ℕ
hn : x✝ ≠ 0
x : A
hx : x ∈ ⊥
⊢ hI.dpow x✝ x ∈ ⊥

Tactic:
mem_bot.mp hx,

Goal state after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
x✝ : ℕ
hn : x✝ ≠ 0
x : A
hx : x ∈ ⊥
⊢ hI.dpow x✝ 0 ∈ ⊥
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
x : R ⧸ Ideal.under R Q
⊢ (↑↑(Ideal.quotientMap Q ↑φ ⋯)).toFun ((algebraMap (R ⧸ Ideal.under R Q) (S ⧸ Q)) x) =
    (algebraMap (R ⧸ Ideal.under R Q) (S ⧸ Q)) x

Tactic:
obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x

Goal state after:
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
x : R
⊢ (↑↑(Ideal.quotientMap Q ↑φ ⋯)).toFun
      ((algebraMap (R ⧸ Ideal.under R Q) (S ⧸ Q)) ((Ideal.Quotient.mk (Ideal.under R Q)) x)) =
    (algebraMap (R ⧸ Ideal.under R Q) (S ⧸ Q)) ((Ideal.Quotient.mk (Ideal.under R Q)) x)
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
x : S ⧸ Q
⊢ H.restrict x = x ^ Nat.card (R ⧸ Ideal.under R Q)

Tactic:
obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x

Goal state after:
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
x : S
⊢ H.restrict ((Ideal.Quotient.mk Q) x) = (Ideal.Quotient.mk Q) x ^ Nat.card (R ⧸ Ideal.under R Q)
Module: Mathlib.RingTheory.HahnSeries.HEval

Goal state before:
pp: Γ : Type u_1
R : Type u_3
V : Type u_4
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : LinearOrder Γ
inst✝³ : IsOrderedCancelAddMonoid Γ
inst✝² : CommRing R
inst✝¹ : CommRing V
inst✝ : Algebra R V
f : PowerSeries R
g : Γ
hg : ¬g = 0
n : ℕ
⊢ ((powerSeriesFamily 0 f) n).coeff g = 0

Tactic:
by_cases hn : n = 0 <;> simp [hg, hn]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
this : Invertible ((PowerSeries.coeff 1) F.Xzero)
aux₀ : PowerSeries.HasSubst F.Xzero
⊢ F.Xzero = PowerSeries.subst F.Xzero PowerSeries.X

Tactic:
PowerSeries.subst_X aux₀,

Goal state after:
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
this : Invertible ((PowerSeries.coeff 1) F.Xzero)
aux₀ : PowerSeries.HasSubst F.Xzero
⊢ F.Xzero = F.Xzero
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
this : Invertible ((PowerSeries.coeff 1) F.zeroX)
aux₀ : PowerSeries.HasSubst F.zeroX
⊢ F.zeroX = PowerSeries.subst F.zeroX PowerSeries.X

Tactic:
PowerSeries.subst_X aux₀,

Goal state after:
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
this : Invertible ((PowerSeries.coeff 1) F.zeroX)
aux₀ : PowerSeries.HasSubst F.zeroX
⊢ F.zeroX = F.zeroX
Module: Mathlib.RingTheory.HahnSeries.PowerSeries

Goal state before:
pp: case pos
Γ : Type u_1
R : Type u_2
inst✝³ : Semiring R
inst✝² : Semiring Γ
inst✝¹ : PartialOrder Γ
inst✝ : IsStrictOrderedRing Γ
r : R
n : Γ
hn : n = 0
⊢ (embDomain Nat.castOrderEmbedding (toPowerSeries.symm (PowerSeries.C r))).coeff n = r

Tactic:
subst hn

Goal state after:
case pos
Γ : Type u_1
R : Type u_2
inst✝³ : Semiring R
inst✝² : Semiring Γ
inst✝¹ : PartialOrder Γ
inst✝ : IsStrictOrderedRing Γ
r : R
⊢ (embDomain Nat.castOrderEmbedding (toPowerSeries.symm (PowerSeries.C r))).coeff 0 = r
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
s : SummableFamily Γ R α
f : α ↪ β
g : Γ
⊢ {a | (if h : a ∈ Set.range ⇑f then s (Classical.choose h) else 0).coeff g ≠ 0} ⊆
    ⇑f '' Function.support fun a ↦ (s a).coeff g

Tactic:
intro b h
        by_cases hb : b ∈ Set.range f
        · simp only [Ne, Set.mem_ofPred_eq, dif_pos hb] at h
          exact ⟨Classical.choose hb, h, Classical.choose_spec hb⟩
        · simp only [Ne, Set.mem_ofPred_eq, dif_neg hb, coeff_zero, not_true_eq_false] at h

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
⊢ powers 0 = single 0 1

Tactic:
ext n
  rw [powers_of_orderTop_pos (by simp)]
  obtain rfl | ha := eq_or_ne n 0 <;> simp [*]

Goal state after: