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

Goal state before:
pp: A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
⊢ ∀ (a : ValueGroup A K), 0 * a = 0

Tactic:
by

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

Goal state before:
pp: A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
⊢ ∀ (a : ValueGroup A K), a * 0 = 0

Tactic:
by

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

Goal state before:
pp: A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
⊢ 0⁻¹ = 0

Tactic:
by

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

Goal state before:
pp: A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
⊢ ∀ (a : ValueGroup A K), a ≠ 0 → a * a⁻¹ = 1

Tactic:
by

Goal state after:
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:
by

Goal state after:
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
⊢ Submodule.IsPrincipal I ↔ ∃ x, IsGreatest (⇑v ∘ ⇑(algebraMap O F) '' ↑I) x

Tactic:
by

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

Goal state before:
pp: A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a✝ : ValueGroup A K
a : K
ha : ¬Quot.mk (⇑(MulAction.orbitRel Aˣ K)) a ≤ 0
b✝ : ValueGroup A K
b : K
c✝ : ValueGroup A K
d : A
⊢ d • b = (algebraMap A K) d * b

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✝ : IsHausdorff I M
x y : M
⊢ x = y ↔ ∀ (n : ℕ), x ≡ y [SMOD I ^ n • ⊤]

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
⊢ IsHausdorff (Ideal.map (algebraMap R S) I) M ↔ IsHausdorff I M

Tactic:
by

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

Goal state before:
pp: A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
⊢ ∀ ⦃a : ValueGroup A K⦄, 0 < a → ∀ ⦃b c : ValueGroup A K⦄, b < c → a * b < a * c

Tactic:
by

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

Goal state before:
pp: A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
⊢ ∀ (a : ValueGroup A K), 0 ≤ a

Tactic:
by

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

Goal state before:
pp: A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
⊢ IsBot 0

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
J : Ideal S
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R S M
hIJ : Ideal.map (algebraMap R S) I ≤ J
inst✝ : IsHausdorff J M
⊢ IsHausdorff 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
N : Type u_5
inst✝² : AddCommGroup N
inst✝¹ : Module R N
M : Type u_6
inst✝ : IsHausdorff I N
f g : M → N
h : ∀ (n : ℕ) (m : M), Submodule.Quotient.mk (f m) = Submodule.Quotient.mk (g m)
⊢ f = g

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
I : Ideal R
N : Type u_5
inst✝² : AddCommGroup N
inst✝¹ : Module R N
M : Type u_6
inst✝ : IsHausdorff I N
f g : M → N
a : ℕ → ℕ
ha : StrictMono a
h : ∀ (n : ℕ) (m : M), Submodule.Quotient.mk (f m) = Submodule.Quotient.mk (g m)
⊢ f = g

Tactic:
by

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

Goal state before:
pp: R : Type u_6
S : Type u_7
inst✝¹ : CommRing S
I : Ideal S
inst✝ : IsHausdorff I S
f g : R → S
h : ∀ (n : ℕ) (r : R), (Ideal.Quotient.mk (I ^ n)) (f r) = (Ideal.Quotient.mk (I ^ n)) (g r)
⊢ f = g

Tactic:
by

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

Goal state before:
pp: A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
⊢ ∀ (x y : K), Quotient.mk'' (x + y) ≤ max (Quotient.mk'' x) (Quotient.mk'' y)

Tactic:
by

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

Goal state before:
pp: R : Type u_6
S : Type u_7
inst✝¹ : CommRing S
I : Ideal S
inst✝ : IsHausdorff I S
f g : R → S
a : ℕ → ℕ
ha : StrictMono a
h : ∀ (n : ℕ) (r : R), (Ideal.Quotient.mk (I ^ a n)) (f r) = (Ideal.Quotient.mk (I ^ a n)) (g r)
⊢ f = g

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
⊢ IsPrecomplete (Ideal.map (algebraMap R S) I) M ↔ IsPrecomplete I M

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 : M
hx : ∀ (n : ℕ), x ≡ 0 [SMOD ⊥ ^ n • ⊤]
⊢ x = 0

Tactic:
simpa only [pow_one ⊥, bot_smul, SModEq.bot] using hx 1

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

Goal state before:
pp: A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
x : K
⊢ x ∈ (valuation A K).integer ↔ ∃ a, (algebraMap A K) a = 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
x : M
hx : ∀ (n : ℕ), x ≡ 0 [SMOD ⊥ ^ n • ⊤]
⊢ x = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : IsHausdorff ⊤ M
x y : M
n : ℕ
⊢ x - y ≡ 0 [SMOD ⊤ ^ n • ⊤]

