Setup for Con(NF) proof in lean: https://randall-holmes.github.io/Nfproof/newattempt.pdf

con_nf.lean

import set_theory.cofinality
import order.symm_diff
import group_theory.subgroup.basic
import group_theory.group_action.basic

noncomputable theory
open_locale cardinal classical

universes u v

namespace ZFA

inductive pSet (A : Type v) : Type (max (u+1) v)
| atom : A → pSet
| range {α : Type u} (A : α → pSet) : pSet

namespace pSet
def equiv {A} : pSet A → pSet A → Prop
| (atom a) y := atom a = y
| x (atom a) := x = atom a
| (range A) (range B) :=
  (∀ a, ∃ b, equiv a (B b)) ∧ (∀ b, ∃ a, equiv a (B b))

def map {A B} (f : A → B) : pSet A → pSet B
| (atom a) := atom (f a)
| (range A) := range (λ x, map (A x))

instance (A : Type*) : mul_action (equiv.perm A) (pSet A) :=
{ smul := λ π x, x.map π, one_smul := sorry, mul_smul := sorry }

def atoms {A} : pSet A := range atom

protected def empty {A} : pSet A := @range A pempty (λ e, match e with end)

instance (A) : has_emptyc (pSet A) := ⟨pSet.empty⟩

def type {A} : pSet A → Type u
| (atom a) := pempty
| (@range _ α A) := α

def func {A} : Π (x : pSet A), x.type → pSet A
| (atom a) := pempty.elim
| (range A) := A

protected def insert {A} (x y : pSet A) : pSet A :=
range (λ o, option.rec x y.func o)

instance (A) : has_insert (pSet A) (pSet A) := ⟨pSet.insert⟩

instance (A) : has_singleton (pSet A) (pSet A) := ⟨λ s, insert s ∅⟩

instance (A) : is_lawful_singleton (pSet A) (pSet A) := ⟨λ _, rfl⟩

def pair {A} (x y : pSet A) : pSet A := {{x}, {x, y}}

