obtain (hzY | ⟨C', hC', hzC', hCzY⟩) := (mem_cl_iff_mem_or_exists_circuit hYE).mp h₄
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x✝ y : α
ι : Type u_2
hC : M.Circuit C
x : ι → α
Cs : ι → Set α
hCs : ∀ (i : ι), M.Circuit (Cs i)
h_mem : ∀ (i : ι), x i ∈ C ∩ Cs i
h_unique : ∀ (i i' : ι), x i ∈ Cs i' → i = i'
z : α
hz : z ∈ C \ ⋃ i, Cs i
Y : Set α := (C ∪ ⋃ x, Cs x) \ insert z (range x)
hY : Y = (C ∪ ⋃ x, Cs x) \ insert z (range x)
hYE : Y ⊆ M.E
h₁ : range x ⊆ M.cl (⋃ i, (Cs i \ {x i}) \ insert z (range x))
h₂ : range x ⊆ M.cl Y
h₃ : M.cl (C \ {z}) ⊆ M.cl Y
h₄ : z ∈ M.cl Y
⊢ ∃ C', M.Circuit C' ∧ z ∈ C' ∧ C' ⊆ (C ∪ ⋃ i, Cs i) \ range x
case inl
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x✝ y : α
ι : Type u_2
hC : M.Circuit C
x : ι → α
Cs : ι → Set α
hCs : ∀ (i : ι), M.Circuit (Cs i)
h_mem : ∀ (i : ι), x i ∈ C ∩ Cs i
h_unique : ∀ (i i' : ι), x i ∈ Cs i' → i = i'
z : α
hz : z ∈ C \ ⋃ i, Cs i
Y : Set α := (C ∪ ⋃ x, Cs x) \ insert z (range x)
hY : Y = (C ∪ ⋃ x, Cs x) \ insert z (range x)
hYE : Y ⊆ M.E
h₁ : range x ⊆ M.cl (⋃ i, (Cs i \ {x i}) \ insert z (range x))
h₂ : range x ⊆ M.cl Y
h₃ : M.cl (C \ {z}) ⊆ M.cl Y
h₄ : z ∈ M.cl Y
hzY : z ∈ Y
⊢ ∃ C', M.Circuit C' ∧ z ∈ C' ∧ C' ⊆ (C ∪ ⋃ i, Cs i) \ range x

case inr.intro.intro.intro
α : Type u_1
M : Matroid α
C C'✝ I X K C₁ C₂ R : Set α
e f x✝ y : α
ι : Type u_2
hC : M.Circuit C
x : ι → α
Cs : ι → Set α
hCs : ∀ (i : ι), M.Circuit (Cs i)
h_mem : ∀ (i : ι), x i ∈ C ∩ Cs i
h_unique : ∀ (i i' : ι), x i ∈ Cs i' → i = i'
z : α
hz : z ∈ C \ ⋃ i, Cs i
Y : Set α := (C ∪ ⋃ x, Cs x) \ insert z (range x)
hY : Y = (C ∪ ⋃ x, Cs x) \ insert z (range x)
hYE : Y ⊆ M.E
h₁ : range x ⊆ M.cl (⋃ i, (Cs i \ {x i}) \ insert z (range x))
h₂ : range x ⊆ M.cl Y
h₃ : M.cl (C \ {z}) ⊆ M.cl Y
h₄ : z ∈ M.cl Y
C' : Set α
hC' : M.Circuit C'
hzC' : z ∈ C'
hCzY : C' ⊆ insert z Y
⊢ ∃ C', M.Circuit C' ∧ z ∈ C' ∧ C' ⊆ (C ∪ ⋃ i, Cs i) \ range x