awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.DirectLimit
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)
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 ⋯),
    ∃ (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)
⊢ ∀
    (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)

Tactic:
simp only [← rangeLiftInclusion, Hom.mem_range, Embedding.coe_toHom]

Premises used: FirstOrder.Language.Hom.mem_range, FirstOrder.Language.Embedding.coe_toHom, FirstOrder.Language.DirectLimit.rangeLiftInclusion
-- Module: Mathlib.ModelTheory.DirectLimit
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 ⋯
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 ⋯) →
            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 ⋯) →
            M)
        x :
      M)
⊢ ∃ (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)

Tactic:
use x
-- Module: Mathlib.ModelTheory.DirectLimit
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)

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
-- Module: Mathlib.ModelTheory.DirectLimit
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
⊢ ∃ (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 ⋯),
    (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)
        y =
      m

Tactic:
rw [← rangeLiftInclusion, Hom.mem_range] at hm

Premises used: FirstOrder.Language.Hom.mem_range, FirstOrder.Language.DirectLimit.rangeLiftInclusion
-- Module: Mathlib.ModelTheory.DirectLimit
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_1 :
  (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
h :
  (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
⊢ ∃ (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

Tactic:
use a
-- Module: Mathlib.ModelTheory.DirectLimit
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
⊢ (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

Tactic:
simpa only [F, Embedding.codRestrict_apply', Subtype.mk.injEq]

Premises used: Subtype.mk.injEq, FirstOrder.Language.Embedding.codRestrict_apply'
-- Module: Mathlib.ModelTheory.DirectLimit
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
⊢ 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 ⋯)
    (β := ↥(⨆ (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 ⋯) →
        ↥(⨆ (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]
-- Module: Mathlib.ModelTheory.DirectLimit
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
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 ⋯)
    (β := ↥(⨆ (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 ⋯) →
        ↥(⨆ (i : ι), (S : (a : ι) → L.Substructure M) i))
⊢ (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))

Tactic:
exact ⟨Equiv.ofBijective F ⟨F.injective, F_surj⟩, F.map_fun', F.map_rel'⟩
-- Module: Mathlib.ModelTheory.DirectLimit
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 : ι
x : ↥((S : (a : ι) → L.Substructure M) i : L.Substructure M)
⊢ Eq.{u_1 + 1} (α := ↥(iSup.{u_1, v + 1} (ι := ι) (⇑S : (a : ι) → L.Substructure M)))
    ((Equiv_iSup S :
          (a :
              DirectLimit (fun (i : ι) ↦ ↥((S : (a : ι) → L.Substructure M) i)) fun (x x_1 : ι) (h : x ≤ x_1) ↦
                Substructure.inclusion ⋯) →
            ↥(iSup (⇑S : (a : ι) → L.Substructure M)))
        (((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 :
              ↥((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 ⋯) :
            (a : ↥((S : (a : ι) → L.Substructure M) i)) →
              DirectLimit (fun (x : ι) ↦ ↥((S : (a : ι) → L.Substructure M) x)) fun (x x_1 : ι) (h : x ≤ x_1) ↦
                Substructure.inclusion ⋯)
          x) :
      ↥(iSup.{u_1, v + 1} (ι := ι) (⇑S : (a : ι) → L.Substructure M)))
    ((Substructure.inclusion ⋯ :
          (a : ↥((S : (a : ι) → L.Substructure M) i)) → ↥(iSup (⇑S : (a : ι) → L.Substructure M)))
        x :
      ↥(iSup.{u_1, v + 1} (ι := ι) (⇑S : (a : ι) → L.Substructure M)))

Tactic:
rfl

Premises used: Set.Mem, rfl
-- Module: Mathlib.ModelTheory.DirectLimit
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 : ι
x : ↥((S : (a : ι) → L.Substructure M) i : L.Substructure M)
⊢ Eq (α := ↥(iSup.{u_1, v + 1} (ι := ι) (⇑S : (a : ι) → L.Substructure M)))
    ((Substructure.inclusion ⋯ :
          (a : ↥((S : (a : ι) → L.Substructure M) i)) → ↥(iSup (⇑S : (a : ι) → L.Substructure M)))
        x :
      ↥(iSup.{u_1, v + 1} (ι := ι) (⇑S : (a : ι) → L.Substructure M)))
    ((Equiv_iSup S :
          (a :
              DirectLimit (fun (i : ι) ↦ ↥((S : (a : ι) → L.Substructure M) i)) fun (x x_1 : ι) (h : x ≤ x_1) ↦
                Substructure.inclusion ⋯) →
            ↥(iSup (⇑S : (a : ι) → L.Substructure M)))
        (((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 :
              ↥((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 ⋯) :
            (a : ↥((S : (a : ι) → L.Substructure M) i)) →
              DirectLimit (fun (x : ι) ↦ ↥((S : (a : ι) → L.Substructure M) x)) fun (x x_1 : ι) (h : x ≤ x_1) ↦
                Substructure.inclusion ⋯)
          x) :
      ↥(iSup.{u_1, v + 1} (ι := ι) (⇑S : (a : ι) → L.Substructure M)))

Tactic:
rfl
-- Module: Mathlib.ModelTheory.DirectLimit
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 : ι
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 ⋯)
      ((Embedding.comp (Equiv.toEmbedding (Equiv.symm (Equiv_iSup S))) (Substructure.inclusion ⋯) :
            (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 ⋯)
          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 ⋯)
      (((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 :
              ↥((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 ⋯) :
            (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 ⋯)
          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 ⋯)
⊢ 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)

Tactic:
ext x
-- Module: Mathlib.ModelTheory.DirectLimit
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 : ι
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 ⋯)
    ((Embedding.comp (Equiv.toEmbedding (Equiv.symm (Equiv_iSup S))) (Substructure.inclusion ⋯) :
          (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 ⋯)
        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 ⋯)
    (((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 :
            ↥((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 ⋯) :
          (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 ⋯)
        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 ⋯)

Tactic:
Equiv_isup_symm_inclusion_apply _ x

Premises used: Set.Mem, Function.surjInv, Classical.choose, FirstOrder.Language.DirectLimit.Equiv_isup_symm_inclusion_apply