Ceva's theorem - Lean adaption of the Metamath

cevath.lean

import data.complex.basic
import tactic

-- Adaption of Metamath Ceva proof: http://us.metamath.org/mpeuni/cevath.html


open complex
open_locale complex_conjugate


-- The G operator, central to the Ceva proof.
def g_op (x y : ℂ) : ℂ := { re:= ((conj x) * y).im, im:= 0}
local infixr ` G `:65 := g_op

example : g_op ⟨0, 0⟩  ⟨0, 0⟩ = 0 :=
begin
  unfold g_op,
  simp,
  refl,
end

lemma g_op_antisymm ( x y : ℂ ) : x G y = - ( y G x ) :=
begin
  unfold g_op,
  simp,
  ext,
  {
    simp,
    rw mul_comm y.im  x.re,
    rw mul_comm y.re  x.im,
  },
  simp,
end


-- sigar theorems, as named in Metamath

lemma cjdiv (A B: ℂ) (hnz: B ≠ 0): conj ( A / B ) = conj A / conj B :=
begin
  exact ring_equiv.map_div conj A B,
end

lemma cjdivd (A B: ℂ) (hnz: B ≠ 0) : conj (A / B) = (conj A) / (conj B) :=
begin
  rwa cjdiv,
end

lemma cjred_2 (A: ℂ) (himz: A.im = 0) : conj (A) = A :=
begin
  exact eq_conj_iff_im.mpr himz,
end

lemma redivcld (A B: ℂ) (hai: A.im = 0) (hbi: B.im=0): (A / B).im = 0 :=
begin
  simp [complex.div_im, hai, hbi],
end

lemma divcan5rd (A B C: ℂ) (hnzb: B ≠ 0) (hnzc: C ≠ 0): (A * C) / (B * C) = (A / B) :=
begin
  exact mul_div_mul_right A B hnzc,
end

-- (𝐴𝐺𝐵) = (ℑ‘((∗‘𝐴) · 𝐵)))
lemma sigarval (A B : ℂ) : A G B = (conj A * B).im :=
begin
  unfold g_op, simp,
  ext,
  {
    simp,
  },
  simp,
end

lemma cjcjd (x : ℂ) : conj (conj x) = x :=
begin
  simp,
end


lemma sigardiv (A B C: ℂ) (hnz: C ≠ A) (hgz: B - A G C - A = 0) :
   ((B - A) / (C - A)).im = 0 :=
begin
  have h9:  C - A ≠ 0,
  {
    exact sub_ne_zero.mpr hnz,
  },

  -- (∗‘((𝐵 − 𝐴) / (𝐶 − 𝐴))) = ((∗‘(𝐵 − 𝐴)) / (∗‘(𝐶 − 𝐴))))
  have h10: conj ((B - A) / (C - A)) = (conj (B - A)) / (conj (C - A)),
  {
    rw cjdivd,
    exact sub_ne_zero.mpr hnz,
  },

  --  (∗‘(𝐶 − 𝐴)) ≠ 0)
  have h13: conj (C - A) ≠ 0,
  {
    exact (ring_equiv.map_ne_zero_iff conj).mpr h9,
  },

   --   (((∗‘(𝐵 − 𝐴)) · (𝐶 − 𝐴)) / ((∗‘(𝐶 − 𝐴)) · (𝐶 − 𝐴))) = ((∗‘(𝐵 − 𝐴)) / (∗‘(𝐶 − 𝐴))))
  have h14: conj (B - A) * (C - A) / (conj (C - A) * (C - A)) = conj (B - A) / conj (C - A),
  {
    exact divcan5rd (conj (B - A)) (conj (C - A)) (C - A) h13 h9,
  },

  -- ((𝐵 − 𝐴)𝐺(𝐶 − 𝐴)) = (ℑ‘((∗‘(𝐵 − 𝐴)) · (𝐶 − 𝐴))))
  have h18: (B - A) G (C - A) =  ((conj (B - A)) * (C - A)).im,
  {
    exact sigarval (B - A) (C - A),
  },

  have h20:  ((conj (B - A)) * (C - A)).im = 0,
  {
    rw hgz at h18,
    norm_cast at h18,
    rw ← h18,
  },

  -- ((∗‘(𝐵 − 𝐴)) · (𝐶 − 𝐴)) ∈ ℝ)
  have h21: (conj (B -A) * (C - A)).im = 0,
  {
    exact h20,
  },

  -- (𝜑 → ((∗‘(𝐶 − 𝐴)) · (𝐶 − 𝐴)) ∈ ℝ)
  have h24: (conj (C - A) * (C - A)).im = 0,
  {
    simp,
    linarith,
  },


  have h26: (conj (B - A) * (C - A) / (conj (C - A) * (C - A))).im = 0,
  {
    rw redivcld _ _ h21 h24,
  },

  -- ((∗‘(𝐵 − 𝐴)) / (∗‘(𝐶 − 𝐴))) ∈ ℝ
  have h27: (conj (B - A) / conj (C - A)).im = 0,
  {
     rw ← h14,
     exact h26,
  },

  -- (∗‘(∗‘((𝐵 − 𝐴) / (𝐶 − 𝐴)))) = (∗‘((𝐵 − 𝐴) / (𝐶 − 𝐴))))
  have h28: (conj ((B - A) / (C - A))).im = 0,
  {
    rw [h10, h27],
  },

  have h29: conj (conj ((B - A) / (C - A))) = conj ((B - A) / (C - A)),
  {
    exact cjred_2 (conj ((B - A) / (C - A))) h28,
  },

  have h31: conj (conj ((B - A) / (C - A))) = ((B - A) / (C - A)),
  {
    exact cjcjd ((B - A) / (C - A)),
  },

            -- ‘((𝐵 − 𝐴) / (𝐶 − 𝐴))) = ((𝐵 − 𝐴) / (𝐶 − 𝐴)))
  have h32: conj ((B - A) / (C - A)) = ((B - A) / (C - A)),
  {
    rw [← h29, h31],
  },

  rw ← h32,
  rw h28,
