awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
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
⊢ Eq (α := 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)
          φ)))
    {v : α → M | Formula.Realize φ (Sum.elim (Subtype.val (p := fun (x : M) ↦ x ∈ A)) v)}
have h : ∀ (x : α → M),
  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: ext
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
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
⊢ 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
have 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
Tactic: simp only [BoundedFormula.constantsVarsEquiv, constantsOn,
    BoundedFormula.mapTermRelEquiv_symm_apply, mem_setOf_eq, Formula.Realize]
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
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
have 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
Tactic: refine BoundedFormula.realize_mapTermRel_id ?_ (fun _ _ _ => rfl)
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
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
⊢ 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
have 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
Tactic: simp only [Term.constantsVarsEquivLeft_symm_apply, Term.realize_varsToConstants,
    coe_con, Term.realize_relabel]
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
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
⊢ 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
have 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
Tactic: congr 1 with a
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
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
⊢ 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
have 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))
Tactic: rcases a with (_ | _) | _
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
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))
⊢ 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
have 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))
Tactic: rcases a with (_ | _) | _
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
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))
⊢ 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
have 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)
Tactic: rcases a with (_ | _) | _
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
Goal:
M : Type w
L : Language
inst : L.Structure M
α : Type u₁
s : Set (α → M)
⊢ Definable ∅ L s ↔ ∃ (φ : L.Formula α), s = setOf φ.Realize
have 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))
Tactic: rw [Definable, Equiv.exists_congr_left (LEquiv.addEmptyConstants L (∅ : Set M)).onFormula]
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
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
⊢ B.Definable L s
have 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
Tactic: rw [definable_iff_empty_definable_with_params] at *
Cleared hypotheses: hAs, hAB
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
⊢ Eq (α := Set (α → M)) ∅ (setOf (Formula.Realize (L := withConstants.{u, v, w} L (↑A : Type w)) ⊥))
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
⊢ Eq (α := Set (α → M)) univ (setOf (Formula.Realize (L := withConstants.{u, v, w} L (↑A : Type w)) ⊤))
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
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
⊢ A.Definable L (f ∩ g)
have rcases : ∀ (φ : (withConstants.{u, v, w} L (↑A : Type w)).Formula α), A.Definable L (setOf φ.Realize ∩ g)
Tactic: rcases hf with ⟨φ, rfl⟩
Cleared hypotheses: f, hf
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
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 α
⊢ A.Definable L (setOf φ.Realize ∩ g)
have rcases : ∀ (θ : (withConstants.{u, v, w} L (↑A : Type w)).Formula α), A.Definable L (setOf φ.Realize ∩ setOf θ.Realize)
Tactic: rcases hg with ⟨θ, rfl⟩
Cleared hypotheses: g, hg
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
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)
have refine : Eq (α := Set (α → M)) (setOf φ.Realize ∩ setOf θ.Realize) (setOf (φ ⊓ θ).Realize)
Tactic: refine ⟨φ ⊓ θ, ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
φ θ : (withConstants.{u, v, w} L (↑A : Type w)).Formula α
⊢ Eq (α := Set (α → M)) (setOf φ.Realize ∩ setOf θ.Realize) (setOf (φ ⊓ θ).Realize)
have h : ∀ (x : α → M),
  Membership.mem (γ := Set (α → M)) (setOf φ.Realize ∩ setOf θ.Realize) x ↔
    Membership.mem (γ := Set (α → M)) (setOf (φ ⊓ θ).Realize) x
