awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
K : Set α
aux : M✶.Dep = fun (X : Set α) ↦ (∀ (B : Set α), M.IsBase B → (X ∩ B).Nonempty) ∧ X ⊆ M.E
X : Set α
hX : ∀ (B : Set α), M.IsBase B → (X ∩ B).Nonempty
B : Set α
hB : M.IsBase B
⊢ (X ∩ B).Nonempty

Tactic:
exact hX B hB
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
K : Set α
⊢ M.IsCocircuit K ↔ Minimal (fun (X : Set α) ↦ ∀ (B : Set α), M.IsBase B → (X ∩ B).Nonempty) K

Tactic:
isCocircuit_iff_minimal

Premises used: Matroid.isCocircuit_iff_minimal
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
K : Set α
h : ∀ (K : Set α), ¬M.Spanning (M.E \ K) ↔ ∀ (B : Set α), M.IsBase B → (K ∩ B).Nonempty
⊢ M.IsCocircuit K ↔ Minimal (fun (X : Set α) ↦ ¬M.Spanning (M.E \ X)) K

Tactic:
convert! isCocircuit_iff_minimal with K

Premises used: Matroid.isCocircuit_iff_minimal
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
K_1 K : Set α
h : (¬∃ (B : Set α), M.IsBase B ∧ B ⊆ M.E \ K) ↔ ∀ (B : Set α), M.IsBase B → (K ∩ B).Nonempty
⊢ ¬M.Spanning (M.E \ K) ↔ ∀ (B : Set α), M.IsBase B → (K ∩ B).Nonempty

Tactic:
rw [spanning_iff_exists_isBase_subset]

Premises used: Matroid.spanning_iff_exists_isBase_subset
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
K_1 K : Set α
h : (∀ (x : Set α), ¬(M.IsBase x ∧ x ⊆ M.E \ K)) ↔ ∀ (B : Set α), M.IsBase B → (K ∩ B).Nonempty
h₁ : (∀ (x : Set α), ¬(M.IsBase x ∧ x ⊆ M.E ∧ Disjoint x K)) ↔ ∀ (B : Set α), M.IsBase B → (K ∩ B).Nonempty
h₂ : (∀ (x : Set α), M.IsBase x → x ⊆ M.E → ¬Disjoint x K) ↔ ∀ (B : Set α), M.IsBase B → (K ∩ B).Nonempty
h₃ : (∀ (x : Set α), M.IsBase x → x ⊆ M.E → (x ∩ K).Nonempty) ↔ ∀ (B : Set α), M.IsBase B → (K ∩ B).Nonempty
h₄ : (∀ (x : Set α), M.IsBase x ∧ x ⊆ M.E → (x ∩ K).Nonempty) ↔ ∀ (B : Set α), M.IsBase B → (K ∩ B).Nonempty
h₅ : (∀ (x : Set α), M.IsBase x → (x ∩ K).Nonempty) ↔ ∀ (B : Set α), M.IsBase B → (K ∩ B).Nonempty
⊢ (¬∃ (B : Set α), M.IsBase B ∧ B ⊆ M.E \ K) ↔ ∀ (B : Set α), M.IsBase B → (K ∩ B).Nonempty

Tactic:
simp_rw [not_exists, subset_diff, not_and, not_disjoint_iff_nonempty_inter, ← and_imp,
    and_iff_left_of_imp IsBase.subset_ground, inter_comm K]

Premises used: and_iff_left_of_imp, and_imp, not_exists, Set.subset_diff, Set.not_disjoint_iff_nonempty_inter, Matroid.IsBase.subset_ground, Set.inter_comm, not_and
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
e : α
B : Set α
hB : M.IsBase B
he : e ∈ B
rw :
  ¬M.Spanning (B \ {e}) ∧
    ∀ ⦃t : Set α⦄, ¬M.Spanning (M.E \ t) → t ⊆ M.E \ M.closure (B \ {e}) → M.E \ M.closure (B \ {e}) = t
