Theorem: SimpleGraph.spanningCoe_induce (LeanCamCombi/Mathlib/Combinatorics/SimpleGraph/Maps.lean)

State before:
α : Type u_1
G : SimpleGraph α
s : Set α
⊢ (induce s G).spanningCoe = G.ind s
Tactic:
ext
State after:
case Adj.h.h.a
α : Type u_1
G : SimpleGraph α
s : Set α
x✝¹ x✝ : α
⊢ (induce s G).spanningCoe.Adj x✝¹ x✝ ↔ (G.ind s).Adj x✝¹ x✝

State before:
case Adj.h.h.a
α : Type u_1
G : SimpleGraph α
s : Set α
x✝¹ x✝ : α
⊢ (induce s G).spanningCoe.Adj x✝¹ x✝ ↔ (G.ind s).Adj x✝¹ x✝
Tactic:
simp [← and_assoc]
State after:
no goals