awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
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 : ℕ∞)
⊢ count J (normalizedFactors I) = multiplicity J I
have e_a : FiniteMultiplicity J I
Tactic: rw [← Nat.cast_inj (R := ℕ∞), ← FiniteMultiplicity.emultiplicity_eq_multiplicity,
      emultiplicity_eq_count_normalizedFactors hJ hI, normalize_eq J]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
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 : ℕ∞)
⊢ FiniteMultiplicity J I
have e_a : emultiplicity J I < ⊤
Tactic: rw [← emultiplicity_lt_top]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
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 : ℕ∞)
⊢ emultiplicity J I < ⊤
have e_a : LT.lt (α := ℕ∞) (↑n : ℕ∞) ⊤
Tactic: apply hn.trans_lt
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (hypothesis)
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 : ℕ∞)
⊢ count J (normalizedFactors I) ≤ n
have hn₁ : LE.le (α := ℕ∞) (↑(count J (normalizedFactors I)) : ℕ∞) (↑n : ℕ∞)
Tactic: rw [emultiplicity_eq_count_normalizedFactors hJ hI, normalize_eq J] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
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 : ℕ∞)
⊢ J ^ n ⊔ I = J ^ multiplicity J I
have rw : J ^ min (count J (normalizedFactors I)) n = 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
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
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
⊢ J ^ n ⊔ I = J ^ multiplicity J I
have rw₁ : J ^ count J (normalizedFactors 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
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
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
⊢ J ^ n ⊔ I = J ^ multiplicity J I
have rw₂ : count J (normalizedFactors I) ≤ n
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
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
T : Type u_4
inst : CommRing T
inst_1 : IsDedekindDomain T
I : Ideal T
hI : I ≠ ⊥
P : Ideal T
hpm : P.IsMaximal
⊢ ∃ (Q : Ideal T), P ⊔ Q = ⊤ ∧ I = P ^ count P (normalizedFactors I) * Q
have 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
Tactic: use (filter (¬ P = ·) (normalizedFactors I)).prod
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
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 = ⊤ ∧
    I = P ^ count P (normalizedFactors I) * (filter (fun (x : Ideal T) ↦ ¬P = x) (normalizedFactors I)).prod
have h : P ⊔ (filter (fun (x : Ideal T) ↦ ¬P = x) (normalizedFactors I)).prod = ⊤
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
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 = ⊤
⊢ 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
have h₁ : I = P ^ count P (normalizedFactors I) * (filter (fun (x : Ideal T) ↦ ¬P = x) (normalizedFactors I)).prod
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
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 = ⊤
have h : ∀ (p : Ideal T) (hpi : p ∈ filter (fun (x : Ideal T) ↦ ¬P = x) (normalizedFactors I)), P ⊔ p = ⊤
Tactic: refine P.sup_multiset_prod_eq_top (fun p hpi ↦ ?_)
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (hypothesis)
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)
⊢ P ⊔ p = ⊤
have hp : Prime p
Tactic: have hp : Prime p := prime_of_normalized_factor p (filter_subset _ (normalizedFactors I) hpi)
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
T : Type u_4
inst : CommRing T
inst_1 : IsDedekindDomain T
I : Ideal T
hI : I ≠ ⊥
P : Ideal T
hpm : P.IsMaximal
⊢ I = P ^ count P (normalizedFactors I) * (filter (fun (x : Ideal T) ↦ ¬P = x) (normalizedFactors I)).prod
have 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
Tactic: nth_rw 1 [← prod_normalizedFactors_eq_self hI, ← filter_add_not (P = ·) (normalizedFactors I)]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
T : Type u_4
inst : CommRing T
inst_1 : IsDedekindDomain T
I : Ideal T
hI : I ≠ ⊥
P : Ideal T
hpm : P.IsMaximal
⊢ (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
have 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
Tactic: rw [prod_add, pow_count]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
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
⊢ (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
have 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
Tactic: rw [prod_add, pow_count]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (hypothesis)
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 ≠ ⊥
⊢ Prime.{u_5} (M := Ideal R) (map f I)
have hI₁ : I.IsPrime
Tactic: rw [prime_iff_isPrime h] at hI
Cleared hypotheses: hI, h
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
hR : ¬IsField R
I : Ideal R
⊢ I ≠ ⊤ ↔ ∃ (P : HeightOneSpectrum R), I ≤ P.asIdeal
have rw : (∃ (M : Ideal R), M.IsMaximal ∧ I ≤ M) ↔ ∃ (P : HeightOneSpectrum R), I ≤ P.asIdeal
Tactic: rw [Ideal.ne_top_iff_exists_maximal]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
hR : ¬IsField R
I : Ideal R
⊢ (∃ (M : Ideal R), M.IsMaximal ∧ I ≤ M) ↔ ∃ (P : HeightOneSpectrum R), I ≤ P.asIdeal
have mp : (∃ (M : Ideal R), M.IsMaximal ∧ I ≤ M) → ∃ (P : HeightOneSpectrum R), I ≤ P.asIdeal
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
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
⊢ (∃ (M : Ideal R), M.IsMaximal ∧ I ≤ M) ↔ ∃ (P : HeightOneSpectrum R), I ≤ P.asIdeal
have mpr : (∃ (P : HeightOneSpectrum R), I ≤ P.asIdeal) → ∃ (M : Ideal R), M.IsMaximal ∧ I ≤ M
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
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
⊢ Eq.{u_3 + 1} (α := Subalgebra R K)
    (⨅ (v : HeightOneSpectrum R), Localization.subalgebra.ofField K v.asIdeal.primeCompl ⋯) ⊥
have h : ∀ (x : K),
  Membership.mem (γ := Subalgebra R K)
      (⨅ (v : HeightOneSpectrum R), Localization.subalgebra.ofField K v.asIdeal.primeCompl sorry) x ↔
    Membership.mem (γ := Subalgebra R K) ⊥ x
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
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
⊢ Membership.mem (γ := Subalgebra R K)
      (⨅ (v : HeightOneSpectrum R), Localization.subalgebra.ofField K v.asIdeal.primeCompl ⋯) x ↔
    Membership.mem (γ := Subalgebra R K) ⊥ x
have h : (∀ (i : HeightOneSpectrum R),
    Membership.mem (γ := Subalgebra R K) (Localization.subalgebra.ofField K i.asIdeal.primeCompl sorry) x) ↔
  Membership.mem (γ := Subalgebra R K) ⊥ x
Tactic: rw [Algebra.mem_iInf]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
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
⊢ (∀ (i : HeightOneSpectrum R),
      Membership.mem (γ := Subalgebra R K) (Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯) x) ↔
    Membership.mem (γ := Subalgebra R K) ⊥ x
have h : (∀ (i : HeightOneSpectrum R),
    Membership.mem (γ := Subalgebra R K) (Localization.subalgebra.ofField K i.asIdeal.primeCompl sorry) x) →
  Membership.mem (γ := Subalgebra R K) ⊥ x
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
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
⊢ (∀ (i : HeightOneSpectrum R),
      Membership.mem (γ := Subalgebra R K) (Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯) x) ↔
    Membership.mem (γ := Subalgebra R K) ⊥ x
have h₁ : Membership.mem (γ := Subalgebra R K) ⊥ x →
  ∀ (i : HeightOneSpectrum R),
    Membership.mem (γ := Subalgebra R K) (Localization.subalgebra.ofField K i.asIdeal.primeCompl sorry) x
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
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
⊢ (∀ (i : HeightOneSpectrum R),
      Membership.mem (γ := Subalgebra R K) (Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯) x) →
    Membership.mem (γ := Subalgebra R K) ⊥ x
have pos : ∀ (hR : IsField R),
  (∀ (i : HeightOneSpectrum R),
      Membership.mem (γ := Subalgebra R K) (Localization.subalgebra.ofField K i.asIdeal.primeCompl sorry) x) →
    Membership.mem (γ := Subalgebra R K) ⊥ x
Tactic: by_cases hR : IsField R
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
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
⊢ (∀ (i : HeightOneSpectrum R),
      Membership.mem (γ := Subalgebra R K) (Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯) x) →
    Membership.mem (γ := Subalgebra R K) ⊥ x
have neg : ∀ (hR : ¬IsField R),
  (∀ (i : HeightOneSpectrum R),
      Membership.mem (γ := Subalgebra R K) (Localization.subalgebra.ofField K i.asIdeal.primeCompl sorry) x) →
    Membership.mem (γ := Subalgebra R K) ⊥ x
Tactic: by_cases hR : IsField R
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
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
⊢ (∀ (i : HeightOneSpectrum R),
      Membership.mem (γ := Subalgebra R K) (Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯) x) →
    Membership.mem (γ := Subalgebra R K) ⊥ x
have pos : ∀ (hR : IsField R),
  (∀ (i : HeightOneSpectrum R),
      Membership.mem (γ := Subalgebra R K) (Localization.subalgebra.ofField K i.asIdeal.primeCompl sorry) x) →
    Membership.mem (γ := Subalgebra R K) ⊥ x
Tactic: on_goal 1 => by_cases hR : IsField R
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
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
⊢ (∀ (i : HeightOneSpectrum R),
      Membership.mem (γ := Subalgebra R K) (Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯) x) →
    Membership.mem (γ := Subalgebra R K) ⊥ x
have neg : ∀ (hR : ¬IsField R),
  (∀ (i : HeightOneSpectrum R),
      Membership.mem (γ := Subalgebra R K) (Localization.subalgebra.ofField K i.asIdeal.primeCompl sorry) x) →
    Membership.mem (γ := Subalgebra R K) ⊥ x
Tactic: on_goal 1 => by_cases hR : IsField R
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
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
⊢ (∀ (i : HeightOneSpectrum R),
      Membership.mem (γ := Subalgebra R K) (Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯) x) →
    Membership.mem (γ := Subalgebra R K) ⊥ x
have 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 sorry) 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⟩
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
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
⊢ (∀ (i : HeightOneSpectrum R),
      Membership.mem (γ := Subalgebra R K) (Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯) x) →
    Membership.mem (γ := Subalgebra R K) ⊥ x
have neg : (∀ (i : HeightOneSpectrum R),
    Membership.mem (γ := Subalgebra R K) (Localization.subalgebra.ofField K i.asIdeal.primeCompl sorry) x) →
  ∀ (i : MaximalSpectrum R),
    Membership.mem (γ := Subalgebra R K) (Localization.subalgebra.ofField K i.asIdeal.primeCompl sorry) x
Tactic: rw [← MaximalSpectrum.iInf_localization_eq_bot, Algebra.mem_iInf]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
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
⊢ Membership.mem (γ := Subalgebra R K) ⊥ x →
    ∀ (i : HeightOneSpectrum R),
      Membership.mem (γ := Subalgebra R K) (Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯) x
have h : (∀ (i : MaximalSpectrum R),
    Membership.mem (γ := Subalgebra R K) (Localization.subalgebra.ofField K i.asIdeal.primeCompl sorry) x) →
  ∀ (i : HeightOneSpectrum R),
    Membership.mem (γ := Subalgebra R K) (Localization.subalgebra.ofField K i.asIdeal.primeCompl sorry) x
Tactic: rw [← MaximalSpectrum.iInf_localization_eq_bot, Algebra.mem_iInf]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
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
S : Type u_4
inst_4 : CommRing S
e : R ≃+* S
x : HeightOneSpectrum R
⊢ comap (↑e : R →+* S) ⋯ (comap (↑e.symm : S →+* R) ⋯ x) = x
have asIdeal : ∀ (x_1 : R),
  Membership.mem (γ := Ideal R) (asIdeal (comap (↑e : R →+* S) sorry (comap (↑e.symm : S →+* R) sorry x))) x_1 ↔ x_1 ∈ x.asIdeal
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
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
S : Type u_4
inst_4 : CommRing S
e : R ≃+* S
x : HeightOneSpectrum S
⊢ comap (↑e.symm : S →+* R) ⋯ (comap (↑e : R →+* S) ⋯ x) = x
have asIdeal : ∀ (x_1 : S),
  Membership.mem (γ := Ideal S) (asIdeal (comap (↑e.symm : S →+* R) sorry (comap (↑e : R →+* S) sorry x))) x_1 ↔ x_1 ∈ x.asIdeal
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
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
S : Type u_4
inst_4 : CommRing S
e : R ≃+* S
x : HeightOneSpectrum S
x_1 : S
⊢ Membership.mem (γ := Ideal S) (asIdeal (comap (↑e.symm : S →+* R) ⋯ (comap (↑e : R →+* S) ⋯ x))) x_1 ↔ x_1 ∈ x.asIdeal
have asIdeal : Membership.mem (γ := Ideal S) (asIdeal (comap (↑e.symm : S →+* R) sorry (comap (↑e : R →+* S) sorry x))) x_1 ↔
  Membership.mem (γ := Ideal S) (Ideal.map e (Ideal.comap e x.asIdeal)) x_1
Tactic: rw [← Ideal.map_comap_eq_self_of_equiv e x.asIdeal]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
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
S : Type u_4
inst_4 : CommRing S
e : R ≃+* S
x : HeightOneSpectrum S
x_1 : S
⊢ Membership.mem (γ := Ideal S) (asIdeal (comap (↑e.symm : S →+* R) ⋯ (comap (↑e : R →+* S) ⋯ x))) x_1 ↔
    Membership.mem (γ := Ideal S) (Ideal.map e (Ideal.comap e x.asIdeal)) x_1
have asIdeal : Membership.mem (γ := Ideal S) (Ideal.map e (Ideal.comap (F := R →+* S) (↑e : R →+* S) x.asIdeal)) x_1 ↔
  Membership.mem (γ := Ideal S) (Ideal.map e (Ideal.comap e x.asIdeal)) x_1
Tactic: simp only [comap_asIdeal, Ideal.mem_comap, RingHom.coe_coe, Ideal.symm_apply_mem_of_equiv_iff]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (hypothesis)
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 A
I : Ideal R
J : Ideal A
f : RingHom.{u_1, u_2} (R ⧸ I) (A ⧸ J)
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R ⧸ I) (β := A ⧸ J) (⇑f : (a : R ⧸ I) → A ⧸ J)
X : { p : Ideal R // p ∣ I }
⊢ comap (F := A →+* A ⧸ J) (Ideal.Quotient.mk J)
      (map (R := R ⧸ I) f (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) (↑X : Ideal R))) ∣
    J
