awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I J X : Set α
hI : M.IsBasis' I X
rw : M.Indep (J \ X ∪ I) ∧ Disjoint X (J \ X) ↔ M.Indep (J \ X ∪ I)
rw₁ rw₂ : M.Indep (J \ X ∪ I) ↔ M.Indep (J \ X ∪ I)
⊢ (M ／ X).Indep (J \ X) ↔ M.Indep (J \ X ∪ I)

Tactic:
rw [hI.contract_indep_iff, and_iff_left disjoint_sdiff_right]

Premises used: and_iff_left, Set.disjoint_sdiff_right, Matroid.IsBasis'.contract_indep_iff
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I J X C : Set α
h : M.IsBasis I X
hJC : M.IsBasis' J C
h_ind : M.Indep (I \ C ∪ J)
⊢ I ⊆ X

Tactic:
have hIX := h.subset
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I J X C : Set α
h : M.IsBasis I X
hJC : M.IsBasis' J C
h_ind : M.Indep (I \ C ∪ J)
hIX : I ⊆ X
⊢ J ⊆ C

Tactic:
have hJCss := hJC.subset
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I J X C : Set α
h : M.IsBasis I X
hJC : M.IsBasis' J C
h_ind : M.Indep (I \ C ∪ J)
hIX : I ⊆ X
hJCss : J ⊆ C
rw : (M ／ J).IsBasis (I \ C) (X \ C) ∧ Disjoint (X \ C) (C \ J)
⊢ (M ／ C).IsBasis (I \ C) (X \ C)

Tactic:
rw [hJC.contract_eq_contract_delete, delete_isBasis_iff]

Premises used: Matroid.IsBasis'.contract_eq_contract_delete, Matroid.delete_isBasis_iff
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I J X C : Set α
h : M.IsBasis I X
hJC : M.IsBasis' J C
h_ind : M.Indep (I \ C ∪ J)
hIX : I ⊆ X
hJCss : J ⊆ C
⊢ (M ／ J).IsBasis (I \ C) (X \ C) ∧ Disjoint (X \ C) (C \ J)

Tactic:
⟨contract_isBasis_union_union (h_ind.isBasis_of_subset_of_subset_closure ?_ ?_) ?_ ?_, ?_⟩

Premises used: Matroid.IsBasis.contract_isBasis_union_union, And.intro, Matroid.Indep.isBasis_of_subset_of_subset_closure
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I J X C : Set α
h : M.IsBasis I X
hJC : M.IsBasis' J C
h_ind : M.Indep (I \ C ∪ J)
hIX : I ⊆ X
hJCss : J ⊆ C
refine_1 : I \ C ∪ J ⊆ X \ C ∪ J
refine_2 : X \ C ∪ J ⊆ M.closure (I \ C ∪ J)
refine_3 : Disjoint (I \ C) J
refine_4 : Disjoint (X \ C) J
refine_5 : Disjoint (X \ C) (C \ J)
⊢ (M ／ J).IsBasis (I \ C) (X \ C) ∧ Disjoint (X \ C) (C \ J)

Tactic:
refine ⟨contract_isBasis_union_union (h_ind.isBasis_of_subset_of_subset_closure ?_ ?_) ?_ ?_, ?_⟩
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I J X C : Set α
h : M.IsBasis I X
hJC : M.IsBasis' J C
h_ind : M.Indep (I \ C ∪ J)
hIX : I ⊆ X
hJCss : J ⊆ C
refine_2 : X \ C ∪ J ⊆ M.closure (X ∪ C)
⊢ X \ C ∪ J ⊆ M.closure (I \ C ∪ J)

Tactic:
rw [closure_union_congr_right hJC.closure_eq_closure, diff_union_self,
      closure_union_congr_left h.closure_eq_closure]

