case h
ι : Sort ?u.71069
𝕜 : Type ?u.71072
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
G₁ G₂ G : SimpleGraph V
s : Set (Sym2 V)
e : Sym2 V
⊢ e ∈ edgeSet G \ (s \ {e | Sym2.IsDiag e}) ↔ e ∈ edgeSet G \ s
ι : Sort ?u.71069
𝕜 : Type ?u.71072
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
G₁ G₂ G : SimpleGraph V
s : Set (Sym2 V)
⊢ edgeSet G \ (s \ {e | Sym2.IsDiag e}) = edgeSet G \ s
ext e
case h
ι : Sort ?u.71069
𝕜 : Type ?u.71072
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
G₁ G₂ G : SimpleGraph V
s : Set (Sym2 V)
e : Sym2 V
⊢ e ∈ edgeSet G → (e ∈ s → Sym2.IsDiag e ↔ ¬e ∈ s)
case h
ι : Sort ?u.71069
𝕜 : Type ?u.71072
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
G₁ G₂ G : SimpleGraph V
s : Set (Sym2 V)
e : Sym2 V
⊢ e ∈ edgeSet G \ (s \ {e | Sym2.IsDiag e}) ↔ e ∈ edgeSet G \ s
simp only [Set.mem_diff, Set.mem_setOf_eq, not_and, not_not, and_congr_right_iff]
case h
ι : Sort ?u.71069
𝕜 : Type ?u.71072
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
G₁ G₂ G : SimpleGraph V
s : Set (Sym2 V)
e : Sym2 V
h : e ∈ edgeSet G
⊢ e ∈ s → Sym2.IsDiag e ↔ ¬e ∈ s
case h
ι : Sort ?u.71069
𝕜 : Type ?u.71072
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
G₁ G₂ G : SimpleGraph V
s : Set (Sym2 V)
e : Sym2 V
⊢ e ∈ edgeSet G → (e ∈ s → Sym2.IsDiag e ↔ ¬e ∈ s)
intro h
no goals
case h
ι : Sort ?u.71069
𝕜 : Type ?u.71072
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
G₁ G₂ G : SimpleGraph V
s : Set (Sym2 V)
e : Sym2 V
h : e ∈ edgeSet G
⊢ e ∈ s → Sym2.IsDiag e ↔ ¬e ∈ s
simp only [G.not_isDiag_of_mem_edgeSet h, imp_false]