⊢ M.IsCocircuit (M.E \ M.closure (B \ {e}))

Tactic:
rw [isCocircuit_iff_minimal_compl_nonspanning, minimal_subset_iff,
    diff_diff_cancel_left (M.closure_subset_ground _),
    closure_spanning_iff (diff_subset.trans hB.subset_ground)]

Premises used: Matroid.isCocircuit_iff_minimal_compl_nonspanning, Set.diff_subset, Matroid.closure_subset_ground, Matroid.closure_spanning_iff, HasSubset.Subset.trans, Matroid.IsBase.subset_ground, minimal_subset_iff, Set.diff_diff_cancel_left
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
e : α
B : Set α
hB : M.IsBase B
he : e ∈ B
⊢ Minimal M.Spanning B

Tactic:
have hB' := (isBase_iff_minimal_spanning.1 hB)
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
e : α
B : Set α
hB : M.IsBase B
he : e ∈ B
hB' : Minimal M.Spanning B
⊢ ¬M.Spanning (B \ {e}) ∧
    ∀ ⦃t : Set α⦄, ¬M.Spanning (M.E \ t) → t ⊆ M.E \ M.closure (B \ {e}) → M.E \ M.closure (B \ {e}) = t

Tactic:
⟨fun hsp ↦ hB'.notMem_of_prop_diff_singleton hsp he, fun X hX hXss ↦ hXss.antisymm' ?_⟩

Premises used: Minimal.notMem_of_prop_diff_singleton, And.intro, HasSubset.Subset.antisymm'
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
e : α
B : Set α
hB : M.IsBase B
he : e ∈ B
hB' : Minimal M.Spanning B
refine :
  ∀ (X : Set α) (hX : ¬M.Spanning (M.E \ X)) (hXss : X ⊆ M.E \ M.closure (B \ {e})), M.E \ M.closure (B \ {e}) ⊆ X
⊢ ¬M.Spanning (B \ {e}) ∧
    ∀ ⦃t : Set α⦄, ¬M.Spanning (M.E \ t) → t ⊆ M.E \ M.closure (B \ {e}) → M.E \ M.closure (B \ {e}) = t

Tactic:
refine ⟨fun hsp ↦ hB'.notMem_of_prop_diff_singleton hsp he, fun X hX hXss ↦ hXss.antisymm' ?_⟩
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
e : α
B : Set α
hB : M.IsBase B
he : e ∈ B
hB' : Minimal M.Spanning B
X : Set α
hX : ¬M.Spanning (M.E \ X)
hXss : X ⊆ M.E \ M.closure (B \ {e})
rw : M.E \ X ⊆ M.closure (B \ {e})
⊢ M.E \ M.closure (B \ {e}) ⊆ X

Tactic:
rw [diff_subset_comm]

Premises used: Set.diff_subset_comm
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
e : α
B : Set α
hB : M.IsBase B
he : e ∈ B
hB' : Minimal M.Spanning B
X : Set α
hX : ¬M.Spanning (M.E \ X)
hXss : X ⊆ M.E \ M.closure (B \ {e})
⊢ M.E \ X ⊆ M.closure (B \ {e})

Tactic:
fun f hf ↦ by_contra fun fcl ↦ hX ?_

Premises used: Set.Subset, by_contra
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
e : α
B : Set α
hB : M.IsBase B
he : e ∈ B
hB' : Minimal M.Spanning B
X : Set α
hX : ¬M.Spanning (M.E \ X)
hXss : X ⊆ M.E \ M.closure (B \ {e})
refine : ∀ (f : α) (hf : f ∈ M.E \ X) (fcl : f ∉ M.closure (B \ {e})), M.Spanning (M.E \ X)
⊢ M.E \ X ⊆ M.closure (B \ {e})

Tactic:
refine fun f hf ↦ by_contra fun fcl ↦ hX ?_

