awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
Goal:
α : Type u_1
M : Matroid α
I D : Set α
hID : Disjoint I D
⊢ M.Indep I ↔ (M ＼ D).Indep I

Tactic:
⟨fun h ↦ h.indep_delete_of_disjoint hID, fun h ↦ h.of_delete⟩

Premises used: Iff.intro, Matroid.Indep.indep_delete_of_disjoint, Matroid.Indep.of_delete
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
Goal:
α : Type u_1
M : Matroid α
D X : Set α
rw : ¬(M.Indep X ∧ Disjoint X D) ∧ X ⊆ M.E ∧ Disjoint X D ↔ (¬M.Indep X ∧ X ⊆ M.E) ∧ Disjoint X D
⊢ (M ＼ D).Dep X ↔ M.Dep X ∧ Disjoint X D

Tactic:
rw [dep_iff, dep_iff, delete_indep_iff, delete_ground, subset_diff]

Premises used: Set.subset_diff, Matroid.delete_ground, Matroid.delete_indep_iff, Matroid.dep_iff
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
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
mpr₆ : Disjoint X D → ¬M.Indep X → X ⊆ M.E → 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

Tactic:
tauto
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
Goal:
α : Type u_1
M : Matroid α
B D : Set α
rw : (M ↾ M.E \ D).IsBase B ↔ M.IsBasis B (M.E \ D)
rw₁ rw₂ : M.IsBasis B (M.E \ D) ↔ M.IsBasis B (M.E \ D)
⊢ (M ＼ D).IsBase B ↔ M.IsBasis B (M.E \ D)

Tactic:
rw [← restrict_compl, isBase_restrict_iff]

Premises used: Matroid.isBase_restrict_iff, Matroid.restrict_compl
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
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
rw₄ rw₅ : M.IsBasis I X ∧ Disjoint X D ↔ M.IsBasis I X ∧ Disjoint X D
⊢ (M ＼ 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]

Premises used: and_iff_left_of_imp, Matroid.IsBasis.subset_ground, Matroid.isBasis_restrict_iff, Set.subset_diff, and_assoc, Matroid.restrict_compl
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
Goal:
α : Type u_1
M : Matroid α
I D X : Set α
rw : M.IsBasis' I (X \ D) → Disjoint ((M.E ∩ X) \ D) D
⊢ (M ＼ D).IsBasis' I X ↔ M.IsBasis' I (X \ 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]

Premises used: Matroid.E, Set.diff_eq, Matroid.isBasis'_iff_isBasis_inter_ground, Matroid.delete_ground, Set.inter_comm, Matroid.delete_isBasis_iff, Set.inter_diff_assoc, and_iff_left_iff_imp, Set.inter_assoc
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
Goal:
α : Type u_1
M : Matroid α
I D X : Set α
⊢ M.IsBasis' I (X \ D) → Disjoint ((M.E ∩ X) \ D) D

Tactic:
fun _ ↦ disjoint_sdiff_left

Premises used: Set.disjoint_sdiff_left
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
Goal:
α : Type u_1
M : Matroid α
I D X : Set α
⊢ M.IsBasis' I (X \ D) → Disjoint ((M.E ∩ X) \ D) D

Tactic:
exact fun _ ↦ disjoint_sdiff_left

Premises used: Set.disjoint_sdiff_left
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
Goal:
α : Type u_1
M : Matroid α
I D X : Set α
h : (M ＼ D).IsBasis I X
⊢ M.IsBasis I X

Tactic:
(delete_isBasis_iff.mp h).1

Premises used: And.left, Iff.mp, Matroid.delete_isBasis_iff
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
Goal:
α : Type u_1
M : Matroid α
I D X : Set α
h : M.IsBasis I X
hX : Disjoint X D
rw : M.IsBasis I X ∧ Disjoint X D
⊢ (M ＼ D).IsBasis I X

Tactic:
rw [delete_isBasis_iff]

