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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit ((Ideal.Quotient.mk I) (Polynomial.eval a₀ (derivative f)))
f' : R[X] := derivative f
c : ℕ → R := fun n ↦ Nat.recOn n a₀ fun x b ↦ b - Polynomial.eval b f * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
⊢ ∃ a, f.IsRoot a ∧ a - a₀ ∈ I

Tactic:
have aux : ∀ m n, m ≤ n → c m ≡ c n [SMOD (I ^ m • ⊤ : Ideal R)] := by
        intro m n hmn
        rw [← Ideal.one_eq_top, Ideal.smul_eq_mul, mul_one]
        obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le hmn
        clear hmn
        induction k with
        | zero => rw [add_zero]
        | succ k ih => ?_
        rw [← add_assoc, hc, ← add_zero (c m), sub_eq_add_neg]
        refine ih.add ?_
        symm
        rw [SModEq.zero, Ideal.neg_mem_iff]
        refine Ideal.mul_mem_right _ _ (Ideal.pow_le_pow_right ?_ (hfcI _))
        rw [add_assoc]
        exact le_self_add

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit ((Ideal.Quotient.mk I) (Polynomial.eval a₀ (derivative f)))
f' : R[X] := derivative f
c : ℕ → R := fun n ↦ Nat.recOn n a₀ fun x b ↦ b - Polynomial.eval b f * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
aux : ∀ (m n : ℕ), m ≤ n → c m ≡ c n [SMOD I ^ m • ⊤]
⊢ ∃ a, f.IsRoot a ∧ a - a₀ ∈ I
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
I : Ideal R
inst✝ : Submodule.IsPrincipal I
hp : IsLocalRing.maximalIdeal R ∈ I.minimalPrimes
q : Ideal R
h₁ : q.IsPrime
h₂ : q < IsLocalRing.maximalIdeal R
this : q.height = 0
⊢ q.height < ↑1

Tactic:
rw [this]; exact zero_lt_one

Goal state after:
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
hp : Submodule.IsPrincipal (map (algebraMap R S) p)
this : Disjoint ↑(Submonoid.powers x) ↑p
hpbot : ¬p = ⊥
hi : Function.Injective ⇑(algebraMap R S)
⊢ map (algebraMap R S) p ≠ ⊥

Tactic:
simp [Ideal.map_eq_bot_iff_of_injective hi, hpbot]

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
H : ClosedSubgroup G
g : G
hg : g ∈ sInf {N | IsOpen ↑N ∧ ↑H ≤ N}
hg_not : g ∉ ↑H
U : Set G := (g • ↑H)ᶜ
UOpen : IsOpen U
einU : 1 ∈ U
N : OpenNormalSubgroup G
hN : ↑N ⊆ U
NH : Subgroup G := ↑N.toOpenSubgroup ⊔ ↑H
hg' : g ∈ NH
y : G
hy : y ∈ ↑N.toOpenSubgroup
z : G
hz : z ∈ ↑H
hyz : y * z = g
⊢ False

Tactic:
← eq_mul_inv_iff_mul_eq

Goal state after:
G : Type u_1
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : CompactSpace G
inst✝ : TotallyDisconnectedSpace G
H : ClosedSubgroup G
g : G
hg : g ∈ sInf {N | IsOpen ↑N ∧ ↑H ≤ N}
hg_not : g ∉ ↑H
U : Set G := (g • ↑H)ᶜ
UOpen : IsOpen U
einU : 1 ∈ U
N : OpenNormalSubgroup G
hN : ↑N ⊆ U
NH : Subgroup G := ↑N.toOpenSubgroup ⊔ ↑H
hg' : g ∈ NH
y : G
hy : y ∈ ↑N.toOpenSubgroup
z : G
hz : z ∈ ↑H
hyz : y = g * z⁻¹
⊢ False
Module: Mathlib.RingTheory.Ideal.Pure

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.Pure
x : R
hx : x ∈ I
h : x ∈ I * span {x}
⊢ ∃ y ∈ I, x = x * y

Tactic:
Ideal.mem_mul_span_singleton

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.Pure
x : R
hx : x ∈ I
h : ∃ z ∈ I, z * x = x
⊢ ∃ y ∈ I, x = x * y
Module: Mathlib.RingTheory.Ideal.Pure

Goal state before:
pp: case refine_2
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.Pure
x : R
hx : x ∈ I
p : ↑(zeroLocus ↑I)
⊢ (algebraMap R (Localization.AtPrime (↑p).asIdeal)) x = 0

