import Mathlib
import Mathlib.Order.Basic
import Beth.Coverage
import Beth.Semantics

universe v u

namespace Beth

namespace BethTrees

inductive SnocList (α : Type u) where
  | nil  : SnocList α
  | snoc : SnocList α → α → SnocList α

open SnocList

notation "εₛ" => SnocList.nil

notation:50 l " :> " a => SnocList.snoc l a

def SnocList.Mem (a : α) : SnocList α → Prop
    | .nil       => False
    | .snoc xs x => a = x ∨ SnocList.Mem a xs

instance : Membership α (SnocList α) where
  mem xs a := SnocList.Mem a xs

def SnocList.append :  (SnocList α) → (SnocList α) → SnocList α
  | as , .nil => as
  | as , .snoc bs b => .snoc (append as bs) b

attribute [simp] SnocList.append

instance : Append (SnocList α) where
  append := SnocList.append

@[simp] theorem SnocList.append_snoc (as bs : SnocList α) (b : α) :
      as ++ (bs :> b) = ((as ++ bs) :> b) := rfl

def SnocList.is_prefix :  (SnocList α) → (SnocList α) → Prop
  | as, .nil => as = .nil
  | as, .snoc bs b => as = .snoc bs b ∨ is_prefix as bs

def SnocList.is_prefix_rfl : (as : SnocList α) → SnocList.is_prefix as as
  | .nil => rfl
  | .snoc _ _ => Or.inl rfl

theorem SnocList.is_prefix_trans {as bs cs : SnocList α} :
  SnocList.is_prefix as bs → SnocList.is_prefix bs cs → SnocList.is_prefix as cs := by
α : Type u_1
as : SnocList α
bs : SnocList α
cs : SnocList α
⊢ as.is_prefix bs → bs.is_prefix cs → as.is_prefix cs
  intro h1 h2
α : Type u_1
as : SnocList α
bs : SnocList α
cs : SnocList α
h1 : as.is_prefix bs
h2 : bs.is_prefix cs
⊢ as.is_prefix cs
  induction cs with
  | nil =>
nil
α : Type u_1
as : SnocList α
bs : SnocList α
h1 : as.is_prefix bs
h2 : bs.is_prefix εₛ
⊢ as.is_prefix εₛ
    cases h2
nil.refl
α : Type u_1
as : SnocList α
h1 : as.is_prefix εₛ
⊢ as.is_prefix εₛ
    rw [h1]
nil.refl
α : Type u_1
as : SnocList α
h1 : as.is_prefix εₛ
⊢ εₛ.is_prefix εₛ
    exact SnocList.is_prefix_rfl _
  | snoc cs' c ih =>