Premises used: Matroid.delete_isBasis_iff
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
Goal:
α : Type u_1
M : Matroid α
I D X : Set α
h : M.IsBasis I X
hX : Disjoint X D
⊢ M.IsBasis I X ∧ Disjoint X D

Tactic:
⟨h, hX⟩

Premises used: And.intro
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
Goal:
α : Type u_1
M : Matroid α
I D X : Set α
h : M.IsBasis I X
hX : Disjoint X D
⊢ M.IsBasis I X ∧ Disjoint X D

Tactic:
exact ⟨h, hX⟩
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
Goal:
α : Type u_1
M : Matroid α
B D : Set α
hD : M.Coindep D
rw : M.IsBasis B (M.E \ D) ↔ M.IsBase B ∧ Disjoint B D
⊢ (M ＼ D).IsBase B ↔ M.IsBase B ∧ Disjoint B D

Tactic:
rw [Matroid.delete_isBase_iff]

Premises used: Matroid.delete_isBase_iff
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
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

Tactic:
⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
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
refine_2 : ∀ (h : M.IsBase B ∧ Disjoint B D), M.IsBasis B (M.E \ D)
⊢ M.IsBasis B (M.E \ D) ↔ M.IsBase B ∧ Disjoint B D

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
Goal:
α : Type u_1
M : Matroid α
B D : Set α
hD : M.Coindep D
h : M.IsBasis B (M.E \ D)
⊢ B ⊆ M.E \ D

Tactic:
have hss := h.subset
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
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
⊢ B ⊆ M.E ∧ Disjoint B D

Tactic:
rw [subset_diff] at hss

Premises used: Set.subset_diff
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
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.IsBasis B (M.closure (M.E \ D))

Tactic:
have hcl := h.isBasis_closure_right
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
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

Tactic:
rw [hD.closure_compl, isBasis_ground_iff] at hcl

Premises used: Matroid.isBasis_ground_iff, Matroid.Coindep.closure_compl
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
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.IsBase B
⊢ M.IsBase B ∧ Disjoint B D

Tactic:
⟨hcl, hss.2⟩

Premises used: And.right, And.intro
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
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.IsBase B
⊢ M.IsBase B ∧ Disjoint B D

Tactic:
exact ⟨hcl, hss.2⟩
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
Goal:
α : Type u_1
M : Matroid α
B D : Set α
hD : M.Coindep D
h : M.IsBase B ∧ Disjoint B D
⊢ B ⊆ M.E \ D

Tactic:
simp [subset_diff, h.1.subset_ground, h.2]

Premises used: Set.subset_diff, Matroid.IsBase.subset_ground, And.right, And.left
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
Goal:
α : Type u_1
M : Matroid α
B D : Set α
hD : M.Coindep D
h : M.IsBase B ∧ Disjoint B D
⊢ M.IsBasis B (M.E \ D)

Tactic:
exact h.1.isBasis_ground.isBasis_subset (by simp [subset_diff, h.1.subset_ground, h.2])
    diff_subset

Premises used: Set.diff_subset, Matroid.IsBasis.isBasis_subset, Matroid.IsBase.isBasis_ground, And.left
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
Goal:
α : Type u_1
M : Matroid α
D : Set α
inst : M.RankPos
hD : M.Coindep D
rw : ¬(M.IsBase ∅ ∧ Disjoint ∅ D)
⊢ (M ＼ D).RankPos

Tactic:
rw [rankPos_iff, hD.delete_isBase_iff]

Premises used: Matroid.rankPos_iff, Matroid.Coindep.delete_isBase_iff
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
Goal:
α : Type u_1
M : Matroid α
D : Set α
inst : M.RankPos
hD : M.Coindep D
⊢ ¬(M.IsBase ∅ ∧ Disjoint ∅ D)

Tactic:
simp [M.empty_not_isBase]

