internlm/Lean-Github huggingface dataset:
Theorem: SimpleGraph.Menger.le_A
Proof 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]
Proof 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
Theorem: SimpleGraph.Menger.le_A
Proof 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 _
Proof state after:
no goals
Theorem: SimpleGraph.Menger.le_B
Proof 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⟩
Proof 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
Theorem: SimpleGraph.Menger.le_B
Proof 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
Proof 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
Theorem: SimpleGraph.Menger.le_B
Proof 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]
Proof 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 }
Theorem: SimpleGraph.Menger.le_B
Proof 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
Proof state after:
no goals
Theorem: SimpleGraph.Menger.le_B
Proof 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
Proof 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₂
Theorem: SimpleGraph.Menger.le_B
Proof 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'
Proof 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
Theorem: SimpleGraph.Menger.le_B
Proof 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]
Proof 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
Theorem: SimpleGraph.Menger.le_B
Proof 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 _
Proof 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
Theorem: SimpleGraph.Menger.le_B
Proof 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 _
Proof 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
Theorem: SimpleGraph.Menger.le_B
Proof 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
Proof state after:
no goals
Theorem: SimpleGraph.Menger.le_B
Proof 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]
Proof state after:
no goals
Theorem: SimpleGraph.Menger.le_B
Proof 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
Proof 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
Theorem: SimpleGraph.Menger.le_B
Proof 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]
Proof 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
Theorem: SimpleGraph.Menger.le_B
Proof 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 _
Proof state after:
no goals
Theorem: SimpleGraph.Menger.Separates.symm
Proof 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 : Separates G A B X
p : AB_Walk G B A
⊢ ∃ x ∈ X, x ∈ Walk.support p.to_Walk
Tactic:
simpa using h p.Reverse
Proof state after:
no goals
Theorem: SimpleGraph.Menger.Separates.inter_subset
Proof 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 : Separates G A B X
⊢ A ∩ B ⊆ X
Tactic:
intro x h1
Proof 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 : Separates G A B X
x : V
h1 : x ∈ A ∩ B
⊢ x ∈ X
Theorem: SimpleGraph.Menger.Separates.inter_subset
Proof 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 : Separates G A B X
x : V
h1 : x ∈ A ∩ B
⊢ x ∈ X
Tactic:
rw [mem_inter] at h1
Proof 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 : Separates G A B X
x : V
h1 : x ∈ A ∧ x ∈ B
⊢ x ∈ X
Theorem: SimpleGraph.Menger.Separates.inter_subset
Proof 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 : Separates G A B X
x : V
h1 : x ∈ A ∧ x ∈ B
⊢ x ∈ X
Tactic:
simpa using h ⟨x, x, h1.1, h1.2, Walk.nil⟩
Proof state after:
no goals
Theorem: SimpleGraph.Menger.Separator.card_symm
Proof 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
X : Separator G A B
⊢ card (symm X) = card X
Tactic:
cases X
Proof state after:
case mk
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 val✝ : Finset V
property✝ : Separates G A B val✝
⊢ card (symm { val := val✝, property := property✝ }) = card { val := val✝, property := property✝ }
Theorem: SimpleGraph.Menger.Separator.card_symm
Proof state before:
case mk
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 val✝ : Finset V
property✝ : Separates G A B val✝
⊢ card (symm { val := val✝, property := property✝ }) = card { val := val✝, property := property✝ }
Tactic:
simp [symm, card]
Proof state after:
no goals
Theorem: SimpleGraph.Menger.min_cut.symm
Proof 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
⊢ min_cut G A B = min_cut G B A
Tactic:
simp_rw [min_cut]
Proof 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
⊢ Nat.find (_ : ∃ n, is_cut_set_size G A B n) = Nat.find (_ : ∃ n, is_cut_set_size G B A n)
Theorem: SimpleGraph.Menger.min_cut.symm
Proof 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
⊢ Nat.find (_ : ∃ n, is_cut_set_size G A B n) = Nat.find (_ : ∃ n, is_cut_set_size G B A n)
Tactic:
congr 1
Proof 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
⊢ is_cut_set_size G A B = is_cut_set_size G B A
Theorem: SimpleGraph.Menger.min_cut.symm
Proof 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
⊢ is_cut_set_size G A B = is_cut_set_size G B A
Tactic:
ext n
Proof state after:
case e_p.h.a
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
n : ℕ
⊢ is_cut_set_size G A B n ↔ is_cut_set_size G B A n
Theorem: SimpleGraph.Menger.min_cut.symm
Proof state before:
case e_p.h.a
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
n : ℕ
⊢ is_cut_set_size G A B n ↔ is_cut_set_size G B A n
Tactic:
constructor <;> exact λ ⟨X, h⟩ => ⟨X.symm, by simp [h]⟩
Proof state after:
no goals
Theorem: SimpleGraph.Menger.min_cut.symm
Proof 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
n : ℕ
x✝ : is_cut_set_size G B A n
X : Separator G B A
h : Separator.card X = n
⊢ Separator.card (Separator.symm X) = n
Tactic:
simp [h]
Proof state after:
no goals
Theorem: SimpleGraph.Menger.min_cut.inter_le_min_cut
Proof 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
⊢ card (A ∩ B) ≤ min_cut G A B
Tactic:
rw [min_cut, Nat.le_find_iff]
Proof 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
⊢ ∀ m < card (A ∩ B), ¬is_cut_set_size G A B m
Theorem: SimpleGraph.Menger.min_cut.inter_le_min_cut
Proof 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
⊢ ∀ m < card (A ∩ B), ¬is_cut_set_size G A B m
Tactic:
rintro n hn ⟨⟨X, h⟩, h'⟩
Proof state after:
case intro.mk
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
n : ℕ
hn : n < card (A ∩ B)
X : Finset V
h : Separates G A B X
h' : Separator.card { val := X, property := h } = n
⊢ False
Theorem: SimpleGraph.Menger.min_cut.inter_le_min_cut
Proof state before:
case intro.mk
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
n : ℕ
hn : n < card (A ∩ B)
X : Finset V
h : Separates G A B X
h' : Separator.card { val := X, property := h } = n
⊢ False
Tactic:
simp only [Separator.card] at h'
Proof state after:
case intro.mk
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
n : ℕ
hn : n < card (A ∩ B)
X : Finset V
h : Separates G A B X
h' : card X = n
⊢ False
Theorem: SimpleGraph.Menger.min_cut.inter_le_min_cut
Proof state before:
case intro.mk
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
n : ℕ
hn : n < card (A ∩ B)
X : Finset V
h : Separates G A B X
h' : card X = n
⊢ False
Tactic:
linarith [card_le_card h.inter_subset]
Proof state after:
no goals
Theorem: SimpleGraph.Menger.upper_bound
Proof 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 ≤ min_cut G A B
Tactic:
obtain ⟨⟨X, h₁⟩, h₂⟩ := min_cut.set G A B
Proof state after:
case mk.mk
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 : Finset V
h₁ : Separates G A B X
h₂ : Separator.card { val := X, property := h₁ } = min_cut G A B
⊢ card P ≤ min_cut G A B
Theorem: SimpleGraph.Menger.upper_bound
Proof state before:
case mk.mk
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 : Finset V
h₁ : Separates G A B X
h₂ : Separator.card { val := X, property := h₁ } = min_cut G A B
⊢ card P ≤ min_cut G A B
Tactic:
simpa [← h₂] using path_le_cut dis h₁
Proof state after:
no goals
Theorem: SimpleGraph.Menger.bot_iff_no_edge
Proof 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 : Fintype.card (Dart G) = 0
⊢ G = ⊥
Tactic:
ext x y
Proof state after:
case Adj.h.h.a
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 : Fintype.card (Dart G) = 0
x y : V
⊢ Adj G x y ↔ Adj ⊥ x y
Theorem: SimpleGraph.Menger.bot_iff_no_edge
Proof state before:
case Adj.h.h.a
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 : Fintype.card (Dart G) = 0
x y : V
⊢ Adj G x y ↔ Adj ⊥ x y
Tactic:
simp
Proof state after:
case Adj.h.h.a
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 : Fintype.card (Dart G) = 0
x y : V
⊢ ¬Adj G x y
Theorem: SimpleGraph.Menger.bot_iff_no_edge
Proof state before:
case Adj.h.h.a
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 : Fintype.card (Dart G) = 0
x y : V
⊢ ¬Adj G x y
Tactic:
exact λ h' => isEmpty_iff.mp (Fintype.card_eq_zero_iff.mp h) ⟨⟨x, y⟩, h'⟩
Proof state after:
no goals
Theorem: SimpleGraph.Menger.bot_iff_no_edge
Proof 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 = ⊥
⊢ Fintype.card (Dart G) = 0
Tactic:
simpa only [h] using Fintype.card_eq_zero_iff.mpr <| isEmpty_iff.mpr Dart.is_adj
Proof state after:
no goals
Theorem: SimpleGraph.Menger.bot_Separates_iff
Proof 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 : A ∩ B ⊆ X
x✝ : AB_Walk ⊥ A B
a b : V
ha : a ∈ A
hb : b ∈ B
p : Walk ⊥ a b
⊢ ∃ x ∈ X, x ∈ Walk.support { a := a, b := b, ha := ha, hb := hb, to_Walk := p }.to_Walk
Tactic:
cases p with
| nil => exact ⟨a, by simpa using h <| mem_inter_of_mem ha hb⟩
| cons h' _ => cases h'
Proof state after:
no goals
Theorem: SimpleGraph.Menger.bot_Separates_iff
Proof state before:
case nil
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 : A ∩ B ⊆ X
x✝ : AB_Walk ⊥ A B
a : V
ha : a ∈ A
hb : a ∈ B
⊢ ∃ x ∈ X, x ∈ Walk.support { a := a, b := a, ha := ha, hb := hb, to_Walk := Walk.nil }.to_Walk
Tactic:
exact ⟨a, by simpa using h <| mem_inter_of_mem ha hb⟩
Proof state after:
no goals
Theorem: SimpleGraph.Menger.bot_Separates_iff
Proof 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 : A ∩ B ⊆ X
x✝ : AB_Walk ⊥ A B
a : V
ha : a ∈ A
hb : a ∈ B
⊢ a ∈ X ∧ a ∈ Walk.support { a := a, b := a, ha := ha, hb := hb, to_Walk := Walk.nil }.to_Walk
Tactic:
simpa using h <| mem_inter_of_mem ha hb
Proof state after:
no goals
Theorem: SimpleGraph.Menger.bot_Separates_iff
Proof state before:
case cons
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 : A ∩ B ⊆ X
x✝ : AB_Walk ⊥ A B
a b : V
ha : a ∈ A
hb : b ∈ B
v✝ : V
h' : Adj ⊥ a v✝
p✝ : Walk ⊥ v✝ b
⊢ ∃ x ∈ X, x ∈ Walk.support { a := a, b := b, ha := ha, hb := hb, to_Walk := Walk.cons h' p✝ }.to_Walk
Tactic:
cases h'
Proof state after:
no goals
Theorem: SimpleGraph.Menger.bot_min_cut
Proof 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
⊢ min_cut ⊥ A B = card (A ∩ B)
Tactic:
refine le_antisymm ?_ min_cut.inter_le_min_cut
Proof 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
⊢ min_cut ⊥ A B ≤ card (A ∩ B)
Theorem: SimpleGraph.Menger.bot_min_cut
Proof 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
⊢ min_cut ⊥ A B ≤ card (A ∩ B)
Tactic:
rw [min_cut, Nat.find_le_iff]
Proof 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
⊢ ∃ m ≤ card (A ∩ B), is_cut_set_size ⊥ A B m
Theorem: SimpleGraph.Menger.bot_min_cut
Proof 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
⊢ ∃ m ≤ card (A ∩ B), is_cut_set_size ⊥ A B m
Tactic:
refine ⟨(A ∩ B).card, le_rfl, ?_⟩
Proof 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
⊢ is_cut_set_size ⊥ A B (card (A ∩ B))
Theorem: SimpleGraph.Menger.bot_min_cut
Proof 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
⊢ is_cut_set_size ⊥ A B (card (A ∩ B))
Tactic:
simpa only [is_cut_set_size] using ⟨⟨A ∩ B, bot_Separates_iff.mpr le_rfl⟩, rfl⟩
Proof state after:
no goals
Theorem: SimpleGraph.Menger.isMenger_bot
Proof 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
⊢ isMenger ⊥
Tactic:
rintro A B
Proof 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 A B : Finset V
⊢ ∃ P, pwd P ∧ card P = min_cut ⊥ A B