awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C : Set α
hC : M.IsCircuit C
⊢ C ⊆ M.E

Tactic:
hC.dep.subset_ground

Premises used: Matroid.Dep.subset_ground, Matroid.IsCircuit.dep
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C : Set α
hC : M.IsCircuit C
⊢ C.Nonempty

Tactic:
hC.dep.nonempty

Premises used: Matroid.Dep.nonempty, Matroid.IsCircuit.dep
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
h : M.IsCircuit ∅
⊢ False

Tactic:
simpa using h.nonempty

Premises used: Matroid.IsCircuit.nonempty
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C : Set α
simp_rw : Minimal M.Dep C ↔ M.Dep C ∧ ∀ ⦃D : Set α⦄, M.Dep D → D ⊆ C → D = C
simp_rw₁ : (M.Dep C ∧ ∀ ⦃t : Set α⦄, M.Dep t → t ⊆ C → C = t) ↔ M.Dep C ∧ ∀ ⦃D : Set α⦄, M.Dep D → D ⊆ C → D = C
⊢ M.IsCircuit C ↔ M.Dep C ∧ ∀ ⦃D : Set α⦄, M.Dep D → D ⊆ C → D = C

Tactic:
simp_rw [isCircuit_def, minimal_subset_iff, eq_comm (a := C)]

Premises used: eq_comm, minimal_subset_iff, Matroid.isCircuit_def
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C X : Set α
hC : M.IsCircuit C
hXC : X ⊂ C
rw : ¬M.Dep X
⊢ M.Indep X

Tactic:
rw [← not_dep_iff (hXC.subset.trans hC.subset_ground)]

Premises used: HasSubset.Subset.trans, HasSSubset.SSubset.subset, Matroid.IsCircuit.subset_ground, Matroid.not_dep_iff
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C X : Set α
hC : M.IsCircuit C
hXC : X ⊂ C
⊢ ¬M.Dep X

Tactic:
fun h ↦ hXC.ne ((isCircuit_iff.1 hC).2 h hXC.subset)

Premises used: HasSSubset.SSubset.subset, And.right, HasSSubset.SSubset.ne, Iff.mp, Not, Matroid.isCircuit_iff
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C X : Set α
hC : M.IsCircuit C
hXC : X ⊂ C
⊢ ¬M.Dep X

Tactic:
exact fun h ↦ hXC.ne ((isCircuit_iff.1 hC).2 h hXC.subset)

Premises used: HasSSubset.SSubset.subset, And.right, HasSSubset.SSubset.ne, Iff.mp, Matroid.isCircuit_iff
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C : Set α
hC : M.IsCircuit C
simp_rw : ∀ ⦃t : Set α⦄, t ⊂ C → M.Indep t
⊢ Minimal (fun (x : Set α) ↦ ¬M.Indep x) C

Tactic:
simp_rw [minimal_iff_forall_ssubset, and_iff_right hC.not_indep, not_not]

Premises used: Set.minimal_iff_forall_ssubset, Classical.not_not, and_iff_right, Matroid.IsCircuit.not_indep
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C : Set α
hC : M.IsCircuit C
⊢ ∀ ⦃t : Set α⦄, t ⊂ C → M.Indep t

Tactic:
fun ⦃t⦄ a ↦ ssubset_indep hC a

Premises used: Matroid.IsCircuit.ssubset_indep
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C : Set α
hC : M.IsCircuit C
⊢ ∀ ⦃t : Set α⦄, t ⊂ C → M.Indep t

Tactic:
exact fun ⦃t⦄ a ↦ ssubset_indep hC a

Premises used: Matroid.IsCircuit.ssubset_indep
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C : Set α
hCE : C ⊆ M.E
⊢ M.IsCircuit C ↔ Minimal (fun (x : Set α) ↦ ¬M.Indep x) C

Tactic:
⟨IsCircuit.minimal_not_indep, fun h ↦ ⟨(not_indep_iff hCE).1 h.prop,
    fun _ hJ hJC ↦ (h.eq_of_superset hJ.not_indep hJC).le⟩⟩

