awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
h : e ∉ I
inr : e ∈ M.E \ M.closure I ↔ e ∈ M.E \ M.closure I ∨ e ∈ I
inr₁ inr₂ : e ∈ M.E \ M.closure I ↔ e ∈ M.E \ M.closure I
⊢ M.Indep (insert e I) ↔ e ∈ M.E \ M.closure I ∨ e ∈ I

Tactic:
rw [hI.insert_indep_iff_of_notMem h, or_iff_left h]

Premises used: or_iff_left, Matroid.Indep.insert_indep_iff_of_notMem
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
e : α
I : Set α
pos : ∀ (hI : M.Indep I), M.Indep (insert e I) ↔ M.Indep I ∧ (e ∉ I → e ∈ M.E \ M.closure I)
neg : ∀ (hI : ¬M.Indep I), M.Indep (insert e I) ↔ M.Indep I ∧ (e ∉ I → e ∈ M.E \ M.closure I)
⊢ M.Indep (insert e I) ↔ M.Indep I ∧ (e ∉ I → e ∈ M.E \ M.closure I)

Tactic:
by_cases hI : M.Indep I

Premises used: Matroid.Indep
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
pos : e ∈ M.E \ M.closure I ∨ e ∈ I ↔ M.Indep I ∧ (e ∉ I → e ∈ M.E \ M.closure I)
pos₁ : e ∈ M.E \ M.closure I ∨ e ∈ I ↔ e ∉ I → e ∈ M.E \ M.closure I
pos₂ pos₃ : e ∉ I → e ∈ M.E \ M.closure I ↔ e ∉ I → e ∈ M.E \ M.closure I
⊢ M.Indep (insert e I) ↔ M.Indep I ∧ (e ∉ I → e ∈ M.E \ M.closure I)

Tactic:
rw [hI.insert_indep_iff, and_iff_right hI, or_iff_not_imp_right]

Premises used: Classical.or_iff_not_imp_right, Matroid.Indep.insert_indep_iff, and_iff_right
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : ¬M.Indep I
⊢ M.Indep (insert e I) ↔ M.Indep I ∧ (e ∉ I → e ∈ M.E \ M.closure I)

Tactic:
simp [hI, show ¬ M.Indep (insert e I) from fun h ↦ hI <| h.subset <| subset_insert _ _]

Premises used: Matroid.Indep.subset, Set.subset_insert
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
e f : α
I : Set α
hI : M.Indep (I \ {e})
heI : e ∈ I
inl : M.Indep (insert e I \ {e}) ↔ e ∈ M.E \ M.closure (I \ {e}) ∨ e ∈ I
inr : ∀ (hne : e ≠ f), M.Indep (insert f I \ {e}) ↔ f ∈ M.E \ M.closure (I \ {e}) ∨ f ∈ I
⊢ M.Indep (insert f I \ {e}) ↔ f ∈ M.E \ M.closure (I \ {e}) ∨ f ∈ I

Tactic:
obtain rfl | hne := eq_or_ne e f

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep (I \ {e})
heI : e ∈ I
⊢ M.Indep (insert e I \ {e}) ↔ e ∈ M.E \ M.closure (I \ {e}) ∨ e ∈ I

Tactic:
simp [hI, heI]
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
e f : α
I : Set α
hI : M.Indep (I \ {e})
heI : e ∈ I
hne : e ≠ f
inr : M.Indep (insert f (I \ {e})) ↔ f ∈ M.E \ M.closure (I \ {e}) ∨ f ∈ I
inr₁ : f ∈ M.E \ M.closure (I \ {e}) ∨ f ∈ I \ {e} ↔ f ∈ M.E \ M.closure (I \ {e}) ∨ f ∈ I
inr₂ : f ∈ M.E \ M.closure (I \ {e}) ∨ f ∈ I ∧ f ≠ e ↔ f ∈ M.E \ M.closure (I \ {e}) ∨ f ∈ I
inr₃ inr₄ : f ∈ M.E \ M.closure (I \ {e}) ∨ f ∈ I ↔ f ∈ M.E \ M.closure (I \ {e}) ∨ f ∈ I
⊢ M.Indep (insert f I \ {e}) ↔ f ∈ M.E \ M.closure (I \ {e}) ∨ f ∈ I

Tactic:
rw [← insert_diff_singleton_comm hne.symm, hI.insert_indep_iff, mem_diff_singleton,
    and_iff_left hne.symm]

