-- Mathlib/ModelTheory/Encoding.lean
theorem listDecode_encode_list (l : List (Σn, L.BoundedFormula α n)) :
    listDecode (l.flatMap (fun φ => φ.2.listEncode)) = l

Proof state:
L : Language
α : Type u'
l✝ : List ((n : ℕ) × L.BoundedFormula α n)
n φ_n φ_l : ℕ
φ_R : L.Relations φ_l
ts : Fin φ_l → L.Term (α ⊕ Fin φ_n)
l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
i : Fin φ_l
⊢ (Sum.getLeft? ∘ fun i => Sum.inl ⟨φ_n, ts i⟩) (finRange φ_l)[↑⟨↑i, ⋯⟩] = some ⟨φ_n, ts i⟩

Tactic:
simp only [getElem_finRange, cast_mk, Fin.eta, Function.comp_apply, Sum.getLeft?_inl]

Result:
no goals

Proof state:
L : Language
α : Type u'
l✝ : List ((n : ℕ) × L.BoundedFormula α n)
n φ_n φ_l : ℕ
φ_R : L.Relations φ_l
ts : Fin φ_l → L.Term (α ⊕ Fin φ_n)
l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
⊢ ∀ (i : Fin φ_l),
    ((List.map Sum.getLeft? (List.map (fun i => Sum.inl ⟨⟨φ_n, rel φ_R ts⟩.fst, ts i⟩) (finRange φ_l) ++ l)).get?
          ↑i).join =
      some ⟨φ_n, ts i⟩

Tactic:
intro i

Result:
L : Language
α : Type u'
l✝ : List ((n : ℕ) × L.BoundedFormula α n)
n φ_n φ_l : ℕ
φ_R : L.Relations φ_l
ts : Fin φ_l → L.Term (α ⊕ Fin φ_n)
l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
i : Fin φ_l
⊢ ((List.map Sum.getLeft? (List.map (fun i => Sum.inl ⟨⟨φ_n, rel φ_R ts⟩.fst, ts i⟩) (finRange φ_l) ++ l)).get?
        ↑i).join =
    some ⟨φ_n, ts i⟩

