case h
𝕜 : Type u_3
V : Type u_1
V₁ : Type ?u.1896593
V₂ : Type ?u.1896596
V₃ : Type ?u.1896599
V₄ : Type ?u.1896602
P₁ : Type ?u.1896605
P : Type u_2
P₂ : Type ?u.1896611
P₃ : Type ?u.1896614
P₄ : Type ?u.1896617
inst✝²¹ : NormedField 𝕜
inst✝²⁰ : SeminormedAddCommGroup V
inst✝¹⁹ : SeminormedAddCommGroup V₁
inst✝¹⁸ : SeminormedAddCommGroup V₂
inst✝¹⁷ : SeminormedAddCommGroup V₃
inst✝¹⁶ : SeminormedAddCommGroup V₄
inst✝¹⁵ : NormedSpace 𝕜 V
inst✝¹⁴ : NormedSpace 𝕜 V₁
inst✝¹³ : NormedSpace 𝕜 V₂
inst✝¹² : NormedSpace 𝕜 V₃
inst✝¹¹ : NormedSpace 𝕜 V₄
inst✝¹⁰ : PseudoMetricSpace P
inst✝⁹ : MetricSpace P₁
inst✝⁸ : PseudoMetricSpace P₂
inst✝⁷ : PseudoMetricSpace P₃
inst✝⁶ : PseudoMetricSpace P₄
inst✝⁵ : NormedAddTorsor V P
inst✝⁴ : NormedAddTorsor V₁ P₁
inst✝³ : NormedAddTorsor V₂ P₂
inst✝² : NormedAddTorsor V₃ P₃
inst✝¹ : NormedAddTorsor V₄ P₄
e : P ≃ᵃⁱ[𝕜] P₂
α : Type ?u.1897141
inst✝ : TopologicalSpace α
p : P
x✝ : V
⊢ ↑(symm (constVSub 𝕜 p)) x✝ =
    ↑(trans (LinearIsometryEquiv.toAffineIsometryEquiv (LinearIsometryEquiv.neg 𝕜)) (vaddConst 𝕜 p)) x✝
𝕜 : Type u_3
V : Type u_1
V₁ : Type ?u.1896593
V₂ : Type ?u.1896596
V₃ : Type ?u.1896599
V₄ : Type ?u.1896602
P₁ : Type ?u.1896605
P : Type u_2
P₂ : Type ?u.1896611
P₃ : Type ?u.1896614
P₄ : Type ?u.1896617
inst✝²¹ : NormedField 𝕜
inst✝²⁰ : SeminormedAddCommGroup V
inst✝¹⁹ : SeminormedAddCommGroup V₁
inst✝¹⁸ : SeminormedAddCommGroup V₂
inst✝¹⁷ : SeminormedAddCommGroup V₃
inst✝¹⁶ : SeminormedAddCommGroup V₄
inst✝¹⁵ : NormedSpace 𝕜 V
inst✝¹⁴ : NormedSpace 𝕜 V₁
inst✝¹³ : NormedSpace 𝕜 V₂
inst✝¹² : NormedSpace 𝕜 V₃
inst✝¹¹ : NormedSpace 𝕜 V₄
inst✝¹⁰ : PseudoMetricSpace P
inst✝⁹ : MetricSpace P₁
inst✝⁸ : PseudoMetricSpace P₂
inst✝⁷ : PseudoMetricSpace P₃
inst✝⁶ : PseudoMetricSpace P₄
inst✝⁵ : NormedAddTorsor V P
inst✝⁴ : NormedAddTorsor V₁ P₁
inst✝³ : NormedAddTorsor V₂ P₂
inst✝² : NormedAddTorsor V₃ P₃
inst✝¹ : NormedAddTorsor V₄ P₄
e : P ≃ᵃⁱ[𝕜] P₂
α : Type ?u.1897141
inst✝ : TopologicalSpace α
p : P
⊢ symm (constVSub 𝕜 p) = trans (LinearIsometryEquiv.toAffineIsometryEquiv (LinearIsometryEquiv.neg 𝕜)) (vaddConst 𝕜 p)
ext
no goals
case h
𝕜 : Type u_3
V : Type u_1
V₁ : Type ?u.1896593
V₂ : Type ?u.1896596
V₃ : Type ?u.1896599
V₄ : Type ?u.1896602
P₁ : Type ?u.1896605
P : Type u_2
P₂ : Type ?u.1896611
P₃ : Type ?u.1896614
P₄ : Type ?u.1896617
inst✝²¹ : NormedField 𝕜
inst✝²⁰ : SeminormedAddCommGroup V
inst✝¹⁹ : SeminormedAddCommGroup V₁
inst✝¹⁸ : SeminormedAddCommGroup V₂
inst✝¹⁷ : SeminormedAddCommGroup V₃
inst✝¹⁶ : SeminormedAddCommGroup V₄
inst✝¹⁵ : NormedSpace 𝕜 V
inst✝¹⁴ : NormedSpace 𝕜 V₁
inst✝¹³ : NormedSpace 𝕜 V₂
inst✝¹² : NormedSpace 𝕜 V₃
inst✝¹¹ : NormedSpace 𝕜 V₄
inst✝¹⁰ : PseudoMetricSpace P
inst✝⁹ : MetricSpace P₁
inst✝⁸ : PseudoMetricSpace P₂
inst✝⁷ : PseudoMetricSpace P₃
inst✝⁶ : PseudoMetricSpace P₄
inst✝⁵ : NormedAddTorsor V P
inst✝⁴ : NormedAddTorsor V₁ P₁
inst✝³ : NormedAddTorsor V₂ P₂
inst✝² : NormedAddTorsor V₃ P₃
inst✝¹ : NormedAddTorsor V₄ P₄
e : P ≃ᵃⁱ[𝕜] P₂
α : Type ?u.1897141
inst✝ : TopologicalSpace α
p : P
x✝ : V
⊢ ↑(symm (constVSub 𝕜 p)) x✝ =
    ↑(trans (LinearIsometryEquiv.toAffineIsometryEquiv (LinearIsometryEquiv.neg 𝕜)) (vaddConst 𝕜 p)) x✝
rfl