import Mathlib
import Mathlib.Order.Basic

universe v u

namespace Beth

structure Sieve {P : Type u}[Preorder P] (p : P) : Type u where
  carrier : Set P
  bounded : ∀ {q : P}, q ∈ carrier → p ≤ q
  upward_closed : ∀ {q r : P}, (r ∈ carrier) → r ≤ q → q ∈ carrier

namespace Sieve

theorem ext {P : Type u} [Preorder P] {p : P} {S T : Sieve p} (h : S.carrier = T.carrier) : S = T := by
P : Type u
inst✝ : Preorder P
p : P
S : Sieve p
T : Sieve p
h : S.carrier = T.carrier
⊢ S = T
  cases S
mk
P : Type u
inst✝ : Preorder P
p : P
T : Sieve p
carrier✝ : Set P
bounded✝ : ∀ {q : P}, q ∈ carrier✝ → p ≤ q
upward_closed✝ : ∀ {q r : P}, r ∈ carrier✝ → r ≤ q → q ∈ carrier✝
h : { carrier := carrier✝, bounded := bounded✝, upward_closed := upward_closed✝ }.carrier = T.carrier
⊢ { carrier := carrier✝, bounded := bounded✝, upward_closed := upward_closed✝ } = T; cases T
mk.mk
P : Type u
inst✝ : Preorder P
p : P
carrier✝¹ : Set P
bounded✝¹ : ∀ {q : P}, q ∈ carrier✝ → p ≤ q
upward_closed✝¹ : ∀ {q r : P}, r ∈ carrier✝ → r ≤ q → q ∈ carrier✝
carrier✝ : Set P
bounded✝ : ∀ {q : P}, q ∈ carrier✝ → p ≤ q
upward_closed✝ : ∀ {q r : P}, r ∈ carrier✝ → r ≤ q → q ∈ carrier✝
h : { carrier := carrier✝¹, bounded := bounded✝¹, upward_closed := upward_closed✝¹ }.carrier =
  { carrier := carrier✝, bounded := bounded✝, upward_closed := upward_closed✝ }.carrier
⊢ { carrier := carrier✝¹, bounded := bounded✝¹, upward_closed := upward_closed✝¹ } =
  { carrier := carrier✝, bounded := bounded✝, upward_closed := upward_closed✝ }; simp at h
mk.mk
P : Type u
inst✝ : Preorder P
p : P
carrier✝¹ : Set P
bounded✝¹ : ∀ {q : P}, q ∈ carrier✝ → p ≤ q
upward_closed✝¹ : ∀ {q r : P}, r ∈ carrier✝ → r ≤ q → q ∈ carrier✝
carrier✝ : Set P
bounded✝ : ∀ {q : P}, q ∈ carrier✝ → p ≤ q
upward_closed✝ : ∀ {q r : P}, r ∈ carrier✝ → r ≤ q → q ∈ carrier✝
h : carrier✝¹ = carrier✝
⊢ { carrier := carrier✝¹, bounded := bounded✝¹, upward_closed := upward_closed✝¹ } =
  { carrier := carrier✝, bounded := bounded✝, upward_closed := upward_closed✝ }; subst h
mk.mk
P : Type u
inst✝ : Preorder P
p : P
carrier✝ : Set P
bounded✝¹ : ∀ {q : P}, q ∈ carrier✝ → p ≤ q
upward_closed✝¹ : ∀ {q r : P}, r ∈ carrier✝ → r ≤ q → q ∈ carrier✝
bounded✝ : ∀ {q : P}, q ∈ carrier✝ → p ≤ q
upward_closed✝ : ∀ {q r : P}, r ∈ carrier✝ → r ≤ q → q ∈ carrier✝
⊢ { carrier := carrier✝, bounded := bounded✝¹, upward_closed := upward_closed✝¹ } =
  { carrier := carrier✝, bounded := bounded✝, upward_closed := upward_closed✝ }; rfl

end Sieve

instance [Preorder P]{p : P} : Membership P (Sieve p) where
  mem S q := S.carrier q

def maximal_sieve [Preorder.{u} P] (p : P) : Sieve p := by
P : Type u
inst✝ : Preorder P
p : P
⊢ Sieve p
  refine {carrier := ?_, bounded := ?_, upward_closed := ?_}
refine_1
P : Type u
inst✝ : Preorder P
p : P
⊢ Set P
refine_2
P : Type u
inst✝ : Preorder P
p : P
⊢ ∀ {q : P}, q ∈ ?refine_1 → p ≤ q
refine_3
P : Type u
inst✝ : Preorder P
p : P
⊢ ∀ {q r : P}, r ∈ ?refine_1 → r ≤ q → q ∈ ?refine_1
  ·
refine_1
P : Type u
inst✝ : Preorder P
p : P
⊢ Set P exact {q | p ≤ q}
  ·
