1. 1
2. 2
3. 3
4. 4
5. 5
6. 6
7. 7
8. 8
9. 9
10. 10
11. 11
12. 12
13. 13
14. 14
15. 15
16. 16
17. 17
18. 18
19. 19
20. 20
21. 21
22. 22
23. 23
24. 24
25. 25
26. 26
27. 27
28. 28
29. 29
30. 30
31. 31

-- https://b-mehta.github.io/formalising-mathematics-notes/Part_1/the_axiom_of_choice.html

import Mathlib
-- import Mathlib.Analysis.Complex.Polynomial -- import proof of fundamental theorem of algebra

open Polynomial -- so I can use notation ℂ[X] for polynomial rings
                -- and so I can write `X` and not `polynomial.X`

suppress_compilation -- because everything is noncomputable

def f : ℂ[X] := X^5 + X + 37 -- a random polynomial

lemma f_degree : degree f = 5 := by
  unfold f
  compute_degree -- polynomial degree computing tactic
  norm_num
  trivial

theorem f_has_a_root : ∃ (z : ℂ), f.IsRoot z := by
  apply Complex.exists_root -- the fundamental theorem of algebra
  -- ⊢ 0 < degree f
  rw [f_degree]
  -- ⊢ 0 < 5
  norm_num

-- let z be a root of f (getting data from a theorem)
def z : ℂ := Classical.choose f_has_a_root

-- proof that z is a root of f (the "API" for `Classical.choose`)
theorem z_is_a_root_of_f : f.IsRoot z := by
  exact Classical.choose_spec f_has_a_root