internlm/Lean-Github huggingface dataset:
Theorem: SimpleGraph.Menger.massage_disjoint
Proof state before:
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₂
Tactic:
suffices γ₁ = γ₂ by simpa using this
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₂ }
⊢ γ₁ = γ₂
Theorem: SimpleGraph.Menger.massage_disjoint
Proof state before:
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₂ }
⊢ γ₁ = γ₂
Tactic:
exact massage_eq h h₁ ⟨z, hz₁, hz₂⟩
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
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₂ }
this : γ₁ = γ₂
⊢ q₁ = q₂
Tactic:
simpa using this
Proof state after:
no goals
Theorem: SimpleGraph.Menger.massage_card
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)
hP : pwd P
⊢ card (image (massage h) P) = card P
Tactic:
apply Finset.card_image_of_injOn
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
h : G₂ ≤ G₁
P : Finset (AB_Walk G₂ A B)
hP : pwd P
⊢ Set.InjOn (massage h) ↑P
Theorem: SimpleGraph.Menger.massage_card
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
h : G₂ ≤ G₁
P : Finset (AB_Walk G₂ A B)
hP : pwd P
⊢ Set.InjOn (massage h) ↑P
Tactic:
rintro p₁ hp₁ p₂ hp₂ he
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
h : G₂ ≤ G₁
P : Finset (AB_Walk G₂ A B)
hP : pwd P
p₁ : AB_Walk G₂ A B
hp₁ : p₁ ∈ ↑P
p₂ : AB_Walk G₂ A B
hp₂ : p₂ ∈ ↑P
he : massage h p₁ = massage h p₂
⊢ p₁ = p₂
Theorem: SimpleGraph.Menger.massage_card
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
h : G₂ ≤ G₁
P : Finset (AB_Walk G₂ A B)
hP : pwd P
p₁ : AB_Walk G₂ A B
hp₁ : p₁ ∈ ↑P
p₂ : AB_Walk G₂ A B
hp₂ : p₂ ∈ ↑P
he : massage h p₁ = massage h p₂
⊢ p₁ = p₂
Tactic:
let q₁ : P := ⟨p₁, hp₁⟩
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
h : G₂ ≤ G₁
P : Finset (AB_Walk G₂ A B)
hP : pwd P
p₁ : AB_Walk G₂ A B
hp₁ : p₁ ∈ ↑P
p₂ : AB_Walk G₂ A B
hp₂ : p₂ ∈ ↑P
he : massage h p₁ = massage h p₂
q₁ : { x // x ∈ P } := { val := p₁, property := hp₁ }
⊢ p₁ = p₂
Theorem: SimpleGraph.Menger.massage_card
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
h : G₂ ≤ G₁
P : Finset (AB_Walk G₂ A B)
hP : pwd P
p₁ : AB_Walk G₂ A B
hp₁ : p₁ ∈ ↑P
p₂ : AB_Walk G₂ A B
hp₂ : p₂ ∈ ↑P
he : massage h p₁ = massage h p₂
q₁ : { x // x ∈ P } := { val := p₁, property := hp₁ }
⊢ p₁ = p₂
Tactic:
let q₂ : P := ⟨p₂, hp₂⟩
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
h : G₂ ≤ G₁
P : Finset (AB_Walk G₂ A B)
hP : pwd P
p₁ : AB_Walk G₂ A B
hp₁ : p₁ ∈ ↑P
p₂ : AB_Walk G₂ A B
hp₂ : p₂ ∈ ↑P
he : massage h p₁ = massage h p₂
q₁ : { x // x ∈ P } := { val := p₁, property := hp₁ }
q₂ : { x // x ∈ P } := { val := p₂, property := hp₂ }
⊢ p₁ = p₂
Theorem: SimpleGraph.Menger.massage_card
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
h : G₂ ≤ G₁
P : Finset (AB_Walk G₂ A B)
hP : pwd P
p₁ : AB_Walk G₂ A B
hp₁ : p₁ ∈ ↑P
p₂ : AB_Walk G₂ A B
hp₂ : p₂ ∈ ↑P
he : massage h p₁ = massage h p₂
q₁ : { x // x ∈ P } := { val := p₁, property := hp₁ }
q₂ : { x // x ∈ P } := { val := p₂, property := hp₂ }
⊢ p₁ = p₂
Tactic:
suffices q₁ = q₂ by simpa using this
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
h : G₂ ≤ G₁
P : Finset (AB_Walk G₂ A B)
hP : pwd P
p₁ : AB_Walk G₂ A B
hp₁ : p₁ ∈ ↑P
p₂ : AB_Walk G₂ A B
hp₂ : p₂ ∈ ↑P
he : massage h p₁ = massage h p₂
q₁ : { x // x ∈ P } := { val := p₁, property := hp₁ }
q₂ : { x // x ∈ P } := { val := p₂, property := hp₂ }
⊢ q₁ = q₂
Theorem: SimpleGraph.Menger.massage_card
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
h : G₂ ≤ G₁
P : Finset (AB_Walk G₂ A B)
hP : pwd P
p₁ : AB_Walk G₂ A B
hp₁ : p₁ ∈ ↑P
p₂ : AB_Walk G₂ A B
hp₂ : p₂ ∈ ↑P
he : massage h p₁ = massage h p₂
q₁ : { x // x ∈ P } := { val := p₁, property := hp₁ }
q₂ : { x // x ∈ P } := { val := p₂, property := hp₂ }
⊢ q₁ = q₂
Tactic:
apply massage_eq h hP
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
h : G₂ ≤ G₁
P : Finset (AB_Walk G₂ A B)
hP : pwd P
p₁ : AB_Walk G₂ A B
hp₁ : p₁ ∈ ↑P
p₂ : AB_Walk G₂ A B
hp₂ : p₂ ∈ ↑P
he : massage h p₁ = massage h p₂
q₁ : { x // x ∈ P } := { val := p₁, property := hp₁ }
q₂ : { x // x ∈ P } := { val := p₂, property := hp₂ }
⊢ ∃ z ∈ Walk.support (massage h ↑q₁).to_Walk, z ∈ Walk.support (massage h ↑q₂).to_Walk
Theorem: SimpleGraph.Menger.massage_card
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
h : G₂ ≤ G₁
P : Finset (AB_Walk G₂ A B)
hP : pwd P
p₁ : AB_Walk G₂ A B
hp₁ : p₁ ∈ ↑P
p₂ : AB_Walk G₂ A B
hp₂ : p₂ ∈ ↑P
he : massage h p₁ = massage h p₂
q₁ : { x // x ∈ P } := { val := p₁, property := hp₁ }
q₂ : { x // x ∈ P } := { val := p₂, property := hp₂ }
⊢ ∃ z ∈ Walk.support (massage h ↑q₁).to_Walk, z ∈ Walk.support (massage h ↑q₂).to_Walk
Tactic:
use (massage h p₂).a
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
h : G₂ ≤ G₁
P : Finset (AB_Walk G₂ A B)
hP : pwd P
p₁ : AB_Walk G₂ A B
hp₁ : p₁ ∈ ↑P
p₂ : AB_Walk G₂ A B
hp₂ : p₂ ∈ ↑P
he : massage h p₁ = massage h p₂
q₁ : { x // x ∈ P } := { val := p₁, property := hp₁ }
q₂ : { x // x ∈ P } := { val := p₂, property := hp₂ }
⊢ (massage h p₂).a ∈ Walk.support (massage h ↑q₁).to_Walk ∧ (massage h p₂).a ∈ Walk.support (massage h ↑q₂).to_Walk
Theorem: SimpleGraph.Menger.massage_card
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
h : G₂ ≤ G₁
P : Finset (AB_Walk G₂ A B)
hP : pwd P
p₁ : AB_Walk G₂ A B
hp₁ : p₁ ∈ ↑P
p₂ : AB_Walk G₂ A B
hp₂ : p₂ ∈ ↑P
he : massage h p₁ = massage h p₂
q₁ : { x // x ∈ P } := { val := p₁, property := hp₁ }
q₂ : { x // x ∈ P } := { val := p₂, property := hp₂ }
⊢ (massage h p₂).a ∈ Walk.support (massage h ↑q₁).to_Walk ∧ (massage h p₂).a ∈ Walk.support (massage h ↑q₂).to_Walk
Tactic:
rw [he]
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
h : G₂ ≤ G₁
P : Finset (AB_Walk G₂ A B)
hP : pwd P
p₁ : AB_Walk G₂ A B
hp₁ : p₁ ∈ ↑P
p₂ : AB_Walk G₂ A B
hp₂ : p₂ ∈ ↑P
he : massage h p₁ = massage h p₂
q₁ : { x // x ∈ P } := { val := p₁, property := hp₁ }
q₂ : { x // x ∈ P } := { val := p₂, property := hp₂ }
⊢ (massage h p₂).a ∈ Walk.support (massage h p₂).to_Walk ∧ (massage h p₂).a ∈ Walk.support (massage h ↑q₂).to_Walk
Theorem: SimpleGraph.Menger.massage_card
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
h : G₂ ≤ G₁
P : Finset (AB_Walk G₂ A B)
hP : pwd P
p₁ : AB_Walk G₂ A B
hp₁ : p₁ ∈ ↑P
p₂ : AB_Walk G₂ A B
hp₂ : p₂ ∈ ↑P
he : massage h p₁ = massage h p₂
q₁ : { x // x ∈ P } := { val := p₁, property := hp₁ }
q₂ : { x // x ∈ P } := { val := p₂, property := hp₂ }
⊢ (massage h p₂).a ∈ Walk.support (massage h p₂).to_Walk ∧ (massage h p₂).a ∈ Walk.support (massage h ↑q₂).to_Walk
Tactic:
simp
Proof state after:
no goals
Theorem: SimpleGraph.Menger.massage_card
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)
hP : pwd P
p₁ : AB_Walk G₂ A B
hp₁ : p₁ ∈ ↑P
p₂ : AB_Walk G₂ A B
hp₂ : p₂ ∈ ↑P
he : massage h p₁ = massage h p₂
q₁ : { x // x ∈ P } := { val := p₁, property := hp₁ }
q₂ : { x // x ∈ P } := { val := p₂, property := hp₂ }
this : q₁ = q₂
⊢ p₁ = p₂
Tactic:
simpa using this
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
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
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
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
Theorem: SimpleGraph.Menger.meet_sub_X
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
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
Proof 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
Theorem: SimpleGraph.Menger.meet_sub_X
Proof 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₂
Proof 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
Theorem: SimpleGraph.Menger.meet_sub_X
Proof 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₂
Proof 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
Theorem: SimpleGraph.Menger.meet_sub_X
Proof 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
Proof 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
Theorem: SimpleGraph.Menger.meet_sub_X
Proof 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]
Proof 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
Theorem: SimpleGraph.Menger.meet_sub_X
Proof 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]
Proof 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
Theorem: SimpleGraph.Menger.meet_sub_X
Proof 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⟩
Proof 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
Theorem: SimpleGraph.Menger.meet_sub_X
Proof 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'
Proof 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
Theorem: SimpleGraph.Menger.meet_sub_X
Proof 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
Proof state after:
no goals