-- Mathlib/ModelTheory/Encoding.lean
theorem listDecode_encode_list (l : List (L.Term α)) :
    listDecode (l.flatMap listEncode) = l

Proof state:
case cons
L : Language
α : Type u'
l✝ : List (L.Term α)
n : ℕ
f : L.Functions n
ts : Fin n → L.Term α
ih : ∀ (a : Fin n) (l : List (α ⊕ (i : ℕ) × L.Functions i)), listDecode ((ts a).listEncode ++ l) = ts a :: listDecode l
l : List (α ⊕ (i : ℕ) × L.Functions i)
i : Fin n
l' : List (Fin n)
l'ih : listDecode (flatMap (fun i => (ts i).listEncode) l' ++ l) = List.map ts l' ++ listDecode l
⊢ listDecode (flatMap (fun i => (ts i).listEncode) (i :: l') ++ l) = List.map ts (i :: l') ++ listDecode l

Tactic:
rw [flatMap_cons, List.append_assoc, ih, map_cons, l'ih, cons_append]

Result:
no goals

Proof state:
case nil
L : Language
α : Type u'
l✝ : List (L.Term α)
n : ℕ
f : L.Functions n
ts : Fin n → L.Term α
ih : ∀ (a : Fin n) (l : List (α ⊕ (i : ℕ) × L.Functions i)), listDecode ((ts a).listEncode ++ l) = ts a :: listDecode l
l : List (α ⊕ (i : ℕ) × L.Functions i)
⊢ listDecode (flatMap (fun i => (ts i).listEncode) [] ++ l) = List.map ts [] ++ listDecode l

Tactic:
rfl

Result:
no goals

Proof state:
case cons
L : Language
α : Type u'
h : ∀ (t : L.Term α) (l : List (α ⊕ (i : ℕ) × L.Functions i)), listDecode (t.listEncode ++ l) = t :: listDecode l
t : L.Term α
l : List (L.Term α)
lih : listDecode (flatMap listEncode l) = l
⊢ listDecode (flatMap listEncode (t :: l)) = t :: l

Tactic:
rw [flatMap_cons, h t (l.flatMap listEncode), lih]

Result:
no goals

Proof state:
L : Language
α : Type u'
l : List (L.Term α)
⊢ ∀ (t : L.Term α) (l : List (α ⊕ (i : ℕ) × L.Functions i)), listDecode (t.listEncode ++ l) = t :: listDecode l

Tactic:
intro t

Result:
L : Language
α : Type u'
l : List (L.Term α)
t : L.Term α
⊢ ∀ (l : List (α ⊕ (i : ℕ) × L.Functions i)), listDecode (t.listEncode ++ l) = t :: listDecode l

Proof state:
case func.refine_2
L : Language
α : Type u'
l✝ : List (L.Term α)
n : ℕ
f : L.Functions n
ts : Fin n → L.Term α
ih : ∀ (a : Fin n) (l : List (α ⊕ (i : ℕ) × L.Functions i)), listDecode ((ts a).listEncode ++ l) = ts a :: listDecode l
l : List (α ⊕ (i : ℕ) × L.Functions i)
h : listDecode (flatMap (fun i => (ts i).listEncode) (finRange n) ++ l) = List.map ts (finRange n) ++ listDecode l
⊢ drop n (List.map ts (finRange n) ++ listDecode l) = listDecode l

Tactic:
simp only [length_map, length_finRange, drop_left']

Result:
no goals

Proof state:
L : Language
α : Type u'
l : List (L.Term α)
h : ∀ (t : L.Term α) (l : List (α ⊕ (i : ℕ) × L.Functions i)), listDecode (t.listEncode ++ l) = t :: listDecode l
⊢ listDecode (flatMap listEncode l) = l

Tactic:
induction' l with t l lih

Result:
case nil
L : Language
α : Type u'
h : ∀ (t : L.Term α) (l : List (α ⊕ (i : ℕ) × L.Functions i)), listDecode (t.listEncode ++ l) = t :: listDecode l
⊢ listDecode (flatMap listEncode []) = []

case cons
L : Language
α : Type u'
h : ∀ (t : L.Term α) (l : List (α ⊕ (i : ℕ) × L.Functions i)), listDecode (t.listEncode ++ l) = t :: listDecode l
t : L.Term α
l : List (L.Term α)
lih : listDecode (flatMap listEncode l) = l
⊢ listDecode (flatMap listEncode (t :: l)) = t :: l

Proof state:
L : Language
α : Type u'
l✝ : List (L.Term α)
n : ℕ
f : L.Functions n
ts : Fin n → L.Term α
ih : ∀ (a : Fin n) (l : List (α ⊕ (i : ℕ) × L.Functions i)), listDecode ((ts a).listEncode ++ l) = ts a :: listDecode l
l : List (α ⊕ (i : ℕ) × L.Functions i)
⊢ listDecode (flatMap (fun i => (ts i).listEncode) (finRange n) ++ l) = List.map ts (finRange n) ++ listDecode l

Tactic:
induction' finRange n with i l' l'ih

Result:
case nil
L : Language
α : Type u'
l✝ : List (L.Term α)
n : ℕ
f : L.Functions n
ts : Fin n → L.Term α
ih : ∀ (a : Fin n) (l : List (α ⊕ (i : ℕ) × L.Functions i)), listDecode ((ts a).listEncode ++ l) = ts a :: listDecode l
l : List (α ⊕ (i : ℕ) × L.Functions i)
⊢ listDecode (flatMap (fun i => (ts i).listEncode) [] ++ l) = List.map ts [] ++ listDecode l

case cons
L : Language
α : Type u'
l✝ : List (L.Term α)
n : ℕ
f : L.Functions n
ts : Fin n → L.Term α
ih : ∀ (a : Fin n) (l : List (α ⊕ (i : ℕ) × L.Functions i)), listDecode ((ts a).listEncode ++ l) = ts a :: listDecode l
l : List (α ⊕ (i : ℕ) × L.Functions i)
i : Fin n
l' : List (Fin n)
l'ih : listDecode (flatMap (fun i => (ts i).listEncode) l' ++ l) = List.map ts l' ++ listDecode l
⊢ listDecode (flatMap (fun i => (ts i).listEncode) (i :: l') ++ l) = List.map ts (i :: l') ++ listDecode l

Proof state:
case var
L : Language
α : Type u'
l✝ : List (L.Term α)
a : α
l : List (α ⊕ (i : ℕ) × L.Functions i)
⊢ listDecode ((var a).listEncode ++ l) = var a :: listDecode l

Tactic:
rw [listEncode, singleton_append, listDecode]

Result:
no goals

Proof state:
case nil
L : Language
α : Type u'
h : ∀ (t : L.Term α) (l : List (α ⊕ (i : ℕ) × L.Functions i)), listDecode (t.listEncode ++ l) = t :: listDecode l
⊢ listDecode (flatMap listEncode []) = []

Tactic:
rfl

Result:
no goals

Proof state:
case func.refine_1
L : Language
α : Type u'
l✝ : List (L.Term α)
n : ℕ
f : L.Functions n
ts : Fin n → L.Term α
ih : ∀ (a : Fin n) (l : List (α ⊕ (i : ℕ) × L.Functions i)), listDecode ((ts a).listEncode ++ l) = ts a :: listDecode l
l : List (α ⊕ (i : ℕ) × L.Functions i)
h : listDecode (flatMap (fun i => (ts i).listEncode) (finRange n) ++ l) = List.map ts (finRange n) ++ listDecode l
i : Fin n
⊢ (List.map ts (finRange n) ++ listDecode l)[↑i] = ts i

Tactic:
simp only [length_map, length_finRange, is_lt, getElem_append_left, getElem_map,
getElem_finRange, cast_mk, Fin.eta]

Result:
no goals

Proof state:
case func
L : Language
α : Type u'
l✝ : List (L.Term α)
n : ℕ
f : L.Functions n
ts : Fin n → L.Term α
ih : ∀ (a : Fin n) (l : List (α ⊕ (i : ℕ) × L.Functions i)), listDecode ((ts a).listEncode ++ l) = ts a :: listDecode l
l : List (α ⊕ (i : ℕ) × L.Functions i)
h : listDecode (flatMap (fun i => (ts i).listEncode) (finRange n) ++ l) = List.map ts (finRange n) ++ listDecode l
⊢ (if h : n ≤ (listDecode (flatMap (fun i => (ts i).listEncode) (finRange n) ++ l)).length then
      (func f fun i => (listDecode (flatMap (fun i => (ts i).listEncode) (finRange n) ++ l))[i]) ::
        drop n (listDecode (flatMap (fun i => (ts i).listEncode) (finRange n) ++ l))
    else []) =
    func f ts :: listDecode l

Tactic:
simp only [h, length_append, length_map, length_finRange, le_add_iff_nonneg_right,
  _root_.zero_le, ↓reduceDIte, getElem_fin, cons.injEq, func.injEq, heq_eq_eq, true_and]

Result:
case func
L : Language
α : Type u'
l✝ : List (L.Term α)
n : ℕ
f : L.Functions n
ts : Fin n → L.Term α
ih : ∀ (a : Fin n) (l : List (α ⊕ (i : ℕ) × L.Functions i)), listDecode ((ts a).listEncode ++ l) = ts a :: listDecode l
l : List (α ⊕ (i : ℕ) × L.Functions i)
h : listDecode (flatMap (fun i => (ts i).listEncode) (finRange n) ++ l) = List.map ts (finRange n) ++ listDecode l
⊢ (fun i => (List.map ts (finRange n) ++ listDecode l)[↑i]) = ts ∧
    drop n (List.map ts (finRange n) ++ listDecode l) = listDecode l

Proof state:
case func
L : Language
α : Type u'
l✝ : List (L.Term α)
n : ℕ
f : L.Functions n
ts : Fin n → L.Term α
ih : ∀ (a : Fin n) (l : List (α ⊕ (i : ℕ) × L.Functions i)), listDecode ((ts a).listEncode ++ l) = ts a :: listDecode l
l : List (α ⊕ (i : ℕ) × L.Functions i)
⊢ listDecode ((func f ts).listEncode ++ l) = func f ts :: listDecode l

Tactic:
rw [listEncode, cons_append, listDecode]

Result:
case func
L : Language
α : Type u'
l✝ : List (L.Term α)
n : ℕ
f : L.Functions n
ts : Fin n → L.Term α
ih : ∀ (a : Fin n) (l : List (α ⊕ (i : ℕ) × L.Functions i)), listDecode ((ts a).listEncode ++ l) = ts a :: listDecode l
l : List (α ⊕ (i : ℕ) × L.Functions i)
⊢ (if h : n ≤ (listDecode (flatMap (fun i => (ts i).listEncode) (finRange n) ++ l)).length then
      (func f fun i => (listDecode (flatMap (fun i => (ts i).listEncode) (finRange n) ++ l))[i]) ::
        drop n (listDecode (flatMap (fun i => (ts i).listEncode) (finRange n) ++ l))
    else []) =
    func f ts :: listDecode l