awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
A : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Field K
inst_3 : IsDomain R
inst_4 : IsPrincipalIdealRing R
inst_5 : NormalizationMonoid R
r : R
hr : r ≠ 0
i : Ideal R
hi :
  Membership.mem (γ := Set (Ideal R))
    {I : Ideal R | Membership.mem (γ := Multiset (Ideal R)) (normalizedFactors (span {r})) I} i
this : i.IsPrime
a : R
ha : a ∈ normalizedFactors r
ha' : Associated (Submodule.IsPrincipal.generator i) a
h :
  (fun (d : (↑{d : R | d ∈ normalizedFactors r} : Type u_1)) ↦
        (Subtype.mk (p := fun (x : Ideal R) ↦
            Membership.mem (γ := Set (Ideal R))
              {I : Ideal R | Membership.mem (γ := Multiset (Ideal R)) (normalizedFactors (span {r})) I} x)
            (span {(↑d : R)}) ⋯ :
          { x : Ideal R //
            Membership.mem (γ := Set (Ideal R))
              {I : Ideal R | Membership.mem (γ := Multiset (Ideal R)) (normalizedFactors (span {r})) I} x }))
      (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Set R) {d : R | d ∈ normalizedFactors r} x) a ha) =
    Subtype.mk (p := fun (x : Ideal R) ↦
      Membership.mem (γ := Set (Ideal R))
        {I : Ideal R | Membership.mem (γ := Multiset (Ideal R)) (normalizedFactors (span {r})) I} x)
      i hi
⊢ ∃ (a : (↑{d : R | d ∈ normalizedFactors r} : Type u_1)),
    (fun (d : (↑{d : R | d ∈ normalizedFactors r} : Type u_1)) ↦
          (Subtype.mk (p := fun (x : Ideal R) ↦
              Membership.mem (γ := Set (Ideal R))
                {I : Ideal R | Membership.mem (γ := Multiset (Ideal R)) (normalizedFactors (span {r})) I} x)
              (span {(↑d : R)}) ⋯ :
            { x : Ideal R //
              Membership.mem (γ := Set (Ideal R))
                {I : Ideal R | Membership.mem (γ := Multiset (Ideal R)) (normalizedFactors (span {r})) I} x }))
        a =
      Subtype.mk (p := fun (x : Ideal R) ↦
        Membership.mem (γ := Set (Ideal R))
          {I : Ideal R | Membership.mem (γ := Multiset (Ideal R)) (normalizedFactors (span {r})) I} x)
        i hi

Tactic:
use ⟨a, ha⟩
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
A : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Field K
inst_3 : IsDomain R
inst_4 : IsPrincipalIdealRing R
inst_5 : NormalizationMonoid R
r : R
hr : r ≠ 0
i : Ideal R
hi :
  Membership.mem (γ := Set (Ideal R))
    {I : Ideal R | Membership.mem (γ := Multiset (Ideal R)) (normalizedFactors (span {r})) I} i
this : i.IsPrime
a : R
ha : a ∈ normalizedFactors r
ha' : Associated (Submodule.IsPrincipal.generator i) a
⊢ (fun (d : (↑{d : R | d ∈ normalizedFactors r} : Type u_1)) ↦
        (Subtype.mk (p := fun (x : Ideal R) ↦
            Membership.mem (γ := Set (Ideal R))
              {I : Ideal R | Membership.mem (γ := Multiset (Ideal R)) (normalizedFactors (span {r})) I} x)
            (span {(↑d : R)}) ⋯ :
          { x : Ideal R //
            Membership.mem (γ := Set (Ideal R))
              {I : Ideal R | Membership.mem (γ := Multiset (Ideal R)) (normalizedFactors (span {r})) I} x }))
      (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Set R) {d : R | d ∈ normalizedFactors r} x) a ha) =
    Subtype.mk (p := fun (x : Ideal R) ↦
      Membership.mem (γ := Set (Ideal R))
        {I : Ideal R | Membership.mem (γ := Multiset (Ideal R)) (normalizedFactors (span {r})) I} x)
      i hi

Tactic:
simp only [← span_singleton_eq_span_singleton.mpr ha',
            span_singleton_generator]

