awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.ModelTheory.ElementaryMaps (goal)
Goal:
L : Language
M : Type u_1
N : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
        (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ x) a) →
      ∃ (b : M),
        BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
          (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ x) ((f : (a : M) → N) b))
n_1 : ℕ
φ_1 : L.BoundedFormula Empty n_1
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
ih :
  ∀ (xs : Fin (n + 1) → M),
    BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ
        (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N) default) ((⇑f : (a : M) → N) ∘ xs) ↔
      φ.Realize default xs
xs : Fin n → M
h :
  ∀ (a : N),
    BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ
      (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N) default)
      (Fin.snoc (α := fun (a : Fin n.succ) ↦ N) ((⇑f : (a : M) → N) ∘ xs) a)
a : M
⊢ BoundedFormula.Realize.{u_5, u_6, u_1, 0} (M := M) φ default (Fin.snoc (α := fun (a : Fin n.succ) ↦ M) xs a)
have refine_5 : BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ
  (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N) default)
  (Fin.snoc (α := fun (i : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ xs) ((f : (a : M) → N) a))
Tactic: rw [← ih, Fin.comp_snoc]
-- Lean 4 proof step from Mathlib.ModelTheory.ElementaryMaps (goal)
Goal:
L : Language
M : Type u_1
N : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
        (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ x) a) →
      ∃ (b : M),
        BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
          (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ x) ((f : (a : M) → N) b))
n_1 : ℕ
φ_1 : L.BoundedFormula Empty n_1
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
ih :
  ∀ (xs : Fin (n + 1) → M),
    BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ
        (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N) default) ((⇑f : (a : M) → N) ∘ xs) ↔
      φ.Realize default xs
xs : Fin n → M
⊢ (∀ (a : M),
      BoundedFormula.Realize.{u_5, u_6, u_1, 0} (M := M) φ default (Fin.snoc (α := fun (a : Fin n.succ) ↦ M) xs a)) →
    ∀ (a : N),
      BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ
        (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N) default)
        (Fin.snoc (α := fun (a : Fin n.succ) ↦ N) ((⇑f : (a : M) → N) ∘ xs) a)
have refine_5 : (∃ (a : N),
    ¬BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ
        (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N) default)
        (Fin.snoc (α := fun (a : Fin n.succ) ↦ N) ((⇑f : (a : M) → N) ∘ xs) a)) →
  ∃ (a : M),
    ¬BoundedFormula.Realize.{u_5, u_6, u_1, 0} (M := M) φ default (Fin.snoc (α := fun (a : Fin n.succ) ↦ M) xs a)
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.ModelTheory.ElementaryMaps (goal)
Goal:
L : Language
M : Type u_1
N : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
        (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ x) a) →
      ∃ (b : M),
        BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
          (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ x) ((f : (a : M) → N) b))
n_1 : ℕ
φ_1 : L.BoundedFormula Empty n_1
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
ih :
  ∀ (xs : Fin (n + 1) → M),
    BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ
        (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N) default) ((⇑f : (a : M) → N) ∘ xs) ↔
      φ.Realize default xs
xs : Fin n → M
a : N
ha :
  ¬BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ
      (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N) default)
      (Fin.snoc (α := fun (a : Fin n.succ) ↦ N) ((⇑f : (a : M) → N) ∘ xs) a)
⊢ ∃ (a : M),
    ¬BoundedFormula.Realize.{u_5, u_6, u_1, 0} (M := M) φ default (Fin.snoc (α := fun (a : Fin n.succ) ↦ M) xs a)
have refine_5 : ∀ (b : M)
  (hb :
    BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) (∼φ) default
      (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ xs) ((f : (a : M) → N) b))),
  ∃ (a : M),
    ¬BoundedFormula.Realize.{u_5, u_6, u_1, 0} (M := M) φ default (Fin.snoc (α := fun (a : Fin n.succ) ↦ M) xs a)
Tactic: obtain ⟨b, hb⟩ := htv n φ.not xs a (by
          rw [BoundedFormula.realize_not, ← Unique.eq_default (f ∘ default)]
          exact ha)
-- Lean 4 proof step from Mathlib.ModelTheory.ElementaryMaps (goal)
Goal:
L : Language
M : Type u_1
N : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
        (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ x) a) →
      ∃ (b : M),
        BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
          (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ x) ((f : (a : M) → N) b))
