internlm/Lean-Github huggingface dataset:
Theorem: Matroid.connected_iff_not_exists_tutteSep
Proof state before:
α : Type u_1
M : Matroid α
k : ℕ
P : Set α → Prop
a b : α
inst✝ : M.Nonempty
⊢ (∃ P,
      (∀ (C : Set α), M.Circuit C → C ⊆ P.left ∪ P.right → C ⊆ P.left ∨ C ⊆ P.right) ∧
        P.left.Nonempty ∧ P.right.Nonempty) ↔
    ∃ x, ∃ x_1 ∈ M.E, x ∈ M.E ∧ ¬M.ConnectedTo x x_1
Tactic:
refine ⟨fun ⟨P, ⟨hc, hA, hB⟩⟩ ↦ ?_, fun ⟨x, y, hy, hx, h⟩ ↦ ?_⟩
Proof state after:
case refine_1
α : Type u_1
M : Matroid α
k : ℕ
P✝ : Set α → Prop
a b : α
inst✝ : M.Nonempty
x✝ :
  ∃ P,
    (∀ (C : Set α), M.Circuit C → C ⊆ P.left ∪ P.right → C ⊆ P.left ∨ C ⊆ P.right) ∧ P.left.Nonempty ∧ P.right.Nonempty
P : M.Partition
hc : ∀ (C : Set α), M.Circuit C → C ⊆ P.left ∪ P.right → C ⊆ P.left ∨ C ⊆ P.right
hA : P.left.Nonempty
hB : P.right.Nonempty
⊢ ∃ x, ∃ x_1 ∈ M.E, x ∈ M.E ∧ ¬M.ConnectedTo x x_1

case refine_2
α : Type u_1
M : Matroid α
k : ℕ
P : Set α → Prop
a b : α
inst✝ : M.Nonempty
x✝ : ∃ x, ∃ x_1 ∈ M.E, x ∈ M.E ∧ ¬M.ConnectedTo x x_1
x y : α
hy : y ∈ M.E
hx : x ∈ M.E
h : ¬M.ConnectedTo x y
⊢ ∃ P,
    (∀ (C : Set α), M.Circuit C → C ⊆ P.left ∪ P.right → C ⊆ P.left ∨ C ⊆ P.right) ∧ P.left.Nonempty ∧ P.right.Nonempty
Theorem: Matroid.connected_iff_not_exists_tutteSep
Proof state before:
case refine_2
α : Type u_1
M : Matroid α
k : ℕ
P : Set α → Prop
a b : α
inst✝ : M.Nonempty
x✝ : ∃ x, ∃ x_1 ∈ M.E, x ∈ M.E ∧ ¬M.ConnectedTo x x_1
x y : α
hy : y ∈ M.E
hx : x ∈ M.E
h : ¬M.ConnectedTo x y
⊢ ∃ P,
    (∀ (C : Set α), M.Circuit C → C ⊆ P.left ∪ P.right → C ⊆ P.left ∨ C ⊆ P.right) ∧ P.left.Nonempty ∧ P.right.Nonempty
Tactic:
refine ⟨Partition.of_subset {z | M.ConnectedTo x z} (fun z hz ↦ hz.mem_ground_right),
  ?_, ⟨x, by simpa⟩, ⟨y, by simp [hy, h]⟩⟩
Proof state after:
case refine_2
α : Type u_1
M : Matroid α
k : ℕ
P : Set α → Prop
a b : α
inst✝ : M.Nonempty
x✝ : ∃ x, ∃ x_1 ∈ M.E, x ∈ M.E ∧ ¬M.ConnectedTo x x_1
x y : α
hy : y ∈ M.E
hx : x ∈ M.E
h : ¬M.ConnectedTo x y
⊢ ∀ (C : Set α),
    M.Circuit C →
      C ⊆ (Partition.of_subset {z | M.ConnectedTo x z} ⋯).left ∪ (Partition.of_subset {z | M.ConnectedTo x z} ⋯).right →
        C ⊆ (Partition.of_subset {z | M.ConnectedTo x z} ⋯).left ∨
          C ⊆ (Partition.of_subset {z | M.ConnectedTo x z} ⋯).right
Theorem: Matroid.connected_iff_not_exists_tutteSep
Proof state before:
case refine_2
α : Type u_1
M : Matroid α
k : ℕ
P : Set α → Prop
a b : α
inst✝ : M.Nonempty
x✝ : ∃ x, ∃ x_1 ∈ M.E, x ∈ M.E ∧ ¬M.ConnectedTo x x_1
x y : α
hy : y ∈ M.E
hx : x ∈ M.E
h : ¬M.ConnectedTo x y
⊢ ∀ (C : Set α),
    M.Circuit C →
      C ⊆ (Partition.of_subset {z | M.ConnectedTo x z} ⋯).left ∪ (Partition.of_subset {z | M.ConnectedTo x z} ⋯).right →
        C ⊆ (Partition.of_subset {z | M.ConnectedTo x z} ⋯).left ∨
          C ⊆ (Partition.of_subset {z | M.ConnectedTo x z} ⋯).right