def powerset {A} (x : pSet A) : pSet A :=
range (λ p : set x.type, range (λ y : {a // p a}, x.func y))

protected def sep {A} (x : pSet A) (p : pSet A → Prop) : pSet A :=
range (λ y : {a // p (x.func a)}, x.func y)

def image {A} (f : pSet A → pSet A) (c : pSet A) : pSet A :=
range (λ a, f (c.func a))

end pSet

def Set (A) : Type* := quotient ⟨@pSet.equiv A, sorry⟩
def Set.mk {A} : pSet A → Set A := quotient.mk'

def Set.map {A B} (f : A → B) (x : Set A) : Set B :=
quotient.lift_on' x (λ x, Set.mk (x.map f)) sorry

instance (A : Type*) : mul_action (equiv.perm A) (Set A) :=
{ smul := λ π x, x.map π, one_smul := sorry, mul_smul := sorry }

protected def empty {A} : Set A := Set.mk ∅

instance (A) : has_emptyc (Set A) := ⟨ZFA.empty⟩

protected def insert {A} (x y : Set A) : Set A :=
quotient.lift_on₂' x y (λ x y, Set.mk (x.insert y)) sorry

instance (A) : has_insert (Set A) (Set A) := ⟨ZFA.insert⟩

instance (A) : has_singleton (Set A) (Set A) := ⟨λ s, insert s ∅⟩

instance (A) : is_lawful_singleton (Set A) (Set A) := ⟨λ _, rfl⟩

def Set.is_bijection {A} (F x y : Set A) : Prop :=
∃ α (f g : α → pSet A),
  function.injective (λ a, Set.mk (f a)) ∧ x = Set.mk (pSet.range f) ∧
  function.injective (λ a, Set.mk (g a)) ∧ y = Set.mk (pSet.range g) ∧
  F = Set.mk (pSet.range (λ a, (f a).pair (g a)))

def Set.bijective {A} (x y : Set A) : Prop := ∃ F, Set.is_bijection F x y

structure normal_filter {A : Type*} (G : subgroup (equiv.perm A)) :=
(Γ : set (subgroup (equiv.perm A)))
(is_perm : ∀ (K ∈ Γ), K ≤ G)
(atoms : ∀ a : A, mul_action.stabilizer (equiv.perm A) a ∈ Γ)
(upward : ∀ H K, H ∈ Γ → H ≤ K → K ∈ Γ)
(inter : ∀ H K, H ∈ Γ → K ∈ Γ → H ⊓ K ∈ Γ)
(conj : ∀ (π ∈ G) (h ∈ Γ), (h:subgroup _).map (mul_aut.conj π).to_monoid_hom ∈ Γ)

def Set.symmetric {A G} (F : @normal_filter A G) (x : Set A) : Prop :=
mul_action.stabilizer (equiv.perm A) x ∈ F.Γ

def pSet.symmetric {A G} (F : @normal_filter A G) (x : pSet A) : Prop := (Set.mk x).symmetric F

def pSet.hereditarily_symmetric {A G} (F : @normal_filter A G) : pSet A → Prop
| (pSet.atom a) := true
| x@(pSet.range f) := pSet.symmetric F x ∧ ∀ a, pSet.hereditarily_symmetric (f a)

def Set.hereditarily_symmetric {A G} (F : @normal_filter A G) (x : Set A) : Prop :=
quotient.lift_on' x (pSet.hereditarily_symmetric F) sorry

def pSet.symm_pow {A G} (F : @normal_filter A G) (x : pSet A) : pSet A :=
x.powerset.sep $ pSet.symmetric F

def Set.symm_pow {A G} (F : @normal_filter A G) (x : Set A) : Set A :=
quotient.lift_on' x (λ x, Set.mk (x.symm_pow F)) sorry

def Set.symm_bijective {A G} (F : @normal_filter A G) (x y : Set A) : Prop :=
∃ f, Set.is_bijection f x y ∧ Set.symmetric F f

end ZFA

namespace con_nf

class params :=
(Λ : Type u) (Λr : Λ → Λ → Prop) [Λwf : is_well_order Λ Λr]
(hΛ : (ordinal.type Λr).is_limit)
(κ : Type u) (hκ : (#κ).is_regular)
(μ : Type u)
(μ_limit : (#μ).is_strong_limit)
(μ_cof : max (#Λ) (#κ) < (#μ).ord.cof)
(δ : Λ)
(hδ : (ordinal.typein Λr δ).is_limit)

open params

variable [params.{u}]

def small {α} (x : set α) := #x < #κ

instance : is_well_order Λ Λr := Λwf
instance : linear_order Λ := linear_order_of_STO' Λr

-- extended type index
def xti : Type* := {s : finset Λ // s.nonempty}

def xti.min (s : xti) : Λ := s.1.min' s.2
def xti.max (s : xti) : Λ := s.1.max' s.2

def xti.drop (s : xti) : option xti := if h : _ then some ⟨s.1.erase s.min, h⟩ else none
def xti.drop_max (s : xti) : option xti := if h : _ then some ⟨s.1.erase s.max, h⟩ else none

instance : has_singleton Λ xti := ⟨λ x, ⟨{x}, finset.singleton_nonempty _⟩⟩
instance : has_insert Λ xti := ⟨λ x s, ⟨insert x s.1, finset.insert_nonempty _ _⟩⟩

noncomputable def xti.dropn (s : xti) : ℕ → option xti
| 0 := some s
| (n+1) := xti.dropn n >>= xti.drop

def clan (A : xti) := μ × κ
def atoms := Σ A, clan A

abbreviation pSet := ZFA.pSet atoms
abbreviation Set := ZFA.Set atoms

def atom {A} (x : clan A) : pSet := ZFA.pSet.atom ⟨A, x⟩

def clan_pSet (A : xti) : pSet := ZFA.pSet.range (@atom _ A)
def clan_Set (A : xti) : Set := ZFA.Set.mk (clan_pSet A)

def is_near_litter {A} (N : set (clan A)) := ∃ x : μ, small (N Δ {p:clan A | p.1 = x})

def near_litter (A) := {N : set (clan A) // is_near_litter N}

def near_litter_pSet {A} (N : near_litter A) : pSet :=
ZFA.pSet.range (λ x : N.1, atom x.1)

def near_litter.near {A} (N : near_litter A) : set (clan A) := {p:clan A | p.1 = N.2.some}

def local_card {A} (N : near_litter A) : set (near_litter A) :=
{M : near_litter A | M.near = N.near}

def local_card_pSet {A} (N : near_litter A) : pSet :=
ZFA.pSet.range (λ M : {M : near_litter A // M.near = N.near}, near_litter_pSet M.1)

def local_cards (A) : set (set (near_litter A)) := set.range local_card

def local_cards_pSet (A : xti) : pSet := ZFA.pSet.range (@local_card_pSet _ A)

def local_cards_Set (A : xti) : Set := ZFA.Set.mk (local_cards_pSet A)

def sdom : xti → xti → Prop
| A := λ B, A.max < B.max ∨ A.max = B.max ∧
  ∀ A' ∈ A.drop_max, ∃ B' ∈ B.drop_max,
    have (A':xti).1.card < A.1.card, from sorry,
    sdom A' B'
using_well_founded {rel_tac := λ _ _, `[exact ⟨_, measure_wf (λ A, A.1.card)⟩]}

instance : has_lt xti := ⟨sdom⟩
instance : is_well_order xti (<) := sorry

variables {P : xti → Prop} (PI : ∀ B, P B → Set)

def allowable' : subgroup (equiv.perm atoms) :=
(⨅ B (h : P B), mul_action.stabilizer _ (PI B h)) ⊓
⨅ C, mul_action.stabilizer _ (local_cards_Set C)

def A_allowable (A) (PI : ∀ B, B < A → Set) : subgroup (equiv.perm atoms) :=
allowable' PI

def support_el := Σ A, clan A ⊕ near_litter A
def support_el.inr (A) (N : near_litter A) : support_el := ⟨A, sum.inr N⟩

structure support_order :=
(S : set support_el)
(small : small S)
(disj (A M N) : support_el.inr A M ∈ S → support_el.inr A N ∈ S → M ≠ N → disjoint M.1 N.1)
(r : S → S → Prop)
(wo : is_well_order S r)

def supported' (S : support_order) : subgroup (equiv.perm atoms) :=
allowable' PI ⊓
⨅ a ∈ S.S, match a with
| ⟨A, sum.inl c⟩ := mul_action.stabilizer _ (@id atoms ⟨A, c⟩)
| ⟨A, sum.inr N⟩ := mul_action.stabilizer _ (near_litter_pSet N)
end

def has_support' (S : support_order)
  {α} [mul_action (equiv.perm atoms) α] (x : α) : Prop :=
supported' PI S ≤ mul_action.stabilizer (equiv.perm atoms) x

def is_symmetric' {P : xti → Prop} (PI : ∀ B, P B → Set)
  {α} [mul_action (equiv.perm atoms) α] (x : α) : Prop :=
∃ S, has_support' PI S x

def support_filter' : ZFA.normal_filter (allowable' PI) :=
{ Γ := {K | ∃ S, supported' PI S ≤ K},
  is_perm := sorry,
  atoms := sorry,
  upward := sorry,
  inter := sorry,
  conj := sorry }

variable (PI_sym : ∀ B (h : P B), ZFA.Set.symmetric (support_filter' PI) (PI B h))

def symm_pow : Set → Set := ZFA.Set.symm_pow (support_filter' PI)
def symm_bij : Set → Set → Prop := ZFA.Set.symm_bijective (support_filter' PI)
def bij : Set → Set → Prop := ZFA.Set.bijective

def xti_below := {A : xti // A < {δ}}
def τ (A : xti_below) : Set := (symm_pow PI)^[2] (clan_Set (insert δ A.1))

theorem τ_power (A A' : xti_below) (h : A.1.drop = some A'.1) :
  symm_bij PI (τ PI A) (symm_pow PI (τ PI A')) := sorry

theorem τ_elementary (A A' B B' : xti_below) (n)
  (hA : A.1.dropn n = some A'.1) (hB : B.1.dropn n = some B'.1)
  (H : A.1.1 \ A'.1.1 = B.1.1 \ B'.1.1) :
  bij ((symm_pow PI)^[n+2] (τ PI A')) ((symm_pow PI)^[n+2] (τ PI B')) := sorry

end con_nf