-- 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
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})).factors

Tactic:
exact min_le_left _ _

Result:
no goals

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 ≤ 0 ⊔ v.intValuationDef x

Tactic:
rw [max_eq_right (WithZero.zero_le (v.intValuationDef x))]

Result:
no goals

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

Tactic:
conv_rhs => rw [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
⊢ v.intValuationDef y ≤ 0 ⊔ 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
⊢ Irreducible (Associates.mk v.asIdeal)

Tactic:
apply v.associates_irreducible

Result:
no goals

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
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)

Tactic:
apply v.associates_irreducible

Result:
no goals

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 + y) ≤ v.intValuationDef x ⊔ v.intValuationDef y

Tactic:
rw [hy, add_zero]

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 ≤ v.intValuationDef x ⊔ v.intValuationDef 0

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
h_dvd_y : y ∈ v.asIdeal ^ nmin
⊢ Associates.mk v.asIdeal ^ nmin ≤ Associates.mk (Ideal.span {x + y})

Tactic:
rw [Associates.le_singleton_iff]

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
h_dvd_y : y ∈ v.asIdeal ^ nmin
⊢ x + y ∈ v.asIdeal ^ nmin

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
⊢ v.intValuationDef (x + y) ≤ v.intValuationDef x ⊔ v.intValuationDef y

Tactic:
rw [intValuationDef, if_pos hxy]

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
⊢ 0 ≤ 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
⊢ v.intValuationDef (x + y) ≤ v.intValuationDef x ⊔ v.intValuationDef y

Tactic:
rw [v.intValuationDef_if_neg hxy, v.intValuationDef_if_neg hx, v.intValuationDef_if_neg hy,
  WithZero.le_max_iff, intValuation.le_max_iff_min_le]

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
⊢ (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

Proof state:
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

Tactic:
rw [hx, zero_add]

Result:
case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : x = 0
⊢ v.intValuationDef y ≤ v.intValuationDef 0 ⊔ 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
⊢ nmin ≤ (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x + y})).factors

Tactic:
have h_dvd_xy : Associates.mk v.asIdeal ^ nmin ≤ Associates.mk (Ideal.span {x + y}) := by
  rw [Associates.le_singleton_iff]
  exact Ideal.add_mem (v.asIdeal ^ nmin) h_dvd_x h_dvd_y

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 : Associates.mk v.asIdeal ^ nmin ≤ Associates.mk (Ideal.span {x + y})
⊢ nmin ≤ (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x + y})).factors

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
⊢ Irreducible (Associates.mk v.asIdeal)

Tactic:
apply v.associates_irreducible

Result:
no goals

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

Tactic:
rw [max_eq_right (WithZero.zero_le (v.intValuationDef y))]

Result:
no goals

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
h_dvd_y : y ∈ v.asIdeal ^ nmin
⊢ x + y ∈ v.asIdeal ^ nmin

Tactic:
exact Ideal.add_mem (v.asIdeal ^ nmin) h_dvd_x h_dvd_y

Result:
no goals