case pos
R : Type ?u.278737
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
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hI : (↑I * (↑I)⁻¹)⁻¹ ≤ 1
hI1 : I = ⊤
⊢ ↑I * (↑I)⁻¹ = 1

case neg
R : Type ?u.278737
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
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hI : (↑I * (↑I)⁻¹)⁻¹ ≤ 1
hI1 : ¬I = ⊤
⊢ ↑I * (↑I)⁻¹ = 1
R : Type ?u.278737
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
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hI : (↑I * (↑I)⁻¹)⁻¹ ≤ 1
⊢ ↑I * (↑I)⁻¹ = 1
by_cases hI1 : I = ⊤
case pos
R : Type ?u.278737
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
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hI : (↑I * (↑I)⁻¹)⁻¹ ≤ 1
hI1 : ¬I = ⊤
hNF : IsField A
⊢ ↑I * (↑I)⁻¹ = 1

case neg
R : Type ?u.278737
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
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hI : (↑I * (↑I)⁻¹)⁻¹ ≤ 1
hI1 : ¬I = ⊤
hNF : ¬IsField A
⊢ ↑I * (↑I)⁻¹ = 1
case neg
R : Type ?u.278737
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
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hI : (↑I * (↑I)⁻¹)⁻¹ ≤ 1
hI1 : ¬I = ⊤
⊢ ↑I * (↑I)⁻¹ = 1
by_cases hNF : IsField A
case neg.intro
R : Type ?u.278737
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
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hI : (↑I * (↑I)⁻¹)⁻¹ ≤ 1
hI1 : ¬I = ⊤
hNF : ¬IsField A
J : Ideal A
hJ : ↑J = ↑I * (↑I)⁻¹
⊢ ↑I * (↑I)⁻¹ = 1
case neg
R : Type ?u.278737
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
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hI : (↑I * (↑I)⁻¹)⁻¹ ≤ 1
hI1 : ¬I = ⊤
hNF : ¬IsField A
⊢ ↑I * (↑I)⁻¹ = 1
obtain ⟨J, hJ⟩ : ∃ J : Ideal A, (J : FractionalIdeal A⁰ K) = I * (I : FractionalIdeal A⁰ K)⁻¹ :=
  le_one_iff_exists_coeIdeal.mp mul_one_div_le_one
case pos
R : Type ?u.278737
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
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hI : (↑I * (↑I)⁻¹)⁻¹ ≤ 1
hI1 : ¬I = ⊤
hNF : ¬IsField A
J : Ideal A
hJ : ↑J = ↑I * (↑I)⁻¹
hJ0 : J = ⊥
⊢ ↑I * (↑I)⁻¹ = 1

case neg
R : Type ?u.278737
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
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hI : (↑I * (↑I)⁻¹)⁻¹ ≤ 1
hI1 : ¬I = ⊤
hNF : ¬IsField A
J : Ideal A
hJ : ↑J = ↑I * (↑I)⁻¹
hJ0 : ¬J = ⊥
⊢ ↑I * (↑I)⁻¹ = 1
case neg.intro
R : Type ?u.278737
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
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hI : (↑I * (↑I)⁻¹)⁻¹ ≤ 1
hI1 : ¬I = ⊤
hNF : ¬IsField A
J : Ideal A
hJ : ↑J = ↑I * (↑I)⁻¹
⊢ ↑I * (↑I)⁻¹ = 1
by_cases hJ0 : J = ⊥
case pos
R : Type ?u.278737
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
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hI : (↑I * (↑I)⁻¹)⁻¹ ≤ 1
hI1 : ¬I = ⊤
hNF : ¬IsField A
J : Ideal A
hJ : ↑J = ↑I * (↑I)⁻¹
hJ0 : ¬J = ⊥
hJ1 : J = ⊤
⊢ ↑I * (↑I)⁻¹ = 1

