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

Goal state before:
pp: case refine_2
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsLocalRing A
g q : A⟦X⟧
r : A[X]
hg : (map (IsLocalRing.residue A)) g ≠ 0
H✝ : (X ^ ((map (IsLocalRing.residue A)) g).order.toNat).IsWeierstrassDivision g q r
n : ℕ := ((map (IsLocalRing.residue A)) g).order.toNat
H : (X ^ n).IsWeierstrassDivision g q r
f : A[X] := Polynomial.X ^ n - r
H1 : r.degree < (Polynomial.X ^ n).degree
hfdeg : f.natDegree = n
this : X ^ n * ↑⋯.unit⁻¹ - ↑r * ↑⋯.unit⁻¹ = g
⊢ g = ↑f * ↑⋯.unit⁻¹

Tactic:
]

Goal state after:
case refine_2
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsLocalRing A
g q : A⟦X⟧
r : A[X]
hg : (map (IsLocalRing.residue A)) g ≠ 0
H✝ : (X ^ ((map (IsLocalRing.residue A)) g).order.toNat).IsWeierstrassDivision g q r
n : ℕ := ((map (IsLocalRing.residue A)) g).order.toNat
H : (X ^ n).IsWeierstrassDivision g q r
f : A[X] := Polynomial.X ^ n - r
H1 : r.degree < (Polynomial.X ^ n).degree
hfdeg : f.natDegree = n
this : X ^ n * ↑⋯.unit⁻¹ - ↑r * ↑⋯.unit⁻¹ = g
⊢ g = ↑f * ↑⋯.unit⁻¹
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: R : Type u_2
M : Type u
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
⊢ IsIsotypic R ↥N ↔
    ∀ (a : Submodule R ↥N) [IsSimpleModule R ↥↑((Submodule.MapSubtype.orderIso N).toEquiv a)],
      IsIsotypicOfType R ↥N ↥↑((Submodule.MapSubtype.orderIso N).toEquiv a)

Tactic:
]

Goal state after:
R : Type u_2
M : Type u
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
⊢ IsIsotypic R ↥N ↔
    ∀ (a : Submodule R ↥N) [IsSimpleModule R ↥↑((Submodule.MapSubtype.orderIso N).toEquiv a)],
      IsIsotypicOfType R ↥N ↥↑((Submodule.MapSubtype.orderIso N).toEquiv a)
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: R : Type u_2
M : Type u
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsSemisimpleModule R M
inst✝ : Nontrivial M
h : IsIsotypic R M
S : Submodule R M
hS : IsSimpleModule R ↥S
⊢ ∃ ι, ∃ (_ : Nonempty ι), ∃ S, IsSimpleModule R ↥S ∧ Nonempty (M ≃ₗ[R] ι →₀ ↥S)

Tactic:
]

Goal state after:
R : Type u_2
M : Type u
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsSemisimpleModule R M
inst✝ : Nontrivial M
h : IsIsotypic R M
S : Submodule R M
hS : IsSimpleModule R ↥S
⊢ ∃ ι, ∃ (_ : Nonempty ι), ∃ S, IsSimpleModule R ↥S ∧ Nonempty (M ≃ₗ[R] ι →₀ ↥S)
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: R : Type u_2
M : Type u
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsSemisimpleModule R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
h : IsIsotypic R M
S : Submodule R M
hS : IsSimpleModule R ↥S
⊢ ∃ n, ∃ (_ : NeZero n), ∃ S, IsSimpleModule R ↥S ∧ Nonempty (M ≃ₗ[R] Fin n → ↥S)

Tactic:
]

