internlm/Lean-Github huggingface dataset:
Theorem: Matroid.singleton_circuit
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
⊢ M.Dep {e} → ∀ ⦃y : Set α⦄, M.Dep y → y = ∅ ∨ y = {e} → {e} = y
Tactic:
rintro _ _ hY (rfl | rfl)
Proof state after:
case inl
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
a✝ : M.Dep {e}
hY : M.Dep ∅
⊢ {e} = ∅

case inr
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
a✝ hY : M.Dep {e}
⊢ {e} = {e}
Theorem: Matroid.singleton_circuit
Proof state before:
case inr
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
a✝ hY : M.Dep {e}
⊢ {e} = {e}
Tactic:
rfl
Proof state after:
no goals
Theorem: Matroid.singleton_circuit
Proof state before:
case inl
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
a✝ : M.Dep {e}
hY : M.Dep ∅
⊢ {e} = ∅
Tactic:
simpa using hY.nonempty
Proof state after:
no goals
Theorem: Matroid.loop_iff_not_mem_base_forall
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
he : autoParam (e ∈ M.E) _auto✝
⊢ M.Loop e ↔ ∀ (B : Set α), M.Base B → e ∉ B
Tactic:
rw [← singleton_dep, ← not_indep_iff, not_iff_comm, not_forall]
Proof state after:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
he : autoParam (e ∈ M.E) _auto✝
⊢ (∃ x, ¬(M.Base x → e ∉ x)) ↔ M.Indep {e}
Theorem: Matroid.loop_iff_not_mem_base_forall
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
he : autoParam (e ∈ M.E) _auto✝
⊢ (∃ x, ¬(M.Base x → e ∉ x)) ↔ M.Indep {e}
Tactic:
simp_rw [_root_.not_imp, not_not, ← singleton_subset_iff, indep_iff]
Proof state after:
no goals
Theorem: Matroid.Loop.mem_flat
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F✝ C K : Set α
he : M.Loop e
F : Set α
hF : M.Flat F
⊢ e ∈ F
Tactic:
have := he.mem_cl F
Proof state after:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F✝ C K : Set α
he : M.Loop e
F : Set α
hF : M.Flat F
this : e ∈ M.cl F
⊢ e ∈ F
Theorem: Matroid.Loop.mem_flat
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F✝ C K : Set α
he : M.Loop e
F : Set α
hF : M.Flat F
this : e ∈ M.cl F
⊢ e ∈ F
Tactic:
rwa [hF.cl] at this
Proof state after:
no goals
Theorem: Matroid.Loop.eq_of_circuit_mem
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
he : M.Loop e
hC : M.Circuit C
h : e ∈ C
⊢ C = {e}
Tactic:
rw [he.circuit.eq_of_subset_circuit hC (singleton_subset_iff.mpr h)]
Proof state after:
no goals
Theorem: Matroid.basis_loops_iff
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
⊢ M.Basis I (M.cl ∅) ↔ I = ∅
Tactic:
refine ⟨fun h ↦ h.indep.eq_empty_of_subset_loops h.subset, ?_⟩
Proof state after:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
⊢ I = ∅ → M.Basis I (M.cl ∅)
Theorem: Matroid.basis_loops_iff
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
⊢ I = ∅ → M.Basis I (M.cl ∅)
Tactic:
rintro rfl
Proof state after:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' X Y Z F C K : Set α
⊢ M.Basis ∅ (M.cl ∅)
Theorem: Matroid.basis_loops_iff
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' X Y Z F C K : Set α
⊢ M.Basis ∅ (M.cl ∅)
Tactic:
exact M.empty_indep.basis_cl
Proof state after:
no goals
Theorem: Matroid.basis_iff_empty_of_subset_loops
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
hX : X ⊆ M.cl ∅
⊢ M.Basis I X ↔ I = ∅
Tactic:
refine ⟨fun h ↦ ?_, by rintro rfl; simpa⟩
Proof state after:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
hX : X ⊆ M.cl ∅
h : M.Basis I X
⊢ I = ∅
Theorem: Matroid.basis_iff_empty_of_subset_loops
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
hX : X ⊆ M.cl ∅
h : M.Basis I X
⊢ I = ∅
Tactic:
replace h := (cl_eq_loops_of_subset hX) ▸ h.basis_cl_right
Proof state after:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
hX : X ⊆ M.cl ∅
h : M.Basis I (M.cl ∅)
⊢ I = ∅
Theorem: Matroid.basis_iff_empty_of_subset_loops
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
hX : X ⊆ M.cl ∅
h : M.Basis I (M.cl ∅)
⊢ I = ∅
Tactic:
simpa using h
Proof state after:
no goals
Theorem: Matroid.basis_iff_empty_of_subset_loops
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
hX : X ⊆ M.cl ∅
⊢ I = ∅ → M.Basis I X
Tactic:
rintro rfl
Proof state after:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' X Y Z F C K : Set α
hX : X ⊆ M.cl ∅
⊢ M.Basis ∅ X
Theorem: Matroid.basis_iff_empty_of_subset_loops
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' X Y Z F C K : Set α
hX : X ⊆ M.cl ∅
⊢ M.Basis ∅ X
Tactic:
simpa
Proof state after:
no goals
Theorem: Matroid.loop_iff_cl_eq_cl_empty'
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
⊢ M.Loop e ↔ M.cl {e} = M.cl ∅ ∧ e ∈ M.E
Tactic:
rw [← singleton_dep, dep_iff, singleton_subset_iff, and_congr_left_iff]
Proof state after:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
⊢ e ∈ M.E → (¬M.Indep {e} ↔ M.cl {e} = M.cl ∅)
Theorem: Matroid.loop_iff_cl_eq_cl_empty'
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
⊢ e ∈ M.E → (¬M.Indep {e} ↔ M.cl {e} = M.cl ∅)
Tactic:
intro he
Proof state after:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
he : e ∈ M.E
⊢ ¬M.Indep {e} ↔ M.cl {e} = M.cl ∅
Theorem: Matroid.loop_iff_cl_eq_cl_empty'
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
he : e ∈ M.E
⊢ ¬M.Indep {e} ↔ M.cl {e} = M.cl ∅
Tactic:
rw [not_indep_iff, singleton_dep]
Proof state after:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
he : e ∈ M.E
⊢ M.Loop e ↔ M.cl {e} = M.cl ∅
Theorem: Matroid.loop_iff_cl_eq_cl_empty'
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
he : e ∈ M.E
⊢ M.Loop e ↔ M.cl {e} = M.cl ∅
Tactic:
exact ⟨fun h ↦ by rw [h.cl], fun h ↦ by rw [loop_iff_mem_cl_empty, ← h]; exact M.mem_cl_self e⟩
Proof state after:
no goals
Theorem: Matroid.loop_iff_cl_eq_cl_empty'
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
he : e ∈ M.E
h : M.Loop e
⊢ M.cl {e} = M.cl ∅
Tactic:
rw [h.cl]
Proof state after:
no goals
Theorem: Matroid.loop_iff_cl_eq_cl_empty'
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
he : e ∈ M.E
h : M.cl {e} = M.cl ∅
⊢ M.Loop e
Tactic:
rw [loop_iff_mem_cl_empty, ← h]
Proof state after:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
he : e ∈ M.E
h : M.cl {e} = M.cl ∅
⊢ e ∈ M.cl {e}
Theorem: Matroid.loop_iff_cl_eq_cl_empty'
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
he : e ∈ M.E
h : M.cl {e} = M.cl ∅
⊢ e ∈ M.cl {e}
Tactic:
exact M.mem_cl_self e
Proof state after:
no goals
Theorem: Matroid.loop_iff_cl_eq_cl_empty
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
he : autoParam (e ∈ M.E) _auto✝
⊢ M.Loop e ↔ M.cl {e} = M.cl ∅
Tactic:
rw [loop_iff_cl_eq_cl_empty', and_iff_left he]
Proof state after:
no goals
Theorem: Matroid.loop_iff_forall_mem_compl_base
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
⊢ M.Loop e ↔ ∀ (B : Set α), M.Base B → e ∈ M.E \ B
Tactic:
refine' ⟨fun h B hB ↦ mem_of_mem_of_subset h _, fun h ↦ _⟩
Proof state after:
case refine'_1
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B✝ L L' I X Y Z F C K : Set α
h : M.Loop e
B : Set α
hB : M.Base B
⊢ M.cl ∅ ⊆ M.E \ B

case refine'_2
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
h : ∀ (B : Set α), M.Base B → e ∈ M.E \ B
⊢ M.Loop e
Theorem: Matroid.loop_iff_forall_mem_compl_base
Proof state before:
case refine'_2
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
h : ∀ (B : Set α), M.Base B → e ∈ M.E \ B
⊢ M.Loop e
Tactic:
have he : e ∈ M.E := M.exists_base.elim (fun B hB ↦ (h B hB).1)
Proof state after:
case refine'_2
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
h : ∀ (B : Set α), M.Base B → e ∈ M.E \ B
he : e ∈ M.E
⊢ M.Loop e
Theorem: Matroid.loop_iff_forall_mem_compl_base
Proof state before:
case refine'_2
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
h : ∀ (B : Set α), M.Base B → e ∈ M.E \ B
he : e ∈ M.E
⊢ M.Loop e
Tactic:
rw [← singleton_dep, ← not_indep_iff]
Proof state after:
case refine'_2
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
h : ∀ (B : Set α), M.Base B → e ∈ M.E \ B
he : e ∈ M.E
⊢ ¬M.Indep {e}
Theorem: Matroid.loop_iff_forall_mem_compl_base
Proof state before:
case refine'_2
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
h : ∀ (B : Set α), M.Base B → e ∈ M.E \ B
he : e ∈ M.E
⊢ ¬M.Indep {e}
Tactic:
intro hei
Proof state after:
case refine'_2
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
h : ∀ (B : Set α), M.Base B → e ∈ M.E \ B
he : e ∈ M.E
hei : M.Indep {e}
⊢ False
Theorem: Matroid.loop_iff_forall_mem_compl_base
Proof state before:
case refine'_2
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
h : ∀ (B : Set α), M.Base B → e ∈ M.E \ B
he : e ∈ M.E
hei : M.Indep {e}
⊢ False
Tactic:
obtain ⟨B, hB, heB⟩ := hei.exists_base_superset
Proof state after:
case refine'_2.intro.intro
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B✝ L L' I X Y Z F C K : Set α
h : ∀ (B : Set α), M.Base B → e ∈ M.E \ B
he : e ∈ M.E
hei : M.Indep {e}
B : Set α
hB : M.Base B
heB : {e} ⊆ B
⊢ False
Theorem: Matroid.loop_iff_forall_mem_compl_base
Proof state before:
case refine'_2.intro.intro
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B✝ L L' I X Y Z F C K : Set α
h : ∀ (B : Set α), M.Base B → e ∈ M.E \ B
he : e ∈ M.E
hei : M.Indep {e}
B : Set α
hB : M.Base B
heB : {e} ⊆ B
⊢ False
Tactic:
exact (h B hB).2 (singleton_subset_iff.mp heB)
Proof state after:
no goals
Theorem: Matroid.loop_iff_forall_mem_compl_base
Proof state before:
case refine'_1
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B✝ L L' I X Y Z F C K : Set α
h : M.Loop e
B : Set α
hB : M.Base B
⊢ M.cl ∅ ⊆ M.E \ B
Tactic:
rw [subset_diff, and_iff_right (cl_subset_ground _ _), disjoint_iff_inter_eq_empty,
  hB.indep.cl_inter_eq_self_of_subset (empty_subset B)]
Proof state after:
no goals
Theorem: Matroid.restrict_loop_iff
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K R : Set α
⊢ (M ↾ R).Loop e ↔ e ∈ R ∧ (M.Loop e ∨ e ∉ M.E)
Tactic:
rw [← singleton_dep, restrict_dep_iff, singleton_subset_iff, ← singleton_dep, and_comm,
  and_congr_right_iff, Dep, and_or_right, singleton_subset_iff, and_iff_left or_not,
  or_iff_left_of_imp (fun he hi ↦ he (singleton_subset_iff.1 hi.subset_ground))]
Proof state after:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K R : Set α
⊢ e ∈ R → (¬M.Indep {e} ↔ ¬M.Indep {e})
Theorem: Matroid.restrict_loop_iff
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K R : Set α
⊢ e ∈ R → (¬M.Indep {e} ↔ ¬M.Indep {e})
Tactic:
simp only [singleton_subset_iff, implies_true]
Proof state after:
no goals
Theorem: Matroid.restriction_loop_iff
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
hNM : N ≤r M
⊢ N.Loop e ↔ e ∈ N.E ∧ M.Loop e
Tactic:
obtain ⟨R, hR, rfl⟩ := hNM
Proof state after:
case intro.intro
α : Type u_1
β : Type u_2
M : Matroid α
e f : α
B L L' I X Y Z F C K R : Set α
hR : R ⊆ M.E
⊢ (M ↾ R).Loop e ↔ e ∈ (M ↾ R).E ∧ M.Loop e
Theorem: Matroid.restriction_loop_iff
Proof state before:
case intro.intro
α : Type u_1
β : Type u_2
M : Matroid α
e f : α
B L L' I X Y Z F C K R : Set α
hR : R ⊆ M.E
⊢ (M ↾ R).Loop e ↔ e ∈ (M ↾ R).E ∧ M.Loop e
Tactic:
simp only [restrict_loop_iff, restrict_ground_eq, and_congr_right_iff, or_iff_left_iff_imp]
Proof state after:
case intro.intro
α : Type u_1
β : Type u_2
M : Matroid α
e f : α
B L L' I X Y Z F C K R : Set α
hR : R ⊆ M.E
⊢ e ∈ R → e ∉ M.E → M.Loop e
Theorem: Matroid.restriction_loop_iff
Proof state before:
case intro.intro
α : Type u_1
β : Type u_2
M : Matroid α
e f : α
B L L' I X Y Z F C K R : Set α
hR : R ⊆ M.E
⊢ e ∈ R → e ∉ M.E → M.Loop e
Tactic:
exact fun heR heE ↦ (heE (hR heR)).elim
Proof state after:
no goals
Theorem: Matroid.comap_loop_iff
Proof state before:
α : Type u_1
β : Type u_2
M✝ N : Matroid α
e f✝ : α
B L L' I X Y Z F C K : Set α
M : Matroid β
f : α → β
⊢ (M.comap f).Loop e ↔ M.Loop (f e)
Tactic:
rw [← singleton_dep, comap_dep_iff]
Proof state after:
α : Type u_1
β : Type u_2
M✝ N : Matroid α
e f✝ : α
B L L' I X Y Z F C K : Set α
M : Matroid β
f : α → β
⊢ M.Dep (f '' {e}) ∨ M.Indep (f '' {e}) ∧ ¬InjOn f {e} ↔ M.Loop (f e)
Theorem: Matroid.comap_loop_iff
Proof state before:
α : Type u_1
β : Type u_2
M✝ N : Matroid α
e f✝ : α
B L L' I X Y Z F C K : Set α
M : Matroid β
f : α → β
⊢ M.Dep (f '' {e}) ∨ M.Indep (f '' {e}) ∧ ¬InjOn f {e} ↔ M.Loop (f e)
Tactic:
simp
Proof state after:
no goals
Theorem: Matroid.loopyOn_loop_iff
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K E : Set α
⊢ (loopyOn E).Loop e ↔ e ∈ E
Tactic:
simp [Loop]
Proof state after:
no goals
Theorem: Matroid.cl_union_loops_eq
Proof state before:
α : Type u_1
β : Type u_2
M✝ N : Matroid α
e f : α
B L L' I X✝ Y Z F C K : Set α
M : Matroid α
X : Set α
⊢ M.cl (X ∪ M.cl ∅) = M.cl X
Tactic:
rw [cl_union_cl_right_eq, union_empty]
Proof state after:
no goals
Theorem: Matroid.cl_diff_loops_eq
Proof state before:
α : Type u_1
β : Type u_2
M✝ N : Matroid α
e f : α
B L L' I X✝ Y Z F C K : Set α
M : Matroid α
X : Set α
⊢ M.cl (X \ M.cl ∅) = M.cl X
Tactic:
rw [← M.cl_union_loops_eq (X \ M.cl ∅), diff_union_self, cl_union_cl_right_eq, union_empty]
Proof state after:
no goals
Theorem: Matroid.LoopEquiv.diff_eq_diff
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
h : M.LoopEquiv X Y
⊢ X \ M.cl ∅ = Y \ M.cl ∅
Tactic:
rw [subset_antisymm_iff, diff_subset_iff, union_diff_self, union_comm, ← h.union_eq_union,
  diff_subset_iff, union_diff_self, union_comm _ X, and_iff_right subset_union_left,
  h.union_eq_union]
Proof state after:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
h : M.LoopEquiv X Y
⊢ Y ⊆ Y ∪ M.cl ∅
Theorem: Matroid.LoopEquiv.diff_eq_diff
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
h : M.LoopEquiv X Y
⊢ Y ⊆ Y ∪ M.cl ∅
Tactic:
apply subset_union_left
Proof state after:
no goals
Theorem: Matroid.LoopEquiv.rfl
Proof state before:
α : Type u_1
β : Type u_2
M✝ N : Matroid α
e f : α
B L L' I X✝ Y Z F C K : Set α
M : Matroid α
X : Set α
⊢ M.LoopEquiv X X
Tactic:
rfl
Proof state after:
no goals
Theorem: Matroid.LoopEquiv.diff_subset_loops
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
h : M.LoopEquiv X Y
⊢ X \ Y ⊆ M.cl ∅
Tactic:
rw [diff_subset_iff, ← h.union_eq_union]
Proof state after:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
h : M.LoopEquiv X Y
⊢ X ⊆ X ∪ M.cl ∅
Theorem: Matroid.LoopEquiv.diff_subset_loops
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
h : M.LoopEquiv X Y
⊢ X ⊆ X ∪ M.cl ∅
Tactic:
exact subset_union_left
Proof state after:
no goals
Theorem: Matroid.LoopEquiv.symmDiff_subset_loops
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
⊢ M.LoopEquiv X Y ↔ X ∆ Y ⊆ M.cl ∅
Tactic:
rw [Set.symmDiff_def, union_subset_iff]
Proof state after:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
⊢ M.LoopEquiv X Y ↔ X \ Y ⊆ M.cl ∅ ∧ Y \ X ⊆ M.cl ∅
Theorem: Matroid.LoopEquiv.symmDiff_subset_loops
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
⊢ M.LoopEquiv X Y ↔ X \ Y ⊆ M.cl ∅ ∧ Y \ X ⊆ M.cl ∅
Tactic:
refine ⟨fun h ↦ ⟨h.diff_subset_loops, h.symm.diff_subset_loops⟩, fun ⟨h1, h2⟩ ↦ ?_⟩
Proof state after:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
x✝ : X \ Y ⊆ M.cl ∅ ∧ Y \ X ⊆ M.cl ∅
h1 : X \ Y ⊆ M.cl ∅
h2 : Y \ X ⊆ M.cl ∅
⊢ M.LoopEquiv X Y
Theorem: Matroid.LoopEquiv.symmDiff_subset_loops
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
x✝ : X \ Y ⊆ M.cl ∅ ∧ Y \ X ⊆ M.cl ∅
h1 : X \ Y ⊆ M.cl ∅
h2 : Y \ X ⊆ M.cl ∅
⊢ M.LoopEquiv X Y
Tactic:
rw [diff_subset_iff] at h1 h2
Proof state after:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
x✝ : X \ Y ⊆ M.cl ∅ ∧ Y \ X ⊆ M.cl ∅
h1 : X ⊆ Y ∪ M.cl ∅
h2 : Y ⊆ X ∪ M.cl ∅
⊢ M.LoopEquiv X Y
Theorem: Matroid.LoopEquiv.symmDiff_subset_loops
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
x✝ : X \ Y ⊆ M.cl ∅ ∧ Y \ X ⊆ M.cl ∅
h1 : X ⊆ Y ∪ M.cl ∅
h2 : Y ⊆ X ∪ M.cl ∅
⊢ M.LoopEquiv X Y
Tactic:
rw [loopEquiv_iff_union_eq_union, subset_antisymm_iff, union_subset_iff, union_subset_iff]
Proof state after:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
x✝ : X \ Y ⊆ M.cl ∅ ∧ Y \ X ⊆ M.cl ∅
h1 : X ⊆ Y ∪ M.cl ∅
h2 : Y ⊆ X ∪ M.cl ∅
⊢ (X ⊆ Y ∪ M.cl ∅ ∧ M.cl ∅ ⊆ Y ∪ M.cl ∅) ∧ Y ⊆ X ∪ M.cl ∅ ∧ M.cl ∅ ⊆ X ∪ M.cl ∅
Theorem: Matroid.LoopEquiv.symmDiff_subset_loops
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
x✝ : X \ Y ⊆ M.cl ∅ ∧ Y \ X ⊆ M.cl ∅
h1 : X ⊆ Y ∪ M.cl ∅
h2 : Y ⊆ X ∪ M.cl ∅
⊢ (X ⊆ Y ∪ M.cl ∅ ∧ M.cl ∅ ⊆ Y ∪ M.cl ∅) ∧ Y ⊆ X ∪ M.cl ∅ ∧ M.cl ∅ ⊆ X ∪ M.cl ∅
Tactic:
exact ⟨⟨h1, subset_union_right⟩, h2, subset_union_right⟩
Proof state after:
no goals
Theorem: Matroid.loopEquiv_union
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X✝ Y Z F C K X : Set α
hL : L ⊆ M.cl ∅
⊢ M.LoopEquiv X (X ∪ L)
Tactic:
rw [loopEquiv_iff_union_eq_union, union_assoc, union_eq_self_of_subset_left hL]
Proof state after:
no goals
Theorem: Matroid.loopEquiv_diff
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X✝ Y Z F C K X : Set α
hL : L ⊆ M.cl ∅
⊢ M.LoopEquiv X (X \ L)
Tactic:
rw [LoopEquiv.comm]
Proof state after:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X✝ Y Z F C K X : Set α
hL : L ⊆ M.cl ∅
⊢ M.LoopEquiv (X \ L) X
Theorem: Matroid.loopEquiv_diff
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X✝ Y Z F C K X : Set α
hL : L ⊆ M.cl ∅
⊢ M.LoopEquiv (X \ L) X
Tactic:
refine (loopEquiv_union (X \ L) hL).trans ?_
Proof state after:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X✝ Y Z F C K X : Set α
hL : L ⊆ M.cl ∅
⊢ M.LoopEquiv (X \ L ∪ L) X
Theorem: Matroid.loopEquiv_diff
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X✝ Y Z F C K X : Set α
hL : L ⊆ M.cl ∅
⊢ M.LoopEquiv (X \ L ∪ L) X
Tactic:
rw [diff_union_self, LoopEquiv.comm]
Proof state after:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X✝ Y Z F C K X : Set α
hL : L ⊆ M.cl ∅
⊢ M.LoopEquiv X (X ∪ L)
Theorem: Matroid.loopEquiv_diff
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X✝ Y Z F C K X : Set α
hL : L ⊆ M.cl ∅
⊢ M.LoopEquiv X (X ∪ L)
Tactic:
exact loopEquiv_union X hL
Proof state after:
no goals
Theorem: Matroid.LoopEquiv.exists_diff_union_loops
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
h : M.LoopEquiv X Y
⊢ Y = (X ∪ Y \ X) \ (X \ Y)
Tactic:
aesop
Proof state after:
no goals
Theorem: Matroid.LoopEquiv.subset_union_loops
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
h : M.LoopEquiv X Y
⊢ Y ⊆ X ∪ M.cl ∅
Tactic:
rw [h.union_eq_union]
Proof state after:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
h : M.LoopEquiv X Y
⊢ Y ⊆ Y ∪ M.cl ∅
Theorem: Matroid.LoopEquiv.subset_union_loops
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
h : M.LoopEquiv X Y
⊢ Y ⊆ Y ∪ M.cl ∅
Tactic:
exact subset_union_left
Proof state after:
no goals
Theorem: Matroid.LoopEquiv.cl_eq_cl
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
h : M.LoopEquiv X Y
⊢ M.cl X = M.cl Y
Tactic:
rw [← cl_union_loops_eq, h.union_eq_union, cl_union_loops_eq]
Proof state after:
no goals
Theorem: Matroid.LoopEquiv.inter_eq_of_indep
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
h : M.LoopEquiv X Y
hI : M.Indep I
⊢ X ∩ I = Y ∩ I
Tactic:
rw [show X ∩ I = (X ∪ M.cl ∅) ∩ I
  by rw [union_inter_distrib_right, hI.disjoint_loops.symm.inter_eq, union_empty],
  h.union_eq_union, union_inter_distrib_right, hI.disjoint_loops.symm.inter_eq, union_empty]
Proof state after:
no goals
Theorem: Matroid.LoopEquiv.inter_eq_of_indep
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
h : M.LoopEquiv X Y
hI : M.Indep I
⊢ X ∩ I = (X ∪ M.cl ∅) ∩ I
Tactic:
rw [union_inter_distrib_right, hI.disjoint_loops.symm.inter_eq, union_empty]
Proof state after:
no goals
Theorem: Matroid.LoopEquiv.subset_iff_of_indep
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
h : M.LoopEquiv X Y
hI : M.Indep I
⊢ I ⊆ X ↔ I ⊆ Y
Tactic:
rw [← sdiff_eq_left.2 hI.disjoint_loops, diff_subset_iff, diff_subset_iff,
  union_comm, h.union_eq_union, union_comm]
Proof state after:
no goals
Theorem: Matroid.LoopEquiv.basis_iff
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
h : M.LoopEquiv X Y
⊢ M.Basis I X ↔ M.Basis I Y
Tactic:
rw [basis_iff_indep_subset_cl, basis_iff_indep_subset_cl, and_congr_right_iff]
Proof state after:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
h : M.LoopEquiv X Y
⊢ M.Indep I → (I ⊆ X ∧ X ⊆ M.cl I ↔ I ⊆ Y ∧ Y ⊆ M.cl I)
Theorem: Matroid.LoopEquiv.basis_iff
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
h : M.LoopEquiv X Y
⊢ M.Indep I → (I ⊆ X ∧ X ⊆ M.cl I ↔ I ⊆ Y ∧ Y ⊆ M.cl I)
Tactic:
intro hI
Proof state after:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
h : M.LoopEquiv X Y
hI : M.Indep I
⊢ I ⊆ X ∧ X ⊆ M.cl I ↔ I ⊆ Y ∧ Y ⊆ M.cl I
Theorem: Matroid.LoopEquiv.basis_iff
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
h : M.LoopEquiv X Y
hI : M.Indep I
⊢ I ⊆ X ∧ X ⊆ M.cl I ↔ I ⊆ Y ∧ Y ⊆ M.cl I
Tactic:
rw [h.subset_iff_of_indep hI, and_congr_right_iff, show M.cl I = M.cl I ∪ M.cl ∅ by simp,
  union_comm, ← diff_subset_iff,  h.diff_eq_diff, diff_subset_iff]
Proof state after:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
h : M.LoopEquiv X Y
hI : M.Indep I
⊢ I ⊆ Y → (Y ⊆ M.cl ∅ ∪ M.cl I ↔ Y ⊆ M.cl ∅ ∪ M.cl I)
Theorem: Matroid.LoopEquiv.basis_iff
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
h : M.LoopEquiv X Y
hI : M.Indep I
⊢ I ⊆ Y → (Y ⊆ M.cl ∅ ∪ M.cl I ↔ Y ⊆ M.cl ∅ ∪ M.cl I)
Tactic:
exact fun _ ↦ Iff.rfl
Proof state after:
no goals
Theorem: Matroid.LoopEquiv.basis_iff
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
h : M.LoopEquiv X Y
hI : M.Indep I
⊢ M.cl I = M.cl I ∪ M.cl ∅
Tactic:
simp
Proof state after:
no goals
Theorem: Matroid.loop_of_not_nonloop
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
he : autoParam (e ∈ M.E) _auto✝
h : ¬M.Nonloop e
⊢ M.Loop e
Tactic:
rwa [Nonloop, and_iff_left he, not_not] at h
Proof state after:
no goals