mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A✝ : Type u_1
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ hI' : DividedPowers I✝
A : Type u_2
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers (Ideal.map (Ideal.Quotient.mk J) I)
φ : hI.DPMorphism hJ
hφ : φ.toRingHom = Ideal.Quotient.mk J
⊢ J ⊓ I ≤ I

Tactic:
simp only [inf_le_right]

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

Goal state before:
pp: ι : 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
i : ι
x : A
hx : x ∈ Subsemiring.closure s
⊢ ↑(((decompose 𝒜) x) i) ∈ Subsemiring.closure s

Tactic:
induction hx using Subsemiring.closure_induction generalizing i with
  | mem _ hx => exact Subsemiring.subset_closure <| h i hx
  | zero => simp
  | one =>
    rw [decompose_one, one_def]
    obtain rfl | h := eq_or_ne i 0 <;> simp [of_eq_of_ne, *]
  | add _ _ _ _ h₁ h₂ => simpa using add_mem (h₁ i) (h₂ i)
  | mul x y _ _ h₁ h₂ =>
    classical
    rw [decompose_mul, DirectSum.mul_eq_dfinsuppSum]
    rw [DFinsupp.sum_apply, DFinsupp.sum, AddSubmonoidClass.coe_finsetSum]
    refine sum_mem fun j _ ↦ ?_
    rw [DFinsupp.sum_apply, DFinsupp.sum, AddSubmonoidClass.coe_finsetSum]
    refine sum_mem fun k _ ↦ ?_
    obtain rfl | h := eq_or_ne i (j + k) <;> simp [of_eq_of_ne, mul_mem, *]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
σ : Type u_3
F : FormalGroup R
inst✝ : F.IsComm
f g : MvPowerSeries σ R
hf : PowerSeries.HasSubst f
hg : PowerSeries.HasSubst g
⊢ ∀ (s : Fin (Nat.succ 0).succ), IsNilpotent (constantCoeff (![f, g] s))

Tactic:
simp [hf, hg]

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.Binomial

Goal state before:
pp: A : Type u_2
inst✝ : CommRing A
d n : ℕ
⊢ ↑↑(↑n).negOnePow * (coeff n) ↑(invOneSubPow A d) = Ring.choose (-↑d) n • 1

Tactic:
← zsmul_eq_mul

Goal state after:
A : Type u_2
inst✝ : CommRing A
d n : ℕ
⊢ ↑(↑n).negOnePow • (coeff n) ↑(invOneSubPow A d) = Ring.choose (-↑d) n • 1
Module: Mathlib.RingTheory.HahnSeries.Binomial

Goal state before:
pp: case neg
Γ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : LinearOrder Γ
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : IsOrderedCancelAddMonoid Γ
inst✝³ : CommRing R
inst✝² : BinomialRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : A⟦Γ⟧
hx : 0 < (x - 1).orderTop
r : R
n : ℕ
g : Γ
hg : g ∈ ((binomialFamily x r) n).support
hn : ¬n = 0
⊢ 0 ≤ g

Tactic:
exact le_of_lt (WithTop.coe_pos.mp (lt_of_lt_of_le (binomialFamily_orderTop_pos hx r
    (Nat.pos_of_ne_zero hn)) (orderTop_le_of_coeff_ne_zero hg)))

Goal state after:
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
f : R[X]
a b : R
ha : Polynomial.eval a f = 0
hb : Polynomial.eval b f = 0
h : ¬IsUnit (a - b)
h' : IsUnit (Polynomial.eval a (derivative f))
c : R
h✝ :
  c * (b - a) ^ 2 + Polynomial.eval a (derivative f) * (b - a) + Polynomial.eval a f = Polynomial.eval (a + (b - a)) f
⊢ a = b

