example(a b c d e f:ℝ)(h:b*c=e*f):a*b*c*d=a*e*f*d:=by
  calc
    a * b * c * d = a * (b * c) * d := by ring
    _ = a * (e * f) * d := by rw [h]
    _ = a * e * f * d := by ring
example(a b c d:ℝ)(hyp:c=b*a-d)(hyp':d=a*b):c=0:=by
  calc 
    c = b * a - d := hyp
    _ = a * b - d := by rw [mul_comm b a]
    _ = 0:= by simp [hyp']
example(a b:ℝ):(a+b)*(a-b)=a^2-b^2:=by

  calc
    (a+b)*(a-b)=a*a-a*b+b*a-b*b:=by ring
    _=a^2-b^2:=by ring
theorem sum_of_first_n_odd_integers(n:ℕ):(∑ i in Finset.range n ,(2*i+1))=(n^2):=by
  induction n with
  | zero => simp
  | succ n ih =>
    rw[Finset.range_succ]
    simp
    rw[ih]
    ring_nf