-- Mathlib/RingTheory/DedekindDomain/Ideal.lean
theorem Ideal.dvd_iff_le {I J : Ideal A} : I ∣ J ↔ J ≤ I :=
  ⟨Ideal.le_of_dvd, fun h => by
    by_cases hI : I = ⊥
    · have hJ : J = ⊥

Proof state:
case pos
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
h : J ≤ I
hI : I = ⊥
⊢ I ∣ J

Tactic:
have hJ : J = ⊥ := by rwa [hI, ← eq_bot_iff] at h

Result:
case pos
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
h : J ≤ I
hI : I = ⊥
hJ : J = ⊥
⊢ I ∣ J

Proof state:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
h : J ≤ I
hI : I = ⊥
⊢ J = ⊥

Tactic:
rwa [hI, ← eq_bot_iff] at h

Result:
no goals

Proof state:
case pos
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
h : J ≤ I
hI : I = ⊥
hJ : J = ⊥
⊢ I ∣ J

Tactic:
rw [hI, hJ]

Result:
no goals

Proof state:
case neg
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
h : J ≤ I
hI : ¬I = ⊥
hI' : ↑I ≠ 0
this : (↑I)⁻¹ * ↑J ≤ 1
⊢ I ∣ J

Tactic:
obtain ⟨H, hH⟩ := le_one_iff_exists_coeIdeal.mp this

Result:
case neg.intro
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
h : J ≤ I
hI : ¬I = ⊥
hI' : ↑I ≠ 0
this : (↑I)⁻¹ * ↑J ≤ 1
H : Ideal A
hH : ↑H = (↑I)⁻¹ * ↑J
⊢ I ∣ J

Proof state:
case h
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
h : J ≤ I
hI : ¬I = ⊥
hI' : ↑I ≠ 0
this : (↑I)⁻¹ * ↑J ≤ 1
H : Ideal A
hH : ↑H = (↑I)⁻¹ * ↑J
⊢ ↑J = ↑(I * H)

Tactic:
rw [coeIdeal_mul, hH, ← mul_assoc, mul_inv_cancel₀ hI', one_mul]

Result:
no goals

Proof state:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
h : J ≤ I
hI : ¬I = ⊥
hI' : ↑I ≠ 0
⊢ (↑I)⁻¹ * ↑J ≤ (↑I)⁻¹ * ↑I

Tactic:
exact mul_left_mono _ ((coeIdeal_le_coeIdeal _).mpr h)

Result:
no goals

Proof state:
case neg.intro
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
h : J ≤ I
hI : ¬I = ⊥
hI' : ↑I ≠ 0
this : (↑I)⁻¹ * ↑J ≤ 1
H : Ideal A
hH : ↑H = (↑I)⁻¹ * ↑J
⊢ I ∣ J

Tactic:
use H

Result:
case h
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
h : J ≤ I
hI : ¬I = ⊥
hI' : ↑I ≠ 0
this : (↑I)⁻¹ * ↑J ≤ 1
H : Ideal A
hH : ↑H = (↑I)⁻¹ * ↑J
⊢ J = I * H

Proof state:
case h
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
h : J ≤ I
hI : ¬I = ⊥
hI' : ↑I ≠ 0
this : (↑I)⁻¹ * ↑J ≤ 1
H : Ideal A
hH : ↑H = (↑I)⁻¹ * ↑J
⊢ J = I * H

Tactic:
refine coeIdeal_injective (show (J : FractionalIdeal A⁰ (FractionRing A)) = ↑(I * H) from ?_)

Result:
case h
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
h : J ≤ I
hI : ¬I = ⊥
hI' : ↑I ≠ 0
this : (↑I)⁻¹ * ↑J ≤ 1
H : Ideal A
hH : ↑H = (↑I)⁻¹ * ↑J
⊢ ↑J = ↑(I * H)

Proof state:
case neg
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
h : J ≤ I
hI : ¬I = ⊥
⊢ I ∣ J

Tactic:
have hI' : (I : FractionalIdeal A⁰ (FractionRing A)) ≠ 0 := coeIdeal_ne_zero.mpr hI

Result:
case neg
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
h : J ≤ I
hI : ¬I = ⊥
hI' : ↑I ≠ 0
⊢ I ∣ J

Proof state:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
h : J ≤ I
hI : ¬I = ⊥
hI' : ↑I ≠ 0
⊢ (↑I)⁻¹ * ↑J ≤ 1

Tactic:
rw [← inv_mul_cancel₀ hI']

Result:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
h : J ≤ I
hI : ¬I = ⊥
hI' : ↑I ≠ 0
⊢ (↑I)⁻¹ * ↑J ≤ (↑I)⁻¹ * ↑I

Proof state:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
h : J ≤ I
⊢ I ∣ J

Tactic:
by_cases hI : I = ⊥

Result:
case pos
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
h : J ≤ I
hI : I = ⊥
⊢ I ∣ J

case neg
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
h : J ≤ I
hI : ¬I = ⊥
⊢ I ∣ J

Proof state:
case neg
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
h : J ≤ I
hI : ¬I = ⊥
hI' : ↑I ≠ 0
⊢ I ∣ J

Tactic:
have : (I : FractionalIdeal A⁰ (FractionRing A))⁻¹ * J ≤ 1 := by
  rw [← inv_mul_cancel₀ hI']
  exact mul_left_mono _ ((coeIdeal_le_coeIdeal _).mpr h)

Result:
case neg
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
h : J ≤ I
hI : ¬I = ⊥
hI' : ↑I ≠ 0
this : (↑I)⁻¹ * ↑J ≤ 1
⊢ I ∣ J