awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
C : Set α
aux : ∀ {α : Type u_1} (M : Matroid α) (C : Set α) (hCE : C ⊆ M.E), M ／ M.closure C = M ／ C ＼ (M.closure C \ C)
hCE : ¬C ⊆ M.E
inr : M ／ M.closure C = M ／ (C ∩ M.E) ＼ (M.closure C \ C)
inr₁ : M ／ M.closure (C ∩ M.E) = M ／ (C ∩ M.E) ＼ (M.closure (C ∩ M.E) \ C)
inr₂ : M ／ (C ∩ M.E) ＼ (M.closure (C ∩ M.E) \ (C ∩ M.E)) = M ／ (C ∩ M.E) ＼ (M.closure (C ∩ M.E) \ C)
inr₃ : M ／ (C ∩ M.E) ＼ (M.closure (C ∩ M.E) \ C ∪ M.closure (C ∩ M.E) \ M.E) = M ／ (C ∩ M.E) ＼ (M.closure (C ∩ M.E) \ C)
inr₄ : M ／ (C ∩ M.E) ＼ (M.closure (C ∩ M.E) \ C ∪ ∅) = M ／ (C ∩ M.E) ＼ (M.closure (C ∩ M.E) \ C)
inr₅ inr₆ : M ／ (C ∩ M.E) ＼ (M.closure (C ∩ M.E) \ C) = M ／ (C ∩ M.E) ＼ (M.closure (C ∩ M.E) \ C)
⊢ M ／ M.closure C = M ／ C ＼ (M.closure C \ C)

Tactic:
rw [← M.contract_inter_ground_eq C, ← closure_inter_ground, aux _ _ inter_subset_right,
      diff_inter, diff_eq_empty.2 (M.closure_subset_ground _), union_empty]

Premises used: Iff.mpr, Set.union_empty, Matroid.closure_subset_ground, Matroid.closure_inter_ground, Matroid.contract_inter_ground_eq, Set.diff_eq_empty, Set.diff_inter, Set.inter_subset_right
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α_1 α : Type u_1
M : Matroid α
C : Set α
hCE : C ⊆ M.E
obtain : ∀ (I : Set α) (hI : M.IsBasis I C), M ／ M.closure C = M ／ C ＼ (M.closure C \ C)
⊢ M ／ M.closure C = M ／ C ＼ (M.closure C \ C)

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

Premises used: Matroid.exists_isBasis
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α_1 α : Type u_1
M : Matroid α
C : Set α
hCE : C ⊆ M.E
I : Set α
hI : M.IsBasis I C
rw : M ／ I ＼ (M.closure C \ I) = M ／ C ＼ (M.closure C \ C)
rw₁ : M ／ I ＼ (M.closure C \ I) = M ／ I ＼ (C \ I) ＼ (M.closure C \ C)
rw₂ : M ／ I ＼ (M.closure C \ I) = M ／ I ＼ (C \ I ∪ M.closure C \ C)
rw₃ : M ／ I ＼ (M.closure C \ I) = M ／ I ＼ (M.closure C \ C ∪ C \ I)
rw₄ rw₅ : M ／ I ＼ (M.closure C \ I) = M ／ I ＼ (M.closure C \ I)
⊢ M ／ M.closure C = M ／ C ＼ (M.closure C \ C)

Tactic:
rw [hI.isBasis_closure_right.contract_eq_contract_delete, hI.contract_eq_contract_delete,
    delete_delete, union_comm, diff_union_diff_cancel (M.subset_closure C) hI.subset]

Premises used: Set.diff_union_diff_cancel, Matroid.subset_closure, Set.union_comm, Matroid.IsBasis.subset, Matroid.IsBasis.isBasis_closure_right, Matroid.IsBasis.contract_eq_contract_delete, Matroid.delete_delete
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
C X : Set α
rw :
  (M ／ C).closure X \ ((M ／ C).closure X \ X) ⊆ M.closure (C ∪ X) \ C ∩ X ∧
    M.closure (C ∪ X) \ C ∩ X ⊆ (M ／ C).closure X
