awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I : Set α
M : Matroid α
N : Matroid β
f_2 : α ≃ β
inst : M.Finitary
f : α ≃ β
⊢ (M.mapEquiv f).Finitary

Tactic:
inferInstanceAs (M.map f f.injective.injOn).Finitary

Premises used: _private.0.Matroid.instFinitaryMapEquiv._proof_1
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I : Set α
M : Matroid α
N : Matroid β
f_2 : α ≃ β
inst : M.RankFinite
f : α ≃ β
⊢ (M.mapEquiv f).RankFinite

Tactic:
inferInstanceAs (M.map f f.injective.injOn).RankFinite

Premises used: _private.0.Matroid.instRankFiniteMapEquiv._proof_1
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I : Set α
M : Matroid α
N : Matroid β
f_2 : α ≃ β
inst : M.RankPos
f : α ≃ β
⊢ (M.mapEquiv f).RankPos

Tactic:
inferInstanceAs (M.map f f.injective.injOn).RankPos

Premises used: _private.0.Matroid.instRankPosMapEquiv._proof_1
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
X : Set α
M : Matroid α
⊢ (M.restrictSubtype X).E = univ

Tactic:
simp [restrictSubtype]

Premises used: Matroid.restrictSubtype
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
X : Set α
M : Matroid α
I : Set (↑X : Type u_1)
⊢ (M.restrictSubtype X).Indep I ↔ M.Indep ↑I

Tactic:
simp [restrictSubtype, Subtype.val_injective.injOn]

Premises used: Subtype.val_injective, Function.Injective.injOn, Matroid.restrictSubtype
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
X I : Set α
M : Matroid α
hIX : I ⊆ X
rw : I ⊆ range (ι := (↑X : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ X))
⊢ (M.restrictSubtype X).Indep (X ↓∩ I) ↔ M.Indep I

Tactic:
rw [restrictSubtype_indep_iff, image_preimage_eq_iff.2]

Premises used: Iff.mpr, Matroid.restrictSubtype_indep_iff, Set.image_preimage_eq_iff
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
X I : Set α
M : Matroid α
hIX : I ⊆ X
⊢ I ⊆ range (ι := (↑X : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ X))

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
X I : Set α
M : Matroid α
⊢ (M.restrictSubtype X).Indep (X ↓∩ I) ↔ M.Indep (X ∩ I)

Tactic:
simp [restrictSubtype, Subtype.val_injective.injOn]

Premises used: Subtype.val_injective, Function.Injective.injOn, Matroid.restrictSubtype
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
M : Matroid α
Y : Set α
I X : Set (↑Y : Type u_1)
rw :
  M.IsBasis (↑I) (↑X ∩ M.E) ∧ ↑X ⊆ Y ↔
    M.IsBasis (Subtype.val (p := fun (x : α) ↦ x ∈ Y) '' I) (Subtype.val (p := fun (x : α) ↦ x ∈ Y) '' X ∩ M.E)
rw₁ : (M ↾ Y).IsBasis ↑I ↑X → I ⊆ X
⊢ (M.restrictSubtype Y).IsBasis I X ↔
    M.IsBasis' (Subtype.val (p := fun (x : α) ↦ x ∈ Y) '' I) (Subtype.val (p := fun (x : α) ↦ x ∈ Y) '' X)

Tactic:
rw [restrictSubtype, comap_isBasis_iff, and_iff_right Subtype.val_injective.injOn,
    and_iff_left_of_imp, isBasis_restrict_iff', isBasis'_iff_isBasis_inter_ground]

Premises used: and_iff_left_of_imp, Subtype.val_injective, Function.Injective.injOn, Matroid.isBasis'_iff_isBasis_inter_ground, and_iff_right, Matroid.comap_isBasis_iff, Matroid.isBasis_restrict_iff', Matroid.restrictSubtype
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
M : Matroid α
Y : Set α
I X : Set (↑Y : Type u_1)
⊢ M.IsBasis (↑I) (↑X ∩ M.E) ∧ ↑X ⊆ Y ↔
    M.IsBasis (Subtype.val (p := fun (x : α) ↦ x ∈ Y) '' I) (Subtype.val (p := fun (x : α) ↦ x ∈ Y) '' X ∩ M.E)

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
M : Matroid α
Y : Set α
I X : Set (↑Y : Type u_1)
⊢ (M ↾ Y).IsBasis ↑I ↑X → I ⊆ X

