awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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) ⋯))) i)))
      v
have 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)
      (v 0)) ↔
  BoundedFormula.Realize (L := withConstants.{u_2, u_3, u_1} L (↑A : Type u_1)) (M := M)
    (BoundedFormula.toFormula (LHom.onBoundedFormula (L.lhomWithConstants (↑A : Type u_1)) φ))
    (Function.comp (β := Fin (n + 1) ⊕ Fin 0)
      (Sum.elim
        (fun (a : Fin (n + 1)) ↦
          Term.realize (L := withConstants.{u_2, u_3, u_1} L (↑A : Type u_1)) v
            (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))) a))
        default)
      (Sum.inl ∘ Sum.elim Empty.elim id))
    default
Tactic: simp only [Fin.isValue, mem_setOf_eq, Formula.relabel, Formula.Realize,
      BoundedFormula.realize_subst, BoundedFormula.realize_relabel, Nat.add_zero, Fin.castAdd_zero,
      Fin.cast_refl, Function.comp_id, Fin.natAdd_zero, D]
-- 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
v : Fin 1 → M
⊢ Eq.{u_1 + 1} (α := Fin (n + 1) → M)
    (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)
      (v 0))
    (Function.comp (β := Fin (n + 1) ⊕ Fin 0)
        (Sum.elim
          (fun (a : Fin (n + 1)) ↦
            Term.realize (L := withConstants.{u_2, u_3, u_1} L (↑A : Type u_1)) v
              (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) ⋯))) a))
          default)
        (Sum.inl ∘ Sum.elim Empty.elim id) ∘
      Sum.inr)
have h : ∀ (i : Fin (n + 1)),
  Eq.{u_1 + 1} (α := M)
    (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)
        (v 0) i :
      M)
    ((Function.comp (β := Fin (n + 1) ⊕ Fin 0)
            (Sum.elim
              (fun (a : Fin (n + 1)) ↦
                Term.realize (L := withConstants.{u_2, u_3, u_1} L (↑A : Type u_1)) v
                  (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)))
                    a))
              default)
            (Sum.inl ∘ Sum.elim Empty.elim id) ∘
          Sum.inr)
        i :
      M)
Tactic: ext 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
v : Fin 1 → M
i : Fin (n + 1)
⊢ Eq.{u_1 + 1} (α := M)
    (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)
        (v 0) i :
      M)
    ((Function.comp (β := Fin (n + 1) ⊕ Fin 0)
            (Sum.elim
              (fun (a : Fin (n + 1)) ↦
                Term.realize (L := withConstants.{u_2, u_3, u_1} L (↑A : Type u_1)) v
                  (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) ⋯)))
                    a))
              default)
            (Sum.inl ∘ Sum.elim Empty.elim id) ∘
          Sum.inr)
        i :
      M)
have h : Eq.{u_1 + 1} (α := M)
  (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)
      (v 0) (Fin.last n) :
    M)
  ((Function.comp (β := Fin (n + 1) ⊕ Fin 0)
          (Sum.elim
            (fun (a : Fin (n + 1)) ↦
              Term.realize (L := withConstants.{u_2, u_3, u_1} L (↑A : Type u_1)) v
                (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))) a))
            default)
          (Sum.inl ∘ Sum.elim Empty.elim id) ∘
        Sum.inr)
      (Fin.last n) :
    M)
Tactic: cases i using Fin.lastCases
Cleared hypotheses: i
-- 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)}
hD_ne : D.Nonempty
⊢ ∃ (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 : A.Definable₁ L D
Tactic: have hD : A.Definable₁ L D := by
    simp only [Definable₁, Definable, Fin.isValue]
    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, ?_⟩
    ext v
    simp only [Fin.isValue, mem_setOf_eq, Formula.relabel, Formula.Realize,
      BoundedFormula.realize_subst, BoundedFormula.realize_relabel, Nat.add_zero, Fin.castAdd_zero,
      Fin.cast_refl, Function.comp_id, Fin.natAdd_zero, D]
    rw [← Formula.Realize, BoundedFormula.realize_toFormula, LHom.realize_onBoundedFormula]
    congr! 1
    ext i; cases i using Fin.lastCases <;> simp
-- 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
hD : A.Definable₁ L D
⊢ ∃ (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 obtain : ∀ (b : M) (hbD : b ∈ D) (hbA : b ∈ 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: obtain ⟨b, hbD, hbA⟩ := hA D hD_ne hD
-- 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
hD : A.Definable₁ L D
b : M
hbD : b ∈ D
hbA : b ∈ A
⊢ Membership.mem (γ := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) A) b
have rwa : ∀ (hbA : b ∈ (↑(LowerAdjoint.toFun (u := SetLike.coe) (closure L) A) : Set M)),
  Membership.mem (γ := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) A) b
Tactic: rwa [← hA.closure_eq_self] at hbA
Cleared hypotheses: hbA
-- Lean 4 proof step from Mathlib.ModelTheory.ElementarySubstructures (hypothesis)
Goal:
L : Language
M : Type u_1
inst : L.Structure M
S : L.ElementarySubstructure M
D : Set M
x : M
hx : x ∈ D
φ : (withConstants.{u_2, u_3, u_1} L (↑(↑S : Set M) : Type u_1)).Formula (Fin 1)
hφ : Eq.{u_1 + 1} (α := Set (Fin 1 → M)) {x : Fin 1 → M | x 0 ∈ D} (setOf φ.Realize)
⊢ φ.Realize ![x]
have hφ₁ : ∀ (x : Fin 1 → M), x 0 ∈ D ↔ φ.Realize x
Tactic: simp [Set.ext_iff] at hφ
Cleared hypotheses: hφ
-- Lean 4 proof step from Mathlib.ModelTheory.ElementarySubstructures (hypothesis)
Goal:
L : Language
M : Type u_1
inst : L.Structure M
S : L.ElementarySubstructure M
D : Set M
x : M
hx : x ∈ D
φ : (withConstants.{u_2, u_3, u_1} L (↑(↑S : Set M) : Type u_1)).Formula (Fin 1)
hφ : Eq.{u_1 + 1} (α := Set (Fin 1 → M)) {x : Fin 1 → M | x 0 ∈ D} (setOf φ.Realize)
⊢ (D ∩ (↑S : Set M)).Nonempty
have hφx : φ.Realize ![x]
Tactic: have hφx : φ.Realize ![x] := by
    simp [Set.ext_iff] at hφ
    simp [← hφ, hx]
-- Lean 4 proof step from Mathlib.ModelTheory.ElementarySubstructures (hypothesis)
Goal:
L : Language
M : Type u_1
inst : L.Structure M
S : L.ElementarySubstructure M
D : Set M
x : M
hx : x ∈ D
φ : (withConstants.{u_2, u_3, u_1} L (↑(↑S : Set M) : Type u_1)).Formula (Fin 1)
hφ : Eq.{u_1 + 1} (α := Set (Fin 1 → M)) {x : Fin 1 → M | x 0 ∈ D} (setOf φ.Realize)
hφx : φ.Realize ![x]
ψ : (withConstants.{u_2, u_3, u_1} L (↑(↑S : Set M) : Type u_1)).Sentence := iExs (Fin 1) (relabel Sum.inr φ)
⊢ (D ∩ (↑S : Set M)).Nonempty
have hψM : M ⊨ ψ
Tactic: have hψM : ψ.Realize M := by
    simpa only [Sentence.Realize, SetLike.coe_sort_coe, Formula.realize_iExs,
      Formula.realize_relabel, Sum.elim_comp_inr, ψ] using
        (⟨![x], hφx⟩ : ∃ w : Fin 1 → M, φ.Realize w)
-- Lean 4 proof step from Mathlib.ModelTheory.ElementarySubstructures (goal)
Goal:
L : Language
M : Type u_1
inst : L.Structure M
S : L.ElementarySubstructure M
D : Set M
x : M
hx : x ∈ D
φ : (withConstants.{u_2, u_3, u_1} L (↑(↑S : Set M) : Type u_1)).Formula (Fin 1)
hφ : Eq.{u_1 + 1} (α := Set (Fin 1 → M)) {x : Fin 1 → M | x 0 ∈ D} (setOf φ.Realize)
hφx : φ.Realize ![x]
ψ : (withConstants.{u_2, u_3, u_1} L (↑(↑S : Set M) : Type u_1)).Sentence := iExs (Fin 1) (relabel Sum.inr φ)
hψM : M ⊨ ψ
⊢ ↥S ⊨ ψ
have rwa : Realize.{u_2, u_3, u_1, u_1} (L := L) (M := ↥S)
  ((_root_.Equiv.symm equivSentence :
      (a : L[[(↑(↑S : Set M) : Type u_1)]].Sentence) → L.Formula (↑(↑S : Set M) : Type u_1))
    ψ)
  fun (a : (↑(↑S : Set M) : Type u_1)) ↦ (↑(L.con a) : ↥S)
Tactic: rwa [← Formula.realize_equivSentence_symm_con, ← S.subtype.map_formula,
      Formula.realize_equivSentence_symm]
-- Lean 4 proof step from Mathlib.ModelTheory.ElementarySubstructures (goal)
Goal:
L : Language
M : Type u_1
inst : L.Structure M
S : L.ElementarySubstructure M
D : Set M
x : M
hx : x ∈ D
φ : (withConstants.{u_2, u_3, u_1} L (↑(↑S : Set M) : Type u_1)).Formula (Fin 1)
hφ : Eq.{u_1 + 1} (α := Set (Fin 1 → M)) {x : Fin 1 → M | x 0 ∈ D} (setOf φ.Realize)
hφx : φ.Realize ![x]
ψ : (withConstants.{u_2, u_3, u_1} L (↑(↑S : Set M) : Type u_1)).Sentence := iExs (Fin 1) (relabel Sum.inr φ)
hψM : M ⊨ ψ
rwa :
  Realize.{u_2, u_3, u_1, u_1} (L := L) (M := ↥S)
    ((_root_.Equiv.symm equivSentence :
        (a : L[[(↑(↑S : Set M) : Type u_1)]].Sentence) → L.Formula (↑(↑S : Set M) : Type u_1))
      ψ)
    fun (a : (↑(↑S : Set M) : Type u_1)) ↦ (↑(L.con a) : ↥S)
⊢ ↥S ⊨ ψ
have rwa₁ : Realize.{u_2, u_3, u_1, u_1} (L := L) (M := M) (α := (↑(↑S : Set M) : Type u_1))
  ((_root_.Equiv.symm equivSentence :
      (a : L[[(↑(↑S : Set M) : Type u_1)]].Sentence) → L.Formula (↑(↑S : Set M) : Type u_1))
    ψ)
  (Function.comp (β := ↥S) (⇑S.subtype : (a : ↥S) → M) fun (a : (↑(↑S : Set M) : Type u_1)) ↦ (↑(L.con a) : ↥S))
Tactic: rwa [← Formula.realize_equivSentence_symm_con, ← S.subtype.map_formula,
      Formula.realize_equivSentence_symm]
-- Lean 4 proof step from Mathlib.ModelTheory.ElementarySubstructures (goal)
Goal:
L : Language
M : Type u_1
inst : L.Structure M
S : L.ElementarySubstructure M
D : Set M
x : M
hx : x ∈ D
φ : (withConstants.{u_2, u_3, u_1} L (↑(↑S : Set M) : Type u_1)).Formula (Fin 1)
hφ : Eq.{u_1 + 1} (α := Set (Fin 1 → M)) {x : Fin 1 → M | x 0 ∈ D} (setOf φ.Realize)
hφx : φ.Realize ![x]
ψ : (withConstants.{u_2, u_3, u_1} L (↑(↑S : Set M) : Type u_1)).Sentence := iExs (Fin 1) (relabel Sum.inr φ)
hψM : M ⊨ ψ
rwa :
  Realize.{u_2, u_3, u_1, u_1} (L := L) (M := ↥S)
    ((_root_.Equiv.symm equivSentence :
        (a : L[[(↑(↑S : Set M) : Type u_1)]].Sentence) → L.Formula (↑(↑S : Set M) : Type u_1))
      ψ)
    fun (a : (↑(↑S : Set M) : Type u_1)) ↦ (↑(L.con a) : ↥S)
rwa₁ :
  Realize.{u_2, u_3, u_1, u_1} (L := L) (M := M) (α := (↑(↑S : Set M) : Type u_1))
    ((_root_.Equiv.symm equivSentence :
        (a : L[[(↑(↑S : Set M) : Type u_1)]].Sentence) → L.Formula (↑(↑S : Set M) : Type u_1))
      ψ)
    (Function.comp (β := ↥S) (⇑S.subtype : (a : ↥S) → M) fun (a : (↑(↑S : Set M) : Type u_1)) ↦ (↑(L.con a) : ↥S))
⊢ ↥S ⊨ ψ
have rwa₂ : M ⊨ ψ
Tactic: rwa [← Formula.realize_equivSentence_symm_con, ← S.subtype.map_formula,
      Formula.realize_equivSentence_symm]
-- Lean 4 proof step from Mathlib.ModelTheory.ElementarySubstructures (hypothesis)
Goal:
L : Language
M : Type u_1
inst : L.Structure M
S : L.ElementarySubstructure M
D : Set M
x : M
hx : x ∈ D
φ : (withConstants.{u_2, u_3, u_1} L (↑(↑S : Set M) : Type u_1)).Formula (Fin 1)
hφ : Eq.{u_1 + 1} (α := Set (Fin 1 → M)) {x : Fin 1 → M | x 0 ∈ D} (setOf φ.Realize)
hφx : φ.Realize ![x]
ψ : (withConstants.{u_2, u_3, u_1} L (↑(↑S : Set M) : Type u_1)).Sentence := iExs (Fin 1) (relabel Sum.inr φ)
hψM : M ⊨ ψ
⊢ (D ∩ (↑S : Set M)).Nonempty
have hψS : ↥S ⊨ ψ
Tactic: have hψS : ψ.Realize S := by
    rwa [← Formula.realize_equivSentence_symm_con, ← S.subtype.map_formula,
      Formula.realize_equivSentence_symm]
-- Lean 4 proof step from Mathlib.ModelTheory.ElementarySubstructures (hypothesis)
Goal:
L : Language
M : Type u_1
inst : L.Structure M
S : L.ElementarySubstructure M
D : Set M
x : M
hx : x ∈ D
φ : (withConstants.{u_2, u_3, u_1} L (↑(↑S : Set M) : Type u_1)).Formula (Fin 1)
hφ : Eq.{u_1 + 1} (α := Set (Fin 1 → M)) {x : Fin 1 → M | x 0 ∈ D} (setOf φ.Realize)
hφx : φ.Realize ![x]
ψ : (withConstants.{u_2, u_3, u_1} L (↑(↑S : Set M) : Type u_1)).Sentence := iExs (Fin 1) (relabel Sum.inr φ)
hψM : M ⊨ ψ
hψS : ↥S ⊨ ψ
⊢ (D ∩ (↑S : Set M)).Nonempty
have hψS₁ : ∃ (i : Fin 1 → ↥S), φ.Realize i
Tactic: simp only [Sentence.Realize, SetLike.coe_sort_coe, Formula.realize_iExs,
    Formula.realize_relabel, Sum.elim_comp_inr, ψ] at hψS
Cleared hypotheses: hψS
-- Lean 4 proof step from Mathlib.ModelTheory.ElementarySubstructures (goal)
Goal:
L : Language
M : Type u_1
inst : L.Structure M
S : L.ElementarySubstructure M
D : Set M
x : M
hx : x ∈ D
φ : (withConstants.{u_2, u_3, u_1} L (↑(↑S : Set M) : Type u_1)).Formula (Fin 1)
hφ : Eq.{u_1 + 1} (α := Set (Fin 1 → M)) {x : Fin 1 → M | x 0 ∈ D} (setOf φ.Realize)
hφx : φ.Realize ![x]
ψ : (withConstants.{u_2, u_3, u_1} L (↑(↑S : Set M) : Type u_1)).Sentence := iExs (Fin 1) (relabel Sum.inr φ)
hψM : M ⊨ ψ
hψS : ∃ (i : Fin 1 → ↥S), φ.Realize i
⊢ (D ∩ (↑S : Set M)).Nonempty
have obtain : ∀ (v' : Fin 1 → ↥S) (hv' : φ.Realize v'), (D ∩ (↑S : Set M)).Nonempty
Tactic: obtain ⟨v', hv'⟩ := hψS
Cleared hypotheses: hψS
-- Lean 4 proof step from Mathlib.ModelTheory.ElementarySubstructures (goal)
Goal:
L : Language
M : Type u_1
inst : L.Structure M
S : L.ElementarySubstructure M
D : Set M
x : M
hx : x ∈ D
φ : (withConstants.{u_2, u_3, u_1} L (↑(↑S : Set M) : Type u_1)).Formula (Fin 1)
hφ : Eq.{u_1 + 1} (α := Set (Fin 1 → M)) {x : Fin 1 → M | x 0 ∈ D} (setOf φ.Realize)
hφx : φ.Realize ![x]
ψ : (withConstants.{u_2, u_3, u_1} L (↑(↑S : Set M) : Type u_1)).Sentence := iExs (Fin 1) (relabel Sum.inr φ)
hψM : M ⊨ ψ
v' : Fin 1 → ↥S
hv' : φ.Realize v'
⊢ (D ∩ (↑S : Set M)).Nonempty
have refine : (↑(v' 0) : M) ∈ D
Tactic: refine ⟨v' 0, ?_, by simp⟩
-- Lean 4 proof step from Mathlib.ModelTheory.ElementarySubstructures (hypothesis)
Goal:
L : Language
M : Type u_1
inst : L.Structure M
S : L.ElementarySubstructure M
D : Set M
x : M
hx : x ∈ D
φ : (withConstants.{u_2, u_3, u_1} L (↑(↑S : Set M) : Type u_1)).Formula (Fin 1)
hφ : Eq.{u_1 + 1} (α := Set (Fin 1 → M)) {x : Fin 1 → M | x 0 ∈ D} (setOf φ.Realize)
hφx : φ.Realize ![x]
ψ : (withConstants.{u_2, u_3, u_1} L (↑(↑S : Set M) : Type u_1)).Sentence := iExs (Fin 1) (relabel Sum.inr φ)
hψM : M ⊨ ψ
v' : Fin 1 → ↥S
hv' : φ.Realize v'
⊢ φ.Realize (Subtype.val (p := fun (x : M) ↦ x ∈ S) ∘ v')
have hv'₁ : BoundedFormula.Realize.{u_2, u_3, u_1, u_1} (L := L) (M := M) (α := (↑(↑S : Set M) : Type u_1) ⊕ Fin 1) (l := 0)
  ((BoundedFormula.constantsVarsEquiv :
      (a : L[[(↑(↑S : Set M) : Type u_1)]].BoundedFormula (Fin 1) 0) →
        L.BoundedFormula ((↑(↑S : Set M) : Type u_1) ⊕ Fin 1) 0)
    φ)
  ((⇑S.subtype : (a : ↥S) → M) ∘ Sum.elim (fun (a : (↑(↑S : Set M) : Type u_1)) ↦ (↑(L.con a) : ↥S)) v')
  (Function.comp (β := ↥S) (⇑S.subtype : (a : ↥S) → M) default)
Tactic: simp only [Formula.Realize, ← BoundedFormula.realize_constantsVarsEquiv,
      ← S.subtype.map_boundedFormula] at hv'
Cleared hypotheses: hv'
-- Lean 4 proof step from Mathlib.ModelTheory.ElementarySubstructures (goal)
Goal:
L : Language
M : Type u_1
inst : L.Structure M
S : L.ElementarySubstructure M
D : Set M
x : M
hx : x ∈ D
φ : (withConstants.{u_2, u_3, u_1} L (↑(↑S : Set M) : Type u_1)).Formula (Fin 1)
hφ : Eq.{u_1 + 1} (α := Set (Fin 1 → M)) {x : Fin 1 → M | x 0 ∈ D} (setOf φ.Realize)
hφx : φ.Realize ![x]
ψ : (withConstants.{u_2, u_3, u_1} L (↑(↑S : Set M) : Type u_1)).Sentence := iExs (Fin 1) (relabel Sum.inr φ)
hψM : M ⊨ ψ
v' : Fin 1 → ↥S
hv' :
  BoundedFormula.Realize.{u_2, u_3, u_1, u_1} (L := L) (M := M) (α := (↑(↑S : Set M) : Type u_1) ⊕ Fin 1) (l := 0)
    ((BoundedFormula.constantsVarsEquiv :
        (a : L[[(↑(↑S : Set M) : Type u_1)]].BoundedFormula (Fin 1) 0) →
          L.BoundedFormula ((↑(↑S : Set M) : Type u_1) ⊕ Fin 1) 0)
      φ)
    ((⇑S.subtype : (a : ↥S) → M) ∘ Sum.elim (fun (a : (↑(↑S : Set M) : Type u_1)) ↦ (↑(L.con a) : ↥S)) v')
    (Function.comp (β := ↥S) (⇑S.subtype : (a : ↥S) → M) default)
⊢ φ.Realize (Subtype.val (p := fun (x : M) ↦ x ∈ S) ∘ v')
have simp : BoundedFormula.Realize.{u_2, u_3, u_1, u_1} (L := L) (α := (↑(↑S : Set M) : Type u_1) ⊕ Fin 1) (l := 0)
  ((BoundedFormula.constantsVarsEquiv :
      (a : L[[(↑(↑S : Set M) : Type u_1)]].BoundedFormula (Fin 1) 0) →
        L.BoundedFormula ((↑(↑S : Set M) : Type u_1) ⊕ Fin 1) 0)
    φ)
  (Sum.elim (fun (a : (↑(↑S : Set M) : Type u_1)) ↦ (↑(L.con a) : M)) (Subtype.val (p := fun (x : M) ↦ x ∈ S) ∘ v'))
  default
Tactic: simp only [Formula.Realize, ← BoundedFormula.realize_constantsVarsEquiv]