awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.DirectLimit
Goal:
L : Language
ι : Type v
inst : Preorder ι
inst_1 : Nonempty ι
inst_2 : IsDirectedOrder ι
M : Type u_1
inst_3 : L.Structure M
S : OrderHom.{v, u_1} ι (L.Substructure M)
i : ι
x : ↥((S : (a : ι) → L.Substructure M) i : L.Substructure M)
⊢ Eq (α :=
    DirectLimit.{v, u_1, u_2, u_3} (L := L) (fun (i : ι) ↦ ↥((S : (a : ι) → L.Substructure M) i : L.Substructure M))
      fun (x x_1 : ι) (h : x ≤ x_1) ↦ Substructure.inclusion ⋯)
    ((Embedding.comp (Equiv.toEmbedding (Equiv.symm (Equiv_iSup S))) (Substructure.inclusion ⋯) :
          (a : ↥((S : (a : ι) → L.Substructure M) i)) →
            DirectLimit (fun (i : ι) ↦ ↥((S : (a : ι) → L.Substructure M) i)) fun (x x_1 : ι) (h : x ≤ x_1) ↦
              Substructure.inclusion ⋯)
        x :
      DirectLimit.{v, u_1, u_2, u_3} (L := L) (fun (i : ι) ↦ ↥((S : (a : ι) → L.Substructure M) i : L.Substructure M))
        fun (x x_1 : ι) (h : x ≤ x_1) ↦ Substructure.inclusion ⋯)
    (((of.{v, u_1, u_2, u_3} L ι (fun (x : ι) ↦ ↥((S : (a : ι) → L.Substructure M) x : L.Substructure M))
              (fun (x x_1 : ι) (h : x ≤ x_1) ↦ Substructure.inclusion ⋯) i :
            ↥((S : (a : ι) → L.Substructure M) i : L.Substructure M) ↪[L]
              DirectLimit.{v, u_1, u_2, u_3} (L := L)
                (fun (x : ι) ↦ ↥((S : (a : ι) → L.Substructure M) x : L.Substructure M)) fun (x x_1 : ι) (h : x ≤ x_1) ↦
                Substructure.inclusion ⋯) :
          (a : ↥((S : (a : ι) → L.Substructure M) i)) →
            DirectLimit (fun (i : ι) ↦ ↥((S : (a : ι) → L.Substructure M) i)) fun (x x_1 : ι) (h : x ≤ x_1) ↦
              Substructure.inclusion ⋯)
        x :
      DirectLimit.{v, u_1, u_2, u_3} (L := L) (fun (i : ι) ↦ ↥((S : (a : ι) → L.Substructure M) i : L.Substructure M))
        fun (x x_1 : ι) (h : x ≤ x_1) ↦ Substructure.inclusion ⋯)

Tactic:
exact Equiv_isup_symm_inclusion_apply _ x