end


lemma sigarms (A B C: ℂ): A G (B - C) = (A G B) - (A G C) :=
begin
  unfold g_op,
  ext,
  simp, linarith,
  simp,
end

lemma sigarmf (A B C: ℂ): (A - C) G B = (A G B) - (C G B) :=
begin
  unfold g_op,
  ext, {
    simp,
    linarith,
  },
  simp,
end

lemma sigaraf {A B C : ℂ}:  ( A + C ) G B = (A G B) + (C G B) :=
begin
  unfold g_op,
  simp,
  ext,
  {
    simp,
    linarith,
  },
  simp,
end

lemma sigarperm (A B C : ℂ) : (A - C G B - C) = (B - A G C - A) :=
begin
  unfold g_op,
  simp,
  rw [sub_mul, mul_sub],
  rw [sub_mul, mul_sub],
  rw [sub_mul, mul_sub],
  rw [sub_mul, mul_sub],
  linarith,
end

lemma sigariz (A B: ℂ) (h: A G B = 0) : B G A = 0 :=
begin
  rw g_op_antisymm,
  rw h,
  simp,
end

lemma sigaradd (A B C D : ℂ) (hb: A - D G B - D = 0) :
   (B - C G A - C)  - (D - C G A - C) = (B - C G D - C) :=
