awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
e f : α
C₁ C₂ : Set α
hC₁ : M.IsCircuit C₁
hC₂ : M.IsCircuit C₂
heC₁ : e ∈ C₁
heC₂ : e ∈ C₂
hfC₁ : f ∈ C₁
hfC₂ : f ∉ C₂
⊢ ∀ (i : Unit), M.IsCircuit ((fun (x : Unit) ↦ C₂) i)

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
e f : α
C₁ C₂ : Set α
hC₁ : M.IsCircuit C₁
hC₂ : M.IsCircuit C₂
heC₁ : e ∈ C₁
heC₂ : e ∈ C₂
hfC₁ : f ∈ C₁
hfC₂ : f ∉ C₂
⊢ ∀ (i : Unit), (fun (i : Unit) ↦ e) i ∈ C₁

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
e f : α
C₁ C₂ : Set α
hC₁ : M.IsCircuit C₁
hC₂ : M.IsCircuit C₂
heC₁ : e ∈ C₁
heC₂ : e ∈ C₂
hfC₁ : f ∈ C₁
hfC₂ : f ∉ C₂
⊢ ∀ (i : Unit), Membership.mem (γ := Set α) ((fun (x : Unit) ↦ C₂) i) ((fun (i : Unit) ↦ e) i)

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
e f : α
C₁ C₂ : Set α
hC₁ : M.IsCircuit C₁
hC₂ : M.IsCircuit C₂
heC₁ : e ∈ C₁
heC₂ : e ∈ C₂
hfC₁ : f ∈ C₁
hfC₂ : f ∉ C₂
⊢ ∀ ⦃i i' : Unit⦄, Membership.mem (γ := Set α) ((fun (x : Unit) ↦ C₂) i') ((fun (i : Unit) ↦ e) i) → i = i'

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
e f : α
C₁ C₂ : Set α
hC₁ : M.IsCircuit C₁
hC₂ : M.IsCircuit C₂
heC₁ : e ∈ C₁
heC₂ : e ∈ C₂
hfC₁ : f ∈ C₁
hfC₂ : f ∉ C₂
⊢ f ∈ C₁

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
e f : α
C₁ C₂ : Set α
hC₁ : M.IsCircuit C₁
hC₂ : M.IsCircuit C₂
heC₁ : e ∈ C₁
heC₂ : e ∈ C₂
hfC₁ : f ∈ C₁
hfC₂ : f ∉ C₂
⊢ ∀ (i : Unit), f ∉ (fun (x : Unit) ↦ C₂) i

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
e f : α
C₁ C₂ : Set α
hC₁ : M.IsCircuit C₁
hC₂ : M.IsCircuit C₂
heC₁ : e ∈ C₁
heC₂ : e ∈ C₂
hfC₁ : f ∈ C₁
hfC₂ : f ∉ C₂
obtain :
  ∀ (C : Set α) (hCs : C ⊆ (C₁ ∪ ⋃ (i : Unit), C₂) \ range fun (i : Unit) ↦ e) (hC : M.IsCircuit C) (hfC : f ∈ C),
    ∃ C ⊆ (C₁ ∪ C₂) \ {e}, M.IsCircuit C ∧ f ∈ C
⊢ ∃ C ⊆ (C₁ ∪ C₂) \ {e}, M.IsCircuit C ∧ f ∈ C

Tactic:
obtain ⟨C, hCs, hC, hfC⟩ := hC₁.strong_multi_elimination (fun i : Unit ↦ e) (fun _ ↦ C₂) f
    (by simpa) (by simpa) (by simpa) (by simp) (by simpa) (by simpa)