Premises used: FirstOrder.Language.DirectLimit.Equiv_isup_symm_inclusion_apply
-- Module: Mathlib.ModelTheory.ElementaryMaps
Goal:
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst : L.Structure M
inst_1 : L.Structure N
inst_2 : L.Structure P
inst_3 : L.Structure Q
f g : M ↪ₑ[L] N
h : Eq (α := (a : M) → N) ((fun (f : M ↪ₑ[L] N) ↦ (↑f : M → N)) f) ((fun (f : M ↪ₑ[L] N) ↦ (↑f : M → N)) g)
mk :
  ∀ (toFun : M → N)
    (map_formula' : ∀ ⦃n : ℕ⦄ (φ : L.Formula (Fin n)) (x : Fin n → M), φ.Realize (toFun ∘ x) ↔ φ.Realize x)
    (h :
      Eq (α := (a : M) → N) ((fun (f : M ↪ₑ[L] N) ↦ (↑f : M → N)) { toFun := toFun, map_formula' := map_formula' })
        ((fun (f : M ↪ₑ[L] N) ↦ (↑f : M → N)) g)),
    { toFun := toFun, map_formula' := map_formula' : M ↪ₑ[L] N } = g
⊢ f = g

Tactic:
cases f
-- Module: Mathlib.ModelTheory.ElementaryMaps
Goal:
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst : L.Structure M
inst_1 : L.Structure N
inst_2 : L.Structure P
inst_3 : L.Structure Q
g : M ↪ₑ[L] N
toFun : M → N
map_formula' : ∀ ⦃n : ℕ⦄ (φ : L.Formula (Fin n)) (x : Fin n → M), φ.Realize (toFun ∘ x) ↔ φ.Realize x
h :
  Eq (α := (a : M) → N) ((fun (f : M ↪ₑ[L] N) ↦ (↑f : M → N)) { toFun := toFun, map_formula' := map_formula' })
    ((fun (f : M ↪ₑ[L] N) ↦ (↑f : M → N)) g)
mk :
  ∀ (toFun_1 : M → N)
    (map_formula'_1 : ∀ ⦃n : ℕ⦄ (φ : L.Formula (Fin n)) (x : Fin n → M), φ.Realize (toFun_1 ∘ x) ↔ φ.Realize x)
    (h :
      Eq (α := (a : M) → N) ((fun (f : M ↪ₑ[L] N) ↦ (↑f : M → N)) { toFun := toFun, map_formula' := map_formula' })
        ((fun (f : M ↪ₑ[L] N) ↦ (↑f : M → N)) { toFun := toFun_1, map_formula' := map_formula'_1 })),
    { toFun := toFun, map_formula' := map_formula' : M ↪ₑ[L] N } = { toFun := toFun_1, map_formula' := map_formula'_1 }
⊢ { toFun := toFun, map_formula' := map_formula' : M ↪ₑ[L] N } = g

Tactic:
cases g
-- Module: Mathlib.ModelTheory.ElementaryMaps
Goal:
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst : L.Structure M
inst_1 : L.Structure N
inst_2 : L.Structure P
inst_3 : L.Structure Q
toFun : M → N
map_formula' : ∀ ⦃n : ℕ⦄ (φ : L.Formula (Fin n)) (x : Fin n → M), φ.Realize (toFun ∘ x) ↔ φ.Realize x
toFun_1 : M → N
map_formula'_1 : ∀ ⦃n : ℕ⦄ (φ : L.Formula (Fin n)) (x : Fin n → M), φ.Realize (toFun_1 ∘ x) ↔ φ.Realize x
h :
  Eq (α := (a : M) → N) ((fun (f : M ↪ₑ[L] N) ↦ (↑f : M → N)) { toFun := toFun, map_formula' := map_formula' })
    ((fun (f : M ↪ₑ[L] N) ↦ (↑f : M → N)) { toFun := toFun_1, map_formula' := map_formula'_1 })
⊢ { toFun := toFun, map_formula' := map_formula' : M ↪ₑ[L] N } = { toFun := toFun_1, map_formula' := map_formula'_1 }

Tactic:
simpa only [ElementaryEmbedding.mk.injEq]

Premises used: FirstOrder.Language.ElementaryEmbedding.mk.injEq
-- Module: Mathlib.ModelTheory.ElementaryMaps
Goal:
L : Language
M : Type u_1
N : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
f : M ↪ₑ[L] N
α : Type u_5
n : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin n → M
rw :
  BoundedFormula.Realize.{u_6, u_7, u_2, u_5} (M := N) (α := (↑(↑φ.freeVarFinset : Set α) : Type u_5))
      (φ.restrictFreeVar id)
      (((⇑f : (a : M) → N) ∘ v) ∘ Subtype.val (p := fun (x : α) ↦ x ∈ (↑φ.freeVarFinset : Set α)))
      ((⇑f : (a : M) → N) ∘ xs) ↔
    φ.Realize v xs
⊢ BoundedFormula.Realize.{u_6, u_7, u_2, u_5} (M := N) φ ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs) ↔
    φ.Realize v xs

Tactic:
rw [← BoundedFormula.realize_restrictFreeVar' Set.Subset.rfl, Set.inclusion_eq_id]

Premises used: Set.inclusion_eq_id, FirstOrder.Language.BoundedFormula.realize_restrictFreeVar', Set.Subset.rfl
-- Module: Mathlib.ModelTheory.ElementaryMaps
Goal:
L : Language
M : Type u_1
N : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
f : M ↪ₑ[L] N
α : Type u_5
n : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin n → M
⊢ Formula.Realize (α := Fin (Fintype.card.{u_5} (↥φ.freeVarFinset ⊕ Fin n)))
      (Formula.relabel (α := ↥φ.freeVarFinset ⊕ Fin n)
        (⇑(Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n)) :
          (a : ↥φ.freeVarFinset ⊕ Fin n) → Fin (Fintype.card (↥φ.freeVarFinset ⊕ Fin n)))
        (BoundedFormula.toFormula (φ.restrictFreeVar id)))
      ((↑f : M → N) ∘
        Function.comp (β := ↥φ.freeVarFinset ⊕ Fin n)
          (Sum.elim (v ∘ Subtype.val (p := fun (x : α) ↦ x ∈ φ.freeVarFinset)) xs)
          (⇑(_root_.Equiv.symm (Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n))) :
            (a : Fin (Fintype.card (↥φ.freeVarFinset ⊕ Fin n))) → ↥φ.freeVarFinset ⊕ Fin n)) ↔
    Formula.Realize (α := Fin (Fintype.card.{u_5} (↥φ.freeVarFinset ⊕ Fin n)))
      (Formula.relabel (α := ↥φ.freeVarFinset ⊕ Fin n)
        (⇑(Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n)) :
          (a : ↥φ.freeVarFinset ⊕ Fin n) → Fin (Fintype.card (↥φ.freeVarFinset ⊕ Fin n)))
        (BoundedFormula.toFormula (φ.restrictFreeVar id)))
      (Function.comp (β := ↥φ.freeVarFinset ⊕ Fin n)
        (Sum.elim (v ∘ Subtype.val (p := fun (x : α) ↦ x ∈ φ.freeVarFinset)) xs)
        (⇑(_root_.Equiv.symm (Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n))) :
          (a : Fin (Fintype.card (↥φ.freeVarFinset ⊕ Fin n))) → ↥φ.freeVarFinset ⊕ Fin n))