Tactic:
fun h ↦ (image_subset_image_iff Subtype.val_injective).1 h.subset

Premises used: Subtype.val_injective, Matroid.IsBasis.subset, Set.image_subset_image_iff, Iff.mp
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
M : Matroid α
Y : Set α
I X : Set (↑Y : Type u_1)
⊢ (M ↾ Y).IsBasis ↑I ↑X → I ⊆ X

Tactic:
exact fun h ↦ (image_subset_image_iff Subtype.val_injective).1 h.subset

Premises used: Subtype.val_injective, Set.image_subset_image_iff, Iff.mp
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
X : Set α
M : Matroid α
B : Set (↑X : Type u_1)
rw :
  (M ↾ X).IsBasis ↑B ↑(X ↓∩ (M ↾ X).E) ∧ InjOn (Subtype.val (p := fun (x : α) ↦ x ∈ X)) B ∧ B ⊆ X ↓∩ (M ↾ X).E ↔
    M.IsBasis' (Subtype.val (p := fun (x : α) ↦ x ∈ X) '' B) X
⊢ (M.restrictSubtype X).IsBase B ↔ M.IsBasis' (Subtype.val (p := fun (x : α) ↦ x ∈ X) '' B) X

Tactic:
rw [restrictSubtype, comap_isBase_iff]

Premises used: Matroid.comap_isBase_iff, Matroid.restrictSubtype
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
X : Set α
M : Matroid α
B : Set (↑X : Type u_1)
⊢ (M ↾ X).IsBasis ↑B ↑(X ↓∩ (M ↾ X).E) ∧ InjOn (Subtype.val (p := fun (x : α) ↦ x ∈ X)) B ∧ B ⊆ X ↓∩ (M ↾ X).E ↔
    M.IsBasis' (Subtype.val (p := fun (x : α) ↦ x ∈ X) '' B) X

