awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.Equivalence
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α n
M : T.ModelType
v : α → (↑M : Type (max (max u v) w))
xs : Fin n → (↑M : Type (max (max u v) w))
⊢ φ.Realize v xs ∧ ψ.Realize v xs → ψ.Realize v xs

Tactic:
exact And.right

Premises used: And.right
-- Module: Mathlib.ModelTheory.Equivalence
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ θ : L.BoundedFormula α n
h₁ : φ ⟹[T] ψ
h₂ : φ ⟹[T] θ
M : T.ModelType
v : α → (↑M : Type (max (max u v) w))
xs : Fin n → (↑M : Type (max (max u v) w))
simp : φ.Realize v xs → ψ.Realize v xs ∧ θ.Realize v xs
⊢ (φ ⟹ ψ ⊓ θ).Realize v xs

Tactic:
simp only [BoundedFormula.realize_imp, BoundedFormula.realize_inf]

Premises used: FirstOrder.Language.BoundedFormula.realize_inf, FirstOrder.Language.BoundedFormula.realize_imp
-- Module: Mathlib.ModelTheory.Equivalence
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ θ : L.BoundedFormula α n
h₁ : φ ⟹[T] ψ
h₂ : φ ⟹[T] θ
M : T.ModelType
v : α → (↑M : Type (max (max u v) w))
xs : Fin n → (↑M : Type (max (max u v) w))
⊢ φ.Realize v xs → ψ.Realize v xs ∧ θ.Realize v xs

Tactic:
fun h => ⟨h₁ M v xs h, h₂ M v xs h⟩

Premises used: And.intro
-- Module: Mathlib.ModelTheory.Equivalence
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ θ : L.BoundedFormula α n
h₁ : φ ⟹[T] ψ
h₂ : φ ⟹[T] θ
M : T.ModelType
v : α → (↑M : Type (max (max u v) w))
xs : Fin n → (↑M : Type (max (max u v) w))
⊢ φ.Realize v xs → ψ.Realize v xs ∧ θ.Realize v xs

Tactic:
exact fun h => ⟨h₁ M v xs h, h₂ M v xs h⟩
-- Module: Mathlib.ModelTheory.Equivalence
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ θ : L.BoundedFormula α n
⊢ φ ⟹[T] ψ ⊓ θ ↔ φ ⟹[T] ψ ∧ φ ⟹[T] θ

Tactic:
⟨fun h => ⟨h.trans (inf_imp_left _ _), h.trans (inf_imp_right _ _)⟩,
    fun ⟨h₁, h₂⟩ => imp_inf h₁ h₂⟩

Premises used: FirstOrder.Language.Theory.imp_inf, FirstOrder.Language.Theory.Imp, FirstOrder.Language.Theory.inf_imp_left, FirstOrder.Language.Theory.inf_imp_right, And.intro, Iff.intro, _private.0.FirstOrder.Language.Theory.imp_inf_iff.match_1, FirstOrder.Language.Theory.Imp.trans, Min.min
-- Module: Mathlib.ModelTheory.Equivalence
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α n
⊢ φ ⇔[T] ψ ↔ φ ⟹[T] ψ ∧ ψ ⟹[T] φ

Tactic:
simp only [Theory.Imp, ModelsBoundedFormula, BoundedFormula.realize_imp, ← forall_and,
    Theory.Iff, BoundedFormula.realize_iff, iff_iff_implies_and_implies]

Premises used: FirstOrder.Language.Theory.ModelsBoundedFormula, iff_iff_implies_and_implies, FirstOrder.Language.Theory.Imp, FirstOrder.Language.Theory.Iff, FirstOrder.Language.BoundedFormula.realize_iff, FirstOrder.Language.BoundedFormula.realize_imp, forall_and
-- Module: Mathlib.ModelTheory.Equivalence
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α n
h₁ : φ ⟹[T] ψ
h₂ : ψ ⟹[T] φ
⊢ φ ⇔[T] ψ

Tactic:
iff_iff_imp_and_imp.2 ⟨h₁, h₂⟩

Premises used: Iff.mpr, FirstOrder.Language.Theory.iff_iff_imp_and_imp, And.intro
-- Module: Mathlib.ModelTheory.Equivalence
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α n
h : φ ⇔[T] ψ
⊢ φ ⟹[T] ψ

Tactic:
(iff_iff_imp_and_imp.1 h).1

Premises used: And.left, FirstOrder.Language.Theory.iff_iff_imp_and_imp, Iff.mp
-- Module: Mathlib.ModelTheory.Equivalence
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α n
h : φ ⇔[T] ψ
⊢ ψ ⟹[T] φ

Tactic:
(iff_iff_imp_and_imp.1 h).2

Premises used: And.right, FirstOrder.Language.Theory.iff_iff_imp_and_imp, Iff.mp
-- Module: Mathlib.ModelTheory.Equivalence
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ : L.BoundedFormula α n
M : T.ModelType
v : α → (↑M : Type (max (max u v) w))
xs : Fin n → (↑M : Type (max (max u v) w))
rw rw₁ : φ.Realize v xs ↔ φ.Realize v xs
⊢ (φ ⇔ φ).Realize v xs

Tactic:
rw [BoundedFormula.realize_iff]

Premises used: FirstOrder.Language.BoundedFormula.realize_iff
-- Module: Mathlib.ModelTheory.Equivalence
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
M : Type u_1
inst : Nonempty M
inst_1 : L.Structure M
inst_2 : M ⊨ T
⊢ Std.Refl (α := L.BoundedFormula α n) T.Iff

Tactic:
⟨Iff.refl⟩

Premises used: Std.Refl.mk, FirstOrder.Language.Theory.Iff.refl
-- Module: Mathlib.ModelTheory.Equivalence
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α n
h : φ ⇔[T] ψ
M : T.ModelType
v : α → (↑M : Type (max (max u v) w))
xs : Fin n → (↑M : Type (max (max u v) w))
rw : (φ ⇔ ψ).Realize v xs
⊢ (ψ ⇔ φ).Realize v xs

Tactic:
rw [BoundedFormula.realize_iff, Iff.comm, ← BoundedFormula.realize_iff]

Premises used: FirstOrder.Language.BoundedFormula.realize_iff, Iff.comm
-- Module: Mathlib.ModelTheory.Equivalence
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α n
h : φ ⇔[T] ψ
M : T.ModelType
v : α → (↑M : Type (max (max u v) w))
xs : Fin n → (↑M : Type (max (max u v) w))
⊢ (φ ⇔ ψ).Realize v xs

Tactic:
h M v xs
-- Module: Mathlib.ModelTheory.Equivalence
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α n
h : φ ⇔[T] ψ
M : T.ModelType
v : α → (↑M : Type (max (max u v) w))
xs : Fin n → (↑M : Type (max (max u v) w))
⊢ (φ ⇔ ψ).Realize v xs

Tactic:
exact h M v xs
-- Module: Mathlib.ModelTheory.Equivalence
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
M : Type u_1
inst : Nonempty M
inst_1 : L.Structure M
inst_2 : M ⊨ T
⊢ Std.Symm (α := L.BoundedFormula α n) T.Iff

Tactic:
⟨fun _ _ => Iff.symm⟩

Premises used: Std.Symm.mk, FirstOrder.Language.Theory.Iff.symm
-- Module: Mathlib.ModelTheory.Equivalence
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ θ : L.BoundedFormula α n
h1 : φ ⇔[T] ψ
h2 : ψ ⇔[T] θ
M : T.ModelType
v : α → (↑M : Type (max (max u v) w))
xs : Fin n → (↑M : Type (max (max u v) w))
⊢ (φ ⇔ ψ).Realize v xs

Tactic:
have h1' := h1 M v xs
-- Module: Mathlib.ModelTheory.Equivalence
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ θ : L.BoundedFormula α n
h1 : φ ⇔[T] ψ
h2 : ψ ⇔[T] θ
M : T.ModelType
v : α → (↑M : Type (max (max u v) w))
xs : Fin n → (↑M : Type (max (max u v) w))
h1' : (φ ⇔ ψ).Realize v xs
⊢ (ψ ⇔ θ).Realize v xs

Tactic:
have h2' := h2 M v xs
-- Module: Mathlib.ModelTheory.Equivalence
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ θ : L.BoundedFormula α n
h1 : φ ⇔[T] ψ
h2 : ψ ⇔[T] θ
M : T.ModelType
v : α → (↑M : Type (max (max u v) w))
xs : Fin n → (↑M : Type (max (max u v) w))
h1' : (φ ⇔ ψ).Realize v xs
h2' : (ψ ⇔ θ).Realize v xs
rw : ∀ (h1' : φ.Realize v xs ↔ ψ.Realize v xs) (h2' : ψ.Realize v xs ↔ θ.Realize v xs), φ.Realize v xs ↔ θ.Realize v xs
⊢ (φ ⇔ θ).Realize v xs

Tactic:
rw [BoundedFormula.realize_iff] at *

Premises used: FirstOrder.Language.BoundedFormula.realize_iff
-- Module: Mathlib.ModelTheory.Equivalence
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ θ : L.BoundedFormula α n
h1 : φ ⇔[T] ψ
h2 : ψ ⇔[T] θ
M : T.ModelType
v : α → (↑M : Type (max (max u v) w))
xs : Fin n → (↑M : Type (max (max u v) w))
h1' : φ.Realize v xs ↔ ψ.Realize v xs
h2' : ψ.Realize v xs ↔ θ.Realize v xs
⊢ φ.Realize v xs ↔ θ.Realize v xs

Tactic:
⟨h2'.1 ∘ h1'.1, h1'.2 ∘ h2'.2⟩

Premises used: Iff.mpr, Function.comp, Iff.intro, Iff.mp
-- Module: Mathlib.ModelTheory.Equivalence
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ θ : L.BoundedFormula α n
h1 : φ ⇔[T] ψ
h2 : ψ ⇔[T] θ
M : T.ModelType
v : α → (↑M : Type (max (max u v) w))
xs : Fin n → (↑M : Type (max (max u v) w))
h1' : φ.Realize v xs ↔ ψ.Realize v xs
h2' : ψ.Realize v xs ↔ θ.Realize v xs
⊢ φ.Realize v xs ↔ θ.Realize v xs

Tactic:
exact ⟨h2'.1 ∘ h1'.1, h1'.2 ∘ h2'.2⟩
-- Module: Mathlib.ModelTheory.Equivalence
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
M : Type u_1
inst : Nonempty M
inst_1 : L.Structure M
inst_2 : M ⊨ T
⊢ IsTrans (L.BoundedFormula α n) T.Iff

Tactic:
⟨fun _ _ _ => Iff.trans⟩

Premises used: IsTrans.mk, FirstOrder.Language.Theory.Iff.trans
-- Module: Mathlib.ModelTheory.Equivalence
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
M : Type u_1
inst : Nonempty M
inst_1 : L.Structure M
inst_2 : M ⊨ T
φ ψ : L.BoundedFormula α n
h : φ ⇔[T] ψ
v : α → M
xs : Fin n → M
⊢ φ.Realize v xs ↔ ψ.Realize v xs

Tactic:
BoundedFormula.realize_iff.1 (h.realize_boundedFormula M)

Premises used: Iff.mp, FirstOrder.Language.BoundedFormula.realize_iff, FirstOrder.Language.Theory.ModelsBoundedFormula.realize_boundedFormula
-- Module: Mathlib.ModelTheory.Equivalence
Goal:
L : Language
T : L.Theory
α : Type w
φ ψ : L.Formula α
M : Type u_2
inst : Nonempty M
inst_1 : L.Structure M
inst_2 : M ⊨ T
h : φ ⇔[T] ψ
v : α → M
⊢ φ.Realize v ↔ ψ.Realize v

Tactic:
h.realize_bd_iff

Premises used: FirstOrder.Language.Theory.Iff.realize_bd_iff, FirstOrder.Language.Formula.Realize
-- Module: Mathlib.ModelTheory.Equivalence
Goal:
L : Language
T : L.Theory
φ ψ : L.Sentence
M : Type u_2
inst : Nonempty M
inst_1 : L.Structure M
inst_2 : M ⊨ T
h : φ ⇔[T] ψ
⊢ M ⊨ φ ↔ M ⊨ ψ

Tactic:
h.realize_iff

Premises used: FirstOrder.Language.Sentence.Realize, FirstOrder.Language.Theory.Iff.realize_iff
-- Module: Mathlib.ModelTheory.Equivalence
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α (n + 1)
h : φ ⇔[T] ψ
simp_rw :
  ∀ (M : T.ModelType) (v : α → (↑M : Type (max (max u v) w))) (xs : Fin n → (↑M : Type (max (max u v) w))),
    (∀ (a : (↑M : Type (max (max u v) w))),
        φ.Realize v (Fin.snoc (α := fun (a : Fin n.succ) ↦ (↑M : Type (max (max u v) w))) xs a)) ↔
      ∀ (a : (↑M : Type (max (max u v) w))),
        ψ.Realize v (Fin.snoc (α := fun (a : Fin n.succ) ↦ (↑M : Type (max (max u v) w))) xs a)
⊢ ∀' φ ⇔[T] ∀' ψ

Tactic:
simp_rw [Theory.Iff, ModelsBoundedFormula, BoundedFormula.realize_iff,
    BoundedFormula.realize_all]

Premises used: FirstOrder.Language.Theory.ModelsBoundedFormula, FirstOrder.Language.BoundedFormula.realize_all, FirstOrder.Language.Theory.Iff, FirstOrder.Language.BoundedFormula.realize_iff
-- Module: Mathlib.ModelTheory.Equivalence
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α (n + 1)
h : φ ⇔[T] ψ
⊢ ∀ (M : T.ModelType) (v : α → (↑M : Type (max (max u v) w))) (xs : Fin n → (↑M : Type (max (max u v) w))),
    (∀ (a : (↑M : Type (max (max u v) w))),
        φ.Realize v (Fin.snoc (α := fun (a : Fin n.succ) ↦ (↑M : Type (max (max u v) w))) xs a)) ↔
      ∀ (a : (↑M : Type (max (max u v) w))),
        ψ.Realize v (Fin.snoc (α := fun (a : Fin n.succ) ↦ (↑M : Type (max (max u v) w))) xs a)

Tactic:
fun M v xs => forall_congr' fun a => h.realize_bd_iff

Premises used: forall_congr', FirstOrder.Language.Theory.Iff.realize_bd_iff
-- Module: Mathlib.ModelTheory.Equivalence
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α (n + 1)
h : φ ⇔[T] ψ
⊢ ∀ (M : T.ModelType) (v : α → (↑M : Type (max (max u v) w))) (xs : Fin n → (↑M : Type (max (max u v) w))),
    (∀ (a : (↑M : Type (max (max u v) w))),
        φ.Realize v (Fin.snoc (α := fun (a : Fin n.succ) ↦ (↑M : Type (max (max u v) w))) xs a)) ↔
      ∀ (a : (↑M : Type (max (max u v) w))),
        ψ.Realize v (Fin.snoc (α := fun (a : Fin n.succ) ↦ (↑M : Type (max (max u v) w))) xs a)

Tactic:
exact fun M v xs => forall_congr' fun a => h.realize_bd_iff

Premises used: forall_congr', FirstOrder.Language.Theory.Iff.realize_bd_iff
-- Module: Mathlib.ModelTheory.Equivalence
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α (n + 1)
h : φ ⇔[T] ψ
simp_rw :
  ∀ (M : T.ModelType) (v : α → (↑M : Type (max (max u v) w))) (xs : Fin n → (↑M : Type (max (max u v) w))),
    (∃ (a : (↑M : Type (max (max u v) w))),
        φ.Realize v (Fin.snoc (α := fun (a : Fin n.succ) ↦ (↑M : Type (max (max u v) w))) xs a)) ↔
      ∃ (a : (↑M : Type (max (max u v) w))),
        ψ.Realize v (Fin.snoc (α := fun (a : Fin n.succ) ↦ (↑M : Type (max (max u v) w))) xs a)
⊢ ∃' φ ⇔[T] ∃' ψ

Tactic:
simp_rw [Theory.Iff, ModelsBoundedFormula, BoundedFormula.realize_iff,
    BoundedFormula.realize_ex]