Premises used: Matroid.closure_union_congr_right, Matroid.IsBasis'.closure_eq_closure, Matroid.closure_union_congr_left, Set.diff_union_self, Matroid.IsBasis.closure_eq_closure
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I J X C : Set α
h : M.IsBasis I X
hJC : M.IsBasis' J C
h_ind : M.Indep (I \ C ∪ J)
hIX : I ⊆ X
hJCss : J ⊆ C
tauto_set tauto_set₁ tauto_set₂ tauto_set₃ :
  ∀ (h_ind : M.Indep (I ∩ Cᶜ ∪ J)) (hIX : ∀ x ∈ I, x ∈ X) (hJCss : ∀ x ∈ J, x ∈ C) (x : α),
    x ∈ X ∧ x ∉ C ∨ x ∈ J → x ∈ X ∨ x ∈ C
⊢ X \ C ∪ J ⊆ X ∪ C

Tactic:
tauto_set
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I J X C : Set α
h : M.IsBasis I X
hJC : M.IsBasis' J C
h_ind : M.Indep (I \ C ∪ J)
hIX : I ⊆ X
hJCss : J ⊆ C
⊢ X \ C ∪ J ⊆ M.closure (X ∪ C)

Tactic:
exact subset_closure_of_subset' _ (by tauto_set)
      (union_subset (diff_subset.trans h.subset_ground) hJC.indep.subset_ground)

Premises used: Set.diff_subset, Matroid.IsBasis.subset_ground, HasSubset.Subset.trans, Matroid.IsBasis'.indep, Set.union_subset, Matroid.Indep.subset_ground, Matroid.subset_closure_of_subset'
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I J X C : Set α
h : M.IsBasis I X
hJC : M.IsBasis' J C
h_ind : M.Indep (I \ C ∪ J)
hIX : I ⊆ X
hJCss : J ⊆ C
refine_3 refine_3₁ refine_3₂ refine_3₃ :
  ∀ (h_ind : M.Indep (I ∩ Cᶜ ∪ J)) (hIX : ∀ x ∈ I, x ∈ X) (hJCss : ∀ x ∈ J, x ∈ C) (x : α),
    (x ∈ I ∧ x ∉ C) ∧ x ∈ J → Membership.mem (γ := Set α) ∅ x
⊢ Disjoint (I \ C) J

Tactic:
tauto_set
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I J X C : Set α
h : M.IsBasis I X
hJC : M.IsBasis' J C
h_ind : M.Indep (I \ C ∪ J)
hIX : I ⊆ X
hJCss : J ⊆ C
refine_4 refine_4₁ refine_4₂ refine_4₃ :
  ∀ (h_ind : M.Indep (I ∩ Cᶜ ∪ J)) (hIX : ∀ x ∈ I, x ∈ X) (hJCss : ∀ x ∈ J, x ∈ C) (x : α),
    (x ∈ X ∧ x ∉ C) ∧ x ∈ J → Membership.mem (γ := Set α) ∅ x
⊢ Disjoint (X \ C) J

Tactic:
tauto_set
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I J X C : Set α
h : M.IsBasis I X
hJC : M.IsBasis' J C
h_ind : M.Indep (I \ C ∪ J)
hIX : I ⊆ X
hJCss : J ⊆ C
refine_5 refine_5₁ refine_5₂ refine_5₃ :
  ∀ (h_ind : M.Indep (I ∩ Cᶜ ∪ J)) (hIX : ∀ x ∈ I, x ∈ X) (hJCss : ∀ x ∈ J, x ∈ C) (x : α),
    (x ∈ X ∧ x ∉ C) ∧ x ∈ C ∧ x ∉ J → Membership.mem (γ := Set α) ∅ x
⊢ Disjoint (X \ C) (C \ J)

