awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
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
x_1 : { 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:
simp [maxPowDividing_eq_pow_multiset_count _ h,
      ramificationIdx_eq_factors_count h v.isPrime v.ne_bot]

Premises used: IsDedekindDomain.HeightOneSpectrum.ne_bot, Ideal.IsDedekindDomain.ramificationIdx_eq_factors_count, IsDedekindDomain.HeightOneSpectrum.maxPowDividing_eq_pow_multiset_count, IsDedekindDomain.HeightOneSpectrum.isPrime
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
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})
v : HeightOneSpectrum R
hv :
  Membership.mem (γ := Set (HeightOneSpectrum R))
    (mulSupport (M := Ideal R) fun (v : HeightOneSpectrum R) ↦ v.maxPowDividing (map (F := S →+* R) (algebraMap S R) p))
    v
⊢ v ∈
    (↑(toFinset {v : HeightOneSpectrum R | v.asIdeal ∣ map (F := S →+* R) (algebraMap S R) p}) :
      Set (HeightOneSpectrum R))

Tactic:
simpa [maxPowDividing, Function.mem_mulSupport, IsPrime.ne_top _,
      Associates.count_ne_zero_iff_dvd h (irreducible v)] using hv

Premises used: IsDedekindDomain.HeightOneSpectrum.irreducible, Function.mem_mulSupport, Associates.count_ne_zero_iff_dvd, Ideal.IsPrime.ne_top, IsDedekindDomain.HeightOneSpectrum.maxPowDividing
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
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))
h h₁ :
  ∀ (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});
    (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))
⊢ 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

Premises used: Function.mem_mulSupport, Finset.prod_set_coe, Ideal.IsPrime.ne_top, IsDedekindDomain.HeightOneSpectrum.maxPowDividing, finprod_eq_finsetProd_of_mulSupport_subset
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
p : HeightOneSpectrum R
⊢ 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
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
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)) : ℕ∞)
⊢ emultiplicity p.asIdeal I = (↑(Multiset.count p.asIdeal (normalizedFactors I)) : ℕ∞)

Tactic:
rw [normalize_eq p.asIdeal] at this

Premises used: IsDedekindDomain.HeightOneSpectrum.asIdeal, normalize_eq
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
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)) : ℕ∞)
⊢ Injective (β := ℕ∞) Nat.cast

Tactic:
CharZero.cast_injective

Premises used: CharZero.cast_injective
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
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)) : ℕ∞)
apply_fun : Eq (α := ℕ∞) (↑(Multiset.count p.asIdeal (normalizedFactors I)) : ℕ∞) (↑(multiplicity p.asIdeal I) : ℕ∞)
⊢ Multiset.count p.asIdeal (normalizedFactors I) = multiplicity p.asIdeal I

Tactic:
apply_fun ((↑) : ℕ → ℕ∞) using CharZero.cast_injective

Premises used: Nat.cast, CharZero.cast_injective
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
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)) : ℕ∞)
rw : emultiplicity p.asIdeal I = (↑(multiplicity p.asIdeal I) : ℕ∞)
⊢ Eq (α := ℕ∞) (↑(Multiset.count p.asIdeal (normalizedFactors I)) : ℕ∞) (↑(multiplicity p.asIdeal I) : ℕ∞)

Tactic:
rw [← this]
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
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)) : ℕ∞)
⊢ emultiplicity p.asIdeal I = (↑(multiplicity p.asIdeal I) : ℕ∞)

Tactic:
(finiteMultiplicity_of_emultiplicity_eq_natCast this).emultiplicity_eq_multiplicity

Premises used: FiniteMultiplicity.emultiplicity_eq_multiplicity, finiteMultiplicity_of_emultiplicity_eq_natCast
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
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)) : ℕ∞)
⊢ emultiplicity p.asIdeal I = (↑(multiplicity p.asIdeal I) : ℕ∞)

Tactic:
exact (finiteMultiplicity_of_emultiplicity_eq_natCast this).emultiplicity_eq_multiplicity

