awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
f : M ≃[L] N
rw : (f.comp f.symm).toEmbedding = Embedding.refl L N
rw₁ : Eq (α := N ↪[L] N) (toEmbedding (refl L N)) (Embedding.refl L N)
rw₂ rw₃ : Eq (α := N ↪[L] N) (Embedding.refl L N) (Embedding.refl L N)
⊢ f.toEmbedding.comp f.symm.toEmbedding = Embedding.refl L N

Tactic:
rw [← comp_toEmbedding, self_comp_symm, refl_toEmbedding]

Premises used: FirstOrder.Language.Equiv.comp_toEmbedding, FirstOrder.Language.Equiv.self_comp_symm, FirstOrder.Language.Equiv.refl_toEmbedding
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
f : M ≃[L] N
rw : (f.symm.comp f).toHom = Hom.id L M
rw₁ : Eq (α := M →[L] M) (toHom (refl L M)) (Hom.id L M)
rw₂ rw₃ : Eq (α := M →[L] M) (Hom.id L M) (Hom.id L M)
⊢ f.symm.toHom.comp f.toHom = Hom.id L M

Tactic:
rw [← comp_toHom, symm_comp_self, refl_toHom]

Premises used: FirstOrder.Language.Equiv.symm_comp_self, FirstOrder.Language.Equiv.comp_toHom, FirstOrder.Language.Equiv.refl_toHom
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
f : M ≃[L] N
rw : (f.comp f.symm).toHom = Hom.id L N
rw₁ : Eq (α := N →[L] N) (toHom (refl L N)) (Hom.id L N)
rw₂ rw₃ : Eq (α := N →[L] N) (Hom.id L N) (Hom.id L N)
⊢ f.toHom.comp f.symm.toHom = Hom.id L N

Tactic:
rw [← comp_toHom, self_comp_symm, refl_toHom]

Premises used: FirstOrder.Language.Equiv.self_comp_symm, FirstOrder.Language.Equiv.comp_toHom, FirstOrder.Language.Equiv.refl_toHom
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
P : Type u_1
inst_2 : L.Structure P
f : M ≃[L] N
g : N ≃[L] P
⊢ (g.comp f).symm = f.symm.comp g.symm

Tactic:
rfl

Premises used: FirstOrder.Language.Equiv.comp, Equiv.symm, rfl, FirstOrder.Language.Equiv.symm
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
P : Type u_1
inst_2 : L.Structure P
h : M ≃[L] N
f g : N ≃[L] P
hfg : Eq (α := M ≃[L] P) ((fun (f : N ≃[L] P) ↦ f.comp h) f) ((fun (f : N ≃[L] P) ↦ f.comp h) g)
⊢ Eq (α := N ≃[L] P) ((fun (r : M ≃[L] P) ↦ r.comp h.symm) ((fun (f : N ≃[L] P) ↦ f.comp h) f))
    ((fun (r : M ≃[L] P) ↦ r.comp h.symm) ((fun (f : N ≃[L] P) ↦ f.comp h) g))

Tactic:
(congr_arg (fun r : (M ≃[L] P) ↦ r.comp h.symm) hfg)

Premises used: congr_arg, FirstOrder.Language.Equiv.comp, FirstOrder.Language.Equiv.symm
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
P : Type u_1
inst_2 : L.Structure P
h : M ≃[L] N
f g : N ≃[L] P
hfg : Eq (α := M ≃[L] P) ((fun (f : N ≃[L] P) ↦ f.comp h) f) ((fun (f : N ≃[L] P) ↦ f.comp h) g)
h₁ : f = comp ((fun (f : N ≃[L] P) ↦ f.comp h) f) h.symm
h₂ : g = comp ((fun (f : N ≃[L] P) ↦ f.comp h) g) h.symm
⊢ f = g

Tactic:
convert! (congr_arg (fun r : (M ≃[L] P) ↦ r.comp h.symm) hfg)

Premises used: congr_arg, FirstOrder.Language.Equiv.comp, FirstOrder.Language.Equiv.symm
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
P : Type u_1
inst_2 : L.Structure P
h : M ≃[L] N
f g : N ≃[L] P
hfg : Eq (α := M ≃[L] P) ((fun (f : N ≃[L] P) ↦ f.comp h) f) ((fun (f : N ≃[L] P) ↦ f.comp h) g)
h₁ : f = f.comp (h.comp h.symm)
h₂ : f = f.comp (refl L N)
h₃ h₄ : f = f
⊢ f = comp ((fun (f : N ≃[L] P) ↦ f.comp h) f) h.symm

