R : Type ?u.874803
A : Type u_1
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_2
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal A⁰ K := spanFinset A s f
⊢ ∃ a, (∀ (i : ι), i ∈ s → IsLocalization.IsInteger A (a * f i)) ∧ ∃ i, i ∈ s ∧ ¬a * f i ∈ ↑J
R : Type ?u.874803
A : Type u_1
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_2
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
⊢ ∃ a, (∀ (i : ι), i ∈ s → IsLocalization.IsInteger A (a * f i)) ∧ ∃ i, i ∈ s ∧ ¬a * f i ∈ ↑J
let I : FractionalIdeal A⁰ K := spanFinset A s f
R : Type ?u.874803
A : Type u_1
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_2
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal A⁰ K := spanFinset A s f
hI0 : I ≠ 0
⊢ ∃ a, (∀ (i : ι), i ∈ s → IsLocalization.IsInteger A (a * f i)) ∧ ∃ i, i ∈ s ∧ ¬a * f i ∈ ↑J
R : Type ?u.874803
A : Type u_1
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_2
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal A⁰ K := spanFinset A s f
⊢ ∃ a, (∀ (i : ι), i ∈ s → IsLocalization.IsInteger A (a * f i)) ∧ ∃ i, i ∈ s ∧ ¬a * f i ∈ ↑J
have hI0 : I ≠ 0 := spanFinset_ne_zero.mpr ⟨j, hjs, hjf⟩
R : Type ?u.874803
A : Type u_1
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_2
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal A⁰ K := spanFinset A s f
hI0 : I ≠ 0
⊢ ↑J < 1
R : Type ?u.874803
A : Type u_1
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_2
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal A⁰ K := spanFinset A s f
hI0 : I ≠ 0
⊢ ↑J / I < I⁻¹
calc
  ↑J / I = ↑J * I⁻¹ := div_eq_mul_inv (↑J) I
  _ < 1 * I⁻¹ := (mul_right_strictMono (inv_ne_zero hI0) ?_)
  _ = I⁻¹ := one_mul _
case intro.intro.intro
R : Type ?u.874803
A : Type u_1
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_2
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : ↑J / I < I⁻¹
left✝ : ↑J / I ≤ I⁻¹
a : K
hI : a ∈ I⁻¹
hpI : ¬a ∈ ↑J / I
⊢ ∃ a, (∀ (i : ι), i ∈ s → IsLocalization.IsInteger A (a * f i)) ∧ ∃ i, i ∈ s ∧ ¬a * f i ∈ ↑J
R : Type ?u.874803
A : Type u_1
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_2
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : ↑J / I < I⁻¹
⊢ ∃ a, (∀ (i : ι), i ∈ s → IsLocalization.IsInteger A (a * f i)) ∧ ∃ i, i ∈ s ∧ ¬a * f i ∈ ↑J
obtain ⟨_, a, hI, hpI⟩ := SetLike.lt_iff_le_and_exists.mp this
case intro.intro.intro
R : Type ?u.874803
A : Type u_1
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_2
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : ↑J / I < I⁻¹
left✝ : ↑J / I ≤ I⁻¹
a : K
hI : ∀ (y : K), y ∈ I → a * y ∈ 1
hpI : ¬a ∈ ↑J / I
⊢ ∃ a, (∀ (i : ι), i ∈ s → IsLocalization.IsInteger A (a * f i)) ∧ ∃ i, i ∈ s ∧ ¬a * f i ∈ ↑J
case intro.intro.intro
R : Type ?u.874803
A : Type u_1
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_2
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : ↑J / I < I⁻¹
left✝ : ↑J / I ≤ I⁻¹
a : K
hI : a ∈ I⁻¹
hpI : ¬a ∈ ↑J / I
⊢ ∃ a, (∀ (i : ι), i ∈ s → IsLocalization.IsInteger A (a * f i)) ∧ ∃ i, i ∈ s ∧ ¬a * f i ∈ ↑J
rw [mem_inv_iff hI0] at hI
case intro.intro.intro.refine'_1
R : Type ?u.874803
A : Type u_1
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_2
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : ↑J / I < I⁻¹
left✝ : ↑J / I ≤ I⁻¹
a : K
hI : ∀ (y : K), y ∈ I → a * y ∈ 1
hpI : ¬a ∈ ↑J / I
i : ι
hi : i ∈ s
⊢ IsLocalization.IsInteger A (a * f i)

