-- 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))
i : Fin φ_l
h1 :
  (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.isSome =
    true
h2 :
  (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.get
      h1 =
    Sigma.mk (β := fun (n : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin n)) φ_n (ts i)
rel rel₁ :
  Sigma.fst (β := fun (k : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin k))
      (Sigma.mk (β := fun (n : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin n)) φ_n (ts i)) =
    (Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) φ_n (BoundedFormula.rel φ_R ts)).fst (β := fun (n : ℕ) ↦
      L.BoundedFormula α n)
⊢ ((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
          ⋯).fst
      (β := 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)

Tactic:
rw [h2]