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

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝³ : PartialOrder Γ
inst✝² : AddCommMonoid Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x : R⟦Γ⟧
a : Γ
r : R
⊢ (x * (single a) r).cardSupp ≤ x.cardSupp

Tactic:
simpa using

Goal state after:
Γ : Type u_1
R : Type u_2
inst✝³ : PartialOrder Γ
inst✝² : AddCommMonoid Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x : R⟦Γ⟧
a : Γ
r : R
⊢ (x * (single a) r).cardSupp ≤ x.cardSupp
Module: Mathlib.RingTheory.HahnSeries.Cardinal

Goal state before:
pp: case succ
Γ : Type u_1
R : Type u_2
inst✝³ : PartialOrder Γ
inst✝² : AddCommMonoid Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : Semiring R
x : R⟦Γ⟧
n : ℕ
IH : (x ^ n).cardSupp ≤ x.cardSupp ^ n
⊢ (x ^ (n + 1)).cardSupp ≤ x.cardSupp ^ (n + 1)

Tactic:
simpa using

Goal state after:
case succ
Γ : Type u_1
R : Type u_2
inst✝³ : PartialOrder Γ
inst✝² : AddCommMonoid Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : Semiring R
x : R⟦Γ⟧
n : ℕ
IH : (x ^ n).cardSupp ≤ x.cardSupp ^ n
⊢ (x ^ n * x).cardSupp ≤ x.cardSupp ^ n * x.cardSupp
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: case pos.refine_1
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
hx : 0 < x.orderTop
g : Γ
hpwo : (⋃ n, (x ^ n).support).IsPWO
h0 : ¬x = 0
hg : g ∈ ⋃ n, {g | (x ^ n).coeff g ≠ 0}
y : Γ
ys : y ∈ ⋃ n, (x ^ n).support
hy : ∀ z ∈ ⋃ n, (x ^ n).support, z < y → {a | ((fun n ↦ x ^ n) a).coeff z ≠ 0}.Finite
ij : Γ × Γ
hij : ij ∈ ↑(antidiagonal ⋯ hpwo y)
⊢ ij.2 < y

pp: case pos.refine_2
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
hx : 0 < x.orderTop
g : Γ
hpwo : (⋃ n, (x ^ n).support).IsPWO
h0 : ¬x = 0
hg : g ∈ ⋃ n, {g | (x ^ n).coeff g ≠ 0}
y : Γ
ys : y ∈ ⋃ n, (x ^ n).support
hy : ∀ z ∈ ⋃ n, (x ^ n).support, z < y → {a | ((fun n ↦ x ^ n) a).coeff z ≠ 0}.Finite
⊢ {a | ((fun n ↦ x ^ n) a).coeff y ≠ 0} ⊆
    (Nat.succ '' ⋃ i ∈ ↑(antidiagonal ⋯ hpwo y), {a | ((fun n ↦ x ^ n) a).coeff i.2 ≠ 0}) ∪ {0}

Tactic:
· obtain ⟨hi, _, rfl⟩ := mem_antidiagonal.1 (mem_coe.1 hij)
    exact lt_add_of_pos_left ij.2 <| lt_of_lt_of_le ((zero_lt_orderTop_iff h0).mp hx) <|
      order_le_of_coeff_ne_zero <| Function.mem_support.mp hi

Goal state after:
case pos.refine_2
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
hx : 0 < x.orderTop
g : Γ
hpwo : (⋃ n, (x ^ n).support).IsPWO
h0 : ¬x = 0
hg : g ∈ ⋃ n, {g | (x ^ n).coeff g ≠ 0}
y : Γ
ys : y ∈ ⋃ n, (x ^ n).support
hy : ∀ z ∈ ⋃ n, (x ^ n).support, z < y → {a | ((fun n ↦ x ^ n) a).coeff z ≠ 0}.Finite
⊢ {a | ((fun n ↦ x ^ n) a).coeff y ≠ 0} ⊆
    (Nat.succ '' ⋃ i ∈ ↑(antidiagonal ⋯ hpwo y), {a | ((fun n ↦ x ^ n) a).coeff i.2 ≠ 0}) ∪ {0}
Module: Mathlib.RingTheory.HahnSeries.Cardinal

Goal state before:
pp: Γ : Type u_1
R : Type u_2
S : Type u_3
α : Type u_4
κ : Cardinal.{u_1}
inst✝¹ : PartialOrder Γ
inst✝ : AddMonoid R
hκ : Fact (ℵ₀ ≤ κ)
⊢ 0 ∈ {x | x.cardSupp < κ}

