Theorem: Matroid.indep_iff_cl_ssubset_ssubset_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 ↔ ∀ J ⊂ I, M.cl J ⊂ 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 : α
hI : autoParam (I ⊆ M.E) _auto✝
⊢ (∀ e ∈ I, e ∉ M.cl (I \ {e})) ↔ ∀ J ⊂ I, M.cl J ⊂ 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 : α
hI : autoParam (I ⊆ M.E) _auto✝
⊢ (∀ e ∈ I, e ∉ M.cl (I \ {e})) ↔ ∀ J ⊂ I, M.cl J ⊂ M.cl I
Tactic:
refine' ⟨fun h J hJI ↦ (M.cl_subset_cl hJI.subset).ssubset_of_ne (fun h_eq ↦ _),
  fun h e heI hin ↦ _⟩
State after:
case refine'_1
α : 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 α
hJI : J ⊂ I
h_eq : M.cl J = M.cl I
⊢ False

case refine'_2
α : 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 : ∀ J ⊂ I, M.cl J ⊂ M.cl I
e : α
heI : e ∈ I
hin : e ∈ M.cl (I \ {e})
⊢ False

State before:
case refine'_2
α : 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 : ∀ J ⊂ I, M.cl J ⊂ M.cl I
e : α
heI : e ∈ I
hin : e ∈ M.cl (I \ {e})
⊢ False
Tactic:
refine' (h (I \ {e}) (diff_singleton_sSubset.2 heI)).ne _
State after:
case refine'_2
α : 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 : ∀ J ⊂ I, M.cl J ⊂ M.cl I
e : α
heI : e ∈ I
hin : e ∈ M.cl (I \ {e})
⊢ M.cl (I \ {e}) = M.cl I

State before:
case refine'_2
α : 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 : ∀ J ⊂ I, M.cl J ⊂ M.cl I
e : α
heI : e ∈ I
hin : e ∈ M.cl (I \ {e})
⊢ M.cl (I \ {e}) = M.cl I
Tactic:
rw [← cl_cl, ← insert_eq_of_mem hin, cl_insert_cl_eq_cl_insert, insert_diff_singleton,
  insert_eq_of_mem heI]
State after:
no goals

State before:
case refine'_1
α : 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 α
hJI : J ⊂ I
h_eq : M.cl J = M.cl I
⊢ False
Tactic:
obtain ⟨e,heJ,h'⟩ := ssubset_iff_insert.1 hJI
State after:
case refine'_1.intro.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 α
hJI : J ⊂ I
h_eq : M.cl J = M.cl I
e : α
heJ : e ∉ J
h' : insert e J ⊆ I
⊢ False

State before:
case refine'_1.intro.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 α
hJI : J ⊂ I
h_eq : M.cl J = M.cl I
e : α
heJ : e ∉ J
h' : insert e J ⊆ I
⊢ False
Tactic:
apply h e (h' (mem_insert _ _))
State after:
case refine'_1.intro.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 α
hJI : J ⊂ I
h_eq : M.cl J = M.cl I
e : α
heJ : e ∉ J
h' : insert e J ⊆ I
⊢ e ∈ M.cl (I \ {e})

State before:
case refine'_1.intro.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 α
hJI : J ⊂ I
h_eq : M.cl J = M.cl I
e : α
heJ : e ∉ J
h' : insert e J ⊆ I
⊢ e ∈ M.cl (I \ {e})
Tactic:
have heI := M.mem_cl_of_mem (h' (mem_insert e J))
State after:
case refine'_1.intro.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 α
hJI : J ⊂ I
h_eq : M.cl J = M.cl I
e : α
heJ : e ∉ J
h' : insert e J ⊆ I
heI : e ∈ M.cl I
⊢ e ∈ M.cl (I \ {e})

State before:
case refine'_1.intro.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 α
hJI : J ⊂ I
h_eq : M.cl J = M.cl I
e : α
heJ : e ∉ J
h' : insert e J ⊆ I
heI : e ∈ M.cl I
⊢ e ∈ M.cl (I \ {e})
Tactic:
rw [← h_eq] at heI
State after:
case refine'_1.intro.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 α
hJI : J ⊂ I
h_eq : M.cl J = M.cl I
e : α
heJ : e ∉ J
h' : insert e J ⊆ I
heI : e ∈ M.cl J
⊢ e ∈ M.cl (I \ {e})

State before:
case refine'_1.intro.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 α
hJI : J ⊂ I
h_eq : M.cl J = M.cl I
e : α
heJ : e ∉ J
h' : insert e J ⊆ I
heI : e ∈ M.cl J
⊢ e ∈ M.cl (I \ {e})
Tactic:
refine' mem_of_mem_of_subset heI (M.cl_subset_cl _)
State after:
case refine'_1.intro.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 α
hJI : J ⊂ I
h_eq : M.cl J = M.cl I
e : α
heJ : e ∉ J
h' : insert e J ⊆ I
heI : e ∈ M.cl J
⊢ J ⊆ I \ {e}

State before:
case refine'_1.intro.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 α
hJI : J ⊂ I
h_eq : M.cl J = M.cl I
e : α
heJ : e ∉ J
h' : insert e J ⊆ I
heI : e ∈ M.cl J
⊢ J ⊆ I \ {e}
Tactic:
rw [subset_diff, disjoint_singleton_right, and_iff_left heJ]
State after:
case refine'_1.intro.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 α
hJI : J ⊂ I
h_eq : M.cl J = M.cl I
e : α
heJ : e ∉ J
h' : insert e J ⊆ I
heI : e ∈ M.cl J
⊢ J ⊆ I

State before:
case refine'_1.intro.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 α
hJI : J ⊂ I
h_eq : M.cl J = M.cl I
e : α
heJ : e ∉ J
h' : insert e J ⊆ I
heI : e ∈ M.cl J
⊢ J ⊆ I
Tactic:
exact (subset_insert _ _).trans h'
State after:
no goals