case neg
R : Type ?u.278737
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
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hI : (↑I * (↑I)⁻¹)⁻¹ ≤ 1
hI1 : ¬I = ⊤
hNF : ¬IsField A
J : Ideal A
hJ : ↑J = ↑I * (↑I)⁻¹
hJ0 : ¬J = ⊥
hJ1 : ¬J = ⊤
⊢ ↑I * (↑I)⁻¹ = 1
case neg
R : Type ?u.278737
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
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hI : (↑I * (↑I)⁻¹)⁻¹ ≤ 1
hI1 : ¬I = ⊤
hNF : ¬IsField A
J : Ideal A
hJ : ↑J = ↑I * (↑I)⁻¹
hJ0 : ¬J = ⊥
⊢ ↑I * (↑I)⁻¹ = 1
by_cases hJ1 : J = ⊤
case neg.intro.intro
R : Type ?u.278737
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
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hI : (↑I * (↑I)⁻¹)⁻¹ ≤ 1
hI1 : ¬I = ⊤
hNF : ¬IsField A
J : Ideal A
hJ : ↑J = ↑I * (↑I)⁻¹
hJ0 : ¬J = ⊥
hJ1 : ¬J = ⊤
x : K
hx : x ∈ (↑J)⁻¹
hx1 : ¬x ∈ 1
⊢ ↑I * (↑I)⁻¹ = 1
case neg
R : Type ?u.278737
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
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hI : (↑I * (↑I)⁻¹)⁻¹ ≤ 1
hI1 : ¬I = ⊤
hNF : ¬IsField A
J : Ideal A
hJ : ↑J = ↑I * (↑I)⁻¹
hJ0 : ¬J = ⊥
hJ1 : ¬J = ⊤
⊢ ↑I * (↑I)⁻¹ = 1
obtain ⟨x, hx, hx1⟩ :
  ∃ x : K, x ∈ (J : FractionalIdeal A⁰ K)⁻¹ ∧ x ∉ (1 : FractionalIdeal A⁰ K) :=
  exists_not_mem_one_of_ne_bot hNF hJ0 hJ1
case neg.intro.intro
R : Type ?u.278737
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
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hI : (↑I * (↑I)⁻¹)⁻¹ ≤ 1
hI1 : ¬I = ⊤
hNF : ¬IsField A
J : Ideal A
hJ : ↑J = ↑I * (↑I)⁻¹
hJ0 : ¬J = ⊥
hJ1 : ¬J = ⊤
x : K
hx : x ∈ (↑J)⁻¹
h_abs : ↑I * (↑I)⁻¹ ≠ 1
⊢ x ∈ 1
case neg.intro.intro
R : Type ?u.278737
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
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hI : (↑I * (↑I)⁻¹)⁻¹ ≤ 1
hI1 : ¬I = ⊤
hNF : ¬IsField A
J : Ideal A
hJ : ↑J = ↑I * (↑I)⁻¹
hJ0 : ¬J = ⊥
hJ1 : ¬J = ⊤
x : K
hx : x ∈ (↑J)⁻¹
hx1 : ¬x ∈ 1
⊢ ↑I * (↑I)⁻¹ = 1
contrapose! hx1 with h_abs
case neg.intro.intro
R : Type ?u.278737
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
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hI : (↑I * (↑I)⁻¹)⁻¹ ≤ 1
hI1 : ¬I = ⊤
hNF : ¬IsField A
J : Ideal A
hJ : ↑J = ↑I * (↑I)⁻¹
hJ0 : ¬J = ⊥
hJ1 : ¬J = ⊤
x : K
hx : x ∈ (↑I * (↑I)⁻¹)⁻¹
h_abs : ↑I * (↑I)⁻¹ ≠ 1
⊢ x ∈ 1
case neg.intro.intro
R : Type ?u.278737
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
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hI : (↑I * (↑I)⁻¹)⁻¹ ≤ 1
hI1 : ¬I = ⊤
hNF : ¬IsField A
J : Ideal A
hJ : ↑J = ↑I * (↑I)⁻¹
hJ0 : ¬J = ⊥
hJ1 : ¬J = ⊤
x : K
hx : x ∈ (↑J)⁻¹
h_abs : ↑I * (↑I)⁻¹ ≠ 1
⊢ x ∈ 1
rw [hJ] at hx
no goals
case neg.intro.intro
R : Type ?u.278737
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
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hI : (↑I * (↑I)⁻¹)⁻¹ ≤ 1
hI1 : ¬I = ⊤
hNF : ¬IsField A
J : Ideal A
hJ : ↑J = ↑I * (↑I)⁻¹
hJ0 : ¬J = ⊥
hJ1 : ¬J = ⊤
x : K
hx : x ∈ (↑I * (↑I)⁻¹)⁻¹
h_abs : ↑I * (↑I)⁻¹ ≠ 1
⊢ x ∈ 1
exact hI hx
no goals
case pos
R : Type ?u.278737
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
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hI : (↑I * (↑I)⁻¹)⁻¹ ≤ 1
hI1 : I = ⊤
⊢ ↑I * (↑I)⁻¹ = 1
rw [hI1, coeIdeal_top, one_mul, inv_one]
case pos
R : Type ?u.278737
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
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hI : (↑I * (↑I)⁻¹)⁻¹ ≤ 1
hI1 : ¬I = ⊤
hNF : IsField A
this : Field A := IsField.toField hNF
⊢ ↑I * (↑I)⁻¹ = 1
case pos
R : Type ?u.278737
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
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hI : (↑I * (↑I)⁻¹)⁻¹ ≤ 1
hI1 : ¬I = ⊤
hNF : IsField A
⊢ ↑I * (↑I)⁻¹ = 1
letI := hNF.toField
no goals
case pos
R : Type ?u.278737
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
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hI : (↑I * (↑I)⁻¹)⁻¹ ≤ 1
hI1 : ¬I = ⊤
hNF : IsField A
this : Field A := IsField.toField hNF
⊢ ↑I * (↑I)⁻¹ = 1
rcases hI1 (I.eq_bot_or_top.resolve_left hI0) with ⟨⟩
case pos
R : Type ?u.278737
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
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hI : (↑I * (↑I)⁻¹)⁻¹ ≤ 1
hI1 : ¬I = ⊤
hNF : ¬IsField A
hJ : ↑⊥ = ↑I * (↑I)⁻¹
⊢ ↑I * (↑I)⁻¹ = 1
case pos
R : Type ?u.278737
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
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hI : (↑I * (↑I)⁻¹)⁻¹ ≤ 1
hI1 : ¬I = ⊤
hNF : ¬IsField A
J : Ideal A
hJ : ↑J = ↑I * (↑I)⁻¹
hJ0 : J = ⊥
⊢ ↑I * (↑I)⁻¹ = 1
subst hJ0
case pos
R : Type ?u.278737
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
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hI : (↑I * (↑I)⁻¹)⁻¹ ≤ 1
hI1 : ¬I = ⊤
hNF : ¬IsField A
hJ : ↑⊥ = ↑I * (↑I)⁻¹
⊢ I = ⊥
case pos
R : Type ?u.278737
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
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hI : (↑I * (↑I)⁻¹)⁻¹ ≤ 1
hI1 : ¬I = ⊤
hNF : ¬IsField A
hJ : ↑⊥ = ↑I * (↑I)⁻¹
⊢ ↑I * (↑I)⁻¹ = 1
refine' absurd _ hI0
case pos
R : Type ?u.278737
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
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hI : (↑I * (↑I)⁻¹)⁻¹ ≤ 1
hI1 : ¬I = ⊤
hNF : ¬IsField A
hJ : ↑⊥ = ↑I * (↑I)⁻¹
⊢ ↑I ≤ ↑I * (↑I)⁻¹
case pos
R : Type ?u.278737
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
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hI : (↑I * (↑I)⁻¹)⁻¹ ≤ 1
hI1 : ¬I = ⊤
hNF : ¬IsField A
hJ : ↑⊥ = ↑I * (↑I)⁻¹
⊢ I = ⊥
rw [eq_bot_iff, ← coeIdeal_le_coeIdeal K, hJ]
no goals
case pos
R : Type ?u.278737
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
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hI : (↑I * (↑I)⁻¹)⁻¹ ≤ 1
hI1 : ¬I = ⊤
hNF : ¬IsField A
hJ : ↑⊥ = ↑I * (↑I)⁻¹
⊢ ↑I ≤ ↑I * (↑I)⁻¹
exact coe_ideal_le_self_mul_inv K I
no goals
case pos
R : Type ?u.278737
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
h : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hI : (↑I * (↑I)⁻¹)⁻¹ ≤ 1
hI1 : ¬I = ⊤
hNF : ¬IsField A
J : Ideal A
hJ : ↑J = ↑I * (↑I)⁻¹
hJ0 : ¬J = ⊥
hJ1 : J = ⊤
⊢ ↑I * (↑I)⁻¹ = 1
rw [← hJ, hJ1, coeIdeal_top]