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
x y : ValueGroup A K
⊢ ∀ (a₁ a₂ b₁ b₂ : K),
    (MulAction.orbitRel Aˣ K) a₁ b₁ → (MulAction.orbitRel Aˣ K) a₂ b₂ → (∃ c, c • a₂ = a₁) = ∃ c, c • b₂ = b₁

Tactic:
by
        rintro _ _ a b ⟨c, rfl⟩ ⟨d, rfl⟩; ext
        constructor
        · rintro ⟨e, he⟩; use (c⁻¹ : Aˣ) * e * d
          apply_fun fun t => c⁻¹ • t at he
          simpa [mul_smul] using! he
        · rintro ⟨e, he⟩; dsimp
          use c * e * (d⁻¹ : Aˣ)
          simp_rw [Units.smul_def, ← he, mul_smul]
          rw [← mul_smul _ _ b, Units.inv_mul, one_smul]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
H : ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
a b : R
ha : a = 0
⊢ ∃ c, a * c = b ∨ b * c = a

Tactic:
subst ha; exact ⟨0, Or.inr <| mul_zero b⟩

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

Goal state before:
pp: case neg
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
H : ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
a b : R
ha : (algebraMap R K) a ≠ 0
hb : (algebraMap R K) b ≠ 0
⊢ ∃ c, a * c = b ∨ b * c = a

Tactic:
obtain ⟨c, e⟩ | ⟨c, e⟩ := H (algebraMap R K a / algebraMap R K b)

Goal state after:
case neg.inl
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
H : ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
a b : R
ha : (algebraMap R K) a ≠ 0
hb : (algebraMap R K) b ≠ 0
c : R
e : (algebraMap R K) c = (algebraMap R K) a / (algebraMap R K) b
⊢ ∃ c, a * c = b ∨ b * c = a

case neg.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
H : ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
a b : R
ha : (algebraMap R K) a ≠ 0
hb : (algebraMap R K) b ≠ 0
c : R
e : (algebraMap R K) c = ((algebraMap R K) a / (algebraMap R K) b)⁻¹
⊢ ∃ c, a * c = b ∨ b * c = a
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
ϖ : R
hϖ : ϖ ≠ 0
h : maximalIdeal R = span {ϖ}
⊢ Irreducible ϖ

Tactic:
have h2 : ¬IsUnit ϖ := show ϖ ∈ maximalIdeal R from h.symm ▸ Submodule.mem_span_singleton_self ϖ

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
ϖ : R
hϖ : ϖ ≠ 0
h : maximalIdeal R = span {ϖ}
h2 : ¬IsUnit ϖ
⊢ Irreducible ϖ
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 : ℕ → M}, a ∈ {f | IsAdicCauchy I M f} → b ∈ {f | IsAdicCauchy I M f} → a + b ∈ {f | IsAdicCauchy I M f}

Tactic:
intro f g hf hg m n hmn
    exact SModEq.add (hf hmn) (hg hmn)

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

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

Tactic:
have hq : q ≠ 0 := by
        rintro rfl
        apply hQ1
        simp

Goal state after:
case h.right
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
RDVR : IsDiscreteValuationRing R
toIsPrincipalIdealRing✝ : IsPrincipalIdealRing R
toIsLocalRing✝ : IsLocalRing R
Rlocal : maximalIdeal R ≠ ⊥
q : R
hQ1 : R ∙ q ≠ ⊥
hQ2 : IsPrime (R ∙ q)
hq : q ≠ 0
⊢ R ∙ q = maximalIdeal R
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: 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

Tactic:
intro q

Goal state after:
case h.left
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsCancelMulZero R
hR : HasUnitMulPowIrreducibleFactorization R
p : R := Classical.choose hR
spec : Irreducible (Classical.choose hR) ∧ ∀ {x : R}, x ≠ 0 → ∃ n, Associated (Classical.choose hR ^ n) x :=
  Classical.choose_spec hR
x : R
hx : x ≠ 0
q : R
⊢ q ∈ Multiset.replicate (Classical.choose ⋯) p → Prime q
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
⊢ ValuationRing R

