-- Lean 4 proof step from Mathlib.Combinatorics.Graph.Maps (goal)
Goal:
α : Type u_1
α' : Type u_2
β : Type u_4
G : Graph α β
x y : α'
f : α → α'
mp :
  (∃ (e : β) (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y) →
    ∃ (a : α) (b : α), (∃ (e : β), G.IsLink e a b) ∧ f a = x ∧ f b = y
mpr :
  (∃ (a : α) (b : α), (∃ (e : β), G.IsLink e a b) ∧ f a = x ∧ f b = y) →
    ∃ (e : β) (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y
mp₁ mp₂ mp₃ :
  ∀ (w : β) (w_1 w_2 : α),
    G.IsLink w w_1 w_2 → f w_1 = x → f w_2 = y → ∃ (a : α) (b : α), (∃ (e : β), G.IsLink e a b) ∧ f a = x ∧ f b = y
mpr₁ mpr₂ mpr₃ :
  ∀ (w w_1 : α) (w_2 : β),
    G.IsLink w_2 w w_1 → f w = x → f w_1 = y → ∃ (e : β) (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y
mp₄ mp₅ mp₆ :
  ∀ (w : β) (w_1 w_2 : α),
    G.IsLink w w_1 w_2 → f w_1 = x → f w_2 = y → ∃ (a : α) (b : α), (∃ (e : β), G.IsLink e a b) ∧ f a = x ∧ f b = y
mpr₄ mpr₅ mpr₆ :
  ∀ (w w_1 : α) (w_2 : β),
    G.IsLink w_2 w w_1 → f w = x → f w_1 = y → ∃ (e : β) (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y
mp₇ mp₈ :
  ∀ (w : β) (w_1 w_2 : α),
    G.IsLink w w_1 w_2 → f w_1 = x → f w_2 = y → ∃ (a : α) (b : α), (∃ (e : β), G.IsLink e a b) ∧ f a = x ∧ f b = y
mp₉ :
  ∀ (w : β) (w_1 w_2 : α),
    G.IsLink w w_1 w_2 → f w_1 = x → f w_2 = y → ∃ (b : α), (∃ (e : β), G.IsLink e w_1 b) ∧ f w_1 = x ∧ f b = y
mp₁₀ : (w : β) → (w_1 w_2 : α) → G.IsLink w w_1 w_2 → f w_1 = x → f w_2 = y → α
mp₁₁ :
  ∀ (w : β) (w_1 w_2 : α),
    G.IsLink w w_1 w_2 → f w_1 = x → f w_2 = y → ∃ (b : α), (∃ (e : β), G.IsLink e w_1 b) ∧ f w_1 = x ∧ f b = y
mp₁₂ : (w : β) → (w_1 w_2 : α) → G.IsLink w w_1 w_2 → f w_1 = x → f w_2 = y → α
mp₁₃ :
  ∀ (w : β) (w_1 w_2 : α),
    G.IsLink w w_1 w_2 → f w_1 = x → f w_2 = y → (∃ (e : β), G.IsLink e w_1 w_2) ∧ f w_1 = x ∧ f w_2 = y
mp₁₄ mp₁₅ : (w : β) → (w_1 w_2 : α) → G.IsLink w w_1 w_2 → f w_1 = x → f w_2 = y → α
mp₁₆ :
  ∀ (w : β) (w_1 w_2 : α),
    G.IsLink w w_1 w_2 → f w_1 = x → f w_2 = y → (∃ (e : β), G.IsLink e w_1 w_2) ∧ f w_1 = x ∧ f w_2 = y
mp₁₇ mp₁₈ : (w : β) → (w_1 w_2 : α) → G.IsLink w w_1 w_2 → f w_1 = x → f w_2 = y → α
mp₁₉ : ∀ (w : β) (w_1 w_2 : α), G.IsLink w w_1 w_2 → f w_1 = x → f w_2 = y → ∃ (e : β), G.IsLink e w_1 w_2
mp₂₀ : ∀ (w : β) (w_1 w_2 : α), G.IsLink w w_1 w_2 → f w_1 = x → f w_2 = y → f w_1 = x ∧ f w_2 = y
mp₂₁ mp₂₂ : (w : β) → (w_1 w_2 : α) → G.IsLink w w_1 w_2 → f w_1 = x → f w_2 = y → α
mp₂₃ : ∀ (w : β) (w_1 w_2 : α), G.IsLink w w_1 w_2 → f w_1 = x → f w_2 = y → ∃ (e : β), G.IsLink e w_1 w_2
mp₂₄ : ∀ (w : β) (w_1 w_2 : α), G.IsLink w w_1 w_2 → f w_1 = x → f w_2 = y → f w_1 = x ∧ f w_2 = y
mp₂₅ mp₂₆ : (w : β) → (w_1 w_2 : α) → G.IsLink w w_1 w_2 → f w_1 = x → f w_2 = y → α
mp₂₇ mp₂₈ : ∀ (w : β) (w_1 w_2 : α), G.IsLink w w_1 w_2 → f w_1 = x → f w_2 = y → f w_1 = x ∧ f w_2 = y
mpr₇ mpr₈ :
  ∀ (w w_1 : α) (w_2 : β),
    G.IsLink w_2 w w_1 → f w = x → f w_1 = y → ∃ (e : β) (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y
⊢ (∃ (e : β) (a : α) (b : α), G.IsLink e a b ∧ f a = x ∧ f b = y) ↔
    ∃ (a : α) (b : α), (∃ (e : β), G.IsLink e a b) ∧ f a = x ∧ f b = y
have mpr₉ : ∀ (w w_1 : α) (w_2 : β),
  G.IsLink w_2 w w_1 → f w = x → f w_1 = y → ∃ (a : α) (b : α), G.IsLink w_2 a b ∧ f a = x ∧ f b = y
Tactic: tauto