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 ι
n : ℕ
F : L.Functions n
i : ι
x : Fin n → G i
simp :
  (setoid G f : Σˣ f → Σˣ f → Prop) (funMap F fun (i_1 : Fin n) ↦ Structure.Sigma.mk (G := G) f i (x i_1))
    (Structure.Sigma.mk (G := G) f i (funMap F x))
⊢ (funMap F fun (a : Fin n) ↦ ⟦Structure.Sigma.mk (G := G) f i (x a)⟧) = ⟦Structure.Sigma.mk (G := G) f i (funMap F x)⟧

Tactic:
simp only [funMap_quotient_mk', Quotient.eq]

Premises used: FirstOrder.Language.funMap_quotient_mk', 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 ι
n : ℕ
F : L.Functions n
i : ι
x : Fin n → G i
obtain :
  ∀ (k : ι) (ik : i ≤ k)
    (jk : Classical.choose (p := Membership.mem (γ := Set ι) (upperBounds (range fun (x : Fin n) ↦ i))) ⋯ ≤ k),
    (setoid G f : Σˣ f → Σˣ f → Prop) (funMap F fun (i_1 : Fin n) ↦ Structure.Sigma.mk (G := G) f i (x i_1))
      (Structure.Sigma.mk (G := G) f i (funMap F x))
⊢ (setoid G f : Σˣ f → Σˣ f → Prop) (funMap F fun (i_1 : Fin n) ↦ Structure.Sigma.mk (G := G) f i (x i_1))
    (Structure.Sigma.mk (G := G) f i (funMap F x))

Tactic:
obtain ⟨k, ik, jk⟩ :=
    directed_of (· ≤ ·) i (Classical.choose (Finite.bddAbove_range fun _ : Fin n => i))

Premises used: LE.le, Finite.bddAbove_range, directed_of, 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
i : ι
x : Fin n → G i
k : ι
ik : i ≤ k
jk : Classical.choose (p := Membership.mem (γ := Set ι) (upperBounds (range fun (x : Fin n) ↦ i))) ⋯ ≤ k
⊢ (setoid G f : Σˣ f → Σˣ f → Prop) (funMap F fun (i_1 : Fin n) ↦ Structure.Sigma.mk (G := G) f i (x i_1))
    (Structure.Sigma.mk (G := G) f i (funMap F x))

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

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)
inst_4 : Nonempty ι
n : ℕ
F : L.Functions n
i : ι
x : Fin n → G i
k : ι
ik : i ≤ k
jk : Classical.choose (p := Membership.mem (γ := Set ι) (upperBounds (range fun (x : Fin n) ↦ i))) ⋯ ≤ k
refine :
  Eq (α := G k)
    ((f
            (Classical.choose (p :=
              Membership.mem (γ := Set ι)
                (upperBounds
                  (range fun (a : Fin n) ↦
                    Sigma.fst (β := fun (i : ι) ↦ G i)
                      ((fun (i_1 : Fin n) ↦ Structure.Sigma.mk (G := G) f i (x i_1)) a))))
              ⋯)
            k jk :
          (a : G (Classical.choose ⋯)) → G k)
        (funMap F
            (unify (G := G) f (fun (i_1 : Fin n) ↦ Structure.Sigma.mk (G := G) f i (x i_1))
              (Classical.choose (p :=
                Membership.mem (γ := Set ι)
                  (upperBounds
                    (range fun (a : Fin n) ↦
                      Sigma.fst (β := fun (i : ι) ↦ G i)
                        ((fun (i_1 : Fin n) ↦ Structure.Sigma.mk (G := G) f i (x i_1)) a))))
                ⋯)
              ⋯) :
          G
            (Classical.choose (p :=
              Membership.mem (γ := Set ι)
                (upperBounds
                  (range fun (a : Fin n) ↦
                    Sigma.fst (β := fun (i : ι) ↦ G i)
                      ((fun (i_1 : Fin n) ↦ Structure.Sigma.mk (G := G) f i (x i_1)) a))))
              ⋯)) :
      G k)
    ((f i k ik : (a : G i) → G k) (funMap F x) : G k)
