awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X : Set α
e f : α
B : Set α
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

Tactic:
⟨hB.1.indep_insert_diff_of_mem_closure (hB.2.1 hfX) he heB, hB.2.1.trans_eq
    (hB.1.closure_insert_diff_eq_of_mem_closure (hB.2.1 hfX) he).symm, diff_subset.trans
    (insert_subset hfX hB.2.2)⟩

Premises used: Set.diff_subset, LE.le.trans_eq, HasSubset.Subset.trans, And.right, And.left, And.intro, Matroid.Indep.indep_insert_diff_of_mem_closure, Matroid.Indep.closure_insert_diff_eq_of_mem_closure, Eq.symm, Set.insert_subset
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X : Set α
e f : α
B : Set α
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

Tactic:
exact ⟨hB.1.indep_insert_diff_of_mem_closure (hB.2.1 hfX) he heB, hB.2.1.trans_eq
    (hB.1.closure_insert_diff_eq_of_mem_closure (hB.2.1 hfX) he).symm, diff_subset.trans
    (insert_subset hfX hB.2.2)⟩
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
e f : α
B : Set α
hB : M.IsBase B
he : e ∈ M.closure (insert f B \ {e})
heB : e ∈ insert f B
rw :
  ∀ (hB : M.IsBasis B M.E) (he : e ∈ M.closure (insert f B \ {e})) (heB : e ∈ insert f B),
    M.IsBasis (insert f B \ {e}) M.E
