Theorem: Matroid.Circuit.subset_cl_diff_subsingleton (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
Z : Set α
hZ : Z.encard ≤ 1
⊢ C ⊆ M.cl (C \ Z)
Tactic:
obtain (rfl | ⟨x, rfl⟩) := encard_le_one_iff_eq.1 hZ
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
hZ : ∅.encard ≤ 1
⊢ C ⊆ M.cl (C \ ∅)

case inr.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x✝ y : α
hC : M.Circuit C
x : α
hZ : {x}.encard ≤ 1
⊢ C ⊆ M.cl (C \ {x})

State before:
case inr.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x✝ y : α
hC : M.Circuit C
x : α
hZ : {x}.encard ≤ 1
⊢ C ⊆ M.cl (C \ {x})
Tactic:
exact hC.subset_cl_diff_singleton _
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
hZ : ∅.encard ≤ 1
⊢ C ⊆ M.cl (C \ ∅)
Tactic:
rw [diff_empty]
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
hZ : ∅.encard ≤ 1
⊢ C ⊆ M.cl C

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
hZ : ∅.encard ≤ 1
⊢ C ⊆ M.cl C
Tactic:
apply M.subset_cl _
State after:
no goals