-- Mathlib/RingTheory/DedekindDomain/Factorization.lean
theorem count_mul {I I' : FractionalIdeal R⁰ K} (hI : I ≠ 0) (hI' : I' ≠ 0) :
    count K v (I * I') = count K v I + count K v I'

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I I' : FractionalIdeal R⁰ K
hI : I ≠ 0
hI' : I' ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
a : R
J : Ideal R
ha : a ≠ 0
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
⊢ Associates.mk (Ideal.span {a}) ≠ 0

Tactic:
rw [ne_eq, Associates.mk_eq_zero, Ideal.zero_eq_bot, Ideal.span_singleton_eq_bot]

Result:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I I' : FractionalIdeal R⁰ K
hI : I ≠ 0
hI' : I' ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
a : R
J : Ideal R
ha : a ≠ 0
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
⊢ ¬a = 0

Proof state:
case intro.intro.intro.intro.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I I' : FractionalIdeal R⁰ K
hI : I ≠ 0
hI' : I' ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
a : R
J : Ideal R
ha : a ≠ 0
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
ha_ne_zero : Associates.mk (Ideal.span {a}) ≠ 0
hJ_ne_zero : Associates.mk J ≠ 0
a' : R
J' : Ideal R
ha' : a' ≠ 0
haJ' : I' = spanSingleton R⁰ ((algebraMap R K) a')⁻¹ * ↑J'
ha'_ne_zero : Associates.mk (Ideal.span {a'}) ≠ 0
hJ'_ne_zero : Associates.mk J' ≠ 0
⊢ count K v (I * I') = count K v I + count K v I'

Tactic:
have h_prod : I * I' = spanSingleton R⁰ ((algebraMap R K) (a * a'))⁻¹ * ↑(J * J') := by
  rw [haJ, haJ', mul_assoc, mul_comm (J : FractionalIdeal R⁰ K), mul_assoc, ← mul_assoc,
    spanSingleton_mul_spanSingleton, coeIdeal_mul, RingHom.map_mul, mul_inv,
    mul_comm (J : FractionalIdeal R⁰ K)]

Result:
case intro.intro.intro.intro.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I I' : FractionalIdeal R⁰ K
hI : I ≠ 0
hI' : I' ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
a : R
J : Ideal R
ha : a ≠ 0
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
ha_ne_zero : Associates.mk (Ideal.span {a}) ≠ 0
hJ_ne_zero : Associates.mk J ≠ 0
a' : R
J' : Ideal R
ha' : a' ≠ 0
haJ' : I' = spanSingleton R⁰ ((algebraMap R K) a')⁻¹ * ↑J'
ha'_ne_zero : Associates.mk (Ideal.span {a'}) ≠ 0
hJ'_ne_zero : Associates.mk J' ≠ 0
h_prod : I * I' = spanSingleton R⁰ ((algebraMap R K) (a * a'))⁻¹ * ↑(J * J')
⊢ count K v (I * I') = count K v I + count K v I'

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I I' : FractionalIdeal R⁰ K
hI : I ≠ 0
hI' : I' ≠ 0
⊢ Irreducible (Associates.mk v.asIdeal)

Tactic:
apply v.associates_irreducible

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I I' : FractionalIdeal R⁰ K
hI : I ≠ 0
hI' : I' ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
a : R
J : Ideal R
ha : a ≠ 0
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
ha_ne_zero : Associates.mk (Ideal.span {a}) ≠ 0
hJ_ne_zero : Associates.mk J ≠ 0
a' : R
J' : Ideal R
ha' : a' ≠ 0
haJ' : I' = spanSingleton R⁰ ((algebraMap R K) a')⁻¹ * ↑J'
⊢ count K v (I * I') = count K v I + count K v I'

Tactic:
have ha'_ne_zero : Associates.mk (Ideal.span {a'} : Ideal R) ≠ 0 := by
  rw [ne_eq, Associates.mk_eq_zero, Ideal.zero_eq_bot, Ideal.span_singleton_eq_bot]; exact ha'

Result:
case intro.intro.intro.intro.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I I' : FractionalIdeal R⁰ K
hI : I ≠ 0
hI' : I' ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
a : R
J : Ideal R
ha : a ≠ 0
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
ha_ne_zero : Associates.mk (Ideal.span {a}) ≠ 0
hJ_ne_zero : Associates.mk J ≠ 0
a' : R
J' : Ideal R
ha' : a' ≠ 0
haJ' : I' = spanSingleton R⁰ ((algebraMap R K) a')⁻¹ * ↑J'
ha'_ne_zero : Associates.mk (Ideal.span {a'}) ≠ 0
⊢ count K v (I * I') = count K v I + count K v I'

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I I' : FractionalIdeal R⁰ K
hI : I ≠ 0
hI' : I' ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
⊢ count K v (I * I') = count K v I + count K v I'

Tactic:
obtain ⟨a, J, ha, haJ⟩ := exists_eq_spanSingleton_mul I

Result:
case intro.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I I' : FractionalIdeal R⁰ K
hI : I ≠ 0
hI' : I' ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
a : R
J : Ideal R
ha : a ≠ 0
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
⊢ count K v (I * I') = count K v I + count K v I'

Proof state:
case intro.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I I' : FractionalIdeal R⁰ K
hI : I ≠ 0
hI' : I' ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
a : R
J : Ideal R
ha : a ≠ 0
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
ha_ne_zero : Associates.mk (Ideal.span {a}) ≠ 0
hJ_ne_zero : Associates.mk J ≠ 0
⊢ count K v (I * I') = count K v I + count K v I'

Tactic:
obtain ⟨a', J', ha', haJ'⟩ := exists_eq_spanSingleton_mul I'

Result:
case intro.intro.intro.intro.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I I' : FractionalIdeal R⁰ K
hI : I ≠ 0
hI' : I' ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
a : R
J : Ideal R
ha : a ≠ 0
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
ha_ne_zero : Associates.mk (Ideal.span {a}) ≠ 0
hJ_ne_zero : Associates.mk J ≠ 0
a' : R
J' : Ideal R
ha' : a' ≠ 0
haJ' : I' = spanSingleton R⁰ ((algebraMap R K) a')⁻¹ * ↑J'
⊢ count K v (I * I') = count K v I + count K v I'