Theorem: Matroid.Circuit.diff_singleton_basis (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
he : e ∈ C
⊢ M.Basis (C \ {e}) C
Tactic:
nth_rw 2 [← insert_eq_of_mem he]
State after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
he : e ∈ C
⊢ M.Basis (C \ {e}) (insert e C)

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
he : e ∈ C
⊢ M.Basis (C \ {e}) (insert e C)
Tactic:
rw [← insert_diff_singleton, (hC.diff_singleton_indep he).basis_insert_iff,
  insert_diff_singleton, insert_eq_of_mem he]
State after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
he : e ∈ C
⊢ M.Dep C ∨ e ∈ C \ {e}

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
he : e ∈ C
⊢ M.Dep C ∨ e ∈ C \ {e}
Tactic:
exact Or.inl hC.dep
State after:
no goals