-- Mathlib/RingTheory/DedekindDomain/Ideal.lean
theorem div_eq_mul_inv [IsDedekindDomain A] (I J : FractionalIdeal A⁰ K) :
    I / J = I * J⁻¹

Proof state:
case neg.refine_1
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDedekindDomain A
I J : FractionalIdeal A⁰ K
hJ : ¬J = 0
⊢ ∀ i ∈ I / J, ∀ j ∈ J, i * j ∈ I

Tactic:
intro x hx y hy

Result:
case neg.refine_1
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDedekindDomain A
I J : FractionalIdeal A⁰ K
hJ : ¬J = 0
x : K
hx : x ∈ I / J
y : K
hy : y ∈ J
⊢ x * y ∈ I

Proof state:
case neg.refine_1
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDedekindDomain A
I J : FractionalIdeal A⁰ K
hJ : ¬J = 0
⊢ I / J * J ≤ I * J⁻¹ * J

Tactic:
rw [mul_assoc, mul_comm J⁻¹, FractionalIdeal.mul_inv_cancel hJ, mul_one, mul_le]

Result:
case neg.refine_1
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDedekindDomain A
I J : FractionalIdeal A⁰ K
hJ : ¬J = 0
⊢ ∀ i ∈ I / J, ∀ j ∈ J, i * j ∈ I

Proof state:
case neg.refine_1
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDedekindDomain A
I J : FractionalIdeal A⁰ K
hJ : ¬J = 0
x : K
hx : ∀ y ∈ J, x * y ∈ I
y : K
hy : y ∈ J
⊢ x * y ∈ I

Tactic:
exact hx y hy

Result:
no goals

Proof state:
case neg
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDedekindDomain A
I J : FractionalIdeal A⁰ K
hJ : ¬J = 0
⊢ I / J = I * J⁻¹

Tactic:
refine le_antisymm ((mul_right_le_iff hJ).mp ?_) ((le_div_iff_mul_le hJ).mpr ?_)

Result:
case neg.refine_1
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDedekindDomain A
I J : FractionalIdeal A⁰ K
hJ : ¬J = 0
⊢ I / J * J ≤ I * J⁻¹ * J

case neg.refine_2
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDedekindDomain A
I J : FractionalIdeal A⁰ K
hJ : ¬J = 0
⊢ I * J⁻¹ * J ≤ I

Proof state:
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDedekindDomain A
I J : FractionalIdeal A⁰ K
⊢ I / J = I * J⁻¹

Tactic:
by_cases hJ : J = 0

Result:
case pos
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDedekindDomain A
I J : FractionalIdeal A⁰ K
hJ : J = 0
⊢ I / J = I * J⁻¹

case neg
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDedekindDomain A
I J : FractionalIdeal A⁰ K
hJ : ¬J = 0
⊢ I / J = I * J⁻¹

Proof state:
case neg.refine_1
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDedekindDomain A
I J : FractionalIdeal A⁰ K
hJ : ¬J = 0
x : K
hx : x ∈ I / J
y : K
hy : y ∈ J
⊢ x * y ∈ I

Tactic:
rw [mem_div_iff_of_nonzero hJ] at hx

Result:
case neg.refine_1
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDedekindDomain A
I J : FractionalIdeal A⁰ K
hJ : ¬J = 0
x : K
hx : ∀ y ∈ J, x * y ∈ I
y : K
hy : y ∈ J
⊢ x * y ∈ I

Proof state:
case neg.refine_2
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDedekindDomain A
I J : FractionalIdeal A⁰ K
hJ : ¬J = 0
⊢ I * J⁻¹ * J ≤ I

Tactic:
rw [mul_assoc, mul_comm J⁻¹, FractionalIdeal.mul_inv_cancel hJ, mul_one]

Result:
no goals

Proof state:
case pos
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDedekindDomain A
I J : FractionalIdeal A⁰ K
hJ : J = 0
⊢ I / J = I * J⁻¹

Tactic:
rw [hJ, div_zero, inv_zero', mul_zero]

Result:
no goals