begin
  have h6: (A - C) - (A - D) = D - C, simp,

  have h7: (( B - D ) G (( A - C ) - ( A - D )) ) = (( B - D ) G ( D - C )),  simp,

  have h13: ( B - D ) G (( A - C ) - ( A - D )) = (( B - D ) G ( A - C )) - (( B - D ) G ( A - D )) ,
  exact sigarms (B - D) (A - C) (A - D),

  have h14: ( ( B - D ) G ( ( A - C ) - ( A - D ) ) ) = ( ( ( B - D ) G ( A - C ) ) - ( ( B - D ) G ( A - D ) ) ) ,
   exact sigarms (B - D) (A - C) (A - D),

  have h15: ( B - D ) G ( D - C )  = ((( B - D ) G ( A - C )) - (( B - D ) G ( A - D ))),
   rw [← h7, h14],


  have h17: ( ( A - D ) G ( B - D ) ) = -( ( B - D ) G ( A - D ) ), {
    exact g_op_antisymm (A - D) (B - D),
  },

  have hb2: -(A - D G B - D ) = 0, {
    rw hb, simp,
  },

  have h26: ( ( B - D ) G ( A - D ) ) = 0, {
    rw ← hb2,
    rw g_op_antisymm ,
  },

  have h27: ( ( B - D ) G ( A - C ) ) - ( ( B - D ) G ( A - D ) )  = ( ( ( B - D ) G ( A - C ) ) - 0 ),
  rw ← h26,

  have h30: ( ( B - D ) G ( A - C ) ) - 0 = ( ( B - D ) G ( A - C ) ), simp,

  have h31: ( B - D ) G ( D - C ) = ( B - D ) G ( A - C ),
  rw [h15, h27, h30],

  have h32:  ( B - C ) - ( D - C ) = ( B - D ), simp,
  have h33: (( B - C ) - ( D - C )) G ( A - C ) = ( B - D ) G ( A - C ), rw h32,

  have h37:  ( ( ( B - C ) - ( D - C ) ) G ( A - C ) ) = ( ( ( B - C ) G ( A - C ) ) - ( ( D - C ) G ( A - C ) ) ),   exact sigarmf (B - C) (A - C) (D - C),

  have h38: (( B - C ) G ( A - C )) - (( D - C ) G ( A - C )) = ( B - D ) G ( D - C ),
  {
    rw [h31, ← h33, h37],
  },

  have h58: (B - D) G (D - C ) = ( C - D ) G ( B - D ),
  {
    unfold g_op,
    simp,
    rw [sub_mul, mul_sub],
    rw [sub_mul, mul_sub],
    rw [sub_mul, mul_sub],
    rw [sub_mul, mul_sub],
    linarith,
  },

  have h60: (C - D) G (B - D ) = ( B - C ) G ( D - C ),
  {
    unfold g_op,
    simp,
    rw [sub_mul, mul_sub],
    rw [sub_mul, mul_sub],
    rw [sub_mul, mul_sub],
    rw [sub_mul, mul_sub],
    linarith,
  },

  rw [h38, h58, h60],
end

lemma sigarls (A B : ℂ) (C : ℝ) : (A G (B * C))  = ((A G B) * C ) :=
begin
  unfold g_op,
  simp,
  repeat { rw ← mul_assoc, },
  ext,
  {
    simp, rw add_mul,
    rw mul_assoc,
    rw tactic.ring.add_neg_eq_sub  (A.re * (B.im * C)) ((A.im * B.re) * C),
    rw ← mul_assoc,
    simp,
    rw tactic.ring.add_neg_eq_sub  (A.re * B.im * C) (A.im * B.re * C),
  },
  {
    simp,
  }
end


lemma sigarls_c (A B C : ℂ) (hr: C.im = 0) : (A G (B * C))  = ((A G B) * C ) :=
begin
  have h1: (A G (B * C.re))  = ((A G B) * C.re ),
  {
    rw sigarls A B C.re,
  },
  have h2: C = C.re,
  {
    ext,
    {
      simp,
    },
    simpa,
  },

  rwa h2,
end