refine_2
P : Type u
inst✝ : Preorder P
p : P
⊢ ∀ {q : P}, q ∈ ?refine_1 → p ≤ q intro q h
refine_2
P : Type u
inst✝ : Preorder P
p : P
q : P
h : q ∈ {q | p ≤ q}
⊢ p ≤ q; exact h
  ·
refine_3
P : Type u
inst✝ : Preorder P
p : P
⊢ ∀ {q r : P}, r ∈ ?refine_1 → r ≤ q → q ∈ ?refine_1 intro q r
refine_3
P : Type u
inst✝ : Preorder P
p : P
q : P
r : P
⊢ r ∈ {q | p ≤ q} → r ≤ q → q ∈ {q | p ≤ q} hgr
refine_3
P : Type u
inst✝ : Preorder P
p : P
q : P
r : P
hgr : r ∈ {q | p ≤ q}
⊢ r ≤ q → q ∈ {q | p ≤ q} hqr
refine_3
P : Type u
inst✝ : Preorder P
p : P
q : P
r : P
hgr : r ∈ {q | p ≤ q}
hqr : r ≤ q
⊢ q ∈ {q | p ≤ q}
    exact le_trans hgr hqr

-- We use the terminology pullback even though this goes forward in our set up
def pullback [Preorder P] {p q : P} (_h : p ≤ q) (S : Sieve p) : Sieve q where
    carrier := {r | r ∈ S.carrier ∧ q ≤ r}
    bounded  := fun ⟨_, hr⟩ => hr
    upward_closed := fun ⟨r'_in_S, q_le_r' ⟩ r'_le_r => ⟨S.upward_closed r'_in_S r'_le_r, le_trans q_le_r' r'_le_r⟩

structure Coverage (P : Type u) [Preorder P] : Type u where
  covers : (p : P) → Set (Sieve p)
  maximal : ∀ (p : P), covers p (maximal_sieve p)
  transitive : ∀ (p : P) (U V : Sieve p), covers p U → (∀ (q : U.carrier),
    (covers (q : P) (pullback (U.bounded q.property) V))) -> covers p V
  stability :  ∀ {p q : P} {U : Sieve p} (_U_Cov : covers p U) (p_le_q : p ≤ q), covers q (pullback p_le_q U)

class HasCoverage (P : Type u) extends Preorder P where
  coverage : Coverage P

variable {P : Type u} [HasCoverage P]

def covers (p : P) : Set (Sieve p) := HasCoverage.coverage.covers p

def covers_maximal (p : P) : covers p (maximal_sieve p) :=
  HasCoverage.coverage.maximal p

def covers_transitive {p : P} {U V : Sieve p} (hU : covers p U)
    (hV : ∀ (q : U.carrier), covers (q : P) (pullback (U.bounded q.property) V)) : covers p V :=
  HasCoverage.coverage.transitive p U V hU hV

def covers_stable {p q : P} {U : Sieve p} (hU : covers p U) (h : p ≤ q) : covers q (pullback h U) :=
  HasCoverage.coverage.stability hU h

theorem covers_mono {p : P} {U V : Sieve p} (hU : covers p U) (hUV : U.carrier ⊆ V.carrier) : covers p V := by
P : Type u
inst✝ : HasCoverage P
p : P
U : Sieve p
V : Sieve p
hU : covers p U
hUV : U.carrier ⊆ V.carrier
⊢ covers p V
  apply covers_transitive hU
P : Type u
inst✝ : HasCoverage P
p : P
U : Sieve p
V : Sieve p
hU : covers p U
hUV : U.carrier ⊆ V.carrier
⊢ ∀ (q : ↑U.carrier), covers (↑q) (pullback ⋯ V)
  intro q
P : Type u
inst✝ : HasCoverage P
p : P
U : Sieve p
V : Sieve p
hU : covers p U
hUV : U.carrier ⊆ V.carrier
q : ↑U.carrier
⊢ covers (↑q) (pullback ⋯ V)
  let hqp : p ≤ (q : P) := U.bounded q.property
P : Type u
inst✝ : HasCoverage P
p : P
U : Sieve p
V : Sieve p
hU : covers p U
hUV : U.carrier ⊆ V.carrier
q : ↑U.carrier
hqp : p ≤ ↑q := ···
⊢ covers (↑q) (pullback ⋯ V)
  have h_pull : (pullback hqp V).carrier = (maximal_sieve (q : P)).carrier := by
P : Type u
inst✝ : HasCoverage P
p : P
U : Sieve p
V : Sieve p
hU : covers p U
hUV : U.carrier ⊆ V.carrier
⊢ covers p V
    apply funext
h
P : Type u
inst✝ : HasCoverage P
p : P
U : Sieve p
V : Sieve p
hU : covers p U
hUV : U.carrier ⊆ V.carrier
q : ↑U.carrier
hqp : p ≤ ↑q := ···
⊢ ∀ (x : P), (pullback hqp V).carrier x = (maximal_sieve ↑q).carrier x
    intro r
