-- Mathlib/Combinatorics/SimpleGraph/Operations.lean
lemma disjoint_sdiff_neighborFinset_image :
    Disjoint (G.edgeFinset \ G.incidenceFinset t) ((G.neighborFinset s).image (s(·, t)))

Proof state:
V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
e : Sym2 V
he : e ∈ G.edgeFinset \ G.incidenceFinset t
⊢ ∀ b ∈ image (fun x => s(x, t)) (G.neighborFinset s), e ≠ b

Tactic:
have : t ∉ e := by
  rw [mem_sdiff, mem_incidenceFinset] at he
  obtain ⟨_, h⟩ := he
  contrapose! h
  simp_all [incidenceSet]

Result:
V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
e : Sym2 V
he : e ∈ G.edgeFinset \ G.incidenceFinset t
this : t ∉ e
⊢ ∀ b ∈ image (fun x => s(x, t)) (G.neighborFinset s), e ≠ b

Proof state:
case intro
V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
e : Sym2 V
left✝ : e ∈ G.edgeFinset
h : e ∉ G.incidenceSet t
⊢ t ∉ e

Tactic:
contrapose! h

Result:
case intro
V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
e : Sym2 V
left✝ : e ∈ G.edgeFinset
h : t ∈ e
⊢ e ∈ G.incidenceSet t

Proof state:
V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
e : Sym2 V
he : e ∈ G.edgeFinset ∧ e ∉ G.incidenceSet t
⊢ t ∉ e

Tactic:
obtain ⟨_, h⟩ := he

Result:
case intro
V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
e : Sym2 V
left✝ : e ∈ G.edgeFinset
h : e ∉ G.incidenceSet t
⊢ t ∉ e

Proof state:
case intro
V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
e : Sym2 V
left✝ : e ∈ G.edgeFinset
h : t ∈ e
⊢ e ∈ G.incidenceSet t

Tactic:
simp_all [incidenceSet]

Result:
no goals

Proof state:
V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ ∀ a ∈ G.edgeFinset \ G.incidenceFinset t, ∀ b ∈ image (fun x => s(x, t)) (G.neighborFinset s), a ≠ b

Tactic:
intro e he

Result:
V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
e : Sym2 V
he : e ∈ G.edgeFinset \ G.incidenceFinset t
⊢ ∀ b ∈ image (fun x => s(x, t)) (G.neighborFinset s), e ≠ b

Proof state:
V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ Disjoint (G.edgeFinset \ G.incidenceFinset t) (image (fun x => s(x, t)) (G.neighborFinset s))

Tactic:
rw [disjoint_iff_ne]

Result:
V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ ∀ a ∈ G.edgeFinset \ G.incidenceFinset t, ∀ b ∈ image (fun x => s(x, t)) (G.neighborFinset s), a ≠ b

Proof state:
V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
e : Sym2 V
he : e ∈ G.edgeFinset \ G.incidenceFinset t
⊢ t ∉ e

Tactic:
rw [mem_sdiff, mem_incidenceFinset] at he

Result:
V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
e : Sym2 V
he : e ∈ G.edgeFinset ∧ e ∉ G.incidenceSet t
⊢ t ∉ e

Proof state:
V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
e : Sym2 V
he : e ∈ G.edgeFinset \ G.incidenceFinset t
this : t ∉ e
⊢ ∀ b ∈ image (fun x => s(x, t)) (G.neighborFinset s), e ≠ b

Tactic:
aesop

Result:
no goals