lemma sharhght {A B C D O: ℂ} (Hb: A - D G B - D = 0) : (C - A G D - A) * (B - D) = (C - B G D - B) * (A - D) :=
begin

  have h14: B = D →( ( ( C - A ) G ( D - A ) ) * 0 ) = 0 ,
  {
    intro h,
    simp,
  },

  have h18: B = D → ( B - D ) = 0,
  {
    intro h, rw h, simp,
  },

  have h19: B = D → (C - A G D - A) * (B - D) = (C - A G D - A) * 0,
  {
    intro h, rw h, simp,
  },

  have h25:  B = D →  ( ( C - B ) G ( D - B ) ) =  ( ( conj ( C - B ) ) * ( D - B ) ).im,
  {
    intro h,
    unfold g_op, ext,
    {
      simp,
    },
    simp,
  },

  have h28: B = D → ( D - B ) = 0,
  {
    intro h, rw h, simp,
  },

  have h29: B = D → conj ( C - B )  * ( D - B ) = conj ( C - B ) * 0,
  {
    intro h,
    rw h28 h,
  },

  have h31: B = D → conj ( C - B ) * 0 = 0,
  simp,

  have h32: B = D → conj ( C - B )  * ( D - B ) = 0,
  {
    intro h,
    rw h29 h, rw h31 h,
  },

  have h33: B = D → ( conj ( C - B )  * ( D - B ) ).im = (mk 0 0).im,
  {
    intro h,
    rw (h32 h), simp,
  },

  have h35: B = D → (mk 0 0).im = 0,
  simp,

  have h36: B = D → ( ( C - B ) G ( D - B ) ) = 0,
  {
    intro h,
    rw [h25 h, h33 h], simp,
  },

  have h37: B = D → ( ( ( C - B ) G ( D - B ) ) * ( A - D ) ) = 0 * ( A - D ),
  {
    intro h,
    rw h36 h,
  },

  have h40: B = D →  0 * ( A - D ) = 0,
  {
    intro h, simp,
  },

  have h41: B = D → (C - B G D - B) * (A - D) = 0,
  {
    intro h,
    rw ← h40 h,
    rw ← h37 h,
  },

  -- 14, 19, 41
  have h42: B = D → (C - A G D - A) * (B - D) = (C - B G D - B) * (A - D),
  {
    intro h,
    rw h41 h,
    rw h19 h,
    simp,
  },

  have h47: ¬B = D →  ( ( ( C - B ) + ( B - A ) ) G ( D - A ) ) = ( ( C - A ) G ( D - A ) ),
  {
    unfold g_op,
    simp,
  },

  -- (((𝐶 − 𝐵) + (𝐵 − 𝐴))𝐺(𝐷 − 𝐴)) = (((𝐶 − 𝐵)𝐺(𝐷 − 𝐴)) + ((𝐵 − 𝐴)𝐺(𝐷 − 𝐴)))
  have h52: ¬B = D → ( (C - B) + (B - A)) G D - A = (C - B G D - A) + (B - A G D - A),
  {
    intro h,
    exact @sigaraf (C - B) (D - A) (B - A),
  },


 -- ((𝐶 − 𝐴)𝐺(𝐷 − 𝐴)) = (((𝐶 − 𝐵)𝐺(𝐷 − 𝐴)) + ((𝐵 − 𝐴)𝐺(𝐷 − 𝐴)))
  have h53: ¬B = D → ( ( C - A ) G ( D - A ) ) = ( ( ( C - B ) G ( D - A ) ) + ( ( B - A ) G ( D - A ) ) )
, {
    intro h,
    rw ← h47 h,
    rw h52 h,
  },

  have h59: (B - A) G (D - A) = 0,  -- 0 = ((𝐵 − 𝐴)𝐺(𝐷 − 𝐴)))
  {
    rw ← sigarperm,
    exact Hb,
  },

  have h60: ¬B = D → ( ( ( C - B ) G ( D - A ) ) + 0 ) = ( ( ( C - B ) G ( D - A ) ) + ( ( B - A ) G ( D - A ) ) )
, {
    intro h,
    rw h59,
  },

  have h64: ¬B = D → ( ( ( ( C - B ) G ( D - A ) ) + 0 ) = ( ( C - B ) G ( D - A ) ) ),
  simp,


  -- 53, 60, 64
  have h65: ¬B = D → ( ( C - A ) G ( D - A ) ) = ( ( C - B ) G ( D - A ) ),
  {
    intro h,
    rw h53 h,
    rw ← h60 h,
    rw h64 h,
  },

  have h67: ¬B = D → (D - B) = - (B - D),
  {
    simp,
  },
  have h68: ¬B = D → ( ( D - B ) / ( B - D ) ) = ( -( B - D ) / ( B - D ) )
, {
    intro h,
    rw h67 h,
  },

  have h72: ¬B = D → B - D ≠ 0,
  {
    intro h,
    exact sub_ne_zero.mpr h,
  },

  have h73: ¬B = D →  - ( ( B - D ) / ( B - D ) ) = ( - ( B - D ) / ( B - D ) )
, {
    intro h,
    rw ← h67 h,
    rw neg_div' (B - D) (B - D),
    simp,
  },
  have h75: ¬B = D → -( ( B - D ) / ( B - D ) ) = -1
