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

Goal state before:
pp: R : Type u_3
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
⊢ span {p.content} ≤ span {Submodule.IsPrincipal.generator p.contentIdeal}

Tactic:
span_singleton_le_span_singleton,

Goal state after:
R : Type u_3
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
⊢ Submodule.IsPrincipal.generator p.contentIdeal ∣ p.content
Module: Mathlib.RingTheory.DedekindDomain.GaussLemma

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
b : NNReal
hb : 1 < b
p : R[X]
hR : ¬IsField R
⊢ p.contentIdeal = ⊤ ↔ ∀ (v : HeightOneSpectrum R), gaussNorm (v.intAdicAbv hb) 1 p = 1

Tactic:
convert_to _ ↔ ∀ (x : HeightOneSpectrum R), 1 ≤ gaussNorm (x.intAdicAbv hb) 1 p
  · grind [gaussNorm_intAdicAbv_le_one]
  simp [← not_iff_not, gaussNorm_lt_one_iff_contentIdeal_le, ideal_ne_top_iff_exists hR]

Goal state after:
Module: Mathlib.RingTheory.Bialgebra.MonoidAlgebra

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
M : Type u_8
N : Type u_9
O : Type u_10
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Group G
inst✝¹ : Group H
inst✝ : Group I
f : R[G] →ₐc[R] R[H]
⊢ (fun m ↦ single m 1) (mapDomainOfBialgHomFun f 1) = (fun m ↦ single m 1) 1

Tactic:
by simp [← one_def]

Goal state after:
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization

Goal state before:
pp: case h.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 : (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
h : IsLocalization.mk' R' r s ∈ p
⊢ ∃ b, 1 • r ^ b • x = 0

Tactic:
simp only [← mem_colon_singleton, one_smul, ← mem_bot R, ← hx, ← Ideal.mem_radical_iff]

Goal state after:
case h.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 : (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
h : IsLocalization.mk' R' r s ∈ p
⊢ r ∈ Ideal.comap (algebraMap R R') p
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: case neg
A : Type u_1
inst✝² : CommSemiring A
M : Type u_2
inst✝¹ : AddCommMonoid M
I : AddSubmonoid M
dpow : ℕ → M → A
dpow_zero : ∀ {x : M}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_3
inst✝ : DecidableEq ι
x : ι → M
dpow_add : ∀ {n : ℕ} {x y : M}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_1 ∈ range n.succ, dpow x_1 x * dpow (n - x_1) y
hx : ∀ i ∈ ∅, x i ∈ I
n : ℕ
hn : ¬n = 0
⊢ ∅.sym n = ∅

Tactic:
sym_eq_empty

Goal state after:
case neg
A : Type u_1
inst✝² : CommSemiring A
M : Type u_2
inst✝¹ : AddCommMonoid M
I : AddSubmonoid M
dpow : ℕ → M → A
dpow_zero : ∀ {x : M}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_3
inst✝ : DecidableEq ι
x : ι → M
dpow_add : ∀ {n : ℕ} {x y : M}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_1 ∈ range n.succ, dpow x_1 x * dpow (n - x_1) y
hx : ∀ i ∈ ∅, x i ∈ I
n : ℕ
hn : ¬n = 0
⊢ n ≠ 0 ∧ ∅ = ∅
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: case neg
A : Type u_1
inst✝² : CommSemiring A
M : Type u_2
inst✝¹ : AddCommMonoid M
I : AddSubmonoid M
dpow : ℕ → M → A
dpow_zero : ∀ {x : M}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_3
inst✝ : DecidableEq ι
x : ι → M
dpow_add : ∀ {n : ℕ} {x y : M}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_1 ∈ range n.succ, dpow x_1 x * dpow (n - x_1) y
hx : ∀ i ∈ ∅, x i ∈ I
n : ℕ
hn : ¬n = 0
⊢ #(∅.sym n) = 0

Tactic:
rw [card_eq_zero, sym_eq_empty]

Goal state after:
case neg
A : Type u_1
inst✝² : CommSemiring A
M : Type u_2
inst✝¹ : AddCommMonoid M
I : AddSubmonoid M
dpow : ℕ → M → A
dpow_zero : ∀ {x : M}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_3
inst✝ : DecidableEq ι
x : ι → M
dpow_add : ∀ {n : ℕ} {x y : M}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_1 ∈ range n.succ, dpow x_1 x * dpow (n - x_1) y
hx : ∀ i ∈ ∅, x i ∈ I
n : ℕ
hn : ¬n = 0
⊢ n ≠ 0 ∧ ∅ = ∅
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
hhI : ∀ {n : ℕ}, n ≠ 0 → ∀ s ∈ S, hI.dpow n s ∈ span S
hSI : span S ≤ I
m : ℕ
hm : m ≠ 0
z : A
⊢ z ∈ span S → hI.dpow m z ∈ span S

Tactic:
hz

Goal state after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
hhI : ∀ {n : ℕ}, n ≠ 0 → ∀ s ∈ S, hI.dpow n s ∈ span S
hSI : span S ≤ I
m : ℕ
hm : m ≠ 0
z : A
hz : z ∈ span S
⊢ hI.dpow m z ∈ span S
Module: Mathlib.RingTheory.DividedPowers.RatAlgebra

Goal state before:
pp: A : Type u_1
inst✝³ : CommRing A
p : ℕ
inst✝² : CharP A p
inst✝¹ : Fact (Nat.Prime p)
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
hIp : I ^ p = 0
n : ℕ
hn : p ≤ n
a : A
⊢ (dividedPowers A p hIp).dpow n a = 0

Tactic:
simp only [dividedPowers, IsNilpotent.dividedPowers, OfInvertibleFactorial.dpow_apply,
    ite_eq_right_iff]
  intro ha
  rw [Ideal.pow_eq_zero_of_mem hIp hn ha, mul_zero]

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

Goal state before:
pp: R✝ : Type u
inst✝⁹ : CommRing R✝
k : Type u
inst✝⁸ : Field k
Ω✝ : Type w
inst✝⁷ : Field Ω✝
inst✝⁶ : Algebra R✝ Ω✝
S✝ : Type w
inst✝⁵ : CommRing S✝
inst✝⁴ : Algebra R✝ S✝
inst✝³ : Algebra S✝ Ω✝
inst✝² : IsScalarTower R✝ S✝ Ω✝
Ω : Type u
inst✝¹ : Field Ω
inst✝ : IsSepClosed Ω
R S : (FiniteEtale Ω)ᵒᵖ
f : R ⟶ S
⊢ (finiteSpec Ω ⋙
            { obj := fun X ↦ Opposite.op (of Ω (X.obj → Ω)),
              map := fun {X Y} f ↦
                (ofHom (AlgHom.pi fun i ↦ Pi.evalAlgHom Ω (fun a ↦ Ω) ((ConcreteCategory.hom f) i))).op,
              map_id := ⋯, map_comp := ⋯ }).map
        f ≫
      (isoMk (Algebra.FormallyEtale.equivPiOfIsSepClosed Ω ↑(Opposite.unop S).obj)).op.hom =
    (isoMk (Algebra.FormallyEtale.equivPiOfIsSepClosed Ω ↑(Opposite.unop R).obj)).op.hom ≫ (𝟭 (FiniteEtale Ω)ᵒᵖ).map f

Tactic:
apply Quiver.Hom.unop_inj

Goal state after:
R✝ : Type u
inst✝⁹ : CommRing R✝
k : Type u
inst✝⁸ : Field k
Ω✝ : Type w
inst✝⁷ : Field Ω✝
inst✝⁶ : Algebra R✝ Ω✝
S✝ : Type w
inst✝⁵ : CommRing S✝
inst✝⁴ : Algebra R✝ S✝
inst✝³ : Algebra S✝ Ω✝
inst✝² : IsScalarTower R✝ S✝ Ω✝
Ω : Type u
inst✝¹ : Field Ω
inst✝ : IsSepClosed Ω
R S : (FiniteEtale Ω)ᵒᵖ
f : R ⟶ S
⊢ ((finiteSpec Ω ⋙
              { obj := fun X ↦ Opposite.op (of Ω (X.obj → Ω)),
                map := fun {X Y} f ↦
                  (ofHom (AlgHom.pi fun i ↦ Pi.evalAlgHom Ω (fun a ↦ Ω) ((ConcreteCategory.hom f) i))).op,
                map_id := ⋯, map_comp := ⋯ }).map
          f ≫
        (isoMk (Algebra.FormallyEtale.equivPiOfIsSepClosed Ω ↑(Opposite.unop S).obj)).op.hom).unop =
    ((isoMk (Algebra.FormallyEtale.equivPiOfIsSepClosed Ω ↑(Opposite.unop R).obj)).op.hom ≫
        (𝟭 (FiniteEtale Ω)ᵒᵖ).map f).unop
Module: Mathlib.RingTheory.Etale.Finite

Goal state before:
pp: R : Type u
inst✝⁹ : CommRing R
k : Type u
inst✝⁸ : Field k
Ω✝ : Type w
inst✝⁷ : Field Ω✝
inst✝⁶ : Algebra R Ω✝
S : Type w
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : Algebra S Ω✝
inst✝² : IsScalarTower R S Ω✝
Ω : Type u
inst✝¹ : Field Ω
inst✝ : IsSepClosed Ω
X : FintypeCat
⊢ (ofHom
          (AlgHom.pi fun i ↦
            Pi.evalAlgHom Ω (fun a ↦ Ω)
              ((ConcreteCategory.hom
                  (FintypeCat.equivEquivIso
                      ((Equiv.sigmaUnique X.obj fun a ↦ PrimeSpectrum Ω).symm.trans
                        (PrimeSpectrum.sigmaToPiHomeo fun a ↦ Ω).toEquiv)).hom)
                i))).op ≫
      (ObjectProperty.homMk (CommAlgCat.ofHom ↑(Algebra.FormallyEtale.equivPiOfIsSepClosed Ω (X.obj → Ω)))).op =
    𝟙 (Opposite.op (of Ω (X.obj → Ω)))

Tactic:
apply Quiver.Hom.unop_inj

Goal state after:
R : Type u
inst✝⁹ : CommRing R
k : Type u
inst✝⁸ : Field k
Ω✝ : Type w
inst✝⁷ : Field Ω✝
inst✝⁶ : Algebra R Ω✝
S : Type w
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : Algebra S Ω✝
inst✝² : IsScalarTower R S Ω✝
Ω : Type u
inst✝¹ : Field Ω
inst✝ : IsSepClosed Ω
X : FintypeCat
⊢ ((ofHom
            (AlgHom.pi fun i ↦
              Pi.evalAlgHom Ω (fun a ↦ Ω)
                ((ConcreteCategory.hom
                    (FintypeCat.equivEquivIso
                        ((Equiv.sigmaUnique X.obj fun a ↦ PrimeSpectrum Ω).symm.trans
                          (PrimeSpectrum.sigmaToPiHomeo fun a ↦ Ω).toEquiv)).hom)
                  i))).op ≫
        (ObjectProperty.homMk (CommAlgCat.ofHom ↑(Algebra.FormallyEtale.equivPiOfIsSepClosed Ω (X.obj → Ω)))).op).unop =
    (𝟙 (Opposite.op (of Ω (X.obj → Ω)))).unop
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
J : hI.SubDPIdeal :=
  { carrier := span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}, isSubideal := ⋯, dpow_mem := ⋯ }
K : hI.SubDPIdeal
hK : K = ⊤ ∨ S ⊆ ↑K.carrier
⊢ S ⊆ ↑K

Tactic:
rcases hK with rfl | hKS

Goal state after:
case inl
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
J : hI.SubDPIdeal :=
  { carrier := span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}, isSubideal := ⋯, dpow_mem := ⋯ }
⊢ S ⊆ ↑⊤

case inr
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
J : hI.SubDPIdeal :=
  { carrier := span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}, isSubideal := ⋯, dpow_mem := ⋯ }
