Theorem: Matroid.mem_cl_insert (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 : α
he : e ∉ M.cl X
hef : e ∈ M.cl (insert f X)
⊢ f ∈ M.cl (insert e X)
Tactic:
rw [← cl_inter_ground] at *
State after:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
he : e ∉ M.cl (X ∩ M.E)
hef : e ∈ M.cl (insert f X ∩ M.E)
⊢ f ∈ M.cl (insert e X ∩ M.E)

State before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
he : e ∉ M.cl (X ∩ M.E)
hef : e ∈ M.cl (insert f X ∩ M.E)
⊢ f ∈ M.cl (insert e X ∩ M.E)
Tactic:
have hfE : f ∈ M.E := by
  by_contra! hfE; rw [insert_inter_of_not_mem hfE] at hef; exact he hef
State after:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
he : e ∉ M.cl (X ∩ M.E)
hef : e ∈ M.cl (insert f X ∩ M.E)
hfE : f ∈ M.E
⊢ f ∈ M.cl (insert e X ∩ M.E)

State before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
he : e ∉ M.cl (X ∩ M.E)
hef : e ∈ M.cl (insert f X ∩ M.E)
hfE : f ∈ M.E
⊢ f ∈ M.cl (insert e X ∩ M.E)
Tactic:
have heE : e ∈ M.E := (M.cl_subset_ground _) hef
State after:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
he : e ∉ M.cl (X ∩ M.E)
hef : e ∈ M.cl (insert f X ∩ M.E)
hfE : f ∈ M.E
heE : e ∈ M.E
⊢ f ∈ M.cl (insert e X ∩ M.E)

State before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
he : e ∉ M.cl (X ∩ M.E)
hef : e ∈ M.cl (insert f X ∩ M.E)
hfE : f ∈ M.E
heE : e ∈ M.E
⊢ f ∈ M.cl (insert e X ∩ M.E)
Tactic:
rw [insert_inter_of_mem hfE] at hef
State after:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
he : e ∉ M.cl (X ∩ M.E)
hef : e ∈ M.cl (insert f (X ∩ M.E))
hfE : f ∈ M.E
heE : e ∈ M.E
⊢ f ∈ M.cl (insert e X ∩ M.E)

State before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
he : e ∉ M.cl (X ∩ M.E)
hef : e ∈ M.cl (insert f (X ∩ M.E))
hfE : f ∈ M.E
heE : e ∈ M.E
⊢ f ∈ M.cl (insert e X ∩ M.E)
Tactic:
rw [insert_inter_of_mem heE]
State after:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
he : e ∉ M.cl (X ∩ M.E)
hef : e ∈ M.cl (insert f (X ∩ M.E))
hfE : f ∈ M.E
heE : e ∈ M.E
⊢ f ∈ M.cl (insert e (X ∩ M.E))

State before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
he : e ∉ M.cl (X ∩ M.E)
hef : e ∈ M.cl (insert f (X ∩ M.E))
hfE : f ∈ M.E
heE : e ∈ M.E
⊢ f ∈ M.cl (insert e (X ∩ M.E))
Tactic:
obtain ⟨I, hI⟩ := M.exists_basis (X ∩ M.E)
State after:
case intro
α : Type u_1
ι : Type u_2
M : Matroid α
F I✝ J X Y B C R : Set α
e f x y : α
he : e ∉ M.cl (X ∩ M.E)
hef : e ∈ M.cl (insert f (X ∩ M.E))
hfE : f ∈ M.E
heE : e ∈ M.E
I : Set α
hI : M.Basis I (X ∩ M.E)
⊢ f ∈ M.cl (insert e (X ∩ M.E))

State before:
case intro
α : Type u_1
ι : Type u_2
M : Matroid α
F I✝ J X Y B C R : Set α
e f x y : α
he : e ∉ M.cl (X ∩ M.E)
hef : e ∈ M.cl (insert f (X ∩ M.E))
hfE : f ∈ M.E
heE : e ∈ M.E
I : Set α
hI : M.Basis I (X ∩ M.E)
⊢ f ∈ M.cl (insert e (X ∩ M.E))
Tactic:
rw [← hI.cl_eq_cl, hI.indep.not_mem_cl_iff] at he
State after:
case intro
α : Type u_1
ι : Type u_2
M : Matroid α
F I✝ J X Y B C R : Set α
e f x y : α
hef : e ∈ M.cl (insert f (X ∩ M.E))
hfE : f ∈ M.E
heE : e ∈ M.E
I : Set α
he : M.Indep (insert e I) ∧ e ∉ I
hI : M.Basis I (X ∩ M.E)
⊢ f ∈ M.cl (insert e (X ∩ M.E))

State before:
case intro
α : Type u_1
ι : Type u_2
M : Matroid α
F I✝ J X Y B C R : Set α
e f x y : α
hef : e ∈ M.cl (insert f (X ∩ M.E))
hfE : f ∈ M.E
heE : e ∈ M.E
I : Set α
he : M.Indep (insert e I) ∧ e ∉ I
hI : M.Basis I (X ∩ M.E)
⊢ f ∈ M.cl (insert e (X ∩ M.E))
Tactic:
rw [← cl_insert_cl_eq_cl_insert, ← hI.cl_eq_cl, cl_insert_cl_eq_cl_insert, he.1.mem_cl_iff] at *
State after:
case intro
α : Type u_1
ι : Type u_2
M : Matroid α
F I✝ J X Y B C R : Set α
e f x y : α
hfE : f ∈ M.E
heE : e ∈ M.E
I : Set α
hef : e ∈ M.cl (insert f I)
he : M.Indep (insert e I) ∧ e ∉ I
hI : M.Basis I (X ∩ M.E)
⊢ M.Dep (insert f (insert e I)) ∨ f ∈ insert e I

State before:
case intro
α : Type u_1
ι : Type u_2
M : Matroid α
F I✝ J X Y B C R : Set α
e f x y : α
hfE : f ∈ M.E
heE : e ∈ M.E
I : Set α
hef : e ∈ M.cl (insert f I)
he : M.Indep (insert e I) ∧ e ∉ I
hI : M.Basis I (X ∩ M.E)
⊢ M.Dep (insert f (insert e I)) ∨ f ∈ insert e I
Tactic:
rw [or_iff_not_imp_left, dep_iff, insert_comm,
  and_iff_left (insert_subset heE (insert_subset hfE hI.indep.subset_ground)), not_not]
State after:
case intro
α : Type u_1
ι : Type u_2
M : Matroid α
F I✝ J X Y B C R : Set α
e f x y : α
hfE : f ∈ M.E
heE : e ∈ M.E
I : Set α
hef : e ∈ M.cl (insert f I)
he : M.Indep (insert e I) ∧ e ∉ I
hI : M.Basis I (X ∩ M.E)
⊢ M.Indep (insert e (insert f I)) → f ∈ insert e I

State before:
case intro
α : Type u_1
ι : Type u_2
M : Matroid α
F I✝ J X Y B C R : Set α
e f x y : α
hfE : f ∈ M.E
heE : e ∈ M.E
I : Set α
hef : e ∈ M.cl (insert f I)
he : M.Indep (insert e I) ∧ e ∉ I
hI : M.Basis I (X ∩ M.E)
⊢ M.Indep (insert e (insert f I)) → f ∈ insert e I
Tactic:
intro h
State after:
case intro
α : Type u_1
ι : Type u_2
M : Matroid α
F I✝ J X Y B C R : Set α
e f x y : α
hfE : f ∈ M.E
heE : e ∈ M.E
I : Set α
hef : e ∈ M.cl (insert f I)
he : M.Indep (insert e I) ∧ e ∉ I
hI : M.Basis I (X ∩ M.E)
h : M.Indep (insert e (insert f I))
⊢ f ∈ insert e I

State before:
case intro
α : Type u_1
ι : Type u_2
M : Matroid α
F I✝ J X Y B C R : Set α
e f x y : α
hfE : f ∈ M.E
heE : e ∈ M.E
I : Set α
hef : e ∈ M.cl (insert f I)
he : M.Indep (insert e I) ∧ e ∉ I
hI : M.Basis I (X ∩ M.E)
h : M.Indep (insert e (insert f I))
⊢ f ∈ insert e I
Tactic:
rw [(h.subset (subset_insert _ _)).mem_cl_iff, or_iff_right (h.not_dep), mem_insert_iff,
  or_iff_left he.2] at hef
State after:
case intro
α : Type u_1
ι : Type u_2
M : Matroid α
F I✝ J X Y B C R : Set α
e f x y : α
hfE : f ∈ M.E
heE : e ∈ M.E
I : Set α
hef : e = f
he : M.Indep (insert e I) ∧ e ∉ I
hI : M.Basis I (X ∩ M.E)
h : M.Indep (insert e (insert f I))
⊢ f ∈ insert e I

State before:
case intro
α : Type u_1
ι : Type u_2
M : Matroid α
F I✝ J X Y B C R : Set α
e f x y : α
hfE : f ∈ M.E
heE : e ∈ M.E
I : Set α
hef : e = f
he : M.Indep (insert e I) ∧ e ∉ I
hI : M.Basis I (X ∩ M.E)
h : M.Indep (insert e (insert f I))
⊢ f ∈ insert e I
Tactic:
subst hef
State after:
case intro
α : Type u_1
ι : Type u_2
M : Matroid α
F I✝ J X Y B C R : Set α
e x y : α
heE : e ∈ M.E
I : Set α
he : M.Indep (insert e I) ∧ e ∉ I
hI : M.Basis I (X ∩ M.E)
hfE : e ∈ M.E
h : M.Indep (insert e (insert e I))
⊢ e ∈ insert e I

State before:
case intro
α : Type u_1
ι : Type u_2
M : Matroid α
F I✝ J X Y B C R : Set α
e x y : α
heE : e ∈ M.E
I : Set α
he : M.Indep (insert e I) ∧ e ∉ I
hI : M.Basis I (X ∩ M.E)
hfE : e ∈ M.E
h : M.Indep (insert e (insert e I))
⊢ e ∈ insert e I
Tactic:
apply mem_insert
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 : α
he : e ∉ M.cl (X ∩ M.E)
hef : e ∈ M.cl (insert f X ∩ M.E)
⊢ f ∈ M.E
Tactic:
by_contra! hfE
State after:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
he : e ∉ M.cl (X ∩ M.E)
hef : e ∈ M.cl (insert f X ∩ M.E)
hfE : f ∉ M.E
⊢ False

State before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
he : e ∉ M.cl (X ∩ M.E)
hef : e ∈ M.cl (insert f X ∩ M.E)
hfE : f ∉ M.E
⊢ False
Tactic:
rw [insert_inter_of_not_mem hfE] at hef
State after:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
he : e ∉ M.cl (X ∩ M.E)
hef : e ∈ M.cl (X ∩ M.E)
hfE : f ∉ M.E
⊢ False

State before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
he : e ∉ M.cl (X ∩ M.E)
hef : e ∈ M.cl (X ∩ M.E)
hfE : f ∉ M.E
⊢ False
Tactic:
exact he hef
State after:
no goals