[GOAL]
α : Type u_1
inst✝¹ : Add α
inst✝ : Small.{u_2, u_1} α
x y : Shrink α
⊢ ↑(equivShrink α).symm (x + y) = ↑(equivShrink α).symm x + ↑(equivShrink α).symm y
[PROOFSTEP]
rw [Equiv.add_def]
[GOAL]
α : Type u_1
inst✝¹ : Add α
inst✝ : Small.{u_2, u_1} α
x y : Shrink α
⊢ ↑(equivShrink α).symm (↑(equivShrink α).symm.symm (↑(equivShrink α).symm x + ↑(equivShrink α).symm y)) =
    ↑(equivShrink α).symm x + ↑(equivShrink α).symm y
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : Add α
inst✝ : Small.{u_2, u_1} α
x y : α
⊢ ↑(equivShrink α) (x + y) = ↑(equivShrink α) x + ↑(equivShrink α) y
[PROOFSTEP]
rw [Equiv.add_def]
[GOAL]
α : Type u_1
inst✝¹ : Add α
inst✝ : Small.{u_2, u_1} α
x y : α
⊢ ↑(equivShrink α) (x + y) =
    ↑(equivShrink α).symm.symm (↑(equivShrink α).symm (↑(equivShrink α) x) + ↑(equivShrink α).symm (↑(equivShrink α) y))
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : Mul α
inst✝ : Small.{u_2, u_1} α
x y : Shrink α
⊢ ↑(equivShrink α).symm (x * y) = ↑(equivShrink α).symm x * ↑(equivShrink α).symm y
[PROOFSTEP]
rw [Equiv.mul_def]
[GOAL]
α : Type u_1
inst✝¹ : Mul α
inst✝ : Small.{u_2, u_1} α
x y : Shrink α
⊢ ↑(equivShrink α).symm (↑(equivShrink α).symm.symm (↑(equivShrink α).symm x * ↑(equivShrink α).symm y)) =
    ↑(equivShrink α).symm x * ↑(equivShrink α).symm y
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : Mul α
inst✝ : Small.{u_2, u_1} α
x y : α
⊢ ↑(equivShrink α) (x * y) = ↑(equivShrink α) x * ↑(equivShrink α) y
[PROOFSTEP]
rw [Equiv.mul_def]
[GOAL]
α : Type u_1
inst✝¹ : Mul α
inst✝ : Small.{u_2, u_1} α
x y : α
⊢ ↑(equivShrink α) (x * y) =
    ↑(equivShrink α).symm.symm (↑(equivShrink α).symm (↑(equivShrink α) x) * ↑(equivShrink α).symm (↑(equivShrink α) y))
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : Sub α
inst✝ : Small.{u_2, u_1} α
x y : Shrink α
⊢ ↑(equivShrink α).symm (x - y) = ↑(equivShrink α).symm x - ↑(equivShrink α).symm y
[PROOFSTEP]
rw [Equiv.sub_def]
[GOAL]
α : Type u_1
inst✝¹ : Sub α
inst✝ : Small.{u_2, u_1} α
x y : Shrink α
⊢ ↑(equivShrink α).symm (↑(equivShrink α).symm.symm (↑(equivShrink α).symm x - ↑(equivShrink α).symm y)) =
    ↑(equivShrink α).symm x - ↑(equivShrink α).symm y
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : Sub α
inst✝ : Small.{u_2, u_1} α
x y : α
⊢ ↑(equivShrink α) (x - y) = ↑(equivShrink α) x - ↑(equivShrink α) y
[PROOFSTEP]
rw [Equiv.sub_def]
[GOAL]
α : Type u_1
inst✝¹ : Sub α
inst✝ : Small.{u_2, u_1} α
x y : α
⊢ ↑(equivShrink α) (x - y) =
    ↑(equivShrink α).symm.symm (↑(equivShrink α).symm (↑(equivShrink α) x) - ↑(equivShrink α).symm (↑(equivShrink α) y))
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : Div α
inst✝ : Small.{u_2, u_1} α
x y : Shrink α
⊢ ↑(equivShrink α).symm (x / y) = ↑(equivShrink α).symm x / ↑(equivShrink α).symm y
[PROOFSTEP]
rw [Equiv.div_def]
[GOAL]
α : Type u_1
inst✝¹ : Div α
inst✝ : Small.{u_2, u_1} α
x y : Shrink α
⊢ ↑(equivShrink α).symm (↑(equivShrink α).symm.symm (↑(equivShrink α).symm x / ↑(equivShrink α).symm y)) =
    ↑(equivShrink α).symm x / ↑(equivShrink α).symm y
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : Div α
inst✝ : Small.{u_2, u_1} α
x y : α
⊢ ↑(equivShrink α) (x / y) = ↑(equivShrink α) x / ↑(equivShrink α) y
[PROOFSTEP]
rw [Equiv.div_def]
[GOAL]
α : Type u_1
inst✝¹ : Div α
inst✝ : Small.{u_2, u_1} α
x y : α
⊢ ↑(equivShrink α) (x / y) =
    ↑(equivShrink α).symm.symm (↑(equivShrink α).symm (↑(equivShrink α) x) / ↑(equivShrink α).symm (↑(equivShrink α) y))
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : Neg α
inst✝ : Small.{u_2, u_1} α
x : Shrink α
⊢ ↑(equivShrink α).symm (-x) = -↑(equivShrink α).symm x
[PROOFSTEP]
rw [Equiv.neg_def]
[GOAL]
α : Type u_1
inst✝¹ : Neg α
inst✝ : Small.{u_2, u_1} α
x : Shrink α
⊢ ↑(equivShrink α).symm (↑(equivShrink α).symm.symm (-↑(equivShrink α).symm x)) = -↑(equivShrink α).symm x
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : Neg α
inst✝ : Small.{u_2, u_1} α
x : α
⊢ ↑(equivShrink α) (-x) = -↑(equivShrink α) x
[PROOFSTEP]
rw [Equiv.neg_def]
[GOAL]
α : Type u_1
inst✝¹ : Neg α
inst✝ : Small.{u_2, u_1} α
x : α
⊢ ↑(equivShrink α) (-x) = ↑(equivShrink α).symm.symm (-↑(equivShrink α).symm (↑(equivShrink α) x))
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : Inv α
inst✝ : Small.{u_2, u_1} α
x : Shrink α
⊢ ↑(equivShrink α).symm x⁻¹ = (↑(equivShrink α).symm x)⁻¹
[PROOFSTEP]
rw [Equiv.inv_def]
[GOAL]
α : Type u_1
inst✝¹ : Inv α
inst✝ : Small.{u_2, u_1} α
x : Shrink α
⊢ ↑(equivShrink α).symm (↑(equivShrink α).symm.symm (↑(equivShrink α).symm x)⁻¹) = (↑(equivShrink α).symm x)⁻¹
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : Inv α
inst✝ : Small.{u_2, u_1} α
x : α
⊢ ↑(equivShrink α) x⁻¹ = (↑(equivShrink α) x)⁻¹
[PROOFSTEP]
rw [Equiv.inv_def]
[GOAL]
α : Type u_1
inst✝¹ : Inv α
inst✝ : Small.{u_2, u_1} α
x : α
⊢ ↑(equivShrink α) x⁻¹ = ↑(equivShrink α).symm.symm (↑(equivShrink α).symm (↑(equivShrink α) x))⁻¹
[PROOFSTEP]
simp
