[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l : List (Term L α)
⊢ listDecode (List.bind l listEncode) = List.map some l
[PROOFSTEP]
suffices h :
  ∀ (t : L.Term α) (l : List (Sum α (Σ i, L.Functions i))), listDecode (t.listEncode ++ l) = some t :: listDecode l
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l : List (Term L α)
h : ∀ (t : Term L α) (l : List (α ⊕ (i : ℕ) × Functions L i)), listDecode (listEncode t ++ l) = some t :: listDecode l
⊢ listDecode (List.bind l listEncode) = List.map some l
[PROOFSTEP]
induction' l with t l lih
[GOAL]
case nil
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
h : ∀ (t : Term L α) (l : List (α ⊕ (i : ℕ) × Functions L i)), listDecode (listEncode t ++ l) = some t :: listDecode l
⊢ listDecode (List.bind [] listEncode) = List.map some []
[PROOFSTEP]
rfl
[GOAL]
case cons
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
h : ∀ (t : Term L α) (l : List (α ⊕ (i : ℕ) × Functions L i)), listDecode (listEncode t ++ l) = some t :: listDecode l
t : Term L α
l : List (Term L α)
lih : listDecode (List.bind l listEncode) = List.map some l
⊢ listDecode (List.bind (t :: l) listEncode) = List.map some (t :: l)
[PROOFSTEP]
rw [cons_bind, h t (l.bind listEncode), lih, List.map]
[GOAL]
case h
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l : List (Term L α)
⊢ ∀ (t : Term L α) (l : List (α ⊕ (i : ℕ) × Functions L i)), listDecode (listEncode t ++ l) = some t :: listDecode l
[PROOFSTEP]
intro t
[GOAL]
case h
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l : List (Term L α)
t : Term L α
⊢ ∀ (l : List (α ⊕ (i : ℕ) × Functions L i)), listDecode (listEncode t ++ l) = some t :: listDecode l
[PROOFSTEP]
induction' t with a n f ts ih
[GOAL]
case h.var
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l : List (Term L α)
a : α
⊢ ∀ (l : List (α ⊕ (i : ℕ) × Functions L i)), listDecode (listEncode (var a) ++ l) = some (var a) :: listDecode l
[PROOFSTEP]
intro l
[GOAL]
case h.func
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l : List (Term L α)
n : ℕ
f : Functions L n
ts : Fin n → Term L α
ih :
  ∀ (a : Fin n) (l : List (α ⊕ (i : ℕ) × Functions L i)),
    listDecode (listEncode (ts a) ++ l) = some (ts a) :: listDecode l
⊢ ∀ (l : List (α ⊕ (i : ℕ) × Functions L i)),
    listDecode (listEncode (func f ts) ++ l) = some (func f ts) :: listDecode l
[PROOFSTEP]
intro l
[GOAL]
case h.var
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l✝ : List (Term L α)
a : α
l : List (α ⊕ (i : ℕ) × Functions L i)
⊢ listDecode (listEncode (var a) ++ l) = some (var a) :: listDecode l
[PROOFSTEP]
rw [listEncode, singleton_append, listDecode]
[GOAL]
case h.func
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l✝ : List (Term L α)
n : ℕ
f : Functions L n
ts : Fin n → Term L α
ih :
  ∀ (a : Fin n) (l : List (α ⊕ (i : ℕ) × Functions L i)),
    listDecode (listEncode (ts a) ++ l) = some (ts a) :: listDecode l
l : List (α ⊕ (i : ℕ) × Functions L i)
⊢ listDecode (listEncode (func f ts) ++ l) = some (func f ts) :: listDecode l
[PROOFSTEP]
rw [listEncode, cons_append, listDecode]
[GOAL]
case h.func
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l✝ : List (Term L α)
n : ℕ
f : Functions L n
ts : Fin n → Term L α
ih :
  ∀ (a : Fin n) (l : List (α ⊕ (i : ℕ) × Functions L i)),
    listDecode (listEncode (ts a) ++ l) = some (ts a) :: listDecode l
l : List (α ⊕ (i : ℕ) × Functions L i)
⊢ (if h :
        ∀ (i : Fin n),
          Option.isSome
              (Option.join (get? (listDecode ((List.bind (finRange n) fun i => listEncode (ts i)) ++ l)) ↑i)) =
            true then
      some
          (func f fun i =>
            Option.get (Option.join (get? (listDecode ((List.bind (finRange n) fun i => listEncode (ts i)) ++ l)) ↑i))
              (_ :
                Option.isSome
                    (Option.join (get? (listDecode ((List.bind (finRange n) fun i => listEncode (ts i)) ++ l)) ↑i)) =
                  true)) ::
        drop n (listDecode ((List.bind (finRange n) fun i => listEncode (ts i)) ++ l))
    else [none]) =
    some (func f ts) :: listDecode l
[PROOFSTEP]
have h :
  listDecode (((finRange n).bind fun i : Fin n => (ts i).listEncode) ++ l) =
    (finRange n).map (Option.some ∘ ts) ++ listDecode l :=
  by
  induction' finRange n with i l' l'ih
  · rfl
  · rw [cons_bind, List.append_assoc, ih, map_cons, l'ih, cons_append, Function.comp]
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l✝ : List (Term L α)
n : ℕ
f : Functions L n
ts : Fin n → Term L α
ih :
  ∀ (a : Fin n) (l : List (α ⊕ (i : ℕ) × Functions L i)),
    listDecode (listEncode (ts a) ++ l) = some (ts a) :: listDecode l
l : List (α ⊕ (i : ℕ) × Functions L i)
⊢ listDecode ((List.bind (finRange n) fun i => listEncode (ts i)) ++ l) =
    List.map (some ∘ ts) (finRange n) ++ listDecode l
[PROOFSTEP]
induction' finRange n with i l' l'ih
[GOAL]
case nil
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l✝ : List (Term L α)
n : ℕ
f : Functions L n
ts : Fin n → Term L α
ih :
  ∀ (a : Fin n) (l : List (α ⊕ (i : ℕ) × Functions L i)),
    listDecode (listEncode (ts a) ++ l) = some (ts a) :: listDecode l
l : List (α ⊕ (i : ℕ) × Functions L i)
⊢ listDecode ((List.bind [] fun i => listEncode (ts i)) ++ l) = List.map (some ∘ ts) [] ++ listDecode l
[PROOFSTEP]
rfl
[GOAL]
case cons
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l✝ : List (Term L α)
n : ℕ
f : Functions L n
ts : Fin n → Term L α
ih :
  ∀ (a : Fin n) (l : List (α ⊕ (i : ℕ) × Functions L i)),
    listDecode (listEncode (ts a) ++ l) = some (ts a) :: listDecode l
l : List (α ⊕ (i : ℕ) × Functions L i)
i : Fin n
l' : List (Fin n)
l'ih : listDecode ((List.bind l' fun i => listEncode (ts i)) ++ l) = List.map (some ∘ ts) l' ++ listDecode l
⊢ listDecode ((List.bind (i :: l') fun i => listEncode (ts i)) ++ l) = List.map (some ∘ ts) (i :: l') ++ listDecode l
[PROOFSTEP]
rw [cons_bind, List.append_assoc, ih, map_cons, l'ih, cons_append, Function.comp]
[GOAL]
case h.func
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l✝ : List (Term L α)
n : ℕ
f : Functions L n
ts : Fin n → Term L α
ih :
  ∀ (a : Fin n) (l : List (α ⊕ (i : ℕ) × Functions L i)),
    listDecode (listEncode (ts a) ++ l) = some (ts a) :: listDecode l
l : List (α ⊕ (i : ℕ) × Functions L i)
h :
  listDecode ((List.bind (finRange n) fun i => listEncode (ts i)) ++ l) =
    List.map (some ∘ ts) (finRange n) ++ listDecode l
⊢ (if h :
        ∀ (i : Fin n),
          Option.isSome
              (Option.join (get? (listDecode ((List.bind (finRange n) fun i => listEncode (ts i)) ++ l)) ↑i)) =
            true then
      some
          (func f fun i =>
            Option.get (Option.join (get? (listDecode ((List.bind (finRange n) fun i => listEncode (ts i)) ++ l)) ↑i))
              (_ :
                Option.isSome
                    (Option.join (get? (listDecode ((List.bind (finRange n) fun i => listEncode (ts i)) ++ l)) ↑i)) =
                  true)) ::
        drop n (listDecode ((List.bind (finRange n) fun i => listEncode (ts i)) ++ l))
    else [none]) =
    some (func f ts) :: listDecode l
[PROOFSTEP]
have h' :
  ∀ i : Fin n,
    (listDecode (((finRange n).bind fun i : Fin n => (ts i).listEncode) ++ l)).get? ↑i = some (some (ts i)) :=
  by
  intro i
  rw [h, get?_append, get?_map]
  · simp only [Option.map_eq_some', Function.comp_apply, get?_eq_some]
    refine' ⟨i, ⟨lt_of_lt_of_le i.2 (ge_of_eq (length_finRange _)), _⟩, rfl⟩
    rw [get_finRange, Fin.eta]
  · refine' lt_of_lt_of_le i.2 _
    simp
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l✝ : List (Term L α)
n : ℕ
f : Functions L n
ts : Fin n → Term L α
ih :
  ∀ (a : Fin n) (l : List (α ⊕ (i : ℕ) × Functions L i)),
    listDecode (listEncode (ts a) ++ l) = some (ts a) :: listDecode l
l : List (α ⊕ (i : ℕ) × Functions L i)
h :
  listDecode ((List.bind (finRange n) fun i => listEncode (ts i)) ++ l) =
    List.map (some ∘ ts) (finRange n) ++ listDecode l
⊢ ∀ (i : Fin n), get? (listDecode ((List.bind (finRange n) fun i => listEncode (ts i)) ++ l)) ↑i = some (some (ts i))
[PROOFSTEP]
intro i
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l✝ : List (Term L α)
n : ℕ
f : Functions L n
ts : Fin n → Term L α
ih :
  ∀ (a : Fin n) (l : List (α ⊕ (i : ℕ) × Functions L i)),
    listDecode (listEncode (ts a) ++ l) = some (ts a) :: listDecode l
l : List (α ⊕ (i : ℕ) × Functions L i)
h :
  listDecode ((List.bind (finRange n) fun i => listEncode (ts i)) ++ l) =
    List.map (some ∘ ts) (finRange n) ++ listDecode l
i : Fin n
⊢ get? (listDecode ((List.bind (finRange n) fun i => listEncode (ts i)) ++ l)) ↑i = some (some (ts i))
[PROOFSTEP]
rw [h, get?_append, get?_map]
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l✝ : List (Term L α)
n : ℕ
f : Functions L n
ts : Fin n → Term L α
ih :
  ∀ (a : Fin n) (l : List (α ⊕ (i : ℕ) × Functions L i)),
    listDecode (listEncode (ts a) ++ l) = some (ts a) :: listDecode l
l : List (α ⊕ (i : ℕ) × Functions L i)
h :
  listDecode ((List.bind (finRange n) fun i => listEncode (ts i)) ++ l) =
    List.map (some ∘ ts) (finRange n) ++ listDecode l
i : Fin n
⊢ Option.map (some ∘ ts) (get? (finRange n) ↑i) = some (some (ts i))
[PROOFSTEP]
simp only [Option.map_eq_some', Function.comp_apply, get?_eq_some]
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l✝ : List (Term L α)
n : ℕ
f : Functions L n
ts : Fin n → Term L α
ih :
  ∀ (a : Fin n) (l : List (α ⊕ (i : ℕ) × Functions L i)),
    listDecode (listEncode (ts a) ++ l) = some (ts a) :: listDecode l
l : List (α ⊕ (i : ℕ) × Functions L i)
h :
  listDecode ((List.bind (finRange n) fun i => listEncode (ts i)) ++ l) =
    List.map (some ∘ ts) (finRange n) ++ listDecode l
i : Fin n
⊢ ∃ a, (∃ h, List.get (finRange n) { val := ↑i, isLt := h } = a) ∧ some (ts a) = some (ts i)
[PROOFSTEP]
refine' ⟨i, ⟨lt_of_lt_of_le i.2 (ge_of_eq (length_finRange _)), _⟩, rfl⟩
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l✝ : List (Term L α)
n : ℕ
f : Functions L n
ts : Fin n → Term L α
ih :
  ∀ (a : Fin n) (l : List (α ⊕ (i : ℕ) × Functions L i)),
    listDecode (listEncode (ts a) ++ l) = some (ts a) :: listDecode l
l : List (α ⊕ (i : ℕ) × Functions L i)
h :
  listDecode ((List.bind (finRange n) fun i => listEncode (ts i)) ++ l) =
    List.map (some ∘ ts) (finRange n) ++ listDecode l
i : Fin n
⊢ List.get (finRange n) { val := ↑i, isLt := (_ : ↑i < length (finRange n)) } = i
[PROOFSTEP]
rw [get_finRange, Fin.eta]
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l✝ : List (Term L α)
n : ℕ
f : Functions L n
ts : Fin n → Term L α
ih :
  ∀ (a : Fin n) (l : List (α ⊕ (i : ℕ) × Functions L i)),
    listDecode (listEncode (ts a) ++ l) = some (ts a) :: listDecode l
l : List (α ⊕ (i : ℕ) × Functions L i)
h :
  listDecode ((List.bind (finRange n) fun i => listEncode (ts i)) ++ l) =
    List.map (some ∘ ts) (finRange n) ++ listDecode l
i : Fin n
⊢ ↑i < length (List.map (some ∘ ts) (finRange n))
[PROOFSTEP]
refine' lt_of_lt_of_le i.2 _
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l✝ : List (Term L α)
n : ℕ
f : Functions L n
ts : Fin n → Term L α
ih :
  ∀ (a : Fin n) (l : List (α ⊕ (i : ℕ) × Functions L i)),
    listDecode (listEncode (ts a) ++ l) = some (ts a) :: listDecode l
l : List (α ⊕ (i : ℕ) × Functions L i)
h :
  listDecode ((List.bind (finRange n) fun i => listEncode (ts i)) ++ l) =
    List.map (some ∘ ts) (finRange n) ++ listDecode l
i : Fin n
⊢ n ≤ length (List.map (some ∘ ts) (finRange n))
[PROOFSTEP]
simp
[GOAL]
case h.func
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l✝ : List (Term L α)
n : ℕ
f : Functions L n
ts : Fin n → Term L α
ih :
  ∀ (a : Fin n) (l : List (α ⊕ (i : ℕ) × Functions L i)),
    listDecode (listEncode (ts a) ++ l) = some (ts a) :: listDecode l
l : List (α ⊕ (i : ℕ) × Functions L i)
h :
  listDecode ((List.bind (finRange n) fun i => listEncode (ts i)) ++ l) =
    List.map (some ∘ ts) (finRange n) ++ listDecode l
h' : ∀ (i : Fin n), get? (listDecode ((List.bind (finRange n) fun i => listEncode (ts i)) ++ l)) ↑i = some (some (ts i))
⊢ (if h :
        ∀ (i : Fin n),
          Option.isSome
              (Option.join (get? (listDecode ((List.bind (finRange n) fun i => listEncode (ts i)) ++ l)) ↑i)) =
            true then
      some
          (func f fun i =>
            Option.get (Option.join (get? (listDecode ((List.bind (finRange n) fun i => listEncode (ts i)) ++ l)) ↑i))
              (_ :
                Option.isSome
                    (Option.join (get? (listDecode ((List.bind (finRange n) fun i => listEncode (ts i)) ++ l)) ↑i)) =
                  true)) ::
        drop n (listDecode ((List.bind (finRange n) fun i => listEncode (ts i)) ++ l))
    else [none]) =
    some (func f ts) :: listDecode l
[PROOFSTEP]
refine' (dif_pos fun i => Option.isSome_iff_exists.2 ⟨ts i, _⟩).trans _
[GOAL]
case h.func.refine'_1
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l✝ : List (Term L α)
n : ℕ
f : Functions L n
ts : Fin n → Term L α
ih :
  ∀ (a : Fin n) (l : List (α ⊕ (i : ℕ) × Functions L i)),
    listDecode (listEncode (ts a) ++ l) = some (ts a) :: listDecode l
l : List (α ⊕ (i : ℕ) × Functions L i)
h :
  listDecode ((List.bind (finRange n) fun i => listEncode (ts i)) ++ l) =
    List.map (some ∘ ts) (finRange n) ++ listDecode l
h' : ∀ (i : Fin n), get? (listDecode ((List.bind (finRange n) fun i => listEncode (ts i)) ++ l)) ↑i = some (some (ts i))
i : Fin n
⊢ Option.join (get? (listDecode ((List.bind (finRange n) fun i => listEncode (ts i)) ++ l)) ↑i) = some (ts i)
[PROOFSTEP]
rw [Option.join_eq_some, h']
[GOAL]
case h.func.refine'_2
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l✝ : List (Term L α)
n : ℕ
f : Functions L n
ts : Fin n → Term L α
ih :
  ∀ (a : Fin n) (l : List (α ⊕ (i : ℕ) × Functions L i)),
    listDecode (listEncode (ts a) ++ l) = some (ts a) :: listDecode l
l : List (α ⊕ (i : ℕ) × Functions L i)
h :
  listDecode ((List.bind (finRange n) fun i => listEncode (ts i)) ++ l) =
    List.map (some ∘ ts) (finRange n) ++ listDecode l
h' : ∀ (i : Fin n), get? (listDecode ((List.bind (finRange n) fun i => listEncode (ts i)) ++ l)) ↑i = some (some (ts i))
⊢ some
        (func f fun i =>
          Option.get (Option.join (get? (listDecode ((List.bind (finRange n) fun i => listEncode (ts i)) ++ l)) ↑i))
            (_ :
              Option.isSome
                  (Option.join (get? (listDecode ((List.bind (finRange n) fun i => listEncode (ts i)) ++ l)) ↑i)) =
                true)) ::
      drop n (listDecode ((List.bind (finRange n) fun i => listEncode (ts i)) ++ l)) =
    some (func f ts) :: listDecode l
[PROOFSTEP]
refine' congr (congr rfl (congr rfl (congr rfl (funext fun i => Option.get_of_mem _ _)))) _
[GOAL]
case h.func.refine'_2.refine'_1
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l✝ : List (Term L α)
n : ℕ
f : Functions L n
ts : Fin n → Term L α
ih :
  ∀ (a : Fin n) (l : List (α ⊕ (i : ℕ) × Functions L i)),
    listDecode (listEncode (ts a) ++ l) = some (ts a) :: listDecode l
l : List (α ⊕ (i : ℕ) × Functions L i)
h :
  listDecode ((List.bind (finRange n) fun i => listEncode (ts i)) ++ l) =
    List.map (some ∘ ts) (finRange n) ++ listDecode l
h' : ∀ (i : Fin n), get? (listDecode ((List.bind (finRange n) fun i => listEncode (ts i)) ++ l)) ↑i = some (some (ts i))
i : Fin n
⊢ ts i ∈ Option.join (get? (listDecode ((List.bind (finRange n) fun i => listEncode (ts i)) ++ l)) ↑i)
[PROOFSTEP]
simp [h']
[GOAL]
case h.func.refine'_2.refine'_2
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l✝ : List (Term L α)
n : ℕ
f : Functions L n
ts : Fin n → Term L α
ih :
  ∀ (a : Fin n) (l : List (α ⊕ (i : ℕ) × Functions L i)),
    listDecode (listEncode (ts a) ++ l) = some (ts a) :: listDecode l
l : List (α ⊕ (i : ℕ) × Functions L i)
h :
  listDecode ((List.bind (finRange n) fun i => listEncode (ts i)) ++ l) =
    List.map (some ∘ ts) (finRange n) ++ listDecode l
h' : ∀ (i : Fin n), get? (listDecode ((List.bind (finRange n) fun i => listEncode (ts i)) ++ l)) ↑i = some (some (ts i))
⊢ drop n (listDecode ((List.bind (finRange n) fun i => listEncode (ts i)) ++ l)) = listDecode l
[PROOFSTEP]
rw [h, drop_left']
[GOAL]
case h.func.refine'_2.refine'_2
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l✝ : List (Term L α)
n : ℕ
f : Functions L n
ts : Fin n → Term L α
ih :
  ∀ (a : Fin n) (l : List (α ⊕ (i : ℕ) × Functions L i)),
    listDecode (listEncode (ts a) ++ l) = some (ts a) :: listDecode l
l : List (α ⊕ (i : ℕ) × Functions L i)
h :
  listDecode ((List.bind (finRange n) fun i => listEncode (ts i)) ++ l) =
    List.map (some ∘ ts) (finRange n) ++ listDecode l
h' : ∀ (i : Fin n), get? (listDecode ((List.bind (finRange n) fun i => listEncode (ts i)) ++ l)) ↑i = some (some (ts i))
⊢ length (List.map (some ∘ ts) (finRange n)) = n
[PROOFSTEP]
rw [length_map, length_finRange]
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
t : Term L α
⊢ (fun l => Option.join (head? (listDecode l))) (listEncode t) = some t
[PROOFSTEP]
have h := listDecode_encode_list [t]
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
t : Term L α
h : listDecode (List.bind [t] listEncode) = List.map some [t]
⊢ (fun l => Option.join (head? (listDecode l))) (listEncode t) = some t
[PROOFSTEP]
rw [bind_singleton] at h
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
t : Term L α
h : listDecode (listEncode t) = List.map some [t]
⊢ (fun l => Option.join (head? (listDecode l))) (listEncode t) = some t
[PROOFSTEP]
simp only [h, Option.join, head?, List.map, Option.some_bind, id.def]
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
⊢ #((n : ℕ) × Term L (α ⊕ Fin n)) = max ℵ₀ #(α ⊕ (i : ℕ) × Functions L i)
[PROOFSTEP]
refine' le_antisymm _ _
[GOAL]
case refine'_1
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
⊢ #((n : ℕ) × Term L (α ⊕ Fin n)) ≤ max ℵ₀ #(α ⊕ (i : ℕ) × Functions L i)
[PROOFSTEP]
rw [mk_sigma]
[GOAL]
case refine'_1
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
⊢ (Cardinal.sum fun i => #(Term L (α ⊕ Fin i))) ≤ max ℵ₀ #(α ⊕ (i : ℕ) × Functions L i)
[PROOFSTEP]
refine' (sum_le_iSup_lift _).trans _
[GOAL]
case refine'_1
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
⊢ lift #ℕ * ⨆ (i : ℕ), #(Term L (α ⊕ Fin i)) ≤ max ℵ₀ #(α ⊕ (i : ℕ) × Functions L i)
[PROOFSTEP]
rw [mk_nat, lift_aleph0, mul_eq_max_of_aleph0_le_left le_rfl, max_le_iff, ciSup_le_iff' (bddAbove_range _)]
[GOAL]
case refine'_1
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
⊢ ℵ₀ ≤ max ℵ₀ #(α ⊕ (i : ℕ) × Functions L i) ∧ ∀ (i : ℕ), #(Term L (α ⊕ Fin i)) ≤ max ℵ₀ #(α ⊕ (i : ℕ) × Functions L i)
[PROOFSTEP]
refine' ⟨le_max_left _ _, fun i => card_le.trans _⟩
[GOAL]
case refine'_1
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
i : ℕ
⊢ max ℵ₀ #((α ⊕ Fin i) ⊕ (i : ℕ) × Functions L i) ≤ max ℵ₀ #(α ⊕ (i : ℕ) × Functions L i)
[PROOFSTEP]
refine' max_le (le_max_left _ _) _
[GOAL]
case refine'_1
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
i : ℕ
⊢ #((α ⊕ Fin i) ⊕ (i : ℕ) × Functions L i) ≤ max ℵ₀ #(α ⊕ (i : ℕ) × Functions L i)
[PROOFSTEP]
rw [← add_eq_max le_rfl, mk_sum, mk_sum, mk_sum, add_comm (Cardinal.lift #α), lift_add, add_assoc, lift_lift, lift_lift,
  mk_fin, lift_natCast]
[GOAL]
case refine'_1
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
i : ℕ
⊢ ↑i + (lift #α + lift #((i : ℕ) × Functions L i)) ≤ ℵ₀ + (lift #α + lift #((i : ℕ) × Functions L i))
[PROOFSTEP]
exact add_le_add_right (nat_lt_aleph0 _).le _
[GOAL]
case refine'_1
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
⊢ ⨆ (i : ℕ), #(Term L (α ⊕ Fin i)) ≠ 0
[PROOFSTEP]
rw [← one_le_iff_ne_zero]
[GOAL]
case refine'_1
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
⊢ 1 ≤ ⨆ (i : ℕ), #(Term L (α ⊕ Fin i))
[PROOFSTEP]
refine' _root_.trans _ (le_ciSup (bddAbove_range _) 1)
[GOAL]
case refine'_1
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
⊢ 1 ≤ #(Term L (α ⊕ Fin 1))
[PROOFSTEP]
rw [one_le_iff_ne_zero, mk_ne_zero_iff]
[GOAL]
case refine'_1
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
⊢ Nonempty (Term L (α ⊕ Fin 1))
[PROOFSTEP]
exact ⟨var (Sum.inr 0)⟩
[GOAL]
case refine'_2
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
⊢ max ℵ₀ #(α ⊕ (i : ℕ) × Functions L i) ≤ #((n : ℕ) × Term L (α ⊕ Fin n))
[PROOFSTEP]
rw [max_le_iff, ← infinite_iff]
[GOAL]
case refine'_2
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
⊢ Infinite ((n : ℕ) × Term L (α ⊕ Fin n)) ∧ #(α ⊕ (i : ℕ) × Functions L i) ≤ #((n : ℕ) × Term L (α ⊕ Fin n))
[PROOFSTEP]
refine' ⟨Infinite.of_injective (fun i => ⟨i + 1, var (Sum.inr i)⟩) fun i j ij => _, _⟩
[GOAL]
case refine'_2.refine'_1
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
i j : ℕ
ij : (fun i => { fst := i + 1, snd := var (Sum.inr ↑i) }) i = (fun i => { fst := i + 1, snd := var (Sum.inr ↑i) }) j
⊢ i = j
[PROOFSTEP]
cases ij
[GOAL]
case refine'_2.refine'_1.refl
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
i : ℕ
⊢ i = i
[PROOFSTEP]
rfl
[GOAL]
case refine'_2.refine'_2
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
⊢ #(α ⊕ (i : ℕ) × Functions L i) ≤ #((n : ℕ) × Term L (α ⊕ Fin n))
[PROOFSTEP]
rw [Cardinal.le_def]
[GOAL]
case refine'_2.refine'_2
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
⊢ Nonempty (α ⊕ (i : ℕ) × Functions L i ↪ (n : ℕ) × Term L (α ⊕ Fin n))
[PROOFSTEP]
refine' ⟨⟨Sum.elim (fun i => ⟨0, var (Sum.inl i)⟩) fun F => ⟨1, func F.2 fun _ => var (Sum.inr 0)⟩, _⟩⟩
[GOAL]
case refine'_2.refine'_2
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
⊢ Function.Injective
    (Sum.elim (fun i => { fst := 0, snd := var (Sum.inl i) }) fun F =>
      { fst := 1, snd := func F.snd fun x => var (Sum.inr 0) })
[PROOFSTEP]
rintro (a | a) (b | b) h
[GOAL]
case refine'_2.refine'_2.inl.inl
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
a b : α
h :
  Sum.elim (fun i => { fst := 0, snd := var (Sum.inl i) })
      (fun F => { fst := 1, snd := func F.snd fun x => var (Sum.inr 0) }) (Sum.inl a) =
    Sum.elim (fun i => { fst := 0, snd := var (Sum.inl i) })
      (fun F => { fst := 1, snd := func F.snd fun x => var (Sum.inr 0) }) (Sum.inl b)
⊢ Sum.inl a = Sum.inl b
[PROOFSTEP]
simp only [Sum.elim_inl, Sigma.mk.inj_iff, heq_eq_eq, var.injEq, Sum.inl.injEq, true_and] at h
[GOAL]
case refine'_2.refine'_2.inl.inl
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
a b : α
h : a = b
⊢ Sum.inl a = Sum.inl b
[PROOFSTEP]
rw [h]
[GOAL]
case refine'_2.refine'_2.inl.inr
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
a : α
b : (i : ℕ) × Functions L i
h :
  Sum.elim (fun i => { fst := 0, snd := var (Sum.inl i) })
      (fun F => { fst := 1, snd := func F.snd fun x => var (Sum.inr 0) }) (Sum.inl a) =
    Sum.elim (fun i => { fst := 0, snd := var (Sum.inl i) })
      (fun F => { fst := 1, snd := func F.snd fun x => var (Sum.inr 0) }) (Sum.inr b)
⊢ Sum.inl a = Sum.inr b
[PROOFSTEP]
simp only [Sum.elim_inl, Sum.elim_inr, Sigma.mk.inj_iff, false_and] at h
[GOAL]
case refine'_2.refine'_2.inr.inl
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
a : (i : ℕ) × Functions L i
b : α
h :
  Sum.elim (fun i => { fst := 0, snd := var (Sum.inl i) })
      (fun F => { fst := 1, snd := func F.snd fun x => var (Sum.inr 0) }) (Sum.inr a) =
    Sum.elim (fun i => { fst := 0, snd := var (Sum.inl i) })
      (fun F => { fst := 1, snd := func F.snd fun x => var (Sum.inr 0) }) (Sum.inl b)
⊢ Sum.inr a = Sum.inl b
[PROOFSTEP]
simp only [Sum.elim_inr, Sum.elim_inl, Sigma.mk.inj_iff, false_and] at h
[GOAL]
case refine'_2.refine'_2.inr.inr
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
a b : (i : ℕ) × Functions L i
h :
  Sum.elim (fun i => { fst := 0, snd := var (Sum.inl i) })
      (fun F => { fst := 1, snd := func F.snd fun x => var (Sum.inr 0) }) (Sum.inr a) =
    Sum.elim (fun i => { fst := 0, snd := var (Sum.inl i) })
      (fun F => { fst := 1, snd := func F.snd fun x => var (Sum.inr 0) }) (Sum.inr b)
⊢ Sum.inr a = Sum.inr b
[PROOFSTEP]
simp only [Sum.elim_inr, Sigma.mk.inj_iff, heq_eq_eq, func.injEq, true_and] at h
[GOAL]
case refine'_2.refine'_2.inr.inr
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
a b : (i : ℕ) × Functions L i
h : a.fst = b.fst ∧ HEq a.snd b.snd ∧ HEq (fun x => var (Sum.inr 0)) fun x => var (Sum.inr 0)
⊢ Sum.inr a = Sum.inr b
[PROOFSTEP]
rw [Sigma.ext_iff.2 ⟨h.1, h.2.1⟩]
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝⁴ : Structure L M
inst✝³ : Structure L N
inst✝² : Structure L P
α : Type u'
β : Type v'
inst✝¹ : Encodable α
inst✝ : Encodable ((i : ℕ) × Functions L i)
t : Term L α
⊢ (fun l => Option.join (head? (listDecode l))) (listEncode t) = some t
[PROOFSTEP]
simp only
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝⁴ : Structure L M
inst✝³ : Structure L N
inst✝² : Structure L P
α : Type u'
β : Type v'
inst✝¹ : Encodable α
inst✝ : Encodable ((i : ℕ) × Functions L i)
t : Term L α
⊢ Option.join (head? (listDecode (listEncode t))) = some t
[PROOFSTEP]
rw [← bind_singleton listEncode, listDecode_encode_list]
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝⁴ : Structure L M
inst✝³ : Structure L N
inst✝² : Structure L P
α : Type u'
β : Type v'
inst✝¹ : Encodable α
inst✝ : Encodable ((i : ℕ) × Functions L i)
t : Term L α
⊢ Option.join (head? (List.map some [t])) = some t
[PROOFSTEP]
simp only [Option.join, head?, List.map, Option.some_bind, id.def]
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
h1 : Countable α
h2 : Countable ((l : ℕ) × Functions L l)
⊢ Countable (Term L α)
[PROOFSTEP]
refine' mk_le_aleph0_iff.1 (card_le.trans (max_le_iff.2 _))
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
h1 : Countable α
h2 : Countable ((l : ℕ) × Functions L l)
⊢ ℵ₀ ≤ ℵ₀ ∧ #(α ⊕ (i : ℕ) × Functions L i) ≤ ℵ₀
[PROOFSTEP]
simp only [le_refl, mk_sum, add_le_aleph0, lift_le_aleph0, true_and_iff]
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
h1 : Countable α
h2 : Countable ((l : ℕ) × Functions L l)
⊢ #α ≤ ℵ₀ ∧ #((i : ℕ) × Functions L i) ≤ ℵ₀
[PROOFSTEP]
exact ⟨Cardinal.mk_le_aleph0, Cardinal.mk_le_aleph0⟩
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
m : ℕ
φ : BoundedFormula L α m
n : ℕ
ψ : BoundedFormula L α n
h : m = n
⊢ BoundedFormula L α n = BoundedFormula L α m
[PROOFSTEP]
rw [h]
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n₁ : ℕ
t₁ : Term L (α ⊕ Fin n₁)
n₂ : ℕ
t₂ : Term L (α ⊕ Fin n₂)
l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)
h : n₁ = n₂
⊢ Term L (α ⊕ Fin n₂) = Term L (α ⊕ Fin n₁)
[PROOFSTEP]
rw [h]
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n₁ : ℕ
t₁ : Term L (α ⊕ Fin n₁)
n₂ : ℕ
t₂ : Term L (α ⊕ Fin n₂)
l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)
⊢ sizeOf l ≤ max 1 (sizeOf (Sum.inl { fst := n₁, snd := t₁ } :: Sum.inl { fst := n₂, snd := t₂ } :: l))
[PROOFSTEP]
simp only [SizeOf.sizeOf, List._sizeOf_1, ← add_assoc]
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n₁ : ℕ
t₁ : Term L (α ⊕ Fin n₁)
n₂ : ℕ
t₂ : Term L (α ⊕ Fin n₂)
l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)
⊢ List.rec 1 (fun head tail tail_ih => 1 + Sum._sizeOf_1 head + tail_ih) l ≤
    max 1
      (1 + Sum._sizeOf_1 (Sum.inl { fst := n₁, snd := t₁ }) + 1 + Sum._sizeOf_1 (Sum.inl { fst := n₂, snd := t₂ }) +
        List.rec 1 (fun head tail tail_ih => 1 + Sum._sizeOf_1 head + tail_ih) l)
[PROOFSTEP]
exact le_max_of_le_right le_add_self
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n : ℕ
R : Relations L n
k : ℕ
l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)
h : ∀ (i : Fin n), Option.isSome (Option.join (get? (List.map Sum.getLeft? l) ↑i)) = true
h' :
  ∀ (i : Fin n),
    (Option.get (Option.join (get? (List.map Sum.getLeft? l) ↑i))
          (_ : Option.isSome (Option.join (get? (List.map Sum.getLeft? l) ↑i)) = true)).fst =
      k
i : Fin n
⊢ Term L
      (α ⊕
        Fin
          (Option.get (Option.join (get? (List.map Sum.getLeft? l) ↑i))
              (_ : Option.isSome (Option.join (get? (List.map Sum.getLeft? l) ↑i)) = true)).fst) =
    Term L (α ⊕ Fin k)
[PROOFSTEP]
rw [h' i]
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)
⊢ sizeOf ↑(listDecode l).snd < 1 + (1 + 1) + sizeOf l
[PROOFSTEP]
refine' lt_of_le_of_lt (listDecode l).2.2 (max_lt _ (Nat.lt_add_of_pos_left (by decide)))
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)
⊢ 0 < 1 + (1 + 1)
[PROOFSTEP]
decide
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)
⊢ 1 < 1 + (1 + 1) + sizeOf l
[PROOFSTEP]
rw [add_assoc, lt_add_iff_pos_right, add_pos_iff]
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)
⊢ 0 < 1 + 1 ∨ 0 < sizeOf l
[PROOFSTEP]
exact Or.inl zero_lt_two
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l : List ((n : ℕ) × BoundedFormula L α n)
⊢ (listDecode (List.bind l fun φ => listEncode φ.snd)).fst = headI l
[PROOFSTEP]
suffices h :
  ∀ (φ : Σ n, L.BoundedFormula α n) (l),
    (listDecode (listEncode φ.2 ++ l)).1 = φ ∧ (listDecode (listEncode φ.2 ++ l)).2.1 = l
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l : List ((n : ℕ) × BoundedFormula L α n)
h :
  ∀ (φ : (n : ℕ) × BoundedFormula L α n) (l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)),
    (listDecode (listEncode φ.snd ++ l)).fst = φ ∧ ↑(listDecode (listEncode φ.snd ++ l)).snd = l
⊢ (listDecode (List.bind l fun φ => listEncode φ.snd)).fst = headI l
[PROOFSTEP]
induction' l with φ l _
[GOAL]
case nil
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
h :
  ∀ (φ : (n : ℕ) × BoundedFormula L α n) (l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)),
    (listDecode (listEncode φ.snd ++ l)).fst = φ ∧ ↑(listDecode (listEncode φ.snd ++ l)).snd = l
⊢ (listDecode (List.bind [] fun φ => listEncode φ.snd)).fst = headI []
[PROOFSTEP]
rw [List.nil_bind]
[GOAL]
case nil
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
h :
  ∀ (φ : (n : ℕ) × BoundedFormula L α n) (l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)),
    (listDecode (listEncode φ.snd ++ l)).fst = φ ∧ ↑(listDecode (listEncode φ.snd ++ l)).snd = l
⊢ (listDecode []).fst = headI []
[PROOFSTEP]
simp [listDecode]
[GOAL]
case cons
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
h :
  ∀ (φ : (n : ℕ) × BoundedFormula L α n) (l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)),
    (listDecode (listEncode φ.snd ++ l)).fst = φ ∧ ↑(listDecode (listEncode φ.snd ++ l)).snd = l
φ : (n : ℕ) × BoundedFormula L α n
l : List ((n : ℕ) × BoundedFormula L α n)
tail_ih✝ : (listDecode (List.bind l fun φ => listEncode φ.snd)).fst = headI l
⊢ (listDecode (List.bind (φ :: l) fun φ => listEncode φ.snd)).fst = headI (φ :: l)
[PROOFSTEP]
rw [cons_bind, (h φ _).1, headI_cons]
[GOAL]
case h
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l : List ((n : ℕ) × BoundedFormula L α n)
⊢ ∀ (φ : (n : ℕ) × BoundedFormula L α n) (l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)),
    (listDecode (listEncode φ.snd ++ l)).fst = φ ∧ ↑(listDecode (listEncode φ.snd ++ l)).snd = l
[PROOFSTEP]
rintro ⟨n, φ⟩
[GOAL]
case h.mk
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l : List ((n : ℕ) × BoundedFormula L α n)
n : ℕ
φ : BoundedFormula L α n
⊢ ∀ (l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)),
    (listDecode (listEncode { fst := n, snd := φ }.snd ++ l)).fst = { fst := n, snd := φ } ∧
      ↑(listDecode (listEncode { fst := n, snd := φ }.snd ++ l)).snd = l
[PROOFSTEP]
induction' φ with _ _ _ _ φ_n φ_l φ_R ts _ _ _ ih1 ih2 _ _ ih
[GOAL]
case h.mk.falsum
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l : List ((n : ℕ) × BoundedFormula L α n)
n n✝ : ℕ
⊢ ∀ (l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)),
    (listDecode (listEncode { fst := n✝, snd := falsum }.snd ++ l)).fst = { fst := n✝, snd := falsum } ∧
      ↑(listDecode (listEncode { fst := n✝, snd := falsum }.snd ++ l)).snd = l
[PROOFSTEP]
intro l
[GOAL]
case h.mk.equal
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l : List ((n : ℕ) × BoundedFormula L α n)
n n✝ : ℕ
t₁✝ t₂✝ : Term L (α ⊕ Fin n✝)
⊢ ∀ (l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)),
    (listDecode (listEncode { fst := n✝, snd := equal t₁✝ t₂✝ }.snd ++ l)).fst = { fst := n✝, snd := equal t₁✝ t₂✝ } ∧
      ↑(listDecode (listEncode { fst := n✝, snd := equal t₁✝ t₂✝ }.snd ++ l)).snd = l