Premises used: Matroid.empty_not_isBase
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
Goal:
α : Type u_1
M : Matroid α
D S : Set α
hD : M.Coindep D
simp : S ⊆ M.E → Disjoint S D → ((∃ (B : Set α), M.IsBase B ∧ Disjoint B D ∧ B ⊆ S) ↔ ∃ (B : Set α), M.IsBase B ∧ B ⊆ S)
⊢ (M ＼ D).Spanning S ↔ M.Spanning S ∧ Disjoint S D

Tactic:
simp only [spanning_iff_exists_isBase_subset', hD.delete_isBase_iff, and_assoc, delete_ground,
    subset_diff, and_congr_left_iff, and_imp]

Premises used: and_imp, Set.subset_diff, Matroid.delete_ground, Matroid.spanning_iff_exists_isBase_subset', and_congr_left_iff, and_assoc, Matroid.Coindep.delete_isBase_iff
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
Goal:
α : Type u_1
M : Matroid α
D S : Set α
hD : M.Coindep D
⊢ S ⊆ M.E → Disjoint S D → ((∃ (B : Set α), M.IsBase B ∧ Disjoint B D ∧ B ⊆ S) ↔ ∃ (B : Set α), M.IsBase B ∧ B ⊆ S)

Tactic:
fun hSE hSD ↦ ⟨fun ⟨B, hB, hBD, hBS⟩ ↦ ⟨B, hB, hBS⟩, fun ⟨B, hB, hBS⟩ ↦ ⟨B, hB, ?_, hBS⟩⟩

Premises used: Disjoint, Exists, Matroid.IsBase, _private.0.Matroid.Coindep.delete_spanning_iff.match_4, HasSubset.Subset, And, And.intro, Iff.intro, _private.0.Matroid.Coindep.delete_spanning_iff.match_5, Exists.intro
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
Goal:
α : Type u_1
M : Matroid α
D S : Set α
hD : M.Coindep D
refine :
  ∀ (hSE : S ⊆ M.E) (hSD : Disjoint S D),
    (∃ (B : Set α), M.IsBase B ∧ B ⊆ S) → ∀ (B : Set α) (hB : M.IsBase B) (hBS : B ⊆ S), Disjoint B D
⊢ S ⊆ M.E → Disjoint S D → ((∃ (B : Set α), M.IsBase B ∧ Disjoint B D ∧ B ⊆ S) ↔ ∃ (B : Set α), M.IsBase B ∧ B ⊆ S)

Tactic:
refine fun hSE hSD ↦ ⟨fun ⟨B, hB, hBD, hBS⟩ ↦ ⟨B, hB, hBS⟩, fun ⟨B, hB, hBS⟩ ↦ ⟨B, hB, ?_, hBS⟩⟩
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
Goal:
α : Type u_1
M : Matroid α
D S : Set α
hD : M.Coindep D
hSE : S ⊆ M.E
hSD : Disjoint S D
h : ∃ (B : Set α), M.IsBase B ∧ B ⊆ S
B : Set α
hB : M.IsBase B
hBS : B ⊆ S
⊢ Disjoint B D

Tactic:
hSD.mono_left hBS

Premises used: Disjoint.mono_left
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
Goal:
α : Type u_1
M : Matroid α
D S : Set α
hD : M.Coindep D
hSE : S ⊆ M.E
hSD : Disjoint S D
h : ∃ (B : Set α), M.IsBase B ∧ B ⊆ S
B : Set α
hB : M.IsBase B
hBS : B ⊆ S
⊢ Disjoint B D

Tactic:
exact hSD.mono_left hBS

Premises used: Disjoint.mono_left
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
Goal:
α : Type u_1
M : Matroid α
e : α
D : Set α
rw : (M ＼ D).Dep {e} ↔ M.IsLoop e ∧ e ∉ D
rw₁ : M.Dep {e} ∧ Disjoint {e} D ↔ M.IsLoop e ∧ e ∉ D
rw₂ : M.Dep {e} ∧ e ∉ D ↔ M.IsLoop e ∧ e ∉ D
rw₃ rw₄ : M.IsLoop e ∧ e ∉ D ↔ M.IsLoop e ∧ e ∉ D
⊢ (M ＼ D).IsLoop e ↔ M.IsLoop e ∧ e ∉ D