Tactic:
tauto_set
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I J X C : Set α
h : M.IsBasis I X
hJC : M.IsBasis' J C
h_ind : M.Indep (I \ C ∪ J)
hIX : I ⊆ X
hJCss : J ⊆ C
refine_1 refine_1₁ refine_1₂ refine_1₃ :
  ∀ (h_ind : M.Indep (I ∩ Cᶜ ∪ J)) (hIX : ∀ x ∈ I, x ∈ X) (hJCss : ∀ x ∈ J, x ∈ C) (x : α),
    x ∈ I ∧ x ∉ C ∨ x ∈ J → x ∈ X ∧ x ∉ C ∨ x ∈ J
⊢ I \ C ∪ J ⊆ X \ C ∪ J

Tactic:
tauto_set
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I J X C : Set α
h : M.IsBasis' I X
hJC : M.IsBasis' J C
h_ind : M.Indep (I \ C ∪ J)
rw : (M ／ C).IsBasis (I \ C) ((X ∩ M.E) \ C)
⊢ (M ／ C).IsBasis' (I \ C) (X \ C)

Tactic:
rw [isBasis'_iff_isBasis_inter_ground, contract_ground, ← diff_inter_distrib_right]

Premises used: Matroid.contract_ground, Matroid.isBasis'_iff_isBasis_inter_ground, Set.diff_inter_distrib_right
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I J X C : Set α
h : M.IsBasis' I X
hJC : M.IsBasis' J C
h_ind : M.Indep (I \ C ∪ J)
⊢ (M ／ C).IsBasis (I \ C) ((X ∩ M.E) \ C)

Tactic:
h.isBasis_inter_ground.contract_isBasis_of_isBasis' hJC h_ind

Premises used: Matroid.IsBasis'.isBasis_inter_ground, Matroid.IsBasis.contract_isBasis_of_isBasis'
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I J X C : Set α
h : M.IsBasis' I X
hJC : M.IsBasis' J C
h_ind : M.Indep (I \ C ∪ J)
⊢ (M ／ C).IsBasis (I \ C) ((X ∩ M.E) \ C)

Tactic:
exact h.isBasis_inter_ground.contract_isBasis_of_isBasis' hJC h_ind

Premises used: Matroid.IsBasis'.isBasis_inter_ground, Matroid.IsBasis.contract_isBasis_of_isBasis'
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I J X C : Set α
h : M.IsBasis I X
hJC : M.IsBasis J C
h_ind : M.Indep (I \ C ∪ J)
⊢ (M ／ C).IsBasis (I \ C) (X \ C)

Tactic:
h.contract_isBasis_of_isBasis' hJC.isBasis' h_ind

Premises used: Matroid.IsBasis.isBasis', Matroid.IsBasis.contract_isBasis_of_isBasis'
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I J X C : Set α
h : M.IsBasis I X
hJC : M.IsBasis J C
hdj : Disjoint C X
h_ind : M.Indep (I ∪ J)
⊢ ∀ (h_ind : M.Indep (I \ C ∪ J)), (M ／ C).IsBasis (I \ C) (X \ C)

Tactic:
have h' := h.contract_isBasis hJC
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I J X C : Set α
h : M.IsBasis I X
hJC : M.IsBasis J C
hdj : Disjoint C X
h_ind : M.Indep (I ∪ J)
h' : ∀ (h_ind : M.Indep (I \ C ∪ J)), (M ／ C).IsBasis (I \ C) (X \ C)
rwa : ∀ (h' : ∀ (h_ind : M.Indep (I ∪ J)), (M ／ C).IsBasis I (X \ C)), (M ／ C).IsBasis I X
rwa₁ : ∀ (h' : ∀ (h_ind : M.Indep (I ∪ J)), (M ／ C).IsBasis I X), (M ／ C).IsBasis I X
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (h' : (M ／ C).IsBasis I X), (M ／ C).IsBasis I X
⊢ (M ／ C).IsBasis I X

Tactic:
rwa [(hdj.mono_right h.subset).sdiff_eq_right, hdj.sdiff_eq_right, imp_iff_right h_ind] at h'

Premises used: Disjoint.sdiff_eq_right, imp_iff_right, Matroid.IsBasis.subset, Disjoint.mono_right
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I J X : Set α
h : M.IsBasis' I X
h_ind : M.Indep (I ∪ J)
⊢ M.Indep (I \ J ∪ J)

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I J X : Set α
h : M.IsBasis I X
h_ind : M.Indep (I ∪ J)
⊢ M.Indep (I \ J ∪ J)

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I J X : Set α
h : M.IsBasis I X
hdj : Disjoint J X
h_ind : M.Indep (I ∪ J)
rw : (M ／ J).IsBasis (I \ J) (X \ J)
⊢ (M ／ J).IsBasis I X

Tactic:
rw [← hdj.sdiff_eq_right, ← (hdj.mono_right h.subset).sdiff_eq_right]

Premises used: Disjoint.sdiff_eq_right, Matroid.IsBasis.subset, Disjoint.mono_right
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I J X : Set α
h : M.IsBasis I X
hdj : Disjoint J X
h_ind : M.Indep (I ∪ J)
⊢ (M ／ J).IsBasis (I \ J) (X \ J)

Tactic:
h.contract_isBasis_of_indep h_ind

Premises used: Matroid.IsBasis.contract_isBasis_of_indep
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I J X : Set α
h : M.IsBasis I X
hdj : Disjoint J X
h_ind : M.Indep (I ∪ J)
⊢ (M ／ J).IsBasis (I \ J) (X \ J)

Tactic:
exact h.contract_isBasis_of_indep h_ind

Premises used: Matroid.IsBasis.contract_isBasis_of_indep
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I C : Set α
hI : (M ／ C).Indep I
⊢ M.Indep I

Tactic:
((M.exists_isBasis' C).choose_spec.contract_indep_iff.1 hI).1.subset subset_union_left

Premises used: Exists.choose_spec, Matroid.Indep.subset, Set.subset_union_left, And.left, Iff.mp, Matroid.exists_isBasis', Matroid.IsBasis'.contract_indep_iff
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
X C : Set α
h : (M ／ C).Dep X
hC : C ⊆ M.E
rw : ¬M.Indep (C ∪ X)
⊢ M.Dep (C ∪ X)

Tactic:
rw [Dep, and_iff_left (union_subset hC (h.subset_ground.trans diff_subset))]

Premises used: Matroid.Dep, Set.diff_subset, Matroid.Dep.subset_ground, and_iff_left, HasSubset.Subset.trans, Set.union_subset
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
X C : Set α
h : (M ／ C).Dep X
hC : C ⊆ M.E
hi : M.Indep (C ∪ X)
⊢ ¬Disjoint X C ∧ X ⊆ (M ／ C).E

Tactic:
rw [Dep, (hi.subset subset_union_left).contract_indep_iff, union_comm,
    and_iff_left hi] at h

Premises used: Matroid.Dep, and_iff_left, Matroid.Indep.subset, Set.union_comm, Set.subset_union_left, Matroid.Indep.contract_indep_iff
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
X C : Set α
h : (M ／ C).Dep X
hC : C ⊆ M.E
hi : M.Indep (C ∪ X)
h₁ : ¬Disjoint X C ∧ X ⊆ (M ／ C).E
⊢ C ⊆ M.E

Tactic:
rw [Dep, (hi.subset subset_union_left).contract_indep_iff, union_comm,
    and_iff_left hi] at h

Premises used: Matroid.Dep, and_iff_left, Matroid.Indep.subset, Set.union_comm, Set.subset_union_left, Matroid.Indep.contract_indep_iff
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
X C : Set α
h : (M ／ C).Dep X
hC : C ⊆ M.E
hi : M.Indep (C ∪ X)
h₁ : ¬Disjoint X C ∧ X ⊆ (M ／ C).E
hC₁ : C ⊆ M.E
⊢ M.Indep (C ∪ X)

Tactic:
rw [Dep, (hi.subset subset_union_left).contract_indep_iff, union_comm,
    and_iff_left hi] at h

Premises used: Matroid.Dep, and_iff_left, Matroid.Indep.subset, Set.union_comm, Set.subset_union_left, Matroid.Indep.contract_indep_iff
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
X C : Set α
h : ¬Disjoint X C ∧ X ⊆ (M ／ C).E
hC : C ⊆ M.E
hi : M.Indep (C ∪ X)
⊢ False

Tactic:
h.1 (subset_diff.1 h.2).2

Premises used: Set.subset_diff, And.right, And.left, Iff.mp
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
X C : Set α
h : ¬Disjoint X C ∧ X ⊆ (M ／ C).E
hC : C ⊆ M.E
hi : M.Indep (C ∪ X)
⊢ False

Tactic:
exact h.1 (subset_diff.1 h.2).2

Premises used: Set.subset_diff, And.right, And.left, Iff.mp
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M M' N : Matroid α
e f : α
I J R D B X Y Z K C C₁ C₂ : Set α
inst : M.Finite
⊢ (M✶ ＼ C)✶.Finite

Tactic:
infer_instance
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M M' N : Matroid α
e f : α
I J R D B X Y Z K C C₁ C₂ : Set α
inst : M.RankFinite
⊢ (M ／ C).RankFinite

Tactic:
let ⟨B, hB⟩ := (M ／ C).exists_isBase
  ⟨B, hB, hB.indep.of_contract.finite⟩

Premises used: Matroid.Indep.finite, Matroid.RankFinite.mk, Matroid.exists_isBase, Matroid.Indep.of_contract, And.intro, Exists.intro, Matroid.IsBase.indep, _private.0.Matroid.contract_rankFinite.match_1, Matroid.RankFinite, Matroid.contract
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M M' N : Matroid α
e f : α
I J R D B X Y Z K C C₁ C₂ : Set α
inst : M.Finitary
obtain : ∀ (J : Set α) (hJ : M.IsBasis' J C), (M ／ C).Finitary
⊢ (M ／ C).Finitary

Tactic:
obtain ⟨J, hJ⟩ := M.exists_isBasis' C

Premises used: Matroid.exists_isBasis'
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M M' N : Matroid α
e f : α
I J_1 R D B X Y Z K C C₁ C₂ : Set α
inst : M.Finitary
J : Set α
hJ : M.IsBasis' J C
this : (M ／ J).Finitary
rw : (M ／ J ＼ (C \ J)).Finitary
⊢ (M ／ C).Finitary

Tactic:
rw [hJ.contract_eq_contract_delete]

Premises used: Matroid.IsBasis'.contract_eq_contract_delete
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M M' N : Matroid α
e f : α
I J_1 R D B X Y Z K C C₁ C₂ : Set α
inst : M.Finitary
J : Set α
hJ : M.IsBasis' J C
this : (M ／ J).Finitary
⊢ (M ／ J ＼ (C \ J)).Finitary

Tactic:
infer_instance
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M M' N : Matroid α
e f : α
I J_1 R D B X Y Z K C C₁ C₂ : Set α
inst : M.Finitary
J : Set α
hJ : M.IsBasis' J C
suffices : (M ／ J).Finitary
⊢ (M ／ C).Finitary

Tactic:
suffices (M ／ J).Finitary by
    rw [hJ.contract_eq_contract_delete]
    infer_instance
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M M' N : Matroid α
e_1 f : α
I_1 J_1 R D B X Y Z K C C₁ C₂ : Set α
inst : M.Finitary
J : Set α
hJ : M.IsBasis' J C
I : Set α
hI : ∀ J_2 ⊆ I, J_2.Finite → (M ／ J).Indep J_2
e : α
heI : e ∈ I
⊢ {e} ⊆ I

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M M' N : Matroid α
e_1 f : α
I_1 J_1 R D B X Y Z K C C₁ C₂ : Set α
inst : M.Finitary
J : Set α
hJ : M.IsBasis' J C
I : Set α
hI : ∀ J_2 ⊆ I, J_2.Finite → (M ／ J).Indep J_2
e : α
heI : e ∈ I
⊢ Set.Finite (α := α) {e}

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M M' N : Matroid α
e f : α
I_1 J_1 R D B X Y Z K_1 C C₁ C₂ : Set α
inst : M.Finitary
J : Set α
hJ : M.IsBasis' J C
I : Set α
hI : ∀ J_2 ⊆ I, J_2.Finite → (M ／ J).Indep J_2
K : Set α
hK : K ⊆ I ∪ J
hKfin : K.Finite
tauto_set tauto_set₁ tauto_set₂ tauto_set₃ :
  ∀ (hI : ∀ (J_2 : Set α), (∀ x ∈ J_2, x ∈ I) → J_2.Finite → (M ／ J).Indep J_2) (hK : ∀ x ∈ K, x ∈ I ∨ x ∈ J)
    (hKfin : K.Finite), ∀ x ∈ K, True ∧ x ∈ I ∨ x ∈ J
⊢ K ⊆ K ∩ I ∪ J

Tactic:
tauto_set
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M M' N : Matroid α
e f : α
I J_1 R D B X Y Z K C C₁ C₂ : Set α
inst : M.Finitary
J : Set α
hJ : M.IsBasis' J C
⊢ (M ／ J).Finitary

Tactic:
exact ⟨fun I hI ↦ hJ.indep.contract_indep_iff.2  ⟨disjoint_left.2 fun e heI ↦
    ((hI {e} (by simpa) (by simp)).subset_ground rfl).2,
    indep_of_forall_finite_subset_indep _ fun K hK hKfin ↦
      (hJ.indep.contract_indep_iff.1 <| hI (K ∩ I)
      inter_subset_right (hKfin.inter_of_left _)).2.subset (by tauto_set)⟩⟩
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.loops
⊢ M ／ X = M ＼ X

Tactic:
simp [(empty_isBasis_iff.2 hX).contract_eq_contract_delete]

Premises used: Iff.mpr, Matroid.empty_isBasis_iff, Matroid.IsBasis.contract_eq_contract_delete
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.coloops
rw : (M ／ X)✶ = (M ＼ X)✶
rw₁ : (M ／ X)✶ = M✶ ／ X
rw₂ : (M ／ X)✶ = M✶ ＼ X
rw₃ rw₄ : M✶ ＼ X = M✶ ＼ X
⊢ M ／ X = M ＼ X

Tactic:
rw [← dual_inj, dual_delete, contract_eq_delete_of_subset_loops hX, dual_contract]

Premises used: Matroid.contract_eq_delete_of_subset_loops, Matroid.dual_contract, Matroid.dual_inj, Matroid.dual_delete
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
e : α
C : Set α
obtain : ∀ (I : Set α) (hI : M.IsBasis' I C), (M ／ C).IsLoop e ↔ e ∈ M.closure C ∧ e ∉ C
⊢ (M ／ C).IsLoop e ↔ e ∈ M.closure C ∧ e ∉ C

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

Premises used: Matroid.exists_isBasis'
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
e : α
C I : Set α
hI : M.IsBasis' I C
rw : (Disjoint {e} I ∧ e ∈ M.closure C \ I) ∧ e ∉ C \ I ↔ e ∈ M.closure C ∧ e ∉ C
⊢ (M ／ C).IsLoop e ↔ e ∈ M.closure C ∧ e ∉ C

Tactic:
rw [hI.contract_eq_contract_delete, delete_isLoop_iff, ← singleton_dep,
    hI.indep.contract_dep_iff, singleton_union, hI.indep.insert_dep_iff, hI.closure_eq_closure]

Premises used: Matroid.IsBasis'.contract_eq_contract_delete, Matroid.IsBasis'.closure_eq_closure, Matroid.Indep.contract_dep_iff, Set.singleton_union, Matroid.Indep.insert_dep_iff, Matroid.IsBasis'.indep, Matroid.delete_isLoop_iff, Matroid.singleton_dep
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
e : α
C I : Set α
hI : M.IsBasis' I C
pos : ∀ (heI : e ∈ I), (Disjoint {e} I ∧ e ∈ M.closure C \ I) ∧ e ∉ C \ I ↔ e ∈ M.closure C ∧ e ∉ C
neg : ∀ (heI : e ∉ I), (Disjoint {e} I ∧ e ∈ M.closure C \ I) ∧ e ∉ C \ I ↔ e ∈ M.closure C ∧ e ∉ C
⊢ (Disjoint {e} I ∧ e ∈ M.closure C \ I) ∧ e ∉ C \ I ↔ e ∈ M.closure C ∧ e ∉ C

Tactic:
by_cases heI : e ∈ I
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
e : α
C I : Set α
hI : M.IsBasis' I C
heI : e ∈ I
⊢ (Disjoint {e} I ∧ e ∈ M.closure C \ I) ∧ e ∉ C \ I ↔ e ∈ M.closure C ∧ e ∉ C

Tactic:
simp [heI, hI.subset heI]

Premises used: Matroid.IsBasis'.subset
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
e : α
C I : Set α
hI : M.IsBasis' I C
heI : e ∉ I
⊢ (Disjoint {e} I ∧ e ∈ M.closure C \ I) ∧ e ∉ C \ I ↔ e ∈ M.closure C ∧ e ∉ C

Tactic:
simp [heI, and_comm]

Premises used: and_comm
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
C : Set α
⊢ (M ／ C).loops = M.closure C \ C

Tactic:
simp [Set.ext_iff, ← isLoop_iff, contract_isLoop_iff_mem_closure]

Premises used: Matroid.isLoop_iff, Set.ext_iff, Matroid.contract_isLoop_iff_mem_closure
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
C : Set α
rw : (M✶ ＼ C)✶.coloops = M.coloops \ C
rw₁ : (M✶ ＼ C).loops = M.coloops \ C
rw₂ : M✶.loops \ C = M.coloops \ C
rw₃ rw₄ : M.coloops \ C = M.coloops \ C
⊢ (M ／ C).coloops = M.coloops \ C

Tactic:
rw [← dual_delete_dual, dual_coloops, delete_loops_eq, dual_loops]

Premises used: Matroid.dual_loops, Matroid.dual_delete_dual, Matroid.delete_loops_eq, Matroid.dual_coloops
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
e : α
C : Set α
⊢ (M ／ C).IsColoop e ↔ M.IsColoop e ∧ e ∉ C

Tactic:
simp [isColoop_iff_mem_coloops]

Premises used: Matroid.isColoop_iff_mem_coloops
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
e : α
C : Set α
h : (M ／ C).IsNonloop e
rw : ∀ (h : (M ／ C).Indep {e}), M.Indep {e}
⊢ M.IsNonloop e

Tactic:
rw [← indep_singleton] at h ⊢

Premises used: Matroid.indep_singleton
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
e : α
C : Set α
h : (M ／ C).Indep {e}
⊢ M.Indep {e}

Tactic:
h.of_contract

Premises used: Matroid.Indep.of_contract
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
e : α
C : Set α
h : (M ／ C).Indep {e}
⊢ M.Indep {e}

Tactic:
exact h.of_contract

Premises used: Matroid.Indep.of_contract
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
e : α
C : Set α
rw : e ∈ (M.E \ C) \ (M.closure C \ C) ↔ e ∈ M.E \ M.closure C
⊢ (M ／ C).IsNonloop e ↔ e ∈ M.E \ M.closure C

Tactic:
rw [isNonloop_iff_mem_compl_loops, contract_ground, contract_loops_eq]

Premises used: Matroid.contract_ground, Matroid.contract_loops_eq, Matroid.isNonloop_iff_mem_compl_loops
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
e : α
C : Set α
⊢ e ∈ (M.E \ C) \ (M.closure C \ C) ↔ e ∈ M.E \ M.closure C

Tactic:
⟨fun ⟨he,heC⟩ ↦ ⟨he.1, fun h ↦ heC ⟨h, he.2⟩⟩,
    fun h ↦ ⟨⟨h.1, fun heC ↦ h.2 ?_⟩, fun h' ↦ h.2 h'.1⟩⟩

Premises used: _private.0.Matroid.contract_isNonloop_iff.match_1, Matroid.E, Membership.mem, SDiff.sdiff, And.right, And.left, And.intro, Iff.intro, Matroid.closure
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
e : α
C : Set α
refine : ∀ (h : e ∈ M.E \ M.closure C) (heC : e ∈ C), e ∈ M.closure C
⊢ e ∈ (M.E \ C) \ (M.closure C \ C) ↔ e ∈ M.E \ M.closure C

Tactic:
refine ⟨fun ⟨he,heC⟩ ↦ ⟨he.1, fun h ↦ heC ⟨h, he.2⟩⟩,
    fun h ↦ ⟨⟨h.1, fun heC ↦ h.2 ?_⟩, fun h' ↦ h.2 h'.1⟩⟩
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
e : α
C : Set α
h : e ∈ M.E \ M.closure C
heC : e ∈ C
rw : e ∈ M.closure (C ∩ M.E)
⊢ e ∈ M.closure C

Tactic:
rw [← closure_inter_ground]

Premises used: Matroid.closure_inter_ground
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
e : α
C : Set α
h : e ∈ M.E \ M.closure C
heC : e ∈ C
⊢ e ∈ M.closure (C ∩ M.E)

Tactic:
(M.subset_closure (C ∩ M.E)) ⟨heC, h.1⟩

Premises used: Matroid.E, Matroid.subset_closure, Inter.inter, And.left, And.intro
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
e : α
C : Set α
h : e ∈ M.E \ M.closure C
heC : e ∈ C
⊢ e ∈ M.closure (C ∩ M.E)

Tactic:
exact (M.subset_closure (C ∩ M.E)) ⟨heC, h.1⟩

Premises used: Matroid.E, Matroid.subset_closure, Inter.inter, And.left, And.intro
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hIX : M.IsBasis I X
rw : X ⊆ M.closure I
⊢ X \ I ⊆ (M ／ I).loops

Tactic:
rw [diff_subset_iff, contract_loops_eq, union_diff_self,
    union_eq_self_of_subset_left (M.subset_closure I)]

Premises used: Set.diff_subset_iff, Matroid.subset_closure, Matroid.contract_loops_eq, Set.union_eq_self_of_subset_left, Set.union_diff_self
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hIX : M.IsBasis I X
⊢ X ⊆ M.closure I

Tactic:
hIX.subset_closure

Premises used: Matroid.IsBasis.subset_closure
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hIX : M.IsBasis I X
⊢ X ⊆ M.closure I

Tactic:
exact hIX.subset_closure

Premises used: Matroid.IsBasis.subset_closure
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
C : Set α
inr :
  ∀ (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), M ／ M.closure C = M ／ C ＼ (M.closure C \ C)
wlog : ∀ {α : Type u_1} (M : Matroid α) (C : Set α) (hCE : C ⊆ M.E), M ／ M.closure C = M ／ C ＼ (M.closure C \ C)
⊢ M ／ M.closure C = M ／ C ＼ (M.closure C \ C)

Tactic:
wlog hCE : C ⊆ M.E with aux

Premises used: Matroid.E