mathlib-initiative/mathlib-tactics huggingface dataset:
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 = ⊤
this : Nontrivial (R ⧸ comap (algebraMap R S) P)
J : Ideal (R ⧸ comap (algebraMap R S) P)
hJ : J ∈ {J | ⊥ ≤ J ∧ J.IsMaximal}
⊢ J.IsMaximal

Tactic:
simpa using

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
hP_top : ¬comap (algebraMap R S) P = ⊤
this : Nontrivial (R ⧸ comap (algebraMap R S) P)
J : Ideal (R ⧸ comap (algebraMap R S) P)
hJ : J ∈ {J | ⊥ ≤ J ∧ J.IsMaximal}
⊢ J.IsMaximal
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
n : ℕ
u : Rˣ
hr : p ^ n * ↑u ∈ I
hr0 : ¬p ^ n * ↑u = 0
⊢ p ^ n ∈ I

Tactic:
simpa using

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
n : ℕ
u : Rˣ
hr : p ^ n * ↑u ∈ I
hr0 : ¬p ^ n * ↑u = 0
⊢ p ^ n ∈ I
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
N : Type u_5
inst✝¹ : AddCommGroup N
inst✝ : Module R N
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ a n • ⊤
m n : ℕ
hle : m ≤ n
x : M
s : ℕ
hf : ∀ {m : ℕ} (x : M), (Submodule.factorPow I N ⋯ ∘ₗ f (m + 1)) x = (f m) x
⊢ (f s) x = (Submodule.factor ⋯) ((f (s + 1)) x)

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
N : Type u_5
inst✝¹ : AddCommGroup N
inst✝ : Module R N
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ a n • ⊤
m n : ℕ
hle : m ≤ n
x : M
s : ℕ
hf : ∀ {m : ℕ} (x : M), (Submodule.factorPow I N ⋯ ∘ₗ f (m + 1)) x = (f m) x
⊢ (f s) x = (Submodule.factor ⋯) ((f (s + 1)) x)
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: case refine_3
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
PID : IsPrincipalIdealRing R
p : R
hp : Irreducible p
I : Ideal R
⊢ (fun P ↦ P ≠ ⊥ ∧ P.IsPrime) (R ∙ Submodule.IsPrincipal.generator I) → R ∙ Submodule.IsPrincipal.generator I = span {p}

Tactic:
rintro ⟨I0, hI⟩

Goal state after:
case refine_3
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
PID : IsPrincipalIdealRing R
p : R
hp : Irreducible p
I : Ideal R
I0 : R ∙ Submodule.IsPrincipal.generator I ≠ ⊥
hI : IsPrime (R ∙ Submodule.IsPrincipal.generator I)
⊢ R ∙ Submodule.IsPrincipal.generator I = span {p}
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
hR : HasUnitMulPowIrreducibleFactorization R
this : UniqueFactorizationMonoid R := HasUnitMulPowIrreducibleFactorization.toUniqueFactorizationMonoid hR
⊢ IsDiscreteValuationRing R

