Theorem: SimpleGraph.Menger.Menger (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
⊢ isMenger G
Tactic:
induction' h : Fintype.card G.edgeSet using Nat.strongInductionOn with n ih generalizing G
State after:
case ind
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G₁ G₂ : SimpleGraph V
a : V
A B X Y Z : Finset V
n : ℕ
ih : ∀ m < n, ∀ {G : SimpleGraph V}, Fintype.card ↑(edgeSet G) = m → isMenger G
G : SimpleGraph V
h : Fintype.card ↑(edgeSet G) = n
⊢ isMenger G

State before:
case ind
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G₁ G₂ : SimpleGraph V
a : V
A B X Y Z : Finset V
n : ℕ
ih : ∀ m < n, ∀ {G : SimpleGraph V}, Fintype.card ↑(edgeSet G) = m → isMenger G
G : SimpleGraph V
h : Fintype.card ↑(edgeSet G) = n
⊢ isMenger G
Tactic:
subst h
State after:
case ind
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G₁ G₂ : SimpleGraph V
a : V
A B X Y Z : Finset V
G : SimpleGraph V
ih : ∀ m < Fintype.card ↑(edgeSet G), ∀ {G : SimpleGraph V}, Fintype.card ↑(edgeSet G) = m → isMenger G
⊢ isMenger G

State before:
case ind
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G₁ G₂ : SimpleGraph V
a : V
A B X Y Z : Finset V
G : SimpleGraph V
ih : ∀ m < Fintype.card ↑(edgeSet G), ∀ {G : SimpleGraph V}, Fintype.card ↑(edgeSet G) = m → isMenger G
⊢ isMenger G
Tactic:
by_cases h' : Fintype.card G.Dart = 0
State after:
case pos
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G₁ G₂ : SimpleGraph V
a : V
A B X Y Z : Finset V
G : SimpleGraph V
ih : ∀ m < Fintype.card ↑(edgeSet G), ∀ {G : SimpleGraph V}, Fintype.card ↑(edgeSet G) = m → isMenger G
h' : Fintype.card (Dart G) = 0
⊢ isMenger G

case neg
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G₁ G₂ : SimpleGraph V
a : V
A B X Y Z : Finset V
G : SimpleGraph V
ih : ∀ m < Fintype.card ↑(edgeSet G), ∀ {G : SimpleGraph V}, Fintype.card ↑(edgeSet G) = m → isMenger G
h' : ¬Fintype.card (Dart G) = 0
⊢ isMenger G

State before:
case pos
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G₁ G₂ : SimpleGraph V
a : V
A B X Y Z : Finset V
G : SimpleGraph V
ih : ∀ m < Fintype.card ↑(edgeSet G), ∀ {G : SimpleGraph V}, Fintype.card ↑(edgeSet G) = m → isMenger G
h' : Fintype.card (Dart G) = 0
⊢ isMenger G
Tactic:
simp [bot_iff_no_edge.mp h']
State after:
no goals

State before:
case neg
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G₁ G₂ : SimpleGraph V
a : V
A B X Y Z : Finset V
G : SimpleGraph V
ih : ∀ m < Fintype.card ↑(edgeSet G), ∀ {G : SimpleGraph V}, Fintype.card ↑(edgeSet G) = m → isMenger G
h' : ¬Fintype.card (Dart G) = 0
⊢ isMenger G
Tactic:
have h2 : ¬ IsEmpty G.Dart := by simpa [← Fintype.card_eq_zero_iff]
State after:
case neg
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G₁ G₂ : SimpleGraph V
a : V
A B X Y Z : Finset V
G : SimpleGraph V
ih : ∀ m < Fintype.card ↑(edgeSet G), ∀ {G : SimpleGraph V}, Fintype.card ↑(edgeSet G) = m → isMenger G
h' : ¬Fintype.card (Dart G) = 0
h2 : ¬IsEmpty (Dart G)
⊢ isMenger G

State before:
case neg
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G₁ G₂ : SimpleGraph V
a : V
A B X Y Z : Finset V
G : SimpleGraph V
ih : ∀ m < Fintype.card ↑(edgeSet G), ∀ {G : SimpleGraph V}, Fintype.card ↑(edgeSet G) = m → isMenger G
h' : ¬Fintype.card (Dart G) = 0
h2 : ¬IsEmpty (Dart G)
⊢ isMenger G
Tactic:
obtain ⟨e⟩ := not_isEmpty_iff.mp h2
State after:
case neg.intro
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G₁ G₂ : SimpleGraph V
a : V
A B X Y Z : Finset V
G : SimpleGraph V
ih : ∀ m < Fintype.card ↑(edgeSet G), ∀ {G : SimpleGraph V}, Fintype.card ↑(edgeSet G) = m → isMenger G
h' : ¬Fintype.card (Dart G) = 0
h2 : ¬IsEmpty (Dart G)
e : Dart G
⊢ isMenger G

State before:
case neg.intro
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G₁ G₂ : SimpleGraph V
a : V
A B X Y Z : Finset V
G : SimpleGraph V
ih : ∀ m < Fintype.card ↑(edgeSet G), ∀ {G : SimpleGraph V}, Fintype.card ↑(edgeSet G) = m → isMenger G
h' : ¬Fintype.card (Dart G) = 0
h2 : ¬IsEmpty (Dart G)
e : Dart G
⊢ isMenger G
Tactic:
refine induction_step e (ih _ contract_edge.fewer_edges rfl) (ih _ (Minus.card_edge e.edge_mem) rfl)
State after:
no goals

State before:
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G₁ G₂ : SimpleGraph V
a : V
A B X Y Z : Finset V
G : SimpleGraph V
ih : ∀ m < Fintype.card ↑(edgeSet G), ∀ {G : SimpleGraph V}, Fintype.card ↑(edgeSet G) = m → isMenger G
h' : ¬Fintype.card (Dart G) = 0
⊢ ¬IsEmpty (Dart G)
Tactic:
simpa [← Fintype.card_eq_zero_iff]
State after:
no goals