Theorem: Matroid.modularPair_insert_cl (Matroid/Modular.lean)

State before:
ι : Type u_1
α : Type u_2
M✝ : Matroid α
B I J X✝ X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e✝ f✝ : α
M : Matroid α
X : Set α
e f : α
⊢ M.ModularPair (M.cl (insert e X)) (M.cl (insert f X))
Tactic:
obtain ⟨I, hI⟩ := M.exists_basis' X
State after:
case intro
ι : Type u_1
α : Type u_2
M✝ : Matroid α
B I✝ J X✝ X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e✝ f✝ : α
M : Matroid α
X : Set α
e f : α
I : Set α
hI : M.Basis' I X
⊢ M.ModularPair (M.cl (insert e X)) (M.cl (insert f X))

State before:
case intro
ι : Type u_1
α : Type u_2
M✝ : Matroid α
B I✝ J X✝ X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e✝ f✝ : α
M : Matroid α
X : Set α
e f : α
I : Set α
hI : M.Basis' I X
⊢ M.ModularPair (M.cl (insert e X)) (M.cl (insert f X))
Tactic:
rw [← cl_insert_cl_eq_cl_insert, ← cl_insert_cl_eq_cl_insert (e := f), ← hI.cl_eq_cl]
State after:
case intro
ι : Type u_1
α : Type u_2
M✝ : Matroid α
B I✝ J X✝ X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e✝ f✝ : α
M : Matroid α
X : Set α
e f : α
I : Set α
hI : M.Basis' I X
⊢ M.ModularPair (M.cl (insert e (M.cl I))) (M.cl (insert f (M.cl I)))

State before:
case intro
ι : Type u_1
α : Type u_2
M✝ : Matroid α
B I✝ J X✝ X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e✝ f✝ : α
M : Matroid α
X : Set α
e f : α
I : Set α
hI : M.Basis' I X
⊢ M.ModularPair (M.cl (insert e (M.cl I))) (M.cl (insert f (M.cl I)))
Tactic:
obtain (he | he) := em' (e ∈ M.E)
State after:
case intro.inl
ι : Type u_1
α : Type u_2
M✝ : Matroid α
B I✝ J X✝ X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e✝ f✝ : α
M : Matroid α
X : Set α
e f : α
I : Set α
hI : M.Basis' I X
he : e ∉ M.E
⊢ M.ModularPair (M.cl (insert e (M.cl I))) (M.cl (insert f (M.cl I)))

case intro.inr
ι : Type u_1
α : Type u_2
M✝ : Matroid α
B I✝ J X✝ X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e✝ f✝ : α
M : Matroid α
X : Set α
e f : α
I : Set α
hI : M.Basis' I X
he : e ∈ M.E
⊢ M.ModularPair (M.cl (insert e (M.cl I))) (M.cl (insert f (M.cl I)))

State before:
case intro.inr
ι : Type u_1
α : Type u_2
M✝ : Matroid α
B I✝ J X✝ X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e✝ f✝ : α
M : Matroid α
X : Set α
e f : α
I : Set α
hI : M.Basis' I X
he : e ∈ M.E
⊢ M.ModularPair (M.cl (insert e (M.cl I))) (M.cl (insert f (M.cl I)))
Tactic:
obtain (hf | hf) := em' (f ∈ M.E)
State after:
case intro.inr.inl
ι : Type u_1
α : Type u_2
M✝ : Matroid α
B I✝ J X✝ X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e✝ f✝ : α
M : Matroid α
X : Set α
e f : α
I : Set α
hI : M.Basis' I X
he : e ∈ M.E
hf : f ∉ M.E
⊢ M.ModularPair (M.cl (insert e (M.cl I))) (M.cl (insert f (M.cl I)))

case intro.inr.inr
ι : Type u_1
α : Type u_2
M✝ : Matroid α
B I✝ J X✝ X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e✝ f✝ : α
M : Matroid α
X : Set α
e f : α
I : Set α
hI : M.Basis' I X
he : e ∈ M.E
hf : f ∈ M.E
⊢ M.ModularPair (M.cl (insert e (M.cl I))) (M.cl (insert f (M.cl I)))