Tactic:
apply of_ufd_of_unique_irreducible _ hR.unique_irreducible

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
hR : HasUnitMulPowIrreducibleFactorization R
this : UniqueFactorizationMonoid R := ⋯
⊢ ∃ p, Irreducible p
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: K : Type u_1
inst✝² : DivisionRing K
Γ₀ : Type u_4
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : Nontrivial Γ₀
v : Valuation K Γ₀
x : K
hx : IsUnit x
⊢ v x ≠ 0

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝² : DivisionRing K
Γ₀ : Type u_4
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : Nontrivial Γ₀
v : Valuation K Γ₀
x : K
hx : IsUnit x
⊢ ¬x = 0
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDiscreteValuationRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
ϖ : R
hϖ : Irreducible ϖ
y : R
hy : y ∈ nonZeroDivisors R
n : ℕ
u : Rˣ
hx : (algebraMap R K) (↑u * ϖ ^ n) / (algebraMap R K) y ≠ 0
⊢ ?m.106 ≠ 0

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDiscreteValuationRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
ϖ : R
hϖ : Irreducible ϖ
y : R
hy : y ∈ nonZeroDivisors R
n : ℕ
u : Rˣ
hx : (algebraMap R K) (↑u * ϖ ^ n) / (algebraMap R K) y ≠ 0
⊢ ¬?m.106 = 0
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDiscreteValuationRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
ϖ : R
hϖ : Irreducible ϖ
n : ℕ
u : Rˣ
m : ℕ
v : Rˣ
hy : ↑v * ϖ ^ m ∈ nonZeroDivisors R
hx : (algebraMap R K) (↑u * ϖ ^ n) / (algebraMap R K) (↑v * ϖ ^ m) ≠ 0
⊢ (algebraMap R K) ϖ ≠ 0

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDiscreteValuationRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
ϖ : R
hϖ : Irreducible ϖ
n : ℕ
u : Rˣ
m : ℕ
v : Rˣ
hy : ↑v * ϖ ^ m ∈ nonZeroDivisors R
hx : (algebraMap R K) (↑u * ϖ ^ n) / (algebraMap R K) (↑v * ϖ ^ m) ≠ 0
⊢ ¬ϖ = 0
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : v (y - x) < v x
this : v (y - x + x) = v x
⊢ v y = v x

Tactic:
simpa using

Goal state after:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : v (y - x) < v x
this : v (y - x + x) = v x
⊢ v y = v x
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: case pos
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
hx : v x = 0
hy : v y = 0
⊢ v (x - y) = v y

Tactic:
simpa using

Goal state after:
case pos
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
hx : v x = 0
hy : v y = 0
⊢ v (x - y) = 0
Module: Mathlib.RingTheory.KrullDimension.Zero

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
tfae_1_to_3 : KrullDimLE 0 R ∧ IsLocalRing R → ∀ (x : R), IsNilpotent x ↔ ¬IsUnit x
H : ∀ (x : R), IsNilpotent x ↔ ¬IsUnit x
e : nilradical R = ⊤
n : ℕ
hn : 1 ^ n ∈ 0
⊢ 1 = 0

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
tfae_1_to_3 : KrullDimLE 0 R ∧ IsLocalRing R → ∀ (x : R), IsNilpotent x ↔ ¬IsUnit x
H : ∀ (x : R), IsNilpotent x ↔ ¬IsUnit x
e : nilradical R = ⊤
n : ℕ
hn : 1 ^ n ∈ 0
⊢ 1 = 0
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x : R
h : v x < v 1
⊢ v (1 + x) = 1

Tactic:
simpa using

Goal state after:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x : R
h : v x < v 1
⊢ v (1 + x) = 1
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x : R
h : v (-x) < v 1
⊢ v (1 + -x) = 1

Tactic:
simpa using

Goal state after:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x : R
h : v (-x) < v 1
⊢ v (1 + -x) = 1
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
ϖ : R
hϖ : Irreducible ϖ
⊢ (addVal R) ϖ = 1

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
ϖ : R
hϖ : Irreducible ϖ
⊢ (addVal R) ϖ = 1
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x y : R
h : (addVal R) x = (addVal R) y
hx : x = 0
⊢ Associated x y

pp: case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x y : R
h : (addVal R) x = (addVal R) y
hx : ¬x = 0
⊢ Associated x y

Tactic:
· simp_all only [AddValuation.map_zero]
      rw [addVal_eq_top_iff.mp h.symm]

Goal state after:
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x y : R
h : (addVal R) x = (addVal R) y
hx : ¬x = 0
⊢ Associated x y
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: case pos
K : Type u_1
F : Type u_2
R : Type u_3
inst✝² : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x✝ y✝ x y : R
h : v x ≠ 0
H : ¬v (x + y) = 0
hy : v y = 0
⊢ v (x + y) ≤ v x ∨ ↑⟨Units.mk0 (v (x + y)) ⋯, ⋯⟩ ≤ if h : v y = 0 then 0 else ↑⟨Units.mk0 (v y) ⋯, ⋯⟩

Tactic:
simpa using

