α : Type u_1
β : Type ?u.885
q₁ q₂ : Semiquot α
h : q₁.s = q₂.s
⊢ q₁ = q₂
α : Type u_1
β : Type ?u.885
q₁ q₂ : Semiquot α
⊢ q₁ = q₂ ↔ q₁.s = q₂.s
refine' ⟨congr_arg _, fun h => _⟩
case mk'
α : Type u_1
β : Type ?u.885
q₂ : Semiquot α
s✝ : Set α
v₁ : Trunc ↑s✝
h : { s := s✝, val := v₁ }.s = q₂.s
⊢ { s := s✝, val := v₁ } = q₂
α : Type u_1
β : Type ?u.885
q₁ q₂ : Semiquot α
h : q₁.s = q₂.s
⊢ q₁ = q₂
cases' q₁ with _ v₁
case mk'.mk'
α : Type u_1
β : Type ?u.885
s✝¹ : Set α
v₁ : Trunc ↑s✝¹
s✝ : Set α
v₂ : Trunc ↑s✝
h : { s := s✝¹, val := v₁ }.s = { s := s✝, val := v₂ }.s
⊢ { s := s✝¹, val := v₁ } = { s := s✝, val := v₂ }
case mk'
α : Type u_1
β : Type ?u.885
q₂ : Semiquot α
s✝ : Set α
v₁ : Trunc ↑s✝
h : { s := s✝, val := v₁ }.s = q₂.s
⊢ { s := s✝, val := v₁ } = q₂
cases' q₂ with _ v₂
case mk'.mk'.h.e_3
α : Type u_1
β : Type ?u.885
s✝¹ : Set α
v₁ : Trunc ↑s✝¹
s✝ : Set α
v₂ : Trunc ↑s✝
h : { s := s✝¹, val := v₁ }.s = { s := s✝, val := v₂ }.s
⊢ HEq v₁ v₂
case mk'.mk'
α : Type u_1
β : Type ?u.885
s✝¹ : Set α
v₁ : Trunc ↑s✝¹
s✝ : Set α
v₂ : Trunc ↑s✝
h : { s := s✝¹, val := v₁ }.s = { s := s✝, val := v₂ }.s
⊢ { s := s✝¹, val := v₁ } = { s := s✝, val := v₂ }
congr
no goals
case mk'.mk'.h.e_3
α : Type u_1
β : Type ?u.885
s✝¹ : Set α
v₁ : Trunc ↑s✝¹
s✝ : Set α
v₂ : Trunc ↑s✝
h : { s := s✝¹, val := v₁ }.s = { s := s✝, val := v₂ }.s
⊢ HEq v₁ v₂
exact Subsingleton.helim (congrArg Trunc (congrArg Set.Elem h)) v₁ v₂