case Adj.h.h.a
ι : Sort ?u.83783
𝕜 : Type ?u.83786
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
s✝ s t : Set (Sym2 V)
v w : V
⊢ Adj (fromEdgeSet s ⊓ fromEdgeSet t) v w ↔ Adj (fromEdgeSet (s ∩ t)) v w
ι : Sort ?u.83783
𝕜 : Type ?u.83786
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
s✝ s t : Set (Sym2 V)
⊢ fromEdgeSet s ⊓ fromEdgeSet t = fromEdgeSet (s ∩ t)
ext (v w)
case Adj.h.h.a
ι : Sort ?u.83783
𝕜 : Type ?u.83786
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
s✝ s t : Set (Sym2 V)
v w : V
⊢ (Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ s ∧ ¬v = w) ∧ Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ t ∧ ¬v = w ↔
    (Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ s ∧ Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ t) ∧ ¬v = w
case Adj.h.h.a
ι : Sort ?u.83783
𝕜 : Type ?u.83786
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
s✝ s t : Set (Sym2 V)
v w : V
⊢ Adj (fromEdgeSet s ⊓ fromEdgeSet t) v w ↔ Adj (fromEdgeSet (s ∩ t)) v w
simp only [fromEdgeSet_adj, Set.mem_inter_iff, Ne.def, inf_adj]
no goals
case Adj.h.h.a
ι : Sort ?u.83783
𝕜 : Type ?u.83786
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
s✝ s t : Set (Sym2 V)
v w : V
⊢ (Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ s ∧ ¬v = w) ∧ Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ t ∧ ¬v = w ↔
    (Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ s ∧ Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ t) ∧ ¬v = w
tauto