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

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
r : R
h : Function.Injective ⇑(DistribSMul.toLinearMap R M r)
⊢ IsSMulRegular (M ⧸ N) r ↔ r • ⊤ ⊓ N ≤ r • N

Tactic:
rw [isSMulRegular_on_quot_iff_lsmul_comap_le, ← map_le_map_iff_of_injective h,
    ← LinearMap.lsmul_eq_distribSMultoLinearMap,
    map_comap_eq, LinearMap.range_eq_map]

Goal state after:
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
r : R
h : Function.Injective ⇑(DistribSMul.toLinearMap R M r)
⊢ map ((LinearMap.lsmul R M) r) ⊤ ⊓ N ≤ map ((LinearMap.lsmul R M) r) N ↔ r • ⊤ ⊓ N ≤ r • N
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization

Goal state before:
pp: case refine_1
R : Type u_1
inst✝⁹ : CommRing R
S : Submonoid R
R' : Type u_2
inst✝⁸ : CommRing R'
inst✝⁷ : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
f : M →ₗ[R] M'
inst✝² : IsLocalizedModule S f
inst✝¹ : Module R' M'
inst✝ : IsScalarTower R R' M'
p : Ideal R'
hp : p.IsPrime
T : Finset R
hT : Ideal.span ↑T = Ideal.comap (algebraMap R R') p
m : M
s : ↥S
hx : p = (⊥.colon {IsLocalizedModule.mk' f m s}).radical
e : ↥T → ℕ
g : ↥T → ↥S
hg : ∀ (a : ↥T), g a • ↑a ^ e a • m = 0
⊢ Ideal.comap (algebraMap R R') p ≤ (⊥.colon {↑(∏ a, g a) • m}).radical

Tactic:
← hT,

Goal state after:
case refine_1
R : Type u_1
inst✝⁹ : CommRing R
S : Submonoid R
R' : Type u_2
inst✝⁸ : CommRing R'
inst✝⁷ : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
f : M →ₗ[R] M'
inst✝² : IsLocalizedModule S f
inst✝¹ : Module R' M'
inst✝ : IsScalarTower R R' M'
p : Ideal R'
hp : p.IsPrime
T : Finset R
hT : Ideal.span ↑T = Ideal.comap (algebraMap R R') p
m : M
s : ↥S
hx : p = (⊥.colon {IsLocalizedModule.mk' f m s}).radical
e : ↥T → ℕ
g : ↥T → ↥S
hg : ∀ (a : ↥T), g a • ↑a ^ e a • m = 0
⊢ Ideal.span ↑T ≤ (⊥.colon {↑(∏ a, g a) • m}).radical
Module: Mathlib.RingTheory.Regular.LinearMap

Goal state before:
pp: case inr
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : IsNoetherianRing R
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R N
hom0 : Subsingleton (N →ₗ[R] M)
h✝ : Nontrivial M
h : ∀ r ∈ annihilator R N, ¬IsSMulRegular M r
p : Ideal R
pass : p ∈ associatedPrimes R M
hp : annihilator R N ≤ p
x✝ : p.IsPrime := IsAssociatedPrime.isPrime pass
p' : PrimeSpectrum R := { asIdeal := p, isPrime := ⋯ }
loc_ne_zero : Nontrivial (LocalizedModule p'.asIdeal.primeCompl N)
Rₚ : Type u_1 := Localization.AtPrime p
Nₚ : Type (max u_1 u_3) := LocalizedModule.AtPrime p'.asIdeal N
Mₚ : Type (max u_1 u_2) := LocalizedModule.AtPrime p'.asIdeal M
Nₚ' : Type (max u_1 u_3) := Nₚ ⧸ maximalIdeal (Localization.AtPrime p) • ⊤
ntr : Nontrivial Nₚ'
Mₚ' : Type (max u_1 u_2) := Mₚ ⧸ maximalIdeal (Localization.AtPrime p) • ⊤
⊢ False

Tactic:
let _ : Module p.ResidueField Nₚ' :=
      Module.instQuotientIdealSubmoduleHSMulTop Nₚ (maximalIdeal (Localization.AtPrime p))

Goal state after:
case inr
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : IsNoetherianRing R
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R N
hom0 : Subsingleton (N →ₗ[R] M)
h✝ : Nontrivial M
h : ∀ r ∈ annihilator R N, ¬IsSMulRegular M r
p : Ideal R
pass : p ∈ associatedPrimes R M
hp : annihilator R N ≤ p
x✝¹ : p.IsPrime := IsAssociatedPrime.isPrime pass
p' : PrimeSpectrum R := { asIdeal := p, isPrime := ⋯ }
loc_ne_zero : Nontrivial (LocalizedModule p'.asIdeal.primeCompl N)
Rₚ : Type u_1 := Localization.AtPrime p
Nₚ : Type (max u_1 u_3) := LocalizedModule.AtPrime p'.asIdeal N
Mₚ : Type (max u_1 u_2) := LocalizedModule.AtPrime p'.asIdeal M
Nₚ' : Type (max u_1 u_3) := Nₚ ⧸ maximalIdeal (Localization.AtPrime p) • ⊤
ntr : Nontrivial Nₚ'
Mₚ' : Type (max u_1 u_2) := Mₚ ⧸ maximalIdeal (Localization.AtPrime p) • ⊤
x✝ : Module p.ResidueField Nₚ' := instQuotientIdealSubmoduleHSMulTop Nₚ (maximalIdeal (Localization.AtPrime p))
⊢ False
Module: Mathlib.RingTheory.Regular.RegularSequence

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
rs : List R
⊢ (IsSMulRegular M r ∧ IsWeaklyRegular (QuotSMulTop r M) (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r}))) rs)) ∧
      ¬⊤ = Ideal.ofList (r :: rs) • ⊤ ↔
    IsSMulRegular M r ∧
      IsWeaklyRegular (QuotSMulTop r M) (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r}))) rs) ∧
        ¬⊤ = Ideal.ofList (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r}))) rs) • ⊤

