awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
P : {m : ℕ} → L.BoundedFormula α m → Prop
φ_1 : L.BoundedFormula α n
hqf : ∀ {m : ℕ} {ψ : L.BoundedFormula α m}, ψ.IsQF → P ψ
hall : ∀ {m : ℕ} {ψ : L.BoundedFormula α (m + 1)}, P ψ → P (∀' ψ)
hex : ∀ {m : ℕ} {φ : L.BoundedFormula α (m + 1)}, P φ → P (∃' φ)
hse : ∀ {m : ℕ} {φ₁ φ₂ : L.BoundedFormula α m}, φ₁ ⇔[∅] φ₂ → (P φ₁ ↔ P φ₂)
m : ℕ
φ : L.BoundedFormula α m
n_1 : ℕ
φ_2 : L.BoundedFormula α (n_1 + 1)
h : φ_2.IsPrenex
hφ : P φ_2
⊢ P (∀' φ_2)

Tactic:
exact hall hφ
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
P : {m : ℕ} → L.BoundedFormula α m → Prop
φ_1 : L.BoundedFormula α n
hqf : ∀ {m : ℕ} {ψ : L.BoundedFormula α m}, ψ.IsQF → P ψ
hall : ∀ {m : ℕ} {ψ : L.BoundedFormula α (m + 1)}, P ψ → P (∀' ψ)
hex : ∀ {m : ℕ} {φ : L.BoundedFormula α (m + 1)}, P φ → P (∃' φ)
hse : ∀ {m : ℕ} {φ₁ φ₂ : L.BoundedFormula α m}, φ₁ ⇔[∅] φ₂ → (P φ₁ ↔ P φ₂)
m : ℕ
φ : L.BoundedFormula α m
n_1 : ℕ
φ_2 : L.BoundedFormula α (n_1 + 1)
h : φ_2.IsPrenex
hφ : P φ_2
⊢ P (∃' φ_2)

Tactic:
hex hφ
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
P : {m : ℕ} → L.BoundedFormula α m → Prop
φ_1 : L.BoundedFormula α n
hqf : ∀ {m : ℕ} {ψ : L.BoundedFormula α m}, ψ.IsQF → P ψ
hall : ∀ {m : ℕ} {ψ : L.BoundedFormula α (m + 1)}, P ψ → P (∀' ψ)
hex : ∀ {m : ℕ} {φ : L.BoundedFormula α (m + 1)}, P φ → P (∃' φ)
hse : ∀ {m : ℕ} {φ₁ φ₂ : L.BoundedFormula α m}, φ₁ ⇔[∅] φ₂ → (P φ₁ ↔ P φ₂)
m : ℕ
φ : L.BoundedFormula α m
n_1 : ℕ
φ_2 : L.BoundedFormula α (n_1 + 1)
h : φ_2.IsPrenex
hφ : P φ_2
⊢ P (∃' φ_2)

Tactic:
exact hex hφ
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
P : {m : ℕ} → L.BoundedFormula α m → Prop
φ_1 : L.BoundedFormula α n
hqf : ∀ {m : ℕ} {ψ : L.BoundedFormula α m}, ψ.IsQF → P ψ
hall : ∀ {m : ℕ} {ψ : L.BoundedFormula α (m + 1)}, P ψ → P (∀' ψ)
hex : ∀ {m : ℕ} {φ : L.BoundedFormula α (m + 1)}, P φ → P (∃' φ)
hse : ∀ {m : ℕ} {φ₁ φ₂ : L.BoundedFormula α m}, φ₁ ⇔[∅] φ₂ → (P φ₁ ↔ P φ₂)
m : ℕ
φ : L.BoundedFormula α m
hφ : φ.IsPrenex
of_isQF : ∀ {n : ℕ} {φ : L.BoundedFormula α n} (hφ : φ.IsQF), P φ
all : ∀ {n : ℕ} {φ : L.BoundedFormula α (n + 1)}, φ.IsPrenex → ∀ (hφ : P φ), P (∀' φ)
ex : ∀ {n : ℕ} {φ : L.BoundedFormula α (n + 1)}, φ.IsPrenex → ∀ (hφ : P φ), P (∃' φ)
⊢ P φ

Tactic:
induction hφ with
  | of_isQF hφ => exact hqf hφ
  | all _ hφ => exact hall hφ
  | ex _ hφ => exact hex hφ

Premises used: FirstOrder.Language.BoundedFormula.all
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
P : {m : ℕ} → L.BoundedFormula α m → Prop
φ : L.BoundedFormula α n
hqf : ∀ {m : ℕ} {ψ : L.BoundedFormula α m}, ψ.IsQF → P ψ
hnot : ∀ {m : ℕ} {φ : L.BoundedFormula α m}, P φ → P ∼φ
hex : ∀ {m : ℕ} {φ : L.BoundedFormula α (m + 1)}, P φ → P (∃' φ)
hse : ∀ {m : ℕ} {φ₁ φ₂ : L.BoundedFormula α m}, φ₁ ⇔[∅] φ₂ → (P φ₁ ↔ P φ₂)
⊢ P φ

Tactic:
φ.induction_on_all_ex (fun {_ _} => hqf)
    (fun {_ φ} hφ => (hse φ.all_iff_not_ex_not).2 (hnot (hex (hnot hφ))))
    (fun {_ _} => hex) fun {_ _ _} => hse

Premises used: Iff.mpr, FirstOrder.Language.BoundedFormula.induction_on_all_ex, FirstOrder.Language.BoundedFormula.all_iff_not_ex_not
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α n
⊢ φ.IsQF → φ.IsUniversal

Tactic:
IsUniversal.of_isQF

Premises used: FirstOrder.Language.BoundedFormula.IsUniversal.of_isQF
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α n
h : φ.IsAtomic
⊢ φ.IsUniversal

Tactic:
h.isQF.isUniversal

Premises used: FirstOrder.Language.BoundedFormula.IsQF.isUniversal, FirstOrder.Language.BoundedFormula.IsAtomic.isQF
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α n
⊢ φ.IsQF → φ.IsExistential

Tactic:
IsExistential.of_isQF

Premises used: FirstOrder.Language.BoundedFormula.IsExistential.of_isQF
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α n
h : φ.IsAtomic
⊢ φ.IsExistential

Tactic:
h.isQF.isExistential

Premises used: FirstOrder.Language.BoundedFormula.IsQF.isExistential, FirstOrder.Language.BoundedFormula.IsAtomic.isQF
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
F : Type u_3
inst_2 : FunLike F M N
φ : L.BoundedFormula α n
inst_3 : L.HomClass F M N
f : F
hInj : Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
v : α → M
xs : Fin n → M
t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n)
⊢ (t₁ =' t₂).Realize v xs →
    Realize.{u, v, u_2, u'} (M := N) (t₁ =' t₂) ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs)

Tactic:
simp only [realize_bdEqual, ← Sum.comp_elim, HomClass.realize_term, hInj.eq_iff,
    imp_self]

Premises used: Function.Injective.eq_iff, FirstOrder.Language.HomClass.realize_term, imp_self, Sum.comp_elim, FirstOrder.Language.BoundedFormula.realize_bdEqual
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
F : Type u_3
inst_2 : FunLike F M N
φ : L.BoundedFormula α n
inst_3 : L.HomClass F M N
f : F
hInj : Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
v : α → M
xs : Fin n → M
l : ℕ
R : L.Relations l
ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n)
rel :
  (RelMap.{u, v, u_1} (M := M) R fun (i : Fin l) ↦ Term.realize (Sum.elim v xs) (ts i)) →
    RelMap.{u, v, u_2} (M := N) R fun (i : Fin l) ↦ (f : (a : M) → N) (Term.realize (Sum.elim v xs) (ts i))
⊢ (R.boundedFormula ts).Realize v xs →
    Realize.{u, v, u_2, u'} (M := N) (R.boundedFormula ts) ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs)

Tactic:
simp only [realize_rel, ← Sum.comp_elim, HomClass.realize_term]

Premises used: FirstOrder.Language.HomClass.realize_term, FirstOrder.Language.BoundedFormula.realize_rel, Sum.comp_elim
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
F : Type u_3
inst_2 : FunLike F M N
φ : L.BoundedFormula α n
inst_3 : L.HomClass F M N
f : F
hInj : Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
v : α → M
xs : Fin n → M
l : ℕ
R : L.Relations l
ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n)
⊢ (RelMap.{u, v, u_1} (M := M) R fun (i : Fin l) ↦ Term.realize (Sum.elim v xs) (ts i)) →
    RelMap.{u, v, u_2} (M := N) R fun (i : Fin l) ↦ (f : (a : M) → N) (Term.realize (Sum.elim v xs) (ts i))

Tactic:
HomClass.map_rel f R (fun i => Term.realize (Sum.elim v xs) (ts i))

Premises used: FirstOrder.Language.Term.realize, FirstOrder.Language.HomClass.map_rel, Sum.elim
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
F : Type u_3
inst_2 : FunLike F M N
φ : L.BoundedFormula α n
inst_3 : L.HomClass F M N
f : F
hInj : Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
v : α → M
xs : Fin n → M
l : ℕ
R : L.Relations l
ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n)
⊢ (RelMap.{u, v, u_1} (M := M) R fun (i : Fin l) ↦ Term.realize (Sum.elim v xs) (ts i)) →
    RelMap.{u, v, u_2} (M := N) R fun (i : Fin l) ↦ (f : (a : M) → N) (Term.realize (Sum.elim v xs) (ts i))

Tactic:
exact HomClass.map_rel f R (fun i => Term.realize (Sum.elim v xs) (ts i))

Premises used: FirstOrder.Language.Term.realize, FirstOrder.Language.HomClass.map_rel, Sum.elim
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
F : Type u_3
inst_2 : FunLike F M N
φ : L.BoundedFormula α n
hA : φ.IsAtomic
inst_3 : L.HomClass F M N
f : F
hInj : Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
v : α → M
xs : Fin n → M
equal :
  ∀ (t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n)),
    (t₁ =' t₂).Realize v xs →
      Realize.{u, v, u_2, u'} (M := N) (t₁ =' t₂) ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs)
rel :
  ∀ {l : ℕ} (R : L.Relations l) (ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n)),
    (R.boundedFormula ts).Realize v xs →
      Realize.{u, v, u_2, u'} (M := N) (R.boundedFormula ts) ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs)
⊢ φ.Realize v xs → Realize.{u, v, u_2, u'} (M := N) φ ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs)

Tactic:
induction hA with
  | equal t₁ t₂ => simp only [realize_bdEqual, ← Sum.comp_elim, HomClass.realize_term, hInj.eq_iff,
    imp_self]
  | rel R ts =>
    simp only [realize_rel, ← Sum.comp_elim, HomClass.realize_term]
    exact HomClass.map_rel f R (fun i => Term.realize (Sum.elim v xs) (ts i))

Premises used: Function.Injective.eq_iff, FirstOrder.Language.BoundedFormula.IsAtomic.equal, FirstOrder.Language.BoundedFormula.IsAtomic.rel, FirstOrder.Language.HomClass.realize_term, imp_self, FirstOrder.Language.BoundedFormula.realize_rel, Sum.comp_elim, FirstOrder.Language.BoundedFormula.realize_bdEqual
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
F : Type u_3
inst_2 : FunLike F M N
φ : L.BoundedFormula α n
hA : φ.IsAtomic
inst_3 : EmbeddingLike F M N
inst_4 : L.HomClass F M N
f : F
v : α → M
xs : Fin n → M
⊢ φ.Realize v xs → Realize.{u, v, u_2, u'} (M := N) φ ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs)

Tactic:
hA.realize_comp_of_injective (EmbeddingLike.injective f)

Premises used: EmbeddingLike.injective, FirstOrder.Language.BoundedFormula.IsAtomic.realize_comp_of_injective
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
F : Type u_3
inst_2 : FunLike F M N
inst_3 : EmbeddingLike F M N
inst_4 : L.StrongHomClass F M N
φ : L.BoundedFormula α n
f : F
v : α → M
xs : Fin n → M
⊢ Realize.{u, v, u_2, u'} (L := L) (M := N) BoundedFormula.falsum ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs) ↔
    Realize.{u, v, u_1, u'} (L := L) BoundedFormula.falsum v xs

Tactic:
rfl
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
F : Type u_3
inst_2 : FunLike F M N
inst_3 : EmbeddingLike F M N
inst_4 : L.StrongHomClass F M N
φ : L.BoundedFormula α n
f : F
v : α → M
xs : Fin n → M
φ_1 : L.BoundedFormula α n
t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n)
⊢ Realize.{u, v, u_2, u'} (M := N) (t₁ =' t₂) ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs) ↔
    (t₁ =' t₂).Realize v xs

Tactic:
simp only [realize_bdEqual, ← Sum.comp_elim, HomClass.realize_term,
        (EmbeddingLike.injective f).eq_iff]

Premises used: Function.Injective.eq_iff, FirstOrder.Language.HomClass.realize_term, EmbeddingLike.injective, Sum.comp_elim, FirstOrder.Language.BoundedFormula.realize_bdEqual
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
F : Type u_3
inst_2 : FunLike F M N
inst_3 : EmbeddingLike F M N
inst_4 : L.StrongHomClass F M N
φ : L.BoundedFormula α n
f : F
v : α → M
xs : Fin n → M
φ_1 : L.BoundedFormula α n
l : ℕ
R : L.Relations l
ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n)
of_isAtomic :
  (RelMap.{u, v, u_2} (M := N) R fun (i : Fin l) ↦ (f : (a : M) → N) (Term.realize (Sum.elim v xs) (ts i))) ↔
    RelMap.{u, v, u_1} (M := M) R fun (i : Fin l) ↦ Term.realize (Sum.elim v xs) (ts i)
⊢ Realize.{u, v, u_2, u'} (M := N) (R.boundedFormula ts) ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs) ↔
    (R.boundedFormula ts).Realize v xs

Tactic:
simp only [realize_rel, ← Sum.comp_elim, HomClass.realize_term]

Premises used: FirstOrder.Language.HomClass.realize_term, FirstOrder.Language.BoundedFormula.realize_rel, Sum.comp_elim
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
F : Type u_3
inst_2 : FunLike F M N
inst_3 : EmbeddingLike F M N
inst_4 : L.StrongHomClass F M N
φ : L.BoundedFormula α n
f : F
v : α → M
xs : Fin n → M
φ_1 : L.BoundedFormula α n
l : ℕ
R : L.Relations l
ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n)
⊢ (RelMap.{u, v, u_2} (M := N) R fun (i : Fin l) ↦ (f : (a : M) → N) (Term.realize (Sum.elim v xs) (ts i))) ↔
    RelMap.{u, v, u_1} (M := M) R fun (i : Fin l) ↦ Term.realize (Sum.elim v xs) (ts i)

Tactic:
StrongHomClass.map_rel f R (fun i => Term.realize (Sum.elim v xs) (ts i))

Premises used: FirstOrder.Language.StrongHomClass.map_rel, FirstOrder.Language.Term.realize, Sum.elim
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
F : Type u_3
inst_2 : FunLike F M N
inst_3 : EmbeddingLike F M N
inst_4 : L.StrongHomClass F M N
φ : L.BoundedFormula α n
f : F
v : α → M
xs : Fin n → M
φ_1 : L.BoundedFormula α n
l : ℕ
R : L.Relations l
ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n)
⊢ (RelMap.{u, v, u_2} (M := N) R fun (i : Fin l) ↦ (f : (a : M) → N) (Term.realize (Sum.elim v xs) (ts i))) ↔
    RelMap.{u, v, u_1} (M := M) R fun (i : Fin l) ↦ Term.realize (Sum.elim v xs) (ts i)

Tactic:
exact StrongHomClass.map_rel f R (fun i => Term.realize (Sum.elim v xs) (ts i))

Premises used: FirstOrder.Language.StrongHomClass.map_rel, FirstOrder.Language.Term.realize, Sum.elim
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
F : Type u_3
inst_2 : FunLike F M N
inst_3 : EmbeddingLike F M N
inst_4 : L.StrongHomClass F M N
φ : L.BoundedFormula α n
f : F
v : α → M
xs : Fin n → M
φ_1 : L.BoundedFormula α n
hA : φ_1.IsAtomic
of_isAtomic :
  ∀ (t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n)),
    Realize.{u, v, u_2, u'} (M := N) (t₁ =' t₂) ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs) ↔
      (t₁ =' t₂).Realize v xs
of_isAtomic₁ :
  ∀ {l : ℕ} (R : L.Relations l) (ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n)),
    Realize.{u, v, u_2, u'} (M := N) (R.boundedFormula ts) ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs) ↔
      (R.boundedFormula ts).Realize v xs
⊢ Realize.{u, v, u_2, u'} (M := N) φ_1 ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs) ↔ φ_1.Realize v xs

Tactic:
induction hA with
    | equal t₁ t₂ => simp only [realize_bdEqual, ← Sum.comp_elim, HomClass.realize_term,
        (EmbeddingLike.injective f).eq_iff]
    | rel R ts =>
      simp only [realize_rel, ← Sum.comp_elim, HomClass.realize_term]
      exact StrongHomClass.map_rel f R (fun i => Term.realize (Sum.elim v xs) (ts i))

Premises used: Function.Injective.eq_iff, FirstOrder.Language.BoundedFormula.equal, FirstOrder.Language.HomClass.realize_term, EmbeddingLike.injective, FirstOrder.Language.BoundedFormula.realize_rel, Sum.comp_elim, FirstOrder.Language.BoundedFormula.realize_bdEqual, FirstOrder.Language.BoundedFormula.rel
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
F : Type u_3
inst_2 : FunLike F M N
inst_3 : EmbeddingLike F M N
inst_4 : L.StrongHomClass F M N
φ : L.BoundedFormula α n
f : F
v : α → M
xs : Fin n → M
φ₁ φ₂ : L.BoundedFormula α n
h₁ : φ₁.IsQF
h₂ : φ₂.IsQF
ihφ : Realize.{u, v, u_2, u'} (M := N) φ₁ ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs) ↔ φ₁.Realize v xs
ihψ : Realize.{u, v, u_2, u'} (M := N) φ₂ ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs) ↔ φ₂.Realize v xs
⊢ Realize.{u, v, u_2, u'} (M := N) (φ₁ ⟹ φ₂) ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs) ↔ (φ₁ ⟹ φ₂).Realize v xs

Tactic:
simp only [realize_imp, ihφ, ihψ]

Premises used: FirstOrder.Language.BoundedFormula.realize_imp
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
F : Type u_3
inst_2 : FunLike F M N
inst_3 : EmbeddingLike F M N
inst_4 : L.StrongHomClass F M N
φ : L.BoundedFormula α n
hQF : φ.IsQF
f : F
v : α → M
xs : Fin n → M
falsum :
  Realize.{u, v, u_2, u'} (L := L) (M := N) BoundedFormula.falsum ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs) ↔
    Realize.{u, v, u_1, u'} (L := L) BoundedFormula.falsum v xs
of_isAtomic :
  ∀ {φ : L.BoundedFormula α n} (hA : φ.IsAtomic),
    Realize.{u, v, u_2, u'} (M := N) φ ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs) ↔ φ.Realize v xs
imp :
  ∀ {φ₁ φ₂ : L.BoundedFormula α n},
    φ₁.IsQF →
      φ₂.IsQF →
        ∀
          (ihφ :
            Realize.{u, v, u_2, u'} (M := N) φ₁ ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs) ↔ φ₁.Realize v xs)
          (ihψ :
            Realize.{u, v, u_2, u'} (M := N) φ₂ ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs) ↔ φ₂.Realize v xs),
          Realize.{u, v, u_2, u'} (M := N) (φ₁ ⟹ φ₂) ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs) ↔
            (φ₁ ⟹ φ₂).Realize v xs
⊢ Realize.{u, v, u_2, u'} (M := N) φ ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs) ↔ φ.Realize v xs

Tactic:
induction hQF with
  | falsum => rfl
  | of_isAtomic hA => induction hA with
    | equal t₁ t₂ => simp only [realize_bdEqual, ← Sum.comp_elim, HomClass.realize_term,
        (EmbeddingLike.injective f).eq_iff]
    | rel R ts =>
      simp only [realize_rel, ← Sum.comp_elim, HomClass.realize_term]
      exact StrongHomClass.map_rel f R (fun i => Term.realize (Sum.elim v xs) (ts i))
  | imp _ _ ihφ ihψ => simp only [realize_imp, ihφ, ihψ]

Premises used: Function.Injective.eq_iff, FirstOrder.Language.BoundedFormula.IsQF.falsum, FirstOrder.Language.BoundedFormula.equal, FirstOrder.Language.HomClass.realize_term, EmbeddingLike.injective, FirstOrder.Language.BoundedFormula.IsQF.of_isAtomic, FirstOrder.Language.BoundedFormula.realize_rel, Sum.comp_elim, FirstOrder.Language.BoundedFormula.realize_bdEqual, FirstOrder.Language.BoundedFormula.realize_imp, FirstOrder.Language.BoundedFormula.IsQF.imp, FirstOrder.Language.BoundedFormula.rel
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
F : Type u_3
inst_2 : FunLike F M N
inst_3 : EmbeddingLike F M N
inst_4 : L.StrongHomClass F M N
φ : L.BoundedFormula α n
f : F
v : α → M
n_1 : ℕ
φ_1 : L.BoundedFormula α n_1
hQF : φ_1.IsQF
xs : Fin n_1 → M
⊢ Realize.{u, v, u_2, u'} (M := N) φ_1 ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs) → φ_1.Realize v xs

Tactic:
simp [hQF.realize_embedding]

Premises used: FirstOrder.Language.BoundedFormula.IsQF.realize_embedding
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
F : Type u_3
inst_2 : FunLike F M N
inst_3 : EmbeddingLike F M N
inst_4 : L.StrongHomClass F M N
φ : L.BoundedFormula α n
f : F
v : α → M
n_1 : ℕ
φ_1 : L.BoundedFormula α (n_1 + 1)
h : φ_1.IsUniversal
ih :
  ∀ {xs : Fin (n_1 + 1) → M},
    Realize.{u, v, u_2, u'} (M := N) φ_1 ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs) → φ_1.Realize v xs
xs : Fin n_1 → M
⊢ (∀ (a : N),
      Realize.{u, v, u_2, u'} (M := N) φ_1 ((⇑f : (a : M) → N) ∘ v)
        (snoc (α := fun (a : Fin (n_1 + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ xs) a)) →
    ∀ (a : M), φ_1.Realize v (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) xs a)

Tactic:
fun h a => ih ?_
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
F : Type u_3
inst_2 : FunLike F M N
inst_3 : EmbeddingLike F M N
inst_4 : L.StrongHomClass F M N
φ : L.BoundedFormula α n
f : F
v : α → M
n_1 : ℕ
φ_1 : L.BoundedFormula α (n_1 + 1)
h : φ_1.IsUniversal
ih :
  ∀ {xs : Fin (n_1 + 1) → M},
    Realize.{u, v, u_2, u'} (M := N) φ_1 ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs) → φ_1.Realize v xs
xs : Fin n_1 → M
all :
  ∀
    (h :
      ∀ (a : N),
        Realize.{u, v, u_2, u'} (M := N) φ_1 ((⇑f : (a : M) → N) ∘ v)
          (snoc (α := fun (a : Fin (n_1 + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ xs) a))
    (a : M),
    Realize.{u, v, u_2, u'} (M := N) φ_1 ((⇑f : (a : M) → N) ∘ v)
      (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N) (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) xs a))
⊢ (∀ (a : N),
      Realize.{u, v, u_2, u'} (M := N) φ_1 ((⇑f : (a : M) → N) ∘ v)
        (snoc (α := fun (a : Fin (n_1 + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ xs) a)) →
    ∀ (a : M), φ_1.Realize v (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) xs a)

Tactic:
refine fun h a => ih ?_
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
F : Type u_3
inst_2 : FunLike F M N
inst_3 : EmbeddingLike F M N
inst_4 : L.StrongHomClass F M N
φ : L.BoundedFormula α n
f : F
v : α → M
n_1 : ℕ
φ_1 : L.BoundedFormula α (n_1 + 1)
h_1 : φ_1.IsUniversal
ih :
  ∀ {xs : Fin (n_1 + 1) → M},
    Realize.{u, v, u_2, u'} (M := N) φ_1 ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs) → φ_1.Realize v xs
xs : Fin n_1 → M
h :
  ∀ (a : N),
    Realize.{u, v, u_2, u'} (M := N) φ_1 ((⇑f : (a : M) → N) ∘ v)
      (snoc (α := fun (a : Fin (n_1 + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ xs) a)
a : M
all :
  Realize.{u, v, u_2, u'} (M := N) φ_1 ((⇑f : (a : M) → N) ∘ v)
    (snoc (α := fun (i : Fin (n_1 + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ xs) ((f : (a : M) → N) a))
⊢ Realize.{u, v, u_2, u'} (M := N) φ_1 ((⇑f : (a : M) → N) ∘ v)
    (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N) (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) xs a))

Tactic:
rw [Fin.comp_snoc]

Premises used: Fin.comp_snoc
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
F : Type u_3
inst_2 : FunLike F M N
inst_3 : EmbeddingLike F M N
inst_4 : L.StrongHomClass F M N
φ : L.BoundedFormula α n
f : F
v : α → M
n_1 : ℕ
φ_1 : L.BoundedFormula α (n_1 + 1)
h_1 : φ_1.IsUniversal
ih :
  ∀ {xs : Fin (n_1 + 1) → M},
    Realize.{u, v, u_2, u'} (M := N) φ_1 ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs) → φ_1.Realize v xs
xs : Fin n_1 → M
h :
  ∀ (a : N),
    Realize.{u, v, u_2, u'} (M := N) φ_1 ((⇑f : (a : M) → N) ∘ v)
      (snoc (α := fun (a : Fin (n_1 + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ xs) a)
a : M
⊢ Realize.{u, v, u_2, u'} (M := N) φ_1 ((⇑f : (a : M) → N) ∘ v)
    (snoc (α := fun (i : Fin (n_1 + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ xs) ((f : (a : M) → N) a))

Tactic:
h (f a)

Premises used: DFunLike.coe
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
F : Type u_3
inst_2 : FunLike F M N
inst_3 : EmbeddingLike F M N
inst_4 : L.StrongHomClass F M N
φ : L.BoundedFormula α n
f : F
v : α → M
n_1 : ℕ
φ_1 : L.BoundedFormula α (n_1 + 1)
h_1 : φ_1.IsUniversal
ih :
  ∀ {xs : Fin (n_1 + 1) → M},
    Realize.{u, v, u_2, u'} (M := N) φ_1 ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs) → φ_1.Realize v xs
xs : Fin n_1 → M
h :
  ∀ (a : N),
    Realize.{u, v, u_2, u'} (M := N) φ_1 ((⇑f : (a : M) → N) ∘ v)
      (snoc (α := fun (a : Fin (n_1 + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ xs) a)
a : M
⊢ Realize.{u, v, u_2, u'} (M := N) φ_1 ((⇑f : (a : M) → N) ∘ v)
    (snoc (α := fun (i : Fin (n_1 + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ xs) ((f : (a : M) → N) a))

Tactic:
exact h (f a)

Premises used: DFunLike.coe