α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
ha : ¬a ∈ s
h : insert a s ⊆ insert a t
x : α
hx : x ∈ s
⊢ x ∈ t
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
ha : ¬a ∈ s
⊢ insert a s ⊆ insert a t ↔ s ⊆ t
refine' ⟨fun h x hx => _, insert_subset_insert⟩
case inl
α : Type u
β : Type v
γ : Type w
ι : Sort x
b : α
s s₁ s₂ t t₁ t₂ u : Set α
x : α
hx : x ∈ s
ha : ¬x ∈ s
h : insert x s ⊆ insert x t
⊢ x ∈ t

case inr
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
ha : ¬a ∈ s
h : insert a s ⊆ insert a t
x : α
hx : x ∈ s
hxt : x ∈ t
⊢ x ∈ t
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
ha : ¬a ∈ s
h : insert a s ⊆ insert a t
x : α
hx : x ∈ s
⊢ x ∈ t
rcases h (subset_insert _ _ hx) with (rfl | hxt)
no goals
case inl
α : Type u
β : Type v
γ : Type w
ι : Sort x
b : α
s s₁ s₂ t t₁ t₂ u : Set α
x : α
hx : x ∈ s
ha : ¬x ∈ s
h : insert x s ⊆ insert x t
⊢ x ∈ t

case inr
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
ha : ¬a ∈ s
h : insert a s ⊆ insert a t
x : α
hx : x ∈ s
hxt : x ∈ t
⊢ x ∈ t
exacts [(ha hx).elim, hxt]