mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
r : S
⊢ absNorm (span {r}) = (LinearMap.det ((Algebra.lmul ℤ S) r)).natAbs

Tactic:
]

Goal state after:
S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
r : S
⊢ absNorm (span {r}) = (LinearMap.det ((Algebra.lmul ℤ S) r)).natAbs
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: case neg
S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
r : S
hr : ¬r = 0
b : Basis (Free.ChooseBasisIndex ℤ S) ℤ S := Free.chooseBasis ℤ S
⊢ (LinearMap.det
        (↑ℤ (Submodule.subtype (span {r})) ∘ₗ
          (↑(b.equiv (basisSpanSingleton b hr) (Equiv.refl (Free.ChooseBasisIndex ℤ S)))).toIntLinearMap)).natAbs =
    (LinearMap.det ((Algebra.lmul ℤ S) r)).natAbs

Tactic:
]

Goal state after:
case neg
S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
r : S
hr : ¬r = 0
b : Basis (Free.ChooseBasisIndex ℤ S) ℤ S := Free.chooseBasis ℤ S
⊢ (LinearMap.det
        (↑ℤ (Submodule.subtype (span {r})) ∘ₗ
          (↑(b.equiv (basisSpanSingleton b hr) (Equiv.refl (Free.ChooseBasisIndex ℤ S)))).toIntLinearMap)).natAbs =
    (LinearMap.det ((Algebra.lmul ℤ S) r)).natAbs
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
I : Ideal S
x : S
h : x ∈ I
⊢ absNorm I ∣ absNorm (span {x})

Tactic:
]

Goal state after:
S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
I : Ideal S
x : S
h : x ∈ I
⊢ absNorm I ∣ absNorm (span {x})
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
r : S
s : Set S
⊢ ((Algebra.norm ℤ) r).natAbs ∣ ((Algebra.norm ℤ) r).natAbs

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: case mp
S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
I : Ideal S
hI : absNorm I = 0
⊢ I ≤ ⊥

Tactic:
]

Goal state after:
case mp
S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
I : Ideal S
hI : absNorm I = 0
⊢ I ≤ ⊥
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: case mp
S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
I : Ideal S
hI : absNorm I = 0
x : S
hx : x ∈ I
⊢ absNorm I ∣ absNorm (span {x})

Tactic:
]

Goal state after:
case mp
S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
I : Ideal S
hI : absNorm I = 0
x : S
hx : x ∈ I
⊢ absNorm I ∣ absNorm (span {x})
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: case mp
S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
I : Ideal S
hI : absNorm I = 0
x : S
hx : x ∈ I
⊢ x ∈ I

Tactic:
]

Goal state after:
case mp
S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
I : Ideal S
hI : absNorm I = 0
x : S
hx : x ∈ I
⊢ x ∈ I
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
I : Ideal S
⊢ absNorm I ≠ 0 ↔ absNorm I ≠ 0

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
I : Ideal S
hI : I ≠ ⊥
⊢ ¬I = ⊥

Tactic:
]

Goal state after:
S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
I : Ideal S
hI : I ≠ ⊥
⊢ ¬I = ⊥
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: case intro
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDedekindDomain S
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
P : Ideal S
inst✝ : P.IsMaximal
this✝² : IsAddTorsionFree S
this✝¹ : CharZero S
this✝ : Finite (S ⧸ P)
val✝ : Fintype (S ⧸ P)
this : Field (S ⧸ P) := Quotient.field P
p : ℕ
hpR : CharP (S ⧸ P) p
n : ℕ+
hp : Nat.Prime p
e : Fintype.card (S ⧸ P) = p ^ ↑n
hP : absNorm P = p ^ ↑n
⊢ ↑(absNorm P) ∈ P

Tactic:
]

