-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
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 ⊕ ℕ)
⊢ listDecode
      ((Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) φ_n (rel φ_R ts)).snd (β := fun (n : ℕ) ↦
            L.BoundedFormula α n).listEncode ++
        l) =
    Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) φ_n (rel φ_R ts) :: listDecode l
have rel : (if h :
        ∀ (i : Fin φ_l),
          (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 (rel φ_R ts)).fst (β :=
                                fun (n : ℕ) ↦ L.BoundedFormula α n))
                              (ts i)))
                        (finRange φ_l) ++
                      l))
                  i).join.isSome =
            true then
      if h' :
          ∀ (i : Fin φ_l),
            ((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 (rel φ_R ts)).fst (β :=
                                        fun (n : ℕ) ↦ L.BoundedFormula α n))
                                      (ts i)))
                                (finRange φ_l) ++
                              l))
                          i).join.get
                    sorry).fst
                (β := fun (k : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin k)) =
              (Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) φ_n (rel φ_R ts)).fst (β := fun (n : ℕ) ↦
                L.BoundedFormula α n) then
        Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n)
          ((Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) φ_n (rel φ_R ts)).fst (β := fun (n : ℕ) ↦
            L.BoundedFormula α n))
          (rel φ_R fun (i : Fin φ_l) ↦
            sorry.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 (rel φ_R ts)).fst (β :=
                                        fun (n : ℕ) ↦ L.BoundedFormula α n))
                                      (ts i)))
                                (finRange φ_l) ++
                              l))
                          i).join.get
                    sorry).snd
                (β := fun (k : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin k))))
      else default
    else default) ::
    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 (rel φ_R ts)).fst (β := fun (n : ℕ) ↦
                    L.BoundedFormula α n))
                  (ts i)))
            (finRange φ_l) ++
          l)) =
  Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) φ_n (rel φ_R ts) :: listDecode l
Tactic: rw [listEncode, cons_append, cons_append, singleton_append, cons_append, listDecode]