Tactic:
have h :=
      f.map_formula' ((φ.restrictFreeVar id).toFormula.relabel (Fintype.equivFin _))
        (Sum.elim (v ∘ (↑)) xs ∘ (Fintype.equivFin _).symm)
-- Module: Mathlib.ModelTheory.ElementaryMaps
Goal:
L : Language
M : Type u_1
N : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
f : M ↪ₑ[L] N
α : Type u_5
n : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin n → M
h :
  BoundedFormula.Realize (α := ↥φ.freeVarFinset) (φ.restrictFreeVar id)
      (((↑f : M → N) ∘ v) ∘ Subtype.val (p := fun (x : α) ↦ x ∈ φ.freeVarFinset)) ((↑f : M → N) ∘ xs) ↔
    BoundedFormula.Realize (α := ↥φ.freeVarFinset) (φ.restrictFreeVar id)
      (Function.comp (β := ↥φ.freeVarFinset ⊕ Fin n)
        (Function.comp (β := Fin (Fintype.card.{u_5} (↥φ.freeVarFinset ⊕ Fin n)))
          (Function.comp (β := ↥φ.freeVarFinset ⊕ Fin n)
            (Sum.elim (v ∘ Subtype.val (p := fun (x : α) ↦ x ∈ φ.freeVarFinset)) xs)
            (⇑(_root_.Equiv.symm (Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n))) :
              (a : Fin (Fintype.card (↥φ.freeVarFinset ⊕ Fin n))) → ↥φ.freeVarFinset ⊕ Fin n))
          (⇑(Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n)) :
            (a : ↥φ.freeVarFinset ⊕ Fin n) → Fin (Fintype.card (↥φ.freeVarFinset ⊕ Fin n))))
        Sum.inl)
      (Function.comp.{1, u_5 + 1, u_1 + 1} (β := ↥φ.freeVarFinset ⊕ Fin n)
        (Function.comp (β := Fin (Fintype.card.{u_5} (↥φ.freeVarFinset ⊕ Fin n)))
          (Function.comp (β := ↥φ.freeVarFinset ⊕ Fin n)
            (Sum.elim (v ∘ Subtype.val (p := fun (x : α) ↦ x ∈ φ.freeVarFinset)) xs)
            (⇑(_root_.Equiv.symm (Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n))) :
              (a : Fin (Fintype.card (↥φ.freeVarFinset ⊕ Fin n))) → ↥φ.freeVarFinset ⊕ Fin n))
          (⇑(Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n)) :
            (a : ↥φ.freeVarFinset ⊕ Fin n) → Fin (Fintype.card (↥φ.freeVarFinset ⊕ Fin n))))
        Sum.inr)
