awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
ι : Sort u_3
I : Set α
inst : Nonempty ι
X : ι → Set α
hI : M.Indep I
h : ∀ (i : ι), M.IsBasis (X i ∩ I) (X i)
⊢ ∀ (i : PLift ι),
    Membership.mem (γ := Set (PLift ι)) univ i →
      M.IsBasis ((fun (i : PLift ι) ↦ X i.down) i ∩ I) ((fun (i : PLift ι) ↦ X i.down) i)

Tactic:
simpa using fun (i : PLift ι) ↦ h i.down

Premises used: PLift.down
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
ι : Sort u_3
I : Set α
inst : Nonempty ι
X : ι → Set α
hI : M.Indep I
h : ∀ (i : ι), M.IsBasis (X i ∩ I) (X i)
h₁ h₂ :
  Eq.{u_2 + 1} (α := Set α) (⋂ (i : ι), X i)
    (⋂ (i : PLift ι), ⋂ (_ : Membership.mem (γ := Set (PLift ι)) univ i), X i.down)
⊢ M.IsBasis ((⋂ (i : ι), X i) ∩ I) (⋂ (i : ι), X i)

Tactic:
convert!
    hI.inter_isBasis_biInter (ι := PLift ι) univ_nonempty (X := fun i ↦ X i.down)
      (by simpa using fun (i : PLift ι) ↦ h i.down)

Premises used: Set.univ_nonempty, Matroid.Indep.inter_isBasis_biInter
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
ι : Sort u_3
I : Set α
inst : Nonempty ι
X : ι → Set α
hI : M.Indep I
h : ∀ (i : ι), M.IsBasis (X i ∩ I) (X i)
h₁ : Eq.{u_2 + 1} (α := Set α) (⋂ (i : ι), X i) (⋂ (i : PLift ι), X i.down)
⊢ Eq.{u_2 + 1} (α := Set α) (⋂ (i : ι), X i)
    (⋂ (i : PLift ι), ⋂ (_ : Membership.mem (γ := Set (PLift ι)) univ i), X i.down)

Tactic:
simp only [mem_univ, iInter_true]

Premises used: Set.mem_univ, Set.iInter_true
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
ι : Sort u_3
I : Set α
inst : Nonempty ι
X : ι → Set α
hI : M.Indep I
h : ∀ (i : ι), M.IsBasis (X i ∩ I) (X i)
⊢ Eq.{u_2 + 1} (α := Set α) (⋂ (i : ι), X i) (⋂ (i : PLift ι), X i.down)

Tactic:
(iInter_plift_down X).symm

Premises used: Set.iInter_plift_down, Eq.symm
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
ι : Sort u_3
I : Set α
inst : Nonempty ι
X : ι → Set α
hI : M.Indep I
h : ∀ (i : ι), M.IsBasis (X i ∩ I) (X i)
⊢ Eq.{u_2 + 1} (α := Set α) (⋂ (i : ι), X i) (⋂ (i : PLift ι), X i.down)

Tactic:
exact (iInter_plift_down X).symm

Premises used: Set.iInter_plift_down, Eq.symm
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I : Set α
Xs : Set (Set α)
hI : M.Indep I
hXs : Xs.Nonempty
h : ∀ X ∈ Xs, M.IsBasis (X ∩ I) X
rw : M.IsBasis ((⋂ i ∈ Xs, i) ∩ I) (⋂ i ∈ Xs, i)
⊢ M.IsBasis (⋂₀ Xs ∩ I) (⋂₀ Xs)

Tactic:
rw [sInter_eq_biInter]

Premises used: Set.sInter_eq_biInter
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I : Set α
Xs : Set (Set α)
hI : M.Indep I
hXs : Xs.Nonempty
h : ∀ X ∈ Xs, M.IsBasis (X ∩ I) X
⊢ M.IsBasis ((⋂ i ∈ Xs, i) ∩ I) (⋂ i ∈ Xs, i)

Tactic:
hI.inter_isBasis_biInter hXs h

Premises used: Matroid.Indep.inter_isBasis_biInter
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I : Set α
Xs : Set (Set α)
hI : M.Indep I
hXs : Xs.Nonempty
h : ∀ X ∈ Xs, M.IsBasis (X ∩ I) X
⊢ M.IsBasis ((⋂ i ∈ Xs, i) ∩ I) (⋂ i ∈ Xs, i)

Tactic:
exact hI.inter_isBasis_biInter hXs h

Premises used: Matroid.Indep.inter_isBasis_biInter
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X I : Set α
hIX : I ⊆ X
hX : X ⊆ M.E
⊢ M.IsBasis I X ↔ M.IsBasis I (M.closure X)

Tactic:
⟨fun h ↦ h.isBasis_closure_right, fun h ↦ h.isBasis_subset hIX (M.subset_closure X hX)⟩

Premises used: Matroid.IsBasis.isBasis_subset, Matroid.subset_closure, Matroid.IsBasis.isBasis_closure_right, Iff.intro
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X I : Set α
hIX : I ⊆ X
⊢ M.IsBasis I X ↔ M.IsBasis I (M.closure X) ∧ X ⊆ M.E

Tactic:
⟨fun h ↦ ⟨h.isBasis_closure_right, h.subset_ground⟩,
    fun h ↦ h.1.isBasis_subset hIX (M.subset_closure X h.2)⟩

Premises used: Matroid.IsBasis.subset_ground, Matroid.IsBasis.isBasis_subset, Matroid.subset_closure, Matroid.IsBasis.isBasis_closure_right, And.right, And.left, And.intro, Iff.intro
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X I : Set α
rw : M.IsBasis I (X ∩ M.E) ↔ M.IsBasis I (M.closure (X ∩ M.E)) ∧ I ⊆ X
⊢ M.IsBasis' I X ↔ M.IsBasis I (M.closure X) ∧ I ⊆ X

Tactic:
rw [← closure_inter_ground, isBasis'_iff_isBasis_inter_ground]

Premises used: Matroid.isBasis'_iff_isBasis_inter_ground, Matroid.closure_inter_ground
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X I : Set α
⊢ M.IsBasis I (X ∩ M.E) ↔ M.IsBasis I (M.closure (X ∩ M.E)) ∧ I ⊆ X

Tactic:
⟨fun h ↦ ⟨h.isBasis_closure_right, h.subset.trans inter_subset_left⟩,
    fun h ↦ h.1.isBasis_subset (subset_inter h.2 h.1.indep.subset_ground) (M.subset_closure _)⟩

Premises used: Matroid.E, Matroid.IsBasis.isBasis_subset, HasSubset.Subset.trans, Matroid.subset_closure, Set.inter_subset_left, Matroid.IsBasis.subset, Matroid.IsBasis.isBasis_closure_right, Inter.inter, Matroid.Indep.subset_ground, Set.subset_inter, And.right, And.left, And.intro, Iff.intro, Matroid.IsBasis.indep
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X I : Set α
⊢ M.IsBasis I (X ∩ M.E) ↔ M.IsBasis I (M.closure (X ∩ M.E)) ∧ I ⊆ X

Tactic:
exact ⟨fun h ↦ ⟨h.isBasis_closure_right, h.subset.trans inter_subset_left⟩,
    fun h ↦ h.1.isBasis_subset (subset_inter h.2 h.1.indep.subset_ground) (M.subset_closure _)⟩
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X : Set α
obtain : ∀ (I : Set α) (hI : M.IsBasis I (X ∩ M.E)), ∃ (I : Set α), M.IsBasis I (X ∩ M.E) ∧ M.IsBasis I (M.closure X)
⊢ ∃ (I : Set α), M.IsBasis I (X ∩ M.E) ∧ M.IsBasis I (M.closure X)

Tactic:
obtain ⟨I, hI⟩ := M.exists_isBasis (X ∩ M.E)

Premises used: Matroid.E, Inter.inter, Matroid.exists_isBasis
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X I : Set α
hI : M.IsBasis I (X ∩ M.E)
⊢ M.IsBasis I (M.closure (X ∩ M.E))

Tactic:
have hI' := hI.isBasis_closure_right
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X I : Set α
hI : M.IsBasis I (X ∩ M.E)
hI' : M.IsBasis I (M.closure (X ∩ M.E))
⊢ M.IsBasis I (M.closure X)

Tactic:
rw [closure_inter_ground] at hI'

Premises used: Matroid.closure_inter_ground
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X I : Set α
hI : M.IsBasis I (X ∩ M.E)
hI' : M.IsBasis I (M.closure X)
⊢ ∃ (I : Set α), M.IsBasis I (X ∩ M.E) ∧ M.IsBasis I (M.closure X)

Tactic:
⟨_, hI, hI'⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X I : Set α
hI : M.IsBasis I (X ∩ M.E)
hI' : M.IsBasis I (M.closure X)
⊢ ∃ (I : Set α), M.IsBasis I (X ∩ M.E) ∧ M.IsBasis I (M.closure X)

Tactic:
exact ⟨_, hI, hI'⟩
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X Y I : Set α
hI : M.IsBasis I X
hY : I ⊆ Y
h : M.closure X = M.closure Y
hYE : Y ⊆ M.E
⊢ M.IsBasis I Y

Tactic:
hI.indep.isBasis_of_subset_of_subset_closure hY ?_

Premises used: Matroid.IsBasis.indep, Matroid.Indep.isBasis_of_subset_of_subset_closure
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X Y I : Set α
hI : M.IsBasis I X
hY : I ⊆ Y
h : M.closure X = M.closure Y
hYE : Y ⊆ M.E
refine : Y ⊆ M.closure I
⊢ M.IsBasis I Y

Tactic:
refine hI.indep.isBasis_of_subset_of_subset_closure hY ?_

Premises used: Matroid.IsBasis.indep, Matroid.Indep.isBasis_of_subset_of_subset_closure
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X Y I : Set α
hI : M.IsBasis I X
hY : I ⊆ Y
h : M.closure X = M.closure Y
hYE : Y ⊆ M.E
rw : Y ⊆ M.closure Y
⊢ Y ⊆ M.closure I

Tactic:
rw [hI.closure_eq_closure, h]

Premises used: Matroid.IsBasis.closure_eq_closure
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X Y I : Set α
hI : M.IsBasis I X
hY : I ⊆ Y
h : M.closure X = M.closure Y
hYE : Y ⊆ M.E
⊢ Y ⊆ M.closure Y

Tactic:
M.subset_closure Y

Premises used: Matroid.subset_closure
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X Y I : Set α
hI : M.IsBasis I X
hY : I ⊆ Y
h : M.closure X = M.closure Y
hYE : Y ⊆ M.E
⊢ Y ⊆ M.closure Y

Tactic:
exact M.subset_closure Y

Premises used: Matroid.subset_closure
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X I : Set α
⊢ M.IsBasis I (I ∪ X) ↔ M.Indep I ∧ X ⊆ M.closure I

Tactic:
⟨fun h ↦ ⟨h.indep, subset_union_right.trans h.subset_closure⟩, fun ⟨hI, hXI⟩ ↦
    hI.isBasis_closure.isBasis_subset subset_union_left (union_subset (M.subset_closure I) hXI)⟩

Premises used: _private.0.Matroid.isBasis_union_iff_indep_closure.match_1, Matroid.Indep.isBasis_closure, Matroid.IsBasis.isBasis_subset, Set.subset_union_right, HasSubset.Subset.trans, Matroid.subset_closure, Set.union_subset, Set.subset_union_left, And.intro, Iff.intro, Matroid.IsBasis.indep, Union.union, Matroid.IsBasis, Matroid.IsBasis.subset_closure
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X I : Set α
⊢ M.IsBasis I X ↔ M.Indep I ∧ X ⊆ M.closure I ∧ I ⊆ X

Tactic:
⟨fun h ↦ ⟨h.indep, h.subset_closure, h.subset⟩, fun h ↦
    (isBasis_union_iff_indep_closure.mpr ⟨h.1, h.2.1⟩).isBasis_subset h.2.2 subset_union_right⟩

Premises used: Iff.mpr, Matroid.IsBasis.isBasis_subset, Set.subset_union_right, Matroid.IsBasis.subset, And.right, And.left, And.intro, Iff.intro, Matroid.isBasis_union_iff_indep_closure, Matroid.IsBasis.indep, Matroid.IsBasis.subset_closure
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I X : Set α
hI : M.Indep I
⊢ M.IsBasis (X ∩ I) X ↔ X ⊆ M.closure (X ∩ I)

Tactic:
⟨IsBasis.subset_closure, (hI.inter_left X).isBasis_of_subset_of_subset_closure inter_subset_left⟩

Premises used: Set.inter_subset_left, Matroid.Indep.inter_left, Iff.intro, Matroid.IsBasis.subset_closure, Matroid.Indep.isBasis_of_subset_of_subset_closure
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X I : Set α
h : M.IsBasis (X ∩ I) X
hI : M.Indep I
rw : ∀ (h : X ⊆ M.closure (X ∩ I)) (hI : M.Indep I), M.closure X ⊆ M.closure (M.closure X ∩ I)
⊢ M.IsBasis (M.closure X ∩ I) (M.closure X)

Tactic:
rw [hI.inter_isBasis_closure_iff_subset_closure_inter] at h ⊢

Premises used: Matroid.Indep.inter_isBasis_closure_iff_subset_closure_inter
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X I : Set α
h : X ⊆ M.closure (X ∩ I)
hI : M.Indep I
⊢ M.closure X ⊆ M.closure (M.closure X ∩ I)

Tactic:
(M.closure_subset_closure_of_subset_closure h).trans (M.closure_subset_closure
    (inter_subset_inter_left _ (h.trans (M.closure_subset_closure inter_subset_left))))

Premises used: HasSubset.Subset.trans, Set.inter_subset_left, Matroid.closure_subset_closure_of_subset_closure, Matroid.closure_subset_closure, Set.inter_subset_inter_left
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X I : Set α
h : X ⊆ M.closure (X ∩ I)
hI : M.Indep I
⊢ M.closure X ⊆ M.closure (M.closure X ∩ I)

Tactic:
exact (M.closure_subset_closure_of_subset_closure h).trans (M.closure_subset_closure
    (inter_subset_inter_left _ (h.trans (M.closure_subset_closure inter_subset_left))))

Premises used: HasSubset.Subset.trans, Set.inter_subset_left, Matroid.closure_subset_closure_of_subset_closure, Matroid.closure_subset_closure, Set.inter_subset_inter_left
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X I J : Set α
hI : M.IsBasis I X
hJI : J ⊆ I
hJ : X ⊆ M.closure J
rw : I ⊆ M.closure J
⊢ J = I

Tactic:
rw [← hI.indep.closure_inter_eq_self_of_subset hJI, inter_eq_self_of_subset_right]

Premises used: Matroid.Indep.closure_inter_eq_self_of_subset, Set.inter_eq_self_of_subset_right, Matroid.IsBasis.indep
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X I J : Set α
hI : M.IsBasis I X
hJI : J ⊆ I
hJ : X ⊆ M.closure J
⊢ I ⊆ M.closure J

Tactic:
hI.subset.trans hJ

Premises used: HasSubset.Subset.trans, Matroid.IsBasis.subset
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X I J : Set α
hI : M.IsBasis I X
hJI : J ⊆ I
hJ : X ⊆ M.closure J
⊢ I ⊆ M.closure J

Tactic:
exact hI.subset.trans hJ

Premises used: HasSubset.Subset.trans, Matroid.IsBasis.subset
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X : Set α
e : α
I : Set α
hIX : M.IsBasis I X
heI : e ∉ M.closure I
heE : e ∈ M.E
⊢ M.IsBasis (insert e I) (insert e X)

Tactic:
hIX.insert_isBasis_insert <| hIX.indep.insert_indep_iff.2 <| .inl ⟨heE, heI⟩

Premises used: Iff.mpr, Matroid.Indep.insert_indep_iff, And.intro, Or.inl, Matroid.IsBasis.indep, Matroid.IsBasis.insert_isBasis_insert
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X : Set α
rw : M.Indep ∅ ∧ X ⊆ M.closure ∅ ∧ ∅ ⊆ X ↔ X ⊆ M.closure ∅
rw₁ : X ⊆ M.closure ∅ ∧ ∅ ⊆ X ↔ X ⊆ M.closure ∅
rw₂ rw₃ : X ⊆ M.closure ∅ ↔ X ⊆ M.closure ∅
⊢ M.IsBasis ∅ X ↔ X ⊆ M.closure ∅

Tactic:
rw [isBasis_iff_indep_closure, and_iff_right M.empty_indep, and_iff_left (empty_subset _)]

Premises used: and_iff_left, and_iff_right, Matroid.empty_indep, Set.empty_subset, Matroid.isBasis_iff_indep_closure
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I : Set α
hI : I ⊆ M.E
mpr : (∀ ⦃e : α⦄, e ∈ I → e ∉ M.closure (I \ {e})) → M.Indep I
⊢ M.Indep I ↔ ∀ ⦃e : α⦄, e ∈ I → e ∉ M.closure (I \ {e})

Tactic:
use fun h e heI he ↦ ((h.closure_inter_eq_self_of_subset diff_subset).subset ⟨he, heI⟩).2 rfl
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I : Set α
hI : I ⊆ M.E
h : ∀ ⦃e : α⦄, e ∈ I → e ∉ M.closure (I \ {e})
mpr : ∀ (J : Set α) (hJ : M.IsBasis J I), M.Indep I
⊢ M.Indep I

Tactic:
obtain ⟨J, hJ⟩ := M.exists_isBasis I

Premises used: Matroid.exists_isBasis
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I : Set α
hI : I ⊆ M.E
h : ∀ ⦃e : α⦄, e ∈ I → e ∉ M.closure (I \ {e})
J : Set α
hJ : M.IsBasis J I
⊢ M.Indep J

Tactic:
hJ.indep

Premises used: Matroid.IsBasis.indep
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I : Set α
hI : I ⊆ M.E
h : ∀ ⦃e : α⦄, e ∈ I → e ∉ M.closure (I \ {e})
J : Set α
hJ : M.IsBasis J I
h₁ : I = J
⊢ M.Indep I

Tactic:
convert! hJ.indep

Premises used: Matroid.IsBasis.indep
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I : Set α
hI : I ⊆ M.E
h : ∀ ⦃e : α⦄, e ∈ I → e ∉ M.closure (I \ {e})
J : Set α
hJ : M.IsBasis J I
⊢ I = J

Tactic:
hJ.subset.antisymm' (fun e he ↦ by_contra fun heJ ↦ h he ?_)

Premises used: Matroid.IsBasis.subset, by_contra, HasSubset.Subset.antisymm'
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I : Set α
hI : I ⊆ M.E
h : ∀ ⦃e : α⦄, e ∈ I → e ∉ M.closure (I \ {e})
J : Set α
hJ : M.IsBasis J I
h₁ : ∀ (e : α) (he : e ∈ I) (heJ : e ∉ J), e ∈ M.closure (I \ {e})
⊢ I = J

Tactic:
refine hJ.subset.antisymm' (fun e he ↦ by_contra fun heJ ↦ h he ?_)

Premises used: Matroid.IsBasis.subset, by_contra, HasSubset.Subset.antisymm'
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I : Set α
hI : I ⊆ M.E
h : ∀ ⦃e : α⦄, e ∈ I → e ∉ M.closure (I \ {e})
J : Set α
hJ : M.IsBasis J I
e : α
he : e ∈ I
heJ : e ∉ J
⊢ e ∈ M.closure (I \ {e})

Tactic:
mem_of_mem_of_subset
    (hJ.subset_closure he) (M.closure_subset_closure (subset_diff_singleton hJ.subset heJ))

Premises used: Matroid.IsBasis.subset, Matroid.closure_subset_closure, Set.subset_diff_singleton, Set.mem_of_mem_of_subset, Matroid.IsBasis.subset_closure
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I : Set α
hI : I ⊆ M.E
h : ∀ ⦃e : α⦄, e ∈ I → e ∉ M.closure (I \ {e})
J : Set α
hJ : M.IsBasis J I
e : α
he : e ∈ I
heJ : e ∉ J
⊢ e ∈ M.closure (I \ {e})

Tactic:
exact mem_of_mem_of_subset
    (hJ.subset_closure he) (M.closure_subset_closure (subset_diff_singleton hJ.subset heJ))

Premises used: Matroid.IsBasis.subset, Matroid.closure_subset_closure, Set.subset_diff_singleton, Set.mem_of_mem_of_subset, Matroid.IsBasis.subset_closure
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I : Set α
⊢ M.Indep I ↔ I ⊆ M.E ∧ ∀ e ∈ I, e ∉ M.closure (I \ {e})

Tactic:
⟨fun h ↦ ⟨h.subset_ground, (indep_iff_forall_notMem_closure_diff h.subset_ground).mp h⟩, fun h ↦
    (indep_iff_forall_notMem_closure_diff h.1).mpr h.2⟩

Premises used: Iff.mpr, Matroid.Indep.subset_ground, And.right, And.left, And.intro, Iff.intro, Iff.mp, Matroid.indep_iff_forall_notMem_closure_diff
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
he : e ∈ I
⊢ e ∉ M.closure (I \ {e})

Tactic:
(indep_iff_forall_notMem_closure_diff'.1 hI).2 e he

Premises used: Matroid.indep_iff_forall_notMem_closure_diff', And.right, Iff.mp
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
e f : α
I : Set α
hI : M.Indep I
hf : f ∈ M.closure I
he : e ∈ M.closure (insert f I \ {e})
a : M.closure (insert f I \ {e}) ⊆ M.closure I
a₁ : M.closure I ⊆ M.closure (insert f I \ {e})
⊢ M.closure (insert f I \ {e}) = M.closure I

Tactic:
apply subset_antisymm

Premises used: subset_antisymm
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
e f : α
I : Set α
hI : M.Indep I
hf : f ∈ M.closure I
he : e ∈ M.closure (insert f I \ {e})
a : insert f I \ {e} ⊆ M.closure I
⊢ M.closure (insert f I \ {e}) ⊆ M.closure I

Tactic:
apply closure_subset_closure_of_subset_closure

Premises used: Matroid.closure_subset_closure_of_subset_closure
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
e f : α
I : Set α
hI : M.Indep I
hf : f ∈ M.closure I
he : e ∈ M.closure (insert f I \ {e})
a : I ⊆ M.closure (insert f I \ {e})
⊢ M.closure I ⊆ M.closure (insert f I \ {e})

Tactic:
apply closure_subset_closure_of_subset_closure

Premises used: Matroid.closure_subset_closure_of_subset_closure
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
a : α
right : ¬a = e
hf : a ∈ M.closure I
he : e ∈ M.closure (insert a I \ {e})
⊢ a ∈ M.closure I

Tactic:
hf
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
e f : α
I : Set α
hI : M.Indep I
hf : f ∈ M.closure I
he : e ∈ M.closure (insert f I \ {e})
a : α
right : ¬a = e
haI : a ∈ I
⊢ a ∈ M.closure I

Tactic:
M.subset_closure _ hI.subset_ground haI

Premises used: Matroid.subset_closure, Matroid.Indep.subset_ground
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
a : α
right : ¬a = e
hf : a ∈ M.closure I
he : e ∈ M.closure (insert a I \ {e})
⊢ a ∈ M.closure I

Tactic:
exacts [hf, M.subset_closure _ hI.subset_ground haI]
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
e f : α
I : Set α
hI : M.Indep I
hf : f ∈ M.closure I
he : e ∈ M.closure (insert f I \ {e})
a : α
haI : a ∈ I
a₁ : ∀ (he : a ∈ M.closure (insert f I \ {a})), a ∈ M.closure (insert f I \ {a})
a₂ : ∀ (ne : a ≠ e), a ∈ M.closure (insert f I \ {e})
⊢ a ∈ M.closure (insert f I \ {e})

Tactic:
obtain rfl | ne := eq_or_ne a e

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
f : α
I : Set α
hI : M.Indep I
hf : f ∈ M.closure I
a : α
haI : a ∈ I
he : a ∈ M.closure (insert f I \ {a})
⊢ a ∈ M.closure (insert f I \ {a})

Tactic:
he
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
e f : α
I : Set α
hI : M.Indep I
hf : f ∈ M.closure I
he : e ∈ M.closure (insert f I \ {e})
a : α
haI : a ∈ I
ne : a ≠ e
⊢ a ∈ M.closure (insert f I \ {e})

Tactic:
M.mem_closure_of_mem' ⟨.inr haI, ne⟩ (hI.subset_ground haI)

Premises used: Matroid.mem_closure_of_mem', Matroid.Indep.subset_ground, And.intro, Or.inr
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
f : α
I : Set α
hI : M.Indep I
hf : f ∈ M.closure I
a : α
haI : a ∈ I
he : a ∈ M.closure (insert f I \ {a})
⊢ a ∈ M.closure (insert f I \ {a})

Tactic:
exacts [he, M.mem_closure_of_mem' ⟨.inr haI, ne⟩ (hI.subset_ground haI)]
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
e f : α
I : Set α
hI : M.Indep I
hfI : f ∈ M.closure I
he : e ∈ M.closure (insert f I \ {e})
heI : e ∈ insert f I
⊢ e = f ∨ e ∈ I

Tactic:
simp only [mem_insert_iff] at heI

Premises used: Set.mem_insert_iff
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
e f : α
I : Set α
hI : M.Indep I
hfI : f ∈ M.closure I
he : e ∈ M.closure (insert f I \ {e})
heI : e = f ∨ e ∈ I
inl : ∀ (hfI : e ∈ M.closure I) (he : e ∈ M.closure (insert e I \ {e})), M.Indep (insert e I \ {e})
inr : ∀ (heI : e ∈ I), M.Indep (insert f I \ {e})
⊢ M.Indep (insert f I \ {e})

Tactic:
obtain rfl | heI := heI

Premises used: rfl
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
hfI : e ∈ M.closure I
he : e ∈ M.closure (insert e I \ {e})
⊢ insert e I \ {e} ⊆ I

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
hfI : e ∈ M.closure I
he : e ∈ M.closure (insert e I \ {e})
⊢ M.Indep (insert e I \ {e})

Tactic:
exact hI.subset (by simp)

Premises used: Matroid.Indep.subset
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
e f : α
I : Set α
hI : M.Indep I
hfI : f ∈ M.closure I
he : e ∈ M.closure (insert f I \ {e})
heI : e ∈ I
inr : f ∈ M.E \ M.closure (I \ {e}) ∨ f ∈ I
⊢ M.Indep (insert f I \ {e})

Tactic:
rw [Indep.insert_diff_indep_iff (hI.subset (diff_subset ..)) heI]

Premises used: Set.diff_subset, Matroid.Indep.subset, Matroid.Indep.insert_diff_indep_iff
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
e f : α
I : Set α
hI : M.Indep I
hfI : f ∈ M.closure I
he : e ∈ M.closure (insert f I \ {e})
heI : e ∈ I
⊢ f ∈ M.E \ M.closure (I \ {e}) ∨ f ∈ I

Tactic:
.inl ⟨mem_ground_of_mem_closure hfI, fun h ↦ hI.notMem_closure_diff_of_mem heI ?_⟩

Premises used: Matroid.Indep.notMem_closure_diff_of_mem, And.intro, Or.inl, Matroid.mem_ground_of_mem_closure
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
e f : α
I : Set α
hI : M.Indep I
hfI : f ∈ M.closure I
he : e ∈ M.closure (insert f I \ {e})
heI : e ∈ I
inr : ∀ (h : f ∈ M.closure (I \ {e})), e ∈ M.closure (I \ {e})
⊢ f ∈ M.E \ M.closure (I \ {e}) ∨ f ∈ I

Tactic:
refine .inl ⟨mem_ground_of_mem_closure hfI, fun h ↦ hI.notMem_closure_diff_of_mem heI ?_⟩
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
e f : α
I : Set α
hI : M.Indep I
hfI : f ∈ M.closure I
he : e ∈ M.closure (insert f I \ {e})
heI : e ∈ I
h : f ∈ M.closure (I \ {e})
a : α
⊢ a ∈ insert f I \ {e} → a ∈ insert f (I \ {e})

Tactic:
simp_all
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
e f : α
I : Set α
hI : M.Indep I
hfI : f ∈ M.closure I
he : e ∈ M.closure (insert f I \ {e})
heI : e ∈ I
h : f ∈ M.closure (I \ {e})
⊢ e ∈ M.closure (I \ {e})

Tactic:
exact closure_insert_eq_of_mem_closure h ▸ M.closure_subset_closure (by intro; simp_all) he
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X : Set α
e f : α
B : Set α
hB : M.IsBasis B X
he : e ∈ M.closure (insert f B \ {e})
heB : e ∈ insert f B
hfX : f ∈ X
rw :
  ∀ (hB : M.Indep B ∧ X ⊆ M.closure B ∧ B ⊆ X) (he : e ∈ M.closure (insert f B \ {e})) (heB : e ∈ insert f B)
    (hfX : f ∈ X), M.Indep (insert f B \ {e}) ∧ X ⊆ M.closure (insert f B \ {e}) ∧ insert f B \ {e} ⊆ X
⊢ M.IsBasis (insert f B \ {e}) X

Tactic:
rw [isBasis_iff_indep_closure] at hB ⊢

Premises used: Matroid.isBasis_iff_indep_closure