internlm/Lean-Github huggingface dataset:
Theorem: SimpleGraph.Menger.sep_AB_of_sep₂_AX
Proof 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 ζ'
Proof 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
Theorem: SimpleGraph.Menger.sep_AB_of_sep₂_AX
Proof 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
Proof 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
Theorem: SimpleGraph.Menger.sep_AB_of_sep₂_AX
Proof 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⟩
Proof state after:
no goals
Theorem: SimpleGraph.Menger.sep_AB_of_sep₂_AX
Proof 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
Proof 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 δ
Theorem: SimpleGraph.Menger.sep_AB_of_sep₂_AX
Proof 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
Proof state after:
no goals
Theorem: SimpleGraph.Menger.sep_AB_of_sep₂_AX
Proof 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
Proof state after:
no goals
Theorem: SimpleGraph.Menger.massage_eq
Proof 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
hG : G₂ ≤ G₁
P : Finset (AB_Walk G₂ A B)
p₁ p₂ : { x // x ∈ P }
hP : pwd P
h : ∃ z ∈ Walk.support (massage hG ↑p₁).to_Walk, z ∈ Walk.support (massage hG ↑p₂).to_Walk
⊢ p₁ = p₂
Tactic:
by_contra hp
Proof 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
hG : G₂ ≤ G₁
P : Finset (AB_Walk G₂ A B)
p₁ p₂ : { x // x ∈ P }
hP : pwd P
h : ∃ z ∈ Walk.support (massage hG ↑p₁).to_Walk, z ∈ Walk.support (massage hG ↑p₂).to_Walk
hp : ¬p₁ = p₂
⊢ False
Theorem: SimpleGraph.Menger.massage_eq
Proof 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
hG : G₂ ≤ G₁
P : Finset (AB_Walk G₂ A B)
p₁ p₂ : { x // x ∈ P }
hP : pwd P
h : ∃ z ∈ Walk.support (massage hG ↑p₁).to_Walk, z ∈ Walk.support (massage hG ↑p₂).to_Walk
hp : ¬p₁ = p₂
⊢ False
Tactic:
obtain ⟨z, hz₁, hz₂⟩ := h
Proof 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
hG : G₂ ≤ G₁
P : Finset (AB_Walk G₂ A B)
p₁ p₂ : { x // x ∈ P }
hP : pwd P
hp : ¬p₁ = p₂
z : V
hz₁ : z ∈ Walk.support (massage hG ↑p₁).to_Walk
hz₂ : z ∈ Walk.support (massage hG ↑p₂).to_Walk
⊢ False
Theorem: SimpleGraph.Menger.massage_eq
Proof 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
hG : G₂ ≤ G₁
P : Finset (AB_Walk G₂ A B)
p₁ p₂ : { x // x ∈ P }
hP : pwd P
hp : ¬p₁ = p₂
z : V
hz₁ : z ∈ Walk.support (massage hG ↑p₁).to_Walk
hz₂ : z ∈ Walk.support (massage hG ↑p₂).to_Walk
⊢ False
Tactic:
have h1 := (p₁.val.massage_aux hG).prop.2 hz₁
Proof 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
hG : G₂ ≤ G₁
P : Finset (AB_Walk G₂ A B)
p₁ p₂ : { x // x ∈ P }
hP : pwd P
hp : ¬p₁ = p₂
z : V
hz₁ : z ∈ Walk.support (massage hG ↑p₁).to_Walk
hz₂ : z ∈ Walk.support (massage hG ↑p₂).to_Walk
h1 : z ∈ Walk.support (↑p₁).to_Walk
⊢ False
Theorem: SimpleGraph.Menger.massage_eq
Proof 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
hG : G₂ ≤ G₁
P : Finset (AB_Walk G₂ A B)
p₁ p₂ : { x // x ∈ P }
hP : pwd P
hp : ¬p₁ = p₂
z : V
hz₁ : z ∈ Walk.support (massage hG ↑p₁).to_Walk
hz₂ : z ∈ Walk.support (massage hG ↑p₂).to_Walk
h1 : z ∈ Walk.support (↑p₁).to_Walk
⊢ False
Tactic:
have h2 := (p₂.val.massage_aux hG).prop.2 hz₂
Proof 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
hG : G₂ ≤ G₁
P : Finset (AB_Walk G₂ A B)
p₁ p₂ : { x // x ∈ P }
hP : pwd P
hp : ¬p₁ = p₂
z : V
hz₁ : z ∈ Walk.support (massage hG ↑p₁).to_Walk
hz₂ : z ∈ Walk.support (massage hG ↑p₂).to_Walk
h1 : z ∈ Walk.support (↑p₁).to_Walk
h2 : z ∈ Walk.support (↑p₂).to_Walk
⊢ False
Theorem: SimpleGraph.Menger.massage_eq
Proof 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
hG : G₂ ≤ G₁
P : Finset (AB_Walk G₂ A B)
p₁ p₂ : { x // x ∈ P }
hP : pwd P
hp : ¬p₁ = p₂
z : V
hz₁ : z ∈ Walk.support (massage hG ↑p₁).to_Walk
hz₂ : z ∈ Walk.support (massage hG ↑p₂).to_Walk
h1 : z ∈ Walk.support (↑p₁).to_Walk
h2 : z ∈ Walk.support (↑p₂).to_Walk
⊢ False
Tactic:
have h3 : p₁.1 ≠ p₂.1 := by contrapose! hp ; ext <;> rw [hp]
Proof 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
hG : G₂ ≤ G₁
P : Finset (AB_Walk G₂ A B)
p₁ p₂ : { x // x ∈ P }
hP : pwd P
hp : ¬p₁ = p₂
z : V
hz₁ : z ∈ Walk.support (massage hG ↑p₁).to_Walk
hz₂ : z ∈ Walk.support (massage hG ↑p₂).to_Walk
h1 : z ∈ Walk.support (↑p₁).to_Walk
h2 : z ∈ Walk.support (↑p₂).to_Walk
h3 : ↑p₁ ≠ ↑p₂
⊢ False
Theorem: SimpleGraph.Menger.massage_eq
Proof 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
hG : G₂ ≤ G₁
P : Finset (AB_Walk G₂ A B)
p₁ p₂ : { x // x ∈ P }
hP : pwd P
hp : ¬p₁ = p₂
z : V
hz₁ : z ∈ Walk.support (massage hG ↑p₁).to_Walk
hz₂ : z ∈ Walk.support (massage hG ↑p₂).to_Walk
h1 : z ∈ Walk.support (↑p₁).to_Walk
h2 : z ∈ Walk.support (↑p₂).to_Walk
h3 : ↑p₁ ≠ ↑p₂
⊢ False
Tactic:
exact hP p₁.prop p₂.prop h3 h1 h2
Proof state after:
no goals
Theorem: SimpleGraph.Menger.massage_eq
Proof 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
hG : G₂ ≤ G₁
P : Finset (AB_Walk G₂ A B)
p₁ p₂ : { x // x ∈ P }
hP : pwd P
hp : ¬p₁ = p₂
z : V
hz₁ : z ∈ Walk.support (massage hG ↑p₁).to_Walk
hz₂ : z ∈ Walk.support (massage hG ↑p₂).to_Walk
h1 : z ∈ Walk.support (↑p₁).to_Walk
h2 : z ∈ Walk.support (↑p₂).to_Walk
⊢ ↑p₁ ≠ ↑p₂
Tactic:
contrapose! hp
Proof 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
hG : G₂ ≤ G₁
P : Finset (AB_Walk G₂ A B)
p₁ p₂ : { x // x ∈ P }
hP : pwd P
z : V
hz₁ : z ∈ Walk.support (massage hG ↑p₁).to_Walk
hz₂ : z ∈ Walk.support (massage hG ↑p₂).to_Walk
h1 : z ∈ Walk.support (↑p₁).to_Walk
h2 : z ∈ Walk.support (↑p₂).to_Walk
hp : ↑p₁ = ↑p₂
⊢ p₁ = p₂
Theorem: SimpleGraph.Menger.massage_eq
Proof 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
hG : G₂ ≤ G₁
P : Finset (AB_Walk G₂ A B)
p₁ p₂ : { x // x ∈ P }
hP : pwd P
z : V
hz₁ : z ∈ Walk.support (massage hG ↑p₁).to_Walk
hz₂ : z ∈ Walk.support (massage hG ↑p₂).to_Walk
h1 : z ∈ Walk.support (↑p₁).to_Walk
h2 : z ∈ Walk.support (↑p₂).to_Walk
hp : ↑p₁ = ↑p₂
⊢ p₁ = p₂
Tactic:
ext <;> rw [hp]
Proof state after:
no goals
Theorem: SimpleGraph.Menger.massage_disjoint
Proof 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₂ ≤ G₁
P : Finset (AB_Walk G₂ A B)
h₁ : pwd P
⊢ pwd (image (massage h) P)
Tactic:
rintro p₁ hp₁ p₂ hp₂ hp₁p₂ z hz₁ hz₂
Proof 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
h : G₂ ≤ G₁
P : Finset (AB_Walk G₂ A B)
h₁ : pwd P
p₁ : AB_Walk G₁ A B
hp₁ : p₁ ∈ ↑(image (massage h) P)
p₂ : AB_Walk G₁ A B
hp₂ : p₂ ∈ ↑(image (massage h) P)
hp₁p₂ : p₁ ≠ p₂
z : V
hz₁ : z ∈ Walk.support p₁.to_Walk
hz₂ : z ∈ Walk.support p₂.to_Walk
⊢ False
Theorem: SimpleGraph.Menger.massage_disjoint
Proof 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₂ ≤ G₁
P : Finset (AB_Walk G₂ A B)
h₁ : pwd P
p₁ : AB_Walk G₁ A B
hp₁ : p₁ ∈ ↑(image (massage h) P)
p₂ : AB_Walk G₁ A B
hp₂ : p₂ ∈ ↑(image (massage h) P)
hp₁p₂ : p₁ ≠ p₂
z : V
hz₁ : z ∈ Walk.support p₁.to_Walk
hz₂ : z ∈ Walk.support p₂.to_Walk
⊢ False
Tactic:
apply hp₁p₂
Proof 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
h : G₂ ≤ G₁
P : Finset (AB_Walk G₂ A B)
h₁ : pwd P
p₁ : AB_Walk G₁ A B
hp₁ : p₁ ∈ ↑(image (massage h) P)
p₂ : AB_Walk G₁ A B
hp₂ : p₂ ∈ ↑(image (massage h) P)
hp₁p₂ : p₁ ≠ p₂
z : V
hz₁ : z ∈ Walk.support p₁.to_Walk
hz₂ : z ∈ Walk.support p₂.to_Walk
⊢ p₁ = p₂
Theorem: SimpleGraph.Menger.massage_disjoint
Proof 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₂ ≤ G₁
P : Finset (AB_Walk G₂ A B)
h₁ : pwd P
p₁ : AB_Walk G₁ A B
hp₁ : p₁ ∈ ↑(image (massage h) P)
p₂ : AB_Walk G₁ A B
hp₂ : p₂ ∈ ↑(image (massage h) P)
hp₁p₂ : p₁ ≠ p₂
z : V
hz₁ : z ∈ Walk.support p₁.to_Walk
hz₂ : z ∈ Walk.support p₂.to_Walk
⊢ p₁ = p₂
Tactic:
choose q₁ hq₁ hq₁' using mem_image.mp hp₁
Proof 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
h : G₂ ≤ G₁
P : Finset (AB_Walk G₂ A B)
h₁ : pwd P
p₁ : AB_Walk G₁ A B
hp₁ : p₁ ∈ ↑(image (massage h) P)
p₂ : AB_Walk G₁ A B
hp₂ : p₂ ∈ ↑(image (massage h) P)
hp₁p₂ : p₁ ≠ p₂
z : V
hz₁ : z ∈ Walk.support p₁.to_Walk
hz₂ : z ∈ Walk.support p₂.to_Walk
q₁ : AB_Walk G₂ A B
hq₁ : q₁ ∈ P
hq₁' : massage h q₁ = p₁
⊢ p₁ = p₂
Theorem: SimpleGraph.Menger.massage_disjoint
Proof 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₂ ≤ G₁
P : Finset (AB_Walk G₂ A B)
h₁ : pwd P
p₁ : AB_Walk G₁ A B
hp₁ : p₁ ∈ ↑(image (massage h) P)
p₂ : AB_Walk G₁ A B
hp₂ : p₂ ∈ ↑(image (massage h) P)
hp₁p₂ : p₁ ≠ p₂
z : V
hz₁ : z ∈ Walk.support p₁.to_Walk
hz₂ : z ∈ Walk.support p₂.to_Walk
q₁ : AB_Walk G₂ A B
hq₁ : q₁ ∈ P
hq₁' : massage h q₁ = p₁
⊢ p₁ = p₂
Tactic:
choose q₂ hq₂ hq₂' using mem_image.mp hp₂
Proof 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
h : G₂ ≤ G₁
P : Finset (AB_Walk G₂ A B)
h₁ : pwd P
p₁ : AB_Walk G₁ A B
hp₁ : p₁ ∈ ↑(image (massage h) P)
p₂ : AB_Walk G₁ A B
hp₂ : p₂ ∈ ↑(image (massage h) P)
hp₁p₂ : p₁ ≠ p₂
z : V
hz₁ : z ∈ Walk.support p₁.to_Walk
hz₂ : z ∈ Walk.support p₂.to_Walk
q₁ : AB_Walk G₂ A B
hq₁ : q₁ ∈ P
hq₁' : massage h q₁ = p₁
q₂ : AB_Walk G₂ A B
hq₂ : q₂ ∈ P
hq₂' : massage h q₂ = p₂
⊢ p₁ = p₂
Theorem: SimpleGraph.Menger.massage_disjoint
Proof 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₂ ≤ G₁
P : Finset (AB_Walk G₂ A B)
h₁ : pwd P
p₁ : AB_Walk G₁ A B
hp₁ : p₁ ∈ ↑(image (massage h) P)
p₂ : AB_Walk G₁ A B
hp₂ : p₂ ∈ ↑(image (massage h) P)
hp₁p₂ : p₁ ≠ p₂
z : V
hz₁ : z ∈ Walk.support p₁.to_Walk
hz₂ : z ∈ Walk.support p₂.to_Walk
q₁ : AB_Walk G₂ A B
hq₁ : q₁ ∈ P
hq₁' : massage h q₁ = p₁
q₂ : AB_Walk G₂ A B
hq₂ : q₂ ∈ P
hq₂' : massage h q₂ = p₂
⊢ p₁ = p₂
Tactic:
subst_vars
Proof 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
h : G₂ ≤ G₁
P : Finset (AB_Walk G₂ A B)
h₁ : pwd P
z : V
q₁ : AB_Walk G₂ A B
hq₁ : q₁ ∈ P
q₂ : AB_Walk G₂ A B
hq₂ : q₂ ∈ P
hp₁ : massage h q₁ ∈ ↑(image (massage h) P)
hz₁ : z ∈ Walk.support (massage h q₁).to_Walk
hp₂ : massage h q₂ ∈ ↑(image (massage h) P)
hz₂ : z ∈ Walk.support (massage h q₂).to_Walk
hp₁p₂ : massage h q₁ ≠ massage h q₂
⊢ massage h q₁ = massage h q₂
Theorem: SimpleGraph.Menger.massage_disjoint
Proof 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₂ ≤ G₁
P : Finset (AB_Walk G₂ A B)
h₁ : pwd P
z : V
q₁ : AB_Walk G₂ A B
hq₁ : q₁ ∈ P
q₂ : AB_Walk G₂ A B
hq₂ : q₂ ∈ P
hp₁ : massage h q₁ ∈ ↑(image (massage h) P)
hz₁ : z ∈ Walk.support (massage h q₁).to_Walk
hp₂ : massage h q₂ ∈ ↑(image (massage h) P)
hz₂ : z ∈ Walk.support (massage h q₂).to_Walk
hp₁p₂ : massage h q₁ ≠ massage h q₂
⊢ massage h q₁ = massage h q₂
Tactic:
let γ₁ : P := ⟨q₁, hq₁⟩
Proof 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
h : G₂ ≤ G₁
P : Finset (AB_Walk G₂ A B)
h₁ : pwd P
z : V
q₁ : AB_Walk G₂ A B
hq₁ : q₁ ∈ P
q₂ : AB_Walk G₂ A B
hq₂ : q₂ ∈ P
hp₁ : massage h q₁ ∈ ↑(image (massage h) P)
hz₁ : z ∈ Walk.support (massage h q₁).to_Walk
hp₂ : massage h q₂ ∈ ↑(image (massage h) P)
hz₂ : z ∈ Walk.support (massage h q₂).to_Walk
hp₁p₂ : massage h q₁ ≠ massage h q₂
γ₁ : { x // x ∈ P } := { val := q₁, property := hq₁ }
⊢ massage h q₁ = massage h q₂
Theorem: SimpleGraph.Menger.massage_disjoint
Proof 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₂ ≤ G₁
P : Finset (AB_Walk G₂ A B)
h₁ : pwd P
z : V
q₁ : AB_Walk G₂ A B
hq₁ : q₁ ∈ P
q₂ : AB_Walk G₂ A B
hq₂ : q₂ ∈ P
hp₁ : massage h q₁ ∈ ↑(image (massage h) P)
hz₁ : z ∈ Walk.support (massage h q₁).to_Walk
hp₂ : massage h q₂ ∈ ↑(image (massage h) P)
hz₂ : z ∈ Walk.support (massage h q₂).to_Walk
hp₁p₂ : massage h q₁ ≠ massage h q₂
γ₁ : { x // x ∈ P } := { val := q₁, property := hq₁ }
⊢ massage h q₁ = massage h q₂
Tactic:
let γ₂ : P := ⟨q₂, hq₂⟩
Proof 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
h : G₂ ≤ G₁
P : Finset (AB_Walk G₂ A B)
h₁ : pwd P
z : V
q₁ : AB_Walk G₂ A B
hq₁ : q₁ ∈ P
q₂ : AB_Walk G₂ A B
hq₂ : q₂ ∈ P
hp₁ : massage h q₁ ∈ ↑(image (massage h) P)
hz₁ : z ∈ Walk.support (massage h q₁).to_Walk
hp₂ : massage h q₂ ∈ ↑(image (massage h) P)
hz₂ : z ∈ Walk.support (massage h q₂).to_Walk
hp₁p₂ : massage h q₁ ≠ massage h q₂
γ₁ : { x // x ∈ P } := { val := q₁, property := hq₁ }
γ₂ : { x // x ∈ P } := { val := q₂, property := hq₂ }
⊢ massage h q₁ = massage h q₂
Theorem: SimpleGraph.Menger.massage_disjoint
Proof 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₂ ≤ G₁
P : Finset (AB_Walk G₂ A B)
h₁ : pwd P
z : V
q₁ : AB_Walk G₂ A B
hq₁ : q₁ ∈ P
q₂ : AB_Walk G₂ A B
hq₂ : q₂ ∈ P
hp₁ : massage h q₁ ∈ ↑(image (massage h) P)
hz₁ : z ∈ Walk.support (massage h q₁).to_Walk
hp₂ : massage h q₂ ∈ ↑(image (massage h) P)
hz₂ : z ∈ Walk.support (massage h q₂).to_Walk
hp₁p₂ : massage h q₁ ≠ massage h q₂
γ₁ : { x // x ∈ P } := { val := q₁, property := hq₁ }
γ₂ : { x // x ∈ P } := { val := q₂, property := hq₂ }
⊢ massage h q₁ = massage h q₂
Tactic:
congr
Proof state after:
case e_p
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₂ ≤ G₁
P : Finset (AB_Walk G₂ A B)
h₁ : pwd P
z : V
q₁ : AB_Walk G₂ A B
hq₁ : q₁ ∈ P
q₂ : AB_Walk G₂ A B
hq₂ : q₂ ∈ P
hp₁ : massage h q₁ ∈ ↑(image (massage h) P)
hz₁ : z ∈ Walk.support (massage h q₁).to_Walk
hp₂ : massage h q₂ ∈ ↑(image (massage h) P)
hz₂ : z ∈ Walk.support (massage h q₂).to_Walk
hp₁p₂ : massage h q₁ ≠ massage h q₂
γ₁ : { x // x ∈ P } := { val := q₁, property := hq₁ }
γ₂ : { x // x ∈ P } := { val := q₂, property := hq₂ }
⊢ q₁ = q₂