have this : LE.le (α := Ideal A) (RingHom.ker (F := A →+* A ⧸ J) (Ideal.Quotient.mk J))
  (comap (F := A →+* A ⧸ J) (Ideal.Quotient.mk J)
    (map (R := R ⧸ I) f (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) (↑X : Ideal R))))
Tactic: have : RingHom.ker (Ideal.Quotient.mk J) ≤
        comap (Ideal.Quotient.mk J) (map f (map (Ideal.Quotient.mk I) X)) :=
      ker_le_comap (Ideal.Quotient.mk J)
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (hypothesis)
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 A
I : Ideal R
J : Ideal A
f : RingHom.{u_1, u_2} (R ⧸ I) (A ⧸ J)
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R ⧸ I) (β := A ⧸ J) (⇑f : (a : R ⧸ I) → A ⧸ J)
X : { p : Ideal R // p ∣ I }
this :
  LE.le (α := Ideal A) (RingHom.ker (F := A →+* A ⧸ J) (Ideal.Quotient.mk J))
    (comap (F := A →+* A ⧸ J) (Ideal.Quotient.mk J)
      (map (R := R ⧸ I) f (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) (↑X : Ideal R))))
⊢ comap (F := A →+* A ⧸ J) (Ideal.Quotient.mk J)
      (map (R := R ⧸ I) f (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) (↑X : Ideal R))) ∣
    J
have this₁ : J ≤
  comap (F := A →+* A ⧸ J) (Ideal.Quotient.mk J)
    (map (R := R ⧸ I) f (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) (↑X : Ideal R)))
Tactic: rw [mk_ker] at this
Cleared hypotheses: this