Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case 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))[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))[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))[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:
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 (α ⊕ (Fin n)))) (finRange φ_l) ++ l))[↑i]?).join = some ⟨_, ts i⟩ := by
      intro i
      simp only [Option.join, map_append, map_map, getElem?_fin, id, Option.bind_eq_some_iff,
        getElem?_eq_some_iff, length_append, length_map, length_finRange, exists_eq_right]
      refine ⟨lt_of_lt_of_le i.2 le_self_add, ?_⟩
      rw [getElem_append_left, getElem_map]
      · simp only [getElem_finRange, cast_mk, Fin.eta, Function.comp_apply, Sum.getLeft?_inl]
      · simp only [length_map, length_finRange, is_lt]

Goal state after:
case 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))[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))[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))[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))[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