-- Mathlib/Data/Matroid/Circuit.lean
/-- In a finitary matroid, each finite set `X` spanned by a set `Y` is in fact
spanned by a finite independent subset of `Y`. -/
lemma exists_subset_finite_closure_of_subset_closure [M.Finitary] (hX : X.Finite)
    (hXY : X ⊆ M.closure Y) : ∃ I ⊆ Y, I.Finite ∧ M.Indep I ∧ X ⊆ M.closure I

Proof state:
case intro.intro.intro.intro
α : Type u_1
M : Matroid α
X Y : Set α
inst✝ : M.Finitary
hX : X.Finite
hXY : X ⊆ M.closure Y
T : Set α
hT : T ⊆ Y
hTfin : T.Finite
hXT : X ⊆ M.closure T
I : Set α
hI : M.IsBasis' I T
⊢ ∃ I ⊆ Y, I.Finite ∧ M.Indep I ∧ X ⊆ M.closure I

Tactic:
exact ⟨_, hI.subset.trans hT, hTfin.subset hI.subset, hI.indep, by rwa [hI.closure_eq_closure]⟩

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
X Y : Set α
inst✝ : M.Finitary
hX : X.Finite
hXY : X ⊆ M.closure Y
⊢ ∃ I ⊆ Y, I.Finite ∧ M.Indep I ∧ X ⊆ M.closure I

Tactic:
suffices aux : ∃ T ⊆ Y, T.Finite ∧ X ⊆ M.closure T by
  obtain ⟨T, hT, hTfin, hXT⟩ := aux
  obtain ⟨I, hI⟩ := M.exists_isBasis' T
  exact ⟨_, hI.subset.trans hT, hTfin.subset hI.subset, hI.indep, by rwa [hI.closure_eq_closure]⟩

Result:
α : Type u_1
M : Matroid α
X Y : Set α
inst✝ : M.Finitary
hX : X.Finite
hXY : X ⊆ M.closure Y
⊢ ∃ T ⊆ Y, T.Finite ∧ X ⊆ M.closure T

Proof state:
α : Type u_1
M : Matroid α
X Y : Set α
inst✝ : M.Finitary
hX : X.Finite
hXY : X ⊆ M.closure Y
e : α
Z : Set α
heX : e ∈ X
x✝¹ : Z ⊆ X
heZ : e ∉ Z
x✝ : ∃ T ⊆ Y, T.Finite ∧ Z ⊆ M.closure T
T : Set α
hTY : T ⊆ Y
hTfin : T.Finite
hT : Z ⊆ M.closure T
⊢ ∃ T ⊆ Y, T.Finite ∧ insert e Z ⊆ M.closure T

Tactic:
obtain ⟨S, hSY, hSfin, -, heS⟩ := exists_mem_finite_closure_of_mem_closure (hXY heX)

Result:
case intro.intro.intro.intro
α : Type u_1
M : Matroid α
X Y : Set α
inst✝ : M.Finitary
hX : X.Finite
hXY : X ⊆ M.closure Y
e : α
Z : Set α
heX : e ∈ X
x✝¹ : Z ⊆ X
heZ : e ∉ Z
x✝ : ∃ T ⊆ Y, T.Finite ∧ Z ⊆ M.closure T
T : Set α
hTY : T ⊆ Y
hTfin : T.Finite
hT : Z ⊆ M.closure T
S : Set α
hSY : S ⊆ Y
hSfin : S.Finite
heS : e ∈ M.closure S
⊢ ∃ T ⊆ Y, T.Finite ∧ insert e Z ⊆ M.closure T

Proof state:
case intro.intro.intro
α : Type u_1
M : Matroid α
X Y : Set α
inst✝ : M.Finitary
hX : X.Finite
hXY : X ⊆ M.closure Y
T : Set α
hT : T ⊆ Y
hTfin : T.Finite
hXT : X ⊆ M.closure T
⊢ ∃ I ⊆ Y, I.Finite ∧ M.Indep I ∧ X ⊆ M.closure I

Tactic:
obtain ⟨I, hI⟩ := M.exists_isBasis' T

