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

Goal state before:
pp: case neg
A : Type u_8
B : Type u_9
C : Type u_10
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Ring C
inst✝¹ : Algebra A C
inst✝ : Algebra B C
e : A ≃+* B
he : (algebraMap B C).comp ↑e = algebraMap A C
x : C
h : ¬∃ s, Nonempty (Basis (↥s) B C)
⊢ 1 = 1

pp: case neg.h
A : Type u_8
B : Type u_9
C : Type u_10
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Ring C
inst✝¹ : Algebra A C
inst✝ : Algebra B C
e : A ≃+* B
he : (algebraMap B C).comp ↑e = algebraMap A C
x : C
h : ¬∃ s, Nonempty (Basis (↥s) B C)
⊢ ¬∃ s, Nonempty (Basis (↥s) A C)

Tactic:
]

Goal state after:
case neg.h
A : Type u_8
B : Type u_9
C : Type u_10
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Ring C
inst✝¹ : Algebra A C
inst✝ : Algebra B C
e : A ≃+* B
he : (algebraMap B C).comp ↑e = algebraMap A C
x : C
h : ¬∃ s, Nonempty (Basis (↥s) B C)
⊢ ¬∃ s, Nonempty (Basis (↥s) A C)
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: S : Type u_1
inst✝¹ : CommRing S
P : Ideal S
P_prime : P.IsPrime
inst✝ : IsDedekindDomain S
hP : P ≠ ⊥
i : ℕ
a c : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
c_mem : c ∈ span {a} ⊔ P ^ (i + 1)
eq_b : P ^ i = span {a} ⊔ P ^ (i + 1)
⊢ ∃ d, ∃ e ∈ P ^ (i + 1), a * d + e = c

Tactic:
]

Goal state after:
S : Type u_1
inst✝¹ : CommRing S
P : Ideal S
P_prime : P.IsPrime
inst✝ : IsDedekindDomain S
hP : P ≠ ⊥
i : ℕ
a c : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
c_mem : c ∈ span {a} ⊔ P ^ (i + 1)
eq_b : P ^ i = span {a} ⊔ P ^ (i + 1)
⊢ ∃ d, ∃ e ∈ P ^ (i + 1), a * d + e = c
Module: Mathlib.RingTheory.Norm.Basic

Goal state before:
pp: case refine_2
A₁ : Type u_8
B₁ : Type u_9
A₂ : Type u_10
B₂ : Type u_11
inst✝⁵ : CommRing A₁
inst✝⁴ : Ring B₁
inst✝³ : CommRing A₂
inst✝² : Ring B₂
inst✝¹ : Algebra A₁ B₁
inst✝ : Algebra A₂ B₂
e₁ : A₁ ≃+* A₂
e₂ : B₁ ≃+* B₂
he : (algebraMap A₂ B₂).comp ↑e₁ = (↑e₂).comp (algebraMap A₁ B₁)
x : B₁
this : Algebra A₁ B₂ := ((↑e₂).comp (algebraMap A₁ B₁)).toAlgebra' ?refine_1
e' : B₁ ≃ₐ[A₁] B₂ := { toEquiv := e₂.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
⊢ (norm A₁) (e' x) = e₁.symm (e₁ ((norm A₁) (e₂ x)))

Tactic:
]

