awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.DirectLimit
Goal:
L : Language
ι : Type v
inst : Preorder ι
G : ι → Type w
inst_1 : (i : ι) → Structure.{u_1, u_2, w} L (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst_2 : IsDirectedOrder ι
inst_3 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
inst_4 : Nonempty ι
P : Type u₁
inst_5 : L.Structure P
g : (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)
i : ι
hx : (Quotient.out x).fst (β := fun (i : ι) ↦ G i) ≤ i
hy : (Quotient.out y).fst (β := fun (i : ι) ↦ G i) ≤ i
⊢ (Quotient.out y).fst (β := fun (i : ι) ↦ G i) ≤ i

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

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

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

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

Tactic:
rw [← Quotient.out_eq x, ← Quotient.out_eq y, Quotient.eq_iff_equiv, equiv_iff G f hx hy]

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

Tactic:
(g i).injective xy

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

Tactic:
exact (g i).injective xy

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 ι
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)
n : ℕ
F : L.Functions n
x : Fin n → DirectLimit G f
obtain :
  ∀ (i : ι) (y : Fin n → G i),
    Eq.{u₁ + 1} (α := P)
      (Quotient.lift (s := setoid G f)
        (fun (x : Σˣ (G := G) f) ↦
          (g (x.fst (β := fun (i : ι) ↦ G i)) : (a : G x.fst) → P) (x.snd (β := fun (i : ι) ↦ G i)))
        ⋯ (funMap F fun (a : Fin n) ↦ ⟦Structure.Sigma.mk (G := G) f i (y a)⟧))
      (funMap F
        (Function.comp (β := DirectLimit G f)
          (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)))
            ⋯)
          fun (a : Fin n) ↦ ⟦Structure.Sigma.mk (G := G) f i (y a)⟧))
⊢ 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)))
      ⋯ (funMap F x))
    (funMap F
      (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))

Tactic:
obtain ⟨i, y, rfl⟩ := exists_quotient_mk'_sigma_mk'_eq G f x

Premises used: FirstOrder.Language.DirectLimit.exists_quotient_mk'_sigma_mk'_eq, 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 ι
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)
n : ℕ
F : L.Functions n
i : ι
y : Fin n → G i
change :
  Eq.{u₁ + 1} (α := P)
    (Quotient.lift (s := setoid G f)
      (fun (x : Σˣ (G := G) f) ↦
        (g (x.fst (β := fun (i : ι) ↦ G i)) : (a : G x.fst) → P) (x.snd (β := fun (i : ι) ↦ G i)))
      ⋯ (funMap F fun (a : Fin n) ↦ ⟦Structure.Sigma.mk (G := G) f i (y a)⟧))
    (funMap F
      (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)))
          ⋯ ∘
        Quotient.mk (setoid G f) ∘ Structure.Sigma.mk (G := G) f i ∘ y))
⊢ Eq.{u₁ + 1} (α := P)
    (Quotient.lift (s := setoid G f)
      (fun (x : Σˣ (G := G) f) ↦
        (g (x.fst (β := fun (i : ι) ↦ G i)) : (a : G x.fst) → P) (x.snd (β := fun (i : ι) ↦ G i)))
      ⋯ (funMap F fun (a : Fin n) ↦ ⟦Structure.Sigma.mk (G := G) f i (y a)⟧))
    (funMap F
      (Function.comp (β := DirectLimit G f)
        (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)))
          ⋯)
        fun (a : Fin n) ↦ ⟦Structure.Sigma.mk (G := G) f i (y a)⟧))

Tactic:
change _ = funMap F (Quotient.lift _ _ ∘ Quotient.mk _ ∘ Structure.Sigma.mk f i ∘ y)

Premises used: FirstOrder.Language.Structure.Sigma.mk, Function.comp, Quotient.mk, Quotient.lift, FirstOrder.Language.Structure.funMap
-- 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)
n : ℕ
F : L.Functions n
i : ι
y : Fin n → G i
rw :
  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)))
      ⋯ ⟦Structure.Sigma.mk (G := G) f i (funMap F y)⟧)
    (funMap F
      ((fun (x : Σˣ (G := G) f) ↦
          (g (x.fst (β := fun (i : ι) ↦ G i)) : (a : G x.fst) → P) (x.snd (β := fun (i : ι) ↦ G i))) ∘
        Structure.Sigma.mk (G := G) f i ∘ y))
⊢ Eq.{u₁ + 1} (α := P)
    (Quotient.lift (s := setoid G f)
      (fun (x : Σˣ (G := G) f) ↦
        (g (x.fst (β := fun (i : ι) ↦ G i)) : (a : G x.fst) → P) (x.snd (β := fun (i : ι) ↦ G i)))
      ⋯ (funMap F fun (a : Fin n) ↦ ⟦Structure.Sigma.mk (G := G) f i (y a)⟧))
    (funMap F
      (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)))
          ⋯ ∘
        Quotient.mk (setoid G f) ∘ Structure.Sigma.mk (G := G) f i ∘ y))

Tactic:
rw [funMap_quotient_mk'_sigma_mk', ← Function.comp_assoc, Quotient.lift_comp_mk]

Premises used: Quotient.lift_comp_mk, FirstOrder.Language.DirectLimit.funMap_quotient_mk'_sigma_mk', Function.comp_assoc
-- 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)
n : ℕ
F : L.Functions n
i : ι
y : Fin n → G i
simp :
  Eq.{u₁ + 1} (α := P) (funMap F ((⇑(g i) : (a : G i) → P) ∘ y))
    (funMap F
      ((fun (x : Σˣ (G := G) f) ↦
          (g (x.fst (β := fun (i : ι) ↦ G i)) : (a : G x.fst) → P) (x.snd (β := fun (i : ι) ↦ G i))) ∘
        Structure.Sigma.mk (G := G) f i ∘ y))
⊢ 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)))
      ⋯ ⟦Structure.Sigma.mk (G := G) f i (funMap F y)⟧)
    (funMap F
      ((fun (x : Σˣ (G := G) f) ↦
          (g (x.fst (β := fun (i : ι) ↦ G i)) : (a : G x.fst) → P) (x.snd (β := fun (i : ι) ↦ G i))) ∘
        Structure.Sigma.mk (G := G) f i ∘ y))

Tactic:
simp only [Quotient.lift_mk, Embedding.map_fun]

Premises used: Quotient.lift_mk, FirstOrder.Language.Embedding.map_fun
-- 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)
n : ℕ
F : L.Functions n
i : ι
y : Fin n → G i
⊢ Eq.{u₁ + 1} (α := P) (funMap F ((⇑(g i) : (a : G i) → P) ∘ y))
    (funMap F
      ((fun (x : Σˣ (G := G) f) ↦
          (g (x.fst (β := fun (i : ι) ↦ G i)) : (a : G x.fst) → P) (x.snd (β := fun (i : ι) ↦ G i))) ∘
        Structure.Sigma.mk (G := G) f i ∘ y))

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 ι
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)
n : ℕ
R : L.Relations n
x : Fin n → DirectLimit G f
obtain :
  ∀ (i : ι) (y : Fin n → G i),
    RelMap.{u_1, u_2, u₁} (M := P) R
        (Function.comp (β := DirectLimit G f)
          (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)))
            ⋯)
          fun (a : Fin n) ↦ ⟦Structure.Sigma.mk (G := G) f i (y a)⟧) ↔
      RelMap (M := DirectLimit G f) R fun (a : Fin n) ↦ ⟦Structure.Sigma.mk (G := G) f i (y a)⟧
⊢ RelMap.{u_1, u_2, u₁} (M := P) R
      (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) ↔
    RelMap R x

Tactic:
obtain ⟨i, y, rfl⟩ := exists_quotient_mk'_sigma_mk'_eq G f x

Premises used: FirstOrder.Language.DirectLimit.exists_quotient_mk'_sigma_mk'_eq, 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 ι
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)
n : ℕ
R : L.Relations n
i : ι
y : Fin n → G i
change :
  RelMap.{u_1, u_2, u₁} (M := P) R
      (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)))
          ⋯ ∘
        Quotient.mk (setoid G f) ∘ Structure.Sigma.mk (G := G) f i ∘ y) ↔
    RelMap (M := DirectLimit G f) R fun (a : Fin n) ↦ ⟦Structure.Sigma.mk (G := G) f i (y a)⟧
⊢ RelMap.{u_1, u_2, u₁} (M := P) R
      (Function.comp (β := DirectLimit G f)
        (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)))
          ⋯)
        fun (a : Fin n) ↦ ⟦Structure.Sigma.mk (G := G) f i (y a)⟧) ↔
    RelMap (M := DirectLimit G f) R fun (a : Fin n) ↦ ⟦Structure.Sigma.mk (G := G) f i (y a)⟧

Tactic:
change RelMap R (Quotient.lift _ _ ∘ Quotient.mk _ ∘ Structure.Sigma.mk f i ∘ y) ↔ _

Premises used: FirstOrder.Language.Structure.Sigma.mk, Function.comp, FirstOrder.Language.Structure.RelMap, Quotient.mk, Quotient.lift
-- 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)
n : ℕ
R : L.Relations n
i : ι
y : Fin n → G i
rw :
  RelMap.{u_1, u_2, u₁} (M := P) R
      ((fun (x : Σˣ (G := G) f) ↦
          (g (x.fst (β := fun (i : ι) ↦ G i)) : (a : G x.fst) → P) (x.snd (β := fun (i : ι) ↦ G i))) ∘
        Structure.Sigma.mk (G := G) f i ∘ y) ↔
    RelMap.{u_1, u_2, u₁} (M := P) R ((⇑(g i) : (a : G i) → P) ∘ y)
⊢ RelMap.{u_1, u_2, u₁} (M := P) R
      (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)))
          ⋯ ∘
        Quotient.mk (setoid G f) ∘ Structure.Sigma.mk (G := G) f i ∘ y) ↔
    RelMap (M := DirectLimit G f) R fun (a : Fin n) ↦ ⟦Structure.Sigma.mk (G := G) f i (y a)⟧

Tactic:
rw [relMap_quotient_mk'_sigma_mk' G f, ← (g i).map_rel R y, ← Function.comp_assoc,
      Quotient.lift_comp_mk]

Premises used: FirstOrder.Language.Embedding.map_rel, Quotient.lift_comp_mk, FirstOrder.Language.DirectLimit.relMap_quotient_mk'_sigma_mk', Function.comp_assoc
-- 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)
n : ℕ
R : L.Relations n
i : ι
y : Fin n → G i
⊢ RelMap.{u_1, u_2, u₁} (M := P) R
      ((fun (x : Σˣ (G := G) f) ↦
          (g (x.fst (β := fun (i : ι) ↦ G i)) : (a : G x.fst) → P) (x.snd (β := fun (i : ι) ↦ G i))) ∘
        Structure.Sigma.mk (G := G) f i ∘ y) ↔
    RelMap.{u_1, u_2, u₁} (M := P) R ((⇑(g i) : (a : G i) → P) ∘ y)

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 ι
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)
i : ι
x : G i
⊢ Function.Embedding.toFun (Embedding.toEmbedding (lift L ι G f g Hg)) ⟦Structure.Sigma.mk (G := G) f i x⟧ =
    (g i : (a : G i) → P) x

Tactic:
simp only [lift, Quotient.lift_mk]

Premises used: Quotient.lift_mk, FirstOrder.Language.DirectLimit.lift
-- 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)
i : ι
x : G i
⊢ Eq.{u₁ + 1} (α := P)
    ((lift L ι G f g Hg : (a : DirectLimit G f) → P)
        ((of L ι G f i : (a : G i) → DirectLimit G f) x : DirectLimit G f) :
      P)
    ((g i : (a : G i) → P) x : P)

Tactic:
simp