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

Goal state before:
pp: case refine_3
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
s : Finset (Submodule R M)
hs : s.inf id = N
hs' : ∀ ⦃J : Submodule R M⦄, J ∈ s → J.IsPrimary
I : Submodule R M
hI :
  I ∈
    ↑(Finset.image (fun t ↦ t.inf id)
        (Finset.image (fun J ↦ {I ∈ s | (I.colon Set.univ).radical = (J.colon Set.univ).radical}) s))
J : Submodule R M
hJ :
  J ∈
    ↑(Finset.image (fun t ↦ t.inf id)
        (Finset.image (fun J ↦ {I ∈ s | (I.colon Set.univ).radical = (J.colon Set.univ).radical}) s))
hIJ : I ≠ J
⊢ ((fun x1 x2 ↦ x1 ≠ x2) on fun J ↦ (J.colon Set.univ).radical) I J

Tactic:
simp only [Finset.coe_image, Set.mem_image, Finset.mem_coe, exists_exists_and_eq_and] at hI hJ

Goal state after:
case refine_3
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
s : Finset (Submodule R M)
hs : s.inf id = N
hs' : ∀ ⦃J : Submodule R M⦄, J ∈ s → J.IsPrimary
I J : Submodule R M
hIJ : I ≠ J
hI : ∃ a ∈ s, {I ∈ s | (I.colon Set.univ).radical = (a.colon Set.univ).radical}.inf id = I
hJ : ∃ a ∈ s, {I ∈ s | (I.colon Set.univ).radical = (a.colon Set.univ).radical}.inf id = J
⊢ ((fun x1 x2 ↦ x1 ≠ x2) on fun J ↦ (J.colon Set.univ).radical) I J
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
s₀ : Finset ↑N.associatedPrimes
hs₀ : IsLowerSet ↑s₀
q : Submodule R M
hqp : q.IsPrimary
p : ↑N.associatedPrimes
hq : (q.colon Set.univ).radical = ↑p
⊢ comap (mkLinearMap (⨅ q ∈ s₀, (↑q).primeCompl) M)
      (localized₀ (⨅ q ∈ s₀, (↑q).primeCompl) (mkLinearMap (⨅ q ∈ s₀, (↑q).primeCompl) M) q) =
    if p ∈ s₀ then q else ⊤