Tactic:
rw [comp_assoc, self_comp_symm, comp_refl]

Premises used: FirstOrder.Language.Equiv.self_comp_symm, FirstOrder.Language.Equiv.comp_assoc, FirstOrder.Language.Equiv.comp_refl
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
P : Type u_1
inst_2 : L.Structure P
h : M ≃[L] N
f g : N ≃[L] P
hfg : Eq (α := M ≃[L] P) ((fun (f : N ≃[L] P) ↦ f.comp h) f) ((fun (f : N ≃[L] P) ↦ f.comp h) g)
h₁ : g = g.comp (h.comp h.symm)
h₂ : g = g.comp (refl L N)
h₃ h₄ : g = g
⊢ g = comp ((fun (f : N ≃[L] P) ↦ f.comp h) g) h.symm

Tactic:
rw [comp_assoc, self_comp_symm, comp_refl]

Premises used: FirstOrder.Language.Equiv.self_comp_symm, FirstOrder.Language.Equiv.comp_assoc, FirstOrder.Language.Equiv.comp_refl
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
P : Type u_1
inst_2 : L.Structure P
h : M ≃[L] N
f g : N ≃[L] P
⊢ f.comp h = g.comp h ↔ f = g

Tactic:
⟨fun eq ↦ h.comp_right_injective eq, congr_arg (fun (r : N ≃[L] P) ↦ r.comp h)⟩

Premises used: congr_arg, FirstOrder.Language.Equiv.comp_right_injective, Iff.intro, FirstOrder.Language.Equiv.comp
-- Module: Mathlib.ModelTheory.Basic
Goal:
L₁ : Language
L₂ : Language
S : Type u_3
inst : L₁.Structure S
inst_1 : L₂.Structure S
n : ℕ
f : L₁.Functions n
⊢ Eq.{u_3 + 1} (α := (Fin n → S) → S) (funMap (L := L₁.sum L₂) (Sum.inl f)) (funMap f)

Tactic:
rfl

Premises used: rfl, Sum.elim
-- Module: Mathlib.ModelTheory.Basic
Goal:
L₁ : Language
L₂ : Language
S : Type u_3
inst : L₁.Structure S
inst_1 : L₂.Structure S
n : ℕ
f : L₂.Functions n
⊢ Eq.{u_3 + 1} (α := (Fin n → S) → S) (funMap (L := L₁.sum L₂) (Sum.inr f)) (funMap f)

Tactic:
rfl

Premises used: rfl, Sum.elim
-- Module: Mathlib.ModelTheory.Basic
Goal:
L₁ : Language
L₂ : Language
S : Type u_3
inst : L₁.Structure S
inst_1 : L₂.Structure S
n : ℕ
R : L₁.Relations n
⊢ Eq.{u_3 + 1} (α := (Fin n → S) → Prop) (RelMap (L := L₁.sum L₂) (Sum.inl R)) (RelMap R)

Tactic:
rfl

Premises used: rfl, Sum.elim
-- Module: Mathlib.ModelTheory.Basic
Goal:
L₁ : Language
L₂ : Language
S : Type u_3
inst : L₁.Structure S
inst_1 : L₂.Structure S
n : ℕ
R : L₂.Relations n
⊢ Eq.{u_3 + 1} (α := (Fin n → S) → Prop) (RelMap (L := L₁.sum L₂) (Sum.inr R)) (RelMap R)

Tactic:
rfl

Premises used: rfl, Sum.elim
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
L' : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
P : Type u_1
inst_2 : L.Structure P
Q : Type u_2
inst_3 : L.Structure Q
a : Language.empty.Structure M
funMap : ∀ (x : ℕ) (f : Language.empty.Functions x) (x_1 : Fin x → M), Structure.funMap f x_1 = Structure.funMap f x_1
RelMap : ∀ (x : ℕ) (f : Language.empty.Relations x) (x_1 : Fin x → M), Structure.RelMap f x_1 ↔ Structure.RelMap f x_1
⊢ a = default

