R : Type u_1
K : Type u_2
L : Type ?u.1378419
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)⁰ }
⊢ ↑(equiv K) (↑mk0 I) = ↑(equiv K) (↑mk0 J) ↔ ∃ x x_1, spanSingleton R⁰ x * ↑↑I = ↑↑J
R : Type u_1
K : Type u_2
L : Type ?u.1378419
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 x_1, spanSingleton R⁰ x * ↑↑I = ↑↑J
refine (ClassGroup.equiv K).injective.eq_iff.symm.trans ?_
R : Type u_1
K : Type u_2
L : Type ?u.1378419
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, (∃ x, spanSingleton R⁰ x = ↑z) ∧ ↑↑I * ↑z = ↑↑J) ↔ ∃ x, x ≠ 0 ∧ spanSingleton R⁰ x * ↑↑I = ↑↑J
R : Type u_1
K : Type u_2
L : Type ?u.1378419
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)⁰ }
⊢ ↑(equiv K) (↑mk0 I) = ↑(equiv K) (↑mk0 J) ↔ ∃ x x_1, spanSingleton R⁰ x * ↑↑I = ↑↑J
simp only [ClassGroup.equiv_mk0, QuotientGroup.mk'_eq_mk', mem_principal_ideals_iff,
  Units.ext_iff, Units.val_mul, FractionalIdeal.coe_mk0, exists_prop]
case mp
R : Type u_1
K : Type u_2
L : Type ?u.1378419
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, (∃ x, spanSingleton R⁰ x = ↑z) ∧ ↑↑I * ↑z = ↑↑J) → ∃ x, x ≠ 0 ∧ spanSingleton R⁰ x * ↑↑I = ↑↑J

case mpr
R : Type u_1
K : Type u_2
L : Type ?u.1378419
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 ≠ 0 ∧ spanSingleton R⁰ x * ↑↑I = ↑↑J) → ∃ z, (∃ x, spanSingleton R⁰ x = ↑z) ∧ ↑↑I * ↑z = ↑↑J
R : Type u_1
K : Type u_2
L : Type ?u.1378419
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, (∃ x, spanSingleton R⁰ x = ↑z) ∧ ↑↑I * ↑z = ↑↑J) ↔ ∃ x, x ≠ 0 ∧ spanSingleton R⁰ x * ↑↑I = ↑↑J
constructor
case mp.intro.intro.intro
R : Type u_1
K : Type u_2
L : Type ?u.1378419
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 : (FractionalIdeal R⁰ K)ˣ
hx : ↑↑I * ↑X = ↑↑J
x : K
hX : spanSingleton R⁰ x = ↑X
⊢ ∃ x, x ≠ 0 ∧ spanSingleton R⁰ x * ↑↑I = ↑↑J
case mp
R : Type u_1
K : Type u_2
L : Type ?u.1378419
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, (∃ x, spanSingleton R⁰ x = ↑z) ∧ ↑↑I * ↑z = ↑↑J) → ∃ x, x ≠ 0 ∧ spanSingleton R⁰ x * ↑↑I = ↑↑J
rintro ⟨X, ⟨x, hX⟩, hx⟩
case mp.intro.intro.intro.refine_1
R : Type u_1
K : Type u_2
L : Type ?u.1378419
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 : (FractionalIdeal R⁰ K)ˣ
hx : ↑↑I * ↑X = ↑↑J
x : K
hX : spanSingleton R⁰ x = ↑X
⊢ x ≠ 0

case mp.intro.intro.intro.refine_2
R : Type u_1
K : Type u_2
L : Type ?u.1378419
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 : (FractionalIdeal R⁰ K)ˣ
hx : ↑↑I * ↑X = ↑↑J
x : K
hX : spanSingleton R⁰ x = ↑X
⊢ spanSingleton R⁰ x * ↑↑I = ↑↑J
case mp.intro.intro.intro
R : Type u_1
K : Type u_2
L : Type ?u.1378419
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 : (FractionalIdeal R⁰ K)ˣ
hx : ↑↑I * ↑X = ↑↑J
x : K
hX : spanSingleton R⁰ x = ↑X
⊢ ∃ x, x ≠ 0 ∧ spanSingleton R⁰ x * ↑↑I = ↑↑J
refine ⟨x, ?_, ?_⟩
no goals
case mp.intro.intro.intro.refine_2
R : Type u_1
K : Type u_2
L : Type ?u.1378419
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 : (FractionalIdeal R⁰ K)ˣ
hx : ↑↑I * ↑X = ↑↑J
x : K
hX : spanSingleton R⁰ x = ↑X
⊢ spanSingleton R⁰ x * ↑↑I = ↑↑J
simpa only [hX, mul_comm] using hx
case mp.intro.intro.intro.refine_1
R : Type u_1
K : Type u_2
L : Type ?u.1378419
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 : (FractionalIdeal R⁰ K)ˣ
hx : ↑↑I * ↑X = ↑↑J
hX : spanSingleton R⁰ 0 = ↑X
⊢ False
case mp.intro.intro.intro.refine_1
R : Type u_1
K : Type u_2
L : Type ?u.1378419
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 : (FractionalIdeal R⁰ K)ˣ
hx : ↑↑I * ↑X = ↑↑J
x : K
hX : spanSingleton R⁰ x = ↑X
⊢ x ≠ 0
rintro rfl
no goals
case mp.intro.intro.intro.refine_1
R : Type u_1
K : Type u_2
L : Type ?u.1378419
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 : (FractionalIdeal R⁰ K)ˣ
hx : ↑↑I * ↑X = ↑↑J
hX : spanSingleton R⁰ 0 = ↑X
⊢ False
simp [X.ne_zero.symm] at hX
case mpr.intro.intro
R : Type u_1
K : Type u_2
L : Type ?u.1378419
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 : K
hx : x ≠ 0
eq_J : spanSingleton R⁰ x * ↑↑I = ↑↑J
⊢ ∃ z, (∃ x, spanSingleton R⁰ x = ↑z) ∧ ↑↑I * ↑z = ↑↑J
case mpr
R : Type u_1
K : Type u_2
L : Type ?u.1378419
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 ≠ 0 ∧ spanSingleton R⁰ x * ↑↑I = ↑↑J) → ∃ z, (∃ x, spanSingleton R⁰ x = ↑z) ∧ ↑↑I * ↑z = ↑↑J
rintro ⟨x, hx, eq_J⟩
case mpr.intro.intro
R : Type u_1
K : Type u_2
L : Type ?u.1378419
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 : K
hx : x ≠ 0
eq_J : spanSingleton R⁰ x * ↑↑I = ↑↑J
⊢ ↑↑I * ↑(Units.mk0 (spanSingleton R⁰ x) (_ : spanSingleton R⁰ x ≠ 0)) = ↑↑J
case mpr.intro.intro
R : Type u_1
K : Type u_2
L : Type ?u.1378419
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 : K
hx : x ≠ 0
eq_J : spanSingleton R⁰ x * ↑↑I = ↑↑J
⊢ ∃ z, (∃ x, spanSingleton R⁰ x = ↑z) ∧ ↑↑I * ↑z = ↑↑J
refine ⟨Units.mk0 _ (spanSingleton_ne_zero_iff.mpr hx), ⟨x, rfl⟩, ?_⟩
no goals
case mpr.intro.intro
R : Type u_1
K : Type u_2
L : Type ?u.1378419
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 : K
hx : x ≠ 0
eq_J : spanSingleton R⁰ x * ↑↑I = ↑↑J
⊢ ↑↑I * ↑(Units.mk0 (spanSingleton R⁰ x) (_ : spanSingleton R⁰ x ≠ 0)) = ↑↑J
simpa only [mul_comm] using eq_J