case intro.intro.intro
R : Type ?u.613996
A : Type u_1
K : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDedekindDomain A
I : FractionalIdeal A⁰ K
hne : I ≠ 0
a : A
J : Ideal A
ha : a ≠ 0
hJ : I = spanSingleton A⁰ (↑(algebraMap A K) a)⁻¹ * ↑J
⊢ I * I⁻¹ = 1
R : Type ?u.613996
A : Type u_1
K : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDedekindDomain A
I : FractionalIdeal A⁰ K
hne : I ≠ 0
⊢ I * I⁻¹ = 1
obtain ⟨a, J, ha, hJ⟩ :
  ∃ (a : A) (aI : Ideal A), a ≠ 0 ∧ I = spanSingleton A⁰ (algebraMap A K a)⁻¹ * aI :=
  exists_eq_spanSingleton_mul I
case intro.intro.intro
R : Type ?u.613996
A : Type u_1
K : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDedekindDomain A
I : FractionalIdeal A⁰ K
hne : I ≠ 0
a : A
J : Ideal A
ha : a ≠ 0
hJ : I = spanSingleton A⁰ (↑(algebraMap A K) a)⁻¹ * ↑J
h₂ : I * (spanSingleton A⁰ (↑(algebraMap A K) a) * (↑J)⁻¹) = 1
⊢ I * I⁻¹ = 1

case h₂
R : Type ?u.613996
A : Type u_1
K : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDedekindDomain A
I : FractionalIdeal A⁰ K
hne : I ≠ 0
a : A
J : Ideal A
ha : a ≠ 0
hJ : I = spanSingleton A⁰ (↑(algebraMap A K) a)⁻¹ * ↑J
⊢ I * (spanSingleton A⁰ (↑(algebraMap A K) a) * (↑J)⁻¹) = 1
case intro.intro.intro
R : Type ?u.613996
A : Type u_1
K : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDedekindDomain A
I : FractionalIdeal A⁰ K
hne : I ≠ 0
a : A
J : Ideal A
ha : a ≠ 0
hJ : I = spanSingleton A⁰ (↑(algebraMap A K) a)⁻¹ * ↑J
⊢ I * I⁻¹ = 1
suffices h₂ : I * (spanSingleton A⁰ (algebraMap _ _ a) * (J : FractionalIdeal A⁰ K)⁻¹) = 1
case h₂
R : Type ?u.613996
A : Type u_1
K : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDedekindDomain A
a : A
J : Ideal A
ha : a ≠ 0
hne : spanSingleton A⁰ (↑(algebraMap A K) a)⁻¹ * ↑J ≠ 0
⊢ spanSingleton A⁰ (↑(algebraMap A K) a)⁻¹ * ↑J * (spanSingleton A⁰ (↑(algebraMap A K) a) * (↑J)⁻¹) = 1
case h₂
R : Type ?u.613996
A : Type u_1
K : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDedekindDomain A
I : FractionalIdeal A⁰ K
hne : I ≠ 0
a : A
J : Ideal A
ha : a ≠ 0
hJ : I = spanSingleton A⁰ (↑(algebraMap A K) a)⁻¹ * ↑J
⊢ I * (spanSingleton A⁰ (↑(algebraMap A K) a) * (↑J)⁻¹) = 1
subst hJ
case h₂
R : Type ?u.613996
A : Type u_1
K : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDedekindDomain A
a : A
J : Ideal A
ha : a ≠ 0
hne : spanSingleton A⁰ (↑(algebraMap A K) a)⁻¹ * ↑J ≠ 0
⊢ ↑(algebraMap A K) a ≠ 0

case h₂.hI0
R : Type ?u.613996
A : Type u_1
K : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDedekindDomain A
a : A
J : Ideal A
ha : a ≠ 0
hne : spanSingleton A⁰ (↑(algebraMap A K) a)⁻¹ * ↑J ≠ 0
⊢ J ≠ ⊥
case h₂
R : Type ?u.613996
A : Type u_1
K : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDedekindDomain A
a : A
J : Ideal A
ha : a ≠ 0
hne : spanSingleton A⁰ (↑(algebraMap A K) a)⁻¹ * ↑J ≠ 0
⊢ spanSingleton A⁰ (↑(algebraMap A K) a)⁻¹ * ↑J * (spanSingleton A⁰ (↑(algebraMap A K) a) * (↑J)⁻¹) = 1
rw [mul_assoc, mul_left_comm (J : FractionalIdeal A⁰ K), coe_ideal_mul_inv, mul_one,
  spanSingleton_mul_spanSingleton, inv_mul_cancel, spanSingleton_one]
case intro.intro.intro
R : Type ?u.613996
A : Type u_1
K : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDedekindDomain A
I : FractionalIdeal A⁰ K
hne : I ≠ 0
a : A
J : Ideal A
ha : a ≠ 0
hJ : I = spanSingleton A⁰ (↑(algebraMap A K) a)⁻¹ * ↑J
h₂ : I * (spanSingleton A⁰ (↑(algebraMap A K) a) * (↑J)⁻¹) = 1
⊢ ∃ J, I * J = 1
case intro.intro.intro
R : Type ?u.613996
A : Type u_1
K : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDedekindDomain A
I : FractionalIdeal A⁰ K
hne : I ≠ 0
a : A
J : Ideal A
ha : a ≠ 0
hJ : I = spanSingleton A⁰ (↑(algebraMap A K) a)⁻¹ * ↑J
h₂ : I * (spanSingleton A⁰ (↑(algebraMap A K) a) * (↑J)⁻¹) = 1
⊢ I * I⁻¹ = 1
rw [mul_inv_cancel_iff]
no goals
case intro.intro.intro
R : Type ?u.613996
A : Type u_1
K : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDedekindDomain A
I : FractionalIdeal A⁰ K
hne : I ≠ 0
a : A
J : Ideal A
ha : a ≠ 0
hJ : I = spanSingleton A⁰ (↑(algebraMap A K) a)⁻¹ * ↑J
h₂ : I * (spanSingleton A⁰ (↑(algebraMap A K) a) * (↑J)⁻¹) = 1
⊢ ∃ J, I * J = 1
exact ⟨spanSingleton A⁰ (algebraMap _ _ a) * (J : FractionalIdeal A⁰ K)⁻¹, h₂⟩
no goals
case h₂
R : Type ?u.613996
A : Type u_1
K : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDedekindDomain A
a : A
J : Ideal A
ha : a ≠ 0
hne : spanSingleton A⁰ (↑(algebraMap A K) a)⁻¹ * ↑J ≠ 0
⊢ ↑(algebraMap A K) a ≠ 0
exact mt ((injective_iff_map_eq_zero (algebraMap A K)).mp (IsFractionRing.injective A K) _) ha
no goals
case h₂.hI0
R : Type ?u.613996
A : Type u_1
K : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDedekindDomain A
a : A
J : Ideal A
ha : a ≠ 0
hne : spanSingleton A⁰ (↑(algebraMap A K) a)⁻¹ * ↑J ≠ 0
⊢ J ≠ ⊥
exact coeIdeal_ne_zero.mp (right_ne_zero_of_mul hne)