Theorem: SimpleGraph.Menger.le_A (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 A
Tactic:
let φ (p : P) : A := ⟨p.val.a, p.val.ha⟩
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 ∈ A } := fun p => { val := (↑p).a, property := (_ : (↑p).a ∈ A) }
⊢ card P ≤ card A

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 ∈ A } := fun p => { val := (↑p).a, property := (_ : (↑p).a ∈ A) }
⊢ card P ≤ card A
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.a ∈ p₁.val.to_Walk.support := Walk.start_mem_support _
  have h2 : p₁.val.a ∈ p₂.val.to_Walk.support := by
    simp at h ; rw [h]
    exact Walk.start_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 ∈ A } := fun p => { val := (↑p).a, property := (_ : (↑p).a ∈ A) }
this : Injective φ
⊢ card P ≤ card A

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 ∈ A } := fun p => { val := (↑p).a, property := (_ : (↑p).a ∈ A) }
this : Injective φ
⊢ card P ≤ card A
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 ∈ A } := fun p => { val := (↑p).a, property := (_ : (↑p).a ∈ A) }
this : Injective φ
⊢ Fintype.card { x // x ∈ P } ≤ Fintype.card { x // x ∈ A }

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 ∈ A } := fun p => { val := (↑p).a, property := (_ : (↑p).a ∈ A) }
this : Injective φ
⊢ Fintype.card { x // x ∈ P } ≤ Fintype.card { x // x ∈ A }
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 ∈ A } := fun p => { val := (↑p).a, property := (_ : (↑p).a ∈ A) }
⊢ 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 ∈ A } := fun p => { val := (↑p).a, property := (_ : (↑p).a ∈ A) }
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 ∈ A } := fun p => { val := (↑p).a, property := (_ : (↑p).a ∈ A) }
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 ∈ A } := fun p => { val := (↑p).a, property := (_ : (↑p).a ∈ A) }
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 ∈ A } := fun p => { val := (↑p).a, property := (_ : (↑p).a ∈ A) }
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 ∈ A } := fun p => { val := (↑p).a, property := (_ : (↑p).a ∈ A) }
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 ∈ A } := fun p => { val := (↑p).a, property := (_ : (↑p).a ∈ A) }
p₁ p₂ : { x // x ∈ P }
h : φ p₁ = φ p₂
h' : ¬p₁ = p₂
h'' : ↑p₁ ≠ ↑p₂
⊢ False
Tactic:
have h1 : p₁.val.a ∈ p₁.val.to_Walk.support := Walk.start_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 ∈ A } := fun p => { val := (↑p).a, property := (_ : (↑p).a ∈ A) }
p₁ p₂ : { x // x ∈ P }
h : φ p₁ = φ p₂
h' : ¬p₁ = p₂
h'' : ↑p₁ ≠ ↑p₂
h1 : (↑p₁).a ∈ 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 ∈ A } := fun p => { val := (↑p).a, property := (_ : (↑p).a ∈ A) }
p₁ p₂ : { x // x ∈ P }
h : φ p₁ = φ p₂
h' : ¬p₁ = p₂
h'' : ↑p₁ ≠ ↑p₂
h1 : (↑p₁).a ∈ Walk.support (↑p₁).to_Walk
⊢ False
Tactic:
have h2 : p₁.val.a ∈ p₂.val.to_Walk.support := by
  simp at h ; rw [h]
  exact Walk.start_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 ∈ A } := fun p => { val := (↑p).a, property := (_ : (↑p).a ∈ A) }
p₁ p₂ : { x // x ∈ P }
h : φ p₁ = φ p₂
h' : ¬p₁ = p₂
h'' : ↑p₁ ≠ ↑p₂
h1 : (↑p₁).a ∈ Walk.support (↑p₁).to_Walk
h2 : (↑p₁).a ∈ 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 ∈ A } := fun p => { val := (↑p).a, property := (_ : (↑p).a ∈ A) }
p₁ p₂ : { x // x ∈ P }
h : φ p₁ = φ p₂
h' : ¬p₁ = p₂
h'' : ↑p₁ ≠ ↑p₂
h1 : (↑p₁).a ∈ Walk.support (↑p₁).to_Walk
h2 : (↑p₁).a ∈ 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 ∈ A } := fun p => { val := (↑p).a, property := (_ : (↑p).a ∈ A) }
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 ∈ A } := fun p => { val := (↑p).a, property := (_ : (↑p).a ∈ A) }
p₁ p₂ : { x // x ∈ P }
h : φ p₁ = φ p₂
h' : ¬p₁ = p₂
h'' : ↑p₁ ≠ ↑p₂
h1 : (↑p₁).a ∈ Walk.support (↑p₁).to_Walk
⊢ (↑p₁).a ∈ 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 ∈ A } := fun p => { val := (↑p).a, property := (_ : (↑p).a ∈ A) }
p₁ p₂ : { x // x ∈ P }
h' : ¬p₁ = p₂
h'' : ↑p₁ ≠ ↑p₂
h1 : (↑p₁).a ∈ Walk.support (↑p₁).to_Walk
h : (↑p₁).a = (↑p₂).a
⊢ (↑p₁).a ∈ 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 ∈ A } := fun p => { val := (↑p).a, property := (_ : (↑p).a ∈ A) }
p₁ p₂ : { x // x ∈ P }
h' : ¬p₁ = p₂
h'' : ↑p₁ ≠ ↑p₂
h1 : (↑p₁).a ∈ Walk.support (↑p₁).to_Walk
h : (↑p₁).a = (↑p₂).a
⊢ (↑p₁).a ∈ 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 ∈ A } := fun p => { val := (↑p).a, property := (_ : (↑p).a ∈ A) }
p₁ p₂ : { x // x ∈ P }
h' : ¬p₁ = p₂
h'' : ↑p₁ ≠ ↑p₂
h1 : (↑p₁).a ∈ Walk.support (↑p₁).to_Walk
h : (↑p₁).a = (↑p₂).a
⊢ (↑p₂).a ∈ 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 ∈ A } := fun p => { val := (↑p).a, property := (_ : (↑p).a ∈ A) }
p₁ p₂ : { x // x ∈ P }
h' : ¬p₁ = p₂
h'' : ↑p₁ ≠ ↑p₂
h1 : (↑p₁).a ∈ Walk.support (↑p₁).to_Walk
h : (↑p₁).a = (↑p₂).a
⊢ (↑p₂).a ∈ Walk.support (↑p₂).to_Walk
Tactic:
exact Walk.start_mem_support _
State after:
no goals