Premises used: FiniteMultiplicity.emultiplicity_eq_multiplicity, finiteMultiplicity_of_emultiplicity_eq_natCast
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
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
rw₁ rw₂ : p.asIdeal ^ multiplicity p.asIdeal I = p.asIdeal ^ multiplicity p.asIdeal I
⊢ p.maxPowDividing I = p.asIdeal ^ multiplicity p.asIdeal I

Tactic:
rw [maxPowDividing_eq_pow_multiset_count _ hI, count_normalizedFactors_eq_multiplicity hI]

Premises used: IsDedekindDomain.HeightOneSpectrum.count_normalizedFactors_eq_multiplicity, IsDedekindDomain.HeightOneSpectrum.maxPowDividing_eq_pow_multiset_count
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
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
rw₁ rw₂ : p.asIdeal ^ multiplicity p.asIdeal I = p.asIdeal ^ multiplicity p.asIdeal I
⊢ p.maxPowDividing I = p.asIdeal ^ multiplicity p.asIdeal I

Tactic:
classical
  rw [maxPowDividing_eq_pow_multiset_count _ hI, count_normalizedFactors_eq_multiplicity hI]

Premises used: IsDedekindDomain.HeightOneSpectrum.count_normalizedFactors_eq_multiplicity, IsDedekindDomain.HeightOneSpectrum.maxPowDividing_eq_pow_multiset_count
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
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
rw₁ rw₂ : multiplicity p.asIdeal I = multiplicity p.asIdeal I
⊢ (factorization I : (a : Ideal R) → ℕ) p.asIdeal = multiplicity p.asIdeal I

Tactic:
rw [factorization_eq_count, count_normalizedFactors_eq_multiplicity hI]

Premises used: IsDedekindDomain.HeightOneSpectrum.count_normalizedFactors_eq_multiplicity, factorization_eq_count
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_3
inst : CommSemiring R
I : Ideal R
⊢ emultiplicity I ⊥ = ⊤

Tactic:
Submodule.zero_eq_bot (R := R) (M := R) ▸ emultiplicity_zero I

Premises used: Eq.rec, emultiplicity_zero, Submodule.zero_eq_bot
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
⊢ ∏ᶠ (p : HeightOneSpectrum R), p.asIdeal ^ multiplicity p.asIdeal I = I

Tactic:
simpa only [maxPowDividing_eq_pow_multiplicity hI]
    using finprod_heightOneSpectrum_factorization hI

Premises used: IsDedekindDomain.HeightOneSpectrum.maxPowDividing_eq_pow_multiplicity, Ideal.finprod_heightOneSpectrum_factorization
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsDedekindDomain R
p : HeightOneSpectrum R
I J : Ideal R
h : J ≤ I
hJ : J ≠ ⊥
rw : Multiset.count p.asIdeal (normalizedFactors I) ≤ Multiset.count p.asIdeal (normalizedFactors J)
⊢ multiplicity p.asIdeal I ≤ multiplicity p.asIdeal J

Tactic:
rw [← count_normalizedFactors_eq_multiplicity hJ,
    ← count_normalizedFactors_eq_multiplicity <| ne_bot_of_le_ne_bot hJ h]

Premises used: ne_bot_of_le_ne_bot, IsDedekindDomain.HeightOneSpectrum.count_normalizedFactors_eq_multiplicity
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsDedekindDomain R
p : HeightOneSpectrum R
I J : Ideal R
h : J ≤ I
hJ : J ≠ ⊥
⊢ Multiset.count p.asIdeal (normalizedFactors I) ≤ Multiset.count p.asIdeal (normalizedFactors J)

Tactic:
Ideal.count_le_of_ideal_ge h hJ _

Premises used: Ideal.count_le_of_ideal_ge
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsDedekindDomain R
p : HeightOneSpectrum R
I J : Ideal R
h : J ≤ I
hJ : J ≠ ⊥
⊢ Multiset.count p.asIdeal (normalizedFactors I) ≤ Multiset.count p.asIdeal (normalizedFactors J)

Tactic:
exact Ideal.count_le_of_ideal_ge h hJ _

Premises used: Ideal.count_le_of_ideal_ge
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
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))
rw₁ : (normalizedFactors I ∩ normalizedFactors J).prod ≠ ⊥
⊢ multiplicity p.asIdeal (I ⊔ J) = min (multiplicity p.asIdeal I) (multiplicity p.asIdeal 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]

