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_1 : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Field K_1
inst_3 : Algebra A K_1
inst_4 : IsFractionRing A K_1
inst_5 : IsDedekindDomain A
I_1 : Ideal A
I : { x : Ideal A // 0 < x }
J K : Ideal A
e :
  (fun (x1 x2 : Ideal A) ↦ x1 ≤ x2) ((fun (x : { x : Ideal A // 0 < x }) (y : Ideal A) ↦ (↑x : Ideal A) * y) I J)
    ((fun (x : { x : Ideal A // 0 < x }) (y : Ideal A) ↦ (↑x : Ideal A) * y) I K)
rwa :
  LE.le (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑J : FractionalIdeal A⁰ (FractionRing A))
    (↑K : FractionalIdeal A⁰ (FractionRing A))
rwa₁ :
  HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑(↑I : Ideal A) : FractionalIdeal A⁰ (FractionRing A))
      (↑J : FractionalIdeal A⁰ (FractionRing A)) ≤
    HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A))
      (↑(↑I : Ideal A) : FractionalIdeal A⁰ (FractionRing A)) (↑K : FractionalIdeal A⁰ (FractionRing A))
⊢ J ≤ K
have rwa₂ : (↑((↑I : Ideal A) * J) : FractionalIdeal A⁰ (FractionRing A)) ≤
  HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑(↑I : Ideal A) : FractionalIdeal A⁰ (FractionRing A))
    (↑K : FractionalIdeal A⁰ (FractionRing A))
Tactic: rwa [← FractionalIdeal.coeIdeal_le_coeIdeal (FractionRing A),
      ← mul_le_mul_iff_right₀ (α := FractionalIdeal A⁰ (FractionRing A)) (a := I.1)
        (by simpa [pos_iff_ne_zero] using I.2.ne'),
      ← FractionalIdeal.coeIdeal_mul, ← FractionalIdeal.coeIdeal_mul,
      FractionalIdeal.coeIdeal_le_coeIdeal]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
K_1 : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Field K_1
inst_3 : Algebra A K_1
inst_4 : IsFractionRing A K_1
inst_5 : IsDedekindDomain A
I_1 : Ideal A
I : { x : Ideal A // 0 < x }
J K : Ideal A
e :
  (fun (x1 x2 : Ideal A) ↦ x1 ≤ x2) ((fun (x : { x : Ideal A // 0 < x }) (y : Ideal A) ↦ (↑x : Ideal A) * y) I J)
    ((fun (x : { x : Ideal A // 0 < x }) (y : Ideal A) ↦ (↑x : Ideal A) * y) I K)
rwa :
  LE.le (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑J : FractionalIdeal A⁰ (FractionRing A))
    (↑K : FractionalIdeal A⁰ (FractionRing A))
rwa₁ :
  HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑(↑I : Ideal A) : FractionalIdeal A⁰ (FractionRing A))
      (↑J : FractionalIdeal A⁰ (FractionRing A)) ≤
    HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A))
      (↑(↑I : Ideal A) : FractionalIdeal A⁰ (FractionRing A)) (↑K : FractionalIdeal A⁰ (FractionRing A))
rwa₂ :
  (↑((↑I : Ideal A) * J) : FractionalIdeal A⁰ (FractionRing A)) ≤
    HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A))
      (↑(↑I : Ideal A) : FractionalIdeal A⁰ (FractionRing A)) (↑K : FractionalIdeal A⁰ (FractionRing A))
⊢ J ≤ K
have rwa₃ : LE.le (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑((↑I : Ideal A) * J) : FractionalIdeal A⁰ (FractionRing A))
  (↑((↑I : Ideal A) * K) : FractionalIdeal A⁰ (FractionRing A))
Tactic: rwa [← FractionalIdeal.coeIdeal_le_coeIdeal (FractionRing A),
      ← mul_le_mul_iff_right₀ (α := FractionalIdeal A⁰ (FractionRing A)) (a := I.1)
        (by simpa [pos_iff_ne_zero] using I.2.ne'),
      ← FractionalIdeal.coeIdeal_mul, ← FractionalIdeal.coeIdeal_mul,
      FractionalIdeal.coeIdeal_le_coeIdeal]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (goal)
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I J : Ideal A
h : J ≤ I
⊢ I ∣ J
have pos : ∀ (hI : I = ⊥), I ∣ J
Tactic: by_cases hI : I = ⊥
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (goal)
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I J : Ideal A
h : J ≤ I
pos : ∀ (hI : I = ⊥), I ∣ J
⊢ I ∣ J
have neg : ∀ (hI : ¬I = ⊥), I ∣ J
Tactic: by_cases hI : I = ⊥
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (goal)
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I J : Ideal A
h : J ≤ I
hI : I = ⊥
⊢ J = ⊥
have rwa : ∀ (h : J ≤ ⊥) (hI : I = ⊥), J = ⊥
Tactic: rwa [hI, ← eq_bot_iff] at h
Cleared hypotheses: h, hI
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (goal)
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I J : Ideal A
h : J ≤ I
hI : I = ⊥
rwa : ∀ (h : J ≤ ⊥) (hI : I = ⊥), J = ⊥
⊢ J = ⊥
have rwa₁ : ∀ (h : J = ⊥) (hI : I = ⊥), J = ⊥
Tactic: rwa [hI, ← eq_bot_iff] at h
Cleared hypotheses: h, hI
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (hypothesis)
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I J : Ideal A
h : J ≤ I
hI : I = ⊥
⊢ I ∣ J
have hJ : J = ⊥
Tactic: have hJ : J = ⊥ := by rwa [hI, ← eq_bot_iff] at h
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (goal)
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I J : Ideal A
h : J ≤ I
hI : I = ⊥
hJ : J = ⊥
⊢ I ∣ J
have pos : ⊥ ∣ J
Tactic: rw [hI, hJ]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (goal)
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I J : Ideal A
h : J ≤ I
hI : I = ⊥
hJ : J = ⊥
pos : ⊥ ∣ J
⊢ I ∣ J
have pos₁ : Dvd.dvd.{u_2} (α := Ideal A) ⊥ ⊥
Tactic: rw [hI, hJ]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (hypothesis)
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I J : Ideal A
h : J ≤ I
hI : ¬I = ⊥
⊢ I ∣ J
have hI' : Ne (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑I : FractionalIdeal A⁰ (FractionRing A)) 0
Tactic: have hI' : (I : FractionalIdeal A⁰ (FractionRing A)) ≠ 0 := coeIdeal_ne_zero.mpr hI
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (goal)
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I J : Ideal A
h : J ≤ I
hI : ¬I = ⊥
hI' : Ne (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑I : FractionalIdeal A⁰ (FractionRing A)) 0
⊢ HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑I : FractionalIdeal A⁰ (FractionRing A))⁻¹
      (↑J : FractionalIdeal A⁰ (FractionRing A)) ≤
    1
have rw : HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑I : FractionalIdeal A⁰ (FractionRing A))⁻¹
    (↑J : FractionalIdeal A⁰ (FractionRing A)) ≤
  HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑I : FractionalIdeal A⁰ (FractionRing A))⁻¹
    (↑I : FractionalIdeal A⁰ (FractionRing A))
Tactic: rw [← inv_mul_cancel₀ hI']
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (hypothesis)
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I J : Ideal A
h : J ≤ I
hI : ¬I = ⊥
hI' : Ne (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑I : FractionalIdeal A⁰ (FractionRing A)) 0
⊢ I ∣ J
have this : HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑I : FractionalIdeal A⁰ (FractionRing A))⁻¹
    (↑J : FractionalIdeal A⁰ (FractionRing A)) ≤
  1
Tactic: have : (I : FractionalIdeal A⁰ (FractionRing A))⁻¹ * J ≤ 1 := by
      rw [← inv_mul_cancel₀ hI']; gcongr
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (goal)
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I J : Ideal A
h : J ≤ I
hI : ¬I = ⊥
hI' : Ne (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑I : FractionalIdeal A⁰ (FractionRing A)) 0
this :
  HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑I : FractionalIdeal A⁰ (FractionRing A))⁻¹
      (↑J : FractionalIdeal A⁰ (FractionRing A)) ≤
    1
⊢ I ∣ J
have neg : ∀ (H : Ideal A)
  (hH :
    (↑H : FractionalIdeal A⁰ (FractionRing A)) =
      HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑I : FractionalIdeal A⁰ (FractionRing A))⁻¹
        (↑J : FractionalIdeal A⁰ (FractionRing A))),
  I ∣ J
Tactic: obtain ⟨H, hH⟩ := le_one_iff_exists_coeIdeal.mp this
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (goal)
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I J : Ideal A
h : J ≤ I
hI : ¬I = ⊥
hI' : Ne (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑I : FractionalIdeal A⁰ (FractionRing A)) 0
this :
  HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑I : FractionalIdeal A⁰ (FractionRing A))⁻¹
      (↑J : FractionalIdeal A⁰ (FractionRing A)) ≤
    1
H : Ideal A
hH :
  (↑H : FractionalIdeal A⁰ (FractionRing A)) =
    HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑I : FractionalIdeal A⁰ (FractionRing A))⁻¹
      (↑J : FractionalIdeal A⁰ (FractionRing A))
⊢ I ∣ J
have h₁ : J = I * H
Tactic: use H
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (goal)
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I J : Ideal A
h : J ≤ I
hI : ¬I = ⊥
hI' : Ne (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑I : FractionalIdeal A⁰ (FractionRing A)) 0
this :
  HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑I : FractionalIdeal A⁰ (FractionRing A))⁻¹
      (↑J : FractionalIdeal A⁰ (FractionRing A)) ≤
    1
H : Ideal A
hH :
  (↑H : FractionalIdeal A⁰ (FractionRing A)) =
    HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑I : FractionalIdeal A⁰ (FractionRing A))⁻¹
      (↑J : FractionalIdeal A⁰ (FractionRing A))
⊢ J = I * H
have h₁ : Eq (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑J : FractionalIdeal A⁰ (FractionRing A))
  (↑(I * H) : FractionalIdeal A⁰ (FractionRing A))
Tactic: refine coeIdeal_injective (show (J : FractionalIdeal A⁰ (FractionRing A)) = ↑(I * H) from ?_)
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (goal)
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I J : Ideal A
h : J ≤ I
hI : ¬I = ⊥
hI' : Ne (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑I : FractionalIdeal A⁰ (FractionRing A)) 0
this :
  HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑I : FractionalIdeal A⁰ (FractionRing A))⁻¹
      (↑J : FractionalIdeal A⁰ (FractionRing A)) ≤
    1
H : Ideal A
hH :
  (↑H : FractionalIdeal A⁰ (FractionRing A)) =
    HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑I : FractionalIdeal A⁰ (FractionRing A))⁻¹
      (↑J : FractionalIdeal A⁰ (FractionRing A))
⊢ Eq (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑J : FractionalIdeal A⁰ (FractionRing A))
    (↑(I * H) : FractionalIdeal A⁰ (FractionRing A))
have h₁ : (↑J : FractionalIdeal A⁰ (FractionRing A)) =
  HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑I : FractionalIdeal A⁰ (FractionRing A))
    (↑H : FractionalIdeal A⁰ (FractionRing A))