Tactic:
have hc : (c * (b - a) + eval a (derivative f)) * (b - a) = 0 := by grind

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
f : R[X]
a b : R
ha : Polynomial.eval a f = 0
hb : Polynomial.eval b f = 0
h : ¬IsUnit (a - b)
h' : IsUnit (Polynomial.eval a (derivative f))
c : R
h✝ :
  c * (b - a) ^ 2 + Polynomial.eval a (derivative f) * (b - a) + Polynomial.eval a f = Polynomial.eval (a + (b - a)) f
hc : (c * (b - a) + Polynomial.eval a (derivative f)) * (b - a) = 0
⊢ a = b
Module: Mathlib.RingTheory.Ideal.UFD

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : WfDvdMonoid R
x : R
hx : Prime x
p : Ideal R
inst✝³ : p.IsPrime
hxp : x ∉ p
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization.Away x S
this : Disjoint ↑(Submonoid.powers x) ↑p
hpbot : ¬p = ⊥
hi : Function.Injective ⇑(algebraMap R S)
hpb : map (algebraMap R S) p ≠ ⊥
g : S
hg : map (algebraMap R S) p = S ∙ g
hg0 : g ≠ 0
a : R
n : ℤ
hxa : ¬x ∣ a
hag : selfZPow x S n * (algebraMap R S) a = g
hu : IsUnit (selfZPow x S n)
⊢ ∀ (y : R), x * y ∈ p → y ∈ p

Tactic:
by simp [IsPrime.mul_mem_left_iff hxp]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
p : Ideal R[X]
ism : (comap C p).IsMaximal
ne : p ≠ Ideal.map C (comap C p)
q : Ideal R := comap C p
this✝ : Field (R ⧸ q) := Quotient.field q
ne' : Ideal.map (mapRingHom (Ideal.Quotient.mk q)) p ≠ ⊥
y : (R ⧸ q)[X]
mony : y.Monic
hy : Ideal.map (mapRingHom (Ideal.Quotient.mk q)) p = span {y}
this : y ∈ lifts (Ideal.Quotient.mk q)
f : R[X]
hf : map (Ideal.Quotient.mk q) f = y
deg : f.natDegree = y.natDegree
monf : f.Monic
⊢ p = p ⊔ RingHom.ker (mapRingHom (Ideal.Quotient.mk q))

Tactic:
simpa [Polynomial.ker_mapRingHom, q] using Ideal.map_comap_le

Goal state after:
Module: Mathlib.Topology.Algebra.ClopenNhdofOne

Goal state before:
pp: G : Type u_1
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : CompactSpace G
inst✝ : TotallyDisconnectedSpace G
U : Set G
UOpen : IsOpen U
einU : 1 ∈ U
⊢ ∃ H, ↑H ⊆ U

