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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹¹ : CommRing R
I : Ideal R
M : Type u_4
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
N : Type u_5
inst✝⁸ : AddCommGroup N
inst✝⁷ : Module R N
inst✝⁶ : SMul S R
inst✝⁵ : SMul Sᵐᵒᵖ R
inst✝⁴ : SMul S M
inst✝³ : SMul Sᵐᵒᵖ M
inst✝² : IsScalarTower S R M
inst✝¹ : IsScalarTower Sᵐᵒᵖ R M
inst✝ : IsCentralScalar S M
s : S
f : AdicCompletion I M
⊢ MulOpposite.op s • f = s • f

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Valuation.Integers

Goal state before:
pp: Γ₀ : Type v
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst✝ : Field K
v : Valuation K Γ₀
I : Ideal ↥v.integer
x : ↥v.integer
hx : x ∈ I
hx0 : x ≠ 0
y : ↥v.integer
hy : y ∈ v.leIdeal (v ↑x)
⊢ v (↑y / ↑x) ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type u_6
s : Finset ι
f : ι → AdicCompletion I M
⊢ ↑(∑ i ∈ s, f i) = ∑ i ∈ s, ↑(f i)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type u_6
s : Finset ι
f : ι → AdicCompletion I M
n : ℕ
⊢ ↑(∑ i ∈ s, f i) n = ∑ i ∈ s, ↑(f i) n

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Valuation.Integers

