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

Goal state before:
pp: case refine_1
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
inst✝¹ : IsScalarTower R₀ R R
inst✝ : Module.Finite R₀ (R ⧸ Ring.jacobson R)
M : Type u
x✝³ : AddCommGroup M
x✝² : Module R₀ M
x✝¹ : Module R M
x✝ : IsScalarTower R₀ R M
hs :
  IsNoetherian R ↥(Ring.jacobson R • ⊤) ∨ IsArtinian R ↥(Ring.jacobson R • ⊤) → Module.Finite R₀ ↥(Ring.jacobson R • ⊤)
hq :
  IsNoetherian R (M ⧸ Ring.jacobson R • ⊤) ∨ IsArtinian R (M ⧸ Ring.jacobson R • ⊤) →
    Module.Finite R₀ (M ⧸ Ring.jacobson R • ⊤)
h : IsNoetherian R M ∨ IsArtinian R M
N : Submodule R₀ M := Submodule.restrictScalars R₀ (Ring.jacobson R • ⊤)
a✝ : IsNoetherian R M
⊢ IsNoetherian R ↥(Ring.jacobson R • ⊤)

Tactic:
;

Goal state after:
case refine_1
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
inst✝¹ : IsScalarTower R₀ R R
inst✝ : Module.Finite R₀ (R ⧸ Ring.jacobson R)
M : Type u
x✝³ : AddCommGroup M
x✝² : Module R₀ M
x✝¹ : Module R M
x✝ : IsScalarTower R₀ R M
hs :
  IsNoetherian R ↥(Ring.jacobson R • ⊤) ∨ IsArtinian R ↥(Ring.jacobson R • ⊤) → Module.Finite R₀ ↥(Ring.jacobson R • ⊤)
hq :
  IsNoetherian R (M ⧸ Ring.jacobson R • ⊤) ∨ IsArtinian R (M ⧸ Ring.jacobson R • ⊤) →
    Module.Finite R₀ (M ⧸ Ring.jacobson R • ⊤)
h : IsNoetherian R M ∨ IsArtinian R M
N : Submodule R₀ M := Submodule.restrictScalars R₀ (Ring.jacobson R • ⊤)
a✝ : IsNoetherian R M
⊢ IsNoetherian R ↥(Ring.jacobson R • ⊤)
Module: Mathlib.RingTheory.HopkinsLevitzki

Goal state before:
pp: case refine_2
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
inst✝¹ : IsScalarTower R₀ R R
inst✝ : Module.Finite R₀ (R ⧸ Ring.jacobson R)
M : Type u
x✝³ : AddCommGroup M
x✝² : Module R₀ M
x✝¹ : Module R M
x✝ : IsScalarTower R₀ R M
hs :
  IsNoetherian R ↥(Ring.jacobson R • ⊤) ∨ IsArtinian R ↥(Ring.jacobson R • ⊤) → Module.Finite R₀ ↥(Ring.jacobson R • ⊤)
hq :
  IsNoetherian R (M ⧸ Ring.jacobson R • ⊤) ∨ IsArtinian R (M ⧸ Ring.jacobson R • ⊤) →
    Module.Finite R₀ (M ⧸ Ring.jacobson R • ⊤)
h : IsNoetherian R M ∨ IsArtinian R M
N : Submodule R₀ M := Submodule.restrictScalars R₀ (Ring.jacobson R • ⊤)
a✝ : IsArtinian R M
⊢ IsArtinian R ↥(Ring.jacobson R • ⊤)

Tactic:
;

Goal state after:
case refine_2
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
inst✝¹ : IsScalarTower R₀ R R
inst✝ : Module.Finite R₀ (R ⧸ Ring.jacobson R)
M : Type u
x✝³ : AddCommGroup M
x✝² : Module R₀ M
x✝¹ : Module R M
x✝ : IsScalarTower R₀ R M
hs :
  IsNoetherian R ↥(Ring.jacobson R • ⊤) ∨ IsArtinian R ↥(Ring.jacobson R • ⊤) → Module.Finite R₀ ↥(Ring.jacobson R • ⊤)
