awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
rw : ¬(Disjoint I J ∧ M.Indep (J ∪ I)) ∧ J ⊆ M.E ∧ Disjoint I J ↔ Disjoint I J ∧ ¬M.Indep (J ∪ I) ∧ J ⊆ M.E
⊢ (M ／ I).Dep J ↔ Disjoint J I ∧ M.Dep (J ∪ I)

Tactic:
rw [dep_iff, hI.contract_indep_iff, dep_iff, contract_ground, subset_diff, disjoint_comm,
    union_subset_iff, and_iff_left hI.subset_ground]

Premises used: Set.union_subset_iff, and_iff_left, Matroid.contract_ground, disjoint_comm, Set.subset_diff, Matroid.Indep.subset_ground, Matroid.Indep.contract_indep_iff, Matroid.dep_iff
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
mp : ¬(Disjoint I J ∧ M.Indep (J ∪ I)) ∧ J ⊆ M.E ∧ Disjoint I J → Disjoint I J ∧ ¬M.Indep (J ∪ I) ∧ J ⊆ M.E
mpr : Disjoint I J ∧ ¬M.Indep (J ∪ I) ∧ J ⊆ M.E → ¬(Disjoint I J ∧ M.Indep (J ∪ I)) ∧ J ⊆ M.E ∧ Disjoint I J
mp₁ mp₂ : ¬(Disjoint I J ∧ M.Indep (J ∪ I)) → J ⊆ M.E → Disjoint I J → Disjoint I J ∧ ¬M.Indep (J ∪ I) ∧ J ⊆ M.E
mp₃ : ¬(Disjoint I J ∧ M.Indep (J ∪ I)) → J ⊆ M.E → Disjoint I J → Disjoint I J
mp₄ : ¬(Disjoint I J ∧ M.Indep (J ∪ I)) → J ⊆ M.E → Disjoint I J → ¬M.Indep (J ∪ I)
mp₅ : ¬(Disjoint I J ∧ M.Indep (J ∪ I)) → J ⊆ M.E → Disjoint I J → J ⊆ M.E
mpr₁ mpr₂ : Disjoint I J → ¬M.Indep (J ∪ I) → J ⊆ M.E → ¬(Disjoint I J ∧ M.Indep (J ∪ I)) ∧ J ⊆ M.E ∧ Disjoint I J
mpr₃ : Disjoint I J → ¬M.Indep (J ∪ I) → J ⊆ M.E → ¬(Disjoint I J ∧ M.Indep (J ∪ I))
mpr₄ : Disjoint I J → ¬M.Indep (J ∪ I) → J ⊆ M.E → J ⊆ M.E
mpr₅ : Disjoint I J → ¬M.Indep (J ∪ I) → J ⊆ M.E → Disjoint I J
mp₆ : J ⊆ M.E → Disjoint I J → M.Indep (J ∪ I) → ¬Disjoint I J → False
mp₇ : J ⊆ M.E → Disjoint I J → M.Indep (J ∪ I) → ¬M.Indep (J ∪ I) → False
mpr₆ : Disjoint I J → ¬M.Indep (J ∪ I) → J ⊆ M.E → Disjoint I J → M.Indep (J ∪ I) → False
⊢ ¬(Disjoint I J ∧ M.Indep (J ∪ I)) ∧ J ⊆ M.E ∧ Disjoint I J ↔ Disjoint I J ∧ ¬M.Indep (J ∪ I) ∧ J ⊆ M.E

Tactic:
tauto
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
nth_rw :
  (M✶ ＼ I ＼ (X \ I)).E = (M✶ ＼ I ／ (X \ I)).E ∧
    ∀ ⦃I_1 : Set α⦄, I_1 ⊆ (M✶ ＼ I ＼ (X \ I)).E → ((M✶ ＼ I ＼ (X \ I)).Indep I_1 ↔ (M✶ ＼ I ／ (X \ I)).Indep I_1)
⊢ M ／ X = M ／ I ＼ (X \ I)

Tactic:
nth_rw 1 [← diff_union_of_subset hI.subset, ← dual_inj, dual_contract_delete, dual_contract,
    union_comm, ← delete_delete, ext_iff_indep]

