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
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)
⊢ 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
have h : Eq (α := (↑(↑S : Set M) : Type u_1) ⊕ Fin 1 → M)
  (Sum.elim (fun (a : (↑(↑S : Set M) : Type u_1)) ↦ (↑(L.con a) : M)) (Subtype.val (p := fun (x : M) ↦ x ∈ S) ∘ v'))
  ((⇑S.subtype : (a : ↥S) → M) ∘ Sum.elim (fun (a : (↑(↑S : Set M) : Type u_1)) ↦ (↑(L.con a) : ↥S)) v')
Tactic: convert! hv' using 1
-- 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)
⊢ Eq (α := (↑(↑S : Set M) : Type u_1) ⊕ Fin 1 → M)
    (Sum.elim (fun (a : (↑(↑S : Set M) : Type u_1)) ↦ (↑(L.con a) : M)) (Subtype.val (p := fun (x : M) ↦ x ∈ S) ∘ v'))
    ((⇑S.subtype : (a : ↥S) → M) ∘ Sum.elim (fun (a : (↑(↑S : Set M) : Type u_1)) ↦ (↑(L.con a) : ↥S)) v')
have h : ∀ (i : (↑(↑S : Set M) : Type u_1) ⊕ Fin 1),
  Sum.elim (fun (a : (↑(↑S : Set M) : Type u_1)) ↦ (↑(L.con a) : M)) (Subtype.val (p := fun (x : M) ↦ x ∈ S) ∘ v') i =
    ((⇑S.subtype : (a : ↥S) → M) ∘ Sum.elim (fun (a : (↑(↑S : Set M) : Type u_1)) ↦ (↑(L.con a) : ↥S)) v') i
Tactic: funext i
-- 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)
i : (↑(↑S : Set M) : Type u_1) ⊕ Fin 1
⊢ Sum.elim (fun (a : (↑(↑S : Set M) : Type u_1)) ↦ (↑(L.con a) : M)) (Subtype.val (p := fun (x : M) ↦ x ∈ S) ∘ v') i =
    ((⇑S.subtype : (a : ↥S) → M) ∘ Sum.elim (fun (a : (↑(↑S : Set M) : Type u_1)) ↦ (↑(L.con a) : ↥S)) v') i
have h : ∀ (val : (↑(↑S : Set M) : Type u_1)),
  Sum.elim (fun (a : (↑(↑S : Set M) : Type u_1)) ↦ (↑(L.con a) : M)) (Subtype.val (p := fun (x : M) ↦ x ∈ S) ∘ v')
      (Sum.inl val) =
    ((⇑S.subtype : (a : ↥S) → M) ∘ Sum.elim (fun (a : (↑(↑S : Set M) : Type u_1)) ↦ (↑(L.con a) : ↥S)) v') (Sum.inl val)
Tactic: cases i
Cleared hypotheses: i
-- 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)
i : (↑(↑S : Set M) : Type u_1) ⊕ Fin 1
h :
  ∀ (val : (↑(↑S : Set M) : Type u_1)),
    Sum.elim (fun (a : (↑(↑S : Set M) : Type u_1)) ↦ (↑(L.con a) : M)) (Subtype.val (p := fun (x : M) ↦ x ∈ S) ∘ v')
        (Sum.inl val) =
      ((⇑S.subtype : (a : ↥S) → M) ∘ Sum.elim (fun (a : (↑(↑S : Set M) : Type u_1)) ↦ (↑(L.con a) : ↥S)) v')
        (Sum.inl val)
⊢ Sum.elim (fun (a : (↑(↑S : Set M) : Type u_1)) ↦ (↑(L.con a) : M)) (Subtype.val (p := fun (x : M) ↦ x ∈ S) ∘ v') i =
    ((⇑S.subtype : (a : ↥S) → M) ∘ Sum.elim (fun (a : (↑(↑S : Set M) : Type u_1)) ↦ (↑(L.con a) : ↥S)) v') i
have h₁ : ∀ (val : Fin 1),
  Sum.elim (fun (a : (↑(↑S : Set M) : Type u_1)) ↦ (↑(L.con a) : M)) (Subtype.val (p := fun (x : M) ↦ x ∈ S) ∘ v')
      (Sum.inr val) =
    Function.comp (α := (↑(↑S : Set M) : Type u_1) ⊕ Fin 1) (⇑S.subtype : (a : ↥S) → M)
      (Sum.elim (fun (a : (↑(↑S : Set M) : Type u_1)) ↦ (↑(L.con a) : ↥S)) v') (Sum.inr val)
Tactic: cases i
Cleared hypotheses: i
-- 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'
⊢ (↑(v' 0) : M) ∈ D
have hv'' : φ.Realize (Subtype.val (p := fun (x : M) ↦ x ∈ S) ∘ v')
Tactic: have hv'' : φ.Realize (Subtype.val ∘ v') := by
    simp only [Formula.Realize, ← BoundedFormula.realize_constantsVarsEquiv,
      ← S.subtype.map_boundedFormula] at hv'
    simp only [Formula.Realize, ← BoundedFormula.realize_constantsVarsEquiv]
    convert! hv' using 1
    funext i
    cases i <;> rfl
-- 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'
hv'' : φ.Realize (Subtype.val (p := fun (x : M) ↦ x ∈ S) ∘ v')
⊢ (↑(v' 0) : M) ∈ D
have change : Membership.mem (γ := Set (Fin 1 → M)) {x : Fin 1 → M | x 0 ∈ D} (Subtype.val (p := fun (x : M) ↦ x ∈ S) ∘ v')
Tactic: change (Subtype.val ∘ v') ∈ {x | x 0 ∈ D}
-- Lean 4 proof step from Mathlib.ModelTheory.ElementarySubstructures (goal)
Goal:
L : Language
M : Type u_1
inst : L.Structure M
S : L.ElementarySubstructure M
⊢ MeetsDefinable.{u_1, u_2, u_3} (L := L) (↑S : Set M)
have rintro : ∀ (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
Tactic: classical
  rintro D ⟨x, hx⟩ ⟨φ, hφ⟩
  have hφx : φ.Realize ![x] := by
    simp [Set.ext_iff] at hφ
    simp [← hφ, hx]
  let ψ : L[[(S : Set M)]].Sentence := (φ.relabel Sum.inr).iExs
  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)
  have hψS : ψ.Realize S := by
    rwa [← Formula.realize_equivSentence_symm_con, ← S.subtype.map_formula,
      Formula.realize_equivSentence_symm]
  simp only [Sentence.Realize, SetLike.coe_sort_coe, Formula.realize_iExs,
    Formula.realize_relabel, Sum.elim_comp_inr, ψ] at hψS
  obtain ⟨v', hv'⟩ := hψS
  refine ⟨v' 0, ?_, by simp⟩
  have hv'' : φ.Realize (Subtype.val ∘ v') := by
    simp only [Formula.Realize, ← BoundedFormula.realize_constantsVarsEquiv,
      ← S.subtype.map_boundedFormula] at hv'
    simp only [Formula.Realize, ← BoundedFormula.realize_constantsVarsEquiv]
    convert! hv' using 1
    funext i
    cases i <;> rfl
  change (Subtype.val ∘ v') ∈ {x | x 0 ∈ D}
  simpa [hφ] using 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
rintro :
  ∀ (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
⊢ MeetsDefinable.{u_1, u_2, u_3} (L := L) (↑S : Set M)
have rintro₁ : ∀ (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]),
  (D ∩ (↑S : Set M)).Nonempty
Tactic: classical
  rintro D ⟨x, hx⟩ ⟨φ, hφ⟩
  have hφx : φ.Realize ![x] := by
    simp [Set.ext_iff] at hφ
    simp [← hφ, hx]
  let ψ : L[[(S : Set M)]].Sentence := (φ.relabel Sum.inr).iExs
  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)
  have hψS : ψ.Realize S := by
    rwa [← Formula.realize_equivSentence_symm_con, ← S.subtype.map_formula,
      Formula.realize_equivSentence_symm]
  simp only [Sentence.Realize, SetLike.coe_sort_coe, Formula.realize_iExs,
    Formula.realize_relabel, Sum.elim_comp_inr, ψ] at hψS
  obtain ⟨v', hv'⟩ := hψS
  refine ⟨v' 0, ?_, by simp⟩
  have hv'' : φ.Realize (Subtype.val ∘ v') := by
    simp only [Formula.Realize, ← BoundedFormula.realize_constantsVarsEquiv,
      ← S.subtype.map_boundedFormula] at hv'
    simp only [Formula.Realize, ← BoundedFormula.realize_constantsVarsEquiv]
    convert! hv' using 1
    funext i
    cases i <;> rfl
  change (Subtype.val ∘ v') ∈ {x | x 0 ∈ D}
  simpa [hφ] using 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
rintro :
  ∀ (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
rintro₁ rintro₂ :
  ∀ (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]),
    (D ∩ (↑S : Set M)).Nonempty
⊢ MeetsDefinable.{u_1, u_2, u_3} (L := L) (↑S : Set M)
have rintro₃ : ∀ (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]),
  let ψ : (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
Tactic: classical
  rintro D ⟨x, hx⟩ ⟨φ, hφ⟩
  have hφx : φ.Realize ![x] := by
    simp [Set.ext_iff] at hφ
    simp [← hφ, hx]
  let ψ : L[[(S : Set M)]].Sentence := (φ.relabel Sum.inr).iExs
  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)
  have hψS : ψ.Realize S := by
    rwa [← Formula.realize_equivSentence_symm_con, ← S.subtype.map_formula,
      Formula.realize_equivSentence_symm]
  simp only [Sentence.Realize, SetLike.coe_sort_coe, Formula.realize_iExs,
    Formula.realize_relabel, Sum.elim_comp_inr, ψ] at hψS
  obtain ⟨v', hv'⟩ := hψS
  refine ⟨v' 0, ?_, by simp⟩
  have hv'' : φ.Realize (Subtype.val ∘ v') := by
    simp only [Formula.Realize, ← BoundedFormula.realize_constantsVarsEquiv,
      ← S.subtype.map_boundedFormula] at hv'
    simp only [Formula.Realize, ← BoundedFormula.realize_constantsVarsEquiv]
    convert! hv' using 1
    funext i
    cases i <;> rfl
  change (Subtype.val ∘ v') ∈ {x | x 0 ∈ D}
  simpa [hφ] using 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
rintro :
  ∀ (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
rintro₁ rintro₂ :
  ∀ (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]),
    (D ∩ (↑S : Set M)).Nonempty
rintro₃ :
  ∀ (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]),
    let ψ : (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
⊢ MeetsDefinable.{u_1, u_2, u_3} (L := L) (↑S : Set M)
have rintro₄ : ∀ (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]),
  let ψ : (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
Tactic: classical
  rintro D ⟨x, hx⟩ ⟨φ, hφ⟩
  have hφx : φ.Realize ![x] := by
    simp [Set.ext_iff] at hφ
    simp [← hφ, hx]
  let ψ : L[[(S : Set M)]].Sentence := (φ.relabel Sum.inr).iExs
  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)
  have hψS : ψ.Realize S := by
    rwa [← Formula.realize_equivSentence_symm_con, ← S.subtype.map_formula,
      Formula.realize_equivSentence_symm]
  simp only [Sentence.Realize, SetLike.coe_sort_coe, Formula.realize_iExs,
    Formula.realize_relabel, Sum.elim_comp_inr, ψ] at hψS
  obtain ⟨v', hv'⟩ := hψS
  refine ⟨v' 0, ?_, by simp⟩
  have hv'' : φ.Realize (Subtype.val ∘ v') := by
    simp only [Formula.Realize, ← BoundedFormula.realize_constantsVarsEquiv,
      ← S.subtype.map_boundedFormula] at hv'
    simp only [Formula.Realize, ← BoundedFormula.realize_constantsVarsEquiv]
    convert! hv' using 1
    funext i
    cases i <;> rfl
  change (Subtype.val ∘ v') ∈ {x | x 0 ∈ D}
  simpa [hφ] using 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
rintro :
  ∀ (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
rintro₁ rintro₂ :
  ∀ (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]),
    (D ∩ (↑S : Set M)).Nonempty
rintro₃ :
  ∀ (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]),
    let ψ : (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
rintro₄ :
  ∀ (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]),
    let ψ : (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
⊢ MeetsDefinable.{u_1, u_2, u_3} (L := L) (↑S : Set M)
have rintro₅ : ∀ (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]),
  let ψ : (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
Tactic: classical
  rintro D ⟨x, hx⟩ ⟨φ, hφ⟩
  have hφx : φ.Realize ![x] := by
    simp [Set.ext_iff] at hφ
    simp [← hφ, hx]
  let ψ : L[[(S : Set M)]].Sentence := (φ.relabel Sum.inr).iExs
  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)
  have hψS : ψ.Realize S := by
    rwa [← Formula.realize_equivSentence_symm_con, ← S.subtype.map_formula,
      Formula.realize_equivSentence_symm]
  simp only [Sentence.Realize, SetLike.coe_sort_coe, Formula.realize_iExs,
    Formula.realize_relabel, Sum.elim_comp_inr, ψ] at hψS
  obtain ⟨v', hv'⟩ := hψS
  refine ⟨v' 0, ?_, by simp⟩
  have hv'' : φ.Realize (Subtype.val ∘ v') := by
    simp only [Formula.Realize, ← BoundedFormula.realize_constantsVarsEquiv,
      ← S.subtype.map_boundedFormula] at hv'
    simp only [Formula.Realize, ← BoundedFormula.realize_constantsVarsEquiv]
    convert! hv' using 1
    funext i
    cases i <;> rfl
  change (Subtype.val ∘ v') ∈ {x | x 0 ∈ D}
  simpa [hφ] using hv''
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
h :
  ∀ (t : L.Term α) (l : List (Sum.{u', u} α ((i : ℕ) × L.Functions i))),
    listDecode (t.listEncode ++ l) = t :: listDecode l
t : L.Term α
l : List (L.Term α)
lih : listDecode (flatMap listEncode l) = l
⊢ listDecode (flatMap listEncode (t :: l)) = t :: l
have cons : listDecode (t.listEncode ++ flatMap listEncode l) = t :: l
Tactic: rw [flatMap_cons, h t (l.flatMap listEncode), lih]
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
h :
  ∀ (t : L.Term α) (l : List (Sum.{u', u} α ((i : ℕ) × L.Functions i))),
    listDecode (t.listEncode ++ l) = t :: listDecode l
t : L.Term α
l : List (L.Term α)
lih : listDecode (flatMap listEncode l) = l
cons : listDecode (t.listEncode ++ flatMap listEncode l) = t :: l
⊢ listDecode (flatMap listEncode (t :: l)) = t :: l
have cons₁ : t :: listDecode (flatMap listEncode l) = t :: l
Tactic: rw [flatMap_cons, h t (l.flatMap listEncode), lih]
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
h :
  ∀ (t : L.Term α) (l : List (Sum.{u', u} α ((i : ℕ) × L.Functions i))),
    listDecode (t.listEncode ++ l) = t :: listDecode l
t : L.Term α
l : List (L.Term α)
lih : listDecode (flatMap listEncode l) = l
cons : listDecode (t.listEncode ++ flatMap listEncode l) = t :: l
cons₁ : t :: listDecode (flatMap listEncode l) = t :: l
⊢ listDecode (flatMap listEncode (t :: l)) = t :: l
have cons₂ : t :: l = t :: l
Tactic: rw [flatMap_cons, h t (l.flatMap listEncode), lih]
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
l : List (L.Term α)
h :
  ∀ (t : L.Term α) (l : List (Sum.{u', u} α ((i : ℕ) × L.Functions i))),
    listDecode (t.listEncode ++ l) = t :: listDecode l
⊢ listDecode (flatMap listEncode l) = l
have nil : Eq (α := List (L.Term α)) (listDecode (flatMap listEncode [])) []
Tactic: induction l with
    | nil => rfl
    | cons t l lih => rw [flatMap_cons, h t (l.flatMap listEncode), lih]
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
l : List (L.Term α)
h :
  ∀ (t : L.Term α) (l : List (Sum.{u', u} α ((i : ℕ) × L.Functions i))),
    listDecode (t.listEncode ++ l) = t :: listDecode l
nil : Eq (α := List (L.Term α)) (listDecode (flatMap listEncode [])) []
⊢ listDecode (flatMap listEncode l) = l
have cons : ∀ (t : L.Term α) (l : List (L.Term α)) (lih : listDecode (flatMap listEncode l) = l),
  listDecode (flatMap listEncode (t :: l)) = t :: l
Tactic: induction l with
    | nil => rfl
    | cons t l lih => rw [flatMap_cons, h t (l.flatMap listEncode), lih]
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
l : List (L.Term α)
⊢ listDecode (flatMap listEncode l) = l
have suffices : ∀ (t : L.Term α) (l : List (Sum.{u', u} α ((i : ℕ) × L.Functions i))),
  listDecode (t.listEncode ++ l) = t :: listDecode l
Tactic: suffices h : ∀ (t : L.Term α) (l : List (α ⊕ (Σ i, L.Functions i))),
      listDecode (t.listEncode ++ l) = t::listDecode l by
    induction l with
    | nil => rfl
    | cons t l lih => rw [flatMap_cons, h t (l.flatMap listEncode), lih]
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
l_1 : List (L.Term α)
a : α
l : List (Sum.{u', u} α ((i : ℕ) × L.Functions i))
⊢ listDecode (listEncode (var a) ++ l) = var a :: listDecode l
have var : listDecode ([Sum.inl a] ++ l) = var a :: listDecode l
Tactic: rw [listEncode, singleton_append, listDecode]
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
l_1 : List (L.Term α)
a : α
l : List (Sum.{u', u} α ((i : ℕ) × L.Functions i))
var : listDecode ([Sum.inl a] ++ l) = Language.var a :: listDecode l
⊢ listDecode (listEncode (Language.var a) ++ l) = Language.var a :: listDecode l
have var₁ : listDecode (Sum.inl a :: l) = Language.var a :: listDecode l
Tactic: rw [listEncode, singleton_append, listDecode]