Theorem: Matroid.uniqueBaseOn_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 : α
I E X : Set α
⊢ (uniqueBaseOn I E).cl X = X ∩ I ∩ E ∪ E \ I
Tactic:
have hb : (uniqueBaseOn (I ∩ E) E).Basis (X ∩ E ∩ (I ∩ E)) (X ∩ E) :=
  (uniqueBaseOn_basis_iff inter_subset_right inter_subset_right).2 rfl
State after:
α : Type u_1
ι : Type u_2
M : Matroid α
F I✝ J X✝ Y B C R : Set α
e f x y : α
I E X : Set α
hb : (uniqueBaseOn (I ∩ E) E).Basis (X ∩ E ∩ (I ∩ E)) (X ∩ E)
⊢ (uniqueBaseOn I E).cl X = X ∩ I ∩ E ∪ E \ 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 E X : Set α
hb : (uniqueBaseOn (I ∩ E) E).Basis (X ∩ E ∩ (I ∩ E)) (X ∩ E)
⊢ (uniqueBaseOn I E).cl X = X ∩ I ∩ E ∪ E \ I
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 : α
I E X : Set α
hb : (uniqueBaseOn (I ∩ E) E).Basis (X ∩ E ∩ (I ∩ E)) (X ∩ E)
e : α
⊢ e ∈ (uniqueBaseOn I E).cl X ↔ e ∈ X ∩ I ∩ E ∪ E \ I

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 : α
I E X : Set α
hb : (uniqueBaseOn (I ∩ E) E).Basis (X ∩ E ∩ (I ∩ E)) (X ∩ E)
e : α
⊢ e ∈ (uniqueBaseOn I E).cl X ↔ e ∈ X ∩ I ∩ E ∪ E \ I
Tactic:
rw [← uniqueBaseOn_inter_ground_eq I E, ← cl_inter_ground _ X, uniqueBaseOn_ground,
  ← hb.cl_eq_cl, hb.indep.mem_cl_iff, dep_iff, uniqueBaseOn_indep_iff', insert_subset_iff,
  uniqueBaseOn_ground, inter_assoc, inter_self,  and_iff_left inter_subset_right,
  ← inter_inter_distrib_right, inter_assoc, inter_union_distrib_right, inter_comm I,
  inter_union_diff, insert_subset_iff, inter_comm X, inter_assoc,
  and_iff_left inter_subset_left, mem_inter_iff]
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 : α
I E X : Set α
hb : (uniqueBaseOn (I ∩ E) E).Basis (X ∩ E ∩ (I ∩ E)) (X ∩ E)
e : α
⊢ ¬(e ∈ E ∧ e ∈ I) ∧ e ∈ E ∨ e ∈ E ∩ (I ∩ X) ↔ e ∈ (X ∪ E \ I) ∩ 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 : α
I E X : Set α
hb : (uniqueBaseOn (I ∩ E) E).Basis (X ∩ E ∩ (I ∩ E)) (X ∩ E)
e : α
⊢ ¬(e ∈ E ∧ e ∈ I) ∧ e ∈ E ∨ e ∈ E ∩ (I ∩ X) ↔ e ∈ (X ∪ E \ I) ∩ E
Tactic:
simp only [not_and, mem_inter_iff, mem_union, mem_diff]
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 : α
I E X : Set α
hb : (uniqueBaseOn (I ∩ E) E).Basis (X ∩ E ∩ (I ∩ E)) (X ∩ E)
e : α
⊢ (e ∈ E → e ∉ I) ∧ e ∈ E ∨ e ∈ E ∧ e ∈ I ∧ e ∈ X ↔ (e ∈ X ∨ e ∈ E ∧ e ∉ I) ∧ e ∈ 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 : α
I E X : Set α
hb : (uniqueBaseOn (I ∩ E) E).Basis (X ∩ E ∩ (I ∩ E)) (X ∩ E)
e : α
⊢ (e ∈ E → e ∉ I) ∧ e ∈ E ∨ e ∈ E ∧ e ∈ I ∧ e ∈ X ↔ (e ∈ X ∨ e ∈ E ∧ e ∉ I) ∧ e ∈ E
Tactic:
tauto
State after:
no goals