awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
htv :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
        (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ x) a) →
      ∃ (b : M),
        BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
          (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ x) ((f : (a : M) → N) b))
n : ℕ
φ : L.BoundedFormula Empty n
n_1 : ℕ
f₁ f₂ : L.BoundedFormula Empty n_1
ih1 :
  ∀ (xs : Fin n_1 → M),
    BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) f₁
        (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N) default) ((⇑f : (a : M) → N) ∘ xs) ↔
      f₁.Realize default xs
ih2 :
  ∀ (xs : Fin n_1 → M),
    BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) f₂
        (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N) default) ((⇑f : (a : M) → N) ∘ xs) ↔
      f₂.Realize default xs
refine_4 :
  ∀ (xs : Fin n_1 → M),
    BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) (f₁ ⟹ f₂)
        (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N) default) ((⇑f : (a : M) → N) ∘ xs) ↔
      (f₁ ⟹ f₂).Realize default xs
⊢ ∀ (xs : Fin n_1 → M),
    BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) (f₁ ⟹ f₂)
        (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N) default) ((⇑f : (a : M) → N) ∘ xs) ↔
      (f₁ ⟹ f₂).Realize default xs

Tactic:
_
-- 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
htv :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
        (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ x) a) →
      ∃ (b : M),
        BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
          (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ x) ((f : (a : M) → N) b))
n : ℕ
φ : L.BoundedFormula Empty n
n_1 : ℕ
f₁ f₂ : L.BoundedFormula Empty n_1
ih1 :
  ∀ (xs : Fin n_1 → M),
    BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) f₁
        (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N) default) ((⇑f : (a : M) → N) ∘ xs) ↔
      f₁.Realize default xs
ih2 :
  ∀ (xs : Fin n_1 → M),
    BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) f₂
        (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N) default) ((⇑f : (a : M) → N) ∘ xs) ↔
      f₂.Realize default xs
xs : Fin n_1 → M
⊢ BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) (f₁ ⟹ f₂)
      (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N) default) ((⇑f : (a : M) → N) ∘ xs) ↔
    (f₁ ⟹ f₂).Realize default xs

Tactic:
simp [ih1, ih2]
-- 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
htv :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
        (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ x) a) →
      ∃ (b : M),
        BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
          (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ x) ((f : (a : M) → N) b))
n_1 : ℕ
φ_1 : L.BoundedFormula Empty n_1
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
ih :
  ∀ (xs : Fin (n + 1) → M),
    BoundedFormula.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) ((⇑f : (a : M) → N) ∘ xs) ↔
      φ.Realize default xs
xs : Fin n → M
refine_5 :
  (∀ (a : N),
      BoundedFormula.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)
        (Fin.snoc (α := fun (a : Fin n.succ) ↦ N) ((⇑f : (a : M) → N) ∘ xs) a)) ↔
    ∀ (a : M),
      BoundedFormula.Realize.{u_5, u_6, u_1, 0} (M := M) φ default (Fin.snoc (α := fun (a : Fin n.succ) ↦ M) xs a)
⊢ BoundedFormula.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) ((⇑f : (a : M) → N) ∘ xs) ↔
    (∀' φ).Realize default xs

Tactic:
simp only [BoundedFormula.realize_all]

Premises used: FirstOrder.Language.BoundedFormula.realize_all
-- 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
htv :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
        (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ x) a) →
      ∃ (b : M),
        BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
          (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ x) ((f : (a : M) → N) b))
n_1 : ℕ
φ_1 : L.BoundedFormula Empty n_1
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
ih :
  ∀ (xs : Fin (n + 1) → M),
    BoundedFormula.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) ((⇑f : (a : M) → N) ∘ xs) ↔
      φ.Realize default xs
xs : Fin n → M
⊢ (∀ (a : N),
      BoundedFormula.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)
        (Fin.snoc (α := fun (a : Fin n.succ) ↦ N) ((⇑f : (a : M) → N) ∘ xs) a)) ↔
    ∀ (a : M),
      BoundedFormula.Realize.{u_5, u_6, u_1, 0} (M := M) φ default (Fin.snoc (α := fun (a : Fin n.succ) ↦ M) xs a)