⊢ M.IsBase (insert f B \ {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 α
e f : α
B : Set α
hB : M.IsBasis B M.E
he : e ∈ M.closure (insert f B \ {e})
heB : e ∈ insert f B
pos : ∀ (hf : f ∈ M.E), M.IsBasis (insert f B \ {e}) M.E
neg : ∀ (hf : f ∉ M.E), M.IsBasis (insert f B \ {e}) M.E
⊢ M.IsBasis (insert f B \ {e}) M.E

Tactic:
by_cases hf : f ∈ M.E

Premises used: Matroid.E
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
e f : α
B : Set α
hB : M.IsBasis B M.E
he : e ∈ M.closure (insert f B \ {e})
heB : e ∈ insert f B
hf : f ∈ M.E
⊢ M.IsBasis (insert f B \ {e}) M.E

Tactic:
hB.isBasis_insert_diff_of_mem_closure he heB hf

Premises used: Matroid.IsBasis.isBasis_insert_diff_of_mem_closure
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
e f : α
B : Set α
hB : M.IsBasis B M.E
he : e ∈ M.closure (insert f B \ {e})
heB : e ∈ insert f B
hf : f ∈ M.E
⊢ M.IsBasis (insert f B \ {e}) M.E

Tactic:
exact hB.isBasis_insert_diff_of_mem_closure he heB hf

Premises used: Matroid.IsBasis.isBasis_insert_diff_of_mem_closure
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
e f : α
B : Set α
hB : M.IsBasis B M.E
he : e ∈ M.closure (insert f B \ {e})
heB : e ∈ insert f B
hf : f ∉ M.E
neg : ∀ (he : e ∈ M.closure (insert e B \ {e})) (hf : e ∉ M.E), M.IsBasis (insert e B \ {e}) M.E
neg₁ : ∀ (heB : e ∈ B), M.IsBasis (insert f B \ {e}) M.E
⊢ M.IsBasis (insert f B \ {e}) M.E

Tactic:
obtain rfl | heB := heB

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

Tactic:
simpa [show e ∉ B from fun h ↦ hf (hB.1.1.2 h)] using hB

Premises used: And.right, And.left
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
e f : α
B : Set α
hB : M.IsBasis B M.E
he : e ∈ M.closure (insert f B \ {e})
hf : f ∉ M.E
heB : e ∈ B
⊢ e ∈ M.closure (insert f B \ {e} ∩ M.E)

Tactic:
rw [← closure_inter_ground] at he

Premises used: Matroid.closure_inter_ground
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
e f : α
B : Set α
hB : M.IsBasis B M.E
he : e ∈ M.closure (insert f B \ {e})
hf : f ∉ M.E
heB : e ∈ B
he₁ : e ∈ M.closure (insert f B \ {e} ∩ M.E)
⊢ f ∉ M.E

Tactic:
rw [← closure_inter_ground] at he

Premises used: Matroid.closure_inter_ground
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
e f : α
B : Set α
hB : M.IsBasis B M.E
he : e ∈ M.closure (insert f B \ {e})
hf : f ∉ M.E
heB : e ∈ B
he₁ : e ∈ M.closure (insert f B \ {e} ∩ M.E)
hf₁ : f ∉ M.E
⊢ e ∈ B

Tactic:
rw [← closure_inter_ground] at he

Premises used: Matroid.closure_inter_ground
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
e f : α
B : Set α
hB : M.IsBasis B M.E
he : e ∈ M.closure (insert f B \ {e} ∩ M.E)
hf : f ∉ M.E
heB : e ∈ B
a : α
⊢ a ∈ insert f B \ {e} ∩ M.E → a ∈ B \ {e}

Tactic:
aesop
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
e f : α
B : Set α
hB : M.IsBasis B M.E
he : e ∈ M.closure (insert f B \ {e} ∩ M.E)
hf : f ∉ M.E
heB : e ∈ B
⊢ M.IsBasis (insert f B \ {e}) M.E

Tactic:
cases hB.indep.notMem_closure_diff_of_mem heB (M.closure_subset_closure (by intro; aesop) he)

Premises used: Matroid.closure_subset_closure, Matroid.Indep.notMem_closure_diff_of_mem, Matroid.IsBasis.indep
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I : Set α
rw : (I ⊆ M.E ∧ ∀ e ∈ I, e ∉ M.closure (I \ {e})) ↔ ∀ ⦃e : α⦄, e ∈ I → M.closure (I \ {e}) ≠ M.closure I
⊢ M.Indep I ↔ ∀ ⦃e : α⦄, e ∈ I → M.closure (I \ {e}) ≠ M.closure I

Tactic:
rw [indep_iff_forall_notMem_closure_diff']

Premises used: Matroid.indep_iff_forall_notMem_closure_diff'
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I : Set α
⊢ (I ⊆ M.E ∧ ∀ e ∈ I, e ∉ M.closure (I \ {e})) ↔ ∀ ⦃e : α⦄, e ∈ I → M.closure (I \ {e}) ≠ M.closure I

Tactic:
⟨fun ⟨hIE, h⟩ e heI h_eq ↦ h e heI (h_eq.symm.subset (M.mem_closure_of_mem heI)),
    fun h ↦ ⟨fun e heI ↦ by_contra fun heE ↦ h heI ?_,fun e heI hin ↦ h heI ?_⟩⟩

Premises used: False, Eq.subset, Matroid.mem_closure_of_mem, And.intro, Iff.intro, by_contra, Eq.symm, _private.0.Matroid.indep_iff_forall_closure_diff_ne.match_1
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I : Set α
refine_1 :
  ∀ (h : ∀ ⦃e : α⦄, e ∈ I → M.closure (I \ {e}) ≠ M.closure I) (e : α) (heI : e ∈ I) (heE : e ∉ M.E),
    M.closure (I \ {e}) = M.closure I
refine_2 :
  ∀ (h : ∀ ⦃e : α⦄, e ∈ I → M.closure (I \ {e}) ≠ M.closure I) (e : α) (heI : e ∈ I) (hin : e ∈ M.closure (I \ {e})),
    M.closure (I \ {e}) = M.closure I
⊢ (I ⊆ M.E ∧ ∀ e ∈ I, e ∉ M.closure (I \ {e})) ↔ ∀ ⦃e : α⦄, e ∈ I → M.closure (I \ {e}) ≠ M.closure I

Tactic:
refine ⟨fun ⟨hIE, h⟩ e heI h_eq ↦ h e heI (h_eq.symm.subset (M.mem_closure_of_mem heI)),
    fun h ↦ ⟨fun e heI ↦ by_contra fun heE ↦ h heI ?_,fun e heI hin ↦ h heI ?_⟩⟩
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I : Set α
h : ∀ ⦃e : α⦄, e ∈ I → M.closure (I \ {e}) ≠ M.closure I
e : α
heI : e ∈ I
heE : e ∉ M.E
refine_1 : M.closure (I \ {e} ∩ M.E) = M.closure I
refine_1₁ : M.closure (M.E ∩ (I \ {e})) = M.closure I
refine_1₂ : M.closure ((M.E ∩ I) \ (M.E ∩ {e})) = M.closure I
refine_1₃ : M.closure ((M.E ∩ I) \ ∅) = M.closure I
refine_1₄ : M.closure (M.E ∩ I) = M.closure I
refine_1₅ : M.closure (I ∩ M.E) = M.closure I
refine_1₆ refine_1₇ : M.closure I = M.closure I
⊢ M.closure (I \ {e}) = M.closure I

Tactic:
rw [← closure_inter_ground, inter_comm, inter_diff_distrib_left,
      inter_singleton_eq_empty.mpr heE, diff_empty, inter_comm, closure_inter_ground]

Premises used: Iff.mpr, Set.inter_singleton_eq_empty, Set.diff_empty, Set.inter_comm, Set.inter_diff_distrib_left, Matroid.closure_inter_ground
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I : Set α
h : ∀ ⦃e : α⦄, e ∈ I → M.closure (I \ {e}) ≠ M.closure I
e : α
heI : e ∈ I
hin : e ∈ M.closure (I \ {e})
⊢ I = insert e (I \ {e})

Tactic:
simp [heI]
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I : Set α
h : ∀ ⦃e : α⦄, e ∈ I → M.closure (I \ {e}) ≠ M.closure I
e : α
heI : e ∈ I
hin : e ∈ M.closure (I \ {e})
refine_2 : M.closure (I \ {e}) = M.closure (insert e (I \ {e}))
⊢ M.closure (I \ {e}) = M.closure I

Tactic:
nth_rw 2 [show I = insert e (I \ {e}) by simp [heI]]
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I : Set α
h : ∀ ⦃e : α⦄, e ∈ I → M.closure (I \ {e}) ≠ M.closure I
e : α
heI : e ∈ I
hin : e ∈ M.closure (I \ {e})
refine_2 : M.closure (I \ {e}) = M.closure (insert e (M.closure (I \ {e})))
refine_2₁ : M.closure (I \ {e}) = M.closure (M.closure (I \ {e}))
refine_2₂ refine_2₃ : M.closure (I \ {e}) = M.closure (I \ {e})
⊢ M.closure (I \ {e}) = M.closure (insert e (I \ {e}))

Tactic:
rw [← closure_insert_closure_eq_closure_insert, insert_eq_of_mem hin, 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 α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
⊢ M.Indep (I ∪ J) ↔ ∀ e ∈ J \ I, e ∉ M.closure (I ∪ J \ {e})

Tactic:
⟨fun h e heJ hecl ↦ h.notMem_closure_diff_of_mem (.inr heJ.1) ?_, fun h ↦ ?_⟩

Premises used: Matroid.Indep.notMem_closure_diff_of_mem, And.left, Iff.intro, Or.inr
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
refine_1 :
  ∀ (h : M.Indep (I ∪ J)) (e : α) (heJ : e ∈ J \ I) (hecl : e ∈ M.closure (I ∪ J \ {e})), e ∈ M.closure ((I ∪ J) \ {e})
refine_2 : ∀ (h : ∀ e ∈ J \ I, e ∉ M.closure (I ∪ J \ {e})), M.Indep (I ∪ J)
⊢ M.Indep (I ∪ J) ↔ ∀ e ∈ J \ I, e ∉ M.closure (I ∪ J \ {e})

Tactic:
refine ⟨fun h e heJ hecl ↦ h.notMem_closure_diff_of_mem (.inr heJ.1) ?_, fun h ↦ ?_⟩
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
h : M.Indep (I ∪ J)
e : α
heJ : e ∈ J \ I
hecl : e ∈ M.closure (I ∪ J \ {e})
refine_1 : e ∈ M.closure (I \ {e} ∪ J \ {e})
refine_1₁ refine_1₂ refine_1₃ refine_1₄ : e ∈ M.closure (I ∪ J \ {e})
⊢ e ∈ M.closure ((I ∪ J) \ {e})

Tactic:
rwa [union_diff_distrib, diff_singleton_eq_self heJ.2]

Premises used: Set.diff_singleton_eq_self, Set.union_diff_distrib, And.right
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
h : ∀ e ∈ J \ I, e ∉ M.closure (I ∪ J \ {e})
refine_2 : ∀ (K : Set α) (hKIJ : M.IsBasis K (I ∪ J)) (hK : I ⊆ K), M.Indep (I ∪ J)
⊢ M.Indep (I ∪ J)

Tactic:
obtain ⟨K, hKIJ, hK⟩ := hI.subset_isBasis_of_subset (show I ⊆ I ∪ J from subset_union_left)

Premises used: Set.subset_union_left, Matroid.Indep.subset_isBasis_of_subset
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
h : ∀ e ∈ J \ I, e ∉ M.closure (I ∪ J \ {e})
K : Set α
hKIJ : M.IsBasis K (I ∪ J)
hK : I ⊆ K
refine_2 : ∀ (hKIJ : M.IsBasis (I ∪ J) (I ∪ J)) (hK : I ⊆ I ∪ J), M.Indep (I ∪ J)
refine_2₁ : ∀ (hssu : K ⊂ I ∪ J), M.Indep (I ∪ J)
⊢ M.Indep (I ∪ J)

Tactic:
obtain rfl | hssu := hKIJ.subset.eq_or_ssubset

Premises used: HasSubset.Subset.eq_or_ssubset, Matroid.IsBasis.subset, rfl
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
h : ∀ e ∈ J \ I, e ∉ M.closure (I ∪ J \ {e})
hKIJ : M.IsBasis (I ∪ J) (I ∪ J)
hK : I ⊆ I ∪ J
⊢ M.Indep (I ∪ J)

Tactic:
hKIJ.indep

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

Tactic:
exact hKIJ.indep

Premises used: Matroid.IsBasis.indep
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
h : ∀ e ∈ J \ I, e ∉ M.closure (I ∪ J \ {e})
K : Set α
hKIJ : M.IsBasis K (I ∪ J)
hK : I ⊆ K
hssu : K ⊂ I ∪ J
refine_2 : False
⊢ M.Indep (I ∪ J)

Tactic:
exfalso
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
h : ∀ e ∈ J \ I, e ∉ M.closure (I ∪ J \ {e})
K : Set α
hKIJ : M.IsBasis K (I ∪ J)
hK : I ⊆ K
hssu : K ⊂ I ∪ J
refine_2 : ∀ (e : α) (heI : e ∈ I ∪ J) (heK : e ∉ K), False
⊢ False

Tactic:
obtain ⟨e, heI, heK⟩ := exists_of_ssubset hssu

Premises used: Set.exists_of_ssubset
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
h : ∀ e ∈ J \ I, e ∉ M.closure (I ∪ J \ {e})
K : Set α
hKIJ : M.IsBasis K (I ∪ J)
hK : I ⊆ K
hssu : K ⊂ I ∪ J
e : α
heI : e ∈ I ∪ J
heK : e ∉ K
rw : e ∈ (I ∪ J) \ I
⊢ e ∈ J \ I

Tactic:
rw [← union_diff_right, union_comm]

Premises used: Set.union_comm, Set.union_diff_right
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
h : ∀ e ∈ J \ I, e ∉ M.closure (I ∪ J \ {e})
K : Set α
hKIJ : M.IsBasis K (I ∪ J)
hK : I ⊆ K
hssu : K ⊂ I ∪ J
e : α
heI : e ∈ I ∪ J
heK : e ∉ K
⊢ e ∈ (I ∪ J) \ I

Tactic:
⟨heI, notMem_subset hK heK⟩

Premises used: Set.Mem, Set.diff, setOf, And.intro, Set.notMem_subset
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
h : ∀ e ∈ J \ I, e ∉ M.closure (I ∪ J \ {e})
K : Set α
hKIJ : M.IsBasis K (I ∪ J)
hK : I ⊆ K
hssu : K ⊂ I ∪ J
e : α
heI : e ∈ I ∪ J
heK : e ∉ K
⊢ e ∈ (I ∪ J) \ I

Tactic:
exact ⟨heI, notMem_subset hK heK⟩
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
h : ∀ e ∈ J \ I, e ∉ M.closure (I ∪ J \ {e})
K : Set α
hKIJ : M.IsBasis K (I ∪ J)
hK : I ⊆ K
hssu : K ⊂ I ∪ J
e : α
heI : e ∈ I ∪ J
heK : e ∉ K
⊢ e ∈ J \ I

Tactic:
have heJI : e ∈ J \ I := by
    rw [← union_diff_right, union_comm]
    exact ⟨heI, notMem_subset hK heK⟩
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
h : ∀ e ∈ J \ I, e ∉ M.closure (I ∪ J \ {e})
K : Set α
hKIJ : M.IsBasis K (I ∪ J)
hK : I ⊆ K
hssu : K ⊂ I ∪ J
e : α
heI : e ∈ I ∪ J
heK : e ∉ K
heJI : e ∈ J \ I
⊢ False

Tactic:
h _ heJI ?_
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
h : ∀ e ∈ J \ I, e ∉ M.closure (I ∪ J \ {e})
K : Set α
hKIJ : M.IsBasis K (I ∪ J)
hK : I ⊆ K
hssu : K ⊂ I ∪ J
e : α
heI : e ∈ I ∪ J
heK : e ∉ K
heJI : e ∈ J \ I
refine_2 : e ∈ M.closure (I ∪ J \ {e})
⊢ False

Tactic:
refine h _ heJI ?_
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
h : ∀ e ∈ J \ I, e ∉ M.closure (I ∪ J \ {e})
K : Set α
hKIJ : M.IsBasis K (I ∪ J)
hK : I ⊆ K
hssu : K ⊂ I ∪ J
e : α
heI : e ∈ I ∪ J
heK : e ∉ K
heJI : e ∈ J \ I
refine_2 : e ∈ M.closure ((I ∪ J) \ {e})
⊢ e ∈ M.closure (I ∪ J \ {e})

Tactic:
rw [← diff_singleton_eq_self heJI.2, ← union_diff_distrib]

Premises used: Set.diff_singleton_eq_self, Set.union_diff_distrib, And.right
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
h : ∀ e ∈ J \ I, e ∉ M.closure (I ∪ J \ {e})
K : Set α
hKIJ : M.IsBasis K (I ∪ J)
hK : I ⊆ K
hssu : K ⊂ I ∪ J
e : α
heI : e ∈ I ∪ J
heK : e ∉ K
heJI : e ∈ J \ I
⊢ e ∈ M.closure ((I ∪ J) \ {e})

Tactic:
M.closure_subset_closure (subset_diff_singleton hKIJ.subset heK) <| hKIJ.subset_closure heI

Premises used: Matroid.IsBasis.subset, Matroid.closure_subset_closure, Set.subset_diff_singleton, Matroid.IsBasis.subset_closure
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
h : ∀ e ∈ J \ I, e ∉ M.closure (I ∪ J \ {e})
K : Set α
hKIJ : M.IsBasis K (I ∪ J)
hK : I ⊆ K
hssu : K ⊂ I ∪ J
e : α
heI : e ∈ I ∪ J
heK : e ∉ K
heJI : e ∈ J \ I
⊢ e ∈ M.closure ((I ∪ J) \ {e})

Tactic:
exact M.closure_subset_closure (subset_diff_singleton hKIJ.subset heK) <| hKIJ.subset_closure heI

Premises used: Matroid.IsBasis.subset, Matroid.closure_subset_closure, Set.subset_diff_singleton, Matroid.IsBasis.subset_closure
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
simp_rw : M.Indep (J ∪ I) ↔ ∀ e ∈ I \ J, e ∉ M.closure (I \ {e} ∪ J)
simp_rw₁ : (∀ e ∈ I \ J, e ∉ M.closure (J ∪ I \ {e})) ↔ ∀ e ∈ I \ J, e ∉ M.closure (I \ {e} ∪ J)
⊢ M.Indep (I ∪ J) ↔ ∀ e ∈ I \ J, e ∉ M.closure (I \ {e} ∪ J)

Tactic:
simp_rw [union_comm I J, hJ.union_indep_iff_forall_notMem_closure_right hI, union_comm]

Premises used: Set.union_comm, Matroid.Indep.union_indep_iff_forall_notMem_closure_right
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJI : J ⊂ I
obtain : ∀ (e : α) (heI : e ∈ I) (heJ : e ∉ J), M.closure J ⊂ M.closure I
⊢ M.closure J ⊂ M.closure I

Tactic:
obtain ⟨e, heI, heJ⟩ := exists_of_ssubset hJI

Premises used: Set.exists_of_ssubset
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJI : J ⊂ I
e : α
heI : e ∈ I
heJ : e ∉ J
⊢ M.closure J ⊂ M.closure I

Tactic:
(M.closure_subset_closure hJI.subset).ssubset_of_not_subset fun hss ↦ heJ <|
    (hI.closure_inter_eq_self_of_subset hJI.subset).subset ⟨hss (M.mem_closure_of_mem heI), heI⟩

Premises used: HasSubset.Subset.ssubset_of_not_subset, HasSSubset.SSubset.subset, Matroid.closure_subset_closure, Eq.subset, Matroid.Indep.closure_inter_eq_self_of_subset, Matroid.mem_closure_of_mem, And.intro
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJI : J ⊂ I
e : α
heI : e ∈ I
heJ : e ∉ J
⊢ M.closure J ⊂ M.closure I

Tactic:
exact (M.closure_subset_closure hJI.subset).ssubset_of_not_subset fun hss ↦ heJ <|
    (hI.closure_inter_eq_self_of_subset hJI.subset).subset ⟨hss (M.mem_closure_of_mem heI), heI⟩

Premises used: HasSubset.Subset.ssubset_of_not_subset, HasSSubset.SSubset.subset, Matroid.closure_subset_closure, Eq.subset, Matroid.Indep.closure_inter_eq_self_of_subset, Matroid.mem_closure_of_mem, And.intro
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I : Set α
hI : I ⊆ M.E
⊢ M.Indep I ↔ ∀ ⦃J : Set α⦄, J ⊂ I → M.closure J ⊂ M.closure I

Tactic:
⟨fun h _ ↦ h.closure_ssubset_closure,
    fun h ↦ (indep_iff_forall_notMem_closure_diff hI).2 fun e heI hecl ↦ ?_⟩

Premises used: Iff.mpr, Iff.intro, Matroid.Indep.closure_ssubset_closure, Matroid.indep_iff_forall_notMem_closure_diff
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I : Set α
hI : I ⊆ M.E
refine :
  ∀ (h : ∀ ⦃J : Set α⦄, J ⊂ I → M.closure J ⊂ M.closure I) (e : α) (heI : e ∈ I) (hecl : e ∈ M.closure (I \ {e})), False
⊢ M.Indep I ↔ ∀ ⦃J : Set α⦄, J ⊂ I → M.closure J ⊂ M.closure I

Tactic:
refine ⟨fun h _ ↦ h.closure_ssubset_closure,
    fun h ↦ (indep_iff_forall_notMem_closure_diff hI).2 fun e heI hecl ↦ ?_⟩
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I : Set α
hI : I ⊆ M.E
h : ∀ ⦃J : Set α⦄, J ⊂ I → M.closure J ⊂ M.closure I
e : α
heI : e ∈ I
hecl : e ∈ M.closure (I \ {e})
⊢ False

Tactic:
(h (diff_singleton_ssubset.2 heI)).ne ?_

Premises used: Iff.mpr, Set.diff_singleton_ssubset, HasSSubset.SSubset.ne
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I : Set α
hI : I ⊆ M.E
h : ∀ ⦃J : Set α⦄, J ⊂ I → M.closure J ⊂ M.closure I
e : α
heI : e ∈ I
hecl : e ∈ M.closure (I \ {e})
refine : M.closure (I \ {e}) = M.closure I
⊢ False

Tactic:
refine (h (diff_singleton_ssubset.2 heI)).ne ?_

Premises used: Iff.mpr, Set.diff_singleton_ssubset, HasSSubset.SSubset.ne
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I : Set α
hI : I ⊆ M.E
h : ∀ ⦃J : Set α⦄, J ⊂ I → M.closure J ⊂ M.closure I
e : α
heI : e ∈ I
hecl : e ∈ M.closure (I \ {e})
⊢ I = insert e (I \ {e})

Tactic:
simp [heI]
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I : Set α
hI : I ⊆ M.E
h : ∀ ⦃J : Set α⦄, J ⊂ I → M.closure J ⊂ M.closure I
e : α
heI : e ∈ I
hecl : e ∈ M.closure (I \ {e})
rw : M.closure (insert e (I \ {e}) \ {e}) = M.closure (M.closure (I \ {e}))
⊢ M.closure (I \ {e}) = M.closure I

Tactic:
rw [show I = insert e (I \ {e}) by simp [heI], ← closure_insert_closure_eq_closure_insert,
    insert_eq_of_mem hecl]

Premises used: Matroid.closure_insert_closure_eq_closure_insert, Set.insert_eq_of_mem
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
I : Set α
hI : I ⊆ M.E
h : ∀ ⦃J : Set α⦄, J ⊂ I → M.closure J ⊂ M.closure I
e : α
heI : e ∈ I
hecl : e ∈ M.closure (I \ {e})
⊢ M.closure (insert e (I \ {e}) \ {e}) = M.closure (M.closure (I \ {e}))

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X I : Set α
hI : M.Indep I
hX : (I ∩ X).Nonempty
⊢ M.closure (I \ X) ⊂ M.closure I

Tactic:
hI.closure_ssubset_closure <| diff_subset.ssubset_of_ne fun h ↦ ?_

Premises used: Set.diff_subset, Matroid.Indep.closure_ssubset_closure, HasSubset.Subset.ssubset_of_ne
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X I : Set α
hI : M.Indep I
hX : (I ∩ X).Nonempty
refine : ∀ (h : I \ X = I), False
⊢ M.closure (I \ X) ⊂ M.closure I

Tactic:
refine hI.closure_ssubset_closure <| diff_subset.ssubset_of_ne fun h ↦ ?_

Premises used: Set.diff_subset, Matroid.Indep.closure_ssubset_closure, HasSubset.Subset.ssubset_of_ne
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X I : Set α
hI : M.Indep I
hX : (I ∩ X).Nonempty
h : I \ X = I
⊢ I ∩ X = ∅

Tactic:
rw [sdiff_eq_left, disjoint_iff_inter_eq_empty] at h

Premises used: Set.disjoint_iff_inter_eq_empty, sdiff_eq_left
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X I : Set α
hI : M.Indep I
hX : (I ∩ X).Nonempty
h : I ∩ X = ∅
⊢ False

Tactic:
simp [h] at hX
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
he : e ∈ I
⊢ I \ {e} ⊂ I

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X : Set α
e f : α
he : e ∉ M.closure X
hef : e ∈ M.closure (insert f X)
rw : ∀ (he : e ∉ M.closure (X ∩ M.E)) (hef : e ∈ M.closure (insert f X ∩ M.E)), f ∈ M.closure (insert e X ∩ M.E)
⊢ f ∈ M.closure (insert e X)

Tactic:
rw [← closure_inter_ground] at *

Premises used: Matroid.closure_inter_ground
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X : Set α
e f : α
he : e ∉ M.closure (X ∩ M.E)
hef : e ∈ M.closure (insert f X ∩ M.E)
by_contra! : ∀ (hfE : f ∉ M.E), False
⊢ f ∈ M.E

Tactic:
by_contra! hfE
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X : Set α
e f : α
he : e ∉ M.closure (X ∩ M.E)
hef : e ∈ M.closure (insert f X ∩ M.E)
hfE : f ∉ M.E
⊢ e ∈ M.closure (X ∩ M.E)

Tactic:
rw [insert_inter_of_notMem hfE] at hef

Premises used: Set.insert_inter_of_notMem
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X : Set α
e f : α
he : e ∉ M.closure (X ∩ M.E)
hef : e ∈ M.closure (insert f X ∩ M.E)
hfE : f ∉ M.E
hef₁ : e ∈ M.closure (X ∩ M.E)
⊢ f ∉ M.E

Tactic:
rw [insert_inter_of_notMem hfE] at hef

Premises used: Set.insert_inter_of_notMem
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X : Set α
e f : α
he : e ∉ M.closure (X ∩ M.E)
hef : e ∈ M.closure (X ∩ M.E)
hfE : f ∉ M.E
⊢ False

Tactic:
he hef
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X : Set α
e f : α
he : e ∉ M.closure (X ∩ M.E)
hef : e ∈ M.closure (X ∩ M.E)
hfE : f ∉ M.E
⊢ False

Tactic:
exact he hef
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
X : Set α
e f : α
he : e ∉ M.closure (X ∩ M.E)
hef : e ∈ M.closure (insert f X ∩ M.E)
⊢ f ∈ M.E

Tactic:
have hfE : f ∈ M.E := by
    by_contra! hfE; rw [insert_inter_of_notMem hfE] at hef; exact he hef