Tactic: rw [coeIdeal_mul, hH, ← mul_assoc, mul_inv_cancel₀ hI', one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (goal)
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I J : Ideal A
h : J ≤ I
hI : ¬I = ⊥
hI' : Ne (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑I : FractionalIdeal A⁰ (FractionRing A)) 0
this :
  HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑I : FractionalIdeal A⁰ (FractionRing A))⁻¹
      (↑J : FractionalIdeal A⁰ (FractionRing A)) ≤
    1
H : Ideal A
hH :
  (↑H : FractionalIdeal A⁰ (FractionRing A)) =
    HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑I : FractionalIdeal A⁰ (FractionRing A))⁻¹
      (↑J : FractionalIdeal A⁰ (FractionRing A))
h₁ :
  (↑J : FractionalIdeal A⁰ (FractionRing A)) =
    HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑I : FractionalIdeal A⁰ (FractionRing A))
      (↑H : FractionalIdeal A⁰ (FractionRing A))
⊢ Eq (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑J : FractionalIdeal A⁰ (FractionRing A))
    (↑(I * H) : FractionalIdeal A⁰ (FractionRing A))
have h₂ : (↑J : FractionalIdeal A⁰ (FractionRing A)) =
  (↑I : FractionalIdeal A⁰ (FractionRing A)) *
    HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑I : FractionalIdeal A⁰ (FractionRing A))⁻¹
      (↑J : FractionalIdeal A⁰ (FractionRing A))
