-- Mathlib/ModelTheory/PartialEquiv.lean
@[simp]
lemma partialEquivLimit_comp_inclusion {i : ι} :
    (partialEquivLimit S).toEquiv.toEmbedding.comp (Substructure.inclusion (le_iSup _ i)) =
    (Substructure.inclusion (le_iSup _ i)).comp (S i).toEquiv.toEmbedding

Proof state:
L : Language
M : Type w
N : Type w'
inst✝⁴ : L.Structure M
inst✝³ : L.Structure N
ι : Type u_1
inst✝² : Preorder ι
inst✝¹ : Nonempty ι
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
S : ι →o M ≃ₚ[L] N
i : ι
⊢ (Equiv_iSup { toFun := fun i => (S i).cod, monotone' := ⋯ }).toEmbedding.comp
      ((equiv_lift L ι (fun i => ↥(S i).dom) (fun x x_1 hij => inclusion ⋯) (fun i => ↥(S i).cod)
              (fun x x_1 hij => inclusion ⋯) (fun i => (S i).toEquiv) ⋯).toEmbedding.comp
        ((Equiv_iSup { toFun := fun i => (S i).dom, monotone' := ⋯ }).symm.toEmbedding.comp (inclusion ⋯))) =
    (inclusion ⋯).comp (S i).toEquiv.toEmbedding

Tactic:
rw [Equiv_isup_symm_inclusion]

Result:
L : Language
M : Type w
N : Type w'
inst✝⁴ : L.Structure M
inst✝³ : L.Structure N
ι : Type u_1
inst✝² : Preorder ι
inst✝¹ : Nonempty ι
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
S : ι →o M ≃ₚ[L] N
i : ι
⊢ (Equiv_iSup { toFun := fun i => (S i).cod, monotone' := ⋯ }).toEmbedding.comp
      ((equiv_lift L ι (fun i => ↥(S i).dom) (fun x x_1 hij => inclusion ⋯) (fun i => ↥(S i).cod)
              (fun x x_1 hij => inclusion ⋯) (fun i => (S i).toEquiv) ⋯).toEmbedding.comp
        (of L ι (fun x => ↥({ toFun := fun i => (S i).dom, monotone' := ⋯ } x)) (fun x x_1 h => inclusion ⋯) i)) =
    (inclusion ⋯).comp (S i).toEquiv.toEmbedding

Proof state:
L : Language
M : Type w
N : Type w'
inst✝⁴ : L.Structure M
inst✝³ : L.Structure N
ι : Type u_1
inst✝² : Preorder ι
inst✝¹ : Nonempty ι
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
S : ι →o M ≃ₚ[L] N
i : ι
⊢ (Equiv_iSup { toFun := fun i => (S i).cod, monotone' := ⋯ }).toEmbedding.comp
      ((equiv_lift L ι (fun i => ↥(S i).dom) (fun x x_1 hij => inclusion ⋯) (fun i => ↥(S i).cod)
              (fun x x_1 hij => inclusion ⋯) (fun i => (S i).toEquiv) ⋯).toEmbedding.comp
        (of L ι (fun x => ↥({ toFun := fun i => (S i).dom, monotone' := ⋯ } x)) (fun x x_1 h => inclusion ⋯) i)) =
    (inclusion ⋯).comp (S i).toEquiv.toEmbedding

Tactic:
congr

Result:
no goals

Proof state:
L : Language
M : Type w
N : Type w'
inst✝⁴ : L.Structure M
inst✝³ : L.Structure N
ι : Type u_1
inst✝² : Preorder ι
inst✝¹ : Nonempty ι
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
S : ι →o M ≃ₚ[L] N
i : ι
⊢ (partialEquivLimit S).toEquiv.toEmbedding.comp (inclusion ⋯) = (inclusion ⋯).comp (S i).toEquiv.toEmbedding

Tactic:
simp only [partialEquivLimit, Equiv.comp_toEmbedding, Embedding.comp_assoc]

Result:
L : Language
M : Type w
N : Type w'
inst✝⁴ : L.Structure M
inst✝³ : L.Structure N
ι : Type u_1
inst✝² : Preorder ι
inst✝¹ : Nonempty ι
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
S : ι →o M ≃ₚ[L] N
i : ι
⊢ (Equiv_iSup { toFun := fun i => (S i).cod, monotone' := ⋯ }).toEmbedding.comp
      ((equiv_lift L ι (fun i => ↥(S i).dom) (fun x x_1 hij => inclusion ⋯) (fun i => ↥(S i).cod)
              (fun x x_1 hij => inclusion ⋯) (fun i => (S i).toEquiv) ⋯).toEmbedding.comp
        ((Equiv_iSup { toFun := fun i => (S i).dom, monotone' := ⋯ }).symm.toEmbedding.comp (inclusion ⋯))) =
    (inclusion ⋯).comp (S i).toEquiv.toEmbedding