Tactic:
by
  refine iff_dvd_total.mpr ⟨fun a b => ?_⟩
  obtain ⟨g, e : _ = Ideal.span _⟩ := IsBezout.span_pair_isPrincipal a b
  obtain ⟨a, rfl⟩ := Ideal.mem_span_singleton'.mp
      (show a ∈ Ideal.span {g} by rw [← e]; exact Ideal.subset_span (by simp))
  obtain ⟨b, rfl⟩ := Ideal.mem_span_singleton'.mp
      (show b ∈ Ideal.span {g} by rw [← e]; exact Ideal.subset_span (by simp))
  obtain ⟨x, y, e'⟩ := Ideal.mem_span_pair.mp
      (show g ∈ Ideal.span {a * g, b * g} by rw [e]; exact Ideal.subset_span (by simp))
  rcases eq_or_ne g 0 with h | h
  · simp [h]
  have : x * a + y * b = 1 := by
    apply mul_left_injective₀ h; convert! e' using 1 <;> ring
  rcases IsLocalRing.isUnit_or_isUnit_of_add_one this with h' | h' <;> [left; right]
  all_goals exact mul_dvd_mul_right (isUnit_iff_forall_dvd.mp (isUnit_of_mul_isUnit_right h') _) _

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

Goal state before:
pp: case mp
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : Function.Surjective ⇑(of I M)
f : ℕ → M
hmn : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]
u : AdicCompletion I M := ⟨fun n ↦ Submodule.Quotient.mk (f n), ⋯⟩
x : M
hx : (of I M) x = u
n : ℕ
⊢ f n ≡ x [SMOD I ^ n • ⊤]

Tactic:
simp only [SModEq]

Goal state after:
case mp
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : Function.Surjective ⇑(of I M)
f : ℕ → M
hmn : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]
u : AdicCompletion I M := ⟨fun n ↦ Submodule.Quotient.mk (f n), ⋯⟩
x : M
hx : (of I M) x = u
n : ℕ
⊢ Submodule.Quotient.mk (f n) = Submodule.Quotient.mk x
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: case mpr
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ IsPrecomplete I M → Function.Surjective ⇑(of I M)

Tactic:
intro h u

Goal state after:
case mpr
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : IsPrecomplete I M
u : AdicCompletion I M
⊢ ∃ a, (of I M) a = u
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: case refine_1
𝒪 : Type u
K : Type v
inst✝⁴ : CommRing 𝒪
inst✝³ : Field K
inst✝² : Algebra 𝒪 K
inst✝¹ : IsDomain 𝒪
inst✝ : ValuationRing 𝒪
h : IsFractionRing 𝒪 K
x : K
⊢ ∃ a, x = (algebraMap 𝒪 K) a ∨ x⁻¹ = (algebraMap 𝒪 K) a

Tactic:
obtain (⟨a, e⟩ | ⟨a, e⟩) := isInteger_or_isInteger 𝒪 x
    exacts [⟨a, .inl e.symm⟩, ⟨a, .inr e.symm⟩]

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

Tactic:
by_cases hP_top : comap (algebraMap R S) P = ⊤

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

case neg
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 = ⊤
⊢ P.jacobson = P
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
f : ℕ → R := fun n ↦ ∑ i ∈ range n, (x * y) ^ i
m n✝ : ℕ
h : m ≤ n✝
n : ℕ
a✝ : n ∈ range (n✝ - m)
⊢ x ^ (m + n) * y ^ (m + n) ∈ I ^ m

Tactic:
pow_add,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
f : ℕ → R := fun n ↦ ∑ i ∈ range n, (x * y) ^ i
m n✝ : ℕ
h : m ≤ n✝
n : ℕ
a✝ : n ∈ range (n✝ - m)
⊢ x ^ m * x ^ n * y ^ (m + n) ∈ I ^ m
Module: Mathlib.RingTheory.KrullDimension.Zero

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : KrullDimLE 0 R
⊢ minimalPrimes R = {I | I.IsMaximal}