Tactic:
set S := ⨅ q ∈ s₀, q.1.primeCompl
  set f := mkLinearMap S M
  split_ifs with hp
  · refine le_antisymm (fun x hx ↦ ?_) (map_le_iff_le_comap.mp (map_le_localized₀ S f q))
    obtain ⟨b, hb, a, ha⟩ := hx
    rw [IsLocalizedModule.mk'_eq_iff, ← LinearMap.map_smul_of_tower] at ha
    obtain ⟨c, hc⟩ := (IsLocalizedModule.eq_iff_exists S f).mp ha
    replace hb := q.smul_mem c hb
    rw [← Submonoid.smul_def, hc, smul_smul] at hb
    apply (hqp.mem_or_mem hb).resolve_right
    grind [Submonoid.mem_iInf, mem_primeCompl_iff]
  · replace hq : ¬ (q.colon Set.univ : Set R) ⊆ ⋃ r ∈ s₀, r := by
      contrapose hp
      obtain ⟨r, hrs, h⟩ := (subset_union_prime p p fun i _ _ _ ↦ i.2.1).mp hp
      rw [← r.2.1.radical_le_iff, hq] at h
      exact hs₀ h hrs
    obtain ⟨y, hy1, hy2⟩ := Set.not_subset_iff_exists_mem_notMem.mp hq
    replace hy2 : y ∈ S := by
      simp only [Submonoid.mem_iInf, Ideal.mem_primeCompl_iff, Subtype.forall, S]
      intro r hrI hrs
      contrapose hy2
      exact Set.mem_biUnion hrs hy2
    rw [eq_top_iff, ← map_le_iff_le_comap, map_top]
    rintro - ⟨x, rfl⟩
    simp_rw [mem_localized₀, IsLocalizedModule.mk'_eq_iff, ← LinearMap.map_smul_of_tower]
    exact ⟨y • x, hy1 (Set.smul_mem_smul_set (Set.mem_univ x)), ⟨y, hy2⟩, rfl⟩

Goal state after:
Module: Mathlib.RingTheory.LocalIso

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
⊢ IsLocalIso R S ↔ Ideal.span {g | IsStandardOpenImmersion R (Localization.Away g)} = ⊤

Tactic:
refine ⟨fun _ ↦ span_isStandardOpenImmersion_eq_top R S, fun h ↦ ⟨fun q hq ↦ ?_⟩⟩
  grind [Ideal.IsPrime.ne_top, Ideal.span_le, SetLike.mem_coe]

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

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommRing R
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
s : Set R
hs : Ideal.span s = ⊤
Mₚ : ↑s → Type u_3
inst✝⁷ : (g : ↑s) → AddCommGroup (Mₚ g)
inst✝⁶ : (g : ↑s) → Module R (Mₚ g)
Rₚ : ↑s → Type u_4
inst✝⁵ : (g : ↑s) → CommRing (Rₚ g)
inst✝⁴ : (g : ↑s) → Algebra R (Rₚ g)
inst✝³ : ∀ (g : ↑s), IsLocalization.Away (↑g) (Rₚ g)
inst✝² : (g : ↑s) → Module (Rₚ g) (Mₚ g)
inst✝¹ : ∀ (g : ↑s), IsScalarTower R (Rₚ g) (Mₚ g)
ϕ : (g : ↑s) → M →ₗ[R] Mₚ g
inst✝ : ∀ (g : ↑s), IsLocalizedModule (Submonoid.powers ↑g) (ϕ g)
h : ∀ (g : ↑s), FinitePresentation (Rₚ g) (Mₚ g)
this : Module.Finite R M
⊢ FinitePresentation R M

Tactic:
obtain ⟨n, f, fsurj⟩ := Module.Finite.exists_fin' R M

Goal state after:
R : Type u_1
inst✝¹⁰ : CommRing R
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
s : Set R
hs : Ideal.span s = ⊤
Mₚ : ↑s → Type u_3
inst✝⁷ : (g : ↑s) → AddCommGroup (Mₚ g)
inst✝⁶ : (g : ↑s) → Module R (Mₚ g)
Rₚ : ↑s → Type u_4
inst✝⁵ : (g : ↑s) → CommRing (Rₚ g)
inst✝⁴ : (g : ↑s) → Algebra R (Rₚ g)
inst✝³ : ∀ (g : ↑s), IsLocalization.Away (↑g) (Rₚ g)
inst✝² : (g : ↑s) → Module (Rₚ g) (Mₚ g)
inst✝¹ : ∀ (g : ↑s), IsScalarTower R (Rₚ g) (Mₚ g)
ϕ : (g : ↑s) → M →ₗ[R] Mₚ g
inst✝ : ∀ (g : ↑s), IsLocalizedModule (Submonoid.powers ↑g) (ϕ g)
h : ∀ (g : ↑s), FinitePresentation (Rₚ g) (Mₚ g)
this : Module.Finite R M
n : ℕ
f : (Fin n → R) →ₗ[R] M
fsurj : Function.Surjective ⇑f
⊢ FinitePresentation R M
Module: Mathlib.RingTheory.LocalIso

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra S T
inst✝³ : Algebra R T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalIso R S
inst✝ : IsLocalIso S T
⊢ IsLocalIso R T

Tactic:
let s : Set S := {g : S | IsStandardOpenImmersion R (Localization.Away g)}

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra S T
inst✝³ : Algebra R T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalIso R S
inst✝ : IsLocalIso S T
s : Set S := {g | IsStandardOpenImmersion R (Localization.Away g)}
⊢ IsLocalIso R T
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
injle : Injective M
⊢ Injective (M.localizedModule S)

Tactic:
rw [← Module.injective_iff_injective_object] at injle ⊢

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✝ : HasInjectiveDimensionLE M 0
injle : Module.Injective R ↑M
⊢ Module.Injective (Localization S) ↑(M.localizedModule S)
Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension

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

Tactic:
exact Module.projective_of_isLocalizedModule S (M.localizedModuleMkLinearMap S)

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
n : ℤ
h : ¬order x ≤ n
⊢ n - order x ∉ Set.range ⇑Nat.castOrderEmbedding

Tactic:
contrapose h
      simp only [Nat.castOrderEmbedding_apply, Set.mem_range] at h
      lia

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
⊢ (ofPowerSeries ℤ R) x.powerSeriesPart =
    (single (-order x)) 1 * ((single (order x)) 1 * (ofPowerSeries ℤ R) x.powerSeriesPart)

Tactic:
← mul_assoc,

Goal state after:
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
⊢ (ofPowerSeries ℤ R) x.powerSeriesPart =
    (single (-order x)) 1 * (single (order x)) 1 * (ofPowerSeries ℤ R) x.powerSeriesPart
Module: Mathlib.RingTheory.Localization.AtPrime.Extension

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
p : Ideal R
inst✝¹² : p.IsPrime
Rₚ : Type u_3
inst✝¹¹ : CommRing Rₚ
inst✝¹⁰ : Algebra R Rₚ
inst✝⁹ : IsLocalization.AtPrime Rₚ p
inst✝⁸ : IsLocalRing Rₚ
Sₚ : Type u_4
inst✝⁷ : CommRing Sₚ
inst✝⁶ : Algebra S Sₚ
inst✝⁵ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
P : Ideal S
hPp : P.LiesOver p
inst✝³ : Algebra R Sₚ
inst✝² : IsScalarTower R S Sₚ
inst✝¹ : IsScalarTower R Rₚ Sₚ
inst✝ : P.IsPrime
this : (Ideal.map (algebraMap S Sₚ) P).LiesOver (maximalIdeal Rₚ)
⊢ (Ideal.map (algebraMap S Sₚ) P).ramificationIdx Rₚ = P.ramificationIdx R

Tactic:
have := IsLocalization.liesOver_map_of_isPrime_disjoint (algebraMapSubmonoid S p.primeCompl) Sₚ
    (Set.disjoint_image_left.mpr (Set.disjoint_compl_left_iff_subset.mpr hPp.over.ge))

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
p : Ideal R
inst✝¹² : p.IsPrime
Rₚ : Type u_3
inst✝¹¹ : CommRing Rₚ
inst✝¹⁰ : Algebra R Rₚ
inst✝⁹ : IsLocalization.AtPrime Rₚ p
inst✝⁸ : IsLocalRing Rₚ
Sₚ : Type u_4
inst✝⁷ : CommRing Sₚ
inst✝⁶ : Algebra S Sₚ
inst✝⁵ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
P : Ideal S
hPp : P.LiesOver p
inst✝³ : Algebra R Sₚ
inst✝² : IsScalarTower R S Sₚ
inst✝¹ : IsScalarTower R Rₚ Sₚ
inst✝ : P.IsPrime
this✝ : (Ideal.map (algebraMap S Sₚ) P).LiesOver (maximalIdeal Rₚ)
this : (Ideal.map (algebraMap S Sₚ) P).LiesOver P
⊢ (Ideal.map (algebraMap S Sₚ) P).ramificationIdx Rₚ = P.ramificationIdx R
Module: Mathlib.RingTheory.MvPolynomial.EulerIdentity

Goal state before:
pp: case refine_3
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})
p q : MvPolynomial σ R
x✝¹ : p ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = n})
x✝ : q ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = n})
hp : ∑ i, w i • (X i * (pderiv i) p) = n • p
hq : ∑ i, w i • (X i * (pderiv i) q) = n • q
⊢ ∑ i, w i • (X i * (pderiv i) (p + q)) = n • (p + q)

