awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
I : Set α
e : α
M : Matroid α
heI : e ∉ I
⊢ M.fundCircuit e I \ {e} ⊆ I

Tactic:
simp [fundCircuit_subset_insert]

Premises used: Matroid.fundCircuit_subset_insert
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
I : Set α
e : α
M : Matroid α
heI : e ∉ I
⊢ e ∉ M.fundCircuit e I ∩ I

Tactic:
simp [heI]
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
X : Set α
e : α
heX : e ∈ X
h : ∀ a ∈ X, (∀ t ⊆ X, M.closure {e} ⊆ M.closure t → a ∈ t) → a = e
⊢ M.fundCircuit e X = {e}

Tactic:
simpa [subset_antisymm_iff, fundCircuit]

Premises used: subset_antisymm_iff, Matroid.fundCircuit
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
X : Set α
e : α
heX : e ∈ X
suffices : ∀ a ∈ X, (∀ t ⊆ X, M.closure {e} ⊆ M.closure t → a ∈ t) → a = e
⊢ M.fundCircuit e X = {e}

Tactic:
suffices h : ∀ a ∈ X, (∀ t ⊆ X, M.closure {e} ⊆ M.closure t → a ∈ t) → a = e by
    simpa [subset_antisymm_iff, fundCircuit]
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
X : Set α
e : α
heX : e ∈ X
⊢ ∀ a ∈ X, (∀ t ⊆ X, M.closure {e} ⊆ M.closure t → a ∈ t) → a = e

Tactic:
fun b hbX h ↦ h _ (singleton_subset_iff.2 heX) Subset.rfl

Premises used: Iff.mpr, Set.singleton_subset_iff, Set.Mem, setOf, Set.Subset.rfl, Set.singleton, Singleton.singleton
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
X : Set α
e : α
heX : e ∈ X
⊢ ∀ a ∈ X, (∀ t ⊆ X, M.closure {e} ⊆ M.closure t → a ∈ t) → a = e

Tactic:
exact fun b hbX h ↦ h _ (singleton_subset_iff.2 heX) Subset.rfl
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
X : Set α
e : α
heX : e ∉ M.E
h : ∀ a ∈ X, (∀ t ⊆ X, M.closure {e} ⊆ M.closure t → a ∈ t) → a = e
⊢ M.fundCircuit e X = {e}

Tactic:
simpa [subset_antisymm_iff, fundCircuit]

Premises used: subset_antisymm_iff, Matroid.fundCircuit
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
X : Set α
e : α
heX : e ∉ M.E
suffices : ∀ a ∈ X, (∀ t ⊆ X, M.closure {e} ⊆ M.closure t → a ∈ t) → a = e
⊢ M.fundCircuit e X = {e}

Tactic:
suffices h : ∀ a ∈ X, (∀ t ⊆ X, M.closure {e} ⊆ M.closure t → a ∈ t) → a = e by
    simpa [subset_antisymm_iff, fundCircuit]
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
X : Set α
e : α
heX : e ∉ M.E
simp_rw : ∀ a ∈ X, (∀ t ⊆ X, M.closure ∅ ⊆ M.closure t → a ∈ t) → a = e
⊢ ∀ a ∈ X, (∀ t ⊆ X, M.closure {e} ⊆ M.closure t → a ∈ t) → a = e

Tactic:
simp_rw [← M.closure_inter_ground {e}, singleton_inter_eq_empty.2 heX]

Premises used: Iff.mpr, Set.singleton_inter_eq_empty, Matroid.closure_inter_ground, Singleton.singleton
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
X : Set α
e : α
heX : e ∉ M.E
a : α
haX : a ∈ X
h : ∀ t ⊆ X, M.closure ∅ ⊆ M.closure t → a ∈ t
⊢ a = e

Tactic:
simpa using h ∅ (empty_subset X) rfl.subset

Premises used: Eq.subset, Set.empty_subset, EmptyCollection.emptyCollection, rfl
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
X : Set α
e : α
heX : e ∉ M.E
⊢ ∀ a ∈ X, (∀ t ⊆ X, M.closure ∅ ⊆ M.closure t → a ∈ t) → a = e

Tactic:
exact fun a haX h ↦ by simpa using h ∅ (empty_subset X) rfl.subset
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
⊢ Membership.mem (γ := Set (Set α)) {J : Set α | J ⊆ I ∧ e ∈ M.closure J} I

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
⊢ ⋂₀ {J : Set α | J ⊆ I ∧ e ∈ M.closure J} ⊆ I

Tactic:
have aux : ⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J} ⊆ I := sInter_subset_of_mem (by simpa)
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
aux : ⋂₀ {J : Set α | J ⊆ I ∧ e ∈ M.closure J} ⊆ I
rw : M.IsCircuit (insert e (⋂₀ {J : Set α | J ⊆ I ∧ e ∈ M.closure J}))
⊢ M.IsCircuit (M.fundCircuit e I)

Tactic:
rw [fundCircuit_eq_sInter hecl]

Premises used: Matroid.fundCircuit_eq_sInter
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
aux : ⋂₀ {J : Set α | J ⊆ I ∧ e ∈ M.closure J} ⊆ I
⊢ M.IsCircuit (insert e (⋂₀ {J : Set α | J ⊆ I ∧ e ∈ M.closure J}))

Tactic:
(hI.subset aux).insert_isCircuit_of_forall ?_ ?_ ?_

Premises used: Matroid.Indep.insert_isCircuit_of_forall, Matroid.Indep.subset
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
aux : ⋂₀ {J : Set α | J ⊆ I ∧ e ∈ M.closure J} ⊆ I
refine_1 : e ∉ ⋂₀ {J : Set α | J ⊆ I ∧ e ∈ M.closure J}
refine_2 : e ∈ M.closure (⋂₀ {J : Set α | J ⊆ I ∧ e ∈ M.closure J})
refine_3 :
  ∀ (f : α),
    Membership.mem (γ := Set α) (⋂₀ {J : Set α | J ⊆ I ∧ e ∈ M.closure J}) f →
      e ∉ M.closure (⋂₀ {J : Set α | J ⊆ I ∧ e ∈ M.closure J} \ {f})
⊢ M.IsCircuit (insert e (⋂₀ {J : Set α | J ⊆ I ∧ e ∈ M.closure J}))

Tactic:
refine (hI.subset aux).insert_isCircuit_of_forall ?_ ?_ ?_

Premises used: Matroid.Indep.insert_isCircuit_of_forall, Matroid.Indep.subset
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
aux : ⋂₀ {J : Set α | J ⊆ I ∧ e ∈ M.closure J} ⊆ I
⊢ I ⊆ I ∧ e ∈ M.closure I ∧ e ∉ I

Tactic:
simp [hecl, heI]
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
aux : ⋂₀ {J : Set α | J ⊆ I ∧ e ∈ M.closure J} ⊆ I
⊢ e ∉ ⋂₀ {J : Set α | J ⊆ I ∧ e ∈ M.closure J}

Tactic:
simp [show ∃ x ⊆ I, e ∈ M.closure x ∧ e ∉ x from ⟨I, by simp [hecl, heI]⟩]

Premises used: Exists.intro
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
aux : ⋂₀ {J : Set α | J ⊆ I ∧ e ∈ M.closure J} ⊆ I
⊢ Membership.mem (γ := Set (Set α)) {J : Set α | J ⊆ I ∧ e ∈ M.closure J} I

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
aux : ⋂₀ {J : Set α | J ⊆ I ∧ e ∈ M.closure J} ⊆ I
⊢ ∀ (J : Set α), Membership.mem (γ := Set (Set α)) {J : Set α | J ⊆ I ∧ e ∈ M.closure J} J → J ⊆ I

