-- Mathlib/RingTheory/DedekindDomain/Ideal.lean
theorem sup_mul_inf (I J : Ideal A) : (I ⊔ J) * (I ⊓ J) = I * J

Proof state:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
this : NormalizedGCDMonoid (Ideal A) := toNormalizedGCDMonoid (Ideal A)
⊢ gcd I J ∣ I ∧ gcd I J ∣ J

Tactic:
exact ⟨gcd_dvd_left _ _, gcd_dvd_right _ _⟩

Result:
no goals

Proof state:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
⊢ (I ⊔ J) * (I ⊓ J) = I * J

Tactic:
letI := UniqueFactorizationMonoid.toNormalizedGCDMonoid (Ideal A)

Result:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
this : NormalizedGCDMonoid (Ideal A) := toNormalizedGCDMonoid (Ideal A)
⊢ (I ⊔ J) * (I ⊓ J) = I * J

Proof state:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
this : NormalizedGCDMonoid (Ideal A) := toNormalizedGCDMonoid (Ideal A)
⊢ gcd I J ∣ I ⊔ J

Tactic:
rw [dvd_iff_le, sup_le_iff, ← dvd_iff_le, ← dvd_iff_le]

Result:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
this : NormalizedGCDMonoid (Ideal A) := toNormalizedGCDMonoid (Ideal A)
⊢ gcd I J ∣ I ∧ gcd I J ∣ J

Proof state:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
this : NormalizedGCDMonoid (Ideal A) := toNormalizedGCDMonoid (Ideal A)
⊢ gcd I J = I ⊔ J

Tactic:
rw [gcd_eq_normalize _ _, normalize_eq]

Result:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
this : NormalizedGCDMonoid (Ideal A) := toNormalizedGCDMonoid (Ideal A)
⊢ gcd I J ∣ I ⊔ J

A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
this : NormalizedGCDMonoid (Ideal A) := toNormalizedGCDMonoid (Ideal A)
⊢ I ⊔ J ∣ gcd I J

Proof state:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
this : NormalizedGCDMonoid (Ideal A) := toNormalizedGCDMonoid (Ideal A)
hgcd : gcd I J = I ⊔ J
⊢ I ∣ lcm I J ∧ J ∣ lcm I J

Tactic:
exact ⟨dvd_lcm_left _ _, dvd_lcm_right _ _⟩

Result:
no goals

Proof state:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
this : NormalizedGCDMonoid (Ideal A) := toNormalizedGCDMonoid (Ideal A)
hgcd : gcd I J = I ⊔ J
⊢ I ⊓ J ≤ I ∧ I ⊓ J ≤ J

Tactic:
simp

Result:
no goals

Proof state:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
this : NormalizedGCDMonoid (Ideal A) := toNormalizedGCDMonoid (Ideal A)
⊢ I ≤ I ⊔ J ∧ J ≤ I ⊔ J

Tactic:
simp

Result:
no goals

Proof state:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
this : NormalizedGCDMonoid (Ideal A) := toNormalizedGCDMonoid (Ideal A)
hgcd : gcd I J = I ⊔ J
⊢ lcm I J = I ⊓ J

Tactic:
rw [lcm_eq_normalize _ _, normalize_eq]

Result:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
this : NormalizedGCDMonoid (Ideal A) := toNormalizedGCDMonoid (Ideal A)
hgcd : gcd I J = I ⊔ J
⊢ lcm I J ∣ I ⊓ J

A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
this : NormalizedGCDMonoid (Ideal A) := toNormalizedGCDMonoid (Ideal A)
hgcd : gcd I J = I ⊔ J
⊢ I ⊓ J ∣ lcm I J

Proof state:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
this : NormalizedGCDMonoid (Ideal A) := toNormalizedGCDMonoid (Ideal A)
hgcd : gcd I J = I ⊔ J
⊢ I ⊓ J ∣ lcm I J

Tactic:
rw [dvd_iff_le, le_inf_iff, ← dvd_iff_le, ← dvd_iff_le]

Result:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
this : NormalizedGCDMonoid (Ideal A) := toNormalizedGCDMonoid (Ideal A)
hgcd : gcd I J = I ⊔ J
⊢ I ∣ lcm I J ∧ J ∣ lcm I J

Proof state:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
this : NormalizedGCDMonoid (Ideal A) := toNormalizedGCDMonoid (Ideal A)
hgcd : gcd I J = I ⊔ J
⊢ lcm I J ∣ I ⊓ J

Tactic:
rw [lcm_dvd_iff, dvd_iff_le, dvd_iff_le]

Result:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
this : NormalizedGCDMonoid (Ideal A) := toNormalizedGCDMonoid (Ideal A)
hgcd : gcd I J = I ⊔ J
⊢ I ⊓ J ≤ I ∧ I ⊓ J ≤ J

Proof state:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
this : NormalizedGCDMonoid (Ideal A) := toNormalizedGCDMonoid (Ideal A)
⊢ I ⊔ J ∣ gcd I J

Tactic:
rw [dvd_gcd_iff, dvd_iff_le, dvd_iff_le]

Result:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
this : NormalizedGCDMonoid (Ideal A) := toNormalizedGCDMonoid (Ideal A)
⊢ I ≤ I ⊔ J ∧ J ≤ I ⊔ J

Proof state:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
this : NormalizedGCDMonoid (Ideal A) := toNormalizedGCDMonoid (Ideal A)
hgcd : gcd I J = I ⊔ J
hlcm : lcm I J = I ⊓ J
⊢ (I ⊔ J) * (I ⊓ J) = I * J

Tactic:
rw [← hgcd, ← hlcm, associated_iff_eq.mp (gcd_mul_lcm _ _)]

Result:
no goals