h
P : Type u
inst✝ : HasCoverage P
p : P
U : Sieve p
V : Sieve p
hU : covers p U
hUV : U.carrier ⊆ V.carrier
q : ↑U.carrier
hqp : p ≤ ↑q := ···
r : P
⊢ (pullback hqp V).carrier r = (maximal_sieve ↑q).carrier r
    apply propext
h.a
P : Type u
inst✝ : HasCoverage P
p : P
U : Sieve p
V : Sieve p
hU : covers p U
hUV : U.carrier ⊆ V.carrier
q : ↑U.carrier
hqp : p ≤ ↑q := ···
r : P
⊢ (pullback hqp V).carrier r ↔ (maximal_sieve ↑q).carrier r
    constructor
h.a.mp
P : Type u
inst✝ : HasCoverage P
p : P
U : Sieve p
V : Sieve p
hU : covers p U
hUV : U.carrier ⊆ V.carrier
q : ↑U.carrier
hqp : p ≤ ↑q := ···
r : P
⊢ (pullback hqp V).carrier r → (maximal_sieve ↑q).carrier r
h.a.mpr
P : Type u
inst✝ : HasCoverage P
p : P
U : Sieve p
V : Sieve p
hU : covers p U
hUV : U.carrier ⊆ V.carrier
q : ↑U.carrier
hqp : p ≤ ↑q := ···
r : P
⊢ (maximal_sieve ↑q).carrier r → (pullback hqp V).carrier r
    ·
h.a.mp
P : Type u
inst✝ : HasCoverage P
p : P
U : Sieve p
V : Sieve p
hU : covers p U
hUV : U.carrier ⊆ V.carrier
q : ↑U.carrier
hqp : p ≤ ↑q := ···
r : P
⊢ (pullback hqp V).carrier r → (maximal_sieve ↑q).carrier r intro h
h.a.mp
P : Type u
inst✝ : HasCoverage P
p : P
U : Sieve p
V : Sieve p
hU : covers p U
hUV : U.carrier ⊆ V.carrier
q : ↑U.carrier
hqp : p ≤ ↑q := ···
r : P
h : (pullback hqp V).carrier r
⊢ (maximal_sieve ↑q).carrier r; exact h.2
    ·
h.a.mpr
P : Type u
inst✝ : HasCoverage P
p : P
U : Sieve p
V : Sieve p
hU : covers p U
hUV : U.carrier ⊆ V.carrier
q : ↑U.carrier
hqp : p ≤ ↑q := ···
r : P
⊢ (maximal_sieve ↑q).carrier r → (pullback hqp V).carrier r intro hqr
h.a.mpr
P : Type u
inst✝ : HasCoverage P
p : P
U : Sieve p
V : Sieve p
hU : covers p U
hUV : U.carrier ⊆ V.carrier
q : ↑U.carrier
hqp : p ≤ ↑q := ···
r : P
hqr : (maximal_sieve ↑q).carrier r
⊢ (pullback hqp V).carrier r; exact ⟨V.upward_closed (hUV q.property) hqr, hqr⟩
  rw [Sieve.ext h_pull]
P : Type u
inst✝ : HasCoverage P
p : P
U : Sieve p
V : Sieve p
hU : covers p U
hUV : U.carrier ⊆ V.carrier
q : ↑U.carrier
hqp : p ≤ ↑q := ···
h_pull : (pullback hqp V).carrier = (maximal_sieve ↑q).carrier
⊢ covers (↑q) (maximal_sieve ↑q)
  apply covers_maximal

def glue_sieves {P : Type u} [Preorder P] {p : P} (U : Sieve p)
    (f : (q : U.carrier) → Sieve (q : P)) : Sieve p where
  carrier := { r | ∃ (q : U.carrier), r ∈ (f q).carrier }
  bounded := fun ⟨q, hq⟩ => le_trans (U.bounded q.property) ((f q).bounded hq)
  upward_closed := fun ⟨q, hq⟩ hrs => ⟨q, (f q).upward_closed hq hrs⟩

theorem covers_glue {P : Type u} [HasCoverage P] {p : P} {U : Sieve p}
    (f : (q : U.carrier) → Sieve (q : P)) (hU : covers p U)
    (hf : ∀ (q : U.carrier), covers (q : P) (f q)) : covers p (glue_sieves U f) := by
P : Type u
inst✝ : HasCoverage P
p : P
U : Sieve p
f : (q : ↑U.carrier) → Sieve ↑q
hU : covers p U
hf : ∀ (q : ↑U.carrier), covers (↑q) (f q)
⊢ covers p (glue_sieves U f)
  apply covers_transitive hU
P : Type u
inst✝ : HasCoverage P
p : P
U : Sieve p
f : (q : ↑U.carrier) → Sieve ↑q
hU : covers p U
hf : ∀ (q : ↑U.carrier), covers (↑q) (f q)
⊢ ∀ (q : ↑U.carrier), covers (↑q) (pullback ⋯ (glue_sieves U f))
  intro q
