awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
e : α
M : Matroid α
B : Set α
he : e ∈ B
refine : insert e (M.E \ B) ∩ B ⊆ {e}
⊢ M.fundCocircuit e B ∩ B ⊆ {e}

Tactic:
refine (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
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
e : α
M : Matroid α
B : Set α
he : e ∈ B
⊢ insert e (M.E \ B) ∩ B ⊆ {e}

Tactic:
simp +contextual
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
e : α
X : Set α
he : e ∉ M.E
rwa : M✶.fundCircuit e (M✶.E \ X) = {e}
rwa₁ : Eq (α := Set α) {e} {e}
rwa₂ : e ∉ M✶.E
rwa₃ : Eq (α := Set α) {e} {e}
rwa₄ rwa₅ rwa₆ : e ∉ M✶.E
⊢ M.fundCocircuit e X = {e}

Tactic:
rwa [fundCocircuit, fundCircuit_eq_of_notMem_ground]

Premises used: Matroid.fundCocircuit, Matroid.fundCircuit_eq_of_notMem_ground
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
X : Set α
e : α
M : Matroid α
heX : e ∉ X
pos : ∀ (he : e ∈ M.E), M.fundCocircuit e X = {e}
neg : ∀ (he : e ∉ M.E), M.fundCocircuit e X = {e}
⊢ M.fundCocircuit e X = {e}

Tactic:
by_cases he : e ∈ M.E

Premises used: Matroid.E
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
X : Set α
e : α
M : Matroid α
heX : e ∉ X
he : e ∈ M.E
pos : e ∈ M✶.E \ X
⊢ M.fundCocircuit e X = {e}

Tactic:
rw [fundCocircuit, fundCircuit_eq_of_mem]

Premises used: Matroid.fundCocircuit, Matroid.fundCircuit_eq_of_mem
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
X : Set α
e : α
M : Matroid α
heX : e ∉ X
he : e ∈ M.E
⊢ e ∈ M✶.E \ X

Tactic:
⟨he, heX⟩

Premises used: Set.Mem, Set.diff, setOf, And.intro
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
X : Set α
e : α
M : Matroid α
heX : e ∉ X
he : e ∈ M.E
⊢ e ∈ M✶.E \ X

Tactic:
exact ⟨he, heX⟩
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
X : Set α
e : α
M : Matroid α
heX : e ∉ X
he : e ∉ M.E
neg neg₁ : Eq (α := Set α) {e} {e}
⊢ M.fundCocircuit e X = {e}

Tactic:
rw [fundCocircuit_eq_of_notMem_ground _ he]

Premises used: Matroid.fundCocircuit_eq_of_notMem_ground
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
heI : e ∈ I
obtain : ∀ (B : Set α) (hB : M.IsBase B) (hIB : I ⊆ B), ∃ (K : Set α), M.IsCocircuit K ∧ K ∩ I = {e}
⊢ ∃ (K : Set α), M.IsCocircuit K ∧ K ∩ I = {e}

Tactic:
obtain ⟨B, hB, hIB⟩ := hI.exists_isBase_superset

Premises used: Matroid.Indep.exists_isBase_superset
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
heI : e ∈ I
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
⊢ ∃ (K : Set α), M.IsCocircuit K ∧ K ∩ I = {e}

Tactic:
⟨M.fundCocircuit e B, fundCocircuit_isCocircuit (hIB heI) hB, ?_⟩

Premises used: Matroid.fundCocircuit, And.intro, Exists.intro, Matroid.fundCocircuit_isCocircuit
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
heI : e ∈ I
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
refine : M.fundCocircuit e B ∩ I = {e}
⊢ ∃ (K : Set α), M.IsCocircuit K ∧ K ∩ I = {e}

Tactic:
refine ⟨M.fundCocircuit e B, fundCocircuit_isCocircuit (hIB heI) hB, ?_⟩
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
heI : e ∈ I
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
rw : M.fundCocircuit e B ∩ I ⊆ M.fundCocircuit e B ∩ B
⊢ M.fundCocircuit e B ∩ I = {e}

Tactic:
rw [subset_antisymm_iff, subset_inter_iff, singleton_subset_iff, and_iff_right
    (mem_fundCocircuit _ _ _), singleton_subset_iff, and_iff_left heI,
    ← M.fundCocircuit_inter_eq (hIB heI)]

Premises used: Set.singleton_subset_iff, Set.subset_inter_iff, and_iff_left, and_iff_right, Matroid.mem_fundCocircuit, subset_antisymm_iff, Matroid.fundCocircuit_inter_eq
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
heI : e ∈ I
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
⊢ M.fundCocircuit e B ∩ I ⊆ M.fundCocircuit e B ∩ B

Tactic:
inter_subset_inter_right _ hIB

Premises used: Set.inter_subset_inter_right
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
heI : e ∈ I
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
⊢ M.fundCocircuit e B ∩ I ⊆ M.fundCocircuit e B ∩ B

Tactic:
exact inter_subset_inter_right _ hIB

Premises used: Set.inter_subset_inter_right
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
aux : ∀ {N : Matroid α} {B' : Set α} (hB' : N.IsBase B') {e f : α}, e ∈ N.fundCocircuit f B' → f ∈ N.fundCircuit e B'
h : f ∈ M.fundCircuit e B
⊢ f ∈ M✶.fundCocircuit e (M.E \ B)

Tactic:
simpa [fundCocircuit, inter_eq_self_of_subset_right hB.subset_ground]

Premises used: Matroid.IsBase.subset_ground, Matroid.fundCocircuit, Set.inter_eq_self_of_subset_right
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
suffices :
  ∀ {N : Matroid α} {B' : Set α} (hB' : N.IsBase B') {e f : α}, e ∈ N.fundCocircuit f B' → f ∈ N.fundCircuit e B'
⊢ e ∈ M.fundCocircuit f B ↔ f ∈ M.fundCircuit e B

Tactic:
suffices aux : ∀ {N : Matroid α} {B' : Set α} (hB' : N.IsBase B') {e f},
      e ∈ N.fundCocircuit f B' → f ∈ N.fundCircuit e B' from
    ⟨fun h ↦ aux hB h, fun h ↦ aux hB.compl_isBase_dual <| by
      simpa [fundCocircuit, inter_eq_self_of_subset_right hB.subset_ground]⟩
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : e ∈ M.fundCocircuit f B
inl : ∀ (he : e ∈ M.fundCocircuit e B), e ∈ M.fundCircuit e B
inr : ∀ (hne : e ≠ f), f ∈ M.fundCircuit e B
⊢ f ∈ M.fundCircuit e B

Tactic:
obtain rfl | hne := eq_or_ne e f

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e : α
he : e ∈ M.fundCocircuit e B
⊢ e ∈ M.fundCircuit e B

Tactic:
simp [mem_fundCircuit]

Premises used: Matroid.mem_fundCircuit
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : e ∈ M.fundCocircuit f B
hne : e ≠ f
⊢ M✶.IsBase (M✶.E \ B)

Tactic:
have hB' : M✶.IsBase (M✶.E \ B) := hB.compl_isBase_dual
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : e ∈ M.fundCocircuit f B
hne : e ≠ f
hB' : M✶.IsBase (M✶.E \ B)
inr : ∀ (hfE : f ∉ M.E), f ∈ M.fundCircuit e B
inr₁ : ∀ (hfE : f ∈ M.E), f ∈ M.fundCircuit e B
⊢ f ∈ M.fundCircuit e B

Tactic:
obtain hfE | hfE := em' <| f ∈ M.E

Premises used: Matroid.E, em'
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : e ∈ M✶.fundCircuit f (M✶.E \ B)
hne : e ≠ f
hB' : M✶.IsBase (M✶.E \ B)
hfE : f ∉ M.E
⊢ f ∉ M✶.E

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : e ∈ M.fundCocircuit f B
hne : e ≠ f
hB' : M✶.IsBase (M✶.E \ B)
hfE : f ∉ M.E
⊢ Membership.mem (γ := Set α) {f} e

Tactic:
rw [fundCocircuit, fundCircuit_eq_of_notMem_ground (by simpa)] at he

Premises used: Matroid.fundCocircuit, Matroid.fundCircuit_eq_of_notMem_ground
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : e ∈ M.fundCocircuit f B
hne : e ≠ f
hB' : M✶.IsBase (M✶.E \ B)
hfE : f ∉ M.E
he₁ : Membership.mem (γ := Set α) {f} e
⊢ e ≠ f

Tactic:
rw [fundCocircuit, fundCircuit_eq_of_notMem_ground (by simpa)] at he

Premises used: Matroid.fundCocircuit, Matroid.fundCircuit_eq_of_notMem_ground
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : e ∈ M.fundCocircuit f B
hne : e ≠ f
hB' : M✶.IsBase (M✶.E \ B)
hfE : f ∉ M.E
he₁ : Membership.mem (γ := Set α) {f} e
hne₁ : e ≠ f
⊢ M✶.IsBase (M✶.E \ B)

Tactic:
rw [fundCocircuit, fundCircuit_eq_of_notMem_ground (by simpa)] at he

Premises used: Matroid.fundCocircuit, Matroid.fundCircuit_eq_of_notMem_ground
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : e ∈ M.fundCocircuit f B
hne : e ≠ f
hB' : M✶.IsBase (M✶.E \ B)
hfE : f ∉ M.E
he₁ : Membership.mem (γ := Set α) {f} e
hne₁ : e ≠ f
hB'₁ : M✶.IsBase (M✶.E \ B)
⊢ f ∉ M.E

Tactic:
rw [fundCocircuit, fundCircuit_eq_of_notMem_ground (by simpa)] at he

Premises used: Matroid.fundCocircuit, Matroid.fundCircuit_eq_of_notMem_ground
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : Membership.mem (γ := Set α) {f} e
hne : e ≠ f
hB' : M✶.IsBase (M✶.E \ B)
hfE : f ∉ M.E
⊢ f ∈ M.fundCircuit e B

Tactic:
contradiction
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : e ∈ M.fundCocircuit f B
hne : e ≠ f
hB' : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
inr : ∀ (hfB : f ∉ B), f ∈ M.fundCircuit e B
inr₁ : ∀ (hfB : f ∈ B), f ∈ M.fundCircuit e B
⊢ f ∈ M.fundCircuit e B

Tactic:
obtain hfB | hfB := em' <| f ∈ B

Premises used: em'
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : e ∈ M✶.fundCircuit f (M✶.E \ B)
hne : e ≠ f
hB' : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
hfB : f ∉ B
⊢ f ∈ M✶.E \ B

Tactic:
simp [hfE, hfB]
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : e ∈ M.fundCocircuit f B
hne : e ≠ f
hB' : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
hfB : f ∉ B
⊢ Membership.mem (γ := Set α) {f} e

Tactic:
rw [fundCocircuit, fundCircuit_eq_of_mem (by simp [hfE, hfB])] at he

Premises used: Matroid.fundCocircuit, Matroid.fundCircuit_eq_of_mem
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : e ∈ M.fundCocircuit f B
hne : e ≠ f
hB' : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
hfB : f ∉ B
he₁ : Membership.mem (γ := Set α) {f} e
⊢ e ≠ f

Tactic:
rw [fundCocircuit, fundCircuit_eq_of_mem (by simp [hfE, hfB])] at he

Premises used: Matroid.fundCocircuit, Matroid.fundCircuit_eq_of_mem
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : e ∈ M.fundCocircuit f B
hne : e ≠ f
hB' : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
hfB : f ∉ B
he₁ : Membership.mem (γ := Set α) {f} e
hne₁ : e ≠ f
⊢ M✶.IsBase (M✶.E \ B)

Tactic:
rw [fundCocircuit, fundCircuit_eq_of_mem (by simp [hfE, hfB])] at he

Premises used: Matroid.fundCocircuit, Matroid.fundCircuit_eq_of_mem
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : e ∈ M.fundCocircuit f B
hne : e ≠ f
hB' : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
hfB : f ∉ B
he₁ : Membership.mem (γ := Set α) {f} e
hne₁ : e ≠ f
hB'₁ : M✶.IsBase (M✶.E \ B)
⊢ f ∈ M.E

Tactic:
rw [fundCocircuit, fundCircuit_eq_of_mem (by simp [hfE, hfB])] at he

Premises used: Matroid.fundCocircuit, Matroid.fundCircuit_eq_of_mem
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : e ∈ M.fundCocircuit f B
hne : e ≠ f
hB' : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
hfB : f ∉ B
he₁ : Membership.mem (γ := Set α) {f} e
hne₁ : e ≠ f
hB'₁ : M✶.IsBase (M✶.E \ B)
hfE₁ : f ∈ M.E
⊢ f ∉ B

Tactic:
rw [fundCocircuit, fundCircuit_eq_of_mem (by simp [hfE, hfB])] at he

Premises used: Matroid.fundCocircuit, Matroid.fundCircuit_eq_of_mem
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : Membership.mem (γ := Set α) {f} e
hne : e ≠ f
hB' : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
hfB : f ∉ B
⊢ f ∈ M.fundCircuit e B

Tactic:
contradiction
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : e ∈ M.fundCocircuit f B
hne : e ≠ f
hB' : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
hfB : f ∈ B
⊢ e ∈ M.E \ B

Tactic:
simpa [hne] using (M.fundCocircuit_subset_insert_compl f B) he

Premises used: Matroid.fundCocircuit_subset_insert_compl
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : e ∈ M.fundCocircuit f B
hne : e ≠ f
hB' : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
hfB : f ∈ B
⊢ e ∈ M.E

Tactic:
obtain ⟨heE, heB⟩ : e ∈ M.E \ B := by
    simpa [hne] using (M.fundCocircuit_subset_insert_compl f B) he

Premises used: Matroid.E
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : e ∈ M.fundCocircuit f B
hne : e ≠ f
hB' : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
hfB : f ∈ B
heE : e ∈ M.E
⊢ e ∉ B

Tactic:
obtain ⟨heE, heB⟩ : e ∈ M.E \ B := by
    simpa [hne] using (M.fundCocircuit_subset_insert_compl f B) he

Premises used: Matroid.E
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : e ∈ M✶.fundCircuit f (M✶.E \ B)
hne : e ≠ f
hB' : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
hfB : f ∈ B
heE : e ∈ M.E
heB : e ∉ B
rwa rwa₁ rwa₂ rwa₃ : f ∈ M✶.E
⊢ f ∈ M✶.closure (M✶.E \ B)

Tactic:
rwa [hB'.closure_eq]

Premises used: Matroid.IsBase.closure_eq
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : e ∈ M✶.fundCircuit f (M✶.E \ B)
hne : e ≠ f
hB' : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
hfB : f ∈ B
heE : e ∈ M.E
heB : e ∉ B
⊢ f ∉ M✶.E \ B

Tactic:
simp [hfB]
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : e ∈ M.fundCocircuit f B
hne : e ≠ f
hB' : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
hfB : f ∈ B
heE : e ∈ M.E
heB : e ∉ B
⊢ M✶.Indep (insert f (M✶.E \ B) \ {e})

Tactic:
rw [fundCocircuit, hB'.indep.mem_fundCircuit_iff (by rwa [hB'.closure_eq]) (by simp [hfB])] at he

Premises used: Matroid.Indep.mem_fundCircuit_iff, Matroid.fundCocircuit, Matroid.IsBase.indep
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : e ∈ M.fundCocircuit f B
hne : e ≠ f
hB' : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
hfB : f ∈ B
heE : e ∈ M.E
heB : e ∉ B
he₁ : M✶.Indep (insert f (M✶.E \ B) \ {e})
⊢ e ≠ f

Tactic:
rw [fundCocircuit, hB'.indep.mem_fundCircuit_iff (by rwa [hB'.closure_eq]) (by simp [hfB])] at he

Premises used: Matroid.Indep.mem_fundCircuit_iff, Matroid.fundCocircuit, Matroid.IsBase.indep
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : e ∈ M.fundCocircuit f B
hne : e ≠ f
hB' : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
hfB : f ∈ B
heE : e ∈ M.E
heB : e ∉ B
he₁ : M✶.Indep (insert f (M✶.E \ B) \ {e})
hne₁ : e ≠ f
⊢ M✶.IsBase (M✶.E \ B)

Tactic:
rw [fundCocircuit, hB'.indep.mem_fundCircuit_iff (by rwa [hB'.closure_eq]) (by simp [hfB])] at he

