Theorem: Matroid.Circuit.cocircuit_disjoint_or_nontrivial_inter (Matroid/Circuit.lean)

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
B : Set α
hC : M.Circuit C
hK : M.Cocircuit K
⊢ Disjoint C K ∨ (C ∩ K).Nontrivial
Tactic:
simp_rw [or_iff_not_imp_left, not_disjoint_iff]
State after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
B : Set α
hC : M.Circuit C
hK : M.Cocircuit K
⊢ (∃ x ∈ C, x ∈ K) → (C ∩ K).Nontrivial

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
B : Set α
hC : M.Circuit C
hK : M.Cocircuit K
⊢ (∃ x ∈ C, x ∈ K) → (C ∩ K).Nontrivial
Tactic:
rintro ⟨e, heC, heK⟩
State after:
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
B : Set α
hC : M.Circuit C
hK : M.Cocircuit K
e : α
heC : e ∈ C
heK : e ∈ K
⊢ (C ∩ K).Nontrivial

State before:
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
B : Set α
hC : M.Circuit C
hK : M.Cocircuit K
e : α
heC : e ∈ C
heK : e ∈ K
⊢ (C ∩ K).Nontrivial
Tactic:
simp_rw [nontrivial_iff_ne_singleton <| show e ∈ C ∩ K from ⟨heC, heK⟩]
State after:
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
B : Set α
hC : M.Circuit C
hK : M.Cocircuit K
e : α
heC : e ∈ C
heK : e ∈ K
⊢ C ∩ K ≠ {e}

State before:
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
B : Set α
hC : M.Circuit C
hK : M.Cocircuit K
e : α
heC : e ∈ C
heK : e ∈ K
⊢ C ∩ K ≠ {e}
Tactic:
intro he
State after:
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
B : Set α
hC : M.Circuit C
hK : M.Cocircuit K
e : α
heC : e ∈ C
heK : e ∈ K
he : C ∩ K = {e}
⊢ False

State before:
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
B : Set α
hC : M.Circuit C
hK : M.Cocircuit K
e : α
heC : e ∈ C
heK : e ∈ K
he : C ∩ K = {e}
⊢ False
Tactic:
simp_rw [cocircuit_iff_mem_minimals_compl_nonspanning, mem_minimals_iff_forall_ssubset_not_mem,
  mem_setOf, not_not] at hK
State after:
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
B : Set α
hC : M.Circuit C
e : α
heC : e ∈ C
heK : e ∈ K
he : C ∩ K = {e}
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃y : Set α⦄, y ⊂ K → M.Spanning (M.E \ y)
⊢ False

State before:
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
B : Set α
hC : M.Circuit C
e : α
heC : e ∈ C
heK : e ∈ K
he : C ∩ K = {e}
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃y : Set α⦄, y ⊂ K → M.Spanning (M.E \ y)
⊢ False
Tactic:
have' hKe := hK.2 (y := K \ {e}) (diff_singleton_sSubset.2 (he.symm.subset rfl).2)
State after:
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
B : Set α
hC : M.Circuit C
e : α
heC : e ∈ C
heK : e ∈ K
he : C ∩ K = {e}
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃y : Set α⦄, y ⊂ K → M.Spanning (M.E \ y)
hKe : M.Spanning (M.E \ (K \ {e}))
⊢ False

State before:
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
B : Set α
hC : M.Circuit C
e : α
heC : e ∈ C
heK : e ∈ K
he : C ∩ K = {e}
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃y : Set α⦄, y ⊂ K → M.Spanning (M.E \ y)
hKe : M.Spanning (M.E \ (K \ {e}))
⊢ False
Tactic:
apply hK.1
State after:
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
B : Set α
hC : M.Circuit C
e : α
heC : e ∈ C
heK : e ∈ K
he : C ∩ K = {e}
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃y : Set α⦄, y ⊂ K → M.Spanning (M.E \ y)
hKe : M.Spanning (M.E \ (K \ {e}))
⊢ M.Spanning (M.E \ K)

State before:
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
B : Set α
hC : M.Circuit C
e : α
heC : e ∈ C
heK : e ∈ K
he : C ∩ K = {e}
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃y : Set α⦄, y ⊂ K → M.Spanning (M.E \ y)
hKe : M.Spanning (M.E \ (K \ {e}))
⊢ M.Spanning (M.E \ K)
Tactic:
rw [spanning_iff_ground_subset_cl]
State after:
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
B : Set α
hC : M.Circuit C
e : α
heC : e ∈ C
heK : e ∈ K
he : C ∩ K = {e}
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃y : Set α⦄, y ⊂ K → M.Spanning (M.E \ y)
hKe : M.Spanning (M.E \ (K \ {e}))
⊢ M.E ⊆ M.cl (M.E \ K)

