-- Mathlib/RingTheory/ClassGroup.lean
theorem ClassGroup.mk_eq_one_iff {I : (FractionalIdeal R⁰ K)ˣ} :
    ClassGroup.mk I = 1 ↔ (I : Submodule R K).IsPrincipal

Proof state:
case intro.refine_1
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ K)ˣ
hI : (↑↑I).IsPrincipal
x : K
hx : ↑↑I = Submodule.span R {x}
hx' : ↑I = spanSingleton R⁰ x
⊢ x ≠ 0

Tactic:
intro x_eq

Result:
case intro.refine_1
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ K)ˣ
hI : (↑↑I).IsPrincipal
x : K
hx : ↑↑I = Submodule.span R {x}
hx' : ↑I = spanSingleton R⁰ x
x_eq : x = 0
⊢ False

Proof state:
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ K)ˣ
⊢ (equiv K) (mk I) = (equiv K) 1 ↔ (↑↑I).IsPrincipal

Tactic:
simp only [equiv_mk, canonicalEquiv_self, RingEquiv.coe_mulEquiv_refl, QuotientGroup.mk'_apply,
  _root_.map_one, QuotientGroup.eq_one_iff, MonoidHom.mem_range, Units.ext_iff,
  coe_toPrincipalIdeal, coe_mapEquiv, MulEquiv.refl_apply]

Result:
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ K)ˣ
⊢ (∃ x, spanSingleton R⁰ ↑x = ↑I) ↔ (↑↑I).IsPrincipal

Proof state:
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
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}

Tactic:
rw [← hx, coe_spanSingleton]

Result:
no goals

Proof state:
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ K)ˣ
⊢ (↑↑I).IsPrincipal → ∃ x, spanSingleton R⁰ ↑x = ↑I

Tactic:
intro hI

Result:
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ K)ˣ
hI : (↑↑I).IsPrincipal
⊢ ∃ x, spanSingleton R⁰ ↑x = ↑I

Proof state:
case intro.refine_1
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ K)ˣ
hI : (↑↑I).IsPrincipal
x : K
hx : ↑↑I = Submodule.span R {x}
hx' : ↑I = spanSingleton R⁰ x
x_eq : x = 0
⊢ ↑I = 0

Tactic:
simp [hx', x_eq]

Result:
no goals

Proof state:
case intro
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ K)ˣ
hI : (↑↑I).IsPrincipal
x : K
hx : ↑↑I = Submodule.span R {x}
⊢ ∃ x, spanSingleton R⁰ ↑x = ↑I

Tactic:
have hx' : (I : FractionalIdeal R⁰ K) = spanSingleton R⁰ x := by
  apply Subtype.coe_injective
  simp only [val_eq_coe, hx, coe_spanSingleton]

Result:
case intro
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ K)ˣ
hI : (↑↑I).IsPrincipal
x : K
hx : ↑↑I = Submodule.span R {x}
hx' : ↑I = spanSingleton R⁰ x
⊢ ∃ x, spanSingleton R⁰ ↑x = ↑I

Proof state:
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ K)ˣ
hI : (↑↑I).IsPrincipal
x : K
hx : ↑↑I = Submodule.span R {x}
⊢ ↑I = spanSingleton R⁰ x

Tactic:
apply Subtype.coe_injective

Result:
case a
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ K)ˣ
hI : (↑↑I).IsPrincipal
x : K
hx : ↑↑I = Submodule.span R {x}
⊢ (fun a => ↑a) ↑I = (fun a => ↑a) (spanSingleton R⁰ x)

Proof state:
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ K)ˣ
hI : (↑↑I).IsPrincipal
⊢ ∃ x, spanSingleton R⁰ ↑x = ↑I

Tactic:
obtain ⟨x, hx⟩ := @Submodule.IsPrincipal.principal _ _ _ _ _ _ hI

Result:
case intro
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ K)ˣ
hI : (↑↑I).IsPrincipal
x : K
hx : ↑↑I = Submodule.span R {x}
⊢ ∃ x, spanSingleton R⁰ ↑x = ↑I

Proof state:
case intro.refine_2
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ K)ˣ
hI : (↑↑I).IsPrincipal
x : K
hx : ↑↑I = Submodule.span R {x}
hx' : ↑I = spanSingleton R⁰ x
⊢ spanSingleton R⁰ ↑(Units.mk0 x ⋯) = ↑I

Tactic:
simp [hx']

Result:
no goals

Proof state:
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ K)ˣ
⊢ mk I = 1 ↔ (↑↑I).IsPrincipal

Tactic:
rw [← (ClassGroup.equiv K).injective.eq_iff]

Result:
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ K)ˣ
⊢ (equiv K) (mk I) = (equiv K) 1 ↔ (↑↑I).IsPrincipal

Proof state:
case a
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ K)ˣ
hI : (↑↑I).IsPrincipal
x : K
hx : ↑↑I = Submodule.span R {x}
⊢ (fun a => ↑a) ↑I = (fun a => ↑a) (spanSingleton R⁰ x)

Tactic:
simp only [val_eq_coe, hx, coe_spanSingleton]

Result:
no goals

Proof state:
case intro
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ K)ˣ
hI : (↑↑I).IsPrincipal
x : K
hx : ↑↑I = Submodule.span R {x}
hx' : ↑I = spanSingleton R⁰ x
⊢ ∃ x, spanSingleton R⁰ ↑x = ↑I

Tactic:
refine ⟨Units.mk0 x ?_, ?_⟩

Result:
case intro.refine_1
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ K)ˣ
hI : (↑↑I).IsPrincipal
x : K
hx : ↑↑I = Submodule.span R {x}
hx' : ↑I = spanSingleton R⁰ x
⊢ x ≠ 0

case intro.refine_2
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ K)ˣ
hI : (↑↑I).IsPrincipal
x : K
hx : ↑↑I = Submodule.span R {x}
hx' : ↑I = spanSingleton R⁰ x
⊢ spanSingleton R⁰ ↑(Units.mk0 x ?intro.refine_1) = ↑I

Proof state:
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ K)ˣ
⊢ (∃ x, spanSingleton R⁰ ↑x = ↑I) ↔ (↑↑I).IsPrincipal

Tactic:
refine ⟨fun ⟨x, hx⟩ => ⟨⟨x, by rw [← hx, coe_spanSingleton]⟩⟩, ?_⟩

Result:
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ K)ˣ
⊢ (↑↑I).IsPrincipal → ∃ x, spanSingleton R⁰ ↑x = ↑I

Proof state:
case intro.refine_1
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ K)ˣ
hI : (↑↑I).IsPrincipal
x : K
hx : ↑↑I = Submodule.span R {x}
hx' : ↑I = spanSingleton R⁰ x
x_eq : x = 0
⊢ False

Tactic:
apply Units.ne_zero I

Result:
case intro.refine_1
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ K)ˣ
hI : (↑↑I).IsPrincipal
x : K
hx : ↑↑I = Submodule.span R {x}
hx' : ↑I = spanSingleton R⁰ x
x_eq : x = 0
⊢ ↑I = 0