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_1, u_2, w} L (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst_2 : IsDirectedOrder ι
inst_3 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
inst_4 : Nonempty ι
P : Type u₁
inst_5 : L.Structure P
g_1 : (i : ι) → Embedding.{u_1, u_2, w, u₁} L (G i) P
Hg :
  ∀ (i j : ι) (hij : i ≤ j) (x : G i),
    Eq.{u₁ + 1} (α := P) ((g_1 j : (a : G j) → P) ((f i j hij : (a : G i) → G j) x : G j) : P)
      ((g_1 i : (a : G i) → P) x : P)
G' : ι → Type w'
inst_6 : (i : ι) → Structure.{u_1, u_2, w'} L (G' i)
f' : (i j : ι) → i ≤ j → G' i ↪[L] G' j
g : (i : ι) → Equiv.{u_1, u_2, w, w'} L (G i) (G' i)
inst_7 : DirectedSystem G' fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G' i) → G' j)
H_commuting :
  ∀ (i j : ι) (hij : i ≤ j) (x : G i),
    Eq.{w' + 1} (α := G' j) ((g j : (a : G j) → G' j) ((f i j hij : (a : G i) → G j) x) : G' j)
      ((f' i j hij : (a : G' i) → G' j) ((g i : (a : G i) → G' i) x : G' i) : G' j)
U : (i : ι) → G i ↪[L] DirectLimit G' f' := fun (i : ι) ↦ Embedding.comp (of L ι G' f' i) (g i).toEmbedding
F : DirectLimit G f ↪[L] DirectLimit G' f' := lift L ι G f U ⋯
surj_f :
  Function.Surjective (α := DirectLimit G f) (β := DirectLimit G' f') (⇑F : (a : DirectLimit G f) → DirectLimit G' f')
⊢ DirectLimit G f ≃[L] DirectLimit G' f'

Tactic:
exact ⟨Equiv.ofBijective F ⟨F.injective, surj_f⟩, F.map_fun', F.map_rel'⟩
-- Module: Mathlib.ModelTheory.DirectLimit
Goal:
L : Language
ι : Type v
inst : Preorder ι
G : ι → Type w
inst_1 : (i : ι) → Structure.{u_1, u_2, w} L (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst_2 : IsDirectedOrder ι
inst_3 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
inst_4 : Nonempty ι
G' : ι → Type w'
inst_5 : (i : ι) → Structure.{u_1, u_2, w'} L (G' i)
f' : (i j : ι) → i ≤ j → G' i ↪[L] G' j
g : (i : ι) → Equiv.{u_1, u_2, w, w'} L (G i) (G' i)
inst_6 : DirectedSystem G' fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G' i) → G' j)
H_commuting :
  ∀ (i j : ι) (hij : i ≤ j) (x : G i),
    Eq.{w' + 1} (α := G' j) ((g j : (a : G j) → G' j) ((f i j hij : (a : G i) → G j) x) : G' j)
      ((f' i j hij : (a : G' i) → G' j) ((g i : (a : G i) → G' i) x : G' i) : G' j)