Premises used: and_iff_left, Matroid.Indep.insert_indep_iff, Ne.symm, Set.insert_diff_singleton_comm, Set.mem_diff_singleton
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X I : Set α
hI : M.Indep I
hIX : I ⊆ X
hXI : X ⊆ M.closure I
⊢ M.IsBasis I X

Tactic:
hI.isBasis_closure.isBasis_subset hIX hXI

Premises used: Matroid.Indep.isBasis_closure, Matroid.IsBasis.isBasis_subset
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X I : Set α
⊢ M.IsBasis I X ↔ M.Indep I ∧ I ⊆ X ∧ X ⊆ M.closure I

Tactic:
⟨fun h ↦ ⟨h.indep, h.subset, h.subset_closure⟩,
    fun h ↦ h.1.isBasis_of_subset_of_subset_closure h.2.1 h.2.2⟩

Premises used: Matroid.IsBasis.subset, And.right, And.left, And.intro, Iff.intro, Matroid.IsBasis.indep, Matroid.IsBasis.subset_closure, Matroid.Indep.isBasis_of_subset_of_subset_closure
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I : Set α
hI : M.Indep I
h : M.E ⊆ M.closure I
rw : M.IsBasis I M.E
⊢ M.IsBase I

Tactic:
rw [← isBasis_ground_iff]

Premises used: Matroid.isBasis_ground_iff
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I : Set α
hI : M.Indep I
h : M.E ⊆ M.closure I
⊢ M.IsBasis I M.E

Tactic:
hI.isBasis_of_subset_of_subset_closure hI.subset_ground h

Premises used: Matroid.Indep.subset_ground, Matroid.Indep.isBasis_of_subset_of_subset_closure
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I : Set α
hI : M.Indep I
h : M.E ⊆ M.closure I
⊢ M.IsBasis I M.E

Tactic:
exact hI.isBasis_of_subset_of_subset_closure hI.subset_ground h

Premises used: Matroid.Indep.subset_ground, Matroid.Indep.isBasis_of_subset_of_subset_closure
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
B : Set α
hB : M.IsBase B
⊢ M.IsBasis B M.E

Tactic:
rw [← isBasis_ground_iff] at hB

Premises used: Matroid.isBasis_ground_iff
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
B : Set α
hB : M.IsBasis B M.E
rw : M.closure M.E = M.E
rw₁ rw₂ : M.E = M.E
⊢ M.closure B = M.E

Tactic:
rw [hB.closure_eq_closure, closure_ground]

Premises used: Matroid.closure_ground, Matroid.IsBasis.closure_eq_closure
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X B : Set α
hB : M.IsBase B
hBX : B ⊆ X
⊢ M.closure X = M.E

Tactic:
(M.closure_subset_ground _).antisymm (hB.closure_eq ▸ M.closure_subset_closure hBX)

Premises used: Matroid.closure_subset_ground, Eq.rec, Matroid.IsBase.closure_eq, Matroid.closure_subset_closure, HasSubset.Subset.antisymm
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
B : Set α
rw : M.Indep B → (B ⊆ M.E ∧ M.E ⊆ M.closure B ↔ M.closure B = M.E)
⊢ M.IsBase B ↔ M.Indep B ∧ M.closure B = M.E

Tactic:
rw [← isBasis_ground_iff, isBasis_iff_indep_subset_closure, and_congr_right_iff]

Premises used: Matroid.isBasis_ground_iff, Matroid.isBasis_iff_indep_subset_closure, and_congr_right_iff
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
B : Set α
⊢ M.Indep B → (B ⊆ M.E ∧ M.E ⊆ M.closure B ↔ M.closure B = M.E)

Tactic:
fun hI ↦ ⟨fun h ↦ (M.closure_subset_ground _).antisymm h.2,
    fun h ↦ ⟨(M.subset_closure B).trans_eq h, h.symm.subset⟩⟩

Premises used: LE.le.trans_eq, Matroid.closure_subset_ground, Matroid.subset_closure, Eq.subset, And.right, HasSubset.Subset.antisymm, And.intro, Iff.intro, Eq.symm
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
B : Set α
⊢ M.Indep B → (B ⊆ M.E ∧ M.E ⊆ M.closure B ↔ M.closure B = M.E)

