Theorem: Matroid.circuitOn_indep_iff (Matroid/Constructions/Truncate.lean)

State before:
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C : Set α
hC : C.Nonempty
⊢ (circuitOn C).Indep I ↔ I ⊂ C
Tactic:
have := freeOn_rkPos hC
State after:
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C : Set α
hC : C.Nonempty
this : (freeOn C).RkPos
⊢ (circuitOn C).Indep I ↔ I ⊂ C

State before:
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C : Set α
hC : C.Nonempty
this : (freeOn C).RkPos
⊢ (circuitOn C).Indep I ↔ I ⊂ C
Tactic:
simp [circuitOn, truncate_indep_iff, ssubset_iff_subset_ne]
State after:
no goals