Tactic:
exact Ideal.le_ker_atPrime_of_forall_exists_eq_mul
      (fun x hx ↦ Ideal.exists_eq_mul_of_pure hx) p.2 hx

Goal state after:
Module: Mathlib.RingTheory.KrullDimension.PID

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsPrincipalIdealRing R
I : Ideal R
hI : I.IsPrime
P : Ideal R
hlt : P < I
hP : P.IsPrime
this✝ : IsPrincipalIdealRing (R ⧸ P)
this : (Ideal.map (Ideal.Quotient.mk P) I).IsPrime
⊢ (Ideal.map (Ideal.Quotient.mk P) I).IsMaximal

Tactic:
refine IsPrime.to_maximal_ideal ?_

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsPrincipalIdealRing R
I : Ideal R
hI : I.IsPrime
P : Ideal R
hlt : P < I
hP : P.IsPrime
this✝ : IsPrincipalIdealRing (R ⧸ P)
this : (Ideal.map (Ideal.Quotient.mk P) I).IsPrime
⊢ Ideal.map (Ideal.Quotient.mk P) I ≠ ⊥
Module: Mathlib.RingTheory.KrullDimension.PID

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsPrincipalIdealRing R
I : Ideal R
hI : I.IsPrime
P : Ideal R
hlt : P < I
hP : P.IsPrime
this✝ : IsPrincipalIdealRing (R ⧸ P)
this : (Ideal.map (Ideal.Quotient.mk P) I).IsMaximal
⊢ I.IsMaximal

Tactic:
have := Ideal.comap_isMaximal_of_surjective (Ideal.Quotient.mk P) Ideal.Quotient.mk_surjective
    (K := I.map (Ideal.Quotient.mk P))

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsPrincipalIdealRing R
I : Ideal R
hI : I.IsPrime
P : Ideal R
hlt : P < I
hP : P.IsPrime
this✝¹ : IsPrincipalIdealRing (R ⧸ P)
this✝ : (Ideal.map (Ideal.Quotient.mk P) I).IsMaximal
this : (Ideal.comap (Ideal.Quotient.mk P) (Ideal.map (Ideal.Quotient.mk P) I)).IsMaximal
⊢ I.IsMaximal
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: case e'_4
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
p : Ideal R
inst✝ : p.IsPrime
I : Ideal R
hI : p ∈ I.minimalPrimes
hr : Submodule.spanRank I ≤ ↑p.height
hs : (Submodule.generators I).Finite
⊢ ↑(Submodule.spanFinrank I) = Cardinal.toENat (Submodule.spanRank I)

Tactic:
symm

Goal state after:
case e'_4
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
p : Ideal R
inst✝ : p.IsPrime
I : Ideal R
hI : p ∈ I.minimalPrimes
hr : Submodule.spanRank I ≤ ↑p.height
hs : (Submodule.generators I).Finite
⊢ Cardinal.toENat (Submodule.spanRank I) = ↑(Submodule.spanFinrank I)
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
I p : Ideal R
inst✝ : p.IsPrime
hrp : I ≤ p
p' : Ideal (R ⧸ I) := map (algebraMap R (R ⧸ I)) p
this✝ : p'.IsPrime
s : Finset (R ⧸ I)
hps : p' ∈ (span ↑s).minimalPrimes
hs : ↑s.card = p'.height
hsp' : ↑s ⊆ ↑p'
this : Set.SurjOn ⇑(Quotient.mk I) ↑p ↑s
o : Finset R
hsubset : ↑o ⊆ ↑p
ho : Set.InjOn ⇑(Quotient.mk I) ↑o
himgo : Finset.image (⇑(Quotient.mk I)) o = s
hI : I.FG
t : Finset R := o ∪ ⋯.toFinset
h : p.height ≤ ↑t.card
⊢ p.height ≤ (map (Quotient.mk I) p).height + ↑(Submodule.spanFinrank I)

Tactic:
by
    refine le_trans h (hs ▸ ?_)
    norm_cast
    have : (Submodule.FG.finite_generators hI).toFinset.card = I.spanFinrank := by
      rw [← Set.ncard_eq_toFinset_card (hs := Submodule.FG.finite_generators hI)]
      exact Submodule.FG.generators_ncard hI
    grind

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I : Ideal R
h : I ≤ Ring.jacobson R
a✝ : Nontrivial R
⊢ ∀ ⦃m : Ideal R⦄, m.IsMaximal → ↑m.height ≤ ringKrullDim (R ⧸ I) + ↑(Submodule.spanFinrank I)

