awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
h1 : Countable α
h2 : Countable.{max (u + 1) 1} ((l : ℕ) × L.Functions l)
⊢ Countable (L.Term α)

Tactic:
mk_le_aleph0_iff.1 (card_le.trans (max_le_iff.2 ?_))

Premises used: Iff.mpr, Cardinal.mk_le_aleph0_iff, max_le_iff, FirstOrder.Language.Term.card_le, Iff.mp, LE.le.trans
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
h1 : Countable α
h2 : Countable.{max (u + 1) 1} ((l : ℕ) × L.Functions l)
refine : ℵ₀ ≤ ℵ₀ ∧ #(Sum.{u', u} α ((i : ℕ) × L.Functions i)) ≤ ℵ₀
⊢ Countable (L.Term α)

Tactic:
refine mk_le_aleph0_iff.1 (card_le.trans (max_le_iff.2 ?_))

Premises used: Iff.mpr, Cardinal.mk_le_aleph0_iff, max_le_iff, FirstOrder.Language.Term.card_le, Iff.mp, LE.le.trans
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
h1 : Countable α
h2 : Countable.{max (u + 1) 1} ((l : ℕ) × L.Functions l)
simp : #α ≤ ℵ₀ ∧ #((i : ℕ) × L.Functions i) ≤ ℵ₀
⊢ ℵ₀ ≤ ℵ₀ ∧ #(Sum.{u', u} α ((i : ℕ) × L.Functions i)) ≤ ℵ₀

Tactic:
simp only [le_refl, mk_sum, add_le_aleph0, lift_le_aleph0, true_and]

Premises used: Cardinal.add_le_aleph0, le_refl, Cardinal.lift_le_aleph0, Cardinal.mk_sum, true_and
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
h1 : Countable α
h2 : Countable.{max (u + 1) 1} ((l : ℕ) × L.Functions l)
⊢ #α ≤ ℵ₀ ∧ #((i : ℕ) × L.Functions i) ≤ ℵ₀

Tactic:
⟨Cardinal.mk_le_aleph0, Cardinal.mk_le_aleph0⟩

Premises used: Cardinal.mk_le_aleph0, And.intro
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
h1 : Countable α
h2 : Countable.{max (u + 1) 1} ((l : ℕ) × L.Functions l)
⊢ #α ≤ ℵ₀ ∧ #((i : ℕ) × L.Functions i) ≤ ℵ₀

Tactic:
exact ⟨Cardinal.mk_le_aleph0, Cardinal.mk_le_aleph0⟩
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
inst : Small.{u, u'} α
⊢ Small.{u, max u u'} (L.Term α)

Tactic:
small_of_injective listEncode_injective

Premises used: small_of_injective, FirstOrder.Language.Term.listEncode_injective
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α (n + 1)
⊢ sigmaAll (Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) (n + 1) φ) =
    Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) n (∀' φ)

Tactic:
rfl

Premises used: FirstOrder.Language.BoundedFormula.sigmaAll, rfl
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
m : ℕ
φ : L.BoundedFormula α m
n : ℕ
ψ : L.BoundedFormula α n
h : m = n
rw rw₁ : L.BoundedFormula α n = L.BoundedFormula α n
⊢ L.BoundedFormula α n = L.BoundedFormula α m

Tactic:
rw [h]
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
n : ℕ
φ ψ : L.BoundedFormula α n
⊢ sigmaImp (Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) n φ)
      (Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) n ψ) =
    Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) n (φ ⟹ ψ)

Tactic:
simp only [sigmaImp, ↓reduceDIte, eq_mp_eq_cast, cast_eq]