Tactic:
simp only [Partition.of_subset_left, Partition.of_subset_right, union_diff_self]
Proof state after:
case refine_2
α : Type u_1
M : Matroid α
k : ℕ
P : Set α → Prop
a b : α
inst✝ : M.Nonempty
x✝ : ∃ x, ∃ x_1 ∈ M.E, x ∈ M.E ∧ ¬M.ConnectedTo x x_1
x y : α
hy : y ∈ M.E
hx : x ∈ M.E
h : ¬M.ConnectedTo x y
⊢ ∀ (C : Set α),
    M.Circuit C → C ⊆ {z | M.ConnectedTo x z} ∪ M.E → C ⊆ {z | M.ConnectedTo x z} ∨ C ⊆ M.E \ {z | M.ConnectedTo x z}
Theorem: Matroid.connected_iff_not_exists_tutteSep
Proof state before:
case refine_2
α : Type u_1
M : Matroid α
k : ℕ
P : Set α → Prop
a b : α
inst✝ : M.Nonempty
x✝ : ∃ x, ∃ x_1 ∈ M.E, x ∈ M.E ∧ ¬M.ConnectedTo x x_1
x y : α
hy : y ∈ M.E
hx : x ∈ M.E
h : ¬M.ConnectedTo x y
⊢ ∀ (C : Set α),
    M.Circuit C → C ⊆ {z | M.ConnectedTo x z} ∪ M.E → C ⊆ {z | M.ConnectedTo x z} ∨ C ⊆ M.E \ {z | M.ConnectedTo x z}
Tactic:
rintro C hC -
Proof state after:
case refine_2
α : Type u_1
M : Matroid α
k : ℕ
P : Set α → Prop
a b : α
inst✝ : M.Nonempty
x✝ : ∃ x, ∃ x_1 ∈ M.E, x ∈ M.E ∧ ¬M.ConnectedTo x x_1
x y : α
hy : y ∈ M.E
hx : x ∈ M.E
h : ¬M.ConnectedTo x y
C : Set α
hC : M.Circuit C
⊢ C ⊆ {z | M.ConnectedTo x z} ∨ C ⊆ M.E \ {z | M.ConnectedTo x z}
Theorem: Matroid.connected_iff_not_exists_tutteSep
Proof state before:
case refine_2
α : Type u_1
M : Matroid α
k : ℕ
P : Set α → Prop
a b : α
inst✝ : M.Nonempty
x✝ : ∃ x, ∃ x_1 ∈ M.E, x ∈ M.E ∧ ¬M.ConnectedTo x x_1
x y : α
hy : y ∈ M.E
hx : x ∈ M.E
h : ¬M.ConnectedTo x y
C : Set α
hC : M.Circuit C
⊢ C ⊆ {z | M.ConnectedTo x z} ∨ C ⊆ M.E \ {z | M.ConnectedTo x z}
Tactic:
obtain ⟨e, he⟩ := hC.nonempty
Proof state after:
case refine_2.intro
α : Type u_1
M : Matroid α
k : ℕ
P : Set α → Prop
a b : α
inst✝ : M.Nonempty
x✝ : ∃ x, ∃ x_1 ∈ M.E, x ∈ M.E ∧ ¬M.ConnectedTo x x_1
x y : α
hy : y ∈ M.E
hx : x ∈ M.E
h : ¬M.ConnectedTo x y
C : Set α
hC : M.Circuit C
e : α
he : e ∈ C
⊢ C ⊆ {z | M.ConnectedTo x z} ∨ C ⊆ M.E \ {z | M.ConnectedTo x z}
Theorem: Matroid.connected_iff_not_exists_tutteSep
Proof state before:
case refine_2.intro
α : Type u_1
M : Matroid α
k : ℕ
P : Set α → Prop
a b : α
inst✝ : M.Nonempty
x✝ : ∃ x, ∃ x_1 ∈ M.E, x ∈ M.E ∧ ¬M.ConnectedTo x x_1
x y : α
hy : y ∈ M.E
hx : x ∈ M.E
h : ¬M.ConnectedTo x y
C : Set α
hC : M.Circuit C
e : α
he : e ∈ C
⊢ C ⊆ {z | M.ConnectedTo x z} ∨ C ⊆ M.E \ {z | M.ConnectedTo x z}
Tactic:
by_cases hex : M.ConnectedTo x e
Proof state after:
case pos
α : Type u_1
M : Matroid α
k : ℕ
P : Set α → Prop
a b : α
inst✝ : M.Nonempty
x✝ : ∃ x, ∃ x_1 ∈ M.E, x ∈ M.E ∧ ¬M.ConnectedTo x x_1
x y : α
hy : y ∈ M.E
hx : x ∈ M.E
h : ¬M.ConnectedTo x y
C : Set α
hC : M.Circuit C
e : α
he : e ∈ C
hex : M.ConnectedTo x e
⊢ C ⊆ {z | M.ConnectedTo x z} ∨ C ⊆ M.E \ {z | M.ConnectedTo x z}