⊢ (setoid G f : Σˣ f → Σˣ f → Prop) (funMap F fun (i_1 : Fin n) ↦ Structure.Sigma.mk (G := G) f i (x i_1))
    (Structure.Sigma.mk (G := G) f i (funMap F x))

Tactic:
refine ⟨k, jk, ik, ?_⟩
-- 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
i : ι
x : Fin n → G i
k : ι
ik : i ≤ k
jk : Classical.choose (p := Membership.mem (γ := Set ι) (upperBounds (range fun (x : Fin n) ↦ i))) ⋯ ≤ k
simp :
  funMap F (unify (G := G) f (fun (i_1 : Fin n) ↦ Structure.Sigma.mk (G := G) f i (x i_1)) k ⋯) =
    funMap F ((⇑(f i k ik) : (a : G i) → G k) ∘ x)
⊢ Eq (α := G k)
    ((f
            (Classical.choose (p :=
              Membership.mem (γ := Set ι)
                (upperBounds
                  (range fun (a : Fin n) ↦
                    Sigma.fst (β := fun (i : ι) ↦ G i)
                      ((fun (i_1 : Fin n) ↦ Structure.Sigma.mk (G := G) f i (x i_1)) a))))
              ⋯)
            k jk :
          (a : G (Classical.choose ⋯)) → G k)
        (funMap F
            (unify (G := G) f (fun (i_1 : Fin n) ↦ Structure.Sigma.mk (G := G) f i (x i_1))
              (Classical.choose (p :=
                Membership.mem (γ := Set ι)
                  (upperBounds
                    (range fun (a : Fin n) ↦
                      Sigma.fst (β := fun (i : ι) ↦ G i)
                        ((fun (i_1 : Fin n) ↦ Structure.Sigma.mk (G := G) f i (x i_1)) a))))
                ⋯)
              ⋯) :
          G
            (Classical.choose (p :=
              Membership.mem (γ := Set ι)
                (upperBounds
                  (range fun (a : Fin n) ↦
                    Sigma.fst (β := fun (i : ι) ↦ G i)
                      ((fun (i_1 : Fin n) ↦ Structure.Sigma.mk (G := G) f i (x i_1)) a))))
              ⋯)) :
      G k)
    ((f i k ik : (a : G i) → G k) (funMap F x) : G k)

Tactic:
simp only [Embedding.map_fun, 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)
inst_4 : Nonempty ι
n : ℕ
F : L.Functions n
i : ι
x : Fin n → G i
k : ι
ik : i ≤ k
jk : Classical.choose (p := Membership.mem (γ := Set ι) (upperBounds (range fun (x : Fin n) ↦ i))) ⋯ ≤ k
⊢ funMap F (unify (G := G) f (fun (i_1 : Fin n) ↦ Structure.Sigma.mk (G := G) f i (x i_1)) k ⋯) =
    funMap F ((⇑(f i k ik) : (a : G i) → G k) ∘ 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 ι
n : ℕ
R : L.Relations n
i : ι
x : Fin n → G i
rw : (RelMap (M := Σˣ (G := G) f) R fun (a : Fin n) ↦ Structure.Sigma.mk (G := G) f i (x a)) = RelMap R x
⊢ (RelMap (M := Quotient (setoid G f)) R fun (a : Fin n) ↦ ⟦Structure.Sigma.mk (G := G) f i (x a)⟧) = RelMap R x

Tactic:
rw [relMap_quotient_mk']

Premises used: FirstOrder.Language.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 ι
n : ℕ
R : L.Relations n
i : ι
x : Fin n → G i
rw : RelMap R (unify (G := G) f (fun (a : Fin n) ↦ Structure.Sigma.mk (G := G) f i (x a)) i ⋯) = RelMap R x
⊢ (RelMap (M := Σˣ (G := G) f) R fun (a : Fin n) ↦ Structure.Sigma.mk (G := G) f i (x a)) = RelMap R x

Tactic:
rw [relMap_equiv_unify G f R (fun a => .mk f i (x a)) i (fun _ ⟨_, hj⟩ => le_of_eq hj.symm)]

Premises used: FirstOrder.Language.Structure.Sigma.mk, _private.0.FirstOrder.Language.DirectLimit.relMap_quotient_mk'_sigma_mk'.match_1, LE.le, FirstOrder.Language.DirectLimit.relMap_equiv_unify, le_of_eq, Eq.symm
-- 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
i : ι
x : Fin n → G i
rw rw₁ : RelMap R x = RelMap R x
⊢ RelMap R (unify (G := G) f (fun (a : Fin n) ↦ Structure.Sigma.mk (G := G) f i (x a)) i ⋯) = RelMap R x

Tactic:
rw [unify_sigma_mk_self]

Premises used: FirstOrder.Language.DirectLimit.unify_sigma_mk_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 : 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 : α → DirectLimit G f
obtain :
  ∀ (i : ι)
    (hi :
      Membership.mem (γ := Set ι) (upperBounds (range fun (a : α) ↦ (Quotient.out (x a)).fst (β := fun (i : ι) ↦ G i)))
        i),
    ∃ (i : ι) (y : α → G i), x = fun (a : α) ↦ ⟦Structure.Sigma.mk (G := G) f i (y a)⟧
⊢ ∃ (i : ι) (y : α → G i), x = fun (a : α) ↦ ⟦Structure.Sigma.mk (G := G) f i (y a)⟧

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

Premises used: Quotient.out, Sigma.fst, Finite.bddAbove_range
-- 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 : α → DirectLimit G f
i : ι
hi : Membership.mem (γ := Set ι) (upperBounds (range fun (a : α) ↦ (Quotient.out (x a)).fst (β := fun (i : ι) ↦ G i))) i
⊢ ∃ (i : ι) (y : α → G i), x = fun (a : α) ↦ ⟦Structure.Sigma.mk (G := G) f i (y a)⟧

Tactic:
⟨i, unify f (Quotient.out ∘ x) i hi, ?_⟩

Premises used: Function.comp, Quotient.out, Exists.intro, FirstOrder.Language.DirectLimit.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 : α → DirectLimit G f
i : ι
hi : Membership.mem (γ := Set ι) (upperBounds (range fun (a : α) ↦ (Quotient.out (x a)).fst (β := fun (i : ι) ↦ G i))) i
refine : x = fun (a : α) ↦ ⟦Structure.Sigma.mk (G := G) f i (unify (G := G) f (Quotient.out ∘ x) i hi a)⟧
⊢ ∃ (i : ι) (y : α → G i), x = fun (a : α) ↦ ⟦Structure.Sigma.mk (G := G) f i (y a)⟧

Tactic:
refine ⟨i, unify f (Quotient.out ∘ x) i hi, ?_⟩
-- 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 : α → DirectLimit G f
i : ι
hi : Membership.mem (γ := Set ι) (upperBounds (range fun (a : α) ↦ (Quotient.out (x a)).fst (β := fun (i : ι) ↦ G i))) i
h : ∀ (a : α), x a = ⟦Structure.Sigma.mk (G := G) f i (unify (G := G) f (Quotient.out ∘ x) i hi a)⟧
⊢ x = fun (a : α) ↦ ⟦Structure.Sigma.mk (G := G) f i (unify (G := G) f (Quotient.out ∘ x) i hi a)⟧

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 : 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 : α → DirectLimit G f
i : ι
hi : Membership.mem (γ := Set ι) (upperBounds (range fun (a : α) ↦ (Quotient.out (x a)).fst (β := fun (i : ι) ↦ G i))) i
a : α
h :
  Quotient.out (x a) ≈
    Structure.Sigma.mk (G := G) f i
      ((f (((Quotient.out ∘ x) a).fst (β := fun (i : ι) ↦ G i)) i ⋯ : (a : G ((Quotient.out ∘ x) a).fst) → G i)
        (((Quotient.out ∘ x) a).snd (β := fun (i : ι) ↦ G i)))
⊢ x a = ⟦Structure.Sigma.mk (G := G) f i (unify (G := G) f (Quotient.out ∘ x) i hi a)⟧

Tactic:
rw [Quotient.eq_mk_iff_out, unify]

Premises used: Quotient.eq_mk_iff_out, FirstOrder.Language.DirectLimit.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 : α → DirectLimit G f
i : ι
hi : Membership.mem (γ := Set ι) (upperBounds (range fun (a : α) ↦ (Quotient.out (x a)).fst (β := fun (i : ι) ↦ G i))) i
a : α
h :
  ∀ (r : ((Quotient.out ∘ x) a).fst (β := fun (i : ι) ↦ G i) ≤ i),
    Quotient.out (x a) ≈
      Structure.Sigma.mk (G := G) f i
        ((f (((Quotient.out ∘ x) a).fst (β := fun (i : ι) ↦ G i)) i r : (a : G ((Quotient.out ∘ x) a).fst) → G i)
          (((Quotient.out ∘ x) a).snd (β := fun (i : ι) ↦ G i)))
⊢ Quotient.out (x a) ≈
    Structure.Sigma.mk (G := G) f i
      ((f (((Quotient.out ∘ x) a).fst (β := fun (i : ι) ↦ G i)) i ⋯ : (a : G ((Quotient.out ∘ x) a).fst) → G i)
        (((Quotient.out ∘ x) a).snd (β := fun (i : ι) ↦ G i)))

Tactic:
generalize_proofs r
-- 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 : α → DirectLimit G f
i : ι
hi : Membership.mem (γ := Set ι) (upperBounds (range fun (a : α) ↦ (Quotient.out (x a)).fst (β := fun (i : ι) ↦ G i))) i
a : α
r : ((Quotient.out ∘ x) a).fst (β := fun (i : ι) ↦ G i) ≤ i
h :
  Quotient.out (x a) ≈
    Structure.Sigma.mk (G := G) f i
      ((f ((Quotient.out (x a)).fst (β := fun (i : ι) ↦ G i)) i r : (a : G (Quotient.out (x a)).fst) → G i)
        ((Quotient.out (x a)).snd (β := fun (i : ι) ↦ G i)))
⊢ Quotient.out (x a) ≈
    Structure.Sigma.mk (G := G) f i
      ((f (((Quotient.out ∘ x) a).fst (β := fun (i : ι) ↦ G i)) i r : (a : G ((Quotient.out ∘ x) a).fst) → G i)
        (((Quotient.out ∘ x) a).snd (β := fun (i : ι) ↦ G i)))

Tactic:
change _ ≈ Structure.Sigma.mk f i (f (Quotient.out (x a)).fst i r (Quotient.out (x a)).snd)

Premises used: FirstOrder.Language.Structure.Sigma.mk, Quotient.out, Sigma.fst, Sigma.snd, DFunLike.coe
-- 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 : α → DirectLimit G f
i : ι
hi : Membership.mem (γ := Set ι) (upperBounds (range fun (a : α) ↦ (Quotient.out (x a)).fst (β := fun (i : ι) ↦ G i))) i
a : α
r : ((Quotient.out ∘ x) a).fst (β := fun (i : ι) ↦ G i) ≤ i
⊢ (Structure.Sigma.mk (G := G) f i
          ((f ((Quotient.out (x a)).fst (β := fun (i : ι) ↦ G i)) i r : (a : G (Quotient.out (x a)).fst) → G i)
            ((Quotient.out (x a)).snd (β := fun (i : ι) ↦ G i)))).fst
      (β := fun (i : ι) ↦ G i) ≤
    i

Tactic:
have : (.mk f i (f (Quotient.out (x a)).fst i r (Quotient.out (x a)).snd) : Σˣ f).fst ≤ i :=
    le_rfl
-- 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 : α → DirectLimit G f
i : ι
hi : Membership.mem (γ := Set ι) (upperBounds (range fun (a : α) ↦ (Quotient.out (x a)).fst (β := fun (i : ι) ↦ G i))) i
a : α
r : ((Quotient.out ∘ x) a).fst (β := fun (i : ι) ↦ G i) ≤ i
this :
  (Structure.Sigma.mk (G := G) f i
          ((f ((Quotient.out (x a)).fst (β := fun (i : ι) ↦ G i)) i r : (a : G (Quotient.out (x a)).fst) → G i)
            ((Quotient.out (x a)).snd (β := fun (i : ι) ↦ G i)))).fst
      (β := fun (i : ι) ↦ G i) ≤
    i
h :
  Eq (α := G i)
    ((f ((Quotient.out (x a)).fst (β := fun (i : ι) ↦ G i)) i ⋯ : (a : G (Quotient.out (x a)).fst) → G i)
        ((Quotient.out (x a)).snd (β := fun (i : ι) ↦ G i)) :
      G i)
    ((f
            ((Structure.Sigma.mk (G := G) f i
                  ((f ((Quotient.out (x a)).fst (β := fun (i : ι) ↦ G i)) i r : (a : G (Quotient.out (x a)).fst) → G i)
                    ((Quotient.out (x a)).snd (β := fun (i : ι) ↦ G i)))).fst
              (β := fun (i : ι) ↦ G i))
            i this :
          (a :
              G
                (Structure.Sigma.mk f i
                    ((f (Quotient.out (x a)).fst i r : (a : G (Quotient.out (x a)).fst) → G i)
                      (Quotient.out (x a)).snd)).fst) →
            G i)
        ((Structure.Sigma.mk (G := G) f i
              ((f ((Quotient.out (x a)).fst (β := fun (i : ι) ↦ G i)) i r : (a : G (Quotient.out (x a)).fst) → G i)
                ((Quotient.out (x a)).snd (β := fun (i : ι) ↦ G i)))).snd
          (β := fun (i : ι) ↦ G i)) :
      G i)
rw :
  Membership.mem (γ := Set ι) (range fun (a : α) ↦ (Quotient.out (x a)).fst (β := fun (i : ι) ↦ G i))
    ((Quotient.out (x a)).fst (β := fun (i : ι) ↦ G i))
⊢ Quotient.out (x a) ≈
    Structure.Sigma.mk (G := G) f i
      ((f ((Quotient.out (x a)).fst (β := fun (i : ι) ↦ G i)) i r : (a : G (Quotient.out (x a)).fst) → G i)
        ((Quotient.out (x a)).snd (β := fun (i : ι) ↦ G i)))

Tactic:
rw [equiv_iff G f (i := i) (hi _) this]

Premises used: FirstOrder.Language.DirectLimit.equiv_iff
-- 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 : α → DirectLimit G f
i : ι
hi : Membership.mem (γ := Set ι) (upperBounds (range fun (a : α) ↦ (Quotient.out (x a)).fst (β := fun (i : ι) ↦ G i))) i
a : α
r : ((Quotient.out ∘ x) a).fst (β := fun (i : ι) ↦ G i) ≤ i
this :
  (Structure.Sigma.mk (G := G) f i
          ((f ((Quotient.out (x a)).fst (β := fun (i : ι) ↦ G i)) i r : (a : G (Quotient.out (x a)).fst) → G i)
            ((Quotient.out (x a)).snd (β := fun (i : ι) ↦ G i)))).fst
      (β := fun (i : ι) ↦ G i) ≤
    i
⊢ Eq (α := G i)
    ((f ((Quotient.out (x a)).fst (β := fun (i : ι) ↦ G i)) i ⋯ : (a : G (Quotient.out (x a)).fst) → G i)
        ((Quotient.out (x a)).snd (β := fun (i : ι) ↦ G i)) :
      G i)
    ((f
            ((Structure.Sigma.mk (G := G) f i
                  ((f ((Quotient.out (x a)).fst (β := fun (i : ι) ↦ G i)) i r : (a : G (Quotient.out (x a)).fst) → G i)
                    ((Quotient.out (x a)).snd (β := fun (i : ι) ↦ G i)))).fst
              (β := fun (i : ι) ↦ G i))
            i this :
          (a :
              G
                (Structure.Sigma.mk f i
                    ((f (Quotient.out (x a)).fst i r : (a : G (Quotient.out (x a)).fst) → G i)
                      (Quotient.out (x a)).snd)).fst) →
            G i)
        ((Structure.Sigma.mk (G := G) f i
              ((f ((Quotient.out (x a)).fst (β := fun (i : ι) ↦ G i)) i r : (a : G (Quotient.out (x a)).fst) → G i)
                ((Quotient.out (x a)).snd (β := fun (i : ι) ↦ G i)))).snd
          (β := fun (i : ι) ↦ G i)) :
      G i)

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_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 : α → DirectLimit G f
i : ι
hi : Membership.mem (γ := Set ι) (upperBounds (range fun (a : α) ↦ (Quotient.out (x a)).fst (β := fun (i : ι) ↦ G i))) i
a : α
r : ((Quotient.out ∘ x) a).fst (β := fun (i : ι) ↦ G i) ≤ i
this :
  (Structure.Sigma.mk (G := G) f i
          ((f ((Quotient.out (x a)).fst (β := fun (i : ι) ↦ G i)) i r : (a : G (Quotient.out (x a)).fst) → G i)
            ((Quotient.out (x a)).snd (β := fun (i : ι) ↦ G i)))).fst
      (β := fun (i : ι) ↦ G i) ≤
    i
⊢ Membership.mem (γ := Set ι) (range fun (a : α) ↦ (Quotient.out (x a)).fst (β := fun (i : ι) ↦ G i))
    ((Quotient.out (x a)).fst (β := fun (i : ι) ↦ G i))

Tactic:
⟨a, rfl⟩

Premises used: Set.Mem, setOf, Exists.intro, Set.range, rfl
-- 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 : α → DirectLimit G f
i : ι
hi : Membership.mem (γ := Set ι) (upperBounds (range fun (a : α) ↦ (Quotient.out (x a)).fst (β := fun (i : ι) ↦ G i))) i
a : α
r : ((Quotient.out ∘ x) a).fst (β := fun (i : ι) ↦ G i) ≤ i
this :
  (Structure.Sigma.mk (G := G) f i
          ((f ((Quotient.out (x a)).fst (β := fun (i : ι) ↦ G i)) i r : (a : G (Quotient.out (x a)).fst) → G i)
            ((Quotient.out (x a)).snd (β := fun (i : ι) ↦ G i)))).fst
      (β := fun (i : ι) ↦ G i) ≤
    i
⊢ Membership.mem (γ := Set ι) (range fun (a : α) ↦ (Quotient.out (x a)).fst (β := fun (i : ι) ↦ G i))
    ((Quotient.out (x a)).fst (β := fun (i : ι) ↦ G i))

Tactic:
exact ⟨a, 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 : ι
x y : G i
h :
  Eq (α := DirectLimit G f) ((fun (a : G i) ↦ ⟦Structure.Sigma.mk (G := G) f i a⟧) x)
    ((fun (a : G i) ↦ ⟦Structure.Sigma.mk (G := G) f i a⟧) y)
⊢ (setoid G f : Σˣ f → Σˣ f → Prop) (Structure.Sigma.mk (G := G) f i x) (Structure.Sigma.mk (G := G) f i y)

Tactic:
rw [Quotient.eq] at h

Premises used: 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 : ι
x y : G i
h : (setoid G f : Σˣ f → Σˣ f → Prop) (Structure.Sigma.mk (G := G) f i x) (Structure.Sigma.mk (G := G) f i y)
obtain :
  ∀ (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
⊢ x = y

Tactic:
obtain ⟨j, h1, _, h3⟩ := h