Tactic:
simp +contextual
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
aux : ⋂₀ {J : Set α | J ⊆ I ∧ e ∈ M.closure J} ⊆ I
refine_2 :
  Membership.mem (γ := Set α)
    (⋂ (J : Set α), ⋂ (_ : Membership.mem (γ := Set (Set α)) {J : Set α | J ⊆ I ∧ e ∈ M.closure J} J), M.closure J) e
⊢ e ∈ M.closure (⋂₀ {J : Set α | J ⊆ I ∧ e ∈ M.closure J})

Tactic:
rw [hI.closure_sInter_eq_biInter_closure_of_forall_subset ⟨I, by simpa⟩ (by simp +contextual)]

Premises used: Exists.intro, Matroid.Indep.closure_sInter_eq_biInter_closure_of_forall_subset
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
aux : ⋂₀ {J : Set α | J ⊆ I ∧ e ∈ M.closure J} ⊆ I
⊢ Membership.mem (γ := Set α)
    (⋂ (J : Set α), ⋂ (_ : Membership.mem (γ := Set (Set α)) {J : Set α | J ⊆ I ∧ e ∈ M.closure J} J), M.closure J) e

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
aux : ⋂₀ {J : Set α | J ⊆ I ∧ e ∈ M.closure J} ⊆ I
refine_3 :
  ∀ (f : α), (∀ t ⊆ I, e ∈ M.closure t → f ∈ t) → e ∉ M.closure (⋂₀ {J : Set α | J ⊆ I ∧ e ∈ M.closure J} \ {f})
⊢ ∀ (f : α),
    Membership.mem (γ := Set α) (⋂₀ {J : Set α | J ⊆ I ∧ e ∈ M.closure J}) f →
      e ∉ M.closure (⋂₀ {J : Set α | J ⊆ I ∧ e ∈ M.closure J} \ {f})

Tactic:
simp only [mem_sInter, mem_setOf_eq, and_imp]

Premises used: and_imp, Set.mem_setOf_eq, Set.mem_sInter
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
aux : ⋂₀ {J : Set α | J ⊆ I ∧ e ∈ M.closure J} ⊆ I
⊢ ∀ (f : α), (∀ t ⊆ I, e ∈ M.closure t → f ∈ t) → e ∉ M.closure (⋂₀ {J : Set α | J ⊆ I ∧ e ∈ M.closure J} \ {f})

Tactic:
fun f hf hecl ↦ (hf _ (diff_subset.trans aux) hecl).2 rfl

Premises used: Set.diff_subset, setOf, Membership.mem, HasSubset.Subset.trans, HasSubset.Subset, SDiff.sdiff, And, And.right, Matroid.closure, Singleton.singleton, Set.sInter, Not, rfl
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
aux : ⋂₀ {J : Set α | J ⊆ I ∧ e ∈ M.closure J} ⊆ I
⊢ ∀ (f : α), (∀ t ⊆ I, e ∈ M.closure t → f ∈ t) → e ∉ M.closure (⋂₀ {J : Set α | J ⊆ I ∧ e ∈ M.closure J} \ {f})

Tactic:
exact fun f hf hecl ↦ (hf _ (diff_subset.trans aux) hecl).2 rfl
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
I : Set α
e x : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
inl : ∀ (hecl : x ∈ M.closure I) (heI : x ∉ I), x ∈ M.fundCircuit x I ↔ M.Indep (insert x I \ {x})
inr : ∀ (hne : x ≠ e), x ∈ M.fundCircuit e I ↔ M.Indep (insert e I \ {x})
⊢ x ∈ M.fundCircuit e I ↔ M.Indep (insert e I \ {x})

Tactic:
obtain rfl | hne := eq_or_ne x e

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
I : Set α
x : α
hI : M.Indep I
hecl : x ∈ M.closure I
heI : x ∉ I
⊢ x ∈ M.fundCircuit x I ↔ M.Indep (insert x I \ {x})

