-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
l : List ((n : ℕ) × L.BoundedFormula α n)
n : ℕ
φ : L.BoundedFormula α n
falsum :
  ∀ {n : ℕ} (l' : List ((k : ℕ) × Term.{u, v, u'} L (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
    listDecode
        (listEncode (n :=
            Sigma.fst (β := fun (n : ℕ) ↦ L.BoundedFormula α n)
              (Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) n BoundedFormula.falsum))
            (Sigma.snd (β := fun (n : ℕ) ↦ L.BoundedFormula α n)
              (Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) n BoundedFormula.falsum)) ++
          l') =
      Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) n BoundedFormula.falsum :: listDecode l'
equal :
  ∀ {n : ℕ} (t₁ t₂ : 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 (BoundedFormula.equal t₁ t₂)).snd (β := fun (n : ℕ) ↦
              L.BoundedFormula α n).listEncode ++
          l') =
      Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) n (BoundedFormula.equal t₁ t₂) :: listDecode l'
rel :
  ∀ {φ_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 (BoundedFormula.rel φ_R ts)).snd (β := fun (n : ℕ) ↦
              L.BoundedFormula α n).listEncode ++
          l') =
      Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) φ_n (BoundedFormula.rel φ_R ts) :: listDecode l'
imp :
  ∀ {n : ℕ} (f₁ f₂ : L.BoundedFormula α n)
    (ih1 :
      ∀ (l' : List ((k : ℕ) × Term.{u, v, u'} L (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
        listDecode
            ((Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) n f₁).snd (β := fun (n : ℕ) ↦
                  L.BoundedFormula α n).listEncode ++
              l') =
          Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) n f₁ :: listDecode l')
    (ih2 :
      ∀ (l' : List ((k : ℕ) × Term.{u, v, u'} L (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
        listDecode
            ((Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) n f₂).snd (β := fun (n : ℕ) ↦
                  L.BoundedFormula α n).listEncode ++
              l') =
          Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) n f₂ :: listDecode l')
    (l' : List ((k : ℕ) × Term.{u, v, u'} L (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
    listDecode
        ((Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) n (f₁ ⟹ f₂)).snd (β := fun (n : ℕ) ↦
              L.BoundedFormula α n).listEncode ++
          l') =
      Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) n (f₁ ⟹ f₂) :: listDecode l'
all :
  ∀ {n : ℕ} (f : L.BoundedFormula α (n + 1))
    (ih :
      ∀ (l' : List ((k : ℕ) × Term.{u, v, u'} L (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
        listDecode
            ((Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) (n + 1) f).snd (β := fun (n : ℕ) ↦
                  L.BoundedFormula α n).listEncode ++
              l') =
          Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) (n + 1) f :: listDecode l')
    (l' : List ((k : ℕ) × Term.{u, v, u'} L (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
    listDecode
        ((Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) n (∀' f)).snd (β := fun (n : ℕ) ↦
              L.BoundedFormula α n).listEncode ++
          l') =
      Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) n (∀' f) :: listDecode l'
⊢ ∀ (l' : List ((k : ℕ) × Term.{u, v, u'} L (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
    listDecode
        ((Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) n φ).snd (β := fun (n : ℕ) ↦
              L.BoundedFormula α n).listEncode ++
          l') =
      Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) n φ :: listDecode l'

Tactic:
induction φ with
  | falsum => intro l; rw [listEncode, singleton_append, listDecode]
  | equal =>
    intro l
    rw [listEncode, cons_append, cons_append, listDecode, dif_pos]
    · simp only [eq_mp_eq_cast, cast_eq, nil_append]
    · simp only
  | @rel φ_n φ_l φ_R ts =>
    intro l
    rw [listEncode, cons_append, cons_append, singleton_append, cons_append, listDecode]
    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]
    rw [dif_pos]
    swap
    · exact fun i => Option.isSome_iff_exists.2 ⟨⟨_, ts i⟩, h i⟩
    rw [dif_pos]
    swap
    · intro i
      obtain ⟨h1, h2⟩ := Option.eq_some_iff_get_eq.1 (h i)
      rw [h2]
    simp only [Option.join, eq_mp_eq_cast, cons.injEq, Sigma.mk.inj_iff, heq_eq_eq, rel.injEq,
      true_and]
    refine ⟨funext fun i => ?_, ?_⟩
    · obtain ⟨h1, h2⟩ := Option.eq_some_iff_get_eq.1 (h i)
      rw [cast_eq_iff_heq]
      exact (Sigma.ext_iff.1 ((Sigma.eta (Option.get _ h1)).trans h2)).2
    rw [List.drop_append, length_map, length_finRange, Nat.sub_self, drop, drop_eq_nil_of_le,
      nil_append]
    rw [length_map, length_finRange]
  | imp _ _ ih1 ih2 =>
    intro l
    simp only [] at *
    rw [listEncode, List.append_assoc, cons_append, listDecode]
    simp only [ih1, ih2, length_cons, le_add_iff_nonneg_left, _root_.zero_le, ↓reduceDIte,
      getElem_cons_zero, getElem_cons_succ, sigmaImp_apply, drop_succ_cons, drop_zero]
  | all _ ih =>
    intro l
    simp only [] at *
    rw [listEncode, cons_append, listDecode]
    simp only [ih, length_cons, le_add_iff_nonneg_left, _root_.zero_le, ↓reduceDIte,
      getElem_cons_zero, sigmaAll_apply, drop_succ_cons, drop_zero]

Premises used: FirstOrder.Language.BoundedFormula.imp, zero_le, List.append_assoc, List.length_cons, List.drop_zero, eq_mp_eq_cast, heq_eq_eq, reduceDIte, FirstOrder.Language.BoundedFormula.sigmaImp_apply, dif_pos, FirstOrder.Language.BoundedFormula.equal, FirstOrder.Language.BoundedFormula.listDecode, Option.join, List.cons.injEq, cast_eq_iff_heq, Nat.sub_self, FirstOrder.Language.BoundedFormula.falsum, List.getElem_cons_zero, List.drop_succ_cons, List.singleton_append, List.drop, FirstOrder.Language.BoundedFormula.listEncode, cast_eq, List.length_finRange, List.nil_append, List.length_map, Sigma.mk.inj_iff, List.drop_append, FirstOrder.Language.BoundedFormula.sigmaAll_apply, FirstOrder.Language.BoundedFormula.all, List.drop_eq_nil_of_le, List.cons_append, FirstOrder.Language.BoundedFormula.rel, List.getElem_cons_succ, le_add_iff_nonneg_left, true_and, FirstOrder.Language.BoundedFormula.rel.injEq