awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
⊢ M.Indep (insert f (J \ {e}))

Tactic:
obtain rfl := hI.eq_of_isBasis (hfb.isBasis_subset (insert_subset hfIJ.1
    (by (rw [diff_subset_iff, singleton_union]; exact hJI.subset))) (subset_insert _ _))

Premises used: Matroid.IsBasis.isBasis_subset, And.left, Set.subset_insert, Matroid.Indep.eq_of_isBasis, Set.insert_subset, rfl
-- 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)
hI₁ : M.Indep (insert f (J \ {e}))
⊢ ∀ J_1 ∈ Js, J_1 ⊆ insert f (J \ {e})

Tactic:
obtain rfl := hI.eq_of_isBasis (hfb.isBasis_subset (insert_subset hfIJ.1
    (by (rw [diff_subset_iff, singleton_union]; exact hJI.subset))) (subset_insert _ _))

Premises used: Matroid.IsBasis.isBasis_subset, And.left, Set.subset_insert, Matroid.Indep.eq_of_isBasis, Set.insert_subset, rfl
-- 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)
hI₁ : M.Indep (insert f (J \ {e}))
hIs₁ : ∀ J_1 ∈ Js, J_1 ⊆ insert f (J \ {e})
⊢ ⋂₀ Js ⊆ insert f (J \ {e})

Tactic:
obtain rfl := hI.eq_of_isBasis (hfb.isBasis_subset (insert_subset hfIJ.1
    (by (rw [diff_subset_iff, singleton_union]; exact hJI.subset))) (subset_insert _ _))

Premises used: Matroid.IsBasis.isBasis_subset, And.left, Set.subset_insert, Matroid.Indep.eq_of_isBasis, Set.insert_subset, rfl
-- 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)
hI₁ : M.Indep (insert f (J \ {e}))
hIs₁ : ∀ J_1 ∈ Js, J_1 ⊆ insert f (J \ {e})
hiX₁ : ⋂₀ Js ⊆ insert f (J \ {e})
⊢ e ∈ M.E \ insert f (J \ {e})

Tactic:
obtain rfl := hI.eq_of_isBasis (hfb.isBasis_subset (insert_subset hfIJ.1
    (by (rw [diff_subset_iff, singleton_union]; exact hJI.subset))) (subset_insert _ _))

Premises used: Matroid.IsBasis.isBasis_subset, And.left, Set.subset_insert, Matroid.Indep.eq_of_isBasis, Set.insert_subset, rfl
-- 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)
hI₁ : M.Indep (insert f (J \ {e}))
hIs₁ : ∀ J_1 ∈ Js, J_1 ⊆ insert f (J \ {e})
hiX₁ : ⋂₀ Js ⊆ insert f (J \ {e})
heEI₁ : e ∈ M.E \ insert f (J \ {e})
⊢ M.IsBasis J (insert e (insert f (J \ {e})))

Tactic:
obtain rfl := hI.eq_of_isBasis (hfb.isBasis_subset (insert_subset hfIJ.1
    (by (rw [diff_subset_iff, singleton_union]; exact hJI.subset))) (subset_insert _ _))

Premises used: Matroid.IsBasis.isBasis_subset, And.left, Set.subset_insert, Matroid.Indep.eq_of_isBasis, Set.insert_subset, rfl
-- 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)
hI₁ : M.Indep (insert f (J \ {e}))
hIs₁ : ∀ J_1 ∈ Js, J_1 ⊆ insert f (J \ {e})
hiX₁ : ⋂₀ Js ⊆ insert f (J \ {e})
heEI₁ : e ∈ M.E \ insert f (J \ {e})
hJI₁ : M.IsBasis J (insert e (insert f (J \ {e})))
⊢ M.IsBasis (insert f (J \ {e})) (insert e (insert f (J \ {e})))

Tactic:
obtain rfl := hI.eq_of_isBasis (hfb.isBasis_subset (insert_subset hfIJ.1
    (by (rw [diff_subset_iff, singleton_union]; exact hJI.subset))) (subset_insert _ _))

