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₁
ι : 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)
have refine₁ : ∀ (i : ι) (s : Finset ι), i ∉ s → ∀ (h : A.Definable L (s.inf f)), A.Definable L (f 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
-- 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.sup f)
have refine : ∀ (i : ι) (s : Finset ι), i ∉ s → ∀ (h : A.Definable L (s.sup f)), A.Definable L ((insert i s).sup f)
Tactic: refine Finset.induction definable_empty (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.sup f)
⊢ A.Definable L ((insert i s).sup f)
have rw : A.Definable L (f i ⊔ s.sup f)
Tactic: rw [Finset.sup_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.sup f)
have refine : ∀ (i : ι) (s : Finset ι), i ∉ s → ∀ (h : A.Definable L (s.sup f)), A.Definable L ((insert i s).sup f)
Tactic: classical
    refine Finset.induction definable_empty (fun i s _ h => ?_) s
    rw [Finset.sup_insert]
    exact (hf i).union h
-- 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 ι
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)
have refine₁ : ∀ (i : ι) (s : Finset ι), i ∉ s → ∀ (h : A.Definable L (s.sup f)), A.Definable L (f i ⊔ s.sup f)
Tactic: classical
    refine Finset.induction definable_empty (fun i s _ h => ?_) s
    rw [Finset.sup_insert]
    exact (hf i).union h
-- 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 ι
⊢ Definable.{u, v, w, u₁} A L (α := α) (⋂ i ∈ s, f i)
have rw : A.Definable L (s.inf f)
Tactic: rw [← Finset.inf_set_eq_iInter]
-- 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 ι
⊢ Definable.{u, v, w, u₁} A L (α := α) (⋃ i ∈ s, f i)
have rw : A.Definable L (s.sup f)
Tactic: rw [← Finset.sup_set_eq_biUnion]
-- 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
inst_1 : Finite ι
f : ι → Set (α → M)
hf : ∀ (i : ι), A.Definable L (f i)
⊢ Definable.{u, v, w, u₁} A L (α := α) (⋂ (i : ι), f i)
have haveI : ∀ (this : Fintype ι), Definable.{u, v, w, u₁} A L (α := α) (⋂ (i : ι), f i)
Tactic: haveI := Fintype.ofFinite ι
-- 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
inst_1 : Finite ι
f : ι → Set (α → M)
hf : ∀ (i : ι), A.Definable L (f i)
this : Fintype ι
⊢ Definable.{u, v, w, u₁} A L (α := α) (⋂ (i : ι), f i)
have h : ⋂ (i : ι), f i = Finset.inf Finset.univ f
Tactic: convert! definable_finset_inf hf Finset.univ using 1
-- 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
inst_1 : Finite ι
f : ι → Set (α → M)
hf : ∀ (i : ι), A.Definable L (f i)
⊢ Definable.{u, v, w, u₁} A L (α := α) (⋃ (i : ι), f i)
have haveI : ∀ (this : Fintype ι), Definable.{u, v, w, u₁} A L (α := α) (⋃ (i : ι), f i)
Tactic: haveI := Fintype.ofFinite ι
-- 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
inst_1 : Finite ι
f : ι → Set (α → M)
hf : ∀ (i : ι), A.Definable L (f i)
this : Fintype ι
⊢ Definable.{u, v, w, u₁} A L (α := α) (⋃ (i : ι), f i)
have h : ⋃ (i : ι), f i = Finset.sup Finset.univ f
Tactic: convert! definable_finset_sup hf Finset.univ using 1
-- 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)
hf : A.Definable L s
⊢ A.Definable L sᶜ
have rcases : ∀ (φ : (withConstants.{u, v, w} L (↑A : Type w)).Formula α) (hφ : s = setOf φ.Realize), A.Definable L sᶜ
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₁
s : Set (α → M)
φ : (withConstants.{u, v, w} L (↑A : Type w)).Formula α
hφ : s = setOf φ.Realize
⊢ A.Definable L sᶜ
have refine : sᶜ = setOf φ.not.Realize
Tactic: refine ⟨φ.not, ?_⟩
-- 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)
φ : (withConstants.{u, v, w} L (↑A : Type w)).Formula α
hφ : s = setOf φ.Realize
⊢ sᶜ = setOf φ.not.Realize
have h : ∀ (v : α → M), v ∈ sᶜ ↔ Membership.mem (γ := Set (α → M)) (setOf φ.not.Realize) v
Tactic: ext v
-- 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)
φ : (withConstants.{u, v, w} L (↑A : Type w)).Formula α
hφ : s = setOf φ.Realize
v : α → M
⊢ v ∈ sᶜ ↔ Membership.mem (γ := Set (α → M)) (setOf φ.not.Realize) v
have h : Membership.mem (γ := Set (α → M)) (setOf φ.Realize)ᶜ v ↔ Membership.mem (γ := Set (α → M)) (setOf φ.not.Realize) v
Tactic: rw [hφ, compl_setOf, mem_setOf, mem_setOf, Formula.realize_not]
-- 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)
φ : (withConstants.{u, v, w} L (↑A : Type w)).Formula α
hφ : s = setOf φ.Realize
v : α → M
h : Membership.mem (γ := Set (α → M)) (setOf φ.Realize)ᶜ v ↔ Membership.mem (γ := Set (α → M)) (setOf φ.not.Realize) v
⊢ v ∈ sᶜ ↔ Membership.mem (γ := Set (α → M)) (setOf φ.not.Realize) v
have h₁ : Membership.mem (γ := Set (α → M)) {a : α → M | ¬φ.Realize a} v ↔
  Membership.mem (γ := Set (α → M)) (setOf φ.not.Realize) v