Goal state after:
case intro
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDedekindDomain S
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
P : Ideal S
inst✝ : P.IsMaximal
this✝² : IsAddTorsionFree S
this✝¹ : CharZero S
this✝ : Finite (S ⧸ P)
val✝ : Fintype (S ⧸ P)
this : Field (S ⧸ P) := Quotient.field P
p : ℕ
hpR : CharP (S ⧸ P) p
n : ℕ+
hp : Nat.Prime p
e : Fintype.card (S ⧸ P) = p ^ ↑n
hP : absNorm P = p ^ ↑n
⊢ ↑(absNorm P) ∈ P
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDedekindDomain S
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
P : Ideal S
inst✝ : P.IsMaximal
⊢ ∃ p n, 0 < n ∧ ↑p ∈ P ∧ Nat.Prime p ∧ absNorm P = p ^ n

Tactic:
have : IsAddTorsionFree S := .of_isTorsionFree ℤ _
  have := CharZero.of_isAddTorsionFree S S
  have : Finite (S ⧸ P) := Submodule.finiteQuotientOfFreeOfRankEq (P.restrictScalars ℤ)
    (Ideal.finrank_eq_finrank (Module.Free.chooseBasis _ _) _
      (Ideal.IsMaximal.ne_bot_of_isIntegral_int P))
  cases nonempty_fintype (S ⧸ P)
  let := Ideal.Quotient.field P
  obtain ⟨p, hpR⟩ := CharP.exists (S ⧸ P)
  obtain ⟨n, hp, e⟩ := FiniteField.card (S ⧸ P) p
  have hP : P.absNorm = p ^ (n : ℕ) := (Nat.card_eq_fintype_card.trans e:)
  refine ⟨p, n, n.2, ?_, hp, hP⟩
  rw [← Ideal.IsPrime.pow_mem_iff_mem (I := P) inferInstance _ n.pos, ← Nat.cast_pow, ← hP]
  exact P.absNorm_mem

Goal state after:
Module: Mathlib.RingTheory.Localization.InvSubmonoid

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
m : ↥M
x✝ : S
⊢ m • x✝ = ↑m • x✝

Tactic:
]

Goal state after:
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
m : ↥M
x✝ : S
⊢ m • x✝ = ↑m • x✝
Module: Mathlib.GroupTheory.Submonoid.Inverses

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
S : Submonoid M
x y : M
z : ↥S
h₁ : y * ↑z = 1
h₂ : x * y = 1
⊢ ↑z = ↑z

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Submonoid.Inverses

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
⊢ S.leftInv.leftInv = S

Tactic:
refine le_antisymm S.leftInv_leftInv_le ?_

Goal state after:
M : Type u_1
inst✝ : Monoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
⊢ S ≤ S.leftInv.leftInv
Module: Mathlib.GroupTheory.Submonoid.Inverses

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : M
hx : x ∈ S
⊢ x = ↑(IsUnit.unit ⋯)

Tactic:
]

Goal state after:
M : Type u_1
inst✝ : Monoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : M
hx : x ∈ S
⊢ x = ↑(IsUnit.unit ⋯)
Module: Mathlib.GroupTheory.Submonoid.Inverses

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : M
hx : x ∈ S
this : x = ↑(IsUnit.unit ⋯)⁻¹⁻¹
⊢ ↑(IsUnit.unit ⋯)⁻¹⁻¹ ∈ S.leftInv.leftInv

Tactic:
]

Goal state after:
M : Type u_1
inst✝ : Monoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : M
hx : x ∈ S
this : x = ↑(IsUnit.unit ⋯)⁻¹⁻¹
⊢ ↑(IsUnit.unit ⋯)⁻¹⁻¹ ∈ S.leftInv.leftInv
Module: Mathlib.GroupTheory.Submonoid.Inverses

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x : ↥S.leftInv
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Submonoid.Inverses

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
a : ↥S.leftInv
b : M
⊢ ↑a * b = 1 ↔ ↑a * b = 1

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Localization.InvSubmonoid

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
z : S
r : R
m : ↥M
e : z * (algebraMap R S) ↑(r, m).2 = (algebraMap R S) r
⊢ z = z * ((algebraMap R S) ↑(r, m).2 * ↑((toInvSubmonoid M S) m))

