awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (goal)
Goal:
α : Type u_1
M : Matroid α
D : Set α
⊢ M ＼ (D ∩ M.E) = M ＼ D
have rw : M ↾ M.E \ (D ∩ M.E) = M ＼ D
Tactic: rw [← restrict_compl, ← restrict_compl, diff_inter_self_eq_diff]
-- 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.E) = M ＼ D
⊢ M ＼ (D ∩ M.E) = M ＼ D
have rw₁ : M ↾ M.E \ (D ∩ M.E) = M ↾ M.E \ D
Tactic: rw [← restrict_compl, ← restrict_compl, diff_inter_self_eq_diff]
-- 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.E) = M ＼ D
rw₁ : M ↾ M.E \ (D ∩ M.E) = M ↾ M.E \ D
⊢ M ＼ (D ∩ M.E) = M ＼ D
have rw₂ : M ↾ M.E \ D = M ↾ M.E \ D
Tactic: rw [← restrict_compl, ← restrict_compl, diff_inter_self_eq_diff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (goal)
Goal:
α : Type u_1
M : Matroid α
D₁ D₂ : Set α
⊢ M ＼ D₁ = M ＼ D₂ ↔ D₁ ∩ M.E = D₂ ∩ M.E
have rw : M ＼ (D₁ ∩ M.E) = M ＼ (D₂ ∩ M.E) ↔ D₁ ∩ M.E = D₂ ∩ M.E
Tactic: rw [← delete_inter_ground_eq, ← M.delete_inter_ground_eq D₂]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (goal)
Goal:
α : Type u_1
M : Matroid α
D₁ D₂ : Set α
h : D₁ ∩ M.E = D₂ ∩ M.E
⊢ M ＼ (D₁ ∩ M.E) = M ＼ (D₂ ∩ M.E)
have rw : M ＼ (D₂ ∩ M.E) = M ＼ (D₂ ∩ M.E)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (goal)
Goal:
α : Type u_1
M : Matroid α
D₁ D₂ : Set α
⊢ M ＼ (D₁ ∩ M.E) = M ＼ (D₂ ∩ M.E) ↔ D₁ ∩ M.E = D₂ ∩ M.E
have refine : ∀ (h : M ＼ (D₁ ∩ M.E) = M ＼ (D₂ ∩ M.E)), D₁ ∩ M.E = D₂ ∩ M.E
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ by rw [h]⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (hypothesis)
Goal:
α : Type u_1
M : Matroid α
D₁ D₂ : Set α
h : M ＼ (D₁ ∩ M.E) = M ＼ (D₂ ∩ M.E)
⊢ D₁ ∩ M.E = D₂ ∩ M.E
have h₁ : M.E \ (M ＼ (D₁ ∩ M.E)).E = M.E \ (M ＼ (D₂ ∩ M.E)).E
Tactic: apply_fun (M.E \ Matroid.E ·) at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (goal)
Goal:
α : Type u_1
M : Matroid α
⊢ M ＼ ∅ = M
have rw : Disjoint ∅ M.E
Tactic: rw [delete_eq_self_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (goal)
Goal:
α : Type u_1
M N : Matroid α
X : Set α
h : N ≤r M
hX : Disjoint X N.E
⊢ N ≤r M ＼ X
have obtain : ∀ (D : Set α) (hD : D ⊆ M.E) (h : M ＼ D ≤r M) (hX : Disjoint X (M ＼ D).E), M ＼ D ≤r M ＼ X
Tactic: obtain ⟨D, hD, rfl⟩ := isRestriction_iff_exists_eq_delete.1 h
Cleared hypotheses: N, h, hX
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (goal)
Goal:
α : Type u_1
M : Matroid α
X D : Set α
hD : D ⊆ M.E
h : M ＼ D ≤r M
hX : Disjoint X (M ＼ D).E
⊢ M ＼ D ≤r M ＼ X
have refine : M ＼ D = M ＼ X ＼ (D \ X)
Tactic: refine isRestriction_iff_exists_eq_delete.2 ⟨D \ X, diff_subset_diff_left hD, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (goal)
Goal:
α : Type u_1
M : Matroid α
X D : Set α
hD : D ⊆ M.E
h : M ＼ D ≤r M
hX : Disjoint X (M ＼ D).E
⊢ M ＼ D = M ＼ X ＼ (D \ X)
have rwa : M ＼ D = M ＼ (X ∪ D \ X)
Tactic: rwa [delete_delete, union_diff_self, union_comm, ← delete_delete, eq_comm,
    delete_eq_self_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (goal)
Goal:
α : Type u_1
M : Matroid α
X D : Set α
hD : D ⊆ M.E
h : M ＼ D ≤r M
hX : Disjoint X (M ＼ D).E
rwa : M ＼ D = M ＼ (X ∪ D \ X)
⊢ M ＼ D = M ＼ X ＼ (D \ X)
have rwa₁ : M ＼ D = M ＼ (X ∪ D)
Tactic: rwa [delete_delete, union_diff_self, union_comm, ← delete_delete, eq_comm,
    delete_eq_self_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (goal)
Goal:
α : Type u_1
M : Matroid α
X D : Set α
hD : D ⊆ M.E
h : M ＼ D ≤r M
hX : Disjoint X (M ＼ D).E
rwa : M ＼ D = M ＼ (X ∪ D \ X)
rwa₁ : M ＼ D = M ＼ (X ∪ D)
⊢ M ＼ D = M ＼ X ＼ (D \ X)
have rwa₂ : M ＼ D = M ＼ (D ∪ X)
Tactic: rwa [delete_delete, union_diff_self, union_comm, ← delete_delete, eq_comm,
    delete_eq_self_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (goal)
Goal:
α : Type u_1
M : Matroid α
X D : Set α
hD : D ⊆ M.E
h : M ＼ D ≤r M
hX : Disjoint X (M ＼ D).E
rwa : M ＼ D = M ＼ (X ∪ D \ X)
rwa₁ : M ＼ D = M ＼ (X ∪ D)
rwa₂ : M ＼ D = M ＼ (D ∪ X)
⊢ M ＼ D = M ＼ X ＼ (D \ X)
have rwa₃ : M ＼ D = M ＼ D ＼ X
Tactic: rwa [delete_delete, union_diff_self, union_comm, ← delete_delete, eq_comm,
    delete_eq_self_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (goal)
Goal:
α : Type u_1
M : Matroid α
X D : Set α
hD : D ⊆ M.E
h : M ＼ D ≤r M
hX : Disjoint X (M ＼ D).E
rwa : M ＼ D = M ＼ (X ∪ D \ X)
rwa₁ : M ＼ D = M ＼ (X ∪ D)
rwa₂ : M ＼ D = M ＼ (D ∪ X)
rwa₃ : M ＼ D = M ＼ D ＼ X
⊢ M ＼ D = M ＼ X ＼ (D \ X)
have rwa₄ : M ＼ D ＼ X = M ＼ D
Tactic: rwa [delete_delete, union_diff_self, union_comm, ← delete_delete, eq_comm,
    delete_eq_self_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (goal)
Goal:
α : Type u_1
M : Matroid α
I D : Set α
⊢ (M ＼ D).Indep I ↔ M.Indep I ∧ Disjoint I D
have rw : (M ↾ M.E \ D).Indep I ↔ M.Indep I ∧ Disjoint I D
Tactic: rw [← restrict_compl, restrict_indep_iff, subset_diff, ← and_assoc,
    and_iff_left_of_imp Indep.subset_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (goal)
Goal:
α : Type u_1
M : Matroid α
I D : Set α
rw : (M ↾ M.E \ D).Indep I ↔ M.Indep I ∧ Disjoint I D
⊢ (M ＼ D).Indep I ↔ M.Indep I ∧ Disjoint I D
have rw₁ : M.Indep I ∧ I ⊆ M.E \ D ↔ M.Indep I ∧ Disjoint I D
Tactic: rw [← restrict_compl, restrict_indep_iff, subset_diff, ← and_assoc,
    and_iff_left_of_imp Indep.subset_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (goal)
Goal:
α : Type u_1
M : Matroid α
I D : Set α
rw : (M ↾ M.E \ D).Indep I ↔ M.Indep I ∧ Disjoint I D
rw₁ : M.Indep I ∧ I ⊆ M.E \ D ↔ M.Indep I ∧ Disjoint I D
⊢ (M ＼ D).Indep I ↔ M.Indep I ∧ Disjoint I D
have rw₂ : M.Indep I ∧ I ⊆ M.E ∧ Disjoint I D ↔ M.Indep I ∧ Disjoint I D
Tactic: rw [← restrict_compl, restrict_indep_iff, subset_diff, ← and_assoc,
    and_iff_left_of_imp Indep.subset_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (goal)
Goal:
α : Type u_1
M : Matroid α
I D : Set α
rw : (M ↾ M.E \ D).Indep I ↔ M.Indep I ∧ Disjoint I D
rw₁ : M.Indep I ∧ I ⊆ M.E \ D ↔ M.Indep I ∧ Disjoint I D
rw₂ : M.Indep I ∧ I ⊆ M.E ∧ Disjoint I D ↔ M.Indep I ∧ Disjoint I D
⊢ (M ＼ D).Indep I ↔ M.Indep I ∧ Disjoint I D
have rw₃ : (M.Indep I ∧ I ⊆ M.E) ∧ Disjoint I D ↔ M.Indep I ∧ Disjoint I D
Tactic: rw [← restrict_compl, restrict_indep_iff, subset_diff, ← and_assoc,
    and_iff_left_of_imp Indep.subset_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (goal)
Goal:
α : Type u_1
M : Matroid α
I D : Set α
rw : (M ↾ M.E \ D).Indep I ↔ M.Indep I ∧ Disjoint I D
rw₁ : M.Indep I ∧ I ⊆ M.E \ D ↔ M.Indep I ∧ Disjoint I D
rw₂ : M.Indep I ∧ I ⊆ M.E ∧ Disjoint I D ↔ M.Indep I ∧ Disjoint I D
rw₃ : (M.Indep I ∧ I ⊆ M.E) ∧ Disjoint I D ↔ M.Indep I ∧ Disjoint I D
⊢ (M ＼ D).Indep I ↔ M.Indep I ∧ Disjoint I D
have rw₄ : M.Indep I ∧ Disjoint I D ↔ M.Indep I ∧ Disjoint I D
Tactic: rw [← restrict_compl, restrict_indep_iff, subset_diff, ← and_assoc,
    and_iff_left_of_imp Indep.subset_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (goal)
Goal:
α : Type u_1
M : Matroid α
D X : Set α
⊢ (M ＼ D).Dep X ↔ M.Dep X ∧ Disjoint X D
have rw : ¬(M.Indep X ∧ Disjoint X D) ∧ X ⊆ M.E ∧ Disjoint X D ↔ (¬M.Indep X ∧ X ⊆ M.E) ∧ Disjoint X D
Tactic: rw [dep_iff, dep_iff, delete_indep_iff, delete_ground, subset_diff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (goal)
Goal:
α : Type u_1
M : Matroid α
D X : Set α
⊢ ¬(M.Indep X ∧ Disjoint X D) ∧ X ⊆ M.E ∧ Disjoint X D ↔ (¬M.Indep X ∧ X ⊆ M.E) ∧ Disjoint X D
have mp : ¬(M.Indep X ∧ Disjoint X D) ∧ X ⊆ M.E ∧ Disjoint X D → (¬M.Indep X ∧ X ⊆ M.E) ∧ Disjoint X D
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (goal)
Goal:
α : Type u_1
M : Matroid α
D X : Set α
mp : ¬(M.Indep X ∧ Disjoint X D) ∧ X ⊆ M.E ∧ Disjoint X D → (¬M.Indep X ∧ X ⊆ M.E) ∧ Disjoint X D
⊢ ¬(M.Indep X ∧ Disjoint X D) ∧ X ⊆ M.E ∧ Disjoint X D ↔ (¬M.Indep X ∧ X ⊆ M.E) ∧ Disjoint X D
have mpr : (¬M.Indep X ∧ X ⊆ M.E) ∧ Disjoint X D → ¬(M.Indep X ∧ Disjoint X D) ∧ X ⊆ M.E ∧ Disjoint X D
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (goal)
Goal:
α : Type u_1
M : Matroid α
D X : Set α
mp : ¬(M.Indep X ∧ Disjoint X D) ∧ X ⊆ M.E ∧ Disjoint X D → (¬M.Indep X ∧ X ⊆ M.E) ∧ Disjoint X D
mpr : (¬M.Indep X ∧ X ⊆ M.E) ∧ Disjoint X D → ¬(M.Indep X ∧ Disjoint X D) ∧ X ⊆ M.E ∧ Disjoint X D
⊢ ¬(M.Indep X ∧ Disjoint X D) ∧ X ⊆ M.E ∧ Disjoint X D ↔ (¬M.Indep X ∧ X ⊆ M.E) ∧ Disjoint X D
have mp₁ : ¬(M.Indep X ∧ Disjoint X D) → X ⊆ M.E → Disjoint X D → (¬M.Indep X ∧ X ⊆ M.E) ∧ Disjoint X D
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (goal)
Goal:
α : Type u_1
M : Matroid α
D X : Set α
mp : ¬(M.Indep X ∧ Disjoint X D) ∧ X ⊆ M.E ∧ Disjoint X D → (¬M.Indep X ∧ X ⊆ M.E) ∧ Disjoint X D
mpr : (¬M.Indep X ∧ X ⊆ M.E) ∧ Disjoint X D → ¬(M.Indep X ∧ Disjoint X D) ∧ X ⊆ M.E ∧ Disjoint X D
mp₁ mp₂ : ¬(M.Indep X ∧ Disjoint X D) → X ⊆ M.E → Disjoint X D → (¬M.Indep X ∧ X ⊆ M.E) ∧ Disjoint X D
⊢ ¬(M.Indep X ∧ Disjoint X D) ∧ X ⊆ M.E ∧ Disjoint X D ↔ (¬M.Indep X ∧ X ⊆ M.E) ∧ Disjoint X D
have mp₃ : ¬(M.Indep X ∧ Disjoint X D) → X ⊆ M.E → Disjoint X D → ¬M.Indep X
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (goal)
Goal:
α : Type u_1
M : Matroid α
D X : Set α
mp : ¬(M.Indep X ∧ Disjoint X D) ∧ X ⊆ M.E ∧ Disjoint X D → (¬M.Indep X ∧ X ⊆ M.E) ∧ Disjoint X D
mpr : (¬M.Indep X ∧ X ⊆ M.E) ∧ Disjoint X D → ¬(M.Indep X ∧ Disjoint X D) ∧ X ⊆ M.E ∧ Disjoint X D
mp₁ mp₂ : ¬(M.Indep X ∧ Disjoint X D) → X ⊆ M.E → Disjoint X D → (¬M.Indep X ∧ X ⊆ M.E) ∧ Disjoint X D
mp₃ : ¬(M.Indep X ∧ Disjoint X D) → X ⊆ M.E → Disjoint X D → ¬M.Indep X
⊢ ¬(M.Indep X ∧ Disjoint X D) ∧ X ⊆ M.E ∧ Disjoint X D ↔ (¬M.Indep X ∧ X ⊆ M.E) ∧ Disjoint X D
have mp₄ : ¬(M.Indep X ∧ Disjoint X D) → X ⊆ M.E → Disjoint X D → X ⊆ M.E
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (goal)
Goal:
α : Type u_1
M : Matroid α
D X : Set α
mp : ¬(M.Indep X ∧ Disjoint X D) ∧ X ⊆ M.E ∧ Disjoint X D → (¬M.Indep X ∧ X ⊆ M.E) ∧ Disjoint X D
mpr : (¬M.Indep X ∧ X ⊆ M.E) ∧ Disjoint X D → ¬(M.Indep X ∧ Disjoint X D) ∧ X ⊆ M.E ∧ Disjoint X D
mp₁ mp₂ : ¬(M.Indep X ∧ Disjoint X D) → X ⊆ M.E → Disjoint X D → (¬M.Indep X ∧ X ⊆ M.E) ∧ Disjoint X D
mp₃ : ¬(M.Indep X ∧ Disjoint X D) → X ⊆ M.E → Disjoint X D → ¬M.Indep X
mp₄ : ¬(M.Indep X ∧ Disjoint X D) → X ⊆ M.E → Disjoint X D → X ⊆ M.E
⊢ ¬(M.Indep X ∧ Disjoint X D) ∧ X ⊆ M.E ∧ Disjoint X D ↔ (¬M.Indep X ∧ X ⊆ M.E) ∧ Disjoint X D
have mp₅ : ¬(M.Indep X ∧ Disjoint X D) → X ⊆ M.E → Disjoint X D → Disjoint X D
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (goal)
Goal:
α : Type u_1
M : Matroid α
D X : Set α
mp : ¬(M.Indep X ∧ Disjoint X D) ∧ X ⊆ M.E ∧ Disjoint X D → (¬M.Indep X ∧ X ⊆ M.E) ∧ Disjoint X D
mpr : (¬M.Indep X ∧ X ⊆ M.E) ∧ Disjoint X D → ¬(M.Indep X ∧ Disjoint X D) ∧ X ⊆ M.E ∧ Disjoint X D
mp₁ mp₂ : ¬(M.Indep X ∧ Disjoint X D) → X ⊆ M.E → Disjoint X D → (¬M.Indep X ∧ X ⊆ M.E) ∧ Disjoint X D
mp₃ : ¬(M.Indep X ∧ Disjoint X D) → X ⊆ M.E → Disjoint X D → ¬M.Indep X
mp₄ : ¬(M.Indep X ∧ Disjoint X D) → X ⊆ M.E → Disjoint X D → X ⊆ M.E
mp₅ : ¬(M.Indep X ∧ Disjoint X D) → X ⊆ M.E → Disjoint X D → Disjoint X D
⊢ ¬(M.Indep X ∧ Disjoint X D) ∧ X ⊆ M.E ∧ Disjoint X D ↔ (¬M.Indep X ∧ X ⊆ M.E) ∧ Disjoint X D
have mpr₁ : Disjoint X D → ¬M.Indep X → X ⊆ M.E → ¬(M.Indep X ∧ Disjoint X D) ∧ X ⊆ M.E ∧ Disjoint X D
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (goal)
Goal:
α : Type u_1
M : Matroid α
D X : Set α
mp : ¬(M.Indep X ∧ Disjoint X D) ∧ X ⊆ M.E ∧ Disjoint X D → (¬M.Indep X ∧ X ⊆ M.E) ∧ Disjoint X D
mpr : (¬M.Indep X ∧ X ⊆ M.E) ∧ Disjoint X D → ¬(M.Indep X ∧ Disjoint X D) ∧ X ⊆ M.E ∧ Disjoint X D
mp₁ mp₂ : ¬(M.Indep X ∧ Disjoint X D) → X ⊆ M.E → Disjoint X D → (¬M.Indep X ∧ X ⊆ M.E) ∧ Disjoint X D
mp₃ : ¬(M.Indep X ∧ Disjoint X D) → X ⊆ M.E → Disjoint X D → ¬M.Indep X
mp₄ : ¬(M.Indep X ∧ Disjoint X D) → X ⊆ M.E → Disjoint X D → X ⊆ M.E
mp₅ : ¬(M.Indep X ∧ Disjoint X D) → X ⊆ M.E → Disjoint X D → Disjoint X D
mpr₁ mpr₂ : Disjoint X D → ¬M.Indep X → X ⊆ M.E → ¬(M.Indep X ∧ Disjoint X D) ∧ X ⊆ M.E ∧ Disjoint X D
⊢ ¬(M.Indep X ∧ Disjoint X D) ∧ X ⊆ M.E ∧ Disjoint X D ↔ (¬M.Indep X ∧ X ⊆ M.E) ∧ Disjoint X D
have mpr₃ : Disjoint X D → ¬M.Indep X → X ⊆ M.E → ¬(M.Indep X ∧ Disjoint X D)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (goal)
Goal:
α : Type u_1
M : Matroid α
D X : Set α
mp : ¬(M.Indep X ∧ Disjoint X D) ∧ X ⊆ M.E ∧ Disjoint X D → (¬M.Indep X ∧ X ⊆ M.E) ∧ Disjoint X D
mpr : (¬M.Indep X ∧ X ⊆ M.E) ∧ Disjoint X D → ¬(M.Indep X ∧ Disjoint X D) ∧ X ⊆ M.E ∧ Disjoint X D
mp₁ mp₂ : ¬(M.Indep X ∧ Disjoint X D) → X ⊆ M.E → Disjoint X D → (¬M.Indep X ∧ X ⊆ M.E) ∧ Disjoint X D
mp₃ : ¬(M.Indep X ∧ Disjoint X D) → X ⊆ M.E → Disjoint X D → ¬M.Indep X
mp₄ : ¬(M.Indep X ∧ Disjoint X D) → X ⊆ M.E → Disjoint X D → X ⊆ M.E
mp₅ : ¬(M.Indep X ∧ Disjoint X D) → X ⊆ M.E → Disjoint X D → Disjoint X D
mpr₁ mpr₂ : Disjoint X D → ¬M.Indep X → X ⊆ M.E → ¬(M.Indep X ∧ Disjoint X D) ∧ X ⊆ M.E ∧ Disjoint X D
mpr₃ : Disjoint X D → ¬M.Indep X → X ⊆ M.E → ¬(M.Indep X ∧ Disjoint X D)
⊢ ¬(M.Indep X ∧ Disjoint X D) ∧ X ⊆ M.E ∧ Disjoint X D ↔ (¬M.Indep X ∧ X ⊆ M.E) ∧ Disjoint X D
have mpr₄ : Disjoint X D → ¬M.Indep X → X ⊆ M.E → X ⊆ M.E
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (goal)
Goal:
α : Type u_1
M : Matroid α
D X : Set α
mp : ¬(M.Indep X ∧ Disjoint X D) ∧ X ⊆ M.E ∧ Disjoint X D → (¬M.Indep X ∧ X ⊆ M.E) ∧ Disjoint X D
mpr : (¬M.Indep X ∧ X ⊆ M.E) ∧ Disjoint X D → ¬(M.Indep X ∧ Disjoint X D) ∧ X ⊆ M.E ∧ Disjoint X D
mp₁ mp₂ : ¬(M.Indep X ∧ Disjoint X D) → X ⊆ M.E → Disjoint X D → (¬M.Indep X ∧ X ⊆ M.E) ∧ Disjoint X D
mp₃ : ¬(M.Indep X ∧ Disjoint X D) → X ⊆ M.E → Disjoint X D → ¬M.Indep X
mp₄ : ¬(M.Indep X ∧ Disjoint X D) → X ⊆ M.E → Disjoint X D → X ⊆ M.E
mp₅ : ¬(M.Indep X ∧ Disjoint X D) → X ⊆ M.E → Disjoint X D → Disjoint X D
mpr₁ mpr₂ : Disjoint X D → ¬M.Indep X → X ⊆ M.E → ¬(M.Indep X ∧ Disjoint X D) ∧ X ⊆ M.E ∧ Disjoint X D
mpr₃ : Disjoint X D → ¬M.Indep X → X ⊆ M.E → ¬(M.Indep X ∧ Disjoint X D)
mpr₄ : Disjoint X D → ¬M.Indep X → X ⊆ M.E → X ⊆ M.E
⊢ ¬(M.Indep X ∧ Disjoint X D) ∧ X ⊆ M.E ∧ Disjoint X D ↔ (¬M.Indep X ∧ X ⊆ M.E) ∧ Disjoint X D
have mpr₅ : Disjoint X D → ¬M.Indep X → X ⊆ M.E → Disjoint X D
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (goal)
Goal:
α : Type u_1
M : Matroid α
D X : Set α
mp : ¬(M.Indep X ∧ Disjoint X D) ∧ X ⊆ M.E ∧ Disjoint X D → (¬M.Indep X ∧ X ⊆ M.E) ∧ Disjoint X D
mpr : (¬M.Indep X ∧ X ⊆ M.E) ∧ Disjoint X D → ¬(M.Indep X ∧ Disjoint X D) ∧ X ⊆ M.E ∧ Disjoint X D
mp₁ mp₂ : ¬(M.Indep X ∧ Disjoint X D) → X ⊆ M.E → Disjoint X D → (¬M.Indep X ∧ X ⊆ M.E) ∧ Disjoint X D
mp₃ : ¬(M.Indep X ∧ Disjoint X D) → X ⊆ M.E → Disjoint X D → ¬M.Indep X
mp₄ : ¬(M.Indep X ∧ Disjoint X D) → X ⊆ M.E → Disjoint X D → X ⊆ M.E
mp₅ : ¬(M.Indep X ∧ Disjoint X D) → X ⊆ M.E → Disjoint X D → Disjoint X D
mpr₁ mpr₂ : Disjoint X D → ¬M.Indep X → X ⊆ M.E → ¬(M.Indep X ∧ Disjoint X D) ∧ X ⊆ M.E ∧ Disjoint X D
mpr₃ : Disjoint X D → ¬M.Indep X → X ⊆ M.E → ¬(M.Indep X ∧ Disjoint X D)
mpr₄ : Disjoint X D → ¬M.Indep X → X ⊆ M.E → X ⊆ M.E
mpr₅ : Disjoint X D → ¬M.Indep X → X ⊆ M.E → Disjoint X D
⊢ ¬(M.Indep X ∧ Disjoint X D) ∧ X ⊆ M.E ∧ Disjoint X D ↔ (¬M.Indep X ∧ X ⊆ M.E) ∧ Disjoint X D
have mp₆ : X ⊆ M.E → Disjoint X D → M.Indep X → ¬M.Indep X → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (goal)
Goal:
α : Type u_1
M : Matroid α
D X : Set α
mp : ¬(M.Indep X ∧ Disjoint X D) ∧ X ⊆ M.E ∧ Disjoint X D → (¬M.Indep X ∧ X ⊆ M.E) ∧ Disjoint X D
mpr : (¬M.Indep X ∧ X ⊆ M.E) ∧ Disjoint X D → ¬(M.Indep X ∧ Disjoint X D) ∧ X ⊆ M.E ∧ Disjoint X D
mp₁ mp₂ : ¬(M.Indep X ∧ Disjoint X D) → X ⊆ M.E → Disjoint X D → (¬M.Indep X ∧ X ⊆ M.E) ∧ Disjoint X D
mp₃ : ¬(M.Indep X ∧ Disjoint X D) → X ⊆ M.E → Disjoint X D → ¬M.Indep X
mp₄ : ¬(M.Indep X ∧ Disjoint X D) → X ⊆ M.E → Disjoint X D → X ⊆ M.E
mp₅ : ¬(M.Indep X ∧ Disjoint X D) → X ⊆ M.E → Disjoint X D → Disjoint X D
mpr₁ mpr₂ : Disjoint X D → ¬M.Indep X → X ⊆ M.E → ¬(M.Indep X ∧ Disjoint X D) ∧ X ⊆ M.E ∧ Disjoint X D
mpr₃ : Disjoint X D → ¬M.Indep X → X ⊆ M.E → ¬(M.Indep X ∧ Disjoint X D)
mpr₄ : Disjoint X D → ¬M.Indep X → X ⊆ M.E → X ⊆ M.E
mpr₅ : Disjoint X D → ¬M.Indep X → X ⊆ M.E → Disjoint X D
mp₆ : X ⊆ M.E → Disjoint X D → M.Indep X → ¬M.Indep X → False
⊢ ¬(M.Indep X ∧ Disjoint X D) ∧ X ⊆ M.E ∧ Disjoint X D ↔ (¬M.Indep X ∧ X ⊆ M.E) ∧ Disjoint X D
have mp₇ : X ⊆ M.E → Disjoint X D → M.Indep X → ¬Disjoint X D → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (goal)
Goal:
α : Type u_1
M : Matroid α
D X : Set α
mp : ¬(M.Indep X ∧ Disjoint X D) ∧ X ⊆ M.E ∧ Disjoint X D → (¬M.Indep X ∧ X ⊆ M.E) ∧ Disjoint X D
mpr : (¬M.Indep X ∧ X ⊆ M.E) ∧ Disjoint X D → ¬(M.Indep X ∧ Disjoint X D) ∧ X ⊆ M.E ∧ Disjoint X D
mp₁ mp₂ : ¬(M.Indep X ∧ Disjoint X D) → X ⊆ M.E → Disjoint X D → (¬M.Indep X ∧ X ⊆ M.E) ∧ Disjoint X D
mp₃ : ¬(M.Indep X ∧ Disjoint X D) → X ⊆ M.E → Disjoint X D → ¬M.Indep X
mp₄ : ¬(M.Indep X ∧ Disjoint X D) → X ⊆ M.E → Disjoint X D → X ⊆ M.E
mp₅ : ¬(M.Indep X ∧ Disjoint X D) → X ⊆ M.E → Disjoint X D → Disjoint X D
mpr₁ mpr₂ : Disjoint X D → ¬M.Indep X → X ⊆ M.E → ¬(M.Indep X ∧ Disjoint X D) ∧ X ⊆ M.E ∧ Disjoint X D
mpr₃ : Disjoint X D → ¬M.Indep X → X ⊆ M.E → ¬(M.Indep X ∧ Disjoint X D)
mpr₄ : Disjoint X D → ¬M.Indep X → X ⊆ M.E → X ⊆ M.E
mpr₅ : Disjoint X D → ¬M.Indep X → X ⊆ M.E → Disjoint X D
mp₆ : X ⊆ M.E → Disjoint X D → M.Indep X → ¬M.Indep X → False
mp₇ : X ⊆ M.E → Disjoint X D → M.Indep X → ¬Disjoint X D → False
⊢ ¬(M.Indep X ∧ Disjoint X D) ∧ X ⊆ M.E ∧ Disjoint X D ↔ (¬M.Indep X ∧ X ⊆ M.E) ∧ Disjoint X D
have mpr₆ : Disjoint X D → ¬M.Indep X → X ⊆ M.E → M.Indep X → Disjoint X D → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (goal)
Goal:
α : Type u_1
M : Matroid α
B D : Set α
⊢ (M ＼ D).IsBase B ↔ M.IsBasis B (M.E \ D)
have rw : (M ↾ M.E \ D).IsBase B ↔ M.IsBasis B (M.E \ D)
Tactic: rw [← restrict_compl, isBase_restrict_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (goal)
Goal:
α : Type u_1
M : Matroid α
B D : Set α
rw : (M ↾ M.E \ D).IsBase B ↔ M.IsBasis B (M.E \ D)
⊢ (M ＼ D).IsBase B ↔ M.IsBasis B (M.E \ D)
have rw₁ : M.IsBasis B (M.E \ D) ↔ M.IsBasis B (M.E \ D)
Tactic: rw [← restrict_compl, isBase_restrict_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (goal)
Goal:
α : Type u_1
M : Matroid α
I D X : Set α
⊢ (M ＼ D).IsBasis I X ↔ M.IsBasis I X ∧ Disjoint X D
have rw : (M ↾ M.E \ D).IsBasis I X ↔ M.IsBasis I X ∧ Disjoint X D
Tactic: rw [← restrict_compl, isBasis_restrict_iff, subset_diff, ← and_assoc,
    and_iff_left_of_imp IsBasis.subset_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (goal)
Goal:
α : Type u_1
M : Matroid α
I D X : Set α
rw : (M ↾ M.E \ D).IsBasis I X ↔ M.IsBasis I X ∧ Disjoint X D
⊢ (M ＼ D).IsBasis I X ↔ M.IsBasis I X ∧ Disjoint X D
have rw₁ : M.IsBasis I X ∧ X ⊆ M.E \ D ↔ M.IsBasis I X ∧ Disjoint X D
Tactic: rw [← restrict_compl, isBasis_restrict_iff, subset_diff, ← and_assoc,
    and_iff_left_of_imp IsBasis.subset_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (goal)
Goal:
α : Type u_1
M : Matroid α
I D X : Set α
rw : (M ↾ M.E \ D).IsBasis I X ↔ M.IsBasis I X ∧ Disjoint X D
rw₁ : M.IsBasis I X ∧ X ⊆ M.E \ D ↔ M.IsBasis I X ∧ Disjoint X D
⊢ (M ＼ D).IsBasis I X ↔ M.IsBasis I X ∧ Disjoint X D
have rw₂ : M.IsBasis I X ∧ X ⊆ M.E ∧ Disjoint X D ↔ M.IsBasis I X ∧ Disjoint X D
Tactic: rw [← restrict_compl, isBasis_restrict_iff, subset_diff, ← and_assoc,
    and_iff_left_of_imp IsBasis.subset_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (goal)
Goal:
α : Type u_1
M : Matroid α
I D X : Set α
rw : (M ↾ M.E \ D).IsBasis I X ↔ M.IsBasis I X ∧ Disjoint X D
rw₁ : M.IsBasis I X ∧ X ⊆ M.E \ D ↔ M.IsBasis I X ∧ Disjoint X D
rw₂ : M.IsBasis I X ∧ X ⊆ M.E ∧ Disjoint X D ↔ M.IsBasis I X ∧ Disjoint X D
⊢ (M ＼ D).IsBasis I X ↔ M.IsBasis I X ∧ Disjoint X D
have rw₃ : (M.IsBasis I X ∧ X ⊆ M.E) ∧ Disjoint X D ↔ M.IsBasis I X ∧ Disjoint X D
Tactic: rw [← restrict_compl, isBasis_restrict_iff, subset_diff, ← and_assoc,
    and_iff_left_of_imp IsBasis.subset_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (goal)
Goal:
α : Type u_1
M : Matroid α
I D X : Set α
rw : (M ↾ M.E \ D).IsBasis I X ↔ M.IsBasis I X ∧ Disjoint X D
rw₁ : M.IsBasis I X ∧ X ⊆ M.E \ D ↔ M.IsBasis I X ∧ Disjoint X D
rw₂ : M.IsBasis I X ∧ X ⊆ M.E ∧ Disjoint X D ↔ M.IsBasis I X ∧ Disjoint X D
rw₃ : (M.IsBasis I X ∧ X ⊆ M.E) ∧ Disjoint X D ↔ M.IsBasis I X ∧ Disjoint X D
⊢ (M ＼ D).IsBasis I X ↔ M.IsBasis I X ∧ Disjoint X D
have rw₄ : M.IsBasis I X ∧ Disjoint X D ↔ M.IsBasis I X ∧ Disjoint X D
Tactic: rw [← restrict_compl, isBasis_restrict_iff, subset_diff, ← and_assoc,
    and_iff_left_of_imp IsBasis.subset_ground]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (goal)
Goal:
α : Type u_1
M : Matroid α
I D X : Set α
⊢ (M ＼ D).IsBasis' I X ↔ M.IsBasis' I (X \ D)
have rw : M.IsBasis' I (X \ D) → Disjoint ((M.E ∩ X) \ D) D
Tactic: rw [isBasis'_iff_isBasis_inter_ground, delete_isBasis_iff, delete_ground, diff_eq, inter_comm M.E,
    ← inter_assoc, ← diff_eq, ← isBasis'_iff_isBasis_inter_ground, and_iff_left_iff_imp,
    inter_comm, ← inter_diff_assoc]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (goal)
Goal:
α : Type u_1
M : Matroid α
I D X : Set α
h : M.IsBasis I X
hX : Disjoint X D
⊢ (M ＼ D).IsBasis I X
have rw : M.IsBasis I X ∧ Disjoint X D
Tactic: rw [delete_isBasis_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (goal)
Goal:
α : Type u_1
M : Matroid α
B D : Set α
hD : M.Coindep D
⊢ (M ＼ D).IsBase B ↔ M.IsBase B ∧ Disjoint B D
have rw : M.IsBasis B (M.E \ D) ↔ M.IsBase B ∧ Disjoint B D
Tactic: rw [Matroid.delete_isBase_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (goal)
Goal:
α : Type u_1
M : Matroid α
B D : Set α
hD : M.Coindep D
⊢ M.IsBasis B (M.E \ D) ↔ M.IsBase B ∧ Disjoint B D
have refine_1 : ∀ (h : M.IsBasis B (M.E \ D)), M.IsBase B ∧ Disjoint B D
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (goal)
Goal:
α : Type u_1
M : Matroid α
B D : Set α
hD : M.Coindep D
refine_1 : ∀ (h : M.IsBasis B (M.E \ D)), M.IsBase B ∧ Disjoint B D
⊢ M.IsBasis B (M.E \ D) ↔ M.IsBase B ∧ Disjoint B D
have refine_2 : ∀ (h : M.IsBase B ∧ Disjoint B D), M.IsBasis B (M.E \ D)
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (hypothesis)
Goal:
α : Type u_1
M : Matroid α
B D : Set α
hD : M.Coindep D
h : M.IsBasis B (M.E \ D)
⊢ M.IsBase B ∧ Disjoint B D
have hss : B ⊆ M.E \ D
Tactic: have hss := h.subset
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (hypothesis)
Goal:
α : Type u_1
M : Matroid α
B D : Set α
hD : M.Coindep D
h : M.IsBasis B (M.E \ D)
hss : B ⊆ M.E \ D
⊢ M.IsBase B ∧ Disjoint B D
have hss₁ : B ⊆ M.E ∧ Disjoint B D
Tactic: rw [subset_diff] at hss
Cleared hypotheses: hss
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (hypothesis)
Goal:
α : Type u_1
M : Matroid α
B D : Set α
hD : M.Coindep D
h : M.IsBasis B (M.E \ D)
hss : B ⊆ M.E ∧ Disjoint B D
⊢ M.IsBase B ∧ Disjoint B D
have hcl : M.IsBasis B (M.closure (M.E \ D))
Tactic: have hcl := h.isBasis_closure_right
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Minor.Delete (hypothesis)
Goal:
α : Type u_1
M : Matroid α
B D : Set α
hD : M.Coindep D
h : M.IsBasis B (M.E \ D)
hss : B ⊆ M.E ∧ Disjoint B D
hcl : M.IsBasis B (M.closure (M.E \ D))
⊢ M.IsBase B ∧ Disjoint B D
have hcl₁ : M.IsBase B
Tactic: rw [hD.closure_compl, isBasis_ground_iff] at hcl
Cleared hypotheses: hcl