Tactic:
ext _ f
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
L' : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
P : Type u_1
inst_2 : L.Structure P
Q : Type u_2
inst_3 : L.Structure Q
a : Language.empty.Structure M
x : ℕ
f : Language.empty.Functions x
x_1 : Fin x → M
⊢ funMap f x_1 = funMap f x_1

Tactic:
Empty.elim f

Premises used: Empty.elim
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
L' : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
P : Type u_1
inst_2 : L.Structure P
Q : Type u_2
inst_3 : L.Structure Q
a : Language.empty.Structure M
x : ℕ
f : Language.empty.Functions x
x_1 : Fin x → M
⊢ funMap f x_1 = funMap f x_1

Tactic:
exact Empty.elim f

Premises used: Empty.elim
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
L' : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
P : Type u_1
inst_2 : L.Structure P
Q : Type u_2
inst_3 : L.Structure Q
a : Language.empty.Structure M
x : ℕ
f : Language.empty.Relations x
x_1 : Fin x → M
⊢ RelMap f x_1 ↔ RelMap f x_1

Tactic:
Empty.elim f

Premises used: Empty.elim
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
L' : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
P : Type u_1
inst_2 : L.Structure P
Q : Type u_2
inst_3 : L.Structure Q
a : Language.empty.Structure M
x : ℕ
f : Language.empty.Relations x
x_1 : Fin x → M
⊢ RelMap f x_1 ↔ RelMap f x_1

Tactic:
exact Empty.elim f

Premises used: Empty.elim
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
L' : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
P : Type u_1
inst_2 : L.Structure P
Q : Type u_2
inst_3 : L.Structure Q
inst_4 : Language.empty.Structure M
inst_5 : Language.empty.Structure N
F : Type u_3
inst_6 : FunLike F M N
⊢ Language.empty.StrongHomClass F M N

Tactic:
⟨fun _ _ f => Empty.elim f, fun _ _ r => Empty.elim r⟩

Premises used: Empty.elim, FirstOrder.Language.StrongHomClass.mk
-- Module: Mathlib.ModelTheory.Basic
Goal:
M : Type w
N : Type w'
inst : Language.empty.Structure M
inst_1 : Language.empty.Structure N
⊢ Nonempty (M ↪[Language.empty] N) ↔ lift.{w', w} #M ≤ lift.{w, w'} #N

Tactic:
_root_.trans ⟨Nonempty.map fun f => f.toEmbedding, Nonempty.map StrongHomClass.toEmbedding⟩
    Cardinal.lift_mk_le'.symm

Premises used: trans, FirstOrder.Language.StrongHomClass.toEmbedding, FirstOrder.Language.Embedding.toEmbedding, Iff.intro, Cardinal.lift_mk_le', Nonempty.map, Iff.symm
-- Module: Mathlib.ModelTheory.Basic
Goal:
M : Type w
N : Type w'
inst : Language.empty.Structure M
inst_1 : Language.empty.Structure N
⊢ Nonempty (M ≃[Language.empty] N) ↔ lift.{w', w} #M = lift.{w, w'} #N

Tactic:
_root_.trans ⟨Nonempty.map fun f => f.toEquiv, Nonempty.map fun f => { toEquiv := f }⟩
    Cardinal.lift_mk_eq'.symm

Premises used: trans, FirstOrder.Language.Equiv.mk, Cardinal.lift_mk_eq', FirstOrder.Language.Equiv.toEquiv, Iff.intro, Nonempty.map, Iff.symm
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
M : Type u_1
N : Type u_2
inst : L.Structure M
e : M ≃ N
this : L.Structure N := e.inducedStructure
n : ℕ
f : L.Functions n
x : Fin n → M
⊢ e.toFun (funMap f x) = funMap f (e.toFun ∘ x)

Tactic:
simp [← Function.comp_assoc e.symm e x]

Premises used: Equiv.symm, DFunLike.coe, Function.comp_assoc
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
M : Type u_1
N : Type u_2
inst : L.Structure M
e : M ≃ N
this : L.Structure N := e.inducedStructure
n : ℕ
r : L.Relations n
x : Fin n → M
⊢ RelMap r (e.toFun ∘ x) ↔ RelMap r x

Tactic:
simp [← Function.comp_assoc e.symm e x]

