import Mathlib

open Function Set

example {A B : Type _ } (f : A → B) : f.Injective ↔ ∃ g : B → A, g ∘ f = id := by
  constructor
  · intro h
    -- hard.
    sorry
  · intro h
    rcases h with ⟨g, h⟩
    unfold Injective
    intro a b hab
    rw [←id_eq a, ←id_eq b]
    rw [← h]
    rw [comp_apply]
    rw [hab]
    simp


lemma singleton_mem_powerset
    {U : Type _} {M : Set U} {x : U} (h : x ∈ M) :
    {x} ∈ 𝒫 M := by
  rw [mem_powerset_iff, singleton_subset_iff]
  assumption

example
    {U : Type _} (M : Set U) :
    {A : Set U // A ∈ 𝒫 M} = {A ∈ 𝒫 M | True} := by
  simp_rw [coe_setOf, and_true]

example
    {U : Type _} (M : Set U) :
    {A : Set U // A ∈ 𝒫 M} = 𝒫 M := by
  rfl

example
    {U : Type _} (M : Set U) :
    {x : U // x ∈ M} = M := by
  rfl

example
    {U : Type _} (M : Set U) :
    ∃ (f : M → 𝒫 M), Injective f := by
  use fun x ↦ ⟨ _, singleton_mem_powerset x.prop ⟩
  intro a b hab
  simp at hab
  rw [Subtype.val_inj] at hab
  assumption

instance {U : Type _} {M : Set U} : Membership ↑M ↑(𝒫 M) :=
{ mem := fun x A ↦ x.1 ∈ A.1 }

instance {U : Type _} {M : Set U} : Membership U (Set ↑M) :=
{ mem := fun x A ↦ _ }


example
    {U : Type _} {M : Set U} (h_empty : M.Nonempty)
    (f : {x : U // x ∈ M} → {A : Set U // A ∈ 𝒫 M}):
    ¬ Surjective f := by
  unfold Surjective
  push_neg
  --by_contra h_sur
  let B : Set M := {x : M | x ∉ (f x)}
  use ⟨B, sorry⟩
  intro ⟨a, ha⟩
  sorry
  -- Too hard?

#check singleton_mem_powerset
#check Subtype.val_inj



-- These are fun exercises for prime.
example (x : ℕ) : 0 < x ↔ 1 ≤ x := by
  rfl

lemma le_cancel_left (n x : ℕ) (h : x ≠ 0): n ≤ n * x := by
  induction n
  simp
  simp
  rw [← zero_lt_iff] at h
  assumption


example (n m : ℕ) (g : m ≠ 0) (h : n ∣ m) : n ≤ m := by
  rcases h with ⟨x, hx⟩
  rw [hx]
  apply le_cancel_left
  by_contra k
  rw [k] at hx
  simp at hx
  rw [hx] at g
  contradiction