awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
R : Set α
hIR : I ⊆ R
heR : e ∈ R
hR : R ⊆ M.E
J : Set α
hJI : J ⊆ I
heJ : M.closure {e} ∩ R ⊆ (M ↾ R).closure J
a : {e} ⊆ M.closure J
⊢ M.closure {e} ⊆ M.closure J

Tactic:
refine closure_subset_closure_of_subset_closure ?_

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

Tactic:
rw [restrict_closure_eq _ (hJI.trans hIR) hR] at heJ

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

Tactic:
simp only [subset_inter_iff, inter_subset_right, and_true] at heJ

Premises used: and_true, Set.subset_inter_iff, Set.inter_subset_right
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
I : Set α
e : α
R : Set α
hIR : I ⊆ R
heR : e ∈ R
hR : R ⊆ M.E
J : Set α
hJI : J ⊆ I
heJ : M.closure {e} ∩ R ⊆ M.closure J
⊢ {e} ⊆ M.closure {e} ∩ R

Tactic:
simpa [M.mem_closure_of_mem' (mem_singleton e) (hR heR)]

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

Tactic:
exact subset_trans (by simpa [M.mem_closure_of_mem' (mem_singleton e) (hR heR)]) heJ

Premises used: subset_trans
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
I : Set α
e : α
M : Matroid α
A B : Set α
⊢ M.closure A ⊆ B ∪ univ \ M.E ↔ M.closure A ⊆ B

Tactic:
⟨fun h ↦ ?_, fun h ↦ h.trans subset_union_left⟩

Premises used: HasSubset.Subset.trans, Set.subset_union_left, Iff.intro
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
I : Set α
e : α
M : Matroid α
A B : Set α
refine : ∀ (h : M.closure A ⊆ B ∪ univ \ M.E), M.closure A ⊆ B
⊢ M.closure A ⊆ B ∪ univ \ M.E ↔ M.closure A ⊆ B

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ h.trans subset_union_left⟩
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
I : Set α
e : α
M : Matroid α
A B : Set α
h : M.closure A ⊆ B ∪ univ \ M.E
⊢ M.closure A ⊆ B

Tactic:
(subset_inter h (M.closure_subset_ground A)).trans ?_

Premises used: Matroid.closure_subset_ground, HasSubset.Subset.trans, Set.subset_inter
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
I : Set α
e : α
M : Matroid α
A B : Set α
h : M.closure A ⊆ B ∪ univ \ M.E
refine : (B ∪ univ \ M.E) ∩ M.E ⊆ B
⊢ M.closure A ⊆ B

Tactic:
refine (subset_inter h (M.closure_subset_ground A)).trans ?_

Premises used: Matroid.closure_subset_ground, HasSubset.Subset.trans, Set.subset_inter
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
I : Set α
e : α
M : Matroid α
A B : Set α
h : M.closure A ⊆ B ∪ univ \ M.E
⊢ (B ∪ univ \ M.E) ∩ M.E ⊆ B

Tactic:
simp [union_inter_distrib_right]

Premises used: Set.union_inter_distrib_right
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
I : Set α
e : α
M : Matroid α
⊢ ∀ (A B : Set α), M.closure A ⊆ B ∪ univ \ M.E ↔ M.closure A ⊆ B

Tactic:
have aux (A B) : M.closure A ⊆ B ∪ univ \ M.E ↔ M.closure A ⊆ B := by
    refine ⟨fun h ↦ ?_, fun h ↦ h.trans subset_union_left⟩
    refine (subset_inter h (M.closure_subset_ground A)).trans ?_
    simp [union_inter_distrib_right]
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
I : Set α
e : α
M : Matroid α
aux : ∀ (A B : Set α), M.closure A ⊆ B ∪ univ \ M.E ↔ M.closure A ⊆ B
⊢ (M ↾ univ).fundCircuit e I = M.fundCircuit e I

Tactic:
simp [fundCircuit, aux]

Premises used: Matroid.fundCircuit
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : M.Dep X
obtain : ∀ (I : Set α) (hI : M.IsBasis I X), ∃ C ⊆ X, M.IsCircuit C
⊢ ∃ C ⊆ X, M.IsCircuit C

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

Premises used: Matroid.exists_isBasis
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
I : Set α
hX : M.Dep I
hI : M.IsBasis I I
⊢ False

Tactic:
hI.indep.not_dep hX

Premises used: Matroid.IsBasis.indep, Matroid.Indep.not_dep
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
I : Set α
hX : M.Dep I
hI : M.IsBasis I I
⊢ False

Tactic:
exact hI.indep.not_dep hX

Premises used: Matroid.IsBasis.indep, Matroid.Indep.not_dep
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : M.Dep X
I : Set α
hI : M.IsBasis I X
obtain : ∀ (e : α) (heX : e ∈ X) (heI : e ∉ I), ∃ C ⊆ X, M.IsCircuit C
⊢ ∃ C ⊆ X, M.IsCircuit C

Tactic:
obtain ⟨e, heX, heI⟩ := exists_of_ssubset
    (hI.subset.ssubset_of_ne (by rintro rfl; exact hI.indep.not_dep hX))

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 α
X : Set α
hX : M.Dep X
I : Set α
hI : M.IsBasis I X
e : α
heX : e ∈ X
heI : e ∉ I
⊢ ∃ C ⊆ X, M.IsCircuit C

Tactic:
⟨M.fundCircuit e I, (M.fundCircuit_subset_insert e I).trans (insert_subset heX hI.subset),
    hI.indep.fundCircuit_isCircuit (hI.subset_closure heX) heI⟩

Premises used: HasSubset.Subset.trans, Matroid.IsBasis.subset, And.intro, Exists.intro, Matroid.fundCircuit, Matroid.IsBasis.indep, Matroid.IsBasis.subset_closure, Matroid.Indep.fundCircuit_isCircuit, Set.insert_subset, Matroid.fundCircuit_subset_insert
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : M.Dep X
I : Set α
hI : M.IsBasis I X
e : α
heX : e ∈ X
heI : e ∉ I
⊢ ∃ C ⊆ X, M.IsCircuit C

Tactic:
exact ⟨M.fundCircuit e I, (M.fundCircuit_subset_insert e I).trans (insert_subset heX hI.subset),
    hI.indep.fundCircuit_isCircuit (hI.subset_closure heX) heI⟩
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
⊢ M.Dep X ↔ ∃ C ⊆ X, M.IsCircuit C

Tactic:
⟨Dep.exists_isCircuit_subset, fun ⟨C, hCX, hC⟩ ↦ hC.dep.superset hCX⟩

Premises used: Matroid.Dep, Matroid.Dep.superset, _private.0.Matroid.dep_iff_superset_isCircuit.match_1, Matroid.Dep.exists_isCircuit_subset, Iff.intro, Matroid.IsCircuit.dep
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
X : Set α
⊢ M.Dep X ↔ (∃ C ⊆ X, M.IsCircuit C) ∧ X ⊆ M.E

Tactic:
⟨fun h ↦ ⟨h.exists_isCircuit_subset, h.subset_ground⟩,
    fun ⟨⟨C, hCX, hC⟩, h⟩ ↦ hC.dep.superset hCX⟩

Premises used: Matroid.Dep, Matroid.Dep.subset_ground, Matroid.Dep.superset, _private.0.Matroid.dep_iff_superset_isCircuit'.match_1, Matroid.Dep.exists_isCircuit_subset, And.intro, Iff.intro, Matroid.IsCircuit.dep
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
I : Set α
simp_rw : ¬((∃ C ⊆ I, M.IsCircuit C) ∧ I ⊆ M.E) ∧ I ⊆ M.E ↔ (∀ C ⊆ I, ¬M.IsCircuit C) ∧ I ⊆ M.E
⊢ M.Indep I ↔ (∀ C ⊆ I, ¬M.IsCircuit C) ∧ I ⊆ M.E

Tactic:
simp_rw [indep_iff_not_dep, dep_iff_superset_isCircuit']

Premises used: Matroid.dep_iff_superset_isCircuit', Matroid.indep_iff_not_dep
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
I : Set α
⊢ ¬((∃ C ⊆ I, M.IsCircuit C) ∧ I ⊆ M.E) ∧ I ⊆ M.E ↔ (∀ C ⊆ I, ¬M.IsCircuit C) ∧ I ⊆ M.E

Tactic:
aesop
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
I : Set α
hI : I ⊆ M.E
rw : (∀ C ⊆ I, ¬M.IsCircuit C) ∧ I ⊆ M.E ↔ ∀ C ⊆ I, ¬M.IsCircuit C
rw₁ rw₂ : (∀ C ⊆ I, ¬M.IsCircuit C) ↔ ∀ C ⊆ I, ¬M.IsCircuit C
⊢ M.Indep I ↔ ∀ C ⊆ I, ¬M.IsCircuit C

Tactic:
rw [indep_iff_forall_subset_not_isCircuit', and_iff_left hI]

Premises used: and_iff_left, Matroid.indep_iff_forall_subset_not_isCircuit'
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C : Set α
hC : M.IsCircuit C
e : α
he : e ∈ C
rw rw₁ : M.closure C = M.closure C
⊢ M.closure (C \ {e}) = M.closure C

Tactic:
rw [(hC.diff_singleton_isBasis he).closure_eq_closure]

Premises used: Matroid.IsCircuit.diff_singleton_isBasis, Matroid.IsBasis.closure_eq_closure
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C : Set α
hC : M.IsCircuit C
e : α
he : e ∉ C
rw rw₁ : M.closure C = M.closure C
⊢ M.closure (C \ {e}) = M.closure C

Tactic:
rw [diff_singleton_eq_self he]

Premises used: Set.diff_singleton_eq_self
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C : Set α
hC : M.IsCircuit C
e : α
rw : C ⊆ M.closure C
⊢ C ⊆ M.closure (C \ {e})

Tactic:
rw [hC.closure_diff_singleton_eq]

Premises used: Matroid.IsCircuit.closure_diff_singleton_eq
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C : Set α
hC : M.IsCircuit C
e : α
⊢ C ⊆ M.closure C

Tactic:
M.subset_closure _ hC.subset_ground

Premises used: Matroid.subset_closure, Matroid.IsCircuit.subset_ground
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C : Set α
hC : M.IsCircuit C
e : α
⊢ C ⊆ M.closure C

Tactic:
exact M.subset_closure _ hC.subset_ground

Premises used: Matroid.subset_closure, Matroid.IsCircuit.subset_ground
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
C : Set α
e : α
hC : M.IsCircuit C
heC : e ∈ C
⊢ e ∈ M.closure (C \ {e})

Tactic:
hC.subset_closure_diff_singleton e heC

Premises used: Matroid.IsCircuit.subset_closure_diff_singleton
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
X : Set α
e : α
he : e ∈ M.closure X
heX : e ∉ X
I : Set α
hI : M.IsBasis' I X
rwa rwa₁ rwa₂ rwa₃ : e ∈ M.closure X
⊢ e ∈ 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 : Set α
e : α
he : e ∉ X
h : ∃ C ⊆ insert e X, M.IsCircuit C ∧ e ∈ C
C : Set α
hCX : 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₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h : ∀ ⦃C : Set α⦄, C ⊆ M₁.E → (M₁.IsCircuit C ↔ M₂.IsCircuit C)
⊢ ∀ {C : Set α}, M₁.IsCircuit C ↔ M₂.IsCircuit C

Tactic:
have h' {C} : M₁.IsCircuit C ↔ M₂.IsCircuit C :=
    (em (C ⊆ M₁.E)).elim (h (C := C)) (fun hC ↦ iff_of_false (mt IsCircuit.subset_ground hC)
      (mt IsCircuit.subset_ground fun hss ↦ hC (hss.trans_eq hE.symm)))
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h : ∀ ⦃C : Set α⦄, C ⊆ M₁.E → (M₁.IsCircuit C ↔ M₂.IsCircuit C)
h' : ∀ {C : Set α}, M₁.IsCircuit C ↔ M₂.IsCircuit C
⊢ M₁ = M₂

Tactic:
ext_indep hE fun I hI ↦ ?_

Premises used: Matroid.ext_indep
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h : ∀ ⦃C : Set α⦄, C ⊆ M₁.E → (M₁.IsCircuit C ↔ M₂.IsCircuit C)
h' : ∀ {C : Set α}, M₁.IsCircuit C ↔ M₂.IsCircuit C
refine : ∀ (I : Set α) (hI : I ⊆ M₁.E), M₁.Indep I ↔ M₂.Indep I
⊢ M₁ = M₂

Tactic:
refine ext_indep hE fun I hI ↦ ?_

Premises used: Matroid.ext_indep
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h : ∀ ⦃C : Set α⦄, C ⊆ M₁.E → (M₁.IsCircuit C ↔ M₂.IsCircuit C)
h' : ∀ {C : Set α}, M₁.IsCircuit C ↔ M₂.IsCircuit C
I : Set α
hI : I ⊆ M₁.E
simp_rw : (∀ C ⊆ I, ¬M₁.IsCircuit C) ↔ M₂.Indep I
simp_rw₁ : (∀ C ⊆ I, ¬M₂.IsCircuit C) ↔ M₂.Indep I
⊢ M₁.Indep I ↔ M₂.Indep I

Tactic:
simp_rw [indep_iff_forall_subset_not_isCircuit hI, h',
    indep_iff_forall_subset_not_isCircuit (hI.trans_eq hE)]

Premises used: LE.le.trans_eq, Matroid.indep_iff_forall_subset_not_isCircuit
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h₁ : ∀ (C : Set α), M₁.IsCircuit C → ¬M₂.Indep C
h₂ : ∀ (C : Set α), M₂.IsCircuit C → ¬M₁.Indep C
⊢ M₁ = M₂

Tactic:
ext_isCircuit hE fun C hCE ↦ ⟨fun hC ↦ ?_, fun hC ↦ ?_⟩

Premises used: Iff.intro, Matroid.ext_isCircuit
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h₁ : ∀ (C : Set α), M₁.IsCircuit C → ¬M₂.Indep C
h₂ : ∀ (C : Set α), M₂.IsCircuit C → ¬M₁.Indep C
refine_1 : ∀ (C : Set α) (hCE : C ⊆ M₁.E) (hC : M₁.IsCircuit C), M₂.IsCircuit C
refine_2 : ∀ (C : Set α) (hCE : C ⊆ M₁.E) (hC : M₂.IsCircuit C), M₁.IsCircuit C
⊢ M₁ = M₂

Tactic:
refine ext_isCircuit hE fun C hCE ↦ ⟨fun hC ↦ ?_, fun hC ↦ ?_⟩

Premises used: Iff.intro, Matroid.ext_isCircuit
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h₁ : ∀ (C : Set α), M₁.IsCircuit C → ¬M₂.Indep C
h₂ : ∀ (C : Set α), M₂.IsCircuit C → ¬M₁.Indep C
C : Set α
hCE : C ⊆ M₁.E
hC : M₁.IsCircuit C
rwa rwa₁ rwa₂ rwa₃ : C ⊆ M₁.E
⊢ C ⊆ M₂.E

Tactic:
rwa [← hE]
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h₁ : ∀ (C : Set α), M₁.IsCircuit C → ¬M₂.Indep C
h₂ : ∀ (C : Set α), M₂.IsCircuit C → ¬M₁.Indep C
C : Set α
hCE : C ⊆ M₁.E
hC : M₁.IsCircuit C
refine_1 : ∀ (C' : Set α) (hC'C : C' ⊆ C) (hC' : M₂.IsCircuit C'), M₂.IsCircuit C
⊢ M₂.IsCircuit C

Tactic:
obtain ⟨C', hC'C, hC'⟩ := ((not_indep_iff (by rwa [← hE])).1 (h₁ C hC)).exists_isCircuit_subset

Premises used: Matroid.Dep.exists_isCircuit_subset, Iff.mp, Matroid.not_indep_iff
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h₁ : ∀ (C : Set α), M₁.IsCircuit C → ¬M₂.Indep C
h₂ : ∀ (C : Set α), M₂.IsCircuit C → ¬M₁.Indep C
C : Set α
hCE : C ⊆ M₁.E
hC : M₁.IsCircuit C
C' : Set α
hC'C : C' ⊆ C
hC' refine_1 refine_1₁ refine_1₂ refine_1₃ : M₂.IsCircuit C'
⊢ M₂.IsCircuit C

Tactic:
rwa [← hC.eq_of_not_indep_subset (h₂ C' hC') hC'C]

Premises used: Matroid.IsCircuit.eq_of_not_indep_subset
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h₁ : ∀ (C : Set α), M₁.IsCircuit C → ¬M₂.Indep C
h₂ : ∀ (C : Set α), M₂.IsCircuit C → ¬M₁.Indep C
C : Set α
hCE : C ⊆ M₁.E
hC : M₂.IsCircuit C
refine_2 : ∀ (C' : Set α) (hC'C : C' ⊆ C) (hC' : M₁.IsCircuit C'), M₁.IsCircuit C
⊢ M₁.IsCircuit C

Tactic:
obtain ⟨C', hC'C, hC'⟩ := ((not_indep_iff hCE).1 (h₂ C hC)).exists_isCircuit_subset

Premises used: Matroid.Dep.exists_isCircuit_subset, Iff.mp, Matroid.not_indep_iff
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h₁ : ∀ (C : Set α), M₁.IsCircuit C → ¬M₂.Indep C
h₂ : ∀ (C : Set α), M₂.IsCircuit C → ¬M₁.Indep C
C : Set α
hCE : C ⊆ M₁.E
hC : M₂.IsCircuit C
C' : Set α
hC'C : C' ⊆ C
hC' refine_2 refine_2₁ refine_2₂ refine_2₃ : M₁.IsCircuit C'
⊢ M₁.IsCircuit C

Tactic:
rwa [← hC.eq_of_not_indep_subset (h₁ C' hC') hC'C]

Premises used: Matroid.IsCircuit.eq_of_not_indep_subset
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M₁ M₂ : Matroid α
h : M₁ = M₂
⊢ M₁.E = M₂.E ∧ ∀ (C : Set α), M₁.IsCircuit C ↔ M₂.IsCircuit C

Tactic:
simp [h]
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
ι : Type u_2
J : Set α
x : ι → α
I : ι → Set α
z : α
hxI : ∀ (i : ι), x i ∉ I i
hC : ∀ (i : ι), M.IsCircuit (insert (x i) (I i))
hJx : M.IsCircuit (J ∪ range x)
hzJ : z ∈ J
hzI : ∀ (i : ι), z ∉ I i
inl : ∀ (hι : IsEmpty ι), ∃ C' ⊆ J ∪ ⋃ (i : ι), I i, M.IsCircuit C' ∧ z ∈ C'
inr : ∀ (hι : Nonempty ι), ∃ C' ⊆ J ∪ ⋃ (i : ι), I i, M.IsCircuit C' ∧ z ∈ C'
⊢ ∃ C' ⊆ J ∪ ⋃ (i : ι), I i, M.IsCircuit C' ∧ z ∈ C'

Tactic:
obtain hι | hι := isEmpty_or_nonempty ι

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
ι : Type u_2
J : Set α
x : ι → α
I : ι → Set α
z : α
hxI : ∀ (i : ι), x i ∉ I i
hC : ∀ (i : ι), M.IsCircuit (insert (x i) (I i))
hJx : M.IsCircuit (J ∪ range x)
hzJ : z ∈ J
hzI : ∀ (i : ι), z ∉ I i
hι : IsEmpty ι
⊢ J ⊆ J ∪ ⋃ (i : ι), I i

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
ι : Type u_2
J : Set α
x : ι → α
I : ι → Set α
z : α
hxI : ∀ (i : ι), x i ∉ I i
hC : ∀ (i : ι), M.IsCircuit (insert (x i) (I i))
hJx : M.IsCircuit (J ∪ range x)
hzJ : z ∈ J
hzI : ∀ (i : ι), z ∉ I i
hι : IsEmpty ι
⊢ M.IsCircuit J

Tactic:
simpa [range_eq_empty] using hJx

Premises used: Set.range_eq_empty
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
ι : Type u_2
J : Set α
x : ι → α
I : ι → Set α
z : α
hxI : ∀ (i : ι), x i ∉ I i
hC : ∀ (i : ι), M.IsCircuit (insert (x i) (I i))
hJx : M.IsCircuit (J ∪ range x)
hzJ : z ∈ J
hzI : ∀ (i : ι), z ∉ I i
hι : IsEmpty ι
⊢ ∃ C' ⊆ J ∪ ⋃ (i : ι), I i, M.IsCircuit C' ∧ z ∈ C'

Tactic:
exact ⟨J, by simp, by simpa [range_eq_empty] using hJx, hzJ⟩
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
ι : Type u_2
J : Set α
x : ι → α
I : ι → Set α
z : α
hxI : ∀ (i : ι), x i ∉ I i
hC : ∀ (i : ι), M.IsCircuit (insert (x i) (I i))
hJx : M.IsCircuit (J ∪ range x)
hzJ : z ∈ J
hzI : ∀ (i : ι), z ∉ I i
hι : Nonempty ι
hcl : z ∈ M.closure ((⋃ (i : ι), I i) ∪ J \ {z})
⊢ z ∉ (⋃ (i : ι), I i) ∪ J \ {z}

Tactic:
simp [hzI]
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
ι : Type u_2
J : Set α
x : ι → α
I : ι → Set α
z : α
hxI : ∀ (i : ι), x i ∉ I i
hC : ∀ (i : ι), M.IsCircuit (insert (x i) (I i))
hJx : M.IsCircuit (J ∪ range x)
hzJ : z ∈ J
hzI : ∀ (i : ι), z ∉ I i
hι : Nonempty ι
hcl : z ∈ M.closure ((⋃ (i : ι), I i) ∪ J \ {z})
⊢ ∃ C ⊆ insert z ((⋃ (i : ι), I i) ∪ J \ {z}), M.IsCircuit C ∧ z ∈ C

Tactic:
rw [mem_closure_iff_exists_isCircuit (by simp [hzI])] at hcl

Premises used: Matroid.mem_closure_iff_exists_isCircuit
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
ι : Type u_2
J : Set α
x : ι → α
I : ι → Set α
z : α
hxI : ∀ (i : ι), x i ∉ I i
hC : ∀ (i : ι), M.IsCircuit (insert (x i) (I i))
hJx : M.IsCircuit (J ∪ range x)
hzJ : z ∈ J
hzI : ∀ (i : ι), z ∉ I i
hι : Nonempty ι
hcl : ∃ C ⊆ insert z ((⋃ (i : ι), I i) ∪ J \ {z}), M.IsCircuit C ∧ z ∈ C
obtain :
  ∀ (C' : Set α) (hC'ss : C' ⊆ insert z ((⋃ (i : ι), I i) ∪ J \ {z})) (hC' : M.IsCircuit C') (hzC' : z ∈ C'),
    ∃ C' ⊆ J ∪ ⋃ (i : ι), I i, M.IsCircuit C' ∧ z ∈ C'
⊢ ∃ C' ⊆ J ∪ ⋃ (i : ι), I i, M.IsCircuit C' ∧ z ∈ C'

Tactic:
obtain ⟨C', hC'ss, hC', hzC'⟩ := hcl
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
ι : Type u_2
J : Set α
x : ι → α
I : ι → Set α
z : α
hxI : ∀ (i : ι), x i ∉ I i
hC : ∀ (i : ι), M.IsCircuit (insert (x i) (I i))
hJx : M.IsCircuit (J ∪ range x)
hzJ : z ∈ J
hzI : ∀ (i : ι), z ∉ I i
hι : Nonempty ι
C' : Set α
hC'ss : C' ⊆ insert z ((⋃ (i : ι), I i) ∪ J \ {z})
hC' : M.IsCircuit C'
hzC' : z ∈ C'
⊢ ∃ C' ⊆ J ∪ ⋃ (i : ι), I i, M.IsCircuit C' ∧ z ∈ C'

Tactic:
⟨C', ?_, hC', hzC'⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
ι : Type u_2
J : Set α
x : ι → α
I : ι → Set α
z : α
hxI : ∀ (i : ι), x i ∉ I i
hC : ∀ (i : ι), M.IsCircuit (insert (x i) (I i))
hJx : M.IsCircuit (J ∪ range x)
hzJ : z ∈ J
hzI : ∀ (i : ι), z ∉ I i
hι : Nonempty ι
C' : Set α
hC'ss : C' ⊆ insert z ((⋃ (i : ι), I i) ∪ J \ {z})
hC' : M.IsCircuit C'
hzC' : z ∈ C'
refine : C' ⊆ J ∪ ⋃ (i : ι), I i
⊢ ∃ C' ⊆ J ∪ ⋃ (i : ι), I i, M.IsCircuit C' ∧ z ∈ C'

Tactic:
refine ⟨C', ?_, hC', hzC'⟩
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
ι : Type u_2
J : Set α
x : ι → α
I : ι → Set α
z : α
hxI : ∀ (i : ι), x i ∉ I i
hC : ∀ (i : ι), M.IsCircuit (insert (x i) (I i))
hJx : M.IsCircuit (J ∪ range x)
hzJ : z ∈ J
hzI : ∀ (i : ι), z ∉ I i
hι : Nonempty ι
C' : Set α
hC'ss : C' ⊆ insert z ((⋃ (i : ι), I i) ∪ J \ {z})
hC' : M.IsCircuit C'
hzC' : z ∈ C'
rwa :
  ∀ (hC'ss : C' ⊆ insert z (J \ {z} ∪ ⋃ (i : ι), I i)) (hC' : M.IsCircuit C') (hzC' : z ∈ C'), C' ⊆ J ∪ ⋃ (i : ι), I i
rwa₁ :
  ∀ (hC'ss : C' ⊆ insert z (J \ {z}) ∪ ⋃ (i : ι), I i) (hC' : M.IsCircuit C') (hzC' : z ∈ C'), C' ⊆ J ∪ ⋃ (i : ι), I i
rwa₂ : ∀ (hC'ss : C' ⊆ insert z J ∪ ⋃ (i : ι), I i) (hC' : M.IsCircuit C') (hzC' : z ∈ C'), C' ⊆ J ∪ ⋃ (i : ι), I i
rwa₃ rwa₄ rwa₅ rwa₆ :
  ∀ (hC'ss : C' ⊆ J ∪ ⋃ (i : ι), I i) (hC' : M.IsCircuit C') (hzC' : z ∈ C'), C' ⊆ J ∪ ⋃ (i : ι), I i
⊢ C' ⊆ J ∪ ⋃ (i : ι), I i

Tactic:
rwa [union_comm, ← insert_union, insert_diff_singleton, insert_eq_of_mem hzJ] at hC'ss

Premises used: Set.insert_eq_of_mem, Set.union_comm, Set.insert_union, Set.insert_diff_singleton
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
ι : Type u_2
J : Set α
x : ι → α
I : ι → Set α
z : α
hxI : ∀ (i : ι), x i ∉ I i
hC : ∀ (i : ι), M.IsCircuit (insert (x i) (I i))
hJx : M.IsCircuit (J ∪ range x)
hzJ : z ∈ J
hzI : ∀ (i : ι), z ∉ I i
hι : Nonempty ι
inr : z ∈ M.closure ((⋃ (i : ι), I i) ∪ J \ {z})
⊢ ∃ C' ⊆ J ∪ ⋃ (i : ι), I i, M.IsCircuit C' ∧ z ∈ C'

Tactic:
suffices hcl : z ∈ M.closure ((⋃ i, I i) ∪ (J \ {z})) by
    rw [mem_closure_iff_exists_isCircuit (by simp [hzI])] at hcl
    obtain ⟨C', hC'ss, hC', hzC'⟩ := hcl
    refine ⟨C', ?_, hC', hzC'⟩
    rwa [union_comm, ← insert_union, insert_diff_singleton, insert_eq_of_mem hzJ] at hC'ss
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
ι : Type u_2
J : Set α
x : ι → α
I : ι → Set α
z : α
hxI : ∀ (i : ι), x i ∉ I i
hC : ∀ (i : ι), M.IsCircuit (insert (x i) (I i))
hJx : M.IsCircuit (J ∪ range x)
hzJ : z ∈ J
hzI : ∀ (i : ι), z ∉ I i
hι : Nonempty ι
i : ι
⊢ M.closure (I i) = M.closure (insert (x i) (I i))

Tactic:
simpa [diff_singleton_eq_self (hxI _)] using (hC i).closure_diff_singleton_eq (x i)

Premises used: Matroid.IsCircuit.closure_diff_singleton_eq, Set.diff_singleton_eq_self
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
ι : Type u_2
J : Set α
x : ι → α
I : ι → Set α
z : α
hxI : ∀ (i : ι), x i ∉ I i
hC : ∀ (i : ι), M.IsCircuit (insert (x i) (I i))
hJx : M.IsCircuit (J ∪ range x)
hzJ : z ∈ J
hzI : ∀ (i : ι), z ∉ I i
hι : Nonempty ι
⊢ ∀ (i : ι), M.closure (I i) = M.closure (insert (x i) (I i))

Tactic:
have hC' (i) : M.closure (I i) = M.closure (insert (x i) (I i)) := by
    simpa [diff_singleton_eq_self (hxI _)] using (hC i).closure_diff_singleton_eq (x i)
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
ι : Type u_2
J : Set α
x : ι → α
I : ι → Set α
z : α
hxI : ∀ (i : ι), x i ∉ I i
hC : ∀ (i : ι), M.IsCircuit (insert (x i) (I i))
hJx : M.IsCircuit (J ∪ range x)
hzJ : z ∈ J
hzI : ∀ (i : ι), z ∉ I i
hι : Nonempty ι
hC' : ∀ (i : ι), M.closure (I i) = M.closure (insert (x i) (I i))
inr : z ∈ M.closure (range x ∪ J \ {z} ∪ ⋃ (i : ι), I i)
⊢ z ∈ M.closure ((⋃ (i : ι), I i) ∪ J \ {z})

Tactic:
rw [closure_union_congr_left <| closure_iUnion_congr _ _ hC',
    iUnion_insert_eq_range_union_iUnion, union_right_comm]

Premises used: Matroid.closure_union_congr_left, Set.union_right_comm, Matroid.closure_iUnion_congr, Set.iUnion_insert_eq_range_union_iUnion
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
ι : Type u_2
J : Set α
x : ι → α
I : ι → Set α
z : α
hxI : ∀ (i : ι), x i ∉ I i
hC : ∀ (i : ι), M.IsCircuit (insert (x i) (I i))
hJx : M.IsCircuit (J ∪ range x)
hzJ : z ∈ J
hzI : ∀ (i : ι), z ∉ I i
hι : Nonempty ι
hC' : ∀ (i : ι), M.closure (I i) = M.closure (insert (x i) (I i))
⊢ z ∈ M.closure (range x ∪ J \ {z} ∪ ⋃ (i : ι), I i)

Tactic:
mem_of_mem_of_subset (hJx.mem_closure_diff_singleton_of_mem (.inl hzJ))
    (M.closure_subset_closure (subset_trans ?_ subset_union_left))

Premises used: Matroid.IsCircuit.mem_closure_diff_singleton_of_mem, subset_trans, Matroid.closure_subset_closure, Set.subset_union_left, Set.mem_of_mem_of_subset, Or.inl