Premises used: Matroid.Indep.mem_fundCircuit_iff, Matroid.fundCocircuit, Matroid.IsBase.indep
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : e ∈ M.fundCocircuit f B
hne : e ≠ f
hB' : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
hfB : f ∈ B
heE : e ∈ M.E
heB : e ∉ B
he₁ : M✶.Indep (insert f (M✶.E \ B) \ {e})
hne₁ : e ≠ f
hB'₁ : M✶.IsBase (M✶.E \ B)
⊢ f ∈ M.E

Tactic:
rw [fundCocircuit, hB'.indep.mem_fundCircuit_iff (by rwa [hB'.closure_eq]) (by simp [hfB])] at he

Premises used: Matroid.Indep.mem_fundCircuit_iff, Matroid.fundCocircuit, Matroid.IsBase.indep
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : e ∈ M.fundCocircuit f B
hne : e ≠ f
hB' : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
hfB : f ∈ B
heE : e ∈ M.E
heB : e ∉ B
he₁ : M✶.Indep (insert f (M✶.E \ B) \ {e})
hne₁ : e ≠ f
hB'₁ : M✶.IsBase (M✶.E \ B)
hfE₁ : f ∈ M.E
⊢ f ∈ B

Tactic:
rw [fundCocircuit, hB'.indep.mem_fundCircuit_iff (by rwa [hB'.closure_eq]) (by simp [hfB])] at he