Premises used: Matroid.dual_contract_delete, Matroid.dual_contract, Set.union_comm, Matroid.IsBasis.subset, Set.diff_union_of_subset, Matroid.delete_delete, Matroid.ext_iff_indep, Matroid.dual_inj
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
⊢ (M✶ ＼ I ＼ (X \ I)).E = (M✶ ＼ I ／ (X \ I)).E ∧
    ∀ ⦃I_1 : Set α⦄, I_1 ⊆ (M✶ ＼ I ＼ (X \ I)).E → ((M✶ ＼ I ＼ (X \ I)).Indep I_1 ↔ (M✶ ＼ I ／ (X \ I)).Indep I_1)

Tactic:
⟨rfl, fun J hJ ↦ ?_⟩

Premises used: And.intro, rfl
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
refine : ∀ (J : Set α) (hJ : J ⊆ (M✶ ＼ I ＼ (X \ I)).E), (M✶ ＼ I ＼ (X \ I)).Indep J ↔ (M✶ ＼ I ／ (X \ I)).Indep J
⊢ (M✶ ＼ I ＼ (X \ I)).E = (M✶ ＼ I ／ (X \ I)).E ∧
    ∀ ⦃I_1 : Set α⦄, I_1 ⊆ (M✶ ＼ I ＼ (X \ I)).E → ((M✶ ＼ I ＼ (X \ I)).Indep I_1 ↔ (M✶ ＼ I ／ (X \ I)).Indep I_1)

Tactic:
refine ⟨rfl, fun J hJ ↦ ?_⟩
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
J : Set α
hJ : J ⊆ (M✶ ＼ I ＼ (X \ I)).E
e : α
he : e ∈ X \ I
⊢ Disjoint {e} I

Tactic:
simpa using he.2

Premises used: And.right
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
J : Set α
hJ : J ⊆ (M✶ ＼ I ＼ (X \ I)).E
e : α
he : e ∈ X \ I
rw : e ∈ M.closure X \ I
⊢ e ∈ (M✶ ＼ I).coloops

Tactic:
rw [← dual_contract, dual_coloops, ← IsLoop, ← singleton_dep, hI.indep.contract_dep_iff,
      singleton_union, and_iff_right (by simpa using he.2), hI.indep.insert_dep_iff,
      hI.closure_eq_closure]

Premises used: Matroid.dual_contract, Matroid.Indep.contract_dep_iff, Set.singleton_union, and_iff_right, Matroid.Indep.insert_dep_iff, Matroid.dual_coloops, Matroid.singleton_dep, Matroid.IsBasis.indep, Matroid.IsLoop, Matroid.IsBasis.closure_eq_closure
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
J : Set α
hJ : J ⊆ (M✶ ＼ I ＼ (X \ I)).E
e : α
he : e ∈ X \ I
⊢ e ∈ M.closure X \ I

Tactic:
diff_subset_diff_left (M.subset_closure X) he

Premises used: Set.diff_subset_diff_left, Matroid.subset_closure
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
J : Set α
hJ : J ⊆ (M✶ ＼ I ＼ (X \ I)).E
e : α
he : e ∈ X \ I
⊢ e ∈ M.closure X \ I

Tactic:
exact diff_subset_diff_left (M.subset_closure X) he

Premises used: Set.diff_subset_diff_left, Matroid.subset_closure
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
J : Set α
hJ : J ⊆ (M✶ ＼ I ＼ (X \ I)).E
⊢ X \ I ⊆ (M✶ ＼ I).coloops

Tactic:
have hss : X \ I ⊆ (M✶ ＼ I).coloops := fun e he ↦ by
    rw [← dual_contract, dual_coloops, ← IsLoop, ← singleton_dep, hI.indep.contract_dep_iff,
      singleton_union, and_iff_right (by simpa using he.2), hI.indep.insert_dep_iff,
      hI.closure_eq_closure]
    exact diff_subset_diff_left (M.subset_closure X) he
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
J : Set α
hJ : J ⊆ (M✶ ＼ I ＼ (X \ I)).E
hss : X \ I ⊆ (M✶ ＼ I).coloops
rw : (M✶ ＼ I ＼ (X \ I)).Indep J ↔ Disjoint J (X \ I) ∧ (M✶ ＼ I).Indep (J ∪ X \ I)
rw₁ : (M✶ ＼ I).Indep J ∧ Disjoint J (X \ I) ↔ Disjoint J (X \ I) ∧ (M✶ ＼ I).Indep (J ∪ X \ I)
rw₂ : (M✶ ＼ I).Indep J ∧ Disjoint J (X \ I) ↔ Disjoint J (X \ I) ∧ (M✶ ＼ I).Indep J
rw₃ rw₄ : Disjoint J (X \ I) ∧ (M✶ ＼ I).Indep J ↔ Disjoint J (X \ I) ∧ (M✶ ＼ I).Indep J
⊢ (M✶ ＼ I ＼ (X \ I)).Indep J ↔ (M✶ ＼ I ／ (X \ I)).Indep J

