Theorem: translationHomeo.toFun.def (src/MainTheorem.lean)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : E
⊢ ⇑(translationHomeo x) = fun x_1 => x_1 + x
Tactic:
unfold translationHomeo
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : E
⊢ ⇑{ toEquiv := { toFun := fun x_1 => x_1 + x, invFun := fun x_1 => x_1 + -x, left_inv := ⋯, right_inv := ⋯ },
        continuous_toFun := ⋯, continuous_invFun := ⋯ } =
    fun x_1 => x_1 + x

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : E
⊢ ⇑{ toEquiv := { toFun := fun x_1 => x_1 + x, invFun := fun x_1 => x_1 + -x, left_inv := ⋯, right_inv := ⋯ },
        continuous_toFun := ⋯, continuous_invFun := ⋯ } =
    fun x_1 => x_1 + x
Tactic:
simp
State after:
no goals