internlm/Lean-Github huggingface dataset:
Theorem: Matroid.cl_diff_singleton_eq_cl
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
h : e ∈ M.cl (X \ {e})
⊢ M.cl (X \ {e}) = M.cl X
Tactic:
refine' (em (e ∈ X)).elim (fun h' ↦ _) (fun h' ↦ by rw [diff_singleton_eq_self h'])
Proof state after:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
h : e ∈ M.cl (X \ {e})
h' : e ∈ X
⊢ M.cl (X \ {e}) = M.cl X
Theorem: Matroid.cl_diff_singleton_eq_cl
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
h : e ∈ M.cl (X \ {e})
h' : e ∈ X
⊢ M.cl (X \ {e}) = M.cl X
Tactic:
convert M.cl_insert_cl_eq_cl_insert e (X \ {e}) using 1
Proof state after:
case h.e'_2
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
h : e ∈ M.cl (X \ {e})
h' : e ∈ X
⊢ M.cl (X \ {e}) = M.cl (insert e (M.cl (X \ {e})))

case h.e'_3
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
h : e ∈ M.cl (X \ {e})
h' : e ∈ X
⊢ M.cl X = M.cl (insert e (X \ {e}))
Theorem: Matroid.cl_diff_singleton_eq_cl
Proof state before:
case h.e'_3
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
h : e ∈ M.cl (X \ {e})
h' : e ∈ X
⊢ M.cl X = M.cl (insert e (X \ {e}))
Tactic:
rw [insert_diff_singleton, insert_eq_of_mem h']
Proof state after:
no goals
Theorem: Matroid.cl_diff_singleton_eq_cl
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
h : e ∈ M.cl (X \ {e})
h' : e ∉ X
⊢ M.cl (X \ {e}) = M.cl X
Tactic:
rw [diff_singleton_eq_self h']
Proof state after:
no goals
Theorem: Matroid.cl_diff_singleton_eq_cl
Proof state before:
case h.e'_2
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
h : e ∈ M.cl (X \ {e})
h' : e ∈ X
⊢ M.cl (X \ {e}) = M.cl (insert e (M.cl (X \ {e})))
Tactic:
rw [insert_eq_of_mem h, cl_cl]
Proof state after:
no goals
Theorem: Matroid.mem_cl_diff_singleton_iff_cl
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
he : e ∈ X
heE : autoParam (e ∈ M.E) _auto✝
h : M.cl (X \ {e}) = M.cl X
⊢ e ∈ M.cl (X \ {e})
Tactic:
rw [h]
Proof state after:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
he : e ∈ X
heE : autoParam (e ∈ M.E) _auto✝
h : M.cl (X \ {e}) = M.cl X
⊢ e ∈ M.cl X
Theorem: Matroid.mem_cl_diff_singleton_iff_cl
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
he : e ∈ X
heE : autoParam (e ∈ M.E) _auto✝
h : M.cl (X \ {e}) = M.cl X
⊢ e ∈ M.cl X
Tactic:
exact M.mem_cl_of_mem' he
Proof state after:
no goals
Theorem: Matroid.indep_iff_not_mem_cl_diff_forall
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
hI : autoParam (I ⊆ M.E) _auto✝
⊢ M.Indep I ↔ ∀ e ∈ I, e ∉ M.cl (I \ {e})
Tactic:
use fun h e heI he ↦ ((h.cl_inter_eq_self_of_subset diff_subset).subset ⟨he, heI⟩).2 rfl
Proof state after:
case mpr
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
hI : autoParam (I ⊆ M.E) _auto✝
⊢ (∀ e ∈ I, e ∉ M.cl (I \ {e})) → M.Indep I
Theorem: Matroid.indep_iff_not_mem_cl_diff_forall
Proof state before:
case mpr
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
hI : autoParam (I ⊆ M.E) _auto✝
⊢ (∀ e ∈ I, e ∉ M.cl (I \ {e})) → M.Indep I
Tactic:
intro h
Proof state after:
case mpr
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
hI : autoParam (I ⊆ M.E) _auto✝
h : ∀ e ∈ I, e ∉ M.cl (I \ {e})
⊢ M.Indep I
Theorem: Matroid.indep_iff_not_mem_cl_diff_forall
Proof state before:
case mpr
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
hI : autoParam (I ⊆ M.E) _auto✝
h : ∀ e ∈ I, e ∉ M.cl (I \ {e})
⊢ M.Indep I
Tactic:
obtain ⟨J, hJ⟩ := M.exists_basis I
Proof state after:
case mpr.intro
α : Type u_1
ι : Type u_2
M : Matroid α
F I J✝ X Y B C R : Set α
e f x y : α
hI : autoParam (I ⊆ M.E) _auto✝
h : ∀ e ∈ I, e ∉ M.cl (I \ {e})
J : Set α
hJ : M.Basis J I
⊢ M.Indep I
Theorem: Matroid.indep_iff_not_mem_cl_diff_forall
Proof state before:
case mpr.intro
α : Type u_1
ι : Type u_2
M : Matroid α
F I J✝ X Y B C R : Set α
e f x y : α
hI : autoParam (I ⊆ M.E) _auto✝
h : ∀ e ∈ I, e ∉ M.cl (I \ {e})
J : Set α
hJ : M.Basis J I
⊢ M.Indep I
Tactic:
convert hJ.indep
Proof state after:
case h.e'_3
α : Type u_1
ι : Type u_2
M : Matroid α
F I J✝ X Y B C R : Set α
e f x y : α
hI : autoParam (I ⊆ M.E) _auto✝
h : ∀ e ∈ I, e ∉ M.cl (I \ {e})
J : Set α
hJ : M.Basis J I
⊢ I = J
Theorem: Matroid.indep_iff_not_mem_cl_diff_forall
Proof state before:
case h.e'_3
α : Type u_1
ι : Type u_2
M : Matroid α
F I J✝ X Y B C R : Set α
e f x y : α
hI : autoParam (I ⊆ M.E) _auto✝
h : ∀ e ∈ I, e ∉ M.cl (I \ {e})
J : Set α
hJ : M.Basis J I
⊢ I = J
Tactic:
refine' hJ.subset.antisymm' (fun e he ↦ by_contra fun heJ ↦ h _ he _)
Proof state after:
case h.e'_3
α : Type u_1
ι : Type u_2
M : Matroid α
F I J✝ X Y B C R : Set α
e✝ f x y : α
hI : autoParam (I ⊆ M.E) _auto✝
h : ∀ e ∈ I, e ∉ M.cl (I \ {e})
J : Set α
hJ : M.Basis J I
e : α
he : e ∈ I
heJ : e ∉ J
⊢ e ∈ M.cl (I \ {e})
Theorem: Matroid.indep_iff_not_mem_cl_diff_forall
Proof state before:
case h.e'_3
α : Type u_1
ι : Type u_2
M : Matroid α
F I J✝ X Y B C R : Set α
e✝ f x y : α
hI : autoParam (I ⊆ M.E) _auto✝
h : ∀ e ∈ I, e ∉ M.cl (I \ {e})
J : Set α
hJ : M.Basis J I
e : α
he : e ∈ I
heJ : e ∉ J
⊢ e ∈ M.cl (I \ {e})
Tactic:
exact mem_of_mem_of_subset
  (hJ.subset_cl he) (M.cl_subset_cl (subset_diff_singleton hJ.subset heJ))
Proof state after:
no goals
Theorem: Matroid.indep_iff_cl_diff_ne_forall
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
⊢ M.Indep I ↔ ∀ e ∈ I, M.cl (I \ {e}) ≠ M.cl I
Tactic:
rw [indep_iff_not_mem_cl_diff_forall']
Proof state after:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
⊢ (I ⊆ M.E ∧ ∀ e ∈ I, e ∉ M.cl (I \ {e})) ↔ ∀ e ∈ I, M.cl (I \ {e}) ≠ M.cl I
Theorem: Matroid.indep_iff_cl_diff_ne_forall
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
⊢ (I ⊆ M.E ∧ ∀ e ∈ I, e ∉ M.cl (I \ {e})) ↔ ∀ e ∈ I, M.cl (I \ {e}) ≠ M.cl I
Tactic:
refine' ⟨fun ⟨hIE, h⟩ e heI h_eq ↦ h e heI (h_eq.symm.subset (M.mem_cl_of_mem heI)),
  fun h ↦ ⟨fun e heI ↦ by_contra fun heE ↦ h e heI _,fun e heI hin ↦ h e heI
    (by rw [cl_diff_singleton_eq_cl hin])⟩⟩
Proof state after:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e✝ f x y : α
h : ∀ e ∈ I, M.cl (I \ {e}) ≠ M.cl I
e : α
heI : e ∈ I
heE : e ∉ M.E
⊢ M.cl (I \ {e}) = M.cl I
Theorem: Matroid.indep_iff_cl_diff_ne_forall
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e✝ f x y : α
h : ∀ e ∈ I, M.cl (I \ {e}) ≠ M.cl I
e : α
heI : e ∈ I
heE : e ∉ M.E
⊢ M.cl (I \ {e}) = M.cl I
Tactic:
rw [← cl_inter_ground, inter_comm, inter_diff_distrib_left,
  inter_singleton_eq_empty.mpr heE, diff_empty, inter_comm, cl_inter_ground]
Proof state after:
no goals
Theorem: Matroid.indep_iff_cl_diff_ne_forall
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e✝ f x y : α
h : ∀ e ∈ I, M.cl (I \ {e}) ≠ M.cl I
e : α
heI : e ∈ I
hin : e ∈ M.cl (I \ {e})
⊢ M.cl (I \ {e}) = M.cl I
Tactic:
rw [cl_diff_singleton_eq_cl hin]
Proof state after:
no goals
Theorem: Matroid.indep_iff_cl_ssubset_ssubset_forall
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
hI : autoParam (I ⊆ M.E) _auto✝
⊢ M.Indep I ↔ ∀ J ⊂ I, M.cl J ⊂ M.cl I
Tactic:
rw [indep_iff_not_mem_cl_diff_forall]
Proof state after:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
hI : autoParam (I ⊆ M.E) _auto✝
⊢ (∀ e ∈ I, e ∉ M.cl (I \ {e})) ↔ ∀ J ⊂ I, M.cl J ⊂ M.cl I
Theorem: Matroid.indep_iff_cl_ssubset_ssubset_forall
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
hI : autoParam (I ⊆ M.E) _auto✝
⊢ (∀ e ∈ I, e ∉ M.cl (I \ {e})) ↔ ∀ J ⊂ I, M.cl J ⊂ M.cl I
Tactic:
refine' ⟨fun h J hJI ↦ (M.cl_subset_cl hJI.subset).ssubset_of_ne (fun h_eq ↦ _),
  fun h e heI hin ↦ _⟩
Proof state after:
case refine'_1
α : Type u_1
ι : Type u_2
M : Matroid α
F I J✝ X Y B C R : Set α
e f x y : α
hI : autoParam (I ⊆ M.E) _auto✝
h : ∀ e ∈ I, e ∉ M.cl (I \ {e})
J : Set α
hJI : J ⊂ I
h_eq : M.cl J = M.cl I
⊢ False

case refine'_2
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e✝ f x y : α
hI : autoParam (I ⊆ M.E) _auto✝
h : ∀ J ⊂ I, M.cl J ⊂ M.cl I
e : α
heI : e ∈ I
hin : e ∈ M.cl (I \ {e})
⊢ False
Theorem: Matroid.indep_iff_cl_ssubset_ssubset_forall
Proof state before:
case refine'_2
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e✝ f x y : α
hI : autoParam (I ⊆ M.E) _auto✝
h : ∀ J ⊂ I, M.cl J ⊂ M.cl I
e : α
heI : e ∈ I
hin : e ∈ M.cl (I \ {e})
⊢ False
Tactic:
refine' (h (I \ {e}) (diff_singleton_sSubset.2 heI)).ne _
Proof state after:
case refine'_2
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e✝ f x y : α
hI : autoParam (I ⊆ M.E) _auto✝
h : ∀ J ⊂ I, M.cl J ⊂ M.cl I
e : α
heI : e ∈ I
hin : e ∈ M.cl (I \ {e})
⊢ M.cl (I \ {e}) = M.cl I
Theorem: Matroid.indep_iff_cl_ssubset_ssubset_forall
Proof state before:
case refine'_2
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e✝ f x y : α
hI : autoParam (I ⊆ M.E) _auto✝
h : ∀ J ⊂ I, M.cl J ⊂ M.cl I
e : α
heI : e ∈ I
hin : e ∈ M.cl (I \ {e})
⊢ M.cl (I \ {e}) = M.cl I
Tactic:
rw [← cl_cl, ← insert_eq_of_mem hin, cl_insert_cl_eq_cl_insert, insert_diff_singleton,
  insert_eq_of_mem heI]
Proof state after:
no goals
Theorem: Matroid.indep_iff_cl_ssubset_ssubset_forall
Proof state before:
case refine'_1
α : Type u_1
ι : Type u_2
M : Matroid α
F I J✝ X Y B C R : Set α
e f x y : α
hI : autoParam (I ⊆ M.E) _auto✝
h : ∀ e ∈ I, e ∉ M.cl (I \ {e})
J : Set α
hJI : J ⊂ I
h_eq : M.cl J = M.cl I
⊢ False
Tactic:
obtain ⟨e,heJ,h'⟩ := ssubset_iff_insert.1 hJI
Proof state after:
case refine'_1.intro.intro
α : Type u_1
ι : Type u_2
M : Matroid α
F I J✝ X Y B C R : Set α
e✝ f x y : α
hI : autoParam (I ⊆ M.E) _auto✝
h : ∀ e ∈ I, e ∉ M.cl (I \ {e})
J : Set α
hJI : J ⊂ I
h_eq : M.cl J = M.cl I
e : α
heJ : e ∉ J
h' : insert e J ⊆ I
⊢ False
Theorem: Matroid.indep_iff_cl_ssubset_ssubset_forall
Proof state before:
case refine'_1.intro.intro
α : Type u_1
ι : Type u_2
M : Matroid α
F I J✝ X Y B C R : Set α
e✝ f x y : α
hI : autoParam (I ⊆ M.E) _auto✝
h : ∀ e ∈ I, e ∉ M.cl (I \ {e})
J : Set α
hJI : J ⊂ I
h_eq : M.cl J = M.cl I
e : α
heJ : e ∉ J
h' : insert e J ⊆ I
⊢ False
Tactic:
apply h e (h' (mem_insert _ _))
Proof state after:
case refine'_1.intro.intro
α : Type u_1
ι : Type u_2
M : Matroid α
F I J✝ X Y B C R : Set α
e✝ f x y : α
hI : autoParam (I ⊆ M.E) _auto✝
h : ∀ e ∈ I, e ∉ M.cl (I \ {e})
J : Set α
hJI : J ⊂ I
h_eq : M.cl J = M.cl I
e : α
heJ : e ∉ J
h' : insert e J ⊆ I
⊢ e ∈ M.cl (I \ {e})
Theorem: Matroid.indep_iff_cl_ssubset_ssubset_forall
Proof state before:
case refine'_1.intro.intro
α : Type u_1
ι : Type u_2
M : Matroid α
F I J✝ X Y B C R : Set α
e✝ f x y : α
hI : autoParam (I ⊆ M.E) _auto✝
h : ∀ e ∈ I, e ∉ M.cl (I \ {e})
J : Set α
hJI : J ⊂ I
h_eq : M.cl J = M.cl I
e : α
heJ : e ∉ J
h' : insert e J ⊆ I
⊢ e ∈ M.cl (I \ {e})
Tactic:
have heI := M.mem_cl_of_mem (h' (mem_insert e J))
Proof state after:
case refine'_1.intro.intro
α : Type u_1
ι : Type u_2
M : Matroid α
F I J✝ X Y B C R : Set α
e✝ f x y : α
hI : autoParam (I ⊆ M.E) _auto✝
h : ∀ e ∈ I, e ∉ M.cl (I \ {e})
J : Set α
hJI : J ⊂ I
h_eq : M.cl J = M.cl I
e : α
heJ : e ∉ J
h' : insert e J ⊆ I
heI : e ∈ M.cl I
⊢ e ∈ M.cl (I \ {e})
Theorem: Matroid.indep_iff_cl_ssubset_ssubset_forall
Proof state before:
case refine'_1.intro.intro
α : Type u_1
ι : Type u_2
M : Matroid α
F I J✝ X Y B C R : Set α
e✝ f x y : α
hI : autoParam (I ⊆ M.E) _auto✝
h : ∀ e ∈ I, e ∉ M.cl (I \ {e})
J : Set α
hJI : J ⊂ I
h_eq : M.cl J = M.cl I
e : α
heJ : e ∉ J
h' : insert e J ⊆ I
heI : e ∈ M.cl I
⊢ e ∈ M.cl (I \ {e})
Tactic:
rw [← h_eq] at heI
Proof state after:
case refine'_1.intro.intro
α : Type u_1
ι : Type u_2
M : Matroid α
F I J✝ X Y B C R : Set α
e✝ f x y : α
hI : autoParam (I ⊆ M.E) _auto✝
h : ∀ e ∈ I, e ∉ M.cl (I \ {e})
J : Set α
hJI : J ⊂ I
h_eq : M.cl J = M.cl I
e : α
heJ : e ∉ J
h' : insert e J ⊆ I
heI : e ∈ M.cl J
⊢ e ∈ M.cl (I \ {e})
Theorem: Matroid.indep_iff_cl_ssubset_ssubset_forall
Proof state before:
case refine'_1.intro.intro
α : Type u_1
ι : Type u_2
M : Matroid α
F I J✝ X Y B C R : Set α
e✝ f x y : α
hI : autoParam (I ⊆ M.E) _auto✝
h : ∀ e ∈ I, e ∉ M.cl (I \ {e})
J : Set α
hJI : J ⊂ I
h_eq : M.cl J = M.cl I
e : α
heJ : e ∉ J
h' : insert e J ⊆ I
heI : e ∈ M.cl J
⊢ e ∈ M.cl (I \ {e})
Tactic:
refine' mem_of_mem_of_subset heI (M.cl_subset_cl _)
Proof state after:
case refine'_1.intro.intro
α : Type u_1
ι : Type u_2
M : Matroid α
F I J✝ X Y B C R : Set α
e✝ f x y : α
hI : autoParam (I ⊆ M.E) _auto✝
h : ∀ e ∈ I, e ∉ M.cl (I \ {e})
J : Set α
hJI : J ⊂ I
h_eq : M.cl J = M.cl I
e : α
heJ : e ∉ J
h' : insert e J ⊆ I
heI : e ∈ M.cl J
⊢ J ⊆ I \ {e}
Theorem: Matroid.indep_iff_cl_ssubset_ssubset_forall
Proof state before:
case refine'_1.intro.intro
α : Type u_1
ι : Type u_2
M : Matroid α
F I J✝ X Y B C R : Set α
e✝ f x y : α
hI : autoParam (I ⊆ M.E) _auto✝
h : ∀ e ∈ I, e ∉ M.cl (I \ {e})
J : Set α
hJI : J ⊂ I
h_eq : M.cl J = M.cl I
e : α
heJ : e ∉ J
h' : insert e J ⊆ I
heI : e ∈ M.cl J
⊢ J ⊆ I \ {e}
Tactic:
rw [subset_diff, disjoint_singleton_right, and_iff_left heJ]
Proof state after:
case refine'_1.intro.intro
α : Type u_1
ι : Type u_2
M : Matroid α
F I J✝ X Y B C R : Set α
e✝ f x y : α
hI : autoParam (I ⊆ M.E) _auto✝
h : ∀ e ∈ I, e ∉ M.cl (I \ {e})
J : Set α
hJI : J ⊂ I
h_eq : M.cl J = M.cl I
e : α
heJ : e ∉ J
h' : insert e J ⊆ I
heI : e ∈ M.cl J
⊢ J ⊆ I
Theorem: Matroid.indep_iff_cl_ssubset_ssubset_forall
Proof state before:
case refine'_1.intro.intro
α : Type u_1
ι : Type u_2
M : Matroid α
F I J✝ X Y B C R : Set α
e✝ f x y : α
hI : autoParam (I ⊆ M.E) _auto✝
h : ∀ e ∈ I, e ∉ M.cl (I \ {e})
J : Set α
hJI : J ⊂ I
h_eq : M.cl J = M.cl I
e : α
heJ : e ∉ J
h' : insert e J ⊆ I
heI : e ∈ M.cl J
⊢ J ⊆ I
Tactic:
exact (subset_insert _ _).trans h'
Proof state after:
no goals
Theorem: Matroid.eq_of_cl_eq_cl_forall
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
M₁ M₂ : Matroid α
h : ∀ (X : Set α), M₁.cl X = M₂.cl X
⊢ M₁.E = M₂.E
Tactic:
simpa using h univ
Proof state after:
no goals
Theorem: Matroid.eq_of_cl_eq_cl_forall
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
M₁ M₂ : Matroid α
h : ∀ (X : Set α), M₁.cl X = M₂.cl X
x✝¹ : Set α
x✝ : x✝¹ ⊆ M₁.E
⊢ M₁.Indep x✝¹ ↔ M₂.Indep x✝¹
Tactic:
simp_rw [indep_iff_cl_diff_ne_forall, h]
Proof state after:
no goals
Theorem: Matroid.restrict_cl_eq'
Proof state before:
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I J X✝ Y B C R✝ : Set α
e f x y : α
M : Matroid α
X R : Set α
⊢ (M ↾ R).cl X = M.cl (X ∩ R) ∩ R ∪ R \ M.E
Tactic:
rw [← cl_inter_ground, restrict_ground_eq]
Proof state after:
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I J X✝ Y B C R✝ : Set α
e f x y : α
M : Matroid α
X R : Set α
⊢ (M ↾ R).cl (X ∩ R) = M.cl (X ∩ R) ∩ R ∪ R \ M.E
Theorem: Matroid.restrict_cl_eq'
Proof state before:
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I J X✝ Y B C R✝ : Set α
e f x y : α
M : Matroid α
X R : Set α
⊢ (M ↾ R).cl (X ∩ R) = M.cl (X ∩ R) ∩ R ∪ R \ M.E
Tactic:
ext e
Proof state after:
case h
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I J X✝ Y B C R✝ : Set α
e✝ f x y : α
M : Matroid α
X R : Set α
e : α
⊢ e ∈ (M ↾ R).cl (X ∩ R) ↔ e ∈ M.cl (X ∩ R) ∩ R ∪ R \ M.E
Theorem: Matroid.restrict_cl_eq'
Proof state before:
case h
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I J X✝ Y B C R✝ : Set α
e✝ f x y : α
M : Matroid α
X R : Set α
e : α
⊢ e ∈ (M ↾ R).cl (X ∩ R) ↔ e ∈ M.cl (X ∩ R) ∩ R ∪ R \ M.E
Tactic:
obtain ⟨I, hI⟩ := (M ↾ R).exists_basis (X ∩ R)
Proof state after:
case h.intro
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X✝ Y B C R✝ : Set α
e✝ f x y : α
M : Matroid α
X R : Set α
e : α
I : Set α
hI : (M ↾ R).Basis I (X ∩ R)
⊢ e ∈ (M ↾ R).cl (X ∩ R) ↔ e ∈ M.cl (X ∩ R) ∩ R ∪ R \ M.E
Theorem: Matroid.restrict_cl_eq'
Proof state before:
case h.intro
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X✝ Y B C R✝ : Set α
e✝ f x y : α
M : Matroid α
X R : Set α
e : α
I : Set α
hI : (M ↾ R).Basis I (X ∩ R)
⊢ e ∈ (M ↾ R).cl (X ∩ R) ↔ e ∈ M.cl (X ∩ R) ∩ R ∪ R \ M.E
Tactic:
have hI' := (basis_restrict_iff'.mp hI).1
Proof state after:
case h.intro
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X✝ Y B C R✝ : Set α
e✝ f x y : α
M : Matroid α
X R : Set α
e : α
I : Set α
hI : (M ↾ R).Basis I (X ∩ R)
hI' : M.Basis I (X ∩ R ∩ M.E)
⊢ e ∈ (M ↾ R).cl (X ∩ R) ↔ e ∈ M.cl (X ∩ R) ∩ R ∪ R \ M.E
Theorem: Matroid.restrict_cl_eq'
Proof state before:
case h.intro
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X✝ Y B C R✝ : Set α
e✝ f x y : α
M : Matroid α
X R : Set α
e : α
I : Set α
hI : (M ↾ R).Basis I (X ∩ R)
hI' : M.Basis I (X ∩ R ∩ M.E)
⊢ e ∈ (M ↾ R).cl (X ∩ R) ↔ e ∈ M.cl (X ∩ R) ∩ R ∪ R \ M.E
Tactic:
rw [← hI.cl_eq_cl, ← M.cl_inter_ground (X ∩ R), ← hI'.cl_eq_cl, mem_union, mem_inter_iff,
  hI'.indep.mem_cl_iff, hI.indep.mem_cl_iff, restrict_dep_iff, insert_subset_iff,
  dep_iff, insert_subset_iff, and_iff_left hI'.indep.subset_ground, mem_diff,
  and_iff_left (show I ⊆ R from hI.indep.subset_ground)]
Proof state after:
case h.intro
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X✝ Y B C R✝ : Set α
e✝ f x y : α
M : Matroid α
X R : Set α
e : α
I : Set α
hI : (M ↾ R).Basis I (X ∩ R)
hI' : M.Basis I (X ∩ R ∩ M.E)
⊢ ¬M.Indep (insert e I) ∧ e ∈ R ∨ e ∈ I ↔ (¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I) ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
Theorem: Matroid.restrict_cl_eq'
Proof state before:
case h.intro
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X✝ Y B C R✝ : Set α
e✝ f x y : α
M : Matroid α
X R : Set α
e : α
I : Set α
hI : (M ↾ R).Basis I (X ∩ R)
hI' : M.Basis I (X ∩ R ∩ M.E)
⊢ ¬M.Indep (insert e I) ∧ e ∈ R ∨ e ∈ I ↔ (¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I) ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
Tactic:
have hIR : I ⊆ R := hI.indep.subset_ground
Proof state after:
case h.intro
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X✝ Y B C R✝ : Set α
e✝ f x y : α
M : Matroid α
X R : Set α
e : α
I : Set α
hI : (M ↾ R).Basis I (X ∩ R)
hI' : M.Basis I (X ∩ R ∩ M.E)
hIR : I ⊆ R
⊢ ¬M.Indep (insert e I) ∧ e ∈ R ∨ e ∈ I ↔ (¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I) ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
Theorem: Matroid.restrict_cl_eq'
Proof state before:
case h.intro
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X✝ Y B C R✝ : Set α
e✝ f x y : α
M : Matroid α
X R : Set α
e : α
I : Set α
hI : (M ↾ R).Basis I (X ∩ R)
hI' : M.Basis I (X ∩ R ∩ M.E)
hIR : I ⊆ R
⊢ ¬M.Indep (insert e I) ∧ e ∈ R ∨ e ∈ I ↔ (¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I) ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
Tactic:
by_cases he : e ∈ M.E
Proof state after:
case pos
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X✝ Y B C R✝ : Set α
e✝ f x y : α
M : Matroid α
X R : Set α
e : α
I : Set α
hI : (M ↾ R).Basis I (X ∩ R)
hI' : M.Basis I (X ∩ R ∩ M.E)
hIR : I ⊆ R
he : e ∈ M.E
⊢ ¬M.Indep (insert e I) ∧ e ∈ R ∨ e ∈ I ↔ (¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I) ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E

case neg
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X✝ Y B C R✝ : Set α
e✝ f x y : α
M : Matroid α
X R : Set α
e : α
I : Set α
hI : (M ↾ R).Basis I (X ∩ R)
hI' : M.Basis I (X ∩ R ∩ M.E)
hIR : I ⊆ R
he : e ∉ M.E
⊢ ¬M.Indep (insert e I) ∧ e ∈ R ∨ e ∈ I ↔ (¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I) ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
Theorem: Matroid.restrict_cl_eq'
Proof state before:
case pos
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X✝ Y B C R✝ : Set α
e✝ f x y : α
M : Matroid α
X R : Set α
e : α
I : Set α
hI : (M ↾ R).Basis I (X ∩ R)
hI' : M.Basis I (X ∩ R ∩ M.E)
hIR : I ⊆ R
he : e ∈ M.E
⊢ ¬M.Indep (insert e I) ∧ e ∈ R ∨ e ∈ I ↔ (¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I) ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E

case neg
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X✝ Y B C R✝ : Set α
e✝ f x y : α
M : Matroid α
X R : Set α
e : α
I : Set α
hI : (M ↾ R).Basis I (X ∩ R)
hI' : M.Basis I (X ∩ R ∩ M.E)
hIR : I ⊆ R
he : e ∉ M.E
⊢ ¬M.Indep (insert e I) ∧ e ∈ R ∨ e ∈ I ↔ (¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I) ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
Tactic:
aesop
Proof state after:
case neg
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X✝ Y B C R✝ : Set α
e✝ f x y : α
M : Matroid α
X R : Set α
e : α
I : Set α
hI : (M ↾ R).Basis I (X ∩ R)
hI' : M.Basis I (X ∩ R ∩ M.E)
hIR : I ⊆ R
he : e ∉ M.E
⊢ ¬M.Indep (insert e I) ∧ e ∈ R ∨ e ∈ I ↔ (¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I) ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
Theorem: Matroid.restrict_cl_eq'
Proof state before:
case neg
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X✝ Y B C R✝ : Set α
e✝ f x y : α
M : Matroid α
X R : Set α
e : α
I : Set α
hI : (M ↾ R).Basis I (X ∩ R)
hI' : M.Basis I (X ∩ R ∩ M.E)
hIR : I ⊆ R
he : e ∉ M.E
⊢ ¬M.Indep (insert e I) ∧ e ∈ R ∨ e ∈ I ↔ (¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I) ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
Tactic:
simp only [iff_false_intro he, and_false, false_or, and_true, ← mem_inter_iff, ← mem_union,
  inter_eq_self_of_subset_left hIR, union_comm I, and_iff_right
    (show ¬M.Indep (insert e I) from fun hi ↦ he (hi.subset_ground (mem_insert _ _))),
  not_false_iff]
Proof state after:
no goals
Theorem: Matroid.restrict_cl_eq
Proof state before:
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I J X Y B C R : Set α
e f x y : α
M : Matroid α
hXR : X ⊆ R
hR : autoParam (R ⊆ M.E) _auto✝
⊢ (M ↾ R).cl X = M.cl X ∩ R
Tactic:
rw [restrict_cl_eq', diff_eq_empty.mpr hR, union_empty, inter_eq_self_of_subset_left hXR]
Proof state after:
no goals
Theorem: Matroid.comap_cl_eq
Proof state before:
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I J X✝ Y B C R : Set α
e f✝ x y : α
β : Type u_3
M : Matroid β
f : α → β
X : Set α
⊢ (M.comap f).cl X = f ⁻¹' M.cl (f '' X)
Tactic:
obtain ⟨I, hI⟩ := (M.comap f).exists_basis' X
Proof state after:
case intro
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X✝ Y B C R : Set α
e f✝ x y : α
β : Type u_3
M : Matroid β
f : α → β
X I : Set α
hI : (M.comap f).Basis' I X
⊢ (M.comap f).cl X = f ⁻¹' M.cl (f '' X)
Theorem: Matroid.comap_cl_eq
Proof state before:
case intro
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X✝ Y B C R : Set α
e f✝ x y : α
β : Type u_3
M : Matroid β
f : α → β
X I : Set α
hI : (M.comap f).Basis' I X
⊢ (M.comap f).cl X = f ⁻¹' M.cl (f '' X)
Tactic:
obtain ⟨hI', -, hIinj⟩ := comap_basis'_iff.1 hI
Proof state after:
case intro.intro.intro
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X✝ Y B C R : Set α
e f✝ x y : α
β : Type u_3
M : Matroid β
f : α → β
X I : Set α
hI : (M.comap f).Basis' I X
hI' : M.Basis' (f '' I) (f '' X)
hIinj : InjOn f I
⊢ (M.comap f).cl X = f ⁻¹' M.cl (f '' X)
Theorem: Matroid.comap_cl_eq
Proof state before:
case intro.intro.intro
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X✝ Y B C R : Set α
e f✝ x y : α
β : Type u_3
M : Matroid β
f : α → β
X I : Set α
hI : (M.comap f).Basis' I X
hI' : M.Basis' (f '' I) (f '' X)
hIinj : InjOn f I
⊢ (M.comap f).cl X = f ⁻¹' M.cl (f '' X)
Tactic:
rw [← hI.cl_eq_cl]
Proof state after:
case intro.intro.intro
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X✝ Y B C R : Set α
e f✝ x y : α
β : Type u_3
M : Matroid β
f : α → β
X I : Set α
hI : (M.comap f).Basis' I X
hI' : M.Basis' (f '' I) (f '' X)
hIinj : InjOn f I
⊢ (M.comap f).cl I = f ⁻¹' M.cl (f '' X)
Theorem: Matroid.comap_cl_eq
Proof state before:
case intro.intro.intro
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X✝ Y B C R : Set α
e f✝ x y : α
β : Type u_3
M : Matroid β
f : α → β
X I : Set α
hI : (M.comap f).Basis' I X
hI' : M.Basis' (f '' I) (f '' X)
hIinj : InjOn f I
⊢ (M.comap f).cl I = f ⁻¹' M.cl (f '' X)
Tactic:
ext x
Proof state after:
case intro.intro.intro.h
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X✝ Y B C R : Set α
e f✝ x✝ y : α
β : Type u_3
M : Matroid β
f : α → β
X I : Set α
hI : (M.comap f).Basis' I X
hI' : M.Basis' (f '' I) (f '' X)
hIinj : InjOn f I
x : α
⊢ x ∈ (M.comap f).cl I ↔ x ∈ f ⁻¹' M.cl (f '' X)