hq :
  IsNoetherian R (M ⧸ Ring.jacobson R • ⊤) ∨ IsArtinian R (M ⧸ Ring.jacobson R • ⊤) →
    Module.Finite R₀ (M ⧸ Ring.jacobson R • ⊤)
h : IsNoetherian R M ∨ IsArtinian R M
N : Submodule R₀ M := Submodule.restrictScalars R₀ (Ring.jacobson R • ⊤)
a✝ : IsArtinian R M
⊢ IsArtinian R ↥(Ring.jacobson R • ⊤)
Module: Mathlib.RingTheory.HopkinsLevitzki

Goal state before:
pp: case refine_1
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
inst✝¹ : IsScalarTower R₀ R R
inst✝ : Module.Finite R₀ (R ⧸ Ring.jacobson R)
M : Type u
x✝³ : AddCommGroup M
x✝² : Module R₀ M
x✝¹ : Module R M
x✝ : IsScalarTower R₀ R M
hs :
  IsNoetherian R ↥(Ring.jacobson R • ⊤) ∨ IsArtinian R ↥(Ring.jacobson R • ⊤) → Module.Finite R₀ ↥(Ring.jacobson R • ⊤)
hq :
  IsNoetherian R (M ⧸ Ring.jacobson R • ⊤) ∨ IsArtinian R (M ⧸ Ring.jacobson R • ⊤) →
    Module.Finite R₀ (M ⧸ Ring.jacobson R • ⊤)
h : IsNoetherian R M ∨ IsArtinian R M
N : Submodule R₀ M := Submodule.restrictScalars R₀ (Ring.jacobson R • ⊤)
this : Module.Finite R₀ ↥N
a✝ : IsNoetherian R M
⊢ IsNoetherian R (M ⧸ Ring.jacobson R • ⊤)

Tactic:
;

Goal state after:
case refine_1
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
inst✝¹ : IsScalarTower R₀ R R
inst✝ : Module.Finite R₀ (R ⧸ Ring.jacobson R)
M : Type u
x✝³ : AddCommGroup M
x✝² : Module R₀ M
x✝¹ : Module R M
x✝ : IsScalarTower R₀ R M
hs :
  IsNoetherian R ↥(Ring.jacobson R • ⊤) ∨ IsArtinian R ↥(Ring.jacobson R • ⊤) → Module.Finite R₀ ↥(Ring.jacobson R • ⊤)
hq :
  IsNoetherian R (M ⧸ Ring.jacobson R • ⊤) ∨ IsArtinian R (M ⧸ Ring.jacobson R • ⊤) →
    Module.Finite R₀ (M ⧸ Ring.jacobson R • ⊤)
h : IsNoetherian R M ∨ IsArtinian R M
N : Submodule R₀ M := Submodule.restrictScalars R₀ (Ring.jacobson R • ⊤)
this : Module.Finite R₀ ↥N
a✝ : IsNoetherian R M
⊢ IsNoetherian R (M ⧸ Ring.jacobson R • ⊤)
Module: Mathlib.Topology.JacobsonSpace

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
ι : Type u_1
U : ι → Opens X
hU : IsOpenCover U
H : ∀ (i : ι), JacobsonSpace ↥(U i)
Z : Set X
hZ' : IsLocallyClosed Z
i : ι
x : X
hx : x ∈ Z
hx' : x ∈ ↑(U i)
y : ↥(U i)
hy : y ∈ Subtype.val ⁻¹' Z
hy' : y ∈ closedPoints ↥(U i)
j : ι
h : ↑y ∈ U j
x✝ : ↥(U j)
⊢ x✝ ∈ Subtype.val ⁻¹' {↑y} ↔ x✝ ∈ {⟨↑y, h⟩}

Tactic:
;

