R : Type ?u.24145
A : Type ?u.24148
K : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Field K
inst✝⁴ : IsDomain A
R₁ : Type u_1
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
I✝ J✝ I J : FractionalIdeal R₁⁰ K
h : I * J = 1
hI : I ≠ 0
⊢ J = I⁻¹
R : Type ?u.24145
A : Type ?u.24148
K : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Field K
inst✝⁴ : IsDomain A
R₁ : Type u_1
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
I✝ J✝ I J : FractionalIdeal R₁⁰ K
h : I * J = 1
⊢ J = I⁻¹
have hI : I ≠ 0 := ne_zero_of_mul_eq_one I J h
R : Type ?u.24145
A : Type ?u.24148
K : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Field K
inst✝⁴ : IsDomain A
R₁ : Type u_1
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
I✝ J✝ I J : FractionalIdeal R₁⁰ K
h : I * J = 1
hI : I ≠ 0
h' : I * (1 / I) = 1
⊢ J = I⁻¹

case h'
R : Type ?u.24145
A : Type ?u.24148
K : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Field K
inst✝⁴ : IsDomain A
R₁ : Type u_1
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
I✝ J✝ I J : FractionalIdeal R₁⁰ K
h : I * J = 1
hI : I ≠ 0
⊢ I * (1 / I) = 1
R : Type ?u.24145
A : Type ?u.24148
K : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Field K
inst✝⁴ : IsDomain A
R₁ : Type u_1
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
I✝ J✝ I J : FractionalIdeal R₁⁰ K
h : I * J = 1
hI : I ≠ 0
⊢ J = I⁻¹
suffices h' : I * (1 / I) = 1
case h'.a
R : Type ?u.24145
A : Type ?u.24148
K : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Field K
inst✝⁴ : IsDomain A
R₁ : Type u_1
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
I✝ J✝ I J : FractionalIdeal R₁⁰ K
h : I * J = 1
hI : I ≠ 0
⊢ I * (1 / I) ≤ 1

case h'.a
R : Type ?u.24145
A : Type ?u.24148
K : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Field K
inst✝⁴ : IsDomain A
R₁ : Type u_1
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
I✝ J✝ I J : FractionalIdeal R₁⁰ K
h : I * J = 1
hI : I ≠ 0
⊢ 1 ≤ I * (1 / I)
case h'
R : Type ?u.24145
A : Type ?u.24148
K : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Field K
inst✝⁴ : IsDomain A
R₁ : Type u_1
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
I✝ J✝ I J : FractionalIdeal R₁⁰ K
h : I * J = 1
hI : I ≠ 0
⊢ I * (1 / I) = 1
apply le_antisymm
case h'.a
R : Type ?u.24145
A : Type ?u.24148
K : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Field K
inst✝⁴ : IsDomain A
R₁ : Type u_1
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
I✝ J✝ I J : FractionalIdeal R₁⁰ K
h : I * J = 1
hI : I ≠ 0
⊢ I * J ≤ I * (I * J / I)
case h'.a
R : Type ?u.24145
A : Type ?u.24148
K : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Field K
inst✝⁴ : IsDomain A
R₁ : Type u_1
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
I✝ J✝ I J : FractionalIdeal R₁⁰ K
h : I * J = 1
hI : I ≠ 0
⊢ 1 ≤ I * (1 / I)
rw [← h]
case h'.a.a
R : Type ?u.24145
A : Type ?u.24148
K : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Field K
inst✝⁴ : IsDomain A
R₁ : Type u_1
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
I✝ J✝ I J : FractionalIdeal R₁⁰ K
h : I * J = 1
hI : I ≠ 0
⊢ J ≤ I * J / I
case h'.a
R : Type ?u.24145
A : Type ?u.24148
K : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Field K
inst✝⁴ : IsDomain A
R₁ : Type u_1
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
I✝ J✝ I J : FractionalIdeal R₁⁰ K
h : I * J = 1
hI : I ≠ 0
⊢ I * J ≤ I * (I * J / I)
apply mul_left_mono I
R : Type ?u.24145
A : Type ?u.24148
K : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Field K
inst✝⁴ : IsDomain A
R₁ : Type u_1
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
I✝ J✝ I J : FractionalIdeal R₁⁰ K
h : I * J = 1
hI : I ≠ 0
⊢ ∀ (x : K), x ∈ J → ∀ (y : K), y ∈ I → x * y ∈ I * J
case h'.a.a
R : Type ?u.24145
A : Type ?u.24148
K : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Field K
inst✝⁴ : IsDomain A
R₁ : Type u_1
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
I✝ J✝ I J : FractionalIdeal R₁⁰ K
h : I * J = 1
hI : I ≠ 0
⊢ J ≤ I * J / I
apply (le_div_iff_of_nonzero hI).mpr _
R : Type ?u.24145
A : Type ?u.24148
K : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Field K
inst✝⁴ : IsDomain A
R₁ : Type u_1
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
I✝ J✝ I J : FractionalIdeal R₁⁰ K
h : I * J = 1
hI : I ≠ 0
y : K
hy : y ∈ J
x : K
hx : x ∈ I
⊢ y * x ∈ I * J
R : Type ?u.24145
A : Type ?u.24148
K : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Field K
inst✝⁴ : IsDomain A
R₁ : Type u_1
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
I✝ J✝ I J : FractionalIdeal R₁⁰ K
h : I * J = 1
hI : I ≠ 0
⊢ ∀ (x : K), x ∈ J → ∀ (y : K), y ∈ I → x * y ∈ I * J
intro y hy x hx
R : Type ?u.24145
A : Type ?u.24148
K : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Field K
inst✝⁴ : IsDomain A
R₁ : Type u_1
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
I✝ J✝ I J : FractionalIdeal R₁⁰ K
h : I * J = 1
hI : I ≠ 0
y : K
hy : y ∈ J
x : K
hx : x ∈ I
⊢ x * y ∈ I * J
R : Type ?u.24145
A : Type ?u.24148
K : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Field K
inst✝⁴ : IsDomain A
R₁ : Type u_1
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
I✝ J✝ I J : FractionalIdeal R₁⁰ K
h : I * J = 1
hI : I ≠ 0
y : K
hy : y ∈ J
x : K
hx : x ∈ I
⊢ y * x ∈ I * J
rw [mul_comm]
no goals
R : Type ?u.24145
A : Type ?u.24148
K : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Field K
inst✝⁴ : IsDomain A
R₁ : Type u_1
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
I✝ J✝ I J : FractionalIdeal R₁⁰ K
h : I * J = 1
hI : I ≠ 0
y : K
hy : y ∈ J
x : K
hx : x ∈ I
⊢ x * y ∈ I * J
exact mul_mem_mul hx hy
no goals
R : Type ?u.24145
A : Type ?u.24148
K : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Field K
inst✝⁴ : IsDomain A
R₁ : Type u_1
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
I✝ J✝ I J : FractionalIdeal R₁⁰ K
h : I * J = 1
hI : I ≠ 0
h' : I * (1 / I) = 1
⊢ J = I⁻¹
exact congr_arg Units.inv <|
  @Units.ext _ _ (Units.mkOfMulEqOne _ _ h) (Units.mkOfMulEqOne _ _ h') rfl
R : Type ?u.24145
A : Type ?u.24148
K : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Field K
inst✝⁴ : IsDomain A
R₁ : Type u_1
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
I✝ J✝ I J : FractionalIdeal R₁⁰ K
h : I * J = 1
hI : I ≠ 0
⊢ ∀ (i : K), i ∈ I → ∀ (j : K), j ∈ 1 / I → i * j ∈ 1
case h'.a
R : Type ?u.24145
A : Type ?u.24148
K : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Field K
inst✝⁴ : IsDomain A
R₁ : Type u_1
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
I✝ J✝ I J : FractionalIdeal R₁⁰ K
h : I * J = 1
hI : I ≠ 0
⊢ I * (1 / I) ≤ 1
apply mul_le.mpr _
R : Type ?u.24145
A : Type ?u.24148
K : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Field K
inst✝⁴ : IsDomain A
R₁ : Type u_1
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
I✝ J✝ I J : FractionalIdeal R₁⁰ K
h : I * J = 1
hI : I ≠ 0
x : K
hx : x ∈ I
y : K
hy : y ∈ 1 / I
⊢ x * y ∈ 1
R : Type ?u.24145
A : Type ?u.24148
K : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Field K
inst✝⁴ : IsDomain A
R₁ : Type u_1
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
I✝ J✝ I J : FractionalIdeal R₁⁰ K
h : I * J = 1
hI : I ≠ 0
⊢ ∀ (i : K), i ∈ I → ∀ (j : K), j ∈ 1 / I → i * j ∈ 1
intro x hx y hy
R : Type ?u.24145
A : Type ?u.24148
K : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Field K
inst✝⁴ : IsDomain A
R₁ : Type u_1
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
I✝ J✝ I J : FractionalIdeal R₁⁰ K
h : I * J = 1
hI : I ≠ 0
x : K
hx : x ∈ I
y : K
hy : y ∈ 1 / I
⊢ y * x ∈ 1
R : Type ?u.24145
A : Type ?u.24148
K : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Field K
inst✝⁴ : IsDomain A
R₁ : Type u_1
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
I✝ J✝ I J : FractionalIdeal R₁⁰ K
h : I * J = 1
hI : I ≠ 0
x : K
hx : x ∈ I
y : K
hy : y ∈ 1 / I
⊢ x * y ∈ 1
rw [mul_comm]
no goals
R : Type ?u.24145
A : Type ?u.24148
K : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Field K
inst✝⁴ : IsDomain A
R₁ : Type u_1
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
I✝ J✝ I J : FractionalIdeal R₁⁰ K
h : I * J = 1
hI : I ≠ 0
x : K
hx : x ∈ I
y : K
hy : y ∈ 1 / I
⊢ y * x ∈ 1
exact (mem_div_iff_of_nonzero hI).mp hy x hx