internlm/Lean-Github huggingface dataset:
Theorem: Matroid.Indep.base_of_ground_subset_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 : α
hI : M.Indep I
h : M.E ⊆ M.cl I
⊢ M.Basis I M.E
Tactic:
exact hI.basis_of_subset_of_subset_cl hI.subset_ground h
Proof state after:
no goals
Theorem: Matroid.Base.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 : α
hB : M.Base B
⊢ M.cl B = M.E
Tactic:
rw [← basis_ground_iff] at hB
Proof state after:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
hB : M.Basis B M.E
⊢ M.cl B = M.E
Theorem: Matroid.Base.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 : α
hB : M.Basis B M.E
⊢ M.cl B = M.E
Tactic:
rw [hB.cl_eq_cl, cl_ground]
Proof state after:
no goals
Theorem: Matroid.Base.mem_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 : α
hB : M.Base B
e : α
he : autoParam (e ∈ M.E) _auto✝
⊢ e ∈ M.cl B
Tactic:
rwa [hB.cl_eq]
Proof state after:
no goals
Theorem: Matroid.Base.cl_of_superset
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
hB : M.Base B
hBX : B ⊆ X
⊢ M.E ⊆ M.cl X
Tactic:
rw [← hB.cl_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 : α
hB : M.Base B
hBX : B ⊆ X
⊢ M.cl B ⊆ M.cl X
Theorem: Matroid.Base.cl_of_superset
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
hB : M.Base B
hBX : B ⊆ X
⊢ M.cl B ⊆ M.cl X
Tactic:
exact M.cl_subset_cl hBX
Proof state after:
no goals
Theorem: Matroid.base_iff_indep_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.Base B ↔ M.Indep B ∧ M.cl B = M.E
Tactic:
rw [← basis_ground_iff, basis_iff_indep_subset_cl, and_congr_right_iff]
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.Indep B → (B ⊆ M.E ∧ M.E ⊆ M.cl B ↔ M.cl B = M.E)
Theorem: Matroid.base_iff_indep_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.Indep B → (B ⊆ M.E ∧ M.E ⊆ M.cl B ↔ M.cl B = M.E)
Tactic:
exact fun hI ↦ ⟨fun h ↦ (M.cl_subset_ground _).antisymm h.2,
  fun h ↦ ⟨(M.subset_cl B).trans_eq h, h.symm.subset⟩⟩
Proof state after:
no goals
Theorem: Matroid.Indep.base_iff_ground_subset_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 : α
hI : M.Indep I
h : M.Base I
⊢ M.E ⊆ M.cl I
Tactic:
rw [h.cl_eq]
Proof state after:
no goals
Theorem: Matroid.Indep.cl_inter_eq_self_of_subset
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 : M.Indep I
hJI : J ⊆ I
⊢ M.cl J ∩ I = J
Tactic:
have hJ := hI.subset hJI
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 : M.Indep I
hJI : J ⊆ I
hJ : M.Indep J
⊢ M.cl J ∩ I = J
Theorem: Matroid.Indep.cl_inter_eq_self_of_subset
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 : M.Indep I
hJI : J ⊆ I
hJ : M.Indep J
⊢ M.cl J ∩ I = J
Tactic:
rw [subset_antisymm_iff, and_iff_left (subset_inter (M.subset_cl _) hJI)]
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 : M.Indep I
hJI : J ⊆ I
hJ : M.Indep J
⊢ M.cl J ∩ I ⊆ J
Theorem: Matroid.Indep.cl_inter_eq_self_of_subset
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 : M.Indep I
hJI : J ⊆ I
hJ : M.Indep J
⊢ M.cl J ∩ I ⊆ J
Tactic:
rintro e ⟨heJ, heI⟩
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 : α
hI : M.Indep I
hJI : J ⊆ I
hJ : M.Indep J
e : α
heJ : e ∈ M.cl J
heI : e ∈ I
⊢ e ∈ J
Theorem: Matroid.Indep.cl_inter_eq_self_of_subset
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 : α
hI : M.Indep I
hJI : J ⊆ I
hJ : M.Indep J
e : α
heJ : e ∈ M.cl J
heI : e ∈ I
⊢ e ∈ J
Tactic:
exact hJ.basis_cl.mem_of_insert_indep heJ (hI.subset (insert_subset heI hJI))
Proof state after:
no goals
Theorem: Matroid.Indep.cl_sInter_eq_biInter_cl_of_forall_subset
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
⊢ M.cl (⋂₀ Js) = ⋂ J ∈ Js, M.cl J
Tactic:
rw [subset_antisymm_iff, subset_iInter₂_iff]
Proof state after:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
⊢ (∀ i ∈ Js, M.cl (⋂₀ Js) ⊆ M.cl i) ∧ ⋂ J ∈ Js, M.cl J ⊆ M.cl (⋂₀ Js)
Theorem: Matroid.Indep.cl_sInter_eq_biInter_cl_of_forall_subset
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
⊢ (∀ i ∈ Js, M.cl (⋂₀ Js) ⊆ M.cl i) ∧ ⋂ J ∈ Js, M.cl J ⊆ M.cl (⋂₀ Js)
Tactic:
have hiX : ⋂₀ Js ⊆ I := (sInter_subset_of_mem hne.some_mem).trans (hIs _ hne.some_mem)
Proof state after:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
⊢ (∀ i ∈ Js, M.cl (⋂₀ Js) ⊆ M.cl i) ∧ ⋂ J ∈ Js, M.cl J ⊆ M.cl (⋂₀ Js)
Theorem: Matroid.Indep.cl_sInter_eq_biInter_cl_of_forall_subset
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
⊢ (∀ i ∈ Js, M.cl (⋂₀ Js) ⊆ M.cl i) ∧ ⋂ J ∈ Js, M.cl J ⊆ M.cl (⋂₀ Js)
Tactic:
have hiI := hI.subset hiX
Proof state after:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
⊢ (∀ i ∈ Js, M.cl (⋂₀ Js) ⊆ M.cl i) ∧ ⋂ J ∈ Js, M.cl J ⊆ M.cl (⋂₀ Js)
Theorem: Matroid.Indep.cl_sInter_eq_biInter_cl_of_forall_subset
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
⊢ (∀ i ∈ Js, M.cl (⋂₀ Js) ⊆ M.cl i) ∧ ⋂ J ∈ Js, M.cl J ⊆ M.cl (⋂₀ Js)
Tactic:
refine' ⟨ fun X hX ↦ M.cl_subset_cl (sInter_subset_of_mem hX), fun e he ↦ by_contra fun he' ↦ _⟩
Proof state after:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e✝ f x y : α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : e ∈ ⋂ J ∈ Js, M.cl J
he' : e ∉ M.cl (⋂₀ Js)
⊢ False
Theorem: Matroid.Indep.cl_sInter_eq_biInter_cl_of_forall_subset
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e✝ f x y : α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : e ∈ ⋂ J ∈ Js, M.cl J
he' : e ∉ M.cl (⋂₀ Js)
⊢ False
Tactic:
rw [mem_iInter₂] at he
Proof state after:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e✝ f x y : α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ i ∈ Js, e ∈ M.cl i
he' : e ∉ M.cl (⋂₀ Js)
⊢ False
Theorem: Matroid.Indep.cl_sInter_eq_biInter_cl_of_forall_subset
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e✝ f x y : α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ i ∈ Js, e ∈ M.cl i
he' : e ∉ M.cl (⋂₀ Js)
⊢ False
Tactic:
have heEI : e ∈ M.E \ I := by
  refine' ⟨M.cl_subset_ground _ (he _ hne.some_mem), fun heI ↦ he' _⟩
  refine' mem_cl_of_mem _ (fun X hX' ↦ _) hiI.subset_ground
  rw [← hI.cl_inter_eq_self_of_subset (hIs X hX')]
  exact ⟨he X hX', heI⟩
Proof state after:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e✝ f x y : α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ i ∈ Js, e ∈ M.cl i
he' : e ∉ M.cl (⋂₀ Js)
heEI : e ∈ M.E \ I
⊢ False
Theorem: Matroid.Indep.cl_sInter_eq_biInter_cl_of_forall_subset
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e✝ f x y : α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ i ∈ Js, e ∈ M.cl i
he' : e ∉ M.cl (⋂₀ Js)
heEI : e ∈ M.E \ I
⊢ False
Tactic:
rw [hiI.not_mem_cl_iff_of_not_mem (not_mem_subset hiX heEI.2)] at he'
Proof state after:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e✝ f x y : α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ i ∈ Js, e ∈ M.cl i
he' : M.Indep (insert e (⋂₀ Js))
heEI : e ∈ M.E \ I
⊢ False
Theorem: Matroid.Indep.cl_sInter_eq_biInter_cl_of_forall_subset
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e✝ f x y : α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ i ∈ Js, e ∈ M.cl i
he' : M.Indep (insert e (⋂₀ Js))
heEI : e ∈ M.E \ I
⊢ False
Tactic:
obtain ⟨J, hJI, heJ⟩ := he'.subset_basis_of_subset (insert_subset_insert hiX)
  (insert_subset heEI.1 hI.subset_ground)
Proof state after:
case intro.intro
α : Type u_1
ι : Type u_2
M : Matroid α
F I J✝ X Y B C R : Set α
e✝ f x y : α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ i ∈ Js, e ∈ M.cl i
he' : M.Indep (insert e (⋂₀ Js))
heEI : e ∈ M.E \ I
J : Set α
hJI : M.Basis J (insert e I)
heJ : insert e (⋂₀ Js) ⊆ J
⊢ False
Theorem: Matroid.Indep.cl_sInter_eq_biInter_cl_of_forall_subset
Proof state before:
case intro.intro
α : Type u_1
ι : Type u_2
M : Matroid α
F I J✝ X Y B C R : Set α
e✝ f x y : α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ i ∈ Js, e ∈ M.cl i
he' : M.Indep (insert e (⋂₀ Js))
heEI : e ∈ M.E \ I
J : Set α
hJI : M.Basis J (insert e I)
heJ : insert e (⋂₀ Js) ⊆ J
⊢ False
Tactic:
have hIb : M.Basis I (insert e I) := by
  rw [hI.insert_basis_iff_mem_cl]; exact (M.cl_subset_cl (hIs _ hne.some_mem)) (he _ hne.some_mem)
Proof state after:
case intro.intro
α : Type u_1
ι : Type u_2
M : Matroid α
F I J✝ X Y B C R : Set α
e✝ f x y : α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ i ∈ Js, e ∈ M.cl i
he' : M.Indep (insert e (⋂₀ Js))
heEI : e ∈ M.E \ I
J : Set α
hJI : M.Basis J (insert e I)
heJ : insert e (⋂₀ Js) ⊆ J
hIb : M.Basis I (insert e I)
⊢ False
Theorem: Matroid.Indep.cl_sInter_eq_biInter_cl_of_forall_subset
Proof state before:
case intro.intro
α : Type u_1
ι : Type u_2
M : Matroid α
F I J✝ X Y B C R : Set α
e✝ f x y : α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ i ∈ Js, e ∈ M.cl i
he' : M.Indep (insert e (⋂₀ Js))
heEI : e ∈ M.E \ I
J : Set α
hJI : M.Basis J (insert e I)
heJ : insert e (⋂₀ Js) ⊆ J
hIb : M.Basis I (insert e I)
⊢ False
Tactic:
obtain ⟨f, hfIJ, hfb⟩ :=  hJI.exchange hIb ⟨heJ (mem_insert e _), heEI.2⟩
Proof state after:
case intro.intro.intro.intro
α : Type u_1
ι : Type u_2
M : Matroid α
F I J✝ X Y B C R : Set α
e✝ f✝ x y : α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ i ∈ Js, e ∈ M.cl i
he' : M.Indep (insert e (⋂₀ Js))
heEI : e ∈ M.E \ I
J : Set α
hJI : M.Basis J (insert e I)
heJ : insert e (⋂₀ Js) ⊆ J
hIb : M.Basis I (insert e I)
f : α
hfIJ : f ∈ I \ J
hfb : M.Basis (insert f (J \ {e})) (insert e I)
⊢ False
Theorem: Matroid.Indep.cl_sInter_eq_biInter_cl_of_forall_subset
Proof state before:
case intro.intro.intro.intro
α : Type u_1
ι : Type u_2
M : Matroid α
F I J✝ X Y B C R : Set α
e✝ f✝ x y : α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ i ∈ Js, e ∈ M.cl i
he' : M.Indep (insert e (⋂₀ Js))
heEI : e ∈ M.E \ I
J : Set α
hJI : M.Basis J (insert e I)
heJ : insert e (⋂₀ Js) ⊆ J
hIb : M.Basis I (insert e I)
f : α
hfIJ : f ∈ I \ J
hfb : M.Basis (insert f (J \ {e})) (insert e I)
⊢ False
Tactic:
obtain rfl := hI.eq_of_basis (hfb.basis_subset (insert_subset hfIJ.1
  (by (rw [diff_subset_iff, singleton_union]; exact hJI.subset))) (subset_insert _ _))
Proof state after:
case intro.intro.intro.intro
α : Type u_1
ι : Type u_2
M : Matroid α
F J✝ X Y B C R : Set α
e✝ f✝ x y : α
Js : Set (Set α)
hne : Js.Nonempty
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ i ∈ Js, e ∈ M.cl i
he' : M.Indep (insert e (⋂₀ Js))
J : Set α
heJ : insert e (⋂₀ Js) ⊆ J
f : α
hI : M.Indep (insert f (J \ {e}))
hIs : ∀ J_1 ∈ Js, J_1 ⊆ insert f (J \ {e})
hiX : ⋂₀ Js ⊆ insert f (J \ {e})
heEI : e ∈ M.E \ insert f (J \ {e})
hJI : M.Basis J (insert e (insert f (J \ {e})))
hIb : M.Basis (insert f (J \ {e})) (insert e (insert f (J \ {e})))
hfIJ : f ∈ insert f (J \ {e}) \ J
hfb : M.Basis (insert f (J \ {e})) (insert e (insert f (J \ {e})))
⊢ False
Theorem: Matroid.Indep.cl_sInter_eq_biInter_cl_of_forall_subset
Proof state before:
case intro.intro.intro.intro
α : Type u_1
ι : Type u_2
M : Matroid α
F J✝ X Y B C R : Set α
e✝ f✝ x y : α
Js : Set (Set α)
hne : Js.Nonempty
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ i ∈ Js, e ∈ M.cl i
he' : M.Indep (insert e (⋂₀ Js))
J : Set α
heJ : insert e (⋂₀ Js) ⊆ J
f : α
hI : M.Indep (insert f (J \ {e}))
hIs : ∀ J_1 ∈ Js, J_1 ⊆ insert f (J \ {e})
hiX : ⋂₀ Js ⊆ insert f (J \ {e})
heEI : e ∈ M.E \ insert f (J \ {e})
hJI : M.Basis J (insert e (insert f (J \ {e})))
hIb : M.Basis (insert f (J \ {e})) (insert e (insert f (J \ {e})))
hfIJ : f ∈ insert f (J \ {e}) \ J
hfb : M.Basis (insert f (J \ {e})) (insert e (insert f (J \ {e})))
⊢ False
Tactic:
refine' hfIJ.2 (heJ (mem_insert_of_mem _ fun X hX' ↦ by_contra fun hfX ↦ _))
Proof state after:
case intro.intro.intro.intro
α : Type u_1
ι : Type u_2
M : Matroid α
F J✝ X✝ Y B C R : Set α
e✝ f✝ x y : α
Js : Set (Set α)
hne : Js.Nonempty
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ i ∈ Js, e ∈ M.cl i
he' : M.Indep (insert e (⋂₀ Js))
J : Set α
heJ : insert e (⋂₀ Js) ⊆ J
f : α
hI : M.Indep (insert f (J \ {e}))
hIs : ∀ J_1 ∈ Js, J_1 ⊆ insert f (J \ {e})
hiX : ⋂₀ Js ⊆ insert f (J \ {e})
heEI : e ∈ M.E \ insert f (J \ {e})
hJI : M.Basis J (insert e (insert f (J \ {e})))
hIb : M.Basis (insert f (J \ {e})) (insert e (insert f (J \ {e})))
hfIJ : f ∈ insert f (J \ {e}) \ J
hfb : M.Basis (insert f (J \ {e})) (insert e (insert f (J \ {e})))
X : Set α
hX' : X ∈ Js
hfX : f ∉ X
⊢ False
Theorem: Matroid.Indep.cl_sInter_eq_biInter_cl_of_forall_subset
Proof state before:
case intro.intro.intro.intro
α : Type u_1
ι : Type u_2
M : Matroid α
F J✝ X✝ Y B C R : Set α
e✝ f✝ x y : α
Js : Set (Set α)
hne : Js.Nonempty
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ i ∈ Js, e ∈ M.cl i
he' : M.Indep (insert e (⋂₀ Js))
J : Set α
heJ : insert e (⋂₀ Js) ⊆ J
f : α
hI : M.Indep (insert f (J \ {e}))
hIs : ∀ J_1 ∈ Js, J_1 ⊆ insert f (J \ {e})
hiX : ⋂₀ Js ⊆ insert f (J \ {e})
heEI : e ∈ M.E \ insert f (J \ {e})
hJI : M.Basis J (insert e (insert f (J \ {e})))
hIb : M.Basis (insert f (J \ {e})) (insert e (insert f (J \ {e})))
hfIJ : f ∈ insert f (J \ {e}) \ J
hfb : M.Basis (insert f (J \ {e})) (insert e (insert f (J \ {e})))
X : Set α
hX' : X ∈ Js
hfX : f ∉ X
⊢ False
Tactic:
obtain (hd | heX) := ((hI.subset (hIs X hX')).mem_cl_iff).mp (he _ hX')
Proof state after:
case intro.intro.intro.intro.inl
α : Type u_1
ι : Type u_2
M : Matroid α
F J✝ X✝ Y B C R : Set α
e✝ f✝ x y : α
Js : Set (Set α)
hne : Js.Nonempty
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ i ∈ Js, e ∈ M.cl i
he' : M.Indep (insert e (⋂₀ Js))
J : Set α
heJ : insert e (⋂₀ Js) ⊆ J
f : α
hI : M.Indep (insert f (J \ {e}))
hIs : ∀ J_1 ∈ Js, J_1 ⊆ insert f (J \ {e})
hiX : ⋂₀ Js ⊆ insert f (J \ {e})
heEI : e ∈ M.E \ insert f (J \ {e})
hJI : M.Basis J (insert e (insert f (J \ {e})))
hIb : M.Basis (insert f (J \ {e})) (insert e (insert f (J \ {e})))
hfIJ : f ∈ insert f (J \ {e}) \ J
hfb : M.Basis (insert f (J \ {e})) (insert e (insert f (J \ {e})))
X : Set α
hX' : X ∈ Js
hfX : f ∉ X
hd : M.Dep (insert e X)
⊢ False

case intro.intro.intro.intro.inr
α : Type u_1
ι : Type u_2
M : Matroid α
F J✝ X✝ Y B C R : Set α
e✝ f✝ x y : α
Js : Set (Set α)
hne : Js.Nonempty
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ i ∈ Js, e ∈ M.cl i
he' : M.Indep (insert e (⋂₀ Js))
J : Set α
heJ : insert e (⋂₀ Js) ⊆ J
f : α
hI : M.Indep (insert f (J \ {e}))
hIs : ∀ J_1 ∈ Js, J_1 ⊆ insert f (J \ {e})
hiX : ⋂₀ Js ⊆ insert f (J \ {e})
heEI : e ∈ M.E \ insert f (J \ {e})
hJI : M.Basis J (insert e (insert f (J \ {e})))
hIb : M.Basis (insert f (J \ {e})) (insert e (insert f (J \ {e})))
hfIJ : f ∈ insert f (J \ {e}) \ J
hfb : M.Basis (insert f (J \ {e})) (insert e (insert f (J \ {e})))
X : Set α
hX' : X ∈ Js
hfX : f ∉ X
heX : e ∈ X
⊢ False
Theorem: Matroid.Indep.cl_sInter_eq_biInter_cl_of_forall_subset
Proof state before:
case intro.intro.intro.intro.inr
α : Type u_1
ι : Type u_2
M : Matroid α
F J✝ X✝ Y B C R : Set α
e✝ f✝ x y : α
Js : Set (Set α)
hne : Js.Nonempty
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ i ∈ Js, e ∈ M.cl i
he' : M.Indep (insert e (⋂₀ Js))
J : Set α
heJ : insert e (⋂₀ Js) ⊆ J
f : α
hI : M.Indep (insert f (J \ {e}))
hIs : ∀ J_1 ∈ Js, J_1 ⊆ insert f (J \ {e})
hiX : ⋂₀ Js ⊆ insert f (J \ {e})
heEI : e ∈ M.E \ insert f (J \ {e})
hJI : M.Basis J (insert e (insert f (J \ {e})))
hIb : M.Basis (insert f (J \ {e})) (insert e (insert f (J \ {e})))
hfIJ : f ∈ insert f (J \ {e}) \ J
hfb : M.Basis (insert f (J \ {e})) (insert e (insert f (J \ {e})))
X : Set α
hX' : X ∈ Js
hfX : f ∉ X
heX : e ∈ X
⊢ False
Tactic:
exact heEI.2 (hIs _ hX' heX)
Proof state after:
no goals
Theorem: Matroid.Indep.cl_sInter_eq_biInter_cl_of_forall_subset
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e✝ f x y : α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ i ∈ Js, e ∈ M.cl i
he' : e ∉ M.cl (⋂₀ Js)
⊢ e ∈ M.E \ I
Tactic:
refine' ⟨M.cl_subset_ground _ (he _ hne.some_mem), fun heI ↦ he' _⟩
Proof state after:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e✝ f x y : α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ i ∈ Js, e ∈ M.cl i
he' : e ∉ M.cl (⋂₀ Js)
heI : e ∈ I
⊢ e ∈ M.cl (⋂₀ Js)
Theorem: Matroid.Indep.cl_sInter_eq_biInter_cl_of_forall_subset
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e✝ f x y : α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ i ∈ Js, e ∈ M.cl i
he' : e ∉ M.cl (⋂₀ Js)
heI : e ∈ I
⊢ e ∈ M.cl (⋂₀ Js)
Tactic:
refine' mem_cl_of_mem _ (fun X hX' ↦ _) hiI.subset_ground
Proof state after:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X✝ Y B C R : Set α
e✝ f x y : α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ i ∈ Js, e ∈ M.cl i
he' : e ∉ M.cl (⋂₀ Js)
heI : e ∈ I
X : Set α
hX' : X ∈ Js
⊢ e ∈ X
Theorem: Matroid.Indep.cl_sInter_eq_biInter_cl_of_forall_subset
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X✝ Y B C R : Set α
e✝ f x y : α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ i ∈ Js, e ∈ M.cl i
he' : e ∉ M.cl (⋂₀ Js)
heI : e ∈ I
X : Set α
hX' : X ∈ Js
⊢ e ∈ X
Tactic:
rw [← hI.cl_inter_eq_self_of_subset (hIs X hX')]
Proof state after:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X✝ Y B C R : Set α
e✝ f x y : α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ i ∈ Js, e ∈ M.cl i
he' : e ∉ M.cl (⋂₀ Js)
heI : e ∈ I
X : Set α
hX' : X ∈ Js
⊢ e ∈ M.cl X ∩ I
Theorem: Matroid.Indep.cl_sInter_eq_biInter_cl_of_forall_subset
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X✝ Y B C R : Set α
e✝ f x y : α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ i ∈ Js, e ∈ M.cl i
he' : e ∉ M.cl (⋂₀ Js)
heI : e ∈ I
X : Set α
hX' : X ∈ Js
⊢ e ∈ M.cl X ∩ I
Tactic:
exact ⟨he X hX', heI⟩
Proof state after:
no goals
Theorem: Matroid.Indep.cl_sInter_eq_biInter_cl_of_forall_subset
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J✝ X Y B C R : Set α
e✝ f x y : α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ i ∈ Js, e ∈ M.cl i
he' : M.Indep (insert e (⋂₀ Js))
heEI : e ∈ M.E \ I
J : Set α
hJI : M.Basis J (insert e I)
heJ : insert e (⋂₀ Js) ⊆ J
⊢ M.Basis I (insert e I)
Tactic:
rw [hI.insert_basis_iff_mem_cl]
Proof state after:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J✝ X Y B C R : Set α
e✝ f x y : α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ i ∈ Js, e ∈ M.cl i
he' : M.Indep (insert e (⋂₀ Js))
heEI : e ∈ M.E \ I
J : Set α
hJI : M.Basis J (insert e I)
heJ : insert e (⋂₀ Js) ⊆ J
⊢ e ∈ M.cl I
Theorem: Matroid.Indep.cl_sInter_eq_biInter_cl_of_forall_subset
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J✝ X Y B C R : Set α
e✝ f x y : α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ i ∈ Js, e ∈ M.cl i
he' : M.Indep (insert e (⋂₀ Js))
heEI : e ∈ M.E \ I
J : Set α
hJI : M.Basis J (insert e I)
heJ : insert e (⋂₀ Js) ⊆ J
⊢ e ∈ M.cl I
Tactic:
exact (M.cl_subset_cl (hIs _ hne.some_mem)) (he _ hne.some_mem)
Proof state after:
no goals
Theorem: Matroid.Indep.cl_sInter_eq_biInter_cl_of_forall_subset
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J✝ X Y B C R : Set α
e✝ f✝ x y : α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ i ∈ Js, e ∈ M.cl i
he' : M.Indep (insert e (⋂₀ Js))
heEI : e ∈ M.E \ I
J : Set α
hJI : M.Basis J (insert e I)
heJ : insert e (⋂₀ Js) ⊆ J
hIb : M.Basis I (insert e I)
f : α
hfIJ : f ∈ I \ J
hfb : M.Basis (insert f (J \ {e})) (insert e I)
⊢ J \ {e} ⊆ I
Tactic:
(rw [diff_subset_iff, singleton_union]; exact hJI.subset)
Proof state after:
no goals
Theorem: Matroid.Indep.cl_sInter_eq_biInter_cl_of_forall_subset
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J✝ X Y B C R : Set α
e✝ f✝ x y : α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ i ∈ Js, e ∈ M.cl i
he' : M.Indep (insert e (⋂₀ Js))
heEI : e ∈ M.E \ I
J : Set α
hJI : M.Basis J (insert e I)
heJ : insert e (⋂₀ Js) ⊆ J
hIb : M.Basis I (insert e I)
f : α
hfIJ : f ∈ I \ J
hfb : M.Basis (insert f (J \ {e})) (insert e I)
⊢ J \ {e} ⊆ I
Tactic:
rw [diff_subset_iff, singleton_union]
Proof state after:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J✝ X Y B C R : Set α
e✝ f✝ x y : α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ i ∈ Js, e ∈ M.cl i
he' : M.Indep (insert e (⋂₀ Js))
heEI : e ∈ M.E \ I
J : Set α
hJI : M.Basis J (insert e I)
heJ : insert e (⋂₀ Js) ⊆ J
hIb : M.Basis I (insert e I)
f : α
hfIJ : f ∈ I \ J
hfb : M.Basis (insert f (J \ {e})) (insert e I)
⊢ J ⊆ insert e I
Theorem: Matroid.Indep.cl_sInter_eq_biInter_cl_of_forall_subset
Proof state before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J✝ X Y B C R : Set α
e✝ f✝ x y : α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ i ∈ Js, e ∈ M.cl i
he' : M.Indep (insert e (⋂₀ Js))
heEI : e ∈ M.E \ I
J : Set α
hJI : M.Basis J (insert e I)
heJ : insert e (⋂₀ Js) ⊆ J
hIb : M.Basis I (insert e I)
f : α
hfIJ : f ∈ I \ J
hfb : M.Basis (insert f (J \ {e})) (insert e I)
⊢ J ⊆ insert e I
Tactic:
exact hJI.subset
Proof state after:
no goals