Tactic: rw [coeIdeal_mul, hH, ← mul_assoc, mul_inv_cancel₀ hI', one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (goal)
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I J : Ideal A
h : J ≤ I
hI : ¬I = ⊥
hI' : Ne (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑I : FractionalIdeal A⁰ (FractionRing A)) 0
this :
  HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑I : FractionalIdeal A⁰ (FractionRing A))⁻¹
      (↑J : FractionalIdeal A⁰ (FractionRing A)) ≤
    1
H : Ideal A
hH :
  (↑H : FractionalIdeal A⁰ (FractionRing A)) =
    HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑I : FractionalIdeal A⁰ (FractionRing A))⁻¹
      (↑J : FractionalIdeal A⁰ (FractionRing A))
h₁ :
  (↑J : FractionalIdeal A⁰ (FractionRing A)) =
    HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑I : FractionalIdeal A⁰ (FractionRing A))
      (↑H : FractionalIdeal A⁰ (FractionRing A))
h₂ :
  (↑J : FractionalIdeal A⁰ (FractionRing A)) =
    (↑I : FractionalIdeal A⁰ (FractionRing A)) *
      HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑I : FractionalIdeal A⁰ (FractionRing A))⁻¹
        (↑J : FractionalIdeal A⁰ (FractionRing A))
