Theorem: SimpleGraph.Menger.massage_disjoint (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
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₂
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

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

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

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

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

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₁⟩
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₂

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

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

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
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₂ }
⊢ γ₁ = γ₂

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