Tactic: ext
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
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
⊢ A.Definable L (f ∪ g)
have rcases : ∀ (φ : (withConstants.{u, v, w} L (↑A : Type w)).Formula α) (hφ : f = setOf φ.Realize), A.Definable L (f ∪ g)
Tactic: rcases hf with ⟨φ, hφ⟩
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
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
⊢ A.Definable L (f ∪ g)
have rcases : ∀ (θ : (withConstants.{u, v, w} L (↑A : Type w)).Formula α) (hθ : g = setOf θ.Realize), A.Definable L (f ∪ g)
Tactic: rcases hg with ⟨θ, hθ⟩
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
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)
have refine : f ∪ g = setOf (φ ⊔ θ).Realize
Tactic: refine ⟨φ ⊔ θ, ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
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
⊢ f ∪ g = setOf (φ ⊔ θ).Realize
have h : ∀ (x : α → M), x ∈ f ∪ g ↔ Membership.mem (γ := Set (α → M)) (setOf (φ ⊔ θ).Realize) x
Tactic: ext
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
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
⊢ x ∈ f ∪ g ↔ Membership.mem (γ := Set (α → M)) (setOf (φ ⊔ θ).Realize) x
have h : x ∈ setOf φ.Realize ∪ 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]
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
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
⊢ x ∈ f ∪ g ↔ Membership.mem (γ := Set (α → M)) (setOf (φ ⊔ θ).Realize) x
have h₁ : Membership.mem (γ := Set (α → M)) (setOf φ.Realize ∪ setOf θ.Realize) x ↔
  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]
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
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
⊢ x ∈ f ∪ g ↔ Membership.mem (γ := Set (α → M)) (setOf (φ ⊔ θ).Realize) x
have h₂ : Membership.mem (γ := Set (α → M)) (setOf φ.Realize ∪ setOf θ.Realize) x ↔ (φ ⊔ θ).Realize x
Tactic: rw [hφ, hθ, mem_setOf_eq, Formula.realize_sup, mem_union, mem_setOf_eq, mem_setOf_eq]
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
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
⊢ x ∈ f ∪ g ↔ Membership.mem (γ := Set (α → M)) (setOf (φ ⊔ θ).Realize) x
have h₃ : Membership.mem (γ := Set (α → M)) (setOf φ.Realize ∪ setOf θ.Realize) x ↔ φ.Realize x ∨ θ.Realize x
Tactic: rw [hφ, hθ, mem_setOf_eq, Formula.realize_sup, mem_union, mem_setOf_eq, mem_setOf_eq]
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
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
⊢ x ∈ f ∪ g ↔ Membership.mem (γ := Set (α → M)) (setOf (φ ⊔ θ).Realize) x
have h₄ : Membership.mem (γ := Set (α → M)) (setOf φ.Realize) x ∨ Membership.mem (γ := Set (α → M)) (setOf θ.Realize) x ↔
  φ.Realize x ∨ θ.Realize x
Tactic: rw [hφ, hθ, mem_setOf_eq, Formula.realize_sup, mem_union, mem_setOf_eq, mem_setOf_eq]
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
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
⊢ x ∈ f ∪ g ↔ Membership.mem (γ := Set (α → M)) (setOf (φ ⊔ θ).Realize) x
have h₅ : φ.Realize x ∨ Membership.mem (γ := Set (α → M)) (setOf θ.Realize) x ↔ φ.Realize x ∨ θ.Realize x
Tactic: rw [hφ, hθ, mem_setOf_eq, Formula.realize_sup, mem_union, mem_setOf_eq, mem_setOf_eq]
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
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
⊢ x ∈ f ∪ g ↔ Membership.mem (γ := Set (α → M)) (setOf (φ ⊔ θ).Realize) x
have h₆ : φ.Realize x ∨ θ.Realize x ↔ φ.Realize x ∨ θ.Realize x
Tactic: rw [hφ, hθ, mem_setOf_eq, Formula.realize_sup, mem_union, mem_setOf_eq, mem_setOf_eq]
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
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)
have refine : ∀ (i : ι) (s : Finset ι), i ∉ s → ∀ (h : A.Definable L (s.inf f)), A.Definable L ((insert i s).inf f)
Tactic: refine Finset.induction definable_univ (fun i s _ h => ?_) s
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
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 ((insert i s).inf f)
have rw : A.Definable L (f i ⊓ s.inf f)
Tactic: rw [Finset.inf_insert]
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
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)
have refine : ∀ (i : ι) (s : Finset ι), i ∉ s → ∀ (h : A.Definable L (s.inf f)), A.Definable L ((insert i s).inf f)
Tactic: classical
    refine Finset.induction definable_univ (fun i s _ h => ?_) s
    rw [Finset.inf_insert]
    exact (hf i).inter h