awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDedekindDomain R
v : HeightOneSpectrum R
I J I' J' : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
H_1 : I * J' = I' * J
h : J ≤ I
h' : J' ≤ I'
hJ' : J' ≠ 0
hI : I ≠ 0
this : J' ⊓ spanSingleton R⁰ (I'.divMod I J') * I = spanSingleton R⁰ (I'.divMod I J') * J
H :
  Submodule.map (σ₁₂ := RingHom.id R) ((Algebra.lsmul R R K : (a : K) → Module.End R K) (I'.divMod I J'))
      (↑I : Submodule R K) =
    (↑(spanSingleton R⁰ (I'.divMod I J')) : Submodule R K) * (↑I : Submodule R K)
refine_4 :
  (↑I' : Submodule R K) ≤
    (↑J' : Submodule R K) ⊔ (↑(spanSingleton R⁰ (I'.divMod I J')) : Submodule R K) * (↑I : Submodule R K)
refine_4₁ : (↑(spanSingleton R⁰ (I'.divMod I J')) : Submodule R K) * (↑I : Submodule R K) ≤ (↑I' : Submodule R K)
⊢ Surjective.{u_2 + 1, u_2 + 1} (α :=
    ↥(↑I : Submodule R K) ⧸ Submodule.comap (↑I : Submodule R K).subtype (↑J : Submodule R K)) (β :=
    ↥(↑I' : Submodule R K) ⧸ Submodule.comap (↑I' : Submodule R K).subtype (↑J' : Submodule R K))
    (⇑((Submodule.comap (↑I : Submodule R K).subtype (↑J : Submodule R K)).mapQ
          (Submodule.comap (↑I' : Submodule R K).subtype (↑J' : Submodule R K))
          (LinearMap.restrict ((Algebra.lsmul R R K : (a : K) → Module.End R K) (I'.divMod I J')) ⋯) ⋯) :
      (a : ↥(↑I : Submodule R K) ⧸ Submodule.comap (↑I : Submodule R K).subtype (↑J : Submodule R K)) →
        ↥(↑I' : Submodule R K) ⧸ Submodule.comap (↑I' : Submodule R K).subtype (↑J' : Submodule R K))
have refine_4₂ : (↑J' : Submodule R K) ≤ (↑I' : Submodule R K)
Tactic: rw [← LinearMap.range_eq_top, Submodule.mapQ, Submodule.range_liftQ,
      LinearMap.range_comp, LinearMap.restrict, LinearMap.range_codRestrict,
      LinearMap.range_domRestrict, ← top_le_iff, H,
      ← LinearMap.range_eq_top.mpr (Submodule.mkQ_surjective _),
      ← Submodule.map_top, Submodule.map_le_iff_le_comap, Submodule.comap_map_eq, Submodule.ker_mkQ,
      ← Submodule.map_le_map_iff_of_injective I'.coeToSubmodule.injective_subtype,
      Submodule.map_top, Submodule.map_sup,
      Submodule.map_comap_eq, Submodule.map_comap_eq, Submodule.range_subtype, sup_comm,
      inf_eq_right.mpr, inf_eq_right.mpr]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
S : Type u_3
inst_2 : CommRing S
inst_3 : Algebra S R
inst_4 : Algebra.IsIntegral S R
inst_5 : IsDomain S
inst_6 : Module.IsTorsionFree S R
p : Ideal S
inst_7 : p.IsMaximal
hp : p ≠ 0
⊢ Eq (α := Ideal R) (map (F := S →+* R) (algebraMap S R) p) (∏ P ∈ toFinset (p.primesOver R), P ^ p.ramificationIdx P)
have h : Ne.{u_1 + 1} (α := Ideal R) (map (F := S →+* R) (algebraMap S R) p) 0
Tactic: have h : map (algebraMap S R) p ≠ 0 := map_ne_bot_of_ne_bot hp
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
S : Type u_3
inst_2 : CommRing S
inst_3 : Algebra S R
inst_4 : Algebra.IsIntegral S R
inst_5 : IsDomain S
inst_6 : Module.IsTorsionFree S R
p : Ideal S
inst_7 : p.IsMaximal
hp : p ≠ 0
h : Ne.{u_1 + 1} (α := Ideal R) (map (F := S →+* R) (algebraMap S R) p) 0
⊢ Eq (α := Ideal R) (map (F := S →+* R) (algebraMap S R) p) (∏ P ∈ toFinset (p.primesOver R), P ^ p.ramificationIdx P)
have rw : Eq (α := Ideal R) (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing (map (F := S →+* R) (algebraMap S R) p))
  (∏ P ∈ toFinset (p.primesOver R), P ^ p.ramificationIdx P)
Tactic: rw [← finprod_heightOneSpectrum_factorization (I := p.map (algebraMap S R)) h]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
S : Type u_3
inst_2 : CommRing S
inst_3 : Algebra S R
inst_4 : Algebra.IsIntegral S R
inst_5 : IsDomain S
inst_6 : Module.IsTorsionFree S R
p : Ideal S
inst_7 : p.IsMaximal
hp : p ≠ 0
h : Ne.{u_1 + 1} (α := Ideal R) (map (F := S →+* R) (algebraMap S R) p) 0
hF : Fintype (↑{v : HeightOneSpectrum R | v.asIdeal ∣ map (F := S →+* R) (algebraMap S R) p} : Type u_1) :=
  ⋯.fintype (s := {v : HeightOneSpectrum R | v.asIdeal ∣ map (F := S →+* R) (algebraMap S R) p})
⊢ Eq (α := Ideal R) (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing (map (F := S →+* R) (algebraMap S R) p))
    (∏ P ∈ toFinset (p.primesOver R), P ^ p.ramificationIdx P)
have rw : Eq.{u_1 + 1} (α := Ideal R)
  (∏ i : (↑{v : HeightOneSpectrum R | v.asIdeal ∣ map (algebraMap S R) p} : Type u_1),
    (↑i : HeightOneSpectrum R).maxPowDividing (map (F := S →+* R) (algebraMap S R) p))
  (∏ i : (↑(p.primesOver R) : Type u_1), (↑i : Ideal R) ^ p.ramificationIdx (↑i : Ideal R))
Tactic: rw [finprod_eq_finsetProd_of_mulSupport_subset
    (s := {v | v.asIdeal ∣ p.map (algebraMap S R)}.toFinset), ← Finset.prod_set_coe,
    ← Finset.prod_set_coe]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
S : Type u_3
inst_2 : CommRing S
inst_3 : Algebra S R
inst_4 : Algebra.IsIntegral S R
inst_5 : IsDomain S
inst_6 : Module.IsTorsionFree S R
p : Ideal S
inst_7 : p.IsMaximal
hp : p ≠ 0
h : Ne.{u_1 + 1} (α := Ideal R) (map (F := S →+* R) (algebraMap S R) p) 0
hF : Fintype (↑{v : HeightOneSpectrum R | v.asIdeal ∣ map (F := S →+* R) (algebraMap S R) p} : Type u_1) :=
  ⋯.fintype (s := {v : HeightOneSpectrum R | v.asIdeal ∣ map (F := S →+* R) (algebraMap S R) p})
rw :
  Eq.{u_1 + 1} (α := Ideal R)
    (∏ i : (↑{v : HeightOneSpectrum R | v.asIdeal ∣ map (algebraMap S R) p} : Type u_1),
      (↑i : HeightOneSpectrum R).maxPowDividing (map (F := S →+* R) (algebraMap S R) p))
    (∏ i : (↑(p.primesOver R) : Type u_1), (↑i : Ideal R) ^ p.ramificationIdx (↑i : Ideal R))
⊢ Eq (α := Ideal R) (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing (map (F := S →+* R) (algebraMap S R) p))
    (∏ P ∈ toFinset (p.primesOver R), P ^ p.ramificationIdx P)
have h₁ : (mulSupport (M := Ideal R) fun (v : HeightOneSpectrum R) ↦ v.maxPowDividing (map (F := S →+* R) (algebraMap S R) p)) ⊆
  (↑(toFinset {v : HeightOneSpectrum R | v.asIdeal ∣ map (F := S →+* R) (algebraMap S R) p}) :
    Set (HeightOneSpectrum R))
Tactic: rw [finprod_eq_finsetProd_of_mulSupport_subset
    (s := {v | v.asIdeal ∣ p.map (algebraMap S R)}.toFinset), ← Finset.prod_set_coe,
    ← Finset.prod_set_coe]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
S : Type u_3
inst_2 : CommRing S
inst_3 : Algebra S R
inst_4 : Algebra.IsIntegral S R
inst_5 : IsDomain S
inst_6 : Module.IsTorsionFree S R
p : Ideal S
inst_7 : p.IsMaximal
hp : p ≠ 0
h : Ne.{u_1 + 1} (α := Ideal R) (map (F := S →+* R) (algebraMap S R) p) 0
hF : Fintype (↑{v : HeightOneSpectrum R | v.asIdeal ∣ map (F := S →+* R) (algebraMap S R) p} : Type u_1) :=
  ⋯.fintype (s := {v : HeightOneSpectrum R | v.asIdeal ∣ map (F := S →+* R) (algebraMap S R) p})
x : Fintype { v : HeightOneSpectrum R // v.asIdeal ∣ map (F := S →+* R) (algebraMap S R) p } := hF
⊢ Eq.{u_1 + 1} (α := Ideal R)
    (∏ i : (↑{v : HeightOneSpectrum R | v.asIdeal ∣ map (algebraMap S R) p} : Type u_1),
      (↑i : HeightOneSpectrum R).maxPowDividing (map (F := S →+* R) (algebraMap S R) p))
    (∏ i : (↑(p.primesOver R) : Type u_1), (↑i : Ideal R) ^ p.ramificationIdx (↑i : Ideal R))
have refine : ∀ (x : { v : HeightOneSpectrum R // v.asIdeal ∣ map (F := S →+* R) (algebraMap S R) p }) (v : HeightOneSpectrum R)
  (property : v.asIdeal ∣ map (F := S →+* R) (algebraMap S R) p),
  (↑(Subtype.mk (p := fun (v : HeightOneSpectrum R) ↦ v.asIdeal ∣ map (F := S →+* R) (algebraMap S R) p) v property) :
          HeightOneSpectrum R).maxPowDividing
      (map (F := S →+* R) (algebraMap S R) p) =
    HPow.hPow (α := Ideal R)
      (↑((equivPrimesOver R hp :
              (a : { v : HeightOneSpectrum R // v.asIdeal ∣ map (algebraMap S R) p }) → (↑(p.primesOver R) : Type u_1))
            (Subtype.mk (p := fun (v : HeightOneSpectrum R) ↦ v.asIdeal ∣ map (F := S →+* R) (algebraMap S R) p) v
              property)) :
        Ideal R)
      (ramificationIdx.{u_3, u_1} (S := R) p
        (↑((equivPrimesOver R hp :
                (a : { v : HeightOneSpectrum R // v.asIdeal ∣ map (algebraMap S R) p }) →
                  (↑(p.primesOver R) : Type u_1))
              (Subtype.mk (p := fun (v : HeightOneSpectrum R) ↦ v.asIdeal ∣ map (F := S →+* R) (algebraMap S R) p) v
                property)) :
          Ideal R))
Tactic: refine Fintype.prod_equiv (equivPrimesOver _ hp) _ _ fun ⟨v, _⟩ ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
S : Type u_3
inst_2 : CommRing S
inst_3 : Algebra S R
inst_4 : Algebra.IsIntegral S R
inst_5 : IsDomain S
inst_6 : Module.IsTorsionFree S R
p : Ideal S
inst_7 : p.IsMaximal
hp : p ≠ 0
⊢ Eq (α := Ideal R) (map (F := S →+* R) (algebraMap S R) p) (∏ P ∈ toFinset (p.primesOver R), P ^ p.ramificationIdx P)
have have : ∀ (h : Ne.{u_1 + 1} (α := Ideal R) (map (F := S →+* R) (algebraMap S R) p) 0),
  Eq (α := Ideal R) (map (F := S →+* R) (algebraMap S R) p) (∏ P ∈ toFinset (p.primesOver R), P ^ p.ramificationIdx P)
Tactic: classical
  have h : map (algebraMap S R) p ≠ 0 := map_ne_bot_of_ne_bot hp
  rw [← finprod_heightOneSpectrum_factorization (I := p.map (algebraMap S R)) h]
  let hF : Fintype {v : HeightOneSpectrum R | v.asIdeal ∣ map (algebraMap S R) p} :=
    (finite_factors h).fintype
  rw [finprod_eq_finsetProd_of_mulSupport_subset
    (s := {v | v.asIdeal ∣ p.map (algebraMap S R)}.toFinset), ← Finset.prod_set_coe,
    ← Finset.prod_set_coe]
  · let _ : Fintype {v : HeightOneSpectrum R // v.asIdeal ∣ map (algebraMap S R) p} := hF
    refine Fintype.prod_equiv (equivPrimesOver _ hp) _ _ fun ⟨v, _⟩ ↦ ?_
    simp [maxPowDividing_eq_pow_multiset_count _ h,
      ramificationIdx_eq_factors_count h v.isPrime v.ne_bot]
  · intro v hv
    simpa [maxPowDividing, Function.mem_mulSupport, IsPrime.ne_top _,
      Associates.count_ne_zero_iff_dvd h (irreducible v)] using hv
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
S : Type u_3
inst_2 : CommRing S
inst_3 : Algebra S R
inst_4 : Algebra.IsIntegral S R
inst_5 : IsDomain S
inst_6 : Module.IsTorsionFree S R
p : Ideal S
inst_7 : p.IsMaximal
hp : p ≠ 0
have have₁ have₂ :
  ∀ (h : Ne.{u_1 + 1} (α := Ideal R) (map (F := S →+* R) (algebraMap S R) p) 0),
    Eq (α := Ideal R) (map (F := S →+* R) (algebraMap S R) p) (∏ P ∈ toFinset (p.primesOver R), P ^ p.ramificationIdx P)
⊢ Eq (α := Ideal R) (map (F := S →+* R) (algebraMap S R) p) (∏ P ∈ toFinset (p.primesOver R), P ^ p.ramificationIdx P)
have have₃ : ∀ (h : Ne.{u_1 + 1} (α := Ideal R) (map (F := S →+* R) (algebraMap S R) p) 0),
  Eq (α := Ideal R) (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing (map (F := S →+* R) (algebraMap S R) p))
    (∏ P ∈ toFinset (p.primesOver R), P ^ p.ramificationIdx P)
Tactic: classical
  have h : map (algebraMap S R) p ≠ 0 := map_ne_bot_of_ne_bot hp
  rw [← finprod_heightOneSpectrum_factorization (I := p.map (algebraMap S R)) h]
  let hF : Fintype {v : HeightOneSpectrum R | v.asIdeal ∣ map (algebraMap S R) p} :=
    (finite_factors h).fintype
  rw [finprod_eq_finsetProd_of_mulSupport_subset
    (s := {v | v.asIdeal ∣ p.map (algebraMap S R)}.toFinset), ← Finset.prod_set_coe,
    ← Finset.prod_set_coe]
  · let _ : Fintype {v : HeightOneSpectrum R // v.asIdeal ∣ map (algebraMap S R) p} := hF
    refine Fintype.prod_equiv (equivPrimesOver _ hp) _ _ fun ⟨v, _⟩ ↦ ?_
    simp [maxPowDividing_eq_pow_multiset_count _ h,
      ramificationIdx_eq_factors_count h v.isPrime v.ne_bot]
  · intro v hv
    simpa [maxPowDividing, Function.mem_mulSupport, IsPrime.ne_top _,
      Associates.count_ne_zero_iff_dvd h (irreducible v)] using hv
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
S : Type u_3
inst_2 : CommRing S
inst_3 : Algebra S R
inst_4 : Algebra.IsIntegral S R
inst_5 : IsDomain S
inst_6 : Module.IsTorsionFree S R
p : Ideal S
inst_7 : p.IsMaximal
hp : p ≠ 0
have have₁ have₂ :
  ∀ (h : Ne.{u_1 + 1} (α := Ideal R) (map (F := S →+* R) (algebraMap S R) p) 0),
    Eq (α := Ideal R) (map (F := S →+* R) (algebraMap S R) p) (∏ P ∈ toFinset (p.primesOver R), P ^ p.ramificationIdx P)
have₃ have₄ :
  ∀ (h : Ne.{u_1 + 1} (α := Ideal R) (map (F := S →+* R) (algebraMap S R) p) 0),
    Eq (α := Ideal R) (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing (map (F := S →+* R) (algebraMap S R) p))
      (∏ P ∈ toFinset (p.primesOver R), P ^ p.ramificationIdx P)
⊢ Eq (α := Ideal R) (map (F := S →+* R) (algebraMap S R) p) (∏ P ∈ toFinset (p.primesOver R), P ^ p.ramificationIdx P)
have have₅ : ∀ (h : Ne.{u_1 + 1} (α := Ideal R) (map (F := S →+* R) (algebraMap S R) p) 0),
  let hF := sorry.fintype (s := {v : HeightOneSpectrum R | v.asIdeal ∣ map (F := S →+* R) (algebraMap S R) p});
  Eq.{u_1 + 1} (α := Ideal R)
    (∏ i : (↑{v : HeightOneSpectrum R | v.asIdeal ∣ map (algebraMap S R) p} : Type u_1),
      (↑i : HeightOneSpectrum R).maxPowDividing (map (F := S →+* R) (algebraMap S R) p))
    (∏ i : (↑(p.primesOver R) : Type u_1), (↑i : Ideal R) ^ p.ramificationIdx (↑i : Ideal R))
Tactic: classical
  have h : map (algebraMap S R) p ≠ 0 := map_ne_bot_of_ne_bot hp
  rw [← finprod_heightOneSpectrum_factorization (I := p.map (algebraMap S R)) h]
  let hF : Fintype {v : HeightOneSpectrum R | v.asIdeal ∣ map (algebraMap S R) p} :=
    (finite_factors h).fintype
  rw [finprod_eq_finsetProd_of_mulSupport_subset
    (s := {v | v.asIdeal ∣ p.map (algebraMap S R)}.toFinset), ← Finset.prod_set_coe,
    ← Finset.prod_set_coe]
  · let _ : Fintype {v : HeightOneSpectrum R // v.asIdeal ∣ map (algebraMap S R) p} := hF
    refine Fintype.prod_equiv (equivPrimesOver _ hp) _ _ fun ⟨v, _⟩ ↦ ?_
    simp [maxPowDividing_eq_pow_multiset_count _ h,
      ramificationIdx_eq_factors_count h v.isPrime v.ne_bot]
  · intro v hv
    simpa [maxPowDividing, Function.mem_mulSupport, IsPrime.ne_top _,
      Associates.count_ne_zero_iff_dvd h (irreducible v)] using hv
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
S : Type u_3
inst_2 : CommRing S
inst_3 : Algebra S R
inst_4 : Algebra.IsIntegral S R
inst_5 : IsDomain S
inst_6 : Module.IsTorsionFree S R
p : Ideal S
inst_7 : p.IsMaximal
hp : p ≠ 0
have have₁ have₂ :
  ∀ (h : Ne.{u_1 + 1} (α := Ideal R) (map (F := S →+* R) (algebraMap S R) p) 0),
    Eq (α := Ideal R) (map (F := S →+* R) (algebraMap S R) p) (∏ P ∈ toFinset (p.primesOver R), P ^ p.ramificationIdx P)
have₃ have₄ :
  ∀ (h : Ne.{u_1 + 1} (α := Ideal R) (map (F := S →+* R) (algebraMap S R) p) 0),
    Eq (α := Ideal R) (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing (map (F := S →+* R) (algebraMap S R) p))
      (∏ P ∈ toFinset (p.primesOver R), P ^ p.ramificationIdx P)
have₅ :
  ∀ (h : Ne.{u_1 + 1} (α := Ideal R) (map (F := S →+* R) (algebraMap S R) p) 0),
    let hF := ⋯.fintype (s := {v : HeightOneSpectrum R | v.asIdeal ∣ map (F := S →+* R) (algebraMap S R) p});
    Eq.{u_1 + 1} (α := Ideal R)
      (∏ i : (↑{v : HeightOneSpectrum R | v.asIdeal ∣ map (algebraMap S R) p} : Type u_1),
        (↑i : HeightOneSpectrum R).maxPowDividing (map (F := S →+* R) (algebraMap S R) p))
      (∏ i : (↑(p.primesOver R) : Type u_1), (↑i : Ideal R) ^ p.ramificationIdx (↑i : Ideal R))
⊢ Eq (α := Ideal R) (map (F := S →+* R) (algebraMap S R) p) (∏ P ∈ toFinset (p.primesOver R), P ^ p.ramificationIdx P)
have h : ∀ (h : Ne.{u_1 + 1} (α := Ideal R) (map (F := S →+* R) (algebraMap S R) p) 0),
  let hF := sorry.fintype (s := {v : HeightOneSpectrum R | v.asIdeal ∣ map (F := S →+* R) (algebraMap S R) p});
  (mulSupport (M := Ideal R) fun (v : HeightOneSpectrum R) ↦ v.maxPowDividing (map (F := S →+* R) (algebraMap S R) p)) ⊆
    (↑(toFinset {v : HeightOneSpectrum R | v.asIdeal ∣ map (F := S →+* R) (algebraMap S R) p}) :
      Set (HeightOneSpectrum R))
Tactic: classical
  have h : map (algebraMap S R) p ≠ 0 := map_ne_bot_of_ne_bot hp
  rw [← finprod_heightOneSpectrum_factorization (I := p.map (algebraMap S R)) h]
  let hF : Fintype {v : HeightOneSpectrum R | v.asIdeal ∣ map (algebraMap S R) p} :=
    (finite_factors h).fintype
  rw [finprod_eq_finsetProd_of_mulSupport_subset
    (s := {v | v.asIdeal ∣ p.map (algebraMap S R)}.toFinset), ← Finset.prod_set_coe,
    ← Finset.prod_set_coe]
  · let _ : Fintype {v : HeightOneSpectrum R // v.asIdeal ∣ map (algebraMap S R) p} := hF
    refine Fintype.prod_equiv (equivPrimesOver _ hp) _ _ fun ⟨v, _⟩ ↦ ?_
    simp [maxPowDividing_eq_pow_multiset_count _ h,
      ramificationIdx_eq_factors_count h v.isPrime v.ne_bot]
  · intro v hv
    simpa [maxPowDividing, Function.mem_mulSupport, IsPrime.ne_top _,
      Associates.count_ne_zero_iff_dvd h (irreducible v)] using hv
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (hypothesis)
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
p : HeightOneSpectrum R
⊢ Multiset.count p.asIdeal (normalizedFactors I) = multiplicity p.asIdeal I
have this : emultiplicity p.asIdeal I =
  (↑(Multiset.count ((normalize : (a : Ideal R) → Ideal R) p.asIdeal) (normalizedFactors I)) : ℕ∞)
Tactic: have := emultiplicity_eq_count_normalizedFactors (irreducible p) hI
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (hypothesis)
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
p : HeightOneSpectrum R
this :
  emultiplicity p.asIdeal I =
    (↑(Multiset.count ((normalize : (a : Ideal R) → Ideal R) p.asIdeal) (normalizedFactors I)) : ℕ∞)
⊢ Multiset.count p.asIdeal (normalizedFactors I) = multiplicity p.asIdeal I
have this₁ : emultiplicity p.asIdeal I = (↑(Multiset.count p.asIdeal (normalizedFactors I)) : ℕ∞)
Tactic: rw [normalize_eq p.asIdeal] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
p : HeightOneSpectrum R
this : emultiplicity p.asIdeal I = (↑(Multiset.count p.asIdeal (normalizedFactors I)) : ℕ∞)
⊢ Multiset.count p.asIdeal (normalizedFactors I) = multiplicity p.asIdeal I
have apply_fun : Eq (α := ℕ∞) (↑(Multiset.count p.asIdeal (normalizedFactors I)) : ℕ∞) (↑(multiplicity p.asIdeal I) : ℕ∞)
Tactic: apply_fun ((↑) : ℕ → ℕ∞) using CharZero.cast_injective
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
p : HeightOneSpectrum R
this : emultiplicity p.asIdeal I = (↑(Multiset.count p.asIdeal (normalizedFactors I)) : ℕ∞)
⊢ Eq (α := ℕ∞) (↑(Multiset.count p.asIdeal (normalizedFactors I)) : ℕ∞) (↑(multiplicity p.asIdeal I) : ℕ∞)
have rw : emultiplicity p.asIdeal I = (↑(multiplicity p.asIdeal I) : ℕ∞)
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
p : HeightOneSpectrum R
⊢ p.maxPowDividing I = p.asIdeal ^ multiplicity p.asIdeal I
have rw : p.asIdeal ^ Multiset.count p.asIdeal (normalizedFactors I) = p.asIdeal ^ multiplicity p.asIdeal I
Tactic: rw [maxPowDividing_eq_pow_multiset_count _ hI, count_normalizedFactors_eq_multiplicity hI]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
p : HeightOneSpectrum R
rw : p.asIdeal ^ Multiset.count p.asIdeal (normalizedFactors I) = p.asIdeal ^ multiplicity p.asIdeal I
⊢ p.maxPowDividing I = p.asIdeal ^ multiplicity p.asIdeal I
have rw₁ : p.asIdeal ^ multiplicity p.asIdeal I = p.asIdeal ^ multiplicity p.asIdeal I
Tactic: rw [maxPowDividing_eq_pow_multiset_count _ hI, count_normalizedFactors_eq_multiplicity hI]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
p : HeightOneSpectrum R
⊢ p.maxPowDividing I = p.asIdeal ^ multiplicity p.asIdeal I
have rw : p.asIdeal ^ Multiset.count p.asIdeal (normalizedFactors I) = p.asIdeal ^ multiplicity p.asIdeal I
Tactic: classical
  rw [maxPowDividing_eq_pow_multiset_count _ hI, count_normalizedFactors_eq_multiplicity hI]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
p : HeightOneSpectrum R
rw : p.asIdeal ^ Multiset.count p.asIdeal (normalizedFactors I) = p.asIdeal ^ multiplicity p.asIdeal I
⊢ p.maxPowDividing I = p.asIdeal ^ multiplicity p.asIdeal I
have rw₁ : p.asIdeal ^ multiplicity p.asIdeal I = p.asIdeal ^ multiplicity p.asIdeal I
Tactic: classical
  rw [maxPowDividing_eq_pow_multiset_count _ hI, count_normalizedFactors_eq_multiplicity hI]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
p : HeightOneSpectrum R
⊢ (factorization I : (a : Ideal R) → ℕ) p.asIdeal = multiplicity p.asIdeal I
have rw : Multiset.count p.asIdeal (normalizedFactors I) = multiplicity p.asIdeal I
Tactic: rw [factorization_eq_count, count_normalizedFactors_eq_multiplicity hI]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
p : HeightOneSpectrum R
rw : Multiset.count p.asIdeal (normalizedFactors I) = multiplicity p.asIdeal I
⊢ (factorization I : (a : Ideal R) → ℕ) p.asIdeal = multiplicity p.asIdeal I
have rw₁ : multiplicity p.asIdeal I = multiplicity p.asIdeal I
Tactic: rw [factorization_eq_count, count_normalizedFactors_eq_multiplicity hI]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsDedekindDomain R
p : HeightOneSpectrum R
I J : Ideal R
h : J ≤ I
hJ : J ≠ ⊥
⊢ multiplicity p.asIdeal I ≤ multiplicity p.asIdeal J
have rw : Multiset.count p.asIdeal (normalizedFactors I) ≤ Multiset.count p.asIdeal (normalizedFactors J)
Tactic: rw [← count_normalizedFactors_eq_multiplicity hJ,
    ← count_normalizedFactors_eq_multiplicity <| ne_bot_of_le_ne_bot hJ h]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsDedekindDomain R
p : HeightOneSpectrum R
I J : Ideal R
hI : I ≠ ⊥
hJ : J ≠ ⊥
⊢ multiplicity p.asIdeal (I ⊔ J) = min (multiplicity p.asIdeal I) (multiplicity p.asIdeal J)
have rw : count p.asIdeal (normalizedFactors (normalizedFactors I ∩ normalizedFactors J).prod) =
  min (count p.asIdeal (normalizedFactors I)) (count p.asIdeal (normalizedFactors J))
Tactic: rw [Ideal.sup_eq_prod_inf_factors hI hJ, ← count_normalizedFactors_eq_multiplicity ?h,
    ← count_normalizedFactors_eq_multiplicity hI, ← count_normalizedFactors_eq_multiplicity hJ]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsDedekindDomain R
p : HeightOneSpectrum R
I J : Ideal R
hI : I ≠ ⊥
hJ : J ≠ ⊥
rw :
  count p.asIdeal (normalizedFactors (normalizedFactors I ∩ normalizedFactors J).prod) =
    min (count p.asIdeal (normalizedFactors I)) (count p.asIdeal (normalizedFactors J))
⊢ multiplicity p.asIdeal (I ⊔ J) = min (multiplicity p.asIdeal I) (multiplicity p.asIdeal J)
have rw₁ : (normalizedFactors I ∩ normalizedFactors J).prod ≠ ⊥
Tactic: rw [Ideal.sup_eq_prod_inf_factors hI hJ, ← count_normalizedFactors_eq_multiplicity ?h,
    ← count_normalizedFactors_eq_multiplicity hI, ← count_normalizedFactors_eq_multiplicity hJ]