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

Goal state before:
pp: case pos
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' := ⋯ }
⊢ length R M = length R N + length R P

Tactic:
let t' : CompositionSeries (Submodule R M) :=
        t.map ⟨Submodule.map f, Submodule.map_covBy_of_injective hf⟩

Goal state after:
case pos
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' := ⋯ }
⊢ length R M = length R N + length R P
Module: Mathlib.RingTheory.Bezout

Goal state before:
pp: R : Type u
inst✝ : CommRing R
⊢ IsBezout R ↔ ∀ (x y : R), Submodule.IsPrincipal (Ideal.span {x, y})

Tactic:
constructor

Goal state after:
case mp
R : Type u
inst✝ : CommRing R
⊢ IsBezout R → ∀ (x y : R), Submodule.IsPrincipal (Ideal.span {x, y})

case mpr
R : Type u
inst✝ : CommRing R
⊢ (∀ (x y : R), Submodule.IsPrincipal (Ideal.span {x, y})) → IsBezout R
Module: Mathlib.RingTheory.Bezout

Goal state before:
pp: case mpr
R : Type u
inst✝ : CommRing R
H : ∀ (x y : R), Submodule.IsPrincipal (Ideal.span {x, y})
⊢ IsBezout R

Tactic:
constructor

Goal state after:
case mpr
R : Type u
inst✝ : CommRing R
H : ∀ (x y : R), Submodule.IsPrincipal (Ideal.span {x, y})
⊢ ∀ (I : Ideal R), I.FG → Submodule.IsPrincipal I
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
x y : ValueGroup A K
a b : K
c d : Aˣ
⊢ (∃ c_1, c_1 • (fun m ↦ m • b) d = (fun m ↦ m • a) c) = ∃ c, c • b = a

Tactic:
ext

Goal state after:
A : Type u
inst✝² : CommRing A
K : Type v
inst✝¹ : Field K
inst✝ : Algebra A K
x y : ValueGroup A K
a b : K
c d : Aˣ
⊢ (∃ c_1, c_1 • (fun m ↦ m • b) d = (fun m ↦ m • a) c) ↔ ∃ c, c • b = a
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
x y : ValueGroup A K
a b : K
c d : Aˣ
⊢ (∃ c_1, c_1 • (fun m ↦ m • b) d = (fun m ↦ m • a) c) ↔ ∃ c, c • b = a

Tactic:
constructor

Goal state after:
case mp
A : Type u
inst✝² : CommRing A
K : Type v
inst✝¹ : Field K
inst✝ : Algebra A K
x y : ValueGroup A K
a b : K
c d : Aˣ
⊢ (∃ c_1, c_1 • (fun m ↦ m • b) d = (fun m ↦ m • a) c) → ∃ c, c • b = a

case mpr
A : Type u
inst✝² : CommRing A
K : Type v
inst✝¹ : Field K
inst✝ : Algebra A K
x y : ValueGroup A K
a b : K
c d : Aˣ
⊢ (∃ c, c • b = a) → ∃ c_1, c_1 • (fun m ↦ m • b) d = (fun m ↦ m • a) c
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: case mp
A : Type u
inst✝² : CommRing A
K : Type v
inst✝¹ : Field K
inst✝ : Algebra A K
x y : ValueGroup A K
a b : K
c d : Aˣ
e : A
he : e • (fun m ↦ m • b) d = (fun m ↦ m • a) c
⊢ ∃ c, c • b = a

Tactic:
use (c⁻¹ : Aˣ) * e * d

Goal state after:
case h
A : Type u
inst✝² : CommRing A
K : Type v
inst✝¹ : Field K
inst✝ : Algebra A K
x y : ValueGroup A K
a b : K
c d : Aˣ
e : A
he : e • (fun m ↦ m • b) d = (fun m ↦ m • a) c
⊢ (↑c⁻¹ * e * ↑d) • b = a
Module: Mathlib.RingTheory.Valuation.Integers

Goal state before:
pp: R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : v.Integers O
⊢ Nontrivial O ↔ Nontrivial R

Tactic:
constructor

Goal state after:
case mp
R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : v.Integers O
⊢ Nontrivial O → Nontrivial R

case mpr
R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : v.Integers O
⊢ Nontrivial R → Nontrivial O
Module: Mathlib.RingTheory.Valuation.Integers

Goal state before:
pp: case inr
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
x : O
hx : x ≠ 0
⊢ ↑(Ideal.span {x}) = {y | v ((algebraMap O F) y) ≤ v ((algebraMap O F) x)}

Tactic:
ext

Goal state after:
case inr
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
x : O
hx : x ≠ 0
x✝ : O
⊢ x✝ ∈ ↑(Ideal.span {x}) ↔ x✝ ∈ {y | v ((algebraMap O F) y) ≤ v ((algebraMap O F) x)}
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:
constructor

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

