Theorem: SimpleGraph.card_edges_add_of_meet_empty (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 ⊔ H)) = card (edgeFinset G) + card (edgeFinset H)
Tactic:
rw [← disjoint_edges_iff_meet_empty,edgeFinset_sup]
State after:
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
⊢ Disjoint (edgeFinset G) (edgeFinset H) →
    card (edgeFinset G ∪ edgeFinset 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
⊢ Disjoint (edgeFinset G) (edgeFinset H) →
    card (edgeFinset G ∪ edgeFinset 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 : Disjoint (edgeFinset G) (edgeFinset H)
⊢ card (edgeFinset G ∪ edgeFinset 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 : Disjoint (edgeFinset G) (edgeFinset H)
⊢ card (edgeFinset G ∪ edgeFinset H) = card (edgeFinset G) + card (edgeFinset H)
Tactic:
exact card_disjoint_union h
State after:
no goals