n_1 : ℕ
φ_1 : L.BoundedFormula Empty n_1
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
ih :
  ∀ (xs : Fin (n + 1) → M),
    BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ
        (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N) default) ((⇑f : (a : M) → N) ∘ xs) ↔
      φ.Realize default xs
xs : Fin n → M
a : N
ha :
  ¬BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ
      (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N) default)
      (Fin.snoc (α := fun (a : Fin n.succ) ↦ N) ((⇑f : (a : M) → N) ∘ xs) a)
b : M
hb :
  BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) (∼φ) default
    (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ xs) ((f : (a : M) → N) b))
⊢ ∃ (a : M),
    ¬BoundedFormula.Realize.{u_5, u_6, u_1, 0} (M := M) φ default (Fin.snoc (α := fun (a : Fin n.succ) ↦ M) xs a)
have refine_5 : ∀ (h : BoundedFormula.Realize.{u_5, u_6, u_1, 0} (M := M) φ default (Fin.snoc (α := fun (a : Fin n.succ) ↦ M) xs b)),
  BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ
      (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N) default)
      (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N)
        (Fin.snoc (α := fun (a : Fin n.succ) ↦ M) xs b)) =
    BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
      (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ xs) ((f : (a : M) → N) b))
Tactic: refine ⟨b, fun h => hb (Eq.mp ?_ ((ih _).2 h))⟩
-- Lean 4 proof step from Mathlib.ModelTheory.ElementaryMaps (goal)
Goal:
L : Language
M : Type u_1
N : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
        (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ x) a) →
      ∃ (b : M),
        BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
          (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ x) ((f : (a : M) → N) b))
n_1 : ℕ
φ_1 : L.BoundedFormula Empty n_1
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
ih :
  ∀ (xs : Fin (n + 1) → M),
    BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ
        (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N) default) ((⇑f : (a : M) → N) ∘ xs) ↔
      φ.Realize default xs
xs : Fin n → M
a : N
ha :
  ¬BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ
      (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N) default)
      (Fin.snoc (α := fun (a : Fin n.succ) ↦ N) ((⇑f : (a : M) → N) ∘ xs) a)
b : M
hb :
  BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) (∼φ) default
    (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ xs) ((f : (a : M) → N) b))
h : BoundedFormula.Realize.{u_5, u_6, u_1, 0} (M := M) φ default (Fin.snoc (α := fun (a : Fin n.succ) ↦ M) xs b)
⊢ BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ
      (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N) default)
      (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N)
        (Fin.snoc (α := fun (a : Fin n.succ) ↦ M) xs b)) =
    BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
      (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ xs) ((f : (a : M) → N) b))
have refine_5 : BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
    (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N) (Fin.snoc (α := fun (a : Fin n.succ) ↦ M) xs b)) =
  BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
    (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ xs) ((f : (a : M) → N) b))
Tactic: rw [Unique.eq_default (f ∘ default), Fin.comp_snoc]
-- Lean 4 proof step from Mathlib.ModelTheory.ElementaryMaps (goal)
Goal:
L : Language
M : Type u_1
N : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
        (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ x) a) →
      ∃ (b : M),
        BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
          (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ x) ((f : (a : M) → N) b))
n_1 : ℕ
φ_1 : L.BoundedFormula Empty n_1
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
ih :
  ∀ (xs : Fin (n + 1) → M),
    BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ
        (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N) default) ((⇑f : (a : M) → N) ∘ xs) ↔
      φ.Realize default xs
xs : Fin n → M
a : N
ha :
  ¬BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ
      (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N) default)
      (Fin.snoc (α := fun (a : Fin n.succ) ↦ N) ((⇑f : (a : M) → N) ∘ xs) a)
b : M
hb :
  BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) (∼φ) default
    (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ xs) ((f : (a : M) → N) b))
h : BoundedFormula.Realize.{u_5, u_6, u_1, 0} (M := M) φ default (Fin.snoc (α := fun (a : Fin n.succ) ↦ M) xs b)
refine_5 :
  BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
      (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N)
        (Fin.snoc (α := fun (a : Fin n.succ) ↦ M) xs b)) =
    BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
      (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ xs) ((f : (a : M) → N) b))
⊢ BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ
      (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N) default)
      (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N)
        (Fin.snoc (α := fun (a : Fin n.succ) ↦ M) xs b)) =
    BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
      (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ xs) ((f : (a : M) → N) b))