case mpr
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, IsGreatest (⇑v ∘ ⇑(algebraMap O F) '' ↑I) x) → Submodule.IsPrincipal I
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, IsGreatest (⇑v ∘ ⇑(algebraMap O F) '' ↑I) x) ↔ ∃ x, ↑I = {y | v ((algebraMap O F) y) ≤ v ((algebraMap O F) x)}

Tactic:
constructor

Goal state after:
case mp
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, IsGreatest (⇑v ∘ ⇑(algebraMap O F) '' ↑I) x) → ∃ x, ↑I = {y | v ((algebraMap O F) y) ≤ v ((algebraMap O F) x)}

case mpr
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, ↑I = {y | v ((algebraMap O F) y) ≤ v ((algebraMap O F) x)}) → ∃ x, IsGreatest (⇑v ∘ ⇑(algebraMap O F) '' ↑I) x
Module: Mathlib.RingTheory.Valuation.Integers

Goal state before:
pp: case mp
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
a : O
ha : a ∈ I
hx : IsGreatest (⇑v ∘ ⇑(algebraMap O F) '' ↑I) ((⇑v ∘ ⇑(algebraMap O F)) a)
b : O
⊢ b ∈ I ↔ v ((algebraMap O F) b) ≤ v ((algebraMap O F) a)

Tactic:
constructor

Goal state after:
case mp.mp
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
a : O
ha : a ∈ I
hx : IsGreatest (⇑v ∘ ⇑(algebraMap O F) '' ↑I) ((⇑v ∘ ⇑(algebraMap O F)) a)
b : O
⊢ b ∈ I → v ((algebraMap O F) b) ≤ v ((algebraMap O F) a)

case mp.mpr
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
a : O
ha : a ∈ I
hx : IsGreatest (⇑v ∘ ⇑(algebraMap O F) '' ↑I) ((⇑v ∘ ⇑(algebraMap O F)) a)
b : O
⊢ v ((algebraMap O F) b) ≤ v ((algebraMap O F) a) → b ∈ I
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:
constructor

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

case mpr
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
⊢ (∃ a, (algebraMap A K) a = x) → x ∈ (valuation A K).integer
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:
constructor

Goal state after:
case left
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.Injective
    ⇑(have this := { toFun := fun a ↦ ⟨(algebraMap A K) a, ⋯⟩, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ };
      this)

case right
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.Surjective
    ⇑(have this := { toFun := fun a ↦ ⟨(algebraMap A K) a, ⋯⟩, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ };
      this)
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:
ext

Goal state after:
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 ↔ x✝ ∈ (algebraMap A K).range
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:
constructor

Goal state after:
A : Type u
inst✝² : CommRing A
inst✝¹ : Nontrivial A
inst✝ : PreValuationRing A
⊢ ∀ (a b : Ideal A), a ≤ b ∨ b ≤ a
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:
ext

Goal state after:
Γ₀ : Type v
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst✝ : Field K
v : Valuation K Γ₀
x✝ : K
⊢ x✝ ∈ v.leSubmodule 0 ↔ x✝ ∈ ⊥
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:
constructor

Goal state after:
case mp
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⁻¹

case mpr
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
⊢ (∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹) → ValuationRing R
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: case mpr
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⁻¹
⊢ PreValuationRing R

Tactic:
constructor

Goal state after:
case mpr
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), ∃ c, a * c = b ∨ b * c = a
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:
ext

Goal state after:
Γ₀ : Type v
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst✝ : Field K
v : Valuation K Γ₀
x✝ : ↥v.integer
⊢ x✝ ∈ v.leIdeal 0 ↔ x✝ ∈ ⊥
Module: Mathlib.RingTheory.Valuation.Integers

Goal state before:
pp: Γ₀ : Type v
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst✝ : Field K
v : Valuation K Γ₀
γ : Γ₀
x : K
⊢ (∃ y, v ↑y ≤ γ ∧ (algebraMap (↥v.integer) K) y = x) ↔ v x ≤ min 1 γ

Tactic:
constructor

Goal state after:
case mp
Γ₀ : Type v
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst✝ : Field K
v : Valuation K Γ₀
γ : Γ₀
x : K
⊢ (∃ y, v ↑y ≤ γ ∧ (algebraMap (↥v.integer) K) y = x) → v x ≤ min 1 γ

case mpr
Γ₀ : Type v
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst✝ : Field K
v : Valuation K Γ₀
γ : Γ₀
x : K
⊢ v x ≤ min 1 γ → ∃ y, v ↑y ≤ γ ∧ (algebraMap (↥v.integer) K) y = x
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:
ext

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
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
n✝ : ℕ
⊢ ↑((s • t) • f) n✝ = ↑(s • t • f) 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
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:
ext

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
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
n✝ : ℕ
⊢ ↑(s • t • f) n✝ = ↑(t • s • f) 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
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:
ext

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
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
n✝ : ℕ
⊢ ↑(MulOpposite.op s • f) n✝ = ↑(s • f) n✝
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:
constructor