Goal state after:
R : Type u_2
M : Type u
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsSemisimpleModule R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
h : IsIsotypic R M
S : Submodule R M
hS : IsSimpleModule R ↥S
⊢ ∃ n, ∃ (_ : NeZero n), ∃ S, IsSimpleModule R ↥S ∧ Nonempty (M ≃ₗ[R] Fin n → ↥S)
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: R₀ : Type u_1
R : Type u_2
M : Type u
N : Type u_3
S : Type u_4
inst✝⁹ : CommSemiring R₀
inst✝⁸ : Ring R
inst✝⁷ : Algebra R₀ R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup S
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R S
inst✝ : IsSemisimpleModule R S
⊢ IsSemisimpleModule R ↥(⨆ a ∈ {m | Nonempty (↥m ≃ₗ[R] S)}, a)

Tactic:
]

Goal state after:
R₀ : Type u_1
R : Type u_2
M : Type u
N : Type u_3
S : Type u_4
inst✝⁹ : CommSemiring R₀
inst✝⁸ : Ring R
inst✝⁷ : Algebra R₀ R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup S
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R S
inst✝ : IsSemisimpleModule R S
⊢ IsSemisimpleModule R ↥(⨆ a ∈ {m | Nonempty (↥m ≃ₗ[R] S)}, a)
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: case degree_lt.refine_2
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsLocalRing A
g : A⟦X⟧
f : A[X]
h : A⟦X⟧
H : g.IsWeierstrassFactorization f h
n : ℕ := ((map (IsLocalRing.residue A)) g).order.toNat
hn : n = ((map (IsLocalRing.residue A)) g).order.toNat
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: R : Type u_2
M : Type u
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
N : Submodule R M
inst✝ : IsSimpleModule R ↥N
s : Set (Submodule R M)
hs : ∀ (m : ↑s), IsSemisimpleModule R ↥↑m
hN : N ≤ ⨆ a ∈ s, a
⊢ ∃ m ∈ s, ∃ S ≤ m, Nonempty (↥N ≃ₗ[R] ↥S)

Tactic:
]

Goal state after:
R : Type u_2
M : Type u
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
N : Submodule R M
inst✝ : IsSimpleModule R ↥N
s : Set (Submodule R M)
hs : ∀ (m : ↑s), IsSemisimpleModule R ↥↑m
hN : N ≤ ⨆ a ∈ s, a
⊢ ∃ m ∈ s, ∃ S ≤ m, Nonempty (↥N ≃ₗ[R] ↥S)
Module: Mathlib.RingTheory.RegularLocalRing.Polynomial

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsRegularLocalRing R
p : Ideal R[X]
inst✝ : p.IsPrime
max : comap C p = maximalIdeal R
q : Ideal R[X] := Ideal.map C (maximalIdeal R)
qle : q ≤ p
reg : ↑(Submodule.spanFinrank (maximalIdeal R)) = ringKrullDim R
fg' : (maximalIdeal R).FG
fg : (Submodule.generators (maximalIdeal R)).Finite
ht : (maximalIdeal R).height ≤ q.height
eq : ¬p = q
lt : q < p
this : (comap C p).IsMaximal
y : R[X]
left✝ : y.Monic
hy : p = Ideal.map C (comap C p) ⊔ span {y}
peq : p = span (⇑(algebraMap R R[X]) '' Submodule.generators (maximalIdeal R) ∪ {y})
fin : (⇑(algebraMap R R[X]) '' Submodule.generators (maximalIdeal R) ∪ {y}).Finite
⊢ (⇑(algebraMap R R[X]) '' Submodule.generators (maximalIdeal R)).ncard ≤ (Submodule.generators (maximalIdeal R)).ncard

Tactic:
]

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsRegularLocalRing R
p : Ideal R[X]
inst✝ : p.IsPrime
max : comap C p = maximalIdeal R
q : Ideal R[X] := Ideal.map C (maximalIdeal R)
qle : q ≤ p
reg : ↑(Submodule.spanFinrank (maximalIdeal R)) = ringKrullDim R
fg' : (maximalIdeal R).FG
fg : (Submodule.generators (maximalIdeal R)).Finite
ht : (maximalIdeal R).height ≤ q.height
eq : ¬p = q
lt : q < p
this : (comap C p).IsMaximal
y : R[X]
left✝ : y.Monic
hy : p = Ideal.map C (comap C p) ⊔ span {y}
peq : p = span (⇑(algebraMap R R[X]) '' Submodule.generators (maximalIdeal R) ∪ {y})
fin : (⇑(algebraMap R R[X]) '' Submodule.generators (maximalIdeal R) ∪ {y}).Finite
⊢ (⇑(algebraMap R R[X]) '' Submodule.generators (maximalIdeal R)).ncard ≤ (Submodule.generators (maximalIdeal R)).ncard
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
inst✝ : IsHausdorff (IsLocalRing.maximalIdeal A) A
g : A⟦X⟧
f f' : A[X]
h h' : A⟦X⟧
H : g.IsWeierstrassFactorization f h
H2 : g.IsWeierstrassFactorization f' h'
h1 : ↑⋯.unit = ↑⋯.unit
h2 :
  Polynomial.X ^ ((map (IsLocalRing.residue A)) g).order.toNat - f =
    Polynomial.X ^ ((map (IsLocalRing.residue A)) g).order.toNat - f'
⊢ f = f' ∧ h = h'

Tactic:
]

Goal state after:
A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
inst✝ : IsHausdorff (IsLocalRing.maximalIdeal A) A
g : A⟦X⟧
f f' : A[X]
h h' : A⟦X⟧
H : g.IsWeierstrassFactorization f h
H2 : g.IsWeierstrassFactorization f' h'
h1 : ↑⋯.unit = ↑⋯.unit
h2 :
  Polynomial.X ^ ((map (IsLocalRing.residue A)) g).order.toNat - f =
    Polynomial.X ^ ((map (IsLocalRing.residue A)) g).order.toNat - f'
⊢ f = f' ∧ h = h'
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: R : Type u_2
M : Type u
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
N : Submodule R M
inst✝ : IsSimpleModule R ↥N
s : Set (Submodule R M)
hs : ∀ (m : ↑s), IsSemisimpleModule R ↥↑m
hN : N ≤ ⨆ a ∈ s, a
e : ↥N ≃ₗ[R] ↥(inclusion hN).range
this✝ : IsSimpleModule R ↥(inclusion hN).range
this : IsSemisimpleModule R ↥(⨆ i ∈ s, i)
⊢ ⊤ = ⊤

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.RegularLocalRing.Polynomial

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsRegularRing R
p : Ideal R[X]
hp : p.IsPrime
q : Ideal R := comap C p
S : Type u_1 := (Localization.AtPrime q)[X]
pc : Submonoid R[X] := Submonoid.map (↑C) q.primeCompl
this✝³ : Algebra R[X] S := algebra R (Localization.AtPrime q)
this✝² : IsLocalization pc S
pS : Ideal S := Ideal.map (algebraMap R[X] S) p
disj : Disjoint ↑pc ↑p
this✝¹ : pS.IsPrime
this✝ : IsLocalization.AtPrime (Localization.AtPrime pS) p
this : IsRegularLocalRing (Localization.AtPrime q)
⊢ Ideal.map (algebraMap R (Localization.AtPrime q)) (under R (comap C pS)) =
    Ideal.map (algebraMap R (Localization.AtPrime q)) (under R (maximalIdeal (Localization.AtPrime q)))

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsRegularRing R
p : Ideal R[X]
hp : p.IsPrime
q : Ideal R := comap C p
S : Type u_1 := (Localization.AtPrime q)[X]
pc : Submonoid R[X] := Submonoid.map (↑C) q.primeCompl
this✝³ : Algebra R[X] S := algebra R (Localization.AtPrime q)
this✝² : IsLocalization pc S
pS : Ideal S := Ideal.map (algebraMap R[X] S) p
disj : Disjoint ↑pc ↑p
this✝¹ : pS.IsPrime
this✝ : IsLocalization.AtPrime (Localization.AtPrime pS) p
this : IsRegularLocalRing (Localization.AtPrime q)
⊢ Ideal.map (algebraMap R (Localization.AtPrime q)) (under R (comap C pS)) =
    Ideal.map (algebraMap R (Localization.AtPrime q)) (under R (maximalIdeal (Localization.AtPrime q)))