Tactic:
simp [hI.diff, mem_fundCircuit]

Premises used: Matroid.Indep.diff, Matroid.mem_fundCircuit
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
I : Set α
e x : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
hne : x ≠ e
this : (∀ t ⊆ I, e ∈ M.closure t → x ∈ t) ↔ e ∉ M.closure (I \ {x})
⊢ x ∈ M.fundCircuit e I ↔ M.Indep (insert e I \ {x})

Tactic:
simpa [fundCircuit_eq_sInter hecl, hne, ← insert_diff_singleton_comm hne.symm,
      (hI.diff _).insert_indep_iff, mem_ground_of_mem_closure hecl, heI]

Premises used: Matroid.fundCircuit_eq_sInter, Matroid.Indep.diff, Matroid.Indep.insert_indep_iff, Ne.symm, Set.insert_diff_singleton_comm, Matroid.mem_ground_of_mem_closure
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
I : Set α
e x : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
hne : x ≠ e
inr : (∀ t ⊆ I, e ∈ M.closure t → x ∈ t) ↔ e ∉ M.closure (I \ {x})
⊢ x ∈ M.fundCircuit e I ↔ M.Indep (insert e I \ {x})

Tactic:
suffices (∀ t ⊆ I, e ∈ M.closure t → x ∈ t) ↔ e ∉ M.closure (I \ {x}) by
    simpa [fundCircuit_eq_sInter hecl, hne, ← insert_diff_singleton_comm hne.symm,
      (hI.diff _).insert_indep_iff, mem_ground_of_mem_closure hecl, heI]
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
I : Set α
e x : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
hne : x ≠ e
⊢ (∀ t ⊆ I, e ∈ M.closure t → x ∈ t) ↔ e ∉ M.closure (I \ {x})

Tactic:
⟨fun h hecl ↦ (h _ diff_subset hecl).2 rfl, fun h J hJ heJ ↦ by_contra fun hxJ ↦ h ?_⟩

Premises used: Set.diff_subset, SDiff.sdiff, And.right, Iff.intro, by_contra, Singleton.singleton, rfl
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
I : Set α
e x : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
hne : x ≠ e
inr :
  ∀ (h : e ∉ M.closure (I \ {x})) (J : Set α) (hJ : J ⊆ I) (heJ : e ∈ M.closure J) (hxJ : x ∉ J),
    e ∈ M.closure (I \ {x})
⊢ (∀ t ⊆ I, e ∈ M.closure t → x ∈ t) ↔ e ∉ M.closure (I \ {x})

Tactic:
refine ⟨fun h hecl ↦ (h _ diff_subset hecl).2 rfl, fun h J hJ heJ ↦ by_contra fun hxJ ↦ h ?_⟩
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
I : Set α
e x : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
hne : x ≠ e
h : e ∉ M.closure (I \ {x})
J : Set α
hJ : J ⊆ I
heJ : e ∈ M.closure J
hxJ : x ∉ J
⊢ e ∈ M.closure (I \ {x})

Tactic:
M.closure_subset_closure (subset_diff_singleton hJ hxJ) heJ

Premises used: Matroid.closure_subset_closure, Set.subset_diff_singleton
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
I : Set α
e x : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
hne : x ≠ e
h : e ∉ M.closure (I \ {x})
J : Set α
hJ : J ⊆ I
heJ : e ∈ M.closure J
hxJ : x ∉ J
⊢ e ∈ M.closure (I \ {x})

Tactic:
exact M.closure_subset_closure (subset_diff_singleton hJ hxJ) heJ

Premises used: Matroid.closure_subset_closure, Set.subset_diff_singleton
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
x : α
B : Set α
hB : M.IsBase B
hxE : x ∈ M.E
hxB : x ∉ B
rwa rwa₁ rwa₂ rwa₃ : x ∈ M.E
⊢ x ∈ M.closure B

