Theorem: Matroid.restrict_cl_eq' (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 : Matroid α
X R : Set α
⊢ (M ↾ R).cl X = M.cl (X ∩ R) ∩ R ∪ R \ M.E
Tactic:
rw [← cl_inter_ground, restrict_ground_eq]
State after:
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I J X✝ Y B C R✝ : Set α
e f x y : α
M : Matroid α
X R : Set α
⊢ (M ↾ R).cl (X ∩ R) = M.cl (X ∩ R) ∩ R ∪ R \ 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 : α
M : Matroid α
X R : Set α
⊢ (M ↾ R).cl (X ∩ R) = M.cl (X ∩ R) ∩ R ∪ R \ M.E
Tactic:
ext e
State after:
case h
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I J X✝ Y B C R✝ : Set α
e✝ f x y : α
M : Matroid α
X R : Set α
e : α
⊢ e ∈ (M ↾ R).cl (X ∩ R) ↔ e ∈ M.cl (X ∩ R) ∩ R ∪ R \ M.E

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

State before:
case h.intro
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X✝ Y B C R✝ : Set α
e✝ f x y : α
M : Matroid α
X R : Set α
e : α
I : Set α
hI : (M ↾ R).Basis I (X ∩ R)
⊢ e ∈ (M ↾ R).cl (X ∩ R) ↔ e ∈ M.cl (X ∩ R) ∩ R ∪ R \ M.E
Tactic:
have hI' := (basis_restrict_iff'.mp hI).1
State after:
case h.intro
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X✝ Y B C R✝ : Set α
e✝ f x y : α
M : Matroid α
X R : Set α
e : α
I : Set α
hI : (M ↾ R).Basis I (X ∩ R)
hI' : M.Basis I (X ∩ R ∩ M.E)
⊢ e ∈ (M ↾ R).cl (X ∩ R) ↔ e ∈ M.cl (X ∩ R) ∩ R ∪ R \ M.E

State before:
case h.intro
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X✝ Y B C R✝ : Set α
e✝ f x y : α
M : Matroid α
X R : Set α
e : α
I : Set α
hI : (M ↾ R).Basis I (X ∩ R)
hI' : M.Basis I (X ∩ R ∩ M.E)
⊢ e ∈ (M ↾ R).cl (X ∩ R) ↔ e ∈ M.cl (X ∩ R) ∩ R ∪ R \ M.E
Tactic:
rw [← hI.cl_eq_cl, ← M.cl_inter_ground (X ∩ R), ← hI'.cl_eq_cl, mem_union, mem_inter_iff,
  hI'.indep.mem_cl_iff, hI.indep.mem_cl_iff, restrict_dep_iff, insert_subset_iff,
  dep_iff, insert_subset_iff, and_iff_left hI'.indep.subset_ground, mem_diff,
  and_iff_left (show I ⊆ R from hI.indep.subset_ground)]
State after:
case h.intro
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X✝ Y B C R✝ : Set α
e✝ f x y : α
M : Matroid α
X R : Set α
e : α
I : Set α
hI : (M ↾ R).Basis I (X ∩ R)
hI' : M.Basis I (X ∩ R ∩ M.E)
⊢ ¬M.Indep (insert e I) ∧ e ∈ R ∨ e ∈ I ↔ (¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I) ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E

State before:
case h.intro
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X✝ Y B C R✝ : Set α
e✝ f x y : α
M : Matroid α
X R : Set α
e : α
I : Set α
hI : (M ↾ R).Basis I (X ∩ R)
hI' : M.Basis I (X ∩ R ∩ M.E)
⊢ ¬M.Indep (insert e I) ∧ e ∈ R ∨ e ∈ I ↔ (¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I) ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
Tactic:
have hIR : I ⊆ R := hI.indep.subset_ground
State after:
case h.intro
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X✝ Y B C R✝ : Set α
e✝ f x y : α
M : Matroid α
X R : Set α
e : α
I : Set α
hI : (M ↾ R).Basis I (X ∩ R)
hI' : M.Basis I (X ∩ R ∩ M.E)
hIR : I ⊆ R
⊢ ¬M.Indep (insert e I) ∧ e ∈ R ∨ e ∈ I ↔ (¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I) ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E