Module: Mathlib.RingTheory.SimpleRing.DivisionRing

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
hM : IsSimpleModule R M
N : Type v
x✝¹ : AddCommGroup N
x✝ : Module R N
f : M →ₗ[R] N
h : Function.Injective ⇑f
⊢ Function.Injective ⇑f

Tactic:
]

Goal state after:
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
hM : IsSimpleModule R M
N : Type v
x✝¹ : AddCommGroup N
x✝ : Module R N
f : M →ₗ[R] N
h : Function.Injective ⇑f
⊢ Function.Injective ⇑f
Module: Mathlib.RingTheory.RegularLocalRing.Polynomial

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsRegularRing R
p : Ideal R[X]
hp : p.IsPrime
q : Ideal R := comap C p
S : Type u_1 := (Localization.AtPrime q)[X]
pc : Submonoid R[X] := Submonoid.map (↑C) q.primeCompl
this✝³ : Algebra R[X] S := algebra R (Localization.AtPrime q)
this✝² : IsLocalization pc S
pS : Ideal S := Ideal.map (algebraMap R[X] S) p
disj : Disjoint ↑pc ↑p
this✝¹ : pS.IsPrime
this✝ : IsLocalization.AtPrime (Localization.AtPrime pS) p
this : IsRegularLocalRing (Localization.AtPrime q)
⊢ Ideal.map (algebraMap R (Localization.AtPrime q)) (comap (algebraMap R R[X]) p) =
    Ideal.map (algebraMap R (Localization.AtPrime q)) (under R (maximalIdeal (Localization.AtPrime q)))

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsRegularRing R
p : Ideal R[X]
hp : p.IsPrime
q : Ideal R := comap C p
S : Type u_1 := (Localization.AtPrime q)[X]
pc : Submonoid R[X] := Submonoid.map (↑C) q.primeCompl
this✝³ : Algebra R[X] S := algebra R (Localization.AtPrime q)
this✝² : IsLocalization pc S
pS : Ideal S := Ideal.map (algebraMap R[X] S) p
disj : Disjoint ↑pc ↑p
this✝¹ : pS.IsPrime
this✝ : IsLocalization.AtPrime (Localization.AtPrime pS) p
this : IsRegularLocalRing (Localization.AtPrime q)
⊢ Ideal.map (algebraMap R (Localization.AtPrime q)) (comap (algebraMap R R[X]) p) =
    Ideal.map (algebraMap R (Localization.AtPrime q)) (under R (maximalIdeal (Localization.AtPrime q)))
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: R : Type u_2
M : Type u
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
c : Submodule R M
hc : c ∈ isotypicComponents R M
s : Set (Submodule R M) := isotypicComponents R M \ {c}
ne : ¬c ⊓ sSup s = ⊥
this✝² : IsSemisimpleModule R ↥c
this✝¹ : IsSemisimpleModule R ↥(c ⊓ sSup s)
this✝ : ∀ (c : ↑s), IsSemisimpleModule R ↥↑c
S : Submodule R M
le : S ≤ c ⊓ sSup s
right✝ : IsSimpleModule R ↥S
c' : Submodule R M
hc' : c' ∈ s
S' : Submodule R M
le' : S' ≤ c'
e : ↥S ≃ₗ[R] ↥S'
this : IsSimpleModule R ↥S'
⊢ isotypicComponent R M ↥S' ∈ {isotypicComponent R M ↥S}

Tactic:
]