Goal state after:
case refine_2
A₁ : Type u_8
B₁ : Type u_9
A₂ : Type u_10
B₂ : Type u_11
inst✝⁵ : CommRing A₁
inst✝⁴ : Ring B₁
inst✝³ : CommRing A₂
inst✝² : Ring B₂
inst✝¹ : Algebra A₁ B₁
inst✝ : Algebra A₂ B₂
e₁ : A₁ ≃+* A₂
e₂ : B₁ ≃+* B₂
he : (algebraMap A₂ B₂).comp ↑e₁ = (↑e₂).comp (algebraMap A₁ B₁)
x : B₁
this : Algebra A₁ B₂ := ((↑e₂).comp (algebraMap A₁ B₁)).toAlgebra' ?refine_1
e' : B₁ ≃ₐ[A₁] B₂ := { toEquiv := e₂.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
⊢ (norm A₁) (e' x) = e₁.symm (e₁ ((norm A₁) (e₂ x)))
Module: Mathlib.RingTheory.Artinian.Ring

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
⊢ IsNilpotent (Ideal.jacobson 0)

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
⊢ IsNilpotent (Ideal.jacobson 0)
Module: Mathlib.RingTheory.Artinian.Ring

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst✝² : CommSemiring L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
r₁ : R
s : ↥S
r₂ : R
h : IsLocalization.mk' L 1 s = (algebraMap R L) r₂
⊢ (algebraMap R L) r₁ * (algebraMap R L) r₂ = (algebraMap R L) r₁ * (algebraMap R L) r₂

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Artinian.Ring

Goal state before:
pp: case h
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst✝² : CommSemiring L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
r₁ : R
s : ↥S
n : ℕ
r : R
hr : ↑s ^ n * (↑s * r) = ↑s ^ n * 1
⊢ IsLocalization.mk' L 1 s = (algebraMap R L) r

Tactic:
]

Goal state after:
case h
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst✝² : CommSemiring L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
r₁ : R
s : ↥S
n : ℕ
r : R
hr : ↑s ^ n * (↑s * r) = ↑s ^ n * 1
⊢ IsLocalization.mk' L 1 s = (algebraMap R L) r
Module: Mathlib.RingTheory.FiniteStability

Goal state before:
pp: R : Type w₁
inst✝⁴ : CommRing R
A : Type w₂
inst✝³ : CommRing A
inst✝² : Algebra R A
B : Type w₃
inst✝¹ : CommRing B
inst✝ : Algebra R B
hfa : ∃ n f, Function.Surjective ⇑f
⊢ ∃ n f, Function.Surjective ⇑f

Tactic:
]

Goal state after:
R : Type w₁
inst✝⁴ : CommRing R
A : Type w₂
inst✝³ : CommRing A
inst✝² : Algebra R A
B : Type w₃
inst✝¹ : CommRing B
inst✝ : Algebra R B
hfa : ∃ n f, Function.Surjective ⇑f
⊢ ∃ n f, Function.Surjective ⇑f
Module: Mathlib.RingTheory.Artinian.Ring

Goal state before:
pp: case h
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst✝² : CommSemiring L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
r₁ : R
s : ↥S
n : ℕ
r : R
hr :
  (algebraMap R L) (↑s ^ n) * ((algebraMap R L) ↑s * (algebraMap R L) r) =
    (algebraMap R L) (↑s ^ n) * (algebraMap R L) 1
⊢ (algebraMap R L) ↑s * (algebraMap R L) r = (algebraMap R L) ↑s * (algebraMap R L) r

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.FiniteStability

Goal state before:
pp: R : Type w₁
inst✝⁵ : CommRing R
A : Type w₂
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B : Type w₃
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FinitePresentation R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hsurj : Function.Surjective ⇑f
hfg : (RingHom.ker f.toRingHom).FG
g : B ⊗[R] MvPolynomial (Fin n) R →ₐ[B] B ⊗[R] A := TensorProduct.map (AlgHom.id B B) f
hgsurj : Function.Surjective ⇑g
hker_eq : RingHom.ker g = Ideal.map TensorProduct.includeRight (RingHom.ker f)
⊢ (Ideal.map TensorProduct.includeRight (RingHom.ker f)).FG

Tactic:
]

Goal state after:
R : Type w₁
inst✝⁵ : CommRing R
A : Type w₂
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B : Type w₃
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FinitePresentation R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hsurj : Function.Surjective ⇑f
hfg : (RingHom.ker f.toRingHom).FG
g : B ⊗[R] MvPolynomial (Fin n) R →ₐ[B] B ⊗[R] A := TensorProduct.map (AlgHom.id B B) f
hgsurj : Function.Surjective ⇑g
hker_eq : RingHom.ker g = Ideal.map TensorProduct.includeRight (RingHom.ker f)
⊢ (Ideal.map TensorProduct.includeRight (RingHom.ker f)).FG
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: S : Type u_1
inst✝¹ : CommRing S
P : Ideal S
P_prime : P.IsPrime
inst✝ : IsDedekindDomain S
hP : P ≠ ⊥
i : ℕ
a c : S
a_mem : a ∈ P ^ i
c_mem : c ∈ P ^ i
this : P ^ (i + 1) = span {a} ⊔ P ^ (i + 1)
⊢ a ∈ span {a} ⊔ P ^ (i + 1)

