形式化数学实验室

/-- A **category** has objects, and for any two objects `X` and `Y` a type `Hom X Y` of
morphisms (arrows) from `X` to `Y`, together with
* an identity arrow `id X : Hom X X` for every object, and
* composition: from `f : Hom X Y` and `g : Hom Y Z` we get `comp f g : Hom X Z`,
such that identities do nothing (`id_comp`, `comp_id`) and composition is associative.

**Order of composition:** `comp f g` means "first `f`, then `g`" (diagrammatic order).
Mathlib uses the same order and writes it `f ≫ g`; ordinary function composition `g ∘ f`
lists the same two steps the other way round. -/
class Category.{v₁, u₁} (Obj : Type u₁) : Type (max u₁ (v₁ + 1)) where
  /-- The arrows from `X` to `Y`. -/
  Hom : Obj → Obj → Type v₁
  /-- The identity arrow on `X`. -/
  id : (X : Obj) → Hom X X
  /-- `comp f g`: first `f`, then `g`. -/
  comp : {X Y Z : Obj} → Hom X Y → Hom Y Z → Hom X Z
  /-- Doing nothing first changes nothing. -/
  id_comp : ∀ {X Y : Obj} (f : Hom X Y), comp (id X) f = f
  /-- Doing nothing afterwards changes nothing. -/
  comp_id : ∀ {X Y : Obj} (f : Hom X Y), comp f (id Y) = f
  /-- Composing three arrows does not depend on the bracketing. -/
  assoc : ∀ {W X Y Z : Obj} (f : Hom W X) (g : Hom X Y) (h : Hom Y Z),
    comp (comp f g) h = comp f (comp g h)

/-- **Types and functions form a category.** Objects are Lean types (in universe `u`),
arrows `X → Y` are functions, and `comp f g` is `g ∘ f` (first `f`, then `g`).
All three laws hold by `rfl` (see `Lumenary.Composition.comp_assoc` for why).

This is the category of Lean *types*, the type-theoretic analogue of the category **Set**
of sets and functions used in set-theoretic mathematics; Lean types are not ZFC sets, but
they play the same role here. (Mathlib analogue: `CategoryTheory.types`.) -/
instance typesCategory : Category.{u, u + 1} (Type u) where
  Hom X Y := X → Y
  id _ := fun x => x
  comp f g := g ∘ f
  id_comp _ := rfl
  comp_id _ := rfl
  assoc _ _ _ := rfl

/-- A **monoid**: a set `M` with an associative operation `mul` and a two-sided identity `one`.
We bundle the operation as data (a structure, not a class) so that one type can carry
several monoid structures, e.g. `Int` with `+` and `Int` with `×`.
(Mathlib analogue: the class `Monoid`, which writes `mul` as `*` and `one` as `1`.) -/
structure Monoid' (M : Type u) where
  mul : M → M → M
  one : M
  mul_assoc : ∀ a b c : M, mul (mul a b) c = mul a (mul b c)
  one_mul : ∀ a : M, mul one a = a
  mul_one : ∀ a : M, mul a one = a

/-- A **group**: a monoid in which every element `a` has an inverse `inv a` with
`mul (inv a) a = one`. Together with the monoid laws this one-sided law already implies
`mul a (inv a) = one` (proved below as `Group'.mul_inv_cancel`); Mathlib's `Group` uses the
same axiom, `inv_mul_cancel`. -/
structure Group' (G : Type u) extends Monoid' G where
  inv : G → G
  inv_mul_cancel : ∀ a : G, mul (inv a) a = one

/-- A left inverse is also a right inverse: `a · a⁻¹ = 1`.
Write `b` for `a⁻¹` and `c` for `b⁻¹`. Then
`a·b = 1·(a·b) = (c·b)·(a·b) = c·(b·(a·b)) = c·((b·a)·b) = c·(1·b) = c·b = 1`. -/
theorem Group'.mul_inv_cancel {G : Type u} (g : Group' G) (a : G) :
    g.mul a (g.inv a) = g.one := by
  generalize hb : g.inv a = b
  have hba : g.mul b a = g.one := by
    rw [← hb]
    exact g.inv_mul_cancel a
  have hcb : g.mul (g.inv b) b = g.one := g.inv_mul_cancel b
  calc g.mul a b
      = g.mul g.one (g.mul a b) := (g.one_mul _).symm
    _ = g.mul (g.mul (g.inv b) b) (g.mul a b) := by rw [hcb]
    _ = g.mul (g.inv b) (g.mul b (g.mul a b)) := g.mul_assoc _ _ _
    _ = g.mul (g.inv b) (g.mul (g.mul b a) b) := by rw [g.mul_assoc b a b]
    _ = g.mul (g.inv b) (g.mul g.one b) := by rw [hba]
    _ = g.mul (g.inv b) b := by rw [g.one_mul b]
    _ = g.one := hcb