K : hI.SubDPIdeal
hKS : S ⊆ ↑K.carrier
⊢ S ⊆ ↑K
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A✝ : Type u_1
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ hI' : DividedPowers I✝
A : Type u_2
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers (Ideal.map (Ideal.Quotient.mk J) I)
φ : hI.DPMorphism hJ
hφ : φ.toRingHom = Ideal.Quotient.mk J
x✝¹ : ℕ
hn : x✝¹ ≠ 0
a : A
x✝ : a ∈ J ⊓ I
haJ : a ∈ ↑J
haI : a ∈ ↑I
⊢ hI.dpow x✝¹ a ∈ J

Tactic:
← Quotient.eq_zero_iff_mem,

Goal state after:
A✝ : Type u_1
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ hI' : DividedPowers I✝
A : Type u_2
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers (Ideal.map (Ideal.Quotient.mk J) I)
φ : hI.DPMorphism hJ
hφ : φ.toRingHom = Ideal.Quotient.mk J
x✝¹ : ℕ
hn : x✝¹ ≠ 0
a : A
x✝ : a ∈ J ⊓ I
haJ : a ∈ ↑J
haI : a ∈ ↑I
⊢ (Ideal.Quotient.mk J) (hI.dpow x✝¹ a) = 0
Module: Mathlib.RingTheory.Frobenius

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
inst✝ : Q.IsPrime
⊢ Ideal.comap (algebraMap R (Localization.AtPrime Q)) (maximalIdeal (Localization.AtPrime Q)) = Ideal.under R Q

