Theorem: Matroid.Indep.cl_eq_setOf_basis_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 : α
hI : M.Indep I
⊢ M.cl I = {x | M.Basis I (insert x I)}
Tactic:
set F := {x | M.Basis I (insert x I)}
State after:
α : Type u_1
ι : Type u_2
M : Matroid α
F✝ I J X Y B C R : Set α
e f x y : α
hI : M.Indep I
F : Set α := {x | M.Basis I (insert x I)}
⊢ M.cl I = F

State before:
α : Type u_1
ι : Type u_2
M : Matroid α
F✝ I J X Y B C R : Set α
e f x y : α
hI : M.Indep I
F : Set α := {x | M.Basis I (insert x I)}
⊢ M.cl I = F
Tactic:
have hIF : M.Basis I F := hI.basis_setOf_insert_basis
State after:
α : Type u_1
ι : Type u_2
M : Matroid α
F✝ I J X Y B C R : Set α
e f x y : α
hI : M.Indep I
F : Set α := {x | M.Basis I (insert x I)}
hIF : M.Basis I F
⊢ M.cl I = F

State before:
α : Type u_1
ι : Type u_2
M : Matroid α
F✝ I J X Y B C R : Set α
e f x y : α
hI : M.Indep I
F : Set α := {x | M.Basis I (insert x I)}
hIF : M.Basis I F
⊢ M.cl I = F
Tactic:
have hF : M.Flat F := by
  refine' ⟨fun J X hJF hJX e heX ↦ (_ : M.Basis _ _), hIF.subset_ground⟩
  exact (hIF.basis_of_basis_of_subset_of_subset (hJX.basis_union hJF) hJF.subset
    (hIF.subset.trans subset_union_right)).basis_subset (subset_insert _ _)
    (insert_subset (Or.inl heX) (hIF.subset.trans subset_union_right))
State after:
α : Type u_1
ι : Type u_2
M : Matroid α
F✝ I J X Y B C R : Set α
e f x y : α
hI : M.Indep I
F : Set α := {x | M.Basis I (insert x I)}
hIF : M.Basis I F
hF : M.Flat F
⊢ M.cl I = F

State before:
α : Type u_1
ι : Type u_2
M : Matroid α
F✝ I J X Y B C R : Set α
e f x y : α
hI : M.Indep I
F : Set α := {x | M.Basis I (insert x I)}
hIF : M.Basis I F
hF : M.Flat F
⊢ M.cl I = F
Tactic:
rw [subset_antisymm_iff, cl_def, subset_sInter_iff, and_iff_right (sInter_subset_of_mem _)]
State after:
α : Type u_1
ι : Type u_2
M : Matroid α
F✝ I J X Y B C R : Set α
e f x y : α
hI : M.Indep I
F : Set α := {x | M.Basis I (insert x I)}
hIF : M.Basis I F
hF : M.Flat F
⊢ ∀ t' ∈ {F | M.Flat F ∧ I ∩ M.E ⊆ F}, F ⊆ t'

α : Type u_1
ι : Type u_2
M : Matroid α
F✝ I J X Y B C R : Set α
e f x y : α
hI : M.Indep I
F : Set α := {x | M.Basis I (insert x I)}
hIF : M.Basis I F
hF : M.Flat F
⊢ F ∈ {F | M.Flat F ∧ I ∩ M.E ⊆ F}