Tactic:
← restrictScalars_inj R (R ⧸ _),

Goal state after:
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
rs : List R
⊢ (IsSMulRegular M r ∧ IsWeaklyRegular (QuotSMulTop r M) (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r}))) rs)) ∧
      ¬⊤ = Ideal.ofList (r :: rs) • ⊤ ↔
    IsSMulRegular M r ∧
      IsWeaklyRegular (QuotSMulTop r M) (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r}))) rs) ∧
        ¬restrictScalars R ⊤ =
            restrictScalars R (Ideal.ofList (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r}))) rs) • ⊤)
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
h : ∀ (I : Ideal R), I.IsMaximal → IsNilpotent I
a : TrivSqZeroExt R M
ha : ¬IsUnit a.fst
I : Ideal R
hI : I.IsMaximal
haI : a.fst ∈ I
⊢ IsNilpotent a.fst

Tactic:
refine (h _ hI).imp fun n hn ↦ ?_

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
h : ∀ (I : Ideal R), I.IsMaximal → IsNilpotent I
a : TrivSqZeroExt R M
ha : ¬IsUnit a.fst
I : Ideal R
hI : I.IsMaximal
haI : a.fst ∈ I
n : ℕ
hn : I ^ n = 0
⊢ a.fst ^ n = 0
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
x : K[ε]
hxI : x ∈ I
hx0 : x ≠ 0
⊢ ∃ r, ε = r * x

Tactic:
obtain ⟨r, rfl⟩ := hd _ hxI

Goal state after:
K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
r : K[ε]
hxI : ε * r ∈ I
hx0 : ε * r ≠ 0
⊢ ∃ r_1, ε = r_1 * (ε * r)
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
x✝ : ℕ
hn : x✝ ≠ 0
x : A
hx : x ∈ hI.dpEqualizer hI'
m : ℕ
⊢ ↑(m.uniformBell x✝) * hI'.dpow (m * x✝) x = hI'.dpow m (hI'.dpow x✝ x)

Tactic:
hI'.dpow_comp hn hx.1

Goal state after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
x✝ : ℕ
hn : x✝ ≠ 0
x : A
hx : x ∈ hI.dpEqualizer hI'
m : ℕ
⊢ ↑(m.uniformBell x✝) * hI'.dpow (m * x✝) x = ↑(m.uniformBell x✝) * hI'.dpow (m * x✝) x
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective ⇑f
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
m✝ n✝ : ℕ
a : A
ha : a ∈ I
hx : f a ∈ J
⊢ f (hI.dpow m✝ a) * f (hI.dpow n✝ a) = ↑((m✝ + n✝).choose m✝) * f (hI.dpow (m✝ + n✝) a)

Tactic:
rw [← _root_.map_mul, hI.mul_dpow ha, _root_.map_mul, map_natCast]

Goal state after:
Module: Mathlib.RingTheory.Grassmannian

Goal state before:
pp: R : Type u
inst✝⁸ : CommRing R
M : Type v
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
k : ℕ
A : Type w
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
B : Type w
inst✝³ : CommRing B
inst✝² : Algebra R B
f✝ : A →ₐ[R] B
C : Type w
inst✝¹ : CommRing C
inst✝ : Algebra R C
g✝ : B →ₐ[R] C
X✝ Y✝ Z✝ : CommAlgCat R
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ ↾map (CommAlgCat.Hom.hom (f ≫ g)) = ↾map (CommAlgCat.Hom.hom f) ≫ ↾map (CommAlgCat.Hom.hom g)

Tactic:
by ext N : 1; exact map_comp k f.hom g.hom N

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

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

Tactic:
· rw [coeff_hsum, finsum_eq_zero_of_forall_eq_zero
      fun n ↦ (by by_cases hn : n = 0 <;> simp [hg, hn])]
    simp [hg]

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

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝⁴ : LinearOrder Γ
inst✝³ : AddCommMonoid Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : CommRing R
inst✝ : BinomialRing R
x : ↥(orderTopSubOnePos Γ R)
r s : R
this : ↑(x ^ (r + s)) = ↑(x ^ r * x ^ s)
⊢ x ^ (r + s) = x ^ r * x ^ s

Tactic:
by exact SetLike.coe_eq_coe.mp this

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

Goal state before:
pp: case neg
Γ : Type u_1
R : Type u_2
inst✝⁴ : AddCancelCommMonoid Γ
inst✝³ : LinearOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : Ring R
inst✝ : IsDomain R
x y : R⟦Γ⟧
hx : ¬x = 0
hy : ¬y = 0
⊢ (x * y).order = x.order + y.order

Tactic:
order_mul hx hy

Goal state after:
case neg
Γ : Type u_1
R : Type u_2
inst✝⁴ : AddCancelCommMonoid Γ
inst✝³ : LinearOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : Ring R
inst✝ : IsDomain R
x y : R⟦Γ⟧
hx : ¬x = 0
hy : ¬y = 0
⊢ x.order + y.order = x.order + y.order
Module: Mathlib.RingTheory.Ideal.HasGoingUp

Goal state before:
pp: case refine_1
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : HasGoingUp R S
P : PrimeSpectrum S
q : PrimeSpectrum R
hq : flip (fun x1 x2 ↦ x1 ⤳ x2) q (PrimeSpectrum.comap (algebraMap R S) P)
⊢ ∃ a', flip (fun x1 x2 ↦ x1 ⤳ x2) a' P ∧ PrimeSpectrum.comap (algebraMap R S) a' = q

Tactic:
simp only [flip] at hq

Goal state after:
case refine_1
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : HasGoingUp R S
P : PrimeSpectrum S
q : PrimeSpectrum R
hq : PrimeSpectrum.comap (algebraMap R S) P ⤳ q
⊢ ∃ a', flip (fun x1 x2 ↦ x1 ⤳ x2) a' P ∧ PrimeSpectrum.comap (algebraMap R S) a' = q
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')
n : ℕ
ih : Polynomial.eval (c n) f ∈ I ^ (n + 1)
i : ℕ
h2i : 2 ≤ i
right✝ : i < ((taylor (c n)) f).natDegree + 2
⊢ n + 2 ≤ i * (n + 1)

Tactic:
trans 2 * (n + 1) <;> nlinarith only [h2i]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
x : PrimeSpectrum A
hx : ∃ m, ∀ (r : A), r • m = 0 → r ∈ x.asIdeal
⊢ ∃ m, ∀ (r : R), r • m = 0 → (algebraMap R A) r ∈ x.asIdeal

Tactic:
obtain ⟨m, hm⟩ := hx

Goal state after:
R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
x : PrimeSpectrum A
m : M
hm : ∀ (r : A), r • m = 0 → r ∈ x.asIdeal
⊢ ∃ m, ∀ (r : R), r • m = 0 → (algebraMap R A) r ∈ x.asIdeal
Module: Mathlib.RingTheory.KrullDimension.Polynomial

Goal state before:
pp: case refine_1
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
⊢ ringKrullDim R[X] ≤ ringKrullDim R + 1

Tactic:
nontriviality R[X]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
a✝ : Nontrivial R[X]
⊢ ringKrullDim R[X] ≤ ringKrullDim R + 1
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: case refine_1
R : Type u_1
inst✝⁸ : CommRing R
inst✝⁷ : IsNoetherianRing R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsNoetherianRing S
inst✝³ : Algebra.HasGoingDown R S
p : Ideal R
inst✝² : p.IsPrime
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : P.LiesOver p
lp : LTSeries (PrimeSpectrum R)
hlp : RelSeries.last lp = { asIdeal := p, isPrime := ⋯ }
hlenp : ↑lp.length = p.height
lq : LTSeries (PrimeSpectrum (S ⧸ map (algebraMap R S) p))
hlq : RelSeries.last lq = { asIdeal := map (Quotient.mk (map (algebraMap R S) p)) P, isPrime := ⋯ }
hlenq : ↑lq.length = (map (Quotient.mk (map (algebraMap R S) p)) P).height
l' : LTSeries (PrimeSpectrum S) := lq.map (PrimeSpectrum.comap (Quotient.mk (map (algebraMap R S) p))) ⋯
⊢ map (algebraMap R S) p ≤ comap (Quotient.mk (map (algebraMap R S) p)) (RelSeries.head lq).asIdeal

Tactic:
← map_le_iff_le_comap

Goal state after:
case refine_1
R : Type u_1
inst✝⁸ : CommRing R
inst✝⁷ : IsNoetherianRing R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsNoetherianRing S
inst✝³ : Algebra.HasGoingDown R S
p : Ideal R
inst✝² : p.IsPrime
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : P.LiesOver p
lp : LTSeries (PrimeSpectrum R)
hlp : RelSeries.last lp = { asIdeal := p, isPrime := ⋯ }
hlenp : ↑lp.length = p.height
lq : LTSeries (PrimeSpectrum (S ⧸ map (algebraMap R S) p))
hlq : RelSeries.last lq = { asIdeal := map (Quotient.mk (map (algebraMap R S) p)) P, isPrime := ⋯ }
hlenq : ↑lq.length = (map (Quotient.mk (map (algebraMap R S) p)) P).height
l' : LTSeries (PrimeSpectrum S) := lq.map (PrimeSpectrum.comap (Quotient.mk (map (algebraMap R S) p))) ⋯
⊢ map (Quotient.mk (map (algebraMap R S) p)) (map (algebraMap R S) p) ≤ (RelSeries.head lq).asIdeal
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 : f n = N ∨ N + a ^ n • ⊤ = N
⊢ b ∈ N ∨ ∃ n, a ^ n • ⊤ ≤ N

Tactic:
add_eq_sup,

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 : f n = N ∨ N ⊔ a ^ n • ⊤ = N
⊢ b ∈ N ∨ ∃ n, a ^ n • ⊤ ≤ N
Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension

Goal state before:
pp: case succ
R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
S : Submonoid R
this : Small.{v, u} (Localization S)
n : ℕ
ih : ∀ (M : ModuleCat R) [HasProjectiveDimensionLE M n], HasProjectiveDimensionLE (M.localizedModule S) n
M : ModuleCat R
inst✝ : HasProjectiveDimensionLE M (n + 1)
⊢ HasProjectiveDimensionLE (M.localizedModule S) (n + 1)

Tactic:
rcases ModuleCat.enoughProjectives.1 M with ⟨⟨P, f⟩⟩
    let T := ShortComplex.mk (kernel.ι f) f (kernel.condition f)
    have T_exact : T.ShortExact := { exact := ShortComplex.exact_kernel f }
    let TS := T.map (ModuleCat.localizedModuleFunctor S)
    have TS_exact : TS.ShortExact := T_exact.map_of_exact (ModuleCat.localizedModuleFunctor S)
    have : Projective TS.X₂ := (ModuleCat.localizedModuleFunctor.{v} S).projective_obj _
    have := (T_exact.hasProjectiveDimensionLT_X₃_iff n ‹_›).mp ‹_›
    exact (TS_exact.hasProjectiveDimensionLT_X₃_iff n ‹_›).mpr (ih (kernel f))

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case neg
K : Type u_2
inst✝ : Field K
P : K[X]
hP : ¬P = 0
span_ne_zero : Ideal.span {P} ≠ 0 ∧ Ideal.span {Polynomial.X} ≠ 0
span_ne_zero' : Ideal.span {↑P} ≠ 0 ∧ (idealX K).asIdeal ≠ 0
⊢ (Associates.mk (Ideal.span {Polynomial.X})).count (Associates.mk (Ideal.span {P})).factors =
    (Associates.mk (idealX K).asIdeal).count (Associates.mk (Ideal.span {↑P})).factors

Tactic:
classical
  rw [Ideal.count_associates_factors_eq span_ne_zero.1
    (Ideal.span_singleton_prime Polynomial.X_ne_zero |>.mpr prime_X) span_ne_zero.2,
    Ideal.count_associates_factors_eq]
  on_goal 1 => convert! (normalized_count_X_eq_of_coe hP).symm
  exacts [Ideal.count_span_normalizedFactors_eq_of_normUnit hP Polynomial.normUnit_X prime_X,
    Ideal.count_span_normalizedFactors_eq_of_normUnit (by simp [hP]) normUnit_X X_prime,
    span_ne_zero'.1, (idealX K).isPrime, span_ne_zero'.2]

Goal state after:
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ₚ)
this✝ : (Ideal.map (algebraMap S Sₚ) P).LiesOver P
this : (Ideal.map (algebraMap S Sₚ) P).IsPrime
⊢ (length (Localization.AtPrime (Ideal.map (algebraMap S Sₚ) P))
        (Localization.AtPrime (Ideal.map (algebraMap S Sₚ) P) ⧸
          Ideal.map (algebraMap Rₚ (Localization.AtPrime (Ideal.map (algebraMap S Sₚ) P))) (maximalIdeal Rₚ))).toNat =
    P.ramificationIdx R

