internlm/Lean-Github huggingface dataset:
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 A B : Finset V
⊢ ∃ P, pwd P ∧ card P = min_cut ⊥ A B
Tactic:
rw [bot_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 A B : Finset V
⊢ ∃ P, pwd P ∧ card P = card (A ∩ B)
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 A B : Finset V
⊢ ∃ P, pwd P ∧ card P = card (A ∩ B)
Tactic:
let φ (z : (A ∩ B : Finset V)) : AB_Walk ⊥ A B :=
  let h := mem_inter.mp z.prop ; ⟨z, z, h.1, h.2, Walk.nil⟩
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
φ : { x // x ∈ A ∩ B } → AB_Walk ⊥ A B :=
  fun z =>
    let h := (_ : ↑z ∈ A ∧ ↑z ∈ B);
    { a := ↑z, b := ↑z, ha := (_ : ↑z ∈ A), hb := (_ : ↑z ∈ B), to_Walk := Walk.nil }
⊢ ∃ P, pwd P ∧ card P = card (A ∩ B)
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 A B : Finset V
φ : { x // x ∈ A ∩ B } → AB_Walk ⊥ A B :=
  fun z =>
    let h := (_ : ↑z ∈ A ∧ ↑z ∈ B);
    { a := ↑z, b := ↑z, ha := (_ : ↑z ∈ A), hb := (_ : ↑z ∈ B), to_Walk := Walk.nil }
⊢ ∃ P, pwd P ∧ card P = card (A ∩ B)
Tactic:
have φ_inj : Injective φ := by intro u v h ; ext ; simp [φ] at h ; exact h.1
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
φ : { x // x ∈ A ∩ B } → AB_Walk ⊥ A B :=
  fun z =>
    let h := (_ : ↑z ∈ A ∧ ↑z ∈ B);
    { a := ↑z, b := ↑z, ha := (_ : ↑z ∈ A), hb := (_ : ↑z ∈ B), to_Walk := Walk.nil }
φ_inj : Injective φ
⊢ ∃ P, pwd P ∧ card P = card (A ∩ B)
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 A B : Finset V
φ : { x // x ∈ A ∩ B } → AB_Walk ⊥ A B :=
  fun z =>
    let h := (_ : ↑z ∈ A ∧ ↑z ∈ B);
    { a := ↑z, b := ↑z, ha := (_ : ↑z ∈ A), hb := (_ : ↑z ∈ B), to_Walk := Walk.nil }
φ_inj : Injective φ
⊢ ∃ P, pwd P ∧ card P = card (A ∩ B)
Tactic:
refine ⟨image φ univ, ?_, by simp [card_image_of_injective, φ_inj]⟩
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
φ : { x // x ∈ A ∩ B } → AB_Walk ⊥ A B :=
  fun z =>
    let h := (_ : ↑z ∈ A ∧ ↑z ∈ B);
    { a := ↑z, b := ↑z, ha := (_ : ↑z ∈ A), hb := (_ : ↑z ∈ B), to_Walk := Walk.nil }
φ_inj : Injective φ
⊢ pwd (image φ univ)
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 A B : Finset V
φ : { x // x ∈ A ∩ B } → AB_Walk ⊥ A B :=
  fun z =>
    let h := (_ : ↑z ∈ A ∧ ↑z ∈ B);
    { a := ↑z, b := ↑z, ha := (_ : ↑z ∈ A), hb := (_ : ↑z ∈ B), to_Walk := Walk.nil }
φ_inj : Injective φ
⊢ pwd (image φ univ)
Tactic:
rintro ⟨a, b, _, _, p⟩ hp ⟨a', b', _, _, q⟩ hq h
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 A B : Finset V
φ : { x // x ∈ A ∩ B } → AB_Walk ⊥ A B :=
  fun z =>
    let h := (_ : ↑z ∈ A ∧ ↑z ∈ B);
    { a := ↑z, b := ↑z, ha := (_ : ↑z ∈ A), hb := (_ : ↑z ∈ B), to_Walk := Walk.nil }
φ_inj : Injective φ
a b : V
ha✝¹ : a ∈ A
hb✝¹ : b ∈ B
p : Walk ⊥ a b
hp : { a := a, b := b, ha := ha✝¹, hb := hb✝¹, to_Walk := p } ∈ ↑(image φ univ)
a' b' : V
ha✝ : a' ∈ A
hb✝ : b' ∈ B
q : Walk ⊥ a' b'
hq : { a := a', b := b', ha := ha✝, hb := hb✝, to_Walk := q } ∈ ↑(image φ univ)
h : { a := a, b := b, ha := ha✝¹, hb := hb✝¹, to_Walk := p } ≠ { a := a', b := b', ha := ha✝, hb := hb✝, to_Walk := q }
⊢ AB_Walk.Disjoint { a := a, b := b, ha := ha✝¹, hb := hb✝¹, to_Walk := p }
    { a := a', b := b', ha := ha✝, hb := hb✝, to_Walk := q }
Theorem: SimpleGraph.Menger.isMenger_bot
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 A B : Finset V
φ : { x // x ∈ A ∩ B } → AB_Walk ⊥ A B :=
  fun z =>
    let h := (_ : ↑z ∈ A ∧ ↑z ∈ B);
    { a := ↑z, b := ↑z, ha := (_ : ↑z ∈ A), hb := (_ : ↑z ∈ B), to_Walk := Walk.nil }
φ_inj : Injective φ
a b : V
ha✝¹ : a ∈ A
hb✝¹ : b ∈ B
p : Walk ⊥ a b
hp : { a := a, b := b, ha := ha✝¹, hb := hb✝¹, to_Walk := p } ∈ ↑(image φ univ)
a' b' : V
ha✝ : a' ∈ A
hb✝ : b' ∈ B
q : Walk ⊥ a' b'
hq : { a := a', b := b', ha := ha✝, hb := hb✝, to_Walk := q } ∈ ↑(image φ univ)
h : { a := a, b := b, ha := ha✝¹, hb := hb✝¹, to_Walk := p } ≠ { a := a', b := b', ha := ha✝, hb := hb✝, to_Walk := q }
⊢ AB_Walk.Disjoint { a := a, b := b, ha := ha✝¹, hb := hb✝¹, to_Walk := p }
    { a := a', b := b', ha := ha✝, hb := hb✝, to_Walk := q }
Tactic:
simp at hp hq h
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 A B : Finset V
φ : { x // x ∈ A ∩ B } → AB_Walk ⊥ A B :=
  fun z =>
    let h := (_ : ↑z ∈ A ∧ ↑z ∈ B);
    { a := ↑z, b := ↑z, ha := (_ : ↑z ∈ A), hb := (_ : ↑z ∈ B), to_Walk := Walk.nil }
φ_inj : Injective φ
a b : V
ha✝¹ : a ∈ A
hb✝¹ : b ∈ B
p : Walk ⊥ a b
a' b' : V
ha✝ : a' ∈ A
hb✝ : b' ∈ B
q : Walk ⊥ a' b'
hp : a = b ∧ (a ∈ A ∧ a ∈ B) ∧ HEq Walk.nil p
hq : a' = b' ∧ (a' ∈ A ∧ a' ∈ B) ∧ HEq Walk.nil q
h : a = a' → b = b' → ¬HEq p q
⊢ AB_Walk.Disjoint { a := a, b := b, ha := ha✝¹, hb := hb✝¹, to_Walk := p }
    { a := a', b := b', ha := ha✝, hb := hb✝, to_Walk := q }
Theorem: SimpleGraph.Menger.isMenger_bot
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 A B : Finset V
φ : { x // x ∈ A ∩ B } → AB_Walk ⊥ A B :=
  fun z =>
    let h := (_ : ↑z ∈ A ∧ ↑z ∈ B);
    { a := ↑z, b := ↑z, ha := (_ : ↑z ∈ A), hb := (_ : ↑z ∈ B), to_Walk := Walk.nil }
φ_inj : Injective φ
a b : V
ha✝¹ : a ∈ A
hb✝¹ : b ∈ B
p : Walk ⊥ a b
a' b' : V
ha✝ : a' ∈ A
hb✝ : b' ∈ B
q : Walk ⊥ a' b'
hp : a = b ∧ (a ∈ A ∧ a ∈ B) ∧ HEq Walk.nil p
hq : a' = b' ∧ (a' ∈ A ∧ a' ∈ B) ∧ HEq Walk.nil q
h : a = a' → b = b' → ¬HEq p q
⊢ AB_Walk.Disjoint { a := a, b := b, ha := ha✝¹, hb := hb✝¹, to_Walk := p }
    { a := a', b := b', ha := ha✝, hb := hb✝, to_Walk := q }
Tactic:
rcases hp with ⟨rfl, -, h4⟩
Proof state after:
case mk.mk.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 A B : Finset V
φ : { x // x ∈ A ∩ B } → AB_Walk ⊥ A B :=
  fun z =>
    let h := (_ : ↑z ∈ A ∧ ↑z ∈ B);
    { a := ↑z, b := ↑z, ha := (_ : ↑z ∈ A), hb := (_ : ↑z ∈ B), to_Walk := Walk.nil }
φ_inj : Injective φ
a : V
ha✝¹ : a ∈ A
a' b' : V
ha✝ : a' ∈ A
hb✝¹ : b' ∈ B
q : Walk ⊥ a' b'
hq : a' = b' ∧ (a' ∈ A ∧ a' ∈ B) ∧ HEq Walk.nil q
hb✝ : a ∈ B
p : Walk ⊥ a a
h : a = a' → a = b' → ¬HEq p q
h4 : HEq Walk.nil p
⊢ AB_Walk.Disjoint { a := a, b := a, ha := ha✝¹, hb := hb✝, to_Walk := p }
    { a := a', b := b', ha := ha✝, hb := hb✝¹, to_Walk := q }
Theorem: SimpleGraph.Menger.isMenger_bot
Proof state before:
case mk.mk.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 A B : Finset V
φ : { x // x ∈ A ∩ B } → AB_Walk ⊥ A B :=
  fun z =>
    let h := (_ : ↑z ∈ A ∧ ↑z ∈ B);
    { a := ↑z, b := ↑z, ha := (_ : ↑z ∈ A), hb := (_ : ↑z ∈ B), to_Walk := Walk.nil }
φ_inj : Injective φ
a : V
ha✝¹ : a ∈ A
a' b' : V
ha✝ : a' ∈ A
hb✝¹ : b' ∈ B
q : Walk ⊥ a' b'
hq : a' = b' ∧ (a' ∈ A ∧ a' ∈ B) ∧ HEq Walk.nil q
hb✝ : a ∈ B
p : Walk ⊥ a a
h : a = a' → a = b' → ¬HEq p q
h4 : HEq Walk.nil p
⊢ AB_Walk.Disjoint { a := a, b := a, ha := ha✝¹, hb := hb✝, to_Walk := p }
    { a := a', b := b', ha := ha✝, hb := hb✝¹, to_Walk := q }
Tactic:
rcases hq with ⟨rfl, -, h8⟩
Proof state after:
case mk.mk.intro.intro.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 A B : Finset V
φ : { x // x ∈ A ∩ B } → AB_Walk ⊥ A B :=
  fun z =>
    let h := (_ : ↑z ∈ A ∧ ↑z ∈ B);
    { a := ↑z, b := ↑z, ha := (_ : ↑z ∈ A), hb := (_ : ↑z ∈ B), to_Walk := Walk.nil }
φ_inj : Injective φ
a : V
ha✝¹ : a ∈ A
a' : V
ha✝ : a' ∈ A
hb✝¹ : a ∈ B
p : Walk ⊥ a a
h4 : HEq Walk.nil p
hb✝ : a' ∈ B
q : Walk ⊥ a' a'
h : a = a' → a = a' → ¬HEq p q
h8 : HEq Walk.nil q
⊢ AB_Walk.Disjoint { a := a, b := a, ha := ha✝¹, hb := hb✝¹, to_Walk := p }
    { a := a', b := a', ha := ha✝, hb := hb✝, to_Walk := q }
Theorem: SimpleGraph.Menger.isMenger_bot
Proof state before:
case mk.mk.intro.intro.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 A B : Finset V
φ : { x // x ∈ A ∩ B } → AB_Walk ⊥ A B :=
  fun z =>
    let h := (_ : ↑z ∈ A ∧ ↑z ∈ B);
    { a := ↑z, b := ↑z, ha := (_ : ↑z ∈ A), hb := (_ : ↑z ∈ B), to_Walk := Walk.nil }
φ_inj : Injective φ
a : V
ha✝¹ : a ∈ A
a' : V
ha✝ : a' ∈ A
hb✝¹ : a ∈ B
p : Walk ⊥ a a
h4 : HEq Walk.nil p
hb✝ : a' ∈ B
q : Walk ⊥ a' a'
h : a = a' → a = a' → ¬HEq p q
h8 : HEq Walk.nil q
⊢ AB_Walk.Disjoint { a := a, b := a, ha := ha✝¹, hb := hb✝¹, to_Walk := p }
    { a := a', b := a', ha := ha✝, hb := hb✝, to_Walk := q }
Tactic:
subst_vars
Proof state after:
case mk.mk.intro.intro.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 A B : Finset V
φ : { x // x ∈ A ∩ B } → AB_Walk ⊥ A B :=
  fun z =>
    let h := (_ : ↑z ∈ A ∧ ↑z ∈ B);
    { a := ↑z, b := ↑z, ha := (_ : ↑z ∈ A), hb := (_ : ↑z ∈ B), to_Walk := Walk.nil }
φ_inj : Injective φ
a : V
ha✝¹ : a ∈ A
a' : V
ha✝ : a' ∈ A
hb✝¹ : a ∈ B
hb✝ : a' ∈ B
h : a = a' → a = a' → ¬HEq Walk.nil Walk.nil
⊢ AB_Walk.Disjoint { a := a, b := a, ha := ha✝¹, hb := hb✝¹, to_Walk := Walk.nil }
    { a := a', b := a', ha := ha✝, hb := hb✝, to_Walk := Walk.nil }
Theorem: SimpleGraph.Menger.isMenger_bot
Proof state before:
case mk.mk.intro.intro.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 A B : Finset V
φ : { x // x ∈ A ∩ B } → AB_Walk ⊥ A B :=
  fun z =>
    let h := (_ : ↑z ∈ A ∧ ↑z ∈ B);
    { a := ↑z, b := ↑z, ha := (_ : ↑z ∈ A), hb := (_ : ↑z ∈ B), to_Walk := Walk.nil }
φ_inj : Injective φ
a : V
ha✝¹ : a ∈ A
a' : V
ha✝ : a' ∈ A
hb✝¹ : a ∈ B
hb✝ : a' ∈ B
h : a = a' → a = a' → ¬HEq Walk.nil Walk.nil
⊢ AB_Walk.Disjoint { a := a, b := a, ha := ha✝¹, hb := hb✝¹, to_Walk := Walk.nil }
    { a := a', b := a', ha := ha✝, hb := hb✝, to_Walk := Walk.nil }
Tactic:
simp [AB_Walk.Disjoint]
Proof state after:
case mk.mk.intro.intro.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 A B : Finset V
φ : { x // x ∈ A ∩ B } → AB_Walk ⊥ A B :=
  fun z =>
    let h := (_ : ↑z ∈ A ∧ ↑z ∈ B);
    { a := ↑z, b := ↑z, ha := (_ : ↑z ∈ A), hb := (_ : ↑z ∈ B), to_Walk := Walk.nil }
φ_inj : Injective φ
a : V
ha✝¹ : a ∈ A
a' : V
ha✝ : a' ∈ A
hb✝¹ : a ∈ B
hb✝ : a' ∈ B
h : a = a' → a = a' → ¬HEq Walk.nil Walk.nil
⊢ ¬a' = a
Theorem: SimpleGraph.Menger.isMenger_bot
Proof state before:
case mk.mk.intro.intro.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 A B : Finset V
φ : { x // x ∈ A ∩ B } → AB_Walk ⊥ A B :=
  fun z =>
    let h := (_ : ↑z ∈ A ∧ ↑z ∈ B);
    { a := ↑z, b := ↑z, ha := (_ : ↑z ∈ A), hb := (_ : ↑z ∈ B), to_Walk := Walk.nil }
φ_inj : Injective φ
a : V
ha✝¹ : a ∈ A
a' : V
ha✝ : a' ∈ A
hb✝¹ : a ∈ B
hb✝ : a' ∈ B
h : a = a' → a = a' → ¬HEq Walk.nil Walk.nil
⊢ ¬a' = a
Tactic:
rintro rfl
Proof state after:
case mk.mk.intro.intro.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 A B : Finset V
φ : { x // x ∈ A ∩ B } → AB_Walk ⊥ A B :=
  fun z =>
    let h := (_ : ↑z ∈ A ∧ ↑z ∈ B);
    { a := ↑z, b := ↑z, ha := (_ : ↑z ∈ A), hb := (_ : ↑z ∈ B), to_Walk := Walk.nil }
φ_inj : Injective φ
a' : V
ha✝¹ : a' ∈ A
hb✝¹ : a' ∈ B
ha✝ : a' ∈ A
hb✝ : a' ∈ B
h : a' = a' → a' = a' → ¬HEq Walk.nil Walk.nil
⊢ False
Theorem: SimpleGraph.Menger.isMenger_bot
Proof state before:
case mk.mk.intro.intro.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 A B : Finset V
φ : { x // x ∈ A ∩ B } → AB_Walk ⊥ A B :=
  fun z =>
    let h := (_ : ↑z ∈ A ∧ ↑z ∈ B);
    { a := ↑z, b := ↑z, ha := (_ : ↑z ∈ A), hb := (_ : ↑z ∈ B), to_Walk := Walk.nil }
φ_inj : Injective φ
a' : V
ha✝¹ : a' ∈ A
hb✝¹ : a' ∈ B
ha✝ : a' ∈ A
hb✝ : a' ∈ B
h : a' = a' → a' = a' → ¬HEq Walk.nil Walk.nil
⊢ False
Tactic:
simp at h
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 A B : Finset V
φ : { x // x ∈ A ∩ B } → AB_Walk ⊥ A B :=
  fun z =>
    let h := (_ : ↑z ∈ A ∧ ↑z ∈ B);
    { a := ↑z, b := ↑z, ha := (_ : ↑z ∈ A), hb := (_ : ↑z ∈ B), to_Walk := Walk.nil }
⊢ Injective φ
Tactic:
intro u v 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 A B : Finset V
φ : { x // x ∈ A ∩ B } → AB_Walk ⊥ A B :=
  fun z =>
    let h := (_ : ↑z ∈ A ∧ ↑z ∈ B);
    { a := ↑z, b := ↑z, ha := (_ : ↑z ∈ A), hb := (_ : ↑z ∈ B), to_Walk := Walk.nil }
u v : { x // x ∈ A ∩ B }
h : φ u = φ v
⊢ u = v
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 A B : Finset V
φ : { x // x ∈ A ∩ B } → AB_Walk ⊥ A B :=
  fun z =>
    let h := (_ : ↑z ∈ A ∧ ↑z ∈ B);
    { a := ↑z, b := ↑z, ha := (_ : ↑z ∈ A), hb := (_ : ↑z ∈ B), to_Walk := Walk.nil }
u v : { x // x ∈ A ∩ B }
h : φ u = φ v
⊢ u = v
Tactic:
ext
Proof state after:
case 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 A B : Finset V
φ : { x // x ∈ A ∩ B } → AB_Walk ⊥ A B :=
  fun z =>
    let h := (_ : ↑z ∈ A ∧ ↑z ∈ B);
    { a := ↑z, b := ↑z, ha := (_ : ↑z ∈ A), hb := (_ : ↑z ∈ B), to_Walk := Walk.nil }
u v : { x // x ∈ A ∩ B }
h : φ u = φ v
⊢ ↑u = ↑v
Theorem: SimpleGraph.Menger.isMenger_bot
Proof state before:
case 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 A B : Finset V
φ : { x // x ∈ A ∩ B } → AB_Walk ⊥ A B :=
  fun z =>
    let h := (_ : ↑z ∈ A ∧ ↑z ∈ B);
    { a := ↑z, b := ↑z, ha := (_ : ↑z ∈ A), hb := (_ : ↑z ∈ B), to_Walk := Walk.nil }
u v : { x // x ∈ A ∩ B }
h : φ u = φ v
⊢ ↑u = ↑v
Tactic:
simp [φ] at h
Proof state after:
case 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 A B : Finset V
φ : { x // x ∈ A ∩ B } → AB_Walk ⊥ A B :=
  fun z =>
    let h := (_ : ↑z ∈ A ∧ ↑z ∈ B);
    { a := ↑z, b := ↑z, ha := (_ : ↑z ∈ A), hb := (_ : ↑z ∈ B), to_Walk := Walk.nil }
u v : { x // x ∈ A ∩ B }
h : ↑u = ↑v ∧ HEq Walk.nil Walk.nil
⊢ ↑u = ↑v
Theorem: SimpleGraph.Menger.isMenger_bot
Proof state before:
case 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 A B : Finset V
φ : { x // x ∈ A ∩ B } → AB_Walk ⊥ A B :=
  fun z =>
    let h := (_ : ↑z ∈ A ∧ ↑z ∈ B);
    { a := ↑z, b := ↑z, ha := (_ : ↑z ∈ A), hb := (_ : ↑z ∈ B), to_Walk := Walk.nil }
u v : { x // x ∈ A ∩ B }
h : ↑u = ↑v ∧ HEq Walk.nil Walk.nil
⊢ ↑u = ↑v
Tactic:
exact h.1
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 A B : Finset V
φ : { x // x ∈ A ∩ B } → AB_Walk ⊥ A B :=
  fun z =>
    let h := (_ : ↑z ∈ A ∧ ↑z ∈ B);
    { a := ↑z, b := ↑z, ha := (_ : ↑z ∈ A), hb := (_ : ↑z ∈ B), to_Walk := Walk.nil }
φ_inj : Injective φ
⊢ card (image φ univ) = card (A ∩ B)
Tactic:
simp [card_image_of_injective, φ_inj]
Proof state after:
no goals
Theorem: SimpleGraph.Menger.transportable_of_not_dart
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
e : Dart G
a b : V
p : Walk G a b
h : e ∉ Walk.darts p
h' : Dart.symm e ∉ Walk.darts p
⊢ Walk.transportable_to (G -ₑ Dart.edge e) p
Tactic:
intro f hf
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
e : Dart G
a b : V
p : Walk G a b
h : e ∉ Walk.darts p
h' : Dart.symm e ∉ Walk.darts p
f : Dart G
hf : f ∈ Walk.darts p
⊢ Adj (G -ₑ Dart.edge e) f.toProd.1 f.toProd.2
Theorem: SimpleGraph.Menger.transportable_of_not_dart
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
e : Dart G
a b : V
p : Walk G a b
h : e ∉ Walk.darts p
h' : Dart.symm e ∉ Walk.darts p
f : Dart G
hf : f ∈ Walk.darts p
⊢ Adj (G -ₑ Dart.edge e) f.toProd.1 f.toProd.2
Tactic:
simp [Minus, f.is_adj, Dart.edge]
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
e : Dart G
a b : V
p : Walk G a b
h : e ∉ Walk.darts p
h' : Dart.symm e ∉ Walk.darts p
f : Dart G
hf : f ∈ Walk.darts p
⊢ ¬(f.toProd = e.toProd ∨ f.toProd = Prod.swap e.toProd)
Theorem: SimpleGraph.Menger.transportable_of_not_dart
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
e : Dart G
a b : V
p : Walk G a b
h : e ∉ Walk.darts p
h' : Dart.symm e ∉ Walk.darts p
f : Dart G
hf : f ∈ Walk.darts p
⊢ ¬(f.toProd = e.toProd ∨ f.toProd = Prod.swap e.toProd)
Tactic:
intro hef
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
e : Dart G
a b : V
p : Walk G a b
h : e ∉ Walk.darts p
h' : Dart.symm e ∉ Walk.darts p
f : Dart G
hf : f ∈ Walk.darts p
hef : f.toProd = e.toProd ∨ f.toProd = Prod.swap e.toProd
⊢ False
Theorem: SimpleGraph.Menger.transportable_of_not_dart
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
e : Dart G
a b : V
p : Walk G a b
h : e ∉ Walk.darts p
h' : Dart.symm e ∉ Walk.darts p
f : Dart G
hf : f ∈ Walk.darts p
hef : f.toProd = e.toProd ∨ f.toProd = Prod.swap e.toProd
⊢ False
Tactic:
cases hef with
| inl h1 => exact h <| Dart.ext _ _ h1 ▸ hf
| inr h2 => rw [← Dart.symm_toProd] at h2 ; exact h' <| Dart.ext _ _ h2 ▸ hf
Proof state after:
no goals
Theorem: SimpleGraph.Menger.transportable_of_not_dart
Proof state before:
case inl
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
e : Dart G
a b : V
p : Walk G a b
h : e ∉ Walk.darts p
h' : Dart.symm e ∉ Walk.darts p
f : Dart G
hf : f ∈ Walk.darts p
h1 : f.toProd = e.toProd
⊢ False
Tactic:
exact h <| Dart.ext _ _ h1 ▸ hf
Proof state after:
no goals
Theorem: SimpleGraph.Menger.transportable_of_not_dart
Proof state before:
case inr
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
e : Dart G
a b : V
p : Walk G a b
h : e ∉ Walk.darts p
h' : Dart.symm e ∉ Walk.darts p
f : Dart G
hf : f ∈ Walk.darts p
h2 : f.toProd = Prod.swap e.toProd
⊢ False
Tactic:
rw [← Dart.symm_toProd] at h2
Proof state after:
case inr
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
e : Dart G
a b : V
p : Walk G a b
h : e ∉ Walk.darts p
h' : Dart.symm e ∉ Walk.darts p
f : Dart G
hf : f ∈ Walk.darts p
h2 : f.toProd = (Dart.symm e).toProd
⊢ False
Theorem: SimpleGraph.Menger.transportable_of_not_dart
Proof state before:
case inr
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
e : Dart G
a b : V
p : Walk G a b
h : e ∉ Walk.darts p
h' : Dart.symm e ∉ Walk.darts p
f : Dart G
hf : f ∈ Walk.darts p
h2 : f.toProd = (Dart.symm e).toProd
⊢ False
Tactic:
exact h' <| Dart.ext _ _ h2 ▸ hf
Proof state after:
no goals
Theorem: SimpleGraph.Menger.sep_AB_of_sep₂_AX
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
e : Dart G
ex_in_X : e.toProd.1 ∈ X
ey_in_X : e.toProd.2 ∈ X
X_sep_AB : Separates G A B X
Z_sep₂_AX : Separates (G -ₑ Dart.edge e) A X Z
⊢ Separates G A B Z
Tactic:
intro γ
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
e : Dart G
ex_in_X : e.toProd.1 ∈ X
ey_in_X : e.toProd.2 ∈ X
X_sep_AB : Separates G A B X
Z_sep₂_AX : Separates (G -ₑ Dart.edge e) A X Z
γ : AB_Walk G A B
⊢ ∃ x ∈ Z, x ∈ Walk.support γ.to_Walk
Theorem: SimpleGraph.Menger.sep_AB_of_sep₂_AX
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
e : Dart G
ex_in_X : e.toProd.1 ∈ X
ey_in_X : e.toProd.2 ∈ X
X_sep_AB : Separates G A B X
Z_sep₂_AX : Separates (G -ₑ Dart.edge e) A X Z
γ : AB_Walk G A B
⊢ ∃ x ∈ Z, x ∈ Walk.support γ.to_Walk
Tactic:
obtain ⟨x, hx1, hx2⟩ := X_sep_AB γ
Proof 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
e : Dart G
ex_in_X : e.toProd.1 ∈ X
ey_in_X : e.toProd.2 ∈ X
X_sep_AB : Separates G A B X
Z_sep₂_AX : Separates (G -ₑ Dart.edge e) A X Z
γ : AB_Walk G A B
x : V
hx1 : x ∈ X
hx2 : x ∈ Walk.support γ.to_Walk
⊢ ∃ x ∈ Z, x ∈ Walk.support γ.to_Walk
Theorem: SimpleGraph.Menger.sep_AB_of_sep₂_AX
Proof 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
e : Dart G
ex_in_X : e.toProd.1 ∈ X
ey_in_X : e.toProd.2 ∈ X
X_sep_AB : Separates G A B X
Z_sep₂_AX : Separates (G -ₑ Dart.edge e) A X Z
γ : AB_Walk G A B
x : V
hx1 : x ∈ X
hx2 : x ∈ Walk.support γ.to_Walk
δ : Walk G γ.a (entrance γ.to_Walk (fun x => x ∈ X) (_ : ∃ v ∈ Walk.support γ.to_Walk, (fun x => x ∈ X) v)) :=
  takeUntil γ.to_Walk (fun x => x ∈ X) (_ : ∃ v ∈ Walk.support γ.to_Walk, (fun x => x ∈ X) v)
key : Walk.transportable_to (G -ₑ Dart.edge e) δ
⊢ ∃ x ∈ Z, x ∈ Walk.support γ.to_Walk
Tactic:
obtain ⟨ζ, hζ⟩ := δ.transport key
Proof state after:
case intro.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
e : Dart G
ex_in_X : e.toProd.1 ∈ X
ey_in_X : e.toProd.2 ∈ X
X_sep_AB : Separates G A B X
Z_sep₂_AX : Separates (G -ₑ Dart.edge e) A X Z
γ : AB_Walk G A B
x : V
hx1 : x ∈ X
hx2 : x ∈ Walk.support γ.to_Walk
δ : Walk G γ.a (entrance γ.to_Walk (fun x => x ∈ X) (_ : ∃ v ∈ Walk.support γ.to_Walk, (fun x => x ∈ X) v)) :=
  takeUntil γ.to_Walk (fun x => x ∈ X) (_ : ∃ v ∈ Walk.support γ.to_Walk, (fun x => x ∈ X) v)
key : Walk.transportable_to (G -ₑ Dart.edge e) δ
ζ :
  Walk (G -ₑ Dart.edge e) γ.a
    (entrance γ.to_Walk (fun x => x ∈ X) (_ : ∃ v ∈ Walk.support γ.to_Walk, (fun x => x ∈ X) v))
hζ : Walk.support ζ = Walk.support δ
⊢ ∃ x ∈ Z, x ∈ Walk.support γ.to_Walk