Goal state after:
R : Type u_2
M : Type u
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
c : Submodule R M
hc : c ∈ isotypicComponents R M
s : Set (Submodule R M) := isotypicComponents R M \ {c}
ne : ¬c ⊓ sSup s = ⊥
this✝² : IsSemisimpleModule R ↥c
this✝¹ : IsSemisimpleModule R ↥(c ⊓ sSup s)
this✝ : ∀ (c : ↑s), IsSemisimpleModule R ↥↑c
S : Submodule R M
le : S ≤ c ⊓ sSup s
right✝ : IsSimpleModule R ↥S
c' : Submodule R M
hc' : c' ∈ s
S' : Submodule R M
le' : S' ≤ c'
e : ↥S ≃ₗ[R] ↥S'
this : IsSimpleModule R ↥S'
⊢ isotypicComponent R M ↥S' ∈ {isotypicComponent R M ↥S}
Module: Mathlib.RingTheory.SimpleRing.DivisionRing

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝³ : Ring R
inst✝² : Ring S
e : ModuleCat R ⥤ ModuleCat S
inst✝¹ : e.IsEquivalence
M : ModuleCat R
inst✝ : Simple M
⊢ Simple (e.obj M)

Tactic:
]

Goal state after:
R : Type u_3
S : Type u_4
inst✝³ : Ring R
inst✝² : Ring S
e : ModuleCat R ⥤ ModuleCat S
inst✝¹ : e.IsEquivalence
M : ModuleCat R
inst✝ : Simple M
⊢ Simple (e.obj M)
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: R : Type u_2
M : Type u
S : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup S
inst✝³ : Module R M
inst✝² : Module R S
inst✝¹ : IsSimpleModule R S
inst✝ : IsSemisimpleModule R M
⊢ IsIsotypicOfType R M S ↔ IsIsotypicOfType R M S

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: R : Type u_2
M : Type u
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
m : Submodule R M
h : m.IsFullyInvariant
S : Submodule R M
le : S ≤ m
x✝¹ : IsSimpleModule R ↥S
S' : Submodule R M
x✝ : S' ∈ {m | Nonempty (↥m ≃ₗ[R] ↥S)}
e : ↥S' ≃ₗ[R] ↥S
p : M →ₗ[R] M
eq : p ∘ₗ S.subtype = S'.subtype ∘ₗ ↑e.symm
⊢ S' ≤ S'

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin

Goal state before:
pp: R : Type u
inst✝ : Ring R
right✝ : IsArtinianRing R
this : IsSemisimpleRing R
x✝ : (Nontrivial R ∧ ∀ (I : Ideal R), I.IsTwoSided → I = ⊥ ∨ I = ⊤) ∧ IsArtinianRing R
left✝ : Nontrivial R ∧ ∀ (I : Ideal R), I.IsTwoSided → I = ⊥ ∨ I = ⊤
⊢ Nontrivial R ∧ ∀ (N : Submodule R R), Ideal.IsTwoSided N → N = ⊥ ∨ N = ⊤

Tactic:
]

Goal state after:
R : Type u
inst✝ : Ring R
right✝ : IsArtinianRing R
this : IsSemisimpleRing R
x✝ : (Nontrivial R ∧ ∀ (I : Ideal R), I.IsTwoSided → I = ⊥ ∨ I = ⊤) ∧ IsArtinianRing R
left✝ : Nontrivial R ∧ ∀ (I : Ideal R), I.IsTwoSided → I = ⊥ ∨ I = ⊤
⊢ Nontrivial R ∧ ∀ (N : Submodule R R), Ideal.IsTwoSided N → N = ⊥ ∨ N = ⊤
Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin

Goal state before:
pp: case refine_1
R : Type u
inst✝ : Ring R
right✝ : IsArtinianRing R
this : IsSemisimpleRing R
x✝ : (Nontrivial R ∧ ∀ (I : Ideal R), I.IsTwoSided → I = ⊥ ∨ I = ⊤) ∧ IsArtinianRing R
left✝ : Nontrivial R ∧ ∀ (I : Ideal R), I.IsTwoSided → I = ⊥ ∨ I = ⊤
⊢ IsSemisimpleRing R ∧ (∀ (N : Submodule R R), Ideal.IsTwoSided N → N = ⊥ ∨ N = ⊤) ∧ Nontrivial R