case neg
α : Type u_1
M : Matroid α
k : ℕ
P : Set α → Prop
a b : α
inst✝ : M.Nonempty
x✝ : ∃ x, ∃ x_1 ∈ M.E, x ∈ M.E ∧ ¬M.ConnectedTo x x_1
x y : α
hy : y ∈ M.E
hx : x ∈ M.E
h : ¬M.ConnectedTo x y
C : Set α
hC : M.Circuit C
e : α
he : e ∈ C
hex : ¬M.ConnectedTo x e
⊢ C ⊆ {z | M.ConnectedTo x z} ∨ C ⊆ M.E \ {z | M.ConnectedTo x z}
Theorem: Matroid.connected_iff_not_exists_tutteSep
Proof state before:
case neg
α : Type u_1
M : Matroid α
k : ℕ
P : Set α → Prop
a b : α
inst✝ : M.Nonempty
x✝ : ∃ x, ∃ x_1 ∈ M.E, x ∈ M.E ∧ ¬M.ConnectedTo x x_1
x y : α
hy : y ∈ M.E
hx : x ∈ M.E
h : ¬M.ConnectedTo x y
C : Set α
hC : M.Circuit C
e : α
he : e ∈ C
hex : ¬M.ConnectedTo x e
⊢ C ⊆ {z | M.ConnectedTo x z} ∨ C ⊆ M.E \ {z | M.ConnectedTo x z}
Tactic:
refine .inr fun z hzC ↦ ⟨hC.subset_ground hzC, fun (hz : M.ConnectedTo x z) ↦ ?_⟩
Proof state after:
case neg
α : Type u_1
M : Matroid α
k : ℕ
P : Set α → Prop
a b : α
inst✝ : M.Nonempty
x✝ : ∃ x, ∃ x_1 ∈ M.E, x ∈ M.E ∧ ¬M.ConnectedTo x x_1
x y : α
hy : y ∈ M.E
hx : x ∈ M.E
h : ¬M.ConnectedTo x y
C : Set α
hC : M.Circuit C
e : α
he : e ∈ C
hex : ¬M.ConnectedTo x e
z : α
hzC : z ∈ C
hz : M.ConnectedTo x z
⊢ False
Theorem: Matroid.connected_iff_not_exists_tutteSep
Proof state before:
case neg
α : Type u_1
M : Matroid α
k : ℕ
P : Set α → Prop
a b : α
inst✝ : M.Nonempty
x✝ : ∃ x, ∃ x_1 ∈ M.E, x ∈ M.E ∧ ¬M.ConnectedTo x x_1
x y : α
hy : y ∈ M.E
hx : x ∈ M.E
h : ¬M.ConnectedTo x y
C : Set α
hC : M.Circuit C
e : α
he : e ∈ C
hex : ¬M.ConnectedTo x e
z : α
hzC : z ∈ C
hz : M.ConnectedTo x z
⊢ False
Tactic:
exact hex <| hz.trans <| hC.mem_connectedTo_mem hzC he
Proof state after:
no goals
Theorem: Matroid.connected_iff_not_exists_tutteSep
Proof state before:
α : Type u_1
M : Matroid α
k : ℕ
P : Set α → Prop
a b : α
inst✝ : M.Nonempty
⊢ M.Nonempty
Tactic:
assumption
Proof state after:
no goals
Theorem: Matroid.connected_iff_not_exists_tutteSep
Proof state before:
case refine_1
α : Type u_1
M : Matroid α
k : ℕ
P✝ : Set α → Prop
a b : α
inst✝ : M.Nonempty
x✝ :
  ∃ P,
    (∀ (C : Set α), M.Circuit C → C ⊆ P.left ∪ P.right → C ⊆ P.left ∨ C ⊆ P.right) ∧ P.left.Nonempty ∧ P.right.Nonempty
P : M.Partition
hc : ∀ (C : Set α), M.Circuit C → C ⊆ P.left ∪ P.right → C ⊆ P.left ∨ C ⊆ P.right
hA : P.left.Nonempty
hB : P.right.Nonempty
⊢ ∃ x, ∃ x_1 ∈ M.E, x ∈ M.E ∧ ¬M.ConnectedTo x x_1
Tactic:
obtain ⟨a, ha⟩ := hA
Proof state after:
case refine_1.intro
α : Type u_1
M : Matroid α
k : ℕ
P✝ : Set α → Prop
a✝ b : α
inst✝ : M.Nonempty
x✝ :
  ∃ P,
    (∀ (C : Set α), M.Circuit C → C ⊆ P.left ∪ P.right → C ⊆ P.left ∨ C ⊆ P.right) ∧ P.left.Nonempty ∧ P.right.Nonempty