, {
    intro h,
    simp,
    exact div_self (h72 h),
  },
  have h76: ¬B = D → ( ( D - B ) / ( B - D ) ) = -1,
  {
    intro h,
    rw h68 h,
    rw ← h73 h,
    rw h75 h,
     --	68, 73, 75
  },


  have h77: ¬B = D → ( ( ( D - B ) / ( B - D ) ) * ( A - D ) ) = ( (- 1) * ( A - D ) ),
  {
    intro h,
    rw ← h76 h,
  },

  have h79: ¬B = D → ( - 1 * ( A - D ) ) = - ( A - D ),
  {
    intro h,
    simp,
  },

  have h80: ¬B = D → - ( A - D ) = ( D - A ),
  {
    intro h,
    simp,
  },

  have h81: ¬B = D → ( ( ( D - B ) / ( B - D ) ) * ( A - D ) ) = ( D - A ),
  {
    intro h,
    rw h77 h,
    rw h79 h,
    rw h80 h,
  },

  have h83: ¬B = D → ( ( ( D - B ) / ( B - D ) ) * ( A - D ) ) = ( ( D - B ) * ( ( A - D ) / ( B - D ) ) )
, {
    intro h,
    exact mul_comm_div' (D - B) (B - D) (A - D),
  },

  have h84: ¬B = D → ( D - A ) = ( ( D - B ) * ( ( A - D ) / ( B - D ) ) ),
  {
     intro h,
     rw ← h81 h,
     rw h83 h,
  },

  have h85: ¬B = D →  ( C - B ) G ( D - A ) = ( C - B ) G ( ( D - B ) * ( ( A - D ) / ( B - D ) ) ),
  {
    intro h,
    rw ← h84 h,
  },

  have h87: ¬B = D → ((A - D) / (B - D)).im = 0,
  {
    intro h,
    exact sigardiv D A B h Hb,
  },

       -- ((𝐶 − 𝐵)𝐺((𝐷 − 𝐵) · ((𝐴 − 𝐷) / (𝐵 − 𝐷)))) = (((𝐶 − 𝐵)𝐺(𝐷 − 𝐵)) · ((𝐴 − 𝐷) / (𝐵 − 𝐷))))
  have h88: ¬B = D → C - B G (D - B) * ((A - D) / (B - D)) = (C - B G D - B) * ((A - D) / (B - D)),
  {
    intro h,

    exact sigarls_c (C - B) (D - B) ((A - D) / (B - D)) (h87 h), -- FIXME
  },


  have h89: ¬B = D → C - B G ((D - B) * ((A - D) / (B - D))) = (C - B G D - B) * ((A - D) / (B - D)),
  {
    -- h48:  (𝐶 − 𝐵),

    exact h88,
  },

  have h90: ¬B = D → ( C - A ) G ( D - A )  = ( ( C - B ) G ( D - B ) ) * ( ( A - D ) / ( B - D ) ),
  {
    intro h,
    rw h65 h,
    rw h85 h,
    rw h89 h,
  },

  have h91: ¬B = D → ( ( ( C - A ) G ( D - A ) ) * ( B - D ) ) = ( ( ( ( C - B ) G ( D - B ) ) * ( ( A - D ) / ( B - D ) ) ) * ( B - D ) ),
  {
    intro h,
    rw h90 h,
  },

  have h96: ¬B = D → ( ( ( ( C - B ) G ( D - B ) ) * ( ( A - D ) / ( B - D ) ) ) * ( B - D ) ) = ( ( ( C - B ) G ( D - B ) ) * ( ( ( A - D ) / ( B - D ) ) * ( B - D ) ) )
, {
    intro h,
    exact mul_assoc _ _ _,
  },

  have h97: ¬B = D → (  (A - D) / (B - D) ) * ( B - D ) = A - D,
  {
    intro h,
    have hz: B - D ≠ 0,  exact sub_ne_zero.mpr h,
    rw (eq_div_iff hz).mp rfl,  -- Deal with division
  },

  have h98: ¬B = D → ( ( C - B ) G ( D - B ) ) * ( ( ( A - D ) / ( B - D )  * ( B - D ) ) ) = ( ( C - B ) G ( D - B ) ) * ( A - D ),
  {
    intro h,
    have hz: B - D ≠ 0,  exact sub_ne_zero.mpr h,
    rw (eq_div_iff hz).mp rfl,  -- Deal with division
  },

  have h99: ¬B = D → (C - A G D - A) * (B - D) = (C - B G D - B) * (A - D),
  {
    intro h,
    rw h91 h,
    rw h96 h,
    rw h98 h,
  },


  by_cases hbd: B = D,
  {
    exact h42 hbd,
  },

  exact h99 hbd,
