Theorem: Matroid.cl_eq_self_of_subset_singleton (Matroid/Simple.lean)

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.Simple
he : e ∈ M.E
hX : X ⊆ {e}
⊢ M.cl X = X
Tactic:
obtain (rfl | rfl) := subset_singleton_iff_eq.1 hX
State after:
case inl
α : Type u_1
M N : Matroid α
e f g : α
I P D : Set α
inst✝ : M.Simple
he : e ∈ M.E
hX : ∅ ⊆ {e}
⊢ M.cl ∅ = ∅

case inr
α : Type u_1
M N : Matroid α
e f g : α
I P D : Set α
inst✝ : M.Simple
he : e ∈ M.E
hX : {e} ⊆ {e}
⊢ M.cl {e} = {e}

State before:
case inr
α : Type u_1
M N : Matroid α
e f g : α
I P D : Set α
inst✝ : M.Simple
he : e ∈ M.E
hX : {e} ⊆ {e}
⊢ M.cl {e} = {e}
Tactic:
exact cl_singleton_eq he
State after:
no goals

State before:
case inl
α : Type u_1
M N : Matroid α
e f g : α
I P D : Set α
inst✝ : M.Simple
he : e ∈ M.E
hX : ∅ ⊆ {e}
⊢ M.cl ∅ = ∅
Tactic:
exact M.cl_empty_eq_empty
State after:
no goals