import Mathlib.Algebra.Ring.Basic
import Mathlib.Algebra.Ring.Defs
import Mathlib.Tactic.NoncommRing

variable {R : Type*} [Ring R] [Nontrivial R]

-- Lean 4.2 version (2023-11-27, updated 2025-11-22)
-- Thanks to the Lean Zulip for their help, especially to the following people:
--- Riccardo Brasca, Eric Wieser, Ruben Van de Velde, Patrick Massot

-- Fadelian, weakly fadelian rings
class Fadelian (R : Type*) [Ring R] [Nontrivial R] where
  prop :
    ∀(x : R), ∀(a : R),
    a ≠ 0 →
    ∃(b : R), ∃(c : R),
    x = a * b + c * a

class WeakFadelian (R : Type*) [Ring R] [Nontrivial R] where
  prop :
    ∀(a : R),
    a ≠ 0 →
    ∃(b : R), ∃(c : R),
    1 = a * b + c * a

-- Fadelian rings are weakly fadelian
instance WeakFadelian.toFadelian [Fadelian R]
  : WeakFadelian R
  := ⟨ Fadelian.prop 1 ⟩

-- Left Ore rings
class LeftOre (R : Type*) [Ring R] [IsDomain R] where
  prop :
    ∀(x:R), ∀(y:R),
    (x≠0) → (y≠0) →
    ∃(a:R),∃(b:R),
    a ≠ 0 ∧ b ≠ 0
    ∧ a * x = b * y

-- In a weakly fadelian ring, xy = yx = 0 ⇒ x² = 0 or y² = 0
lemma lem_domain_1
  [WeakFadelian R]
  (x y : R)
  (xy_zero : x * y = 0) (yx_zero : y * x = 0)
  :
  (x * x = 0) ∨ (y * y = 0)
  := by
    by_cases x_zero : x = 0
    · left
      rw [x_zero, mul_zero]
    · right
      obtain ⟨b,c,d⟩ := WeakFadelian.prop x x_zero
      rw [← mul_one y, d]
      simp [mul_add, ← mul_assoc, yx_zero]
      simp [mul_assoc, xy_zero]

-- In a weakly fadelian ring, x² = 0 ⇒ x = 0
lemma lem_domain_2
  [WeakFadelian R]
  (x : R)
  (xx_zero : x * x = 0)
  :
  x = 0
  := by
    by_contra x_nonzero
    obtain ⟨b, c, d⟩ := WeakFadelian.prop x x_nonzero

    have cx_eq_cxcx :
      c * x = c * (x * c) * x
      := by
      rw [← mul_one (c * x), d, mul_add]
      simp [mul_assoc]
      rw [← mul_assoc x, xx_zero]
      simp
    have xb_eq_xbxb : x * b = x * (b * x) * b := by
      rw [← one_mul (x * b), d, add_mul]
      simp [mul_assoc]
      simp [← mul_assoc x, xx_zero]
    have xbxb_or_cxcx_zero : (x * b) * (x * b) = 0 ∨ (c * x) * (c * x) = 0 := by
      apply lem_domain_1
      · have xb_from_cx : x * b = 1 - c * x := by simp [d]
        have xb_cx_commute : (x * b) * (c * x) = (c * x) * (x * b) := by
          rw [xb_from_cx, sub_mul, one_mul, mul_sub, mul_one]
        rw [xb_cx_commute]
        rw [mul_assoc c, ← mul_assoc x, xx_zero]
        simp
      · rw [mul_assoc, ←mul_assoc x, xx_zero]
        simp

    suffices one_eq_zero :(0 : R) = (1 : R) by
      apply x_nonzero
      rw [← one_mul x, ← one_eq_zero, zero_mul]

    rcases xbxb_or_cxcx_zero with xbxb_zero | cxcx_zero
    · have xb_zero : x*b=0 := by
        rw [xb_eq_xbxb, mul_assoc, mul_assoc, ← mul_assoc, xbxb_zero]
      rw [xb_zero, zero_add] at d
      have ccxx_one : (c*c)*(x*x) = 1 := by
        rw [← mul_assoc, mul_assoc c c x, ← d, mul_one, ← d]
      simp [←ccxx_one, xx_zero]
    · have cx_zero : c*x=0 := by
        rw [cx_eq_cxcx, mul_assoc, mul_assoc, ← mul_assoc, cxcx_zero]
      rw [cx_zero, add_zero] at d
      have xxbb_one : (x*x)*(b*b) = 1 := by
        rw [← mul_assoc, mul_assoc x x b, ← d, mul_one, ← d]
      simp [←xxbb_one, xx_zero]

-- Weakly fadelian rings are domains
instance WeakFadelian.to_isDomain
  [WeakFadelian R]
  :
  IsDomain R
  := by
    apply (isDomain_iff_noZeroDivisors_and_nontrivial R).2
    constructor
    swap
    · apply_assumption
    constructor
    intro x y xy_zero
    have yx_zero : y * x = 0 := by
      apply lem_domain_2
      simp [mul_assoc, ←mul_assoc x, xy_zero]
    rcases (lem_domain_1 x y xy_zero yx_zero) with xx_zero | yy_zero
    · left
      exact lem_domain_2 x xx_zero
    · right
      exact lem_domain_2 y yy_zero

-- Weakly fadelian left Ore rings are fadelian
theorem left_ore_weak_fadelian_is_fadelian
  [WeakFadelian R]
  [LeftOre R]
  :
  Fadelian R
  := by
    constructor
    intro x a a_nonzero
    by_cases x_zero : x = 0
    · use 0, 0
      simp [x_zero]
    · obtain ⟨b, c, b_nonzero, _, bx_eq_ca⟩ :=
        LeftOre.prop x a x_zero a_nonzero
      have ab_nonzero : (a*b ≠ 0) := by
        simp [a_nonzero, b_nonzero]
      obtain ⟨k, l, abk_p_lab_eq_one⟩ :=
        WeakFadelian.prop (a*b) ab_nonzero
      use (b*k*x), (l*a*c)
      simp [mul_assoc, ←bx_eq_ca]
      simp [← mul_assoc, ← add_mul]
      simp [mul_assoc l a b, ← abk_p_lab_eq_one]