pp: case refine_2
R : Type u
inst✝ : Ring R
left✝¹ : IsSemisimpleRing R
right✝ : Nontrivial R
x✝ : IsSemisimpleRing R ∧ (∀ (N : Submodule R R), Ideal.IsTwoSided N → N = ⊥ ∨ N = ⊤) ∧ Nontrivial R
left✝ : ∀ (N : Submodule R R), Ideal.IsTwoSided N → N = ⊥ ∨ N = ⊤
⊢ (Nontrivial R ∧ ∀ (I : Ideal R), I.IsTwoSided → I = ⊥ ∨ I = ⊤) ∧ IsArtinianRing R

Tactic:
· exact ⟨this, by rwa [and_comm]⟩

Goal state after:
case refine_2
R : Type u
inst✝ : Ring R
left✝¹ : IsSemisimpleRing R
right✝ : Nontrivial R
x✝ : IsSemisimpleRing R ∧ (∀ (N : Submodule R R), Ideal.IsTwoSided N → N = ⊥ ∨ N = ⊤) ∧ Nontrivial R
left✝ : ∀ (N : Submodule R R), Ideal.IsTwoSided N → N = ⊥ ∨ N = ⊤
⊢ (Nontrivial R ∧ ∀ (I : Ideal R), I.IsTwoSided → I = ⊥ ∨ I = ⊤) ∧ IsArtinianRing R
Module: Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
⊢ IsOpen (⋃ i, {x | f.coeff i ∉ x.asIdeal})

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommRing R
f : R[X]
⊢ IsOpen (⋃ i, {x | f.coeff i ∉ x.asIdeal})
Module: Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommRing R
f : R[X]
x : PrimeSpectrum R
hx : x ∈ imageOfDf f
⊢ f ∉ ↑{ asIdeal := Ideal.map C x.asIdeal, isPrime := ⋯ }.asIdeal

Tactic:
]

Goal state after:
case refine_1
R : Type u_1
inst✝ : CommRing R
f : R[X]
x : PrimeSpectrum R
hx : x ∈ imageOfDf f
⊢ f ∉ ↑{ asIdeal := Ideal.map C x.asIdeal, isPrime := ⋯ }.asIdeal
Module: Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : CommRing R
f : R[X]
x✝ : PrimeSpectrum R
hx : x✝ ∈ imageOfDf f
x : R
h : x ∈ (PrimeSpectrum.comap C { asIdeal := Ideal.map C x✝.asIdeal, isPrime := ⋯ }).asIdeal
⊢ (C x).coeff 0 ∈ x✝.asIdeal

Tactic:
]

Goal state after:
case refine_2
R : Type u_1
inst✝ : CommRing R
f : R[X]
x✝ : PrimeSpectrum R
hx : x✝ ∈ imageOfDf f
x : R
h : x ∈ (PrimeSpectrum.comap C { asIdeal := Ideal.map C x✝.asIdeal, isPrime := ⋯ }).asIdeal
⊢ (C x).coeff 0 ∈ x✝.asIdeal
Module: Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
U : Set (PrimeSpectrum R[X])
s : Set R[X]
z : zeroLocus s = Uᶜ
⊢ IsOpen (⋃ i, PrimeSpectrum.comap C '' (zeroLocus {↑i})ᶜ)

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommRing R
U : Set (PrimeSpectrum R[X])
s : Set R[X]
z : zeroLocus s = Uᶜ
⊢ IsOpen (⋃ i, PrimeSpectrum.comap C '' (zeroLocus {↑i})ᶜ)
Module: Mathlib.RingTheory.TwoSidedIdeal.BigOperators

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
ι : Type u_2
l : List ι
f : ι → R
hl : ∀ x ∈ l, f x ∈ I
⊢ I.ringCon (List.map f l).sum (List.map (fun x ↦ 0) ?m.26).sum

pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
ι : Type u_2
l : List ι
f : ι → R
hl : ∀ x ∈ l, f x ∈ I
⊢ Type ?u.29

pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
ι : Type u_2
l : List ι
f : ι → R
hl : ∀ x ∈ l, f x ∈ I
⊢ List ?m.23

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
ι : Type u_2
l : List ι
f : ι → R
hl : ∀ x ∈ l, f x ∈ I
⊢ I.ringCon (List.map f l).sum (List.map (fun x ↦ 0) ?m.26).sum

R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
ι : Type u_2
l : List ι
f : ι → R
hl : ∀ x ∈ l, f x ∈ I
⊢ Type ?u.29

R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
ι : Type u_2
l : List ι
f : ι → R
hl : ∀ x ∈ l, f x ∈ I
⊢ List ?m.23
Module: Mathlib.RingTheory.TwoSidedIdeal.BigOperators

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
ι : Type u_2
s : Multiset ι
f : ι → R
hs : ∀ x ∈ s, f x ∈ I
⊢ I.ringCon (Multiset.map f s).sum (Multiset.map (fun x ↦ 0) ?m.25).sum

pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
ι : Type u_2
s : Multiset ι
f : ι → R
hs : ∀ x ∈ s, f x ∈ I
⊢ Type ?u.29

pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
ι : Type u_2
s : Multiset ι
f : ι → R
hs : ∀ x ∈ s, f x ∈ I
⊢ Multiset ?m.22

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
ι : Type u_2
s : Multiset ι
f : ι → R
hs : ∀ x ∈ s, f x ∈ I
⊢ I.ringCon (Multiset.map f s).sum (Multiset.map (fun x ↦ 0) ?m.25).sum

R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
ι : Type u_2
s : Multiset ι
f : ι → R
hs : ∀ x ∈ s, f x ∈ I
⊢ Type ?u.29

R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
ι : Type u_2
s : Multiset ι
f : ι → R
hs : ∀ x ∈ s, f x ∈ I
⊢ Multiset ?m.22
Module: Mathlib.RingTheory.TwoSidedIdeal.BigOperators

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
ι : Type u_2
s : Finset ι
f : ι → R
hs : ∀ x ∈ s, f x ∈ I
⊢ I.ringCon (s.sum f) (∑ _x ∈ ?m.23, 0)

pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
ι : Type u_2
s : Finset ι
f : ι → R
hs : ∀ x ∈ s, f x ∈ I
⊢ Type ?u.28

pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
ι : Type u_2
s : Finset ι
f : ι → R
hs : ∀ x ∈ s, f x ∈ I
⊢ Finset ?m.21

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
ι : Type u_2
s : Finset ι
f : ι → R
hs : ∀ x ∈ s, f x ∈ I
⊢ I.ringCon (s.sum f) (∑ _x ∈ ?m.23, 0)

R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
ι : Type u_2
s : Finset ι
f : ι → R
hs : ∀ x ∈ s, f x ∈ I
⊢ Type ?u.28

R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
ι : Type u_2
s : Finset ι
f : ι → R
hs : ∀ x ∈ s, f x ∈ I
⊢ Finset ?m.21
Module: Mathlib.RingTheory.TwoSidedIdeal.BigOperators

Goal state before:
pp: case mk
R : Type u_1
inst✝ : CommRing R
I : TwoSidedIdeal R
ι : Type u_2
s : Multiset ι
f : ι → R
a✝ : List ι
hs : ∃ x ∈ Quot.mk (⇑(List.isSetoid ι)) a✝, f x ∈ I
⊢ (Multiset.map f (Quot.mk (⇑(List.isSetoid ι)) a✝)).prod ∈ I