Premises used: Matroid.IsCircuit.strong_multi_elimination
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
e f : α
C₁ C₂ : Set α
hC₁ : M.IsCircuit C₁
hC₂ : M.IsCircuit C₂
heC₁ : e ∈ C₁
heC₂ : e ∈ C₂
hfC₁ : f ∈ C₁
hfC₂ : f ∉ C₂
C : Set α
hCs : C ⊆ (C₁ ∪ ⋃ (i : Unit), C₂) \ range fun (i : Unit) ↦ e
hC : M.IsCircuit C
hfC : f ∈ C
⊢ C₁ ∪ ⋃ (i : Unit), C₂ ⊆ C₁ ∪ C₂

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
e f : α
C₁ C₂ : Set α
hC₁ : M.IsCircuit C₁
hC₂ : M.IsCircuit C₂
heC₁ : e ∈ C₁
heC₂ : e ∈ C₂
hfC₁ : f ∈ C₁
hfC₂ : f ∉ C₂
C : Set α
hCs : C ⊆ (C₁ ∪ ⋃ (i : Unit), C₂) \ range fun (i : Unit) ↦ e
hC : M.IsCircuit C
hfC : f ∈ C
⊢ Subset (α := Set α) {e} (range fun (i : Unit) ↦ e)

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
e f : α
C₁ C₂ : Set α
hC₁ : M.IsCircuit C₁
hC₂ : M.IsCircuit C₂
heC₁ : e ∈ C₁
heC₂ : e ∈ C₂
hfC₁ : f ∈ C₁
hfC₂ : f ∉ C₂
C : Set α
hCs : C ⊆ (C₁ ∪ ⋃ (i : Unit), C₂) \ range fun (i : Unit) ↦ e
hC : M.IsCircuit C
hfC : f ∈ C
⊢ ∃ C ⊆ (C₁ ∪ C₂) \ {e}, M.IsCircuit C ∧ f ∈ C

Tactic:
exact ⟨C, hCs.trans (diff_subset_diff (by simp) (by simp)), hC, hfC⟩
-- 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₂
e : α
⊢ ¬C₁ ⊆ C₂

Tactic:
have hnss : ¬ (C₁ ⊆ C₂) := fun hss ↦ h <| hC₁.eq_of_subset_isCircuit hC₂ hss
-- 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₂
e : α
hnss : ¬C₁ ⊆ C₂
obtain : ∀ (f : α) (hf₁ : f ∈ C₁) (hf₂ : f ∉ C₂), ∃ C ⊆ (C₁ ∪ C₂) \ {e}, M.IsCircuit C
⊢ ∃ C ⊆ (C₁ ∪ C₂) \ {e}, M.IsCircuit C

Tactic:
obtain ⟨f, hf₁, hf₂⟩ := not_subset.1 hnss

Premises used: Set.not_subset, Iff.mp
-- 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₂
e : α
hnss : ¬C₁ ⊆ C₂
f : α
hf₁ : f ∈ C₁
hf₂ : f ∉ C₂
pos : ∀ (he₁ : e ∈ C₁), ∃ C ⊆ (C₁ ∪ C₂) \ {e}, M.IsCircuit C
neg : ∀ (he₁ : e ∉ C₁), ∃ C ⊆ (C₁ ∪ C₂) \ {e}, M.IsCircuit C
⊢ ∃ C ⊆ (C₁ ∪ C₂) \ {e}, M.IsCircuit C

Tactic:
by_cases he₁ : e ∈ C₁
-- 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₂
e : α
hnss : ¬C₁ ⊆ C₂
f : α
hf₁ : f ∈ C₁
hf₂ : f ∉ C₂
he₁ : e ∈ C₁
pos : ∀ (he₂ : e ∈ C₂), ∃ C ⊆ (C₁ ∪ C₂) \ {e}, M.IsCircuit C
neg : ∀ (he₂ : e ∉ C₂), ∃ C ⊆ (C₁ ∪ C₂) \ {e}, M.IsCircuit C
⊢ ∃ C ⊆ (C₁ ∪ C₂) \ {e}, M.IsCircuit C

