I need to prove the following theorems using Lean theorem prover (which is a online software tool).

I need to prove the following theorems using Lean theorem prover (which is a online software tool).

Do the following in Lean, and submit your successful input typed

1. Express the claim that there are infinitely many primes.
2. Prove that the sum of two evens is even by just applying aven_plus_aven.
3. Prove that for any predicates, (∀ x, p x) ∨ (∀ x, q x) → ∀ x, p x ∨ q x.
4. Prove that every integer divides 0. (Using the definition of divides.)
5. Complete the Lean proof of odd_plus_odd, modifying the calculational proof part.