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

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
B : Set α
⊢ M✶.RkPos ↔ ∃ C, M.Circuit C
Tactic:
rw [rkPos_iff_empty_not_base, dual_base_iff, diff_empty, not_iff_comm, not_exists,
  ← ground_indep_iff_base, indep_iff_forall_subset_not_circuit]
State after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
B : Set α
⊢ (∀ (x : Set α), ¬M.Circuit x) ↔ ∀ C ⊆ M.E, ¬M.Circuit C

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
B : Set α
⊢ (∀ (x : Set α), ¬M.Circuit x) ↔ ∀ C ⊆ M.E, ¬M.Circuit C
Tactic:
exact ⟨fun h C _ ↦ h C, fun h C hC ↦ h C hC.subset_ground hC⟩
State after:
no goals