Theorem: Matroid.cl_union_eq_of_subset_coloops (Matroid/Loop.lean)

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 α
hK : K ⊆ M✶.cl ∅
⊢ M.cl (X ∪ K) = M.cl X ∪ K
Tactic:
rw [← cl_union_cl_left_eq]
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 α
hK : K ⊆ M✶.cl ∅
⊢ M.cl (M.cl X ∪ K) = M.cl X ∪ K

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 α
hK : K ⊆ M✶.cl ∅
⊢ M.cl (M.cl X ∪ K) = M.cl X ∪ K
Tactic:
refine' (M.subset_cl _).antisymm' fun e he ↦ _
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 α
hK : K ⊆ M✶.cl ∅
e : α
he : e ∈ M.cl (M.cl X ∪ K)
⊢ e ∈ M.cl X ∪ K

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 α
hK : K ⊆ M✶.cl ∅
e : α
he : e ∈ M.cl (M.cl X ∪ K)
⊢ e ∈ M.cl X ∪ K
Tactic:
obtain he' | ⟨C, hC, heC, hCss⟩ := (mem_cl_iff_mem_or_exists_circuit
  (union_subset (M.cl_subset_ground _) (hK.trans (M✶.cl_subset_ground _)))).1 he
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 X : Set α
hK : K ⊆ M✶.cl ∅
e : α
he : e ∈ M.cl (M.cl X ∪ K)
he' : e ∈ M.cl X ∪ K
⊢ e ∈ M.cl X ∪ K

case inr.intro.intro.intro
α : Type u_1
β : Type u_2
M N : Matroid α
e✝ f : α
B L L' I X✝ Y Z F C✝ K X : Set α
hK : K ⊆ M✶.cl ∅
e : α
he : e ∈ M.cl (M.cl X ∪ K)
C : Set α
hC : M.Circuit C
heC : e ∈ C
hCss : C ⊆ insert e (M.cl X ∪ K)
⊢ e ∈ M.cl X ∪ K

State before:
case inr.intro.intro.intro
α : Type u_1
β : Type u_2
M N : Matroid α
e✝ f : α
B L L' I X✝ Y Z F C✝ K X : Set α
hK : K ⊆ M✶.cl ∅
e : α
he : e ∈ M.cl (M.cl X ∪ K)
C : Set α
hC : M.Circuit C
heC : e ∈ C
hCss : C ⊆ insert e (M.cl X ∪ K)
hCX : C \ {e} ⊆ M.cl X
⊢ e ∈ M.cl X ∪ K
Tactic:
exact Or.inl (M.cl_subset_cl_of_subset_cl hCX (hC.mem_cl_diff_singleton_of_mem heC))
State after:
no goals

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 X : Set α
hK : K ⊆ M✶.cl ∅
e : α
he : e ∈ M.cl (M.cl X ∪ K)
he' : e ∈ M.cl X ∪ K
⊢ e ∈ M.cl X ∪ K
Tactic:
exact he'
State after:
no goals

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 α
hK : K ⊆ M✶.cl ∅
e : α
he : e ∈ M.cl (M.cl X ∪ K)
C : Set α
hC : M.Circuit C
heC : e ∈ C
hCss : C ⊆ insert e (M.cl X ∪ K)
⊢ C \ {e} ⊆ M.cl X
Tactic:
rw [diff_subset_iff, singleton_union]
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 α
hK : K ⊆ M✶.cl ∅
e : α
he : e ∈ M.cl (M.cl X ∪ K)
C : Set α
hC : M.Circuit C
heC : e ∈ C
hCss : C ⊆ insert e (M.cl X ∪ K)
⊢ C ⊆ insert e (M.cl X)

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 α
hK : K ⊆ M✶.cl ∅
e : α
he : e ∈ M.cl (M.cl X ∪ K)
C : Set α
hC : M.Circuit C
heC : e ∈ C
hCss : C ⊆ insert e (M.cl X ∪ K)
⊢ C ⊆ insert e (M.cl X)
Tactic:
refine (subset_inter hCss Subset.rfl).trans ?_
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 α
hK : K ⊆ M✶.cl ∅
e : α
he : e ∈ M.cl (M.cl X ∪ K)
C : Set α
hC : M.Circuit C
heC : e ∈ C
hCss : C ⊆ insert e (M.cl X ∪ K)
⊢ insert e (M.cl X ∪ K) ∩ C ⊆ insert e (M.cl X)

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 α
hK : K ⊆ M✶.cl ∅
e : α
he : e ∈ M.cl (M.cl X ∪ K)
C : Set α
hC : M.Circuit C
heC : e ∈ C
hCss : C ⊆ insert e (M.cl X ∪ K)
⊢ insert e (M.cl X ∪ K) ∩ C ⊆ insert e (M.cl X)
Tactic:
rintro f ⟨rfl | h1 | h2, h⟩
State after:
case intro.inl
α : Type u_1
β : Type u_2
M N : Matroid α
e f✝ : α
B L L' I X✝ Y Z F C✝ K X : Set α
hK : K ⊆ M✶.cl ∅
C : Set α
hC : M.Circuit C
f : α
h : f ∈ C
he : f ∈ M.cl (M.cl X ∪ K)
heC : f ∈ C
hCss : C ⊆ insert f (M.cl X ∪ K)
⊢ f ∈ insert f (M.cl X)