Tactic:
rw [← singleton_dep, delete_dep_iff, disjoint_singleton_left, singleton_dep]

Premises used: Set.disjoint_singleton_left, Matroid.delete_dep_iff, Matroid.singleton_dep
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
Goal:
α : Type u_1
M : Matroid α
e : α
D : Set α
rw : (M ＼ D).Indep {e} ↔ M.IsNonloop e ∧ e ∉ D
rw₁ : M.Indep {e} ∧ Disjoint {e} D ↔ M.IsNonloop e ∧ e ∉ D
rw₂ : M.Indep {e} ∧ e ∉ D ↔ M.IsNonloop e ∧ e ∉ D
rw₃ rw₄ : M.IsNonloop e ∧ e ∉ D ↔ M.IsNonloop e ∧ e ∉ D
⊢ (M ＼ D).IsNonloop e ↔ M.IsNonloop e ∧ e ∉ D

Tactic:
rw [← indep_singleton, delete_indep_iff, disjoint_singleton_left, indep_singleton]

Premises used: Set.disjoint_singleton_left, Matroid.indep_singleton, Matroid.delete_indep_iff
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
Goal:
α : Type u_1
M : Matroid α
e : α
D : Set α
h : (M ＼ D).IsNonloop e
⊢ M.IsNonloop e

Tactic:
(delete_isNonloop_iff.1 h).1

Premises used: Matroid.delete_isNonloop_iff, And.left, Iff.mp
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
Goal:
α : Type u_1
M : Matroid α
e : α
D : Set α
he : e ∉ D
⊢ M.IsNonloop e ↔ (M ＼ D).IsNonloop e

Tactic:
⟨fun h ↦ delete_isNonloop_iff.2 ⟨h, he⟩, fun h ↦ h.of_delete⟩

Premises used: Iff.mpr, Matroid.IsNonloop.of_delete, Matroid.delete_isNonloop_iff, And.intro, Iff.intro
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
Goal:
α : Type u_1
M : Matroid α
rw : M ＼ M.loops = M ↾ {e : α | M.IsNonloop e}
rw₁ : M ↾ M.E \ M.loops = M ↾ {e : α | M.IsNonloop e}
rw₂ rw₃ : M ↾ {e : α | M.IsNonloop e} = M ↾ {e : α | M.IsNonloop e}
⊢ M ＼ M.loops = M.removeLoops

Tactic:
rw [removeLoops, delete_eq_restrict, compl_loops_eq]

Premises used: Matroid.delete_eq_restrict, Matroid.removeLoops, Matroid.compl_loops_eq
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
Goal:
α : Type u_1
M : Matroid α
D C : Set α
rw : M.IsCircuit C → Disjoint C D → C ⊆ M.E
⊢ (M ＼ D).IsCircuit C ↔ M.IsCircuit C ∧ Disjoint C D

Tactic:
rw [delete_eq_restrict, restrict_isCircuit_iff, and_congr_right_iff, subset_diff,
    and_iff_right_iff_imp]

Premises used: Matroid.restrict_isCircuit_iff, Set.subset_diff, and_congr_right_iff, Matroid.delete_eq_restrict, and_iff_right_iff_imp
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
Goal:
α : Type u_1
M : Matroid α
D C : Set α
⊢ M.IsCircuit C → Disjoint C D → C ⊆ M.E

Tactic:
fun h _ ↦ h.subset_ground

Premises used: Matroid.IsCircuit.subset_ground
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
Goal:
α : Type u_1
M : Matroid α
D C : Set α
⊢ M.IsCircuit C → Disjoint C D → C ⊆ M.E

Tactic:
exact fun h _ ↦ h.subset_ground
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
Goal:
α : Type u_1
M : Matroid α
D C : Set α
h : (M ＼ D).IsCircuit C
⊢ M.IsCircuit C

