Theorem: Matroid.Circuit.basis_iff_insert_eq (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
⊢ M.Basis I C ↔ ∃ e ∈ C \ I, C = insert e I
Tactic:
rw [hC.basis_iff_eq_diff_singleton]
State after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
⊢ (∃ e ∈ C, I = C \ {e}) ↔ ∃ e ∈ C \ I, C = insert e I

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
⊢ (∃ e ∈ C, I = C \ {e}) ↔ ∃ e ∈ C \ I, C = insert e I
Tactic:
refine' ⟨fun ⟨e, he, hI⟩ ↦ ⟨e, ⟨he, fun heI ↦ (hI.subset heI).2 rfl⟩, _⟩,
  fun ⟨e, he, hC⟩ ↦ ⟨e, he.1, _⟩⟩
State after:
case refine'_1
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
hC : M.Circuit C
x✝ : ∃ e ∈ C, I = C \ {e}
e : α
he : e ∈ C
hI : I = C \ {e}
⊢ C = insert e I

case refine'_2
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
hC✝ : M.Circuit C
x✝ : ∃ e ∈ C \ I, C = insert e I
e : α
he : e ∈ C \ I
hC : C = insert e I
⊢ I = C \ {e}

State before:
case refine'_2
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
hC✝ : M.Circuit C
x✝ : ∃ e ∈ C \ I, C = insert e I
e : α
he : e ∈ C \ I
hC : C = insert e I
⊢ I = C \ {e}
Tactic:
rw [hC, insert_diff_self_of_not_mem he.2]
State after:
no goals

State before:
case refine'_1
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
hC : M.Circuit C
x✝ : ∃ e ∈ C, I = C \ {e}
e : α
he : e ∈ C
hI : I = C \ {e}
⊢ C = insert e I
Tactic:
rw [hI, insert_diff_singleton, insert_eq_of_mem he]
State after:
no goals