Tactic:
map_add,

Goal state after:
case refine_3
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})
p q : MvPolynomial σ R
x✝¹ : p ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = n})
x✝ : q ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = n})
hp : ∑ i, w i • (X i * (pderiv i) p) = n • p
hq : ∑ i, w i • (X i * (pderiv i) q) = n • q
⊢ ∑ x, w x • (X x * ((pderiv x) p + (pderiv x) q)) = n • (p + q)
Module: Mathlib.RingTheory.MvPolynomial.Expand

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
f x✝¹ x✝ : MvPolynomial σ R
ha : (map (frobenius R p)) ((expand p) x✝¹) = x✝¹ ^ p
hb : (map (frobenius R p)) ((expand p) x✝) = x✝ ^ p
⊢ (map (frobenius R p)) ((expand p) (x✝¹ + x✝)) = (x✝¹ + x✝) ^ p

Tactic:
map_add,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
f x✝¹ x✝ : MvPolynomial σ R
ha : (map (frobenius R p)) ((expand p) x✝¹) = x✝¹ ^ p
hb : (map (frobenius R p)) ((expand p) x✝) = x✝ ^ p
⊢ (map (frobenius R p)) ((expand p) x✝¹ + (expand p) x✝) = (x✝¹ + x✝) ^ p
Module: Mathlib.RingTheory.MvPolynomial.Expand

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
f x✝¹ x✝ : MvPolynomial σ R
ha : (map (frobenius R p)) ((expand p) x✝¹) = x✝¹ ^ p
hb : (map (frobenius R p)) ((expand p) x✝) = x✝ ^ p
⊢ (map (frobenius R p)) ((expand p) x✝¹ + (expand p) x✝) = (x✝¹ + x✝) ^ p