Tactic:
(delete_isCircuit_iff.1 h).1

Premises used: And.left, Iff.mp, Matroid.delete_isCircuit_iff
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
Goal:
α : Type u_1
M : Matroid α
D C : Set α
hCD : Disjoint C D
⊢ M.IsCircuit C ↔ (M ＼ D).IsCircuit C

Tactic:
⟨fun h ↦ delete_isCircuit_iff.2 ⟨h, hCD⟩, fun h ↦ h.of_delete⟩

Premises used: Iff.mpr, Matroid.IsCircuit.of_delete, And.intro, Iff.intro, Matroid.delete_isCircuit_iff
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
Goal:
α : Type u_1
M : Matroid α
D X : Set α
rw : M.closure (X \ D) \ D ⊆ M.E
⊢ (M ＼ D).closure X = M.closure (X \ D) \ D

Tactic:
rw [← restrict_compl, restrict_closure_eq', sdiff_sdiff_self, bot_eq_empty, union_empty,
    diff_eq, inter_comm M.E, ← inter_assoc X, ← diff_eq, closure_inter_ground,
    ← inter_assoc, ← diff_eq, inter_eq_left]

Premises used: Set.inter_eq_left, Set.union_empty, Matroid.E, Set.diff_eq, Set.bot_eq_empty, sdiff_sdiff_self, Set.inter_comm, Matroid.closure_inter_ground, Matroid.restrict_closure_eq', Matroid.restrict_compl, Set.inter_assoc
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
Goal:
α : Type u_1
M : Matroid α
D X : Set α
⊢ M.closure (X \ D) \ D ⊆ M.E

Tactic:
diff_subset.trans (M.closure_subset_ground _)

Premises used: Set.diff_subset, Matroid.closure_subset_ground, HasSubset.Subset.trans
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
Goal:
α : Type u_1
M : Matroid α
D X : Set α
⊢ M.closure (X \ D) \ D ⊆ M.E

Tactic:
exact diff_subset.trans (M.closure_subset_ground _)

Premises used: Set.diff_subset, Matroid.closure_subset_ground, HasSubset.Subset.trans
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
Goal:
α : Type u_1
M : Matroid α
D X : Set α
hXD : Disjoint X D
rw : M.closure (X \ D) \ D = M.closure X \ D
rw₁ rw₂ : M.closure X \ D = M.closure X \ D
⊢ (M ＼ D).closure X = M.closure X \ D

Tactic:
rw [delete_closure_eq, hXD.sdiff_eq_left]

Premises used: Matroid.delete_closure_eq, Disjoint.sdiff_eq_left
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
Goal:
α : Type u_1
M : Matroid α
D : Set α
⊢ (M ＼ D).loops = M.loops \ D

Tactic:
simp [loops]

Premises used: Matroid.loops
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
Goal:
α : Type u_1
e : α
M : Matroid α
D : Set α
rw : e ∈ M.E → e ∉ D → (e ∉ M.closure ((M.E \ D) \ {e}) ↔ e ∉ M.closure ((M.E \ D) \ {e}))
⊢ (M ＼ D).IsColoop e ↔ e ∉ M.closure ((M.E \ D) \ {e}) ∧ e ∈ M.E ∧ e ∉ D

Tactic:
rw [delete_eq_restrict, restrict_isColoop_iff diff_subset, mem_diff, and_congr_left_iff, and_imp]

Premises used: Set.diff_subset, and_imp, Matroid.restrict_isColoop_iff, Matroid.delete_eq_restrict, Set.mem_diff, and_congr_left_iff
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
Goal:
α : Type u_1
e : α
M : Matroid α
D : Set α
⊢ e ∈ M.E → e ∉ D → (e ∉ M.closure ((M.E \ D) \ {e}) ↔ e ∉ M.closure ((M.E \ D) \ {e}))

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
Goal:
α : Type u_1
M_1 M' N : Matroid α
e f : α
I B D_1 R X : Set α
M : Matroid α
inst : M.Finitary
D : Set α
⊢ (M ＼ D).Finitary

