Theorem: SimpleGraph.Menger.le_B (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
P : Finset (AB_Walk G A B)
dis : pwd P
⊢ card P ≤ card B
Tactic:
let φ (p : P) : B := ⟨p.val.b, p.val.hb⟩
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
P : Finset (AB_Walk G A B)
dis : pwd P
φ : { x // x ∈ P } → { x // x ∈ B } := fun p => { val := (↑p).b, property := (_ : (↑p).b ∈ B) }
⊢ card P ≤ card B

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
P : Finset (AB_Walk G A B)
dis : pwd P
φ : { x // x ∈ P } → { x // x ∈ B } := fun p => { val := (↑p).b, property := (_ : (↑p).b ∈ B) }
⊢ card P ≤ card B
Tactic:
have : Injective φ := by
  rintro p₁ p₂ h
  by_contra h'
  have h'' : p₁.val ≠ p₂.val := by simpa [← Subtype.ext_iff]
  have h1 : p₁.val.b ∈ p₁.val.to_Walk.support := Walk.end_mem_support _
  have h2 : p₁.val.b ∈ p₂.val.to_Walk.support := by
    simp at h ; rw [h]
    exact Walk.end_mem_support _
  exact dis p₁.prop p₂.prop h'' h1 h2
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
P : Finset (AB_Walk G A B)
dis : pwd P
φ : { x // x ∈ P } → { x // x ∈ B } := fun p => { val := (↑p).b, property := (_ : (↑p).b ∈ B) }
this : Injective φ
⊢ card P ≤ card B

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
P : Finset (AB_Walk G A B)
dis : pwd P
φ : { x // x ∈ P } → { x // x ∈ B } := fun p => { val := (↑p).b, property := (_ : (↑p).b ∈ B) }
this : Injective φ
⊢ card P ≤ card B
Tactic:
simp_rw [← Fintype.card_coe]
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
P : Finset (AB_Walk G A B)
dis : pwd P
φ : { x // x ∈ P } → { x // x ∈ B } := fun p => { val := (↑p).b, property := (_ : (↑p).b ∈ B) }
this : Injective φ
⊢ Fintype.card { x // x ∈ P } ≤ Fintype.card { x // x ∈ B }

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
P : Finset (AB_Walk G A B)
dis : pwd P
φ : { x // x ∈ P } → { x // x ∈ B } := fun p => { val := (↑p).b, property := (_ : (↑p).b ∈ B) }
this : Injective φ
⊢ Fintype.card { x // x ∈ P } ≤ Fintype.card { x // x ∈ B }
Tactic:
exact Fintype.card_le_of_injective φ this
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
P : Finset (AB_Walk G A B)
dis : pwd P
φ : { x // x ∈ P } → { x // x ∈ B } := fun p => { val := (↑p).b, property := (_ : (↑p).b ∈ B) }
⊢ Injective φ
Tactic:
rintro p₁ p₂ h
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
P : Finset (AB_Walk G A B)
dis : pwd P
φ : { x // x ∈ P } → { x // x ∈ B } := fun p => { val := (↑p).b, property := (_ : (↑p).b ∈ B) }
p₁ p₂ : { x // x ∈ P }
h : φ 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
P : Finset (AB_Walk G A B)
dis : pwd P
φ : { x // x ∈ P } → { x // x ∈ B } := fun p => { val := (↑p).b, property := (_ : (↑p).b ∈ B) }
p₁ p₂ : { x // x ∈ P }
h : φ p₁ = φ p₂
⊢ p₁ = p₂
Tactic:
by_contra h'
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
P : Finset (AB_Walk G A B)
dis : pwd P
φ : { x // x ∈ P } → { x // x ∈ B } := fun p => { val := (↑p).b, property := (_ : (↑p).b ∈ B) }
p₁ p₂ : { x // x ∈ P }
h : φ p₁ = φ p₂
h' : ¬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
P : Finset (AB_Walk G A B)
dis : pwd P
φ : { x // x ∈ P } → { x // x ∈ B } := fun p => { val := (↑p).b, property := (_ : (↑p).b ∈ B) }
p₁ p₂ : { x // x ∈ P }
h : φ p₁ = φ p₂
h' : ¬p₁ = p₂
⊢ False
Tactic:
have h'' : p₁.val ≠ p₂.val := by simpa [← Subtype.ext_iff]
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
P : Finset (AB_Walk G A B)
dis : pwd P
φ : { x // x ∈ P } → { x // x ∈ B } := fun p => { val := (↑p).b, property := (_ : (↑p).b ∈ B) }
p₁ p₂ : { x // x ∈ P }
h : φ p₁ = φ p₂
h' : ¬p₁ = p₂
h'' : ↑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
P : Finset (AB_Walk G A B)
dis : pwd P
φ : { x // x ∈ P } → { x // x ∈ B } := fun p => { val := (↑p).b, property := (_ : (↑p).b ∈ B) }
p₁ p₂ : { x // x ∈ P }
h : φ p₁ = φ p₂
h' : ¬p₁ = p₂
h'' : ↑p₁ ≠ ↑p₂
⊢ False
Tactic:
have h1 : p₁.val.b ∈ p₁.val.to_Walk.support := Walk.end_mem_support _
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
P : Finset (AB_Walk G A B)
dis : pwd P
φ : { x // x ∈ P } → { x // x ∈ B } := fun p => { val := (↑p).b, property := (_ : (↑p).b ∈ B) }
p₁ p₂ : { x // x ∈ P }
h : φ p₁ = φ p₂
h' : ¬p₁ = p₂
h'' : ↑p₁ ≠ ↑p₂
h1 : (↑p₁).b ∈ 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
P : Finset (AB_Walk G A B)
dis : pwd P
φ : { x // x ∈ P } → { x // x ∈ B } := fun p => { val := (↑p).b, property := (_ : (↑p).b ∈ B) }
p₁ p₂ : { x // x ∈ P }
h : φ p₁ = φ p₂
h' : ¬p₁ = p₂
h'' : ↑p₁ ≠ ↑p₂
h1 : (↑p₁).b ∈ Walk.support (↑p₁).to_Walk
⊢ False
Tactic:
have h2 : p₁.val.b ∈ p₂.val.to_Walk.support := by
  simp at h ; rw [h]
  exact Walk.end_mem_support _
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
P : Finset (AB_Walk G A B)
dis : pwd P
φ : { x // x ∈ P } → { x // x ∈ B } := fun p => { val := (↑p).b, property := (_ : (↑p).b ∈ B) }
p₁ p₂ : { x // x ∈ P }
h : φ p₁ = φ p₂
h' : ¬p₁ = p₂
h'' : ↑p₁ ≠ ↑p₂
h1 : (↑p₁).b ∈ Walk.support (↑p₁).to_Walk
h2 : (↑p₁).b ∈ 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
P : Finset (AB_Walk G A B)
dis : pwd P
φ : { x // x ∈ P } → { x // x ∈ B } := fun p => { val := (↑p).b, property := (_ : (↑p).b ∈ B) }
p₁ p₂ : { x // x ∈ P }
h : φ p₁ = φ p₂
h' : ¬p₁ = p₂
h'' : ↑p₁ ≠ ↑p₂
h1 : (↑p₁).b ∈ Walk.support (↑p₁).to_Walk
h2 : (↑p₁).b ∈ Walk.support (↑p₂).to_Walk
⊢ False
Tactic:
exact dis p₁.prop p₂.prop h'' 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
P : Finset (AB_Walk G A B)
dis : pwd P
φ : { x // x ∈ P } → { x // x ∈ B } := fun p => { val := (↑p).b, property := (_ : (↑p).b ∈ B) }
p₁ p₂ : { x // x ∈ P }
h : φ p₁ = φ p₂
h' : ¬p₁ = p₂
⊢ ↑p₁ ≠ ↑p₂
Tactic:
simpa [← Subtype.ext_iff]
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
P : Finset (AB_Walk G A B)
dis : pwd P
φ : { x // x ∈ P } → { x // x ∈ B } := fun p => { val := (↑p).b, property := (_ : (↑p).b ∈ B) }
p₁ p₂ : { x // x ∈ P }
h : φ p₁ = φ p₂
h' : ¬p₁ = p₂
h'' : ↑p₁ ≠ ↑p₂
h1 : (↑p₁).b ∈ Walk.support (↑p₁).to_Walk
⊢ (↑p₁).b ∈ Walk.support (↑p₂).to_Walk
Tactic:
simp at h
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
P : Finset (AB_Walk G A B)
dis : pwd P
φ : { x // x ∈ P } → { x // x ∈ B } := fun p => { val := (↑p).b, property := (_ : (↑p).b ∈ B) }
p₁ p₂ : { x // x ∈ P }
h' : ¬p₁ = p₂
h'' : ↑p₁ ≠ ↑p₂
h1 : (↑p₁).b ∈ Walk.support (↑p₁).to_Walk
h : (↑p₁).b = (↑p₂).b
⊢ (↑p₁).b ∈ Walk.support (↑p₂).to_Walk

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
P : Finset (AB_Walk G A B)
dis : pwd P
φ : { x // x ∈ P } → { x // x ∈ B } := fun p => { val := (↑p).b, property := (_ : (↑p).b ∈ B) }
p₁ p₂ : { x // x ∈ P }
h' : ¬p₁ = p₂
h'' : ↑p₁ ≠ ↑p₂
h1 : (↑p₁).b ∈ Walk.support (↑p₁).to_Walk
h : (↑p₁).b = (↑p₂).b
⊢ (↑p₁).b ∈ Walk.support (↑p₂).to_Walk
Tactic:
rw [h]
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
P : Finset (AB_Walk G A B)
dis : pwd P
φ : { x // x ∈ P } → { x // x ∈ B } := fun p => { val := (↑p).b, property := (_ : (↑p).b ∈ B) }
p₁ p₂ : { x // x ∈ P }
h' : ¬p₁ = p₂
h'' : ↑p₁ ≠ ↑p₂
h1 : (↑p₁).b ∈ Walk.support (↑p₁).to_Walk
h : (↑p₁).b = (↑p₂).b
⊢ (↑p₂).b ∈ Walk.support (↑p₂).to_Walk

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
P : Finset (AB_Walk G A B)
dis : pwd P
φ : { x // x ∈ P } → { x // x ∈ B } := fun p => { val := (↑p).b, property := (_ : (↑p).b ∈ B) }
p₁ p₂ : { x // x ∈ P }
h' : ¬p₁ = p₂
h'' : ↑p₁ ≠ ↑p₂
h1 : (↑p₁).b ∈ Walk.support (↑p₁).to_Walk
h : (↑p₁).b = (↑p₂).b
⊢ (↑p₂).b ∈ Walk.support (↑p₂).to_Walk
Tactic:
exact Walk.end_mem_support _
State after:
no goals