[GOAL]
α : Type v
inst✝ : Small.{w, v} α
x y : Shrink α
w : ↑(equivShrink α).symm x = ↑(equivShrink α).symm y
⊢ x = y
[PROOFSTEP]
simpa using w
[GOAL]
α : Type v
inst✝ : Subsingleton α
⊢ Small.{w, v} α
[PROOFSTEP]
rcases isEmpty_or_nonempty α with ⟨⟩
[GOAL]
case inl
α : Type v
inst✝ : Subsingleton α
h✝ : IsEmpty α
⊢ Small.{w, v} α
[PROOFSTEP]
skip
[GOAL]
case inr
α : Type v
inst✝ : Subsingleton α
h✝ : Nonempty α
⊢ Small.{w, v} α
[PROOFSTEP]
skip
[GOAL]
case inl
α : Type v
inst✝ : Subsingleton α
h✝ : IsEmpty α
⊢ Small.{w, v} α
[PROOFSTEP]
apply small_map (Equiv.equivPEmpty α)
[GOAL]
case inr
α : Type v
inst✝ : Subsingleton α
h✝ : Nonempty α
⊢ Small.{w, v} α
[PROOFSTEP]
apply small_map Equiv.punitOfNonemptyOfSubsingleton
[GOAL]
α : Type ?u.2397
β : α → Type u_1
inst✝¹ : Small.{w, ?u.2397} α
inst✝ : ∀ (a : α), Small.{w, u_1} (β a)
a : α
⊢ β a ≃ Shrink (β (↑(equivShrink α).symm (↑(equivShrink α) a)))
[PROOFSTEP]
simpa using equivShrink (β a)
[GOAL]
α : Type ?u.2805
β : α → Type u_1
inst✝¹ : Small.{w, ?u.2805} α
inst✝ : ∀ (a : α), Small.{w, u_1} (β a)
a : α
⊢ β a ≃ Shrink (β (↑(equivShrink α).symm (↑(equivShrink α) a)))
[PROOFSTEP]
simpa using equivShrink (β a)
[GOAL]
S : Type u
e✝ : Type (max u v) ≃ S
a b : Set ((α : S) × ↑e✝.symm α)
e :
  (fun a =>
        { fst := Equiv.toFun e✝ (Set ((α : S) × ↑e✝.symm α)),
          snd :=
            cast (_ : Set ((α : S) × ↑e✝.symm α) = Equiv.invFun e✝ (Equiv.toFun e✝ (Set ((α : S) × ↑e✝.symm α)))) a })
      a =
    (fun a =>
        { fst := Equiv.toFun e✝ (Set ((α : S) × ↑e✝.symm α)),
          snd :=
            cast (_ : Set ((α : S) × ↑e✝.symm α) = Equiv.invFun e✝ (Equiv.toFun e✝ (Set ((α : S) × ↑e✝.symm α)))) a })
      b
⊢ a = b
[PROOFSTEP]
dsimp at e 
[GOAL]
S : Type u
e✝ : Type (max u v) ≃ S
a b : Set ((α : S) × ↑e✝.symm α)
e :
  { fst := ↑e✝ (Set ((α : S) × ↑e✝.symm α)),
      snd := cast (_ : Set ((α : S) × ↑e✝.symm α) = ↑e✝.symm (↑e✝ (Set ((α : S) × ↑e✝.symm α)))) a } =
    { fst := ↑e✝ (Set ((α : S) × ↑e✝.symm α)),
      snd := cast (_ : Set ((α : S) × ↑e✝.symm α) = ↑e✝.symm (↑e✝ (Set ((α : S) × ↑e✝.symm α)))) b }
⊢ a = b
[PROOFSTEP]
injection e with h₁ h₂
[GOAL]
S : Type u
e : Type (max u v) ≃ S
a b : Set ((α : S) × ↑e.symm α)
h₁ : ↑e (Set ((α : S) × ↑e.symm α)) = ↑e (Set ((α : S) × ↑e.symm α))
h₂ :
  cast (_ : Set ((α : S) × ↑e.symm α) = ↑e.symm (↑e (Set ((α : S) × ↑e.symm α)))) a =
    cast (_ : Set ((α : S) × ↑e.symm α) = ↑e.symm (↑e (Set ((α : S) × ↑e.symm α)))) b
⊢ a = b
[PROOFSTEP]
simpa using h₂
