case refine_1
R : Type u_1
K : Type ?u.1434681
L : Type ?u.1434684
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : { x // x ∈ (Ideal R)⁰ }
⊢ (∃ x x_1, spanSingleton R⁰ x * ↑↑I = ↑↑J) → ∃ x y _hx _hy, Ideal.span {x} * ↑I = Ideal.span {y} * ↑J

case refine_2
R : Type u_1
K : Type ?u.1434681
L : Type ?u.1434684
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : { x // x ∈ (Ideal R)⁰ }
⊢ (∃ x y _hx _hy, Ideal.span {x} * ↑I = Ideal.span {y} * ↑J) → ∃ x x_1, spanSingleton R⁰ x * ↑↑I = ↑↑J
R : Type u_1
K : Type ?u.1434681
L : Type ?u.1434684
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : { x // x ∈ (Ideal R)⁰ }
⊢ ↑mk0 I = ↑mk0 J ↔ ∃ x y _hx _hy, Ideal.span {x} * ↑I = Ideal.span {y} * ↑J
refine (ClassGroup.mk0_eq_mk0_iff_exists_fraction_ring (FractionRing R)).trans ⟨?_, ?_⟩
case refine_1.intro.intro
R : Type u_1
K : Type ?u.1434681
L : Type ?u.1434684
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : { x // x ∈ (Ideal R)⁰ }
z : FractionRing R
hz : z ≠ 0
h : spanSingleton R⁰ z * ↑↑I = ↑↑J
⊢ ∃ x y _hx _hy, Ideal.span {x} * ↑I = Ideal.span {y} * ↑J
case refine_1
R : Type u_1
K : Type ?u.1434681
L : Type ?u.1434684
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : { x // x ∈ (Ideal R)⁰ }
⊢ (∃ x x_1, spanSingleton R⁰ x * ↑↑I = ↑↑J) → ∃ x y _hx _hy, Ideal.span {x} * ↑I = Ideal.span {y} * ↑J
rintro ⟨z, hz, h⟩
case refine_1.intro.intro.intro.intro.mk
R : Type u_1
K : Type ?u.1434681
L : Type ?u.1434684
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : { x // x ∈ (Ideal R)⁰ }
x y : R
hy : y ∈ R⁰
hz : mk' (FractionRing R) x { val := y, property := hy } ≠ 0
h : spanSingleton R⁰ (mk' (FractionRing R) x { val := y, property := hy }) * ↑↑I = ↑↑J
⊢ ∃ x y _hx _hy, Ideal.span {x} * ↑I = Ideal.span {y} * ↑J
case refine_1.intro.intro
R : Type u_1
K : Type ?u.1434681
L : Type ?u.1434684
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : { x // x ∈ (Ideal R)⁰ }
z : FractionRing R
hz : z ≠ 0
h : spanSingleton R⁰ z * ↑↑I = ↑↑J
⊢ ∃ x y _hx _hy, Ideal.span {x} * ↑I = Ideal.span {y} * ↑J
obtain ⟨x, ⟨y, hy⟩, rfl⟩ := IsLocalization.mk'_surjective R⁰ z
case refine_1.intro.intro.intro.intro.mk.refine_1
R : Type u_1
K : Type ?u.1434681
L : Type ?u.1434684
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : { x // x ∈ (Ideal R)⁰ }
x y : R
hy : y ∈ R⁰
hz : mk' (FractionRing R) x { val := y, property := hy } ≠ 0
h : spanSingleton R⁰ (mk' (FractionRing R) x { val := y, property := hy }) * ↑↑I = ↑↑J
⊢ x ≠ 0

case refine_1.intro.intro.intro.intro.mk.refine_2
R : Type u_1
K : Type ?u.1434681
L : Type ?u.1434684
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : { x // x ∈ (Ideal R)⁰ }
x y : R
hy : y ∈ R⁰
hz : mk' (FractionRing R) x { val := y, property := hy } ≠ 0
h : spanSingleton R⁰ (mk' (FractionRing R) x { val := y, property := hy }) * ↑↑I = ↑↑J
⊢ Ideal.span {x} * ↑I = Ideal.span {y} * ↑J
case refine_1.intro.intro.intro.intro.mk
R : Type u_1
K : Type ?u.1434681
L : Type ?u.1434684
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : { x // x ∈ (Ideal R)⁰ }
x y : R
hy : y ∈ R⁰
hz : mk' (FractionRing R) x { val := y, property := hy } ≠ 0
h : spanSingleton R⁰ (mk' (FractionRing R) x { val := y, property := hy }) * ↑↑I = ↑↑J
⊢ ∃ x y _hx _hy, Ideal.span {x} * ↑I = Ideal.span {y} * ↑J
refine ⟨x, y, ?_, mem_nonZeroDivisors_iff_ne_zero.mp hy, ?_⟩
case refine_1.intro.intro.intro.intro.mk.refine_1
R : Type u_1
K : Type ?u.1434681
L : Type ?u.1434684
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : { x // x ∈ (Ideal R)⁰ }
x y : R
hy : y ∈ R⁰
hz : mk' (FractionRing R) x { val := y, property := hy } ≠ 0
h : spanSingleton R⁰ (mk' (FractionRing R) x { val := y, property := hy }) * ↑↑I = ↑↑J
hx : x = 0
⊢ False
case refine_1.intro.intro.intro.intro.mk.refine_1
R : Type u_1
K : Type ?u.1434681
L : Type ?u.1434684
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : { x // x ∈ (Ideal R)⁰ }
x y : R
hy : y ∈ R⁰
hz : mk' (FractionRing R) x { val := y, property := hy } ≠ 0
h : spanSingleton R⁰ (mk' (FractionRing R) x { val := y, property := hy }) * ↑↑I = ↑↑J
⊢ x ≠ 0
rintro hx
case refine_1.intro.intro.intro.intro.mk.refine_1
R : Type u_1
K : Type ?u.1434681
L : Type ?u.1434684
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : { x // x ∈ (Ideal R)⁰ }
x y : R
hy : y ∈ R⁰
hz : mk' (FractionRing R) x { val := y, property := hy } ≠ 0
h : spanSingleton R⁰ (mk' (FractionRing R) x { val := y, property := hy }) * ↑↑I = ↑↑J
hx : x = 0
⊢ mk' (FractionRing R) x { val := y, property := hy } = 0
case refine_1.intro.intro.intro.intro.mk.refine_1
R : Type u_1
K : Type ?u.1434681
L : Type ?u.1434684
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : { x // x ∈ (Ideal R)⁰ }
x y : R
hy : y ∈ R⁰
hz : mk' (FractionRing R) x { val := y, property := hy } ≠ 0
h : spanSingleton R⁰ (mk' (FractionRing R) x { val := y, property := hy }) * ↑↑I = ↑↑J
hx : x = 0
⊢ False
apply hz
no goals
case refine_1.intro.intro.intro.intro.mk.refine_1
R : Type u_1
K : Type ?u.1434681
L : Type ?u.1434684
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : { x // x ∈ (Ideal R)⁰ }
x y : R
hy : y ∈ R⁰
hz : mk' (FractionRing R) x { val := y, property := hy } ≠ 0
h : spanSingleton R⁰ (mk' (FractionRing R) x { val := y, property := hy }) * ↑↑I = ↑↑J
hx : x = 0
⊢ mk' (FractionRing R) x { val := y, property := hy } = 0
rw [hx, IsFractionRing.mk'_eq_div, _root_.map_zero, zero_div]
no goals
case refine_1.intro.intro.intro.intro.mk.refine_2
R : Type u_1
K : Type ?u.1434681
L : Type ?u.1434684
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : { x // x ∈ (Ideal R)⁰ }
x y : R
hy : y ∈ R⁰
hz : mk' (FractionRing R) x { val := y, property := hy } ≠ 0
h : spanSingleton R⁰ (mk' (FractionRing R) x { val := y, property := hy }) * ↑↑I = ↑↑J
⊢ Ideal.span {x} * ↑I = Ideal.span {y} * ↑J
exact (FractionalIdeal.mk'_mul_coeIdeal_eq_coeIdeal _ hy).mp h
case refine_2.intro.intro.intro.intro
R : Type u_1
K : Type ?u.1434681
L : Type ?u.1434684
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : { x // x ∈ (Ideal R)⁰ }
x y : R
hx : x ≠ 0
hy : y ≠ 0
h : Ideal.span {x} * ↑I = Ideal.span {y} * ↑J
⊢ ∃ x x_1, spanSingleton R⁰ x * ↑↑I = ↑↑J
case refine_2
R : Type u_1
K : Type ?u.1434681
L : Type ?u.1434684
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : { x // x ∈ (Ideal R)⁰ }
⊢ (∃ x y _hx _hy, Ideal.span {x} * ↑I = Ideal.span {y} * ↑J) → ∃ x x_1, spanSingleton R⁰ x * ↑↑I = ↑↑J
rintro ⟨x, y, hx, hy, h⟩
case refine_2.intro.intro.intro.intro
R : Type u_1
K : Type ?u.1434681
L : Type ?u.1434684
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : { x // x ∈ (Ideal R)⁰ }
x y : R
hx : x ≠ 0
hy : y ≠ 0
h : Ideal.span {x} * ↑I = Ideal.span {y} * ↑J
hy' : y ∈ R⁰
⊢ ∃ x x_1, spanSingleton R⁰ x * ↑↑I = ↑↑J
case refine_2.intro.intro.intro.intro
R : Type u_1
K : Type ?u.1434681
L : Type ?u.1434684
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : { x // x ∈ (Ideal R)⁰ }
x y : R
hx : x ≠ 0
hy : y ≠ 0
h : Ideal.span {x} * ↑I = Ideal.span {y} * ↑J
⊢ ∃ x x_1, spanSingleton R⁰ x * ↑↑I = ↑↑J
have hy' : y ∈ R⁰ := mem_nonZeroDivisors_iff_ne_zero.mpr hy
case refine_2.intro.intro.intro.intro.refine_1
R : Type u_1
K : Type ?u.1434681
L : Type ?u.1434684
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : { x // x ∈ (Ideal R)⁰ }
x y : R
hx : x ≠ 0
hy : y ≠ 0
h : Ideal.span {x} * ↑I = Ideal.span {y} * ↑J
hy' : y ∈ R⁰
⊢ mk' (FractionRing R) x { val := y, property := hy' } ≠ 0

case refine_2.intro.intro.intro.intro.refine_2
R : Type u_1
K : Type ?u.1434681
L : Type ?u.1434684
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : { x // x ∈ (Ideal R)⁰ }
x y : R
hx : x ≠ 0
hy : y ≠ 0
h : Ideal.span {x} * ↑I = Ideal.span {y} * ↑J
hy' : y ∈ R⁰
⊢ spanSingleton R⁰ (mk' (FractionRing R) x { val := y, property := hy' }) * ↑↑I = ↑↑J
case refine_2.intro.intro.intro.intro
R : Type u_1
K : Type ?u.1434681
L : Type ?u.1434684
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : { x // x ∈ (Ideal R)⁰ }
x y : R
hx : x ≠ 0
hy : y ≠ 0
h : Ideal.span {x} * ↑I = Ideal.span {y} * ↑J
hy' : y ∈ R⁰
⊢ ∃ x x_1, spanSingleton R⁰ x * ↑↑I = ↑↑J
refine ⟨IsLocalization.mk' _ x ⟨y, hy'⟩, ?_, ?_⟩
case refine_2.intro.intro.intro.intro.refine_1
R : Type u_1
K : Type ?u.1434681
L : Type ?u.1434684
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : { x // x ∈ (Ideal R)⁰ }
x y : R
hy : y ≠ 0
h : Ideal.span {x} * ↑I = Ideal.span {y} * ↑J
hy' : y ∈ R⁰
hx : mk' (FractionRing R) x { val := y, property := hy' } = 0
⊢ x = 0
case refine_2.intro.intro.intro.intro.refine_1
R : Type u_1
K : Type ?u.1434681
L : Type ?u.1434684
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : { x // x ∈ (Ideal R)⁰ }
x y : R
hx : x ≠ 0
hy : y ≠ 0
h : Ideal.span {x} * ↑I = Ideal.span {y} * ↑J
hy' : y ∈ R⁰
⊢ mk' (FractionRing R) x { val := y, property := hy' } ≠ 0
contrapose! hx
no goals
case refine_2.intro.intro.intro.intro.refine_1
R : Type u_1
K : Type ?u.1434681
L : Type ?u.1434684
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : { x // x ∈ (Ideal R)⁰ }
x y : R
hy : y ≠ 0
h : Ideal.span {x} * ↑I = Ideal.span {y} * ↑J
hy' : y ∈ R⁰
hx : mk' (FractionRing R) x { val := y, property := hy' } = 0
⊢ x = 0
rwa [mk'_eq_iff_eq_mul, MulZeroClass.zero_mul, ← (algebraMap R (FractionRing R)).map_zero,
  (IsFractionRing.injective R (FractionRing R)).eq_iff] at hx
no goals
case refine_2.intro.intro.intro.intro.refine_2
R : Type u_1
K : Type ?u.1434681
L : Type ?u.1434684
inst✝¹¹ : CommRing R
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : DecidableEq L
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : Algebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : { x // x ∈ (Ideal R)⁰ }
x y : R
hx : x ≠ 0
hy : y ≠ 0
h : Ideal.span {x} * ↑I = Ideal.span {y} * ↑J
hy' : y ∈ R⁰
⊢ spanSingleton R⁰ (mk' (FractionRing R) x { val := y, property := hy' }) * ↑↑I = ↑↑J
exact (FractionalIdeal.mk'_mul_coeIdeal_eq_coeIdeal _ hy').mpr h