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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_3
P : Type u_4
inst✝³ : AddCommGroup N
inst✝² : AddCommGroup P
inst✝¹ : Module R N
inst✝ : Module R P
f : N →ₗ[R] M
g : M →ₗ[R] P
hf : Function.Injective ⇑f
hg : Function.Surjective ⇑g
H : Function.Exact ⇑f ⇑g
hP : IsFiniteLength R P
hN : IsFiniteLength R N
s : CompositionSeries (Submodule R P)
hs₁ : RelSeries.head s = ⊥
hs₂ : RelSeries.last s = ⊤
t : CompositionSeries (Submodule R N)
ht₁ : RelSeries.head t = ⊥
ht₂ : RelSeries.last t = ⊤
s' : CompositionSeries (Submodule R M) := RelSeries.map s { toFun := Submodule.comap g, map_rel' := ⋯ }
t' : CompositionSeries (Submodule R M) := RelSeries.map t { toFun := Submodule.map f, map_rel' := ⋯ }
hfg : Submodule.map f ⊤ = Submodule.comap g ⊥
r : RelSeries {(x, y) | JordanHolderLattice.IsMaximal x y} := RelSeries.smash t' s' ⋯
⊢ r.last = ⊤

Tactic:
simpa using

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_3
P : Type u_4
inst✝³ : AddCommGroup N
inst✝² : AddCommGroup P
inst✝¹ : Module R N
inst✝ : Module R P
f : N →ₗ[R] M
g : M →ₗ[R] P
hf : Function.Injective ⇑f
hg : Function.Surjective ⇑g
H : Function.Exact ⇑f ⇑g
hP : IsFiniteLength R P
hN : IsFiniteLength R N
s : CompositionSeries (Submodule R P)
hs₁ : RelSeries.head s = ⊥
hs₂ : RelSeries.last s = ⊤
t : CompositionSeries (Submodule R N)
ht₁ : RelSeries.head t = ⊥
ht₂ : RelSeries.last t = ⊤
s' : CompositionSeries (Submodule R M) := RelSeries.map s { toFun := Submodule.comap g, map_rel' := ⋯ }
t' : CompositionSeries (Submodule R M) := RelSeries.map t { toFun := Submodule.map f, map_rel' := ⋯ }
hfg : Submodule.map f ⊤ = Submodule.comap g ⊥
r : RelSeries {(x, y) | JordanHolderLattice.IsMaximal x y} := RelSeries.smash t' s' ⋯
⊢ Submodule.comap g ⊤ = ⊤
Module: Mathlib.RingTheory.Valuation.Integers

Goal state before:
pp: F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
I : Ideal O
x : Γ₀
hx : IsGreatest (⇑v ∘ ⇑(algebraMap O F) '' ↑I) x
⊢ ∃ a ∈ I, (⇑v ∘ ⇑(algebraMap O F)) a = x

Tactic:
simpa using

Goal state after:
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
I : Ideal O
x : Γ₀
hx : IsGreatest (⇑v ∘ ⇑(algebraMap O F) '' ↑I) x
⊢ ∃ a ∈ I, v ((algebraMap O F) a) = x
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✝ : IsHausdorff I M
x y : M
h : ∀ (n : ℕ), x ≡ y [SMOD I ^ n • ⊤]
⊢ ∀ (n : ℕ), x - y ≡ 0 [SMOD I ^ n • ⊤]

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝³ : CommRing R
I : Ideal R
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsHausdorff I M
x y : M
h : ∀ (n : ℕ), x ≡ y [SMOD I ^ n • ⊤]
⊢ ∀ (n : ℕ), x - y ∈ I ^ n • ⊤
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 : M
hx : ∀ (n : ℕ), x ≡ 0 [SMOD ⊥ ^ n • ⊤]
⊢ x = 0

Tactic:
simpa using

Goal state after:
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 : M
hx : ∀ (n : ℕ), x ≡ 0 [SMOD ⊥ ^ n • ⊤]
⊢ x = 0
Module: Mathlib.RingTheory.Valuation.Integers

Goal state before:
pp: F : Type u
Γ₀ : Type v
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝² : CommRing O
inst✝¹ : Algebra O F
inst✝ : IsPrincipalIdealRing O
hv : v.Integers O
H : DenselyOrdered ↑(range ⇑v)
a b : O
ha : a ∈ ⇑v ∘ ⇑(algebraMap O F) ⁻¹' Iio 1
hb : b ∈ ⇑v ∘ ⇑(algebraMap O F) ⁻¹' Iio 1
⊢ a + b ∈ ⇑v ∘ ⇑(algebraMap O F) ⁻¹' Iio 1

Tactic:
simpa using