case intro.inr.inl
α : Type u_1
β : Type u_2
M N : Matroid α
e✝ f✝ : α
B L L' I X✝ Y Z F C✝ K X : Set α
hK : K ⊆ M✶.cl ∅
e : α
he : e ∈ M.cl (M.cl X ∪ K)
C : Set α
hC : M.Circuit C
heC : e ∈ C
hCss : C ⊆ insert e (M.cl X ∪ K)
f : α
h : f ∈ C
h1 : f ∈ M.cl X
⊢ f ∈ insert e (M.cl X)

case intro.inr.inr
α : Type u_1
β : Type u_2
M N : Matroid α
e✝ f✝ : α
B L L' I X✝ Y Z F C✝ K X : Set α
hK : K ⊆ M✶.cl ∅
e : α
he : e ∈ M.cl (M.cl X ∪ K)
C : Set α
hC : M.Circuit C
heC : e ∈ C
hCss : C ⊆ insert e (M.cl X ∪ K)
f : α
h : f ∈ C
h2 : f ∈ K
⊢ f ∈ insert e (M.cl X)

State before:
case intro.inr.inr
α : Type u_1
β : Type u_2
M N : Matroid α
e✝ f✝ : α
B L L' I X✝ Y Z F C✝ K X : Set α
hK : K ⊆ M✶.cl ∅
e : α
he : e ∈ M.cl (M.cl X ∪ K)
C : Set α
hC : M.Circuit C
heC : e ∈ C
hCss : C ⊆ insert e (M.cl X ∪ K)
f : α
h : f ∈ C
h2 : f ∈ K
⊢ f ∈ insert e (M.cl X)
Tactic:
exact (hC.not_coloop_of_mem h (hK h2)).elim
State after:
no goals

State before:
case intro.inl
α : Type u_1
β : Type u_2
M N : Matroid α
e f✝ : α
B L L' I X✝ Y Z F C✝ K X : Set α
hK : K ⊆ M✶.cl ∅
C : Set α
hC : M.Circuit C
f : α
h : f ∈ C
he : f ∈ M.cl (M.cl X ∪ K)
heC : f ∈ C
hCss : C ⊆ insert f (M.cl X ∪ K)
⊢ f ∈ insert f (M.cl X)
Tactic:
apply mem_insert
State after:
no goals

State before:
case intro.inr.inl
α : Type u_1
β : Type u_2
M N : Matroid α
e✝ f✝ : α
B L L' I X✝ Y Z F C✝ K X : Set α
hK : K ⊆ M✶.cl ∅
e : α
he : e ∈ M.cl (M.cl X ∪ K)
C : Set α
hC : M.Circuit C
heC : e ∈ C
hCss : C ⊆ insert e (M.cl X ∪ K)
f : α
h : f ∈ C
h1 : f ∈ M.cl X
⊢ f ∈ insert e (M.cl X)
Tactic:
exact Or.inr h1
State after:
no goals