P : Type u
inst✝ : HasCoverage P
p : P
U : Sieve p
f : (q : ↑U.carrier) → Sieve ↑q
hU : covers p U
hf : ∀ (q : ↑U.carrier), covers (↑q) (f q)
q : ↑U.carrier
⊢ covers (↑q) (pullback ⋯ (glue_sieves U f))
  apply covers_mono (hf q)
P : Type u
inst✝ : HasCoverage P
p : P
U : Sieve p
f : (q : ↑U.carrier) → Sieve ↑q
hU : covers p U
hf : ∀ (q : ↑U.carrier), covers (↑q) (f q)
q : ↑U.carrier
⊢ (f q).carrier ⊆ (pullback ⋯ (glue_sieves U f)).carrier
  intro r hr
P : Type u
inst✝ : HasCoverage P
p : P
U : Sieve p
f : (q : ↑U.carrier) → Sieve ↑q
hU : covers p U
hf : ∀ (q : ↑U.carrier), covers (↑q) (f q)
q : ↑U.carrier
r : P
hr : r ∈ (f q).carrier
⊢ r ∈ (pullback ⋯ (glue_sieves U f)).carrier
  simp [pullback]
P : Type u
inst✝ : HasCoverage P
p : P
U : Sieve p
f : (q : ↑U.carrier) → Sieve ↑q
hU : covers p U
hf : ∀ (q : ↑U.carrier), covers (↑q) (f q)
q : ↑U.carrier
r : P
hr : r ∈ (f q).carrier
⊢ r ∈ (glue_sieves U f).carrier ∧ ↑q ≤ r
  constructor
left
P : Type u
inst✝ : HasCoverage P
p : P
U : Sieve p
f : (q : ↑U.carrier) → Sieve ↑q
hU : covers p U
hf : ∀ (q : ↑U.carrier), covers (↑q) (f q)
q : ↑U.carrier
r : P
hr : r ∈ (f q).carrier
⊢ r ∈ (glue_sieves U f).carrier
right
P : Type u
inst✝ : HasCoverage P
p : P
U : Sieve p
f : (q : ↑U.carrier) → Sieve ↑q
hU : covers p U
hf : ∀ (q : ↑U.carrier), covers (↑q) (f q)
q : ↑U.carrier
r : P
hr : r ∈ (f q).carrier
⊢ ↑q ≤ r
  ·
left
P : Type u
inst✝ : HasCoverage P
p : P
U : Sieve p
f : (q : ↑U.carrier) → Sieve ↑q
hU : covers p U
hf : ∀ (q : ↑U.carrier), covers (↑q) (f q)
q : ↑U.carrier
r : P
hr : r ∈ (f q).carrier
⊢ r ∈ (glue_sieves U f).carrier exact ⟨q, hr⟩
  ·
right
P : Type u
inst✝ : HasCoverage P
p : P
U : Sieve p
f : (q : ↑U.carrier) → Sieve ↑q
hU : covers p U
hf : ∀ (q : ↑U.carrier), covers (↑q) (f q)
q : ↑U.carrier
r : P
hr : r ∈ (f q).carrier
⊢ ↑q ≤ r exact (f q).bounded hr

theorem pullback_maximal (W : Type u) [Preorder W] (c : Coverage W)
  (w v : W) (w_le_v : w ≤ v) :
  (pullback w_le_v (maximal_sieve w)).carrier = (maximal_sieve v).carrier := by
W : Type u
inst✝ : Preorder W
c : Coverage W
w : W
v : W
w_le_v : w ≤ v
⊢ (pullback w_le_v (maximal_sieve w)).carrier = (maximal_sieve v).carrier
  simp [pullback, maximal_sieve]
W : Type u
inst✝ : Preorder W
c : Coverage W
w : W
v : W
w_le_v : w ≤ v
⊢ {r | w ≤ r ∧ v ≤ r} = {q | v ≤ q}
  ext s
h
W : Type u
inst✝ : Preorder W
c : Coverage W
w : W
v : W
w_le_v : w ≤ v
s : W
⊢ s ∈ {r | w ≤ r ∧ v ≤ r} ↔ s ∈ {q | v ≤ q}
  constructor
h.mp
W : Type u
inst✝ : Preorder W
c : Coverage W
w : W
v : W
w_le_v : w ≤ v
s : W
⊢ s ∈ {r | w ≤ r ∧ v ≤ r} → s ∈ {q | v ≤ q}
h.mpr
W : Type u
inst✝ : Preorder W
c : Coverage W
w : W
v : W
w_le_v : w ≤ v
s : W
⊢ s ∈ {q | v ≤ q} → s ∈ {r | w ≤ r ∧ v ≤ r}
  ·