⊢ BoundedFormula.Realize.{u_6, u_7, u_2, u_5} (M := N) (α := (↑(↑φ.freeVarFinset : Set α) : Type u_5))
      (φ.restrictFreeVar id)
      (((⇑f : (a : M) → N) ∘ v) ∘ Subtype.val (p := fun (x : α) ↦ x ∈ (↑φ.freeVarFinset : Set α)))
      ((⇑f : (a : M) → N) ∘ xs) ↔
    φ.Realize v xs

Tactic:
h.trans ?_

Premises used: Iff.trans
-- Module: Mathlib.ModelTheory.ElementaryMaps
Goal:
L : Language
M : Type u_1
N : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
f : M ↪ₑ[L] N
α : Type u_5
n : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin n → M
h :
  BoundedFormula.Realize (α := ↥φ.freeVarFinset) (φ.restrictFreeVar id)
      (((↑f : M → N) ∘ v) ∘ Subtype.val (p := fun (x : α) ↦ x ∈ φ.freeVarFinset)) ((↑f : M → N) ∘ xs) ↔
    BoundedFormula.Realize (α := ↥φ.freeVarFinset) (φ.restrictFreeVar id)
      (Function.comp (β := ↥φ.freeVarFinset ⊕ Fin n)
        (Function.comp (β := Fin (Fintype.card.{u_5} (↥φ.freeVarFinset ⊕ Fin n)))
          (Function.comp (β := ↥φ.freeVarFinset ⊕ Fin n)
            (Sum.elim (v ∘ Subtype.val (p := fun (x : α) ↦ x ∈ φ.freeVarFinset)) xs)
            (⇑(_root_.Equiv.symm (Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n))) :
              (a : Fin (Fintype.card (↥φ.freeVarFinset ⊕ Fin n))) → ↥φ.freeVarFinset ⊕ Fin n))
          (⇑(Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n)) :
            (a : ↥φ.freeVarFinset ⊕ Fin n) → Fin (Fintype.card (↥φ.freeVarFinset ⊕ Fin n))))
        Sum.inl)
      (Function.comp.{1, u_5 + 1, u_1 + 1} (β := ↥φ.freeVarFinset ⊕ Fin n)
        (Function.comp (β := Fin (Fintype.card.{u_5} (↥φ.freeVarFinset ⊕ Fin n)))
          (Function.comp (β := ↥φ.freeVarFinset ⊕ Fin n)
            (Sum.elim (v ∘ Subtype.val (p := fun (x : α) ↦ x ∈ φ.freeVarFinset)) xs)
            (⇑(_root_.Equiv.symm (Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n))) :
              (a : Fin (Fintype.card (↥φ.freeVarFinset ⊕ Fin n))) → ↥φ.freeVarFinset ⊕ Fin n))
          (⇑(Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n)) :
            (a : ↥φ.freeVarFinset ⊕ Fin n) → Fin (Fintype.card (↥φ.freeVarFinset ⊕ Fin n))))
        Sum.inr)
⊢ ∀ (a : ↥φ.freeVarFinset), (v ∘ Subtype.val (p := fun (x : α) ↦ x ∈ φ.freeVarFinset)) (id a) = v (↑a : α)

Tactic:
simp
-- Module: Mathlib.ModelTheory.ElementaryMaps
Goal:
L : Language
M : Type u_1
N : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
f : M ↪ₑ[L] N
α : Type u_5
φ : L.Formula α
x : α → M
rw : BoundedFormula.Realize.{u_6, u_7, u_2, u_5} (M := N) φ ((⇑f : (a : M) → N) ∘ x) default ↔ φ.Realize x
rw₁ :
  BoundedFormula.Realize.{u_6, u_7, u_2, u_5} (M := N) φ ((⇑f : (a : M) → N) ∘ x) default ↔
    BoundedFormula.Realize φ x default
