R : Type u_2
K : Type u_1
L : Type ?u.1775691
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⁰ K)ˣ
⊢ ↑(equiv K) (↑mk I) = ↑(equiv K) 1 ↔ Submodule.IsPrincipal ↑↑I
R : Type u_2
K : Type u_1
L : Type ?u.1775691
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⁰ K)ˣ
⊢ ↑mk I = 1 ↔ Submodule.IsPrincipal ↑↑I
rw [← (ClassGroup.equiv K).injective.eq_iff]
R : Type u_2
K : Type u_1
L : Type ?u.1775691
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⁰ K)ˣ
⊢ (∃ x, spanSingleton R⁰ ↑x = ↑I) ↔ Submodule.IsPrincipal ↑↑I
R : Type u_2
K : Type u_1
L : Type ?u.1775691
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⁰ K)ˣ
⊢ ↑(equiv K) (↑mk I) = ↑(equiv K) 1 ↔ Submodule.IsPrincipal ↑↑I
simp only [equiv_mk, canonicalEquiv_self, RingEquiv.coe_mulEquiv_refl, QuotientGroup.mk'_apply,
  _root_.map_one, QuotientGroup.eq_one_iff, MonoidHom.mem_range, ext_iff, coe_toPrincipalIdeal,
  coe_mapEquiv, MulEquiv.refl_apply]
R : Type u_2
K : Type u_1
L : Type ?u.1775691
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⁰ K)ˣ
⊢ Submodule.IsPrincipal ↑↑I → ∃ x, spanSingleton R⁰ ↑x = ↑I
R : Type u_2
K : Type u_1
L : Type ?u.1775691
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⁰ K)ˣ
⊢ (∃ x, spanSingleton R⁰ ↑x = ↑I) ↔ Submodule.IsPrincipal ↑↑I
refine ⟨fun ⟨x, hx⟩ => ⟨⟨x, by rw [← hx, coe_spanSingleton]⟩⟩, ?_⟩
R : Type u_2
K : Type u_1
L : Type ?u.1775691
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⁰ K)ˣ
hI : Submodule.IsPrincipal ↑↑I
⊢ ∃ x, spanSingleton R⁰ ↑x = ↑I
R : Type u_2
K : Type u_1
L : Type ?u.1775691
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⁰ K)ˣ
⊢ Submodule.IsPrincipal ↑↑I → ∃ x, spanSingleton R⁰ ↑x = ↑I
intro hI
case intro
R : Type u_2
K : Type u_1
L : Type ?u.1775691
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⁰ K)ˣ
hI : Submodule.IsPrincipal ↑↑I
x : K
hx : ↑↑I = Submodule.span R {x}
⊢ ∃ x, spanSingleton R⁰ ↑x = ↑I
R : Type u_2
K : Type u_1
L : Type ?u.1775691
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⁰ K)ˣ
hI : Submodule.IsPrincipal ↑↑I
⊢ ∃ x, spanSingleton R⁰ ↑x = ↑I
obtain ⟨x, hx⟩ := @Submodule.IsPrincipal.principal _ _ _ _ _ _ hI
case intro
R : Type u_2
K : Type u_1
L : Type ?u.1775691
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⁰ K)ˣ
hI : Submodule.IsPrincipal ↑↑I
x : K
hx : ↑↑I = Submodule.span R {x}
hx' : ↑I = spanSingleton R⁰ x
⊢ ∃ x, spanSingleton R⁰ ↑x = ↑I
case intro
R : Type u_2
K : Type u_1
L : Type ?u.1775691
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⁰ K)ˣ
hI : Submodule.IsPrincipal ↑↑I
x : K
hx : ↑↑I = Submodule.span R {x}
⊢ ∃ x, spanSingleton R⁰ ↑x = ↑I
have hx' : (I : FractionalIdeal R⁰ K) = spanSingleton R⁰ x := by
  apply Subtype.coe_injective
  simp only [val_eq_coe, hx, coe_spanSingleton]
case intro.refine_1
R : Type u_2
K : Type u_1
L : Type ?u.1775691
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⁰ K)ˣ
hI : Submodule.IsPrincipal ↑↑I
x : K
hx : ↑↑I = Submodule.span R {x}
hx' : ↑I = spanSingleton R⁰ x
⊢ x ≠ 0

case intro.refine_2
R : Type u_2
K : Type u_1
L : Type ?u.1775691
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⁰ K)ˣ
hI : Submodule.IsPrincipal ↑↑I
x : K
hx : ↑↑I = Submodule.span R {x}
hx' : ↑I = spanSingleton R⁰ x
⊢ spanSingleton R⁰ ↑(Units.mk0 x ?intro.refine_1) = ↑I
case intro
R : Type u_2
K : Type u_1
L : Type ?u.1775691
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⁰ K)ˣ
hI : Submodule.IsPrincipal ↑↑I
x : K
hx : ↑↑I = Submodule.span R {x}
hx' : ↑I = spanSingleton R⁰ x
⊢ ∃ x, spanSingleton R⁰ ↑x = ↑I
refine ⟨Units.mk0 x ?_, ?_⟩
no goals
R : Type u_2
K : Type u_1
L : Type ?u.1775691
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⁰ K)ˣ
x✝ : ∃ x, spanSingleton R⁰ ↑x = ↑I
x : Kˣ
hx : spanSingleton R⁰ ↑x = ↑I
⊢ ↑↑I = Submodule.span R {↑x}
rw [← hx, coe_spanSingleton]
case a
R : Type u_2
K : Type u_1
L : Type ?u.1775691
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⁰ K)ˣ
hI : Submodule.IsPrincipal ↑↑I
x : K
hx : ↑↑I = Submodule.span R {x}
⊢ (fun a => ↑a) ↑I = (fun a => ↑a) (spanSingleton R⁰ x)
R : Type u_2
K : Type u_1
L : Type ?u.1775691
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⁰ K)ˣ
hI : Submodule.IsPrincipal ↑↑I
x : K
hx : ↑↑I = Submodule.span R {x}
⊢ ↑I = spanSingleton R⁰ x
apply Subtype.coe_injective
no goals
case a
R : Type u_2
K : Type u_1
L : Type ?u.1775691
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⁰ K)ˣ
hI : Submodule.IsPrincipal ↑↑I
x : K
hx : ↑↑I = Submodule.span R {x}
⊢ (fun a => ↑a) ↑I = (fun a => ↑a) (spanSingleton R⁰ x)
simp only [val_eq_coe, hx, coe_spanSingleton]
case intro.refine_1
R : Type u_2
K : Type u_1
L : Type ?u.1775691
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⁰ K)ˣ
hI : Submodule.IsPrincipal ↑↑I
x : K
hx : ↑↑I = Submodule.span R {x}
hx' : ↑I = spanSingleton R⁰ x
x_eq : x = 0
⊢ False
case intro.refine_1
R : Type u_2
K : Type u_1
L : Type ?u.1775691
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⁰ K)ˣ
hI : Submodule.IsPrincipal ↑↑I
x : K
hx : ↑↑I = Submodule.span R {x}
hx' : ↑I = spanSingleton R⁰ x
⊢ x ≠ 0
intro x_eq
case intro.refine_1
R : Type u_2
K : Type u_1
L : Type ?u.1775691
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⁰ K)ˣ
hI : Submodule.IsPrincipal ↑↑I
x : K
hx : ↑↑I = Submodule.span R {x}
hx' : ↑I = spanSingleton R⁰ x
x_eq : x = 0
⊢ ↑I = 0
case intro.refine_1
R : Type u_2
K : Type u_1
L : Type ?u.1775691
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⁰ K)ˣ
hI : Submodule.IsPrincipal ↑↑I
x : K
hx : ↑↑I = Submodule.span R {x}
hx' : ↑I = spanSingleton R⁰ x
x_eq : x = 0
⊢ False
apply Units.ne_zero I
no goals
case intro.refine_1
R : Type u_2
K : Type u_1
L : Type ?u.1775691
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⁰ K)ˣ
hI : Submodule.IsPrincipal ↑↑I
x : K
hx : ↑↑I = Submodule.span R {x}
hx' : ↑I = spanSingleton R⁰ x
x_eq : x = 0
⊢ ↑I = 0
simp [hx', x_eq]
no goals
case intro.refine_2
R : Type u_2
K : Type u_1
L : Type ?u.1775691
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⁰ K)ˣ
hI : Submodule.IsPrincipal ↑↑I
x : K
hx : ↑↑I = Submodule.span R {x}
hx' : ↑I = spanSingleton R⁰ x
⊢ spanSingleton R⁰ ↑(Units.mk0 x (_ : x = 0 → False)) = ↑I
simp [hx']