Tactic:
rcases ((Filter.HasBasis.mem_iff' ((nhds_basis_clopen (1 : G))) U).mp <|
    mem_nhds_iff.mpr (by use U)) with ⟨W, hW, h⟩
  rcases IsTopologicalGroup.exist_openNormalSubgroup_sub_clopen_nhds_of_one hW.2 hW.1 with ⟨H, hH⟩
  exact ⟨H, fun _ a ↦ h (hH a)⟩

Goal state after:
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits

Goal state before:
pp: P : ProfiniteGrp.{u}
U : OpenNormalSubgroup ↑P.toProfinite.toTop
⊢ Continuous (⇑(Hom.hom ((limitCone P.diagram).π.app U)) ∘ ⇑(Hom.hom P.toLimit))

Tactic:
fun_prop

Goal state after:
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
t : Finset (Submodule R M)
ht : N.IsMinimalPrimaryDecomposition t
h : ∀ (x : M), (N.colon {x}).radical = {x_1 ∈ t | x ∉ x_1}.inf fun q ↦ (q.colon Set.univ).radical
p : Ideal R
⊢ p ∈ N.associatedPrimes → p ∈ (fun J ↦ (J.colon Set.univ).radical) '' ↑t

Tactic:
rintro ⟨hp, x, rfl⟩

Goal state after:
case mpr
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
t : Finset (Submodule R M)
ht : N.IsMinimalPrimaryDecomposition t
h : ∀ (x : M), (N.colon {x}).radical = {x_1 ∈ t | x ∉ x_1}.inf fun q ↦ (q.colon Set.univ).radical
x : M
hp : (N.colon {x}).radical.IsPrime
⊢ (N.colon {x}).radical ∈ (fun J ↦ (J.colon Set.univ).radical) '' ↑t
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
N : Submodule R M
a : R
b : M
hab : a • b ∈ N
f : ℕ → Submodule R M := fun n ↦ { carrier := {x | a ^ n • x ∈ N}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
hf : Monotone f
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → { toFun := f, monotone' := hf } n = { toFun := f, monotone' := hf } m
h : ∀ ⦃b c : Submodule R M⦄, b ⊓ c = N → b = N ∨ c = N
⊢ b ∈ N ∨ ∃ n, a ^ n • ⊤ ≤ N

Tactic:
specialize @h (f n) (N + a ^ n • ⊤) ?_

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
N : Submodule R M
a : R
b : M
hab : a • b ∈ N
f : ℕ → Submodule R M := fun n ↦ { carrier := {x | a ^ n • x ∈ N}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
hf : Monotone f
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → { toFun := f, monotone' := hf } n = { toFun := f, monotone' := hf } m
h : ∀ ⦃b c : Submodule R M⦄, b ⊓ c = N → b = N ∨ c = N
⊢ f n ⊓ (N + a ^ n • ⊤) = N

R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
N : Submodule R M
a : R
b : M
hab : a • b ∈ N
f : ℕ → Submodule R M := fun n ↦ { carrier := {x | a ^ n • x ∈ N}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
hf : Monotone f
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → { toFun := f, monotone' := hf } n = { toFun := f, monotone' := hf } m
h : f n = N ∨ N + a ^ n • ⊤ = N
⊢ b ∈ N ∨ ∃ n, a ^ n • ⊤ ≤ N
Module: Mathlib.RingTheory.LocalProperties.Injective

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
H : ∀ (I : Ideal R) (x : I.IsMaximal), Injective (Localization.AtPrime I) (LocalizedModule I.primeCompl M)
I : Ideal R
x✝² : FinitePresentation R ↥I := finitePresentation_of_finite R ↥I
m : Ideal R
x✝¹ : m.IsMaximal
Rₘ : Type u := Localization.AtPrime m
Mₘ : Type (max u v) := LocalizedModule m.primeCompl M
f : M →ₗ[R] LocalizedModule m.primeCompl M := LocalizedModule.mkLinearMap m.primeCompl M
h : R →ₗ[R] Rₘ := Algebra.linearMap R Rₘ
Iₘ : Ideal Rₘ := Submodule.localized' Rₘ m.primeCompl h I
g : ↥I →ₗ[R] ↥Iₘ := Submodule.toLocalized' Rₘ m.primeCompl h I
gM : (↥I →ₗ[R] M) →ₗ[R] ↥Iₘ →ₗ[Rₘ] LocalizedModule m.primeCompl M :=
  IsLocalizedModule.mapExtendScalars m.primeCompl g f Rₘ
hM : (R →ₗ[R] M) →ₗ[R] Rₘ →ₗ[Rₘ] LocalizedModule m.primeCompl M :=
  IsLocalizedModule.mapExtendScalars m.primeCompl h f Rₘ
eq'' : ↑R (Submodule.subtype Iₘ) = (IsLocalizedModule.map m.primeCompl g h) (Submodule.subtype I)
l : R →ₗ[R] M
x✝ : ↥I
⊢ (↑R ((↑R (LinearMap.lcomp Rₘ Mₘ (Submodule.subtype Iₘ)) ∘ₗ hM) l) ∘ₗ g) x✝ =
    (↑R (((IsLocalizedModule.map m.primeCompl hM gM) (LinearMap.lcomp R M (Submodule.subtype I)) ∘ₗ hM) l) ∘ₗ g) x✝

Tactic:
simp +zetaDelta [-Algebra.linearMap_apply]

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension

Goal state before:
pp: case zero
R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
S : Submonoid R
this : Small.{v, u} (Localization S)
M : ModuleCat R
inst✝ : HasInjectiveDimensionLE M 0
⊢ HasInjectiveDimensionLE (M.localizedModule S) 0

Tactic:
have injle : HasInjectiveDimensionLE M 0 := ‹_›

Goal state after:
case zero
R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
S : Submonoid R
this : Small.{v, u} (Localization S)
M : ModuleCat R
inst✝ injle : HasInjectiveDimensionLE M 0
⊢ HasInjectiveDimensionLE (M.localizedModule S) 0
Module: Mathlib.RingTheory.LocalRing.Etale

Goal state before:
pp: case mp.refine_1
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalRing S
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R S
inst✝¹ : FaithfulSMul R S
inst✝ : FormallyUnramified R S
β : S
hβ : Function.Surjective ⇑(aeval ((residue S) β))
s : S
a✝ : s ∈ ⊤
q : R[X]
hp : (aeval ((residue S) β)) (map (residue R) q) = (residue S) s
⊢ (aeval β) q ∈ Subalgebra.toSubmodule R[β]

pp: case mp.refine_2
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalRing S
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R S
inst✝¹ : FaithfulSMul R S
inst✝ : FormallyUnramified R S
β : S
hβ : Function.Surjective ⇑(aeval ((residue S) β))
s : S
a✝ : s ∈ ⊤
q : R[X]
hp : (aeval ((residue S) β)) (map (residue R) q) = (residue S) s
⊢ s - (aeval β) q ∈ Submodule.restrictScalars R (Ideal.map (algebraMap R S) (maximalIdeal R))

Tactic:
· rw [adjoin_singleton_eq_range_aeval]; exact ⟨q, rfl⟩

Goal state after:
case mp.refine_2
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalRing S
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R S
inst✝¹ : FaithfulSMul R S
inst✝ : FormallyUnramified R S
β : S
hβ : Function.Surjective ⇑(aeval ((residue S) β))
s : S
a✝ : s ∈ ⊤
q : R[X]
hp : (aeval ((residue S) β)) (map (residue R) q) = (residue S) s
⊢ s - (aeval β) q ∈ Submodule.restrictScalars R (Ideal.map (algebraMap R S) (maximalIdeal R))
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
n D : ℤ
f : K⸨X⸩
H : Valued.v f ≤ exp (-D)
⊢ n < D → f.coeff n = 0

Tactic:
by
  intro hnd
  by_cases! h_n_ord : n < f.order
  · exact coeff_eq_zero_of_lt_order h_n_ord
  set F := powerSeriesPart f with hF
  by_cases! ord_nonpos : f.order ≤ 0
  · obtain ⟨s, hs⟩ := Int.exists_eq_neg_ofNat ord_nonpos
    obtain ⟨m, hm⟩ := Int.eq_ofNat_of_zero_le (neg_le_iff_add_nonneg.mp (hs ▸ h_n_ord))
    obtain ⟨d, hd⟩ := Int.eq_ofNat_of_zero_le (a := D + s) (by lia)
    rw [eq_add_neg_of_add_eq hm, add_comm, ← hs, ← powerSeriesPart_coeff]
    apply (intValuation_le_iff_coeff_lt_eq_zero K F).mp _ m (by linarith)
    rw [hF, ofPowerSeries_powerSeriesPart f, hs, neg_neg, ← hd, neg_add_rev, exp_add, map_mul,
      ← ofPowerSeries_X_pow s, PowerSeries.coe_pow, valuation_X_pow K s]
    gcongr
  · obtain ⟨s, hs⟩ := Int.exists_eq_neg_ofNat (Int.neg_nonpos_of_nonneg (le_of_lt ord_nonpos))
    obtain ⟨m, hm⟩ := Int.eq_ofNat_of_zero_le (a := n - s) (by grind)
    obtain ⟨d, hd⟩ := Int.eq_ofNat_of_zero_le (a := D - s) (by lia)
    rw [sub_eq_iff_eq_add.mp hm, add_comm, ← neg_neg (s : ℤ), ← hs, neg_neg,
      ← powerSeriesPart_coeff]
    apply (intValuation_le_iff_coeff_lt_eq_zero K F).mp _ m (by linarith)
    rw [hF, ofPowerSeries_powerSeriesPart f, map_mul, ← hd, hs, neg_sub, sub_eq_add_neg,
      exp_add, valuation_single_zpow, neg_neg]
    gcongr

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
f : K⸨X⸩
⊢ Valued.v f ≤ 1 ↔ ∃ F, (ofPowerSeries ℤ K) F = f

Tactic:
valuation_le_iff_coeff_lt_log_eq_zero _ one_ne_zero,

Goal state after:
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
⊢ (∀ n < -log 1, f.coeff n = 0) ↔ ∃ F, (ofPowerSeries ℤ K) F = f
Module: Mathlib.RingTheory.MvPolynomial.Expand

Goal state before:
pp: case succ
σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
f : MvPolynomial σ R
k : ℕ
n_ih : (map (iterateFrobenius R p k)) ((expand (p ^ k)) f) = f ^ p ^ k
⊢ (map (frobenius R p)) ((expand p) ((map (iterateFrobenius R p k)) ((expand (p ^ k)) f))) =
    (map (iterateFrobenius R p 1)) ((map (iterateFrobenius R p k)) ((expand (p * p ^ k)) f))

Tactic:
← map_expand,

Goal state after:
case succ
σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
f : MvPolynomial σ R
k : ℕ
n_ih : (map (iterateFrobenius R p k)) ((expand (p ^ k)) f) = f ^ p ^ k
⊢ (map (frobenius R p)) ((map (iterateFrobenius R p k)) ((expand p) ((expand (p ^ k)) f))) =
    (map (iterateFrobenius R p 1)) ((map (iterateFrobenius R p k)) ((expand (p * p ^ k)) f))
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
D : ℤ
φ : ℤ → Set K⸨X⸩ := fun d ↦ {f | coeff hℱ d = f.coeff d}
intersec₁ : ⋂ n ∈ Set.Iio D, φ n ⊆ {x | ∀ d < D, coeff hℱ d = x.coeff d}
ℓ : ℤ := ⋯.choose
N : ℤ := max ℓ D
intersec₂ : ⋂ n ∈ Set.Iio D, φ n ⊇ (⋂ n ∈ Set.Iio ℓ, φ n) ∩ ⋂ n ∈ Set.Icc ℓ N, φ n
this : {x | ∀ d < ⋯.choose, coeff hℱ d = x.coeff d} ∈ ℱ
x✝ : K⸨X⸩
⊢ x✝ ∈ ⋂ n, ⋂ (_ : n < ℓ), φ n ↔ x✝ ∈ {x | ∀ d < ⋯.choose, coeff hℱ d = x.coeff d}

Tactic:
simp only [Set.mem_iInter, Set.mem_ofPred_eq]

Goal state after:
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
D : ℤ
φ : ℤ → Set K⸨X⸩ := fun d ↦ {f | coeff hℱ d = f.coeff d}
intersec₁ : ⋂ n ∈ Set.Iio D, φ n ⊆ {x | ∀ d < D, coeff hℱ d = x.coeff d}
ℓ : ℤ := ⋯.choose
N : ℤ := max ℓ D
intersec₂ : ⋂ n ∈ Set.Iio D, φ n ⊇ (⋂ n ∈ Set.Iio ℓ, φ n) ∩ ⋂ n ∈ Set.Icc ℓ N, φ n
this : {x | ∀ d < ⋯.choose, coeff hℱ d = x.coeff d} ∈ ℱ
x✝ : K⸨X⸩
⊢ (∀ i < ℓ, x✝ ∈ φ i) ↔ ∀ d < ⋯.choose, coeff hℱ d = x✝.coeff d
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: i n m : ℕ
hin : i < n
him : i + 1 < m
t : Fin n → ℕ
⊢ (accumulate n m) t ⟨i, ⋯⟩ = t ⟨i, hin⟩ + (accumulate n m) t ⟨i + 1, him⟩

Tactic:
simp_rw [accumulate_apply]
  convert! (add_sum_erase _ _ _).symm
  · ext
    rw [mem_erase]
    simp_rw [mem_filter_univ, i.succ_le_iff, lt_iff_le_and_ne]
    rw [and_comm, ne_comm, ← Fin.val_ne_iff]
  · exact mem_filter.2 ⟨mem_univ _, le_rfl⟩

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic

Goal state before:
pp: case h
n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : MvPolynomial n R
nontrivial : f.support.Nontrivial
d : n →₀ ℕ
hd : d ∈ f.support
i : n
hdi : d i = 1
disjoint : (↑f.support).PairwiseDisjoint Finsupp.support
isPrimitive : ∀ (r : R), (∀ (d : n →₀ ℕ), r ∣ coeff d f) → IsUnit r
hfd : coeff d f ≠ 0
d₀ : n →₀ ℕ := Finsupp.erase i d
φ : MvPolynomial n R := (monomial d₀) (coeff d f)
ψ : MvPolynomial n R := f - φ * X i
hf : f = φ * X i + ψ
hφ : φ * X i = (monomial d) (coeff d f)
hdψ : ∀ (k : n →₀ ℕ), coeff k ψ = if d = k then 0 else coeff k f
p : MvPolynomial n R
hpφ : p ∣ φ
q : MvPolynomial n R
hq : ψ = p * q
⊢ IsUnit p

Tactic:
obtain ⟨m, b, hm, hb, rfl⟩ := (dvd_monomial_iff_exists hfd).mp hpφ

Goal state after:
case h
n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : MvPolynomial n R
nontrivial : f.support.Nontrivial
d : n →₀ ℕ
hd : d ∈ f.support
i : n
hdi : d i = 1
disjoint : (↑f.support).PairwiseDisjoint Finsupp.support
isPrimitive : ∀ (r : R), (∀ (d : n →₀ ℕ), r ∣ coeff d f) → IsUnit r
hfd : coeff d f ≠ 0
d₀ : n →₀ ℕ := Finsupp.erase i d
φ : MvPolynomial n R := (monomial d₀) (coeff d f)
ψ : MvPolynomial n R := f - φ * X i
hf : f = φ * X i + ψ
hφ : φ * X i = (monomial d) (coeff d f)
hdψ : ∀ (k : n →₀ ℕ), coeff k ψ = if d = k then 0 else coeff k f
q : MvPolynomial n R
m : n →₀ ℕ
b : R
hm : m ≤ d₀
hb : b ∣ coeff d f
hpφ : (monomial m) b ∣ φ
hq : ψ = (monomial m) b * q
⊢ IsUnit ((monomial m) b)
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
U : Set K⸨X⸩
hU : U ∈ 𝓝 (limit hℱ)
⊢ ∀ᶠ (f : K⸨X⸩) in ℱ, f ∈ U

Tactic:
by
  obtain ⟨γ, hU₁⟩ := Valued.mem_nhds.mp hU
  suffices ∀ᶠ f in ℱ, f ∈ {y : K⸨X⸩ | Valued.v (y - limit hℱ) < embedding γ.1} by
    simp_rw [← Valued.v.restrict_lt_iff_lt_embedding] at this
    apply this.mono fun _ hf ↦ hU₁ hf
  set D := -(log (embedding γ.1) - 1) with hD₀
  have hD : exp (-D) < embedding γ.1 := by
    rw [← lt_log_iff_exp_lt (by simp), hD₀]
    simp
  apply coeff_eventually_equal (D := D) hℱ |>.mono
  intro _ hf
  apply lt_of_le_of_lt (valuation_le_iff_coeff_lt_eq_zero K |>.mpr _) hD
  intro n hn
  rw [HahnSeries.coeff_sub, sub_eq_zero, eq_comm]
  exact hf _ hn

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
c : n →₀ R
inst✝ : IsDomain R
hc_gcd : ∀ (r : R), (∀ (i : n), r ∣ c i) → IsUnit r
h : ∀ m ∈ (sumSMulX c).support, ∀ (x : n), m x = 0
i : n
hi : c i ≠ 0
⊢ Finsupp.single i 1 ∈ (sumSMulX c).support

Tactic:
rwa [mem_support_iff, coeff_sumSMulX]

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case h
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
γ : (WithZero (Multiplicative ℤ))ˣ
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : HahnSeries.order f < 0
η : (WithZero (Multiplicative ℤ))ˣ := Units.mk0 (exp (HahnSeries.order f)) ⋯
hη : η = Units.mk0 (exp (HahnSeries.order f)) ⋯
P : K[X]
hP : (PowerSeries.idealX K).intValuation (F - ↑P) < ↑(η * γ)
s : ℕ
F_mul : ((ofPowerSeries ℤ K) (PowerSeries.X ^ s))⁻¹ * (ofPowerSeries ℤ K) F = f
hs : HahnSeries.order f = -↑s
⊢ Valued.v (f - (algebraMap K⟮X⟯ K⸨X⸩) (RatFunc.X ^ HahnSeries.order f * ↑P)) < ↑γ

Tactic:
have : (algebraMap K⟮X⟯ K⸨X⸩) 1 = 1 := by exact algebraMap.coe_one
      rw [hs, ← F_mul, PowerSeries.coe_pow, PowerSeries.coe_X, map_mul, zpow_neg,
        zpow_natCast, inv_eq_one_div (RatFunc.X ^ s), map_div₀, map_pow,
        RatFunc.coe_X]
      simp only [map_one]
      rw [← inv_eq_one_div, ← mul_sub, map_mul, map_inv₀,
        ← PowerSeries.coe_X, valuation_X_pow, ← hs, ← RatFunc.coe_coe, ← PowerSeries.coe_sub,
        ← coe_algebraMap, adicValued_apply, valuation_of_algebraMap,
        ← Units.val_mk0 (a := exp f.order) exp_ne_zero, ← hη]
      apply inv_mul_lt_of_lt_mul₀
      rwa [← Units.val_mul]

Goal state after:
Module: Mathlib.RingTheory.Morita.Matrix

Goal state before:
pp: R : Type u
ι : Type v
inst✝⁴ : Ring R
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ι
r : R
x✝ : ↥(toModuleCatObj R (ι → M) i)
x : ι → M
hx : x ∈ toModuleCatObj R (ι → M) i
⊢ ∑ i_1, ↑(r • ⟨x, hx⟩) i_1 = (RingHom.id R) r • ∑ i_1, ↑⟨x, hx⟩ i_1

Tactic:
by simp [Finset.smul_sum]

Goal state after:
Module: Mathlib.RingTheory.Morita.Matrix

Goal state before:
pp: R : Type u
ι : Type v
inst✝² : Ring R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
X : ModuleCat R
this :
  ↑(toModuleCatFromModuleCatLinearEquiv R ((toMatrixModCat R ι).obj X) i).symm ∘ₗ
      LinearMap.mapMatrixModule ι (Hom.hom ((unitIso R i).inv.app X)) =
    LinearMap.id
⊢ Hom.hom
      ((toMatrixModCat R ι).map ((unitIso R i).symm.hom.app X) ≫ (counitIso R i).hom.app ((toMatrixModCat R ι).obj X)) =
    Hom.hom (𝟙 ((toMatrixModCat R ι).obj X))

Tactic:
by simpa using! this

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

Goal state before:
pp: case succ
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p : ℕ
hp : p ≠ 0
inst✝ : ExpChar R p
f : MvPowerSeries σ R
k : ℕ
n_ih : (map (iterateFrobenius R p k)) ((expand (p ^ k) ⋯) f) = f ^ p ^ k
⊢ (map (frobenius R p)) ((expand p hp) ((map (iterateFrobenius R p k)) ((expand (p ^ k) ⋯) f))) =
    (map (iterateFrobenius R p 1)) ((map (iterateFrobenius R p k)) ((expand (p * p ^ k) ⋯) f))

Tactic:
← map_expand,

Goal state after:
case succ
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p : ℕ
hp : p ≠ 0
inst✝ : ExpChar R p
f : MvPowerSeries σ R
k : ℕ
n_ih : (map (iterateFrobenius R p k)) ((expand (p ^ k) ⋯) f) = f ^ p ^ k
⊢ (map (frobenius R p)) ((map (iterateFrobenius R p k)) ((expand p hp) ((expand (p ^ k) ⋯) f))) =
    (map (iterateFrobenius R p 1)) ((map (iterateFrobenius R p k)) ((expand (p * p ^ k) ⋯) f))
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: R : Type u_1
K : Type u_2
inst✝ : Field K
a : K
⊢ (powerSeriesRingEquiv K) ((algebraMap K K⟦X⟧) a) = (algebraMap K ↥(adicCompletionIntegers K⟮X⟯ (idealX K))) a

Tactic:
rw [PowerSeries.algebraMap_eq, RingHom.algebraMap_toAlgebra, ← Subtype.coe_inj,
    powerSeriesRingEquiv_coe_apply,
    RingHom.codRestrict_apply _ _ (algebraMap_C_mem_adicCompletionIntegers K)]

Goal state after:
R : Type u_1
K : Type u_2
inst✝ : Field K
a : K
⊢ (LaurentSeriesRingEquiv K) ((ofPowerSeries ℤ K) (PowerSeries.C a)) =
    ((LaurentSeriesRingEquiv K).toRingHom.comp HahnSeries.C) a
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝¹ : CommRing R
hp : NeZero p
inst✝ : CharZero R
n : ℕ
this : ∀ (i : ℕ), ((monomial (single i (p ^ (n - i)))) (↑p ^ i)).vars = {i}
⊢ (∑ i ∈ range (n + 1), (monomial (single i (p ^ (n - i)))) (↑p ^ i)).vars = range (n + 1)

Tactic:
vars_sum_of_disjoint

Goal state after:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
hp : NeZero p
inst✝ : CharZero R
n : ℕ
this : ∀ (i : ℕ), ((monomial (single i (p ^ (n - i)))) (↑p ^ i)).vars = {i}
⊢ ((range (n + 1)).biUnion fun i ↦ ((monomial (single i (p ^ (n - i)))) (↑p ^ i)).vars) = range (n + 1)

case h
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
hp : NeZero p
inst✝ : CharZero R
n : ℕ
this : ∀ (i : ℕ), ((monomial (single i (p ^ (n - i)))) (↑p ^ i)).vars = {i}
⊢ Pairwise (Function.onFun Disjoint fun i ↦ ((monomial (single i (p ^ (n - i)))) (↑p ^ i)).vars)
Module: Mathlib.RingTheory.WittVector.Defs

Goal state before:
pp: p : ℕ
R : Type u_1
x y : 𝕎 R
h : ∀ (n : ℕ), x.coeff n = y.coeff n
⊢ x = y

Tactic:
by
  cases x
  cases y
  simp only at h
  simp [funext_iff, h]

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

Goal state before:
pp: p : ℕ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
α : Type u_3
β : Type u_4
inst✝ : Invertible ↑p
⊢ LeftInverse (fun x ↦ mk p fun n ↦ (aeval x) (xInTermsOfW p R n)) ghostFun

Tactic:
by
    intro x
    ext n
    have := bind₁_wittPolynomial_xInTermsOfW p R n
    apply_fun aeval x.coeff at this
    simpa +unfoldPartialApp only [aeval_bind₁, aeval_X, ghostFun,
      aeval_wittPolynomial]

Goal state after: