Theorem: Matroid.Circuit.basis_iff_eq_diff_singleton (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 \ {e}
Tactic:
refine' ⟨fun h ↦ _, _⟩
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
h : M.Basis I C
⊢ ∃ e ∈ C, I = C \ {e}

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
⊢ (∃ e ∈ C, I = C \ {e}) → M.Basis I C

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
⊢ (∃ e ∈ C, I = C \ {e}) → M.Basis I C
Tactic:
rintro ⟨e, he, rfl⟩
State after:
case refine'_2.intro.intro
α : Type u_1
M : Matroid α
C C' X K C₁ C₂ R : Set α
e✝ f x y : α
hC : M.Circuit C
e : α
he : e ∈ C
⊢ M.Basis (C \ {e}) C

State before:
case refine'_2.intro.intro
α : Type u_1
M : Matroid α
C C' X K C₁ C₂ R : Set α
e✝ f x y : α
hC : M.Circuit C
e : α
he : e ∈ C
⊢ M.Basis (C \ {e}) C
Tactic:
exact hC.diff_singleton_basis he
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
h : M.Basis I C
⊢ ∃ e ∈ C, I = C \ {e}
Tactic:
obtain ⟨e, he⟩ := exists_of_ssubset
  (h.subset.ssubset_of_ne (by rintro rfl; exact hC.dep.not_indep h.indep))
State after:
case refine'_1.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
hC : M.Circuit C
h : M.Basis I C
e : α
he : e ∈ C ∧ e ∉ I
⊢ ∃ e ∈ C, I = C \ {e}

State before:
case refine'_1.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
hC : M.Circuit C
h : M.Basis I C
e : α
he : e ∈ C ∧ e ∉ I
⊢ ∃ e ∈ C, I = C \ {e}
Tactic:
exact ⟨e, he.1, h.eq_of_subset_indep (hC.diff_singleton_indep he.1)
  (subset_diff_singleton h.subset he.2) diff_subset⟩
State after:
no goals

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
h : M.Basis I C
⊢ I ≠ C
Tactic:
rintro rfl
State after:
α : Type u_1
M : Matroid α
C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit I
h : M.Basis I I
⊢ False

State before:
α : Type u_1
M : Matroid α
C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit I
h : M.Basis I I
⊢ False
Tactic:
exact hC.dep.not_indep h.indep
State after:
no goals