case h
𝕜 : Type u_1
V : Type ?u.375824
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type ?u.375833
V₄ : Type ?u.375836
P₁ : Type u_5
P : Type ?u.375842
P₂ : Type u_4
P₃ : Type ?u.375848
P₄ : Type ?u.375851
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₂
e : P₁ → P₂
e' : V₁ ≃ₗᵢ[𝕜] V₂
p : P₁
h : ∀ (p' : P₁), e p' = ↑e' (p' -ᵥ p) +ᵥ e p
x✝ : V₁
⊢ ↑(AffineIsometryEquiv.linearIsometryEquiv (mk' e e' p h)) x✝ = ↑e' x✝
𝕜 : Type u_1
V : Type ?u.375824
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type ?u.375833
V₄ : Type ?u.375836
P₁ : Type u_5
P : Type ?u.375842
P₂ : Type u_4
P₃ : Type ?u.375848
P₄ : Type ?u.375851
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₂
e : P₁ → P₂
e' : V₁ ≃ₗᵢ[𝕜] V₂
p : P₁
h : ∀ (p' : P₁), e p' = ↑e' (p' -ᵥ p) +ᵥ e p
⊢ AffineIsometryEquiv.linearIsometryEquiv (mk' e e' p h) = e'
ext
no goals
case h
𝕜 : Type u_1
V : Type ?u.375824
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type ?u.375833
V₄ : Type ?u.375836
P₁ : Type u_5
P : Type ?u.375842
P₂ : Type u_4
P₃ : Type ?u.375848
P₄ : Type ?u.375851
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₂
e : P₁ → P₂
e' : V₁ ≃ₗᵢ[𝕜] V₂
p : P₁
h : ∀ (p' : P₁), e p' = ↑e' (p' -ᵥ p) +ᵥ e p
x✝ : V₁
⊢ ↑(AffineIsometryEquiv.linearIsometryEquiv (mk' e e' p h)) x✝ = ↑e' x✝
rfl