Tactic:
]

Goal state after:
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
z : S
r : R
m : ↥M
e : z * (algebraMap R S) ↑(r, m).2 = (algebraMap R S) r
⊢ z = z * ((algebraMap R S) ↑(r, m).2 * ↑((toInvSubmonoid M S) m))
Module: Mathlib.GroupTheory.Submonoid.Inverses

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x y : ↥S.leftInv
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Localization.InvSubmonoid

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : ↥M
⊢ ↑((toInvSubmonoid M S) x) * (algebraMap R S) ↑x = mk' S 1 x * (algebraMap R S) ↑x

Tactic:
]

Goal state after:
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : ↥M
⊢ ↑((toInvSubmonoid M S) x) * (algebraMap R S) ↑x = mk' S 1 x * (algebraMap R S) ↑x
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: case h₃.inl
S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
p : ℤ
hp : Prime p
this✝¹ : IsAddTorsionFree S
this✝ : CharZero S
hpMax : (span {p}).IsMaximal
I P : Ideal S
hI' : I ≠ 0
hP : Prime P
IH : p ∣ ↑(absNorm I) → ∃ P, P.IsMaximal ∧ under ℤ P = span {p} ∧ P ∣ I
this : P.IsMaximal
q n : ℕ
hI : ∃ i ≤ n, Associated p (↑q ^ i)
hn : 0 < n
hqP : ↑q ∈ P
hq : Nat.Prime q
H : absNorm P = q ^ n
⊢ span {p} ≤ under ℤ P

Tactic:
]

Goal state after:
case h₃.inl
S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
p : ℤ
hp : Prime p
this✝¹ : IsAddTorsionFree S
this✝ : CharZero S
hpMax : (span {p}).IsMaximal
I P : Ideal S
hI' : I ≠ 0
hP : Prime P
IH : p ∣ ↑(absNorm I) → ∃ P, P.IsMaximal ∧ under ℤ P = span {p} ∧ P ∣ I
this : P.IsMaximal
q n : ℕ
hI : ∃ i ≤ n, Associated p (↑q ^ i)
hn : 0 < n
hqP : ↑q ∈ P
hq : Nat.Prime q
H : absNorm P = q ^ n
⊢ span {p} ≤ under ℤ P
Module: Mathlib.RingTheory.HopkinsLevitzki

Goal state before:
pp: R₀ : Type u_1
R : Type u_2
M✝ : Type u
inst✝¹¹ : Ring R₀
inst✝¹⁰ : Ring R
inst✝⁹ : Module R₀ R
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R₀ M✝
inst✝⁶ : Module R M✝
inst✝⁵ : IsScalarTower R₀ R M✝
inst✝⁴ : IsSemiprimaryRing R
P : (M : Type u) → [inst : AddCommGroup M] → [Module R₀ M] → [Module R M] → Prop
ss : IsSemisimpleRing (R ⧸ Ring.jacobson R)
n : ℕ
Jac : Ideal R := Ring.jacobson R
h0 :
  ∀ (M : Type u) [inst : AddCommGroup M] [inst_1 : Module R₀ M] [inst_2 : Module R M] [IsScalarTower R₀ R M]
    [IsSemisimpleModule R M], Module.IsTorsionBySet R M ↑Jac → P M
h1 :
  ∀ (M : Type u) [inst : AddCommGroup M] [inst_1 : Module R₀ M] [inst_2 : Module R M] [inst_3 : IsScalarTower R₀ R M],
    let N := Jac • ⊤;
    P ↥N → P (M ⧸ N) → P M
hn : Jac ^ n ≤ Module.annihilator R M✝
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R₀ M
inst✝¹ : Module R M
inst✝ : IsScalarTower R₀ R M
⊢ Module.IsTorsionBySet R M ↑Jac → P M

