case mk.mk
𝕜 : Type u_5
V : Type u_1
V₁ : Type ?u.25742
V₂ : Type u_2
V₃ : Type ?u.25748
V₄ : Type ?u.25751
P₁ : Type ?u.25754
P : Type u_3
P₂ : Type u_4
P₃ : Type ?u.25763
P₄ : Type ?u.25766
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₄
f✝ : P →ᵃⁱ[𝕜] P₂
f : P →ᵃ[𝕜] P₂
norm_map✝¹ : ∀ (x : V), ‖↑f.linear x‖ = ‖x‖
norm_map✝ : ∀ (x : V), ‖↑{ toAffineMap := f, norm_map := norm_map✝¹ }.toAffineMap.linear x‖ = ‖x‖
⊢ { toAffineMap := f, norm_map := norm_map✝¹ } =
    { toAffineMap := { toAffineMap := f, norm_map := norm_map✝¹ }.toAffineMap, norm_map := norm_map✝ }
𝕜 : Type u_5
V : Type u_1
V₁ : Type ?u.25742
V₂ : Type u_2
V₃ : Type ?u.25748
V₄ : Type ?u.25751
P₁ : Type ?u.25754
P : Type u_3
P₂ : Type u_4
P₃ : Type ?u.25763
P₄ : Type ?u.25766
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₄
f : P →ᵃⁱ[𝕜] P₂
⊢ Injective toAffineMap
rintro ⟨f, _⟩ ⟨g, _⟩ rfl
no goals
case mk.mk
𝕜 : Type u_5
V : Type u_1
V₁ : Type ?u.25742
V₂ : Type u_2
V₃ : Type ?u.25748
V₄ : Type ?u.25751
P₁ : Type ?u.25754
P : Type u_3
P₂ : Type u_4
P₃ : Type ?u.25763
P₄ : Type ?u.25766
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₄
f✝ : P →ᵃⁱ[𝕜] P₂
f : P →ᵃ[𝕜] P₂
norm_map✝¹ : ∀ (x : V), ‖↑f.linear x‖ = ‖x‖
norm_map✝ : ∀ (x : V), ‖↑{ toAffineMap := f, norm_map := norm_map✝¹ }.toAffineMap.linear x‖ = ‖x‖
⊢ { toAffineMap := f, norm_map := norm_map✝¹ } =
    { toAffineMap := { toAffineMap := f, norm_map := norm_map✝¹ }.toAffineMap, norm_map := norm_map✝ }
rfl