Tactic:
ramificationIdx_eq p P

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
this : (Ideal.map (algebraMap S Sₚ) P).IsPrime
⊢ (length (Localization.AtPrime (Ideal.map (algebraMap S Sₚ) P))
        (Localization.AtPrime (Ideal.map (algebraMap S Sₚ) P) ⧸
          Ideal.map (algebraMap Rₚ (Localization.AtPrime (Ideal.map (algebraMap S Sₚ) P))) (maximalIdeal Rₚ))).toNat =
    (length (Localization.AtPrime P)
        (Localization.AtPrime P ⧸ Ideal.map (algebraMap R (Localization.AtPrime P)) p)).toNat
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:
| succ k n_ih =>

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) < ↑(η * γ)
F_mul : (ofPowerSeries ℤ K) f.powerSeriesPart = (single (-HahnSeries.order f)) 1 * f
⊢ Valued.v (f - (algebraMap K⟮X⟯ K⸨X⸩) (RatFunc.X ^ HahnSeries.order f * ↑P)) < ↑γ

Tactic:
obtain ⟨s, hs⟩ := Int.exists_eq_neg_ofNat (le_of_lt ord_nonpos)

Goal state after:
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) < ↑(η * γ)
F_mul : (ofPowerSeries ℤ K) f.powerSeriesPart = (single (-HahnSeries.order f)) 1 * f
s : ℕ
hs : HahnSeries.order f = -↑s
⊢ Valued.v (f - (algebraMap K⟮X⟯ K⸨X⸩) (RatFunc.X ^ HahnSeries.order f * ↑P)) < ↑γ
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case refine_2.refine_1
R : Type u_3
m : ℕ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i : ℕ
him : i < m
t : Finset (Fin m)
ht : t ∈ powersetCard (i + 1) univ
ht' : #t = #(Iic ⟨i, him⟩)
hne : ∃ x, x ∈ Iic ⟨i, him⟩ \ t
hkm : (Iic ⟨i, him⟩ \ t).min' hne ∈ Iic ⟨i, him⟩ ∧ (Iic ⟨i, him⟩ \ t).min' hne ∉ t
k : Fin m
hk : (fun x1 x2 ↦ x1 < x2) k ((Iic ⟨i, him⟩ \ t).min' hne)
⊢ (if hi : k ∈ t then 1 else 0) = if hi : k ∈ Iic ⟨i, him⟩ then 1 else 0

Tactic:
have hki := mem_Iic.2 (hk.le.trans <| mem_Iic.1 hkm.1)

Goal state after:
case refine_2.refine_1
R : Type u_3
m : ℕ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i : ℕ
him : i < m
t : Finset (Fin m)
ht : t ∈ powersetCard (i + 1) univ
ht' : #t = #(Iic ⟨i, him⟩)
hne : ∃ x, x ∈ Iic ⟨i, him⟩ \ t
hkm : (Iic ⟨i, him⟩ \ t).min' hne ∈ Iic ⟨i, him⟩ ∧ (Iic ⟨i, him⟩ \ t).min' hne ∉ t
k : Fin m
hk : (fun x1 x2 ↦ x1 < x2) k ((Iic ⟨i, him⟩ \ t).min' hne)
hki : k ∈ Iic ⟨i, him⟩
⊢ (if hi : k ∈ t then 1 else 0) = if hi : k ∈ Iic ⟨i, him⟩ then 1 else 0
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
this : (algebraMap K⟮X⟯ K⸨X⸩) 1 = 1
⊢ Valued.v ((single 1) 1 ^ s)⁻¹ * Valued.v ((ofPowerSeries ℤ K) F - (algebraMap K⟮X⟯ K⸨X⸩) ↑P) < ↑γ

Tactic:
map_inv₀,

Goal state after:
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
this : (algebraMap K⟮X⟯ K⸨X⸩) 1 = 1
⊢ (Valued.v ((single 1) 1 ^ s))⁻¹ * Valued.v ((ofPowerSeries ℤ K) F - (algebraMap K⟮X⟯ K⸨X⸩) ↑P) < ↑γ
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case zero
R : Type u_3
n m : ℕ
inst✝ : CommSemiring R
r : R
hnm : n ≤ m
⊢ leadingCoeff (⇑toLex) (C r) = r

Tactic:
leadingCoeff_toLex_C

Goal state after:
case zero
R : Type u_3
n m : ℕ
inst✝ : CommSemiring R
r : R
hnm : n ≤ m
⊢ r = r