P : M.Partition
hc : ∀ (C : Set α), M.Circuit C → C ⊆ P.left ∪ P.right → C ⊆ P.left ∨ C ⊆ P.right
hB : P.right.Nonempty
a : α
ha : a ∈ P.left
⊢ ∃ x, ∃ x_1 ∈ M.E, x ∈ M.E ∧ ¬M.ConnectedTo x x_1
Theorem: Matroid.connected_iff_not_exists_tutteSep
Proof state before:
case refine_1.intro
α : Type u_1
M : Matroid α
k : ℕ
P✝ : Set α → Prop
a✝ b : α
inst✝ : M.Nonempty
x✝ :
  ∃ P,
    (∀ (C : Set α), M.Circuit C → C ⊆ P.left ∪ P.right → C ⊆ P.left ∨ C ⊆ P.right) ∧ P.left.Nonempty ∧ P.right.Nonempty
P : M.Partition
hc : ∀ (C : Set α), M.Circuit C → C ⊆ P.left ∪ P.right → C ⊆ P.left ∨ C ⊆ P.right
hB : P.right.Nonempty
a : α
ha : a ∈ P.left
⊢ ∃ x, ∃ x_1 ∈ M.E, x ∈ M.E ∧ ¬M.ConnectedTo x x_1
Tactic:
obtain ⟨b, hb⟩ := hB
Proof state after:
case refine_1.intro.intro
α : Type u_1
M : Matroid α
k : ℕ
P✝ : Set α → Prop
a✝ b✝ : α
inst✝ : M.Nonempty
x✝ :
  ∃ P,
    (∀ (C : Set α), M.Circuit C → C ⊆ P.left ∪ P.right → C ⊆ P.left ∨ C ⊆ P.right) ∧ P.left.Nonempty ∧ P.right.Nonempty
P : M.Partition
hc : ∀ (C : Set α), M.Circuit C → C ⊆ P.left ∪ P.right → C ⊆ P.left ∨ C ⊆ P.right
a : α
ha : a ∈ P.left
b : α
hb : b ∈ P.right
⊢ ∃ x, ∃ x_1 ∈ M.E, x ∈ M.E ∧ ¬M.ConnectedTo x x_1
Theorem: Matroid.connected_iff_not_exists_tutteSep
Proof state before:
case refine_1.intro.intro
α : Type u_1
M : Matroid α
k : ℕ
P✝ : Set α → Prop
a✝ b✝ : α
inst✝ : M.Nonempty
x✝ :
  ∃ P,
    (∀ (C : Set α), M.Circuit C → C ⊆ P.left ∪ P.right → C ⊆ P.left ∨ C ⊆ P.right) ∧ P.left.Nonempty ∧ P.right.Nonempty
P : M.Partition
hc : ∀ (C : Set α), M.Circuit C → C ⊆ P.left ∪ P.right → C ⊆ P.left ∨ C ⊆ P.right
a : α
ha : a ∈ P.left
b : α
hb : b ∈ P.right
⊢ ∃ x, ∃ x_1 ∈ M.E, x ∈ M.E ∧ ¬M.ConnectedTo x x_1
Tactic:
refine ⟨a, b, by simp [P.union_eq.symm, hb], by simp [P.union_eq.symm, ha], fun hconn ↦ ?_⟩
Proof state after:
case refine_1.intro.intro
α : Type u_1
M : Matroid α
k : ℕ
P✝ : Set α → Prop
a✝ b✝ : α
inst✝ : M.Nonempty
x✝ :
  ∃ P,
    (∀ (C : Set α), M.Circuit C → C ⊆ P.left ∪ P.right → C ⊆ P.left ∨ C ⊆ P.right) ∧ P.left.Nonempty ∧ P.right.Nonempty
P : M.Partition
hc : ∀ (C : Set α), M.Circuit C → C ⊆ P.left ∪ P.right → C ⊆ P.left ∨ C ⊆ P.right
a : α
ha : a ∈ P.left
b : α
hb : b ∈ P.right
hconn : M.ConnectedTo a b
⊢ False
Theorem: Matroid.connected_iff_not_exists_tutteSep
Proof state before:
case refine_1.intro.intro
α : Type u_1
M : Matroid α
k : ℕ
P✝ : Set α → Prop
a✝ b✝ : α
inst✝ : M.Nonempty
x✝ :
  ∃ P,
    (∀ (C : Set α), M.Circuit C → C ⊆ P.left ∪ P.right → C ⊆ P.left ∨ C ⊆ P.right) ∧ P.left.Nonempty ∧ P.right.Nonempty
