R : Type u_1
K : Type ?u.554196
L : Type ?u.554199
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
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' : Ideal R
hI : ↑I = ↑I'
⊢ (∃ x y, x ≠ 0 ∧ y ≠ 0 ∧ Ideal.span {x} * I' = Ideal.span {y} * ⊤) ↔ ∃ x, x ≠ 0 ∧ I' = Ideal.span {x}

R : Type u_1
K : Type ?u.554196
L : Type ?u.554199
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
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' : Ideal R
hI : ↑I = ↑I'
⊢ ↑1 = ↑⊤
R : Type u_1
K : Type ?u.554196
L : Type ?u.554199
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
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' : Ideal R
hI : ↑I = ↑I'
⊢ ↑mk I = 1 ↔ ∃ x, x ≠ 0 ∧ I' = Ideal.span {x}
rw [← map_one (ClassGroup.mk (R := R) (K := FractionRing R)),
  ClassGroup.mk_eq_mk_of_coe_ideal hI (?_ : _ = ↑(⊤ : Ideal R))]
R : Type u_1
K : Type ?u.554196
L : Type ?u.554199
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
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' : Ideal R
hI : ↑I = ↑I'
⊢ (∃ x y, x ≠ 0 ∧ y ≠ 0 ∧ Ideal.span {x} * I' = Ideal.span {y} * ⊤) ↔ ∃ x, x ≠ 0 ∧ I' = Ideal.span {x}
R : Type u_1
K : Type ?u.554196
L : Type ?u.554199
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
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' : Ideal R
hI : ↑I = ↑I'
⊢ (∃ x y, x ≠ 0 ∧ y ≠ 0 ∧ Ideal.span {x} * I' = Ideal.span {y} * ⊤) ↔ ∃ x, x ≠ 0 ∧ I' = Ideal.span {x}

R : Type u_1
K : Type ?u.554196
L : Type ?u.554199
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
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' : Ideal R
hI : ↑I = ↑I'
⊢ ↑1 = ↑⊤
any_goals rfl
case mp
R : Type u_1
K : Type ?u.554196
L : Type ?u.554199
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
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' : Ideal R
hI : ↑I = ↑I'
⊢ (∃ x y, x ≠ 0 ∧ y ≠ 0 ∧ Ideal.span {x} * I' = Ideal.span {y} * ⊤) → ∃ x, x ≠ 0 ∧ I' = Ideal.span {x}

case mpr
R : Type u_1
K : Type ?u.554196
L : Type ?u.554199
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
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' : Ideal R
hI : ↑I = ↑I'
⊢ (∃ x, x ≠ 0 ∧ I' = Ideal.span {x}) → ∃ x y, x ≠ 0 ∧ y ≠ 0 ∧ Ideal.span {x} * I' = Ideal.span {y} * ⊤
R : Type u_1
K : Type ?u.554196
L : Type ?u.554199
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
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' : Ideal R
hI : ↑I = ↑I'
⊢ (∃ x y, x ≠ 0 ∧ y ≠ 0 ∧ Ideal.span {x} * I' = Ideal.span {y} * ⊤) ↔ ∃ x, x ≠ 0 ∧ I' = Ideal.span {x}
constructor
no goals
R : Type u_1
K : Type ?u.554196
L : Type ?u.554199
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
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' : Ideal R
hI : ↑I = ↑I'
⊢ ↑1 = ↑⊤
rfl
case mp.intro.intro.intro.intro
R : Type u_1
K : Type ?u.554196
L : Type ?u.554199
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
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' : Ideal R
hI : ↑I = ↑I'
x y : R
hx : x ≠ 0
hy : y ≠ 0
h : Ideal.span {x} * I' = Ideal.span {y} * ⊤
⊢ ∃ x, x ≠ 0 ∧ I' = Ideal.span {x}
case mp
R : Type u_1
K : Type ?u.554196
L : Type ?u.554199
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
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' : Ideal R
hI : ↑I = ↑I'
⊢ (∃ x y, x ≠ 0 ∧ y ≠ 0 ∧ Ideal.span {x} * I' = Ideal.span {y} * ⊤) → ∃ x, x ≠ 0 ∧ I' = Ideal.span {x}
rintro ⟨x, y, hx, hy, h⟩
case mp.intro.intro.intro.intro
R : Type u_1
K : Type ?u.554196
L : Type ?u.554199
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
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' : Ideal R
hI : ↑I = ↑I'
x y : R
hx : x ≠ 0
hy : y ≠ 0
h : Ideal.span {x} * I' = Ideal.span {y}
⊢ ∃ x, x ≠ 0 ∧ I' = Ideal.span {x}
case mp.intro.intro.intro.intro
R : Type u_1
K : Type ?u.554196
L : Type ?u.554199
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
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' : Ideal R
hI : ↑I = ↑I'
x y : R
hx : x ≠ 0
hy : y ≠ 0
h : Ideal.span {x} * I' = Ideal.span {y} * ⊤
⊢ ∃ x, x ≠ 0 ∧ I' = Ideal.span {x}
rw [Ideal.mul_top] at h
case mp.intro.intro.intro.intro.intro.intro
R : Type u_1
K : Type ?u.554196
L : Type ?u.554199
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
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' : Ideal R
hI : ↑I = ↑I'
x : R
hx : x ≠ 0
i : R
_hi : i ∈ I'
hy : x * i ≠ 0
h : Ideal.span {x} * I' = Ideal.span {x * i}
⊢ ∃ x, x ≠ 0 ∧ I' = Ideal.span {x}
case mp.intro.intro.intro.intro
R : Type u_1
K : Type ?u.554196
L : Type ?u.554199
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
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' : Ideal R
hI : ↑I = ↑I'
x y : R
hx : x ≠ 0
hy : y ≠ 0
h : Ideal.span {x} * I' = Ideal.span {y}
⊢ ∃ x, x ≠ 0 ∧ I' = Ideal.span {x}
rcases Ideal.mem_span_singleton_mul.mp ((Ideal.span_singleton_le_iff_mem _).mp h.ge) with
  ⟨i, _hi, rfl⟩
case mp.intro.intro.intro.intro.intro.intro
R : Type u_1
K : Type ?u.554196
L : Type ?u.554199
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
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' : Ideal R
hI : ↑I = ↑I'
x : R
hx : x ≠ 0
i : R
_hi : i ∈ I'
hy : x * i ≠ 0
h : I' = Ideal.span {i}
⊢ ∃ x, x ≠ 0 ∧ I' = Ideal.span {x}
case mp.intro.intro.intro.intro.intro.intro
R : Type u_1
K : Type ?u.554196
L : Type ?u.554199
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
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' : Ideal R
hI : ↑I = ↑I'
x : R
hx : x ≠ 0
i : R
_hi : i ∈ I'
hy : x * i ≠ 0
h : Ideal.span {x} * I' = Ideal.span {x * i}
⊢ ∃ x, x ≠ 0 ∧ I' = Ideal.span {x}
rw [← Ideal.span_singleton_mul_span_singleton, Ideal.span_singleton_mul_right_inj hx] at h
no goals
case mp.intro.intro.intro.intro.intro.intro
R : Type u_1
K : Type ?u.554196
L : Type ?u.554199
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
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' : Ideal R
hI : ↑I = ↑I'
x : R
hx : x ≠ 0
i : R
_hi : i ∈ I'
hy : x * i ≠ 0
h : I' = Ideal.span {i}
⊢ ∃ x, x ≠ 0 ∧ I' = Ideal.span {x}
exact ⟨i, right_ne_zero_of_mul hy, h⟩
case mpr.intro.intro
R : Type u_1
K : Type ?u.554196
L : Type ?u.554199
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
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
x : R
hx : x ≠ 0
hI : ↑I = ↑(Ideal.span {x})
⊢ ∃ x_1 y, x_1 ≠ 0 ∧ y ≠ 0 ∧ Ideal.span {x_1} * Ideal.span {x} = Ideal.span {y} * ⊤
case mpr
R : Type u_1
K : Type ?u.554196
L : Type ?u.554199
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
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' : Ideal R
hI : ↑I = ↑I'
⊢ (∃ x, x ≠ 0 ∧ I' = Ideal.span {x}) → ∃ x y, x ≠ 0 ∧ y ≠ 0 ∧ Ideal.span {x} * I' = Ideal.span {y} * ⊤
rintro ⟨x, hx, rfl⟩
no goals
case mpr.intro.intro
R : Type u_1
K : Type ?u.554196
L : Type ?u.554199
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
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
x : R
hx : x ≠ 0
hI : ↑I = ↑(Ideal.span {x})
⊢ ∃ x_1 y, x_1 ≠ 0 ∧ y ≠ 0 ∧ Ideal.span {x_1} * Ideal.span {x} = Ideal.span {y} * ⊤
exact ⟨1, x, one_ne_zero, hx, by rw [Ideal.span_singleton_one, Ideal.top_mul, Ideal.mul_top]⟩
no goals
R : Type u_1
K : Type ?u.554196
L : Type ?u.554199
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
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
x : R
hx : x ≠ 0
hI : ↑I = ↑(Ideal.span {x})
⊢ Ideal.span {1} * Ideal.span {x} = Ideal.span {x} * ⊤
rw [Ideal.span_singleton_one, Ideal.top_mul, Ideal.mul_top]