rw₂ :
  BoundedFormula.Realize.{u_6, u_7, u_2, u_5} (M := N) φ ((⇑f : (a : M) → N) ∘ x) default ↔
    BoundedFormula.Realize.{u_6, u_7, u_2, u_5} (M := N) φ ((⇑f : (a : M) → N) ∘ x)
      (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N) default)
rw₃ rw₄ :
  BoundedFormula.Realize.{u_6, u_7, u_2, u_5} (M := N) φ ((⇑f : (a : M) → N) ∘ x) default ↔
    BoundedFormula.Realize.{u_6, u_7, u_2, u_5} (M := N) φ ((⇑f : (a : M) → N) ∘ x) default
⊢ Formula.Realize.{u_6, u_7, u_2, u_5} (M := N) φ ((⇑f : (a : M) → N) ∘ x) ↔ φ.Realize x

Tactic:
rw [Formula.Realize, Formula.Realize, ← f.map_boundedFormula, Unique.eq_default (f ∘ default)]

Premises used: Inhabited.default, Function.comp, FirstOrder.Language.ElementaryEmbedding.map_boundedFormula, Unique.eq_default, DFunLike.coe, FirstOrder.Language.Formula.Realize
-- Module: Mathlib.ModelTheory.ElementaryMaps
Goal:
L : Language
M : Type u_1
N : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
f : M ↪ₑ[L] N
φ : L.Sentence
rw : Formula.Realize.{u_5, u_6, u_1, 0} (M := M) φ default ↔ N ⊨ φ
rw₁ : Formula.Realize.{u_5, u_6, u_1, 0} (M := M) φ default ↔ Formula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
rw₂ :
  Formula.Realize.{u_5, u_6, u_2, 0} (M := N) φ
      (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N) default) ↔
    Formula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
rw₃ rw₄ : Formula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default ↔ Formula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
⊢ M ⊨ φ ↔ N ⊨ φ

Tactic:
rw [Sentence.Realize, Sentence.Realize, ← f.map_formula, Unique.eq_default (f ∘ default)]

Premises used: FirstOrder.Language.Sentence.Realize, Inhabited.default, Function.comp, Unique.eq_default, FirstOrder.Language.ElementaryEmbedding.map_formula, DFunLike.coe
-- Module: Mathlib.ModelTheory.ElementaryMaps
Goal:
L : Language
M : Type u_1
N : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
f : M ↪ₑ[L] N
T : L.Theory
⊢ M ⊨ T ↔ N ⊨ T

Tactic:
simp only [Theory.model_iff, f.map_sentence]

Premises used: FirstOrder.Language.ElementaryEmbedding.map_sentence, FirstOrder.Language.Theory.model_iff
-- Module: Mathlib.ModelTheory.ElementaryMaps
Goal:
L : Language
M : Type u_1
N : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
f : M ↪ₑ[L] N
⊢ M ≅[L] N

Tactic:
elementarilyEquivalent_iff.2 f.map_sentence

Premises used: Iff.mpr, FirstOrder.Language.ElementaryEmbedding.map_sentence, FirstOrder.Language.elementarilyEquivalent_iff
-- Module: Mathlib.ModelTheory.ElementaryMaps
Goal:
L : Language
M : Type u_1
N : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
φ : M ↪ₑ[L] N
x y : M
⊢ Eq.{u_2 + 1} (α := N) ((φ : (a : M) → N) x : N) ((φ : (a : M) → N) y : N) → x = y

Tactic:
(φ.map_formula ((var 0).equal (var 1)) fun i => if i = 0 then x else y).1

Premises used: FirstOrder.Language.Term.bdEqual, FirstOrder.Language.BoundedFormula.Realize, FirstOrder.Language.Term.equal, FirstOrder.Language.Term.var, Iff.mp, FirstOrder.Language.Term.realize, OfNat.ofNat, Eq, FirstOrder.Language.ElementaryEmbedding.map_formula, FirstOrder.Language.Formula.Realize, Sum.elim, ite
-- Module: Mathlib.ModelTheory.ElementaryMaps
Goal:
L : Language
M : Type u_1
N : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
φ : M ↪ₑ[L] N
x y : M
⊢ Eq.{u_2 + 1} (α := N) ((φ : (a : M) → N) x : N) ((φ : (a : M) → N) y : N) → x = y

Tactic:
exact (φ.map_formula ((var 0).equal (var 1)) fun i => if i = 0 then x else y).1

Premises used: FirstOrder.Language.Term.equal, FirstOrder.Language.Term.var, Iff.mp, OfNat.ofNat, Eq, FirstOrder.Language.ElementaryEmbedding.map_formula, ite
-- Module: Mathlib.ModelTheory.ElementaryMaps
Goal:
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst : L.Structure M
inst_1 : L.Structure N
inst_2 : L.Structure P
inst_3 : L.Structure Q
⊢ EmbeddingLike (M ↪ₑ[L] N) M N

Tactic:
{ show FunLike (M ↪ₑ[L] N) M N from inferInstance with injective' := injective }

Premises used: EmbeddingLike.mk, FirstOrder.Language.ElementaryEmbedding.injective, inferInstance
-- Module: Mathlib.ModelTheory.ElementaryMaps
Goal:
L : Language
M : Type u_1
N : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
φ : M ↪ₑ[L] N
n : ℕ
f : L.Functions n
x : Fin n → M
⊢ Formula.Realize.{u_5, u_6, u_2, 0} (M := N) (Formula.graph f)
      (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑φ : (a : M) → N)
        (Fin.cons (α := fun (a : Fin (n + 1)) ↦ M) (funMap f x) x)) ↔
    Formula.Realize.{u_5, u_6, u_1, 0} (M := M) (Formula.graph f)
      (Fin.cons (α := fun (a : Fin (n + 1)) ↦ M) (funMap f x) x)

Tactic:
have h := φ.map_formula (Formula.graph f) (Fin.cons (funMap f x) x)
-- Module: Mathlib.ModelTheory.ElementaryMaps
Goal:
L : Language
M : Type u_1
N : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
φ : M ↪ₑ[L] N
n : ℕ
f : L.Functions n
x : Fin n → M
h :
  Formula.Realize.{u_5, u_6, u_2, 0} (M := N) (Formula.graph f)
      (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑φ : (a : M) → N)
        (Fin.cons (α := fun (a : Fin (n + 1)) ↦ M) (funMap f x) x)) ↔
    Formula.Realize.{u_5, u_6, u_1, 0} (M := M) (Formula.graph f)
      (Fin.cons (α := fun (a : Fin (n + 1)) ↦ M) (funMap f x) x)
⊢ Eq.{u_2 + 1} (α := N) (funMap f ((⇑φ : (a : M) → N) ∘ x) : N) ((φ : (a : M) → N) (funMap f x) : N) ↔
    funMap f x = funMap f x

Tactic:
rw [Formula.realize_graph, Fin.comp_cons, Formula.realize_graph] at h

Premises used: FirstOrder.Language.Formula.realize_graph, Fin.comp_cons
-- Module: Mathlib.ModelTheory.ElementaryMaps
Goal:
L : Language
M : Type u_1
N : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
φ : M ↪ₑ[L] N
n : ℕ
f : L.Functions n
x : Fin n → M
h :
  Eq.{u_2 + 1} (α := N) (funMap f ((⇑φ : (a : M) → N) ∘ x) : N) ((φ : (a : M) → N) (funMap f x) : N) ↔
    funMap f x = funMap f x
rw : Eq.{u_2 + 1} (α := N) (funMap f ((⇑φ : (a : M) → N) ∘ x) : N) ((φ : (a : M) → N) (funMap f x) : N)
rw₁ rw₂ : funMap f x = funMap f x
⊢ Eq.{u_2 + 1} (α := N) ((φ : (a : M) → N) (funMap f x) : N) (funMap f ((⇑φ : (a : M) → N) ∘ x) : N)

Tactic:
rw [eq_comm, h]