Premises used: Matroid.Indep.mem_fundCircuit_iff, Matroid.fundCocircuit, Matroid.IsBase.indep
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : e ∈ M.fundCocircuit f B
hne : e ≠ f
hB' : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
hfB : f ∈ B
heE : e ∈ M.E
heB : e ∉ B
he₁ : M✶.Indep (insert f (M✶.E \ B) \ {e})
hne₁ : e ≠ f
hB'₁ : M✶.IsBase (M✶.E \ B)
hfE₁ : f ∈ M.E
hfB₁ : f ∈ B
⊢ e ∈ M.E

Tactic:
rw [fundCocircuit, hB'.indep.mem_fundCircuit_iff (by rwa [hB'.closure_eq]) (by simp [hfB])] at he

Premises used: Matroid.Indep.mem_fundCircuit_iff, Matroid.fundCocircuit, Matroid.IsBase.indep
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : e ∈ M.fundCocircuit f B
hne : e ≠ f
hB' : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
hfB : f ∈ B
heE : e ∈ M.E
heB : e ∉ B
he₁ : M✶.Indep (insert f (M✶.E \ B) \ {e})
hne₁ : e ≠ f
hB'₁ : M✶.IsBase (M✶.E \ B)
hfE₁ : f ∈ M.E
hfB₁ : f ∈ B
heE₁ : e ∈ M.E
⊢ e ∉ B