Premises used: Ideal.sup_eq_prod_inf_factors, IsDedekindDomain.HeightOneSpectrum.count_normalizedFactors_eq_multiplicity
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsDedekindDomain R
p : HeightOneSpectrum R
I J : Ideal R
hI : I ≠ ⊥
hJ : J ≠ ⊥
⊢ (normalizedFactors I ∩ normalizedFactors J).prod ≠ ⊥

Tactic:
prod_inter_normalizedFactors_ne_zero I J

Premises used: UniqueFactorizationMonoid.prod_inter_normalizedFactors_ne_zero
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsDedekindDomain R
p : HeightOneSpectrum R
I J : Ideal R
hI : I ≠ ⊥
hJ : J ≠ ⊥
⊢ (normalizedFactors I ∩ normalizedFactors J).prod ≠ ⊥

Tactic:
exact prod_inter_normalizedFactors_ne_zero I J

Premises used: UniqueFactorizationMonoid.prod_inter_normalizedFactors_ne_zero
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsDedekindDomain R
p : HeightOneSpectrum R
I J : Ideal R
hI : I ≠ ⊥
hJ : J ≠ ⊥
⊢ (normalizedFactors I ∩ normalizedFactors J).prod ≠ ⊥

Tactic:
case h => exact prod_inter_normalizedFactors_ne_zero I J

Premises used: UniqueFactorizationMonoid.prod_inter_normalizedFactors_ne_zero
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
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 I ∩ normalizedFactors J) =
    min (count p.asIdeal (normalizedFactors I)) (count p.asIdeal (normalizedFactors J))
⊢ count p.asIdeal (normalizedFactors (normalizedFactors I ∩ normalizedFactors J).prod) =
    min (count p.asIdeal (normalizedFactors I)) (count p.asIdeal (normalizedFactors J))

Tactic:
rw [normalizedFactors_prod_inter_eq_inter]

Premises used: UniqueFactorizationMonoid.normalizedFactors_prod_inter_eq_inter
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsDedekindDomain R
p : HeightOneSpectrum R
I J : Ideal R
hI : I ≠ ⊥
hJ : J ≠ ⊥
⊢ count p.asIdeal (normalizedFactors I ∩ normalizedFactors J) =
    min (count p.asIdeal (normalizedFactors I)) (count p.asIdeal (normalizedFactors J))

Tactic:
count_inter ..

Premises used: Multiset.count_inter
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsDedekindDomain R
p : HeightOneSpectrum R
I J : Ideal R
hI : I ≠ ⊥
hJ : J ≠ ⊥
⊢ count p.asIdeal (normalizedFactors I ∩ normalizedFactors J) =
    min (count p.asIdeal (normalizedFactors I)) (count p.asIdeal (normalizedFactors J))

Tactic:
exact count_inter ..

Premises used: Multiset.count_inter
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsDedekindDomain R
p : HeightOneSpectrum R
I J : Ideal R
inl : emultiplicity p.asIdeal (⊥ ⊔ J) = min (emultiplicity p.asIdeal ⊥) (emultiplicity p.asIdeal J)
inr : ∀ (hI : I ≠ ⊥), emultiplicity p.asIdeal (I ⊔ J) = min (emultiplicity p.asIdeal I) (emultiplicity p.asIdeal J)
⊢ emultiplicity p.asIdeal (I ⊔ J) = min (emultiplicity p.asIdeal I) (emultiplicity p.asIdeal J)

Tactic:
rcases eq_or_ne I ⊥ with rfl | hI

Premises used: Bot.bot, eq_or_ne, rfl
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsDedekindDomain R
p : HeightOneSpectrum R
J : Ideal R
⊢ emultiplicity p.asIdeal (⊥ ⊔ J) = min (emultiplicity p.asIdeal ⊥) (emultiplicity p.asIdeal J)