Tactic:
rw [((coloops_indep _).subset hss).contract_indep_iff, delete_indep_iff,
    union_indep_iff_indep_of_subset_coloops hss, and_comm]

Premises used: Matroid.Indep.subset, and_comm, Matroid.coloops_indep, Matroid.Indep.contract_indep_iff, Matroid.delete_indep_iff, Matroid.union_indep_iff_indep_of_subset_coloops
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I J X : Set α
hI : M.Indep I
hB : (M ／ I).IsBasis J X
⊢ (((Disjoint J I ∧ M.Indep (J ∪ I)) ∧ J ⊆ X) ∧ ∀ ⦃t : Set α⦄, Disjoint t I → M.Indep (t ∪ I) → t ⊆ X → J ⊆ t → J = t) ∧
    X ⊆ M.E ∧ Disjoint X I

Tactic:
simp_rw [IsBasis, hI.contract_indep_iff, contract_ground, subset_diff,
    maximal_subset_iff, and_imp] at hB

Premises used: and_imp, Matroid.contract_ground, Set.subset_diff, maximal_subset_iff, Matroid.Indep.contract_indep_iff, Matroid.IsBasis
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I J X : Set α
hI : M.Indep I
hB :
  (((Disjoint J I ∧ M.Indep (J ∪ I)) ∧ J ⊆ X) ∧ ∀ ⦃t : Set α⦄, Disjoint t I → M.Indep (t ∪ I) → t ⊆ X → J ⊆ t → J = t) ∧
    X ⊆ M.E ∧ Disjoint X I
⊢ M.IsBasis (J ∪ I) (X ∪ I)

Tactic:
hB.1.1.1.2.isBasis_of_maximal_subset (union_subset_union_left _ hB.1.1.2)
    fun K hK hKJ hKX ↦ ?_

Premises used: Matroid.Indep.isBasis_of_maximal_subset, And.right, And.left, Set.union_subset_union_left
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I J X : Set α
hI : M.Indep I
hB :
  (((Disjoint J I ∧ M.Indep (J ∪ I)) ∧ J ⊆ X) ∧ ∀ ⦃t : Set α⦄, Disjoint t I → M.Indep (t ∪ I) → t ⊆ X → J ⊆ t → J = t) ∧
    X ⊆ M.E ∧ Disjoint X I
refine : ∀ (K : Set α) (hK : M.Indep K) (hKJ : J ∪ I ⊆ K) (hKX : K ⊆ X ∪ I), K ⊆ J ∪ I
⊢ M.IsBasis (J ∪ I) (X ∪ I)

Tactic:
refine hB.1.1.1.2.isBasis_of_maximal_subset (union_subset_union_left _ hB.1.1.2)
    fun K hK hKJ hKX ↦ ?_

Premises used: Matroid.Indep.isBasis_of_maximal_subset, And.right, And.left, Set.union_subset_union_left
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I J X : Set α
hI : M.Indep I
hB :
  (((Disjoint J I ∧ M.Indep (J ∪ I)) ∧ J ⊆ X) ∧ ∀ ⦃t : Set α⦄, Disjoint t I → M.Indep (t ∪ I) → t ⊆ X → J ⊆ t → J = t) ∧
    X ⊆ M.E ∧ Disjoint X I
K : Set α
hK : M.Indep K
hKJ : J ∪ I ⊆ K
hKX : K ⊆ X ∪ I
⊢ J ⊆ K ∧ I ⊆ K

Tactic:
rw [union_subset_iff] at hKJ

Premises used: Set.union_subset_iff
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I J X : Set α
hI : M.Indep I
hB :
  (((Disjoint J I ∧ M.Indep (J ∪ I)) ∧ J ⊆ X) ∧ ∀ ⦃t : Set α⦄, Disjoint t I → M.Indep (t ∪ I) → t ⊆ X → J ⊆ t → J = t) ∧
    X ⊆ M.E ∧ Disjoint X I
