-- Mathlib/RingTheory/ClassGroup.lean
theorem ClassGroup.mk_eq_one_of_coe_ideal {I : (FractionalIdeal R⁰ <| FractionRing R)ˣ}
    {I' : Ideal R} (hI : (I : FractionalIdeal R⁰ <| FractionRing R) = I') :
    ClassGroup.mk I = 1 ↔ ∃ x : R, x ≠ 0 ∧ I' = Ideal.span {x}

Proof state:
R : Type u_1
inst✝¹ : CommRing R
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}

Tactic:
constructor

Result:
case mp
R : Type u_1
inst✝¹ : CommRing R
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
inst✝¹ : CommRing R
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} * ⊤

Proof state:
case mp.intro.intro.intro.intro.intro.intro
R : Type u_1
inst✝¹ : CommRing R
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}

Tactic:
rw [← Ideal.span_singleton_mul_span_singleton, Ideal.span_singleton_mul_right_inj hx] at h

Result:
case mp.intro.intro.intro.intro.intro.intro
R : Type u_1
inst✝¹ : CommRing R
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}

Proof state:
R : Type u_1
inst✝¹ : CommRing R
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} * ?m.66692) ↔ ∃ x, x ≠ 0 ∧ I' = Ideal.span {x}

R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' : Ideal R
hI : ↑I = ↑I'
⊢ ↑1 = ↑?m.66692

R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' : Ideal R
hI : ↑I = ↑I'
⊢ Ideal R

Tactic:
any_goals rfl

Result:
R : Type u_1
inst✝¹ : CommRing R
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}

Proof state:
case mp
R : Type u_1
inst✝¹ : CommRing R
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}

Tactic:
rintro ⟨x, y, hx, hy, h⟩

Result:
case mp.intro.intro.intro.intro
R : Type u_1
inst✝¹ : CommRing R
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}

Proof state:
case mp.intro.intro.intro.intro
R : Type u_1
inst✝¹ : CommRing R
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}

Tactic:
rcases Ideal.mem_span_singleton_mul.mp ((Ideal.span_singleton_le_iff_mem _).mp h.ge) with
  ⟨i, _hi, rfl⟩

Result:
case mp.intro.intro.intro.intro.intro.intro
R : Type u_1
inst✝¹ : CommRing R
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}

Proof state:
case mpr
R : Type u_1
inst✝¹ : CommRing R
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} * ⊤

Tactic:
rintro ⟨x, hx, rfl⟩

Result:
case mpr.intro.intro
R : Type u_1
inst✝¹ : CommRing R
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} * ⊤

Proof state:
case mp.intro.intro.intro.intro.intro.intro
R : Type u_1
inst✝¹ : CommRing R
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}

Tactic:
exact ⟨i, right_ne_zero_of_mul hy, h⟩

Result:
no goals

Proof state:
case mp.intro.intro.intro.intro
R : Type u_1
inst✝¹ : CommRing R
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}

Tactic:
rw [Ideal.mul_top] at h

Result:
case mp.intro.intro.intro.intro
R : Type u_1
inst✝¹ : CommRing R
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}

Proof state:
R : Type u_1
inst✝¹ : CommRing R
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} * ⊤

Tactic:
rw [Ideal.span_singleton_one, Ideal.top_mul, Ideal.mul_top]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' : Ideal R
hI : ↑I = ↑I'
⊢ mk I = 1 ↔ ∃ x, x ≠ 0 ∧ I' = Ideal.span {x}

Tactic:
rw [← map_one (ClassGroup.mk (R := R) (K := FractionRing R)),
  ClassGroup.mk_eq_mk_of_coe_ideal hI]

Result:
R : Type u_1
inst✝¹ : CommRing R
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} * ?m.66692) ↔ ∃ x, x ≠ 0 ∧ I' = Ideal.span {x}

R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' : Ideal R
hI : ↑I = ↑I'
⊢ ↑1 = ↑?m.66692

R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' : Ideal R
hI : ↑I = ↑I'
⊢ Ideal R

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' : Ideal R
hI : ↑I = ↑I'
⊢ ↑1 = ↑?m.66692

Tactic:
rfl

Result:
no goals

Proof state:
case mpr.intro.intro
R : Type u_1
inst✝¹ : CommRing R
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} * ⊤

Tactic:
exact ⟨1, x, one_ne_zero, hx, by rw [Ideal.span_singleton_one, Ideal.top_mul, Ideal.mul_top]⟩

Result:
no goals