have refine_5₁ : BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
    (Fin.snoc (α := fun (i : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ xs) ((f : (a : M) → N) b)) =
  BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
    (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ xs) ((f : (a : M) → N) b))
Tactic: rw [Unique.eq_default (f ∘ default), Fin.comp_snoc]
-- Lean 4 proof step from Mathlib.ModelTheory.ElementarySubstructures (goal)
Goal:
L : Language
M : Type u_1
inst : L.Structure M
A : Set M
hA : MeetsDefinable.{u_1, u_2, u_3} (L := L) A
⊢ (↑(LowerAdjoint.toFun (u := SetLike.coe) (closure L) A) : Set M) = A
have refine : (↑(LowerAdjoint.toFun (u := SetLike.coe) (closure L) A) : Set M) ⊆ A
Tactic: refine Subset.antisymm ?_ subset_closure
-- Lean 4 proof step from Mathlib.ModelTheory.ElementarySubstructures (goal)
Goal:
L : Language
M : Type u_1
inst : L.Structure M
A : Set M
hA : MeetsDefinable.{u_1, u_2, u_3} (L := L) A
⊢ (↑(LowerAdjoint.toFun (u := SetLike.coe) (closure L) A) : Set M) ⊆ A
have rw : range (ι := Term.{u_2, u_3, u_1} L { x : M // x ∈ A }) (Term.realize (Subtype.val (p := fun (x : M) ↦ x ∈ A))) ⊆ A
Tactic: rw [coe_closure_eq_range_term_realize]
-- Lean 4 proof step from Mathlib.ModelTheory.ElementarySubstructures (goal)
Goal:
L : Language
M : Type u_1
inst : L.Structure M
A : Set M
hA : MeetsDefinable.{u_1, u_2, u_3} (L := L) A
x : M
hx :
  Membership.mem (γ := Set M)
    (range (ι := Term.{u_2, u_3, u_1} L { x : M // x ∈ A }) (Term.realize (Subtype.val (p := fun (x : M) ↦ x ∈ A)))) x
⊢ A.Definable₁ L {x}
have obtain : ∀ (t : Term.{u_2, u_3, u_1} L { x : M // x ∈ A }),
  A.Definable₁ L {Term.realize (Subtype.val (p := fun (x : M) ↦ x ∈ A)) t}
Tactic: obtain ⟨t, rfl⟩ := hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.ModelTheory.ElementarySubstructures (goal)
Goal:
L : Language
M : Type u_1
inst : L.Structure M
A : Set M
hA : MeetsDefinable.{u_1, u_2, u_3} (L := L) A
t : Term.{u_2, u_3, u_1} L { x : M // x ∈ A }
⊢ A.Definable₁ L {Term.realize (Subtype.val (p := fun (x : M) ↦ x ∈ A)) t}
have h : Eq.{u_1 + 1} (α := Set (Fin 1 → M))
  {x : Fin 1 → M | Membership.mem (γ := Set M) {Term.realize (Subtype.val (p := fun (x : M) ↦ x ∈ A)) t} (x 0)}
  (setOf (Formula.Realize (Term.equal (var 0) (Term.varsToConstants (Term.relabel Sum.inl t)))))
Tactic: use (Term.var 0).equal (t.relabel Sum.inl).varsToConstants
-- Lean 4 proof step from Mathlib.ModelTheory.ElementarySubstructures (hypothesis)
Goal:
L : Language
M : Type u_1
inst : L.Structure M
A : Set M
hA : MeetsDefinable.{u_1, u_2, u_3} (L := L) A
x : M
hx :
  Membership.mem (γ := Set M)
    (range (ι := Term.{u_2, u_3, u_1} L { x : M // x ∈ A }) (Term.realize (Subtype.val (p := fun (x : M) ↦ x ∈ A)))) x
⊢ x ∈ A
have this : A.Definable₁ L {x}
Tactic: have : A.Definable₁ L {x} := by
    obtain ⟨t, rfl⟩ := hx
    use (Term.var 0).equal (t.relabel Sum.inl).varsToConstants
    simp [Set.ext_iff]
-- Lean 4 proof step from Mathlib.ModelTheory.ElementarySubstructures (goal)
Goal:
L : Language
M : Type u_1
inst : L.Structure M
A : Set M
hA : MeetsDefinable.{u_1, u_2, u_3} (L := L) A
⊢ IsElementary (LowerAdjoint.toFun (u := SetLike.coe) (closure L) A)
have refine : ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → ↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) A))
  (a : M),
  BoundedFormula.Realize.{u_2, u_3, u_1, 0} (M := M) φ default
      (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ M)
        (Subtype.val (p := fun (x : M) ↦
            Membership.mem (γ := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) A) x) ∘
          x)
        a) →
    ∃ (b : ↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) A)),
      BoundedFormula.Realize.{u_2, u_3, u_1, 0} (M := M) φ default
        (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ M)
          (Subtype.val (p := fun (x : M) ↦
              Membership.mem (γ := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) A) x) ∘
            x)
          (↑b : M))
Tactic: refine isElementary_of_exists ((closure L).toFun A) ?_
-- Lean 4 proof step from Mathlib.ModelTheory.ElementarySubstructures (hypothesis)
Goal:
L : Language
M : Type u_1
inst : L.Structure M
A : Set M
hA : MeetsDefinable.{u_1, u_2, u_3} (L := L) A
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
x : Fin n → ↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) A)
a : M
hφ :
  BoundedFormula.Realize.{u_2, u_3, u_1, 0} (M := M) φ default
    (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ M)
      (Subtype.val (p := fun (x : M) ↦
          Membership.mem (γ := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) A) x) ∘
        x)
      a)
D : Set M :=
  {y : M |
    BoundedFormula.Realize.{u_2, u_3, u_1, 0} (M := M) φ default
      (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ M)
        (Subtype.val (p := fun (x : M) ↦
            Membership.mem (γ := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) A) x) ∘
          x)
        y)}
⊢ ∃ (b : ↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) A)),
    BoundedFormula.Realize.{u_2, u_3, u_1, 0} (M := M) φ default
      (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ M)
        (Subtype.val (p := fun (x : M) ↦
            Membership.mem (γ := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) A) x) ∘
          x)
        (↑b : M))
have hD_ne : D.Nonempty
Tactic: have hD_ne : D.Nonempty := ⟨a,hφ⟩
-- Lean 4 proof step from Mathlib.ModelTheory.ElementarySubstructures (goal)
Goal:
L : Language
M : Type u_1
inst : L.Structure M
A : Set M
hA : MeetsDefinable.{u_1, u_2, u_3} (L := L) A
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
x : Fin n → ↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) A)
a : M
hφ :
  BoundedFormula.Realize.{u_2, u_3, u_1, 0} (M := M) φ default
    (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ M)
      (Subtype.val (p := fun (x : M) ↦
          Membership.mem (γ := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) A) x) ∘
        x)
      a)
D : Set M :=
  {y : M |
    BoundedFormula.Realize.{u_2, u_3, u_1, 0} (M := M) φ default
      (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ M)
        (Subtype.val (p := fun (x : M) ↦
            Membership.mem (γ := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) A) x) ∘
          x)
        y)}
hD_ne : D.Nonempty
i : Fin (n + 1)
j : Fin n
⊢ (↑(x j) : M) ∈ A
have nth_rw : (↑(x j) : M) ∈ (↑(LowerAdjoint.toFun (u := SetLike.coe) (closure L) A) : Set M)
Tactic: nth_rw 1 [← hA.closure_eq_self]
-- Lean 4 proof step from Mathlib.ModelTheory.ElementarySubstructures (goal)
Goal:
L : Language
M : Type u_1
inst : L.Structure M
A : Set M
hA : MeetsDefinable.{u_1, u_2, u_3} (L := L) A
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
x : Fin n → ↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) A)
a : M
hφ :
  BoundedFormula.Realize.{u_2, u_3, u_1, 0} (M := M) φ default
    (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ M)
      (Subtype.val (p := fun (x : M) ↦
          Membership.mem (γ := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) A) x) ∘
        x)
      a)
D : Set M :=
  {y : M |
    BoundedFormula.Realize.{u_2, u_3, u_1, 0} (M := M) φ default
      (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ M)
        (Subtype.val (p := fun (x : M) ↦
            Membership.mem (γ := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) A) x) ∘
          x)
        y)}
hD_ne : D.Nonempty
⊢ ∃ (φ : (withConstants.{u_2, u_3, u_1} L (↑A : Type u_1)).Formula (Fin 1)),
    Eq.{u_1 + 1} (α := Set (Fin 1 → M)) {x : Fin 1 → M | x 0 ∈ D} (setOf φ.Realize)
have refine : Eq.{u_1 + 1} (α := Set (Fin 1 → M)) {x : Fin 1 → M | x 0 ∈ D}
  (setOf
    (Formula.Realize (L := withConstants.{u_2, u_3, u_1} L (↑A : Type u_1))
      (BoundedFormula.subst
        (Formula.relabel (Sum.elim Empty.elim id)
          (BoundedFormula.toFormula (LHom.onBoundedFormula (L.lhomWithConstants (↑A : Type u_1)) φ)))
        fun (i : Fin (n + 1)) ↦
        Fin.lastCases (motive := fun (x : Fin (n + 1)) ↦ (withConstants.{u_2, u_3, u_1} L (↑A : Type u_1)).Term (Fin 1))
          (var 0) (fun (j : Fin n) ↦ Constants.term (L.con (Subtype.mk (p := fun (x : M) ↦ x ∈ A) (↑(x j) : M) sorry))) i)))
Tactic: refine ⟨((L.lhomWithConstants A).onBoundedFormula φ).toFormula.relabel
      (Sum.elim Empty.elim id) |>.subst fun i => Fin.lastCases (Term.var 0)
        (fun j => (L.con ⟨x j, by
        nth_rw 1 [← hA.closure_eq_self]
        simp only [Subtype.coe_prop]
        ⟩).term) i, ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.ElementarySubstructures (goal)
Goal:
L : Language
M : Type u_1
inst : L.Structure M
A : Set M
hA : MeetsDefinable.{u_1, u_2, u_3} (L := L) A
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
x : Fin n → ↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) A)
a : M
hφ :
  BoundedFormula.Realize.{u_2, u_3, u_1, 0} (M := M) φ default
    (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ M)
      (Subtype.val (p := fun (x : M) ↦
          Membership.mem (γ := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) A) x) ∘
        x)
      a)
D : Set M :=
  {y : M |
    BoundedFormula.Realize.{u_2, u_3, u_1, 0} (M := M) φ default
      (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ M)
        (Subtype.val (p := fun (x : M) ↦
            Membership.mem (γ := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) A) x) ∘
          x)
        y)}
hD_ne : D.Nonempty
⊢ Eq.{u_1 + 1} (α := Set (Fin 1 → M)) {x : Fin 1 → M | x 0 ∈ D}
    (setOf
      (Formula.Realize (L := withConstants.{u_2, u_3, u_1} L (↑A : Type u_1))
        (BoundedFormula.subst
          (Formula.relabel (Sum.elim Empty.elim id)
            (BoundedFormula.toFormula (LHom.onBoundedFormula (L.lhomWithConstants (↑A : Type u_1)) φ)))
          fun (i : Fin (n + 1)) ↦
          Fin.lastCases (motive := fun (x : Fin (n + 1)) ↦
            (withConstants.{u_2, u_3, u_1} L (↑A : Type u_1)).Term (Fin 1)) (var 0)
            (fun (j : Fin n) ↦ Constants.term (L.con (Subtype.mk (p := fun (x : M) ↦ x ∈ A) (↑(x j) : M) ⋯))) i)))
have h : ∀ (v : Fin 1 → M),
  Membership.mem (γ := Set (Fin 1 → M)) {x : Fin 1 → M | x 0 ∈ D} v ↔
    Membership.mem (γ := Set (Fin 1 → M))
      (setOf
        (Formula.Realize (L := withConstants.{u_2, u_3, u_1} L (↑A : Type u_1))
          (BoundedFormula.subst
            (Formula.relabel (Sum.elim Empty.elim id)
              (BoundedFormula.toFormula (LHom.onBoundedFormula (L.lhomWithConstants (↑A : Type u_1)) φ)))
            fun (i : Fin (n + 1)) ↦
            Fin.lastCases (motive := fun (x : Fin (n + 1)) ↦
              (withConstants.{u_2, u_3, u_1} L (↑A : Type u_1)).Term (Fin 1)) (var 0)
              (fun (j : Fin n) ↦ Constants.term (L.con (Subtype.mk (p := fun (x : M) ↦ x ∈ A) (↑(x j) : M) sorry))) i)))
      v
Tactic: ext v