Tactic:
by_cases he₂ : e ∈ C₂
-- 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₂
e : α
hnss : ¬C₁ ⊆ C₂
f : α
hf₁ : f ∈ C₁
hf₂ : f ∉ C₂
he₁ : e ∈ C₁
he₂ : e ∈ C₂
pos : ∀ (C : Set α) (hC : C ⊆ (C₁ ∪ C₂) \ {e}) (hC' : M.IsCircuit C), ∃ C ⊆ (C₁ ∪ C₂) \ {e}, M.IsCircuit C
⊢ ∃ C ⊆ (C₁ ∪ C₂) \ {e}, M.IsCircuit C

Tactic:
obtain ⟨C, hC, hC', -⟩ := hC₁.strong_elimination hC₂ he₁ he₂ hf₁ hf₂

Premises used: Matroid.IsCircuit.strong_elimination
-- 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₂
e : α
hnss : ¬C₁ ⊆ C₂
f : α
hf₁ : f ∈ C₁
hf₂ : f ∉ C₂
he₁ : e ∈ C₁
he₂ : e ∈ C₂
C : Set α
hC : C ⊆ (C₁ ∪ C₂) \ {e}
hC' : M.IsCircuit C
⊢ ∃ C ⊆ (C₁ ∪ C₂) \ {e}, M.IsCircuit C

Tactic:
⟨C, hC, hC'⟩

Premises used: And.intro, Exists.intro
-- 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₂
e : α
hnss : ¬C₁ ⊆ C₂
f : α
hf₁ : f ∈ C₁
hf₂ : f ∉ C₂
he₁ : e ∈ C₁
he₂ : e ∈ C₂
C : Set α
hC : C ⊆ (C₁ ∪ C₂) \ {e}
hC' : M.IsCircuit C
⊢ ∃ C ⊆ (C₁ ∪ C₂) \ {e}, M.IsCircuit C

Tactic:
exact ⟨C, hC, hC'⟩
-- 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₂
e : α
hnss : ¬C₁ ⊆ C₂
f : α
hf₁ : f ∈ C₁
hf₂ : f ∉ C₂
he₁ : e ∈ C₁
he₂ : e ∉ C₂
⊢ ∃ C ⊆ (C₁ ∪ C₂) \ {e}, M.IsCircuit C

Tactic:
⟨C₂, subset_diff_singleton subset_union_right he₂, hC₂⟩

Premises used: Set.subset_union_right, Set.subset_diff_singleton, And.intro, Exists.intro
-- 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₂
e : α
hnss : ¬C₁ ⊆ C₂
f : α
hf₁ : f ∈ C₁
hf₂ : f ∉ C₂
he₁ : e ∈ C₁
he₂ : e ∉ C₂
⊢ ∃ C ⊆ (C₁ ∪ C₂) \ {e}, M.IsCircuit C

Tactic:
exact ⟨C₂, subset_diff_singleton subset_union_right he₂, hC₂⟩
-- 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₂
e : α
hnss : ¬C₁ ⊆ C₂
f : α
hf₁ : f ∈ C₁
hf₂ : f ∉ C₂
he₁ : e ∉ C₁
⊢ ∃ C ⊆ (C₁ ∪ C₂) \ {e}, M.IsCircuit C

Tactic:
⟨C₁, subset_diff_singleton subset_union_left he₁, hC₁⟩

Premises used: Set.subset_union_left, Set.subset_diff_singleton, And.intro, Exists.intro
-- 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₂
e : α
hnss : ¬C₁ ⊆ C₂
f : α
hf₁ : f ∈ C₁
hf₂ : f ∉ C₂
he₁ : e ∉ C₁
⊢ ∃ C ⊆ (C₁ ∪ C₂) \ {e}, M.IsCircuit C

Tactic:
exact ⟨C₁, subset_diff_singleton subset_union_left he₁, hC₁⟩
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C : Set α
inst : M.Finitary
hC : M.IsCircuit C
⊢ ¬M.Indep C

Tactic:
have hi := hC.dep.not_indep
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C : Set α
inst : M.Finitary
hC : M.IsCircuit C
hi : ¬M.Indep C
⊢ ¬∀ J ⊆ C, J.Finite → M.Indep J

Tactic:
rw [indep_iff_forall_finite_subset_indep] at hi

Premises used: Matroid.indep_iff_forall_finite_subset_indep
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C : Set α
inst : M.Finitary
hC : M.IsCircuit C
hi : ¬∀ J ⊆ C, J.Finite → M.Indep J
⊢ ∃ J ⊆ C, J.Finite ∧ ¬M.Indep J

Tactic:
push Not at hi

Premises used: Not
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C : Set α
inst : M.Finitary
hC : M.IsCircuit C
hi : ∃ J ⊆ C, J.Finite ∧ ¬M.Indep J
obtain : ∀ (J : Set α) (hJC : J ⊆ C) (hJfin : J.Finite) (hJ : ¬M.Indep J), C.Finite
⊢ C.Finite

Tactic:
obtain ⟨J, hJC, hJfin, hJ⟩ := hi
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C : Set α
inst : M.Finitary
hC : M.IsCircuit C
J : Set α
hJC : J ⊆ C
hJfin : J.Finite
hJ : ¬M.Indep J
rwa rwa₁ rwa₂ rwa₃ : J.Finite
⊢ C.Finite

Tactic:
rwa [← hC.eq_of_not_indep_subset hJ hJC]

Premises used: Matroid.IsCircuit.eq_of_not_indep_subset
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
⊢ M.Finitary ↔ ∀ (C : Set α), M.IsCircuit C → C.Finite

Tactic:
⟨fun _ _ ↦ IsCircuit.finite, fun h ↦
    ⟨fun I hI ↦ indep_iff_not_dep.2 ⟨fun hd ↦ ?_,fun x hx ↦ ?_⟩⟩⟩

Premises used: Iff.mpr, Matroid.IsCircuit.finite, Matroid.indep_iff_not_dep, And.intro, Iff.intro, Matroid.Finitary.mk
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
refine_1 :
  ∀ (h : ∀ (C : Set α), M.IsCircuit C → C.Finite) (I : Set α) (hI : ∀ J ⊆ I, J.Finite → M.Indep J) (hd : M.Dep I), False
refine_2 :
  ∀ (h : ∀ (C : Set α), M.IsCircuit C → C.Finite) (I : Set α) (hI : ∀ J ⊆ I, J.Finite → M.Indep J) (x : α) (hx : x ∈ I),
    x ∈ M.E
⊢ M.Finitary ↔ ∀ (C : Set α), M.IsCircuit C → C.Finite

Tactic:
refine ⟨fun _ _ ↦ IsCircuit.finite, fun h ↦
    ⟨fun I hI ↦ indep_iff_not_dep.2 ⟨fun hd ↦ ?_,fun x hx ↦ ?_⟩⟩⟩
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
h : ∀ (C : Set α), M.IsCircuit C → C.Finite
I : Set α
hI : ∀ J ⊆ I, J.Finite → M.Indep J
hd : M.Dep I
refine_1 : ∀ (C : Set α) (hCI : C ⊆ I) (hC : M.IsCircuit C), False
⊢ False

Tactic:
obtain ⟨C, hCI, hC⟩ := hd.exists_isCircuit_subset

Premises used: Matroid.Dep.exists_isCircuit_subset
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
h : ∀ (C : Set α), M.IsCircuit C → C.Finite
I : Set α
hI : ∀ J ⊆ I, J.Finite → M.Indep J
hd : M.Dep I
C : Set α
hCI : C ⊆ I
hC : M.IsCircuit C
⊢ False

Tactic:
hC.dep.not_indep <| hI _ hCI (h C hC)

Premises used: Matroid.Dep.not_indep, Matroid.IsCircuit.dep
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
h : ∀ (C : Set α), M.IsCircuit C → C.Finite
I : Set α
hI : ∀ J ⊆ I, J.Finite → M.Indep J
hd : M.Dep I
C : Set α
hCI : C ⊆ I
hC : M.IsCircuit C
⊢ False

Tactic:
exact hC.dep.not_indep <| hI _ hCI (h C hC)

Premises used: Matroid.Dep.not_indep, Matroid.IsCircuit.dep
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
h : ∀ (C : Set α), M.IsCircuit C → C.Finite
I : Set α
hI : ∀ J ⊆ I, J.Finite → M.Indep J
x : α
hx : x ∈ I
⊢ {x} ⊆ I

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
h : ∀ (C : Set α), M.IsCircuit C → C.Finite
I : Set α
hI : ∀ J ⊆ I, J.Finite → M.Indep J
x : α
hx : x ∈ I
⊢ x ∈ M.E

Tactic:
simpa using (hI {x} (by simpa) (finite_singleton _)).subset_ground

Premises used: Matroid.Indep.subset_ground, Singleton.singleton, Set.finite_singleton
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
X : Set α
e : α
inst : M.Finitary
he : e ∈ M.closure X
pos : ∀ (heY : e ∈ X), ∃ I ⊆ X, I.Finite ∧ M.Indep I ∧ e ∈ M.closure I
neg : ∀ (heY : e ∉ X), ∃ I ⊆ X, I.Finite ∧ M.Indep I ∧ e ∈ M.closure I
⊢ ∃ I ⊆ X, I.Finite ∧ M.Indep I ∧ e ∈ M.closure I

Tactic:
by_cases heY : e ∈ X
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
X : Set α
e : α
inst : M.Finitary
he : e ∈ M.closure X
heY : e ∈ X
pos : ∀ (J : Set α) (hJ : M.IsBasis J {e}), ∃ I ⊆ X, I.Finite ∧ M.Indep I ∧ e ∈ M.closure I
⊢ ∃ I ⊆ X, I.Finite ∧ M.Indep I ∧ e ∈ M.closure I

Tactic:
obtain ⟨J, hJ⟩ := M.exists_isBasis {e}

Premises used: Matroid.exists_isBasis, Singleton.singleton
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
X : Set α
e : α
inst : M.Finitary
he : e ∈ M.closure X
heY : e ∈ X
J : Set α
hJ : M.IsBasis J {e}
⊢ {e} ⊆ X

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
X : Set α
e : α
inst : M.Finitary
he : e ∈ M.closure X
heY : e ∈ X
J : Set α
hJ : M.IsBasis J {e}
⊢ e ∈ M.closure J

Tactic:
simpa using hJ.subset_closure

Premises used: Matroid.IsBasis.subset_closure
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
X : Set α
e : α
inst : M.Finitary
he : e ∈ M.closure X
heY : e ∈ X
J : Set α
hJ : M.IsBasis J {e}
⊢ ∃ I ⊆ X, I.Finite ∧ M.Indep I ∧ e ∈ M.closure I

Tactic:
exact ⟨J, hJ.subset.trans (by simpa), (finite_singleton e).subset hJ.subset, hJ.indep,
      by simpa using hJ.subset_closure⟩
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
X : Set α
e : α
inst : M.Finitary
he : e ∈ M.closure X
heY : e ∉ X
neg :
  ∀ (C : Set α) (hCs : C ⊆ insert e X) (hC : M.IsCircuit C) (heC : e ∈ C),
    ∃ I ⊆ X, I.Finite ∧ M.Indep I ∧ e ∈ M.closure I
⊢ ∃ I ⊆ X, I.Finite ∧ M.Indep I ∧ e ∈ M.closure I

Tactic:
obtain ⟨C, hCs, hC, heC⟩ := exists_isCircuit_of_mem_closure he heY

Premises used: Matroid.exists_isCircuit_of_mem_closure
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
X : Set α
e : α
inst : M.Finitary
he : e ∈ M.closure X
heY : e ∉ X
C : Set α
hCs : C ⊆ insert e X
hC : M.IsCircuit C
heC : e ∈ C
⊢ C \ {e} ⊆ X

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
X : Set α
e : α
inst : M.Finitary
he : e ∈ M.closure X
heY : e ∉ X
C : Set α
hCs : C ⊆ insert e X
hC : M.IsCircuit C
heC : e ∈ C
⊢ ∃ I ⊆ X, I.Finite ∧ M.Indep I ∧ e ∈ M.closure I

Tactic:
exact ⟨C \ {e}, by simpa, hC.finite.diff, hC.diff_singleton_indep heC,
    hC.mem_closure_diff_singleton_of_mem heC⟩
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
inst : M.Finitary
hX : X.Finite
hXY : X ⊆ M.closure Y
aux : ∃ T ⊆ Y, T.Finite ∧ X ⊆ M.closure T
obtain :
  ∀ (T : Set α) (hT : T ⊆ Y) (hTfin : T.Finite) (hXT : X ⊆ M.closure T), ∃ I ⊆ Y, I.Finite ∧ M.Indep I ∧ X ⊆ M.closure I
⊢ ∃ I ⊆ Y, I.Finite ∧ M.Indep I ∧ X ⊆ M.closure I

Tactic:
obtain ⟨T, hT, hTfin, hXT⟩ := aux
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
inst : M.Finitary
hX : X.Finite
hXY : X ⊆ M.closure Y
T : Set α
hT : T ⊆ Y
hTfin : T.Finite
hXT : X ⊆ M.closure T
obtain : ∀ (I : Set α) (hI : M.IsBasis' I T), ∃ I ⊆ Y, I.Finite ∧ M.Indep I ∧ X ⊆ M.closure I
⊢ ∃ I ⊆ Y, I.Finite ∧ M.Indep I ∧ X ⊆ M.closure I

Tactic:
obtain ⟨I, hI⟩ := M.exists_isBasis' T

Premises used: Matroid.exists_isBasis'
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
inst : M.Finitary
hX : X.Finite
hXY : X ⊆ M.closure Y
T : Set α
hT : T ⊆ Y
hTfin : T.Finite
hXT : X ⊆ M.closure T
I : Set α
hI : M.IsBasis' I T
rwa rwa₁ rwa₂ rwa₃ : X ⊆ M.closure T
⊢ X ⊆ M.closure I

Tactic:
rwa [hI.closure_eq_closure]

Premises used: Matroid.IsBasis'.closure_eq_closure
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
inst : M.Finitary
hX : X.Finite
hXY : X ⊆ M.closure Y
T : Set α
hT : T ⊆ Y
hTfin : T.Finite
hXT : X ⊆ M.closure T
I : Set α
hI : M.IsBasis' I T
⊢ ∃ I ⊆ Y, I.Finite ∧ M.Indep I ∧ X ⊆ M.closure I

Tactic:
exact ⟨_, hI.subset.trans hT, hTfin.subset hI.subset, hI.indep, by rwa [hI.closure_eq_closure]⟩
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
inst : M.Finitary
hX : X.Finite
hXY : X ⊆ M.closure Y
suffices : ∃ T ⊆ Y, T.Finite ∧ X ⊆ M.closure T
⊢ ∃ I ⊆ Y, I.Finite ∧ M.Indep I ∧ X ⊆ M.closure I

Tactic:
suffices aux : ∃ T ⊆ Y, T.Finite ∧ X ⊆ M.closure T by
    obtain ⟨T, hT, hTfin, hXT⟩ := aux
    obtain ⟨I, hI⟩ := M.exists_isBasis' T
    exact ⟨_, hI.subset.trans hT, hTfin.subset hI.subset, hI.indep, by rwa [hI.closure_eq_closure]⟩
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
inst : M.Finitary
hX : X.Finite
hXY : X ⊆ M.closure Y
⊢ ∅ ⊆ Y ∧ Set.Finite.{u_1} (α := α) ∅ ∧ ∅ ⊆ M.closure ∅

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
inst : M.Finitary
hX : X.Finite
hXY : X ⊆ M.closure Y
refine :
  ∀ {e : α} {Z : Set α} (heX : e ∈ X),
    Z ⊆ X →
      ∀ (heZ : e ∉ Z),
        (∃ T ⊆ Y, T.Finite ∧ Z ⊆ M.closure T) →
          ∀ (T : Set α) (hTY : T ⊆ Y) (hTfin : T.Finite) (hT : Z ⊆ M.closure T),
            ∃ T ⊆ Y, T.Finite ∧ insert e Z ⊆ M.closure T
⊢ ∃ T ⊆ Y, T.Finite ∧ X ⊆ M.closure T

Tactic:
refine Finite.induction_on_subset X hX ⟨∅, by simp⟩ (fun {e Z} heX _ heZ ⟨T, hTY, hTfin, hT⟩ ↦ ?_)
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
inst : M.Finitary
hX : X.Finite
hXY : X ⊆ M.closure Y
e : α
Z : Set α
heX : e ∈ X
h : Z ⊆ X
heZ : e ∉ Z
h_1 : ∃ T ⊆ Y, T.Finite ∧ Z ⊆ M.closure T
T : Set α
hTY : T ⊆ Y
hTfin : T.Finite
hT : Z ⊆ M.closure T
obtain :
  ∀ (S : Set α) (hSY : S ⊆ Y) (hSfin : S.Finite) (heS : e ∈ M.closure S), ∃ T ⊆ Y, T.Finite ∧ insert e Z ⊆ M.closure T
⊢ ∃ T ⊆ Y, T.Finite ∧ insert e Z ⊆ M.closure T

Tactic:
obtain ⟨S, hSY, hSfin, -, heS⟩ := exists_mem_finite_closure_of_mem_closure (hXY heX)

Premises used: Matroid.exists_mem_finite_closure_of_mem_closure
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
inst : M.Finitary
hX : X.Finite
hXY : X ⊆ M.closure Y
e : α
Z : Set α
heX : e ∈ X
h : Z ⊆ X
heZ : e ∉ Z
h_1 : ∃ T ⊆ Y, T.Finite ∧ Z ⊆ M.closure T
T : Set α
hTY : T ⊆ Y
hTfin : T.Finite
hT : Z ⊆ M.closure T
S : Set α
hSY : S ⊆ Y
hSfin : S.Finite
heS : e ∈ M.closure S
⊢ ∃ T ⊆ Y, T.Finite ∧ insert e Z ⊆ M.closure T

Tactic:
⟨S ∪ T, union_subset hSY hTY, hSfin.union hTfin, insert_subset
    (M.closure_mono subset_union_left heS) (hT.trans (M.closure_mono subset_union_right))⟩

Premises used: Set.Finite.union, Set.subset_union_right, Matroid.closure_mono, HasSubset.Subset.trans, Set.union_subset, Set.subset_union_left, And.intro, Exists.intro, Union.union, Set.insert_subset
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
inst : M.Finitary
hX : X.Finite
hXY : X ⊆ M.closure Y
e : α
Z : Set α
heX : e ∈ X
h : Z ⊆ X
heZ : e ∉ Z
h_1 : ∃ T ⊆ Y, T.Finite ∧ Z ⊆ M.closure T
T : Set α
hTY : T ⊆ Y
hTfin : T.Finite
hT : Z ⊆ M.closure T
S : Set α
hSY : S ⊆ Y
hSfin : S.Finite
heS : e ∈ M.closure S
⊢ ∃ T ⊆ Y, T.Finite ∧ insert e Z ⊆ M.closure T

Tactic:
exact ⟨S ∪ T, union_subset hSY hTY, hSfin.union hTfin, insert_subset
    (M.closure_mono subset_union_left heS) (hT.trans (M.closure_mono subset_union_right))⟩
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
K : Set α
⊢ M.IsCocircuit K ↔ M✶.IsCircuit K

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
K : Set α
hK : M.IsCocircuit K
⊢ M✶.IsCircuit K

Tactic:
hK
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C : Set α
hC : M.IsCircuit C
rwa : M✶✶.IsCircuit C
rwa₁ rwa₂ rwa₃ rwa₄ : M.IsCircuit C
⊢ M✶.IsCocircuit C

Tactic:
rwa [isCocircuit_def, dual_dual]

Premises used: Matroid.isCocircuit_def, Matroid.dual_dual
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C : Set α
hC : M.IsCocircuit C
⊢ C.Nonempty

Tactic:
hC.isCircuit.nonempty

Premises used: Matroid.IsCircuit.nonempty, Matroid.IsCocircuit.isCircuit
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C : Set α
hC : M.IsCocircuit C
⊢ C ⊆ M.E

Tactic:
hC.isCircuit.subset_ground

Premises used: Matroid.IsCircuit.subset_ground, Maximal, Matroid.IsCocircuit.isCircuit
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C : Set α
rw : M✶✶.IsCircuit C ↔ M.IsCircuit C
rw₁ rw₂ : M.IsCircuit C ↔ M.IsCircuit C
⊢ M✶.IsCocircuit C ↔ M.IsCircuit C

Tactic:
rw [isCocircuit_def, dual_dual]

Premises used: Matroid.isCocircuit_def, Matroid.dual_dual
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
X : Set α
⊢ M.Coindep X ↔ (∀ K ⊆ X, ¬M.IsCocircuit K) ∧ X ⊆ M.E

Tactic:
indep_iff_forall_subset_not_isCircuit'

Premises used: Maximal, Matroid.indep_iff_forall_subset_not_isCircuit'
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
K : Set α
h : ∀ (x : Set α), M✶.Dep x ↔ (∀ (B : Set α), M.IsBase B → (x ∩ B).Nonempty) ∧ x ⊆ M.E
⊢ M✶.Dep = fun (X : Set α) ↦ (∀ (B : Set α), M.IsBase B → (X ∩ B).Nonempty) ∧ X ⊆ M.E

Tactic:
ext
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
K x : Set α
⊢ M✶.Dep x ↔ (∀ (B : Set α), M.IsBase B → (x ∩ B).Nonempty) ∧ x ⊆ M.E

Tactic:
apply dual_dep_iff_forall

Premises used: Matroid.dual_dep_iff_forall
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
K : Set α
⊢ M✶.Dep = fun (X : Set α) ↦ (∀ (B : Set α), M.IsBase B → (X ∩ B).Nonempty) ∧ X ⊆ M.E

Tactic:
have aux : M✶.Dep = fun X ↦ (∀ B, M.IsBase B → (X ∩ B).Nonempty) ∧ X ⊆ M.E := by
    ext; apply dual_dep_iff_forall
-- 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
rw :
  Minimal (fun (X : Set α) ↦ ∀ (B : Set α), M.IsBase B → (X ∩ B).Nonempty) K ↔
    Minimal (fun (X : Set α) ↦ (∀ (B : Set α), M.IsBase B → (X ∩ B).Nonempty) ∧ X ⊆ M.E) K
⊢ M.IsCocircuit K ↔ Minimal (fun (X : Set α) ↦ ∀ (B : Set α), M.IsBase B → (X ∩ B).Nonempty) K

Tactic:
rw [isCocircuit_def, isCircuit_def, aux, iff_comm]

Premises used: iff_comm, Matroid.isCocircuit_def, Matroid.isCircuit_def
-- 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
⊢ Minimal (fun (X : Set α) ↦ ∀ (B : Set α), M.IsBase B → (X ∩ B).Nonempty) K ↔
    Minimal (fun (X : Set α) ↦ (∀ (B : Set α), M.IsBase B → (X ∩ B).Nonempty) ∧ X ⊆ M.E) K

Tactic:
minimal_iff_minimal_of_imp_of_forall (fun _ h ↦ h.1) fun X hX ↦
    ⟨X ∩ M.E, inter_subset_left, fun B hB ↦ ?_, inter_subset_right⟩

Premises used: minimal_iff_minimal_of_imp_of_forall, Matroid.E, Set.inter_subset_left, Inter.inter, And.left, And.intro, Exists.intro, Set.inter_subset_right
-- 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
refine :
  ∀ (X : Set α) (hX : ∀ (B : Set α), M.IsBase B → (X ∩ B).Nonempty) (B : Set α) (hB : M.IsBase B),
    (X ∩ M.E ∩ B).Nonempty
⊢ Minimal (fun (X : Set α) ↦ ∀ (B : Set α), M.IsBase B → (X ∩ B).Nonempty) K ↔
    Minimal (fun (X : Set α) ↦ (∀ (B : Set α), M.IsBase B → (X ∩ B).Nonempty) ∧ X ⊆ M.E) K

Tactic:
refine minimal_iff_minimal_of_imp_of_forall (fun _ h ↦ h.1) fun X hX ↦
    ⟨X ∩ M.E, inter_subset_left, fun B hB ↦ ?_, 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 α
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
rw : (X ∩ B).Nonempty
⊢ (X ∩ M.E ∩ B).Nonempty

Tactic:
rw [inter_assoc, inter_eq_self_of_subset_right hB.subset_ground]

Premises used: Matroid.IsBase.subset_ground, Set.inter_eq_self_of_subset_right, Set.inter_assoc
-- 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:
hX B hB