Validation of Lean

Example of valid input: 
import Mathlib.Data.Real.Basic

theorem add_to_both_sides (a b c : Real) : a = b <-> a + c = b + c := by
  exact (add_right_cancel_iff).symm

#print axioms add_to_both_sides
which produces 
'add_to_both_sides' depends on axioms: [propext, Classical.choice, Quot.sound]
after about 30 seconds.