Tactic:
exact fun hI ↦ ⟨fun h ↦ (M.closure_subset_ground _).antisymm h.2,
    fun h ↦ ⟨(M.subset_closure B).trans_eq h, h.symm.subset⟩⟩
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
e f : α
B : Set α
hB : M.IsBase B
he : e ∈ B
hf : f ∉ M.closure (B \ {e})
hfE : f ∈ M.E
inl : ∀ (he : f ∈ B) (hf : f ∉ M.closure (B \ {f})), M.IsBase (insert f (B \ {f}))
inr : ∀ (hne : f ≠ e), M.IsBase (insert f (B \ {e}))
⊢ M.IsBase (insert f (B \ {e}))

Tactic:
obtain rfl | hne := eq_or_ne f e

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
f : α
B : Set α
hB : M.IsBase B
hfE : f ∈ M.E
he : f ∈ B
hf : f ∉ M.closure (B \ {f})
⊢ M.IsBase (insert f (B \ {f}))

Tactic:
simpa [he]
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
e f : α
B : Set α
hB : M.IsBase B
he : e ∈ B
hf : f ∉ M.closure (B \ {e})
hfE : f ∈ M.E
hne : f ≠ e
⊢ M.Indep (insert f (B \ {e})) ∧ f ∉ B

Tactic:
simpa [(hB.indep.diff _).notMem_closure_iff, hne] using hf

Premises used: Matroid.Indep.diff, Matroid.Indep.notMem_closure_iff, Matroid.IsBase.indep
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
e f : α
B : Set α
hB : M.IsBase B
he : e ∈ B
hf : f ∉ M.closure (B \ {e})
hfE : f ∈ M.E
hne : f ≠ e
⊢ M.Indep (insert f (B \ {e}))

Tactic:
have ⟨hi, hfB⟩ : M.Indep (insert f (B \ {e})) ∧ f ∉ B := by
    simpa [(hB.indep.diff _).notMem_closure_iff, hne] using hf
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
e f : α
B : Set α
hB : M.IsBase B
he : e ∈ B
hf : f ∉ M.closure (B \ {e})
hfE : f ∈ M.E
hne : f ≠ e
hi : M.Indep (insert f (B \ {e}))
⊢ f ∉ B

Tactic:
have ⟨hi, hfB⟩ : M.Indep (insert f (B \ {e})) ∧ f ∉ B := by
    simpa [(hB.indep.diff _).notMem_closure_iff, hne] using hf
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
e f : α
B : Set α
hB : M.IsBase B
he : e ∈ B
hf : f ∉ M.closure (B \ {e})
hfE : f ∈ M.E
hne : f ≠ e
hi : M.Indep (insert f (B \ {e}))
hfB : f ∉ B
⊢ M.IsBase (insert f (B \ {e}))

Tactic:
hB.exchange_isBase_of_indep hfB hi

Premises used: Matroid.IsBase.exchange_isBase_of_indep
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
e f : α
B : Set α
hB : M.IsBase B
he : e ∈ B
hf : f ∉ M.closure (B \ {e})
hfE : f ∈ M.E
hne : f ≠ e
hi : M.Indep (insert f (B \ {e}))
hfB : f ∉ B
⊢ M.IsBase (insert f (B \ {e}))

Tactic:
exact hB.exchange_isBase_of_indep hfB hi

Premises used: Matroid.IsBase.exchange_isBase_of_indep
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I : Set α
hI : M.Indep I
⊢ M.IsBase I ↔ M.E ⊆ M.closure I

Tactic:
⟨fun h ↦ h.closure_eq.symm.subset, hI.isBase_of_ground_subset_closure⟩

Premises used: Matroid.IsBase.closure_eq, Eq.subset, Iff.intro, Eq.symm, Matroid.Indep.isBase_of_ground_subset_closure
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJI : J ⊆ I
⊢ M.Indep J

Tactic:
have hJ := hI.subset hJI
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJI : J ⊆ I
hJ : M.Indep J
rw : M.closure J ∩ I ⊆ J
⊢ M.closure J ∩ I = J

Tactic:
rw [subset_antisymm_iff, and_iff_left (subset_inter (M.subset_closure _) hJI)]

Premises used: and_iff_left, Matroid.subset_closure, Set.subset_inter, subset_antisymm_iff
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJI : J ⊆ I
hJ : M.Indep J
e : α
heJ : e ∈ M.closure J
heI : e ∈ I
⊢ e ∈ J

Tactic:
hJ.isBasis_closure.mem_of_insert_indep heJ (hI.subset (insert_subset heI hJI))

Premises used: Matroid.Indep.isBasis_closure, Matroid.Indep.subset, Matroid.IsBasis.mem_of_insert_indep, Set.insert_subset
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJI : J ⊆ I
hJ : M.Indep J
e : α
heJ : e ∈ M.closure J
heI : e ∈ I
⊢ e ∈ J

