rintro f ⟨rfl | h1 | h2, h⟩
α : Type u_1
β : Type u_2
M N : Matroid α
e✝ f : α
B L L' I X✝ Y Z F C✝ K X : Set α
hK : K ⊆ M✶.cl ∅
e : α
he : e ∈ M.cl (M.cl X ∪ K)
C : Set α
hC : M.Circuit C
heC : e ∈ C
hCss : C ⊆ insert e (M.cl X ∪ K)
⊢ insert e (M.cl X ∪ K) ∩ C ⊆ insert e (M.cl X)
case intro.inl
α : Type u_1
β : Type u_2
M N : Matroid α
e f✝ : α
B L L' I X✝ Y Z F C✝ K X : Set α
hK : K ⊆ M✶.cl ∅
C : Set α
hC : M.Circuit C
f : α
h : f ∈ C
he : f ∈ M.cl (M.cl X ∪ K)
heC : f ∈ C
hCss : C ⊆ insert f (M.cl X ∪ K)
⊢ f ∈ insert f (M.cl X)

case intro.inr.inl
α : Type u_1
β : Type u_2
M N : Matroid α
e✝ f✝ : α
B L L' I X✝ Y Z F C✝ K X : Set α
hK : K ⊆ M✶.cl ∅
e : α
he : e ∈ M.cl (M.cl X ∪ K)
C : Set α
hC : M.Circuit C
heC : e ∈ C
hCss : C ⊆ insert e (M.cl X ∪ K)
f : α
h : f ∈ C
h1 : f ∈ M.cl X
⊢ f ∈ insert e (M.cl X)

case intro.inr.inr
α : Type u_1
β : Type u_2
M N : Matroid α
e✝ f✝ : α
B L L' I X✝ Y Z F C✝ K X : Set α
hK : K ⊆ M✶.cl ∅
e : α
he : e ∈ M.cl (M.cl X ∪ K)
C : Set α
hC : M.Circuit C
heC : e ∈ C
hCss : C ⊆ insert e (M.cl X ∪ K)
f : α
h : f ∈ C
h2 : f ∈ K
⊢ f ∈ insert e (M.cl X)