Goal state before:
pp: Γ₀ : Type v
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst✝ : Field K
v : Valuation K Γ₀
I : Ideal ↥v.integer
x : ↥v.integer
hx : x ∈ I
⊢ v.leIdeal (v ↑x) ≤ I

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_5
inst✝¹ : AddCommGroup N
inst✝ : Module R N
x : AdicCompletion I M
h : ∀ (n : ℕ), x ≡ 0 [SMOD I ^ n • ⊤]
n : ℕ
⊢ ↑x n = ↑0 n

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
ϖ : R
hϖ : ϖ ≠ 0
h : maximalIdeal R = span {ϖ}
⊢ Irreducible ϖ

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
ϖ : R
h : maximalIdeal R = span {ϖ}
e : ϖ = 0
⊢ maximalIdeal R = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m n : ℕ
hmn : m ≤ n
⊢ transitionMap I M hmn ∘ₗ eval I M n = eval I M m

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
⊢ ∃ ϖ, Irreducible ϖ

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_5
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ ∀ {a b : ℕ → M}, a ∈ {f | IsAdicCauchy I M f} → b ∈ {f | IsAdicCauchy I M f} → a + b ∈ {f | IsAdicCauchy I M f}

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_5
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ 0 ∈ {f | IsAdicCauchy I M f}

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_5
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ ∀ (c : R) {x : ℕ → M}, x ∈ {f | IsAdicCauchy I M f} → c • x ∈ {f | IsAdicCauchy I M f}

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : IsDiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toIsLocalRing✝ : IsLocalRing R
Rlocal : maximalIdeal R ≠ ⊥
q : R
hQ1 : R ∙ q ≠ ⊥
hQ2 : IsPrime (R ∙ q)
⊢ q ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_5
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ AddCommGroup (AdicCauchySequence I M)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → M
h : ∀ (n : ℕ), f n ≡ f (n + 1) [SMOD I ^ n • ⊤]
m n✝ n : ℕ
hmn : m ≤ n
ih : f m ≡ f n [SMOD I ^ m • ⊤]
⊢ ⊤ ≤ ⊤

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : ValuationRing R
⊢ IsBezout R

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ IsDiscreteValuationRing R ↔ IsPrincipalIdealRing R ∧ ∃! P, P ≠ ⊥ ∧ P.IsPrime

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → M
⊢ IsAdicCauchy I M f ↔ ∀ (n : ℕ), f n ≡ f (n + 1) [SMOD I ^ n • ⊤]

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsLocalRing R
inst✝ : IsBezout R
a b g : R
e : Ideal.span {a, b} = Ideal.span {g}
⊢ a ∈ {a, b}

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
a b : R
ha : Irreducible a
hb : Irreducible b
⊢ Associated a b

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
p q : R
hp : Irreducible p
hq : Irreducible q
ϖ : R
hϖ : Irreducible ϖ
hR : ∀ {x : R}, x ≠ 0 → ∃ n, Associated (ϖ ^ n) x
this : ∀ {p : R}, Irreducible p → Associated p ϖ
⊢ Associated p q

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_5
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : ℕ → M
h : ∀ (n : ℕ), f n ≡ f (n + 1) [SMOD I ^ n • ⊤]
⊢ IsAdicCauchy I M f

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsLocalRing R
inst✝ : IsBezout R
b g a : R
e : Ideal.span {a * g, b} = Ideal.span {g}
⊢ b ∈ {a * g, b}

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_5
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : AdicCauchySequence I M
⊢ ∀ {m n : ℕ} (hmn : m ≤ n),
    (transitionMap I M hmn) ((fun n ↦ (I ^ n • ⊤).mkQ (↑f n)) n) = (fun n ↦ (I ^ n • ⊤).mkQ (↑f n)) m

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsLocalRing R
inst✝ : IsBezout R
g a b : R
e : Ideal.span {a * g, b * g} = Ideal.span {g}
⊢ g ∈ {g}

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
ϖ : R
hϖ : Irreducible ϖ
hR : ∀ {x : R}, x ≠ 0 → ∃ n, Associated (ϖ ^ n) x
p : R
hp : Irreducible p
n : ℕ
hn : Associated (ϖ ^ n) p
this : Irreducible (ϖ ^ n)
H : n < 1
⊢ n = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : AdicCauchySequence I M
k : ℕ
h : ∀ n ≥ k, ∃ m ≥ n, ∃ l ≥ n, ↑f m ∈ I ^ l • ⊤
n : ℕ
⊢ n + k ≥ k

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : AdicCauchySequence I M
k : ℕ
h : ∀ n ≥ k, ∃ m ≥ n, ∃ l ≥ n, ↑f m ∈ I ^ l • ⊤
n m : ℕ
hnm : m ≥ n + k
l : ℕ
hnl : l ≥ n + k
hl : ↑f m ∈ I ^ l • ⊤
⊢ n ≤ l

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsLocalRing R
inst✝ : IsBezout R
g a b : R
e : Ideal.span {a * g, b * g} = Ideal.span {g}
x y : R
e' : x * (a * g) + y * (b * g) = g
h : g ≠ 0
⊢ x * a + y * b = 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
hR : HasUnitMulPowIrreducibleFactorization R
p q : R
hp : Irreducible p
hq : Irreducible q
⊢ Associated p q

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : AdicCauchySequence I M
h : ∃ k, ∀ n ≥ k, ∃ m ≥ n, ∃ l ≥ n, ↑f m ∈ I ^ l • ⊤
⊢ (mk I M) f = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsLocalRing R
inst✝ : IsBezout R
⊢ ValuationRing R

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ Function.Surjective ⇑(mk I M)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : AdicCompletion I M → Prop
x : AdicCompletion I M
h : ∀ (f : AdicCauchySequence I M), p ((mk I M) f)
⊢ p x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_5
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ n • ⊤
h : ∀ {m n : ℕ} (hle : m ≤ n), transitionMap I N hle ∘ₗ f n = f m
x y : M
⊢ ⟨fun n ↦ (f n) (x + y), ⋯⟩ = ⟨fun n ↦ (f n) x, ⋯⟩ + ⟨fun n ↦ (f n) y, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ [ValuationRing R, ∀ (x : FractionRing R), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹,
      Std.Total fun x1 x2 ↦ x1 ∣ x2, Std.Total fun x1 x2 ↦ x1 ≤ x2, IsLocalRing R ∧ IsBezout R].TFAE

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : Mul R
inst✝¹ : PreValuationRing R
inst✝ : Mul S
f : R →ₙ* S
hf : Function.Surjective ⇑f
a b : S
⊢ ∃ c, a * c = b ∨ b * c = a

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_5
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ n • ⊤
h : ∀ {m n : ℕ} (hle : m ≤ n), transitionMap I N hle ∘ₗ f n = f m
r : R
x : M
⊢ ⟨fun n ↦ (f n) (r • x), ⋯⟩ = (RingHom.id R) r • ⟨fun n ↦ (f n) x, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: 𝒪 : Type u
K : Type v
inst✝² : CommRing 𝒪
inst✝¹ : Field K
inst✝ : Algebra 𝒪 K
h : ∀ (x : K), ∃ a, x = (algebraMap 𝒪 K) a ∨ x⁻¹ = (algebraMap 𝒪 K) a
hinj : Function.Injective ⇑(algebraMap 𝒪 K)
this✝¹ : IsDomain 𝒪
this✝ : FaithfulSMul 𝒪 K
this : IsDomain 𝒪
⊢ ∀ (y : ↥(nonZeroDivisors 𝒪)), IsUnit ((algebraMap 𝒪 K) ↑y)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: 𝒪 : Type u
K : Type v
inst✝² : CommRing 𝒪
inst✝¹ : Field K
inst✝ : Algebra 𝒪 K
h : ∀ (x : K), ∃ a, x = (algebraMap 𝒪 K) a ∨ x⁻¹ = (algebraMap 𝒪 K) a
hinj : Function.Injective ⇑(algebraMap 𝒪 K)
this✝¹ : IsDomain 𝒪
this✝ : FaithfulSMul 𝒪 K
this : IsDomain 𝒪
x✝ y✝ : 𝒪
hab : (algebraMap 𝒪 K) x✝ = (algebraMap 𝒪 K) y✝
⊢ ↑1 * x✝ = ↑1 * y✝

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : IsHausdorff I M
x : M
hx : x = 0
⊢ (of I M) x = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: 𝒪 : Type u
K : Type v
inst✝² : CommRing 𝒪
inst✝¹ : Field K
inst✝ : Algebra 𝒪 K
h : ∀ (x : K), ∃ a, x = (algebraMap 𝒪 K) a ∨ x⁻¹ = (algebraMap 𝒪 K) a
hinj : Function.Injective ⇑(algebraMap 𝒪 K)
this✝¹ : IsDomain 𝒪
this✝ : FaithfulSMul 𝒪 K
this : IsDomain 𝒪
x : K
a : 𝒪
ha : x = (algebraMap 𝒪 K) a ∨ x⁻¹ = (algebraMap 𝒪 K) a
h0 : a = 0
⊢ x * (algebraMap 𝒪 K) ↑(0, 1).2 = (algebraMap 𝒪 K) (0, 1).1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ Function.Injective ⇑(of I M) ↔ IsHausdorff I M

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: 𝒪 : Type u
K : Type v
inst✝² : CommRing 𝒪
inst✝¹ : Field K
inst✝ : Algebra 𝒪 K
h : ∀ (x : K), ∃ a, x = (algebraMap 𝒪 K) a ∨ x⁻¹ = (algebraMap 𝒪 K) a
hinj : Function.Injective ⇑(algebraMap 𝒪 K)
this✝¹ : IsDomain 𝒪
this✝ : FaithfulSMul 𝒪 K
this : IsDomain 𝒪
x : K
a : 𝒪
ha : x = (algebraMap 𝒪 K) a ∨ x⁻¹ = (algebraMap 𝒪 K) a
h0 : ¬a = 0
⊢ (algebraMap 𝒪 K) a ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsCancelMulZero R
hR : HasUnitMulPowIrreducibleFactorization R
p : R := Classical.choose hR
spec : Irreducible (Classical.choose hR) ∧ ∀ {x : R}, x ≠ 0 → ∃ n, Associated (Classical.choose hR ^ n) x :=
  Classical.choose_spec hR
