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 ι
i : ι
x y : G i
j : ι
h1 w : i ≤ j
h3 : Eq (α := G j) ((f i j h1 : (a : G i) → G j) x : G j) ((f i j w : (a : G i) → G j) y : G j)
⊢ x = y

Tactic:
(f i j h1).injective h3

Premises used: FirstOrder.Language.Embedding.injective
-- 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 ι
i : ι
x y : G i
j : ι
h1 w : i ≤ j
h3 : Eq (α := G j) ((f i j h1 : (a : G i) → G j) x : G j) ((f i j w : (a : G i) → G j) y : G j)
⊢ x = y

Tactic:
exact (f i j h1).injective h3

Premises used: FirstOrder.Language.Embedding.injective
-- 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 ι
i : ι
n : ℕ
F : L.Functions n
x : Fin n → G i
rw :
  Eq (α := DirectLimit G f) (funMap F fun (a : Fin n) ↦ ⟦Structure.Sigma.mk (G := G) f i (x a)⟧)
    (funMap F ((fun (a : G i) ↦ ⟦Structure.Sigma.mk (G := G) f i a⟧) ∘ x))
⊢ ⟦Structure.Sigma.mk (G := G) f i (funMap F x)⟧ = funMap F ((fun (a : G i) ↦ ⟦Structure.Sigma.mk (G := G) f i a⟧) ∘ x)

Tactic:
rw [← funMap_quotient_mk'_sigma_mk']

Premises used: FirstOrder.Language.DirectLimit.funMap_quotient_mk'_sigma_mk'
-- 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 ι
i : ι
n : ℕ
F : L.Functions n
x : Fin n → G i
⊢ Eq (α := DirectLimit G f) (funMap F fun (a : Fin n) ↦ ⟦Structure.Sigma.mk (G := G) f i (x a)⟧)
    (funMap F ((fun (a : G i) ↦ ⟦Structure.Sigma.mk (G := G) f i a⟧) ∘ x))

Tactic:
rfl
-- 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 ι
i : ι
n : ℕ
R : L.Relations n
x : Fin n → G i
change : (RelMap (M := Quotient (setoid G f)) R fun (a : Fin n) ↦ ⟦Structure.Sigma.mk (G := G) f i (x a)⟧) ↔ RelMap R x
⊢ RelMap (M := DirectLimit G f) R ((fun (a : G i) ↦ ⟦Structure.Sigma.mk (G := G) f i a⟧) ∘ x) ↔ RelMap R x

Tactic:
change RelMap R (fun a => (⟦.mk f i (x a)⟧ : DirectLimit G f)) ↔ _

Premises used: FirstOrder.Language.Structure.Sigma.mk, FirstOrder.Language.DirectLimit.setoid, FirstOrder.Language.Structure.RelMap, Quotient.mk
-- 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 ι
i : ι
n : ℕ
R : L.Relations n
x : Fin n → G i
⊢ (RelMap (M := Quotient (setoid G f)) R fun (a : Fin n) ↦ ⟦Structure.Sigma.mk (G := G) f i (x a)⟧) ↔ RelMap R x

Tactic:
simp only [relMap_quotient_mk'_sigma_mk']

Premises used: FirstOrder.Language.DirectLimit.relMap_quotient_mk'_sigma_mk'
-- 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 ι
i : ι
x : G i
⊢ (of L ι G f i : (a : G i) → DirectLimit G f) x = ⟦Structure.Sigma.mk (G := G) f i x⟧

Tactic:
rfl

Premises used: rfl
-- 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 ι
i j : ι
hij : i ≤ j
x : G i
rw :
  (setoid G f : Σˣ f → Σˣ f → Prop) (Structure.Sigma.mk (G := G) f j ((f i j hij : (a : G i) → G j) x))
    (Structure.Sigma.mk (G := G) f i x)
⊢ Eq (α := DirectLimit G f)
    ((of L ι G f j : (a : G j) → DirectLimit G f) ((f i j hij : (a : G i) → G j) x) : DirectLimit G f)
    ((of L ι G f i : (a : G i) → DirectLimit G f) x : DirectLimit G f)

Tactic:
rw [of_apply, of_apply, Quotient.eq]

Premises used: FirstOrder.Language.DirectLimit.of_apply, Quotient.eq
-- 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 ι
i j : ι
hij : i ≤ j
x : G i
⊢ (setoid G f : Σˣ f → Σˣ f → Prop) (Structure.Sigma.mk (G := G) f j ((f i j hij : (a : G i) → G j) x))
    (Structure.Sigma.mk (G := G) f i x)

