-- Mathlib/RingTheory/DedekindDomain/AdicValuation.lean
theorem intValuation.map_mul' (x y : R) :
    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
⊢ Associates.mk (Ideal.span {x}) ≠ 0

Tactic:
apply Associates.mk_ne_zero'.mpr hx

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
⊢ (if x * y = 0 then 0
    else ↑(ofAdd (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x * y})).factors)))) =
    (if x = 0 then 0 else ↑(ofAdd (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors)))) *
      if y = 0 then 0 else ↑(ofAdd (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {y})).factors)))

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
⊢ (if x * y = 0 then 0
    else ↑(ofAdd (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x * y})).factors)))) =
    (if x = 0 then 0 else ↑(ofAdd (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors)))) *
      if y = 0 then 0 else ↑(ofAdd (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {y})).factors)))

case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
⊢ (if x * y = 0 then 0
    else ↑(ofAdd (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x * y})).factors)))) =
    (if x = 0 then 0 else ↑(ofAdd (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors)))) *
      if y = 0 then 0 else ↑(ofAdd (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {y})).factors)))

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
⊢ (if x * y = 0 then 0
    else ↑(ofAdd (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x * y})).factors)))) =
    (if x = 0 then 0 else ↑(ofAdd (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors)))) *
      if y = 0 then 0 else ↑(ofAdd (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {y})).factors)))

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
⊢ (if x * y = 0 then 0
    else ↑(ofAdd (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x * y})).factors)))) =
    (if x = 0 then 0 else ↑(ofAdd (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors)))) *
      if y = 0 then 0 else ↑(ofAdd (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {y})).factors)))

case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
⊢ (if x * y = 0 then 0
    else ↑(ofAdd (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x * y})).factors)))) =
    (if x = 0 then 0 else ↑(ofAdd (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors)))) *
      if y = 0 then 0 else ↑(ofAdd (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {y})).factors)))

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:
simp only [intValuationDef]

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
⊢ (if x * y = 0 then 0
    else ↑(ofAdd (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x * y})).factors)))) =
    (if x = 0 then 0 else ↑(ofAdd (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors)))) *
      if y = 0 then 0 else ↑(ofAdd (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {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
⊢ 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
⊢ Associates.mk (Ideal.span {y}) ≠ 0

Tactic:
apply Associates.mk_ne_zero'.mpr hy

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
⊢ ofAdd
      (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors +
            (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {y})).factors)) =
    ofAdd
      (-(↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors) +
          ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {y})).factors)))

Tactic:
rfl

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
⊢ (if x * y = 0 then 0
    else ↑(ofAdd (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x * y})).factors)))) =
    (if x = 0 then 0 else ↑(ofAdd (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors)))) *
      if y = 0 then 0 else ↑(ofAdd (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {y})).factors)))

Tactic:
rw [hx, zero_mul, if_pos (Eq.refl _), zero_mul]

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
⊢ (if x * y = 0 then 0
    else ↑(ofAdd (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x * y})).factors)))) =
    (if x = 0 then 0 else ↑(ofAdd (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors)))) *
      if y = 0 then 0 else ↑(ofAdd (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {y})).factors)))

Tactic:
rw [hy, mul_zero, if_pos (Eq.refl _), mul_zero]

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
⊢ (if x * y = 0 then 0
    else ↑(ofAdd (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x * y})).factors)))) =
    (if x = 0 then 0 else ↑(ofAdd (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors)))) *
      if y = 0 then 0 else ↑(ofAdd (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {y})).factors)))

Tactic:
rw [if_neg hx, if_neg hy, if_neg (mul_ne_zero hx hy), ← WithZero.coe_mul, WithZero.coe_inj, ←
  ofAdd_add, ← Ideal.span_singleton_mul_span_singleton, ← Associates.mk_mul_mk, ← neg_add,
  Associates.count_mul (by apply Associates.mk_ne_zero'.mpr hx)
    (by apply Associates.mk_ne_zero'.mpr hy) (by apply v.associates_irreducible)]

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
⊢ ofAdd
      (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors +
            (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {y})).factors)) =
    ofAdd
      (-(↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors) +
          ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {y})).factors)))