Tactic:
← Ideal.under_def,

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
inst✝ : Q.IsPrime
⊢ Ideal.under R (maximalIdeal (Localization.AtPrime Q)) = Ideal.under R Q
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
σ : Type u_3
F : FormalGroup R
f₀ f₁ f₂ : MvPowerSeries σ R
h₀ : PowerSeries.HasSubst f₀
h₁ : PowerSeries.HasSubst f₁
h₂ : PowerSeries.HasSubst f₂
aux₁ : HasSubst ![subst ![Y₀, Y₁] F.toPowerSeries, Y₂]
aux₂ : HasSubst ![Y₀, subst ![Y₁, Y₂] F.toPowerSeries]
this : HasSubst ![f₀, f₁, f₂]
⊢ subst ![f₀, f₁, f₂] (subst ![subst ![Y₀, Y₁] F.toPowerSeries, Y₂] F.toPowerSeries) =
    subst ![f₀, subst ![f₁, f₂] F.toPowerSeries] F.toPowerSeries

Tactic:
by
      rw [F.assoc, subst_comp_subst_apply aux₂ this]
      congr! 2 with s
      fin_cases s
      · simp [subst_X this]
      · simp only [Fin.mk_one, Matrix.cons_val_one, Matrix.cons_val_fin_one,
          subst_comp_subst_apply HasSubst.X_X this]
        congr! 2 with s
        fin_cases s <;> simp [subst]

Goal state after:
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
this : (if h : s.hsum = 0 then ⊤ else ↑(⋯.min ⋯)) = ↑g
h : s.hsum = 0
⊢ False

Tactic:
simp [h] at this