case intro.intro.intro.refine'_2
R : Type ?u.874803
A : Type u_1
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_2
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : ↑J / I < I⁻¹
left✝ : ↑J / I ≤ I⁻¹
a : K
hI : ∀ (y : K), y ∈ I → a * y ∈ 1
hpI : ¬a ∈ ↑J / I
⊢ ∃ i, i ∈ s ∧ ¬a * f i ∈ ↑J
case intro.intro.intro
R : Type ?u.874803
A : Type u_1
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_2
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : ↑J / I < I⁻¹
left✝ : ↑J / I ≤ I⁻¹
a : K
hI : ∀ (y : K), y ∈ I → a * y ∈ 1
hpI : ¬a ∈ ↑J / I
⊢ ∃ a, (∀ (i : ι), i ∈ s → IsLocalization.IsInteger A (a * f i)) ∧ ∃ i, i ∈ s ∧ ¬a * f i ∈ ↑J
refine' ⟨a, fun i hi => _, _⟩
no goals
case intro.intro.intro.refine'_1
R : Type ?u.874803
A : Type u_1
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_2
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : ↑J / I < I⁻¹
left✝ : ↑J / I ≤ I⁻¹
a : K
hI : ∀ (y : K), y ∈ I → a * y ∈ 1
hpI : ¬a ∈ ↑J / I
i : ι
hi : i ∈ s
⊢ IsLocalization.IsInteger A (a * f i)
exact (mem_one_iff _).mp (hI (f i) (Submodule.subset_span (Set.mem_image_of_mem f hi)))
case intro.intro.intro.refine'_2
R : Type ?u.874803
A : Type u_1
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_2
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : ↑J / I < I⁻¹
left✝ : ↑J / I ≤ I⁻¹
a : K
hI : ∀ (y : K), y ∈ I → a * y ∈ 1
hpI : ∀ (i : ι), i ∈ s → a * f i ∈ ↑J
⊢ a ∈ ↑J / spanFinset A s f
case intro.intro.intro.refine'_2
R : Type ?u.874803
A : Type u_1
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_2
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : ↑J / I < I⁻¹
left✝ : ↑J / I ≤ I⁻¹
a : K
hI : ∀ (y : K), y ∈ I → a * y ∈ 1
hpI : ¬a ∈ ↑J / I
⊢ ∃ i, i ∈ s ∧ ¬a * f i ∈ ↑J
contrapose! hpI
case intro.intro.intro.refine'_2.refine'_1
R : Type ?u.874803
A : Type u_1
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_2
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : ↑J / I < I⁻¹
left✝ : ↑J / I ≤ I⁻¹
a : K
hI : ∀ (y : K), y ∈ I → a * y ∈ 1
hpI : ∀ (i : ι), i ∈ s → a * f i ∈ ↑J
y : K
hy : y ∈ I
⊢ ∀ (x : K), x ∈ f '' ↑s → a * x ∈ ↑J

case intro.intro.intro.refine'_2.refine'_2
R : Type ?u.874803
A : Type u_1
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_2
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : ↑J / I < I⁻¹
left✝ : ↑J / I ≤ I⁻¹
a : K
hI : ∀ (y : K), y ∈ I → a * y ∈ 1
hpI : ∀ (i : ι), i ∈ s → a * f i ∈ ↑J
y : K
hy : y ∈ I
⊢ a * 0 ∈ ↑J

case intro.intro.intro.refine'_2.refine'_3
R : Type ?u.874803
A : Type u_1
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_2
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : ↑J / I < I⁻¹
left✝ : ↑J / I ≤ I⁻¹
a : K
hI : ∀ (y : K), y ∈ I → a * y ∈ 1
hpI : ∀ (i : ι), i ∈ s → a * f i ∈ ↑J
y : K
hy : y ∈ I
⊢ ∀ (x y : K), a * x ∈ ↑J → a * y ∈ ↑J → a * (x + y) ∈ ↑J

case intro.intro.intro.refine'_2.refine'_4
R : Type ?u.874803
A : Type u_1
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_2
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : ↑J / I < I⁻¹
left✝ : ↑J / I ≤ I⁻¹
a : K
hI : ∀ (y : K), y ∈ I → a * y ∈ 1
hpI : ∀ (i : ι), i ∈ s → a * f i ∈ ↑J
y : K
hy : y ∈ I
⊢ ∀ (a_1 : A) (x : K), a * x ∈ ↑J → a * a_1 • x ∈ ↑J
case intro.intro.intro.refine'_2
R : Type ?u.874803
A : Type u_1
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_2
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : ↑J / I < I⁻¹
left✝ : ↑J / I ≤ I⁻¹
a : K
hI : ∀ (y : K), y ∈ I → a * y ∈ 1
hpI : ∀ (i : ι), i ∈ s → a * f i ∈ ↑J
⊢ a ∈ ↑J / spanFinset A s f
refine' (mem_div_iff_of_nonzero hI0).mpr fun y hy => Submodule.span_induction hy _ _ _ _
case intro.intro.intro.refine'_2.refine'_1.intro.intro
R : Type ?u.874803
A : Type u_1
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_2
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : ↑J / I < I⁻¹
left✝ : ↑J / I ≤ I⁻¹
a : K
hI : ∀ (y : K), y ∈ I → a * y ∈ 1
hpI : ∀ (i : ι), i ∈ s → a * f i ∈ ↑J
y : K
hy : y ∈ I
i : ι
hi : i ∈ ↑s
⊢ a * f i ∈ ↑J
case intro.intro.intro.refine'_2.refine'_1
R : Type ?u.874803
A : Type u_1
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_2
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : ↑J / I < I⁻¹
left✝ : ↑J / I ≤ I⁻¹
a : K
hI : ∀ (y : K), y ∈ I → a * y ∈ 1
hpI : ∀ (i : ι), i ∈ s → a * f i ∈ ↑J
y : K
hy : y ∈ I
⊢ ∀ (x : K), x ∈ f '' ↑s → a * x ∈ ↑J
rintro _ ⟨i, hi, rfl⟩
no goals
case intro.intro.intro.refine'_2.refine'_1.intro.intro
R : Type ?u.874803
A : Type u_1
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_2
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : ↑J / I < I⁻¹
left✝ : ↑J / I ≤ I⁻¹
a : K
hI : ∀ (y : K), y ∈ I → a * y ∈ 1
hpI : ∀ (i : ι), i ∈ s → a * f i ∈ ↑J
y : K
hy : y ∈ I
i : ι
hi : i ∈ ↑s
⊢ a * f i ∈ ↑J
exact hpI i hi
case intro.intro.intro.refine'_2.refine'_2
R : Type ?u.874803
A : Type u_1
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_2
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : ↑J / I < I⁻¹
left✝ : ↑J / I ≤ I⁻¹
a : K
hI : ∀ (y : K), y ∈ I → a * y ∈ 1
hpI : ∀ (i : ι), i ∈ s → a * f i ∈ ↑J
y : K
hy : y ∈ I
⊢ 0 ∈ ↑J
case intro.intro.intro.refine'_2.refine'_2
R : Type ?u.874803
A : Type u_1
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_2
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : ↑J / I < I⁻¹
left✝ : ↑J / I ≤ I⁻¹
a : K
hI : ∀ (y : K), y ∈ I → a * y ∈ 1
hpI : ∀ (i : ι), i ∈ s → a * f i ∈ ↑J
y : K
hy : y ∈ I
⊢ a * 0 ∈ ↑J
rw [MulZeroClass.mul_zero]
no goals
case intro.intro.intro.refine'_2.refine'_2
R : Type ?u.874803
A : Type u_1
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_2
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : ↑J / I < I⁻¹
left✝ : ↑J / I ≤ I⁻¹
a : K
hI : ∀ (y : K), y ∈ I → a * y ∈ 1
hpI : ∀ (i : ι), i ∈ s → a * f i ∈ ↑J
y : K
hy : y ∈ I
⊢ 0 ∈ ↑J
exact Submodule.zero_mem _
case intro.intro.intro.refine'_2.refine'_3
R : Type ?u.874803
A : Type u_1
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_2
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : ↑J / I < I⁻¹
left✝ : ↑J / I ≤ I⁻¹
a : K
hI : ∀ (y : K), y ∈ I → a * y ∈ 1
hpI : ∀ (i : ι), i ∈ s → a * f i ∈ ↑J
y✝ : K
hy✝ : y✝ ∈ I
x y : K
hx : a * x ∈ ↑J
hy : a * y ∈ ↑J
⊢ a * (x + y) ∈ ↑J
case intro.intro.intro.refine'_2.refine'_3
R : Type ?u.874803
A : Type u_1
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_2
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : ↑J / I < I⁻¹
left✝ : ↑J / I ≤ I⁻¹
a : K
hI : ∀ (y : K), y ∈ I → a * y ∈ 1
hpI : ∀ (i : ι), i ∈ s → a * f i ∈ ↑J
y : K
hy : y ∈ I
⊢ ∀ (x y : K), a * x ∈ ↑J → a * y ∈ ↑J → a * (x + y) ∈ ↑J
intro x y hx hy
case intro.intro.intro.refine'_2.refine'_3
R : Type ?u.874803
A : Type u_1
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_2
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : ↑J / I < I⁻¹
left✝ : ↑J / I ≤ I⁻¹
a : K
hI : ∀ (y : K), y ∈ I → a * y ∈ 1
hpI : ∀ (i : ι), i ∈ s → a * f i ∈ ↑J
y✝ : K
hy✝ : y✝ ∈ I
x y : K
hx : a * x ∈ ↑J
hy : a * y ∈ ↑J
⊢ a * x + a * y ∈ ↑J
case intro.intro.intro.refine'_2.refine'_3
R : Type ?u.874803
A : Type u_1
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_2
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : ↑J / I < I⁻¹
left✝ : ↑J / I ≤ I⁻¹
a : K
hI : ∀ (y : K), y ∈ I → a * y ∈ 1
hpI : ∀ (i : ι), i ∈ s → a * f i ∈ ↑J
y✝ : K
hy✝ : y✝ ∈ I
x y : K
hx : a * x ∈ ↑J
hy : a * y ∈ ↑J
⊢ a * (x + y) ∈ ↑J
rw [mul_add]
no goals
case intro.intro.intro.refine'_2.refine'_3
R : Type ?u.874803
A : Type u_1
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_2
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : ↑J / I < I⁻¹
left✝ : ↑J / I ≤ I⁻¹
a : K
hI : ∀ (y : K), y ∈ I → a * y ∈ 1
hpI : ∀ (i : ι), i ∈ s → a * f i ∈ ↑J
y✝ : K
hy✝ : y✝ ∈ I
x y : K
hx : a * x ∈ ↑J
hy : a * y ∈ ↑J
⊢ a * x + a * y ∈ ↑J
exact Submodule.add_mem _ hx hy
case intro.intro.intro.refine'_2.refine'_4
R : Type ?u.874803
A : Type u_1
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_2
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : ↑J / I < I⁻¹
left✝ : ↑J / I ≤ I⁻¹
a : K
hI : ∀ (y : K), y ∈ I → a * y ∈ 1
hpI : ∀ (i : ι), i ∈ s → a * f i ∈ ↑J
y : K
hy : y ∈ I
b : A
x : K
hx : a * x ∈ ↑J
⊢ a * b • x ∈ ↑J
case intro.intro.intro.refine'_2.refine'_4
R : Type ?u.874803
A : Type u_1
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_2
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : ↑J / I < I⁻¹
left✝ : ↑J / I ≤ I⁻¹
a : K
hI : ∀ (y : K), y ∈ I → a * y ∈ 1
hpI : ∀ (i : ι), i ∈ s → a * f i ∈ ↑J
y : K
hy : y ∈ I
⊢ ∀ (a_1 : A) (x : K), a * x ∈ ↑J → a * a_1 • x ∈ ↑J
intro b x hx
case intro.intro.intro.refine'_2.refine'_4
R : Type ?u.874803
A : Type u_1
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_2
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : ↑J / I < I⁻¹
left✝ : ↑J / I ≤ I⁻¹
a : K
hI : ∀ (y : K), y ∈ I → a * y ∈ 1
hpI : ∀ (i : ι), i ∈ s → a * f i ∈ ↑J
y : K
hy : y ∈ I
b : A
x : K
hx : a * x ∈ ↑J
⊢ b • (a * x) ∈ ↑J
case intro.intro.intro.refine'_2.refine'_4
R : Type ?u.874803
A : Type u_1
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_2
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : ↑J / I < I⁻¹
left✝ : ↑J / I ≤ I⁻¹
a : K
hI : ∀ (y : K), y ∈ I → a * y ∈ 1
hpI : ∀ (i : ι), i ∈ s → a * f i ∈ ↑J
y : K
hy : y ∈ I
b : A
x : K
hx : a * x ∈ ↑J
⊢ a * b • x ∈ ↑J
rw [mul_smul_comm]
no goals
case intro.intro.intro.refine'_2.refine'_4
R : Type ?u.874803
A : Type u_1
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_2
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal A⁰ K := spanFinset A s f
hI0 : I ≠ 0
this : ↑J / I < I⁻¹
left✝ : ↑J / I ≤ I⁻¹
a : K
hI : ∀ (y : K), y ∈ I → a * y ∈ 1
hpI : ∀ (i : ι), i ∈ s → a * f i ∈ ↑J
y : K
hy : y ∈ I
b : A
x : K
hx : a * x ∈ ↑J
⊢ b • (a * x) ∈ ↑J
exact Submodule.smul_mem _ b hx
R : Type ?u.874803
A : Type u_1
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_2
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal A⁰ K := spanFinset A s f
hI0 : I ≠ 0
⊢ ↑J < ↑⊤
R : Type ?u.874803
A : Type u_1
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_2
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal A⁰ K := spanFinset A s f
hI0 : I ≠ 0
⊢ ↑J < 1
rw [← coeIdeal_top]
no goals
R : Type ?u.874803
A : Type u_1
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_2
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal A⁰ K := spanFinset A s f
hI0 : I ≠ 0
⊢ ↑J < ↑⊤
exact
  strictMono_of_le_iff_le (fun _ _ => (coeIdeal_le_coeIdeal K).symm)
    (lt_top_iff_ne_top.mpr hJ)