Tactic:
exact hJ.isBasis_closure.mem_of_insert_indep heJ (hI.subset (insert_subset heI hJI))

Premises used: Matroid.Indep.isBasis_closure, Matroid.Indep.subset, Matroid.IsBasis.mem_of_insert_indep, Set.insert_subset
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I : Set α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
rw : (∀ (i : Set α) (j : i ∈ Js), M.closure (⋂₀ Js) ⊆ M.closure i) ∧ ⋂ J ∈ Js, M.closure J ⊆ M.closure (⋂₀ Js)
⊢ M.closure (⋂₀ Js) = ⋂ J ∈ Js, M.closure J

Tactic:
rw [subset_antisymm_iff, subset_iInter₂_iff]

Premises used: Set.subset_iInter₂_iff, subset_antisymm_iff
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I : Set α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
⊢ ⋂₀ Js ⊆ I

Tactic:
have hiX : ⋂₀ Js ⊆ I := (sInter_subset_of_mem hne.some_mem).trans (hIs _ hne.some_mem)
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I : Set α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
⊢ M.Indep (⋂₀ Js)

Tactic:
have hiI := hI.subset hiX
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I : Set α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
⊢ (∀ (i : Set α) (j : i ∈ Js), M.closure (⋂₀ Js) ⊆ M.closure i) ∧ ⋂ J ∈ Js, M.closure J ⊆ M.closure (⋂₀ Js)

Tactic:
⟨ fun X hX ↦ M.closure_subset_closure (sInter_subset_of_mem hX),
    fun e he ↦ by_contra fun he' ↦ ?_⟩