Goal state after:
F : Type u
Γ₀ : Type v
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝² : CommRing O
inst✝¹ : Algebra O F
inst✝ : IsPrincipalIdealRing O
hv : v.Integers O
H : DenselyOrdered ↑(range ⇑v)
a b : O
ha : a ∈ ⇑v ∘ ⇑(algebraMap O F) ⁻¹' Iio 1
hb : b ∈ ⇑v ∘ ⇑(algebraMap O F) ⁻¹' Iio 1
⊢ v ((algebraMap O F) a + (algebraMap O F) b) < 1
Module: Mathlib.RingTheory.Valuation.Integers

Goal state before:
pp: F : Type u
Γ₀ : Type v
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝² : CommRing O
inst✝¹ : Algebra O F
inst✝ : IsPrincipalIdealRing O
hv : v.Integers O
H : DenselyOrdered ↑(range ⇑v)
I : Ideal O := { carrier := ⇑v ∘ ⇑(algebraMap O F) ⁻¹' Iio 1, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
⊢ ∃ x, v ((algebraMap O F) x) < 1 ∧ v ((algebraMap O F) x) ∈ upperBounds (Iio 1 ∩ range (⇑v ∘ ⇑(algebraMap O F)))

Tactic:
simpa using

Goal state after:
F : Type u
Γ₀ : Type v
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝² : CommRing O
inst✝¹ : Algebra O F
inst✝ : IsPrincipalIdealRing O
hv : v.Integers O
H : DenselyOrdered ↑(range ⇑v)
I : Ideal O := { carrier := ⇑v ∘ ⇑(algebraMap O F) ⁻¹' Iio 1, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
⊢ ∃ x,
    v ((algebraMap O F) x) < 1 ∧
      v ((algebraMap O F) x) ∈ upperBounds ((fun a ↦ v ((algebraMap O F) a)) '' ⇑v ∘ ⇑(algebraMap O F) ⁻¹' Iio 1)
Module: Mathlib.RingTheory.Valuation.Integers

Goal state before:
pp: F : Type u
Γ₀ : Type v
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝² : CommRing O
inst✝¹ : Algebra O F
inst✝ : IsPrincipalIdealRing O
hv : v.Integers O
H : DenselyOrdered ↑(range ⇑v)
I : Ideal O := { carrier := ⇑v ∘ ⇑(algebraMap O F) ⁻¹' Iio 1, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
x : O
hx₁ : v ((algebraMap O F) x) < 1
hx : v ((algebraMap O F) x) ∈ upperBounds (Iio 1 ∩ range (⇑v ∘ ⇑(algebraMap O F)))
⊢ ∃ y, v ((algebraMap O F) x) < v y ∧ v y < 1

Tactic:
simpa using

Goal state after:
F : Type u
Γ₀ : Type v
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝² : CommRing O
inst✝¹ : Algebra O F
inst✝ : IsPrincipalIdealRing O
hv : v.Integers O
H : DenselyOrdered ↑(range ⇑v)
I : Ideal O := { carrier := ⇑v ∘ ⇑(algebraMap O F) ⁻¹' Iio 1, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
x : O
hx₁ : v ((algebraMap O F) x) < 1
hx : v ((algebraMap O F) x) ∈ upperBounds (Iio 1 ∩ range (⇑v ∘ ⇑(algebraMap O F)))
⊢ ∃ y, v ((algebraMap O F) x) < v y ∧ v y < 1
Module: Mathlib.RingTheory.Valuation.Integers

Goal state before:
pp: R : Type u
Γ₀ : Type v
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ : Γ₀
r : ↥v.integer
x : R
h : x ∈ (v.leAddSubgroup γ).carrier
⊢ r • x ∈ (v.leAddSubgroup γ).carrier

Tactic:
simpa using

Goal state after:
R : Type u
Γ₀ : Type v
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ : Γ₀
r : ↥v.integer
x : R
h : x ∈ (v.leAddSubgroup γ).carrier
⊢ v ↑r * v x ≤ γ
Module: Mathlib.RingTheory.Valuation.Integers

Goal state before:
pp: R : Type u
Γ₀ : Type v
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ : Γ₀ˣ
r : ↥v.integer
x : R
h : x ∈ (v.ltAddSubgroup γ).carrier
⊢ r • x ∈ (v.ltAddSubgroup γ).carrier

Tactic:
simpa using

Goal state after:
R : Type u
Γ₀ : Type v
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ : Γ₀ˣ
r : ↥v.integer
x : R
h : x ∈ (v.ltAddSubgroup γ).carrier
⊢ v ↑r * v x < ↑γ
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: case zero
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
hf : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD ⊥ ^ m • ⊤]
⊢ f 0 ≡ f 1 [SMOD ⊥ ^ 0 • ⊤]

pp: case succ
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
hf : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD ⊥ ^ m • ⊤]
n : ℕ
⊢ f (n + 1) ≡ f 1 [SMOD ⊥ ^ (n + 1) • ⊤]

Tactic:
· rw [pow_zero, Ideal.one_eq_top, top_smul]
    exact SModEq.top

Goal state after:
case succ
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
hf : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD ⊥ ^ m • ⊤]
n : ℕ
⊢ f (n + 1) ≡ f 1 [SMOD ⊥ ^ (n + 1) • ⊤]
Module: Mathlib.RingTheory.Valuation.Integers

Goal state before:
pp: case inr
Γ₀ : Type v
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst✝ : Field K
v : Valuation K Γ₀
S : Submodule (↥v.integer) K
x : K
hx : x ∈ S
hx0 : x ≠ 0
y : K
hy : y ∈ v.leSubmodule (v x)
this : v (y / x) ≤ 1
⊢ y ∈ S

Tactic:
simpa using

Goal state after:
case inr
Γ₀ : Type v
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst✝ : Field K
v : Valuation K Γ₀
S : Submodule (↥v.integer) K
x : K
hx : x ∈ S
hx0 : x ≠ 0
y : K
hy : y ∈ v.leSubmodule (v x)
this : v (y / x) ≤ 1
⊢ y ∈ S
Module: Mathlib.RingTheory.Valuation.Integers

Goal state before:
pp: R : Type u
Γ₀ : Type v
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ : Γ₀
r x : ↥v.integer
h : x ∈ ((v.leAddSubgroup γ).addSubgroupOf v.integer.toAddSubgroup).carrier
⊢ ↑(r • x) ∈ v.leAddSubgroup γ

Tactic:
simpa using

Goal state after:
R : Type u
Γ₀ : Type v
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ : Γ₀
r x : ↥v.integer
h : x ∈ ((v.leAddSubgroup γ).addSubgroupOf v.integer.toAddSubgroup).carrier
⊢ v ↑r * v ↑x ≤ γ
Module: Mathlib.RingTheory.Valuation.Integers

Goal state before:
pp: R : Type u
Γ₀ : Type v
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ : Γ₀ˣ
r x : ↥v.integer
h : x ∈ ((v.ltAddSubgroup γ).addSubgroupOf v.integer.toAddSubgroup).carrier
⊢ v (↑r * ↑x) < ↑γ

Tactic:
simpa using

Goal state after:
R : Type u
Γ₀ : Type v
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ : Γ₀ˣ
r x : ↥v.integer
h : x ∈ ((v.ltAddSubgroup γ).addSubgroupOf v.integer.toAddSubgroup).carrier
⊢ v ↑r * v ↑x < ↑γ
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: case neg.inl
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
H : ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
a b : R
ha : (algebraMap R K) a ≠ 0
hb : (algebraMap R K) b ≠ 0
c : R
e : b * c = a
⊢ ∃ c, a * c = b ∨ b * c = a

Tactic:
exact ⟨c, Or.inr e⟩

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:
simpa using

Goal state after:
Γ₀ : 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 / v ↑x ≤ 1
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) (Submodule.Quotient.mk (↑f n)) = Submodule.Quotient.mk (↑f m)

Tactic:
exact (f.property hmn).symm

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

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

Tactic:
simp [not_irreducible_one, pow_zero] at this

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

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

Tactic:
simpa using

Goal state after:
case inr.inl
R : Type u_1
inst✝ : CommRing R
ϖ : R
hϖ : Irreducible ϖ
hR : ∀ {x : R}, x ≠ 0 → ∃ n, Associated (ϖ ^ n) x
p : R
hp : Irreducible p
hn : Associated (ϖ ^ 1) p
this : Irreducible (ϖ ^ 1)
⊢ Associated p ϖ
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 • ⊤
⊢ Submodule.Quotient.mk (↑f m) = 0 n

Tactic:
simpa using

Goal state after:
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 • ⊤
⊢ ↑f m ∈ I ^ n • ⊤
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:
simpa using

Goal state after:
𝒪 : 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✝
⊢ x✝ = y✝
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: case mp
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : Function.Injective ⇑(of I M)
x : M
hx : ∀ (n : ℕ), x ≡ 0 [SMOD I ^ n • ⊤]
n : ℕ
⊢ ↑((of I M) x) n = ↑((of I M) 0) n

Tactic:
simpa using

Goal state after:
case mp
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : Function.Injective ⇑(of I M)
x : M
hx : ∀ (n : ℕ), x ≡ 0 [SMOD I ^ n • ⊤]
n : ℕ
⊢ x ∈ I ^ n • ⊤
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:
simpa using

Goal state after:
𝒪 : 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 = 0
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: case pos
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
q : R
hq : q ∈ Multiset.replicate (Classical.choose ⋯) p
hpq : q = p
b : R
m : ℕ
u : Rˣ
h : p ∣ Classical.choose hR ^ m * b
ha : ¬Classical.choose hR ^ m * ↑u = 0
hm : m = 0
⊢ p ∣ Classical.choose hR ^ m ∨ p ∣ b

pp: case neg
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
q : R
hq : q ∈ Multiset.replicate (Classical.choose ⋯) p
hpq : q = p
b : R
m : ℕ
u : Rˣ
h : p ∣ Classical.choose hR ^ m * b
ha : ¬Classical.choose hR ^ m * ↑u = 0
hm : ¬m = 0
⊢ p ∣ Classical.choose hR ^ m ∨ p ∣ b

Tactic:
· simp only [hm, one_mul, pow_zero] at h ⊢
        right
        exact h

Goal state after:
case neg
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
q : R
hq : q ∈ Multiset.replicate (Classical.choose ⋯) p
hpq : q = p
b : R
m : ℕ
u : Rˣ
h : p ∣ Classical.choose hR ^ m * b
ha : ¬Classical.choose hR ^ m * ↑u = 0
hm : ¬m = 0
⊢ p ∣ Classical.choose hR ^ m ∨ p ∣ b
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: case mpr
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 : ↑((of I M) x) = ↑0
n : ℕ
⊢ x ≡ 0 [SMOD I ^ n • ⊤]

Tactic:
simpa using

Goal state after:
case mpr
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 : ↑((of I M) x) = ↑0
n : ℕ
⊢ x ∈ I ^ n • ⊤
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:
simpa using

Goal state after:
𝒪 : 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
⊢ ¬a = 0
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: case neg
𝒪 : 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
this : (algebraMap 𝒪 K) a ≠ 0
⊢ ∃ x_1, x * (algebraMap 𝒪 K) ↑x_1.2 = (algebraMap 𝒪 K) x_1.1

Tactic:
← one_div,

Goal state after:
case neg
𝒪 : 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 = 1 / (algebraMap 𝒪 K) a
h0 : ¬a = 0
this : (algebraMap 𝒪 K) a ≠ 0
⊢ ∃ x_1, x * (algebraMap 𝒪 K) ↑x_1.2 = (algebraMap 𝒪 K) x_1.1
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:
simpa using

Goal state after:
𝒪 : 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) a = 1
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: case h
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
a : M
ha : ∀ (n : ℕ), x n ≡ a [SMOD I ^ n • ⊤]
n : ℕ
⊢ ↑((of I M) a) n = ↑u n