h.mp
W : Type u
inst✝ : Preorder W
c : Coverage W
w : W
v : W
w_le_v : w ≤ v
s : W
⊢ s ∈ {r | w ≤ r ∧ v ≤ r} → s ∈ {q | v ≤ q} intro s_in_pullback
h.mp
W : Type u
inst✝ : Preorder W
c : Coverage W
w : W
v : W
w_le_v : w ≤ v
s : W
s_in_pullback : s ∈ {r | w ≤ r ∧ v ≤ r}
⊢ s ∈ {q | v ≤ q}
    simp at s_in_pullback
h.mp
W : Type u
inst✝ : Preorder W
c : Coverage W
w : W
v : W
w_le_v : w ≤ v
s : W
s_in_pullback : w ≤ s ∧ v ≤ s
⊢ s ∈ {q | v ≤ q}
    simp
h.mp
W : Type u
inst✝ : Preorder W
c : Coverage W
w : W
v : W
w_le_v : w ≤ v
s : W
s_in_pullback : w ≤ s ∧ v ≤ s
⊢ v ≤ s
    apply s_in_pullback.2
  ·
h.mpr
W : Type u
inst✝ : Preorder W
c : Coverage W
w : W
v : W
w_le_v : w ≤ v
s : W
⊢ s ∈ {q | v ≤ q} → s ∈ {r | w ≤ r ∧ v ≤ r} intro s_in_maximal
h.mpr
W : Type u
inst✝ : Preorder W
c : Coverage W
w : W
v : W
w_le_v : w ≤ v
s : W
s_in_maximal : s ∈ {q | v ≤ q}
⊢ s ∈ {r | w ≤ r ∧ v ≤ r}
    simp
h.mpr
W : Type u
inst✝ : Preorder W
c : Coverage W
w : W
v : W
w_le_v : w ≤ v
s : W
s_in_maximal : s ∈ {q | v ≤ q}
⊢ w ≤ s ∧ v ≤ s
    simp at s_in_maximal
h.mpr
W : Type u
inst✝ : Preorder W
c : Coverage W
w : W
v : W
w_le_v : w ≤ v
s : W
s_in_maximal : v ≤ s
⊢ w ≤ s ∧ v ≤ s
    constructor
h.mpr.left
W : Type u
inst✝ : Preorder W
c : Coverage W
w : W
v : W
w_le_v : w ≤ v
s : W
s_in_maximal : v ≤ s
⊢ w ≤ s
h.mpr.right
W : Type u
inst✝ : Preorder W
c : Coverage W
w : W
v : W
w_le_v : w ≤ v
s : W
s_in_maximal : v ≤ s
⊢ v ≤ s
    ·
h.mpr.left
W : Type u
inst✝ : Preorder W
c : Coverage W
w : W
v : W
w_le_v : w ≤ v
s : W
s_in_maximal : v ≤ s
⊢ w ≤ s apply le_trans
h.mpr.left.a
W : Type u
inst✝ : Preorder W
c : Coverage W
w : W
v : W
w_le_v : w ≤ v
s : W
s_in_maximal : v ≤ s
⊢ w ≤ ?h.mpr.left.b
h.mpr.left.a
W : Type u
inst✝ : Preorder W
c : Coverage W
w : W
v : W
w_le_v : w ≤ v
s : W
s_in_maximal : v ≤ s
⊢ ?h.mpr.left.b ≤ s
h.mpr.left.b
W : Type u
inst✝ : Preorder W
c : Coverage W
w : W
v : W
w_le_v : w ≤ v
s : W
s_in_maximal : v ≤ s
⊢ W
      ·
h.mpr.left.a
W : Type u
inst✝ : Preorder W
c : Coverage W
w : W
v : W
w_le_v : w ≤ v
s : W
s_in_maximal : v ≤ s
⊢ w ≤ ?h.mpr.left.b exact w_le_v
      ·
h.mpr.left.a
W : Type u
inst✝ : Preorder W
c : Coverage W
w : W
v : W
w_le_v : w ≤ v
s : W
s_in_maximal : v ≤ s
⊢ ?h.mpr.left.b ≤ s assumption
    ·
h.mpr.right
W : Type u
inst✝ : Preorder W
c : Coverage W
w : W
v : W
w_le_v : w ≤ v
s : W
s_in_maximal : v ≤ s
⊢ v ≤ s assumption

def maximalSieveCoverage (W : Type u) [Preorder W] : Coverage W where
  covers w S := S.carrier = (maximal_sieve w).carrier
  maximal _w := rfl
  transitive := by
P : Type u
inst✝¹ : HasCoverage P
W : Type u
inst✝ : Preorder W
⊢ ∀ (p : W) (U V : Sieve p),
  U.carrier = (maximal_sieve p).carrier →
    (∀ (q : ↑U.carrier), (pullback ⋯ V).carrier = (maximal_sieve ↑q).carrier) → V.carrier = (maximal_sieve p).carrier
    intro p U
P : Type u
inst✝¹ : HasCoverage P
W : Type u
inst✝ : Preorder W
p : W
U : Sieve p
⊢ ∀ (V : Sieve p),
  U.carrier = (maximal_sieve p).carrier →
    (∀ (q : ↑U.carrier), (pullback ⋯ V).carrier = (maximal_sieve ↑q).carrier) → V.carrier = (maximal_sieve p).carrier V