Tactic:
inferInstanceAs <| Finitary (M ↾ (M.E \ D))

Premises used: _private.0.Matroid.delete_finitary._proof_1
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
Goal:
α : Type u_1
M M' N : Matroid α
e f : α
I B D R X : Set α
inst : M.Finite
⊢ (M ＼ D).Finite

Tactic:
⟨M.ground_finite.diff⟩

Premises used: Set.Finite.diff, Matroid.Finite.mk, Matroid.ground_finite
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
Goal:
α : Type u_1
M M' N : Matroid α
e f : α
I B D R X : Set α
inst : M.RankFinite
⊢ (M ＼ D).RankFinite

Tactic:
restrict_rankFinite _

Premises used: Matroid.restrict_rankFinite, Matroid.delete
-- Module: Mathlib.Combinatorics.Matroid.Minor.Order
Goal:
α : Type u_1
M : Matroid α
C D : Set α
⊢ M ／ C ＼ D ≤m M

Tactic:
⟨C, D, rfl⟩

Premises used: Matroid.IsMinor, Exists.intro, rfl
-- Module: Mathlib.Combinatorics.Matroid.Minor.Order
Goal:
α : Type u_1
M N : Matroid α
h : N ≤m M
obtain :
  ∀ (C D : Set α), ∃ (C_1 : Set α) (D_1 : Set α), C_1 ⊆ M.E ∧ D_1 ⊆ M.E ∧ Disjoint C_1 D_1 ∧ M ／ C ＼ D = M ／ C_1 ＼ D_1
⊢ ∃ (C : Set α) (D : Set α), C ⊆ M.E ∧ D ⊆ M.E ∧ Disjoint C D ∧ N = M ／ C ＼ D

Tactic:
obtain ⟨C, D, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.Combinatorics.Matroid.Minor.Order
Goal:
α : Type u_1
M : Matroid α
C D : Set α
⊢ M ／ C ＼ D = M ／ (C ∩ M.E) ＼ ((D ∩ M.E) \ C)

Tactic:
simp [delete_eq_delete_iff, inter_assoc, inter_diff_assoc]

Premises used: Set.inter_diff_assoc, Matroid.delete_eq_delete_iff, Set.inter_assoc
-- Module: Mathlib.Combinatorics.Matroid.Minor.Order
Goal:
α : Type u_1
M : Matroid α
C D : Set α
⊢ ∃ (C_1 : Set α) (D_1 : Set α), C_1 ⊆ M.E ∧ D_1 ⊆ M.E ∧ Disjoint C_1 D_1 ∧ M ／ C ＼ D = M ／ C_1 ＼ D_1

Tactic:
exact ⟨C ∩ M.E, (D ∩ M.E) \ C, inter_subset_right, diff_subset.trans inter_subset_right,
    disjoint_sdiff_right.mono_left inter_subset_left,
    by simp [delete_eq_delete_iff, inter_assoc, inter_diff_assoc]⟩
-- Module: Mathlib.Combinatorics.Matroid.Minor.Order
Goal:
α : Type u_1
M N : Matroid α
h : N ≤m M
obtain : ∀ (C D : Set α), (M ／ C ＼ D).E ⊆ M.E
⊢ N.E ⊆ M.E

Tactic:
obtain ⟨C, D, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.Combinatorics.Matroid.Minor.Order
Goal:
α : Type u_1
M : Matroid α
C D : Set α
⊢ (M ／ C ＼ D).E ⊆ M.E

Tactic:
diff_subset.trans diff_subset

Premises used: Set.diff_subset, HasSubset.Subset.trans
-- Module: Mathlib.Combinatorics.Matroid.Minor.Order
Goal:
α : Type u_1
M : Matroid α
C D : Set α
⊢ (M ／ C ＼ D).E ⊆ M.E

Tactic:
exact diff_subset.trans diff_subset