Tactic:
]

Goal state after:
S : Type u_1
inst✝¹ : CommRing S
P : Ideal S
P_prime : P.IsPrime
inst✝ : IsDedekindDomain S
hP : P ≠ ⊥
i : ℕ
a c : S
a_mem : a ∈ P ^ i
c_mem : c ∈ P ^ i
this : P ^ (i + 1) = span {a} ⊔ P ^ (i + 1)
⊢ a ∈ span {a} ⊔ P ^ (i + 1)
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: S : Type u_1
inst✝¹ : CommRing S
P : Ideal S
P_prime : P.IsPrime
inst✝ : IsDedekindDomain S
hP : P ≠ ⊥
i : ℕ
ih : cardQuot (P ^ i) = cardQuot P ^ i
this : P ^ (i + 1) < P ^ i
hquot : ↥(map (mkQ (P ^ i.succ)) (P ^ i)) ≃ S ⧸ P
⊢ Nat.card (S ⧸ P) * Nat.card (S ⧸ P ^ i) = Nat.card (S ⧸ P) * Nat.card (S ⧸ P ^ i)

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative

Goal state before:
pp: case neg.refine_2.inl.inl
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_3
inst✝ : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this✝¹ : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝ : Nontrivial α
this : StrongNormalizationMonoid α := UniqueFactorizationMonoid.strongNormalizationMonoid
p : α
hp : p ∈ normalizedFactors a
q : α
hq : q ∈ normalizedFactors a
hdvd : p ∣ q
⊢ normalize p = normalize q

Tactic:
]

Goal state after:
case neg.refine_2.inl.inl
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_3
inst✝ : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this✝¹ : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝ : Nontrivial α
this : StrongNormalizationMonoid α := UniqueFactorizationMonoid.strongNormalizationMonoid
p : α
hp : p ∈ normalizedFactors a
q : α
hq : q ∈ normalizedFactors a
hdvd : p ∣ q
⊢ normalize p = normalize q
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative

Goal state before:
pp: case neg.refine_2.inl.inr
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_3
inst✝ : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this✝¹ : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝ : Nontrivial α
this : StrongNormalizationMonoid α := UniqueFactorizationMonoid.strongNormalizationMonoid
p : α
hp : p ∈ normalizedFactors a
q : α
hq : q ∈ normalizedFactors b
hdvd : p ∣ q
⊢ normalize p = normalize q

Tactic:
]

Goal state after:
case neg.refine_2.inl.inr
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_3
inst✝ : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this✝¹ : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝ : Nontrivial α
this : StrongNormalizationMonoid α := UniqueFactorizationMonoid.strongNormalizationMonoid
p : α
hp : p ∈ normalizedFactors a
q : α
hq : q ∈ normalizedFactors b
hdvd : p ∣ q
⊢ normalize p = normalize q
Module: Mathlib.RingTheory.Finiteness.NilpotentKer

Goal state before:
pp: case zero
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Module.Finite R T
f : S →ₐ[R] T
hf₁ : Function.Surjective ⇑f
I : Ideal S
hI : RingHom.ker f = I
hf₂ : I ≤ nilradical S
hf₃ : I.FG
this : Module.Finite R (S ⧸ I)
⊢ Module.Finite R (S ⧸ ⊤)

Tactic:
]

