awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
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)

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)
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
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)
rw : C' \ K ⊆ C'
⊢ C ⊆ C'

Tactic:
rw [← (hC.eq_of_dep_subset hdep2 (diff_subset_iff.2 (union_comm _ _ ▸ hC'ss)))]

Premises used: Iff.mpr, Matroid.IsCircuit.eq_of_dep_subset, Set.diff_subset_iff, Eq.rec, Set.union_comm
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
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' \ K ⊆ C'

Tactic:
diff_subset

Premises used: Set.diff_subset
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
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' \ K ⊆ C'

Tactic:
exact diff_subset

Premises used: Set.diff_subset
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
K C : Set α
hK : (M ／ C).IsCocircuit K
⊢ (M✶ ＼ C).IsCircuit K

Tactic:
rw [isCocircuit_def, dual_contract] at hK

Premises used: Matroid.dual_contract, Matroid.isCocircuit_def
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
K C : Set α
hK : (M✶ ＼ C).IsCircuit K
⊢ M.IsCocircuit K

Tactic:
hK.of_delete

Premises used: Matroid.IsCircuit.of_delete
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
K C : Set α
hK : (M✶ ＼ C).IsCircuit K
⊢ M.IsCocircuit K

Tactic:
exact hK.of_delete

Premises used: Matroid.IsCircuit.of_delete
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
K D : Set α
hK : M.IsCocircuit K
hD : D ⊂ K
rw : (M✶ ／ D).IsCircuit (K \ D)
⊢ (M ＼ D).IsCocircuit (K \ D)

Tactic:
rw [isCocircuit_def, dual_delete]

Premises used: Matroid.isCocircuit_def, Matroid.dual_delete
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
K D : Set α
hK : M.IsCocircuit K
hD : D ⊂ K
⊢ (M✶ ／ D).IsCircuit (K \ D)

Tactic:
hK.isCircuit.contract_isCircuit hD

Premises used: Matroid.IsCircuit.contract_isCircuit, Matroid.IsCocircuit.isCircuit
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
K D : Set α
hK : M.IsCocircuit K
hD : D ⊂ K
⊢ (M✶ ／ D).IsCircuit (K \ D)

Tactic:
exact hK.isCircuit.contract_isCircuit hD

Premises used: Matroid.IsCircuit.contract_isCircuit, Matroid.IsCocircuit.isCircuit
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
K X : Set α
hK : M.IsCocircuit K
hXK : X ⊆ K
hX : X.Nonempty
rw : (M✶ ／ (K \ X)).IsCircuit X
⊢ (M ＼ (K \ X)).IsCocircuit X

Tactic:
rw [isCocircuit_def, dual_delete]

Premises used: Matroid.isCocircuit_def, Matroid.dual_delete
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
K X : Set α
hK : M.IsCocircuit K
hXK : X ⊆ K
hX : X.Nonempty
⊢ (M✶ ／ (K \ X)).IsCircuit X

Tactic:
hK.isCircuit.contract_diff_isCircuit hX hXK

Premises used: Matroid.IsCircuit.contract_diff_isCircuit, Matroid.IsCocircuit.isCircuit
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
K X : Set α
hK : M.IsCocircuit K
hXK : X ⊆ K
hX : X.Nonempty
⊢ (M✶ ／ (K \ X)).IsCircuit X

Tactic:
exact hK.isCircuit.contract_diff_isCircuit hX hXK

Premises used: Matroid.IsCircuit.contract_diff_isCircuit, Matroid.IsCocircuit.isCircuit
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
C D : Set α
rw : D ∩ (M ／ C).E = D \ C ∩ (M ／ C).E
rw₁ : D ∩ (M.E \ C) = D \ C ∩ (M.E \ C)
rw₂ : D ∩ (M.E ∩ Cᶜ) = D \ C ∩ (M.E ∩ Cᶜ)
rw₃ : D ∩ (M.E ∩ Cᶜ) = D ∩ Cᶜ ∩ (M.E ∩ Cᶜ)
rw₄ : D ∩ (M.E ∩ Cᶜ) = D ∩ M.E ∩ Cᶜ
rw₅ rw₆ : D ∩ (M.E ∩ Cᶜ) = D ∩ (M.E ∩ Cᶜ)
⊢ M ／ C ＼ D = M ／ C ＼ (D \ C)

Tactic:
rw [delete_eq_delete_iff, contract_ground, diff_eq, diff_eq, ← inter_inter_distrib_right,
    inter_assoc]

Premises used: Set.inter_inter_distrib_right, Matroid.contract_ground, Set.diff_eq, Matroid.delete_eq_delete_iff, Set.inter_assoc
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
R C : Set α
M : Matroid α
h : Disjoint C R
⊢ (M ／ C ↾ R).E = ((M ↾ (R ∪ C)) ／ C).E

Tactic:
simp [h.sdiff_eq_right]

Premises used: Disjoint.sdiff_eq_right
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
R C : Set α
M : Matroid α
h : Disjoint C R
refine : ∀ (I : Set α) (hI : I ⊆ R), (M ／ C ↾ R).Indep I ↔ ((M ↾ (R ∪ C)) ／ C).Indep I
⊢ M ／ C ↾ R = (M ↾ (R ∪ C)) ／ C

Tactic:
refine ext_indep (by simp [h.sdiff_eq_right]) fun I (hI : I ⊆ R) ↦ ?_

Premises used: Matroid.ext_indep
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
R C : Set α
M : Matroid α
h : Disjoint C R
I : Set α
hI : I ⊆ R
obtain : ∀ (J : Set α) (hJ : (M ↾ (R ∪ C)).IsBasis' J C), (M ／ C ↾ R).Indep I ↔ ((M ↾ (R ∪ C)) ／ C).Indep I
⊢ (M ／ C ↾ R).Indep I ↔ ((M ↾ (R ∪ C)) ／ C).Indep I

Tactic:
obtain ⟨J, hJ⟩ := (M ↾ (R ∪ C)).exists_isBasis' C

Premises used: Union.union, Matroid.restrict, Matroid.exists_isBasis'
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
R C : Set α
M : Matroid α
h : Disjoint C R
I : Set α
hI : I ⊆ R
J : Set α
hJ : (M ↾ (R ∪ C)).IsBasis' J C
⊢ M.IsBasis' J C

Tactic:
simpa [inter_eq_self_of_subset_left subset_union_right] using (isBasis'_restrict_iff.1 hJ).1

Premises used: Matroid.isBasis'_restrict_iff, Set.subset_union_right, And.left, Iff.mp, Set.inter_eq_self_of_subset_left
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
R C : Set α
M : Matroid α
h : Disjoint C R
I : Set α
hI : I ⊆ R
J : Set α
hJ : (M ↾ (R ∪ C)).IsBasis' J C
⊢ M.IsBasis' J C

Tactic:
have hJ' : M.IsBasis' J C := by
    simpa [inter_eq_self_of_subset_left subset_union_right] using (isBasis'_restrict_iff.1 hJ).1
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
R C : Set α
M : Matroid α
h : Disjoint C R
I : Set α
hI : I ⊆ R
J : Set α
hJ : (M ↾ (R ∪ C)).IsBasis' J C
hJ' : M.IsBasis' J C
rw : (M.Indep (I ∪ J) ∧ Disjoint C I) ∧ I ⊆ R ↔ (M.Indep (I ∪ J) ∧ I ∪ J ⊆ R ∪ C) ∧ Disjoint C I
⊢ (M ／ C ↾ R).Indep I ↔ ((M ↾ (R ∪ C)) ／ C).Indep I

Tactic:
rw [restrict_indep_iff, hJ.contract_indep_iff, hJ'.contract_indep_iff, restrict_indep_iff]

Premises used: Matroid.restrict_indep_iff, Matroid.IsBasis'.contract_indep_iff
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
R C : Set α
M : Matroid α
h : Disjoint C R
I : Set α
hI : I ⊆ R
J : Set α
hJ : (M ↾ (R ∪ C)).IsBasis' J C
hJ' : M.IsBasis' J C
⊢ J ⊆ C

Tactic:
have hJC := hJ'.subset
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
R C : Set α
M : Matroid α
h : Disjoint C R
I : Set α
hI : I ⊆ R
J : Set α
hJ : (M ↾ (R ∪ C)).IsBasis' J C
hJ' : M.IsBasis' J C
hJC : J ⊆ C
tauto_set tauto_set₁ tauto_set₂ tauto_set₃ :
  ∀ (h : ∀ (x : α), x ∈ C ∧ x ∈ R → Membership.mem (γ := Set α) ∅ x) (hI : ∀ x ∈ I, x ∈ R)
    (hJ : (M ↾ (R ∪ C)).IsBasis' J C) (hJ' : M.IsBasis' J C) (hJC : ∀ x ∈ J, x ∈ C),
    ((M.Indep (I ∪ J) ∧ ∀ (x : α), x ∈ C ∧ x ∈ I → Membership.mem (γ := Set α) ∅ x) ∧ ∀ x ∈ I, True) ↔
      (M.Indep (I ∪ J) ∧ ∀ (x : α), x ∈ I ∨ x ∈ J → x ∈ R ∨ x ∈ C) ∧
        ∀ (x : α), x ∈ C ∧ x ∈ I → Membership.mem (γ := Set α) ∅ x
⊢ (M.Indep (I ∪ J) ∧ Disjoint C I) ∧ I ⊆ R ↔ (M.Indep (I ∪ J) ∧ I ∪ J ⊆ R ∪ C) ∧ Disjoint C I

Tactic:
tauto_set
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
R C : Set α
M : Matroid α
hCR : C ⊆ R
rw : (M ↾ R) ／ C = (M ↾ (R \ C ∪ C)) ／ C
⊢ (M ↾ R) ／ C = M ／ C ↾ R \ C

Tactic:
rw [contract_restrict_eq_restrict_contract _ disjoint_sdiff_right]

Premises used: Set.disjoint_sdiff_right, Matroid.contract_restrict_eq_restrict_contract
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
R C : Set α
M : Matroid α
hCR : C ⊆ R
⊢ (M ↾ R) ／ C = (M ↾ (R \ C ∪ C)) ／ C

Tactic:
simp [union_eq_self_of_subset_right hCR]

Premises used: Set.union_eq_self_of_subset_right
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
D C : Set α
M : Matroid α
hCD : Disjoint C D
inr :
  ∀ (aux : ∀ {C : Set α} (hCD : Disjoint C D) (hCE : C ⊆ M.E), M ／ C ＼ D = M ＼ D ／ C) (hCE : ¬C ⊆ M.E),
    M ／ C ＼ D = M ＼ D ／ C
wlog : ∀ {C : Set α} (hCD : Disjoint C D) (hCE : C ⊆ M.E), M ／ C ＼ D = M ＼ D ／ C
⊢ M ／ C ＼ D = M ＼ D ／ C

Tactic:
wlog hCE : C ⊆ M.E generalizing C with aux

Premises used: Matroid.E
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
D C : Set α
M : Matroid α
hCD : Disjoint C D
aux : ∀ {C : Set α} (hCD : Disjoint C D) (hCE : C ⊆ M.E), M ／ C ＼ D = M ＼ D ／ C
hCE : ¬C ⊆ M.E
inr : M ／ (C ∩ M.E) ＼ D = M ＼ D ／ C
inr₁ : M ＼ D ／ (C ∩ M.E) = M ＼ D ／ C
inr₂ : C ∩ M.E ∩ (M ＼ D).E = C ∩ (M ＼ D).E
inr₃ : C ∩ (M.E ∩ (M ＼ D).E) = C ∩ (M ＼ D).E
inr₄ : C ∩ (M.E ∩ (M.E \ D)) = C ∩ (M.E \ D)
inr₅ inr₆ : C ∩ (M.E \ D) = C ∩ (M.E \ D)
⊢ M ／ C ＼ D = M ＼ D ／ C

Tactic:
rw [← contract_inter_ground_eq, aux (hCD.mono_left inter_subset_left) inter_subset_right,
      contract_eq_contract_iff, inter_assoc, delete_ground,
      inter_eq_self_of_subset_right diff_subset]

Premises used: Set.diff_subset, Set.inter_subset_left, Matroid.delete_ground, Disjoint.mono_left, Set.inter_eq_self_of_subset_right, Matroid.contract_inter_ground_eq, Matroid.contract_eq_contract_iff, Set.inter_assoc, Set.inter_subset_right
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
D C_1 : Set α
M : Matroid α
C : Set α
hCD : Disjoint C D
hCE : C ⊆ M.E
⊢ C ⊆ M.E \ D

Tactic:
simpa [hCE, subset_diff]

Premises used: Set.subset_diff
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
D C_1 : Set α
M : Matroid α
C : Set α
hCD : Disjoint C D
hCE : C ⊆ M.E
rw : M ／ C ↾ (M ／ C).E \ D = M ＼ D ／ C
rw₁ : M ／ C ↾ (M ／ C).E \ D = (M ↾ M.E \ D) ／ C
rw₂ : M ／ C ↾ (M.E \ C) \ D = (M ↾ M.E \ D) ／ C
rw₃ : M ／ C ↾ (M.E \ D) \ C = (M ↾ M.E \ D) ／ C
rw₄ rw₅ : M ／ C ↾ (M.E \ D) \ C = M ／ C ↾ (M.E \ D) \ C
⊢ M ／ C ＼ D = M ＼ D ／ C

Tactic:
rw [delete_eq_restrict, delete_eq_restrict, contract_ground, diff_diff_comm,
    restrict_contract_eq_contract_restrict _ (by simpa [hCE, subset_diff])]

Premises used: Matroid.contract_ground, Matroid.delete_eq_restrict, Set.diff_diff_comm, Matroid.restrict_contract_eq_contract_restrict
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
C D : Set α
rw : M ／ C ＼ (D \ C) = M ＼ (D \ C) ／ C
rw₁ rw₂ : M ＼ (D \ C) ／ C = M ＼ (D \ C) ／ C
⊢ M ／ C ＼ D = M ＼ (D \ C) ／ C

Tactic:
rw [contract_delete_diff, contract_delete_comm _ disjoint_sdiff_right]

Premises used: Matroid.contract_delete_diff, Set.disjoint_sdiff_right, Matroid.contract_delete_comm
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
D C : Set α
rw : C ∩ (M ＼ D).E = C \ D ∩ (M ＼ D).E
rw₁ : C ∩ (M.E \ D) = C \ D ∩ (M.E \ D)
rw₂ : C ∩ (M.E \ D) = (C ∩ M.E) \ D
rw₃ : C ∩ (M.E ∩ Dᶜ) = (C ∩ M.E) \ D
rw₄ : C ∩ (M.E ∩ Dᶜ) = C ∩ M.E ∩ Dᶜ
rw₅ rw₆ : C ∩ (M.E ∩ Dᶜ) = C ∩ (M.E ∩ Dᶜ)
⊢ M ＼ D ／ C = M ＼ D ／ (C \ D)

Tactic:
rw [contract_eq_contract_iff, delete_ground, ← diff_inter_distrib_right, diff_eq, diff_eq,
    inter_assoc]

Premises used: Set.diff_eq, Matroid.delete_ground, Matroid.contract_eq_contract_iff, Set.diff_inter_distrib_right, Set.inter_assoc
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
D C : Set α
rw : M ＼ D ／ (C \ D) = M ／ (C \ D) ＼ D
rw₁ rw₂ : M ／ (C \ D) ＼ D = M ／ (C \ D) ＼ D
⊢ M ＼ D ／ C = M ／ (C \ D) ＼ D

Tactic:
rw [delete_contract_eq_diff, ← contract_delete_comm _ disjoint_sdiff_left]

Premises used: Matroid.delete_contract_eq_diff, Set.disjoint_sdiff_left, Matroid.contract_delete_comm
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
C D C' : Set α
rw : M ／ C ＼ D ／ (C' \ D) = M ／ (C ∪ C' \ D) ＼ D
rw₁ : M ／ C ／ (C' \ D) ＼ D = M ／ (C ∪ C' \ D) ＼ D
rw₂ rw₃ : M ／ (C ∪ C' \ D) ＼ D = M ／ (C ∪ C' \ D) ＼ D
⊢ M ／ C ＼ D ／ C' = M ／ (C ∪ C' \ D) ＼ D

Tactic:
rw [delete_contract_eq_diff, ← contract_delete_comm _ disjoint_sdiff_left, contract_contract]

Premises used: Matroid.delete_contract_eq_diff, Set.disjoint_sdiff_left, Matroid.contract_delete_comm, Matroid.contract_contract
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
C D C' : Set α
h : Disjoint C' D
rw : M ／ (C ∪ C' \ D) ＼ D = M ／ (C ∪ C') ＼ D
rw₁ rw₂ : M ／ (C ∪ C') ＼ D = M ／ (C ∪ C') ＼ D
⊢ M ／ C ＼ D ／ C' = M ／ (C ∪ C') ＼ D

Tactic:
rw [contract_delete_contract', sdiff_eq_left.mpr h]

Premises used: Iff.mpr, Matroid.contract_delete_contract', sdiff_eq_left
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
C D C' D' : Set α
rw : M ／ (C ∪ C' \ D) ＼ D ＼ D' = M ／ (C ∪ C' \ D) ＼ (D ∪ D')
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_delete]

Premises used: Matroid.contract_delete_contract', Matroid.delete_delete
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
C D C' D' : Set α
h : Disjoint C' D
rw : M ／ (C ∪ C' \ D) ＼ (D ∪ D') = M ／ (C ∪ C') ＼ (D ∪ D')
rw₁ rw₂ : M ／ (C ∪ C') ＼ (D ∪ D') = M ／ (C ∪ C') ＼ (D ∪ D')
⊢ M ／ C ＼ D ／ C' ＼ D' = M ／ (C ∪ C') ＼ (D ∪ D')

Tactic:
rw [contract_delete_contract_delete', sdiff_eq_left.mpr h]

Premises used: Iff.mpr, sdiff_eq_left, Matroid.contract_delete_contract_delete'
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
D C D' : Set α
rw : M ／ (C \ D) ＼ D ＼ D' = M ／ (C \ D) ＼ (D ∪ D')
rw₁ rw₂ : M ／ (C \ D) ＼ (D ∪ D') = M ／ (C \ D) ＼ (D ∪ D')
⊢ M ＼ D ／ C ＼ D' = M ／ (C \ D) ＼ (D ∪ D')

Tactic:
rw [delete_contract_comm', delete_delete]

Premises used: Matroid.delete_contract_comm', Matroid.delete_delete
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
D C D' : Set α
h : Disjoint C D
rw : M ／ (C \ D) ＼ (D ∪ D') = M ／ C ＼ (D ∪ D')
rw₁ rw₂ : M ／ C ＼ (D ∪ D') = M ／ C ＼ (D ∪ D')
⊢ M ＼ D ／ C ＼ D' = M ／ C ＼ (D ∪ D')

Tactic:
rw [delete_contract_delete', sdiff_eq_left.mpr h]

Premises used: Iff.mpr, sdiff_eq_left, Matroid.delete_contract_delete'
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
Goal:
α : Type u_1
M : Matroid α
D : Set α
⊢ M ＼ D = M ↾ M.E \ D

Tactic:
rfl

Premises used: Matroid.delete, rfl
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
Goal:
α : Type u_1
M : Matroid α
D : Set α
⊢ M ↾ M.E \ D = M ＼ D

Tactic:
rfl

Premises used: Matroid.delete, rfl
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
Goal:
α : Type u_1
M : Matroid α
R : Set α
hR : R ⊆ M.E
rw : M ↾ M.E \ (M.E \ R) = M ↾ R
rw₁ rw₂ : M ↾ R = M ↾ R
⊢ M ＼ (M.E \ R) = M ↾ R

Tactic:
rw [← restrict_compl, diff_diff_cancel_left hR]

Premises used: Set.diff_diff_cancel_left, Matroid.restrict_compl
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
Goal:
α : Type u_1
M : Matroid α
D : Set α
⊢ M ＼ D ≤r M

Tactic:
restrict_isRestriction _ _ diff_subset

Premises used: Set.diff_subset, Matroid.restrict_isRestriction, Matroid.delete
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
Goal:
α : Type u_1
M N : Matroid α
hNM : N ≤r M
obtain : ∀ (R : Set α) (hR : R ⊆ M.E), M ↾ R = M ＼ (M.E \ (M ↾ R).E)
⊢ N = M ＼ (M.E \ N.E)

Tactic:
obtain ⟨R, hR, rfl⟩ := hNM

Premises used: rfl
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
Goal:
α : Type u_1
M : Matroid α
R : Set α
hR : R ⊆ M.E
rw : M ↾ R = M ↾ (M ↾ R).E
rw₁ rw₂ : M ↾ R = M ↾ R
⊢ M ↾ R = M ＼ (M.E \ (M ↾ R).E)

Tactic:
rw [delete_compl, restrict_ground_eq]

Premises used: Matroid.delete_compl, Matroid.restrict_ground_eq
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
Goal:
α : Type u_1
M : Matroid α
D : Set α
⊢ M ＼ D ≤r M

Tactic:
apply delete_isRestriction

Premises used: Matroid.delete_isRestriction
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
Goal:
α : Type u_1
M : Matroid α
D : Set α
⊢ (M ＼ D).E = M.E \ D

Tactic:
rfl

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

Tactic:
diff_subset

Premises used: Set.diff_subset
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
Goal:
α : Type u_1
M : Matroid α
D : Set α
rw : M ↾ M.E \ D = M ↔ Disjoint D M.E
rw₁ : M.E \ D = M.E ↔ Disjoint D M.E
rw₂ : Disjoint M.E D ↔ Disjoint D M.E
rw₃ rw₄ : Disjoint D M.E ↔ Disjoint D M.E
⊢ M ＼ D = M ↔ Disjoint D M.E

Tactic:
rw [← restrict_compl, restrict_eq_self_iff, sdiff_eq_left, disjoint_comm]

Premises used: Matroid.restrict_eq_self_iff, disjoint_comm, sdiff_eq_left, Matroid.restrict_compl
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
Goal:
α : Type u_1
M : Matroid α
e : α
he : e ∉ M.E
⊢ M ＼ {e} = M

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
Goal:
α : Type u_1
M : Matroid α
D₁ D₂ : Set α
hR : (M ↾ M.E \ D₁).E \ D₂ ⊆ M.E \ D₁
⊢ M ＼ D₁ ＼ D₂ = M ＼ (D₁ ∪ D₂)

Tactic:
rw [← restrict_compl, ← restrict_compl, ← restrict_compl, restrict_restrict_eq,
    restrict_ground_eq, diff_diff]

Premises used: Matroid.restrict_ground_eq, Set.diff_diff, Matroid.restrict_restrict_eq, Matroid.restrict_compl
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
Goal:
α : Type u_1
M : Matroid α
D₁ D₂ : Set α
⊢ (M ↾ M.E \ D₁).E \ D₂ ⊆ M.E \ D₁

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
Goal:
α : Type u_1
M : Matroid α
D₁ D₂ : Set α
rw : M ＼ (D₁ ∪ D₂) = M ＼ D₂ ＼ D₁
rw₁ : M ＼ (D₂ ∪ D₁) = M ＼ D₂ ＼ D₁
rw₂ rw₃ : M ＼ (D₂ ∪ D₁) = M ＼ (D₂ ∪ D₁)
⊢ M ＼ D₁ ＼ D₂ = M ＼ D₂ ＼ D₁

Tactic:
rw [delete_delete, union_comm, delete_delete]

Premises used: Set.union_comm, Matroid.delete_delete
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
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
rw₂ rw₃ : M ↾ M.E \ D = M ↾ M.E \ D
⊢ M ＼ (D ∩ M.E) = M ＼ D

Tactic:
rw [← restrict_compl, ← restrict_compl, diff_inter_self_eq_diff]

Premises used: Set.diff_inter_self_eq_diff, Matroid.restrict_compl
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
Goal:
α : Type u_1
M : Matroid α
D₁ D₂ : Set α
rw : M ＼ (D₁ ∩ M.E) = M ＼ (D₂ ∩ M.E) ↔ D₁ ∩ M.E = D₂ ∩ M.E
⊢ M ＼ D₁ = M ＼ D₂ ↔ D₁ ∩ M.E = D₂ ∩ M.E

Tactic:
rw [← delete_inter_ground_eq, ← M.delete_inter_ground_eq D₂]

Premises used: Matroid.delete_inter_ground_eq
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
Goal:
α : Type u_1
M : Matroid α
D₁ D₂ : Set α
h : D₁ ∩ M.E = D₂ ∩ M.E
rw rw₁ : M ＼ (D₂ ∩ M.E) = M ＼ (D₂ ∩ M.E)
⊢ M ＼ (D₁ ∩ M.E) = M ＼ (D₂ ∩ M.E)

Tactic:
rw [h]
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
Goal:
α : Type u_1
M : Matroid α
D₁ D₂ : Set α
refine : ∀ (h : M ＼ (D₁ ∩ M.E) = M ＼ (D₂ ∩ M.E)), D₁ ∩ M.E = D₂ ∩ M.E
⊢ M ＼ (D₁ ∩ M.E) = M ＼ (D₂ ∩ M.E) ↔ D₁ ∩ M.E = D₂ ∩ M.E

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ by rw [h]⟩
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
Goal:
α : Type u_1
M : Matroid α
D₁ D₂ : Set α
h : M ＼ (D₁ ∩ M.E) = M ＼ (D₂ ∩ M.E)
⊢ M.E \ (M ＼ (D₁ ∩ M.E)).E = M.E \ (M ＼ (D₂ ∩ M.E)).E

Tactic:
apply_fun (M.E \ Matroid.E ·) at h

Premises used: Matroid.E, SDiff.sdiff
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
Goal:
α : Type u_1
M : Matroid α
D₁ D₂ : Set α
h : M.E \ (M ＼ (D₁ ∩ M.E)).E = M.E \ (M ＼ (D₂ ∩ M.E)).E
⊢ D₁ ∩ M.E = D₂ ∩ M.E

Tactic:
simp_rw [delete_ground, diff_diff_cancel_left inter_subset_right] at h

Premises used: Matroid.delete_ground, Set.diff_diff_cancel_left, Set.inter_subset_right
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
Goal:
α : Type u_1
M : Matroid α
D₁ D₂ : Set α
h : D₁ ∩ M.E = D₂ ∩ M.E
⊢ D₁ ∩ M.E = D₂ ∩ M.E

Tactic:
assumption
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
Goal:
α : Type u_1
M : Matroid α
rw : Disjoint ∅ M.E
⊢ M ＼ ∅ = M

Tactic:
rw [delete_eq_self_iff]

Premises used: Matroid.delete_eq_self_iff
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
Goal:
α : Type u_1
M : Matroid α
⊢ Disjoint ∅ M.E

Tactic:
empty_disjoint _

Premises used: Set.empty_disjoint
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
Goal:
α : Type u_1
M : Matroid α
⊢ Disjoint ∅ M.E

Tactic:
exact empty_disjoint _

Premises used: Set.empty_disjoint
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
Goal:
α : Type u_1
M : Matroid α
D₁ D₂ : Set α
⊢ M ＼ D₁ ＼ D₂ = M ＼ D₁ ＼ (D₂ \ D₁)

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
Goal:
α : Type u_1
M N : Matroid α
X : Set α
h : N ≤r M
hX : Disjoint X N.E
obtain : ∀ (D : Set α) (hD : D ⊆ M.E) (h : M ＼ D ≤r M) (hX : Disjoint X (M ＼ D).E), M ＼ D ≤r M ＼ X
⊢ N ≤r M ＼ X

Tactic:
obtain ⟨D, hD, rfl⟩ := isRestriction_iff_exists_eq_delete.1 h

Premises used: Matroid.isRestriction_iff_exists_eq_delete, Iff.mp, rfl
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
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

Tactic:
isRestriction_iff_exists_eq_delete.2 ⟨D \ X, diff_subset_diff_left hD, ?_⟩

Premises used: Iff.mpr, Set.diff_subset_diff_left, SDiff.sdiff, And.intro, Matroid.isRestriction_iff_exists_eq_delete, Exists.intro
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
Goal:
α : Type u_1
M : Matroid α
X D : Set α
hD : D ⊆ M.E
h : M ＼ D ≤r M
hX : Disjoint X (M ＼ D).E
refine : M ＼ D = M ＼ X ＼ (D \ X)
⊢ M ＼ D ≤r M ＼ X

Tactic:
refine isRestriction_iff_exists_eq_delete.2 ⟨D \ X, diff_subset_diff_left hD, ?_⟩

Premises used: Iff.mpr, SDiff.sdiff, And.intro, Matroid.isRestriction_iff_exists_eq_delete, Exists.intro
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
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
rwa₄ : M ＼ D ＼ X = M ＼ D
rwa₅ rwa₆ rwa₇ rwa₈ : Disjoint X (M ＼ D).E
⊢ M ＼ D = M ＼ X ＼ (D \ X)

Tactic:
rwa [delete_delete, union_diff_self, union_comm, ← delete_delete, eq_comm,
    delete_eq_self_iff]

Premises used: Matroid.delete_eq_self_iff, Set.union_comm, eq_comm, Matroid.delete_delete, Set.union_diff_self
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
Goal:
α : Type u_1
M N : Matroid α
e : α
h : N ≤r M
he : e ∉ N.E
⊢ Disjoint {e} N.E

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
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
rw₄ rw₅ : M.Indep I ∧ Disjoint I D ↔ M.Indep I ∧ Disjoint I D
⊢ (M ＼ 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]

Premises used: and_iff_left_of_imp, Set.subset_diff, Matroid.Indep.subset_ground, and_assoc, Matroid.restrict_indep_iff, Matroid.restrict_compl
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
Goal:
α : Type u_1
M : Matroid α
e : α
I : Set α
⊢ (M ＼ {e}).Indep I ↔ M.Indep I ∧ e ∉ I

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
Goal:
α : Type u_1
M : Matroid α
I D : Set α
h : (M ＼ D).Indep I
⊢ M.Indep I

Tactic:
(delete_indep_iff.mp h).1

Premises used: And.left, Iff.mp, Matroid.delete_indep_iff
-- Module: Mathlib.Combinatorics.Matroid.Minor.Delete
Goal:
α : Type u_1
M : Matroid α
I D : Set α
h : M.Indep I
hID : Disjoint I D
⊢ (M ＼ D).Indep I

Tactic:
delete_indep_iff.mpr ⟨h, hID⟩

Premises used: Iff.mpr, And.intro, Matroid.delete_indep_iff