x : R
hx : x ≠ 0
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated f.prod x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: 𝒪 : Type u
K : Type v
inst✝² : CommRing 𝒪
inst✝¹ : Field K
inst✝ : Algebra 𝒪 K
h : ∀ (x : K), ∃ a, x = (algebraMap 𝒪 K) a ∨ x⁻¹ = (algebraMap 𝒪 K) a
hinj : Function.Injective ⇑(algebraMap 𝒪 K)
this✝² : IsDomain 𝒪
this✝¹ : FaithfulSMul 𝒪 K
this✝ : IsDomain 𝒪
x : K
a : 𝒪
h0 : ¬a = 0
this : (algebraMap 𝒪 K) a ≠ 0
ha : x = (algebraMap 𝒪 K) a
⊢ x * (algebraMap 𝒪 K) ↑(a, 1).2 = (algebraMap 𝒪 K) (a, 1).1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: 𝒪 : Type u
K : Type v
inst✝² : CommRing 𝒪
inst✝¹ : Field K
inst✝ : Algebra 𝒪 K
h : ∀ (x : K), ∃ a, x = (algebraMap 𝒪 K) a ∨ x⁻¹ = (algebraMap 𝒪 K) a
hinj : Function.Injective ⇑(algebraMap 𝒪 K)
this✝² : IsDomain 𝒪
this✝¹ : FaithfulSMul 𝒪 K
this✝ : IsDomain 𝒪
x : K
a : 𝒪
h0 : ¬a = 0
this : (algebraMap 𝒪 K) a ≠ 0
ha : x * (algebraMap 𝒪 K) a = 1
⊢ x * (algebraMap 𝒪 K) ↑(1, ⟨a, ⋯⟩).2 = (algebraMap 𝒪 K) (1, ⟨a, ⋯⟩).1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : IsPrecomplete I M
u : AdicCompletion I M
x : ℕ → M
hx : ∀ (n : ℕ), Submodule.Quotient.mk (x n) = ↑u n
m✝ n✝ : ℕ
hmn : m✝ ≤ n✝
⊢ x m✝ ≡ x n✝ [SMOD I ^ m✝ • ⊤]

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: 𝒪 : Type u
K : Type v
inst✝² : CommRing 𝒪
inst✝¹ : Field K
inst✝ : Algebra 𝒪 K
h : ∀ (x : K), ∃ a, x = (algebraMap 𝒪 K) a ∨ x⁻¹ = (algebraMap 𝒪 K) a
hinj : Function.Injective ⇑(algebraMap 𝒪 K)
⊢ IsFractionRing 𝒪 K

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ Function.Surjective ⇑(of I M) ↔ IsPrecomplete I M

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
I : Ideal R
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsAdicComplete I M
x : M
⊢ (ofLinearEquiv I M).symm ((of I M) x) = x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
I : Ideal R
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsAdicComplete I M
x : AdicCompletion I M
⊢ (of I M) ((ofLinearEquiv I M).symm x) = x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: 𝒪 : Type u
K : Type v
Γ : Type w
inst✝³ : CommRing 𝒪
inst✝² : Field K
inst✝¹ : Algebra 𝒪 K
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
hh : v.Integers 𝒪
⊢ ValuationRing 𝒪

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
⊢ I ^ n • ⊤ ≤ (eval I M n).ker

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: 𝒪 : Type u
K : Type v
inst✝⁴ : CommRing 𝒪
inst✝³ : Field K
inst✝² : Algebra 𝒪 K
inst✝¹ : IsDomain 𝒪
inst✝ : ValuationRing 𝒪
⊢ IsFractionRing 𝒪 K ↔
    (∀ (x : K), ∃ a, x = (algebraMap 𝒪 K) a ∨ x⁻¹ = (algebraMap 𝒪 K) a) ∧ Function.Injective ⇑(algebraMap 𝒪 K)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m n : ℕ