Goal state after:
case zero
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Module.Finite R T
f : S →ₐ[R] T
hf₁ : Function.Surjective ⇑f
I : Ideal S
hI : RingHom.ker f = I
hf₂ : I ≤ nilradical S
hf₃ : I.FG
this : Module.Finite R (S ⧸ I)
⊢ Module.Finite R (S ⧸ ⊤)
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: case succ.refine_1
S : Type u_1
inst✝¹ : CommRing S
P : Ideal S
P_prime : P.IsPrime
inst✝ : IsDedekindDomain S
hP : P ≠ ⊥
i : ℕ
ih : cardQuot (P ^ i) = cardQuot P ^ i
this : P ^ (i + 1) < P ^ i
a : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
f g : (c : S) → c ∈ P ^ i → S
hg : ∀ (c : S) (hc : c ∈ P ^ i), g c hc ∈ P ^ (i + 1)
hf : ∀ (c : S) (hc : c ∈ P ^ i), a * f c hc + g c hc = c
k : (c' : S ⧸ P ^ i.succ) → c' ∈ map (mkQ (P ^ i.succ)) (P ^ i) → S
hk_mem : ∀ (c' : S ⧸ P ^ i.succ) (hc' : c' ∈ map (mkQ (P ^ i.succ)) (P ^ i)), k c' hc' ∈ P ^ i
hk_eq : ∀ (c' : S ⧸ P ^ i.succ) (hc' : c' ∈ map (mkQ (P ^ i.succ)) (P ^ i)), (mkQ (P ^ i.succ)) (k c' hc') = c'
c₁' : S ⧸ P ^ i.succ
hc₁' : c₁' ∈ map (mkQ (P ^ i.succ)) (P ^ i)
c₂' : S ⧸ P ^ i.succ
hc₂' : c₂' ∈ map (mkQ (P ^ i.succ)) (P ^ i)
h : (fun c' ↦ Quotient.mk'' (f (k ↑c' ⋯) ⋯)) ⟨c₁', hc₁'⟩ = (fun c' ↦ Quotient.mk'' (f (k ↑c' ⋯) ⋯)) ⟨c₂', hc₂'⟩
⊢ a * f (k c₁' hc₁') ⋯ + g (k c₁' hc₁') ⋯ - (a * f (k c₂' hc₂') ⋯ + g (k c₂' hc₂') ⋯) ∈ P ^ i.succ

Tactic:
]

Goal state after:
case succ.refine_1
S : Type u_1
inst✝¹ : CommRing S
P : Ideal S
P_prime : P.IsPrime
inst✝ : IsDedekindDomain S
hP : P ≠ ⊥
i : ℕ
ih : cardQuot (P ^ i) = cardQuot P ^ i
this : P ^ (i + 1) < P ^ i
a : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
f g : (c : S) → c ∈ P ^ i → S
hg : ∀ (c : S) (hc : c ∈ P ^ i), g c hc ∈ P ^ (i + 1)
hf : ∀ (c : S) (hc : c ∈ P ^ i), a * f c hc + g c hc = c
k : (c' : S ⧸ P ^ i.succ) → c' ∈ map (mkQ (P ^ i.succ)) (P ^ i) → S
hk_mem : ∀ (c' : S ⧸ P ^ i.succ) (hc' : c' ∈ map (mkQ (P ^ i.succ)) (P ^ i)), k c' hc' ∈ P ^ i
hk_eq : ∀ (c' : S ⧸ P ^ i.succ) (hc' : c' ∈ map (mkQ (P ^ i.succ)) (P ^ i)), (mkQ (P ^ i.succ)) (k c' hc') = c'
c₁' : S ⧸ P ^ i.succ
hc₁' : c₁' ∈ map (mkQ (P ^ i.succ)) (P ^ i)
c₂' : S ⧸ P ^ i.succ
hc₂' : c₂' ∈ map (mkQ (P ^ i.succ)) (P ^ i)
h : (fun c' ↦ Quotient.mk'' (f (k ↑c' ⋯) ⋯)) ⟨c₁', hc₁'⟩ = (fun c' ↦ Quotient.mk'' (f (k ↑c' ⋯) ⋯)) ⟨c₂', hc₂'⟩
⊢ a * f (k c₁' hc₁') ⋯ + g (k c₁' hc₁') ⋯ - (a * f (k c₂' hc₂') ⋯ + g (k c₂' hc₂') ⋯) ∈ P ^ i.succ
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative

Goal state before:
pp: case neg.refine_2.inr.inl
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_3
inst✝ : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this✝¹ : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝ : Nontrivial α
this : StrongNormalizationMonoid α := UniqueFactorizationMonoid.strongNormalizationMonoid
p : α
hp : p ∈ normalizedFactors b
q : α
hq : q ∈ normalizedFactors a
hdvd : p ∣ q
⊢ normalize p = normalize q

Tactic:
]

Goal state after:
case neg.refine_2.inr.inl
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_3
inst✝ : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this✝¹ : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝ : Nontrivial α
this : StrongNormalizationMonoid α := UniqueFactorizationMonoid.strongNormalizationMonoid
p : α
hp : p ∈ normalizedFactors b
q : α
hq : q ∈ normalizedFactors a
hdvd : p ∣ q
⊢ normalize p = normalize q
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative

Goal state before:
pp: case neg.refine_2.inr.inr
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_3
inst✝ : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this✝¹ : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝ : Nontrivial α
this : StrongNormalizationMonoid α := UniqueFactorizationMonoid.strongNormalizationMonoid
p : α
hp : p ∈ normalizedFactors b
q : α
hq : q ∈ normalizedFactors b
hdvd : p ∣ q
⊢ normalize p = normalize q

Tactic:
]

Goal state after:
case neg.refine_2.inr.inr
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_3
inst✝ : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this✝¹ : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝ : Nontrivial α
this : StrongNormalizationMonoid α := UniqueFactorizationMonoid.strongNormalizationMonoid
p : α
hp : p ∈ normalizedFactors b
q : α
hq : q ∈ normalizedFactors b
hdvd : p ∣ q
⊢ normalize p = normalize q
Module: Mathlib.RingTheory.Finiteness.NilpotentKer

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Module.Finite R T
f : S →ₐ[R] T
hf₁ : Function.Surjective ⇑f
I : Ideal S
hI : RingHom.ker f = I
hf₂ : I ≤ nilradical S
hf₃ : I.FG
this✝ : Module.Finite R (S ⧸ I)
n : ℕ
IH : Module.Finite R (S ⧸ I ^ n)
φ : S ⧸ I ^ (n + 1) →ₐ[S] S ⧸ I ^ n := Ideal.Quotient.factorₐ S ⋯
hφ : Function.Surjective ⇑φ
hφ' : φ.toLinearMap ∘ₗ Submodule.mkQ (I ^ (n + 1)) = Submodule.mkQ (I ^ n)
this : Module.Finite R ((S ⧸ I) ⊗[S] ↥(I ^ n))
⊢ I • Submodule.map (Submodule.subtype (I ^ n)) ⊤ ≤
    (Submodule.subtype (I ^ n)).range ⊓ (Submodule.mkQ (I ^ (n + 1))).ker

Tactic:
]

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Module.Finite R T
f : S →ₐ[R] T
hf₁ : Function.Surjective ⇑f
I : Ideal S
hI : RingHom.ker f = I
hf₂ : I ≤ nilradical S
hf₃ : I.FG
this✝ : Module.Finite R (S ⧸ I)
n : ℕ
IH : Module.Finite R (S ⧸ I ^ n)
φ : S ⧸ I ^ (n + 1) →ₐ[S] S ⧸ I ^ n := Ideal.Quotient.factorₐ S ⋯
hφ : Function.Surjective ⇑φ
hφ' : φ.toLinearMap ∘ₗ Submodule.mkQ (I ^ (n + 1)) = Submodule.mkQ (I ^ n)
this : Module.Finite R ((S ⧸ I) ⊗[S] ↥(I ^ n))
⊢ I • Submodule.map (Submodule.subtype (I ^ n)) ⊤ ≤
    (Submodule.subtype (I ^ n)).range ⊓ (Submodule.mkQ (I ^ (n + 1))).ker