Result:
case intro.intro.intro.intro
α : Type u_1
M : Matroid α
X Y : Set α
inst✝ : M.Finitary
hX : X.Finite
hXY : X ⊆ M.closure Y
T : Set α
hT : T ⊆ Y
hTfin : T.Finite
hXT : X ⊆ M.closure T
I : Set α
hI : M.IsBasis' I T
⊢ ∃ I ⊆ Y, I.Finite ∧ M.Indep I ∧ X ⊆ M.closure I

Proof state:
α : Type u_1
M : Matroid α
X Y : Set α
inst✝ : M.Finitary
hX : X.Finite
hXY : X ⊆ M.closure Y
⊢ ∃ T ⊆ Y, T.Finite ∧ X ⊆ M.closure T

Tactic:
refine Finite.induction_on_subset X hX ⟨∅, by simp⟩ (fun {e Z} heX _ heZ ⟨T, hTY, hTfin, hT⟩ ↦ ?_)

Result:
α : Type u_1
M : Matroid α
X Y : Set α
inst✝ : M.Finitary
hX : X.Finite
hXY : X ⊆ M.closure Y
e : α
Z : Set α
heX : e ∈ X
x✝¹ : Z ⊆ X
heZ : e ∉ Z
x✝ : ∃ T ⊆ Y, T.Finite ∧ Z ⊆ M.closure T
T : Set α
hTY : T ⊆ Y
hTfin : T.Finite
hT : Z ⊆ M.closure T
⊢ ∃ T ⊆ Y, T.Finite ∧ insert e Z ⊆ M.closure T

Proof state:
α : Type u_1
M : Matroid α
X Y : Set α
inst✝ : M.Finitary
hX : X.Finite
hXY : X ⊆ M.closure Y
aux : ∃ T ⊆ Y, T.Finite ∧ X ⊆ M.closure T
⊢ ∃ I ⊆ Y, I.Finite ∧ M.Indep I ∧ X ⊆ M.closure I

Tactic:
obtain ⟨T, hT, hTfin, hXT⟩ := aux

Result:
case intro.intro.intro
α : Type u_1
M : Matroid α
X Y : Set α
inst✝ : M.Finitary
hX : X.Finite
hXY : X ⊆ M.closure Y
T : Set α
hT : T ⊆ Y
hTfin : T.Finite
hXT : X ⊆ M.closure T
⊢ ∃ I ⊆ Y, I.Finite ∧ M.Indep I ∧ X ⊆ M.closure I

Proof state:
α : Type u_1
M : Matroid α
X Y : Set α
inst✝ : M.Finitary
hX : X.Finite
hXY : X ⊆ M.closure Y
⊢ ∅ ⊆ Y ∧ ∅.Finite ∧ ∅ ⊆ M.closure ∅

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
X Y : Set α
inst✝ : M.Finitary
hX : X.Finite
hXY : X ⊆ M.closure Y
T : Set α
hT : T ⊆ Y
hTfin : T.Finite
hXT : X ⊆ M.closure T
I : Set α
hI : M.IsBasis' I T
⊢ X ⊆ M.closure I

Tactic:
rwa [hI.closure_eq_closure]

Result:
no goals

Proof state:
case intro.intro.intro.intro
α : Type u_1
M : Matroid α
X Y : Set α
inst✝ : M.Finitary
hX : X.Finite
hXY : X ⊆ M.closure Y
e : α
Z : Set α
heX : e ∈ X
x✝¹ : Z ⊆ X
heZ : e ∉ Z
x✝ : ∃ T ⊆ Y, T.Finite ∧ Z ⊆ M.closure T
T : Set α
hTY : T ⊆ Y
hTfin : T.Finite
hT : Z ⊆ M.closure T
S : Set α
hSY : S ⊆ Y
hSfin : S.Finite
heS : e ∈ M.closure S
⊢ ∃ T ⊆ Y, T.Finite ∧ insert e Z ⊆ M.closure T

Tactic:
exact ⟨S ∪ T, union_subset hSY hTY, hSfin.union hTfin, insert_subset
  (M.closure_mono subset_union_left heS) (hT.trans (M.closure_mono subset_union_right))⟩

Result:
no goals