State before:
case h.intro
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X✝ Y B C R✝ : Set α
e✝ f x y : α
M : Matroid α
X R : Set α
e : α
I : Set α
hI : (M ↾ R).Basis I (X ∩ R)
hI' : M.Basis I (X ∩ R ∩ M.E)
hIR : I ⊆ R
⊢ ¬M.Indep (insert e I) ∧ e ∈ R ∨ e ∈ I ↔ (¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I) ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
Tactic:
by_cases he : e ∈ M.E
State after:
case pos
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X✝ Y B C R✝ : Set α
e✝ f x y : α
M : Matroid α
X R : Set α
e : α
I : Set α
hI : (M ↾ R).Basis I (X ∩ R)
hI' : M.Basis I (X ∩ R ∩ M.E)
hIR : I ⊆ R
he : e ∈ M.E
⊢ ¬M.Indep (insert e I) ∧ e ∈ R ∨ e ∈ I ↔ (¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I) ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E

case neg
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X✝ Y B C R✝ : Set α
e✝ f x y : α
M : Matroid α
X R : Set α
e : α
I : Set α
hI : (M ↾ R).Basis I (X ∩ R)
hI' : M.Basis I (X ∩ R ∩ M.E)
hIR : I ⊆ R
he : e ∉ M.E
⊢ ¬M.Indep (insert e I) ∧ e ∈ R ∨ e ∈ I ↔ (¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I) ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E

State before:
case pos
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X✝ Y B C R✝ : Set α
e✝ f x y : α
M : Matroid α
X R : Set α
e : α
I : Set α
hI : (M ↾ R).Basis I (X ∩ R)
hI' : M.Basis I (X ∩ R ∩ M.E)
hIR : I ⊆ R
he : e ∈ M.E
⊢ ¬M.Indep (insert e I) ∧ e ∈ R ∨ e ∈ I ↔ (¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I) ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E

case neg
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X✝ Y B C R✝ : Set α
e✝ f x y : α
M : Matroid α
X R : Set α
e : α
I : Set α
hI : (M ↾ R).Basis I (X ∩ R)
hI' : M.Basis I (X ∩ R ∩ M.E)
hIR : I ⊆ R
he : e ∉ M.E
⊢ ¬M.Indep (insert e I) ∧ e ∈ R ∨ e ∈ I ↔ (¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I) ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
Tactic:
aesop
State after:
case neg
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X✝ Y B C R✝ : Set α
e✝ f x y : α
M : Matroid α
X R : Set α
e : α
I : Set α
hI : (M ↾ R).Basis I (X ∩ R)
hI' : M.Basis I (X ∩ R ∩ M.E)
hIR : I ⊆ R
he : e ∉ M.E
⊢ ¬M.Indep (insert e I) ∧ e ∈ R ∨ e ∈ I ↔ (¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I) ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E

State before:
case neg
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X✝ Y B C R✝ : Set α
e✝ f x y : α
M : Matroid α
X R : Set α
e : α
I : Set α
hI : (M ↾ R).Basis I (X ∩ R)
hI' : M.Basis I (X ∩ R ∩ M.E)
hIR : I ⊆ R
he : e ∉ M.E
⊢ ¬M.Indep (insert e I) ∧ e ∈ R ∨ e ∈ I ↔ (¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I) ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
Tactic:
simp only [iff_false_intro he, and_false, false_or, and_true, ← mem_inter_iff, ← mem_union,
  inter_eq_self_of_subset_left hIR, union_comm I, and_iff_right
    (show ¬M.Indep (insert e I) from fun hi ↦ he (hi.subset_ground (mem_insert _ _))),
  not_false_iff]
State after:
no goals