awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
T : Type u_4
inst : CommRing T
inst_1 : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : Irreducible J
n : ℕ
hn : emultiplicity J I ≤ (↑n : ℕ∞)
rw : J ^ count J (normalizedFactors I) = J ^ multiplicity J I
rw₁ : count J (normalizedFactors I) ≤ n
⊢ J ^ n ⊔ I = J ^ multiplicity J I

Tactic:
rw [irreducible_pow_sup hI hJ, min_eq_left]

Premises used: Ideal.irreducible_pow_sup, min_eq_left
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
T : Type u_4
inst : CommRing T
inst_1 : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : Irreducible J
n : ℕ
hn : emultiplicity J I ≤ (↑n : ℕ∞)
e_a : count J (normalizedFactors I) = multiplicity J I
⊢ J ^ count J (normalizedFactors I) = J ^ multiplicity J I

Tactic:
congr
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
T : Type u_4
inst : CommRing T
inst_1 : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : Irreducible J
n : ℕ
hn : emultiplicity J I ≤ (↑n : ℕ∞)
e_a : FiniteMultiplicity J I
⊢ count J (normalizedFactors I) = multiplicity J I

Tactic:
rw [← Nat.cast_inj (R := ℕ∞), ← FiniteMultiplicity.emultiplicity_eq_multiplicity,
      emultiplicity_eq_count_normalizedFactors hJ hI, normalize_eq J]

Premises used: FiniteMultiplicity.emultiplicity_eq_multiplicity, Nat.cast_inj, UniqueFactorizationMonoid.emultiplicity_eq_count_normalizedFactors, normalize_eq
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
T : Type u_4
inst : CommRing T
inst_1 : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : Irreducible J
n : ℕ
hn : emultiplicity J I ≤ (↑n : ℕ∞)
e_a : emultiplicity J I < ⊤
⊢ FiniteMultiplicity J I

Tactic:
rw [← emultiplicity_lt_top]

Premises used: emultiplicity_lt_top
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
T : Type u_4
inst : CommRing T
inst_1 : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : Irreducible J
n : ℕ
hn : emultiplicity J I ≤ (↑n : ℕ∞)
e_a : LT.lt (α := ℕ∞) (↑n : ℕ∞) ⊤
⊢ emultiplicity J I < ⊤

Tactic:
apply hn.trans_lt

Premises used: LE.le.trans_lt
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
T : Type u_4
inst : CommRing T
inst_1 : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : Irreducible J
n : ℕ
hn : emultiplicity J I ≤ (↑n : ℕ∞)
⊢ LT.lt (α := ℕ∞) (↑n : ℕ∞) ⊤

Tactic:
simp
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
T : Type u_4
inst : CommRing T
inst_1 : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : Irreducible J
n : ℕ
hn : emultiplicity J I ≤ (↑n : ℕ∞)
⊢ LE.le (α := ℕ∞) (↑(count J (normalizedFactors I)) : ℕ∞) (↑n : ℕ∞)

Tactic:
rw [emultiplicity_eq_count_normalizedFactors hJ hI, normalize_eq J] at hn

Premises used: UniqueFactorizationMonoid.emultiplicity_eq_count_normalizedFactors, normalize_eq
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
T : Type u_4
inst : CommRing T
inst_1 : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : Irreducible J
n : ℕ
hn : LE.le (α := ℕ∞) (↑(count J (normalizedFactors I)) : ℕ∞) (↑n : ℕ∞)
⊢ count J (normalizedFactors I) ≤ n

Tactic:
exact_mod_cast hn
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
T : Type u_4
inst : CommRing T
inst_1 : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : Irreducible J
n : ℕ
hn : emultiplicity J I ≤ (↑n : ℕ∞)
rw : J ^ min (count J (normalizedFactors I)) n = J ^ multiplicity J I
rw₁ : J ^ count J (normalizedFactors I) = J ^ multiplicity J I
rw₂ : count J (normalizedFactors I) ≤ n
rw₃ : J ^ count J (normalizedFactors I) = J ^ multiplicity J I
rw₄ : count J (normalizedFactors I) ≤ n
rw₅ : J ^ count J (normalizedFactors I) = J ^ multiplicity J I
rw₆ rw₇ : count J (normalizedFactors I) ≤ n
⊢ J ^ n ⊔ I = J ^ multiplicity J I

Tactic:
classical
  rw [irreducible_pow_sup hI hJ, min_eq_left]
  · congr
    rw [← Nat.cast_inj (R := ℕ∞), ← FiniteMultiplicity.emultiplicity_eq_multiplicity,
      emultiplicity_eq_count_normalizedFactors hJ hI, normalize_eq J]
    rw [← emultiplicity_lt_top]
    apply hn.trans_lt
    simp
  · rw [emultiplicity_eq_count_normalizedFactors hJ hI, normalize_eq J] at hn
    exact_mod_cast hn

Premises used: Ideal.irreducible_pow_sup, FiniteMultiplicity.emultiplicity_eq_multiplicity, Nat.cast_inj, min_eq_left, emultiplicity_lt_top, UniqueFactorizationMonoid.emultiplicity_eq_count_normalizedFactors, LE.le.trans_lt, normalize_eq
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
T : Type u_4
inst : CommRing T
inst_1 : IsDedekindDomain T
I : Ideal T
hI : I ≠ ⊥
P : Ideal T
hpm : P.IsMaximal
h :
  P ⊔ (filter (fun (x : Ideal T) ↦ ¬P = x) (normalizedFactors I)).prod = ⊤ ∧
    I = P ^ count P (normalizedFactors I) * (filter (fun (x : Ideal T) ↦ ¬P = x) (normalizedFactors I)).prod
⊢ ∃ (Q : Ideal T), P ⊔ Q = ⊤ ∧ I = P ^ count P (normalizedFactors I) * Q

Tactic:
use (filter (¬ P = ·) (normalizedFactors I)).prod

Premises used: UniqueFactorizationMonoid.normalizedFactors, Multiset.prod, Eq, Not, Multiset.filter
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
T : Type u_4
inst : CommRing T
inst_1 : IsDedekindDomain T
I : Ideal T
hI : I ≠ ⊥
P : Ideal T
hpm : P.IsMaximal
h : P ⊔ (filter (fun (x : Ideal T) ↦ ¬P = x) (normalizedFactors I)).prod = ⊤
h₁ : I = P ^ count P (normalizedFactors I) * (filter (fun (x : Ideal T) ↦ ¬P = x) (normalizedFactors I)).prod
⊢ P ⊔ (filter (fun (x : Ideal T) ↦ ¬P = x) (normalizedFactors I)).prod = ⊤ ∧
    I = P ^ count P (normalizedFactors I) * (filter (fun (x : Ideal T) ↦ ¬P = x) (normalizedFactors I)).prod

Tactic:
constructor
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
T : Type u_4
inst : CommRing T
inst_1 : IsDedekindDomain T
I : Ideal T
hI : I ≠ ⊥
P : Ideal T
hpm : P.IsMaximal
⊢ P ⊔ (filter (fun (x : Ideal T) ↦ ¬P = x) (normalizedFactors I)).prod = ⊤

Tactic:
P.sup_multiset_prod_eq_top (fun p hpi ↦ ?_)

Premises used: Set.Mem, setOf, Ideal.sup_multiset_prod_eq_top
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
T : Type u_4
inst : CommRing T
inst_1 : IsDedekindDomain T
I : Ideal T
hI : I ≠ ⊥
P : Ideal T
hpm : P.IsMaximal
h : ∀ (p : Ideal T) (hpi : p ∈ filter (fun (x : Ideal T) ↦ ¬P = x) (normalizedFactors I)), P ⊔ p = ⊤
⊢ P ⊔ (filter (fun (x : Ideal T) ↦ ¬P = x) (normalizedFactors I)).prod = ⊤

Tactic:
refine P.sup_multiset_prod_eq_top (fun p hpi ↦ ?_)

Premises used: Ideal.sup_multiset_prod_eq_top
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
T : Type u_4
inst : CommRing T
inst_1 : IsDedekindDomain T
I : Ideal T
hI : I ≠ ⊥
P : Ideal T
hpm : P.IsMaximal
p : Ideal T
hpi : p ∈ filter (fun (x : Ideal T) ↦ ¬P = x) (normalizedFactors I)
⊢ Prime p

Tactic:
have hp : Prime p := prime_of_normalized_factor p (filter_subset _ (normalizedFactors I) hpi)
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
T : Type u_4
inst : CommRing T
inst_1 : IsDedekindDomain T
I : Ideal T
hI : I ≠ ⊥
P : Ideal T
hpm : P.IsMaximal
p : Ideal T
hpi : p ∈ filter (fun (x : Ideal T) ↦ ¬P = x) (normalizedFactors I)
hp : Prime p
⊢ P ⊔ p = ⊤

Tactic:
hpm.coprime_of_ne ((isPrime_of_prime hp).isMaximal hp.ne_zero) (of_mem_filter hpi)

Premises used: Set.Mem, Ideal.IsPrime.isMaximal, setOf, Multiset.of_mem_filter, Ideal.IsMaximal.coprime_of_ne, Prime.ne_zero, Ideal.isPrime_of_prime
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
T : Type u_4
inst : CommRing T
inst_1 : IsDedekindDomain T
I : Ideal T
hI : I ≠ ⊥
P : Ideal T
hpm : P.IsMaximal
p : Ideal T
hpi : p ∈ filter (fun (x : Ideal T) ↦ ¬P = x) (normalizedFactors I)
hp : Prime p
⊢ P ⊔ p = ⊤

Tactic:
exact hpm.coprime_of_ne ((isPrime_of_prime hp).isMaximal hp.ne_zero) (of_mem_filter hpi)

Premises used: Ideal.IsPrime.isMaximal, Multiset.of_mem_filter, Ideal.IsMaximal.coprime_of_ne, Prime.ne_zero, Ideal.isPrime_of_prime
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
T : Type u_4
inst : CommRing T
inst_1 : IsDedekindDomain T
I : Ideal T
hI : I ≠ ⊥
P : Ideal T
hpm : P.IsMaximal
h :
  (filter (fun (x : Ideal T) ↦ P = x) (normalizedFactors I) +
        filter (fun (a : Ideal T) ↦ ¬P = a) (normalizedFactors I)).prod =
    P ^ count P (normalizedFactors I) * (filter (fun (x : Ideal T) ↦ ¬P = x) (normalizedFactors I)).prod
⊢ I = P ^ count P (normalizedFactors I) * (filter (fun (x : Ideal T) ↦ ¬P = x) (normalizedFactors I)).prod

Tactic:
nth_rw 1 [← prod_normalizedFactors_eq_self hI, ← filter_add_not (P = ·) (normalizedFactors I)]

Premises used: UniqueFactorizationMonoid.normalizedFactors, Multiset.filter_add_not, Ideal.prod_normalizedFactors_eq_self, Eq
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
T : Type u_4
inst : CommRing T
inst_1 : IsDedekindDomain T
I : Ideal T
hI : I ≠ ⊥
P : Ideal T
hpm : P.IsMaximal
h :
  (filter (fun (x : Ideal T) ↦ P = x) (normalizedFactors I)).prod *
      (filter (fun (a : Ideal T) ↦ ¬P = a) (normalizedFactors I)).prod =
    P ^ count P (normalizedFactors I) * (filter (fun (x : Ideal T) ↦ ¬P = x) (normalizedFactors I)).prod
h₁ h₂ :
  (filter (fun (x : Ideal T) ↦ P = x) (normalizedFactors I)).prod *
      (filter (fun (a : Ideal T) ↦ ¬P = a) (normalizedFactors I)).prod =
    (filter (Eq P) (normalizedFactors I)).prod * (filter (fun (x : Ideal T) ↦ ¬P = x) (normalizedFactors I)).prod
⊢ (filter (fun (x : Ideal T) ↦ P = x) (normalizedFactors I) +
        filter (fun (a : Ideal T) ↦ ¬P = a) (normalizedFactors I)).prod =
    P ^ count P (normalizedFactors I) * (filter (fun (x : Ideal T) ↦ ¬P = x) (normalizedFactors I)).prod

Tactic:
rw [prod_add, pow_count]

Premises used: Multiset.pow_count, Multiset.prod_add
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
T : Type u_4
inst : CommRing T
inst_1 : IsDedekindDomain T
R : Type u_5
inst_2 : CommRing R
inst_3 : IsDedekindDomain R
f : T ≃+* R
I : Ideal T
hI : Prime I
h : I ≠ ⊥
⊢ I.IsPrime

Tactic:
rw [prime_iff_isPrime h] at hI

Premises used: Ideal.prime_iff_isPrime
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
T : Type u_4
inst : CommRing T
inst_1 : IsDedekindDomain T
R : Type u_5
inst_2 : CommRing R
inst_3 : IsDedekindDomain R
f : T ≃+* R
I : Ideal T
hI : Prime I
h : I ≠ ⊥
hI₁ : I.IsPrime
⊢ I ≠ ⊥

Tactic:
rw [prime_iff_isPrime h] at hI

Premises used: Ideal.prime_iff_isPrime
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
T : Type u_4
inst : CommRing T
inst_1 : IsDedekindDomain T
R : Type u_5
inst_2 : CommRing R
inst_3 : IsDedekindDomain R
f : T ≃+* R
I : Ideal T
hI : I.IsPrime
h : I ≠ ⊥
⊢ Prime.{u_5} (M := Ideal R) (map f I)

Tactic:
(prime_iff_isPrime <| (I.map_eq_bot_iff_of_injective f.injective).not.2 h).2
    (map_isPrime_of_equiv _)

Premises used: Iff.mpr, RingEquiv.injective, Iff.not, Ideal.map_eq_bot_iff_of_injective, Ideal.map_isPrime_of_equiv, Ideal.prime_iff_isPrime
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
T : Type u_4
inst : CommRing T
inst_1 : IsDedekindDomain T
R : Type u_5
inst_2 : CommRing R
inst_3 : IsDedekindDomain R
f : T ≃+* R
I : Ideal T
hI : I.IsPrime
h : I ≠ ⊥
⊢ Prime.{u_5} (M := Ideal R) (map f I)

Tactic:
exact (prime_iff_isPrime <| (I.map_eq_bot_iff_of_injective f.injective).not.2 h).2
    (map_isPrime_of_equiv _)

Premises used: Iff.mpr, RingEquiv.injective, Iff.not, Ideal.map_eq_bot_iff_of_injective, Ideal.map_isPrime_of_equiv, Ideal.prime_iff_isPrime
-- 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 : IsDedekindDomain R
v : HeightOneSpectrum R
⊢ v.asIdeal.IsMaximal

Tactic:
v.isPrime.isMaximal v.ne_bot

Premises used: Ideal.IsPrime.isMaximal, IsDedekindDomain.HeightOneSpectrum.ne_bot, IsDedekindDomain.HeightOneSpectrum.isPrime
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
⊢ Prime v.asIdeal

Tactic:
Ideal.prime_of_isPrime v.ne_bot v.isPrime

Premises used: IsDedekindDomain.HeightOneSpectrum.ne_bot, IsDedekindDomain.HeightOneSpectrum.isPrime, Ideal.prime_of_isPrime
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
inst : CommRing R
⊢ Function.Injective.{u_1 + 1, u_1 + 1} (α := HeightOneSpectrum R) asIdeal

Tactic:
fun ⦃_ _⦄ h ↦ HeightOneSpectrum.ext h

Premises used: IsDedekindDomain.HeightOneSpectrum.ext, Function.Injective
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
⊢ ofPrime ⋯ = v

Tactic:
rfl

Premises used: IsDedekindDomain.HeightOneSpectrum.ofPrime, rfl
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
⊢ Irreducible v.asIdeal

Tactic:
UniqueFactorizationMonoid.irreducible_iff_prime.mpr v.prime

Premises used: Iff.mpr, UniqueFactorizationMonoid.irreducible_iff_prime, IsDedekindDomain.HeightOneSpectrum.prime
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
⊢ Irreducible (M := Associates (Ideal R)) (Associates.mk v.asIdeal)

Tactic:
Associates.irreducible_mk.mpr v.irreducible

Premises used: Iff.mpr, Associates.irreducible_mk, IsDedekindDomain.HeightOneSpectrum.irreducible
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
hR : ¬IsField R
I : Ideal R
rw : (∃ (M : Ideal R), M.IsMaximal ∧ I ≤ M) ↔ ∃ (P : HeightOneSpectrum R), I ≤ P.asIdeal
⊢ I ≠ ⊤ ↔ ∃ (P : HeightOneSpectrum R), I ≤ P.asIdeal

Tactic:
rw [Ideal.ne_top_iff_exists_maximal]

Premises used: Ideal.ne_top_iff_exists_maximal
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
hR : ¬IsField R
I : Ideal R
mp : (∃ (M : Ideal R), M.IsMaximal ∧ I ≤ M) → ∃ (P : HeightOneSpectrum R), I ≤ P.asIdeal
mpr : (∃ (P : HeightOneSpectrum R), I ≤ P.asIdeal) → ∃ (M : Ideal R), M.IsMaximal ∧ I ≤ M
⊢ (∃ (M : Ideal R), M.IsMaximal ∧ I ≤ M) ↔ ∃ (P : HeightOneSpectrum R), I ≤ P.asIdeal

Tactic:
constructor
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
hR : ¬IsField R
I M : Ideal R
hMmax : M.IsMaximal
hIM : I ≤ M
⊢ ∃ (P : HeightOneSpectrum R), I ≤ P.asIdeal

Tactic:
⟨(equivMaximalSpectrum hR).symm ⟨M, hMmax⟩, hIM⟩

Premises used: MaximalSpectrum.mk, IsDedekindDomain.HeightOneSpectrum.equivMaximalSpectrum, Exists.intro, Equiv.symm, DFunLike.coe
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
hR : ¬IsField R
I M : Ideal R
hMmax : M.IsMaximal
hIM : I ≤ M
⊢ ∃ (P : HeightOneSpectrum R), I ≤ P.asIdeal

Tactic:
exact ⟨(equivMaximalSpectrum hR).symm ⟨M, hMmax⟩, hIM⟩
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
hR : ¬IsField R
I : Ideal R
P : HeightOneSpectrum R
hP : I ≤ P.asIdeal
⊢ ∃ (M : Ideal R), M.IsMaximal ∧ I ≤ M

Tactic:
⟨((equivMaximalSpectrum hR) P).asIdeal, ((equivMaximalSpectrum hR) P).isMaximal, hP⟩

Premises used: MaximalSpectrum.asIdeal, MaximalSpectrum.isMaximal, IsDedekindDomain.HeightOneSpectrum.equivMaximalSpectrum, And.intro, Exists.intro, DFunLike.coe
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
hR : ¬IsField R
I : Ideal R
P : HeightOneSpectrum R
hP : I ≤ P.asIdeal
⊢ ∃ (M : Ideal R), M.IsMaximal ∧ I ≤ M

Tactic:
exact ⟨((equivMaximalSpectrum hR) P).asIdeal, ((equivMaximalSpectrum hR) P).isMaximal, hP⟩
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
P Q : HeightOneSpectrum R
hPQ : P ≠ Q
⊢ P.asIdeal ≠ Q.asIdeal

Tactic:
simpa [HeightOneSpectrum.ext_iff] using hPQ

Premises used: IsDedekindDomain.HeightOneSpectrum.ext_iff
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
P Q : HeightOneSpectrum R
hPQ : P ≠ Q
n m : ℕ
⊢ IsCoprime (P.asIdeal ^ n) (Q.asIdeal ^ m)

Tactic:
Ideal.isCoprime_iff_sup_eq.mpr (Ideal.pow_sup_pow_eq_top (P.isCoprime_of_ne Q hPQ).sup_eq)

Premises used: Iff.mpr, IsDedekindDomain.HeightOneSpectrum.isCoprime_of_ne, Ideal.pow_sup_pow_eq_top, IsCoprime.sup_eq, Ideal.isCoprime_iff_sup_eq
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
K : Type u_3
inst : CommRing R
inst_1 : Field K
inst_2 : IsDedekindDomain R
inst_3 : Algebra R K
hK : IsFractionRing R K
h :
  ∀ (x : K),
    Membership.mem (γ := Subalgebra R K)
        (⨅ (v : HeightOneSpectrum R), Localization.subalgebra.ofField K v.asIdeal.primeCompl ⋯) x ↔
      Membership.mem (γ := Subalgebra R K) ⊥ x
⊢ Eq.{u_3 + 1} (α := Subalgebra R K)
    (⨅ (v : HeightOneSpectrum R), Localization.subalgebra.ofField K v.asIdeal.primeCompl ⋯) ⊥

Tactic:
ext x
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
K : Type u_3
inst : CommRing R
inst_1 : Field K
inst_2 : IsDedekindDomain R
inst_3 : Algebra R K
hK : IsFractionRing R K
x : K
h :
  (∀ (i : HeightOneSpectrum R),
      Membership.mem (γ := Subalgebra R K) (Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯) x) ↔
    Membership.mem (γ := Subalgebra R K) ⊥ x
⊢ Membership.mem (γ := Subalgebra R K)
      (⨅ (v : HeightOneSpectrum R), Localization.subalgebra.ofField K v.asIdeal.primeCompl ⋯) x ↔
    Membership.mem (γ := Subalgebra R K) ⊥ x

Tactic:
rw [Algebra.mem_iInf]

Premises used: Algebra.mem_iInf
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
K : Type u_3
inst : CommRing R
inst_1 : Field K
inst_2 : IsDedekindDomain R
inst_3 : Algebra R K
hK : IsFractionRing R K
x : K
h :
  (∀ (i : HeightOneSpectrum R),
      Membership.mem (γ := Subalgebra R K) (Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯) x) →
    Membership.mem (γ := Subalgebra R K) ⊥ x
h₁ :
  Membership.mem (γ := Subalgebra R K) ⊥ x →
    ∀ (i : HeightOneSpectrum R),
      Membership.mem (γ := Subalgebra R K) (Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯) x
⊢ (∀ (i : HeightOneSpectrum R),
      Membership.mem (γ := Subalgebra R K) (Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯) x) ↔
    Membership.mem (γ := Subalgebra R K) ⊥ x

Tactic:
constructor
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
K : Type u_3
inst : CommRing R
inst_1 : Field K
inst_2 : IsDedekindDomain R
inst_3 : Algebra R K
hK : IsFractionRing R K
x : K
pos :
  ∀ (hR : IsField R),
    (∀ (i : HeightOneSpectrum R),
        Membership.mem (γ := Subalgebra R K) (Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯) x) →
      Membership.mem (γ := Subalgebra R K) ⊥ x
neg :
  ∀ (hR : ¬IsField R),
    (∀ (i : HeightOneSpectrum R),
        Membership.mem (γ := Subalgebra R K) (Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯) x) →
      Membership.mem (γ := Subalgebra R K) ⊥ x
⊢ (∀ (i : HeightOneSpectrum R),
      Membership.mem (γ := Subalgebra R K) (Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯) x) →
    Membership.mem (γ := Subalgebra R K) ⊥ x

Tactic:
by_cases hR : IsField R

Premises used: IsField
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
K : Type u_3
inst : CommRing R
inst_1 : Field K
inst_2 : IsDedekindDomain R
inst_3 : Algebra R K
hK : IsFractionRing R K
x : K
pos :
  ∀ (hR : IsField R),
    (∀ (i : HeightOneSpectrum R),
        Membership.mem (γ := Subalgebra R K) (Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯) x) →
      Membership.mem (γ := Subalgebra R K) ⊥ x
neg :
  ∀ (hR : ¬IsField R),
    (∀ (i : HeightOneSpectrum R),
        Membership.mem (γ := Subalgebra R K) (Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯) x) →
      Membership.mem (γ := Subalgebra R K) ⊥ x
⊢ (∀ (i : HeightOneSpectrum R),
      Membership.mem (γ := Subalgebra R K) (Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯) x) →
    Membership.mem (γ := Subalgebra R K) ⊥ x

Tactic:
on_goal 1 => by_cases hR : IsField R

Premises used: IsField
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
K : Type u_3
inst : CommRing R
inst_1 : Field K
inst_2 : IsDedekindDomain R
inst_3 : Algebra R K
hK : IsFractionRing R K
x : K
hR : IsField R
pos :
  ∀ (algebra_map_inv : K → R),
    Function.LeftInverse algebra_map_inv (⇑(algebraMap R K) : (a : R) → K) →
      ∀ (algebra_map_right_inv : Function.RightInverse algebra_map_inv (⇑(algebraMap R K) : (a : R) → K)),
        (∀ (i : HeightOneSpectrum R),
            Membership.mem (γ := Subalgebra R K) (Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯) x) →
          Membership.mem (γ := Subalgebra R K) ⊥ x
⊢ (∀ (i : HeightOneSpectrum R),
      Membership.mem (γ := Subalgebra R K) (Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯) x) →
    Membership.mem (γ := Subalgebra R K) ⊥ x

Tactic:
rcases Function.bijective_iff_has_inverse.mp
      (IsField.localization_map_bijective (Rₘ := K) (flip nonZeroDivisors.ne_zero rfl : 0 ∉ R⁰) hR)
      with ⟨algebra_map_inv, _, algebra_map_right_inv⟩

Premises used: IsField.localization_map_bijective, flip, nonZeroDivisors.ne_zero, Function.bijective_iff_has_inverse, Iff.mp, rfl
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
K : Type u_3
inst : CommRing R
inst_1 : Field K
inst_2 : IsDedekindDomain R
inst_3 : Algebra R K
hK : IsFractionRing R K
x : K
hR : IsField R
algebra_map_inv : K → R
left : Function.LeftInverse algebra_map_inv (⇑(algebraMap R K) : (a : R) → K)
algebra_map_right_inv : Function.RightInverse algebra_map_inv (⇑(algebraMap R K) : (a : R) → K)
⊢ (∀ (i : HeightOneSpectrum R),
      Membership.mem (γ := Subalgebra R K) (Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯) x) →
    Membership.mem (γ := Subalgebra R K) ⊥ x

Tactic:
fun _ => Algebra.mem_bot.mpr ⟨algebra_map_inv x, algebra_map_right_inv x⟩

Premises used: Iff.mpr, Algebra.mem_bot, Exists.intro
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
K : Type u_3
inst : CommRing R
inst_1 : Field K
inst_2 : IsDedekindDomain R
inst_3 : Algebra R K
hK : IsFractionRing R K
x : K
hR : IsField R
algebra_map_inv : K → R
left : Function.LeftInverse algebra_map_inv (⇑(algebraMap R K) : (a : R) → K)
algebra_map_right_inv : Function.RightInverse algebra_map_inv (⇑(algebraMap R K) : (a : R) → K)
⊢ (∀ (i : HeightOneSpectrum R),
      Membership.mem (γ := Subalgebra R K) (Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯) x) →
    Membership.mem (γ := Subalgebra R K) ⊥ x

Tactic:
exact fun _ => Algebra.mem_bot.mpr ⟨algebra_map_inv x, algebra_map_right_inv x⟩

Premises used: Iff.mpr, Algebra.mem_bot, Exists.intro
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
K : Type u_3
inst : CommRing R
inst_1 : Field K
inst_2 : IsDedekindDomain R
inst_3 : Algebra R K
hK : IsFractionRing R K
x : K
hR : ¬IsField R
neg :
  (∀ (i : HeightOneSpectrum R),
      Membership.mem (γ := Subalgebra R K) (Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯) x) →
    ∀ (i : MaximalSpectrum R),
      Membership.mem (γ := Subalgebra R K) (Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯) x
⊢ (∀ (i : HeightOneSpectrum R),
      Membership.mem (γ := Subalgebra R K) (Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯) x) →
    Membership.mem (γ := Subalgebra R K) ⊥ x

Tactic:
rw [← MaximalSpectrum.iInf_localization_eq_bot, Algebra.mem_iInf]

Premises used: Algebra.mem_iInf, MaximalSpectrum.iInf_localization_eq_bot
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
K : Type u_3
inst : CommRing R
inst_1 : Field K
inst_2 : IsDedekindDomain R
inst_3 : Algebra R K
hK : IsFractionRing R K
x : K
h :
  (∀ (i : MaximalSpectrum R),
      Membership.mem (γ := Subalgebra R K) (Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯) x) →
    ∀ (i : HeightOneSpectrum R),
      Membership.mem (γ := Subalgebra R K) (Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯) x
⊢ Membership.mem (γ := Subalgebra R K) ⊥ x →
    ∀ (i : HeightOneSpectrum R),
      Membership.mem (γ := Subalgebra R K) (Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯) x

Tactic:
rw [← MaximalSpectrum.iInf_localization_eq_bot, Algebra.mem_iInf]

Premises used: Algebra.mem_iInf, MaximalSpectrum.iInf_localization_eq_bot