Tactic:
simpa using

Goal state after:
case h
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
a : M
ha : ∀ (n : ℕ), x n ≡ a [SMOD I ^ n • ⊤]
n : ℕ
⊢ Submodule.Quotient.mk a = Submodule.Quotient.mk (x n)
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: case refine_2
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
h : ↑x n = 0
⊢ ↑x m ∈ I ^ n • ⊤

Tactic:
simpa using

Goal state after:
case refine_2
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
h : ↑x n = 0
⊢ ↑x m ∈ I ^ n • ⊤
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
r1 : X ≠ 0
⊢ f ∈ ⊥

Tactic:
simpa using

Goal state after:
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
r1 : X ≠ 0
⊢ f = 0
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 = ⊥
p : R
left✝ : Irreducible p
H : ∀ {x : R}, x ≠ 0 → ∃ n, Associated (p ^ n) x
n : ℕ
u : Rˣ
hxI : p ^ n * ↑u ∈ I
hx0 : p ^ n * ↑u ≠ 0
⊢ p ^ n ∈ I

Tactic:
simpa using

Goal state after:
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 = ⊥
p : R
left✝ : Irreducible p
H : ∀ {x : R}, x ≠ 0 → ∃ n, Associated (p ^ n) x
n : ℕ
u : Rˣ
hxI : p ^ n * ↑u ∈ I
hx0 : p ^ n * ↑u ≠ 0
⊢ p ^ n ∈ I
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
h : ∀ (P : Ideal R), P.IsPrime → P.jacobson = P
I : Ideal R
hI : I.IsRadical
x : R
hx : x ∈ I.jacobson
⊢ ∀ ⦃I_1 : Ideal R⦄, I_1 ∈ {J | I ≤ J ∧ J.IsPrime} → x ∈ I_1

Tactic:
intro P hP

Goal state after:
R : Type u_1
inst✝ : CommRing R
h : ∀ (P : Ideal R), P.IsPrime → P.jacobson = P
I : Ideal R
hI : I.IsRadical
x : R
hx : x ∈ I.jacobson
P : Ideal R
hP : P ∈ {J | I ≤ J ∧ J.IsPrime}
⊢ x ∈ P
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), P.IsPrime → P.jacobson = P

Tactic:
intro P hP

Goal state after:
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
⊢ P.jacobson = P