Premises used: by_contra
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
e : α
B : Set α
hB : M.IsBase B
he : e ∈ B
hB' : Minimal M.Spanning B
X : Set α
hX : ¬M.Spanning (M.E \ X)
hXss : X ⊆ M.E \ M.closure (B \ {e})
f : α
hf : f ∈ M.E \ X
fcl : f ∉ M.closure (B \ {e})
rw :
  ∀ (hXss : X ⊆ M.E ∧ Disjoint X (M.closure (B \ {e}))) (f : α) (hf : f ∈ M.E \ X) (fcl : f ∉ M.closure (B \ {e})),
    M.Spanning (M.E \ X)
⊢ M.Spanning (M.E \ X)

Tactic:
rw [subset_diff] at hXss

Premises used: Set.subset_diff
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
e : α
B : Set α
hB : M.IsBase B
he : e ∈ B
hB' : Minimal M.Spanning B
X : Set α
hX : ¬M.Spanning (M.E \ X)
hXss : X ⊆ M.E ∧ Disjoint X (M.closure (B \ {e}))
f : α
hf : f ∈ M.E \ X
fcl : f ∉ M.closure (B \ {e})
hsp : M.IsBase (insert f (B \ {e}))
⊢ M.Spanning (M.E \ X)

Tactic:
hsp.spanning.superset <| insert_subset hf <|
      (M.subset_closure _ (diff_subset.trans hB.subset_ground)).trans ?_

Premises used: Set.diff_subset, Matroid.IsBase.spanning, HasSubset.Subset.trans, Matroid.subset_closure, Matroid.IsBase.subset_ground, Matroid.Spanning.superset, Set.insert_subset
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
e : α
B : Set α
hB : M.IsBase B
he : e ∈ B
hB' : Minimal M.Spanning B
X : Set α
hX : ¬M.Spanning (M.E \ X)
hXss : X ⊆ M.E ∧ Disjoint X (M.closure (B \ {e}))
f : α
hf : f ∈ M.E \ X
fcl : f ∉ M.closure (B \ {e})
hsp : M.IsBase (insert f (B \ {e}))
refine : M.closure (B \ {e}) ⊆ M.E \ X
⊢ M.Spanning (M.E \ X)

Tactic:
refine hsp.spanning.superset <| insert_subset hf <|
      (M.subset_closure _ (diff_subset.trans hB.subset_ground)).trans ?_

Premises used: Set.diff_subset, Matroid.IsBase.spanning, HasSubset.Subset.trans, Matroid.subset_closure, Matroid.IsBase.subset_ground, Matroid.Spanning.superset, Set.insert_subset
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
e : α
B : Set α
hB : M.IsBase B
he : e ∈ B
hB' : Minimal M.Spanning B
X : Set α
hX : ¬M.Spanning (M.E \ X)
hXss : X ⊆ M.E ∧ Disjoint X (M.closure (B \ {e}))
f : α
hf : f ∈ M.E \ X
fcl : f ∉ M.closure (B \ {e})
hsp : M.IsBase (insert f (B \ {e}))
rw : M.closure (B \ {e}) ⊆ M.E
⊢ M.closure (B \ {e}) ⊆ M.E \ X

Tactic:
rw [subset_diff, and_iff_left hXss.2.symm]

Premises used: and_iff_left, Set.subset_diff, Disjoint.symm, And.right
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
e : α
B : Set α
hB : M.IsBase B
he : e ∈ B
hB' : Minimal M.Spanning B
X : Set α
hX : ¬M.Spanning (M.E \ X)
hXss : X ⊆ M.E ∧ Disjoint X (M.closure (B \ {e}))
f : α
hf : f ∈ M.E \ X
fcl : f ∉ M.closure (B \ {e})
hsp : M.IsBase (insert f (B \ {e}))
⊢ M.closure (B \ {e}) ⊆ M.E

Tactic:
apply closure_subset_ground