P : Type u
inst✝¹ : HasCoverage P
W : Type u
inst✝ : Preorder W
p : W
U : Sieve p
V : Sieve p
⊢ U.carrier = (maximal_sieve p).carrier →
  (∀ (q : ↑U.carrier), (pullback ⋯ V).carrier = (maximal_sieve ↑q).carrier) → V.carrier = (maximal_sieve p).carrier hU
P : Type u
inst✝¹ : HasCoverage P
W : Type u
inst✝ : Preorder W
p : W
U : Sieve p
V : Sieve p
hU : U.carrier = (maximal_sieve p).carrier
⊢ (∀ (q : ↑U.carrier), (pullback ⋯ V).carrier = (maximal_sieve ↑q).carrier) → V.carrier = (maximal_sieve p).carrier hV
P : Type u
inst✝¹ : HasCoverage P
W : Type u
inst✝ : Preorder W
p : W
U : Sieve p
V : Sieve p
hU : U.carrier = (maximal_sieve p).carrier
hV : ∀ (q : ↑U.carrier), (pullback ⋯ V).carrier = (maximal_sieve ↑q).carrier
⊢ V.carrier = (maximal_sieve p).carrier
    have p_in_U : p ∈ U.carrier := by
P : Type u
inst✝¹ : HasCoverage P
W : Type u
inst✝ : Preorder W
⊢ ∀ (p : W) (U V : Sieve p),
  U.carrier = (maximal_sieve p).carrier →
    (∀ (q : ↑U.carrier), (pullback ⋯ V).carrier = (maximal_sieve ↑q).carrier) → V.carrier = (maximal_sieve p).carrier rw [hU]
P : Type u
inst✝¹ : HasCoverage P
W : Type u
inst✝ : Preorder W
p : W
U : Sieve p
V : Sieve p
hU : U.carrier = (maximal_sieve p).carrier
hV : ∀ (q : ↑U.carrier), (pullback ⋯ V).carrier = (maximal_sieve ↑q).carrier
⊢ p ∈ (maximal_sieve p).carrier; exact le_refl p
    have pullback_maximal  := hV ⟨p, p_in_U⟩
P : Type u
inst✝¹ : HasCoverage P
W : Type u
inst✝ : Preorder W
p : W
U : Sieve p
V : Sieve p
hU : U.carrier = (maximal_sieve p).carrier
hV : ∀ (q : ↑U.carrier), (pullback ⋯ V).carrier = (maximal_sieve ↑q).carrier
p_in_U : p ∈ U.carrier
pullback_maximal : (pullback ⋯ V).carrier = (maximal_sieve ↑⟨p, p_in_U⟩).carrier
⊢ V.carrier = (maximal_sieve p).carrier
    ext s
h
P : Type u
inst✝¹ : HasCoverage P
W : Type u
inst✝ : Preorder W
p : W
U : Sieve p
V : Sieve p
hU : U.carrier = (maximal_sieve p).carrier
hV : ∀ (q : ↑U.carrier), (pullback ⋯ V).carrier = (maximal_sieve ↑q).carrier
p_in_U : p ∈ U.carrier
pullback_maximal : (pullback ⋯ V).carrier = (maximal_sieve ↑⟨p, p_in_U⟩).carrier
s : W
⊢ s ∈ V.carrier ↔ s ∈ (maximal_sieve p).carrier
    simp only [maximal_sieve, Set.mem_setOf_eq]
h
P : Type u
inst✝¹ : HasCoverage P
W : Type u
inst✝ : Preorder W
p : W
U : Sieve p
V : Sieve p
hU : U.carrier = (maximal_sieve p).carrier
hV : ∀ (q : ↑U.carrier), (pullback ⋯ V).carrier = (maximal_sieve ↑q).carrier
p_in_U : p ∈ U.carrier
pullback_maximal : (pullback ⋯ V).carrier = (maximal_sieve ↑⟨p, p_in_U⟩).carrier
s : W
⊢ s ∈ V.carrier ↔ p ≤ s
    constructor
h.mp
P : Type u
inst✝¹ : HasCoverage P
W : Type u
inst✝ : Preorder W
p : W
U : Sieve p
V : Sieve p
hU : U.carrier = (maximal_sieve p).carrier
hV : ∀ (q : ↑U.carrier), (pullback ⋯ V).carrier = (maximal_sieve ↑q).carrier
p_in_U : p ∈ U.carrier
pullback_maximal : (pullback ⋯ V).carrier = (maximal_sieve ↑⟨p, p_in_U⟩).carrier
s : W
⊢ s ∈ V.carrier → p ≤ s
h.mpr
P : Type u
inst✝¹ : HasCoverage P
W : Type u
inst✝ : Preorder W
p : W
U : Sieve p
V : Sieve p
hU : U.carrier = (maximal_sieve p).carrier
hV : ∀ (q : ↑U.carrier), (pullback ⋯ V).carrier = (maximal_sieve ↑q).carrier
p_in_U : p ∈ U.carrier
pullback_maximal : (pullback ⋯ V).carrier = (maximal_sieve ↑⟨p, p_in_U⟩).carrier
s : W
⊢ p ≤ s → s ∈ V.carrier
    ·