Tactic:
Setoid.symm ⟨j, hij, refl j, ?_⟩

Premises used: Setoid.symm, Exists.intro, refl
-- 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 ι
i j : ι
hij : i ≤ j
x : G i
refine :
  Eq (α := G j) ((f i j hij : (a : G i) → G j) x : G j)
    ((f j j ⋯ : (a : G j) → G j) ((f i j hij : (a : G i) → G j) x : G j) : G j)
⊢ (setoid G f : Σˣ f → Σˣ f → Prop) (Structure.Sigma.mk (G := G) f j ((f i j hij : (a : G i) → G j) x))
    (Structure.Sigma.mk (G := G) f i x)

Tactic:
refine Setoid.symm ⟨j, hij, refl j, ?_⟩
-- 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 ι
i j : ι
hij : i ≤ j
x : G i
⊢ Eq (α := G j) ((f i j hij : (a : G i) → G j) x : G j)
    ((f j j ⋯ : (a : G j) → G j) ((f i j hij : (a : G i) → G j) x : G j) : G j)

Tactic:
simp only [DirectedSystem.map_self]

Premises used: FirstOrder.Language.DirectedSystem.map_self
-- 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 ι
z : DirectLimit G f
⊢ (of L ι G f ((Quotient.out z).fst (β := fun (i : ι) ↦ G i)) : (a : G (Quotient.out z).fst) → DirectLimit G f)
      ((Quotient.out z).snd (β := fun (i : ι) ↦ G i)) =
    z

Tactic:
simp
-- 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 ι
C : DirectLimit G f → Prop
z : DirectLimit G f
ih : ∀ (i : ι) (x : G i), C ((of L ι G f i : (a : G i) → DirectLimit G f) x)
⊢ C z

Tactic:
let ⟨i, x, h⟩ := exists_of z
  h ▸ ih i x

Premises used: _private.0.FirstOrder.Language.DirectLimit.inductionOn.match_1, Eq.rec, FirstOrder.Language.DirectLimit.exists_of
-- 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 ι
⊢ Eq (α := L.Substructure (DirectLimit G f)) (⨆ (i : ι), Hom.range (Embedding.toHom (of L ι G f i))) ⊤

Tactic:
eq_top_iff.2 (fun x _ ↦ DirectLimit.inductionOn x
    (fun i _ ↦ le_iSup (fun i ↦ Hom.range (Embedding.toHom (of L ι G f i))) i (mem_range_self _)))

Premises used: Iff.mpr, eq_top_iff, FirstOrder.Language.DirectLimit.inductionOn
-- 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 ι
S : L.Substructure (DirectLimit G f)
S_fg : S.FG
let :
  ∀ (A : Finset (DirectLimit G f))
    (A_closure : LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L) (↑A : Set (DirectLimit G f)) = S),
    ∃ (i : ι) (T : L.Substructure (G i)), Substructure.map (Embedding.toHom (of L ι G f i)) T = S
⊢ ∃ (i : ι) (T : L.Substructure (G i)), Substructure.map (Embedding.toHom (of L ι G f i)) T = S

Tactic:
let ⟨A, A_closure⟩ := S_fg
-- 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 ι
S : L.Substructure (DirectLimit G f)
S_fg : S.FG
A : Finset (DirectLimit G f)
A_closure : LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L) (↑A : Set (DirectLimit G f)) = S
let :
  ∀ (i : ι) (y : ↥A → G i)
    (eq_y :
      Eq (α := ↥A → DirectLimit G f) (fun (a : ↥A) ↦ (↑a : DirectLimit G f)) fun (a : ↥A) ↦
        ⟦Structure.Sigma.mk (G := G) f i (y a)⟧),
    ∃ (i : ι) (T : L.Substructure (G i)), Substructure.map (Embedding.toHom (of L ι G f i)) T = S
⊢ ∃ (i : ι) (T : L.Substructure (G i)), Substructure.map (Embedding.toHom (of L ι G f i)) T = S