Tactic:
simpa using

Goal state after:
Γ : Type u_1
R : Type u_2
S : Type u_3
α : Type u_4
κ : Cardinal.{u_1}
inst✝¹ : PartialOrder Γ
inst✝ : AddMonoid R
hκ : Fact (ℵ₀ ≤ κ)
⊢ 0 < κ
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
⊢ ∃ a, f.IsRoot a ∧ a - a₀ ∈ I

Tactic:
let c : ℕ → R := fun n => Nat.recOn n a₀ fun _ b => b - f.eval b * (f'.eval b)⁻¹ʳ

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')⁻¹ʳ
⊢ ∃ a, f.IsRoot a ∧ a - a₀ ∈ I
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommGroup Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedAddMonoid Γ
inst✝ : Field R
m : ℕ
e : Bool
s : ℕ
⊢ (single 0) (OfScientific.ofScientific m e s) = OfScientific.ofScientific m e s

Tactic:
simpa using

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommGroup Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedAddMonoid Γ
inst✝ : Field R
m : ℕ
e : Bool
s : ℕ
⊢ (single 0) (OfScientific.ofScientific m e s) = OfScientific.ofScientific m e s
Module: Mathlib.RingTheory.HopfAlgebra.MonoidAlgebra

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : HopfAlgebra R A
G : Type u_3
inst✝ : Group G
a : G
b : A
⊢ ((LinearMap.mul' R A[G] ∘ₗ LinearMap.rTensor A[G] (antipode R) ∘ₗ comul) ∘ₗ lsingle a) b =
    ((Algebra.linearMap R A[G] ∘ₗ counit) ∘ₗ lsingle a) b

Tactic:
simpa using

Goal state after:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : HopfAlgebra R A
G : Type u_3
inst✝ : Group G
a : G
b : A
⊢ ∑ x ∈ (ℛ R b).index, single 1 ((antipode R) ((ℛ R b).left x) * (ℛ R b).right x) =
    single 1 ((algebraMap R A) (counit b))
Module: Mathlib.RingTheory.HopfAlgebra.MonoidAlgebra

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : HopfAlgebra R A
G : Type u_3
inst✝ : Group G
a : G
b : A
⊢ ((LinearMap.mul' R A[G] ∘ₗ LinearMap.lTensor A[G] (antipode R) ∘ₗ comul) ∘ₗ lsingle a) b =
    ((Algebra.linearMap R A[G] ∘ₗ counit) ∘ₗ lsingle a) b

Tactic:
simpa using

Goal state after:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : HopfAlgebra R A
G : Type u_3
inst✝ : Group G
a : G
b : A
⊢ ∑ x ∈ (ℛ R b).index, single 1 ((ℛ R b).left x * (antipode R) ((ℛ R b).right x)) =
    single 1 ((algebraMap R A) (counit b))
Module: Mathlib.RingTheory.Ideal.HasGoingUp

Goal state before:
pp: case singleton
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.HasGoingUp R S
q : PrimeSpectrum R
P : Ideal S
inst✝ : P.IsPrime
lo : P.LiesOver (RelSeries.singleton {(a, b) | a < b} q).head.asIdeal
⊢ List.map (PrimeSpectrum.comap (algebraMap R S))
      (RelSeries.singleton {(a, b) | a < b} { asIdeal := P, isPrime := ⋯ }).toList =
    (RelSeries.singleton {(a, b) | a < b} q).toList

Tactic:
simpa using

Goal state after:
case singleton
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.HasGoingUp R S
q : PrimeSpectrum R
P : Ideal S
inst✝ : P.IsPrime
lo : P.LiesOver (RelSeries.singleton {(a, b) | a < b} q).head.asIdeal
⊢ comap (algebraMap R S) P = q.asIdeal
Module: Mathlib.RingTheory.Ideal.HasGoingUp

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.HasGoingUp R S
l : RelSeries {(a, b) | a < b}
q : PrimeSpectrum R
lt : (q, l.head) ∈ {(a, b) | a < b}
ih :
  ∀ (P : Ideal S) [inst : P.IsPrime] [lo : P.LiesOver l.head.asIdeal],
    ∃ L,
      L.length = l.length ∧
        RelSeries.head L = { asIdeal := P, isPrime := ⋯ } ∧
          List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.toList L) = l.toList
P : Ideal S
inst✝ : P.IsPrime
lo : P.LiesOver q.asIdeal
Q : Ideal S
PQlt : P < Q
hQ : Q.IsPrime
Qlo : Q.LiesOver l.head.asIdeal
L : LTSeries (PrimeSpectrum S)
len : L.length = l.length
head : RelSeries.head L = { asIdeal := Q, isPrime := ⋯ }
spec : List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.toList L) = l.toList
⊢ (RelSeries.cons L { asIdeal := P, isPrime := ⋯ } ⋯).length = (l.cons q lt).length

Tactic:
simpa using

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.HasGoingUp R S
l : RelSeries {(a, b) | a < b}
q : PrimeSpectrum R
lt : (q, l.head) ∈ {(a, b) | a < b}
ih :
  ∀ (P : Ideal S) [inst : P.IsPrime] [lo : P.LiesOver l.head.asIdeal],
    ∃ L,
      L.length = l.length ∧
        RelSeries.head L = { asIdeal := P, isPrime := ⋯ } ∧
          List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.toList L) = l.toList
P : Ideal S
inst✝ : P.IsPrime
lo : P.LiesOver q.asIdeal
Q : Ideal S
PQlt : P < Q
hQ : Q.IsPrime
Qlo : Q.LiesOver l.head.asIdeal
L : LTSeries (PrimeSpectrum S)
len : L.length = l.length
head : RelSeries.head L = { asIdeal := Q, isPrime := ⋯ }
spec : List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.toList L) = l.toList
⊢ L.length = l.length
Module: Mathlib.RingTheory.Ideal.HasGoingUp

Goal state before:
pp: case cons
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.HasGoingUp R S
l : RelSeries {(a, b) | a < b}
q : PrimeSpectrum R
lt : (q, l.head) ∈ {(a, b) | a < b}
ih :
  ∀ (P : Ideal S) [inst : P.IsPrime] [lo : P.LiesOver l.head.asIdeal],
    ∃ L,
      L.length = l.length ∧
        RelSeries.head L = { asIdeal := P, isPrime := ⋯ } ∧
          List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.toList L) = l.toList
