Theorem: Matroid.indep_iff_cl_diff_ne_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 : α
⊢ M.Indep I ↔ ∀ e ∈ I, M.cl (I \ {e}) ≠ M.cl I
Tactic:
rw [indep_iff_not_mem_cl_diff_forall']
State after:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
⊢ (I ⊆ M.E ∧ ∀ e ∈ I, e ∉ M.cl (I \ {e})) ↔ ∀ e ∈ I, M.cl (I \ {e}) ≠ M.cl I

State before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
⊢ (I ⊆ M.E ∧ ∀ e ∈ I, e ∉ M.cl (I \ {e})) ↔ ∀ e ∈ I, M.cl (I \ {e}) ≠ M.cl I
Tactic:
refine' ⟨fun ⟨hIE, h⟩ e heI h_eq ↦ h e heI (h_eq.symm.subset (M.mem_cl_of_mem heI)),
  fun h ↦ ⟨fun e heI ↦ by_contra fun heE ↦ h e heI _,fun e heI hin ↦ h e heI
    (by rw [cl_diff_singleton_eq_cl hin])⟩⟩
State after:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e✝ f x y : α
h : ∀ e ∈ I, M.cl (I \ {e}) ≠ M.cl I
e : α
heI : e ∈ I
heE : e ∉ M.E
⊢ M.cl (I \ {e}) = M.cl I

State before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e✝ f x y : α
h : ∀ e ∈ I, M.cl (I \ {e}) ≠ M.cl I
e : α
heI : e ∈ I
heE : e ∉ M.E
⊢ M.cl (I \ {e}) = M.cl I
Tactic:
rw [← cl_inter_ground, inter_comm, inter_diff_distrib_left,
  inter_singleton_eq_empty.mpr heE, diff_empty, inter_comm, cl_inter_ground]
State after:
no goals

State before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e✝ f x y : α
h : ∀ e ∈ I, M.cl (I \ {e}) ≠ M.cl I
e : α
heI : e ∈ I
hin : e ∈ M.cl (I \ {e})
⊢ M.cl (I \ {e}) = M.cl I
Tactic:
rw [cl_diff_singleton_eq_cl hin]
State after:
no goals