Tactic:
let ⟨i, y, eq_y⟩ := exists_quotient_mk'_sigma_mk'_eq G _ (fun a : A ↦ a.1)
-- 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 ι
S : L.Substructure (DirectLimit G f)
S_fg : S.FG
A : Finset (DirectLimit G f)
A_closure : LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L) (↑A : Set (DirectLimit G f)) = S
i : ι
y : ↥A → G i
eq_y :
  Eq (α := ↥A → DirectLimit G f) (fun (a : ↥A) ↦ (↑a : DirectLimit G f)) fun (a : ↥A) ↦
    ⟦Structure.Sigma.mk (G := G) f i (y a)⟧
h : ∃ (T : L.Substructure (G i)), Substructure.map (Embedding.toHom (of L ι G f i)) T = S
⊢ ∃ (i : ι) (T : L.Substructure (G i)), Substructure.map (Embedding.toHom (of L ι G f i)) T = S

Tactic:
use i
-- 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 ι
S : L.Substructure (DirectLimit G f)
S_fg : S.FG
A : Finset (DirectLimit G f)
A_closure : LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L) (↑A : Set (DirectLimit G f)) = S
i : ι
y : ↥A → G i
eq_y :
  Eq (α := ↥A → DirectLimit G f) (fun (a : ↥A) ↦ (↑a : DirectLimit G f)) fun (a : ↥A) ↦
    ⟦Structure.Sigma.mk (G := G) f i (y a)⟧
h :
  Substructure.map (Embedding.toHom (of L ι G f i))
      (LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L) (range y)) =
    S
⊢ ∃ (T : L.Substructure (G i)), Substructure.map (Embedding.toHom (of L ι G f i)) T = S

Tactic:
use Substructure.closure L (range y)

Premises used: LowerAdjoint.toFun, FirstOrder.Language.Substructure.closure, Set.range
-- 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 ι
S : L.Substructure (DirectLimit G f)
S_fg : S.FG
A : Finset (DirectLimit G f)
A_closure : LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L) (↑A : Set (DirectLimit G f)) = S
i : ι
y : ↥A → G i
eq_y :
  Eq (α := ↥A → DirectLimit G f) (fun (a : ↥A) ↦ (↑a : DirectLimit G f)) fun (a : ↥A) ↦
    ⟦Structure.Sigma.mk (G := G) f i (y a)⟧
h :
  LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L)
      ((⇑(Embedding.toHom (of L ι G f i)) : (a : G i) → DirectLimit G f) '' range y) =
    S
⊢ Substructure.map (Embedding.toHom (of L ι G f i))
      (LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L) (range y)) =
    S

Tactic:
rw [Substructure.map_closure]

Premises used: FirstOrder.Language.Substructure.map_closure
-- 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 ι
S : L.Substructure (DirectLimit G f)
S_fg : S.FG
A : Finset (DirectLimit G f)
A_closure : LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L) (↑A : Set (DirectLimit G f)) = S
i : ι
y : ↥A → G i
eq_y :
  Eq (α := ↥A → DirectLimit G f) (fun (a : ↥A) ↦ (↑a : DirectLimit G f)) fun (a : ↥A) ↦
    ⟦Structure.Sigma.mk (G := G) f i (y a)⟧
h :
  LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L)
      ((fun (a : G i) ↦ ⟦Structure.Sigma.mk (G := G) f i a⟧) '' y '' univ) =
    S
h₁ :
  LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L)
      ((fun (x : ↥A) ↦ ⟦Structure.Sigma.mk (G := G) f i (y x)⟧) '' univ) =
    S
h₂ :
  LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L)
      (range fun (x : ↥A) ↦ ⟦Structure.Sigma.mk (G := G) f i (y x)⟧) =
    S
h₃ : LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L) (range fun (a : ↥A) ↦ (↑a : DirectLimit G f)) = S
h₄ : LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L) {x : DirectLimit G f | x ∈ A} = S
h₅ : LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L) (↑A : Set (DirectLimit G f)) = S
h₆ h₇ : S = S
⊢ LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L)
      ((fun (a : G i) ↦ ⟦Structure.Sigma.mk (G := G) f i a⟧) '' range y) =
    S

Tactic:
rw [← image_univ, image_image, image_univ, ← eq_y,
    Subtype.range_coe_subtype, Finset.setOf_mem, A_closure]

Premises used: Set.image_image, Set.image_univ, Finset.setOf_mem, Subtype.range_coe_subtype
-- 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 : (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 j : (a : G j) → P) ((f i j hij : (a : G i) → G j) x : G j) : P)
      ((g i : (a : G i) → P) x : P)
x y : Σˣ (G := G) f
xy : x ≈ y
simp :
  Eq.{u₁ + 1} (α := P) ((g (x.fst (β := fun (i : ι) ↦ G i)) : (a : G x.fst) → P) (x.snd (β := fun (i : ι) ↦ G i)) : P)
    ((g (y.fst (β := fun (i : ι) ↦ G i)) : (a : G y.fst) → P) (y.snd (β := fun (i : ι) ↦ G i)) : P)
⊢ Eq.{u₁ + 1} (α := P)
    ((fun (x : Σˣ (G := G) f) ↦
        ((g (x.fst (β := fun (i : ι) ↦ G i)) : (a : G x.fst) → P) (x.snd (β := fun (i : ι) ↦ G i)) : P))
      x)
    ((fun (x : Σˣ (G := G) f) ↦
        ((g (x.fst (β := fun (i : ι) ↦ G i)) : (a : G x.fst) → P) (x.snd (β := fun (i : ι) ↦ G i)) : P))
      y)

Tactic:
simp only
-- 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 : (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 j : (a : G j) → P) ((f i j hij : (a : G i) → G j) x : G j) : P)
      ((g i : (a : G i) → P) x : P)
x y : Σˣ (G := G) f
xy : x ≈ y
obtain :
  ∀ (i : ι) (hx : x.fst (β := fun (i : ι) ↦ G i) ≤ i) (hy : y.fst (β := fun (i : ι) ↦ G i) ≤ i),
    Eq.{u₁ + 1} (α := P) ((g (x.fst (β := fun (i : ι) ↦ G i)) : (a : G x.fst) → P) (x.snd (β := fun (i : ι) ↦ G i)) : P)
      ((g (y.fst (β := fun (i : ι) ↦ G i)) : (a : G y.fst) → P) (y.snd (β := fun (i : ι) ↦ G i)) : P)
⊢ Eq.{u₁ + 1} (α := P) ((g (x.fst (β := fun (i : ι) ↦ G i)) : (a : G x.fst) → P) (x.snd (β := fun (i : ι) ↦ G i)) : P)
    ((g (y.fst (β := fun (i : ι) ↦ G i)) : (a : G y.fst) → P) (y.snd (β := fun (i : ι) ↦ G i)) : P)

Tactic:
obtain ⟨i, hx, hy⟩ := directed_of (· ≤ ·) x.1 y.1

Premises used: Sigma.fst, LE.le, directed_of
-- 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 : (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 j : (a : G j) → P) ((f i j hij : (a : G i) → G j) x : G j) : P)
      ((g i : (a : G i) → P) x : P)
x y : Σˣ (G := G) f
xy : x ≈ y
i : ι
hx : x.fst (β := fun (i : ι) ↦ G i) ≤ i
hy : y.fst (β := fun (i : ι) ↦ G i) ≤ i
rw :
  Eq.{u₁ + 1} (α := P)
    ((g i : (a : G i) → P)
        ((f (x.fst (β := fun (i : ι) ↦ G i)) i hx : (a : G x.fst) → G i) (x.snd (β := fun (i : ι) ↦ G i)) : G i) :
      P)
    ((g i : (a : G i) → P)
        ((f (y.fst (β := fun (i : ι) ↦ G i)) i hy : (a : G y.fst) → G i) (y.snd (β := fun (i : ι) ↦ G i)) : G i) :
      P)
⊢ Eq.{u₁ + 1} (α := P) ((g (x.fst (β := fun (i : ι) ↦ G i)) : (a : G x.fst) → P) (x.snd (β := fun (i : ι) ↦ G i)) : P)
    ((g (y.fst (β := fun (i : ι) ↦ G i)) : (a : G y.fst) → P) (y.snd (β := fun (i : ι) ↦ G i)) : P)

Tactic:
rw [← Hg x.1 i hx, ← Hg y.1 i hy]

Premises used: Sigma.fst
-- 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 : (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 j : (a : G j) → P) ((f i j hij : (a : G i) → G j) x : G j) : P)
      ((g i : (a : G i) → P) x : P)
x y : Σˣ (G := G) f
xy : x ≈ y
i : ι
hx : x.fst (β := fun (i : ι) ↦ G i) ≤ i
hy : y.fst (β := fun (i : ι) ↦ G i) ≤ i
⊢ Eq.{u₁ + 1} (α := P)
    ((g i : (a : G i) → P)
        ((f (x.fst (β := fun (i : ι) ↦ G i)) i hx : (a : G x.fst) → G i) (x.snd (β := fun (i : ι) ↦ G i)) : G i) :
      P)
    ((g i : (a : G i) → P)
        ((f (y.fst (β := fun (i : ι) ↦ G i)) i hy : (a : G y.fst) → G i) (y.snd (β := fun (i : ι) ↦ G i)) : G i) :
      P)

Tactic:
congr_arg _ ((equiv_iff ..).1 xy)

Premises used: congr_arg, FirstOrder.Language.DirectLimit.equiv_iff, Iff.mp
-- 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 : (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 j : (a : G j) → P) ((f i j hij : (a : G i) → G j) x : G j) : P)
      ((g i : (a : G i) → P) x : P)
x y : Σˣ (G := G) f
xy : x ≈ y
i : ι
hx : x.fst (β := fun (i : ι) ↦ G i) ≤ i
hy : y.fst (β := fun (i : ι) ↦ G i) ≤ i
⊢ Eq.{u₁ + 1} (α := P)
    ((g i : (a : G i) → P)
        ((f (x.fst (β := fun (i : ι) ↦ G i)) i hx : (a : G x.fst) → G i) (x.snd (β := fun (i : ι) ↦ G i)) : G i) :
      P)
    ((g i : (a : G i) → P)
        ((f (y.fst (β := fun (i : ι) ↦ G i)) i hy : (a : G y.fst) → G i) (y.snd (β := fun (i : ι) ↦ G i)) : G i) :
      P)

Tactic:
exact congr_arg _ ((equiv_iff ..).1 xy)

Premises used: congr_arg, FirstOrder.Language.DirectLimit.equiv_iff, Iff.mp
-- 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 : (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 j : (a : G j) → P) ((f i j hij : (a : G i) → G j) x : G j) : P)
      ((g i : (a : G i) → P) x : P)
x y : DirectLimit G f
xy :
  Eq.{u₁ + 1} (α := P)
    (Quotient.lift
      (fun (x : Σˣ (G := G) f) ↦
        (g (x.fst (β := fun (i : ι) ↦ G i)) : (a : G x.fst) → P) (x.snd (β := fun (i : ι) ↦ G i)))
      ⋯ x)
    (Quotient.lift
      (fun (x : Σˣ (G := G) f) ↦
        (g (x.fst (β := fun (i : ι) ↦ G i)) : (a : G x.fst) → P) (x.snd (β := fun (i : ι) ↦ G i)))
      ⋯ y)
⊢ Eq.{u₁ + 1} (α := P)
    ((g ((Quotient.out x).fst (β := fun (i : ι) ↦ G i)) : (a : G (Quotient.out x).fst) → P)
        ((Quotient.out x).snd (β := fun (i : ι) ↦ G i)) :
      P)
    ((g ((Quotient.out y).fst (β := fun (i : ι) ↦ G i)) : (a : G (Quotient.out y).fst) → P)
        ((Quotient.out y).snd (β := fun (i : ι) ↦ G i)) :
      P)

Tactic:
rw [← Quotient.out_eq x, ← Quotient.out_eq y, Quotient.lift_mk, Quotient.lift_mk] at xy

Premises used: Quotient.lift_mk, Quotient.out_eq
-- 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 : (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 j : (a : G j) → P) ((f i j hij : (a : G i) → G j) x : G j) : P)
      ((g i : (a : G i) → P) x : P)
x y : DirectLimit G f
xy :
  Eq.{u₁ + 1} (α := P)
    ((g ((Quotient.out x).fst (β := fun (i : ι) ↦ G i)) : (a : G (Quotient.out x).fst) → P)
        ((Quotient.out x).snd (β := fun (i : ι) ↦ G i)) :
      P)
    ((g ((Quotient.out y).fst (β := fun (i : ι) ↦ G i)) : (a : G (Quotient.out y).fst) → P)
        ((Quotient.out y).snd (β := fun (i : ι) ↦ G i)) :
      P)
obtain :
  ∀ (i : ι) (hx : (Quotient.out x).fst (β := fun (i : ι) ↦ G i) ≤ i)
    (hy : (Quotient.out y).fst (β := fun (i : ι) ↦ G i) ≤ i), x = y
⊢ x = y

Tactic:
obtain ⟨i, hx, hy⟩ := directed_of (· ≤ ·) x.out.1 y.out.1

Premises used: Quotient.out, Sigma.fst, LE.le, directed_of