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

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

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

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

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

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

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