Premises used: Matroid.IsBasis.isBasis_subset, And.left, Set.subset_insert, Matroid.Indep.eq_of_isBasis, Set.insert_subset, rfl
-- 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)
hI₁ : M.Indep (insert f (J \ {e}))
hIs₁ : ∀ J_1 ∈ Js, J_1 ⊆ insert f (J \ {e})
hiX₁ : ⋂₀ Js ⊆ insert f (J \ {e})
heEI₁ : e ∈ M.E \ insert f (J \ {e})
hJI₁ : M.IsBasis J (insert e (insert f (J \ {e})))
hIb₁ : M.IsBasis (insert f (J \ {e})) (insert e (insert f (J \ {e})))
⊢ f ∈ insert f (J \ {e}) \ J

Tactic:
obtain rfl := hI.eq_of_isBasis (hfb.isBasis_subset (insert_subset hfIJ.1
    (by (rw [diff_subset_iff, singleton_union]; exact hJI.subset))) (subset_insert _ _))

Premises used: Matroid.IsBasis.isBasis_subset, And.left, Set.subset_insert, Matroid.Indep.eq_of_isBasis, Set.insert_subset, rfl
-- 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)
hI₁ : M.Indep (insert f (J \ {e}))
hIs₁ : ∀ J_1 ∈ Js, J_1 ⊆ insert f (J \ {e})
hiX₁ : ⋂₀ Js ⊆ insert f (J \ {e})
heEI₁ : e ∈ M.E \ insert f (J \ {e})
hJI₁ : M.IsBasis J (insert e (insert f (J \ {e})))
hIb₁ : M.IsBasis (insert f (J \ {e})) (insert e (insert f (J \ {e})))
hfIJ₁ : f ∈ insert f (J \ {e}) \ J
⊢ M.IsBasis (insert f (J \ {e})) (insert e (insert f (J \ {e})))

Tactic:
obtain rfl := hI.eq_of_isBasis (hfb.isBasis_subset (insert_subset hfIJ.1
    (by (rw [diff_subset_iff, singleton_union]; exact hJI.subset))) (subset_insert _ _))

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

