-- 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⟩
⊢ ⟨⟨φ_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

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.get
          ⋯).fst =
      ⟨φ_n, rel φ_R ts⟩.fst

Tactic:
swap

Result:
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.get
          ⋯).fst =
      ⟨φ_n, rel φ_R ts⟩.fst

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

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 (⟨n✝, f₁✝⟩.snd.listEncode ++ l') = ⟨n✝, f₁✝⟩ :: listDecode l'
ih2 :
  ∀ (l' : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
    listDecode (⟨n✝, f₂✝⟩.snd.listEncode ++ l') = ⟨n✝, f₂✝⟩ :: listDecode l'
⊢ ∀ (l' : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
    listDecode (⟨n✝, f₁✝ ⟹ f₂✝⟩.snd.listEncode ++ l') = ⟨n✝, f₁✝ ⟹ f₂✝⟩ :: listDecode l'

Tactic:
intro l

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 (⟨n✝, f₁✝⟩.snd.listEncode ++ l') = ⟨n✝, f₁✝⟩ :: listDecode l'
ih2 :
  ∀ (l' : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
    listDecode (⟨n✝, f₂✝⟩.snd.listEncode ++ l') = ⟨n✝, f₂✝⟩ :: listDecode l'
l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
⊢ listDecode (⟨n✝, f₁✝ ⟹ f₂✝⟩.snd.listEncode ++ l) = ⟨n✝, f₁✝ ⟹ f₂✝⟩ :: listDecode 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.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

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⟩
⊢ ⟨⟨φ_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

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.get
          ⋯).fst =
      ⟨φ_n, rel φ_R ts⟩.fst

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
⊢ ∃ (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⟩

Tactic:
refine ⟨lt_of_lt_of_le i.2 le_self_add, ?_⟩

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