awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 (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),
    (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

Tactic:
exact fun i => Option.isSome_iff_exists.2 ⟨⟨_, ts i⟩, h i⟩

Premises used: Iff.mpr, Option.isSome_iff_exists, Exists.intro
-- 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 (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
⊢ (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.isSome =
    true

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

Premises used: Option.eq_some_iff_get_eq, Iff.mp
-- 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 (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 (rel φ_R ts)).fst (β := fun (n : ℕ) ↦
                        L.BoundedFormula α n))
                      (ts i)))
                (finRange φ_l) ++
              l))
          i).join.isSome =
    true
⊢ (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.get
      h1 =
    Sigma.mk (β := fun (n : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin n)) φ_n (ts i)

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

Premises used: Option.eq_some_iff_get_eq, Iff.mp
-- 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 (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))
⊢ (fun (i : Fin φ_l) ↦
        cast ⋯
          ((((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)) φ_n (ts i)))
                              (finRange φ_l) ++
                            l))
                        i).bind
                    id).get
                ⋯).snd
            (β := fun (k : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin k)))) =
      ts ∧
    listDecode
        (drop φ_l
          (List.map
              (fun (i : Fin φ_l) ↦ Sum.inl (Sigma.mk (β := fun (k : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin k)) φ_n (ts i)))
              (finRange φ_l) ++
            l)) =
      listDecode l

Tactic:
⟨funext fun i => ?_, ?_⟩

Premises used: funext, And.intro
-- 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))
rel :
  ∀ (i : Fin φ_l),
    cast ⋯
        ((((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)) φ_n (ts i)))
                            (finRange φ_l) ++
                          l))
                      i).bind
                  id).get
              ⋯).snd
          (β := fun (k : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin k))) =
      ts i
rel₁ :
  listDecode
      (drop φ_l
        (List.map (fun (i : Fin φ_l) ↦ Sum.inl (Sigma.mk (β := fun (k : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin k)) φ_n (ts i)))
            (finRange φ_l) ++
          l)) =
    listDecode l
⊢ (fun (i : Fin φ_l) ↦
        cast ⋯
          ((((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)) φ_n (ts i)))
                              (finRange φ_l) ++
                            l))
                        i).bind
                    id).get
                ⋯).snd
            (β := fun (k : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin k)))) =
      ts ∧
    listDecode
        (drop φ_l
          (List.map
              (fun (i : Fin φ_l) ↦ Sum.inl (Sigma.mk (β := fun (k : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin k)) φ_n (ts i)))
              (finRange φ_l) ++
            l)) =
      listDecode l

Tactic:
refine ⟨funext fun i => ?_, ?_⟩
-- 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 (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 (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 (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)
⊢ (((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)) φ_n (ts i)))
                        (finRange φ_l) ++
                      l))
                  i).bind
              id).get
          ⋯).snd
      (β := fun (k : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin k)) ≍
    ts i

Tactic:
(Sigma.ext_iff.1 ((Sigma.eta (Option.get _ h1)).trans h2)).2

Premises used: Sigma.eta, Sigma.ext_iff, And.right, Option.get, Iff.mp, Eq.trans
-- 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 (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 (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 (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)
⊢ (((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)) φ_n (ts i)))
                        (finRange φ_l) ++
                      l))
                  i).bind
              id).get
          ⋯).snd
      (β := fun (k : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin k)) ≍
    ts i

Tactic:
exact (Sigma.ext_iff.1 ((Sigma.eta (Option.get _ h1)).trans h2)).2

Premises used: Sigma.eta, Sigma.ext_iff, And.right, Option.get, Iff.mp, Eq.trans
-- 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))
rel :
  length (α := (k : ℕ) × Term.{u, v, u'} L (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
      (List.map (fun (i : Fin φ_l) ↦ Sum.inl (Sigma.mk (β := fun (k : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin k)) φ_n (ts i)))
        (finRange φ_l)) ≤
    φ_l
⊢ listDecode
      (drop φ_l
        (List.map (fun (i : Fin φ_l) ↦ Sum.inl (Sigma.mk (β := fun (k : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin k)) φ_n (ts i)))
            (finRange φ_l) ++
          l)) =
    listDecode l

Tactic:
rw [List.drop_append, length_map, length_finRange, Nat.sub_self, drop, drop_eq_nil_of_le,
      nil_append]

Premises used: Nat.sub_self, List.drop, List.length_finRange, List.nil_append, List.length_map, List.drop_append, List.drop_eq_nil_of_le
-- 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))
rel : (finRange φ_l).length ≤ φ_l
rel₁ rel₂ : φ_l ≤ φ_l
⊢ length (α := (k : ℕ) × Term.{u, v, u'} L (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
      (List.map (fun (i : Fin φ_l) ↦ Sum.inl (Sigma.mk (β := fun (k : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin k)) φ_n (ts i)))
        (finRange φ_l)) ≤
    φ_l

Tactic:
rw [length_map, length_finRange]

Premises used: List.length_finRange, List.length_map
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
l_1 : List ((n : ℕ) × L.BoundedFormula α n)
n n_1 : ℕ
f₁ f₂ : L.BoundedFormula α n_1
ih1 :
  ∀ (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'
ih2 :
  ∀ (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 ⊕ ℕ)
imp :
  listDecode ((f₁ ⟹ f₂).listEncode ++ l) =
    Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) n_1 (f₁ ⟹ f₂) :: listDecode l
⊢ listDecode
      ((Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) n_1 (f₁ ⟹ f₂)).snd (β := fun (n : ℕ) ↦
            L.BoundedFormula α n).listEncode ++
        l) =
    Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) n_1 (f₁ ⟹ f₂) :: listDecode l

Tactic:
simp only [] at *
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
l_1 : List ((n : ℕ) × L.BoundedFormula α n)
n n_1 : ℕ
f₁ f₂ : L.BoundedFormula α n_1
ih1 :
  ∀ (l' : List ((k : ℕ) × Term.{u, v, u'} L (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
    listDecode (f₁.listEncode ++ l') = Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) n_1 f₁ :: listDecode l'
ih2 :
  ∀ (l' : List ((k : ℕ) × Term.{u, v, u'} L (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
    listDecode (f₂.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 ⊕ ℕ)
imp :
  (if h : 2 ≤ (listDecode (f₁.listEncode ++ (f₂.listEncode ++ l))).length then
      sigmaImp
          (getElem (valid := fun (as : List ((n : ℕ) × L.BoundedFormula α n)) (i : ℕ) ↦ i < as.length)
            (listDecode (f₁.listEncode ++ (f₂.listEncode ++ l))) 0 ⋯)
          (getElem (valid := fun (as : List ((n : ℕ) × L.BoundedFormula α n)) (i : ℕ) ↦ i < as.length)
            (listDecode (f₁.listEncode ++ (f₂.listEncode ++ l))) 1 h) ::
        drop 2 (listDecode (f₁.listEncode ++ (f₂.listEncode ++ l)))
    else []) =
    Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) n_1 (f₁ ⟹ f₂) :: listDecode l
⊢ listDecode ((f₁ ⟹ f₂).listEncode ++ l) =
    Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) n_1 (f₁ ⟹ f₂) :: listDecode l

Tactic:
rw [listEncode, List.append_assoc, cons_append, listDecode]

Premises used: List.append_assoc, FirstOrder.Language.BoundedFormula.listDecode, FirstOrder.Language.BoundedFormula.listEncode, List.cons_append