internlm/Lean-Github huggingface dataset:
Theorem: PartialEquiv.image_isImage_of_subset_source
Proof state before:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
h : s ⊆ e.source
⊢ e.IsImage s (↑e '' s)
Tactic:
apply PartialEquiv.IsImage.of_image_eq
Proof state after:
case h
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
h : s ⊆ e.source
⊢ ↑e '' (e.source ∩ s) = e.target ∩ ↑e '' s
Theorem: PartialEquiv.image_isImage_of_subset_source
Proof state before:
case h
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
h : s ⊆ e.source
⊢ ↑e '' (e.source ∩ s) = e.target ∩ ↑e '' s
Tactic:
rw [inter_eq_self_of_subset_right h, eq_comm, inter_eq_right]
Proof state after:
case h
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
h : s ⊆ e.source
⊢ ↑e '' s ⊆ e.target
Theorem: PartialEquiv.image_isImage_of_subset_source
Proof state before:
case h
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
h : s ⊆ e.source
⊢ ↑e '' s ⊆ e.target
Tactic:
exact image_subset_target e h
Proof state after:
no goals
Theorem: PartialEquiv.symm_image_isImage_of_subset_target
Proof state before:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set β
h : s ⊆ e.target
⊢ e.IsImage (↑e.symm '' s) s
Tactic:
simpa using e.symm.image_isImage_of_subset_source (s := s) (by simpa)
Proof state after:
no goals
Theorem: PartialEquiv.symm_image_isImage_of_subset_target
Proof state before:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set β
h : s ⊆ e.target
⊢ s ⊆ e.symm.source
Tactic:
simpa
Proof state after:
no goals
Theorem: PartialEquiv.symm_empty
Proof state before:
α : Type u_1
β : Type u_2
inst✝¹ : Nonempty α
inst✝ : Nonempty β
⊢ empty.symm = empty
Tactic:
ext <;> simp
Proof state after:
no goals
Theorem: Finite.exists_PartialEquiv_of_encard_eq
Proof state before:
α : Type u_1
β : Type u_2
inst✝¹ : Nonempty α
inst✝ : Nonempty β
s : Set α
t : Set β
hfin : s.Finite
h : s.encard = t.encard
⊢ ∃ e, e.source = s ∧ e.target = t
Tactic:
obtain ⟨f, hf⟩ := hfin.exists_bijOn_of_encard_eq h
Proof state after:
case intro
α : Type u_1
β : Type u_2
inst✝¹ : Nonempty α
inst✝ : Nonempty β
s : Set α
t : Set β
hfin : s.Finite
h : s.encard = t.encard
f : α → β
hf : BijOn f s t
⊢ ∃ e, e.source = s ∧ e.target = t
Theorem: Finite.exists_PartialEquiv_of_encard_eq
Proof state before:
case intro
α : Type u_1
β : Type u_2
inst✝¹ : Nonempty α
inst✝ : Nonempty β
s : Set α
t : Set β
hfin : s.Finite
h : s.encard = t.encard
f : α → β
hf : BijOn f s t
⊢ ∃ e, e.source = s ∧ e.target = t
Tactic:
exact ⟨hf.toPartialEquiv, rfl, hf.toPartialEquiv_target⟩
Proof state after:
no goals
Theorem: PartialEquiv.ofSetEquiv_apply_mem
Proof state before:
α : Type u_1
β : Type u_2
inst✝³ : Nonempty α
inst✝² : Nonempty β
s : Set α
t : Set β
inst✝¹ : DecidablePred fun x => x ∈ s
inst✝ : DecidablePred fun x => x ∈ t
e : ↑s ≃ ↑t
x : α
hx : x ∈ s
⊢ ↑(PartialEquiv.ofSetEquiv e) x = ↑(e ⟨x, hx⟩)
Tactic:
simp [hx]
Proof state after:
no goals
Theorem: PartialEquiv.insert_apply_mem
Proof state before:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
φ φ' : PartialEquiv α β
a : α
b : β
e : PartialEquiv α β
ha : a ∉ e.source
hb : b ∉ e.target
i : α
hi : i ∈ e.source
⊢ ↑(e.insert ha hb) i = ↑e i
Tactic:
rw [insert_apply, update_apply, if_neg]
Proof state after:
case hnc
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
φ φ' : PartialEquiv α β
a : α
b : β
e : PartialEquiv α β
ha : a ∉ e.source
hb : b ∉ e.target
i : α
hi : i ∈ e.source
⊢ ¬i = a
Theorem: PartialEquiv.insert_apply_mem
Proof state before:
case hnc
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
φ φ' : PartialEquiv α β
a : α
b : β
e : PartialEquiv α β
ha : a ∉ e.source
hb : b ∉ e.target
i : α
hi : i ∈ e.source
⊢ ¬i = a
Tactic:
exact fun h ↦ ha <| h ▸ hi
Proof state after:
no goals
Theorem: insert_symm
Proof state before:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
φ φ' : PartialEquiv α β
a : α
b : β
e : PartialEquiv α β
ha : a ∉ e.source
hb : b ∉ e.target
⊢ (e.insert ha hb).symm = e.symm.insert hb ha
Tactic:
ext <;> simp
Proof state after:
no goals
Theorem: PartialEquiv.insert_apply_symm_mem
Proof state before:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
φ φ' : PartialEquiv α β
a : α
b : β
e : PartialEquiv α β
ha : a ∉ e.source
hb : b ∉ e.target
j : β
hj : j ∈ e.target
⊢ ↑(e.insert ha hb).symm j = ↑e.symm j
Tactic:
rw [insert_symm, insert_apply_mem]
Proof state after:
case hi
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
φ φ' : PartialEquiv α β
a : α
b : β
e : PartialEquiv α β
ha : a ∉ e.source
hb : b ∉ e.target
j : β
hj : j ∈ e.target
⊢ j ∈ e.symm.source
Theorem: PartialEquiv.insert_apply_symm_mem
Proof state before:
case hi
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
φ φ' : PartialEquiv α β
a : α
b : β
e : PartialEquiv α β
ha : a ∉ e.source
hb : b ∉ e.target
j : β
hj : j ∈ e.target
⊢ j ∈ e.symm.source
Tactic:
exact hj
Proof state after:
no goals
Theorem: PartialEquiv.target_subset
Proof state before:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
φ φ' : PartialEquiv α β
a : α
b : β
h : φ ≤ φ'
⊢ φ.target ⊆ φ'.target
Tactic:
rw [← φ.image_source_eq_target, ← φ'.image_source_eq_target]
Proof state after:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
φ φ' : PartialEquiv α β
a : α
b : β
h : φ ≤ φ'
⊢ ↑φ '' φ.source ⊆ ↑φ' '' φ'.source
Theorem: PartialEquiv.target_subset
Proof state before:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
φ φ' : PartialEquiv α β
a : α
b : β
h : φ ≤ φ'
⊢ ↑φ '' φ.source ⊆ ↑φ' '' φ'.source
Tactic:
rintro _ ⟨x,hx,rfl⟩
Proof state after:
case intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
φ φ' : PartialEquiv α β
a : α
b : β
h : φ ≤ φ'
x : α
hx : x ∈ φ.source
⊢ ↑φ x ∈ ↑φ' '' φ'.source
Theorem: PartialEquiv.target_subset
Proof state before:
case intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
φ φ' : PartialEquiv α β
a : α
b : β
h : φ ≤ φ'
x : α
hx : x ∈ φ.source
⊢ ↑φ x ∈ ↑φ' '' φ'.source
Tactic:
rw [← PartialEquiv.eq_of_mem_source h hx]
Proof state after:
case intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
φ φ' : PartialEquiv α β
a : α
b : β
h : φ ≤ φ'
x : α
hx : x ∈ φ.source
⊢ ↑φ' x ∈ ↑φ' '' φ'.source
Theorem: PartialEquiv.target_subset
Proof state before:
case intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
φ φ' : PartialEquiv α β
a : α
b : β
h : φ ≤ φ'
x : α
hx : x ∈ φ.source
⊢ ↑φ' x ∈ ↑φ' '' φ'.source
Tactic:
exact mem_image_of_mem _ (source_subset h hx)
Proof state after:
no goals
Theorem: PartialEquiv.symm_le_symm_of_le
Proof state before:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
φ φ' : PartialEquiv α β
a : α
b : β
h : φ ≤ φ'
⊢ φ.symm ≤ φ'.symm
Tactic:
refine ⟨target_subset h, fun {i} hi ↦ φ'.injOn ?_ ?_ ?_⟩
Proof state after:
case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
φ φ' : PartialEquiv α β
a : α
b : β
h : φ ≤ φ'
i : β
hi : i ∈ φ.symm.source
⊢ ↑φ'.symm i ∈ φ'.source

case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
φ φ' : PartialEquiv α β
a : α
b : β
h : φ ≤ φ'
i : β
hi : i ∈ φ.symm.source
⊢ ↑φ.symm i ∈ φ'.source

case refine_3
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
φ φ' : PartialEquiv α β
a : α
b : β
h : φ ≤ φ'
i : β
hi : i ∈ φ.symm.source
⊢ ↑φ' (↑φ'.symm i) = ↑φ' (↑φ.symm i)
Theorem: PartialEquiv.symm_le_symm_of_le
Proof state before:
case refine_3
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
φ φ' : PartialEquiv α β
a : α
b : β
h : φ ≤ φ'
i : β
hi : i ∈ φ.symm.source
⊢ ↑φ' (↑φ'.symm i) = ↑φ' (↑φ.symm i)
Tactic:
rw [eq_comm, h.2 (φ.map_target hi), φ.right_inv hi, φ'.right_inv (target_subset h hi)]
Proof state after:
no goals
Theorem: PartialEquiv.symm_le_symm_of_le
Proof state before:
case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
φ φ' : PartialEquiv α β
a : α
b : β
h : φ ≤ φ'
i : β
hi : i ∈ φ.symm.source
⊢ ↑φ'.symm i ∈ φ'.source
Tactic:
exact φ'.map_target (target_subset h hi)
Proof state after:
no goals
Theorem: PartialEquiv.symm_le_symm_of_le
Proof state before:
case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
φ φ' : PartialEquiv α β
a : α
b : β
h : φ ≤ φ'
i : β
hi : i ∈ φ.symm.source
⊢ ↑φ.symm i ∈ φ'.source
Tactic:
exact h.1 <| φ.map_target hi
Proof state after:
no goals
Theorem: PartialEquiv.symm_le_symm_iff_le
Proof state before:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
φ φ' : PartialEquiv α β
a : α
b : β
h : φ ≤ φ'
⊢ φ.symm ≤ φ'.symm
Tactic:
simpa using symm_le_symm_of_le h
Proof state after:
no goals
Theorem: PartialEquiv.lt_insert
Proof state before:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
φ φ' : PartialEquiv α β
a : α
b : β
ha : a ∉ φ.source
hb : b ∉ φ.target
⊢ φ < φ.insert ha hb
Tactic:
refine ⟨⟨subset_insert _ _, fun hi ↦ φ.insert_apply_mem _ _ hi⟩, ?_⟩
Proof state after:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
φ φ' : PartialEquiv α β
a : α
b : β
ha : a ∉ φ.source
hb : b ∉ φ.target
⊢ ¬((φ.insert ha hb).source ⊆ φ.source ∧ ∀ {i : α}, i ∈ (φ.insert ha hb).source → ↑φ i = ↑(φ.insert ha hb) i)
Theorem: PartialEquiv.lt_insert
Proof state before:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
φ φ' : PartialEquiv α β
a : α
b : β
ha : a ∉ φ.source
hb : b ∉ φ.target
⊢ ¬((φ.insert ha hb).source ⊆ φ.source ∧ ∀ {i : α}, i ∈ (φ.insert ha hb).source → ↑φ i = ↑(φ.insert ha hb) i)
Tactic:
simp only [insert_source, not_and]
Proof state after:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
φ φ' : PartialEquiv α β
a : α
b : β
ha : a ∉ φ.source
hb : b ∉ φ.target
⊢ insert a φ.source ⊆ φ.source → ¬∀ {i : α}, i ∈ insert a φ.source → ↑φ i = ↑(φ.insert ha hb) i
Theorem: PartialEquiv.lt_insert
Proof state before:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
φ φ' : PartialEquiv α β
a : α
b : β
ha : a ∉ φ.source
hb : b ∉ φ.target
⊢ insert a φ.source ⊆ φ.source → ¬∀ {i : α}, i ∈ insert a φ.source → ↑φ i = ↑(φ.insert ha hb) i
Tactic:
exact fun h ↦ (ha <| h (Or.inl rfl)).elim
Proof state after:
no goals
Theorem: Matroid.uniqueBaseOn_finiteRk
Proof state before:
α : Type u_1
E I : Set α
hI : I.Finite
⊢ (uniqueBaseOn I E).FiniteRk
Tactic:
rw [← uniqueBaseOn_inter_ground_eq]
Proof state after:
α : Type u_1
E I : Set α
hI : I.Finite
⊢ (uniqueBaseOn (I ∩ E) E).FiniteRk
Theorem: Matroid.uniqueBaseOn_finiteRk
Proof state before:
α : Type u_1
E I : Set α
hI : I.Finite
⊢ (uniqueBaseOn (I ∩ E) E).FiniteRk
Tactic:
refine ⟨I ∩ E, ?_⟩
Proof state after:
α : Type u_1
E I : Set α
hI : I.Finite
⊢ (uniqueBaseOn (I ∩ E) E).Base (I ∩ E) ∧ (I ∩ E).Finite
Theorem: Matroid.uniqueBaseOn_finiteRk
Proof state before:
α : Type u_1
E I : Set α
hI : I.Finite
⊢ (uniqueBaseOn (I ∩ E) E).Base (I ∩ E) ∧ (I ∩ E).Finite
Tactic:
rw [uniqueBaseOn_base_iff inter_subset_right, and_iff_right rfl]
Proof state after:
α : Type u_1
E I : Set α
hI : I.Finite
⊢ (I ∩ E).Finite
Theorem: Matroid.uniqueBaseOn_finiteRk
Proof state before:
α : Type u_1
E I : Set α
hI : I.Finite
⊢ (I ∩ E).Finite
Tactic:
exact hI.subset inter_subset_left
Proof state after:
no goals
Theorem: Matroid.uniqueBaseOn_rkPos
Proof state before:
α : Type u_1
E I : Set α
hIE : I ⊆ E
hI : I.Nonempty
⊢ ¬(uniqueBaseOn I E).Base ∅
Tactic:
simpa [uniqueBaseOn_base_iff hIE] using Ne.symm <| hI.ne_empty
Proof state after:
no goals
Theorem: Matroid.freeOn_rkPos
Proof state before:
α : Type u_1
E I : Set α
hE : E.Nonempty
⊢ (freeOn E).RkPos
Tactic:
rw [← uniqueBaseOn_self]
Proof state after:
α : Type u_1
E I : Set α
hE : E.Nonempty
⊢ (uniqueBaseOn E E).RkPos
Theorem: Matroid.freeOn_rkPos
Proof state before:
α : Type u_1
E I : Set α
hE : E.Nonempty
⊢ (uniqueBaseOn E E).RkPos
Tactic:
exact uniqueBaseOn_rkPos Subset.rfl hE
Proof state after:
no goals
Theorem: Matroid.delete_compl
Proof state before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R✝ B X Y Z K D D₁ D₂ R : Set α
hR : autoParam (R ⊆ M.E) _auto✝
⊢ M ＼ (M.E \ R) = M ↾ R
Tactic:
rw [← restrict_compl, diff_diff_cancel_left hR]
Proof state after:
no goals
Theorem: Matroid.Restriction.exists_eq_delete
Proof state before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R✝ B X Y Z K D D₁ D₂ R : Set α
hNM : N ≤r M
⊢ N = M ＼ (M.E \ N.E)
Tactic:
obtain ⟨R, hR, rfl⟩ := hNM
Proof state after:
case intro.intro
α : Type u_1
M M' : Matroid α
e f : α
I J R✝¹ B X Y Z K D D₁ D₂ R✝ R : Set α
hR : R ⊆ M.E
⊢ M ↾ R = M ＼ (M.E \ (M ↾ R).E)
Theorem: Matroid.Restriction.exists_eq_delete
Proof state before:
case intro.intro
α : Type u_1
M M' : Matroid α
e f : α
I J R✝¹ B X Y Z K D D₁ D₂ R✝ R : Set α
hR : R ⊆ M.E
⊢ M ↾ R = M ＼ (M.E \ (M ↾ R).E)
Tactic:
rw [delete_compl, restrict_ground_eq]
Proof state after:
no goals
Theorem: Matroid.restriction_iff_exists_eq_delete
Proof state before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R✝ B X Y Z K D D₁ D₂ R : Set α
⊢ (∃ D ⊆ M.E, N = M ＼ D) → N ≤r M
Tactic:
rintro ⟨D, -, rfl⟩
Proof state after:
case intro.intro
α : Type u_1
M M' : Matroid α
e f : α
I J R✝ B X Y Z K D✝ D₁ D₂ R D : Set α
⊢ M ＼ D ≤r M
Theorem: Matroid.restriction_iff_exists_eq_delete
Proof state before:
case intro.intro
α : Type u_1
M M' : Matroid α
e f : α
I J R✝ B X Y Z K D✝ D₁ D₂ R D : Set α
⊢ M ＼ D ≤r M
Tactic:
apply delete_restriction
Proof state after:
no goals
Theorem: Matroid.deleteElem_eq_self
Proof state before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R✝ B X Y Z K D D₁ D₂ R : Set α
he : e ∉ M.E
⊢ M ＼ e = M
Tactic:
rwa [deleteElem, delete_eq_restrict, restrict_eq_self_iff, sdiff_eq_left,
  disjoint_singleton_right]
Proof state after:
no goals
Theorem: Matroid.delete_delete
Proof state before:
α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R✝ B X Y Z K D D₁✝ D₂✝ R : Set α
M : Matroid α
D₁ D₂ : Set α
⊢ M ＼ D₁ ＼ D₂ = M ＼ (D₁ ∪ D₂)
Tactic:
rw [← restrict_compl, ← restrict_compl, ← restrict_compl, restrict_restrict_eq,
  restrict_ground_eq, diff_diff]
Proof state after:
case hR
α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R✝ B X Y Z K D D₁✝ D₂✝ R : Set α
M : Matroid α
D₁ D₂ : Set α
⊢ (M ↾ M.E \ D₁).E \ D₂ ⊆ M.E \ D₁
Theorem: Matroid.delete_delete
Proof state before:
case hR
α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R✝ B X Y Z K D D₁✝ D₂✝ R : Set α
M : Matroid α
D₁ D₂ : Set α
⊢ (M ↾ M.E \ D₁).E \ D₂ ⊆ M.E \ D₁
Tactic:
simp [diff_subset]
Proof state after:
no goals
Theorem: Matroid.delete_comm
Proof state before:
α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R✝ B X Y Z K D D₁✝ D₂✝ R : Set α
M : Matroid α
D₁ D₂ : Set α
⊢ M ＼ D₁ ＼ D₂ = M ＼ D₂ ＼ D₁
Tactic:
rw [delete_delete, union_comm, delete_delete]
Proof state after:
no goals
Theorem: Matroid.delete_inter_ground_eq
Proof state before:
α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R✝ B X Y Z K D✝ D₁ D₂ R : Set α
M : Matroid α
D : Set α
⊢ M ＼ (D ∩ M.E) = M ＼ D
Tactic:
rw [← restrict_compl, ← restrict_compl, diff_inter_self_eq_diff]
Proof state after:
no goals
Theorem: Matroid.delete_eq_delete_iff
Proof state before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R✝ B X Y Z K D D₁ D₂ R : Set α
⊢ M ＼ D₁ = M ＼ D₂ ↔ D₁ ∩ M.E = D₂ ∩ M.E
Tactic:
rw [← delete_inter_ground_eq, ← M.delete_inter_ground_eq D₂]
Proof state after:
α : Type u_1
M M' N : Matroid α
e f : α
I J R✝ B X Y Z K D D₁ D₂ R : Set α
⊢ M ＼ (D₁ ∩ M.E) = M ＼ (D₂ ∩ M.E) ↔ D₁ ∩ M.E = D₂ ∩ M.E
Theorem: Matroid.delete_eq_delete_iff
Proof state before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R✝ B X Y Z K D D₁ D₂ R : Set α
⊢ M ＼ (D₁ ∩ M.E) = M ＼ (D₂ ∩ M.E) ↔ D₁ ∩ M.E = D₂ ∩ M.E
Tactic:
refine' ⟨fun h ↦ _, fun h ↦ by rw [h]⟩
Proof state after:
α : Type u_1
M M' N : Matroid α
e f : α
I J R✝ B X Y Z K D D₁ D₂ R : Set α
h : M ＼ (D₁ ∩ M.E) = M ＼ (D₂ ∩ M.E)
⊢ D₁ ∩ M.E = D₂ ∩ M.E
Theorem: Matroid.delete_eq_delete_iff
Proof state before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R✝ B X Y Z K D D₁ D₂ R : 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
Proof state after:
α : Type u_1
M M' N : Matroid α
e f : α
I J R✝ B X Y Z K D D₁ D₂ R : Set α
h : D₁ ∩ M.E = D₂ ∩ M.E
⊢ D₁ ∩ M.E = D₂ ∩ M.E
Theorem: Matroid.delete_eq_delete_iff
Proof state before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R✝ B X Y Z K D D₁ D₂ R : Set α
h : D₁ ∩ M.E = D₂ ∩ M.E
⊢ D₁ ∩ M.E = D₂ ∩ M.E
Tactic:
assumption
Proof state after:
no goals
Theorem: Matroid.delete_eq_delete_iff
Proof state before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R✝ B X Y Z K D D₁ D₂ R : Set α
h : D₁ ∩ M.E = D₂ ∩ M.E
⊢ M ＼ (D₁ ∩ M.E) = M ＼ (D₂ ∩ M.E)
Tactic:
rw [h]
Proof state after:
no goals
Theorem: Matroid.delete_eq_self_iff
Proof state before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R✝ B X Y Z K D D₁ D₂ R : Set α
⊢ M ＼ D = M ↔ Disjoint D M.E
Tactic:
rw [← restrict_compl, restrict_eq_self_iff, sdiff_eq_left, disjoint_comm]
Proof state after:
no goals
Theorem: Matroid.Restriction.restrict_delete_of_disjoint
Proof state before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R✝ B X Y Z K D D₁ D₂ R : Set α
h : N ≤r M
hX : Disjoint X N.E
⊢ N ≤r M ＼ X
Tactic:
obtain ⟨D, hD, rfl⟩ := restriction_iff_exists_eq_delete.1 h
Proof state after:
case intro.intro
α : Type u_1
M M' : Matroid α
e f : α
I J R✝ B X Y Z K D✝ D₁ D₂ R D : Set α
hD : D ⊆ M.E
h : M ＼ D ≤r M
hX : Disjoint X (M ＼ D).E
⊢ M ＼ D ≤r M ＼ X
Theorem: Matroid.Restriction.restrict_delete_of_disjoint
Proof state before:
case intro.intro
α : Type u_1
M M' : Matroid α
e f : α
I J R✝ B X Y Z K D✝ D₁ D₂ R D : Set α
hD : D ⊆ M.E
h : M ＼ D ≤r M
hX : Disjoint X (M ＼ D).E
⊢ M ＼ D ≤r M ＼ X
Tactic:
refine restriction_iff_exists_eq_delete.2 ⟨D \ X, diff_subset_diff_left hD, ?_⟩
Proof state after:
case intro.intro
α : Type u_1
M M' : Matroid α
e f : α
I J R✝ B X Y Z K D✝ D₁ D₂ R D : Set α
hD : D ⊆ M.E
h : M ＼ D ≤r M
hX : Disjoint X (M ＼ D).E
⊢ M ＼ D = M ＼ X ＼ (D \ X)
Theorem: Matroid.Restriction.restrict_delete_of_disjoint
Proof state before:
case intro.intro
α : Type u_1
M M' : Matroid α
e f : α
I J R✝ B X Y Z K D✝ D₁ D₂ R D : Set α
hD : D ⊆ M.E
h : M ＼ D ≤r M
hX : 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]
Proof state after:
no goals
Theorem: Matroid.Restriction.restriction_deleteElem
Proof state before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R✝ B X Y Z K D D₁ D₂ R : Set α
h : N ≤r M
he : e ∉ N.E
⊢ Disjoint {e} N.E
Tactic:
simpa
Proof state after:
no goals
Theorem: Matroid.delete_indep_iff
Proof state before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R✝ B X Y Z K D D₁ D₂ R : Set α
⊢ (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]
Proof state after:
no goals
Theorem: Matroid.deleteElem_indep_iff
Proof state before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R✝ B X Y Z K D D₁ D₂ R : Set α
⊢ (M ＼ e).Indep I ↔ M.Indep I ∧ e ∉ I
Tactic:
rw [deleteElem, delete_indep_iff, disjoint_singleton_right]
Proof state after:
no goals
Theorem: Matroid.delete_dep_iff
Proof state before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R✝ B X Y Z K D D₁ D₂ R : Set α
⊢ (M ＼ D).Dep X ↔ M.Dep X ∧ Disjoint X D
Tactic:
rw [dep_iff, dep_iff, delete_indep_iff, delete_ground, subset_diff]
Proof state after:
α : Type u_1
M M' N : Matroid α
e f : α
I J R✝ B X Y Z K D D₁ D₂ R : Set α
⊢ ¬(M.Indep X ∧ Disjoint X D) ∧ X ⊆ M.E ∧ Disjoint X D ↔ (¬M.Indep X ∧ X ⊆ M.E) ∧ Disjoint X D
Theorem: Matroid.delete_dep_iff
Proof state before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R✝ B X Y Z K D D₁ D₂ R : Set α
⊢ ¬(M.Indep X ∧ Disjoint X D) ∧ X ⊆ M.E ∧ Disjoint X D ↔ (¬M.Indep X ∧ X ⊆ M.E) ∧ Disjoint X D
Tactic:
tauto
Proof state after:
no goals
Theorem: Matroid.delete_base_iff
Proof state before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R✝ B X Y Z K D D₁ D₂ R : Set α
⊢ (M ＼ D).Base B ↔ M.Basis B (M.E \ D)
Tactic:
rw [← restrict_compl, base_restrict_iff]
Proof state after:
no goals
Theorem: Matroid.delete_basis_iff
Proof state before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R✝ B X Y Z K D D₁ D₂ R : Set α
⊢ (M ＼ D).Basis I X ↔ M.Basis I X ∧ Disjoint X D
Tactic:
rw [← restrict_compl, basis_restrict_iff, subset_diff, ← and_assoc,
  and_iff_left_of_imp Basis.subset_ground]
