awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
C D : Set α
⊢ M ／ C ＼ D = M ／ C ＼ (D \ C)
have rw : D ∩ (M ／ C).E = D \ C ∩ (M ／ C).E
Tactic: rw [delete_eq_delete_iff, contract_ground, diff_eq, diff_eq, ← inter_inter_distrib_right,
    inter_assoc]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
C D : Set α
rw : D ∩ (M ／ C).E = D \ C ∩ (M ／ C).E
⊢ M ／ C ＼ D = M ／ C ＼ (D \ C)
have rw₁ : D ∩ (M.E \ C) = D \ C ∩ (M.E \ C)
Tactic: rw [delete_eq_delete_iff, contract_ground, diff_eq, diff_eq, ← inter_inter_distrib_right,
    inter_assoc]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
C D : Set α
rw : D ∩ (M ／ C).E = D \ C ∩ (M ／ C).E
rw₁ : D ∩ (M.E \ C) = D \ C ∩ (M.E \ C)
⊢ M ／ C ＼ D = M ／ C ＼ (D \ C)
have rw₂ : D ∩ (M.E ∩ Cᶜ) = D \ C ∩ (M.E ∩ Cᶜ)
Tactic: rw [delete_eq_delete_iff, contract_ground, diff_eq, diff_eq, ← inter_inter_distrib_right,
    inter_assoc]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
C D : Set α
rw : D ∩ (M ／ C).E = D \ C ∩ (M ／ C).E
rw₁ : D ∩ (M.E \ C) = D \ C ∩ (M.E \ C)
rw₂ : D ∩ (M.E ∩ Cᶜ) = D \ C ∩ (M.E ∩ Cᶜ)
⊢ M ／ C ＼ D = M ／ C ＼ (D \ C)
have rw₃ : D ∩ (M.E ∩ Cᶜ) = D ∩ Cᶜ ∩ (M.E ∩ Cᶜ)
Tactic: rw [delete_eq_delete_iff, contract_ground, diff_eq, diff_eq, ← inter_inter_distrib_right,
    inter_assoc]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
C D : Set α
rw : D ∩ (M ／ C).E = D \ C ∩ (M ／ C).E
rw₁ : D ∩ (M.E \ C) = D \ C ∩ (M.E \ C)
rw₂ : D ∩ (M.E ∩ Cᶜ) = D \ C ∩ (M.E ∩ Cᶜ)
rw₃ : D ∩ (M.E ∩ Cᶜ) = D ∩ Cᶜ ∩ (M.E ∩ Cᶜ)
⊢ M ／ C ＼ D = M ／ C ＼ (D \ C)
have rw₄ : D ∩ (M.E ∩ Cᶜ) = D ∩ M.E ∩ Cᶜ
Tactic: rw [delete_eq_delete_iff, contract_ground, diff_eq, diff_eq, ← inter_inter_distrib_right,
    inter_assoc]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
C D : Set α
rw : D ∩ (M ／ C).E = D \ C ∩ (M ／ C).E
rw₁ : D ∩ (M.E \ C) = D \ C ∩ (M.E \ C)
rw₂ : D ∩ (M.E ∩ Cᶜ) = D \ C ∩ (M.E ∩ Cᶜ)
rw₃ : D ∩ (M.E ∩ Cᶜ) = D ∩ Cᶜ ∩ (M.E ∩ Cᶜ)
rw₄ : D ∩ (M.E ∩ Cᶜ) = D ∩ M.E ∩ Cᶜ
⊢ M ／ C ＼ D = M ／ C ＼ (D \ C)
have rw₅ : D ∩ (M.E ∩ Cᶜ) = D ∩ (M.E ∩ Cᶜ)
Tactic: rw [delete_eq_delete_iff, contract_ground, diff_eq, diff_eq, ← inter_inter_distrib_right,
    inter_assoc]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
R C : Set α
M : Matroid α
h : Disjoint C R
⊢ M ／ C ↾ R = (M ↾ (R ∪ C)) ／ C
have refine : ∀ (I : Set α) (hI : I ⊆ R), (M ／ C ↾ R).Indep I ↔ ((M ↾ (R ∪ C)) ／ C).Indep I
Tactic: refine ext_indep (by simp [h.sdiff_eq_right]) fun I (hI : I ⊆ R) ↦ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
R C : Set α
M : Matroid α
h : Disjoint C R
I : Set α
hI : I ⊆ R
⊢ (M ／ C ↾ R).Indep I ↔ ((M ↾ (R ∪ C)) ／ C).Indep I
have obtain : ∀ (J : Set α) (hJ : (M ↾ (R ∪ C)).IsBasis' J C), (M ／ C ↾ R).Indep I ↔ ((M ↾ (R ∪ C)) ／ C).Indep I
Tactic: obtain ⟨J, hJ⟩ := (M ↾ (R ∪ C)).exists_isBasis' C
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (hypothesis)
Goal:
α : Type u_1
R C : Set α
M : Matroid α
h : Disjoint C R
I : Set α
hI : I ⊆ R
J : Set α
hJ : (M ↾ (R ∪ C)).IsBasis' J C
⊢ (M ／ C ↾ R).Indep I ↔ ((M ↾ (R ∪ C)) ／ C).Indep I
have hJ' : M.IsBasis' J C
Tactic: have hJ' : M.IsBasis' J C := by
    simpa [inter_eq_self_of_subset_left subset_union_right] using (isBasis'_restrict_iff.1 hJ).1
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
R C : Set α
M : Matroid α
h : Disjoint C R
I : Set α
hI : I ⊆ R
J : Set α
hJ : (M ↾ (R ∪ C)).IsBasis' J C
hJ' : M.IsBasis' J C
⊢ (M ／ C ↾ R).Indep I ↔ ((M ↾ (R ∪ C)) ／ C).Indep I
have rw : (M.Indep (I ∪ J) ∧ Disjoint C I) ∧ I ⊆ R ↔ (M.Indep (I ∪ J) ∧ I ∪ J ⊆ R ∪ C) ∧ Disjoint C I
Tactic: rw [restrict_indep_iff, hJ.contract_indep_iff, hJ'.contract_indep_iff, restrict_indep_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (hypothesis)
Goal:
α : Type u_1
R C : Set α
M : Matroid α
h : Disjoint C R
I : Set α
hI : I ⊆ R
J : Set α
hJ : (M ↾ (R ∪ C)).IsBasis' J C
hJ' : M.IsBasis' J C
⊢ (M.Indep (I ∪ J) ∧ Disjoint C I) ∧ I ⊆ R ↔ (M.Indep (I ∪ J) ∧ I ∪ J ⊆ R ∪ C) ∧ Disjoint C I
have hJC : J ⊆ C
Tactic: have hJC := hJ'.subset
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
R C : Set α
M : Matroid α
h : Disjoint C R
I : Set α
hI : I ⊆ R
J : Set α
hJ : (M ↾ (R ∪ C)).IsBasis' J C
hJ' : M.IsBasis' J C
hJC : J ⊆ C
⊢ (M.Indep (I ∪ J) ∧ Disjoint C I) ∧ I ⊆ R ↔ (M.Indep (I ∪ J) ∧ I ∪ J ⊆ R ∪ C) ∧ Disjoint C I
have tauto_set : ∀ (h : ∀ (x : α), x ∈ C ∧ x ∈ R → Membership.mem (γ := Set α) ∅ x) (hI : ∀ x ∈ I, x ∈ R)
  (hJ : (M ↾ (R ∪ C)).IsBasis' J C) (hJ' : M.IsBasis' J C) (hJC : ∀ x ∈ J, x ∈ C),
  ((M.Indep (I ∪ J) ∧ ∀ (x : α), x ∈ C ∧ x ∈ I → Membership.mem (γ := Set α) ∅ x) ∧ ∀ x ∈ I, True) ↔
    (M.Indep (I ∪ J) ∧ ∀ (x : α), x ∈ I ∨ x ∈ J → x ∈ R ∨ x ∈ C) ∧
      ∀ (x : α), x ∈ C ∧ x ∈ I → Membership.mem (γ := Set α) ∅ x
Tactic: tauto_set
Cleared hypotheses: h, hI, hJ, hJ', hJC
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
R C : Set α
M : Matroid α
hCR : C ⊆ R
⊢ (M ↾ R) ／ C = M ／ C ↾ R \ C
have rw : (M ↾ R) ／ C = (M ↾ (R \ C ∪ C)) ／ C
Tactic: rw [contract_restrict_eq_restrict_contract _ disjoint_sdiff_right]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
D C : Set α
M : Matroid α
hCD : Disjoint C D
⊢ M ／ C ＼ D = M ＼ D ／ C
have inr : ∀ (aux : ∀ {C : Set α} (hCD : Disjoint C D) (hCE : C ⊆ M.E), M ／ C ＼ D = M ＼ D ／ C) (hCE : ¬C ⊆ M.E),
  M ／ C ＼ D = M ＼ D ／ C
Tactic: wlog hCE : C ⊆ M.E generalizing C with aux
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
D C : Set α
M : Matroid α
hCD : Disjoint C D
inr :
  ∀ (aux : ∀ {C : Set α} (hCD : Disjoint C D) (hCE : C ⊆ M.E), M ／ C ＼ D = M ＼ D ／ C) (hCE : ¬C ⊆ M.E),
    M ／ C ＼ D = M ＼ D ／ C
⊢ M ／ C ＼ D = M ＼ D ／ C
have wlog : ∀ {C : Set α} (hCD : Disjoint C D) (hCE : C ⊆ M.E), M ／ C ＼ D = M ＼ D ／ C
Tactic: wlog hCE : C ⊆ M.E generalizing C with aux
Cleared hypotheses: hCD
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
D C : Set α
M : Matroid α
hCD : Disjoint C D
aux : ∀ {C : Set α} (hCD : Disjoint C D) (hCE : C ⊆ M.E), M ／ C ＼ D = M ＼ D ／ C
hCE : ¬C ⊆ M.E
⊢ M ／ C ＼ D = M ＼ D ／ C
have inr : M ／ (C ∩ M.E) ＼ D = M ＼ D ／ C
Tactic: rw [← contract_inter_ground_eq, aux (hCD.mono_left inter_subset_left) inter_subset_right,
      contract_eq_contract_iff, inter_assoc, delete_ground,
      inter_eq_self_of_subset_right diff_subset]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
D C : Set α
M : Matroid α
hCD : Disjoint C D
aux : ∀ {C : Set α} (hCD : Disjoint C D) (hCE : C ⊆ M.E), M ／ C ＼ D = M ＼ D ／ C
hCE : ¬C ⊆ M.E
inr : M ／ (C ∩ M.E) ＼ D = M ＼ D ／ C
⊢ M ／ C ＼ D = M ＼ D ／ C
have inr₁ : M ＼ D ／ (C ∩ M.E) = M ＼ D ／ C
Tactic: rw [← contract_inter_ground_eq, aux (hCD.mono_left inter_subset_left) inter_subset_right,
      contract_eq_contract_iff, inter_assoc, delete_ground,
      inter_eq_self_of_subset_right diff_subset]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
D C : Set α
M : Matroid α
hCD : Disjoint C D
aux : ∀ {C : Set α} (hCD : Disjoint C D) (hCE : C ⊆ M.E), M ／ C ＼ D = M ＼ D ／ C
hCE : ¬C ⊆ M.E
inr : M ／ (C ∩ M.E) ＼ D = M ＼ D ／ C
inr₁ : M ＼ D ／ (C ∩ M.E) = M ＼ D ／ C
⊢ M ／ C ＼ D = M ＼ D ／ C
have inr₂ : C ∩ M.E ∩ (M ＼ D).E = C ∩ (M ＼ D).E
Tactic: rw [← contract_inter_ground_eq, aux (hCD.mono_left inter_subset_left) inter_subset_right,
      contract_eq_contract_iff, inter_assoc, delete_ground,
      inter_eq_self_of_subset_right diff_subset]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
D C : Set α
M : Matroid α
hCD : Disjoint C D
aux : ∀ {C : Set α} (hCD : Disjoint C D) (hCE : C ⊆ M.E), M ／ C ＼ D = M ＼ D ／ C
hCE : ¬C ⊆ M.E
inr : M ／ (C ∩ M.E) ＼ D = M ＼ D ／ C
inr₁ : M ＼ D ／ (C ∩ M.E) = M ＼ D ／ C
inr₂ : C ∩ M.E ∩ (M ＼ D).E = C ∩ (M ＼ D).E
⊢ M ／ C ＼ D = M ＼ D ／ C
have inr₃ : C ∩ (M.E ∩ (M ＼ D).E) = C ∩ (M ＼ D).E
Tactic: rw [← contract_inter_ground_eq, aux (hCD.mono_left inter_subset_left) inter_subset_right,
      contract_eq_contract_iff, inter_assoc, delete_ground,
      inter_eq_self_of_subset_right diff_subset]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
D C : Set α
M : Matroid α
hCD : Disjoint C D
aux : ∀ {C : Set α} (hCD : Disjoint C D) (hCE : C ⊆ M.E), M ／ C ＼ D = M ＼ D ／ C
hCE : ¬C ⊆ M.E
inr : M ／ (C ∩ M.E) ＼ D = M ＼ D ／ C
inr₁ : M ＼ D ／ (C ∩ M.E) = M ＼ D ／ C
inr₂ : C ∩ M.E ∩ (M ＼ D).E = C ∩ (M ＼ D).E
inr₃ : C ∩ (M.E ∩ (M ＼ D).E) = C ∩ (M ＼ D).E
⊢ M ／ C ＼ D = M ＼ D ／ C
have inr₄ : C ∩ (M.E ∩ (M.E \ D)) = C ∩ (M.E \ D)
Tactic: rw [← contract_inter_ground_eq, aux (hCD.mono_left inter_subset_left) inter_subset_right,
      contract_eq_contract_iff, inter_assoc, delete_ground,
      inter_eq_self_of_subset_right diff_subset]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
D C : Set α
M : Matroid α
hCD : Disjoint C D
aux : ∀ {C : Set α} (hCD : Disjoint C D) (hCE : C ⊆ M.E), M ／ C ＼ D = M ＼ D ／ C
hCE : ¬C ⊆ M.E
inr : M ／ (C ∩ M.E) ＼ D = M ＼ D ／ C
inr₁ : M ＼ D ／ (C ∩ M.E) = M ＼ D ／ C
inr₂ : C ∩ M.E ∩ (M ＼ D).E = C ∩ (M ＼ D).E
inr₃ : C ∩ (M.E ∩ (M ＼ D).E) = C ∩ (M ＼ D).E
inr₄ : C ∩ (M.E ∩ (M.E \ D)) = C ∩ (M.E \ D)
⊢ M ／ C ＼ D = M ＼ D ／ C
have inr₅ : C ∩ (M.E \ D) = C ∩ (M.E \ D)
Tactic: rw [← contract_inter_ground_eq, aux (hCD.mono_left inter_subset_left) inter_subset_right,
      contract_eq_contract_iff, inter_assoc, delete_ground,
      inter_eq_self_of_subset_right diff_subset]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
D C_1 : Set α
M : Matroid α
C : Set α
hCD : Disjoint C D
hCE : C ⊆ M.E
⊢ M ／ C ＼ D = M ＼ D ／ C
have rw : M ／ C ↾ (M ／ C).E \ D = M ＼ D ／ C
Tactic: rw [delete_eq_restrict, delete_eq_restrict, contract_ground, diff_diff_comm,
    restrict_contract_eq_contract_restrict _ (by simpa [hCE, subset_diff])]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
D C_1 : Set α
M : Matroid α
C : Set α
hCD : Disjoint C D
hCE : C ⊆ M.E
rw : M ／ C ↾ (M ／ C).E \ D = M ＼ D ／ C
⊢ M ／ C ＼ D = M ＼ D ／ C
have rw₁ : M ／ C ↾ (M ／ C).E \ D = (M ↾ M.E \ D) ／ C
Tactic: rw [delete_eq_restrict, delete_eq_restrict, contract_ground, diff_diff_comm,
    restrict_contract_eq_contract_restrict _ (by simpa [hCE, subset_diff])]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
D C_1 : Set α
M : Matroid α
C : Set α
hCD : Disjoint C D
hCE : C ⊆ M.E
rw : M ／ C ↾ (M ／ C).E \ D = M ＼ D ／ C
rw₁ : M ／ C ↾ (M ／ C).E \ D = (M ↾ M.E \ D) ／ C
⊢ M ／ C ＼ D = M ＼ D ／ C
have rw₂ : M ／ C ↾ (M.E \ C) \ D = (M ↾ M.E \ D) ／ C
Tactic: rw [delete_eq_restrict, delete_eq_restrict, contract_ground, diff_diff_comm,
    restrict_contract_eq_contract_restrict _ (by simpa [hCE, subset_diff])]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
D C_1 : Set α
M : Matroid α
C : Set α
hCD : Disjoint C D
hCE : C ⊆ M.E
rw : M ／ C ↾ (M ／ C).E \ D = M ＼ D ／ C
rw₁ : M ／ C ↾ (M ／ C).E \ D = (M ↾ M.E \ D) ／ C
rw₂ : M ／ C ↾ (M.E \ C) \ D = (M ↾ M.E \ D) ／ C
⊢ M ／ C ＼ D = M ＼ D ／ C
have rw₃ : M ／ C ↾ (M.E \ D) \ C = (M ↾ M.E \ D) ／ C
Tactic: rw [delete_eq_restrict, delete_eq_restrict, contract_ground, diff_diff_comm,
    restrict_contract_eq_contract_restrict _ (by simpa [hCE, subset_diff])]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
D C_1 : Set α
M : Matroid α
C : Set α
hCD : Disjoint C D
hCE : C ⊆ M.E
rw : M ／ C ↾ (M ／ C).E \ D = M ＼ D ／ C
rw₁ : M ／ C ↾ (M ／ C).E \ D = (M ↾ M.E \ D) ／ C
rw₂ : M ／ C ↾ (M.E \ C) \ D = (M ↾ M.E \ D) ／ C
rw₃ : M ／ C ↾ (M.E \ D) \ C = (M ↾ M.E \ D) ／ C
⊢ M ／ C ＼ D = M ＼ D ／ C
have rw₄ : M ／ C ↾ (M.E \ D) \ C = M ／ C ↾ (M.E \ D) \ C
Tactic: rw [delete_eq_restrict, delete_eq_restrict, contract_ground, diff_diff_comm,
    restrict_contract_eq_contract_restrict _ (by simpa [hCE, subset_diff])]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
C D : Set α
⊢ M ／ C ＼ D = M ＼ (D \ C) ／ C
have rw : M ／ C ＼ (D \ C) = M ＼ (D \ C) ／ C
Tactic: rw [contract_delete_diff, contract_delete_comm _ disjoint_sdiff_right]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
C D : Set α
rw : M ／ C ＼ (D \ C) = M ＼ (D \ C) ／ C
⊢ M ／ C ＼ D = M ＼ (D \ C) ／ C
have rw₁ : M ＼ (D \ C) ／ C = M ＼ (D \ C) ／ C
Tactic: rw [contract_delete_diff, contract_delete_comm _ disjoint_sdiff_right]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
D C : Set α
⊢ M ＼ D ／ C = M ＼ D ／ (C \ D)
have rw : C ∩ (M ＼ D).E = C \ D ∩ (M ＼ D).E
Tactic: rw [contract_eq_contract_iff, delete_ground, ← diff_inter_distrib_right, diff_eq, diff_eq,
    inter_assoc]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
D C : Set α
rw : C ∩ (M ＼ D).E = C \ D ∩ (M ＼ D).E
⊢ M ＼ D ／ C = M ＼ D ／ (C \ D)
have rw₁ : C ∩ (M.E \ D) = C \ D ∩ (M.E \ D)
Tactic: rw [contract_eq_contract_iff, delete_ground, ← diff_inter_distrib_right, diff_eq, diff_eq,
    inter_assoc]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
D C : Set α
rw : C ∩ (M ＼ D).E = C \ D ∩ (M ＼ D).E
rw₁ : C ∩ (M.E \ D) = C \ D ∩ (M.E \ D)
⊢ M ＼ D ／ C = M ＼ D ／ (C \ D)
have rw₂ : C ∩ (M.E \ D) = (C ∩ M.E) \ D
Tactic: rw [contract_eq_contract_iff, delete_ground, ← diff_inter_distrib_right, diff_eq, diff_eq,
    inter_assoc]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
D C : Set α
rw : C ∩ (M ＼ D).E = C \ D ∩ (M ＼ D).E
rw₁ : C ∩ (M.E \ D) = C \ D ∩ (M.E \ D)
rw₂ : C ∩ (M.E \ D) = (C ∩ M.E) \ D
⊢ M ＼ D ／ C = M ＼ D ／ (C \ D)
have rw₃ : C ∩ (M.E ∩ Dᶜ) = (C ∩ M.E) \ D
Tactic: rw [contract_eq_contract_iff, delete_ground, ← diff_inter_distrib_right, diff_eq, diff_eq,
    inter_assoc]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
D C : Set α
rw : C ∩ (M ＼ D).E = C \ D ∩ (M ＼ D).E
rw₁ : C ∩ (M.E \ D) = C \ D ∩ (M.E \ D)
rw₂ : C ∩ (M.E \ D) = (C ∩ M.E) \ D
rw₃ : C ∩ (M.E ∩ Dᶜ) = (C ∩ M.E) \ D
⊢ M ＼ D ／ C = M ＼ D ／ (C \ D)
have rw₄ : C ∩ (M.E ∩ Dᶜ) = C ∩ M.E ∩ Dᶜ
Tactic: rw [contract_eq_contract_iff, delete_ground, ← diff_inter_distrib_right, diff_eq, diff_eq,
    inter_assoc]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
D C : Set α
rw : C ∩ (M ＼ D).E = C \ D ∩ (M ＼ D).E
rw₁ : C ∩ (M.E \ D) = C \ D ∩ (M.E \ D)
rw₂ : C ∩ (M.E \ D) = (C ∩ M.E) \ D
rw₃ : C ∩ (M.E ∩ Dᶜ) = (C ∩ M.E) \ D
rw₄ : C ∩ (M.E ∩ Dᶜ) = C ∩ M.E ∩ Dᶜ
⊢ M ＼ D ／ C = M ＼ D ／ (C \ D)
have rw₅ : C ∩ (M.E ∩ Dᶜ) = C ∩ (M.E ∩ Dᶜ)
Tactic: rw [contract_eq_contract_iff, delete_ground, ← diff_inter_distrib_right, diff_eq, diff_eq,
    inter_assoc]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
D C : Set α
⊢ M ＼ D ／ C = M ／ (C \ D) ＼ D
have rw : M ＼ D ／ (C \ D) = M ／ (C \ D) ＼ D
Tactic: rw [delete_contract_eq_diff, ← contract_delete_comm _ disjoint_sdiff_left]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
D C : Set α
rw : M ＼ D ／ (C \ D) = M ／ (C \ D) ＼ D
⊢ M ＼ D ／ C = M ／ (C \ D) ＼ D
have rw₁ : M ／ (C \ D) ＼ D = M ／ (C \ D) ＼ D
Tactic: rw [delete_contract_eq_diff, ← contract_delete_comm _ disjoint_sdiff_left]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
C D C' : Set α
⊢ M ／ C ＼ D ／ C' = M ／ (C ∪ C' \ D) ＼ D
have rw : M ／ C ＼ D ／ (C' \ D) = M ／ (C ∪ C' \ D) ＼ D
Tactic: rw [delete_contract_eq_diff, ← contract_delete_comm _ disjoint_sdiff_left, contract_contract]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
C D C' : Set α
rw : M ／ C ＼ D ／ (C' \ D) = M ／ (C ∪ C' \ D) ＼ D
⊢ M ／ C ＼ D ／ C' = M ／ (C ∪ C' \ D) ＼ D
have rw₁ : M ／ C ／ (C' \ D) ＼ D = M ／ (C ∪ C' \ D) ＼ D
Tactic: rw [delete_contract_eq_diff, ← contract_delete_comm _ disjoint_sdiff_left, contract_contract]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
C D C' : Set α
rw : M ／ C ＼ D ／ (C' \ D) = M ／ (C ∪ C' \ D) ＼ D
rw₁ : M ／ C ／ (C' \ D) ＼ D = M ／ (C ∪ C' \ D) ＼ D
⊢ M ／ C ＼ D ／ C' = M ／ (C ∪ C' \ D) ＼ D
have rw₂ : M ／ (C ∪ C' \ D) ＼ D = M ／ (C ∪ C' \ D) ＼ D
Tactic: rw [delete_contract_eq_diff, ← contract_delete_comm _ disjoint_sdiff_left, contract_contract]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
C D C' : Set α
h : Disjoint C' D
⊢ M ／ C ＼ D ／ C' = M ／ (C ∪ C') ＼ D
have rw : M ／ (C ∪ C' \ D) ＼ D = M ／ (C ∪ C') ＼ D
Tactic: rw [contract_delete_contract', sdiff_eq_left.mpr h]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
C D C' : Set α
h : Disjoint C' D
rw : M ／ (C ∪ C' \ D) ＼ D = M ／ (C ∪ C') ＼ D
⊢ M ／ C ＼ D ／ C' = M ／ (C ∪ C') ＼ D
have rw₁ : M ／ (C ∪ C') ＼ D = M ／ (C ∪ C') ＼ D
Tactic: rw [contract_delete_contract', sdiff_eq_left.mpr h]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
C D C' D' : Set α
⊢ M ／ C ＼ D ／ C' ＼ D' = M ／ (C ∪ C' \ D) ＼ (D ∪ D')
have rw : M ／ (C ∪ C' \ D) ＼ D ＼ D' = M ／ (C ∪ C' \ D) ＼ (D ∪ D')
Tactic: rw [contract_delete_contract', delete_delete]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
C D C' D' : Set α
rw : M ／ (C ∪ C' \ D) ＼ D ＼ D' = M ／ (C ∪ C' \ D) ＼ (D ∪ D')
⊢ M ／ C ＼ D ／ C' ＼ D' = M ／ (C ∪ C' \ D) ＼ (D ∪ D')
have rw₁ : M ／ (C ∪ C' \ D) ＼ (D ∪ D') = M ／ (C ∪ C' \ D) ＼ (D ∪ D')
Tactic: rw [contract_delete_contract', delete_delete]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
C D C' D' : Set α
h : Disjoint C' D
⊢ M ／ C ＼ D ／ C' ＼ D' = M ／ (C ∪ C') ＼ (D ∪ D')
have rw : M ／ (C ∪ C' \ D) ＼ (D ∪ D') = M ／ (C ∪ C') ＼ (D ∪ D')
Tactic: rw [contract_delete_contract_delete', sdiff_eq_left.mpr h]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
C D C' D' : Set α
h : Disjoint C' D
rw : M ／ (C ∪ C' \ D) ＼ (D ∪ D') = M ／ (C ∪ C') ＼ (D ∪ D')
⊢ M ／ C ＼ D ／ C' ＼ D' = M ／ (C ∪ C') ＼ (D ∪ D')
have rw₁ : M ／ (C ∪ C') ＼ (D ∪ D') = M ／ (C ∪ C') ＼ (D ∪ D')
Tactic: rw [contract_delete_contract_delete', sdiff_eq_left.mpr h]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
D C D' : Set α
⊢ M ＼ D ／ C ＼ D' = M ／ (C \ D) ＼ (D ∪ D')
have rw : M ／ (C \ D) ＼ D ＼ D' = M ／ (C \ D) ＼ (D ∪ D')
Tactic: rw [delete_contract_comm', delete_delete]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
D C D' : Set α
rw : M ／ (C \ D) ＼ D ＼ D' = M ／ (C \ D) ＼ (D ∪ D')
⊢ M ＼ D ／ C ＼ D' = M ／ (C \ D) ＼ (D ∪ D')
have rw₁ : M ／ (C \ D) ＼ (D ∪ D') = M ／ (C \ D) ＼ (D ∪ D')
Tactic: rw [delete_contract_comm', delete_delete]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
D C D' : Set α
h : Disjoint C D
⊢ M ＼ D ／ C ＼ D' = M ／ C ＼ (D ∪ D')
have rw : M ／ (C \ D) ＼ (D ∪ D') = M ／ C ＼ (D ∪ D')
Tactic: rw [delete_contract_delete', sdiff_eq_left.mpr h]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
D C D' : Set α
h : Disjoint C D
rw : M ／ (C \ D) ＼ (D ∪ D') = M ／ C ＼ (D ∪ D')
⊢ M ＼ D ／ C ＼ D' = M ／ C ＼ (D ∪ D')
have rw₁ : M ／ C ＼ (D ∪ D') = M ／ C ＼ (D ∪ D')
Tactic: rw [delete_contract_delete', sdiff_eq_left.mpr h]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (goal)
Goal:
α : Type u_1
M : Matroid α
R : Set α
hR : R ⊆ M.E
⊢ M ＼ (M.E \ R) = M ↾ R
have rw : M ↾ M.E \ (M.E \ R) = M ↾ R
Tactic: rw [← restrict_compl, diff_diff_cancel_left hR]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (goal)
Goal:
α : Type u_1
M : Matroid α
R : Set α
hR : R ⊆ M.E
rw : M ↾ M.E \ (M.E \ R) = M ↾ R
⊢ M ＼ (M.E \ R) = M ↾ R
have rw₁ : M ↾ R = M ↾ R
Tactic: rw [← restrict_compl, diff_diff_cancel_left hR]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (goal)
Goal:
α : Type u_1
M N : Matroid α
hNM : N ≤r M
⊢ N = M ＼ (M.E \ N.E)
have obtain : ∀ (R : Set α) (hR : R ⊆ M.E), M ↾ R = M ＼ (M.E \ (M ↾ R).E)
Tactic: obtain ⟨R, hR, rfl⟩ := hNM
Cleared hypotheses: N, hNM
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (goal)
Goal:
α : Type u_1
M : Matroid α
R : Set α
hR : R ⊆ M.E
⊢ M ↾ R = M ＼ (M.E \ (M ↾ R).E)
have rw : M ↾ R = M ↾ (M ↾ R).E
Tactic: rw [delete_compl, restrict_ground_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (goal)
Goal:
α : Type u_1
M : Matroid α
R : Set α
hR : R ⊆ M.E
rw : M ↾ R = M ↾ (M ↾ R).E
⊢ M ↾ R = M ＼ (M.E \ (M ↾ R).E)
have rw₁ : M ↾ R = M ↾ R
Tactic: rw [delete_compl, restrict_ground_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (goal)
Goal:
α : Type u_1
M : Matroid α
D : Set α
⊢ M ＼ D = M ↔ Disjoint D M.E
have rw : M ↾ M.E \ D = M ↔ Disjoint D M.E
Tactic: rw [← restrict_compl, restrict_eq_self_iff, sdiff_eq_left, disjoint_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (goal)
Goal:
α : Type u_1
M : Matroid α
D : Set α
rw : M ↾ M.E \ D = M ↔ Disjoint D M.E
⊢ M ＼ D = M ↔ Disjoint D M.E
have rw₁ : M.E \ D = M.E ↔ Disjoint D M.E
Tactic: rw [← restrict_compl, restrict_eq_self_iff, sdiff_eq_left, disjoint_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (goal)
Goal:
α : Type u_1
M : Matroid α
D : Set α
rw : M ↾ M.E \ D = M ↔ Disjoint D M.E
rw₁ : M.E \ D = M.E ↔ Disjoint D M.E
⊢ M ＼ D = M ↔ Disjoint D M.E
have rw₂ : Disjoint M.E D ↔ Disjoint D M.E
Tactic: rw [← restrict_compl, restrict_eq_self_iff, sdiff_eq_left, disjoint_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (goal)
Goal:
α : Type u_1
M : Matroid α
D : Set α
rw : M ↾ M.E \ D = M ↔ Disjoint D M.E
rw₁ : M.E \ D = M.E ↔ Disjoint D M.E
rw₂ : Disjoint M.E D ↔ Disjoint D M.E
⊢ M ＼ D = M ↔ Disjoint D M.E
have rw₃ : Disjoint D M.E ↔ Disjoint D M.E
Tactic: rw [← restrict_compl, restrict_eq_self_iff, sdiff_eq_left, disjoint_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (goal)
Goal:
α : Type u_1
M : Matroid α
D₁ D₂ : Set α
⊢ M ＼ D₁ ＼ D₂ = M ＼ (D₁ ∪ D₂)
have hR : (M ↾ M.E \ D₁).E \ D₂ ⊆ M.E \ D₁
Tactic: rw [← restrict_compl, ← restrict_compl, ← restrict_compl, restrict_restrict_eq,
    restrict_ground_eq, diff_diff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (goal)
Goal:
α : Type u_1
M : Matroid α
D₁ D₂ : Set α
⊢ M ＼ D₁ ＼ D₂ = M ＼ D₂ ＼ D₁
have rw : M ＼ (D₁ ∪ D₂) = M ＼ D₂ ＼ D₁
Tactic: rw [delete_delete, union_comm, delete_delete]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (goal)
Goal:
α : Type u_1
M : Matroid α
D₁ D₂ : Set α
rw : M ＼ (D₁ ∪ D₂) = M ＼ D₂ ＼ D₁
⊢ M ＼ D₁ ＼ D₂ = M ＼ D₂ ＼ D₁
have rw₁ : M ＼ (D₂ ∪ D₁) = M ＼ D₂ ＼ D₁
Tactic: rw [delete_delete, union_comm, delete_delete]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (goal)
Goal:
α : Type u_1
M : Matroid α
D₁ D₂ : Set α
rw : M ＼ (D₁ ∪ D₂) = M ＼ D₂ ＼ D₁
rw₁ : M ＼ (D₂ ∪ D₁) = M ＼ D₂ ＼ D₁
⊢ M ＼ D₁ ＼ D₂ = M ＼ D₂ ＼ D₁
have rw₂ : M ＼ (D₂ ∪ D₁) = M ＼ (D₂ ∪ D₁)
Tactic: rw [delete_delete, union_comm, delete_delete]