some Lean maths puzzles

puzzles.lean

import tactic
import data.real.basic
/-

# Some puzzles.

1) (easy logic). If `P`, `Q` and `R` are true-false statements, then show
that `(P → (Q → R)) → ((P → Q) → (P → R))` (where `→` means "implies")

2) (group theory) If `G` is a group such that `∀ g, g^2 = 1`
then `G` is abelian.

3) (analysis) A set of reals has at most one least upper bound.

4) (linear orders) If `(a, b]` denotes the set of reals `x` with `a < x ≤ b` then
prove `[a,b) ∪ [b,c) ∪ [c,a) = [b,a) ∪ [c,b) ∪ [a,c)`

5) (group theory) If `G` is a group and `g : G`, and if `g^a = g^b = 1` with `a`
and `b` integers, then `g^(gcd a b) = 1`

6) (number theory) Prove there's a nontrivial solution to `a^2-94b^2=1` in integers.

7) (analysis) : If `aₙ → l` and `cₙ → l` and `aₙ ≤ bₙ ≤ cₙ` then `bₙ → l` 


-/

section Q1

variables (P Q R : Prop)

example : (P → (Q → R)) → ((P → Q) → (P → R)) :=
begin
  sorry
end

end Q1

section Q2

variables (G : Type) [group G]

example : (∀ (g : G), g^2 = 1) → (∀ g h : G, g * h = h * g) :=
begin
  sorry
end

end Q2

section Q3

/-
def upper_bounds (S : set ℝ) : set ℝ := { b | ∀s ∈ S, s ≤ b }
def lower_bounds (S : set ℝ) : set ℝ := { b | ∀s ∈ S, b ≤ s }
def is_least (S : set ℝ) (l : ℝ) : Prop := l ∈ S ∧ l ∈ lower_bounds S
def is_lub (S : set ℝ) (l : ℝ) : Prop := is_least (upper_bounds S) l
-/

/-- A set has at most one least upper bound -/
example (S : set ℝ) (a b : ℝ) (ha : is_lub S a) (hb : is_lub S b) : a = b :=
begin
  sorry
end

end Q3

section Q4

variables (a b c : ℝ)

open set

example : Ico a b ∪ Ico b c ∪ Ico c a = Ico b a ∪ Ico c b ∪ Ico a c :=
begin
  sorry
end

end Q4

section Q5

variables (G : Type) [group G] (a b : ℤ) (g : G)

open int

example : g^a = 1 ∧ g^b = 1 → g^(gcd a b) = 1 :=
begin
  sorry
end

end Q5

section Q6

example : ∃ a b : ℤ, b ≠ 0 ∧ a^2 - 94*b^2 = 1 :=
begin
  sorry
end

end Q6

section Q7

-- l is the limit of aₙ if ∀ ε>0 ∃ N, n ≥ N → |aₙ - l| < ε
def is_limit (a : ℕ → ℝ) (l : ℝ) :=
∀ ε > 0, ∃ N, ∀ n, N ≤ n → abs (a n - l) < ε

example (a b c : ℕ → ℝ) (h : ∀ n, a n ≤ b n ∧ b n ≤ c n) (l : ℝ)
  (ha : is_limit a l) (hc : is_limit c l) : is_limit b l :=
begin
  sorry
end

end Q7