Tactic:
map_add,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
f x✝¹ x✝ : MvPolynomial σ R
ha : (map (frobenius R p)) ((expand p) x✝¹) = x✝¹ ^ p
hb : (map (frobenius R p)) ((expand p) x✝) = x✝ ^ p
⊢ (map (frobenius R p)) ((expand p) x✝¹) + (map (frobenius R p)) ((expand p) x✝) = (x✝¹ + x✝) ^ p
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case add_single
R : Type u_3
n m : ℕ
inst✝¹ : CommSemiring R
r : R
hr : r ≠ 0
hnm : n ≤ m
inst✝ : Nontrivial R
i : Fin n
b✝ : ℕ
f✝ : Fin n →₀ ℕ
a✝¹ : i ∉ f✝.support
a✝ : b✝ ≠ 0
ih : ⇑(ofLex (supDegree (⇑toLex) (esymmAlgHomMonomial (Fin m) f✝ r))) = (accumulate n m) ⇑f✝
this : ↑i < m
⊢ (accumulate n m) ⇑f✝ + ⇑(ofLex (supDegree (⇑toLex) (esymm (Fin m) R (↑i + 1) ^ b✝))) =
    (accumulate n m) (⇑f✝ + ⇑fun₀ | i => b✝)

pp: case add_single.hq
R : Type u_3
n m : ℕ
inst✝¹ : CommSemiring R
r : R
hr : r ≠ 0
hnm : n ≤ m
inst✝ : Nontrivial R
i : Fin n
b✝ : ℕ
f✝ : Fin n →₀ ℕ
a✝¹ : i ∉ f✝.support
a✝ : b✝ ≠ 0
ih : ⇑(ofLex (supDegree (⇑toLex) (esymmAlgHomMonomial (Fin m) f✝ r))) = (accumulate n m) ⇑f✝
this : ↑i < m
⊢ Monic (⇑toLex) (esymm (Fin m) R (↑i + 1) ^ b✝)

pp: case add_single.hp
R : Type u_3
n m : ℕ
inst✝¹ : CommSemiring R
r : R
hr : r ≠ 0
hnm : n ≤ m
inst✝ : Nontrivial R
i : Fin n
b✝ : ℕ
f✝ : Fin n →₀ ℕ
a✝¹ : i ∉ f✝.support
a✝ : b✝ ≠ 0
ih : ⇑(ofLex (supDegree (⇑toLex) (esymmAlgHomMonomial (Fin m) f✝ r))) = (accumulate n m) ⇑f✝
this : ↑i < m
⊢ esymmAlgHomMonomial (Fin m) f✝ r ≠ 0

Tactic:
map_add,

Goal state after:
case add_single
R : Type u_3
n m : ℕ
inst✝¹ : CommSemiring R
r : R
hr : r ≠ 0
hnm : n ≤ m
inst✝ : Nontrivial R
i : Fin n
b✝ : ℕ
f✝ : Fin n →₀ ℕ
a✝¹ : i ∉ f✝.support
a✝ : b✝ ≠ 0
ih : ⇑(ofLex (supDegree (⇑toLex) (esymmAlgHomMonomial (Fin m) f✝ r))) = (accumulate n m) ⇑f✝
this : ↑i < m
⊢ (accumulate n m) ⇑f✝ + ⇑(ofLex (supDegree (⇑toLex) (esymm (Fin m) R (↑i + 1) ^ b✝))) =
    (accumulate n m) ⇑f✝ + (accumulate n m) ⇑fun₀ | i => b✝