Tactic:
simp [Subtype.val_injective.injOn, isBasis_restrict_iff',
    isBasis'_iff_isBasis_inter_ground]

Premises used: Subtype.val_injective, Function.Injective.injOn, Matroid.isBasis'_iff_isBasis_inter_ground, Matroid.isBasis_restrict_iff'
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
M : Matroid α
B : Set (↑M.E : Type u_1)
rw :
  M.IsBasis' (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' B) M.E ↔
    M.IsBase (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' B)
rw₁ :
  M.IsBasis (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' B) M.E ↔
    M.IsBase (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' B)
rw₂ rw₃ :
  M.IsBase (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' B) ↔ M.IsBase (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' B)
⊢ IsBase (M.restrictSubtype M.E) B ↔ M.IsBase (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' B)

Tactic:
rw [restrictSubtype_isBase_iff, isBasis'_iff_isBasis, isBasis_ground_iff]

Premises used: Matroid.isBasis_ground_iff, Matroid.isBasis'_iff_isBasis, Matroid.restrictSubtype_isBase_iff
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
M : Matroid α
I X : Set (↑M.E : Type u_1)
rw :
  M.IsBasis' (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' I) (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' X) ↔
    M.IsBasis (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' I) (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' X)
rw₁ rw₂ :
  M.IsBasis (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' I) (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' X) ↔
    M.IsBasis (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' I) (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' X)
⊢ IsBasis (M.restrictSubtype M.E) I X ↔
    M.IsBasis (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' I) (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' X)

Tactic:
rw [restrictSubtype_isBasis_iff, isBasis'_iff_isBasis]

Premises used: Matroid.restrictSubtype_isBasis_iff, Matroid.isBasis'_iff_isBasis
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
E : Set α
M N : Matroid α
hM : M.E = E
hN : N.E = E
h : M.restrictSubtype E = N.restrictSubtype E
⊢ N.E = M.E

Tactic:
subst hM
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
E : Set α
M N : Matroid α
hM : M.E = E
hN : N.E = E
h : M.restrictSubtype E = N.restrictSubtype E
hN₁ : N.E = M.E
⊢ Eq (α := Matroid (↑M.E : Type u_1)) (M.restrictSubtype M.E) (N.restrictSubtype M.E)

Tactic:
subst hM
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
M N : Matroid α
hN : N.E = M.E
h : Eq (α := Matroid (↑M.E : Type u_1)) (M.restrictSubtype M.E) (N.restrictSubtype M.E)
rw rw₁ : M.E = M.E
⊢ M.E = N.E

Tactic:
rw [hN]
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
M N : Matroid α
hN : N.E = M.E
h : Eq (α := Matroid (↑M.E : Type u_1)) (M.restrictSubtype M.E) (N.restrictSubtype M.E)
refine : ∀ (I : Set α) (hI : I ⊆ M.E), M.Indep I ↔ N.Indep I
⊢ M = N

Tactic:
refine ext_indep (by rw [hN]) (fun I hI ↦ ?_)

Premises used: Matroid.ext_indep
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
M N : Matroid α
hN : N.E = M.E
h : Eq (α := Matroid (↑M.E : Type u_1)) (M.restrictSubtype M.E) (N.restrictSubtype M.E)
I : Set α
hI : I ⊆ M.E
rwa : Indep (α := (↑M.E : Type u_1)) (M.restrictSubtype M.E) (M.E ↓∩ I) ↔ N.Indep I
rwa₁ : Indep (α := (↑M.E : Type u_1)) (N.restrictSubtype M.E) (M.E ↓∩ I) ↔ N.Indep I
rwa₂ : N.Indep I ↔ N.Indep I
rwa₃ : I ⊆ M.E
rwa₄ : N.Indep I ↔ N.Indep I
rwa₅ rwa₆ rwa₇ : I ⊆ M.E
⊢ M.Indep I ↔ N.Indep I

Tactic:
rwa [← restrictSubtype_indep_iff_of_subset hI, h, restrictSubtype_indep_iff_of_subset]

Premises used: Matroid.restrictSubtype_indep_iff_of_subset
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
M : Matroid α
rw : BijOn (α := (↑M.E : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ M.E)) (M.E ↓∩ (M ↾ M.E).E) (M ↾ M.E).E
⊢ Eq (α := Matroid (↑M.E : Type u_1)) (M.restrictSubtype M.E)✶ (M✶.restrictSubtype M.E)

Tactic:
rw [restrictSubtype, ← comapOn_preimage_eq, comapOn_dual_eq_of_bijOn, restrict_ground_eq_self,
    ← dual_ground, comapOn_preimage_eq, restrictSubtype, restrict_ground_eq_self]

Premises used: Matroid.restrict_ground_eq_self, Matroid.dual_ground, Matroid.comapOn_dual_eq_of_bijOn, Matroid.restrictSubtype, Matroid.comapOn_preimage_eq
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
M : Matroid α
⊢ MapsTo (α := (↑M.E : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ M.E)) (M.E ↓∩ (M ↾ M.E).E) (M ↾ M.E).E

Tactic:
simp [MapsTo]

Premises used: Set.MapsTo
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
M : Matroid α
⊢ SurjOn (α := (↑M.E : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ M.E)) (M.E ↓∩ (M ↾ M.E).E) (M ↾ M.E).E

Tactic:
simp [SurjOn]

Premises used: Set.SurjOn
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
M : Matroid α
⊢ BijOn (α := (↑M.E : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ M.E)) (M.E ↓∩ (M ↾ M.E).E) (M ↾ M.E).E

Tactic:
exact ⟨by simp [MapsTo], Subtype.val_injective.injOn, by simp [SurjOn]⟩
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
E : Set α
M : Matroid α
hM : M.E = E
rw : Eq (α := Matroid (↑M.E : Type u_1)) (M.restrictSubtype M.E)✶ (M✶.restrictSubtype M.E)
rw₁ rw₂ : Eq (α := Matroid (↑M.E : Type u_1)) (M✶.restrictSubtype M.E) (M✶.restrictSubtype M.E)
⊢ (M.restrictSubtype E)✶ = M✶.restrictSubtype E

Tactic:
rw [← hM, restrictSubtype_dual]

Premises used: Matroid.restrictSubtype_dual
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
M : Matroid α
X : Set α
⊢ (M.restrictSubtype X).map (Subtype.val (p := fun (x : α) ↦ x ∈ X)) ⋯ = M ↾ X

Tactic:
simp [restrictSubtype, map_comap]

Premises used: Matroid.map_comap, Matroid.restrictSubtype
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
M : Matroid α
⊢ map (α := (↑M.E : Type u_1)) (M.restrictSubtype M.E) (Subtype.val (p := fun (x : α) ↦ x ∈ M.E)) ⋯ = M

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
E_1 I_1 : Set α
M_1 : Matroid α
N : Matroid β
E X_1 I : Set α
M : Matroid α
inst : M.Finitary
X : Set α
⊢ Finitary (α := (↑X : Type u_1)) ((M ↾ X).comap (Subtype.val (p := fun (x : α) ↦ x ∈ X)))

Tactic:
infer_instance
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
E_1 I_1 : Set α
M_1 : Matroid α
N : Matroid β
E X_1 I : Set α
M : Matroid α
inst : M.RankFinite
X : Set α
⊢ RankFinite (α := (↑X : Type u_1)) ((M ↾ X).comap (Subtype.val (p := fun (x : α) ↦ x ∈ X)))

Tactic:
infer_instance
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
E_1 I_1 : Set α
M_1 : Matroid α
N : Matroid β
E X I : Set α
M : Matroid α
inst : M.Finite
⊢ Matroid.Finite (α := (↑M.E : Type u_1)) (M.restrictSubtype M.E)

Tactic:
have := M.ground_finite.to_subtype
  ⟨Finite.ground_finite⟩

Premises used: Set.Finite.to_subtype, Matroid.Finite.mk, Matroid.ground_finite, Matroid.Finite.ground_finite
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
E_1 I_1 : Set α
M_1 : Matroid α
N : Matroid β
E X I : Set α
M : Matroid α
inst : M.Nonempty
this : Nonempty.{u_1 + 1} (↑M.E : Type u_1)
⊢ Set.Nonempty (α := (↑M.E : Type u_1)) (Matroid.E (M.restrictSubtype M.E))

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
E_1 I_1 : Set α
M_1 : Matroid α
N : Matroid β
E X I : Set α
M : Matroid α
inst : M.RankPos
obtain :
  ∀ (B : Set (↑M.E : Type u_1)) (hB : IsBase (M.restrictSubtype M.E) B),
    RankPos (α := (↑M.E : Type u_1)) (M.restrictSubtype M.E)
⊢ RankPos (α := (↑M.E : Type u_1)) (M.restrictSubtype M.E)

Tactic:
obtain ⟨B, hB⟩ := (M.restrictSubtype M.E).exists_isBase

Premises used: Matroid.E, Matroid.exists_isBase, Matroid.restrictSubtype
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
E_1 I_1 : Set α
M_1 : Matroid α
N : Matroid β
E X I : Set α
M : Matroid α
inst : M.RankPos
B : Set (↑M.E : Type u_1)
hB : IsBase (M.restrictSubtype M.E) B
⊢ M.IsBase (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' B)

Tactic:
simpa using hB.map Subtype.val_injective.injOn

Premises used: Matroid.IsBase.map, Subtype.val_injective, Function.Injective.injOn
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
E_1 I_1 : Set α
M_1 : Matroid α
N : Matroid β
E X I : Set α
M : Matroid α
inst : M.RankPos
B : Set (↑M.E : Type u_1)
hB : IsBase (M.restrictSubtype M.E) B
⊢ M.IsBase (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' B)

Tactic:
have hB' : M.IsBase ↑B := by simpa using hB.map Subtype.val_injective.injOn
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
E_1 I_1 : Set α
M_1 : Matroid α
N : Matroid β
E X I : Set α
M : Matroid α
inst : M.RankPos
B : Set (↑M.E : Type u_1)
hB : IsBase (M.restrictSubtype M.E) B
hB' : M.IsBase (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' B)
⊢ B.Nonempty

Tactic:
simpa using hB'.nonempty

Premises used: Matroid.IsBase.nonempty
-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f : α → β
E_1 I_1 : Set α
M_1 : Matroid α
N : Matroid β
E X I : Set α
M : Matroid α
inst : M.RankPos
B : Set (↑M.E : Type u_1)
hB : IsBase (M.restrictSubtype M.E) B
hB' : M.IsBase (Subtype.val (p := fun (x : α) ↦ x ∈ M.E) '' B)
⊢ RankPos (α := (↑M.E : Type u_1)) (M.restrictSubtype M.E)

Tactic:
exact hB.rankPos_of_nonempty <| by simpa using hB'.nonempty

Premises used: Matroid.IsBase.rankPos_of_nonempty
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
C : Set α
⊢ (M ／ C).E = M.E \ C

Tactic:
rfl

Premises used: Maximal, rfl
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
X : Set α
⊢ (M✶ ＼ X)✶ = M ／ X

Tactic:
rfl

Premises used: Matroid.contract, rfl
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
X : Set α
rw : (M✶✶ ＼ X)✶ = M✶✶✶ ／ X
rw₁ : M✶ ／ X = M✶✶✶ ／ X
rw₂ rw₃ : M✶ ／ X = M✶ ／ X
⊢ (M ＼ X)✶ = M✶ ／ X

Tactic:
rw [← dual_dual M, dual_delete_dual, dual_dual]

Premises used: Matroid.dual_dual, Matroid.dual_delete_dual
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
X : Set α
rw : (M✶ ＼ X)✶✶ = M✶ ＼ X
rw₁ rw₂ : M✶ ＼ X = M✶ ＼ X
⊢ (M ／ X)✶ = M✶ ＼ X

Tactic:
rw [← dual_delete_dual, dual_dual]

Premises used: Matroid.dual_dual, Matroid.dual_delete_dual
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
X : Set α
⊢ (M✶ ／ X)✶ = M ＼ X

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
C₁ C₂ : Set α
⊢ M ／ C₁ ／ C₂ = M ／ (C₁ ∪ C₂)

Tactic:
simp [← dual_inj]

Premises used: Matroid.dual_inj
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
C₁ C₂ : Set α
⊢ M ／ C₁ ／ C₂ = M ／ C₂ ／ C₁

Tactic:
simp [union_comm]

Premises used: Set.union_comm
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
⊢ (M ／ X ＼ Y)✶ = M✶ ＼ X ／ Y

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
X Y : Set α
⊢ (M ＼ X ／ Y)✶ = M✶ ／ X ＼ Y

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
C : Set α
rw : (M✶ ＼ C)✶ = M ↔ Disjoint C M.E
rw₁ : (M✶ ＼ C)✶✶ = M✶ ↔ Disjoint C M.E
rw₂ : M✶ ＼ C = M✶ ↔ Disjoint C M.E
rw₃ : Disjoint C M✶.E ↔ Disjoint C M.E
rw₄ rw₅ : Disjoint C M.E ↔ Disjoint C M.E
⊢ M ／ C = M ↔ Disjoint C M.E

Tactic:
rw [← dual_delete_dual, ← dual_inj, dual_dual, delete_eq_self_iff, dual_ground]

Premises used: Matroid.delete_eq_self_iff, Matroid.dual_dual, Matroid.dual_delete_dual, Matroid.dual_ground, Matroid.dual_inj
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
e : α
he : e ∉ M.E
⊢ e ∉ M✶.E

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
e : α
he : e ∉ M.E
rw : (M✶ ＼ {e})✶ = M
rw₁ : M✶✶ = M
rw₂ rw₃ : M = M
⊢ M ／ {e} = M

Tactic:
rw [← dual_delete_dual, deleteElem_eq_self (by simpa), dual_dual]

Premises used: Matroid.deleteElem_eq_self, Matroid.dual_dual, Matroid.dual_delete_dual
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
rw : (M✶ ＼ ∅)✶ = M
rw₁ : M✶✶ = M
rw₂ rw₃ : M = M
⊢ M ／ ∅ = M

Tactic:
rw [← dual_delete_dual, delete_empty, dual_dual]

Premises used: Matroid.delete_empty, Matroid.dual_dual, Matroid.dual_delete_dual
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
C₁ C₂ : Set α
⊢ M ／ C₁ ／ C₂ = M ／ C₁ ／ (C₂ \ C₁)

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
C₁ C₂ : Set α
rw : (M✶ ＼ C₁)✶ = M ／ C₂ ↔ C₁ ∩ M.E = C₂ ∩ M.E
rw₁ : (M✶ ＼ C₁)✶ = (M✶ ＼ C₂)✶ ↔ C₁ ∩ M.E = C₂ ∩ M.E
rw₂ : M✶ ＼ C₁ = M✶ ＼ C₂ ↔ C₁ ∩ M.E = C₂ ∩ M.E
rw₃ : C₁ ∩ M✶.E = C₂ ∩ M✶.E ↔ C₁ ∩ M.E = C₂ ∩ M.E
rw₄ rw₅ : C₁ ∩ M.E = C₂ ∩ M.E ↔ C₁ ∩ M.E = C₂ ∩ M.E
⊢ M ／ C₁ = M ／ C₂ ↔ C₁ ∩ M.E = C₂ ∩ M.E

Tactic:
rw [← dual_delete_dual, ← dual_delete_dual, dual_inj, delete_eq_delete_iff, dual_ground]

Premises used: Matroid.dual_delete_dual, Matroid.dual_ground, Matroid.delete_eq_delete_iff, Matroid.dual_inj
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
C : Set α
rw : (M✶ ＼ (C ∩ M.E))✶ = M ／ C
rw₁ : (M✶ ＼ (C ∩ M✶.E))✶ = M ／ C
rw₂ : (M✶ ＼ C)✶ = M ／ C
rw₃ rw₄ : M ／ C = M ／ C
⊢ M ／ (C ∩ M.E) = M ／ C

Tactic:
rw [← dual_delete_dual, ← dual_ground, delete_inter_ground_eq, dual_delete_dual]

Premises used: Matroid.delete_inter_ground_eq, Matroid.dual_delete_dual, Matroid.dual_ground
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
C : Set α
⊢ (M ／ C).E ⊆ M.E

Tactic:
(M.contract_ground C).trans_subset diff_subset

Premises used: Set.diff_subset, Matroid.contract_ground, Eq.trans_subset
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
X C : Set α
rw : (M ／ C)✶.Indep X ↔ M.Coindep X ∧ Disjoint X C
rw₁ : (M✶ ＼ C).Indep X ↔ M.Coindep X ∧ Disjoint X C
rw₂ : M✶.Indep X ∧ Disjoint X C ↔ M.Coindep X ∧ Disjoint X C
rw₃ rw₄ : M.Coindep X ∧ Disjoint X C ↔ M.Coindep X ∧ Disjoint X C
⊢ (M ／ C).Coindep X ↔ M.Coindep X ∧ Disjoint X C

Tactic:
rw [coindep_def, dual_contract, delete_indep_iff, ← coindep_def]

Premises used: Matroid.dual_contract, Matroid.delete_indep_iff, Matroid.coindep_def
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
X C : Set α
hX : M.Coindep X
hXC : Disjoint X C
⊢ (M ／ C).Coindep X

Tactic:
coindep_contract_iff.2 ⟨hX, hXC⟩

Premises used: Iff.mpr, Matroid.coindep_contract_iff, And.intro
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
K C : Set α
rw : (M ／ C)✶.IsCircuit K ↔ M.IsCocircuit K ∧ Disjoint K C
rw₁ : (M✶ ＼ C).IsCircuit K ↔ M.IsCocircuit K ∧ Disjoint K C
rw₂ rw₃ : M✶.IsCircuit K ∧ Disjoint K C ↔ M.IsCocircuit K ∧ Disjoint K C
⊢ (M ／ C).IsCocircuit K ↔ M.IsCocircuit K ∧ Disjoint K C

Tactic:
rw [isCocircuit_def, dual_contract, delete_isCircuit_iff]

Premises used: Matroid.dual_contract, Matroid.isCocircuit_def, Matroid.delete_isCircuit_iff
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I B : Set α
hI : M.Indep I
rw : Disjoint B I → B ⊆ M.E → (M✶.IsBase (M.E \ (I ∪ B)) ↔ M✶.IsBase (M.E \ (I ∪ B)))
rw₁ : M✶.Spanning (M.E \ I)
⊢ (M ／ I).IsBase B ↔ M.IsBase (B ∪ I) ∧ Disjoint B I

Tactic:
rw [← dual_delete_dual, dual_isBase_iff', delete_ground, dual_ground, delete_isBase_iff,
    subset_diff, ← and_assoc, and_congr_left_iff, ← dual_dual M, dual_isBase_iff', dual_dual,
    dual_dual, union_comm, dual_ground, union_subset_iff, and_iff_right hI.subset_ground,
    and_congr_left_iff, ← isBase_restrict_iff, diff_diff, Spanning.isBase_restrict_iff,
    and_iff_left (diff_subset_diff_right subset_union_left)]

Premises used: Matroid.dual_isBase_iff', Set.union_subset_iff, and_iff_left, Set.subset_diff, Set.union_comm, and_iff_right, Matroid.delete_ground, Matroid.dual_dual, Set.subset_union_left, Matroid.dual_delete_dual, Matroid.Indep.subset_ground, Set.diff_diff, and_congr_left_iff, and_assoc, Matroid.Spanning.isBase_restrict_iff, Matroid.dual_ground, Matroid.isBase_restrict_iff, Set.diff_subset_diff_right, Matroid.delete_isBase_iff
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I B : Set α
hI : M.Indep I
⊢ Disjoint B I → B ⊆ M.E → (M✶.IsBase (M.E \ (I ∪ B)) ↔ M✶.IsBase (M.E \ (I ∪ B)))

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I B : Set α
hI : M.Indep I
rwa : M✶.Spanning (M✶.E \ I)
rwa₁ : M✶.Coindep I
rwa₂ rwa₃ rwa₄ rwa₅ : M.Indep I
⊢ M✶.Spanning (M.E \ I)

Tactic:
rwa [← dual_ground, ← coindep_iff_compl_spanning, dual_coindep_iff]

Premises used: Matroid.dual_coindep_iff, Matroid.dual_ground, Matroid.coindep_iff_compl_spanning
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
simp_rw :
  (∃ (B : Set α), (M.IsBase (B ∪ I) ∧ Disjoint B I) ∧ J ⊆ B) ↔ Disjoint J I ∧ ∃ (B : Set α), M.IsBase B ∧ J ⊆ B ∧ I ⊆ B
⊢ (M ／ I).Indep J ↔ Disjoint J I ∧ M.Indep (J ∪ I)

Tactic:
simp_rw [indep_iff, hI.contract_isBase_iff, union_subset_iff]

Premises used: Set.union_subset_iff, Matroid.indep_iff, Matroid.Indep.contract_isBase_iff
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
h : Disjoint J I ∧ ∃ (B : Set α), M.IsBase B ∧ J ⊆ B ∧ I ⊆ B
hdj : Disjoint J I
B : Set α
hB : M.IsBase B
hJB : J ⊆ B
hIB : I ⊆ B
⊢ M.IsBase (B \ I ∪ I)

Tactic:
simpa [union_eq_self_of_subset_right hIB]

Premises used: Set.union_eq_self_of_subset_right
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
⊢ (∃ (B : Set α), (M.IsBase (B ∪ I) ∧ Disjoint B I) ∧ J ⊆ B) ↔ Disjoint J I ∧ ∃ (B : Set α), M.IsBase B ∧ J ⊆ B ∧ I ⊆ B

Tactic:
exact ⟨fun ⟨B, ⟨hBI, hdj⟩, hJB⟩ ↦ ⟨disjoint_of_subset_left hJB hdj, _, hBI,
    hJB.trans subset_union_left, subset_union_right⟩,
    fun ⟨hdj, B, hB, hJB, hIB⟩ ↦ ⟨B \ I,⟨by simpa [union_eq_self_of_subset_right hIB],
      disjoint_sdiff_left⟩, subset_diff.2 ⟨hJB, hdj⟩ ⟩⟩
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
e : α
I : Set α
he : M.IsNonloop e
⊢ (M ／ {e}).Indep I ↔ e ∉ I ∧ M.Indep (insert e I)

Tactic:
simp [he.indep.contract_indep_iff]

Premises used: Matroid.Indep.contract_indep_iff, Matroid.IsNonloop.indep
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
rw : M.Indep (I ∪ J) ↔ Disjoint (J \ I) I ∧ M.Indep (J \ I ∪ I)
rw₁ : M.Indep (I ∪ J) ↔ M.Indep (J \ I ∪ I)
rw₂ : M.Indep (I ∪ J) ↔ M.Indep (J ∪ I)
rw₃ rw₄ : M.Indep (J ∪ I) ↔ M.Indep (J ∪ I)
⊢ M.Indep (I ∪ J) ↔ (M ／ I).Indep (J \ I)

Tactic:
rw [hI.contract_indep_iff, and_iff_right disjoint_sdiff_left, diff_union_self, union_comm]

Premises used: Set.diff_union_self, Set.union_comm, and_iff_right, Set.disjoint_sdiff_left, Matroid.Indep.contract_indep_iff
-- Module: Mathlib.Combinatorics.Matroid.Minor.Contract
Goal:
α : Type u_1
M : Matroid α
I J : Set α
hJ : M.Indep J
hIJ : I ⊆ J
rwa : M.Indep (I ∪ J)
rwa₁ rwa₂ rwa₃ rwa₄ : M.Indep J
⊢ (M ／ I).Indep (J \ I)

Tactic:
rwa [← (hJ.subset hIJ).union_indep_iff_contract_indep, union_eq_self_of_subset_left hIJ]

Premises used: Matroid.Indep.subset, Matroid.Indep.union_indep_iff_contract_indep, Set.union_eq_self_of_subset_left