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 : Set α
⊢ M ／ M.closure C = M ／ C ＼ (M.closure C \ C)
have 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)
Tactic: wlog hCE : C ⊆ M.E with aux
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
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)
⊢ M ／ M.closure C = M ／ C ＼ (M.closure C \ C)
have wlog : ∀ {α : Type u_1} (M : Matroid α) (C : Set α) (hCE : C ⊆ M.E), M ／ M.closure C = M ／ C ＼ (M.closure C \ C)
Tactic: wlog hCE : C ⊆ M.E with aux
Cleared hypotheses: M, C
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
C : Set α
aux : ∀ {α : Type u_1} (M : Matroid α) (C : Set α) (hCE : C ⊆ M.E), M ／ M.closure C = M ／ C ＼ (M.closure C \ C)
hCE : ¬C ⊆ M.E
⊢ M ／ M.closure C = M ／ C ＼ (M.closure C \ C)
have inr : M ／ M.closure C = M ／ (C ∩ M.E) ＼ (M.closure C \ C)
Tactic: rw [← M.contract_inter_ground_eq C, ← closure_inter_ground, aux _ _ inter_subset_right,
      diff_inter, diff_eq_empty.2 (M.closure_subset_ground _), union_empty]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
C : Set α
aux : ∀ {α : Type u_1} (M : Matroid α) (C : Set α) (hCE : C ⊆ M.E), M ／ M.closure C = M ／ C ＼ (M.closure C \ C)
hCE : ¬C ⊆ M.E
inr : M ／ M.closure C = M ／ (C ∩ M.E) ＼ (M.closure C \ C)
⊢ M ／ M.closure C = M ／ C ＼ (M.closure C \ C)
have inr₁ : M ／ M.closure (C ∩ M.E) = M ／ (C ∩ M.E) ＼ (M.closure (C ∩ M.E) \ C)
Tactic: rw [← M.contract_inter_ground_eq C, ← closure_inter_ground, aux _ _ inter_subset_right,
      diff_inter, diff_eq_empty.2 (M.closure_subset_ground _), union_empty]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
C : Set α
aux : ∀ {α : Type u_1} (M : Matroid α) (C : Set α) (hCE : C ⊆ M.E), M ／ M.closure C = M ／ C ＼ (M.closure C \ C)
hCE : ¬C ⊆ M.E
inr : M ／ M.closure C = M ／ (C ∩ M.E) ＼ (M.closure C \ C)
inr₁ : M ／ M.closure (C ∩ M.E) = M ／ (C ∩ M.E) ＼ (M.closure (C ∩ M.E) \ C)
⊢ M ／ M.closure C = M ／ C ＼ (M.closure C \ C)
have inr₂ : M ／ (C ∩ M.E) ＼ (M.closure (C ∩ M.E) \ (C ∩ M.E)) = M ／ (C ∩ M.E) ＼ (M.closure (C ∩ M.E) \ C)
Tactic: rw [← M.contract_inter_ground_eq C, ← closure_inter_ground, aux _ _ inter_subset_right,
      diff_inter, diff_eq_empty.2 (M.closure_subset_ground _), union_empty]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
C : Set α
aux : ∀ {α : Type u_1} (M : Matroid α) (C : Set α) (hCE : C ⊆ M.E), M ／ M.closure C = M ／ C ＼ (M.closure C \ C)
hCE : ¬C ⊆ M.E
inr : M ／ M.closure C = M ／ (C ∩ M.E) ＼ (M.closure C \ C)
inr₁ : M ／ M.closure (C ∩ M.E) = M ／ (C ∩ M.E) ＼ (M.closure (C ∩ M.E) \ C)
inr₂ : M ／ (C ∩ M.E) ＼ (M.closure (C ∩ M.E) \ (C ∩ M.E)) = M ／ (C ∩ M.E) ＼ (M.closure (C ∩ M.E) \ C)
⊢ M ／ M.closure C = M ／ C ＼ (M.closure C \ C)
have inr₃ : M ／ (C ∩ M.E) ＼ (M.closure (C ∩ M.E) \ C ∪ M.closure (C ∩ M.E) \ M.E) = M ／ (C ∩ M.E) ＼ (M.closure (C ∩ M.E) \ C)
Tactic: rw [← M.contract_inter_ground_eq C, ← closure_inter_ground, aux _ _ inter_subset_right,
      diff_inter, diff_eq_empty.2 (M.closure_subset_ground _), union_empty]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
C : Set α
aux : ∀ {α : Type u_1} (M : Matroid α) (C : Set α) (hCE : C ⊆ M.E), M ／ M.closure C = M ／ C ＼ (M.closure C \ C)
hCE : ¬C ⊆ M.E
inr : M ／ M.closure C = M ／ (C ∩ M.E) ＼ (M.closure C \ C)
inr₁ : M ／ M.closure (C ∩ M.E) = M ／ (C ∩ M.E) ＼ (M.closure (C ∩ M.E) \ C)
inr₂ : M ／ (C ∩ M.E) ＼ (M.closure (C ∩ M.E) \ (C ∩ M.E)) = M ／ (C ∩ M.E) ＼ (M.closure (C ∩ M.E) \ C)
inr₃ : M ／ (C ∩ M.E) ＼ (M.closure (C ∩ M.E) \ C ∪ M.closure (C ∩ M.E) \ M.E) = M ／ (C ∩ M.E) ＼ (M.closure (C ∩ M.E) \ C)
⊢ M ／ M.closure C = M ／ C ＼ (M.closure C \ C)
have inr₄ : M ／ (C ∩ M.E) ＼ (M.closure (C ∩ M.E) \ C ∪ ∅) = M ／ (C ∩ M.E) ＼ (M.closure (C ∩ M.E) \ C)
Tactic: rw [← M.contract_inter_ground_eq C, ← closure_inter_ground, aux _ _ inter_subset_right,
      diff_inter, diff_eq_empty.2 (M.closure_subset_ground _), union_empty]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
C : Set α
aux : ∀ {α : Type u_1} (M : Matroid α) (C : Set α) (hCE : C ⊆ M.E), M ／ M.closure C = M ／ C ＼ (M.closure C \ C)
hCE : ¬C ⊆ M.E
inr : M ／ M.closure C = M ／ (C ∩ M.E) ＼ (M.closure C \ C)
inr₁ : M ／ M.closure (C ∩ M.E) = M ／ (C ∩ M.E) ＼ (M.closure (C ∩ M.E) \ C)
inr₂ : M ／ (C ∩ M.E) ＼ (M.closure (C ∩ M.E) \ (C ∩ M.E)) = M ／ (C ∩ M.E) ＼ (M.closure (C ∩ M.E) \ C)
inr₃ : M ／ (C ∩ M.E) ＼ (M.closure (C ∩ M.E) \ C ∪ M.closure (C ∩ M.E) \ M.E) = M ／ (C ∩ M.E) ＼ (M.closure (C ∩ M.E) \ C)
inr₄ : M ／ (C ∩ M.E) ＼ (M.closure (C ∩ M.E) \ C ∪ ∅) = M ／ (C ∩ M.E) ＼ (M.closure (C ∩ M.E) \ C)
⊢ M ／ M.closure C = M ／ C ＼ (M.closure C \ C)
have inr₅ : M ／ (C ∩ M.E) ＼ (M.closure (C ∩ M.E) \ C) = M ／ (C ∩ M.E) ＼ (M.closure (C ∩ M.E) \ C)
Tactic: rw [← M.contract_inter_ground_eq C, ← closure_inter_ground, aux _ _ inter_subset_right,
      diff_inter, diff_eq_empty.2 (M.closure_subset_ground _), union_empty]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α_1 α : Type u_1
M : Matroid α
C : Set α
hCE : C ⊆ M.E
⊢ M ／ M.closure C = M ／ C ＼ (M.closure C \ C)
have obtain : ∀ (I : Set α) (hI : M.IsBasis I C), M ／ M.closure C = M ／ C ＼ (M.closure C \ C)
Tactic: obtain ⟨I, hI⟩ := M.exists_isBasis C
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α_1 α : Type u_1
M : Matroid α
C : Set α
hCE : C ⊆ M.E
I : Set α
hI : M.IsBasis I C
⊢ M ／ M.closure C = M ／ C ＼ (M.closure C \ C)
have rw : M ／ I ＼ (M.closure C \ I) = M ／ C ＼ (M.closure C \ C)
Tactic: rw [hI.isBasis_closure_right.contract_eq_contract_delete, hI.contract_eq_contract_delete,
    delete_delete, union_comm, diff_union_diff_cancel (M.subset_closure C) hI.subset]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α_1 α : Type u_1
M : Matroid α
C : Set α
hCE : C ⊆ M.E
I : Set α
hI : M.IsBasis I C
rw : M ／ I ＼ (M.closure C \ I) = M ／ C ＼ (M.closure C \ C)
⊢ M ／ M.closure C = M ／ C ＼ (M.closure C \ C)
have rw₁ : M ／ I ＼ (M.closure C \ I) = M ／ I ＼ (C \ I) ＼ (M.closure C \ C)
Tactic: rw [hI.isBasis_closure_right.contract_eq_contract_delete, hI.contract_eq_contract_delete,
    delete_delete, union_comm, diff_union_diff_cancel (M.subset_closure C) hI.subset]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α_1 α : Type u_1
M : Matroid α
C : Set α
hCE : C ⊆ M.E
I : Set α
hI : M.IsBasis I C
rw : M ／ I ＼ (M.closure C \ I) = M ／ C ＼ (M.closure C \ C)
rw₁ : M ／ I ＼ (M.closure C \ I) = M ／ I ＼ (C \ I) ＼ (M.closure C \ C)
⊢ M ／ M.closure C = M ／ C ＼ (M.closure C \ C)
have rw₂ : M ／ I ＼ (M.closure C \ I) = M ／ I ＼ (C \ I ∪ M.closure C \ C)
Tactic: rw [hI.isBasis_closure_right.contract_eq_contract_delete, hI.contract_eq_contract_delete,
    delete_delete, union_comm, diff_union_diff_cancel (M.subset_closure C) hI.subset]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α_1 α : Type u_1
M : Matroid α
C : Set α
hCE : C ⊆ M.E
I : Set α
hI : M.IsBasis I C
rw : M ／ I ＼ (M.closure C \ I) = M ／ C ＼ (M.closure C \ C)
rw₁ : M ／ I ＼ (M.closure C \ I) = M ／ I ＼ (C \ I) ＼ (M.closure C \ C)
rw₂ : M ／ I ＼ (M.closure C \ I) = M ／ I ＼ (C \ I ∪ M.closure C \ C)
⊢ M ／ M.closure C = M ／ C ＼ (M.closure C \ C)
have rw₃ : M ／ I ＼ (M.closure C \ I) = M ／ I ＼ (M.closure C \ C ∪ C \ I)
Tactic: rw [hI.isBasis_closure_right.contract_eq_contract_delete, hI.contract_eq_contract_delete,
    delete_delete, union_comm, diff_union_diff_cancel (M.subset_closure C) hI.subset]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α_1 α : Type u_1
M : Matroid α
C : Set α
hCE : C ⊆ M.E
I : Set α
hI : M.IsBasis I C
rw : M ／ I ＼ (M.closure C \ I) = M ／ C ＼ (M.closure C \ C)
rw₁ : M ／ I ＼ (M.closure C \ I) = M ／ I ＼ (C \ I) ＼ (M.closure C \ C)
rw₂ : M ／ I ＼ (M.closure C \ I) = M ／ I ＼ (C \ I ∪ M.closure C \ C)
rw₃ : M ／ I ＼ (M.closure C \ I) = M ／ I ＼ (M.closure C \ C ∪ C \ I)
⊢ M ／ M.closure C = M ／ C ＼ (M.closure C \ C)
have rw₄ : M ／ I ＼ (M.closure C \ I) = M ／ I ＼ (M.closure C \ I)
Tactic: rw [hI.isBasis_closure_right.contract_eq_contract_delete, hI.contract_eq_contract_delete,
    delete_delete, union_comm, diff_union_diff_cancel (M.subset_closure C) hI.subset]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
C X : Set α
⊢ (M ／ C).closure X = M.closure (X ∪ C) \ C
have rw : (M ／ C).closure X \ ((M ／ C).closure X \ X) ⊆ M.closure (C ∪ X) \ C ∩ X ∧ M.closure (C ∪ X) \ C ∩ X ⊆ (M ／ C).closure X
Tactic: rw [← diff_union_inter (M.closure (X ∪ C) \ C) X, diff_diff, union_comm C, ← contract_loops_eq,
    union_comm X, ← contract_contract, contract_loops_eq, subset_antisymm_iff, union_subset_iff,
    and_iff_right diff_subset, ← diff_subset_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
C X : Set α
⊢ (M ／ C).closure X \ ((M ／ C).closure X \ X) ⊆ M.closure (C ∪ X) \ C ∩ X ∧
    M.closure (C ∪ X) \ C ∩ X ⊆ (M ／ C).closure X
have simp : (M ／ C).closure X ∩ X ⊆ M.closure (C ∪ X) \ C ∧ M.closure (C ∪ X) \ C ∩ X ⊆ (M ／ C).closure X
Tactic: simp only [sdiff_sdiff_right_self, inf_eq_inter, subset_inter_iff, inter_subset_right, and_true]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
X C : Set α
hC : C ⊆ M.E
⊢ (M ／ C).Spanning X ↔ M.Spanning (X ∪ C) ∧ Disjoint X C
have rw : Disjoint X C → X ⊆ M.E → (M.closure (X ∪ C) \ C = M.E \ C ↔ M.closure (X ∪ C) = M.E ∧ C ⊆ M.E)
Tactic: rw [spanning_iff, contract_closure_eq, contract_ground, spanning_iff, union_subset_iff,
    subset_diff, ← and_assoc, and_congr_left_iff, and_comm (a := X ⊆ _), ← and_assoc,
    and_congr_left_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
X C : Set α
hC : C ⊆ M.E
⊢ Disjoint X C → X ⊆ M.E → (M.closure (X ∪ C) \ C = M.E \ C ↔ M.closure (X ∪ C) = M.E ∧ C ⊆ M.E)
have refine : ∀ (hdj : Disjoint X C) (hX : X ⊆ M.E) (h : M.closure (X ∪ C) \ C = M.E \ C), M.closure (X ∪ C) = M.E
Tactic: refine fun hdj hX ↦ ⟨fun h ↦ ⟨?_, hC⟩, fun h ↦ by simp [h]⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
X C : Set α
hC : C ⊆ M.E
hdj : Disjoint X C
hX : X ⊆ M.E
h : M.closure (X ∪ C) \ C = M.E \ C
⊢ M.closure (X ∪ C) = M.E
have rwa : C ∪ M.closure (X ∪ C) \ C = M.E
Tactic: rwa [← union_diff_cancel (M.subset_closure_of_subset' subset_union_right hC), h,
    union_diff_cancel]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
X C : Set α
hC : C ⊆ M.E
hdj : Disjoint X C
hX : X ⊆ M.E
h : M.closure (X ∪ C) \ C = M.E \ C
rwa : C ∪ M.closure (X ∪ C) \ C = M.E
⊢ M.closure (X ∪ C) = M.E
have rwa₁ : C ∪ M.E \ C = M.E
Tactic: rwa [← union_diff_cancel (M.subset_closure_of_subset' subset_union_right hC), h,
    union_diff_cancel]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
X C : Set α
hC : C ⊆ M.E
hdj : Disjoint X C
hX : X ⊆ M.E
h : M.closure (X ∪ C) \ C = M.E \ C
rwa : C ∪ M.closure (X ∪ C) \ C = M.E
rwa₁ : C ∪ M.E \ C = M.E
⊢ M.closure (X ∪ C) = M.E
have rwa₂ : M.E = M.E
Tactic: rwa [← union_diff_cancel (M.subset_closure_of_subset' subset_union_right hC), h,
    union_diff_cancel]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
X C : Set α
⊢ (M ／ C).Spanning X ↔ M.Spanning (X ∪ C ∩ M.E) ∧ Disjoint X C
have rw : M.Spanning (X ∪ C ∩ M.E) → (Disjoint X (C ∩ M.E) ↔ Disjoint X C)
Tactic: rw [← contract_inter_ground_eq, contract_spanning_iff, and_congr_right_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
X C : Set α
⊢ M.Spanning (X ∪ C ∩ M.E) → (Disjoint X (C ∩ M.E) ↔ Disjoint X C)
have refine : ∀ (h : M.Spanning (X ∪ C ∩ M.E)) (hdj : Disjoint X (C ∩ M.E)), Disjoint X C
Tactic: refine fun h ↦ ⟨fun hdj ↦ ?_, Disjoint.mono_right inter_subset_left⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
X C : Set α
h : M.Spanning (X ∪ C ∩ M.E)
hdj : Disjoint X (C ∩ M.E)
⊢ Disjoint X C
have rw : Disjoint X (C \ M.E)
Tactic: rw [← diff_union_inter C M.E, disjoint_union_right, and_iff_left hdj]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (hypothesis)
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : M.Spanning X
C : Set α
⊢ (M ／ C).Spanning (X \ C)
have hXE : X ⊆ M.E
Tactic: have hXE := hX.subset_ground
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : M.Spanning X
C : Set α
hXE : X ⊆ M.E
⊢ (M ／ C).Spanning (X \ C)
have rw : M.Spanning (X \ C ∪ C ∩ M.E)
Tactic: rw [contract_spanning_iff', and_iff_left disjoint_sdiff_left]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : M.Spanning X
C : Set α
hXE : X ⊆ M.E
⊢ X ⊆ X \ C ∪ C ∩ M.E
have tauto_set : ∀ (hXE : ∀ x ∈ X, x ∈ M.E), ∀ x ∈ X, True ∧ x ∉ C ∨ x ∈ C ∧ True
Tactic: tauto_set
Cleared hypotheses: hXE
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : M.Spanning X
C : Set α
hXE : X ⊆ M.E
⊢ X \ C ∪ C ∩ M.E ⊆ M.E
have tauto_set : ∀ (hXE : ∀ x ∈ X, x ∈ M.E) (x : α), x ∈ X ∧ x ∉ C ∨ x ∈ C ∧ x ∈ M.E → x ∈ M.E
Tactic: tauto_set
Cleared hypotheses: hXE
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : M.Spanning X
⊢ M ／ X = loopyOn (M.E \ X)
have rw : (M ／ X).loops = M.E \ X ∧ (M ／ X).E = M.E \ X
Tactic: rw [eq_loopyOn_iff_loops_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
K C : Set α
hK : M.IsCircuit K
hC : C ⊂ K
⊢ (M ／ C).IsCircuit (K \ C)
have suffices : ∀ e ∈ K, e ∉ C → M.Indep (K \ {e} ∪ C)
Tactic: suffices ∀ e ∈ K, e ∉ C → M.Indep (K \ {e} ∪ C) by
    simpa [isCircuit_iff_dep_forall_diff_singleton_indep, diff_diff_comm (s := K) (t := C),
    dep_iff, (hK.ssubset_indep hC).contract_indep_iff, diff_subset_diff_left hK.subset_ground,
    disjoint_sdiff_left, diff_union_of_subset hC.subset, hK.not_indep]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
K C : Set α
hK : M.IsCircuit K
hCK : Disjoint C K
⊢ (M ／ C).Dep K
have obtain : ∀ (I : Set α) (hI : M.IsBasis I (C ∩ M.E)), (M ／ C).Dep K
Tactic: obtain ⟨I, hI⟩ := M.exists_isBasis (C ∩ M.E)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
K C : Set α
hK : M.IsCircuit K
hCK : Disjoint C K
I : Set α
hI : M.IsBasis I (C ∩ M.E)
⊢ (M ／ C).Dep K
have rw : ¬M.Indep (K ∪ I)
Tactic: rw [← contract_inter_ground_eq, Dep, hI.contract_indep_iff,
    and_iff_left (hCK.mono_left inter_subset_left), contract_ground, subset_diff,
    and_iff_left (hCK.symm.mono_right inter_subset_left), and_iff_left hK.subset_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (hypothesis)
Goal:
α : Type u_1
M : Matroid α
K : Set α
hK : M.IsCircuit K
C : Set α
hKC : ¬K ⊆ C
⊢ (M ／ C).Dep (K \ C)
have h' : (M ／ (C ∩ K)).IsCircuit (K \ (C ∩ K))
Tactic: have h' := hK.contract_isCircuit (C := C ∩ K) (inter_subset_right.ssubset_of_ne (by simpa))
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (hypothesis)
Goal:
α : Type u_1
M : Matroid α
K : Set α
hK : M.IsCircuit K
C : Set α
hKC : ¬K ⊆ C
h' : (M ／ (C ∩ K)).IsCircuit (K \ (C ∩ K))
⊢ (M ／ C).Dep (K \ C)
have h'₁ : (M ／ (C ∩ K)).IsCircuit (K \ C)
Tactic: simp only [diff_inter_self_eq_diff] at h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (hypothesis)
Goal:
α : Type u_1
M : Matroid α
K : Set α
hK : M.IsCircuit K
C : Set α
hKC : ¬K ⊆ C
h' : (M ／ (C ∩ K)).IsCircuit (K \ C)
⊢ (M ／ C).Dep (K \ C)
have hwin : (M ／ (C ∩ K) ／ (C \ K)).Dep (K \ C)
Tactic: have hwin := h'.contract_dep (C := C \ K) disjoint_sdiff_sdiff
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
K : Set α
hK : M.IsCircuit K
C : Set α
hKC : ¬K ⊆ C
h' : (M ／ (C ∩ K)).IsCircuit (K \ C)
hwin : (M ／ (C ∩ K) ／ (C \ K)).Dep (K \ C)
⊢ (M ／ C).Dep (K \ C)
have rwa : ∀ (hwin : (M ／ (C ∩ K ∪ C \ K)).Dep (K \ C)), (M ／ C).Dep (K \ C)
Tactic: rwa [contract_contract, inter_union_diff] at hwin
Cleared hypotheses: hwin
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
K : Set α
hK : M.IsCircuit K
C : Set α
hKC : ¬K ⊆ C
h' : (M ／ (C ∩ K)).IsCircuit (K \ C)
hwin : (M ／ (C ∩ K) ／ (C \ K)).Dep (K \ C)
rwa : ∀ (hwin : (M ／ (C ∩ K ∪ C \ K)).Dep (K \ C)), (M ／ C).Dep (K \ C)
⊢ (M ／ C).Dep (K \ C)
have rwa₁ : ∀ (hwin : (M ／ C).Dep (K \ C)), (M ／ C).Dep (K \ C)
Tactic: rwa [contract_contract, inter_union_diff] at hwin
Cleared hypotheses: hwin
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
K C : Set α
hC : M.IsCircuit C
hK : K.Nonempty
hKC : K ⊆ C
⊢ C \ K ⊂ C
have rwa : (C ∩ K).Nonempty
Tactic: rwa [diff_ssubset_left_iff, inter_eq_self_of_subset_right hKC]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
K C : Set α
hC : (M ／ K).IsCircuit C
⊢ ∃ (C' : Set α), M.IsCircuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K
have inr : ∀
  (aux :
    ∀ {K : Set α} (hC : (M ／ K).IsCircuit C) (hKi : M.Indep K), ∃ (C' : Set α), M.IsCircuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K)
  (hKi : ¬M.Indep K), ∃ (C' : Set α), M.IsCircuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K
Tactic: wlog hKi : M.Indep K generalizing K with aux
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
K C : Set α
hC : (M ／ K).IsCircuit C
inr :
  ∀
    (aux :
      ∀ {K : Set α} (hC : (M ／ K).IsCircuit C) (hKi : M.Indep K), ∃ (C' : Set α), M.IsCircuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K)
    (hKi : ¬M.Indep K), ∃ (C' : Set α), M.IsCircuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K
⊢ ∃ (C' : Set α), M.IsCircuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K
have wlog : ∀ {K : Set α} (hC : (M ／ K).IsCircuit C) (hKi : M.Indep K), ∃ (C' : Set α), M.IsCircuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K
Tactic: wlog hKi : M.Indep K generalizing K with aux
Cleared hypotheses: hC
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
K C : Set α
hC : (M ／ K).IsCircuit C
aux : ∀ {K : Set α} (hC : (M ／ K).IsCircuit C) (hKi : M.Indep K), ∃ (C' : Set α), M.IsCircuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K
hKi : ¬M.Indep K
⊢ ∃ (C' : Set α), M.IsCircuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K
have inr : ∀ (I : Set α) (hI : M.IsBasis' I K), ∃ (C' : Set α), M.IsCircuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K
Tactic: obtain ⟨I, hI⟩ := M.exists_isBasis' K
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (hypothesis)
Goal:
α : Type u_1
M : Matroid α
K C : Set α
hC : (M ／ K).IsCircuit C
aux : ∀ {K : Set α} (hC : (M ／ K).IsCircuit C) (hKi : M.Indep K), ∃ (C' : Set α), M.IsCircuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K
hKi : ¬M.Indep K
I : Set α
hI : M.IsBasis' I K
⊢ ∃ (C' : Set α), M.IsCircuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K
have hC₁ : (M ／ I).IsCircuit C ∧ Disjoint C (K \ I)
Tactic: rw [hI.contract_eq_contract_delete, delete_isCircuit_iff] at hC
Cleared hypotheses: hC, hI
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
K C : Set α
aux : ∀ {K : Set α} (hC : (M ／ K).IsCircuit C) (hKi : M.Indep K), ∃ (C' : Set α), M.IsCircuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K
hKi : ¬M.Indep K
I : Set α
hC : (M ／ I).IsCircuit C ∧ Disjoint C (K \ I)
hI : M.IsBasis' I K
⊢ ∃ (C' : Set α), M.IsCircuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K
have inr : ∀ (C' : Set α) (hC' : M.IsCircuit C') (hCC' : C ⊆ C') (hC'ss : C' ⊆ C ∪ I),
  ∃ (C' : Set α), M.IsCircuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K
Tactic: obtain ⟨C', hC', hCC', hC'ss⟩ := aux hC.1 hI.indep
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (hypothesis)
Goal:
α : Type u_1
M : Matroid α
K_1 C K : Set α
hC : (M ／ K).IsCircuit C
hKi : M.Indep K
⊢ ∃ (C' : Set α), M.IsCircuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K
have hCE : C ⊆ M.E
Tactic: obtain ⟨hCE : C ⊆ M.E, hCK : Disjoint C K⟩ := subset_diff.1 hC.subset_ground
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (hypothesis)
Goal:
α : Type u_1
M : Matroid α
K_1 C K : Set α
hC : (M ／ K).IsCircuit C
hKi : M.Indep K
hCE : C ⊆ M.E
⊢ ∃ (C' : Set α), M.IsCircuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K
have hCK : Disjoint C K
Tactic: obtain ⟨hCE : C ⊆ M.E, hCK : Disjoint C K⟩ := subset_diff.1 hC.subset_ground
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
K_1 C K : Set α
hC : (M ／ K).IsCircuit C
hKi : M.Indep K
hCE : C ⊆ M.E
hCK : Disjoint C K
⊢ ∃ (C' : Set α), M.IsCircuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K
have obtain : ∀ (C' : Set α) (hC'ss : C' ⊆ C ∪ K) (hC' : M.IsCircuit C'), ∃ (C' : Set α), M.IsCircuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K
Tactic: obtain ⟨C', hC'ss, hC'⟩ := (hKi.contract_dep_iff.1 hC.dep).2.exists_isCircuit_subset
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
K_1 C K : Set α
hC : (M ／ K).IsCircuit C
hKi : M.Indep K
hCE : C ⊆ M.E
hCK : Disjoint C K
C' : Set α
hC'ss : C' ⊆ C ∪ K
hC' : M.IsCircuit C'
⊢ ∃ (C' : Set α), M.IsCircuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K
have refine : C ⊆ C'
Tactic: refine ⟨C', hC', ?_, hC'ss⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
K_1 C K : Set α
hC : (M ／ K).IsCircuit C
hKi : M.Indep K
hCE : C ⊆ M.E
hCK : Disjoint C K
C' : Set α
hC'ss : C' ⊆ C ∪ K
hC' : M.IsCircuit C'
⊢ (M ／ K).Dep (C' \ K)
have rw : M.Dep (C' \ K ∪ K)
Tactic: rw [hKi.contract_dep_iff, and_iff_right disjoint_sdiff_left]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (hypothesis)
Goal:
α : Type u_1
M : Matroid α
K_1 C K : Set α
hC : (M ／ K).IsCircuit C
hKi : M.Indep K
hCE : C ⊆ M.E
hCK : Disjoint C K
C' : Set α
hC'ss : C' ⊆ C ∪ K
hC' : M.IsCircuit C'
⊢ C ⊆ C'
have hdep2 : (M ／ K).Dep (C' \ K)
Tactic: have hdep2 : (M ／ K).Dep (C' \ K) := by
    rw [hKi.contract_dep_iff, and_iff_right disjoint_sdiff_left]
    refine hC'.dep.superset (by simp)
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
K_1 C K : Set α
hC : (M ／ K).IsCircuit C
hKi : M.Indep K
hCE : C ⊆ M.E
hCK : Disjoint C K
C' : Set α
hC'ss : C' ⊆ C ∪ K
hC' : M.IsCircuit C'
hdep2 : (M ／ K).Dep (C' \ K)
⊢ C ⊆ C'
have rw : C' \ K ⊆ C'
Tactic: rw [← (hC.eq_of_dep_subset hdep2 (diff_subset_iff.2 (union_comm _ _ ▸ hC'ss)))]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (hypothesis)
Goal:
α : Type u_1
M : Matroid α
K C : Set α
hK : (M ／ C).IsCocircuit K
⊢ M.IsCocircuit K
have hK₁ : (M✶ ＼ C).IsCircuit K
Tactic: rw [isCocircuit_def, dual_contract] at hK
Cleared hypotheses: hK
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
K D : Set α
hK : M.IsCocircuit K
hD : D ⊂ K
⊢ (M ＼ D).IsCocircuit (K \ D)
have rw : (M✶ ／ D).IsCircuit (K \ D)
Tactic: rw [isCocircuit_def, dual_delete]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
K X : Set α
hK : M.IsCocircuit K
hXK : X ⊆ K
hX : X.Nonempty
⊢ (M ＼ (K \ X)).IsCocircuit X
have rw : (M✶ ／ (K \ X)).IsCircuit X
Tactic: rw [isCocircuit_def, dual_delete]