Tactic: rw [hφ, compl_setOf, mem_setOf, mem_setOf, Formula.realize_not]
-- 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)
φ : (withConstants.{u, v, w} L (↑A : Type w)).Formula α
hφ : s = setOf φ.Realize
v : α → M
h : Membership.mem (γ := Set (α → M)) (setOf φ.Realize)ᶜ v ↔ Membership.mem (γ := Set (α → M)) (setOf φ.not.Realize) v
h₁ :
  Membership.mem (γ := Set (α → M)) {a : α → M | ¬φ.Realize a} v ↔
    Membership.mem (γ := Set (α → M)) (setOf φ.not.Realize) v
⊢ v ∈ sᶜ ↔ Membership.mem (γ := Set (α → M)) (setOf φ.not.Realize) v
have h₂ : ¬φ.Realize v ↔ Membership.mem (γ := Set (α → M)) (setOf φ.not.Realize) v
Tactic: rw [hφ, compl_setOf, mem_setOf, mem_setOf, Formula.realize_not]
-- 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)
φ : (withConstants.{u, v, w} L (↑A : Type w)).Formula α
hφ : s = setOf φ.Realize
v : α → M
h : Membership.mem (γ := Set (α → M)) (setOf φ.Realize)ᶜ v ↔ Membership.mem (γ := Set (α → M)) (setOf φ.not.Realize) v
h₁ :
  Membership.mem (γ := Set (α → M)) {a : α → M | ¬φ.Realize a} v ↔
    Membership.mem (γ := Set (α → M)) (setOf φ.not.Realize) v
h₂ : ¬φ.Realize v ↔ Membership.mem (γ := Set (α → M)) (setOf φ.not.Realize) v
⊢ v ∈ sᶜ ↔ Membership.mem (γ := Set (α → M)) (setOf φ.not.Realize) v
have h₃ : ¬φ.Realize v ↔ φ.not.Realize v
Tactic: rw [hφ, compl_setOf, mem_setOf, mem_setOf, Formula.realize_not]
-- 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)
φ : (withConstants.{u, v, w} L (↑A : Type w)).Formula α
hφ : s = setOf φ.Realize
v : α → M
h : Membership.mem (γ := Set (α → M)) (setOf φ.Realize)ᶜ v ↔ Membership.mem (γ := Set (α → M)) (setOf φ.not.Realize) v
h₁ :
  Membership.mem (γ := Set (α → M)) {a : α → M | ¬φ.Realize a} v ↔
    Membership.mem (γ := Set (α → M)) (setOf φ.not.Realize) v
h₂ : ¬φ.Realize v ↔ Membership.mem (γ := Set (α → M)) (setOf φ.not.Realize) v
h₃ : ¬φ.Realize v ↔ φ.not.Realize v
⊢ v ∈ sᶜ ↔ Membership.mem (γ := Set (α → M)) (setOf φ.not.Realize) v
have h₄ : ¬φ.Realize v ↔ ¬φ.Realize v
Tactic: rw [hφ, compl_setOf, mem_setOf, mem_setOf, Formula.realize_not]
-- 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 t : Set (α → M)
hs : A.Definable L s
ht : A.Definable L t
⊢ A.Definable L (s ⇨ t)
have rw : A.Definable L (t ⊔ sᶜ)
Tactic: rw [himp_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_1
f : α → β
s : Set (α → M)
h : A.Definable L s
⊢ Definable.{u, v, w, u_1} A L (α := β) ((fun (g : β → M) ↦ g ∘ f) ⁻¹' s)
have obtain : ∀ (φ : (withConstants.{u, v, w} L (↑A : Type w)).Formula α),
  Definable.{u, v, w, u_1} A L (α := β) (preimage (β := α → M) (fun (g : β → M) ↦ g ∘ f) (setOf φ.Realize))
Tactic: obtain ⟨φ, rfl⟩ := h
Cleared hypotheses: s, h
-- 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_1
f : α → β
φ : (withConstants.{u, v, w} L (↑A : Type w)).Formula α
⊢ Definable.{u, v, w, u_1} A L (α := β) (preimage (β := α → M) (fun (g : β → M) ↦ g ∘ f) (setOf φ.Realize))
have refine : Eq (α := Set (β → M)) (preimage (β := α → M) (fun (g : β → M) ↦ g ∘ f) (setOf φ.Realize))
  (setOf (Formula.relabel f φ).Realize)
Tactic: refine ⟨φ.relabel f, ?_⟩
-- 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_1
f : α → β
φ : (withConstants.{u, v, w} L (↑A : Type w)).Formula α
⊢ Eq (α := Set (β → M)) (preimage (β := α → M) (fun (g : β → M) ↦ g ∘ f) (setOf φ.Realize))
    (setOf (Formula.relabel f φ).Realize)
have h : ∀ (x : β → M),
  Membership.mem (γ := Set (β → M)) (preimage (β := α → M) (fun (g : β → M) ↦ g ∘ f) (setOf φ.Realize)) x ↔
    Membership.mem (γ := Set (β → M)) (setOf (Formula.relabel f φ).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₁
β : Type u_1
s : Set (β → M)
h : A.Definable L s
f : α ≃ β
⊢ Definable.{u, v, w, u₁} A L (α := α) ((fun (g : β → M) ↦ g ∘ (⇑f : (a : α) → β)) '' s)
have refine : Eq (α := Set (α → M)) ((fun (g : α → M) ↦ g ∘ (⇑f.symm : (a : β) → α)) ⁻¹' s)
  ((fun (g : β → M) ↦ g ∘ (⇑f : (a : α) → β)) '' s)
Tactic: refine (congr rfl ?_).mp (h.preimage_comp f.symm)
-- 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_1
s : Set (β → M)
h : A.Definable L s
f : α ≃ β
⊢ Eq (α := Set (α → M)) ((fun (g : α → M) ↦ g ∘ (⇑f.symm : (a : β) → α)) ⁻¹' s)
    ((fun (g : β → M) ↦ g ∘ (⇑f : (a : α) → β)) '' s)
have h₁ : Function.LeftInverse (fun (g : α → M) ↦ g ∘ (⇑f.symm : (a : β) → α)) fun (g : β → M) ↦ g ∘ (⇑f : (a : α) → β)
Tactic: rw [image_eq_preimage_of_inverse]
-- 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_1
s : Set (β → M)
h : A.Definable L s
f : α ≃ β
h₁ : Function.LeftInverse (fun (g : α → M) ↦ g ∘ (⇑f.symm : (a : β) → α)) fun (g : β → M) ↦ g ∘ (⇑f : (a : α) → β)
⊢ Eq (α := Set (α → M)) ((fun (g : α → M) ↦ g ∘ (⇑f.symm : (a : β) → α)) ⁻¹' s)
    ((fun (g : β → M) ↦ g ∘ (⇑f : (a : α) → β)) '' s)
have h₂ : Function.RightInverse (fun (g : α → M) ↦ g ∘ (⇑f.symm : (a : β) → α)) fun (g : β → M) ↦ g ∘ (⇑f : (a : α) → β)
Tactic: rw [image_eq_preimage_of_inverse]
-- 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_1
s : Set (β → M)
h : A.Definable L s
f : α ≃ β
i : β → M
⊢ (fun (g : α → M) ↦ (g ∘ (⇑f.symm : (a : β) → α) : β → M)) ((fun (g : β → M) ↦ (g ∘ (⇑f : (a : α) → β) : α → M)) i) = i
have h₁ : ∀ (b : β),
  (fun (g : α → M) ↦ (g ∘ (⇑f.symm : (a : β) → α) : β → M)) ((fun (g : β → M) ↦ (g ∘ (⇑f : (a : α) → β) : α → M)) i) b =
    i b
Tactic: ext b
-- 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_1
s : Set (β → M)
h : A.Definable L s
f : α ≃ β
i : α → M
⊢ (fun (g : β → M) ↦ (g ∘ (⇑f : (a : α) → β) : α → M)) ((fun (g : α → M) ↦ (g ∘ (⇑f.symm : (a : β) → α) : β → M)) i) = i
have h₂ : ∀ (a : α),
  (fun (g : β → M) ↦ (g ∘ (⇑f : (a : α) → β) : α → M)) ((fun (g : α → M) ↦ (g ∘ (⇑f.symm : (a : β) → α) : β → M)) i) a =
    i a
Tactic: ext 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)
⊢ A.Definable L s ↔ ∃ (A0 : Finset M), (↑A0 : Set M) ⊆ A ∧ (↑A0 : Set M).Definable L s
have mp : A.Definable L s → ∃ (A0 : Finset M), (↑A0 : Set M) ⊆ A ∧ (↑A0 : Set M).Definable L s
Tactic: constructor
-- 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)
mp : A.Definable L s → ∃ (A0 : Finset M), (↑A0 : Set M) ⊆ A ∧ (↑A0 : Set M).Definable L s
⊢ A.Definable L s ↔ ∃ (A0 : Finset M), (↑A0 : Set M) ⊆ A ∧ (↑A0 : Set M).Definable L s
have mpr : (∃ (A0 : Finset M), (↑A0 : Set M) ⊆ A ∧ (↑A0 : Set M).Definable L s) → A.Definable L s
Tactic: constructor
-- 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)
⊢ A.Definable L s → ∃ (A0 : Finset M), (↑A0 : Set M) ⊆ A ∧ (↑A0 : Set M).Definable L s
have mp : (∃ (φ : L.Formula (Sum.{w, u₁} (↑A : Type w) α)),
    s = {v : α → M | φ.Realize (Sum.elim (Subtype.val (p := fun (x : M) ↦ x ∈ A)) v)}) →
  ∃ (A0 : Finset M),
    (↑A0 : Set M) ⊆ A ∧
      ∃ (φ : L.Formula (Sum.{w, u₁} (↑(↑A0 : Set M) : Type w) α)),
        s = {v : α → M | φ.Realize (Sum.elim (Subtype.val (p := fun (x : M) ↦ x ∈ (↑A0 : Set M))) v)}
Tactic: simp only [definable_iff_exists_formula_sum]
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
φ : L.Formula (Sum.{w, u₁} (↑A : Type w) α)
A0 : Finset M := Finset.image (Subtype.val (p := fun (x : M) ↦ x ∈ A)) (BoundedFormula.freeVarFinset φ).toLeft
⊢ ∃ (A0 : Finset M),
    (↑A0 : Set M) ⊆ A ∧
      ∃ (φ_1 : L.Formula (Sum.{w, u₁} (↑(↑A0 : Set M) : Type w) α)),
        Eq (α := Set (α → M)) {v : α → M | φ.Realize (Sum.elim (Subtype.val (p := fun (x : M) ↦ x ∈ A)) v)}
          {v : α → M | φ_1.Realize (Sum.elim (Subtype.val (p := fun (x : M) ↦ x ∈ (↑A0 : Set M))) v)}
have mp : Eq (α := Set (α → M)) {v : α → M | φ.Realize (Sum.elim (Subtype.val (p := fun (x : M) ↦ x ∈ A)) v)}
  {v : α → M |
    Formula.Realize (α := Sum.{w, u₁} (↑(↑A0 : Set M) : Type w) α)
      (BoundedFormula.restrictFreeVar φ fun (x : ↥(BoundedFormula.freeVarFinset φ)) ↦
        Sum.casesOn (motive := fun (x : Sum.{w, u₁} (↑A : Type w) α) ↦
          x ∈ BoundedFormula.freeVarFinset φ → Sum.{w, u₁} (↑(↑A0 : Set M) : Type w) α) (↑x : (↑A : Type w) ⊕ α)
          (fun (x : (↑A : Type w)) (hx : Sum.inl x ∈ BoundedFormula.freeVarFinset φ) ↦
            Sum.inl (Subtype.mk (p := fun (x : M) ↦ x ∈ (↑A0 : Set M)) (↑x : M) sorry))
          (fun (x : α) (x_1 : Sum.inr x ∈ BoundedFormula.freeVarFinset φ) ↦ Sum.inr x) sorry)
      (Sum.elim (Subtype.val (p := fun (x : M) ↦ x ∈ (↑A0 : Set M))) v)}
Tactic: refine ⟨A0, by simp [A0], (φ.restrictFreeVar <| fun x => Sum.casesOn x.1
        (fun x hx => Sum.inl ⟨x, by simp [A0, hx]⟩) (fun x _ => Sum.inr x) x.2), ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
φ : L.Formula (Sum.{w, u₁} (↑A : Type w) α)
A0 : Finset M := Finset.image (Subtype.val (p := fun (x : M) ↦ x ∈ A)) (BoundedFormula.freeVarFinset φ).toLeft
⊢ Eq (α := Set (α → M)) {v : α → M | φ.Realize (Sum.elim (Subtype.val (p := fun (x : M) ↦ x ∈ A)) v)}
    {v : α → M |
      Formula.Realize (α := Sum.{w, u₁} (↑(↑A0 : Set M) : Type w) α)
        (BoundedFormula.restrictFreeVar φ fun (x : ↥(BoundedFormula.freeVarFinset φ)) ↦
          Sum.casesOn (motive := fun (x : Sum.{w, u₁} (↑A : Type w) α) ↦
            x ∈ BoundedFormula.freeVarFinset φ → Sum.{w, u₁} (↑(↑A0 : Set M) : Type w) α) (↑x : (↑A : Type w) ⊕ α)
            (fun (x : (↑A : Type w)) (hx : Sum.inl x ∈ BoundedFormula.freeVarFinset φ) ↦
              Sum.inl (Subtype.mk (p := fun (x : M) ↦ x ∈ (↑A0 : Set M)) (↑x : M) ⋯))
            (fun (x : α) (x_1 : Sum.inr x ∈ BoundedFormula.freeVarFinset φ) ↦ Sum.inr x) ⋯)
        (Sum.elim (Subtype.val (p := fun (x : M) ↦ x ∈ (↑A0 : Set M))) v)}
have mp : ∀ (x : α → M),
  Membership.mem (γ := Set (α → M)) {v : α → M | φ.Realize (Sum.elim (Subtype.val (p := fun (x : M) ↦ x ∈ A)) v)} x ↔
    Membership.mem (γ := Set (α → M))
      {v : α → M |
        Formula.Realize (α := Sum.{w, u₁} (↑(↑A0 : Set M) : Type w) α)
          (BoundedFormula.restrictFreeVar φ fun (x : ↥(BoundedFormula.freeVarFinset φ)) ↦
            Sum.casesOn (motive := fun (x : Sum.{w, u₁} (↑A : Type w) α) ↦
              x ∈ BoundedFormula.freeVarFinset φ → Sum.{w, u₁} (↑(↑A0 : Set M) : Type w) α) (↑x : (↑A : Type w) ⊕ α)
              (fun (x : (↑A : Type w)) (hx : Sum.inl x ∈ BoundedFormula.freeVarFinset φ) ↦
                Sum.inl (Subtype.mk (p := fun (x : M) ↦ x ∈ (↑A0 : Set M)) (↑x : M) sorry))
              (fun (x : α) (x_1 : Sum.inr x ∈ BoundedFormula.freeVarFinset φ) ↦ Sum.inr x) sorry)
          (Sum.elim (Subtype.val (p := fun (x : M) ↦ x ∈ (↑A0 : Set M))) 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₁
φ : L.Formula (Sum.{w, u₁} (↑A : Type w) α)
A0 : Finset M := Finset.image (Subtype.val (p := fun (x : M) ↦ x ∈ A)) (BoundedFormula.freeVarFinset φ).toLeft
x : α → M
⊢ Membership.mem (γ := Set (α → M)) {v : α → M | φ.Realize (Sum.elim (Subtype.val (p := fun (x : M) ↦ x ∈ A)) v)} x ↔
    Membership.mem (γ := Set (α → M))
      {v : α → M |
        Formula.Realize (α := Sum.{w, u₁} (↑(↑A0 : Set M) : Type w) α)
          (BoundedFormula.restrictFreeVar φ fun (x : ↥(BoundedFormula.freeVarFinset φ)) ↦
            Sum.casesOn (motive := fun (x : Sum.{w, u₁} (↑A : Type w) α) ↦
              x ∈ BoundedFormula.freeVarFinset φ → Sum.{w, u₁} (↑(↑A0 : Set M) : Type w) α) (↑x : (↑A : Type w) ⊕ α)
              (fun (x : (↑A : Type w)) (hx : Sum.inl x ∈ BoundedFormula.freeVarFinset φ) ↦
                Sum.inl (Subtype.mk (p := fun (x : M) ↦ x ∈ (↑A0 : Set M)) (↑x : M) ⋯))
              (fun (x : α) (x_1 : Sum.inr x ∈ BoundedFormula.freeVarFinset φ) ↦ Sum.inr x) ⋯)
          (Sum.elim (Subtype.val (p := fun (x : M) ↦ x ∈ (↑A0 : Set M))) v)}
      x
have mp : BoundedFormula.Realize φ (Sum.elim (Subtype.val (p := fun (x : M) ↦ x ∈ A)) x) default ↔
  BoundedFormula.Realize (α := Sum.{w, u₁} (↥A0) α)
    (BoundedFormula.restrictFreeVar φ fun (x : ↥(BoundedFormula.freeVarFinset φ)) ↦
      Sum.rec (motive := fun (x : Sum.{w, u₁} (↑A : Type w) α) ↦
        x ∈ BoundedFormula.freeVarFinset φ → Sum.{w, u₁} (↥A0) α)
        (fun (val : (↑A : Type w)) (hx : Sum.inl val ∈ BoundedFormula.freeVarFinset φ) ↦
          Sum.inl (Subtype.mk (p := fun (x : M) ↦ x ∈ (↑A0 : Set M)) (↑val : M) sorry))
        (fun (val : α) (x : Sum.inr val ∈ BoundedFormula.freeVarFinset φ) ↦ Sum.inr val) (↑x : (↑A : Type w) ⊕ α) sorry)
    (Sum.elim (Subtype.val (p := fun (x : M) ↦ x ∈ (↑A0 : Set M))) x) default
Tactic: simp only [Formula.Realize, mem_setOf_eq, Finset.coe_sort_coe]
-- 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)
⊢ A.Definable L s ↔ ∃ (A0 : Finset M), (↑A0 : Set M) ⊆ A ∧ (↑A0 : Set M).Definable L s
have mp : A.Definable L s → ∃ (A0 : Finset M), (↑A0 : Set M) ⊆ A ∧ (↑A0 : Set M).Definable L s
Tactic: classical
  constructor
  · simp only [definable_iff_exists_formula_sum]
    rintro ⟨φ, rfl⟩
    let A0 := (φ.freeVarFinset.toLeft).image Subtype.val
    refine ⟨A0, by simp [A0], (φ.restrictFreeVar <| fun x => Sum.casesOn x.1
        (fun x hx => Sum.inl ⟨x, by simp [A0, hx]⟩) (fun x _ => Sum.inr x) x.2), ?_⟩
    ext
    simp only [Formula.Realize, mem_setOf_eq, Finset.coe_sort_coe]
    exact iff_comm.1 <| BoundedFormula.realize_restrictFreeVar _ (by simp)
  · rintro ⟨A0, hA0, hd⟩
    exact Definable.mono hd hA0
-- 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)
mp : A.Definable L s → ∃ (A0 : Finset M), (↑A0 : Set M) ⊆ A ∧ (↑A0 : Set M).Definable L s
⊢ A.Definable L s ↔ ∃ (A0 : Finset M), (↑A0 : Set M) ⊆ A ∧ (↑A0 : Set M).Definable L s
have mpr : (∃ (A0 : Finset M), (↑A0 : Set M) ⊆ A ∧ (↑A0 : Set M).Definable L s) → A.Definable L s
Tactic: classical
  constructor
  · simp only [definable_iff_exists_formula_sum]
    rintro ⟨φ, rfl⟩
    let A0 := (φ.freeVarFinset.toLeft).image Subtype.val
    refine ⟨A0, by simp [A0], (φ.restrictFreeVar <| fun x => Sum.casesOn x.1
        (fun x hx => Sum.inl ⟨x, by simp [A0, hx]⟩) (fun x _ => Sum.inr x) x.2), ?_⟩
    ext
    simp only [Formula.Realize, mem_setOf_eq, Finset.coe_sort_coe]
    exact iff_comm.1 <| BoundedFormula.realize_restrictFreeVar _ (by simp)
  · rintro ⟨A0, hA0, hd⟩
    exact Definable.mono hd hA0
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
m : ℕ
s : Set (α ⊕ Fin m → M)
h : A.Definable L s
⊢ Definable.{u, v, w, u₁} A L (α := α) ((fun (g : α ⊕ Fin m → M) ↦ g ∘ Sum.inl) '' s)
have obtain : ∀ (φ : (withConstants.{u, v, w} L (↑A : Type w)).Formula (α ⊕ Fin m)),
  Definable.{u, v, w, u₁} A L (α := α) ((fun (g : α ⊕ Fin m → M) ↦ g ∘ Sum.inl) '' setOf φ.Realize)
Tactic: obtain ⟨φ, rfl⟩ := h
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
m : ℕ
φ : (withConstants.{u, v, w} L (↑A : Type w)).Formula (α ⊕ Fin m)
⊢ Definable.{u, v, w, u₁} A L (α := α) ((fun (g : α ⊕ Fin m → M) ↦ g ∘ Sum.inl) '' setOf φ.Realize)
have refine : Eq (α := Set (α → M)) ((fun (g : α ⊕ Fin m → M) ↦ g ∘ Sum.inl) '' setOf φ.Realize)
  (setOf (BoundedFormula.relabel id φ).exs.Realize)
Tactic: refine ⟨(BoundedFormula.relabel id φ).exs, ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
m : ℕ
φ : (withConstants.{u, v, w} L (↑A : Type w)).Formula (α ⊕ Fin m)
⊢ Eq (α := Set (α → M)) ((fun (g : α ⊕ Fin m → M) ↦ g ∘ Sum.inl) '' setOf φ.Realize)
    (setOf (BoundedFormula.relabel id φ).exs.Realize)
have h : ∀ (x : α → M),
  Membership.mem (γ := Set (α → M)) ((fun (g : α ⊕ Fin m → M) ↦ g ∘ Sum.inl) '' setOf φ.Realize) x ↔
    Membership.mem (γ := Set (α → M)) (setOf (BoundedFormula.relabel id φ).exs.Realize) x
Tactic: ext x