Premises used: Matroid.Dep.not_indep, Minimal.prop, Eq.le, And.intro, Iff.intro, Iff.mp, Matroid.not_indep_iff, Matroid.IsCircuit.minimal_not_indep, Minimal.eq_of_superset
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C : Set α
e : α
hC : M.IsCircuit C
he : e ∈ C
⊢ M.Indep (C \ {e})

Tactic:
hC.ssubset_indep (diff_singleton_ssubset.2 he)

Premises used: Iff.mpr, Set.diff_singleton_ssubset, Matroid.IsCircuit.ssubset_indep
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C : Set α
rw : M.Dep C → ((∀ ⦃t : Set α⦄, t ⊂ C → ¬M.Dep t) ↔ ∀ ⦃I : Set α⦄, I ⊂ C → M.Indep I)
⊢ M.IsCircuit C ↔ M.Dep C ∧ ∀ ⦃I : Set α⦄, I ⊂ C → M.Indep I

Tactic:
rw [IsCircuit, minimal_iff_forall_ssubset, and_congr_right_iff]

Premises used: Set.minimal_iff_forall_ssubset, and_congr_right_iff, Matroid.IsCircuit
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C : Set α
⊢ M.Dep C → ((∀ ⦃t : Set α⦄, t ⊂ C → ¬M.Dep t) ↔ ∀ ⦃I : Set α⦄, I ⊂ C → M.Indep I)

Tactic:
fun h ↦ ⟨fun h' I hIC ↦ ((not_dep_iff (hIC.subset.trans h.subset_ground)).1 (h' hIC)),
    fun h I hIC ↦ (h hIC).not_dep⟩

Premises used: Matroid.Dep.subset_ground, HasSubset.Subset.trans, HasSSubset.SSubset.subset, Iff.intro, Iff.mp, Matroid.not_dep_iff, Matroid.Indep.not_dep
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C : Set α
⊢ M.Dep C → ((∀ ⦃t : Set α⦄, t ⊂ C → ¬M.Dep t) ↔ ∀ ⦃I : Set α⦄, I ⊂ C → M.Indep I)

Tactic:
exact fun h ↦ ⟨fun h' I hIC ↦ ((not_dep_iff (hIC.subset.trans h.subset_ground)).1 (h' hIC)),
    fun h I hIC ↦ (h hIC).not_dep⟩
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
⊢ IsAntichain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) (setOf M.IsCircuit)

Tactic:
fun _ hC _ hC' hne hss ↦ hne <| (IsCircuit.minimal hC').eq_of_subset hC.dep hss

Premises used: Matroid.IsCircuit.minimal, Set.Pairwise, Minimal.eq_of_subset, IsAntichain, Matroid.IsCircuit.dep, Not
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C X : Set α
hC : M.IsCircuit C
hX : ¬M.Indep X
hXC : X ⊆ C
⊢ X = C

Tactic:
eq_of_le_of_not_lt hXC (hX ∘ hC.ssubset_indep)

Premises used: Function.comp, eq_of_le_of_not_lt, Matroid.IsCircuit.ssubset_indep
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C X : Set α
hC : M.IsCircuit C
hX : M.Dep X
hXC : X ⊆ C
⊢ X = C

Tactic:
hC.eq_of_not_indep_subset hX.not_indep hXC

Premises used: Matroid.Dep.not_indep, Matroid.IsCircuit.eq_of_not_indep_subset
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C C' : Set α
hC : M.IsCircuit C
hC' : M.IsCircuit C'
⊢ ¬C' ⊂ C

Tactic:
fun h' ↦ h'.ne (hC.eq_of_dep_subset hC'.dep h'.subset)

Premises used: Matroid.IsCircuit.eq_of_dep_subset, HasSSubset.SSubset.subset, HasSSubset.SSubset.ne, Matroid.IsCircuit.dep, Not
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C C' : Set α
hC : M.IsCircuit C
hC' : M.IsCircuit C'
h : C ⊆ C'
⊢ C = C'