P : Ideal S
inst✝ : P.IsPrime
lo : P.LiesOver q.asIdeal
Q : Ideal S
PQlt : P < Q
hQ : Q.IsPrime
Qlo : Q.LiesOver l.head.asIdeal
L : LTSeries (PrimeSpectrum S)
len : L.length = l.length
head : RelSeries.head L = { asIdeal := Q, isPrime := ⋯ }
spec : List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.toList L) = l.toList
⊢ List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.cons L { asIdeal := P, isPrime := ⋯ } ⋯).toList =
    (l.cons q lt).toList

Tactic:
simpa using

Goal state after:
case cons
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.HasGoingUp R S
l : RelSeries {(a, b) | a < b}
q : PrimeSpectrum R
lt : (q, l.head) ∈ {(a, b) | a < b}
ih :
  ∀ (P : Ideal S) [inst : P.IsPrime] [lo : P.LiesOver l.head.asIdeal],
    ∃ L,
      L.length = l.length ∧
        RelSeries.head L = { asIdeal := P, isPrime := ⋯ } ∧
          List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.toList L) = l.toList
P : Ideal S
inst✝ : P.IsPrime
lo : P.LiesOver q.asIdeal
Q : Ideal S
PQlt : P < Q
hQ : Q.IsPrime
Qlo : Q.LiesOver l.head.asIdeal
L : LTSeries (PrimeSpectrum S)
len : L.length = l.length
head : RelSeries.head L = { asIdeal := Q, isPrime := ⋯ }
spec : List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.toList L) = l.toList
⊢ comap (algebraMap R S) P = q.asIdeal
Module: Mathlib.RingTheory.Ideal.HasGoingUp

Goal state before:
pp: case refine_2
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : SpecializingMap (PrimeSpectrum.comap (algebraMap R S))
q : Ideal R
hq : q.IsPrime
P : Ideal S
hP : P.IsPrime
hlt : Ideal.under R P < q
this : PrimeSpectrum.comap (algebraMap R S) { asIdeal := P, isPrime := hP } ⤳ { asIdeal := q, isPrime := hq }
Q : PrimeSpectrum S
hs : flip (fun x1 x2 ↦ x1 ⤳ x2) Q { asIdeal := P, isPrime := hP }
heq : PrimeSpectrum.comap (algebraMap R S) Q = { asIdeal := q, isPrime := hq }
⊢ q = Ideal.under R Q.asIdeal

Tactic:
simpa using