⊢ (M ／ C).closure X = M.closure (X ∪ C) \ C

Tactic:
rw [← diff_union_inter (M.closure (X ∪ C) \ C) X, diff_diff, union_comm C, ← contract_loops_eq,
    union_comm X, ← contract_contract, contract_loops_eq, subset_antisymm_iff, union_subset_iff,
    and_iff_right diff_subset, ← diff_subset_iff]

Premises used: Set.diff_subset, Set.union_subset_iff, Set.diff_subset_iff, Set.union_comm, and_iff_right, Matroid.contract_loops_eq, SDiff.sdiff, Set.diff_diff, subset_antisymm_iff, Set.diff_union_inter, Matroid.closure, Matroid.contract_contract, Union.union
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
C X : Set α
simp : (M ／ C).closure X ∩ X ⊆ M.closure (C ∪ X) \ C ∧ M.closure (C ∪ X) \ C ∩ X ⊆ (M ／ C).closure X
⊢ (M ／ C).closure X \ ((M ／ C).closure X \ X) ⊆ M.closure (C ∪ X) \ C ∩ X ∧
    M.closure (C ∪ X) \ C ∩ X ⊆ (M ／ C).closure X

Tactic:
simp only [sdiff_sdiff_right_self, inf_eq_inter, subset_inter_iff, inter_subset_right, and_true]

Premises used: and_true, Set.subset_inter_iff, Set.inf_eq_inter, sdiff_sdiff_right_self, Set.inter_subset_right
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
C X : Set α
⊢ (M ／ C).closure X ∩ X ⊆ M.closure (C ∪ X) \ C ∧ M.closure (C ∪ X) \ C ∩ X ⊆ (M ／ C).closure X

