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 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
α : Type u_1
i : ι
x : α → G i
a : α
⊢ ((f ((Structure.Sigma.mk (G := G) f i (x a)).fst (β := fun (i : ι) ↦ G i)) i ⋯ :
          G ((Structure.Sigma.mk (G := G) f i (x a)).fst (β := fun (i : ι) ↦ G i)) ↪[L] G i) :
        (a : G (Structure.Sigma.mk f i (x a)).fst) → G i)
      ((Structure.Sigma.mk (G := G) f i (x a)).snd (β := fun (i : ι) ↦ G i)) =
    x a

Tactic:
apply 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_2, u_3, w} L (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst_2 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
α : Type u_1
x : α → Σˣ (G := G) f
i j : ι
ij : i ≤ j
h : i ∈ upperBounds (range (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ x))
h₁ : ∀ (a : α), ((⇑(f i j ij) : (a : G i) → G j) ∘ unify (G := G) f x i h) a = unify (G := G) f x j ⋯ a
⊢ (⇑(f i j ij) : (a : G i) → G j) ∘ unify (G := G) f x i h = unify (G := G) f x j ⋯

Tactic:
ext 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 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
α : Type u_1
x : α → Σˣ (G := G) f
i j : ι
ij : i ≤ j
h : i ∈ upperBounds (range (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ x))
a : α
⊢ ((⇑(f i j ij) : (a : G i) → G j) ∘ unify (G := G) f x i h) a = unify (G := G) f x j ⋯ a

Tactic:
simp [unify, DirectedSystem.map_map]

Premises used: FirstOrder.Language.DirectedSystem.map_map, FirstOrder.Language.DirectLimit.unify
-- 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 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
inst_3 : IsDirectedOrder ι
x_1 x_2 x_3 : Σˣ (G := G) f
i : ι
x : G i
j : ι
y : G j
h :
  match (motive := Σˣ (G := G) f → Prop) Sigma.mk (β := fun (i : ι) ↦ G i) i x with
  | ⟨i, x⟩ =>
    match (motive := Σˣ (G := G) f → Prop) Sigma.mk (β := fun (i : ι) ↦ G i) j y with
    | ⟨j, y⟩ =>
      ∃ (k : ι) (ik : i ≤ k) (jk : j ≤ k),
        Eq (α := G k) ((f i k ik : (a : G i) → G k) x : G k) ((f j k jk : (a : G j) → G k) y : G k)
k : ι
z : G k
h_1 :
  match (motive := Σˣ (G := G) f → Prop) Sigma.mk (β := fun (i : ι) ↦ G i) j y with
  | ⟨i, x⟩ =>
    match (motive := Σˣ (G := G) f → Prop) Sigma.mk (β := fun (i : ι) ↦ G i) k z with
    | ⟨j, y⟩ =>
      ∃ (k : ι) (ik : i ≤ k) (jk : j ≤ k),
        Eq (α := G k) ((f i k ik : (a : G i) → G k) x : G k) ((f j k jk : (a : G j) → G k) y : G k)
ij : ι
hiij : i ≤ ij
hjij : j ≤ ij
hij : Eq (α := G ij) ((f i ij hiij : (a : G i) → G ij) x : G ij) ((f j ij hjij : (a : G j) → G ij) y : G ij)
jk : ι
hjjk : j ≤ jk
hkjk : k ≤ jk
hjk : Eq (α := G jk) ((f j jk hjjk : (a : G j) → G jk) y : G jk) ((f k jk hkjk : (a : G k) → G jk) z : G jk)
obtain :
  ∀ (ijk : ι) (hijijk : ij ≤ ijk) (hjkijk : jk ≤ ijk),
    match (motive := Σˣ (G := G) f → Prop) Sigma.mk (β := fun (i : ι) ↦ G i) i x with
    | ⟨i, x⟩ =>
      match (motive := Σˣ (G := G) f → Prop) Sigma.mk (β := fun (i : ι) ↦ G i) k z with
      | ⟨j, y⟩ =>
        ∃ (k : ι) (ik : i ≤ k) (jk : j ≤ k),
          Eq (α := G k) ((f i k ik : (a : G i) → G k) x : G k) ((f j k jk : (a : G j) → G k) y : G k)
⊢ match (motive := Σˣ (G := G) f → Prop) Sigma.mk (β := fun (i : ι) ↦ G i) i x with
  | ⟨i, x⟩ =>
    match (motive := Σˣ (G := G) f → Prop) Sigma.mk (β := fun (i : ι) ↦ G i) k z with
    | ⟨j, y⟩ =>
      ∃ (k : ι) (ik : i ≤ k) (jk : j ≤ k),
        Eq (α := G k) ((f i k ik : (a : G i) → G k) x : G k) ((f j k jk : (a : G j) → G k) y : G k)

Tactic:
obtain ⟨ijk, hijijk, hjkijk⟩ := directed_of (· ≤ ·) ij jk

Premises used: 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 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
inst_3 : IsDirectedOrder ι
x_1 x_2 x_3 : Σˣ (G := G) f
i : ι
x : G i
j : ι
y : G j
h :
  match (motive := Σˣ (G := G) f → Prop) Sigma.mk (β := fun (i : ι) ↦ G i) i x with
  | ⟨i, x⟩ =>
    match (motive := Σˣ (G := G) f → Prop) Sigma.mk (β := fun (i : ι) ↦ G i) j y with
    | ⟨j, y⟩ =>
      ∃ (k : ι) (ik : i ≤ k) (jk : j ≤ k),
        Eq (α := G k) ((f i k ik : (a : G i) → G k) x : G k) ((f j k jk : (a : G j) → G k) y : G k)
k : ι
z : G k
h_1 :
  match (motive := Σˣ (G := G) f → Prop) Sigma.mk (β := fun (i : ι) ↦ G i) j y with
  | ⟨i, x⟩ =>
    match (motive := Σˣ (G := G) f → Prop) Sigma.mk (β := fun (i : ι) ↦ G i) k z with
    | ⟨j, y⟩ =>
      ∃ (k : ι) (ik : i ≤ k) (jk : j ≤ k),
        Eq (α := G k) ((f i k ik : (a : G i) → G k) x : G k) ((f j k jk : (a : G j) → G k) y : G k)
ij : ι
hiij : i ≤ ij
hjij : j ≤ ij
hij : Eq (α := G ij) ((f i ij hiij : (a : G i) → G ij) x : G ij) ((f j ij hjij : (a : G j) → G ij) y : G ij)
jk : ι
hjjk : j ≤ jk
hkjk : k ≤ jk
hjk : Eq (α := G jk) ((f j jk hjjk : (a : G j) → G jk) y : G jk) ((f k jk hkjk : (a : G k) → G jk) z : G jk)
ijk : ι
hijijk : ij ≤ ijk
hjkijk : jk ≤ ijk
⊢ match (motive := Σˣ (G := G) f → Prop) Sigma.mk (β := fun (i : ι) ↦ G i) i x with
  | ⟨i, x⟩ =>
    match (motive := Σˣ (G := G) f → Prop) Sigma.mk (β := fun (i : ι) ↦ G i) k z with
    | ⟨j, y⟩ =>
      ∃ (k : ι) (ik : i ≤ k) (jk : j ≤ k),
        Eq (α := G k) ((f i k ik : (a : G i) → G k) x : G k) ((f j k jk : (a : G j) → G k) y : G k)

Tactic:
⟨ijk, le_trans hiij hijijk, le_trans hkjk hjkijk, ?_⟩

Premises used: Exists.intro, le_trans
-- 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 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
inst_3 : IsDirectedOrder ι
x_1 x_2 x_3 : Σˣ (G := G) f
i : ι
x : G i
j : ι
y : G j
h :
  match (motive := Σˣ (G := G) f → Prop) Sigma.mk (β := fun (i : ι) ↦ G i) i x with
  | ⟨i, x⟩ =>
    match (motive := Σˣ (G := G) f → Prop) Sigma.mk (β := fun (i : ι) ↦ G i) j y with
    | ⟨j, y⟩ =>
      ∃ (k : ι) (ik : i ≤ k) (jk : j ≤ k),
        Eq (α := G k) ((f i k ik : (a : G i) → G k) x : G k) ((f j k jk : (a : G j) → G k) y : G k)
k : ι
z : G k
h_1 :
  match (motive := Σˣ (G := G) f → Prop) Sigma.mk (β := fun (i : ι) ↦ G i) j y with
  | ⟨i, x⟩ =>
    match (motive := Σˣ (G := G) f → Prop) Sigma.mk (β := fun (i : ι) ↦ G i) k z with
    | ⟨j, y⟩ =>
      ∃ (k : ι) (ik : i ≤ k) (jk : j ≤ k),
        Eq (α := G k) ((f i k ik : (a : G i) → G k) x : G k) ((f j k jk : (a : G j) → G k) y : G k)
ij : ι
hiij : i ≤ ij
hjij : j ≤ ij
hij : Eq (α := G ij) ((f i ij hiij : (a : G i) → G ij) x : G ij) ((f j ij hjij : (a : G j) → G ij) y : G ij)
jk : ι
hjjk : j ≤ jk
hkjk : k ≤ jk
hjk : Eq (α := G jk) ((f j jk hjjk : (a : G j) → G jk) y : G jk) ((f k jk hkjk : (a : G k) → G jk) z : G jk)
ijk : ι
hijijk : ij ≤ ijk
hjkijk : jk ≤ ijk
refine : Eq (α := G ijk) ((f i ijk ⋯ : (a : G i) → G ijk) x : G ijk) ((f k ijk ⋯ : (a : G k) → G ijk) z : G ijk)
⊢ match (motive := Σˣ (G := G) f → Prop) Sigma.mk (β := fun (i : ι) ↦ G i) i x with
  | ⟨i, x⟩ =>
    match (motive := Σˣ (G := G) f → Prop) Sigma.mk (β := fun (i : ι) ↦ G i) k z with
    | ⟨j, y⟩ =>
      ∃ (k : ι) (ik : i ≤ k) (jk : j ≤ k),
        Eq (α := G k) ((f i k ik : (a : G i) → G k) x : G k) ((f j k jk : (a : G j) → G k) y : G k)

Tactic:
refine ⟨ijk, le_trans hiij hijijk, le_trans hkjk hjkijk, ?_⟩
-- 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 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
inst_3 : IsDirectedOrder ι
x_1 x_2 x_3 : Σˣ (G := G) f
i : ι
x : G i
j : ι
y : G j
h :
  match (motive := Σˣ (G := G) f → Prop) Sigma.mk (β := fun (i : ι) ↦ G i) i x with
  | ⟨i, x⟩ =>
    match (motive := Σˣ (G := G) f → Prop) Sigma.mk (β := fun (i : ι) ↦ G i) j y with
    | ⟨j, y⟩ =>
      ∃ (k : ι) (ik : i ≤ k) (jk : j ≤ k),
        Eq (α := G k) ((f i k ik : (a : G i) → G k) x : G k) ((f j k jk : (a : G j) → G k) y : G k)
k : ι
z : G k
h_1 :
  match (motive := Σˣ (G := G) f → Prop) Sigma.mk (β := fun (i : ι) ↦ G i) j y with
  | ⟨i, x⟩ =>
    match (motive := Σˣ (G := G) f → Prop) Sigma.mk (β := fun (i : ι) ↦ G i) k z with
    | ⟨j, y⟩ =>
      ∃ (k : ι) (ik : i ≤ k) (jk : j ≤ k),
        Eq (α := G k) ((f i k ik : (a : G i) → G k) x : G k) ((f j k jk : (a : G j) → G k) y : G k)
ij : ι
hiij : i ≤ ij
hjij : j ≤ ij
hij : Eq (α := G ij) ((f i ij hiij : (a : G i) → G ij) x : G ij) ((f j ij hjij : (a : G j) → G ij) y : G ij)
jk : ι
hjjk : j ≤ jk
hkjk : k ≤ jk
hjk : Eq (α := G jk) ((f j jk hjjk : (a : G j) → G jk) y : G jk) ((f k jk hkjk : (a : G k) → G jk) z : G jk)
ijk : ι
hijijk : ij ≤ ijk
hjkijk : jk ≤ ijk
rw : Eq (α := G ijk) ((f j ijk ⋯ : (a : G j) → G ijk) y : G ijk) ((f k ijk ⋯ : (a : G k) → G ijk) z : G ijk)
⊢ Eq (α := G ijk) ((f i ijk ⋯ : (a : G i) → G ijk) x : G ijk) ((f k ijk ⋯ : (a : G k) → G ijk) z : G ijk)

Tactic:
rw [← DirectedSystem.map_map _ hiij hijijk, hij, DirectedSystem.map_map]

Premises used: FirstOrder.Language.DirectedSystem.map_map
-- 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 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
inst_3 : IsDirectedOrder ι
x_1 x_2 x_3 : Σˣ (G := G) f
i : ι
x : G i
j : ι
y : G j
h :
  match (motive := Σˣ (G := G) f → Prop) Sigma.mk (β := fun (i : ι) ↦ G i) i x with
  | ⟨i, x⟩ =>
    match (motive := Σˣ (G := G) f → Prop) Sigma.mk (β := fun (i : ι) ↦ G i) j y with
    | ⟨j, y⟩ =>
      ∃ (k : ι) (ik : i ≤ k) (jk : j ≤ k),
        Eq (α := G k) ((f i k ik : (a : G i) → G k) x : G k) ((f j k jk : (a : G j) → G k) y : G k)
k : ι
z : G k
h_1 :
  match (motive := Σˣ (G := G) f → Prop) Sigma.mk (β := fun (i : ι) ↦ G i) j y with
  | ⟨i, x⟩ =>
    match (motive := Σˣ (G := G) f → Prop) Sigma.mk (β := fun (i : ι) ↦ G i) k z with
    | ⟨j, y⟩ =>
      ∃ (k : ι) (ik : i ≤ k) (jk : j ≤ k),
        Eq (α := G k) ((f i k ik : (a : G i) → G k) x : G k) ((f j k jk : (a : G j) → G k) y : G k)
ij : ι
hiij : i ≤ ij
hjij : j ≤ ij
hij : Eq (α := G ij) ((f i ij hiij : (a : G i) → G ij) x : G ij) ((f j ij hjij : (a : G j) → G ij) y : G ij)
jk : ι
hjjk : j ≤ jk
hkjk : k ≤ jk
hjk : Eq (α := G jk) ((f j jk hjjk : (a : G j) → G jk) y : G jk) ((f k jk hkjk : (a : G k) → G jk) z : G jk)
ijk : ι
hijijk : ij ≤ ijk
hjkijk : jk ≤ ijk
rw :
  Eq (α := G ijk) ((f j ijk ⋯ : (a : G j) → G ijk) y : G ijk)
    ((f jk ijk hjkijk : (a : G jk) → G ijk) ((f k jk hkjk : (a : G k) → G jk) z : G jk) : G ijk)
rw₁ :
  Eq (α := G ijk) ((f j ijk ⋯ : (a : G j) → G ijk) y : G ijk)
    ((f jk ijk hjkijk : (a : G jk) → G ijk) ((f j jk hjjk : (a : G j) → G jk) y : G jk) : G ijk)
rw₂ rw₃ : Eq (α := G ijk) ((f j ijk ⋯ : (a : G j) → G ijk) y : G ijk) ((f j ijk ⋯ : (a : G j) → G ijk) y : G ijk)
⊢ Eq (α := G ijk) ((f j ijk ⋯ : (a : G j) → G ijk) y : G ijk) ((f k ijk ⋯ : (a : G k) → G ijk) z : G ijk)

Tactic:
rw [← DirectedSystem.map_map _ hkjk hjkijk, ← hjk, DirectedSystem.map_map]

Premises used: FirstOrder.Language.DirectedSystem.map_map
-- 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)
x y : Σˣ (G := G) f
i : ι
hx : x.fst (β := fun (i : ι) ↦ G i) ≤ i
hy : y.fst (β := fun (i : ι) ↦ G i) ≤ i
mk :
  ∀ (fst : ι) (snd : G fst) (hx : (Sigma.mk (β := fun (i : ι) ↦ G i) fst snd).fst (β := fun (i : ι) ↦ G i) ≤ i),
    Sigma.mk (β := fun (i : ι) ↦ G i) fst snd ≈ y ↔
      Eq (α := G i)
        ((f ((Sigma.mk (β := fun (i : ι) ↦ G i) fst snd).fst (β := fun (i : ι) ↦ G i)) i hx :
              (a : G ⟨fst, snd⟩.fst) → G i)
            ((Sigma.mk (β := fun (i : ι) ↦ G i) fst snd).snd (β := fun (i : ι) ↦ G i)) :
          G i)
        ((f (y.fst (β := fun (i : ι) ↦ G i)) i hy : (a : G y.fst) → G i) (y.snd (β := fun (i : ι) ↦ G i)) : G i)