Premises used: Matroid.closure_subset_ground
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
e : α
B : Set α
hB : M.IsBase B
he : e ∈ B
hB' : Minimal M.Spanning B
X : Set α
hX : ¬M.Spanning (M.E \ X)
hXss : X ⊆ M.E ∧ Disjoint X (M.closure (B \ {e}))
f : α
hf : f ∈ M.E \ X
fcl : f ∉ M.closure (B \ {e})
suffices : M.IsBase (insert f (B \ {e}))
⊢ M.Spanning (M.E \ X)

Tactic:
suffices hsp : M.IsBase (insert f (B \ {e})) by
    refine hsp.spanning.superset <| insert_subset hf <|
      (M.subset_closure _ (diff_subset.trans hB.subset_ground)).trans ?_
    rw [subset_diff, and_iff_left hXss.2.symm]
    apply closure_subset_ground
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
e : α
B : Set α
hB : M.IsBase B
he : e ∈ B
hB' : Minimal M.Spanning B
X : Set α
hX : ¬M.Spanning (M.E \ X)
hXss : X ⊆ M.E ∧ Disjoint X (M.closure (B \ {e}))
f : α
hf : f ∈ M.E \ X
fcl : f ∉ M.closure (B \ {e})
⊢ M.IsBase (insert f (B \ {e}))

Tactic:
hB.exchange_base_of_notMem_closure he fcl

Premises used: Matroid.IsBase.exchange_base_of_notMem_closure
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
e : α
B : Set α
hB : M.IsBase B
he : e ∈ B
hB' : Minimal M.Spanning B
X : Set α
hX : ¬M.Spanning (M.E \ X)
hXss : X ⊆ M.E ∧ Disjoint X (M.closure (B \ {e}))
f : α
hf : f ∈ M.E \ X
fcl : f ∉ M.closure (B \ {e})
⊢ M.IsBase (insert f (B \ {e}))

Tactic:
exact hB.exchange_base_of_notMem_closure he fcl

Premises used: Matroid.IsBase.exchange_base_of_notMem_closure
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
K : Set α
rw : Minimal (fun (X : Set α) ↦ ¬M.Spanning (M.E \ X)) K ↔ Minimal (fun (X : Set α) ↦ ¬M.Spanning (M.E \ X) ∧ X ⊆ M.E) K
⊢ M.IsCocircuit K ↔ Minimal (fun (X : Set α) ↦ ¬M.Spanning (M.E \ X) ∧ X ⊆ M.E) K

Tactic:
rw [isCocircuit_iff_minimal_compl_nonspanning]

Premises used: Matroid.isCocircuit_iff_minimal_compl_nonspanning
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
K X : Set α
hX rwa rwa₁ rwa₂ rwa₃ : ¬M.Spanning (M.E \ X)
⊢ ¬M.Spanning (M.E \ (X ∩ M.E))

Tactic:
rwa [diff_inter_self_eq_diff]

Premises used: Set.diff_inter_self_eq_diff
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
K : Set α
⊢ Minimal (fun (X : Set α) ↦ ¬M.Spanning (M.E \ X)) K ↔ Minimal (fun (X : Set α) ↦ ¬M.Spanning (M.E \ X) ∧ X ⊆ M.E) K

Tactic:
exact minimal_iff_minimal_of_imp_of_forall (fun _ h ↦ h.1)
    (fun X hX ↦ ⟨X ∩ M.E, inter_subset_left, by rwa [diff_inter_self_eq_diff], inter_subset_right⟩)

Premises used: minimal_iff_minimal_of_imp_of_forall, Matroid.E, Set.inter_subset_left, Inter.inter, And.intro, Exists.intro
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C : Set α
e : α
K : Set α
hC : M.IsCircuit C
hK : M.IsCocircuit K
he : C ∩ K = {e}
⊢ e ∈ C

Tactic:
have heC : e ∈ C := (he.symm.subset rfl).1
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C : Set α
e : α
K : Set α
hC : M.IsCircuit C
hK : M.IsCocircuit K
he : C ∩ K = {e}
heC : e ∈ C
⊢ ¬M.Spanning (M.E \ K) ∧ ∀ ⦃t : Set α⦄, t ⊂ K → M.Spanning (M.E \ t)

