awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
s : Set (α → M)
φ : L.BoundedFormula (Sum.{w, u₁} (↑A : Type w) α) 0
x : α → M
h :
  BoundedFormula.Realize (L := withConstants.{u, v, w} L (↑A : Type w)) (l := 0)
      (BoundedFormula.mapTermRel (L' := withConstants.{u, v, w} L (↑A : Type w)) (β := α) (g := fun (n : ℕ) ↦ n)
          (fun (n : ℕ) ↦
            (⇑(Equiv.symm Term.constantsVarsEquivLeft) :
              (a : L.Term (((↑A : Type w) ⊕ α) ⊕ Fin n)) → L[[(↑A : Type w)]].Term (α ⊕ Fin n)))
          (fun (n : ℕ) ↦
            (⇑(Equiv.symm (Equiv.sumEmpty (L.Relations n) Empty)) :
              (a : L.Relations n) → L[[(↑A : Type w)]].Relations n))
          (fun (x : ℕ) ↦ id) φ :
        (withConstants.{u, v, w} L (↑A : Type w)).BoundedFormula α 0)
      x (default : Fin 0 → M) ↔
    φ.Realize (Sum.elim (Subtype.val (p := fun (x : M) ↦ x ∈ A)) x) default
⊢ Membership.mem (γ := Set (α → M))
      (setOf
        (Formula.Realize (L := withConstants.{u, v, w} L (↑A : Type w))
          ((Equiv.symm BoundedFormula.constantsVarsEquiv :
              (a : L.BoundedFormula ((↑A : Type w) ⊕ α) 0) → L[[(↑A : Type w)]].BoundedFormula α 0)
            φ)))
      x ↔
    Membership.mem (γ := Set (α → M))
      {v : α → M | Formula.Realize φ (Sum.elim (Subtype.val (p := fun (x : M) ↦ x ∈ A)) v)} x

Tactic:
simp only [BoundedFormula.constantsVarsEquiv, constantsOn,
    BoundedFormula.mapTermRelEquiv_symm_apply, mem_setOf_eq, Formula.Realize]

Premises used: FirstOrder.Language.BoundedFormula.constantsVarsEquiv, Set.mem_setOf_eq, FirstOrder.Language.constantsOn, FirstOrder.Language.BoundedFormula.mapTermRelEquiv_symm_apply, FirstOrder.Language.Formula.Realize
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
s : Set (α → M)
φ : L.BoundedFormula (Sum.{w, u₁} (↑A : Type w) α) 0
x : α → M
⊢ BoundedFormula.Realize (L := withConstants.{u, v, w} L (↑A : Type w)) (l := 0)
      (BoundedFormula.mapTermRel (L' := withConstants.{u, v, w} L (↑A : Type w)) (β := α) (g := fun (n : ℕ) ↦ n)
          (fun (n : ℕ) ↦
            (⇑(Equiv.symm Term.constantsVarsEquivLeft) :
              (a : L.Term (((↑A : Type w) ⊕ α) ⊕ Fin n)) → L[[(↑A : Type w)]].Term (α ⊕ Fin n)))
          (fun (n : ℕ) ↦
            (⇑(Equiv.symm (Equiv.sumEmpty (L.Relations n) Empty)) :
              (a : L.Relations n) → L[[(↑A : Type w)]].Relations n))
          (fun (x : ℕ) ↦ id) φ :
        (withConstants.{u, v, w} L (↑A : Type w)).BoundedFormula α 0)
      x (default : Fin 0 → M) ↔
    φ.Realize (Sum.elim (Subtype.val (p := fun (x : M) ↦ x ∈ A)) x) default

Tactic:
BoundedFormula.realize_mapTermRel_id ?_ (fun _ _ _ => rfl)

Premises used: FirstOrder.Language.BoundedFormula.realize_mapTermRel_id, rfl
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
s : Set (α → M)
φ : L.BoundedFormula (Sum.{w, u₁} (↑A : Type w) α) 0
x : α → M
h :
  ∀ (n : ℕ) (t : L.Term (Sum.{w, u₁} (↑A : Type w) α ⊕ Fin n)) (xs : Fin n → M),
    Term.realize (L := withConstants.{u, v, w} L (↑A : Type w)) (Sum.elim x xs)
        ((Equiv.symm Term.constantsVarsEquivLeft :
            (a : L.Term (((↑A : Type w) ⊕ α) ⊕ Fin n)) → L[[(↑A : Type w)]].Term (α ⊕ Fin n))
          t) =
      Term.realize (Sum.elim (Sum.elim (Subtype.val (p := fun (x : M) ↦ x ∈ A)) x) xs) t
⊢ BoundedFormula.Realize (L := withConstants.{u, v, w} L (↑A : Type w)) (l := 0)
      (BoundedFormula.mapTermRel (L' := withConstants.{u, v, w} L (↑A : Type w)) (β := α) (g := fun (n : ℕ) ↦ n)
          (fun (n : ℕ) ↦
            (⇑(Equiv.symm Term.constantsVarsEquivLeft) :
              (a : L.Term (((↑A : Type w) ⊕ α) ⊕ Fin n)) → L[[(↑A : Type w)]].Term (α ⊕ Fin n)))
          (fun (n : ℕ) ↦
            (⇑(Equiv.symm (Equiv.sumEmpty (L.Relations n) Empty)) :
              (a : L.Relations n) → L[[(↑A : Type w)]].Relations n))
          (fun (x : ℕ) ↦ id) φ :
        (withConstants.{u, v, w} L (↑A : Type w)).BoundedFormula α 0)
      x (default : Fin 0 → M) ↔
    φ.Realize (Sum.elim (Subtype.val (p := fun (x : M) ↦ x ∈ A)) x) default

Tactic:
refine BoundedFormula.realize_mapTermRel_id ?_ (fun _ _ _ => rfl)

Premises used: FirstOrder.Language.BoundedFormula.realize_mapTermRel_id, rfl
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
s : Set (α → M)
φ : L.BoundedFormula (Sum.{w, u₁} (↑A : Type w) α) 0
x : α → M
n : ℕ
t : L.Term (Sum.{w, u₁} (↑A : Type w) α ⊕ Fin n)
xs : Fin n → M
h :
  Term.realize
      (Function.comp (β := Sum.{w, u₁} (↑A : Type w) (α ⊕ Fin n))
        (Sum.elim (fun (a : (↑A : Type w)) ↦ (↑a : M)) (Sum.elim x xs))
        (⇑(Equiv.sumAssoc (↑A : Type w) α (Fin n)) : (a : ((↑A : Type w) ⊕ α) ⊕ Fin n) → (↑A : Type w) ⊕ α ⊕ Fin n))
      t =
    Term.realize (Sum.elim (Sum.elim (Subtype.val (p := fun (x : M) ↦ x ∈ A)) x) xs) t
⊢ Term.realize (L := withConstants.{u, v, w} L (↑A : Type w)) (Sum.elim x xs)
      ((Equiv.symm Term.constantsVarsEquivLeft :
          (a : L.Term (((↑A : Type w) ⊕ α) ⊕ Fin n)) → L[[(↑A : Type w)]].Term (α ⊕ Fin n))
        t) =
    Term.realize (Sum.elim (Sum.elim (Subtype.val (p := fun (x : M) ↦ x ∈ A)) x) xs) t

Tactic:
simp only [Term.constantsVarsEquivLeft_symm_apply, Term.realize_varsToConstants,
    coe_con, Term.realize_relabel]

Premises used: FirstOrder.Language.coe_con, FirstOrder.Language.Term.realize_relabel, FirstOrder.Language.Term.constantsVarsEquivLeft_symm_apply, FirstOrder.Language.Term.realize_varsToConstants
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
s : Set (α → M)
φ : L.BoundedFormula (Sum.{w, u₁} (↑A : Type w) α) 0
x : α → M
n : ℕ
t : L.Term (Sum.{w, u₁} (↑A : Type w) α ⊕ Fin n)
xs : Fin n → M
h :
  ∀ (a : Sum.{w, u₁} (↑A : Type w) α ⊕ Fin n),
    Function.comp (β := Sum.{w, u₁} (↑A : Type w) (α ⊕ Fin n))
        (Sum.elim (fun (a : (↑A : Type w)) ↦ (↑a : M)) (Sum.elim x xs))
        (⇑(Equiv.sumAssoc (↑A : Type w) α (Fin n)) : (a : ((↑A : Type w) ⊕ α) ⊕ Fin n) → (↑A : Type w) ⊕ α ⊕ Fin n) a =
      Sum.elim (Sum.elim (Subtype.val (p := fun (x : M) ↦ x ∈ A)) x) xs a
⊢ Term.realize
      (Function.comp (β := Sum.{w, u₁} (↑A : Type w) (α ⊕ Fin n))
        (Sum.elim (fun (a : (↑A : Type w)) ↦ (↑a : M)) (Sum.elim x xs))
        (⇑(Equiv.sumAssoc (↑A : Type w) α (Fin n)) : (a : ((↑A : Type w) ⊕ α) ⊕ Fin n) → (↑A : Type w) ⊕ α ⊕ Fin n))
      t =
    Term.realize (Sum.elim (Sum.elim (Subtype.val (p := fun (x : M) ↦ x ∈ A)) x) xs) t

Tactic:
congr 1 with a
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
s : Set (α → M)
φ : L.BoundedFormula (Sum.{w, u₁} (↑A : Type w) α) 0
x : α → M
n : ℕ
t : L.Term (Sum.{w, u₁} (↑A : Type w) α ⊕ Fin n)
xs : Fin n → M
a : Sum.{w, u₁} (↑A : Type w) α ⊕ Fin n
h :
  ∀ (val : (↑A : Type w)),
    Function.comp (α := Sum.{w, u₁} (↑A : Type w) α ⊕ Fin n) (β := Sum.{w, u₁} (↑A : Type w) (α ⊕ Fin n))
        (Sum.elim (fun (a : (↑A : Type w)) ↦ (↑a : M)) (Sum.elim x xs))
        (⇑(Equiv.sumAssoc (↑A : Type w) α (Fin n)) : (a : ((↑A : Type w) ⊕ α) ⊕ Fin n) → (↑A : Type w) ⊕ α ⊕ Fin n)
        (Sum.inl (Sum.inl val)) =
      Sum.elim (Sum.elim (Subtype.val (p := fun (x : M) ↦ x ∈ A)) x) xs (Sum.inl (Sum.inl val))
h₁ :
  ∀ (val : α),
    Function.comp (α := Sum.{w, u₁} (↑A : Type w) α ⊕ Fin n) (β := Sum.{w, u₁} (↑A : Type w) (α ⊕ Fin n))
        (Sum.elim (fun (a : (↑A : Type w)) ↦ (↑a : M)) (Sum.elim x xs))
        (⇑(Equiv.sumAssoc (↑A : Type w) α (Fin n)) : (a : ((↑A : Type w) ⊕ α) ⊕ Fin n) → (↑A : Type w) ⊕ α ⊕ Fin n)
        (Sum.inl (Sum.inr val)) =
      Sum.elim (α := Sum.{w, u₁} (↑A : Type w) α) (Sum.elim (Subtype.val (p := fun (x : M) ↦ x ∈ A)) x) xs
        (Sum.inl (Sum.inr val))
h₂ :
  ∀ (val : Fin n),
    Function.comp (α := Sum.{w, u₁} (↑A : Type w) α ⊕ Fin n) (β := Sum.{w, u₁} (↑A : Type w) (α ⊕ Fin n))
        (Sum.elim (fun (a : (↑A : Type w)) ↦ (↑a : M)) (Sum.elim x xs))
        (⇑(Equiv.sumAssoc (↑A : Type w) α (Fin n)) : (a : ((↑A : Type w) ⊕ α) ⊕ Fin n) → (↑A : Type w) ⊕ α ⊕ Fin n)
        (Sum.inr val) =
      Sum.elim (α := Sum.{w, u₁} (↑A : Type w) α) (Sum.elim (Subtype.val (p := fun (x : M) ↦ x ∈ A)) x) xs (Sum.inr val)
⊢ Function.comp (β := Sum.{w, u₁} (↑A : Type w) (α ⊕ Fin n))
      (Sum.elim (fun (a : (↑A : Type w)) ↦ (↑a : M)) (Sum.elim x xs))
      (⇑(Equiv.sumAssoc (↑A : Type w) α (Fin n)) : (a : ((↑A : Type w) ⊕ α) ⊕ Fin n) → (↑A : Type w) ⊕ α ⊕ Fin n) a =
    Sum.elim (Sum.elim (Subtype.val (p := fun (x : M) ↦ x ∈ A)) x) xs a

Tactic:
rcases a with (_ | _) | _
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
s : Set (α → M)
φ : L.BoundedFormula (Sum.{w, u₁} (↑A : Type w) α) 0
x : α → M
n : ℕ
t : L.Term (Sum.{w, u₁} (↑A : Type w) α ⊕ Fin n)
xs : Fin n → M
val : (↑A : Type w)
⊢ Function.comp (α := Sum.{w, u₁} (↑A : Type w) α ⊕ Fin n) (β := Sum.{w, u₁} (↑A : Type w) (α ⊕ Fin n))
      (Sum.elim (fun (a : (↑A : Type w)) ↦ (↑a : M)) (Sum.elim x xs))
      (⇑(Equiv.sumAssoc (↑A : Type w) α (Fin n)) : (a : ((↑A : Type w) ⊕ α) ⊕ Fin n) → (↑A : Type w) ⊕ α ⊕ Fin n)
      (Sum.inl (Sum.inl val)) =
    Sum.elim (Sum.elim (Subtype.val (p := fun (x : M) ↦ x ∈ A)) x) xs (Sum.inl (Sum.inl val))

Tactic:
rfl
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
s : Set (α → M)
φ : L.BoundedFormula (Sum.{w, u₁} (↑A : Type w) α) 0
x : α → M
n : ℕ
t : L.Term (Sum.{w, u₁} (↑A : Type w) α ⊕ Fin n)
xs : Fin n → M
val : α
⊢ Function.comp (α := Sum.{w, u₁} (↑A : Type w) α ⊕ Fin n) (β := Sum.{w, u₁} (↑A : Type w) (α ⊕ Fin n))
      (Sum.elim (fun (a : (↑A : Type w)) ↦ (↑a : M)) (Sum.elim x xs))
      (⇑(Equiv.sumAssoc (↑A : Type w) α (Fin n)) : (a : ((↑A : Type w) ⊕ α) ⊕ Fin n) → (↑A : Type w) ⊕ α ⊕ Fin n)
      (Sum.inl (Sum.inr val)) =
    Sum.elim (α := Sum.{w, u₁} (↑A : Type w) α) (Sum.elim (Subtype.val (p := fun (x : M) ↦ x ∈ A)) x) xs
      (Sum.inl (Sum.inr val))

Tactic:
rfl
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
s : Set (α → M)
φ : L.BoundedFormula (Sum.{w, u₁} (↑A : Type w) α) 0
x : α → M
n : ℕ
t : L.Term (Sum.{w, u₁} (↑A : Type w) α ⊕ Fin n)
xs : Fin n → M
val : Fin n
⊢ Function.comp (α := Sum.{w, u₁} (↑A : Type w) α ⊕ Fin n) (β := Sum.{w, u₁} (↑A : Type w) (α ⊕ Fin n))
      (Sum.elim (fun (a : (↑A : Type w)) ↦ (↑a : M)) (Sum.elim x xs))
      (⇑(Equiv.sumAssoc (↑A : Type w) α (Fin n)) : (a : ((↑A : Type w) ⊕ α) ⊕ Fin n) → (↑A : Type w) ⊕ α ⊕ Fin n)
      (Sum.inr val) =
    Sum.elim (α := Sum.{w, u₁} (↑A : Type w) α) (Sum.elim (Subtype.val (p := fun (x : M) ↦ x ∈ A)) x) xs (Sum.inr val)

Tactic:
rfl
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
L : Language
inst : L.Structure M
α : Type u₁
s : Set (α → M)
rw :
  (∃ (φ : (withConstants.{u, v, w} L (↑∅ : Type w)).Formula α), s = setOf φ.Realize) ↔
    ∃ (b : (withConstants.{u, v, w} L (↑∅ : Type w)).Formula α),
      s =
        setOf
          (Formula.Realize.{u, v, w, u₁} (L := L)
            ((Equiv.symm (LEquiv.onFormula (LEquiv.addEmptyConstants L (↑∅ : Type w))) :
                (a : L[[(↑∅ : Type w)]].Formula α) → L.Formula α)
              b))
⊢ Definable ∅ L s ↔ ∃ (φ : L.Formula α), s = setOf φ.Realize

Tactic:
rw [Definable, Equiv.exists_congr_left (LEquiv.addEmptyConstants L (∅ : Set M)).onFormula]

Premises used: Equiv.exists_congr_left, Set.Definable, Set.Elem, FirstOrder.Language.LEquiv.addEmptyConstants, EmptyCollection.emptyCollection, FirstOrder.Language.LEquiv.onFormula
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
L : Language
inst : L.Structure M
α : Type u₁
s : Set (α → M)
⊢ (∃ (φ : (withConstants.{u, v, w} L (↑∅ : Type w)).Formula α), s = setOf φ.Realize) ↔
    ∃ (b : (withConstants.{u, v, w} L (↑∅ : Type w)).Formula α),
      s =
        setOf
          (Formula.Realize.{u, v, w, u₁} (L := L)
            ((Equiv.symm (LEquiv.onFormula (LEquiv.addEmptyConstants L (↑∅ : Type w))) :
                (a : L[[(↑∅ : Type w)]].Formula α) → L.Formula α)
              b))

Tactic:
simp
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
s : Set (α → M)
⊢ A.Definable L s ↔ Definable ∅ (withConstants.{u, v, w} L (↑A : Type w)) s

Tactic:
empty_definable_iff.symm

Premises used: Set.empty_definable_iff, Set.Definable, Iff.symm
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
B : Set M
s : Set (α → M)
hAs : A.Definable L s
hAB : A ⊆ B
rw :
  ∀ (hAs : Definable ∅ (withConstants.{u, v, w} L (↑A : Type w)) s) (hAB : A ⊆ B),
    Definable ∅ (withConstants.{u, v, w} L (↑B : Type w)) s
⊢ B.Definable L s

Tactic:
rw [definable_iff_empty_definable_with_params] at *

Premises used: Set.definable_iff_empty_definable_with_params
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
B : Set M
s : Set (α → M)
hAs : Definable ∅ (withConstants.{u, v, w} L (↑A : Type w)) s
hAB : A ⊆ B
⊢ Definable ∅ (withConstants.{u, v, w} L (↑B : Type w)) s

Tactic:
hAs.map_expansion (L.lhomWithConstantsMap (Set.inclusion hAB))

Premises used: FirstOrder.Language.lhomWithConstantsMap, Set.inclusion, Set.Definable.map_expansion
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
B : Set M
s : Set (α → M)
hAs : Definable ∅ (withConstants.{u, v, w} L (↑A : Type w)) s
hAB : A ⊆ B
⊢ Definable ∅ (withConstants.{u, v, w} L (↑B : Type w)) s

Tactic:
exact hAs.map_expansion (L.lhomWithConstantsMap (Set.inclusion hAB))

Premises used: FirstOrder.Language.lhomWithConstantsMap, Set.inclusion, Set.Definable.map_expansion
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
h :
  ∀ (x : α → M),
    Membership.mem (γ := Set (α → M)) ∅ x ↔
      Membership.mem (γ := Set (α → M)) (setOf (Formula.Realize (L := withConstants.{u, v, w} L (↑A : Type w)) ⊥)) x
⊢ Eq (α := Set (α → M)) ∅ (setOf (Formula.Realize (L := withConstants.{u, v, w} L (↑A : Type w)) ⊥))

Tactic:
ext
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
x : α → M
⊢ Membership.mem (γ := Set (α → M)) ∅ x ↔
    Membership.mem (γ := Set (α → M)) (setOf (Formula.Realize (L := withConstants.{u, v, w} L (↑A : Type w)) ⊥)) x

Tactic:
simp
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
h :
  ∀ (x : α → M),
    Membership.mem (γ := Set (α → M)) univ x ↔
      Membership.mem (γ := Set (α → M)) (setOf (Formula.Realize (L := withConstants.{u, v, w} L (↑A : Type w)) ⊤)) x
⊢ Eq (α := Set (α → M)) univ (setOf (Formula.Realize (L := withConstants.{u, v, w} L (↑A : Type w)) ⊤))

Tactic:
ext
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
x : α → M
⊢ Membership.mem (γ := Set (α → M)) univ x ↔
    Membership.mem (γ := Set (α → M)) (setOf (Formula.Realize (L := withConstants.{u, v, w} L (↑A : Type w)) ⊤)) x

Tactic:
simp
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
f g : Set (α → M)
hf : A.Definable L f
hg : A.Definable L g
rcases : ∀ (φ : (withConstants.{u, v, w} L (↑A : Type w)).Formula α), A.Definable L (setOf φ.Realize ∩ g)
⊢ A.Definable L (f ∩ g)

Tactic:
rcases hf with ⟨φ, rfl⟩

Premises used: rfl
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
g : Set (α → M)
hg : A.Definable L g
φ : (withConstants.{u, v, w} L (↑A : Type w)).Formula α
rcases : ∀ (θ : (withConstants.{u, v, w} L (↑A : Type w)).Formula α), A.Definable L (setOf φ.Realize ∩ setOf θ.Realize)
⊢ A.Definable L (setOf φ.Realize ∩ g)

Tactic:
rcases hg with ⟨θ, rfl⟩

Premises used: rfl
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
φ θ : (withConstants.{u, v, w} L (↑A : Type w)).Formula α
⊢ A.Definable L (setOf φ.Realize ∩ setOf θ.Realize)

Tactic:
⟨φ ⊓ θ, ?_⟩

Premises used: Set.Definable, Exists.intro, Min.min
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
φ θ : (withConstants.{u, v, w} L (↑A : Type w)).Formula α
refine : Eq (α := Set (α → M)) (setOf φ.Realize ∩ setOf θ.Realize) (setOf (φ ⊓ θ).Realize)
⊢ A.Definable L (setOf φ.Realize ∩ setOf θ.Realize)

Tactic:
refine ⟨φ ⊓ θ, ?_⟩
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
φ θ : (withConstants.{u, v, w} L (↑A : Type w)).Formula α
h :
  ∀ (x : α → M),
    Membership.mem (γ := Set (α → M)) (setOf φ.Realize ∩ setOf θ.Realize) x ↔
      Membership.mem (γ := Set (α → M)) (setOf (φ ⊓ θ).Realize) x
⊢ Eq (α := Set (α → M)) (setOf φ.Realize ∩ setOf θ.Realize) (setOf (φ ⊓ θ).Realize)

Tactic:
ext
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
φ θ : (withConstants.{u, v, w} L (↑A : Type w)).Formula α
x : α → M
⊢ Membership.mem (γ := Set (α → M)) (setOf φ.Realize ∩ setOf θ.Realize) x ↔
    Membership.mem (γ := Set (α → M)) (setOf (φ ⊓ θ).Realize) x

Tactic:
simp
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
f g : Set (α → M)
hf : A.Definable L f
hg : A.Definable L g
rcases : ∀ (φ : (withConstants.{u, v, w} L (↑A : Type w)).Formula α) (hφ : f = setOf φ.Realize), A.Definable L (f ∪ g)
⊢ A.Definable L (f ∪ g)

Tactic:
rcases hf with ⟨φ, hφ⟩
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
f g : Set (α → M)
hg : A.Definable L g
φ : (withConstants.{u, v, w} L (↑A : Type w)).Formula α
hφ : f = setOf φ.Realize
rcases : ∀ (θ : (withConstants.{u, v, w} L (↑A : Type w)).Formula α) (hθ : g = setOf θ.Realize), A.Definable L (f ∪ g)
⊢ A.Definable L (f ∪ g)

Tactic:
rcases hg with ⟨θ, hθ⟩
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
f g : Set (α → M)
φ : (withConstants.{u, v, w} L (↑A : Type w)).Formula α
hφ : f = setOf φ.Realize
θ : (withConstants.{u, v, w} L (↑A : Type w)).Formula α
hθ : g = setOf θ.Realize
⊢ A.Definable L (f ∪ g)

Tactic:
⟨φ ⊔ θ, ?_⟩

Premises used: Set.Definable, Max.max, Exists.intro
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
f g : Set (α → M)
φ : (withConstants.{u, v, w} L (↑A : Type w)).Formula α
hφ : f = setOf φ.Realize
θ : (withConstants.{u, v, w} L (↑A : Type w)).Formula α
hθ : g = setOf θ.Realize
refine : f ∪ g = setOf (φ ⊔ θ).Realize
⊢ A.Definable L (f ∪ g)

Tactic:
refine ⟨φ ⊔ θ, ?_⟩
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
f g : Set (α → M)
φ : (withConstants.{u, v, w} L (↑A : Type w)).Formula α
hφ : f = setOf φ.Realize
θ : (withConstants.{u, v, w} L (↑A : Type w)).Formula α
hθ : g = setOf θ.Realize
h : ∀ (x : α → M), x ∈ f ∪ g ↔ Membership.mem (γ := Set (α → M)) (setOf (φ ⊔ θ).Realize) x
⊢ f ∪ g = setOf (φ ⊔ θ).Realize

Tactic:
ext
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
f g : Set (α → M)
φ : (withConstants.{u, v, w} L (↑A : Type w)).Formula α
hφ : f = setOf φ.Realize
θ : (withConstants.{u, v, w} L (↑A : Type w)).Formula α
hθ : g = setOf θ.Realize
x : α → M
h : x ∈ setOf φ.Realize ∪ g ↔ Membership.mem (γ := Set (α → M)) (setOf (φ ⊔ θ).Realize) x
h₁ :
  Membership.mem (γ := Set (α → M)) (setOf φ.Realize ∪ setOf θ.Realize) x ↔
    Membership.mem (γ := Set (α → M)) (setOf (φ ⊔ θ).Realize) x
h₂ : Membership.mem (γ := Set (α → M)) (setOf φ.Realize ∪ setOf θ.Realize) x ↔ (φ ⊔ θ).Realize x
h₃ : Membership.mem (γ := Set (α → M)) (setOf φ.Realize ∪ setOf θ.Realize) x ↔ φ.Realize x ∨ θ.Realize x
h₄ :
  Membership.mem (γ := Set (α → M)) (setOf φ.Realize) x ∨ Membership.mem (γ := Set (α → M)) (setOf θ.Realize) x ↔
    φ.Realize x ∨ θ.Realize x
h₅ : φ.Realize x ∨ Membership.mem (γ := Set (α → M)) (setOf θ.Realize) x ↔ φ.Realize x ∨ θ.Realize x
h₆ h₇ : φ.Realize x ∨ θ.Realize x ↔ φ.Realize x ∨ θ.Realize x
⊢ x ∈ f ∪ g ↔ Membership.mem (γ := Set (α → M)) (setOf (φ ⊔ θ).Realize) x

Tactic:
rw [hφ, hθ, mem_setOf_eq, Formula.realize_sup, mem_union, mem_setOf_eq, mem_setOf_eq]

Premises used: Set.mem_union, Set.mem_setOf_eq, FirstOrder.Language.Formula.realize_sup
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
ι : Type u_2
f : ι → Set (α → M)
hf : ∀ (i : ι), A.Definable L (f i)
s : Finset ι
⊢ A.Definable L (s.inf f)

Tactic:
Finset.induction definable_univ (fun i s _ h => ?_) s

Premises used: Finset.induction
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
ι : Type u_2
f : ι → Set (α → M)
hf : ∀ (i : ι), A.Definable L (f i)
s : Finset ι
refine : ∀ (i : ι) (s : Finset ι), i ∉ s → ∀ (h : A.Definable L (s.inf f)), A.Definable L ((insert i s).inf f)
⊢ A.Definable L (s.inf f)

Tactic:
refine Finset.induction definable_univ (fun i s _ h => ?_) s
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
ι : Type u_2
f : ι → Set (α → M)
hf : ∀ (i : ι), A.Definable L (f i)
s_1 : Finset ι
i : ι
s : Finset ι
h_1 : i ∉ s
h : A.Definable L (s.inf f)
rw : A.Definable L (f i ⊓ s.inf f)
⊢ A.Definable L ((insert i s).inf f)

Tactic:
rw [Finset.inf_insert]

Premises used: Finset.inf_insert
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
ι : Type u_2
f : ι → Set (α → M)
hf : ∀ (i : ι), A.Definable L (f i)
s_1 : Finset ι
i : ι
s : Finset ι
h_1 : i ∉ s
h : A.Definable L (s.inf f)
⊢ A.Definable L (f i ⊓ s.inf f)

Tactic:
(hf i).inter h

Premises used: Set.Definable.inter
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
ι : Type u_2
f : ι → Set (α → M)
hf : ∀ (i : ι), A.Definable L (f i)
s_1 : Finset ι
i : ι
s : Finset ι
h_1 : i ∉ s
h : A.Definable L (s.inf f)
⊢ A.Definable L (f i ⊓ s.inf f)

Tactic:
exact (hf i).inter h

Premises used: Set.Definable.inter
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
ι : Type u_2
f : ι → Set (α → M)
hf : ∀ (i : ι), A.Definable L (f i)
s : Finset ι
refine : ∀ (i : ι) (s : Finset ι), i ∉ s → ∀ (h : A.Definable L (s.inf f)), A.Definable L ((insert i s).inf f)
refine₁ : ∀ (i : ι) (s : Finset ι), i ∉ s → ∀ (h : A.Definable L (s.inf f)), A.Definable L (f i ⊓ s.inf f)
⊢ A.Definable L (s.inf f)

Tactic:
classical
    refine Finset.induction definable_univ (fun i s _ h => ?_) s
    rw [Finset.inf_insert]
    exact (hf i).inter h

Premises used: Finset.inf_insert
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
ι : Type u_2
f : ι → Set (α → M)
hf : ∀ (i : ι), A.Definable L (f i)
s : Finset ι
⊢ A.Definable L (s.sup f)

Tactic:
Finset.induction definable_empty (fun i s _ h => ?_) s

Premises used: Finset.induction
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
ι : Type u_2
f : ι → Set (α → M)
hf : ∀ (i : ι), A.Definable L (f i)
s : Finset ι
refine : ∀ (i : ι) (s : Finset ι), i ∉ s → ∀ (h : A.Definable L (s.sup f)), A.Definable L ((insert i s).sup f)
⊢ A.Definable L (s.sup f)

Tactic:
refine Finset.induction definable_empty (fun i s _ h => ?_) s