-- 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
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⟩
⊢ (if 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.isSome =
              true then
        if 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.get
                    ⋯).fst =
                ⟨φ_n, rel φ_R ts⟩.fst then
          ⟨⟨φ_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⟩
        else default
      else default) ::
      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:
rw [dif_pos]

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⟩
⊢ (if 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.get
                  ⋯).fst =
              ⟨φ_n, rel φ_R ts⟩.fst then
        ⟨⟨φ_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⟩
      else default) ::
      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

case mk.rel.hc
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),
    ((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

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 ⊕ ℕ)
⊢ listDecode (⟨φ_n, rel φ_R ts⟩.snd.listEncode ++ l) = ⟨φ_n, rel φ_R ts⟩ :: listDecode l

Tactic:
rw [listEncode, cons_append, cons_append, singleton_append, cons_append, listDecode]

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 ⊕ ℕ)
⊢ (if 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.isSome =
              true then
        if 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.get
                    ⋯).fst =
                ⟨φ_n, rel φ_R ts⟩.fst then
          ⟨⟨φ_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⟩
        else default
      else default) ::
      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

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? (List.map (fun i => Sum.inl ⟨⟨φ_n, rel φ_R ts⟩.fst, ts i⟩) (finRange φ_l) ++ l)).get?
        ↑i).join =
    some ⟨φ_n, ts i⟩

Tactic:
simp only [Option.join, map_append, map_map, Option.bind_eq_some, id, exists_eq_right,
  get?_eq_some_iff, length_append, length_map, length_finRange]

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
⊢ ∃ (h : ↑i < φ_l + l.length),
    (List.map (Sum.getLeft? ∘ fun i => Sum.inl ⟨φ_n, ts i⟩) (finRange φ_l) ++ List.map Sum.getLeft? l).get ⟨↑i, ⋯⟩ =
      some ⟨φ_n, ts i⟩

Proof state:
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

Tactic:
simp only [length_map, length_finRange, is_lt]

Result:
no goals

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

Tactic:
simp only [] at *

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