Tactic:
rwa [hB.closure_eq]

Premises used: Matroid.IsBase.closure_eq
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C I : Set α
e : α
hC : M.IsCircuit C
hI : M.Indep I
hCs : C ⊆ insert e I
inl : ∀ (hCI : C ⊆ I), C = M.fundCircuit e I
inr : ∀ (heC : e ∈ C) (hCeI : C \ {e} ⊆ I), C = M.fundCircuit e I
⊢ C = M.fundCircuit e I

Tactic:
obtain hCI | ⟨heC, hCeI⟩ := subset_insert_iff.1 hCs

Premises used: Set.subset_insert_iff, Iff.mp
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C I : Set α
e : α
hC : M.IsCircuit C
hI : M.Indep I
hCs : C ⊆ insert e I
hCI : C ⊆ I
⊢ C = M.fundCircuit e I

Tactic:
(hC.not_indep (hI.subset hCI)).elim

Premises used: False.elim, Matroid.Indep.subset, Matroid.IsCircuit.not_indep
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C I : Set α
e : α
hC : M.IsCircuit C
hI : M.Indep I
hCs : C ⊆ insert e I
hCI : C ⊆ I
⊢ C = M.fundCircuit e I

Tactic:
exact (hC.not_indep (hI.subset hCI)).elim

Premises used: False.elim, Matroid.Indep.subset, Matroid.IsCircuit.not_indep
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C I : Set α
e : α
hC : M.IsCircuit C
hI : M.Indep I
hCs : C ⊆ insert e I
heC : e ∈ C
hCeI : C \ {e} ⊆ I
hss : M.fundCircuit e I ⊆ C
⊢ C = M.fundCircuit e I

Tactic:
hC.eq_of_superset_isCircuit (hI.fundCircuit_isCircuit ?_ fun heI ↦ ?_) hss

Premises used: Matroid.IsCircuit.eq_of_superset_isCircuit, Matroid.Indep.fundCircuit_isCircuit
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C I : Set α
e : α
hC : M.IsCircuit C
hI : M.Indep I
hCs : C ⊆ insert e I
heC : e ∈ C
hCeI : C \ {e} ⊆ I
hss : M.fundCircuit e I ⊆ C
refine_1 : e ∈ M.closure I
refine_2 : ∀ (heI : e ∈ I), False
⊢ C = M.fundCircuit e I

Tactic:
refine hC.eq_of_superset_isCircuit (hI.fundCircuit_isCircuit ?_ fun heI ↦ ?_) hss

Premises used: Matroid.IsCircuit.eq_of_superset_isCircuit, Matroid.Indep.fundCircuit_isCircuit
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C I : Set α
e : α
hC : M.IsCircuit C
hI : M.Indep I
hCs : C ⊆ insert e I
heC : e ∈ C
hCeI : C \ {e} ⊆ I
hss : M.fundCircuit e I ⊆ C
refine_1 : M.Dep (insert e I) ∨ e ∈ I
⊢ e ∈ M.closure I

Tactic:
rw [hI.mem_closure_iff]

Premises used: Matroid.Indep.mem_closure_iff
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C I : Set α
e : α
hC : M.IsCircuit C
hI : M.Indep I
hCs : C ⊆ insert e I
heC : e ∈ C
hCeI : C \ {e} ⊆ I
hss : M.fundCircuit e I ⊆ C
⊢ M.Dep (insert e I) ∨ e ∈ I

Tactic:
.inl (hC.dep.superset hCs (insert_subset (hC.subset_ground heC) hI.subset_ground))

Premises used: Matroid.Dep.superset, Matroid.Indep.subset_ground, Matroid.IsCircuit.subset_ground, Or.inl, Matroid.IsCircuit.dep, Set.insert_subset
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C I : Set α
e : α
hC : M.IsCircuit C
hI : M.Indep I
hCs : C ⊆ insert e I
heC : e ∈ C
hCeI : C \ {e} ⊆ I
hss : M.fundCircuit e I ⊆ C
⊢ M.Dep (insert e I) ∨ e ∈ I