Tactic:
simp_rw [isCocircuit_iff_minimal_compl_nonspanning, minimal_iff_forall_ssubset, not_not] at hK

Premises used: Set.minimal_iff_forall_ssubset, Matroid.isCocircuit_iff_minimal_compl_nonspanning, Classical.not_not
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C : Set α
e : α
K : Set α
hC : M.IsCircuit C
he : C ∩ K = {e}
heC : e ∈ C
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃t : Set α⦄, t ⊂ K → M.Spanning (M.E \ t)
⊢ M.Spanning (M.E \ (K \ {e}))

Tactic:
have' hKe := hK.2 (t := K \ {e}) (diff_singleton_ssubset.2 (he.symm.subset rfl).2)
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C : Set α
e : α
K : Set α
hC : M.IsCircuit C
he : C ∩ K = {e}
heC : e ∈ C
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃t : Set α⦄, t ⊂ K → M.Spanning (M.E \ t)
hKe : M.Spanning (M.E \ (K \ {e}))
apply : M.Spanning (M.E \ K)
⊢ False

Tactic:
apply hK.1

Premises used: And.left
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C : Set α
e : α
K : Set α
hC : M.IsCircuit C
he : C ∩ K = {e}
heC : e ∈ C
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃t : Set α⦄, t ⊂ K → M.Spanning (M.E \ t)
hKe : M.Spanning (M.E \ (K \ {e}))
rw : M.E ⊆ M.closure (M.E \ K)
⊢ M.Spanning (M.E \ K)

Tactic:
rw [spanning_iff_ground_subset_closure]

Premises used: Matroid.spanning_iff_ground_subset_closure
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C : Set α
e : α
K : Set α
hC : M.IsCircuit C
he : C ∩ K = {e}
heC : e ∈ C
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃t : Set α⦄, t ⊂ K → M.Spanning (M.E \ t)
hKe : M.Spanning (M.E \ (K \ {e}))
nth_rw : M.closure (M.E \ K ∪ {e}) ⊆ M.closure (M.E \ K)
nth_rw₁ : {e} ⊆ M.E
⊢ M.E ⊆ M.closure (M.E \ K)

Tactic:
nth_rw 1 [← hKe.closure_eq, diff_diff_eq_sdiff_union]

Premises used: Matroid.Spanning.closure_eq, Set.diff_diff_eq_sdiff_union
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C : Set α
e : α
K : Set α
hC : M.IsCircuit C
he : C ∩ K = {e}
heC : e ∈ C
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃t : Set α⦄, t ⊂ K → M.Spanning (M.E \ t)
hKe : M.Spanning (M.E \ (K \ {e}))
⊢ M.closure (M.E \ K ∪ {e}) ⊆ M.closure (M.E \ K)

Tactic:
(M.closure_subset_closure (subset_union_left (t := C))).trans ?_

Premises used: HasSubset.Subset.trans, Matroid.closure_subset_closure, Set.subset_union_left
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C : Set α
e : α
K : Set α
hC : M.IsCircuit C
he : C ∩ K = {e}
heC : e ∈ C
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃t : Set α⦄, t ⊂ K → M.Spanning (M.E \ t)
hKe : M.Spanning (M.E \ (K \ {e}))
refine : M.closure (M.E \ K ∪ {e} ∪ C) ⊆ M.closure (M.E \ K)
⊢ M.closure (M.E \ K ∪ {e}) ⊆ M.closure (M.E \ K)

Tactic:
refine (M.closure_subset_closure (subset_union_left (t := C))).trans ?_

