-- Mathlib/ModelTheory/DirectLimit.lean
theorem relMap_quotient_mk'_sigma_mk' {n : ℕ} {R : L.Relations n} {i : ι} {x : Fin n → G i} :
    RelMap R (fun a => (⟦.mk f i (x a)⟧ : DirectLimit G f)) = RelMap R x

Proof state:
case intro.intro
L : Language
ι : Type v
inst✝⁴ : Preorder ι
G : ι → Type w
inst✝³ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝² : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝¹ : DirectedSystem G fun i j h => ⇑(f i j h)
inst✝ : Nonempty ι
n : ℕ
R : L.Relations n
i : ι
x : Fin n → G i
k : ι
left✝ : i ≤ k
right✝ : Classical.choose ⋯ ≤ k
⊢ (RelMap R fun a => Structure.Sigma.mk f i (x a)) = RelMap R x

Tactic:
rw [relMap_equiv_unify G f R (fun a => .mk f i (x a)) i]

Result:
case intro.intro
L : Language
ι : Type v
inst✝⁴ : Preorder ι
G : ι → Type w
inst✝³ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝² : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝¹ : DirectedSystem G fun i j h => ⇑(f i j h)
inst✝ : Nonempty ι
n : ℕ
R : L.Relations n
i : ι
x : Fin n → G i
k : ι
left✝ : i ≤ k
right✝ : Classical.choose ⋯ ≤ k
⊢ RelMap R (unify f (fun a => Structure.Sigma.mk f i (x a)) i ?intro.intro) = RelMap R x

case intro.intro
L : Language
ι : Type v
inst✝⁴ : Preorder ι
G : ι → Type w
inst✝³ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝² : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝¹ : DirectedSystem G fun i j h => ⇑(f i j h)
inst✝ : Nonempty ι
n : ℕ
R : L.Relations n
i : ι
x : Fin n → G i
k : ι
left✝ : i ≤ k
right✝ : Classical.choose ⋯ ≤ k
⊢ i ∈ upperBounds (range (Sigma.fst ∘ fun a => Structure.Sigma.mk f i (x a)))

Proof state:
case intro.intro
L : Language
ι : Type v
inst✝⁴ : Preorder ι
G : ι → Type w
inst✝³ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝² : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝¹ : DirectedSystem G fun i j h => ⇑(f i j h)
inst✝ : Nonempty ι
n : ℕ
R : L.Relations n
i : ι
x : Fin n → G i
k : ι
left✝ : i ≤ k
right✝ : Classical.choose ⋯ ≤ k
⊢ RelMap R (unify f (fun a => Structure.Sigma.mk f i (x a)) i ?intro.intro) = RelMap R x

case intro.intro
L : Language
ι : Type v
inst✝⁴ : Preorder ι
G : ι → Type w
inst✝³ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝² : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝¹ : DirectedSystem G fun i j h => ⇑(f i j h)
inst✝ : Nonempty ι
n : ℕ
R : L.Relations n
i : ι
x : Fin n → G i
k : ι
left✝ : i ≤ k
right✝ : Classical.choose ⋯ ≤ k
⊢ i ∈ upperBounds (range (Sigma.fst ∘ fun a => Structure.Sigma.mk f i (x a)))

Tactic:
rw [unify_sigma_mk_self]

Result:
no goals

Proof state:
L : Language
ι : Type v
inst✝⁴ : Preorder ι
G : ι → Type w
inst✝³ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝² : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝¹ : DirectedSystem G fun i j h => ⇑(f i j h)
inst✝ : Nonempty ι
n : ℕ
R : L.Relations n
i : ι
x : Fin n → G i
⊢ (RelMap R fun a => ⟦Structure.Sigma.mk f i (x a)⟧) = RelMap R x

Tactic:
rw [relMap_quotient_mk']

Result:
L : Language
ι : Type v
inst✝⁴ : Preorder ι
G : ι → Type w
inst✝³ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝² : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝¹ : DirectedSystem G fun i j h => ⇑(f i j h)
inst✝ : Nonempty ι
n : ℕ
R : L.Relations n
i : ι
x : Fin n → G i
⊢ (RelMap R fun a => Structure.Sigma.mk f i (x a)) = RelMap R x