Theorem: SimpleGraph.Menger.meet_sub_X (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
X_sep_AB : Separates G A B X
p : AB_Walk G A X
q : AB_Walk G B X
hp : minimal p
hq : minimal q
⊢ ∀ x ∈ Walk.support p.to_Walk, x ∈ Walk.support q.to_Walk → x ∈ X
Tactic:
obtain ⟨ap, bp, pa, pb, p⟩ := p
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
X_sep_AB : Separates G A B X
q : AB_Walk G B X
hq : minimal q
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 }
⊢ ∀ x ∈ Walk.support { a := ap, b := bp, ha := pa, hb := pb, to_Walk := p }.to_Walk, x ∈ Walk.support q.to_Walk → x ∈ X

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
X_sep_AB : Separates G A B X
q : AB_Walk G B X
hq : minimal q
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 }
⊢ ∀ x ∈ Walk.support { a := ap, b := bp, ha := pa, hb := pb, to_Walk := p }.to_Walk, x ∈ Walk.support q.to_Walk → x ∈ X
Tactic:
obtain ⟨aq, bq, qa, qb, q⟩ := q
State after:
case mk.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
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 ∈ Walk.support { a := ap, b := bp, ha := pa, hb := pb, to_Walk := p }.to_Walk,
    x ∈ Walk.support { a := aq, b := bq, ha := qa, hb := qb, to_Walk := q }.to_Walk → x ∈ X

State before:
case mk.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
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 ∈ Walk.support { a := ap, b := bp, ha := pa, hb := pb, to_Walk := p }.to_Walk,
    x ∈ Walk.support { a := aq, b := bq, ha := qa, hb := qb, to_Walk := q }.to_Walk → x ∈ X
Tactic:
intro x hx₁ hx₂
State after:
case mk.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
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 { a := ap, b := bp, ha := pa, hb := pb, to_Walk := p }.to_Walk
hx₂ : x ∈ Walk.support { a := aq, b := bq, ha := qa, hb := qb, to_Walk := q }.to_Walk
⊢ x ∈ X

State before:
case mk.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
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 { a := ap, b := bp, ha := pa, hb := pb, to_Walk := p }.to_Walk
hx₂ : x ∈ Walk.support { a := aq, b := bq, ha := qa, hb := qb, to_Walk := q }.to_Walk
⊢ x ∈ X
Tactic:
dsimp at hx₁ hx₂
State after:
case mk.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
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

State before:
case mk.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
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
Tactic:
by_contra
State after:
case mk.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
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
⊢ False

State before:
case mk.mk.mk.mk.mk.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
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
⊢ False
Tactic:
have h1 : ∀ y ∈ p'.support, y ∉ X := by
  intro y hy
  simp [Walk.support_eq_init₀_union_last] at hy
  cases hy with
  | inl h => exact hp.1 y <| Walk.init₀_subset_of_support_prefix hp1 h
  | inr h => rwa [h]
State after:
case mk.mk.mk.mk.mk.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
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
⊢ False

State before:
case mk.mk.mk.mk.mk.intro.mk.mk.mk.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
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
⊢ False
Tactic:
have h2 : ∀ y ∈ q'.support, y ∉ X := by
  intro y hy
  simp [Walk.support_eq_init₀_union_last] at hy
  cases hy with
  | inl h => exact hq.1 y <| Walk.init₀_subset_of_support_prefix hq1 h
  | inr h => rwa [h]
State after:
case mk.mk.mk.mk.mk.intro.mk.mk.mk.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
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
⊢ False

State before:
case mk.mk.mk.mk.mk.intro.mk.mk.mk.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
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
⊢ False
Tactic:
choose z hz hz' using X_sep_AB ⟨_, _, pa, qa, p'.append q'.reverse⟩
State after:
case mk.mk.mk.mk.mk.intro.mk.mk.mk.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
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
hz' : z ∈ Walk.support { a := ap, b := aq, ha := pa, hb := qa, to_Walk := Walk.append p' (Walk.reverse q') }.to_Walk
⊢ False

State before:
case mk.mk.mk.mk.mk.intro.mk.mk.mk.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
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
hz' : z ∈ Walk.support { a := ap, b := aq, ha := pa, hb := qa, to_Walk := Walk.append p' (Walk.reverse q') }.to_Walk
⊢ False
Tactic:
simp at hz'
State after:
case mk.mk.mk.mk.mk.intro.mk.mk.mk.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
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
hz' : z ∈ Walk.support p' ∨ z ∈ Walk.support q'
⊢ False

State before:
case mk.mk.mk.mk.mk.intro.mk.mk.mk.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
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
hz' : z ∈ Walk.support p' ∨ z ∈ Walk.support q'
⊢ False
Tactic:
cases hz' with
| inl h => cases h1 _ h hz
| inr h => cases h2 _ h hz
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
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
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

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
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

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]
State after:
no goals

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
State after:
no goals

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]
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
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
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

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
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

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]
State after:
no goals

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
State after:
no goals

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]
State after:
no goals

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
State after:
no goals

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
State after:
no goals