Tactic:
]

Goal state after:
R₀ : Type u_1
R : Type u_2
M✝ : Type u
inst✝¹¹ : Ring R₀
inst✝¹⁰ : Ring R
inst✝⁹ : Module R₀ R
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R₀ M✝
inst✝⁶ : Module R M✝
inst✝⁵ : IsScalarTower R₀ R M✝
inst✝⁴ : IsSemiprimaryRing R
P : (M : Type u) → [inst : AddCommGroup M] → [Module R₀ M] → [Module R M] → Prop
ss : IsSemisimpleRing (R ⧸ Ring.jacobson R)
n : ℕ
Jac : Ideal R := Ring.jacobson R
h0 :
  ∀ (M : Type u) [inst : AddCommGroup M] [inst_1 : Module R₀ M] [inst_2 : Module R M] [IsScalarTower R₀ R M]
    [IsSemisimpleModule R M], Module.IsTorsionBySet R M ↑Jac → P M
h1 :
  ∀ (M : Type u) [inst : AddCommGroup M] [inst_1 : Module R₀ M] [inst_2 : Module R M] [inst_3 : IsScalarTower R₀ R M],
    let N := Jac • ⊤;
    P ↥N → P (M ⧸ N) → P M
hn : Jac ^ n ≤ Module.annihilator R M✝
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R₀ M
inst✝¹ : Module R M
inst✝ : IsScalarTower R₀ R M
⊢ Module.IsTorsionBySet R M ↑Jac → P M
Module: Mathlib.RingTheory.Localization.InvSubmonoid

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
⊢ ⊤ ≤ Submodule.span R ↑(invSubmonoid M S)

Tactic:
]

Goal state after:
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
⊢ ⊤ ≤ Submodule.span R ↑(invSubmonoid M S)
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: case h₃.inl
S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
p : ℤ
hp✝ : Prime p
this✝¹ : IsAddTorsionFree S
this✝ : CharZero S
hpMax : (span {p}).IsMaximal
I P : Ideal S
hI' : I ≠ 0
hP : Prime P
IH : p ∣ ↑(absNorm I) → ∃ P, P.IsMaximal ∧ under ℤ P = span {p} ∧ P ∣ I
this : P.IsMaximal
q n : ℕ
hn : 0 < n
hqP : ↑q ∈ P
hq : Nat.Prime q
H : absNorm P = q ^ n
m : ℕ
hmn : m ≤ n
hp : Associated p (↑q ^ m)
⊢ p ∈ under ℤ P

Tactic:
]

Goal state after:
case h₃.inl
S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
p : ℤ
hp✝ : Prime p
this✝¹ : IsAddTorsionFree S
this✝ : CharZero S
hpMax : (span {p}).IsMaximal
I P : Ideal S
hI' : I ≠ 0
hP : Prime P
IH : p ∣ ↑(absNorm I) → ∃ P, P.IsMaximal ∧ under ℤ P = span {p} ∧ P ∣ I
this : P.IsMaximal
q n : ℕ
hn : 0 < n
hqP : ↑q ∈ P
hq : Nat.Prime q
H : absNorm P = q ^ n
m : ℕ
hmn : m ≤ n
hp : Associated p (↑q ^ m)
⊢ p ∈ under ℤ P
Module: Mathlib.GroupTheory.Submonoid.Inverses

Goal state before:
pp: M : Type u_1
inst✝ : Group M
S : Submonoid M
x : ↥S.leftInv
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Submonoid.Inverses

Goal state before:
pp: M : Type u_1
inst✝ : CommGroup M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : ↥S
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Localization.InvSubmonoid

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
inst✝ : Monoid.FG ↥M
this : (invSubmonoid M S).FG
⊢ Algebra.FiniteType R S