Goal state after:
case refine_2
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : SpecializingMap (PrimeSpectrum.comap (algebraMap R S))
q : Ideal R
hq : q.IsPrime
P : Ideal S
hP : P.IsPrime
hlt : Ideal.under R P < q
this : PrimeSpectrum.comap (algebraMap R S) { asIdeal := P, isPrime := hP } ⤳ { asIdeal := q, isPrime := hq }
Q : PrimeSpectrum S
hs : flip (fun x1 x2 ↦ x1 ⤳ x2) Q { asIdeal := P, isPrime := hP }
heq : PrimeSpectrum.comap (algebraMap R S) Q = { asIdeal := q, isPrime := hq }
⊢ q = Ideal.under R Q.asIdeal
Module: Mathlib.RingTheory.Ideal.MonicSpan

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
p : Ideal R[X]
ism : (comap C p).IsMaximal
ne : p ≠ Ideal.map C (comap C p)
q : Ideal R := comap C p
this✝ : Field (R ⧸ q) := Quotient.field q
ne' : Ideal.map (mapRingHom (Ideal.Quotient.mk q)) p ≠ ⊥
y : (R ⧸ q)[X]
mony : y.Monic
hy : Ideal.map (mapRingHom (Ideal.Quotient.mk q)) p = span {y}
this : y ∈ lifts (Ideal.Quotient.mk q)
f : R[X]
hf : map (Ideal.Quotient.mk q) f = y
deg : f.natDegree = y.natDegree
monf : f.Monic
⊢ p = p ⊔ RingHom.ker (mapRingHom (Ideal.Quotient.mk q))

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝ : CommRing R
p : Ideal R[X]
ism : (comap C p).IsMaximal
ne : p ≠ Ideal.map C (comap C p)
q : Ideal R := comap C p
this✝ : Field (R ⧸ q) := Quotient.field q
ne' : Ideal.map (mapRingHom (Ideal.Quotient.mk q)) p ≠ ⊥
y : (R ⧸ q)[X]
mony : y.Monic
hy : Ideal.map (mapRingHom (Ideal.Quotient.mk q)) p = span {y}
this : y ∈ lifts (Ideal.Quotient.mk q)
f : R[X]
hf : map (Ideal.Quotient.mk q) f = y
deg : f.natDegree = y.natDegree
monf : f.Monic
⊢ Ideal.map C (comap C p) ≤ p
Module: Mathlib.RingTheory.IdealFilter.Basic

Goal state before:
pp: A : Type u_1
inst✝ : Ring A
F : IdealFilter A
L K : Ideal A
h : F.IsTorsionQuot (L ⊓ K) K
k : A
hk : k ∈ K
I : Ideal A
hI : I ∈ F
hI_le : I ≤ Submodule.colon (L ⊓ K) {k}
hcol : Submodule.colon (L ⊓ K) {k} = Submodule.colon L {k}
⊢ I ≤ Submodule.colon L {k}

Tactic:
simpa using

Goal state after:
A : Type u_1
inst✝ : Ring A
F : IdealFilter A
L K : Ideal A
h : F.IsTorsionQuot (L ⊓ K) K
k : A
hk : k ∈ K
I : Ideal A
hI : I ∈ F
hI_le : I ≤ Submodule.colon (L ⊓ K) {k}
hcol : Submodule.colon (L ⊓ K) {k} = Submodule.colon L {k}
⊢ I ≤ Submodule.colon L {k}
Module: Mathlib.RingTheory.IdealFilter.Basic

Goal state before:
pp: A : Type u_1
inst✝ : Ring A
F : IdealFilter A
L K : Ideal A
h : F.IsTorsionQuot L K
k : A
hk : k ∈ K
I : Ideal A
hI : I ∈ F
hI_le : I ≤ Submodule.colon L {k}
hcol : Submodule.colon (L ⊓ K) {k} = Submodule.colon L {k}
⊢ I ≤ Submodule.colon (L ⊓ K) {k}

Tactic:
simpa using

Goal state after:
A : Type u_1
inst✝ : Ring A
F : IdealFilter A
L K : Ideal A
h : F.IsTorsionQuot L K
k : A
hk : k ∈ K
I : Ideal A
hI : I ∈ F
hI_le : I ≤ Submodule.colon L {k}
hcol : Submodule.colon (L ⊓ K) {k} = Submodule.colon L {k}
⊢ I ≤ Submodule.colon L {k}
Module: Mathlib.RingTheory.IdealFilter.Topology