Goal state after:
X : Type u_2
inst✝ : TopologicalSpace X
ι : Type u_1
U : ι → Opens X
hU : IsOpenCover U
H : ∀ (i : ι), JacobsonSpace ↥(U i)
Z : Set X
hZ' : IsLocallyClosed Z
i : ι
x : X
hx : x ∈ Z
hx' : x ∈ ↑(U i)
y : ↥(U i)
hy : y ∈ Subtype.val ⁻¹' Z
hy' : y ∈ closedPoints ↥(U i)
j : ι
h : ↑y ∈ U j
x✝ : ↥(U j)
⊢ x✝ ∈ Subtype.val ⁻¹' {↑y} ↔ x✝ ∈ {⟨↑y, h⟩}
Module: Mathlib.RingTheory.HopkinsLevitzki

Goal state before:
pp: case refine_2
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
inst✝¹ : IsScalarTower R₀ R R
inst✝ : Module.Finite R₀ (R ⧸ Ring.jacobson R)
M : Type u
x✝³ : AddCommGroup M
x✝² : Module R₀ M
x✝¹ : Module R M
x✝ : IsScalarTower R₀ R M
hs :
  IsNoetherian R ↥(Ring.jacobson R • ⊤) ∨ IsArtinian R ↥(Ring.jacobson R • ⊤) → Module.Finite R₀ ↥(Ring.jacobson R • ⊤)
hq :
  IsNoetherian R (M ⧸ Ring.jacobson R • ⊤) ∨ IsArtinian R (M ⧸ Ring.jacobson R • ⊤) →
    Module.Finite R₀ (M ⧸ Ring.jacobson R • ⊤)
h : IsNoetherian R M ∨ IsArtinian R M
N : Submodule R₀ M := Submodule.restrictScalars R₀ (Ring.jacobson R • ⊤)
this : Module.Finite R₀ ↥N
a✝ : IsArtinian R M
⊢ IsArtinian R (M ⧸ Ring.jacobson R • ⊤)

Tactic:
;

Goal state after:
case refine_2
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
inst✝¹ : IsScalarTower R₀ R R
inst✝ : Module.Finite R₀ (R ⧸ Ring.jacobson R)
M : Type u
x✝³ : AddCommGroup M
x✝² : Module R₀ M
x✝¹ : Module R M
x✝ : IsScalarTower R₀ R M
hs :
  IsNoetherian R ↥(Ring.jacobson R • ⊤) ∨ IsArtinian R ↥(Ring.jacobson R • ⊤) → Module.Finite R₀ ↥(Ring.jacobson R • ⊤)
hq :
  IsNoetherian R (M ⧸ Ring.jacobson R • ⊤) ∨ IsArtinian R (M ⧸ Ring.jacobson R • ⊤) →
    Module.Finite R₀ (M ⧸ Ring.jacobson R • ⊤)
h : IsNoetherian R M ∨ IsArtinian R M
N : Submodule R₀ M := Submodule.restrictScalars R₀ (Ring.jacobson R • ⊤)
this : Module.Finite R₀ ↥N
a✝ : IsArtinian R M
⊢ IsArtinian R (M ⧸ Ring.jacobson R • ⊤)
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
inst✝ : JacobsonSpace X
S : Set X
hS : IsLocallyClosed S
hf₁ : Continuous[inst✝², inst✝¹] f
hf₂ : IsClosedMap f
hfS : (f '' S).Finite
hS'' : S.Nonempty
hS' : IsIrreducible S
H₁ : IsIrreducible (S ∩ closedPoints X)
x : X
hx : x ∈ S ∩ closedPoints X
⊢ f x ∈ closedPoints Y