/-- The integers under addition form a group: the operation is `+`, the identity is `0`,
and the inverse of `a` is `-a`. (We still call the operation `mul`; Mathlib instead has a
separate `AddGroup` with additive notation.) -/
def intAdd : Group' Int where
  mul a b := a + b
  one := 0
  inv a := -a
  mul_assoc := Int.add_assoc
  one_mul := Int.zero_add
  mul_one := Int.add_zero
  inv_mul_cancel := Int.add_left_neg

/-- The integers under multiplication form a monoid with identity `1`. -/
def intMul : Monoid' Int where
  mul a b := a * b
  one := 1
  mul_assoc := Int.mul_assoc
  one_mul := Int.one_mul
  mul_one := Int.mul_one

/-- …but the integers under multiplication are **not** a group: not every integer has a
multiplicative inverse. Indeed `2 · b = 1` has no integer solution
(`Lumenary.Integers.no_int_half`). -/
theorem int_mul_not_group : ¬ ∀ a : Int, ∃ b, a * b = 1 := by
  intro h
  obtain ⟨b, hb⟩ := h 2        -- `hb : 2 * b = 1`
  exact Lumenary.Integers.no_int_half ⟨b, hb⟩

/-- **A monoid is a category with one object.** Take a single object (the only element of
`Unit`); its arrows are the elements of `M`; composing arrows is multiplying; the identity
arrow is `one`. The category laws are exactly the monoid laws.
(Declared with `abbrev` so that Lean can unfold it when it is used as an instance.) -/
abbrev monoidAsCategory {M : Type u} (m : Monoid' M) : Category.{u, 0} Unit where
  Hom _ _ := M
  id _ := m.one
  comp f g := m.mul f g
  id_comp f := m.one_mul f
  comp_id f := m.mul_one f
  assoc f g h := m.mul_assoc f g h

/-- Given `f : Z → A` and `g : Z → B`, `pair f g : Z → A × B` sends `z` to `(f z, g z)`. -/
def pair (f : Z → A) (g : Z → B) : Z → A × B := fun z => (f z, g z)

/-- Following `pair f g` by the first projection gives back `f`. -/
theorem fst_comp_pair (f : Z → A) (g : Z → B) : Prod.fst ∘ pair f g = f := rfl

/-- Following `pair f g` by the second projection gives back `g`. -/
theorem snd_comp_pair (f : Z → A) (g : Z → B) : Prod.snd ∘ pair f g = g := rfl

/-- **Universal property of the product, uniqueness half.** Any `h : Z → A × B` whose two
coordinates are `f` and `g` *is* `pair f g`. Together with `fst_comp_pair` and
`snd_comp_pair` (existence), this says: maps into `A × B` are the same thing as pairs of
maps into `A` and into `B`. -/
theorem pair_unique {f : Z → A} {g : Z → B} (h : Z → A × B)
    (hf : Prod.fst ∘ h = f) (hg : Prod.snd ∘ h = g) : h = pair f g := by
  funext z
  show h z = (f z, g z)
  rw [← hf, ← hg]
  -- The goal is now `h z = ((h z).1, (h z).2)`: every pair is built from its coordinates.
  rfl

/-- A basket of fruit, written as a list. Lists keep their members in order. -/
def basket : List String := ["mango", "orange", "banana"]

/-- There is a mango in the basket: it is the very first thing in the list. -/
theorem mango_in_basket : "mango" ∈ basket :=
  List.Mem.head ["orange", "banana"]

/-- The basket holds three pieces of fruit. Lean counts them itself, so `rfl` is enough. -/
theorem basket_count : basket.length = 3 := rfl

/-- For lists, order matters: `[1, 2]` and `[2, 1]` are different lists.
`decide` asks Lean to compare the two lists element by element. -/
theorem order_matters_for_lists : ([1, 2] : List Nat) ≠ [2, 1] := by decide

/-- …but `[1, 2]` and `[2, 1]` have exactly the same members. As *sets* they would be equal;
as *lists* they are not (see `order_matters_for_lists`). -/
theorem same_members : ∀ x : Nat, x ∈ [1, 2] ↔ x ∈ [2, 1] := by
  intro x
  -- Being in a list means being equal to one of its entries:
  -- `x ∈ [1, 2]` unfolds to `x = 1 ∨ x = 2`, and `x ∈ [2, 1]` to `x = 2 ∨ x = 1`.
  simp only [List.mem_cons, List.not_mem_nil, or_false]
  -- "or" does not care about order.
  exact Or.comm

/-- The empty list has no members at all. -/
theorem nothing_in_empty : ∀ x : String, x ∉ ([] : List String) := by
  intro x h
  -- A proof of `x ∈ []` would have to come from one of the ways of building membership,
  -- but none of them produces an empty list, so there is no case left to consider.
  cases h

/-- Composition is **associative**: `h ∘ (g ∘ f) = (h ∘ g) ∘ f`.

Why does `rfl` prove it? By definition `(g ∘ f) = fun x => g (f x)`. Unfolding the
definition on both sides, each one becomes `fun x => h (g (f x))` — literally the same
function. Lean accepts `rfl` ("both sides are the same by definition") because its kernel
unfolds definitions and simplifies `(fun x => …) a` automatically. -/
theorem comp_assoc (f : α → β) (g : β → γ) (h : γ → δ) : h ∘ (g ∘ f) = (h ∘ g) ∘ f := rfl

/-- Doing nothing first changes nothing: `id ∘ f = f`. Both sides send `x` to `f x`, and
Lean identifies `fun x => f x` with `f` (η-conversion), so `rfl` works. -/
theorem id_comp (f : α → β) : id ∘ f = f := rfl

/-- Doing nothing afterwards changes nothing: `f ∘ id = f`. -/
theorem comp_id (f : α → β) : f ∘ id = f := rfl

/-- A composite of injective functions is injective.
If `g (f a) = g (f b)`, injectivity of `g` gives `f a = f b`, and then injectivity of `f`
gives `a = b`. (Core analogue: `Function.Injective.comp`.) -/
theorem injective_comp {f : α → β} {g : β → γ} (hg : Injective g) (hf : Injective f) :
    Injective (g ∘ f) := by
  intro a b h
  -- `h : g (f a) = g (f b)`
  have hfab : f a = f b := hg h
  exact hf hfab

/-- A composite of surjective functions is surjective.
To hit `c`, first find `b` with `g b = c`, then `a` with `f a = b`; then `g (f a) = c`.
(Core analogue: `Function.Surjective.comp`.) -/
theorem surjective_comp {f : α → β} {g : β → γ} (hg : Surjective g) (hf : Surjective f) :
    Surjective (g ∘ f) := by
  intro c
  obtain ⟨b, hb⟩ := hg c      -- `hb : g b = c`
  obtain ⟨a, ha⟩ := hf b      -- `ha : f a = b`
  refine ⟨a, ?_⟩
  show g (f a) = c
  rw [ha, hb]

/-- A composite of bijections is a bijection: combine the two previous results.
(Mathlib analogue: `Function.Bijective.comp`.) -/
theorem bijective_comp {f : α → β} {g : β → γ} (hg : Bijective g) (hf : Bijective f) :
    Bijective (g ∘ f) :=
  ⟨injective_comp hg.1 hf.1, surjective_comp hg.2 hf.2⟩

/-- Composition is **not commutative**: "double, then add 1" differs from
"add 1, then double". At `0` the first gives `1` and the second gives `2`. -/
theorem comp_not_comm :
    (fun n : Int => n + 1) ∘ (fun n : Int => 2 * n) ≠ (fun n : Int => 2 * n) ∘ (fun n : Int => n + 1) := by
  intro h
  -- Evaluate both sides at `0`.
  have h0 : (2 * 0 + 1 : Int) = 2 * (0 + 1) := congrFun h 0
  -- But `2 * 0 + 1 = 1` and `2 * (0 + 1) = 2`.
  exact absurd h0 (by decide)

/-- A function is **bijective** when it is both injective and surjective: every element of
the target is hit by exactly one input. -/
def Bijective (f : α → β) : Prop := Injective f ∧ Surjective f

/-- `n ↦ 2n + 1` is injective: if `2a + 1 = 2b + 1`, subtract 1 and divide by 2. -/
theorem injective_two_mul_add_one : Injective (fun n : Int => 2 * n + 1) := by
  intro a b h
  -- `h : 2 * a + 1 = 2 * b + 1`
  have h1 : 2 * a = 2 * b := (Int.add_left_inj 1).mp h      -- subtract 1
  exact Int.eq_of_mul_eq_mul_left (by decide) h1           -- divide by 2 (and 2 ≠ 0)

/-- `n ↦ n²` is **not** injective on the integers: `1² = (-1)²` but `1 ≠ -1`. -/
theorem not_injective_square : ¬ Injective (fun n : Int => n * n) := by
  intro h
  have h1 : (1 : Int) = -1 := h (by decide)   -- the hypothesis needed is `1 * 1 = -1 * -1`
  exact absurd h1 (by decide)

/-- `n ↦ n + 1` is surjective on the integers: to hit `y`, start from `y - 1`. -/
theorem surjective_add_one : Surjective (fun n : Int => n + 1) := by
  intro y
  exact ⟨y - 1, Int.sub_add_cancel y 1⟩

/-- `n ↦ 2n` is **not** surjective on the integers: nothing is sent to `1`, because there is
no integer half (`Lumenary.Integers.no_int_half`). -/
theorem not_surjective_two_mul : ¬ Surjective (fun n : Int => 2 * n) := by
  intro h
  obtain ⟨x, hx⟩ := h 1          -- `hx : 2 * x = 1`
  exact Lumenary.Integers.no_int_half ⟨x, hx⟩

/-- Negation `n ↦ -n` is a bijection of the integers (it is its own inverse). -/
theorem bijective_neg : Bijective (fun n : Int => -n) := by
  constructor
  · -- Injective: from `-a = -b`, negate both sides.
    intro a b h
    exact Int.neg_inj.mp h
  · -- Surjective: `-(-y) = y`.
    intro y
    exact ⟨-y, Int.neg_neg y⟩

/-- The **graph** of `f`: the set of pairs `(a, b)` with `f a = b`, written as a predicate on
pairs (in `Lumenary.Sets` this is a `Set (α × β)`). In set theory a function *is* such a set
of pairs. -/
def graph (f : α → β) : α × β → Prop := fun p => f p.1 = p.2

/-- A graph is **functional**: each input `a` is paired with `f a`, and with nothing else. -/
theorem graph_functional (f : α → β) (a : α) :
    graph f (a, f a) ∧ ∀ b, graph f (a, b) → b = f a := by
  constructor
  · -- `graph f (a, f a)` says `f a = f a`.
    rfl
  · intro b h
    -- `h : f a = b`
    exact Eq.symm h

/-- Every integer cancels with its negative: `a + (-a) = 0`.
This applies core Lean's `Int.add_right_neg`. -/
theorem add_neg_cancel (a : Int) : a + -a = 0 := Int.add_right_neg a

/-- In the integers, every number has an additive inverse: some `b` with `a + b = 0`.
The witness is `-a`. -/
theorem add_inverse_exists : ∀ a : Int, ∃ b, a + b = 0 := by
  intro a
  exact ⟨-a, add_neg_cancel a⟩

/-- In the natural numbers there is no additive inverse of `1`: no `n` with `1 + n = 0`.
This is why we extend the natural numbers to the integers. -/
theorem nat_no_additive_inverse : ¬ ∃ n : Nat, 1 + n = 0 := by
  intro ⟨n, h⟩
  -- `1 + n` is the successor `n + 1`, and a successor is never `0`.
  rw [Nat.add_comm] at h
  exact Nat.succ_ne_zero n h

/-- If `x + y = 0` then `x = -y`: an additive inverse is unique. Uses only `add_zero`,
associativity, `y + (-y) = 0` and `zero_add`. -/
theorem eq_neg_of_add_eq_zero {x y : Int} (h : x + y = 0) : x = -y :=
  calc x = x + 0 := (Int.add_zero x).symm
    _ = x + (y + -y) := by rw [Int.add_right_neg]
    _ = (x + y) + -y := (Int.add_assoc x y (-y)).symm
    _ = 0 + -y := by rw [h]
    _ = -y := Int.zero_add (-y)

/-- If `x + (-y) = 0` then `x = y`. Same idea as `eq_neg_of_add_eq_zero`, using `-y + y = 0`. -/
theorem eq_of_add_neg_eq_zero {x y : Int} (h : x + -y = 0) : x = y :=
  calc x = x + 0 := (Int.add_zero x).symm
    _ = x + (-y + y) := by rw [Int.add_left_neg]
    _ = (x + -y) + y := (Int.add_assoc x (-y) y).symm
    _ = 0 + y := by rw [h]
    _ = y := Int.zero_add y

/-- `a · 0 = 0`, derived from distributivity and cancellation:
`a·0 + a·0 = a·(0 + 0) = a·0 = a·0 + 0`, and cancelling `a·0` leaves `a·0 = 0`. -/
theorem mul_zero_from_distrib (a : Int) : a * 0 = 0 := by
  have h : a * 0 + a * 0 = a * 0 + 0 :=
    calc a * 0 + a * 0 = a * (0 + 0) := (Int.mul_add a 0 0).symm
      _ = a * 0 := by rw [Int.add_zero]
      _ = a * 0 + 0 := (Int.add_zero (a * 0)).symm
  exact Int.add_left_cancel h

/-- `(-a) · b = -(a · b)`, from distributivity:
`(-a)·b + a·b = (-a + a)·b = 0·b = 0`, so `(-a)·b` is the additive inverse of `a·b`. -/
theorem neg_mul_from_distrib (a b : Int) : -a * b = -(a * b) := by
  have h : -a * b + a * b = 0 :=
    calc -a * b + a * b = (-a + a) * b := (Int.add_mul (-a) a b).symm
      _ = 0 * b := by rw [Int.add_left_neg]
      _ = b * 0 := Int.mul_comm 0 b
      _ = 0 := mul_zero_from_distrib b
  exact eq_neg_of_add_eq_zero h

/-- "Negative times negative is positive": `(-a) · (-b) = a · b`.
This version just applies core Lean's theorem `Int.neg_mul_neg`. Compare
`neg_mul_neg_from_axioms`, which proves the same statement from the ring axioms. -/
theorem neg_mul_neg_library (a b : Int) : -a * -b = a * b := Int.neg_mul_neg a b

/-- "Negative times negative is positive", proved the way a student would:
1. `(-a)(-b) + (-a)b = (-a)(-b + b) = (-a)·0 = 0`  (distributivity, then `-b + b = 0`);
2. `(-a)b = -(ab)`  (`neg_mul_from_distrib`);
3. so `(-a)(-b) + -(ab) = 0`, which forces `(-a)(-b) = ab`. -/
theorem neg_mul_neg_from_axioms (a b : Int) : -a * -b = a * b := by
  -- Step 1.
  have step1 : -a * -b + -a * b = 0 :=
    calc -a * -b + -a * b = -a * (-b + b) := (Int.mul_add (-a) (-b) b).symm
      _ = -a * 0 := by rw [Int.add_left_neg]
      _ = 0 := mul_zero_from_distrib (-a)
  -- Step 2.
  have step2 : -a * b = -(a * b) := neg_mul_from_distrib a b
  -- Step 3: substitute step 2 into step 1, then cancel.
  rw [step2] at step1
  exact eq_of_add_neg_eq_zero step1

/-- There is no integer `x` with `2 · x = 1`, so `2` has no multiplicative inverse in `Int`.
Reason: `2 · x` always leaves remainder `0` when divided by `2`, but `1` leaves remainder `1`. -/
theorem no_int_half : ¬ ∃ x : Int, 2 * x = 1 := by
  intro ⟨x, h⟩
  have hrem : (2 * x) % 2 = 1 % 2 := by rw [h]
  rw [Int.mul_emod_right] at hrem
  -- `hrem : 0 = 1 % 2`, i.e. `0 = 1`, which is false.
  exact absurd hrem (by decide)

/-- There is no integer `x` with `3 · x = 1`. Same argument as `no_int_half`, using
remainders on division by `3`. -/
theorem no_int_third : ¬ ∃ x : Int, 3 * x = 1 := by
  intro ⟨x, h⟩
  have hrem : (3 * x) % 3 = 1 % 3 := by rw [h]
  rw [Int.mul_emod_right] at hrem
  exact absurd hrem (by decide)

/-- The only integers with a multiplicative inverse are `1` and `-1`:
if `a · b = 1` then `a = 1` or `a = -1`.
Proof: take absolute values. `|a| · |b| = |a · b| = 1` in the natural numbers, which forces
`|a| = 1`; an integer with absolute value `1` is `1` or `-1`. -/
theorem int_units (a b : Int) (h : a * b = 1) : a = 1 ∨ a = -1 := by
  have habs : a.natAbs * b.natAbs = 1 := by
    rw [← Int.natAbs_mul, h]
    rfl
  have ha : a.natAbs = 1 := Nat.eq_one_of_mul_eq_one_right habs
  -- Every integer is `+|a|` or `-|a|`.
  cases Int.natAbs_eq a with
  | inl hpos => left; rw [hpos, ha]; rfl
  | inr hneg => right; rw [hneg, ha]; rfl

/-- On a 12-hour clock, 5 hours after 9 o'clock is 2 o'clock: `(9 + 5) mod 12 = 2`. -/
theorem clock_wraps : (9 + 5) % 12 = 2 := by decide

/-- Modulo 7, the number 3 has an inverse, namely 5: `3 · 5 = 15 = 2 · 7 + 1`. -/
theorem three_inv_mod_seven : (3 * 5) % 7 = 1 := by decide

/-- Modulo 4, the number 2 has **no** inverse: `2 · x` is always even, so it is never `1`
more than a multiple of 4. `decide` checks all four possibilities `x = 0, 1, 2, 3`. -/
theorem two_no_inv_mod_four : ∀ x : Fin 4, (2 * x.val) % 4 ≠ 1 := by decide

/-- Modulo 5 (a prime), every non-zero number has an inverse:
`1·1 = 1`, `2·3 = 6`, `3·2 = 6`, `4·4 = 16`, and each of these leaves remainder 1.
`decide` checks every `a` and searches for each `b`. -/
theorem inverses_mod_five : ∀ a : Fin 5, a.val ≠ 0 → ∃ b : Fin 5, (a.val * b.val) % 5 = 1 := by
  decide

/-- You may reduce before or after adding: `(a mod k + b mod k) mod k = (a + b) mod k`.
This applies core Lean's `Nat.add_mod`. -/
theorem mod_add_mod (a b k : Nat) : (a % k + b % k) % k = (a + b) % k :=
  (Nat.add_mod a b k).symm

/-- `ModEq k a b` ("`a ≡ b (mod k)`"): `a` and `b` leave the same remainder on division by `k`.
(Mathlib analogue: `Int.ModEq`, defined the same way.) -/
def ModEq (k a b : Int) : Prop := a % k = b % k

/-- Every integer is congruent to itself. -/
theorem modEq_refl (k a : Int) : ModEq k a a := rfl

/-- If `a ≡ b` then `b ≡ a`. -/
theorem modEq_symm {k a b : Int} (h : ModEq k a b) : ModEq k b a := Eq.symm h

/-- If `a ≡ b` and `b ≡ c` then `a ≡ c`: equal remainders chain together. -/
theorem modEq_trans {k a b c : Int} (h₁ : ModEq k a b) (h₂ : ModEq k b c) : ModEq k a c :=
  Eq.trans h₁ h₂

/-- Congruence modulo `k` is an **equivalence relation** (reflexive, symmetric, transitive).
Its equivalence classes are the "hours" on a `k`-hour clock. -/
theorem modEq_equivalence (k : Int) : Equivalence (ModEq k) :=
  ⟨modEq_refl k, modEq_symm, modEq_trans⟩

/-- A set of elements of `α` is a yes/no property of elements of `α`:
`A x` is the statement "`x` belongs to `A`". -/
def Set (α : Type u) : Type u := α → Prop

/-- `x ∈ A` means that `x` has the property `A`. -/
instance instMembership : Membership α (Set α) := ⟨fun A x => A x⟩

/-- `setOf p` is the set of all `x` with property `p`. We write it `{x | p x}` (notation below). -/
def setOf (p : α → Prop) : Set α := p

/-- Belonging to `{x | p x}` means having property `p` — true by definition. -/
theorem mem_setOf (p : α → Prop) (a : α) : a ∈ {x | p x} ↔ p a := Iff.rfl

/-- `A ⊆ B` ("`A` is a subset of `B`"): every member of `A` is a member of `B`.
(Mathlib states this with a strict-implicit `∀ ⦃x⦄`; we keep `x` explicit for readability.) -/
def Subset (A B : Set α) : Prop := ∀ x, x ∈ A → x ∈ B

/-- Lets us write `A ⊆ B` for `Subset A B`. -/
instance instHasSubset : HasSubset (Set α) := ⟨Subset⟩

/-- The union `A ∪ B`: everything in `A` *or* in `B` (or both). -/
def union (A B : Set α) : Set α := {x | x ∈ A ∨ x ∈ B}

/-- Lets us write `A ∪ B`. -/
instance instUnion : Union (Set α) := ⟨union⟩

/-- The intersection `A ∩ B`: everything in `A` *and* in `B`. -/
def inter (A B : Set α) : Set α := {x | x ∈ A ∧ x ∈ B}

/-- Lets us write `A ∩ B`. -/
instance instInter : Inter (Set α) := ⟨inter⟩

/-- The complement `Aᶜ`: everything (of type `α`) that is *not* in `A`. -/
def compl (A : Set α) : Set α := {x | x ∉ A}

/-- The empty set: nothing belongs to it. (The underscore in `_x` says the name is unused.) -/
def empty : Set α := {_x | False}

/-- Lets us write `∅` for the empty set. -/
instance instEmptyCollection : EmptyCollection (Set α) := ⟨empty⟩

/-- The universal set: everything of type `α` belongs to it. -/
def univ : Set α := {_x | True}

/-- The Cartesian product `A ×ˢ B`: all pairs `(a, b)` with `a ∈ A` and `b ∈ B`. -/
def prod (A : Set α) (B : Set β) : Set (α × β) := {p | p.1 ∈ A ∧ p.2 ∈ B}

/-- `x ∈ A ∪ B` means `x ∈ A ∨ x ∈ B`. -/
theorem mem_union (x : α) (A B : Set α) : x ∈ A ∪ B ↔ x ∈ A ∨ x ∈ B := Iff.rfl

/-- `x ∈ A ∩ B` means `x ∈ A ∧ x ∈ B`. -/
theorem mem_inter (x : α) (A B : Set α) : x ∈ A ∩ B ↔ x ∈ A ∧ x ∈ B := Iff.rfl

/-- `x ∈ Aᶜ` means `x ∉ A`. -/
theorem mem_compl (x : α) (A : Set α) : x ∈ Aᶜ ↔ x ∉ A := Iff.rfl

/-- **Extensionality.** Two sets are equal when they have exactly the same members.
This is where sets differ from lists: order and repetition are invisible.
The proof uses function extensionality and propositional extensionality, so the axiom
report lists `propext` and `Quot.sound` (from which `funext` is derived). -/
theorem ext {A B : Set α} (h : ∀ x, x ∈ A ↔ x ∈ B) : A = B :=
  funext fun x => propext (h x)

/-- Every set is a subset of itself. -/
theorem subset_refl (A : Set α) : A ⊆ A := by
  intro x hx
  exact hx

/-- Inclusion is transitive: if `A ⊆ B` and `B ⊆ C` then `A ⊆ C`. -/
theorem subset_trans {A B C : Set α} (hAB : A ⊆ B) (hBC : B ⊆ C) : A ⊆ C := by
  intro x hxA
  have hxB : x ∈ B := hAB x hxA
  exact hBC x hxB

/-- The empty set is a subset of every set: there is no member of `∅` that could fail to be
in `A`. (Logicians say the statement is *vacuously* true.) -/
theorem empty_subset (A : Set α) : ∅ ⊆ A := by
  intro x hx
  -- `hx : x ∈ ∅` is a proof of `False`, and from `False` anything follows.
  exact False.elim hx

/-- Every set is a subset of the universal set. -/
theorem subset_univ (A : Set α) : A ⊆ univ := by
  intro x _
  -- `x ∈ univ` is just `True`.
  trivial

/-- `A ∩ B ⊆ A`: whatever is in both sets is, in particular, in the first one. -/
theorem inter_subset_left (A B : Set α) : A ∩ B ⊆ A := by
  intro x hx
  -- `hx : x ∈ A ∧ x ∈ B`; keep the left half.
  exact hx.1

/-- `A ∩ B ⊆ B`: whatever is in both sets is, in particular, in the second one. -/
theorem inter_subset_right (A B : Set α) : A ∩ B ⊆ B := by
  intro x hx
  -- `hx : x ∈ A ∧ x ∈ B`; keep the right half.
  exact hx.2

/-- `A ⊆ A ∪ B`: anything in `A` is in `A` or in `B`. -/
theorem subset_union_left (A B : Set α) : A ⊆ A ∪ B := by
  intro x hx
  exact Or.inl hx

/-- Union is commutative: `A ∪ B = B ∪ A`. -/
theorem union_comm (A B : Set α) : A ∪ B = B ∪ A := by
  apply ext
  intro x
  constructor
  · intro h
    -- `h : x ∈ A ∨ x ∈ B`, and "or" can be swapped.
    exact Or.symm h
  · intro h
    exact Or.symm h

/-- Intersection is commutative: `A ∩ B = B ∩ A`. -/
theorem inter_comm (A B : Set α) : A ∩ B = B ∩ A := by
  apply ext
  intro x
  constructor
  · intro h
    -- `h : x ∈ A ∧ x ∈ B`, and "and" can be swapped.
    exact And.symm h
  · intro h
    exact And.symm h

/-- Intersection distributes over union: `A ∩ (B ∪ C) = (A ∩ B) ∪ (A ∩ C)`.
(Mathlib analogue: `Set.inter_union_distrib_left`.) -/
theorem inter_union_distrib (A B C : Set α) : A ∩ (B ∪ C) = (A ∩ B) ∪ (A ∩ C) := by
  apply ext
  intro x
  constructor
  · -- If `x ∈ A` and `x` is in `B` or `C`, look at which one.
    intro ⟨hA, hBC⟩
    cases hBC with
    | inl hB => exact Or.inl ⟨hA, hB⟩
    | inr hC => exact Or.inr ⟨hA, hC⟩
  · -- Either way round, `x ∈ A`, and `x` is in `B` or in `C`.
    intro h
    cases h with
    | inl hAB => exact ⟨hAB.1, Or.inl hAB.2⟩
    | inr hAC => exact ⟨hAC.1, Or.inr hAC.2⟩

/-- **De Morgan's law** for unions: `(A ∪ B)ᶜ = Aᶜ ∩ Bᶜ`.
Not being in `A ∪ B` means being in neither set. This proof is constructive: it does not
use the law of excluded middle. -/
theorem compl_union (A B : Set α) : (A ∪ B)ᶜ = Aᶜ ∩ Bᶜ := by
  apply ext
  intro x
  constructor
  · intro h
    -- `h : ¬ (x ∈ A ∨ x ∈ B)`. If `x` were in `A`, it would be in `A ∪ B`; same for `B`.
    exact ⟨fun hA => h (Or.inl hA), fun hB => h (Or.inr hB)⟩
  · intro ⟨hnA, hnB⟩ hAB
    -- `x` is in `A` or in `B`, and both cases contradict what we know.
    cases hAB with
    | inl hA => exact hnA hA
    | inr hB => exact hnB hB

/-- **De Morgan's law** for intersections: `(A ∩ B)ᶜ = Aᶜ ∪ Bᶜ`.
The direction `(A ∩ B)ᶜ ⊆ Aᶜ ∪ Bᶜ` needs **classical logic**: knowing only that `x` is not in
both sets, we must still decide *which* set it misses. We use excluded middle
(`Classical.em`), so the axiom report for this theorem includes `Classical.choice`. -/
theorem compl_inter (A B : Set α) : (A ∩ B)ᶜ = Aᶜ ∪ Bᶜ := by
  apply ext
  intro x
  constructor
  · intro h
    -- `h : ¬ (x ∈ A ∧ x ∈ B)`. Either `x ∈ A` or not (excluded middle).
    cases Classical.em (x ∈ A) with
    | inl hA =>
      -- Then `x` cannot also be in `B`.
      exact Or.inr (fun hB => h ⟨hA, hB⟩)
    | inr hnA => exact Or.inl hnA
  · intro h ⟨hA, hB⟩
    cases h with
    | inl hnA => exact hnA hA
    | inr hnB => exact hnB hB

/-- A pair `(a, b)` is in `A ×ˢ B` exactly when `a ∈ A` and `b ∈ B`. True by definition. -/
theorem mem_prod (a : α) (b : β) (A : Set α) (B : Set β) :
    (a, b) ∈ A ×ˢ B ↔ a ∈ A ∧ b ∈ B :=
  Iff.rfl