⊢ Eq (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑J : FractionalIdeal A⁰ (FractionRing A))
    (↑(I * H) : FractionalIdeal A⁰ (FractionRing A))
have h₃ : (↑J : FractionalIdeal A⁰ (FractionRing A)) =
  HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑I : FractionalIdeal A⁰ (FractionRing A))
      (↑I : FractionalIdeal A⁰ (FractionRing A))⁻¹ *
    (↑J : FractionalIdeal A⁰ (FractionRing A))
Tactic: rw [coeIdeal_mul, hH, ← mul_assoc, mul_inv_cancel₀ hI', one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (goal)
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I J : Ideal A
h : J ≤ I
hI : ¬I = ⊥
hI' : Ne (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑I : FractionalIdeal A⁰ (FractionRing A)) 0
this :
  HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑I : FractionalIdeal A⁰ (FractionRing A))⁻¹
      (↑J : FractionalIdeal A⁰ (FractionRing A)) ≤
    1
H : Ideal A
hH :
  (↑H : FractionalIdeal A⁰ (FractionRing A)) =
    HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑I : FractionalIdeal A⁰ (FractionRing A))⁻¹
      (↑J : FractionalIdeal A⁰ (FractionRing A))
h₁ :
  (↑J : FractionalIdeal A⁰ (FractionRing A)) =
    HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑I : FractionalIdeal A⁰ (FractionRing A))
      (↑H : FractionalIdeal A⁰ (FractionRing A))
h₂ :
  (↑J : FractionalIdeal A⁰ (FractionRing A)) =
    (↑I : FractionalIdeal A⁰ (FractionRing A)) *
      HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑I : FractionalIdeal A⁰ (FractionRing A))⁻¹
        (↑J : FractionalIdeal A⁰ (FractionRing A))
h₃ :
  (↑J : FractionalIdeal A⁰ (FractionRing A)) =
    HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑I : FractionalIdeal A⁰ (FractionRing A))
        (↑I : FractionalIdeal A⁰ (FractionRing A))⁻¹ *
      (↑J : FractionalIdeal A⁰ (FractionRing A))
⊢ Eq (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑J : FractionalIdeal A⁰ (FractionRing A))
    (↑(I * H) : FractionalIdeal A⁰ (FractionRing A))
have h₄ : (↑J : FractionalIdeal A⁰ (FractionRing A)) =
  HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) 1 (↑J : FractionalIdeal A⁰ (FractionRing A))
Tactic: rw [coeIdeal_mul, hH, ← mul_assoc, mul_inv_cancel₀ hI', one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (goal)
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I J : Ideal A
h : J ≤ I
hI : ¬I = ⊥
hI' : Ne (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑I : FractionalIdeal A⁰ (FractionRing A)) 0
this :
  HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑I : FractionalIdeal A⁰ (FractionRing A))⁻¹
      (↑J : FractionalIdeal A⁰ (FractionRing A)) ≤
    1
H : Ideal A
hH :
  (↑H : FractionalIdeal A⁰ (FractionRing A)) =
    HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑I : FractionalIdeal A⁰ (FractionRing A))⁻¹
      (↑J : FractionalIdeal A⁰ (FractionRing A))
h₁ :
  (↑J : FractionalIdeal A⁰ (FractionRing A)) =
    HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑I : FractionalIdeal A⁰ (FractionRing A))
      (↑H : FractionalIdeal A⁰ (FractionRing A))