Premises used: Iff.mpr, Ideal.span_singleton_eq_span_singleton, Ideal.span_singleton_generator
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
A : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Field K
inst_3 : IsDomain R
inst_4 : IsPrincipalIdealRing R
inst_5 : NormalizationMonoid R
r : R
hr : r ≠ 0
i : Ideal R
hi :
  Membership.mem (γ := Set (Ideal R))
    {I : Ideal R | Membership.mem (γ := Multiset (Ideal R)) (normalizedFactors (span {r})) I} i
this : i.IsPrime
⊢ Submodule.IsPrincipal.generator i ∣ r

Tactic:
(Submodule.IsPrincipal.mem_iff_generator_dvd i).mp
          ((show span {r} ≤ i from dvd_iff_le.mp (dvd_of_mem_normalizedFactors hi))
            (mem_span_singleton.mpr (dvd_refl r)))

Premises used: Iff.mpr, Ideal.dvd_iff_le, UniqueFactorizationMonoid.dvd_of_mem_normalizedFactors, Iff.mp, Ideal.mem_span_singleton, Submodule.IsPrincipal.mem_iff_generator_dvd, dvd_refl
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
A : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Field K
inst_3 : IsDomain R
inst_4 : IsPrincipalIdealRing R
inst_5 : NormalizationMonoid R
r : R
hr : r ≠ 0
i : Ideal R
hi :
  Membership.mem (γ := Set (Ideal R))
    {I : Ideal R | Membership.mem (γ := Multiset (Ideal R)) (normalizedFactors (span {r})) I} i
this : i.IsPrime
⊢ Submodule.IsPrincipal.generator i ∣ r

Tactic:
exact (Submodule.IsPrincipal.mem_iff_generator_dvd i).mp
          ((show span {r} ≤ i from dvd_iff_le.mp (dvd_of_mem_normalizedFactors hi))
            (mem_span_singleton.mpr (dvd_refl r)))

Premises used: Iff.mpr, Ideal.dvd_iff_le, UniqueFactorizationMonoid.dvd_of_mem_normalizedFactors, Iff.mp, Ideal.mem_span_singleton, Submodule.IsPrincipal.mem_iff_generator_dvd, dvd_refl
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
inst_3 : NormalizationMonoid R
r d : R
hr : r ≠ 0
hd : d ∈ normalizedFactors r
⊢ emultiplicity d r =
    emultiplicity (α := Ideal R)
      (↑(((normalizedFactorsEquivSpanNormalizedFactors hr :
                (↑{d : R | d ∈ normalizedFactors r} : Type u_1) ≃
                  (↑{I : Ideal R | Membership.mem (γ := Multiset (Ideal R)) (normalizedFactors (span {r})) I} :
                    Type u_1)) :
              (a : (↑{d : R | d ∈ normalizedFactors r} : Type u_1)) →
                (↑{I : Ideal R | I ∈ normalizedFactors (span {r})} : Type u_1))
            (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Set R) {d : R | d ∈ normalizedFactors r} x) d hd)) :
        Ideal R)
      (span {r})

Tactic:
simp only [normalizedFactorsEquivSpanNormalizedFactors, emultiplicity_eq_emultiplicity_span,
    Subtype.coe_mk, Equiv.ofBijective_apply]

Premises used: Subtype.coe_mk, Equiv.ofBijective_apply, Ideal.emultiplicity_eq_emultiplicity_span, Ideal.normalizedFactorsEquivSpanNormalizedFactors
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
inst_3 : NormalizationMonoid R
r : R
hr : r ≠ 0
I : (↑{I : Ideal R | Membership.mem (γ := Multiset (Ideal R)) (normalizedFactors (span {r})) I} : Type u_1)
obtain :
  ∀ (x : (↑{d : R | d ∈ normalizedFactors r} : Type u_1))
    (hx :
      ((normalizedFactorsEquivSpanNormalizedFactors hr :
              (↑{d : R | d ∈ normalizedFactors r} : Type u_1) ≃
                (↑{I : Ideal R | Membership.mem (γ := Multiset (Ideal R)) (normalizedFactors (span {r})) I} :
                  Type u_1)) :
            (a : (↑{d : R | d ∈ normalizedFactors r} : Type u_1)) →
              (↑{I : Ideal R | I ∈ normalizedFactors (span {r})} : Type u_1))
          x =
        I),
    emultiplicity
        (↑(((Equiv.symm (normalizedFactorsEquivSpanNormalizedFactors hr) :
                  (↑{I : Ideal R | Membership.mem (γ := Multiset (Ideal R)) (normalizedFactors (span {r})) I} :
                      Type u_1) ≃
                    (↑{d : R | d ∈ normalizedFactors r} : Type u_1)) :
                (a : (↑{I : Ideal R | I ∈ normalizedFactors (span {r})} : Type u_1)) →
                  (↑{d : R | d ∈ normalizedFactors r} : Type u_1))
              I) :
          R)
        r =
      emultiplicity (↑I : Ideal R) (span {r})
