A total quotient ring with a proper invertible ideal

import Mathlib.Algebra.TrivSqZeroExt.Basic
import Mathlib.LinearAlgebra.TensorProduct.Prod
import Mathlib.RingTheory.Localization.FractionRing
import Mathlib.RingTheory.PicardGroup
import Definitions.Def_RybinP18_CuspidalCubicInput
import Definitions.Def_RybinP18_MO507128

/-!
# MathOverflow 507128: the idealization step

This file deliberately does not import or clone `formal-conjectures`.  It copies the
statement of the target theorem and proves the square-zero idealization argument using
mathlib.

The input for the idealization is constructed explicitly from the cuspidal cubic
`Y² = X³`.  Thus the final `#print axioms` contains no problem-specific axiom.
-/

namespace Mathoverflow507128

universe u v

variable (D : Type u) [CommRing D]
variable (M : Type v) [AddCommGroup M] [Module D M]

local instance p2m_Theorems_Thm_Mathoverflow507128_exists_isFractionRing_self_ideal_ne_top_invertible_1 : Module Dᵐᵒᵖ M :=
  Module.compHom M ((RingHom.id D).fromOpposite mul_comm)

local instance p2m_Theorems_Thm_Mathoverflow507128_exists_isFractionRing_self_ideal_ne_top_invertible_2 : IsCentralScalar D M := ⟨fun _ _ => rfl⟩

local notation "R" => TrivSqZeroExt D M



































end Mathoverflow507128

namespace Mathoverflow507128

/-- The theorem statement copied from Formal Conjectures, with its project-specific
attributes removed. -/
theorem exists_isFractionRing_self_ideal_ne_top_invertible :
    ∃ (R : Type) (_ : CommRing R) (_ : IsFractionRing R R) (I : Ideal R),
      I ≠ ⊤ ∧ Module.Invertible R I := by
  sorry

end Mathoverflow507128