Tactic:
rw [fundCocircuit, hB'.indep.mem_fundCircuit_iff (by rwa [hB'.closure_eq]) (by simp [hfB])] at he

Premises used: Matroid.Indep.mem_fundCircuit_iff, Matroid.fundCocircuit, Matroid.IsBase.indep
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : M✶.Indep (insert f (M✶.E \ B) \ {e})
hne : e ≠ f
hB' : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
hfB : f ∈ B
heE : e ∈ M.E
heB : e ∉ B
rwa rwa₁ rwa₂ rwa₃ : e ∈ M.E
⊢ e ∈ 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 α
B : Set α
hB : M.IsBase B
e f : α
he : M✶.Indep (insert f (M✶.E \ B) \ {e})
hne : e ≠ f
hB' : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
hfB : f ∈ B
heE : e ∈ M.E
heB : e ∉ B
inr : M.Indep (insert e B \ {f})
⊢ f ∈ M.fundCircuit e B

Tactic:
rw [hB.indep.mem_fundCircuit_iff (by rwa [hB.closure_eq]) heB]

Premises used: Matroid.Indep.mem_fundCircuit_iff, Matroid.IsBase.indep
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : M✶.Indep (insert f (M✶.E \ B) \ {e})
hne : e ≠ f
hB' : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
hfB : f ∈ B
heE : e ∈ M.E
heB : e ∉ B
⊢ f ∉ M✶.E \ B