Goal state before:
pp: A : Type u_1
inst✝ : Ring A
F : IdealFilter A
x✝ : ∃ B, B.sets = {x | ∃ I ∈ F, ↑I = x}
B : RingFilterBasis A
hB : B.sets = {x | ∃ I ∈ F, ↑I = x}
I : Ideal A
hI : I ∈ F
a : A
J : Ideal A
hJ : J ∈ F
hbasis : ↑J ∈ B
hsub : ↑J ⊆ (fun x ↦ x * a) ⁻¹' ↑I
x : A
hx : x ∈ J
⊢ x ∈ Submodule.colon I {a}

Tactic:
simpa using

Goal state after:
A : Type u_1
inst✝ : Ring A
F : IdealFilter A
x✝ : ∃ B, B.sets = {x | ∃ I ∈ F, ↑I = x}
B : RingFilterBasis A
hB : B.sets = {x | ∃ I ∈ F, ↑I = x}
I : Ideal A
hI : I ∈ F
a : A
J : Ideal A
hJ : J ∈ F
hbasis : ↑J ∈ B
hsub : ↑J ⊆ (fun x ↦ x * a) ⁻¹' ↑I
x : A
hx : x ∈ J
⊢ x * a ∈ I
Module: Mathlib.RingTheory.IdealFilter.Basic

Goal state before:
pp: A : Type u_1
inst✝ : Ring A
F G : IdealFilter A
⊢ Order.IsPFilter {L | ∃ K ∈ G, F.IsTorsionQuot L K}

Tactic:
refine Order.IsPFilter.of_def ?nonempty ?directed ?mem_of_le
  · obtain ⟨J, hJ⟩ := G.nonempty
    exact ⟨J, J, hJ, isTorsionQuot_self F J⟩
  · rintro I ⟨K, hK, hIK⟩ J ⟨L, hL, hJL⟩
    refine ⟨I ⊓ J, ?_, inf_le_left, inf_le_right⟩
    exact ⟨K ⊓ L, G.inf_mem hK hL,
      (hIK.anti_right inf_le_left).inf (hJL.anti_right inf_le_right)⟩
  · intro I J hIJ ⟨K, hK, hIK⟩
    exact ⟨K, hK, hIK.mono_left hIJ⟩

Goal state after:
Module: Mathlib.RingTheory.IdealFilter.Topology

Goal state before:
pp: A : Type u_1
inst✝ : Ring A
F : IdealFilter A
s : Set (WithIdealFilter F)
⊢ s ∈ 𝓝 0 ↔ ∃ I ∈ F, idealSet I ⊆ s

Tactic:
simpa using

