internlm/Lean-Github huggingface dataset:
Theorem: SimpleGraph.Menger.meet_sub_X
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
X_sep_AB : Separates G A B X
ap bp : V
pa : ap ∈ A
pb : bp ∈ X
p : Walk G ap bp
hp : minimal { a := ap, b := bp, ha := pa, hb := pb, to_Walk := p }
aq bq : V
qa : aq ∈ B
qb : bq ∈ X
q : Walk G aq bq
hq : minimal { a := aq, b := bq, ha := qa, hb := qb, to_Walk := q }
x : V
hx₁ : x ∈ Walk.support p
hx₂ : x ∈ Walk.support q
x✝ : x ∉ X
p' : Walk G ap ↑{ val := x, property := (_ : x = x) }
hp1 : Walk.support p' <+: Walk.support p
right✝ : ∀ v ∈ Walk.init₀ p', ¬v = x
⊢ ∀ y ∈ Walk.support p', y ∉ X
Tactic:
intro y hy
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
X_sep_AB : Separates G A B X
ap bp : V
pa : ap ∈ A
pb : bp ∈ X
p : Walk G ap bp
hp : minimal { a := ap, b := bp, ha := pa, hb := pb, to_Walk := p }
aq bq : V
qa : aq ∈ B
qb : bq ∈ X
q : Walk G aq bq
hq : minimal { a := aq, b := bq, ha := qa, hb := qb, to_Walk := q }
x : V
hx₁ : x ∈ Walk.support p
hx₂ : x ∈ Walk.support q
x✝ : x ∉ X
p' : Walk G ap ↑{ val := x, property := (_ : x = x) }
hp1 : Walk.support p' <+: Walk.support p
right✝ : ∀ v ∈ Walk.init₀ p', ¬v = x
y : V
hy : y ∈ Walk.support p'
⊢ y ∉ X
Theorem: SimpleGraph.Menger.meet_sub_X
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
X_sep_AB : Separates G A B X
ap bp : V
pa : ap ∈ A
pb : bp ∈ X
p : Walk G ap bp
hp : minimal { a := ap, b := bp, ha := pa, hb := pb, to_Walk := p }
aq bq : V
qa : aq ∈ B
qb : bq ∈ X
q : Walk G aq bq
hq : minimal { a := aq, b := bq, ha := qa, hb := qb, to_Walk := q }
x : V
hx₁ : x ∈ Walk.support p
hx₂ : x ∈ Walk.support q
x✝ : x ∉ X
p' : Walk G ap ↑{ val := x, property := (_ : x = x) }
hp1 : Walk.support p' <+: Walk.support p
right✝ : ∀ v ∈ Walk.init₀ p', ¬v = x
y : V
hy : y ∈ Walk.support p'
⊢ y ∉ X
Tactic:
simp [Walk.support_eq_init₀_union_last] at hy
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
X_sep_AB : Separates G A B X
ap bp : V
pa : ap ∈ A
pb : bp ∈ X
p : Walk G ap bp
hp : minimal { a := ap, b := bp, ha := pa, hb := pb, to_Walk := p }
aq bq : V
qa : aq ∈ B
qb : bq ∈ X
q : Walk G aq bq
hq : minimal { a := aq, b := bq, ha := qa, hb := qb, to_Walk := q }
x : V
hx₁ : x ∈ Walk.support p
hx₂ : x ∈ Walk.support q
x✝ : x ∉ X
p' : Walk G ap ↑{ val := x, property := (_ : x = x) }
hp1 : Walk.support p' <+: Walk.support p
right✝ : ∀ v ∈ Walk.init₀ p', ¬v = x
y : V
hy : y ∈ Walk.init₀ p' ∨ y = x
⊢ y ∉ X
Theorem: SimpleGraph.Menger.meet_sub_X
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
X_sep_AB : Separates G A B X
ap bp : V
pa : ap ∈ A
pb : bp ∈ X
p : Walk G ap bp
hp : minimal { a := ap, b := bp, ha := pa, hb := pb, to_Walk := p }
aq bq : V
qa : aq ∈ B
qb : bq ∈ X
q : Walk G aq bq
hq : minimal { a := aq, b := bq, ha := qa, hb := qb, to_Walk := q }
x : V
hx₁ : x ∈ Walk.support p
hx₂ : x ∈ Walk.support q
x✝ : x ∉ X
p' : Walk G ap ↑{ val := x, property := (_ : x = x) }
hp1 : Walk.support p' <+: Walk.support p
right✝ : ∀ v ∈ Walk.init₀ p', ¬v = x
y : V
hy : y ∈ Walk.init₀ p' ∨ y = x
⊢ y ∉ X
Tactic:
cases hy with
| inl h => exact hp.1 y <| Walk.init₀_subset_of_support_prefix hp1 h
| inr h => rwa [h]
Proof state after:
no goals
Theorem: SimpleGraph.Menger.meet_sub_X
Proof state before:
case inl
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
X_sep_AB : Separates G A B X
ap bp : V
pa : ap ∈ A
pb : bp ∈ X
p : Walk G ap bp
hp : minimal { a := ap, b := bp, ha := pa, hb := pb, to_Walk := p }
aq bq : V
qa : aq ∈ B
qb : bq ∈ X
q : Walk G aq bq
hq : minimal { a := aq, b := bq, ha := qa, hb := qb, to_Walk := q }
x : V
hx₁ : x ∈ Walk.support p
hx₂ : x ∈ Walk.support q
x✝ : x ∉ X
p' : Walk G ap ↑{ val := x, property := (_ : x = x) }
hp1 : Walk.support p' <+: Walk.support p
right✝ : ∀ v ∈ Walk.init₀ p', ¬v = x
y : V
h : y ∈ Walk.init₀ p'
⊢ y ∉ X
Tactic:
exact hp.1 y <| Walk.init₀_subset_of_support_prefix hp1 h
Proof state after:
no goals
Theorem: SimpleGraph.Menger.meet_sub_X
Proof state before:
case inr
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
X_sep_AB : Separates G A B X
ap bp : V
pa : ap ∈ A
pb : bp ∈ X
p : Walk G ap bp
hp : minimal { a := ap, b := bp, ha := pa, hb := pb, to_Walk := p }
aq bq : V
qa : aq ∈ B
qb : bq ∈ X
q : Walk G aq bq
hq : minimal { a := aq, b := bq, ha := qa, hb := qb, to_Walk := q }
x : V
hx₁ : x ∈ Walk.support p
hx₂ : x ∈ Walk.support q
x✝ : x ∉ X
p' : Walk G ap ↑{ val := x, property := (_ : x = x) }
hp1 : Walk.support p' <+: Walk.support p
right✝ : ∀ v ∈ Walk.init₀ p', ¬v = x
y : V
h : y = x
⊢ y ∉ X
Tactic:
rwa [h]
Proof state after:
no goals
Theorem: SimpleGraph.Menger.meet_sub_X
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
X_sep_AB : Separates G A B X
ap bp : V
pa : ap ∈ A
pb : bp ∈ X
p : Walk G ap bp
hp : minimal { a := ap, b := bp, ha := pa, hb := pb, to_Walk := p }
aq bq : V
qa : aq ∈ B
qb : bq ∈ X
q : Walk G aq bq
hq : minimal { a := aq, b := bq, ha := qa, hb := qb, to_Walk := q }
x : V
hx₁ : x ∈ Walk.support p
hx₂ : x ∈ Walk.support q
x✝ : x ∉ X
p' : Walk G ap ↑{ val := x, property := (_ : x = x) }
hp1 : Walk.support p' <+: Walk.support p
right✝¹ : ∀ v ∈ Walk.init₀ p', ¬v = x
h1 : ∀ y ∈ Walk.support p', y ∉ X
q' : Walk G aq ↑{ val := x, property := (_ : x = x) }
hq1 : Walk.support q' <+: Walk.support q
right✝ : ∀ v ∈ Walk.init₀ q', ¬v = x
⊢ ∀ y ∈ Walk.support q', y ∉ X
Tactic:
intro y hy
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
X_sep_AB : Separates G A B X
ap bp : V
pa : ap ∈ A
pb : bp ∈ X
p : Walk G ap bp
hp : minimal { a := ap, b := bp, ha := pa, hb := pb, to_Walk := p }
aq bq : V
qa : aq ∈ B
qb : bq ∈ X
q : Walk G aq bq
hq : minimal { a := aq, b := bq, ha := qa, hb := qb, to_Walk := q }
x : V
hx₁ : x ∈ Walk.support p
hx₂ : x ∈ Walk.support q
x✝ : x ∉ X
p' : Walk G ap ↑{ val := x, property := (_ : x = x) }
hp1 : Walk.support p' <+: Walk.support p
right✝¹ : ∀ v ∈ Walk.init₀ p', ¬v = x
h1 : ∀ y ∈ Walk.support p', y ∉ X
q' : Walk G aq ↑{ val := x, property := (_ : x = x) }
hq1 : Walk.support q' <+: Walk.support q
right✝ : ∀ v ∈ Walk.init₀ q', ¬v = x
y : V
hy : y ∈ Walk.support q'
⊢ y ∉ X
Theorem: SimpleGraph.Menger.meet_sub_X
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
X_sep_AB : Separates G A B X
ap bp : V
pa : ap ∈ A
pb : bp ∈ X
p : Walk G ap bp
hp : minimal { a := ap, b := bp, ha := pa, hb := pb, to_Walk := p }
aq bq : V
qa : aq ∈ B
qb : bq ∈ X
q : Walk G aq bq
hq : minimal { a := aq, b := bq, ha := qa, hb := qb, to_Walk := q }
x : V
hx₁ : x ∈ Walk.support p
hx₂ : x ∈ Walk.support q
x✝ : x ∉ X
p' : Walk G ap ↑{ val := x, property := (_ : x = x) }
hp1 : Walk.support p' <+: Walk.support p
right✝¹ : ∀ v ∈ Walk.init₀ p', ¬v = x
h1 : ∀ y ∈ Walk.support p', y ∉ X
q' : Walk G aq ↑{ val := x, property := (_ : x = x) }
hq1 : Walk.support q' <+: Walk.support q
right✝ : ∀ v ∈ Walk.init₀ q', ¬v = x
y : V
hy : y ∈ Walk.support q'
⊢ y ∉ X
Tactic:
simp [Walk.support_eq_init₀_union_last] at hy
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
X_sep_AB : Separates G A B X
ap bp : V
pa : ap ∈ A
pb : bp ∈ X
p : Walk G ap bp
hp : minimal { a := ap, b := bp, ha := pa, hb := pb, to_Walk := p }
aq bq : V
qa : aq ∈ B
qb : bq ∈ X
q : Walk G aq bq
hq : minimal { a := aq, b := bq, ha := qa, hb := qb, to_Walk := q }
x : V
hx₁ : x ∈ Walk.support p
hx₂ : x ∈ Walk.support q
x✝ : x ∉ X
p' : Walk G ap ↑{ val := x, property := (_ : x = x) }
hp1 : Walk.support p' <+: Walk.support p
right✝¹ : ∀ v ∈ Walk.init₀ p', ¬v = x
h1 : ∀ y ∈ Walk.support p', y ∉ X
q' : Walk G aq ↑{ val := x, property := (_ : x = x) }
hq1 : Walk.support q' <+: Walk.support q
right✝ : ∀ v ∈ Walk.init₀ q', ¬v = x
y : V
hy : y ∈ Walk.init₀ q' ∨ y = x
⊢ y ∉ X
Theorem: SimpleGraph.Menger.meet_sub_X
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
X_sep_AB : Separates G A B X
ap bp : V
pa : ap ∈ A
pb : bp ∈ X
p : Walk G ap bp
hp : minimal { a := ap, b := bp, ha := pa, hb := pb, to_Walk := p }
aq bq : V
qa : aq ∈ B
qb : bq ∈ X
q : Walk G aq bq
hq : minimal { a := aq, b := bq, ha := qa, hb := qb, to_Walk := q }
x : V
hx₁ : x ∈ Walk.support p
hx₂ : x ∈ Walk.support q
x✝ : x ∉ X
p' : Walk G ap ↑{ val := x, property := (_ : x = x) }
hp1 : Walk.support p' <+: Walk.support p
right✝¹ : ∀ v ∈ Walk.init₀ p', ¬v = x
h1 : ∀ y ∈ Walk.support p', y ∉ X
q' : Walk G aq ↑{ val := x, property := (_ : x = x) }
hq1 : Walk.support q' <+: Walk.support q
right✝ : ∀ v ∈ Walk.init₀ q', ¬v = x
y : V
hy : y ∈ Walk.init₀ q' ∨ y = x
⊢ y ∉ X
Tactic:
cases hy with
| inl h => exact hq.1 y <| Walk.init₀_subset_of_support_prefix hq1 h
| inr h => rwa [h]
Proof state after:
no goals
Theorem: SimpleGraph.Menger.meet_sub_X
Proof state before:
case inl
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
X_sep_AB : Separates G A B X
ap bp : V
pa : ap ∈ A
pb : bp ∈ X
p : Walk G ap bp
hp : minimal { a := ap, b := bp, ha := pa, hb := pb, to_Walk := p }
aq bq : V
qa : aq ∈ B
qb : bq ∈ X
q : Walk G aq bq
hq : minimal { a := aq, b := bq, ha := qa, hb := qb, to_Walk := q }
x : V
hx₁ : x ∈ Walk.support p
hx₂ : x ∈ Walk.support q
x✝ : x ∉ X
p' : Walk G ap ↑{ val := x, property := (_ : x = x) }
hp1 : Walk.support p' <+: Walk.support p
right✝¹ : ∀ v ∈ Walk.init₀ p', ¬v = x
h1 : ∀ y ∈ Walk.support p', y ∉ X
q' : Walk G aq ↑{ val := x, property := (_ : x = x) }
hq1 : Walk.support q' <+: Walk.support q
right✝ : ∀ v ∈ Walk.init₀ q', ¬v = x
y : V
h : y ∈ Walk.init₀ q'
⊢ y ∉ X
Tactic:
exact hq.1 y <| Walk.init₀_subset_of_support_prefix hq1 h
Proof state after:
no goals
Theorem: SimpleGraph.Menger.meet_sub_X
Proof state before:
case inr
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
X_sep_AB : Separates G A B X
ap bp : V
pa : ap ∈ A
pb : bp ∈ X
p : Walk G ap bp
hp : minimal { a := ap, b := bp, ha := pa, hb := pb, to_Walk := p }
aq bq : V
qa : aq ∈ B
qb : bq ∈ X
q : Walk G aq bq
hq : minimal { a := aq, b := bq, ha := qa, hb := qb, to_Walk := q }
x : V
hx₁ : x ∈ Walk.support p
hx₂ : x ∈ Walk.support q
x✝ : x ∉ X
p' : Walk G ap ↑{ val := x, property := (_ : x = x) }
hp1 : Walk.support p' <+: Walk.support p
right✝¹ : ∀ v ∈ Walk.init₀ p', ¬v = x
h1 : ∀ y ∈ Walk.support p', y ∉ X
q' : Walk G aq ↑{ val := x, property := (_ : x = x) }
hq1 : Walk.support q' <+: Walk.support q
right✝ : ∀ v ∈ Walk.init₀ q', ¬v = x
y : V
h : y = x
⊢ y ∉ X
Tactic:
rwa [h]
Proof state after:
no goals
Theorem: SimpleGraph.Menger.meet_sub_X
Proof state before:
case mk.mk.mk.mk.mk.intro.mk.mk.mk.intro.inl
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
X_sep_AB : Separates G A B X
ap bp : V
pa : ap ∈ A
pb : bp ∈ X
p : Walk G ap bp
hp : minimal { a := ap, b := bp, ha := pa, hb := pb, to_Walk := p }
aq bq : V
qa : aq ∈ B
qb : bq ∈ X
q : Walk G aq bq
hq : minimal { a := aq, b := bq, ha := qa, hb := qb, to_Walk := q }
x : V
hx₁ : x ∈ Walk.support p
hx₂ : x ∈ Walk.support q
x✝ : x ∉ X
p' : Walk G ap ↑{ val := x, property := (_ : x = x) }
hp1 : Walk.support p' <+: Walk.support p
right✝¹ : ∀ v ∈ Walk.init₀ p', ¬v = x
h1 : ∀ y ∈ Walk.support p', y ∉ X
q' : Walk G aq ↑{ val := x, property := (_ : x = x) }
hq1 : Walk.support q' <+: Walk.support q
right✝ : ∀ v ∈ Walk.init₀ q', ¬v = x
h2 : ∀ y ∈ Walk.support q', y ∉ X
z : V
hz : z ∈ X
h : z ∈ Walk.support p'
⊢ False
Tactic:
cases h1 _ h hz
Proof state after:
no goals
Theorem: SimpleGraph.Menger.meet_sub_X
Proof state before:
case mk.mk.mk.mk.mk.intro.mk.mk.mk.intro.inr
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
X_sep_AB : Separates G A B X
ap bp : V
pa : ap ∈ A
pb : bp ∈ X
p : Walk G ap bp
hp : minimal { a := ap, b := bp, ha := pa, hb := pb, to_Walk := p }
aq bq : V
qa : aq ∈ B
qb : bq ∈ X
q : Walk G aq bq
hq : minimal { a := aq, b := bq, ha := qa, hb := qb, to_Walk := q }
x : V
hx₁ : x ∈ Walk.support p
hx₂ : x ∈ Walk.support q
x✝ : x ∉ X
p' : Walk G ap ↑{ val := x, property := (_ : x = x) }
hp1 : Walk.support p' <+: Walk.support p
right✝¹ : ∀ v ∈ Walk.init₀ p', ¬v = x
h1 : ∀ y ∈ Walk.support p', y ∉ X
q' : Walk G aq ↑{ val := x, property := (_ : x = x) }
hq1 : Walk.support q' <+: Walk.support q
right✝ : ∀ v ∈ Walk.init₀ q', ¬v = x
h2 : ∀ y ∈ Walk.support q', y ∉ X
z : V
hz : z ∈ X
h : z ∈ Walk.support q'
⊢ False
Tactic:
cases h2 _ h hz
Proof state after:
no goals
Theorem: SimpleGraph.Menger.sep_of_sep_in_merge
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
Y_sep : Separates (G /ₑ e) (image (merge_edge e) A) (image (merge_edge e) B) Y
⊢ Separates G A B (Y ∪ {e.toProd.2})
Tactic:
rintro γ
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
e : Dart G
Y_sep : Separates (G /ₑ e) (image (merge_edge e) A) (image (merge_edge e) B) Y
γ : AB_Walk G A B
⊢ ∃ x ∈ Y ∪ {e.toProd.2}, x ∈ Walk.support γ.to_Walk
Theorem: SimpleGraph.Menger.sep_of_sep_in_merge
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
Y_sep : Separates (G /ₑ e) (image (merge_edge e) A) (image (merge_edge e) B) Y
γ : AB_Walk G A B
⊢ ∃ x ∈ Y ∪ {e.toProd.2}, x ∈ Walk.support γ.to_Walk
Tactic:
obtain ⟨z, hz1, hz2⟩ := Y_sep (γ.push (merge_edge e))
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
e : Dart G
Y_sep : Separates (G /ₑ e) (image (merge_edge e) A) (image (merge_edge e) B) Y
γ : AB_Walk G A B
z : V
hz1 : z ∈ Y
hz2 : z ∈ Walk.support (push (merge_edge e) γ).to_Walk
⊢ ∃ x ∈ Y ∪ {e.toProd.2}, x ∈ Walk.support γ.to_Walk
Theorem: SimpleGraph.Menger.sep_of_sep_in_merge
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
e : Dart G
Y_sep : Separates (G /ₑ e) (image (merge_edge e) A) (image (merge_edge e) B) Y
γ : AB_Walk G A B
z : V
hz1 : z ∈ Y
hz2 : z ∈ Walk.support (push (merge_edge e) γ).to_Walk
⊢ ∃ x ∈ Y ∪ {e.toProd.2}, x ∈ Walk.support γ.to_Walk
Tactic:
simp [mem_inter, push] at hz2
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
e : Dart G
Y_sep : Separates (G /ₑ e) (image (merge_edge e) A) (image (merge_edge e) B) Y
γ : AB_Walk G A B
z : V
hz1 : z ∈ Y
hz2 : z ∈ Walk.support (push_Walk (merge_edge e) γ.to_Walk)
⊢ ∃ x ∈ Y ∪ {e.toProd.2}, x ∈ Walk.support γ.to_Walk
Theorem: SimpleGraph.Menger.sep_of_sep_in_merge
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
e : Dart G
Y_sep : Separates (G /ₑ e) (image (merge_edge e) A) (image (merge_edge e) B) Y
γ : AB_Walk G A B
z : V
hz1 : z ∈ Y
hz2 : z ∈ Walk.support (push_Walk (merge_edge e) γ.to_Walk)
⊢ ∃ x ∈ Y ∪ {e.toProd.2}, x ∈ Walk.support γ.to_Walk
Tactic:
have := support_push_Walk hz2
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
e : Dart G
Y_sep : Separates (G /ₑ e) (image (merge_edge e) A) (image (merge_edge e) B) Y
γ : AB_Walk G A B
z : V
hz1 : z ∈ Y
hz2 : z ∈ Walk.support (push_Walk (merge_edge e) γ.to_Walk)
this : z ∈ List.map (merge_edge e) (Walk.support γ.to_Walk)
⊢ ∃ x ∈ Y ∪ {e.toProd.2}, x ∈ Walk.support γ.to_Walk
Theorem: SimpleGraph.Menger.sep_of_sep_in_merge
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
e : Dart G
Y_sep : Separates (G /ₑ e) (image (merge_edge e) A) (image (merge_edge e) B) Y
γ : AB_Walk G A B
z : V
hz1 : z ∈ Y
hz2 : z ∈ Walk.support (push_Walk (merge_edge e) γ.to_Walk)
this : z ∈ List.map (merge_edge e) (Walk.support γ.to_Walk)
⊢ ∃ x ∈ Y ∪ {e.toProd.2}, x ∈ Walk.support γ.to_Walk
Tactic:
simp at this
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
e : Dart G
Y_sep : Separates (G /ₑ e) (image (merge_edge e) A) (image (merge_edge e) B) Y
γ : AB_Walk G A B
z : V
hz1 : z ∈ Y
hz2 : z ∈ Walk.support (push_Walk (merge_edge e) γ.to_Walk)
this : ∃ a ∈ Walk.support γ.to_Walk, merge_edge e a = z
⊢ ∃ x ∈ Y ∪ {e.toProd.2}, x ∈ Walk.support γ.to_Walk
Theorem: SimpleGraph.Menger.sep_of_sep_in_merge
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
e : Dart G
Y_sep : Separates (G /ₑ e) (image (merge_edge e) A) (image (merge_edge e) B) Y
γ : AB_Walk G A B
z : V
hz1 : z ∈ Y
hz2 : z ∈ Walk.support (push_Walk (merge_edge e) γ.to_Walk)
this : ∃ a ∈ Walk.support γ.to_Walk, merge_edge e a = z
⊢ ∃ x ∈ Y ∪ {e.toProd.2}, x ∈ Walk.support γ.to_Walk
Tactic:
obtain ⟨x, hx₁, hx₂⟩ := this
Proof state after:
case intro.intro.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
Y_sep : Separates (G /ₑ e) (image (merge_edge e) A) (image (merge_edge e) B) Y
γ : AB_Walk G A B
z : V
hz1 : z ∈ Y
hz2 : z ∈ Walk.support (push_Walk (merge_edge e) γ.to_Walk)
x : V
hx₁ : x ∈ Walk.support γ.to_Walk
hx₂ : merge_edge e x = z
⊢ ∃ x ∈ Y ∪ {e.toProd.2}, x ∈ Walk.support γ.to_Walk
Theorem: SimpleGraph.Menger.sep_of_sep_in_merge
Proof state before:
case intro.intro.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
Y_sep : Separates (G /ₑ e) (image (merge_edge e) A) (image (merge_edge e) B) Y
γ : AB_Walk G A B
z : V
hz1 : z ∈ Y
hz2 : z ∈ Walk.support (push_Walk (merge_edge e) γ.to_Walk)
x : V
hx₁ : x ∈ Walk.support γ.to_Walk
hx₂ : merge_edge e x = z
⊢ ∃ x ∈ Y ∪ {e.toProd.2}, x ∈ Walk.support γ.to_Walk
Tactic:
use x
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
Y_sep : Separates (G /ₑ e) (image (merge_edge e) A) (image (merge_edge e) B) Y
γ : AB_Walk G A B
z : V
hz1 : z ∈ Y
hz2 : z ∈ Walk.support (push_Walk (merge_edge e) γ.to_Walk)
x : V
hx₁ : x ∈ Walk.support γ.to_Walk
hx₂ : merge_edge e x = z
⊢ x ∈ Y ∪ {e.toProd.2} ∧ x ∈ Walk.support γ.to_Walk
Theorem: SimpleGraph.Menger.sep_of_sep_in_merge
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
Y_sep : Separates (G /ₑ e) (image (merge_edge e) A) (image (merge_edge e) B) Y
γ : AB_Walk G A B
z : V
hz1 : z ∈ Y
hz2 : z ∈ Walk.support (push_Walk (merge_edge e) γ.to_Walk)
x : V
hx₁ : x ∈ Walk.support γ.to_Walk
hx₂ : merge_edge e x = z
⊢ x ∈ Y ∪ {e.toProd.2} ∧ x ∈ Walk.support γ.to_Walk
Tactic:
by_cases h : x = e.snd <;> simp [merge_edge, update, h] at hx₂ <;> subst_vars <;> simp [hx₁, hz1]
Proof state after:
no goals
Theorem: SimpleGraph.Menger.step_1
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
h_contract : isMenger (G /ₑ e)
too_small : ∀ (P : Finset (AB_Walk G A B)), pwd P → card P < min_cut G A B
⊢ ∃ X, e.toProd.1 ∈ X ∧ e.toProd.2 ∈ X ∧ Separates G A B X ∧ card X = min_cut G A B
Tactic:
let A₁ := image (merge_edge e) A
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
e : Dart G
h_contract : isMenger (G /ₑ e)
too_small : ∀ (P : Finset (AB_Walk G A B)), pwd P → card P < min_cut G A B
A₁ : Finset V := image (merge_edge e) A
⊢ ∃ X, e.toProd.1 ∈ X ∧ e.toProd.2 ∈ X ∧ Separates G A B X ∧ card X = min_cut G A B
Theorem: SimpleGraph.Menger.step_1
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
h_contract : isMenger (G /ₑ e)
too_small : ∀ (P : Finset (AB_Walk G A B)), pwd P → card P < min_cut G A B
A₁ : Finset V := image (merge_edge e) A
⊢ ∃ X, e.toProd.1 ∈ X ∧ e.toProd.2 ∈ X ∧ Separates G A B X ∧ card X = min_cut G A B
Tactic:
let B₁ := image (merge_edge e) B
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
e : Dart G
h_contract : isMenger (G /ₑ e)
too_small : ∀ (P : Finset (AB_Walk G A B)), pwd P → card P < min_cut G A B
A₁ : Finset V := image (merge_edge e) A
B₁ : Finset V := image (merge_edge e) B
⊢ ∃ X, e.toProd.1 ∈ X ∧ e.toProd.2 ∈ X ∧ Separates G A B X ∧ card X = min_cut G A B
Theorem: SimpleGraph.Menger.step_1
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
h_contract : isMenger (G /ₑ e)
too_small : ∀ (P : Finset (AB_Walk G A B)), pwd P → card P < min_cut G A B
A₁ : Finset V := image (merge_edge e) A
B₁ : Finset V := image (merge_edge e) B
⊢ ∃ X, e.toProd.1 ∈ X ∧ e.toProd.2 ∈ X ∧ Separates G A B X ∧ card X = min_cut G A B
Tactic:
obtain ⟨Y, Y_eq_min₁⟩ := min_cut.set (G /ₑ e) A₁ B₁
Proof state after:
case 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
h_contract : isMenger (G /ₑ e)
too_small : ∀ (P : Finset (AB_Walk G A B)), pwd P → card P < min_cut G A B
A₁ : Finset V := image (merge_edge e) A
B₁ : Finset V := image (merge_edge e) B
Y : Separator (G /ₑ e) A₁ B₁
Y_eq_min₁ : Separator.card Y = min_cut (G /ₑ e) A₁ B₁
⊢ ∃ X, e.toProd.1 ∈ X ∧ e.toProd.2 ∈ X ∧ Separates G A B X ∧ card X = min_cut G A B
Theorem: SimpleGraph.Menger.step_1
Proof state before:
case 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
h_contract : isMenger (G /ₑ e)
too_small : ∀ (P : Finset (AB_Walk G A B)), pwd P → card P < min_cut G A B
A₁ : Finset V := image (merge_edge e) A
B₁ : Finset V := image (merge_edge e) B
Y : Separator (G /ₑ e) A₁ B₁
Y_eq_min₁ : Separator.card Y = min_cut (G /ₑ e) A₁ B₁
⊢ ∃ X, e.toProd.1 ∈ X ∧ e.toProd.2 ∈ X ∧ Separates G A B X ∧ card X = min_cut G A B
Tactic:
let X := Y.val ∪ {e.snd}
Proof state after:
case 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
h_contract : isMenger (G /ₑ e)
too_small : ∀ (P : Finset (AB_Walk G A B)), pwd P → card P < min_cut G A B
A₁ : Finset V := image (merge_edge e) A
B₁ : Finset V := image (merge_edge e) B
Y : Separator (G /ₑ e) A₁ B₁
Y_eq_min₁ : Separator.card Y = min_cut (G /ₑ e) A₁ B₁
X : Finset V := ↑Y ∪ {e.toProd.2}
⊢ ∃ X, e.toProd.1 ∈ X ∧ e.toProd.2 ∈ X ∧ Separates G A B X ∧ card X = min_cut G A B