Tactic:
hC'.eq_of_dep_subset hC.dep h

Premises used: Matroid.IsCircuit.eq_of_dep_subset, Matroid.IsCircuit.dep
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C C' : Set α
hC : M.IsCircuit C
hC' : M.IsCircuit C'
h : C' ⊆ C
⊢ C = C'

Tactic:
(hC'.eq_of_subset_isCircuit hC h).symm

Premises used: Matroid.IsCircuit.eq_of_subset_isCircuit, Eq.symm
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C : Set α
inr :
  ∀
    (this :
      ∀ {α : Type u_1} {M : Matroid α} {C : Set α} (hCE : C ⊆ M.E),
        M.IsCircuit C ↔ M.Dep C ∧ ∀ e ∈ C, M.Indep (C \ {e}))
    (hCE : ¬C ⊆ M.E), M.IsCircuit C ↔ M.Dep C ∧ ∀ e ∈ C, M.Indep (C \ {e})
wlog :
  ∀ {α : Type u_1} {M : Matroid α} {C : Set α} (hCE : C ⊆ M.E), M.IsCircuit C ↔ M.Dep C ∧ ∀ e ∈ C, M.Indep (C \ {e})
⊢ M.IsCircuit C ↔ M.Dep C ∧ ∀ e ∈ C, M.Indep (C \ {e})

Tactic:
wlog hCE : C ⊆ M.E

Premises used: Matroid.E
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C : Set α
this :
  ∀ {α : Type u_1} {M : Matroid α} {C : Set α} (hCE : C ⊆ M.E), M.IsCircuit C ↔ M.Dep C ∧ ∀ e ∈ C, M.Indep (C \ {e})
hCE : ¬C ⊆ M.E
⊢ M.IsCircuit C ↔ M.Dep C ∧ ∀ e ∈ C, M.Indep (C \ {e})

Tactic:
iff_of_false (hCE ∘ IsCircuit.subset_ground) (fun h ↦ hCE h.1.subset_ground)

Premises used: Matroid.Dep.subset_ground, Function.comp, iff_of_false, And.left, Matroid.IsCircuit.subset_ground
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C : Set α
this :
  ∀ {α : Type u_1} {M : Matroid α} {C : Set α} (hCE : C ⊆ M.E), M.IsCircuit C ↔ M.Dep C ∧ ∀ e ∈ C, M.Indep (C \ {e})
hCE : ¬C ⊆ M.E
⊢ M.IsCircuit C ↔ M.Dep C ∧ ∀ e ∈ C, M.Indep (C \ {e})

Tactic:
exact iff_of_false (hCE ∘ IsCircuit.subset_ground) (fun h ↦ hCE h.1.subset_ground)

Premises used: Function.comp, iff_of_false, Matroid.IsCircuit.subset_ground
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α_1 : Type u_1
M_1 : Matroid α_1
C_1 : Set α_1
α : Type u_1
M : Matroid α
C : Set α
hCE : C ⊆ M.E
⊢ M.IsCircuit C ↔ M.Dep C ∧ ∀ e ∈ C, M.Indep (C \ {e})

Tactic:
simp [isCircuit_iff_minimal_not_indep hCE, ← not_indep_iff hCE,
    minimal_iff_forall_diff_singleton (P := (¬ M.Indep ·))
    (fun _ _ hY hYX hX ↦ hY <| hX.subset hYX)]

Premises used: Set.minimal_iff_forall_diff_singleton, Matroid.Indep.subset, Matroid.isCircuit_iff_minimal_not_indep, Matroid.not_indep_iff
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
heI : e ∉ I
he : e ∈ M.closure I
h : ∀ f ∈ I, e ∉ M.closure (I \ {f})
rw : ∀ e_1 ∈ insert e I, M.Indep (insert e I \ {e_1})
⊢ M.IsCircuit (insert e I)

Tactic:
rw [isCircuit_iff_dep_forall_diff_singleton_indep, hI.insert_dep_iff, and_iff_right ⟨he, heI⟩]

Premises used: and_iff_right, Matroid.Indep.insert_dep_iff, Matroid.isCircuit_iff_dep_forall_diff_singleton_indep
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
f : α
heI : f ∉ I
he : f ∈ M.closure I
h : ∀ f_1 ∈ I, f ∉ M.closure (I \ {f_1})
⊢ M.Indep (insert f I \ {f})

Tactic:
simpa [heI]
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
heI : e ∉ I
he : e ∈ M.closure I
h : ∀ f ∈ I, e ∉ M.closure (I \ {f})
hfI : e ∈ I
⊢ False

Tactic:
contradiction
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
heI : e ∉ I
he : e ∈ M.closure I
h : ∀ f ∈ I, e ∉ M.closure (I \ {f})
f : α
hfI : f ∈ I
⊢ e ∉ I \ {f}

Tactic:
simp [heI]
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
heI : e ∉ I
he : e ∈ M.closure I
h : ∀ f ∈ I, e ∉ M.closure (I \ {f})
f : α
hfI : f ∈ I
inr : e ∈ M.E \ M.closure (I \ {f})
⊢ M.Indep (insert e I \ {f})

Tactic:
rw [← insert_diff_singleton_comm (by rintro rfl; contradiction),
    (hI.diff _).insert_indep_iff_of_notMem (by simp [heI])]

Premises used: Matroid.Indep.diff, Set.insert_diff_singleton_comm, Matroid.Indep.insert_indep_iff_of_notMem
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
heI : e ∉ I
he : e ∈ M.closure I
h : ∀ f ∈ I, e ∉ M.closure (I \ {f})
f : α
hfI : f ∈ I
⊢ e ∈ M.E \ M.closure (I \ {f})

Tactic:
⟨mem_ground_of_mem_closure he, h f hfI⟩

Premises used: Set.Mem, Set.diff, setOf, And.intro, Matroid.mem_ground_of_mem_closure
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
heI : e ∉ I
he : e ∈ M.closure I
h : ∀ f ∈ I, e ∉ M.closure (I \ {f})
f : α
hfI : f ∈ I
⊢ e ∈ M.E \ M.closure (I \ {f})

Tactic:
exact ⟨mem_ground_of_mem_closure he, h f hfI⟩
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hInt : I.Nontrivial
he : e ∈ M.closure I
h : ∀ f ∈ I, e ∉ M.closure (I \ {f})
⊢ M.IsCircuit (insert e I)

Tactic:
hI.insert_isCircuit_of_forall (fun heI ↦ ?_) he h

Premises used: Matroid.Indep.insert_isCircuit_of_forall
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hInt : I.Nontrivial
he : e ∈ M.closure I
h : ∀ f ∈ I, e ∉ M.closure (I \ {f})
refine : ∀ (heI : e ∈ I), False
⊢ M.IsCircuit (insert e I)

Tactic:
refine hI.insert_isCircuit_of_forall (fun heI ↦ ?_) he h

Premises used: Matroid.Indep.insert_isCircuit_of_forall
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hInt : I.Nontrivial
he : e ∈ M.closure I
h : ∀ f ∈ I, e ∉ M.closure (I \ {f})
heI : e ∈ I
obtain : ∀ (f : α) (hf : f ∈ I) (hne : f ≠ e), False
⊢ False

Tactic:
obtain ⟨f, hf, hne⟩ := hInt.exists_ne e

Premises used: Set.Nontrivial.exists_ne
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hInt : I.Nontrivial
he : e ∈ M.closure I
h : ∀ f ∈ I, e ∉ M.closure (I \ {f})
heI : e ∈ I
f : α
hf : f ∈ I
hne : f ≠ e
⊢ e ∈ I \ {f}

Tactic:
simp [heI, hne.symm]

Premises used: Ne.symm
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hInt : I.Nontrivial
he : e ∈ M.closure I
h : ∀ f ∈ I, e ∉ M.closure (I \ {f})
heI : e ∈ I
f : α
hf : f ∈ I
hne : f ≠ e
⊢ False

Tactic:
exact h f hf (mem_closure_of_mem' _ (by simp [heI, hne.symm]))

Premises used: Matroid.mem_closure_of_mem'
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C : Set α
e : α
hC : M.IsCircuit C
he : e ∈ C
nth_rw : M.IsBasis (C \ {e}) (insert e C)
⊢ M.IsBasis (C \ {e}) C

Tactic:
nth_rw 2 [← insert_eq_of_mem he]

Premises used: Set.insert_eq_of_mem
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C : Set α
e : α
hC : M.IsCircuit C
he : e ∈ C
rw : M.Dep C ∨ e ∈ C \ {e}
⊢ M.IsBasis (C \ {e}) (insert e C)

Tactic:
rw [← insert_diff_singleton, (hC.diff_singleton_indep he).isBasis_insert_iff,
    insert_diff_singleton, insert_eq_of_mem he]

Premises used: Matroid.Indep.isBasis_insert_iff, Set.insert_eq_of_mem, Matroid.IsCircuit.diff_singleton_indep, Set.insert_diff_singleton
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C : Set α
e : α
hC : M.IsCircuit C
he : e ∈ C
⊢ M.Dep C ∨ e ∈ C \ {e}

Tactic:
Or.inl hC.dep

Premises used: Or.inl, Matroid.IsCircuit.dep
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C : Set α
e : α
hC : M.IsCircuit C
he : e ∈ C
⊢ M.Dep C ∨ e ∈ C \ {e}

Tactic:
exact Or.inl hC.dep

Premises used: Or.inl, Matroid.IsCircuit.dep
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C I : Set α
hC : M.IsCircuit C
⊢ M.IsBasis I C ↔ ∃ e ∈ C, I = C \ {e}

Tactic:
⟨fun h ↦ ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C I : Set α
hC : M.IsCircuit C
refine_1 : ∀ (h : M.IsBasis I C), ∃ e ∈ C, I = C \ {e}
refine_2 : (∃ e ∈ C, I = C \ {e}) → M.IsBasis I C
⊢ M.IsBasis I C ↔ ∃ e ∈ C, I = C \ {e}

Tactic:
refine ⟨fun h ↦ ?_, ?_⟩
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
I : Set α
hC : M.IsCircuit I
h : M.IsBasis I I
⊢ False

Tactic:
hC.dep.not_indep h.indep

Premises used: Matroid.Dep.not_indep, Matroid.IsBasis.indep, Matroid.IsCircuit.dep
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
I : Set α
hC : M.IsCircuit I
h : M.IsBasis I I
⊢ False

Tactic:
exact hC.dep.not_indep h.indep

Premises used: Matroid.Dep.not_indep, Matroid.IsBasis.indep, Matroid.IsCircuit.dep
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C I : Set α
hC : M.IsCircuit C
h : M.IsBasis I C
refine_1 : ∀ (e : α) (he : e ∈ C ∧ e ∉ I), ∃ e ∈ C, I = C \ {e}
⊢ ∃ e ∈ C, I = C \ {e}

Tactic:
obtain ⟨e, he⟩ := exists_of_ssubset
      (h.subset.ssubset_of_ne (by rintro rfl; exact hC.dep.not_indep h.indep))

Premises used: Set.exists_of_ssubset, Matroid.IsBasis.subset, HasSubset.Subset.ssubset_of_ne
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C I : Set α
hC : M.IsCircuit C
h : M.IsBasis I C
e : α
he : e ∈ C ∧ e ∉ I
⊢ ∃ e ∈ C, I = C \ {e}

Tactic:
⟨e, he.1, h.eq_of_subset_indep (hC.diff_singleton_indep he.1)
      (subset_diff_singleton h.subset he.2) diff_subset⟩

Premises used: Set.diff_subset, Matroid.IsBasis.subset, Matroid.IsBasis.eq_of_subset_indep, And.right, And.left, Set.subset_diff_singleton, And.intro, Exists.intro, Matroid.IsCircuit.diff_singleton_indep
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C I : Set α
hC : M.IsCircuit C
h : M.IsBasis I C
e : α
he : e ∈ C ∧ e ∉ I
⊢ ∃ e ∈ C, I = C \ {e}

Tactic:
exact ⟨e, he.1, h.eq_of_subset_indep (hC.diff_singleton_indep he.1)
      (subset_diff_singleton h.subset he.2) diff_subset⟩
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C : Set α
hC : M.IsCircuit C
e : α
he : e ∈ C
⊢ M.IsBasis (C \ {e}) C

Tactic:
hC.diff_singleton_isBasis he

Premises used: Matroid.IsCircuit.diff_singleton_isBasis
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C : Set α
hC : M.IsCircuit C
e : α
he : e ∈ C
⊢ M.IsBasis (C \ {e}) C

Tactic:
exact hC.diff_singleton_isBasis he

Premises used: Matroid.IsCircuit.diff_singleton_isBasis
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C I : Set α
hC : M.IsCircuit C
rw : (∃ e ∈ C, I = C \ {e}) ↔ ∃ e ∈ C \ I, C = insert e I
⊢ M.IsBasis I C ↔ ∃ e ∈ C \ I, C = insert e I

Tactic:
rw [hC.isBasis_iff_eq_diff_singleton]

Premises used: Matroid.IsCircuit.isBasis_iff_eq_diff_singleton
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C I : Set α
hC : M.IsCircuit C
⊢ (∃ e ∈ C, I = C \ {e}) ↔ ∃ e ∈ C \ I, C = insert e I

Tactic:
⟨fun ⟨e, he, hI⟩ ↦ ⟨e, ⟨he, fun heI ↦ (hI.subset heI).2 rfl⟩, ?_⟩,
    fun ⟨e, he, hC⟩ ↦ ⟨e, he.1, ?_⟩⟩

Premises used: _private.0.Matroid.IsCircuit.isBasis_iff_insert_eq.match_1, Membership.mem, Exists, Insert.insert, Eq.subset, SDiff.sdiff, And, _private.0.Matroid.IsCircuit.isBasis_iff_insert_eq.match_2, And.right, And.left, And.intro, Iff.intro, Exists.intro, Singleton.singleton, Eq, rfl
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C I : Set α
hC : M.IsCircuit C
refine_1 : (∃ e ∈ C, I = C \ {e}) → ∀ (e : α) (he : e ∈ C) (hI : I = C \ {e}), C = insert e I
refine_2 : (∃ e ∈ C \ I, C = insert e I) → ∀ (e : α) (he : e ∈ C \ I) (hC : C = insert e I), I = C \ {e}
⊢ (∃ e ∈ C, I = C \ {e}) ↔ ∃ e ∈ C \ I, C = insert e I

Tactic:
refine ⟨fun ⟨e, he, hI⟩ ↦ ⟨e, ⟨he, fun heI ↦ (hI.subset heI).2 rfl⟩, ?_⟩,
    fun ⟨e, he, hC⟩ ↦ ⟨e, he.1, ?_⟩⟩
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C I : Set α
hC : M.IsCircuit C
h : ∃ e ∈ C, I = C \ {e}
e : α
he : e ∈ C
hI : I = C \ {e}
refine_1 : C = insert e (C \ {e})
refine_1₁ : C = insert e C
refine_1₂ refine_1₃ : C = C
⊢ C = insert e I

Tactic:
rw [hI, insert_diff_singleton, insert_eq_of_mem he]

Premises used: Set.insert_eq_of_mem, Set.insert_diff_singleton
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C I : Set α
hC_1 : M.IsCircuit C
h : ∃ e ∈ C \ I, C = insert e I
e : α
he : e ∈ C \ I
hC : C = insert e I
refine_2 : I = insert e I \ {e}
refine_2₁ refine_2₂ : I = I
⊢ I = C \ {e}

Tactic:
rw [hC, insert_diff_self_of_notMem he.2]

Premises used: Set.insert_diff_self_of_notMem, And.right
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C R : Set α
hC : M.IsCircuit C
hCR : C ⊆ R
simp_rw :
  ∀ (hC : (¬M.Indep C ∧ C ⊆ M.E) ∧ ∀ ⦃D : Set α⦄, ¬M.Indep D → D ⊆ M.E → D ⊆ C → D = C),
    (¬M.Indep C ∧ C ⊆ R) ∧ ∀ ⦃D : Set α⦄, ¬M.Indep D → D ⊆ R → D ⊆ C → D = C
⊢ (M ↾ R).IsCircuit C

Tactic:
simp_rw [isCircuit_iff, restrict_dep_iff, dep_iff, and_imp] at *

Premises used: and_imp, Matroid.restrict_dep_iff, Matroid.isCircuit_iff, Matroid.dep_iff
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C R : Set α
hCR : C ⊆ R
hC : (¬M.Indep C ∧ C ⊆ M.E) ∧ ∀ ⦃D : Set α⦄, ¬M.Indep D → D ⊆ M.E → D ⊆ C → D = C
⊢ (¬M.Indep C ∧ C ⊆ R) ∧ ∀ ⦃D : Set α⦄, ¬M.Indep D → D ⊆ R → D ⊆ C → D = C

Tactic:
⟨⟨hC.1.1, hCR⟩, fun I hI _ hIC ↦ hC.2 hI (hIC.trans hC.1.2) hIC⟩

Premises used: HasSubset.Subset.trans, And.right, And.left, And.intro
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C R : Set α
hCR : C ⊆ R
hC : (¬M.Indep C ∧ C ⊆ M.E) ∧ ∀ ⦃D : Set α⦄, ¬M.Indep D → D ⊆ M.E → D ⊆ C → D = C
⊢ (¬M.Indep C ∧ C ⊆ R) ∧ ∀ ⦃D : Set α⦄, ¬M.Indep D → D ⊆ R → D ⊆ C → D = C

Tactic:
exact ⟨⟨hC.1.1, hCR⟩, fun I hI _ hIC ↦ hC.2 hI (hIC.trans hC.1.2) hIC⟩
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C R : Set α
hR : R ⊆ M.E
⊢ (M ↾ R).IsCircuit C ↔ M.IsCircuit C ∧ C ⊆ R

Tactic:
⟨?_, fun h ↦ h.1.isCircuit_restrict_of_subset h.2⟩

Premises used: And.right, And.left, Iff.intro, Matroid.IsCircuit.isCircuit_restrict_of_subset
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C R : Set α
hR : R ⊆ M.E
refine : (M ↾ R).IsCircuit C → M.IsCircuit C ∧ C ⊆ R
⊢ (M ↾ R).IsCircuit C ↔ M.IsCircuit C ∧ C ⊆ R

Tactic:
refine ⟨?_, fun h ↦ h.1.isCircuit_restrict_of_subset h.2⟩
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C R : Set α
hR : R ⊆ M.E
simp_rw :
  ¬M.Indep C →
    C ⊆ R →
      (∀ ⦃D : Set α⦄, ¬M.Indep D → D ⊆ R → D ⊆ C → D = C) →
        ((¬M.Indep C ∧ C ⊆ M.E) ∧ ∀ ⦃D : Set α⦄, ¬M.Indep D ∧ D ⊆ M.E → D ⊆ C → D = C) ∧ C ⊆ R
⊢ (M ↾ R).IsCircuit C → M.IsCircuit C ∧ C ⊆ R

Tactic:
simp_rw [isCircuit_iff, restrict_dep_iff, and_imp, dep_iff]

Premises used: and_imp, Matroid.restrict_dep_iff, Matroid.isCircuit_iff, Matroid.dep_iff
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C R : Set α
hR : R ⊆ M.E
⊢ ¬M.Indep C →
    C ⊆ R →
      (∀ ⦃D : Set α⦄, ¬M.Indep D → D ⊆ R → D ⊆ C → D = C) →
        ((¬M.Indep C ∧ C ⊆ M.E) ∧ ∀ ⦃D : Set α⦄, ¬M.Indep D ∧ D ⊆ M.E → D ⊆ C → D = C) ∧ C ⊆ R

Tactic:
fun hC hCR h ↦ ⟨⟨⟨hC,hCR.trans hR⟩,fun I hI hIC ↦ h hI.1 (hIC.trans hCR) hIC⟩,hCR⟩

Premises used: HasSubset.Subset.trans, And.left, And.intro
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C R : Set α
hR : R ⊆ M.E
⊢ ¬M.Indep C →
    C ⊆ R →
      (∀ ⦃D : Set α⦄, ¬M.Indep D → D ⊆ R → D ⊆ C → D = C) →
        ((¬M.Indep C ∧ C ⊆ M.E) ∧ ∀ ⦃D : Set α⦄, ¬M.Indep D ∧ D ⊆ M.E → D ⊆ C → D = C) ∧ C ⊆ R

Tactic:
exact fun hC hCR h ↦ ⟨⟨⟨hC,hCR.trans hR⟩,fun I hI hIC ↦ h hI.1 (hIC.trans hCR) hIC⟩,hCR⟩
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
he : e ∈ M.closure I
⊢ {e} ⊆ M.E

Tactic:
simpa using mem_ground_of_mem_closure he

Premises used: Matroid.mem_ground_of_mem_closure
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
he : e ∈ M.closure I
simp_rw : insert e (I ∩ ⋂₀ {J : Set α | J ⊆ I ∧ e ∈ M.closure J}) = insert e (⋂₀ {J : Set α | J ⊆ I ∧ e ∈ M.closure J})
⊢ insert e (I ∩ ⋂₀ {J : Set α | J ⊆ I ∧ M.closure {e} ⊆ M.closure J}) =
    insert e (⋂₀ {J : Set α | J ⊆ I ∧ e ∈ M.closure J})

Tactic:
simp_rw [closure_subset_closure_iff_subset_closure
    (show {e} ⊆ M.E by simpa using mem_ground_of_mem_closure he), singleton_subset_iff]

Premises used: Set.singleton_subset_iff, Matroid.closure_subset_closure_iff_subset_closure
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
he : e ∈ M.closure 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 : α
he : e ∈ M.closure I
rw rw₁ :
  Eq (α := Set α) (insert e (⋂₀ {J : Set α | J ⊆ I ∧ e ∈ M.closure J}))
    (insert e (⋂₀ {J : Set α | J ⊆ I ∧ e ∈ M.closure J}))
⊢ insert e (I ∩ ⋂₀ {J : Set α | J ⊆ I ∧ e ∈ M.closure J}) = insert e (⋂₀ {J : Set α | J ⊆ I ∧ e ∈ M.closure J})

Tactic:
rw [inter_eq_self_of_subset_right (sInter_subset_of_mem (by simpa))]

Premises used: Set.sInter_subset_of_mem, Set.inter_eq_self_of_subset_right
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
e : α
I : Set α
⊢ M.fundCircuit e I ⊆ insert e I

Tactic:
insert_subset_insert inter_subset_left

Premises used: Set.inter_subset_left, Matroid.fundCircuit, Set.insert_subset_insert
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
he : e ∈ M.E
hI : I ⊆ M.E
⊢ M.fundCircuit e I ⊆ M.E

Tactic:
(M.fundCircuit_subset_insert e I).trans (insert_subset he hI)

Premises used: HasSubset.Subset.trans, Set.insert_subset, Matroid.fundCircuit_subset_insert
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
e : α
I : Set α
⊢ e ∈ M.fundCircuit e I

Tactic:
mem_insert ..

Premises used: Set.Mem, Set.mem_insert, Matroid.fundCircuit