-- Mathlib/Data/Matroid/Closure.lean
lemma Indep.closure_eq_setOf_isBasis_insert (hI : M.Indep I) :
    M.closure I = {x | M.IsBasis I (insert x I)}

Proof state:
α : Type u_2
M : Matroid α
I : Set α
hI : M.Indep I
F : Set α := {x | M.IsBasis I (insert x I)}
⊢ M.closure I = F

Tactic:
have hIF : M.IsBasis I F := hI.isBasis_setOf_insert_isBasis

Result:
α : Type u_2
M : Matroid α
I : Set α
hI : M.Indep I
F : Set α := {x | M.IsBasis I (insert x I)}
hIF : M.IsBasis I F
⊢ M.closure I = F

Proof state:
α : Type u_2
M : Matroid α
I : Set α
hI : M.Indep I
F : Set α := {x | M.IsBasis I (insert x I)}
hIF : M.IsBasis I F
⊢ M.IsFlat F

Tactic:
refine ⟨fun J X hJF hJX e heX ↦ show M.IsBasis _ _ from ?_, hIF.subset_ground⟩

Result:
α : Type u_2
M : Matroid α
I : Set α
hI : M.Indep I
F : Set α := {x | M.IsBasis I (insert x I)}
hIF : M.IsBasis I F
J X : Set α
hJF : M.IsBasis J F
hJX : M.IsBasis J X
e : α
heX : e ∈ X
⊢ M.IsBasis I (insert e I)

Proof state:
α : Type u_2
M : Matroid α
I : Set α
hI : M.Indep I
F : Set α := {x | M.IsBasis I (insert x I)}
hIF : M.IsBasis I F
⊢ M.closure I = F

Tactic:
have hF : M.IsFlat F := by
  refine ⟨fun J X hJF hJX e heX ↦ show M.IsBasis _ _ from ?_, hIF.subset_ground⟩
  exact (hIF.isBasis_of_isBasis_of_subset_of_subset (hJX.isBasis_union hJF) hJF.subset
    (hIF.subset.trans subset_union_right)).isBasis_subset (subset_insert _ _)
    (insert_subset (Or.inl heX) (hIF.subset.trans subset_union_right))

Result:
α : Type u_2
M : Matroid α
I : Set α
hI : M.Indep I
F : Set α := {x | M.IsBasis I (insert x I)}
hIF : M.IsBasis I F
hF : M.IsFlat F
⊢ M.closure I = F

Proof state:
α : Type u_2
M : Matroid α
I : Set α
hI : M.Indep I
F : Set α := {x | M.IsBasis I (insert x I)}
hIF : M.IsBasis I F
J X : Set α
hJF : M.IsBasis J F
hJX : M.IsBasis J X
e : α
heX : e ∈ X
⊢ M.IsBasis I (insert e I)

Tactic:
exact (hIF.isBasis_of_isBasis_of_subset_of_subset (hJX.isBasis_union hJF) hJF.subset
  (hIF.subset.trans subset_union_right)).isBasis_subset (subset_insert _ _)
  (insert_subset (Or.inl heX) (hIF.subset.trans subset_union_right))

Result:
no goals

Proof state:
α : Type u_2
M : Matroid α
I : Set α
hI : M.Indep I
F : Set α := {x | M.IsBasis I (insert x I)}
hIF : M.IsBasis I F
hF : M.IsFlat F
⊢ ∀ t' ∈ {F | M.IsFlat F ∧ I ∩ M.E ⊆ F}, F ⊆ t'

Tactic:
rintro F' ⟨hF', hIF'⟩ e (he : M.IsBasis I (insert e I))

Result:
case intro
α : Type u_2
M : Matroid α
I : Set α
hI : M.Indep I
F : Set α := {x | M.IsBasis I (insert x I)}
hIF : M.IsBasis I F
hF : M.IsFlat F
F' : Set α
hF' : M.IsFlat F'
hIF' : I ∩ M.E ⊆ F'
e : α
he : M.IsBasis I (insert e I)
⊢ e ∈ F'

Proof state:
α : Type u_2
M : Matroid α
I : Set α
hI : M.Indep I
F : Set α := {x | M.IsBasis I (insert x I)}
hIF : M.IsBasis I F
hF : M.IsFlat F
⊢ M.closure I = F