Goal state after:
case pos
K : Type u_1
F : Type u_2
R : Type u_3
inst✝² : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x✝ y✝ x y : R
h : v x ≠ 0
H : ¬v (x + y) = 0
hy : v y = 0
⊢ v (x + y) ≤ v x
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: case pos
K : Type u_1
F : Type u_2
R : Type u_3
inst✝² : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x✝ y✝ x y : R
h : v y ≠ 0
H : ¬v (x + y) = 0
hx : v x = 0
⊢ (↑⟨Units.mk0 (v (x + y)) ⋯, ⋯⟩ ≤ if h : v x = 0 then 0 else ↑⟨Units.mk0 (v x) ⋯, ⋯⟩) ∨
    Units.mk0 (v (x + y)) ⋯ ≤ Units.mk0 (v y) ⋯

Tactic:
simpa using

Goal state after:
case pos
K : Type u_1
F : Type u_2
R : Type u_3
inst✝² : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x✝ y✝ x y : R
h : v y ≠ 0
H : ¬v (x + y) = 0
hx : v x = 0
⊢ v (x + y) ≤ v y
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: case refine_1.inl.refine_1
R : Type u_1
inst✝⁶ : CommRing R
Rₘ : Type u_3
Sₘ : Type u_4
inst✝⁵ : CommRing Rₘ
inst✝⁴ : CommRing Sₘ
P : Ideal R[X]
pX : R[X]
hpX : pX ∈ P
inst✝³ : Algebra (R ⧸ comap C P) Rₘ
inst✝² : IsLocalization.Away (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff Rₘ
inst✝¹ : Algebra (R[X] ⧸ P) Sₘ
inst✝ :
  IsLocalization
    (Submonoid.map (quotientMap P C ⋯) (Submonoid.powers (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff)) Sₘ
P' : Ideal R := comap C P
M : Submonoid (R ⧸ P') := Submonoid.powers (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff
M' : Submonoid (R[X] ⧸ P) :=
  Submonoid.map (quotientMap P C ⋯) (Submonoid.powers (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff)
φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯
φ' : Rₘ →+* Sₘ := IsLocalization.map Sₘ φ ⋯
hφ' : φ.comp (Ideal.Quotient.mk P') = (Ideal.Quotient.mk P).comp C
p✝ : Sₘ
p' q : R[X] ⧸ P
hq : q ∈ M'
hp : p✝ * (algebraMap (R[X] ⧸ P) Sₘ) q = (algebraMap (R[X] ⧸ P) Sₘ) p'
p : R[X]
hy : p = X
⊢ (Ideal.Quotient.mk P) (eval₂ C X pX) = 0

Tactic:
Quotient.eq_zero_iff_mem,

Goal state after:
case refine_1.inl.refine_1
R : Type u_1
inst✝⁶ : CommRing R
Rₘ : Type u_3
Sₘ : Type u_4
inst✝⁵ : CommRing Rₘ
inst✝⁴ : CommRing Sₘ
P : Ideal R[X]
pX : R[X]
hpX : pX ∈ P
inst✝³ : Algebra (R ⧸ comap C P) Rₘ
inst✝² : IsLocalization.Away (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff Rₘ
inst✝¹ : Algebra (R[X] ⧸ P) Sₘ
inst✝ :
  IsLocalization
    (Submonoid.map (quotientMap P C ⋯) (Submonoid.powers (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff)) Sₘ
P' : Ideal R := comap C P
M : Submonoid (R ⧸ P') := Submonoid.powers (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff
M' : Submonoid (R[X] ⧸ P) :=
  Submonoid.map (quotientMap P C ⋯) (Submonoid.powers (map (Ideal.Quotient.mk (comap C P)) pX).leadingCoeff)
φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯
φ' : Rₘ →+* Sₘ := IsLocalization.map Sₘ φ ⋯
hφ' : φ.comp (Ideal.Quotient.mk P') = (Ideal.Quotient.mk P).comp C
p✝ : Sₘ
p' q : R[X] ⧸ P
hq : q ∈ M'
hp : p✝ * (algebraMap (R[X] ⧸ P) Sₘ) q = (algebraMap (R[X] ⧸ P) Sₘ) p'
p : R[X]
hy : p = X
⊢ eval₂ C X pX ∈ P
Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE

Goal state before:
pp: case a
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
I : Ideal R
hI : I ≠ ⊥
h : ¬IsField R
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝ : x ≠ 0
hx' : Irreducible x
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
this : ∃ n, x ^ n ∈ I
⊢ maximalIdeal R ^ Nat.find this ≤ I

Tactic:
rw [hx, Ideal.span_singleton_pow, Ideal.span_le, Set.singleton_subset_iff]
    exact Nat.find_spec this

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

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ : (ofClass v).ValueGroup₀ˣ
u : ↥(ofClass v).valueGroup := WithZero.unzero ⋯
hu_def : u = WithZero.unzero ⋯
a : R
ha : (ofClass v) a ≠ 0
x : R
hax : (ofClass v) a * ↑↑u = (ofClass v) x
hx : 0 < v x
⊢ v.restrict a ≠ 0

Tactic:
simpa using

Goal state after:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ : (ofClass v).ValueGroup₀ˣ
u : ↥(ofClass v).valueGroup := WithZero.unzero ⋯
hu_def : u = WithZero.unzero ⋯
a : R
ha : (ofClass v) a ≠ 0
x : R
hax : (ofClass v) a * ↑↑u = (ofClass v) x
hx : 0 < v x
⊢ ¬v a = 0
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: K : Type u_7
inst✝¹ : DivisionRing K
Γ₀ : Type u_8
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
h : v.IsNontrivial
⊢ ∃ x, x ≠ 0 ∧ v x < 1

Tactic:
simpa using

Goal state after:
K : Type u_7
inst✝¹ : DivisionRing K
Γ₀ : Type u_8
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
h : v.IsNontrivial
⊢ ∃ x, ¬x = 0 ∧ v x < 1
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: K : Type u_7
inst✝¹ : DivisionRing K
Γ₀ : Type u_8
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
h : v.IsNontrivial
⊢ ∃ x, 1 < v x

Tactic:
simpa using

Goal state after:
K : Type u_7
inst✝¹ : DivisionRing K
Γ₀ : Type u_8
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
h : v.IsNontrivial
⊢ ∃ x, 1 < v x
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v₁ : Valuation R Γ₀
v₂ : Valuation R Γ'₀
h : v₁.IsEquiv v₂
r s : R
⊢ v₁ r = v₁ s ↔ v₂ r = v₂ s

Tactic:
simpa using

Goal state after:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v₁ : Valuation R Γ₀
v₂ : Valuation R Γ'₀
h : v₁.IsEquiv v₂
r s : R
⊢ v₁ r ≤ v₁ s ∧ v₁ s ≤ v₁ r ↔ v₂ r ≤ v₂ s ∧ v₂ s ≤ v₂ r
Module: Mathlib.RingTheory.Flat.Tensor

Goal state before:
pp: R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ Flat R M ↔ ∀ (I : Ideal R), Function.Injective ⇑(lTensor M (Submodule.subtype I))

Tactic:
simpa using

Goal state after:
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ Flat R M ↔ ∀ (I : Ideal R), Function.Injective ⇑(rTensor M (Submodule.subtype I))
Module: Mathlib.RingTheory.Flat.Tensor

Goal state before:
pp: R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ Flat R M ↔ ∀ ⦃I : Ideal R⦄, I.FG → Function.Injective ⇑(lTensor M (Submodule.subtype I))

Tactic:
simpa using

Goal state after:
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ Flat R M ↔ ∀ ⦃I : Ideal R⦄, I.FG → Function.Injective ⇑(rTensor M (Submodule.subtype I))
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst✝¹ : IsJacobsonRing R
inst✝ : Nontrivial R
hP' : ∀ (x : R), C x ∈ P → x = 0
P' : Ideal R := comap C P
hP'_prime : P'.IsPrime
m : R[X]
hmem_P : m ∈ P
hm : ⟨m, hmem_P⟩ ≠ 0
⊢ m ≠ 0

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝² : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst✝¹ : IsJacobsonRing R
inst✝ : Nontrivial R
hP' : ∀ (x : R), C x ∈ P → x = 0
P' : Ideal R := comap C P
hP'_prime : P'.IsPrime
m : R[X]
hmem_P : m ∈ P
hm : ⟨m, hmem_P⟩ ≠ 0
⊢ ¬m = 0
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst✝¹ : IsJacobsonRing R
inst✝ : Nontrivial R
hP' : ∀ (x : R), C x ∈ P → x = 0
P' : Ideal R := comap C P
hP'_prime : P'.IsPrime
m : R[X]
hmem_P : m ∈ P
hm : ⟨m, hmem_P⟩ ≠ 0
hm' : m ≠ 0
φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯
a : R ⧸ P' := (map (Ideal.Quotient.mk P') m).leadingCoeff
M : Submonoid (R ⧸ P') := Submonoid.powers a
hp0' : a = 0
x : R
hx : (Ideal.Quotient.mk (comap C P)) x = 0
⊢ x = 0

Tactic:
Quotient.eq_zero_iff_mem,

Goal state after:
R : Type u_1
inst✝² : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst✝¹ : IsJacobsonRing R
inst✝ : Nontrivial R
hP' : ∀ (x : R), C x ∈ P → x = 0
P' : Ideal R := comap C P
hP'_prime : P'.IsPrime
m : R[X]
hmem_P : m ∈ P
hm : ⟨m, hmem_P⟩ ≠ 0
hm' : m ≠ 0
φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯
a : R ⧸ P' := (map (Ideal.Quotient.mk P') m).leadingCoeff
M : Submonoid (R ⧸ P') := Submonoid.powers a
hp0' : a = 0
x : R
hx : x ∈ comap C P
⊢ x = 0
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst✝¹ : IsJacobsonRing R
inst✝ : Nontrivial R
hP' : ∀ (x : R), C x ∈ P → x = 0
P' : Ideal R := comap C P
hP'_prime : P'.IsPrime
m : R[X]
hmem_P : m ∈ P
hm : ⟨m, hmem_P⟩ ≠ 0
hm' : m ≠ 0
φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯
a : R ⧸ P' := (map (Ideal.Quotient.mk P') m).leadingCoeff
M : Submonoid (R ⧸ P') := Submonoid.powers a
hp0' : a = 0
⊢ map (Ideal.Quotient.mk (comap C P)) m = map (Ideal.Quotient.mk (comap C P)) 0

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝² : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst✝¹ : IsJacobsonRing R
inst✝ : Nontrivial R
hP' : ∀ (x : R), C x ∈ P → x = 0
P' : Ideal R := comap C P
hP'_prime : P'.IsPrime
m : R[X]
hmem_P : m ∈ P
hm : ⟨m, hmem_P⟩ ≠ 0
hm' : m ≠ 0
φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯
a : R ⧸ P' := (map (Ideal.Quotient.mk P') m).leadingCoeff
M : Submonoid (R ⧸ P') := Submonoid.powers a
hp0' : a = 0
⊢ map (Ideal.Quotient.mk (comap C P)) m = 0
Module: Mathlib.RingTheory.Flat.TorsionFree

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Flat R M
m : M
r : R
hr : r ∈ R⁰
h : ⟨r, hr⟩ • m = 0
⊢ (fun x ↦ r • x) m = (fun x ↦ r • x) 0

Tactic:
simpa using

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Flat R M
m : M
r : R
hr : r ∈ R⁰
h : ⟨r, hr⟩ • m = 0
⊢ r • m = 0
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst✝ : IsJacobsonRing R
P' : Ideal R := comap C P
this✝ : P'.IsPrime
f : R[X] →+* (R ⧸ P')[X] := mapRingHom (Ideal.Quotient.mk P')
hf : Function.Surjective ⇑f
hPJ : P = comap f (Ideal.map f P)
this : (Ideal.map (mapRingHom (Ideal.Quotient.mk (comap C P))) P).IsMaximal
z : R
hx : C ((Ideal.Quotient.mk P') z) ∈ Ideal.map (mapRingHom (Ideal.Quotient.mk (comap C P))) P
⊢ (Ideal.Quotient.mk P') z = 0

Tactic:
Quotient.eq_zero_iff_mem,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst✝ : IsJacobsonRing R
P' : Ideal R := comap C P
this✝ : P'.IsPrime
f : R[X] →+* (R ⧸ P')[X] := mapRingHom (Ideal.Quotient.mk P')
hf : Function.Surjective ⇑f
hPJ : P = comap f (Ideal.map f P)
this : (Ideal.map (mapRingHom (Ideal.Quotient.mk (comap C P))) P).IsMaximal
z : R
hx : C ((Ideal.Quotient.mk P') z) ∈ Ideal.map (mapRingHom (Ideal.Quotient.mk (comap C P))) P
⊢ z ∈ P'
Module: Mathlib.RingTheory.Flat.TorsionFree

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
h✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], ValuationRing (Localization P.primeCompl)
h : torsion R M = ⊥
⊢ ∀ (P : Ideal R) [inst : P.IsMaximal], Flat R (LocalizedModule P.primeCompl M)

Tactic:
intro P hP

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
h✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], ValuationRing (Localization P.primeCompl)
h : torsion R M = ⊥
P : Ideal R
hP : P.IsMaximal
⊢ Flat R (LocalizedModule P.primeCompl M)
Module: Mathlib.LinearAlgebra.RootSystem.BaseChange

Goal state before:
pp: ι : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹² : Field L
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : AddCommGroup N
inst✝⁹ : Module L M
inst✝⁸ : Module L N
P : RootPairing ι L M N
K : Type u_5
inst✝⁷ : Field K
inst✝⁶ : Algebra K L
inst✝⁵ : Module K M
inst✝⁴ : Module K N
inst✝³ : IsScalarTower K L M
inst✝² : IsScalarTower K L N
inst✝¹ : P.IsBalanced
inst✝ : P.IsValuedIn K
⊢ P.IsPerfectCompl (span L ↑(span K (range ⇑P.root)).subtype.range) (span L ↑(span K (range ⇑P.coroot)).subtype.range)

Tactic:
simpa using

Goal state after:
ι : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹² : Field L
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : AddCommGroup N
inst✝⁹ : Module L M
inst✝⁸ : Module L N
P : RootPairing ι L M N
K : Type u_5
inst✝⁷ : Field K
inst✝⁶ : Algebra K L
inst✝⁵ : Module K M
inst✝⁴ : Module K N
inst✝³ : IsScalarTower K L M
inst✝² : IsScalarTower K L N
inst✝¹ : P.IsBalanced
inst✝ : P.IsValuedIn K
⊢ P.IsPerfectCompl (span L (range ⇑P.root)) (span L (range ⇑P.coroot))
Module: Mathlib.LinearAlgebra.RootSystem.BaseChange

Goal state before:
pp: ι : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹² : Field L
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : AddCommGroup N
inst✝⁹ : Module L M
inst✝⁸ : Module L N
P : RootPairing ι L M N
K : Type u_5
inst✝⁷ : Field K
inst✝⁶ : Algebra K L
inst✝⁵ : Module K M
inst✝⁴ : Module K N
inst✝³ : IsScalarTower K L M
inst✝² : IsScalarTower K L N
inst✝¹ : P.IsBalanced
inst✝ : P.IsValuedIn K
i j : ι
h : (fun i ↦ ⟨P.root i, ⋯⟩) i = (fun i ↦ ⟨P.root i, ⋯⟩) j
⊢ i = j

Tactic:
simpa using

Goal state after:
ι : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹² : Field L
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : AddCommGroup N
inst✝⁹ : Module L M
inst✝⁸ : Module L N
P : RootPairing ι L M N
K : Type u_5
inst✝⁷ : Field K
inst✝⁶ : Algebra K L
inst✝⁵ : Module K M
inst✝⁴ : Module K N
inst✝³ : IsScalarTower K L M
inst✝² : IsScalarTower K L N
inst✝¹ : P.IsBalanced
inst✝ : P.IsValuedIn K
i j : ι
h : (fun i ↦ ⟨P.root i, ⋯⟩) i = (fun i ↦ ⟨P.root i, ⋯⟩) j
⊢ i = j