Arrow's theorem is a basic result in social choice theory which has several simple proofs. (For three proofs see this paper: Three Brief Proofs of Arrow's Impossibility Theorem by J. Geanakoplos)
It also has a few complicated proofs: The paper by Tang, Pingzhong and Lin, Fangzhen Computer-aided proofs of Arrow's and other impossibility theorems, Artificial Intelligence 173 (2009), no. 11, 1041–1053. Gives an inductive proof based on rather complicted inductive step and a computerized check for the base case. The paper by Yuliy Baryshnikov, Unifying impossibility theorems: a topological approach. Adv. in Appl. Math. 14 (1993), 404–415, gives a proof based on algebraic topology. My paper: A Fourier-theoretic perspective on the Condorcet paradox and Arrow's theorem. Adv. in Appl. Math. 29 (2002), 412–426, gives a fairly complicated Fourier-theoretic proof but only to a special case of the theorem.
(A complicated proof to a related theorem is by Shelah, Saharon, On the Arrow property, Adv. in Appl. Math. 34 (2005), 217–251.)