Premises used: FirstOrder.Language.BoundedFormula.realize_ex, FirstOrder.Language.Theory.ModelsBoundedFormula, FirstOrder.Language.Theory.Iff, FirstOrder.Language.BoundedFormula.realize_iff
-- Module: Mathlib.ModelTheory.Equivalence
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α (n + 1)
h : φ ⇔[T] ψ
⊢ ∀ (M : T.ModelType) (v : α → (↑M : Type (max (max u v) w))) (xs : Fin n → (↑M : Type (max (max u v) w))),
    (∃ (a : (↑M : Type (max (max u v) w))),
        φ.Realize v (Fin.snoc (α := fun (a : Fin n.succ) ↦ (↑M : Type (max (max u v) w))) xs a)) ↔
      ∃ (a : (↑M : Type (max (max u v) w))),
        ψ.Realize v (Fin.snoc (α := fun (a : Fin n.succ) ↦ (↑M : Type (max (max u v) w))) xs a)

Tactic:
fun M v xs => exists_congr fun a => h.realize_bd_iff

Premises used: exists_congr, FirstOrder.Language.Theory.Iff.realize_bd_iff
-- Module: Mathlib.ModelTheory.Equivalence
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α (n + 1)
h : φ ⇔[T] ψ
⊢ ∀ (M : T.ModelType) (v : α → (↑M : Type (max (max u v) w))) (xs : Fin n → (↑M : Type (max (max u v) w))),
    (∃ (a : (↑M : Type (max (max u v) w))),
        φ.Realize v (Fin.snoc (α := fun (a : Fin n.succ) ↦ (↑M : Type (max (max u v) w))) xs a)) ↔
      ∃ (a : (↑M : Type (max (max u v) w))),
        ψ.Realize v (Fin.snoc (α := fun (a : Fin n.succ) ↦ (↑M : Type (max (max u v) w))) xs a)

Tactic:
exact fun M v xs => exists_congr fun a => h.realize_bd_iff

Premises used: exists_congr, FirstOrder.Language.Theory.Iff.realize_bd_iff
-- Module: Mathlib.ModelTheory.Equivalence
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α n
h : φ ⇔[T] ψ
simp_rw :
  ∀ (M : T.ModelType) (v : α → (↑M : Type (max (max u v) w))) (xs : Fin n → (↑M : Type (max (max u v) w))),
    ¬φ.Realize v xs ↔ ¬ψ.Realize v xs
⊢ ∼φ ⇔[T] ∼ψ

Tactic:
simp_rw [Theory.Iff, ModelsBoundedFormula, BoundedFormula.realize_iff,
    BoundedFormula.realize_not]

Premises used: FirstOrder.Language.Theory.ModelsBoundedFormula, FirstOrder.Language.BoundedFormula.realize_not, FirstOrder.Language.Theory.Iff, FirstOrder.Language.BoundedFormula.realize_iff
-- Module: Mathlib.ModelTheory.Equivalence
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α n
h : φ ⇔[T] ψ
⊢ ∀ (M : T.ModelType) (v : α → (↑M : Type (max (max u v) w))) (xs : Fin n → (↑M : Type (max (max u v) w))),
    ¬φ.Realize v xs ↔ ¬ψ.Realize v xs

Tactic:
fun M v xs => not_congr h.realize_bd_iff

Premises used: FirstOrder.Language.Theory.Iff.realize_bd_iff, not_congr
-- Module: Mathlib.ModelTheory.Equivalence
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α n
h : φ ⇔[T] ψ
⊢ ∀ (M : T.ModelType) (v : α → (↑M : Type (max (max u v) w))) (xs : Fin n → (↑M : Type (max (max u v) w))),
    ¬φ.Realize v xs ↔ ¬ψ.Realize v xs

Tactic:
exact fun M v xs => not_congr h.realize_bd_iff

Premises used: FirstOrder.Language.Theory.Iff.realize_bd_iff, not_congr
-- Module: Mathlib.ModelTheory.Equivalence
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ φ' ψ' : L.BoundedFormula α n
h : φ ⇔[T] ψ
h' : φ' ⇔[T] ψ'
simp_rw :
  ∀ (M : T.ModelType) (v : α → (↑M : Type (max (max u v) w))) (xs : Fin n → (↑M : Type (max (max u v) w))),
    φ.Realize v xs → φ'.Realize v xs ↔ ψ.Realize v xs → ψ'.Realize v xs
⊢ φ ⟹ φ' ⇔[T] ψ ⟹ ψ'

Tactic:
simp_rw [Theory.Iff, ModelsBoundedFormula, BoundedFormula.realize_iff,
    BoundedFormula.realize_imp]

Premises used: FirstOrder.Language.Theory.ModelsBoundedFormula, FirstOrder.Language.Theory.Iff, FirstOrder.Language.BoundedFormula.realize_iff, FirstOrder.Language.BoundedFormula.realize_imp
-- Module: Mathlib.ModelTheory.Equivalence
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ φ' ψ' : L.BoundedFormula α n
h : φ ⇔[T] ψ
h' : φ' ⇔[T] ψ'
⊢ ∀ (M : T.ModelType) (v : α → (↑M : Type (max (max u v) w))) (xs : Fin n → (↑M : Type (max (max u v) w))),
    φ.Realize v xs → φ'.Realize v xs ↔ ψ.Realize v xs → ψ'.Realize v xs

Tactic:
fun M v xs => imp_congr h.realize_bd_iff h'.realize_bd_iff

Premises used: imp_congr, FirstOrder.Language.Theory.Iff.realize_bd_iff
-- Module: Mathlib.ModelTheory.Equivalence
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ φ' ψ' : L.BoundedFormula α n
h : φ ⇔[T] ψ
h' : φ' ⇔[T] ψ'
⊢ ∀ (M : T.ModelType) (v : α → (↑M : Type (max (max u v) w))) (xs : Fin n → (↑M : Type (max (max u v) w))),
    φ.Realize v xs → φ'.Realize v xs ↔ ψ.Realize v xs → ψ'.Realize v xs

Tactic:
exact fun M v xs => imp_congr h.realize_bd_iff h'.realize_bd_iff

Premises used: imp_congr, FirstOrder.Language.Theory.Iff.realize_bd_iff
-- Module: Mathlib.ModelTheory.Equivalence
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ : L.BoundedFormula α n
M : T.ModelType
v : α → (↑M : Type (max (max u v) w))
xs : Fin n → (↑M : Type (max (max u v) w))
⊢ (φ ⇔ ∼∼φ).Realize v xs

Tactic:
simp
-- Module: Mathlib.ModelTheory.Equivalence
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α n
M : T.ModelType
v : α → (↑M : Type (max (max u v) w))
xs : Fin n → (↑M : Type (max (max u v) w))
⊢ (φ ⟹ ψ ⇔ ∼φ ⊔ ψ).Realize v xs

Tactic:
simp [imp_iff_not_or]

Premises used: imp_iff_not_or
-- Module: Mathlib.ModelTheory.Equivalence
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α n
M : T.ModelType
v : α → (↑M : Type (max (max u v) w))
xs : Fin n → (↑M : Type (max (max u v) w))
⊢ (φ ⊔ ψ ⇔ ∼(∼φ ⊓ ∼ψ)).Realize v xs

Tactic:
simp [imp_iff_not_or]

Premises used: imp_iff_not_or
-- Module: Mathlib.ModelTheory.Equivalence
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α n
M : T.ModelType
v : α → (↑M : Type (max (max u v) w))
xs : Fin n → (↑M : Type (max (max u v) w))
⊢ (φ ⊓ ψ ⇔ ∼(∼φ ⊔ ∼ψ)).Realize v xs

Tactic:
simp
-- Module: Mathlib.ModelTheory.Equivalence
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ : L.BoundedFormula α (n + 1)
M : T.ModelType
v : α → (↑M : Type (max (max u v) w))
xs : Fin n → (↑M : Type (max (max u v) w))
⊢ (∀' φ ⇔ ∼(∃' ∼φ)).Realize v xs

Tactic:
simp
-- Module: Mathlib.ModelTheory.Equivalence
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ : L.BoundedFormula α (n + 1)
M : T.ModelType
v : α → (↑M : Type (max (max u v) w))
xs : Fin n → (↑M : Type (max (max u v) w))
⊢ (∃' φ ⇔ ∼(∀' ∼φ)).Realize v xs

