-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (hypothesis)
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 ⊕ ℕ)
⊢ (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
                      ⋯).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) ↦
              ⋯.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
                      ⋯).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
have 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 (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))
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]