State before:
case intro.inr.inr
ι : Type u_1
α : Type u_2
M✝ : Matroid α
B I✝ J X✝ X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e✝ f✝ : α
M : Matroid α
X : Set α
e f : α
I : Set α
hI : M.Basis' I X
he : e ∈ M.E
hf : f ∈ M.E
⊢ M.ModularPair (M.cl (insert e (M.cl I))) (M.cl (insert f (M.cl I)))
Tactic:
obtain (hfI | hfI) := em (f ∈ M.cl I)
State after:
case intro.inr.inr.inl
ι : Type u_1
α : Type u_2
M✝ : Matroid α
B I✝ J X✝ X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e✝ f✝ : α
M : Matroid α
X : Set α
e f : α
I : Set α
hI : M.Basis' I X
he : e ∈ M.E
hf : f ∈ M.E
hfI : f ∈ M.cl I
⊢ M.ModularPair (M.cl (insert e (M.cl I))) (M.cl (insert f (M.cl I)))

case intro.inr.inr.inr
ι : Type u_1
α : Type u_2
M✝ : Matroid α
B I✝ J X✝ X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e✝ f✝ : α
M : Matroid α
X : Set α
e f : α
I : Set α
hI : M.Basis' I X
he : e ∈ M.E
hf : f ∈ M.E
hfI : f ∉ M.cl I
⊢ M.ModularPair (M.cl (insert e (M.cl I))) (M.cl (insert f (M.cl I)))

State before:
case intro.inr.inr.inr
ι : Type u_1
α : Type u_2
M✝ : Matroid α
B I✝ J X✝ X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e✝ f✝ : α
M : Matroid α
X : Set α
e f : α
I : Set α
hI : M.Basis' I X
he : e ∈ M.E
hf : f ∈ M.E
hfI : f ∉ M.cl I
⊢ M.ModularPair (M.cl (insert e (M.cl I))) (M.cl (insert f (M.cl I)))
Tactic:
rw [cl_insert_cl_eq_cl_insert, cl_insert_cl_eq_cl_insert]
State after:
case intro.inr.inr.inr
ι : Type u_1
α : Type u_2
M✝ : Matroid α
B I✝ J X✝ X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e✝ f✝ : α
M : Matroid α
X : Set α
e f : α
I : Set α
hI : M.Basis' I X
he : e ∈ M.E
hf : f ∈ M.E
hfI : f ∉ M.cl I
⊢ M.ModularPair (M.cl (insert e I)) (M.cl (insert f I))

State before:
case intro.inr.inr.inr
ι : Type u_1
α : Type u_2
M✝ : Matroid α
B I✝ J X✝ X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e✝ f✝ : α
M : Matroid α
X : Set α
e f : α
I : Set α
hI : M.Basis' I X
he : e ∈ M.E
hf : f ∈ M.E
hfI : f ∉ M.cl I
⊢ M.ModularPair (M.cl (insert e I)) (M.cl (insert f I))
Tactic:
obtain (hef | hef) := em (e ∈ M.cl (insert f I))
State after:
case intro.inr.inr.inr.inl
ι : Type u_1
α : Type u_2
M✝ : Matroid α
B I✝ J X✝ X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e✝ f✝ : α
M : Matroid α
X : Set α
e f : α
I : Set α
hI : M.Basis' I X
he : e ∈ M.E
hf : f ∈ M.E
hfI : f ∉ M.cl I
hef : e ∈ M.cl (insert f I)
⊢ M.ModularPair (M.cl (insert e I)) (M.cl (insert f I))

case intro.inr.inr.inr.inr
ι : Type u_1
α : Type u_2
M✝ : Matroid α
B I✝ J X✝ X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e✝ f✝ : α
M : Matroid α
X : Set α
e f : α
I : Set α
hI : M.Basis' I X
he : e ∈ M.E
hf : f ∈ M.E
hfI : f ∉ M.cl I
hef : e ∉ M.cl (insert f I)
⊢ M.ModularPair (M.cl (insert e I)) (M.cl (insert f I))