⊢ emultiplicity
      (↑(((Equiv.symm (normalizedFactorsEquivSpanNormalizedFactors hr) :
                (↑{I : Ideal R | Membership.mem (γ := Multiset (Ideal R)) (normalizedFactors (span {r})) I} :
                    Type u_1) ≃
                  (↑{d : R | d ∈ normalizedFactors r} : Type u_1)) :
              (a : (↑{I : Ideal R | I ∈ normalizedFactors (span {r})} : Type u_1)) →
                (↑{d : R | d ∈ normalizedFactors r} : Type u_1))
            I) :
        R)
      r =
    emultiplicity (↑I : Ideal R) (span {r})

Tactic:
obtain ⟨x, hx⟩ := (normalizedFactorsEquivSpanNormalizedFactors hr).surjective I

Premises used: Equiv.surjective, Ideal.normalizedFactorsEquivSpanNormalizedFactors
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
inst_3 : NormalizationMonoid R
r : R
hr : r ≠ 0
I : (↑{I : Ideal R | Membership.mem (γ := Multiset (Ideal R)) (normalizedFactors (span {r})) I} : Type u_1)
x : (↑{d : R | d ∈ normalizedFactors r} : Type u_1)
hx :
  ((normalizedFactorsEquivSpanNormalizedFactors hr :
          (↑{d : R | d ∈ normalizedFactors r} : Type u_1) ≃
            (↑{I : Ideal R | Membership.mem (γ := Multiset (Ideal R)) (normalizedFactors (span {r})) I} : Type u_1)) :
        (a : (↑{d : R | d ∈ normalizedFactors r} : Type u_1)) →
          (↑{I : Ideal R | I ∈ normalizedFactors (span {r})} : Type u_1))
      x =
    I
obtain :
  ∀ (a : R) (ha : Membership.mem (γ := Set R) {d : R | d ∈ normalizedFactors r} a)
    (hx :
      ((normalizedFactorsEquivSpanNormalizedFactors hr :
              (↑{d : R | d ∈ normalizedFactors r} : Type u_1) ≃
                (↑{I : Ideal R | Membership.mem (γ := Multiset (Ideal R)) (normalizedFactors (span {r})) I} :
                  Type u_1)) :
            (a : (↑{d : R | d ∈ normalizedFactors r} : Type u_1)) →
              (↑{I : Ideal R | I ∈ normalizedFactors (span {r})} : Type u_1))
          (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Set R) {d : R | d ∈ normalizedFactors r} x) a ha) =
        I),
    emultiplicity
        (↑(((Equiv.symm (normalizedFactorsEquivSpanNormalizedFactors hr) :
                  (↑{I : Ideal R | Membership.mem (γ := Multiset (Ideal R)) (normalizedFactors (span {r})) I} :
                      Type u_1) ≃
                    (↑{d : R | d ∈ normalizedFactors r} : Type u_1)) :
                (a : (↑{I : Ideal R | I ∈ normalizedFactors (span {r})} : Type u_1)) →
                  (↑{d : R | d ∈ normalizedFactors r} : Type u_1))
              I) :
          R)
        r =
      emultiplicity (↑I : Ideal R) (span {r})
⊢ emultiplicity
      (↑(((Equiv.symm (normalizedFactorsEquivSpanNormalizedFactors hr) :
                (↑{I : Ideal R | Membership.mem (γ := Multiset (Ideal R)) (normalizedFactors (span {r})) I} :
                    Type u_1) ≃
                  (↑{d : R | d ∈ normalizedFactors r} : Type u_1)) :
              (a : (↑{I : Ideal R | I ∈ normalizedFactors (span {r})} : Type u_1)) →
                (↑{d : R | d ∈ normalizedFactors r} : Type u_1))
            I) :
        R)
      r =
    emultiplicity (↑I : Ideal R) (span {r})

