case inl
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type ?u.3812785
E : Type u_3
Eₗ : Type ?u.3812791
F : Type u_4
Fₗ : Type ?u.3812797
G : Type ?u.3812800
Gₗ : Type ?u.3812803
𝓕 : Type ?u.3812806
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedAddCommGroup G
inst✝⁹ : NormedAddCommGroup Fₗ
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜₂
inst✝⁶ : NontriviallyNormedField 𝕜₃
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst✝³ : RingHomInvPair σ₁₂ σ₂₁
inst✝² : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : RingHomIsometric σ₂₁
inst✝ : RingHomIsometric σ₁₂
e : E ≃SL[σ₁₂] F
_i : Subsingleton E
⊢ Subsingleton E ∨ 0 < ‖↑(ContinuousLinearEquiv.symm e)‖

case inr
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type ?u.3812785
E : Type u_3
Eₗ : Type ?u.3812791
F : Type u_4
Fₗ : Type ?u.3812797
G : Type ?u.3812800
Gₗ : Type ?u.3812803
𝓕 : Type ?u.3812806
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedAddCommGroup G
inst✝⁹ : NormedAddCommGroup Fₗ
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜₂
inst✝⁶ : NontriviallyNormedField 𝕜₃
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst✝³ : RingHomInvPair σ₁₂ σ₂₁
inst✝² : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : RingHomIsometric σ₂₁
inst✝ : RingHomIsometric σ₁₂
e : E ≃SL[σ₁₂] F
_i : Nontrivial E
⊢ Subsingleton E ∨ 0 < ‖↑(ContinuousLinearEquiv.symm e)‖
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type ?u.3812785
E : Type u_3
Eₗ : Type ?u.3812791
F : Type u_4
Fₗ : Type ?u.3812797
G : Type ?u.3812800
Gₗ : Type ?u.3812803
𝓕 : Type ?u.3812806
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedAddCommGroup G
inst✝⁹ : NormedAddCommGroup Fₗ
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜₂
inst✝⁶ : NontriviallyNormedField 𝕜₃
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst✝³ : RingHomInvPair σ₁₂ σ₂₁
inst✝² : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : RingHomIsometric σ₂₁
inst✝ : RingHomIsometric σ₁₂
e : E ≃SL[σ₁₂] F
⊢ Subsingleton E ∨ 0 < ‖↑(ContinuousLinearEquiv.symm e)‖
rcases subsingleton_or_nontrivial E with (_i | _i) <;> skip
case inl.h
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type ?u.3812785
E : Type u_3
Eₗ : Type ?u.3812791
F : Type u_4
Fₗ : Type ?u.3812797
G : Type ?u.3812800
Gₗ : Type ?u.3812803
𝓕 : Type ?u.3812806
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedAddCommGroup G
inst✝⁹ : NormedAddCommGroup Fₗ
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜₂
inst✝⁶ : NontriviallyNormedField 𝕜₃
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst✝³ : RingHomInvPair σ₁₂ σ₂₁
inst✝² : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : RingHomIsometric σ₂₁
inst✝ : RingHomIsometric σ₁₂
e : E ≃SL[σ₁₂] F
_i : Subsingleton E
⊢ Subsingleton E
case inl
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type ?u.3812785
E : Type u_3
Eₗ : Type ?u.3812791
F : Type u_4
Fₗ : Type ?u.3812797
G : Type ?u.3812800
Gₗ : Type ?u.3812803
𝓕 : Type ?u.3812806
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedAddCommGroup G
inst✝⁹ : NormedAddCommGroup Fₗ
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜₂
inst✝⁶ : NontriviallyNormedField 𝕜₃
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst✝³ : RingHomInvPair σ₁₂ σ₂₁
inst✝² : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : RingHomIsometric σ₂₁
inst✝ : RingHomIsometric σ₁₂
e : E ≃SL[σ₁₂] F
_i : Subsingleton E
⊢ Subsingleton E ∨ 0 < ‖↑(ContinuousLinearEquiv.symm e)‖
left
no goals
case inl.h
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type ?u.3812785
E : Type u_3
Eₗ : Type ?u.3812791
F : Type u_4
Fₗ : Type ?u.3812797
G : Type ?u.3812800
Gₗ : Type ?u.3812803
𝓕 : Type ?u.3812806
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedAddCommGroup G
inst✝⁹ : NormedAddCommGroup Fₗ
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜₂
inst✝⁶ : NontriviallyNormedField 𝕜₃
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst✝³ : RingHomInvPair σ₁₂ σ₂₁
inst✝² : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : RingHomIsometric σ₂₁
inst✝ : RingHomIsometric σ₁₂
e : E ≃SL[σ₁₂] F
_i : Subsingleton E
⊢ Subsingleton E
infer_instance
case inr.h
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type ?u.3812785
E : Type u_3
Eₗ : Type ?u.3812791
F : Type u_4
Fₗ : Type ?u.3812797
G : Type ?u.3812800
Gₗ : Type ?u.3812803
𝓕 : Type ?u.3812806
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedAddCommGroup G
inst✝⁹ : NormedAddCommGroup Fₗ
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜₂
inst✝⁶ : NontriviallyNormedField 𝕜₃
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst✝³ : RingHomInvPair σ₁₂ σ₂₁
inst✝² : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : RingHomIsometric σ₂₁
inst✝ : RingHomIsometric σ₁₂
e : E ≃SL[σ₁₂] F
_i : Nontrivial E
⊢ 0 < ‖↑(ContinuousLinearEquiv.symm e)‖
case inr
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type ?u.3812785
E : Type u_3
Eₗ : Type ?u.3812791
F : Type u_4
Fₗ : Type ?u.3812797
G : Type ?u.3812800
Gₗ : Type ?u.3812803
𝓕 : Type ?u.3812806
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedAddCommGroup G
inst✝⁹ : NormedAddCommGroup Fₗ
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜₂
inst✝⁶ : NontriviallyNormedField 𝕜₃
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst✝³ : RingHomInvPair σ₁₂ σ₂₁
inst✝² : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : RingHomIsometric σ₂₁
inst✝ : RingHomIsometric σ₁₂
e : E ≃SL[σ₁₂] F
_i : Nontrivial E
⊢ Subsingleton E ∨ 0 < ‖↑(ContinuousLinearEquiv.symm e)‖
right
no goals
case inr.h
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type ?u.3812785
E : Type u_3
Eₗ : Type ?u.3812791
F : Type u_4
Fₗ : Type ?u.3812797
G : Type ?u.3812800
Gₗ : Type ?u.3812803
𝓕 : Type ?u.3812806
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedAddCommGroup G
inst✝⁹ : NormedAddCommGroup Fₗ
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜₂
inst✝⁶ : NontriviallyNormedField 𝕜₃
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst✝³ : RingHomInvPair σ₁₂ σ₂₁
inst✝² : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : RingHomIsometric σ₂₁
inst✝ : RingHomIsometric σ₁₂
e : E ≃SL[σ₁₂] F
_i : Nontrivial E
⊢ 0 < ‖↑(ContinuousLinearEquiv.symm e)‖
exact e.norm_symm_pos