-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
l_1 : List ((n : ℕ) × L.BoundedFormula α n)
n φ_n φ_l : ℕ
φ_R : L.Relations φ_l
ts : Fin φ_l → Term.{u, v, u'} L (α ⊕ Fin φ_n)
l : List ((k : ℕ) × Term.{u, v, u'} L (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
h :
  ∀ (i : Fin φ_l),
    (getElem? (valid := fun (xs : List (Option ((n : ℕ) × Term.{u, v, u'} L (α ⊕ Fin n)))) (i : Fin φ_l) ↦
          (↑i : ℕ) < xs.length)
          (List.map Sum.getLeft?
            (List.map
                (fun (i : Fin φ_l) ↦
                  Sum.inl
                    (Sigma.mk (β := fun (n : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin n))
                      ((Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) φ_n (BoundedFormula.rel φ_R ts)).fst (β :=
                        fun (n : ℕ) ↦ L.BoundedFormula α n))
                      (ts i)))
                (finRange φ_l) ++
              l))
          i).join =
      some (Sigma.mk (β := fun (n : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin n)) φ_n (ts i))
rel :
  (fun (i : Fin φ_l) ↦
        cast ⋯
          ((((getElem? (valid := fun (xs : List (Option ((k : ℕ) × Term.{u, v, u'} L (α ⊕ Fin k)))) (i : Fin φ_l) ↦
                        (↑i : ℕ) < xs.length)
                        (List.map Sum.getLeft?
                          (List.map
                              (fun (i : Fin φ_l) ↦
                                Sum.inl (Sigma.mk (β := fun (k : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin k)) φ_n (ts i)))
                              (finRange φ_l) ++
                            l))
                        i).bind
                    id).get
                ⋯).snd
            (β := fun (k : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin k)))) =
      ts ∧
    listDecode
        (drop φ_l
          (List.map
              (fun (i : Fin φ_l) ↦ Sum.inl (Sigma.mk (β := fun (k : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin k)) φ_n (ts i)))
              (finRange φ_l) ++
            l)) =
      listDecode l
⊢ Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n)
        ((Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) φ_n (BoundedFormula.rel φ_R ts)).fst (β := fun (n : ℕ) ↦
          L.BoundedFormula α n))
        (BoundedFormula.rel φ_R fun (i : Fin φ_l) ↦
          Eq.mp ⋯
            (((getElem? (valid := fun (xs : List (Option ((k : ℕ) × Term.{u, v, u'} L (α ⊕ Fin k)))) (i : Fin φ_l) ↦
                        (↑i : ℕ) < xs.length)
                        (List.map Sum.getLeft?
                          (List.map
                              (fun (i : Fin φ_l) ↦
                                Sum.inl
                                  (Sigma.mk (β := fun (k : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin k))
                                    ((Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) φ_n
                                          (BoundedFormula.rel φ_R ts)).fst
                                      (β := fun (n : ℕ) ↦ L.BoundedFormula α n))
                                    (ts i)))
                              (finRange φ_l) ++
                            l))
                        i).join.get
                  ⋯).snd
              (β := fun (k : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin k)))) ::
      listDecode
        (drop φ_l
          (List.map
              (fun (i : Fin φ_l) ↦
                Sum.inl
                  (Sigma.mk (β := fun (k : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin k))
                    ((Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) φ_n (BoundedFormula.rel φ_R ts)).fst (β :=
                      fun (n : ℕ) ↦ L.BoundedFormula α n))
                    (ts i)))
              (finRange φ_l) ++
            l)) =
    Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) φ_n (BoundedFormula.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]

Premises used: eq_mp_eq_cast, heq_eq_eq, Option.join, List.cons.injEq, Sigma.mk.inj_iff, true_and, FirstOrder.Language.BoundedFormula.rel.injEq