-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
G G₁ G₂ G₃ : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph X
A : SimpleGraph α
B : SimpleGraph β
C : SimpleGraph γ
f : A.Copy B
A' : A.Subgraph
map_rel_iff' :
  ∀ {a b : (↑A'.verts : Type u_4)},
    (Subgraph.map f.toHom A').coe.Adj
        ((Equiv.Set.image (⇑f.toHom : (a : α) → β) A'.verts ⋯ :
            (a : (↑A'.verts : Type u_4)) → (↑((⇑f.toHom : (a : α) → β) '' A'.verts) : Type u_5))
          a)
        ((Equiv.Set.image (⇑f.toHom : (a : α) → β) A'.verts ⋯ :
            (a : (↑A'.verts : Type u_4)) → (↑((⇑f.toHom : (a : α) → β) '' A'.verts) : Type u_5))
          b) ↔
      A'.coe.Adj a b
map_rel_iff'₁ :
  ∀ {a b : (↑A'.verts : Type u_4)},
    (Subgraph.map f.toHom A').coe.Adj
        (Subtype.mk (p := fun (x : β) ↦ Membership.mem (γ := Set β) ((⇑f.toHom : (a : α) → β) '' A'.verts) x)
          ((f.toHom : (a : α) → β) (↑a : α)) ⋯)
        (Subtype.mk (p := fun (x : β) ↦ Membership.mem (γ := Set β) ((⇑f.toHom : (a : α) → β) '' A'.verts) x)
          ((f.toHom : (a : α) → β) (↑b : α)) ⋯) ↔
      A'.coe.Adj a b
map_rel_iff'₂ :
  ∀ {a b : (↑A'.verts : Type u_4)},
    (Subgraph.map f.toHom A').Adj ((f.toHom : (a : α) → β) (↑a : α)) ((f.toHom : (a : α) → β) (↑b : α)) ↔
      A'.Adj (↑a : α) (↑b : α)
map_rel_iff'₃ :
  ∀ {a b : (↑A'.verts : Type u_4)},
    Relation.Map.{u_4 + 1, u_4 + 1, u_5 + 1, u_5 + 1} (γ := β) (δ := β) A'.Adj ((⇑f.toHom : (a : α) → β) : (a : α) → β)
        ((⇑f.toHom : (a : α) → β) : (a : α) → β) ((f.toHom : (a : α) → β) (↑a : α) : β)
        ((f.toHom : (a : α) → β) (↑b : α) : β) ↔
      A'.Adj (↑a : α) (↑b : α)
map_rel_iff'₄ :
  ∀ {a b : (↑A'.verts : Type u_4)},
    (∃ (a_1 : α) (b_1 : α),
        A'.Adj a_1 b_1 ∧
          Eq.{u_5 + 1} (α := β) ((f.toHom : (a : α) → β) a_1 : β) ((f.toHom : (a : α) → β) (↑a : α) : β) ∧
            Eq.{u_5 + 1} (α := β) ((f.toHom : (a : α) → β) b_1 : β) ((f.toHom : (a : α) → β) (↑b : α) : β)) ↔
      A'.Adj (↑a : α) (↑b : α)
map_rel_iff'₅ :
  ∀ {a b : (↑A'.verts : Type u_4)},
    (∃ (a_1 : α) (b_1 : α), A'.Adj a_1 b_1 ∧ a_1 = (↑a : α) ∧ b_1 = (↑b : α)) ↔ A'.Adj (↑a : α) (↑b : α)
map_rel_iff'₆ :
  ∀ {a b : (↑A'.verts : Type u_4)}, (∃ (a_1 : α), A'.Adj a_1 (↑b : α) ∧ a_1 = (↑a : α)) ↔ A'.Adj (↑a : α) (↑b : α)
map_rel_iff'₇ : ∀ {a b : (↑A'.verts : Type u_4)}, True
⊢ ∀ {a b : (↑A'.verts : Type u_4)},
    (Subgraph.map f.toHom A').coe.Adj
        ((Equiv.Set.image (⇑f.toHom : (a : α) → β) A'.verts ⋯ :
            (a : (↑A'.verts : Type u_4)) → (↑(Subgraph.map f.toHom A').verts : Type u_5))
          a)
        ((Equiv.Set.image (⇑f.toHom : (a : α) → β) A'.verts ⋯ :
            (a : (↑A'.verts : Type u_4)) → (↑(Subgraph.map f.toHom A').verts : Type u_5))
          b) ↔
      A'.coe.Adj a b

Tactic:
simp_rw [Subgraph.map_verts, Equiv.Set.image_apply, Subgraph.coe_adj, Subgraph.map_adj,
    Relation.map_apply, f.injective.eq_iff, exists_eq_right_right, exists_eq_right, forall_true_iff]

Premises used: exists_eq_right_right, Equiv.Set.image_apply, Function.Injective.eq_iff, SimpleGraph.Copy.injective, SimpleGraph.Subgraph.coe_adj, exists_eq_right, SimpleGraph.Subgraph.map_verts, SimpleGraph.Subgraph.map_adj, Relation.map_apply, forall_true_iff