awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.DedekindDomain.Dvr
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
h : IsDedekindDomainDvr A
p : Ideal A
hp : p ≠ ⊥
hpp : p.IsPrime
q : Ideal A
hq : q.IsMaximal
hpq : p ≤ q
f : { p : Ideal A // p.IsPrime ∧ Disjoint (↑q.primeCompl : Set A) (↑p : Set A) } ≃o
  { p : Ideal (Localization.AtPrime q) // p.IsPrime } :=
  OrderIso.symm (IsLocalization.orderIsoOfPrime q.primeCompl (Localization.AtPrime q))
P : { p : Ideal (Localization.AtPrime q) // p.IsPrime } :=
  (f :
      (a : { p : Ideal A // p.IsPrime ∧ Disjoint (↑q.primeCompl : Set A) (↑p : Set A) }) →
        { p : Ideal (Localization.AtPrime q) // p.IsPrime })
    (Subtype.mk (p := fun (p : Ideal A) ↦ p.IsPrime ∧ Disjoint (↑q.primeCompl : Set A) (↑p : Set A)) p ⋯)
Q : { p : Ideal (Localization.AtPrime q) // p.IsPrime } :=
  (f :
      (a : { p : Ideal A // p.IsPrime ∧ Disjoint (↑q.primeCompl : Set A) (↑p : Set A) }) →
        { p : Ideal (Localization.AtPrime q) // p.IsPrime })
    (Subtype.mk (p := fun (p : Ideal A) ↦ p.IsPrime ∧ Disjoint (↑q.primeCompl : Set A) (↑p : Set A)) q ⋯)
hinj :
  Function.Injective (α := A) (β := Localization.AtPrime q)
    (⇑(algebraMap A (Localization.AtPrime q)) : (a : A) → Localization.AtPrime q)
⊢ (↑P : Ideal (Localization.AtPrime q)) ≠ ⊥

Tactic:
have hp1 : P.1 ≠ ⊥ := fun x => hp ((p.map_eq_bot_iff_of_injective hinj).mp x)
-- Module: Mathlib.RingTheory.DedekindDomain.Dvr
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
h : IsDedekindDomainDvr A
p : Ideal A
hp : p ≠ ⊥
hpp : p.IsPrime
q : Ideal A
hq : q.IsMaximal
hpq : p ≤ q
f : { p : Ideal A // p.IsPrime ∧ Disjoint (↑q.primeCompl : Set A) (↑p : Set A) } ≃o
  { p : Ideal (Localization.AtPrime q) // p.IsPrime } :=
  OrderIso.symm (IsLocalization.orderIsoOfPrime q.primeCompl (Localization.AtPrime q))
P : { p : Ideal (Localization.AtPrime q) // p.IsPrime } :=
  (f :
      (a : { p : Ideal A // p.IsPrime ∧ Disjoint (↑q.primeCompl : Set A) (↑p : Set A) }) →
        { p : Ideal (Localization.AtPrime q) // p.IsPrime })
    (Subtype.mk (p := fun (p : Ideal A) ↦ p.IsPrime ∧ Disjoint (↑q.primeCompl : Set A) (↑p : Set A)) p ⋯)
Q : { p : Ideal (Localization.AtPrime q) // p.IsPrime } :=
  (f :
      (a : { p : Ideal A // p.IsPrime ∧ Disjoint (↑q.primeCompl : Set A) (↑p : Set A) }) →
        { p : Ideal (Localization.AtPrime q) // p.IsPrime })
    (Subtype.mk (p := fun (p : Ideal A) ↦ p.IsPrime ∧ Disjoint (↑q.primeCompl : Set A) (↑p : Set A)) q ⋯)
hinj :
  Function.Injective (α := A) (β := Localization.AtPrime q)
    (⇑(algebraMap A (Localization.AtPrime q)) : (a : A) → Localization.AtPrime q)
hp1 : (↑P : Ideal (Localization.AtPrime q)) ≠ ⊥
⊢ (↑Q : Ideal (Localization.AtPrime q)) ≠ ⊥

Tactic:
have hq1 : Q.1 ≠ ⊥ :=
      fun x => (ne_bot_of_le_ne_bot hp hpq) ((q.map_eq_bot_iff_of_injective hinj).mp x)
-- Module: Mathlib.RingTheory.DedekindDomain.Dvr
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
h : IsDedekindDomainDvr A
p : Ideal A
hp : p ≠ ⊥
hpp : p.IsPrime
q : Ideal A
hq : q.IsMaximal
hpq : p ≤ q
f : { p : Ideal A // p.IsPrime ∧ Disjoint (↑q.primeCompl : Set A) (↑p : Set A) } ≃o
  { p : Ideal (Localization.AtPrime q) // p.IsPrime } :=
  OrderIso.symm (IsLocalization.orderIsoOfPrime q.primeCompl (Localization.AtPrime q))
P : { p : Ideal (Localization.AtPrime q) // p.IsPrime } :=
  (f :
      (a : { p : Ideal A // p.IsPrime ∧ Disjoint (↑q.primeCompl : Set A) (↑p : Set A) }) →
        { p : Ideal (Localization.AtPrime q) // p.IsPrime })
    (Subtype.mk (p := fun (p : Ideal A) ↦ p.IsPrime ∧ Disjoint (↑q.primeCompl : Set A) (↑p : Set A)) p ⋯)
Q : { p : Ideal (Localization.AtPrime q) // p.IsPrime } :=
  (f :
      (a : { p : Ideal A // p.IsPrime ∧ Disjoint (↑q.primeCompl : Set A) (↑p : Set A) }) →
        { p : Ideal (Localization.AtPrime q) // p.IsPrime })
    (Subtype.mk (p := fun (p : Ideal A) ↦ p.IsPrime ∧ Disjoint (↑q.primeCompl : Set A) (↑p : Set A)) q ⋯)
hinj :
  Function.Injective (α := A) (β := Localization.AtPrime q)
    (⇑(algebraMap A (Localization.AtPrime q)) : (a : A) → Localization.AtPrime q)
hp1 : (↑P : Ideal (Localization.AtPrime q)) ≠ ⊥
hq1 : (↑Q : Ideal (Localization.AtPrime q)) ≠ ⊥
⊢ IsPrincipalIdealRing.{u_1} (Localization.AtPrime q)

Tactic:
rcases (IsDiscreteValuationRing.iff_pid_with_one_nonzero_prime (Localization.AtPrime q)).mp
      (h.is_dvr_at_nonzero_prime q (ne_bot_of_le_ne_bot hp hpq) hq.isPrime) with ⟨_, huq⟩

Premises used: ne_bot_of_le_ne_bot, Localization.AtPrime, Ideal.IsMaximal.isPrime, IsDedekindDomainDvr.is_dvr_at_nonzero_prime, Iff.mp, IsDiscreteValuationRing.iff_pid_with_one_nonzero_prime
-- Module: Mathlib.RingTheory.DedekindDomain.Dvr
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
h : IsDedekindDomainDvr A
p : Ideal A
hp : p ≠ ⊥
hpp : p.IsPrime
q : Ideal A
hq : q.IsMaximal
hpq : p ≤ q
f : { p : Ideal A // p.IsPrime ∧ Disjoint (↑q.primeCompl : Set A) (↑p : Set A) } ≃o
  { p : Ideal (Localization.AtPrime q) // p.IsPrime } :=
  OrderIso.symm (IsLocalization.orderIsoOfPrime q.primeCompl (Localization.AtPrime q))
P : { p : Ideal (Localization.AtPrime q) // p.IsPrime } :=
  (f :
      (a : { p : Ideal A // p.IsPrime ∧ Disjoint (↑q.primeCompl : Set A) (↑p : Set A) }) →
        { p : Ideal (Localization.AtPrime q) // p.IsPrime })
    (Subtype.mk (p := fun (p : Ideal A) ↦ p.IsPrime ∧ Disjoint (↑q.primeCompl : Set A) (↑p : Set A)) p ⋯)
Q : { p : Ideal (Localization.AtPrime q) // p.IsPrime } :=
  (f :
      (a : { p : Ideal A // p.IsPrime ∧ Disjoint (↑q.primeCompl : Set A) (↑p : Set A) }) →
        { p : Ideal (Localization.AtPrime q) // p.IsPrime })
    (Subtype.mk (p := fun (p : Ideal A) ↦ p.IsPrime ∧ Disjoint (↑q.primeCompl : Set A) (↑p : Set A)) q ⋯)
hinj :
  Function.Injective (α := A) (β := Localization.AtPrime q)
    (⇑(algebraMap A (Localization.AtPrime q)) : (a : A) → Localization.AtPrime q)
hp1 : (↑P : Ideal (Localization.AtPrime q)) ≠ ⊥
hq1 : (↑Q : Ideal (Localization.AtPrime q)) ≠ ⊥
left : IsPrincipalIdealRing.{u_1} (Localization.AtPrime q)
⊢ ∃! P : Ideal (Localization.AtPrime q), P ≠ ⊥ ∧ P.IsPrime

Tactic:
rcases (IsDiscreteValuationRing.iff_pid_with_one_nonzero_prime (Localization.AtPrime q)).mp
      (h.is_dvr_at_nonzero_prime q (ne_bot_of_le_ne_bot hp hpq) hq.isPrime) with ⟨_, huq⟩

Premises used: ne_bot_of_le_ne_bot, Localization.AtPrime, Ideal.IsMaximal.isPrime, IsDedekindDomainDvr.is_dvr_at_nonzero_prime, Iff.mp, IsDiscreteValuationRing.iff_pid_with_one_nonzero_prime
-- Module: Mathlib.RingTheory.DedekindDomain.Dvr
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
h : IsDedekindDomainDvr A
p : Ideal A
hp : p ≠ ⊥
hpp : p.IsPrime
q : Ideal A
hq : q.IsMaximal
hpq : p ≤ q
f : { p : Ideal A // p.IsPrime ∧ Disjoint (↑q.primeCompl : Set A) (↑p : Set A) } ≃o
  { p : Ideal (Localization.AtPrime q) // p.IsPrime } :=
  OrderIso.symm (IsLocalization.orderIsoOfPrime q.primeCompl (Localization.AtPrime q))
P : { p : Ideal (Localization.AtPrime q) // p.IsPrime } :=
  (f :
      (a : { p : Ideal A // p.IsPrime ∧ Disjoint (↑q.primeCompl : Set A) (↑p : Set A) }) →
        { p : Ideal (Localization.AtPrime q) // p.IsPrime })
    (Subtype.mk (p := fun (p : Ideal A) ↦ p.IsPrime ∧ Disjoint (↑q.primeCompl : Set A) (↑p : Set A)) p ⋯)
Q : { p : Ideal (Localization.AtPrime q) // p.IsPrime } :=
  (f :
      (a : { p : Ideal A // p.IsPrime ∧ Disjoint (↑q.primeCompl : Set A) (↑p : Set A) }) →
        { p : Ideal (Localization.AtPrime q) // p.IsPrime })
    (Subtype.mk (p := fun (p : Ideal A) ↦ p.IsPrime ∧ Disjoint (↑q.primeCompl : Set A) (↑p : Set A)) q ⋯)
hinj :
  Function.Injective (α := A) (β := Localization.AtPrime q)
    (⇑(algebraMap A (Localization.AtPrime q)) : (a : A) → Localization.AtPrime q)
hp1 : (↑P : Ideal (Localization.AtPrime q)) ≠ ⊥
hq1 : (↑Q : Ideal (Localization.AtPrime q)) ≠ ⊥
left : IsPrincipalIdealRing.{u_1} (Localization.AtPrime q)
huq : ∃! P : Ideal (Localization.AtPrime q), P ≠ ⊥ ∧ P.IsPrime
rw : q.IsMaximal
⊢ p.IsMaximal

Tactic:
rw [show p = q from Subtype.val_inj.mpr <| f.injective <|
      Subtype.val_inj.mp (huq.unique ⟨hp1, P.2⟩ ⟨hq1, Q.2⟩)]

Premises used: Iff.mpr, Subtype.val_inj, OrderIso.injective, And.intro, Iff.mp, ExistsUnique.unique, Subtype.property
-- Module: Mathlib.RingTheory.DedekindDomain.Dvr
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
h : IsDedekindDomainDvr A
p : Ideal A
hp : p ≠ ⊥
hpp : p.IsPrime
q : Ideal A
hq : q.IsMaximal
hpq : p ≤ q
f : { p : Ideal A // p.IsPrime ∧ Disjoint (↑q.primeCompl : Set A) (↑p : Set A) } ≃o
  { p : Ideal (Localization.AtPrime q) // p.IsPrime } :=
  OrderIso.symm (IsLocalization.orderIsoOfPrime q.primeCompl (Localization.AtPrime q))
P : { p : Ideal (Localization.AtPrime q) // p.IsPrime } :=
  (f :
      (a : { p : Ideal A // p.IsPrime ∧ Disjoint (↑q.primeCompl : Set A) (↑p : Set A) }) →
        { p : Ideal (Localization.AtPrime q) // p.IsPrime })
    (Subtype.mk (p := fun (p : Ideal A) ↦ p.IsPrime ∧ Disjoint (↑q.primeCompl : Set A) (↑p : Set A)) p ⋯)
Q : { p : Ideal (Localization.AtPrime q) // p.IsPrime } :=
  (f :
      (a : { p : Ideal A // p.IsPrime ∧ Disjoint (↑q.primeCompl : Set A) (↑p : Set A) }) →
        { p : Ideal (Localization.AtPrime q) // p.IsPrime })
    (Subtype.mk (p := fun (p : Ideal A) ↦ p.IsPrime ∧ Disjoint (↑q.primeCompl : Set A) (↑p : Set A)) q ⋯)
hinj :
  Function.Injective (α := A) (β := Localization.AtPrime q)
    (⇑(algebraMap A (Localization.AtPrime q)) : (a : A) → Localization.AtPrime q)
hp1 : (↑P : Ideal (Localization.AtPrime q)) ≠ ⊥
hq1 : (↑Q : Ideal (Localization.AtPrime q)) ≠ ⊥
left : IsPrincipalIdealRing.{u_1} (Localization.AtPrime q)
huq : ∃! P : Ideal (Localization.AtPrime q), P ≠ ⊥ ∧ P.IsPrime
⊢ q.IsMaximal

Tactic:
hq
-- Module: Mathlib.RingTheory.DedekindDomain.Dvr
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
h : IsDedekindDomainDvr A
p : Ideal A
hp : p ≠ ⊥
hpp : p.IsPrime
q : Ideal A
hq : q.IsMaximal
hpq : p ≤ q
f : { p : Ideal A // p.IsPrime ∧ Disjoint (↑q.primeCompl : Set A) (↑p : Set A) } ≃o
  { p : Ideal (Localization.AtPrime q) // p.IsPrime } :=
  OrderIso.symm (IsLocalization.orderIsoOfPrime q.primeCompl (Localization.AtPrime q))
P : { p : Ideal (Localization.AtPrime q) // p.IsPrime } :=
  (f :
      (a : { p : Ideal A // p.IsPrime ∧ Disjoint (↑q.primeCompl : Set A) (↑p : Set A) }) →
        { p : Ideal (Localization.AtPrime q) // p.IsPrime })
    (Subtype.mk (p := fun (p : Ideal A) ↦ p.IsPrime ∧ Disjoint (↑q.primeCompl : Set A) (↑p : Set A)) p ⋯)
Q : { p : Ideal (Localization.AtPrime q) // p.IsPrime } :=
  (f :
      (a : { p : Ideal A // p.IsPrime ∧ Disjoint (↑q.primeCompl : Set A) (↑p : Set A) }) →
        { p : Ideal (Localization.AtPrime q) // p.IsPrime })
    (Subtype.mk (p := fun (p : Ideal A) ↦ p.IsPrime ∧ Disjoint (↑q.primeCompl : Set A) (↑p : Set A)) q ⋯)
hinj :
  Function.Injective (α := A) (β := Localization.AtPrime q)
    (⇑(algebraMap A (Localization.AtPrime q)) : (a : A) → Localization.AtPrime q)
hp1 : (↑P : Ideal (Localization.AtPrime q)) ≠ ⊥
hq1 : (↑Q : Ideal (Localization.AtPrime q)) ≠ ⊥
left : IsPrincipalIdealRing.{u_1} (Localization.AtPrime q)
huq : ∃! P : Ideal (Localization.AtPrime q), P ≠ ⊥ ∧ P.IsPrime
⊢ q.IsMaximal

Tactic:
exact hq
-- Module: Mathlib.RingTheory.DedekindDomain.Dvr
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
h : IsDedekindDomainDvr A
⊢ IsIntegrallyClosed A

Tactic:
IsIntegrallyClosed.of_localization_maximal <| fun p hp0 hpm ↦
    let ⟨_, _⟩ := (IsDiscreteValuationRing.iff_pid_with_one_nonzero_prime
      (Localization.AtPrime p)).mp (h.is_dvr_at_nonzero_prime p hp0 hpm.isPrime)
    inferInstance

Premises used: IsIntegrallyClosed.of_localization_maximal, Localization.AtPrime, inferInstance, Ideal.IsMaximal.isPrime, _private.0.IsDedekindDomainDvr.isIntegrallyClosed.match_1, IsDedekindDomainDvr.is_dvr_at_nonzero_prime, IsIntegrallyClosed, Iff.mp, IsDiscreteValuationRing.iff_pid_with_one_nonzero_prime
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
rw :
  v.asIdeal ^ count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)) =
    v.asIdeal ^ Multiset.count v.asIdeal (normalizedFactors I)
rw₁ :
  v.asIdeal ^
      count (Associates.mk v.asIdeal)
        (↑(factors' I) : WithTop (Multiset { a : Associates (Ideal R) // Irreducible a })) =
    v.asIdeal ^ Multiset.count v.asIdeal (normalizedFactors I)
rw₂ :
  v.asIdeal ^
      Multiset.count (Subtype.mk (p := fun (a : Associates (Ideal R)) ↦ Irreducible a) (Associates.mk v.asIdeal) ⋯)
        (factors' I) =
    v.asIdeal ^ Multiset.count v.asIdeal (normalizedFactors I)
rw₃ :
  v.asIdeal ^
      Multiset.count
        (↑(Subtype.mk (p := fun (a : Associates (Ideal R)) ↦ Irreducible a) (Associates.mk v.asIdeal) ⋯) :
          Associates (Ideal R))
        (Multiset.map (Subtype.val (p := fun (a : Associates (Ideal R)) ↦ Irreducible a)) (factors' I)) =
    v.asIdeal ^ Multiset.count v.asIdeal (normalizedFactors I)
rw₄ :
  v.asIdeal ^
      Multiset.count
        (↑(Subtype.mk (p := fun (a : Associates (Ideal R)) ↦ Irreducible a) (Associates.mk v.asIdeal) ⋯) :
          Associates (Ideal R))
        (Multiset.map Associates.mk (UniqueFactorizationMonoid.factors I)) =
    v.asIdeal ^ Multiset.count v.asIdeal (normalizedFactors I)
rw₅ :
  v.asIdeal ^
      Multiset.count
        (↑(Subtype.mk (p := fun (a : Associates (Ideal R)) ↦ Irreducible a) (Associates.mk v.asIdeal) ⋯) :
          Associates (Ideal R))
        (Multiset.map Associates.mk (normalizedFactors I)) =
    v.asIdeal ^ Multiset.count v.asIdeal (normalizedFactors I)
rw₆ rw₇ :
  v.asIdeal ^
      Multiset.count
        (↑(Subtype.mk (p := fun (a : Associates (Ideal R)) ↦ Irreducible a) (Associates.mk v.asIdeal) ⋯) :
          Associates (Ideal R))
        (Multiset.map Associates.mk (normalizedFactors I)) =
    v.asIdeal ^
      Multiset.count (α := Associates (Ideal R)) (Associates.mk v.asIdeal)
        (Multiset.map Associates.mk (normalizedFactors I))
⊢ v.maxPowDividing I = v.asIdeal ^ Multiset.count v.asIdeal (normalizedFactors I)

Tactic:
rw [maxPowDividing, factors_mk _ hI, count_some (irreducible_mk.mpr v.irreducible),
    ← Multiset.count_map_eq_count' _ _ Subtype.val_injective, map_subtype_coe_factors',
    factors_eq_normalizedFactors, ← Multiset.count_map_eq_count' _ _ (mk_injective (M := Ideal R))]

Premises used: Iff.mpr, UniqueFactorizationMonoid.factors_eq_normalizedFactors, Associates.irreducible_mk, Subtype.val_injective, Associates.count_some, IsDedekindDomain.HeightOneSpectrum.irreducible, Associates.factors_mk, Associates.map_subtype_coe_factors', Associates.mk_injective, IsDedekindDomain.HeightOneSpectrum.maxPowDividing, Multiset.count_map_eq_count'
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
haveI : ∀ (h_fin : Fintype { x : Ideal R // x ∣ I }), Finite.{u_1 + 1} { x : HeightOneSpectrum R // x.asIdeal ∣ I }
⊢ Finite.{u_1 + 1} { x : HeightOneSpectrum R // x.asIdeal ∣ I }

Tactic:
haveI h_fin := fintypeSubtypeDvd I hI
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
h_fin : Fintype { x : Ideal R // x ∣ I }
⊢ Finite.{u_1 + 1} { x : HeightOneSpectrum R // x.asIdeal ∣ I }

Tactic:
Finite.of_injective (fun v => (⟨(v : HeightOneSpectrum R).asIdeal, v.2⟩ : { x // x ∣ I })) ?_

Premises used: IsDedekindDomain.HeightOneSpectrum.asIdeal, Subtype.mk, Subtype.val, Subtype.property, Finite.of_injective
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
h_fin : Fintype { x : Ideal R // x ∣ I }
v :
  Injective (β := { x : Ideal R // x ∣ I }) fun (v : { x : HeightOneSpectrum R // x.asIdeal ∣ I }) ↦
    Subtype.mk (p := fun (x : Ideal R) ↦ x ∣ I) (↑v : HeightOneSpectrum R).asIdeal ⋯
⊢ Finite.{u_1 + 1} { x : HeightOneSpectrum R // x.asIdeal ∣ I }

Tactic:
refine
    Finite.of_injective (fun v => (⟨(v : HeightOneSpectrum R).asIdeal, v.2⟩ : { x // x ∣ I })) ?_
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
h_fin : Fintype { x : Ideal R // x ∣ I }
v w : { x : HeightOneSpectrum R // x.asIdeal ∣ I }
hvw :
  Eq.{u_1 + 1} (α := { x : Ideal R // x ∣ I })
    ((fun (v : { x : HeightOneSpectrum R // x.asIdeal ∣ I }) ↦
        (Subtype.mk (p := fun (x : Ideal R) ↦ x ∣ I) (↑v : HeightOneSpectrum R).asIdeal ⋯ : { x : Ideal R // x ∣ I }))
      v)
    ((fun (v : { x : HeightOneSpectrum R // x.asIdeal ∣ I }) ↦
        (Subtype.mk (p := fun (x : Ideal R) ↦ x ∣ I) (↑v : HeightOneSpectrum R).asIdeal ⋯ : { x : Ideal R // x ∣ I }))
      w)
⊢ Eq.{u_1 + 1} (α := Ideal R)
    (asIdeal ((fun (a : { x : HeightOneSpectrum R // x.asIdeal ∣ I }) ↦ (↑a : HeightOneSpectrum R)) v))
    (asIdeal ((fun (a : { x : HeightOneSpectrum R // x.asIdeal ∣ I }) ↦ (↑a : HeightOneSpectrum R)) w))

Tactic:
simpa using hvw
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
h_fin : Fintype { x : Ideal R // x ∣ I }
v w : { x : HeightOneSpectrum R // x.asIdeal ∣ I }
hvw :
  Eq.{u_1 + 1} (α := { x : Ideal R // x ∣ I })
    ((fun (v : { x : HeightOneSpectrum R // x.asIdeal ∣ I }) ↦
        (Subtype.mk (p := fun (x : Ideal R) ↦ x ∣ I) (↑v : HeightOneSpectrum R).asIdeal ⋯ : { x : Ideal R // x ∣ I }))
      v)
    ((fun (v : { x : HeightOneSpectrum R // x.asIdeal ∣ I }) ↦
        (Subtype.mk (p := fun (x : Ideal R) ↦ x ∣ I) (↑v : HeightOneSpectrum R).asIdeal ⋯ : { x : Ideal R // x ∣ I }))
      w)
⊢ v = w

Tactic:
exact Subtype.coe_injective (HeightOneSpectrum.ext (by simpa using hvw))

Premises used: IsDedekindDomain.HeightOneSpectrum.ext, Subtype.coe_injective
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
h :
  ∀ (v : HeightOneSpectrum R),
    Membership.mem (γ := Set (HeightOneSpectrum R))
        {v : HeightOneSpectrum R | ¬Eq (α := ℤ) (↑(count (Associates.mk v.asIdeal) (factors (Associates.mk I))) : ℤ) 0}
        v ↔
      Membership.mem (γ := Set (HeightOneSpectrum R)) {v : HeightOneSpectrum R | v.asIdeal ∣ I} v
⊢ Eq.{u_1 + 1} (α := Set (HeightOneSpectrum R))
    {v : HeightOneSpectrum R | ¬Eq (α := ℤ) (↑(count (Associates.mk v.asIdeal) (factors (Associates.mk I))) : ℤ) 0}
    {v : HeightOneSpectrum R | v.asIdeal ∣ I}

Tactic:
ext v
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
v : HeightOneSpectrum R
h :
  Membership.mem (γ := Set (HeightOneSpectrum R))
      {v : HeightOneSpectrum R | ¬count (Associates.mk v.asIdeal) (factors (Associates.mk I)) = 0} v ↔
    Membership.mem (γ := Set (HeightOneSpectrum R)) {v : HeightOneSpectrum R | v.asIdeal ∣ I} v
⊢ Membership.mem (γ := Set (HeightOneSpectrum R))
      {v : HeightOneSpectrum R | ¬Eq (α := ℤ) (↑(count (Associates.mk v.asIdeal) (factors (Associates.mk I))) : ℤ) 0}
      v ↔
    Membership.mem (γ := Set (HeightOneSpectrum R)) {v : HeightOneSpectrum R | v.asIdeal ∣ I} v

Tactic:
simp_rw [Int.natCast_eq_zero]

Premises used: Int.natCast_eq_zero
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
v : HeightOneSpectrum R
⊢ Membership.mem (γ := Set (HeightOneSpectrum R))
      {v : HeightOneSpectrum R | ¬count (Associates.mk v.asIdeal) (factors (Associates.mk I)) = 0} v ↔
    Membership.mem (γ := Set (HeightOneSpectrum R)) {v : HeightOneSpectrum R | v.asIdeal ∣ I} v

Tactic:
Associates.count_ne_zero_iff_dvd hI v.irreducible

Premises used: Set.Mem, setOf, IsDedekindDomain.HeightOneSpectrum.irreducible, Associates.count_ne_zero_iff_dvd, Not
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
v : HeightOneSpectrum R
⊢ Membership.mem (γ := Set (HeightOneSpectrum R))
      {v : HeightOneSpectrum R | ¬count (Associates.mk v.asIdeal) (factors (Associates.mk I)) = 0} v ↔
    Membership.mem (γ := Set (HeightOneSpectrum R)) {v : HeightOneSpectrum R | v.asIdeal ∣ I} v

Tactic:
exact Associates.count_ne_zero_iff_dvd hI v.irreducible

Premises used: IsDedekindDomain.HeightOneSpectrum.irreducible, Associates.count_ne_zero_iff_dvd
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
⊢ Eq.{u_1 + 1} (α := Set (HeightOneSpectrum R))
    {v : HeightOneSpectrum R | ¬Eq (α := ℤ) (↑(count (Associates.mk v.asIdeal) (factors (Associates.mk I))) : ℤ) 0}
    {v : HeightOneSpectrum R | v.asIdeal ∣ I}

Tactic:
have h_supp : {v : HeightOneSpectrum R | ¬((Associates.mk v.asIdeal).count
      (Associates.mk I).factors : ℤ) = 0} = {v : HeightOneSpectrum R | v.asIdeal ∣ I} := by
    ext v
    simp_rw [Int.natCast_eq_zero]
    exact Associates.count_ne_zero_iff_dvd hI v.irreducible
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
h_supp :
  Eq.{u_1 + 1} (α := Set (HeightOneSpectrum R))
    {v : HeightOneSpectrum R | ¬Eq (α := ℤ) (↑(count (Associates.mk v.asIdeal) (factors (Associates.mk I))) : ℤ) 0}
    {v : HeightOneSpectrum R | v.asIdeal ∣ I}
rw : Set.Finite.{u_1} (α := HeightOneSpectrum R) {v : HeightOneSpectrum R | v.asIdeal ∣ I}
⊢ ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite,
    Eq (α := ℤ) (↑(count (Associates.mk v.asIdeal) (factors (Associates.mk I))) : ℤ) 0

Tactic:
rw [Filter.eventually_cofinite, h_supp]

Premises used: Filter.eventually_cofinite
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
h_supp :
  Eq.{u_1 + 1} (α := Set (HeightOneSpectrum R))
    {v : HeightOneSpectrum R | ¬Eq (α := ℤ) (↑(count (Associates.mk v.asIdeal) (factors (Associates.mk I))) : ℤ) 0}
    {v : HeightOneSpectrum R | v.asIdeal ∣ I}
⊢ Set.Finite.{u_1} (α := HeightOneSpectrum R) {v : HeightOneSpectrum R | v.asIdeal ∣ I}

Tactic:
Ideal.finite_factors hI

Premises used: Ideal.finite_factors
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
h_supp :
  Eq.{u_1 + 1} (α := Set (HeightOneSpectrum R))
    {v : HeightOneSpectrum R | ¬Eq (α := ℤ) (↑(count (Associates.mk v.asIdeal) (factors (Associates.mk I))) : ℤ) 0}
    {v : HeightOneSpectrum R | v.asIdeal ∣ I}
⊢ Set.Finite.{u_1} (α := HeightOneSpectrum R) {v : HeightOneSpectrum R | v.asIdeal ∣ I}

Tactic:
exact Ideal.finite_factors hI

Premises used: Ideal.finite_factors
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
v : HeightOneSpectrum R
hv : Membership.mem (γ := Set (HeightOneSpectrum R)) {v : HeightOneSpectrum R | v.maxPowDividing I ≠ 1} v
h_zero : Eq (α := ℤ) (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))) : ℤ) 0
rw : v.asIdeal ^ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)) = 1
rw₁ : HPow.hPow (β := ℕ) v.asIdeal 0 = 1
rw₂ rw₃ : Eq.{u_1 + 1} (α := Ideal R) 1 1
⊢ v.maxPowDividing I = 1

Tactic:
rw [IsDedekindDomain.HeightOneSpectrum.maxPowDividing, Int.natCast_eq_zero.mp h_zero,
        pow_zero _]

Premises used: Int.natCast_eq_zero, pow_zero, Iff.mp, IsDedekindDomain.HeightOneSpectrum.maxPowDividing
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
v : HeightOneSpectrum R
hv : Membership.mem (γ := Set (HeightOneSpectrum R)) {v : HeightOneSpectrum R | v.maxPowDividing I ≠ 1} v
h_zero : Eq (α := ℤ) (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))) : ℤ) 0
⊢ v.maxPowDividing I = 1

Tactic:
have hv' : v.maxPowDividing I = 1 := by
      rw [IsDedekindDomain.HeightOneSpectrum.maxPowDividing, Int.natCast_eq_zero.mp h_zero,
        pow_zero _]