refine .inr fun z hzC ↦ ⟨hC.subset_ground hzC, fun (hz : 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}
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