Theorem: Set.diff_ssubset (Matroid/ForMathlib/Set.lean)

State before:
α : Type u_1
ι : Type u_2
s t : Set α
hst : s ⊆ t
hs : s.Nonempty
⊢ t \ s ⊂ t
Tactic:
refine diff_subset.ssubset_of_ne fun h_eq ↦ ?_
State after:
α : Type u_1
ι : Type u_2
s t : Set α
hst : s ⊆ t
hs : s.Nonempty
h_eq : t \ s = t
⊢ False

State before:
α : Type u_1
ι : Type u_2
s t : Set α
hst : s ⊆ t
hs : s.Nonempty
h_eq : t \ s = t
⊢ False
Tactic:
rw [sdiff_eq_left, disjoint_iff_inter_eq_empty, inter_eq_self_of_subset_right hst] at h_eq
State after:
α : Type u_1
ι : Type u_2
s t : Set α
hst : s ⊆ t
hs : s.Nonempty
h_eq : s = ∅
⊢ False

State before:
α : Type u_1
ι : Type u_2
s t : Set α
hst : s ⊆ t
hs : s.Nonempty
h_eq : s = ∅
⊢ False
Tactic:
simp [h_eq] at hs
State after:
no goals