Tactic:
⟨fun e ⟨he, he'⟩ ↦ ⟨mem_closure_of_mem' _ (.inr he') (mem_ground_of_mem_closure he).1,
    (closure_subset_ground _ _ he).2⟩, fun e ⟨⟨he, heC⟩, he'⟩ ↦
    mem_closure_of_mem' _ he' ⟨M.closure_subset_ground _ he, heC⟩⟩

Premises used: Matroid.closure_subset_ground, Membership.mem, Matroid.mem_closure_of_mem', SDiff.sdiff, _private.0.Matroid.contract_closure_eq.match_3, And.right, And.left, And.intro, Matroid.closure, Union.union, Matroid.contract, Or.inr, Matroid.mem_ground_of_mem_closure, _private.0.Matroid.contract_closure_eq.match_2
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
C X : Set α
⊢ (M ／ C).closure X ∩ X ⊆ M.closure (C ∪ X) \ C ∧ M.closure (C ∪ X) \ C ∩ X ⊆ (M ／ C).closure X

Tactic:
refine ⟨fun e ⟨he, he'⟩ ↦ ⟨mem_closure_of_mem' _ (.inr he') (mem_ground_of_mem_closure he).1,
    (closure_subset_ground _ _ he).2⟩, fun e ⟨⟨he, heC⟩, he'⟩ ↦
    mem_closure_of_mem' _ he' ⟨M.closure_subset_ground _ he, heC⟩⟩
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
X C : Set α
hC : C ⊆ M.E
rw : Disjoint X C → X ⊆ M.E → (M.closure (X ∪ C) \ C = M.E \ C ↔ M.closure (X ∪ C) = M.E ∧ C ⊆ M.E)
⊢ (M ／ C).Spanning X ↔ M.Spanning (X ∪ C) ∧ Disjoint X C

Tactic:
rw [spanning_iff, contract_closure_eq, contract_ground, spanning_iff, union_subset_iff,
    subset_diff, ← and_assoc, and_congr_left_iff, and_comm (a := X ⊆ _), ← and_assoc,
    and_congr_left_iff]

Premises used: Set.union_subset_iff, Matroid.contract_ground, Matroid.contract_closure_eq, Set.subset_diff, Matroid.spanning_iff, and_comm, and_congr_left_iff, and_assoc
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
X C : Set α
hC : C ⊆ M.E
hdj : Disjoint X C
hX : X ⊆ M.E
h : M.closure (X ∪ C) = M.E ∧ C ⊆ M.E
⊢ M.closure (X ∪ C) \ C = M.E \ C

Tactic:
simp [h]
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
X C : Set α
hC : C ⊆ M.E
refine : ∀ (hdj : Disjoint X C) (hX : X ⊆ M.E) (h : M.closure (X ∪ C) \ C = M.E \ C), M.closure (X ∪ C) = M.E
⊢ Disjoint X C → X ⊆ M.E → (M.closure (X ∪ C) \ C = M.E \ C ↔ M.closure (X ∪ C) = M.E ∧ C ⊆ M.E)

Tactic:
refine fun hdj hX ↦ ⟨fun h ↦ ⟨?_, hC⟩, fun h ↦ by simp [h]⟩
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
X C : Set α
hC : C ⊆ M.E
hdj : Disjoint X C
hX : X ⊆ M.E
h : M.closure (X ∪ C) \ C = M.E \ C
rwa : C ∪ M.closure (X ∪ C) \ C = M.E
rwa₁ : C ∪ M.E \ C = M.E
rwa₂ : M.E = M.E
rwa₃ : C ⊆ M.E
rwa₄ : M.E = M.E
rwa₅ rwa₆ rwa₇ : C ⊆ M.E
⊢ M.closure (X ∪ C) = M.E

Tactic:
rwa [← union_diff_cancel (M.subset_closure_of_subset' subset_union_right hC), h,
    union_diff_cancel]

Premises used: Set.subset_union_right, Set.union_diff_cancel, Matroid.subset_closure_of_subset'
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
X C : Set α
rw : M.Spanning (X ∪ C ∩ M.E) → (Disjoint X (C ∩ M.E) ↔ Disjoint X C)
⊢ (M ／ C).Spanning X ↔ M.Spanning (X ∪ C ∩ M.E) ∧ Disjoint X C

Tactic:
rw [← contract_inter_ground_eq, contract_spanning_iff, and_congr_right_iff]

Premises used: and_congr_right_iff, Matroid.contract_spanning_iff, Matroid.contract_inter_ground_eq
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
X C : Set α
⊢ M.Spanning (X ∪ C ∩ M.E) → (Disjoint X (C ∩ M.E) ↔ Disjoint X C)

Tactic:
fun h ↦ ⟨fun hdj ↦ ?_, Disjoint.mono_right inter_subset_left⟩

Premises used: Set.inter_subset_left, Iff.intro, Disjoint.mono_right
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
X C : Set α
refine : ∀ (h : M.Spanning (X ∪ C ∩ M.E)) (hdj : Disjoint X (C ∩ M.E)), Disjoint X C
⊢ M.Spanning (X ∪ C ∩ M.E) → (Disjoint X (C ∩ M.E) ↔ Disjoint X C)

Tactic:
refine fun h ↦ ⟨fun hdj ↦ ?_, Disjoint.mono_right inter_subset_left⟩
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
X C : Set α
h : M.Spanning (X ∪ C ∩ M.E)
hdj : Disjoint X (C ∩ M.E)
rw : Disjoint X (C \ M.E)
⊢ Disjoint X C

Tactic:
rw [← diff_union_inter C M.E, disjoint_union_right, and_iff_left hdj]

Premises used: Set.disjoint_union_right, Matroid.E, and_iff_left, Set.diff_union_inter
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
X C : Set α
h : M.Spanning (X ∪ C ∩ M.E)
hdj : Disjoint X (C ∩ M.E)
⊢ Disjoint X (C \ M.E)

Tactic:
disjoint_sdiff_right.mono_left (subset_union_left.trans h.subset_ground)

Premises used: HasSubset.Subset.trans, Set.subset_union_left, Disjoint.mono_left, Matroid.Spanning.subset_ground, Set.disjoint_sdiff_right
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
X C : Set α
h : M.Spanning (X ∪ C ∩ M.E)
hdj : Disjoint X (C ∩ M.E)
⊢ Disjoint X (C \ M.E)

Tactic:
exact disjoint_sdiff_right.mono_left (subset_union_left.trans h.subset_ground)

Premises used: HasSubset.Subset.trans, Set.subset_union_left, Disjoint.mono_left, Matroid.Spanning.subset_ground, Set.disjoint_sdiff_right
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : M.Spanning X
C : Set α
⊢ X ⊆ M.E

Tactic:
have hXE := hX.subset_ground
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : M.Spanning X
C : Set α
hXE : X ⊆ M.E
rw : M.Spanning (X \ C ∪ C ∩ M.E)
⊢ (M ／ C).Spanning (X \ C)

Tactic:
rw [contract_spanning_iff', and_iff_left disjoint_sdiff_left]

Premises used: and_iff_left, Set.disjoint_sdiff_left, Matroid.contract_spanning_iff'
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : M.Spanning X
C : Set α
hXE : X ⊆ M.E
tauto_set tauto_set₁ tauto_set₂ tauto_set₃ : ∀ (hXE : ∀ x ∈ X, x ∈ M.E), ∀ x ∈ X, True ∧ x ∉ C ∨ x ∈ C ∧ True
⊢ X ⊆ X \ C ∪ C ∩ M.E

Tactic:
tauto_set
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : M.Spanning X
C : Set α
hXE : X ⊆ M.E
tauto_set tauto_set₁ tauto_set₂ tauto_set₃ :
  ∀ (hXE : ∀ x ∈ X, x ∈ M.E) (x : α), x ∈ X ∧ x ∉ C ∨ x ∈ C ∧ x ∈ M.E → x ∈ M.E
⊢ X \ C ∪ C ∩ M.E ⊆ M.E

Tactic:
tauto_set
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : M.Spanning X
C : Set α
hXE : X ⊆ M.E
⊢ M.Spanning (X \ C ∪ C ∩ M.E)

Tactic:
exact hX.superset (by tauto_set) (by tauto_set)

Premises used: Matroid.Spanning.superset
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : M.Spanning X
rw : (M ／ X).loops = M.E \ X ∧ (M ／ X).E = M.E \ X
⊢ M ／ X = loopyOn (M.E \ X)

Tactic:
rw [eq_loopyOn_iff_loops_eq]

Premises used: Matroid.eq_loopyOn_iff_loops_eq
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : M.Spanning X
⊢ (M ／ X).loops = M.E \ X ∧ (M ／ X).E = M.E \ X

Tactic:
simp [hX.closure_eq]

Premises used: Matroid.Spanning.closure_eq
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
K C : Set α
hK : M.IsCircuit K
hC : C ⊂ K
this : ∀ e ∈ K, e ∉ C → M.Indep (K \ {e} ∪ C)
⊢ (M ／ C).IsCircuit (K \ C)

Tactic:
simpa [isCircuit_iff_dep_forall_diff_singleton_indep, diff_diff_comm (s := K) (t := C),
    dep_iff, (hK.ssubset_indep hC).contract_indep_iff, diff_subset_diff_left hK.subset_ground,
    disjoint_sdiff_left, diff_union_of_subset hC.subset, hK.not_indep]

Premises used: Set.diff_subset_diff_left, HasSSubset.SSubset.subset, Set.diff_diff_comm, Matroid.isCircuit_iff_dep_forall_diff_singleton_indep, Matroid.IsCircuit.not_indep, Matroid.IsCircuit.subset_ground, Set.disjoint_sdiff_left, Matroid.Indep.contract_indep_iff, Set.diff_union_of_subset, Matroid.IsCircuit.ssubset_indep, Matroid.dep_iff
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
K C : Set α
hK : M.IsCircuit K
hC : C ⊂ K
suffices : ∀ e ∈ K, e ∉ C → M.Indep (K \ {e} ∪ C)
⊢ (M ／ C).IsCircuit (K \ C)

Tactic:
suffices ∀ e ∈ K, e ∉ C → M.Indep (K \ {e} ∪ C) by
    simpa [isCircuit_iff_dep_forall_diff_singleton_indep, diff_diff_comm (s := K) (t := C),
    dep_iff, (hK.ssubset_indep hC).contract_indep_iff, diff_subset_diff_left hK.subset_ground,
    disjoint_sdiff_left, diff_union_of_subset hC.subset, hK.not_indep]
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
K C : Set α
hK : M.IsCircuit K
hC : C ⊂ K
e : α
heK : e ∈ K
heC : e ∉ C
⊢ K \ {e} ∪ C ⊆ K \ {e}

Tactic:
simp [subset_diff_singleton hC.subset heC]

Premises used: HasSSubset.SSubset.subset, Set.subset_diff_singleton
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
K C : Set α
hK : M.IsCircuit K
hC : C ⊂ K
⊢ ∀ e ∈ K, e ∉ C → M.Indep (K \ {e} ∪ C)

Tactic:
exact fun e heK heC ↦ (hK.diff_singleton_indep heK).subset <| by
    simp [subset_diff_singleton hC.subset heC]

Premises used: Matroid.Indep.subset, Matroid.IsCircuit.diff_singleton_indep
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
e : α
C : Set α
hC : M.IsCircuit C
hnt : C.Nontrivial
heC : e ∈ C
⊢ {e} ⊆ C

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
K C : Set α
hK : M.IsCircuit K
hCK : Disjoint C K
obtain : ∀ (I : Set α) (hI : M.IsBasis I (C ∩ M.E)), (M ／ C).Dep K
⊢ (M ／ C).Dep K

Tactic:
obtain ⟨I, hI⟩ := M.exists_isBasis (C ∩ M.E)

Premises used: Matroid.E, Inter.inter, Matroid.exists_isBasis
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
K C : Set α
hK : M.IsCircuit K
hCK : Disjoint C K
I : Set α
hI : M.IsBasis I (C ∩ M.E)
rw : ¬M.Indep (K ∪ I)
⊢ (M ／ C).Dep K

Tactic:
rw [← contract_inter_ground_eq, Dep, hI.contract_indep_iff,
    and_iff_left (hCK.mono_left inter_subset_left), contract_ground, subset_diff,
    and_iff_left (hCK.symm.mono_right inter_subset_left), and_iff_left hK.subset_ground]

Premises used: Matroid.Dep, Matroid.IsBasis.contract_indep_iff, and_iff_left, Matroid.contract_ground, Set.subset_diff, Set.inter_subset_left, Disjoint.mono_left, Disjoint.symm, Matroid.IsCircuit.subset_ground, Matroid.contract_inter_ground_eq, Disjoint.mono_right
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
K C : Set α
hK : M.IsCircuit K
hCK : Disjoint C K
I : Set α
hI : M.IsBasis I (C ∩ M.E)
⊢ ¬M.Indep (K ∪ I)

Tactic:
fun hi ↦ hK.dep.not_indep (hi.subset subset_union_left)

Premises used: Matroid.Dep.not_indep, Matroid.Indep.subset, Set.subset_union_left, Matroid.IsCircuit.dep, Not
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
K C : Set α
hK : M.IsCircuit K
hCK : Disjoint C K
I : Set α
hI : M.IsBasis I (C ∩ M.E)
⊢ ¬M.Indep (K ∪ I)

Tactic:
exact fun hi ↦ hK.dep.not_indep (hi.subset subset_union_left)

Premises used: Matroid.Dep.not_indep, Matroid.IsCircuit.dep
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
K : Set α
hK : M.IsCircuit K
C : Set α
hKC : ¬K ⊆ C
⊢ C ∩ K ≠ K

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
K : Set α
hK : M.IsCircuit K
C : Set α
hKC : ¬K ⊆ C
⊢ (M ／ (C ∩ K)).IsCircuit (K \ (C ∩ K))

Tactic:
have h' := hK.contract_isCircuit (C := C ∩ K) (inter_subset_right.ssubset_of_ne (by simpa))
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
K : Set α
hK : M.IsCircuit K
C : Set α
hKC : ¬K ⊆ C
h' : (M ／ (C ∩ K)).IsCircuit (K \ (C ∩ K))
⊢ (M ／ (C ∩ K)).IsCircuit (K \ C)

Tactic:
simp only [diff_inter_self_eq_diff] at h'

Premises used: Set.diff_inter_self_eq_diff
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
K : Set α
hK : M.IsCircuit K
C : Set α
hKC : ¬K ⊆ C
h' : (M ／ (C ∩ K)).IsCircuit (K \ C)
⊢ (M ／ (C ∩ K) ／ (C \ K)).Dep (K \ C)

Tactic:
have hwin := h'.contract_dep (C := C \ K) disjoint_sdiff_sdiff
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
K : Set α
hK : M.IsCircuit K
C : Set α
hKC : ¬K ⊆ C
h' : (M ／ (C ∩ K)).IsCircuit (K \ C)
hwin : (M ／ (C ∩ K) ／ (C \ K)).Dep (K \ C)
rwa : ∀ (hwin : (M ／ (C ∩ K ∪ C \ K)).Dep (K \ C)), (M ／ C).Dep (K \ C)
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (hwin : (M ／ C).Dep (K \ C)), (M ／ C).Dep (K \ C)
⊢ (M ／ C).Dep (K \ C)

Tactic:
rwa [contract_contract, inter_union_diff] at hwin

Premises used: Set.inter_union_diff, Matroid.contract_contract
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
K C : Set α
hC : M.IsCircuit C
hK : K.Nonempty
hKC : K ⊆ C
rwa : (C ∩ K).Nonempty
rwa₁ rwa₂ rwa₃ rwa₄ : K.Nonempty
⊢ C \ K ⊂ C

Tactic:
rwa [diff_ssubset_left_iff, inter_eq_self_of_subset_right hKC]

Premises used: Set.diff_ssubset_left_iff, Set.inter_eq_self_of_subset_right
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
K C : Set α
hC : M.IsCircuit C
hK : K.Nonempty
hKC : K ⊆ C
⊢ (M ／ (C \ K)).IsCircuit K

Tactic:
simpa [inter_eq_self_of_subset_right hKC] using hC.contract_isCircuit (C := C \ K) <|
    by rwa [diff_ssubset_left_iff, inter_eq_self_of_subset_right hKC]

Premises used: Matroid.IsCircuit.contract_isCircuit, Set.inter_eq_self_of_subset_right
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
K C : Set α
hC : (M ／ K).IsCircuit C
inr :
  ∀
    (aux :
      ∀ {K : Set α} (hC : (M ／ K).IsCircuit C) (hKi : M.Indep K), ∃ (C' : Set α), M.IsCircuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K)
    (hKi : ¬M.Indep K), ∃ (C' : Set α), M.IsCircuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K
wlog : ∀ {K : Set α} (hC : (M ／ K).IsCircuit C) (hKi : M.Indep K), ∃ (C' : Set α), M.IsCircuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K
⊢ ∃ (C' : Set α), M.IsCircuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K

Tactic:
wlog hKi : M.Indep K generalizing K with aux

Premises used: Matroid.Indep
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
K C : Set α
hC : (M ／ K).IsCircuit C
aux : ∀ {K : Set α} (hC : (M ／ K).IsCircuit C) (hKi : M.Indep K), ∃ (C' : Set α), M.IsCircuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K
hKi : ¬M.Indep K
inr : ∀ (I : Set α) (hI : M.IsBasis' I K), ∃ (C' : Set α), M.IsCircuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K
⊢ ∃ (C' : Set α), M.IsCircuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K

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

Premises used: Matroid.exists_isBasis'
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
K C : Set α
hC : (M ／ K).IsCircuit C
aux : ∀ {K : Set α} (hC : (M ／ K).IsCircuit C) (hKi : M.Indep K), ∃ (C' : Set α), M.IsCircuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K
hKi : ¬M.Indep K
I : Set α
hI : M.IsBasis' I K
⊢ (M ／ I).IsCircuit C ∧ Disjoint C (K \ I)

Tactic:
rw [hI.contract_eq_contract_delete, delete_isCircuit_iff] at hC

Premises used: Matroid.IsBasis'.contract_eq_contract_delete, Matroid.delete_isCircuit_iff
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
K C : Set α
hC : (M ／ K).IsCircuit C
aux : ∀ {K : Set α} (hC : (M ／ K).IsCircuit C) (hKi : M.Indep K), ∃ (C' : Set α), M.IsCircuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K
hKi : ¬M.Indep K
I : Set α
hI : M.IsBasis' I K
hC₁ : (M ／ I).IsCircuit C ∧ Disjoint C (K \ I)
⊢ M.IsBasis' I K

Tactic:
rw [hI.contract_eq_contract_delete, delete_isCircuit_iff] at hC

Premises used: Matroid.IsBasis'.contract_eq_contract_delete, Matroid.delete_isCircuit_iff
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
K C : Set α
aux : ∀ {K : Set α} (hC : (M ／ K).IsCircuit C) (hKi : M.Indep K), ∃ (C' : Set α), M.IsCircuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K
hKi : ¬M.Indep K
I : Set α
hC : (M ／ I).IsCircuit C ∧ Disjoint C (K \ I)
hI : M.IsBasis' I K
inr :
  ∀ (C' : Set α) (hC' : M.IsCircuit C') (hCC' : C ⊆ C') (hC'ss : C' ⊆ C ∪ I),
    ∃ (C' : Set α), M.IsCircuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K
⊢ ∃ (C' : Set α), M.IsCircuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K

Tactic:
obtain ⟨C', hC', hCC', hC'ss⟩ := aux hC.1 hI.indep

Premises used: Matroid.IsBasis'.indep, And.left
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
K C : Set α
aux : ∀ {K : Set α} (hC : (M ／ K).IsCircuit C) (hKi : M.Indep K), ∃ (C' : Set α), M.IsCircuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K
hKi : ¬M.Indep K
I : Set α
hC : (M ／ I).IsCircuit C ∧ Disjoint C (K \ I)
hI : M.IsBasis' I K
C' : Set α
hC' : M.IsCircuit C'
hCC' : C ⊆ C'
hC'ss : C' ⊆ C ∪ I
⊢ ∃ (C' : Set α), M.IsCircuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K

Tactic:
⟨C', hC', hCC', hC'ss.trans (union_subset_union_right _ hI.subset)⟩

Premises used: Set.union_subset_union_right, HasSubset.Subset.trans, And.intro, Exists.intro, Matroid.IsBasis'.subset
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
K C : Set α
aux : ∀ {K : Set α} (hC : (M ／ K).IsCircuit C) (hKi : M.Indep K), ∃ (C' : Set α), M.IsCircuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K
hKi : ¬M.Indep K
I : Set α
hC : (M ／ I).IsCircuit C ∧ Disjoint C (K \ I)
hI : M.IsBasis' I K
C' : Set α
hC' : M.IsCircuit C'
hCC' : C ⊆ C'
hC'ss : C' ⊆ C ∪ I
⊢ ∃ (C' : Set α), M.IsCircuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K

Tactic:
exact ⟨C', hC', hCC', hC'ss.trans (union_subset_union_right _ hI.subset)⟩
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
K_1 C K : Set α
hC : (M ／ K).IsCircuit C
hKi : M.Indep K
⊢ C ⊆ M.E

Tactic:
obtain ⟨hCE : C ⊆ M.E, hCK : Disjoint C K⟩ := subset_diff.1 hC.subset_ground

Premises used: Matroid.E, Disjoint, Set.subset_diff, Matroid.IsCircuit.subset_ground, Iff.mp
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
K_1 C K : Set α
hC : (M ／ K).IsCircuit C
hKi : M.Indep K
hCE : C ⊆ M.E
⊢ Disjoint C K

Tactic:
obtain ⟨hCE : C ⊆ M.E, hCK : Disjoint C K⟩ := subset_diff.1 hC.subset_ground

Premises used: Matroid.E, Disjoint, Set.subset_diff, Matroid.IsCircuit.subset_ground, Iff.mp
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
K_1 C K : Set α
hC : (M ／ K).IsCircuit C
hKi : M.Indep K
hCE : C ⊆ M.E
hCK : Disjoint C K
obtain :
  ∀ (C' : Set α) (hC'ss : C' ⊆ C ∪ K) (hC' : M.IsCircuit C'), ∃ (C' : Set α), M.IsCircuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K
⊢ ∃ (C' : Set α), M.IsCircuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K

Tactic:
obtain ⟨C', hC'ss, hC'⟩ := (hKi.contract_dep_iff.1 hC.dep).2.exists_isCircuit_subset

Premises used: Matroid.Indep.contract_dep_iff, Matroid.Dep.exists_isCircuit_subset, And.right, Iff.mp, Matroid.IsCircuit.dep
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
K_1 C K : Set α
hC : (M ／ K).IsCircuit C
hKi : M.Indep K
hCE : C ⊆ M.E
hCK : Disjoint C K
C' : Set α
hC'ss : C' ⊆ C ∪ K
hC' : M.IsCircuit C'
⊢ ∃ (C' : Set α), M.IsCircuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K

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

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
K_1 C K : Set α
hC : (M ／ K).IsCircuit C
hKi : M.Indep K
hCE : C ⊆ M.E
hCK : Disjoint C K
C' : Set α
hC'ss : C' ⊆ C ∪ K
hC' : M.IsCircuit C'
refine : C ⊆ C'
⊢ ∃ (C' : Set α), M.IsCircuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K

Tactic:
refine ⟨C', hC', ?_, hC'ss⟩
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
K_1 C K : Set α
hC : (M ／ K).IsCircuit C
hKi : M.Indep K
hCE : C ⊆ M.E
hCK : Disjoint C K
C' : Set α
hC'ss : C' ⊆ C ∪ K
hC' : M.IsCircuit C'
rw : M.Dep (C' \ K ∪ K)
⊢ (M ／ K).Dep (C' \ K)

Tactic:
rw [hKi.contract_dep_iff, and_iff_right disjoint_sdiff_left]

Premises used: Matroid.Indep.contract_dep_iff, and_iff_right, Set.disjoint_sdiff_left
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
K_1 C K : Set α
hC : (M ／ K).IsCircuit C
hKi : M.Indep K
hCE : C ⊆ M.E
hCK : Disjoint C K
C' : Set α
hC'ss : C' ⊆ C ∪ K
hC' : M.IsCircuit C'
⊢ C' ⊆ C' \ K ∪ K

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
K_1 C K : Set α
hC : (M ／ K).IsCircuit C
hKi : M.Indep K
hCE : C ⊆ M.E
hCK : Disjoint C K
C' : Set α
hC'ss : C' ⊆ C ∪ K
hC' : M.IsCircuit C'
⊢ M.Dep (C' \ K ∪ K)

Tactic:
refine hC'.dep.superset (by simp)

Premises used: Matroid.Dep.superset, Matroid.IsCircuit.dep