Premises used: HasSubset.Subset.trans, Matroid.closure_subset_closure, Set.subset_union_left
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C : Set α
e : α
K : Set α
hC : M.IsCircuit C
he : C ∩ K = {e}
heC : e ∈ C
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃t : Set α⦄, t ⊂ K → M.Spanning (M.E \ t)
hKe : M.Spanning (M.E \ (K \ {e}))
rw : C \ {e} ⊆ M.E \ K
⊢ M.closure (M.E \ K ∪ {e} ∪ C) ⊆ M.closure (M.E \ K)

Tactic:
rw [union_assoc, singleton_union, insert_eq_of_mem heC, ← closure_union_congr_right
      (hC.closure_diff_singleton_eq e), union_eq_self_of_subset_right]

Premises used: Matroid.closure_union_congr_right, Matroid.IsCircuit.closure_diff_singleton_eq, Set.union_eq_self_of_subset_right, Set.singleton_union, Set.insert_eq_of_mem, Set.union_assoc
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C : Set α
e : α
K : Set α
hC : M.IsCircuit C
he : C ∩ K = {e}
heC : e ∈ C
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃t : Set α⦄, t ⊂ K → M.Spanning (M.E \ t)
hKe : M.Spanning (M.E \ (K \ {e}))
rw : C \ K ⊆ M.E \ K
⊢ C \ {e} ⊆ M.E \ K

Tactic:
rw [← he, diff_self_inter]

Premises used: Set.diff_self_inter
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C : Set α
e : α
K : Set α
hC : M.IsCircuit C
he : C ∩ K = {e}
heC : e ∈ C
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃t : Set α⦄, t ⊂ K → M.Spanning (M.E \ t)
hKe : M.Spanning (M.E \ (K \ {e}))
⊢ C \ K ⊆ M.E \ K

Tactic:
diff_subset_diff_left hC.subset_ground

Premises used: Set.diff_subset_diff_left, Matroid.IsCircuit.subset_ground
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C : Set α
e : α
K : Set α
hC : M.IsCircuit C
he : C ∩ K = {e}
heC : e ∈ C
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃t : Set α⦄, t ⊂ K → M.Spanning (M.E \ t)
hKe : M.Spanning (M.E \ (K \ {e}))
⊢ C \ K ⊆ M.E \ K

Tactic:
exact diff_subset_diff_left hC.subset_ground

Premises used: Set.diff_subset_diff_left, Matroid.IsCircuit.subset_ground
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C : Set α
e : α
K : Set α
hC : M.IsCircuit C
he : C ∩ K = {e}
heC : e ∈ C
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃t : Set α⦄, t ⊂ K → M.Spanning (M.E \ t)
hKe : M.Spanning (M.E \ (K \ {e}))
rw : C ∩ K ⊆ M.E
⊢ {e} ⊆ M.E

Tactic:
rw [← he]
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C : Set α
e : α
K : Set α
hC : M.IsCircuit C
he : C ∩ K = {e}
heC : e ∈ C
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃t : Set α⦄, t ⊂ K → M.Spanning (M.E \ t)
hKe : M.Spanning (M.E \ (K \ {e}))
⊢ C ∩ K ⊆ M.E

Tactic:
inter_subset_left.trans hC.subset_ground

Premises used: HasSubset.Subset.trans, Set.inter_subset_left, Matroid.IsCircuit.subset_ground
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C : Set α
e : α
K : Set α
hC : M.IsCircuit C
he : C ∩ K = {e}
heC : e ∈ C
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃t : Set α⦄, t ⊂ K → M.Spanning (M.E \ t)
hKe : M.Spanning (M.E \ (K \ {e}))
⊢ C ∩ K ⊆ M.E

Tactic:
exact inter_subset_left.trans hC.subset_ground

Premises used: HasSubset.Subset.trans, Set.inter_subset_left, Matroid.IsCircuit.subset_ground
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C K : Set α
hC : M.IsCircuit C
hK : M.IsCocircuit K
hCK : (C ∩ K).Nonempty
obtain : ∀ (e : α) (heCK : e ∈ C ∩ K), (C ∩ K).Nontrivial
⊢ (C ∩ K).Nontrivial

