Theorem: SimpleGraph.Menger.bot_iff_no_edge (Untitled/Graphs/Menger.lean)

State before:
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a : V
A B X Y Z : Finset V
h : Fintype.card (Dart G) = 0
⊢ G = ⊥
Tactic:
ext x y
State after:
case Adj.h.h.a
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a : V
A B X Y Z : Finset V
h : Fintype.card (Dart G) = 0
x y : V
⊢ Adj G x y ↔ Adj ⊥ x y

State before:
case Adj.h.h.a
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a : V
A B X Y Z : Finset V
h : Fintype.card (Dart G) = 0
x y : V
⊢ Adj G x y ↔ Adj ⊥ x y
Tactic:
simp
State after:
case Adj.h.h.a
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a : V
A B X Y Z : Finset V
h : Fintype.card (Dart G) = 0
x y : V
⊢ ¬Adj G x y

State before:
case Adj.h.h.a
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a : V
A B X Y Z : Finset V
h : Fintype.card (Dart G) = 0
x y : V
⊢ ¬Adj G x y
Tactic:
exact λ h' => isEmpty_iff.mp (Fintype.card_eq_zero_iff.mp h) ⟨⟨x, y⟩, h'⟩
State after:
no goals

State before:
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a : V
A B X Y Z : Finset V
h : G = ⊥
⊢ Fintype.card (Dart G) = 0
Tactic:
simpa only [h] using Fintype.card_eq_zero_iff.mpr <| isEmpty_iff.mpr Dart.is_adj
State after:
no goals