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)
F : DirectLimit G f ↪[L] P
x_1 : DirectLimit G f
i j : ι
hij : i ≤ j
x : G i
rw :
  Eq.{u₁ + 1} (α := P)
    ((F : (a : DirectLimit G f) → P)
        ((of L ι G f j : (a : G j) → DirectLimit G f) ((f i j hij : (a : G i) → G j) x) : DirectLimit G f) :
      P)
    (((fun (i : ι) ↦ F.comp (of L ι G f i)) i : (a : G i) → P) x : P)
rw₁ :
  Eq.{u₁ + 1} (α := P)
    ((F : (a : DirectLimit G f) → P)
        ((of L ι G f j : (a : G j) → DirectLimit G f) ((f i j hij : (a : G i) → G j) x) : DirectLimit G f) :
      P)
    ((F : (a : DirectLimit G f) → P) ((of L ι G f i : (a : G i) → DirectLimit G f) x : DirectLimit G f) : P)
rw₂ rw₃ :
  Eq.{u₁ + 1} (α := P)
    ((F : (a : DirectLimit G f) → P) ((of L ι G f i : (a : G i) → DirectLimit G f) x : DirectLimit G f) : P)
    ((F : (a : DirectLimit G f) → P) ((of L ι G f i : (a : G i) → DirectLimit G f) x : DirectLimit G f) : P)
⊢ Eq.{u₁ + 1} (α := P)
    (((fun (i : ι) ↦ F.comp (of L ι G f i)) j : (a : G j) → P) ((f i j hij : (a : G i) → G j) x : G j) : P)
    (((fun (i : ι) ↦ F.comp (of L ι G f i)) i : (a : G i) → P) x : P)

Tactic:
rw [F.comp_apply, F.comp_apply, of_f]

Premises used: FirstOrder.Language.DirectLimit.of_f, FirstOrder.Language.Embedding.comp_apply
-- 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
F : DirectLimit G f ↪[L] P
x_1 : DirectLimit G f
i : ι
x : G i
rw :
  Eq.{u₁ + 1} (α := P)
    ((F : (a : DirectLimit G f) → P) ((of L ι G f i : (a : G i) → DirectLimit G f) x : DirectLimit G f) : P)
    ((F.comp (of L ι G f i) : (a : G i) → P) x : P)
⊢ Eq.{u₁ + 1} (α := P)
    ((F : (a : DirectLimit G f) → P) ((of L ι G f i : (a : G i) → DirectLimit G f) x : DirectLimit G f) : P)
    ((lift L ι G f (fun (i : ι) ↦ F.comp (of L ι G f i)) ⋯ : (a : DirectLimit G f) → P)
        ((of L ι G f i : (a : G i) → DirectLimit G f) x : DirectLimit G f) :
      P)

Tactic:
rw [lift_of]

Premises used: FirstOrder.Language.DirectLimit.lift_of
-- Module: Mathlib.ModelTheory.DirectLimit
Goal:
L : Language
ι : Type v
inst : Preorder ι
G : ι → Type w
inst_1 : (i : ι) → Structure.{u_1, u_2, w} L (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst_2 : IsDirectedOrder ι
inst_3 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
inst_4 : Nonempty ι
P : Type u₁
inst_5 : L.Structure P
F : DirectLimit G f ↪[L] P
x_1 : DirectLimit G f
i : ι
x : G i
⊢ Eq.{u₁ + 1} (α := P)
    ((F : (a : DirectLimit G f) → P) ((of L ι G f i : (a : G i) → DirectLimit G f) x : DirectLimit G f) : P)
    ((F.comp (of L ι G f i) : (a : G i) → P) x : P)

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)
simp_rw :
  Substructure.map (M := DirectLimit G f) (Embedding.toHom (lift L ι G f g Hg)) ⊤ =
    ⨆ (i : ι), Substructure.map (g i).toHom ⊤
⊢ Hom.range (M := DirectLimit G f) (Embedding.toHom (lift L ι G f g Hg)) = ⨆ (i : ι), (g i).toHom.range

Tactic:
simp_rw [Hom.range_eq_map]

Premises used: FirstOrder.Language.Hom.range_eq_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)
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)
rw :
  Eq.{u₁ + 1} (α := L.Substructure P)
    (⨆ (i : ι),
      Substructure.map (M := DirectLimit G f) (Embedding.toHom (lift L ι G f g Hg))
        (Hom.range (Embedding.toHom (of L ι G f i))))
    (⨆ (i : ι), Substructure.map (g i).toHom ⊤)
⊢ Substructure.map (M := DirectLimit G f) (Embedding.toHom (lift L ι G f g Hg)) ⊤ =
    ⨆ (i : ι), Substructure.map (g i).toHom ⊤

Tactic:
rw [← iSup_range_of_eq_top, Substructure.map_iSup]

Premises used: FirstOrder.Language.DirectLimit.iSup_range_of_eq_top, FirstOrder.Language.Substructure.map_iSup
-- 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)
simp_rw :
  Eq.{u₁ + 1} (α := L.Substructure P)
    (⨆ (i : ι),
      Substructure.map
        (Hom.comp (N := DirectLimit G f) (Embedding.toHom (lift L ι G f g Hg)) (Embedding.toHom (of L ι G f i))) ⊤)
    (⨆ (i : ι), Substructure.map (g i).toHom ⊤)
⊢ Eq.{u₁ + 1} (α := L.Substructure P)
    (⨆ (i : ι),
      Substructure.map (M := DirectLimit G f) (Embedding.toHom (lift L ι G f g Hg))
        (Hom.range (Embedding.toHom (of L ι G f i))))
    (⨆ (i : ι), Substructure.map (g i).toHom ⊤)

Tactic:
simp_rw [Hom.range_eq_map, Substructure.map_map]

Premises used: FirstOrder.Language.Substructure.map_map, FirstOrder.Language.Hom.range_eq_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)
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)
⊢ Eq.{u₁ + 1} (α := L.Substructure P)
    (⨆ (i : ι),
      Substructure.map
        (Hom.comp (N := DirectLimit G f) (Embedding.toHom (lift L ι G f g Hg)) (Embedding.toHom (of L ι G f i))) ⊤)
    (⨆ (i : ι), Substructure.map (g i).toHom ⊤)

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_1 : (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_1 j : (a : G j) → P) ((f i j hij : (a : G i) → G j) x : G j) : P)
      ((g_1 i : (a : G i) → P) x : P)
G' : ι → Type w'
inst_6 : (i : ι) → Structure.{u_1, u_2, w'} L (G' i)
f' : (i j : ι) → i ≤ j → G' i ↪[L] G' j
g : (i : ι) → Equiv.{u_1, u_2, w, w'} L (G i) (G' i)
inst_7 : DirectedSystem G' fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G' i) → G' j)
H_commuting :
  ∀ (i j : ι) (hij : i ≤ j) (x : G i),
    Eq.{w' + 1} (α := G' j) ((g j : (a : G j) → G' j) ((f i j hij : (a : G i) → G j) x) : G' j)
      ((f' i j hij : (a : G' i) → G' j) ((g i : (a : G i) → G' i) x : G' i) : G' j)
U : (i : ι) → G i ↪[L] DirectLimit G' f' := fun (i : ι) ↦ Embedding.comp (of L ι G' f' i) (g i).toEmbedding
i : ι
_ :
  ∀ (j : ι) (hij : i ≤ j) (x : G i),
    Eq (α := DirectLimit G' f')
      ((U j : (a : G j) → DirectLimit G' f') ((f i j hij : (a : G i) → G j) x) : DirectLimit G' f')
      ((U i : (a : G i) → DirectLimit G' f') x : DirectLimit G' f')
⊢ ∀ (j : ι) (hij : i ≤ j) (x : G i),
    Eq (α := DirectLimit G' f')
      ((U j : (a : G j) → DirectLimit G' f') ((f i j hij : (a : G i) → G j) x) : DirectLimit G' f')
      ((U i : (a : G i) → DirectLimit G' f') x : DirectLimit G' f')

Tactic:
_
-- 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_1 : (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_1 j : (a : G j) → P) ((f i j hij : (a : G i) → G j) x : G j) : P)
      ((g_1 i : (a : G i) → P) x : P)
G' : ι → Type w'
inst_6 : (i : ι) → Structure.{u_1, u_2, w'} L (G' i)
f' : (i j : ι) → i ≤ j → G' i ↪[L] G' j
g : (i : ι) → Equiv.{u_1, u_2, w, w'} L (G i) (G' i)
inst_7 : DirectedSystem G' fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G' i) → G' j)
H_commuting :
  ∀ (i j : ι) (hij : i ≤ j) (x : G i),
    Eq.{w' + 1} (α := G' j) ((g j : (a : G j) → G' j) ((f i j hij : (a : G i) → G j) x) : G' j)
      ((f' i j hij : (a : G' i) → G' j) ((g i : (a : G i) → G' i) x : G' i) : G' j)
U : (i : ι) → G i ↪[L] DirectLimit G' f' := fun (i : ι) ↦ Embedding.comp (of L ι G' f' i) (g i).toEmbedding
i j : ι
_ :
  ∀ (hij : i ≤ j) (x : G i),
    Eq (α := DirectLimit G' f')
      ((U j : (a : G j) → DirectLimit G' f') ((f i j hij : (a : G i) → G j) x) : DirectLimit G' f')
      ((U i : (a : G i) → DirectLimit G' f') x : DirectLimit G' f')
⊢ ∀ (hij : i ≤ j) (x : G i),
    Eq (α := DirectLimit G' f')
      ((U j : (a : G j) → DirectLimit G' f') ((f i j hij : (a : G i) → G j) x) : DirectLimit G' f')
      ((U i : (a : G i) → DirectLimit G' f') x : DirectLimit G' f')

Tactic:
_
-- 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_1 : (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_1 j : (a : G j) → P) ((f i j hij : (a : G i) → G j) x : G j) : P)
      ((g_1 i : (a : G i) → P) x : P)
G' : ι → Type w'
inst_6 : (i : ι) → Structure.{u_1, u_2, w'} L (G' i)
f' : (i j : ι) → i ≤ j → G' i ↪[L] G' j
g : (i : ι) → Equiv.{u_1, u_2, w, w'} L (G i) (G' i)
inst_7 : DirectedSystem G' fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G' i) → G' j)
H_commuting :
  ∀ (i j : ι) (hij : i ≤ j) (x : G i),
    Eq.{w' + 1} (α := G' j) ((g j : (a : G j) → G' j) ((f i j hij : (a : G i) → G j) x) : G' j)
      ((f' i j hij : (a : G' i) → G' j) ((g i : (a : G i) → G' i) x : G' i) : G' j)
U : (i : ι) → G i ↪[L] DirectLimit G' f' := fun (i : ι) ↦ Embedding.comp (of L ι G' f' i) (g i).toEmbedding
i j : ι
hij : i ≤ j
_ :
  ∀ (x : G i),
    Eq (α := DirectLimit G' f')
      ((U j : (a : G j) → DirectLimit G' f') ((f i j hij : (a : G i) → G j) x) : DirectLimit G' f')
      ((U i : (a : G i) → DirectLimit G' f') x : DirectLimit G' f')
⊢ ∀ (x : G i),
    Eq (α := DirectLimit G' f')
      ((U j : (a : G j) → DirectLimit G' f') ((f i j hij : (a : G i) → G j) x) : DirectLimit G' f')
      ((U i : (a : G i) → DirectLimit G' f') x : DirectLimit G' f')

Tactic:
_
-- 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_1 : (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_1 j : (a : G j) → P) ((f i j hij : (a : G i) → G j) x : G j) : P)
      ((g_1 i : (a : G i) → P) x : P)
G' : ι → Type w'
inst_6 : (i : ι) → Structure.{u_1, u_2, w'} L (G' i)
f' : (i j : ι) → i ≤ j → G' i ↪[L] G' j
g : (i : ι) → Equiv.{u_1, u_2, w, w'} L (G i) (G' i)
inst_7 : DirectedSystem G' fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G' i) → G' j)
H_commuting :
  ∀ (i j : ι) (hij : i ≤ j) (x : G i),
    Eq.{w' + 1} (α := G' j) ((g j : (a : G j) → G' j) ((f i j hij : (a : G i) → G j) x) : G' j)
      ((f' i j hij : (a : G' i) → G' j) ((g i : (a : G i) → G' i) x : G' i) : G' j)
U : (i : ι) → G i ↪[L] DirectLimit G' f' := fun (i : ι) ↦ Embedding.comp (of L ι G' f' i) (g i).toEmbedding
i j : ι
hij : i ≤ j
x : G i
⊢ Eq (α := DirectLimit G' f')
    ((U j : (a : G j) → DirectLimit G' f') ((f i j hij : (a : G i) → G j) x) : DirectLimit G' f')
    ((U i : (a : G i) → DirectLimit G' f') x : DirectLimit G' f')

Tactic:
simp only [U, Embedding.comp_apply, Equiv.coe_toEmbedding, H_commuting, of_f]

Premises used: FirstOrder.Language.DirectLimit.of_f, FirstOrder.Language.Embedding.comp_apply, FirstOrder.Language.Equiv.coe_toEmbedding
-- 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_1 : (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_1 j : (a : G j) → P) ((f i j hij : (a : G i) → G j) x : G j) : P)
      ((g_1 i : (a : G i) → P) x : P)
G' : ι → Type w'
inst_6 : (i : ι) → Structure.{u_1, u_2, w'} L (G' i)
f' : (i j : ι) → i ≤ j → G' i ↪[L] G' j
g : (i : ι) → Equiv.{u_1, u_2, w, w'} L (G i) (G' i)
inst_7 : DirectedSystem G' fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G' i) → G' j)
H_commuting :
  ∀ (i j : ι) (hij : i ≤ j) (x : G i),
    Eq.{w' + 1} (α := G' j) ((g j : (a : G j) → G' j) ((f i j hij : (a : G i) → G j) x) : G' j)
      ((f' i j hij : (a : G' i) → G' j) ((g i : (a : G i) → G' i) x : G' i) : G' j)
U : (i : ι) → G i ↪[L] DirectLimit G' f' := fun (i : ι) ↦ Embedding.comp (of L ι G' f' i) (g i).toEmbedding
F : DirectLimit G f ↪[L] DirectLimit G' f' := lift L ι G f U ⋯
x : DirectLimit G' f'
mk :
  ∀ (i : ι) (pre_x : G' i),
    ∃ (a : DirectLimit G f),
      Eq (α := DirectLimit G' f') ((F : (a : DirectLimit G f) → DirectLimit G' f') a : DirectLimit G' f')
        (Quot.mk (⇑(setoid G' f') : Σˣ f' → Σˣ f' → Prop) (Sigma.mk (β := fun (i : ι) ↦ G' i) i pre_x) :
          Quot (α := Σˣ (G := G') f') (⇑(setoid G' f') : Σˣ f' → Σˣ f' → Prop))
⊢ ∃ (a : DirectLimit G f), (F : (a : DirectLimit G f) → DirectLimit G' f') a = x

Tactic:
rcases x with ⟨i, pre_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)
inst_4 : Nonempty ι
P : Type u₁
inst_5 : L.Structure P
g_1 : (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_1 j : (a : G j) → P) ((f i j hij : (a : G i) → G j) x : G j) : P)
      ((g_1 i : (a : G i) → P) x : P)
G' : ι → Type w'
inst_6 : (i : ι) → Structure.{u_1, u_2, w'} L (G' i)
f' : (i j : ι) → i ≤ j → G' i ↪[L] G' j
g : (i : ι) → Equiv.{u_1, u_2, w, w'} L (G i) (G' i)
inst_7 : DirectedSystem G' fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G' i) → G' j)
H_commuting :
  ∀ (i j : ι) (hij : i ≤ j) (x : G i),
    Eq.{w' + 1} (α := G' j) ((g j : (a : G j) → G' j) ((f i j hij : (a : G i) → G j) x) : G' j)
      ((f' i j hij : (a : G' i) → G' j) ((g i : (a : G i) → G' i) x : G' i) : G' j)
U : (i : ι) → G i ↪[L] DirectLimit G' f' := fun (i : ι) ↦ Embedding.comp (of L ι G' f' i) (g i).toEmbedding
F : DirectLimit G f ↪[L] DirectLimit G' f' := lift L ι G f U ⋯
x : DirectLimit G' f'
i : ι
pre_x : G' i
h :
  Eq (α := DirectLimit G' f')
    ((F : (a : DirectLimit G f) → DirectLimit G' f')
        ((of L ι G f i : (a : G i) → DirectLimit G f) (((g i).symm : (a : G' i) → G i) pre_x)) :
      DirectLimit G' f')
    (Quot.mk (⇑(setoid G' f') : Σˣ f' → Σˣ f' → Prop) (Sigma.mk (β := fun (i : ι) ↦ G' i) i pre_x) :
      Quot (α := Σˣ (G := G') f') (⇑(setoid G' f') : Σˣ f' → Σˣ f' → Prop))
⊢ ∃ (a : DirectLimit G f),
    Eq (α := DirectLimit G' f') ((F : (a : DirectLimit G f) → DirectLimit G' f') a : DirectLimit G' f')
      (Quot.mk (⇑(setoid G' f') : Σˣ f' → Σˣ f' → Prop) (Sigma.mk (β := fun (i : ι) ↦ G' i) i pre_x) :
        Quot (α := Σˣ (G := G') f') (⇑(setoid G' f') : Σˣ f' → Σˣ f' → Prop))

Tactic:
use of L _ G f i ((g i).symm pre_x)

Premises used: FirstOrder.Language.DirectLimit.of, DFunLike.coe, FirstOrder.Language.Equiv.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 ι
P : Type u₁
inst_5 : L.Structure P
g_1 : (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_1 j : (a : G j) → P) ((f i j hij : (a : G i) → G j) x : G j) : P)
      ((g_1 i : (a : G i) → P) x : P)
G' : ι → Type w'
inst_6 : (i : ι) → Structure.{u_1, u_2, w'} L (G' i)
f' : (i j : ι) → i ≤ j → G' i ↪[L] G' j
g : (i : ι) → Equiv.{u_1, u_2, w, w'} L (G i) (G' i)
inst_7 : DirectedSystem G' fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G' i) → G' j)
H_commuting :
  ∀ (i j : ι) (hij : i ≤ j) (x : G i),
    Eq.{w' + 1} (α := G' j) ((g j : (a : G j) → G' j) ((f i j hij : (a : G i) → G j) x) : G' j)
      ((f' i j hij : (a : G' i) → G' j) ((g i : (a : G i) → G' i) x : G' i) : G' j)
U : (i : ι) → G i ↪[L] DirectLimit G' f' := fun (i : ι) ↦ Embedding.comp (of L ι G' f' i) (g i).toEmbedding
F : DirectLimit G f ↪[L] DirectLimit G' f' := lift L ι G f U ⋯
x : DirectLimit G' f'
i : ι
pre_x : G' i
h :
  Eq (α := DirectLimit G' f') ((of L ι G' f' i : (a : G' i) → DirectLimit G' f') pre_x : DirectLimit G' f')
    (Quot.mk (⇑(setoid G' f') : Σˣ f' → Σˣ f' → Prop) (Sigma.mk (β := fun (i : ι) ↦ G' i) i pre_x) :
      Quot (α := Σˣ (G := G') f') (⇑(setoid G' f') : Σˣ f' → Σˣ f' → Prop))
⊢ Eq (α := DirectLimit G' f')
    ((F : (a : DirectLimit G f) → DirectLimit G' f')
        ((of L ι G f i : (a : G i) → DirectLimit G f) (((g i).symm : (a : G' i) → G i) pre_x)) :
      DirectLimit G' f')
    (Quot.mk (⇑(setoid G' f') : Σˣ f' → Σˣ f' → Prop) (Sigma.mk (β := fun (i : ι) ↦ G' i) i pre_x) :
      Quot (α := Σˣ (G := G') f') (⇑(setoid G' f') : Σˣ f' → Σˣ f' → Prop))

Tactic:
simp only [F, U, lift_of, Embedding.comp_apply, Equiv.coe_toEmbedding, Equiv.apply_symm_apply]

Premises used: FirstOrder.Language.Equiv.apply_symm_apply, FirstOrder.Language.DirectLimit.lift_of, FirstOrder.Language.Embedding.comp_apply, FirstOrder.Language.Equiv.coe_toEmbedding
-- 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_1 : (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_1 j : (a : G j) → P) ((f i j hij : (a : G i) → G j) x : G j) : P)
      ((g_1 i : (a : G i) → P) x : P)
G' : ι → Type w'
inst_6 : (i : ι) → Structure.{u_1, u_2, w'} L (G' i)
f' : (i j : ι) → i ≤ j → G' i ↪[L] G' j
g : (i : ι) → Equiv.{u_1, u_2, w, w'} L (G i) (G' i)
inst_7 : DirectedSystem G' fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G' i) → G' j)
H_commuting :
  ∀ (i j : ι) (hij : i ≤ j) (x : G i),
    Eq.{w' + 1} (α := G' j) ((g j : (a : G j) → G' j) ((f i j hij : (a : G i) → G j) x) : G' j)
      ((f' i j hij : (a : G' i) → G' j) ((g i : (a : G i) → G' i) x : G' i) : G' j)
U : (i : ι) → G i ↪[L] DirectLimit G' f' := fun (i : ι) ↦ Embedding.comp (of L ι G' f' i) (g i).toEmbedding
F : DirectLimit G f ↪[L] DirectLimit G' f' := lift L ι G f U ⋯
x : DirectLimit G' f'
i : ι
pre_x : G' i
⊢ Eq (α := DirectLimit G' f') ((of L ι G' f' i : (a : G' i) → DirectLimit G' f') pre_x : DirectLimit G' f')
    (Quot.mk (⇑(setoid G' f') : Σˣ f' → Σˣ f' → Prop) (Sigma.mk (β := fun (i : ι) ↦ G' i) i pre_x) :
      Quot (α := Σˣ (G := G') f') (⇑(setoid G' f') : Σˣ f' → Σˣ f' → Prop))

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_1 : (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_1 j : (a : G j) → P) ((f i j hij : (a : G i) → G j) x : G j) : P)
      ((g_1 i : (a : G i) → P) x : P)
G' : ι → Type w'
inst_6 : (i : ι) → Structure.{u_1, u_2, w'} L (G' i)
f' : (i j : ι) → i ≤ j → G' i ↪[L] G' j
g : (i : ι) → Equiv.{u_1, u_2, w, w'} L (G i) (G' i)
inst_7 : DirectedSystem G' fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G' i) → G' j)
H_commuting :
  ∀ (i j : ι) (hij : i ≤ j) (x : G i),
    Eq.{w' + 1} (α := G' j) ((g j : (a : G j) → G' j) ((f i j hij : (a : G i) → G j) x) : G' j)
      ((f' i j hij : (a : G' i) → G' j) ((g i : (a : G i) → G' i) x : G' i) : G' j)
U : (i : ι) → G i ↪[L] DirectLimit G' f' := fun (i : ι) ↦ Embedding.comp (of L ι G' f' i) (g i).toEmbedding
F : DirectLimit G f ↪[L] DirectLimit G' f' := lift L ι G f U ⋯
⊢ Function.Surjective (α := DirectLimit G f) (β := DirectLimit G' f') (⇑F : (a : DirectLimit G f) → DirectLimit G' f')

Tactic:
have surj_f : Function.Surjective F := by
    intro x
    rcases x with ⟨i, pre_x⟩
    use of L _ G f i ((g i).symm pre_x)
    simp only [F, U, lift_of, Embedding.comp_apply, Equiv.coe_toEmbedding, Equiv.apply_symm_apply]
    rfl