h.mp
P : Type u
inst✝¹ : HasCoverage P
W : Type u
inst✝ : Preorder W
p : W
U : Sieve p
V : Sieve p
hU : U.carrier = (maximal_sieve p).carrier
hV : ∀ (q : ↑U.carrier), (pullback ⋯ V).carrier = (maximal_sieve ↑q).carrier
p_in_U : p ∈ U.carrier
pullback_maximal : (pullback ⋯ V).carrier = (maximal_sieve ↑⟨p, p_in_U⟩).carrier
s : W
⊢ s ∈ V.carrier → p ≤ s intro hr
h.mp
P : Type u
inst✝¹ : HasCoverage P
W : Type u
inst✝ : Preorder W
p : W
U : Sieve p
V : Sieve p
hU : U.carrier = (maximal_sieve p).carrier
hV : ∀ (q : ↑U.carrier), (pullback ⋯ V).carrier = (maximal_sieve ↑q).carrier
p_in_U : p ∈ U.carrier
pullback_maximal : (pullback ⋯ V).carrier = (maximal_sieve ↑⟨p, p_in_U⟩).carrier
s : W
hr : s ∈ V.carrier
⊢ p ≤ s; exact V.bounded hr
    ·
h.mpr
P : Type u
inst✝¹ : HasCoverage P
W : Type u
inst✝ : Preorder W
p : W
U : Sieve p
V : Sieve p
hU : U.carrier = (maximal_sieve p).carrier
hV : ∀ (q : ↑U.carrier), (pullback ⋯ V).carrier = (maximal_sieve ↑q).carrier
p_in_U : p ∈ U.carrier
pullback_maximal : (pullback ⋯ V).carrier = (maximal_sieve ↑⟨p, p_in_U⟩).carrier
s : W
⊢ p ≤ s → s ∈ V.carrier intro hr
h.mpr
P : Type u
inst✝¹ : HasCoverage P
W : Type u
inst✝ : Preorder W
p : W
U : Sieve p
V : Sieve p
hU : U.carrier = (maximal_sieve p).carrier
hV : ∀ (q : ↑U.carrier), (pullback ⋯ V).carrier = (maximal_sieve ↑q).carrier
p_in_U : p ∈ U.carrier
pullback_maximal : (pullback ⋯ V).carrier = (maximal_sieve ↑⟨p, p_in_U⟩).carrier
s : W
hr : p ≤ s
⊢ s ∈ V.carrier
      have hmem : s ∈ (pullback (U.bounded p_in_U) V).carrier := by
P : Type u
inst✝¹ : HasCoverage P
W : Type u
inst✝ : Preorder W
⊢ ∀ (p : W) (U V : Sieve p),
  U.carrier = (maximal_sieve p).carrier →
    (∀ (q : ↑U.carrier), (pullback ⋯ V).carrier = (maximal_sieve ↑q).carrier) → V.carrier = (maximal_sieve p).carrier
        rw [pullback_maximal]
P : Type u
inst✝¹ : HasCoverage P
W : Type u
inst✝ : Preorder W
p : W
U : Sieve p
V : Sieve p
hU : U.carrier = (maximal_sieve p).carrier
hV : ∀ (q : ↑U.carrier), (pullback ⋯ V).carrier = (maximal_sieve ↑q).carrier
p_in_U : p ∈ U.carrier
pullback_maximal : (pullback ⋯ V).carrier = (maximal_sieve ↑⟨p, p_in_U⟩).carrier
s : W
hr : p ≤ s
⊢ s ∈ (maximal_sieve ↑⟨p, p_in_U⟩).carrier; assumption
      simp only [pullback, Set.mem_setOf_eq] at hmem
h.mpr
P : Type u
inst✝¹ : HasCoverage P
W : Type u
inst✝ : Preorder W
p : W
U : Sieve p
V : Sieve p
hU : U.carrier = (maximal_sieve p).carrier
hV : ∀ (q : ↑U.carrier), (pullback ⋯ V).carrier = (maximal_sieve ↑q).carrier
p_in_U : p ∈ U.carrier
pullback_maximal : (pullback ⋯ V).carrier = (maximal_sieve ↑⟨p, p_in_U⟩).carrier
s : W
hr : p ≤ s
hmem : s ∈ V.carrier ∧ p ≤ s
⊢ s ∈ V.carrier
      exact hmem.1
  stability := by
P : Type u
inst✝¹ : HasCoverage P
W : Type u
inst✝ : Preorder W
⊢ ∀ {p q : W} {U : Sieve p},
  U.carrier = (maximal_sieve p).carrier → ∀ (p_le_q : p ≤ q), (pullback p_le_q U).carrier = (maximal_sieve q).carrier
    intro p q