Tactic:
exact .inl (hC.dep.superset hCs (insert_subset (hC.subset_ground heC) hI.subset_ground))
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C I : Set α
e : α
hC : M.IsCircuit C
hI : M.Indep I
hCs : C ⊆ insert e I
heC : e ∈ C
hCeI : C \ {e} ⊆ I
hss : M.fundCircuit e I ⊆ C
heI : e ∈ I
⊢ insert e I ⊆ I

Tactic:
simp [heI]
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C I : Set α
e : α
hC : M.IsCircuit C
hI : M.Indep I
hCs : C ⊆ insert e I
heC : e ∈ C
hCeI : C \ {e} ⊆ I
hss : M.fundCircuit e I ⊆ C
heI : e ∈ I
⊢ False

Tactic:
exact hC.not_indep (hI.subset (hCs.trans (by simp [heI])))

Premises used: HasSubset.Subset.trans, Matroid.Indep.subset, Matroid.IsCircuit.not_indep
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C I : Set α
e : α
hC : M.IsCircuit C
hI : M.Indep I
hCs : C ⊆ insert e I
heC : e ∈ C
hCeI : C \ {e} ⊆ I
inr : M.fundCircuit e I ⊆ C
⊢ C = M.fundCircuit e I

Tactic:
suffices hss : M.fundCircuit e I ⊆ C by
    refine hC.eq_of_superset_isCircuit (hI.fundCircuit_isCircuit ?_ fun heI ↦ ?_) hss
    · rw [hI.mem_closure_iff]
      exact .inl (hC.dep.superset hCs (insert_subset (hC.subset_ground heC) hI.subset_ground))
    exact hC.not_indep (hI.subset (hCs.trans (by simp [heI])))
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C I : Set α
e : α
hC : M.IsCircuit C
hI : M.Indep I
hCs : C ⊆ insert e I
heC : e ∈ C
hCeI : C \ {e} ⊆ I
⊢ e ∈ M.closure (C \ {e})

Tactic:
have heCcl := (hC.diff_singleton_isBasis heC).subset_closure heC
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C I : Set α
e : α
hC : M.IsCircuit C
hI : M.Indep I
hCs : C ⊆ insert e I
heC : e ∈ C
hCeI : C \ {e} ⊆ I
heCcl : e ∈ M.closure (C \ {e})
⊢ e ∈ M.closure I

Tactic:
have heI : e ∈ M.closure I := M.closure_subset_closure hCeI heCcl
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C I : Set α
e : α
hC : M.IsCircuit C
hI : M.Indep I
hCs : C ⊆ insert e I
heC : e ∈ C
hCeI : C \ {e} ⊆ I
heCcl : e ∈ M.closure (C \ {e})
heI : e ∈ M.closure I
inr : insert e (⋂₀ {J : Set α | J ⊆ I ∧ e ∈ M.closure J}) ⊆ C
⊢ M.fundCircuit e I ⊆ C

Tactic:
rw [fundCircuit_eq_sInter heI]

Premises used: Matroid.fundCircuit_eq_sInter
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C I : Set α
e : α
hC : M.IsCircuit C
hI : M.Indep I
hCs : C ⊆ insert e I
heC : e ∈ C
hCeI : C \ {e} ⊆ I
heCcl : e ∈ M.closure (C \ {e})
heI : e ∈ M.closure I
⊢ insert e (⋂₀ {J : Set α | J ⊆ I ∧ e ∈ M.closure J}) ⊆ C

Tactic:
insert_subset heC <| (sInter_subset_of_mem (t := C \ {e}) ?_).trans diff_subset

