-- Mathlib/RingTheory/DedekindDomain/AdicValuation.lean
theorem intValuation.map_add_le_max' (x y : R) :
    v.intValuationDef (x + y) ≤ max (v.intValuationDef x) (v.intValuationDef y)

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
⊢ v.intValuationDef (x + y) ≤ v.intValuationDef x ⊔ v.intValuationDef y

Tactic:
by_cases hx : x = 0

Result:
case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : x = 0
⊢ v.intValuationDef (x + y) ≤ v.intValuationDef x ⊔ v.intValuationDef y

case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
⊢ v.intValuationDef (x + y) ≤ v.intValuationDef x ⊔ v.intValuationDef y

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
nmin : ℕ :=
  (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors ⊓
    (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {y})).factors
h_dvd_x : x ∈ v.asIdeal ^ nmin
⊢ nmin ≤ (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {y})).factors

Tactic:
exact min_le_right _ _

Result:
no goals

Proof state:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
nmin : ℕ :=
  (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors ⊓
    (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {y})).factors
h_dvd_x : x ∈ v.asIdeal ^ nmin
h_dvd_y : y ∈ v.asIdeal ^ nmin
h_dvd_xy : Associates.mk v.asIdeal ^ nmin ≤ Associates.mk (Ideal.span {x + y})
⊢ nmin ≤ (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x + y})).factors

Tactic:
rw [Associates.prime_pow_dvd_iff_le (Associates.mk_ne_zero'.mpr hxy) _] at h_dvd_xy

Result:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
nmin : ℕ :=
  (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors ⊓
    (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {y})).factors
h_dvd_x : x ∈ v.asIdeal ^ nmin
h_dvd_y : y ∈ v.asIdeal ^ nmin
h_dvd_xy : nmin ≤ (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x + y})).factors
⊢ nmin ≤ (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x + y})).factors

R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
nmin : ℕ :=
  (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors ⊓
    (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {y})).factors
h_dvd_x : x ∈ v.asIdeal ^ nmin
h_dvd_y : y ∈ v.asIdeal ^ nmin
h_dvd_xy : Associates.mk v.asIdeal ^ nmin ≤ Associates.mk (Ideal.span {x + y})
⊢ Irreducible (Associates.mk v.asIdeal)

Proof state:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
⊢ (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors ⊓
      (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {y})).factors ≤
    (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x + y})).factors

Tactic:
set nmin :=
  min ((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span { x })).factors)
    ((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span { y })).factors)

Result:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
nmin : ℕ :=
  (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors ⊓
    (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {y})).factors
⊢ nmin ≤ (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x + y})).factors

Proof state:
case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : y = 0
⊢ v.intValuationDef x ≤ v.intValuationDef x ⊔ v.intValuationDef 0

Tactic:
conv_rhs => rw [max_comm, intValuationDef, if_pos (Eq.refl _)]

Result:
case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : y = 0
⊢ v.intValuationDef x ≤ 0 ⊔ v.intValuationDef x

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
nmin : ℕ :=
  (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors ⊓
    (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {y})).factors
h_dvd_x : x ∈ v.asIdeal ^ nmin
⊢ y ∈ v.asIdeal ^ nmin

Tactic:
rw [← Associates.le_singleton_iff y nmin _,
  Associates.prime_pow_dvd_iff_le (Associates.mk_ne_zero'.mpr hy) _]

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
nmin : ℕ :=
  (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors ⊓
    (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {y})).factors
h_dvd_x : x ∈ v.asIdeal ^ nmin
⊢ nmin ≤ (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {y})).factors

R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
nmin : ℕ :=
  (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors ⊓
    (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {y})).factors
h_dvd_x : x ∈ v.asIdeal ^ nmin
⊢ Irreducible (Associates.mk v.asIdeal)

Proof state:
case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : x + y = 0
⊢ 0 ≤ v.intValuationDef x ⊔ v.intValuationDef y

Tactic:
exact zero_le'

Result:
no goals

Proof state:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
⊢ v.intValuationDef (x + y) ≤ v.intValuationDef x ⊔ v.intValuationDef y

Tactic:
by_cases hy : y = 0

Result:
case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : y = 0
⊢ v.intValuationDef (x + y) ≤ v.intValuationDef x ⊔ v.intValuationDef y

case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
⊢ v.intValuationDef (x + y) ≤ v.intValuationDef x ⊔ v.intValuationDef y

Proof state:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
nmin : ℕ :=
  (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors ⊓
    (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {y})).factors
h_dvd_x : x ∈ v.asIdeal ^ nmin
h_dvd_y : y ∈ v.asIdeal ^ nmin
h_dvd_xy : nmin ≤ (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x + y})).factors
⊢ nmin ≤ (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x + y})).factors

Tactic:
exact h_dvd_xy

Result:
no goals

Proof state:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
⊢ v.intValuationDef (x + y) ≤ v.intValuationDef x ⊔ v.intValuationDef y

Tactic:
by_cases hxy : x + y = 0

Result:
case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : x + y = 0
⊢ v.intValuationDef (x + y) ≤ v.intValuationDef x ⊔ v.intValuationDef y

case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
⊢ v.intValuationDef (x + y) ≤ v.intValuationDef x ⊔ v.intValuationDef y