x : AdicCompletion I M
m_ge : n ≤ m
⊢ ↑x m ∈ I ^ n • ⊤ ↔ ↑x n = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : UniqueFactorizationMonoid R
h₁ : ∃ p, Irreducible p
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
⊢ HasUnitMulPowIrreducibleFactorization R

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
J : Ideal R[X]
j : Ideal R
hj : j ∈ {J | J.IsMaximal} ∧ map C j = J
this : j.IsMaximal
t : ⊥.jacobson = ⊥
⊢ J.jacobson = J

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
J : Ideal R[X]
j : Ideal R
hj : j ∈ {J | J.IsMaximal} ∧ map C j = J
this : j.IsMaximal
f : (R ⧸ j)[X]
hf : f ∈ ⊥.jacobson
⊢ X.coeff 1 ≠ coeff 0 1

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ ⊥.jacobson ≤ sInf (map C '' {J | J.IsMaximal})

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
I : Ideal R
M : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : CommRing S
inst✝² : Module S M
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R S M
⊢ IsAdicComplete (Ideal.map (algebraMap R S) I) M ↔ IsAdicComplete I M

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_4
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_5
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I N
f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ n • ⊤
h : ∀ {m n : ℕ} (hle : m ≤ n), Submodule.factorPow I N hle ∘ₗ f n = f m
x : M
⊢ (of I N) ((lift I f ⋯) x) = (AdicCompletion.lift I f ⋯) x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
h : ⊥.jacobson = ⊥
f : R[X]
hf : f ∈ sInf (map C '' {J | J.IsMaximal})
n : ℕ
this : f.coeff n ∈ ⊥.jacobson
⊢ f.coeff n = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_4
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_5
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I N
f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ n • ⊤
h : ∀ {m n : ℕ} (hle : m ≤ n), Submodule.factorPow I N hle ∘ₗ f n = f m
⊢ of I N ∘ₗ lift I f ⋯ = AdicCompletion.lift I f ⋯

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
h : ⊥.jacobson = ⊥
⊢ ⊥.jacobson = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : UniqueFactorizationMonoid R
h₁ : ∃ p, Irreducible p
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
I : Ideal R
I0 : ¬I = ⊥
x : R
hxI : x ∈ I
hx0 : x ≠ 0
p : R
left✝ : Irreducible p
H : ∀ {x : R}, x ≠ 0 → ∃ n, Associated (p ^ n) x
⊢ ∃ n, p ^ n ∈ I

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ IsJacobsonRing R ↔ ∀ (P : Ideal R), P.IsPrime → P.jacobson = P

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
H : IsJacobsonRing R
⊢ (∃ f, Function.Surjective ⇑f) → IsJacobsonRing S

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
I : Ideal R
inst✝ : IsJacobsonRing R
⊢ Function.Surjective ⇑(Ideal.Quotient.mk I)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.IsIntegral R S
inst✝ : IsJacobsonRing R
P : Ideal S
hP : P.IsPrime
hP_top : ¬comap (algebraMap R S) P = ⊤
⊢ Nontrivial (R ⧸ comap (algebraMap R S) P)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_4
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_5
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I N
f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ n • ⊤
h : ∀ {m n : ℕ} (hle : m ≤ n), Submodule.factorPow I N hle ∘ₗ f n = f m
n : ℕ
x : M
⊢ Submodule.Quotient.mk ((lift I f ⋯) x) = (f n) x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_4
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_5
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I N
f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ n • ⊤
h : ∀ {m n : ℕ} (hle : m ≤ n), Submodule.factorPow I N hle ∘ₗ f n = f m
n : ℕ
⊢ (I ^ n • ⊤).mkQ ∘ₗ lift I f ⋯ = f n

Tactic:
by

Goal state after: