awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
ι : Type u_1
α : Type u_2
M : Matroid α
Xs Ys : ι → Set α
A : Set ι
h : ∀ i ∈ A, M.closure (Xs i) = M.closure (Ys i)
rw : M.closure (⋃ i ∈ A, M.closure (Xs i)) = M.closure (⋃ i ∈ A, Ys i)
rw₁ : M.closure (⋃ i ∈ A, M.closure (Ys i)) = M.closure (⋃ i ∈ A, Ys i)
rw₂ rw₃ : M.closure (⋃ i ∈ A, Ys i) = M.closure (⋃ i ∈ A, Ys i)
⊢ M.closure (⋃ i ∈ A, Xs i) = M.closure (⋃ i ∈ A, Ys i)

Tactic:
rw [← closure_biUnion_closure_eq_closure_biUnion, iUnion₂_congr h,
    closure_biUnion_closure_eq_closure_biUnion]

Premises used: Set.iUnion₂_congr, Matroid.closure_biUnion_closure_eq_closure_biUnion
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X Y : Set α
rw :
  M.closure (⋃ (i : Bool), M.closure (bif i then X else Y)) =
    M.closure (⋃ (b : Bool), bif b then M.closure X else M.closure Y)
⊢ M.closure (M.closure X ∪ M.closure Y) = M.closure (X ∪ Y)

Tactic:
rw [eq_comm, union_eq_iUnion, ← closure_iUnion_closure_eq_closure_iUnion, union_eq_iUnion]

Premises used: Matroid.closure_iUnion_closure_eq_closure_iUnion, eq_comm, Set.union_eq_iUnion
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X Y : Set α
simp_rw :
  M.closure (⋃ (i : Bool), M.closure (if i = true then X else Y)) =
    M.closure (⋃ (b : Bool), if b = true then M.closure X else M.closure Y)
⊢ M.closure (⋃ (i : Bool), M.closure (bif i then X else Y)) =
    M.closure (⋃ (b : Bool), bif b then M.closure X else M.closure Y)

Tactic:
simp_rw [Bool.cond_eq_ite, apply_ite]

Premises used: apply_ite, Bool.cond_eq_ite
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X Y : Set α
rw : M.closure (M.closure X ∪ M.closure (M.closure Y)) = M.closure (X ∪ Y)
rw₁ : M.closure (M.closure X ∪ M.closure Y) = M.closure (X ∪ Y)
rw₂ rw₃ : M.closure (X ∪ Y) = M.closure (X ∪ Y)
⊢ M.closure (X ∪ M.closure Y) = M.closure (X ∪ Y)

Tactic:
rw [← closure_closure_union_closure_eq_closure_union, closure_closure,
    closure_closure_union_closure_eq_closure_union]

Premises used: Matroid.closure_closure, Matroid.closure_closure_union_closure_eq_closure_union
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X Y : Set α
rw : M.closure (M.closure (M.closure X) ∪ M.closure Y) = M.closure (X ∪ Y)
rw₁ : M.closure (M.closure X ∪ M.closure Y) = M.closure (X ∪ Y)
rw₂ rw₃ : M.closure (X ∪ Y) = M.closure (X ∪ Y)
⊢ M.closure (M.closure X ∪ Y) = M.closure (X ∪ Y)

Tactic:
rw [← closure_closure_union_closure_eq_closure_union, closure_closure,
    closure_closure_union_closure_eq_closure_union]

Premises used: Matroid.closure_closure, Matroid.closure_closure_union_closure_eq_closure_union
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X Y X' : Set α
h : M.closure X = M.closure X'
rw : M.closure (M.closure X ∪ Y) = M.closure (X' ∪ Y)
rw₁ : M.closure (M.closure X' ∪ Y) = M.closure (X' ∪ Y)
rw₂ rw₃ : M.closure (X' ∪ Y) = M.closure (X' ∪ Y)
⊢ M.closure (X ∪ Y) = M.closure (X' ∪ Y)

Tactic:
rw [← M.closure_union_closure_left_eq, h, M.closure_union_closure_left_eq]

Premises used: Matroid.closure_union_closure_left_eq
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X Y Y' : Set α
h : M.closure Y = M.closure Y'
rw : M.closure (X ∪ M.closure Y) = M.closure (X ∪ Y')
rw₁ : M.closure (X ∪ M.closure Y') = M.closure (X ∪ Y')
rw₂ rw₃ : M.closure (X ∪ Y') = M.closure (X ∪ Y')
⊢ M.closure (X ∪ Y) = M.closure (X ∪ Y')

Tactic:
rw [← M.closure_union_closure_right_eq, h, M.closure_union_closure_right_eq]

Premises used: Matroid.closure_union_closure_right_eq
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X Y : Set α
e : α
h : M.closure X = M.closure Y
⊢ M.closure (insert e X) = M.closure (insert e Y)

Tactic:
simp [← union_singleton, closure_union_congr_left h]

Premises used: Matroid.closure_union_congr_left, Set.union_singleton
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X : Set α
⊢ M.closure X ∪ M.closure ∅ = M.closure X

Tactic:
union_eq_self_of_subset_right (M.closure_subset_closure (empty_subset _))

Premises used: Set.union_eq_self_of_subset_right, Matroid.closure_subset_closure, Set.empty_subset
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X : Set α
⊢ M.closure ∅ ∪ M.closure X = M.closure X

Tactic:
union_eq_self_of_subset_left (M.closure_subset_closure (empty_subset _))

Premises used: Matroid.closure_subset_closure, Set.union_eq_self_of_subset_left, Set.empty_subset
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X : Set α
e : α
he : e ∈ M.closure X
rw : M.closure (insert e (M.closure X)) = M.closure X
rw₁ : M.closure (M.closure X) = M.closure X
rw₂ rw₃ : M.closure X = M.closure X
⊢ M.closure (insert e X) = M.closure X

Tactic:
rw [← closure_insert_closure_eq_closure_insert, insert_eq_of_mem he, closure_closure]

Premises used: Matroid.closure_insert_closure_eq_closure_insert, Set.insert_eq_of_mem, Matroid.closure_closure
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
e : α
he : e ∈ M.E
⊢ e ∈ M.closure {e}

Tactic:
mem_closure_of_mem' M rfl

Premises used: Matroid.mem_closure_of_mem', rfl
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I : Set α
hI : M.Indep I
set :
  let F : Set α := {x : α | M.IsBasis I (insert x I)};
  M.closure I = F
⊢ M.closure I = {x : α | M.IsBasis I (insert x I)}

Tactic:
set F := {x | M.IsBasis I (insert x I)}
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I : Set α
hI : M.Indep I
F : Set α := {x : α | M.IsBasis I (insert x I)}
⊢ M.IsBasis I F

Tactic:
have hIF : M.IsBasis I F := hI.isBasis_setOf_insert_isBasis
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : 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:
⟨fun J X hJF hJX e heX ↦ show M.IsBasis _ _ from ?_, hIF.subset_ground⟩

Premises used: Matroid.IsBasis.subset_ground, Matroid.IsFlat.mk
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : 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
refine : ∀ (J X : Set α) (hJF : M.IsBasis J F) (hJX : M.IsBasis J X) (e : α) (heX : e ∈ X), M.IsBasis I (insert e I)
⊢ M.IsFlat F

Tactic:
refine ⟨fun J X hJF hJX e heX ↦ show M.IsBasis _ _ from ?_, hIF.subset_ground⟩
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : 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:
(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))

Premises used: Matroid.IsBasis.isBasis_subset, Set.subset_union_right, HasSubset.Subset.trans, Matroid.IsBasis.subset, Matroid.IsBasis.isBasis_union, Matroid.IsBasis.isBasis_of_isBasis_of_subset_of_subset, Or.inl, Set.subset_insert, Set.insert_subset
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : 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))

Premises used: Matroid.IsBasis.isBasis_subset, Set.subset_union_right, HasSubset.Subset.trans, Matroid.IsBasis.subset, Matroid.IsBasis.isBasis_union, Matroid.IsBasis.isBasis_of_isBasis_of_subset_of_subset, Or.inl, Set.subset_insert, Set.insert_subset
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : 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:
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))
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : 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
rw : ∀ (t' : Set α), Membership.mem (γ := Set (Set α)) {F : Set α | M.IsFlat F ∧ I ∩ M.E ⊆ F} t' → F ⊆ t'
rw₁ : Membership.mem (γ := Set (Set α)) {F : Set α | M.IsFlat F ∧ I ∩ M.E ⊆ F} F
⊢ M.closure I = F

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

Premises used: and_iff_right, Set.sInter_subset_of_mem, Matroid.closure_def, subset_antisymm_iff, Set.subset_sInter_iff
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : 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)
rw : ∀ (hIF' : I ⊆ F') ⦃e : α⦄ (he : M.IsBasis I (insert e I)), e ∈ F'
⊢ e ∈ F'

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