K : Set α
hK : M.Indep K
hKJ : J ∪ I ⊆ K
hKX : K ⊆ X ∪ I
hKJ₁ : J ⊆ K ∧ I ⊆ K
⊢ K ⊆ X ∪ I

Tactic:
rw [union_subset_iff] at hKJ

Premises used: Set.union_subset_iff
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I J X : Set α
hI : M.Indep I
hB :
  (((Disjoint J I ∧ M.Indep (J ∪ I)) ∧ J ⊆ X) ∧ ∀ ⦃t : Set α⦄, Disjoint t I → M.Indep (t ∪ I) → t ⊆ X → J ⊆ t → J = t) ∧
    X ⊆ M.E ∧ Disjoint X I
K : Set α
hK : M.Indep K
hKJ : J ⊆ K ∧ I ⊆ K
hKX : K ⊆ X ∪ I
⊢ M.Indep (K \ I ∪ I)

Tactic:
simpa [diff_union_of_subset hKJ.2]

Premises used: And.right, Set.diff_union_of_subset
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I J X : Set α
hI : M.Indep I
hB :
  (((Disjoint J I ∧ M.Indep (J ∪ I)) ∧ J ⊆ X) ∧ ∀ ⦃t : Set α⦄, Disjoint t I → M.Indep (t ∪ I) → t ⊆ X → J ⊆ t → J = t) ∧
    X ⊆ M.E ∧ Disjoint X I
K : Set α
hK : M.Indep K
hKJ : J ⊆ K ∧ I ⊆ K
hKX rwa rwa₁ rwa₂ rwa₃ : K ⊆ X ∪ I
⊢ K ⊆ I ∪ X

Tactic:
rwa [union_comm]

Premises used: Set.union_comm
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I J X : Set α
hI : M.Indep I
hB :
  (((Disjoint J I ∧ M.Indep (J ∪ I)) ∧ J ⊆ X) ∧ ∀ ⦃t : Set α⦄, Disjoint t I → M.Indep (t ∪ I) → t ⊆ X → J ⊆ t → J = t) ∧
    X ⊆ M.E ∧ Disjoint X I
K : Set α
hK : M.Indep K
hKJ : J ⊆ K ∧ I ⊆ K
hKX : K ⊆ X ∪ I
rw : K ⊆ K \ I ∪ I
rw₁ rw₂ : K ⊆ K
⊢ K ⊆ J ∪ I

Tactic:
rw [hB.1.2 (t := K \ I) disjoint_sdiff_left (by simpa [diff_union_of_subset hKJ.2])
    (diff_subset_iff.2 (by rwa [union_comm])) (subset_diff.2 ⟨hKJ.1, hB.1.1.1.1⟩),
    diff_union_of_subset hKJ.2]

Premises used: Iff.mpr, Set.diff_subset_iff, Set.subset_diff, And.right, And.left, Set.disjoint_sdiff_left, And.intro, Set.diff_union_of_subset
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I J X : Set α
hIX : M.IsBasis' I X
hJI : J ⊆ I
this : ∀ ⦃K : Set α⦄, Disjoint K J → M.Indep (K ∪ J) → K ⊆ X → I ⊆ K ∪ J → K ⊆ I
⊢ (M ／ J).IsBasis' (I \ J) (X \ J)

Tactic:
simpa +contextual [IsBasis', (hIX.indep.subset hJI).contract_indep_iff,
      subset_diff, maximal_subset_iff, disjoint_sdiff_left,
      union_eq_self_of_subset_right hJI, hIX.indep, diff_subset.trans hIX.subset,
      diff_subset_iff, subset_antisymm_iff, union_comm J]

Premises used: Set.diff_subset, Set.diff_subset_iff, Matroid.IsBasis', Set.union_eq_self_of_subset_right, HasSubset.Subset.trans, Set.subset_diff, Matroid.Indep.subset, Set.union_comm, Matroid.IsBasis'.indep, subset_antisymm_iff, Set.disjoint_sdiff_left, maximal_subset_iff, Matroid.Indep.contract_indep_iff, Matroid.IsBasis'.subset
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I J X : Set α
hIX : M.IsBasis' I X
hJI : J ⊆ I
suffices : ∀ ⦃K : Set α⦄, Disjoint K J → M.Indep (K ∪ J) → K ⊆ X → I ⊆ K ∪ J → K ⊆ I
⊢ (M ／ J).IsBasis' (I \ J) (X \ J)

