Theorem: SimpleGraph.Menger.massage_card (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)
hP : pwd P
⊢ card (image (massage h) P) = card P
Tactic:
apply Finset.card_image_of_injOn
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

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

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

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

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

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

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

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

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