i : ι
x : G i
⊢ Eq (α := DirectLimit G' f')
    ((equiv_lift L ι G f G' f' g H_commuting : (a : DirectLimit G f) → DirectLimit G' f')
        ((of L ι G f i : (a : G i) → DirectLimit G f) x) :
      DirectLimit G' f')
    ((of L ι G' f' i : (a : G' i) → DirectLimit G' f') ((g i : (a : G i) → G' i) x) : DirectLimit G' f')

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.ModelTheory.DirectLimit
Goal:
L : Language
ι : Type u_1
inst : Countable ι
inst_1 : Preorder ι
inst_2 : IsDirectedOrder ι
inst_3 : Nonempty ι
G : ι → Type w
inst_4 : (i : ι) → Structure.{u_2, u_3, w} L (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
h : ∀ (i : ι), CG.{w, u_2, u_3} L (G i)
inst_5 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
⊢ CG L (DirectLimit G f)

Tactic:
⟨⟨⋃ i, DirectLimit.of L ι G f i '' Classical.choose (h i).out, ?_, ?_⟩⟩

Premises used: FirstOrder.Language.DirectLimit.of, FirstOrder.Language.Structure.CG.mk, And.intro, Exists.intro, Classical.choose, Set.image, FirstOrder.Language.Structure.CG.out, DFunLike.coe, Set.iUnion
-- Module: Mathlib.ModelTheory.DirectLimit
Goal:
L : Language
ι : Type u_1
inst : Countable ι
inst_1 : Preorder ι
inst_2 : IsDirectedOrder ι
inst_3 : Nonempty ι
G : ι → Type w
inst_4 : (i : ι) → Structure.{u_2, u_3, w} L (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
h : ∀ (i : ι), CG.{w, u_2, u_3} L (G i)
inst_5 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
refine_1 :
  Set.Countable (α := DirectLimit G f)
    (⋃ (i : ι),
      image (α := G i) (⇑(of L ι G f i) : (a : G i) → DirectLimit G f)
        (Classical.choose (p := fun (x : Set (G i)) ↦
          x.Countable ∧
            Eq (α := L.Substructure (G i)) (LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L) x) ⊤)
          ⋯))
refine_2 :
  Eq (α := L.Substructure (DirectLimit G f))
    (LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L)
      (⋃ (i : ι),
        image (α := G i) (⇑(of L ι G f i) : (a : G i) → DirectLimit G f)
          (Classical.choose (p := fun (x : Set (G i)) ↦
            x.Countable ∧
              Eq (α := L.Substructure (G i)) (LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L) x) ⊤)
            ⋯)))
    ⊤
⊢ CG L (DirectLimit G f)

Tactic:
refine ⟨⟨⋃ i, DirectLimit.of L ι G f i '' Classical.choose (h i).out, ?_, ?_⟩⟩
-- Module: Mathlib.ModelTheory.DirectLimit
Goal:
L : Language
ι : Type u_1
inst : Countable ι
inst_1 : Preorder ι
inst_2 : IsDirectedOrder ι
inst_3 : Nonempty ι
G : ι → Type w
inst_4 : (i : ι) → Structure.{u_2, u_3, w} L (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
h : ∀ (i : ι), CG.{w, u_2, u_3} L (G i)
inst_5 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
⊢ Set.Countable (α := DirectLimit G f)
    (⋃ (i : ι),
      image (α := G i) (⇑(of L ι G f i) : (a : G i) → DirectLimit G f)
        (Classical.choose (p := fun (x : Set (G i)) ↦
          x.Countable ∧
            Eq (α := L.Substructure (G i)) (LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L) x) ⊤)
          ⋯))

Tactic:
Set.countable_iUnion fun i => Set.Countable.image (Classical.choose_spec (h i).out).1 _

Premises used: FirstOrder.Language.DirectLimit.of, Set.Countable.image, Classical.choose_spec, Set.countable_iUnion, And.left, FirstOrder.Language.Structure.CG.out, DFunLike.coe
-- Module: Mathlib.ModelTheory.DirectLimit
Goal:
L : Language
ι : Type u_1
inst : Countable ι
inst_1 : Preorder ι
inst_2 : IsDirectedOrder ι
inst_3 : Nonempty ι
G : ι → Type w
inst_4 : (i : ι) → Structure.{u_2, u_3, w} L (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
h : ∀ (i : ι), CG.{w, u_2, u_3} L (G i)
inst_5 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
⊢ Set.Countable (α := DirectLimit G f)
    (⋃ (i : ι),
      image (α := G i) (⇑(of L ι G f i) : (a : G i) → DirectLimit G f)
        (Classical.choose (p := fun (x : Set (G i)) ↦
          x.Countable ∧
            Eq (α := L.Substructure (G i)) (LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L) x) ⊤)
          ⋯))

Tactic:
exact Set.countable_iUnion fun i => Set.Countable.image (Classical.choose_spec (h i).out).1 _

Premises used: Set.Countable.image, Classical.choose_spec, Set.countable_iUnion, And.left, FirstOrder.Language.Structure.CG.out
-- Module: Mathlib.ModelTheory.DirectLimit
Goal:
L : Language
ι : Type u_1
inst : Countable ι
inst_1 : Preorder ι
inst_2 : IsDirectedOrder ι
inst_3 : Nonempty ι
G : ι → Type w
inst_4 : (i : ι) → Structure.{u_2, u_3, w} L (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
h : ∀ (i : ι), CG.{w, u_2, u_3} L (G i)
inst_5 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
refine_2 :
  LE.le (α := L.Substructure (DirectLimit G f)) ⊤
    (⨆ (i : ι),
      LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L)
        (image (α := G i) (⇑(of L ι G f i) : (a : G i) → DirectLimit G f)
          (Classical.choose (p := fun (x : Set (G i)) ↦
            x.Countable ∧
              Eq (α := L.Substructure (G i)) (LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L) x) ⊤)
            ⋯)))