Tactic:
obtain ⟨e, heCK⟩ := hCK
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C K : Set α
hC : M.IsCircuit C
hK : M.IsCocircuit K
e : α
heCK : e ∈ C ∩ K
rw : C ∩ K ≠ {e}
⊢ (C ∩ K).Nontrivial

Tactic:
rw [nontrivial_iff_ne_singleton heCK]

Premises used: Set.nontrivial_iff_ne_singleton
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C K : Set α
hC : M.IsCircuit C
hK : M.IsCocircuit K
e : α
heCK : e ∈ C ∩ K
⊢ C ∩ K ≠ {e}

Tactic:
hC.inter_isCocircuit_ne_singleton hK

Premises used: Matroid.IsCircuit.inter_isCocircuit_ne_singleton
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C K : Set α
hC : M.IsCircuit C
hK : M.IsCocircuit K
e : α
heCK : e ∈ C ∩ K
⊢ C ∩ K ≠ {e}

Tactic:
exact hC.inter_isCocircuit_ne_singleton hK

Premises used: Matroid.IsCircuit.inter_isCocircuit_ne_singleton
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C K : Set α
hC : M.IsCircuit C
hK : M.IsCocircuit K
rw : (C ∩ K).Nonempty → (C ∩ K).Nontrivial
⊢ Disjoint C K ∨ (C ∩ K).Nontrivial

Tactic:
rw [or_iff_not_imp_left, disjoint_iff_inter_eq_empty, ← ne_eq, ← nonempty_iff_ne_empty]

Premises used: ne_eq, Set.disjoint_iff_inter_eq_empty, Classical.or_iff_not_imp_left, Set.nonempty_iff_ne_empty
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C K : Set α
hC : M.IsCircuit C
hK : M.IsCocircuit K
⊢ (C ∩ K).Nonempty → (C ∩ K).Nontrivial

Tactic:
hC.isCocircuit_inter_nontrivial hK

Premises used: Matroid.IsCircuit.isCocircuit_inter_nontrivial
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C K : Set α
hC : M.IsCircuit C
hK : M.IsCocircuit K
⊢ (C ∩ K).Nonempty → (C ∩ K).Nontrivial

Tactic:
exact hC.isCocircuit_inter_nontrivial hK

Premises used: Matroid.IsCircuit.isCocircuit_inter_nontrivial
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
rw : (∀ (x : Set α), ¬M.IsCircuit x) ↔ ∀ C ⊆ M.E, ¬M.IsCircuit C
⊢ M✶.RankPos ↔ ∃ (C : Set α), M.IsCircuit C

Tactic:
rw [rankPos_iff, dual_isBase_iff, diff_empty, not_iff_comm, not_exists,
    ← ground_indep_iff_isBase, indep_iff_forall_subset_not_isCircuit]

Premises used: Matroid.rankPos_iff, Matroid.indep_iff_forall_subset_not_isCircuit, not_exists, Matroid.dual_isBase_iff, Set.diff_empty, Matroid.ground_indep_iff_isBase, not_iff_comm
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
⊢ (∀ (x : Set α), ¬M.IsCircuit x) ↔ ∀ C ⊆ M.E, ¬M.IsCircuit C

Tactic:
⟨fun h C _ ↦ h C, fun h C hC ↦ h C hC.subset_ground hC⟩

Premises used: Matroid.IsCircuit.subset_ground, Iff.intro
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
⊢ (∀ (x : Set α), ¬M.IsCircuit x) ↔ ∀ C ⊆ M.E, ¬M.IsCircuit C

Tactic:
exact ⟨fun h C _ ↦ h C, fun h C hC ↦ h C hC.subset_ground hC⟩
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C : Set α
hC : M.IsCircuit C
⊢ M✶.RankPos

Tactic:
dual_rankPos_iff_exists_isCircuit.mpr ⟨C, hC⟩

Premises used: Iff.mpr, Matroid.dual_rankPos_iff_exists_isCircuit, Exists.intro
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
inst : M✶.RankPos
⊢ M✶.RankPos