Tactic:
hfIJ.2 (heJ (mem_insert_of_mem _ fun X hX' ↦ by_contra fun hfX ↦ ?_))

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

Tactic:
refine hfIJ.2 (heJ (mem_insert_of_mem _ fun X hX' ↦ by_contra fun hfX ↦ ?_))

Premises used: Set.mem_insert_of_mem, And.right, by_contra
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
Js : Set (Set α)
hne : Js.Nonempty
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ (i : Set α) (j : i ∈ Js), e ∈ M.closure i
he' : M.Indep (insert e (⋂₀ Js))
J : Set α
heJ : insert e (⋂₀ Js) ⊆ J
f : α
hI : M.Indep (insert f (J \ {e}))
hIs : ∀ J_1 ∈ Js, J_1 ⊆ insert f (J \ {e})
hiX : ⋂₀ Js ⊆ insert f (J \ {e})
heEI : e ∈ M.E \ insert f (J \ {e})
hJI : M.IsBasis J (insert e (insert f (J \ {e})))
hIb : M.IsBasis (insert f (J \ {e})) (insert e (insert f (J \ {e})))
hfIJ : f ∈ insert f (J \ {e}) \ J
hfb : M.IsBasis (insert f (J \ {e})) (insert e (insert f (J \ {e})))
X : Set α
hX' : X ∈ Js
hfX : f ∉ X
inl : ∀ (hd : M.Dep (insert e X)), False
inr : ∀ (heX : e ∈ X), False
⊢ False

Tactic:
obtain (hd | heX) := ((hI.subset (hIs X hX')).mem_closure_iff).mp (he _ hX')

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

Tactic:
(hJI.indep.subset (insert_subset (heJ (mem_insert _ _)) ?_)).not_dep hd

Premises used: Matroid.Indep.subset, Set.mem_insert, Matroid.IsBasis.indep, Matroid.Indep.not_dep, Set.insert_subset
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
Js : Set (Set α)
hne : Js.Nonempty
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ (i : Set α) (j : i ∈ Js), e ∈ M.closure i
he' : M.Indep (insert e (⋂₀ Js))
J : Set α
heJ : insert e (⋂₀ Js) ⊆ J
f : α
hI : M.Indep (insert f (J \ {e}))
hIs : ∀ J_1 ∈ Js, J_1 ⊆ insert f (J \ {e})
hiX : ⋂₀ Js ⊆ insert f (J \ {e})
heEI : e ∈ M.E \ insert f (J \ {e})
hJI : M.IsBasis J (insert e (insert f (J \ {e})))
hIb : M.IsBasis (insert f (J \ {e})) (insert e (insert f (J \ {e})))
hfIJ : f ∈ insert f (J \ {e}) \ J
hfb : M.IsBasis (insert f (J \ {e})) (insert e (insert f (J \ {e})))
X : Set α
hX' : X ∈ Js
hfX : f ∉ X
hd : M.Dep (insert e X)
inl : X ⊆ J
⊢ False

Tactic:
refine (hJI.indep.subset (insert_subset (heJ (mem_insert _ _)) ?_)).not_dep hd

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

Tactic:
specialize hIs _ hX'
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
Js : Set (Set α)
hne : Js.Nonempty
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ (i : Set α) (j : i ∈ Js), e ∈ M.closure i
he' : M.Indep (insert e (⋂₀ Js))
J : Set α
heJ : insert e (⋂₀ Js) ⊆ J
f : α
hI : M.Indep (insert f (J \ {e}))
hiX : ⋂₀ Js ⊆ insert f (J \ {e})
heEI : e ∈ M.E \ insert f (J \ {e})
hJI : M.IsBasis J (insert e (insert f (J \ {e})))
hIb : M.IsBasis (insert f (J \ {e})) (insert e (insert f (J \ {e})))
hfIJ : f ∈ insert f (J \ {e}) \ J
hfb : M.IsBasis (insert f (J \ {e})) (insert e (insert f (J \ {e})))
X : Set α
hX' : X ∈ Js
hfX : f ∉ X
hd : M.Dep (insert e X)
hIs : X ⊆ insert f (J \ {e})
⊢ X ⊆ J \ {e}

Tactic:
rw [← singleton_union, ← diff_subset_iff, diff_singleton_eq_self hfX] at hIs

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

Tactic:
hIs.trans diff_subset

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

Tactic:
exact hIs.trans diff_subset

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

Tactic:
heEI.2 (hIs _ hX' heX)

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

Tactic:
exact heEI.2 (hIs _ hX' heX)

Premises used: And.right
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
ι : Sort u_3
hι : Nonempty ι
Is : ι → Set α
h : M.Indep (⋃ (i : ι), Is i)
⊢ ∀ J ∈ range Is, J ⊆ ⋃ (i : ι), Is i

Tactic:
simp [subset_iUnion]

Premises used: Set.subset_iUnion
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
ι : Sort u_3
hι : Nonempty ι
Is : ι → Set α
h : M.Indep (⋃ (i : ι), Is i)
h₁ : Eq.{u_2 + 1} (α := Set α) (⋂ (i : ι), M.closure (Is i)) (⋂ J ∈ range Is, M.closure J)
⊢ M.closure (⋂ (i : ι), Is i) = ⋂ (i : ι), M.closure (Is i)

Tactic:
convert!
    h.closure_sInter_eq_biInter_closure_of_forall_subset (range_nonempty Is)
      (by simp [subset_iUnion])

Premises used: Set.range_nonempty, Matroid.Indep.closure_sInter_eq_biInter_closure_of_forall_subset
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
ι : Sort u_3
hι : Nonempty ι
Is : ι → Set α
h : M.Indep (⋃ (i : ι), Is i)
⊢ Eq.{u_2 + 1} (α := Set α) (⋂ (i : ι), M.closure (Is i)) (⋂ J ∈ range Is, M.closure J)

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
Is : Set (Set α)
hIs : Is.Nonempty
h : M.Indep (⋃₀ Is)
⊢ M.closure (⋂₀ Is) = ⋂ I ∈ Is, M.closure I

Tactic:
h.closure_sInter_eq_biInter_closure_of_forall_subset hIs (fun _ ↦ subset_sUnion_of_mem)

Premises used: Set.subset_sUnion_of_mem, Matroid.Indep.closure_sInter_eq_biInter_closure_of_forall_subset
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
ι : Type u_4
A : Set ι
hA : A.Nonempty
I : ι → Set α
h : M.Indep (⋃ i ∈ A, I i)
⊢ Nonempty.{u_4 + 1} (↑A : Type u_4)

Tactic:
have := hA.coe_sort
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
ι : Type u_4
A : Set ι
hA : A.Nonempty
I : ι → Set α
h : M.Indep (⋃ i ∈ A, I i)
this : Nonempty.{u_4 + 1} (↑A : Type u_4)
⊢ M.Indep (⋃ (i : (↑A : Type u_4)), (fun (i : (↑A : Type u_4)) ↦ I (↑i : ι)) i)

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
ι : Type u_4
A : Set ι
hA : A.Nonempty
I : ι → Set α
h : M.Indep (⋃ i ∈ A, I i)
this : Nonempty.{u_4 + 1} (↑A : Type u_4)
h₁ : Eq.{u_2 + 1} (α := Set α) (⋂ i ∈ A, I i) (⋂ (i : (↑A : Type u_4)), I (↑i : ι))
h₂ : Eq.{u_2 + 1} (α := Set α) (⋂ i ∈ A, M.closure (I i)) (⋂ (i : (↑A : Type u_4)), M.closure (I (↑i : ι)))
⊢ M.closure (⋂ i ∈ A, I i) = ⋂ i ∈ A, M.closure (I i)

Tactic:
convert! closure_iInter_eq_iInter_closure_of_iUnion_indep (Is := fun i : A ↦ I i) (by simpa)

Premises used: Matroid.closure_iInter_eq_iInter_closure_of_iUnion_indep, Subtype.val
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
ι : Type u_4
A : Set ι
hA : A.Nonempty
I : ι → Set α
h : M.Indep (⋃ i ∈ A, I i)
this : Nonempty.{u_4 + 1} (↑A : Type u_4)
⊢ Eq.{u_2 + 1} (α := Set α) (⋂ i ∈ A, I i) (⋂ (i : (↑A : Type u_4)), I (↑i : ι))

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
ι : Type u_4
A : Set ι
hA : A.Nonempty
I : ι → Set α
h : M.Indep (⋃ i ∈ A, I i)
this : Nonempty.{u_4 + 1} (↑A : Type u_4)
⊢ Eq.{u_2 + 1} (α := Set α) (⋂ i ∈ A, M.closure (I i)) (⋂ (i : (↑A : Type u_4)), M.closure (I (↑i : ι)))

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
ι : Sort u_3
I : Set α
inst : Nonempty ι
Js : ι → Set α
hI : M.Indep I
hJs : ∀ (i : ι), Js i ⊆ I
⊢ ⋃ (i : ι), Js i ⊆ I

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I J : Set α
h : M.Indep (I ∪ J)
rw :
  Eq.{u_2 + 1} (α := Set α) (⋂ (i : Bool), M.closure (bif i then I else J))
    (⋂ (b : Bool), bif b then M.closure I else M.closure J)
h₁ : M.Indep (⋃ (i : Bool), bif i then I else J)
⊢ M.closure (I ∩ J) = M.closure I ∩ M.closure J

Tactic:
rw [inter_eq_iInter, closure_iInter_eq_iInter_closure_of_iUnion_indep, inter_eq_iInter]

Premises used: Matroid.closure_iInter_eq_iInter_closure_of_iUnion_indep, Set.inter_eq_iInter
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I J : Set α
h : M.Indep (I ∪ J)
⊢ ∀ (i : Bool), M.closure (bif i then I else J) = bif i then M.closure I else M.closure J

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I J : Set α
h : M.Indep (I ∪ J)
⊢ Eq.{u_2 + 1} (α := Set α) (⋂ (i : Bool), M.closure (bif i then I else J))
    (⋂ (b : Bool), bif b then M.closure I else M.closure J)

Tactic:
exact iInter_congr (by simp)

Premises used: Set.iInter_congr
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I J : Set α
h h₁ h₂ h₃ h₄ : M.Indep (I ∪ J)
⊢ M.Indep (⋃ (i : Bool), bif i then I else J)

Tactic:
rwa [← union_eq_iUnion]

Premises used: Set.union_eq_iUnion
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I : Set α
ι : Type u_4
hI : M.Indep I
X : ι → Set α
A : Set ι
hA : A.Nonempty
h : ∀ i ∈ A, M.IsBasis (X i ∩ I) (X i)
⊢ M.IsBasis ((⋂ i ∈ A, X i) ∩ I) (⋂ i ∈ A, X i)

Tactic:
(hI.inter_left _).isBasis_of_subset_of_subset_closure inter_subset_left ?_

Premises used: Set.inter_subset_left, Matroid.Indep.inter_left, Matroid.Indep.isBasis_of_subset_of_subset_closure
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I : Set α
ι : Type u_4
hI : M.Indep I
X : ι → Set α
A : Set ι
hA : A.Nonempty
h : ∀ i ∈ A, M.IsBasis (X i ∩ I) (X i)
refine : ⋂ i ∈ A, X i ⊆ M.closure ((⋂ i ∈ A, X i) ∩ I)
⊢ M.IsBasis ((⋂ i ∈ A, X i) ∩ I) (⋂ i ∈ A, X i)

Tactic:
refine (hI.inter_left _).isBasis_of_subset_of_subset_closure inter_subset_left ?_

Premises used: Set.inter_subset_left, Matroid.Indep.inter_left, Matroid.Indep.isBasis_of_subset_of_subset_closure
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I : Set α
ι : Type u_4
hI : M.Indep I
X : ι → Set α
A : Set ι
hA : A.Nonempty
h : ∀ i ∈ A, M.IsBasis (X i ∩ I) (X i)
⊢ ⋃ i ∈ A, (fun (i : ι) ↦ X i ∩ I) i ⊆ I

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I : Set α
ι : Type u_4
hI : M.Indep I
X : ι → Set α
A : Set ι
hA : A.Nonempty
h : ∀ i ∈ A, M.IsBasis (X i ∩ I) (X i)
simp_rw : ∀ (i : ι) (i_1 : i ∈ A), ⋂ i ∈ A, X i ⊆ M.closure (X i ∩ I)
⊢ ⋂ i ∈ A, X i ⊆ M.closure ((⋂ i ∈ A, X i) ∩ I)

Tactic:
simp_rw [← biInter_inter hA,
  closure_biInter_eq_biInter_closure_of_biUnion_indep hA (I := fun i ↦ (X i) ∩ I)
      (hI.subset (by simp)), subset_iInter_iff]

Premises used: Set.biInter_inter, Set.subset_iInter_iff, Matroid.closure_biInter_eq_biInter_closure_of_biUnion_indep, Matroid.Indep.subset
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I : Set α
ι : Type u_4
hI : M.Indep I
X : ι → Set α
A : Set ι
hA : A.Nonempty
h : ∀ i ∈ A, M.IsBasis (X i ∩ I) (X i)
⊢ ∀ (i : ι) (i_1 : i ∈ A), ⋂ i ∈ A, X i ⊆ M.closure (X i ∩ I)

Tactic:
fun i hiA ↦ (biInter_subset_of_mem hiA).trans (h i hiA).subset_closure

Premises used: HasSubset.Subset.trans, Set.biInter_subset_of_mem, Matroid.IsBasis.subset_closure
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I : Set α
ι : Type u_4
hI : M.Indep I
X : ι → Set α
A : Set ι
hA : A.Nonempty
h : ∀ i ∈ A, M.IsBasis (X i ∩ I) (X i)
⊢ ∀ (i : ι) (i_1 : i ∈ A), ⋂ i ∈ A, X i ⊆ M.closure (X i ∩ I)

Tactic:
exact fun i hiA ↦ (biInter_subset_of_mem hiA).trans (h i hiA).subset_closure

Premises used: HasSubset.Subset.trans, Set.biInter_subset_of_mem, Matroid.IsBasis.subset_closure