Proof state:
case mk.all
L : Language
α : Type u'
l : List ((n : ℕ) × L.BoundedFormula α n)
n n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih :
  ∀ (l' : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
    listDecode (⟨n✝ + 1, f✝⟩.snd.listEncode ++ l') = ⟨n✝ + 1, f✝⟩ :: listDecode l'
⊢ ∀ (l' : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
    listDecode (⟨n✝, ∀'f✝⟩.snd.listEncode ++ l') = ⟨n✝, ∀'f✝⟩ :: listDecode l'

Tactic:
intro l

Result:
case mk.all
L : Language
α : Type u'
l✝ : List ((n : ℕ) × L.BoundedFormula α n)
n n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih :
  ∀ (l' : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
    listDecode (⟨n✝ + 1, f✝⟩.snd.listEncode ++ l') = ⟨n✝ + 1, f✝⟩ :: listDecode l'
l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
⊢ listDecode (⟨n✝, ∀'f✝⟩.snd.listEncode ++ l) = ⟨n✝, ∀'f✝⟩ :: listDecode l

Proof state:
case mk.rel
L : Language
α : Type u'
l : List ((n : ℕ) × L.BoundedFormula α n)
n φ_n φ_l : ℕ
φ_R : L.Relations φ_l
ts : Fin φ_l → L.Term (α ⊕ Fin φ_n)
⊢ ∀ (l' : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
    listDecode (⟨φ_n, rel φ_R ts⟩.snd.listEncode ++ l') = ⟨φ_n, rel φ_R ts⟩ :: listDecode l'

Tactic:
intro l

Result:
case mk.rel
L : Language
α : Type u'
l✝ : List ((n : ℕ) × L.BoundedFormula α n)
n φ_n φ_l : ℕ
φ_R : L.Relations φ_l
ts : Fin φ_l → L.Term (α ⊕ Fin φ_n)
l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
⊢ listDecode (⟨φ_n, rel φ_R ts⟩.snd.listEncode ++ l) = ⟨φ_n, rel φ_R ts⟩ :: listDecode l

Proof state:
case mk.all
L : Language
α : Type u'
l✝ : List ((n : ℕ) × L.BoundedFormula α n)
n n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih :
  ∀ (l' : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
    listDecode (f✝.listEncode ++ l') = ⟨n✝ + 1, f✝⟩ :: listDecode l'
l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
⊢ listDecode ((∀'f✝).listEncode ++ l) = ⟨n✝, ∀'f✝⟩ :: listDecode l

Tactic:
rw [listEncode, cons_append, listDecode]

Result:
case mk.all
L : Language
α : Type u'
l✝ : List ((n : ℕ) × L.BoundedFormula α n)
n n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih :
  ∀ (l' : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
    listDecode (f✝.listEncode ++ l') = ⟨n✝ + 1, f✝⟩ :: listDecode l'
l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
⊢ (if h : 1 ≤ (listDecode (f✝.listEncode ++ l)).length then
      sigmaAll (listDecode (f✝.listEncode ++ l))[0] :: drop 1 (listDecode (f✝.listEncode ++ l))
    else []) =
    ⟨n✝, ∀'f✝⟩ :: listDecode l

Proof state:
case mk.imp
L : Language
α : Type u'
l✝ : List ((n : ℕ) × L.BoundedFormula α n)
n n✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula α n✝
ih1 :
  ∀ (l' : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
    listDecode (⟨n✝, f₁✝⟩.snd.listEncode ++ l') = ⟨n✝, f₁✝⟩ :: listDecode l'
ih2 :
  ∀ (l' : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
    listDecode (⟨n✝, f₂✝⟩.snd.listEncode ++ l') = ⟨n✝, f₂✝⟩ :: listDecode l'
l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
⊢ listDecode (⟨n✝, f₁✝ ⟹ f₂✝⟩.snd.listEncode ++ l) = ⟨n✝, f₁✝ ⟹ f₂✝⟩ :: listDecode l

Tactic:
simp only [] at *

Result:
case mk.imp
L : Language
α : Type u'
l✝ : List ((n : ℕ) × L.BoundedFormula α n)
n n✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula α n✝
ih1 :
  ∀ (l' : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
    listDecode (f₁✝.listEncode ++ l') = ⟨n✝, f₁✝⟩ :: listDecode l'
ih2 :
  ∀ (l' : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
    listDecode (f₂✝.listEncode ++ l') = ⟨n✝, f₂✝⟩ :: listDecode l'
l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
⊢ listDecode ((f₁✝ ⟹ f₂✝).listEncode ++ l) = ⟨n✝, f₁✝ ⟹ f₂✝⟩ :: listDecode l

Proof state:
L : Language
α : Type u'
l : List ((n : ℕ) × L.BoundedFormula α n)
⊢ ∀ (φ : (n : ℕ) × L.BoundedFormula α n) (l' : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
    listDecode (φ.snd.listEncode ++ l') = φ :: listDecode l'

Tactic:
rintro ⟨n, φ⟩

Result:
case mk
L : Language
α : Type u'
l : List ((n : ℕ) × L.BoundedFormula α n)
n : ℕ
φ : L.BoundedFormula α n
⊢ ∀ (l' : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
    listDecode (⟨n, φ⟩.snd.listEncode ++ l') = ⟨n, φ⟩ :: listDecode l'

Proof state:
case cons
L : Language
α : Type u'
h :
  ∀ (φ : (n : ℕ) × L.BoundedFormula α n) (l' : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
    listDecode (φ.snd.listEncode ++ l') = φ :: listDecode l'
φ : (n : ℕ) × L.BoundedFormula α n
l : List ((n : ℕ) × L.BoundedFormula α n)
ih : listDecode (flatMap (fun φ => φ.snd.listEncode) l) = l
⊢ listDecode (flatMap (fun φ => φ.snd.listEncode) (φ :: l)) = φ :: l

Tactic:
rw [flatMap_cons, h φ _, ih]

Result:
no goals

Proof state:
case mk.rel.refine_1
L : Language
α : Type u'
l✝ : List ((n : ℕ) × L.BoundedFormula α n)
n φ_n φ_l : ℕ
φ_R : L.Relations φ_l
ts : Fin φ_l → L.Term (α ⊕ Fin φ_n)
l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
h :
  ∀ (i : Fin φ_l),
    ((List.map Sum.getLeft? (List.map (fun i => Sum.inl ⟨⟨φ_n, rel φ_R ts⟩.fst, ts i⟩) (finRange φ_l) ++ l)).get?
          ↑i).join =
      some ⟨φ_n, ts i⟩
i : Fin φ_l
⊢ cast ⋯
      ((((List.map Sum.getLeft? (List.map (fun i => Sum.inl ⟨φ_n, ts i⟩) (finRange φ_l) ++ l)).get? ↑i).bind id).get
          ⋯).snd =
    ts i

Tactic:
obtain ⟨h1, h2⟩ := Option.eq_some_iff_get_eq.1 (h i)

Result:
case mk.rel.refine_1.intro
L : Language
α : Type u'
l✝ : List ((n : ℕ) × L.BoundedFormula α n)
n φ_n φ_l : ℕ
φ_R : L.Relations φ_l
ts : Fin φ_l → L.Term (α ⊕ Fin φ_n)
l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
h :
  ∀ (i : Fin φ_l),
    ((List.map Sum.getLeft? (List.map (fun i => Sum.inl ⟨⟨φ_n, rel φ_R ts⟩.fst, ts i⟩) (finRange φ_l) ++ l)).get?
          ↑i).join =
      some ⟨φ_n, ts i⟩
i : Fin φ_l
h1 :
  ((List.map Sum.getLeft? (List.map (fun i => Sum.inl ⟨⟨φ_n, rel φ_R ts⟩.fst, ts i⟩) (finRange φ_l) ++ l)).get?
          ↑i).join.isSome =
    true
h2 :
  ((List.map Sum.getLeft? (List.map (fun i => Sum.inl ⟨⟨φ_n, rel φ_R ts⟩.fst, ts i⟩) (finRange φ_l) ++ l)).get?
            ↑i).join.get
      h1 =
    ⟨φ_n, ts i⟩
⊢ cast ⋯
      ((((List.map Sum.getLeft? (List.map (fun i => Sum.inl ⟨φ_n, ts i⟩) (finRange φ_l) ++ l)).get? ↑i).bind id).get
          ⋯).snd =
    ts i