P : M.Partition
hc : ∀ (C : Set α), M.Circuit C → C ⊆ P.left ∪ P.right → C ⊆ P.left ∨ C ⊆ P.right
a : α
ha : a ∈ P.left
b : α
hb : b ∈ P.right
hconn : M.ConnectedTo a b
⊢ False
Tactic:
obtain ⟨C, hC, haC, hbC⟩ := hconn.exists_circuit_of_ne (P.disjoint.ne_of_mem ha hb)
Proof state after:
case refine_1.intro.intro.intro.intro.intro
α : Type u_1
M : Matroid α
k : ℕ
P✝ : Set α → Prop
a✝ b✝ : α
inst✝ : M.Nonempty
x✝ :
  ∃ P,
    (∀ (C : Set α), M.Circuit C → C ⊆ P.left ∪ P.right → C ⊆ P.left ∨ C ⊆ P.right) ∧ P.left.Nonempty ∧ P.right.Nonempty
P : M.Partition
hc : ∀ (C : Set α), M.Circuit C → C ⊆ P.left ∪ P.right → C ⊆ P.left ∨ C ⊆ P.right
a : α
ha : a ∈ P.left
b : α
hb : b ∈ P.right
hconn : M.ConnectedTo a b
C : Set α
hC : M.Circuit C
haC : a ∈ C
hbC : b ∈ C
⊢ False
Theorem: Matroid.connected_iff_not_exists_tutteSep
Proof state before:
case refine_1.intro.intro.intro.intro.intro
α : Type u_1
M : Matroid α
k : ℕ
P✝ : Set α → Prop
a✝ b✝ : α
inst✝ : M.Nonempty
x✝ :
  ∃ P,
    (∀ (C : Set α), M.Circuit C → C ⊆ P.left ∪ P.right → C ⊆ P.left ∨ C ⊆ P.right) ∧ P.left.Nonempty ∧ P.right.Nonempty
P : M.Partition
hc : ∀ (C : Set α), M.Circuit C → C ⊆ P.left ∪ P.right → C ⊆ P.left ∨ C ⊆ P.right
a : α
ha : a ∈ P.left
b : α
hb : b ∈ P.right
hconn : M.ConnectedTo a b
C : Set α
hC : M.Circuit C
haC : a ∈ C
hbC : b ∈ C
⊢ False
Tactic:
obtain (hCA | hCB) := hc C hC (hC.subset_ground.trans_eq P.union_eq.symm)
Proof state after:
case refine_1.intro.intro.intro.intro.intro.inl
α : Type u_1
M : Matroid α
k : ℕ
P✝ : Set α → Prop
a✝ b✝ : α
inst✝ : M.Nonempty
x✝ :
  ∃ P,
    (∀ (C : Set α), M.Circuit C → C ⊆ P.left ∪ P.right → C ⊆ P.left ∨ C ⊆ P.right) ∧ P.left.Nonempty ∧ P.right.Nonempty
P : M.Partition
hc : ∀ (C : Set α), M.Circuit C → C ⊆ P.left ∪ P.right → C ⊆ P.left ∨ C ⊆ P.right
a : α
ha : a ∈ P.left
b : α
hb : b ∈ P.right
hconn : M.ConnectedTo a b
C : Set α
hC : M.Circuit C
haC : a ∈ C
hbC : b ∈ C
hCA : C ⊆ P.left
⊢ False

case refine_1.intro.intro.intro.intro.intro.inr
α : Type u_1
M : Matroid α
k : ℕ
P✝ : Set α → Prop
a✝ b✝ : α
inst✝ : M.Nonempty
x✝ :
  ∃ P,
    (∀ (C : Set α), M.Circuit C → C ⊆ P.left ∪ P.right → C ⊆ P.left ∨ C ⊆ P.right) ∧ P.left.Nonempty ∧ P.right.Nonempty
P : M.Partition
hc : ∀ (C : Set α), M.Circuit C → C ⊆ P.left ∪ P.right → C ⊆ P.left ∨ C ⊆ P.right
a : α
ha : a ∈ P.left
b : α
hb : b ∈ P.right
hconn : M.ConnectedTo a b
C : Set α
hC : M.Circuit C
haC : a ∈ C
hbC : b ∈ C
hCB : C ⊆ P.right
⊢ False
Theorem: Matroid.connected_iff_not_exists_tutteSep
Proof state before:
case refine_1.intro.intro.intro.intro.intro.inr
α : Type u_1
M : Matroid α
k : ℕ
P✝ : Set α → Prop
a✝ b✝ : α
inst✝ : M.Nonempty
x✝ :
  ∃ P,
    (∀ (C : Set α), M.Circuit C → C ⊆ P.left ∪ P.right → C ⊆ P.left ∨ C ⊆ P.right) ∧ P.left.Nonempty ∧ P.right.Nonempty
P : M.Partition
hc : ∀ (C : Set α), M.Circuit C → C ⊆ P.left ∪ P.right → C ⊆ P.left ∨ C ⊆ P.right
a : α
ha : a ∈ P.left
b : α
hb : b ∈ P.right
hconn : M.ConnectedTo a b
C : Set α
hC : M.Circuit C
haC : a ∈ C
hbC : b ∈ C
hCB : C ⊆ P.right
⊢ False
Tactic:
exact P.symm.disjoint.ne_of_mem (hCB haC) ha rfl
Proof state after:
no goals
Theorem: Matroid.connected_iff_not_exists_tutteSep
Proof state before:
α : Type u_1
M : Matroid α
k : ℕ
P✝ : Set α → Prop
a✝ b✝ : α
inst✝ : M.Nonempty
x✝ :
  ∃ P,
    (∀ (C : Set α), M.Circuit C → C ⊆ P.left ∪ P.right → C ⊆ P.left ∨ C ⊆ P.right) ∧ P.left.Nonempty ∧ P.right.Nonempty
P : M.Partition
hc : ∀ (C : Set α), M.Circuit C → C ⊆ P.left ∪ P.right → C ⊆ P.left ∨ C ⊆ P.right
a : α
ha : a ∈ P.left
b : α
hb : b ∈ P.right
⊢ b ∈ M.E
Tactic:
simp [P.union_eq.symm, hb]
Proof state after:
no goals
Theorem: Matroid.connected_iff_not_exists_tutteSep
Proof state before:
α : Type u_1
M : Matroid α
k : ℕ
P✝ : Set α → Prop
a✝ b✝ : α
inst✝ : M.Nonempty
x✝ :
  ∃ P,
    (∀ (C : Set α), M.Circuit C → C ⊆ P.left ∪ P.right → C ⊆ P.left ∨ C ⊆ P.right) ∧ P.left.Nonempty ∧ P.right.Nonempty
P : M.Partition
hc : ∀ (C : Set α), M.Circuit C → C ⊆ P.left ∪ P.right → C ⊆ P.left ∨ C ⊆ P.right
a : α
ha : a ∈ P.left
b : α
hb : b ∈ P.right
⊢ a ∈ M.E
Tactic:
simp [P.union_eq.symm, ha]
Proof state after:
no goals
Theorem: Matroid.connected_iff_not_exists_tutteSep
Proof state before:
case refine_1.intro.intro.intro.intro.intro.inl
α : Type u_1
M : Matroid α
k : ℕ
P✝ : Set α → Prop
a✝ b✝ : α
inst✝ : M.Nonempty
x✝ :
  ∃ P,
    (∀ (C : Set α), M.Circuit C → C ⊆ P.left ∪ P.right → C ⊆ P.left ∨ C ⊆ P.right) ∧ P.left.Nonempty ∧ P.right.Nonempty
P : M.Partition
hc : ∀ (C : Set α), M.Circuit C → C ⊆ P.left ∪ P.right → C ⊆ P.left ∨ C ⊆ P.right
a : α
ha : a ∈ P.left
b : α
hb : b ∈ P.right
hconn : M.ConnectedTo a b
C : Set α
hC : M.Circuit C
haC : a ∈ C
hbC : b ∈ C
hCA : C ⊆ P.left
⊢ False
Tactic:
exact P.disjoint.ne_of_mem (hCA hbC) hb rfl
Proof state after:
no goals
Theorem: Matroid.connected_iff_not_exists_tutteSep
Proof state before:
α : Type u_1
M : Matroid α
k : ℕ
P : Set α → Prop
a b : α
inst✝ : M.Nonempty
x✝ : ∃ x, ∃ x_1 ∈ M.E, x ∈ M.E ∧ ¬M.ConnectedTo x x_1
x y : α
hy : y ∈ M.E
hx : x ∈ M.E
h : ¬M.ConnectedTo x y
⊢ x ∈ (Partition.of_subset {z | M.ConnectedTo x z} ⋯).left
Tactic:
simpa
Proof state after:
no goals
Theorem: Matroid.connected_iff_not_exists_tutteSep
Proof state before:
α : Type u_1
M : Matroid α
k : ℕ
P : Set α → Prop
a b : α
inst✝ : M.Nonempty
x✝ : ∃ x, ∃ x_1 ∈ M.E, x ∈ M.E ∧ ¬M.ConnectedTo x x_1
x y : α
hy : y ∈ M.E
hx : x ∈ M.E
h : ¬M.ConnectedTo x y
⊢ y ∈ (Partition.of_subset {z | M.ConnectedTo x z} ⋯).right
Tactic:
simp [hy, h]
Proof state after:
no goals
Theorem: Matroid.connected_iff_not_exists_tutteSep
Proof state before:
case pos
α : Type u_1
M : Matroid α
k : ℕ
P : Set α → Prop
a b : α
inst✝ : M.Nonempty
x✝ : ∃ x, ∃ x_1 ∈ M.E, x ∈ M.E ∧ ¬M.ConnectedTo x x_1
x y : α
hy : y ∈ M.E
hx : x ∈ M.E
h : ¬M.ConnectedTo x y
C : Set α
hC : M.Circuit C
e : α
he : e ∈ C
hex : M.ConnectedTo x e
⊢ C ⊆ {z | M.ConnectedTo x z} ∨ C ⊆ M.E \ {z | M.ConnectedTo x z}
Tactic:
refine .inl (fun y hy ↦ hex.trans <| hC.mem_connectedTo_mem he hy )
Proof state after:
no goals
Theorem: Matroid.Hyperplane.exchange_base_of_circuit
Proof state before:
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ H
hf : f ∈ M.E \ H
⊢ M.Base (insert f (H \ {e}))
Tactic:
have hcl := hH.cl_insert_eq hf.2 hf.1
Proof state after:
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ H
hf : f ∈ M.E \ H
hcl : M.cl (insert f H) = M.E
⊢ M.Base (insert f (H \ {e}))
Theorem: Matroid.Hyperplane.exchange_base_of_circuit
Proof state before:
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ H
hf : f ∈ M.E \ H
hcl : M.cl (insert f H) = M.E
⊢ M.Base (insert f (H \ {e}))
Tactic:
rw [← cl_insert_cl_eq_cl_insert, ← hHc.cl_diff_singleton_eq_cl e, cl_insert_cl_eq_cl_insert,
  ← spanning_iff_cl (insert_subset hf.1 (diff_subset.trans hH.subset_ground))] at hcl
Proof state after:
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ H
hf : f ∈ M.E \ H
hcl : M.Spanning (insert f (H \ {e}))
⊢ M.Base (insert f (H \ {e}))
Theorem: Matroid.Hyperplane.exchange_base_of_circuit
Proof state before:
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ H
hf : f ∈ M.E \ H
hcl : M.Spanning (insert f (H \ {e}))
⊢ M.Base (insert f (H \ {e}))
Tactic:
refine' hcl.base_of_indep _
Proof state after:
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ H
hf : f ∈ M.E \ H
hcl : M.Spanning (insert f (H \ {e}))
⊢ M.Indep (insert f (H \ {e}))
Theorem: Matroid.Hyperplane.exchange_base_of_circuit
Proof state before:
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ H
hf : f ∈ M.E \ H
hcl : M.Spanning (insert f (H \ {e}))
⊢ M.Indep (insert f (H \ {e}))
Tactic:
rw [← (hHc.diff_singleton_indep he).not_mem_cl_iff_of_not_mem (fun hf' ↦ hf.2 hf'.1),
  hHc.cl_diff_singleton_eq_cl e, hH.flat.cl]
Proof state after:
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ H
hf : f ∈ M.E \ H
hcl : M.Spanning (insert f (H \ {e}))
⊢ f ∉ H
Theorem: Matroid.Hyperplane.exchange_base_of_circuit
Proof state before:
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ H
hf : f ∈ M.E \ H
hcl : M.Spanning (insert f (H \ {e}))
⊢ f ∉ H
Tactic:
exact hf.2
Proof state after:
no goals
Theorem: Matroid.Base.exists_exchange_of_circuit_of_hyperplane
Proof state before:
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hB : M.Base B
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ B
⊢ ∃ f ∈ H \ B, M.Base (insert f (B \ {e})) ∨ insert f (B \ {e}) = H
Tactic:
by_contra! h
Proof state after:
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hB : M.Base B
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ B
h : ∀ f ∈ H \ B, ¬M.Base (insert f (B \ {e})) ∧ insert f (B \ {e}) ≠ H
⊢ False
Theorem: Matroid.Base.exists_exchange_of_circuit_of_hyperplane
Proof state before:
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hB : M.Base B
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ B
h : ∀ f ∈ H \ B, ¬M.Base (insert f (B \ {e})) ∧ insert f (B \ {e}) ≠ H
⊢ False
Tactic:
have h1 : H \ {e} ⊆ M.cl (B \ {e})
Proof state after:
case h1
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hB : M.Base B
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ B
h : ∀ f ∈ H \ B, ¬M.Base (insert f (B \ {e})) ∧ insert f (B \ {e}) ≠ H
⊢ H \ {e} ⊆ M.cl (B \ {e})

α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hB : M.Base B
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ B
h : ∀ f ∈ H \ B, ¬M.Base (insert f (B \ {e})) ∧ insert f (B \ {e}) ≠ H
h1 : H \ {e} ⊆ M.cl (B \ {e})
⊢ False
Theorem: Matroid.Base.exists_exchange_of_circuit_of_hyperplane
Proof state before:
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hB : M.Base B
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ B
h : ∀ f ∈ H \ B, ¬M.Base (insert f (B \ {e})) ∧ insert f (B \ {e}) ≠ H
h1 : H \ {e} ⊆ M.cl (B \ {e})
⊢ False
Tactic:
rw [← cl_subset_cl_iff_subset_cl (diff_subset.trans hH.subset_ground),
  hHc.cl_diff_singleton_eq_cl, hH.flat.cl] at h1
Proof state after:
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hB : M.Base B
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ B
h : ∀ f ∈ H \ B, ¬M.Base (insert f (B \ {e})) ∧ insert f (B \ {e}) ≠ H
h1 : H ⊆ M.cl (B \ {e})
⊢ False
Theorem: Matroid.Base.exists_exchange_of_circuit_of_hyperplane
Proof state before:
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hB : M.Base B
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ B
h : ∀ f ∈ H \ B, ¬M.Base (insert f (B \ {e})) ∧ insert f (B \ {e}) ≠ H
h1 : H ⊆ M.cl (B \ {e})
⊢ False
Tactic:
obtain hBH := hH.eq_of_subset (hB.hyperplane_of_cl_diff_singleton he) h1
Proof state after:
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hB : M.Base B
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ B
h : ∀ f ∈ H \ B, ¬M.Base (insert f (B \ {e})) ∧ insert f (B \ {e}) ≠ H
h1 : H ⊆ M.cl (B \ {e})
hBH : H = M.cl (B \ {e})
⊢ False
Theorem: Matroid.Base.exists_exchange_of_circuit_of_hyperplane
Proof state before:
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hB : M.Base B
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ B
h : ∀ f ∈ H \ B, ¬M.Base (insert f (B \ {e})) ∧ insert f (B \ {e}) ≠ H
h1 : H ⊆ M.cl (B \ {e})
hBH : H = M.cl (B \ {e})
⊢ False
Tactic:
have hb : M.Basis (B \ {e}) H
Proof state after:
case hb
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hB : M.Base B
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ B
h : ∀ f ∈ H \ B, ¬M.Base (insert f (B \ {e})) ∧ insert f (B \ {e}) ≠ H
h1 : H ⊆ M.cl (B \ {e})
hBH : H = M.cl (B \ {e})
⊢ M.Basis (B \ {e}) H

α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hB : M.Base B
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ B
h : ∀ f ∈ H \ B, ¬M.Base (insert f (B \ {e})) ∧ insert f (B \ {e}) ≠ H
h1 : H ⊆ M.cl (B \ {e})
hBH : H = M.cl (B \ {e})
hb : M.Basis (B \ {e}) H
⊢ False
Theorem: Matroid.Base.exists_exchange_of_circuit_of_hyperplane
Proof state before:
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hB : M.Base B
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ B
h : ∀ f ∈ H \ B, ¬M.Base (insert f (B \ {e})) ∧ insert f (B \ {e}) ≠ H
h1 : H ⊆ M.cl (B \ {e})
hBH : H = M.cl (B \ {e})
hb : M.Basis (B \ {e}) H
⊢ False
Tactic:
obtain ⟨f, ⟨hfH, hfBe⟩, hfB⟩ := hHc.basis_iff_insert_eq.1 hb
Proof state after:
case intro.intro.intro
α : Type u_1
M : Matroid α
E I H B X : Set α
e f✝ : α
hB : M.Base B
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ B
h : ∀ f ∈ H \ B, ¬M.Base (insert f (B \ {e})) ∧ insert f (B \ {e}) ≠ H
h1 : H ⊆ M.cl (B \ {e})
hBH : H = M.cl (B \ {e})
hb : M.Basis (B \ {e}) H
f : α
hfB : H = insert f (B \ {e})
hfH : f ∈ H
hfBe : f ∉ B \ {e}
⊢ False
Theorem: Matroid.Base.exists_exchange_of_circuit_of_hyperplane
Proof state before:
case intro.intro.intro
α : Type u_1
M : Matroid α
E I H B X : Set α
e f✝ : α
hB : M.Base B
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ B
h : ∀ f ∈ H \ B, ¬M.Base (insert f (B \ {e})) ∧ insert f (B \ {e}) ≠ H
h1 : H ⊆ M.cl (B \ {e})
hBH : H = M.cl (B \ {e})
hb : M.Basis (B \ {e}) H
f : α
hfB : H = insert f (B \ {e})
hfH : f ∈ H
hfBe : f ∉ B \ {e}
⊢ False
Tactic:
refine (h _ ⟨hfH, fun hfB ↦ hfBe ⟨hfB, fun (hfe : f = e) ↦ ?_⟩⟩).2 hfB.symm
Proof state after:
case intro.intro.intro
α : Type u_1
M : Matroid α
E I H B X : Set α
e f✝ : α
hB : M.Base B
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ B
h : ∀ f ∈ H \ B, ¬M.Base (insert f (B \ {e})) ∧ insert f (B \ {e}) ≠ H
h1 : H ⊆ M.cl (B \ {e})
hBH : H = M.cl (B \ {e})
hb : M.Basis (B \ {e}) H
f : α
hfB✝ : H = insert f (B \ {e})
hfH : f ∈ H
hfBe : f ∉ B \ {e}
hfB : f ∈ B
hfe : f = e
⊢ False