h₂ :
  (↑J : FractionalIdeal A⁰ (FractionRing A)) =
    (↑I : FractionalIdeal A⁰ (FractionRing A)) *
      HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑I : FractionalIdeal A⁰ (FractionRing A))⁻¹
        (↑J : FractionalIdeal A⁰ (FractionRing A))
h₃ :
  (↑J : FractionalIdeal A⁰ (FractionRing A)) =
    HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑I : FractionalIdeal A⁰ (FractionRing A))
        (↑I : FractionalIdeal A⁰ (FractionRing A))⁻¹ *
      (↑J : FractionalIdeal A⁰ (FractionRing A))
h₄ :
  (↑J : FractionalIdeal A⁰ (FractionRing A)) =
    HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) 1 (↑J : FractionalIdeal A⁰ (FractionRing A))
⊢ Eq (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑J : FractionalIdeal A⁰ (FractionRing A))
    (↑(I * H) : FractionalIdeal A⁰ (FractionRing A))
have h₅ : Eq (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (↑J : FractionalIdeal A⁰ (FractionRing A))
  (↑J : FractionalIdeal A⁰ (FractionRing A))
Tactic: rw [coeIdeal_mul, hH, ← mul_assoc, mul_inv_cancel₀ hI', one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : IsDedekindDomain A
inst_3 : Algebra R A
p : Ideal R
P : Ideal A
hP : P ≠ ⊤
inst_4 : p.IsMaximal
⊢ P.LiesOver p ↔ P ∣ map (F := R →+* A) (algebraMap R A) p
have rw : p = under R P ↔ P ∣ map (F := R →+* A) (algebraMap R A) p
Tactic: rw [liesOver_iff, dvd_iff_le, under_def, map_le_iff_le_comap,
    IsCoatom.le_iff_eq (by rwa [← isMaximal_def]) (comap_ne_top _ hP), eq_comm]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : IsDedekindDomain A
inst_3 : Algebra R A
p : Ideal R
P : Ideal A
hP : P ≠ ⊤
inst_4 : p.IsMaximal
rw : p = under R P ↔ P ∣ map (F := R →+* A) (algebraMap R A) p
⊢ P.LiesOver p ↔ P ∣ map (F := R →+* A) (algebraMap R A) p
have rw₁ : p = under R P ↔ map (F := R →+* A) (algebraMap R A) p ≤ P
Tactic: rw [liesOver_iff, dvd_iff_le, under_def, map_le_iff_le_comap,
    IsCoatom.le_iff_eq (by rwa [← isMaximal_def]) (comap_ne_top _ hP), eq_comm]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : IsDedekindDomain A
inst_3 : Algebra R A
p : Ideal R
P : Ideal A
hP : P ≠ ⊤
inst_4 : p.IsMaximal
rw : p = under R P ↔ P ∣ map (F := R →+* A) (algebraMap R A) p
rw₁ : p = under R P ↔ map (F := R →+* A) (algebraMap R A) p ≤ P
⊢ P.LiesOver p ↔ P ∣ map (F := R →+* A) (algebraMap R A) p
have rw₂ : p = comap (F := R →+* A) (algebraMap R A) P ↔ map (F := R →+* A) (algebraMap R A) p ≤ P
Tactic: rw [liesOver_iff, dvd_iff_le, under_def, map_le_iff_le_comap,
    IsCoatom.le_iff_eq (by rwa [← isMaximal_def]) (comap_ne_top _ hP), eq_comm]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : IsDedekindDomain A
inst_3 : Algebra R A
p : Ideal R
P : Ideal A
hP : P ≠ ⊤
inst_4 : p.IsMaximal
rw : p = under R P ↔ P ∣ map (F := R →+* A) (algebraMap R A) p
rw₁ : p = under R P ↔ map (F := R →+* A) (algebraMap R A) p ≤ P
rw₂ : p = comap (F := R →+* A) (algebraMap R A) P ↔ map (F := R →+* A) (algebraMap R A) p ≤ P
⊢ P.LiesOver p ↔ P ∣ map (F := R →+* A) (algebraMap R A) p
have rw₃ : p = comap (F := R →+* A) (algebraMap R A) P ↔ p ≤ comap (F := R →+* A) (algebraMap R A) P
Tactic: rw [liesOver_iff, dvd_iff_le, under_def, map_le_iff_le_comap,
    IsCoatom.le_iff_eq (by rwa [← isMaximal_def]) (comap_ne_top _ hP), eq_comm]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : IsDedekindDomain A
inst_3 : Algebra R A
p : Ideal R
P : Ideal A
hP : P ≠ ⊤
inst_4 : p.IsMaximal
rw : p = under R P ↔ P ∣ map (F := R →+* A) (algebraMap R A) p
rw₁ : p = under R P ↔ map (F := R →+* A) (algebraMap R A) p ≤ P
rw₂ : p = comap (F := R →+* A) (algebraMap R A) P ↔ map (F := R →+* A) (algebraMap R A) p ≤ P
rw₃ : p = comap (F := R →+* A) (algebraMap R A) P ↔ p ≤ comap (F := R →+* A) (algebraMap R A) P
⊢ P.LiesOver p ↔ P ∣ map (F := R →+* A) (algebraMap R A) p
have rw₄ : p = comap (F := R →+* A) (algebraMap R A) P ↔ comap (F := R →+* A) (algebraMap R A) P = p
Tactic: rw [liesOver_iff, dvd_iff_le, under_def, map_le_iff_le_comap,
    IsCoatom.le_iff_eq (by rwa [← isMaximal_def]) (comap_ne_top _ hP), eq_comm]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : IsDedekindDomain A
inst_3 : Algebra R A
p : Ideal R
P : Ideal A
hP : P ≠ ⊤
inst_4 : p.IsMaximal
rw : p = under R P ↔ P ∣ map (F := R →+* A) (algebraMap R A) p
rw₁ : p = under R P ↔ map (F := R →+* A) (algebraMap R A) p ≤ P
rw₂ : p = comap (F := R →+* A) (algebraMap R A) P ↔ map (F := R →+* A) (algebraMap R A) p ≤ P
rw₃ : p = comap (F := R →+* A) (algebraMap R A) P ↔ p ≤ comap (F := R →+* A) (algebraMap R A) P
rw₄ : p = comap (F := R →+* A) (algebraMap R A) P ↔ comap (F := R →+* A) (algebraMap R A) P = p
⊢ P.LiesOver p ↔ P ∣ map (F := R →+* A) (algebraMap R A) p
have rw₅ : comap (F := R →+* A) (algebraMap R A) P = p ↔ comap (F := R →+* A) (algebraMap R A) P = p
Tactic: rw [liesOver_iff, dvd_iff_le, under_def, map_le_iff_le_comap,
    IsCoatom.le_iff_eq (by rwa [← isMaximal_def]) (comap_ne_top _ hP), eq_comm]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (goal)
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I J : Ideal A
h_1 : DvdNotUnit I J
hI : I ≠ 0
H : Ideal A
hunit : ¬IsUnit H
hmul : J = I * H
h : J = I
⊢ I * H = I * 1
have rw : J = I * 1
Tactic: rw [← hmul, h, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (goal)
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I J : Ideal A
h_1 : DvdNotUnit I J
hI : I ≠ 0
H : Ideal A
hunit : ¬IsUnit H
hmul : J = I * H
h : J = I
rw : J = I * 1
⊢ I * H = I * 1
have rw₁ : I = I * 1
Tactic: rw [← hmul, h, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Basic (goal)
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
I J : Ideal A
h_1 : DvdNotUnit I J
hI : I ≠ 0
H : Ideal A
hunit : ¬IsUnit H
hmul : J = I * H
h : J = I
rw : J = I * 1
rw₁ : I = I * 1
⊢ I * H = I * 1
have rw₂ : I = I
Tactic: rw [← hmul, h, mul_one]
-- 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
⊢ WellFounded.{u_2 + 1} (α := Ideal A) DvdNotUnit
have this : WellFoundedGT.{u_2} (Ideal A)
Tactic: have : WellFoundedGT (Ideal A) := inferInstance
-- 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
this : WellFoundedGT.{u_2} (Ideal A)
⊢ WellFounded.{u_2 + 1} (α := Ideal A) DvdNotUnit
have h : ∀ (x x_1 : Ideal A), DvdNotUnit x x_1 ↔ x_1 < x
Tactic: convert! this.wf using 3
-- 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
⊢ P.IsMaximal
have refine : ∀ (b : Ideal A), P < b → b = ⊤
Tactic: refine ⟨⟨mt Ideal.isUnit_iff.mpr hirr.not_isUnit, ?_⟩⟩