Tactic:
simp [hfE, hfB]
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : M✶.Indep (insert f (M✶.E \ B) \ {e})
hne : e ≠ f
hB' : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
hfB : f ∈ B
heE : e ∈ M.E
heB : e ∉ B
⊢ M.IsBase (M.E \ (insert f (M✶.E \ B) \ {e}))

Tactic:
have hB' : M.IsBase (M.E \ (insert f (M✶.E \ B) \ {e})) :=
    (hB'.exchange_isBase_of_indep' ⟨heE, heB⟩ (by simp [hfE, hfB]) he).compl_isBase_of_dual
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : M✶.Indep (insert f (M✶.E \ B) \ {e})
hne : e ≠ f
hB'_1 : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
hfB : f ∈ B
heE : e ∈ M.E
heB : e ∉ B
hB' : M.IsBase (M.E \ (insert f (M✶.E \ B) \ {e}))
⊢ M.Indep (insert e B \ {f})

Tactic:
hB'.indep.subset ?_

Premises used: Matroid.Indep.subset, Matroid.IsBase.indep
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : M✶.Indep (insert f (M✶.E \ B) \ {e})
hne : e ≠ f
hB'_1 : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
hfB : f ∈ B
heE : e ∈ M.E
heB : e ∉ B
hB' : M.IsBase (M.E \ (insert f (M✶.E \ B) \ {e}))
inr : insert e B \ {f} ⊆ M.E \ (insert f (M✶.E \ B) \ {e})
⊢ M.Indep (insert e B \ {f})

Tactic:
refine hB'.indep.subset ?_

Premises used: Matroid.Indep.subset, Matroid.IsBase.indep
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : M✶.Indep (insert f (M✶.E \ B) \ {e})
hne : e ≠ f
hB'_1 : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
hfB : f ∈ B
heE : e ∈ M.E
heB : e ∉ B
hB' : M.IsBase (M.E \ (insert f (M✶.E \ B) \ {e}))
inr : insert e B ⊆ insert f (M.E \ (insert f (M.E \ B) \ {e}))
⊢ insert e B \ {f} ⊆ M.E \ (insert f (M✶.E \ B) \ {e})

Tactic:
simp only [dual_ground, diff_singleton_subset_iff]

Premises used: Set.diff_singleton_subset_iff, Matroid.dual_ground
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : M✶.Indep (insert f (M✶.E \ B) \ {e})
hne : e ≠ f
hB'_1 : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
hfB : f ∈ B
heE : e ∈ M.E
heB : e ∉ B
hB' : M.IsBase (M.E \ (insert f (M✶.E \ B) \ {e}))
⊢ {e} ⊆ M.E

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : M✶.Indep (insert f (M✶.E \ B) \ {e})
hne : e ≠ f
hB'_1 : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
hfB : f ∈ B
heE : e ∈ M.E
heB : e ∉ B
hB' : M.IsBase (M.E \ (insert f (M✶.E \ B) \ {e}))
inr : insert e B ⊆ insert e (insert f (B \ {f}))
⊢ insert e B ⊆ insert f (M.E \ (insert f (M.E \ B) \ {e}))