case add_single.hq
R : Type u_3
n m : ℕ
inst✝¹ : CommSemiring R
r : R
hr : r ≠ 0
hnm : n ≤ m
inst✝ : Nontrivial R
i : Fin n
b✝ : ℕ
f✝ : Fin n →₀ ℕ
a✝¹ : i ∉ f✝.support
a✝ : b✝ ≠ 0
ih : ⇑(ofLex (supDegree (⇑toLex) (esymmAlgHomMonomial (Fin m) f✝ r))) = (accumulate n m) ⇑f✝
this : ↑i < m
⊢ Monic (⇑toLex) (esymm (Fin m) R (↑i + 1) ^ b✝)

case add_single.hp
R : Type u_3
n m : ℕ
inst✝¹ : CommSemiring R
r : R
hr : r ≠ 0
hnm : n ≤ m
inst✝ : Nontrivial R
i : Fin n
b✝ : ℕ
f✝ : Fin n →₀ ℕ
a✝¹ : i ∉ f✝.support
a✝ : b✝ ≠ 0
ih : ⇑(ofLex (supDegree (⇑toLex) (esymmAlgHomMonomial (Fin m) f✝ r))) = (accumulate n m) ⇑f✝
this : ↑i < m
⊢ esymmAlgHomMonomial (Fin m) f✝ r ≠ 0
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

Goal state before:
pp: σ : Type u_1
inst✝ : DecidableEq σ
⊢ Function.Involutive (pairMap σ)

Tactic:
by
  intro t
  rw [pairMap, pairMap]
  split_ifs with h1 h2 h3
  · simp at h2
  · simp [insert_erase h1]
  · simp_all
  · simp at h3

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
n : ℕ
p : MvPolynomial (Fin n) R
hp : p ∈ symmetricSubalgebra (Fin n) R
h0 : p ≠ 0
ih :
  ∀ y < supDegree (⇑toLex) p,
    ∀ (p : MvPolynomial (Fin n) R) (hp : p ∈ symmetricSubalgebra (Fin n) R),
      p ≠ 0 → supDegree (⇑toLex) p = y → ⟨p, hp⟩ ∈ (esymmAlgHom (Fin n) R n).range
t : Fin n →₀ ℕ := Finsupp.equivFunOnFinite.symm (invAccumulate n n ⇑(ofLex (supDegree (⇑toLex) p)))
⊢ ¬leadingCoeff (⇑toLex) p = 0

Tactic:
leadingCoeff_eq_zero toLex.injective

Goal state after:
R : Type u_3
inst✝ : CommRing R
n : ℕ
p : MvPolynomial (Fin n) R
hp : p ∈ symmetricSubalgebra (Fin n) R
h0 : p ≠ 0
ih :
  ∀ y < supDegree (⇑toLex) p,
    ∀ (p : MvPolynomial (Fin n) R) (hp : p ∈ symmetricSubalgebra (Fin n) R),
      p ≠ 0 → supDegree (⇑toLex) p = y → ⟨p, hp⟩ ∈ (esymmAlgHom (Fin n) R n).range
t : Fin n →₀ ℕ := Finsupp.equivFunOnFinite.symm (invAccumulate n n ⇑(ofLex (supDegree (⇑toLex) p)))
⊢ ¬p = 0
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
f : Finset σ × σ → MvPolynomial σ R
⊢ ∑ t ∈ pairs σ k with #t.1 < k, f t = ∑ a ∈ antidiagonal k with a.1 < k, ∑ A ∈ powersetCard a.1 univ, ∑ j, f (A, j)

Tactic:
rw [filter_pairs_lt, sum_product, sum_disjiUnion]

Goal state after:
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
f : Finset σ × σ → MvPolynomial σ R
⊢ ∑ i ∈ range k, ∑ x ∈ powersetCard i univ, ∑ y, f (x, y) =
    ∑ a ∈ antidiagonal k with a.1 < k, ∑ A ∈ powersetCard a.1 univ, ∑ j, f (A, j)
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

