case a
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type u_1
s t : Set α
h : s ⊆ t
inst✝ : DecidablePred fun x => x ∈ s
x : ↑t
hx : ↑x ∈ s
⊢ ↑(Set.sumDiffSubset h) (↑(Set.sumDiffSubset h).symm x) =
    ↑(Set.sumDiffSubset h) (Sum.inl { val := ↑x, property := hx })
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type u_1
s t : Set α
h : s ⊆ t
inst✝ : DecidablePred fun x => x ∈ s
x : ↑t
hx : ↑x ∈ s
⊢ ↑(Set.sumDiffSubset h).symm x = Sum.inl { val := ↑x, property := hx }
apply (Equiv.Set.sumDiffSubset h).injective
case a
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type u_1
s t : Set α
h : s ⊆ t
inst✝ : DecidablePred fun x => x ∈ s
x : ↑t
hx : ↑x ∈ s
⊢ x = inclusion h { val := ↑x, property := hx }
case a
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type u_1
s t : Set α
h : s ⊆ t
inst✝ : DecidablePred fun x => x ∈ s
x : ↑t
hx : ↑x ∈ s
⊢ ↑(Set.sumDiffSubset h) (↑(Set.sumDiffSubset h).symm x) =
    ↑(Set.sumDiffSubset h) (Sum.inl { val := ↑x, property := hx })
simp only [apply_symm_apply, sumDiffSubset_apply_inl]
no goals
case a
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type u_1
s t : Set α
h : s ⊆ t
inst✝ : DecidablePred fun x => x ∈ s
x : ↑t
hx : ↑x ∈ s
⊢ x = inclusion h { val := ↑x, property := hx }
exact Subtype.eq rfl