awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ⊕ ℕ)
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
have rel : ∀ (i : Fin φ_l),
  cast sorry
      ((((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
            sorry).snd
        (β := fun (k : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin k))) =
    ts i
Tactic: refine ⟨funext fun i => ?_, ?_⟩
-- 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 ⊕ ℕ)
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
⊢ (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
have 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
Tactic: refine ⟨funext fun i => ?_, ?_⟩
-- 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 ⊕ ℕ)
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
⊢ 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
have 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
Tactic: obtain ⟨h1, h2⟩ := Option.eq_some_iff_get_eq.1 (h i)
-- 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 ⊕ ℕ)
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
⊢ 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
have 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)
Tactic: obtain ⟨h1, h2⟩ := Option.eq_some_iff_get_eq.1 (h i)
-- 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 ⊕ ℕ)
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))
⊢ 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
have 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
Tactic: rw [List.drop_append, length_map, length_finRange, Nat.sub_self, drop, drop_eq_nil_of_le,
      nil_append]
-- 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 ⊕ ℕ)
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))
⊢ 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
have rel : (finRange φ_l).length ≤ φ_l
Tactic: rw [length_map, length_finRange]
-- 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 ⊕ ℕ)
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
⊢ 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
have rel₁ : φ_l ≤ φ_l
Tactic: rw [length_map, length_finRange]
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
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 ⊕ ℕ)
⊢ 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
have imp : listDecode ((f₁ ⟹ f₂).listEncode ++ l) =
  Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) n_1 (f₁ ⟹ f₂) :: listDecode l
Tactic: simp only [] at *
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
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 ⊕ ℕ)
⊢ listDecode ((f₁ ⟹ f₂).listEncode ++ l) =
    Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) n_1 (f₁ ⟹ f₂) :: listDecode l