Tactic:
]

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
inst✝ : Monoid.FG ↥M
this : (invSubmonoid M S).FG
⊢ Algebra.FiniteType R S
Module: Mathlib.RingTheory.Localization.InvSubmonoid

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
inst✝ : Monoid.FG ↥M
s : Finset S
hs : Submonoid.closure ↑s = invSubmonoid M S
⊢ ⊤ ≤ Algebra.adjoin R ↑s

Tactic:
]

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
inst✝ : Monoid.FG ↥M
s : Finset S
hs : Submonoid.closure ↑s = invSubmonoid M S
⊢ ⊤ ≤ Algebra.adjoin R ↑s
Module: Mathlib.RingTheory.Localization.InvSubmonoid

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
inst✝ : Monoid.FG ↥M
s : Finset S
hs : Submonoid.closure ↑s = invSubmonoid M S
x : S
⊢ x ∈ ↑⊤

Tactic:
]

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
inst✝ : Monoid.FG ↥M
s : Finset S
hs : Submonoid.closure ↑s = invSubmonoid M S
x : S
⊢ x ∈ ↑⊤
Module: Mathlib.RingTheory.HopkinsLevitzki

Goal state before:
pp: case zero
R₀ : Type u_1
R : Type u_2
inst✝⁷ : Ring R₀
inst✝⁶ : Ring R
inst✝⁵ : Module R₀ R
inst✝⁴ : IsSemiprimaryRing R
P : (M : Type u) → [inst : AddCommGroup M] → [Module R₀ M] → [Module R M] → Prop
ss : IsSemisimpleRing (R ⧸ Ring.jacobson R)
Jac : Ideal R := Ring.jacobson R
h0 :
  ∀ (M : Type u) [inst : AddCommGroup M] [inst_1 : Module R₀ M] [inst_2 : Module R M] [IsScalarTower R₀ R M]
    [IsSemisimpleModule R M], Module.IsTorsionBySet R M ↑Jac → P M
h1 :
  ∀ (M : Type u) [inst : AddCommGroup M] [inst_1 : Module R₀ M] [inst_2 : Module R M] [inst_3 : IsScalarTower R₀ R M],
    let N := Jac • ⊤;
    P ↥N → P (M ⧸ N) → P M
this :
  ∀ {M : Type u} [inst : AddCommGroup M] [inst_1 : Module R₀ M] [inst_2 : Module R M] [IsScalarTower R₀ R M],
    Jac ≤ Module.annihilator R M → P M
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R₀ M
inst✝¹ : Module R M
inst✝ : IsScalarTower R₀ R M
hn : ⊤ ≤ Module.annihilator R M
⊢ P M

Tactic:
]

Goal state after:
case zero
R₀ : Type u_1
R : Type u_2
inst✝⁷ : Ring R₀
inst✝⁶ : Ring R
inst✝⁵ : Module R₀ R
inst✝⁴ : IsSemiprimaryRing R
P : (M : Type u) → [inst : AddCommGroup M] → [Module R₀ M] → [Module R M] → Prop
ss : IsSemisimpleRing (R ⧸ Ring.jacobson R)
Jac : Ideal R := Ring.jacobson R
h0 :
  ∀ (M : Type u) [inst : AddCommGroup M] [inst_1 : Module R₀ M] [inst_2 : Module R M] [IsScalarTower R₀ R M]
    [IsSemisimpleModule R M], Module.IsTorsionBySet R M ↑Jac → P M
h1 :
  ∀ (M : Type u) [inst : AddCommGroup M] [inst_1 : Module R₀ M] [inst_2 : Module R M] [inst_3 : IsScalarTower R₀ R M],
    let N := Jac • ⊤;
    P ↥N → P (M ⧸ N) → P M
this :
  ∀ {M : Type u} [inst : AddCommGroup M] [inst_1 : Module R₀ M] [inst_2 : Module R M] [IsScalarTower R₀ R M],
    Jac ≤ Module.annihilator R M → P M
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R₀ M
inst✝¹ : Module R M
inst✝ : IsScalarTower R₀ R M
hn : ⊤ ≤ Module.annihilator R M
⊢ P M
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: case inr.refine_1
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDedekindDomain S
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : CharZero S
n : ℕ
hn : n > 0
f : Ideal S → Ideal (S ⧸ span {↑n}) := fun I ↦ map (Quotient.mk (span {↑n})) I
⊢ ((Algebra.norm ℤ) ↑n).natAbs ≠ 0