Tactic:
simpa using listProd_mem (hl := hs)

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

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
H : ∀ (x : S), ∃ n > 0, x ^ n ∈ f.range
hker : RingHom.ker f ≤ nilradical R
q q' : PrimeSpectrum S
hqq' : comap f q = comap f q'
x : S
n : ℕ
hn : n > 0
y : R
hy : f y = x ^ n
⊢ f y ∈ q.asIdeal ↔ f y ∈ q'.asIdeal

Tactic:
]

Goal state after:
R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
H : ∀ (x : S), ∃ n > 0, x ^ n ∈ f.range
hker : RingHom.ker f ≤ nilradical R
q q' : PrimeSpectrum S
hqq' : comap f q = comap f q'
x : S
n : ℕ
hn : n > 0
y : R
hy : f y = x ^ n
⊢ f y ∈ q.asIdeal ↔ f y ∈ q'.asIdeal
Module: Mathlib.RingTheory.Spectrum.Prime.Homeomorph

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
H : ∀ (x : S), ∃ n > 0, x ^ n ∈ f.range
hker : RingHom.ker f ≤ nilradical R
q q' : PrimeSpectrum S
hqq' : ∀ (x : R), x ∈ (comap f q).asIdeal ↔ x ∈ (comap f q').asIdeal
x : S
n : ℕ
hn : n > 0
y : R
hy : f y = x ^ n
⊢ f y ∈ q.asIdeal ↔ f y ∈ q'.asIdeal

Tactic:
]

Goal state after:
R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
H : ∀ (x : S), ∃ n > 0, x ^ n ∈ f.range
hker : RingHom.ker f ≤ nilradical R
q q' : PrimeSpectrum S
hqq' : ∀ (x : R), x ∈ (comap f q).asIdeal ↔ x ∈ (comap f q').asIdeal
x : S
n : ℕ
hn : n > 0
y : R
hy : f y = x ^ n
⊢ f y ∈ q.asIdeal ↔ f y ∈ q'.asIdeal
Module: Mathlib.RingTheory.Spectrum.Prime.Homeomorph

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
H : ∀ (x : S), ∃ n > 0, x ^ n ∈ f.range
hker : RingHom.ker f ≤ nilradical R
h1 : Function.Injective (comap f)
hint : f.kerLift.IsIntegral
hbij : Function.Bijective (comap f)
⊢ ∀ s ∈ Set.range fun r ↦ ↑(basicOpen r), IsOpen (comap f '' s)

Tactic:
]

Goal state after:
R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
H : ∀ (x : S), ∃ n > 0, x ^ n ∈ f.range
hker : RingHom.ker f ≤ nilradical R
h1 : Function.Injective (comap f)
hint : f.kerLift.IsIntegral
hbij : Function.Bijective (comap f)
⊢ ∀ s ∈ Set.range fun r ↦ ↑(basicOpen r), IsOpen (comap f '' s)
Module: Mathlib.RingTheory.Spectrum.Prime.Homeomorph

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
H : ∀ (x : S), ∃ n > 0, x ^ n ∈ f.range
hker : RingHom.ker f ≤ nilradical R
h1 : Function.Injective (comap f)
hint : f.kerLift.IsIntegral
hbij : Function.Bijective (comap f)
s : S
n : ℕ
hn : n > 0
r : R
hr : f r = s ^ n
⊢ ↑(basicOpen (f r)) = comap f ⁻¹' ↑(basicOpen r)

Tactic:
]

Goal state after:
R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
H : ∀ (x : S), ∃ n > 0, x ^ n ∈ f.range
hker : RingHom.ker f ≤ nilradical R
h1 : Function.Injective (comap f)
hint : f.kerLift.IsIntegral
hbij : Function.Bijective (comap f)
s : S
n : ℕ
hn : n > 0
r : R
hr : f r = s ^ n
⊢ ↑(basicOpen (f r)) = comap f ⁻¹' ↑(basicOpen r)