mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.KrullDimension.LocalRing

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
x✝ : ¬IsField R ∧ ∀ (x : R), x ≠ 0 → IsLocalRing.maximalIdeal R ≤ (Ideal.span {x}).radical
hn : ¬IsField R
h✝ : ∀ (x : R), x ≠ 0 → IsLocalRing.maximalIdeal R ≤ (Ideal.span {x}).radical
this : ¬ringKrullDim R ≤ 0
h : Ring.KrullDimLE 1 R
⊢ ringKrullDim R = 1

Tactic:
Ring.krullDimLE_iff

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
x✝ : ¬IsField R ∧ ∀ (x : R), x ≠ 0 → IsLocalRing.maximalIdeal R ≤ (Ideal.span {x}).radical
hn : ¬IsField R
h✝ : ∀ (x : R), x ≠ 0 → IsLocalRing.maximalIdeal R ≤ (Ideal.span {x}).radical
this : ¬ringKrullDim R ≤ 0
h : ringKrullDim R ≤ ↑1
⊢ ringKrullDim R = 1
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
⊢ f n ⊓ (N + a ^ n • ⊤) = N

Tactic:
refine le_antisymm (fun r ⟨h1, h2⟩ ↦ ?_) (le_inf (fun x ↦ N.smul_mem (a ^ n)) (by simp))
    simp only [add_eq_sup, SetLike.mem_coe, mem_sup, mem_smul_pointwise_iff_exists] at h2
    obtain ⟨x, hx, -, ⟨y, -, rfl⟩, rfl⟩ := h2
    have h : (a ^ n • y ∈ N) = (a ^ (n + n) • y ∈ N) := congr_arg (y ∈ ·) (hn (n + n) le_add_self)
    rw [pow_add, mul_smul] at h
    rwa [N.add_mem_iff_right hx, h, ← N.add_mem_iff_right (N.smul_mem (a ^ n) hx), ← smul_add]

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
S : Submonoid R
X : ModuleCat R
inj : Injective X
⊢ Injective ((localizedModuleFunctor S).obj X)

Tactic:
by
    let _ : Small.{v, u} (Localization S) := small_of_surjective Localization.mkHom_surjective
    rw [← Module.injective_iff_injective_object] at inj ⊢
    simpa [ModuleCat.localizedModuleFunctor] using
      Module.injective_of_isLocalizedModule S (X.localizedModuleMkLinearMap S)

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
M : ModuleCat R
⊢ Injective M ↔ ∀ (m : MaximalSpectrum R), Injective (M.localizedModule m.asIdeal.primeCompl)

Tactic:
refine ⟨fun h m ↦ ?_, fun h ↦ ?_⟩

Goal state after:
case zero.refine_1
R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
M : ModuleCat R
h : Injective M
m : MaximalSpectrum R
⊢ Injective (M.localizedModule m.asIdeal.primeCompl)

case zero.refine_2
R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
M : ModuleCat R
h : ∀ (m : MaximalSpectrum R), Injective (M.localizedModule m.asIdeal.primeCompl)
⊢ Injective M
Module: Mathlib.RingTheory.MvPolynomial.EulerIdentity

Goal state before:
pp: case refine_4
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
φ : MvPolynomial σ R
inst✝ : Fintype σ
n : ℕ
w : σ → ℕ
h✝ : φ ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = n})
r : R
p : MvPolynomial σ R
x✝ : p ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = n})
h : ∑ i, w i • (X i * (pderiv i) p) = n • p
⊢ ∑ x, ↑(w x) * (X x * r • (pderiv x) p) = ↑n * r • p

Tactic:
mul_smul_comm,

Goal state after:
case refine_4
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
φ : MvPolynomial σ R
inst✝ : Fintype σ
n : ℕ
w : σ → ℕ
h✝ : φ ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = n})
r : R
p : MvPolynomial σ R
x✝ : p ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = n})
h : ∑ i, w i • (X i * (pderiv i) p) = n • p
⊢ ∑ x, r • (↑(w x) * (X x * (pderiv x) p)) = r • (↑n * p)
Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic

Goal state before:
pp: 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
⊢ Irreducible f