Premises used: Set.inter_eq_left, Iff.mpr, Matroid.IsBasis.subset_ground, HasSubset.Subset.trans, Matroid.IsBasis.subset
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : 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)
obtain : ∀ (J : Set α) (hJ : M.IsBasis J F') (hIJ : I ⊆ J), e ∈ F'
⊢ e ∈ F'

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

Premises used: Matroid.Indep.subset_isBasis_of_subset, Matroid.IsFlat.subset_ground
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : 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:
(hF'.1 hJ (he.isBasis_union_of_subset hJ.indep hIJ)) (Or.inr (mem_insert _ _))

Premises used: Set.mem_insert, Matroid.IsBasis.indep, Matroid.IsFlat.subset_of_isBasis_of_isBasis, Or.inr, Matroid.IsBasis.isBasis_union_of_subset
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : 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 _ _))

Premises used: Set.mem_insert, Matroid.IsBasis.indep, Matroid.IsFlat.subset_of_isBasis_of_isBasis, Or.inr, Matroid.IsBasis.isBasis_union_of_subset
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : 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
⊢ Membership.mem (γ := Set (Set α)) {F : Set α | M.IsFlat F ∧ I ∩ M.E ⊆ F} F

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

Premises used: Set.Mem, setOf, HasSubset.Subset.trans, Set.inter_subset_left, Matroid.IsBasis.subset, And.intro
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : 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
⊢ Membership.mem (γ := Set (Set α)) {F : Set α | M.IsFlat F ∧ I ∩ M.E ⊆ F} F

Tactic:
exact ⟨hF, inter_subset_left.trans hIF.subset⟩
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
rw : M.IsBasis I (insert e I) ↔ Membership.mem (γ := Set α) {x : α | M.IsBasis I (insert x I)} e
rw₁ rw₂ : M.IsBasis I (insert e I) ↔ M.IsBasis I (insert e I)
⊢ M.IsBasis I (insert e I) ↔ e ∈ M.closure I

Tactic:
rw [hI.closure_eq_setOf_isBasis_insert, mem_setOf]

Premises used: Matroid.Indep.closure_eq_setOf_isBasis_insert, Set.mem_setOf
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I : Set α
hI : M.Indep I
rw : M.IsBasis I {x : α | M.IsBasis I (insert x I)}
⊢ M.IsBasis I (M.closure I)

Tactic:
rw [hI.closure_eq_setOf_isBasis_insert]

Premises used: Matroid.Indep.closure_eq_setOf_isBasis_insert
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I : Set α
hI : M.Indep I
⊢ M.IsBasis I {x : α | M.IsBasis I (insert x I)}

Tactic:
hI.isBasis_setOf_insert_isBasis

Premises used: Matroid.Indep.isBasis_setOf_insert_isBasis
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I : Set α
hI : M.Indep I
⊢ M.IsBasis I {x : α | M.IsBasis I (insert x I)}

Tactic:
exact hI.isBasis_setOf_insert_isBasis

Premises used: Matroid.Indep.isBasis_setOf_insert_isBasis
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X I : Set α
h : M.IsBasis I X
⊢ M.closure I = M.closure X

Tactic:
subset_antisymm (M.closure_subset_closure h.subset) ?_

Premises used: subset_antisymm, Matroid.IsBasis.subset, Matroid.closure_subset_closure
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X I : Set α
h : M.IsBasis I X
refine : M.closure X ⊆ M.closure I
⊢ M.closure I = M.closure X

Tactic:
refine subset_antisymm (M.closure_subset_closure h.subset) ?_

Premises used: subset_antisymm, Matroid.IsBasis.subset, Matroid.closure_subset_closure
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X I : Set α
h : M.IsBasis I X
rw : M.closure X ⊆ M.closure {x : α | M.IsBasis I (insert x I)}
⊢ M.closure X ⊆ M.closure I

Tactic:
rw [← M.closure_closure I, h.indep.closure_eq_setOf_isBasis_insert]

Premises used: Matroid.closure_closure, Matroid.Indep.closure_eq_setOf_isBasis_insert, Matroid.IsBasis.indep
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X I : Set α
h : M.IsBasis I X
⊢ M.closure X ⊆ M.closure {x : α | M.IsBasis I (insert x I)}

Tactic:
M.closure_subset_closure fun e he ↦ (h.isBasis_subset (subset_insert _ _)
    (insert_subset he h.subset))

Premises used: Matroid.IsBasis.isBasis_subset, Matroid.IsBasis.subset, Matroid.closure_subset_closure, Set.subset_insert, Set.insert_subset
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X I : Set α
h : M.IsBasis I X
⊢ M.closure X ⊆ M.closure {x : α | M.IsBasis I (insert x I)}

Tactic:
exact M.closure_subset_closure fun e he ↦ (h.isBasis_subset (subset_insert _ _)
    (insert_subset he h.subset))

Premises used: Matroid.IsBasis.isBasis_subset, Matroid.IsBasis.subset, Matroid.closure_subset_closure, Set.subset_insert, Set.insert_subset
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X I : Set α
h : M.IsBasis I (M.closure X)
⊢ M.closure I = M.closure X

Tactic:
M.closure_closure X ▸ h.closure_eq_closure

Premises used: Eq.rec, Matroid.closure_closure, Matroid.IsBasis.closure_eq_closure
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X I : Set α
h : M.IsBasis' I X
rw : M.closure I = M.closure (X ∩ M.E)
rw₁ rw₂ : M.closure (X ∩ M.E) = M.closure (X ∩ M.E)
⊢ M.closure I = M.closure X

Tactic:
rw [← closure_inter_ground _ X, h.isBasis_inter_ground.closure_eq_closure]

Premises used: Matroid.IsBasis'.isBasis_inter_ground, Matroid.closure_inter_ground, Matroid.IsBasis.closure_eq_closure
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X I : Set α
h : M.IsBasis I X
rw : M.closure X ⊆ M.closure I
rw₁ rw₂ : M.closure X ⊆ M.closure X
⊢ X ⊆ M.closure I

Tactic:
rw [← closure_subset_closure_iff_subset_closure, h.closure_eq_closure]

Premises used: Matroid.closure_subset_closure_iff_subset_closure, Matroid.IsBasis.closure_eq_closure
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X I : Set α
h : M.IsBasis' I X
rw : M.IsBasis I (M.closure I)
⊢ M.IsBasis I (M.closure X)

Tactic:
rw [← h.closure_eq_closure]

Premises used: Matroid.IsBasis'.closure_eq_closure
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X I : Set α
h : M.IsBasis' I X
⊢ M.IsBasis I (M.closure I)

Tactic:
h.indep.isBasis_closure

Premises used: Matroid.Indep.isBasis_closure, Matroid.IsBasis'.indep
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X I : Set α
h : M.IsBasis' I X
⊢ M.IsBasis I (M.closure I)

Tactic:
exact h.indep.isBasis_closure

Premises used: Matroid.Indep.isBasis_closure, Matroid.IsBasis'.indep
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X I : Set α
h : M.IsBasis I X
⊢ M.IsBasis I (M.closure X)

Tactic:
h.isBasis'.isBasis_closure_right

Premises used: Matroid.IsBasis.isBasis', Matroid.IsBasis'.isBasis_closure_right
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I : Set α
x : α
hI : M.Indep I
rwa : Membership.mem (γ := Set α) {x : α | M.IsBasis I (insert x I)} x ↔ M.Dep (insert x I) ∨ x ∈ I
rwa₁ : M.IsBasis I (insert x I) ↔ M.Dep (insert x I) ∨ x ∈ I
rwa₂ : M.Dep (insert x I) ∨ x ∈ I ↔ M.Dep (insert x I) ∨ x ∈ I
rwa₃ : M.Indep I
rwa₄ : M.Dep (insert x I) ∨ x ∈ I ↔ M.Dep (insert x I) ∨ x ∈ I
rwa₅ rwa₆ rwa₇ : M.Indep I
⊢ x ∈ M.closure I ↔ M.Dep (insert x I) ∨ x ∈ I

Tactic:
rwa [hI.closure_eq_setOf_isBasis_insert, mem_setOf, isBasis_insert_iff]

Premises used: Matroid.Indep.isBasis_insert_iff, Matroid.Indep.closure_eq_setOf_isBasis_insert, Set.mem_setOf
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I : Set α
x : α
hI : M.Indep I
rw : ¬M.Indep (insert x I) ∧ x ∈ M.E ∨ x ∈ I ↔ x ∈ M.E ∧ (¬M.Indep (insert x I) ∨ x ∈ I)
⊢ x ∈ M.closure I ↔ x ∈ M.E ∧ (M.Indep (insert x I) → x ∈ I)

Tactic:
rw [hI.mem_closure_iff, dep_iff, insert_subset_iff, and_iff_left hI.subset_ground,
    imp_iff_not_or]

Premises used: Matroid.Indep.mem_closure_iff, and_iff_left, imp_iff_not_or, Set.insert_subset_iff, Matroid.Indep.subset_ground, Matroid.dep_iff
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I : Set α
x : α
hI : M.Indep I
⊢ I ⊆ M.E

Tactic:
have := hI.subset_ground
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I : Set α
x : α
hI : M.Indep I
this : I ⊆ M.E
⊢ ¬M.Indep (insert x I) ∧ x ∈ M.E ∨ x ∈ I ↔ x ∈ M.E ∧ (¬M.Indep (insert x I) ∨ x ∈ I)

Tactic:
aesop
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
rw : e ∈ I → ¬M.Dep (insert e I)
⊢ M.Dep (insert e I) ↔ e ∈ M.closure I \ I

Tactic:
rw [mem_diff, hI.mem_closure_iff, or_and_right, and_not_self_iff, or_false,
    iff_self_and, imp_not_comm]

Premises used: Matroid.Indep.mem_closure_iff, and_not_self_iff, iff_self_and, imp_not_comm, Set.mem_diff, or_false, or_and_right
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
heI : e ∈ I
rw : ¬M.Dep I
⊢ ¬M.Dep (insert e I)

Tactic:
rw [insert_eq_of_mem heI]

Premises used: Set.insert_eq_of_mem
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
heI : e ∈ I
⊢ ¬M.Dep I

Tactic:
hI.not_dep

Premises used: Matroid.Indep.not_dep
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
heI : e ∈ I
⊢ ¬M.Dep I

Tactic:
exact hI.not_dep

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

Tactic:
rw [hI.insert_dep_iff, mem_diff, and_iff_left heI]

Premises used: and_iff_left, Matroid.Indep.insert_dep_iff, Set.mem_diff
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
he : e ∈ M.E
rw : ¬(¬M.Indep (insert e I) ∨ e ∈ I) ↔ M.Indep (insert e I) ∧ e ∉ I
⊢ e ∉ M.closure I ↔ M.Indep (insert e I) ∧ e ∉ I

Tactic:
rw [hI.mem_closure_iff, dep_iff, insert_subset_iff, and_iff_right he,
    and_iff_left hI.subset_ground]

Premises used: Matroid.Indep.mem_closure_iff, and_iff_left, and_iff_right, Set.insert_subset_iff, Matroid.Indep.subset_ground, Matroid.dep_iff
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
he : e ∈ M.E
mp : ¬(¬M.Indep (insert e I) ∨ e ∈ I) → M.Indep (insert e I) ∧ e ∉ I
mpr : M.Indep (insert e I) ∧ e ∉ I → ¬(¬M.Indep (insert e I) ∨ e ∈ I)
mp₁ mp₂ : ¬¬M.Indep (insert e I) → e ∉ I → M.Indep (insert e I) ∧ e ∉ I
mp₃ : ¬¬M.Indep (insert e I) → e ∉ I → M.Indep (insert e I)
mp₄ : ¬¬M.Indep (insert e I) → e ∉ I → e ∉ I
mpr₁ mpr₂ : M.Indep (insert e I) → e ∉ I → ¬(¬M.Indep (insert e I) ∨ e ∈ I)
mpr₃ : M.Indep (insert e I) → e ∉ I → ¬M.Indep (insert e I) ∨ e ∈ I → False
mp₅ mp₆ mp₇ : M.Indep (insert e I) → e ∉ I → M.Indep (insert e I)
mpr₄ : M.Indep (insert e I) → e ∉ I → ¬M.Indep (insert e I) → False
mpr₅ : M.Indep (insert e I) → e ∉ I → e ∈ I → False
⊢ ¬(¬M.Indep (insert e I) ∨ e ∈ I) ↔ M.Indep (insert e I) ∧ e ∉ I

Tactic:
tauto
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
heI : e ∉ I
he : e ∈ M.E
rw : M.Indep (insert e I) ∧ e ∉ I ↔ M.Indep (insert e I)
rw₁ rw₂ : M.Indep (insert e I) ↔ M.Indep (insert e I)
⊢ e ∉ M.closure I ↔ M.Indep (insert e I)

Tactic:
rw [hI.notMem_closure_iff, and_iff_left heI]

Premises used: and_iff_left, Matroid.Indep.notMem_closure_iff
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
heI : e ∉ I
rw : M.Indep (insert e I) ↔ e ∈ M.E ∧ (e ∈ M.E → M.Indep (insert e I))
⊢ M.Indep (insert e I) ↔ e ∈ M.E \ M.closure I

Tactic:
rw [mem_diff, hI.mem_closure_iff_of_notMem heI, dep_iff, not_and, not_imp_not, insert_subset_iff,
    and_iff_left hI.subset_ground]

Premises used: and_iff_left, Set.insert_subset_iff, Matroid.Indep.subset_ground, Set.mem_diff, Matroid.Indep.mem_closure_iff_of_notMem, not_and, Matroid.dep_iff, not_imp_not
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
heI : e ∉ I
⊢ M.Indep (insert e I) ↔ e ∈ M.E ∧ (e ∈ M.E → M.Indep (insert e I))

Tactic:
⟨fun h ↦ ⟨h.subset_ground (mem_insert e I), fun _ ↦ h⟩, fun h ↦ h.2 h.1⟩

Premises used: Matroid.Indep.subset_ground, And.right, And.left, And.intro, Iff.intro, Set.mem_insert
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
heI : e ∉ I
⊢ M.Indep (insert e I) ↔ e ∈ M.E ∧ (e ∈ M.E → M.Indep (insert e I))

Tactic:
exact ⟨fun h ↦ ⟨h.subset_ground (mem_insert e I), fun _ ↦ h⟩, fun h ↦ h.2 h.1⟩
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
inl : ∀ (h : e ∈ I), M.Indep (insert e I) ↔ e ∈ M.E \ M.closure I ∨ e ∈ I
inr : ∀ (h : e ∉ I), M.Indep (insert e I) ↔ e ∈ M.E \ M.closure I ∨ e ∈ I
⊢ M.Indep (insert e I) ↔ e ∈ M.E \ M.closure I ∨ e ∈ I

Tactic:
obtain (h | h) := em (e ∈ I)

Premises used: Membership.mem, em
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
h : e ∈ I
inl : M.Indep I ↔ e ∈ M.E \ M.closure I ∨ e ∈ I
inl₁ : True ↔ e ∈ M.E \ M.closure I ∨ e ∈ I
inl₂ : e ∈ M.E \ M.closure I ∨ e ∈ I
inl₃ : e ∈ M.E \ M.closure I ∨ True
⊢ M.Indep (insert e I) ↔ e ∈ M.E \ M.closure I ∨ e ∈ I

Tactic:
simp_rw [insert_eq_of_mem h, iff_true_intro hI, true_iff, iff_true_intro h, or_true]

Premises used: true_iff, Set.insert_eq_of_mem, iff_true_intro, or_true