Proof state after:
no goals
Theorem: Matroid.delete_basis'_iff
Proof state before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R✝ B X Y Z K D D₁ D₂ R : Set α
⊢ (M ＼ D).Basis' I X ↔ M.Basis' I (X \ D)
Tactic:
rw [basis'_iff_basis_inter_ground, delete_basis_iff, delete_ground, diff_eq, inter_comm M.E,
  ← inter_assoc, ← diff_eq, ← basis'_iff_basis_inter_ground, and_iff_left_iff_imp,
  inter_comm, ← inter_diff_assoc]
Proof state after:
α : Type u_1
M M' N : Matroid α
e f : α
I J R✝ B X Y Z K D D₁ D₂ R : Set α
⊢ M.Basis' I (X \ D) → Disjoint ((M.E ∩ X) \ D) D
Theorem: Matroid.delete_basis'_iff
Proof state before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R✝ B X Y Z K D D₁ D₂ R : Set α
⊢ M.Basis' I (X \ D) → Disjoint ((M.E ∩ X) \ D) D
Tactic:
exact fun _ ↦ disjoint_sdiff_left
Proof state after:
no goals
Theorem: Matroid.Basis.to_delete
Proof state before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R✝ B X Y Z K D D₁ D₂ R : Set α
h : M.Basis I X
hX : Disjoint X D
⊢ (M ＼ D).Basis I X
Tactic:
rw [delete_basis_iff]
Proof state after:
α : Type u_1
M M' N : Matroid α
e f : α
I J R✝ B X Y Z K D D₁ D₂ R : Set α
h : M.Basis I X
hX : Disjoint X D
⊢ M.Basis I X ∧ Disjoint X D
Theorem: Matroid.Basis.to_delete
Proof state before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R✝ B X Y Z K D D₁ D₂ R : Set α
h : M.Basis I X
hX : Disjoint X D
⊢ M.Basis I X ∧ Disjoint X D
Tactic:
exact ⟨h, hX⟩
Proof state after:
no goals
Theorem: Matroid.delete_loop_iff
Proof state before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R✝ B X Y Z K D D₁ D₂ R : Set α
⊢ (M ＼ D).Loop e ↔ M.Loop e ∧ e ∉ D
Tactic:
rw [← singleton_dep, delete_dep_iff, disjoint_singleton_left, singleton_dep]
Proof state after:
no goals
Theorem: Matroid.delete_nonloop_iff
Proof state before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R✝ B X Y Z K D D₁ D₂ R : Set α
⊢ (M ＼ D).Nonloop e ↔ M.Nonloop e ∧ e ∉ D
Tactic:
rw [← indep_singleton, delete_indep_iff, disjoint_singleton_left, indep_singleton]
Proof state after:
no goals
Theorem: Matroid.delete_circuit_iff
Proof state before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R✝ B X Y Z K D D₁ D₂ R C : Set α
⊢ (M ＼ D).Circuit C ↔ M.Circuit C ∧ Disjoint C D
Tactic:
simp_rw [circuit_iff, delete_dep_iff, and_imp]
Proof state after:
α : Type u_1
M M' N : Matroid α
e f : α
I J R✝ B X Y Z K D D₁ D₂ R C : Set α
⊢ ((M.Dep C ∧ Disjoint C D) ∧ ∀ ⦃I : Set α⦄, M.Dep I → Disjoint I D → I ⊆ C → I = C) ↔
    (M.Dep C ∧ ∀ ⦃I : Set α⦄, M.Dep I → I ⊆ C → I = C) ∧ Disjoint C D