Premises used: Set.diff_subset, HasSubset.Subset.trans
-- Module: Mathlib.Combinatorics.Matroid.Minor.Order
Goal:
α : Type u_1
M : Matroid α
⊢ M = M ／ ∅ ＼ ∅

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Minor.Order
Goal:
α : Type u_1
M₁ M₂ M₃ : Matroid α
h : M₁ ≤m M₂
h' : M₂ ≤m M₃
obtain : ∀ (C₁ D₁ : Set α), M₂ ／ C₁ ＼ D₁ ≤m M₃
⊢ M₁ ≤m M₃

Tactic:
obtain ⟨C₁, D₁, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.Combinatorics.Matroid.Minor.Order
Goal:
α : Type u_1
M₂ M₃ : Matroid α
h' : M₂ ≤m M₃
C₁ D₁ : Set α
obtain : ∀ (C₂ D₂ : Set α), M₃ ／ C₂ ＼ D₂ ／ C₁ ＼ D₁ ≤m M₃
⊢ M₂ ／ C₁ ＼ D₁ ≤m M₃

Tactic:
obtain ⟨C₂, D₂, rfl⟩ := h'

Premises used: rfl
-- Module: Mathlib.Combinatorics.Matroid.Minor.Order
Goal:
α : Type u_1
M₃ : Matroid α
C₁ D₁ C₂ D₂ : Set α
rw rw₁ : M₃ ／ (C₂ ∪ C₁ \ D₂) ＼ (D₂ ∪ D₁) = M₃ ／ (C₂ ∪ C₁ \ D₂) ＼ (D₂ ∪ D₁)
⊢ M₃ ／ C₂ ＼ D₂ ／ C₁ ＼ D₁ = M₃ ／ (C₂ ∪ C₁ \ D₂) ＼ (D₂ ∪ D₁)