⊢ Eq (α := L.Substructure (DirectLimit G f))
    (LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L)
      (⋃ (i : ι),
        image (α := G i) (⇑(of L ι G f i) : (a : G i) → DirectLimit G f)
          (Classical.choose (p := fun (x : Set (G i)) ↦
            x.Countable ∧
              Eq (α := L.Substructure (G i)) (LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L) x) ⊤)
            ⋯)))
    ⊤

Tactic:
rw [eq_top_iff, Substructure.closure_iUnion]

Premises used: eq_top_iff, FirstOrder.Language.Substructure.closure_iUnion
-- Module: Mathlib.ModelTheory.DirectLimit
Goal:
L : Language
ι : Type u_1
inst : Countable ι
inst_1 : Preorder ι
inst_2 : IsDirectedOrder ι
inst_3 : Nonempty ι
G : ι → Type w
inst_4 : (i : ι) → Structure.{u_2, u_3, w} L (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
h : ∀ (i : ι), CG.{w, u_2, u_3} L (G i)
inst_5 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
refine_2 :
  LE.le (α := L.Substructure (DirectLimit G f)) ⊤
    (⨆ (i : ι),
      Substructure.map (Embedding.toHom (of L ι G f i))
        (LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L)
          (Classical.choose (p := fun (x : Set (G i)) ↦
            x.Countable ∧
              Eq (α := L.Substructure (G i)) (LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L) x) ⊤)
            ⋯)))
⊢ LE.le (α := L.Substructure (DirectLimit G f)) ⊤
    (⨆ (i : ι),
      LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L)
        (image (α := G i) (⇑(of L ι G f i) : (a : G i) → DirectLimit G f)
          (Classical.choose (p := fun (x : Set (G i)) ↦
            x.Countable ∧
              Eq (α := L.Substructure (G i)) (LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L) x) ⊤)
            ⋯)))

Tactic:
simp_rw [← Embedding.coe_toHom, Substructure.closure_image]

Premises used: FirstOrder.Language.Embedding.coe_toHom, FirstOrder.Language.Substructure.closure_image
-- Module: Mathlib.ModelTheory.DirectLimit
Goal:
L : Language
ι : Type u_1
inst : Countable ι
inst_1 : Preorder ι
inst_2 : IsDirectedOrder ι
inst_3 : Nonempty ι
G : ι → Type w
inst_4 : (i : ι) → Structure.{u_2, u_3, w} L (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
h : ∀ (i : ι), CG.{w, u_2, u_3} L (G i)
inst_5 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
refine_2 :
  ∀ (b : L.Substructure (DirectLimit G f)),
    (∀ (i : ι),
        Substructure.map (Embedding.toHom (of L ι G f i))
            (LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L)
              (Classical.choose (p := fun (x : Set (G i)) ↦
                x.Countable ∧
                  Eq (α := L.Substructure (G i)) (LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L) x) ⊤)
                ⋯)) ≤
          b) →
      ⊤ ≤ b
⊢ LE.le (α := L.Substructure (DirectLimit G f)) ⊤
    (⨆ (i : ι),
      Substructure.map (Embedding.toHom (of L ι G f i))
        (LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L)
          (Classical.choose (p := fun (x : Set (G i)) ↦
            x.Countable ∧
              Eq (α := L.Substructure (G i)) (LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L) x) ⊤)
            ⋯)))

Tactic:
rw [le_iSup_iff]

Premises used: le_iSup_iff
-- Module: Mathlib.ModelTheory.DirectLimit
Goal:
L : Language
ι : Type u_1
inst : Countable ι
inst_1 : Preorder ι
inst_2 : IsDirectedOrder ι
inst_3 : Nonempty ι
G : ι → Type w
inst_4 : (i : ι) → Structure.{u_2, u_3, w} L (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
h : ∀ (i : ι), CG.{w, u_2, u_3} L (G i)
inst_5 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
S : L.Substructure (DirectLimit G f)
hS :
  ∀ (i : ι),
    Substructure.map (Embedding.toHom (of L ι G f i))
        (LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L)
          (Classical.choose (p := fun (x : Set (G i)) ↦
            x.Countable ∧
              Eq (α := L.Substructure (G i)) (LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L) x) ⊤)
            ⋯)) ≤
      S