State before:
case intro.inr.inr.inr.inr
ι : Type u_1
α : Type u_2
M✝ : Matroid α
B I✝ J X✝ X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e✝ f✝ : α
M : Matroid α
X : Set α
e f : α
I : Set α
hI : M.Basis' I X
he : e ∈ M.E
hf : f ∈ M.E
hfI : f ∉ M.cl I
hef : e ∉ M.cl (insert f I)
⊢ M.ModularPair (M.cl (insert e I)) (M.cl (insert f I))
Tactic:
refine ModularPair.cl_cl ?_
State after:
case intro.inr.inr.inr.inr
ι : Type u_1
α : Type u_2
M✝ : Matroid α
B I✝ J X✝ X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e✝ f✝ : α
M : Matroid α
X : Set α
e f : α
I : Set α
hI : M.Basis' I X
he : e ∈ M.E
hf : f ∈ M.E
hfI : f ∉ M.cl I
hef : e ∉ M.cl (insert f I)
⊢ M.ModularPair (insert e I) (insert f I)

State before:
case intro.inr.inr.inr.inr
ι : Type u_1
α : Type u_2
M✝ : Matroid α
B I✝ J X✝ X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e✝ f✝ : α
M : Matroid α
X : Set α
e f : α
I : Set α
hI : M.Basis' I X
he : e ∈ M.E
hf : f ∈ M.E
hfI : f ∉ M.cl I
hef : e ∉ M.cl (insert f I)
⊢ M.ModularPair (insert e I) (insert f I)
Tactic:
apply Indep.modularPair_of_union
State after:
case intro.inr.inr.inr.inr.hi
ι : Type u_1
α : Type u_2
M✝ : Matroid α
B I✝ J X✝ X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e✝ f✝ : α
M : Matroid α
X : Set α
e f : α
I : Set α
hI : M.Basis' I X
he : e ∈ M.E
hf : f ∈ M.E
hfI : f ∉ M.cl I
hef : e ∉ M.cl (insert f I)
⊢ M.Indep (insert e I ∪ insert f I)

State before:
case intro.inr.inr.inr.inr.hi
ι : Type u_1
α : Type u_2
M✝ : Matroid α
B I✝ J X✝ X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e✝ f✝ : α
M : Matroid α
X : Set α
e f : α
I : Set α
hI : M.Basis' I X
he : e ∈ M.E
hf : f ∈ M.E
hfI : f ∉ M.cl I
hef : e ∉ M.cl (insert f I)
⊢ M.Indep (insert e I ∪ insert f I)
Tactic:
rw [union_insert, union_eq_self_of_subset_right (subset_insert _ _), insert_comm,
  Indep.insert_indep_iff]
State after:
case intro.inr.inr.inr.inr.hi
ι : Type u_1
α : Type u_2
M✝ : Matroid α
B I✝ J X✝ X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e✝ f✝ : α
M : Matroid α
X : Set α
e f : α
I : Set α
hI : M.Basis' I X
he : e ∈ M.E
hf : f ∈ M.E
hfI : f ∉ M.cl I
hef : e ∉ M.cl (insert f I)
⊢ e ∈ M.E \ M.cl (insert f I) ∨ e ∈ insert f I

case intro.inr.inr.inr.inr.hi
ι : Type u_1
α : Type u_2
M✝ : Matroid α
B I✝ J X✝ X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e✝ f✝ : α
M : Matroid α
X : Set α
e f : α
I : Set α
hI : M.Basis' I X
he : e ∈ M.E
hf : f ∈ M.E
hfI : f ∉ M.cl I
hef : e ∉ M.cl (insert f I)
⊢ M.Indep (insert f I)