Tactic:
rw [contract_delete_contract_delete']

Premises used: Matroid.contract_delete_contract_delete'
-- Module: Mathlib.Combinatorics.Matroid.Minor.Order
Goal:
α : Type u_1
M₃ : Matroid α
C₁ D₁ C₂ D₂ : Set α
⊢ M₃ ／ C₂ ＼ D₂ ／ C₁ ＼ D₁ ≤m M₃

Tactic:
exact ⟨C₂ ∪ C₁ \ D₂, D₂ ∪ D₁, by rw [contract_delete_contract_delete']⟩
-- Module: Mathlib.Combinatorics.Matroid.Minor.Order
Goal:
α : Type u_1
M N : Matroid α
h : N ≤m M
hE : M.E ⊆ N.E
obtain : ∀ (C D : Set α) (hE : M.E ⊆ (M ／ C ＼ D).E), M = M ／ C ＼ D
⊢ M = N

Tactic:
obtain ⟨C, D, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.Combinatorics.Matroid.Minor.Order
Goal:
α : Type u_1
M : Matroid α
C D : Set α
hE : M.E ⊆ (M ／ C ＼ D).E
⊢ (M.E ⊆ M.E ∧ Disjoint M.E C) ∧ Disjoint M.E D

Tactic:
rw [delete_ground, contract_ground, subset_diff, subset_diff] at hE

Premises used: Matroid.contract_ground, Set.subset_diff, Matroid.delete_ground
-- Module: Mathlib.Combinatorics.Matroid.Minor.Order
Goal:
α : Type u_1
M : Matroid α
C D : Set α
hE : (M.E ⊆ M.E ∧ Disjoint M.E C) ∧ Disjoint M.E D
rw : M = M ／ (C ∩ M.E) ＼ D
rw₁ : M = M ／ ∅ ＼ D
rw₂ : M = M ＼ D
rw₃ : M = M ＼ (D ∩ M.E)
rw₄ : M = M ＼ ∅
rw₅ rw₆ : M = M
⊢ M = M ／ C ＼ D

Tactic:
rw [← contract_inter_ground_eq, hE.1.2.symm.inter_eq, contract_empty, ← delete_inter_ground_eq,
    hE.2.symm.inter_eq, delete_empty]

Premises used: Matroid.delete_inter_ground_eq, Matroid.delete_empty, Matroid.contract_empty, Disjoint.symm, And.right, And.left, Matroid.contract_inter_ground_eq, Disjoint.inter_eq
-- Module: Mathlib.Combinatorics.Matroid.Minor.Order
Goal:
α : Type u_1
M N : Matroid α
h : N ≤m M
h' : M ≤m N
⊢ N = M

Tactic:
h'.eq_of_ground_subset h.subset

Premises used: Matroid.IsMinor.eq_of_ground_subset, Matroid.IsMinor.subset
-- Module: Mathlib.Combinatorics.Matroid.Minor.Order
Goal:
α : Type u_1
M N : Matroid α
h : N ≤m M
⊢ N ≤ M

Tactic:
h
-- Module: Mathlib.Combinatorics.Matroid.Minor.Order
Goal:
α : Type u_1
M N : Matroid α
h : N <m M
⊢ N < M

Tactic:
h
-- Module: Mathlib.Combinatorics.Matroid.Minor.Order
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := (M M' : Matroid α) → Prop) (fun (M M' : Matroid α) ↦ M ≤ M') IsMinor

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.Matroid.Minor.Order
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := (M M' : Matroid α) → Prop) (fun (M M' : Matroid α) ↦ M < M') IsStrictMinor

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.Matroid.Minor.Order
Goal:
α : Type u_1
M N : Matroid α
⊢ N <m M ↔ N ≤m M ∧ N ≠ M

Tactic:
lt_iff_le_and_ne (α := Matroid α)

Premises used: lt_iff_le_and_ne
-- Module: Mathlib.Combinatorics.Matroid.Minor.Order
Goal:
α : Type u_1
M N : Matroid α
h : N <m M
⊢ N ≠ M

Tactic:
h.lt.ne

Premises used: Matroid.IsStrictMinor.lt, LT.lt.ne
-- Module: Mathlib.Combinatorics.Matroid.Minor.Order
Goal:
α : Type u_1
M : Matroid α
⊢ ¬M <m M

Tactic:
lt_irrefl M

Premises used: lt_irrefl
-- Module: Mathlib.Combinatorics.Matroid.Minor.Order
Goal:
α : Type u_1
M N : Matroid α
h : N <m M
⊢ N ≤m M

Tactic:
h.lt.le

Premises used: LT.lt.le, Matroid.IsStrictMinor.lt
-- Module: Mathlib.Combinatorics.Matroid.Minor.Order
Goal:
α : Type u_1
M N : Matroid α
h : N <m M
⊢ ¬M ≤m N

Tactic:
h.lt.not_ge

Premises used: Matroid.IsStrictMinor.lt, LT.lt.not_ge
-- Module: Mathlib.Combinatorics.Matroid.Minor.Order
Goal:
α : Type u_1
M N : Matroid α
h : N <m M
⊢ N.E ⊂ M.E

Tactic:
h.isMinor.subset.ssubset_of_ne (fun hE ↦ h.ne (h.isMinor.eq_of_ground_subset hE.symm.subset).symm)

Premises used: Matroid.IsStrictMinor.isMinor, Matroid.IsStrictMinor.ne, Eq.subset, Matroid.IsMinor.eq_of_ground_subset, Matroid.IsMinor.subset, Eq.symm, HasSubset.Subset.ssubset_of_ne
-- Module: Mathlib.Combinatorics.Matroid.Minor.Order
Goal:
α : Type u_1
M N : Matroid α
h_1 : N ≤m M ∧ N.E ⊂ M.E
h : N ≤m M
hss : N.E ⊂ M.E
h' : M ≤m N
rw rw₁ : N.E = N.E
⊢ N.E = M.E

Tactic:
rw [h'.antisymm h]

Premises used: Matroid.IsMinor.antisymm