Module: Mathlib.Combinatorics.Graph.Simple

Goal state before:
pp: α : Type u_1
β : Type u_2
G H : Graph α β
GV : Set α
GL : β → α → α → Prop
GE : Set β
isLink_symm✝¹ : ∀ ⦃e : β⦄, e ∈ GE → Std.Symm (GL e)
eq_or_eq_of_isLink_of_isLink✝¹ : ∀ ⦃e : β⦄ ⦃x y v w : α⦄, GL e x y → GL e v w → x = v ∨ x = w
edge_mem_iff_exists_isLink✝¹ : ∀ (e : β), e ∈ GE ↔ ∃ x y, GL e x y
left_mem_of_isLink✝¹ : ∀ ⦃e : β⦄ ⦃x y : α⦄, GL e x y → x ∈ GV
HV : Set α
HL : β → α → α → Prop
HE : Set β
isLink_symm✝ : ∀ ⦃e : β⦄, e ∈ HE → Std.Symm (HL e)
eq_or_eq_of_isLink_of_isLink✝ : ∀ ⦃e : β⦄ ⦃x y v w : α⦄, HL e x y → HL e v w → x = v ∨ x = w
edge_mem_iff_exists_isLink✝ : ∀ (e : β), e ∈ HE ↔ ∃ x y, HL e x y
left_mem_of_isLink✝ : ∀ ⦃e : β⦄ ⦃x y : α⦄, HL e x y → x ∈ HV
h :
  { vertexSet := GV, IsLink := GL, edgeSet := GE, isLink_symm := isLink_symm✝¹,
      eq_or_eq_of_isLink_of_isLink := eq_or_eq_of_isLink_of_isLink✝¹,
      edge_mem_iff_exists_isLink := edge_mem_iff_exists_isLink✝¹, left_mem_of_isLink := left_mem_of_isLink✝¹ } ≤s
    { vertexSet := HV, IsLink := HL, edgeSet := HE, isLink_symm := isLink_symm✝,
      eq_or_eq_of_isLink_of_isLink := eq_or_eq_of_isLink_of_isLink✝,
      edge_mem_iff_exists_isLink := edge_mem_iff_exists_isLink✝, left_mem_of_isLink := left_mem_of_isLink✝ }
u v :
  ↑V({ vertexSet := GV, IsLink := GL, edgeSet := GE, isLink_symm := isLink_symm✝¹,
        eq_or_eq_of_isLink_of_isLink := eq_or_eq_of_isLink_of_isLink✝¹,
        edge_mem_iff_exists_isLink := edge_mem_iff_exists_isLink✝¹, left_mem_of_isLink := left_mem_of_isLink✝¹ })
hadj :
  { vertexSet := GV, IsLink := GL, edgeSet := GE, isLink_symm := isLink_symm✝¹,
          eq_or_eq_of_isLink_of_isLink := eq_or_eq_of_isLink_of_isLink✝¹,
          edge_mem_iff_exists_isLink := edge_mem_iff_exists_isLink✝¹,
          left_mem_of_isLink := left_mem_of_isLink✝¹ }.toSimpleGraph.Adj
    u v
⊢ (⋯ ▸
        { vertexSet := HV, IsLink := HL, edgeSet := HE, isLink_symm := isLink_symm✝,
            eq_or_eq_of_isLink_of_isLink := eq_or_eq_of_isLink_of_isLink✝,
            edge_mem_iff_exists_isLink := edge_mem_iff_exists_isLink✝,
            left_mem_of_isLink := left_mem_of_isLink✝ }.toSimpleGraph).Adj
    u v

Tactic:
obtain ⟨hne, hadj⟩ := toSimpleGraph_adj .. ▸ hadj

Goal state after:
α : Type u_1
β : Type u_2
G H : Graph α β
GV : Set α
GL : β → α → α → Prop
GE : Set β
isLink_symm✝¹ : ∀ ⦃e : β⦄, e ∈ GE → Std.Symm (GL e)
eq_or_eq_of_isLink_of_isLink✝¹ : ∀ ⦃e : β⦄ ⦃x y v w : α⦄, GL e x y → GL e v w → x = v ∨ x = w
edge_mem_iff_exists_isLink✝¹ : ∀ (e : β), e ∈ GE ↔ ∃ x y, GL e x y
left_mem_of_isLink✝¹ : ∀ ⦃e : β⦄ ⦃x y : α⦄, GL e x y → x ∈ GV
HV : Set α
HL : β → α → α → Prop
HE : Set β
isLink_symm✝ : ∀ ⦃e : β⦄, e ∈ HE → Std.Symm (HL e)
eq_or_eq_of_isLink_of_isLink✝ : ∀ ⦃e : β⦄ ⦃x y v w : α⦄, HL e x y → HL e v w → x = v ∨ x = w
edge_mem_iff_exists_isLink✝ : ∀ (e : β), e ∈ HE ↔ ∃ x y, HL e x y
left_mem_of_isLink✝ : ∀ ⦃e : β⦄ ⦃x y : α⦄, HL e x y → x ∈ HV
h :
  { vertexSet := GV, IsLink := GL, edgeSet := GE, isLink_symm := isLink_symm✝¹,
      eq_or_eq_of_isLink_of_isLink := eq_or_eq_of_isLink_of_isLink✝¹,
      edge_mem_iff_exists_isLink := edge_mem_iff_exists_isLink✝¹, left_mem_of_isLink := left_mem_of_isLink✝¹ } ≤s
    { vertexSet := HV, IsLink := HL, edgeSet := HE, isLink_symm := isLink_symm✝,
      eq_or_eq_of_isLink_of_isLink := eq_or_eq_of_isLink_of_isLink✝,
      edge_mem_iff_exists_isLink := edge_mem_iff_exists_isLink✝, left_mem_of_isLink := left_mem_of_isLink✝ }
u v :
  ↑V({ vertexSet := GV, IsLink := GL, edgeSet := GE, isLink_symm := isLink_symm✝¹,
        eq_or_eq_of_isLink_of_isLink := eq_or_eq_of_isLink_of_isLink✝¹,
        edge_mem_iff_exists_isLink := edge_mem_iff_exists_isLink✝¹, left_mem_of_isLink := left_mem_of_isLink✝¹ })
hadj✝ :
  { vertexSet := GV, IsLink := GL, edgeSet := GE, isLink_symm := isLink_symm✝¹,
          eq_or_eq_of_isLink_of_isLink := eq_or_eq_of_isLink_of_isLink✝¹,
          edge_mem_iff_exists_isLink := edge_mem_iff_exists_isLink✝¹,
          left_mem_of_isLink := left_mem_of_isLink✝¹ }.toSimpleGraph.Adj
    u v
hne : u ≠ v
hadj :
  { vertexSet := GV, IsLink := GL, edgeSet := GE, isLink_symm := isLink_symm✝¹,
        eq_or_eq_of_isLink_of_isLink := eq_or_eq_of_isLink_of_isLink✝¹,
        edge_mem_iff_exists_isLink := edge_mem_iff_exists_isLink✝¹, left_mem_of_isLink := left_mem_of_isLink✝¹ }.Adj
    ↑u ↑v
⊢ (⋯ ▸
        { vertexSet := HV, IsLink := HL, edgeSet := HE, isLink_symm := isLink_symm✝,
            eq_or_eq_of_isLink_of_isLink := eq_or_eq_of_isLink_of_isLink✝,
            edge_mem_iff_exists_isLink := edge_mem_iff_exists_isLink✝,
            left_mem_of_isLink := left_mem_of_isLink✝ }.toSimpleGraph).Adj
    u v