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

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

Tactic:
simp

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

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

Tactic:
simp

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 g : ℕ → M
⊢ f ∈ {f | IsAdicCauchy I M f} → g ∈ {f | IsAdicCauchy I M f} → f + g ∈ {f | IsAdicCauchy I M f}

Tactic:
hf

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
f g : ℕ → M
hf : f ∈ {f | IsAdicCauchy I M f}
⊢ g ∈ {f | IsAdicCauchy I M f} → f + g ∈ {f | IsAdicCauchy I M f}
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
r : R
f : ℕ → M
⊢ f ∈ {f | IsAdicCauchy I M f} → r • f ∈ {f | IsAdicCauchy I M f}

Tactic:
hf

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
r : R
f : ℕ → M
hf : f ∈ {f | IsAdicCauchy I M f}
⊢ r • f ∈ {f | IsAdicCauchy I M f}
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

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

Tactic:
simp

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

Goal state before:
pp: case inr
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : ValuationRing R
x y : R
h : Ideal.span {y} ≤ Ideal.span {x}
⊢ Submodule.IsPrincipal (max (Ideal.span {x}) (Ideal.span {y}))

Tactic:
rw [sup_eq_left.mpr h]

Goal state after:
case inr
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : ValuationRing R
x y : R
h : Ideal.span {y} ≤ Ideal.span {x}
⊢ Submodule.IsPrincipal (Ideal.span {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
inst✝¹ : IsLocalRing R
inst✝ : IsBezout R
a b g : R
e : Ideal.span {a, b} = Ideal.span {g}
⊢ a ∈ {a, b}

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ a n • ⊤
hf : ∀ {m : ℕ}, Submodule.factorPow I N ⋯ ∘ₗ f (m + 1) = f m
inst✝ : IsAdicComplete I N
n : ℕ
x✝ : M
⊢ ((I ^ a n • ⊤).mkQ ∘ₗ lift I ha f ⋯) x✝ = (f n) x✝

Tactic:
simp

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

Goal state before:
pp: 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✝³ : LinearOrderedCommMonoidWithZero Γ₀
inst✝² : LinearOrderedCommMonoidWithZero Γ'₀
inst✝¹ : LinearOrderedCommMonoidWithZero Γ''₀
v✝ : Valuation R Γ₀
S : Type u_7
inst✝ : Ring S
f : S →+* R
v : Valuation R Γ₀
x y : S
⊢ (⇑v ∘ ⇑f) (x + y) ≤ max ((⇑v ∘ ⇑f) x) ((⇑v ∘ ⇑f) y)

Tactic:
simp

Goal state after:
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✝ x y : R
h : v x ≠ v y
h' : v (x + y) < v x
vyx : v y < v x
⊢ v x = v (x + y - y)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.KrullDimension.Zero

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
I : Ideal R
⊢ Ring.KrullDimLE 0 (R ⧸ I) ↔ ∀ J ∈ I.minimalPrimes, J.IsMaximal

Tactic:
rw [Ring.krullDimLE_zero_iff_forall_minimalPrimes_isMaximal, minimalPrimes_eq_comap,
    Set.forall_mem_image]

Goal state after:
R : Type u_2
inst✝ : CommRing R
I : Ideal R
⊢ (∀ I_1 ∈ minimalPrimes (R ⧸ I), I_1.IsMaximal) ↔
    ∀ ⦃x : Ideal (R ⧸ I)⦄, x ∈ minimalPrimes (R ⧸ I) → (comap (Quotient.mk I) x).IsMaximal
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: 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✝² : LinearOrderedCommMonoidWithZero Γ₀
inst✝¹ : LinearOrderedCommMonoidWithZero Γ'₀
inst✝ : LinearOrderedCommMonoidWithZero Γ''₀
v : Valuation R Γ₀
x y : R
f : Γ₀ ≃*o Γ'₀
x✝ : Valuation R Γ₀
r✝ : R
⊢ (map (MonoidWithZeroHom.ofClass f.symm) ⋯ (map (MonoidWithZeroHom.ofClass f) ⋯ x✝)) r✝ = x✝ r✝

Tactic:
simp

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

Goal state before:
pp: 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✝² : LinearOrderedCommMonoidWithZero Γ₀
inst✝¹ : LinearOrderedCommMonoidWithZero Γ'₀
inst✝ : LinearOrderedCommMonoidWithZero Γ''₀
v : Valuation R Γ₀
x y : R
f : Γ₀ ≃*o Γ'₀
x✝ : Valuation R Γ'₀
r✝ : R
⊢ (map (MonoidWithZeroHom.ofClass f) ⋯ (map (MonoidWithZeroHom.ofClass f.symm) ⋯ x✝)) r✝ = x✝ r✝

Tactic:
simp

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

Goal state before:
pp: K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_4
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x : K
⊢ v x = 1 ↔ v x⁻¹ = 1

Tactic:
simp

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

Goal state before:
pp: case inl
K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_4
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
⊢ v 0 ≤ 1 ∨ v 0⁻¹ < 1

Tactic:
simp

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

Goal state before:
pp: 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 : R
v : Valuation R Γ₀
γ : Γ₀
⊢ 0 ∈ {x | v x ≤ γ}

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
u : Rˣ
ϖ : R
hϖ : Irreducible ϖ
⊢ ↑0 = 0

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
u : Rˣ
ϖ : R
hϖ : Irreducible ϖ
⊢ ↑u = ↑u * ϖ ^ 0

Tactic:
simp

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

Goal state before:
pp: case inl
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
⊢ (addVal R) 0 = 0 ↔ IsUnit 0

Tactic:
simp

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

Goal state before:
pp: case pos.inl
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
⊢ (if h : v (x + y) = 0 then 0 else ↑⟨Units.mk0 (v (x + y)) ⋯, ⋯⟩) ≤ ↑⟨Units.mk0 (v x) ⋯, ⋯⟩ ∨
    (if h : v (x + y) = 0 then 0 else ↑⟨Units.mk0 (v (x + y)) ⋯, ⋯⟩) ≤
      if h : v y = 0 then 0 else ↑⟨Units.mk0 (v y) ⋯, ⋯⟩

pp: case pos.inr
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
⊢ ((if h : v (x + y) = 0 then 0 else ↑⟨Units.mk0 (v (x + y)) ⋯, ⋯⟩) ≤
      if h : v x = 0 then 0 else ↑⟨Units.mk0 (v x) ⋯, ⋯⟩) ∨
    (if h : v (x + y) = 0 then 0 else ↑⟨Units.mk0 (v (x + y)) ⋯, ⋯⟩) ≤ ↑⟨Units.mk0 (v y) ⋯, ⋯⟩

Tactic:
all_goals split_ifs with H

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
⊢ (if h : v (x + y) = 0 then 0 else ↑⟨Units.mk0 (v (x + y)) ⋯, ⋯⟩) ≤ ↑⟨Units.mk0 (v x) ⋯, ⋯⟩ ∨
    (if h : v (x + y) = 0 then 0 else ↑⟨Units.mk0 (v (x + y)) ⋯, ⋯⟩) ≤
      if h : v y = 0 then 0 else ↑⟨Units.mk0 (v y) ⋯, ⋯⟩

case neg
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
⊢ (if h : v (x + y) = 0 then 0 else ↑⟨Units.mk0 (v (x + y)) ⋯, ⋯⟩) ≤ ↑⟨Units.mk0 (v x) ⋯, ⋯⟩ ∨
    (if h : v (x + y) = 0 then 0 else ↑⟨Units.mk0 (v (x + y)) ⋯, ⋯⟩) ≤
      if h : v y = 0 then 0 else ↑⟨Units.mk0 (v y) ⋯, ⋯⟩

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
⊢ ((if h : v (x + y) = 0 then 0 else ↑⟨Units.mk0 (v (x + y)) ⋯, ⋯⟩) ≤
      if h : v x = 0 then 0 else ↑⟨Units.mk0 (v x) ⋯, ⋯⟩) ∨
    (if h : v (x + y) = 0 then 0 else ↑⟨Units.mk0 (v (x + y)) ⋯, ⋯⟩) ≤ ↑⟨Units.mk0 (v y) ⋯, ⋯⟩

case neg
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
⊢ ((if h : v (x + y) = 0 then 0 else ↑⟨Units.mk0 (v (x + y)) ⋯, ⋯⟩) ≤
      if h : v x = 0 then 0 else ↑⟨Units.mk0 (v x) ⋯, ⋯⟩) ∨
    (if h : v (x + y) = 0 then 0 else ↑⟨Units.mk0 (v (x + y)) ⋯, ⋯⟩) ≤ ↑⟨Units.mk0 (v y) ⋯, ⋯⟩
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: case top
R✝ : Type u
inst✝⁵ : CommRing R✝
inst✝⁴ : IsDomain R✝
inst✝³ : IsDiscreteValuationRing R✝
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
⊢ OrderDual.toDual ((addVal R) (generator (ENat.recTopCoe ⊥ (fun n ↦ maximalIdeal R ^ n) ⊤))) = OrderDual.toDual ⊤

Tactic:
simp

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

Goal state before:
pp: R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x : R
⊢ toWithBotNat x ≠ ⊥ ↔ x ≠ 0

Tactic:
simp

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

Goal state before:
pp: case top
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x y : R
hx : x ≠ 0
hy : y ≠ 0
vy : ℕ∞
hvy : (addVal R) y = vy
hvx : (addVal R) x = ⊤
⊢ ⊤ ≤ vy ↔ x ∣ y

Tactic:
rw [addVal_eq_top_iff] at hvx

Goal state after:
case top
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x y : R
hx : x ≠ 0
hy : y ≠ 0
vy : ℕ∞
hvy : (addVal R) y = vy
hvx : x = 0
⊢ ⊤ ≤ vy ↔ x ∣ y
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
g : (ofClass v).ValueGroup₀
⊢ embedding (v.restrict x) < embedding g ↔ v x < embedding g

Tactic:
simp

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 Γ₀
x : R
g : (ofClass v).ValueGroup₀
⊢ embedding (v.restrict x) ≤ embedding g ↔ v x ≤ embedding g

Tactic:
simp

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

Goal state before:
pp: 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 : R
hx : v x ≠ 0
⊢ (ofClass v) 1 ≠ 0

Tactic:
simp

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 Γ₀
x y : R
⊢ embedding (v.restrict x) = embedding (v.restrict y) ↔ v x = v y

Tactic:
simp

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

Goal state before:
pp: case a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDedekindDomain R
ne_bot : ¬maximalIdeal R = ⊥
a : R
ha₁ : a ∈ maximalIdeal R
ha₂ : a ≠ 0
hle : Ideal.span {a} ≤ maximalIdeal R
⊢ maximalIdeal R ≤ sInf {J | Ideal.span {a} ≤ J ∧ J.IsPrime}

Tactic:
refine
        le_sInf fun I hI =>
          (eq_maximalIdeal <| hI.2.isMaximal (fun e => ha₂ ?_)).ge
      rw [← Ideal.span_singleton_eq_bot, eq_bot_iff, ← e]; exact hI.1

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

Goal state before:
pp: K : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst✝⁴ : Field K
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : CommRing O
inst✝¹ : Algebra O K
v : Valuation K Γ₀
hv : v.Integers O
this : IsDomain O := Function.Injective.isDomain (algebraMap O K) hv.hom_inj
inst✝ : IsDiscreteValuationRing O
ϖ : O
h : Irreducible ϖ
n : ℕ
⊢ v ((algebraMap O K) ϖ) ^ n = v ((algebraMap O K) (ϖ ^ n))

Tactic:
simp

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

Goal state before:
pp: 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 : R
v : Valuation R Γ₀
γ : Γ₀ˣ
⊢ 0 ∈ {x | v x < ↑γ}

Tactic:
simp

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

Goal state before:
pp: Γ₀ : Type u_4
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
K : Type u_7
inst✝ : Field K
v : Valuation K Γ₀
x✝ : K
⊢ x✝ ∈ v.leAddSubgroup 0 ↔ x✝ ∈ ⊥

Tactic:
simp

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

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝² : LinearOrderedCommGroupWithZero Γ₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ'₀
inst✝ : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
h : v.IsEquiv w
r s : R
hr : (ofClass v) r ≠ 0
hs : (ofClass v) s ≠ 0
hr' : (ofClass w) r ≠ 0
hs' : (ofClass w) s ≠ 0
⊢ ¬↑(valueGroup.mk (ofClass v) r s hr hs) = 0

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Ideal.IsPrincipal

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ ↑1 = R ∙ 1

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
hR : IsJacobsonRing R
I : Ideal R[X]
hI : I.IsPrime
R' : Subring (R[X] ⧸ I) := ((Ideal.Quotient.mk I).comp C).range
i : R →+* ↥R' := ((Ideal.Quotient.mk I).comp C).rangeRestrict
hi : Function.Surjective ⇑i
f : R[X]
⊢ f ∈ RingHom.ker (mapRingHom i) → f ∈ I

Tactic:
hf

Goal state after:
R : Type u_1
inst✝ : CommRing R
hR : IsJacobsonRing R
I : Ideal R[X]
hI : I.IsPrime
R' : Subring (R[X] ⧸ I) := ((Ideal.Quotient.mk I).comp C).range
i : R →+* ↥R' := ((Ideal.Quotient.mk I).comp C).rangeRestrict
hi : Function.Surjective ⇑i
f : R[X]
hf : f ∈ RingHom.ker (mapRingHom i)
⊢ f ∈ I
Module: Mathlib.RingTheory.Ideal.IsPrincipal

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
hprinc : IsPrincipal I
h : I ≠ ⊥
⊢ (Submodule.subtype I ∘ₗ ↑(isoBaseOfIsPrincipal h)) 1 = ((LinearMap.mul R R) (IsPrincipal.generator I)) 1

Tactic:
simp

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
⊢ KrullDimLE 1 R

pp: case refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
h : ringKrullDim R < 1
⊢ False

Tactic:
· exact krullDimLE_one_iff_of_isPrime_bot.mpr fun I hI hI' ↦ hI'.isMaximal hI

Goal state after:
case refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
h : ringKrullDim R < 1
⊢ False
Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
h : ringKrullDim R < 1
this : KrullDimLE 0 R
⊢ False

Tactic:
exact IsDiscreteValuationRing.not_isField R KrullDimLE.isField_of_isDomain

Goal state after:
Module: Mathlib.RingTheory.Flat.TorsionFree

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
r : R
hr : IsRegular r
inst✝ : Flat R M
h : Function.Injective ⇑(rTensor M (toSpanSingleton R R r))
x✝ : M
⊢ r • x✝ = (↑(TensorProduct.lid R M) ∘ₗ rTensor M (toSpanSingleton R R r) ∘ₗ ↑(TensorProduct.lid R M).symm) x✝

Tactic:
simp

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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst✝ : Nontrivial R
hR : IsJacobsonRing R
hP' : ∀ (x : R), C x ∈ P → x = 0
P' : Ideal R := comap C P
pX : R[X]
hpX : pX ∈ P
hp0 : map (Ideal.Quotient.mk (comap C P)) pX ≠ 0
a : R ⧸ P' := (map (Ideal.Quotient.mk P') pX).leadingCoeff
M : Submonoid (R ⧸ P') := Submonoid.powers a
φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯
hP'_prime : P'.IsPrime
hM : 0 ∉ M
M' : Submonoid (R[X] ⧸ P) := Submonoid.map φ M
⊢ ((algebraMap (R[X] ⧸ P) (Localization M')).comp φ).IsIntegral

Tactic:
suffices RingHom.comp (algebraMap (R[X] ⧸ P) (Localization M')) φ =
      (IsLocalization.map (Localization M') φ M.le_comap_map).comp
        (algebraMap (R ⧸ P') (Localization M)) by
      rw [this]
      refine RingHom.IsIntegral.trans (algebraMap (R ⧸ P') (Localization M))
        (IsLocalization.map (Localization M') φ M.le_comap_map) ?_ ?_
      · exact (algebraMap (R ⧸ P') (Localization M)).isIntegral_of_surjective
          (IsField.localization_map_bijective hM ((Quotient.maximal_ideal_iff_isField_quotient _).mp
            (isMaximal_comap_C_of_isMaximal P hP'))).2
      · -- `convert` here is faster than `exact`, and this proof is near the time limit.
        -- convert isIntegral_isLocalization_polynomial_quotient P pX hpX
        have isloc : IsLocalization M' (Localization M') := by infer_instance
        exact @isIntegral_isLocalization_polynomial_quotient R _
          (Localization M) (Localization M') _ _ P pX hpX _ _ _ isloc
    rw [IsLocalization.map_comp M.le_comap_map]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsJacobsonRing R
S : Type u_2
inst✝ : Field S
f : R[X] →+* S
hf : Function.Surjective ⇑f
⊢ (f.comp C).IsIntegral

Tactic:
have : (RingHom.ker f).IsMaximal := RingHom.ker_isMaximal_of_surjective f hf

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsJacobsonRing R
S : Type u_2
inst✝ : Field S
f : R[X] →+* S
hf : Function.Surjective ⇑f
this : (RingHom.ker f).IsMaximal
⊢ (f.comp C).IsIntegral
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✝¹ : IsBezout R
inst✝ : IsDomain R
htors : IsTorsionFree R M
I : Ideal R
hFG : I.FG
h : I ≠ ⊥
hprinc : Submodule.IsPrincipal I
this : IsPrincipal.generator I ≠ 0
x✝ : M
⊢ (⇑(lift (lsmul R M)) ∘ ⇑(TensorProduct.lid R M).symm.toEquiv) x✝ = id x✝

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.BaseChange

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsRootSystem
⊢ P.IsPerfectCompl (P.rootSpan R) (P.corootSpan R)

Tactic:
simp

Goal state after: