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
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
⊢ (M ／ X).Dep D ↔ M.Dep (D ∪ I) ∧ Disjoint X D
have rw₃ : Disjoint D (X \ I) ∧ Disjoint D I ∧ M.Dep (D ∪ 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
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
⊢ (M ／ X).Dep D ↔ M.Dep (D ∪ I) ∧ Disjoint X D
have rw₄ : (Disjoint D (X \ I) ∧ Disjoint D I) ∧ M.Dep (D ∪ 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
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
⊢ (M ／ X).Dep D ↔ M.Dep (D ∪ I) ∧ Disjoint X D
have rw₅ : Disjoint D (X \ I ∪ I) ∧ M.Dep (D ∪ 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
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
⊢ (M ／ X).Dep D ↔ M.Dep (D ∪ I) ∧ Disjoint X D
have rw₆ : Disjoint D X ∧ M.Dep (D ∪ 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
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
⊢ (M ／ X).Dep D ↔ M.Dep (D ∪ I) ∧ Disjoint X D
have rw₇ : Disjoint X D ∧ M.Dep (D ∪ 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
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
⊢ (M ／ X).Dep D ↔ M.Dep (D ∪ I) ∧ Disjoint X D
have rw₈ : M.Dep (D ∪ I) ∧ Disjoint X 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 J X : Set α
hI : M.IsBasis I X
hdj : Disjoint X J
⊢ (M ／ X).Indep J ↔ M.Indep (J ∪ I)
have rw : M.Indep (J ∪ I) ∧ Disjoint X J ↔ M.Indep (J ∪ I)
Tactic: rw [hI.contract_indep_iff, and_iff_left hdj]
-- 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
hdj : Disjoint X J
rw : M.Indep (J ∪ I) ∧ Disjoint X J ↔ M.Indep (J ∪ I)
⊢ (M ／ X).Indep J ↔ M.Indep (J ∪ I)
have rw₁ : M.Indep (J ∪ I) ↔ M.Indep (J ∪ I)
Tactic: rw [hI.contract_indep_iff, and_iff_left hdj]
-- 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 \ X) ↔ M.Indep (J \ X ∪ I)
have rw : M.Indep (J \ X ∪ I) ∧ Disjoint X (J \ X) ↔ M.Indep (J \ X ∪ I)
Tactic: rw [hI.contract_indep_iff, and_iff_left disjoint_sdiff_right]
-- 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.Indep (J \ X ∪ I) ∧ Disjoint X (J \ X) ↔ M.Indep (J \ X ∪ I)
⊢ (M ／ X).Indep (J \ X) ↔ M.Indep (J \ X ∪ I)
have rw₁ : M.Indep (J \ X ∪ I) ↔ M.Indep (J \ X ∪ I)
Tactic: rw [hI.contract_indep_iff, and_iff_left disjoint_sdiff_right]
-- 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 \ X) ↔ M.Indep (J \ X ∪ I)
have rw : M.Indep (J \ X ∪ I) ∧ Disjoint X (J \ X) ↔ M.Indep (J \ X ∪ I)
Tactic: rw [hI.contract_indep_iff, and_iff_left disjoint_sdiff_right]
-- 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.Indep (J \ X ∪ I) ∧ Disjoint X (J \ X) ↔ M.Indep (J \ X ∪ I)
⊢ (M ／ X).Indep (J \ X) ↔ M.Indep (J \ X ∪ I)
have rw₁ : M.Indep (J \ X ∪ I) ↔ M.Indep (J \ X ∪ I)
Tactic: rw [hI.contract_indep_iff, and_iff_left disjoint_sdiff_right]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (hypothesis)
Goal:
α : Type u_1
M : Matroid α
I J X C : Set α
h : M.IsBasis I X
hJC : M.IsBasis' J C
h_ind : M.Indep (I \ C ∪ J)
⊢ (M ／ C).IsBasis (I \ C) (X \ C)
have hIX : I ⊆ X
Tactic: have hIX := h.subset
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (hypothesis)
Goal:
α : Type u_1
M : Matroid α
I J X C : Set α
h : M.IsBasis I X
hJC : M.IsBasis' J C
h_ind : M.Indep (I \ C ∪ J)
hIX : I ⊆ X
⊢ (M ／ C).IsBasis (I \ C) (X \ C)
have hJCss : J ⊆ C
Tactic: have hJCss := hJC.subset
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
I J X C : Set α
h : M.IsBasis I X
hJC : M.IsBasis' J C
h_ind : M.Indep (I \ C ∪ J)
hIX : I ⊆ X
hJCss : J ⊆ C
⊢ (M ／ C).IsBasis (I \ C) (X \ C)
have rw : (M ／ J).IsBasis (I \ C) (X \ C) ∧ Disjoint (X \ C) (C \ J)
Tactic: rw [hJC.contract_eq_contract_delete, delete_isBasis_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
I J X C : Set α
h : M.IsBasis I X
hJC : M.IsBasis' J C
h_ind : M.Indep (I \ C ∪ J)
hIX : I ⊆ X
hJCss : J ⊆ C
⊢ (M ／ J).IsBasis (I \ C) (X \ C) ∧ Disjoint (X \ C) (C \ J)
have refine_1 : I \ C ∪ J ⊆ X \ C ∪ J
Tactic: refine ⟨contract_isBasis_union_union (h_ind.isBasis_of_subset_of_subset_closure ?_ ?_) ?_ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
I J X C : Set α
h : M.IsBasis I X
hJC : M.IsBasis' J C
h_ind : M.Indep (I \ C ∪ J)
hIX : I ⊆ X
hJCss : J ⊆ C
refine_1 : I \ C ∪ J ⊆ X \ C ∪ J
⊢ (M ／ J).IsBasis (I \ C) (X \ C) ∧ Disjoint (X \ C) (C \ J)
have refine_2 : X \ C ∪ J ⊆ M.closure (I \ C ∪ J)
Tactic: refine ⟨contract_isBasis_union_union (h_ind.isBasis_of_subset_of_subset_closure ?_ ?_) ?_ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
I J X C : Set α
h : M.IsBasis I X
hJC : M.IsBasis' J C
h_ind : M.Indep (I \ C ∪ J)
hIX : I ⊆ X
hJCss : J ⊆ C
refine_1 : I \ C ∪ J ⊆ X \ C ∪ J
refine_2 : X \ C ∪ J ⊆ M.closure (I \ C ∪ J)
⊢ (M ／ J).IsBasis (I \ C) (X \ C) ∧ Disjoint (X \ C) (C \ J)
have refine_3 : Disjoint (I \ C) J
Tactic: refine ⟨contract_isBasis_union_union (h_ind.isBasis_of_subset_of_subset_closure ?_ ?_) ?_ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
I J X C : Set α
h : M.IsBasis I X
hJC : M.IsBasis' J C
h_ind : M.Indep (I \ C ∪ J)
hIX : I ⊆ X
hJCss : J ⊆ C
refine_1 : I \ C ∪ J ⊆ X \ C ∪ J
refine_2 : X \ C ∪ J ⊆ M.closure (I \ C ∪ J)
refine_3 : Disjoint (I \ C) J
⊢ (M ／ J).IsBasis (I \ C) (X \ C) ∧ Disjoint (X \ C) (C \ J)
have refine_4 : Disjoint (X \ C) J
Tactic: refine ⟨contract_isBasis_union_union (h_ind.isBasis_of_subset_of_subset_closure ?_ ?_) ?_ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
I J X C : Set α
h : M.IsBasis I X
hJC : M.IsBasis' J C
h_ind : M.Indep (I \ C ∪ J)
hIX : I ⊆ X
hJCss : J ⊆ C
refine_1 : I \ C ∪ J ⊆ X \ C ∪ J
refine_2 : X \ C ∪ J ⊆ M.closure (I \ C ∪ J)
refine_3 : Disjoint (I \ C) J
refine_4 : Disjoint (X \ C) J
⊢ (M ／ J).IsBasis (I \ C) (X \ C) ∧ Disjoint (X \ C) (C \ J)
have refine_5 : Disjoint (X \ C) (C \ J)
Tactic: refine ⟨contract_isBasis_union_union (h_ind.isBasis_of_subset_of_subset_closure ?_ ?_) ?_ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
I J X C : Set α
h : M.IsBasis I X
hJC : M.IsBasis' J C
h_ind : M.Indep (I \ C ∪ J)
hIX : I ⊆ X
hJCss : J ⊆ C
⊢ X \ C ∪ J ⊆ M.closure (I \ C ∪ J)
have refine_2 : X \ C ∪ J ⊆ M.closure (X ∪ C)
Tactic: rw [closure_union_congr_right hJC.closure_eq_closure, diff_union_self,
      closure_union_congr_left h.closure_eq_closure]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
I J X C : Set α
h : M.IsBasis I X
hJC : M.IsBasis' J C
h_ind : M.Indep (I \ C ∪ J)
hIX : I ⊆ X
hJCss : J ⊆ C
⊢ X \ C ∪ J ⊆ X ∪ C
have tauto_set : ∀ (h_ind : M.Indep (I ∩ Cᶜ ∪ J)) (hIX : ∀ x ∈ I, x ∈ X) (hJCss : ∀ x ∈ J, x ∈ C) (x : α),
  x ∈ X ∧ x ∉ C ∨ x ∈ J → x ∈ X ∨ x ∈ C
Tactic: tauto_set
Cleared hypotheses: h_ind, hIX, hJCss
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
I J X C : Set α
h : M.IsBasis I X
hJC : M.IsBasis' J C
h_ind : M.Indep (I \ C ∪ J)
hIX : I ⊆ X
hJCss : J ⊆ C
⊢ Disjoint (I \ C) J
have refine_3 : ∀ (h_ind : M.Indep (I ∩ Cᶜ ∪ J)) (hIX : ∀ x ∈ I, x ∈ X) (hJCss : ∀ x ∈ J, x ∈ C) (x : α),
  (x ∈ I ∧ x ∉ C) ∧ x ∈ J → Membership.mem (γ := Set α) ∅ x
Tactic: tauto_set
Cleared hypotheses: h_ind, hIX, hJCss
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
I J X C : Set α
h : M.IsBasis I X
hJC : M.IsBasis' J C
h_ind : M.Indep (I \ C ∪ J)
hIX : I ⊆ X
hJCss : J ⊆ C
⊢ Disjoint (X \ C) J
have refine_4 : ∀ (h_ind : M.Indep (I ∩ Cᶜ ∪ J)) (hIX : ∀ x ∈ I, x ∈ X) (hJCss : ∀ x ∈ J, x ∈ C) (x : α),
  (x ∈ X ∧ x ∉ C) ∧ x ∈ J → Membership.mem (γ := Set α) ∅ x
Tactic: tauto_set
Cleared hypotheses: h_ind, hIX, hJCss
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
I J X C : Set α
h : M.IsBasis I X
hJC : M.IsBasis' J C
h_ind : M.Indep (I \ C ∪ J)
hIX : I ⊆ X
hJCss : J ⊆ C
⊢ Disjoint (X \ C) (C \ J)
have refine_5 : ∀ (h_ind : M.Indep (I ∩ Cᶜ ∪ J)) (hIX : ∀ x ∈ I, x ∈ X) (hJCss : ∀ x ∈ J, x ∈ C) (x : α),
  (x ∈ X ∧ x ∉ C) ∧ x ∈ C ∧ x ∉ J → Membership.mem (γ := Set α) ∅ x
Tactic: tauto_set
Cleared hypotheses: h_ind, hIX, hJCss
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
I J X C : Set α
h : M.IsBasis I X
hJC : M.IsBasis' J C
h_ind : M.Indep (I \ C ∪ J)
hIX : I ⊆ X
hJCss : J ⊆ C
⊢ I \ C ∪ J ⊆ X \ C ∪ J
have refine_1 : ∀ (h_ind : M.Indep (I ∩ Cᶜ ∪ J)) (hIX : ∀ x ∈ I, x ∈ X) (hJCss : ∀ x ∈ J, x ∈ C) (x : α),
  x ∈ I ∧ x ∉ C ∨ x ∈ J → x ∈ X ∧ x ∉ C ∨ x ∈ J
Tactic: tauto_set
Cleared hypotheses: h_ind, hIX, hJCss
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
I J X C : Set α
h : M.IsBasis' I X
hJC : M.IsBasis' J C
h_ind : M.Indep (I \ C ∪ J)
⊢ (M ／ C).IsBasis' (I \ C) (X \ C)
have rw : (M ／ C).IsBasis (I \ C) ((X ∩ M.E) \ C)
Tactic: rw [isBasis'_iff_isBasis_inter_ground, contract_ground, ← diff_inter_distrib_right]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (hypothesis)
Goal:
α : Type u_1
M : Matroid α
I J X C : Set α
h : M.IsBasis I X
hJC : M.IsBasis J C
hdj : Disjoint C X
h_ind : M.Indep (I ∪ J)
⊢ (M ／ C).IsBasis I X
have h' : ∀ (h_ind : M.Indep (I \ C ∪ J)), (M ／ C).IsBasis (I \ C) (X \ C)
Tactic: have h' := h.contract_isBasis hJC
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
I J X C : Set α
h : M.IsBasis I X
hJC : M.IsBasis J C
hdj : Disjoint C X
h_ind : M.Indep (I ∪ J)
h' : ∀ (h_ind : M.Indep (I \ C ∪ J)), (M ／ C).IsBasis (I \ C) (X \ C)
⊢ (M ／ C).IsBasis I X
have rwa : ∀ (h' : ∀ (h_ind : M.Indep (I ∪ J)), (M ／ C).IsBasis I (X \ C)), (M ／ C).IsBasis I X
Tactic: rwa [(hdj.mono_right h.subset).sdiff_eq_right, hdj.sdiff_eq_right, imp_iff_right h_ind] at h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
I J X C : Set α
h : M.IsBasis I X
hJC : M.IsBasis J C
hdj : Disjoint C X
h_ind : M.Indep (I ∪ J)
h' : ∀ (h_ind : M.Indep (I \ C ∪ J)), (M ／ C).IsBasis (I \ C) (X \ C)
rwa : ∀ (h' : ∀ (h_ind : M.Indep (I ∪ J)), (M ／ C).IsBasis I (X \ C)), (M ／ C).IsBasis I X
⊢ (M ／ C).IsBasis I X
have rwa₁ : ∀ (h' : ∀ (h_ind : M.Indep (I ∪ J)), (M ／ C).IsBasis I X), (M ／ C).IsBasis I X
Tactic: rwa [(hdj.mono_right h.subset).sdiff_eq_right, hdj.sdiff_eq_right, imp_iff_right h_ind] at h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
I J X C : Set α
h : M.IsBasis I X
hJC : M.IsBasis J C
hdj : Disjoint C X
h_ind : M.Indep (I ∪ J)
h' : ∀ (h_ind : M.Indep (I \ C ∪ J)), (M ／ C).IsBasis (I \ C) (X \ C)
rwa : ∀ (h' : ∀ (h_ind : M.Indep (I ∪ J)), (M ／ C).IsBasis I (X \ C)), (M ／ C).IsBasis I X
rwa₁ : ∀ (h' : ∀ (h_ind : M.Indep (I ∪ J)), (M ／ C).IsBasis I X), (M ／ C).IsBasis I X
⊢ (M ／ C).IsBasis I X
have rwa₂ : ∀ (h' : (M ／ C).IsBasis I X), (M ／ C).IsBasis I X
Tactic: rwa [(hdj.mono_right h.subset).sdiff_eq_right, hdj.sdiff_eq_right, imp_iff_right h_ind] at h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
I J X : Set α
h : M.IsBasis I X
hdj : Disjoint J X
h_ind : M.Indep (I ∪ J)
⊢ (M ／ J).IsBasis I X
have rw : (M ／ J).IsBasis (I \ J) (X \ J)
Tactic: rw [← hdj.sdiff_eq_right, ← (hdj.mono_right h.subset).sdiff_eq_right]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
X C : Set α
h : (M ／ C).Dep X
hC : C ⊆ M.E
⊢ M.Dep (C ∪ X)
have rw : ¬M.Indep (C ∪ X)
Tactic: rw [Dep, and_iff_left (union_subset hC (h.subset_ground.trans diff_subset))]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (hypothesis)
Goal:
α : Type u_1
M : Matroid α
X C : Set α
h : (M ／ C).Dep X
hC : C ⊆ M.E
hi : M.Indep (C ∪ X)
⊢ False
have h₁ : ¬Disjoint X C ∧ X ⊆ (M ／ C).E
Tactic: rw [Dep, (hi.subset subset_union_left).contract_indep_iff, union_comm,
    and_iff_left hi] at h
Cleared hypotheses: h, hC, hi
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M M' N : Matroid α
e f : α
I J R D B X Y Z K C C₁ C₂ : Set α
inst : M.Finitary
⊢ (M ／ C).Finitary
have obtain : ∀ (J : Set α) (hJ : M.IsBasis' J C), (M ／ C).Finitary
Tactic: obtain ⟨J, hJ⟩ := M.exists_isBasis' C
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M M' N : Matroid α
e f : α
I J_1 R D B X Y Z K C C₁ C₂ : Set α
inst : M.Finitary
J : Set α
hJ : M.IsBasis' J C
this : (M ／ J).Finitary
⊢ (M ／ C).Finitary
have rw : (M ／ J ＼ (C \ J)).Finitary
Tactic: rw [hJ.contract_eq_contract_delete]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M M' N : Matroid α
e f : α
I J_1 R D B X Y Z K C C₁ C₂ : Set α
inst : M.Finitary
J : Set α
hJ : M.IsBasis' J C
⊢ (M ／ C).Finitary
have suffices : (M ／ J).Finitary
Tactic: suffices (M ／ J).Finitary by
    rw [hJ.contract_eq_contract_delete]
    infer_instance
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M M' N : Matroid α
e f : α
I_1 J_1 R D B X Y Z K_1 C C₁ C₂ : Set α
inst : M.Finitary
J : Set α
hJ : M.IsBasis' J C
I : Set α
hI : ∀ J_2 ⊆ I, J_2.Finite → (M ／ J).Indep J_2
K : Set α
hK : K ⊆ I ∪ J
hKfin : K.Finite
⊢ K ⊆ K ∩ I ∪ J
have tauto_set : ∀ (hI : ∀ (J_2 : Set α), (∀ x ∈ J_2, x ∈ I) → J_2.Finite → (M ／ J).Indep J_2) (hK : ∀ x ∈ K, x ∈ I ∨ x ∈ J)
  (hKfin : K.Finite), ∀ x ∈ K, True ∧ x ∈ I ∨ x ∈ J
Tactic: tauto_set
Cleared hypotheses: hI, hK, hKfin
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.coloops
⊢ M ／ X = M ＼ X
have rw : (M ／ X)✶ = (M ＼ X)✶
Tactic: rw [← dual_inj, dual_delete, contract_eq_delete_of_subset_loops hX, dual_contract]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.coloops
rw : (M ／ X)✶ = (M ＼ X)✶
⊢ M ／ X = M ＼ X
have rw₁ : (M ／ X)✶ = M✶ ／ X
Tactic: rw [← dual_inj, dual_delete, contract_eq_delete_of_subset_loops hX, dual_contract]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.coloops
rw : (M ／ X)✶ = (M ＼ X)✶
rw₁ : (M ／ X)✶ = M✶ ／ X
⊢ M ／ X = M ＼ X
have rw₂ : (M ／ X)✶ = M✶ ＼ X
Tactic: rw [← dual_inj, dual_delete, contract_eq_delete_of_subset_loops hX, dual_contract]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.coloops
rw : (M ／ X)✶ = (M ＼ X)✶
rw₁ : (M ／ X)✶ = M✶ ／ X
rw₂ : (M ／ X)✶ = M✶ ＼ X
⊢ M ／ X = M ＼ X
have rw₃ : M✶ ＼ X = M✶ ＼ X
Tactic: rw [← dual_inj, dual_delete, contract_eq_delete_of_subset_loops hX, dual_contract]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
C : Set α
⊢ (M ／ C).IsLoop e ↔ e ∈ M.closure C ∧ e ∉ C
have obtain : ∀ (I : Set α) (hI : M.IsBasis' I C), (M ／ C).IsLoop e ↔ e ∈ M.closure C ∧ e ∉ C
Tactic: obtain ⟨I, hI⟩ := M.exists_isBasis' C
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
C I : Set α
hI : M.IsBasis' I C
⊢ (M ／ C).IsLoop e ↔ e ∈ M.closure C ∧ e ∉ C
have rw : (Disjoint {e} I ∧ e ∈ M.closure C \ I) ∧ e ∉ C \ I ↔ e ∈ M.closure C ∧ e ∉ C
Tactic: rw [hI.contract_eq_contract_delete, delete_isLoop_iff, ← singleton_dep,
    hI.indep.contract_dep_iff, singleton_union, hI.indep.insert_dep_iff, hI.closure_eq_closure]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
C I : Set α
hI : M.IsBasis' I C
⊢ (Disjoint {e} I ∧ e ∈ M.closure C \ I) ∧ e ∉ C \ I ↔ e ∈ M.closure C ∧ e ∉ C
have pos : ∀ (heI : e ∈ I), (Disjoint {e} I ∧ e ∈ M.closure C \ I) ∧ e ∉ C \ I ↔ e ∈ M.closure C ∧ e ∉ C
Tactic: by_cases heI : e ∈ I
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
C I : Set α
hI : M.IsBasis' I C
pos : ∀ (heI : e ∈ I), (Disjoint {e} I ∧ e ∈ M.closure C \ I) ∧ e ∉ C \ I ↔ e ∈ M.closure C ∧ e ∉ C
⊢ (Disjoint {e} I ∧ e ∈ M.closure C \ I) ∧ e ∉ C \ I ↔ e ∈ M.closure C ∧ e ∉ C
have neg : ∀ (heI : e ∉ I), (Disjoint {e} I ∧ e ∈ M.closure C \ I) ∧ e ∉ C \ I ↔ e ∈ M.closure C ∧ e ∉ C
Tactic: by_cases heI : e ∈ I
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
C : Set α
⊢ (M ／ C).coloops = M.coloops \ C
have rw : (M✶ ＼ C)✶.coloops = M.coloops \ C
Tactic: rw [← dual_delete_dual, dual_coloops, delete_loops_eq, dual_loops]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
C : Set α
rw : (M✶ ＼ C)✶.coloops = M.coloops \ C
⊢ (M ／ C).coloops = M.coloops \ C
have rw₁ : (M✶ ＼ C).loops = M.coloops \ C
Tactic: rw [← dual_delete_dual, dual_coloops, delete_loops_eq, dual_loops]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
C : Set α
rw : (M✶ ＼ C)✶.coloops = M.coloops \ C
rw₁ : (M✶ ＼ C).loops = M.coloops \ C
⊢ (M ／ C).coloops = M.coloops \ C
have rw₂ : M✶.loops \ C = M.coloops \ C
Tactic: rw [← dual_delete_dual, dual_coloops, delete_loops_eq, dual_loops]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
C : Set α
rw : (M✶ ＼ C)✶.coloops = M.coloops \ C
rw₁ : (M✶ ＼ C).loops = M.coloops \ C
rw₂ : M✶.loops \ C = M.coloops \ C
⊢ (M ／ C).coloops = M.coloops \ C
have rw₃ : M.coloops \ C = M.coloops \ C
Tactic: rw [← dual_delete_dual, dual_coloops, delete_loops_eq, dual_loops]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
C : Set α
h : (M ／ C).IsNonloop e
⊢ M.IsNonloop e
have rw : ∀ (h : (M ／ C).Indep {e}), M.Indep {e}
Tactic: rw [← indep_singleton] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
C : Set α
⊢ (M ／ C).IsNonloop e ↔ e ∈ M.E \ M.closure C
have rw : e ∈ (M.E \ C) \ (M.closure C \ C) ↔ e ∈ M.E \ M.closure C
Tactic: rw [isNonloop_iff_mem_compl_loops, contract_ground, contract_loops_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
C : Set α
⊢ e ∈ (M.E \ C) \ (M.closure C \ C) ↔ e ∈ M.E \ M.closure C
have refine : ∀ (h : e ∈ M.E \ M.closure C) (heC : e ∈ C), e ∈ M.closure C
Tactic: refine ⟨fun ⟨he,heC⟩ ↦ ⟨he.1, fun h ↦ heC ⟨h, he.2⟩⟩,
    fun h ↦ ⟨⟨h.1, fun heC ↦ h.2 ?_⟩, fun h' ↦ h.2 h'.1⟩⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
e : α
C : Set α
h : e ∈ M.E \ M.closure C
heC : e ∈ C
⊢ e ∈ M.closure C
have rw : e ∈ M.closure (C ∩ M.E)
Tactic: rw [← closure_inter_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Contract (goal)
Goal:
α : Type u_1
M : Matroid α
I X : Set α
hIX : M.IsBasis I X
⊢ X \ I ⊆ (M ／ I).loops
have rw : X ⊆ M.closure I
Tactic: rw [diff_subset_iff, contract_loops_eq, union_diff_self,
    union_eq_self_of_subset_left (M.subset_closure I)]