Tactic:
⟨fun h a => ?_, ?_⟩

Premises used: Iff.intro
-- 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
htv :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
        (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ x) a) →
      ∃ (b : M),
        BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
          (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ x) ((f : (a : M) → N) b))
n_1 : ℕ
φ_1 : L.BoundedFormula Empty n_1
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
ih :
  ∀ (xs : Fin (n + 1) → M),
    BoundedFormula.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) ((⇑f : (a : M) → N) ∘ xs) ↔
      φ.Realize default xs
xs : Fin n → M
refine_5 :
  ∀
    (h :
      ∀ (a : N),
        BoundedFormula.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)
          (Fin.snoc (α := fun (a : Fin n.succ) ↦ N) ((⇑f : (a : M) → N) ∘ xs) a))
    (a : M),
    BoundedFormula.Realize.{u_5, u_6, u_1, 0} (M := M) φ default (Fin.snoc (α := fun (a : Fin n.succ) ↦ M) xs a)
refine_5₁ :
  (∀ (a : M),
      BoundedFormula.Realize.{u_5, u_6, u_1, 0} (M := M) φ default (Fin.snoc (α := fun (a : Fin n.succ) ↦ M) xs a)) →
    ∀ (a : N),
      BoundedFormula.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)
        (Fin.snoc (α := fun (a : Fin n.succ) ↦ N) ((⇑f : (a : M) → N) ∘ xs) a)
⊢ (∀ (a : N),
      BoundedFormula.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)
        (Fin.snoc (α := fun (a : Fin n.succ) ↦ N) ((⇑f : (a : M) → N) ∘ xs) a)) ↔
    ∀ (a : M),
      BoundedFormula.Realize.{u_5, u_6, u_1, 0} (M := M) φ default (Fin.snoc (α := fun (a : Fin n.succ) ↦ M) xs a)

Tactic:
refine ⟨fun h a => ?_, ?_⟩
-- 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
htv :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
        (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ x) a) →
      ∃ (b : M),
        BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
          (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ x) ((f : (a : M) → N) b))
n_1 : ℕ
φ_1 : L.BoundedFormula Empty n_1
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
ih :
  ∀ (xs : Fin (n + 1) → M),
    BoundedFormula.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) ((⇑f : (a : M) → N) ∘ xs) ↔
      φ.Realize default xs
xs : Fin n → M
h :
  ∀ (a : N),
    BoundedFormula.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)
      (Fin.snoc (α := fun (a : Fin n.succ) ↦ N) ((⇑f : (a : M) → N) ∘ xs) a)
a : M
refine_5 :
  BoundedFormula.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)
    (Fin.snoc (α := fun (i : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ xs) ((f : (a : M) → N) a))
⊢ BoundedFormula.Realize.{u_5, u_6, u_1, 0} (M := M) φ default (Fin.snoc (α := fun (a : Fin n.succ) ↦ M) xs a)

Tactic:
rw [← ih, Fin.comp_snoc]

Premises used: Fin.comp_snoc
-- 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
htv :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
        (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ x) a) →
      ∃ (b : M),
        BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
          (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ x) ((f : (a : M) → N) b))
n_1 : ℕ
φ_1 : L.BoundedFormula Empty n_1
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
ih :
  ∀ (xs : Fin (n + 1) → M),
    BoundedFormula.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) ((⇑f : (a : M) → N) ∘ xs) ↔
      φ.Realize default xs
xs : Fin n → M
h :
  ∀ (a : N),
    BoundedFormula.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)
      (Fin.snoc (α := fun (a : Fin n.succ) ↦ N) ((⇑f : (a : M) → N) ∘ xs) a)
a : M
⊢ BoundedFormula.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)
    (Fin.snoc (α := fun (i : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ xs) ((f : (a : M) → N) a))

Tactic:
h (f a)

Premises used: 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
htv :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
        (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ x) a) →
      ∃ (b : M),
        BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
          (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ x) ((f : (a : M) → N) b))
n_1 : ℕ
φ_1 : L.BoundedFormula Empty n_1
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
ih :
  ∀ (xs : Fin (n + 1) → M),
    BoundedFormula.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) ((⇑f : (a : M) → N) ∘ xs) ↔
      φ.Realize default xs