Premises used: Set.diff_subset, HasSubset.Subset.trans, Set.sInter_subset_of_mem, Set.insert_subset
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C I : Set α
e : α
hC : M.IsCircuit C
hI : M.Indep I
hCs : C ⊆ insert e I
heC : e ∈ C
hCeI : C \ {e} ⊆ I
heCcl : e ∈ M.closure (C \ {e})
heI : e ∈ M.closure I
inr : Membership.mem (γ := Set (Set α)) {J : Set α | J ⊆ I ∧ e ∈ M.closure J} (C \ {e})
⊢ insert e (⋂₀ {J : Set α | J ⊆ I ∧ e ∈ M.closure J}) ⊆ C

Tactic:
refine insert_subset heC <| (sInter_subset_of_mem (t := C \ {e}) ?_).trans diff_subset

Premises used: Set.diff_subset, HasSubset.Subset.trans, Set.sInter_subset_of_mem, Set.insert_subset
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C I : Set α
e : α
hC : M.IsCircuit C
hI : M.Indep I
hCs : C ⊆ insert e I
heC : e ∈ C
hCeI : C \ {e} ⊆ I
heCcl : e ∈ M.closure (C \ {e})
heI : e ∈ M.closure I
⊢ Membership.mem (γ := Set (Set α)) {J : Set α | J ⊆ I ∧ e ∈ M.closure J} (C \ {e})

Tactic:
⟨hCeI, heCcl⟩

Premises used: Set.Mem, setOf, And.intro
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C I : Set α
e : α
hC : M.IsCircuit C
hI : M.Indep I
hCs : C ⊆ insert e I
heC : e ∈ C
hCeI : C \ {e} ⊆ I
heCcl : e ∈ M.closure (C \ {e})
heI : e ∈ M.closure I
⊢ Membership.mem (γ := Set (Set α)) {J : Set α | J ⊆ I ∧ e ∈ M.closure J} (C \ {e})

Tactic:
exact ⟨hCeI, heCcl⟩
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
R : Set α
hIR : I ⊆ R
heR : e ∈ R
hR : R ⊆ M.E
⊢ {e} ⊆ R

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
R : Set α
hIR : I ⊆ R
heR : e ∈ R
hR : R ⊆ M.E
simp_rw :
  insert e (I ∩ ⋂₀ {J : Set α | J ⊆ I ∧ M.closure {e} ∩ R ⊆ (M ↾ R).closure J}) =
    insert e (I ∩ ⋂₀ {J : Set α | J ⊆ I ∧ M.closure {e} ⊆ M.closure J})
⊢ (M ↾ R).fundCircuit e I = M.fundCircuit e I

Tactic:
simp_rw [fundCircuit, M.restrict_closure_eq (R := R) (X := {e}) (by simpa)]

Premises used: Matroid.restrict_closure_eq, Matroid.fundCircuit
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
R : Set α
hIR : I ⊆ R
heR : e ∈ R
hR : R ⊆ M.E
a :
  insert e (I ∩ ⋂₀ {J : Set α | J ⊆ I ∧ M.closure {e} ∩ R ⊆ (M ↾ R).closure J}) ⊆
    insert e (I ∩ ⋂₀ {J : Set α | J ⊆ I ∧ M.closure {e} ⊆ M.closure J})
a₁ :
  insert e (I ∩ ⋂₀ {J : Set α | J ⊆ I ∧ M.closure {e} ⊆ M.closure J}) ⊆
    insert e (I ∩ ⋂₀ {J : Set α | J ⊆ I ∧ M.closure {e} ∩ R ⊆ (M ↾ R).closure J})
⊢ insert e (I ∩ ⋂₀ {J : Set α | J ⊆ I ∧ M.closure {e} ∩ R ⊆ (M ↾ R).closure J}) =
    insert e (I ∩ ⋂₀ {J : Set α | J ⊆ I ∧ M.closure {e} ⊆ M.closure J})

Tactic:
apply subset_antisymm