P : Type u
inst✝¹ : HasCoverage P
W : Type u
inst✝ : Preorder W
p : W
q : W
⊢ ∀ {U : Sieve p},
  U.carrier = (maximal_sieve p).carrier → ∀ (p_le_q : p ≤ q), (pullback p_le_q U).carrier = (maximal_sieve q).carrier U
P : Type u
inst✝¹ : HasCoverage P
W : Type u
inst✝ : Preorder W
p : W
q : W
U : Sieve p
⊢ U.carrier = (maximal_sieve p).carrier → ∀ (p_le_q : p ≤ q), (pullback p_le_q U).carrier = (maximal_sieve q).carrier hU
P : Type u
inst✝¹ : HasCoverage P
W : Type u
inst✝ : Preorder W
p : W
q : W
U : Sieve p
hU : U.carrier = (maximal_sieve p).carrier
⊢ ∀ (p_le_q : p ≤ q), (pullback p_le_q U).carrier = (maximal_sieve q).carrier h
P : Type u
inst✝¹ : HasCoverage P
W : Type u
inst✝ : Preorder W
p : W
q : W
U : Sieve p
hU : U.carrier = (maximal_sieve p).carrier
h : p ≤ q
⊢ (pullback h U).carrier = (maximal_sieve q).carrier
    ext r
h
P : Type u
inst✝¹ : HasCoverage P
W : Type u
inst✝ : Preorder W
p : W
q : W
U : Sieve p
hU : U.carrier = (maximal_sieve p).carrier
h : p ≤ q
r : W
⊢ r ∈ (pullback h U).carrier ↔ r ∈ (maximal_sieve q).carrier
    simp only [pullback, maximal_sieve, Set.mem_setOf_eq]
h
P : Type u
inst✝¹ : HasCoverage P
W : Type u
inst✝ : Preorder W
p : W
q : W
U : Sieve p
hU : U.carrier = (maximal_sieve p).carrier
h : p ≤ q
r : W
⊢ r ∈ U.carrier ∧ q ≤ r ↔ q ≤ r
    constructor
h.mp
P : Type u
inst✝¹ : HasCoverage P
W : Type u
inst✝ : Preorder W
p : W
q : W
U : Sieve p
hU : U.carrier = (maximal_sieve p).carrier
h : p ≤ q
r : W
⊢ r ∈ U.carrier ∧ q ≤ r → q ≤ r
h.mpr
P : Type u
inst✝¹ : HasCoverage P
W : Type u
inst✝ : Preorder W
p : W
q : W
U : Sieve p
hU : U.carrier = (maximal_sieve p).carrier
h : p ≤ q
r : W
⊢ q ≤ r → r ∈ U.carrier ∧ q ≤ r
    ·
h.mp
P : Type u
inst✝¹ : HasCoverage P
W : Type u
inst✝ : Preorder W
p : W
q : W
U : Sieve p
hU : U.carrier = (maximal_sieve p).carrier
h : p ≤ q
r : W
⊢ r ∈ U.carrier ∧ q ≤ r → q ≤ r rintro ⟨_, hr⟩
h.mp
P : Type u
inst✝¹ : HasCoverage P
W : Type u
inst✝ : Preorder W
p : W
q : W
U : Sieve p
hU : U.carrier = (maximal_sieve p).carrier
h : p ≤ q
r : W
left✝ : r ∈ U.carrier
hr : q ≤ r
⊢ q ≤ r; exact hr
    ·
h.mpr
P : Type u
inst✝¹ : HasCoverage P
W : Type u
inst✝ : Preorder W
p : W
q : W
U : Sieve p
hU : U.carrier = (maximal_sieve p).carrier
h : p ≤ q
r : W
⊢ q ≤ r → r ∈ U.carrier ∧ q ≤ r intro hr
h.mpr
P : Type u
inst✝¹ : HasCoverage P
W : Type u
inst✝ : Preorder W
p : W
q : W
U : Sieve p
hU : U.carrier = (maximal_sieve p).carrier
h : p ≤ q
r : W
hr : q ≤ r
⊢ r ∈ U.carrier ∧ q ≤ r
      exact ⟨by
P : Type u
inst✝¹ : HasCoverage P
W : Type u
inst✝ : Preorder W
p : W
q : W
U : Sieve p
hU : U.carrier = (maximal_sieve p).carrier
h : p ≤ q
r : W
hr : q ≤ r
⊢ r ∈ U.carrier rw [hU]
P : Type u
inst✝¹ : HasCoverage P
W : Type u
inst✝ : Preorder W
p : W
q : W
U : Sieve p
hU : U.carrier = (maximal_sieve p).carrier
h : p ≤ q
r : W
hr : q ≤ r
⊢ r ∈ (maximal_sieve p).carrier; exact le_trans h hr, hr⟩