xs : Fin n → M
h :
  ∀ (a : N),
    BoundedFormula.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)
      (Fin.snoc (α := fun (a : Fin n.succ) ↦ N) ((⇑f : (a : M) → N) ∘ xs) a)
a : M
⊢ BoundedFormula.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)
    (Fin.snoc (α := fun (i : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ xs) ((f : (a : M) → N) a))

Tactic:
exact h (f a)

Premises used: 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
htv :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
        (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ x) a) →
      ∃ (b : M),
        BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
          (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ x) ((f : (a : M) → N) b))
n_1 : ℕ
φ_1 : L.BoundedFormula Empty n_1
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
ih :
  ∀ (xs : Fin (n + 1) → M),
    BoundedFormula.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) ((⇑f : (a : M) → N) ∘ xs) ↔
      φ.Realize default xs
xs : Fin n → M
refine_5 :
  (∃ (a : N),
      ¬BoundedFormula.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)
          (Fin.snoc (α := fun (a : Fin n.succ) ↦ N) ((⇑f : (a : M) → N) ∘ xs) a)) →
    ∃ (a : M),
      ¬BoundedFormula.Realize.{u_5, u_6, u_1, 0} (M := M) φ default (Fin.snoc (α := fun (a : Fin n.succ) ↦ M) xs a)
⊢ (∀ (a : M),
      BoundedFormula.Realize.{u_5, u_6, u_1, 0} (M := M) φ default (Fin.snoc (α := fun (a : Fin n.succ) ↦ M) xs a)) →
    ∀ (a : N),
      BoundedFormula.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)
        (Fin.snoc (α := fun (a : Fin n.succ) ↦ N) ((⇑f : (a : M) → N) ∘ xs) a)

Tactic:
contrapose!
-- 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
htv :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
        (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ x) a) →
      ∃ (b : M),
        BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
          (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ x) ((f : (a : M) → N) b))
n_1 : ℕ
φ_1 : L.BoundedFormula Empty n_1
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
ih :
  ∀ (xs : Fin (n + 1) → M),
    BoundedFormula.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) ((⇑f : (a : M) → N) ∘ xs) ↔
      φ.Realize default xs
xs : Fin n → M
a : N
ha :
  ¬BoundedFormula.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)
      (Fin.snoc (α := fun (a : Fin n.succ) ↦ N) ((⇑f : (a : M) → N) ∘ xs) a)
rw :
  ¬BoundedFormula.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)
      (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ xs) a)
⊢ BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) (∼φ) default
    (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ xs) a)

Tactic:
rw [BoundedFormula.realize_not, ← Unique.eq_default (f ∘ default)]

Premises used: Inhabited.default, Function.comp, FirstOrder.Language.BoundedFormula.realize_not, Unique.eq_default, 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
htv :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
        (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ x) a) →
      ∃ (b : M),
        BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
          (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ x) ((f : (a : M) → N) b))
n_1 : ℕ
φ_1 : L.BoundedFormula Empty n_1
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
ih :
  ∀ (xs : Fin (n + 1) → M),
    BoundedFormula.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) ((⇑f : (a : M) → N) ∘ xs) ↔
      φ.Realize default xs
xs : Fin n → M
a : N
ha :
  ¬BoundedFormula.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)
      (Fin.snoc (α := fun (a : Fin n.succ) ↦ N) ((⇑f : (a : M) → N) ∘ xs) a)
⊢ ¬BoundedFormula.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)
      (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ xs) a)

Tactic:
ha
-- 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
htv :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
        (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ x) a) →
      ∃ (b : M),
        BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
          (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ x) ((f : (a : M) → N) b))
n_1 : ℕ
φ_1 : L.BoundedFormula Empty n_1
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
ih :
  ∀ (xs : Fin (n + 1) → M),
    BoundedFormula.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) ((⇑f : (a : M) → N) ∘ xs) ↔
      φ.Realize default xs
xs : Fin n → M
a : N
ha :
  ¬BoundedFormula.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)
      (Fin.snoc (α := fun (a : Fin n.succ) ↦ N) ((⇑f : (a : M) → N) ∘ xs) a)
⊢ ¬BoundedFormula.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)
      (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ xs) a)