Theorem: Matroid.delete_circuit_iff
Proof state before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R✝ B X Y Z K D D₁ D₂ R C : Set α
⊢ ((M.Dep C ∧ Disjoint C D) ∧ ∀ ⦃I : Set α⦄, M.Dep I → Disjoint I D → I ⊆ C → I = C) ↔
    (M.Dep C ∧ ∀ ⦃I : Set α⦄, M.Dep I → I ⊆ C → I = C) ∧ Disjoint C D
Tactic:
rw [and_comm, ← and_assoc, and_congr_left_iff, and_comm, and_congr_right_iff]
Proof state after:
α : Type u_1
M M' N : Matroid α
e f : α
I J R✝ B X Y Z K D D₁ D₂ R C : Set α
⊢ Disjoint C D →
    M.Dep C → ((∀ ⦃I : Set α⦄, M.Dep I → Disjoint I D → I ⊆ C → I = C) ↔ ∀ ⦃I : Set α⦄, M.Dep I → I ⊆ C → I = C)
Theorem: Matroid.delete_circuit_iff
Proof state before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R✝ B X Y Z K D D₁ D₂ R C : Set α
⊢ Disjoint C D →
    M.Dep C → ((∀ ⦃I : Set α⦄, M.Dep I → Disjoint I D → I ⊆ C → I = C) ↔ ∀ ⦃I : Set α⦄, M.Dep I → I ⊆ C → I = C)
Tactic:
exact fun hdj _↦ ⟨fun h I hId hIC ↦ h hId (disjoint_of_subset_left hIC hdj) hIC,
  fun h I hI _ hIC ↦ h hI hIC⟩
Proof state after:
no goals
Theorem: Matroid.delete_cl_eq
Proof state before:
α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R✝ B X✝ Y Z K D✝ D₁ D₂ R : Set α
M : Matroid α
D X : Set α
⊢ (M ＼ D).cl X = M.cl (X \ D) \ D
Tactic:
rw [← restrict_compl, restrict_cl_eq', sdiff_sdiff_self, bot_eq_empty, union_empty,
  diff_eq, inter_comm M.E, ← inter_assoc X, ← diff_eq, cl_inter_ground,
  ← inter_assoc, ← diff_eq, inter_eq_left]
Proof state after:
α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R✝ B X✝ Y Z K D✝ D₁ D₂ R : Set α
M : Matroid α
D X : Set α
⊢ M.cl (X \ D) \ D ⊆ M.E