Tactic:
by
  ext; simp [minimalPrimes_eq_setOfPred_isPrime, Ideal.isMaximal_iff_isPrime]

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

Goal state before:
pp: case h
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
fa : R
fs : Multiset R
fh : fs ≠ ∅ → (∀ b ∈ fs, Associated x b) → ∃ n, Associated (x ^ n) fs.prod
hf₂ : fa ::ₘ fs ≠ ∅
this : ∀ b ∈ fa ::ₘ fs, Associated x b
hf' : fs ≠ ∅
n : ℕ
hn : Associated (x ^ n) fs.prod
⊢ Associated (x ^ (n + 1)) (fa ::ₘ fs).prod

Tactic:
pow_add,

Goal state after:
case h
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
fa : R
fs : Multiset R
fh : fs ≠ ∅ → (∀ b ∈ fs, Associated x b) → ∃ n, Associated (x ^ n) fs.prod
hf₂ : fa ::ₘ fs ≠ ∅
this : ∀ b ∈ fa ::ₘ fs, Associated x b
hf' : fs ≠ ∅
n : ℕ
hn : Associated (x ^ n) fs.prod
⊢ Associated (x ^ n * x ^ 1) (fa ::ₘ fs).prod
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: K : Type u_7
inst✝¹ : DivisionRing K
Γ₀ : Type u_8
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
hv : v.IsNontrivial
⊢ ∃ x, x ≠ 0 ∧ v x < 1

Tactic:
obtain ⟨x, hx⟩ := isNontrivial_iff_exists_unit.mp hv
  rw [ne_iff_lt_or_gt] at hx
  rcases hx with hx | hx
  · use x
    simp [hx]
  · use x⁻¹
    simp [-map_inv₀, ← one_lt_val_iff, hx]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
x y : Associates R
⊢ ↑((associatesEquivIsPrincipal R) (Associates.mk (Quot.out x) * Associates.mk (Quot.out y))) =
    ↑((associatesEquivIsPrincipal R) (Associates.mk (Quot.out x))) *
      ↑((associatesEquivIsPrincipal R) (Associates.mk (Quot.out y)))

Tactic:
mk_mul_mk,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
x y : Associates R
⊢ ↑((associatesEquivIsPrincipal R) (Associates.mk (Quot.out x * Quot.out y))) =
    ↑((associatesEquivIsPrincipal R) (Associates.mk (Quot.out x))) *
      ↑((associatesEquivIsPrincipal R) (Associates.mk (Quot.out y)))
Module: Mathlib.RingTheory.Ideal.IsPrincipal

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
x✝¹ x✝ : Associates R
⊢ ↑((associatesEquivIsPrincipal R).toFun (x✝¹ * x✝)) =
    ↑((associatesEquivIsPrincipal R).toFun x✝¹ * (associatesEquivIsPrincipal R).toFun x✝)

Tactic:
associatesEquivIsPrincipal_mul

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
x✝¹ x✝ : Associates R
⊢ ↑((associatesEquivIsPrincipal R) x✝¹) * ↑((associatesEquivIsPrincipal R) x✝) =
    ↑((associatesEquivIsPrincipal R).toFun x✝¹ * (associatesEquivIsPrincipal R).toFun x✝)
Module: Mathlib.RingTheory.Ideal.IsPrincipal

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
x y : Associates ↥R⁰
⊢ ↑((associatesEquivIsPrincipal R)
        (↑(associatesNonZeroDivisorsEquiv.symm x) * ↑(associatesNonZeroDivisorsEquiv.symm y))) =
    ↑((associatesEquivIsPrincipal R) ↑(associatesNonZeroDivisorsEquiv.symm x)) *
      ↑((associatesEquivIsPrincipal R) ↑(associatesNonZeroDivisorsEquiv.symm y))

Tactic:
associatesEquivIsPrincipal_mul

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

Goal state before:
pp: case neg.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
this✝¹ : (Ideal.span {a}).radical = maximalIdeal R
this✝ : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this✝ = n + 1
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : b ∉ Ideal.span {a}
hb₃ : ∀ m ∈ maximalIdeal R, ∃ k, k * a = b * m
hb₄ : b ≠ 0
K : Type u_1 := FractionRing R
x : K := (algebraMap R K) b / (algebraMap R K) a
M : Submodule R K := Submodule.map (Algebra.linearMap R K) (maximalIdeal R)
ha₃ : (algebraMap R K) a ≠ 0
hx : ¬∀ y ∈ M, x * y ∈ M
this : Submodule.comap (Algebra.linearMap R K) (Submodule.map (DistribSMul.toLinearMap R K x) M) = ⊤
y : R
hy₁ : y ∈ maximalIdeal R
hy₂ : b * y = a
m : R
hm : m ∈ maximalIdeal R
k : R
hk : b * (y * k) = b * m
⊢ m ∈ R ∙ y

Tactic:
rw [← mul_left_cancel₀ hb₄ hk, mul_comm]

Goal state after:
case neg.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
this✝¹ : (Ideal.span {a}).radical = maximalIdeal R
this✝ : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this✝ = n + 1
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : b ∉ Ideal.span {a}
hb₃ : ∀ m ∈ maximalIdeal R, ∃ k, k * a = b * m
hb₄ : b ≠ 0
K : Type u_1 := FractionRing R
x : K := (algebraMap R K) b / (algebraMap R K) a
M : Submodule R K := Submodule.map (Algebra.linearMap R K) (maximalIdeal R)
ha₃ : (algebraMap R K) a ≠ 0
hx : ¬∀ y ∈ M, x * y ∈ M
this : Submodule.comap (Algebra.linearMap R K) (Submodule.map (DistribSMul.toLinearMap R K x) M) = ⊤
y : R
hy₁ : y ∈ maximalIdeal R
hy₂ : b * y = a
m : R
hm : m ∈ maximalIdeal R
k : R
hk : b * (y * k) = b * m
⊢ k * y ∈ R ∙ y
Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
h : ¬IsField R
this : finrank (ResidueField R) (CotangentSpace R) = 1 ↔ finrank (ResidueField R) (CotangentSpace R) ≤ 1
⊢ [IsDiscreteValuationRing R, ValuationRing R, IsDedekindDomain R, IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ P.IsPrime,
      Submodule.IsPrincipal (maximalIdeal R), finrank (ResidueField R) (CotangentSpace R) = 1,
      ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n].TFAE