⊢ x ≈ y ↔
    Eq (α := G i)
      ((f (x.fst (β := fun (i : ι) ↦ G i)) i hx : (a : G x.fst) → G i) (x.snd (β := fun (i : ι) ↦ G i)) : G i)
      ((f (y.fst (β := fun (i : ι) ↦ G i)) i hy : (a : G y.fst) → G i) (y.snd (β := fun (i : ι) ↦ G i)) : G i)

Tactic:
cases x
-- 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)
y : Σˣ (G := G) f
i : ι
hy : y.fst (β := fun (i : ι) ↦ G i) ≤ i
fst : ι
snd : G fst
hx : (Sigma.mk (β := fun (i : ι) ↦ G i) fst snd).fst (β := fun (i : ι) ↦ G i) ≤ i
mk :
  ∀ (fst_1 : ι) (snd_1 : G fst_1)
    (hy : (Sigma.mk (β := fun (i : ι) ↦ G i) fst_1 snd_1).fst (β := fun (i : ι) ↦ G i) ≤ i),
    Sigma.mk (β := fun (i : ι) ↦ G i) fst snd ≈ Sigma.mk (β := fun (i : ι) ↦ G i) fst_1 snd_1 ↔
      Eq (α := G i)
        ((f ((Sigma.mk (β := fun (i : ι) ↦ G i) fst snd).fst (β := fun (i : ι) ↦ G i)) i hx :
              (a : G ⟨fst, snd⟩.fst) → G i)
            ((Sigma.mk (β := fun (i : ι) ↦ G i) fst snd).snd (β := fun (i : ι) ↦ G i)) :
          G i)
        ((f ((Sigma.mk (β := fun (i : ι) ↦ G i) fst_1 snd_1).fst (β := fun (i : ι) ↦ G i)) i hy :
              (a : G ⟨fst_1, snd_1⟩.fst) → G i)
            ((Sigma.mk (β := fun (i : ι) ↦ G i) fst_1 snd_1).snd (β := fun (i : ι) ↦ G i)) :
          G i)
⊢ Sigma.mk (β := fun (i : ι) ↦ G i) fst snd ≈ y ↔
    Eq (α := G i)
      ((f ((Sigma.mk (β := fun (i : ι) ↦ G i) fst snd).fst (β := fun (i : ι) ↦ G i)) i hx :
            (a : G ⟨fst, snd⟩.fst) → G i)
          ((Sigma.mk (β := fun (i : ι) ↦ G i) fst snd).snd (β := fun (i : ι) ↦ G i)) :
        G i)
      ((f (y.fst (β := fun (i : ι) ↦ G i)) i hy : (a : G y.fst) → G i) (y.snd (β := fun (i : ι) ↦ G i)) : G i)

Tactic:
cases y
-- 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)
i fst : ι
snd : G fst
hx : (Sigma.mk (β := fun (i : ι) ↦ G i) fst snd).fst (β := fun (i : ι) ↦ G i) ≤ i
fst_1 : ι
snd_1 : G fst_1
hy : (Sigma.mk (β := fun (i : ι) ↦ G i) fst_1 snd_1).fst (β := fun (i : ι) ↦ G i) ≤ i
⊢ Sigma.mk (β := fun (i : ι) ↦ G i) fst snd ≈ Sigma.mk (β := fun (i : ι) ↦ G i) fst_1 snd_1 ↔
    Eq (α := G i)
      ((f ((Sigma.mk (β := fun (i : ι) ↦ G i) fst snd).fst (β := fun (i : ι) ↦ G i)) i hx :
            (a : G ⟨fst, snd⟩.fst) → G i)
          ((Sigma.mk (β := fun (i : ι) ↦ G i) fst snd).snd (β := fun (i : ι) ↦ G i)) :
        G i)
      ((f ((Sigma.mk (β := fun (i : ι) ↦ G i) fst_1 snd_1).fst (β := fun (i : ι) ↦ G i)) i hy :
            (a : G ⟨fst_1, snd_1⟩.fst) → G i)
          ((Sigma.mk (β := fun (i : ι) ↦ G i) fst_1 snd_1).snd (β := fun (i : ι) ↦ G i)) :
        G i)

Tactic:
⟨fun xy => ?_, fun xy => ⟨i, hx, hy, xy⟩⟩

Premises used: Iff.intro, Exists.intro
-- 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)
i fst : ι
snd : G fst
hx : (Sigma.mk (β := fun (i : ι) ↦ G i) fst snd).fst (β := fun (i : ι) ↦ G i) ≤ i
fst_1 : ι
snd_1 : G fst_1
hy : (Sigma.mk (β := fun (i : ι) ↦ G i) fst_1 snd_1).fst (β := fun (i : ι) ↦ G i) ≤ i
mk :
  ∀ (xy : Sigma.mk (β := fun (i : ι) ↦ G i) fst snd ≈ Sigma.mk (β := fun (i : ι) ↦ G i) fst_1 snd_1),
    Eq (α := G i)
      ((f ((Sigma.mk (β := fun (i : ι) ↦ G i) fst snd).fst (β := fun (i : ι) ↦ G i)) i hx :
            (a : G ⟨fst, snd⟩.fst) → G i)
          ((Sigma.mk (β := fun (i : ι) ↦ G i) fst snd).snd (β := fun (i : ι) ↦ G i)) :
        G i)
      ((f ((Sigma.mk (β := fun (i : ι) ↦ G i) fst_1 snd_1).fst (β := fun (i : ι) ↦ G i)) i hy :
            (a : G ⟨fst_1, snd_1⟩.fst) → G i)
          ((Sigma.mk (β := fun (i : ι) ↦ G i) fst_1 snd_1).snd (β := fun (i : ι) ↦ G i)) :
        G i)
⊢ Sigma.mk (β := fun (i : ι) ↦ G i) fst snd ≈ Sigma.mk (β := fun (i : ι) ↦ G i) fst_1 snd_1 ↔
    Eq (α := G i)
      ((f ((Sigma.mk (β := fun (i : ι) ↦ G i) fst snd).fst (β := fun (i : ι) ↦ G i)) i hx :
            (a : G ⟨fst, snd⟩.fst) → G i)
          ((Sigma.mk (β := fun (i : ι) ↦ G i) fst snd).snd (β := fun (i : ι) ↦ G i)) :
        G i)
      ((f ((Sigma.mk (β := fun (i : ι) ↦ G i) fst_1 snd_1).fst (β := fun (i : ι) ↦ G i)) i hy :
            (a : G ⟨fst_1, snd_1⟩.fst) → G i)
          ((Sigma.mk (β := fun (i : ι) ↦ G i) fst_1 snd_1).snd (β := fun (i : ι) ↦ G i)) :
        G i)

Tactic:
refine ⟨fun xy => ?_, fun xy => ⟨i, hx, hy, xy⟩⟩
-- 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)
i fst : ι
snd : G fst
hx : (Sigma.mk (β := fun (i : ι) ↦ G i) fst snd).fst (β := fun (i : ι) ↦ G i) ≤ i
fst_1 : ι
snd_1 : G fst_1
hy : (Sigma.mk (β := fun (i : ι) ↦ G i) fst_1 snd_1).fst (β := fun (i : ι) ↦ G i) ≤ i
xy : Sigma.mk (β := fun (i : ι) ↦ G i) fst snd ≈ Sigma.mk (β := fun (i : ι) ↦ G i) fst_1 snd_1
mk :
  ∀ (j : ι) (w : fst ≤ j) (w_1 : fst_1 ≤ j)
    (h : Eq (α := G j) ((f fst j w : (a : G fst) → G j) snd : G j) ((f fst_1 j w_1 : (a : G fst_1) → G j) snd_1 : G j)),
    Eq (α := G i)
      ((f ((Sigma.mk (β := fun (i : ι) ↦ G i) fst snd).fst (β := fun (i : ι) ↦ G i)) i hx :
            (a : G ⟨fst, snd⟩.fst) → G i)
          ((Sigma.mk (β := fun (i : ι) ↦ G i) fst snd).snd (β := fun (i : ι) ↦ G i)) :
        G i)
      ((f ((Sigma.mk (β := fun (i : ι) ↦ G i) fst_1 snd_1).fst (β := fun (i : ι) ↦ G i)) i hy :
            (a : G ⟨fst_1, snd_1⟩.fst) → G i)
          ((Sigma.mk (β := fun (i : ι) ↦ G i) fst_1 snd_1).snd (β := fun (i : ι) ↦ G i)) :
        G i)
⊢ Eq (α := G i)
    ((f ((Sigma.mk (β := fun (i : ι) ↦ G i) fst snd).fst (β := fun (i : ι) ↦ G i)) i hx : (a : G ⟨fst, snd⟩.fst) → G i)
        ((Sigma.mk (β := fun (i : ι) ↦ G i) fst snd).snd (β := fun (i : ι) ↦ G i)) :
      G i)
    ((f ((Sigma.mk (β := fun (i : ι) ↦ G i) fst_1 snd_1).fst (β := fun (i : ι) ↦ G i)) i hy :
          (a : G ⟨fst_1, snd_1⟩.fst) → G i)
        ((Sigma.mk (β := fun (i : ι) ↦ G i) fst_1 snd_1).snd (β := fun (i : ι) ↦ G i)) :
      G i)

Tactic:
obtain ⟨j, _, _, h⟩ := xy
-- 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)
i fst : ι
snd : G fst
hx : (Sigma.mk (β := fun (i : ι) ↦ G i) fst snd).fst (β := fun (i : ι) ↦ G i) ≤ i
fst_1 : ι
snd_1 : G fst_1
hy : (Sigma.mk (β := fun (i : ι) ↦ G i) fst_1 snd_1).fst (β := fun (i : ι) ↦ G i) ≤ i
j : ι
w : fst ≤ j
w_1 : fst_1 ≤ j
h : Eq (α := G j) ((f fst j w : (a : G fst) → G j) snd : G j) ((f fst_1 j w_1 : (a : G fst_1) → G j) snd_1 : G j)
mk :
  ∀ (k : ι) (ik : i ≤ k) (jk : j ≤ k),
    Eq (α := G i)
      ((f ((Sigma.mk (β := fun (i : ι) ↦ G i) fst snd).fst (β := fun (i : ι) ↦ G i)) i hx :
            (a : G ⟨fst, snd⟩.fst) → G i)
          ((Sigma.mk (β := fun (i : ι) ↦ G i) fst snd).snd (β := fun (i : ι) ↦ G i)) :
        G i)
      ((f ((Sigma.mk (β := fun (i : ι) ↦ G i) fst_1 snd_1).fst (β := fun (i : ι) ↦ G i)) i hy :
            (a : G ⟨fst_1, snd_1⟩.fst) → G i)
          ((Sigma.mk (β := fun (i : ι) ↦ G i) fst_1 snd_1).snd (β := fun (i : ι) ↦ G i)) :
        G i)
⊢ Eq (α := G i)
    ((f ((Sigma.mk (β := fun (i : ι) ↦ G i) fst snd).fst (β := fun (i : ι) ↦ G i)) i hx : (a : G ⟨fst, snd⟩.fst) → G i)
        ((Sigma.mk (β := fun (i : ι) ↦ G i) fst snd).snd (β := fun (i : ι) ↦ G i)) :
      G i)
    ((f ((Sigma.mk (β := fun (i : ι) ↦ G i) fst_1 snd_1).fst (β := fun (i : ι) ↦ G i)) i hy :
          (a : G ⟨fst_1, snd_1⟩.fst) → G i)
        ((Sigma.mk (β := fun (i : ι) ↦ G i) fst_1 snd_1).snd (β := fun (i : ι) ↦ G i)) :
      G i)

Tactic:
obtain ⟨k, ik, jk⟩ := directed_of (· ≤ ·) i j

Premises used: 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)
i fst : ι
snd : G fst
hx : (Sigma.mk (β := fun (i : ι) ↦ G i) fst snd).fst (β := fun (i : ι) ↦ G i) ≤ i
fst_1 : ι
snd_1 : G fst_1
hy : (Sigma.mk (β := fun (i : ι) ↦ G i) fst_1 snd_1).fst (β := fun (i : ι) ↦ G i) ≤ i
j : ι
w : fst ≤ j
w_1 : fst_1 ≤ j
h : Eq (α := G j) ((f fst j w : (a : G fst) → G j) snd : G j) ((f fst_1 j w_1 : (a : G fst_1) → G j) snd_1 : G j)
k : ι
ik : i ≤ k
jk : j ≤ k
⊢ Eq (α := G k) ((f j k jk : (a : G j) → G k) ((f fst j w : (a : G fst) → G j) snd : G j) : G k)
    ((f j k jk : (a : G j) → G k) ((f fst_1 j w_1 : (a : G fst_1) → G j) snd_1 : G j) : G k)

Tactic:
have h := congr_arg (f j k jk) h
-- 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)
i fst : ι
snd : G fst
hx : (Sigma.mk (β := fun (i : ι) ↦ G i) fst snd).fst (β := fun (i : ι) ↦ G i) ≤ i
fst_1 : ι
snd_1 : G fst_1
hy : (Sigma.mk (β := fun (i : ι) ↦ G i) fst_1 snd_1).fst (β := fun (i : ι) ↦ G i) ≤ i
j : ι
w : fst ≤ j
w_1 : fst_1 ≤ j
h_1 : Eq (α := G j) ((f fst j w : (a : G fst) → G j) snd : G j) ((f fst_1 j w_1 : (a : G fst_1) → G j) snd_1 : G j)
k : ι
ik : i ≤ k
jk : j ≤ k
h :
  Eq (α := G k) ((f j k jk : (a : G j) → G k) ((f fst j w : (a : G fst) → G j) snd : G j) : G k)
    ((f j k jk : (a : G j) → G k) ((f fst_1 j w_1 : (a : G fst_1) → G j) snd_1 : G j) : G k)
mk :
  Eq (α := G k)
    ((f i k ik : (a : G i) → G k)
        ((f ((Sigma.mk (β := fun (i : ι) ↦ G i) fst snd).fst (β := fun (i : ι) ↦ G i)) i hx :
              (a : G ⟨fst, snd⟩.fst) → G i)
            ((Sigma.mk (β := fun (i : ι) ↦ G i) fst snd).snd (β := fun (i : ι) ↦ G i)) :
          G i) :
      G k)
    ((f i k ik : (a : G i) → G k)
        ((f ((Sigma.mk (β := fun (i : ι) ↦ G i) fst_1 snd_1).fst (β := fun (i : ι) ↦ G i)) i hy :
              (a : G ⟨fst_1, snd_1⟩.fst) → G i)
            ((Sigma.mk (β := fun (i : ι) ↦ G i) fst_1 snd_1).snd (β := fun (i : ι) ↦ G i)) :
          G i) :
      G k)
⊢ Eq (α := G i)
    ((f ((Sigma.mk (β := fun (i : ι) ↦ G i) fst snd).fst (β := fun (i : ι) ↦ G i)) i hx : (a : G ⟨fst, snd⟩.fst) → G i)
        ((Sigma.mk (β := fun (i : ι) ↦ G i) fst snd).snd (β := fun (i : ι) ↦ G i)) :
      G i)
    ((f ((Sigma.mk (β := fun (i : ι) ↦ G i) fst_1 snd_1).fst (β := fun (i : ι) ↦ G i)) i hy :
          (a : G ⟨fst_1, snd_1⟩.fst) → G i)
        ((Sigma.mk (β := fun (i : ι) ↦ G i) fst_1 snd_1).snd (β := fun (i : ι) ↦ G i)) :
      G i)

Tactic:
apply (f i k ik).injective

Premises used: FirstOrder.Language.Embedding.injective