Tactic:
exact ha
-- 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
htv :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
        (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ x) a) →
      ∃ (b : M),
        BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
          (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ x) ((f : (a : M) → N) b))
n_1 : ℕ
φ_1 : L.BoundedFormula Empty n_1
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
ih :
  ∀ (xs : Fin (n + 1) → M),
    BoundedFormula.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) ((⇑f : (a : M) → N) ∘ xs) ↔
      φ.Realize default xs
xs : Fin n → M
a : N
ha :
  ¬BoundedFormula.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)
      (Fin.snoc (α := fun (a : Fin n.succ) ↦ N) ((⇑f : (a : M) → N) ∘ xs) a)
refine_5 :
  ∀ (b : M)
    (hb :
      BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) (∼φ) default
        (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ xs) ((f : (a : M) → N) b))),
    ∃ (a : M),
      ¬BoundedFormula.Realize.{u_5, u_6, u_1, 0} (M := M) φ default (Fin.snoc (α := fun (a : Fin n.succ) ↦ M) xs a)
⊢ ∃ (a : M),
    ¬BoundedFormula.Realize.{u_5, u_6, u_1, 0} (M := M) φ default (Fin.snoc (α := fun (a : Fin n.succ) ↦ M) xs a)

Tactic:
obtain ⟨b, hb⟩ := htv n φ.not xs a (by
          rw [BoundedFormula.realize_not, ← Unique.eq_default (f ∘ default)]
          exact ha)

Premises used: FirstOrder.Language.BoundedFormula.not
-- 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
htv :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
        (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ x) a) →
      ∃ (b : M),
        BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
          (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ x) ((f : (a : M) → N) b))
n_1 : ℕ
φ_1 : L.BoundedFormula Empty n_1
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
ih :
  ∀ (xs : Fin (n + 1) → M),
    BoundedFormula.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) ((⇑f : (a : M) → N) ∘ xs) ↔
      φ.Realize default xs
xs : Fin n → M
a : N
ha :
  ¬BoundedFormula.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)
      (Fin.snoc (α := fun (a : Fin n.succ) ↦ N) ((⇑f : (a : M) → N) ∘ xs) a)
b : M
hb :
  BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) (∼φ) default
    (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ xs) ((f : (a : M) → N) b))
⊢ ∃ (a : M),
    ¬BoundedFormula.Realize.{u_5, u_6, u_1, 0} (M := M) φ default (Fin.snoc (α := fun (a : Fin n.succ) ↦ M) xs a)

Tactic:
⟨b, fun h => hb (Eq.mp ?_ ((ih _).2 h))⟩

Premises used: Iff.mpr, Eq.mp, Fin.snoc, Exists.intro
-- 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
htv :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
        (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ x) a) →
      ∃ (b : M),
        BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
          (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ x) ((f : (a : M) → N) b))
n_1 : ℕ
φ_1 : L.BoundedFormula Empty n_1
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
ih :
  ∀ (xs : Fin (n + 1) → M),
    BoundedFormula.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) ((⇑f : (a : M) → N) ∘ xs) ↔
      φ.Realize default xs
xs : Fin n → M
a : N
ha :
  ¬BoundedFormula.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)
      (Fin.snoc (α := fun (a : Fin n.succ) ↦ N) ((⇑f : (a : M) → N) ∘ xs) a)
b : M
hb :
  BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) (∼φ) default
    (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ xs) ((f : (a : M) → N) b))
refine_5 :
  ∀ (h : BoundedFormula.Realize.{u_5, u_6, u_1, 0} (M := M) φ default (Fin.snoc (α := fun (a : Fin n.succ) ↦ M) xs b)),
    BoundedFormula.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)
        (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N)
          (Fin.snoc (α := fun (a : Fin n.succ) ↦ M) xs b)) =
      BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
        (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ xs) ((f : (a : M) → N) b))
⊢ ∃ (a : M),
    ¬BoundedFormula.Realize.{u_5, u_6, u_1, 0} (M := M) φ default (Fin.snoc (α := fun (a : Fin n.succ) ↦ M) xs a)

Tactic:
refine ⟨b, fun h => hb (Eq.mp ?_ ((ih _).2 h))⟩