[PROOFSTEP]
intro l
[GOAL]
case h.mk.rel
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l : List ((n : ℕ) × BoundedFormula L α n)
n φ_n φ_l : ℕ
φ_R : Relations L φ_l
ts : Fin φ_l → Term L (α ⊕ Fin φ_n)
⊢ ∀ (l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)),
    (listDecode (listEncode { fst := φ_n, snd := rel φ_R ts }.snd ++ l)).fst = { fst := φ_n, snd := rel φ_R ts } ∧
      ↑(listDecode (listEncode { fst := φ_n, snd := rel φ_R ts }.snd ++ l)).snd = l
[PROOFSTEP]
intro l
[GOAL]
case h.mk.imp
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l : List ((n : ℕ) × BoundedFormula L α n)
n n✝ : ℕ
f₁✝ f₂✝ : BoundedFormula L α n✝
ih1 :
  ∀ (l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)),
    (listDecode (listEncode { fst := n✝, snd := f₁✝ }.snd ++ l)).fst = { fst := n✝, snd := f₁✝ } ∧
      ↑(listDecode (listEncode { fst := n✝, snd := f₁✝ }.snd ++ l)).snd = l
ih2 :
  ∀ (l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)),
    (listDecode (listEncode { fst := n✝, snd := f₂✝ }.snd ++ l)).fst = { fst := n✝, snd := f₂✝ } ∧
      ↑(listDecode (listEncode { fst := n✝, snd := f₂✝ }.snd ++ l)).snd = l
⊢ ∀ (l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)),
    (listDecode (listEncode { fst := n✝, snd := f₁✝ ⟹ f₂✝ }.snd ++ l)).fst = { fst := n✝, snd := f₁✝ ⟹ f₂✝ } ∧
      ↑(listDecode (listEncode { fst := n✝, snd := f₁✝ ⟹ f₂✝ }.snd ++ l)).snd = l
[PROOFSTEP]
intro l
[GOAL]
case h.mk.all
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l : List ((n : ℕ) × BoundedFormula L α n)
n n✝ : ℕ
f✝ : BoundedFormula L α (n✝ + 1)
ih :
  ∀ (l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)),
    (listDecode (listEncode { fst := n✝ + 1, snd := f✝ }.snd ++ l)).fst = { fst := n✝ + 1, snd := f✝ } ∧
      ↑(listDecode (listEncode { fst := n✝ + 1, snd := f✝ }.snd ++ l)).snd = l
⊢ ∀ (l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)),
    (listDecode (listEncode { fst := n✝, snd := ∀'f✝ }.snd ++ l)).fst = { fst := n✝, snd := ∀'f✝ } ∧
      ↑(listDecode (listEncode { fst := n✝, snd := ∀'f✝ }.snd ++ l)).snd = l
[PROOFSTEP]
intro l
[GOAL]
case h.mk.falsum
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l✝ : List ((n : ℕ) × BoundedFormula L α n)
n n✝ : ℕ
l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)
⊢ (listDecode (listEncode { fst := n✝, snd := falsum }.snd ++ l)).fst = { fst := n✝, snd := falsum } ∧
    ↑(listDecode (listEncode { fst := n✝, snd := falsum }.snd ++ l)).snd = l
[PROOFSTEP]
rw [listEncode, singleton_append, listDecode]
[GOAL]
case h.mk.falsum
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l✝ : List ((n : ℕ) × BoundedFormula L α n)
n n✝ : ℕ
l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)
⊢ ({ fst := { fst := n✝, snd := falsum }.fst, snd := falsum },
          { val := l,
            property :=
              (_ : sizeOf l ≤ max 1 (sizeOf (Sum.inr (Sum.inr ({ fst := n✝, snd := falsum }.fst + 2)) :: l))) }).fst =
      { fst := n✝, snd := falsum } ∧
    ↑({ fst := { fst := n✝, snd := falsum }.fst, snd := falsum },
            { val := l,
              property :=
                (_ : sizeOf l ≤ max 1 (sizeOf (Sum.inr (Sum.inr ({ fst := n✝, snd := falsum }.fst + 2)) :: l))) }).snd =
      l
[PROOFSTEP]
simp only [eq_self_iff_true, heq_iff_eq, and_self_iff]
[GOAL]
case h.mk.equal
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l✝ : List ((n : ℕ) × BoundedFormula L α n)
n n✝ : ℕ
t₁✝ t₂✝ : Term L (α ⊕ Fin n✝)
l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)
⊢ (listDecode (listEncode { fst := n✝, snd := equal t₁✝ t₂✝ }.snd ++ l)).fst = { fst := n✝, snd := equal t₁✝ t₂✝ } ∧
    ↑(listDecode (listEncode { fst := n✝, snd := equal t₁✝ t₂✝ }.snd ++ l)).snd = l
[PROOFSTEP]
rw [listEncode, cons_append, cons_append, listDecode, dif_pos]
[GOAL]
case h.mk.equal
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l✝ : List ((n : ℕ) × BoundedFormula L α n)
n n✝ : ℕ
t₁✝ t₂✝ : Term L (α ⊕ Fin n✝)
l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)
⊢ ({ fst := { fst := n✝, snd := equal t₁✝ t₂✝ }.fst,
            snd :=
              equal t₁✝
                (Eq.mp
                  (_ :
                    Term L (α ⊕ Fin { fst := n✝, snd := equal t₁✝ t₂✝ }.fst) =
                      Term L (α ⊕ Fin { fst := n✝, snd := equal t₁✝ t₂✝ }.fst))
                  t₂✝) },
          { val := [] ++ l,
            property :=
              (_ :
                sizeOf ([] ++ l) ≤
                  max 1
                    (sizeOf
                      (Sum.inl { fst := { fst := n✝, snd := equal t₁✝ t₂✝ }.fst, snd := t₁✝ } ::
                        Sum.inl { fst := { fst := n✝, snd := equal t₁✝ t₂✝ }.fst, snd := t₂✝ } :: ([] ++ l)))) }).fst =
      { fst := n✝, snd := equal t₁✝ t₂✝ } ∧
    ↑({ fst := { fst := n✝, snd := equal t₁✝ t₂✝ }.fst,
              snd :=
                equal t₁✝
                  (Eq.mp
                    (_ :
                      Term L (α ⊕ Fin { fst := n✝, snd := equal t₁✝ t₂✝ }.fst) =
                        Term L (α ⊕ Fin { fst := n✝, snd := equal t₁✝ t₂✝ }.fst))
                    t₂✝) },
            { val := [] ++ l,
              property :=
                (_ :
                  sizeOf ([] ++ l) ≤
                    max 1
                      (sizeOf
                        (Sum.inl { fst := { fst := n✝, snd := equal t₁✝ t₂✝ }.fst, snd := t₁✝ } ::
                          Sum.inl { fst := { fst := n✝, snd := equal t₁✝ t₂✝ }.fst, snd := t₂✝ } ::
                            ([] ++ l)))) }).snd =
      l
[PROOFSTEP]
simp only [eq_mp_eq_cast, cast_eq, eq_self_iff_true, heq_iff_eq, and_self_iff, nil_append]
[GOAL]
case h.mk.equal.hc
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l✝ : List ((n : ℕ) × BoundedFormula L α n)
n n✝ : ℕ
t₁✝ t₂✝ : Term L (α ⊕ Fin n✝)
l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)
⊢ { fst := n✝, snd := equal t₁✝ t₂✝ }.fst = { fst := n✝, snd := equal t₁✝ t₂✝ }.fst
[PROOFSTEP]
simp only [eq_self_iff_true, heq_iff_eq, and_self_iff]
[GOAL]
case h.mk.rel
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l✝ : List ((n : ℕ) × BoundedFormula L α n)
n φ_n φ_l : ℕ
φ_R : Relations L φ_l
ts : Fin φ_l → Term L (α ⊕ Fin φ_n)
l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)
⊢ (listDecode (listEncode { fst := φ_n, snd := rel φ_R ts }.snd ++ l)).fst = { fst := φ_n, snd := rel φ_R ts } ∧
    ↑(listDecode (listEncode { fst := φ_n, snd := rel φ_R ts }.snd ++ l)).snd = l
[PROOFSTEP]
rw [listEncode, cons_append, cons_append, singleton_append, cons_append, listDecode]
[GOAL]
case h.mk.rel
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l✝ : List ((n : ℕ) × BoundedFormula L α n)
n φ_n φ_l : ℕ
φ_R : Relations L φ_l
ts : Fin φ_l → Term L (α ⊕ Fin φ_n)
l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)
⊢ (if h :
              ∀ (i : Fin φ_l),
                Option.isSome
                    (Option.join
                      (get?
                        (List.map Sum.getLeft?
                          (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                              (finRange φ_l) ++
                            l))
                        ↑i)) =
                  true then
            if h' :
                ∀ (i : Fin φ_l),
                  (Option.get
                        (Option.join
                          (get?
                            (List.map Sum.getLeft?
                              (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                                  (finRange φ_l) ++
                                l))
                            ↑i))
                        (_ :
                          Option.isSome
                              (Option.join
                                (get?
                                  (List.map Sum.getLeft?
                                    (List.map
                                        (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                                        (finRange φ_l) ++
                                      l))
                                  ↑i)) =
                            true)).fst =
                    { fst := φ_n, snd := rel φ_R ts }.fst then
              { fst := { fst := φ_n, snd := rel φ_R ts }.fst,
                snd :=
                  rel φ_R fun i =>
                    Eq.mp
                      (_ :
                        Term L
                            (α ⊕
                              Fin
                                (Option.get
                                    (Option.join
                                      (get?
                                        (List.map Sum.getLeft?
                                          (List.map
                                              (fun i =>
                                                Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                                              (finRange φ_l) ++
                                            l))
                                        ↑i))
                                    (_ :
                                      Option.isSome
                                          (Option.join
                                            (get?
                                              (List.map Sum.getLeft?
                                                (List.map
                                                    (fun i =>
                                                      Sum.inl
                                                        { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                                                    (finRange φ_l) ++
                                                  l))
                                              ↑i)) =
                                        true)).fst) =
                          Term L (α ⊕ Fin { fst := φ_n, snd := rel φ_R ts }.fst))
                      (Option.get
                          (Option.join
                            (get?
                              (List.map Sum.getLeft?
                                (List.map
                                    (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                                    (finRange φ_l) ++
                                  l))
                              ↑i))
                          (_ :
                            Option.isSome
                                (Option.join
                                  (get?
                                    (List.map Sum.getLeft?
                                      (List.map
                                          (fun i =>
                                            Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                                          (finRange φ_l) ++
                                        l))
                                    ↑i)) =
                              true)).snd }
            else default
          else default,
          {
            val :=
              drop φ_l
                (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                    (finRange φ_l) ++
                  l),
            property :=
              (_ :
                sizeOf
                    (drop φ_l
                      (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                          (finRange φ_l) ++
                        l)) ≤
                  max 1
                    (sizeOf
                      (Sum.inr (Sum.inl { fst := φ_l, snd := φ_R }) ::
                        Sum.inr (Sum.inr { fst := φ_n, snd := rel φ_R ts }.fst) ::
                          (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                              (finRange φ_l) ++
                            l)))) }).fst =
      { fst := φ_n, snd := rel φ_R ts } ∧
    ↑(if h :
                ∀ (i : Fin φ_l),
                  Option.isSome
                      (Option.join
                        (get?
                          (List.map Sum.getLeft?
                            (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                                (finRange φ_l) ++
                              l))
                          ↑i)) =
                    true then
              if h' :
                  ∀ (i : Fin φ_l),
                    (Option.get
                          (Option.join
                            (get?
                              (List.map Sum.getLeft?
                                (List.map
                                    (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                                    (finRange φ_l) ++
                                  l))
                              ↑i))
                          (_ :
                            Option.isSome
                                (Option.join
                                  (get?
                                    (List.map Sum.getLeft?
                                      (List.map
                                          (fun i =>
                                            Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                                          (finRange φ_l) ++
                                        l))
                                    ↑i)) =
                              true)).fst =
                      { fst := φ_n, snd := rel φ_R ts }.fst then
                { fst := { fst := φ_n, snd := rel φ_R ts }.fst,
                  snd :=
                    rel φ_R fun i =>
                      Eq.mp
                        (_ :
                          Term L
                              (α ⊕
                                Fin
                                  (Option.get
                                      (Option.join
                                        (get?
                                          (List.map Sum.getLeft?
                                            (List.map
                                                (fun i =>
                                                  Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                                                (finRange φ_l) ++
                                              l))
                                          ↑i))
                                      (_ :
                                        Option.isSome
                                            (Option.join
                                              (get?
                                                (List.map Sum.getLeft?
                                                  (List.map
                                                      (fun i =>
                                                        Sum.inl
                                                          { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                                                      (finRange φ_l) ++
                                                    l))
                                                ↑i)) =
                                          true)).fst) =
                            Term L (α ⊕ Fin { fst := φ_n, snd := rel φ_R ts }.fst))
                        (Option.get
                            (Option.join
                              (get?
                                (List.map Sum.getLeft?
                                  (List.map
                                      (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                                      (finRange φ_l) ++
                                    l))
                                ↑i))
                            (_ :
                              Option.isSome
                                  (Option.join
                                    (get?
                                      (List.map Sum.getLeft?
                                        (List.map
                                            (fun i =>
                                              Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                                            (finRange φ_l) ++
                                          l))
                                      ↑i)) =
                                true)).snd }
              else default
            else default,
            {
              val :=
                drop φ_l
                  (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                      (finRange φ_l) ++
                    l),
              property :=
                (_ :
                  sizeOf
                      (drop φ_l
                        (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                            (finRange φ_l) ++
                          l)) ≤
                    max 1
                      (sizeOf
                        (Sum.inr (Sum.inl { fst := φ_l, snd := φ_R }) ::
                          Sum.inr (Sum.inr { fst := φ_n, snd := rel φ_R ts }.fst) ::
                            (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                                (finRange φ_l) ++
                              l)))) }).snd =
      l
[PROOFSTEP]
have h :
  ∀ i : Fin φ_l,
    ((List.map Sum.getLeft?
              (List.map
                  (fun i : Fin φ_l =>
                    Sum.inl (⟨(⟨φ_n, rel φ_R ts⟩ : Σ n, L.BoundedFormula α n).fst, ts i⟩ : Σ n, L.Term (Sum α (Fin n))))
                  (finRange φ_l) ++
                l)).get?
          ↑i).join =
      some ⟨_, ts i⟩ :=
  by
  intro i
  simp only [Option.join, map_append, map_map, Option.bind_eq_some, id.def, exists_eq_right, get?_eq_some,
    length_append, length_map, length_finRange]
  refine' ⟨lt_of_lt_of_le i.2 le_self_add, _⟩
  rw [get_append, get_map]
  · simp only [Sum.getLeft?, get_finRange, Fin.eta, Function.comp_apply, eq_self_iff_true, heq_iff_eq, and_self_iff]
  · simp only [length_map, length_finRange, is_lt]
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l✝ : List ((n : ℕ) × BoundedFormula L α n)
n φ_n φ_l : ℕ
φ_R : Relations L φ_l
ts : Fin φ_l → Term L (α ⊕ Fin φ_n)
l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)
⊢ ∀ (i : Fin φ_l),
    Option.join
        (get?
          (List.map Sum.getLeft?
            (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i }) (finRange φ_l) ++
              l))
          ↑i) =
      some { fst := φ_n, snd := ts i }
[PROOFSTEP]
intro i
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l✝ : List ((n : ℕ) × BoundedFormula L α n)
n φ_n φ_l : ℕ
φ_R : Relations L φ_l
ts : Fin φ_l → Term L (α ⊕ Fin φ_n)
l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)
i : Fin φ_l
⊢ Option.join
      (get?
        (List.map Sum.getLeft?
          (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i }) (finRange φ_l) ++
            l))
        ↑i) =
    some { fst := φ_n, snd := ts i }
[PROOFSTEP]
simp only [Option.join, map_append, map_map, Option.bind_eq_some, id.def, exists_eq_right, get?_eq_some, length_append,
  length_map, length_finRange]
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l✝ : List ((n : ℕ) × BoundedFormula L α n)
n φ_n φ_l : ℕ
φ_R : Relations L φ_l
ts : Fin φ_l → Term L (α ⊕ Fin φ_n)
l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)
i : Fin φ_l
⊢ ∃ h,
    List.get
        (List.map (Sum.getLeft? ∘ fun i => Sum.inl { fst := φ_n, snd := ts i }) (finRange φ_l) ++
          List.map Sum.getLeft? l)
        { val := ↑i,
          isLt :=
            (_ :
              ↑i <
                length
                  (List.map (Sum.getLeft? ∘ fun i => Sum.inl { fst := φ_n, snd := ts i }) (finRange φ_l) ++
                    List.map Sum.getLeft? l)) } =
      some { fst := φ_n, snd := ts i }
[PROOFSTEP]
refine' ⟨lt_of_lt_of_le i.2 le_self_add, _⟩
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l✝ : List ((n : ℕ) × BoundedFormula L α n)
n φ_n φ_l : ℕ
φ_R : Relations L φ_l
ts : Fin φ_l → Term L (α ⊕ Fin φ_n)
l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)
i : Fin φ_l
⊢ List.get
      (List.map (Sum.getLeft? ∘ fun i => Sum.inl { fst := φ_n, snd := ts i }) (finRange φ_l) ++ List.map Sum.getLeft? l)
      { val := ↑i,
        isLt :=
          (_ :
            ↑i <
              length
                (List.map (Sum.getLeft? ∘ fun i => Sum.inl { fst := φ_n, snd := ts i }) (finRange φ_l) ++
                  List.map Sum.getLeft? l)) } =
    some { fst := φ_n, snd := ts i }
[PROOFSTEP]
rw [get_append, get_map]
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l✝ : List ((n : ℕ) × BoundedFormula L α n)
n φ_n φ_l : ℕ
φ_R : Relations L φ_l
ts : Fin φ_l → Term L (α ⊕ Fin φ_n)
l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)
i : Fin φ_l
⊢ (Sum.getLeft? ∘ fun i => Sum.inl { fst := φ_n, snd := ts i })
      (List.get (finRange φ_l)
        { val := ↑{ val := ↑i, isLt := ?h }, isLt := (_ : ↑{ val := ↑i, isLt := ?h } < length (finRange φ_l)) }) =
    some { fst := φ_n, snd := ts i }
[PROOFSTEP]
simp only [Sum.getLeft?, get_finRange, Fin.eta, Function.comp_apply, eq_self_iff_true, heq_iff_eq, and_self_iff]
[GOAL]
case h
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l✝ : List ((n : ℕ) × BoundedFormula L α n)
n φ_n φ_l : ℕ
φ_R : Relations L φ_l
ts : Fin φ_l → Term L (α ⊕ Fin φ_n)
l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)
i : Fin φ_l
⊢ ↑i < length (List.map (Sum.getLeft? ∘ fun i => Sum.inl { fst := φ_n, snd := ts i }) (finRange φ_l))
[PROOFSTEP]
simp only [length_map, length_finRange, is_lt]
[GOAL]
case h.mk.rel
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l✝ : List ((n : ℕ) × BoundedFormula L α n)
n φ_n φ_l : ℕ
φ_R : Relations L φ_l
ts : Fin φ_l → Term L (α ⊕ Fin φ_n)
l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)
h :
  ∀ (i : Fin φ_l),
    Option.join
        (get?
          (List.map Sum.getLeft?
            (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i }) (finRange φ_l) ++
              l))
          ↑i) =
      some { fst := φ_n, snd := ts i }
⊢ (if h :
              ∀ (i : Fin φ_l),
                Option.isSome
                    (Option.join
                      (get?
                        (List.map Sum.getLeft?
                          (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                              (finRange φ_l) ++
                            l))
                        ↑i)) =
                  true then
            if h' :
                ∀ (i : Fin φ_l),
                  (Option.get
                        (Option.join
                          (get?
                            (List.map Sum.getLeft?
                              (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                                  (finRange φ_l) ++
                                l))
                            ↑i))
                        (_ :
                          Option.isSome
                              (Option.join
                                (get?
                                  (List.map Sum.getLeft?
                                    (List.map
                                        (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                                        (finRange φ_l) ++
                                      l))
                                  ↑i)) =
                            true)).fst =
                    { fst := φ_n, snd := rel φ_R ts }.fst then
              { fst := { fst := φ_n, snd := rel φ_R ts }.fst,
                snd :=
                  rel φ_R fun i =>
                    Eq.mp
                      (_ :
                        Term L
                            (α ⊕
                              Fin
                                (Option.get
                                    (Option.join
                                      (get?
                                        (List.map Sum.getLeft?
                                          (List.map
                                              (fun i =>
                                                Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                                              (finRange φ_l) ++
                                            l))
                                        ↑i))
                                    (_ :
                                      Option.isSome
                                          (Option.join
                                            (get?
                                              (List.map Sum.getLeft?
                                                (List.map
                                                    (fun i =>
                                                      Sum.inl
                                                        { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                                                    (finRange φ_l) ++
                                                  l))
                                              ↑i)) =
                                        true)).fst) =
                          Term L (α ⊕ Fin { fst := φ_n, snd := rel φ_R ts }.fst))
                      (Option.get
                          (Option.join
                            (get?
                              (List.map Sum.getLeft?
                                (List.map
                                    (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                                    (finRange φ_l) ++
                                  l))
                              ↑i))
                          (_ :
                            Option.isSome
                                (Option.join
                                  (get?
                                    (List.map Sum.getLeft?
                                      (List.map
                                          (fun i =>
                                            Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                                          (finRange φ_l) ++
                                        l))
                                    ↑i)) =
                              true)).snd }
            else default
          else default,
          {
            val :=
              drop φ_l
                (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                    (finRange φ_l) ++
                  l),
            property :=
              (_ :
                sizeOf
                    (drop φ_l
                      (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                          (finRange φ_l) ++
                        l)) ≤
                  max 1
                    (sizeOf
                      (Sum.inr (Sum.inl { fst := φ_l, snd := φ_R }) ::
                        Sum.inr (Sum.inr { fst := φ_n, snd := rel φ_R ts }.fst) ::
                          (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                              (finRange φ_l) ++
                            l)))) }).fst =
      { fst := φ_n, snd := rel φ_R ts } ∧
    ↑(if h :
                ∀ (i : Fin φ_l),
                  Option.isSome
                      (Option.join
                        (get?
                          (List.map Sum.getLeft?
                            (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                                (finRange φ_l) ++
                              l))
                          ↑i)) =
                    true then
              if h' :
                  ∀ (i : Fin φ_l),
                    (Option.get
                          (Option.join
                            (get?
                              (List.map Sum.getLeft?
                                (List.map
                                    (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                                    (finRange φ_l) ++
                                  l))
                              ↑i))
                          (_ :
                            Option.isSome
                                (Option.join
                                  (get?
                                    (List.map Sum.getLeft?
                                      (List.map
                                          (fun i =>
                                            Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                                          (finRange φ_l) ++
                                        l))
                                    ↑i)) =
                              true)).fst =
                      { fst := φ_n, snd := rel φ_R ts }.fst then
                { fst := { fst := φ_n, snd := rel φ_R ts }.fst,
                  snd :=
                    rel φ_R fun i =>
                      Eq.mp
                        (_ :
                          Term L
                              (α ⊕
                                Fin
                                  (Option.get
                                      (Option.join
                                        (get?
                                          (List.map Sum.getLeft?
                                            (List.map
                                                (fun i =>
                                                  Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                                                (finRange φ_l) ++
                                              l))
                                          ↑i))
                                      (_ :
                                        Option.isSome
                                            (Option.join
                                              (get?
                                                (List.map Sum.getLeft?
                                                  (List.map
                                                      (fun i =>
                                                        Sum.inl
                                                          { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                                                      (finRange φ_l) ++
                                                    l))
                                                ↑i)) =
                                          true)).fst) =
                            Term L (α ⊕ Fin { fst := φ_n, snd := rel φ_R ts }.fst))
                        (Option.get
                            (Option.join
                              (get?
                                (List.map Sum.getLeft?
                                  (List.map
                                      (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                                      (finRange φ_l) ++
                                    l))
                                ↑i))
                            (_ :
                              Option.isSome
                                  (Option.join
                                    (get?
                                      (List.map Sum.getLeft?
                                        (List.map
                                            (fun i =>
                                              Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                                            (finRange φ_l) ++
                                          l))
                                      ↑i)) =
                                true)).snd }
              else default
            else default,
            {
              val :=
                drop φ_l
                  (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                      (finRange φ_l) ++
                    l),
              property :=
                (_ :
                  sizeOf
                      (drop φ_l
                        (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                            (finRange φ_l) ++
                          l)) ≤
                    max 1
                      (sizeOf
                        (Sum.inr (Sum.inl { fst := φ_l, snd := φ_R }) ::
                          Sum.inr (Sum.inr { fst := φ_n, snd := rel φ_R ts }.fst) ::
                            (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                                (finRange φ_l) ++
                              l)))) }).snd =
      l
[PROOFSTEP]
rw [dif_pos]
[GOAL]
case h.mk.rel
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l✝ : List ((n : ℕ) × BoundedFormula L α n)
n φ_n φ_l : ℕ
φ_R : Relations L φ_l
ts : Fin φ_l → Term L (α ⊕ Fin φ_n)
l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)
h :
  ∀ (i : Fin φ_l),
    Option.join
        (get?
          (List.map Sum.getLeft?
            (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i }) (finRange φ_l) ++
              l))
          ↑i) =
      some { fst := φ_n, snd := ts i }
⊢ (if h' :
              ∀ (i : Fin φ_l),
                (Option.get
                      (Option.join
                        (get?
                          (List.map Sum.getLeft?
                            (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                                (finRange φ_l) ++
                              l))
                          ↑i))
                      (_ :
                        Option.isSome
                            (Option.join
                              (get?
                                (List.map Sum.getLeft?
                                  (List.map
                                      (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                                      (finRange φ_l) ++
                                    l))
                                ↑i)) =
                          true)).fst =
                  { fst := φ_n, snd := rel φ_R ts }.fst then
            { fst := { fst := φ_n, snd := rel φ_R ts }.fst,
              snd :=
                rel φ_R fun i =>
                  Eq.mp
                    (_ :
                      Term L
                          (α ⊕
                            Fin
                              (Option.get
                                  (Option.join
                                    (get?
                                      (List.map Sum.getLeft?
                                        (List.map
                                            (fun i =>
                                              Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                                            (finRange φ_l) ++
                                          l))
                                      ↑i))
                                  (_ :
                                    Option.isSome
                                        (Option.join
                                          (get?
                                            (List.map Sum.getLeft?
                                              (List.map
                                                  (fun i =>
                                                    Sum.inl
                                                      { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                                                  (finRange φ_l) ++
                                                l))
                                            ↑i)) =
                                      true)).fst) =
                        Term L (α ⊕ Fin { fst := φ_n, snd := rel φ_R ts }.fst))
                    (Option.get
                        (Option.join
                          (get?
                            (List.map Sum.getLeft?
                              (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                                  (finRange φ_l) ++
                                l))
                            ↑i))
                        (_ :
                          Option.isSome
                              (Option.join
                                (get?
                                  (List.map Sum.getLeft?
                                    (List.map
                                        (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                                        (finRange φ_l) ++
                                      l))
                                  ↑i)) =
                            true)).snd }
          else default,
          {
            val :=
              drop φ_l
                (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                    (finRange φ_l) ++
                  l),
            property :=
              (_ :
                sizeOf
                    (drop φ_l
                      (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                          (finRange φ_l) ++
                        l)) ≤
                  max 1
                    (sizeOf
                      (Sum.inr (Sum.inl { fst := φ_l, snd := φ_R }) ::
                        Sum.inr (Sum.inr { fst := φ_n, snd := rel φ_R ts }.fst) ::
                          (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                              (finRange φ_l) ++
                            l)))) }).fst =
      { fst := φ_n, snd := rel φ_R ts } ∧
    ↑(if h' :
                ∀ (i : Fin φ_l),
                  (Option.get
                        (Option.join
                          (get?
                            (List.map Sum.getLeft?
                              (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                                  (finRange φ_l) ++
                                l))
                            ↑i))
                        (_ :
                          Option.isSome
                              (Option.join
                                (get?
                                  (List.map Sum.getLeft?
                                    (List.map
                                        (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                                        (finRange φ_l) ++
                                      l))
                                  ↑i)) =
                            true)).fst =
                    { fst := φ_n, snd := rel φ_R ts }.fst then
              { fst := { fst := φ_n, snd := rel φ_R ts }.fst,
                snd :=
                  rel φ_R fun i =>
                    Eq.mp
                      (_ :
                        Term L
                            (α ⊕
                              Fin
                                (Option.get
                                    (Option.join
                                      (get?
                                        (List.map Sum.getLeft?
                                          (List.map
                                              (fun i =>
                                                Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                                              (finRange φ_l) ++
                                            l))
                                        ↑i))
                                    (_ :
                                      Option.isSome
                                          (Option.join
                                            (get?
                                              (List.map Sum.getLeft?
                                                (List.map
                                                    (fun i =>
                                                      Sum.inl
                                                        { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                                                    (finRange φ_l) ++
                                                  l))
                                              ↑i)) =
                                        true)).fst) =
                          Term L (α ⊕ Fin { fst := φ_n, snd := rel φ_R ts }.fst))
                      (Option.get
                          (Option.join
                            (get?
                              (List.map Sum.getLeft?
                                (List.map
                                    (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                                    (finRange φ_l) ++
                                  l))
                              ↑i))
                          (_ :
                            Option.isSome
                                (Option.join
                                  (get?
                                    (List.map Sum.getLeft?
                                      (List.map
                                          (fun i =>
                                            Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                                          (finRange φ_l) ++
                                        l))
                                    ↑i)) =
                              true)).snd }
            else default,
            {
              val :=
                drop φ_l
                  (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                      (finRange φ_l) ++
                    l),
              property :=
                (_ :
                  sizeOf
                      (drop φ_l
                        (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                            (finRange φ_l) ++
                          l)) ≤
                    max 1
                      (sizeOf
                        (Sum.inr (Sum.inl { fst := φ_l, snd := φ_R }) ::
                          Sum.inr (Sum.inr { fst := φ_n, snd := rel φ_R ts }.fst) ::
                            (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                                (finRange φ_l) ++
                              l)))) }).snd =
      l
case h.mk.rel.hc
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l✝ : List ((n : ℕ) × BoundedFormula L α n)
n φ_n φ_l : ℕ
φ_R : Relations L φ_l
ts : Fin φ_l → Term L (α ⊕ Fin φ_n)
l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)
h :
  ∀ (i : Fin φ_l),
    Option.join
        (get?
          (List.map Sum.getLeft?
            (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i }) (finRange φ_l) ++
              l))
          ↑i) =
      some { fst := φ_n, snd := ts i }
⊢ ∀ (i : Fin φ_l),
    Option.isSome
        (Option.join
          (get?
            (List.map Sum.getLeft?
              (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                  (finRange φ_l) ++
                l))
            ↑i)) =
      true
[PROOFSTEP]
swap
[GOAL]
case h.mk.rel.hc
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l✝ : List ((n : ℕ) × BoundedFormula L α n)
n φ_n φ_l : ℕ
φ_R : Relations L φ_l
ts : Fin φ_l → Term L (α ⊕ Fin φ_n)
l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)
h :
  ∀ (i : Fin φ_l),
    Option.join
        (get?
          (List.map Sum.getLeft?
            (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i }) (finRange φ_l) ++
              l))
          ↑i) =
      some { fst := φ_n, snd := ts i }
⊢ ∀ (i : Fin φ_l),
    Option.isSome
        (Option.join
          (get?
            (List.map Sum.getLeft?
              (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                  (finRange φ_l) ++
                l))
            ↑i)) =
      true
[PROOFSTEP]
exact fun i => Option.isSome_iff_exists.2 ⟨⟨_, ts i⟩, h i⟩
[GOAL]
case h.mk.rel
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l✝ : List ((n : ℕ) × BoundedFormula L α n)
n φ_n φ_l : ℕ
φ_R : Relations L φ_l
ts : Fin φ_l → Term L (α ⊕ Fin φ_n)
l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)
h :
  ∀ (i : Fin φ_l),
    Option.join
        (get?
          (List.map Sum.getLeft?
            (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i }) (finRange φ_l) ++
              l))
          ↑i) =
      some { fst := φ_n, snd := ts i }
⊢ (if h' :
              ∀ (i : Fin φ_l),
                (Option.get
                      (Option.join
                        (get?
                          (List.map Sum.getLeft?
                            (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                                (finRange φ_l) ++
                              l))
                          ↑i))
                      (_ :
                        Option.isSome
                            (Option.join
                              (get?
                                (List.map Sum.getLeft?
                                  (List.map
                                      (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                                      (finRange φ_l) ++
                                    l))
                                ↑i)) =
                          true)).fst =
                  { fst := φ_n, snd := rel φ_R ts }.fst then
            { fst := { fst := φ_n, snd := rel φ_R ts }.fst,
              snd :=
                rel φ_R fun i =>
                  Eq.mp
                    (_ :
                      Term L
                          (α ⊕
                            Fin
                              (Option.get
                                  (Option.join
                                    (get?
                                      (List.map Sum.getLeft?
                                        (List.map
                                            (fun i =>
                                              Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                                            (finRange φ_l) ++
                                          l))
                                      ↑i))
                                  (_ :
                                    Option.isSome
                                        (Option.join
                                          (get?
                                            (List.map Sum.getLeft?
                                              (List.map
                                                  (fun i =>
                                                    Sum.inl
                                                      { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                                                  (finRange φ_l) ++
                                                l))
                                            ↑i)) =
                                      true)).fst) =
                        Term L (α ⊕ Fin { fst := φ_n, snd := rel φ_R ts }.fst))
                    (Option.get
                        (Option.join
                          (get?
                            (List.map Sum.getLeft?
                              (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                                  (finRange φ_l) ++
                                l))
                            ↑i))
                        (_ :
                          Option.isSome
                              (Option.join
                                (get?
                                  (List.map Sum.getLeft?
                                    (List.map
                                        (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                                        (finRange φ_l) ++
                                      l))
                                  ↑i)) =
                            true)).snd }
          else default,
          {
            val :=
              drop φ_l
                (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                    (finRange φ_l) ++
                  l),
            property :=
              (_ :
                sizeOf
                    (drop φ_l
                      (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                          (finRange φ_l) ++
                        l)) ≤
                  max 1
                    (sizeOf
                      (Sum.inr (Sum.inl { fst := φ_l, snd := φ_R }) ::
                        Sum.inr (Sum.inr { fst := φ_n, snd := rel φ_R ts }.fst) ::
                          (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                              (finRange φ_l) ++
                            l)))) }).fst =
      { fst := φ_n, snd := rel φ_R ts } ∧
    ↑(if h' :
                ∀ (i : Fin φ_l),
                  (Option.get
                        (Option.join
                          (get?
                            (List.map Sum.getLeft?
                              (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                                  (finRange φ_l) ++
                                l))
                            ↑i))
                        (_ :
                          Option.isSome
                              (Option.join
                                (get?
                                  (List.map Sum.getLeft?
                                    (List.map
                                        (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                                        (finRange φ_l) ++
                                      l))
                                  ↑i)) =
                            true)).fst =
                    { fst := φ_n, snd := rel φ_R ts }.fst then
              { fst := { fst := φ_n, snd := rel φ_R ts }.fst,
                snd :=
                  rel φ_R fun i =>
                    Eq.mp
                      (_ :
                        Term L
                            (α ⊕
                              Fin
                                (Option.get
                                    (Option.join
                                      (get?
                                        (List.map Sum.getLeft?
                                          (List.map
                                              (fun i =>
                                                Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                                              (finRange φ_l) ++
                                            l))
                                        ↑i))
                                    (_ :
                                      Option.isSome
                                          (Option.join
                                            (get?
                                              (List.map Sum.getLeft?
                                                (List.map
                                                    (fun i =>
                                                      Sum.inl
                                                        { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                                                    (finRange φ_l) ++
                                                  l))
                                              ↑i)) =
                                        true)).fst) =
                          Term L (α ⊕ Fin { fst := φ_n, snd := rel φ_R ts }.fst))
                      (Option.get
                          (Option.join
                            (get?
                              (List.map Sum.getLeft?
                                (List.map
                                    (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                                    (finRange φ_l) ++
                                  l))
                              ↑i))
                          (_ :
                            Option.isSome
                                (Option.join
                                  (get?
                                    (List.map Sum.getLeft?
                                      (List.map
                                          (fun i =>
                                            Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                                          (finRange φ_l) ++
                                        l))
                                    ↑i)) =
                              true)).snd }
            else default,
            {
              val :=
                drop φ_l
                  (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                      (finRange φ_l) ++
                    l),
              property :=
                (_ :
                  sizeOf
                      (drop φ_l
                        (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                            (finRange φ_l) ++
                          l)) ≤
                    max 1
                      (sizeOf
                        (Sum.inr (Sum.inl { fst := φ_l, snd := φ_R }) ::
                          Sum.inr (Sum.inr { fst := φ_n, snd := rel φ_R ts }.fst) ::
                            (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                                (finRange φ_l) ++
                              l)))) }).snd =
      l
[PROOFSTEP]
rw [dif_pos]
[GOAL]
case h.mk.rel
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l✝ : List ((n : ℕ) × BoundedFormula L α n)
n φ_n φ_l : ℕ
φ_R : Relations L φ_l
ts : Fin φ_l → Term L (α ⊕ Fin φ_n)
l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)
h :
  ∀ (i : Fin φ_l),
    Option.join
        (get?
          (List.map Sum.getLeft?
            (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i }) (finRange φ_l) ++
              l))
          ↑i) =
      some { fst := φ_n, snd := ts i }
⊢ ({ fst := { fst := φ_n, snd := rel φ_R ts }.fst,
            snd :=
              rel φ_R fun i =>
                Eq.mp
                  (_ :
                    Term L
                        (α ⊕
                          Fin
                            (Option.get
                                (Option.join
                                  (get?
                                    (List.map Sum.getLeft?
                                      (List.map
                                          (fun i =>
                                            Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                                          (finRange φ_l) ++
                                        l))
                                    ↑i))
                                (_ :
                                  Option.isSome
                                      (Option.join
                                        (get?
                                          (List.map Sum.getLeft?
                                            (List.map
                                                (fun i =>
                                                  Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                                                (finRange φ_l) ++
                                              l))
                                          ↑i)) =
                                    true)).fst) =
                      Term L (α ⊕ Fin { fst := φ_n, snd := rel φ_R ts }.fst))
                  (Option.get
                      (Option.join
                        (get?
                          (List.map Sum.getLeft?
                            (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                                (finRange φ_l) ++
                              l))
                          ↑i))
                      (_ :
                        Option.isSome
                            (Option.join
                              (get?
                                (List.map Sum.getLeft?
                                  (List.map
                                      (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                                      (finRange φ_l) ++
                                    l))
                                ↑i)) =
                          true)).snd },
          {
            val :=
              drop φ_l
                (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                    (finRange φ_l) ++
                  l),
            property :=
              (_ :
                sizeOf
                    (drop φ_l
                      (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                          (finRange φ_l) ++
                        l)) ≤
                  max 1
                    (sizeOf
                      (Sum.inr (Sum.inl { fst := φ_l, snd := φ_R }) ::
                        Sum.inr (Sum.inr { fst := φ_n, snd := rel φ_R ts }.fst) ::
                          (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                              (finRange φ_l) ++
                            l)))) }).fst =
      { fst := φ_n, snd := rel φ_R ts } ∧
    ↑({ fst := { fst := φ_n, snd := rel φ_R ts }.fst,
              snd :=
                rel φ_R fun i =>
                  Eq.mp
                    (_ :
                      Term L
                          (α ⊕
                            Fin
                              (Option.get
                                  (Option.join
                                    (get?
                                      (List.map Sum.getLeft?
                                        (List.map
                                            (fun i =>
                                              Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                                            (finRange φ_l) ++
                                          l))
                                      ↑i))
                                  (_ :
                                    Option.isSome
                                        (Option.join
                                          (get?
                                            (List.map Sum.getLeft?
                                              (List.map
                                                  (fun i =>
                                                    Sum.inl
                                                      { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                                                  (finRange φ_l) ++
                                                l))
                                            ↑i)) =
                                      true)).fst) =
                        Term L (α ⊕ Fin { fst := φ_n, snd := rel φ_R ts }.fst))
                    (Option.get
                        (Option.join
                          (get?
                            (List.map Sum.getLeft?
                              (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                                  (finRange φ_l) ++
                                l))
                            ↑i))
                        (_ :
                          Option.isSome
                              (Option.join
                                (get?
                                  (List.map Sum.getLeft?
                                    (List.map
                                        (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                                        (finRange φ_l) ++
                                      l))
                                  ↑i)) =
                            true)).snd },
            {
              val :=
                drop φ_l
                  (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                      (finRange φ_l) ++
                    l),
              property :=
                (_ :
                  sizeOf
                      (drop φ_l
                        (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                            (finRange φ_l) ++
                          l)) ≤
                    max 1
                      (sizeOf
                        (Sum.inr (Sum.inl { fst := φ_l, snd := φ_R }) ::
                          Sum.inr (Sum.inr { fst := φ_n, snd := rel φ_R ts }.fst) ::
                            (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                                (finRange φ_l) ++
                              l)))) }).snd =
      l
case h.mk.rel.hc
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l✝ : List ((n : ℕ) × BoundedFormula L α n)
n φ_n φ_l : ℕ
φ_R : Relations L φ_l
ts : Fin φ_l → Term L (α ⊕ Fin φ_n)
l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)
h :
  ∀ (i : Fin φ_l),
    Option.join
        (get?
          (List.map Sum.getLeft?
            (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i }) (finRange φ_l) ++
              l))
          ↑i) =
      some { fst := φ_n, snd := ts i }
⊢ ∀ (i : Fin φ_l),
    (Option.get
          (Option.join
            (get?
              (List.map Sum.getLeft?
                (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                    (finRange φ_l) ++
                  l))
              ↑i))
          (_ :
            Option.isSome
                (Option.join
                  (get?
                    (List.map Sum.getLeft?
                      (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                          (finRange φ_l) ++
                        l))
                    ↑i)) =
              true)).fst =
      { fst := φ_n, snd := rel φ_R ts }.fst
[PROOFSTEP]
swap
[GOAL]
case h.mk.rel.hc
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l✝ : List ((n : ℕ) × BoundedFormula L α n)
n φ_n φ_l : ℕ
φ_R : Relations L φ_l
ts : Fin φ_l → Term L (α ⊕ Fin φ_n)
l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)
h :
  ∀ (i : Fin φ_l),
    Option.join
        (get?
          (List.map Sum.getLeft?
            (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i }) (finRange φ_l) ++
              l))
          ↑i) =
      some { fst := φ_n, snd := ts i }
⊢ ∀ (i : Fin φ_l),
    (Option.get
          (Option.join
            (get?
              (List.map Sum.getLeft?
                (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                    (finRange φ_l) ++
                  l))
              ↑i))
          (_ :
            Option.isSome
                (Option.join
                  (get?
                    (List.map Sum.getLeft?
                      (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                          (finRange φ_l) ++
                        l))
                    ↑i)) =
              true)).fst =
      { fst := φ_n, snd := rel φ_R ts }.fst
[PROOFSTEP]
intro i
[GOAL]
case h.mk.rel.hc
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l✝ : List ((n : ℕ) × BoundedFormula L α n)
n φ_n φ_l : ℕ
φ_R : Relations L φ_l
ts : Fin φ_l → Term L (α ⊕ Fin φ_n)
l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)
h :
  ∀ (i : Fin φ_l),
    Option.join
        (get?
          (List.map Sum.getLeft?
            (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i }) (finRange φ_l) ++
              l))
          ↑i) =
      some { fst := φ_n, snd := ts i }
i : Fin φ_l
⊢ (Option.get
        (Option.join
          (get?
            (List.map Sum.getLeft?
              (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                  (finRange φ_l) ++
                l))
            ↑i))
        (_ :
          Option.isSome
              (Option.join
                (get?
                  (List.map Sum.getLeft?
                    (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                        (finRange φ_l) ++
                      l))
                  ↑i)) =
            true)).fst =
    { fst := φ_n, snd := rel φ_R ts }.fst
[PROOFSTEP]
obtain ⟨h1, h2⟩ := Option.eq_some_iff_get_eq.1 (h i)
[GOAL]
case h.mk.rel.hc.intro
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l✝ : List ((n : ℕ) × BoundedFormula L α n)
n φ_n φ_l : ℕ
φ_R : Relations L φ_l
ts : Fin φ_l → Term L (α ⊕ Fin φ_n)
l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)
h :
  ∀ (i : Fin φ_l),
    Option.join
        (get?
          (List.map Sum.getLeft?
            (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i }) (finRange φ_l) ++
              l))
          ↑i) =
      some { fst := φ_n, snd := ts i }
i : Fin φ_l
h1 :
  Option.isSome
      (Option.join
        (get?
          (List.map Sum.getLeft?
            (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i }) (finRange φ_l) ++
              l))
          ↑i)) =
    true
h2 :
  Option.get
      (Option.join
        (get?
          (List.map Sum.getLeft?
            (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i }) (finRange φ_l) ++
              l))
          ↑i))
      h1 =
    { fst := φ_n, snd := ts i }
⊢ (Option.get
        (Option.join
          (get?
            (List.map Sum.getLeft?
              (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                  (finRange φ_l) ++
                l))
            ↑i))
        (_ :
          Option.isSome
              (Option.join
                (get?
                  (List.map Sum.getLeft?
                    (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                        (finRange φ_l) ++
                      l))
                  ↑i)) =
            true)).fst =
    { fst := φ_n, snd := rel φ_R ts }.fst
[PROOFSTEP]
rw [h2]
[GOAL]
case h.mk.rel
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l✝ : List ((n : ℕ) × BoundedFormula L α n)
n φ_n φ_l : ℕ
φ_R : Relations L φ_l
ts : Fin φ_l → Term L (α ⊕ Fin φ_n)
l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)
h :
  ∀ (i : Fin φ_l),
    Option.join
        (get?
          (List.map Sum.getLeft?
            (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i }) (finRange φ_l) ++
              l))
          ↑i) =
      some { fst := φ_n, snd := ts i }
⊢ ({ fst := { fst := φ_n, snd := rel φ_R ts }.fst,
            snd :=
              rel φ_R fun i =>
                Eq.mp
                  (_ :
                    Term L
                        (α ⊕
                          Fin
                            (Option.get
                                (Option.join
                                  (get?
                                    (List.map Sum.getLeft?
                                      (List.map
                                          (fun i =>
                                            Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                                          (finRange φ_l) ++
                                        l))
                                    ↑i))
                                (_ :
                                  Option.isSome
                                      (Option.join
                                        (get?
                                          (List.map Sum.getLeft?
                                            (List.map
                                                (fun i =>
                                                  Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                                                (finRange φ_l) ++
                                              l))
                                          ↑i)) =
                                    true)).fst) =
                      Term L (α ⊕ Fin { fst := φ_n, snd := rel φ_R ts }.fst))
                  (Option.get
                      (Option.join
                        (get?
                          (List.map Sum.getLeft?
                            (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                                (finRange φ_l) ++
                              l))
                          ↑i))
                      (_ :
                        Option.isSome
                            (Option.join
                              (get?
                                (List.map Sum.getLeft?
                                  (List.map
                                      (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                                      (finRange φ_l) ++
                                    l))
                                ↑i)) =
                          true)).snd },
          {
            val :=
              drop φ_l
                (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                    (finRange φ_l) ++
                  l),
            property :=
              (_ :
                sizeOf
                    (drop φ_l
                      (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                          (finRange φ_l) ++
                        l)) ≤
                  max 1
                    (sizeOf
                      (Sum.inr (Sum.inl { fst := φ_l, snd := φ_R }) ::
                        Sum.inr (Sum.inr { fst := φ_n, snd := rel φ_R ts }.fst) ::
                          (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                              (finRange φ_l) ++
                            l)))) }).fst =
      { fst := φ_n, snd := rel φ_R ts } ∧
    ↑({ fst := { fst := φ_n, snd := rel φ_R ts }.fst,
              snd :=
                rel φ_R fun i =>
                  Eq.mp
                    (_ :
                      Term L
                          (α ⊕
                            Fin
                              (Option.get
                                  (Option.join
                                    (get?
                                      (List.map Sum.getLeft?
                                        (List.map
                                            (fun i =>
                                              Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                                            (finRange φ_l) ++
                                          l))
                                      ↑i))
                                  (_ :
                                    Option.isSome
                                        (Option.join
                                          (get?
                                            (List.map Sum.getLeft?
                                              (List.map
                                                  (fun i =>
                                                    Sum.inl
                                                      { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                                                  (finRange φ_l) ++
                                                l))
                                            ↑i)) =
                                      true)).fst) =
                        Term L (α ⊕ Fin { fst := φ_n, snd := rel φ_R ts }.fst))
                    (Option.get
                        (Option.join
                          (get?
                            (List.map Sum.getLeft?
                              (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                                  (finRange φ_l) ++
                                l))
                            ↑i))
                        (_ :
                          Option.isSome
                              (Option.join
                                (get?
                                  (List.map Sum.getLeft?
                                    (List.map
                                        (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                                        (finRange φ_l) ++
                                      l))
                                  ↑i)) =
                            true)).snd },
            {
              val :=
                drop φ_l
                  (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                      (finRange φ_l) ++
                    l),
              property :=
                (_ :
                  sizeOf
                      (drop φ_l
                        (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                            (finRange φ_l) ++
                          l)) ≤
                    max 1
                      (sizeOf
                        (Sum.inr (Sum.inl { fst := φ_l, snd := φ_R }) ::
                          Sum.inr (Sum.inr { fst := φ_n, snd := rel φ_R ts }.fst) ::
                            (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                                (finRange φ_l) ++
                              l)))) }).snd =
      l
[PROOFSTEP]
simp only [Sigma.mk.inj_iff, heq_eq_eq, rel.injEq, true_and]
[GOAL]
case h.mk.rel
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l✝ : List ((n : ℕ) × BoundedFormula L α n)
n φ_n φ_l : ℕ
φ_R : Relations L φ_l
ts : Fin φ_l → Term L (α ⊕ Fin φ_n)
l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)
h :
  ∀ (i : Fin φ_l),
    Option.join
        (get?
          (List.map Sum.getLeft?
            (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i }) (finRange φ_l) ++
              l))
          ↑i) =
      some { fst := φ_n, snd := ts i }
⊢ (fun i =>
        Eq.mp
          (_ :
            Term L
                (α ⊕
                  Fin
                    (Option.get
                        (Option.join
                          (get?
                            (List.map Sum.getLeft?
                              (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                                  (finRange φ_l) ++
                                l))
                            ↑i))
                        (_ :
                          Option.isSome
                              (Option.join
                                (get?
                                  (List.map Sum.getLeft?
                                    (List.map
                                        (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                                        (finRange φ_l) ++
                                      l))
                                  ↑i)) =
                            true)).fst) =
              Term L (α ⊕ Fin { fst := φ_n, snd := rel φ_R ts }.fst))
          (Option.get
              (Option.join
                (get?
                  (List.map Sum.getLeft? (List.map (fun i => Sum.inl { fst := φ_n, snd := ts i }) (finRange φ_l) ++ l))
                  ↑i))
              (_ :
                Option.isSome
                    (Option.join
                      (get?
                        (List.map Sum.getLeft?
                          (List.map (fun i => Sum.inl { fst := φ_n, snd := ts i }) (finRange φ_l) ++ l))
                        ↑i)) =
                  true)).snd) =
      ts ∧
    drop φ_l (List.map (fun i => Sum.inl { fst := φ_n, snd := ts i }) (finRange φ_l) ++ l) = l
[PROOFSTEP]
refine' ⟨funext fun i => _, _⟩
[GOAL]
case h.mk.rel.refine'_1
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l✝ : List ((n : ℕ) × BoundedFormula L α n)
n φ_n φ_l : ℕ
φ_R : Relations L φ_l
ts : Fin φ_l → Term L (α ⊕ Fin φ_n)
l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)
h :
  ∀ (i : Fin φ_l),
    Option.join
        (get?
          (List.map Sum.getLeft?
            (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i }) (finRange φ_l) ++
              l))
          ↑i) =
      some { fst := φ_n, snd := ts i }
i : Fin φ_l
⊢ Eq.mp
      (_ :
        Term L
            (α ⊕
              Fin
                (Option.get
                    (Option.join
                      (get?
                        (List.map Sum.getLeft?
                          (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                              (finRange φ_l) ++
                            l))
                        ↑i))
                    (_ :
                      Option.isSome
                          (Option.join
                            (get?
                              (List.map Sum.getLeft?
                                (List.map
                                    (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                                    (finRange φ_l) ++
                                  l))
                              ↑i)) =
                        true)).fst) =
          Term L (α ⊕ Fin { fst := φ_n, snd := rel φ_R ts }.fst))
      (Option.get
          (Option.join
            (get? (List.map Sum.getLeft? (List.map (fun i => Sum.inl { fst := φ_n, snd := ts i }) (finRange φ_l) ++ l))
              ↑i))
          (_ :
            Option.isSome
                (Option.join
                  (get?
                    (List.map Sum.getLeft?
                      (List.map (fun i => Sum.inl { fst := φ_n, snd := ts i }) (finRange φ_l) ++ l))
                    ↑i)) =
              true)).snd =
    ts i
[PROOFSTEP]
obtain ⟨h1, h2⟩ := Option.eq_some_iff_get_eq.1 (h i)
[GOAL]
case h.mk.rel.refine'_1.intro
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l✝ : List ((n : ℕ) × BoundedFormula L α n)
n φ_n φ_l : ℕ
φ_R : Relations L φ_l
ts : Fin φ_l → Term L (α ⊕ Fin φ_n)
l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)
h :
  ∀ (i : Fin φ_l),
    Option.join
        (get?
          (List.map Sum.getLeft?
            (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i }) (finRange φ_l) ++
              l))
          ↑i) =
      some { fst := φ_n, snd := ts i }
i : Fin φ_l
h1 :
  Option.isSome
      (Option.join
        (get?
          (List.map Sum.getLeft?
            (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i }) (finRange φ_l) ++
              l))
          ↑i)) =
    true
h2 :
  Option.get
      (Option.join
        (get?
          (List.map Sum.getLeft?
            (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i }) (finRange φ_l) ++
              l))
          ↑i))
      h1 =
    { fst := φ_n, snd := ts i }
⊢ Eq.mp
      (_ :
        Term L
            (α ⊕
              Fin
                (Option.get
                    (Option.join
                      (get?
                        (List.map Sum.getLeft?
                          (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                              (finRange φ_l) ++
                            l))
                        ↑i))
                    (_ :
                      Option.isSome
                          (Option.join
                            (get?
                              (List.map Sum.getLeft?
                                (List.map
                                    (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i })
                                    (finRange φ_l) ++
                                  l))
                              ↑i)) =
                        true)).fst) =
          Term L (α ⊕ Fin { fst := φ_n, snd := rel φ_R ts }.fst))
      (Option.get
          (Option.join
            (get? (List.map Sum.getLeft? (List.map (fun i => Sum.inl { fst := φ_n, snd := ts i }) (finRange φ_l) ++ l))
              ↑i))
          (_ :
            Option.isSome
                (Option.join
                  (get?
                    (List.map Sum.getLeft?
                      (List.map (fun i => Sum.inl { fst := φ_n, snd := ts i }) (finRange φ_l) ++ l))
                    ↑i)) =
              true)).snd =
    ts i
[PROOFSTEP]
rw [eq_mp_eq_cast, cast_eq_iff_heq]
[GOAL]
case h.mk.rel.refine'_1.intro
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l✝ : List ((n : ℕ) × BoundedFormula L α n)
n φ_n φ_l : ℕ
φ_R : Relations L φ_l
ts : Fin φ_l → Term L (α ⊕ Fin φ_n)
l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)
h :
  ∀ (i : Fin φ_l),
    Option.join
        (get?
          (List.map Sum.getLeft?
            (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i }) (finRange φ_l) ++
              l))
          ↑i) =
      some { fst := φ_n, snd := ts i }
i : Fin φ_l
h1 :
  Option.isSome
      (Option.join
        (get?
          (List.map Sum.getLeft?
            (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i }) (finRange φ_l) ++
              l))
          ↑i)) =
    true
h2 :
  Option.get
      (Option.join
        (get?
          (List.map Sum.getLeft?
            (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i }) (finRange φ_l) ++
              l))
          ↑i))
      h1 =
    { fst := φ_n, snd := ts i }
⊢ HEq
    (Option.get
        (Option.join
          (get? (List.map Sum.getLeft? (List.map (fun i => Sum.inl { fst := φ_n, snd := ts i }) (finRange φ_l) ++ l))
            ↑i))
        (_ :
          Option.isSome
              (Option.join
                (get?
                  (List.map Sum.getLeft? (List.map (fun i => Sum.inl { fst := φ_n, snd := ts i }) (finRange φ_l) ++ l))
                  ↑i)) =
            true)).snd
    (ts i)
[PROOFSTEP]
exact (Sigma.ext_iff.1 ((Sigma.eta (Option.get _ h1)).trans h2)).2
[GOAL]
case h.mk.rel.refine'_2
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l✝ : List ((n : ℕ) × BoundedFormula L α n)
n φ_n φ_l : ℕ
φ_R : Relations L φ_l
ts : Fin φ_l → Term L (α ⊕ Fin φ_n)
l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)
h :
  ∀ (i : Fin φ_l),
    Option.join
        (get?
          (List.map Sum.getLeft?
            (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i }) (finRange φ_l) ++
              l))
          ↑i) =
      some { fst := φ_n, snd := ts i }
⊢ drop φ_l (List.map (fun i => Sum.inl { fst := φ_n, snd := ts i }) (finRange φ_l) ++ l) = l
[PROOFSTEP]
rw [List.drop_append_eq_append_drop, length_map, length_finRange, Nat.sub_self, drop, drop_eq_nil_of_le, nil_append]
[GOAL]
case h.mk.rel.refine'_2
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l✝ : List ((n : ℕ) × BoundedFormula L α n)
n φ_n φ_l : ℕ
φ_R : Relations L φ_l
ts : Fin φ_l → Term L (α ⊕ Fin φ_n)
l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)
h :
  ∀ (i : Fin φ_l),
    Option.join
        (get?
          (List.map Sum.getLeft?
            (List.map (fun i => Sum.inl { fst := { fst := φ_n, snd := rel φ_R ts }.fst, snd := ts i }) (finRange φ_l) ++
              l))
          ↑i) =
      some { fst := φ_n, snd := ts i }
⊢ length (List.map (fun i => Sum.inl { fst := φ_n, snd := ts i }) (finRange φ_l)) ≤ φ_l
[PROOFSTEP]
rw [length_map, length_finRange]
[GOAL]
case h.mk.imp
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l✝ : List ((n : ℕ) × BoundedFormula L α n)
n n✝ : ℕ
f₁✝ f₂✝ : BoundedFormula L α n✝
ih1 :
  ∀ (l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)),
    (listDecode (listEncode { fst := n✝, snd := f₁✝ }.snd ++ l)).fst = { fst := n✝, snd := f₁✝ } ∧
      ↑(listDecode (listEncode { fst := n✝, snd := f₁✝ }.snd ++ l)).snd = l
ih2 :
  ∀ (l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)),
    (listDecode (listEncode { fst := n✝, snd := f₂✝ }.snd ++ l)).fst = { fst := n✝, snd := f₂✝ } ∧
      ↑(listDecode (listEncode { fst := n✝, snd := f₂✝ }.snd ++ l)).snd = l
l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)
⊢ (listDecode (listEncode { fst := n✝, snd := f₁✝ ⟹ f₂✝ }.snd ++ l)).fst = { fst := n✝, snd := f₁✝ ⟹ f₂✝ } ∧
    ↑(listDecode (listEncode { fst := n✝, snd := f₁✝ ⟹ f₂✝ }.snd ++ l)).snd = l
[PROOFSTEP]
rw [listEncode, List.append_assoc, cons_append, listDecode]
[GOAL]
case h.mk.imp
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l✝ : List ((n : ℕ) × BoundedFormula L α n)
n n✝ : ℕ
f₁✝ f₂✝ : BoundedFormula L α n✝
ih1 :
  ∀ (l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)),
    (listDecode (listEncode { fst := n✝, snd := f₁✝ }.snd ++ l)).fst = { fst := n✝, snd := f₁✝ } ∧
      ↑(listDecode (listEncode { fst := n✝, snd := f₁✝ }.snd ++ l)).snd = l
ih2 :
  ∀ (l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)),
    (listDecode (listEncode { fst := n✝, snd := f₂✝ }.snd ++ l)).fst = { fst := n✝, snd := f₂✝ } ∧
      ↑(listDecode (listEncode { fst := n✝, snd := f₂✝ }.snd ++ l)).snd = l
l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)
⊢ ((fun this =>
            (sigmaImp (listDecode (listEncode f₁✝ ++ (listEncode f₂✝ ++ l))).fst
                (listDecode ↑(listDecode (listEncode f₁✝ ++ (listEncode f₂✝ ++ l))).snd).fst,
              { val := ↑(listDecode ↑(listDecode (listEncode f₁✝ ++ (listEncode f₂✝ ++ l))).snd).snd,
                property :=
                  (_ :
                    sizeOf ↑(listDecode ↑(listDecode (listEncode f₁✝ ++ (listEncode f₂✝ ++ l))).snd).snd ≤
                      max 1 (sizeOf (Sum.inr (Sum.inr 0) :: (listEncode f₁✝ ++ (listEncode f₂✝ ++ l))))) }))
          (_ :
            sizeOf ↑(listDecode (listEncode f₁✝ ++ (listEncode f₂✝ ++ l))).snd <
              1 + (1 + 1) + sizeOf (listEncode f₁✝ ++ (listEncode f₂✝ ++ l)))).fst =
      { fst := n✝, snd := f₁✝ ⟹ f₂✝ } ∧
    ↑((fun this =>
              (sigmaImp (listDecode (listEncode f₁✝ ++ (listEncode f₂✝ ++ l))).fst
                  (listDecode ↑(listDecode (listEncode f₁✝ ++ (listEncode f₂✝ ++ l))).snd).fst,
                { val := ↑(listDecode ↑(listDecode (listEncode f₁✝ ++ (listEncode f₂✝ ++ l))).snd).snd,
                  property :=
                    (_ :
                      sizeOf ↑(listDecode ↑(listDecode (listEncode f₁✝ ++ (listEncode f₂✝ ++ l))).snd).snd ≤
                        max 1 (sizeOf (Sum.inr (Sum.inr 0) :: (listEncode f₁✝ ++ (listEncode f₂✝ ++ l))))) }))
            (_ :
              sizeOf ↑(listDecode (listEncode f₁✝ ++ (listEncode f₂✝ ++ l))).snd <
                1 + (1 + 1) + sizeOf (listEncode f₁✝ ++ (listEncode f₂✝ ++ l)))).snd =
      l
[PROOFSTEP]
simp only [] at *
[GOAL]
case h.mk.imp
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l✝ : List ((n : ℕ) × BoundedFormula L α n)
n n✝ : ℕ
f₁✝ f₂✝ : BoundedFormula L α n✝
ih1 :
  ∀ (l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)),
    (listDecode (listEncode f₁✝ ++ l)).fst = { fst := n✝, snd := f₁✝ } ∧ ↑(listDecode (listEncode f₁✝ ++ l)).snd = l
ih2 :
  ∀ (l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)),
    (listDecode (listEncode f₂✝ ++ l)).fst = { fst := n✝, snd := f₂✝ } ∧ ↑(listDecode (listEncode f₂✝ ++ l)).snd = l
l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)
⊢ sigmaImp (listDecode (listEncode f₁✝ ++ (listEncode f₂✝ ++ l))).fst
        (listDecode ↑(listDecode (listEncode f₁✝ ++ (listEncode f₂✝ ++ l))).snd).fst =
      { fst := n✝, snd := f₁✝ ⟹ f₂✝ } ∧
    ↑(listDecode ↑(listDecode (listEncode f₁✝ ++ (listEncode f₂✝ ++ l))).snd).snd = l
[PROOFSTEP]
rw [(ih1 _).1, (ih1 _).2, (ih2 _).1, (ih2 _).2, sigmaImp]
[GOAL]
case h.mk.imp
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l✝ : List ((n : ℕ) × BoundedFormula L α n)
n n✝ : ℕ
f₁✝ f₂✝ : BoundedFormula L α n✝
ih1 :
  ∀ (l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)),
    (listDecode (listEncode f₁✝ ++ l)).fst = { fst := n✝, snd := f₁✝ } ∧ ↑(listDecode (listEncode f₁✝ ++ l)).snd = l
ih2 :
  ∀ (l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)),
    (listDecode (listEncode f₂✝ ++ l)).fst = { fst := n✝, snd := f₂✝ } ∧ ↑(listDecode (listEncode f₂✝ ++ l)).snd = l
l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)
⊢ (match { fst := n✝, snd := f₁✝ }, { fst := n✝, snd := f₂✝ } with
      | { fst := m, snd := φ }, { fst := n, snd := ψ } =>
        if h : m = n then { fst := m, snd := φ ⟹ Eq.mp (_ : BoundedFormula L α n = BoundedFormula L α m) ψ }
        else default) =
      { fst := n✝, snd := f₁✝ ⟹ f₂✝ } ∧
    l = l
[PROOFSTEP]
simp only [dite_true]
[GOAL]
case h.mk.imp
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l✝ : List ((n : ℕ) × BoundedFormula L α n)
n n✝ : ℕ
f₁✝ f₂✝ : BoundedFormula L α n✝
ih1 :
  ∀ (l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)),
    (listDecode (listEncode f₁✝ ++ l)).fst = { fst := n✝, snd := f₁✝ } ∧ ↑(listDecode (listEncode f₁✝ ++ l)).snd = l
ih2 :
  ∀ (l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)),
    (listDecode (listEncode f₂✝ ++ l)).fst = { fst := n✝, snd := f₂✝ } ∧ ↑(listDecode (listEncode f₂✝ ++ l)).snd = l
l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)
⊢ { fst := n✝, snd := f₁✝ ⟹ Eq.mp (_ : BoundedFormula L α n✝ = BoundedFormula L α n✝) f₂✝ } =
      { fst := n✝, snd := f₁✝ ⟹ f₂✝ } ∧
    True
[PROOFSTEP]
exact ⟨rfl, trivial⟩
[GOAL]
case h.mk.all
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l✝ : List ((n : ℕ) × BoundedFormula L α n)
n n✝ : ℕ
f✝ : BoundedFormula L α (n✝ + 1)
ih :
  ∀ (l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)),
    (listDecode (listEncode { fst := n✝ + 1, snd := f✝ }.snd ++ l)).fst = { fst := n✝ + 1, snd := f✝ } ∧
      ↑(listDecode (listEncode { fst := n✝ + 1, snd := f✝ }.snd ++ l)).snd = l
l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)
⊢ (listDecode (listEncode { fst := n✝, snd := ∀'f✝ }.snd ++ l)).fst = { fst := n✝, snd := ∀'f✝ } ∧
    ↑(listDecode (listEncode { fst := n✝, snd := ∀'f✝ }.snd ++ l)).snd = l
[PROOFSTEP]
rw [listEncode, cons_append, listDecode]
[GOAL]
case h.mk.all
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l✝ : List ((n : ℕ) × BoundedFormula L α n)
n n✝ : ℕ
f✝ : BoundedFormula L α (n✝ + 1)
ih :
  ∀ (l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)),
    (listDecode (listEncode { fst := n✝ + 1, snd := f✝ }.snd ++ l)).fst = { fst := n✝ + 1, snd := f✝ } ∧
      ↑(listDecode (listEncode { fst := n✝ + 1, snd := f✝ }.snd ++ l)).snd = l
l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)
⊢ (sigmaAll (listDecode (listEncode f✝ ++ l)).fst,
          { val := ↑(listDecode (listEncode f✝ ++ l)).snd,
            property :=
              (_ :
                sizeOf ↑(listDecode (listEncode f✝ ++ l)).snd ≤
                  max 1 (sizeOf (Sum.inr (Sum.inr 1) :: (listEncode f✝ ++ l)))) }).fst =
      { fst := n✝, snd := ∀'f✝ } ∧
    ↑(sigmaAll (listDecode (listEncode f✝ ++ l)).fst,
            { val := ↑(listDecode (listEncode f✝ ++ l)).snd,
              property :=
                (_ :
                  sizeOf ↑(listDecode (listEncode f✝ ++ l)).snd ≤
                    max 1 (sizeOf (Sum.inr (Sum.inr 1) :: (listEncode f✝ ++ l)))) }).snd =
      l
[PROOFSTEP]
simp only
[GOAL]
case h.mk.all
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l✝ : List ((n : ℕ) × BoundedFormula L α n)
n n✝ : ℕ
f✝ : BoundedFormula L α (n✝ + 1)
ih :
  ∀ (l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)),
    (listDecode (listEncode { fst := n✝ + 1, snd := f✝ }.snd ++ l)).fst = { fst := n✝ + 1, snd := f✝ } ∧
      ↑(listDecode (listEncode { fst := n✝ + 1, snd := f✝ }.snd ++ l)).snd = l
l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)
⊢ sigmaAll (listDecode (listEncode f✝ ++ l)).fst = { fst := n✝, snd := ∀'f✝ } ∧
    ↑(listDecode (listEncode f✝ ++ l)).snd = l
[PROOFSTEP]
simp only [] at *
[GOAL]
case h.mk.all
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l✝ : List ((n : ℕ) × BoundedFormula L α n)
n n✝ : ℕ
f✝ : BoundedFormula L α (n✝ + 1)
ih :
  ∀ (l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)),
    (listDecode (listEncode f✝ ++ l)).fst = { fst := n✝ + 1, snd := f✝ } ∧ ↑(listDecode (listEncode f✝ ++ l)).snd = l
l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)
⊢ sigmaAll (listDecode (listEncode f✝ ++ l)).fst = { fst := n✝, snd := ∀'f✝ } ∧
    ↑(listDecode (listEncode f✝ ++ l)).snd = l
[PROOFSTEP]
rw [(ih _).1, (ih _).2, sigmaAll]
[GOAL]
case h.mk.all
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
l✝ : List ((n : ℕ) × BoundedFormula L α n)
n n✝ : ℕ
f✝ : BoundedFormula L α (n✝ + 1)
ih :
  ∀ (l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)),
    (listDecode (listEncode f✝ ++ l)).fst = { fst := n✝ + 1, snd := f✝ } ∧ ↑(listDecode (listEncode f✝ ++ l)).snd = l
l : List ((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ)
⊢ (match { fst := n✝ + 1, snd := f✝ } with
      | { fst := Nat.succ n, snd := φ } => { fst := n, snd := ∀'φ }
      | x => default) =
      { fst := n✝, snd := ∀'f✝ } ∧
    l = l
[PROOFSTEP]
exact ⟨rfl, rfl⟩
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
φ : (n : ℕ) × BoundedFormula L α n
⊢ (fun l => some (listDecode l).fst) ((fun φ => listEncode φ.snd) φ) = some φ
[PROOFSTEP]
have h := listDecode_encode_list [φ]
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
φ : (n : ℕ) × BoundedFormula L α n
h : (listDecode (List.bind [φ] fun φ => listEncode φ.snd)).fst = headI [φ]
⊢ (fun l => some (listDecode l).fst) ((fun φ => listEncode φ.snd) φ) = some φ
[PROOFSTEP]
rw [bind_singleton] at h
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
φ : (n : ℕ) × BoundedFormula L α n
h : (listDecode (listEncode φ.snd)).fst = headI [φ]
⊢ (fun l => some (listDecode l).fst) ((fun φ => listEncode φ.snd) φ) = some φ
[PROOFSTEP]
simp only
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
φ : (n : ℕ) × BoundedFormula L α n
h : (listDecode (listEncode φ.snd)).fst = headI [φ]
⊢ some (listDecode (listEncode φ.snd)).fst = some φ
[PROOFSTEP]
rw [h]
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
φ : (n : ℕ) × BoundedFormula L α n
h : (listDecode (listEncode φ.snd)).fst = headI [φ]
⊢ some (headI [φ]) = some φ
[PROOFSTEP]
rfl
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
⊢ #((n : ℕ) × BoundedFormula L α n) ≤ max ℵ₀ (lift #α + lift (card L))
[PROOFSTEP]
refine' lift_le.1 (BoundedFormula.encoding.card_le_card_list.trans _)
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
⊢ lift #(List BoundedFormula.encoding.Γ) ≤ lift (max ℵ₀ (lift #α + lift (card L)))
[PROOFSTEP]
rw [encoding_Γ, mk_list_eq_max_mk_aleph0, lift_max, lift_aleph0, lift_max, lift_aleph0, max_le_iff]
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
⊢ lift #((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ) ≤ max ℵ₀ (lift (lift #α + lift (card L))) ∧
    ℵ₀ ≤ max ℵ₀ (lift (lift #α + lift (card L)))
[PROOFSTEP]
refine' ⟨_, le_max_left _ _⟩
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
⊢ lift #((k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ) ≤ max ℵ₀ (lift (lift #α + lift (card L)))
[PROOFSTEP]
rw [mk_sum, Term.card_sigma, mk_sum, ← add_eq_max le_rfl, mk_sum, mk_nat]
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
⊢ lift (lift (ℵ₀ + (lift #α + lift #((i : ℕ) × Functions L i))) + lift (lift #((n : ℕ) × Relations L n) + lift ℵ₀)) ≤
    max ℵ₀ (lift (lift #α + lift (card L)))
[PROOFSTEP]
simp only [lift_add, lift_lift, lift_aleph0]
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
⊢ ℵ₀ + (lift #α + lift #((i : ℕ) × Functions L i)) + (lift #((n : ℕ) × Relations L n) + ℵ₀) ≤
    max ℵ₀ (lift #α + lift (card L))
[PROOFSTEP]
rw [← add_assoc, add_comm, ← add_assoc, ← add_assoc, aleph0_add_aleph0, add_assoc, add_eq_max le_rfl, add_assoc, card,
  Symbols, mk_sum, lift_add, lift_lift, lift_lift]