Tactic:
suffices ∀ ⦃K⦄, Disjoint K J → M.Indep (K ∪ J) → K ⊆ X → I ⊆ K ∪ J → K ⊆ I by
    simpa +contextual [IsBasis', (hIX.indep.subset hJI).contract_indep_iff,
      subset_diff, maximal_subset_iff, disjoint_sdiff_left,
      union_eq_self_of_subset_right hJI, hIX.indep, diff_subset.trans hIX.subset,
      diff_subset_iff, subset_antisymm_iff, union_comm J]
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I J X : Set α
hIX : M.IsBasis' I X
hJI : J ⊆ I
K : Set α
hJK : Disjoint K J
hKJi : M.Indep (K ∪ J)
hKX : K ⊆ X
hIJK : I ⊆ K ∪ J
⊢ K ⊆ I

Tactic:
simp [hIX.eq_of_subset_indep hKJi hIJK (union_subset hKX (hJI.trans hIX.subset))]

Premises used: HasSubset.Subset.trans, Matroid.IsBasis'.eq_of_subset_indep, Set.union_subset, Matroid.IsBasis'.subset
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I J X : Set α
hIX : M.IsBasis' I X
hJI : J ⊆ I
⊢ ∀ ⦃K : Set α⦄, Disjoint K J → M.Indep (K ∪ J) → K ⊆ X → I ⊆ K ∪ J → K ⊆ I

Tactic:
exact fun K hJK hKJi hKX hIJK ↦ by
    simp [hIX.eq_of_subset_indep hKJi hIJK (union_subset hKX (hJI.trans hIX.subset))]
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I J X : Set α
hIX : M.IsBasis' I X
hJI : J ⊆ I
⊢ (M ／ J).IsBasis' (I \ J) X

Tactic:
simpa [isBasis'_iff_isBasis_inter_ground, inter_diff_assoc, ← diff_inter_distrib_right] using
    (hIX.contract_isBasis'_diff_diff_of_subset hJI).isBasis_inter_ground

Premises used: Matroid.isBasis'_iff_isBasis_inter_ground, Matroid.IsBasis'.isBasis_inter_ground, Set.diff_inter_distrib_right, Set.inter_diff_assoc, Matroid.IsBasis'.contract_isBasis'_diff_diff_of_subset
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I J X : Set α
hIX : M.IsBasis I X
hJI : J ⊆ I
⊢ (M ／ J).IsBasis (I \ J) (X ∩ (M ／ J).E)

Tactic:
have h := (hIX.isBasis'.contract_isBasis'_diff_of_subset hJI).isBasis_inter_ground
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I J X : Set α
hIX : M.IsBasis I X
hJI : J ⊆ I
h : (M ／ J).IsBasis (I \ J) (X ∩ (M ／ J).E)
rwa : ∀ (h : (M ／ J).IsBasis (I \ J) (X ∩ (M.E \ J))), (M ／ J).IsBasis (I \ J) (X \ J)
rwa₁ : ∀ (h : (M ／ J).IsBasis (I \ J) ((X ∩ M.E) \ J)), (M ／ J).IsBasis (I \ J) (X \ J)
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (h : (M ／ J).IsBasis (I \ J) (X \ J)), (M ／ J).IsBasis (I \ J) (X \ J)
⊢ (M ／ J).IsBasis (I \ J) (X \ J)

Tactic:
rwa [contract_ground, ← inter_diff_assoc, inter_eq_self_of_subset_left hIX.subset_ground] at h

Premises used: Matroid.IsBasis.subset_ground, Matroid.contract_ground, Set.inter_diff_assoc, Set.inter_eq_self_of_subset_left
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I J X Y : Set α
hIX : M.IsBasis I X
hJY : M.IsBasis J Y
hIJ : I ⊆ J
⊢ (M ／ I).IsBasis (J \ I) (Y \ X)

Tactic:
(hJY.contract_isBasis_diff_diff_of_subset hIJ).isBasis_subset ?_ ?_

Premises used: Matroid.IsBasis.isBasis_subset, Matroid.IsBasis.contract_isBasis_diff_diff_of_subset
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I J X Y : Set α
hIX : M.IsBasis I X
hJY : M.IsBasis J Y
hIJ : I ⊆ J
refine_1 : J \ I ⊆ Y \ X
refine_2 : Y \ X ⊆ Y \ I
⊢ (M ／ I).IsBasis (J \ I) (Y \ X)

Tactic:
refine (hJY.contract_isBasis_diff_diff_of_subset hIJ).isBasis_subset ?_ ?_

Premises used: Matroid.IsBasis.isBasis_subset, Matroid.IsBasis.contract_isBasis_diff_diff_of_subset
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I J X Y : Set α
hIX : M.IsBasis I X
hJY : M.IsBasis J Y
hIJ : I ⊆ J
refine_1 : Disjoint (J \ X) X
⊢ J \ I ⊆ Y \ X

Tactic:
rw [subset_diff, and_iff_right (diff_subset.trans hJY.subset),
      hIX.eq_of_subset_indep (hJY.indep.inter_right X) (subset_inter hIJ hIX.subset)
      inter_subset_right, diff_self_inter]

Premises used: Set.diff_subset, Set.diff_self_inter, HasSubset.Subset.trans, Set.subset_diff, and_iff_right, Matroid.IsBasis.subset, Set.subset_inter, Matroid.IsBasis.eq_of_subset_indep, Matroid.Indep.inter_right, Matroid.IsBasis.indep, Set.inter_subset_right
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I J X Y : Set α
hIX : M.IsBasis I X
hJY : M.IsBasis J Y
hIJ : I ⊆ J
⊢ Disjoint (J \ X) X

Tactic:
disjoint_sdiff_left

Premises used: Set.disjoint_sdiff_left
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I J X Y : Set α
hIX : M.IsBasis I X
hJY : M.IsBasis J Y
hIJ : I ⊆ J
⊢ Disjoint (J \ X) X

Tactic:
exact disjoint_sdiff_left

Premises used: Set.disjoint_sdiff_left
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I J X Y : Set α
hIX : M.IsBasis I X
hJY : M.IsBasis J Y
hIJ : I ⊆ J
⊢ Y \ X ⊆ Y \ I

Tactic:
diff_subset_diff_right hIX.subset

Premises used: Matroid.IsBasis.subset, Set.diff_subset_diff_right
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I J X Y : Set α
hIX : M.IsBasis I X
hJY : M.IsBasis J Y
hIJ : I ⊆ J
⊢ Y \ X ⊆ Y \ I

Tactic:
refine diff_subset_diff_right hIX.subset

Premises used: Matroid.IsBasis.subset, Set.diff_subset_diff_right
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I J X : Set α
h : M.IsBasis' (J ∪ I) (X ∪ I)
hJI : Disjoint J I
hXI : Disjoint X I
⊢ (M ／ I).IsBasis' J X

Tactic:
simpa [hJI.sdiff_eq_left, hXI.sdiff_eq_left] using
    h.contract_isBasis'_diff_diff_of_subset subset_union_right

Premises used: Set.subset_union_right, Disjoint.sdiff_eq_left, Matroid.IsBasis'.contract_isBasis'_diff_diff_of_subset
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I J X : Set α
h : M.IsBasis (J ∪ I) (X ∪ I)
hJI : Disjoint J I
hXI : Disjoint X I
⊢ (M ／ I).IsBasis J X

Tactic:
(isBasis'_iff_isBasis ?_).1 <| h.isBasis'.contract_isBasis_union_union hJI hXI

Premises used: Matroid.IsBasis.isBasis', Matroid.IsBasis'.contract_isBasis_union_union, Matroid.isBasis'_iff_isBasis, Iff.mp
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I J X : Set α
h : M.IsBasis (J ∪ I) (X ∪ I)
hJI : Disjoint J I
hXI : Disjoint X I
refine : X ⊆ (M ／ I).E
⊢ (M ／ I).IsBasis J X

Tactic:
refine (isBasis'_iff_isBasis ?_).1 <| h.isBasis'.contract_isBasis_union_union hJI hXI

Premises used: Matroid.IsBasis.isBasis', Matroid.IsBasis'.contract_isBasis_union_union, Matroid.isBasis'_iff_isBasis, Iff.mp
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I J X : Set α
h : M.IsBasis (J ∪ I) (X ∪ I)
hJI : Disjoint J I
hXI : Disjoint X I
rw : X ⊆ M.E
⊢ X ⊆ (M ／ I).E

Tactic:
rw [contract_ground, subset_diff, and_iff_left hXI]

Premises used: and_iff_left, Matroid.contract_ground, Set.subset_diff
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I J X : Set α
h : M.IsBasis (J ∪ I) (X ∪ I)
hJI : Disjoint J I
hXI : Disjoint X I
⊢ X ⊆ M.E

Tactic:
subset_union_left.trans h.subset_ground

Premises used: Matroid.IsBasis.subset_ground, HasSubset.Subset.trans, Set.subset_union_left
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I J X : Set α
h : M.IsBasis (J ∪ I) (X ∪ I)
hJI : Disjoint J I
hXI : Disjoint X I
⊢ X ⊆ M.E

Tactic:
exact subset_union_left.trans h.subset_ground

Premises used: Matroid.IsBasis.subset_ground, HasSubset.Subset.trans, Set.subset_union_left
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis' I X
rw : M ／ (X ∩ M.E) = M ／ I ＼ (X \ I)
rw₁ : M ／ I ＼ ((X ∩ M.E) \ I) = M ／ I ＼ (X \ I)
rw₂ : M ／ I ＼ (X \ I) = M ／ I ＼ ((X ∩ M.E) \ I)
rw₃ : M ／ I ＼ (X \ I ∩ (M ／ I).E) = M ／ I ＼ ((X ∩ M.E) \ I)
rw₄ : M ／ I ＼ (X \ I ∩ (M.E \ I)) = M ／ I ＼ ((X ∩ M.E) \ I)
rw₅ : M ／ I ＼ (X ∩ Iᶜ ∩ (M.E \ I)) = M ／ I ＼ ((X ∩ M.E) \ I)
rw₆ : M ／ I ＼ (X ∩ Iᶜ ∩ (M.E ∩ Iᶜ)) = M ／ I ＼ ((X ∩ M.E) \ I)
rw₇ : M ／ I ＼ (X ∩ M.E ∩ Iᶜ) = M ／ I ＼ ((X ∩ M.E) \ I)
rw₈ rw₉ : M ／ I ＼ ((X ∩ M.E) \ I) = M ／ I ＼ ((X ∩ M.E) \ I)
⊢ M ／ X = M ／ I ＼ (X \ I)

Tactic:
rw [← contract_inter_ground_eq, hI.isBasis_inter_ground.contract_eq_contract_delete, eq_comm,
    ← delete_inter_ground_eq, contract_ground, diff_eq, diff_eq, ← inter_inter_distrib_right,
    ← diff_eq]

Premises used: Set.inter_inter_distrib_right, Matroid.delete_inter_ground_eq, Matroid.contract_ground, Set.diff_eq, eq_comm, Matroid.IsBasis'.isBasis_inter_ground, Matroid.contract_inter_ground_eq, Matroid.IsBasis.contract_eq_contract_delete
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I J X : Set α
hI : M.IsBasis' I X
rw : (M ／ I ＼ (X \ I)).Indep J ↔ M.Indep (J ∪ I) ∧ Disjoint X J
rw₁ : (M ／ I).Indep J ∧ Disjoint J (X \ I) ↔ M.Indep (J ∪ I) ∧ Disjoint X J
rw₂ : (Disjoint J I ∧ M.Indep (J ∪ I)) ∧ Disjoint J (X \ I) ↔ M.Indep (J ∪ I) ∧ Disjoint X J
rw₃ : Disjoint J (X \ I) ∧ Disjoint J I ∧ M.Indep (J ∪ I) ↔ M.Indep (J ∪ I) ∧ Disjoint X J
rw₄ : (Disjoint J (X \ I) ∧ Disjoint J I) ∧ M.Indep (J ∪ I) ↔ M.Indep (J ∪ I) ∧ Disjoint X J
rw₅ : Disjoint J (X \ I ∪ I) ∧ M.Indep (J ∪ I) ↔ M.Indep (J ∪ I) ∧ Disjoint X J
rw₆ : Disjoint J (X ∪ I) ∧ M.Indep (J ∪ I) ↔ M.Indep (J ∪ I) ∧ Disjoint X J
rw₇ : Disjoint J X ∧ M.Indep (J ∪ I) ↔ M.Indep (J ∪ I) ∧ Disjoint X J
rw₈ : M.Indep (J ∪ I) ∧ Disjoint J X ↔ M.Indep (J ∪ I) ∧ Disjoint X J
rw₉ rw₁₀ : M.Indep (J ∪ I) ∧ Disjoint X J ↔ M.Indep (J ∪ I) ∧ Disjoint X J
⊢ (M ／ X).Indep J ↔ M.Indep (J ∪ I) ∧ Disjoint X J

Tactic:
rw [hI.contract_eq_contract_delete, delete_indep_iff, hI.indep.contract_indep_iff,
    and_comm, ← and_assoc, ← disjoint_union_right, diff_union_self,
    union_eq_self_of_subset_right hI.subset, and_comm, disjoint_comm]

Premises used: Matroid.IsBasis'.contract_eq_contract_delete, Set.disjoint_union_right, Set.union_eq_self_of_subset_right, disjoint_comm, Set.diff_union_self, and_comm, Matroid.IsBasis'.indep, Matroid.Indep.contract_indep_iff, and_assoc, Matroid.IsBasis'.subset, Matroid.delete_indep_iff
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I J X : Set α
hI : M.IsBasis I X
⊢ (M ／ X).Indep J ↔ M.Indep (J ∪ I) ∧ Disjoint X J

Tactic:
hI.isBasis'.contract_indep_iff

Premises used: Matroid.IsBasis.isBasis', Matroid.IsBasis'.contract_indep_iff
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis' I X
D : Set α
rw : (M ／ I ＼ (X \ I)).Dep D ↔ M.Dep (D ∪ I) ∧ Disjoint X D
rw₁ : (M ／ I).Dep D ∧ Disjoint D (X \ I) ↔ M.Dep (D ∪ I) ∧ Disjoint X D
rw₂ : (Disjoint D I ∧ M.Dep (D ∪ I)) ∧ Disjoint D (X \ I) ↔ M.Dep (D ∪ I) ∧ Disjoint X D
rw₃ : Disjoint D (X \ I) ∧ Disjoint D I ∧ M.Dep (D ∪ I) ↔ M.Dep (D ∪ I) ∧ Disjoint X D
rw₄ : (Disjoint D (X \ I) ∧ Disjoint D I) ∧ M.Dep (D ∪ I) ↔ M.Dep (D ∪ I) ∧ Disjoint X D
rw₅ : Disjoint D (X \ I ∪ I) ∧ M.Dep (D ∪ I) ↔ M.Dep (D ∪ I) ∧ Disjoint X D
rw₆ : Disjoint D X ∧ M.Dep (D ∪ I) ↔ M.Dep (D ∪ I) ∧ Disjoint X D
rw₇ : Disjoint X D ∧ M.Dep (D ∪ I) ↔ M.Dep (D ∪ I) ∧ Disjoint X D
rw₈ rw₉ : M.Dep (D ∪ I) ∧ Disjoint X D ↔ M.Dep (D ∪ I) ∧ Disjoint X D
⊢ (M ／ X).Dep D ↔ M.Dep (D ∪ I) ∧ Disjoint X D

Tactic:
rw [hI.contract_eq_contract_delete, delete_dep_iff, hI.indep.contract_dep_iff, and_comm,
    ← and_assoc, ← disjoint_union_right, diff_union_of_subset hI.subset, disjoint_comm, and_comm]

Premises used: Matroid.IsBasis'.contract_eq_contract_delete, Set.disjoint_union_right, Matroid.Indep.contract_dep_iff, disjoint_comm, and_comm, Matroid.IsBasis'.indep, Matroid.delete_dep_iff, and_assoc, Set.diff_union_of_subset, Matroid.IsBasis'.subset
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
D : Set α
⊢ (M ／ X).Dep D ↔ M.Dep (D ∪ I) ∧ Disjoint X D

Tactic:
hI.isBasis'.contract_dep_iff

Premises used: Matroid.IsBasis.isBasis', Matroid.IsBasis'.contract_dep_iff
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I J X : Set α
hI : M.IsBasis I X
hdj : Disjoint X J
rw : M.Indep (J ∪ I) ∧ Disjoint X J ↔ M.Indep (J ∪ I)
rw₁ rw₂ : M.Indep (J ∪ I) ↔ M.Indep (J ∪ I)
⊢ (M ／ X).Indep J ↔ M.Indep (J ∪ I)

Tactic:
rw [hI.contract_indep_iff, and_iff_left hdj]

Premises used: Matroid.IsBasis.contract_indep_iff, and_iff_left
-- 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: Matroid.IsBasis.contract_indep_iff, and_iff_left, Set.disjoint_sdiff_right