Theorem: SimpleGraph.Menger.sep_AB_of_sep₂_AX (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
e : Dart G
ex_in_X : e.toProd.1 ∈ X
ey_in_X : e.toProd.2 ∈ X
X_sep_AB : Separates G A B X
Z_sep₂_AX : Separates (G -ₑ Dart.edge e) A X Z
⊢ Separates G A B Z
Tactic:
intro γ
State after:
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
e : Dart G
ex_in_X : e.toProd.1 ∈ X
ey_in_X : e.toProd.2 ∈ X
X_sep_AB : Separates G A B X
Z_sep₂_AX : Separates (G -ₑ Dart.edge e) A X Z
γ : AB_Walk G A B
⊢ ∃ x ∈ Z, x ∈ Walk.support γ.to_Walk

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
e : Dart G
ex_in_X : e.toProd.1 ∈ X
ey_in_X : e.toProd.2 ∈ X
X_sep_AB : Separates G A B X
Z_sep₂_AX : Separates (G -ₑ Dart.edge e) A X Z
γ : AB_Walk G A B
⊢ ∃ x ∈ Z, x ∈ Walk.support γ.to_Walk
Tactic:
obtain ⟨x, hx1, hx2⟩ := X_sep_AB γ
State after:
case intro.intro
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
e : Dart G
ex_in_X : e.toProd.1 ∈ X
ey_in_X : e.toProd.2 ∈ X
X_sep_AB : Separates G A B X
Z_sep₂_AX : Separates (G -ₑ Dart.edge e) A X Z
γ : AB_Walk G A B
x : V
hx1 : x ∈ X
hx2 : x ∈ Walk.support γ.to_Walk
⊢ ∃ x ∈ Z, x ∈ Walk.support γ.to_Walk

State before:
case intro.intro
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
e : Dart G
ex_in_X : e.toProd.1 ∈ X
ey_in_X : e.toProd.2 ∈ X
X_sep_AB : Separates G A B X
Z_sep₂_AX : Separates (G -ₑ Dart.edge e) A X Z
γ : AB_Walk G A B
x : V
hx1 : x ∈ X
hx2 : x ∈ Walk.support γ.to_Walk
δ : Walk G γ.a (entrance γ.to_Walk (fun x => x ∈ X) (_ : ∃ v ∈ Walk.support γ.to_Walk, (fun x => x ∈ X) v)) :=
  takeUntil γ.to_Walk (fun x => x ∈ X) (_ : ∃ v ∈ Walk.support γ.to_Walk, (fun x => x ∈ X) v)
key : Walk.transportable_to (G -ₑ Dart.edge e) δ
⊢ ∃ x ∈ Z, x ∈ Walk.support γ.to_Walk
Tactic:
obtain ⟨ζ, hζ⟩ := δ.transport key
State after:
case intro.intro.mk
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
e : Dart G
ex_in_X : e.toProd.1 ∈ X
ey_in_X : e.toProd.2 ∈ X
X_sep_AB : Separates G A B X
Z_sep₂_AX : Separates (G -ₑ Dart.edge e) A X Z
γ : AB_Walk G A B
x : V
hx1 : x ∈ X
hx2 : x ∈ Walk.support γ.to_Walk
δ : Walk G γ.a (entrance γ.to_Walk (fun x => x ∈ X) (_ : ∃ v ∈ Walk.support γ.to_Walk, (fun x => x ∈ X) v)) :=
  takeUntil γ.to_Walk (fun x => x ∈ X) (_ : ∃ v ∈ Walk.support γ.to_Walk, (fun x => x ∈ X) v)
key : Walk.transportable_to (G -ₑ Dart.edge e) δ
ζ :
  Walk (G -ₑ Dart.edge e) γ.a
    (entrance γ.to_Walk (fun x => x ∈ X) (_ : ∃ v ∈ Walk.support γ.to_Walk, (fun x => x ∈ X) v))
hζ : Walk.support ζ = Walk.support δ
⊢ ∃ x ∈ Z, x ∈ Walk.support γ.to_Walk

State before:
case intro.intro.mk
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
e : Dart G
ex_in_X : e.toProd.1 ∈ X
ey_in_X : e.toProd.2 ∈ X
X_sep_AB : Separates G A B X
Z_sep₂_AX : Separates (G -ₑ Dart.edge e) A X Z
γ : AB_Walk G A B
x : V
hx1 : x ∈ X
hx2 : x ∈ Walk.support γ.to_Walk
δ : Walk G γ.a (entrance γ.to_Walk (fun x => x ∈ X) (_ : ∃ v ∈ Walk.support γ.to_Walk, (fun x => x ∈ X) v)) :=
  takeUntil γ.to_Walk (fun x => x ∈ X) (_ : ∃ v ∈ Walk.support γ.to_Walk, (fun x => x ∈ X) v)
key : Walk.transportable_to (G -ₑ Dart.edge e) δ
ζ :
  Walk (G -ₑ Dart.edge e) γ.a
    (entrance γ.to_Walk (fun x => x ∈ X) (_ : ∃ v ∈ Walk.support γ.to_Walk, (fun x => x ∈ X) v))
hζ : Walk.support ζ = Walk.support δ
ζ' : AB_Walk (G -ₑ Dart.edge e) A X :=
  { a := γ.a, b := entrance γ.to_Walk (fun x => x ∈ X) (_ : ∃ v ∈ Walk.support γ.to_Walk, (fun x => x ∈ X) v),
    ha := (_ : γ.a ∈ A),
    hb := (_ : entrance γ.to_Walk (fun x => x ∈ X) (_ : ∃ v ∈ Walk.support γ.to_Walk, (fun x => x ∈ X) v) ∈ X),
    to_Walk := ζ }
⊢ ∃ x ∈ Z, x ∈ Walk.support γ.to_Walk
Tactic:
obtain ⟨z, hz1, hz2⟩ := Z_sep₂_AX ζ'
State after:
case intro.intro.mk.intro.intro
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
e : Dart G
ex_in_X : e.toProd.1 ∈ X
ey_in_X : e.toProd.2 ∈ X
X_sep_AB : Separates G A B X
Z_sep₂_AX : Separates (G -ₑ Dart.edge e) A X Z
γ : AB_Walk G A B
x : V
hx1 : x ∈ X
hx2 : x ∈ Walk.support γ.to_Walk
δ : Walk G γ.a (entrance γ.to_Walk (fun x => x ∈ X) (_ : ∃ v ∈ Walk.support γ.to_Walk, (fun x => x ∈ X) v)) :=
  takeUntil γ.to_Walk (fun x => x ∈ X) (_ : ∃ v ∈ Walk.support γ.to_Walk, (fun x => x ∈ X) v)
key : Walk.transportable_to (G -ₑ Dart.edge e) δ
ζ :
  Walk (G -ₑ Dart.edge e) γ.a
    (entrance γ.to_Walk (fun x => x ∈ X) (_ : ∃ v ∈ Walk.support γ.to_Walk, (fun x => x ∈ X) v))
hζ : Walk.support ζ = Walk.support δ
ζ' : AB_Walk (G -ₑ Dart.edge e) A X :=
  { a := γ.a, b := entrance γ.to_Walk (fun x => x ∈ X) (_ : ∃ v ∈ Walk.support γ.to_Walk, (fun x => x ∈ X) v),
    ha := (_ : γ.a ∈ A),
    hb := (_ : entrance γ.to_Walk (fun x => x ∈ X) (_ : ∃ v ∈ Walk.support γ.to_Walk, (fun x => x ∈ X) v) ∈ X),
    to_Walk := ζ }
z : V
hz1 : z ∈ Z
hz2 : z ∈ Walk.support ζ'.to_Walk
⊢ ∃ x ∈ Z, x ∈ Walk.support γ.to_Walk

State before:
case intro.intro.mk.intro.intro
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
e : Dart G
ex_in_X : e.toProd.1 ∈ X
ey_in_X : e.toProd.2 ∈ X
X_sep_AB : Separates G A B X
Z_sep₂_AX : Separates (G -ₑ Dart.edge e) A X Z
γ : AB_Walk G A B
x : V
hx1 : x ∈ X
hx2 : x ∈ Walk.support γ.to_Walk
δ : Walk G γ.a (entrance γ.to_Walk (fun x => x ∈ X) (_ : ∃ v ∈ Walk.support γ.to_Walk, (fun x => x ∈ X) v)) :=
  takeUntil γ.to_Walk (fun x => x ∈ X) (_ : ∃ v ∈ Walk.support γ.to_Walk, (fun x => x ∈ X) v)
key : Walk.transportable_to (G -ₑ Dart.edge e) δ
ζ :
  Walk (G -ₑ Dart.edge e) γ.a
    (entrance γ.to_Walk (fun x => x ∈ X) (_ : ∃ v ∈ Walk.support γ.to_Walk, (fun x => x ∈ X) v))
hζ : Walk.support ζ = Walk.support δ
ζ' : AB_Walk (G -ₑ Dart.edge e) A X :=
  { a := γ.a, b := entrance γ.to_Walk (fun x => x ∈ X) (_ : ∃ v ∈ Walk.support γ.to_Walk, (fun x => x ∈ X) v),
    ha := (_ : γ.a ∈ A),
    hb := (_ : entrance γ.to_Walk (fun x => x ∈ X) (_ : ∃ v ∈ Walk.support γ.to_Walk, (fun x => x ∈ X) v) ∈ X),
    to_Walk := ζ }
z : V
hz1 : z ∈ Z
hz2 : z ∈ Walk.support ζ'.to_Walk
⊢ ∃ x ∈ Z, x ∈ Walk.support γ.to_Walk
Tactic:
simp [hζ] at hz2
State after:
case intro.intro.mk.intro.intro
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
e : Dart G
ex_in_X : e.toProd.1 ∈ X
ey_in_X : e.toProd.2 ∈ X
X_sep_AB : Separates G A B X
Z_sep₂_AX : Separates (G -ₑ Dart.edge e) A X Z
γ : AB_Walk G A B
x : V
hx1 : x ∈ X
hx2 : x ∈ Walk.support γ.to_Walk
δ : Walk G γ.a (entrance γ.to_Walk (fun x => x ∈ X) (_ : ∃ v ∈ Walk.support γ.to_Walk, (fun x => x ∈ X) v)) :=
  takeUntil γ.to_Walk (fun x => x ∈ X) (_ : ∃ v ∈ Walk.support γ.to_Walk, (fun x => x ∈ X) v)
key : Walk.transportable_to (G -ₑ Dart.edge e) δ
ζ :
  Walk (G -ₑ Dart.edge e) γ.a
    (entrance γ.to_Walk (fun x => x ∈ X) (_ : ∃ v ∈ Walk.support γ.to_Walk, (fun x => x ∈ X) v))
hζ : Walk.support ζ = Walk.support δ
ζ' : AB_Walk (G -ₑ Dart.edge e) A X :=
  { a := γ.a, b := entrance γ.to_Walk (fun x => x ∈ X) (_ : ∃ v ∈ Walk.support γ.to_Walk, (fun x => x ∈ X) v),
    ha := (_ : γ.a ∈ A),
    hb := (_ : entrance γ.to_Walk (fun x => x ∈ X) (_ : ∃ v ∈ Walk.support γ.to_Walk, (fun x => x ∈ X) v) ∈ X),
    to_Walk := ζ }
z : V
hz1 : z ∈ Z
hz2 : z ∈ Walk.support (takeUntil γ.to_Walk (fun x => x ∈ X) (_ : ∃ v ∈ Walk.support γ.to_Walk, v ∈ X))
⊢ ∃ x ∈ Z, x ∈ Walk.support γ.to_Walk

State before:
case intro.intro.mk.intro.intro
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
e : Dart G
ex_in_X : e.toProd.1 ∈ X
ey_in_X : e.toProd.2 ∈ X
X_sep_AB : Separates G A B X
Z_sep₂_AX : Separates (G -ₑ Dart.edge e) A X Z
γ : AB_Walk G A B
x : V
hx1 : x ∈ X
hx2 : x ∈ Walk.support γ.to_Walk
δ : Walk G γ.a (entrance γ.to_Walk (fun x => x ∈ X) (_ : ∃ v ∈ Walk.support γ.to_Walk, (fun x => x ∈ X) v)) :=
  takeUntil γ.to_Walk (fun x => x ∈ X) (_ : ∃ v ∈ Walk.support γ.to_Walk, (fun x => x ∈ X) v)
key : Walk.transportable_to (G -ₑ Dart.edge e) δ
ζ :
  Walk (G -ₑ Dart.edge e) γ.a
    (entrance γ.to_Walk (fun x => x ∈ X) (_ : ∃ v ∈ Walk.support γ.to_Walk, (fun x => x ∈ X) v))
hζ : Walk.support ζ = Walk.support δ
ζ' : AB_Walk (G -ₑ Dart.edge e) A X :=
  { a := γ.a, b := entrance γ.to_Walk (fun x => x ∈ X) (_ : ∃ v ∈ Walk.support γ.to_Walk, (fun x => x ∈ X) v),
    ha := (_ : γ.a ∈ A),
    hb := (_ : entrance γ.to_Walk (fun x => x ∈ X) (_ : ∃ v ∈ Walk.support γ.to_Walk, (fun x => x ∈ X) v) ∈ X),
    to_Walk := ζ }
z : V
hz1 : z ∈ Z
hz2 : z ∈ Walk.support (takeUntil γ.to_Walk (fun x => x ∈ X) (_ : ∃ v ∈ Walk.support γ.to_Walk, v ∈ X))
this :
  Walk.support ↑(takeUntil_aux γ.to_Walk (fun x => x ∈ X) (_ : ∃ v ∈ Walk.support γ.to_Walk, (fun x => x ∈ X) v)).snd ⊆
    Walk.support γ.to_Walk
⊢ ∃ x ∈ Z, x ∈ Walk.support γ.to_Walk
Tactic:
refine ⟨z, hz1, this hz2⟩
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
e : Dart G
ex_in_X : e.toProd.1 ∈ X
ey_in_X : e.toProd.2 ∈ X
X_sep_AB : Separates G A B X
Z_sep₂_AX : Separates (G -ₑ Dart.edge e) A X Z
γ : AB_Walk G A B
x : V
hx1 : x ∈ X
hx2 : x ∈ Walk.support γ.to_Walk
δ : Walk G γ.a (entrance γ.to_Walk (fun x => x ∈ X) (_ : ∃ v ∈ Walk.support γ.to_Walk, (fun x => x ∈ X) v)) :=
  takeUntil γ.to_Walk (fun x => x ∈ X) (_ : ∃ v ∈ Walk.support γ.to_Walk, (fun x => x ∈ X) v)
⊢ Walk.transportable_to (G -ₑ Dart.edge e) δ
Tactic:
apply transportable_of_not_dart
State after:
case h
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
e : Dart G
ex_in_X : e.toProd.1 ∈ X
ey_in_X : e.toProd.2 ∈ X
X_sep_AB : Separates G A B X
Z_sep₂_AX : Separates (G -ₑ Dart.edge e) A X Z
γ : AB_Walk G A B
x : V
hx1 : x ∈ X
hx2 : x ∈ Walk.support γ.to_Walk
δ : Walk G γ.a (entrance γ.to_Walk (fun x => x ∈ X) (_ : ∃ v ∈ Walk.support γ.to_Walk, (fun x => x ∈ X) v)) :=
  takeUntil γ.to_Walk (fun x => x ∈ X) (_ : ∃ v ∈ Walk.support γ.to_Walk, (fun x => x ∈ X) v)
⊢ e ∉ Walk.darts δ

case h'
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
e : Dart G
ex_in_X : e.toProd.1 ∈ X
ey_in_X : e.toProd.2 ∈ X
X_sep_AB : Separates G A B X
Z_sep₂_AX : Separates (G -ₑ Dart.edge e) A X Z
γ : AB_Walk G A B
x : V
hx1 : x ∈ X
hx2 : x ∈ Walk.support γ.to_Walk
δ : Walk G γ.a (entrance γ.to_Walk (fun x => x ∈ X) (_ : ∃ v ∈ Walk.support γ.to_Walk, (fun x => x ∈ X) v)) :=
  takeUntil γ.to_Walk (fun x => x ∈ X) (_ : ∃ v ∈ Walk.support γ.to_Walk, (fun x => x ∈ X) v)
⊢ Dart.symm e ∉ Walk.darts δ

State before:
case h
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
e : Dart G
ex_in_X : e.toProd.1 ∈ X
ey_in_X : e.toProd.2 ∈ X
X_sep_AB : Separates G A B X
Z_sep₂_AX : Separates (G -ₑ Dart.edge e) A X Z
γ : AB_Walk G A B
x : V
hx1 : x ∈ X
hx2 : x ∈ Walk.support γ.to_Walk
δ : Walk G γ.a (entrance γ.to_Walk (fun x => x ∈ X) (_ : ∃ v ∈ Walk.support γ.to_Walk, (fun x => x ∈ X) v)) :=
  takeUntil γ.to_Walk (fun x => x ∈ X) (_ : ∃ v ∈ Walk.support γ.to_Walk, (fun x => x ∈ X) v)
⊢ e ∉ Walk.darts δ
Tactic:
sorry
State after:
no goals

State before:
case h'
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
e : Dart G
ex_in_X : e.toProd.1 ∈ X
ey_in_X : e.toProd.2 ∈ X
X_sep_AB : Separates G A B X
Z_sep₂_AX : Separates (G -ₑ Dart.edge e) A X Z
γ : AB_Walk G A B
x : V
hx1 : x ∈ X
hx2 : x ∈ Walk.support γ.to_Walk
δ : Walk G γ.a (entrance γ.to_Walk (fun x => x ∈ X) (_ : ∃ v ∈ Walk.support γ.to_Walk, (fun x => x ∈ X) v)) :=
  takeUntil γ.to_Walk (fun x => x ∈ X) (_ : ∃ v ∈ Walk.support γ.to_Walk, (fun x => x ∈ X) v)
⊢ Dart.symm e ∉ Walk.darts δ
Tactic:
sorry
State after:
no goals