Tactic:
assumption
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
rw : M✶✶.RankPos ↔ ∃ (K : Set α), M✶✶.IsCocircuit K
rw₁ : (∃ (C : Set α), M✶.IsCircuit C) ↔ ∃ (K : Set α), M✶✶.IsCocircuit K
rw₂ rw₃ : (∃ (C : Set α), M✶.IsCircuit C) ↔ ∃ (K : Set α), M.IsCocircuit K
⊢ M.RankPos ↔ ∃ (K : Set α), M.IsCocircuit K

Tactic:
rw [← dual_dual M, dual_rankPos_iff_exists_isCircuit, dual_dual M]

Premises used: Matroid.dual_rankPos_iff_exists_isCircuit, Matroid.dual_dual
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
e : α
B : Set α
he : e ∈ B
hB : M.IsBase B
⊢ e ∉ M.E \ B

Tactic:
simp [he]
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
e : α
B : Set α
he : e ∈ B
hB : M.IsBase B
apply : e ∈ M✶.closure (M.E \ B)
⊢ M.IsCocircuit (M.fundCocircuit e B)

Tactic:
apply hB.compl_isBase_dual.indep.fundCircuit_isCircuit _ (by simp [he])

Premises used: Matroid.IsBase.compl_isBase_dual, Matroid.IsBase.indep, Matroid.Indep.fundCircuit_isCircuit
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
e : α
B : Set α
he : e ∈ B
hB : M.IsBase B
rw : e ∈ M.E
⊢ e ∈ M✶.closure (M.E \ B)

Tactic:
rw [hB.compl_isBase_dual.closure_eq, dual_ground]

Premises used: Matroid.IsBase.closure_eq, Matroid.IsBase.compl_isBase_dual, Matroid.dual_ground
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
e : α
B : Set α
he : e ∈ B
hB : M.IsBase B
⊢ e ∈ M.E

Tactic:
hB.subset_ground he

Premises used: Matroid.IsBase.subset_ground
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
e : α
B : Set α
he : e ∈ B
hB : M.IsBase B
⊢ e ∈ M.E

Tactic:
exact hB.subset_ground he

Premises used: Matroid.IsBase.subset_ground
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
e : α
B : Set α
⊢ e ∈ M.fundCocircuit e B

Tactic:
mem_insert _ _

Premises used: Set.Mem, Matroid.fundCocircuit, Set.mem_insert, Matroid.fundCircuit
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
e : α
B : Set α
⊢ M.fundCocircuit e B ⊆ insert e (M.E \ B)

Tactic:
fundCircuit_subset_insert ..

Premises used: Matroid.fundCocircuit, Maximal, Matroid.fundCircuit_subset_insert
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
e : α
M : Matroid α
B : Set α
he : e ∈ B
⊢ M.fundCocircuit e B ∩ B = {e}

Tactic:
subset_antisymm ?_ (singleton_subset_iff.2 ⟨M.mem_fundCocircuit _ _, he⟩)

Premises used: Iff.mpr, Set.singleton_subset_iff, subset_antisymm, Matroid.mem_fundCocircuit, And.intro
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
e : α
M : Matroid α
B : Set α
he : e ∈ B
refine : M.fundCocircuit e B ∩ B ⊆ {e}
⊢ M.fundCocircuit e B ∩ B = {e}

Tactic:
refine subset_antisymm ?_ (singleton_subset_iff.2 ⟨M.mem_fundCocircuit _ _, he⟩)
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
e : α
M : Matroid α
B : Set α
he : e ∈ B
⊢ M.fundCocircuit e B ∩ B ⊆ {e}

Tactic:
(inter_subset_inter_left _ (M.fundCocircuit_subset_insert_compl _ _)).trans ?_

Premises used: Matroid.fundCocircuit_subset_insert_compl, HasSubset.Subset.trans, Set.inter_subset_inter_left