Tactic:
]

Goal state after:
case inr.refine_1
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDedekindDomain S
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : CharZero S
n : ℕ
hn : n > 0
f : Ideal S → Ideal (S ⧸ span {↑n}) := fun I ↦ map (Quotient.mk (span {↑n})) I
⊢ ((Algebra.norm ℤ) ↑n).natAbs ≠ 0
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: case inr.refine_2
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDedekindDomain S
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : CharZero S
n : ℕ
hn : n > 0
f : Ideal S → Ideal (S ⧸ span {↑n}) := fun I ↦ map (Quotient.mk (span {↑n})) I
I : Ideal S
⊢ I ∈ {I | absNorm I = n} → ∀ ⦃x₂ : Ideal S⦄, x₂ ∈ {I | absNorm I = n} → f I = f x₂ → I = x₂

Tactic:
hI

Goal state after:
case inr.refine_2
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDedekindDomain S
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : CharZero S
n : ℕ
hn : n > 0
f : Ideal S → Ideal (S ⧸ span {↑n}) := fun I ↦ map (Quotient.mk (span {↑n})) I
I : Ideal S
hI : I ∈ {I | absNorm I = n}
⊢ ∀ ⦃x₂ : Ideal S⦄, x₂ ∈ {I | absNorm I = n} → f I = f x₂ → I = x₂
Module: Mathlib.RingTheory.HopkinsLevitzki

Goal state before:
pp: case succ.zero
R₀ : Type u_1
R : Type u_2
inst✝⁷ : Ring R₀
inst✝⁶ : Ring R
inst✝⁵ : Module R₀ R
inst✝⁴ : IsSemiprimaryRing R
P : (M : Type u) → [inst : AddCommGroup M] → [Module R₀ M] → [Module R M] → Prop
ss : IsSemisimpleRing (R ⧸ Ring.jacobson R)
Jac : Ideal R := Ring.jacobson R
h0 :
  ∀ (M : Type u) [inst : AddCommGroup M] [inst_1 : Module R₀ M] [inst_2 : Module R M] [IsScalarTower R₀ R M]
    [IsSemisimpleModule R M], Module.IsTorsionBySet R M ↑Jac → P M
h1 :
  ∀ (M : Type u) [inst : AddCommGroup M] [inst_1 : Module R₀ M] [inst_2 : Module R M] [inst_3 : IsScalarTower R₀ R M],
    let N := Jac • ⊤;
    P ↥N → P (M ⧸ N) → P M
this :
  ∀ {M : Type u} [inst : AddCommGroup M] [inst_1 : Module R₀ M] [inst_2 : Module R M] [IsScalarTower R₀ R M],
    Jac ≤ Module.annihilator R M → P M
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R₀ M
inst✝¹ : Module R M
inst✝ : IsScalarTower R₀ R M
ih :
  ∀ (M : Type u) [inst : AddCommGroup M] [inst_1 : Module R₀ M] [inst_2 : Module R M] [IsScalarTower R₀ R M],
    Jac ^ 0 ≤ Module.annihilator R M → P M
hn : Jac ≤ Module.annihilator R M
⊢ P M

Tactic:
]

Goal state after:
case succ.zero
R₀ : Type u_1
R : Type u_2
inst✝⁷ : Ring R₀
inst✝⁶ : Ring R
inst✝⁵ : Module R₀ R
inst✝⁴ : IsSemiprimaryRing R
P : (M : Type u) → [inst : AddCommGroup M] → [Module R₀ M] → [Module R M] → Prop
ss : IsSemisimpleRing (R ⧸ Ring.jacobson R)
Jac : Ideal R := Ring.jacobson R
h0 :
  ∀ (M : Type u) [inst : AddCommGroup M] [inst_1 : Module R₀ M] [inst_2 : Module R M] [IsScalarTower R₀ R M]
    [IsSemisimpleModule R M], Module.IsTorsionBySet R M ↑Jac → P M
