-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Subgraph (goal)
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
hHG : H ≤i G
mp :
  (∃ (x : α) (y : α), (∃ (e : β), G.IsLink e x y) ∧ x ∈ V(H) ∧ y ∉ V(H)) →
    ∃ (e : β) (x : α) (y : α), G.IsLink e x y ∧ x ∈ V(H) ∧ y ∉ V(H)
mpr :
  (∃ (e : β) (x : α) (y : α), G.IsLink e x y ∧ x ∈ V(H) ∧ y ∉ V(H)) →
    ∃ (x : α) (y : α), (∃ (e : β), G.IsLink e x y) ∧ x ∈ V(H) ∧ y ∉ V(H)
mp₁ mp₂ mp₃ :
  ∀ (w w_1 : α) (w_2 : β),
    G.IsLink w_2 w w_1 → w ∈ V(H) → w_1 ∉ V(H) → ∃ (e : β) (x : α) (y : α), G.IsLink e x y ∧ x ∈ V(H) ∧ y ∉ V(H)
mpr₁ mpr₂ mpr₃ :
  ∀ (w : β) (w_1 w_2 : α),
    G.IsLink w w_1 w_2 → w_1 ∈ V(H) → w_2 ∉ V(H) → ∃ (x : α) (y : α), (∃ (e : β), G.IsLink e x y) ∧ x ∈ V(H) ∧ y ∉ V(H)
mp₄ mp₅ mp₆ :
  ∀ (w w_1 : α) (w_2 : β),
    G.IsLink w_2 w w_1 → w ∈ V(H) → w_1 ∉ V(H) → ∃ (e : β) (x : α) (y : α), G.IsLink e x y ∧ x ∈ V(H) ∧ y ∉ V(H)
mpr₄ mpr₅ mpr₆ :
  ∀ (w : β) (w_1 w_2 : α),
    G.IsLink w w_1 w_2 → w_1 ∈ V(H) → w_2 ∉ V(H) → ∃ (x : α) (y : α), (∃ (e : β), G.IsLink e x y) ∧ x ∈ V(H) ∧ y ∉ V(H)
mp₇ mp₈ :
  ∀ (w w_1 : α) (w_2 : β),
    G.IsLink w_2 w w_1 → w ∈ V(H) → w_1 ∉ V(H) → ∃ (e : β) (x : α) (y : α), G.IsLink e x y ∧ x ∈ V(H) ∧ y ∉ V(H)
mp₉ :
  ∀ (w w_1 : α) (w_2 : β),
    G.IsLink w_2 w w_1 → w ∈ V(H) → w_1 ∉ V(H) → ∃ (x : α) (y : α), G.IsLink w_2 x y ∧ x ∈ V(H) ∧ y ∉ V(H)
mp₁₀ : (w w_1 : α) → (w_2 : β) → G.IsLink w_2 w w_1 → w ∈ V(H) → w_1 ∉ V(H) → β
mp₁₁ :
  ∀ (w w_1 : α) (w_2 : β),
    G.IsLink w_2 w w_1 → w ∈ V(H) → w_1 ∉ V(H) → ∃ (x : α) (y : α), G.IsLink w_2 x y ∧ x ∈ V(H) ∧ y ∉ V(H)
mp₁₂ : (w w_1 : α) → (w_2 : β) → G.IsLink w_2 w w_1 → w ∈ V(H) → w_1 ∉ V(H) → β
mp₁₃ :
  ∀ (w w_1 : α) (w_2 : β),
    G.IsLink w_2 w w_1 → w ∈ V(H) → w_1 ∉ V(H) → ∃ (y : α), G.IsLink w_2 w y ∧ w ∈ V(H) ∧ y ∉ V(H)
mp₁₄ : (w w_1 : α) → (w_2 : β) → G.IsLink w_2 w w_1 → w ∈ V(H) → w_1 ∉ V(H) → α
mp₁₅ : (w w_1 : α) → (w_2 : β) → G.IsLink w_2 w w_1 → w ∈ V(H) → w_1 ∉ V(H) → β
mp₁₆ :
  ∀ (w w_1 : α) (w_2 : β),
    G.IsLink w_2 w w_1 → w ∈ V(H) → w_1 ∉ V(H) → ∃ (y : α), G.IsLink w_2 w y ∧ w ∈ V(H) ∧ y ∉ V(H)
mp₁₇ : (w w_1 : α) → (w_2 : β) → G.IsLink w_2 w w_1 → w ∈ V(H) → w_1 ∉ V(H) → α
mp₁₈ : (w w_1 : α) → (w_2 : β) → G.IsLink w_2 w w_1 → w ∈ V(H) → w_1 ∉ V(H) → β
mp₁₉ : ∀ (w w_1 : α) (w_2 : β), G.IsLink w_2 w w_1 → w ∈ V(H) → w_1 ∉ V(H) → G.IsLink w_2 w w_1 ∧ w ∈ V(H) ∧ w_1 ∉ V(H)
mp₂₀ mp₂₁ : (w w_1 : α) → (w_2 : β) → G.IsLink w_2 w w_1 → w ∈ V(H) → w_1 ∉ V(H) → α
mp₂₂ : (w w_1 : α) → (w_2 : β) → G.IsLink w_2 w w_1 → w ∈ V(H) → w_1 ∉ V(H) → β
mp₂₃ : ∀ (w w_1 : α) (w_2 : β), G.IsLink w_2 w w_1 → w ∈ V(H) → w_1 ∉ V(H) → G.IsLink w_2 w w_1 ∧ w ∈ V(H) ∧ w_1 ∉ V(H)
mp₂₄ mp₂₅ : (w w_1 : α) → (w_2 : β) → G.IsLink w_2 w w_1 → w ∈ V(H) → w_1 ∉ V(H) → α
mp₂₆ : (w w_1 : α) → (w_2 : β) → G.IsLink w_2 w w_1 → w ∈ V(H) → w_1 ∉ V(H) → β
mpr₇ mpr₈ :
  ∀ (w : β) (w_1 w_2 : α),
    G.IsLink w w_1 w_2 → w_1 ∈ V(H) → w_2 ∉ V(H) → ∃ (x : α) (y : α), (∃ (e : β), G.IsLink e x y) ∧ x ∈ V(H) ∧ y ∉ V(H)
⊢ (∃ (x : α) (y : α), (∃ (e : β), G.IsLink e x y) ∧ x ∈ V(H) ∧ y ∉ V(H)) ↔
    ∃ (e : β) (x : α) (y : α), G.IsLink e x y ∧ x ∈ V(H) ∧ y ∉ V(H)
have mpr₉ : ∀ (w : β) (w_1 w_2 : α),
  G.IsLink w w_1 w_2 → w_1 ∈ V(H) → w_2 ∉ V(H) → ∃ (y : α), (∃ (e : β), G.IsLink e w_1 y) ∧ w_1 ∈ V(H) ∧ y ∉ V(H)
Tactic: tauto