State before:
case intro.inr.inr.inr.inr.hi
ι : Type u_1
α : Type u_2
M✝ : Matroid α
B I✝ J X✝ X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e✝ f✝ : α
M : Matroid α
X : Set α
e f : α
I : Set α
hI : M.Basis' I X
he : e ∈ M.E
hf : f ∈ M.E
hfI : f ∉ M.cl I
hef : e ∉ M.cl (insert f I)
⊢ M.Indep (insert f I)
Tactic:
rw [hI.indep.insert_indep_iff]
State after:
case intro.inr.inr.inr.inr.hi
ι : Type u_1
α : Type u_2
M✝ : Matroid α
B I✝ J X✝ X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e✝ f✝ : α
M : Matroid α
X : Set α
e f : α
I : Set α
hI : M.Basis' I X
he : e ∈ M.E
hf : f ∈ M.E
hfI : f ∉ M.cl I
hef : e ∉ M.cl (insert f I)
⊢ f ∈ M.E \ M.cl I ∨ f ∈ I

State before:
case intro.inr.inr.inr.inr.hi
ι : Type u_1
α : Type u_2
M✝ : Matroid α
B I✝ J X✝ X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e✝ f✝ : α
M : Matroid α
X : Set α
e f : α
I : Set α
hI : M.Basis' I X
he : e ∈ M.E
hf : f ∈ M.E
hfI : f ∉ M.cl I
hef : e ∉ M.cl (insert f I)
⊢ f ∈ M.E \ M.cl I ∨ f ∈ I
Tactic:
exact .inl ⟨hf, hfI⟩
State after:
no goals

State before:
case intro.inl
ι : Type u_1
α : Type u_2
M✝ : Matroid α
B I✝ J X✝ X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e✝ f✝ : α
M : Matroid α
X : Set α
e f : α
I : Set α
hI : M.Basis' I X
he : e ∉ M.E
⊢ M.ModularPair (M.cl (insert e (M.cl I))) (M.cl (insert f (M.cl I)))
Tactic:
rw [← cl_inter_ground, insert_inter_of_not_mem he, cl_inter_ground]
State after:
case intro.inl
ι : Type u_1
α : Type u_2
M✝ : Matroid α
B I✝ J X✝ X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e✝ f✝ : α
M : Matroid α
X : Set α
e f : α
I : Set α
hI : M.Basis' I X
he : e ∉ M.E
⊢ M.ModularPair (M.cl (M.cl I)) (M.cl (insert f (M.cl I)))

State before:
case intro.inl
ι : Type u_1
α : Type u_2
M✝ : Matroid α
B I✝ J X✝ X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e✝ f✝ : α
M : Matroid α
X : Set α
e f : α
I : Set α
hI : M.Basis' I X
he : e ∉ M.E
⊢ M.ModularPair (M.cl (M.cl I)) (M.cl (insert f (M.cl I)))
Tactic:
exact modularPair_of_subset (M.cl_subset_cl (subset_insert _ _)) (M.cl_subset_ground _)
State after:
no goals

State before:
case intro.inr.inl
ι : Type u_1
α : Type u_2
M✝ : Matroid α
B I✝ J X✝ X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e✝ f✝ : α
M : Matroid α
X : Set α
e f : α
I : Set α
hI : M.Basis' I X
he : e ∈ M.E
hf : f ∉ M.E
⊢ M.ModularPair (M.cl (insert e (M.cl I))) (M.cl (insert f (M.cl I)))
Tactic:
rw [ModularPair.comm, ← cl_inter_ground, insert_inter_of_not_mem hf, cl_inter_ground]
State after:
case intro.inr.inl
ι : Type u_1
α : Type u_2
M✝ : Matroid α
B I✝ J X✝ X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e✝ f✝ : α
M : Matroid α
X : Set α
e f : α
I : Set α
hI : M.Basis' I X
he : e ∈ M.E
hf : f ∉ M.E
⊢ M.ModularPair (M.cl (M.cl I)) (M.cl (insert e (M.cl I)))

State before:
case intro.inr.inl
ι : Type u_1
α : Type u_2
M✝ : Matroid α
B I✝ J X✝ X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e✝ f✝ : α
M : Matroid α
X : Set α
e f : α
I : Set α
hI : M.Basis' I X
he : e ∈ M.E
hf : f ∉ M.E
⊢ M.ModularPair (M.cl (M.cl I)) (M.cl (insert e (M.cl I)))
Tactic:
exact modularPair_of_subset (M.cl_subset_cl (subset_insert _ _)) (M.cl_subset_ground _)
State after:
no goals

