import Mathlib.Tactic

open Set
/-
# Conjuntos y tipos finitos

En Lean hay varias nociones de finitud (en parte porque en las propias matemáticas también las hay):
  - Tipos finitos (`Fintype`)
  - Conjuntos finitos (`Finset`)
  - Tipos ordinarios que tienen la propiedad de ser finitos (`Finite`)
  - Conjuntos ordinarios que tienen la propiedad de ser finitos (`Set.Finite`)
  - ...

De momento vamos a centrarnos sólo en los dos últimos casos, es decir, vamos a trabajar
con conjuntos o tipos como antes, pero usaremos en ocasiones la propiedad de que son finitos

Que un tipo sea finito quiere decir que es biyectivo con {0,1,..,n} para algún n. Que un
conjunto sea finito quiere decir que su correspondiente tipo sea finito.
-/


-- un conjunto es finito si y sólo si su tipo correspondiente es finito

lemma tipo_finito_sii_conjunto_finito (X : Type) (S : Set X) : Finite ↥S  ↔ Set.Finite S  := by
  exact finite_coe_iff


-- un conjunto es finito si y sólo si es biyectivo con {0,1,...,n} para algún natural n

lemma Set_Finite_iff_bijective_fin_n (X : Type) ( S : Set X) : Set.Finite S ↔ ∃ n : ℕ, ∃ (a :  ↥S → (Fin n)), Function.Bijective a := by
  rw  [← tipo_finito_sii_conjunto_finito]
  fconstructor
  . intro h
    cases' h with n hn
    use n
    use hn
    exact Equiv.bijective hn
  . intro h
    cases' h with n hn
    cases' hn with a ha
    fconstructor
    · use n
    · apply Equiv.ofBijective a ha



/-
Una propiedad importante es que los conjuntos finitos tienen principio de inducción:
si una propiedad es cierta para el conjunto vacío, y si es cierta para un conjunto finito
entonceses cierta para el conjunto obtenido añadiendo un elemento, entonces es cierta
para cualquier conjunto finito.

Veamos el ejemplo de lo que ocurre con la unión de cerrados en una topología
-/

example
  (X : Type)
  (P : Set X → Prop)
  (hu : ∀ A B : Set X, P A  → P B → P  (A ∪ B))
  (S : Set (Set X))
  (hSI : ∀ x ∈ S, P x)
  (h0 : P ∅ )
  (hfin : Set.Finite S) :
  P (⋃₀ S) := by

  revert hSI   -- esto es necesario porque queremos "arrastrar" la hipótesis a la inducción
  induction' S, hfin  using Set.Finite.induction_on with a T ha hT huT hSI
  . simp only [Set.sUnion_empty]
    intro h
    exact h0
  . simp only [Set.sUnion_insert]
    intro h
    apply hu
    . apply h
      left
      rfl
    · apply huT
      intro x hx
      apply h
      right
      exact hx

-- Para ver el recíproco, símplemente hay que ver que los conjuntos de dos elementos son finitos


example (X : Type) (a b : X) : Set.Finite ({a, b} : Set X) := by
  exact toFinite {a, b}

-- y que la unión de dos conjuntos es lo mismo que la unión del conjunto formado por ambos

example (X : Type) (a b : Set X) : a ∪ b = ⋃₀ ({a , b} : Set (Set X)) := by
  rw [sUnion_insert]
  rw [sUnion_singleton]


/-
# Ejercicio

Demuestra que todo conjunto finito  no vacío de los naturales tiene un elemento maximal

(puede ser útil la ráctica `linarith`, que intenta demostrar (des)igualdades que se puedan deducir
mediante operaciones lineales)
-/

example ( S : Set ℕ ) (hf : Set.Finite S) : S ≠ ∅ → ∃ m ∈ S, ∀ n ∈ S, n ≤ m := by
  sorry