Tactic:
by

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

Goal state before:
pp: A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
x✝¹ x✝ : A
⊢ ⟨(algebraMap A K) (x✝¹ * x✝), ⋯⟩ = ⟨(algebraMap A K) x✝¹, ⋯⟩ * ⟨(algebraMap A K) x✝, ⋯⟩

Tactic:
by

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

Goal state before:
pp: A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
⊢ ⟨(algebraMap A K) 0, ⋯⟩ = 0

Tactic:
by

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

Goal state before:
pp: A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
x✝¹ x✝ : A
⊢ ⟨(algebraMap A K) (x✝¹ + x✝), ⋯⟩ = ⟨(algebraMap A K) x✝¹, ⋯⟩ + ⟨(algebraMap A K) x✝, ⋯⟩

Tactic:
by

Goal state after:
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
⊢ Submodule.IsPrincipal I ↔ ∃ x, ↑I = {y | v ((algebraMap O F) y) ≤ v ((algebraMap O F) x)}

Tactic:
by

Goal state after:
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:
by

Goal state after:
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)
⊢ 0 ∈ ⇑v ∘ ⇑(algebraMap O F) ⁻¹' Iio 1

Tactic:
by

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

Goal state before:
pp: A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
⊢ Function.Bijective
    ⇑(have this := { toFun := fun a ↦ ⟨(algebraMap A K) a, ⋯⟩, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ };
      this)

Tactic:
by

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

Goal state before:
pp: A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
⊢ (valuation A K).integer = (algebraMap A K).range

Tactic:
by

Goal state after:
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)
⊢ ∀ (c : O) {x : O}, x ∈ ⇑v ∘ ⇑(algebraMap O F) ⁻¹' Iio 1 → c • x ∈ ⇑v ∘ ⇑(algebraMap O F) ⁻¹' Iio 1

Tactic:
by

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

Goal state before:
pp: A : Type u
inst✝² : CommRing A
inst✝¹ : Nontrivial A
inst✝ : PreValuationRing A
a : A
⊢ IsUnit a ∨ IsUnit (1 - 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
x✝ : Hausdorffification I M
x : M
hx : ∀ (n : ℕ), Quotient.mk'' x ≡ 0 [SMOD I ^ n • ⊤]
n : ℕ
⊢ x ∈ I ^ n • ⊤

Tactic:
by

Goal state after:
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:
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
h : IsHausdorff I N
f : M →ₗ[R] N
n : ℕ
⊢ Submodule.map f (I ^ n • ⊤) ≤ I ^ n • ⊤

Tactic:
by

Goal state after:
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:
by

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

Goal state before:
pp: A : Type u
inst✝² : CommRing A
inst✝¹ : Nontrivial A
inst✝ : PreValuationRing A
⊢ Std.Total fun x1 x2 ↦ x1 ≤ x2

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
h : IsHausdorff I N
f : M →ₗ[R] N
g : Hausdorffification I M →ₗ[R] N
hg : g ∘ₗ of I M = f
x✝ : Hausdorffification I M
x : M
⊢ g ((of I M) x) = (lift I f) ((of I M) x)

Tactic:
by

Goal state after:
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
⊢ ¬DenselyOrdered ↑(range ⇑v)

Tactic:
by

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

Goal state before:
pp: F : Type u
Γ₀ : Type v
inst✝¹ : Field F
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
x : ↥v.integer
⊢ ¬IsUnit x ↔ v ↑x < 1

Tactic:
by

Goal state after:
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:
by

Goal state after:
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:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semigroup R
⊢ PreValuationRing R ↔ Std.Total fun x1 x2 ↦ x1 ∣ x2

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 Γ₀
⊢ v.leSubmodule 0 = ⊥

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ PreValuationRing R ↔ Std.Total fun x1 x2 ↦ x1 ≤ x2

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : PreValuationRing R
p q : R
hp : Irreducible p
hq : Irreducible q
⊢ Associated p q

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 Γ₀
S : Submodule (↥v.integer) K
x : K
hx : x ∈ S
hx0 : x ≠ 0
y : K
hy : y ∈ v.leSubmodule (v x)
⊢ v (y / x) ≤ 1

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 Γ₀
S : Submodule (↥v.integer) K
x : K
hx : x ∈ S
⊢ v.leSubmodule (v x) ≤ S

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
H : ValuationRing R
x s : R
hy : x * s ∈ nonZeroDivisors R
this : (algebraMap R K) (x * s) ≠ 0
⊢ (algebraMap R K) s * ((algebraMap R K) x / (algebraMap R K) (x * s)) = 1

Tactic:
by

Goal state after:
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:
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
H : ValuationRing R
y : R
hy : y ∈ nonZeroDivisors R
this : (algebraMap R K) y ≠ 0
s : R
⊢ (algebraMap R K) s = (algebraMap R K) (y * s) / (algebraMap R K) y

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
⊢ IsPrecomplete ⊥ M

Tactic:
by

Goal state after:
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
⊢ r • x ∈ ((v.ltAddSubgroup γ).addSubgroupOf v.integer.toAddSubgroup).carrier

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 Γ₀
⊢ v.leIdeal 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
f : ℕ → M
x✝ : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD ⊤ ^ m • ⊤]
n : ℕ
⊢ f n ≡ 0 [SMOD ⊤ ^ n • ⊤]

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
inst✝ : Subsingleton M
f : ℕ → M
x✝ : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]
n : ℕ
⊢ f n ≡ 0 [SMOD I ^ n • ⊤]

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✝ : (n : ℕ) → M ⧸ I ^ n • ⊤
hf : a✝ ∈ {f | ∀ {m n : ℕ} (hmn : m ≤ n), (transitionMap I M hmn) (f n) = f m}
hg : b✝ ∈ {f | ∀ {m n : ℕ} (hmn : m ≤ n), (transitionMap I M hmn) (f n) = f m}
m n : ℕ
hmn : m ≤ n
⊢ (transitionMap I M hmn) ((a✝ + b✝) n) = (a✝ + b✝) m

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
m✝ n✝ : ℕ
hmn : m✝ ≤ n✝
⊢ (transitionMap I M hmn) (0 n✝) = 0 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
⊢ ValuationRing R ↔ ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R 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
c : R
f : (n : ℕ) → M ⧸ I ^ n • ⊤
hf : f ∈ {f | ∀ {m n : ℕ} (hmn : m ≤ n), (transitionMap I M hmn) (f n) = f m}
m n : ℕ
hmn : m ≤ n
⊢ (transitionMap I M hmn) ((c • f) n) = (c • f) m

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
⊢ ∀ {m n : ℕ} (hmn : m ≤ n), (transitionMap I M hmn) (0 n) = 0 m

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 y : AdicCompletion I M
⊢ ∀ {m n : ℕ} (hmn : m ≤ n), (transitionMap I M hmn) ((↑x + ↑y) n) = (↑x + ↑y) m

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
⊢ ∀ {m n : ℕ} (hmn : m ≤ n), (transitionMap I M hmn) ((-↑x) n) = (-↑x) m

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 y : AdicCompletion I M
⊢ ∀ {m n : ℕ} (hmn : m ≤ n), (transitionMap I M hmn) ((↑x - ↑y) n) = (↑x - ↑y) m

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
inst✝² : SMul S R
inst✝¹ : SMul S M
inst✝ : IsScalarTower S R M
r : S
x : AdicCompletion I M
⊢ ∀ {m n : ℕ} (hmn : m ≤ n), (transitionMap I M hmn) ((r • ↑x) n) = (r • ↑x) m

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 Γ₀
γ : Γ₀
⊢ Submodule.map (Algebra.linearMap (↥v.integer) K) (v.leIdeal γ) = v.leSubmodule (min 1 γ)

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
inst✝⁷ : SMul S T
inst✝⁶ : SMul S R
inst✝⁵ : SMul T R
inst✝⁴ : SMul S M
inst✝³ : SMul T M
inst✝² : IsScalarTower S R M
inst✝¹ : IsScalarTower T R M
inst✝ : IsScalarTower S T M
s : S
t : T
f : AdicCompletion I M
⊢ (s • t) • f = s • t • 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
inst✝⁶ : SMul S R
inst✝⁵ : SMul T R
inst✝⁴ : SMul S M
inst✝³ : SMul T M
inst✝² : IsScalarTower S R M
inst✝¹ : IsScalarTower T R M
inst✝ : SMulCommClass S T M
s : S
t : T
f : AdicCompletion I M
⊢ s • t • f = t • s • f

Tactic:
by

Goal state after: