-- Mathlib/ModelTheory/Encoding.lean
theorem listDecode_encode_list (l : List (Σn, L.BoundedFormula α n)) :
    listDecode (l.flatMap (fun φ => φ.2.listEncode)) = l

Proof state:
case mk.rel.hc.intro
L : Language
α : Type u'
l✝ : List ((n : ℕ) × L.BoundedFormula α n)
n φ_n φ_l : ℕ
φ_R : L.Relations φ_l
ts : Fin φ_l → L.Term (α ⊕ Fin φ_n)
l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
h :
  ∀ (i : Fin φ_l),
    ((List.map Sum.getLeft? (List.map (fun i => Sum.inl ⟨⟨φ_n, rel φ_R ts⟩.fst, ts i⟩) (finRange φ_l) ++ l)).get?
          ↑i).join =
      some ⟨φ_n, ts i⟩
i : Fin φ_l
h1 :
  ((List.map Sum.getLeft? (List.map (fun i => Sum.inl ⟨⟨φ_n, rel φ_R ts⟩.fst, ts i⟩) (finRange φ_l) ++ l)).get?
          ↑i).join.isSome =
    true
h2 :
  ((List.map Sum.getLeft? (List.map (fun i => Sum.inl ⟨⟨φ_n, rel φ_R ts⟩.fst, ts i⟩) (finRange φ_l) ++ l)).get?
            ↑i).join.get
      h1 =
    ⟨φ_n, ts i⟩
⊢ (((List.map Sum.getLeft? (List.map (fun i => Sum.inl ⟨⟨φ_n, rel φ_R ts⟩.fst, ts i⟩) (finRange φ_l) ++ l)).get?
              ↑i).join.get
        ⋯).fst =
    ⟨φ_n, rel φ_R ts⟩.fst

Tactic:
rw [h2]

Result:
no goals

Proof state:
case mk.rel
L : Language
α : Type u'
l✝ : List ((n : ℕ) × L.BoundedFormula α n)
n φ_n φ_l : ℕ
φ_R : L.Relations φ_l
ts : Fin φ_l → L.Term (α ⊕ Fin φ_n)
l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
h :
  ∀ (i : Fin φ_l),
    ((List.map Sum.getLeft? (List.map (fun i => Sum.inl ⟨⟨φ_n, rel φ_R ts⟩.fst, ts i⟩) (finRange φ_l) ++ l)).get?
          ↑i).join =
      some ⟨φ_n, ts i⟩
⊢ ⟨⟨φ_n, rel φ_R ts⟩.fst,
        rel φ_R fun i =>
          ⋯.mp
            (((List.map Sum.getLeft?
                          (List.map (fun i => Sum.inl ⟨⟨φ_n, rel φ_R ts⟩.fst, ts i⟩) (finRange φ_l) ++ l)).get?
                      ↑i).join.get
                ⋯).snd⟩ ::
      listDecode (drop φ_l (List.map (fun i => Sum.inl ⟨⟨φ_n, rel φ_R ts⟩.fst, ts i⟩) (finRange φ_l) ++ l)) =
    ⟨φ_n, rel φ_R ts⟩ :: listDecode l

Tactic:
simp only [Option.join, eq_mp_eq_cast, cons.injEq, Sigma.mk.inj_iff, heq_eq_eq, rel.injEq,
  true_and]

Result:
case mk.rel
L : Language
α : Type u'
l✝ : List ((n : ℕ) × L.BoundedFormula α n)
n φ_n φ_l : ℕ
φ_R : L.Relations φ_l
ts : Fin φ_l → L.Term (α ⊕ Fin φ_n)
l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
h :
  ∀ (i : Fin φ_l),
    ((List.map Sum.getLeft? (List.map (fun i => Sum.inl ⟨⟨φ_n, rel φ_R ts⟩.fst, ts i⟩) (finRange φ_l) ++ l)).get?
          ↑i).join =
      some ⟨φ_n, ts i⟩
⊢ (fun i =>
        cast ⋯
          ((((List.map Sum.getLeft? (List.map (fun i => Sum.inl ⟨φ_n, ts i⟩) (finRange φ_l) ++ l)).get? ↑i).bind id).get
              ⋯).snd) =
      ts ∧
    listDecode (drop φ_l (List.map (fun i => Sum.inl ⟨φ_n, ts i⟩) (finRange φ_l) ++ l)) = listDecode l

Proof state:
case mk.falsum
L : Language
α : Type u'
l : List ((n : ℕ) × L.BoundedFormula α n)
n n✝ : ℕ
⊢ ∀ (l' : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
    listDecode (⟨n✝, falsum⟩.snd.listEncode ++ l') = ⟨n✝, falsum⟩ :: listDecode l'

Tactic:
intro l

Result:
case mk.falsum
L : Language
α : Type u'
l✝ : List ((n : ℕ) × L.BoundedFormula α n)
n n✝ : ℕ
l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
⊢ listDecode (⟨n✝, falsum⟩.snd.listEncode ++ l) = ⟨n✝, falsum⟩ :: listDecode l

Proof state:
L : Language
α : Type u'
l✝ : List ((n : ℕ) × L.BoundedFormula α n)
n φ_n φ_l : ℕ
φ_R : L.Relations φ_l
ts : Fin φ_l → L.Term (α ⊕ Fin φ_n)
l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
i : Fin φ_l
⊢ (List.map (Sum.getLeft? ∘ fun i => Sum.inl ⟨φ_n, ts i⟩) (finRange φ_l) ++ List.map Sum.getLeft? l).get ⟨↑i, ⋯⟩ =
    some ⟨φ_n, ts i⟩

Tactic:
rw [get_eq_getElem, getElem_append_left, getElem_map]

Result:
L : Language
α : Type u'
l✝ : List ((n : ℕ) × L.BoundedFormula α n)
n φ_n φ_l : ℕ
φ_R : L.Relations φ_l
ts : Fin φ_l → L.Term (α ⊕ Fin φ_n)
l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
i : Fin φ_l
⊢ (Sum.getLeft? ∘ fun i => Sum.inl ⟨φ_n, ts i⟩) (finRange φ_l)[↑⟨↑i, ⋯⟩] = some ⟨φ_n, ts i⟩

case h
L : Language
α : Type u'
l✝ : List ((n : ℕ) × L.BoundedFormula α n)
n φ_n φ_l : ℕ
φ_R : L.Relations φ_l
ts : Fin φ_l → L.Term (α ⊕ Fin φ_n)
l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
i : Fin φ_l
⊢ ↑⟨↑i, ⋯⟩ < (List.map (Sum.getLeft? ∘ fun i => Sum.inl ⟨φ_n, ts i⟩) (finRange φ_l)).length

Proof state:
case mk.rel.refine_2
L : Language
α : Type u'
l✝ : List ((n : ℕ) × L.BoundedFormula α n)
n φ_n φ_l : ℕ
φ_R : L.Relations φ_l
ts : Fin φ_l → L.Term (α ⊕ Fin φ_n)
l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
h :
  ∀ (i : Fin φ_l),
    ((List.map Sum.getLeft? (List.map (fun i => Sum.inl ⟨⟨φ_n, rel φ_R ts⟩.fst, ts i⟩) (finRange φ_l) ++ l)).get?
          ↑i).join =
      some ⟨φ_n, ts i⟩
⊢ listDecode (drop φ_l (List.map (fun i => Sum.inl ⟨φ_n, ts i⟩) (finRange φ_l) ++ l)) = listDecode l

Tactic:
rw [List.drop_append_eq_append_drop, length_map, length_finRange, Nat.sub_self, drop,
  drop_eq_nil_of_le, nil_append]

Result:
case mk.rel.refine_2
L : Language
α : Type u'
l✝ : List ((n : ℕ) × L.BoundedFormula α n)
n φ_n φ_l : ℕ
φ_R : L.Relations φ_l
ts : Fin φ_l → L.Term (α ⊕ Fin φ_n)
l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
h :
  ∀ (i : Fin φ_l),
    ((List.map Sum.getLeft? (List.map (fun i => Sum.inl ⟨⟨φ_n, rel φ_R ts⟩.fst, ts i⟩) (finRange φ_l) ++ l)).get?
          ↑i).join =
      some ⟨φ_n, ts i⟩
⊢ (List.map (fun i => Sum.inl ⟨φ_n, ts i⟩) (finRange φ_l)).length ≤ φ_l

Proof state:
case mk.falsum
L : Language
α : Type u'
l✝ : List ((n : ℕ) × L.BoundedFormula α n)
n n✝ : ℕ
l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
⊢ listDecode (⟨n✝, falsum⟩.snd.listEncode ++ l) = ⟨n✝, falsum⟩ :: listDecode l

Tactic:
rw [listEncode, singleton_append, listDecode]

Result:
no goals

Proof state:
case mk.rel.refine_2
L : Language
α : Type u'
l✝ : List ((n : ℕ) × L.BoundedFormula α n)
n φ_n φ_l : ℕ
φ_R : L.Relations φ_l
ts : Fin φ_l → L.Term (α ⊕ Fin φ_n)
l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
h :
  ∀ (i : Fin φ_l),
    ((List.map Sum.getLeft? (List.map (fun i => Sum.inl ⟨⟨φ_n, rel φ_R ts⟩.fst, ts i⟩) (finRange φ_l) ++ l)).get?
          ↑i).join =
      some ⟨φ_n, ts i⟩
⊢ (List.map (fun i => Sum.inl ⟨φ_n, ts i⟩) (finRange φ_l)).length ≤ φ_l

Tactic:
rw [length_map, length_finRange]

Result:
no goals

Proof state:
case mk.imp
L : Language
α : Type u'
l✝ : List ((n : ℕ) × L.BoundedFormula α n)
n n✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula α n✝
ih1 :
  ∀ (l' : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
    listDecode (f₁✝.listEncode ++ l') = ⟨n✝, f₁✝⟩ :: listDecode l'
ih2 :
  ∀ (l' : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
    listDecode (f₂✝.listEncode ++ l') = ⟨n✝, f₂✝⟩ :: listDecode l'
l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
⊢ listDecode ((f₁✝ ⟹ f₂✝).listEncode ++ l) = ⟨n✝, f₁✝ ⟹ f₂✝⟩ :: listDecode l

Tactic:
rw [listEncode, List.append_assoc, cons_append, listDecode]

Result:
case mk.imp
L : Language
α : Type u'
l✝ : List ((n : ℕ) × L.BoundedFormula α n)
n n✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula α n✝
ih1 :
  ∀ (l' : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
    listDecode (f₁✝.listEncode ++ l') = ⟨n✝, f₁✝⟩ :: listDecode l'
ih2 :
  ∀ (l' : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
    listDecode (f₂✝.listEncode ++ l') = ⟨n✝, f₂✝⟩ :: listDecode l'
l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
⊢ (if h : 2 ≤ (listDecode (f₁✝.listEncode ++ (f₂✝.listEncode ++ l))).length then
      sigmaImp (listDecode (f₁✝.listEncode ++ (f₂✝.listEncode ++ l)))[0]
          (listDecode (f₁✝.listEncode ++ (f₂✝.listEncode ++ l)))[1] ::
        drop 2 (listDecode (f₁✝.listEncode ++ (f₂✝.listEncode ++ l)))
    else []) =
    ⟨n✝, f₁✝ ⟹ f₂✝⟩ :: listDecode l