ι : Sort ?u.101434
𝕜 : Type ?u.101437
V : Type u
W : Type v
X : Type w
G : SimpleGraph V
G' : SimpleGraph W
a b c u v w : V
e : Sym2 V
h : ¬Adj G a b
hn : a ≠ b
⊢ ∀ (x : Sym2 V), x ∈ incidenceSet G a → ¬x ∈ incidenceSet G b
ι : Sort ?u.101434
𝕜 : Type ?u.101437
V : Type u
W : Type v
X : Type w
G : SimpleGraph V
G' : SimpleGraph W
a b c u v w : V
e : Sym2 V
h : ¬Adj G a b
hn : a ≠ b
⊢ incidenceSet G a ∩ incidenceSet G b = ∅
simp_rw [Set.eq_empty_iff_forall_not_mem, Set.mem_inter_iff, not_and]
ι : Sort ?u.101434
𝕜 : Type ?u.101437
V : Type u
W : Type v
X : Type w
G : SimpleGraph V
G' : SimpleGraph W
a b c u✝ v w : V
e : Sym2 V
h : ¬Adj G a b
hn : a ≠ b
u : Sym2 V
ha : u ∈ incidenceSet G a
hb : u ∈ incidenceSet G b
⊢ False
ι : Sort ?u.101434
𝕜 : Type ?u.101437
V : Type u
W : Type v
X : Type w
G : SimpleGraph V
G' : SimpleGraph W
a b c u v w : V
e : Sym2 V
h : ¬Adj G a b
hn : a ≠ b
⊢ ∀ (x : Sym2 V), x ∈ incidenceSet G a → ¬x ∈ incidenceSet G b
intro u ha hb
no goals
ι : Sort ?u.101434
𝕜 : Type ?u.101437
V : Type u
W : Type v
X : Type w
G : SimpleGraph V
G' : SimpleGraph W
a b c u✝ v w : V
e : Sym2 V
h : ¬Adj G a b
hn : a ≠ b
u : Sym2 V
ha : u ∈ incidenceSet G a
hb : u ∈ incidenceSet G b
⊢ False
exact h (G.adj_of_mem_incidenceSet hn ha hb)