h1 :
  ∀ (M : Type u) [inst : AddCommGroup M] [inst_1 : Module R₀ M] [inst_2 : Module R M] [inst_3 : IsScalarTower R₀ R M],
    let N := Jac • ⊤;
    P ↥N → P (M ⧸ N) → P M
this :
  ∀ {M : Type u} [inst : AddCommGroup M] [inst_1 : Module R₀ M] [inst_2 : Module R M] [IsScalarTower R₀ R M],
    Jac ≤ Module.annihilator R M → P M
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R₀ M
inst✝¹ : Module R M
inst✝ : IsScalarTower R₀ R M
ih :
  ∀ (M : Type u) [inst : AddCommGroup M] [inst_1 : Module R₀ M] [inst_2 : Module R M] [IsScalarTower R₀ R M],
    Jac ^ 0 ≤ Module.annihilator R M → P M
hn : Jac ≤ Module.annihilator R M
⊢ P M
Module: Mathlib.Topology.JacobsonSpace

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Function.Injective f
hf' : Continuous[inst✝¹, inst✝] f
x : X
hx : x ∈ f ⁻¹' closedPoints Y
⊢ IsClosed[inst✝¹] {x}

Tactic:
]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Function.Injective f
hf' : Continuous[inst✝¹, inst✝] f
x : X
hx : x ∈ f ⁻¹' closedPoints Y
⊢ IsClosed[inst✝¹] {x}
Module: Mathlib.Topology.JacobsonSpace

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Function.Injective f
hf' : Continuous[inst✝¹, inst✝] f
x : X
hx : x ∈ f ⁻¹' closedPoints Y
⊢ {x} = {x}

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: case inr.refine_2
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDedekindDomain S
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : CharZero S
n : ℕ
hn : n > 0
f : Ideal S → Ideal (S ⧸ span {↑n}) := fun I ↦ map (Quotient.mk (span {↑n})) I
I : Ideal S
hI : I ∈ {I | absNorm I = n}
J : Ideal S
hJ : J ∈ {I | absNorm I = n}
h : f I = f J
⊢ comap (Quotient.mk (span {↑n})) (map (Quotient.mk (span {↑n})) I) =
    comap (Quotient.mk (span {↑n})) (map (Quotient.mk (span {↑n})) J)

Tactic:
]

Goal state after:
case inr.refine_2
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDedekindDomain S
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : CharZero S
n : ℕ
hn : n > 0
f : Ideal S → Ideal (S ⧸ span {↑n}) := fun I ↦ map (Quotient.mk (span {↑n})) I
I : Ideal S
hI : I ∈ {I | absNorm I = n}
J : Ideal S
hJ : J ∈ {I | absNorm I = n}
h : f I = f J
⊢ comap (Quotient.mk (span {↑n})) (map (Quotient.mk (span {↑n})) I) =
    comap (Quotient.mk (span {↑n})) (map (Quotient.mk (span {↑n})) J)
Module: Mathlib.Topology.JacobsonSpace

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
⊢ (∀ {Z : Set X}, IsClosed[inst✝] Z → closure[inst✝] (Z ∩ closedPoints X) = Z) ↔
    ∀ (Z : Set X), Z.Nonempty → IsLocallyClosed Z → (Z ∩ closedPoints X).Nonempty

Tactic:
]

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
⊢ (∀ {Z : Set X}, IsClosed[inst✝] Z → closure[inst✝] (Z ∩ closedPoints X) = Z) ↔
    ∀ (Z : Set X), Z.Nonempty → IsLocallyClosed Z → (Z ∩ closedPoints X).Nonempty