Theorem: SimpleGraph.eq_imp_edges_card_eq (Turan4/Fedges.lean)

State before:
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
⊢ G = H → card (edgeFinset G) = card (edgeFinset H)
Tactic:
intro h
State after:
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
h : G = H
⊢ card (edgeFinset G) = card (edgeFinset H)

State before:
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
h : G = H
⊢ card (edgeFinset G) = card (edgeFinset H)
Tactic:
rw [eq_iff_edges_eq.mp h]
State after:
no goals