Tactic:
simp
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsDedekindDomain R
p : HeightOneSpectrum R
I J : Ideal R
hI : I ≠ ⊥
inr : emultiplicity p.asIdeal (I ⊔ ⊥) = min (emultiplicity p.asIdeal I) (emultiplicity p.asIdeal ⊥)
inr₁ : ∀ (hJ : J ≠ ⊥), emultiplicity p.asIdeal (I ⊔ J) = min (emultiplicity p.asIdeal I) (emultiplicity p.asIdeal J)
⊢ emultiplicity p.asIdeal (I ⊔ J) = min (emultiplicity p.asIdeal I) (emultiplicity p.asIdeal J)

Tactic:
rcases eq_or_ne J ⊥ with rfl | hJ

Premises used: Bot.bot, eq_or_ne, rfl
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsDedekindDomain R
p : HeightOneSpectrum R
I : Ideal R
hI : I ≠ ⊥
⊢ emultiplicity p.asIdeal (I ⊔ ⊥) = min (emultiplicity p.asIdeal I) (emultiplicity p.asIdeal ⊥)

Tactic:
simp
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsDedekindDomain R
p : HeightOneSpectrum R
I J : Ideal R
hI : I ≠ ⊥
hJ : J ≠ ⊥
⊢ I ⊔ J ≠ ⊥

Tactic:
grind
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsDedekindDomain R
p : HeightOneSpectrum R
I J : Ideal R
hI : I ≠ ⊥
hJ : J ≠ ⊥
⊢ I ⊔ J ≠ ⊥

Tactic:
have : I ⊔ J ≠ ⊥ := by grind
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsDedekindDomain R
p : HeightOneSpectrum R
I J : Ideal R
hI : I ≠ ⊥
hJ : J ≠ ⊥
this : I ⊔ J ≠ ⊥
⊢ ∀ {I' : Ideal R} (h : I' ≠ ⊥), FiniteMultiplicity p.asIdeal I'

Tactic:
have H {I' : Ideal R} (h : I' ≠ ⊥) : FiniteMultiplicity p.asIdeal I' :=
    FiniteMultiplicity.of_prime_left (prime p) h
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsDedekindDomain R
p : HeightOneSpectrum R
I J : Ideal R
hI : I ≠ ⊥
hJ : J ≠ ⊥
this : I ⊔ J ≠ ⊥
H : ∀ {I' : Ideal R} (h : I' ≠ ⊥), FiniteMultiplicity p.asIdeal I'
inr :
  Eq (α := ℕ∞) (↑(min (multiplicity p.asIdeal I) (multiplicity p.asIdeal J)) : ℕ∞)
    (min (↑(multiplicity p.asIdeal I) : ℕ∞) (↑(multiplicity p.asIdeal J) : ℕ∞))
⊢ emultiplicity p.asIdeal (I ⊔ J) = min (emultiplicity p.asIdeal I) (emultiplicity p.asIdeal J)

Tactic:
rw [(H this).emultiplicity_eq_multiplicity, (H hI).emultiplicity_eq_multiplicity,
    (H hJ).emultiplicity_eq_multiplicity, multiplicity_sup _ hI hJ]

Premises used: FiniteMultiplicity.emultiplicity_eq_multiplicity, IsDedekindDomain.HeightOneSpectrum.multiplicity_sup
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsDedekindDomain R
p : HeightOneSpectrum R
I J : Ideal R
hI : I ≠ ⊥
hJ : J ≠ ⊥
this : I ⊔ J ≠ ⊥
H : ∀ {I' : Ideal R} (h : I' ≠ ⊥), FiniteMultiplicity p.asIdeal I'
⊢ Eq (α := ℕ∞) (↑(min (multiplicity p.asIdeal I) (multiplicity p.asIdeal J)) : ℕ∞)
    (min (↑(multiplicity p.asIdeal I) : ℕ∞) (↑(multiplicity p.asIdeal J) : ℕ∞))

Tactic:
norm_cast
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsDedekindDomain R
p : HeightOneSpectrum R
ι : Type u_4
inst_2 : Finite ι
I : PEmpty.{u_4 + 1} → Ideal R
h_empty : emultiplicity p.asIdeal ⊥ = ⊤
⊢ emultiplicity p.asIdeal (⨆ (i : PEmpty.{u_4 + 1}), I i) = ⨅ (i : PEmpty.{u_4 + 1}), emultiplicity p.asIdeal (I i)

Tactic:
rw [iSup_of_empty, iInf_of_empty]

Premises used: iInf_of_empty, iSup_of_empty
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsDedekindDomain R
p : HeightOneSpectrum R
ι : Type u_4
inst_2 : Finite ι
I : PEmpty.{u_4 + 1} → Ideal R
⊢ emultiplicity p.asIdeal ⊥ = ⊤

Tactic:
emultiplicity_zero _

Premises used: emultiplicity_zero
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsDedekindDomain R
p : HeightOneSpectrum R
ι : Type u_4
inst_2 : Finite ι
I : PEmpty.{u_4 + 1} → Ideal R
⊢ emultiplicity p.asIdeal ⊥ = ⊤

Tactic:
exact emultiplicity_zero _

Premises used: emultiplicity_zero
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsDedekindDomain R
p : HeightOneSpectrum R
ι : Type u_4
inst_2 : Finite ι
α β : Type u_4
e : α ≃ β
ih : ∀ (I : α → Ideal R), emultiplicity p.asIdeal (⨆ (i : α), I i) = ⨅ (i : α), emultiplicity p.asIdeal (I i)
I : β → Ideal R
⊢ emultiplicity p.asIdeal (⨆ (i : α), (I ∘ (⇑e : (a : α) → β)) i) =
    ⨅ (i : α), emultiplicity p.asIdeal ((I ∘ (⇑e : (a : α) → β)) i)

Tactic:
specialize ih (I ∘ e)

Premises used: Function.comp, DFunLike.coe
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsDedekindDomain R
p : HeightOneSpectrum R
ι : Type u_4
inst_2 : Finite ι
α β : Type u_4
e : α ≃ β
I : β → Ideal R
ih :
  emultiplicity p.asIdeal (⨆ (i : α), (I ∘ (⇑e : (a : α) → β)) i) =
    ⨅ (i : α), emultiplicity p.asIdeal ((I ∘ (⇑e : (a : α) → β)) i)
⊢ emultiplicity p.asIdeal (sSup (range fun (i : α) ↦ (I ∘ (⇑e : (a : α) → β)) i)) =
    sInf (range fun (i : α) ↦ emultiplicity p.asIdeal ((I ∘ (⇑e : (a : α) → β)) i))

Tactic:
rw [← sSup_range, ← sInf_range] at ih ⊢

Premises used: sSup_range, sInf_range
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsDedekindDomain R
p : HeightOneSpectrum R
ι : Type u_4
inst_2 : Finite ι
α β : Type u_4
e : α ≃ β
I : β → Ideal R
ih :
  emultiplicity p.asIdeal (sSup (range fun (i : α) ↦ (I ∘ (⇑e : (a : α) → β)) i)) =
    sInf (range fun (i : α) ↦ emultiplicity p.asIdeal ((I ∘ (⇑e : (a : α) → β)) i))
⊢ emultiplicity p.asIdeal (sSup (range I)) =
    sInf (range fun (i : α) ↦ emultiplicity p.asIdeal ((I ∘ (⇑e : (a : α) → β)) i))

Tactic:
rw [EquivLike.range_comp I e] at ih

Premises used: EquivLike.range_comp
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsDedekindDomain R
p : HeightOneSpectrum R
ι : Type u_4
inst_2 : Finite ι
α β : Type u_4
e : α ≃ β
I : β → Ideal R
ih :
  emultiplicity p.asIdeal (sSup (range I)) =
    sInf (range fun (i : α) ↦ emultiplicity p.asIdeal ((I ∘ (⇑e : (a : α) → β)) i))
of_equiv :
  Eq (α := ℕ∞) (sInf (range fun (i : α) ↦ emultiplicity p.asIdeal ((I ∘ (⇑e : (a : α) → β)) i)))
    (sInf (range fun (i : β) ↦ emultiplicity p.asIdeal (I i)))
⊢ emultiplicity p.asIdeal (sSup (range fun (i : β) ↦ I i)) = sInf (range fun (i : β) ↦ emultiplicity p.asIdeal (I i))

Tactic:
rw [ih]