Theorem: Matroid.Indep.base_of_forall_insert (Matroid/ForMathlib/MatroidBasic.lean)

State before:
α : Type u_1
M : Matroid α
B : Set α
hB : M.Indep B
hBmax : ∀ e ∈ M.E \ B, ¬M.Indep (insert e B)
⊢ M.Base B
Tactic:
refine by_contra fun hnb ↦ ?_
State after:
α : Type u_1
M : Matroid α
B : Set α
hB : M.Indep B
hBmax : ∀ e ∈ M.E \ B, ¬M.Indep (insert e B)
hnb : ¬M.Base B
⊢ False

State before:
α : Type u_1
M : Matroid α
B : Set α
hB : M.Indep B
hBmax : ∀ e ∈ M.E \ B, ¬M.Indep (insert e B)
hnb : ¬M.Base B
⊢ False
Tactic:
obtain ⟨B', hB'⟩ := M.exists_base
State after:
case intro
α : Type u_1
M : Matroid α
B : Set α
hB : M.Indep B
hBmax : ∀ e ∈ M.E \ B, ¬M.Indep (insert e B)
hnb : ¬M.Base B
B' : Set α
hB' : M.Base B'
⊢ False

State before:
case intro
α : Type u_1
M : Matroid α
B : Set α
hB : M.Indep B
hBmax : ∀ e ∈ M.E \ B, ¬M.Indep (insert e B)
hnb : ¬M.Base B
B' : Set α
hB' : M.Base B'
⊢ False
Tactic:
obtain ⟨e, he, h⟩ := hB.exists_insert_of_not_base hnb hB'
State after:
case intro.intro.intro
α : Type u_1
M : Matroid α
B : Set α
hB : M.Indep B
hBmax : ∀ e ∈ M.E \ B, ¬M.Indep (insert e B)
hnb : ¬M.Base B
B' : Set α
hB' : M.Base B'
e : α
he : e ∈ B' \ B
h : M.Indep (insert e B)
⊢ False

State before:
case intro.intro.intro
α : Type u_1
M : Matroid α
B : Set α
hB : M.Indep B
hBmax : ∀ e ∈ M.E \ B, ¬M.Indep (insert e B)
hnb : ¬M.Base B
B' : Set α
hB' : M.Base B'
e : α
he : e ∈ B' \ B
h : M.Indep (insert e B)
⊢ False
Tactic:
exact hBmax e ⟨hB'.subset_ground he.1, he.2⟩ h
State after:
no goals