-- Mathlib/RingTheory/DedekindDomain/PID.lean
theorem FractionalIdeal.isPrincipal_of_unit_of_comap_mul_span_singleton_eq_top {R A : Type*}
    [CommRing R] [CommRing A] [Algebra R A] {S : Submonoid R} [IsLocalization S A]
    (I : (FractionalIdeal S A)ˣ) {v : A} (hv : v ∈ (↑I⁻¹ : FractionalIdeal S A))
    (h : Submodule.comap (Algebra.linearMap R A) ((I : Submodule R A) * Submodule.span R {v}) = ⊤) :
    Submodule.IsPrincipal (I : Submodule R A)

Proof state:
case intro.intro.refine_2
R : Type u_2
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
I : (FractionalIdeal S A)ˣ
v : A
hv : v ∈ ↑I⁻¹
hinv : ↑I * ↑I⁻¹ = 1
J : Submodule R R := Submodule.comap (Algebra.linearMap R A) (↑↑I * Submodule.span R {v})
h : J = ⊤
hJ : IsLocalization.coeSubmodule A J = ↑↑I * Submodule.span R {v}
this : 1 ∈ ↑↑I * Submodule.span R {v}
w : A
hw : w ∈ ↑↑I
hvw : w * v = 1
⊢ 1 ≤ ↑I⁻¹ * spanSingleton S w

Tactic:
rw [FractionalIdeal.one_le, ← hvw, mul_comm]

Result:
case intro.intro.refine_2
R : Type u_2
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
I : (FractionalIdeal S A)ˣ
v : A
hv : v ∈ ↑I⁻¹
hinv : ↑I * ↑I⁻¹ = 1
J : Submodule R R := Submodule.comap (Algebra.linearMap R A) (↑↑I * Submodule.span R {v})
h : J = ⊤
hJ : IsLocalization.coeSubmodule A J = ↑↑I * Submodule.span R {v}
this : 1 ∈ ↑↑I * Submodule.span R {v}
w : A
hw : w ∈ ↑↑I
hvw : w * v = 1
⊢ w * v ∈ spanSingleton S w * ↑I⁻¹

Proof state:
R : Type u_2
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
I : (FractionalIdeal S A)ˣ
v : A
hv : v ∈ ↑I⁻¹
hinv : ↑I * ↑I⁻¹ = 1
J : Submodule R R := Submodule.comap (Algebra.linearMap R A) (↑↑I * Submodule.span R {v})
h : J = ⊤
⊢ (↑↑I).IsPrincipal

Tactic:
have hJ : IsLocalization.coeSubmodule A J = ↑I * Submodule.span R {v} := by
  rw [Subtype.ext_iff, val_eq_coe, coe_mul, val_eq_coe, coe_one] at hinv
  apply Submodule.map_comap_eq_self
  rw [← Submodule.one_eq_range, ← hinv]
  exact Submodule.mul_le_mul_right ((Submodule.span_singleton_le_iff_mem _ _).2 hv)

Result:
R : Type u_2
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
I : (FractionalIdeal S A)ˣ
v : A
hv : v ∈ ↑I⁻¹
hinv : ↑I * ↑I⁻¹ = 1
J : Submodule R R := Submodule.comap (Algebra.linearMap R A) (↑↑I * Submodule.span R {v})
h : J = ⊤
hJ : IsLocalization.coeSubmodule A J = ↑↑I * Submodule.span R {v}
⊢ (↑↑I).IsPrincipal

Proof state:
R : Type u_2
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
I : (FractionalIdeal S A)ˣ
v : A
hv : v ∈ ↑I⁻¹
hinv : ↑I * ↑I⁻¹ = 1
J : Submodule R R := Submodule.comap (Algebra.linearMap R A) (↑↑I * Submodule.span R {v})
h : J = ⊤
hJ : IsLocalization.coeSubmodule A J = ↑↑I * Submodule.span R {v}
⊢ (↑↑I).IsPrincipal

Tactic:
have : (1 : A) ∈ ↑I * Submodule.span R {v} := by
  rw [← hJ, h, IsLocalization.coeSubmodule_top, Submodule.mem_one]
  exact ⟨1, (algebraMap R _).map_one⟩

Result:
R : Type u_2
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
I : (FractionalIdeal S A)ˣ
v : A
hv : v ∈ ↑I⁻¹
hinv : ↑I * ↑I⁻¹ = 1
J : Submodule R R := Submodule.comap (Algebra.linearMap R A) (↑↑I * Submodule.span R {v})
h : J = ⊤
hJ : IsLocalization.coeSubmodule A J = ↑↑I * Submodule.span R {v}
this : 1 ∈ ↑↑I * Submodule.span R {v}
⊢ (↑↑I).IsPrincipal

Proof state:
R : Type u_2
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
I : (FractionalIdeal S A)ˣ
v : A
hv : v ∈ ↑I⁻¹
hinv : ↑I * ↑I⁻¹ = 1
J : Submodule R R := Submodule.comap (Algebra.linearMap R A) (↑↑I * Submodule.span R {v})
h : J = ⊤
⊢ IsLocalization.coeSubmodule A J = ↑↑I * Submodule.span R {v}