snoc
α : Type u_1
as : SnocList α
bs : SnocList α
h1 : as.is_prefix bs
cs' : SnocList α
c : α
ih : bs.is_prefix cs' → as.is_prefix cs'
h2 : bs.is_prefix (cs' :> c)
⊢ as.is_prefix (cs' :> c)
    rcases h2 with rfl | h2
snoc.inl
α : Type u_1
as : SnocList α
cs' : SnocList α
c : α
h1 : as.is_prefix (cs' :> c)
ih : (cs' :> c).is_prefix cs' → as.is_prefix cs'
⊢ as.is_prefix (cs' :> c)
snoc.inr
α : Type u_1
as : SnocList α
bs : SnocList α
h1 : as.is_prefix bs
cs' : SnocList α
c : α
ih : bs.is_prefix cs' → as.is_prefix cs'
h2 : bs.is_prefix cs'
⊢ as.is_prefix (cs' :> c)
    ·
snoc.inl
α : Type u_1
as : SnocList α
cs' : SnocList α
c : α
h1 : as.is_prefix (cs' :> c)
ih : (cs' :> c).is_prefix cs' → as.is_prefix cs'
⊢ as.is_prefix (cs' :> c) exact h1
    ·
snoc.inr
α : Type u_1
as : SnocList α
bs : SnocList α
h1 : as.is_prefix bs
cs' : SnocList α
c : α
ih : bs.is_prefix cs' → as.is_prefix cs'
h2 : bs.is_prefix cs'
⊢ as.is_prefix (cs' :> c) exact Or.inr (ih h2)

instance : Preorder (SnocList α) where
  le as bs := SnocList.is_prefix as bs
  le_refl := SnocList.is_prefix_rfl
  le_trans := fun _ _ _ h1 h2 => SnocList.is_prefix_trans h1 h2

def initial {α : Type u} (f : ℕ → α) : ℕ → SnocList α
  | 0     => .nil
  | n + 1 => initial f n :> f n

def SnocList.append_nil (l : SnocList α) : l ++ .nil = l := rfl

attribute [simp] SnocList.append_nil

structure BethTree (α : Type u) where
  tree_node   : SnocList α → Prop
  root        : tree_node .nil
  prefix_closed : ∀ l a, tree_node (l :> a) → tree_node l
  pruned      : ∀ l, tree_node l → ∃ a, tree_node (l :> a)

theorem BethTree.nonempty {α : Type u} (T : BethTree α) : Nonempty α :=
  let ⟨a, _⟩ := T.pruned .nil T.root; ⟨a⟩

def IsBar {α : Type u} (T : BethTree α) (l : SnocList α) (S : SnocList α → Prop) : Prop :=
  ∀ f : ℕ → α,
    T.tree_node l →
    (∀ n, T.tree_node (l ++ initial f n)) →
    ∃ n, S (l ++ initial f n)

theorem SnocList.append_assoc (as bs cs : SnocList α) :
  (as ++ bs) ++ cs = as ++ (bs ++ cs) := by
α : Type u_1
as : SnocList α
bs : SnocList α
cs : SnocList α
⊢ as ++ bs ++ cs = as ++ (bs ++ cs)
  induction cs with
  | nil =>
nil
α : Type u_1
as : SnocList α
bs : SnocList α
⊢ as ++ bs ++ εₛ = as ++ (bs ++ εₛ) rfl
  | snoc cs' c ih =>
snoc
α : Type u_1
as : SnocList α
bs : SnocList α
cs' : SnocList α
c : α
ih : as ++ bs ++ cs' = as ++ (bs ++ cs')
⊢ as ++ bs ++ (cs' :> c) = as ++ (bs ++ (cs' :> c))
    simp
snoc
α : Type u_1
as : SnocList α
bs : SnocList α
cs' : SnocList α
c : α
ih : as ++ bs ++ cs' = as ++ (bs ++ cs')
⊢ as ++ bs ++ cs' = as ++ (bs ++ cs')
    rw [ih]

private lemma initial_eq_of_agree {α : Type u} {f g : ℕ → α} {n : ℕ} (h : ∀ i < n, f i = g i) :
    initial f n = initial g n := by
α : Type u
f : ℕ → α
g : ℕ → α
n : ℕ
h : ∀ i < n, f i = g i
⊢ initial f n = initial g n
  induction n with
  | zero =>
zero
α : Type u
f : ℕ → α
g : ℕ → α
h : ∀ i < 0, f i = g i
⊢ initial f 0 = initial g 0 simp [initial]
  | succ k ihk =>
succ
α : Type u
f : ℕ → α
g : ℕ → α
k : ℕ
ihk : (∀ i < k, f i = g i) → initial f k = initial g k
h : ∀ i < k + 1, f i = g i
⊢ initial f (k + 1) = initial g (k + 1)
    simp only [initial]
succ
α : Type u
f : ℕ → α
g : ℕ → α
k : ℕ
ihk : (∀ i < k, f i = g i) → initial f k = initial g k
h : ∀ i < k + 1, f i = g i
⊢ (initial f k :> f k) = (initial g k :> g k)
    congr 1
succ.e_a
α : Type u
f : ℕ → α
g : ℕ → α
k : ℕ
ihk : (∀ i < k, f i = g i) → initial f k = initial g k
h : ∀ i < k + 1, f i = g i
⊢ initial f k = initial g k
succ.e_a
α : Type u
f : ℕ → α
g : ℕ → α
k : ℕ
ihk : (∀ i < k, f i = g i) → initial f k = initial g k
h : ∀ i < k + 1, f i = g i
⊢ f k = g k
    ·
succ.e_a
α : Type u
f : ℕ → α
g : ℕ → α
k : ℕ
ihk : (∀ i < k, f i = g i) → initial f k = initial g k
h : ∀ i < k + 1, f i = g i
⊢ initial f k = initial g k exact ihk (fun i hi => h i (Nat.lt_succ_of_lt hi))
    ·
succ.e_a
α : Type u
f : ℕ → α
g : ℕ → α
k : ℕ
ihk : (∀ i < k, f i = g i) → initial f k = initial g k
h : ∀ i < k + 1, f i = g i
⊢ f k = g k exact h k (Nat.lt_succ_self k)

def le_init {α : Type u} [Nonempty α] (xs ys : SnocList α) (le : xs ≤ ys) :
    ∃ f : ℕ → α, ∃ n, ys = xs ++ initial f n := by
α : Type u
inst✝ : Nonempty α
xs : SnocList α
ys : SnocList α
le : xs ≤ ys
⊢ ∃ f n, ys = xs ++ initial f n
  induction ys with
  | nil =>
nil
α : Type u
inst✝ : Nonempty α
xs : SnocList α
le : xs ≤ εₛ
⊢ ∃ f n, εₛ = xs ++ initial f n
    cases le
nil.refl
α : Type u
inst✝ : Nonempty α
⊢ ∃ f n, εₛ = εₛ ++ initial f n
    exists (fun _ => Classical.choice ‹Nonempty α›)
nil.refl
α : Type u
inst✝ : Nonempty α
⊢ ∃ n, εₛ = εₛ ++ initial (fun x => Classical.choice inst✝) n
    exists 0
  | snoc ys' y ih =>
snoc
α : Type u
inst✝ : Nonempty α
xs : SnocList α
ys' : SnocList α
y : α
ih : xs ≤ ys' → ∃ f n, ys' = xs ++ initial f n
le : xs ≤ (ys' :> y)
⊢ ∃ f n, (ys' :> y) = xs ++ initial f n
    rcases le with rfl | hle
snoc.inl
α : Type u
inst✝ : Nonempty α
ys' : SnocList α
y : α
ih : (ys' :> y) ≤ ys' → ∃ f n, ys' = (ys' :> y) ++ initial f n
⊢ ∃ f n, (ys' :> y) = (ys' :> y) ++ initial f n
snoc.inr
α : Type u
inst✝ : Nonempty α
xs : SnocList α
ys' : SnocList α
y : α
ih : xs ≤ ys' → ∃ f n, ys' = xs ++ initial f n
hle : xs.is_prefix ys'
⊢ ∃ f n, (ys' :> y) = xs ++ initial f n
    ·
snoc.inl
α : Type u
inst✝ : Nonempty α
ys' : SnocList α
y : α
ih : (ys' :> y) ≤ ys' → ∃ f n, ys' = (ys' :> y) ++ initial f n
⊢ ∃ f n, (ys' :> y) = (ys' :> y) ++ initial f n exists fun _ => Classical.choice ‹Nonempty α›
snoc.inl
α : Type u
inst✝ : Nonempty α
ys' : SnocList α
y : α
ih : (ys' :> y) ≤ ys' → ∃ f n, ys' = (ys' :> y) ++ initial f n
⊢ ∃ n, (ys' :> y) = (ys' :> y) ++ initial (fun x => Classical.choice inst✝) n
      exists 0
    ·
snoc.inr
α : Type u
inst✝ : Nonempty α
xs : SnocList α
ys' : SnocList α
y : α
ih : xs ≤ ys' → ∃ f n, ys' = xs ++ initial f n
hle : xs.is_prefix ys'
⊢ ∃ f n, (ys' :> y) = xs ++ initial f n obtain ⟨f, n, rfl⟩ := ih hle
snoc.inr
α : Type u
inst✝ : Nonempty α
xs : SnocList α
y : α
f : ℕ → α
n : ℕ
ih : xs ≤ xs ++ initial f n → ∃ f_1 n_1, xs ++ initial f n = xs ++ initial f_1 n_1
hle : xs.is_prefix (xs ++ initial f n)
⊢ ∃ f_1 n_1, (xs ++ initial f n :> y) = xs ++ initial f_1 n_1
      use (λ i => if i < n then f i else y), n + 1
h
α : Type u
inst✝ : Nonempty α
xs : SnocList α
y : α
f : ℕ → α
n : ℕ
ih : xs ≤ xs ++ initial f n → ∃ f_1 n_1, xs ++ initial f n = xs ++ initial f_1 n_1
hle : xs.is_prefix (xs ++ initial f n)
⊢ (xs ++ initial f n :> y) = xs ++ initial (fun i => if i < n then f i else y) (n + 1)
      simp only [initial, Nat.lt_irrefl, ite_false]
h
α : Type u
inst✝ : Nonempty α
xs : SnocList α
y : α
f : ℕ → α
n : ℕ
ih : xs ≤ xs ++ initial f n → ∃ f_1 n_1, xs ++ initial f n = xs ++ initial f_1 n_1
hle : xs.is_prefix (xs ++ initial f n)
⊢ (xs ++ initial f n :> y) = xs ++ (initial (fun i => if i < n then f i else y) n :> y)
      congr 1
h.e_a
α : Type u
inst✝ : Nonempty α
xs : SnocList α
y : α
f : ℕ → α
n : ℕ
ih : xs ≤ xs ++ initial f n → ∃ f_1 n_1, xs ++ initial f n = xs ++ initial f_1 n_1
hle : xs.is_prefix (xs ++ initial f n)
⊢ xs ++ initial f n = xs.append (initial (fun i => if i < n then f i else y) n)
      have eq : initial f n = initial (fun i => if i < n then f i else y) n := by
α : Type u
inst✝ : Nonempty α
xs : SnocList α
ys : SnocList α
le : xs ≤ ys
⊢ ∃ f n, ys = xs ++ initial f n
        apply initial_eq_of_agree
h
α : Type u
inst✝ : Nonempty α
xs : SnocList α
y : α
f : ℕ → α
n : ℕ
ih : xs ≤ xs ++ initial f n → ∃ f_1 n_1, xs ++ initial f n = xs ++ initial f_1 n_1
hle : xs.is_prefix (xs ++ initial f n)
⊢ ∀ i < n, f i = if i < n then f i else y
        intro i i_le_n
h
α : Type u
inst✝ : Nonempty α
xs : SnocList α
y : α
f : ℕ → α
n : ℕ
ih : xs ≤ xs ++ initial f n → ∃ f_1 n_1, xs ++ initial f n = xs ++ initial f_1 n_1
hle : xs.is_prefix (xs ++ initial f n)
i : ℕ
i_le_n : i < n
⊢ f i = if i < n then f i else y
        simp [if_pos i_le_n]
      rw [<- eq]
h.e_a
α : Type u
inst✝ : Nonempty α
xs : SnocList α
y : α
f : ℕ → α
n : ℕ
ih : xs ≤ xs ++ initial f n → ∃ f_1 n_1, xs ++ initial f n = xs ++ initial f_1 n_1
hle : xs.is_prefix (xs ++ initial f n)
eq : initial f n = initial (fun i => if i < n then f i else y) n
⊢ xs ++ initial f n = xs.append (initial f n)
      rfl

theorem initial_add {α : Type u} (f : ℕ → α) (m n : ℕ) :
  initial f (m + n) = initial f m ++ initial (λ i => f (m + i)) n := by
α : Type u
f : ℕ → α
m : ℕ
n : ℕ
⊢ initial f (m + n) = initial f m ++ initial (fun i => f (m + i)) n
  induction n with
  | zero =>
zero
α : Type u
f : ℕ → α
m : ℕ
⊢ initial f (m + 0) = initial f m ++ initial (fun i => f (m + i)) 0 simp [initial, SnocList.append_nil]
  | succ n ih =>
succ
α : Type u
f : ℕ → α
m : ℕ
n : ℕ
ih : initial f (m + n) = initial f m ++ initial (fun i => f (m + i)) n
⊢ initial f (m + (n + 1)) = initial f m ++ initial (fun i => f (m + i)) (n + 1)
    rw [Nat.add_succ, initial, ih, initial]
succ
α : Type u
f : ℕ → α
m : ℕ
n : ℕ
ih : initial f (m + n) = initial f m ++ initial (fun i => f (m + i)) n
⊢ (initial f m ++ initial (fun i => f (m + i)) n :> f (m + n)) =
  initial f m ++ (initial (fun i => f (m + i)) n :> f (m + n))
    rfl

theorem SnocList.is_prefix_append (as bs : SnocList α) :
  as ≤ as ++ bs := by
α : Type u_1
as : SnocList α
bs : SnocList α
⊢ as ≤ as ++ bs
  induction bs with
  | nil =>
nil
α : Type u_1
as : SnocList α
⊢ as ≤ as ++ εₛ
    rw [SnocList.append_nil]
  | snoc bs' b ih =>
snoc
α : Type u_1
as : SnocList α
bs' : SnocList α
b : α
ih : as ≤ as ++ bs'
⊢ as ≤ as ++ (bs' :> b)
    simp
snoc
α : Type u_1
as : SnocList α
bs' : SnocList α
b : α
ih : as ≤ as ++ bs'
⊢ as ≤ (as ++ bs' :> b)
    exact Or.inr ih

theorem BethTree.prefix_closed' {α : Type u} (T : BethTree α) {l m : SnocList α} :
    l ≤ m → T.tree_node m → T.tree_node l := by
α : Type u
T : BethTree α
l : SnocList α
m : SnocList α
⊢ l ≤ m → T.tree_node m → T.tree_node l
  intro h hm
α : Type u
T : BethTree α
l : SnocList α
m : SnocList α
h : l ≤ m
hm : T.tree_node m
⊢ T.tree_node l
  induction m generalizing l with
  | nil =>
nil
α : Type u
T : BethTree α
l : SnocList α
h : l ≤ εₛ
hm : T.tree_node εₛ
⊢ T.tree_node l
    cases h
nil.refl
α : Type u
T : BethTree α
hm : T.tree_node εₛ
⊢ T.tree_node εₛ
    exact hm
  | snoc m a ih =>
snoc
α : Type u
T : BethTree α
m : SnocList α
a : α
ih : ∀ {l : SnocList α}, l ≤ m → T.tree_node m → T.tree_node l
l : SnocList α
h : l ≤ (m :> a)
hm : T.tree_node (m :> a)
⊢ T.tree_node l
    rcases h with rfl | h
snoc.inl
α : Type u
T : BethTree α
m : SnocList α
a : α
ih : ∀ {l : SnocList α}, l ≤ m → T.tree_node m → T.tree_node l
hm : T.tree_node (m :> a)
⊢ T.tree_node (m :> a)
snoc.inr
α : Type u
T : BethTree α
m : SnocList α
a : α
ih : ∀ {l : SnocList α}, l ≤ m → T.tree_node m → T.tree_node l
l : SnocList α
hm : T.tree_node (m :> a)
h : l.is_prefix m
⊢ T.tree_node l
    ·
snoc.inl
α : Type u
T : BethTree α
m : SnocList α
a : α
ih : ∀ {l : SnocList α}, l ≤ m → T.tree_node m → T.tree_node l
hm : T.tree_node (m :> a)
⊢ T.tree_node (m :> a) exact hm
    ·
snoc.inr
α : Type u
T : BethTree α
m : SnocList α
a : α
ih : ∀ {l : SnocList α}, l ≤ m → T.tree_node m → T.tree_node l
l : SnocList α
hm : T.tree_node (m :> a)
h : l.is_prefix m
⊢ T.tree_node l exact ih h (T.prefix_closed m a hm)

theorem SnocList.le_of_initial_le {α : Type u} (as : SnocList α) {f : ℕ → α} {m n : ℕ} (h : m ≤ n) :
  as ++ initial f m ≤ (as ++ initial f n) := by
α : Type u
as : SnocList α
f : ℕ → α
m : ℕ
n : ℕ
h : m ≤ n
⊢ as ++ initial f m ≤ as ++ initial f n
  induction n with
  | zero =>
zero
α : Type u
as : SnocList α
f : ℕ → α
m : ℕ
h : m ≤ 0
⊢ as ++ initial f m ≤ as ++ initial f 0
    cases h
zero.refl
α : Type u
as : SnocList α
f : ℕ → α
⊢ as ++ initial f 0 ≤ as ++ initial f 0
    exact SnocList.is_prefix_rfl _
  | succ n ih =>
succ
α : Type u
as : SnocList α
f : ℕ → α
m : ℕ
n : ℕ
ih : m ≤ n → as ++ initial f m ≤ as ++ initial f n
h : m ≤ n + 1
⊢ as ++ initial f m ≤ as ++ initial f (n + 1)
    by_cases h' : m = n + 1
pos
α : Type u
as : SnocList α
f : ℕ → α
m : ℕ
n : ℕ
ih : m ≤ n → as ++ initial f m ≤ as ++ initial f n
h : m ≤ n + 1
h' : m = n + 1
⊢ as ++ initial f m ≤ as ++ initial f (n + 1)
neg
α : Type u
as : SnocList α
f : ℕ → α
m : ℕ
n : ℕ
ih : m ≤ n → as ++ initial f m ≤ as ++ initial f n
h : m ≤ n + 1
h' : ¬m = n + 1
⊢ as ++ initial f m ≤ as ++ initial f (n + 1)
    ·
pos
α : Type u
as : SnocList α
f : ℕ → α
m : ℕ
n : ℕ
ih : m ≤ n → as ++ initial f m ≤ as ++ initial f n
h : m ≤ n + 1
h' : m = n + 1
⊢ as ++ initial f m ≤ as ++ initial f (n + 1) subst h'
pos
α : Type u
as : SnocList α
f : ℕ → α
n : ℕ
ih : n + 1 ≤ n → as ++ initial f (n + 1) ≤ as ++ initial f n
h : n + 1 ≤ n + 1
⊢ as ++ initial f (n + 1) ≤ as ++ initial f (n + 1); exact SnocList.is_prefix_rfl _
    ·
neg
α : Type u
as : SnocList α
f : ℕ → α
m : ℕ
n : ℕ
ih : m ≤ n → as ++ initial f m ≤ as ++ initial f n
h : m ≤ n + 1
h' : ¬m = n + 1
⊢ as ++ initial f m ≤ as ++ initial f (n + 1) rw [initial]
neg
α : Type u
as : SnocList α
f : ℕ → α
m : ℕ
n : ℕ
ih : m ≤ n → as ++ initial f m ≤ as ++ initial f n
h : m ≤ n + 1
h' : ¬m = n + 1
⊢ as ++ initial f m ≤ as ++ (initial f n :> f n)
      apply Or.inr
neg.h
α : Type u
as : SnocList α
f : ℕ → α
m : ℕ
n : ℕ
ih : m ≤ n → as ++ initial f m ≤ as ++ initial f n
h : m ≤ n + 1
h' : ¬m = n + 1
⊢ (as ++ initial f m).is_prefix (as.append (initial f n))
      apply ih
neg.h
α : Type u
as : SnocList α
f : ℕ → α
m : ℕ
n : ℕ
ih : m ≤ n → as ++ initial f m ≤ as ++ initial f n
h : m ≤ n + 1
h' : ¬m = n + 1
⊢ m ≤ n
      omega

def SnocList.length : SnocList α → ℕ
  | .nil      => 0
  | .snoc l _ => l.length + 1

@[simp] lemma SnocList.length_nil : (SnocList.nil : SnocList α).length = 0 := rfl

@[simp] lemma SnocList.length_snoc (l : SnocList α) (a : α) :
    (l :> a).length = l.length + 1 := rfl

theorem IsBar.nonempty {α : Type u} (T : BethTree α) {l : SnocList α} {S : SnocList α → Prop}
    (hbar : IsBar T l S) (hl : T.tree_node l) : ∃ m, S m ∧ l ≤ m := by
α : Type u
T : BethTree α
l : SnocList α
S : SnocList α → Prop
hbar : IsBar T l S
hl : T.tree_node l
⊢ ∃ m, S m ∧ l ≤ m
  haveI : Nonempty α := T.nonempty
α : Type u
T : BethTree α
l : SnocList α
S : SnocList α → Prop
hbar : IsBar T l S
hl : T.tree_node l
this : Nonempty α
⊢ ∃ m, S m ∧ l ≤ m
  let branch : ℕ → {m : SnocList α // T.tree_node m} :=
    Nat.rec ⟨l, hl⟩ (fun _ b =>
      let a := Classical.choose (T.pruned b.1 b.2)
      ⟨b.1 :> a, Classical.choose_spec (T.pruned b.1 b.2)⟩)
α : Type u
T : BethTree α
l : SnocList α
S : SnocList α → Prop
hbar : IsBar T l S
hl : T.tree_node l
this : Nonempty α
branch : ℕ → { m // T.tree_node m } := 
  fun t =>
    Nat.rec ⟨l, hl⟩
      (fun x b =>
        let a := Classical.choose ⋯;
        ⟨↑b :> a, ⋯⟩)
      t
⊢ ∃ m, S m ∧ l ≤ m
  let f : ℕ → α := fun n => Classical.choose (T.pruned (branch n).1 (branch n).2)
α : Type u
T : BethTree α
l : SnocList α
S : SnocList α → Prop
hbar : IsBar T l S
hl : T.tree_node l
this : Nonempty α
branch : ℕ → { m // T.tree_node m } := 
  fun t =>
    Nat.rec ⟨l, hl⟩
      (fun x b =>
        let a := Classical.choose ⋯;
        ⟨↑b :> a, ⋯⟩)
      t
f : ℕ → α := fun n => Classical.choose ⋯
⊢ ∃ m, S m ∧ l ≤ m
  have hbranch : ∀ n, (branch n).1 = l ++ initial f n := by
α : Type u
T : BethTree α
l : SnocList α
S : SnocList α → Prop
hbar : IsBar T l S
hl : T.tree_node l
⊢ ∃ m, S m ∧ l ≤ m
    intro n
α : Type u
T : BethTree α
l : SnocList α
S : SnocList α → Prop
hbar : IsBar T l S
hl : T.tree_node l
this : Nonempty α
branch : ℕ → { m // T.tree_node m } := 
  fun t =>
    Nat.rec ⟨l, hl⟩
      (fun x b =>
        let a := Classical.choose ⋯;
        ⟨↑b :> a, ⋯⟩)
      t
f : ℕ → α := fun n => Classical.choose ⋯
n : ℕ
⊢ ↑(branch n) = l ++ initial f n
    induction n with
    | zero =>
zero
α : Type u
T : BethTree α
l : SnocList α
S : SnocList α → Prop
hbar : IsBar T l S
hl : T.tree_node l
this : Nonempty α
branch : ℕ → { m // T.tree_node m } := 
  fun t =>
    Nat.rec ⟨l, hl⟩
      (fun x b =>
        let a := Classical.choose ⋯;
        ⟨↑b :> a, ⋯⟩)
      t
f : ℕ → α := fun n => Classical.choose ⋯
⊢ ↑(branch 0) = l ++ initial f 0
        simp [branch, initial]
    | succ n ih =>
succ
α : Type u
T : BethTree α
l : SnocList α
S : SnocList α → Prop
hbar : IsBar T l S
hl : T.tree_node l
this : Nonempty α
branch : ℕ → { m // T.tree_node m } := 
  fun t =>
    Nat.rec ⟨l, hl⟩
      (fun x b =>
        let a := Classical.choose ⋯;
        ⟨↑b :> a, ⋯⟩)
      t
f : ℕ → α := fun n => Classical.choose ⋯
n : ℕ
ih : ↑(branch n) = l ++ initial f n
⊢ ↑(branch (n + 1)) = l ++ initial f (n + 1)
        simp [branch, f, initial, ih]
  have hpath : ∀ n, T.tree_node (l ++ initial f n) := by
α : Type u
T : BethTree α
l : SnocList α
S : SnocList α → Prop
hbar : IsBar T l S
hl : T.tree_node l
⊢ ∃ m, S m ∧ l ≤ m
    intro n
α : Type u
T : BethTree α
l : SnocList α
S : SnocList α → Prop
hbar : IsBar T l S
hl : T.tree_node l
this : Nonempty α
branch : ℕ → { m // T.tree_node m } := 
  fun t =>
    Nat.rec ⟨l, hl⟩
      (fun x b =>
        let a := Classical.choose ⋯;
        ⟨↑b :> a, ⋯⟩)
      t
f : ℕ → α := fun n => Classical.choose ⋯
hbranch : ∀ (n : ℕ), ↑(branch n) = l ++ initial f n
n : ℕ
⊢ T.tree_node (l ++ initial f n)
    rw [← hbranch n]
α : Type u
T : BethTree α
l : SnocList α
S : SnocList α → Prop
hbar : IsBar T l S
hl : T.tree_node l
this : Nonempty α
branch : ℕ → { m // T.tree_node m } := 
  fun t =>
    Nat.rec ⟨l, hl⟩
      (fun x b =>
        let a := Classical.choose ⋯;
        ⟨↑b :> a, ⋯⟩)
      t
f : ℕ → α := fun n => Classical.choose ⋯
hbranch : ∀ (n : ℕ), ↑(branch n) = l ++ initial f n
n : ℕ
⊢ T.tree_node ↑(branch n)
    exact (branch n).2
  obtain ⟨n, hn⟩ := hbar f hl hpath
α : Type u
T : BethTree α
l : SnocList α
S : SnocList α → Prop
hbar : IsBar T l S
hl : T.tree_node l
this : Nonempty α
branch : ℕ → { m // T.tree_node m } := 
  fun t =>
    Nat.rec ⟨l, hl⟩
      (fun x b =>
        let a := Classical.choose ⋯;
        ⟨↑b :> a, ⋯⟩)
      t
f : ℕ → α := fun n => Classical.choose ⋯
hbranch : ∀ (n : ℕ), ↑(branch n) = l ++ initial f n
hpath : ∀ (n : ℕ), T.tree_node (l ++ initial f n)
n : ℕ
hn : S (l ++ initial f n)
⊢ ∃ m, S m ∧ l ≤ m
  refine ⟨l ++ initial f n, hn, SnocList.is_prefix_append _ _⟩

structure BethVal {α : Type u} (T : BethTree α) where
  val      : SnocList α → ℕ → Prop
  mono_val : ∀ {l m : SnocList α} {i : ℕ}, l ≤ m → T.tree_node m → val l i → val m i
  sheaf_val : ∀ {l : SnocList α} {i : ℕ}, T.tree_node l → IsBar T l {m | val m i} → val l i

def nodeBar {α : Type u} {T : BethTree α} {w : {l : SnocList α // T.tree_node l}}
    (S : Sieve w) (m : SnocList α) : Prop :=
  ∃ hm : T.tree_node m, ⟨m, hm⟩ ∈ S.carrier

def BethTreeCoverage {α : Type u} (T : BethTree α) :
    Coverage {l : SnocList α // T.tree_node l} where
  covers w S := IsBar T w.1 (nodeBar S)
  maximal := by
α : Type u
T : BethTree α
⊢ ∀ (p : { l // T.tree_node l }), IsBar T (↑p) (nodeBar (maximal_sieve p))
    intro ⟨l, hl⟩ f
α : Type u
T : BethTree α
l : SnocList α
hl : T.tree_node l
f : ℕ → α
⊢ T.tree_node ↑⟨l, hl⟩ →
  (∀ (n : ℕ), T.tree_node (↑⟨l, hl⟩ ++ initial f n)) → ∃ n, nodeBar (maximal_sieve ⟨l, hl⟩) (↑⟨l, hl⟩ ++ initial f n) hl'
α : Type u
T : BethTree α
l : SnocList α
hl : T.tree_node l
f : ℕ → α
hl' : T.tree_node ↑⟨l, hl⟩
⊢ (∀ (n : ℕ), T.tree_node (↑⟨l, hl⟩ ++ initial f n)) → ∃ n, nodeBar (maximal_sieve ⟨l, hl⟩) (↑⟨l, hl⟩ ++ initial f n) hpaths
α : Type u
T : BethTree α
l : SnocList α
hl : T.tree_node l
f : ℕ → α
hl' : T.tree_node ↑⟨l, hl⟩
hpaths : ∀ (n : ℕ), T.tree_node (↑⟨l, hl⟩ ++ initial f n)
⊢ ∃ n, nodeBar (maximal_sieve ⟨l, hl⟩) (↑⟨l, hl⟩ ++ initial f n)
    refine ⟨0, ?_⟩
α : Type u
T : BethTree α
l : SnocList α
hl : T.tree_node l
f : ℕ → α
hl' : T.tree_node ↑⟨l, hl⟩
hpaths : ∀ (n : ℕ), T.tree_node (↑⟨l, hl⟩ ++ initial f n)
⊢ nodeBar (maximal_sieve ⟨l, hl⟩) (↑⟨l, hl⟩ ++ initial f 0)
    simp only [initial, SnocList.append_nil, nodeBar, maximal_sieve, Set.mem_setOf_eq]
α : Type u
T : BethTree α
l : SnocList α
hl : T.tree_node l
f : ℕ → α
hl' : T.tree_node ↑⟨l, hl⟩
hpaths : ∀ (n : ℕ), T.tree_node (↑⟨l, hl⟩ ++ initial f n)
⊢ ∃ (h : T.tree_node l), ⟨l, hl⟩ ≤ ⟨l, ⋯⟩
    exact ⟨hl', le_refl _⟩
  stability := by
α : Type u
T : BethTree α
⊢ ∀ {p q : { l // T.tree_node l }} {U : Sieve p},
  IsBar T (↑p) (nodeBar U) → ∀ (p_le_q : p ≤ q), IsBar T (↑q) (nodeBar (pullback p_le_q U))
    intro ⟨ps, hps⟩ ⟨qs, hqs⟩
α : Type u
T : BethTree α
ps : SnocList α
hps : T.tree_node ps
qs : SnocList α
hqs : T.tree_node qs
⊢ ∀ {U : Sieve ⟨ps, hps⟩},
  IsBar T (↑⟨ps, hps⟩) (nodeBar U) →
    ∀ (p_le_q : ⟨ps, hps⟩ ≤ ⟨qs, hqs⟩), IsBar T (↑⟨qs, hqs⟩) (nodeBar (pullback p_le_q U)) S
α : Type u
T : BethTree α
ps : SnocList α
hps : T.tree_node ps
qs : SnocList α
hqs : T.tree_node qs
S : Sieve ⟨ps, hps⟩
⊢ IsBar T (↑⟨ps, hps⟩) (nodeBar S) →
  ∀ (p_le_q : ⟨ps, hps⟩ ≤ ⟨qs, hqs⟩), IsBar T (↑⟨qs, hqs⟩) (nodeBar (pullback p_le_q S)) bar_in_S
α : Type u
T : BethTree α
ps : SnocList α
hps : T.tree_node ps
qs : SnocList α
hqs : T.tree_node qs
S : Sieve ⟨ps, hps⟩
bar_in_S : IsBar T (↑⟨ps, hps⟩) (nodeBar S)
⊢ ∀ (p_le_q : ⟨ps, hps⟩ ≤ ⟨qs, hqs⟩), IsBar T (↑⟨qs, hqs⟩) (nodeBar (pullback p_le_q S)) p_le_q
α : Type u
T : BethTree α
ps : SnocList α
hps : T.tree_node ps
qs : SnocList α
hqs : T.tree_node qs
S : Sieve ⟨ps, hps⟩
bar_in_S : IsBar T (↑⟨ps, hps⟩) (nodeBar S)
p_le_q : ⟨ps, hps⟩ ≤ ⟨qs, hqs⟩
⊢ IsBar T (↑⟨qs, hqs⟩) (nodeBar (pullback p_le_q S)) f_qs
α : Type u
T : BethTree α
ps : SnocList α
hps : T.tree_node ps
qs : SnocList α
hqs : T.tree_node qs
S : Sieve ⟨ps, hps⟩
bar_in_S : IsBar T (↑⟨ps, hps⟩) (nodeBar S)
p_le_q : ⟨ps, hps⟩ ≤ ⟨qs, hqs⟩
f_qs : ℕ → α
⊢ T.tree_node ↑⟨qs, hqs⟩ →
  (∀ (n : ℕ), T.tree_node (↑⟨qs, hqs⟩ ++ initial f_qs n)) →
    ∃ n, nodeBar (pullback p_le_q S) (↑⟨qs, hqs⟩ ++ initial f_qs n) in_T
α : Type u
T : BethTree α
ps : SnocList α
hps : T.tree_node ps
qs : SnocList α
hqs : T.tree_node qs
S : Sieve ⟨ps, hps⟩
bar_in_S : IsBar T (↑⟨ps, hps⟩) (nodeBar S)
p_le_q : ⟨ps, hps⟩ ≤ ⟨qs, hqs⟩
f_qs : ℕ → α
in_T : T.tree_node ↑⟨qs, hqs⟩
⊢ (∀ (n : ℕ), T.tree_node (↑⟨qs, hqs⟩ ++ initial f_qs n)) →
  ∃ n, nodeBar (pullback p_le_q S) (↑⟨qs, hqs⟩ ++ initial f_qs n) f_in_T
α : Type u
T : BethTree α
ps : SnocList α
hps : T.tree_node ps
qs : SnocList α
hqs : T.tree_node qs
S : Sieve ⟨ps, hps⟩
bar_in_S : IsBar T (↑⟨ps, hps⟩) (nodeBar S)
p_le_q : ⟨ps, hps⟩ ≤ ⟨qs, hqs⟩
f_qs : ℕ → α
in_T : T.tree_node ↑⟨qs, hqs⟩
f_in_T : ∀ (n : ℕ), T.tree_node (↑⟨qs, hqs⟩ ++ initial f_qs n)
⊢ ∃ n, nodeBar (pullback p_le_q S) (↑⟨qs, hqs⟩ ++ initial f_qs n)

    haveI : Nonempty α := T.nonempty
α : Type u
T : BethTree α
ps : SnocList α
hps : T.tree_node ps
qs : SnocList α
hqs : T.tree_node qs
S : Sieve ⟨ps, hps⟩
bar_in_S : IsBar T (↑⟨ps, hps⟩) (nodeBar S)
p_le_q : ⟨ps, hps⟩ ≤ ⟨qs, hqs⟩
f_qs : ℕ → α
in_T : T.tree_node ↑⟨qs, hqs⟩
f_in_T : ∀ (n : ℕ), T.tree_node (↑⟨qs, hqs⟩ ++ initial f_qs n)
this : Nonempty α
⊢ ∃ n, nodeBar (pullback p_le_q S) (↑⟨qs, hqs⟩ ++ initial f_qs n)
    obtain ⟨f_ps, n_ps, rfl⟩ := le_init ps qs p_le_q
α : Type u
T : BethTree α
ps : SnocList α
hps : T.tree_node ps
S : Sieve ⟨ps, hps⟩
bar_in_S : IsBar T (↑⟨ps, hps⟩) (nodeBar S)
f_qs : ℕ → α
this : Nonempty α
f_ps : ℕ → α
n_ps : ℕ
hqs : T.tree_node (ps ++ initial f_ps n_ps)
p_le_q : ⟨ps, hps⟩ ≤ ⟨ps ++ initial f_ps n_ps, hqs⟩
in_T : T.tree_node ↑⟨ps ++ initial f_ps n_ps, hqs⟩
f_in_T : ∀ (n : ℕ), T.tree_node (↑⟨ps ++ initial f_ps n_ps, hqs⟩ ++ initial f_qs n)
⊢ ∃ n, nodeBar (pullback p_le_q S) (↑⟨ps ++ initial f_ps n_ps, hqs⟩ ++ initial f_qs n)

    let f_total (i : ℕ) := if h : i < n_ps then f_ps i else f_qs (i - n_ps)
α : Type u
T : BethTree α
ps : SnocList α
hps : T.tree_node ps
S : Sieve ⟨ps, hps⟩
bar_in_S : IsBar T (↑⟨ps, hps⟩) (nodeBar S)
f_qs : ℕ → α
this : Nonempty α
f_ps : ℕ → α
n_ps : ℕ
hqs : T.tree_node (ps ++ initial f_ps n_ps)
p_le_q : ⟨ps, hps⟩ ≤ ⟨ps ++ initial f_ps n_ps, hqs⟩
in_T : T.tree_node ↑⟨ps ++ initial f_ps n_ps, hqs⟩
f_in_T : ∀ (n : ℕ), T.tree_node (↑⟨ps ++ initial f_ps n_ps, hqs⟩ ++ initial f_qs n)
f_total : ℕ → α := fun i => if h : i < n_ps then f_ps i else f_qs (i - n_ps)
⊢ ∃ n, nodeBar (pullback p_le_q S) (↑⟨ps ++ initial f_ps n_ps, hqs⟩ ++ initial f_qs n)
    have f_total_low  : ∀ i < n_ps, f_total i = f_ps i := fun i hi => by
α : Type u
T : BethTree α
ps : SnocList α
hps : T.tree_node ps
S : Sieve ⟨ps, hps⟩
bar_in_S : IsBar T (↑⟨ps, hps⟩) (nodeBar S)
f_qs : ℕ → α
this : Nonempty α
f_ps : ℕ → α
n_ps : ℕ
hqs : T.tree_node (ps ++ initial f_ps n_ps)
p_le_q : ⟨ps, hps⟩ ≤ ⟨ps ++ initial f_ps n_ps, hqs⟩
in_T : T.tree_node ↑⟨ps ++ initial f_ps n_ps, hqs⟩
f_in_T : ∀ (n : ℕ), T.tree_node (↑⟨ps ++ initial f_ps n_ps, hqs⟩ ++ initial f_qs n)
f_total : ℕ → α := fun i => if h : i < n_ps then f_ps i else f_qs (i - n_ps)
i : ℕ
hi : i < n_ps
⊢ f_total i = f_ps i simp [f_total, hi]
    have f_total_high : ∀ i, f_total (n_ps + i) = f_qs i := fun i => by
α : Type u
T : BethTree α
ps : SnocList α
hps : T.tree_node ps
S : Sieve ⟨ps, hps⟩
bar_in_S : IsBar T (↑⟨ps, hps⟩) (nodeBar S)
f_qs : ℕ → α
this : Nonempty α
f_ps : ℕ → α
n_ps : ℕ
hqs : T.tree_node (ps ++ initial f_ps n_ps)
p_le_q : ⟨ps, hps⟩ ≤ ⟨ps ++ initial f_ps n_ps, hqs⟩
in_T : T.tree_node ↑⟨ps ++ initial f_ps n_ps, hqs⟩
f_in_T : ∀ (n : ℕ), T.tree_node (↑⟨ps ++ initial f_ps n_ps, hqs⟩ ++ initial f_qs n)
f_total : ℕ → α := fun i => if h : i < n_ps then f_ps i else f_qs (i - n_ps)
f_total_low : ∀ i < n_ps, f_total i = f_ps i
i : ℕ
⊢ f_total (n_ps + i) = f_qs i
      simp [f_total, show ¬ (n_ps + i < n_ps) from Nat.not_lt_of_le (Nat.le_add_right _ _)]
    have h_total_init : ∀ m ≤ n_ps, initial f_total m = initial f_ps m := fun m hm =>
      initial_eq_of_agree (fun i hi => f_total_low i (Nat.lt_of_lt_of_le hi hm))
α : Type u
T : BethTree α
ps : SnocList α
hps : T.tree_node ps
S : Sieve ⟨ps, hps⟩
bar_in_S : IsBar T (↑⟨ps, hps⟩) (nodeBar S)
f_qs : ℕ → α
this : Nonempty α
f_ps : ℕ → α
n_ps : ℕ
hqs : T.tree_node (ps ++ initial f_ps n_ps)
p_le_q : ⟨ps, hps⟩ ≤ ⟨ps ++ initial f_ps n_ps, hqs⟩
in_T : T.tree_node ↑⟨ps ++ initial f_ps n_ps, hqs⟩
f_in_T : ∀ (n : ℕ), T.tree_node (↑⟨ps ++ initial f_ps n_ps, hqs⟩ ++ initial f_qs n)
f_total : ℕ → α := fun i => if h : i < n_ps then f_ps i else f_qs (i - n_ps)
f_total_low : ∀ i < n_ps, f_total i = f_ps i
f_total_high : ∀ (i : ℕ), f_total (n_ps + i) = f_qs i
h_total_init : ∀ m ≤ n_ps, initial f_total m = initial f_ps m
⊢ ∃ n, nodeBar (pullback p_le_q S) (↑⟨ps ++ initial f_ps n_ps, hqs⟩ ++ initial f_qs n)
    have h_total_split : initial f_total n_ps = initial f_ps n_ps :=
      h_total_init n_ps (le_refl _)
α : Type u
T : BethTree α
ps : SnocList α
hps : T.tree_node ps
S : Sieve ⟨ps, hps⟩
bar_in_S : IsBar T (↑⟨ps, hps⟩) (nodeBar S)
f_qs : ℕ → α
this : Nonempty α
f_ps : ℕ → α
n_ps : ℕ
hqs : T.tree_node (ps ++ initial f_ps n_ps)
p_le_q : ⟨ps, hps⟩ ≤ ⟨ps ++ initial f_ps n_ps, hqs⟩
in_T : T.tree_node ↑⟨ps ++ initial f_ps n_ps, hqs⟩
f_in_T : ∀ (n : ℕ), T.tree_node (↑⟨ps ++ initial f_ps n_ps, hqs⟩ ++ initial f_qs n)
f_total : ℕ → α := fun i => if h : i < n_ps then f_ps i else f_qs (i - n_ps)
f_total_low : ∀ i < n_ps, f_total i = f_ps i
f_total_high : ∀ (i : ℕ), f_total (n_ps + i) = f_qs i
h_total_init : ∀ m ≤ n_ps, initial f_total m = initial f_ps m
h_total_split : initial f_total n_ps = initial f_ps n_ps
⊢ ∃ n, nodeBar (pullback p_le_q S) (↑⟨ps ++ initial f_ps n_ps, hqs⟩ ++ initial f_qs n)
    have hpath_total : ∀ n, T.tree_node (ps ++ initial f_total n) := by
α : Type u
T : BethTree α
⊢ ∀ {p q : { l // T.tree_node l }} {U : Sieve p},
  IsBar T (↑p) (nodeBar U) → ∀ (p_le_q : p ≤ q), IsBar T (↑q) (nodeBar (pullback p_le_q U))
      intro n
α : Type u
T : BethTree α
ps : SnocList α
hps : T.tree_node ps
S : Sieve ⟨ps, hps⟩
bar_in_S : IsBar T (↑⟨ps, hps⟩) (nodeBar S)
f_qs : ℕ → α
this : Nonempty α
f_ps : ℕ → α
n_ps : ℕ
hqs : T.tree_node (ps ++ initial f_ps n_ps)
p_le_q : ⟨ps, hps⟩ ≤ ⟨ps ++ initial f_ps n_ps, hqs⟩
in_T : T.tree_node ↑⟨ps ++ initial f_ps n_ps, hqs⟩
f_in_T : ∀ (n : ℕ), T.tree_node (↑⟨ps ++ initial f_ps n_ps, hqs⟩ ++ initial f_qs n)
f_total : ℕ → α := fun i => if h : i < n_ps then f_ps i else f_qs (i - n_ps)
f_total_low : ∀ i < n_ps, f_total i = f_ps i
f_total_high : ∀ (i : ℕ), f_total (n_ps + i) = f_qs i
h_total_init : ∀ m ≤ n_ps, initial f_total m = initial f_ps m
h_total_split : initial f_total n_ps = initial f_ps n_ps
n : ℕ
⊢ T.tree_node (ps ++ initial f_total n)
      by_cases h : n ≤ n_ps
pos
α : Type u
T : BethTree α
ps : SnocList α
hps : T.tree_node ps
S : Sieve ⟨ps, hps⟩
bar_in_S : IsBar T (↑⟨ps, hps⟩) (nodeBar S)
f_qs : ℕ → α
this : Nonempty α
f_ps : ℕ → α
n_ps : ℕ
hqs : T.tree_node (ps ++ initial f_ps n_ps)
p_le_q : ⟨ps, hps⟩ ≤ ⟨ps ++ initial f_ps n_ps, hqs⟩
in_T : T.tree_node ↑⟨ps ++ initial f_ps n_ps, hqs⟩
f_in_T : ∀ (n : ℕ), T.tree_node (↑⟨ps ++ initial f_ps n_ps, hqs⟩ ++ initial f_qs n)
f_total : ℕ → α := fun i => if h : i < n_ps then f_ps i else f_qs (i - n_ps)
f_total_low : ∀ i < n_ps, f_total i = f_ps i
f_total_high : ∀ (i : ℕ), f_total (n_ps + i) = f_qs i
h_total_init : ∀ m ≤ n_ps, initial f_total m = initial f_ps m
h_total_split : initial f_total n_ps = initial f_ps n_ps
n : ℕ
h : n ≤ n_ps
⊢ T.tree_node (ps ++ initial f_total n)
neg
α : Type u
T : BethTree α
ps : SnocList α
hps : T.tree_node ps
S : Sieve ⟨ps, hps⟩
bar_in_S : IsBar T (↑⟨ps, hps⟩) (nodeBar S)
f_qs : ℕ → α
this : Nonempty α
f_ps : ℕ → α
n_ps : ℕ
hqs : T.tree_node (ps ++ initial f_ps n_ps)
p_le_q : ⟨ps, hps⟩ ≤ ⟨ps ++ initial f_ps n_ps, hqs⟩
in_T : T.tree_node ↑⟨ps ++ initial f_ps n_ps, hqs⟩
f_in_T : ∀ (n : ℕ), T.tree_node (↑⟨ps ++ initial f_ps n_ps, hqs⟩ ++ initial f_qs n)
f_total : ℕ → α := fun i => if h : i < n_ps then f_ps i else f_qs (i - n_ps)
f_total_low : ∀ i < n_ps, f_total i = f_ps i
f_total_high : ∀ (i : ℕ), f_total (n_ps + i) = f_qs i
h_total_init : ∀ m ≤ n_ps, initial f_total m = initial f_ps m
h_total_split : initial f_total n_ps = initial f_ps n_ps
n : ℕ
h : ¬n ≤ n_ps
⊢ T.tree_node (ps ++ initial f_total n)
      ·
pos
α : Type u
T : BethTree α
ps : SnocList α
hps : T.tree_node ps
S : Sieve ⟨ps, hps⟩
bar_in_S : IsBar T (↑⟨ps, hps⟩) (nodeBar S)
f_qs : ℕ → α
this : Nonempty α
f_ps : ℕ → α
n_ps : ℕ
hqs : T.tree_node (ps ++ initial f_ps n_ps)
p_le_q : ⟨ps, hps⟩ ≤ ⟨ps ++ initial f_ps n_ps, hqs⟩
in_T : T.tree_node ↑⟨ps ++ initial f_ps n_ps, hqs⟩
f_in_T : ∀ (n : ℕ), T.tree_node (↑⟨ps ++ initial f_ps n_ps, hqs⟩ ++ initial f_qs n)
f_total : ℕ → α := fun i => if h : i < n_ps then f_ps i else f_qs (i - n_ps)
f_total_low : ∀ i < n_ps, f_total i = f_ps i
f_total_high : ∀ (i : ℕ), f_total (n_ps + i) = f_qs i
h_total_init : ∀ m ≤ n_ps, initial f_total m = initial f_ps m
h_total_split : initial f_total n_ps = initial f_ps n_ps
n : ℕ
h : n ≤ n_ps
⊢ T.tree_node (ps ++ initial f_total n) rw [h_total_init n h]
pos
α : Type u
T : BethTree α
ps : SnocList α
hps : T.tree_node ps
S : Sieve ⟨ps, hps⟩
bar_in_S : IsBar T (↑⟨ps, hps⟩) (nodeBar S)
f_qs : ℕ → α
this : Nonempty α
f_ps : ℕ → α
n_ps : ℕ
hqs : T.tree_node (ps ++ initial f_ps n_ps)
p_le_q : ⟨ps, hps⟩ ≤ ⟨ps ++ initial f_ps n_ps, hqs⟩
in_T : T.tree_node ↑⟨ps ++ initial f_ps n_ps, hqs⟩
f_in_T : ∀ (n : ℕ), T.tree_node (↑⟨ps ++ initial f_ps n_ps, hqs⟩ ++ initial f_qs n)
f_total : ℕ → α := fun i => if h : i < n_ps then f_ps i else f_qs (i - n_ps)
f_total_low : ∀ i < n_ps, f_total i = f_ps i
f_total_high : ∀ (i : ℕ), f_total (n_ps + i) = f_qs i
h_total_init : ∀ m ≤ n_ps, initial f_total m = initial f_ps m
h_total_split : initial f_total n_ps = initial f_ps n_ps
n : ℕ
h : n ≤ n_ps
⊢ T.tree_node (ps ++ initial f_ps n)
        exact T.prefix_closed' (SnocList.le_of_initial_le ps h) in_T
      ·
neg
α : Type u
T : BethTree α
ps : SnocList α
hps : T.tree_node ps
S : Sieve ⟨ps, hps⟩
bar_in_S : IsBar T (↑⟨ps, hps⟩) (nodeBar S)
f_qs : ℕ → α
this : Nonempty α
f_ps : ℕ → α
n_ps : ℕ
hqs : T.tree_node (ps ++ initial f_ps n_ps)
p_le_q : ⟨ps, hps⟩ ≤ ⟨ps ++ initial f_ps n_ps, hqs⟩
in_T : T.tree_node ↑⟨ps ++ initial f_ps n_ps, hqs⟩
f_in_T : ∀ (n : ℕ), T.tree_node (↑⟨ps ++ initial f_ps n_ps, hqs⟩ ++ initial f_qs n)
f_total : ℕ → α := fun i => if h : i < n_ps then f_ps i else f_qs (i - n_ps)
f_total_low : ∀ i < n_ps, f_total i = f_ps i
f_total_high : ∀ (i : ℕ), f_total (n_ps + i) = f_qs i
h_total_init : ∀ m ≤ n_ps, initial f_total m = initial f_ps m
h_total_split : initial f_total n_ps = initial f_ps n_ps
n : ℕ
h : ¬n ≤ n_ps
⊢ T.tree_node (ps ++ initial f_total n) push Not at h
neg
α : Type u
T : BethTree α
ps : SnocList α
hps : T.tree_node ps
S : Sieve ⟨ps, hps⟩
bar_in_S : IsBar T (↑⟨ps, hps⟩) (nodeBar S)
f_qs : ℕ → α
this : Nonempty α
f_ps : ℕ → α
n_ps : ℕ
hqs : T.tree_node (ps ++ initial f_ps n_ps)
p_le_q : ⟨ps, hps⟩ ≤ ⟨ps ++ initial f_ps n_ps, hqs⟩
in_T : T.tree_node ↑⟨ps ++ initial f_ps n_ps, hqs⟩
f_in_T : ∀ (n : ℕ), T.tree_node (↑⟨ps ++ initial f_ps n_ps, hqs⟩ ++ initial f_qs n)
f_total : ℕ → α := fun i => if h : i < n_ps then f_ps i else f_qs (i - n_ps)
f_total_low : ∀ i < n_ps, f_total i = f_ps i
f_total_high : ∀ (i : ℕ), f_total (n_ps + i) = f_qs i
h_total_init : ∀ m ≤ n_ps, initial f_total m = initial f_ps m
h_total_split : initial f_total n_ps = initial f_ps n_ps
n : ℕ
h : n_ps < n
⊢ T.tree_node (ps ++ initial f_total n)
        obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le (Nat.le_of_lt h)
neg
α : Type u
T : BethTree α
ps : SnocList α
hps : T.tree_node ps
S : Sieve ⟨ps, hps⟩
bar_in_S : IsBar T (↑⟨ps, hps⟩) (nodeBar S)
f_qs : ℕ → α
this : Nonempty α
f_ps : ℕ → α
n_ps : ℕ
hqs : T.tree_node (ps ++ initial f_ps n_ps)
p_le_q : ⟨ps, hps⟩ ≤ ⟨ps ++ initial f_ps n_ps, hqs⟩
in_T : T.tree_node ↑⟨ps ++ initial f_ps n_ps, hqs⟩
f_in_T : ∀ (n : ℕ), T.tree_node (↑⟨ps ++ initial f_ps n_ps, hqs⟩ ++ initial f_qs n)
f_total : ℕ → α := fun i => if h : i < n_ps then f_ps i else f_qs (i - n_ps)
f_total_low : ∀ i < n_ps, f_total i = f_ps i
f_total_high : ∀ (i : ℕ), f_total (n_ps + i) = f_qs i
h_total_init : ∀ m ≤ n_ps, initial f_total m = initial f_ps m
h_total_split : initial f_total n_ps = initial f_ps n_ps
k : ℕ
h : n_ps < n_ps + k
⊢ T.tree_node (ps ++ initial f_total (n_ps + k))
        rw [initial_add, ← SnocList.append_assoc, h_total_split,
            initial_eq_of_agree (fun i _ => f_total_high i)]
neg
α : Type u
T : BethTree α
ps : SnocList α
hps : T.tree_node ps
S : Sieve ⟨ps, hps⟩
bar_in_S : IsBar T (↑⟨ps, hps⟩) (nodeBar S)
f_qs : ℕ → α
this : Nonempty α
f_ps : ℕ → α
n_ps : ℕ
hqs : T.tree_node (ps ++ initial f_ps n_ps)
p_le_q : ⟨ps, hps⟩ ≤ ⟨ps ++ initial f_ps n_ps, hqs⟩
in_T : T.tree_node ↑⟨ps ++ initial f_ps n_ps, hqs⟩
f_in_T : ∀ (n : ℕ), T.tree_node (↑⟨ps ++ initial f_ps n_ps, hqs⟩ ++ initial f_qs n)
f_total : ℕ → α := fun i => if h : i < n_ps then f_ps i else f_qs (i - n_ps)
f_total_low : ∀ i < n_ps, f_total i = f_ps i
f_total_high : ∀ (i : ℕ), f_total (n_ps + i) = f_qs i
h_total_init : ∀ m ≤ n_ps, initial f_total m = initial f_ps m
h_total_split : initial f_total n_ps = initial f_ps n_ps
k : ℕ
h : n_ps < n_ps + k
⊢ T.tree_node (ps ++ initial f_ps n_ps ++ initial f_qs k)
        exact f_in_T k
    obtain ⟨m, hm_bar⟩ := bar_in_S f_total hps hpath_total
α : Type u
T : BethTree α
ps : SnocList α
hps : T.tree_node ps
S : Sieve ⟨ps, hps⟩
bar_in_S : IsBar T (↑⟨ps, hps⟩) (nodeBar S)
f_qs : ℕ → α
this : Nonempty α
f_ps : ℕ → α
n_ps : ℕ
hqs : T.tree_node (ps ++ initial f_ps n_ps)
p_le_q : ⟨ps, hps⟩ ≤ ⟨ps ++ initial f_ps n_ps, hqs⟩
in_T : T.tree_node ↑⟨ps ++ initial f_ps n_ps, hqs⟩
f_in_T : ∀ (n : ℕ), T.tree_node (↑⟨ps ++ initial f_ps n_ps, hqs⟩ ++ initial f_qs n)
f_total : ℕ → α := fun i => if h : i < n_ps then f_ps i else f_qs (i - n_ps)
f_total_low : ∀ i < n_ps, f_total i = f_ps i
f_total_high : ∀ (i : ℕ), f_total (n_ps + i) = f_qs i
h_total_init : ∀ m ≤ n_ps, initial f_total m = initial f_ps m
h_total_split : initial f_total n_ps = initial f_ps n_ps
hpath_total : ∀ (n : ℕ), T.tree_node (ps ++ initial f_total n)
m : ℕ
hm_bar : nodeBar S (↑⟨ps, hps⟩ ++ initial f_total m)
⊢ ∃ n, nodeBar (pullback p_le_q S) (↑⟨ps ++ initial f_ps n_ps, hqs⟩ ++ initial f_qs n)
    obtain ⟨hm_node, hm_mem⟩ := hm_bar
α : Type u
T : BethTree α
ps : SnocList α
hps : T.tree_node ps
S : Sieve ⟨ps, hps⟩
bar_in_S : IsBar T (↑⟨ps, hps⟩) (nodeBar S)
f_qs : ℕ → α
this : Nonempty α
f_ps : ℕ → α
n_ps : ℕ
hqs : T.tree_node (ps ++ initial f_ps n_ps)
p_le_q : ⟨ps, hps⟩ ≤ ⟨ps ++ initial f_ps n_ps, hqs⟩
in_T : T.tree_node ↑⟨ps ++ initial f_ps n_ps, hqs⟩
f_in_T : ∀ (n : ℕ), T.tree_node (↑⟨ps ++ initial f_ps n_ps, hqs⟩ ++ initial f_qs n)
f_total : ℕ → α := fun i => if h : i < n_ps then f_ps i else f_qs (i - n_ps)
f_total_low : ∀ i < n_ps, f_total i = f_ps i
f_total_high : ∀ (i : ℕ), f_total (n_ps + i) = f_qs i
h_total_init : ∀ m ≤ n_ps, initial f_total m = initial f_ps m
h_total_split : initial f_total n_ps = initial f_ps n_ps
hpath_total : ∀ (n : ℕ), T.tree_node (ps ++ initial f_total n)
m : ℕ
hm_node : T.tree_node (↑⟨ps, hps⟩ ++ initial f_total m)
hm_mem : ⟨↑⟨ps, hps⟩ ++ initial f_total m, hm_node⟩ ∈ S.carrier
⊢ ∃ n, nodeBar (pullback p_le_q S) (↑⟨ps ++ initial f_ps n_ps, hqs⟩ ++ initial f_qs n)
    by_cases hmle : n_ps ≤ m
pos
α : Type u
T : BethTree α
ps : SnocList α
hps : T.tree_node ps
S : Sieve ⟨ps, hps⟩
bar_in_S : IsBar T (↑⟨ps, hps⟩) (nodeBar S)
f_qs : ℕ → α
this : Nonempty α
f_ps : ℕ → α
n_ps : ℕ
hqs : T.tree_node (ps ++ initial f_ps n_ps)
p_le_q : ⟨ps, hps⟩ ≤ ⟨ps ++ initial f_ps n_ps, hqs⟩
in_T : T.tree_node ↑⟨ps ++ initial f_ps n_ps, hqs⟩
f_in_T : ∀ (n : ℕ), T.tree_node (↑⟨ps ++ initial f_ps n_ps, hqs⟩ ++ initial f_qs n)
f_total : ℕ → α := fun i => if h : i < n_ps then f_ps i else f_qs (i - n_ps)
f_total_low : ∀ i < n_ps, f_total i = f_ps i
f_total_high : ∀ (i : ℕ), f_total (n_ps + i) = f_qs i
h_total_init : ∀ m ≤ n_ps, initial f_total m = initial f_ps m
h_total_split : initial f_total n_ps = initial f_ps n_ps
hpath_total : ∀ (n : ℕ), T.tree_node (ps ++ initial f_total n)
m : ℕ
hm_node : T.tree_node (↑⟨ps, hps⟩ ++ initial f_total m)
hm_mem : ⟨↑⟨ps, hps⟩ ++ initial f_total m, hm_node⟩ ∈ S.carrier
hmle : n_ps ≤ m
⊢ ∃ n, nodeBar (pullback p_le_q S) (↑⟨ps ++ initial f_ps n_ps, hqs⟩ ++ initial f_qs n)
neg
α : Type u
T : BethTree α
ps : SnocList α
hps : T.tree_node ps
S : Sieve ⟨ps, hps⟩
bar_in_S : IsBar T (↑⟨ps, hps⟩) (nodeBar S)
f_qs : ℕ → α
this : Nonempty α
f_ps : ℕ → α
n_ps : ℕ
hqs : T.tree_node (ps ++ initial f_ps n_ps)
p_le_q : ⟨ps, hps⟩ ≤ ⟨ps ++ initial f_ps n_ps, hqs⟩
in_T : T.tree_node ↑⟨ps ++ initial f_ps n_ps, hqs⟩
f_in_T : ∀ (n : ℕ), T.tree_node (↑⟨ps ++ initial f_ps n_ps, hqs⟩ ++ initial f_qs n)
f_total : ℕ → α := fun i => if h : i < n_ps then f_ps i else f_qs (i - n_ps)
f_total_low : ∀ i < n_ps, f_total i = f_ps i
f_total_high : ∀ (i : ℕ), f_total (n_ps + i) = f_qs i
h_total_init : ∀ m ≤ n_ps, initial f_total m = initial f_ps m
h_total_split : initial f_total n_ps = initial f_ps n_ps
hpath_total : ∀ (n : ℕ), T.tree_node (ps ++ initial f_total n)
m : ℕ
hm_node : T.tree_node (↑⟨ps, hps⟩ ++ initial f_total m)
hm_mem : ⟨↑⟨ps, hps⟩ ++ initial f_total m, hm_node⟩ ∈ S.carrier
hmle : ¬n_ps ≤ m
⊢ ∃ n, nodeBar (pullback p_le_q S) (↑⟨ps ++ initial f_ps n_ps, hqs⟩ ++ initial f_qs n)
    ·
pos
α : Type u
T : BethTree α
ps : SnocList α
hps : T.tree_node ps
S : Sieve ⟨ps, hps⟩
bar_in_S : IsBar T (↑⟨ps, hps⟩) (nodeBar S)
f_qs : ℕ → α
this : Nonempty α
f_ps : ℕ → α
n_ps : ℕ
hqs : T.tree_node (ps ++ initial f_ps n_ps)
p_le_q : ⟨ps, hps⟩ ≤ ⟨ps ++ initial f_ps n_ps, hqs⟩
in_T : T.tree_node ↑⟨ps ++ initial f_ps n_ps, hqs⟩
f_in_T : ∀ (n : ℕ), T.tree_node (↑⟨ps ++ initial f_ps n_ps, hqs⟩ ++ initial f_qs n)
f_total : ℕ → α := fun i => if h : i < n_ps then f_ps i else f_qs (i - n_ps)
f_total_low : ∀ i < n_ps, f_total i = f_ps i
f_total_high : ∀ (i : ℕ), f_total (n_ps + i) = f_qs i
h_total_init : ∀ m ≤ n_ps, initial f_total m = initial f_ps m
h_total_split : initial f_total n_ps = initial f_ps n_ps
hpath_total : ∀ (n : ℕ), T.tree_node (ps ++ initial f_total n)
m : ℕ
hm_node : T.tree_node (↑⟨ps, hps⟩ ++ initial f_total m)
hm_mem : ⟨↑⟨ps, hps⟩ ++ initial f_total m, hm_node⟩ ∈ S.carrier
hmle : n_ps ≤ m
⊢ ∃ n, nodeBar (pullback p_le_q S) (↑⟨ps ++ initial f_ps n_ps, hqs⟩ ++ initial f_qs n) obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le hmle
pos
α : Type u
T : BethTree α
ps : SnocList α
hps : T.tree_node ps
S : Sieve ⟨ps, hps⟩
bar_in_S : IsBar T (↑⟨ps, hps⟩) (nodeBar S)
f_qs : ℕ → α
this : Nonempty α
f_ps : ℕ → α
n_ps : ℕ
hqs : T.tree_node (ps ++ initial f_ps n_ps)
p_le_q : ⟨ps, hps⟩ ≤ ⟨ps ++ initial f_ps n_ps, hqs⟩
in_T : T.tree_node ↑⟨ps ++ initial f_ps n_ps, hqs⟩
f_in_T : ∀ (n : ℕ), T.tree_node (↑⟨ps ++ initial f_ps n_ps, hqs⟩ ++ initial f_qs n)
f_total : ℕ → α := fun i => if h : i < n_ps then f_ps i else f_qs (i - n_ps)
f_total_low : ∀ i < n_ps, f_total i = f_ps i
f_total_high : ∀ (i : ℕ), f_total (n_ps + i) = f_qs i
h_total_init : ∀ m ≤ n_ps, initial f_total m = initial f_ps m
h_total_split : initial f_total n_ps = initial f_ps n_ps
hpath_total : ∀ (n : ℕ), T.tree_node (ps ++ initial f_total n)
k : ℕ
hm_node : T.tree_node (↑⟨ps, hps⟩ ++ initial f_total (n_ps + k))
hm_mem : ⟨↑⟨ps, hps⟩ ++ initial f_total (n_ps + k), hm_node⟩ ∈ S.carrier
hmle : n_ps ≤ n_ps + k
⊢ ∃ n, nodeBar (pullback p_le_q S) (↑⟨ps ++ initial f_ps n_ps, hqs⟩ ++ initial f_qs n)
      refine ⟨k, ?_⟩
pos
α : Type u
T : BethTree α
ps : SnocList α
hps : T.tree_node ps
S : Sieve ⟨ps, hps⟩
bar_in_S : IsBar T (↑⟨ps, hps⟩) (nodeBar S)
f_qs : ℕ → α
this : Nonempty α
f_ps : ℕ → α
n_ps : ℕ
hqs : T.tree_node (ps ++ initial f_ps n_ps)
p_le_q : ⟨ps, hps⟩ ≤ ⟨ps ++ initial f_ps n_ps, hqs⟩
in_T : T.tree_node ↑⟨ps ++ initial f_ps n_ps, hqs⟩
f_in_T : ∀ (n : ℕ), T.tree_node (↑⟨ps ++ initial f_ps n_ps, hqs⟩ ++ initial f_qs n)
f_total : ℕ → α := fun i => if h : i < n_ps then f_ps i else f_qs (i - n_ps)
f_total_low : ∀ i < n_ps, f_total i = f_ps i
f_total_high : ∀ (i : ℕ), f_total (n_ps + i) = f_qs i
h_total_init : ∀ m ≤ n_ps, initial f_total m = initial f_ps m
h_total_split : initial f_total n_ps = initial f_ps n_ps
hpath_total : ∀ (n : ℕ), T.tree_node (ps ++ initial f_total n)
k : ℕ
hm_node : T.tree_node (↑⟨ps, hps⟩ ++ initial f_total (n_ps + k))
hm_mem : ⟨↑⟨ps, hps⟩ ++ initial f_total (n_ps + k), hm_node⟩ ∈ S.carrier
hmle : n_ps ≤ n_ps + k
⊢ nodeBar (pullback p_le_q S) (↑⟨ps ++ initial f_ps n_ps, hqs⟩ ++ initial f_qs k)
      simp only [nodeBar, pullback, Set.mem_setOf_eq]
pos
α : Type u
T : BethTree α
ps : SnocList α
hps : T.tree_node ps
S : Sieve ⟨ps, hps⟩
bar_in_S : IsBar T (↑⟨ps, hps⟩) (nodeBar S)
f_qs : ℕ → α
this : Nonempty α
f_ps : ℕ → α
n_ps : ℕ
hqs : T.tree_node (ps ++ initial f_ps n_ps)
p_le_q : ⟨ps, hps⟩ ≤ ⟨ps ++ initial f_ps n_ps, hqs⟩
in_T : T.tree_node ↑⟨ps ++ initial f_ps n_ps, hqs⟩
f_in_T : ∀ (n : ℕ), T.tree_node (↑⟨ps ++ initial f_ps n_ps, hqs⟩ ++ initial f_qs n)
f_total : ℕ → α := fun i => if h : i < n_ps then f_ps i else f_qs (i - n_ps)
f_total_low : ∀ i < n_ps, f_total i = f_ps i
f_total_high : ∀ (i : ℕ), f_total (n_ps + i) = f_qs i
h_total_init : ∀ m ≤ n_ps, initial f_total m = initial f_ps m
h_total_split : initial f_total n_ps = initial f_ps n_ps
hpath_total : ∀ (n : ℕ), T.tree_node (ps ++ initial f_total n)
k : ℕ
hm_node : T.tree_node (↑⟨ps, hps⟩ ++ initial f_total (n_ps + k))
hm_mem : ⟨↑⟨ps, hps⟩ ++ initial f_total (n_ps + k), hm_node⟩ ∈ S.carrier
hmle : n_ps ≤ n_ps + k
⊢ ∃ (h : T.tree_node (ps ++ initial f_ps n_ps ++ initial f_qs k)),
  ⟨ps ++ initial f_ps n_ps ++ initial f_qs k, ⋯⟩ ∈ S.carrier ∧
    ⟨ps ++ initial f_ps n_ps, hqs⟩ ≤ ⟨ps ++ initial f_ps n_ps ++ initial f_qs k, ⋯⟩

      have heq : ps ++ initial f_total (n_ps + k) =
                 ps ++ initial f_ps n_ps ++ initial f_qs k := by
α : Type u
T : BethTree α
⊢ ∀ {p q : { l // T.tree_node l }} {U : Sieve p},
  IsBar T (↑p) (nodeBar U) → ∀ (p_le_q : p ≤ q), IsBar T (↑q) (nodeBar (pullback p_le_q U))
        rw [initial_add, ← SnocList.append_assoc, h_total_split,
            initial_eq_of_agree (fun i _ => f_total_high i)]
      have hm_node' : T.tree_node (ps ++ initial f_ps n_ps ++ initial f_qs k) := heq ▸ hm_node
pos
α : Type u
T : BethTree α
ps : SnocList α
hps : T.tree_node ps
S : Sieve ⟨ps, hps⟩
bar_in_S : IsBar T (↑⟨ps, hps⟩) (nodeBar S)
f_qs : ℕ → α
this : Nonempty α
f_ps : ℕ → α
n_ps : ℕ
hqs : T.tree_node (ps ++ initial f_ps n_ps)
p_le_q : ⟨ps, hps⟩ ≤ ⟨ps ++ initial f_ps n_ps, hqs⟩
in_T : T.tree_node ↑⟨ps ++ initial f_ps n_ps, hqs⟩
f_in_T : ∀ (n : ℕ), T.tree_node (↑⟨ps ++ initial f_ps n_ps, hqs⟩ ++ initial f_qs n)
f_total : ℕ → α := fun i => if h : i < n_ps then f_ps i else f_qs (i - n_ps)
f_total_low : ∀ i < n_ps, f_total i = f_ps i
f_total_high : ∀ (i : ℕ), f_total (n_ps + i) = f_qs i
h_total_init : ∀ m ≤ n_ps, initial f_total m = initial f_ps m
h_total_split : initial f_total n_ps = initial f_ps n_ps
hpath_total : ∀ (n : ℕ), T.tree_node (ps ++ initial f_total n)
k : ℕ
hm_node : T.tree_node (↑⟨ps, hps⟩ ++ initial f_total (n_ps + k))
hm_mem : ⟨↑⟨ps, hps⟩ ++ initial f_total (n_ps + k), hm_node⟩ ∈ S.carrier
hmle : n_ps ≤ n_ps + k
heq : ps ++ initial f_total (n_ps + k) = ps ++ initial f_ps n_ps ++ initial f_qs k
hm_node' : T.tree_node (ps ++ initial f_ps n_ps ++ initial f_qs k)
⊢ ∃ (h : T.tree_node (ps ++ initial f_ps n_ps ++ initial f_qs k)),
  ⟨ps ++ initial f_ps n_ps ++ initial f_qs k, ⋯⟩ ∈ S.carrier ∧
    ⟨ps ++ initial f_ps n_ps, hqs⟩ ≤ ⟨ps ++ initial f_ps n_ps ++ initial f_qs k, ⋯⟩
      have helem : (⟨ps ++ initial f_total (n_ps + k), hm_node⟩ : {l : SnocList α // T.tree_node l}) =
                   ⟨ps ++ initial f_ps n_ps ++ initial f_qs k, hm_node'⟩ := Subtype.ext heq
pos
α : Type u
T : BethTree α
ps : SnocList α
hps : T.tree_node ps
S : Sieve ⟨ps, hps⟩
bar_in_S : IsBar T (↑⟨ps, hps⟩) (nodeBar S)
f_qs : ℕ → α
this : Nonempty α
f_ps : ℕ → α
n_ps : ℕ
hqs : T.tree_node (ps ++ initial f_ps n_ps)
p_le_q : ⟨ps, hps⟩ ≤ ⟨ps ++ initial f_ps n_ps, hqs⟩
in_T : T.tree_node ↑⟨ps ++ initial f_ps n_ps, hqs⟩
f_in_T : ∀ (n : ℕ), T.tree_node (↑⟨ps ++ initial f_ps n_ps, hqs⟩ ++ initial f_qs n)
f_total : ℕ → α := fun i => if h : i < n_ps then f_ps i else f_qs (i - n_ps)
f_total_low : ∀ i < n_ps, f_total i = f_ps i
f_total_high : ∀ (i : ℕ), f_total (n_ps + i) = f_qs i
h_total_init : ∀ m ≤ n_ps, initial f_total m = initial f_ps m
h_total_split : initial f_total n_ps = initial f_ps n_ps
hpath_total : ∀ (n : ℕ), T.tree_node (ps ++ initial f_total n)
k : ℕ
hm_node : T.tree_node (↑⟨ps, hps⟩ ++ initial f_total (n_ps + k))
hm_mem : ⟨↑⟨ps, hps⟩ ++ initial f_total (n_ps + k), hm_node⟩ ∈ S.carrier
hmle : n_ps ≤ n_ps + k
heq : ps ++ initial f_total (n_ps + k) = ps ++ initial f_ps n_ps ++ initial f_qs k
hm_node' : T.tree_node (ps ++ initial f_ps n_ps ++ initial f_qs k)
helem : ⟨ps ++ initial f_total (n_ps + k), hm_node⟩ = ⟨ps ++ initial f_ps n_ps ++ initial f_qs k, hm_node'⟩
⊢ ∃ (h : T.tree_node (ps ++ initial f_ps n_ps ++ initial f_qs k)),
  ⟨ps ++ initial f_ps n_ps ++ initial f_qs k, ⋯⟩ ∈ S.carrier ∧
    ⟨ps ++ initial f_ps n_ps, hqs⟩ ≤ ⟨ps ++ initial f_ps n_ps ++ initial f_qs k, ⋯⟩
      exact ⟨hm_node', helem ▸ hm_mem, SnocList.is_prefix_append _ _⟩
    ·
neg
α : Type u
T : BethTree α
ps : SnocList α
hps : T.tree_node ps
S : Sieve ⟨ps, hps⟩
bar_in_S : IsBar T (↑⟨ps, hps⟩) (nodeBar S)
f_qs : ℕ → α
this : Nonempty α
f_ps : ℕ → α
n_ps : ℕ
hqs : T.tree_node (ps ++ initial f_ps n_ps)
p_le_q : ⟨ps, hps⟩ ≤ ⟨ps ++ initial f_ps n_ps, hqs⟩
in_T : T.tree_node ↑⟨ps ++ initial f_ps n_ps, hqs⟩
f_in_T : ∀ (n : ℕ), T.tree_node (↑⟨ps ++ initial f_ps n_ps, hqs⟩ ++ initial f_qs n)
f_total : ℕ → α := fun i => if h : i < n_ps then f_ps i else f_qs (i - n_ps)
f_total_low : ∀ i < n_ps, f_total i = f_ps i
f_total_high : ∀ (i : ℕ), f_total (n_ps + i) = f_qs i
h_total_init : ∀ m ≤ n_ps, initial f_total m = initial f_ps m
h_total_split : initial f_total n_ps = initial f_ps n_ps
hpath_total : ∀ (n : ℕ), T.tree_node (ps ++ initial f_total n)
m : ℕ
hm_node : T.tree_node (↑⟨ps, hps⟩ ++ initial f_total m)
hm_mem : ⟨↑⟨ps, hps⟩ ++ initial f_total m, hm_node⟩ ∈ S.carrier
hmle : ¬n_ps ≤ m
⊢ ∃ n, nodeBar (pullback p_le_q S) (↑⟨ps ++ initial f_ps n_ps, hqs⟩ ++ initial f_qs n) push Not at hmle
neg
α : Type u
T : BethTree α
ps : SnocList α
hps : T.tree_node ps
S : Sieve ⟨ps, hps⟩
bar_in_S : IsBar T (↑⟨ps, hps⟩) (nodeBar S)
f_qs : ℕ → α
this : Nonempty α
f_ps : ℕ → α
n_ps : ℕ
hqs : T.tree_node (ps ++ initial f_ps n_ps)
p_le_q : ⟨ps, hps⟩ ≤ ⟨ps ++ initial f_ps n_ps, hqs⟩
in_T : T.tree_node ↑⟨ps ++ initial f_ps n_ps, hqs⟩
f_in_T : ∀ (n : ℕ), T.tree_node (↑⟨ps ++ initial f_ps n_ps, hqs⟩ ++ initial f_qs n)
f_total : ℕ → α := fun i => if h : i < n_ps then f_ps i else f_qs (i - n_ps)
f_total_low : ∀ i < n_ps, f_total i = f_ps i
f_total_high : ∀ (i : ℕ), f_total (n_ps + i) = f_qs i
h_total_init : ∀ m ≤ n_ps, initial f_total m = initial f_ps m
h_total_split : initial f_total n_ps = initial f_ps n_ps
hpath_total : ∀ (n : ℕ), T.tree_node (ps ++ initial f_total n)
m : ℕ
hm_node : T.tree_node (↑⟨ps, hps⟩ ++ initial f_total m)
hm_mem : ⟨↑⟨ps, hps⟩ ++ initial f_total m, hm_node⟩ ∈ S.carrier
hmle : m < n_ps
⊢ ∃ n, nodeBar (pullback p_le_q S) (↑⟨ps ++ initial f_ps n_ps, hqs⟩ ++ initial f_qs n)
      refine ⟨0, ?_⟩
neg
α : Type u
T : BethTree α
ps : SnocList α
hps : T.tree_node ps
S : Sieve ⟨ps, hps⟩
bar_in_S : IsBar T (↑⟨ps, hps⟩) (nodeBar S)
f_qs : ℕ → α
this : Nonempty α
f_ps : ℕ → α
n_ps : ℕ
hqs : T.tree_node (ps ++ initial f_ps n_ps)
p_le_q : ⟨ps, hps⟩ ≤ ⟨ps ++ initial f_ps n_ps, hqs⟩
in_T : T.tree_node ↑⟨ps ++ initial f_ps n_ps, hqs⟩
f_in_T : ∀ (n : ℕ), T.tree_node (↑⟨ps ++ initial f_ps n_ps, hqs⟩ ++ initial f_qs n)
f_total : ℕ → α := fun i => if h : i < n_ps then f_ps i else f_qs (i - n_ps)
f_total_low : ∀ i < n_ps, f_total i = f_ps i
f_total_high : ∀ (i : ℕ), f_total (n_ps + i) = f_qs i
h_total_init : ∀ m ≤ n_ps, initial f_total m = initial f_ps m
h_total_split : initial f_total n_ps = initial f_ps n_ps
hpath_total : ∀ (n : ℕ), T.tree_node (ps ++ initial f_total n)
m : ℕ
hm_node : T.tree_node (↑⟨ps, hps⟩ ++ initial f_total m)
hm_mem : ⟨↑⟨ps, hps⟩ ++ initial f_total m, hm_node⟩ ∈ S.carrier
hmle : m < n_ps
⊢ nodeBar (pullback p_le_q S) (↑⟨ps ++ initial f_ps n_ps, hqs⟩ ++ initial f_qs 0)
      simp only [initial, SnocList.append_nil, nodeBar, pullback, Set.mem_setOf_eq]
neg
α : Type u
T : BethTree α
ps : SnocList α
hps : T.tree_node ps
S : Sieve ⟨ps, hps⟩
bar_in_S : IsBar T (↑⟨ps, hps⟩) (nodeBar S)
f_qs : ℕ → α
this : Nonempty α
f_ps : ℕ → α
n_ps : ℕ
hqs : T.tree_node (ps ++ initial f_ps n_ps)
p_le_q : ⟨ps, hps⟩ ≤ ⟨ps ++ initial f_ps n_ps, hqs⟩
in_T : T.tree_node ↑⟨ps ++ initial f_ps n_ps, hqs⟩
f_in_T : ∀ (n : ℕ), T.tree_node (↑⟨ps ++ initial f_ps n_ps, hqs⟩ ++ initial f_qs n)
f_total : ℕ → α := fun i => if h : i < n_ps then f_ps i else f_qs (i - n_ps)
f_total_low : ∀ i < n_ps, f_total i = f_ps i
f_total_high : ∀ (i : ℕ), f_total (n_ps + i) = f_qs i
h_total_init : ∀ m ≤ n_ps, initial f_total m = initial f_ps m
h_total_split : initial f_total n_ps = initial f_ps n_ps
hpath_total : ∀ (n : ℕ), T.tree_node (ps ++ initial f_total n)
m : ℕ
hm_node : T.tree_node (↑⟨ps, hps⟩ ++ initial f_total m)
hm_mem : ⟨↑⟨ps, hps⟩ ++ initial f_total m, hm_node⟩ ∈ S.carrier
hmle : m < n_ps
⊢ ∃ (h : T.tree_node (ps ++ initial f_ps n_ps)),
  ⟨ps ++ initial f_ps n_ps, ⋯⟩ ∈ S.carrier ∧ ⟨ps ++ initial f_ps n_ps, hqs⟩ ≤ ⟨ps ++ initial f_ps n_ps, ⋯⟩
      have hm_le : m ≤ n_ps := Nat.le_of_lt hmle
neg
α : Type u
T : BethTree α
ps : SnocList α
hps : T.tree_node ps
S : Sieve ⟨ps, hps⟩
bar_in_S : IsBar T (↑⟨ps, hps⟩) (nodeBar S)
f_qs : ℕ → α
this : Nonempty α
f_ps : ℕ → α
n_ps : ℕ
hqs : T.tree_node (ps ++ initial f_ps n_ps)
p_le_q : ⟨ps, hps⟩ ≤ ⟨ps ++ initial f_ps n_ps, hqs⟩
in_T : T.tree_node ↑⟨ps ++ initial f_ps n_ps, hqs⟩
f_in_T : ∀ (n : ℕ), T.tree_node (↑⟨ps ++ initial f_ps n_ps, hqs⟩ ++ initial f_qs n)
f_total : ℕ → α := fun i => if h : i < n_ps then f_ps i else f_qs (i - n_ps)
f_total_low : ∀ i < n_ps, f_total i = f_ps i
f_total_high : ∀ (i : ℕ), f_total (n_ps + i) = f_qs i
h_total_init : ∀ m ≤ n_ps, initial f_total m = initial f_ps m
h_total_split : initial f_total n_ps = initial f_ps n_ps
hpath_total : ∀ (n : ℕ), T.tree_node (ps ++ initial f_total n)
m : ℕ
hm_node : T.tree_node (↑⟨ps, hps⟩ ++ initial f_total m)
hm_mem : ⟨↑⟨ps, hps⟩ ++ initial f_total m, hm_node⟩ ∈ S.carrier
hmle : m < n_ps
hm_le : m ≤ n_ps
⊢ ∃ (h : T.tree_node (ps ++ initial f_ps n_ps)),
  ⟨ps ++ initial f_ps n_ps, ⋯⟩ ∈ S.carrier ∧ ⟨ps ++ initial f_ps n_ps, hqs⟩ ≤ ⟨ps ++ initial f_ps n_ps, ⋯⟩
      have hle_qs : ps ++ initial f_total m ≤ ps ++ initial f_ps n_ps := by
α : Type u
T : BethTree α
⊢ ∀ {p q : { l // T.tree_node l }} {U : Sieve p},
  IsBar T (↑p) (nodeBar U) → ∀ (p_le_q : p ≤ q), IsBar T (↑q) (nodeBar (pullback p_le_q U))
        rw [h_total_init m hm_le]
α : Type u
T : BethTree α
ps : SnocList α
hps : T.tree_node ps
S : Sieve ⟨ps, hps⟩
bar_in_S : IsBar T (↑⟨ps, hps⟩) (nodeBar S)
f_qs : ℕ → α
this : Nonempty α
f_ps : ℕ → α
n_ps : ℕ
hqs : T.tree_node (ps ++ initial f_ps n_ps)
p_le_q : ⟨ps, hps⟩ ≤ ⟨ps ++ initial f_ps n_ps, hqs⟩
in_T : T.tree_node ↑⟨ps ++ initial f_ps n_ps, hqs⟩
f_in_T : ∀ (n : ℕ), T.tree_node (↑⟨ps ++ initial f_ps n_ps, hqs⟩ ++ initial f_qs n)
f_total : ℕ → α := fun i => if h : i < n_ps then f_ps i else f_qs (i - n_ps)
f_total_low : ∀ i < n_ps, f_total i = f_ps i
f_total_high : ∀ (i : ℕ), f_total (n_ps + i) = f_qs i
h_total_init : ∀ m ≤ n_ps, initial f_total m = initial f_ps m
h_total_split : initial f_total n_ps = initial f_ps n_ps
hpath_total : ∀ (n : ℕ), T.tree_node (ps ++ initial f_total n)
m : ℕ
hm_node : T.tree_node (↑⟨ps, hps⟩ ++ initial f_total m)
hm_mem : ⟨↑⟨ps, hps⟩ ++ initial f_total m, hm_node⟩ ∈ S.carrier
hmle : m < n_ps
hm_le : m ≤ n_ps
⊢ ps ++ initial f_ps m ≤ ps ++ initial f_ps n_ps; exact SnocList.le_of_initial_le ps hm_le
      exact ⟨hqs, S.upward_closed hm_mem hle_qs, le_refl _⟩
  transitive := by
α : Type u
T : BethTree α
⊢ ∀ (p : { l // T.tree_node l }) (U V : Sieve p),
  IsBar T (↑p) (nodeBar U) → (∀ (q : ↑U.carrier), IsBar T (↑↑q) (nodeBar (pullback ⋯ V))) → IsBar T (↑p) (nodeBar V)
    intro ⟨l, hl⟩ U
α : Type u
T : BethTree α
l : SnocList α
hl : T.tree_node l
U : Sieve ⟨l, hl⟩
⊢ ∀ (V : Sieve ⟨l, hl⟩),
  IsBar T (↑⟨l, hl⟩) (nodeBar U) →
    (∀ (q : ↑U.carrier), IsBar T (↑↑q) (nodeBar (pullback ⋯ V))) → IsBar T (↑⟨l, hl⟩) (nodeBar V) V
α : Type u
T : BethTree α
l : SnocList α
hl : T.tree_node l
U : Sieve ⟨l, hl⟩
V : Sieve ⟨l, hl⟩
⊢ IsBar T (↑⟨l, hl⟩) (nodeBar U) →
  (∀ (q : ↑U.carrier), IsBar T (↑↑q) (nodeBar (pullback ⋯ V))) → IsBar T (↑⟨l, hl⟩) (nodeBar V) bar_in_U
α : Type u
T : BethTree α
l : SnocList α
hl : T.tree_node l
U : Sieve ⟨l, hl⟩
V : Sieve ⟨l, hl⟩
bar_in_U : IsBar T (↑⟨l, hl⟩) (nodeBar U)
⊢ (∀ (q : ↑U.carrier), IsBar T (↑↑q) (nodeBar (pullback ⋯ V))) → IsBar T (↑⟨l, hl⟩) (nodeBar V) h_UV
α : Type u
T : BethTree α
l : SnocList α
hl : T.tree_node l
U : Sieve ⟨l, hl⟩
V : Sieve ⟨l, hl⟩
bar_in_U : IsBar T (↑⟨l, hl⟩) (nodeBar U)
h_UV : ∀ (q : ↑U.carrier), IsBar T (↑↑q) (nodeBar (pullback ⋯ V))
⊢ IsBar T (↑⟨l, hl⟩) (nodeBar V) f
α : Type u
T : BethTree α
l : SnocList α
hl : T.tree_node l
U : Sieve ⟨l, hl⟩
V : Sieve ⟨l, hl⟩
bar_in_U : IsBar T (↑⟨l, hl⟩) (nodeBar U)
h_UV : ∀ (q : ↑U.carrier), IsBar T (↑↑q) (nodeBar (pullback ⋯ V))
f : ℕ → α
⊢ T.tree_node ↑⟨l, hl⟩ → (∀ (n : ℕ), T.tree_node (↑⟨l, hl⟩ ++ initial f n)) → ∃ n, nodeBar V (↑⟨l, hl⟩ ++ initial f n) in_T
α : Type u
T : BethTree α
l : SnocList α
hl : T.tree_node l
U : Sieve ⟨l, hl⟩
V : Sieve ⟨l, hl⟩
bar_in_U : IsBar T (↑⟨l, hl⟩) (nodeBar U)
h_UV : ∀ (q : ↑U.carrier), IsBar T (↑↑q) (nodeBar (pullback ⋯ V))
f : ℕ → α
in_T : T.tree_node ↑⟨l, hl⟩
⊢ (∀ (n : ℕ), T.tree_node (↑⟨l, hl⟩ ++ initial f n)) → ∃ n, nodeBar V (↑⟨l, hl⟩ ++ initial f n) f_in_T
α : Type u
T : BethTree α
l : SnocList α
hl : T.tree_node l
U : Sieve ⟨l, hl⟩
V : Sieve ⟨l, hl⟩
bar_in_U : IsBar T (↑⟨l, hl⟩) (nodeBar U)
h_UV : ∀ (q : ↑U.carrier), IsBar T (↑↑q) (nodeBar (pullback ⋯ V))
f : ℕ → α
in_T : T.tree_node ↑⟨l, hl⟩
f_in_T : ∀ (n : ℕ), T.tree_node (↑⟨l, hl⟩ ++ initial f n)
⊢ ∃ n, nodeBar V (↑⟨l, hl⟩ ++ initial f n)
    obtain ⟨n1, hn1_bar⟩ := bar_in_U f hl f_in_T
α : Type u
T : BethTree α
l : SnocList α
hl : T.tree_node l
U : Sieve ⟨l, hl⟩
V : Sieve ⟨l, hl⟩
bar_in_U : IsBar T (↑⟨l, hl⟩) (nodeBar U)
h_UV : ∀ (q : ↑U.carrier), IsBar T (↑↑q) (nodeBar (pullback ⋯ V))
f : ℕ → α
in_T : T.tree_node ↑⟨l, hl⟩
f_in_T : ∀ (n : ℕ), T.tree_node (↑⟨l, hl⟩ ++ initial f n)
n1 : ℕ
hn1_bar : nodeBar U (↑⟨l, hl⟩ ++ initial f n1)
⊢ ∃ n, nodeBar V (↑⟨l, hl⟩ ++ initial f n)
    obtain ⟨hn1_node, hn1_mem⟩ := hn1_bar
α : Type u
T : BethTree α
l : SnocList α
hl : T.tree_node l
U : Sieve ⟨l, hl⟩
V : Sieve ⟨l, hl⟩
bar_in_U : IsBar T (↑⟨l, hl⟩) (nodeBar U)
h_UV : ∀ (q : ↑U.carrier), IsBar T (↑↑q) (nodeBar (pullback ⋯ V))
f : ℕ → α
in_T : T.tree_node ↑⟨l, hl⟩
f_in_T : ∀ (n : ℕ), T.tree_node (↑⟨l, hl⟩ ++ initial f n)
n1 : ℕ
hn1_node : T.tree_node (↑⟨l, hl⟩ ++ initial f n1)
hn1_mem : ⟨↑⟨l, hl⟩ ++ initial f n1, hn1_node⟩ ∈ U.carrier
⊢ ∃ n, nodeBar V (↑⟨l, hl⟩ ++ initial f n)
    let q := l ++ initial f n1
α : Type u
T : BethTree α
l : SnocList α
hl : T.tree_node l
U : Sieve ⟨l, hl⟩
V : Sieve ⟨l, hl⟩
bar_in_U : IsBar T (↑⟨l, hl⟩) (nodeBar U)
h_UV : ∀ (q : ↑U.carrier), IsBar T (↑↑q) (nodeBar (pullback ⋯ V))
f : ℕ → α
in_T : T.tree_node ↑⟨l, hl⟩
f_in_T : ∀ (n : ℕ), T.tree_node (↑⟨l, hl⟩ ++ initial f n)
n1 : ℕ
hn1_node : T.tree_node (↑⟨l, hl⟩ ++ initial f n1)
hn1_mem : ⟨↑⟨l, hl⟩ ++ initial f n1, hn1_node⟩ ∈ U.carrier
q : SnocList α := l ++ initial f n1
⊢ ∃ n, nodeBar V (↑⟨l, hl⟩ ++ initial f n)
    let f_tail (i : ℕ) := f (n1 + i)
α : Type u
T : BethTree α
l : SnocList α
hl : T.tree_node l
U : Sieve ⟨l, hl⟩
V : Sieve ⟨l, hl⟩
bar_in_U : IsBar T (↑⟨l, hl⟩) (nodeBar U)
h_UV : ∀ (q : ↑U.carrier), IsBar T (↑↑q) (nodeBar (pullback ⋯ V))
f : ℕ → α
in_T : T.tree_node ↑⟨l, hl⟩
f_in_T : ∀ (n : ℕ), T.tree_node (↑⟨l, hl⟩ ++ initial f n)
n1 : ℕ
hn1_node : T.tree_node (↑⟨l, hl⟩ ++ initial f n1)
hn1_mem : ⟨↑⟨l, hl⟩ ++ initial f n1, hn1_node⟩ ∈ U.carrier
q : SnocList α := l ++ initial f n1
f_tail : ℕ → α := fun i => f (n1 + i)
⊢ ∃ n, nodeBar V (↑⟨l, hl⟩ ++ initial f n)
    have f_tail_in_T : ∀ n, T.tree_node (q ++ initial f_tail n) := fun n => by
α : Type u
T : BethTree α
l : SnocList α
hl : T.tree_node l
U : Sieve ⟨l, hl⟩
V : Sieve ⟨l, hl⟩
bar_in_U : IsBar T (↑⟨l, hl⟩) (nodeBar U)
h_UV : ∀ (q : ↑U.carrier), IsBar T (↑↑q) (nodeBar (pullback ⋯ V))
f : ℕ → α
in_T : T.tree_node ↑⟨l, hl⟩
f_in_T : ∀ (n : ℕ), T.tree_node (↑⟨l, hl⟩ ++ initial f n)
n1 : ℕ
hn1_node : T.tree_node (↑⟨l, hl⟩ ++ initial f n1)
hn1_mem : ⟨↑⟨l, hl⟩ ++ initial f n1, hn1_node⟩ ∈ U.carrier
q : SnocList α := l ++ initial f n1
f_tail : ℕ → α := fun i => f (n1 + i)
n : ℕ
⊢ T.tree_node (q ++ initial f_tail n)
      simpa [q, f_tail, initial_add, SnocList.append_assoc] using f_in_T (n1 + n)

    have h_cov_q := h_UV ⟨⟨q, hn1_node⟩, hn1_mem⟩
α : Type u
T : BethTree α
l : SnocList α
hl : T.tree_node l
U : Sieve ⟨l, hl⟩
V : Sieve ⟨l, hl⟩
bar_in_U : IsBar T (↑⟨l, hl⟩) (nodeBar U)
h_UV : ∀ (q : ↑U.carrier), IsBar T (↑↑q) (nodeBar (pullback ⋯ V))
f : ℕ → α
in_T : T.tree_node ↑⟨l, hl⟩
f_in_T : ∀ (n : ℕ), T.tree_node (↑⟨l, hl⟩ ++ initial f n)
n1 : ℕ
hn1_node : T.tree_node (↑⟨l, hl⟩ ++ initial f n1)
hn1_mem : ⟨↑⟨l, hl⟩ ++ initial f n1, hn1_node⟩ ∈ U.carrier
q : SnocList α := l ++ initial f n1
f_tail : ℕ → α := fun i => f (n1 + i)
f_tail_in_T : ∀ (n : ℕ), T.tree_node (q ++ initial f_tail n)
h_cov_q : IsBar T (↑↑⟨⟨q, hn1_node⟩, hn1_mem⟩) (nodeBar (pullback ⋯ V))
⊢ ∃ n, nodeBar V (↑⟨l, hl⟩ ++ initial f n)
    obtain ⟨n2, hn2_bar⟩ := h_cov_q f_tail hn1_node f_tail_in_T
α : Type u
T : BethTree α
l : SnocList α
hl : T.tree_node l
U : Sieve ⟨l, hl⟩
V : Sieve ⟨l, hl⟩
bar_in_U : IsBar T (↑⟨l, hl⟩) (nodeBar U)
h_UV : ∀ (q : ↑U.carrier), IsBar T (↑↑q) (nodeBar (pullback ⋯ V))
f : ℕ → α
in_T : T.tree_node ↑⟨l, hl⟩
f_in_T : ∀ (n : ℕ), T.tree_node (↑⟨l, hl⟩ ++ initial f n)
n1 : ℕ
hn1_node : T.tree_node (↑⟨l, hl⟩ ++ initial f n1)
hn1_mem : ⟨↑⟨l, hl⟩ ++ initial f n1, hn1_node⟩ ∈ U.carrier
q : SnocList α := l ++ initial f n1
f_tail : ℕ → α := fun i => f (n1 + i)
f_tail_in_T : ∀ (n : ℕ), T.tree_node (q ++ initial f_tail n)
h_cov_q : IsBar T (↑↑⟨⟨q, hn1_node⟩, hn1_mem⟩) (nodeBar (pullback ⋯ V))
n2 : ℕ
hn2_bar : nodeBar (pullback ⋯ V) (↑↑⟨⟨q, hn1_node⟩, hn1_mem⟩ ++ initial f_tail n2)
⊢ ∃ n, nodeBar V (↑⟨l, hl⟩ ++ initial f n)
    obtain ⟨hn2_node, hn2_mem⟩ := hn2_bar
α : Type u
T : BethTree α
l : SnocList α
hl : T.tree_node l
U : Sieve ⟨l, hl⟩
V : Sieve ⟨l, hl⟩
bar_in_U : IsBar T (↑⟨l, hl⟩) (nodeBar U)
h_UV : ∀ (q : ↑U.carrier), IsBar T (↑↑q) (nodeBar (pullback ⋯ V))
f : ℕ → α
in_T : T.tree_node ↑⟨l, hl⟩
f_in_T : ∀ (n : ℕ), T.tree_node (↑⟨l, hl⟩ ++ initial f n)
n1 : ℕ
hn1_node : T.tree_node (↑⟨l, hl⟩ ++ initial f n1)
hn1_mem : ⟨↑⟨l, hl⟩ ++ initial f n1, hn1_node⟩ ∈ U.carrier
q : SnocList α := l ++ initial f n1
f_tail : ℕ → α := fun i => f (n1 + i)
f_tail_in_T : ∀ (n : ℕ), T.tree_node (q ++ initial f_tail n)
h_cov_q : IsBar T (↑↑⟨⟨q, hn1_node⟩, hn1_mem⟩) (nodeBar (pullback ⋯ V))
n2 : ℕ
hn2_node : T.tree_node (↑↑⟨⟨q, hn1_node⟩, hn1_mem⟩ ++ initial f_tail n2)
hn2_mem : ⟨↑↑⟨⟨q, hn1_node⟩, hn1_mem⟩ ++ initial f_tail n2, hn2_node⟩ ∈ (pullback ⋯ V).carrier
⊢ ∃ n, nodeBar V (↑⟨l, hl⟩ ++ initial f n)
    simp only [pullback, Set.mem_setOf_eq] at hn2_mem
α : Type u
T : BethTree α
l : SnocList α
hl : T.tree_node l
U : Sieve ⟨l, hl⟩
V : Sieve ⟨l, hl⟩
bar_in_U : IsBar T (↑⟨l, hl⟩) (nodeBar U)
h_UV : ∀ (q : ↑U.carrier), IsBar T (↑↑q) (nodeBar (pullback ⋯ V))
f : ℕ → α
in_T : T.tree_node ↑⟨l, hl⟩
f_in_T : ∀ (n : ℕ), T.tree_node (↑⟨l, hl⟩ ++ initial f n)
n1 : ℕ
hn1_node : T.tree_node (↑⟨l, hl⟩ ++ initial f n1)
hn1_mem : ⟨↑⟨l, hl⟩ ++ initial f n1, hn1_node⟩ ∈ U.carrier
q : SnocList α := l ++ initial f n1
f_tail : ℕ → α := fun i => f (n1 + i)
f_tail_in_T : ∀ (n : ℕ), T.tree_node (q ++ initial f_tail n)
h_cov_q : IsBar T (↑↑⟨⟨q, hn1_node⟩, hn1_mem⟩) (nodeBar (pullback ⋯ V))
n2 : ℕ
hn2_node : T.tree_node (↑↑⟨⟨q, hn1_node⟩, hn1_mem⟩ ++ initial f_tail n2)
hn2_mem : ⟨q ++ initial f_tail n2, hn2_node⟩ ∈ V.carrier ∧ ⟨q, hn1_node⟩ ≤ ⟨q ++ initial f_tail n2, hn2_node⟩
⊢ ∃ n, nodeBar V (↑⟨l, hl⟩ ++ initial f n)
    refine ⟨n1 + n2, ?_⟩
α : Type u
T : BethTree α
l : SnocList α
hl : T.tree_node l
U : Sieve ⟨l, hl⟩
V : Sieve ⟨l, hl⟩
bar_in_U : IsBar T (↑⟨l, hl⟩) (nodeBar U)
h_UV : ∀ (q : ↑U.carrier), IsBar T (↑↑q) (nodeBar (pullback ⋯ V))
f : ℕ → α
in_T : T.tree_node ↑⟨l, hl⟩
f_in_T : ∀ (n : ℕ), T.tree_node (↑⟨l, hl⟩ ++ initial f n)
n1 : ℕ
hn1_node : T.tree_node (↑⟨l, hl⟩ ++ initial f n1)
hn1_mem : ⟨↑⟨l, hl⟩ ++ initial f n1, hn1_node⟩ ∈ U.carrier
q : SnocList α := l ++ initial f n1
f_tail : ℕ → α := fun i => f (n1 + i)
f_tail_in_T : ∀ (n : ℕ), T.tree_node (q ++ initial f_tail n)
h_cov_q : IsBar T (↑↑⟨⟨q, hn1_node⟩, hn1_mem⟩) (nodeBar (pullback ⋯ V))
n2 : ℕ
hn2_node : T.tree_node (↑↑⟨⟨q, hn1_node⟩, hn1_mem⟩ ++ initial f_tail n2)
hn2_mem : ⟨q ++ initial f_tail n2, hn2_node⟩ ∈ V.carrier ∧ ⟨q, hn1_node⟩ ≤ ⟨q ++ initial f_tail n2, hn2_node⟩
⊢ nodeBar V (↑⟨l, hl⟩ ++ initial f (n1 + n2))
    simp only [nodeBar]
α : Type u
T : BethTree α
l : SnocList α
hl : T.tree_node l
U : Sieve ⟨l, hl⟩
V : Sieve ⟨l, hl⟩
bar_in_U : IsBar T (↑⟨l, hl⟩) (nodeBar U)
h_UV : ∀ (q : ↑U.carrier), IsBar T (↑↑q) (nodeBar (pullback ⋯ V))
f : ℕ → α
in_T : T.tree_node ↑⟨l, hl⟩
f_in_T : ∀ (n : ℕ), T.tree_node (↑⟨l, hl⟩ ++ initial f n)
n1 : ℕ
hn1_node : T.tree_node (↑⟨l, hl⟩ ++ initial f n1)
hn1_mem : ⟨↑⟨l, hl⟩ ++ initial f n1, hn1_node⟩ ∈ U.carrier
q : SnocList α := l ++ initial f n1
f_tail : ℕ → α := fun i => f (n1 + i)
f_tail_in_T : ∀ (n : ℕ), T.tree_node (q ++ initial f_tail n)
h_cov_q : IsBar T (↑↑⟨⟨q, hn1_node⟩, hn1_mem⟩) (nodeBar (pullback ⋯ V))
n2 : ℕ
hn2_node : T.tree_node (↑↑⟨⟨q, hn1_node⟩, hn1_mem⟩ ++ initial f_tail n2)
hn2_mem : ⟨q ++ initial f_tail n2, hn2_node⟩ ∈ V.carrier ∧ ⟨q, hn1_node⟩ ≤ ⟨q ++ initial f_tail n2, hn2_node⟩
⊢ ∃ (h : T.tree_node (l ++ initial f (n1 + n2))), ⟨l ++ initial f (n1 + n2), ⋯⟩ ∈ V.carrier

    have heq : q ++ initial f_tail n2 = l ++ initial f (n1 + n2) := by
α : Type u
T : BethTree α
⊢ ∀ (p : { l // T.tree_node l }) (U V : Sieve p),
  IsBar T (↑p) (nodeBar U) → (∀ (q : ↑U.carrier), IsBar T (↑↑q) (nodeBar (pullback ⋯ V))) → IsBar T (↑p) (nodeBar V)
      simp [q, f_tail, initial_add, SnocList.append_assoc]
    have hn2_node' : T.tree_node (l ++ initial f (n1 + n2)) := heq ▸ hn2_node
α : Type u
T : BethTree α
l : SnocList α
hl : T.tree_node l
U : Sieve ⟨l, hl⟩
V : Sieve ⟨l, hl⟩
bar_in_U : IsBar T (↑⟨l, hl⟩) (nodeBar U)
h_UV : ∀ (q : ↑U.carrier), IsBar T (↑↑q) (nodeBar (pullback ⋯ V))
f : ℕ → α
in_T : T.tree_node ↑⟨l, hl⟩
f_in_T : ∀ (n : ℕ), T.tree_node (↑⟨l, hl⟩ ++ initial f n)
n1 : ℕ
hn1_node : T.tree_node (↑⟨l, hl⟩ ++ initial f n1)
hn1_mem : ⟨↑⟨l, hl⟩ ++ initial f n1, hn1_node⟩ ∈ U.carrier
q : SnocList α := l ++ initial f n1
f_tail : ℕ → α := fun i => f (n1 + i)
f_tail_in_T : ∀ (n : ℕ), T.tree_node (q ++ initial f_tail n)
h_cov_q : IsBar T (↑↑⟨⟨q, hn1_node⟩, hn1_mem⟩) (nodeBar (pullback ⋯ V))
n2 : ℕ
hn2_node : T.tree_node (↑↑⟨⟨q, hn1_node⟩, hn1_mem⟩ ++ initial f_tail n2)
hn2_mem : ⟨q ++ initial f_tail n2, hn2_node⟩ ∈ V.carrier ∧ ⟨q, hn1_node⟩ ≤ ⟨q ++ initial f_tail n2, hn2_node⟩
heq : q ++ initial f_tail n2 = l ++ initial f (n1 + n2)
hn2_node' : T.tree_node (l ++ initial f (n1 + n2))
⊢ ∃ (h : T.tree_node (l ++ initial f (n1 + n2))), ⟨l ++ initial f (n1 + n2), ⋯⟩ ∈ V.carrier
    have helem : (⟨q ++ initial f_tail n2, hn2_node⟩ : {l : SnocList α // T.tree_node l}) =
                 ⟨l ++ initial f (n1 + n2), hn2_node'⟩ := Subtype.ext heq
α : Type u
T : BethTree α
l : SnocList α
hl : T.tree_node l
U : Sieve ⟨l, hl⟩
V : Sieve ⟨l, hl⟩
bar_in_U : IsBar T (↑⟨l, hl⟩) (nodeBar U)
h_UV : ∀ (q : ↑U.carrier), IsBar T (↑↑q) (nodeBar (pullback ⋯ V))
f : ℕ → α
in_T : T.tree_node ↑⟨l, hl⟩
f_in_T : ∀ (n : ℕ), T.tree_node (↑⟨l, hl⟩ ++ initial f n)
n1 : ℕ
hn1_node : T.tree_node (↑⟨l, hl⟩ ++ initial f n1)
hn1_mem : ⟨↑⟨l, hl⟩ ++ initial f n1, hn1_node⟩ ∈ U.carrier
q : SnocList α := l ++ initial f n1
f_tail : ℕ → α := fun i => f (n1 + i)
f_tail_in_T : ∀ (n : ℕ), T.tree_node (q ++ initial f_tail n)
h_cov_q : IsBar T (↑↑⟨⟨q, hn1_node⟩, hn1_mem⟩) (nodeBar (pullback ⋯ V))
n2 : ℕ
hn2_node : T.tree_node (↑↑⟨⟨q, hn1_node⟩, hn1_mem⟩ ++ initial f_tail n2)
hn2_mem : ⟨q ++ initial f_tail n2, hn2_node⟩ ∈ V.carrier ∧ ⟨q, hn1_node⟩ ≤ ⟨q ++ initial f_tail n2, hn2_node⟩
heq : q ++ initial f_tail n2 = l ++ initial f (n1 + n2)
hn2_node' : T.tree_node (l ++ initial f (n1 + n2))
helem : ⟨q ++ initial f_tail n2, hn2_node⟩ = ⟨l ++ initial f (n1 + n2), hn2_node'⟩
⊢ ∃ (h : T.tree_node (l ++ initial f (n1 + n2))), ⟨l ++ initial f (n1 + n2), ⋯⟩ ∈ V.carrier
    exact ⟨hn2_node', helem ▸ hn2_mem.1⟩