Premises used: eq_comm
-- Module: Mathlib.ModelTheory.ElementaryMaps
Goal:
L : Language
M : Type u_1
N : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
φ : M ↪ₑ[L] N
n : ℕ
r : L.Relations n
x : Fin n → M
⊢ RelMap.{u_5, u_6, u_2} (M := N) r ((⇑φ : (a : M) → N) ∘ x) ↔ RelMap r x

Tactic:
haveI h := φ.map_formula (r.formula var) x
  h

Premises used: FirstOrder.Language.Relations.boundedFormula, FirstOrder.Language.BoundedFormula.Realize, FirstOrder.Language.Term.var, FirstOrder.Language.Term.realize, FirstOrder.Language.ElementaryEmbedding.map_formula, FirstOrder.Language.Relations.formula, FirstOrder.Language.Formula.Realize, Sum.elim
-- Module: Mathlib.ModelTheory.ElementaryMaps
Goal:
L : Language
M : Type u_1
N : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
φ : M ↪ₑ[L] N
c : L.Constants
⊢ Eq.{u_2 + 1} (α := N) ((φ : (a : M) → N) (↑c : M) : N) ((↑c : N) : N)

Tactic:
HomClass.map_constants φ c

Premises used: FirstOrder.Language.HomClass.map_constants
-- Module: Mathlib.ModelTheory.ElementaryMaps
Goal:
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst : L.Structure M
inst_1 : L.Structure N
inst_2 : L.Structure P
inst_3 : L.Structure Q
f_1 : M ↪ₑ[L] N
x_1 : ℕ
f : L.Functions x_1
x : Fin x_1 → M
⊢ Eq.{u_2 + 1} (α := N) ((f_1 : (a : M) → N) (funMap f x) : N) (funMap f ((⇑f_1 : (a : M) → N) ∘ x) : N)

Tactic:
simp
-- Module: Mathlib.ModelTheory.ElementaryMaps
Goal:
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst : L.Structure M
inst_1 : L.Structure N
inst_2 : L.Structure P
inst_3 : L.Structure Q
f : M ↪ₑ[L] N
x_1 : ℕ
R : L.Relations x_1
x : Fin x_1 → M
⊢ RelMap.{u_5, u_6, u_2} (M := N) R ((⇑f : (a : M) → N) ∘ x) ↔ RelMap R x

Tactic:
simp
-- Module: Mathlib.ModelTheory.ElementaryMaps
Goal:
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst : L.Structure M
inst_1 : L.Structure N
inst_2 : L.Structure P
inst_3 : L.Structure Q
f : M ↪ₑ[L] N
x_1 : ℕ
R : L.Relations x_1
x : Fin x_1 → M
⊢ RelMap R x → RelMap.{u_5, u_6, u_2} (M := N) R ((⇑f : (a : M) → N) ∘ x)

Tactic:
simp
-- Module: Mathlib.ModelTheory.ElementaryMaps
Goal:
L : Language
M : Type u_1
N : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
f : M ↪ₑ[L] N
⊢ f.toEmbedding.toHom = f.toHom

Tactic:
rfl

