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

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
hC₁ : M.Circuit C₁
hC₂ : M.Circuit C₂
h : C₁ ≠ C₂
e : α
⊢ ∃ C, M.Circuit C ∧ C ⊆ (C₁ ∪ C₂) \ {e}
Tactic:
have hne : (C₁ \ C₂).Nonempty := by
  rw [nonempty_iff_ne_empty, Ne, diff_eq_empty]
  exact fun hss ↦ h (hC₁.eq_of_subset_circuit hC₂ hss)
State after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
hC₁ : M.Circuit C₁
hC₂ : M.Circuit C₂
h : C₁ ≠ C₂
e : α
hne : (C₁ \ C₂).Nonempty
⊢ ∃ C, M.Circuit C ∧ C ⊆ (C₁ ∪ C₂) \ {e}

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
hC₁ : M.Circuit C₁
hC₂ : M.Circuit C₂
h : C₁ ≠ C₂
e : α
hne : (C₁ \ C₂).Nonempty
⊢ ∃ C, M.Circuit C ∧ C ⊆ (C₁ ∪ C₂) \ {e}
Tactic:
obtain (he₁ | he₁) := em (e ∈ C₁)
State after:
case inl
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
hC₁ : M.Circuit C₁
hC₂ : M.Circuit C₂
h : C₁ ≠ C₂
e : α
hne : (C₁ \ C₂).Nonempty
he₁ : e ∈ C₁
⊢ ∃ C, M.Circuit C ∧ C ⊆ (C₁ ∪ C₂) \ {e}

case inr
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
hC₁ : M.Circuit C₁
hC₂ : M.Circuit C₂
h : C₁ ≠ C₂
e : α
hne : (C₁ \ C₂).Nonempty
he₁ : e ∉ C₁
⊢ ∃ C, M.Circuit C ∧ C ⊆ (C₁ ∪ C₂) \ {e}

State before:
case inr
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
hC₁ : M.Circuit C₁
hC₂ : M.Circuit C₂
h : C₁ ≠ C₂
e : α
hne : (C₁ \ C₂).Nonempty
he₁ : e ∉ C₁
⊢ ∃ C, M.Circuit C ∧ C ⊆ (C₁ ∪ C₂) \ {e}
Tactic:
exact ⟨C₁, hC₁, subset_diff_singleton subset_union_left he₁⟩
State after:
no goals

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
hC₁ : M.Circuit C₁
hC₂ : M.Circuit C₂
h : C₁ ≠ C₂
e : α
⊢ (C₁ \ C₂).Nonempty
Tactic:
rw [nonempty_iff_ne_empty, Ne, diff_eq_empty]
State after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
hC₁ : M.Circuit C₁
hC₂ : M.Circuit C₂
h : C₁ ≠ C₂
e : α
⊢ ¬C₁ ⊆ C₂

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
hC₁ : M.Circuit C₁
hC₂ : M.Circuit C₂
h : C₁ ≠ C₂
e : α
⊢ ¬C₁ ⊆ C₂
Tactic:
exact fun hss ↦ h (hC₁.eq_of_subset_circuit hC₂ hss)
State after:
no goals

State before:
case inl
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
hC₁ : M.Circuit C₁
hC₂ : M.Circuit C₂
h : C₁ ≠ C₂
e : α
hne : (C₁ \ C₂).Nonempty
he₁ : e ∈ C₁
⊢ ∃ C, M.Circuit C ∧ C ⊆ (C₁ ∪ C₂) \ {e}
Tactic:
obtain (he₂ | he₂) := em (e ∈ C₂)
State after:
case inl.inl
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
hC₁ : M.Circuit C₁
hC₂ : M.Circuit C₂
h : C₁ ≠ C₂
e : α
hne : (C₁ \ C₂).Nonempty
he₁ : e ∈ C₁
he₂ : e ∈ C₂
⊢ ∃ C, M.Circuit C ∧ C ⊆ (C₁ ∪ C₂) \ {e}

case inl.inr
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
hC₁ : M.Circuit C₁
hC₂ : M.Circuit C₂
h : C₁ ≠ C₂
e : α
hne : (C₁ \ C₂).Nonempty
he₁ : e ∈ C₁
he₂ : e ∉ C₂
⊢ ∃ C, M.Circuit C ∧ C ⊆ (C₁ ∪ C₂) \ {e}

State before:
case inl.inr
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
hC₁ : M.Circuit C₁
hC₂ : M.Circuit C₂
h : C₁ ≠ C₂
e : α
hne : (C₁ \ C₂).Nonempty
he₁ : e ∈ C₁
he₂ : e ∉ C₂
⊢ ∃ C, M.Circuit C ∧ C ⊆ (C₁ ∪ C₂) \ {e}
Tactic:
exact ⟨C₂, hC₂, subset_diff_singleton subset_union_right he₂⟩
State after:
no goals

State before:
case inl.inl
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
hC₁ : M.Circuit C₁
hC₂ : M.Circuit C₂
h : C₁ ≠ C₂
e : α
hne : (C₁ \ C₂).Nonempty
he₁ : e ∈ C₁
he₂ : e ∈ C₂
⊢ ∃ C, M.Circuit C ∧ C ⊆ (C₁ ∪ C₂) \ {e}
Tactic:
obtain ⟨C, h⟩ :=  hC₁.strong_elimination hC₂ ⟨he₁,he₂⟩ hne.some_mem
State after:
case inl.inl.intro
α : Type u_1
M : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e✝ f x y : α
hC₁ : M.Circuit C₁
hC₂ : M.Circuit C₂
h✝ : C₁ ≠ C₂
e : α
hne : (C₁ \ C₂).Nonempty
he₁ : e ∈ C₁
he₂ : e ∈ C₂
C : Set α
h : M.Circuit C ∧ C ⊆ (C₁ ∪ C₂) \ {e} ∧ hne.some ∈ C
⊢ ∃ C, M.Circuit C ∧ C ⊆ (C₁ ∪ C₂) \ {e}

State before:
case inl.inl.intro
α : Type u_1
M : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e✝ f x y : α
hC₁ : M.Circuit C₁
hC₂ : M.Circuit C₂
h✝ : C₁ ≠ C₂
e : α
hne : (C₁ \ C₂).Nonempty
he₁ : e ∈ C₁
he₂ : e ∈ C₂
C : Set α
h : M.Circuit C ∧ C ⊆ (C₁ ∪ C₂) \ {e} ∧ hne.some ∈ C
⊢ ∃ C, M.Circuit C ∧ C ⊆ (C₁ ∪ C₂) \ {e}
Tactic:
exact ⟨C, h.1, h.2.1⟩
State after:
no goals