Goal state after:
A : Type u_1
inst✝ : Ring A
F : IdealFilter A
s : Set (WithIdealFilter F)
⊢ s ∈ 𝓝 0 ↔ ∃ I ∈ F, idealSet I ⊆ s
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
q p : Ideal R
inst✝ : q.IsPrime
hqp : q < p
x : R
s : Set R
hp : p ∈ (span (insert x s)).minimalPrimes
t : Set R
htq : t ⊆ ↑q
hsp : s ⊆ ↑(span (insert x t)).radical
f : R →+* R ⧸ span t := Quotient.mk (span t)
hf : Function.Surjective ⇑f
hI'q : span t ≤ q
hI'p : span t ≤ p
this✝ : p.IsPrime
this : (map f p).IsPrime
h : (map f p).height ≤ 1
e : map f p ≤ map f q
⊢ p ≤ q

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
q p : Ideal R
inst✝ : q.IsPrime
hqp : q < p
x : R
s : Set R
hp : p ∈ (span (insert x s)).minimalPrimes
t : Set R
htq : t ⊆ ↑q
hsp : s ⊆ ↑(span (insert x t)).radical
f : R →+* R ⧸ span t := Quotient.mk (span t)
hf : Function.Surjective ⇑f
hI'q : span t ≤ q
hI'p : span t ≤ p
this✝ : p.IsPrime
this : (map f p).IsPrime
h : (map f p).height ≤ 1
e : map f p ≤ map f q
⊢ p ≤ q
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
p : Ideal R
s : Finset R
this✝ : p.IsPrime
hp : maximalIdeal (Localization p.primeCompl) ∈ (span (⇑(algebraMap R (Localization p.primeCompl)) '' ↑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) ∈
    (span ↑(Finset.image (⇑(algebraMap R (Localization p.primeCompl))) s)).minimalPrimes

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
p : Ideal R
s : Finset R
this✝ : p.IsPrime
hp : maximalIdeal (Localization p.primeCompl) ∈ (span (⇑(algebraMap R (Localization p.primeCompl)) '' ↑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
⊢ (span (⇑(algebraMap R (Localization p.primeCompl)) '' ↑s)).IsMinimalPrime (maximalIdeal (Localization p.primeCompl))
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
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
w✝ : IsLocalRing R
this✝ : (maximalIdeal R).IsPrime
q : Ideal R
hq✝ : q.IsPrime
hpq : q < maximalIdeal R
hq' : ∀ (q' : Ideal R), q'.IsPrime → q < q' → ¬q' < maximalIdeal R
x : R
s' : Finset R
hxs' : x ∉ s'
hxq : x ∉ q
hn : (insert x s').card ≤ n + 1
hp : maximalIdeal R ∈ (span ↑(insert x s')).minimalPrimes
this : maximalIdeal R ≤ (q ⊔ span {x}).radical
h : ↑s' ⊆ ↑(q ⊔ span {x}).radical
t✝ : ↑↑s' → R
ht : Set.range t✝ ⊆ ↑q
hspan : ↑s' ⊆ ↑(span (Set.range t✝) ⊔ span {x}).radical
t : Finset R := Finset.image t✝ Finset.univ
hq : q ∈ (span ↑t).minimalPrimes
⊢ Finset.univ.card < (insert x s').card

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
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
w✝ : IsLocalRing R
this✝ : (maximalIdeal R).IsPrime
q : Ideal R
hq✝ : q.IsPrime
hpq : q < maximalIdeal R
hq' : ∀ (q' : Ideal R), q'.IsPrime → q < q' → ¬q' < maximalIdeal R
x : R
s' : Finset R
hxs' : x ∉ s'
hxq : x ∉ q
hn : (insert x s').card ≤ n + 1
hp : maximalIdeal R ∈ (span ↑(insert x s')).minimalPrimes
this : maximalIdeal R ≤ (q ⊔ span {x}).radical
h : ↑s' ⊆ ↑(q ⊔ span {x}).radical
t✝ : ↑↑s' → R
ht : Set.range t✝ ⊆ ↑q
hspan : ↑s' ⊆ ↑(span (Set.range t✝) ⊔ span {x}).radical
t : Finset R := Finset.image t✝ Finset.univ
hq : q ∈ (span ↑t).minimalPrimes
⊢ s'.card < (insert x s').card
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)
⊢ RingHom.ker (Ideal.Quotient.mk P) ≤ I

Tactic:
simpa using

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)
⊢ 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
this : (Ideal.comap (Ideal.Quotient.mk P) (Ideal.map (Ideal.Quotient.mk P) I)).IsMaximal
⊢ I.IsMaximal

Tactic:
simpa using

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.KrullDimension.PID

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
m : Ideal R
inst✝ : m.IsMaximal
h : ¬IsField R
⊢ m.height = 1

Tactic:
refine le_antisymm ?_ ?_
  · suffices h : (m.height : WithBot ℕ∞) ≤ 1 by norm_cast at h
    rw [← IsPrincipalIdealRing.ringKrullDim_eq_one _ h]
    exact Ideal.height_le_ringKrullDim_of_ne_top Ideal.IsPrime.ne_top'
  · apply le_of_eq_of_le _ (Ideal.height_add_one_le_of_lt_of_isPrime (Ideal.bot_lt_of_maximal m h))
    simp

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
p : Ideal R
s : Finset R
hI : p ∈ (span ↑s).minimalPrimes
⊢ Cardinal.toENat (Submodule.spanRank (span ↑s)) ≤ ↑s.card

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
p : Ideal R
s : Finset R
hI : p ∈ (span ↑s).minimalPrimes
⊢ Submodule.spanRank (span ↑s) ≤ ↑s.card
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
p : Ideal R
inst✝ : p.IsPrime
n : ℕ∞
I : Ideal R
hp : p ∈ I.minimalPrimes
hI : Submodule.spanRank I ≤ ↑n
⊢ Cardinal.toENat (Submodule.spanRank I) ≤ n

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
p : Ideal R
inst✝ : p.IsPrime
n : ℕ∞
I : Ideal R
hp : p ∈ I.minimalPrimes
hI : Submodule.spanRank I ≤ ↑n
⊢ Cardinal.toENat (Submodule.spanRank I) ≤ n
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
⊢ Cardinal.toENat (Submodule.spanRank I) = ↑(Submodule.spanFinrank I)

Tactic:
simpa using

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
⊢ Submodule.FG I