Tactic:
by
  classical
  have hfd : f.coeff d ≠ 0 := by simpa using hd
  let d₀ := d.erase i
  let φ : MvPolynomial n R := monomial d₀ (f.coeff d)
  let ψ : MvPolynomial n R := f - φ * X i
  have hf : f = φ * X i + ψ := by grind only
  have hφ : φ * X i = monomial d (f.coeff d) := by
    nth_rw 1 [← Finsupp.erase_add_single i d]; simp [φ, monomial_add_single, hdi, d₀]
  have hdψ (k) : ψ.coeff k = if d = k then 0 else f.coeff k := by
    simp +contextual [ψ, hφ, sub_eq_iff_eq_add, ite_add_ite]
  rw [hf]
  apply irreducible_mul_X_add
  · grind only [monomial_eq_zero]
  · simp [φ, hfd, d₀, hdi]
  · suffices ∀ x, d ≠ x → x ∈ f.support → i ∉ x.support by
      simpa [mem_vars_iff_mem_support, hdψ] using this
    exact fun x hxd hx hix ↦
      Finset.disjoint_iff_ne.mp (disjoint hd hx hxd) i (by simp [hdi]) _ hix rfl
  · rintro p hpφ ⟨q, hq⟩
    obtain ⟨m, b, hm, hb, rfl⟩ := (dvd_monomial_iff_exists hfd).mp hpφ
    obtain ⟨d₂, hd₂, H⟩ := nontrivial.exists_ne d
    obtain rfl : m = 0 := by
      have aux : coeff d₂ ψ ≠ 0 := by simpa [hdψ, H.symm] using hd₂
      simp only [hq, coeff_monomial_mul', ne_eq, ite_eq_right_iff, Classical.not_imp] at aux
      simpa using disjoint hd₂ hd H (Finsupp.support_mono aux.1)
        ((Finsupp.support_mono hm).trans (d.support.erase_subset i))
    have hb' : IsUnit b := isPrimitive _ fun k ↦
      if hk : k = d then hk ▸ hb else hf ▸ by simp [hq, hφ, Ne.symm hk]
    simpa

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:
mem_support_iff,

Goal state after:
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
⊢ coeff (Finsupp.single i 1) (sumSMulX c) ≠ 0
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : LinearOrder σ
p : MvPolynomial σ R
hp : p.IsSymmetric
h0 : p ≠ 0
i j : σ
hle : i ≤ j
hlt : (ofLex (supDegree (⇑toLex) p)) i < (ofLex (supDegree (⇑toLex) p)) j
⊢ ?m.112 ∈ ((rename ⇑(Equiv.swap i j)) p).support

Tactic:
mem_support_iff,

Goal state after:
σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : LinearOrder σ
p : MvPolynomial σ R
hp : p.IsSymmetric
h0 : p ≠ 0
i j : σ
hle : i ≤ j
hlt : (ofLex (supDegree (⇑toLex) p)) i < (ofLex (supDegree (⇑toLex) p)) j
⊢ coeff ?m.126 ((rename ⇑(Equiv.swap i j)) p) ≠ 0

σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : LinearOrder σ
p : MvPolynomial σ R
hp : p.IsSymmetric
h0 : p ≠ 0
i j : σ
hle : i ≤ j
hlt : (ofLex (supDegree (⇑toLex) p)) i < (ofLex (supDegree (⇑toLex) p)) j
⊢ σ →₀ ℕ
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

Goal state before:
pp: σ : Type u_1
inst✝ : DecidableEq σ
t : Finset σ × σ
⊢ pairMap σ t ≠ t

Tactic:
by
  rw [pairMap]
  split_ifs with h1
  all_goals by_contra ht; rw [← ht] at h1; simp_all

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

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
m : σ →₀ ℕ
i : σ
h : ∑ᶠ (d : σ →₀ ℕ), (coeff d) φ • (coeff m) (d.prod fun s e ↦ (X s ^ p) ^ e) ≠ 0
hc : ∀ (d : σ →₀ ℕ), (coeff m) (d.prod fun s e ↦ (X s ^ p) ^ e) = 0
⊢ False

Tactic:
finsum_eq_zero_of_forall_eq_zero fun d => by simp [hc d]

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
m : σ →₀ ℕ
i : σ
h : 0 ≠ 0
hc : ∀ (d : σ →₀ ℕ), (coeff m) (d.prod fun s e ↦ (X s ^ p) ^ e) = 0
⊢ False
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case pos
K : Type u_2
inst✝ : Field K
a : adicCompletion K⟮X⟯ (idealX K)
this : ∀ (s : Set (adicCompletion K⟮X⟯ (idealX K))), s ∈ 𝓝 0 ↔ ∃ γ, {x | Valued.v.restrict x < ↑γ} ⊆ s
ha : a = 0
S : Set (WithZero (Multiplicative ℤ))
⊢ S ∈ 𝓝 (Valued.v a) →
    ⇑Valued.v ⁻¹' S ∈
      Filter.comap (fun x ↦ { toCompletion := ↑((WithVal.equiv (valuation K⟮X⟯ (idealX K))).symm x) }) (𝓝 a)

Tactic:
hS

Goal state after:
case pos
K : Type u_2
inst✝ : Field K
a : adicCompletion K⟮X⟯ (idealX K)
this : ∀ (s : Set (adicCompletion K⟮X⟯ (idealX K))), s ∈ 𝓝 0 ↔ ∃ γ, {x | Valued.v.restrict x < ↑γ} ⊆ s
ha : a = 0
S : Set (WithZero (Multiplicative ℤ))
hS : S ∈ 𝓝 (Valued.v a)
⊢ ⇑Valued.v ⁻¹' S ∈
    Filter.comap (fun x ↦ { toCompletion := ↑((WithVal.equiv (valuation K⟮X⟯ (idealX K))).symm x) }) (𝓝 a)
Module: Mathlib.RingTheory.MvPowerSeries.Expand

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
hφ : φ ≠ 0
d : σ →₀ ℕ
hd : ↑(Finsupp.degree d) < p • φ.order
h : ∀ (i : σ), p ∣ d i
m : σ →₀ ℕ
hm : p • m = d
⊢ (coeff d) ((expand p hp) φ) = 0

Tactic:
rw [← hm, coeff_expand_smul, coeff_of_lt_order]

Goal state after:
case pos
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
hφ : φ ≠ 0
d : σ →₀ ℕ
hd : ↑(Finsupp.degree d) < p • φ.order
h : ∀ (i : σ), p ∣ d i
m : σ →₀ ℕ
hm : p • m = d
⊢ ↑(Finsupp.degree m) < φ.order
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: 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}
a b : ℕ
h : a ≠ b
⊢ Function.onFun Disjoint (fun i ↦ {i}) a b

Tactic:
apply disjoint_singleton_left.mpr

Goal state after:
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}
a b : ℕ
h : a ≠ b
⊢ a ∉ (fun i ↦ {i}) b
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: case ind
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Invertible ↑p
n : ℕ
IH : ∀ m < n, constantCoeff (xInTermsOfW p R m) = 0
m : ℕ
H : m < n
⊢ ↑p ^ m * 0 ^ p ^ (n - m) = 0

Tactic:
rw [zero_pow, mul_zero]

Goal state after:
case ind
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Invertible ↑p
n : ℕ
IH : ∀ m < n, constantCoeff (xInTermsOfW p R m) = 0
m : ℕ
H : m < n
⊢ p ^ (n - m) ≠ 0
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: case ind
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ (xInTermsOfW p ℚ m).vars ∧ (xInTermsOfW p ℚ m).vars ⊆ range (m + 1)
i : ℕ
⊢ i ∈ {n} ∪ (∑ i ∈ range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)).vars → i ∈ {n} ∪ range n

Tactic:
mem_union,

Goal state after:
case ind
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ (xInTermsOfW p ℚ m).vars ∧ (xInTermsOfW p ℚ m).vars ⊆ range (m + 1)
i : ℕ
⊢ i ∈ {n} ∨ i ∈ (∑ i ∈ range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)).vars → i ∈ {n} ∪ range n
Module: Mathlib.RingTheory.WittVector.Basic

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
x : 𝕎 R
n : ℕ
hx : ∀ i ≤ n, ↑p ∣ x.coeff i
i : ℕ
hi : i ∈ Finset.range (n + 1)
⊢ ↑p ^ (n + 1) ∣ (aeval x.coeff) ((monomial (Finsupp.single i (p ^ (n - i)))) (↑p ^ i))

Tactic:
simp only [Finset.mem_range] at hi