State before:
case intro.inr.inr.inl
ι : Type u_1
α : Type u_2
M✝ : Matroid α
B I✝ J X✝ X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e✝ f✝ : α
M : Matroid α
X : Set α
e f : α
I : Set α
hI : M.Basis' I X
he : e ∈ M.E
hf : f ∈ M.E
hfI : f ∈ M.cl I
⊢ M.ModularPair (M.cl (insert e (M.cl I))) (M.cl (insert f (M.cl I)))
Tactic:
rw [ModularPair.comm, insert_eq_of_mem hfI]
State after:
case intro.inr.inr.inl
ι : Type u_1
α : Type u_2
M✝ : Matroid α
B I✝ J X✝ X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e✝ f✝ : α
M : Matroid α
X : Set α
e f : α
I : Set α
hI : M.Basis' I X
he : e ∈ M.E
hf : f ∈ M.E
hfI : f ∈ M.cl I
⊢ M.ModularPair (M.cl (M.cl I)) (M.cl (insert e (M.cl I)))

State before:
case intro.inr.inr.inl
ι : Type u_1
α : Type u_2
M✝ : Matroid α
B I✝ J X✝ X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e✝ f✝ : α
M : Matroid α
X : Set α
e f : α
I : Set α
hI : M.Basis' I X
he : e ∈ M.E
hf : f ∈ M.E
hfI : f ∈ M.cl I
⊢ M.ModularPair (M.cl (M.cl I)) (M.cl (insert e (M.cl I)))
Tactic:
exact modularPair_of_subset (M.cl_subset_cl (subset_insert _ _)) (M.cl_subset_ground _)
State after:
no goals

State before:
case intro.inr.inr.inr.inl
ι : Type u_1
α : Type u_2
M✝ : Matroid α
B I✝ J X✝ X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e✝ f✝ : α
M : Matroid α
X : Set α
e f : α
I : Set α
hI : M.Basis' I X
he : e ∈ M.E
hf : f ∈ M.E
hfI : f ∉ M.cl I
hef : e ∈ M.cl (insert f I)
⊢ M.ModularPair (M.cl (insert e I)) (M.cl (insert f I))
Tactic:
refine modularPair_of_subset (M.cl_subset_cl_of_subset_cl ?_) (M.cl_subset_ground _)
State after:
case intro.inr.inr.inr.inl
ι : Type u_1
α : Type u_2
M✝ : Matroid α
B I✝ J X✝ X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e✝ f✝ : α
M : Matroid α
X : Set α
e f : α
I : Set α
hI : M.Basis' I X
he : e ∈ M.E
hf : f ∈ M.E
hfI : f ∉ M.cl I
hef : e ∈ M.cl (insert f I)
⊢ insert e I ⊆ M.cl (insert f I)

State before:
case intro.inr.inr.inr.inl
ι : Type u_1
α : Type u_2
M✝ : Matroid α
B I✝ J X✝ X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e✝ f✝ : α
M : Matroid α
X : Set α
e f : α
I : Set α
hI : M.Basis' I X
he : e ∈ M.E
hf : f ∈ M.E
hfI : f ∉ M.cl I
hef : e ∈ M.cl (insert f I)
⊢ insert e I ⊆ M.cl (insert f I)
Tactic:
exact insert_subset hef (M.subset_cl_of_subset (subset_insert _ _)
  (insert_subset hf hI.indep.subset_ground))
State after:
no goals

State before:
case intro.inr.inr.inr.inr.hi
ι : Type u_1
α : Type u_2
M✝ : Matroid α
B I✝ J X✝ X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e✝ f✝ : α
M : Matroid α
X : Set α
e f : α
I : Set α
hI : M.Basis' I X
he : e ∈ M.E
hf : f ∈ M.E
hfI : f ∉ M.cl I
hef : e ∉ M.cl (insert f I)
⊢ e ∈ M.E \ M.cl (insert f I) ∨ e ∈ insert f I
Tactic:
exact .inl ⟨he, hef⟩
State after:
no goals