awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
l_1 : List (L.Term α)
n : ℕ
f : L.Functions n
ts : Fin n → L.Term α
ih :
  ∀ (a : Fin n) (l : List (Sum.{u', u} α ((i : ℕ) × L.Functions i))),
    listDecode ((ts a).listEncode ++ l) = ts a :: listDecode l
l : List (Sum.{u', u} α ((i : ℕ) × L.Functions i))
h :
  listDecode (flatMap (fun (i : Fin n) ↦ (ts i).listEncode) (finRange n) ++ l) =
    List.map ts (finRange n) ++ listDecode l
i : Fin n
⊢ getElem (valid := fun (as : List (L.Term α)) (i : ℕ) ↦ i < as.length) (List.map ts (finRange n) ++ listDecode l)
      (↑i : ℕ) ⋯ =
    ts i

Tactic:
simp only [length_map, length_finRange, is_lt, getElem_append_left, getElem_map,
      getElem_finRange, cast_mk, Fin.eta]

Premises used: Fin.is_lt, Fin.eta, List.getElem_append_left, List.getElem_map, List.length_finRange, List.length_map, Fin.cast_mk, List.getElem_finRange
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
l_1 : List (L.Term α)
n : ℕ
f : L.Functions n
ts : Fin n → L.Term α
ih :
  ∀ (a : Fin n) (l : List (Sum.{u', u} α ((i : ℕ) × L.Functions i))),
    listDecode ((ts a).listEncode ++ l) = ts a :: listDecode l
l : List (Sum.{u', u} α ((i : ℕ) × L.Functions i))
h :
  listDecode (flatMap (fun (i : Fin n) ↦ (ts i).listEncode) (finRange n) ++ l) =
    List.map ts (finRange n) ++ listDecode l
⊢ drop n (List.map ts (finRange n) ++ listDecode l) = listDecode l

Tactic:
simp only [length_map, length_finRange, drop_left']

Premises used: List.length_finRange, List.length_map, List.drop_left'
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
l_1 : List (L.Term α)
t : L.Term α
l : List (Sum.{u', u} α ((i : ℕ) × L.Functions i))
var :
  ∀ (a : α) (l : List (Sum.{u', u} α ((i : ℕ) × L.Functions i))),
    listDecode (listEncode (Language.var a) ++ l) = Language.var a :: listDecode l
func :
  ∀ {n : ℕ} (f : L.Functions n) (ts : Fin n → L.Term α)
    (ih :
      ∀ (a : Fin n) (l : List (Sum.{u', u} α ((i : ℕ) × L.Functions i))),
        listDecode ((ts a).listEncode ++ l) = ts a :: listDecode l)
    (l : List (Sum.{u', u} α ((i : ℕ) × L.Functions i))),
    listDecode ((Language.func f ts).listEncode ++ l) = Language.func f ts :: listDecode l
⊢ listDecode (t.listEncode ++ l) = t :: listDecode l

Tactic:
induction t generalizing l with
  | var => rw [listEncode, singleton_append, listDecode]
  | @func n f ts ih =>
    rw [listEncode, cons_append, listDecode]
    have h : listDecode (((finRange n).flatMap fun i : Fin n => (ts i).listEncode) ++ l) =
        (finRange n).map ts ++ listDecode l := by
      induction finRange n with
      | nil => rfl
      | cons i l' l'ih => rw [flatMap_cons, List.append_assoc, ih, map_cons, l'ih, cons_append]
    simp only [h, length_append, length_map, length_finRange, le_add_iff_nonneg_right,
      _root_.zero_le, ↓reduceDIte, getElem_fin, cons.injEq, func.injEq, heq_eq_eq, true_and]
    refine ⟨funext (fun i => ?_), ?_⟩
    · simp only [length_map, length_finRange, is_lt, getElem_append_left, getElem_map,
      getElem_finRange, cast_mk, Fin.eta]
    · simp only [length_map, length_finRange, drop_left']

Premises used: zero_le, le_add_iff_nonneg_right, FirstOrder.Language.Term.listEncode, heq_eq_eq, reduceDIte, Fin.is_lt, List.length_append, Fin.eta, FirstOrder.Language.Term.func, List.cons.injEq, List.getElem_append_left, List.singleton_append, FirstOrder.Language.Term.var, List.getElem_map, FirstOrder.Language.Term.func.injEq, List.length_finRange, Fin.getElem_fin, List.length_map, Fin.cast_mk, FirstOrder.Language.Term.listDecode, List.cons_append, true_and, List.drop_left', List.getElem_finRange
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
t : L.Term α
⊢ listDecode (flatMap listEncode [t]) = [t]

Tactic:
have h := listDecode_encode_list [t]
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
t : L.Term α
h : listDecode (flatMap listEncode [t]) = [t]
⊢ listDecode t.listEncode = [t]

Tactic:
rw [flatMap_singleton] at h

Premises used: List.flatMap_singleton
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
t : L.Term α
h : listDecode t.listEncode = [t]
⊢ (Option.join do
      let a ← (listDecode t.listEncode).head?
      pure (some a)) =
    some t

Tactic:
simp only [Option.join, h, head?_cons, Option.pure_def, Option.bind_eq_bind, Option.bind_some,
      id_eq]

Premises used: Option.bind_some, Option.bind_eq_bind, Option.join, List.head?_cons, Option.pure_def, id_eq
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
⊢ Function.Injective (α := L.Term α) listEncode

Tactic:
Term.encoding.encode_injective

Premises used: FirstOrder.Language.Term.encoding, Computability.Encoding.encode_injective
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
⊢ #(L.Term α) ≤ max ℵ₀ #(Sum.{u', u} α ((i : ℕ) × L.Functions i))

Tactic:
lift_le.1 (_root_.trans Term.encoding.card_le_card_list (lift_le.2 (mk_list_le_max _)))

Premises used: Iff.mpr, Cardinal.mk_list_le_max, trans, Computability.Encoding.card_le_card_list, FirstOrder.Language.Term.encoding, Iff.mp, Cardinal.lift_le
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
⊢ #((n : ℕ) × Term.{u, v, u'} L (α ⊕ Fin n)) = max ℵ₀ #(Sum.{u', u} α ((i : ℕ) × L.Functions i))

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
refine_1 : #((n : ℕ) × Term.{u, v, u'} L (α ⊕ Fin n)) ≤ max ℵ₀ #(Sum.{u', u} α ((i : ℕ) × L.Functions i))
refine_2 : max ℵ₀ #(Sum.{u', u} α ((i : ℕ) × L.Functions i)) ≤ #((n : ℕ) × Term.{u, v, u'} L (α ⊕ Fin n))
⊢ #((n : ℕ) × Term.{u, v, u'} L (α ⊕ Fin n)) = max ℵ₀ #(Sum.{u', u} α ((i : ℕ) × L.Functions i))

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
refine_1 :
  (Cardinal.sum fun (i : ℕ) ↦ #(Term.{u, v, u'} L (α ⊕ Fin i))) ≤ max ℵ₀ #(Sum.{u', u} α ((i : ℕ) × L.Functions i))
⊢ #((n : ℕ) × Term.{u, v, u'} L (α ⊕ Fin n)) ≤ max ℵ₀ #(Sum.{u', u} α ((i : ℕ) × L.Functions i))

Tactic:
rw [mk_sigma]

Premises used: Cardinal.mk_sigma
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
⊢ (Cardinal.sum fun (i : ℕ) ↦ #(Term.{u, v, u'} L (α ⊕ Fin i))) ≤ max ℵ₀ #(Sum.{u', u} α ((i : ℕ) × L.Functions i))

Tactic:
(sum_le_lift_mk_mul_iSup _).trans ?_

Premises used: Cardinal.sum_le_lift_mk_mul_iSup, LE.le.trans
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
refine_1 :
  lift.{max u u', 0} #ℕ * ⨆ (i : ℕ), #(Term.{u, v, u'} L (α ⊕ Fin i)) ≤
    max ℵ₀ #(Sum.{u', u} α ((i : ℕ) × L.Functions i))
⊢ (Cardinal.sum fun (i : ℕ) ↦ #(Term.{u, v, u'} L (α ⊕ Fin i))) ≤ max ℵ₀ #(Sum.{u', u} α ((i : ℕ) × L.Functions i))

Tactic:
refine (sum_le_lift_mk_mul_iSup _).trans ?_

Premises used: Cardinal.sum_le_lift_mk_mul_iSup, LE.le.trans
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
refine_1 :
  ℵ₀ ≤ max ℵ₀ #(Sum.{u', u} α ((i : ℕ) × L.Functions i)) ∧
    ∀ (i : ℕ), #(Term.{u, v, u'} L (α ⊕ Fin i)) ≤ max ℵ₀ #(Sum.{u', u} α ((i : ℕ) × L.Functions i))
refine_1₁ : Ne (α := Cardinal.{max u u'}) (⨆ (i : ℕ), #(Term.{u, v, u'} L (α ⊕ Fin i))) 0
⊢ lift.{max u u', 0} #ℕ * ⨆ (i : ℕ), #(Term.{u, v, u'} L (α ⊕ Fin i)) ≤
    max ℵ₀ #(Sum.{u', u} α ((i : ℕ) × L.Functions i))

Tactic:
rw [mk_nat, lift_aleph0, mul_eq_max_of_aleph0_le_left le_rfl, max_le_iff,
      ciSup_le_iff' bddAbove_of_small]

Premises used: le_rfl, ciSup_le_iff', Cardinal.mk_nat, max_le_iff, Cardinal.lift_aleph0, Cardinal.bddAbove_of_small, Cardinal.mul_eq_max_of_aleph0_le_left
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
⊢ ℵ₀ ≤ max ℵ₀ #(Sum.{u', u} α ((i : ℕ) × L.Functions i)) ∧
    ∀ (i : ℕ), #(Term.{u, v, u'} L (α ⊕ Fin i)) ≤ max ℵ₀ #(Sum.{u', u} α ((i : ℕ) × L.Functions i))

Tactic:
⟨le_max_left _ _, fun i => card_le.trans ?_⟩

Premises used: And.intro, FirstOrder.Language.Term.card_le, LE.le.trans, le_max_left
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
refine_1 :
  ∀ (i : ℕ),
    max ℵ₀ #(Sum.{u', u} (α ⊕ Fin i) ((i : ℕ) × L.Functions i)) ≤ max ℵ₀ #(Sum.{u', u} α ((i : ℕ) × L.Functions i))
⊢ ℵ₀ ≤ max ℵ₀ #(Sum.{u', u} α ((i : ℕ) × L.Functions i)) ∧
    ∀ (i : ℕ), #(Term.{u, v, u'} L (α ⊕ Fin i)) ≤ max ℵ₀ #(Sum.{u', u} α ((i : ℕ) × L.Functions i))

Tactic:
refine ⟨le_max_left _ _, fun i => card_le.trans ?_⟩
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
i : ℕ
⊢ max ℵ₀ #(Sum.{u', u} (α ⊕ Fin i) ((i : ℕ) × L.Functions i)) ≤ max ℵ₀ #(Sum.{u', u} α ((i : ℕ) × L.Functions i))

Tactic:
max_le (le_max_left _ _) ?_

Premises used: max_le, le_max_left
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
i : ℕ
refine_1 : #(Sum.{u', u} (α ⊕ Fin i) ((i : ℕ) × L.Functions i)) ≤ max ℵ₀ #(Sum.{u', u} α ((i : ℕ) × L.Functions i))
⊢ max ℵ₀ #(Sum.{u', u} (α ⊕ Fin i) ((i : ℕ) × L.Functions i)) ≤ max ℵ₀ #(Sum.{u', u} α ((i : ℕ) × L.Functions i))

Tactic:
refine max_le (le_max_left _ _) ?_

Premises used: max_le, le_max_left
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
i : ℕ
refine_1 : #(Sum.{u', u} (α ⊕ Fin i) ((i : ℕ) × L.Functions i)) ≤ ℵ₀ + #(Sum.{u', u} α ((i : ℕ) × L.Functions i))
refine_1₁ :
  lift.{u, u'} #(α ⊕ Fin i) + lift.{u', u} #((i : ℕ) × L.Functions i) ≤ ℵ₀ + #(Sum.{u', u} α ((i : ℕ) × L.Functions i))
refine_1₂ :
  lift.{u, u'} (lift.{0, u'} #α + lift.{u', 0} #(Fin i)) + lift.{u', u} #((i : ℕ) × L.Functions i) ≤
    ℵ₀ + #(Sum.{u', u} α ((i : ℕ) × L.Functions i))
refine_1₃ :
  lift.{u, u'} (lift.{0, u'} #α + lift.{u', 0} #(Fin i)) + lift.{u', u} #((i : ℕ) × L.Functions i) ≤
    ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))
refine_1₄ :
  lift.{u, u'} (lift.{u', 0} #(Fin i) + lift.{0, u'} #α) + lift.{u', u} #((i : ℕ) × L.Functions i) ≤
    ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))
refine_1₅ :
  lift.{u, u'} (lift.{u', 0} #(Fin i)) + lift.{u, u'} (lift.{0, u'} #α) + lift.{u', u} #((i : ℕ) × L.Functions i) ≤
    ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))
refine_1₆ :
  lift.{u, u'} (lift.{u', 0} #(Fin i)) + (lift.{u, u'} (lift.{0, u'} #α) + lift.{u', u} #((i : ℕ) × L.Functions i)) ≤
    ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))
refine_1₇ :
  lift.{max u' u, 0} #(Fin i) + (lift.{u, u'} (lift.{0, u'} #α) + lift.{u', u} #((i : ℕ) × L.Functions i)) ≤
    ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))
refine_1₈ :
  lift.{max u' u, 0} #(Fin i) + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i)) ≤
    ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))
refine_1₉ :
  lift.{max u' u, 0} (↑i : Cardinal.{0}) + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i)) ≤
    ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))
refine_1₁₀ :
  (↑i : Cardinal.{max u u'}) + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i)) ≤
    ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))
refine_1₁₁ refine_1₁₂ :
  ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i)) ≤
    ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))
⊢ #(Sum.{u', u} (α ⊕ Fin i) ((i : ℕ) × L.Functions i)) ≤ max ℵ₀ #(Sum.{u', u} α ((i : ℕ) × L.Functions i))

Tactic:
grw [← add_eq_max le_rfl, mk_sum, mk_sum, mk_sum, add_comm (Cardinal.lift #α), lift_add,
        add_assoc, lift_lift, lift_lift, mk_fin, lift_natCast, natCast_lt_aleph0]

Premises used: le_rfl, Cardinal.mk_fin, Cardinal.lift_lift, add_assoc, Cardinal.lift, Cardinal.mk, Cardinal.natCast_lt_aleph0, add_comm, Cardinal.add_eq_max, Cardinal.lift_natCast, Cardinal.mk_sum, Cardinal.lift_add
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
refine_1 : LE.le (α := Cardinal.{max u u'}) 1 (⨆ (i : ℕ), #(Term.{u, v, u'} L (α ⊕ Fin i)))
⊢ Ne (α := Cardinal.{max u u'}) (⨆ (i : ℕ), #(Term.{u, v, u'} L (α ⊕ Fin i))) 0

Tactic:
rw [← Cardinal.one_le_iff_ne_zero]

Premises used: Cardinal.one_le_iff_ne_zero
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
⊢ LE.le (α := Cardinal.{max u u'}) 1 (⨆ (i : ℕ), #(Term.{u, v, u'} L (α ⊕ Fin i)))

Tactic:
_root_.trans ?_ (le_ciSup bddAbove_of_small 1)

Premises used: trans, le_ciSup, Cardinal.bddAbove_of_small, OfNat.ofNat
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
refine_1 : 1 ≤ #(Term.{u, v, u'} L (α ⊕ Fin 1))
⊢ LE.le (α := Cardinal.{max u u'}) 1 (⨆ (i : ℕ), #(Term.{u, v, u'} L (α ⊕ Fin i)))

Tactic:
refine _root_.trans ?_ (le_ciSup bddAbove_of_small 1)

Premises used: trans, le_ciSup, Cardinal.bddAbove_of_small, OfNat.ofNat
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
refine_1 : Nonempty (Term.{u, v, u'} L (α ⊕ Fin 1))
⊢ 1 ≤ #(Term.{u, v, u'} L (α ⊕ Fin 1))

Tactic:
rw [Cardinal.one_le_iff_ne_zero, mk_ne_zero_iff]

Premises used: Cardinal.mk_ne_zero_iff, Cardinal.one_le_iff_ne_zero
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
⊢ Nonempty (Term.{u, v, u'} L (α ⊕ Fin 1))

Tactic:
⟨var (Sum.inr 0)⟩

Premises used: Nonempty.intro, FirstOrder.Language.Term.var, Sum.inr, OfNat.ofNat
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
⊢ Nonempty (Term.{u, v, u'} L (α ⊕ Fin 1))

Tactic:
exact ⟨var (Sum.inr 0)⟩
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
refine_2 :
  Infinite ((n : ℕ) × Term.{u, v, u'} L (α ⊕ Fin n)) ∧
    #(Sum.{u', u} α ((i : ℕ) × L.Functions i)) ≤ #((n : ℕ) × Term.{u, v, u'} L (α ⊕ Fin n))
⊢ max ℵ₀ #(Sum.{u', u} α ((i : ℕ) × L.Functions i)) ≤ #((n : ℕ) × Term.{u, v, u'} L (α ⊕ Fin n))

Tactic:
rw [max_le_iff, ← infinite_iff]

Premises used: Cardinal.infinite_iff, max_le_iff
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
⊢ Infinite ((n : ℕ) × Term.{u, v, u'} L (α ⊕ Fin n)) ∧
    #(Sum.{u', u} α ((i : ℕ) × L.Functions i)) ≤ #((n : ℕ) × Term.{u, v, u'} L (α ⊕ Fin n))

Tactic:
⟨Infinite.of_injective
        (fun i => ⟨i + 1, var (Sum.inr (last i))⟩) fun i j ij => ?_, ?_⟩

Premises used: Infinite.of_injective, FirstOrder.Language.Term.var, HAdd.hAdd, Sum.inr, Fin.last, And.intro, Sigma.mk, OfNat.ofNat
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
refine_2 :
  ∀ (i j : ℕ)
    (ij :
      Eq (α := (n : ℕ) × Term.{u, v, u'} L (α ⊕ Fin n))
        ((fun (i : ℕ) ↦
            (Sigma.mk (β := fun (n : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin n)) (i + 1) (var (Sum.inr (last i))) :
              (n : ℕ) × Term.{u, v, u'} L (α ⊕ Fin n)))
          i)
        ((fun (i : ℕ) ↦
            (Sigma.mk (β := fun (n : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin n)) (i + 1) (var (Sum.inr (last i))) :
              (n : ℕ) × Term.{u, v, u'} L (α ⊕ Fin n)))
          j)),
    i = j
refine_2₁ : #(Sum.{u', u} α ((i : ℕ) × L.Functions i)) ≤ #((n : ℕ) × Term.{u, v, u'} L (α ⊕ Fin n))
⊢ Infinite ((n : ℕ) × Term.{u, v, u'} L (α ⊕ Fin n)) ∧
    #(Sum.{u', u} α ((i : ℕ) × L.Functions i)) ≤ #((n : ℕ) × Term.{u, v, u'} L (α ⊕ Fin n))

Tactic:
refine ⟨Infinite.of_injective
        (fun i => ⟨i + 1, var (Sum.inr (last i))⟩) fun i j ij => ?_, ?_⟩
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
i j : ℕ
ij :
  Eq (α := (n : ℕ) × Term.{u, v, u'} L (α ⊕ Fin n))
    ((fun (i : ℕ) ↦
        (Sigma.mk (β := fun (n : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin n)) (i + 1) (var (Sum.inr (last i))) :
          (n : ℕ) × Term.{u, v, u'} L (α ⊕ Fin n)))
      i)
    ((fun (i : ℕ) ↦
        (Sigma.mk (β := fun (n : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin n)) (i + 1) (var (Sum.inr (last i))) :
          (n : ℕ) × Term.{u, v, u'} L (α ⊕ Fin n)))
      j)
refine_2 : i = i
⊢ i = j

Tactic:
cases ij
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
i : ℕ
⊢ i = i

Tactic:
rfl
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
⊢ Nonempty (Sum.{u', u} α ((i : ℕ) × L.Functions i) ↪ (n : ℕ) × Term.{u, v, u'} L (α ⊕ Fin n))

Tactic:
⟨⟨Sum.elim (fun i => ⟨0, var (Sum.inl i)⟩)
        fun F => ⟨1, func F.2 fun _ => var (Sum.inr 0)⟩, ?_⟩⟩

Premises used: Function.Embedding.mk, Sum.inl, Nonempty.intro, FirstOrder.Language.Term.func, FirstOrder.Language.Term.var, Sum.inr, Sigma.mk, OfNat.ofNat, Sigma.snd, Sum.elim
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
refine_2 :
  Function.Injective (α := Sum.{u', u} α ((i : ℕ) × L.Functions i)) (β := (n : ℕ) × Term.{u, v, u'} L (α ⊕ Fin n))
    (Sum.elim (fun (i : α) ↦ Sigma.mk (β := fun (n : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin n)) 0 (var (Sum.inl i)))
      fun (F : (i : ℕ) × L.Functions i) ↦
      Sigma.mk (β := fun (n : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin n)) 1
        (func (F.snd (β := fun (i : ℕ) ↦ L.Functions i)) fun (x : Fin (F.fst (β := fun (i : ℕ) ↦ L.Functions i))) ↦
          var (Sum.inr 0)))
⊢ Nonempty (Sum.{u', u} α ((i : ℕ) × L.Functions i) ↪ (n : ℕ) × Term.{u, v, u'} L (α ⊕ Fin n))

Tactic:
refine ⟨⟨Sum.elim (fun i => ⟨0, var (Sum.inl i)⟩)
        fun F => ⟨1, func F.2 fun _ => var (Sum.inr 0)⟩, ?_⟩⟩
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
a b : α
h :
  Eq (α := (n : ℕ) × Term.{u, v, u'} L (α ⊕ Fin n))
    (Sum.elim (fun (i : α) ↦ Sigma.mk (β := fun (n : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin n)) 0 (var (Sum.inl i)))
      (fun (F : (i : ℕ) × L.Functions i) ↦
        Sigma.mk (β := fun (n : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin n)) 1
          (func (F.snd (β := fun (i : ℕ) ↦ L.Functions i)) fun (x : Fin (F.fst (β := fun (i : ℕ) ↦ L.Functions i))) ↦
            var (Sum.inr 0)))
      (Sum.inl a))
    (Sum.elim (fun (i : α) ↦ Sigma.mk (β := fun (n : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin n)) 0 (var (Sum.inl i)))
      (fun (F : (i : ℕ) × L.Functions i) ↦
        Sigma.mk (β := fun (n : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin n)) 1
          (func (F.snd (β := fun (i : ℕ) ↦ L.Functions i)) fun (x : Fin (F.fst (β := fun (i : ℕ) ↦ L.Functions i))) ↦
            var (Sum.inr 0)))
      (Sum.inl b))
⊢ a = b

Tactic:
simp only [Sum.elim_inl, Sigma.mk.inj_iff, heq_eq_eq, var.injEq, Sum.inl.injEq, true_and]
          at h

Premises used: heq_eq_eq, FirstOrder.Language.Term.var.injEq, Sum.inl.injEq, Sigma.mk.inj_iff, Sum.elim_inl, true_and
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
a b : α
h : a = b
refine_2 refine_2₁ : Eq (α := Sum.{u', u} α ((i : ℕ) × L.Functions i)) (Sum.inl b) (Sum.inl b)
⊢ Eq (α := Sum.{u', u} α ((i : ℕ) × L.Functions i)) (Sum.inl a) (Sum.inl b)

Tactic:
rw [h]
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
a : α
b : (i : ℕ) × L.Functions i
h :
  Eq (α := (n : ℕ) × Term.{u, v, u'} L (α ⊕ Fin n))
    (Sum.elim (fun (i : α) ↦ Sigma.mk (β := fun (n : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin n)) 0 (var (Sum.inl i)))
      (fun (F : (i : ℕ) × L.Functions i) ↦
        Sigma.mk (β := fun (n : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin n)) 1
          (func (F.snd (β := fun (i : ℕ) ↦ L.Functions i)) fun (x : Fin (F.fst (β := fun (i : ℕ) ↦ L.Functions i))) ↦
            var (Sum.inr 0)))
      (Sum.inl a))
    (Sum.elim (fun (i : α) ↦ Sigma.mk (β := fun (n : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin n)) 0 (var (Sum.inl i)))
      (fun (F : (i : ℕ) × L.Functions i) ↦
        Sigma.mk (β := fun (n : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin n)) 1
          (func (F.snd (β := fun (i : ℕ) ↦ L.Functions i)) fun (x : Fin (F.fst (β := fun (i : ℕ) ↦ L.Functions i))) ↦
            var (Sum.inr 0)))
      (Sum.inr b))
⊢ Sum.inl a = Sum.inr b

Tactic:
simp only [Sum.elim_inl, Sum.elim_inr, Sigma.mk.inj_iff, false_and, reduceCtorEq] at h

Premises used: reduceCtorEq, false_and, Sum.elim_inr, Sigma.mk.inj_iff, Sum.elim_inl
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
a : (i : ℕ) × L.Functions i
b : α
h :
  Eq (α := (n : ℕ) × Term.{u, v, u'} L (α ⊕ Fin n))
    (Sum.elim (fun (i : α) ↦ Sigma.mk (β := fun (n : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin n)) 0 (var (Sum.inl i)))
      (fun (F : (i : ℕ) × L.Functions i) ↦
        Sigma.mk (β := fun (n : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin n)) 1
          (func (F.snd (β := fun (i : ℕ) ↦ L.Functions i)) fun (x : Fin (F.fst (β := fun (i : ℕ) ↦ L.Functions i))) ↦
            var (Sum.inr 0)))
      (Sum.inr a))
    (Sum.elim (fun (i : α) ↦ Sigma.mk (β := fun (n : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin n)) 0 (var (Sum.inl i)))
      (fun (F : (i : ℕ) × L.Functions i) ↦
        Sigma.mk (β := fun (n : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin n)) 1
          (func (F.snd (β := fun (i : ℕ) ↦ L.Functions i)) fun (x : Fin (F.fst (β := fun (i : ℕ) ↦ L.Functions i))) ↦
            var (Sum.inr 0)))
      (Sum.inl b))
⊢ Sum.inr a = Sum.inl b

Tactic:
simp only [Sum.elim_inr, Sum.elim_inl, Sigma.mk.inj_iff, false_and, reduceCtorEq] at h

Premises used: reduceCtorEq, false_and, Sum.elim_inr, Sigma.mk.inj_iff, Sum.elim_inl
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
a b : (i : ℕ) × L.Functions i
h :
  Eq (α := (n : ℕ) × Term.{u, v, u'} L (α ⊕ Fin n))
    (Sum.elim (fun (i : α) ↦ Sigma.mk (β := fun (n : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin n)) 0 (var (Sum.inl i)))
      (fun (F : (i : ℕ) × L.Functions i) ↦
        Sigma.mk (β := fun (n : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin n)) 1
          (func (F.snd (β := fun (i : ℕ) ↦ L.Functions i)) fun (x : Fin (F.fst (β := fun (i : ℕ) ↦ L.Functions i))) ↦
            var (Sum.inr 0)))
      (Sum.inr a))
    (Sum.elim (fun (i : α) ↦ Sigma.mk (β := fun (n : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin n)) 0 (var (Sum.inl i)))
      (fun (F : (i : ℕ) × L.Functions i) ↦
        Sigma.mk (β := fun (n : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin n)) 1
          (func (F.snd (β := fun (i : ℕ) ↦ L.Functions i)) fun (x : Fin (F.fst (β := fun (i : ℕ) ↦ L.Functions i))) ↦
            var (Sum.inr 0)))
      (Sum.inr b))
⊢ a.fst (β := fun (i : ℕ) ↦ L.Functions i) = b.fst (β := fun (i : ℕ) ↦ L.Functions i) ∧
    a.snd (β := fun (i : ℕ) ↦ L.Functions i) ≍ b.snd (β := fun (i : ℕ) ↦ L.Functions i) ∧
      HEq (α := Fin (a.fst (β := fun (i : ℕ) ↦ L.Functions i)) → Term.{u, v, u'} L (α ⊕ Fin 1))
        fun (x : Fin (a.fst (β := fun (i : ℕ) ↦ L.Functions i))) ↦ var (Sum.inr 0) (β :=
        Fin (b.fst (β := fun (i : ℕ) ↦ L.Functions i)) → Term.{u, v, u'} L (α ⊕ Fin 1))
        fun (x : Fin (b.fst (β := fun (i : ℕ) ↦ L.Functions i))) ↦ var (Sum.inr 0)

Tactic:
simp only [Sum.elim_inr, Sigma.mk.inj_iff, heq_eq_eq, func.injEq, true_and] at h

Premises used: heq_eq_eq, Sum.elim_inr, FirstOrder.Language.Term.func.injEq, Sigma.mk.inj_iff, true_and
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
a b : (i : ℕ) × L.Functions i
h :
  a.fst (β := fun (i : ℕ) ↦ L.Functions i) = b.fst (β := fun (i : ℕ) ↦ L.Functions i) ∧
    a.snd (β := fun (i : ℕ) ↦ L.Functions i) ≍ b.snd (β := fun (i : ℕ) ↦ L.Functions i) ∧
      HEq (α := Fin (a.fst (β := fun (i : ℕ) ↦ L.Functions i)) → Term.{u, v, u'} L (α ⊕ Fin 1))
        fun (x : Fin (a.fst (β := fun (i : ℕ) ↦ L.Functions i))) ↦ var (Sum.inr 0) (β :=
        Fin (b.fst (β := fun (i : ℕ) ↦ L.Functions i)) → Term.{u, v, u'} L (α ⊕ Fin 1))
        fun (x : Fin (b.fst (β := fun (i : ℕ) ↦ L.Functions i))) ↦ var (Sum.inr 0)
refine_2 refine_2₁ : Eq (α := Sum.{u', u} α ((i : ℕ) × L.Functions i)) (Sum.inr b) (Sum.inr b)
⊢ Eq (α := Sum.{u', u} α ((i : ℕ) × L.Functions i)) (Sum.inr a) (Sum.inr b)

Tactic:
rw [Sigma.ext_iff.2 ⟨h.1, h.2.1⟩]

Premises used: Iff.mpr, Sigma.ext_iff, And.right, And.left, And.intro
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
inst : Encodable α
inst_1 : Encodable ((i : ℕ) × L.Functions i)
t : L.Term α
rw :
  (Option.join do
      let a ← [t].head?
      pure (some a)) =
    some t
⊢ (Option.join do
      let a ← (listDecode t.listEncode).head?
      pure (some a)) =
    some t

Tactic:
rw [← flatMap_singleton listEncode, listDecode_encode_list]

Premises used: FirstOrder.Language.Term.listDecode_encode_list, FirstOrder.Language.Term.listEncode, List.flatMap_singleton
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
inst : Encodable α
inst_1 : Encodable ((i : ℕ) × L.Functions i)
t : L.Term α
⊢ (Option.join do
      let a ← [t].head?
      pure (some a)) =
    some t

Tactic:
simp only [Option.join, head?_cons, Option.pure_def, Option.bind_eq_bind, Option.bind_some,
      id_eq]

Premises used: Option.bind_some, Option.bind_eq_bind, Option.join, List.head?_cons, Option.pure_def, id_eq