Tactic:
rw [this]

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
h : ¬IsField R
this : finrank (ResidueField R) (CotangentSpace R) = 1 ↔ finrank (ResidueField R) (CotangentSpace R) ≤ 1
⊢ [IsDiscreteValuationRing R, ValuationRing R, IsDedekindDomain R, IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ P.IsPrime,
      Submodule.IsPrincipal (maximalIdeal R), finrank (ResidueField R) (CotangentSpace R) ≤ 1,
      ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n].TFAE
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: 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
this :
  (algebraMap (R[X] ⧸ P) (Localization M')).comp φ =
    (IsLocalization.map (Localization M') φ ⋯).comp (algebraMap (R ⧸ P') (Localization M))
⊢ ((algebraMap (R[X] ⧸ P) (Localization M')).comp φ).IsIntegral

Tactic:
rw [this]

Goal state after:
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
this :
  (algebraMap (R[X] ⧸ P) (Localization M')).comp φ =
    (IsLocalization.map (Localization M') φ ⋯).comp (algebraMap (R ⧸ P') (Localization M))
⊢ ((IsLocalization.map (Localization M') φ ⋯).comp (algebraMap (R ⧸ P') (Localization M))).IsIntegral
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: R : Type u
S : Type v
T : Type w
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : IsJacobsonRing S
inst✝¹ : Algebra R S
inst✝ : Algebra R T
IH : ∀ (Q : Ideal S), Q.IsMaximal → (algebraMap R (S ⧸ Q)).IsIntegral
v : S[X] ≃ₐ[R] T
P : Ideal T
hP : P.IsMaximal
Q : Ideal S[X] := comap (↑v).toRingHom P
hw : Ideal.map v Q = P
hQ : Q.IsMaximal
w : (S[X] ⧸ Q) ≃ₐ[R] T ⧸ P := Q.quotientEquivAlg P v ⋯
Q' : Ideal S := comap Polynomial.C Q
w' : S ⧸ Q' →ₐ[R] S[X] ⧸ Q := quotientMapₐ Q (Cₐ R S) ⋯
h_eq : algebraMap R (T ⧸ P) = w.toRingEquiv.toRingHom.comp (w'.comp (algebraMap R (S ⧸ Q')))
this : w'.toRingHom = quotientMap Q Polynomial.C ⋯
⊢ w'.IsIntegral

Tactic:
rw [this]

Goal state after:
R : Type u
S : Type v
T : Type w
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : IsJacobsonRing S
inst✝¹ : Algebra R S
inst✝ : Algebra R T
IH : ∀ (Q : Ideal S), Q.IsMaximal → (algebraMap R (S ⧸ Q)).IsIntegral
v : S[X] ≃ₐ[R] T
P : Ideal T
hP : P.IsMaximal
Q : Ideal S[X] := comap (↑v).toRingHom P
hw : Ideal.map v Q = P
hQ : Q.IsMaximal
w : (S[X] ⧸ Q) ≃ₐ[R] T ⧸ P := Q.quotientEquivAlg P v ⋯
Q' : Ideal S := comap Polynomial.C Q
w' : S ⧸ Q' →ₐ[R] S[X] ⧸ Q := quotientMapₐ Q (Cₐ R S) ⋯
h_eq : algebraMap R (T ⧸ P) = w.toRingEquiv.toRingHom.comp (w'.comp (algebraMap R (S ⧸ Q')))
this : w'.toRingHom = quotientMap Q Polynomial.C ⋯
⊢ (quotientMap Q Polynomial.C ⋯).IsIntegral
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsJacobsonRing R
σ : Type u_2
inst✝¹ : _root_.Finite σ
S : Type u_3
inst✝ : Field S
f : MvPolynomial σ R →+* S
hf : Function.Surjective ⇑f
val✝ : Fintype σ
e : Fin (Fintype.card σ) ≃ σ
f' : MvPolynomial (Fin (Fintype.card σ)) R →+* S := f.comp (renameEquiv R e).toRingEquiv.toRingHom
hf' : Function.Surjective ⇑f'
this : (ker f').IsMaximal
g : MvPolynomial (Fin (Fintype.card σ)) R ⧸ ker f' →+* S := Ideal.Quotient.lift (ker f') f' ⋯
hfg : g.comp (Ideal.Quotient.mk (ker f')) = f'
⊢ Function.Surjective ⇑g

Tactic:
rw [← hfg, coe_comp] at hf'

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsJacobsonRing R
σ : Type u_2
inst✝¹ : _root_.Finite σ
S : Type u_3
inst✝ : Field S
f : MvPolynomial σ R →+* S
hf : Function.Surjective ⇑f
val✝ : Fintype σ
e : Fin (Fintype.card σ) ≃ σ
f' : MvPolynomial (Fin (Fintype.card σ)) R →+* S := f.comp (renameEquiv R e).toRingEquiv.toRingHom
this : (ker f').IsMaximal
g : MvPolynomial (Fin (Fintype.card σ)) R ⧸ ker f' →+* S := Ideal.Quotient.lift (ker f') f' ⋯
hf' : Function.Surjective (⇑g ∘ ⇑(Ideal.Quotient.mk (ker f')))
hfg : g.comp (Ideal.Quotient.mk (ker f')) = f'
⊢ Function.Surjective ⇑g
Module: Mathlib.LinearAlgebra.RootSystem.RootPositive

Goal state before:
pp: ι : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
N : Type u_5
inst✝¹² : CommRing S
inst✝¹¹ : LinearOrder S
inst✝¹⁰ : CommRing R
inst✝⁹ : Algebra S R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
P : RootPairing ι R M N
inst✝⁴ : P.IsValuedIn S
B : RootPositiveForm S P
i j : ι
inst✝³ : FaithfulSMul S R
inst✝² : Module S M
inst✝¹ : IsScalarTower S R M
inst✝ : IsStrictOrderedRing S
hi : P.root i ∈ span S (range ⇑P.root)
hj : P.root j ∈ span S (range ⇑P.root)
ri : ↥(span S (range ⇑P.root)) := ⟨P.root i, hi⟩
rj : ↥(span S (range ⇑P.root)) := ⟨P.root j, hj⟩
this : 2 * (B.posForm ri) rj = P.pairingIn S i j * (B.posForm rj) rj
⊢ 0 < 2 * (B.posForm ri) rj ↔ 0 < P.pairingIn S i j * (B.posForm rj) rj

Tactic:
rw [this]

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : Fintype ι
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Field R
inst✝² : Module R M
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsAnisotropic
this✝¹ : IsReflexive R M
this✝ : IsReflexive R N
this : finrank R ↥(LinearMap.ker P.RootForm) = finrank R ↥(P.corootSpan R).dualAnnihilator
⊢ finrank R ↥(Submodule.map (↑P.toPerfPair.symm) (P.corootSpan R).dualAnnihilator) =
    finrank R ↥(LinearMap.ker P.RootForm)

Tactic:
rw [this]

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : Fintype ι
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Field R
inst✝² : Module R M
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsAnisotropic
this✝¹ : IsReflexive R M
this✝ : IsReflexive R N
this : finrank R ↥(LinearMap.ker P.RootForm) = finrank R ↥(P.corootSpan R).dualAnnihilator
⊢ finrank R ↥(Submodule.map (↑P.toPerfPair.symm) (P.corootSpan R).dualAnnihilator) =
    finrank R ↥(P.corootSpan R).dualAnnihilator
Module: Mathlib.Algebra.Module.Submodule.Union

Goal state before:
pp: ι : Type u_1
K : Type u_2
M : Type u_3
inst✝⁴ : Field K
inst✝³ : AddCommGroup M
inst✝² : Module K M
inst✝¹ : Finite ι
inst✝ : Infinite K
f : ι → Dual K M
p : ι → Submodule K M := fun i ↦ LinearMap.ker (f i)
h : ∀ (i : ι), p i ≠ ⊤
⊢ ∃ x, ∀ (i : ι), (f i) x ≠ 0

Tactic:
obtain ⟨x, hx⟩ := Submodule.exists_forall_notMem_of_forall_ne_top p h

Goal state after:
ι : Type u_1
K : Type u_2
M : Type u_3
inst✝⁴ : Field K
inst✝³ : AddCommGroup M
inst✝² : Module K M
inst✝¹ : Finite ι
inst✝ : Infinite K
f : ι → Dual K M
p : ι → Submodule K M := fun i ↦ LinearMap.ker (f i)
h : ∀ (i : ι), p i ≠ ⊤
x : M
hx : ∀ (i : ι), x ∉ p i
⊢ ∃ x, ∀ (i : ι), (f i) x ≠ 0
Module: Mathlib.LinearAlgebra.QuadraticForm.Prod

Goal state before:
pp: R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R P
inst✝¹ : PartialOrder P
inst✝ : AddLeftMono P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
⊢ (Q₁.prod Q₂).PosDef ↔ Q₁.PosDef ∧ Q₂.PosDef

Tactic:
simp_rw [posDef_iff_nonneg, nonneg_prod_iff]

Goal state after:
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R P
inst✝¹ : PartialOrder P
inst✝ : AddLeftMono P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
⊢ ((∀ (x : M₁), 0 ≤ Q₁ x) ∧ ∀ (x : M₂), 0 ≤ Q₂ x) ∧ (Q₁.prod Q₂).Anisotropic ↔
    ((∀ (x : M₁), 0 ≤ Q₁ x) ∧ Q₁.Anisotropic) ∧ (∀ (x : M₂), 0 ≤ Q₂ x) ∧ Q₂.Anisotropic