Goal state before:
pp: σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
⊢ {t ∈ pairs σ k | #t.1 < k}.disjUnion ({t ∈ pairs σ k | #t.1 = k}) ⋯ = pairs σ k

Tactic:
by
  grind [MvPolynomial.NewtonIdentities.pairs]

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
k : ℕ
⊢ ↑k * ∑ t ∈ powersetCard k univ, ∏ i ∈ t, X i = (-1) ^ k * ((-1) ^ k * ↑k * ∑ i ∈ powersetCard k univ, ∏ i ∈ i, X i)

Tactic:
← mul_assoc,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
k : ℕ
⊢ ↑k * ∑ t ∈ powersetCard k univ, ∏ i ∈ t, X i = (-1) ^ k * ((-1) ^ k * ↑k) * ∑ i ∈ powersetCard k univ, ∏ i ∈ i, X i
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
k : ℕ
⊢ ↑k * ∑ t ∈ powersetCard k univ, ∏ i ∈ t, X i = (-1) ^ k * ((-1) ^ k * ↑k) * ∑ i ∈ powersetCard k univ, ∏ i ∈ i, X i

Tactic:
← mul_assoc,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
k : ℕ
⊢ ↑k * ∑ t ∈ powersetCard k univ, ∏ i ∈ t, X i = (-1) ^ k * (-1) ^ k * ↑k * ∑ i ∈ powersetCard k univ, ∏ i ∈ i, X i
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 : σ →₀ ℕ
this : ∀ {d : σ →₀ ℕ}, (d.prod fun s e ↦ (X s ^ p) ^ e) = (monomial (p • d)) 1
⊢ ((coeff m) φ * if p • m = p • m then 1 else 0) = (coeff m) φ

Tactic:
if_pos rfl,

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
m : σ →₀ ℕ
this : ∀ {d : σ →₀ ℕ}, (d.prod fun s e ↦ (X s ^ p) ^ e) = (monomial (p • d)) 1
⊢ (coeff m) φ * 1 = (coeff m) φ
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
d : σ →₀ ℕ
hd : d ∈ Function.support ((expand p hp) φ)
this : ∀ (i : σ), p ∣ d i
m : σ →₀ ℕ := Finsupp.mapRange (fun n ↦ n / p) ⋯ d
eq_aux : p • m = d
⊢ d ∈ (fun x ↦ p • x) '' Function.support φ

Tactic:
Function.mem_support,

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
d : σ →₀ ℕ
hd : (expand p hp) φ d ≠ 0
this : ∀ (i : σ), p ∣ d i
m : σ →₀ ℕ := Finsupp.mapRange (fun n ↦ n / p) ⋯ d
eq_aux : p • m = d
⊢ d ∈ (fun x ↦ p • x) '' Function.support φ
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
d n : σ →₀ ℕ
hn₁ : n ∈ Function.support φ
hn₂ : (fun x ↦ p • x) n = d
hc : (expand p hp) φ (p • n) = 0
⊢ False

Tactic:
Function.mem_support,

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
d n : σ →₀ ℕ
hn₁ : φ n ≠ 0
hn₂ : (fun x ↦ p • x) n = d
hc : (expand p hp) φ (p • n) = 0
⊢ False
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

Goal state before:
pp: σ : Type u_1
inst✝¹ : Fintype σ
R : Type u_2
inst✝ : CommRing R
k : ℕ
h : 0 < k
hesymm :
  ↑k * esymm σ R k =
    (-1) ^ (k + 1) *
      (∑ x ∈ {a ∈ antidiagonal k | a.1 < k} with 0 < x.1, (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2 +
        ∑ x ∈ {a ∈ antidiagonal k | a.1 < k} with ¬0 < x.1, (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2)
sub_both_sides✝ :
  ↑k * esymm σ R k -
      (-1) ^ (k + 1) * ∑ a ∈ {a ∈ antidiagonal k | a.1 < k} with 0 < a.1, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2 =
    (-1) ^ (k + 1) * ∑ a ∈ {a ∈ antidiagonal k | a.1 < k} with ¬0 < a.1, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2
sub_both_sides :
  (-1) ^ (k + 1) * ↑k * esymm σ R k -
      ∑ a ∈ {a ∈ antidiagonal k | a.1 < k} with 0 < a.1, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2 =
    ∑ a ∈ antidiagonal k with a.1 < k ∧ ¬0 < a.1, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2
a : ℕ × ℕ
ha : a.1 + a.2 = k
left✝ : a.1 < k
ha0 : ¬0 < a.1
⊢ a = (0, a.1 + a.2)

Tactic:
Nat.eq_zero_of_not_pos ha0,

Goal state after:
σ : Type u_1
inst✝¹ : Fintype σ
R : Type u_2
inst✝ : CommRing R
k : ℕ
h : 0 < k
hesymm :
  ↑k * esymm σ R k =
    (-1) ^ (k + 1) *
      (∑ x ∈ {a ∈ antidiagonal k | a.1 < k} with 0 < x.1, (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2 +
        ∑ x ∈ {a ∈ antidiagonal k | a.1 < k} with ¬0 < x.1, (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2)
sub_both_sides✝ :
  ↑k * esymm σ R k -
      (-1) ^ (k + 1) * ∑ a ∈ {a ∈ antidiagonal k | a.1 < k} with 0 < a.1, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2 =
    (-1) ^ (k + 1) * ∑ a ∈ {a ∈ antidiagonal k | a.1 < k} with ¬0 < a.1, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2
sub_both_sides :
  (-1) ^ (k + 1) * ↑k * esymm σ R k -
      ∑ a ∈ {a ∈ antidiagonal k | a.1 < k} with 0 < a.1, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2 =
    ∑ a ∈ antidiagonal k with a.1 < k ∧ ¬0 < a.1, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2
a : ℕ × ℕ
ha : a.1 + a.2 = k
left✝ : a.1 < k
ha0 : ¬0 < a.1
⊢ a = (0, 0 + a.2)
Module: Mathlib.RingTheory.Morita.Matrix

Goal state before:
pp: R : Type u
ι : Type v
inst✝⁴ : Ring R
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
R₀ : Type u_1
inst✝¹ : CommRing R₀
inst✝ : Algebra R₀ R
i : ι
X Y : ModuleCat R
f : X ⟶ Y
r : R₀
⊢ (ModuleCat.matrixEquivalence R i).functor.map (r • f) = r • (ModuleCat.matrixEquivalence R i).functor.map f

Tactic:
ext (v : ι → X)
    simp only [ModuleCat.matrixEquivalence_functor, ModuleCat.toMatrixModCat_obj_carrier,
      ModuleCat.toMatrixModCat_map, ModuleCat.hom_smul, ModuleCat.hom_ofHom, LinearMap.smul_apply]
    ext i
    simp only [LinearMap.mapMatrixModule_apply, LinearMap.compLeft_apply, Function.comp_apply,
      LinearMap.smul_apply]
    change _ = ((algebraMap R₀ (Matrix ι ι R) r) • ((ModuleCat.Hom.hom f).mapMatrixModule ι v)) i
    simp [Matrix.algebraMap_matrix_apply]

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

Goal state before:
pp: R : Type u_1
inst✝ : NormedRing R
σ : Type u_2
c : σ → ℝ
f g : MvPowerSeries σ R
hf : Tendsto (fun t ↦ ‖(coeff t) f‖ * t.prod fun x1 x2 ↦ |c| x1 ^ x2) cofinite (𝓝 0)
hg : Tendsto (fun t ↦ ‖(coeff t) g‖ * t.prod fun x1 x2 ↦ |c| x1 ^ x2) cofinite (𝓝 0)
n : σ →₀ ℕ
⊢ 0 ≤ n.prod fun x1 x2 ↦ |c| x1 ^ x2

Tactic:
by dsimp [Finsupp.prod]; positivity

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case neg
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
⊢ ∃ γ,
    {y | Valued.v.restrict (y - a) < ↑γ} ⊆
      {x |
        ∀ (a_1 : K⟮X⟯),
          { toCompletion := ↑((WithVal.equiv (valuation K⟮X⟯ (idealX K))).symm a_1) } = x → Valued.v a_1 = Valued.v a}

Tactic:
use Units.mk0 (Valued.v.restrict a) (by simp [Valuation.restrict_def, ha])

Goal state after:
case h
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
⊢ {y | Valued.v.restrict (y - a) < ↑(Units.mk0 (Valued.v.restrict a) ⋯)} ⊆
    {x |
      ∀ (a_1 : K⟮X⟯),
        { toCompletion := ↑((WithVal.equiv (valuation K⟮X⟯ (idealX K))).symm a_1) } = x → Valued.v a_1 = Valued.v a}