Premises used: subset_antisymm
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
R : Set α
hIR : I ⊆ R
heR : e ∈ R
hR : R ⊆ M.E
a : ∀ (J : Set α) (hJI : J ⊆ I), M.closure {e} ⊆ M.closure J → M.closure {e} ∩ R ⊆ (M ↾ R).closure J
⊢ insert e (I ∩ ⋂₀ {J : Set α | J ⊆ I ∧ M.closure {e} ∩ R ⊆ (M ↾ R).closure J}) ⊆
    insert e (I ∩ ⋂₀ {J : Set α | J ⊆ I ∧ M.closure {e} ⊆ M.closure J})

Tactic:
gcongr 5 with J hJI
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
R : Set α
hIR : I ⊆ R
heR : e ∈ R
hR : R ⊆ M.E
J : Set α
hJI : J ⊆ I
heJ : M.closure {e} ⊆ M.closure J
a : M.closure {e} ∩ R ⊆ M.closure (J ∩ R) ∩ R ∪ R \ M.E
⊢ M.closure {e} ∩ R ⊆ (M ↾ R).closure J

Tactic:
simp only [restrict_closure_eq']

Premises used: Matroid.restrict_closure_eq'
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
R : Set α
hIR : I ⊆ R
heR : e ∈ R
hR : R ⊆ M.E
J : Set α
hJI : J ⊆ I
heJ : M.closure {e} ⊆ M.closure J
⊢ M.closure {e} ∩ R ⊆ M.closure (J ∩ R) ∩ R ∪ R \ M.E

Tactic:
(inter_subset_inter_left _ ?_).trans subset_union_left

Premises used: HasSubset.Subset.trans, Set.inter_subset_inter_left, Set.subset_union_left
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
R : Set α
hIR : I ⊆ R
heR : e ∈ R
hR : R ⊆ M.E
J : Set α
hJI : J ⊆ I
heJ : M.closure {e} ⊆ M.closure J
a : M.closure {e} ⊆ M.closure (J ∩ R)
⊢ M.closure {e} ∩ R ⊆ M.closure (J ∩ R) ∩ R ∪ R \ M.E

Tactic:
refine (inter_subset_inter_left _ ?_).trans subset_union_left

Premises used: HasSubset.Subset.trans, Set.inter_subset_inter_left, Set.subset_union_left
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
R : Set α
hIR : I ⊆ R
heR : e ∈ R
hR : R ⊆ M.E
J : Set α
hJI : J ⊆ I
heJ a a₁ a₂ a₃ : M.closure {e} ⊆ M.closure J
⊢ M.closure {e} ⊆ M.closure (J ∩ R)

Tactic:
rwa [inter_eq_self_of_subset_left (hJI.trans hIR)]

Premises used: HasSubset.Subset.trans, Set.inter_eq_self_of_subset_left
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
R : Set α
hIR : I ⊆ R
heR : e ∈ R
hR : R ⊆ M.E
a : ∀ (J : Set α) (hJI : J ⊆ I), M.closure {e} ∩ R ⊆ (M ↾ R).closure J → M.closure {e} ⊆ M.closure J
⊢ insert e (I ∩ ⋂₀ {J : Set α | J ⊆ I ∧ M.closure {e} ⊆ M.closure J}) ⊆
    insert e (I ∩ ⋂₀ {J : Set α | J ⊆ I ∧ M.closure {e} ∩ R ⊆ (M ↾ R).closure J})

Tactic:
gcongr 5 with J hJI
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
R : Set α
hIR : I ⊆ R
heR : e ∈ R
hR : R ⊆ M.E
J : Set α
hJI : J ⊆ I
heJ : M.closure {e} ∩ R ⊆ (M ↾ R).closure J
⊢ M.closure {e} ⊆ M.closure J

Tactic:
closure_subset_closure_of_subset_closure ?_

Premises used: Matroid.closure_subset_closure_of_subset_closure