Tactic:
obtain ⟨a, ha⟩ := x
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
inst_3 : NormalizationMonoid R
inst_4 : DecidableEq R
r X : R
hr : r ≠ 0
hX : Prime X
⊢ emultiplicity (α := Ideal R) (span {X}) (span {r}) = emultiplicity X r

Tactic:
have := emultiplicity_eq_emultiplicity_span (R := R) (a := X) (b := r)
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
inst_3 : NormalizationMonoid R
inst_4 : DecidableEq R
r X : R
hr : r ≠ 0
hX : Prime X
this : emultiplicity (α := Ideal R) (span {X}) (span {r}) = emultiplicity X r
rw :
  ∀
    (this :
      Multiset.count (α := Ideal R) (span {X}) (normalizedFactors (span {r})) =
        Multiset.count ((normalize : (a : R) → R) X) (normalizedFactors r)),
    Multiset.count (α := Ideal R) (span {X}) (normalizedFactors (span {r})) =
      Multiset.count ((normalize : (a : R) → R) X) (normalizedFactors r)
rw₁ :
  ∀
    (this :
      emultiplicity (α := Ideal R) (span {X}) (span {r}) =
        (↑(Multiset.count ((normalize : (a : R) → R) X) (normalizedFactors r)) : ℕ∞)),
    Ne (α := Ideal R) (span {r}) 0
rw₂ :
  ∀
    (this :
      emultiplicity (α := Ideal R) (span {X}) (span {r}) =
        (↑(Multiset.count ((normalize : (a : R) → R) X) (normalizedFactors r)) : ℕ∞)),
    Prime (M := Ideal R) (span {X})
⊢ Multiset.count (α := Ideal R) (span {X}) (normalizedFactors (span {r})) =
    Multiset.count ((normalize : (a : R) → R) X) (normalizedFactors r)

Tactic:
rw [emultiplicity_eq_count_normalizedFactors (Prime.irreducible hX) hr,
    emultiplicity_eq_count_normalizedFactors (Prime.irreducible ?_), normalize_apply,
    normUnit_eq_one, Units.val_one, one_eq_top, mul_top, Nat.cast_inj] at this

Premises used: Prime.irreducible, normUnit_eq_one, Ideal.one_eq_top, normalize_apply, Nat.cast_inj, UniqueFactorizationMonoid.emultiplicity_eq_count_normalizedFactors, Units.val_one, Ideal.mul_top
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
inst_3 : NormalizationMonoid R
inst_4 : DecidableEq R
r X : R
hr : r ≠ 0
hX : Prime X
this :
  Multiset.count (α := Ideal R) (span {X}) (normalizedFactors (span {r})) =
    Multiset.count ((normalize : (a : R) → R) X) (normalizedFactors r)
⊢ Multiset.count (α := Ideal R) (span {X}) (normalizedFactors (span {r})) =
    Multiset.count ((normalize : (a : R) → R) X) (normalizedFactors r)

Tactic:
simp only [normalize_apply, this]

Premises used: normalize_apply
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
inst_3 : NormalizationMonoid R
inst_4 : DecidableEq R
r X : R
hr : r ≠ 0
hX : Prime X
this :
  emultiplicity (α := Ideal R) (span {X}) (span {r}) =
    (↑(Multiset.count ((normalize : (a : R) → R) X) (normalizedFactors r)) : ℕ∞)
⊢ Ne (α := Ideal R) (span {r}) 0

Tactic:
simp only [Submodule.zero_eq_bot, ne_eq, span_singleton_eq_bot, hr, not_false_eq_true]

Premises used: Ideal.span_singleton_eq_bot, ne_eq, Submodule.zero_eq_bot, not_false_eq_true
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
inst_3 : NormalizationMonoid R
inst_4 : DecidableEq R
r X : R
hr : r ≠ 0
hX : Prime X
this :
  emultiplicity (α := Ideal R) (span {X}) (span {r}) =
    (↑(Multiset.count ((normalize : (a : R) → R) X) (normalizedFactors r)) : ℕ∞)
⊢ Prime (M := Ideal R) (span {X})

Tactic:
simpa only [prime_span_singleton_iff]

Premises used: Ideal.prime_span_singleton_iff
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
inst_3 : NormalizationMonoid R
inst_4 : DecidableEq R
r X : R
hr : r ≠ 0
hX₁ : Eq (α := Rˣ) (normUnit X) 1
hX : Prime X
⊢ Multiset.count (α := Ideal R) (span {X}) (normalizedFactors (span {r})) = Multiset.count X (normalizedFactors r)

Tactic:
simpa [hX₁, normalize_apply] using count_span_normalizedFactors_eq hr hX

Premises used: normalize_apply, Ideal.count_span_normalizedFactors_eq
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_4
inst : CommRing A
p : Ideal A
hpb : p ≠ ⊥
hpm : p.IsMaximal
B : Type u_5
inst_1 : CommRing B
inst_2 : IsDedekindDomain B
inst_3 : Algebra A B
inst_4 : IsDomain A
inst_5 : IsTorsionFree A B
h :
  ∀ (x : Ideal B),
    x ∈ (↑(primesOverFinset p B) : Set (Ideal B)) ↔ Membership.mem (γ := Set (Ideal B)) (p.primesOver B) x
⊢ (↑(primesOverFinset p B) : Set (Ideal B)) = p.primesOver B

Tactic:
ext
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_4
inst : CommRing A
p : Ideal A
hpb : p ≠ ⊥
hpm : p.IsMaximal
B : Type u_5
inst_1 : CommRing B
inst_2 : IsDedekindDomain B
inst_3 : Algebra A B
inst_4 : IsDomain A
inst_5 : IsTorsionFree A B
x : Ideal B
⊢ x ∈ (↑(primesOverFinset p B) : Set (Ideal B)) ↔ Membership.mem (γ := Set (Ideal B)) (p.primesOver B) x

Tactic:
simpa using (mem_primesOver_iff_mem_normalizedFactors _ hpb).symm

Premises used: Ideal.mem_primesOver_iff_mem_normalizedFactors, Iff.symm
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_4
inst : CommRing A
p : Ideal A
hpb : p ≠ ⊥
hpm : p.IsMaximal
B : Type u_5
inst_1 : CommRing B
inst_2 : IsDedekindDomain B
inst_3 : Algebra A B
inst_4 : IsDomain A
inst_5 : IsTorsionFree A B
P : Ideal B
rw : P ∈ (↑(primesOverFinset p B) : Set (Ideal B)) ↔ Membership.mem (γ := Set (Ideal B)) (p.primesOver B) P
rw₁ rw₂ :
  Membership.mem (γ := Set (Ideal B)) (p.primesOver B) P ↔ Membership.mem (γ := Set (Ideal B)) (p.primesOver B) P
⊢ Membership.mem (γ := Finset (Ideal B)) (primesOverFinset p B) P ↔
    Membership.mem (γ := Set (Ideal B)) (p.primesOver B) P

Tactic:
rw [← Finset.mem_coe, coe_primesOverFinset hpb]

Premises used: IsDedekindDomain.coe_primesOverFinset, Finset.mem_coe
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
inst : CommRing R
A : Type u_4
inst_1 : CommRing A
inst_2 : IsDomain A
inst_3 : IsLocalRing A
inst_4 : IsDedekindDomain A
inst_5 : Algebra R A
inst_6 : FaithfulSMul R A
inst_7 : Module.Finite R A
p : Ideal R
inst_8 : p.IsMaximal
hp0 : p ≠ ⊥
⊢ IsDomain R

Tactic:
have : IsDomain R := .of_faithfulSMul R A
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
inst : CommRing R
A : Type u_4
inst_1 : CommRing A
inst_2 : IsDomain A
inst_3 : IsLocalRing A
inst_4 : IsDedekindDomain A
inst_5 : Algebra R A
inst_6 : FaithfulSMul R A
inst_7 : Module.Finite R A
p : Ideal R
inst_8 : p.IsMaximal
hp0 : p ≠ ⊥
this : IsDomain R
rw : (↑(IsDedekindDomain.primesOverFinset p A) : Set (Ideal A)) = {maximalIdeal A}
rw₁ : Eq (α := Set (Ideal A)) (p.primesOver A) {maximalIdeal A}
rw₂ rw₃ : Eq (α := Set (Ideal A)) {maximalIdeal A} {maximalIdeal A}
⊢ Eq (α := Finset (Ideal A)) (IsDedekindDomain.primesOverFinset p A) {maximalIdeal A}

Tactic:
rw [← Finset.coe_eq_singleton, IsDedekindDomain.coe_primesOverFinset hp0,
    IsLocalRing.primesOver_eq A hp0]

Premises used: Finset.coe_eq_singleton, IsDedekindDomain.coe_primesOverFinset, IsLocalRing.primesOver_eq
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
A_1 : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing A_1
inst_2 : Field K
A : Type u_4
inst_3 : CommRing A
p : Ideal A
hpb : p ≠ ⊥
hpm : p.IsMaximal
B : Type u_5
inst_4 : CommRing B
inst_5 : IsDedekindDomain B
inst_6 : Algebra A B
inst_7 : IsDomain A
inst_8 : IsTorsionFree A B
hp : p ≠ 0
v : HeightOneSpectrum B
hv :
  Membership.mem (γ := Set (HeightOneSpectrum B))
    (fun (v : HeightOneSpectrum B) ↦ ∃ (c : Ideal B), map (F := A →+* B) (algebraMap A B) p = v.asIdeal * c) v
rwa rwa₁ rwa₂ rwa₃ : v.asIdeal ∣ map (F := A →+* B) (algebraMap A B) p
⊢ v.asIdeal.LiesOver p

Tactic:
rwa [liesOver_iff_dvd_map v.isPrime.ne_top]

Premises used: Ideal.liesOver_iff_dvd_map, IsDedekindDomain.HeightOneSpectrum.isPrime, Ideal.IsPrime.ne_top
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_4
inst : CommRing A
p : Ideal A
hpm : p.IsMaximal
B : Type u_5
inst_1 : CommRing B
inst_2 : IsDedekindDomain B
inst_3 : Algebra A B
inst_4 : IsDomain A
inst_5 : IsTorsionFree A B
hp : p ≠ 0
v : { v : HeightOneSpectrum B // v.asIdeal ∣ map (F := A →+* B) (algebraMap A B) p }
⊢ (↑((equivPrimesOver B hp :
            (a : { v : HeightOneSpectrum B // v.asIdeal ∣ map (algebraMap A B) p }) → (↑(p.primesOver B) : Type u_5))
          v) :
      Ideal B) =
    (↑v : HeightOneSpectrum B).asIdeal

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_4
inst : CommRing A
p : Ideal A
hpm : p.IsMaximal
B : Type u_5
inst_1 : CommRing B
inst_2 : IsDedekindDomain B
inst_3 : Algebra A B
inst_4 : IsDomain A
inst_5 : IsTorsionFree A B
inst_6 : Algebra.IsIntegral A B
pos : ∀ (hpb : p = ⊥), Set.Finite (α := Ideal B) (p.primesOver B)
neg : ∀ (hpb : ¬p = ⊥), Set.Finite (α := Ideal B) (p.primesOver B)
⊢ Set.Finite (α := Ideal B) (p.primesOver B)

Tactic:
by_cases hpb : p = ⊥
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_4
inst : CommRing A
p : Ideal A
hpm : p.IsMaximal
B : Type u_5
inst_1 : CommRing B
inst_2 : IsDedekindDomain B
inst_3 : Algebra A B
inst_4 : IsDomain A
inst_5 : IsTorsionFree A B
inst_6 : Algebra.IsIntegral A B
hpb : p = ⊥
pos :
  ∀ (hpm : IsMaximal.{u_4} (α := A) ⊥) (B : Type u_5) [inst_7 : CommRing B] [IsDedekindDomain B] [inst_9 : Algebra A B]
    [IsDomain A] [IsTorsionFree A B] [Algebra.IsIntegral A B] (hpb : p = ⊥),
    Set.Finite (α := Ideal B) (primesOver.{u_4, u_5} (A := A) ⊥ B)
⊢ Set.Finite (α := Ideal B) (p.primesOver B)

Tactic:
rw [hpb] at hpm ⊢
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_4
inst : CommRing A
p : Ideal A
hpm : IsMaximal.{u_4} (α := A) ⊥
B : Type u_5
inst_1 : CommRing B
inst_2 : IsDedekindDomain B
inst_3 : Algebra A B
inst_4 : IsDomain A
inst_5 : IsTorsionFree A B
inst_6 : Algebra.IsIntegral A B
hpb : p = ⊥
⊢ IsDomain A

Tactic:
haveI : IsDomain A := IsDomain.of_bot_isPrime A
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_4
inst : CommRing A
p : Ideal A
hpm : IsMaximal.{u_4} (α := A) ⊥
B : Type u_5
inst_1 : CommRing B
inst_2 : IsDedekindDomain B
inst_3 : Algebra A B
inst_4 : IsDomain A
inst_5 : IsTorsionFree A B
inst_6 : Algebra.IsIntegral A B
hpb : p = ⊥
this : IsDomain A
pos : Set.Finite (α := Ideal B) {⊥}
⊢ Set.Finite (α := Ideal B) (primesOver.{u_4, u_5} (A := A) ⊥ B)

Tactic:
rw [primesOver_bot A B]

Premises used: Ideal.primesOver_bot
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_4
inst : CommRing A
p : Ideal A
hpm : IsMaximal.{u_4} (α := A) ⊥
B : Type u_5
inst_1 : CommRing B
inst_2 : IsDedekindDomain B
inst_3 : Algebra A B
inst_4 : IsDomain A
inst_5 : IsTorsionFree A B
inst_6 : Algebra.IsIntegral A B
hpb : p = ⊥
this : IsDomain A
⊢ Set.Finite (α := Ideal B) {⊥}

Tactic:
Set.finite_singleton ⊥

Premises used: Bot.bot, Set.finite_singleton
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_4
inst : CommRing A
p : Ideal A
hpm : IsMaximal.{u_4} (α := A) ⊥
B : Type u_5
inst_1 : CommRing B
inst_2 : IsDedekindDomain B
inst_3 : Algebra A B
inst_4 : IsDomain A
inst_5 : IsTorsionFree A B
inst_6 : Algebra.IsIntegral A B
hpb : p = ⊥
this : IsDomain A
⊢ Set.Finite (α := Ideal B) {⊥}

Tactic:
exact Set.finite_singleton ⊥

Premises used: Bot.bot, Set.finite_singleton
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_4
inst : CommRing A
p : Ideal A
hpm : p.IsMaximal
B : Type u_5
inst_1 : CommRing B
inst_2 : IsDedekindDomain B
inst_3 : Algebra A B
inst_4 : IsDomain A
inst_5 : IsTorsionFree A B
inst_6 : Algebra.IsIntegral A B
hpb : ¬p = ⊥
neg : (↑(primesOverFinset p B) : Set (Ideal B)).Finite
⊢ Set.Finite (α := Ideal B) (p.primesOver B)

Tactic:
rw [← coe_primesOverFinset hpb B]

Premises used: IsDedekindDomain.coe_primesOverFinset
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_4
inst : CommRing A
p : Ideal A
hpm : p.IsMaximal
B : Type u_5
inst_1 : CommRing B
inst_2 : IsDedekindDomain B
inst_3 : Algebra A B
inst_4 : IsDomain A
inst_5 : IsTorsionFree A B
inst_6 : Algebra.IsIntegral A B
hpb : ¬p = ⊥
⊢ (↑(primesOverFinset p B) : Set (Ideal B)).Finite

Tactic:
(primesOverFinset p B).finite_toSet

Premises used: IsDedekindDomain.primesOverFinset, Finset.finite_toSet
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_4
inst : CommRing A
p : Ideal A
hpm : p.IsMaximal
B : Type u_5
inst_1 : CommRing B
inst_2 : IsDedekindDomain B
inst_3 : Algebra A B
inst_4 : IsDomain A
inst_5 : IsTorsionFree A B
inst_6 : Algebra.IsIntegral A B
hpb : ¬p = ⊥
⊢ (↑(primesOverFinset p B) : Set (Ideal B)).Finite

Tactic:
exact (primesOverFinset p B).finite_toSet

Premises used: IsDedekindDomain.primesOverFinset, Finset.finite_toSet