Module: Mathlib.RingTheory.Spectrum.Prime.Noetherian

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
p : Ideal R
inst✝ : p.IsPrime
r : R
hr : (toPiLocalization R) r = Pi.single { asIdeal := p, isPrime := ⋯ } 1
this : (algebraMap R (Localization p.primeCompl)) r = 1
⊢ 1 ∉ IsLocalRing.maximalIdeal (Localization.AtPrime p)

Tactic:
]

Goal state after:
case refine_1
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
p : Ideal R
inst✝ : p.IsPrime
r : R
hr : (toPiLocalization R) r = Pi.single { asIdeal := p, isPrime := ⋯ } 1
this : (algebraMap R (Localization p.primeCompl)) r = 1
⊢ 1 ∉ IsLocalRing.maximalIdeal (Localization.AtPrime p)
Module: Mathlib.RingTheory.Spectrum.Prime.Noetherian

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
p : Ideal R
inst✝ : p.IsPrime
r : R
hr : (toPiLocalization R) r = Pi.single { asIdeal := p, isPrime := ⋯ } 1
this✝ : (algebraMap R (Localization p.primeCompl)) r = 1
q : Ideal R
hq : q.IsPrime
e : q ≠ p
this : { asIdeal := q, isPrime := ⋯ } ≠ { asIdeal := p, isPrime := ⋯ }
⊢ (algebraMap R (Localization.AtPrime q)) r = 0

Tactic:
simpa [PrimeSpectrum.toPiLocalization, this,
        -FaithfulSMul.algebraMap_eq_zero_iff] using funext_iff.mp hr ⟨q, inferInstance⟩

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

Goal state before:
pp: case refine_3
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
p : Ideal R
inst✝ : p.IsPrime
r : R
hr : (toPiLocalization R) r = Pi.single { asIdeal := p, isPrime := ⋯ } 1
this✝¹ : (algebraMap R (Localization p.primeCompl)) r = 1
q : Ideal R
hq : q.IsPrime
e : q ≠ p
this✝ : { asIdeal := q, isPrime := ⋯ } ≠ { asIdeal := p, isPrime := ⋯ }
this : (algebraMap R (Localization.AtPrime q)) r = 0
⊢ 0 ∈ IsLocalRing.maximalIdeal (Localization.AtPrime q)

Tactic:
]

Goal state after:
case refine_3
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
p : Ideal R
inst✝ : p.IsPrime
r : R
hr : (toPiLocalization R) r = Pi.single { asIdeal := p, isPrime := ⋯ } 1
this✝¹ : (algebraMap R (Localization p.primeCompl)) r = 1
q : Ideal R
hq : q.IsPrime
e : q ≠ p
this✝ : { asIdeal := q, isPrime := ⋯ } ≠ { asIdeal := p, isPrime := ⋯ }
this : (algebraMap R (Localization.AtPrime q)) r = 0
⊢ 0 ∈ IsLocalRing.maximalIdeal (Localization.AtPrime q)
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: case succ.refine_2.h
S : Type u_1
inst✝¹ : CommRing S
P : Ideal S
P_prime : P.IsPrime
inst✝ : IsDedekindDomain S
hP : P ≠ ⊥
i : ℕ
ih : cardQuot (P ^ i) = cardQuot P ^ i
this : P ^ (i + 1) < P ^ i
a : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
f g : (c : S) → c ∈ P ^ i → S
hg : ∀ (c : S) (hc : c ∈ P ^ i), g c hc ∈ P ^ (i + 1)
hf : ∀ (c : S) (hc : c ∈ P ^ i), a * f c hc + g c hc = c
k : (c' : S ⧸ P ^ i.succ) → c' ∈ map (mkQ (P ^ i.succ)) (P ^ i) → S
hk_mem : ∀ (c' : S ⧸ P ^ i.succ) (hc' : c' ∈ map (mkQ (P ^ i.succ)) (P ^ i)), k c' hc' ∈ P ^ i
hk_eq : ∀ (c' : S ⧸ P ^ i.succ) (hc' : c' ∈ map (mkQ (P ^ i.succ)) (P ^ i)), (mkQ (P ^ i.succ)) (k c' hc') = c'
d : S
hd' : (mkQ (P ^ i.succ)) (a * d) ∈ map (mkQ (P ^ i.succ)) (P ^ i)
⊢ k ((mkQ (P ^ i.succ)) (a * d)) ⋯ - a * d ∈ P ^ (i + 1)

Tactic:
]

Goal state after:
case succ.refine_2.h
S : Type u_1
inst✝¹ : CommRing S
P : Ideal S
P_prime : P.IsPrime
inst✝ : IsDedekindDomain S
hP : P ≠ ⊥
i : ℕ
ih : cardQuot (P ^ i) = cardQuot P ^ i
this : P ^ (i + 1) < P ^ i
a : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
f g : (c : S) → c ∈ P ^ i → S
hg : ∀ (c : S) (hc : c ∈ P ^ i), g c hc ∈ P ^ (i + 1)
hf : ∀ (c : S) (hc : c ∈ P ^ i), a * f c hc + g c hc = c
k : (c' : S ⧸ P ^ i.succ) → c' ∈ map (mkQ (P ^ i.succ)) (P ^ i) → S
hk_mem : ∀ (c' : S ⧸ P ^ i.succ) (hc' : c' ∈ map (mkQ (P ^ i.succ)) (P ^ i)), k c' hc' ∈ P ^ i
hk_eq : ∀ (c' : S ⧸ P ^ i.succ) (hc' : c' ∈ map (mkQ (P ^ i.succ)) (P ^ i)), (mkQ (P ^ i.succ)) (k c' hc') = c'
d : S
hd' : (mkQ (P ^ i.succ)) (a * d) ∈ map (mkQ (P ^ i.succ)) (P ^ i)
⊢ k ((mkQ (P ^ i.succ)) (a * d)) ⋯ - a * d ∈ P ^ (i + 1)
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDedekindDomain S
inst✝ : Free ℤ S
this : Infinite S
⊢ 0 = 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
⊢ 1 = 1

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
I J : Ideal S
⊢ cardQuot I * cardQuot J = cardQuot I * cardQuot J

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
⊢ 0 = 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
I : Ideal S
⊢ I = ⊤ ↔ I = ⊤

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
I : Ideal S
⊢ 0 = 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
I : Ideal S
hI : Nat.Prime (absNorm I)
⊢ Nat.Prime (absNorm I)

Tactic:
]

Goal state after:
S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDedekindDomain S
inst✝ : Free ℤ S
I : Ideal S
hI : Nat.Prime (absNorm I)
⊢ Nat.Prime (absNorm I)
Module: Mathlib.RingTheory.Jacobson.Artinian

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra.FiniteType R A
inst✝ : IsArtinianRing R
this : IsNoetherianRing A
⊢ Ring.KrullDimLE 0 A ↔ Ring.KrullDimLE 0 A

Tactic:
]

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

Goal state before:
pp: case IJ
S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDedekindDomain S
inst✝ : Free ℤ S
I : Ideal S
hI : Nat.Prime (absNorm I)
this : (span {↑(absNorm I)}).IsPrime
⊢ ↑(absNorm I) ∈ I

Tactic:
]

Goal state after:
case IJ
S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDedekindDomain S
inst✝ : Free ℤ S
I : Ideal S
hI : Nat.Prime (absNorm I)
this : (span {↑(absNorm I)}).IsPrime
⊢ ↑(absNorm I) ∈ I
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDedekindDomain S
inst✝ : Free ℤ S
I : Ideal S
hI : Nat.Prime (absNorm I)
this : (span {↑(absNorm I)}).IsPrime
⊢ ¬↑(absNorm I) = 0

Tactic:
]

Goal state after:
S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDedekindDomain S
inst✝ : Free ℤ S
I : Ideal S
hI : Nat.Prime (absNorm I)
this : (span {↑(absNorm I)}).IsPrime
⊢ ¬↑(absNorm I) = 0