Tactic:
rw [Subtype.ext_iff, val_eq_coe, coe_mul, val_eq_coe, coe_one] at hinv

Result:
R : Type u_2
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
I : (FractionalIdeal S A)ˣ
v : A
hv : v ∈ ↑I⁻¹
hinv : ↑↑I * ↑↑I⁻¹ = 1
J : Submodule R R := Submodule.comap (Algebra.linearMap R A) (↑↑I * Submodule.span R {v})
h : J = ⊤
⊢ IsLocalization.coeSubmodule A J = ↑↑I * Submodule.span R {v}

Proof state:
R : Type u_2
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
I : (FractionalIdeal S A)ˣ
v : A
hv : v ∈ ↑I⁻¹
h : Submodule.comap (Algebra.linearMap R A) (↑↑I * Submodule.span R {v}) = ⊤
⊢ (↑↑I).IsPrincipal

Tactic:
have hinv := I.mul_inv

Result:
R : Type u_2
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
I : (FractionalIdeal S A)ˣ
v : A
hv : v ∈ ↑I⁻¹
h : Submodule.comap (Algebra.linearMap R A) (↑↑I * Submodule.span R {v}) = ⊤
hinv : ↑I * ↑I⁻¹ = 1
⊢ (↑↑I).IsPrincipal

Proof state:
case h
R : Type u_2
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
I : (FractionalIdeal S A)ˣ
v : A
hv : v ∈ ↑I⁻¹
hinv : ↑↑I * ↑↑I⁻¹ = 1
J : Submodule R R := Submodule.comap (Algebra.linearMap R A) (↑↑I * Submodule.span R {v})
h : J = ⊤
⊢ ↑↑I * Submodule.span R {v} ≤ LinearMap.range (Algebra.linearMap R A)

Tactic:
rw [← Submodule.one_eq_range, ← hinv]

Result:
case h
R : Type u_2
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
I : (FractionalIdeal S A)ˣ
v : A
hv : v ∈ ↑I⁻¹
hinv : ↑↑I * ↑↑I⁻¹ = 1
J : Submodule R R := Submodule.comap (Algebra.linearMap R A) (↑↑I * Submodule.span R {v})
h : J = ⊤
⊢ ↑↑I * Submodule.span R {v} ≤ ↑↑I * ↑↑I⁻¹

Proof state:
case h
R : Type u_2
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
I : (FractionalIdeal S A)ˣ
v : A
hv : v ∈ ↑I⁻¹
hinv : ↑↑I * ↑↑I⁻¹ = 1
J : Submodule R R := Submodule.comap (Algebra.linearMap R A) (↑↑I * Submodule.span R {v})
h : J = ⊤
⊢ ↑↑I * Submodule.span R {v} ≤ ↑↑I * ↑↑I⁻¹

Tactic:
exact Submodule.mul_le_mul_right ((Submodule.span_singleton_le_iff_mem _ _).2 hv)

Result:
no goals

Proof state:
case intro.intro.refine_1
R : Type u_2
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
I : (FractionalIdeal S A)ˣ
v : A
hv : v ∈ ↑I⁻¹
hinv : ↑I * ↑I⁻¹ = 1
J : Submodule R R := Submodule.comap (Algebra.linearMap R A) (↑↑I * Submodule.span R {v})
h : J = ⊤
hJ : IsLocalization.coeSubmodule A J = ↑↑I * Submodule.span R {v}
this : 1 ∈ ↑↑I * Submodule.span R {v}
w : A
hw : w ∈ ↑↑I
hvw : w * v = 1
⊢ ↑I⁻¹ * spanSingleton S w ≤ ↑I⁻¹ * ↑I

Tactic:
apply FractionalIdeal.mul_le_mul_left (FractionalIdeal.spanSingleton_le_iff_mem.mpr hw)

Result:
no goals

Proof state:
R : Type u_2
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
I : (FractionalIdeal S A)ˣ
v : A
hv : v ∈ ↑I⁻¹
hinv : ↑I * ↑I⁻¹ = 1
J : Submodule R R := Submodule.comap (Algebra.linearMap R A) (↑↑I * Submodule.span R {v})
h : J = ⊤
hJ : IsLocalization.coeSubmodule A J = ↑↑I * Submodule.span R {v}
⊢ 1 ∈ ↑↑I * Submodule.span R {v}

Tactic:
rw [← hJ, h, IsLocalization.coeSubmodule_top, Submodule.mem_one]

Result:
R : Type u_2
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
I : (FractionalIdeal S A)ˣ
v : A
hv : v ∈ ↑I⁻¹
hinv : ↑I * ↑I⁻¹ = 1
J : Submodule R R := Submodule.comap (Algebra.linearMap R A) (↑↑I * Submodule.span R {v})
h : J = ⊤
hJ : IsLocalization.coeSubmodule A J = ↑↑I * Submodule.span R {v}
⊢ ∃ y, (algebraMap R A) y = 1