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.inr { val := ↑x, property := (_ : ↑x ∈ t ∧ ¬↑x ∈ s) })
α✝ : 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.inr { val := ↑x, property := (_ : ↑x ∈ t ∧ ¬↑x ∈ s) }
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 (_ : t \ s ⊆ t) { val := ↑x, property := (_ : ↑x ∈ t ∧ ¬↑x ∈ s) }
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.inr { val := ↑x, property := (_ : ↑x ∈ t ∧ ¬↑x ∈ s) })
simp only [apply_symm_apply, sumDiffSubset_apply_inr]
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 (_ : t \ s ⊆ t) { val := ↑x, property := (_ : ↑x ∈ t ∧ ¬↑x ∈ s) }
exact Subtype.eq rfl