Theorem: Matroid.Basis.rev_exchange (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.Basis I₁ X
hI₂ : M.Basis I₂ X
he : e ∈ I₁ \ I₂
⊢ ∀ (a : α),
    a ∈ I₂ \ I₁ ∧ M.Basis (insert e I₂ \ {a}) X ∧ M.Basis (insert a I₁ \ {e}) X →
      a ∈ I₂ \ I₁ ∧ M.Basis (insert e I₂ \ {a}) X
Tactic:
simp only [mem_diff, mem_insert_iff, mem_singleton_iff]
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.Basis I₁ X
hI₂ : M.Basis I₂ X
he : e ∈ I₁ \ I₂
⊢ ∀ (a : α),
    (a ∈ I₂ ∧ a ∉ I₁) ∧ M.Basis (insert e I₂ \ {a}) X ∧ M.Basis (insert a I₁ \ {e}) X →
      (a ∈ I₂ ∧ a ∉ I₁) ∧ M.Basis (insert e I₂ \ {a}) X

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.Basis I₁ X
hI₂ : M.Basis I₂ X
he : e ∈ I₁ \ I₂
⊢ ∀ (a : α),
    (a ∈ I₂ ∧ a ∉ I₁) ∧ M.Basis (insert e I₂ \ {a}) X ∧ M.Basis (insert a I₁ \ {e}) X →
      (a ∈ I₂ ∧ a ∉ I₁) ∧ M.Basis (insert e I₂ \ {a}) X
Tactic:
tauto
State after:
no goals