Theorem: Matroid.Circuit.ssubset_indep (Matroid/Circuit.lean)

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
hXC : X ⊂ C
⊢ M.Indep X
Tactic:
rw [← not_dep_iff (hXC.subset.trans hC.subset_ground)]
State after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
hXC : X ⊂ C
⊢ ¬M.Dep X

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
hXC : X ⊂ C
⊢ ¬M.Dep X
Tactic:
exact fun h ↦ hXC.ne ((circuit_iff.1 hC).2 h hXC.subset)
State after:
no goals