awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.ModelTheory.DirectLimit (goal)
Goal:
L : Language
ι : Type v
inst : Preorder ι
G : ι → Type w
inst_1 : (i : ι) → Structure.{u_2, u_3, w} L (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst_2 : Nonempty ι
inst_3 : IsDirectedOrder ι
M : Type u_1
inst_4 : L.Structure M
S : OrderHom.{v, u_1} ι (L.Substructure M)
⊢ ∀
    (x :
      DirectLimit.{v, u_1, u_2, u_3} (L := L) (fun (i : ι) ↦ ↥((S : (a : ι) → L.Substructure M) i : L.Substructure M))
        fun (x x_1 : ι) (h : x ≤ x_1) ↦ Substructure.inclusion ⋯),
    Membership.mem.{u_1, u_1} (α := M) (γ := L.Substructure M) (⨆ (i : ι), (S : (a : ι) → L.Substructure M) i)
      ((liftInclusion S :
            (a :
                DirectLimit (fun (i : ι) ↦ ↥((S : (a : ι) → L.Substructure M) i)) fun (x x_1 : ι) (h : x ≤ x_1) ↦
                  Substructure.inclusion ⋯) →
              M)
          x :
        M)
have simp : ∀
  (x :
    DirectLimit.{v, u_1, u_2, u_3} (L := L) (fun (i : ι) ↦ ↥((S : (a : ι) → L.Substructure M) i : L.Substructure M))
      fun (x x_1 : ι) (h : x ≤ x_1) ↦ Substructure.inclusion sorry),
  ∃ (y :
    DirectLimit.{v, u_1, u_2, u_3} (L := L) (fun (i : ι) ↦ ↥((S : (a : ι) → L.Substructure M) i : L.Substructure M))
      fun (x x_1 : ι) (h : x ≤ x_1) ↦ Substructure.inclusion sorry),
    Eq.{u_1 + 1} (α := M)
      ((liftInclusion S :
            (a :
                DirectLimit (fun (i : ι) ↦ ↥((S : (a : ι) → L.Substructure M) i)) fun (x x_1 : ι) (h : x ≤ x_1) ↦
                  Substructure.inclusion sorry) →
              M)
          y :
        M)
      ((liftInclusion S :
            (a :
                DirectLimit (fun (i : ι) ↦ ↥((S : (a : ι) → L.Substructure M) i)) fun (x x_1 : ι) (h : x ≤ x_1) ↦
                  Substructure.inclusion sorry) →
              M)
          x :
        M)
Tactic: simp only [← rangeLiftInclusion, Hom.mem_range, Embedding.coe_toHom]
-- Lean 4 proof step from Mathlib.ModelTheory.DirectLimit (goal)
Goal:
L : Language
ι : Type v
inst : Preorder ι
G : ι → Type w
inst_1 : (i : ι) → Structure.{u_2, u_3, w} L (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst_2 : Nonempty ι
inst_3 : IsDirectedOrder ι
M : Type u_1
inst_4 : L.Structure M
S : OrderHom.{v, u_1} ι (L.Substructure M)
x w :
  DirectLimit.{v, u_1, u_2, u_3} (L := L) (fun (i : ι) ↦ ↥((S : (a : ι) → L.Substructure M) i : L.Substructure M))
    fun (x x_1 : ι) (h : x ≤ x_1) ↦ Substructure.inclusion ⋯
⊢ ∃ (y :
    DirectLimit.{v, u_1, u_2, u_3} (L := L) (fun (i : ι) ↦ ↥((S : (a : ι) → L.Substructure M) i : L.Substructure M))
      fun (x x_1 : ι) (h : x ≤ x_1) ↦ Substructure.inclusion ⋯),
    Eq.{u_1 + 1} (α := M)
      ((liftInclusion S :
            (a :
                DirectLimit (fun (i : ι) ↦ ↥((S : (a : ι) → L.Substructure M) i)) fun (x x_1 : ι) (h : x ≤ x_1) ↦
                  Substructure.inclusion ⋯) →
              M)
          y :
        M)
      ((liftInclusion S :
            (a :
                DirectLimit (fun (i : ι) ↦ ↥((S : (a : ι) → L.Substructure M) i)) fun (x x_1 : ι) (h : x ≤ x_1) ↦
                  Substructure.inclusion ⋯) →
              M)
          x :
        M)
have h : Eq.{u_1 + 1} (α := M)
  ((liftInclusion S :
        (a :
            DirectLimit (fun (i : ι) ↦ ↥((S : (a : ι) → L.Substructure M) i)) fun (x x_1 : ι) (h : x ≤ x_1) ↦
              Substructure.inclusion sorry) →
          M)
      x :
    M)
  ((liftInclusion S :
        (a :
            DirectLimit (fun (i : ι) ↦ ↥((S : (a : ι) → L.Substructure M) i)) fun (x x_1 : ι) (h : x ≤ x_1) ↦
              Substructure.inclusion sorry) →
          M)
      x :
    M)
Tactic: use x
-- Lean 4 proof step from Mathlib.ModelTheory.DirectLimit (hypothesis)
Goal:
L : Language
ι : Type v
inst : Preorder ι
G : ι → Type w
inst_1 : (i : ι) → Structure.{u_2, u_3, w} L (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst_2 : Nonempty ι
inst_3 : IsDirectedOrder ι
M : Type u_1
inst_4 : L.Structure M
S : OrderHom.{v, u_1} ι (L.Substructure M)
⊢ (DirectLimit.{v, u_1, u_2, u_3} (L := L) (fun (i : ι) ↦ ↥((S : (a : ι) → L.Substructure M) i : L.Substructure M))
      fun (x x_1 : ι) (h : x ≤ x_1) ↦ Substructure.inclusion ⋯) ≃[L]
    ↥(iSup.{u_1, v + 1} (ι := ι) (⇑S : (a : ι) → L.Substructure M))
have liftInclusion_in_sup : ∀
  (x :
    DirectLimit.{v, u_1, u_2, u_3} (L := L) (fun (i : ι) ↦ ↥((S : (a : ι) → L.Substructure M) i : L.Substructure M))
      fun (x x_1 : ι) (h : x ≤ x_1) ↦ Substructure.inclusion sorry),
  Membership.mem.{u_1, u_1} (α := M) (γ := L.Substructure M) (⨆ (i : ι), (S : (a : ι) → L.Substructure M) i)
    ((liftInclusion S :
          (a :
              DirectLimit (fun (i : ι) ↦ ↥((S : (a : ι) → L.Substructure M) i)) fun (x x_1 : ι) (h : x ≤ x_1) ↦
                Substructure.inclusion sorry) →
            M)
        x :
      M)
Tactic: have liftInclusion_in_sup : ∀ x, liftInclusion S x ∈ (⨆ i, S i) := by
    simp only [← rangeLiftInclusion, Hom.mem_range, Embedding.coe_toHom]
    intro x; use x
-- Lean 4 proof step from Mathlib.ModelTheory.DirectLimit (hypothesis)
Goal:
L : Language
ι : Type v
inst : Preorder ι
G : ι → Type w
inst_1 : (i : ι) → Structure.{u_2, u_3, w} L (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst_2 : Nonempty ι
inst_3 : IsDirectedOrder ι
M : Type u_1
inst_4 : L.Structure M
S : OrderHom.{v, u_1} ι (L.Substructure M)
liftInclusion_in_sup :
  ∀
    (x :
      DirectLimit.{v, u_1, u_2, u_3} (L := L) (fun (i : ι) ↦ ↥((S : (a : ι) → L.Substructure M) i : L.Substructure M))
        fun (x x_1 : ι) (h : x ≤ x_1) ↦ Substructure.inclusion ⋯),
    Membership.mem.{u_1, u_1} (α := M) (γ := L.Substructure M) (⨆ (i : ι), (S : (a : ι) → L.Substructure M) i)
      ((liftInclusion S :
            (a :
                DirectLimit (fun (i : ι) ↦ ↥((S : (a : ι) → L.Substructure M) i)) fun (x x_1 : ι) (h : x ≤ x_1) ↦
                  Substructure.inclusion ⋯) →
              M)
          x :
        M)
F : (DirectLimit.{v, u_1, u_2, u_3} (L := L) (fun (i : ι) ↦ ↥((S : (a : ι) → L.Substructure M) i : L.Substructure M))
    fun (x x_1 : ι) (h : x ≤ x_1) ↦ Substructure.inclusion ⋯) ↪[L]
  ↥(⨆ (i : ι), (S : (a : ι) → L.Substructure M) i) :=
  Embedding.codRestrict (⨆ (i : ι), (S : (a : ι) → L.Substructure M) i) (liftInclusion S) liftInclusion_in_sup
m : M
hm : Membership.mem (γ := L.Substructure M) (⨆ (i : ι), (S : (a : ι) → L.Substructure M) i) m
⊢ ∃ (a :
    DirectLimit.{v, u_1, u_2, u_3} (L := L) (fun (i : ι) ↦ ↥((S : (a : ι) → L.Substructure M) i : L.Substructure M))
      fun (x x_1 : ι) (h : x ≤ x_1) ↦ Substructure.inclusion ⋯),
    (F :
          (a :
              DirectLimit (fun (i : ι) ↦ ↥((S : (a : ι) → L.Substructure M) i)) fun (x x_1 : ι) (h : x ≤ x_1) ↦
                Substructure.inclusion ⋯) →
            ↥(⨆ (i : ι), (S : (a : ι) → L.Substructure M) i))
        a =
      Subtype.mk (p := fun (x : M) ↦
        Membership.mem (γ := L.Substructure M) (⨆ (i : ι), (S : (a : ι) → L.Substructure M) i) x) m hm
have hm₁ : ∃ (y :
  DirectLimit.{v, u_1, u_2, u_3} (L := L) (fun (i : ι) ↦ ↥((S : (a : ι) → L.Substructure M) i : L.Substructure M))
    fun (x x_1 : ι) (h : x ≤ x_1) ↦ Substructure.inclusion sorry),
  (Embedding.toHom (liftInclusion S) :
        (a :
            DirectLimit (fun (i : ι) ↦ ↥((S : (a : ι) → L.Substructure M) i)) fun (x x_1 : ι) (h : x ≤ x_1) ↦
              Substructure.inclusion sorry) →
          M)
      y =
    m
Tactic: rw [← rangeLiftInclusion, Hom.mem_range] at hm
-- Lean 4 proof step from Mathlib.ModelTheory.DirectLimit (goal)
Goal:
L : Language
ι : Type v
inst : Preorder ι
G : ι → Type w
inst_1 : (i : ι) → Structure.{u_2, u_3, w} L (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst_2 : Nonempty ι
inst_3 : IsDirectedOrder ι
M : Type u_1
inst_4 : L.Structure M
S : OrderHom.{v, u_1} ι (L.Substructure M)
liftInclusion_in_sup :
  ∀
    (x :
      DirectLimit.{v, u_1, u_2, u_3} (L := L) (fun (i : ι) ↦ ↥((S : (a : ι) → L.Substructure M) i : L.Substructure M))
        fun (x x_1 : ι) (h : x ≤ x_1) ↦ Substructure.inclusion ⋯),
    Membership.mem.{u_1, u_1} (α := M) (γ := L.Substructure M) (⨆ (i : ι), (S : (a : ι) → L.Substructure M) i)
      ((liftInclusion S :
            (a :
                DirectLimit (fun (i : ι) ↦ ↥((S : (a : ι) → L.Substructure M) i)) fun (x x_1 : ι) (h : x ≤ x_1) ↦
                  Substructure.inclusion ⋯) →
              M)
          x :
        M)
F : (DirectLimit.{v, u_1, u_2, u_3} (L := L) (fun (i : ι) ↦ ↥((S : (a : ι) → L.Substructure M) i : L.Substructure M))
    fun (x x_1 : ι) (h : x ≤ x_1) ↦ Substructure.inclusion ⋯) ↪[L]
  ↥(⨆ (i : ι), (S : (a : ι) → L.Substructure M) i) :=
  Embedding.codRestrict (⨆ (i : ι), (S : (a : ι) → L.Substructure M) i) (liftInclusion S) liftInclusion_in_sup
m : M
hm : Membership.mem (γ := L.Substructure M) (⨆ (i : ι), (S : (a : ι) → L.Substructure M) i) m
a :
  DirectLimit.{v, u_1, u_2, u_3} (L := L) (fun (i : ι) ↦ ↥((S : (a : ι) → L.Substructure M) i : L.Substructure M))
    fun (x x_1 : ι) (h : x ≤ x_1) ↦ Substructure.inclusion ⋯
h :
  (Embedding.toHom (liftInclusion S) :
        (a :
            DirectLimit (fun (i : ι) ↦ ↥((S : (a : ι) → L.Substructure M) i)) fun (x x_1 : ι) (h : x ≤ x_1) ↦
              Substructure.inclusion ⋯) →
          M)
      a =
    m
⊢ ∃ (a :
    DirectLimit.{v, u_1, u_2, u_3} (L := L) (fun (i : ι) ↦ ↥((S : (a : ι) → L.Substructure M) i : L.Substructure M))
      fun (x x_1 : ι) (h : x ≤ x_1) ↦ Substructure.inclusion ⋯),
    (F :
          (a :
              DirectLimit (fun (i : ι) ↦ ↥((S : (a : ι) → L.Substructure M) i)) fun (x x_1 : ι) (h : x ≤ x_1) ↦
                Substructure.inclusion ⋯) →
            ↥(⨆ (i : ι), (S : (a : ι) → L.Substructure M) i))
        a =
      Subtype.mk (p := fun (x : M) ↦
        Membership.mem (γ := L.Substructure M) (⨆ (i : ι), (S : (a : ι) → L.Substructure M) i) x) m hm
have h : (F :
      (a :
          DirectLimit (fun (i : ι) ↦ ↥((S : (a : ι) → L.Substructure M) i)) fun (x x_1 : ι) (h : x ≤ x_1) ↦
            Substructure.inclusion sorry) →
        ↥(⨆ (i : ι), (S : (a : ι) → L.Substructure M) i))
    a =
  Subtype.mk (p := fun (x : M) ↦
    Membership.mem (γ := L.Substructure M) (⨆ (i : ι), (S : (a : ι) → L.Substructure M) i) x) m hm
Tactic: use a
-- Lean 4 proof step from Mathlib.ModelTheory.DirectLimit (hypothesis)
Goal:
L : Language
ι : Type v
inst : Preorder ι
G : ι → Type w
inst_1 : (i : ι) → Structure.{u_2, u_3, w} L (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst_2 : Nonempty ι
inst_3 : IsDirectedOrder ι
M : Type u_1
inst_4 : L.Structure M
S : OrderHom.{v, u_1} ι (L.Substructure M)
liftInclusion_in_sup :
  ∀
    (x :
      DirectLimit.{v, u_1, u_2, u_3} (L := L) (fun (i : ι) ↦ ↥((S : (a : ι) → L.Substructure M) i : L.Substructure M))
        fun (x x_1 : ι) (h : x ≤ x_1) ↦ Substructure.inclusion ⋯),
    Membership.mem.{u_1, u_1} (α := M) (γ := L.Substructure M) (⨆ (i : ι), (S : (a : ι) → L.Substructure M) i)
      ((liftInclusion S :
            (a :
                DirectLimit (fun (i : ι) ↦ ↥((S : (a : ι) → L.Substructure M) i)) fun (x x_1 : ι) (h : x ≤ x_1) ↦
                  Substructure.inclusion ⋯) →
              M)
          x :
        M)
F : (DirectLimit.{v, u_1, u_2, u_3} (L := L) (fun (i : ι) ↦ ↥((S : (a : ι) → L.Substructure M) i : L.Substructure M))
    fun (x x_1 : ι) (h : x ≤ x_1) ↦ Substructure.inclusion ⋯) ↪[L]
  ↥(⨆ (i : ι), (S : (a : ι) → L.Substructure M) i) :=
  Embedding.codRestrict (⨆ (i : ι), (S : (a : ι) → L.Substructure M) i) (liftInclusion S) liftInclusion_in_sup
⊢ (DirectLimit.{v, u_1, u_2, u_3} (L := L) (fun (i : ι) ↦ ↥((S : (a : ι) → L.Substructure M) i : L.Substructure M))
      fun (x x_1 : ι) (h : x ≤ x_1) ↦ Substructure.inclusion ⋯) ≃[L]
    ↥(iSup.{u_1, v + 1} (ι := ι) (⇑S : (a : ι) → L.Substructure M))
have F_surj : Function.Surjective (α :=
  DirectLimit.{v, u_1, u_2, u_3} (L := L) (fun (i : ι) ↦ ↥((S : (a : ι) → L.Substructure M) i : L.Substructure M))
    fun (x x_1 : ι) (h : x ≤ x_1) ↦ Substructure.inclusion sorry)
  (β := ↥(⨆ (i : ι), (S : (a : ι) → L.Substructure M) i))
  (⇑F :
    (a :
        DirectLimit (fun (i : ι) ↦ ↥((S : (a : ι) → L.Substructure M) i)) fun (x x_1 : ι) (h : x ≤ x_1) ↦
          Substructure.inclusion sorry) →
      ↥(⨆ (i : ι), (S : (a : ι) → L.Substructure M) i))
Tactic: have F_surj : Function.Surjective F := by
    rintro ⟨m, hm⟩
    rw [← rangeLiftInclusion, Hom.mem_range] at hm
    rcases hm with ⟨a, _⟩; use a
    simpa only [F, Embedding.codRestrict_apply', Subtype.mk.injEq]
-- Lean 4 proof step from Mathlib.ModelTheory.DirectLimit (goal)
Goal:
L : Language
ι : Type v
inst : Preorder ι
inst_1 : Nonempty ι
inst_2 : IsDirectedOrder ι
M : Type u_1
inst_3 : L.Structure M
S : OrderHom.{v, u_1} ι (L.Substructure M)
i : ι
⊢ Eq (α :=
    ↥((S : (a : ι) → L.Substructure M) i : L.Substructure M) ↪[L]
      DirectLimit.{v, u_1, u_2, u_3} (L := L) (fun (i : ι) ↦ ↥((S : (a : ι) → L.Substructure M) i : L.Substructure M))
        fun (x x_1 : ι) (h : x ≤ x_1) ↦ Substructure.inclusion ⋯)
    (Embedding.comp (Equiv.toEmbedding (Equiv.symm (Equiv_iSup S))) (Substructure.inclusion ⋯))
    (of.{v, u_1, u_2, u_3} L ι (fun (x : ι) ↦ ↥((S : (a : ι) → L.Substructure M) x : L.Substructure M))
      (fun (x x_1 : ι) (h : x ≤ x_1) ↦ Substructure.inclusion ⋯) i)
have h : ∀ (x : ↥((S : (a : ι) → L.Substructure M) i : L.Substructure M)),
  Eq (α :=
    DirectLimit.{v, u_1, u_2, u_3} (L := L) (fun (i : ι) ↦ ↥((S : (a : ι) → L.Substructure M) i : L.Substructure M))
      fun (x x_1 : ι) (h : x ≤ x_1) ↦ Substructure.inclusion sorry)
    ((Embedding.comp (Equiv.toEmbedding (Equiv.symm (Equiv_iSup S))) (Substructure.inclusion sorry) :
          (a : ↥((S : (a : ι) → L.Substructure M) i)) →
            DirectLimit (fun (i : ι) ↦ ↥((S : (a : ι) → L.Substructure M) i)) fun (x x_1 : ι) (h : x ≤ x_1) ↦
              Substructure.inclusion sorry)
        x :
      DirectLimit.{v, u_1, u_2, u_3} (L := L) (fun (i : ι) ↦ ↥((S : (a : ι) → L.Substructure M) i : L.Substructure M))
        fun (x x_1 : ι) (h : x ≤ x_1) ↦ Substructure.inclusion sorry)
    (((of.{v, u_1, u_2, u_3} L ι (fun (x : ι) ↦ ↥((S : (a : ι) → L.Substructure M) x : L.Substructure M))
              (fun (x x_1 : ι) (h : x ≤ x_1) ↦ Substructure.inclusion sorry) i :
            ↥((S : (a : ι) → L.Substructure M) i : L.Substructure M) ↪[L]
              DirectLimit.{v, u_1, u_2, u_3} (L := L)
                (fun (x : ι) ↦ ↥((S : (a : ι) → L.Substructure M) x : L.Substructure M)) fun (x x_1 : ι) (h : x ≤ x_1) ↦
                Substructure.inclusion sorry) :
          (a : ↥((S : (a : ι) → L.Substructure M) i)) →
            DirectLimit (fun (i : ι) ↦ ↥((S : (a : ι) → L.Substructure M) i)) fun (x x_1 : ι) (h : x ≤ x_1) ↦
              Substructure.inclusion sorry)
        x :
      DirectLimit.{v, u_1, u_2, u_3} (L := L) (fun (i : ι) ↦ ↥((S : (a : ι) → L.Substructure M) i : L.Substructure M))
        fun (x x_1 : ι) (h : x ≤ x_1) ↦ Substructure.inclusion sorry)
Tactic: ext x
-- Lean 4 proof step from Mathlib.ModelTheory.ElementaryMaps (goal)
Goal:
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst : L.Structure M
inst_1 : L.Structure N
inst_2 : L.Structure P
inst_3 : L.Structure Q
f g : M ↪ₑ[L] N
h : Eq (α := (a : M) → N) ((fun (f : M ↪ₑ[L] N) ↦ (↑f : M → N)) f) ((fun (f : M ↪ₑ[L] N) ↦ (↑f : M → N)) g)
⊢ f = g
have mk : ∀ (toFun : M → N)
  (map_formula' : ∀ ⦃n : ℕ⦄ (φ : L.Formula (Fin n)) (x : Fin n → M), φ.Realize (toFun ∘ x) ↔ φ.Realize x)
  (h :
    Eq (α := (a : M) → N) ((fun (f : M ↪ₑ[L] N) ↦ (↑f : M → N)) { toFun := toFun, map_formula' := map_formula' })
      ((fun (f : M ↪ₑ[L] N) ↦ (↑f : M → N)) g)),
  { toFun := toFun, map_formula' := map_formula' : M ↪ₑ[L] N } = g
Tactic: cases f
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.ModelTheory.ElementaryMaps (goal)
Goal:
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst : L.Structure M
inst_1 : L.Structure N
inst_2 : L.Structure P
inst_3 : L.Structure Q
g : M ↪ₑ[L] N
toFun : M → N
map_formula' : ∀ ⦃n : ℕ⦄ (φ : L.Formula (Fin n)) (x : Fin n → M), φ.Realize (toFun ∘ x) ↔ φ.Realize x
h :
  Eq (α := (a : M) → N) ((fun (f : M ↪ₑ[L] N) ↦ (↑f : M → N)) { toFun := toFun, map_formula' := map_formula' })
    ((fun (f : M ↪ₑ[L] N) ↦ (↑f : M → N)) g)
⊢ { toFun := toFun, map_formula' := map_formula' : M ↪ₑ[L] N } = g
have mk : ∀ (toFun_1 : M → N)
  (map_formula'_1 : ∀ ⦃n : ℕ⦄ (φ : L.Formula (Fin n)) (x : Fin n → M), φ.Realize (toFun_1 ∘ x) ↔ φ.Realize x)
  (h :
    Eq (α := (a : M) → N) ((fun (f : M ↪ₑ[L] N) ↦ (↑f : M → N)) { toFun := toFun, map_formula' := map_formula' })
      ((fun (f : M ↪ₑ[L] N) ↦ (↑f : M → N)) { toFun := toFun_1, map_formula' := map_formula'_1 })),
  { toFun := toFun, map_formula' := map_formula' : M ↪ₑ[L] N } = { toFun := toFun_1, map_formula' := map_formula'_1 }
Tactic: cases g
Cleared hypotheses: g, 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
α : Type u_5
n : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin n → M
⊢ BoundedFormula.Realize.{u_6, u_7, u_2, u_5} (M := N) φ ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs) ↔
    φ.Realize v xs
have rw : BoundedFormula.Realize.{u_6, u_7, u_2, u_5} (M := N) (α := (↑(↑φ.freeVarFinset : Set α) : Type u_5))
    (φ.restrictFreeVar id) (((⇑f : (a : M) → N) ∘ v) ∘ Subtype.val (p := fun (x : α) ↦ x ∈ (↑φ.freeVarFinset : Set α)))
    ((⇑f : (a : M) → N) ∘ xs) ↔
  φ.Realize v xs
Tactic: rw [← BoundedFormula.realize_restrictFreeVar' Set.Subset.rfl, Set.inclusion_eq_id]
-- Lean 4 proof step from Mathlib.ModelTheory.ElementaryMaps (hypothesis)
Goal:
L : Language
M : Type u_1
N : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
f : M ↪ₑ[L] N
α : Type u_5
n : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin n → M
⊢ BoundedFormula.Realize.{u_6, u_7, u_2, u_5} (M := N) (α := (↑(↑φ.freeVarFinset : Set α) : Type u_5))
      (φ.restrictFreeVar id)
      (((⇑f : (a : M) → N) ∘ v) ∘ Subtype.val (p := fun (x : α) ↦ x ∈ (↑φ.freeVarFinset : Set α)))
      ((⇑f : (a : M) → N) ∘ xs) ↔
    φ.Realize v xs
have h : Formula.Realize (α := Fin (Fintype.card.{u_5} (↥φ.freeVarFinset ⊕ Fin n)))
    (Formula.relabel (α := ↥φ.freeVarFinset ⊕ Fin n)
      (⇑(Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n)) :
        (a : ↥φ.freeVarFinset ⊕ Fin n) → Fin (Fintype.card (↥φ.freeVarFinset ⊕ Fin n)))
      (BoundedFormula.toFormula (φ.restrictFreeVar id)))
    ((↑f : M → N) ∘
      Function.comp (β := ↥φ.freeVarFinset ⊕ Fin n)
        (Sum.elim (v ∘ Subtype.val (p := fun (x : α) ↦ x ∈ φ.freeVarFinset)) xs)
        (⇑(_root_.Equiv.symm (Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n))) :
          (a : Fin (Fintype.card (↥φ.freeVarFinset ⊕ Fin n))) → ↥φ.freeVarFinset ⊕ Fin n)) ↔
  Formula.Realize (α := Fin (Fintype.card.{u_5} (↥φ.freeVarFinset ⊕ Fin n)))
    (Formula.relabel (α := ↥φ.freeVarFinset ⊕ Fin n)
      (⇑(Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n)) :
        (a : ↥φ.freeVarFinset ⊕ Fin n) → Fin (Fintype.card (↥φ.freeVarFinset ⊕ Fin n)))
      (BoundedFormula.toFormula (φ.restrictFreeVar id)))
    (Function.comp (β := ↥φ.freeVarFinset ⊕ Fin n)
      (Sum.elim (v ∘ Subtype.val (p := fun (x : α) ↦ x ∈ φ.freeVarFinset)) xs)
      (⇑(_root_.Equiv.symm (Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n))) :
        (a : Fin (Fintype.card (↥φ.freeVarFinset ⊕ Fin n))) → ↥φ.freeVarFinset ⊕ Fin n))
Tactic: have h :=
      f.map_formula' ((φ.restrictFreeVar id).toFormula.relabel (Fintype.equivFin _))
        (Sum.elim (v ∘ (↑)) xs ∘ (Fintype.equivFin _).symm)
-- 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
α : Type u_5
n : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin n → M
⊢ BoundedFormula.Realize.{u_6, u_7, u_2, u_5} (M := N) φ ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs) ↔
    φ.Realize v xs
have rw : BoundedFormula.Realize.{u_6, u_7, u_2, u_5} (M := N) (α := (↑(↑φ.freeVarFinset : Set α) : Type u_5))
    (φ.restrictFreeVar (Set.inclusion (s := (↑φ.freeVarFinset : Set α)) (t := (↑φ.freeVarFinset : Set α)) sorry))
    (((⇑f : (a : M) → N) ∘ v) ∘ Subtype.val (p := fun (x : α) ↦ x ∈ (↑φ.freeVarFinset : Set α)))
    ((⇑f : (a : M) → N) ∘ xs) ↔
  φ.Realize v xs
Tactic: classical
    rw [← BoundedFormula.realize_restrictFreeVar' Set.Subset.rfl, Set.inclusion_eq_id]
    have h :=
      f.map_formula' ((φ.restrictFreeVar id).toFormula.relabel (Fintype.equivFin _))
        (Sum.elim (v ∘ (↑)) xs ∘ (Fintype.equivFin _).symm)
    simp only [Formula.realize_relabel, BoundedFormula.realize_toFormula] at h
    rw [← Function.comp_assoc _ _ (Fintype.equivFin _).symm,
      Function.comp_assoc _ (Fintype.equivFin _).symm (Fintype.equivFin _),
      _root_.Equiv.symm_comp_self, Function.comp_id, Function.comp_assoc, Sum.elim_comp_inl,
      Function.comp_assoc _ _ Sum.inr, Sum.elim_comp_inr, ← Function.comp_assoc] at h
    refine h.trans ?_
    rw [Function.comp_assoc _ _ (Fintype.equivFin _), _root_.Equiv.symm_comp_self,
      Function.comp_id, Sum.elim_comp_inl, Sum.elim_comp_inr (v ∘ Subtype.val) xs,
      BoundedFormula.realize_restrictFreeVar v (by simp)]
-- 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
α : Type u_5
n : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin n → M
rw :
  BoundedFormula.Realize.{u_6, u_7, u_2, u_5} (M := N) (α := (↑(↑φ.freeVarFinset : Set α) : Type u_5))
      (φ.restrictFreeVar (Set.inclusion (s := (↑φ.freeVarFinset : Set α)) (t := (↑φ.freeVarFinset : Set α)) ⋯))
      (((⇑f : (a : M) → N) ∘ v) ∘ Subtype.val (p := fun (x : α) ↦ x ∈ (↑φ.freeVarFinset : Set α)))
      ((⇑f : (a : M) → N) ∘ xs) ↔
    φ.Realize v xs
⊢ BoundedFormula.Realize.{u_6, u_7, u_2, u_5} (M := N) φ ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs) ↔
    φ.Realize v xs
have rw₁ : BoundedFormula.Realize.{u_6, u_7, u_2, u_5} (M := N) (α := (↑(↑φ.freeVarFinset : Set α) : Type u_5))
    (φ.restrictFreeVar id) (((⇑f : (a : M) → N) ∘ v) ∘ Subtype.val (p := fun (x : α) ↦ x ∈ (↑φ.freeVarFinset : Set α)))
    ((⇑f : (a : M) → N) ∘ xs) ↔
  φ.Realize v xs
Tactic: classical
    rw [← BoundedFormula.realize_restrictFreeVar' Set.Subset.rfl, Set.inclusion_eq_id]
    have h :=
      f.map_formula' ((φ.restrictFreeVar id).toFormula.relabel (Fintype.equivFin _))
        (Sum.elim (v ∘ (↑)) xs ∘ (Fintype.equivFin _).symm)
    simp only [Formula.realize_relabel, BoundedFormula.realize_toFormula] at h
    rw [← Function.comp_assoc _ _ (Fintype.equivFin _).symm,
      Function.comp_assoc _ (Fintype.equivFin _).symm (Fintype.equivFin _),
      _root_.Equiv.symm_comp_self, Function.comp_id, Function.comp_assoc, Sum.elim_comp_inl,
      Function.comp_assoc _ _ Sum.inr, Sum.elim_comp_inr, ← Function.comp_assoc] at h
    refine h.trans ?_
    rw [Function.comp_assoc _ _ (Fintype.equivFin _), _root_.Equiv.symm_comp_self,
      Function.comp_id, Sum.elim_comp_inl, Sum.elim_comp_inr (v ∘ Subtype.val) xs,
      BoundedFormula.realize_restrictFreeVar v (by simp)]
-- 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
α : Type u_5
φ : L.Formula α
x : α → M
⊢ Formula.Realize.{u_6, u_7, u_2, u_5} (M := N) φ ((⇑f : (a : M) → N) ∘ x) ↔ φ.Realize x
have rw : BoundedFormula.Realize.{u_6, u_7, u_2, u_5} (M := N) φ ((⇑f : (a : M) → N) ∘ x) default ↔ φ.Realize x
Tactic: rw [Formula.Realize, Formula.Realize, ← f.map_boundedFormula, Unique.eq_default (f ∘ default)]
-- 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
α : Type u_5
φ : L.Formula α
x : α → M
rw : BoundedFormula.Realize.{u_6, u_7, u_2, u_5} (M := N) φ ((⇑f : (a : M) → N) ∘ x) default ↔ φ.Realize x
⊢ Formula.Realize.{u_6, u_7, u_2, u_5} (M := N) φ ((⇑f : (a : M) → N) ∘ x) ↔ φ.Realize x
have rw₁ : BoundedFormula.Realize.{u_6, u_7, u_2, u_5} (M := N) φ ((⇑f : (a : M) → N) ∘ x) default ↔
  BoundedFormula.Realize φ x default
Tactic: rw [Formula.Realize, Formula.Realize, ← f.map_boundedFormula, Unique.eq_default (f ∘ default)]