Premises used: eq_mp_eq_cast, FirstOrder.Language.BoundedFormula.sigmaImp, reduceDIte, cast_eq
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
n₁ : ℕ
t₁ : Term.{u, v, u'} L (α ⊕ Fin n₁)
n₂ : ℕ
t₂ : Term.{u, v, u'} L (α ⊕ Fin n₂)
l : List ((k : ℕ) × Term.{u, v, u'} L (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
h : n₁ = n₂
rw rw₁ : Term.{u, v, u'} L (α ⊕ Fin n₂) = Term.{u, v, u'} L (α ⊕ Fin n₂)
⊢ Term.{u, v, u'} L (α ⊕ Fin n₂) = Term.{u, v, u'} L (α ⊕ Fin n₁)

Tactic:
rw [h]
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
n : ℕ
R : L.Relations n
k : ℕ
l : List ((k : ℕ) × Term.{u, v, u'} L (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
h :
  ∀ (i : Fin n),
    (getElem? (valid := fun (xs : List (Option ((k : ℕ) × Term.{u, v, u'} L (α ⊕ Fin k)))) (i : Fin n) ↦
            (↑i : ℕ) < xs.length) (List.map Sum.getLeft? l) i).join.isSome =
      true
h' :
  ∀ (i : Fin n),
    ((getElem? (valid := fun (xs : List (Option ((k : ℕ) × Term.{u, v, u'} L (α ⊕ Fin k)))) (i : Fin n) ↦
                  (↑i : ℕ) < xs.length) (List.map Sum.getLeft? l) i).join.get
            ⋯).fst
        (β := fun (k : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin k)) =
      k
i : Fin n
rw rw₁ : Term.{u, v, u'} L (α ⊕ Fin k) = Term.{u, v, u'} L (α ⊕ Fin k)
⊢ Term.{u, v, u'} L
      (α ⊕
        Fin
          (((getElem? (valid := fun (xs : List (Option ((k : ℕ) × Term.{u, v, u'} L (α ⊕ Fin k)))) (i : Fin n) ↦
                      (↑i : ℕ) < xs.length) (List.map Sum.getLeft? l) i).join.get
                ⋯).fst
            (β := fun (k : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin k)))) =
    Term.{u, v, u'} L (α ⊕ Fin k)

Tactic:
rw [h' i]
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
h :
  ∀ (φ : (n : ℕ) × L.BoundedFormula α n)
    (l' : List ((k : ℕ) × Term.{u, v, u'} L (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
    listDecode (φ.snd (β := fun (n : ℕ) ↦ L.BoundedFormula α n).listEncode ++ l') = φ :: listDecode l'
⊢ Eq (α := List ((n : ℕ) × L.BoundedFormula α n))
    (listDecode
      (flatMap (fun (φ : (n : ℕ) × L.BoundedFormula α n) ↦ φ.snd (β := fun (n : ℕ) ↦ L.BoundedFormula α n).listEncode)
        []))
    []

Tactic:
simp [listDecode]

Premises used: FirstOrder.Language.BoundedFormula.listDecode
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
h :
  ∀ (φ : (n : ℕ) × L.BoundedFormula α n)
    (l' : List ((k : ℕ) × Term.{u, v, u'} L (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
    listDecode (φ.snd (β := fun (n : ℕ) ↦ L.BoundedFormula α n).listEncode ++ l') = φ :: listDecode l'
φ : (n : ℕ) × L.BoundedFormula α n
l : List ((n : ℕ) × L.BoundedFormula α n)
ih :
  listDecode
      (flatMap (fun (φ : (n : ℕ) × L.BoundedFormula α n) ↦ φ.snd (β := fun (n : ℕ) ↦ L.BoundedFormula α n).listEncode)
        l) =
    l
cons :
  listDecode
      (φ.snd (β := fun (n : ℕ) ↦ L.BoundedFormula α n).listEncode ++
        flatMap (fun (φ : (n : ℕ) × L.BoundedFormula α n) ↦ φ.snd (β := fun (n : ℕ) ↦ L.BoundedFormula α n).listEncode)
          l) =
    φ :: l
cons₁ :
  φ ::
      listDecode
        (flatMap (fun (φ : (n : ℕ) × L.BoundedFormula α n) ↦ φ.snd (β := fun (n : ℕ) ↦ L.BoundedFormula α n).listEncode)
          l) =
    φ :: l
cons₂ cons₃ : φ :: l = φ :: l
⊢ listDecode
      (flatMap (fun (φ : (n : ℕ) × L.BoundedFormula α n) ↦ φ.snd (β := fun (n : ℕ) ↦ L.BoundedFormula α n).listEncode)
        (φ :: l)) =
    φ :: l

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

Premises used: List.flatMap_cons
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
l : List ((n : ℕ) × L.BoundedFormula α n)
h :
  ∀ (φ : (n : ℕ) × L.BoundedFormula α n)
    (l' : List ((k : ℕ) × Term.{u, v, u'} L (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
    listDecode (φ.snd (β := fun (n : ℕ) ↦ L.BoundedFormula α n).listEncode ++ l') = φ :: listDecode l'
nil :
  Eq (α := List ((n : ℕ) × L.BoundedFormula α n))
    (listDecode
      (flatMap (fun (φ : (n : ℕ) × L.BoundedFormula α n) ↦ φ.snd (β := fun (n : ℕ) ↦ L.BoundedFormula α n).listEncode)
        []))
    []
cons :
  ∀ (φ : (n : ℕ) × L.BoundedFormula α n) (l : List ((n : ℕ) × L.BoundedFormula α n))
    (ih :
      listDecode
          (flatMap
            (fun (φ : (n : ℕ) × L.BoundedFormula α n) ↦ φ.snd (β := fun (n : ℕ) ↦ L.BoundedFormula α n).listEncode) l) =
        l),
    listDecode
        (flatMap (fun (φ : (n : ℕ) × L.BoundedFormula α n) ↦ φ.snd (β := fun (n : ℕ) ↦ L.BoundedFormula α n).listEncode)
          (φ :: l)) =
      φ :: l
⊢ listDecode
      (flatMap (fun (φ : (n : ℕ) × L.BoundedFormula α n) ↦ φ.snd (β := fun (n : ℕ) ↦ L.BoundedFormula α n).listEncode)
        l) =
    l

Tactic:
induction l with
    | nil =>
      simp [listDecode]
    | cons φ l ih => rw [flatMap_cons, h φ _, ih]

Premises used: FirstOrder.Language.BoundedFormula.listDecode, List.flatMap_cons, List.nil
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
l : List ((n : ℕ) × L.BoundedFormula α n)
suffices :
  ∀ (φ : (n : ℕ) × L.BoundedFormula α n)
    (l' : List ((k : ℕ) × Term.{u, v, u'} L (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
    listDecode (φ.snd (β := fun (n : ℕ) ↦ L.BoundedFormula α n).listEncode ++ l') = φ :: listDecode l'
⊢ listDecode
      (flatMap (fun (φ : (n : ℕ) × L.BoundedFormula α n) ↦ φ.snd (β := fun (n : ℕ) ↦ L.BoundedFormula α n).listEncode)
        l) =
    l

Tactic:
suffices h : ∀ (φ : Σ n, L.BoundedFormula α n)
      (l' : List ((Σ k, L.Term (α ⊕ Fin k)) ⊕ ((Σ n, L.Relations n) ⊕ ℕ))),
      (listDecode (listEncode φ.2 ++ l')) = φ::(listDecode l') by
    induction l with
    | nil =>
      simp [listDecode]
    | cons φ l ih => rw [flatMap_cons, h φ _, ih]
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
l_1 : List ((n : ℕ) × L.BoundedFormula α n)
n n_1 : ℕ
l : List ((k : ℕ) × Term.{u, v, u'} L (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
falsum :
  listDecode
      ([Sum.inr
            (Sum.inr
              (Sigma.fst (β := fun (n : ℕ) ↦ L.BoundedFormula α n)
                  (Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) n_1 BoundedFormula.falsum) +
                2))] ++
        l) =
    Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) n_1 BoundedFormula.falsum :: listDecode l
falsum₁ :
  listDecode
      (Sum.inr
          (Sum.inr
            (Sigma.fst (β := fun (n : ℕ) ↦ L.BoundedFormula α n)
                (Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) n_1 BoundedFormula.falsum) +
              2)) ::
        l) =
    Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) n_1 BoundedFormula.falsum :: listDecode l
falsum₂ falsum₃ :
  Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n)
        (Sigma.fst (β := fun (n : ℕ) ↦ L.BoundedFormula α n)
          (Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) n_1 BoundedFormula.falsum))
        BoundedFormula.falsum ::
      listDecode l =
    Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) n_1 BoundedFormula.falsum :: listDecode l
⊢ listDecode
      (listEncode (n :=
          Sigma.fst (β := fun (n : ℕ) ↦ L.BoundedFormula α n)
            (Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) n_1 BoundedFormula.falsum))
          (Sigma.snd (β := fun (n : ℕ) ↦ L.BoundedFormula α n)
            (Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) n_1 BoundedFormula.falsum)) ++
        l) =
    Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) n_1 BoundedFormula.falsum :: listDecode l

Tactic:
rw [listEncode, singleton_append, listDecode]

Premises used: FirstOrder.Language.BoundedFormula.listDecode, List.singleton_append, FirstOrder.Language.BoundedFormula.listEncode
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
l_1 : List ((n : ℕ) × L.BoundedFormula α n)
n n_1 : ℕ
t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n_1)
l : List ((k : ℕ) × Term.{u, v, u'} L (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
equal :
  Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n)
        ((Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) n_1 (BoundedFormula.equal t₁ t₂)).fst (β := fun (n : ℕ) ↦
          L.BoundedFormula α n))
        (BoundedFormula.equal t₁ (Eq.mp ⋯ t₂)) ::
      listDecode ([] ++ l) =
    Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) n_1 (BoundedFormula.equal t₁ t₂) :: listDecode l
equal₁ :
  (Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) n_1 (BoundedFormula.equal t₁ t₂)).fst (β := fun (n : ℕ) ↦
      L.BoundedFormula α n) =
    (Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) n_1 (BoundedFormula.equal t₁ t₂)).fst (β := fun (n : ℕ) ↦
      L.BoundedFormula α n)
⊢ listDecode
      ((Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) n_1 (BoundedFormula.equal t₁ t₂)).snd (β := fun (n : ℕ) ↦
            L.BoundedFormula α n).listEncode ++
        l) =
    Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) n_1 (BoundedFormula.equal t₁ t₂) :: listDecode l

Tactic:
rw [listEncode, cons_append, cons_append, listDecode, dif_pos]

Premises used: dif_pos, FirstOrder.Language.BoundedFormula.listDecode, FirstOrder.Language.BoundedFormula.listEncode, List.cons_append
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
l_1 : List ((n : ℕ) × L.BoundedFormula α n)
n n_1 : ℕ
t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n_1)
l : List ((k : ℕ) × Term.{u, v, u'} L (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
⊢ Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n)
        ((Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) n_1 (equal t₁ t₂)).fst (β := fun (n : ℕ) ↦
          L.BoundedFormula α n))
        (equal t₁ (Eq.mp ⋯ t₂)) ::
      listDecode ([] ++ l) =
    Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) n_1 (equal t₁ t₂) :: listDecode l

Tactic:
simp only [eq_mp_eq_cast, cast_eq, nil_append]

Premises used: eq_mp_eq_cast, cast_eq, List.nil_append
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
l_1 : List ((n : ℕ) × L.BoundedFormula α n)
n n_1 : ℕ
t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n_1)
l : List ((k : ℕ) × Term.{u, v, u'} L (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
⊢ (Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) n_1 (equal t₁ t₂)).fst (β := fun (n : ℕ) ↦ L.BoundedFormula α n) =
    (Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) n_1 (equal t₁ t₂)).fst (β := fun (n : ℕ) ↦ L.BoundedFormula α n)

Tactic:
simp only
-- 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 ⊕ ℕ)
i : Fin φ_l
simp :
  ∃ (h : (↑i : ℕ) < φ_l + l.length),
    getElem (valid := fun (as : List (Option ((n : ℕ) × Term.{u, v, u'} L (α ⊕ Fin n)))) (i : ℕ) ↦ i < as.length)
        (List.map
            (Function.comp (β := (n : ℕ) × Term.{u, v, u'} L (α ⊕ Fin n) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ) Sum.getLeft?
              fun (i : Fin φ_l) ↦ Sum.inl (Sigma.mk (β := fun (n : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin n)) φ_n (ts i)))
            (finRange φ_l) ++
          List.map Sum.getLeft? l)
        (↑i : ℕ) ⋯ =
      some (Sigma.mk (β := fun (n : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin n)) φ_n (ts i))
⊢ (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:
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]

Premises used: Fin.getElem?_fin, List.getElem?_eq_some_iff, exists_eq_right, List.length_append, id, List.map_map, Option.join, List.length_finRange, List.length_map, Option.bind_eq_some_iff, List.map_append
-- 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 ⊕ ℕ)
i : Fin φ_l
⊢ ∃ (h : (↑i : ℕ) < φ_l + l.length),
    getElem (valid := fun (as : List (Option ((n : ℕ) × Term.{u, v, u'} L (α ⊕ Fin n)))) (i : ℕ) ↦ i < as.length)
        (List.map
            (Function.comp (β := (n : ℕ) × Term.{u, v, u'} L (α ⊕ Fin n) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ) Sum.getLeft?
              fun (i : Fin φ_l) ↦ Sum.inl (Sigma.mk (β := fun (n : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin n)) φ_n (ts i)))
            (finRange φ_l) ++
          List.map Sum.getLeft? l)
        (↑i : ℕ) ⋯ =
      some (Sigma.mk (β := fun (n : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin n)) φ_n (ts i))

Tactic:
⟨lt_of_lt_of_le i.2 le_self_add, ?_⟩

Premises used: Fin.isLt, Exists.intro, le_self_add, lt_of_lt_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 ⊕ ℕ)
i : Fin φ_l
refine :
  getElem (valid := fun (as : List (Option ((n : ℕ) × Term.{u, v, u'} L (α ⊕ Fin n)))) (i : ℕ) ↦ i < as.length)
      (List.map
          (Function.comp (β := (n : ℕ) × Term.{u, v, u'} L (α ⊕ Fin n) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ) Sum.getLeft?
            fun (i : Fin φ_l) ↦ Sum.inl (Sigma.mk (β := fun (n : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin n)) φ_n (ts i)))
          (finRange φ_l) ++
        List.map Sum.getLeft? l)
      (↑i : ℕ) ⋯ =
    some (Sigma.mk (β := fun (n : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin n)) φ_n (ts i))
⊢ ∃ (h : (↑i : ℕ) < φ_l + l.length),
    getElem (valid := fun (as : List (Option ((n : ℕ) × Term.{u, v, u'} L (α ⊕ Fin n)))) (i : ℕ) ↦ i < as.length)
        (List.map
            (Function.comp (β := (n : ℕ) × Term.{u, v, u'} L (α ⊕ Fin n) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ) Sum.getLeft?
              fun (i : Fin φ_l) ↦ Sum.inl (Sigma.mk (β := fun (n : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin n)) φ_n (ts i)))
            (finRange φ_l) ++
          List.map Sum.getLeft? l)
        (↑i : ℕ) ⋯ =
      some (Sigma.mk (β := fun (n : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin n)) φ_n (ts i))

Tactic:
refine ⟨lt_of_lt_of_le i.2 le_self_add, ?_⟩
-- 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 ⊕ ℕ)
i : Fin φ_l
rw :
  Eq (α := Option ((n : ℕ) × Term.{u, v, u'} L (α ⊕ Fin n)))
    (Function.comp (β := (n : ℕ) × Term.{u, v, u'} L (α ⊕ Fin n) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ) Sum.getLeft?
      (fun (i : Fin φ_l) ↦ Sum.inl (Sigma.mk (β := fun (n : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin n)) φ_n (ts i)))
      (getElem (valid := fun (as : List (Fin φ_l)) (i : ℕ) ↦ i < as.length) (finRange φ_l) (↑i : ℕ) ⋯))
    (some (Sigma.mk (β := fun (n : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin n)) φ_n (ts i)))
h :
  (↑i : ℕ) <
    length (α := Option ((n : ℕ) × Term.{u, v, u'} L (α ⊕ Fin n)))
      (List.map
        (Function.comp (β := (n : ℕ) × Term.{u, v, u'} L (α ⊕ Fin n) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ) Sum.getLeft?
          fun (i : Fin φ_l) ↦ Sum.inl (Sigma.mk (β := fun (n : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin n)) φ_n (ts i)))
        (finRange φ_l))
⊢ getElem (valid := fun (as : List (Option ((n : ℕ) × Term.{u, v, u'} L (α ⊕ Fin n)))) (i : ℕ) ↦ i < as.length)
      (List.map
          (Function.comp (β := (n : ℕ) × Term.{u, v, u'} L (α ⊕ Fin n) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ) Sum.getLeft?
            fun (i : Fin φ_l) ↦ Sum.inl (Sigma.mk (β := fun (n : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin n)) φ_n (ts i)))
          (finRange φ_l) ++
        List.map Sum.getLeft? l)
      (↑i : ℕ) ⋯ =
    some (Sigma.mk (β := fun (n : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin n)) φ_n (ts i))

Tactic:
rw [getElem_append_left, getElem_map]

Premises used: List.getElem_append_left, List.getElem_map
-- 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 ⊕ ℕ)
i : Fin φ_l
⊢ Eq (α := Option ((n : ℕ) × Term.{u, v, u'} L (α ⊕ Fin n)))
    (Function.comp (β := (n : ℕ) × Term.{u, v, u'} L (α ⊕ Fin n) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ) Sum.getLeft?
      (fun (i : Fin φ_l) ↦ Sum.inl (Sigma.mk (β := fun (n : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin n)) φ_n (ts i)))
      (getElem (valid := fun (as : List (Fin φ_l)) (i : ℕ) ↦ i < as.length) (finRange φ_l) (↑i : ℕ) ⋯))
    (some (Sigma.mk (β := fun (n : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin n)) φ_n (ts i)))

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

Premises used: Fin.eta, Sum.getLeft?_inl, Fin.cast_mk, Function.comp_apply, List.getElem_finRange
-- 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 ⊕ ℕ)
i : Fin φ_l
⊢ (↑i : ℕ) <
    length (α := Option ((n : ℕ) × Term.{u, v, u'} L (α ⊕ Fin n)))
      (List.map
        (Function.comp (β := (n : ℕ) × Term.{u, v, u'} L (α ⊕ Fin n) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ) Sum.getLeft?
          fun (i : Fin φ_l) ↦ Sum.inl (Sigma.mk (β := fun (n : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin n)) φ_n (ts i)))
        (finRange φ_l))

Tactic:
simp only [length_map, length_finRange, is_lt]

Premises used: Fin.is_lt, List.length_finRange, List.length_map
-- 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 ⊕ ℕ)
⊢ ∀ (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]
-- 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:
fun i => Option.isSome_iff_exists.2 ⟨⟨_, ts i⟩, h i⟩

Premises used: Iff.mpr, Option.isSome_iff_exists, Exists.intro, Sigma.mk