x : DirectLimit G f
refine_2 : Membership.mem (γ := L.Substructure (DirectLimit G f)) ⊤ x → x ∈ S
⊢ Membership.mem (γ := L.Substructure (DirectLimit G f)) ⊤ x → x ∈ S

Tactic:
_
-- Module: Mathlib.ModelTheory.DirectLimit
Goal:
L : Language
ι : Type u_1
inst : Countable ι
inst_1 : Preorder ι
inst_2 : IsDirectedOrder ι
inst_3 : Nonempty ι
G : ι → Type w
inst_4 : (i : ι) → Structure.{u_2, u_3, w} L (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
h : ∀ (i : ι), CG.{w, u_2, u_3} L (G i)
inst_5 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
S : L.Substructure (DirectLimit G f)
hS :
  ∀ (i : ι),
    Substructure.map (Embedding.toHom (of L ι G f i))
        (LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L)
          (Classical.choose (p := fun (x : Set (G i)) ↦
            x.Countable ∧
              Eq (α := L.Substructure (G i)) (LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L) x) ⊤)
            ⋯)) ≤
      S
x : DirectLimit G f
h_1 : Membership.mem (γ := L.Substructure (DirectLimit G f)) ⊤ x
out : Quotient (setoid G f) → Σˣ (G := G) f := Quotient.out
⊢ x ∈ S

Tactic:
hS (out x).1 ⟨(out x).2, ?_, ?_⟩

Premises used: Sigma.fst, And.intro, Exists.intro, Sigma.snd
-- Module: Mathlib.ModelTheory.DirectLimit
Goal:
L : Language
ι : Type u_1
inst : Countable ι
inst_1 : Preorder ι
inst_2 : IsDirectedOrder ι
inst_3 : Nonempty ι
G : ι → Type w
inst_4 : (i : ι) → Structure.{u_2, u_3, w} L (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
h : ∀ (i : ι), CG.{w, u_2, u_3} L (G i)
inst_5 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
S : L.Substructure (DirectLimit G f)
hS :
  ∀ (i : ι),
    Substructure.map (Embedding.toHom (of L ι G f i))
        (LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L)
          (Classical.choose (p := fun (x : Set (G i)) ↦
            x.Countable ∧
              Eq (α := L.Substructure (G i)) (LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L) x) ⊤)
            ⋯)) ≤
      S
x : DirectLimit G f
h_1 : Membership.mem (γ := L.Substructure (DirectLimit G f)) ⊤ x
out : Quotient (setoid G f) → Σˣ (G := G) f := Quotient.out
refine_2 :
  (out x).snd (β := fun (i : ι) ↦ G i) ∈
    (↑(LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L)
          (Classical.choose (p := fun (x_1 : Set (G ((out x).fst (β := fun (i : ι) ↦ G i)))) ↦
            x_1.Countable ∧
              Eq (α := L.Substructure (G ((out x).fst (β := fun (i : ι) ↦ G i))))
                (LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L) x_1) ⊤)
            ⋯)) :
      Set (G (out x).fst))
refine_2₁ :
  (Embedding.toHom (of L ι G f ((out x).fst (β := fun (i : ι) ↦ G i))) : (a : G (out x).fst) → DirectLimit G f)
      ((out x).snd (β := fun (i : ι) ↦ G i)) =
    x
⊢ x ∈ S

Tactic:
refine hS (out x).1 ⟨(out x).2, ?_, ?_⟩

Premises used: Sigma.fst, And.intro, Exists.intro, Sigma.snd
-- Module: Mathlib.ModelTheory.DirectLimit
Goal:
L : Language
ι : Type u_1
inst : Countable ι
inst_1 : Preorder ι
inst_2 : IsDirectedOrder ι
inst_3 : Nonempty ι
G : ι → Type w
inst_4 : (i : ι) → Structure.{u_2, u_3, w} L (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
h : ∀ (i : ι), CG.{w, u_2, u_3} L (G i)
inst_5 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
S : L.Substructure (DirectLimit G f)
hS :
  ∀ (i : ι),
    Substructure.map (Embedding.toHom (of L ι G f i))
        (LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L)
          (Classical.choose (p := fun (x : Set (G i)) ↦
            x.Countable ∧
              Eq (α := L.Substructure (G i)) (LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L) x) ⊤)
            ⋯)) ≤
      S
x : DirectLimit G f
h_1 : Membership.mem (γ := L.Substructure (DirectLimit G f)) ⊤ x
out : Quotient (setoid G f) → Σˣ (G := G) f := Quotient.out
refine_2 : (out x).snd (β := fun (i : ι) ↦ G i) ∈ (↑⊤ : Set (G (out x).fst))
⊢ (out x).snd (β := fun (i : ι) ↦ G i) ∈
    (↑(LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L)
          (Classical.choose (p := fun (x_1 : Set (G ((out x).fst (β := fun (i : ι) ↦ G i)))) ↦
            x_1.Countable ∧
              Eq (α := L.Substructure (G ((out x).fst (β := fun (i : ι) ↦ G i))))
                (LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L) x_1) ⊤)
            ⋯)) :
      Set (G (out x).fst))

Tactic:
rw [(Classical.choose_spec (h (out x).1).out).2]

Premises used: Classical.choose_spec, And.right, FirstOrder.Language.Structure.CG.out
-- Module: Mathlib.ModelTheory.DirectLimit
Goal:
L : Language
ι : Type u_1
inst : Countable ι
inst_1 : Preorder ι
inst_2 : IsDirectedOrder ι
inst_3 : Nonempty ι
G : ι → Type w
inst_4 : (i : ι) → Structure.{u_2, u_3, w} L (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
h : ∀ (i : ι), CG.{w, u_2, u_3} L (G i)
inst_5 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
S : L.Substructure (DirectLimit G f)
hS :
  ∀ (i : ι),
    Substructure.map (Embedding.toHom (of L ι G f i))
        (LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L)
          (Classical.choose (p := fun (x : Set (G i)) ↦
            x.Countable ∧
              Eq (α := L.Substructure (G i)) (LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L) x) ⊤)
            ⋯)) ≤
      S
x : DirectLimit G f
h_1 : Membership.mem (γ := L.Substructure (DirectLimit G f)) ⊤ x
out : Quotient (setoid G f) → Σˣ (G := G) f := Quotient.out
⊢ (out x).snd (β := fun (i : ι) ↦ G i) ∈ (↑⊤ : Set (G (out x).fst))

Tactic:
trivial
-- Module: Mathlib.ModelTheory.DirectLimit
Goal:
L : Language
ι : Type u_1
inst : Countable ι
inst_1 : Preorder ι
inst_2 : IsDirectedOrder ι
inst_3 : Nonempty ι
G : ι → Type w
inst_4 : (i : ι) → Structure.{u_2, u_3, w} L (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
h : ∀ (i : ι), CG.{w, u_2, u_3} L (G i)
inst_5 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
S : L.Substructure (DirectLimit G f)
hS :
  ∀ (i : ι),
    Substructure.map (Embedding.toHom (of L ι G f i))
        (LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L)
          (Classical.choose (p := fun (x : Set (G i)) ↦
            x.Countable ∧
              Eq (α := L.Substructure (G i)) (LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L) x) ⊤)
            ⋯)) ≤
      S
x : DirectLimit G f
h_1 : Membership.mem (γ := L.Substructure (DirectLimit G f)) ⊤ x
out : Quotient (setoid G f) → Σˣ (G := G) f := Quotient.out
⊢ (Embedding.toHom (of L ι G f ((out x).fst (β := fun (i : ι) ↦ G i))) : (a : G (out x).fst) → DirectLimit G f)
      ((out x).snd (β := fun (i : ι) ↦ G i)) =
    x

Tactic:
simp only [out, Embedding.coe_toHom, DirectLimit.of_apply, Sigma.eta, Quotient.out_eq]

Premises used: Sigma.eta, FirstOrder.Language.Embedding.coe_toHom, FirstOrder.Language.DirectLimit.of_apply, Quotient.out_eq
-- Module: Mathlib.ModelTheory.DirectLimit
Goal:
L : Language
ι_1 : Type v
inst : Preorder ι_1
G_1 : ι_1 → Type w
inst_1 : (i : ι_1) → Structure.{u_2, u_3, w} L (G_1 i)
f_1 : (i j : ι_1) → i ≤ j → G_1 i ↪[L] G_1 j
inst_2 : IsDirectedOrder ι_1
inst_3 : DirectedSystem G_1 fun (i j : ι_1) (h : i ≤ j) ↦ (⇑(f_1 i j h) : (a : G_1 i) → G_1 j)
inst_4 : Nonempty ι_1
P : Type u₁
inst_5 : L.Structure P
g_1 : (i : ι_1) → Embedding.{u_2, u_3, w, u₁} L (G_1 i) P
Hg :
  ∀ (i j : ι_1) (hij : i ≤ j) (x : G_1 i),
    Eq.{u₁ + 1} (α := P) ((g_1 j : (a : G_1 j) → P) ((f_1 i j hij : (a : G_1 i) → G_1 j) x : G_1 j) : P)
      ((g_1 i : (a : G_1 i) → P) x : P)
G' : ι_1 → Type w'
inst_6 : (i : ι_1) → Structure.{u_2, u_3, w'} L (G' i)
f' : (i j : ι_1) → i ≤ j → G' i ↪[L] G' j
g : (i : ι_1) → Equiv.{u_2, u_3, w, w'} L (G_1 i) (G' i)
inst_7 : DirectedSystem G' fun (i j : ι_1) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G' i) → G' j)
H_commuting :
  ∀ (i j : ι_1) (hij : i ≤ j) (x : G_1 i),
    Eq.{w' + 1} (α := G' j) ((g j : (a : G_1 j) → G' j) ((f_1 i j hij : (a : G_1 i) → G_1 j) x) : G' j)
      ((f' i j hij : (a : G' i) → G' j) ((g i : (a : G_1 i) → G' i) x : G' i) : G' j)
ι : Type u_1
inst_8 : Countable ι
inst_9 : Preorder ι
inst_10 : IsDirectedOrder ι
inst_11 : Nonempty ι
G : ι → Type w
inst_12 : (i : ι) → Structure.{u_2, u_3, w} L (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
h : ∀ (i : ι), CG.{w, u_2, u_3} L (G i)
inst_13 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
⊢ CG L (DirectLimit G f)

Tactic:
cg f h

Premises used: FirstOrder.Language.DirectLimit.cg
-- 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} (α := M)
    ((liftInclusion S :
          (a :
              DirectLimit (fun (i : ι) ↦ ↥((S : (a : ι) → L.Substructure M) i)) fun (x x_1 : ι) (h : x ≤ x_1) ↦
                Substructure.inclusion ⋯) →
            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 :
          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 ⋯) :
      M)
    ((Substructure.subtype ((S : (a : ι) → L.Substructure M) i) : (a : ↥((S : (a : ι) → L.Substructure M) i)) → M) x :
      M)

Tactic:
rfl

Premises used: 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)
simp_rw :
  Hom.range (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 ⋯)
      (Embedding.toHom
        (lift L ι (fun (i : ι) ↦ ↥((S : (a : ι) → L.Substructure M) i : L.Substructure M))
          (fun (x x_1 : ι) (h : x ≤ x_1) ↦ Substructure.inclusion ⋯)
          (fun (x : ι) ↦ Substructure.subtype ((S : (a : ι) → L.Substructure M) x)) ⋯)) =
    ⨆ (i : ι), (S : (a : ι) → L.Substructure M) i
simp_rw₁ :
  Eq.{u_1 + 1} (α := L.Substructure M)
    (⨆ (i : ι),
      Hom.range (M := ↥((S : (a : ι) → L.Substructure M) i : L.Substructure M))
        (Embedding.toHom (Substructure.subtype ((S : (a : ι) → L.Substructure M) i))))
    (⨆ (i : ι), (S : (a : ι) → L.Substructure M) i)
⊢ Hom.range (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 ⋯)
      (Embedding.toHom (liftInclusion S)) =
    ⨆ (i : ι), (S : (a : ι) → L.Substructure M) i

Tactic:
simp_rw [liftInclusion, range_lift, Substructure.range_subtype]

Premises used: FirstOrder.Language.Substructure.range_subtype, FirstOrder.Language.DirectLimit.liftInclusion, FirstOrder.Language.DirectLimit.range_lift