import algebra.ring
import tactic.nth_rewrite
import tactic.noncomm_ring

-- Thanks to the Lean Zulip for their help, especially to the following people: Riccardo Brasca, Eric Wieser, Ruben Van de Velde, Patrick Massot

-- (Def 1.1) Fadelian rings
class fadelian (R : Type*) [ring R] : Prop :=
  (prop : ∀(x:R), ∀(a:R), (a ≠ 0) → (∃(b:R), ∃(c:R), x=a*b+c*a))

-- (Def 1.1) Weakly fadelian rings
class weak_fadelian (R : Type*) [ring R] : Prop :=
  (prop : ∀(a:R), (a ≠ 0) → (∃(b:R), ∃(c:R), 1=a*b+c*a))

-- Integral rings
class integral (R : Type*) [ring R] : Prop :=
  (prop : ∀(x:R), ∀(y:R), (x*y=0) → (x=0) ∨ (y=0))

-- (Def 2.5) Left Ore rings
class left_ore (R : Type*) [ring R] : Prop :=
  (prop : ∀(x:R), ∀(y:R), (x≠0) → (y≠0) → ∃(a:R),∃(b:R),(a≠0) ∧ (b≠0) ∧ (a*x=b*y))

-- (Intro) Fadelian rings are weakly fadelian
instance fadelian.to_weak_fadelian {R : Type*} [ring R] [fadelian R] :
  weak_fadelian R := begin
    apply weak_fadelian.mk,
    exact fadelian.prop 1,
  end

-- (Lemma 2.3) In a weakly fadelian ring, xy=yx=0 ⇒ x²=0 or y²=0
lemma lem_integral_1 {R :Type*} [ring R] [weak_fadelian R]
  (x:R) (y:R) (xy_zero : x*y=0) (yx_zero : y*x=0) :
  (x*x=0) ∨ (y*y=0) :=
  begin
    cases (em (x=0)) with x_zero x_nonzero,
    
    have xx_zero : x*x=0 := by rw [x_zero, mul_zero],
    left, exact xx_zero,

    obtain ⟨b,c,d⟩ := weak_fadelian.prop x x_nonzero,
    have yy_zero : (y*y = 0) := begin
      nth_rewrite 0 ← mul_one y,
      rw [d, mul_add, add_mul],
      assoc_rewrite yx_zero,
      assoc_rewrite xy_zero,
      noncomm_ring,
    end,
    right, exact yy_zero,
end

-- (Lemma 2.4) In a weakly fadelian ring, x²=0 ⇒ x=0
lemma lem_integral_2 {R :Type*} [ring R] [weak_fadelian R]
  (x : R) (xx_zero : x*x=0) :
  x=0 :=
  begin
    classical,
    by_contradiction x_nonzero,
    obtain ⟨b, c, d⟩ := weak_fadelian.prop x x_nonzero,

    have cx_eq_cxcx : c*x=c*(x*c)*x := begin
      rw [← mul_one (c*x), d, mul_add],
      assoc_rewrite xx_zero,
      noncomm_ring,
    end,
    have xb_eq_xbxb : x*b=x*(b*x)*b := begin
      rw [← one_mul (x*b), d, add_mul],
      assoc_rewrite xx_zero,
      noncomm_ring,
    end,

    have cxxb_zero : (c*x)*(x*b) = 0 :=
      begin assoc_rewrite xx_zero, noncomm_ring end,

    have xb_from_cx : x*b = 1 - c * x
      := eq_sub_of_add_eq (eq.symm 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],
    have xbcx_zero : (x*b)*(c*x) = 0
      := (eq.congr rfl cxxb_zero).mp xb_cx_commute,

    have xbxb_or_cxcx_zero : ((x*b)*(x*b)=0) ∨ ((c*x)*(c*x))=0
      := lem_integral_1 (x*b) (c*x) xbcx_zero cxxb_zero,

    have one_eq_zero : ((0:R)=(1:R)) := begin
      cases xbxb_or_cxcx_zero with xbxb_zero cxcx_zero,

      assoc_rewrite (eq.symm xb_eq_xbxb) at xbxb_zero,
      rw [xbxb_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],
      rw [xx_zero, mul_zero] at ccxx_one,
      apply ccxx_one,

      assoc_rewrite (eq.symm cx_eq_cxcx) at cxcx_zero,
      rw [cxcx_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],
      rw [xx_zero, zero_mul] at xxbb_one,
      apply xxbb_one,
    end,

    have x_one : (x=x*1) := by rw mul_one,
    rw [← one_eq_zero, mul_zero] at x_one,
    exact x_nonzero x_one,
  end

-- (Theorem 2.2) Weakly fadelian rings are integral
instance weak_fadelian.to_integral {R :Type*} [ring R] [weak_fadelian R] :
  integral R :=
begin
  apply integral.mk, intro x, intro y, intro xy_zero,
  have yx_zero : y*x=0 := begin
    apply lem_integral_2 (y*x),
    assoc_rewrite xy_zero,
    noncomm_ring,
  end,
  cases (lem_integral_1 x y xy_zero yx_zero)
    with xx_zero yy_zero,
  left, exact lem_integral_2 x xx_zero,
  right, exact lem_integral_2 y yy_zero,
end

-- (Theorem 2.6) Weakly fadelian left Ore rings are fadelian
theorem left_ore_weak_fadelian_is_fadelian {R :Type*} [ring R] [left_ore R] [weak_fadelian R] :
  fadelian R :=
begin
  have H : integral R := by apply weak_fadelian.to_integral,

  apply fadelian.mk, intro x, intro a, intro a_nonzero,
  cases (em (x=0)) with x_zero x_nonzero,

  existsi (0:R), existsi (0:R), rw x_zero, noncomm_ring,

  obtain ⟨b, c, b_nonzero, c_nonzero, bx_eq_ca⟩
    := left_ore.prop x a x_nonzero a_nonzero,
  have ab_nonzero : (a*b ≠ 0) := begin
    intro ab_zero,
    cases (integral.prop a b ab_zero) with a_zero b_zero,
    exact a_nonzero a_zero, exact b_nonzero b_zero,
  end,
  obtain ⟨k, l, abk_p_lab_eq_one⟩ := weak_fadelian.prop (a*b) ab_nonzero,
  existsi (b*k*x), existsi (l*a*c),
  assoc_rewrite (eq.symm bx_eq_ca),
  rw [← mul_assoc, ← mul_assoc, ← add_mul],
  rw [mul_assoc l a, ← abk_p_lab_eq_one, one_mul],
end