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

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

pp: case mpr.inr
Γ₀ : Type v
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst✝ : Field K
v : Valuation K Γ₀
γ : Γ₀
x : K
hx : v x ≤ min 1 γ
h : min 1 γ = γ
h' : γ < 1
⊢ ∃ y, v ↑y ≤ γ ∧ (algebraMap (↥v.integer) K) y = x

Tactic:
<;>

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

case mpr.inr
Γ₀ : Type v
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst✝ : Field K
v : Valuation K Γ₀
γ : Γ₀
x : K
hx : v x ≤ min 1 γ
h : min 1 γ = γ
h' : γ < 1
⊢ ∃ y, v ↑y ≤ γ ∧ (algebraMap (↥v.integer) K) y = x
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 ≠ ⊥
⊢ ∀ (y : Ideal R), (fun P ↦ P ≠ ⊥ ∧ P.IsPrime) y → y = maximalIdeal R

Tactic:
rintro Q ⟨hQ1, hQ2⟩
      obtain ⟨q, rfl⟩ := (IsPrincipalIdealRing.principal Q).1
      have hq : q ≠ 0 := by
        rintro rfl
        apply hQ1
        simp
      rw [submodule_span_eq, span_singleton_prime hq] at hQ2
      replace hQ2 := hQ2.irreducible
      rw [irreducible_iff_uniformizer] at hQ2
      exact hQ2.symm

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

Goal state before:
pp: case e'_2
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}
x y : R
e' : x * (a * g) + y * (b * g) = g
h : g ≠ 0
⊢ (fun a ↦ a * g) (x * a + y * b) = x * (a * g) + y * (b * g)

pp: case e'_3
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}
x y : R
e' : x * (a * g) + y * (b * g) = g
h : g ≠ 0
⊢ (fun a ↦ a * g) 1 = g

Tactic:
<;>

Goal state after:
case e'_2
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}
x y : R
e' : x * (a * g) + y * (b * g) = g
h : g ≠ 0
⊢ (fun a ↦ a * g) (x * a + y * b) = x * (a * g) + y * (b * g)

case e'_3
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}
x y : R
e' : x * (a * g) + y * (b * g) = g
h : g ≠ 0
⊢ (fun a ↦ a * g) 1 = g
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: case pos
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
r : R
hr : r ∈ I
hr0 : r = 0
⊢ r ∈ span {p ^ Nat.find ex}

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
r : R
hr : r ∈ I
hr0 : ¬r = 0
⊢ r ∈ span {p ^ Nat.find ex}

Tactic:
· simp only [hr0, Submodule.zero_mem]

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
r : R
hr : r ∈ I
hr0 : ¬r = 0
⊢ r ∈ span {p ^ Nat.find ex}
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
y : R
inst✝¹ : Algebra R S
inst✝ : Away y S
H : IsJacobsonRing R
P' : Ideal S
hP'✝ : P'.IsPrime
hP' : (under R P').IsPrime
hPM : Disjoint ↑(powers y) ↑(under R P')
hP : (under R P').jacobson = under R P'
x : R
hx : x ∈ sInf {I | Ideal.comap (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I}
J : Ideal R
hJ : J ∈ {J | Ideal.comap (algebraMap R S) P' ≤ J ∧ J.IsMaximal}
⊢ x * y ∈ J

Tactic:
by_cases h : y ∈ J

Goal state after:
case pos
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
y : R
inst✝¹ : Algebra R S
inst✝ : Away y S
H : IsJacobsonRing R
P' : Ideal S
hP'✝ : P'.IsPrime
hP' : (under R P').IsPrime
hPM : Disjoint ↑(powers y) ↑(under R P')
hP : (under R P').jacobson = under R P'
x : R
hx : x ∈ sInf {I | Ideal.comap (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I}
J : Ideal R
hJ : J ∈ {J | Ideal.comap (algebraMap R S) P' ≤ J ∧ J.IsMaximal}
h : y ∈ J
⊢ x * y ∈ J

case neg
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
y : R
inst✝¹ : Algebra R S
inst✝ : Away y S
H : IsJacobsonRing R
P' : Ideal S
hP'✝ : P'.IsPrime
hP' : (under R P').IsPrime
hPM : Disjoint ↑(powers y) ↑(under R P')
hP : (under R P').jacobson = under R P'
x : R
hx : x ∈ sInf {I | Ideal.comap (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I}
J : Ideal R
hJ : J ∈ {J | Ideal.comap (algebraMap R S) P' ≤ J ∧ J.IsMaximal}
h : y ∉ J
⊢ x * y ∈ J
Module: Mathlib.RingTheory.KrullDimension.Zero

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I✝ : Ideal R
inst✝ : Ring.KrullDimLE 0 R
I : Ideal R
hI : I.IsRadical
⊢ I.jacobson = I

Tactic:
by rw [I.jacobson_eq_radical, hI.radical]

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

Goal state before:
pp: case pos
R : Type u_3
Γ₀ : Type u_4
inst✝⁴ : Ring R
inst✝³ : LinearOrderedCommMonoidWithZero Γ₀
inst✝² : Nontrivial R
inst✝¹ : NoZeroDivisors R
inst✝ : DecidablePred fun x ↦ x = 0
x : R
h✝ : x = 0
⊢ 0 ≤ 1

pp: case neg
R : Type u_3
Γ₀ : Type u_4
inst✝⁴ : Ring R
inst✝³ : LinearOrderedCommMonoidWithZero Γ₀
inst✝² : Nontrivial R
inst✝¹ : NoZeroDivisors R
inst✝ : DecidablePred fun x ↦ x = 0
x : R
h✝ : ¬x = 0
⊢ 1 ≤ 1

Tactic:
<;>

Goal state after:
case pos
R : Type u_3
Γ₀ : Type u_4
inst✝⁴ : Ring R
inst✝³ : LinearOrderedCommMonoidWithZero Γ₀
inst✝² : Nontrivial R
inst✝¹ : NoZeroDivisors R
inst✝ : DecidablePred fun x ↦ x = 0
x : R
h✝ : x = 0
⊢ 0 ≤ 1

case neg
R : Type u_3
Γ₀ : Type u_4
inst✝⁴ : Ring R
inst✝³ : LinearOrderedCommMonoidWithZero Γ₀
inst✝² : Nontrivial R
inst✝¹ : NoZeroDivisors R
inst✝ : DecidablePred fun x ↦ x = 0
x : R
h✝ : ¬x = 0
⊢ 1 ≤ 1
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: case pos
R : Type u_3
Γ₀ : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : LinearOrderedCommMonoidWithZero Γ₀
inst✝³ : Nontrivial R
inst✝² : NoZeroDivisors R
inst✝¹ : DecidablePred fun x ↦ x = 0
inst✝ : Nontrivial Γ₀
x : R
h✝ : x = 0
⊢ 0 < 1 ↔ x = 0

pp: case neg
R : Type u_3
Γ₀ : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : LinearOrderedCommMonoidWithZero Γ₀
inst✝³ : Nontrivial R
inst✝² : NoZeroDivisors R
inst✝¹ : DecidablePred fun x ↦ x = 0
inst✝ : Nontrivial Γ₀
x : R
h✝ : ¬x = 0
⊢ 1 < 1 ↔ x = 0

Tactic:
<;>

Goal state after:
case pos
R : Type u_3
Γ₀ : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : LinearOrderedCommMonoidWithZero Γ₀
inst✝³ : Nontrivial R
inst✝² : NoZeroDivisors R
inst✝¹ : DecidablePred fun x ↦ x = 0
inst✝ : Nontrivial Γ₀
x : R
h✝ : x = 0
⊢ 0 < 1 ↔ x = 0

case neg
R : Type u_3
Γ₀ : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : LinearOrderedCommMonoidWithZero Γ₀
inst✝³ : Nontrivial R
inst✝² : NoZeroDivisors R
inst✝¹ : DecidablePred fun x ↦ x = 0
inst✝ : Nontrivial Γ₀
x : R
h✝ : ¬x = 0
⊢ 1 < 1 ↔ x = 0
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: case mp
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
a b : R
hp : Prime (Classical.choose ⋯)
⊢ (addVal R) a ≤ (addVal R) b → a ∣ b

pp: case mpr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
a b : R
hp : Prime (Classical.choose ⋯)
⊢ a ∣ b → (addVal R) a ≤ (addVal R) b

Tactic:
<;>

Goal state after:
case mp
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
a b : R
hp : Prime (Classical.choose ⋯)
⊢ (addVal R) a ≤ (addVal R) b → a ∣ b

case mpr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
a b : R
hp : Prime (Classical.choose ⋯)
⊢ a ∣ b → (addVal R) a ≤ (addVal R) b
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
a b : R
hp : Prime (Classical.choose ⋯)
h : (addVal R) b = ⊤
ha0 : a = 0
⊢ a ∣ b

Tactic:
addVal_eq_top_iff

Goal state after:
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
a b : R
hp : Prime (Classical.choose ⋯)
h : b = 0
ha0 : a = 0
⊢ a ∣ b
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

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

Tactic:
<;>

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

R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
u : Rˣ
ϖ : R
hϖ : Irreducible ϖ
⊢ ↑u = ↑u * ϖ ^ 0
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:
addVal_eq_top_iff

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.DiscreteValuationRing.Basic

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

Tactic:
addVal_eq_top_iff

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

Goal state before:
pp: case pos
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
h : (ofClass v) x = 0
⊢ 0 < 0 ↔ 0 < v x

pp: case neg
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
h : ¬(ofClass v) x = 0
⊢ 0 < ↑⟨Units.mk0 ((ofClass v) x) h, ⋯⟩ ↔ 0 < v x

Tactic:
<;>

Goal state after:
case pos
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
h : (ofClass v) x = 0
⊢ 0 < 0 ↔ 0 < v x

case neg
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
h : ¬(ofClass v) x = 0
⊢ 0 < ↑⟨Units.mk0 ((ofClass v) x) h, ⋯⟩ ↔ 0 < v x
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: case coe
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
vx : ℕ
hvx : (addVal R) x = ↑vx
⊢ ↑vx ≤ vy ↔ x ∣ y

Tactic:
| coe vx =>

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

Goal state before:
pp: case inl
R : Type u_3
Γ₀ : Type u_4
inst✝³ : Ring R
inst✝² : LinearOrderedCommMonoidWithZero Γ₀
inst✝¹ : IsDomain R
inst✝ : DecidablePred fun x ↦ x = 0
hx : 1 0 ≠ 0
hx' : 1 0 ≠ 1
⊢ False

pp: case inr
R : Type u_3
Γ₀ : Type u_4
inst✝³ : Ring R
inst✝² : LinearOrderedCommMonoidWithZero Γ₀
inst✝¹ : IsDomain R
inst✝ : DecidablePred fun x ↦ x = 0
x : R
hx : 1 x ≠ 0
hx' : 1 x ≠ 1
hx0 : x ≠ 0
⊢ False

Tactic:
<;>

Goal state after:
case inl
R : Type u_3
Γ₀ : Type u_4
inst✝³ : Ring R
inst✝² : LinearOrderedCommMonoidWithZero Γ₀
inst✝¹ : IsDomain R
inst✝ : DecidablePred fun x ↦ x = 0
hx : 1 0 ≠ 0
hx' : 1 0 ≠ 1
⊢ False

case inr
R : Type u_3
Γ₀ : Type u_4
inst✝³ : Ring R
inst✝² : LinearOrderedCommMonoidWithZero Γ₀
inst✝¹ : IsDomain R
inst✝ : DecidablePred fun x ↦ x = 0
x : R
hx : 1 x ≠ 0
hx' : 1 x ≠ 1
hx0 : x ≠ 0
⊢ False
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: case inl
R : Type u_3
Γ₀ : Type u_4
inst✝³ : Ring R
inst✝² : LinearOrderedCommMonoidWithZero Γ₀
inst✝¹ : IsDomain R
inst✝ : DecidablePred fun x ↦ x = 0
hx : 1 0 ≠ 0
hx' : 1 0 ≠ 1
⊢ False

Tactic:
simp_all [one_apply_of_ne_zero]

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

Goal state before:
pp: case inr
R : Type u_3
Γ₀ : Type u_4
inst✝³ : Ring R
inst✝² : LinearOrderedCommMonoidWithZero Γ₀
inst✝¹ : IsDomain R
inst✝ : DecidablePred fun x ↦ x = 0
x : R
hx : 1 x ≠ 0
hx' : 1 x ≠ 1
hx0 : x ≠ 0
⊢ False

Tactic:
simp_all [one_apply_of_ne_zero]

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Dvr

Goal state before:
pp: R : Type u_2
Rₘ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
M : Submonoid R
inst✝ : IsLocalization M Rₘ
hM : M ≤ R⁰
h : DimensionLEOne R
p : Ideal Rₘ
hp0 : p ≠ ⊥
hpp : p.IsPrime
P : Ideal Rₘ
hpP : p < P
hPm : P.IsMaximal
hpP' : ⟨p, hpp⟩ < ⟨P, ⋯⟩
⊢ False

Tactic:
← (IsLocalization.orderIsoOfPrime M Rₘ).lt_iff_lt

Goal state after:
R : Type u_2
Rₘ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
M : Submonoid R
inst✝ : IsLocalization M Rₘ
hM : M ≤ R⁰
h : DimensionLEOne R
p : Ideal Rₘ
hp0 : p ≠ ⊥
hpp : p.IsPrime
P : Ideal Rₘ
hpP : p < P
hPm : P.IsMaximal
hpP' : (IsLocalization.orderIsoOfPrime M Rₘ) ⟨p, hpp⟩ < (IsLocalization.orderIsoOfPrime M Rₘ) ⟨P, ⋯⟩
⊢ False
Module: Mathlib.RingTheory.DedekindDomain.Dvr

Goal state before:
pp: R : Type u_2
Rₘ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
M : Submonoid R
inst✝ : IsLocalization M Rₘ
hM : M ≤ R⁰
h : DimensionLEOne R
p : Ideal Rₘ
hp0 : p ≠ ⊥
hpp : p.IsPrime
P : Ideal Rₘ
hpP : p < P
hPm : P.IsMaximal
hpP' : (IsLocalization.orderIsoOfPrime M Rₘ) ⟨p, hpp⟩ < (IsLocalization.orderIsoOfPrime M Rₘ) ⟨P, ⋯⟩
⊢ False

Tactic:
refine h.not_lt_lt ⊥ (p.under R) (P.under R) ⟨?_, hpP'⟩

Goal state after:
R : Type u_2
Rₘ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
M : Submonoid R
inst✝ : IsLocalization M Rₘ
hM : M ≤ R⁰
h : DimensionLEOne R
p : Ideal Rₘ
hp0 : p ≠ ⊥
hpp : p.IsPrime
P : Ideal Rₘ
hpP : p < P
hPm : P.IsMaximal
hpP' : (IsLocalization.orderIsoOfPrime M Rₘ) ⟨p, hpp⟩ < (IsLocalization.orderIsoOfPrime M Rₘ) ⟨P, ⋯⟩
⊢ ⊥ < Ideal.under R p
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: case pos
Γ₀ : Type u_4
inst✝⁴ : LinearOrderedCommMonoidWithZero Γ₀
B : Type u_7
A : Type u_8
inst✝³ : CommSemiring A
inst✝² : Ring B
inst✝¹ : Algebra A B
v : Valuation B Γ₀
inst✝ : IsTrivialOn A v
a : A
h✝ : a = 0
⊢ v ((algebraMap A B) a) ≤ 1

pp: case neg
Γ₀ : Type u_4
inst✝⁴ : LinearOrderedCommMonoidWithZero Γ₀
B : Type u_7
A : Type u_8
inst✝³ : CommSemiring A
inst✝² : Ring B
inst✝¹ : Algebra A B
v : Valuation B Γ₀
inst✝ : IsTrivialOn A v
a : A
h✝ : ¬a = 0
⊢ v ((algebraMap A B) a) ≤ 1

Tactic:
<;>

Goal state after:
case pos
Γ₀ : Type u_4
inst✝⁴ : LinearOrderedCommMonoidWithZero Γ₀
B : Type u_7
A : Type u_8
inst✝³ : CommSemiring A
inst✝² : Ring B
inst✝¹ : Algebra A B
v : Valuation B Γ₀
inst✝ : IsTrivialOn A v
a : A
h✝ : a = 0
⊢ v ((algebraMap A B) a) ≤ 1

case neg
Γ₀ : Type u_4
inst✝⁴ : LinearOrderedCommMonoidWithZero Γ₀
B : Type u_7
A : Type u_8
inst✝³ : CommSemiring A
inst✝² : Ring B
inst✝¹ : Algebra A B
v : Valuation B Γ₀
inst✝ : IsTrivialOn A v
a : A
h✝ : ¬a = 0
⊢ v ((algebraMap A B) a) ≤ 1
Module: Mathlib.RingTheory.Ideal.IsPrincipal

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x : R
property✝¹ : R ∙ x ∈ (Ideal R)⁰
y : R
property✝ : R ∙ y ∈ (Ideal R)⁰
⊢ span {x} * span {y} = span {x * y}

Tactic:
span_singleton_mul_span_singleton

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
⊢ span {Quot.out x * Quot.out y} = span {Quot.out x} * span {Quot.out y}

Tactic:
span_singleton_mul_span_singleton

Goal state after:
Module: Mathlib.Algebra.Ring.SumsOfSquares

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : AddMonoid R
inst✝ : Mul R
s₁ s₂ : R
h₂ : IsSumSq s₂
⊢ IsSumSq (0 + s₂)

pp: case sq_add
R : Type u_1
inst✝¹ : AddMonoid R
inst✝ : Mul R
s₁ s₂ : R
h₂ : IsSumSq s₂
a✝ s✝ : R
hs✝ : IsSumSq s✝
hs_ih✝ : IsSumSq (s✝ + s₂)
⊢ IsSumSq (a✝ * a✝ + s✝ + s₂)

Tactic:
<;>

Goal state after:
case zero
R : Type u_1
inst✝¹ : AddMonoid R
inst✝ : Mul R
s₁ s₂ : R
h₂ : IsSumSq s₂
⊢ IsSumSq (0 + s₂)

case sq_add
R : Type u_1
inst✝¹ : AddMonoid R
inst✝ : Mul R
s₁ s₂ : R
h₂ : IsSumSq s₂
a✝ s✝ : R
hs✝ : IsSumSq s✝
hs_ih✝ : IsSumSq (s✝ + s₂)
⊢ IsSumSq (a✝ * a✝ + s✝ + s₂)
Module: Mathlib.Algebra.Ring.SumsOfSquares

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : AddMonoid R
inst✝ : Mul R
x : R
⊢ 0 ∈ closure {x | IsSquare x}

pp: case sq_add
R : Type u_1
inst✝¹ : AddMonoid R
inst✝ : Mul R
x a✝ s✝ : R
hs✝ : IsSumSq s✝
hs_ih✝ : s✝ ∈ closure {x | IsSquare x}
⊢ a✝ * a✝ + s✝ ∈ closure {x | IsSquare x}

Tactic:
<;>

Goal state after:
case zero
R : Type u_1
inst✝¹ : AddMonoid R
inst✝ : Mul R
x : R
⊢ 0 ∈ closure {x | IsSquare x}

case sq_add
R : Type u_1
inst✝¹ : AddMonoid R
inst✝ : Mul R
x a✝ s✝ : R
hs✝ : IsSumSq s✝
hs_ih✝ : s✝ ∈ closure {x | IsSquare x}
⊢ a✝ * a✝ + s✝ ∈ closure {x | IsSquare x}
Module: Mathlib.Algebra.Ring.SumsOfSquares

Goal state before:
pp: case zero
R : Type u_2
inst✝ : NonAssocSemiring R
⊢ IsSumSq ↑0

pp: case succ
R : Type u_2
inst✝ : NonAssocSemiring R
n✝ : ℕ
a✝ : IsSumSq ↑n✝
⊢ IsSumSq ↑(n✝ + 1)

Tactic:
<;>

Goal state after:
case zero
R : Type u_2
inst✝ : NonAssocSemiring R
⊢ IsSumSq ↑0

case succ
R : Type u_2
inst✝ : NonAssocSemiring R
n✝ : ℕ
a✝ : IsSumSq ↑n✝
⊢ IsSumSq ↑(n✝ + 1)
Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
⊢ ⨅ i, LinearMap.ker (P.root' i) = (span R (range P.root')).dualCoannihilator

Tactic:
by
  rw [← rootSpan_dualAnnihilator_map_eq, rootSpan_dualAnnihilator_map_eq_iInf_ker_root']

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
inst✝⁸ : AddCommGroup N
inst✝⁷ : Module R N
P : RootPairing ι R M N
S : Type u_5
inst✝⁶ : CommRing S
inst✝⁵ : Algebra S R
inst✝⁴ : FaithfulSMul S R
inst✝³ : Module S M
inst✝² : IsScalarTower S R M
inst✝¹ : P.IsValuedIn S
inst✝ : Fintype ι
x y : ↥(P.rootSpan S)
⊢ (algebraMap S R) (((P.RootFormIn S) x) y) = (P.RootForm ↑x) ↑y

Tactic:
simp [RootFormIn, rootForm_apply_apply]

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
P₁ P₂ : RootPairing ι R M N
he : P₁.toLinearMap = P₂.toLinearMap
hr : P₁.root = P₂.root
hc : range ⇑P₁.coroot = range ⇑P₂.coroot
⊢ P₁ = P₂

Tactic:
by
  have hp (hc' : P₁.coroot = P₂.coroot) : P₁.reflectionPerm = P₂.reflectionPerm := by
    ext i j
    refine P₁.root.injective ?_
    conv_rhs => rw [hr]
    simp only [root_reflectionPerm, reflection_apply, coroot']
    simp only [hr, he, hc']
  suffices P₁.coroot = P₂.coroot by
    obtain ⟨p₁⟩ := P₁; obtain ⟨p₂⟩ := P₂
    #adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
    (replacing grind's canonicalizer with a type-directed normalizer), `grind` closed this goal.
    It is not yet clear whether this is due to defeq abuse in Mathlib or a problem in the new
    canonicalizer; a minimization would help. The original proof was: `grind` -/
    simp_all
  have : IsAddTorsionFree M := .of_isTorsionFree R M
  ext i
  apply P₁.injOn_dualMap_subtype_span_root_coroot (mem_range_self i) (hc ▸ mem_range_self i)
  simp only [LinearMap.coe_comp, comp_apply]
  apply Dual.eq_of_preReflection_mapsTo' (finite_range P₁.root)
  · exact Submodule.subset_span (mem_range_self i)
  · exact P₁.coroot_root_two i
  · exact P₁.mapsTo_reflection_root i
  · exact hr ▸ he ▸ P₂.coroot_root_two i
  · exact hr ▸ he ▸ P₂.mapsTo_reflection_root i

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

Goal state before:
pp: case inr
K : Type u_1
inst✝² : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ (x : K), v x ≤ 1 ↔ v' x ≤ 1
x y : K
hy : y ≠ 0
⊢ 0 < v' y

pp: case inr
K : Type u_1
inst✝² : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ (x : K), v x ≤ 1 ↔ v' x ≤ 1
x y : K
hy : y ≠ 0
⊢ 0 < v y

Tactic:
<;>

Goal state after:
case inr
K : Type u_1
inst✝² : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ (x : K), v x ≤ 1 ↔ v' x ≤ 1
x y : K
hy : y ≠ 0
⊢ 0 < v' y

case inr
K : Type u_1
inst✝² : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ (x : K), v x ≤ 1 ↔ v' x ≤ 1
x y : K
hy : y ≠ 0
⊢ 0 < v y