Goal state after:
case mp
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ IsDiscreteValuationRing R → IsPrincipalIdealRing R ∧ ∃! P, P ≠ ⊥ ∧ P.IsPrime

case mpr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ (IsPrincipalIdealRing R ∧ ∃! P, P ≠ ⊥ ∧ P.IsPrime) → IsDiscreteValuationRing R
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: case mp
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : IsDiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toIsLocalRing✝ : IsLocalRing R
Rlocal : maximalIdeal R ≠ ⊥
⊢ IsPrincipalIdealRing R ∧ ∃! P, P ≠ ⊥ ∧ P.IsPrime

Tactic:
constructor

Goal state after:
case mp.left
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : IsDiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toIsLocalRing✝ : IsLocalRing R
Rlocal : maximalIdeal R ≠ ⊥
⊢ IsPrincipalIdealRing R

case mp.right
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : IsDiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toIsLocalRing✝ : IsLocalRing R
Rlocal : maximalIdeal R ≠ ⊥
⊢ ∃! P, P ≠ ⊥ ∧ P.IsPrime
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: case h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : IsDiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toIsLocalRing✝ : IsLocalRing R
Rlocal : maximalIdeal R ≠ ⊥
⊢ (fun P ↦ P ≠ ⊥ ∧ P.IsPrime) (maximalIdeal R) ∧ ∀ (y : Ideal R), (fun P ↦ P ≠ ⊥ ∧ P.IsPrime) y → y = maximalIdeal R

Tactic:
constructor

Goal state after:
case h.left
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : IsDiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toIsLocalRing✝ : IsLocalRing R
Rlocal : maximalIdeal R ≠ ⊥
⊢ (fun P ↦ P ≠ ⊥ ∧ P.IsPrime) (maximalIdeal R)

case h.right
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : IsDiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toIsLocalRing✝ : IsLocalRing R
Rlocal : maximalIdeal R ≠ ⊥
⊢ ∀ (y : Ideal R), (fun P ↦ P ≠ ⊥ ∧ P.IsPrime) y → y = maximalIdeal R
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:
constructor

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
f : ℕ → M
⊢ IsAdicCauchy I M f → ∀ (n : ℕ), f n ≡ f (n + 1) [SMOD I ^ n • ⊤]

case mpr
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → M
⊢ (∀ (n : ℕ), f n ≡ f (n + 1) [SMOD I ^ n • ⊤]) → IsAdicCauchy I M f
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

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

Tactic:
constructor

Goal state after:
case h.left
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsCancelMulZero R
hR : HasUnitMulPowIrreducibleFactorization R
p : R := ⋯
spec : Irreducible (Classical.choose hR) ∧ ∀ {x : R}, x ≠ 0 → ∃ n, Associated (Classical.choose hR ^ n) x := ⋯
x : R
hx : x ≠ 0
⊢ ∀ b ∈ Multiset.replicate (Classical.choose ⋯) p, Prime b

case h.right
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsCancelMulZero R
hR : HasUnitMulPowIrreducibleFactorization R
p : R := ⋯
spec : Irreducible (Classical.choose hR) ∧ ∀ {x : R}, x ≠ 0 → ∃ n, Associated (Classical.choose hR ^ n) x := ⋯
x : R
hx : x ≠ 0
⊢ Associated (Multiset.replicate (Classical.choose ⋯) p).prod 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
⊢ Function.Injective ⇑(of I M) ↔ IsHausdorff I M

Tactic:
constructor

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
⊢ Function.Injective ⇑(of I M) → IsHausdorff I M

case mpr
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ IsHausdorff I M → Function.Injective ⇑(of I M)
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:
constructor

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
⊢ Function.Surjective ⇑(of I M) → IsPrecomplete I M

case mpr
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ IsPrecomplete I M → Function.Surjective ⇑(of I M)
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 𝒪
this : IsDomain 𝒪
⊢ PreValuationRing 𝒪

Tactic:
constructor

Goal state after:
𝒪 : Type u
K : Type v
Γ : Type w
inst✝³ : CommRing 𝒪
inst✝² : Field K
inst✝¹ : Algebra 𝒪 K
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
hh : v.Integers 𝒪
this : IsDomain 𝒪
⊢ ∀ (a b : 𝒪), ∃ c, a * c = b ∨ b * c = a
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
⊢ IsPrincipalIdealRing R

Tactic:
constructor

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
⊢ ∀ (S : Ideal R), Submodule.IsPrincipal S
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: case neg
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
ex : ∃ n, p ^ n ∈ I
⊢ Submodule.IsPrincipal I

Tactic:
constructor

Goal state after:
case neg
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
ex : ∃ n, p ^ n ∈ I
⊢ ∃ a, I = R ∙ a