awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (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 A
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
P : Ideal A
hirr : Irreducible P
I J_1 J : Ideal A
hJ : P < J
⊢ J = ⊤
have obtain : ∀ (_J_ne : J ≠ 0) (H : Ideal A) (hunit : ¬IsUnit H) (P_eq : P = J * H), J = ⊤
Tactic: obtain ⟨_J_ne, H, hunit, P_eq⟩ := Ideal.dvdNotUnit_iff_lt.mpr hJ
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (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
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
P : Ideal A
hirr : Irreducible P
I J : Ideal A
⊢ P ∣ I * J → P ∣ I ∨ P ∣ J
have this : P.IsMaximal
Tactic: have : P.IsMaximal := by
          refine ⟨⟨mt Ideal.isUnit_iff.mpr hirr.not_isUnit, ?_⟩⟩
          intro J hJ
          obtain ⟨_J_ne, H, hunit, P_eq⟩ := Ideal.dvdNotUnit_iff_lt.mpr hJ
          exact Ideal.isUnit_iff.mp ((hirr.isUnit_or_isUnit P_eq).resolve_right hunit)
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (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 A
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
P : Ideal A
hirr : Irreducible P
I J : Ideal A
this : P.IsMaximal
⊢ P ∣ I * J → P ∣ I ∨ P ∣ J
have rw : (∀ ⦃x : A⦄, x ∈ I * J → x ∈ P) → (∀ ⦃x : A⦄, x ∈ I → x ∈ P) ∨ ∀ ⦃x : A⦄, x ∈ J → x ∈ P
Tactic: rw [Ideal.dvd_iff_le, Ideal.dvd_iff_le, Ideal.dvd_iff_le, SetLike.le_def, SetLike.le_def,
          SetLike.le_def]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (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 A
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
P : Ideal A
hirr : Irreducible P
I J : Ideal A
this : P.IsMaximal
⊢ (∀ ⦃x : A⦄, x ∈ I * J → x ∈ P) → (∀ ⦃x : A⦄, x ∈ I → x ∈ P) ∨ ∀ ⦃x : A⦄, x ∈ J → x ∈ P
have contrapose! : ((∃ x ∈ I, x ∉ P) ∧ ∃ x ∈ J, x ∉ P) → ∃ x ∈ I * J, x ∉ P
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
P : Ideal A
h : Prime P
⊢ P.IsPrime
have refine_1 : P ≠ ⊤
Tactic: refine ⟨?_, fun hxy => ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
P : Ideal A
h : Prime P
refine_1 : P ≠ ⊤
⊢ P.IsPrime
have refine_2 : ∀ {x y : A} (hxy : x * y ∈ P), x ∈ P ∨ y ∈ P
Tactic: refine ⟨?_, fun hxy => ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (hypothesis)
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
h : Prime.{u_2} (M := Ideal A) ⊤
⊢ False
have h₁ : Prime.{u_2} (M := Ideal A) 1
Tactic: rw [← one_eq_top] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
P : Ideal A
h : Prime P
x y : A
hxy : x * y ∈ P
⊢ x ∈ P ∨ y ∈ P
have refine_2 : ∀ (hxy : P ∣ HMul.hMul (α := Ideal A) (span {x}) (span {y})), P ∣ span {x} ∨ P ∣ span {y}
Tactic: simp only [← dvd_span_singleton, ← span_singleton_mul_span_singleton] at hxy ⊢
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
P : Ideal A
hP : P ≠ ⊥
h : P.IsPrime
⊢ Prime P
have refine : ∀ (I J : Ideal A) (hIJ : P ∣ I * J), P ∣ I ∨ P ∣ J
Tactic: refine ⟨hP, mt isUnit_iff.mp h.ne_top, fun I J hIJ => ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
a : A
⊢ Prime (M := Ideal A) (span {a}) ↔ Prime a
have inl : Prime (M := Ideal A) (span {0}) ↔ Prime.{u_2} (M := A) 0
Tactic: rcases eq_or_ne a 0 with rfl | ha
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
a : A
inl : Prime (M := Ideal A) (span {0}) ↔ Prime.{u_2} (M := A) 0
⊢ Prime (M := Ideal A) (span {a}) ↔ Prime a
have inr : ∀ (ha : a ≠ 0), Prime (M := Ideal A) (span {a}) ↔ Prime a
Tactic: rcases eq_or_ne a 0 with rfl | ha
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
⊢ Prime (M := Ideal A) (span {0}) ↔ Prime.{u_2} (M := A) 0
have inl : ¬Prime.{u_2} (M := Ideal A) 0 ↔ ¬Prime.{u_2} (M := A) 0
Tactic: rw [Set.singleton_zero, span_zero, ← zero_eq_bot, ← not_iff_not]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (hypothesis)
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
a : A
ha : a ≠ 0
⊢ Prime (M := Ideal A) (span {a}) ↔ Prime a
have ha' : Ne (α := Ideal A) (span {a}) ⊥
Tactic: have ha' : span {a} ≠ ⊥ := by simpa only [ne_eq, span_singleton_eq_bot] using ha
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
a : A
ha : a ≠ 0
ha' : Ne (α := Ideal A) (span {a}) ⊥
⊢ Prime (M := Ideal A) (span {a}) ↔ Prime a
have inr : IsPrime (α := A) (span {a}) ↔ Prime a
Tactic: rw [prime_iff_isPrime ha', span_singleton_prime ha]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
a : A
ha : a ≠ 0
ha' : Ne (α := Ideal A) (span {a}) ⊥
inr : IsPrime (α := A) (span {a}) ↔ Prime a
⊢ Prime (M := Ideal A) (span {a}) ↔ Prime a
have inr₁ : Prime a ↔ Prime a
Tactic: rw [prime_iff_isPrime ha', span_singleton_prime ha]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
p I : Ideal A
hI : I ≠ ⊥
⊢ p ∈ normalizedFactors I ↔ p.IsPrime ∧ I ≤ p
have rw : p ∈ normalizedFactors I ↔ p.IsPrime ∧ p ∣ I
Tactic: rw [← dvd_iff_le]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
p I : Ideal A
hI : I ≠ ⊥
⊢ p ∈ normalizedFactors I ↔ p.IsPrime ∧ p ∣ I
have pos : ∀ (hp : p = 0), p ∈ normalizedFactors I ↔ p.IsPrime ∧ p ∣ I
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
p I : Ideal A
hI : I ≠ ⊥
pos : ∀ (hp : p = 0), p ∈ normalizedFactors I ↔ p.IsPrime ∧ p ∣ I
⊢ p ∈ normalizedFactors I ↔ p.IsPrime ∧ p ∣ I
have neg : ∀ (hp : ¬p = 0), p ∈ normalizedFactors I ↔ p.IsPrime ∧ p ∣ I
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (hypothesis)
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
p I : Ideal A
hI : I ≠ ⊥
hp : p = 0
⊢ p ∈ normalizedFactors I ↔ p.IsPrime ∧ p ∣ I
have hI₁ : I ≠ 0
Tactic: rw [← zero_eq_bot] at hI
Cleared hypotheses: hI, hp
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
p I : Ideal A
hI : I ≠ ⊥
hp : ¬p = 0
⊢ p ∈ normalizedFactors I ↔ p.IsPrime ∧ p ∣ I
have neg : Prime p ∧ p ∣ I ↔ p.IsPrime ∧ p ∣ I
Tactic: rwa [mem_normalizedFactors_iff hI, prime_iff_isPrime]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
p I : Ideal A
hI : I ≠ ⊥
hp : ¬p = 0
neg : Prime p ∧ p ∣ I ↔ p.IsPrime ∧ p ∣ I
⊢ p ∈ normalizedFactors I ↔ p.IsPrime ∧ p ∣ I
have neg₁ : p.IsPrime ∧ p ∣ I ↔ p.IsPrime ∧ p ∣ I
Tactic: rwa [mem_normalizedFactors_iff hI, prime_iff_isPrime]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
p I : Ideal A
hI : I ≠ ⊥
hp : ¬p = 0
neg : Prime p ∧ p ∣ I ↔ p.IsPrime ∧ p ∣ I
neg₁ : p.IsPrime ∧ p ∣ I ↔ p.IsPrime ∧ p ∣ I
⊢ p ∈ normalizedFactors I ↔ p.IsPrime ∧ p ∣ I
have neg₂ : p ≠ ⊥
Tactic: rwa [mem_normalizedFactors_iff hI, prime_iff_isPrime]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : IsDedekindDomain A
p : Ideal R
h : p.IsMaximal
inst_3 : Algebra R A
inst_4 : IsDomain R
inst_5 : IsTorsionFree R A
hp : p ≠ ⊥
P : Ideal A
⊢ Membership.mem (γ := Set (Ideal A)) (p.primesOver A) P ↔
    Membership.mem (γ := Multiset (Ideal A)) (normalizedFactors (map (F := R →+* A) (algebraMap R A) p)) P
have rw : P.IsPrime → (p = comap (F := R →+* A) (algebraMap R A) P ↔ p ≤ comap (F := R →+* A) (algebraMap R A) P)
Tactic: rw [primesOver, Set.mem_setOf_eq, mem_normalizedFactors_iff (map_ne_bot_of_ne_bot hp),
    liesOver_iff, under_def, and_congr_right_iff, map_le_iff_le_comap]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : IsDedekindDomain A
p : Ideal R
h : p.IsMaximal
inst_3 : Algebra R A
inst_4 : IsDomain R
inst_5 : IsTorsionFree R A
hp : p ≠ ⊥
P : Ideal A
hP : P.IsPrime
⊢ p = comap (F := R →+* A) (algebraMap R A) P ↔ p ≤ comap (F := R →+* A) (algebraMap R A) P
have refine : ∀ (h' : p ≤ comap (F := R →+* A) (algebraMap R A) P), Ne (α := Ideal R) (comap (F := R →+* A) (algebraMap R A) P) ⊤
Tactic: refine ⟨fun h ↦ le_of_eq h, fun h' ↦ ((IsCoatom.le_iff_eq (isMaximal_def.mp h) ?_).mp h').symm⟩
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hI1 : I ≠ ⊤
e : ℕ
he : 2 ≤ e
⊢ I ^ e < I
have h : I = (fun (x : ℕ) ↦ I ^ x) 1
Tactic: convert! I.pow_right_strictAnti hI0 hI1 he
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hI1 : I ≠ ⊤
e : ℕ
he : 2 ≤ e
⊢ I = HPow.hPow (β := ℕ) I 1
have h : I = I
Tactic: rw [pow_one]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
P I : Ideal A
P_prime : P.IsPrime
hP : P ≠ ⊥
i : ℕ
hlt : P ^ (i + 1) < I
hle : I ≤ P ^ i
⊢ I = P ^ i
have refine : P ^ i ≤ I
Tactic: refine le_antisymm hle ?_
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (hypothesis)
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
P I : Ideal A
P_prime : P.IsPrime
hP : P ≠ ⊥
i : ℕ
hlt : P ^ (i + 1) < I
hle : I ≤ P ^ i
⊢ P ^ i ≤ I
have P_prime' : Prime P
Tactic: have P_prime' := prime_of_isPrime hP P_prime
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (hypothesis)
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
P I : Ideal A
P_prime : P.IsPrime
hP : P ≠ ⊥
i : ℕ
hlt : P ^ (i + 1) < I
hle : I ≤ P ^ i
P_prime' : Prime P
⊢ P ^ i ≤ I
have h1 : I ≠ ⊥
Tactic: have h1 : I ≠ ⊥ := (lt_of_le_of_lt bot_le hlt).ne'
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (hypothesis)
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
P I : Ideal A
P_prime : P.IsPrime
hP : P ≠ ⊥
i : ℕ
hlt : P ^ (i + 1) < I
hle : I ≤ P ^ i
P_prime' : Prime P
h1 : I ≠ ⊥
⊢ P ^ i ≤ I
have this : P ^ i ≠ 0
Tactic: have := pow_ne_zero i hP
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (hypothesis)
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
P I : Ideal A
P_prime : P.IsPrime
hP : P ≠ ⊥
i : ℕ
hlt : P ^ (i + 1) < I
hle : I ≤ P ^ i
P_prime' : Prime P
h1 : I ≠ ⊥
this : P ^ i ≠ 0
⊢ P ^ i ≤ I
have h3 : P ^ (i + 1) ≠ 0
Tactic: have h3 := pow_ne_zero (i + 1) hP
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (hypothesis)
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
P I : Ideal A
P_prime : P.IsPrime
hP : P ≠ ⊥
i : ℕ
hlt : P ^ (i + 1) < I
hle : I ≤ P ^ i
P_prime' : Prime P
h1 : I ≠ ⊥
this : P ^ i ≠ 0
h3 : P ^ (i + 1) ≠ 0
⊢ P ^ i ≤ I
have hlt₁ : normalizedFactors I ≤ Multiset.replicate i ((normalize : (a : Ideal A) → Ideal A) P)
Tactic: rw [← dvdNotUnit_iff_lt, dvdNotUnit_iff_normalizedFactors_lt_normalizedFactors h1 h3,
    normalizedFactors_pow, normalizedFactors_irreducible P_prime'.irreducible,
    Multiset.nsmul_singleton, Multiset.lt_replicate_succ] at hlt
Cleared hypotheses: hlt, hle, P_prime', h1, this, h3
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
P I : Ideal A
P_prime : P.IsPrime
hP : P ≠ ⊥
i : ℕ
hlt : normalizedFactors I ≤ Multiset.replicate i ((normalize : (a : Ideal A) → Ideal A) P)
hle : I ≤ P ^ i
P_prime' : Prime P
h1 : I ≠ ⊥
this : P ^ i ≠ 0
h3 : P ^ (i + 1) ≠ 0
rw : normalizedFactors I ≤ Multiset.replicate i ((normalize : (a : Ideal A) → Ideal A) P)
⊢ P ^ i ≤ I
have hx : I ≠ 0
Tactic: rw [← dvd_iff_le, dvd_iff_normalizedFactors_le_normalizedFactors, normalizedFactors_pow,
    normalizedFactors_irreducible P_prime'.irreducible, Multiset.nsmul_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
x : A
n : ℕ
I : Ideal A
⊢ HPow.hPow (α := Associates (Ideal A)) (Associates.mk I) n ≤ Associates.mk (Ideal.span {x}) ↔ x ∈ I ^ n
have simp_rw : HPow.hPow (α := Associates (Ideal A)) (Associates.mk I) n ∣ Associates.mk (Ideal.span {x}) ↔ x ∈ I ^ n
Tactic: simp_rw [← Associates.dvd_eq_le, ← Associates.mk_pow, Associates.mk_dvd_mk,
    Ideal.dvd_span_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
x : A
n : ℕ
I : Ideal A
simp_rw : HPow.hPow (α := Associates (Ideal A)) (Associates.mk I) n ∣ Associates.mk (Ideal.span {x}) ↔ x ∈ I ^ n
⊢ HPow.hPow (α := Associates (Ideal A)) (Associates.mk I) n ≤ Associates.mk (Ideal.span {x}) ↔ x ∈ I ^ n
have simp_rw₁ : Dvd.dvd (α := Associates (Ideal A)) (Associates.mk (I ^ n)) (Associates.mk (Ideal.span {x})) ↔ x ∈ I ^ n
Tactic: simp_rw [← Associates.dvd_eq_le, ← Associates.mk_pow, Associates.mk_dvd_mk,
    Ideal.dvd_span_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
x : A
n : ℕ
I : Ideal A
simp_rw : HPow.hPow (α := Associates (Ideal A)) (Associates.mk I) n ∣ Associates.mk (Ideal.span {x}) ↔ x ∈ I ^ n
simp_rw₁ : Dvd.dvd (α := Associates (Ideal A)) (Associates.mk (I ^ n)) (Associates.mk (Ideal.span {x})) ↔ x ∈ I ^ n
⊢ HPow.hPow (α := Associates (Ideal A)) (Associates.mk I) n ≤ Associates.mk (Ideal.span {x}) ↔ x ∈ I ^ n
have simp_rw₂ : I ^ n ∣ Ideal.span {x} ↔ x ∈ I ^ n
Tactic: simp_rw [← Associates.dvd_eq_le, ← Associates.mk_pow, Associates.mk_dvd_mk,
    Ideal.dvd_span_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : IsDedekindDomain A
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
I J : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K
hI : I ≠ 0
hJ : J ≠ 0
⊢ I ≤ J⁻¹ ↔ J ≤ I⁻¹
have rw : I ≤ 1 / J ↔ J ≤ I⁻¹
Tactic: rw [inv_eq, inv_eq, le_div_iff_mul_le hI, le_div_iff_mul_le hJ, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : IsDedekindDomain A
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
I J : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K
hI : I ≠ 0
hJ : J ≠ 0
rw : I ≤ 1 / J ↔ J ≤ I⁻¹
⊢ I ≤ J⁻¹ ↔ J ≤ I⁻¹
have rw₁ : I ≤ 1 / J ↔ J ≤ 1 / I
Tactic: rw [inv_eq, inv_eq, le_div_iff_mul_le hI, le_div_iff_mul_le hJ, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : IsDedekindDomain A
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
I J : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K
hI : I ≠ 0
hJ : J ≠ 0
rw : I ≤ 1 / J ↔ J ≤ I⁻¹
rw₁ : I ≤ 1 / J ↔ J ≤ 1 / I
⊢ I ≤ J⁻¹ ↔ J ≤ I⁻¹
have rw₂ : I ≤ 1 / J ↔ J * I ≤ 1
Tactic: rw [inv_eq, inv_eq, le_div_iff_mul_le hI, le_div_iff_mul_le hJ, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : IsDedekindDomain A
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
I J : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K
hI : I ≠ 0
hJ : J ≠ 0
rw : I ≤ 1 / J ↔ J ≤ I⁻¹
rw₁ : I ≤ 1 / J ↔ J ≤ 1 / I
rw₂ : I ≤ 1 / J ↔ J * I ≤ 1
⊢ I ≤ J⁻¹ ↔ J ≤ I⁻¹
have rw₃ : I * J ≤ 1 ↔ J * I ≤ 1
Tactic: rw [inv_eq, inv_eq, le_div_iff_mul_le hI, le_div_iff_mul_le hJ, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : IsDedekindDomain A
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
I J : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K
hI : I ≠ 0
hJ : J ≠ 0
rw : I ≤ 1 / J ↔ J ≤ I⁻¹
rw₁ : I ≤ 1 / J ↔ J ≤ 1 / I
rw₂ : I ≤ 1 / J ↔ J * I ≤ 1
rw₃ : I * J ≤ 1 ↔ J * I ≤ 1
⊢ I ≤ J⁻¹ ↔ J ≤ I⁻¹
have rw₄ : J * I ≤ 1 ↔ J * I ≤ 1
Tactic: rw [inv_eq, inv_eq, le_div_iff_mul_le hI, le_div_iff_mul_le hJ, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : IsDedekindDomain A
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
I J : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K
hI : I ≠ 0
hJ : J ≠ 0
⊢ I⁻¹ ≤ J⁻¹ ↔ J ≤ I
have rw : J ≤ I⁻¹⁻¹ ↔ J ≤ I
Tactic: rw [le_inv_comm (inv_ne_zero hI) hJ, inv_inv]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : IsDedekindDomain A
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
I J : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K
hI : I ≠ 0
hJ : J ≠ 0
rw : J ≤ I⁻¹⁻¹ ↔ J ≤ I
⊢ I⁻¹ ≤ J⁻¹ ↔ J ≤ I
have rw₁ : J ≤ I ↔ J ≤ I
Tactic: rw [le_inv_comm (inv_ne_zero hI) hJ, inv_inv]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (hypothesis)
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : IsDedekindDomain A
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_4
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K := spanFinset A s f
⊢ ∃ (a : K), (∀ i ∈ s, IsLocalization.IsInteger A (a * f i)) ∧ ∃ i ∈ s, a * f i ∉ (↑J : FractionalIdeal A⁰ K)
have hI0 : I ≠ 0
Tactic: have hI0 : I ≠ 0 := spanFinset_ne_zero.mpr ⟨j, hjs, hjf⟩
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : IsDedekindDomain A
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_4
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : (↑J : FractionalIdeal A⁰ K) / I < I⁻¹
⊢ ∃ (a : K), (∀ i ∈ s, IsLocalization.IsInteger A (a * f i)) ∧ ∃ i ∈ s, a * f i ∉ (↑J : FractionalIdeal A⁰ K)
have obtain : (↑J : FractionalIdeal A⁰ K) / I ≤ I⁻¹ →
  ∀ (a : K) (hI : a ∈ I⁻¹) (hpI : a ∉ (↑J : FractionalIdeal A⁰ K) / I),
    ∃ (a : K), (∀ i ∈ s, IsLocalization.IsInteger A (a * f i)) ∧ ∃ i ∈ s, a * f i ∉ (↑J : FractionalIdeal A⁰ K)
Tactic: obtain ⟨_, a, hI, hpI⟩ := SetLike.lt_iff_le_and_exists.mp this
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (hypothesis)
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : IsDedekindDomain A
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_4
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : (↑J : FractionalIdeal A⁰ K) / I < I⁻¹
left : (↑J : FractionalIdeal A⁰ K) / I ≤ I⁻¹
a : K
hI : a ∈ I⁻¹
hpI : a ∉ (↑J : FractionalIdeal A⁰ K) / I
⊢ ∃ (a : K), (∀ i ∈ s, IsLocalization.IsInteger A (a * f i)) ∧ ∃ i ∈ s, a * f i ∉ (↑J : FractionalIdeal A⁰ K)
have hI₁ : ∀ y ∈ I, Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) 1 (a * y)
Tactic: rw [mem_inv_iff hI0] at hI
Cleared hypotheses: hI, hpI
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : IsDedekindDomain A
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_4
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : (↑J : FractionalIdeal A⁰ K) / I < I⁻¹
left : (↑J : FractionalIdeal A⁰ K) / I ≤ I⁻¹
a : K
hI : ∀ y ∈ I, Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) 1 (a * y)
hpI : a ∉ (↑J : FractionalIdeal A⁰ K) / I
⊢ ∃ (a : K), (∀ i ∈ s, IsLocalization.IsInteger A (a * f i)) ∧ ∃ i ∈ s, a * f i ∉ (↑J : FractionalIdeal A⁰ K)
have refine_1 : ∀ (i : ι) (hi : i ∈ s), IsLocalization.IsInteger A (a * f i)
Tactic: refine ⟨a, fun i hi => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : IsDedekindDomain A
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_4
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : (↑J : FractionalIdeal A⁰ K) / I < I⁻¹
left : (↑J : FractionalIdeal A⁰ K) / I ≤ I⁻¹
a : K
hI : ∀ y ∈ I, Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) 1 (a * y)
hpI : a ∉ (↑J : FractionalIdeal A⁰ K) / I
refine_1 : ∀ (i : ι) (hi : i ∈ s), IsLocalization.IsInteger A (a * f i)
⊢ ∃ (a : K), (∀ i ∈ s, IsLocalization.IsInteger A (a * f i)) ∧ ∃ i ∈ s, a * f i ∉ (↑J : FractionalIdeal A⁰ K)
have refine_2 : ∃ i ∈ s, a * f i ∉ (↑J : FractionalIdeal A⁰ K)
Tactic: refine ⟨a, fun i hi => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : IsDedekindDomain A
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_4
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : (↑J : FractionalIdeal A⁰ K) / I < I⁻¹
left : (↑J : FractionalIdeal A⁰ K) / I ≤ I⁻¹
a : K
hI : ∀ y ∈ I, Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) 1 (a * y)
hpI : a ∉ (↑J : FractionalIdeal A⁰ K) / I
⊢ ∃ i ∈ s, a * f i ∉ (↑J : FractionalIdeal A⁰ K)
have refine_2 : ∀
  (hpI :
    ∀ (i : ι) (_ : i ∈ s),
      Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (a * f i)),
  a ∈ (↑J : FractionalIdeal A⁰ K) / I
Tactic: contrapose! hpI
Cleared hypotheses: hpI
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : IsDedekindDomain A
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_4
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : (↑J : FractionalIdeal A⁰ K) / I < I⁻¹
left : (↑J : FractionalIdeal A⁰ K) / I ≤ I⁻¹
a : K
hI : ∀ y ∈ I, Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) 1 (a * y)
hpI :
  ∀ (i : ι) (_ : i ∈ s),
    Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (a * f i)
⊢ a ∈ (↑J : FractionalIdeal A⁰ K) / I
have refine_2 : ∀ (y : K) (hy : y ∈ I) (x : K) (h : x ∈ f '' (↑s : Set ι)),
  Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑J : FractionalIdeal A⁰ K) (a * x)
Tactic: refine (mem_div_iff_of_ne_zero hI0).mpr fun y hy => Submodule.span_induction ?_ ?_ ?_ ?_ hy