Theorem: Matroid.connected_iff_not_exists_tutteSep (Matroid/Connectivity.lean)

State before:
α : Type u_1
M : Matroid α
k : ℕ
P : Set α → Prop
a b : α
inst✝ : M.Nonempty
⊢ M.Connected ↔ ¬∃ P, P.IsTutteSep 1
Tactic:
rw [iff_not_comm]
State after:
α : Type u_1
M : Matroid α
k : ℕ
P : Set α → Prop
a b : α
inst✝ : M.Nonempty
⊢ (∃ P, P.IsTutteSep 1) ↔ ¬M.Connected

State before:
α : Type u_1
M : Matroid α
k : ℕ
P : Set α → Prop
a b : α
inst✝ : M.Nonempty
⊢ (∃ P, P.IsTutteSep 1) ↔ ¬M.Connected
Tactic:
simp only [Connected, show M.Nonempty by assumption, true_and, not_forall, Classical.not_imp,
  exists_and_left, exists_prop, exists_and_left, Partition.IsTutteSep, Nat.cast_one,
  ENat.lt_one_iff, one_le_encard_iff_nonempty]
State after:
α : Type u_1
M : Matroid α
k : ℕ
P : Set α → Prop
a b : α
inst✝ : M.Nonempty
⊢ (∃ P, P.conn = 0 ∧ P.left.Nonempty ∧ P.right.Nonempty) ↔ ∃ x, ∃ x_1 ∈ M.E, x ∈ M.E ∧ ¬M.ConnectedTo x x_1

State before:
α : Type u_1
M : Matroid α
k : ℕ
P : Set α → Prop
a b : α
inst✝ : M.Nonempty
⊢ (∃ P, P.conn = 0 ∧ P.left.Nonempty ∧ P.right.Nonempty) ↔ ∃ x, ∃ x_1 ∈ M.E, x ∈ M.E ∧ ¬M.ConnectedTo x x_1
Tactic:
simp only [Partition.conn_eq_zero_iff, and_self,
  skew_iff_forall_circuit (Partition.disjoint _) (Partition.left_subset_ground _)
    (Partition.right_subset_ground _)]
State after:
α : 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

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⟩ ↦ ?_⟩
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

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]⟩⟩
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

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]
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}

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 -
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}

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
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}

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
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}

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) ↦ ?_⟩
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

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
State after:
no goals

State before:
α : Type u_1
M : Matroid α
k : ℕ
P : Set α → Prop
a b : α
inst✝ : M.Nonempty
⊢ M.Nonempty
Tactic:
assumption
State after:
no goals

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
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

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
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

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 ↦ ?_⟩
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

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)
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

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)
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

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
State after:
no goals

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]
State after:
no goals

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]
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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]
State after:
no goals

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 )
State after:
no goals