awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.ElementarySubstructures
Goal:
L : Language
M : Type u_1
inst : L.Structure M
S : L.ElementarySubstructure M
D : Set M
x : M
hx : x ∈ D
φ : (withConstants.{u_2, u_3, u_1} L (↑(↑S : Set M) : Type u_1)).Formula (Fin 1)
hφ : Eq.{u_1 + 1} (α := Set (Fin 1 → M)) {x : Fin 1 → M | x 0 ∈ D} (setOf φ.Realize)
hφx : φ.Realize ![x]
ψ : (withConstants.{u_2, u_3, u_1} L (↑(↑S : Set M) : Type u_1)).Sentence := iExs (Fin 1) (relabel Sum.inr φ)
hψM : M ⊨ ψ
v' : Fin 1 → ↥S
hv' : φ.Realize v'
⊢ BoundedFormula.Realize.{u_2, u_3, u_1, u_1} (L := L) (M := M) (α := (↑(↑S : Set M) : Type u_1) ⊕ Fin 1) (l := 0)
    ((BoundedFormula.constantsVarsEquiv :
        (a : L[[(↑(↑S : Set M) : Type u_1)]].BoundedFormula (Fin 1) 0) →
          L.BoundedFormula ((↑(↑S : Set M) : Type u_1) ⊕ Fin 1) 0)
      φ)
    ((⇑S.subtype : (a : ↥S) → M) ∘ Sum.elim (fun (a : (↑(↑S : Set M) : Type u_1)) ↦ (↑(L.con a) : ↥S)) v')
    (Function.comp (β := ↥S) (⇑S.subtype : (a : ↥S) → M) default)

Tactic:
simp only [Formula.Realize, ← BoundedFormula.realize_constantsVarsEquiv,
      ← S.subtype.map_boundedFormula] at hv'

Premises used: FirstOrder.Language.ElementarySubstructure.subtype, FirstOrder.Language.ElementaryEmbedding.map_boundedFormula, FirstOrder.Language.BoundedFormula.realize_constantsVarsEquiv, FirstOrder.Language.Formula.Realize
-- Module: Mathlib.ModelTheory.ElementarySubstructures
Goal:
L : Language
M : Type u_1
inst : L.Structure M
S : L.ElementarySubstructure M
D : Set M
x : M
hx : x ∈ D
φ : (withConstants.{u_2, u_3, u_1} L (↑(↑S : Set M) : Type u_1)).Formula (Fin 1)
hφ : Eq.{u_1 + 1} (α := Set (Fin 1 → M)) {x : Fin 1 → M | x 0 ∈ D} (setOf φ.Realize)
hφx : φ.Realize ![x]
ψ : (withConstants.{u_2, u_3, u_1} L (↑(↑S : Set M) : Type u_1)).Sentence := iExs (Fin 1) (relabel Sum.inr φ)
hψM : M ⊨ ψ
v' : Fin 1 → ↥S
hv' :
  BoundedFormula.Realize.{u_2, u_3, u_1, u_1} (L := L) (M := M) (α := (↑(↑S : Set M) : Type u_1) ⊕ Fin 1) (l := 0)
    ((BoundedFormula.constantsVarsEquiv :
        (a : L[[(↑(↑S : Set M) : Type u_1)]].BoundedFormula (Fin 1) 0) →
          L.BoundedFormula ((↑(↑S : Set M) : Type u_1) ⊕ Fin 1) 0)
      φ)
    ((⇑S.subtype : (a : ↥S) → M) ∘ Sum.elim (fun (a : (↑(↑S : Set M) : Type u_1)) ↦ (↑(L.con a) : ↥S)) v')
    (Function.comp (β := ↥S) (⇑S.subtype : (a : ↥S) → M) default)
simp :
  BoundedFormula.Realize.{u_2, u_3, u_1, u_1} (L := L) (α := (↑(↑S : Set M) : Type u_1) ⊕ Fin 1) (l := 0)
    ((BoundedFormula.constantsVarsEquiv :
        (a : L[[(↑(↑S : Set M) : Type u_1)]].BoundedFormula (Fin 1) 0) →
          L.BoundedFormula ((↑(↑S : Set M) : Type u_1) ⊕ Fin 1) 0)
      φ)
    (Sum.elim (fun (a : (↑(↑S : Set M) : Type u_1)) ↦ (↑(L.con a) : M)) (Subtype.val (p := fun (x : M) ↦ x ∈ S) ∘ v'))
    default
⊢ φ.Realize (Subtype.val (p := fun (x : M) ↦ x ∈ S) ∘ v')

Tactic:
simp only [Formula.Realize, ← BoundedFormula.realize_constantsVarsEquiv]

Premises used: FirstOrder.Language.BoundedFormula.realize_constantsVarsEquiv, FirstOrder.Language.Formula.Realize
-- Module: Mathlib.ModelTheory.ElementarySubstructures
Goal:
L : Language
M : Type u_1
inst : L.Structure M
S : L.ElementarySubstructure M
D : Set M
x : M
hx : x ∈ D
φ : (withConstants.{u_2, u_3, u_1} L (↑(↑S : Set M) : Type u_1)).Formula (Fin 1)
hφ : Eq.{u_1 + 1} (α := Set (Fin 1 → M)) {x : Fin 1 → M | x 0 ∈ D} (setOf φ.Realize)
hφx : φ.Realize ![x]
ψ : (withConstants.{u_2, u_3, u_1} L (↑(↑S : Set M) : Type u_1)).Sentence := iExs (Fin 1) (relabel Sum.inr φ)
hψM : M ⊨ ψ
v' : Fin 1 → ↥S
hv' :
  BoundedFormula.Realize.{u_2, u_3, u_1, u_1} (L := L) (M := M) (α := (↑(↑S : Set M) : Type u_1) ⊕ Fin 1) (l := 0)
    ((BoundedFormula.constantsVarsEquiv :
        (a : L[[(↑(↑S : Set M) : Type u_1)]].BoundedFormula (Fin 1) 0) →
          L.BoundedFormula ((↑(↑S : Set M) : Type u_1) ⊕ Fin 1) 0)
      φ)
    ((⇑S.subtype : (a : ↥S) → M) ∘ Sum.elim (fun (a : (↑(↑S : Set M) : Type u_1)) ↦ (↑(L.con a) : ↥S)) v')
    (Function.comp (β := ↥S) (⇑S.subtype : (a : ↥S) → M) default)
⊢ BoundedFormula.Realize.{u_2, u_3, u_1, u_1} (L := L) (M := M) (α := (↑(↑S : Set M) : Type u_1) ⊕ Fin 1) (l := 0)
    ((BoundedFormula.constantsVarsEquiv :
        (a : L[[(↑(↑S : Set M) : Type u_1)]].BoundedFormula (Fin 1) 0) →
          L.BoundedFormula ((↑(↑S : Set M) : Type u_1) ⊕ Fin 1) 0)
      φ)
    ((⇑S.subtype : (a : ↥S) → M) ∘ Sum.elim (fun (a : (↑(↑S : Set M) : Type u_1)) ↦ (↑(L.con a) : ↥S)) v')
    (Function.comp (β := ↥S) (⇑S.subtype : (a : ↥S) → M) default)

Tactic:
hv'
-- Module: Mathlib.ModelTheory.ElementarySubstructures
Goal:
L : Language
M : Type u_1
inst : L.Structure M
S : L.ElementarySubstructure M
D : Set M
x : M
hx : x ∈ D
φ : (withConstants.{u_2, u_3, u_1} L (↑(↑S : Set M) : Type u_1)).Formula (Fin 1)
hφ : Eq.{u_1 + 1} (α := Set (Fin 1 → M)) {x : Fin 1 → M | x 0 ∈ D} (setOf φ.Realize)
hφx : φ.Realize ![x]
ψ : (withConstants.{u_2, u_3, u_1} L (↑(↑S : Set M) : Type u_1)).Sentence := iExs (Fin 1) (relabel Sum.inr φ)
hψM : M ⊨ ψ
v' : Fin 1 → ↥S
hv' :
  BoundedFormula.Realize.{u_2, u_3, u_1, u_1} (L := L) (M := M) (α := (↑(↑S : Set M) : Type u_1) ⊕ Fin 1) (l := 0)
    ((BoundedFormula.constantsVarsEquiv :
        (a : L[[(↑(↑S : Set M) : Type u_1)]].BoundedFormula (Fin 1) 0) →
          L.BoundedFormula ((↑(↑S : Set M) : Type u_1) ⊕ Fin 1) 0)
      φ)
    ((⇑S.subtype : (a : ↥S) → M) ∘ Sum.elim (fun (a : (↑(↑S : Set M) : Type u_1)) ↦ (↑(L.con a) : ↥S)) v')
    (Function.comp (β := ↥S) (⇑S.subtype : (a : ↥S) → M) default)
h :
  Eq (α := (↑(↑S : Set M) : Type u_1) ⊕ Fin 1 → M)
    (Sum.elim (fun (a : (↑(↑S : Set M) : Type u_1)) ↦ (↑(L.con a) : M)) (Subtype.val (p := fun (x : M) ↦ x ∈ S) ∘ v'))
    ((⇑S.subtype : (a : ↥S) → M) ∘ Sum.elim (fun (a : (↑(↑S : Set M) : Type u_1)) ↦ (↑(L.con a) : ↥S)) v')
⊢ BoundedFormula.Realize.{u_2, u_3, u_1, u_1} (L := L) (α := (↑(↑S : Set M) : Type u_1) ⊕ Fin 1) (l := 0)
    ((BoundedFormula.constantsVarsEquiv :
        (a : L[[(↑(↑S : Set M) : Type u_1)]].BoundedFormula (Fin 1) 0) →
          L.BoundedFormula ((↑(↑S : Set M) : Type u_1) ⊕ Fin 1) 0)
      φ)
    (Sum.elim (fun (a : (↑(↑S : Set M) : Type u_1)) ↦ (↑(L.con a) : M)) (Subtype.val (p := fun (x : M) ↦ x ∈ S) ∘ v'))
    default

Tactic:
convert! hv' using 1
-- Module: Mathlib.ModelTheory.ElementarySubstructures
Goal:
L : Language
M : Type u_1
inst : L.Structure M
S : L.ElementarySubstructure M
D : Set M
x : M
hx : x ∈ D
φ : (withConstants.{u_2, u_3, u_1} L (↑(↑S : Set M) : Type u_1)).Formula (Fin 1)
hφ : Eq.{u_1 + 1} (α := Set (Fin 1 → M)) {x : Fin 1 → M | x 0 ∈ D} (setOf φ.Realize)
hφx : φ.Realize ![x]
ψ : (withConstants.{u_2, u_3, u_1} L (↑(↑S : Set M) : Type u_1)).Sentence := iExs (Fin 1) (relabel Sum.inr φ)
hψM : M ⊨ ψ
v' : Fin 1 → ↥S
hv' :
  BoundedFormula.Realize.{u_2, u_3, u_1, u_1} (L := L) (M := M) (α := (↑(↑S : Set M) : Type u_1) ⊕ Fin 1) (l := 0)
    ((BoundedFormula.constantsVarsEquiv :
        (a : L[[(↑(↑S : Set M) : Type u_1)]].BoundedFormula (Fin 1) 0) →
          L.BoundedFormula ((↑(↑S : Set M) : Type u_1) ⊕ Fin 1) 0)
      φ)
    ((⇑S.subtype : (a : ↥S) → M) ∘ Sum.elim (fun (a : (↑(↑S : Set M) : Type u_1)) ↦ (↑(L.con a) : ↥S)) v')
    (Function.comp (β := ↥S) (⇑S.subtype : (a : ↥S) → M) default)
h :
  ∀ (i : (↑(↑S : Set M) : Type u_1) ⊕ Fin 1),
    Sum.elim (fun (a : (↑(↑S : Set M) : Type u_1)) ↦ (↑(L.con a) : M)) (Subtype.val (p := fun (x : M) ↦ x ∈ S) ∘ v') i =
      ((⇑S.subtype : (a : ↥S) → M) ∘ Sum.elim (fun (a : (↑(↑S : Set M) : Type u_1)) ↦ (↑(L.con a) : ↥S)) v') i
⊢ Eq (α := (↑(↑S : Set M) : Type u_1) ⊕ Fin 1 → M)
    (Sum.elim (fun (a : (↑(↑S : Set M) : Type u_1)) ↦ (↑(L.con a) : M)) (Subtype.val (p := fun (x : M) ↦ x ∈ S) ∘ v'))
    ((⇑S.subtype : (a : ↥S) → M) ∘ Sum.elim (fun (a : (↑(↑S : Set M) : Type u_1)) ↦ (↑(L.con a) : ↥S)) v')

Tactic:
funext i
-- Module: Mathlib.ModelTheory.ElementarySubstructures
Goal:
L : Language
M : Type u_1
inst : L.Structure M
S : L.ElementarySubstructure M
D : Set M
x : M
hx : x ∈ D
φ : (withConstants.{u_2, u_3, u_1} L (↑(↑S : Set M) : Type u_1)).Formula (Fin 1)
hφ : Eq.{u_1 + 1} (α := Set (Fin 1 → M)) {x : Fin 1 → M | x 0 ∈ D} (setOf φ.Realize)
hφx : φ.Realize ![x]
ψ : (withConstants.{u_2, u_3, u_1} L (↑(↑S : Set M) : Type u_1)).Sentence := iExs (Fin 1) (relabel Sum.inr φ)
hψM : M ⊨ ψ
v' : Fin 1 → ↥S
hv' :
  BoundedFormula.Realize.{u_2, u_3, u_1, u_1} (L := L) (M := M) (α := (↑(↑S : Set M) : Type u_1) ⊕ Fin 1) (l := 0)
    ((BoundedFormula.constantsVarsEquiv :
        (a : L[[(↑(↑S : Set M) : Type u_1)]].BoundedFormula (Fin 1) 0) →
          L.BoundedFormula ((↑(↑S : Set M) : Type u_1) ⊕ Fin 1) 0)
      φ)
    ((⇑S.subtype : (a : ↥S) → M) ∘ Sum.elim (fun (a : (↑(↑S : Set M) : Type u_1)) ↦ (↑(L.con a) : ↥S)) v')
    (Function.comp (β := ↥S) (⇑S.subtype : (a : ↥S) → M) default)
i : (↑(↑S : Set M) : Type u_1) ⊕ Fin 1
h :
  ∀ (val : (↑(↑S : Set M) : Type u_1)),
    Sum.elim (fun (a : (↑(↑S : Set M) : Type u_1)) ↦ (↑(L.con a) : M)) (Subtype.val (p := fun (x : M) ↦ x ∈ S) ∘ v')
        (Sum.inl val) =
      ((⇑S.subtype : (a : ↥S) → M) ∘ Sum.elim (fun (a : (↑(↑S : Set M) : Type u_1)) ↦ (↑(L.con a) : ↥S)) v')
        (Sum.inl val)
h₁ :
  ∀ (val : Fin 1),
    Sum.elim (fun (a : (↑(↑S : Set M) : Type u_1)) ↦ (↑(L.con a) : M)) (Subtype.val (p := fun (x : M) ↦ x ∈ S) ∘ v')
        (Sum.inr val) =
      Function.comp (α := (↑(↑S : Set M) : Type u_1) ⊕ Fin 1) (⇑S.subtype : (a : ↥S) → M)
        (Sum.elim (fun (a : (↑(↑S : Set M) : Type u_1)) ↦ (↑(L.con a) : ↥S)) v') (Sum.inr val)
⊢ Sum.elim (fun (a : (↑(↑S : Set M) : Type u_1)) ↦ (↑(L.con a) : M)) (Subtype.val (p := fun (x : M) ↦ x ∈ S) ∘ v') i =
    ((⇑S.subtype : (a : ↥S) → M) ∘ Sum.elim (fun (a : (↑(↑S : Set M) : Type u_1)) ↦ (↑(L.con a) : ↥S)) v') i

Tactic:
cases i
-- Module: Mathlib.ModelTheory.ElementarySubstructures
Goal:
L : Language
M : Type u_1
inst : L.Structure M
S : L.ElementarySubstructure M
D : Set M
x : M
hx : x ∈ D
φ : (withConstants.{u_2, u_3, u_1} L (↑(↑S : Set M) : Type u_1)).Formula (Fin 1)
hφ : Eq.{u_1 + 1} (α := Set (Fin 1 → M)) {x : Fin 1 → M | x 0 ∈ D} (setOf φ.Realize)
hφx : φ.Realize ![x]
ψ : (withConstants.{u_2, u_3, u_1} L (↑(↑S : Set M) : Type u_1)).Sentence := iExs (Fin 1) (relabel Sum.inr φ)
hψM : M ⊨ ψ
v' : Fin 1 → ↥S
hv' :
  BoundedFormula.Realize.{u_2, u_3, u_1, u_1} (L := L) (M := M) (α := (↑(↑S : Set M) : Type u_1) ⊕ Fin 1) (l := 0)
    ((BoundedFormula.constantsVarsEquiv :
        (a : L[[(↑(↑S : Set M) : Type u_1)]].BoundedFormula (Fin 1) 0) →
          L.BoundedFormula ((↑(↑S : Set M) : Type u_1) ⊕ Fin 1) 0)
      φ)
    ((⇑S.subtype : (a : ↥S) → M) ∘ Sum.elim (fun (a : (↑(↑S : Set M) : Type u_1)) ↦ (↑(L.con a) : ↥S)) v')
    (Function.comp (β := ↥S) (⇑S.subtype : (a : ↥S) → M) default)
val : (↑(↑S : Set M) : Type u_1)
⊢ Sum.elim (fun (a : (↑(↑S : Set M) : Type u_1)) ↦ (↑(L.con a) : M)) (Subtype.val (p := fun (x : M) ↦ x ∈ S) ∘ v')
      (Sum.inl val) =
    ((⇑S.subtype : (a : ↥S) → M) ∘ Sum.elim (fun (a : (↑(↑S : Set M) : Type u_1)) ↦ (↑(L.con a) : ↥S)) v') (Sum.inl val)

Tactic:
rfl
-- Module: Mathlib.ModelTheory.ElementarySubstructures
Goal:
L : Language
M : Type u_1
inst : L.Structure M
S : L.ElementarySubstructure M
D : Set M
x : M
hx : x ∈ D
φ : (withConstants.{u_2, u_3, u_1} L (↑(↑S : Set M) : Type u_1)).Formula (Fin 1)
hφ : Eq.{u_1 + 1} (α := Set (Fin 1 → M)) {x : Fin 1 → M | x 0 ∈ D} (setOf φ.Realize)
hφx : φ.Realize ![x]
ψ : (withConstants.{u_2, u_3, u_1} L (↑(↑S : Set M) : Type u_1)).Sentence := iExs (Fin 1) (relabel Sum.inr φ)
hψM : M ⊨ ψ
v' : Fin 1 → ↥S
hv' :
  BoundedFormula.Realize.{u_2, u_3, u_1, u_1} (L := L) (M := M) (α := (↑(↑S : Set M) : Type u_1) ⊕ Fin 1) (l := 0)
    ((BoundedFormula.constantsVarsEquiv :
        (a : L[[(↑(↑S : Set M) : Type u_1)]].BoundedFormula (Fin 1) 0) →
          L.BoundedFormula ((↑(↑S : Set M) : Type u_1) ⊕ Fin 1) 0)
      φ)
    ((⇑S.subtype : (a : ↥S) → M) ∘ Sum.elim (fun (a : (↑(↑S : Set M) : Type u_1)) ↦ (↑(L.con a) : ↥S)) v')
    (Function.comp (β := ↥S) (⇑S.subtype : (a : ↥S) → M) default)
val : Fin 1
⊢ Sum.elim (fun (a : (↑(↑S : Set M) : Type u_1)) ↦ (↑(L.con a) : M)) (Subtype.val (p := fun (x : M) ↦ x ∈ S) ∘ v')
      (Sum.inr val) =
    Function.comp (α := (↑(↑S : Set M) : Type u_1) ⊕ Fin 1) (⇑S.subtype : (a : ↥S) → M)
      (Sum.elim (fun (a : (↑(↑S : Set M) : Type u_1)) ↦ (↑(L.con a) : ↥S)) v') (Sum.inr val)

Tactic:
rfl
-- Module: Mathlib.ModelTheory.ElementarySubstructures
Goal:
L : Language
M : Type u_1
inst : L.Structure M
S : L.ElementarySubstructure M
D : Set M
x : M
hx : x ∈ D
φ : (withConstants.{u_2, u_3, u_1} L (↑(↑S : Set M) : Type u_1)).Formula (Fin 1)
hφ : Eq.{u_1 + 1} (α := Set (Fin 1 → M)) {x : Fin 1 → M | x 0 ∈ D} (setOf φ.Realize)
hφx : φ.Realize ![x]
ψ : (withConstants.{u_2, u_3, u_1} L (↑(↑S : Set M) : Type u_1)).Sentence := iExs (Fin 1) (relabel Sum.inr φ)
hψM : M ⊨ ψ
v' : Fin 1 → ↥S
hv' : φ.Realize v'
⊢ φ.Realize (Subtype.val (p := fun (x : M) ↦ x ∈ S) ∘ v')

Tactic:
have hv'' : φ.Realize (Subtype.val ∘ v') := by
    simp only [Formula.Realize, ← BoundedFormula.realize_constantsVarsEquiv,
      ← S.subtype.map_boundedFormula] at hv'
    simp only [Formula.Realize, ← BoundedFormula.realize_constantsVarsEquiv]
    convert! hv' using 1
    funext i
    cases i <;> rfl
-- Module: Mathlib.ModelTheory.ElementarySubstructures
Goal:
L : Language
M : Type u_1
inst : L.Structure M
S : L.ElementarySubstructure M
D : Set M
x : M
hx : x ∈ D
φ : (withConstants.{u_2, u_3, u_1} L (↑(↑S : Set M) : Type u_1)).Formula (Fin 1)
hφ : Eq.{u_1 + 1} (α := Set (Fin 1 → M)) {x : Fin 1 → M | x 0 ∈ D} (setOf φ.Realize)
hφx : φ.Realize ![x]
ψ : (withConstants.{u_2, u_3, u_1} L (↑(↑S : Set M) : Type u_1)).Sentence := iExs (Fin 1) (relabel Sum.inr φ)
hψM : M ⊨ ψ
v' : Fin 1 → ↥S
hv' : φ.Realize v'
hv'' : φ.Realize (Subtype.val (p := fun (x : M) ↦ x ∈ S) ∘ v')
change : Membership.mem (γ := Set (Fin 1 → M)) {x : Fin 1 → M | x 0 ∈ D} (Subtype.val (p := fun (x : M) ↦ x ∈ S) ∘ v')
⊢ (↑(v' 0) : M) ∈ D

Tactic:
change (Subtype.val ∘ v') ∈ {x | x 0 ∈ D}

Premises used: Function.comp, Subtype.val
-- Module: Mathlib.ModelTheory.ElementarySubstructures
Goal:
L : Language
M : Type u_1
inst : L.Structure M
S : L.ElementarySubstructure M
D : Set M
x : M
hx : x ∈ D
φ : (withConstants.{u_2, u_3, u_1} L (↑(↑S : Set M) : Type u_1)).Formula (Fin 1)
hφ : Eq.{u_1 + 1} (α := Set (Fin 1 → M)) {x : Fin 1 → M | x 0 ∈ D} (setOf φ.Realize)
hφx : φ.Realize ![x]
ψ : (withConstants.{u_2, u_3, u_1} L (↑(↑S : Set M) : Type u_1)).Sentence := iExs (Fin 1) (relabel Sum.inr φ)
hψM : M ⊨ ψ
v' : Fin 1 → ↥S
hv' : φ.Realize v'
hv'' : φ.Realize (Subtype.val (p := fun (x : M) ↦ x ∈ S) ∘ v')
⊢ Membership.mem (γ := Set (Fin 1 → M)) {x : Fin 1 → M | x 0 ∈ D} (Subtype.val (p := fun (x : M) ↦ x ∈ S) ∘ v')

Tactic:
simpa [hφ] using hv''
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
h :
  ∀ (t : L.Term α) (l : List (Sum.{u', u} α ((i : ℕ) × L.Functions i))),
    listDecode (t.listEncode ++ l) = t :: listDecode l
⊢ Eq (α := List (L.Term α)) (listDecode (flatMap listEncode [])) []

Tactic:
rfl
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
h :
  ∀ (t : L.Term α) (l : List (Sum.{u', u} α ((i : ℕ) × L.Functions i))),
    listDecode (t.listEncode ++ l) = t :: listDecode l
t : L.Term α
l : List (L.Term α)
lih : listDecode (flatMap listEncode l) = l
cons : listDecode (t.listEncode ++ flatMap listEncode l) = t :: l
cons₁ : t :: listDecode (flatMap listEncode l) = t :: l
cons₂ cons₃ : t :: l = t :: l
⊢ listDecode (flatMap listEncode (t :: l)) = t :: l

Tactic:
rw [flatMap_cons, h t (l.flatMap listEncode), lih]

Premises used: FirstOrder.Language.Term.listEncode, List.flatMap_cons, List.flatMap
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
l : List (L.Term α)
h :
  ∀ (t : L.Term α) (l : List (Sum.{u', u} α ((i : ℕ) × L.Functions i))),
    listDecode (t.listEncode ++ l) = t :: listDecode l
nil : Eq (α := List (L.Term α)) (listDecode (flatMap listEncode [])) []
cons :
  ∀ (t : L.Term α) (l : List (L.Term α)) (lih : listDecode (flatMap listEncode l) = l),
    listDecode (flatMap listEncode (t :: l)) = t :: l
⊢ listDecode (flatMap listEncode l) = l

Tactic:
induction l with
    | nil => rfl
    | cons t l lih => rw [flatMap_cons, h t (l.flatMap listEncode), lih]

Premises used: List.flatMap_cons, List.nil
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
l : List (L.Term α)
suffices :
  ∀ (t : L.Term α) (l : List (Sum.{u', u} α ((i : ℕ) × L.Functions i))),
    listDecode (t.listEncode ++ l) = t :: listDecode l
⊢ listDecode (flatMap listEncode l) = l

Tactic:
suffices h : ∀ (t : L.Term α) (l : List (α ⊕ (Σ i, L.Functions i))),
      listDecode (t.listEncode ++ l) = t::listDecode l by
    induction l with
    | nil => rfl
    | cons t l lih => rw [flatMap_cons, h t (l.flatMap listEncode), lih]
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
l_1 : List (L.Term α)
a : α
l : List (Sum.{u', u} α ((i : ℕ) × L.Functions i))
var : listDecode ([Sum.inl a] ++ l) = Language.var a :: listDecode l
var₁ : listDecode (Sum.inl a :: l) = Language.var a :: listDecode l
var₂ var₃ : Language.var a :: listDecode l = Language.var a :: listDecode l
⊢ listDecode (listEncode (Language.var a) ++ l) = Language.var a :: listDecode l

Tactic:
rw [listEncode, singleton_append, listDecode]

Premises used: FirstOrder.Language.Term.listEncode, List.singleton_append, FirstOrder.Language.Term.listDecode
-- 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))
⊢ listDecode (flatMap (fun (i : Fin n) ↦ (ts i).listEncode) [] ++ l) = List.map ts [] ++ listDecode l

Tactic:
rfl
-- 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))
i : Fin n
l' : List (Fin n)
l'ih : listDecode (flatMap (fun (i : Fin n) ↦ (ts i).listEncode) l' ++ l) = List.map ts l' ++ listDecode l
cons :
  listDecode ((ts i).listEncode ++ flatMap (fun (i : Fin n) ↦ (ts i).listEncode) l' ++ l) =
    List.map ts (i :: l') ++ listDecode l
cons₁ :
  listDecode ((ts i).listEncode ++ (flatMap (fun (i : Fin n) ↦ (ts i).listEncode) l' ++ l)) =
    List.map ts (i :: l') ++ listDecode l
cons₂ :
  ts i :: listDecode (flatMap (fun (i : Fin n) ↦ (ts i).listEncode) l' ++ l) = List.map ts (i :: l') ++ listDecode l
cons₃ :
  ts i :: listDecode (flatMap (fun (i : Fin n) ↦ (ts i).listEncode) l' ++ l) = ts i :: List.map ts l' ++ listDecode l
cons₄ : ts i :: (List.map ts l' ++ listDecode l) = ts i :: List.map ts l' ++ listDecode l
cons₅ cons₆ : ts i :: (List.map ts l' ++ listDecode l) = ts i :: (List.map ts l' ++ listDecode l)
⊢ listDecode (flatMap (fun (i : Fin n) ↦ (ts i).listEncode) (i :: l') ++ l) = List.map ts (i :: l') ++ listDecode l

Tactic:
rw [flatMap_cons, List.append_assoc, ih, map_cons, l'ih, cons_append]

Premises used: List.append_assoc, List.map_cons, List.flatMap_cons, List.cons_append
-- 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))
induction :
  ∀ (x : List (Fin n)),
    listDecode (flatMap (fun (i : Fin n) ↦ (ts i).listEncode) x ++ l) = List.map ts x ++ listDecode l
⊢ listDecode (flatMap (fun (i : Fin n) ↦ (ts i).listEncode) (finRange n) ++ l) =
    List.map ts (finRange n) ++ listDecode l

Tactic:
induction finRange n with
      | nil => rfl
      | cons i l' l'ih => rw [flatMap_cons, List.append_assoc, ih, map_cons, l'ih, cons_append]

Premises used: List.append_assoc, List.map_cons, List.flatMap_cons, List.finRange, List.cons_append, List.nil
-- 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))
⊢ listDecode (flatMap (fun (i : Fin n) ↦ (ts i).listEncode) (finRange n) ++ l) =
    List.map ts (finRange n) ++ listDecode l

Tactic:
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]
-- 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
func :
  (fun (i : Fin n) ↦
        getElem (valid := fun (as : List (L.Term α)) (i : ℕ) ↦ i < as.length) (List.map ts (finRange n) ++ listDecode l)
          (↑i : ℕ) ⋯) =
      ts ∧
    drop n (List.map ts (finRange n) ++ listDecode l) = listDecode l
⊢ (if h : n ≤ (listDecode (flatMap (fun (i : Fin n) ↦ (ts i).listEncode) (finRange n) ++ l)).length then
      (Language.func f fun (i : Fin n) ↦
          getElem (valid := fun (xs : List (L.Term α)) (i : Fin n) ↦ (↑i : ℕ) < xs.length)
            (listDecode (flatMap (fun (i : Fin n) ↦ (ts i).listEncode) (finRange n) ++ l)) i ⋯) ::
        drop n (listDecode (flatMap (fun (i : Fin n) ↦ (ts i).listEncode) (finRange n) ++ l))
    else []) =
    Language.func f ts :: listDecode l

Tactic:
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]

Premises used: zero_le, le_add_iff_nonneg_right, heq_eq_eq, reduceDIte, List.length_append, List.cons.injEq, FirstOrder.Language.Term.func.injEq, List.length_finRange, Fin.getElem_fin, List.length_map, true_and
-- 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
⊢ (fun (i : Fin n) ↦
        getElem (valid := fun (as : List (L.Term α)) (i : ℕ) ↦ i < as.length) (List.map ts (finRange n) ++ listDecode l)
          (↑i : ℕ) ⋯) =
      ts ∧
    drop n (List.map ts (finRange n) ++ listDecode l) = listDecode l

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

Premises used: funext, And.intro
-- 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
func :
  ∀ (i : Fin n),
    getElem (valid := fun (as : List (L.Term α)) (i : ℕ) ↦ i < as.length) (List.map ts (finRange n) ++ listDecode l)
        (↑i : ℕ) ⋯ =
      ts i
func₁ : drop n (List.map ts (finRange n) ++ listDecode l) = listDecode l
⊢ (fun (i : Fin n) ↦
        getElem (valid := fun (as : List (L.Term α)) (i : ℕ) ↦ i < as.length) (List.map ts (finRange n) ++ listDecode l)
          (↑i : ℕ) ⋯) =
      ts ∧
    drop n (List.map ts (finRange n) ++ listDecode l) = listDecode l

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