Premises used: Equiv.symm, DFunLike.coe, Function.comp_assoc
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
M : Type u_1
N : Type u_2
inst : L.Structure M
e : M ≃ N
this : L.Structure N := e.inducedStructure
⊢ M ≃[L] N

Tactic:
exact
  { e with
    map_fun' := @fun n f x => by simp [← Function.comp_assoc e.symm e x]
    map_rel' := @fun n r x => by simp [← Function.comp_assoc e.symm e x] }
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
M : Type u_1
N : Type u_2
inst : L.Structure M
e : M ≃ N
⊢ Equiv.toEquiv.{u_3, u_4, u_1, u_2} (L := L) e.inducedStructureEquiv = e

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
M : Type u_1
N : Type u_2
inst : L.Structure M
e : M ≃ N
⊢ Eq (α := (a : M) → N) (⇑e.inducedStructureEquiv : (a : M) → N) (⇑e : (a : M) → N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
M : Type u_1
N : Type u_2
inst : L.Structure M
e : M ≃ N
this : L.Structure N := e.inducedStructure
⊢ (a : N) → M

Tactic:
exact DFunLike.coe (@inducedStructureEquiv L M N _ e).symm

Premises used: Equiv.inducedStructureEquiv, DFunLike.coe, FirstOrder.Language.Equiv.symm
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
M : Type u_1
N : Type u_2
inst : L.Structure M
e : M ≃ N
⊢ Eq (α := (a : N) → M) (⇑(Language.Equiv.symm e.inducedStructureEquiv) : (a : N) → M) (⇑e.symm : (a : N) → M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.ModelTheory.Bundled
Goal:
L : Language
T : L.Theory
M : Type w
inst : L.Structure M
inst_1 : M ⊨ T
inst_2 : Nonempty M
⊢ (↑(of T M) : Type w) = M

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.ModelTheory.Bundled
Goal:
L : Language
T : L.Theory
M : ModelType.{u, v, u_1} T
⊢ Nonempty.{u_1 + 1} (↑M : Type u_1)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.ModelTheory.Bundled
Goal:
L : Language
T : L.Theory
M : Type w
inst : Nonempty M
inst_1 : L.Structure M
inst_2 : M ⊨ T
h : Small.{w', w} M
⊢ Small.{w', w} (↑(of T M) : Type w)

Tactic:
h
-- Module: Mathlib.ModelTheory.Bundled
Goal:
L : Language
T : L.Theory
M : ModelType.{u, v, u_1} T
T' : L.Theory
h : T' ⊆ T
⊢ Model.{u, v, u_1} (↑(M.subtheoryModel (T := T) (T' := T') h) : Type u_1) T

Tactic:
M.is_model

Premises used: FirstOrder.Language.Theory.ModelType.is_model
-- Module: Mathlib.ModelTheory.Bundled
Goal:
L : Language
T : L.Theory
M : Type w
inst : L.Structure M
inst_1 : Nonempty M
h : M ⊨ T
⊢ (↑(h.bundled (T := T)) : Type w) = M

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.ModelTheory.Bundled
Goal:
L : Language
T : L.Theory
M : Theory.ModelType.{u, v, x} T
S : L.ElementarySubstructure (↑M : Type x)
h : Small.{w, x} ↥S
⊢ Small.{w, x} (↑(toModel T S) : Type x)

Tactic:
h
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α (n + 1)
con : (∀' φ).IsAtomic
⊢ False

Tactic:
cases con
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α (n + 1)
con : (∃' φ).IsAtomic
⊢ False

Tactic:
cases con
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
β : Type v'
n m : ℕ
φ : L.BoundedFormula α m
h : φ.IsAtomic
f : α → β ⊕ Fin n
⊢ (BoundedFormula.relabel f φ).IsAtomic

Tactic:
IsAtomic.recOn h (fun _ _ => IsAtomic.equal _ _) fun _ _ => IsAtomic.rel _ _

Premises used: FirstOrder.Language.BoundedFormula.IsAtomic.recOn
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
l : ℕ
φ : L.BoundedFormula α l
k m : ℕ
h : φ.IsAtomic
⊢ (BoundedFormula.liftAt k m φ).IsAtomic

Tactic:
IsAtomic.recOn h (fun _ _ => IsAtomic.equal _ _) fun _ _ => IsAtomic.rel _ _

Premises used: FirstOrder.Language.BoundedFormula.IsAtomic.recOn
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n l : ℕ
φ : L.BoundedFormula α l
h : l ≤ n
hφ : φ.IsAtomic
⊢ (BoundedFormula.castLE h φ).IsAtomic

Tactic:
IsAtomic.recOn hφ (fun _ _ => IsAtomic.equal _ _) fun _ _ => IsAtomic.rel _ _

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

Tactic:
IsQF.of_isAtomic

Premises used: FirstOrder.Language.BoundedFormula.IsQF.of_isAtomic
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
⊢ IsQF.{u, v, u'} (L := L) (α := α) (n := n) ⊥

Tactic:
IsQF.falsum

Premises used: FirstOrder.Language.BoundedFormula.IsQF.falsum
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α n
h : φ.IsQF
⊢ (∼φ).IsQF

Tactic:
h.imp isQF_bot

Premises used: FirstOrder.Language.BoundedFormula.isQF_bot, FirstOrder.Language.BoundedFormula.not, FirstOrder.Language.BoundedFormula.IsQF.imp
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
⊢ IsQF.{u, v, u'} (L := L) (α := α) (n := n) ⊤

Tactic:
isQF_bot.not

Premises used: FirstOrder.Language.BoundedFormula.isQF_bot, FirstOrder.Language.BoundedFormula.IsQF.not
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
φ ψ : L.BoundedFormula α n
hφ : φ.IsQF
hψ : ψ.IsQF
⊢ (φ ⊔ ψ).IsQF

Tactic:
hφ.not.imp hψ

Premises used: FirstOrder.Language.BoundedFormula.IsQF.not, FirstOrder.Language.BoundedFormula.IsQF.imp
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
φ ψ : L.BoundedFormula α n
hφ : φ.IsQF
hψ : ψ.IsQF
⊢ (φ ⊓ ψ).IsQF

Tactic:
(hφ.imp hψ.not).not

Premises used: FirstOrder.Language.BoundedFormula.IsQF.not, FirstOrder.Language.BoundedFormula.IsQF.imp
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
β : Type v'
n m : ℕ
φ : L.BoundedFormula α m
h : φ.IsQF
f : α → β ⊕ Fin n
⊢ (relabel f φ).IsQF

Tactic:
IsQF.recOn h isQF_bot (fun h => (h.relabel f).isQF) fun _ _ h1 h2 => h1.imp h2

Premises used: FirstOrder.Language.BoundedFormula.IsQF.recOn
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
l : ℕ
φ : L.BoundedFormula α l
k m : ℕ
h : φ.IsQF
⊢ (liftAt k m φ).IsQF

Tactic:
IsQF.recOn h isQF_bot (fun ih => ih.liftAt.isQF) fun _ _ ih1 ih2 => ih1.imp ih2

Premises used: FirstOrder.Language.BoundedFormula.IsQF.recOn
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n l : ℕ
φ : L.BoundedFormula α l
h : l ≤ n
hφ : φ.IsQF
⊢ (castLE h φ).IsQF

Tactic:
IsQF.recOn hφ isQF_bot (fun ih => ih.castLE.isQF) fun _ _ ih1 ih2 => ih1.imp ih2

Premises used: FirstOrder.Language.BoundedFormula.IsQF.recOn
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α (n + 1)
con : (∀' φ).IsQF
⊢ (∀' φ).IsAtomic

Tactic:
obtain - | con := con
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α (n + 1)
con : (∀' φ).IsAtomic
⊢ False

Tactic:
φ.not_all_isAtomic con

Premises used: FirstOrder.Language.BoundedFormula.not_all_isAtomic
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α (n + 1)
con : (∀' φ).IsAtomic
⊢ False

Tactic:
exact φ.not_all_isAtomic con

Premises used: FirstOrder.Language.BoundedFormula.not_all_isAtomic
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α (n + 1)
con : (∃' φ).IsQF
of_isAtomic : ∀ (con : (∃' φ).IsAtomic), False
imp : ∀ (con : (∀' ∼φ).IsQF), IsQF.{u, v, u'} (L := L) (α := α) (n := n) ⊥ → False
⊢ False

Tactic:
obtain - | con | con := con
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α (n + 1)
con : (∃' φ).IsAtomic
⊢ False

Tactic:
φ.not_ex_isAtomic con

Premises used: FirstOrder.Language.BoundedFormula.not_ex_isAtomic
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α (n + 1)
con : (∃' φ).IsAtomic
⊢ False

Tactic:
exact φ.not_ex_isAtomic con

Premises used: FirstOrder.Language.BoundedFormula.not_ex_isAtomic
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α (n + 1)
con : (∀' ∼φ).IsQF
h₂ : IsQF.{u, v, u'} (L := L) (α := α) (n := n) ⊥
⊢ False

Tactic:
not_all_isQF _ con

Premises used: FirstOrder.Language.BoundedFormula.not_all_isQF
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α (n + 1)
con : (∀' ∼φ).IsQF
h₂ : IsQF.{u, v, u'} (L := L) (α := α) (n := n) ⊥
⊢ False

Tactic:
exact not_all_isQF _ con

Premises used: FirstOrder.Language.BoundedFormula.not_all_isQF
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α n
⊢ φ.IsQF → φ.IsPrenex

Tactic:
IsPrenex.of_isQF

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

Tactic:
h.isQF.isPrenex

Premises used: FirstOrder.Language.BoundedFormula.IsQF.isPrenex, FirstOrder.Language.BoundedFormula.IsAtomic.isQF
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
P : {n : ℕ} → L.BoundedFormula α n → Prop
φ : L.BoundedFormula α n
h : φ.IsPrenex
hq : ∀ {m : ℕ} {ψ : L.BoundedFormula α m}, ψ.IsQF → P ψ
ha : ∀ {m : ℕ} {ψ : L.BoundedFormula α (m + 1)}, P ψ → P (∀' ψ)
hn : ∀ {m : ℕ} {ψ : L.BoundedFormula α m}, P ψ → P ∼ψ
⊢ P φ

Tactic:
IsPrenex.recOn h hq (fun _ => ha) fun _ ih => hn (ha (hn ih))

Premises used: FirstOrder.Language.BoundedFormula.IsPrenex.recOn
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
β : Type v'
n m : ℕ
φ : L.BoundedFormula α m
h_1 : φ.IsPrenex
f : α → β ⊕ Fin n
n_1 : ℕ
φ_1 : L.BoundedFormula α (n_1 + 1)
h_2 : φ_1.IsPrenex
h : (BoundedFormula.relabel f φ_1).IsPrenex
⊢ (BoundedFormula.relabel f (∀' φ_1)).IsPrenex

Tactic:
simp [h.all]

Premises used: FirstOrder.Language.BoundedFormula.IsPrenex.all
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
β : Type v'
n m : ℕ
φ : L.BoundedFormula α m
h_1 : φ.IsPrenex
f : α → β ⊕ Fin n
n_1 : ℕ
φ_1 : L.BoundedFormula α (n_1 + 1)
h_2 : φ_1.IsPrenex
h : (BoundedFormula.relabel f φ_1).IsPrenex
⊢ (BoundedFormula.relabel f (∃' φ_1)).IsPrenex

Tactic:
simp [h.ex]

Premises used: FirstOrder.Language.BoundedFormula.IsPrenex.ex
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
l : ℕ
φ : L.BoundedFormula α l
hφ : φ.IsPrenex
n : ℕ
h : l ≤ n
⊢ (BoundedFormula.castLE h φ).IsPrenex

Tactic:
IsPrenex.recOn (motive := @fun l φ _ => ∀ (n : ℕ) (h : l ≤ n), (φ.castLE h).IsPrenex) hφ
    (@fun _ _ ih _ _ => ih.castLE.isPrenex)
    (@fun _ _ _ ih _ _ => (ih _ _).all)
    (@fun _ _ _ ih _ _ => (ih _ _).ex) _ _

Premises used: FirstOrder.Language.BoundedFormula.IsPrenex.ex, FirstOrder.Language.BoundedFormula.castLE._proof_3, FirstOrder.Language.BoundedFormula.IsQF.isPrenex, FirstOrder.Language.BoundedFormula.IsPrenex.all, HAdd.hAdd, OfNat.ofNat, FirstOrder.Language.BoundedFormula.IsPrenex.recOn, FirstOrder.Language.BoundedFormula.IsQF.castLE
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
l : ℕ
φ : L.BoundedFormula α l
k m : ℕ
h : φ.IsPrenex
⊢ (BoundedFormula.liftAt k m φ).IsPrenex

Tactic:
IsPrenex.recOn h (fun ih => ih.liftAt.isPrenex) (fun _ ih => ih.castLE.all)
    fun _ ih => ih.castLE.ex

Premises used: FirstOrder.Language.BoundedFormula.IsPrenex.recOn
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
ψ : L.BoundedFormula α n
n_1 : ℕ
φ_1 : L.BoundedFormula α n_1
hψ : φ_1.IsQF
φ : L.BoundedFormula α n_1
hφ : φ.IsQF
of_isQF : (φ ⟹ φ_1).IsPrenex
⊢ (φ.toPrenexImpRight φ_1).IsPrenex

Tactic:
rw [hψ.toPrenexImpRight]

Premises used: FirstOrder.Language.BoundedFormula.IsQF.toPrenexImpRight
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
ψ : L.BoundedFormula α n
n_1 : ℕ
φ_1 : L.BoundedFormula α n_1
hψ : φ_1.IsQF
φ : L.BoundedFormula α n_1
hφ : φ.IsQF
⊢ (φ ⟹ φ_1).IsPrenex

Tactic:
(hφ.imp hψ).isPrenex

Premises used: FirstOrder.Language.BoundedFormula.IsQF.isPrenex, FirstOrder.Language.BoundedFormula.IsQF.imp
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
ψ : L.BoundedFormula α n
n_1 : ℕ
φ_1 : L.BoundedFormula α n_1
hψ : φ_1.IsQF
φ : L.BoundedFormula α n_1
hφ : φ.IsQF
⊢ (φ ⟹ φ_1).IsPrenex

Tactic:
exact (hφ.imp hψ).isPrenex

Premises used: FirstOrder.Language.BoundedFormula.IsQF.isPrenex, FirstOrder.Language.BoundedFormula.IsQF.imp
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
ψ : L.BoundedFormula α n
n_1 : ℕ
φ_1 : L.BoundedFormula α (n_1 + 1)
h : φ_1.IsPrenex
ih1 : ∀ {φ : L.BoundedFormula α (n_1 + 1)} (hφ : φ.IsQF), (φ.toPrenexImpRight φ_1).IsPrenex
φ : L.BoundedFormula α n_1
hφ : φ.IsQF
⊢ (φ.toPrenexImpRight (∀' φ_1)).IsPrenex

Tactic:
(ih1 hφ.liftAt).all

Premises used: FirstOrder.Language.BoundedFormula.toPrenexImpRight, FirstOrder.Language.BoundedFormula.IsPrenex.all, FirstOrder.Language.BoundedFormula.IsQF.liftAt
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
ψ : L.BoundedFormula α n
n_1 : ℕ
φ_1 : L.BoundedFormula α (n_1 + 1)
h : φ_1.IsPrenex
ih1 : ∀ {φ : L.BoundedFormula α (n_1 + 1)} (hφ : φ.IsQF), (φ.toPrenexImpRight φ_1).IsPrenex
φ : L.BoundedFormula α n_1
hφ : φ.IsQF
⊢ (φ.toPrenexImpRight (∀' φ_1)).IsPrenex

Tactic:
exact (ih1 hφ.liftAt).all

Premises used: FirstOrder.Language.BoundedFormula.IsPrenex.all, FirstOrder.Language.BoundedFormula.IsQF.liftAt
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
ψ : L.BoundedFormula α n
n_1 : ℕ
φ_1 : L.BoundedFormula α (n_1 + 1)
h : φ_1.IsPrenex
ih2 : ∀ {φ : L.BoundedFormula α (n_1 + 1)} (hφ : φ.IsQF), (φ.toPrenexImpRight φ_1).IsPrenex
φ : L.BoundedFormula α n_1
hφ : φ.IsQF
⊢ (φ.toPrenexImpRight (∃' φ_1)).IsPrenex

Tactic:
(ih2 hφ.liftAt).ex

Premises used: FirstOrder.Language.BoundedFormula.IsPrenex.ex, FirstOrder.Language.BoundedFormula.toPrenexImpRight, FirstOrder.Language.BoundedFormula.not, FirstOrder.Language.BoundedFormula.IsQF.liftAt, FirstOrder.Language.BoundedFormula.ex