State before:
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
B : Set α
hC : M.Circuit C
e : α
heC : e ∈ C
heK : e ∈ K
he : C ∩ K = {e}
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃y : Set α⦄, y ⊂ K → M.Spanning (M.E \ y)
hKe : M.Spanning (M.E \ (K \ {e}))
⊢ M.E ⊆ M.cl (M.E \ K)
Tactic:
nth_rw 1 [← hKe.cl_eq, diff_diff_eq_sdiff_union]
State after:
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
B : Set α
hC : M.Circuit C
e : α
heC : e ∈ C
heK : e ∈ K
he : C ∩ K = {e}
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃y : Set α⦄, y ⊂ K → M.Spanning (M.E \ y)
hKe : M.Spanning (M.E \ (K \ {e}))
⊢ M.cl (M.E \ K ∪ {e}) ⊆ M.cl (M.E \ K)

case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
B : Set α
hC : M.Circuit C
e : α
heC : e ∈ C
heK : e ∈ K
he : C ∩ K = {e}
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃y : Set α⦄, y ⊂ K → M.Spanning (M.E \ y)
hKe : M.Spanning (M.E \ (K \ {e}))
⊢ {e} ⊆ M.E

State before:
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
B : Set α
hC : M.Circuit C
e : α
heC : e ∈ C
heK : e ∈ K
he : C ∩ K = {e}
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃y : Set α⦄, y ⊂ K → M.Spanning (M.E \ y)
hKe : M.Spanning (M.E \ (K \ {e}))
⊢ {e} ⊆ M.E
Tactic:
rw [← he]
State after:
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
B : Set α
hC : M.Circuit C
e : α
heC : e ∈ C
heK : e ∈ K
he : C ∩ K = {e}
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃y : Set α⦄, y ⊂ K → M.Spanning (M.E \ y)
hKe : M.Spanning (M.E \ (K \ {e}))
⊢ C ∩ K ⊆ M.E

State before:
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
B : Set α
hC : M.Circuit C
e : α
heC : e ∈ C
heK : e ∈ K
he : C ∩ K = {e}
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃y : Set α⦄, y ⊂ K → M.Spanning (M.E \ y)
hKe : M.Spanning (M.E \ (K \ {e}))
⊢ C ∩ K ⊆ M.E
Tactic:
exact inter_subset_left.trans hC.subset_ground
State after:
no goals

State before:
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
B : Set α
hC : M.Circuit C
e : α
heC : e ∈ C
heK : e ∈ K
he : C ∩ K = {e}
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃y : Set α⦄, y ⊂ K → M.Spanning (M.E \ y)
hKe : M.Spanning (M.E \ (K \ {e}))
⊢ M.cl (M.E \ K ∪ {e}) ⊆ M.cl (M.E \ K)
Tactic:
refine (M.cl_subset_cl (subset_union_left (t := C))).trans ?_
State after:
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
B : Set α
hC : M.Circuit C
e : α
heC : e ∈ C
heK : e ∈ K
he : C ∩ K = {e}
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃y : Set α⦄, y ⊂ K → M.Spanning (M.E \ y)
hKe : M.Spanning (M.E \ (K \ {e}))
⊢ M.cl (M.E \ K ∪ {e} ∪ C) ⊆ M.cl (M.E \ K)

State before:
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
B : Set α
hC : M.Circuit C
e : α
heC : e ∈ C
heK : e ∈ K
he : C ∩ K = {e}
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃y : Set α⦄, y ⊂ K → M.Spanning (M.E \ y)
hKe : M.Spanning (M.E \ (K \ {e}))
⊢ M.cl (M.E \ K ∪ {e} ∪ C) ⊆ M.cl (M.E \ K)
Tactic:
rw [union_assoc, singleton_union, insert_eq_of_mem heC, ← cl_union_cl_right_eq,
  ← hC.cl_diff_singleton_eq_cl e, cl_union_cl_right_eq, union_eq_self_of_subset_right]
State after:
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
B : Set α
hC : M.Circuit C
e : α
heC : e ∈ C
heK : e ∈ K
he : C ∩ K = {e}
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃y : Set α⦄, y ⊂ K → M.Spanning (M.E \ y)
hKe : M.Spanning (M.E \ (K \ {e}))
⊢ C \ {e} ⊆ M.E \ K

State before:
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
B : Set α
hC : M.Circuit C
e : α
heC : e ∈ C
heK : e ∈ K
he : C ∩ K = {e}
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃y : Set α⦄, y ⊂ K → M.Spanning (M.E \ y)
hKe : M.Spanning (M.E \ (K \ {e}))
⊢ C \ {e} ⊆ M.E \ K
Tactic:
rw [← he, diff_self_inter]
State after:
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
B : Set α
hC : M.Circuit C
e : α
heC : e ∈ C
heK : e ∈ K
he : C ∩ K = {e}
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃y : Set α⦄, y ⊂ K → M.Spanning (M.E \ y)
hKe : M.Spanning (M.E \ (K \ {e}))
⊢ C \ K ⊆ M.E \ K

State before:
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
B : Set α
hC : M.Circuit C
e : α
heC : e ∈ C
heK : e ∈ K
he : C ∩ K = {e}
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃y : Set α⦄, y ⊂ K → M.Spanning (M.E \ y)
hKe : M.Spanning (M.E \ (K \ {e}))
⊢ C \ K ⊆ M.E \ K
Tactic:
exact diff_subset_diff_left hC.subset_ground
State after:
no goals