Tactic:
;

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : JacobsonSpace X
S : Set X
hS : IsLocallyClosed S
hf₁ : Continuous[inst✝², inst✝¹] f
hf₂ : IsClosedMap f
hfS : (f '' S).Finite
hS'' : S.Nonempty
hS' : IsIrreducible S
H₁ : IsIrreducible (S ∩ closedPoints X)
x : X
hx : x ∈ S ∩ closedPoints X
⊢ f x ∈ closedPoints Y
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
n : ℕ
inst✝ : CharZero S
this✝ : Finite { I // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n }
this : Finite { I // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n }
e : { I // absNorm I ≤ n } ≃ { I // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n } ⊕ { I // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n } :=
  (Equiv.subtypeEquivRight ⋯).trans
    (subtypeOrEquiv (fun I ↦ I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n) (fun I ↦ I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n) ⋯)
I : Ideal S
h : absNorm I = 0
⊢ 0 ≤ n

Tactic:
;

Goal state after:
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDedekindDomain S
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
n : ℕ
inst✝ : CharZero S
this✝ : Finite { I // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n }
this : Finite { I // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n }
e : { I // absNorm I ≤ n } ≃ { I // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n } ⊕ { I // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n } :=
  (Equiv.subtypeEquivRight ⋯).trans
    (subtypeOrEquiv (fun I ↦ I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n) (fun I ↦ I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n) ⋯)
I : Ideal S
h : absNorm I = 0
⊢ 0 ≤ n
Module: Mathlib.Topology.JacobsonSpace

Goal state before:
pp: case inr
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : JacobsonSpace X
S : Set X
hS : IsLocallyClosed S
hf₁ : Continuous[inst✝², inst✝¹] f
hf₂ : IsClosedMap f
hfS : (f '' S).Finite
hS'' : S.Nonempty
hS' : IsIrreducible S
H₁ : IsIrreducible (S ∩ closedPoints X)
H₂ : f '' (S ∩ closedPoints X) ⊆ closedPoints Y
H₃ : (f '' (S ∩ closedPoints X)).Subsingleton
x : Y
hx : x ∈ f '' (S ∩ closedPoints X)
⊢ IsClosed[inst✝¹] {x}

Tactic:
;

Goal state after:
case inr
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : JacobsonSpace X
S : Set X
hS : IsLocallyClosed S
hf₁ : Continuous[inst✝², inst✝¹] f
hf₂ : IsClosedMap f
hfS : (f '' S).Finite
hS'' : S.Nonempty
hS' : IsIrreducible S
H₁ : IsIrreducible (S ∩ closedPoints X)
H₂ : f '' (S ∩ closedPoints X) ⊆ closedPoints Y
H₃ : (f '' (S ∩ closedPoints X)).Subsingleton
x : Y
hx : x ∈ f '' (S ∩ closedPoints X)
⊢ IsClosed[inst✝¹] {x}
Module: Mathlib.RingTheory.LocalRing.Length

Goal state before:
pp: case pos.zero
A : Type u_1
B : Type u_2
M : Type u_3
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : IsLocalRing A
inst✝⁶ : IsLocalRing B
inst✝⁵ : Algebra A B
inst✝⁴ : IsLocalHom (algebraMap A B)
inst✝³ : AddCommGroup M
inst✝² : Module A M
inst✝¹ : Module B M
inst✝ : IsScalarTower A B M
h : IsFiniteLength B M
s : CompositionSeries (Submodule B M)
hs_bot : RelSeries.head s = ⊥
hs_top : RelSeries.last s = ⊤
⊢ length A ↥⊥ = ↑↑0 * length (ResidueField A) (ResidueField B)

Tactic:
;

Goal state after:
case pos.zero
A : Type u_1
B : Type u_2
M : Type u_3
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : IsLocalRing A
inst✝⁶ : IsLocalRing B
inst✝⁵ : Algebra A B
inst✝⁴ : IsLocalHom (algebraMap A B)
inst✝³ : AddCommGroup M
inst✝² : Module A M
inst✝¹ : Module B M
inst✝ : IsScalarTower A B M
h : IsFiniteLength B M
s : CompositionSeries (Submodule B M)
hs_bot : RelSeries.head s = ⊥
hs_top : RelSeries.last s = ⊤
⊢ length A ↥⊥ = ↑↑0 * length (ResidueField A) (ResidueField B)
Module: Mathlib.RingTheory.RamificationInertia.Inertia

Goal state before:
pp: case pos
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
q : Ideal S
G : Type u_4
inst✝² : Group G
inst✝¹ : MulSemiringAction G S
inst✝ : SMulCommClass G R S
g : G
hq : q.IsPrime
⊢ (g • q).inertiaDeg R = q.inertiaDeg R

pp: case neg
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
q : Ideal S
G : Type u_4
inst✝² : Group G
inst✝¹ : MulSemiringAction G S
inst✝ : SMulCommClass G R S
g : G
hq : ¬q.IsPrime
⊢ (g • q).inertiaDeg R = q.inertiaDeg R

Tactic:
;

Goal state after:
case pos
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
q : Ideal S
G : Type u_4
inst✝² : Group G
inst✝¹ : MulSemiringAction G S
inst✝ : SMulCommClass G R S
g : G
hq : q.IsPrime
⊢ (g • q).inertiaDeg R = q.inertiaDeg R

case neg
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
q : Ideal S
G : Type u_4
inst✝² : Group G
inst✝¹ : MulSemiringAction G S
inst✝ : SMulCommClass G R S
g : G
hq : ¬q.IsPrime
⊢ (g • q).inertiaDeg R = q.inertiaDeg R
Module: Mathlib.NumberTheory.RamificationInertia.Ramification

Goal state before:
pp: R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : Ideal R
P : Ideal S
h : ∀ (n : ℕ), ∃ k, map f p ≤ P ^ k ∧ n < k
⊢ ∀ (n : ℕ), ∃ a ∈ {n | map f p ≤ P ^ n}, n < a

Tactic:
;

Goal state after:
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : Ideal R
P : Ideal S
h : ∀ (n : ℕ), ∃ k, map f p ≤ P ^ k ∧ n < k
⊢ ∀ (n : ℕ), ∃ a ∈ {n | map f p ≤ P ^ n}, n < a
Module: Mathlib.NumberTheory.RamificationInertia.Ramification

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal R
S₁ : Type u_1
inst✝¹ : CommRing S₁
inst✝ : Algebra R S₁
e : S ≃ₐ[R] S₁
P : Ideal S₁
n : ℕ
⊢ p ≤ comap ((↑e.toRingEquiv.symm.symm).comp f) (P ^ n) ↔ p ≤ comap (algebraMap R S₁) (P ^ n)

Tactic:
RingEquiv.symm_symm,

Goal state after:
R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal R
S₁ : Type u_1
inst✝¹ : CommRing S₁
inst✝ : Algebra R S₁
e : S ≃ₐ[R] S₁
P : Ideal S₁
n : ℕ
⊢ p ≤ comap ((↑e.toRingEquiv).comp f) (P ^ n) ↔ p ≤ comap (algebraMap R S₁) (P ^ n)
Module: Mathlib.NumberTheory.RamificationInertia.Ramification

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal R
S₁ : Type u_1
inst✝¹ : CommRing S₁
inst✝ : Algebra R S₁
e : S ≃ₐ[R] S₁
P : Ideal S₁
n : ℕ
⊢ p ≤ comap ((↑e).comp f) (P ^ n) ↔ p ≤ comap (algebraMap R S₁) (P ^ n)

Tactic:
← e.toAlgHom_toRingHom,

Goal state after:
R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal R
S₁ : Type u_1
inst✝¹ : CommRing S₁
inst✝ : Algebra R S₁
e : S ≃ₐ[R] S₁
P : Ideal S₁
n : ℕ
⊢ p ≤ comap ((↑↑e).comp f) (P ^ n) ↔ p ≤ comap (algebraMap R S₁) (P ^ n)
Module: Mathlib.RingTheory.LocalRing.Length

Goal state before:
pp: case pos.zero
A : Type u_1
B : Type u_2
M : Type u_3
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : IsLocalRing A
inst✝⁵ : IsLocalRing B
inst✝⁴ : Algebra A B
inst✝³ : IsLocalHom (algebraMap A B)
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Flat A B
h : IsFiniteLength A M
s : CompositionSeries (Submodule A M)
hs_bot : RelSeries.head s = ⊥
hs_top : RelSeries.last s = ⊤
⊢ length B ↥⊥ = ↑↑0 * length B (B ⧸ Ideal.map (algebraMap A B) (maximalIdeal A))

Tactic:
;

Goal state after:
case pos.zero
A : Type u_1
B : Type u_2
M : Type u_3
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : IsLocalRing A
inst✝⁵ : IsLocalRing B
inst✝⁴ : Algebra A B
inst✝³ : IsLocalHom (algebraMap A B)
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Flat A B
h : IsFiniteLength A M
s : CompositionSeries (Submodule A M)
hs_bot : RelSeries.head s = ⊥
hs_top : RelSeries.last s = ⊤
⊢ length B ↥⊥ = ↑↑0 * length B (B ⧸ Ideal.map (algebraMap A B) (maximalIdeal A))
Module: Mathlib.RingTheory.Ideal.IdempotentFG

Goal state before:
pp: case mpr
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I.FG
⊢ (∃ e, IsIdempotentElem e ∧ I = R ∙ e) → IsIdempotentElem I

Tactic:
rintro ⟨e, he, rfl⟩

Goal state after:
case mpr
R : Type u_1
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
h : FG (R ∙ e)
⊢ IsIdempotentElem (R ∙ e)
Module: Mathlib.RingTheory.LocalRing.ResidueField.Instances

Goal state before:
pp: R✝ : Type u_1
A : Type u_2
B : Type u_3
inst✝¹² : CommRing R✝
inst✝¹¹ : CommRing A
inst✝¹⁰ : CommRing B
inst✝⁹ : Algebra R✝ A
inst✝⁸ : Algebra A B
inst✝⁷ : Algebra R✝ B
inst✝⁶ : IsScalarTower R✝ A B
p : Ideal A
q : Ideal B
inst✝⁵ : q.LiesOver p
R : Type u_4
k : Type u_5
inst✝⁴ : CommRing R
inst✝³ : IsLocalRing R
inst✝² : Field k
inst✝¹ : Algebra R k
inst✝ : Module.Finite R k
x✝ : R
⊢ (((algebraMap (ResidueField R) k).comp ↑(Ideal.quotEquivOfEq ⋯)).comp
        (Ideal.Quotient.mk (Ideal.comap (algebraMap R k) ⊥)))
      x✝ =
    (((↑(RingEquiv.quotientBot k)).comp (algebraMap (R ⧸ Ideal.comap (algebraMap R k) ⊥) (k ⧸ ⊥))).comp
        (Ideal.Quotient.mk (Ideal.comap (algebraMap R k) ⊥)))
      x✝

Tactic:
;

Goal state after:
R✝ : Type u_1
A : Type u_2
B : Type u_3
inst✝¹² : CommRing R✝
inst✝¹¹ : CommRing A
inst✝¹⁰ : CommRing B
inst✝⁹ : Algebra R✝ A
inst✝⁸ : Algebra A B
inst✝⁷ : Algebra R✝ B
inst✝⁶ : IsScalarTower R✝ A B
p : Ideal A
q : Ideal B
inst✝⁵ : q.LiesOver p
R : Type u_4
k : Type u_5
inst✝⁴ : CommRing R
inst✝³ : IsLocalRing R
inst✝² : Field k
inst✝¹ : Algebra R k
inst✝ : Module.Finite R k
x✝ : R
⊢ (((algebraMap (ResidueField R) k).comp ↑(Ideal.quotEquivOfEq ⋯)).comp
        (Ideal.Quotient.mk (Ideal.comap (algebraMap R k) ⊥)))
      x✝ =
    (((↑(RingEquiv.quotientBot k)).comp (algebraMap (R ⧸ Ideal.comap (algebraMap R k) ⊥) (k ⧸ ⊥))).comp
        (Ideal.Quotient.mk (Ideal.comap (algebraMap R k) ⊥)))
      x✝
Module: Mathlib.NumberTheory.RamificationInertia.Ramification

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
p : Ideal R
P : Ideal S
inst✝ : IsDedekindDomain S
hp : map f p ≠ ⊥
hP : P.IsPrime
⊢ p.ramificationIdx' P = multiplicity P (map f p)

Tactic:
by_cases hP₂ : P = ⊥

Goal state after:
case pos
R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
p : Ideal R
P : Ideal S
inst✝ : IsDedekindDomain S
hp : map f p ≠ ⊥
hP : P.IsPrime
hP₂ : P = ⊥
⊢ p.ramificationIdx' P = multiplicity P (map f p)

case neg
R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
p : Ideal R
P : Ideal S
inst✝ : IsDedekindDomain S
hp : map f p ≠ ⊥
hP : P.IsPrime
hP₂ : ¬P = ⊥
⊢ p.ramificationIdx' P = multiplicity P (map f p)
Module: Mathlib.NumberTheory.RamificationInertia.Ramification

Goal state before:
pp: case neg
R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
p : Ideal R
P : Ideal S
inst✝ : IsDedekindDomain S
hp : map f p ≠ ⊥
hP : P.IsPrime
hP₂ : ¬P = ⊥
⊢ p.ramificationIdx' P = multiplicity P (map f p)

Tactic:
multiplicity_eq_of_emultiplicity_eq_some

Goal state after:
case neg
R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
p : Ideal R
P : Ideal S
inst✝ : IsDedekindDomain S
hp : map f p ≠ ⊥
hP : P.IsPrime
hP₂ : ¬P = ⊥
⊢ p.ramificationIdx' P = ?m.79

case neg
R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
p : Ideal R
P : Ideal S
inst✝ : IsDedekindDomain S
hp : map f p ≠ ⊥
hP : P.IsPrime
hP₂ : ¬P = ⊥
⊢ emultiplicity P (map f p) = ↑?m.79

R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
p : Ideal R
P : Ideal S
inst✝ : IsDedekindDomain S
hp : map f p ≠ ⊥
hP : P.IsPrime
hP₂ : ¬P = ⊥
⊢ ℕ
Module: Mathlib.NumberTheory.RamificationInertia.Ramification

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
p : Ideal R
P : Ideal S
inst✝ : IsDedekindDomain S
hp0 : map f p ≠ ⊥
hP : P.IsPrime
le : map f p ≤ P
hP0 : P ≠ ⊥
hPirr : Irreducible P
⊢ Multiset.count P (normalizedFactors (map f p)) ≠ 0

Tactic:
obtain ⟨P', hP', P'_eq⟩ :=
    exists_mem_normalizedFactors_of_dvd hp0 hPirr (Ideal.dvd_iff_le.mpr le)

Goal state after:
R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
p : Ideal R
P : Ideal S
inst✝ : IsDedekindDomain S
hp0 : map f p ≠ ⊥
hP : P.IsPrime
le : map f p ≤ P
hP0 : P ≠ ⊥
hPirr : Irreducible P
P' : Ideal S
hP' : P' ∈ normalizedFactors (map f p)
P'_eq : Associated P P'
⊢ Multiset.count P (normalizedFactors (map f p)) ≠ 0
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: case mp
R : Type v
inst✝⁵ : CommRing R
A : Type u
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Small.{w, u} A
a✝ : FormallyUnramified R A
B✝ : Type w
inst✝¹ : CommRing B✝
inst✝ : Algebra R B✝
I✝ : Ideal B✝
x✝ : I✝ ^ 2 = ⊥
⊢ Function.Injective (Ideal.Quotient.mkₐ R I✝).comp

Tactic:
;

Goal state after:
case mp
R : Type v
inst✝⁵ : CommRing R
A : Type u
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Small.{w, u} A
a✝ : FormallyUnramified R A
B✝ : Type w
inst✝¹ : CommRing B✝
inst✝ : Algebra R B✝
I✝ : Ideal B✝
x✝ : I✝ ^ 2 = ⊥
⊢ Function.Injective (Ideal.Quotient.mkₐ R I✝).comp
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: R : Type v
inst✝⁶ : CommRing R
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
inst✝³ : Small.{w, u} A
H :
  ∀ ⦃B : Type w⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B),
    I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp
B : Type u
inst✝² : CommRing B
inst✝¹ : Small.{w, u} B
inst✝ : Algebra R B
I : Ideal B
hI : I ^ 2 = ⊥
f g : A →ₐ[R] B
e : (Ideal.Quotient.mkₐ R I).comp f = (Ideal.Quotient.mkₐ R I).comp g
⊢ Ideal.map (Shrink.ringEquiv B).symm ⊥ = ⊥

Tactic:
;

Goal state after:
R : Type v
inst✝⁶ : CommRing R
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
inst✝³ : Small.{w, u} A
H :
  ∀ ⦃B : Type w⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B),
    I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp
B : Type u
inst✝² : CommRing B
inst✝¹ : Small.{w, u} B
inst✝ : Algebra R B
I : Ideal B
hI : I ^ 2 = ⊥
f g : A →ₐ[R] B
e : (Ideal.Quotient.mkₐ R I).comp f = (Ideal.Quotient.mkₐ R I).comp g
⊢ Ideal.map (Shrink.ringEquiv B).symm ⊥ = ⊥
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: case h₁
R : Type v
inst✝⁶ : CommRing R
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
B✝ : Type w
inst✝³ : CommRing B✝
inst✝² : FormallyUnramified R A
I✝ : Ideal B✝
hI✝ : IsNilpotent I✝
B : Type w
inst✝¹ : CommRing B
I : Ideal B
hI : I ^ 2 = ⊥
inst✝ : Algebra R B
⊢ Function.Injective (Ideal.Quotient.mkₐ R I).comp

Tactic:
;

Goal state after:
case h₁
R : Type v
inst✝⁶ : CommRing R
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
B✝ : Type w
inst✝³ : CommRing B✝
inst✝² : FormallyUnramified R A
I✝ : Ideal B✝
hI✝ : IsNilpotent I✝
B : Type w
inst✝¹ : CommRing B
I : Ideal B
hI : I ^ 2 = ⊥
inst✝ : Algebra R B
⊢ Function.Injective (Ideal.Quotient.mkₐ R I).comp
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommRing R
A : Type u_2
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
B : Type u_3
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FormallyUnramified R A
inst✝ : FormallyUnramified A B
⊢ FormallyUnramified R B

Tactic:
rw [iff_comp_injective]
  intro C _ _ I hI f₁ f₂ e
  have e' :=
    FormallyUnramified.lift_unique I ⟨2, hI⟩ (f₁.comp <| IsScalarTower.toAlgHom R A B)
      (f₂.comp <| IsScalarTower.toAlgHom R A B) (by rw [← AlgHom.comp_assoc, e, AlgHom.comp_assoc])
  let := (f₁.domRestrict A).toAlgebra
  let F₁ : B →ₐ[A] C := { f₁ with commutes' := fun r => rfl }
  let F₂ : B →ₐ[A] C := { f₂ with commutes' := AlgHom.congr_fun e'.symm }
  ext1 x
  change F₁ x = F₂ x
  congr
  exact FormallyUnramified.ext I ⟨2, hI⟩ (AlgHom.congr_fun e)

Goal state after: