Theorem: Matroid.Indep.rev_exchange_indep_iff (Matroid/Circuit.lean)

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
I₁ I₂ B₁ B₂ : Set α
hI : M.Indep I
he : e ∈ M.cl I \ I
⊢ M.Indep (insert e I \ {f}) ↔ f ∈ M.fundCct e I
Tactic:
simp_rw [indep_iff_forall_subset_not_circuit', and_iff_left (diff_subset.trans
  (insert_subset ((M.cl_subset_ground I) he.1) hI.subset_ground)), imp_not_comm, subset_diff,
  disjoint_singleton_right, not_and, not_not]
State after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
I₁ I₂ B₁ B₂ : Set α
hI : M.Indep I
he : e ∈ M.cl I \ I
⊢ (∀ (C : Set α), M.Circuit C → C ⊆ insert e I → f ∈ C) ↔ f ∈ M.fundCct e I

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
I₁ I₂ B₁ B₂ : Set α
hI : M.Indep I
he : e ∈ M.cl I \ I
⊢ (∀ (C : Set α), M.Circuit C → C ⊆ insert e I → f ∈ C) ↔ f ∈ M.fundCct e I
Tactic:
exact ⟨fun h ↦ h _ (hI.fundCct_circuit he) (fundCct_subset_insert _ _),
  fun h C hC hCeI ↦ by rwa [hC.eq_fundCct_of_subset_insert_indep hI hCeI]⟩
State after:
no goals

State before:
α : Type u_1
M : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e f x y : α
I₁ I₂ B₁ B₂ : Set α
hI : M.Indep I
he : e ∈ M.cl I \ I
h : f ∈ M.fundCct e I
C : Set α
hC : M.Circuit C
hCeI : C ⊆ insert e I
⊢ f ∈ C
Tactic:
rwa [hC.eq_fundCct_of_subset_insert_indep hI hCeI]
State after:
no goals