Theorem: Matroid.Indep.cl_sInter_eq_biInter_cl_of_forall_subset (Matroid/Closure.lean)

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]
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)

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)
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)

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
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)

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' ↦ _⟩
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

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
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

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⟩
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

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'
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

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)
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

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)
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

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⟩
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

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 _ _))
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

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 ↦ _))
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

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')
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

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)
State after:
no goals

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' _⟩
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)

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
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

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')]
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

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⟩
State after:
no goals

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]
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

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)
State after:
no goals

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)
State after:
no goals

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]
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

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
State after:
no goals

State before:
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
Tactic:
refine' (hJI.indep.subset (insert_subset (heJ (mem_insert _ _)) _)).not_dep hd
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)
⊢ X ⊆ J

State before:
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)
⊢ X ⊆ J
Tactic:
specialize hIs _ hX'
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}))
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)
hIs : X ⊆ insert f (J \ {e})
⊢ X ⊆ J

State before:
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}))
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)
hIs : X ⊆ insert f (J \ {e})
⊢ X ⊆ J
Tactic:
rw [← singleton_union, ← diff_subset_iff, diff_singleton_eq_self hfX] at hIs
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}))
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)
hIs : X ⊆ J \ {e}
⊢ X ⊆ J

State before:
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}))
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)
hIs : X ⊆ J \ {e}
⊢ X ⊆ J
Tactic:
exact hIs.trans diff_subset
State after:
no goals