Goal state after:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
x : 𝕎 R
n : ℕ
hx : ∀ i ≤ n, ↑p ∣ x.coeff i
i : ℕ
hi : i < n + 1
⊢ ↑p ^ (n + 1) ∣ (aeval x.coeff) ((monomial (Finsupp.single i (p ^ (n - i)))) (↑p ^ i))
Module: Mathlib.RingTheory.WittVector.IsPoly

Goal state before:
pp: p : ℕ
R S : Type u
idx : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
⊢ ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x : 𝕎 R), coeff 1 = fun n ↦ (aeval x.coeff) (onePoly n)

Tactic:
by
      intros; funext n; cases n
      · simp only [one_coeff_zero, onePoly, ite_true, map_one]
      · simp only [Nat.succ_pos', one_coeff_eq_of_pos, onePoly, Nat.succ_ne_zero, ite_false,
          map_zero]

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

Goal state before:
pp: case h
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst✝² : CommRing R
inst✝¹ : CharP R p
inst✝ : PerfectRing R p
x : 𝕎 R
n i : ℕ
hi : i < n + 1
⊢ ∀ (n_1 : ℕ),
    Subsingleton
      ↑{r |
          r ∈ Finset.Iic n ∧
            ((teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ r) (x.coeff r)) * ↑p ^ r).coeff n_1 ≠ 0}

Tactic:
· refine fun n ↦ ⟨fun ⟨a, _, ha⟩ ⟨b, _, hb⟩ ↦ ?_⟩
    ext
    dsimp only [ne_eq, Set.mem_ofPred_eq]
    rw [← Not.imp_symm (teichmuller_mul_pow_coeff_of_ne _) ha]
    exact Not.imp_symm (teichmuller_mul_pow_coeff_of_ne _) hb

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Hermite.Basic

Goal state before:
pp: case neg
n k : ℕ
h : ¬Even (n + k)
⊢ (hermite n).coeff k = 0

Tactic:
exact coeff_hermite_of_odd_add (Nat.not_even_iff_odd.1 h)

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

Goal state before:
pp: n : ℕ
z : ℂ
h1✝ : z ^ n = z + 1
h1 : z = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
z_ne_zero : z ≠ 0
key : z ^ n = z
⊢ 1 = 0

Tactic:
left_eq_add

Goal state after:
n : ℕ
z : ℂ
h1✝ : z ^ n = z + 1
h1 : 1 = 0
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
z_ne_zero : z ≠ 0
key : z ^ n = z
⊢ 1 = 0
Module: Mathlib.RingTheory.Polynomial.Selmer

Goal state before:
pp: n : ℕ
hn1 : n ≠ 1
⊢ Irreducible (X ^ n - X - 1)

Tactic:
by
  by_cases hn0 : n = 0
  · rw [hn0, pow_zero, sub_sub, add_comm, ← sub_sub, sub_self, zero_sub]
    exact Associated.irreducible ⟨-1, mul_neg_one X⟩ irreducible_X
  have hn : 1 < n := Nat.one_lt_iff_ne_zero_and_ne_one.mpr ⟨hn0, hn1⟩
  have hp : (X ^ n - X - 1 : ℤ[X]) = trinomial 0 1 n (-1) (-1) 1 := by
    simp only [trinomial, C_neg, C_1]; ring
  rw [hp]
  apply IsUnitTrinomial.irreducible_of_coprime' ⟨0, 1, n, zero_lt_one, hn, -1, -1, 1, rfl⟩
  rintro z ⟨h1, h2⟩
  apply X_pow_sub_X_sub_one_irreducible_aux (n := n) z
  rw [trinomial_mirror zero_lt_one hn (-1 : ℤˣ).ne_zero (1 : ℤˣ).ne_zero] at h2
  simp_rw [trinomial, aeval_add, aeval_mul, aeval_X_pow, aeval_C,
    Units.val_neg, Units.val_one, map_neg, map_one] at h1 h2
  replace h1 : z ^ n = z + 1 := by linear_combination h1
  replace h2 := mul_eq_zero_of_left h2 z
  rw [add_mul, add_mul, add_zero, mul_assoc (-1 : ℂ), ← pow_succ, Nat.sub_add_cancel hn.le] at h2
  rw [h1] at h2 ⊢
  exact ⟨rfl, by linear_combination -h2⟩

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