Premises used: FirstOrder.Language.ElementaryEmbedding.toHom, FirstOrder.Language.HomClass.toHom, rfl
-- Module: Mathlib.ModelTheory.ElementaryMaps
Goal:
L : Language
M : Type u_1
N : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
f : M ↪ₑ[L] N
⊢ Eq (α := (a : M) → N) (⇑f.toHom : (a : M) → N) (⇑f : (a : M) → N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.ModelTheory.ElementaryMaps
Goal:
L : Language
M : Type u_1
N : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
f : M ↪ₑ[L] N
⊢ Eq (α := (a : M) → N) (⇑f.toEmbedding : (a : M) → N) (⇑f : (a : M) → N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.ModelTheory.ElementaryMaps
Goal:
L : Language
M : Type u_1
N : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
⊢ Function.Injective (α := M ↪ₑ[L] N) (β := M → N) (DFunLike.coe (β := fun (x : M) ↦ N))

Tactic:
DFunLike.coe_injective

Premises used: DFunLike.coe_injective
-- Module: Mathlib.ModelTheory.ElementaryMaps
Goal:
L : Language
M : Type u_1
N : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
f g : M ↪ₑ[L] N
h : ∀ (x : M), Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N)
⊢ f = g

Tactic:
DFunLike.ext f g h

Premises used: DFunLike.ext
-- Module: Mathlib.ModelTheory.ElementaryMaps
Goal:
L : Language
M : Type u_1
inst : L.Structure M
x : M
⊢ (refl L M : (a : M) → M) x = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.ModelTheory.ElementaryMaps
Goal:
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst : L.Structure M
inst_1 : L.Structure N
inst_2 : L.Structure P
inst_3 : L.Structure Q
hnp : N ↪ₑ[L] P
hmn : M ↪ₑ[L] N
n : ℕ
φ : L.Formula (Fin n)
x : Fin n → M
⊢ Formula.Realize.{u_5, u_6, u_3, 0} (M := P) φ
      (Function.comp.{u_1 + 1, u_2 + 1, u_3 + 1} (β := N) (⇑hnp : (a : N) → P) (⇑hmn : (a : M) → N) ∘ x) ↔
    φ.Realize x

Tactic:
simp [Function.comp_assoc]

Premises used: Function.comp_assoc
-- Module: Mathlib.ModelTheory.ElementaryMaps
Goal:
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
inst : L.Structure M
inst_1 : L.Structure N
inst_2 : L.Structure P
g : N ↪ₑ[L] P
f : M ↪ₑ[L] N
x : M
⊢ Eq.{u_3 + 1} (α := P) ((g.comp f : (a : M) → P) x : P) ((g : (a : N) → P) ((f : (a : M) → N) x : N) : P)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.ModelTheory.ElementaryMaps
Goal:
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst : L.Structure M
inst_1 : L.Structure N
inst_2 : L.Structure P
inst_3 : L.Structure Q
f : M ↪ₑ[L] N
g : N ↪ₑ[L] P
h : P ↪ₑ[L] Q
⊢ (h.comp g).comp f = h.comp (g.comp f)

Tactic:
rfl

Premises used: FirstOrder.Language.ElementaryEmbedding.comp, rfl
-- Module: Mathlib.ModelTheory.ElementaryMaps
Goal:
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst : L.Structure M
inst_1 : L.Structure N
inst_2 : L.Structure P
inst_3 : L.Structure Q
f : M ↪ₑ[L] N
A : Set M
refine :
  ∀ ⦃n : ℕ⦄ (φ : (withConstants.{u_5, u_6, u_1} L (↑A : Type u_1)).Formula (Fin n)) (x : Fin n → M),
    φ.Realize (M := f.toEmbedding.withConstants A) ((⇑f : (a : M) → N) ∘ x) ↔ φ.Realize x
⊢ M ↪ₑ[withConstants.{u_5, u_6, u_1} L (↑A : Type u_1)] f.toEmbedding.withConstants A

Tactic:
refine ⟨f, ?_⟩
-- Module: Mathlib.ModelTheory.ElementaryMaps
Goal:
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst : L.Structure M
inst_1 : L.Structure N
inst_2 : L.Structure P
inst_3 : L.Structure Q
f : M ↪ₑ[L] N
A : Set M
n : ℕ
φ : (withConstants.{u_5, u_6, u_1} L (↑A : Type u_1)).Formula (Fin n)
x : Fin n → M
⊢ Eq (α := (↑A : Type u_1) ⊕ Fin n → f.toEmbedding.withConstants A)
    (Sum.elim (fun (a : (↑A : Type u_1)) ↦ (↑(L.con a) : f.toEmbedding.withConstants A)) ((⇑f : (a : M) → N) ∘ x))
    ((⇑f : (a : M) → N) ∘ Sum.elim (fun (a : (↑A : Type u_1)) ↦ (↑(L.con a) : M)) x)

Tactic:
have h :
    (Sum.elim (fun a ↦ ↑(L.con a)) (⇑f ∘ x) :
      ↑A ⊕ Fin n → f.toEmbedding.withConstants A) =
    f ∘ Sum.elim (fun a ↦ ↑(L.con a)) x :=
    (Sum.comp_elim _ _ _).symm