end


-- Lean proof for lemma 1 from http://us.metamath.org/mpeuni/cevathlem1.html
lemma cevathlem1 (A B C D E F L H K : ℂ)
      (hAz: A ≠ 0) (hEz: E ≠ 0) (hCz: C ≠ 0)
      (h1: A * B = C * D)
      (h2: E * F = A * L)
      (h3: C * H = E * K) : (B * F) * H = (D * L) * K :=
begin
  have h10: A * B * E * F = C * D * A * L,
  {
    rw h1,
    rw mul_assoc,
    rw h2,
    rw ← mul_assoc,
  },
  have h11: A * B * E * F * C * H = C * D * A * L * E * K,
  {
    rw h10,
    rw mul_assoc,
    rw h3,
    rw ← mul_assoc,
  },
  rw mul_comm (C * D) A at h11,
  repeat {rw mul_assoc at h11 },

  rw mul_right_inj' hAz at h11,

  repeat {rw ← mul_assoc at h11 },
  rw ← mul_comm C (B * E * F)  at h11,

  repeat {rw mul_assoc at h11 },
  rw mul_right_inj' hCz at h11,

  rw mul_comm B _ at h11,
  rw mul_comm D _ at h11,
  rw mul_comm L _ at h11,

  repeat {rw mul_assoc at h11 },
  rw mul_right_inj' hEz at h11,
  repeat  { rw ← mul_assoc at h11, },
  rw mul_comm F H at h11,
  rw mul_comm (H * F) B at h11,
  rw mul_comm H F at h11,
  repeat {rw ← mul_assoc at h11 },
  rw mul_comm K L at h11,
  rw mul_comm (L * K) D at h11,
  rw ← mul_assoc at h11,
  exact h11,
end


-- Adaption of Metamath proof for Ceva, lemma 2: http://us.metamath.org/mpeuni/cevathlem2.html
lemma cevathlem2  (A B C D E F O: ℂ)
  ( h1 : ( A - O  G  D - O ) = 0 )
  ( h2 : ( B - O  G  E - O ) = 0 )
  ( h3 : ( C - O  G  F - O ) = 0 )
  ( h4 : ( A - F  G  B - F ) = 0 )
  ( h5 : ( B - D  G  C - D ) = 0 )
  ( h6 : ( C - E  G  A - E ) = 0 )
  ( h7 : ( A - O  G  B - O ) ≠ 0 )
  ( h8 : ( B - O  G  C - O ) ≠ 0 )
  ( h9 : ( C - O  G  A - O ) ≠ 0 ) :
  ( (C - O G A - O)  * (B - D) = ((A - O G B - O))*(D - C) ) :=