Tactic:
rw [subset_antisymm_iff, closure_def, subset_sInter_iff, and_iff_right (sInter_subset_of_mem _)]

Result:
α : Type u_2
M : Matroid α
I : Set α
hI : M.Indep I
F : Set α := {x | M.IsBasis I (insert x I)}
hIF : M.IsBasis I F
hF : M.IsFlat F
⊢ ∀ t' ∈ {F | M.IsFlat F ∧ I ∩ M.E ⊆ F}, F ⊆ t'

α : Type u_2
M : Matroid α
I : Set α
hI : M.Indep I
F : Set α := {x | M.IsBasis I (insert x I)}
hIF : M.IsBasis I F
hF : M.IsFlat F
⊢ F ∈ {F | M.IsFlat F ∧ I ∩ M.E ⊆ F}

Proof state:
case intro.intro.intro
α : Type u_2
M : Matroid α
I : Set α
hI : M.Indep I
F : Set α := {x | M.IsBasis I (insert x I)}
hIF : M.IsBasis I F
hF : M.IsFlat F
F' : Set α
hF' : M.IsFlat F'
hIF' : I ⊆ F'
e : α
he : M.IsBasis I (insert e I)
J : Set α
hJ : M.IsBasis J F'
hIJ : I ⊆ J
⊢ e ∈ F'

Tactic:
exact (hF'.1 hJ (he.isBasis_union_of_subset hJ.indep hIJ)) (Or.inr (mem_insert _ _))

Result:
no goals

Proof state:
α : Type u_2
M : Matroid α
I : Set α
hI : M.Indep I
⊢ M.closure I = {x | M.IsBasis I (insert x I)}

Tactic:
set F := {x | M.IsBasis I (insert x I)}

Result:
α : Type u_2
M : Matroid α
I : Set α
hI : M.Indep I
F : Set α := {x | M.IsBasis I (insert x I)}
⊢ M.closure I = F

Proof state:
α : Type u_2
M : Matroid α
I : Set α
hI : M.Indep I
F : Set α := {x | M.IsBasis I (insert x I)}
hIF : M.IsBasis I F
hF : M.IsFlat F
⊢ F ∈ {F | M.IsFlat F ∧ I ∩ M.E ⊆ F}

Tactic:
exact ⟨hF, inter_subset_left.trans hIF.subset⟩

Result:
no goals

Proof state:
case intro
α : Type u_2
M : Matroid α
I : Set α
hI : M.Indep I
F : Set α := {x | M.IsBasis I (insert x I)}
hIF : M.IsBasis I F
hF : M.IsFlat F
F' : Set α
hF' : M.IsFlat F'
hIF' : I ∩ M.E ⊆ F'
e : α
he : M.IsBasis I (insert e I)
⊢ e ∈ F'

Tactic:
rw [inter_eq_left.mpr (hIF.subset.trans hIF.subset_ground)] at hIF'

Result:
case intro
α : Type u_2
M : Matroid α
I : Set α
hI : M.Indep I
F : Set α := {x | M.IsBasis I (insert x I)}
hIF : M.IsBasis I F
hF : M.IsFlat F
F' : Set α
hF' : M.IsFlat F'
hIF' : I ⊆ F'
e : α
he : M.IsBasis I (insert e I)
⊢ e ∈ F'

Proof state:
case intro
α : Type u_2
M : Matroid α
I : Set α
hI : M.Indep I
F : Set α := {x | M.IsBasis I (insert x I)}
hIF : M.IsBasis I F
hF : M.IsFlat F
F' : Set α
hF' : M.IsFlat F'
hIF' : I ⊆ F'
e : α
he : M.IsBasis I (insert e I)
⊢ e ∈ F'

Tactic:
obtain ⟨J, hJ, hIJ⟩ := hI.subset_isBasis_of_subset hIF' hF'.2

Result:
case intro.intro.intro
α : Type u_2
M : Matroid α
I : Set α
hI : M.Indep I
F : Set α := {x | M.IsBasis I (insert x I)}
hIF : M.IsBasis I F
hF : M.IsFlat F
F' : Set α
hF' : M.IsFlat F'
hIF' : I ⊆ F'
e : α
he : M.IsBasis I (insert e I)
J : Set α
hJ : M.IsBasis J F'
hIJ : I ⊆ J
⊢ e ∈ F'