theorem and_self_idem (p : Prop) : (p ∧ p) ↔ p := by tauto

-- The only solution to xᵃ = yᵇ + 1 with x,y,a,b > 1 is 3² = 2³ + 1. theorem catalan_conjecture (x y a b : ℕ) (hx : 1 < x) (hy : 1 < y) (ha : 1 < a) (hb : 1 < b) (h : x ^ a = y ^ b + 1) : x = 3 ∧ a = 2 ∧ y = 2 ∧ b = 3 := sorry

-- There are infinitely many prime numbers. theorem inf_primes : ∀ n : ℕ, ∃ p : ℕ, n < p ∧ Nat.Prime p := fun n => (Nat.exists_infinite_primes (n + 1)).elim fun p hp => ⟨p, Nat.lt_of_...