begin
  -- Hypothesis numbers from Metamath proof.
  have h15 : D - O G A - O = 0,
  exact sigariz (A - O) (D - O)  h1,

  have h16: (A - B G D - B) - (O - B G D - B) = A - B G O - B,
  exact sigaradd  D A B O h15,

  have h18: B - O G A - O = A - B G O - B,
  exact sigarperm B A O,

  have h19: (A - B G D - B) - (O - B G D - B) = B - O G A - O,
  rw [h16,h18],

  have h20: ((A - B G D - B) - (O - B G D - B)) * (C - D) = (B - O G A - O) * (C - D),
  rw h19,

  have h30: ((A - B G D - B) - (O - B G D - B)) * (C - D) = (A - B G D - B) * (C - D) - (O - B G D - B) * (C - D),
  rw sub_mul,

  have h31:( ( ( B - O ) G ( A - O ) ) * ( C - D ) ) = ( ( ( ( A - B ) G ( D - B ) ) * ( C - D ) ) - ( ( ( O - B ) G ( D - B ) ) * ( C - D ) ) ),
  rw [← h30, h20],

  have h36: (A - B G D - B) * (C - D) = (A - C G D - C) * (B - D),
  exact @sharhght B C A D O h5,

  have h38: (O - B G D - B) * (C - D) = (O - C G D - C) * (B - D),
  exact @sharhght B C O D O h5,

  have h39: (A - B G D - B) * (C - D) - (O - B G D - B) * (C - D) = (A - C G D - C) * (B - D) - (O - C G D - C) * (B - D),
  rw [h38, h36],

  have h49: ((A - C G D - C) - (O - C G D - C)) * (B - D) = (A - C G D - C) * (B - D) - (O - C G D - C) * (B - D),
  rw sub_mul,

  have h51: ( ( ( A - C ) G ( D - C ) ) - ( ( O - C ) G ( D - C ) ) ) = ( ( A - C ) G ( O - C ) ),
  exact sigaradd D A C O h15,

  have h51: ( ( ( A - C ) G ( D - C ) ) - ( ( O - C ) G ( D - C ) ) ) = ( ( A - C ) G ( O - C ) ),
  exact sigaradd  D A C O h15,

  have h53: ( ( C - O ) G ( A - O ) ) = ( ( A - C ) G ( O - C ) ),
  exact sigarperm C A O,

  have h54: (A - C G D - C) - (O - C  G  D - C) = (C - O G A - O),
  rw [h51, h53],

  have h55:  ( (A - C G D - C) - (O - C  G  D - C) ) * ( B - D )  =  ( ( C - O ) G ( A - O ) ) * ( B - D ),
  rw h54,

  have h56: ( ( ( A - C ) G ( D - C ) ) * ( B - D ) ) - ( ( ( O - C ) G ( D - C ) ) * ( B - D)) = ( ( ( C - O ) G ( A - O ) ) * ( B - D ) ),
  rw [← h49, h55],

  have h57: ((( C - O ) G ( A - O)) * (B - D)) = (((B - O) G (A - O)) * (C - D)),
  rw [h31, h39, h56],

  have h60: ( B - O ) G ( A - O )  =  - ( ( A - O ) G ( B - O ) ),
  exact g_op_antisymm (B-O) (A-O),

  have h61: (B - O G A - O) * (C - D) = - (A - O G B - O) * (C - D),
  rw h60,

  have h65:( - ( ( A - O ) G ( B - O ) ) * ( C - D ) ) = ( ( ( A - O ) G ( B - O ) ) * -( C - D ) ),
  exact neg_mul_comm (A - O G B - O) (C - D),

  have h66:  - ( C - D ) = ( D - C ),
  simp,

  have h67: ( ( ( A - O ) G ( B - O ) ) * - ( C - D ) ) = ( ( ( A - O ) G ( B - O ) ) * ( D - C ) ),
  rw h66,

  have h68: ( -((A - O) G (B - O)) * (C - D)) = (((A - O) G (B - O)) * (D - C)),
  rw [h65, h67],

  rw [h57, h61, h68],
end

-- Top level theorem
theorem cevath  (A B C D E F O : ℂ)
  ( h1 : ( A - O  G  D - O ) = 0 )
  ( h2 : ( B - O  G  E - O ) = 0 )
  ( h3 : ( C - O  G  F - O ) = 0 )
  ( h4 : ( A - F  G  B - F ) = 0 )
  ( h5 : ( B - D  G  C - D ) = 0 )
  ( h6 : ( C - E  G  A - E ) = 0 )
  ( h7 : ( A - O  G  B - O ) ≠ 0 )
  ( h8 : ( B - O  G  C - O ) ≠ 0 )
  ( h9 : ( C - O  G  A - O ) ≠ 0 ) :
  ( (A - F)*(C - E)*(B - D) = (F - B)*(E - A)*(D - C) ) :=
begin

  have h53 :  ( (A - O G B - O) * (C - E) = ((B - O G C - O))*(E - A) ),
    exact cevathlem2 B C A E _ _ O h2 h3 h1 h5 h6 h4 h8 h9 h7,

  have h47 :  ( (B - O G C - O ) * (A - F) = ((C - O G A - O))*(F - B) ),
    exact cevathlem2 C A B F _ _ O h3 h1 h2 h6 h4 h5 h9 h7 h8,

  have h54 :  ( (C - O G A - O) * (B - D) = ((A - O G B - O))*(D - C) ),
    exact cevathlem2 A B C D E F O h1 h2 h3 h4 h5 h6 h7 h8 h9,

  exact cevathlem1 (B - O G C - O) (A - F)
                   (C - O G A - O) (F - B)
                   (A - O G B - O) (C - E)
                   (E - A) (B - D) (D - C)
                   h8 h7 h9 h47 h53 h54,
end