Tactic:
rw [diff_diff_right, inter_eq_self_of_subset_right (by simpa), union_singleton, insert_comm,
    ← union_singleton (s := M.E \ B), ← diff_diff, diff_diff_cancel_left hB.subset_ground]

Premises used: Matroid.IsBase.subset_ground, Set.insert_comm, Set.diff_diff, Set.inter_eq_self_of_subset_right, Set.diff_diff_cancel_left, Set.union_singleton, Set.diff_diff_right
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : M✶.Indep (insert f (M✶.E \ B) \ {e})
hne : e ≠ f
hB'_1 : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
hfB : f ∈ B
heE : e ∈ M.E
heB : e ∉ B
hB' : M.IsBase (M.E \ (insert f (M✶.E \ B) \ {e}))
⊢ insert e B ⊆ insert e (insert f (B \ {f}))

Tactic:
simp [hfB]
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
⊢ M.IsFlat M.E

Tactic:
⟨fun _ _ _ ↦ IsBasis.subset_ground, Subset.rfl⟩

Premises used: Matroid.IsBasis.subset_ground, Matroid.IsFlat.mk, Set.Subset.rfl
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
ι : Type u_3
inst : Nonempty ι
Fs : ι → Set α
hFs : ∀ (i : ι), M.IsFlat (Fs i)
⊢ M.IsFlat (⋂ (i : ι), Fs i)

Tactic:
⟨fun I X hI hIX ↦ subset_iInter fun i ↦ ?_,
    (iInter_subset _ (Classical.arbitrary _)).trans (hFs _).subset_ground⟩

Premises used: Matroid.IsFlat.mk, Set.subset_iInter, HasSubset.Subset.trans, Classical.arbitrary, Set.iInter_subset, Matroid.IsFlat.subset_ground
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
ι : Type u_3
inst : Nonempty ι
Fs : ι → Set α
hFs : ∀ (i : ι), M.IsFlat (Fs i)
refine : ∀ (I X : Set α) (hI : M.IsBasis I (⋂ (i : ι), Fs i)) (hIX : M.IsBasis I X) (i : ι), X ⊆ Fs i
⊢ M.IsFlat (⋂ (i : ι), Fs i)

Tactic:
refine ⟨fun I X hI hIX ↦ subset_iInter fun i ↦ ?_,
    (iInter_subset _ (Classical.arbitrary _)).trans (hFs _).subset_ground⟩
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
ι : Type u_3
inst : Nonempty ι
Fs : ι → Set α
hFs : ∀ (i : ι), M.IsFlat (Fs i)
I X : Set α
hI : M.IsBasis I (⋂ (i : ι), Fs i)
hIX : M.IsBasis I X
i : ι
obtain : ∀ (J : Set α) (hIJ : M.IsBasis J (Fs i)) (hJ : I ⊆ J), X ⊆ Fs i
⊢ X ⊆ Fs i

Tactic:
obtain ⟨J, hIJ, hJ⟩ := hI.indep.subset_isBasis_of_subset (hI.subset.trans (iInter_subset _ i))

Premises used: HasSubset.Subset.trans, Matroid.IsBasis.subset, Set.iInter_subset, Matroid.IsBasis.indep, Matroid.Indep.subset_isBasis_of_subset
-- Module: Mathlib.Combinatorics.Matroid.Closure
Goal:
α : Type u_2
M : Matroid α
ι : Type u_3
inst : Nonempty ι
Fs : ι → Set α
hFs : ∀ (i : ι), M.IsFlat (Fs i)
I X : Set α
hI : M.IsBasis I (⋂ (i : ι), Fs i)
hIX : M.IsBasis I X
i : ι
J : Set α
hIJ : M.IsBasis J (Fs i)
hJ : I ⊆ J
⊢ X ⊆ Fs i

Tactic:
subset_union_right.trans ((hFs i).1 (X := Fs i ∪ X) hIJ ?_)

Premises used: Set.subset_union_right, HasSubset.Subset.trans, Matroid.IsFlat.subset_of_isBasis_of_isBasis