mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization

Goal state before:
pp: case h.refine_2
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 : (Ideal.comap (algebraMap R R') p).IsPrime
x : M
hx : Ideal.comap (algebraMap R R') p = (⊥.colon {x}).radical
t✝ : R'
r : R
s : ↥S
hrs : IsLocalization.mk' R' r s = t✝
x✝ : ∃ n s', s' • r ^ n • x = 0
n : ℕ
t : ↥S
ht : t • r ^ n • x = 0
this : IsLocalization.mk' R' r s = IsLocalization.mk' R' (↑t * r) 1 * IsLocalization.mk' R' 1 (t * s)
⊢ (algebraMap R R') (↑t * r) ∈ p

Tactic:
← Ideal.mem_comap,

Goal state after:
case h.refine_2
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 : (Ideal.comap (algebraMap R R') p).IsPrime
x : M
hx : Ideal.comap (algebraMap R R') p = (⊥.colon {x}).radical
t✝ : R'
r : R
s : ↥S
hrs : IsLocalization.mk' R' r s = t✝
x✝ : ∃ n s', s' • r ^ n • x = 0
n : ℕ
t : ↥S
ht : t • r ^ n • x = 0
this : IsLocalization.mk' R' r s = IsLocalization.mk' R' (↑t * r) 1 * IsLocalization.mk' R' 1 (t * s)
⊢ ↑t * r ∈ Ideal.comap (algebraMap R R') p
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization

Goal state before:
pp: 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'
inst✝ : IsNoetherianRing R
⊢ Ideal.comap (algebraMap R R') ⁻¹' associatedPrimes R M = associatedPrimes R' M'

Tactic:
ext p

Goal state after:
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'
inst✝ : IsNoetherianRing R
p : Ideal R'
⊢ p ∈ Ideal.comap (algebraMap R R') ⁻¹' associatedPrimes R M ↔ p ∈ associatedPrimes R' M'
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: case add
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
x : A
hx : x ∈ I • J
y : A
hy : y ∈ I • J
hx' : ∀ {n : ℕ}, hI.dpow n x = hJ.dpow n x
hy' : ∀ {n : ℕ}, hI.dpow n y = hJ.dpow n y
n : ℕ
k : ℕ × ℕ
a✝ : k ∈ antidiagonal n
⊢ hJ.dpow k.1 x * hI.dpow k.2 y = hJ.dpow k.1 x * hJ.dpow k.2 y

Tactic:
hy'

Goal state after:
case add
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
x : A
hx : x ∈ I • J
y : A
hy : y ∈ I • J
hx' : ∀ {n : ℕ}, hI.dpow n x = hJ.dpow n x
hy' : ∀ {n : ℕ}, hI.dpow n y = hJ.dpow n y
n : ℕ
k : ℕ × ℕ
a✝ : k ∈ antidiagonal n
⊢ hJ.dpow k.1 x * hJ.dpow k.2 y = hJ.dpow k.1 x * hJ.dpow k.2 y
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: case h.mul_X
R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P : DividedPowerAlgebra R M → Prop
h_C : ∀ (a : R), P ↑(C a)
h_add : ∀ (f g : DividedPowerAlgebra R M), P f → P g → P (f + g)
h_dp : ∀ (f : DividedPowerAlgebra R M) (n : ℕ) (m : M), P f → P (f * dp R n m)
g : MvPolynomial (ℕ × M) R
nm : ℕ × M
h : P ↑g
⊢ P ↑(g * X nm)

Tactic:
rw [RingCon.coe_mul]

Goal state after:
case h.mul_X
R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P : DividedPowerAlgebra R M → Prop
h_C : ∀ (a : R), P ↑(C a)
h_add : ∀ (f g : DividedPowerAlgebra R M), P f → P g → P (f + g)
h_dp : ∀ (f : DividedPowerAlgebra R M) (n : ℕ) (m : M), P f → P (f * dp R n m)
g : MvPolynomial (ℕ × M) R
nm : ℕ × M
h : P ↑g
⊢ P (↑g * ↑(X nm))
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: case C
R : Type u_4
M : Type u_5
ι : Type u_6
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
hv : Submodule.span R (Set.range v) = ⊤
r : R
⊢ (algebraMap R (DividedPowerAlgebra R M)) r ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))

Tactic:
simp only [Algebra.algebraMap_eq_smul_one]
    exact smul_mem _ _ (subset_span ⟨0, by simp⟩)

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: case smul
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J : Ideal A
x a : A
ha : a ∈ I
b : A
hb : b ∈ J
m : ℕ
hm : m ≠ 0
⊢ hI.dpow m (a • b) ∈ I • J

Tactic:
rw [smul_eq_mul, smul_eq_mul, mul_comm a b, hI.dpow_mul ha, mul_comm]

Goal state after:
case smul
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J : Ideal A
x a : A
ha : a ∈ I
b : A
hb : b ∈ J
m : ℕ
hm : m ≠ 0
⊢ b ^ m * hI.dpow m a ∈ J * I
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: R : Type u_1
K : Type u_2
inst✝ : DivisionRing K
a b : K[ε]
h : a + b = 1
⊢ IsUnit a ∨ IsUnit b

Tactic:
rw [add_comm, ← eq_sub_iff_add_eq] at h

Goal state after:
R : Type u_1
K : Type u_2
inst✝ : DivisionRing K
a b : K[ε]
h : b = 1 - a
⊢ IsUnit a ∨ IsUnit b
Module: Mathlib.RingTheory.TotallySplit

Goal state before:
pp: k : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : Field k
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra k R
inst✝¹ : Algebra R S
ι : Type u_4
inst✝ : Finite ι
⊢ ∃ n, Nonempty ((ι → R) ≃ₐ[R] Fin n → R)

Tactic:
by
    cases nonempty_fintype ι
    exact ⟨_, ⟨AlgEquiv.piCongrLeft' _ _ (Fintype.equivFin ι)⟩⟩

Goal state after:
Module: Mathlib.RingTheory.TotallySplit

Goal state before:
pp: n : ℕ
ih :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Etale R S] [Module.Finite R S],
    Module.rankAtStalk S = ↑n →
      ∃ T x x_1, ∃ (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ : Etale R T), IsFiniteSplit T (T ⊗[R] S)
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Etale R S
inst✝ : Module.Finite R S
hn : Module.rankAtStalk S = ↑(n + 1)
h✝ : Nontrivial R
this✝³ : Nontrivial S
U : Type u
w✝¹ : CommRing U
w✝ : Algebra S U
e : S ⊗[R] S ≃ₐ[S] S × U
algInst✝ : Algebra (S × U) U := (RingHom.snd S U).toAlgebra
this✝² : IsScalarTower S (S × U) U
this✝¹ : Etale S U
this✝ : Module.Finite S U
this : ∀ (p : PrimeSpectrum S), 1 + Module.rankAtStalk U p = n + 1
⊢ Module.rankAtStalk U = ↑n

Tactic:
ext p

Goal state after:
n : ℕ
ih :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Etale R S] [Module.Finite R S],
    Module.rankAtStalk S = ↑n →
      ∃ T x x_1, ∃ (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ : Etale R T), IsFiniteSplit T (T ⊗[R] S)
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Etale R S
inst✝ : Module.Finite R S
hn : Module.rankAtStalk S = ↑(n + 1)
h✝ : Nontrivial R
this✝³ : Nontrivial S
U : Type u
w✝¹ : CommRing U
w✝ : Algebra S U
e : S ⊗[R] S ≃ₐ[S] S × U
algInst✝ : Algebra (S × U) U := (RingHom.snd S U).toAlgebra
this✝² : IsScalarTower S (S × U) U
this✝¹ : Etale S U
this✝ : Module.Finite S U
this : ∀ (p : PrimeSpectrum S), 1 + Module.rankAtStalk U p = n + 1
p : PrimeSpectrum S
⊢ Module.rankAtStalk U p = ↑n p
Module: Mathlib.RingTheory.Extension.ExtendScalars

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
x : P.Ring
x_in : x ∈ P.ker
property✝ : Cotangent.mk ⟨x, x_in⟩ ∈ P.extendScalars.cotangentComplex.ker
⊢ (algebraMap P.Ring (Generators.self P.Ring S).toExtension.Ring) x ∈ (Generators.self P.Ring S).toExtension.ker

Tactic:
← Ideal.mem_comap,

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
x : P.Ring
x_in : x ∈ P.ker
property✝ : Cotangent.mk ⟨x, x_in⟩ ∈ P.extendScalars.cotangentComplex.ker
⊢ x ∈
    Ideal.comap (algebraMap P.Ring (Generators.self P.Ring S).toExtension.Ring)
      (Generators.self P.Ring S).toExtension.ker
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
a x : A
hx : x ∈ {a | a ∈ I ∧ ∀ (n : ℕ), hI.dpow n a = hI'.dpow n a}
n : ℕ
⊢ hI.dpow n (a * x) = hI'.dpow n (a * x)

Tactic:
by rw [hI.dpow_mul hx.1, hI'.dpow_mul hx.1, hx.2]

Goal state after:
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
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
n : ℕ
a : A
ha : a ∈ I
⊢ dpow hI f n (f a) = f (hI.dpow n a)

Tactic:
simp only [dpow, Function.extend_def]

Goal state after:
A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
n : ℕ
a : A
ha : a ∈ I
⊢ (if h : ∃ a_1, f ↑a_1 = f a then f (hI.dpow n ↑(Classical.choose h)) else 0 (f a)) = f (hI.dpow n a)
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
x : V⟦Γ⟧
a b : PowerSeries R
h : ¬0 < x.orderTop
⊢ (PowerSeries.constantCoeff a * PowerSeries.constantCoeff b) • 1 =
    PowerSeries.constantCoeff a • 1 * PowerSeries.constantCoeff b • 1

Tactic:
smul_mul_smul_comm,

Goal state after:
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
x : V⟦Γ⟧
a b : PowerSeries R
h : ¬0 < x.orderTop
⊢ (PowerSeries.constantCoeff a * PowerSeries.constantCoeff b) • 1 =
    (PowerSeries.constantCoeff a * PowerSeries.constantCoeff b) • (1 * 1)
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : PartialOrder Γ
inst✝² : AddCommMonoid R
inst✝¹ : AddCommMonoid V
inst✝ : SMulWithZero R V
f : α → R
s : SummableFamily Γ V α
g : Γ
hg : ∃ i, ¬f i • (s i).coeff g = 0
⊢ ∃ i, ¬(s i).coeff g = 0

Tactic:
obtain ⟨i, hi⟩ := hg

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : PartialOrder Γ
inst✝² : AddCommMonoid R
inst✝¹ : AddCommMonoid V
inst✝ : SMulWithZero R V
f : α → R
s : SummableFamily Γ V α
g : Γ
i : α
hi : ¬f i • (s i).coeff g = 0
⊢ ∃ i, ¬(s i).coeff g = 0
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
R : Type u_3
α : Type u_5
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
s : SummableFamily Γ R α
g : Γ
a : α
ha : ↑g = (s a).orderTop
hg : ∀ (b : α), ∀ g' ∈ (s b).support, g ≤ g'
hna : ∀ (b : α), b ≠ a → (s b).coeff g = 0
⊢ s.hsum.coeff g = (s a).coeff g

Tactic:
by rw [coeff_hsum, finsum_eq_single (fun i ↦ (s i).coeff g) a
    hna]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
⊢ PowerSeries.constantCoeff (subst ![0, PowerSeries.X] F.toPowerSeries) = 0

Tactic:
rw [PowerSeries.constantCoeff, PowerSeries.X, constantCoeff_subst_eq_zero HasSubst.zero_X
          (by simp) F.zero_constantCoeff]

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

Goal state before:
pp: case pos
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
h : 0 < x.orderTop
⊢ (⋃ a, ((if 0 < x.orderTop then x else 0) ^ a).support).IsPWO

Tactic:
simp only [h, ↓reduceIte]
      exact isPWO_iUnion_support_powers (zero_le_orderTop_iff.mp <| le_of_lt h)

Goal state after:
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: case succ.refine_2
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)
⊢ ∑ k ∈ Finset.Ico 2 (((taylor (c n)) f).natDegree + 2),
      ((taylor (c n)) f).coeff k * (-(Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ)) ^ k ∈
    I ^ (n + 1 + 1)

Tactic:
· refine Submodule.sum_mem _ ?_
          simp only [Finset.mem_Ico]
          rintro i ⟨h2i, _⟩
          have aux : n + 2 ≤ i * (n + 1) := by trans 2 * (n + 1) <;> nlinarith only [h2i]
          refine Ideal.mul_mem_left _ _ (Ideal.pow_le_pow_right aux ?_)
          rw [pow_mul']
          exact Ideal.pow_mem_pow ((Ideal.neg_mem_iff _).2 <| Ideal.mul_mem_right _ _ ih) _

Goal state after:
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: case refine_1
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 : R
n : ℕ
ha : c n ≡ a [SMOD I ^ n • ⊤]
⊢ Polynomial.eval a f ≡ 0 [SMOD I ^ n • ⊤]

Tactic:
rw [← Ideal.one_eq_top, Ideal.smul_eq_mul, mul_one] at ha ⊢

Goal state after:
case refine_1
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 : R
n : ℕ
ha : c n ≡ a [SMOD I ^ n]
⊢ Polynomial.eval a f ≡ 0 [SMOD I ^ n]
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
⊢ (RingHom.pi fun p ↦ algebraMap R (Localization.AtPrime (↑p).asIdeal)) x = 0

Tactic:
ext p

Goal state after:
case refine_2
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.Pure
x : R
hx : x ∈ I
p : ↑(zeroLocus ↑I)
⊢ (RingHom.pi fun p ↦ algebraMap R (Localization.AtPrime (↑p).asIdeal)) x p = 0 p
Module: Mathlib.RingTheory.KrullDimension.Polynomial

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

pp: R : Type u_1
inst✝ : CommRing R
p : PrimeSpectrum R
⊢ Order.krullDim ↑(PrimeSpectrum.comap C ⁻¹' {p}) ≤ ↑1

Tactic:
· exact fun {a b} h ↦ Ideal.comap_mono h

Goal state after:
R : Type u_1
inst✝ : CommRing R
p : PrimeSpectrum R
⊢ Order.krullDim ↑(PrimeSpectrum.comap C ⁻¹' {p}) ≤ ↑1
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.height ≤ (map (Quotient.mk I) p).height + ↑(Submodule.spanFinrank I)

Tactic:
let p' := p.map (algebraMap R (R ⧸ I))

Goal state after:
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
⊢ p.height ≤ (map (Quotient.mk I) p).height + ↑(Submodule.spanFinrank I)
Module: Mathlib.RingTheory.Spectrum.Prime.LTSeries

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
p : LTSeries (PrimeSpectrum R)
x : R
hx : x ∈ (RelSeries.last p).asIdeal
n : ℕ
hp : p.length = n
⊢ ∃ q,
    x ∈ (q.toFun 1).asIdeal ∧ n = q.length ∧ RelSeries.head p = RelSeries.head q ∧ RelSeries.last p = RelSeries.last q

Tactic:
induction n generalizing p with

Goal state after:
case succ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
x : R
n : ℕ
hn :
  ∀ (p : LTSeries (PrimeSpectrum R)),
    x ∈ (RelSeries.last p).asIdeal →
      p.length = n →
        ∃ q,
          x ∈ (q.toFun 1).asIdeal ∧
            n = q.length ∧ RelSeries.head p = RelSeries.head q ∧ RelSeries.last p = RelSeries.last q
p : LTSeries (PrimeSpectrum R)
hx : x ∈ (RelSeries.last p).asIdeal
hp : p.length = n + 1
⊢ ∃ q,
    x ∈ (q.toFun 1).asIdeal ∧
      n + 1 = q.length ∧ RelSeries.head p = RelSeries.head q ∧ RelSeries.last p = RelSeries.last q
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: case neg
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)
IH :
  ∀ s_1 ∈ s,
    (s.erase s_1).inf id = N → ∃ t ⊆ s.erase s_1, t.inf id = N ∧ ∀ ⦃J : Submodule R M⦄, J ∈ t → ¬(t.erase J).inf id ≤ J
hs : s.inf id = N
J : Submodule R M
hJ : J ∈ s
hJ' : (s.erase J).inf id ≤ J
⊢ (s.erase J).inf id = N

Tactic:
← Finset.insert_erase hJ

Goal state after:
case neg
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)
IH :
  ∀ s_1 ∈ s,
    (s.erase s_1).inf id = N → ∃ t ⊆ s.erase s_1, t.inf id = N ∧ ∀ ⦃J : Submodule R M⦄, J ∈ t → ¬(t.erase J).inf id ≤ J
J : Submodule R M
hs : (insert J (s.erase J)).inf id = N
hJ : J ∈ s
hJ' : (s.erase J).inf id ≤ J
⊢ (s.erase J).inf id = N
Module: Mathlib.RingTheory.Lasker

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

Tactic:
ext p

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

Goal state before:
pp: case refine_3
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 ⋯
q : ℕ := card ↥Z
card_Z : q = card ↥Z
hq : 1 < q
n : ℕ := finrank (↥Z) D
card_D : card D = q ^ n
h1qn : 1 ≤ q ^ n
Φₙ : ℤ[X] := cyclotomic n ℤ
key : ↑q - 1 + ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card) = ↑q ^ n - 1
this : eval (↑q) Φₙ ∣ ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card)
contra : eval (↑q) Φₙ ∣ ↑q - 1
h : n ≤ 1
x : D
hx : ∀ (w : D), ∃ c, c • x = w
r : ↥Z
x✝ : r • x ∈ ⊤
s : ↥Z
⊢ s • x * r • x = r • x * s • x

Tactic:
smul_mul_smul_comm,

Goal state after:
case refine_3
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 ⋯
q : ℕ := card ↥Z
card_Z : q = card ↥Z
hq : 1 < q
n : ℕ := finrank (↥Z) D
card_D : card D = q ^ n
h1qn : 1 ≤ q ^ n
Φₙ : ℤ[X] := cyclotomic n ℤ
key : ↑q - 1 + ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card) = ↑q ^ n - 1
this : eval (↑q) Φₙ ∣ ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card)
contra : eval (↑q) Φₙ ∣ ↑q - 1
h : n ≤ 1
x : D
hx : ∀ (w : D), ∃ c, c • x = w
r : ↥Z
x✝ : r • x ∈ ⊤
s : ↥Z
⊢ (s * r) • (x * x) = r • x * s • x
Module: Mathlib.RingTheory.LittleWedderburn

Goal state before:
pp: case refine_3
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 ⋯
q : ℕ := card ↥Z
card_Z : q = card ↥Z
hq : 1 < q
n : ℕ := finrank (↥Z) D
card_D : card D = q ^ n
h1qn : 1 ≤ q ^ n
Φₙ : ℤ[X] := cyclotomic n ℤ
key : ↑q - 1 + ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card) = ↑q ^ n - 1
this : eval (↑q) Φₙ ∣ ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card)
contra : eval (↑q) Φₙ ∣ ↑q - 1
h : n ≤ 1
x : D
hx : ∀ (w : D), ∃ c, c • x = w
r : ↥Z
x✝ : r • x ∈ ⊤
s : ↥Z
⊢ (s * r) • (x * x) = r • x * s • x

Tactic:
smul_mul_smul_comm,

Goal state after:
case refine_3
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 ⋯
q : ℕ := card ↥Z
card_Z : q = card ↥Z
hq : 1 < q
n : ℕ := finrank (↥Z) D
card_D : card D = q ^ n
h1qn : 1 ≤ q ^ n
Φₙ : ℤ[X] := cyclotomic n ℤ
key : ↑q - 1 + ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card) = ↑q ^ n - 1
this : eval (↑q) Φₙ ∣ ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card)
contra : eval (↑q) Φₙ ∣ ↑q - 1
h : n ≤ 1
x : D
hx : ∀ (w : D), ∃ c, c • x = w
r : ↥Z
x✝ : r • x ∈ ⊤
s : ↥Z
⊢ (s * r) • (x * x) = (r * s) • (x * x)
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
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 ∉ ⋃ r ∈ s₀, ↑↑r
⊢ y ∈ S

Tactic:
simp only [Submonoid.mem_iInf, Ideal.mem_primeCompl_iff, Subtype.forall, S]

Goal state after:
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 ∉ ⋃ r ∈ s₀, ↑↑r
⊢ ∀ (a : Ideal R) (b : a ∈ N.associatedPrimes), ⟨a, b⟩ ∈ s₀ → y ∉ a