α : Type u_1
β : Type ?u.43357
x : α
s t : Set α
hst : s ≤ t
h2t : t ≤ insert x s
⊢ t = s ∨ t = insert x s
α : Type u_1
β : Type ?u.43357
x : α
s : Set α
⊢ s ⩿ insert x s
refine' wcovby_of_eq_or_eq (subset_insert x s) fun t hst h2t => _
case pos
α : Type u_1
β : Type ?u.43357
x : α
s t : Set α
hst : s ≤ t
h2t : t ≤ insert x s
h : x ∈ t
⊢ t = s ∨ t = insert x s

case neg
α : Type u_1
β : Type ?u.43357
x : α
s t : Set α
hst : s ≤ t
h2t : t ≤ insert x s
h : ¬x ∈ t
⊢ t = s ∨ t = insert x s
α : Type u_1
β : Type ?u.43357
x : α
s t : Set α
hst : s ≤ t
h2t : t ≤ insert x s
⊢ t = s ∨ t = insert x s
by_cases h : x ∈ t
no goals
case pos
α : Type u_1
β : Type ?u.43357
x : α
s t : Set α
hst : s ≤ t
h2t : t ≤ insert x s
h : x ∈ t
⊢ t = s ∨ t = insert x s
exact Or.inr (subset_antisymm h2t <| insert_subset.mpr ⟨h, hst⟩)
case neg
α : Type u_1
β : Type ?u.43357
x : α
s t : Set α
hst : s ≤ t
h2t : t ≤ insert x s
h : ¬x ∈ t
⊢ t ⊆ s
case neg
α : Type u_1
β : Type ?u.43357
x : α
s t : Set α
hst : s ≤ t
h2t : t ≤ insert x s
h : ¬x ∈ t
⊢ t = s ∨ t = insert x s
refine' Or.inl (subset_antisymm _ hst)
no goals
case neg
α : Type u_1
β : Type ?u.43357
x : α
s t : Set α
hst : s ≤ t
h2t : t ≤ insert x s
h : ¬x ∈ t
⊢ t ⊆ s
rwa [← diff_singleton_eq_self h, diff_singleton_subset_iff]