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)
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 :
  ∀ (h : Eq (α := G k) ((f fst k ⋯ : (a : G fst) → G k) snd : G k) ((f fst_1 k ⋯ : (a : G fst_1) → G k) snd_1 : G k)),
    Eq (α := G k)
      ((f ((Sigma.mk (β := fun (i : ι) ↦ G i) fst snd).fst (β := fun (i : ι) ↦ G i)) k ⋯ : (a : G ⟨fst, snd⟩.fst) → G k)
          ((Sigma.mk (β := fun (i : ι) ↦ G i) fst snd).snd (β := fun (i : ι) ↦ G i)) :
        G k)
      ((f ((Sigma.mk (β := fun (i : ι) ↦ G i) fst_1 snd_1).fst (β := fun (i : ι) ↦ G i)) k ⋯ :
            (a : G ⟨fst_1, snd_1⟩.fst) → G k)
          ((Sigma.mk (β := fun (i : ι) ↦ G i) fst_1 snd_1).snd (β := fun (i : ι) ↦ G i)) :
        G k)
⊢ 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)

Tactic:
rw [DirectedSystem.map_map, DirectedSystem.map_map] at *

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)
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 fst k ⋯ : (a : G fst) → G k) snd : G k) ((f fst_1 k ⋯ : (a : G fst_1) → G k) snd_1 : G k)
⊢ Eq (α := G k)
    ((f ((Sigma.mk (β := fun (i : ι) ↦ G i) fst snd).fst (β := fun (i : ι) ↦ G i)) k ⋯ : (a : G ⟨fst, snd⟩.fst) → G k)
        ((Sigma.mk (β := fun (i : ι) ↦ G i) fst snd).snd (β := fun (i : ι) ↦ G i)) :
      G k)
    ((f ((Sigma.mk (β := fun (i : ι) ↦ G i) fst_1 snd_1).fst (β := fun (i : ι) ↦ G i)) k ⋯ :
          (a : G ⟨fst_1, snd_1⟩.fst) → G k)
        ((Sigma.mk (β := fun (i : ι) ↦ G i) fst_1 snd_1).snd (β := fun (i : ι) ↦ G i)) :
      G k)

Tactic:
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 fst k ⋯ : (a : G fst) → G k) snd : G k) ((f fst_1 k ⋯ : (a : G fst_1) → G k) snd_1 : G k)
⊢ Eq (α := G k)
    ((f ((Sigma.mk (β := fun (i : ι) ↦ G i) fst snd).fst (β := fun (i : ι) ↦ G i)) k ⋯ : (a : G ⟨fst, snd⟩.fst) → G k)
        ((Sigma.mk (β := fun (i : ι) ↦ G i) fst snd).snd (β := fun (i : ι) ↦ G i)) :
      G k)
    ((f ((Sigma.mk (β := fun (i : ι) ↦ G i) fst_1 snd_1).fst (β := fun (i : ι) ↦ G i)) k ⋯ :
          (a : G ⟨fst_1, snd_1⟩.fst) → G k)
        ((Sigma.mk (β := fun (i : ι) ↦ G i) fst_1 snd_1).snd (β := fun (i : ι) ↦ G i)) :
      G k)

Tactic:
exact 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)
n : ℕ
F : L.Functions n
x : Fin n → Σˣ (G := G) f
i j : ι
hi : i ∈ upperBounds (range (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ x))
hj : j ∈ upperBounds (range (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ x))
obtain :
  ∀ (k : ι) (ik : i ≤ k) (jk : j ≤ k),
    Structure.Sigma.mk (G := G) f i (funMap F (unify (G := G) f x i hi)) ≈
      Structure.Sigma.mk (G := G) f j (funMap F (unify (G := G) f x j hj))
⊢ Structure.Sigma.mk (G := G) f i (funMap F (unify (G := G) f x i hi)) ≈
    Structure.Sigma.mk (G := G) f j (funMap F (unify (G := G) f x j hj))

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)
n : ℕ
F : L.Functions n
x : Fin n → Σˣ (G := G) f
i j : ι
hi : i ∈ upperBounds (range (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ x))
hj : j ∈ upperBounds (range (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ x))
k : ι
ik : i ≤ k
jk : j ≤ k
⊢ Structure.Sigma.mk (G := G) f i (funMap F (unify (G := G) f x i hi)) ≈
    Structure.Sigma.mk (G := G) f j (funMap F (unify (G := G) f x j hj))

Tactic:
⟨k, ik, jk, ?_⟩

Premises used: 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)
n : ℕ
F : L.Functions n
x : Fin n → Σˣ (G := G) f
i j : ι
hi : i ∈ upperBounds (range (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ x))
hj : j ∈ upperBounds (range (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ x))
k : ι
ik : i ≤ k
jk : j ≤ k
refine :
  Eq (α := G k) ((f i k ik : (a : G i) → G k) (funMap F (unify (G := G) f x i hi)) : G k)
    ((f j k jk : (a : G j) → G k) (funMap F (unify (G := G) f x j hj)) : G k)
⊢ Structure.Sigma.mk (G := G) f i (funMap F (unify (G := G) f x i hi)) ≈
    Structure.Sigma.mk (G := G) f j (funMap F (unify (G := G) f x j hj))

Tactic:
refine ⟨k, ik, jk, ?_⟩
-- 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)
n : ℕ
F : L.Functions n
x : Fin n → Σˣ (G := G) f
i j : ι
hi : i ∈ upperBounds (range (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ x))
hj : j ∈ upperBounds (range (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ x))
k : ι
ik : i ≤ k
jk : j ≤ k
rw :
  Eq (α := G k) (funMap F ((⇑(f i k ik) : (a : G i) → G k) ∘ unify (G := G) f x i hi) : G k)
    ((f j k jk : (a : G j) → G k) (funMap F (unify (G := G) f x j hj)) : G k)
rw₁ :
  Eq (α := G k) (funMap F ((⇑(f i k ik) : (a : G i) → G k) ∘ unify (G := G) f x i hi))
    (funMap F ((⇑(f j k jk) : (a : G j) → G k) ∘ unify (G := G) f x j hj))
rw₂ : funMap F (unify (G := G) f x k ⋯) = funMap F ((⇑(f j k jk) : (a : G j) → G k) ∘ unify (G := G) f x j hj)
rw₃ rw₄ : funMap F (unify (G := G) f x k ⋯) = funMap F (unify (G := G) f x k ⋯)
⊢ Eq (α := G k) ((f i k ik : (a : G i) → G k) (funMap F (unify (G := G) f x i hi)) : G k)
    ((f j k jk : (a : G j) → G k) (funMap F (unify (G := G) f x j hj)) : G k)

Tactic:
rw [(f i k ik).map_fun, (f j k jk).map_fun, comp_unify, comp_unify]

Premises used: FirstOrder.Language.Embedding.map_fun, FirstOrder.Language.DirectLimit.comp_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 : IsDirectedOrder ι
inst_3 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
n : ℕ
R : L.Relations n
x : Fin n → Σˣ (G := G) f
i j : ι
hi : i ∈ upperBounds (range (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ x))
hj : j ∈ upperBounds (range (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ x))
obtain : ∀ (k : ι) (ik : i ≤ k) (jk : j ≤ k), RelMap R (unify (G := G) f x i hi) = RelMap R (unify (G := G) f x j hj)
⊢ RelMap R (unify (G := G) f x i hi) = RelMap R (unify (G := G) f x j hj)

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)
n : ℕ
R : L.Relations n
x : Fin n → Σˣ (G := G) f
i j : ι
hi : i ∈ upperBounds (range (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ x))
hj : j ∈ upperBounds (range (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ x))
k : ι
ik : i ≤ k
jk : j ≤ k
rw :
  RelMap (M := G k) R ((⇑(f i k ik) : (a : G i) → G k) ∘ unify (G := G) f x i hi) = RelMap R (unify (G := G) f x j hj)
rw₁ : RelMap R (unify (G := G) f x k ⋯) = RelMap R (unify (G := G) f x j hj)
rw₂ :
  RelMap R (unify (G := G) f x k ⋯) = RelMap (M := G k) R ((⇑(f j k jk) : (a : G j) → G k) ∘ unify (G := G) f x j hj)
rw₃ rw₄ : RelMap R (unify (G := G) f x k ⋯) = RelMap R (unify (G := G) f x k ⋯)
⊢ RelMap R (unify (G := G) f x i hi) = RelMap R (unify (G := G) f x j hj)

Tactic:
rw [← (f i k ik).map_rel, comp_unify, ← (f j k jk).map_rel, comp_unify]

Premises used: FirstOrder.Language.Embedding.map_rel, FirstOrder.Language.DirectLimit.comp_unify
-- 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 : IsDirectedOrder ι
inst_3 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
inst_4 : Nonempty ι
α : Type u_1
inst_5 : Finite α
x y : α → Σˣ (G := G) f
xy : x ≈ y
obtain :
  ∀ (i : ι)
    (hi :
      Membership.mem (γ := Set ι)
        (upperBounds
          (range.{v, u_1 + 1} (ι := α ⊕ α)
            (Sum.elim (fun (a : α) ↦ (x a).fst (β := fun (i : ι) ↦ G i)) fun (a : α) ↦
              (y a).fst (β := fun (i : ι) ↦ G i))))
        i),
    ∃ (i : ι) (hx : i ∈ upperBounds (range (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ x))) (hy :
      i ∈ upperBounds (range (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ y))),
      unify (G := G) f x i hx = unify (G := G) f y i hy
⊢ ∃ (i : ι) (hx : i ∈ upperBounds (range (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ x))) (hy :
    i ∈ upperBounds (range (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ y))), unify (G := G) f x i hx = unify (G := G) f y i hy

Tactic:
obtain ⟨i, hi⟩ := Finite.bddAbove_range (Sum.elim (fun a => (x a).1) fun a => (y a).1)

Premises used: Sigma.fst, Finite.bddAbove_range, Sum.elim
-- 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 : IsDirectedOrder ι
inst_3 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
inst_4 : Nonempty ι
α : Type u_1
inst_5 : Finite α
x y : α → Σˣ (G := G) f
xy : x ≈ y
i : ι
hi :
  Membership.mem (γ := Set ι)
    (upperBounds
      (range.{v, u_1 + 1} (ι := α ⊕ α)
        (Sum.elim (fun (a : α) ↦ (x a).fst (β := fun (i : ι) ↦ G i)) fun (a : α) ↦ (y a).fst (β := fun (i : ι) ↦ G i))))
    i
⊢ Membership.mem (γ := Set ι)
    (upperBounds (range fun (a : α) ↦ (x a).fst (β := fun (i : ι) ↦ G i)) ∩
      upperBounds (range fun (a : α) ↦ (y a).fst (β := fun (i : ι) ↦ G i)))
    i

Tactic:
rw [Sum.elim_range, upperBounds_union] at hi

Premises used: Set.Sum.elim_range, upperBounds_union
-- 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 : IsDirectedOrder ι
inst_3 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
inst_4 : Nonempty ι
α : Type u_1
inst_5 : Finite α
x y : α → Σˣ (G := G) f
xy : x ≈ y
i : ι
hi :
  Membership.mem (γ := Set ι)
    (upperBounds (range fun (a : α) ↦ (x a).fst (β := fun (i : ι) ↦ G i)) ∩
      upperBounds (range fun (a : α) ↦ (y a).fst (β := fun (i : ι) ↦ G i)))
    i
⊢ Membership.mem (γ := Set ι)
    (upperBounds (range fun (a : α) ↦ (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ x) a) ∩
      upperBounds (range fun (a : α) ↦ (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ y) a))
    i

Tactic:
simp_rw [← Function.comp_apply (f := Sigma.fst)] at hi

Premises used: Function.comp_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 : IsDirectedOrder ι
inst_3 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
inst_4 : Nonempty ι
α : Type u_1
inst_5 : Finite α
x y : α → Σˣ (G := G) f
xy : x ≈ y
i : ι
hi :
  Membership.mem (γ := Set ι)
    (upperBounds (range fun (a : α) ↦ (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ x) a) ∩
      upperBounds (range fun (a : α) ↦ (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ y) a))
    i
⊢ ∃ (i : ι) (hx : i ∈ upperBounds (range (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ x))) (hy :
    i ∈ upperBounds (range (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ y))), unify (G := G) f x i hx = unify (G := G) f y i hy

Tactic:
⟨i, hi.1, hi.2, funext fun a => (equiv_iff G f _ _).1 (xy a)⟩

Premises used: FirstOrder.Language.DirectLimit.equiv_iff, funext, And.right, And.left, Exists.intro, Iff.mp, FirstOrder.Language.DirectLimit.unify._proof_1
-- 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 : IsDirectedOrder ι
inst_3 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
inst_4 : Nonempty ι
α : Type u_1
inst_5 : Finite α
x y : α → Σˣ (G := G) f
xy : x ≈ y
i : ι
hi :
  Membership.mem (γ := Set ι)
    (upperBounds (range fun (a : α) ↦ (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ x) a) ∩
      upperBounds (range fun (a : α) ↦ (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ y) a))
    i
⊢ ∃ (i : ι) (hx : i ∈ upperBounds (range (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ x))) (hy :
    i ∈ upperBounds (range (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ y))), unify (G := G) f x i hx = unify (G := G) f y i hy

Tactic:
exact ⟨i, hi.1, hi.2, funext fun a => (equiv_iff G f _ _).1 (xy a)⟩
-- 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 ι
n : ℕ
F : L.Functions n
x : Fin n → Σˣ (G := G) f
i : ι
hi : i ∈ upperBounds (range (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ x))
⊢ funMap F x ≈ Structure.Sigma.mk (G := G) f i (funMap F (unify (G := G) f x i hi))

Tactic:
funMap_unify_equiv G f F x (Classical.choose (Finite.bddAbove_range fun a => (x a).1)) i _ hi

Premises used: Sigma.fst, Finite.bddAbove_range, Classical.choose, FirstOrder.Language.DirectLimit.funMap_unify_equiv
-- 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 ι
n : ℕ
R : L.Relations n
x : Fin n → Σˣ (G := G) f
i : ι
hi : i ∈ upperBounds (range (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ x))
⊢ RelMap R x = RelMap R (unify (G := G) f x i hi)

Tactic:
relMap_unify_equiv G f R x (Classical.choose (Finite.bddAbove_range fun a => (x a).1)) i _ hi

Premises used: FirstOrder.Language.DirectLimit.relMap_unify_equiv, Sigma.fst, Finite.bddAbove_range, Classical.choose
-- 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 ι
n : ℕ
F : L.Functions n
x y : Fin n → Σˣ (G := G) f
xy : x ≈ y
obtain :
  ∀ (i : ι) (hx : i ∈ upperBounds (range (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ x)))
    (hy : i ∈ upperBounds (range (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ y)))
    (h : unify (G := G) f x i hx = unify (G := G) f y i hy), funMap F x ≈ funMap F y
⊢ funMap F x ≈ funMap F y

Tactic:
obtain ⟨i, hx, hy, h⟩ := exists_unify_eq G f xy

Premises used: FirstOrder.Language.DirectLimit.exists_unify_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 ι
n : ℕ
F : L.Functions n
x y : Fin n → Σˣ (G := G) f
xy : x ≈ y
i : ι
hx : i ∈ upperBounds (range (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ x))
hy : i ∈ upperBounds (range (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ y))
h : unify (G := G) f x i hx = unify (G := G) f y i hy
⊢ funMap F x ≈ funMap F y

Tactic:
Setoid.trans (funMap_equiv_unify G f F x i hx)
        (Setoid.trans ?_ (Setoid.symm (funMap_equiv_unify G f F y i hy)))

Premises used: FirstOrder.Language.DirectLimit.funMap_equiv_unify, Setoid.symm, Setoid.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 : IsDirectedOrder ι
inst_3 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
inst_4 : Nonempty ι
n : ℕ
F : L.Functions n
x y : Fin n → Σˣ (G := G) f
xy : x ≈ y
i : ι
hx : i ∈ upperBounds (range (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ x))
hy : i ∈ upperBounds (range (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ y))
h : unify (G := G) f x i hx = unify (G := G) f y i hy
G₁ :
  Structure.Sigma.mk (G := G) f i (funMap F (unify (G := G) f x i hx)) ≈
    Structure.Sigma.mk (G := G) f i (funMap F (unify (G := G) f y i hy))
⊢ funMap F x ≈ funMap F y

Tactic:
refine
      Setoid.trans (funMap_equiv_unify G f F x i hx)
        (Setoid.trans ?_ (Setoid.symm (funMap_equiv_unify G f F y i hy)))

Premises used: FirstOrder.Language.DirectLimit.funMap_equiv_unify, Setoid.symm, Setoid.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 : IsDirectedOrder ι
inst_3 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
inst_4 : Nonempty ι
n : ℕ
F : L.Functions n
x y : Fin n → Σˣ (G := G) f
xy : x ≈ y
i : ι
hx : i ∈ upperBounds (range (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ x))
hy : i ∈ upperBounds (range (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ y))
h : unify (G := G) f x i hx = unify (G := G) f y i hy
rw rw₁ :
  (setoid G f : Σˣ f → Σˣ f → Prop) (Structure.Sigma.mk (G := G) f i (funMap F (unify (G := G) f y i hy)))
    (Structure.Sigma.mk (G := G) f i (funMap F (unify (G := G) f y i hy)))
⊢ Structure.Sigma.mk (G := G) f i (funMap F (unify (G := G) f x i hx)) ≈
    Structure.Sigma.mk (G := G) f i (funMap F (unify (G := G) f y i hy))

Tactic:
rw [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)
inst_4 : Nonempty ι
n : ℕ
R : L.Relations n
x y : Fin n → Σˣ (G := G) f
xy : x ≈ y
obtain :
  ∀ (i : ι) (hx : i ∈ upperBounds (range (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ x)))
    (hy : i ∈ upperBounds (range (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ y)))
    (h : unify (G := G) f x i hx = unify (G := G) f y i hy), RelMap R x = RelMap R y
⊢ RelMap R x = RelMap R y

Tactic:
obtain ⟨i, hx, hy, h⟩ := exists_unify_eq G f xy

Premises used: FirstOrder.Language.DirectLimit.exists_unify_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 ι
n : ℕ
R : L.Relations n
x y : Fin n → Σˣ (G := G) f
xy : x ≈ y
i : ι
hx : i ∈ upperBounds (range (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ x))
hy : i ∈ upperBounds (range (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ y))
h : unify (G := G) f x i hx = unify (G := G) f y i hy
⊢ RelMap R x = RelMap R y

Tactic:
_root_.trans (relMap_equiv_unify G f R x i hx)
      (_root_.trans ?_ (symm (relMap_equiv_unify G f R y i hy)))

Premises used: trans, symm, FirstOrder.Language.DirectLimit.relMap_equiv_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 : IsDirectedOrder ι
inst_3 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
inst_4 : Nonempty ι
n : ℕ
R : L.Relations n
x y : Fin n → Σˣ (G := G) f
xy : x ≈ y
i : ι
hx : i ∈ upperBounds (range (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ x))
hy : i ∈ upperBounds (range (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ y))
h : unify (G := G) f x i hx = unify (G := G) f y i hy
refine : RelMap R (unify (G := G) f x i hx) = RelMap R (unify (G := G) f y i hy)
⊢ RelMap R x = RelMap R y

Tactic:
refine _root_.trans (relMap_equiv_unify G f R x i hx)
      (_root_.trans ?_ (symm (relMap_equiv_unify G f R y i hy)))

Premises used: trans, symm, FirstOrder.Language.DirectLimit.relMap_equiv_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 : IsDirectedOrder ι
inst_3 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
inst_4 : Nonempty ι
n : ℕ
R : L.Relations n
x y : Fin n → Σˣ (G := G) f
xy : x ≈ y
i : ι
hx : i ∈ upperBounds (range (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ x))
hy : i ∈ upperBounds (range (Sigma.fst (β := fun (i : ι) ↦ G i) ∘ y))
h : unify (G := G) f x i hx = unify (G := G) f y i hy
rw rw₁ : RelMap R (unify (G := G) f y i hy) = RelMap R (unify (G := G) f y i hy)
⊢ RelMap R (unify (G := G) f x i hx) = RelMap R (unify (G := G) f y i hy)

Tactic:
rw [h]