Theorem: Matroid.Circuit.subset_cl_diff_singleton (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
e : α
⊢ C ⊆ M.cl (C \ {e})
Tactic:
by_cases he : e ∈ C
State after:
case pos
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
hC : M.Circuit C
e : α
he : e ∈ C
⊢ C ⊆ M.cl (C \ {e})

case neg
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
hC : M.Circuit C
e : α
he : e ∉ C
⊢ C ⊆ M.cl (C \ {e})

State before:
case neg
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
hC : M.Circuit C
e : α
he : e ∉ C
⊢ C ⊆ M.cl (C \ {e})
Tactic:
rw [diff_singleton_eq_self he]
State after:
case neg
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
hC : M.Circuit C
e : α
he : e ∉ C
⊢ C ⊆ M.cl C

State before:
case neg
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
hC : M.Circuit C
e : α
he : e ∉ C
⊢ C ⊆ M.cl C
Tactic:
exact M.subset_cl _
State after:
no goals

State before:
case pos
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
hC : M.Circuit C
e : α
he : e ∈ C
⊢ C ⊆ M.cl (C \ {e})
Tactic:
rw [(hC.diff_singleton_basis he).cl_eq_cl]
State after:
case pos
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
hC : M.Circuit C
e : α
he : e ∈ C
⊢ C ⊆ M.cl C

State before:
case pos
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
hC : M.Circuit C
e : α
he : e ∈ C
⊢ C ⊆ M.cl C
Tactic:
exact M.subset_cl _
State after:
no goals