Goal state before:
pp: A : Type u_1
inst✝ : Semiring A
I J : Ideal A
f g : A⟦X⟧
n : ℕ
hf : ∀ i ≤ n, (coeff i) f ∈ I
hg : ∀ i ≤ n, (coeff i) g ∈ J
i : ℕ
hi : i ≤ n
⊢ (coeff i) (f * g) ∈ I * J

Tactic:
coeff_mul

Goal state after:
A : Type u_1
inst✝ : Semiring A
I J : Ideal A
f g : A⟦X⟧
n : ℕ
hf : ∀ i ≤ n, (coeff i) f ∈ I
hg : ∀ i ≤ n, (coeff i) g ∈ J
i : ℕ
hi : i ≤ n
⊢ ∑ p ∈ Finset.antidiagonal i, (coeff p.1) f * (coeff p.2) g ∈ I * J
Module: Mathlib.RingTheory.PowerSeries.Expand

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
⊢ expand 1 ⋯ = AlgHom.id R R⟦X⟧

Tactic:
simp [expand]

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

Goal state before:
pp: R : Type u_1
inst✝ : NormedRing R
c : ℝ
f : R⟦X⟧
⊢ Tendsto ((fun n ↦ ‖(coeff n) f‖ * c ^ n) ∘ ⇑(Finsupp.uniqueEquiv ())) cofinite (𝓝 0) ↔
    Tendsto (fun t ↦ ‖(coeff t) f‖ * c ^ t) cofinite (𝓝 0)

Tactic:
exact ⟨fun H ↦ (H.comp (Finsupp.uniqueEquiv ()).symm.injective.tendsto_cofinite).congr fun n ↦
    by simp, fun H ↦ H.comp (Finsupp.uniqueEquiv ()).injective.tendsto_cofinite⟩

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

Goal state before:
pp: n : ℕ
hn : 0 < n
⊢ (coeff n) (X * largeSchroderSeries * largeSchroderSeries) = ∑ i ∈ range n, i.largeSchroder * (n - 1 - i).largeSchroder

Tactic:
coeff_mul

Goal state after:
n : ℕ
hn : 0 < n
⊢ ∑ p ∈ antidiagonal n, (coeff p.1) (X * largeSchroderSeries) * (coeff p.2) largeSchroderSeries =
    ∑ i ∈ range n, i.largeSchroder * (n - 1 - i).largeSchroder
Module: Mathlib.RingTheory.Radical.NatInt

Goal state before:
pp: n : ℕ
⊢ (normalizedFactors n).toFinset = n.primeFactors

Tactic:
Nat.factors_eq,

Goal state after:
n : ℕ
⊢ (↑n.primeFactorsList).toFinset = n.primeFactors
Module: Mathlib.RingTheory.Radical.NatInt

Goal state before:
pp: z : ℤ
⊢ 1 < radical z ↔ 1 < z.natAbs

Tactic:
rw [← radical_natAbs_eq_radical, Nat.one_lt_cast]

Goal state after:
z : ℤ
⊢ 1 < radical z.natAbs ↔ 1 < z.natAbs
Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG

Goal state before:
pp: case right
R : Type u_1
S : Type u_2
N : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
A : Subalgebra R S
hA : A.FG
t t' : ↥A ⊗[R] N
h✝ : (rTensor N A.val.toLinearMap) t = (rTensor N A.val.toLinearMap) t'
P : Submodule R ↥A
hP : P.FG
u : ↥P ⊗[R] N
hu : (rTensor N P.subtype) u = t
P' : Submodule R ↥A
hP' : P'.FG
u' : ↥P' ⊗[R] N
hu' : (rTensor N P'.subtype) u' = t'
P₁ : Submodule R S := Submodule.map (Subalgebra.toSubmodule A).subtype (P ⊔ P')
hP₁ : P₁.FG
j : ↥P →ₗ[R] ↥P₁ := (Subalgebra.toSubmodule A).subtype.restrict ⋯
j' : ↥P' →ₗ[R] ↥P₁ := (Subalgebra.toSubmodule A).subtype.restrict ⋯
u₁ : ↥P₁ ⊗[R] N := (rTensor N j) u
hu₁ : u₁ = (rTensor N j) u
u'₁ : ↥P₁ ⊗[R] N := (rTensor N j') u'
hu'₁ : u'₁ = (rTensor N j') u'
this : (rTensor N P₁.subtype) u₁ = (rTensor N P₁.subtype) u'₁
P'₁ : Submodule R S
hP₁_le : P₁ ≤ P'₁
hP'₁ : P'₁.FG
h : (rTensor N (inclusion hP₁_le)) u₁ = (rTensor N (inclusion hP₁_le)) u'₁
s : Finset S
hs : span R ↑s = P'₁
w : Finset S
hw : Algebra.adjoin R ↑w = A
B : Subalgebra R S := Algebra.adjoin R ↑(s ∪ w)
hBA : A ≤ B
hP'₁_le : P'₁ ≤ Subalgebra.toSubmodule B
k : (Subalgebra.inclusion hBA).toLinearMap ∘ₗ P.subtype = inclusion hP'₁_le ∘ₗ inclusion hP₁_le ∘ₗ j
k' : (Subalgebra.inclusion hBA).toLinearMap ∘ₗ P'.subtype = inclusion hP'₁_le ∘ₗ inclusion hP₁_le ∘ₗ j'
⊢ (rTensor N ((Subalgebra.inclusion hBA).toLinearMap ∘ₗ P.subtype)) u =
    (rTensor N ((Subalgebra.inclusion hBA).toLinearMap ∘ₗ P'.subtype)) u'

Tactic:
k,

Goal state after:
case right
R : Type u_1
S : Type u_2
N : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
A : Subalgebra R S
hA : A.FG
t t' : ↥A ⊗[R] N
h✝ : (rTensor N A.val.toLinearMap) t = (rTensor N A.val.toLinearMap) t'
P : Submodule R ↥A
hP : P.FG
u : ↥P ⊗[R] N
hu : (rTensor N P.subtype) u = t
P' : Submodule R ↥A
hP' : P'.FG
u' : ↥P' ⊗[R] N
hu' : (rTensor N P'.subtype) u' = t'
P₁ : Submodule R S := Submodule.map (Subalgebra.toSubmodule A).subtype (P ⊔ P')
hP₁ : P₁.FG
j : ↥P →ₗ[R] ↥P₁ := (Subalgebra.toSubmodule A).subtype.restrict ⋯
j' : ↥P' →ₗ[R] ↥P₁ := (Subalgebra.toSubmodule A).subtype.restrict ⋯
u₁ : ↥P₁ ⊗[R] N := (rTensor N j) u
hu₁ : u₁ = (rTensor N j) u
u'₁ : ↥P₁ ⊗[R] N := (rTensor N j') u'
hu'₁ : u'₁ = (rTensor N j') u'
this : (rTensor N P₁.subtype) u₁ = (rTensor N P₁.subtype) u'₁
P'₁ : Submodule R S
hP₁_le : P₁ ≤ P'₁
hP'₁ : P'₁.FG
h : (rTensor N (inclusion hP₁_le)) u₁ = (rTensor N (inclusion hP₁_le)) u'₁
s : Finset S
hs : span R ↑s = P'₁
w : Finset S
hw : Algebra.adjoin R ↑w = A
B : Subalgebra R S := Algebra.adjoin R ↑(s ∪ w)
hBA : A ≤ B
hP'₁_le : P'₁ ≤ Subalgebra.toSubmodule B
k : (Subalgebra.inclusion hBA).toLinearMap ∘ₗ P.subtype = inclusion hP'₁_le ∘ₗ inclusion hP₁_le ∘ₗ j
k' : (Subalgebra.inclusion hBA).toLinearMap ∘ₗ P'.subtype = inclusion hP'₁_le ∘ₗ inclusion hP₁_le ∘ₗ j'
⊢ (rTensor N (inclusion hP'₁_le ∘ₗ inclusion hP₁_le ∘ₗ j)) u =
    (rTensor N ((Subalgebra.inclusion hBA).toLinearMap ∘ₗ P'.subtype)) u'
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝ : CommRing A
f g q : A⟦X⟧
r : A[X]
I : Ideal A
i : ℕ
hi : i < ((map (Ideal.Quotient.mk I)) g).order.toNat
H : f - ↑r = g * q
j : ℕ
hj : j ≤ i
this : (coeff j) ((map (Ideal.Quotient.mk I)) g) = 0
⊢ (coeff j) g ∈ I

Tactic:
rwa [coeff_map, ← RingHom.mem_ker, Ideal.mk_ker] at this

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

Goal state before:
pp: A : Type u_1
inst✝ : CommRing A
f g q : A⟦X⟧
r : A[X]
I : Ideal A
f' q' : A⟦X⟧
r' : A[X]
H : f.IsWeierstrassDivisionAt g q r I
H' : f'.IsWeierstrassDivisionAt g q' r' I
⊢ g * q + ↑r + (g * q' + ↑r') = g * (q + q') + ↑(r + r')

Tactic:
Polynomial.coe_add

Goal state after:
A : Type u_1
inst✝ : CommRing A
f g q : A⟦X⟧
r : A[X]
I : Ideal A
f' q' : A⟦X⟧
r' : A[X]
H : f.IsWeierstrassDivisionAt g q r I
H' : f'.IsWeierstrassDivisionAt g q' r' I
⊢ g * q + ↑r + (g * q' + ↑r') = g * (q + q') + (↑r + ↑r')
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: case succ
A : Type u_1
inst✝ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
f : A⟦X⟧
k i✝ : ℕ
q : A⟦X⟧ := H.seq f k
s : A⟦X⟧ := f - g * q
n : ℕ := ((map (Ideal.Quotient.mk I)) g).order.toNat
hi : i✝ ≥ n
hq : ∀ {i : ℕ}, i ≥ n → (coeff i) s ∈ I ^ k
s₀ : A[X] := (trunc n) s
s₁ : A⟦X⟧ := mk fun i ↦ (coeff (i + n)) s
hs : s = X ^ n * s₁ + ↑s₀
q' : A⟦X⟧ := q + s₁ * ↑⋯.unit⁻¹
key : f - g * q' = ↑s₀ - ↑((trunc n) g) * s₁ * ↑⋯.unit⁻¹
i : ℕ
⊢ (coeff i) (↑((trunc n) g) * s₁) ∈ I * I ^ k

Tactic:
refine coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal'
      (by simp [n, g.coeff_trunc_order_mem]) (fun i ↦ ?_) i

Goal state after:
case succ
A : Type u_1
inst✝ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
f : A⟦X⟧
k i✝¹ : ℕ
q : A⟦X⟧ := H.seq f k
s : A⟦X⟧ := f - g * q
n : ℕ := ((map (Ideal.Quotient.mk I)) g).order.toNat
hi : i✝¹ ≥ n
hq : ∀ {i : ℕ}, i ≥ n → (coeff i) s ∈ I ^ k
s₀ : A[X] := (trunc n) s
s₁ : A⟦X⟧ := mk fun i ↦ (coeff (i + n)) s
hs : s = X ^ n * s₁ + ↑s₀
q' : A⟦X⟧ := q + s₁ * ↑⋯.unit⁻¹
key : f - g * q' = ↑s₀ - ↑((trunc n) g) * s₁ * ↑⋯.unit⁻¹
i✝ i : ℕ
⊢ (coeff i) s₁ ∈ I ^ k
Module: Mathlib.RingTheory.RegularLocalRing.Defs

Goal state before:
pp: case pos
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsLocalRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
isf : IsField R
⊢ IsRegularLocalRing R

Tactic:
let := isf.toField
    simp [isRegularLocalRing_iff, maximalIdeal_eq_bot]

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

Goal state before:
pp: R : Type u
inst✝⁶ : CommSemiring R
M : Type u_3
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N : Type u_4
inst✝³ : AddCommMonoid N
inst✝² : Module R N
f : M →ₚₗ[R] N
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
x : M
⊢ 1 ⊗ₜ[R] f.ground x = toFun S f (1 ⊗ₜ[R] x)

Tactic:
simp only [ground, toFun'_eq_toFun]
  convert! f.isCompat_apply (Algebra.ofId R S) (1 ⊗ₜ[R] x)
  · simp only [Function.comp_apply, TensorProduct.lid_symm_apply, TensorProduct.includeRight_lid]
    congr
  · rw [rTensor_tmul, toLinearMap_apply, _root_.map_one]

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ IsOpenMap (PrimeSpectrum.comap C)

Tactic:
by
  rintro U ⟨s, z⟩
  rw [← compl_compl U, ← z, ← iUnion_of_singleton_coe s, zeroLocus_iUnion, compl_iInter,
    image_iUnion]
  simp_rw [← imageOfDf_eq_comap_C_compl_zeroLocus]
  exact isOpen_iUnion fun f => isOpen_imageOfDf

Goal state after: