Theorem: GraphTheory.ES1.q5 (LeanCamCombi/ExampleSheets/Graph/ES1.lean)

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
hG : G.IsAcyclic
⊢ G.edgeFinset.card ≤ card α - 1
Tactic:
cases isEmpty_or_nonempty α
State after:
case inl
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
hG : G.IsAcyclic
h✝ : IsEmpty α
⊢ G.edgeFinset.card ≤ card α - 1

case inr
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
hG : G.IsAcyclic
h✝ : Nonempty α
⊢ G.edgeFinset.card ≤ card α - 1

State before:
case inr
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
hG : G.IsAcyclic
h✝ : Nonempty α
⊢ G.edgeFinset.card ≤ card α - 1
Tactic:
sorry
State after:
no goals

State before:
case inl
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
hG : G.IsAcyclic
h✝ : IsEmpty α
⊢ G.edgeFinset.card ≤ card α - 1
Tactic:
simp
State after:
no goals