case H
E : Type u_3
PE : Type u_1
F : Type u_4
PF : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MetricSpace PE
inst✝⁴ : NormedAddTorsor E PE
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : MetricSpace PF
inst✝ : NormedAddTorsor F PF
f : PE ≃ᵢ PF
x✝ : PE
⊢ ↑(toIsometryEquiv (toRealAffineIsometryEquiv f)) x✝ = ↑f x✝
E : Type u_3
PE : Type u_1
F : Type u_4
PF : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MetricSpace PE
inst✝⁴ : NormedAddTorsor E PE
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : MetricSpace PF
inst✝ : NormedAddTorsor F PF
f : PE ≃ᵢ PF
⊢ toIsometryEquiv (toRealAffineIsometryEquiv f) = f
ext
no goals
case H
E : Type u_3
PE : Type u_1
F : Type u_4
PF : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MetricSpace PE
inst✝⁴ : NormedAddTorsor E PE
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : MetricSpace PF
inst✝ : NormedAddTorsor F PF
f : PE ≃ᵢ PF
x✝ : PE
⊢ ↑(toIsometryEquiv (toRealAffineIsometryEquiv f)) x✝ = ↑f x✝
rfl