Premises used: Set.sInter_subset_of_mem, Matroid.closure_subset_closure, And.intro, by_contra
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I : Set α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
refine : ∀ (e : α) (he : Membership.mem (γ := Set α) (⋂ J ∈ Js, M.closure J) e) (he' : e ∉ M.closure (⋂₀ Js)), False
⊢ (∀ (i : Set α) (j : i ∈ Js), M.closure (⋂₀ Js) ⊆ M.closure i) ∧ ⋂ J ∈ Js, M.closure J ⊆ M.closure (⋂₀ Js)

Tactic:
refine ⟨ fun X hX ↦ M.closure_subset_closure (sInter_subset_of_mem hX),
    fun e he ↦ by_contra fun he' ↦ ?_⟩
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I : Set α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : Membership.mem (γ := Set α) (⋂ J ∈ Js, M.closure J) e
he' : e ∉ M.closure (⋂₀ Js)
⊢ ∀ (i : Set α) (j : i ∈ Js), e ∈ M.closure i

Tactic:
rw [mem_iInter₂] at he

Premises used: Set.mem_iInter₂
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I : Set α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : Membership.mem (γ := Set α) (⋂ J ∈ Js, M.closure J) e
he' : e ∉ M.closure (⋂₀ Js)
he₁ : ∀ (i : Set α) (j : i ∈ Js), e ∈ M.closure i
⊢ e ∉ M.closure (⋂₀ Js)

Tactic:
rw [mem_iInter₂] at he

Premises used: Set.mem_iInter₂
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I : Set α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ (i : Set α) (j : i ∈ Js), e ∈ M.closure i
he' : e ∉ M.closure (⋂₀ Js)
⊢ e ∈ M.E \ I

Tactic:
⟨M.closure_subset_ground _ (he _ hne.some_mem), fun heI ↦ he' ?_⟩

Premises used: Set.Mem, Matroid.closure_subset_ground, Set.diff, setOf, Set.Nonempty.some_mem, And.intro
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I : Set α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ (i : Set α) (j : i ∈ Js), e ∈ M.closure i
he' : e ∉ M.closure (⋂₀ Js)
refine : ∀ (heI : e ∈ I), e ∈ M.closure (⋂₀ Js)
⊢ e ∈ M.E \ I

Tactic:
refine ⟨M.closure_subset_ground _ (he _ hne.some_mem), fun heI ↦ he' ?_⟩
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I : Set α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ (i : Set α) (j : i ∈ Js), e ∈ M.closure i
he' : e ∉ M.closure (⋂₀ Js)
heI : e ∈ I
⊢ e ∈ M.closure (⋂₀ Js)

Tactic:
mem_closure_of_mem _ (fun X hX' ↦ ?_) hiI.subset_ground

Premises used: Matroid.Indep.subset_ground, Matroid.mem_closure_of_mem
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I : Set α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ (i : Set α) (j : i ∈ Js), e ∈ M.closure i
he' : e ∉ M.closure (⋂₀ Js)
heI : e ∈ I
refine : ∀ (X : Set α) (hX' : X ∈ Js), e ∈ X
⊢ e ∈ M.closure (⋂₀ Js)

Tactic:
refine mem_closure_of_mem _ (fun X hX' ↦ ?_) hiI.subset_ground
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I : Set α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ (i : Set α) (j : i ∈ Js), e ∈ M.closure i
he' : e ∉ M.closure (⋂₀ Js)
heI : e ∈ I
X : Set α
hX' : X ∈ Js
rw : e ∈ M.closure X ∩ I
⊢ e ∈ X

Tactic:
rw [← hI.closure_inter_eq_self_of_subset (hIs X hX')]

Premises used: Matroid.Indep.closure_inter_eq_self_of_subset
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I : Set α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ (i : Set α) (j : i ∈ Js), e ∈ M.closure i
he' : e ∉ M.closure (⋂₀ Js)
heI : e ∈ I
X : Set α
hX' : X ∈ Js
⊢ e ∈ M.closure X ∩ I

Tactic:
⟨he X hX', heI⟩

Premises used: Set.Mem, setOf, Set.inter, And.intro
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I : Set α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ (i : Set α) (j : i ∈ Js), e ∈ M.closure i
he' : e ∉ M.closure (⋂₀ Js)
heI : e ∈ I
X : Set α
hX' : X ∈ Js
⊢ e ∈ M.closure X ∩ I

Tactic:
exact ⟨he X hX', heI⟩
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I : Set α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ (i : Set α) (j : i ∈ Js), e ∈ M.closure i
he' : e ∉ M.closure (⋂₀ Js)
⊢ e ∈ M.E \ I

Tactic:
have heEI : e ∈ M.E \ I := by
    refine ⟨M.closure_subset_ground _ (he _ hne.some_mem), fun heI ↦ he' ?_⟩
    refine mem_closure_of_mem _ (fun X hX' ↦ ?_) hiI.subset_ground
    rw [← hI.closure_inter_eq_self_of_subset (hIs X hX')]
    exact ⟨he X hX', heI⟩
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I : Set α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ (i : Set α) (j : i ∈ Js), e ∈ M.closure i
he' : e ∉ M.closure (⋂₀ Js)
heEI : e ∈ M.E \ I
⊢ M.Indep (insert e (⋂₀ Js))

Tactic:
rw [hiI.notMem_closure_iff_of_notMem (notMem_subset hiX heEI.2)] at he'

Premises used: And.right, Matroid.Indep.notMem_closure_iff_of_notMem, Set.notMem_subset
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I : Set α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ (i : Set α) (j : i ∈ Js), e ∈ M.closure i
he' : e ∉ M.closure (⋂₀ Js)
heEI : e ∈ M.E \ I
he'₁ : M.Indep (insert e (⋂₀ Js))
⊢ e ∈ M.E \ I

Tactic:
rw [hiI.notMem_closure_iff_of_notMem (notMem_subset hiX heEI.2)] at he'

Premises used: And.right, Matroid.Indep.notMem_closure_iff_of_notMem, Set.notMem_subset
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I : Set α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ (i : Set α) (j : i ∈ Js), e ∈ M.closure i
he' : M.Indep (insert e (⋂₀ Js))
heEI : e ∈ M.E \ I
obtain : ∀ (J : Set α) (hJI : M.IsBasis J (insert e I)) (heJ : insert e (⋂₀ Js) ⊆ J), False
⊢ False

Tactic:
obtain ⟨J, hJI, heJ⟩ := he'.subset_isBasis_of_subset (insert_subset_insert hiX)
    (insert_subset heEI.1 hI.subset_ground)

Premises used: Matroid.Indep.subset_ground, And.left, Matroid.Indep.subset_isBasis_of_subset, Set.insert_subset, Set.insert_subset_insert
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I : Set α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ (i : Set α) (j : i ∈ Js), e ∈ M.closure i
he' : M.Indep (insert e (⋂₀ Js))
heEI : e ∈ M.E \ I
J : Set α
hJI : M.IsBasis J (insert e I)
heJ : insert e (⋂₀ Js) ⊆ J
rw : e ∈ M.closure I
⊢ M.IsBasis I (insert e I)

Tactic:
rw [hI.insert_isBasis_iff_mem_closure]

Premises used: Matroid.Indep.insert_isBasis_iff_mem_closure
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I : Set α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ (i : Set α) (j : i ∈ Js), e ∈ M.closure i
he' : M.Indep (insert e (⋂₀ Js))
heEI : e ∈ M.E \ I
J : Set α
hJI : M.IsBasis J (insert e I)
heJ : insert e (⋂₀ Js) ⊆ J
⊢ e ∈ M.closure I

Tactic:
(M.closure_subset_closure (hIs _ hne.some_mem)) (he _ hne.some_mem)

Premises used: Set.Nonempty.some_mem, Matroid.closure_subset_closure
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I : Set α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ (i : Set α) (j : i ∈ Js), e ∈ M.closure i
he' : M.Indep (insert e (⋂₀ Js))
heEI : e ∈ M.E \ I
J : Set α
hJI : M.IsBasis J (insert e I)
heJ : insert e (⋂₀ Js) ⊆ J
⊢ e ∈ M.closure I

Tactic:
exact (M.closure_subset_closure (hIs _ hne.some_mem)) (he _ hne.some_mem)

Premises used: Set.Nonempty.some_mem, Matroid.closure_subset_closure
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I : Set α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ (i : Set α) (j : i ∈ Js), e ∈ M.closure i
he' : M.Indep (insert e (⋂₀ Js))
heEI : e ∈ M.E \ I
J : Set α
hJI : M.IsBasis J (insert e I)
heJ : insert e (⋂₀ Js) ⊆ J
⊢ M.IsBasis I (insert e I)

Tactic:
have hIb : M.IsBasis I (insert e I) := by
    rw [hI.insert_isBasis_iff_mem_closure]
    exact (M.closure_subset_closure (hIs _ hne.some_mem)) (he _ hne.some_mem)
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I : Set α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ (i : Set α) (j : i ∈ Js), e ∈ M.closure i
he' : M.Indep (insert e (⋂₀ Js))
heEI : e ∈ M.E \ I
J : Set α
hJI : M.IsBasis J (insert e I)
heJ : insert e (⋂₀ Js) ⊆ J
hIb : M.IsBasis I (insert e I)
obtain : ∀ (f : α) (hfIJ : f ∈ I \ J) (hfb : M.IsBasis (insert f (J \ {e})) (insert e I)), False
⊢ False

Tactic:
obtain ⟨f, hfIJ, hfb⟩ := hJI.exchange hIb ⟨heJ (mem_insert e _), heEI.2⟩

Premises used: And.right, And.intro, Set.mem_insert, Matroid.IsBasis.exchange
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I : Set α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ (i : Set α) (j : i ∈ Js), e ∈ M.closure i
he' : M.Indep (insert e (⋂₀ Js))
heEI : e ∈ M.E \ I
J : Set α
hJI : M.IsBasis J (insert e I)
heJ : insert e (⋂₀ Js) ⊆ J
hIb : M.IsBasis I (insert e I)
f : α
hfIJ : f ∈ I \ J
hfb : M.IsBasis (insert f (J \ {e})) (insert e I)
rw : J ⊆ insert e I
⊢ J \ {e} ⊆ I

Tactic:
rw [diff_subset_iff, singleton_union]

Premises used: Set.diff_subset_iff, Set.singleton_union
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I : Set α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ (i : Set α) (j : i ∈ Js), e ∈ M.closure i
he' : M.Indep (insert e (⋂₀ Js))
heEI : e ∈ M.E \ I
J : Set α
hJI : M.IsBasis J (insert e I)
heJ : insert e (⋂₀ Js) ⊆ J
hIb : M.IsBasis I (insert e I)
f : α
hfIJ : f ∈ I \ J
hfb : M.IsBasis (insert f (J \ {e})) (insert e I)
⊢ J ⊆ insert e I

Tactic:
hJI.subset

Premises used: Matroid.IsBasis.subset
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I : Set α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ (i : Set α) (j : i ∈ Js), e ∈ M.closure i
he' : M.Indep (insert e (⋂₀ Js))
heEI : e ∈ M.E \ I
J : Set α
hJI : M.IsBasis J (insert e I)
heJ : insert e (⋂₀ Js) ⊆ J
hIb : M.IsBasis I (insert e I)
f : α
hfIJ : f ∈ I \ J
hfb : M.IsBasis (insert f (J \ {e})) (insert e I)
⊢ J ⊆ insert e I

Tactic:
exact hJI.subset

Premises used: Matroid.IsBasis.subset