Tactic:
intro m hm

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I : Ideal R
h : I ≤ Ring.jacobson R
a✝ : Nontrivial R
m : Ideal R
hm : m.IsMaximal
⊢ ↑m.height ≤ ringKrullDim (R ⧸ I) + ↑(Submodule.spanFinrank I)
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : IsNoetherianRing R
S : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsNoetherianRing S
p : Ideal R
inst✝² : p.IsPrime
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : P.LiesOver p
s : Finset R
hp : p ∈ (span ↑s).minimalPrimes
heq : ↑s.card = p.height
P' : Ideal (S ⧸ map (algebraMap R S) p) := map (Quotient.mk (map (algebraMap R S) p)) P
s' : Finset (S ⧸ map (algebraMap R S) p)
hP' : P' ∈ (span ↑s').minimalPrimes
heq' : ↑s'.card = P'.height
hsP'sub : ↑s' ⊆ ↑P'
this : Set.SurjOn ⇑(Quotient.mk (map (algebraMap R S) p)) ↑P ↑s'
o : Finset S
ho : ↑o ⊆ ↑P
hinj : Set.InjOn ⇑(Quotient.mk (map (algebraMap R S) p)) ↑o
himgo : Finset.image (⇑(Quotient.mk (map (algebraMap R S) p))) o = s'
t : Finset S := Finset.image (⇑(algebraMap R S)) s ∪ o
h : P.height ≤ ↑t.card
⊢ P.height ≤ p.height + (map (Quotient.mk (map (algebraMap R S) p)) P).height

Tactic:
by
    rw [← heq, ← heq']
    apply le_trans h
    norm_cast
    refine le_trans (Finset.card_union_le _ _) (add_le_add Finset.card_image_le ?_)
    rw [← himgo, Finset.card_image_of_injOn hinj]

Goal state after:
Module: Mathlib.RingTheory.LittleWedderburn

Goal state before:
pp: case intro
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
hD : InductionHyp D
val✝ : Fintype D
Z : Subring D := Subring.center D
hZ : Z ≠ ⊤
⊢ False

Tactic:
let : Field Z := hD.field hZ.lt_top

Goal state after:
case intro
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
hD : InductionHyp D
val✝ : Fintype D
Z : Subring D := Subring.center D
hZ : Z ≠ ⊤
this : Field ↥Z := hD.field ⋯
⊢ False
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: case neg
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
S : Submonoid R := ⨅ q ∈ s₀, (↑q).primeCompl
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
hp : p ∉ s₀
hq : ¬↑(q.colon Set.univ) ⊆ ⋃ r ∈ s₀, ↑↑r
y : R
hy1 : y ∈ ↑(q.colon Set.univ)
hy2 : y ∈ S
⊢ comap (mkLinearMap S M) (localized₀ S (mkLinearMap S M) q) = ⊤

Tactic:
eq_top_iff,

Goal state after:
case neg
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
S : Submonoid R := ⨅ q ∈ s₀, (↑q).primeCompl
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
hp : p ∉ s₀
hq : ¬↑(q.colon Set.univ) ⊆ ⋃ r ∈ s₀, ↑↑r
y : R
hy1 : y ∈ ↑(q.colon Set.univ)
hy2 : y ∈ S
⊢ ⊤ ≤ comap (mkLinearMap S M) (localized₀ S (mkLinearMap S M) q)
Module: Mathlib.RingTheory.LocalIso

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
ι : Type u_3
f : ι → S
h✝ : Ideal.span (Set.range f) = ⊤
T : ι → Type u_4
inst✝⁵ : (i : ι) → CommSemiring (T i)
inst✝⁴ : (i : ι) → Algebra R (T i)
inst✝³ : (i : ι) → Algebra S (T i)
inst✝² : ∀ (i : ι), IsScalarTower R S (T i)
inst✝¹ : ∀ (i : ι), IsLocalization.Away (f i) (T i)
inst✝ : ∀ (i : ι), IsLocalIso R (T i)
q : Ideal S
hq : q.IsPrime
i : ι
hi : f i ∉ q
q' : PrimeSpectrum (T i)
hq' : PrimeSpectrum.comap (algebraMap S (T i)) q' = { asIdeal := q, isPrime := hq }
g' : T i
hg' : g' ∉ q'.asIdeal
h : IsStandardOpenImmersion R (Localization.Away g')
n : ℕ
g : S
hg : g' * (algebraMap S (T i)) (f i) ^ n = (algebraMap S (T i)) g
this : IsLocalization.Away g' (Localization.Away ((algebraMap S (T i)) g))
e₁ : Localization.Away ((algebraMap S (T i)) g) ≃ₐ[S] Localization.Away (g * f i) :=
  IsLocalization.algEquiv (Submonoid.powers (g * f i)) (Localization.Away ((algebraMap S (T i)) g))
    (Localization.Away (g * f i))
e₂ : Localization.Away g' ≃ₐ[R] Localization.Away (g * f i) :=
  (AlgEquiv.restrictScalars R
        (IsLocalization.algEquiv (Submonoid.powers g') (Localization.Away g')
          (Localization.Away ((algebraMap S (T i)) g)))).trans
    (AlgEquiv.restrictScalars R e₁)
⊢ IsStandardOpenImmersion R (Localization.Away (g * f i))

Tactic:
exact .of_algEquiv e₂

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

Goal state before:
pp: case h
R : Type u_1
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Finite (MaximalSpectrum R)
M : Type u_2
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_3
inst✝⁷ : (P : Ideal R) → [inst : P.IsMaximal] → CommSemiring (Rₚ P)
inst✝⁶ : (P : Ideal R) → [inst : P.IsMaximal] → Algebra R (Rₚ P)
inst✝⁵ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_4
inst✝⁴ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝³ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → Module (Rₚ P) (Mₚ P)
inst✝¹ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsScalarTower R (Rₚ P) (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
H : ∀ (P : Ideal R) [inst : P.IsMaximal], Module.Finite (Rₚ P) (Mₚ P)
this : Fintype (MaximalSpectrum R)
s : (P : MaximalSpectrum R) → Finset (Mₚ P.asIdeal)
hs : ∀ (P : MaximalSpectrum R), Submodule.span (Rₚ P.asIdeal) ↑(s P) = ⊤
frac : (P : MaximalSpectrum R) → Mₚ P.asIdeal → M × ↥P.asIdeal.primeCompl
hfrac : ∀ (P : MaximalSpectrum R) (y : Mₚ P.asIdeal), (frac P y).2 • y = (f P.asIdeal) (frac P y).1
P : Ideal R
hP : P.IsMaximal
⊢ Submodule.localized' (Rₚ P) P.primeCompl (f P)
      (Submodule.span R ↑(Finset.univ.biUnion fun P ↦ Finset.image (fun x ↦ (frac P x).1) (s P))) =
    ⊤

Tactic:
eq_top_iff,

Goal state after:
case h
R : Type u_1
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Finite (MaximalSpectrum R)
M : Type u_2
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_3
inst✝⁷ : (P : Ideal R) → [inst : P.IsMaximal] → CommSemiring (Rₚ P)
inst✝⁶ : (P : Ideal R) → [inst : P.IsMaximal] → Algebra R (Rₚ P)
inst✝⁵ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_4
inst✝⁴ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝³ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → Module (Rₚ P) (Mₚ P)
inst✝¹ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsScalarTower R (Rₚ P) (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
H : ∀ (P : Ideal R) [inst : P.IsMaximal], Module.Finite (Rₚ P) (Mₚ P)
this : Fintype (MaximalSpectrum R)
s : (P : MaximalSpectrum R) → Finset (Mₚ P.asIdeal)
hs : ∀ (P : MaximalSpectrum R), Submodule.span (Rₚ P.asIdeal) ↑(s P) = ⊤
frac : (P : MaximalSpectrum R) → Mₚ P.asIdeal → M × ↥P.asIdeal.primeCompl
hfrac : ∀ (P : MaximalSpectrum R) (y : Mₚ P.asIdeal), (frac P y).2 • y = (f P.asIdeal) (frac P y).1
P : Ideal R
hP : P.IsMaximal
⊢ ⊤ ≤
    Submodule.localized' (Rₚ P) P.primeCompl (f P)
      (Submodule.span R ↑(Finset.univ.biUnion fun P ↦ Finset.image (fun x ↦ (frac P x).1) (s P)))
Module: Mathlib.RingTheory.LocalProperties.Semilocal

Goal state before:
pp: R : Type u_1
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Finite (MaximalSpectrum R)
M : Type u_2
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_3
inst✝⁷ : (P : Ideal R) → [inst : P.IsMaximal] → CommSemiring (Rₚ P)
inst✝⁶ : (P : Ideal R) → [inst : P.IsMaximal] → Algebra R (Rₚ P)
inst✝⁵ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_4
inst✝⁴ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝³ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → Module (Rₚ P) (Mₚ P)
inst✝¹ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsScalarTower R (Rₚ P) (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
H : ∀ (P : Ideal R) [inst : P.IsMaximal], Module.Finite (Rₚ P) (Mₚ P)
this : Fintype (MaximalSpectrum R)
s : (P : MaximalSpectrum R) → Finset (Mₚ P.asIdeal)
hs : ∀ (P : MaximalSpectrum R), Submodule.span (Rₚ P.asIdeal) ↑(s P) = ⊤
frac : (P : MaximalSpectrum R) → Mₚ P.asIdeal → M × ↥P.asIdeal.primeCompl
hfrac : ∀ (P : MaximalSpectrum R) (y : Mₚ P.asIdeal), (frac P y).2 • y = (f P.asIdeal) (frac P y).1
P : Ideal R
hP : P.IsMaximal
x : ↥(s { asIdeal := P, isMaximal := hP })
⊢ (frac { asIdeal := P, isMaximal := hP } ↑x).1 ∈
    ↑(Finset.univ.biUnion fun P ↦ Finset.image (fun x ↦ (frac P x).1) (s P))

Tactic:
simpa using ⟨_, _, x.2, rfl⟩

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

Goal state before:
pp: case 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✝ : Etale R S
β : S
hadj : R[β] = ⊤
h : (minpoly R β).Monic
⊢ (aeval ((residue S) β)) (map (residue R) (minpoly R β)) = 0

pp: case 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✝ : Etale R S
β : S
hadj : R[β] = ⊤
h : (minpoly R β).Monic
⊢ (map (residue R) (minpoly R β)).natDegree ≤ (minpoly (ResidueField R) ((residue S) β)).natDegree

Tactic:
· rw [← map_aeval_eq_aeval_map (ψ := residue S) (φ := residue R) rfl]
    simp

Goal state after:
case 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✝ : Etale R S
β : S
hadj : R[β] = ⊤
h : (minpoly R β).Monic
⊢ (map (residue R) (minpoly R β)).natDegree ≤ (minpoly (ResidueField R) ((residue S) β)).natDegree
Module: Mathlib.RingTheory.MvPolynomial.EulerIdentity

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
i : σ
h : φ.IsHomogeneous n
⊢ ((pderiv i) φ).IsHomogeneous (n - 1)

Tactic:
by
  obtain _ | n := n
  · rw [← totalDegree_zero_iff_isHomogeneous, totalDegree_eq_zero_iff_eq_C] at h
    rw [h, pderiv_C]; apply isHomogeneous_zero
  · exact IsWeightedHomogeneous.pderiv h rfl

Goal state after:
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 (iterateFrobenius R p (k + 1))) ((expand (p ^ (k + 1))) f) = f ^ p ^ (k + 1)

Tactic:
symm

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
⊢ f ^ p ^ (k + 1) = (map (iterateFrobenius R p (k + 1))) ((expand (p ^ (k + 1))) f)
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case inl
n m : ℕ
hnm : n ≤ m
t s : Fin n → ℕ
he : (accumulate n m) t = (accumulate n m) s
i : Fin n
h : ↑i + 1 < m
this : (accumulate n m) s ⟨↑i, ⋯⟩ = s ⟨↑i, ⋯⟩ + (accumulate n m) s ⟨↑i + 1, h⟩
⊢ t i = s i

Tactic:
rwa [← he, accumulate_rec i.2 h t, add_right_cancel_iff] at this

Goal state after:
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
k : σ
hk : (fun x1 x2 ↦ x1 < x2) k i
| (Finsupp.mapDomain (⇑(Equiv.swap i j)) (ofLex (supDegree (⇑toLex) p))) k

Tactic:
← Equiv.swap_apply_of_ne_of_ne hk.ne (hk.trans_le hle).ne

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
k : σ
hk : (fun x1 x2 ↦ x1 < x2) k i
| (Finsupp.mapDomain (⇑(Equiv.swap i j)) (ofLex (supDegree (⇑toLex) p))) ((Equiv.swap i j) k)
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case mpr.refine_1
K : Type u_2
inst✝ : Field K
S : Set (K⟮X⟯ × K⟮X⟯)
w✝ : Set K⟮X⟯
hT : w✝ ∈ nhds 0
pre_T : (fun x ↦ x.2 - x.1) ⁻¹' w✝ ⊆ S
d : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ
hd : {y | Valued.v.restrict (y - 0) < ↑d} ⊆ w✝
X : Set K⸨X⸩ := {f | Valued.v f < embedding ↑d}
X_def : X = {f | Valued.v f < embedding ↑d}
x : K⟮X⟯
hx : (restrict₀ (MonoidWithZeroHom.ofClass Valued.v)) x = ↑d
⊢ ∃ γ, {y | Valued.v y < embedding ↑γ} ⊆ X

Tactic:
use Units.mk0 (Valued.v.restrict (x : K⸨X⸩)) (by
          simp only [ne_eq, map_eq_zero]
          intro h
          simp only [h, map_zero] at hx
          exact Units.ne_zero _ hx.symm)

Goal state after:
case h
K : Type u_2
inst✝ : Field K
S : Set (K⟮X⟯ × K⟮X⟯)
w✝ : Set K⟮X⟯
hT : w✝ ∈ nhds 0
pre_T : (fun x ↦ x.2 - x.1) ⁻¹' w✝ ⊆ S
d : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ
hd : {y | Valued.v.restrict (y - 0) < ↑d} ⊆ w✝
X : Set K⸨X⸩ := ⋯
X_def : X = {f | Valued.v f < embedding ↑d}
x : K⟮X⟯
hx : (restrict₀ (MonoidWithZeroHom.ofClass Valued.v)) x = ↑d
⊢ {y | Valued.v y < embedding ↑(Units.mk0 (Valued.v.restrict ((algebraMap K⟮X⟯ K⸨X⸩) x)) ⋯)} ⊆ X
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

Goal state before:
pp: σ : Type u_1
inst✝¹ : Fintype σ
R : Type u_2
inst✝ : CommRing R
k : ℕ
⊢ (-1) ^ (k + 1) * ∑ x ∈ NewtonIdentities.pairs σ k, NewtonIdentities.weight σ R k x = 0

Tactic:
NewtonIdentities.weight_sum σ R k,

Goal state after:
σ : Type u_1
inst✝¹ : Fintype σ
R : Type u_2
inst✝ : CommRing R
k : ℕ
⊢ (-1) ^ (k + 1) * 0 = 0
Module: Mathlib.RingTheory.Morita.Matrix

Goal state before:
pp: R : Type u
ι : Type v
inst✝² : Ring R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : ModuleCat (Matrix ι ι R)
j : ι
v : ι → ↥(toModuleCatObj R (↑M) j)
i : ι
⊢ ?m.237

Tactic:
simpa [-SetLike.coe_mem] using (v i).2

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 (iterateFrobenius R p (k + 1))) ((expand (p ^ (k + 1)) ⋯) f) = f ^ p ^ (k + 1)

Tactic:
symm

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
⊢ f ^ p ^ (k + 1) = (map (iterateFrobenius R p (k + 1))) ((expand (p ^ (k + 1)) ⋯) f)
Module: Mathlib.RingTheory.NoetherNormalization

Goal state before:
pp: k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v w : Fin (n + 1) →₀ ℕ
hv : v ∈ f.support
hw : w ∈ f.support
ne : v ≠ w
⊢ degreeOf 0 ((T f) ((MvPolynomial.monomial v) (MvPolynomial.coeff v f))) ≠
    degreeOf 0 ((T f) ((MvPolynomial.monomial w) (MvPolynomial.coeff w f)))

Tactic:
degreeOf_zero_t _ _ <| mem_support_iff.mp hv,

Goal state after:
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v w : Fin (n + 1) →₀ ℕ
hv : v ∈ f.support
hw : w ∈ f.support
ne : v ≠ w
⊢ ∑ i, r i * v i ≠ degreeOf 0 ((T f) ((MvPolynomial.monomial w) (MvPolynomial.coeff w f)))
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝ : CommRing R
hp : NeZero p
n : ℕ
⊢ ((map (Int.castRingHom R)) (W_ ℤ n)).vars ⊆ range (n + 1)

Tactic:
← wittPolynomial_vars p ℤ

Goal state after:
p : ℕ
R : Type u_1
inst✝ : CommRing R
hp : NeZero p
n : ℕ
⊢ ((map (Int.castRingHom R)) (W_ ℤ n)).vars ⊆ (W_ ℤ n).vars