Goal state after:
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
tfae_3_to_2 :
  (∀ {K : Type u} [inst : Field K] (φ : R →+* K),
      Surjective ⇑φ →
        ∀ (f : R[X]),
          f.Monic → ∀ (a₀ : K), eval₂ φ a₀ f = 0 → eval₂ φ a₀ (derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ φ a = a₀) →
    ∀ (f : R[X]),
      f.Monic →
        ∀ (a₀ : ResidueField R), (aeval a₀) f = 0 → (aeval a₀) (derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ (residue R) a = a₀
x✝ :
  ∀ (f : R[X]),
    f.Monic →
      ∀ (a₀ : ResidueField R), (aeval a₀) f = 0 → (aeval a₀) (derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ (residue R) a = a₀
H : ∀ (f : R[X]),
  f.Monic →
    ∀ (a₀ : ResidueField R), (aeval a₀) f = 0 → (aeval a₀) (derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ (residue R) a = a₀ :=
  x✝
f : R[X]
hf : f.Monic
⊢ ∀ (a₀ : R),
    Polynomial.eval a₀ f ∈ maximalIdeal R →
      IsUnit (Polynomial.eval a₀ (derivative f)) → ∃ a, f.IsRoot a ∧ a - a₀ ∈ maximalIdeal R

Tactic:
a₀

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
tfae_3_to_2 :
  (∀ {K : Type u} [inst : Field K] (φ : R →+* K),
      Surjective ⇑φ →
        ∀ (f : R[X]),
          f.Monic → ∀ (a₀ : K), eval₂ φ a₀ f = 0 → eval₂ φ a₀ (derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ φ a = a₀) →
    ∀ (f : R[X]),
      f.Monic →
        ∀ (a₀ : ResidueField R), (aeval a₀) f = 0 → (aeval a₀) (derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ (residue R) a = a₀
x✝ :
  ∀ (f : R[X]),
    f.Monic →
      ∀ (a₀ : ResidueField R), (aeval a₀) f = 0 → (aeval a₀) (derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ (residue R) a = a₀
H : ∀ (f : R[X]),
  f.Monic →
    ∀ (a₀ : ResidueField R), (aeval a₀) f = 0 → (aeval a₀) (derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ (residue R) a = a₀ :=
  x✝
f : R[X]
hf : f.Monic
a₀ : R
⊢ Polynomial.eval a₀ f ∈ maximalIdeal R →
    IsUnit (Polynomial.eval a₀ (derivative f)) → ∃ a, f.IsRoot a ∧ a - a₀ ∈ maximalIdeal R
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
r : R
hr : r * x.leadingCoeff = 1
oinv : Γ
hxo : oinv + x.order = 0
y : R⟦Γ⟧ := x - (single x.order) x.leadingCoeff
hy : y = 0
⊢ (single 0) 1 = 1

Tactic:
single_zero_one

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
r : R
hr : r * x.leadingCoeff = 1
oinv : Γ
hxo : oinv + x.order = 0
y : R⟦Γ⟧ := x - (single x.order) x.leadingCoeff
hy : y = 0
⊢ 1 = 1
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
hR : HenselianLocalRing R
f : R[X]
hf : f.Monic
⊢ ∀ (a₀ : R),
    Polynomial.eval a₀ f ∈ maximalIdeal R →
      IsUnit ((Ideal.Quotient.mk (maximalIdeal R)) (Polynomial.eval a₀ (derivative f))) →
        ∃ a, f.IsRoot a ∧ a - a₀ ∈ maximalIdeal R

Tactic:
a₀

Goal state after:
R : Type u_1
inst✝ : CommRing R
hR : HenselianLocalRing R
f : R[X]
hf : f.Monic
a₀ : R
⊢ Polynomial.eval a₀ f ∈ maximalIdeal R →
    IsUnit ((Ideal.Quotient.mk (maximalIdeal R)) (Polynomial.eval a₀ (derivative f))) →
      ∃ a, f.IsRoot a ∧ a - a₀ ∈ maximalIdeal R
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),
    Polynomial.eval a₀ f ∈ I →
      IsUnit ((Ideal.Quotient.mk I) (Polynomial.eval a₀ (derivative f))) → ∃ a, f.IsRoot a ∧ a - a₀ ∈ I

Tactic:
a₀

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
⊢ Polynomial.eval a₀ f ∈ I →
    IsUnit ((Ideal.Quotient.mk I) (Polynomial.eval a₀ (derivative f))) → ∃ a, f.IsRoot a ∧ a - a₀ ∈ I
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)
⊢ ∀ c_1 ∈ Finset.Ico 2 (((taylor (c n)) f).natDegree + 2),
    ((taylor (c n)) f).coeff c_1 * (-(Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ)) ^ c_1 ∈ I ^ (n + 1 + 1)

Tactic:
simp only [Finset.mem_Ico]

Goal state after:
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)
⊢ ∀ (c_1 : ℕ),
    2 ≤ c_1 ∧ c_1 < ((taylor (c n)) f).natDegree + 2 →
      ((taylor (c n)) f).coeff c_1 * (-(Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ)) ^ c_1 ∈
        I ^ (n + 1 + 1)
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I p : Ideal R
hp : p ∈ I.minimalPrimes
⊢ p.height ≤ ⨅ s, ↑(↑s).card

Tactic:
le_iInf_iff

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I p : Ideal R
hp : p ∈ I.minimalPrimes
⊢ ∀ (i : { s // Submodule.span R ↑s = I }), p.height ≤ ↑(↑i).card
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: case h.succ.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
p : Ideal R
s : Finset R
this✝ : p.IsPrime
hp : under R (maximalIdeal (Localization p.primeCompl)) ∈ (span ↑s).minimalPrimes
n : ℕ
H :
  ∀ m < n + 1,
    ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (s : Finset R),
      p ∈ (span ↑s).minimalPrimes → s.card = m → p.height ≤ ↑m
hn : s.card ≤ n + 1
this :
  ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (s : Finset R),
    p ∈ (span ↑s).minimalPrimes →
      p.IsPrime →
        ∀ (n : ℕ),
          (∀ m < n + 1,
              ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (s : Finset R),
                p ∈ (span ↑s).minimalPrimes → s.card = m → p.height ≤ ↑m) →
            s.card ≤ n + 1 → (∃ (x : IsLocalRing R), p = maximalIdeal R) → p.height ≤ ↑(n + 1)
hR : ¬∃ (x : IsLocalRing R), p = maximalIdeal R
⊢ (under R (maximalIdeal (Localization p.primeCompl))).height ≤ ↑(n + 1)

Tactic:
IsLocalization.height_under p.primeCompl

Goal state after:
case h.succ.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
p : Ideal R
s : Finset R
this✝ : p.IsPrime
hp : under R (maximalIdeal (Localization p.primeCompl)) ∈ (span ↑s).minimalPrimes
n : ℕ
H :
  ∀ m < n + 1,
    ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (s : Finset R),
      p ∈ (span ↑s).minimalPrimes → s.card = m → p.height ≤ ↑m
hn : s.card ≤ n + 1
this :
  ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (s : Finset R),
    p ∈ (span ↑s).minimalPrimes →
      p.IsPrime →
        ∀ (n : ℕ),
          (∀ m < n + 1,
              ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (s : Finset R),
                p ∈ (span ↑s).minimalPrimes → s.card = m → p.height ≤ ↑m) →
            s.card ≤ n + 1 → (∃ (x : IsLocalRing R), p = maximalIdeal R) → p.height ≤ ↑(n + 1)
hR : ¬∃ (x : IsLocalRing R), p = maximalIdeal R
⊢ (maximalIdeal (Localization p.primeCompl)).height ≤ ↑(n + 1)
Module: Mathlib.RingTheory.KrullDimension.Module

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ supportDim R R = ringKrullDim R

Tactic:
have : annihilator R R = ⊥ :=
    annihilator_eq_bot.mpr ((faithfulSMul_iff_algebraMap_injective R R).mpr fun {a₁ a₂} a ↦ a)
  rw [supportDim_eq_ringKrullDim_quotient_annihilator, this]
  exact (RingEquiv.ringKrullDim (RingEquiv.quotientBot R))

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsLocalRing R
dim : Module.supportDim R N = 0
x✝ : Nontrivial N :=
  of_eq_true
    (Eq.trans
      ((fun M [AddCommGroup M] [Module R M] ↦ Eq.symm (propext (Module.supportDim_ne_bot_iff_nontrivial R M))) N)
      (Eq.trans (congrFun' (congrArg Ne dim) ⊥)
        (Eq.trans (congrArg Not WithBot.zero_ne_bot._simp_1) not_false_eq_true)))
⊢ Module.support R N = PrimeSpectrum.zeroLocus ↑(maximalIdeal R)

Tactic:
PrimeSpectrum.zeroLocus_eq_singleton

Goal state after:
R : Type u_1
inst✝³ : CommRing R
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsLocalRing R
dim : Module.supportDim R N = 0
x✝ : Nontrivial N :=
  of_eq_true
    (Eq.trans
      ((fun M [AddCommGroup M] [Module R M] ↦ Eq.symm (propext (Module.supportDim_ne_bot_iff_nontrivial R M))) N)
      (Eq.trans (congrFun' (congrArg Ne dim) ⊥)
        (Eq.trans (congrArg Not WithBot.zero_ne_bot._simp_1) not_false_eq_true)))
⊢ Module.support R N = {{ asIdeal := maximalIdeal R, isPrime := ⋯ }}
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
⊢ p ∈ (span ↑t).minimalPrimes

Tactic:
Finset.coe_union,

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
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
⊢ p ∈ (span (↑o ∪ ↑⋯.toFinset)).minimalPrimes