Theorem: Matroid.indep_iff_not_mem_cl_diff_forall (Matroid/Closure.lean)

State before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
hI : autoParam (I ⊆ M.E) _auto✝
⊢ M.Indep I ↔ ∀ e ∈ I, e ∉ M.cl (I \ {e})
Tactic:
use fun h e heI he ↦ ((h.cl_inter_eq_self_of_subset diff_subset).subset ⟨he, heI⟩).2 rfl
State after:
case mpr
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
hI : autoParam (I ⊆ M.E) _auto✝
⊢ (∀ e ∈ I, e ∉ M.cl (I \ {e})) → M.Indep I

State before:
case mpr
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
hI : autoParam (I ⊆ M.E) _auto✝
⊢ (∀ e ∈ I, e ∉ M.cl (I \ {e})) → M.Indep I
Tactic:
intro h
State after:
case mpr
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
hI : autoParam (I ⊆ M.E) _auto✝
h : ∀ e ∈ I, e ∉ M.cl (I \ {e})
⊢ M.Indep I

State before:
case mpr
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
hI : autoParam (I ⊆ M.E) _auto✝
h : ∀ e ∈ I, e ∉ M.cl (I \ {e})
⊢ M.Indep I
Tactic:
obtain ⟨J, hJ⟩ := M.exists_basis I
State after:
case mpr.intro
α : Type u_1
ι : Type u_2
M : Matroid α
F I J✝ X Y B C R : Set α
e f x y : α
hI : autoParam (I ⊆ M.E) _auto✝
h : ∀ e ∈ I, e ∉ M.cl (I \ {e})
J : Set α
hJ : M.Basis J I
⊢ M.Indep I

State before:
case mpr.intro
α : Type u_1
ι : Type u_2
M : Matroid α
F I J✝ X Y B C R : Set α
e f x y : α
hI : autoParam (I ⊆ M.E) _auto✝
h : ∀ e ∈ I, e ∉ M.cl (I \ {e})
J : Set α
hJ : M.Basis J I
⊢ M.Indep I
Tactic:
convert hJ.indep
State after:
case h.e'_3
α : Type u_1
ι : Type u_2
M : Matroid α
F I J✝ X Y B C R : Set α
e f x y : α
hI : autoParam (I ⊆ M.E) _auto✝
h : ∀ e ∈ I, e ∉ M.cl (I \ {e})
J : Set α
hJ : M.Basis J I
⊢ I = J

State before:
case h.e'_3
α : Type u_1
ι : Type u_2
M : Matroid α
F I J✝ X Y B C R : Set α
e f x y : α
hI : autoParam (I ⊆ M.E) _auto✝
h : ∀ e ∈ I, e ∉ M.cl (I \ {e})
J : Set α
hJ : M.Basis J I
⊢ I = J
Tactic:
refine' hJ.subset.antisymm' (fun e he ↦ by_contra fun heJ ↦ h _ he _)
State after:
case h.e'_3
α : Type u_1
ι : Type u_2
M : Matroid α
F I J✝ X Y B C R : Set α
e✝ f x y : α
hI : autoParam (I ⊆ M.E) _auto✝
h : ∀ e ∈ I, e ∉ M.cl (I \ {e})
J : Set α
hJ : M.Basis J I
e : α
he : e ∈ I
heJ : e ∉ J
⊢ e ∈ M.cl (I \ {e})

State before:
case h.e'_3
α : Type u_1
ι : Type u_2
M : Matroid α
F I J✝ X Y B C R : Set α
e✝ f x y : α
hI : autoParam (I ⊆ M.E) _auto✝
h : ∀ e ∈ I, e ∉ M.cl (I \ {e})
J : Set α
hJ : M.Basis J I
e : α
he : e ∈ I
heJ : e ∉ J
⊢ e ∈ M.cl (I \ {e})
Tactic:
exact mem_of_mem_of_subset
  (hJ.subset_cl he) (M.cl_subset_cl (subset_diff_singleton hJ.subset heJ))
State after:
no goals