State before:
α : Type u_1
ι : Type u_2
M : Matroid α
F✝ I J X Y B C R : Set α
e f x y : α
hI : M.Indep I
F : Set α := {x | M.Basis I (insert x I)}
hIF : M.Basis I F
hF : M.Flat F
⊢ F ∈ {F | M.Flat F ∧ I ∩ M.E ⊆ F}
Tactic:
exact ⟨hF, inter_subset_left.trans hIF.subset⟩
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 : α
hI : M.Indep I
F : Set α := {x | M.Basis I (insert x I)}
hIF : M.Basis I F
⊢ M.Flat F
Tactic:
refine' ⟨fun J X hJF hJX e heX ↦ (_ : M.Basis _ _), hIF.subset_ground⟩
State after:
α : Type u_1
ι : Type u_2
M : Matroid α
F✝ I J✝ X✝ Y B C R : Set α
e✝ f x y : α
hI : M.Indep I
F : Set α := {x | M.Basis I (insert x I)}
hIF : M.Basis I F
J X : Set α
hJF : M.Basis J F
hJX : M.Basis J X
e : α
heX : e ∈ X
⊢ M.Basis I (insert 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 : α
hI : M.Indep I
F : Set α := {x | M.Basis I (insert x I)}
hIF : M.Basis I F
J X : Set α
hJF : M.Basis J F
hJX : M.Basis J X
e : α
heX : e ∈ X
⊢ M.Basis I (insert e I)
Tactic:
exact (hIF.basis_of_basis_of_subset_of_subset (hJX.basis_union hJF) hJF.subset
  (hIF.subset.trans subset_union_right)).basis_subset (subset_insert _ _)
  (insert_subset (Or.inl heX) (hIF.subset.trans subset_union_right))
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 : α
hI : M.Indep I
F : Set α := {x | M.Basis I (insert x I)}
hIF : M.Basis I F
hF : M.Flat F
⊢ ∀ t' ∈ {F | M.Flat F ∧ I ∩ M.E ⊆ F}, F ⊆ t'
Tactic:
rintro F' ⟨hF', hIF'⟩ e (he : M.Basis I (insert e I))
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 : α
hI : M.Indep I
F : Set α := {x | M.Basis I (insert x I)}
hIF : M.Basis I F
hF : M.Flat F
F' : Set α
hF' : M.Flat F'
hIF' : I ∩ M.E ⊆ F'
e : α
he : M.Basis I (insert e I)
⊢ e ∈ F'

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 : α
hI : M.Indep I
F : Set α := {x | M.Basis I (insert x I)}
hIF : M.Basis I F
hF : M.Flat F
F' : Set α
hF' : M.Flat F'
hIF' : I ∩ M.E ⊆ F'
e : α
he : M.Basis I (insert e I)
⊢ e ∈ F'
Tactic:
rw [inter_eq_left.mpr (hIF.subset.trans hIF.subset_ground)] at hIF'
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 : α
hI : M.Indep I
F : Set α := {x | M.Basis I (insert x I)}
hIF : M.Basis I F
hF : M.Flat F
F' : Set α
hF' : M.Flat F'
hIF' : I ⊆ F'
e : α
he : M.Basis I (insert e I)
⊢ e ∈ F'

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 : α
hI : M.Indep I
F : Set α := {x | M.Basis I (insert x I)}
hIF : M.Basis I F
hF : M.Flat F
F' : Set α
hF' : M.Flat F'
hIF' : I ⊆ F'
e : α
he : M.Basis I (insert e I)
⊢ e ∈ F'
Tactic:
obtain ⟨J, hJ, hIJ⟩ := hI.subset_basis_of_subset hIF' hF'.2
State after:
case intro.intro.intro
α : Type u_1
ι : Type u_2
M : Matroid α
F✝ I J✝ X Y B C R : Set α
e✝ f x y : α
hI : M.Indep I
F : Set α := {x | M.Basis I (insert x I)}
hIF : M.Basis I F
hF : M.Flat F
F' : Set α
hF' : M.Flat F'
hIF' : I ⊆ F'
e : α
he : M.Basis I (insert e I)
J : Set α
hJ : M.Basis J F'
hIJ : I ⊆ J
⊢ e ∈ F'

State before:
case intro.intro.intro
α : Type u_1
ι : Type u_2
M : Matroid α
F✝ I J✝ X Y B C R : Set α
e✝ f x y : α
hI : M.Indep I
F : Set α := {x | M.Basis I (insert x I)}
hIF : M.Basis I F
hF : M.Flat F
F' : Set α
hF' : M.Flat F'
hIF' : I ⊆ F'
e : α
he : M.Basis I (insert e I)
J : Set α
hJ : M.Basis J F'
hIJ : I ⊆ J
⊢ e ∈ F'
Tactic:
exact (hF'.1 hJ (he.basis_union_of_subset hJ.indep hIJ)) (Or.inr (mem_insert _ _))
State after:
no goals