have 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 sorry)
        (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
Tactic: rw [listEncode, List.append_assoc, cons_append, listDecode]
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
l_1 : List ((n : ℕ) × L.BoundedFormula α n)
n n_1 : ℕ
f : L.BoundedFormula α (n_1 + 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 + 1) f).snd (β := fun (n : ℕ) ↦
              L.BoundedFormula α n).listEncode ++
          l') =
      Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) (n_1 + 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_1 (∀' f)).snd (β := fun (n : ℕ) ↦
            L.BoundedFormula α n).listEncode ++
        l) =
    Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) n_1 (∀' f) :: listDecode l
have all : listDecode ((∀' f).listEncode ++ l) = Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) n_1 (∀' f) :: listDecode l
Tactic: simp only [] at *
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
l_1 : List ((n : ℕ) × L.BoundedFormula α n)
n n_1 : ℕ
f : L.BoundedFormula α (n_1 + 1)
ih :
  ∀ (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 + 1) f :: listDecode l'
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
have all : (if h : 1 ≤ (listDecode (f.listEncode ++ l)).length then
    sigmaAll
        (getElem (valid := fun (as : List ((n : ℕ) × L.BoundedFormula α n)) (i : ℕ) ↦ i < as.length)
          (listDecode (f.listEncode ++ l)) 0 h) ::
      drop 1 (listDecode (f.listEncode ++ l))
  else []) =
  Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) n_1 (∀' f) :: listDecode l
Tactic: rw [listEncode, cons_append, listDecode]
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (hypothesis)
Goal:
L : Language
α : Type u'
φ : (n : ℕ) × L.BoundedFormula α n
⊢ getElem? (valid := fun (as : List ((n : ℕ) × L.BoundedFormula α n)) (i : ℕ) ↦ i < as.length)
      (listDecode φ.snd (β := fun (n : ℕ) ↦ L.BoundedFormula α n).listEncode) 0 =
    some φ
have h : listDecode
    (flatMap (fun (φ : (n : ℕ) × L.BoundedFormula α n) ↦ φ.snd (β := fun (n : ℕ) ↦ L.BoundedFormula α n).listEncode)
      [φ]) =
  [φ]
Tactic: have h := listDecode_encode_list [φ]
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (hypothesis)
Goal:
L : Language
α : Type u'
φ : (n : ℕ) × L.BoundedFormula α n
h :
  listDecode
      (flatMap (fun (φ : (n : ℕ) × L.BoundedFormula α n) ↦ φ.snd (β := fun (n : ℕ) ↦ L.BoundedFormula α n).listEncode)
        [φ]) =
    [φ]
⊢ getElem? (valid := fun (as : List ((n : ℕ) × L.BoundedFormula α n)) (i : ℕ) ↦ i < as.length)
      (listDecode φ.snd (β := fun (n : ℕ) ↦ L.BoundedFormula α n).listEncode) 0 =
    some φ
have h₁ : listDecode φ.snd (β := fun (n : ℕ) ↦ L.BoundedFormula α n).listEncode = [φ]
Tactic: rw [flatMap_singleton] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
φ : (n : ℕ) × L.BoundedFormula α n
h : listDecode φ.snd (β := fun (n : ℕ) ↦ L.BoundedFormula α n).listEncode = [φ]
⊢ getElem? (valid := fun (as : List ((n : ℕ) × L.BoundedFormula α n)) (i : ℕ) ↦ i < as.length)
      (listDecode φ.snd (β := fun (n : ℕ) ↦ L.BoundedFormula α n).listEncode) 0 =
    some φ
have rw : getElem? (valid := fun (as : List ((n : ℕ) × L.BoundedFormula α n)) (i : ℕ) ↦ i < as.length) [φ] 0 = some φ
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
⊢ #((n : ℕ) × L.BoundedFormula α n) ≤ max ℵ₀ (lift.{max u v, u'} #α + lift.{u', max u v} L.card)
have refine : lift.{max (max u' v) u, max (max u' v) u}
    #(List (Encoding.Γ (α := (n : ℕ) × L.BoundedFormula α n) BoundedFormula.encoding)) ≤
  lift.{max (max u u') v, max (max u u') v} (max ℵ₀ (lift.{max u v, u'} #α + lift.{u', max u v} L.card))
Tactic: refine lift_le.1 (BoundedFormula.encoding.card_le_card_list.trans ?_)
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
⊢ lift.{max (max u' v) u, max (max u' v) u}
      #(List (Encoding.Γ (α := (n : ℕ) × L.BoundedFormula α n) BoundedFormula.encoding)) ≤
    lift.{max (max u u') v, max (max u u') v} (max ℵ₀ (lift.{max u v, u'} #α + lift.{u', max u v} L.card))
have rw : lift.{max (max u u') v, max (max u u') v} #((k : ℕ) × Term.{u, v, u'} L (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ) ≤
    max ℵ₀ (lift.{max (max u u') v, max (max u u') v} (lift.{max u v, u'} #α + lift.{u', max u v} L.card)) ∧
  ℵ₀ ≤ max ℵ₀ (lift.{max (max u u') v, max (max u u') v} (lift.{max u v, u'} #α + lift.{u', max u v} L.card))
Tactic: rw [encoding_Γ, mk_list_eq_max_mk_aleph0, lift_max, lift_aleph0, lift_max, lift_aleph0,
    max_le_iff]
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
⊢ lift.{max (max u u') v, max (max u u') v} #((k : ℕ) × Term.{u, v, u'} L (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ) ≤
      max ℵ₀ (lift.{max (max u u') v, max (max u u') v} (lift.{max u v, u'} #α + lift.{u', max u v} L.card)) ∧
    ℵ₀ ≤ max ℵ₀ (lift.{max (max u u') v, max (max u u') v} (lift.{max u v, u'} #α + lift.{u', max u v} L.card))
have refine : lift.{max (max u u') v, max (max u u') v} #((k : ℕ) × Term.{u, v, u'} L (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ) ≤
  max ℵ₀ (lift.{max (max u u') v, max (max u u') v} (lift.{max u v, u'} #α + lift.{u', max u v} L.card))
Tactic: refine ⟨?_, le_max_left _ _⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
⊢ lift.{max (max u u') v, max (max u u') v} #((k : ℕ) × Term.{u, v, u'} L (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ) ≤
    max ℵ₀ (lift.{max (max u u') v, max (max u u') v} (lift.{max u v, u'} #α + lift.{u', max u v} L.card))
have rw : lift.{max (max u u') v, max (max u u') v}
    (lift.{v, max u u'} (ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))) +
      lift.{max u u', v} (lift.{0, v} #((n : ℕ) × L.Relations n) + lift.{v, 0} ℵ₀)) ≤
  max ℵ₀ (lift.{max (max u u') v, max (max u u') v} (lift.{max u v, u'} #α + lift.{u', max u v} L.card))
Tactic: rw [mk_sum, Term.card_sigma, mk_sum, ← add_eq_max le_rfl, mk_sum, mk_nat]