awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
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
⊢ (M✶ ＼ I ＼ (X \ I)).Indep J ↔ (M✶ ＼ I ／ (X \ I)).Indep J
have rw₃ : Disjoint J (X \ I) ∧ (M✶ ＼ I).Indep J ↔ Disjoint J (X \ I) ∧ (M✶ ＼ 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]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (hypothesis)
Goal:
α : Type u_1
M : Matroid α
I J X : Set α
hI : M.Indep I
hB : (M ／ I).IsBasis J X
⊢ M.IsBasis (J ∪ I) (X ∪ I)
have 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
Tactic: simp_rw [IsBasis, hI.contract_indep_iff, contract_ground, subset_diff,
    maximal_subset_iff, and_imp] at hB
Cleared hypotheses: hB
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
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)
have refine : ∀ (K : Set α) (hK : M.Indep K) (hKJ : J ∪ I ⊆ K) (hKX : K ⊆ X ∪ I), K ⊆ J ∪ 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 ↦ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (hypothesis)
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
⊢ K ⊆ J ∪ I
have hKJ₁ : J ⊆ K ∧ I ⊆ K
Tactic: rw [union_subset_iff] at hKJ
Cleared hypotheses: hKJ, hKX
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
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
⊢ K ⊆ J ∪ I
have rw : K ⊆ K \ I ∪ 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]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
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
⊢ K ⊆ J ∪ I
have rw₁ : K ⊆ K
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]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
I J X : Set α
hIX : M.IsBasis' I X
hJI : J ⊆ I
⊢ (M ／ J).IsBasis' (I \ J) (X \ J)
have suffices : ∀ ⦃K : Set α⦄, Disjoint K J → M.Indep (K ∪ J) → K ⊆ X → I ⊆ K ∪ J → K ⊆ I
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]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (hypothesis)
Goal:
α : Type u_1
M : Matroid α
I J X : Set α
hIX : M.IsBasis I X
hJI : J ⊆ I
⊢ (M ／ J).IsBasis (I \ J) (X \ J)
have h : (M ／ J).IsBasis (I \ J) (X ∩ (M ／ J).E)
Tactic: have h := (hIX.isBasis'.contract_isBasis'_diff_of_subset hJI).isBasis_inter_ground
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
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)
⊢ (M ／ J).IsBasis (I \ J) (X \ J)
have rwa : ∀ (h : (M ／ J).IsBasis (I \ J) (X ∩ (M.E \ 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
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)
⊢ (M ／ J).IsBasis (I \ J) (X \ J)
have rwa₁ : ∀ (h : (M ／ J).IsBasis (I \ J) ((X ∩ M.E) \ 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
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)
⊢ (M ／ J).IsBasis (I \ J) (X \ J)
have rwa₂ : ∀ (h : (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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
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)
have refine_1 : J \ I ⊆ Y \ X
Tactic: refine (hJY.contract_isBasis_diff_diff_of_subset hIJ).isBasis_subset ?_ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
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
⊢ (M ／ I).IsBasis (J \ I) (Y \ X)
have refine_2 : Y \ X ⊆ Y \ I
Tactic: refine (hJY.contract_isBasis_diff_diff_of_subset hIJ).isBasis_subset ?_ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
I J X Y : Set α
hIX : M.IsBasis I X
hJY : M.IsBasis J Y
hIJ : I ⊆ J
⊢ J \ I ⊆ Y \ X
have refine_1 : Disjoint (J \ X) 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]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
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
have refine : X ⊆ (M ／ I).E
Tactic: refine (isBasis'_iff_isBasis ?_).1 <| h.isBasis'.contract_isBasis_union_union hJI hXI
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
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 ／ I).E
have rw : X ⊆ M.E
Tactic: rw [contract_ground, subset_diff, and_iff_left hXI]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis' I X
⊢ M ／ X = M ／ I ＼ (X \ I)
have rw : M ／ (X ∩ M.E) = 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]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis' I X
rw : M ／ (X ∩ M.E) = M ／ I ＼ (X \ I)
⊢ M ／ X = M ／ I ＼ (X \ I)
have rw₁ : M ／ I ＼ ((X ∩ M.E) \ I) = 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]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
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)
⊢ M ／ X = M ／ I ＼ (X \ I)
have rw₂ : M ／ I ＼ (X \ I) = M ／ I ＼ ((X ∩ M.E) \ 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]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
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)
⊢ M ／ X = M ／ I ＼ (X \ I)
have rw₃ : M ／ I ＼ (X \ I ∩ (M ／ I).E) = M ／ I ＼ ((X ∩ M.E) \ 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]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
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)
⊢ M ／ X = M ／ I ＼ (X \ I)
have rw₄ : M ／ I ＼ (X \ I ∩ (M.E \ I)) = M ／ I ＼ ((X ∩ M.E) \ 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]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
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)
⊢ M ／ X = M ／ I ＼ (X \ I)
have rw₅ : M ／ I ＼ (X ∩ Iᶜ ∩ (M.E \ I)) = M ／ I ＼ ((X ∩ M.E) \ 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]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
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)
⊢ M ／ X = M ／ I ＼ (X \ I)
have rw₆ : M ／ I ＼ (X ∩ Iᶜ ∩ (M.E ∩ Iᶜ)) = M ／ I ＼ ((X ∩ M.E) \ 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]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
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)
⊢ M ／ X = M ／ I ＼ (X \ I)
have rw₇ : M ／ I ＼ (X ∩ M.E ∩ Iᶜ) = M ／ I ＼ ((X ∩ M.E) \ 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]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
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)
⊢ M ／ X = M ／ I ＼ (X \ I)
have rw₈ : M ／ I ＼ ((X ∩ M.E) \ I) = M ／ I ＼ ((X ∩ M.E) \ 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]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
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
have rw : (M ／ I ＼ (X \ I)).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]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
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
⊢ (M ／ X).Indep J ↔ M.Indep (J ∪ I) ∧ Disjoint X J
have rw₁ : (M ／ I).Indep J ∧ Disjoint J (X \ I) ↔ 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]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
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
⊢ (M ／ X).Indep J ↔ M.Indep (J ∪ I) ∧ Disjoint X J
have rw₂ : (Disjoint J I ∧ M.Indep (J ∪ I)) ∧ Disjoint J (X \ I) ↔ 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]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
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
⊢ (M ／ X).Indep J ↔ M.Indep (J ∪ I) ∧ Disjoint X J
have rw₃ : Disjoint J (X \ I) ∧ Disjoint J I ∧ M.Indep (J ∪ I) ↔ 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]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
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
⊢ (M ／ X).Indep J ↔ M.Indep (J ∪ I) ∧ Disjoint X J
have rw₄ : (Disjoint J (X \ I) ∧ Disjoint J I) ∧ M.Indep (J ∪ I) ↔ 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]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
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
⊢ (M ／ X).Indep J ↔ M.Indep (J ∪ I) ∧ Disjoint X J
have rw₅ : Disjoint J (X \ I ∪ I) ∧ M.Indep (J ∪ I) ↔ 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]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
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
⊢ (M ／ X).Indep J ↔ M.Indep (J ∪ I) ∧ Disjoint X J
have rw₆ : Disjoint J (X ∪ I) ∧ M.Indep (J ∪ I) ↔ 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]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
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
⊢ (M ／ X).Indep J ↔ M.Indep (J ∪ I) ∧ Disjoint X J
have rw₇ : Disjoint J X ∧ M.Indep (J ∪ I) ↔ 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]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
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
⊢ (M ／ X).Indep J ↔ M.Indep (J ∪ I) ∧ Disjoint X J
have rw₈ : M.Indep (J ∪ I) ∧ Disjoint J X ↔ 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]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
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
⊢ (M ／ X).Indep J ↔ M.Indep (J ∪ I) ∧ Disjoint X J
have rw₉ : M.Indep (J ∪ I) ∧ Disjoint X 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]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
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
have rw : (M ／ I ＼ (X \ I)).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]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
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
⊢ (M ／ X).Dep D ↔ M.Dep (D ∪ I) ∧ Disjoint X D
have rw₁ : (M ／ I).Dep D ∧ Disjoint D (X \ I) ↔ 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]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
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
⊢ (M ／ X).Dep D ↔ M.Dep (D ∪ I) ∧ Disjoint X D
have rw₂ : (Disjoint D I ∧ M.Dep (D ∪ I)) ∧ Disjoint D (X \ I) ↔ 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]