R : Type ?u.1525795
inst✝⁷ : CommRing R
S : Submonoid R
P : Type ?u.1526002
inst✝⁶ : CommRing P
inst✝⁵ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝⁴ : CommRing R₁
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
J : FractionalIdeal R₁⁰ K
d : K
⊢ J / spanSingleton R₁⁰ d = 1 / spanSingleton R₁⁰ d * J
R : Type ?u.1525795
inst✝⁷ : CommRing R
S : Submonoid R
P : Type ?u.1526002
inst✝⁶ : CommRing P
inst✝⁵ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝⁴ : CommRing R₁
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
J : FractionalIdeal R₁⁰ K
d : K
⊢ J / spanSingleton R₁⁰ d = spanSingleton R₁⁰ d⁻¹ * J
rw [← one_div_spanSingleton]
case pos
R : Type ?u.1525795
inst✝⁷ : CommRing R
S : Submonoid R
P : Type ?u.1526002
inst✝⁶ : CommRing P
inst✝⁵ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝⁴ : CommRing R₁
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
J : FractionalIdeal R₁⁰ K
d : K
hd : d = 0
⊢ J / spanSingleton R₁⁰ d = 1 / spanSingleton R₁⁰ d * J

case neg
R : Type ?u.1525795
inst✝⁷ : CommRing R
S : Submonoid R
P : Type ?u.1526002
inst✝⁶ : CommRing P
inst✝⁵ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝⁴ : CommRing R₁
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
J : FractionalIdeal R₁⁰ K
d : K
hd : ¬d = 0
⊢ J / spanSingleton R₁⁰ d = 1 / spanSingleton R₁⁰ d * J
R : Type ?u.1525795
inst✝⁷ : CommRing R
S : Submonoid R
P : Type ?u.1526002
inst✝⁶ : CommRing P
inst✝⁵ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝⁴ : CommRing R₁
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
J : FractionalIdeal R₁⁰ K
d : K
⊢ J / spanSingleton R₁⁰ d = 1 / spanSingleton R₁⁰ d * J
by_cases hd : d = 0
case neg
R : Type ?u.1525795
inst✝⁷ : CommRing R
S : Submonoid R
P : Type ?u.1526002
inst✝⁶ : CommRing P
inst✝⁵ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝⁴ : CommRing R₁
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
J : FractionalIdeal R₁⁰ K
d : K
hd : ¬d = 0
h_spand : spanSingleton R₁⁰ d ≠ 0
⊢ J / spanSingleton R₁⁰ d = 1 / spanSingleton R₁⁰ d * J
case neg
R : Type ?u.1525795
inst✝⁷ : CommRing R
S : Submonoid R
P : Type ?u.1526002
inst✝⁶ : CommRing P
inst✝⁵ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝⁴ : CommRing R₁
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
J : FractionalIdeal R₁⁰ K
d : K
hd : ¬d = 0
⊢ J / spanSingleton R₁⁰ d = 1 / spanSingleton R₁⁰ d * J
have h_spand : spanSingleton R₁⁰ d ≠ 0 := mt spanSingleton_eq_zero_iff.mp hd
case neg.a
R : Type ?u.1525795
inst✝⁷ : CommRing R
S : Submonoid R
P : Type ?u.1526002
inst✝⁶ : CommRing P
inst✝⁵ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝⁴ : CommRing R₁
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
J : FractionalIdeal R₁⁰ K
d : K
hd : ¬d = 0
h_spand : spanSingleton R₁⁰ d ≠ 0
⊢ J / spanSingleton R₁⁰ d ≤ 1 / spanSingleton R₁⁰ d * J

case neg.a
R : Type ?u.1525795
inst✝⁷ : CommRing R
S : Submonoid R
P : Type ?u.1526002
inst✝⁶ : CommRing P
inst✝⁵ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝⁴ : CommRing R₁
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
J : FractionalIdeal R₁⁰ K
d : K
hd : ¬d = 0
h_spand : spanSingleton R₁⁰ d ≠ 0
⊢ 1 / spanSingleton R₁⁰ d * J ≤ J / spanSingleton R₁⁰ d
case neg
R : Type ?u.1525795
inst✝⁷ : CommRing R
S : Submonoid R
P : Type ?u.1526002
inst✝⁶ : CommRing P
inst✝⁵ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝⁴ : CommRing R₁
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
J : FractionalIdeal R₁⁰ K
d : K
hd : ¬d = 0
h_spand : spanSingleton R₁⁰ d ≠ 0
⊢ J / spanSingleton R₁⁰ d = 1 / spanSingleton R₁⁰ d * J
apply le_antisymm
no goals
case pos
R : Type ?u.1525795
inst✝⁷ : CommRing R
S : Submonoid R
P : Type ?u.1526002
inst✝⁶ : CommRing P
inst✝⁵ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝⁴ : CommRing R₁
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
J : FractionalIdeal R₁⁰ K
d : K
hd : d = 0
⊢ J / spanSingleton R₁⁰ d = 1 / spanSingleton R₁⁰ d * J
simp only [hd, spanSingleton_zero, div_zero, MulZeroClass.zero_mul]
case neg.a
R : Type ?u.1525795
inst✝⁷ : CommRing R
S : Submonoid R
P : Type ?u.1526002
inst✝⁶ : CommRing P
inst✝⁵ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝⁴ : CommRing R₁
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
J : FractionalIdeal R₁⁰ K
d : K
hd : ¬d = 0
h_spand : spanSingleton R₁⁰ d ≠ 0
x : K
hx : x ∈ (fun a => ↑a) (J / spanSingleton R₁⁰ d)
⊢ x ∈ (fun a => ↑a) (1 / spanSingleton R₁⁰ d * J)
case neg.a
R : Type ?u.1525795
inst✝⁷ : CommRing R
S : Submonoid R
P : Type ?u.1526002
inst✝⁶ : CommRing P
inst✝⁵ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝⁴ : CommRing R₁
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
J : FractionalIdeal R₁⁰ K
d : K
hd : ¬d = 0
h_spand : spanSingleton R₁⁰ d ≠ 0
⊢ J / spanSingleton R₁⁰ d ≤ 1 / spanSingleton R₁⁰ d * J
intro x hx
case neg.a
R : Type ?u.1525795
inst✝⁷ : CommRing R
S : Submonoid R
P : Type ?u.1526002
inst✝⁶ : CommRing P
inst✝⁵ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝⁴ : CommRing R₁
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
J : FractionalIdeal R₁⁰ K
d : K
hd : ¬d = 0
h_spand : spanSingleton R₁⁰ d ≠ 0
x : K
hx : x ∈ ↑(J / spanSingleton R₁⁰ d)
⊢ x ∈ ↑(1 / spanSingleton R₁⁰ d * J)
case neg.a
R : Type ?u.1525795
inst✝⁷ : CommRing R
S : Submonoid R
P : Type ?u.1526002
inst✝⁶ : CommRing P
inst✝⁵ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝⁴ : CommRing R₁
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
J : FractionalIdeal R₁⁰ K
d : K
hd : ¬d = 0
h_spand : spanSingleton R₁⁰ d ≠ 0
x : K
hx : x ∈ (fun a => ↑a) (J / spanSingleton R₁⁰ d)
⊢ x ∈ (fun a => ↑a) (1 / spanSingleton R₁⁰ d * J)
dsimp only [val_eq_coe] at hx ⊢
case neg.a
R : Type ?u.1525795
inst✝⁷ : CommRing R
S : Submonoid R
P : Type ?u.1526002
inst✝⁶ : CommRing P
inst✝⁵ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝⁴ : CommRing R₁
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
J : FractionalIdeal R₁⁰ K
d : K
hd : ¬d = 0
h_spand : spanSingleton R₁⁰ d ≠ 0
x : K
hx : ∀ (y : K), y ∈ ↑(spanSingleton R₁⁰ d) → x * y ∈ ↑J
⊢ x ∈ ↑(1 / spanSingleton R₁⁰ d * J)
case neg.a
R : Type ?u.1525795
inst✝⁷ : CommRing R
S : Submonoid R
P : Type ?u.1526002
inst✝⁶ : CommRing P
inst✝⁵ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝⁴ : CommRing R₁
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
J : FractionalIdeal R₁⁰ K
d : K
hd : ¬d = 0
h_spand : spanSingleton R₁⁰ d ≠ 0
x : K
hx : x ∈ ↑(J / spanSingleton R₁⁰ d)
⊢ x ∈ ↑(1 / spanSingleton R₁⁰ d * J)
rw [coe_div h_spand, Submodule.mem_div_iff_forall_mul_mem] at hx
case neg.a
R : Type ?u.1525795
inst✝⁷ : CommRing R
S : Submonoid R
P : Type ?u.1526002
inst✝⁶ : CommRing P
inst✝⁵ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝⁴ : CommRing R₁
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
J : FractionalIdeal R₁⁰ K
d : K
hd : ¬d = 0
h_spand : spanSingleton R₁⁰ d ≠ 0
x : K
hx : x * d ∈ ↑J
⊢ x ∈ ↑(1 / spanSingleton R₁⁰ d * J)
case neg.a
R : Type ?u.1525795
inst✝⁷ : CommRing R
S : Submonoid R
P : Type ?u.1526002
inst✝⁶ : CommRing P
inst✝⁵ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝⁴ : CommRing R₁
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
J : FractionalIdeal R₁⁰ K
d : K
hd : ¬d = 0
h_spand : spanSingleton R₁⁰ d ≠ 0
x : K
hx : ∀ (y : K), y ∈ ↑(spanSingleton R₁⁰ d) → x * y ∈ ↑J
⊢ x ∈ ↑(1 / spanSingleton R₁⁰ d * J)
specialize hx d (mem_spanSingleton_self R₁⁰ d)
case neg.a
R : Type ?u.1525795
inst✝⁷ : CommRing R
S : Submonoid R
P : Type ?u.1526002
inst✝⁶ : CommRing P
inst✝⁵ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝⁴ : CommRing R₁
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
J : FractionalIdeal R₁⁰ K
d : K
hd : ¬d = 0
h_spand : spanSingleton R₁⁰ d ≠ 0
x : K
hx : x * d ∈ ↑J
h_xd : x = d⁻¹ * (x * d)
⊢ x ∈ ↑(1 / spanSingleton R₁⁰ d * J)
case neg.a
R : Type ?u.1525795
inst✝⁷ : CommRing R
S : Submonoid R
P : Type ?u.1526002
inst✝⁶ : CommRing P
inst✝⁵ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝⁴ : CommRing R₁
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
J : FractionalIdeal R₁⁰ K
d : K
hd : ¬d = 0
h_spand : spanSingleton R₁⁰ d ≠ 0
x : K
hx : x * d ∈ ↑J
⊢ x ∈ ↑(1 / spanSingleton R₁⁰ d * J)
have h_xd : x = d⁻¹ * (x * d) := by field_simp
case neg.a
R : Type ?u.1525795
inst✝⁷ : CommRing R
S : Submonoid R
P : Type ?u.1526002
inst✝⁶ : CommRing P
inst✝⁵ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝⁴ : CommRing R₁
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
J : FractionalIdeal R₁⁰ K
d : K
hd : ¬d = 0
h_spand : spanSingleton R₁⁰ d ≠ 0
x : K
hx : x * d ∈ ↑J
h_xd : x = d⁻¹ * (x * d)
⊢ d⁻¹ * (x * d) ∈ ↑(spanSingleton R₁⁰ d⁻¹) * ↑J
case neg.a
R : Type ?u.1525795
inst✝⁷ : CommRing R
S : Submonoid R
P : Type ?u.1526002
inst✝⁶ : CommRing P
inst✝⁵ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝⁴ : CommRing R₁
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
J : FractionalIdeal R₁⁰ K
d : K
hd : ¬d = 0
h_spand : spanSingleton R₁⁰ d ≠ 0
x : K
hx : x * d ∈ ↑J
h_xd : x = d⁻¹ * (x * d)
⊢ x ∈ ↑(1 / spanSingleton R₁⁰ d * J)
rw [coe_mul, one_div_spanSingleton, h_xd]
no goals
case neg.a
R : Type ?u.1525795
inst✝⁷ : CommRing R
S : Submonoid R
P : Type ?u.1526002
inst✝⁶ : CommRing P
inst✝⁵ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝⁴ : CommRing R₁
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
J : FractionalIdeal R₁⁰ K
d : K
hd : ¬d = 0
h_spand : spanSingleton R₁⁰ d ≠ 0
x : K
hx : x * d ∈ ↑J
h_xd : x = d⁻¹ * (x * d)
⊢ d⁻¹ * (x * d) ∈ ↑(spanSingleton R₁⁰ d⁻¹) * ↑J
exact Submodule.mul_mem_mul (mem_spanSingleton_self R₁⁰ _) hx
no goals
R : Type ?u.1525795
inst✝⁷ : CommRing R
S : Submonoid R
P : Type ?u.1526002
inst✝⁶ : CommRing P
inst✝⁵ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝⁴ : CommRing R₁
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
J : FractionalIdeal R₁⁰ K
d : K
hd : ¬d = 0
h_spand : spanSingleton R₁⁰ d ≠ 0
x : K
hx : x * d ∈ ↑J
⊢ x = d⁻¹ * (x * d)
field_simp
no goals
case neg.a
R : Type ?u.1525795
inst✝⁷ : CommRing R
S : Submonoid R
P : Type ?u.1526002
inst✝⁶ : CommRing P
inst✝⁵ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝⁴ : CommRing R₁
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
J : FractionalIdeal R₁⁰ K
d : K
hd : ¬d = 0
h_spand : spanSingleton R₁⁰ d ≠ 0
⊢ 1 / spanSingleton R₁⁰ d * J ≤ J / spanSingleton R₁⁰ d
rw [le_div_iff_mul_le h_spand, mul_assoc, mul_left_comm, one_div_spanSingleton,
  spanSingleton_mul_spanSingleton, inv_mul_cancel hd, spanSingleton_one, mul_one]