Tactic:
simp
-- Module: Mathlib.ModelTheory.Equivalence
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ : L.BoundedFormula α n
M : T.ModelType
v : α → (↑M : Type (max (max u v) w))
xs : Fin n → (↑M : Type (max (max u v) w))
rw : φ.Realize v xs ↔ (∀' liftAt 1 n φ).Realize v xs
rw₁ rw₂ : φ.Realize v xs ↔ φ.Realize v xs
⊢ (φ ⇔ ∀' liftAt 1 n φ).Realize v xs

Tactic:
rw [realize_iff, realize_all_liftAt_one_self]

Premises used: FirstOrder.Language.BoundedFormula.realize_all_liftAt_one_self, FirstOrder.Language.BoundedFormula.realize_iff
-- Module: Mathlib.ModelTheory.Equivalence
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ : L.BoundedFormula α n
M : T.ModelType
v : α → (↑M : Type (max (max u v) w))
xs : Fin n → (↑M : Type (max (max u v) w))
⊢ (φ ⊓ ∼φ ⇔ ⊥).Realize v xs

Tactic:
simp only [realize_iff, realize_inf, realize_not, and_not_self, realize_bot]

Premises used: FirstOrder.Language.BoundedFormula.realize_inf, FirstOrder.Language.BoundedFormula.realize_not, FirstOrder.Language.BoundedFormula.realize_bot, and_not_self, FirstOrder.Language.BoundedFormula.realize_iff
-- Module: Mathlib.ModelTheory.Equivalence
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ : L.BoundedFormula α n
M : T.ModelType
v : α → (↑M : Type (max (max u v) w))
xs : Fin n → (↑M : Type (max (max u v) w))
⊢ (φ ⊔ ∼φ ⇔ ⊤).Realize v xs

Tactic:
simp only [realize_iff, realize_sup, realize_not, realize_top, or_not]

Premises used: FirstOrder.Language.BoundedFormula.realize_not, or_not, FirstOrder.Language.BoundedFormula.realize_top, FirstOrder.Language.BoundedFormula.realize_iff, FirstOrder.Language.BoundedFormula.realize_sup
-- Module: Mathlib.ModelTheory.Equivalence
Goal:
L : Language
T : L.Theory
α : Type w
φ : L.Formula α
⊢ φ ⇔[T] φ.not.not

Tactic:
BoundedFormula.iff_not_not φ

Premises used: FirstOrder.Language.BoundedFormula.iff_not_not
-- Module: Mathlib.ModelTheory.Equivalence
Goal:
L : Language
T : L.Theory
α : Type w
φ ψ : L.Formula α
⊢ φ.imp ψ ⇔[T] φ.not ⊔ ψ

Tactic:
BoundedFormula.imp_iff_not_sup φ ψ

Premises used: FirstOrder.Language.BoundedFormula.imp_iff_not_sup
-- Module: Mathlib.ModelTheory.Equivalence
Goal:
L : Language
T : L.Theory
α : Type w
φ ψ : L.Formula α
⊢ φ ⊔ ψ ⇔[T] (φ.not ⊓ ψ.not).not

Tactic:
BoundedFormula.sup_iff_not_inf_not φ ψ

Premises used: FirstOrder.Language.BoundedFormula.sup_iff_not_inf_not
-- Module: Mathlib.ModelTheory.Equivalence
Goal:
L : Language
T : L.Theory
α : Type w
φ ψ : L.Formula α
⊢ φ ⊓ ψ ⇔[T] (φ.not ⊔ ψ.not).not

Tactic:
BoundedFormula.inf_iff_not_sup_not φ ψ

Premises used: FirstOrder.Language.BoundedFormula.inf_iff_not_sup_not
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
t' : Set M
h : t'.Finite
rcases : ∀ (t : Finset M) (h : (↑t : Set M).Finite), FG (LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑t : Set M))
⊢ FG (LowerAdjoint.toFun (u := SetLike.coe) (closure L) t')

Tactic:
rcases Finite.exists_finset_coe h with ⟨t, rfl⟩

Premises used: Set.Finite.exists_finset_coe, rfl
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
t : Finset M
h : (↑t : Set M).Finite
⊢ FG (LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑t : Set M))

Tactic:
⟨t, rfl⟩

Premises used: FirstOrder.Language.Substructure.FG, Exists.intro, rfl
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
t : Finset M
h : (↑t : Set M).Finite
⊢ FG (LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑t : Set M))

Tactic:
exact ⟨t, rfl⟩
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
N : L.Substructure M
rw :
  (∃ (S : Set M), S.Finite ∧ LowerAdjoint.toFun (u := SetLike.coe) (closure L) S = N) ↔
    ∃ (n : ℕ) (s : Fin n → M), LowerAdjoint.toFun (u := SetLike.coe) (closure L) (range s) = N
⊢ N.FG ↔ ∃ (n : ℕ) (s : Fin n → M), LowerAdjoint.toFun (u := SetLike.coe) (closure L) (range s) = N

Tactic:
rw [fg_def]

Premises used: FirstOrder.Language.Substructure.fg_def
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
N : L.Substructure M
mp :
  (∃ (S : Set M), S.Finite ∧ LowerAdjoint.toFun (u := SetLike.coe) (closure L) S = N) →
    ∃ (n : ℕ) (s : Fin n → M), LowerAdjoint.toFun (u := SetLike.coe) (closure L) (range s) = N
mpr :
  (∃ (n : ℕ) (s : Fin n → M), LowerAdjoint.toFun (u := SetLike.coe) (closure L) (range s) = N) →
    ∃ (S : Set M), S.Finite ∧ LowerAdjoint.toFun (u := SetLike.coe) (closure L) S = N
⊢ (∃ (S : Set M), S.Finite ∧ LowerAdjoint.toFun (u := SetLike.coe) (closure L) S = N) ↔
    ∃ (n : ℕ) (s : Fin n → M), LowerAdjoint.toFun (u := SetLike.coe) (closure L) (range s) = N

Tactic:
constructor
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
N : L.Substructure M
S : Set M
Sfin : S.Finite
hS : LowerAdjoint.toFun (u := SetLike.coe) (closure L) S = N
mp :
  ∀ (n : ℕ) (f : Fin n ↪ M) (Sfin : Set.Finite (α := M) (range (ι := Fin n) (⇑f : (a : Fin n) → M)))
    (hS : LowerAdjoint.toFun (u := SetLike.coe) (closure L) (range (ι := Fin n) (⇑f : (a : Fin n) → M)) = N),
    ∃ (n : ℕ) (s : Fin n → M), LowerAdjoint.toFun (u := SetLike.coe) (closure L) (range s) = N
⊢ ∃ (n : ℕ) (s : Fin n → M), LowerAdjoint.toFun (u := SetLike.coe) (closure L) (range s) = N

Tactic:
obtain ⟨n, f, rfl⟩ := Sfin.fin_embedding

Premises used: Set.Finite.fin_embedding, rfl
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
N : L.Substructure M
n : ℕ
f : Fin n ↪ M
Sfin : Set.Finite (α := M) (range (ι := Fin n) (⇑f : (a : Fin n) → M))
hS : LowerAdjoint.toFun (u := SetLike.coe) (closure L) (range (ι := Fin n) (⇑f : (a : Fin n) → M)) = N
⊢ ∃ (n : ℕ) (s : Fin n → M), LowerAdjoint.toFun (u := SetLike.coe) (closure L) (range s) = N

Tactic:
⟨n, f, hS⟩

Premises used: Exists.intro, DFunLike.coe
-- Module: Mathlib.ModelTheory.FinitelyGenerated
Goal:
L : Language
M : Type u_1
inst : L.Structure M
N : L.Substructure M
n : ℕ
f : Fin n ↪ M
Sfin : Set.Finite (α := M) (range (ι := Fin n) (⇑f : (a : Fin n) → M))
hS : LowerAdjoint.toFun (u := SetLike.coe) (closure L) (range (ι := Fin n) (⇑f : (a : Fin n) → M)) = N
⊢ ∃ (n : ℕ) (s : Fin n → M), LowerAdjoint.toFun (u := SetLike.coe) (closure L) (range s) = N

Tactic:
exact ⟨n, f, hS⟩